(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Chapter: Local Fan *) (* Author: Hoang Le Truong *) (* Date: 2012-04-01 *) (* ========================================================================= *) (* remaining conclusions from appendix to Local Fan chapter *) module Aursipd = 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 REP_NUMSEG=prove(`~(k=0) ==> {i | i < k}= 0.. (k-1)`, REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC);; let SUM_AZIM_EQ_ANGLE_LE4_FUN=prove_by_refinement( ` ~(scs_k_v39 s<=3)/\ BBs_v39 s vv /\ is_scs_v39 s /\ (vv:num->real^3) (p MOD (scs_k_v39 s))=u /\ IMAGE (vv:num->real^3) (:num)=V/\ IMAGE (\i. {vv i,(vv:num->real^3) (SUC i)}) (:num)=E/\ IMAGE (\i. (vv i,(vv:num->real^3) (SUC i))) (:num)=FF ==> sum {i | i < scs_k_v39 s} (\i. ff((vv:num->real^3) (i+p MOD scs_k_v39 s)) * interior_angle1 (vec 0) FF (ITER i (rho_node1 FF) u)) =sum FF (\e. ff(FST e) * azim_in_fan e E) `, [ MRESA_TAC (GEN_ALL IN_IMAGE_VV)[`p MOD scs_k_v39 s`;`vv:num->real^3`] THEN ASM_TAC THEN ASM_REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;is_scs_v39;scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;scs_diag;dist] THEN ABBREV_TAC`k= scs_k_v39 s` THEN REPEAT RESA_TAC; REPLICATE_TAC (30-2)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[]; MATCH_MP_TAC SUM_EQ_GENERAL THEN EXISTS_TAC`(\i. (vv:num->real^3) (i+ p MOD k), vv (SUC i + p MOD k))` THEN MP_TAC(ARITH_RULE`3<= k ==> ~(k=0) /\ 1(x MOD k+ k- p MOD k) + p MOD k = x MOD k+k /\ (x + p MOD k) + k- p MOD k= x+k`) THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(4=0)`;] THEN POP_ASSUM(fun th-> MRESA1_TAC th `(x MOD k + k - p MOD k) MOD k + p MOD k:num` THEN MRESA1_TAC th ` x:num`) THEN MRESA_TAC MOD_ADD_MOD[`x:num`;`1`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`(x MOD k + k - p MOD k) MOD k + p MOD k`;`1`;`k:num`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(4=0)`;ARITH_RULE`SUC ((x MOD k + k - p MOD k) MOD k) + p MOD k = ((x MOD k + k - p MOD k) MOD k + p MOD k)+1`] THEN POP_ASSUM(fun th-> MRESA1_TAC th `((x MOD k + k - p MOD k) MOD k + p MOD k)+1:num` THEN MRESA1_TAC th ` x+1:num`) THEN REWRITE_TAC[ADD1] THEN REPEAT STRIP_TAC THEN MRESA_TAC DIVISION[`x:num`;`k:num`] THEN MRESA_TAC DIVISION[`y' + p MOD k:num`;`k:num`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(4=0)`;] THEN POP_ASSUM(fun th-> MRESA1_TAC th `y' + p MOD k:num`) THEN MP_TAC VV_INJ THEN ASM_REWRITE_TAC[MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;dsv_v39;scs_slice_v39;scs_half_slice_v39;PAIR_EQ;REAL_ARITH`#0.11 < #0.9`;ARITH_RULE`3<=3`;dist] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA_TAC th[`(y'+ p MOD k) MOD k:num`;`(x MOD k + k)MOD k`]) THEN MRESA_TAC MOD_LT[`y':num`;`k:num`] THEN MRESAL_TAC(GEN_ALL Hdplygy.MOD_EQ_MOD)[`y':num`;`x MOD k + k- p MOD k`;`p MOD k`;`k:num`][] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[ADD_SYM] THEN RESA_TAC; REWRITE_TAC[IN_ELIM_THM;] THEN REPEAT STRIP_TAC; EXPAND_TAC"FF" THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`x+ p MOD k` THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ADD1;ARITH_RULE`(x + 1) + p MOD k= (x + p MOD k)+1`]; MRESAL_TAC(GEN_ALL VV_SUC_EQ_RHO_NODE_PRIME)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`k:num`;`s:scs_v39`;`FF:real^3#real^3->bool`;`u:real^3`;`vv:num->real^3`;`p:num MOD k`] [is_scs_v39;scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;scs_diag;dist] THEN SUBGOAL_THEN`(vv:num->real^3) (x + p MOD k) IN V`ASSUME_TAC; EXPAND_TAC"V" THEN REWRITE_TAC[IN_ELIM_THM;IMAGE] THEN EXISTS_TAC`x+ p MOD k` THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`]; REPLICATE_TAC (35-6)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MP_TAC Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM THEN RESA_TAC THEN POP_ASSUM(fun th-> MRESA_TAC th[`(vv:num->real^3) (x + p MOD k )`]) THEN REPLICATE_TAC (3) REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> ASSUME_TAC th THEN MRESAL1_TAC th`SUC x`[ITER])]);; let PERIODIC_IMAGE2=prove(`~(n = 0) /\ periodic f n ==> {f i | i < n} = IMAGE f (:num)`, STRIP_TAC THEN MRESA_TAC Oxlzlez.PERIODIC_IMAGE[`f`;`n`] THEN SYM_ASSUM_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN SET_TAC[]);; let AURSIPD_concl = `!s v. 3< scs_k_v39 s /\ is_scs_v39 s /\ scs_generic v /\ v IN MMs_v39 s ==> 3 + CARD { i | i < scs_k_v39 s /\ scs_is_str s v i} <= scs_k_v39 s`;; let AURSIPD= prove_by_refinement((AURSIPD_concl), [REWRITE_TAC[IN;scs_is_str;scs_generic] THEN REPEAT STRIP_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 MATCH_MP_TAC(ARITH_RULE`~(b-3< c) /\ 3 3+c <= b:num`) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN SUBGOAL_THEN `CARD {i | i < k /\ azim (vec 0) (v i) (v (SUC i)) (v (i + k - 1)) = pi}<= CARD (0..(k-1))` ASSUME_TAC; MATCH_MP_TAC CARD_SUBSET THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN DICH_TAC 8 THEN ARITH_TAC; POP_ASSUM MP_TAC THEN REWRITE_TAC[CARD_NUMSEG] THEN MP_TAC(ARITH_RULE`3 (k-1+1)-0=k`) THEN RESA_TAC THEN STRIP_TAC THEN SUBGOAL_THEN`{i | i < k /\ azim (vec 0:real^3) (v i) (v (SUC i)) (v (i + k - 1)) = pi} SUBSET (0..(k-1))`ASSUME_TAC; ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN DICH_TAC 8 THEN ARITH_TAC; ABBREV_TAC`a=CARD {i | i < k /\ azim (vec 0) (v i) ((v:num->real^3) (SUC i)) (v (i + k - 1)) = pi}` THEN MP_TAC(ARITH_RULE`3 a=k \/ a =k-1\/ a=k-2`) THEN RESA_TAC; MRESAL_TAC SUBSET_CARD_EQ[`{i | i < k /\ azim (vec 0) (v i) ((v:num->real^3) (SUC i)) (v (i + k - 1)) = pi}`;`0..(k-1)`][FINITE_NUMSEG;CARD_NUMSEG] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG] THEN STRIP_TAC THEN ABBREV_TAC`v0= (v:num->real^3) 0` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`] THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`] THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC THEN MRESA_TAC WL_IN_V[`0`;`v`] THEN MRESA_TAC Odxlstcv2.CARD_V_EQ_SCS_K1[`s`;`v`;`V`;`k:num`] THEN POP_ASSUM MP_TAC THEN MRESAL_TAC Nuxcoea.MMS_IMP_BBPRIME[`s:scs_v39`;`v`][LET_DEF;LET_END_DEF;BBprime_v39] THEN MRESA_TAC JKQEWGV1[`s:scs_v39`;`v`] THEN STRIP_TAC THEN DICH_TAC 1 THEN REWRITE_TAC[REAL_ARITH`~(a< b)<=> b<=a`;sol_local] THEN MATCH_MP_TAC (REAL_ARITH`&0< a/\ b= &0==> a<= &2 *a +b`) THEN REWRITE_TAC[PI_WORKS] THEN MATCH_MP_TAC SUM_EQ_0 THEN GEN_TAC THEN STRIP_TAC THEN MRESA_TAC Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA[`V:real^3->bool`;`FF`;`E`;`x`] THEN MRESA_TAC Local_lemmas.DETER_RHO_NODE[`V:real^3->bool`;`E`;`FF`;`FST x`;`SND x`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IMP_IN_V2[`E`;`FF`;`x`;`V`] THEN MRESA_TAC Local_lemmas1.LF_AZIM_CYCLE_EQ_IVS_ND[`V`;`E`;`FF`;`FST x`] THEN DICH_TAC (27-22) THEN EXPAND_TAC "FF" THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[IMAGE;IN_ELIM_THM] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`3 ~(k<=3)/\ (k+1)-1=k/\ ~(k=0)/\ 1 x' MOD k <= k-1 /\ 0<= x' MOD k `) THEN RESA_TAC THEN RESA_TAC THEN THAYTHEL_TAC 0 [`x' MOD k`][ARITH_RULE`a+1= SUC a/\ a+2= SUC (SUC a)`] THEN POP_ASSUM MP_TAC THEN MRESA_TAC Yxionxl2.MOD_SUC_MOD[`x'`;`k`] THEN MRESA_TAC MOD_REFL[`SUC x' `;`k`] THEN MRESA_TAC MOD_REFL[`x' `;`k`] THEN MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC ((x') MOD k)`;`v:num->real^3`;`SUC ((x') MOD k) MOD k`] THEN MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC (x') MOD k`;`v:num->real^3`;`SUC (x')`] THEN MRESA_TAC WL_IN_V[`x' MOD k`;`v`] THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1 THEN RESA_TAC THEN THAYTHE_TAC 0[`v (x' MOD k)`] THEN POP_ASSUM MP_TAC THEN MRESAL_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v (x' MOD k)`;`v`;` x' MOD k`][ARITH_RULE`a+0=a`] THEN MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`x' MOD k`;`v:num->real^3`;`x'`] THEN STRIP_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`a+k-1=k-1+a`] THEN REAL_ARITH_TAC; MP_TAC(SET_RULE`(!i. i < k ==> azim (vec 0) (v i) (v (SUC i)) (v (i + k - 1)) = pi) \/ ~(!i. i < k ==> azim (vec 0:real^3) (v i) (v (SUC i)) (v (i + k - 1)) = pi)`) THEN RESA_TAC; MP_TAC(SET_RULE`(!i. i < k ==> azim (vec 0) (v i) (v (SUC i)) (v (i + k - 1)) = pi) ==> {i | i < k /\ azim (vec 0) (v i) (v (SUC i)) (v (i + k - 1)) = pi}= {i| i ~(k=0)/\ ~(k=k-1)`) THEN RESA_TAC THEN MRESAL_TAC REP_NUMSEG[`k:num`][CARD_NUMSEG] ; POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[NOT_FORALL_THM;NOT_IMP] THEN REWRITE_TAC[NOT_IMP] THEN STRIP_TAC THEN SUBGOAL_THEN`{i | i < k /\ azim (vec 0:real^3) (v i) (v (SUC i)) (v (i + k - 1)) = pi} SUBSET (0..(k-1)) DELETE i` ASSUME_TAC; MATCH_MP_TAC (SET_RULE`A SUBSET B /\ ~(a IN A) ==> A SUBSET B DELETE a`) THEN ASM_REWRITE_TAC[IN_ELIM_THM]; MRESAL_TAC FINITE_SUBSET[`(0..k - 1) DELETE i`;`(0..k - 1)`][FINITE_NUMSEG;DELETE_SUBSET] THEN SUBGOAL_THEN`i IN 0..(k-1)`ASSUME_TAC ; ASM_REWRITE_TAC[IN_NUMSEG] THEN DICH_TAC 3 THEN DICH_TAC 16 THEN ARITH_TAC; MRESAL_TAC CARD_DELETE[`i`;`0..(k-1)`][FINITE_NUMSEG] THEN MRESAL_TAC SUBSET_CARD_EQ[`{i | i < k /\ azim (vec 0) (v i) ((v:num->real^3) (SUC i)) (v (i + k - 1)) = pi}`;`(0..(k-1)) DELETE i`][FINITE_NUMSEG;CARD_NUMSEG] ; POP_ASSUM MP_TAC THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG] THEN STRIP_TAC THEN ABBREV_TAC`v0= (v:num->real^3) 0` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`] THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`] THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC THEN MRESA_TAC WL_IN_V[`0`;`v`] THEN MRESA_TAC Odxlstcv2.CARD_V_EQ_SCS_K1[`s`;`v`;`V`;`k:num`] THEN POP_ASSUM MP_TAC THEN MRESAL_TAC Nuxcoea.MMS_IMP_BBPRIME[`s:scs_v39`;`v`][LET_DEF;LET_END_DEF;BBprime_v39] THEN MRESA_TAC JKQEWGV1[`s:scs_v39`;`v`] THEN STRIP_TAC THEN DICH_TAC 1 THEN REWRITE_TAC[REAL_ARITH`~(a< b)<=> b<=a`;sol_local] THEN MP_TAC(ARITH_RULE`3 ~(k<=3)/\ 0 b=a+c`] THEN SUBGOAL_THEN`sum ((0..k - 1) DELETE i) (\i. interior_angle1 (vec 0) FF (ITER i (rho_node1 FF) v0)-pi) = &0`ASSUME_TAC ; MATCH_MP_TAC SUM_EQ_0 THEN GEN_TAC THEN STRIP_TAC THEN MP_TAC(ARITH_RULE`3 ~(k<=3)/\ (k+1)-1=k/\ ~(k=0)/\ 1 a=b`] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`3 1<=k`) THEN RESA_TAC THEN MRESA_TAC REAL_OF_NUM_SUB[`1`;`k`] THEN SYM_ASSUM_TAC THEN MATCH_MP_TAC(REAL_ARITH` &0<= interior_angle1 (vec 0) FF (ITER i (rho_node1 FF) v0) ==> pi <= &2 * pi + ((&k - &1) * pi + interior_angle1 (vec 0) FF (ITER i (rho_node1 FF) v0)) - &k * pi`) THEN REWRITE_TAC[interior_angle1;azim] ; MP_TAC(SET_RULE`(!i. i < k ==> azim (vec 0) (v i) (v (SUC i)) (v (i + k - 1)) = pi) \/ ~(!i. i < k ==> azim (vec 0:real^3) (v i) (v (SUC i)) (v (i + k - 1)) = pi)`) THEN RESA_TAC; MP_TAC(SET_RULE`(!i. i < k ==> azim (vec 0) (v i) (v (SUC i)) (v (i + k - 1)) = pi) ==> {i | i < k /\ azim (vec 0) (v i) (v (SUC i)) (v (i + k - 1)) = pi}= {i| i ~(k=0)/\ ~(k=k-2)`) THEN RESA_TAC THEN MRESAL_TAC REP_NUMSEG[`k:num`][CARD_NUMSEG] ; POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[NOT_FORALL_THM;NOT_IMP] THEN REWRITE_TAC[NOT_IMP] THEN STRIP_TAC THEN MP_TAC(SET_RULE`(!j. j < k /\ ~(i=j) ==> azim (vec 0) (v j) (v (SUC j)) (v (j + k - 1)) = pi) \/ ~(!j. j < k /\ ~(i=j) ==> azim (vec 0:real^3) (v j) (v (SUC j)) (v (j + k - 1)) = pi)`) THEN RESA_TAC; SUBGOAL_THEN`{i | i < k /\ azim (vec 0:real^3) (v i) (v (SUC i)) (v (i + k - 1)) = pi} = (0..(k-1)) DELETE i` ASSUME_TAC; REWRITE_TAC[EXTENSION;IN_ELIM_THM;DELETE;IN_NUMSEG] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC; MP_TAC(ARITH_RULE`x 0<=x/\ x<= k-1`) THEN RESA_TAC THEN STRIP_TAC THEN DICH_TAC 3 THEN ASM_REWRITE_TAC[]; MP_TAC(ARITH_RULE`x<=k-1/\ 3 x< k`) THEN RESA_TAC THEN MATCH_DICH_TAC 4 THEN ASM_REWRITE_TAC[]; DICH_TAC (17-12) THEN ASM_REWRITE_TAC[] THEN MRESAL_TAC FINITE_SUBSET[`(0..k - 1) DELETE i`;`(0..k - 1)`][FINITE_NUMSEG;DELETE_SUBSET] THEN SUBGOAL_THEN`i IN 0..(k-1)`ASSUME_TAC ; ASM_REWRITE_TAC[IN_NUMSEG] THEN DICH_TAC (17-13) THEN DICH_TAC 16 THEN ARITH_TAC; MRESAL_TAC CARD_DELETE[`i`;`0..(k-1)`][FINITE_NUMSEG;CARD_NUMSEG] THEN MP_TAC(ARITH_RULE`3 ~(k=0)/\ ~(k-1=k-2)`) THEN RESA_TAC ; POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[NOT_FORALL_THM;NOT_IMP] THEN REWRITE_TAC[NOT_IMP] THEN STRIP_TAC THEN SUBGOAL_THEN`{i | i < k /\ azim (vec 0) (v i) ((v:num->real^3) (SUC i)) (v (i + k - 1)) = pi} SUBSET (0..(k-1)) DELETE i DELETE j`ASSUME_TAC; REWRITE_TAC[SUBSET;DELETE;IN_ELIM_THM;IN_NUMSEG] THEN GEN_TAC THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x 0<=x/\ x<=k-1`) THEN REPEAT RESA_TAC ; DICH_TAC (23-15) THEN DICH_TAC(22-19) THEN ASM_REWRITE_TAC[] ; DICH_TAC (23-18) THEN DICH_TAC(22-19) THEN ASM_REWRITE_TAC[] ; SUBGOAL_THEN`i IN 0..(k-1)`ASSUME_TAC ; ASM_REWRITE_TAC[IN_NUMSEG] THEN DICH_TAC (19-14) THEN DICH_TAC 18 THEN ARITH_TAC; SUBGOAL_THEN`j IN ((0..(k-1)) DELETE i)`ASSUME_TAC ; ASM_REWRITE_TAC[IN_NUMSEG;DELETE;IN_ELIM_THM] THEN DICH_TAC (19-15) THEN DICH_TAC 19 THEN ARITH_TAC; MRESA_TAC FINITE_DELETE[`0..(k-1)`;`i`] THEN MRESA_TAC FINITE_DELETE[`(0..(k-1)) DELETE i`;`j`] THEN MRESAL_TAC CARD_DELETE[`i`;`0..(k-1)`][FINITE_NUMSEG] THEN MRESAL_TAC CARD_DELETE[`j`;`(0..(k-1)) DELETE i`][FINITE_NUMSEG] THEN MRESAL_TAC SUBSET_CARD_EQ[`{i | i < k /\ azim (vec 0) (v i) ((v:num->real^3) (SUC i)) (v (i + k - 1)) = pi}`;`(0..(k-1)) DELETE i DELETE j`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`k-2=k-1-1`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_ELIM_THM;EXTENSION;DELETE;IN_NUMSEG] THEN RESA_TAC; MP_TAC(ARITH_RULE`~(i=j:num)==> i coplanar ({v (i+t1)| t1<=t} UNION {vec 0:real^3, (v:num->real^3) i})`ASSUME_TAC ; INDUCT_TAC ; REWRITE_TAC[ARITH_RULE`t<=0<=> t=0`;] THEN SUBGOAL_THEN`{v (i + t1) | t1 = 0} = {(v:num->real^3) i}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN REWRITE_TAC[ARITH_RULE`a+0=a`] THEN EXISTS_TAC`0` THEN REWRITE_TAC[ARITH_RULE`a+0=a`] ; ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,a}={a,b}`;COPLANAR_2] ; STRIP_TAC THEN MP_TAC(ARITH_RULE`SUC t<= j-i==> t<= j-i`) THEN RESA_TAC THEN DICH_TAC 2 THEN RESA_TAC THEN SUBGOAL_THEN`{v (i + t1) | t1 <= SUC t}= {v (i + t1) | t1 <= t} UNION {(v:num->real^3) (i+ SUC t)}`ASSUME_TAC; REWRITE_TAC[UNION;IN_ELIM_THM;EXTENSION;IN_SING] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC; MP_TAC(ARITH_RULE`t1<= SUC t==> t1<=t\/ t1= SUC t`) THEN RESA_TAC ; MATCH_MP_TAC(SET_RULE`A==>A\/B`) THEN EXISTS_TAC`t1:num` THEN ASM_REWRITE_TAC[] ; EXISTS_TAC`t1:num` THEN DICH_TAC 1 THEN ASM_REWRITE_TAC[] THEN ARITH_TAC; EXISTS_TAC`SUC t` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC ; ASM_REWRITE_TAC[SET_RULE`(a UNION b) UNION c= a UNION b UNION c`] THEN MP_TAC(ARITH_RULE`t=0 \/ 0 t=0`;] THEN SUBGOAL_THEN`{v (i + t1) | t1 = 0} = {(v:num->real^3) i}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN REWRITE_TAC[ARITH_RULE`a+0=a`] THEN EXISTS_TAC`0` THEN REWRITE_TAC[ARITH_RULE`a+0=a`] ; ASM_REWRITE_TAC[SET_RULE`{a} UNION {b} UNION {c,a}={a,b,c}`;Tskajxy_lemmas.KY_COPLANAR_3] ; MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`] THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`] THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC THEN MRESA_TAC WL_IN_V[`i+t-1`;`v`] THEN MRESA_TAC WL_IN_V[`j`;`v`] THEN MRESA_TAC WL_IN_V[`i+t:num`;`v`] THEN MP_TAC(ARITH_RULE`0 ~(i+t-1=i+t) /\ i+t-1real^3`] THEN THAYTHE_TAC 0[`i+t-1`;`i+t:num`] THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`(v:num->real^3) (i+t-1)`;`v j`;`V`] THEN THAYTHEL_TAC 0[`(v:num->real^3) (i+t-1)`;`(v:num->real^3) (i+t)`][SET_RULE`a IN {a,b}`;coplanar] THEN EXISTS_TAC`vec 0:real^3` THEN EXISTS_TAC`(v:num->real^3) (i+t-1)` THEN EXISTS_TAC`(v:num->real^3) (i+t)` THEN ASM_REWRITE_TAC[UNION;SUBSET;IN_ELIM_THM;] THEN REPEAT RESA_TAC; SUBGOAL_THEN`{vec 0, v (i+t-1), v (i + t),v (i + t1)} SUBSET {v (i + t1) | t1 <= t} UNION {vec 0, (v:num->real^3) i}`ASSUME_TAC ; MATCH_MP_TAC(SET_RULE`{b,c,d} SUBSET A==> {a,b,c,d} SUBSET A UNION {a,e}`) THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {b,c,d}<=> a=b\/ a=c\/ a=d`] THEN REPEAT RESA_TAC; EXISTS_TAC`t-1:num` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC; EXISTS_TAC`t:num` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC; EXISTS_TAC`t1:num` THEN ASM_REWRITE_TAC[] ; MRESA_TAC COPLANAR_SUBSET[`{vec 0, v (i+t-1), v (i + t), v (i + t1:num)}`;`{v (i + t1) | t1 <= t:num} UNION {vec 0, v i}`] THEN MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,C,D,A}`] THEN ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_SING] THEN RESA_TAC THEN MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,D,A,C}`] THEN MATCH_MP_TAC AZIM_EQ_0_PI_IMP_COPLANAR THEN MATCH_MP_TAC(SET_RULE`A==> B \/ A`); MP_TAC(ARITH_RULE`0SUC (i + t)= i+ SUC t/\ 0<= i+t/\ i+t<=k-1/\ ~(i + t = i)/\ ~(i+t=j)/\ (i + t) + k - 1= (i + t - 1)+k`) THEN RESA_TAC THEN THAYTHE_TAC (51-26)[`i+t:num`] THEN ASM_TAC THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;periodic] THEN REPEAT RESA_TAC THEN POP_ASSUM MP_TAC THEN THAYTHE_TAC (53-33)[`i+t-1`]; POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`] THEN RESA_TAC; REWRITE_TAC[Collect_geom2.THREE_GEN_POINTS_IN_AFF3;GSYM aff] ; MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull THEN ASM_REWRITE_TAC[] ; SUBGOAL_THEN`{vec 0, v (i+t-1), v (i + t),v (i)} SUBSET {v (i + t1) | t1 <= t} UNION {vec 0, (v:num->real^3) i}`ASSUME_TAC ; MATCH_MP_TAC(SET_RULE`{b,c,d} SUBSET A==> {a,b,c,d} SUBSET A UNION {a,e}`) THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {b,c,d}<=> a=b\/ a=c\/ a=d`] THEN REPEAT RESA_TAC; EXISTS_TAC`t-1:num` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC; EXISTS_TAC`t:num` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC; EXISTS_TAC`0:num` THEN ASM_REWRITE_TAC[ARITH_RULE`0<=t/\ i+0=i`] ; MRESA_TAC COPLANAR_SUBSET[`{vec 0, v (i+t-1), v (i + t), v (i:num)}`;`{v (i + t1) | t1 <= t:num} UNION {vec 0, v i}`] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,C,D,A}`] THEN ASM_REWRITE_TAC[]; SUBGOAL_THEN`!t. t <= i+k-j ==> coplanar ({v (i+k - t1) | t1 <= t} UNION {vec 0, (v:num->real^3) i})`ASSUME_TAC ; INDUCT_TAC ; REWRITE_TAC[ARITH_RULE`t<=0<=> t=0`;] THEN SUBGOAL_THEN`{v (i+k - t1) | t1 = 0} = {(v:num->real^3) i}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN REWRITE_TAC[ARITH_RULE`a-0=a`] ; ASM_TAC THEN REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;BBs_v39;LET_DEF;LET_END_DEF;periodic] THEN REPEAT RESA_TAC THEN THAYTHE_TAC (41-4)[`i:num`] ; EXISTS_TAC`0` THEN REWRITE_TAC[ARITH_RULE`a-0=a`] THEN ASM_TAC THEN REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;BBs_v39;LET_DEF;LET_END_DEF;periodic] THEN REPEAT RESA_TAC THEN THAYTHE_TAC (40-4)[`i:num`] ; ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}= {a,b,c}`;Tskajxy_lemmas.KY_COPLANAR_3] ; STRIP_TAC THEN MP_TAC(ARITH_RULE`SUC t<= i+k-j==> t<= i+k-j`) THEN RESA_TAC THEN DICH_TAC 2 THEN RESA_TAC ; MP_TAC(ARITH_RULE`t=0\/ 0real^3) (i + k - t1) | t1 <= SUC 0} ={v i, v(i+k-1)}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;ARITH_RULE`t<= SUC 0<=> t=0\/ t=1`;IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC; ASM_TAC THEN REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;BBs_v39;LET_DEF;LET_END_DEF;periodic;ARITH_RULE`a- 0=a`] THEN REPEAT RESA_TAC THEN THAYTHE_TAC (45-4)[`i:num`] THEN SET_TAC[]; SET_TAC[] ; POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`] THEN RESA_TAC ; EXISTS_TAC`0` THEN REWRITE_TAC[ARITH_RULE`a-0=a`] THEN ASM_TAC THEN REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;BBs_v39;LET_DEF;LET_END_DEF;periodic;ARITH_RULE`a- 0=a`] THEN REPEAT RESA_TAC THEN THAYTHE_TAC (44-4)[`i:num`] ; EXISTS_TAC`1` THEN ASM_REWRITE_TAC[] ; ASM_REWRITE_TAC[SET_RULE`{a,b} UNION {c,a}={a,b,c}`;Tskajxy_lemmas.KY_COPLANAR_3] ; REWRITE_TAC[coplanar] THEN EXISTS_TAC`vec 0:real^3` THEN EXISTS_TAC`(v:num->real^3) (i+k-t+1)` THEN EXISTS_TAC`(v:num->real^3) (i+k-t)` THEN ASM_REWRITE_TAC[UNION;SUBSET;IN_ELIM_THM;] THEN REPEAT RESA_TAC ; MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull THEN ASM_REWRITE_TAC[] ; MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`] THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`] THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC THEN MRESA_TAC WL_IN_V[`i+k-t+1`;`v`] THEN MRESA_TAC WL_IN_V[`i+k-t:num`;`v`] THEN MP_TAC(ARITH_RULE`3 1real^3`;`(i + k - t+1):num`] THEN DICH_TAC 0 THEN ASM_SIMP_TAC[MOD_REFL] THEN RESA_TAC THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i + k - t) MOD k`;`v:num->real^3`;`(i + k - t):num`] THEN DICH_TAC 0 THEN ASM_SIMP_TAC[MOD_REFL] THEN RESA_TAC THEN MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`v:num->real^3`] THEN THAYTHE_TAC 0[`(i+k- t+1) MOD k`;`(i+k-t:num) MOD k`] THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`(v:num->real^3) (i+k- t+1)`;`v (i+k-t:num)`;`V`] THEN THAYTHEL_TAC 0[`v(i+k- t+1)`;`v(i+k-t:num)`][SET_RULE`a IN {a,b}`;] ; MP_TAC(ARITH_RULE`t1<= SUC t==> t1<= t\/ t1= SUC t`) THEN RESA_TAC ; SUBGOAL_THEN`{vec 0, v (i+k-t+1), v (i+k-t),v (i+k-t1)} SUBSET {v (i+k- t1) | t1 <= t} UNION {vec 0, (v:num->real^3) i}`ASSUME_TAC ; MATCH_MP_TAC(SET_RULE`{b,c,d} SUBSET A==> {a,b,c,d} SUBSET A UNION {a,e}`) THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {b,c,d}<=> a=b\/ a=c\/ a=d`] THEN REPEAT RESA_TAC; EXISTS_TAC`t-1:num` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC ; DICH_TAC (53-32) THEN ARITH_TAC; MP_TAC(ARITH_RULE`0 1<=t/\i+k-t+1=i+(k+1)-t`) THEN RESA_TAC THEN MRESA_TAC Ssrnat.subn_subA[`k:num`;`t:num`;`1`] ; EXISTS_TAC`t:num` THEN ASM_REWRITE_TAC[ARITH_RULE`a<=a:num`] ; EXISTS_TAC`t1:num` THEN ASM_REWRITE_TAC[] ; MRESA_TAC COPLANAR_SUBSET[`{vec 0, v (i + k - t + 1), v (i + k - t), v (i + k - t1)}`;`{v (i + k-t1) | t1 <= t:num} UNION {vec 0, v i}`] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,C,D,A}`] THEN ASM_REWRITE_TAC[]; ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,D,C,A}`] THEN MATCH_MP_TAC AZIM_EQ_0_PI_IMP_COPLANAR THEN MATCH_MP_TAC(SET_RULE`A==> B \/ A`); THAYTHEL_TAC (53-26)[`(i+k-t) MOD k`][ARITH_RULE`0<=a`] THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`(i + k - t) MOD k < k/\ 3 (i + k - t) MOD k <= k - 1/\ 0 (j + k - t) + t= j + k - t + t/\ t<=k/\ (j + k - t) + i + k - j= (i + k - t) + k - j+j/\ j<=k/\ treal^3`;`SUC ((i + k - t) MOD k) MOD k`] THEN DICH_TAC 0 THEN ASM_SIMP_TAC[MOD_REFL;Hypermap.lemma_suc_mod] THEN RESA_TAC THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i + k - t) MOD k + k - 1:num`;`v:num->real^3`;`((i + k - t) MOD k + k - 1) MOD k`] THEN DICH_TAC 0 THEN ASM_SIMP_TAC[MOD_REFL;Hypermap.lemma_suc_mod] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`3 k-1real^3`;`(i + k - (t + 1))`] THEN DICH_TAC 0 THEN ASM_SIMP_TAC[MOD_REFL;Hypermap.lemma_suc_mod] THEN RESA_TAC ; POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`] THEN RESA_TAC; REWRITE_TAC[Collect_geom2.THREE_GEN_POINTS_IN_AFF3;GSYM aff] ; MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull THEN ASM_REWRITE_TAC[] ; MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`] THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`] THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC THEN MRESA_TAC WL_IN_V[`i+k-t+1`;`v`] THEN MRESA_TAC WL_IN_V[`i+k-t:num`;`v`] THEN MP_TAC(ARITH_RULE`3 1real^3`;`(i + k - t+1):num`] THEN DICH_TAC 0 THEN ASM_SIMP_TAC[MOD_REFL] THEN RESA_TAC THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(i + k - t) MOD k`;`v:num->real^3`;`(i + k - t):num`] THEN DICH_TAC 0 THEN ASM_SIMP_TAC[MOD_REFL] THEN RESA_TAC THEN MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`v:num->real^3`] THEN THAYTHE_TAC 0[`(i+k- t+1) MOD k`;`(i+k-t:num) MOD k`] THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`(v:num->real^3) (i+k- t+1)`;`v (i+k-t:num)`;`V`] THEN THAYTHEL_TAC 0[`v(i+k- t+1)`;`v(i+k-t:num)`][SET_RULE`a IN {a,b}`;] ; SUBGOAL_THEN`{vec 0, v (i + k - t + 1), v (i + k - t),v (i)} SUBSET {v (i+k- t1) | t1 <= t} UNION {vec 0, (v:num->real^3) i}`ASSUME_TAC ; MATCH_MP_TAC(SET_RULE`{b,c} SUBSET A==> {a,b,c,e} SUBSET A UNION {a,e}`) THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {b,c}<=> a=b\/ a=c`] THEN REPEAT RESA_TAC; EXISTS_TAC`t-1:num` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC ; DICH_TAC (52-32) THEN ARITH_TAC; MP_TAC(ARITH_RULE`0 1<=t/\i+k-t+1=i+(k+1)-t`) THEN RESA_TAC THEN MRESA_TAC Ssrnat.subn_subA[`k:num`;`t:num`;`1`] ; EXISTS_TAC`t:num` THEN ASM_REWRITE_TAC[ARITH_RULE`a<=a:num`] ; MRESA_TAC COPLANAR_SUBSET[`{vec 0:real^3, v (i + k - t + 1), v (i + k - t), v i}`;`{(v:num->real^3) (i + k - t1) | t1 <= t} UNION {vec 0:real^3, v i}`] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,C,D,A}`] THEN ASM_REWRITE_TAC[]; MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`] THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`] THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC WL_IN_V[`i`;`v`] THEN MRESA_TAC WL_IN_V[`j:num`;`v`] THEN MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`v:num->real^3`] THEN THAYTHE_TAC 0[`i`;`j`] THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`(v:num->real^3) (i)`;`v (j:num)`;`V`] THEN THAYTHEL_TAC 0[`v i`;`v j`][SET_RULE`a IN {a, b}`] THEN SUBGOAL_THEN `coplanar ({vec 0} UNION {(v:num->real^3) (i+t)| treal^3) i` THEN EXISTS_TAC`(v:num->real^3) j` THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;UNION;IN_SING] THEN REPEAT RESA_TAC; REWRITE_TAC[Collect_geom2.THREE_GEN_POINTS_IN_AFF3;GSYM aff] ; MP_TAC(ARITH_RULE`t<=j-i\/ j-i<=t:num`) THEN RESA_TAC ; MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull THEN ASM_REWRITE_TAC[] THEN THAYTHEL_TAC (39-28)[`j-i:num`][ARITH_RULE`j-i<=j-i:num`] THEN MATCH_MP_TAC COPLANAR_SUBSET THEN EXISTS_TAC`({v (i + t1) | t1 | t1 <= j - i} UNION {vec 0, (v:num->real^3) i})` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(SET_RULE`a IN A/\ d IN A==>{a,b,c,d} SUBSET A UNION {b,c}`) THEN STRIP_TAC THEN REWRITE_TAC[IN_ELIM_THM] ; EXISTS_TAC`t:num` THEN ASM_REWRITE_TAC[]; EXISTS_TAC`j-i:num` THEN ASM_REWRITE_TAC[ARITH_RULE`j-i<=j-i:num/\ i+j-i=j-i+i`] THEN MP_TAC(ARITH_RULE`i i<=j:num`) THEN RESA_TAC THEN MRESA_TAC SUB_ADD[`j`;`i`]; MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull THEN ASM_REWRITE_TAC[] THEN THAYTHEL_TAC (39-29)[`i+k-j:num`][ARITH_RULE`i+k-j<=i+k-j:num`] THEN MATCH_MP_TAC COPLANAR_SUBSET THEN EXISTS_TAC`({v (i + k - t1) | t1 | t1 <= i + k - j} UNION {vec 0, (v:num->real^3) i})` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(SET_RULE`a IN A/\ d IN A==>{a,b,c,d} SUBSET A UNION {b,c}`) THEN STRIP_TAC THEN REWRITE_TAC[IN_ELIM_THM] ; EXISTS_TAC`k-t:num` THEN ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`t t<=k:num/\ k-t<= i+k-j`) THEN RESA_TAC THEN MRESA_TAC Ssrnat.subKn[`t`;`k`] ; EXISTS_TAC`i+k-j:num` THEN ASM_REWRITE_TAC[ARITH_RULE`i + k - j<=i + k - j:num/\ i+j-i=j-i+i`] THEN MP_TAC(ARITH_RULE`i i<=j:num/\ (i+k)-j= i+k-j/\ j<=i+k /\ (i + k) - (i + k - j)= i + k - (i + k - j)`) THEN RESA_TAC THEN MRESA_TAC Ssrnat.subKn[`j:num`;`i+k:num`] ; POP_ASSUM MP_TAC THEN MRESA_TAC BB_TRANS_SUBSET_BB[`s`;`v`;`i`] THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`3 ~(k<=3)/\ ~(k=0)`) THEN RESA_TAC THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;dsv_v39;scs_slice_v39;PAIR_EQ;scs_half_slice_v39] THEN RESA_TAC THEN ASM_SIMP_TAC[PERIODIC_IMAGE2] THEN MRESA_TAC TRANS_V[`s`;`i`;`v`] THEN MRESAL_TAC FEKTYIY[`s`;`v`][IN] ; (****************j coplanar ({v (j+t1)| t1<=t} UNION {vec 0:real^3, (v:num->real^3) j})`ASSUME_TAC ; INDUCT_TAC ; REWRITE_TAC[ARITH_RULE`t<=0<=> t=0`;] THEN SUBGOAL_THEN`{v (j + t1) | t1 = 0} = {(v:num->real^3) j}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN REWRITE_TAC[ARITH_RULE`a+0=a`] THEN EXISTS_TAC`0` THEN REWRITE_TAC[ARITH_RULE`a+0=a`] ; ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,a}={a,b}`;COPLANAR_2] ; STRIP_TAC THEN MP_TAC(ARITH_RULE`SUC t<= i-j==> t<= i-j`) THEN RESA_TAC THEN DICH_TAC 2 THEN RESA_TAC THEN SUBGOAL_THEN`{v (j + t1) | t1 <= SUC t}= {v (j + t1) | t1 <= t} UNION {(v:num->real^3) (j+ SUC t)}`ASSUME_TAC; REWRITE_TAC[UNION;IN_ELIM_THM;EXTENSION;IN_SING] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC; MP_TAC(ARITH_RULE`t1<= SUC t==> t1<=t\/ t1= SUC t`) THEN RESA_TAC ; MATCH_MP_TAC(SET_RULE`A==>A\/B`) THEN EXISTS_TAC`t1:num` THEN ASM_REWRITE_TAC[] ; EXISTS_TAC`t1:num` THEN DICH_TAC 1 THEN ASM_REWRITE_TAC[] THEN ARITH_TAC; EXISTS_TAC`SUC t` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC ; ASM_REWRITE_TAC[SET_RULE`(a UNION b) UNION c= a UNION b UNION c`] THEN MP_TAC(ARITH_RULE`t=0 \/ 0 t=0`;] THEN SUBGOAL_THEN`{v (j + t1) | t1 = 0} = {(v:num->real^3) j}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN REWRITE_TAC[ARITH_RULE`a+0=a`] THEN EXISTS_TAC`0` THEN REWRITE_TAC[ARITH_RULE`a+0=a`] ; ASM_REWRITE_TAC[SET_RULE`{a} UNION {b} UNION {c,a}={a,b,c}`;Tskajxy_lemmas.KY_COPLANAR_3] ; MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`] THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`] THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC THEN MRESA_TAC WL_IN_V[`j+t-1`;`v`] THEN MRESA_TAC WL_IN_V[`i`;`v`] THEN MRESA_TAC WL_IN_V[`j+t:num`;`v`] THEN MP_TAC(ARITH_RULE`0 ~(j+t-1=j+t) /\ j+t-1real^3`] THEN THAYTHE_TAC 0[`j+t-1`;`j+t:num`] THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`(v:num->real^3) (j+t-1)`;`v i`;`V`] THEN THAYTHEL_TAC 0[`(v:num->real^3) (j+t-1)`;`(v:num->real^3) (j+t)`][SET_RULE`a IN {a,b}`;coplanar] THEN EXISTS_TAC`vec 0:real^3` THEN EXISTS_TAC`(v:num->real^3) (j+t-1)` THEN EXISTS_TAC`(v:num->real^3) (j+t)` THEN ASM_REWRITE_TAC[UNION;SUBSET;IN_ELIM_THM;] THEN REPEAT RESA_TAC; SUBGOAL_THEN`{vec 0, v (j+t-1), v (j + t),v (j + t1)} SUBSET {v (j + t1) | t1 <= t} UNION {vec 0, (v:num->real^3) j}`ASSUME_TAC ; MATCH_MP_TAC(SET_RULE`{b,c,d} SUBSET A==> {a,b,c,d} SUBSET A UNION {a,e}`) THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {b,c,d}<=> a=b\/ a=c\/ a=d`] THEN REPEAT RESA_TAC; EXISTS_TAC`t-1:num` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC; EXISTS_TAC`t:num` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC; EXISTS_TAC`t1:num` THEN ASM_REWRITE_TAC[] ; MRESA_TAC COPLANAR_SUBSET[`{vec 0, v (j+t-1), v (j + t), v (j + t1:num)}`;`{v (j + t1) | t1 <= t:num} UNION {vec 0, v j}`] THEN MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,C,D,A}`] THEN ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_SING] THEN RESA_TAC THEN MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,D,A,C}`] THEN MATCH_MP_TAC AZIM_EQ_0_PI_IMP_COPLANAR THEN MATCH_MP_TAC(SET_RULE`A==> B \/ A`); MP_TAC(ARITH_RULE`0SUC (j + t)= j+ SUC t/\ 0<= j+t/\ j+t<=k-1/\ ~(j + t = j)/\ ~(j+t=i)/\ (j + t) + k - 1= (j + t - 1)+k`) THEN RESA_TAC THEN THAYTHE_TAC (51-26)[`j+t:num`] THEN ASM_TAC THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;periodic] THEN REPEAT RESA_TAC THEN POP_ASSUM MP_TAC THEN THAYTHE_TAC (53-33)[`j+t-1`]; POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`] THEN RESA_TAC; REWRITE_TAC[Collect_geom2.THREE_GEN_POINTS_IN_AFF3;GSYM aff] ; MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull THEN ASM_REWRITE_TAC[] ; SUBGOAL_THEN`{vec 0, v (j+t-1), v (j + t),v (j)} SUBSET {v (j + t1) | t1 <= t} UNION {vec 0, (v:num->real^3) j}`ASSUME_TAC ; MATCH_MP_TAC(SET_RULE`{b,c,d} SUBSET A==> {a,b,c,d} SUBSET A UNION {a,e}`) THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {b,c,d}<=> a=b\/ a=c\/ a=d`] THEN REPEAT RESA_TAC; EXISTS_TAC`t-1:num` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC; EXISTS_TAC`t:num` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC; EXISTS_TAC`0:num` THEN ASM_REWRITE_TAC[ARITH_RULE`0<=t/\ i+0=i`] ; MRESA_TAC COPLANAR_SUBSET[`{vec 0, v (j+t-1), v (j + t), v (j:num)}`;`{v (j + t1) | t1 <= t:num} UNION {vec 0, v j}`] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,C,D,A}`] THEN ASM_REWRITE_TAC[]; SUBGOAL_THEN`!t. t <= j+k-i ==> coplanar ({v (j+k - t1) | t1 <= t} UNION {vec 0, (v:num->real^3) j})`ASSUME_TAC ; INDUCT_TAC ; REWRITE_TAC[ARITH_RULE`t<=0<=> t=0`;] THEN SUBGOAL_THEN`{v (j+k - t1) | t1 = 0} = {(v:num->real^3) j}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN REWRITE_TAC[ARITH_RULE`a-0=a`] ; ASM_TAC THEN REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;BBs_v39;LET_DEF;LET_END_DEF;periodic] THEN REPEAT RESA_TAC THEN THAYTHE_TAC (41-4)[`j:num`] ; EXISTS_TAC`0` THEN REWRITE_TAC[ARITH_RULE`a-0=a`] THEN ASM_TAC THEN REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;BBs_v39;LET_DEF;LET_END_DEF;periodic] THEN REPEAT RESA_TAC THEN THAYTHE_TAC (40-4)[`j:num`] ; ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}= {a,b,c}`;Tskajxy_lemmas.KY_COPLANAR_3] ; STRIP_TAC THEN MP_TAC(ARITH_RULE`SUC t<= j+k-i==> t<= j+k-i`) THEN RESA_TAC THEN DICH_TAC 2 THEN RESA_TAC ; MP_TAC(ARITH_RULE`t=0\/ 0real^3) (j + k - t1) | t1 <= SUC 0} ={v j, v(j+k-1)}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;ARITH_RULE`t<= SUC 0<=> t=0\/ t=1`;IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC; ASM_TAC THEN REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;BBs_v39;LET_DEF;LET_END_DEF;periodic;ARITH_RULE`a- 0=a`] THEN REPEAT RESA_TAC THEN THAYTHE_TAC (45-4)[`j:num`] THEN SET_TAC[]; SET_TAC[] ; POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`] THEN RESA_TAC ; EXISTS_TAC`0` THEN REWRITE_TAC[ARITH_RULE`a-0=a`] THEN ASM_TAC THEN REWRITE_TAC[MMs_v39;BBprime_v39;BBprime2_v39;BBs_v39;LET_DEF;LET_END_DEF;periodic;ARITH_RULE`a- 0=a`] THEN REPEAT RESA_TAC THEN THAYTHE_TAC (44-4)[`j:num`] ; EXISTS_TAC`1` THEN ASM_REWRITE_TAC[] ; ASM_REWRITE_TAC[SET_RULE`{a,b} UNION {c,a}={a,b,c}`;Tskajxy_lemmas.KY_COPLANAR_3] ; REWRITE_TAC[coplanar] THEN EXISTS_TAC`vec 0:real^3` THEN EXISTS_TAC`(v:num->real^3) (j+k-t+1)` THEN EXISTS_TAC`(v:num->real^3) (j+k-t)` THEN ASM_REWRITE_TAC[UNION;SUBSET;IN_ELIM_THM;] THEN REPEAT RESA_TAC ; MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull THEN ASM_REWRITE_TAC[] ; MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`] THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`] THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC THEN MRESA_TAC WL_IN_V[`j+k-t+1`;`v`] THEN MRESA_TAC WL_IN_V[`j+k-t:num`;`v`] THEN MP_TAC(ARITH_RULE`3 1real^3`;`(j + k - t+1):num`] THEN DICH_TAC 0 THEN ASM_SIMP_TAC[MOD_REFL] THEN RESA_TAC THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(j + k - t) MOD k`;`v:num->real^3`;`(j + k - t):num`] THEN DICH_TAC 0 THEN ASM_SIMP_TAC[MOD_REFL] THEN RESA_TAC THEN MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`v:num->real^3`] THEN THAYTHE_TAC 0[`(j+k- t+1) MOD k`;`(j+k-t:num) MOD k`] THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`(v:num->real^3) (j+k- t+1)`;`v (j+k-t:num)`;`V`] THEN THAYTHEL_TAC 0[`v(j+k- t+1)`;`v(j+k-t:num)`][SET_RULE`a IN {a,b}`;] ; MP_TAC(ARITH_RULE`t1<= SUC t==> t1<= t\/ t1= SUC t`) THEN RESA_TAC ; SUBGOAL_THEN`{vec 0, v (j+k-t+1), v (j+k-t),v (j+k-t1)} SUBSET {v (j+k- t1) | t1 <= t} UNION {vec 0, (v:num->real^3) j}`ASSUME_TAC ; MATCH_MP_TAC(SET_RULE`{b,c,d} SUBSET A==> {a,b,c,d} SUBSET A UNION {a,e}`) THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {b,c,d}<=> a=b\/ a=c\/ a=d`] THEN REPEAT RESA_TAC; EXISTS_TAC`t-1:num` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC ; DICH_TAC (53-32) THEN ARITH_TAC; MP_TAC(ARITH_RULE`0 1<=t/\j+k-t+1=j+(k+1)-t`) THEN RESA_TAC THEN MRESA_TAC Ssrnat.subn_subA[`k:num`;`t:num`;`1`] ; EXISTS_TAC`t:num` THEN ASM_REWRITE_TAC[ARITH_RULE`a<=a:num`] ; EXISTS_TAC`t1:num` THEN ASM_REWRITE_TAC[] ; MRESA_TAC COPLANAR_SUBSET[`{vec 0, v (j + k - t + 1), v (j + k - t), v (j + k - t1)}`;`{v (j + k-t1) | t1 <= t:num} UNION {vec 0, v j}`] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,C,D,A}`] THEN ASM_REWRITE_TAC[]; ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,D,C,A}`] THEN MATCH_MP_TAC AZIM_EQ_0_PI_IMP_COPLANAR THEN MATCH_MP_TAC(SET_RULE`A==> B \/ A`); THAYTHEL_TAC (53-26)[`(j+k-t) MOD k`][ARITH_RULE`0<=a`] THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`(j + k - t) MOD k < k/\ 3 (j + k - t) MOD k <= k - 1/\ 0 (i + k - t) + t= i + k - t + t/\ t<=k/\ (i + k - t) + j + k - i= (j + k - t) + k - i+i/\ i<=k/\ treal^3`;`SUC ((j + k - t) MOD k) MOD k`] THEN DICH_TAC 0 THEN ASM_SIMP_TAC[MOD_REFL;Hypermap.lemma_suc_mod] THEN RESA_TAC THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(j + k - t) MOD k + k - 1:num`;`v:num->real^3`;`((j + k - t) MOD k + k - 1) MOD k`] THEN DICH_TAC 0 THEN ASM_SIMP_TAC[MOD_REFL;Hypermap.lemma_suc_mod] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`3 k-1real^3`;`(j + k - (t + 1))`] THEN DICH_TAC 0 THEN ASM_SIMP_TAC[MOD_REFL;Hypermap.lemma_suc_mod] THEN RESA_TAC ; POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`] THEN RESA_TAC; REWRITE_TAC[Collect_geom2.THREE_GEN_POINTS_IN_AFF3;GSYM aff] ; MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull THEN ASM_REWRITE_TAC[] ; MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`] THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`] THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC THEN MRESA_TAC WL_IN_V[`j+k-t+1`;`v`] THEN MRESA_TAC WL_IN_V[`j+k-t:num`;`v`] THEN MP_TAC(ARITH_RULE`3 1real^3`;`(j + k - t+1):num`] THEN DICH_TAC 0 THEN ASM_SIMP_TAC[MOD_REFL] THEN RESA_TAC THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(j + k - t) MOD k`;`v:num->real^3`;`(j + k - t):num`] THEN DICH_TAC 0 THEN ASM_SIMP_TAC[MOD_REFL] THEN RESA_TAC THEN MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`v:num->real^3`] THEN THAYTHE_TAC 0[`(j+k- t+1) MOD k`;`(j+k-t:num) MOD k`] THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`(v:num->real^3) (j+k- t+1)`;`v (j+k-t:num)`;`V`] THEN THAYTHEL_TAC 0[`v(j+k- t+1)`;`v(j+k-t:num)`][SET_RULE`a IN {a,b}`;] ; SUBGOAL_THEN`{vec 0, v (j + k - t + 1), v (j + k - t),v (j)} SUBSET {v (j+k- t1) | t1 <= t} UNION {vec 0, (v:num->real^3) j}`ASSUME_TAC ; MATCH_MP_TAC(SET_RULE`{b,c} SUBSET A==> {a,b,c,e} SUBSET A UNION {a,e}`) THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;SET_RULE`a IN {b,c}<=> a=b\/ a=c`] THEN REPEAT RESA_TAC; EXISTS_TAC`t-1:num` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC ; DICH_TAC (52-32) THEN ARITH_TAC; MP_TAC(ARITH_RULE`0 1<=t/\j+k-t+1=j+(k+1)-t`) THEN RESA_TAC THEN MRESA_TAC Ssrnat.subn_subA[`k:num`;`t:num`;`1`] ; EXISTS_TAC`t:num` THEN ASM_REWRITE_TAC[ARITH_RULE`a<=a:num`] ; MRESA_TAC COPLANAR_SUBSET[`{vec 0:real^3, v (j + k - t + 1), v (j + k - t), v j}`;`{(v:num->real^3) (j + k - t1) | t1 <= t} UNION {vec 0:real^3, v j}`] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={B,C,D,A}`] THEN ASM_REWRITE_TAC[]; MRESA_TAC Nuxcoea.MMS_IMP_BBS[`s:scs_v39`;`v`] THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`] THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC WL_IN_V[`j`;`v`] THEN MRESA_TAC WL_IN_V[`i:num`;`v`] THEN MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`v:num->real^3`] THEN THAYTHE_TAC 0[`j`;`i`] THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`(v:num->real^3) (j)`;`v (i:num)`;`V`] THEN THAYTHEL_TAC 0[`v j`;`v i`][SET_RULE`a IN {a, b}`] THEN SUBGOAL_THEN `coplanar ({vec 0} UNION {(v:num->real^3) (j+t)| treal^3) j` THEN EXISTS_TAC`(v:num->real^3) i` THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;UNION;IN_SING] THEN REPEAT RESA_TAC; REWRITE_TAC[Collect_geom2.THREE_GEN_POINTS_IN_AFF3;GSYM aff] ; MP_TAC(ARITH_RULE`t<=i-j\/ i-j<=t:num`) THEN RESA_TAC ; MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull THEN ASM_REWRITE_TAC[] THEN THAYTHEL_TAC (39-28)[`i-j:num`][ARITH_RULE`i-j<=i-j:num`] THEN MATCH_MP_TAC COPLANAR_SUBSET THEN EXISTS_TAC`({v (j + t1) | t1 | t1 <= i - j} UNION {vec 0, (v:num->real^3) j})` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(SET_RULE`a IN A/\ d IN A==>{a,b,c,d} SUBSET A UNION {b,c}`) THEN STRIP_TAC THEN REWRITE_TAC[IN_ELIM_THM] ; EXISTS_TAC`t:num` THEN ASM_REWRITE_TAC[]; EXISTS_TAC`i-j:num` THEN ASM_REWRITE_TAC[ARITH_RULE`j-i<=j-i:num/\ i+j-i=j-i+i`] THEN MP_TAC(ARITH_RULE`j j<=i:num`) THEN RESA_TAC THEN MRESA_TAC SUB_ADD[`i`;`j`]; MATCH_MP_TAC Zlzthic.coplanar_in_affine_hull THEN ASM_REWRITE_TAC[] THEN THAYTHEL_TAC (39-29)[`j+k-i:num`][ARITH_RULE`i+k-j<=i+k-j:num`] THEN MATCH_MP_TAC COPLANAR_SUBSET THEN EXISTS_TAC`({v (j + k - t1) | t1 | t1 <= j + k - i} UNION {vec 0, (v:num->real^3) j})` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(SET_RULE`a IN A/\ d IN A==>{a,b,c,d} SUBSET A UNION {b,c}`) THEN STRIP_TAC THEN REWRITE_TAC[IN_ELIM_THM] ; EXISTS_TAC`k-t:num` THEN ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`t t<=k:num/\ k-t<= j+k-i`) THEN RESA_TAC THEN MRESA_TAC Ssrnat.subKn[`t`;`k`] ; EXISTS_TAC`j+k-i:num` THEN ASM_REWRITE_TAC[ARITH_RULE`i + k - j<=i + k - j:num/\ i+j-i=j-i+i`] THEN MP_TAC(ARITH_RULE`j j<=i:num/\ (j+k)-i= j+k-i/\ i<=j+k /\ (j + k) - (j + k - i)= j + k - (j + k - i)`) THEN RESA_TAC THEN MRESA_TAC Ssrnat.subKn[`i:num`;`j+k:num`] ; POP_ASSUM MP_TAC THEN MRESA_TAC BB_TRANS_SUBSET_BB[`s`;`v`;`j`] THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`3 ~(k<=3)/\ ~(k=0)`) THEN RESA_TAC THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_prop_equ_v39;MMs_v39; BBprime2_v39;BBprime_v39;BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39;scs_diag;scs_v39_explicit;is_scs_slice_v39;dsv_v39;scs_slice_v39;PAIR_EQ;scs_half_slice_v39] THEN RESA_TAC THEN ASM_SIMP_TAC[PERIODIC_IMAGE2] THEN MRESA_TAC TRANS_V[`s`;`j`;`v`] THEN MRESAL_TAC FEKTYIY[`s`;`v`][IN] ; ]);; end;; (* let check_completeness_claimA_concl = Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) *)