legacy/oldpacking/ky_packing/UPFZBZM.hl

   1
   2 (* ========================================================================= *)
   3 (*                FLYSPECK - BOOK FORMALIZATION                              *)
   4 (*                                                                           *)
   5 (*      Authour   : VU KHAC KY                                               *)
   6 (*      Book lemma: UPFZBZM                                                  *)
   7 (*      Chaper    : Packing (Clusters)                                       *)
   8 (*      Date      : October 3, 2010                                          *)
   9 (*                                                                           *)
  10 (* ========================================================================= *)
  11
  12 (* ========================================================================= *)
  13 (*                     FILES NEED TO BE LOADED                               *)
  14 (* ========================================================================= *)
  15
  16 (* dmtcp: needs "flyspeck_load.hl";; *)
  17
  18 flyspeck_needs "nonlinear/vukhacky_tactics.hl";;
  19 flyspeck_needs "packing/pack_defs.hl";;
  20 flyspeck_needs "packing/pack_concl.hl";;
  21 flyspeck_needs "packing/beta_pair_thm.hl";;
  22 flyspeck_needs "packing/ky/UPFZBZM_support_lemmas.hl";;
  23 (* Note that UPFZBZM_support_lemmas.hl also load a file including unproved
  24    lemmas that need to be finished
  25 *)
  26
  27 module Upfzbzm = struct
  28
  29 open Pack_defs;;
  30 open Pack_concl;;
  31 open Vukhacky_tactics;;
  32
  33 (*-------------------------------------------------------------------------- *)
  34
  35  let UPFZBZM_concl =
  36    `!V.  saturated V /\ packing V /\ cell_cluster_estimate V /\
  37          marchal_inequality /\
  38          lmfun_inequality V ==>
  39     (?G. negligible_fun_0 G V /\ fcc_compatible G V)`;;
  40
  41 (* ------------------------------------------------------------------------- *)
  42
  43
  44
  45 (* ========================================================================= *)
  46 (*                            THE THEOREM                                    *)
  47 (* ========================================================================= *)
  48
  49 (* PART 1 OF THE LEMMA *)
  50
  51 let FCC_COMPATABILITY_FUNC = prove_by_refinement (
  52  `!V.  saturated V /\ packing V /\ cell_cluster_estimate V /\
  53    marchal_inequality /\
  54    lmfun_inequality V /\ G = (\u. --vol(voronoi_open V u) +
  55    &8 * mm1 - &8 * mm2 * sum { v | v IN V /\ ~(u=v) /\ dist(u,v) <= &2*h0 }
  56 (\v. lmfun (hl [u;v])))
  57 ==> fcc_compatible G V`,
  58
  59 [(REWRITE_TAC[lmfun_inequality;fcc_compatible]);
  60  (REPEAT STRIP_TAC);
  61  (ASM_REWRITE_TAC[REAL_ARITH `a + --a + b - c = b - c`]);
  62  (MATCH_MP_TAC (REAL_ARITH
  63   `x = &8 * mm1 - &8 * (&12 * mm2) /\ y <= &8 * (&12 * mm2) ==>
  64    x <= &8 * mm1 - y`));
  65  STRIP_TAC;
  66  (REWRITE_TAC[SQRT_OF_32_lemma]);
  67  (REWRITE_TAC[REAL_ARITH `a * b - a * c = a * (b - c)`]);
  68  (REWRITE_TAC[m1_minus_12m2]);
  69  (MATCH_MP_TAC REAL_LE_LMUL);
  70  (REWRITE_TAC[REAL_ARITH `&0 <= &8`]);
  71  (REWRITE_TAC[REAL_ARITH `&12 * mm2 = mm2 * &12`]);
  72  (MATCH_MP_TAC REAL_LE_LMUL);
  73  (REWRITE_TAC[ZERO_LE_MM2_LEMMA]);
  74  (ASM_MESON_TAC[])]);;
  75
  76
  77 (* ========================================================================= *)
  78
  79
  80 (* ========================================================================= *)
  81
  82 g `!V.  saturated V /\ packing V /\ cell_cluster_estimate V /\
  83    marchal_inequality /\
  84    lmfun_inequality V /\
  85   G = (\u. --vol(voronoi_open V u) +
  86    &8 * mm1 - &8 * mm2 * sum { v | v IN V /\ ~(u=v) /\ dist(u,v) <= &2*h0 }
  87 (\v. lmfun (hl [u;v])))
  88 ==> negligible_fun_0 G V`;;
  89
  90 e (REWRITE_TAC[negligible_fun_0; negligible_fun_any_C]);;
  91 e (REPEAT STRIP_TAC);;
  92 e (ASM_REWRITE_TAC[]);;
  93
  94 e (MP_TAC (SPEC `V:real^3->bool` KIZHLTL1));;
  95 e (DISCH_THEN (LABEL_TAC "asm1"));;
  96 e (USE_THEN "asm1" CHOOSE_TAC);;
  97
  98 e (MP_TAC (SPEC `V:real^3->bool`  KIZHLTL2));;
  99 e (DISCH_THEN (LABEL_TAC "asm2"));;
 100 e (USE_THEN "asm2" CHOOSE_TAC);;
 101
 102 (* ! It appears that the constant used in KIZHLTL3 needs to be changed.     *)
 103 (* ! Rather than prove indirectly, better to directly prove the  similar result for Lmfun, as in this adapted form of 'KIZHLTL3_concl' from 'packing/pack_concl.hl'
 104 (so if KIZHLTL3_concl is just for Ky's lemma, then this needs to change)
 105
 106 let KIZHLTL3_concl* = `!(V:real^3->bool) f. ?c. !r. saturated V /\ packing V /\ (&1 <= r) /\
 107   (?c1. !x.  &2 <= x /\ x < sqrt(&8) ==> abs( f x) <= c1)
 108    ==>
 109    (( &8 * mm2 /pi)*
 110          sum { X | X SUBSET ball(vec 0, r) /\  mcell_set V X }
 111             ( \ X.   sum (edgeX V X) ( \ {u,v}. (dihX V X (u ,v))*f (hl[u;v])))
 112                                           +c*r pow 2 <=
 113         &8*mm2 *
 114          sum (V INTER ball(vec 0,r))
 115            ( \u.  sum { v | v IN V /\ ~(u=v) /\ dist(u,v) < sqrt(&8)}
 116                ( \v.  lmfun (hl [u;v]))))`;;
 117
 118 ( and the ?c from here becomes c'' in the proof below )
 119
 120 ! instead of for F fun. The two have the same techinique:
 121
 122 *)
 123
 124 e (MP_TAC (SPEC `lmfun:real->real`(SPEC `V:real^3->bool` KIZHLTL3)));;
 125 e (DISCH_THEN (LABEL_TAC "asm3"));;
 126 e (USE_THEN "asm3" CHOOSE_TAC);;
 127
 128 e (MP_TAC (SPEC `V:real^3->bool` SUM_GAMMAX_LMFUM_ESTIMATE));;
 129 e (DISCH_THEN (LABEL_TAC "asm4"));;
 130 e (USE_THEN "asm4" CHOOSE_TAC);;
 131
 132 e (EXISTS_TAC `--(c + c' + c'' + c''')`);;
 133
 134 e (GEN_TAC THEN DISCH_TAC);;
 135 e (MP_TAC FINITE_PACK_LEMMA THEN DISCH_TAC);;
 136
 137 e (REWRITE_WITH `sum (V INTER ball (vec 0,r))
 138  (\u. --vol (voronoi_open V u) +
 139       &8 * mm1 -
 140       &8 *
 141       mm2 *
 142       sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 143       (\v. lmfun (hl [u; v]))) =
 144 sum (V INTER ball (vec 0,r))
 145  (\u. --vol (voronoi_open V u)) +
 146 sum (V INTER ball (vec 0,r))
 147  (\u.  &8 * mm1 -  &8 *
 148       mm2 *
 149       sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 150       (\v. lmfun (hl [u; v])))`);;
 151 e (MATCH_MP_TAC SUM_ADD);;
 152 e (ASM_SIMP_TAC[]);;
 153
 154 e (REWRITE_WITH `sum (V INTER ball (vec 0,r))
 155  (\u. &8 * mm1 -
 156       &8 *
 157       mm2 *
 158       sum {v:real^3 | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 159       (\v. lmfun (hl [u; v]))) =
 160 sum (V INTER ball (vec 0,r))
 161  (\u. &8 * mm1) -
 162 sum (V INTER ball (vec 0,r))
 163  (\u. &8 *
 164       mm2 *
 165       sum {v | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 166       (\v. lmfun (hl [u; v])))`);;
 167 e (MATCH_MP_TAC SUM_SUB);;
 168 e (ASM_SIMP_TAC[]);;
 169
 170 e (ASM_SIMP_TAC[SUM_NEG;SUM_CONST;SUM_LMUL]);;
 171 e (MATCH_MP_TAC (REAL_ARITH `--A <= x - y + z ==> --x + y - z <= A `));;
 172 e (REWRITE_TAC[REAL_ARITH `--(--x * y) = x * y`]);;
 173
 174 e (ABBREV_TAC `T1' = sum (V INTER ball (vec 0,r)) (\u. vol (voronoi_open V u))`);;
 175 e (ABBREV_TAC `T2' = &8 * &(CARD ((V:real^3 -> bool) INTER ball (vec 0,r))) * mm1`);;
 176 e (ABBREV_TAC `T3' = &8 *
 177       mm2 * sum (V INTER ball (vec 0,r))
 178  (\u. sum {v:real^3 | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 179       (\v. lmfun (hl [u; v])))`);;
 180
 181 e (ABBREV_TAC `B_0_r = {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X}`);;
 182
 183 e (ABBREV_TAC `T1 = sum B_0_r vol`);;
 184 e (ABBREV_TAC `T2 = --(&2 * mm1 / pi) * sum B_0_r (total_solid V)`);;
 185 e (ABBREV_TAC `T3 = (&8 * mm2 / pi) * sum B_0_r (\X. sum (edgeX V X)
 186                 (\({u, v}). dihX V X (u,v) * lmfun (hl [u; v])))`);;
 187
 188 e (MATCH_MP_TAC (REAL_ARITH
 189   `T1 + c * r pow 2 <= T1' /\
 190    T2 + c' * r pow 2 <= -- T2' /\
 191    T3 + c'' * r pow 2 <= T3' /\
 192    c''' * r pow 2 <= T1 + T2 + T3 ==>
 193   (c + c' + c'' + c''') * r pow 2 <= T1' - T2' + T3'`));;
 194 e (REPEAT STRIP_TAC);;
 195
 196 e (EXPAND_TAC "T1" THEN EXPAND_TAC "T1'");;
 197 e (EXPAND_TAC "B_0_r");;
 198 e (MP_TAC (ASSUME `!r. saturated V /\ packing V /\ &1 <= r
 199           ==> sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X} vol +
 200               c * r pow 2 <=
 201               sum (V INTER ball (vec 0,r)) (\u. vol (voronoi_open V u))`));;
 202 e (ASM_SIMP_TAC[]);;
 203
 204 e (EXPAND_TAC "T2" THEN EXPAND_TAC "T2'");;
 205 e (EXPAND_TAC "B_0_r");;
 206 e (MATCH_MP_TAC(REAL_ARITH `t + z <= x * y ==> --x * y + z <= --t`));;
 207 e (REWRITE_TAC[REAL_ARITH `a * b * c = b * a * c`]);;
 208 e (MP_TAC (ASSUME `!r. saturated V /\ packing V /\ &1 <= r
 209           ==> &(CARD (V INTER ball (vec 0,r))) * &8 * mm1 + c' * r pow 2 <=
 210               (&2 * mm1 / pi) *
 211               sum {X | X SUBSET ball (vec 0,r) /\ mcell_set V X}
 212               (total_solid V)`));;
 213 e (ASM_SIMP_TAC[]);;
 214
 215
 216
 217 (* !!!!! This part may then become very easy (maybe little more than a rewrite) *)
 218
 219 e (EXPAND_TAC "T3" THEN EXPAND_TAC "T3'");;
 220 e (EXPAND_TAC "B_0_r");;
 221 e (ABBREV_TAC `temp = &8 * mm2 *
 222    sum ((V:real^3->bool) INTER ball (vec 0,r))
 223    (\u. sum {v | v IN V /\ ~(u = v) /\ dist (u,v) < sqrt (&8)}
 224       (\v. lmfun (hl [u; v])))`);;
 225
 226 e (MATCH_MP_TAC (REAL_ARITH `(a <= temp /\ temp <= b) ==> a <= b`));;
 227 e STRIP_TAC;;
 228  (* Break into 2 subgoals *)
 229  (* First subgoal *)
 230
 231   e (EXPAND_TAC "temp");;
 232   e (MATCH_MP_TAC (ASSUME `!r. saturated V /\
 233            packing V /\
 234           &1 <= r /\
 235           (?c1. !x. &2 <= x /\ x < sqrt (&8) ==> abs (lmfun x) <= c1)
 236           ==> (&8 * mm2 / pi) *
 237              sum {X | (X:real^3 -> bool) SUBSET ball (vec 0,r) /\ mcell_set V X}
 238              (\X. sum (edgeX V X)
 239                   (\({u, v}). dihX V X (u,v) * lmfun (hl [u; v]))) +
 240              c'' * r pow 2 <=
 241              &8 *
 242              mm2 *
 243              sum ((V:real^3->bool) INTER ball (vec 0,r))
 244              (\u. sum {v | v IN V /\ ~(u = v) /\ dist (u,v) < sqrt (&8)}
 245                   (\v. lmfun (hl [u; v])))`));;
 246
 247   e (ASM_SIMP_TAC[]);;
 248   e (EXISTS_TAC `&1`);;
 249   e (GEN_TAC THEN DISCH_TAC);;
 250   e (REWRITE_TAC[lmfun]);;
 251   e (COND_CASES_TAC);;
 252   e (UP_ASM_TAC THEN UP_ASM_TAC);;
 253   e (REWRITE_TAC[h0]);;
 254   e (MESON_TAC[REAL_ARITH `&2 <= x /\ x < sqrt (&8) ==> x <= #1.26 ==> F`]);;
 255   e (REAL_ARITH_TAC);;
 256
 257   (* second subgoal *)
 258   e (EXPAND_TAC "temp");;
 259   e (REWRITE_TAC[REAL_ARITH `a * b * c = (a * b) * c`]);;
 260   e (MATCH_MP_TAC REAL_LE_LMUL);;
 261   e (STRIP_TAC);;
 262   e (MATCH_MP_TAC REAL_LE_MUL);;
 263   e (REWRITE_TAC[REAL_ARITH `&0 <= &8`;ZERO_LE_MM2_LEMMA]);;
 264   e (MATCH_MP_TAC SUM_LE);;
 265
 266     e (STRIP_TAC);;
 267     e (ASM_SIMP_TAC[]);;
 268     e (GEN_TAC THEN DISCH_TAC);;
 269     e (REWRITE_TAC[IN_ELIM_THM]);;
 270     e (ABBREV_TAC
 271       `temp_s1 = {v:real^3 | v IN V /\ ~(x = v) /\ dist (x,v) < sqrt (&8)}`);;
 272     e (ABBREV_TAC
 273       `temp_s2 = {v:real^3 | v IN V /\ ~(x = v) /\ dist (x,v) <= &2 * h0}`);;
 274     e (MATCH_MP_TAC SUM_SUBSET_SIMPLE);;
 275     e (REPEAT STRIP_TAC);;
 276     (* Break into 3 subgoals *)
 277
 278       (* First subgoal *)
 279       e (NEW_GOAL `temp_s2 SUBSET (V INTER ball (x:real^3, &10))`);;
 280       e (EXPAND_TAC "temp_s2");;
 281       e (REWRITE_TAC[SUBSET]);;
 282       e (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM;IN_INTER] THEN DISCH_TAC);;
 283       e (ASM_SIMP_TAC[ball;IN_ELIM_THM]);;
 284       e (MATCH_MP_TAC
 285         (REAL_ARITH `&2 * h0 < &10 /\ a <= &2 * h0 ==> a < &10`));;
 286       e (ASM_REWRITE_TAC[h0] THEN REAL_ARITH_TAC);;
 287       e (NEW_GOAL `FINITE (V INTER ball (x:real^3,&10))`);;
 288       e (ASM_SIMP_TAC[]);;
 289       e (UP_ASM_TAC THEN UP_ASM_TAC THEN MESON_TAC[FINITE_SUBSET]);;
 290
 291       (* Second subgoal *)
 292       e (EXPAND_TAC "temp_s1" THEN EXPAND_TAC "temp_s2");;
 293       e (REWRITE_TAC[SUBSET;IN_ELIM_THM]);;
 294       e (GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[h0]);;
 295       e (MATCH_MP_TAC
 296         (REAL_ARITH `x < sqrt(&8) /\ sqrt(&8) < y ==> x <= y`));;
 297       e (ASM_REWRITE_TAC[h0]);;
 298
 299 e CHEAT_TAC;;  (* ! Because it isn't true at all - see KIZHLTL3 above *)
 300 e CHEAT_TAC;;
 301
 302 (* !!!!! End of part that will become very easy  *)
 303
 304
 305
 306  (* ! There is a serious logical mistake here, we have to fix it right away *)
 307
 308
 309 e (REWRITE_WITH `T1 + T2 + T3 =
 310   sum B_0_r (\X:real^3->bool. gammaX V X lmfun)`);;
 311 e (SUBGOAL_THEN `FINITE (B_0_r:(real^3->bool)->bool)` ASSUME_TAC);;
 312 e (EXPAND_TAC "B_0_r");;
 313 e (REWRITE_TAC[FINITE_MCELL_SET_LEMMA]);;
 314
 315 e (SUBGOAL_THEN
 316   `sum B_0_r (\X. gammaX V X lmfun) =
 317    sum B_0_r (\X. vol X - (&2 * mm1 / pi) * total_solid V X) +
 318    sum B_0_r
 319    (\X. (&8 * mm2 / pi) *
 320         sum (edgeX V X) (\({u, v}). dihX V X (u,v) * lmfun (hl [u; v])))`
 321    ASSUME_TAC);;
 322 e (REWRITE_TAC[gammaX]);;
 323 e (MATCH_MP_TAC SUM_ADD);;
 324 e (ASM_REWRITE_TAC[]);;
 325 e (SUBGOAL_THEN
 326    `sum B_0_r (\X. vol X - (&2 * mm1 / pi) * total_solid V X) =
 327     sum B_0_r (\X. vol X) - sum B_0_r (\X. (&2 * mm1 / pi) * total_solid V X)`
 328   ASSUME_TAC);;
 329 e (ABBREV_TAC `temp1 = (\X. (&2 * mm1 / pi) * total_solid V X)`);;
 330 e (ABBREV_TAC `temp2:(real^3->bool)->real = (\X. vol X)`);;
 331
 332 e (REWRITE_WITH `(\X. vol X - (&2 * mm1 / pi) * total_solid V X) =
 333                  (\X. temp2 X - temp1 X)`);;
 334 e (EXPAND_TAC "temp1" THEN EXPAND_TAC "temp2" THEN REWRITE_TAC[]);;
 335 e (MATCH_MP_TAC SUM_SUB);;
 336 e (ASM_REWRITE_TAC[]);;
 337
 338 e (ASM_REWRITE_TAC[]);;
 339 e (EXPAND_TAC "T1" THEN EXPAND_TAC "T2" THEN EXPAND_TAC "T3");;
 340 e (MATCH_MP_TAC (REAL_ARITH ` x1 = x2 /\ --y1 = y2 /\ z1 = z2 ==>
 341                               x1 + y1 + z1 = x2 - y2 + z2`));;
 342 e (REPEAT STRIP_TAC);;
 343 e (MATCH_MP_TAC SUM_EQ);;
 344 e (GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[IN_ELIM_THM]);;
 345 e (REWRITE_TAC[REAL_ARITH `--(--x * y) = x * y`]);;
 346 e (REWRITE_TAC[SUM_LMUL]);;
 347 e (REWRITE_TAC[REAL_EQ_MUL_LCANCEL]);;
 348 e (DISJ2_TAC);;
 349 e (MATCH_MP_TAC SUM_EQ);;
 350 e (GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[IN_ELIM_THM]);;
 351 e (REWRITE_TAC[SUM_LMUL]);;
 352 e (EXPAND_TAC "B_0_r");;
 353
 354 e (ASM_SIMP_TAC[]);;
 355
 356 let NEGLIGIBLE_FUNC = top_thm();;
 357
 358 (* ========================================================================= *)
 359 (*             Main theorm                                                   *)
 360 (* ========================================================================= *)
 361
 362 let UPFZBZM = prove (UPFZBZM_concl,
 363  (REPEAT STRIP_TAC) THEN (ABBREV_TAC `G = (\u. --vol (voronoi_open V u) +
 364               &8 * mm1 -
 365               &8 *
 366               mm2 *
 367               sum {v:real^3 | v IN V /\ ~(u = v) /\ dist (u,v) <= &2 * h0}
 368               (\v. lmfun (hl [u; v])))`) THEN
 369  (EXISTS_TAC `G:real^3->real`) THEN
 370  (ASM_MESON_TAC[NEGLIGIBLE_FUNC;FCC_COMPATABILITY_FUNC]));;
 371
 372
 373
 374 (* ========================================================================== *)
 375 (*               Continue back up of complementary lemmas                     *)
 376 (* ========================================================================== *)
 377
 378 let SUM_GAMMAX_LMFUM_ESTIMATE_concl =
 379   `!V. ?c. !r. saturated V /\ packing V /\ &1 <= r /\
 380                cell_cluster_estimate V /\ marchal_inequality /\
 381                lmfun_inequality V ==>
 382     c * r pow 2 <=  sum {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X}
 383     (\X. gammaX V X lmfun)`;;
 384
 385 (* ----------------------  We prove it below ------------------------------- *)
 386
 387 g SUM_GAMMAX_LMFUM_ESTIMATE_concl;;
 388 e (GEN_TAC);;
 389 e (EXISTS_TAC `c:real`);;
 390 e (REPEAT STRIP_TAC);;
 391
 392 e (SUBGOAL_THEN `!X. (critical_edgeX V X  = {}) ==>
 393      (!u v:real^3. {u, v} IN edgeX V X ==>
 394      lmfun (hl [u; v]) >= marchal (hl [u ; v]))`  ASSUME_TAC);;
 395 e (REPEAT STRIP_TAC);;
 396 e (SUBGOAL_THEN `~(hminus <= hl [u:real^3; v] /\ hl [u; v] <= hplus)`
 397    ASSUME_TAC);;
 398 e STRIP_TAC;;
 399 e (SUBGOAL_THEN `critical_edgeX V X {u, v}` ASSUME_TAC);;
 400 e (REWRITE_TAC[critical_edgeX]);;
 401 e (REWRITE_TAC[IN_ELIM_THM]);;
 402 e (EXISTS_TAC `u:real^3`);;
 403 e (EXISTS_TAC `v:real^3`);;
 404 e (ASM_REWRITE_TAC[]);;
 405 e (SUBGOAL_THEN `~ (critical_edgeX V X = {})` ASSUME_TAC);;
 406 e (UP_ASM_TAC);;
 407 e (SET_TAC[]);;
 408 e (ASM_MESON_TAC[]);;
 409 e (ASM_SIMP_TAC[lmfun_vs_marchal]);;
 410
 411 (*  We have already proved that :
 412
 413 !X. critical_edgeX V X = {}
 414           ==> (!u v.
 415                    {u, v} IN edgeX V X
 416                    ==> lmfun (hl [u; v]) >= marchal (hl [u; v]))
 417 *)
 418
 419 e (SUBGOAL_THEN
 420   `!X. mcell_set V X /\ (critical_edgeX V X  = {}) ==> gammaX V X lmfun >= &0` ASSUME_TAC);;
 421 e (REPEAT STRIP_TAC);;
 422 e (MATCH_MP_TAC (REAL_ARITH
 423   `a >= gammaX V X marchal /\ gammaX V X marchal >= &0 ==> a >= &0`));;
 424 e CONJ_TAC;;
 425
 426   (* break into 2 small part *)
 427
 428 e (REWRITE_TAC[gammaX]);;
 429 e (MATCH_MP_TAC (REAL_ARITH `a <= b ==> x - y + b >= x - y + a`));;
 430 e (MATCH_MP_TAC REAL_LE_LMUL);;
 431 e STRIP_TAC;;
 432 e (MATCH_MP_TAC REAL_LE_MUL);;
 433 e CONJ_TAC;;
 434 e REAL_ARITH_TAC;;
 435 e (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));;
 436 e (MATCH_MP_TAC REAL_LT_DIV);;
 437 e (REWRITE_TAC[PI_POS;ZERO_LT_MM2_LEMMA]);;
 438
 439 e (MATCH_MP_TAC SUM_LE);;
 440 e (REWRITE_TAC[FINITE_edgeX]);;
 441 e (REWRITE_TAC[edgeX;IN_ELIM_THM]);;
 442 e (REPEAT STRIP_TAC);;
 443 e (REWRITE_TAC[ASSUME `x = {u:real^3, v}`;BETA_THM]);;
 444
 445 e (REWRITE_WITH `(\({u, v}). dihX V X (u,v) * marchal (hl [u; v])) {u, v} =
 446                  dihX V X (u,v) * marchal (hl [u; v])`);;
 447 e (MATCH_MP_TAC BETA_PAIR_THM);;
 448
 449 e (REWRITE_TAC[HL;DIHX_SYM]);;
 450 e (REPEAT GEN_TAC);;
 451 e (REWRITE_WITH `set_of_list [u':real^3; v'] = set_of_list [v'; u']`);;
 452 e (REWRITE_TAC[set_of_list]);;
 453 e (SET_TAC[]);;
 454
 455 e (REWRITE_WITH `(\({u, v}). dihX V X (u,v) * lmfun (hl [u; v])) {u, v} =
 456                  dihX V X (u,v) * lmfun (hl [u; v])`);;
 457 e (MATCH_MP_TAC BETA_PAIR_THM);;
 458
 459 e (REWRITE_TAC[HL;DIHX_SYM]);;
 460 e (REPEAT GEN_TAC);;
 461 e (REWRITE_WITH `set_of_list [u':real^3; v'] = set_of_list [v'; u']`);;
 462 e (REWRITE_TAC[set_of_list]);;
 463 e (SET_TAC[]);;
 464
 465 e (MATCH_MP_TAC (REAL_ARITH `&0 <= a * ( y - x) ==> a * x <= a * y`));;
 466 e (MATCH_MP_TAC REAL_LE_MUL);;
 467 e STRIP_TAC;;
 468 e (REWRITE_TAC[DIHX_POS]);;
 469 e (MATCH_MP_TAC (REAL_ARITH `a >= b ==> &0 <= a - b`));;
 470 e (NEW_GOAL `{u, v} IN edgeX V X`);;
 471 e (ASM_REWRITE_TAC[edgeX]);;
 472 e (DEL_TAC THEN REPLICATE_TAC 3 UP_ASM_TAC THEN SET_TAC[]);;
 473 e (ASM_MESON_TAC[]);;
 474
 475 e (MP_TAC (ASSUME `marchal_inequality`));;
 476 e (REWRITE_TAC[marchal_inequality]);;
 477 e (DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC);;
 478 e (ASM_REWRITE_TAC[]);;
 479
 480 (* ------------------------------------------------------------------------ *)
 481
 482 e (ABBREV_TAC `B_0_r = {X | X SUBSET ball (vec 0, r)  /\ mcell_set V X}`);;
 483 e (ABBREV_TAC `B_0_r_empty = B_0_r INTER {X| critical_edgeX V X = {}}`);;
 484 e (ABBREV_TAC `B_0_r_no_empty = B_0_r INTER {X| ~(critical_edgeX V X = {})}`);;
 485
 486 e (SUBGOAL_THEN
 487   `B_0_r:(real^3->bool)->bool = B_0_r_empty UNION B_0_r_no_empty` ASSUME_TAC);;
 488 e (EXPAND_TAC "B_0_r_empty");;
 489 e (EXPAND_TAC "B_0_r_no_empty");;
 490 e (EXPAND_TAC "B_0_r");;
 491 e (SET_TAC[]);;
 492 e (ASM_REWRITE_TAC[]);;
 493
 494 e (SUBGOAL_THEN `FINITE (B_0_r:(real^3->bool)->bool)` ASSUME_TAC);;
 495 e (EXPAND_TAC "B_0_r");;
 496 e (REWRITE_TAC[FINITE_MCELL_SET_LEMMA]);;
 497
 498 e (SUBGOAL_THEN `FINITE (B_0_r_empty:(real^3->bool)->bool)` ASSUME_TAC);;
 499 e (MATCH_MP_TAC FINITE_SUBSET);;
 500 e (EXISTS_TAC `(B_0_r:(real^3->bool)->bool)`);;
 501 e (ASM_REWRITE_TAC[]);;
 502 e (SET_TAC[]);;
 503
 504 e (SUBGOAL_THEN `FINITE (B_0_r_no_empty:(real^3->bool)->bool)` ASSUME_TAC);;
 505 e (MATCH_MP_TAC FINITE_SUBSET);;
 506 e (EXISTS_TAC `(B_0_r:(real^3->bool)->bool)`);;
 507 e (ASM_REWRITE_TAC[]);;
 508 e (SET_TAC[]);;
 509
 510 e (SUBGOAL_THEN `DISJOINT B_0_r_empty (B_0_r_no_empty:(real^3->bool)->bool)` ASSUME_TAC);;
 511 e (REWRITE_TAC[IN_DISJOINT]);;
 512 e (EXPAND_TAC "B_0_r_empty" THEN EXPAND_TAC "B_0_r_no_empty");;
 513 e (STRIP_TAC);;
 514 e (SUBGOAL_THEN `x IN {X | critical_edgeX V X = {}}` ASSUME_TAC);;
 515 e (DEL_TAC THEN UP_ASM_TAC THEN SET_TAC[]);;
 516 e (SUBGOAL_THEN `x IN {X | ~(critical_edgeX V X = {})}` ASSUME_TAC);;
 517 e (DEL_TAC THEN UP_ASM_TAC THEN SET_TAC[]);;
 518 e (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);;
 519
 520 e (REWRITE_WITH
 521   `sum (B_0_r_empty UNION B_0_r_no_empty) (\X. gammaX V X lmfun) =
 522    sum (B_0_r_empty) (\X. gammaX V X lmfun) +
 523    sum (B_0_r_no_empty) (\X. gammaX V X lmfun)`);;
 524 e (MATCH_MP_TAC SUM_UNION);;
 525 e (ASM_REWRITE_TAC[]);;
 526
 527 e (SUBGOAL_THEN `&0 <= sum B_0_r_empty (\X. gammaX V X lmfun)` ASSUME_TAC);;
 528 e (MATCH_MP_TAC SUM_POS_LE);;
 529 e STRIP_TAC;;
 530
 531     e (ASM_REWRITE_TAC[]);;
 532     e (EXPAND_TAC "B_0_r_empty");;
 533     e (EXPAND_TAC "B_0_r");;
 534     e (REWRITE_TAC[REAL_ARITH `&0 <= x <=> x >= &0`]);;
 535     e (MP_TAC (ASSUME
 536       `!X. mcell_set V X /\ critical_edgeX V X = {} ==>
 537         gammaX V X lmfun >= &0`));;
 538     e (SET_TAC[]);;
 539
 540 e (MATCH_MP_TAC (REAL_ARITH `x <= a /\ &0 <= b ==> x <= b + a`));;
 541 e (ASM_REWRITE_TAC[]);;
 542
 543 e (REWRITE_WITH
 544   `sum B_0_r_no_empty (\X. gammaX V X lmfun) =
 545    sum B_0_r (\X. (gammaX V X lmfun) *
 546    sum (critical_edgeX V X) (\e. critical_weight V X))`);;
 547 e (ASM_REWRITE_TAC[]);;
 548
 549 e (REWRITE_WITH
 550 `sum (B_0_r_empty UNION B_0_r_no_empty)
 551  (\X. gammaX V X lmfun * sum (critical_edgeX V X) (\e. critical_weight V X)) =
 552  sum B_0_r_empty
 553  (\X. gammaX V X lmfun * sum (critical_edgeX V X) (\e. critical_weight V X)) +
 554  sum B_0_r_no_empty
 555  (\X. gammaX V X lmfun * sum (critical_edgeX V X) (\e. critical_weight V X))`
 556 );;
 557 e (MATCH_MP_TAC SUM_UNION);;
 558 e (ASM_REWRITE_TAC[]);;
 559
 560 e (SUBGOAL_THEN
 561  `sum B_0_r_empty
 562   (\X. gammaX V X lmfun * sum (critical_edgeX V X)
 563   (\e. critical_weight V X)) = &0` ASSUME_TAC);;
 564 e (MATCH_MP_TAC SUM_EQ_0);;
 565 e (EXPAND_TAC "B_0_r_empty");;
 566 e (GEN_TAC THEN REWRITE_TAC[IN_INTER;IN_ELIM_THM]);;
 567 e (STRIP_TAC);;
 568 e (MATCH_MP_TAC (MESON[REAL_MUL_RZERO] `x = &0 ==> y * x = &0`));;
 569 e (MATCH_MP_TAC (MESON[SUM_CLAUSES] `x = {} ==> sum x f = &0`));;
 570 e (ASM_REWRITE_TAC[]);;
 571
 572
 573 e (ASM_REWRITE_TAC[REAL_ADD_LID]);;
 574 e (MATCH_MP_TAC (SUM_EQ));;
 575 e GEN_TAC;;
 576 e (EXPAND_TAC "B_0_r_no_empty" THEN EXPAND_TAC "B_0_r");;
 577 e (REWRITE_TAC[IN_INTER;IN_ELIM_THM]);;
 578 e DISCH_TAC;;
 579 e (MATCH_MP_TAC (MESON[REAL_MUL_RID] `x = &1 ==> y = y * x`));;
 580 e (REWRITE_TAC[critical_weight]);;
 581 e (SUBGOAL_THEN )
 582 e (SIMP_TAC[SUM_CONST]);;
 583 e (NEW_GOAL `FINITE (critical_edgeX V x)`);;
 584 e (ASM_SIMP_TAC[FINITE_critical_edgeX]);;
 585 e (ASM_SIMP_TAC[SUM_CONST]);;
 586 e (REWRITE_TAC[REAL_ARITH `a * &1 / a = (a * &1) / a`; REAL_MUL_RID]);;
 587 e (MATCH_MP_TAC REAL_DIV_REFL);;
 588 e (MATCH_MP_TAC (MESON[REAL_OF_NUM_EQ] `~(x = 0) ==> ~ (&x = &0)`));;
 589 e (UP_ASM_TAC THEN UP_ASM_TAC);;
 590 e (MESON_TAC[CARD_EQ_0]);;
 591
 592 (* ------------------------------------------------------------------------- *)
 593
 594 e (ABBREV_TAC
 595  `temp_set = {e:real^3->bool | (?X. X IN B_0_r /\ e IN critical_edgeX V X)}`);;
 596 e (SUBGOAL_THEN `FINITE (temp_set:(real^3->bool)->bool)` ASSUME_TAC);;
 597 e CHEAT_TAC;;
 598
 599   (* Used CHEAT_TAC here. But it seems to be easy *)
 600
 601 e (REWRITE_WITH
 602  `sum B_0_r
 603  (\X. gammaX V X lmfun *
 604       sum (critical_edgeX V X) (\e. critical_weight V X)) =
 605   sum B_0_r
 606  (\X. sum (critical_edgeX V X) (\e. gammaX V X lmfun * critical_weight V X))`);;
 607 e (REWRITE_TAC[GSYM SUM_LMUL]);;
 608
 609 e (REWRITE_WITH
 610  `sum B_0_r
 611  (\X. sum (critical_edgeX V X) (\e. gammaX V X lmfun * critical_weight V X)) =
 612   sum B_0_r
 613  (\X. sum {e | e IN temp_set /\ critical_edgeX V X e}
 614  (\e. gammaX V X lmfun * critical_weight V X))`);;
 615 e (MATCH_MP_TAC SUM_EQ);;
 616 e (GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[IN_ELIM_THM]);;
 617 e (MATCH_MP_TAC (MESON[] `(s = r) ==> sum s f = sum r f`));;
 618 e (REWRITE_TAC[SET_RULE
 619  `(X = Y) <=> (!x. (x IN X ==> x IN Y) /\ (x IN Y ==> x IN X))`]);;
 620 e (GEN_TAC THEN STRIP_TAC);;
 621 e (REWRITE_TAC[IN_ELIM_THM]);;
 622 e (REPEAT STRIP_TAC);;
 623 e (EXPAND_TAC "temp_set" THEN REWRITE_TAC[IN_ELIM_THM]);;
 624 e (EXISTS_TAC `x:real^3 -> bool`);;
 625 e (ASM_REWRITE_TAC[]);;
 626 e (UP_ASM_TAC THEN SET_TAC[]);;
 627 e (REWRITE_TAC[IN_ELIM_THM]);;
 628 e (SET_TAC[]);;
 629 e (REWRITE_WITH
 630  `sum B_0_r
 631   (\X. sum {e | e IN temp_set /\ critical_edgeX V X e}
 632       (\e. gammaX V X lmfun * critical_weight V X)) =
 633   sum temp_set
 634  (\e. sum {X | X IN B_0_r /\ critical_edgeX V X e}
 635       (\X. gammaX V X lmfun * critical_weight V X))`);;
 636 e (MATCH_MP_TAC SUM_SUM_RESTRICT);;
 637 e (ASM_REWRITE_TAC[]);;
 638
 639
 640 (* need to continue *)
 641
 642
 643
 644 (*-------------------- The lemma about sum of beta_bump ---------------------*)
 645
 646
 647 g `!V X. saturated V /\ packing V /\ mcell_set V X ==>
 648          sum {e | e IN critical_edgeX V X } (\e. beta_bump V e X) = &0`;;
 649 e (REPEAT STRIP_TAC THEN UP_ASM_TAC);;
 650 e (REWRITE_TAC[mcell_set; IN_ELIM_THM]);;
 651 e (DISCH_TAC);;
 652 e (REWRITE_TAC[beta_bump]);;
 653 e (REPEAT LET_TAC);;
 654 e (ASM_CASES_TAC `~(k = 4)`);;
 655
 656    (* Two case. Here is CASE 1*)
 657
 658 e (NEW_GOAL `!e. sum
 659       {e',e'',p,vl | k = 4 /\
 660                      critical_edgeX V X = {e', e''} /\
 661                      e = e' /\
 662                      p permutes 0..3 /\
 663                      vl = left_action_list p ul /\
 664                      e' = {EL 0 vl, EL 1 vl} /\
 665                      e'' = {EL 2 vl, EL 3 vl}}
 666       (\(e',e'',p,vl). (bump (hl [EL 0 vl; EL 1 vl]) -
 667                         bump (hl [EL 2 vl; EL 3 vl])) /
 668                        &4) = &0`);;
 669 e GEN_TAC;;
 670 e (ABBREV_TAC `SET1 = {e',e'',p,vl | k = 4 /\
 671                     critical_edgeX V X = {e', e''} /\
 672                     e = e' /\
 673                     p permutes 0..3 /\
 674                     vl = left_action_list p ul /\
 675                     e' = {EL 0 vl, EL 1 vl} /\
 676                     e'' = {EL 2 vl, EL 3 vl}}`);;
 677
 678 e (NEW_GOAL
 679   `SET1:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->bool = {}`);;
 680 e (EXPAND_TAC "SET1");;
 681 e (MP_TAC (ASSUME `~(k = 4)`));;
 682 e (SET_TAC[]);;
 683 e (ASM_REWRITE_TAC[]);;
 684 e (ASM_REWRITE_TAC[SUM_CLAUSES]);;
 685 e (ASM_REWRITE_TAC[SUM_0]);;
 686
 687   (* Here is case 2 *)
 688
 689 e (NEW_GOAL `k = 4`);;
 690 e (UP_ASM_TAC THEN MESON_TAC[]);;
 691 e (SWITCH_TAC THEN DEL_TAC);;
 692 e (SWITCH_TAC);;
 693 e (UP_ASM_TAC THEN REWRITE_TAC[cell_params]);;
 694 e DISCH_TAC;;
 695
 696 (* ------------------------------------------------------------------------ *)
 697
 698 e (NEW_GOAL `k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul`);;
 699 e (NEW_GOAL ` (?k ul. k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul) /\ ((@(k,ul). k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul) = k,ul)`);;
 700 e (ASM_REWRITE_TAC[]);;
 701 e (CHOOSE_TAC (ASSUME `?i ul. X = mcell i V ul /\ ul IN barV V 3`));;
 702 e (CHOOSE_TAC (ASSUME `?ul. X = mcell i V ul /\ ul IN barV V 3`));;
 703 e (ASM_CASES_TAC `i <= 4`);;
 704 e (EXISTS_TAC `i:num`);;
 705 e (EXISTS_TAC `ul':(real^3) list`);;
 706 e (ASM_REWRITE_TAC[]);;
 707
 708 e (EXISTS_TAC `4`);;
 709 e (EXISTS_TAC `ul':(real^3) list`);;
 710 e (ASM_REWRITE_TAC[ARITH_RULE `4 <= 4`]);;
 711 e (REWRITE_TAC[mcell]);;
 712 e (COND_CASES_TAC);;
 713 e (UP_ASM_TAC THEN UP_ASM_TAC);;
 714 e (MESON_TAC[ARITH_RULE `~(i <= 4) ==> (i = 0) ==> F`]);;
 715 e (DEL_TAC);;
 716 e (COND_CASES_TAC);;
 717 e (UP_ASM_TAC THEN UP_ASM_TAC);;
 718 e (MESON_TAC[ARITH_RULE `~(i <= 4) ==> (i = 1) ==> F`]);;
 719 e (DEL_TAC);;
 720 e (COND_CASES_TAC);;
 721 e (UP_ASM_TAC THEN UP_ASM_TAC);;
 722 e (MESON_TAC[ARITH_RULE `~(i <= 4) ==> (i = 2) ==> F`]);;
 723 e (DEL_TAC);;
 724 e (COND_CASES_TAC);;
 725 e (UP_ASM_TAC THEN UP_ASM_TAC);;
 726 e (MESON_TAC[ARITH_RULE `~(i <= 4) ==> (i = 3) ==> F`]);;
 727 e (DEL_TAC);;
 728 e (COND_CASES_TAC);;
 729 e (UP_ASM_TAC THEN MESON_TAC[ARITH_RULE `4 = 0 ==> F`]);;
 730 e (COND_CASES_TAC);;
 731 e (UP_ASM_TAC THEN MESON_TAC[ARITH_RULE `4 = 1 ==> F`]);;
 732 e (COND_CASES_TAC);;
 733 e (UP_ASM_TAC THEN MESON_TAC[ARITH_RULE `4 = 2 ==> F`]);;
 734 e (COND_CASES_TAC);;
 735 e (UP_ASM_TAC THEN MESON_TAC[ARITH_RULE `4 = 3 ==> F`]);;
 736 e (REWRITE_TAC[]);;
 737 e (UP_ASM_TAC);;
 738
 739 e (ABBREV_TAC `P = (\k. k <= 4)`);;
 740 e (ABBREV_TAC `Q = (\ul. ul IN barV V 3)`);;
 741 e (ABBREV_TAC `R = (\k ul. X = mcell k V ul)`);;
 742
 743 e (REWRITE_WITH
 744 `(?k ul. k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul) /\
 745  (@(k,ul). k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul) = k,ul
 746  ==> k <= 4 /\ ul IN barV V 3 /\ X = mcell k V ul <=>
 747  (?k ul. P k /\ Q ul /\ R k ul) /\ (@(k,ul). P k /\ Q ul /\ R k ul) = k,ul
 748  ==> P k /\ Q ul /\ R k ul`);;
 749 e (EXPAND_TAC "P" THEN EXPAND_TAC "Q" THEN EXPAND_TAC "R");;
 750 e (REWRITE_TAC[IN_ELIM_THM]);;
 751 e (REWRITE_TAC[JOHN_SELECT_THM]);;
 752 e (UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN DEL_TAC THEN REPEAT STRIP_TAC);;
 753 e (UP_ASM_TAC THEN UP_ASM_TAC THEN DEL_TAC THEN REPEAT STRIP_TAC);;
 754
 755 (* ------------------------------------------------------------------------- *)
 756
 757 e (REWRITE_WITH `{e | e IN critical_edgeX V X} = critical_edgeX V X`);;
 758 e (SET_TAC[]);;
 759 e (ASM_CASES_TAC `?e e'. ~ (e = e') /\ critical_edgeX V X = {e , e'}`);;
 760 e (CHOOSE_TAC (ASSUME `?e e'. ~ (e = e') /\ critical_edgeX V X = {e, e'}`));;
 761 e (CHOOSE_TAC (ASSUME `?e'. ~ (e = e') /\ critical_edgeX V X = {e, e'}`));;
 762 e (UP_ASM_TAC THEN DEL_TAC THEN DEL_TAC THEN DISCH_TAC);;
 763
 764 e (ASM_SIMP_TAC [SUM_SET_OF_2_ELEMENTS]);;
 765 e (ABBREV_TAC `K1 = {e'',e''',p,(vl:(real^3)list) | {e, e'} = {e'', e'''} /\
 766                   e' = e'' /\
 767                   p permutes 0..3 /\
 768                   vl = left_action_list p ul /\
 769                   e'' = {EL 0 vl, EL 1 vl} /\
 770                   e''' = {EL 2 vl, EL 3 vl}}`);;
 771 e (REWRITE_WITH
 772 ` sum (K1:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->bool)
 773  (\(e',e'',p,vl). (bump (hl [EL 0 vl; EL 1 vl]) -
 774                    bump (hl [EL 2 vl; EL 3 vl])) /
 775                   &4) =
 776  sum K1 (\(e',e'',p,vl). --((bump (hl [EL 2 vl; EL 3 vl]) -
 777                    bump (hl [EL 0 vl; EL 1 vl])) /
 778                   &4))`);;
 779 e (MATCH_MP_TAC SUM_EQ);;
 780 e (EXPAND_TAC "K1" THEN REWRITE_TAC[IN;IN_ELIM_THM;BETA_THM]);;
 781 e (REPEAT STRIP_TAC);;
 782 e (ASM_REWRITE_TAC[BETA_THM]);;
 783 e (REAL_ARITH_TAC);;
 784
 785 e (REWRITE_WITH
 786 ` sum (K1:(real^3->bool)#(real^3->bool)#(num->num)#(real^3)list->bool)
 787  (\(e',e'',p,vl). --((bump (hl [EL 2 vl; EL 3 vl]) -
 788                    bump (hl [EL 0 vl; EL 1 vl])) /
 789                   &4)) =
 790 -- sum K1 (\(e',e'',p,vl). (bump (hl [EL 2 vl; EL 3 vl]) -
 791                    bump (hl [EL 0 vl; EL 1 vl])) /
 792                   &4)`);;
 793
 794
 795 (* need to continue  *)
 796
 797
 798
 799
 800
 801 e (MESON_TAC[SUM_NEG;john_harrison_lemma1]);;
 802 seans_fn();;
 803 SUM_NEG;;
 804 seans_fn();;
 805
 806
 807 e (ABBREV_TAC `S1 = {e',e'',p,vl | k = 4 /\
 808                      critical_edgeX V X = {e', e''} /\
 809                      e = e' /\
 810                      p permutes 0..3 /\
 811                      vl = left_action_list p ul /\
 812                      e' = {EL 0 vl, EL 1 (vl:(real^3)list)} /\
 813                      e'' = {EL 2 vl, EL 3 vl}}`);;
 814
 815
 816 search [`sum f (\x. s - t)`];;
 817
 818
 819 e CHEAT_TAC;;
 820 (* ! this may be difficult here *)
 821
 822 (* -------------------------------------------------------*)
 823
 824 e (MATCH_MP_TAC SUM_EQ_0);;
 825 e (GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[IN_ELIM_THM]);;
 826 e (NEW_GOAL `! e e'. (e = e') \/ ~(critical_edgeX V X = {e, e'})`);;
 827 e (ASM_MESON_TAC[]);;
 828 e (MATCH_MP_TAC SUM_EQ_0);;
 829 e (GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM]);;
 830 e (STRIP_TAC);;
 831 e (ASM_REWRITE_TAC[IN_ELIM_THM]);;
 832 e (MATCH_MP_TAC (REAL_ARITH `a = &0 ==> a / &4 = &0`));;
 833 e (MATCH_MP_TAC (REAL_ARITH `a = b ==> a - b = &0`));;
 834 e (AP_TERM_TAC);;
 835 e (REWRITE_TAC[HL]);;
 836 e (AP_TERM_TAC);;
 837 e (REWRITE_WITH `!a:real^3 b. set_of_list[a;b] = {a, b}`);;
 838 e (MESON_TAC[set_of_list]);;
 839 e (REWRITE_TAC[GSYM
 840   (ASSUME `vl:(real^3)list = left_action_list (p:num->num) ul`)]);;
 841 e (SUBGOAL_THEN `e':real^3->bool = e''`ASSUME_TAC);;
 842 e (ASM_MESON_TAC[]);;
 843 e (ASM_MESON_TAC[]);;
 844
 845 let SUM_BETA_BUMP_LEMMA = top_thm();;
 846
 847 end;;