(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Chapter: Local Fan *) (* Author: Hoang Le Truong *) (* Date: 2012-04-01 *) (* ========================================================================= *) (* remaining conclusions from appendix to Local Fan chapter *) module Ardbzye = 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 Aursipd;; open Cuxvzoz;; open Rrcwnsj;; open Tfitskc;; open Hexagons;; open Otmtotj;; open Hijqaha;; open Cnicgsf;; let GSXRFWM1= prove_by_refinement(`!s v. is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\ (!i. scs_b_v39 s i (i+1) <= cstab) ==> scs_generic v`, [ REWRITE_TAC[IN;GSYM ADD1] THEN 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 REPEAT RESA_TAC THEN ASSUME_TAC(ARITH_RULE`3<4`) THEN MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39] THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic] 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 MP_TAC Wrgcvdr_cizmrrh.CIZMRRH THEN RESA_TAC THEN MRESA_TAC LUNAR_IN_V[`E`;`v'`;`w`;`V`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN EXPAND_TAC "V" THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN REPEAT RESA_TAC ; DICH_TAC(21-17) THEN DICH_TAC(20-16) THEN RESA_TAC THEN ASSUME_TAC(ARITH_RULE`3<6/\ ~(4<=3)`) THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v x`;`v`;`x`] 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 x'`;`V`;`FF`;`v x`] THEN MP_TAC(ARITH_RULE`i+1<4/\ ~(i=0)/\ ~(i=1)==> i=2`) THEN RESA_TAC; MP_TAC Axjrpnc.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[`x`;`v`] THEN MRESA_TAC Localization.LOFA_IMP_LT_CARD_SET_V_ALT[`V`;`E`;`FF`;`v x`] 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+x:num`;`s`] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`n+x: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+x)`] THEN MP_TAC(ARITH_RULE`n<4==> n=0\/ n=1\/ n=2\/ n=3`) THEN RESA_TAC; POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`0+a=a`] THEN REPEAT RESA_TAC) THEN DICH_TAC (37-31) THEN RESA_TAC THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`x`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC x`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC x)`] THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`x`] THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC x`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v x`;`v (SUC x)`;`&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 Axjrpnc.NORM_V_IN_BB_LE_CSTAB THEN RESA_TAC THEN THAYTHE_TAC 0[`SUC x`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC x)`;`v (SUC(SUC x))`;`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 (x)) (v (SUC (x))) <= arclength (&2) (&2) (&2 * h0) /\ arcV (vec 0) ((v:num->real^3) (SUC (x))) (v (SUC (SUC (x)))) <= arclength (&2) (&2) (cstab) /\ arclength (&2) (&2) (&2 * h0) + arclength (&2) (&2) (cstab) < pi ==>arcV (vec 0) (v ((x))) (v ((SUC (x))))+ arcV (vec 0) (v (SUC (x))) (v (SUC (SUC (x)))) < pi`) THEN ASM_SIMP_TAC[Axjrpnc.arclength_2h0_cstab] THEN STRIP_TAC THEN MRESA_TAC WL_IN_FF[`(x)`;`v`] THEN MRESA_TAC WL_IN_FF[`SUC (x)`;`v`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (x), v (SUC (x))`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (x)), v (SUC (SUC (x)))`] THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (x)`;`v (SUC(SUC (x)))`;`v (SUC (x))`] 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 MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v x`;`v(x')`] THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v x, v (2+x)}`] ; POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`1+a=SUC a`] THEN REPEAT RESA_TAC) THEN DICH_TAC (37-31) THEN RESA_TAC THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`x`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC x`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC x)`] THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`x`] THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC x`] THEN MP_TAC Axjrpnc.NORM_V_IN_BB_LE_CSTAB THEN RESA_TAC THEN THAYTHE_TAC 0[`x`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v x`;`v (SUC x)`;`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 x)`;`v (SUC(SUC x))`;`&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 (x)) (v (SUC (x))) <= arclength (&2) (&2) (cstab) /\ arcV (vec 0) ((v:num->real^3) (SUC (x))) (v (SUC (SUC (x)))) <= arclength (&2) (&2) (&2 * h0) /\ arclength (&2) (&2) (&2 * h0) + arclength (&2) (&2) (cstab) < pi ==>arcV (vec 0) (v ((x))) (v ((SUC (x))))+ arcV (vec 0) (v (SUC (x))) (v (SUC (SUC (x)))) < pi`) THEN ASM_SIMP_TAC[Axjrpnc.arclength_2h0_cstab] THEN STRIP_TAC THEN MRESA_TAC WL_IN_FF[`(x)`;`v`] THEN MRESA_TAC WL_IN_FF[`SUC (x)`;`v`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (x), v (SUC (x))`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (x)), v (SUC (SUC (x)))`] THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (x)`;`v (SUC(SUC (x)))`;`v (SUC (x))`] 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 MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v x`;`v(x')`] THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v x, v (2+x)}`] ; POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`0+a=a`] THEN REPEAT RESA_TAC) THEN DICH_TAC (37-31) THEN RESA_TAC THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`(2+x)`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (2+x)`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (2+x))`] THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(2+x)`] THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (2+x)`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (2+x)`;`v (SUC (2+x))`;`&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 Axjrpnc.NORM_V_IN_BB_LE_CSTAB THEN RESA_TAC THEN THAYTHE_TAC 0[`SUC (2+x)`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (2+x))`;`v (SUC(SUC (2+x)))`;`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+x))) (v (SUC ((2+x)))) <= arclength (&2) (&2) (&2 * h0) /\ arcV (vec 0) ((v:num->real^3) (SUC ((2+x)))) (v (SUC (SUC ((2+x))))) <= arclength (&2) (&2) (cstab) /\ arclength (&2) (&2) (&2 * h0) + arclength (&2) (&2) (cstab) < pi ==>arcV (vec 0) (v (((2+x)))) (v ((SUC ((2+x)))))+ arcV (vec 0) (v (SUC ((2+x)))) (v (SUC (SUC ((2+x))))) < pi`) THEN ASM_SIMP_TAC[Axjrpnc.arclength_2h0_cstab] THEN STRIP_TAC THEN MRESA_TAC WL_IN_FF[`((2+x))`;`v`] THEN MRESA_TAC WL_IN_FF[`SUC ((2+x))`;`v`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v ((2+x)), v (SUC ((2+x)))`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC ((2+x))), v (SUC (SUC ((2+x))))`] THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v ((2+x))`;`v (SUC(SUC ((2+x))))`;`v (SUC ((2+x)))`] 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 MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v x`;`v(x')`] THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v (2+x), v (2+(2+x))}`] THEN DICH_TAC 0 THEN ASM_REWRITE_TAC[ARITH_RULE`2+2+i= 1*4+i`] THEN MRESAS_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(1*4+x):num`;`v:num->real^3`;`(1*4+x) MOD k`][MOD_REFL;ARITH_RULE`~(4=0)`;MOD_MULT_ADD] THEN MRESAS_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(x MOD k):num`;`v:num->real^3`;`x`][MOD_REFL;ARITH_RULE`~(4=0)`] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN RESA_TAC; POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`3+a=SUC(2+a)`] THEN REPEAT RESA_TAC) THEN DICH_TAC (36-31) THEN RESA_TAC THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`(2+x)`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (2+x)`] THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (2+x))`] THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(2+x)`] THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (2+x)`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (2+x))`;`v (SUC(SUC (2+x)))`;`&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 Axjrpnc.NORM_V_IN_BB_LE_CSTAB THEN RESA_TAC THEN THAYTHE_TAC 0[`(2+x)`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (2+x)`;`v (SUC (2+x))`;`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+x))) (v (SUC ((2+x)))) <= arclength (&2) (&2) (cstab) /\ arcV (vec 0) ((v:num->real^3) (SUC ((2+x)))) (v (SUC (SUC ((2+x))))) <= arclength (&2) (&2) (&2 * h0) /\ arclength (&2) (&2) (&2 * h0) + arclength (&2) (&2) (cstab) < pi ==>arcV (vec 0) (v (((2+x)))) (v ((SUC ((2+x)))))+ arcV (vec 0) (v (SUC ((2+x)))) (v (SUC (SUC ((2+x))))) < pi`) THEN ASM_SIMP_TAC[Axjrpnc.arclength_2h0_cstab] THEN STRIP_TAC THEN MRESA_TAC WL_IN_FF[`((2+x))`;`v`] THEN MRESA_TAC WL_IN_FF[`SUC ((2+x))`;`v`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v ((2+x)), v (SUC ((2+x)))`] THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC ((2+x))), v (SUC (SUC ((2+x))))`] THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v ((2+x))`;`v (SUC(SUC ((2+x))))`;`v (SUC ((2+x)))`] 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 MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v x`;`v(x')`] THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v (2+x), v (2+(2+x))}`] THEN DICH_TAC 0 THEN ASM_REWRITE_TAC[ARITH_RULE`2+2+i= 1*4+i`] THEN MRESAS_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(1*4+x):num`;`v:num->real^3`;`(1*4+x) MOD k`][MOD_REFL;ARITH_RULE`~(4=0)`;MOD_MULT_ADD] THEN MRESAS_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(x MOD k):num`;`v:num->real^3`;`x`][MOD_REFL;ARITH_RULE`~(4=0)`] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN RESA_TAC; ]);; let SCS_B_LE_CSTAB=prove(`!s v. is_scs_v39 s /\ scs_k_v39 s = 4 ==> (!i. scs_b_v39 s i (i+1) <= cstab)`, REPEAT RESA_TAC THEN DICH_TAC 1 THEN ASM_SIMP_TAC[is_scs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`3<4`;ADD1]);; let GSXRFWM= prove(`!s v. is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s ==> scs_generic v`, REPEAT STRIP_TAC THEN MATCH_MP_TAC GSXRFWM1 THEN EXISTS_TAC`s:scs_v39` THEN ASM_SIMP_TAC[GSXRFWM1;SCS_B_LE_CSTAB]);; (************************) let PSORT_5_EXPLICIT=prove(` psort 5 (0,0)= (0,0)/\ psort 5 (1,1)= (1,1)/\ psort 5 (2,2)= (2,2)/\ psort 5 (3,3)= (3,3)/\ psort 5 (4,4)= (4,4)/\ psort 5 (0,1)= (0,1)/\ psort 5 (0,2)= (0,2)/\ psort 5 (0,3)= (0,3)/\ psort 5 (0,4)= (0,4)/\ psort 5 (1,0)= (0,1)/\ psort 5 (1,2)= (1,2)/\ psort 5 (1,3)= (1,3)/\ psort 5 (1,4)= (1,4)/\ psort 5 (2,0)= (0,2)/\ psort 5 (2,1)= (1,2)/\ psort 5 (2,3)= (2,3)/\ psort 5 (2,4)= (2,4)/\ psort 5 (3,0)= (0,3)/\ psort 5 (3,1)= (1,3)/\ psort 5 (3,2)= (2,3)/\ psort 5 (3,4)= (3,4)/\ psort 5 (4,0)= (0,4)/\ psort 5 (4,1)= (1,4)/\ psort 5 (4,2)= (2,4)/\ psort 5 (4,3)= (3,4)/\ psort 5 (4,5)= (0,4)/\ psort 5 (3,5)= (0,3)/\ psort 5 (2,5)= (0,2)/\ psort 5 (1,5)= (0,1)/\ psort 5 (5,1)= (0,1)/\ psort 5 (5,2)= (0,2)/\ psort 5 (5,3)= (0,3)/\ psort 5 (5,4)= (0,4)/\ psort 5 (5,5)= (0,0)/\ psort 5 (5,6)= (0,1)/\ psort 5 (5,7)= (0,2)/\ psort 5 (4,6)= (1,4)/\ psort 5 (6,4)= (1,4)/\ psort 5 (6,5)= (0,1)/\ psort 5 (6,7)= (1,2)/\ psort 5 (7,5)= (0,2)/\ psort 5 (7,6)= (1,2)/\ psort 5 (7,7)= (2,2)/\ psort 5 (6,6)= (1,1)/\ psort 4 (3,4)= (0,3)/\ psort 3 (2,0)= (0,2)/\ psort 3 (2,1)= (1,2)/\ psort 3 (1,0)= (0,1)/\ psort 4 (0,0)= (0,0)/\ psort 4 (1,1)= (1,1)/\ psort 4 (2,2)= (2,2)/\ psort 4 (3,3)= (3,3)/\ psort 4 (4,3)= (0,3)/\ psort 4 (4,4)= (0,0)/\ psort 4 (0,2)= (0,2)/\ psort 4 (4,5)= (0,1)/\ psort 4 (5,4)= (0,1)/\ psort 4 (5,5)= (1,1) `, REWRITE_TAC[psort;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_4_TAC;LET_DEF;LET_END_DEF;MOD_5_EXPLICIT;ARITH_RULE`0<=a/\ ~(1<= 0)/\ ~(2<=0)/\ ~(3<=0)/\ ~(4<=0)/\a<=a/\ ~(2<=1)/\ ~(3<=2)/\ ~(4<=3)/\ ~(3<=1)/\ ~(4<=1)/\ ~(4<=2)/\ 2<=3`]);; let SCS_TAC= ASM_SIMP_TAC[scs_basic;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} j <=> {} i`;periodic2;scs_basic;unadorned_v39;scs_prop_equ_v39;LET_DEF;LET_END_DEF;scs_stab_diag_v39;scs_half_slice_v39; Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_5_TAC; scs_5M1;scs_3M1;scs_6I1;scs_3T1;scs_4M2;scs_6M1;scs_6T1;scs_5I1;scs_5I2;scs_5I3;scs_5M2;scs_4M6;scs_3T4;scs_5M3;scs_3T4_prime;scs_4M6_prime;scs_4M7_prime;scs_4M7;scs_3T1_prime;scs_4M8;scs_4M8_prime;scs_5T1;scs_3T5;scs_4M3;scs_3T6;scs_4M4;scs_4M5;scs_4I2;scs_4T1;scs_4T2;scs_4I1;scs_4T4;scs_4I3;scs_3T3;scs_4T5; Terminal.FUNLIST_EXPLICIT;Yrtafyh.PSORT_PERIODIC;PSORT_5_EXPLICIT; ARITH_RULE`SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6/\ SUC 6=7/\ SUC 7=8`];; (***********************) let SCS_4I2_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4I2`, [ SIMP_TAC[scs_4I2;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.467 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN REAL_ARITH_TAC; ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(&2 * #1.26 < &2)/\ ~(a {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(&2 * #1.26 < &2)/\ ~(a {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN REAL_ARITH_TAC; ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(&2 * #1.26 < &2)/\ ~(a {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN REAL_ARITH_TAC; ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(&2 * #1.26 < &2)/\ ~(a {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN MP_TAC LT_sqrt8_2h0 THEN MP_TAC sqrt8_LE_6 THEN MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN MP_TAC LE_sqrt8_2 THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`] THEN SUBGOAL_THEN`{i | i < 4 /\ (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then sqrt8 else &2 * #1.26) \/ &2 < (if psort 4 (i,SUC i) = 0,1 then &2 * #1.26 else &2))} ={0}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN MP_TAC LT_sqrt8_2h0 THEN MP_TAC sqrt8_LE_6 THEN MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN MP_TAC LE_sqrt8_2 THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`] THEN SUBGOAL_THEN`{i | i < 4 /\ (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/ &2 < (if psort 4 (i,SUC i) = 0,1 then &2 * #1.26 else &2))} ={0}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN MP_TAC LT_sqrt8_2h0 THEN MP_TAC sqrt8_LE_6 THEN MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN MP_TAC LE_sqrt8_2 THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`] THEN SUBGOAL_THEN`{i | i < 4 /\ (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then sqrt8 else &2 * #1.26) \/ &2 < (if psort 4 (i,SUC i) = 0,1 then &2 * #1.26 else &2))} ={0}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;h0] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN REAL_ARITH_TAC; MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\ (&2 * h0 < funlist_v39 [] cstab 3 i (SUC i) \/ &2 < funlist_v39 [] (&2 * h0) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`] THEN MATCH_DICH_TAC 0 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC; ]);; (*****************) let SCS_4I2_BASIC=prove(`scs_basic_v39 scs_4I2`, SCS_TAC);; let K_SCS_4I2=prove(`scs_k_v39 scs_4I2=4`, SCS_TAC);; let J_SCS_4I2=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4I2 i) i1 j= F`, SCS_TAC );; let SCS_4I1_BASIC=prove(`scs_basic_v39 scs_4I1`, SCS_TAC);; let K_SCS_4I1=prove(`scs_k_v39 scs_4I1=4`, SCS_TAC);; let J_SCS_4I1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4I1 i) i1 j= F`, SCS_TAC );; let SCS_4T1_BASIC=prove(`scs_basic_v39 scs_4T1`, SCS_TAC);; let K_SCS_4T1=prove(`scs_k_v39 scs_4T1=4`, SCS_TAC);; let J_SCS_4T1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4T1 i) i1 j= F`, SCS_TAC );; let SCS_4T2_BASIC=prove(`scs_basic_v39 scs_4T2`, SCS_TAC);; let K_SCS_4T2=prove(`scs_k_v39 scs_4T2=4`, SCS_TAC);; let J_SCS_4T2=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4T2 i) i1 j= F`, SCS_TAC );; let SCS_4T4_BASIC=prove(`scs_basic_v39 scs_4T4`, SCS_TAC);; let K_SCS_4T4=prove(`scs_k_v39 scs_4T4=4`, SCS_TAC);; let J_SCS_4T4=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4T4 i) i1 j= F`, SCS_TAC );; let J_SCS_3T4_1=prove(`scs_J_v39 (scs_3T4 ) i1 j= F`, SCS_TAC );; let SCS_4I3_BASIC=prove(`scs_basic_v39 scs_4I3`, SCS_TAC);; let K_SCS_4I3=prove(`scs_k_v39 scs_4I3=4`, SCS_TAC);; let J_SCS_4I3=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4I3 i) i1 j= F`, SCS_TAC );; let SCS_3T3_BASIC=prove(`scs_basic_v39 scs_3T3`, SCS_TAC);; let K_SCS_3T3=prove(`scs_k_v39 scs_3T3=3`, SCS_TAC);; let J_SCS_3T3=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T3 i) i1 j= F`, SCS_TAC );; let J_SCS_3T3_1=prove(`scs_J_v39 (scs_3T3 ) i1 j= F`, SCS_TAC );; let SCS_4T5_BASIC=prove(`scs_basic_v39 scs_4T5`, SCS_TAC);; let K_SCS_4T5=prove(`scs_k_v39 scs_4T5=4`, SCS_TAC);; let J_SCS_4T5=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4T5 i) i1 j= F`, SCS_TAC );; let B_LE_CSTAB_SCS_4I2=prove(` (!i. scs_b_v39 scs_4I2 i (SUC i) <= cstab)/\ (!i. scs_a_v39 scs_4I2 i (SUC i) = &2 /\ scs_b_v39 scs_4I2 i (SUC i) <= &2 * h0)`, SCS_TAC THEN REWRITE_TAC[h0;scs_diag;cstab] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;] THEN REAL_ARITH_TAC);; let B_LE_CSTAB_SCS_4I1=prove(` (!i. scs_b_v39 scs_4I1 i (SUC i) <= cstab)`, SCS_TAC THEN REWRITE_TAC[h0;scs_diag;cstab] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;] THEN REAL_ARITH_TAC);; let h0_LT_B_SCS_4I2=prove( ` (!i j. scs_diag 4 i j ==> &4 * h0 < scs_b_v39 scs_4I2 i j) /\ (!i j. scs_diag 4 i j ==> scs_a_v39 scs_4I2 i j <= cstab)`, SCS_TAC THEN REWRITE_TAC[h0;scs_diag;cstab] THEN REPEAT RESA_TAC THEN REAL_ARITH_TAC);; let h0_LT_B_SCS_4I1=prove( ` (!i j. scs_diag 4 i j ==> &4 * h0 < scs_b_v39 scs_4I1 i j) /\ (!i j. scs_diag 4 i j ==> scs_a_v39 scs_4I1 i j <= cstab)`, SCS_TAC THEN REWRITE_TAC[h0;scs_diag;cstab] THEN REPEAT RESA_TAC THEN REAL_ARITH_TAC);; let SCS_4I2_GENERIC=prove( `!v. v IN MMs_v39 scs_4I2 ==> scs_generic v`, REPEAT STRIP_TAC THEN MATCH_MP_TAC GSXRFWM THEN EXISTS_TAC`scs_4I2` THEN ASM_SIMP_TAC[GSYM ADD1;SCS_4I2_IS_SCS;K_SCS_4I2;B_LE_CSTAB_SCS_4I2]);; let A_LT_B_4I2=prove( `(!i. &2 < scs_b_v39 scs_4I2 i (SUC i)) /\ (!i. scs_a_v39 scs_4I2 i (SUC i) = &2)`, SCS_TAC THEN ASM_SIMP_TAC[h0;scs_diag;cstab;ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;] THEN REPEAT RESA_TAC THEN REAL_ARITH_TAC);; let A_LT_B_4I1=prove( `(!i. &2 < scs_b_v39 scs_4I1 i (SUC i)) /\ (!i. scs_a_v39 scs_4I1 i (SUC i) = &2)`, SCS_TAC THEN ASM_SIMP_TAC[h0;scs_diag;cstab;ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;] THEN REPEAT RESA_TAC THEN REAL_ARITH_TAC);; let CARD_SCS_M_4I2=prove(`CARD (scs_M scs_4I2) <= 1`, ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a(!v. v IN MMs_v39 scs_4I2 /\ (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==> ~(MMs_v39 (scs_4T1)={}))`, [REWRITE_TAC[IN;SET_RULE`~(A={})<=> ?a. a IN A`] THEN REPEAT STRIP_TAC THEN MP_TAC SCS_4I2_IS_SCS THEN STRIP_TAC THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN ASSUME_TAC SCS_4I2_BASIC THEN ASSUME_TAC K_SCS_4I2 THEN ASSUME_TAC SCS_4T1_BASIC THEN ASSUME_TAC K_SCS_4T1 THEN ASSUME_TAC SCS_4T1_IS_SCS THEN MP_TAC Rrcwnsj.RRCWNSJ THEN RESA_TAC THEN THAYTHES_TAC 0[`scs_4I2`;`v`][ARITH_RULE`3<4`;h0_LT_B_SCS_4I2;B_LE_CSTAB_SCS_4I2] THEN MP_TAC JCYFMRP_V3 THEN RESA_TAC THEN THAYTHES_TAC 0[`scs_4I2`;`v`][ARITH_RULE`3<4`;h0_LT_B_SCS_4I2;B_LE_CSTAB_SCS_4I2;IN;CARD_SCS_M_4I2;GSYM ADD1;A_LT_B_4I2] THEN MP_TAC Jlxfdmj.JLXFDMJ THEN RESA_TAC THEN THAYTHES_TAC 0[`scs_4I2`;`v`;`i`][ARITH_RULE`3<4`;h0_LT_B_SCS_4I2;B_LE_CSTAB_SCS_4I2;IN;CARD_SCS_M_4I2;GSYM ADD1;A_LT_B_4I2;SCS_M_4I2;SET_RULE`~{} (j MOD 4)<=> T`] THEN MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN REWRITE_TAC[IN;SET_RULE`~(A={})<=> ?a. a IN A`] THEN STRIP_TAC THEN MATCH_DICH_TAC 0 THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC`scs_4I2` THEN ASM_SIMP_TAC[SCS_M_4I2] THEN STRIP_TAC; DICH_TAC(12-4) THEN REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(5<=3))`;IN;K_SCS_4I2;K_SCS_4T1;scs_prop_equ_v39;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN SCS_TAC THEN REWRITE_TAC[ARITH_RULE`~(4<=3)`] THEN REPEAT STRIP_TAC; MP_TAC(SET_RULE`i' MOD 4 = j MOD 4\/ ~(i' MOD 4 = j MOD 4)`) THEN RESA_TAC; THAYTHE_TAC 2[`i'`;`j`]; MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN MP_TAC(SET_RULE`SUC i' MOD 4 = j MOD 4\/ ~(SUC i' MOD 4 = j MOD 4)`) THEN RESA_TAC; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`j:num`;`v`;` SUC i'`][SCS_4I2_IS_SCS;K_SCS_4I2;MOD_REFL;ARITH_RULE`~(4=0)`;] THEN REAL_ARITH_TAC; MP_TAC(SET_RULE`i' MOD 4 =SUC j MOD 4\/ ~(i' MOD 4 =SUC j MOD 4)`) THEN RESA_TAC; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`i':num`;`v`;` SUC j`][SCS_4I2_IS_SCS;K_SCS_4I2;MOD_REFL;ARITH_RULE`~(5=0)`;] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; THAYTHEL_TAC (20-15)[`i'`;`j`][scs_diag] THEN DICH_TAC 0 THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC]);; let SCS_DIAG_4_CASES=prove(`scs_diag 4 i j<=> ((i MOD 4= 0 /\ j MOD 4=2)\/ (i MOD 4= 1 /\ j MOD 4=3)\/ (j MOD 4= 0 /\ i MOD 4=2)\/ (j MOD 4= 1 /\ i MOD 4=3))`, REWRITE_TAC[scs_diag] THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`] THEN RESA_TAC THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`4`][ARITH_RULE`1<4`] THEN SYM_ASSUM_TAC THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`4`][ARITH_RULE`1<4`] THEN SYM_ASSUM_TAC THEN ARITH_TAC);; let WLOG_4_BB_SCS=prove_by_refinement(` is_scs_v39 s/\ v IN BBs_v39 s /\ scs_k_v39 s=4/\ scs_diag 4 i j /\ (!i j. (P (v i) (v j)<=> P (v j) (v i)))/\ P (v i) (v j) ==> P (v 0) (v 2)\/ P (v 1) (v 3)`, [REWRITE_TAC[SCS_DIAG_4_CASES;IN] THEN REPEAT RESA_TAC THEN POP_ASSUM MP_TAC; MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v`;`0`][ARITH_RULE`0 MOD 4=0`] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j`;`v`;`2`][ARITH_RULE`2 MOD 4=2`] THEN RESA_TAC; MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v`;`1`][ARITH_RULE`1 MOD 4=1`] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j`;`v`;`3`][ARITH_RULE`3 MOD 4=3`] THEN RESA_TAC; MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v`;`2`][ARITH_RULE`2 MOD 4=2`] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j`;`v`;`0`][ARITH_RULE`0 MOD 4=0`] THEN RESA_TAC; MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j`;`v`;`1`][ARITH_RULE`1 MOD 4=1`] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v`;`3`][ARITH_RULE`3 MOD 4=3`] THEN RESA_TAC]);; let DIST_DIAG_2_CASES=prove(`v IN MMs_v39 scs_4I2 /\ scs_diag 4 i j /\ dist(v i,v j)<= cstab ==> dist(v 0,v 2)<= cstab\/ dist(v 1,v 3)<= cstab`, REWRITE_TAC[IN] THEN STRIP_TAC THEN MRESA_TAC (INST[`scs_4I2`,`s:scs_v39`;`i:num`,`i:num`;`j:num`,`j:num`;`(\i:real^3. (\j:real^3. dist(i,j)<= cstab))`,`P:real^3->real^3->bool`;`v:num->real^3`,`v:num->real^3`]WLOG_4_BB_SCS )[`i`;`j`;`v`] THEN MATCH_DICH_TAC 0 THEN SIMP_TAC[DIST_SYM;K_SCS_4I2;SCS_4I2_IS_SCS;IN] THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]);; let WLOG_4_BB_SCS_DIAG=prove_by_refinement(` is_scs_v39 s/\ v IN BBs_v39 s /\ scs_k_v39 s=4/\ scs_diag 4 i j /\ (!i j i1 j1. P i j i1 j1 <=> P j i i1 j1)/\ (!i j i1 j1. P i j i1 j1 <=> P i j j1 i1)/\ P (v i) (v j) (v (i+1)) (v (j+1)) ==> P (v 0) (v 2) (v 1) (v 3) \/ P (v 1) (v 3) (v 0) (v 2)`, [REWRITE_TAC[SCS_DIAG_4_CASES;IN] THEN REPEAT RESA_TAC THEN POP_ASSUM MP_TAC; ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0`) THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v`;`0`][ARITH_RULE`0 MOD 4=0`;GSYM ADD1] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j`;`v`;`2`][ARITH_RULE`2 MOD 4=2`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`0`;`4`] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i`;`v`;`1`][ARITH_RULE`2 MOD 4=2`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`2`;`4`] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j`;`v`;`3`][ARITH_RULE`2 MOD 4=2`] THEN RESA_TAC; ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0`) THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v`;`1`][ARITH_RULE`0 MOD 4=0`;GSYM ADD1] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j`;`v`;`3`][ARITH_RULE`2 MOD 4=2`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`1`;`4`] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i`;`v`;`2`][ARITH_RULE`2 MOD 4=2`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`3`;`4`] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j`;`v`;`4`][ARITH_RULE`2 MOD 4=2`] THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`] THEN THAYTHE_TAC 0[`4`;`0`] THEN RESA_TAC; ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0`) THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j`;`v`;`0`][ARITH_RULE`0 MOD 4=0`;GSYM ADD1] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v`;`2`][ARITH_RULE`2 MOD 4=2`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`0`;`4`] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j`;`v`;`1`][ARITH_RULE`2 MOD 4=2`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`2`;`4`] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i`;`v`;`3`][ARITH_RULE`2 MOD 4=2`] THEN RESA_TAC; ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0`) THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j`;`v`;`1`][ARITH_RULE`0 MOD 4=0`;GSYM ADD1] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v`;`3`][ARITH_RULE`2 MOD 4=2`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`1`;`4`] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j`;`v`;`2`][ARITH_RULE`2 MOD 4=2`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`3`;`4`] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i`;`v`;`4`][ARITH_RULE`2 MOD 4=2`] THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`] THEN THAYTHE_TAC 0[`4`;`0`] THEN RESA_TAC;]);; let DIST_DIAG_2_CASES_EQ_3=prove( `v IN MMs_v39 scs_4I2 /\ scs_diag 4 i j /\ dist(v i,v j)= &3 /\ dist(v (i+1),v (j+1))= &3 ==> dist(v 0,v 2)= &3 /\ dist(v 1,v 3)= &3`, REWRITE_TAC[IN] THEN STRIP_TAC THEN MRESA_TAC (INST[`scs_4I2`,`s:scs_v39`;`i:num`,`i:num`;`j:num`,`j:num`;`(\i:real^3. (\j:real^3. (\i1:real^3. (\j1:real^3. dist(i,j)= &3/\ dist(i1,j1)= &3))))`,`P:real^3->real^3->real^3->real^3->bool`;`v:num->real^3`,`v:num->real^3`]WLOG_4_BB_SCS_DIAG )[`i`;`j`;`v`] THEN DICH_TAC 0 THEN SIMP_TAC[DIST_SYM;K_SCS_4I2;SCS_4I2_IS_SCS;IN] THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN RESA_TAC);; let DIST_DIAG_2_CASES_3_LE=prove( `MMs_v39 scs_4I2 v /\ scs_diag 4 i j /\ &3<= dist(v i,v j) /\ &3<= dist(v (i+1),v (j+1)) ==> &3<= dist(v 0,v 2) /\ &3<= dist(v 1,v 3)`, REWRITE_TAC[IN] THEN STRIP_TAC THEN MRESA_TAC (INST[`scs_4I2`,`s:scs_v39`;`i:num`,`i:num`;`j:num`,`j:num`;`(\i:real^3. (\j:real^3. (\i1:real^3. (\j1:real^3. &3<= dist(i,j)/\ &3<= dist(i1,j1)))))`,`P:real^3->real^3->real^3->real^3->bool`;`v:num->real^3`,`v:num->real^3`]WLOG_4_BB_SCS_DIAG )[`i`;`j`;`v`] THEN DICH_TAC 0 THEN SIMP_TAC[DIST_SYM;K_SCS_4I2;SCS_4I2_IS_SCS;IN] THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN RESA_TAC);; let DIST_DIAG_2_CASES_3_LT=prove( `MMs_v39 scs_4I2 v /\ scs_diag 4 i j /\ &3<= dist(v i,v j) /\ &3< dist(v (i+1),v (j+1)) ==> (&3<= dist(v 0,v 2) /\ &3< dist(v 1,v 3))\/ (&3<= dist(v 1,v 3) /\ &3< dist(v 0,v 2))`, REWRITE_TAC[IN] THEN STRIP_TAC THEN MRESA_TAC (INST[`scs_4I2`,`s:scs_v39`;`i:num`,`i:num`;`j:num`,`j:num`;`(\i:real^3. (\j:real^3. (\i1:real^3. (\j1:real^3. &3<= dist(i,j)/\ &3< dist(i1,j1)))))`,`P:real^3->real^3->real^3->real^3->bool`;`v:num->real^3`,`v:num->real^3`]WLOG_4_BB_SCS_DIAG )[`i`;`j`;`v`] THEN DICH_TAC 0 THEN SIMP_TAC[DIST_SYM;K_SCS_4I2;SCS_4I2_IS_SCS;IN] THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN RESA_TAC);; let WLOG_ASSUME_MIN=prove(`((a<=c /\ a<=b)\/ (c<=a /\ c<=b) ==> Q) ==> (a<=b \/ c<=b ==> Q)`, REPEAT STRIP_TAC THEN MATCH_DICH_TAC 1 THEN DICH_TAC 0 THEN REAL_ARITH_TAC);; let ASSUME_MIN_DIAG= prove_by_refinement(` (!i j. MMs_v39 scs_4I2 v/\ scs_diag 4 i j /\ dist(v i,v j)<= cstab/\ dist(v i,v j)<= dist(v (i+1),v (j+1)) ==> ~(MMs_v39 (scs_4T1)={})\/ ~(MMs_v39 (scs_4T2)={})) ==>(!i j. MMs_v39 scs_4I2 v /\ scs_diag 4 i j /\ dist(v i,v j)<= cstab ==> ~(MMs_v39 (scs_4T1)={})\/ ~(MMs_v39 (scs_4T2)={}))`, [ REPEAT RESA_TAC THEN MP_TAC(SET_RULE` dist(v i,v j)<= dist(v (i+1),v (j+1)) \/ ~( dist(v i,v j)<= dist(v (i+1),(v:num->real^3) (j+1))) `) THEN RESA_TAC; MATCH_DICH_TAC 4 THEN EXISTS_TAC`i:num` THEN EXISTS_TAC`j:num` THEN ASM_REWRITE_TAC[]; MATCH_DICH_TAC 4 THEN EXISTS_TAC`i+1:num` THEN EXISTS_TAC`j+1:num` THEN ASM_REWRITE_TAC[] THEN DICH_TAC 2 THEN ASM_REWRITE_TAC[SCS_DIAG_4_CASES] THEN RESA_TAC THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`4`][ARITH_RULE`1<4`;GSYM ADD1] THEN SYM_ASSUM_TAC THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`4`][ARITH_RULE`1<4`] THEN SYM_ASSUM_TAC THEN STRIP_TAC THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN ASSUME_TAC SCS_4I2_IS_SCS THEN ASSUME_TAC K_SCS_4I2; ARITH_TAC; ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0`) THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`0`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`1`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`2`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC j`;`3`;`4`] THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`] THEN THAYTHEL_ASM_TAC 0[`SUC i`;`1`][] THEN THAYTHEL_ASM_TAC 0[`SUC j`;`3`][] THEN THAYTHEL_ASM_TAC 0[`SUC(SUC j)`;`4`][] THEN THAYTHEL_ASM_TAC 0[`SUC(SUC i)`;`2`][] THEN THAYTHEL_ASM_TAC 0[`4`;`0`][] THEN THAYTHEL_ASM_TAC 0[`i`;`0`][] THEN THAYTHEL_ASM_TAC 0[`j`;`2`][] THEN DICH_TAC(20-1) THEN DICH_TAC(19-1) THEN ASM_SIMP_TAC[GSYM ADD1] THEN MRESA_TAC DIST_SYM[`v 2`;`v 0`] THEN REAL_ARITH_TAC; ARITH_TAC; ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ SUC 4=5/\ 5 MOD 4=1`) THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`1`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`2`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`3`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC j`;`4`;`4`] THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`] THEN THAYTHEL_ASM_TAC 0[`SUC i`;`2`][] THEN THAYTHEL_ASM_TAC 0[`SUC j`;`4`][] THEN THAYTHEL_ASM_TAC 0[`SUC(SUC j)`;`1`][] THEN THAYTHEL_ASM_TAC 0[`SUC(SUC i)`;`3`][] THEN THAYTHEL_ASM_TAC 0[`4`;`0`][] THEN THAYTHEL_ASM_TAC 0[`i`;`1`][] THEN THAYTHEL_ASM_TAC 0[`j`;`3`][] THEN DICH_TAC(20-1) THEN DICH_TAC(19-1) THEN ASM_SIMP_TAC[GSYM ADD1] THEN MRESA_TAC DIST_SYM[`v 3`;`v 1`] THEN REAL_ARITH_TAC; ARITH_TAC; ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0`) THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`2`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`3`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`0`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC j`;`1`;`4`] THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`] THEN THAYTHEL_ASM_TAC 0[`SUC i`;`3`][] THEN THAYTHEL_ASM_TAC 0[`SUC j`;`1`][] THEN THAYTHEL_ASM_TAC 0[`SUC(SUC j)`;`2`][] THEN THAYTHEL_ASM_TAC 0[`SUC(SUC i)`;`4`][] THEN THAYTHEL_ASM_TAC 0[`4`;`0`][] THEN THAYTHEL_ASM_TAC 0[`i`;`2`][] THEN THAYTHEL_ASM_TAC 0[`j`;`0`][] THEN DICH_TAC(20-1) THEN DICH_TAC(19-1) THEN ASM_SIMP_TAC[GSYM ADD1] THEN MRESA_TAC DIST_SYM[`v 0`;`v 2`] THEN REAL_ARITH_TAC; ARITH_TAC; ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ SUC 4=5/\ 5 MOD 4=1`) THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`3`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`4`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`1`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC j`;`2`;`4`] THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`] THEN THAYTHEL_ASM_TAC 0[`SUC i`;`4`][] THEN THAYTHEL_ASM_TAC 0[`SUC j`;`2`][] THEN THAYTHEL_ASM_TAC 0[`SUC(SUC j)`;`3`][] THEN THAYTHEL_ASM_TAC 0[`SUC(SUC i)`;`1`][] THEN THAYTHEL_ASM_TAC 0[`4`;`0`][] THEN THAYTHEL_ASM_TAC 0[`i`;`3`][] THEN THAYTHEL_ASM_TAC 0[`j`;`1`][] THEN DICH_TAC(20-1) THEN DICH_TAC(19-1) THEN ASM_SIMP_TAC[GSYM ADD1] THEN MRESA_TAC DIST_SYM[`v 1`;`v 3`] THEN REAL_ARITH_TAC]);; let SCS_4I2_3_LE_A=prove_by_refinement(` BBs_v39 scs_4I2 v/\ scs_diag 4 i j ==> &3<= dist(v i,v j)`, [ REWRITE_TAC[IN] THEN REPEAT RESA_TAC THEN DICH_TAC 0 THEN REWRITE_TAC[SCS_DIAG_4_CASES] THEN RESA_TAC; ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ ~(0=1)/\ ~(1=2)/\ ~(3=0)`) THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`i`;`v`;`0`][ARITH_RULE`0 MOD 4=0`;SCS_4I2_IS_SCS;K_SCS_4I2] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`j`;`v`;`2`][ARITH_RULE`2 MOD 4=2`;SCS_4I2_IS_SCS;K_SCS_4I2] THEN DICH_TAC 5 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;mk_unadorned_v39;scs_v39_explicit;scs_4I2;CS_ADJ;ARITH_RULE`~(4<=3)`] THEN RESA_TAC THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`0`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`2`;`4`] THEN THAYTHES_TAC 3[`i`;`j`][ARITH_RULE`~(0=2)`]; ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ ~(0=1)/\ ~(1=2)/\ ~(3=0)/\ ~(1=3)/\ ~(2=3)`) THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`i`;`v`;`1`][ARITH_RULE`0 MOD 4=0`;SCS_4I2_IS_SCS;K_SCS_4I2] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`j`;`v`;`3`][ARITH_RULE`2 MOD 4=2`;SCS_4I2_IS_SCS;K_SCS_4I2] THEN DICH_TAC 5 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;mk_unadorned_v39;scs_v39_explicit;scs_4I2;CS_ADJ;ARITH_RULE`~(4<=3)`] THEN RESA_TAC THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`1`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`3`;`4`] THEN THAYTHES_TAC 3[`i`;`j`][ARITH_RULE`~(0=2)`]; ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ ~(0=1)/\ ~(1=2)/\ ~(3=0)`) THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`j`;`v`;`0`][ARITH_RULE`0 MOD 4=0`;SCS_4I2_IS_SCS;K_SCS_4I2] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`i`;`v`;`2`][ARITH_RULE`2 MOD 4=2`;SCS_4I2_IS_SCS;K_SCS_4I2] THEN DICH_TAC 5 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;mk_unadorned_v39;scs_v39_explicit;scs_4I2;CS_ADJ;ARITH_RULE`~(4<=3)`] THEN RESA_TAC THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`0`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`2`;`4`] THEN THAYTHES_TAC 3[`i`;`j`][ARITH_RULE`~(0=2)`]; ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ ~(0=1)/\ ~(1=2)/\ ~(3=0)/\ ~(1=3)/\ ~(2=3)`) THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`j`;`v`;`1`][ARITH_RULE`0 MOD 4=0`;SCS_4I2_IS_SCS;K_SCS_4I2] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`i`;`v`;`3`][ARITH_RULE`2 MOD 4=2`;SCS_4I2_IS_SCS;K_SCS_4I2] THEN DICH_TAC 5 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;mk_unadorned_v39;scs_v39_explicit;scs_4I2;CS_ADJ;ARITH_RULE`~(4<=3)`] THEN RESA_TAC THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`1`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`3`;`4`] THEN THAYTHES_TAC 3[`i`;`j`][ARITH_RULE`~(0=2)`]]);; let SCS_DIAG_ADD1=prove_by_refinement(`scs_diag 4 i j==> scs_diag 4 (i+1) (j+1)`, [REWRITE_TAC[SCS_DIAG_4_CASES;GSYM ADD1] THEN RESA_TAC; ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ ~(0=1)/\ ~(1=2)/\ ~(3=0)/\ ~(1=3)/\ ~(2=3)`) THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`0`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`2`;`4`]; ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ ~(0=1)/\ ~(1=2)/\ ~(3=0)/\ ~(1=3)/\ ~(2=3)`) THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`1`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`3`;`4`]; ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ ~(0=1)/\ ~(1=2)/\ ~(3=0)/\ ~(1=3)/\ ~(2=3)`) THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`0`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`2`;`4`]; ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ ~(0=1)/\ ~(1=2)/\ ~(3=0)/\ ~(1=3)/\ ~(2=3)`) THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`1`;`4`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`3`;`4`]]);; let ear_acute = prove_by_refinement( `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6. &2 <= y1 /\ y1 <= &2 * h0 /\ &2 <= y2 /\ y2 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 /\ &2 <= y4 /\ y4 <= &2 * h0 /\ &2 <= y6 /\ y6 <= &2 * h0 /\ &3 <= y5 /\ &0 < ups_x (y1*y1) (y3*y3) (y5*y5) ==> dih_y y1 y2 y3 y4 y5 y6 < pi / &2)`, (* {{{ proof *) [ REWRITE_TAC[Sphere.h0;arith `&2 * #1.26 = #2.52`;Trigonometry.IHIQXLM]; REPEAT WEAKER_STRIP_TAC; INTRO_TAC (Terminal.get_main_nonlinear "2485876245a") [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`]; ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;arith `#3.0 = &3`;]; ANTS_TAC; REWRITE_TAC[arith `x <= y <=> ~(y < x)`]; DISCH_TAC; FIRST_X_ASSUM_ST `&16` MP_TAC THEN REWRITE_TAC[arith `a * b * c = (a * b) * c`]; REWRITE_TAC[arith `~(&0 < x * y) <=> &0 <= x * (-- y)`]; REPEAT (GMATCH_SIMP_TAC REAL_LE_MUL_EQ); REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ); BY(ASM_TAC THEN REAL_ARITH_TAC); REWRITE_TAC[Nonlinear_lemma.dih_x_alt;Sphere.dih_y;LET_THM;GSYM Sphere.delta_y]; REWRITE_TAC[GSYM Sphere.delta4_y;GSYM Sphere.y_of_x]; REWRITE_TAC[arith `pi2 + a < pi2 <=> a < &0`]; DISCH_TAC; GMATCH_SIMP_TAC Tskajxy.ATN2_Y_NEG; CONJ_TAC; BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC); BY(REWRITE_TAC[arith `p - a = p + -- a`;GSYM ATN_NEG;arith `-- p + a < &0 <=> a < p`;ATN_BOUNDS]) ]);; (* }}} *) let SCS_DIAG_4_ADD2=prove(`scs_diag 4 (i+1) (i+3)`, SIMP_TAC[scs_diag;ARITH_RULE`~(4=0)/\ SUC(i+1)= i+2/\ SUC (i+3)=i+4`;Ocbicby.MOD_EQ_MOD_SHIFT;] THEN ARITH_TAC);; let SCS_DIAG_4_ADD0=prove(`scs_diag 4 (i) (i+2)`, SIMP_TAC[scs_diag;ARITH_RULE`~(4=0)/\ SUC(i)= i+1/\ SUC (i+2)=i+3`;Ocbicby.MOD_EQ_MOD_SHIFT;] THEN MP_TAC(SET_RULE`i= i+0==> i MOD 4= (i+0) MOD 4`) THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`i+0=i`] THEN RESA_TAC THEN SIMP_TAC[scs_diag;ARITH_RULE`~(4=0)/\ SUC(i)= i+1/\ SUC (i+2)=i+3`;Ocbicby.MOD_EQ_MOD_SHIFT;] THEN ARITH_TAC);; let EDGE_4I2_LE_2H0=prove(`BBs_v39 scs_4I2 v ==> dist(v i, v (i+1))<= &2* h0/\ &2<= dist(v i, v (i+1))`, REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4I2;K_SCS_4T1;scs_prop_equ_v39;] THEN STRIP_TAC THEN THAYTHE_TAC 1[`i`;`i+1`] THEN DICH_TAC 0 THEN DICH_TAC 0 THEN SCS_TAC THEN ASM_SIMP_TAC[GSYM ADD1;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]);; let SCS_4I2_STRAIGHT= prove_by_refinement(`main_nonlinear_terminal_v11 ==>(!i. MMs_v39 scs_4I2 v ==> azim (vec 0) (v i) (v (i+1)) (v (i+3))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 MRESAL_TAC SCS_4I2_GENERIC[`v`][IN;scs_generic] THEN ASSUME_TAC(ARITH_RULE`3<4`) THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`scs_4I2`;`v`] THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC THEN MRESA_TAC WL_IN_V[`(i+1)`;`v:num->real^3`] THEN MRESA_TAC WL_IN_V[`i+3`;`v:num->real^3`] THEN MRESA_TAC WL_IN_V[`i`;`v:num->real^3`] THEN MRESA_TAC WL_IN_V[`i+2`;`v:num->real^3`] THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`] THEN MP_TAC(SET_RULE`i= i+0==> i MOD 4= (i+0) MOD 4`) THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`i+0=i`] THEN RESA_TAC THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v i`;`v (i+2)`;`V`] THEN THAYTHES_TAC 0[`v i`;`v (i+2)`][SET_RULE`a IN {a,b}`;ARITH_RULE`~(4=0)/\ ~(0 MOD 4 = 2 MOD 4)`;Ocbicby.MOD_EQ_MOD_SHIFT] THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (i+1)`;`v (i+3)`;`V`] THEN THAYTHES_TAC 0[`v (i+3)`;`v (i)`][SET_RULE`a IN {b,a}`;ARITH_RULE`~(4=0)/\ ~(0 MOD 4 = 3 MOD 4)`;Ocbicby.MOD_EQ_MOD_SHIFT] THEN DICH_TAC 0 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN STRIP_TAC THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (i+1)`;`v (i+3)`;`V`] THEN THAYTHES_TAC 0[`v (i+1)`;`v (i)`][SET_RULE`a IN {a,b}`;ARITH_RULE`~(4=0)/\ ~(0 MOD 4 = 1 MOD 4)`;Ocbicby.MOD_EQ_MOD_SHIFT] THEN DICH_TAC 0 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN STRIP_TAC THEN MRESAL_TAC Collect_geom2.NOT_COL_EQ_UPS_X_POS[`vec 0:real^3`;`v (i)`;`v(i+2)`][dist;VECTOR_ARITH`vec 0-A= --A`;NORM_NEG] THEN DICH_TAC 0 THEN REWRITE_TAC[GSYM dist] THEN RESA_TAC THEN MRESA_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`scs_4I2`;`FF`;`v i`;`v`;`i`;`4`] THEN MRESA_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v i`] THEN THAYTHE_TAC 0[`v(i+2)`] THEN MP_TAC ear_acute THEN RESA_TAC THEN THAYTHES_TAC 0[`norm (v (i))`;`norm (v (i+1))`;`norm (v (i+2))`;`dist(v (i+1),v (i+2))`;`dist(v (i),v(i+2))`;`dist(v i, v(i+1))`][REAL_ARITH`a*a= a pow 2`] THEN DICH_TAC 0 THEN MRESAL_TAC Iunbuig.azim_dih_y[`vec 0:real^3`;`v i`;`v (i+1)`;`v(i+2)`][dist;VECTOR_ARITH`vec 0-A= --A`;NORM_NEG] THEN SYM_ASSUM_TAC THEN MRESA_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v i`] THEN THAYTHE_TAC 0[`v(i+3)`] THEN MRESAL_TAC Terminal.vv_split_azim_generic[`v`;`4`;`i`;`2`;`3`][LET_DEF;LET_END_DEF;ARITH_RULE`3<=4/\0<2/\ 2<3`] THEN DICH_TAC 0 THEN SUBGOAL_THEN`(!i j. i < 4 /\ j < 4 /\ i MOD 4 = j MOD 4 ==> i = j)`ASSUME_TAC; REPEAT RESA_TAC THEN DICH_TAC 0 THEN ASM_SIMP_TAC[ARITH_RULE`~(4=0)`;MOD_LT]; ASM_REWRITE_TAC[] THEN DICH_TAC(54-5) THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;K_SCS_4I2;ARITH_RULE`~(4<=3)`;ADD1] THEN RESA_TAC THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`azim (vec 0) (v i) (v (i + 1)) (v (i + 3)) <= pi/\ azim (vec 0) (v i) (v (i + 1)) (v (i + 3)) = azim (vec 0) (v i) (v (i + 1)) (v (i + 2)) + azim (vec 0) (v i) (v (i + 2)) (v (i + 3)) /\ &0<= azim (vec 0) (v i) (v (i + 1)) (v (i + 2)) ==> azim (vec 0) (v i) (v (i + 2)) (v (i + 3))<= pi `) THEN ASM_REWRITE_TAC[azim] THEN STRIP_TAC THEN MP_TAC ear_acute THEN RESA_TAC THEN THAYTHEL_TAC 0[`norm (v (i))`;`norm (v (i+3))`;`norm (v (i+2))`;`dist(v (i+2),v (i+3))`;`dist(v (i),v(i+2))`;`dist(v i, v(i+3))`][REAL_ARITH`a*a= a pow 2`] THEN DICH_TAC 0 THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC(REAL_ARITH`a a+b< c`) THEN ASM_REWRITE_TAC[] THEN MRESAL_TAC Iunbuig.azim_dih_y[`vec 0:real^3`;`v i`;`v (i+2)`;`v(i+3)`][dist;VECTOR_ARITH`vec 0-A= --A`;NORM_NEG] THEN ONCE_REWRITE_TAC[Nonlinear_lemma.dih_y_sym] THEN REWRITE_TAC[GSYM dist] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]]);; let SCS_4I2_STRAIGHT_ALL= prove_by_refinement(`main_nonlinear_terminal_v11 ==>( MMs_v39 scs_4I2 v==> azim (vec 0) (v 0) (v 1) (v 3) < pi /\ azim (vec 0) (v 1) (v 2) (v 0) < pi /\ azim (vec 0) (v 2) (v 3) (v 1) < pi /\ azim (vec 0) (v 3) (v 0) (v 2) < pi )`, [REPEAT STRIP_TAC THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN ASSUME_TAC(SCS_4I2_IS_SCS) THEN ASSUME_TAC(K_SCS_4I2) THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`] THEN MP_TAC SCS_4I2_STRAIGHT THEN RESA_TAC; THAYTHEL_TAC 0[`0`][ARITH_RULE`0+a=a`]; THAYTHEL_TAC 1[`4`;`0`][ARITH_RULE`4 MOD 4 = 0 MOD 4`] THEN THAYTHEL_TAC 1[`1`][ARITH_RULE`1+1=2/\1+3=4`]; THAYTHEL_TAC 1[`5`;`1`][ARITH_RULE`5 MOD 4 = 1 MOD 4`] THEN THAYTHEL_TAC 1[`2`][ARITH_RULE`2+1=3/\2+3=5`]; THAYTHEL_ASM_TAC 1[`4`;`0`][ARITH_RULE`4 MOD 4 = 0 MOD 4`] THEN THAYTHEL_TAC 0[`6`;`2`][ARITH_RULE`6 MOD 4 = 2 MOD 4`] THEN THAYTHEL_TAC 2[`3`][ARITH_RULE`3+1=4/\3+3=6`]]);; let EXPAND_DIAG_4=prove_by_refinement(`scs_diag 4 i j ==> j MOD 4= (i+2) MOD 4`, [REWRITE_TAC[SCS_DIAG_4_CASES;ARITH_RULE`i+2=SUC(SUC i)`] THEN RESA_TAC; MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`0`;`4`][Uxckfpe.ARITH_4_TAC] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`1`;`4`][Uxckfpe.ARITH_4_TAC]; MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`1`;`4`][Uxckfpe.ARITH_4_TAC] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`2`;`4`][Uxckfpe.ARITH_4_TAC]; MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`2`;`4`][Uxckfpe.ARITH_4_TAC] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`3`;`4`][Uxckfpe.ARITH_4_TAC]; MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`3`;`4`][Uxckfpe.ARITH_4_TAC] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`4`;`4`][Uxckfpe.ARITH_4_TAC]]);; let EDGE_EQ_2_4I2=prove_by_refinement(`main_nonlinear_terminal_v11 ==>(!i j. MMs_v39 scs_4I2 v/\ scs_diag 4 i j /\ &3 <= dist (v i,v j) /\ &3 < dist (v (i + 1),v (j + 1)) ==> dist(v (SUC i), v(SUC (SUC i)))= &2 )`, [REPEAT RESA_TAC 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 ASSUME_TAC(ARITH_RULE`3<4/\ 0 + 4 - 1= 3/\ 0+1=1/\ SUC 0=1/\ SUC i + 4 - 1=i+4/\ ~(4=0)/\ 2 MOD 4=2/\ 0 MOD 4=0/\ (i + 1) + 2= i+3/\ 2+2=4/\ 3+2=5 /\ 3+1=4/\ 3+3=6/\ 6 MOD 4=2/\ 1 MOD 4=1/\ 3 MOD 4=3 /\ 2+1=3/\ 2+3=5`) THEN ASSUME_TAC(ARITH_RULE`i+4= 1*4+i/\ SUC i+1=i+2/\ SUC i + 3= i+4`) THEN ASSUME_TAC(SCS_4I2_IS_SCS) THEN ASSUME_TAC(K_SCS_4I2) THEN ASSUME_TAC(SCS_4I2_BASIC) THEN ASSUME_TAC(h0_LT_B_SCS_4I2) THEN MRESAL_TAC SCS_4I2_GENERIC[`v`][IN] THEN MP_TAC CUXVZOZ THEN RESA_TAC THEN THAYTHEL_TAC 0[`scs_4I2`;`FF`;`4`;`i+1`;`v`][GSYM ADD1;B_LE_CSTAB_SCS_4I2] THEN MATCH_DICH_TAC 0 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHEL_TAC 0[`i+4`;`i`][MOD_MULT_ADD;] THEN DICH_TAC 1 THEN REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4M8_prime;K_SCS_4M8;scs_prop_equ_v39;K_SCS_4I2] THEN STRIP_TAC THEN THAYTHEL_TAC 1[`i`;`SUC i`][B_LE_CSTAB_SCS_4I2] THEN MP_TAC(REAL_ARITH`scs_b_v39 scs_4I2 i (SUC i) <= cstab /\ dist (v i,v (SUC i)) <= scs_b_v39 scs_4I2 i (SUC i) ==> dist (v i,(v:num->real^3) (SUC i)) <= cstab`) THEN ASM_SIMP_TAC[B_LE_CSTAB_SCS_4I2] THEN STRIP_TAC THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN MRESAL_TAC SCS_4I2_3_LE_A[`i`;`v`;`i+2`][SCS_DIAG_4_ADD0] THEN MP_TAC SCS_4I2_STRAIGHT THEN RESA_TAC THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1] THEN MRESA_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`scs_4I2`;`FF`;`v (SUC i)`;`v`;`SUC i`;`4`] THEN THAYTHEL_ASM_TAC 2[`SUC i`][] THEN MRESA_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`scs_4I2`;`FF`;`v (SUC(SUC i))`;`v`;`SUC (SUC i)`;`4`] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHEL_TAC 0[`1 * 4 + SUC i`;`SUC i`][MOD_MULT_ADD;] THEN THAYTHEL_ASM_TAC (29-26)[`SUC (SUC i)`][] THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC i)=i+2`] THEN REPEAT GEN_TAC THEN REWRITE_TAC[SCS_DIAG_4_CASES;] THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i':num`;`j':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`] THEN SYM_ASSUM_TAC THEN MRESAS_TAC Hexagons.PSORT_MOD[`4`;`1*4+i:num`;`i+2:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`;MOD_MULT_ADD] THEN SYM_ASSUM_TAC THEN MRESA_TAC MOD_ADD_MOD[`i`;`2`;`4`] THEN SYM_ASSUM_TAC THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHEL_TAC 0[`i'`;`i' MOD 4`][MOD_MULT_ADD;] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHEL_TAC 0[`j'`;`j' MOD 4`][MOD_MULT_ADD;] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHES_TAC 0[`i+1`;`(i+1) MOD 4`][MOD_REFL;] THEN POP_ASSUM MP_TAC THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`] THEN SYM_ASSUM_TAC THEN STRIP_TAC THEN MP_TAC SCS_DIAG_ADD1 THEN RESA_TAC THEN MRESA_TAC EXPAND_DIAG_4[`j+1`;`i+1`] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHES_TAC 0[`j+1`;`(i+3) MOD 4`][MOD_REFL;] THEN POP_ASSUM MP_TAC THEN MRESA_TAC MOD_ADD_MOD[`i`;`3`;`4`] THEN SYM_ASSUM_TAC THEN STRIP_TAC THEN DICH_TAC(39-4) THEN ASM_REWRITE_TAC[]; MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION] THEN RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`0+2=2`] THEN SCS_TAC THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`0`;`4`][Uxckfpe.ARITH_4_TAC] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`2`;`4`][Uxckfpe.ARITH_4_TAC] THEN ASM_SIMP_TAC[DIST_SYM]; MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION] THEN RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`0+2=2`] THEN SCS_TAC THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`1`;`4`][Uxckfpe.ARITH_4_TAC] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`3`;`4`][Uxckfpe.ARITH_4_TAC] THEN ASM_SIMP_TAC[DIST_SYM]; MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION] THEN RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`0+2=2`] THEN SCS_TAC THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`2`;`4`][Uxckfpe.ARITH_4_TAC] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`0`;`4`][Uxckfpe.ARITH_4_TAC] THEN ASM_SIMP_TAC[DIST_SYM]; MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION] THEN RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`0+2=2`] THEN SCS_TAC THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`3`;`4`][Uxckfpe.ARITH_4_TAC] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`1`;`4`][Uxckfpe.ARITH_4_TAC] THEN ASM_SIMP_TAC[DIST_SYM]]);; let EXPAND_DIAG_4_DIST=prove_by_refinement(`main_nonlinear_terminal_v11 ==>(!i j. MMs_v39 scs_4I2 v/\ scs_diag 4 i j /\ &3 <= dist (v i,v j) /\ &3 < dist (v (i + 1),v (j + 1)) ==> &3 <= dist (v i,v (i+2)) /\ &3 < dist (v (i + 1),v (i + 3)))`, [ REPEAT RESA_TAC THEN MP_TAC EXPAND_DIAG_4 THEN RESA_TAC THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]; MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHES_TAC 0[`i+2`;`j `][MOD_REFL;]; MP_TAC SCS_DIAG_ADD1 THEN RESA_TAC THEN MRESA_TAC EXPAND_DIAG_4[`j+1`;`i+1`] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHES_TAC 0[`(i+3)`;`j+1`][MOD_REFL;ARITH_RULE`(i + 1) + 2= i+3`]]);; let B_LE_CSTAB_SCS_4I2_prime=prove(`scs_a_v39 scs_4I2 (SUC i) (1 * 4 + i) = &2 /\ scs_b_v39 scs_4I2 (SUC i) (1 * 4 + i) <= &2 * h0`, SCS_TAC THEN ASM_SIMP_TAC[MOD_MULT_ADD] THEN REWRITE_TAC[h0;scs_diag;cstab] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`SUC (1 * 4 + i)= 1 * 4 + SUC i`;MOD_MULT_ADD] THEN REAL_ARITH_TAC);; let EDGE_EQ_2_4I2_1=prove_by_refinement(`main_nonlinear_terminal_v11 ==>(!i j. MMs_v39 scs_4I2 v/\ scs_diag 4 i j /\ &3 <= dist (v i,v j) /\ &3 < dist (v (i + 1),v (j + 1)) ==> dist(v (i), v((SUC i)))= &2 )`, [REPEAT RESA_TAC 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 ASSUME_TAC(ARITH_RULE`3<4/\ 0 + 4 - 1= 3/\ 0+1=1/\ SUC 0=1/\ SUC i + 4 - 1=i+4/\ ~(4=0)/\ 2 MOD 4=2/\ 0 MOD 4=0/\ (i + 1) + 2= i+3/\ 2+2=4/\ 3+2=5 /\ 3+1=4/\ 3+3=6/\ 6 MOD 4=2/\ 1 MOD 4=1/\ 3 MOD 4=3 /\ 2+1=3/\ 2+3=5`) THEN ASSUME_TAC(ARITH_RULE`i+4= 1*4+i/\ SUC i+1=i+2/\ SUC i + 3= i+4`) THEN ASSUME_TAC(SCS_4I2_IS_SCS) THEN ASSUME_TAC(K_SCS_4I2) THEN ASSUME_TAC(SCS_4I2_BASIC) THEN ASSUME_TAC(h0_LT_B_SCS_4I2) THEN MRESAL_TAC SCS_4I2_GENERIC[`v`][IN] THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHEL_TAC 0[`i+4`;`i`][MOD_MULT_ADD;] THEN MP_TAC CJBDXXN THEN RESA_TAC THEN THAYTHEL_TAC 0[`scs_4I2`;`FF`;`4`;`i+1`;`v`][GSYM ADD1;B_LE_CSTAB_SCS_4I2] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN MATCH_DICH_TAC 0 THEN DICH_TAC 1 THEN REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4M8_prime;K_SCS_4M8;scs_prop_equ_v39;K_SCS_4I2] THEN STRIP_TAC THEN THAYTHEL_TAC 1[`SUC i`;`SUC(SUC i)`;][B_LE_CSTAB_SCS_4I2] THEN MP_TAC(REAL_ARITH`scs_b_v39 scs_4I2 (SUC i) (SUC(SUC i)) <= cstab /\ dist (v (SUC i), v(SUC(SUC i))) <= scs_b_v39 scs_4I2 (SUC i) (SUC(SUC i)) ==> dist ((v:num->real^3) (SUC i),v(SUC(SUC i))) <= cstab`) THEN ASM_SIMP_TAC[B_LE_CSTAB_SCS_4I2] THEN STRIP_TAC THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[B_LE_CSTAB_SCS_4I2_prime] THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN MRESAL_TAC SCS_4I2_3_LE_A[`i`;`v`;`i+2`][SCS_DIAG_4_ADD0;ARITH_RULE`SUC(SUC i)=i+2`] THEN MP_TAC SCS_4I2_STRAIGHT THEN RESA_TAC THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1] THEN MRESA_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`scs_4I2`;`FF`;`v (SUC i)`;`v`;`SUC i`;`4`] THEN THAYTHEL_ASM_TAC 2[`SUC i`][] THEN MRESAL_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`scs_4I2`;`FF`;`v i`;`v`;`i`;`4`][ARITH_RULE`i+4-1=i+3`] THEN REPEAT GEN_TAC THEN REWRITE_TAC[SCS_DIAG_4_CASES;] THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i':num`;`j':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`] THEN SYM_ASSUM_TAC THEN MRESAS_TAC Hexagons.PSORT_MOD[`4`;`i+2:num`;`1*4+i:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`;MOD_MULT_ADD] THEN SYM_ASSUM_TAC THEN MRESA_TAC MOD_ADD_MOD[`i`;`2`;`4`] THEN SYM_ASSUM_TAC THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHEL_TAC 0[`i'`;`i' MOD 4`][MOD_MULT_ADD;] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHEL_TAC 0[`j'`;`j' MOD 4`][MOD_MULT_ADD;] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHES_TAC 0[`i+1`;`(i+1) MOD 4`][MOD_REFL;] THEN POP_ASSUM MP_TAC THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`] THEN SYM_ASSUM_TAC THEN STRIP_TAC THEN MP_TAC SCS_DIAG_ADD1 THEN RESA_TAC THEN MRESA_TAC EXPAND_DIAG_4[`j+1`;`i+1`] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHES_TAC 0[`j+1`;`(i+3) MOD 4`][MOD_REFL;] THEN POP_ASSUM MP_TAC THEN MRESA_TAC MOD_ADD_MOD[`i`;`3`;`4`] THEN SYM_ASSUM_TAC THEN STRIP_TAC THEN DICH_TAC(37-4) THEN ASM_REWRITE_TAC[]; MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION] THEN RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`0+2=2`] THEN SCS_TAC THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`0`;`4`][Uxckfpe.ARITH_4_TAC] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`2`;`4`][Uxckfpe.ARITH_4_TAC] THEN ASM_SIMP_TAC[DIST_SYM]; MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION] THEN RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`0+2=2`] THEN SCS_TAC THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`1`;`4`][Uxckfpe.ARITH_4_TAC] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`3`;`4`][Uxckfpe.ARITH_4_TAC] THEN ASM_SIMP_TAC[DIST_SYM]; MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION] THEN RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`0+2=2`] THEN SCS_TAC THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`2`;`4`][Uxckfpe.ARITH_4_TAC] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`0`;`4`][Uxckfpe.ARITH_4_TAC] THEN ASM_SIMP_TAC[DIST_SYM]; MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION] THEN RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`0+2=2`] THEN SCS_TAC THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`3`;`4`][Uxckfpe.ARITH_4_TAC] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`1`;`4`][Uxckfpe.ARITH_4_TAC] THEN ASM_SIMP_TAC[DIST_SYM]]);; let EDGE_EQ_2_4I2_2=prove(`main_nonlinear_terminal_v11 ==>(!i j. MMs_v39 scs_4I2 v/\ scs_diag 4 i j /\ &3 <= dist (v i,v j) /\ &3 < dist (v (i + 1),v (j + 1)) ==> dist (v (i+2) ,v (i + 3))= &2)`, REPEAT STRIP_TAC THEN MP_TAC EXPAND_DIAG_4_DIST THEN RESA_TAC THEN THAYTHE_TAC 0[`i`;`j`] THEN MP_TAC EDGE_EQ_2_4I2_1 THEN RESA_TAC THEN THAYTHEL_TAC 0[`i+2`;`i`][ARITH_RULE`SUC(i+2)=i+3/\ (i+2)+1= i+3`] THEN MATCH_DICH_TAC 0 THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[] THEN MP_TAC SCS_DIAG_4_ADD0 THEN REWRITE_TAC[scs_diag] THEN RESA_TAC);; let EDGE_EQ_2_4I2_3=prove(`main_nonlinear_terminal_v11 ==>(!i j. MMs_v39 scs_4I2 v/\ scs_diag 4 i j /\ &3 <= dist (v i,v j) /\ &3 < dist (v (i + 1),v (j + 1)) ==> dist (v (i) ,v (i + 3))= &2)`, REPEAT STRIP_TAC THEN MP_TAC EXPAND_DIAG_4_DIST THEN RESA_TAC THEN THAYTHE_TAC 0[`i`;`j`] THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHES_TAC 0[`1*4+i`;`i`][MOD_MULT_ADD] THEN MP_TAC EDGE_EQ_2_4I2 THEN RESA_TAC THEN THAYTHEL_TAC 0[`i+2`;`i`][ARITH_RULE`SUC(SUC(i+2))=1*4+i/\ SUC (i+2)= i+3/\ (i+2)+1=i+3`] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN MATCH_DICH_TAC 0 THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[] THEN MP_TAC SCS_DIAG_4_ADD0 THEN REWRITE_TAC[scs_diag] THEN RESA_TAC);; let EDGE_EQ_2_4I2_ALL=prove(`main_nonlinear_terminal_v11 ==>( MMs_v39 scs_4I2 v/\ scs_diag 4 i j /\ &3 <= dist (v i,v j) /\ &3 < dist (v (i + 1),v (j + 1)) ==> (!i. dist (v (i) ,v (i+1))= &2))`, REPEAT RESA_TAC THEN MP_TAC EDGE_EQ_2_4I2_3 THEN RESA_TAC THEN THAYTHE_TAC 0[`i`;`j`] THEN MP_TAC EDGE_EQ_2_4I2_2 THEN RESA_TAC THEN THAYTHE_TAC 0[`i`;`j`] THEN MP_TAC EDGE_EQ_2_4I2_1 THEN RESA_TAC THEN THAYTHE_TAC 0[`i`;`j`] THEN MP_TAC EDGE_EQ_2_4I2 THEN RESA_TAC THEN THAYTHE_TAC 0[`i`;`j`] THEN DICH_TAC 0 THEN DICH_TAC 0 THEN DICH_TAC 0 THEN DICH_TAC 0 THEN REWRITE_TAC[ARITH_RULE`SUC i=i+1/\ (i + 1) + 1= i+2`] THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHES_TAC 0[`i`;`i MOD 4`][MOD_REFL;ARITH_RULE`~(4=0)`] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHES_TAC 0[`i+1`;`(i+1) MOD 4`][MOD_REFL;ARITH_RULE`~(4=0)`] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHES_TAC 0[`i+2`;`(i+2) MOD 4`][MOD_REFL;ARITH_RULE`~(4=0)`] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHES_TAC 0[`i+3`;`(i+3) MOD 4`][MOD_REFL;ARITH_RULE`~(4=0)`] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHES_TAC 0[`i'+1`;`(i'+1) MOD 4`][MOD_REFL;ARITH_RULE`~(4=0)`] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHES_TAC 0[`i'`;`(i') MOD 4`][MOD_REFL;ARITH_RULE`~(4=0)`] THEN MRESAL_TAC MOD_ADD_MOD[`i`;`1`;`4`][ARITH_RULE`~(4=0)`] THEN SYM_ASSUM_TAC THEN MRESAL_TAC MOD_ADD_MOD[`i'`;`1`;`4`][ARITH_RULE`~(4=0)`] THEN SYM_ASSUM_TAC THEN MRESAL_TAC MOD_ADD_MOD[`i`;`2`;`4`][ARITH_RULE`~(4=0)`] THEN SYM_ASSUM_TAC THEN MRESAL_TAC MOD_ADD_MOD[`i`;`3`;`4`][ARITH_RULE`~(4=0)`] THEN SYM_ASSUM_TAC THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`i' MOD 4<4==> i' MOD 4=0\/ i' MOD 4=1\/ i' MOD 4=2\/ i' MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`] THEN RESA_TAC THEN ASSUME_TAC(ARITH_RULE`2+1=3/\ 3+1=4/\ 2+3=5/\ 2+2=4/\ 3+3=6/\ 3+2=5/\ 6 MOD 4=2`) THEN SCS_TAC THEN ASM_SIMP_TAC[DIST_SYM]);; let MM_4I2_IMP_4T2_4T1=prove_by_refinement (`main_nonlinear_terminal_v11 ==>(!i j. MMs_v39 scs_4I2 v/\ scs_diag 4 i j /\ dist(v i,v j)<= cstab ==> ~(MMs_v39 (scs_4T1)={})\/ ~(MMs_v39 (scs_4T2)={}))`, [STRIP_TAC THEN MATCH_MP_TAC ASSUME_MIN_DIAG THEN REPEAT RESA_TAC THEN MP_TAC SCS_DIAG_ADD1 THEN RESA_TAC THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN MRESA_TAC SCS_4I2_3_LE_A[`i`;`v`;`j`] THEN MRESA_TAC SCS_4I2_3_LE_A[`i+1`;`v`;`j+1`] THEN MP_TAC SCS_4I2_STRAIGHT_ALL THEN RESA_TAC THEN MP_TAC(REAL_ARITH`&3 <= dist ((v:num->real^3) (i + 1),v (j + 1)) ==> dist (v (i + 1),v (j + 1))= &3\/ &3< dist (v (i + 1),v (j + 1))`) THEN RESA_TAC; MP_TAC(REAL_ARITH`dist (v i,v j) <= dist (v (i + 1),v (j + 1))/\ &3 <= dist ((v:num->real^3) i,v j)/\ dist (v (i + 1),v (j + 1)) = &3 ==> dist ((v:num->real^3) i,v j)= &3`) THEN RESA_TAC THEN MATCH_MP_TAC (SET_RULE`A==> B\/A`) THEN MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN REWRITE_TAC[IN;SET_RULE`~(A={})<=> ?a. a IN A`] THEN STRIP_TAC THEN MATCH_DICH_TAC 0 THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC`scs_4I2` THEN ASM_SIMP_TAC[SCS_4T2_IS_SCS;SCS_4I2_IS_SCS;SCS_4I2_BASIC;SCS_4T2_BASIC;K_SCS_4I2;K_SCS_4T2] THEN STRIP_TAC ; DICH_TAC(14-6) THEN REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4M8_prime;K_SCS_4M8;scs_prop_equ_v39;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN SCS_TAC THEN REWRITE_TAC[ARITH_RULE`~(4<=3)`] THEN REPEAT STRIP_TAC THEN MP_TAC DIST_DIAG_2_CASES_EQ_3 THEN ASM_REWRITE_TAC[IN] THEN DISCH_TAC THEN MP_TAC(SET_RULE`i' MOD 4 = j' MOD 4\/ ~(i' MOD 4 = j' MOD 4)`) THEN RESA_TAC; THAYTHE_TAC 3[`i':num`;`j':num`] ; MP_TAC(SET_RULE`j' MOD 4 = SUC i' MOD 4\/ ~(j' MOD 4 = SUC i' MOD 4)`) THEN RESA_TAC ; THAYTHE_TAC 4[`i':num`;`j':num`] ; MP_TAC(SET_RULE`SUC j' MOD 4 = i' MOD 4\/ ~(SUC j' MOD 4 = i' MOD 4)`) THEN RESA_TAC ; THAYTHE_TAC 5[`i':num`;`j':num`] ; MRESAL_TAC SCS_DIAG_4_CASES[`i'`;`j'`][scs_diag] THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] ; THAYTHEL_ASM_TAC 0[`j'`;`0`][ARITH_RULE`0 MOD 4=0`] THEN THAYTHEL_ASM_TAC 0[`i'`;`2`][ARITH_RULE`2 MOD 4=2`] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[REAL_ARITH`a<=a`]; THAYTHEL_ASM_TAC 0[`j'`;`1`][ARITH_RULE`1 MOD 4=1`] THEN THAYTHEL_ASM_TAC 0[`i'`;`3`][ARITH_RULE`3 MOD 4=3`] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[REAL_ARITH`a<=a`]; THAYTHEL_ASM_TAC 0[`i'`;`0`][ARITH_RULE`0 MOD 4=0`] THEN THAYTHEL_ASM_TAC 0[`j'`;`2`][ARITH_RULE`2 MOD 4=2`] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[REAL_ARITH`a<=a`]; THAYTHEL_ASM_TAC 0[`i'`;`1`][ARITH_RULE`1 MOD 4=1`] THEN THAYTHEL_ASM_TAC 0[`j'`;`3`][ARITH_RULE`3 MOD 4=3`] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[REAL_ARITH`a<=a`]; SCS_TAC THEN REAL_ARITH_TAC; MATCH_MP_TAC(SET_RULE`A==> A\/ B`) THEN MP_TAC EDGE_EQ_2_4I2_ALL THEN RESA_TAC THEN MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN REWRITE_TAC[IN;SET_RULE`~(A={})<=> ?a. a IN A`] THEN STRIP_TAC THEN MATCH_DICH_TAC 0 THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC`scs_4I2` THEN ASM_SIMP_TAC[SCS_4T1_IS_SCS;SCS_4I2_IS_SCS;SCS_4I2_BASIC;SCS_4T1_BASIC;K_SCS_4I2;K_SCS_4T1] THEN STRIP_TAC ; DICH_TAC(14-6) THEN REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4M8_prime;K_SCS_4M8;scs_prop_equ_v39;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN SCS_TAC THEN REWRITE_TAC[ARITH_RULE`~(4<=3)`] THEN REPEAT STRIP_TAC THEN MP_TAC(SET_RULE`i' MOD 4 = j' MOD 4\/ ~(i' MOD 4 = j' MOD 4)`) THEN RESA_TAC; THAYTHE_TAC 2[`i':num`;`j':num`] ; MP_TAC(SET_RULE`j' MOD 4 = SUC i' MOD 4\/ ~(j' MOD 4 = SUC i' MOD 4)`) THEN RESA_TAC ; MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHES_TAC 0[`j'`;`SUC i'`][MOD_REFL;ARITH_RULE`~(4=0)`;ADD1;REAL_ARITH`a<=a`] ; MP_TAC(SET_RULE`SUC j' MOD 4 = i' MOD 4\/ ~(SUC j' MOD 4 = i' MOD 4)`) THEN RESA_TAC ; MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`] THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2] THEN THAYTHES_TAC 0[`i'`;`SUC j'`][MOD_REFL;ARITH_RULE`~(4=0)`;ADD1;REAL_ARITH`a<=a`] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[REAL_ARITH`a<=a`] ; THAYTHE_TAC 4[`i'`;`j'`] ; SCS_TAC THEN REAL_ARITH_TAC ; ]);; let ARDBZYE=prove_by_refinement(`main_nonlinear_terminal_v11 ==> scs_arrow_v39 { scs_4I2 } { scs_4T1, scs_4T2 }`, [ STRIP_TAC THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;SET_RULE`a IN {b,c}<=> a=b\/ a=c`] THEN ABBREV_TAC`k=scs_k_v39 s` THEN REPEAT RESA_TAC; ASM_SIMP_TAC[SCS_4T1_IS_SCS;SCS_4T2_IS_SCS]; ASM_SIMP_TAC[SCS_4T1_IS_SCS;SCS_4T2_IS_SCS]; DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4I2 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4I2 ==> MMs_v39 s = {}))`); ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN] THEN STRIP_TAC; MP_TAC(SET_RULE`(!i j. scs_diag 4 i j ==> cstab < dist(v i,v j))\/ ~((!i j. scs_diag 4 i j ==> cstab < dist((v:num->real^3) i,v j)))`) THEN RESA_TAC; EXISTS_TAC`scs_4T1` THEN ASM_REWRITE_TAC[] THEN MP_TAC SCS_4I2_IMP_SCS_4T1 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN] THEN RESA_TAC THEN MATCH_DICH_TAC 0 THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`v:num->real^3` THEN ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a b<=a`] THEN STRIP_TAC THEN MP_TAC MM_4I2_IMP_4T2_4T1 THEN RESA_TAC THEN THAYTHE_TAC 0[`i`;`j`] THEN DICH_TAC 0 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN] THEN STRIP_TAC; EXISTS_TAC`scs_4T1` THEN REWRITE_TAC[] THEN EXISTS_TAC`v':num->real^3` THEN ASM_REWRITE_TAC[]; EXISTS_TAC`scs_4T2` THEN REWRITE_TAC[] THEN EXISTS_TAC`v':num->real^3` THEN ASM_REWRITE_TAC[]]);; let SCS_4I1_IMP_SCS_4I2= prove_by_refinement (`main_nonlinear_terminal_v11 ==>(!v. v IN MMs_v39 scs_4I1 /\ (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==> ~(MMs_v39 (scs_4I2)={}))`, [ REWRITE_TAC[IN;SET_RULE`~(A={})<=> ?a. a IN A`] THEN REPEAT STRIP_TAC THEN MP_TAC SCS_4I1_IS_SCS THEN STRIP_TAC THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I1`;`v`] THEN ASSUME_TAC SCS_4I1_BASIC THEN ASSUME_TAC K_SCS_4I1 THEN ASSUME_TAC SCS_4I2_BASIC THEN ASSUME_TAC K_SCS_4I2 THEN ASSUME_TAC SCS_4I2_IS_SCS THEN MP_TAC Rrcwnsj.RRCWNSJ THEN RESA_TAC THEN THAYTHES_TAC 0[`scs_4I1`;`v`][ARITH_RULE`3<4`;h0_LT_B_SCS_4I1;B_LE_CSTAB_SCS_4I1] THEN MP_TAC JCYFMRP_V3 THEN RESA_TAC THEN THAYTHES_TAC 0[`scs_4I1`;`v`][ARITH_RULE`3<4`;h0_LT_B_SCS_4I1;B_LE_CSTAB_SCS_4I1;IN;CARD_SCS_M_4I1;GSYM ADD1;A_LT_B_4I1] THEN MP_TAC Jlxfdmj.JLXFDMJ THEN RESA_TAC THEN THAYTHES_TAC 0[`scs_4I1`;`v`;`i`][ARITH_RULE`3<4`;h0_LT_B_SCS_4I1;B_LE_CSTAB_SCS_4I1;IN;CARD_SCS_M_4I1;GSYM ADD1;A_LT_B_4I1;SCS_M_4I1;SET_RULE`~{} (j MOD 4)<=> T`] THEN MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN REWRITE_TAC[IN;SET_RULE`~(A={})<=> ?a. a IN A`] THEN STRIP_TAC THEN MATCH_DICH_TAC 0 THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC`scs_4I1` THEN ASM_SIMP_TAC[SCS_M_4I1] THEN STRIP_TAC; DICH_TAC(13-4) THEN REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4I1;K_SCS_4I2;scs_prop_equ_v39;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN SCS_TAC THEN REWRITE_TAC[ARITH_RULE`~(4<=3)`] THEN REPEAT STRIP_TAC; MP_TAC(SET_RULE`i' MOD 4 = j MOD 4\/ ~(i' MOD 4 = j MOD 4)`) THEN RESA_TAC; THAYTHE_TAC 2[`i'`;`j`]; MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I1`;`v`] THEN MP_TAC(SET_RULE`SUC i' MOD 4 = j MOD 4\/ ~(SUC i' MOD 4 = j MOD 4)`) THEN RESA_TAC; THAYTHE_TAC (19-15)[`i'`;`j`]; MP_TAC(SET_RULE`i' MOD 4 =SUC j MOD 4\/ ~(i' MOD 4 =SUC j MOD 4)`) THEN RESA_TAC; THAYTHE_TAC (20-15)[`i'`;`j`]; THAYTHEL_TAC (20-2)[`i'`;`j`][scs_diag;cstab] THEN DICH_TAC 0 THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC]);; let SCS_4I1_STAB_DIAG=prove_by_refinement(`!v i j. BBs_v39 scs_4I1 v/\ scs_diag 4 i j /\ dist(v i,v j) <= cstab ==> BBs_v39 (scs_stab_diag_v39 scs_4I1 i j) v`, [ REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN DICH_TAC 2 THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASSUME_TAC th THEN MP_TAC th) THEN REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4I1;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I1;Terminal.FUNLIST_EXPLICIT;] THEN ASM_SIMP_TAC[] THEN REPEAT RESA_TAC THEN SCS_TAC THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`) THEN RESA_TAC; MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`j`;`j'`;`i`;`4`][PSORT_5_EXPLICIT]; MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4I1`][SCS_4I1_IS_SCS;K_SCS_4I1] THEN THAYTHE_TAC 0[`i'`;`i`] THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4I1`][SCS_4I1_IS_SCS;K_SCS_4I1] THEN THAYTHE_TAC 0[`j'`;`j`]; MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4I1`][SCS_4I1_IS_SCS;K_SCS_4I1] THEN THAYTHE_TAC 0[`j'`;`i`] THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4I1`][SCS_4I1_IS_SCS;K_SCS_4I1] THEN THAYTHE_TAC 0[`i'`;`j`] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]]);; let STAB_4I1_SCS=prove(` scs_diag (scs_k_v39 scs_4I1) i j ==> is_scs_v39 (scs_stab_diag_v39 scs_4I1 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4I1 i j)`, STRIP_TAC THEN MATCH_MP_TAC Yrtafyh.YRTAFYH THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4I1_IS_SCS;SCS_4I1_BASIC;K_SCS_4I1; ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab] THEN SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC);; let MM_4I1_IMP_STAB_4I1=prove(` MMs_v39 scs_4I1 v/\ scs_diag 4 i j /\ dist(v i,v j) <= cstab ==> ~(MMs_v39 (scs_stab_diag_v39 scs_4I1 i j) ={})`, STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC`scs_4I1` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I1`;`v`] THEN ASSUME_TAC SCS_4I1_BASIC THEN ASSUME_TAC K_SCS_4I1 THEN ASM_SIMP_TAC[SCS_4I1_IS_SCS;STAB_4I1_SCS;K_SCS_4I1;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_4I1_STAB_DIAG] THEN REAL_ARITH_TAC);; let SCS_4I1_ARROW_SCS_4I2_STAB_4I1=prove_by_refinement( `main_nonlinear_terminal_v11 ==> scs_arrow_v39 { scs_4I1 } ({scs_4I2} UNION {scs_stab_diag_v39 scs_4I1 i j| scs_diag 4 i j})`, [STRIP_TAC THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM] THEN ABBREV_TAC`k=scs_k_v39 s` THEN REPEAT RESA_TAC; ASM_SIMP_TAC[SCS_4I2_IS_SCS]; ASM_SIMP_TAC[STAB_4I1_SCS;K_SCS_4I1]; DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4I1 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4I1 ==> MMs_v39 s = {}))`); ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN] THEN STRIP_TAC; MP_TAC(SET_RULE`(!i j. scs_diag 4 i j ==> cstab < dist(v i,v j))\/ ~((!i j. scs_diag 4 i j ==> cstab < dist((v:num->real^3) i,v j)))`) THEN RESA_TAC; EXISTS_TAC`scs_4I2` THEN ASM_REWRITE_TAC[] THEN MP_TAC SCS_4I1_IMP_SCS_4I2 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN] THEN RESA_TAC THEN MATCH_DICH_TAC 0 THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`v:num->real^3` THEN ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a b<=a`] THEN STRIP_TAC THEN MP_TAC MM_4I1_IMP_STAB_4I1 THEN RESA_TAC THEN DICH_TAC 0 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN] THEN STRIP_TAC THEN EXISTS_TAC `scs_stab_diag_v39 scs_4I1 i j` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC; MATCH_MP_TAC(SET_RULE`A==> B\/A`) THEN EXISTS_TAC`i:num` THEN EXISTS_TAC`j:num` THEN ASM_REWRITE_TAC[]; EXISTS_TAC`v':num->real^3` THEN ASM_REWRITE_TAC[]]);; let SET_STAB_4I1=prove(`{ scs_stab_diag_v39 scs_4I1 i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4I1 (i MOD 4) (j MOD 4)| scs_diag 4 (i MOD 4) (j MOD 4) }`, ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;] THEN MRESAL_TAC STAB_MOD[`scs_4I1`][SCS_4I1_IS_SCS;K_SCS_4I1]);; let EXPAND_DIAG_4V=prove_by_refinement( `scs_diag 4 i j <=> j MOD 4= (i+2) MOD 4`, [ EQ_TAC THEN ASM_SIMP_TAC[EXPAND_DIAG_4;] THEN REWRITE_TAC[SCS_DIAG_4_CASES;ARITH_RULE`i+2=SUC(SUC i)`] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`] THEN RESA_TAC; MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`0`;`4`][Uxckfpe.ARITH_4_TAC] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`1`;`4`][Uxckfpe.ARITH_4_TAC]; MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`1`;`4`][Uxckfpe.ARITH_4_TAC] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`2`;`4`][Uxckfpe.ARITH_4_TAC]; MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`2`;`4`][Uxckfpe.ARITH_4_TAC] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`3`;`4`][Uxckfpe.ARITH_4_TAC]; MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`3`;`4`][Uxckfpe.ARITH_4_TAC] THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`4`;`4`][Uxckfpe.ARITH_4_TAC]]);; let EXPAND_STAB_DIAG_4=prove_by_refinement(`is_scs_v39 s /\scs_k_v39 s=4==> {scs_stab_diag_v39 s (i MOD 4) (j MOD 4) | j MOD 4 = (i MOD 4 + 2) MOD 4}= {scs_stab_diag_v39 s (i+2) i| i<4} `, [REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;UNION] THEN STRIP_TAC THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC; MRESAS_TAC STAB_MOD[`s`;`i MOD 4`;`i MOD 4 + 2`][MOD_REFL;ARITH_RULE`~(4=0)`] THEN EXISTS_TAC`i MOD 4` THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`;STAB_SYM]; EXISTS_TAC`i+2` THEN EXISTS_TAC`i:num` THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`;MOD_LT] THEN MRESAS_TAC STAB_MOD[`s`;`(i + 2)`;`i`][SCS_5I1_IS_SCS;K_SCS_5I1;MOD_REFL;ARITH_RULE`~(4=0)`;MOD_LT] THEN MRESAS_TAC MOD_ADD_MOD[`i+2`;`2`;`4`][ARITH_RULE`~(4=0)/\ 2 MOD 4=2/\ (i + 2) + 2= 1*4+i`;MOD_MULT_ADD;MOD_LT]]);; let EXPAND_STAB_DIAG_4I1=prove(` {scs_stab_diag_v39 scs_4I1 (i MOD 4) (j MOD 4) | j MOD 4 = (i MOD 4 + 2) MOD 4}= {scs_stab_diag_v39 scs_4I1 (i+2) i| i<4} `, ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4I1_IS_SCS;K_SCS_4I1]);; let h0_EQ_B_SCS_4I1=prove( `(!i j. scs_diag 4 i j ==> scs_b_v39 scs_4I1 i j= &6) /\ (!i j. scs_diag 4 i j ==> scs_a_v39 scs_4I1 i j= &2 *h0)`, SCS_TAC THEN REWRITE_TAC[h0;scs_diag;cstab] THEN REPEAT RESA_TAC);; let EQ_DIAG_STAB_4I1_02=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4I1 (i + 2) i } {scs_stab_diag_v39 scs_4I1 0 2}`, MRESA_TAC STAB_SYM[`scs_4I1`;`2`;`0`] THEN MP_TAC (GEN_ALL Wkeidft.WKEIDFT) THEN REWRITE_TAC[LET_DEF;LET_END_DEF] THEN STRIP_TAC THEN MATCH_DICH_TAC 0 THEN ASM_SIMP_TAC[ARITH_RULE`2 + i = (i + 2) + 0/\ 3<6/\ i+1= SUC i`;K_SCS_4I1 ;h0_LT_B_SCS_4I1;h0_EQ_B_SCS_4I1;SCS_4I1_IS_SCS;SCS_4I1_BASIC] THEN SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;] THEN EXISTS_TAC`&0` THEN EXISTS_TAC`&2` THEN EXISTS_TAC`&2 *h0` THEN EXISTS_TAC`&2 *h0` THEN EXISTS_TAC`&6` THEN ASM_SIMP_TAC[] THEN MP_TAC SCS_DIAG_4_ADD0 THEN ASM_REWRITE_TAC[scs_diag] THEN RESA_TAC THEN ARITH_TAC);; let SET_EQ_DIAG_STAB_4I1_02=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4I1 (i + 2) i |i<4} {scs_stab_diag_v39 scs_4I1 0 2}`, REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4I1 (i + 2) i |i=0\/i=1\/i=2\/i=3} = {scs_stab_diag_v39 scs_4I1 (0 + 2) 0} UNION {scs_stab_diag_v39 scs_4I1 (1 + 2) 1} UNION {scs_stab_diag_v39 scs_4I1 (2 + 2) 2} UNION {scs_stab_diag_v39 scs_4I1 (3 + 2) 3} `;] THEN REPEAT (ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4I1 0 2}={scs_stab_diag_v39 scs_4I1 0 2} UNION {scs_stab_diag_v39 scs_4I1 0 2}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_SIMP_TAC[EQ_DIAG_STAB_4I1_02]));; let SET_EQ_DIAG_STAB_4I1=prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_4I1 i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4I1 0 2}`, ASM_SIMP_TAC[SET_STAB_4I1] THEN ASM_SIMP_TAC[EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`;EXPAND_STAB_DIAG_4I1;SET_EQ_DIAG_STAB_4I1_02]);; let FYSSVEV= prove(` main_nonlinear_terminal_v11 ==> scs_arrow_v39 { scs_4I1 } {scs_4I2, scs_stab_diag_v39 scs_4I1 0 2 }`, STRIP_TAC THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`({scs_4I2} UNION {scs_stab_diag_v39 scs_4I1 i j| scs_diag 4 i j})` THEN ASM_SIMP_TAC[SCS_4I1_ARROW_SCS_4I2_STAB_4I1;SET_RULE`{A,B}={A}UNION {B}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_4I1] THEN MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[SCS_4I2_IS_SCS]);; end;; (* let check_completeness_claimA_concl = Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) *)