1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Local Fan *)
5 (* Author: Hoang Le Truong *)
7 (* ========================================================================= *)
11 remaining conclusions from appendix to Local Fan chapter
15 module Axjrpnc = struct
27 open Wrgcvdr_cizmrrh;;
35 open Flyspeck_constants;;
51 open Wrgcvdr_cizmrrh;;
53 open Flyspeck_constants;;
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`,
95 THEN POP_ASSUM (fun th-> MP_TAC th
97 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
101 THEN REWRITE_TAC[ARITH_RULE`a+b<=b <=> a= 0`]
102 THEN SUBGOAL_THEN`FINITE
104 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC
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]
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)`]
117 THEN THAYTHEL_TAC 0[`i MOD 6`][DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`]
119 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`]
121 THEN THAYTHEL_TAC 1[`i`;`SUC i`][dist]
122 THEN POP_ASSUM MP_TAC
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)`]
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]);;
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))`,
134 THEN POP_ASSUM(fun th-> MP_TAC th
136 THEN REWRITE_TAC[BBs_v39;is_scs_v39;LET_DEF;LET_END_DEF;]
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`)
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)`]
147 THEN REWRITE_TAC[dist]
148 THEN REAL_ARITH_TAC);;
152 let arclength222h0 = prove_by_refinement(
153 `arclength (&2) (&2) (&2 * h0) < pi / &2`,
156 GMATCH_SIMP_TAC Compute_2158872499.ATN_UPS_X_BREAKDOWN1;
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];
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;]
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`,
184 THEN POP_ASSUM (fun th-> MP_TAC th
186 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
189 THEN REWRITE_TAC[ARITH_RULE`a+b<=b <=> a= 0`]
190 THEN SUBGOAL_THEN`FINITE
192 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC;
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]
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;
204 ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
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
212 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))} <=
216 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}) =
221 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}
225 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))})`)
227 THEN POP_ASSUM MP_TAC
229 THEN MP_TAC(SET_RULE`(0..3) DIFF
231 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}= {}
234 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))} ={})`)
237 REWRITE_TAC[Oxl_2012.CARD_EMPTY]
241 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;DIFF;IN_ELIM_THM;IN_ELIM_THM;IN_NUMSEG]
243 THEN POP_ASSUM MP_TAC
244 THEN MP_TAC(ARITH_RULE`a<=3==> a<4`)
246 THEN REWRITE_TAC[DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`]
249 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`]
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]);;
259 let NORM_V_IN_BB_LE_CSTAB=prove(` (!i. scs_b_v39 s i (SUC i) <= cstab) /\
261 ==> !i. norm (v i- v (SUC i))<= cstab`,
262 REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;dist]
265 THEN THAYTHE_TAC 1[`i`;`SUC i`]
266 THEN THAYTHE_TAC 5[`i`]
268 THEN REAL_ARITH_TAC);;
272 let arclength_2h0_cstab = prove_by_refinement(
273 `arclength (&2) (&2) (&2 *h0) + arclength (&2) (&2) cstab < pi`,
276 REPEAT (GMATCH_SIMP_TAC Compute_2158872499.ATN_UPS_X_BREAKDOWN1);
277 REWRITE_TAC[GSYM CONJ_ASSOC];
279 BY(REWRITE_TAC[Sphere.h0;Sphere.cstab] THEN REAL_ARITH_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
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 `,
303 THEN POP_ASSUM (fun th-> MP_TAC th
305 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
308 THEN REWRITE_TAC[ARITH_RULE`a+b<=b <=> a= 0`]
309 THEN SUBGOAL_THEN`FINITE
311 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC;
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]
318 REWRITE_TAC[ARITH_RULE`a+5<=6 <=> a<= 1`]
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)`)
326 THEN POP_ASSUM MP_TAC
327 THEN REWRITE_TAC[DE_MORGAN_THM;REAL_ARITH`~(a<=b) <=> b<a`]
330 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(5<=3)`]
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))`)
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;
341 REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {c,b}<=> a= c\/ a= b`]
342 THEN REPEAT RESA_TAC;
344 ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`];
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)`]
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)`]
356 ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`];
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)`]
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)`]
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`]
372 THEN MRESA_TAC CARD_SUBSET[`{i MOD 5, SUC i MOD 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
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) /\
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))`;;
390 let AXJRPNC = prove_by_refinement(
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)`
399 THEN MP_TAC Qknvmlb.SCS_K_LE_6
401 THEN MP_TAC(ARITH_RULE`k<=6==> k=6\/ k<6`)
405 MRESA_TAC MMS_IMP_BBS[`s`;`v`]
406 THEN MP_TAC DIST_LE_2h0_IN_CASES_6
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`]
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`)
421 THEN POP_ASSUM(fun th-> ASM_TAC
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]
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]
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)))
445 THEN ASM_SIMP_TAC[arclength222h0]
447 THEN MP_TAC Local_lemmas.CVLF_LF_F
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}`]
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)`;]
462 THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (SUC (SUC i))}`];
468 THEN POP_ASSUM(fun th-> ASM_TAC
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]
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]
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))))
492 THEN ASM_SIMP_TAC[arclength222h0]
494 THEN MP_TAC Local_lemmas.CVLF_LF_F
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)`]
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)`]
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)`;]
519 THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (4+i)}`]
522 ONCE_REWRITE_TAC[ARITH_RULE`3+i=i+3`]
529 THEN MP_TAC(ARITH_RULE`3<=k/\ k<6==> k=3\/ (3<k/\ k=4)\/ (3<k/\ k=5)`)
534 MRESA_TAC MMS_IMP_BBS[`s`;`v`]
535 THEN MRESAL_TAC Jkqewgv.IS_SCS_NOT_COLLINEAR_BBs_CASE_3[`s`;`v`][IN]
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)`]
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)`]
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)`]
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)`]
552 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C} ={A,C,B}`]
553 THEN ASM_REWRITE_TAC[]
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`]
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`)
573 MP_TAC DIST_LE2_BB_CASSE_4
575 THEN POP_ASSUM MP_TAC
576 THEN MP_TAC Local_lemmas.CVLF_LF_F
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
583 THEN REWRITE_TAC[IN_ELIM_THM]
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`)
595 REWRITE_TAC[ARITH_RULE`0+a=a`]
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]
607 THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
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]
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))))
621 THEN ASM_SIMP_TAC[arclength_2h0_cstab]
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`]
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)}`]
642 REWRITE_TAC[ARITH_RULE`1+a=SUC a`]
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
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]
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]
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))))
668 THEN ASM_SIMP_TAC[arclength_2h0_cstab]
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`]
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)}`]
687 REWRITE_TAC[ARITH_RULE`0+a=a`]
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]
699 THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
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]
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))))
713 THEN ASM_SIMP_TAC[arclength_2h0_cstab]
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`]
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)}`]
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)`]
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)`]
739 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
745 REWRITE_TAC[ARITH_RULE`3+i=SUC(2+i)`]
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
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]
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]
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))))
771 THEN ASM_SIMP_TAC[arclength_2h0_cstab]
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`]
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)}`]
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)`]
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)`]
797 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
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`]
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`)
818 MP_TAC DIST_LE2_BB_CASSE_5
820 THEN MP_TAC Local_lemmas.CVLF_LF_F
829 REWRITE_TAC[ARITH_RULE`0+a=a`]
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]
841 THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
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]
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))))
855 THEN ASM_SIMP_TAC[arclength_2h0_cstab]
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`]
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)}`]
877 REWRITE_TAC[ARITH_RULE`1+a=SUC a`]
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
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]
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]
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))))
903 THEN ASM_SIMP_TAC[arclength_2h0_cstab]
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`]
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)}`]
925 MRESA_TAC DIST_LE2_BB_CASSE_5[`s`;`v`;`3+i`]
926 THEN MP_TAC Local_lemmas.CVLF_LF_F
934 REWRITE_TAC[ARITH_RULE`0+a=a`]
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]
946 THEN MP_TAC NORM_V_IN_BB_LE_CSTAB
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]
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))))
960 THEN ASM_SIMP_TAC[arclength_2h0_cstab]
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`]
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)`]
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)`]
984 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
990 REWRITE_TAC[ARITH_RULE`0+a=a`]
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
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]
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]
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))))
1016 THEN ASM_SIMP_TAC[arclength_2h0_cstab]
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`]
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)`]
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)`]
1040 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1052 let check_completeness_claimA_concl =
1053 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)