text_formalization/local/AXJRPNC.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Local Fan                                              *)
   5 (* Author: Hoang Le Truong                                        *)
   6 (* Date: 2012-04-01                                                           *)
   7 (* ========================================================================= *)
   8
   9
  10 (*
  11 remaining conclusions from appendix to Local Fan chapter
  12 *)
  13
  14
  15 module Axjrpnc = struct
  16
  17
  18 open Polyhedron;;
  19 open Sphere;;
  20 open Topology;;
  21 open Fan_misc;;
  22 open Planarity;;
  23 open Conforming;;
  24 open Hypermap;;
  25 open Fan;;
  26 open Topology;;
  27 open Wrgcvdr_cizmrrh;;
  28 open Local_lemmas;;
  29 open Collect_geom;;
  30 open Dih2k_hypermap;;
  31 open Wjscpro;;
  32 open Tecoxbm;;
  33 open Hdplygy;;
  34 open Nkezbfc_local;;
  35 open Flyspeck_constants;;
  36 open Gbycpxs;;
  37 open Pcrttid;;
  38 open Local_lemmas1;;
  39 open Pack_defs;;
  40
  41 open Hales_tactic;;
  42
  43 open Appendix;;
  44
  45
  46
  47
  48
  49 open Hypermap;;
  50 open Fan;;
  51 open Wrgcvdr_cizmrrh;;
  52 open Local_lemmas;;
  53 open Flyspeck_constants;;
  54 open Pack_defs;;
  55
  56 open Hales_tactic;;
  57
  58 open Appendix;;
  59
  60
  61 open Zithlqn;;
  62
  63
  64 open Xwitccn;;
  65
  66 open Ayqjtmd;;
  67
  68 open Jkqewgv;;
  69
  70
  71 open Mtuwlun;;
  72
  73
  74 open Uxckfpe;;
  75 open Sgtrnaf;;
  76
  77 open Yxionxl;;
  78
  79 open Qknvmlb;;
  80 open Odxlstcv2;;
  81
  82 open Yxionxl2;;
  83 open Eyypqdw;;
  84 open Ocbicby;;
  85 open Imjxphr;;
  86
  87 open Nuxcoea;;
  88 open Fektyiy;;
  89
  90
  91
  92 let DIST_LE_2h0_IN_CASES_6=prove(`scs_k_v39 s=6 /\ BBs_v39 s v /\ is_scs_v39 s
  93 ==> !i. norm(v i- v (SUC i))<= &2 *h0`,
  94 STRIP_TAC
  95 THEN POP_ASSUM (fun th-> MP_TAC th
  96 THEN ASSUME_TAC th)
  97 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
  98 THEN RESA_TAC
  99 THEN GEN_TAC
 100 THEN DICH_TAC (0)
 101 THEN REWRITE_TAC[ARITH_RULE`a+b<=b <=> a= 0`]
 102 THEN SUBGOAL_THEN`FINITE
 103       {i | i < 6 /\
 104            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC
 105 THENL[
 106
 107 MATCH_MP_TAC FINITE_SUBSET
 108 THEN EXISTS_TAC`0..6`
 109 THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
 110 THEN ARITH_TAC;
 111
 112 MRESA_TAC CARD_EQ_0[`{i | i < 6 /\
 113         (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`]
 114 THEN REWRITE_TAC[SET_RULE`A={}<=> !x. ~(x IN A)`;IN_ELIM_THM]
 115 THEN MRESAL_TAC DIVISION[`i`;`6`][ARITH_RULE`~(6=0)`]
 116 THEN STRIP_TAC
 117 THEN THAYTHEL_TAC 0[`i MOD 6`][DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`]
 118 THEN DICH_TAC (27-1)
 119 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`]
 120 THEN STRIP_TAC
 121 THEN THAYTHEL_TAC 1[`i`;`SUC i`][dist]
 122 THEN POP_ASSUM MP_TAC
 123 THEN DICH_TAC(29-24)
 124 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i:num`;`SUC(i MOD 6)  MOD 6:num`;`s:scs_v39`;`i MOD 6:num`;`SUC(i MOD 6):num`][MOD_REFL;ARITH_RULE`~(6=0)`]
 125 THEN SYM_ASSUM_TAC
 126 THEN ASM_SIMP_TAC[Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)`]
 127 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i:num`;`SUC i MOD 6:num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`]
 128 THEN REAL_ARITH_TAC]);;
 129
 130
 131 let DIST_EDGE_IN_BB_LE_2=prove(`BBs_v39 s v /\ is_scs_v39 s
 132 ==> &2<= norm(v i- v (SUC i))`,
 133 DISCH_TAC
 134 THEN POP_ASSUM(fun th-> MP_TAC th
 135 THEN ASSUME_TAC th)
 136 THEN REWRITE_TAC[BBs_v39;is_scs_v39;LET_DEF;LET_END_DEF;]
 137 THEN STRIP_TAC
 138 THEN ABBREV_TAC`k= scs_k_v39 s`
 139 THEN THAYTHE_TAC (24-2)[`i`;`SUC i`]
 140 THEN THAYTHE_TAC (25-17)[`i MOD k`;`SUC i MOD k`]
 141 THEN POP_ASSUM MP_TAC
 142 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`)
 143 THEN RESA_TAC
 144 THEN ASM_SIMP_TAC[DIVISION;Qknvmlb.SUC_MOD_NOT_EQ]
 145 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k:num`;`SUC i MOD k `;`s:scs_v39`;`i:num`;`SUC i:num`][is_scs_v39;MOD_REFL;ARITH_RULE`~(6=0)`]
 146 THEN DICH_TAC 4
 147 THEN REWRITE_TAC[dist]
 148 THEN REAL_ARITH_TAC);;
 149
 150
 151
 152 let arclength222h0 = prove_by_refinement(
 153   `arclength (&2) (&2) (&2 * h0) < pi / &2`,
 154   (* {{{ proof *)
 155   [
 156   GMATCH_SIMP_TAC Compute_2158872499.ATN_UPS_X_BREAKDOWN1;
 157   CONJ_TAC;
 158     GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
 159     REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
 160     BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
 161   REWRITE_TAC[arith `x + y < x <=> y < &0`];
 162   ONCE_REWRITE_TAC[GSYM ATN_0];
 163   MATCH_MP_TAC ATN_MONO_LT;
 164   REWRITE_TAC[arith `(x / y < &0 <=> &0 < (-- x)/ y)`];
 165   GMATCH_SIMP_TAC REAL_LT_DIV;
 166   GMATCH_SIMP_TAC SQRT_POS_LT;
 167   REWRITE_TAC[Sphere.h0];
 168   BY(REAL_ARITH_TAC)
 169   ]);;
 170   (* }}} *)
 171
 172
 173
 174
 175 let is_scs_k_le_3=prove(`is_scs_v39 s ==> 3<= scs_k_v39 s`,
 176 REWRITE_TAC[BBs_v39;is_scs_v39;LET_DEF;LET_END_DEF;]
 177 THEN RESA_TAC);;
 178
 179
 180 let DIST_LE2_BB_CASSE_4= prove_by_refinement(`scs_k_v39 s=4 /\ BBs_v39 s v /\ is_scs_v39 s
 181 ==> ?i. norm(v i- v (SUC i))<= &2 *h0`,
 182 [
 183 STRIP_TAC
 184 THEN POP_ASSUM (fun th-> MP_TAC th
 185 THEN ASSUME_TAC th)
 186 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
 187 THEN RESA_TAC
 188 THEN DICH_TAC (0)
 189 THEN REWRITE_TAC[ARITH_RULE`a+b<=b <=> a= 0`]
 190 THEN SUBGOAL_THEN`FINITE
 191       {i | i < 6 /\
 192            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC;
 193
 194 MATCH_MP_TAC FINITE_SUBSET
 195 THEN EXISTS_TAC`0..6`
 196 THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
 197 THEN ARITH_TAC;
 198
 199
 200 REWRITE_TAC[ARITH_RULE`a+4<=6 <=> a<= 2`]
 201 THEN SUBGOAL_THEN`{i | i < 4 /\
 202       (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}SUBSET 0..3` ASSUME_TAC;
 203
 204 ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
 205 THEN ARITH_TAC;
 206
 207 STRIP_TAC
 208 THEN MRESAL_TAC CARD_DIFF[`0..3`;`{i | i < 4 /\
 209       (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`][FINITE_NUMSEG;CARD_NUMSEG;]
 210 THEN MP_TAC(ARITH_RULE`CARD
 211       {i | i < 4 /\
 212            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))} <=
 213       2 /\ CARD
 214       ((0..3) DIFF
 215        {i | i < 4 /\
 216             (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}) =
 217       (3 + 1) -
 218       0 -
 219       CARD
 220       {i | i < 4 /\
 221            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}
 222 ==> 0 <CARD
 223       ((0..3) DIFF
 224        {i | i < 4 /\
 225             (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))})`)
 226 THEN RESA_TAC
 227 THEN POP_ASSUM MP_TAC
 228 THEN SYM_ASSUM_TAC
 229 THEN MP_TAC(SET_RULE`(0..3) DIFF
 230   {i | i < 4 /\
 231        (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}= {}
 232 \/ ~((0..3) DIFF
 233   {i | i < 4 /\
 234        (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))} ={})`)
 235 THEN RESA_TAC;
 236
 237 REWRITE_TAC[Oxl_2012.CARD_EMPTY]
 238 THEN ARITH_TAC;
 239
 240 POP_ASSUM MP_TAC
 241 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;DIFF;IN_ELIM_THM;IN_ELIM_THM;IN_NUMSEG]
 242 THEN RESA_TAC
 243 THEN POP_ASSUM MP_TAC
 244 THEN MP_TAC(ARITH_RULE`a<=3==> a<4`)
 245 THEN RESA_TAC
 246 THEN REWRITE_TAC[DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`]
 247 THEN REPEAT RESA_TAC
 248 THEN DICH_TAC (30-1)
 249 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`]
 250 THEN STRIP_TAC
 251 THEN THAYTHEL_TAC 1[`a`;`SUC a`][dist]
 252 THEN EXISTS_TAC`a:num`
 253 THEN POP_ASSUM MP_TAC
 254 THEN DICH_TAC (33-27)
 255 THEN REAL_ARITH_TAC]);;
 256
 257
 258
 259 let NORM_V_IN_BB_LE_CSTAB=prove(`  (!i. scs_b_v39 s i (SUC i) <= cstab) /\
 260   BBs_v39 s v
 261 ==> !i. norm (v i- v (SUC i))<= cstab`,
 262 REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;dist]
 263 THEN RESA_TAC
 264 THEN GEN_TAC
 265 THEN THAYTHE_TAC 1[`i`;`SUC i`]
 266 THEN THAYTHE_TAC 5[`i`]
 267 THEN ASM_TAC
 268 THEN REAL_ARITH_TAC);;
 269
 270
 271
 272 let arclength_2h0_cstab = prove_by_refinement(
 273   `arclength (&2) (&2) (&2 *h0) + arclength (&2) (&2) cstab < pi`,
 274   (* {{{ proof *)
 275   [
 276   REPEAT (GMATCH_SIMP_TAC Compute_2158872499.ATN_UPS_X_BREAKDOWN1);
 277   REWRITE_TAC[GSYM CONJ_ASSOC];
 278   CONJ_TAC;
 279     BY(REWRITE_TAC[Sphere.h0;Sphere.cstab] THEN REAL_ARITH_TAC);
 280   CONJ_TAC;
 281     BY(REWRITE_TAC[Sphere.h0;Sphere.cstab] THEN REAL_ARITH_TAC);
 282   REWRITE_TAC[arith `(pi/ &2 + b) + (pi / &2 + d) < pi <=> b + d < &0`];
 283   REWRITE_TAC[Sphere.h0;Sphere.cstab];
 284   MP_TAC (Flyspeck_constants.calc `atn (((&2 *  #1.26) * &2 *  #1.26 -
 285 &2 * &2 - &2 * &2) /  sqrt  ((&2 + &2 + &2 *  #1.26) *   (&2 + &2 - &2
 286 *  #1.26) *   (&2 + &2 *  #1.26 - &2) *   (&2 *  #1.26 + &2 - &2))) +
 287 atn (( #3.01 *  #3.01 - &2 * &2 - &2 * &2) /  sqrt  ((&2 + &2 +
 288 #3.01) *   (&2 + &2 -  #3.01) *   (&2 +  #3.01 - &2) *   ( #3.01 + &2
 289 -  &2))) < &0`);
 290   BY(REWRITE_TAC[])
 291   ]);;
 292   (* }}} *)
 293
 294
 295
 296
 297
 298 let DIST_LE2_BB_CASSE_5 = prove_by_refinement(
 299 `scs_k_v39 s=5 /\ BBs_v39 s v /\ is_scs_v39 s
 300 ==> norm(v i- v (SUC i))<= &2 *h0 \/ norm(v (SUC i)- v (SUC (SUC i)))<= &2 *h0 `,
 301 [
 302 STRIP_TAC
 303 THEN POP_ASSUM (fun th-> MP_TAC th
 304 THEN ASSUME_TAC th)
 305 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
 306 THEN RESA_TAC
 307 THEN DICH_TAC (0)
 308 THEN REWRITE_TAC[ARITH_RULE`a+b<=b <=> a= 0`]
 309 THEN SUBGOAL_THEN`FINITE
 310       {i | i < 5 /\
 311            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC;
 312
 313 MATCH_MP_TAC FINITE_SUBSET
 314 THEN EXISTS_TAC`0..5`
 315 THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
 316 THEN ARITH_TAC;
 317
 318 REWRITE_TAC[ARITH_RULE`a+5<=6 <=> a<= 1`]
 319 THEN STRIP_TAC
 320 THEN MP_TAC(SET_RULE`norm (v i - v (SUC i)) <= &2 * h0 \/
 321      norm (v (SUC i) - (v:num->real^3) (SUC (SUC i))) <= &2 * h0 \/ ~(norm (v i - v (SUC i)) <= &2 * h0 \/
 322      norm (v (SUC i) - v (SUC (SUC i))) <= &2 * h0)`)
 323 THEN RESA_TAC;
 324
 325 DICH_TAC 1
 326 THEN POP_ASSUM MP_TAC
 327 THEN REWRITE_TAC[DE_MORGAN_THM;REAL_ARITH`~(a<=b) <=> b<a`]
 328 THEN STRIP_TAC
 329 THEN DICH_TAC (24-1)
 330 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(5<=3)`]
 331 THEN STRIP_TAC
 332 THEN DICH_TAC 1
 333 THEN STRIP_TAC
 334 THEN POP_ASSUM (fun th-> MRESAL_TAC th[`i`;`SUC i`][dist] THEN MRESAL_TAC th[`SUC i`;`SUC (SUC i)`][dist])
 335 THEN MP_TAC(REAL_ARITH`&2 * h0 < norm (v i - v (SUC i)) /\  norm (v i - v (SUC i))<= scs_b_v39 s i (SUC i) /\  &2 * h0 < norm (v (SUC i) - v (SUC (SUC i))) /\  norm ((v:num->real^3) (SUC i) - v (SUC (SUC i)))<= scs_b_v39 s (SUC i) (SUC (SUC i))
 336 ==> &2 * h0< scs_b_v39 s (SUC i) (SUC (SUC i)) /\ &2 * h0< scs_b_v39 s (i) (SUC (i))`)
 337 THEN RESA_TAC
 338 THEN SUBGOAL_THEN`{i MOD 5,SUC i MOD 5} SUBSET {i | i < 5 /\
 339         (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC;
 340
 341 REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {c,b}<=> a= c\/ a= b`]
 342 THEN REPEAT RESA_TAC;
 343
 344 ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`];
 345
 346 MRESAL_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i MOD 5:num`;`SUC (i MOD 5) `;`s:scs_v39`;`i:num`;`SUC (i MOD 5) MOD 5:num`][is_scs_v39]
 347 THEN POP_ASSUM MP_TAC
 348 THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`]
 349 THEN RESA_TAC
 350 THEN ASM_SIMP_TAC[Hypermap.lemma_suc_mod;ARITH_RULE`~(5=0)`]
 351 THEN MRESAL_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i:num`;`SUC i MOD 5 `;`s:scs_v39`;`i:num`;`SUC i:num`][is_scs_v39]
 352 THEN POP_ASSUM MP_TAC
 353 THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`]
 354 THEN RESA_TAC;
 355
 356 ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`];
 357
 358 MRESAL_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`(SUC i) MOD 5:num`;`SUC ((SUC i) MOD 5) `;`s:scs_v39`;`(SUC i):num`;`SUC ((SUC i) MOD 5) MOD 5:num`][is_scs_v39]
 359 THEN POP_ASSUM MP_TAC
 360 THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`]
 361 THEN RESA_TAC
 362 THEN ASM_SIMP_TAC[Hypermap.lemma_suc_mod;ARITH_RULE`~(5=0)`]
 363 THEN MRESAL_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`(SUC i):num`;`SUC (SUC i) MOD 5 `;`s:scs_v39`;`(SUC i):num`;`SUC (SUC i):num`][is_scs_v39]
 364 THEN POP_ASSUM MP_TAC
 365 THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`]
 366 THEN RESA_TAC;
 367
 368 MRESA_TAC Hypermap.CARD_TWO_ELEMENTS[`i MOD 5`;`SUC i MOD 5`]
 369 THEN POP_ASSUM MP_TAC
 370 THEN ASM_SIMP_TAC[Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`]
 371 THEN STRIP_TAC
 372 THEN MRESA_TAC CARD_SUBSET[`{i MOD 5, SUC i MOD 5}`;`
 373       {i | i < 5 /\
 374            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`]
 375 THEN POP_ASSUM MP_TAC
 376 THEN ARITH_TAC]);;
 377
 378
 379
 380 let AXJRPNC_concl = `!s (v:num->real^3) i j.
 381   is_scs_v39 s /\ scs_basic_v39 s /\
 382   (!i. scs_b_v39 s i (SUC i) <= cstab) /\
 383   MMs_v39 s v /\
 384   (lunar (v i,v j) (IMAGE v (:num))
 385      (IMAGE (\i. {v i, v (SUC i)}) (:num))   ) ==>
 386   (scs_k_v39 s = 6 /\ v j = v (i + 3))`;;
 387
 388
 389
 390 let  AXJRPNC = prove_by_refinement(
 391  AXJRPNC_concl,
 392 [
 393 REPEAT GEN_TAC
 394 THEN ABBREV_TAC`k=scs_k_v39 s`
 395 THEN ABBREV_TAC`V=(IMAGE (v:num->real^3) (:num))`
 396 THEN ABBREV_TAC`E=(IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num))`
 397 THEN ABBREV_TAC`FF=IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
 398 THEN STRIP_TAC
 399 THEN MP_TAC Qknvmlb.SCS_K_LE_6
 400 THEN RESA_TAC
 401 THEN MP_TAC(ARITH_RULE`k<=6==> k=6\/ k<6`)
 402 THEN RESA_TAC;
 403
 404
 405 MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 406 THEN MP_TAC DIST_LE_2h0_IN_CASES_6
 407 THEN RESA_TAC;
 408
 409
 410 MRESAL_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k`;`s`;`v`][ARITH_RULE`3<6`]
 411 THEN ASSUME_TAC(ARITH_RULE`3<6/\ ~(6<=3)`)
 412 THEN MRESA_TAC(GEN_ALL CARD_V_EQ_SCS_K1)[`s:scs_v39`;`v:num->real^3`;`IMAGE (v:num->real^3) (:num)`;`k:num`]
 413 THEN MRESA_TAC Local_lemmas.NEXT_OPOSITE_POINT_IS_NOT_IN_AFF_GT2[`E`;`v j`;`V`;`FF`;`v i`]
 414 THEN DICH_TAC(20-16)
 415 THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v i`;`v`;`i`]
 416 THEN MP_TAC(ARITH_RULE`i'+1<6/\ ~(i'=0)/\ ~(i'=1)==> i'=2\/ i'=4\/ i'=3`)
 417 THEN RESA_TAC;
 418
 419
 420 STRIP_TAC
 421 THEN POP_ASSUM(fun th-> ASM_TAC
 422 THEN MP_TAC th
 423 THEN REPEAT RESA_TAC)
 424 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`]
 425 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`]
 426 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`]
 427 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`]
 428 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`]
 429 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`&2* h0`][dist;]
 430 THEN POP_ASSUM MP_TAC
 431 THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
 432 THEN REWRITE_TAC[GSYM h0]
 433 THEN STRIP_TAC
 434 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`&2* h0`][dist;]
 435 THEN POP_ASSUM MP_TAC
 436 THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
 437 THEN REWRITE_TAC[GSYM h0]
 438 THEN STRIP_TAC
 439 THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v i) (v (SUC i)) <= arclength (&2) (&2) (&2 * h0)
 440 /\ arcV (vec 0) ((v:num->real^3) (SUC i)) (v (SUC (SUC i))) <=
 441       arclength (&2) (&2) (&2 * h0)
 442 /\ arclength (&2) (&2) (&2 * h0)< pi/ &2
 443 ==>arcV (vec 0) (v (i)) (v ((SUC i)))+ arcV (vec 0) (v (SUC i)) (v (SUC (SUC i)))
 444  < pi`)
 445 THEN ASM_SIMP_TAC[arclength222h0]
 446 THEN STRIP_TAC
 447 THEN MP_TAC Local_lemmas.CVLF_LF_F
 448 THEN RESA_TAC
 449 THEN MRESA_TAC WL_IN_FF[`i`;`v`]
 450 THEN MRESA_TAC WL_IN_FF[`SUC i`;`v`]
 451 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v i, v (SUC i)`]
 452 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC i), v (SUC (SUC i))`]
 453 THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v i`;`v (SUC(SUC i))`;`v (SUC i)`]
 454 THEN POP_ASSUM MP_TAC
 455 THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 456 THEN RESA_TAC
 457 THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(2+i)`]
 458 THEN REMOVE_ASSUM_TAC
 459 THEN POP_ASSUM MP_TAC
 460 THEN REWRITE_TAC[ARITH_RULE`2+i= SUC(SUC i)`;]
 461 THEN STRIP_TAC
 462 THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (SUC (SUC i))}`];
 463
 464
 465
 466
 467 STRIP_TAC
 468 THEN POP_ASSUM(fun th-> ASM_TAC
 469 THEN MP_TAC th
 470 THEN REPEAT RESA_TAC)
 471 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`4+i`]
 472 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (4+i)`]
 473 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (4+i))`]
 474 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(4+i)`]
 475 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (4+i)`]
 476 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (4+i)`;`v (SUC (4+i))`;`&2* h0`][dist;]
 477 THEN POP_ASSUM MP_TAC
 478 THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
 479 THEN REWRITE_TAC[GSYM h0]
 480 THEN STRIP_TAC
 481 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (4+i))`;`v (SUC(SUC (4+i)))`;`&2* h0`][dist;]
 482 THEN POP_ASSUM MP_TAC
 483 THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
 484 THEN REWRITE_TAC[GSYM h0]
 485 THEN STRIP_TAC
 486 THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (4+i)) (v (SUC (4+i))) <= arclength (&2) (&2) (&2 * h0)
 487 /\ arcV (vec 0) ((v:num->real^3) (SUC (4+i))) (v (SUC (SUC (4+i)))) <=
 488       arclength (&2) (&2) (&2 * h0)
 489 /\ arclength (&2) (&2) (&2 * h0)< pi/ &2
 490 ==>arcV (vec 0) (v ((4+i))) (v ((SUC (4+i))))+ arcV (vec 0) (v (SUC (4+i))) (v (SUC (SUC (4+i))))
 491  < pi`)
 492 THEN ASM_SIMP_TAC[arclength222h0]
 493 THEN STRIP_TAC
 494 THEN MP_TAC Local_lemmas.CVLF_LF_F
 495 THEN RESA_TAC
 496 THEN MRESA_TAC WL_IN_FF[`(4+i)`;`v`]
 497 THEN MRESA_TAC WL_IN_FF[`SUC (4+i)`;`v`]
 498 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (4+i), v (SUC (4+i))`]
 499 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (4+i)), v (SUC (SUC (4+i)))`]
 500 THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (4+i)`;`v (SUC(SUC (4+i)))`;`v (SUC (4+i))`]
 501 THEN POP_ASSUM MP_TAC
 502 THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 503 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(4+i))= 1*6+i`]
 504 THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(1*6+i):num`;`v:num->real^3`;`(1*6+i) MOD k`]
 505 THEN POP_ASSUM MP_TAC
 506 THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(6=0)`]
 507 THEN RESA_TAC
 508 THEN MRESA_TAC MOD_MULT_ADD[`1`;`6`;`i`]
 509 THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i MOD k):num`;`v:num->real^3`;`i`]
 510 THEN POP_ASSUM MP_TAC
 511 THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(6=0)`]
 512 THEN RESA_TAC
 513 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 514 THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(4+i)`]
 515 THEN REMOVE_ASSUM_TAC
 516 THEN POP_ASSUM MP_TAC
 517 THEN REWRITE_TAC[ARITH_RULE`2+i= SUC(SUC i)`;]
 518 THEN STRIP_TAC
 519 THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (4+i)}`]
 520 ;
 521
 522 ONCE_REWRITE_TAC[ARITH_RULE`3+i=i+3`]
 523 THEN REWRITE_TAC[];
 524
 525
 526
 527 MP_TAC is_scs_k_le_3
 528 THEN RESA_TAC
 529 THEN MP_TAC(ARITH_RULE`3<=k/\ k<6==> k=3\/ (3<k/\ k=4)\/ (3<k/\ k=5)`)
 530 THEN RESA_TAC;
 531
 532
 533
 534 MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 535 THEN MRESAL_TAC Jkqewgv.IS_SCS_NOT_COLLINEAR_BBs_CASE_3[`s`;`v`][IN]
 536 THEN DICH_TAC 8
 537 THEN REWRITE_TAC[lunar]
 538 THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`i:num`;`v:num->real^3`;`i MOD k`]
 539 THEN POP_ASSUM MP_TAC
 540 THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(3=0)`]
 541 THEN RESA_TAC
 542 THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`j:num`;`v:num->real^3`;`j MOD k`]
 543 THEN POP_ASSUM MP_TAC
 544 THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(3=0)`]
 545 THEN RESA_TAC
 546 THEN MP_TAC(ARITH_RULE`i MOD 3< 3==> i MOD 3= 0\/ i MOD 3= 1\/ i MOD 3=2`)
 547 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(3=0)`]
 548 THEN RESA_TAC
 549 THEN MP_TAC(ARITH_RULE`j MOD 3< 3==> j MOD 3= 0\/ j MOD 3= 1\/ j MOD 3=2`)
 550 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(3=0)`]
 551 THEN RESA_TAC
 552 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C} ={A,C,B}`]
 553 THEN ASM_REWRITE_TAC[]
 554 ;
 555
 556
 557
 558
 559
 560 MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 561 THEN MRESAL_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k`;`s`;`v`][ARITH_RULE`3<6`]
 562 THEN ASSUME_TAC(ARITH_RULE`3<4/\ ~(4<=3)`)
 563 THEN MRESA_TAC(GEN_ALL CARD_V_EQ_SCS_K1)[`s:scs_v39`;`v:num->real^3`;`IMAGE (v:num->real^3) (:num)`;`k:num`]
 564 THEN MRESA_TAC Local_lemmas.NEXT_OPOSITE_POINT_IS_NOT_IN_AFF_GT2[`E`;`v j`;`V`;`FF`;`v i`]
 565 THEN DICH_TAC(22-18)
 566 THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v i`;`v`;`i`]
 567 THEN MP_TAC(ARITH_RULE`i'+1<4/\ ~(i'=0)/\ ~(i'=1)==> i'=2`)
 568 THEN RESA_TAC;
 569
 570
 571
 572
 573 MP_TAC DIST_LE2_BB_CASSE_4
 574 THEN RESA_TAC
 575 THEN POP_ASSUM MP_TAC
 576 THEN MP_TAC Local_lemmas.CVLF_LF_F
 577 THEN RESA_TAC
 578 THEN MRESA_TAC WL_IN_V[`i`;`v`]
 579 THEN MRESA_TAC Localization.LOFA_IMP_LT_CARD_SET_V_ALT[`V`;`E`;`FF`;`v i`]
 580 THEN MRESA_TAC WL_IN_V[`i''`;`v`]
 581 THEN POP_ASSUM MP_TAC
 582 THEN SYM_ASSUM_TAC
 583 THEN REWRITE_TAC[IN_ELIM_THM]
 584 THEN RESA_TAC
 585 THEN MRESA_TAC Nuxcoea.W_IN_BB_FUN_EQ[`v:num->real^3`;`i'':num`;`n+i:num`;`s`]
 586 THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i''`;`n+i:num`;`k`][ARITH_RULE`~(4=0)`]
 587 THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`SUC i'':num`;`v:num->real^3`;`SUC (n+i)`]
 588 THEN MP_TAC(ARITH_RULE`n<4==> n=0\/ n=1\/ n=2\/ n=3`)
 589 THEN RESA_TAC;
 590
 591
 592
 593
 594
 595 REWRITE_TAC[ARITH_RULE`0+a=a`]
 596 THEN STRIP_TAC
 597 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`]
 598 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`]
 599 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`]
 600 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`]
 601 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`]
 602 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`&2* h0`][dist;]
 603 THEN POP_ASSUM MP_TAC
 604 THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
 605 THEN REWRITE_TAC[GSYM h0]
 606 THEN STRIP_TAC
 607 THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
 608 THEN RESA_TAC
 609 THEN THAYTHE_TAC 0[`SUC i`]
 610 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`cstab`][dist;]
 611 THEN POP_ASSUM MP_TAC
 612 THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
 613 THEN REWRITE_TAC[GSYM cstab]
 614 THEN STRIP_TAC
 615 THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (i)) (v (SUC (i))) <= arclength (&2) (&2) (&2 * h0)
 616 /\ arcV (vec 0) ((v:num->real^3) (SUC (i))) (v (SUC (SUC (i)))) <=
 617       arclength (&2) (&2) (cstab)
 618 /\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
 619 ==>arcV (vec 0) (v ((i))) (v ((SUC (i))))+ arcV (vec 0) (v (SUC (i))) (v (SUC (SUC (i))))
 620  < pi`)
 621 THEN ASM_SIMP_TAC[arclength_2h0_cstab]
 622 THEN STRIP_TAC
 623 THEN MRESA_TAC WL_IN_FF[`(i)`;`v`]
 624 THEN MRESA_TAC WL_IN_FF[`SUC (i)`;`v`]
 625 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (i), v (SUC (i))`]
 626 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (i)), v (SUC (SUC (i)))`]
 627 THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (i)`;`v (SUC(SUC (i)))`;`v (SUC (i))`]
 628 THEN POP_ASSUM MP_TAC
 629 THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 630 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`]
 631 THEN STRIP_TAC
 632 THEN STRIP_TAC
 633 THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`]
 634 THEN REMOVE_ASSUM_TAC
 635 THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`]
 636 ;
 637
 638
 639
 640
 641
 642 REWRITE_TAC[ARITH_RULE`1+a=SUC a`]
 643 THEN STRIP_TAC
 644 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`]
 645 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`]
 646 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`]
 647 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`]
 648 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`]
 649 THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
 650 THEN RESA_TAC
 651 THEN THAYTHE_TAC 0[`i`]
 652 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`cstab`][dist;]
 653 THEN POP_ASSUM MP_TAC
 654 THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
 655 THEN REWRITE_TAC[GSYM cstab]
 656 THEN STRIP_TAC
 657 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`&2* h0`][dist;]
 658 THEN POP_ASSUM MP_TAC
 659 THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
 660 THEN REWRITE_TAC[GSYM h0]
 661 THEN STRIP_TAC
 662 THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (i)) (v (SUC (i))) <= arclength (&2) (&2) (cstab)
 663 /\ arcV (vec 0) ((v:num->real^3) (SUC (i))) (v (SUC (SUC (i)))) <=
 664        arclength (&2) (&2) (&2 * h0)
 665 /\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
 666 ==>arcV (vec 0) (v ((i))) (v ((SUC (i))))+ arcV (vec 0) (v (SUC (i))) (v (SUC (SUC (i))))
 667  < pi`)
 668 THEN ASM_SIMP_TAC[arclength_2h0_cstab]
 669 THEN STRIP_TAC
 670 THEN MRESA_TAC WL_IN_FF[`(i)`;`v`]
 671 THEN MRESA_TAC WL_IN_FF[`SUC (i)`;`v`]
 672 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (i), v (SUC (i))`]
 673 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (i)), v (SUC (SUC (i)))`]
 674 THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (i)`;`v (SUC(SUC (i)))`;`v (SUC (i))`]
 675 THEN POP_ASSUM MP_TAC
 676 THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 677 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`]
 678 THEN STRIP_TAC
 679 THEN STRIP_TAC
 680 THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`]
 681 THEN REMOVE_ASSUM_TAC
 682 THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`]
 683 ;
 684
 685
 686
 687 REWRITE_TAC[ARITH_RULE`0+a=a`]
 688 THEN STRIP_TAC
 689 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`(2+i)`]
 690 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (2+i)`]
 691 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (2+i))`]
 692 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(2+i)`]
 693 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (2+i)`]
 694 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (2+i)`;`v (SUC (2+i))`;`&2* h0`][dist;]
 695 THEN POP_ASSUM MP_TAC
 696 THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
 697 THEN REWRITE_TAC[GSYM h0]
 698 THEN STRIP_TAC
 699 THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
 700 THEN RESA_TAC
 701 THEN THAYTHE_TAC 0[`SUC (2+i)`]
 702 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (2+i))`;`v (SUC(SUC (2+i)))`;`cstab`][dist;]
 703 THEN POP_ASSUM MP_TAC
 704 THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
 705 THEN REWRITE_TAC[GSYM cstab]
 706 THEN STRIP_TAC
 707 THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (2+i)) (v (SUC (2+i))) <= arclength (&2) (&2) (&2 * h0)
 708 /\ arcV (vec 0) ((v:num->real^3) (SUC (2+i))) (v (SUC (SUC (2+i)))) <=
 709       arclength (&2) (&2) (cstab)
 710 /\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
 711 ==>arcV (vec 0) (v ((2+i))) (v ((SUC (2+i))))+ arcV (vec 0) (v (SUC (2+i))) (v (SUC (SUC (2+i))))
 712  < pi`)
 713 THEN ASM_SIMP_TAC[arclength_2h0_cstab]
 714 THEN STRIP_TAC
 715 THEN MRESA_TAC WL_IN_FF[`(2+i)`;`v`]
 716 THEN MRESA_TAC WL_IN_FF[`SUC (2+i)`;`v`]
 717 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (2+i), v (SUC (2+i))`]
 718 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (2+i)), v (SUC (SUC (2+i)))`]
 719 THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (2+i)`;`v (SUC(SUC (2+i)))`;`v (SUC (2+i))`]
 720 THEN POP_ASSUM MP_TAC
 721 THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 722 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`]
 723 THEN STRIP_TAC
 724 THEN STRIP_TAC
 725 THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`]
 726 THEN REMOVE_ASSUM_TAC
 727 THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`]
 728 THEN DICH_TAC 3
 729 THEN ASM_REWRITE_TAC[ARITH_RULE`2+2+i= 1*4+i`]
 730 THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(1*4+i):num`;`v:num->real^3`;`(1*4+i) MOD k`]
 731 THEN POP_ASSUM MP_TAC
 732 THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(4=0)`]
 733 THEN RESA_TAC
 734 THEN MRESA_TAC MOD_MULT_ADD[`1`;`4`;`i`]
 735 THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i MOD k):num`;`v:num->real^3`;`i`]
 736 THEN POP_ASSUM MP_TAC
 737 THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(4=0)`]
 738 THEN RESA_TAC
 739 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 740 THEN RESA_TAC;
 741
 742
 743
 744
 745 REWRITE_TAC[ARITH_RULE`3+i=SUC(2+i)`]
 746 THEN STRIP_TAC
 747 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`(2+i)`]
 748 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (2+i)`]
 749 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (2+i))`]
 750 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(2+i)`]
 751 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (2+i)`]
 752 THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
 753 THEN RESA_TAC
 754 THEN THAYTHE_TAC 0[`(2+i)`]
 755 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (2+i)`;`v (SUC (2+i))`;`cstab`][dist;]
 756 THEN POP_ASSUM MP_TAC
 757 THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
 758 THEN REWRITE_TAC[GSYM cstab]
 759 THEN STRIP_TAC
 760 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (2+i))`;`v (SUC(SUC (2+i)))`;`&2* h0`][dist;]
 761 THEN POP_ASSUM MP_TAC
 762 THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
 763 THEN REWRITE_TAC[GSYM h0]
 764 THEN STRIP_TAC
 765 THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (2+i)) (v (SUC (2+i))) <= arclength (&2) (&2) (cstab)
 766 /\ arcV (vec 0) ((v:num->real^3) (SUC (2+i))) (v (SUC (SUC (2+i)))) <=
 767       arclength (&2) (&2) (&2 * h0)
 768 /\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
 769 ==>arcV (vec 0) (v ((2+i))) (v ((SUC (2+i))))+ arcV (vec 0) (v (SUC (2+i))) (v (SUC (SUC (2+i))))
 770  < pi`)
 771 THEN ASM_SIMP_TAC[arclength_2h0_cstab]
 772 THEN STRIP_TAC
 773 THEN MRESA_TAC WL_IN_FF[`(2+i)`;`v`]
 774 THEN MRESA_TAC WL_IN_FF[`SUC (2+i)`;`v`]
 775 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (2+i), v (SUC (2+i))`]
 776 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (2+i)), v (SUC (SUC (2+i)))`]
 777 THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (2+i)`;`v (SUC(SUC (2+i)))`;`v (SUC (2+i))`]
 778 THEN POP_ASSUM MP_TAC
 779 THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 780 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`]
 781 THEN STRIP_TAC
 782 THEN STRIP_TAC
 783 THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`]
 784 THEN REMOVE_ASSUM_TAC
 785 THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`]
 786 THEN DICH_TAC 3
 787 THEN ASM_REWRITE_TAC[ARITH_RULE`2+2+i= 1*4+i`]
 788 THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(1*4+i):num`;`v:num->real^3`;`(1*4+i) MOD k`]
 789 THEN POP_ASSUM MP_TAC
 790 THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(4=0)`]
 791 THEN RESA_TAC
 792 THEN MRESA_TAC MOD_MULT_ADD[`1`;`4`;`i`]
 793 THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i MOD k):num`;`v:num->real^3`;`i`]
 794 THEN POP_ASSUM MP_TAC
 795 THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(4=0)`]
 796 THEN RESA_TAC
 797 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 798 THEN RESA_TAC;
 799
 800
 801
 802
 803
 804
 805 MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 806 THEN MRESAL_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k`;`s`;`v`][ARITH_RULE`3<5`]
 807 THEN ASSUME_TAC(ARITH_RULE`3<5/\ ~(5<=3)`)
 808 THEN MRESA_TAC(GEN_ALL CARD_V_EQ_SCS_K1)[`s:scs_v39`;`v:num->real^3`;`IMAGE (v:num->real^3) (:num)`;`k:num`]
 809 THEN MRESA_TAC Local_lemmas.NEXT_OPOSITE_POINT_IS_NOT_IN_AFF_GT2[`E`;`v j`;`V`;`FF`;`v i`]
 810 THEN DICH_TAC(22-18)
 811 THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v i`;`v`;`i`]
 812 THEN MP_TAC(ARITH_RULE`i'+1<5/\ ~(i'=0)/\ ~(i'=1)==> i'=2\/ i'=3`)
 813 THEN RESA_TAC;
 814
 815
 816
 817
 818 MP_TAC DIST_LE2_BB_CASSE_5
 819 THEN RESA_TAC
 820 THEN MP_TAC Local_lemmas.CVLF_LF_F
 821 THEN RESA_TAC
 822 ;
 823
 824
 825
 826
 827
 828
 829 REWRITE_TAC[ARITH_RULE`0+a=a`]
 830 THEN STRIP_TAC
 831 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`]
 832 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`]
 833 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`]
 834 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`]
 835 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`]
 836 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`&2* h0`][dist;]
 837 THEN POP_ASSUM MP_TAC
 838 THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
 839 THEN REWRITE_TAC[GSYM h0]
 840 THEN STRIP_TAC
 841 THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
 842 THEN RESA_TAC
 843 THEN THAYTHE_TAC 0[`SUC i`]
 844 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`cstab`][dist;]
 845 THEN POP_ASSUM MP_TAC
 846 THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
 847 THEN REWRITE_TAC[GSYM cstab]
 848 THEN STRIP_TAC
 849 THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (i)) (v (SUC (i))) <= arclength (&2) (&2) (&2 * h0)
 850 /\ arcV (vec 0) ((v:num->real^3) (SUC (i))) (v (SUC (SUC (i)))) <=
 851       arclength (&2) (&2) (cstab)
 852 /\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
 853 ==>arcV (vec 0) (v ((i))) (v ((SUC (i))))+ arcV (vec 0) (v (SUC (i))) (v (SUC (SUC (i))))
 854  < pi`)
 855 THEN ASM_SIMP_TAC[arclength_2h0_cstab]
 856 THEN STRIP_TAC
 857 THEN MRESA_TAC WL_IN_FF[`(i)`;`v`]
 858 THEN MRESA_TAC WL_IN_FF[`SUC (i)`;`v`]
 859 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (i), v (SUC (i))`]
 860 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (i)), v (SUC (SUC (i)))`]
 861 THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (i)`;`v (SUC(SUC (i)))`;`v (SUC (i))`]
 862 THEN POP_ASSUM MP_TAC
 863 THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 864 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`]
 865 THEN STRIP_TAC
 866 THEN STRIP_TAC
 867 THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`]
 868 THEN REMOVE_ASSUM_TAC
 869 THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`]
 870 ;
 871
 872
 873
 874
 875
 876
 877 REWRITE_TAC[ARITH_RULE`1+a=SUC a`]
 878 THEN STRIP_TAC
 879 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`]
 880 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`]
 881 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`]
 882 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`]
 883 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`]
 884 THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
 885 THEN RESA_TAC
 886 THEN THAYTHE_TAC 0[`i`]
 887 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`cstab`][dist;]
 888 THEN POP_ASSUM MP_TAC
 889 THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
 890 THEN REWRITE_TAC[GSYM cstab]
 891 THEN STRIP_TAC
 892 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`&2* h0`][dist;]
 893 THEN POP_ASSUM MP_TAC
 894 THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
 895 THEN REWRITE_TAC[GSYM h0]
 896 THEN STRIP_TAC
 897 THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (i)) (v (SUC (i))) <= arclength (&2) (&2) (cstab)
 898 /\ arcV (vec 0) ((v:num->real^3) (SUC (i))) (v (SUC (SUC (i)))) <=
 899        arclength (&2) (&2) (&2 * h0)
 900 /\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
 901 ==>arcV (vec 0) (v ((i))) (v ((SUC (i))))+ arcV (vec 0) (v (SUC (i))) (v (SUC (SUC (i))))
 902  < pi`)
 903 THEN ASM_SIMP_TAC[arclength_2h0_cstab]
 904 THEN STRIP_TAC
 905 THEN MRESA_TAC WL_IN_FF[`(i)`;`v`]
 906 THEN MRESA_TAC WL_IN_FF[`SUC (i)`;`v`]
 907 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (i), v (SUC (i))`]
 908 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (i)), v (SUC (SUC (i)))`]
 909 THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (i)`;`v (SUC(SUC (i)))`;`v (SUC (i))`]
 910 THEN POP_ASSUM MP_TAC
 911 THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 912 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`]
 913 THEN STRIP_TAC
 914 THEN STRIP_TAC
 915 THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`]
 916 THEN REMOVE_ASSUM_TAC
 917 THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`]
 918 ;
 919
 920
 921
 922
 923
 924
 925 MRESA_TAC DIST_LE2_BB_CASSE_5[`s`;`v`;`3+i`]
 926 THEN MP_TAC Local_lemmas.CVLF_LF_F
 927 THEN RESA_TAC
 928 ;
 929
 930
 931
 932
 933
 934 REWRITE_TAC[ARITH_RULE`0+a=a`]
 935 THEN STRIP_TAC
 936 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`(3+i)`]
 937 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (3+i)`]
 938 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (3+i))`]
 939 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(3+i)`]
 940 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (3+i)`]
 941 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (3+i)`;`v (SUC (3+i))`;`&2* h0`][dist;]
 942 THEN POP_ASSUM MP_TAC
 943 THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
 944 THEN REWRITE_TAC[GSYM h0]
 945 THEN STRIP_TAC
 946 THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
 947 THEN RESA_TAC
 948 THEN THAYTHE_TAC 0[`SUC (3+i)`]
 949 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (3+i))`;`v (SUC(SUC (3+i)))`;`cstab`][dist;]
 950 THEN POP_ASSUM MP_TAC
 951 THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
 952 THEN REWRITE_TAC[GSYM cstab]
 953 THEN STRIP_TAC
 954 THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (3+i)) (v (SUC (3+i))) <= arclength (&2) (&2) (&2 * h0)
 955 /\ arcV (vec 0) ((v:num->real^3) (SUC (3+i))) (v (SUC (SUC (3+i)))) <=
 956       arclength (&2) (&2) (cstab)
 957 /\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
 958 ==>arcV (vec 0) (v ((3+i))) (v ((SUC (3+i))))+ arcV (vec 0) (v (SUC (3+i))) (v (SUC (SUC (3+i))))
 959  < pi`)
 960 THEN ASM_SIMP_TAC[arclength_2h0_cstab]
 961 THEN STRIP_TAC
 962 THEN MRESA_TAC WL_IN_FF[`(3+i)`;`v`]
 963 THEN MRESA_TAC WL_IN_FF[`SUC (3+i)`;`v`]
 964 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (3+i), v (SUC (3+i))`]
 965 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (3+i)), v (SUC (SUC (3+i)))`]
 966 THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (3+i)`;`v (SUC(SUC (3+i)))`;`v (SUC (3+i))`]
 967 THEN POP_ASSUM MP_TAC
 968 THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 969 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(3+i))= 1*5+i`]
 970 THEN STRIP_TAC
 971 THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`]
 972 THEN REMOVE_ASSUM_TAC
 973 THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (3+i)}`]
 974 THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(1*5+i):num`;`v:num->real^3`;`(1*5+i) MOD k`]
 975 THEN POP_ASSUM MP_TAC
 976 THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`]
 977 THEN RESA_TAC
 978 THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i`]
 979 THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i MOD k):num`;`v:num->real^3`;`i`]
 980 THEN POP_ASSUM MP_TAC
 981 THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`]
 982 THEN RESA_TAC
 983 THEN DICH_TAC 5
 984 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 985 THEN RESA_TAC;
 986
 987
 988
 989
 990 REWRITE_TAC[ARITH_RULE`0+a=a`]
 991 THEN STRIP_TAC
 992 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`(3+i)`]
 993 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (3+i)`]
 994 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (3+i))`]
 995 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(3+i)`]
 996 THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (3+i)`]
 997 THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
 998 THEN RESA_TAC
 999 THEN THAYTHE_TAC 0[`(3+i)`]
1000 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (3+i)`;`v (SUC (3+i))`;`cstab`][dist;]
1001 THEN POP_ASSUM MP_TAC
1002 THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
1003 THEN REWRITE_TAC[GSYM cstab]
1004 THEN STRIP_TAC
1005 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (3+i))`;`v (SUC(SUC (3+i)))`;`&2* h0`][dist;]
1006 THEN POP_ASSUM MP_TAC
1007 THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
1008 THEN REWRITE_TAC[GSYM h0]
1009 THEN STRIP_TAC
1010 THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (3+i)) (v (SUC (3+i))) <= arclength (&2) (&2)  (cstab)
1011 /\ arcV (vec 0) ((v:num->real^3) (SUC (3+i))) (v (SUC (SUC (3+i)))) <=
1012       arclength (&2) (&2) (&2 * h0)
1013 /\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
1014 ==>arcV (vec 0) (v ((3+i))) (v ((SUC (3+i))))+ arcV (vec 0) (v (SUC (3+i))) (v (SUC (SUC (3+i))))
1015  < pi`)
1016 THEN ASM_SIMP_TAC[arclength_2h0_cstab]
1017 THEN STRIP_TAC
1018 THEN MRESA_TAC WL_IN_FF[`(3+i)`;`v`]
1019 THEN MRESA_TAC WL_IN_FF[`SUC (3+i)`;`v`]
1020 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (3+i), v (SUC (3+i))`]
1021 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (3+i)), v (SUC (SUC (3+i)))`]
1022 THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (3+i)`;`v (SUC(SUC (3+i)))`;`v (SUC (3+i))`]
1023 THEN POP_ASSUM MP_TAC
1024 THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1025 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(3+i))= 1*5+i`]
1026 THEN STRIP_TAC
1027 THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`]
1028 THEN REMOVE_ASSUM_TAC
1029 THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (3+i)}`]
1030 THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(1*5+i):num`;`v:num->real^3`;`(1*5+i) MOD k`]
1031 THEN POP_ASSUM MP_TAC
1032 THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`]
1033 THEN RESA_TAC
1034 THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i`]
1035 THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i MOD k):num`;`v:num->real^3`;`i`]
1036 THEN POP_ASSUM MP_TAC
1037 THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`]
1038 THEN RESA_TAC
1039 THEN DICH_TAC 5
1040 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1041 THEN RESA_TAC;
1042
1043
1044 ]);;
1045
1046
1047
1048  end;;
1049
1050
1051 (*
1052 let check_completeness_claimA_concl =
1053   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
1054 *)
1055
1056
1057
1058