(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Chapter: Local Fan *) (* Author: Hoang Le Truong *) (* Date: 2012-04-01 *) (* ========================================================================= *) (* remaining conclusions from appendix to Local Fan chapter *) module Axjrpnc = struct open Polyhedron;; open Sphere;; open Topology;; open Fan_misc;; open Planarity;; open Conforming;; open Hypermap;; open Fan;; open Topology;; open Wrgcvdr_cizmrrh;; open Local_lemmas;; open Collect_geom;; open Dih2k_hypermap;; open Wjscpro;; open Tecoxbm;; open Hdplygy;; open Nkezbfc_local;; open Flyspeck_constants;; open Gbycpxs;; open Pcrttid;; open Local_lemmas1;; open Pack_defs;; open Hales_tactic;; open Appendix;; open Hypermap;; open Fan;; open Wrgcvdr_cizmrrh;; open Local_lemmas;; open Flyspeck_constants;; open Pack_defs;; open Hales_tactic;; open Appendix;; open Zithlqn;; open Xwitccn;; open Ayqjtmd;; open Jkqewgv;; open Mtuwlun;; open Uxckfpe;; open Sgtrnaf;; open Yxionxl;; open Qknvmlb;; open Odxlstcv2;; open Yxionxl2;; open Eyypqdw;; open Ocbicby;; open Imjxphr;; open Nuxcoea;; open Fektyiy;; let DIST_LE_2h0_IN_CASES_6=prove(`scs_k_v39 s=6 /\ BBs_v39 s v /\ is_scs_v39 s ==> !i. norm(v i- v (SUC i))<= &2 *h0`, STRIP_TAC THEN POP_ASSUM (fun th-> MP_TAC th THEN ASSUME_TAC th) THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;] THEN RESA_TAC THEN GEN_TAC THEN DICH_TAC (0) THEN REWRITE_TAC[ARITH_RULE`a+b<=b <=> a= 0`] THEN SUBGOAL_THEN`FINITE {i | i < 6 /\ (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC THENL[ MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC`0..6` THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC; MRESA_TAC CARD_EQ_0[`{i | i < 6 /\ (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`] THEN REWRITE_TAC[SET_RULE`A={}<=> !x. ~(x IN A)`;IN_ELIM_THM] THEN MRESAL_TAC DIVISION[`i`;`6`][ARITH_RULE`~(6=0)`] THEN STRIP_TAC THEN THAYTHEL_TAC 0[`i MOD 6`][DE_MORGAN_THM;REAL_ARITH`~(a b<=a`] THEN DICH_TAC (27-1) THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`] THEN STRIP_TAC THEN THAYTHEL_TAC 1[`i`;`SUC i`][dist] THEN POP_ASSUM MP_TAC THEN DICH_TAC(29-24) 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)`] THEN SYM_ASSUM_TAC THEN ASM_SIMP_TAC[Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)`] 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)`] THEN REAL_ARITH_TAC]);; let DIST_EDGE_IN_BB_LE_2=prove(`BBs_v39 s v /\ is_scs_v39 s ==> &2<= norm(v i- v (SUC i))`, DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC th THEN ASSUME_TAC th) THEN REWRITE_TAC[BBs_v39;is_scs_v39;LET_DEF;LET_END_DEF;] THEN STRIP_TAC THEN ABBREV_TAC`k= scs_k_v39 s` THEN THAYTHE_TAC (24-2)[`i`;`SUC i`] THEN THAYTHE_TAC (25-17)[`i MOD k`;`SUC i MOD k`] THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1 y < &0`]; ONCE_REWRITE_TAC[GSYM ATN_0]; MATCH_MP_TAC ATN_MONO_LT; REWRITE_TAC[arith `(x / y < &0 <=> &0 < (-- x)/ y)`]; GMATCH_SIMP_TAC REAL_LT_DIV; GMATCH_SIMP_TAC SQRT_POS_LT; REWRITE_TAC[Sphere.h0]; BY(REAL_ARITH_TAC) ]);; (* }}} *) let is_scs_k_le_3=prove(`is_scs_v39 s ==> 3<= scs_k_v39 s`, REWRITE_TAC[BBs_v39;is_scs_v39;LET_DEF;LET_END_DEF;] THEN RESA_TAC);; let DIST_LE2_BB_CASSE_4= prove_by_refinement(`scs_k_v39 s=4 /\ BBs_v39 s v /\ is_scs_v39 s ==> ?i. norm(v i- v (SUC i))<= &2 *h0`, [ STRIP_TAC THEN POP_ASSUM (fun th-> MP_TAC th THEN ASSUME_TAC th) THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;] THEN RESA_TAC THEN DICH_TAC (0) THEN REWRITE_TAC[ARITH_RULE`a+b<=b <=> a= 0`] THEN SUBGOAL_THEN`FINITE {i | i < 6 /\ (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC; MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC`0..6` THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC; REWRITE_TAC[ARITH_RULE`a+4<=6 <=> a<= 2`] THEN SUBGOAL_THEN`{i | i < 4 /\ (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}SUBSET 0..3` ASSUME_TAC; ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC; STRIP_TAC THEN MRESAL_TAC CARD_DIFF[`0..3`;`{i | i < 4 /\ (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`][FINITE_NUMSEG;CARD_NUMSEG;] THEN MP_TAC(ARITH_RULE`CARD {i | i < 4 /\ (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))} <= 2 /\ CARD ((0..3) DIFF {i | i < 4 /\ (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}) = (3 + 1) - 0 - CARD {i | i < 4 /\ (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))} ==> 0 ?a. a IN A`;DIFF;IN_ELIM_THM;IN_ELIM_THM;IN_NUMSEG] THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`a<=3==> a<4`) THEN RESA_TAC THEN REWRITE_TAC[DE_MORGAN_THM;REAL_ARITH`~(a b<=a`] THEN REPEAT RESA_TAC THEN DICH_TAC (30-1) THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`] THEN STRIP_TAC THEN THAYTHEL_TAC 1[`a`;`SUC a`][dist] THEN EXISTS_TAC`a:num` THEN POP_ASSUM MP_TAC THEN DICH_TAC (33-27) THEN REAL_ARITH_TAC]);; let NORM_V_IN_BB_LE_CSTAB=prove(` (!i. scs_b_v39 s i (SUC i) <= cstab) /\ BBs_v39 s v ==> !i. norm (v i- v (SUC i))<= cstab`, REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;dist] THEN RESA_TAC THEN GEN_TAC THEN THAYTHE_TAC 1[`i`;`SUC i`] THEN THAYTHE_TAC 5[`i`] THEN ASM_TAC THEN REAL_ARITH_TAC);; let arclength_2h0_cstab = prove_by_refinement( `arclength (&2) (&2) (&2 *h0) + arclength (&2) (&2) cstab < pi`, (* {{{ proof *) [ REPEAT (GMATCH_SIMP_TAC Compute_2158872499.ATN_UPS_X_BREAKDOWN1); REWRITE_TAC[GSYM CONJ_ASSOC]; CONJ_TAC; BY(REWRITE_TAC[Sphere.h0;Sphere.cstab] THEN REAL_ARITH_TAC); CONJ_TAC; BY(REWRITE_TAC[Sphere.h0;Sphere.cstab] THEN REAL_ARITH_TAC); REWRITE_TAC[arith `(pi/ &2 + b) + (pi / &2 + d) < pi <=> b + d < &0`]; REWRITE_TAC[Sphere.h0;Sphere.cstab]; MP_TAC (Flyspeck_constants.calc `atn (((&2 * #1.26) * &2 * #1.26 - &2 * &2 - &2 * &2) / sqrt ((&2 + &2 + &2 * #1.26) * (&2 + &2 - &2 * #1.26) * (&2 + &2 * #1.26 - &2) * (&2 * #1.26 + &2 - &2))) + atn (( #3.01 * #3.01 - &2 * &2 - &2 * &2) / sqrt ((&2 + &2 + #3.01) * (&2 + &2 - #3.01) * (&2 + #3.01 - &2) * ( #3.01 + &2 - &2))) < &0`); BY(REWRITE_TAC[]) ]);; (* }}} *) let DIST_LE2_BB_CASSE_5 = prove_by_refinement( `scs_k_v39 s=5 /\ BBs_v39 s v /\ is_scs_v39 s ==> norm(v i- v (SUC i))<= &2 *h0 \/ norm(v (SUC i)- v (SUC (SUC i)))<= &2 *h0 `, [ STRIP_TAC THEN POP_ASSUM (fun th-> MP_TAC th THEN ASSUME_TAC th) THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;] THEN RESA_TAC THEN DICH_TAC (0) THEN REWRITE_TAC[ARITH_RULE`a+b<=b <=> a= 0`] THEN SUBGOAL_THEN`FINITE {i | i < 5 /\ (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC; MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC`0..5` THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC; REWRITE_TAC[ARITH_RULE`a+5<=6 <=> a<= 1`] THEN STRIP_TAC THEN MP_TAC(SET_RULE`norm (v i - v (SUC i)) <= &2 * h0 \/ norm (v (SUC i) - (v:num->real^3) (SUC (SUC i))) <= &2 * h0 \/ ~(norm (v i - v (SUC i)) <= &2 * h0 \/ norm (v (SUC i) - v (SUC (SUC i))) <= &2 * h0)`) THEN RESA_TAC; DICH_TAC 1 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[DE_MORGAN_THM;REAL_ARITH`~(a<=b) <=> b MRESAL_TAC th[`i`;`SUC i`][dist] THEN MRESAL_TAC th[`SUC i`;`SUC (SUC i)`][dist]) 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)) ==> &2 * h0< scs_b_v39 s (SUC i) (SUC (SUC i)) /\ &2 * h0< scs_b_v39 s (i) (SUC (i))`) THEN RESA_TAC THEN SUBGOAL_THEN`{i MOD 5,SUC i MOD 5} SUBSET {i | i < 5 /\ (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC; REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {c,b}<=> a= c\/ a= b`] THEN REPEAT RESA_TAC; ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]; 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] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN ASM_SIMP_TAC[Hypermap.lemma_suc_mod;ARITH_RULE`~(5=0)`] 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] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`] THEN RESA_TAC; ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]; 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] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN ASM_SIMP_TAC[Hypermap.lemma_suc_mod;ARITH_RULE`~(5=0)`] 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] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`] THEN RESA_TAC; MRESA_TAC Hypermap.CARD_TWO_ELEMENTS[`i MOD 5`;`SUC i MOD 5`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`] THEN STRIP_TAC THEN MRESA_TAC CARD_SUBSET[`{i MOD 5, SUC i MOD 5}`;` {i | i < 5 /\ (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`] THEN POP_ASSUM MP_TAC THEN ARITH_TAC]);; let AXJRPNC_concl = `!s (v:num->real^3) i j. is_scs_v39 s /\ scs_basic_v39 s /\ (!i. scs_b_v39 s i (SUC i) <= cstab) /\ MMs_v39 s v /\ (lunar (v i,v j) (IMAGE v (:num)) (IMAGE (\i. {v i, v (SUC i)}) (:num)) ) ==> (scs_k_v39 s = 6 /\ v j = v (i + 3))`;; let AXJRPNC = prove_by_refinement( AXJRPNC_concl, [ REPEAT GEN_TAC THEN ABBREV_TAC`k=scs_k_v39 s` THEN ABBREV_TAC`V=(IMAGE (v:num->real^3) (:num))` THEN ABBREV_TAC`E=(IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num))` THEN ABBREV_TAC`FF=IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)` THEN STRIP_TAC THEN MP_TAC Qknvmlb.SCS_K_LE_6 THEN RESA_TAC THEN MP_TAC(ARITH_RULE`k<=6==> k=6\/ k<6`) THEN RESA_TAC; MRESA_TAC MMS_IMP_BBS[`s`;`v`] THEN MP_TAC DIST_LE_2h0_IN_CASES_6 THEN RESA_TAC; MRESAL_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k`;`s`;`v`][ARITH_RULE`3<6`] THEN ASSUME_TAC(ARITH_RULE`3<6/\ ~(6<=3)`) 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`] THEN MRESA_TAC Local_lemmas.NEXT_OPOSITE_POINT_IS_NOT_IN_AFF_GT2[`E`;`v j`;`V`;`FF`;`v i`] THEN DICH_TAC(20-16) THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v i`;`v`;`i`] THEN MP_TAC(ARITH_RULE`i'+1<6/\ ~(i'=0)/\ ~(i'=1)==> i'=2\/ i'=4\/ i'=3`) THEN RESA_TAC; STRIP_TAC THEN POP_ASSUM(fun th-> ASM_TAC THEN MP_TAC th THEN REPEAT RESA_TAC) THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`&2* h0`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`] THEN REWRITE_TAC[GSYM h0] THEN STRIP_TAC THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`&2* h0`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`] THEN REWRITE_TAC[GSYM h0] THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v i) (v (SUC i)) <= arclength (&2) (&2) (&2 * h0) /\ arcV (vec 0) ((v:num->real^3) (SUC i)) (v (SUC (SUC i))) <= arclength (&2) (&2) (&2 * h0) /\ arclength (&2) (&2) (&2 * h0)< pi/ &2 ==>arcV (vec 0) (v (i)) (v ((SUC i)))+ arcV (vec 0) (v (SUC i)) (v (SUC (SUC i))) < pi`) THEN ASM_SIMP_TAC[arclength222h0] THEN STRIP_TAC THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC THEN MRESA_TAC WL_IN_FF[`i`;`v`] THEN MRESA_TAC WL_IN_FF[`SUC i`;`v`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v i, v (SUC i)`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC i), v (SUC (SUC i))`] THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v i`;`v (SUC(SUC i))`;`v (SUC i)`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN RESA_TAC THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(2+i)`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ARITH_RULE`2+i= SUC(SUC i)`;] THEN STRIP_TAC THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (SUC (SUC i))}`]; STRIP_TAC THEN POP_ASSUM(fun th-> ASM_TAC THEN MP_TAC th THEN REPEAT RESA_TAC) THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`4+i`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (4+i)`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (4+i))`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(4+i)`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (4+i)`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (4+i)`;`v (SUC (4+i))`;`&2* h0`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`] THEN REWRITE_TAC[GSYM h0] THEN STRIP_TAC THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (4+i))`;`v (SUC(SUC (4+i)))`;`&2* h0`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`] THEN REWRITE_TAC[GSYM h0] THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (4+i)) (v (SUC (4+i))) <= arclength (&2) (&2) (&2 * h0) /\ arcV (vec 0) ((v:num->real^3) (SUC (4+i))) (v (SUC (SUC (4+i)))) <= arclength (&2) (&2) (&2 * h0) /\ arclength (&2) (&2) (&2 * h0)< pi/ &2 ==>arcV (vec 0) (v ((4+i))) (v ((SUC (4+i))))+ arcV (vec 0) (v (SUC (4+i))) (v (SUC (SUC (4+i)))) < pi`) THEN ASM_SIMP_TAC[arclength222h0] THEN STRIP_TAC THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC THEN MRESA_TAC WL_IN_FF[`(4+i)`;`v`] THEN MRESA_TAC WL_IN_FF[`SUC (4+i)`;`v`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (4+i), v (SUC (4+i))`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (4+i)), v (SUC (SUC (4+i)))`] THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (4+i)`;`v (SUC(SUC (4+i)))`;`v (SUC (4+i))`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(4+i))= 1*6+i`] 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`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(6=0)`] THEN RESA_TAC THEN MRESA_TAC MOD_MULT_ADD[`1`;`6`;`i`] THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i MOD k):num`;`v:num->real^3`;`i`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(6=0)`] THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(4+i)`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[ARITH_RULE`2+i= SUC(SUC i)`;] THEN STRIP_TAC THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (4+i)}`] ; ONCE_REWRITE_TAC[ARITH_RULE`3+i=i+3`] THEN REWRITE_TAC[]; MP_TAC is_scs_k_le_3 THEN RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k/\ k<6==> k=3\/ (3real^3`;`i MOD k`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(3=0)`] THEN RESA_TAC THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`j:num`;`v:num->real^3`;`j MOD k`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(3=0)`] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`i MOD 3< 3==> i MOD 3= 0\/ i MOD 3= 1\/ i MOD 3=2`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(3=0)`] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`j MOD 3< 3==> j MOD 3= 0\/ j MOD 3= 1\/ j MOD 3=2`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(3=0)`] THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C} ={A,C,B}`] THEN ASM_REWRITE_TAC[] ; MRESA_TAC MMS_IMP_BBS[`s`;`v`] THEN MRESAL_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k`;`s`;`v`][ARITH_RULE`3<6`] THEN ASSUME_TAC(ARITH_RULE`3<4/\ ~(4<=3)`) 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`] THEN MRESA_TAC Local_lemmas.NEXT_OPOSITE_POINT_IS_NOT_IN_AFF_GT2[`E`;`v j`;`V`;`FF`;`v i`] THEN DICH_TAC(22-18) THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v i`;`v`;`i`] THEN MP_TAC(ARITH_RULE`i'+1<4/\ ~(i'=0)/\ ~(i'=1)==> i'=2`) THEN RESA_TAC; MP_TAC DIST_LE2_BB_CASSE_4 THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC THEN MRESA_TAC WL_IN_V[`i`;`v`] THEN MRESA_TAC Localization.LOFA_IMP_LT_CARD_SET_V_ALT[`V`;`E`;`FF`;`v i`] THEN MRESA_TAC WL_IN_V[`i''`;`v`] THEN POP_ASSUM MP_TAC THEN SYM_ASSUM_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN RESA_TAC THEN MRESA_TAC Nuxcoea.W_IN_BB_FUN_EQ[`v:num->real^3`;`i'':num`;`n+i:num`;`s`] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i''`;`n+i:num`;`k`][ARITH_RULE`~(4=0)`] 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)`] THEN MP_TAC(ARITH_RULE`n<4==> n=0\/ n=1\/ n=2\/ n=3`) THEN RESA_TAC; REWRITE_TAC[ARITH_RULE`0+a=a`] THEN STRIP_TAC THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`&2* h0`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`] THEN REWRITE_TAC[GSYM h0] THEN STRIP_TAC THEN MP_TAC NORM_V_IN_BB_LE_CSTAB THEN RESA_TAC THEN THAYTHE_TAC 0[`SUC i`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`cstab`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`] THEN REWRITE_TAC[GSYM cstab] THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (i)) (v (SUC (i))) <= arclength (&2) (&2) (&2 * h0) /\ arcV (vec 0) ((v:num->real^3) (SUC (i))) (v (SUC (SUC (i)))) <= arclength (&2) (&2) (cstab) /\ arclength (&2) (&2) (&2 * h0) + arclength (&2) (&2) (cstab) < pi ==>arcV (vec 0) (v ((i))) (v ((SUC (i))))+ arcV (vec 0) (v (SUC (i))) (v (SUC (SUC (i)))) < pi`) THEN ASM_SIMP_TAC[arclength_2h0_cstab] THEN STRIP_TAC THEN MRESA_TAC WL_IN_FF[`(i)`;`v`] THEN MRESA_TAC WL_IN_FF[`SUC (i)`;`v`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (i), v (SUC (i))`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (i)), v (SUC (SUC (i)))`] THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (i)`;`v (SUC(SUC (i)))`;`v (SUC (i))`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`] THEN STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`] THEN REMOVE_ASSUM_TAC THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`] ; REWRITE_TAC[ARITH_RULE`1+a=SUC a`] THEN STRIP_TAC THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`] THEN MP_TAC NORM_V_IN_BB_LE_CSTAB THEN RESA_TAC THEN THAYTHE_TAC 0[`i`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`cstab`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`] THEN REWRITE_TAC[GSYM cstab] THEN STRIP_TAC THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`&2* h0`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`] THEN REWRITE_TAC[GSYM h0] THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (i)) (v (SUC (i))) <= arclength (&2) (&2) (cstab) /\ arcV (vec 0) ((v:num->real^3) (SUC (i))) (v (SUC (SUC (i)))) <= arclength (&2) (&2) (&2 * h0) /\ arclength (&2) (&2) (&2 * h0) + arclength (&2) (&2) (cstab) < pi ==>arcV (vec 0) (v ((i))) (v ((SUC (i))))+ arcV (vec 0) (v (SUC (i))) (v (SUC (SUC (i)))) < pi`) THEN ASM_SIMP_TAC[arclength_2h0_cstab] THEN STRIP_TAC THEN MRESA_TAC WL_IN_FF[`(i)`;`v`] THEN MRESA_TAC WL_IN_FF[`SUC (i)`;`v`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (i), v (SUC (i))`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (i)), v (SUC (SUC (i)))`] THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (i)`;`v (SUC(SUC (i)))`;`v (SUC (i))`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`] THEN STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`] THEN REMOVE_ASSUM_TAC THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`] ; REWRITE_TAC[ARITH_RULE`0+a=a`] THEN STRIP_TAC THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`(2+i)`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (2+i)`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (2+i))`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(2+i)`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (2+i)`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (2+i)`;`v (SUC (2+i))`;`&2* h0`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`] THEN REWRITE_TAC[GSYM h0] THEN STRIP_TAC THEN MP_TAC NORM_V_IN_BB_LE_CSTAB THEN RESA_TAC THEN THAYTHE_TAC 0[`SUC (2+i)`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (2+i))`;`v (SUC(SUC (2+i)))`;`cstab`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`] THEN REWRITE_TAC[GSYM cstab] THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (2+i)) (v (SUC (2+i))) <= arclength (&2) (&2) (&2 * h0) /\ arcV (vec 0) ((v:num->real^3) (SUC (2+i))) (v (SUC (SUC (2+i)))) <= arclength (&2) (&2) (cstab) /\ arclength (&2) (&2) (&2 * h0) + arclength (&2) (&2) (cstab) < pi ==>arcV (vec 0) (v ((2+i))) (v ((SUC (2+i))))+ arcV (vec 0) (v (SUC (2+i))) (v (SUC (SUC (2+i)))) < pi`) THEN ASM_SIMP_TAC[arclength_2h0_cstab] THEN STRIP_TAC THEN MRESA_TAC WL_IN_FF[`(2+i)`;`v`] THEN MRESA_TAC WL_IN_FF[`SUC (2+i)`;`v`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (2+i), v (SUC (2+i))`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (2+i)), v (SUC (SUC (2+i)))`] THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (2+i)`;`v (SUC(SUC (2+i)))`;`v (SUC (2+i))`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`] THEN STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`] THEN REMOVE_ASSUM_TAC THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`] THEN DICH_TAC 3 THEN ASM_REWRITE_TAC[ARITH_RULE`2+2+i= 1*4+i`] 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`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(4=0)`] THEN RESA_TAC THEN MRESA_TAC MOD_MULT_ADD[`1`;`4`;`i`] THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i MOD k):num`;`v:num->real^3`;`i`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(4=0)`] THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN RESA_TAC; REWRITE_TAC[ARITH_RULE`3+i=SUC(2+i)`] THEN STRIP_TAC THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`(2+i)`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (2+i)`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (2+i))`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(2+i)`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (2+i)`] THEN MP_TAC NORM_V_IN_BB_LE_CSTAB THEN RESA_TAC THEN THAYTHE_TAC 0[`(2+i)`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (2+i)`;`v (SUC (2+i))`;`cstab`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`] THEN REWRITE_TAC[GSYM cstab] THEN STRIP_TAC THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (2+i))`;`v (SUC(SUC (2+i)))`;`&2* h0`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`] THEN REWRITE_TAC[GSYM h0] THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (2+i)) (v (SUC (2+i))) <= arclength (&2) (&2) (cstab) /\ arcV (vec 0) ((v:num->real^3) (SUC (2+i))) (v (SUC (SUC (2+i)))) <= arclength (&2) (&2) (&2 * h0) /\ arclength (&2) (&2) (&2 * h0) + arclength (&2) (&2) (cstab) < pi ==>arcV (vec 0) (v ((2+i))) (v ((SUC (2+i))))+ arcV (vec 0) (v (SUC (2+i))) (v (SUC (SUC (2+i)))) < pi`) THEN ASM_SIMP_TAC[arclength_2h0_cstab] THEN STRIP_TAC THEN MRESA_TAC WL_IN_FF[`(2+i)`;`v`] THEN MRESA_TAC WL_IN_FF[`SUC (2+i)`;`v`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (2+i), v (SUC (2+i))`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (2+i)), v (SUC (SUC (2+i)))`] THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (2+i)`;`v (SUC(SUC (2+i)))`;`v (SUC (2+i))`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`] THEN STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`] THEN REMOVE_ASSUM_TAC THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`] THEN DICH_TAC 3 THEN ASM_REWRITE_TAC[ARITH_RULE`2+2+i= 1*4+i`] 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`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(4=0)`] THEN RESA_TAC THEN MRESA_TAC MOD_MULT_ADD[`1`;`4`;`i`] THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i MOD k):num`;`v:num->real^3`;`i`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(4=0)`] THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN RESA_TAC; MRESA_TAC MMS_IMP_BBS[`s`;`v`] THEN MRESAL_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k`;`s`;`v`][ARITH_RULE`3<5`] THEN ASSUME_TAC(ARITH_RULE`3<5/\ ~(5<=3)`) 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`] THEN MRESA_TAC Local_lemmas.NEXT_OPOSITE_POINT_IS_NOT_IN_AFF_GT2[`E`;`v j`;`V`;`FF`;`v i`] THEN DICH_TAC(22-18) THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v i`;`v`;`i`] THEN MP_TAC(ARITH_RULE`i'+1<5/\ ~(i'=0)/\ ~(i'=1)==> i'=2\/ i'=3`) THEN RESA_TAC; MP_TAC DIST_LE2_BB_CASSE_5 THEN RESA_TAC THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC ; REWRITE_TAC[ARITH_RULE`0+a=a`] THEN STRIP_TAC THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`&2* h0`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`] THEN REWRITE_TAC[GSYM h0] THEN STRIP_TAC THEN MP_TAC NORM_V_IN_BB_LE_CSTAB THEN RESA_TAC THEN THAYTHE_TAC 0[`SUC i`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`cstab`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`] THEN REWRITE_TAC[GSYM cstab] THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (i)) (v (SUC (i))) <= arclength (&2) (&2) (&2 * h0) /\ arcV (vec 0) ((v:num->real^3) (SUC (i))) (v (SUC (SUC (i)))) <= arclength (&2) (&2) (cstab) /\ arclength (&2) (&2) (&2 * h0) + arclength (&2) (&2) (cstab) < pi ==>arcV (vec 0) (v ((i))) (v ((SUC (i))))+ arcV (vec 0) (v (SUC (i))) (v (SUC (SUC (i)))) < pi`) THEN ASM_SIMP_TAC[arclength_2h0_cstab] THEN STRIP_TAC THEN MRESA_TAC WL_IN_FF[`(i)`;`v`] THEN MRESA_TAC WL_IN_FF[`SUC (i)`;`v`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (i), v (SUC (i))`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (i)), v (SUC (SUC (i)))`] THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (i)`;`v (SUC(SUC (i)))`;`v (SUC (i))`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`] THEN STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`] THEN REMOVE_ASSUM_TAC THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`] ; REWRITE_TAC[ARITH_RULE`1+a=SUC a`] THEN STRIP_TAC THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`] THEN MP_TAC NORM_V_IN_BB_LE_CSTAB THEN RESA_TAC THEN THAYTHE_TAC 0[`i`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`cstab`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`] THEN REWRITE_TAC[GSYM cstab] THEN STRIP_TAC THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`&2* h0`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`] THEN REWRITE_TAC[GSYM h0] THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (i)) (v (SUC (i))) <= arclength (&2) (&2) (cstab) /\ arcV (vec 0) ((v:num->real^3) (SUC (i))) (v (SUC (SUC (i)))) <= arclength (&2) (&2) (&2 * h0) /\ arclength (&2) (&2) (&2 * h0) + arclength (&2) (&2) (cstab) < pi ==>arcV (vec 0) (v ((i))) (v ((SUC (i))))+ arcV (vec 0) (v (SUC (i))) (v (SUC (SUC (i)))) < pi`) THEN ASM_SIMP_TAC[arclength_2h0_cstab] THEN STRIP_TAC THEN MRESA_TAC WL_IN_FF[`(i)`;`v`] THEN MRESA_TAC WL_IN_FF[`SUC (i)`;`v`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (i), v (SUC (i))`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (i)), v (SUC (SUC (i)))`] THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (i)`;`v (SUC(SUC (i)))`;`v (SUC (i))`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`] THEN STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`] THEN REMOVE_ASSUM_TAC THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (2+i)}`] ; MRESA_TAC DIST_LE2_BB_CASSE_5[`s`;`v`;`3+i`] THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC ; REWRITE_TAC[ARITH_RULE`0+a=a`] THEN STRIP_TAC THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`(3+i)`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (3+i)`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (3+i))`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(3+i)`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (3+i)`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (3+i)`;`v (SUC (3+i))`;`&2* h0`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`] THEN REWRITE_TAC[GSYM h0] THEN STRIP_TAC THEN MP_TAC NORM_V_IN_BB_LE_CSTAB THEN RESA_TAC THEN THAYTHE_TAC 0[`SUC (3+i)`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (3+i))`;`v (SUC(SUC (3+i)))`;`cstab`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`] THEN REWRITE_TAC[GSYM cstab] THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (3+i)) (v (SUC (3+i))) <= arclength (&2) (&2) (&2 * h0) /\ arcV (vec 0) ((v:num->real^3) (SUC (3+i))) (v (SUC (SUC (3+i)))) <= arclength (&2) (&2) (cstab) /\ arclength (&2) (&2) (&2 * h0) + arclength (&2) (&2) (cstab) < pi ==>arcV (vec 0) (v ((3+i))) (v ((SUC (3+i))))+ arcV (vec 0) (v (SUC (3+i))) (v (SUC (SUC (3+i)))) < pi`) THEN ASM_SIMP_TAC[arclength_2h0_cstab] THEN STRIP_TAC THEN MRESA_TAC WL_IN_FF[`(3+i)`;`v`] THEN MRESA_TAC WL_IN_FF[`SUC (3+i)`;`v`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (3+i), v (SUC (3+i))`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (3+i)), v (SUC (SUC (3+i)))`] THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (3+i)`;`v (SUC(SUC (3+i)))`;`v (SUC (3+i))`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(3+i))= 1*5+i`] THEN STRIP_TAC THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`] THEN REMOVE_ASSUM_TAC THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (3+i)}`] 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`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i`] THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i MOD k):num`;`v:num->real^3`;`i`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN DICH_TAC 5 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN RESA_TAC; REWRITE_TAC[ARITH_RULE`0+a=a`] THEN STRIP_TAC THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`(3+i)`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (3+i)`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (3+i))`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(3+i)`] THEN MRESA_TAC DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (3+i)`] THEN MP_TAC NORM_V_IN_BB_LE_CSTAB THEN RESA_TAC THEN THAYTHE_TAC 0[`(3+i)`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (3+i)`;`v (SUC (3+i))`;`cstab`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`] THEN REWRITE_TAC[GSYM cstab] THEN STRIP_TAC THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (3+i))`;`v (SUC(SUC (3+i)))`;`&2* h0`][dist;] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`] THEN REWRITE_TAC[GSYM h0] THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (3+i)) (v (SUC (3+i))) <= arclength (&2) (&2) (cstab) /\ arcV (vec 0) ((v:num->real^3) (SUC (3+i))) (v (SUC (SUC (3+i)))) <= arclength (&2) (&2) (&2 * h0) /\ arclength (&2) (&2) (&2 * h0) + arclength (&2) (&2) (cstab) < pi ==>arcV (vec 0) (v ((3+i))) (v ((SUC (3+i))))+ arcV (vec 0) (v (SUC (3+i))) (v (SUC (SUC (3+i)))) < pi`) THEN ASM_SIMP_TAC[arclength_2h0_cstab] THEN STRIP_TAC THEN MRESA_TAC WL_IN_FF[`(3+i)`;`v`] THEN MRESA_TAC WL_IN_FF[`SUC (3+i)`;`v`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (3+i), v (SUC (3+i))`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (3+i)), v (SUC (SUC (3+i)))`] THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (3+i)`;`v (SUC(SUC (3+i)))`;`v (SUC (3+i))`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(3+i))= 1*5+i`] THEN STRIP_TAC THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v i`;`v(j)`] THEN REMOVE_ASSUM_TAC THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v i, v (3+i)}`] 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`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN MRESA_TAC MOD_MULT_ADD[`1`;`5`;`i`] THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i MOD k):num`;`v:num->real^3`;`i`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_REFL;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN DICH_TAC 5 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN RESA_TAC; ]);; end;; (* let check_completeness_claimA_concl = Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) *)