(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Chapter: Local Fan *) (* Author: Hoang Le Truong *) (* Date: 2012-04-01 *) (* ========================================================================= *) (* remaining conclusions from appendix to Local Fan chapter *) module Aueaheh = 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;; open Ardbzye;;let SCS_4I1_SLICE_02=prove_by_refinement( `scs_arrow_v39 {scs_stab_diag_v39 scs_4I1 0 2 } { scs_prop_equ_v39 scs_3M1 1}`,[ONCE_REWRITE_TAC[SET_RULE`{ scs_prop_equ_v39 scs_3M1 1}={ scs_prop_equ_v39 scs_3M1 1, scs_prop_equ_v39 scs_3M1 1}`] THEN MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI) THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4I1_02;STAB_4I1_SCS;SCS_K_D_A_STAB_EQ;] THEN EXISTS_TAC`0` THEN EXISTS_TAC`2` THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4I1_02] THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ] THEN REPEAT RESA_TAC; REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;] THEN STRIP_TAC THEN MATCH_MP_TAC scs_inj THEN ASM_SIMP_TAC[SCS_3M1_BASIC;SCS_4I1_BASIC;J_SCS_4I1;BASIC_HALF_SLICE_STAB;J_SCS_3M1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4I1_BASIC] THEN STRIP_TAC; ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4I1] THEN ARITH_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4I1;scs_3T4_prime;scs_5M3; ARITH_RULE`(2 + 1 + 4 - 0) MOD 4= 3/\ 0 MOD 4=0/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN SCS_TAC THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`] THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`] THEN ASM_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\ 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1) /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\ 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`] THEN SYM_ASSUM_TAC THEN SCS_TAC; ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4I1] THEN ARITH_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4I1;scs_3T4_prime;scs_5M3; ARITH_RULE`(0 + 1 + 4 - 2) MOD 4= 3/\ 2 MOD 4=2/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN SCS_TAC THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`] THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`] THEN ASM_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\ 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1) /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\ 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`] THEN SYM_ASSUM_TAC THEN SCS_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN REWRITE_TAC[J_SCS_3M1]; ]);;(*************************)let AUEAHEH=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4I1 0 2 } {scs_3M1}`,MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_3M1 1}` THEN ASM_REWRITE_TAC[SCS_4I1_SLICE_02] THEN MRESAS_TAC PRO_EQU_ID1[`scs_3M1`;`1`;`3`][SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`(3 - 1 MOD 3)=2`] THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1 1`;`2`][PROP_EQU_IS_SCS;SCS_3M1_IS_SCS] THEN DICH_TAC 0 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th]) THEN REWRITE_TAC[]);;let BB_4I3_IMP_4T4=prove(`!v. BBs_v39 (scs_stab_diag_v39 scs_4I3 1 3) v ==> BBs_v39 (scs_4T4) v`,SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4I3;scs_4T4;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;] THEN REPEAT RESA_TAC THEN THAYTHE_TAC 1[`i`;`j`] THEN DICH_TAC 0 THEN MP_TAC(SET_RULE`psort 4 (i,j) = 1,3\/ ~(psort 4 (i,j) = 1,3)`) THEN RESA_TAC THEN MRESAL_TAC Uaghhbm.CASE_PSORT[`i`;`3`;`j`;`1`;`4`][PSORT_5_EXPLICIT;Uxckfpe.ARITH_4_TAC;PAIR_EQ;cstab] THEN DICH_TAC 0 THEN SCS_TAC THEN RESA_TAC THEN SCS_TAC);;let STAB_4I3_SCS=prove(` scs_diag (scs_k_v39 scs_4I3) i j ==> is_scs_v39 (scs_stab_diag_v39 scs_4I3 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4I3 i j)`,STRIP_TAC THEN MATCH_MP_TAC Yrtafyh.YRTAFYH THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4I3_IS_SCS;SCS_4I3_BASIC;K_SCS_4I3; 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 MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC);;let STAB_4M2_SCS=prove(` scs_diag (scs_k_v39 scs_4M2) i j ==> is_scs_v39 (scs_stab_diag_v39 scs_4M2 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M2 i j)`,STRIP_TAC THEN MATCH_MP_TAC Yrtafyh.YRTAFYH THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M2_IS_SCS;SCS_4M2_BASIC;K_SCS_4M2; 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 MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC);;let STAB_4M3_SCS=prove(` scs_diag (scs_k_v39 scs_4M3') i j ==> is_scs_v39 (scs_stab_diag_v39 scs_4M3' i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M3' i j)`,STRIP_TAC THEN MATCH_MP_TAC Yrtafyh.YRTAFYH THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M3_IS_SCS;SCS_4M3_BASIC;K_SCS_4M3; 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 MP_TAC sqrt8_LE_CSTAB THEN MP_TAC LE_sqrt8_2h0 THEN REAL_ARITH_TAC);;let STAB_4M4_SCS=prove(` scs_diag (scs_k_v39 scs_4M4') i j ==> is_scs_v39 (scs_stab_diag_v39 scs_4M4' i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M4' i j)`,STRIP_TAC THEN MATCH_MP_TAC Yrtafyh.YRTAFYH THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M4_IS_SCS;SCS_4M4_BASIC;K_SCS_4M4; 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 MP_TAC sqrt8_LE_CSTAB THEN MP_TAC LE_sqrt8_2h0 THEN REAL_ARITH_TAC);;let STAB_4M5_SCS=prove(` scs_diag (scs_k_v39 scs_4M5') i j ==> is_scs_v39 (scs_stab_diag_v39 scs_4M5' i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M5' i j)`,STRIP_TAC THEN MATCH_MP_TAC Yrtafyh.YRTAFYH THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M5_IS_SCS;SCS_4M5_BASIC;K_SCS_4M5; 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 MP_TAC sqrt8_LE_CSTAB THEN MP_TAC LE_sqrt8_2h0 THEN REAL_ARITH_TAC);;let STAB_4M6_SCS=prove(` scs_diag (scs_k_v39 scs_4M6') i j ==> is_scs_v39 (scs_stab_diag_v39 scs_4M6' i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M6' i j)`,STRIP_TAC THEN MATCH_MP_TAC Yrtafyh.YRTAFYH THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6; 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 MP_TAC sqrt8_LE_CSTAB THEN MP_TAC LE_sqrt8_2h0 THEN REAL_ARITH_TAC);;let STAB_4M7_SCS=prove(` scs_diag (scs_k_v39 scs_4M7) i j ==> is_scs_v39 (scs_stab_diag_v39 scs_4M7 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M7 i j)`,STRIP_TAC THEN MATCH_MP_TAC Yrtafyh.YRTAFYH THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M7_IS_SCS;SCS_4M7_BASIC;K_SCS_4M7; 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 MP_TAC sqrt8_LE_CSTAB THEN MP_TAC LE_sqrt8_2h0 THEN REAL_ARITH_TAC);;let STAB_4M8_SCS=prove(` scs_diag (scs_k_v39 scs_4M8) i j ==> is_scs_v39 (scs_stab_diag_v39 scs_4M8 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M8 i j)`,STRIP_TAC THEN MATCH_MP_TAC Yrtafyh.YRTAFYH THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M8_IS_SCS;SCS_4M8_BASIC;K_SCS_4M8; 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 MP_TAC sqrt8_LE_CSTAB THEN MP_TAC LE_sqrt8_2h0 THEN REAL_ARITH_TAC);;let MM_4I3_IMP_4T4=prove(`MMs_v39 (scs_stab_diag_v39 scs_4I3 1 3) v ==> ~(MMs_v39 (scs_4T4) ={})`,STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC`(scs_stab_diag_v39 scs_4I3 1 3)` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`(scs_stab_diag_v39 scs_4I3 1 3)`;`v`] THEN ASSUME_TAC SCS_4T4_BASIC THEN ASSUME_TAC K_SCS_4T4 THEN ASM_SIMP_TAC[SCS_4T4_IS_SCS;STAB_4I3_SCS;K_SCS_4I3;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4I3_13;BB_4I3_IMP_4T4] THEN SCS_TAC THEN REAL_ARITH_TAC);;let SCS_4I3_ARROW_4T4 =prove_by_refinement(`scs_arrow_v39 { scs_stab_diag_v39 scs_4I3 1 3 } { scs_4T4 }`,[ REPEAT GEN_TAC THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN] THEN ABBREV_TAC`k=scs_k_v39 s` THEN REPEAT RESA_TAC; ASM_SIMP_TAC[SCS_4T4_IS_SCS]; DISJ_CASES_TAC(SET_RULE`(!s. s = scs_stab_diag_v39 scs_4I3 1 3 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_stab_diag_v39 scs_4I3 1 3 ==> 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 EXISTS_TAC`scs_4T4` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC (GEN_ALL MM_4I3_IMP_4T4) THEN POP_ASSUM MP_TAC THEN SET_TAC[]]);;let PROP_OPP_DIAG_4I3_13=prove_by_refinement(`scs_stab_diag_v39 scs_4I3 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4I3 0 2)) 2 `,[REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;SCS_K_D_A_STAB_EQ;scs_opp_v39] THEN MATCH_MP_TAC scs_inj THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4I3_BASIC;STAB_4I3_SCS;SCS_DIAG_SCS_4I3_13;scs_basic;unadorned_v39;peropp;peropp2] THEN SCS_TAC THEN STRIP_TAC; SET_TAC[]; STRIP_TAC THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN REPEAT GEN_TAC THEN ASSUME_TAC (ARITH_RULE`~(4=0)`) THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`] THEN SYM_ASSUM_TAC THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`] THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`] THEN SYM_ASSUM_TAC THEN SYM_ASSUM_TAC THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/ x' MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_4_TAC;PSORT_5_EXPLICIT;ARITH_RULE`4-1=3/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;let STAB_4I3_02_ARROW_4I3_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4I3 0 2}{scs_stab_diag_v39 scs_4I3 1 3}`,ASM_SIMP_TAC[PROP_OPP_DIAG_4I3_13] THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4I3 0 2)}` THEN STRIP_TAC THENL[ MATCH_MP_TAC (GEN_ALL YXIONXL2) THEN EXISTS_TAC`4` THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4I3;STAB_4I3_SCS;SCS_DIAG_SCS_4I3_02] ; MATCH_MP_TAC(GEN_ALL YXIONXL3) THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS) THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4I3 0 2)` THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4I3;STAB_4I3_SCS;SCS_DIAG_SCS_4I3_02]]);;(******************)let ZNLLLDL=prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_4I3 0 2 } { scs_4T4 }`,MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4I3 1 3}` THEN ASM_SIMP_TAC[STAB_4I3_02_ARROW_4I3_13;SCS_4I3_ARROW_4T4]);;let h0_LT_B_SCS_4I3=prove(` (!i j. scs_diag 4 i j ==> &4 * h0 < scs_b_v39 scs_4I3 i j) /\ (!i j. scs_diag 4 i j ==> scs_a_v39 scs_4I3 i j <= cstab)`,SCS_TAC THEN REWRITE_TAC[h0;SCS_DIAG_4_CASES;cstab] THEN REPEAT RESA_TAC THEN ASSUME_TAC(ARITH_RULE`~(4=0)`) THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`] THEN SYM_ASSUM_TAC THEN SCS_TAC THEN MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC);;let B_LE_CSTAB_SCS_4I3=prove( ` (!i. scs_b_v39 scs_4I3 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 ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`) THEN MRESA_TAC PSORT_MOD[`4`;`i`;`SUC i`] THEN SYM_ASSUM_TAC THEN REWRITE_TAC[ADD1] THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`] 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 SCS_TAC THEN MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC);;let BB_4I3_IMP_BB_4M6=prove (` BBs_v39 scs_4I3 v /\ (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==> BBs_v39 (scs_4M6') v`,SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4I3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6] THEN REPEAT RESA_TAC THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`) THEN SCS_TAC THEN THAYTHE_TAC 1[`i`;`j`] THEN DICH_TAC 0 THEN THAYTHE_TAC 2[`i`;`j`] THEN DICH_TAC 0 THEN DICH_TAC 0 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`] THEN SYM_ASSUM_TAC THEN REWRITE_TAC[ADD1] THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`] THEN SYM_ASSUM_TAC THEN MRESA_TAC MOD_ADD_MOD[`j`;`1`;`4`] 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`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 SCS_TAC THEN MP_TAC sqrt8_LE_CSTAB THEN REWRITE_TAC[cstab;h0] THEN REAL_ARITH_TAC);;let MM_4I3_IMP_4M6=prove(` MMs_v39 scs_4I3 v /\ (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==> ~(MMs_v39 (scs_4M6') ={})`,STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC` scs_4I3 ` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I3 `;`v`] THEN ASSUME_TAC SCS_4M6_BASIC THEN ASSUME_TAC K_SCS_4M6 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4I3_IS_SCS;SCS_4I3_BASIC;K_SCS_4I3;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4I3_13;BB_4I3_IMP_BB_4M6] THEN SCS_TAC THEN REAL_ARITH_TAC);;let BB_4I3_IMP_BB_STAN_4I3=prove(` BBs_v39 scs_4I3 v /\ scs_diag 4 i j /\ dist(v i,v j)<= cstab ==> BBs_v39 (scs_stab_diag_v39 scs_4I3 i j) v`,SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4I3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6] THEN REPEAT RESA_TAC THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`) 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 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`] THENL[ MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I3`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4I3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4I3_IS_SCS] THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][] THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][]; MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I3`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4I3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4I3_IS_SCS] THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][] THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]]);;let MM_4I3_IMP_STAB_4I3=prove(` MMs_v39 scs_4I3 v /\ scs_diag 4 i j /\ dist(v i,v j)<= cstab ==> ~(MMs_v39 (scs_stab_diag_v39 scs_4I3 i j) ={})`,STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC` scs_4I3 ` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I3 `;`v`] THEN ASSUME_TAC SCS_4I3_BASIC THEN ASSUME_TAC K_SCS_4I3 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4I3_IS_SCS;SCS_4I3_BASIC;K_SCS_4I3;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4I3_13;BB_4I3_IMP_BB_STAN_4I3;STAB_4I3_SCS] THEN SCS_TAC THEN REAL_ARITH_TAC);;let SCS_4I3_ARROW_SCS_4M6_STAB_4I3=prove_by_refinement( ` scs_arrow_v39 { scs_4I3 } ({scs_4M6'} UNION {scs_stab_diag_v39 scs_4I3 i j| scs_diag 4 i j})`,[ 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_4M6_IS_SCS]; ASM_SIMP_TAC[STAB_4I3_SCS;K_SCS_4I3]; DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4I3 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4I3 ==> 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_4M6'` THEN ASM_REWRITE_TAC[] THEN MP_TAC MM_4I3_IMP_4M6 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)<=> b<=a`] THEN STRIP_TAC THEN MP_TAC MM_4I3_IMP_STAB_4I3 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_4I3 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_4I3=prove(`{ scs_stab_diag_v39 scs_4I3 i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4I3 (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_4I3`][SCS_4I3_IS_SCS;K_SCS_4I3]);;let EXPAND_STAB_DIAG_4I3=prove(` {scs_stab_diag_v39 scs_4I3 (i MOD 4) (j MOD 4) | j MOD 4 = (i MOD 4 + 2) MOD 4}= {scs_stab_diag_v39 scs_4I3 (i+2) i| i<4} `,let SET_EQ_DIAG_STAB_4I3=prove_by_refinement( `scs_arrow_v39 { scs_stab_diag_v39 scs_4I3 i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4I3 0 2,scs_stab_diag_v39 scs_4I3 1 3}`,[ ASM_SIMP_TAC[EXPAND_STAB_DIAG_4I3;SET_STAB_4I3;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`] THEN REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4I3 (i + 2) i |i=0\/i=1\/i=2\/i=3} = {scs_stab_diag_v39 scs_4I3 (0 + 2) 0} UNION {scs_stab_diag_v39 scs_4I3 (1 + 2) 1} UNION {scs_stab_diag_v39 scs_4I3 (2 + 2) 2} UNION {scs_stab_diag_v39 scs_4I3 (3 + 2) 3} `;] THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4I3 0 2,scs_stab_diag_v39 scs_4I3 1 3}={scs_stab_diag_v39 scs_4I3 0 2} UNION {scs_stab_diag_v39 scs_4I3 1 3}UNION {scs_stab_diag_v39 scs_4I3 0 2} UNION {scs_stab_diag_v39 scs_4I3 1 3}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`] THEN MRESA_TAC STAB_SYM[`scs_4I3`;`0`;`2`] THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4I3_SCS;SCS_DIAG_SCS_4I3_02]; MATCH_MP_TAC FZIOTEF_UNION THEN MRESA_TAC STAB_SYM[`scs_4I3`;`1`;`3`] THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4I3_SCS;SCS_DIAG_SCS_4I3_13]; MATCH_MP_TAC FZIOTEF_UNION THEN MRESAL_TAC STAB_MOD[`scs_4I3`;`4`;`2`][SCS_4I3_IS_SCS;K_SCS_4I3;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`] THEN SYM_ASSUM_TAC THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4I3_SCS;SCS_DIAG_SCS_4I3_02]; MRESAL_TAC STAB_MOD[`scs_4I3`;`5`;`3`][SCS_4I3_IS_SCS;K_SCS_4I3;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`] THEN SYM_ASSUM_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4I3_SCS;SCS_DIAG_SCS_4I3_13]]);;(***********************)let VQFYMZY=prove(` scs_arrow_v39 { scs_4I3 } ({scs_4M6', scs_4T4})`,MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`({scs_4M6'} UNION {scs_stab_diag_v39 scs_4I3 i j| scs_diag 4 i j})` THEN ASM_SIMP_TAC[SCS_4I3_ARROW_SCS_4M6_STAB_4I3;SET_RULE`{a,b}={a}UNION {b}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC THENL[ MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS]; MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4I3 0 2,scs_stab_diag_v39 scs_4I3 1 3}` THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_4I3;SET_RULE`{a,b}={a}UNION {b}`] THEN ONCE_REWRITE_TAC[SET_RULE` {scs_4T4}={scs_4T4} UNION {scs_4T4}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_SIMP_TAC[ZNLLLDL;SCS_4I3_ARROW_4T4]]);;let BB_4M2_IMP_BB_4M6=prove (` BBs_v39 scs_4M2 v /\ (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==> BBs_v39 (scs_4M6') v`,SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M2;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M2;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6] THEN REPEAT RESA_TAC THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`) THEN SCS_TAC THEN THAYTHE_TAC 1[`i`;`j`] THEN DICH_TAC 0 THEN THAYTHE_TAC 2[`i`;`j`] THEN DICH_TAC 0 THEN DICH_TAC 0 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`] THEN SYM_ASSUM_TAC THEN REWRITE_TAC[ADD1] THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`] THEN SYM_ASSUM_TAC THEN MRESA_TAC MOD_ADD_MOD[`j`;`1`;`4`] 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`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 SCS_TAC THEN MP_TAC sqrt8_LE_CSTAB THEN REWRITE_TAC[cstab;h0] THEN REAL_ARITH_TAC);;let MM_4M2_IMP_4M6=prove( ` MMs_v39 scs_4M2 v /\ (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==> ~(MMs_v39 (scs_4M6') ={})`,STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC` scs_4M2 ` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M2 `;`v`] THEN ASSUME_TAC SCS_4M6_BASIC THEN ASSUME_TAC K_SCS_4M6 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M2_IS_SCS;SCS_4M2_BASIC;K_SCS_4M2;SCS_K_D_A_STAB_EQ;IN; ADD1;BB_4M2_IMP_BB_4M6] THEN SCS_TAC THEN REAL_ARITH_TAC);;let BB_4M2_IMP_BB_STAN_4M2=prove( ` BBs_v39 scs_4M2 v /\ scs_diag 4 i j /\ dist(v i,v j)<= cstab ==> BBs_v39 (scs_stab_diag_v39 scs_4M2 i j) v`,SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M2;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M2;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6] THEN REPEAT RESA_TAC THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`) 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 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`] THENL[ MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M2`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M2;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M2;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M2_IS_SCS] THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][] THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][]; MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M2`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M2;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M2;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M2_IS_SCS] THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][] THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]]);;let MM_4M2_IMP_STAB_4M2=prove(` MMs_v39 scs_4M2 v /\ scs_diag 4 i j /\ dist(v i,v j)<= cstab ==> ~(MMs_v39 (scs_stab_diag_v39 scs_4M2 i j) ={})`,STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC` scs_4M2 ` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M2 `;`v`] THEN ASSUME_TAC SCS_4M2_BASIC THEN ASSUME_TAC K_SCS_4M2 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M2_IS_SCS;SCS_4M2_BASIC;K_SCS_4M2;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M2_13;BB_4M2_IMP_BB_STAN_4M2;STAB_4M2_SCS] THEN SCS_TAC THEN REAL_ARITH_TAC);;let SCS_4M2_ARROW_SCS_4M6_STAB_4M2=prove_by_refinement( ` scs_arrow_v39 { scs_4M2 } ({scs_4M6'} UNION {scs_stab_diag_v39 scs_4M2 i j| scs_diag 4 i j})`,[ 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_4M6_IS_SCS]; ASM_SIMP_TAC[STAB_4M2_SCS;K_SCS_4M2]; DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M2 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M2 ==> 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_4M6'` THEN ASM_REWRITE_TAC[] THEN MP_TAC MM_4M2_IMP_4M6 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)<=> b<=a`] THEN STRIP_TAC THEN MP_TAC MM_4M2_IMP_STAB_4M2 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_4M2 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_4M2=prove(`{ scs_stab_diag_v39 scs_4M2 i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M2 (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_4M2`][SCS_4M2_IS_SCS;K_SCS_4M2]);;let EXPAND_STAB_DIAG_4M2=prove(` {scs_stab_diag_v39 scs_4M2 (i MOD 4) (j MOD 4) | j MOD 4 = (i MOD 4 + 2) MOD 4}= {scs_stab_diag_v39 scs_4M2 (i+2) i| i<4} `,let SET_EQ_DIAG_STAB_4M2=prove_by_refinement( `scs_arrow_v39 { scs_stab_diag_v39 scs_4M2 i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4M2 0 2,scs_stab_diag_v39 scs_4M2 1 3}`,[ ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M2;SET_STAB_4M2;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`] THEN REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M2 (i + 2) i |i=0\/i=1\/i=2\/i=3} = {scs_stab_diag_v39 scs_4M2 (0 + 2) 0} UNION {scs_stab_diag_v39 scs_4M2 (1 + 2) 1} UNION {scs_stab_diag_v39 scs_4M2 (2 + 2) 2} UNION {scs_stab_diag_v39 scs_4M2 (3 + 2) 3} `;] THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M2 0 2,scs_stab_diag_v39 scs_4M2 1 3}={scs_stab_diag_v39 scs_4M2 0 2} UNION {scs_stab_diag_v39 scs_4M2 1 3}UNION {scs_stab_diag_v39 scs_4M2 0 2} UNION {scs_stab_diag_v39 scs_4M2 1 3}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`] THEN MRESA_TAC STAB_SYM[`scs_4M2`;`0`;`2`] THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M2_SCS;SCS_DIAG_SCS_4M2_02]; MATCH_MP_TAC FZIOTEF_UNION THEN MRESA_TAC STAB_SYM[`scs_4M2`;`1`;`3`] THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M2_SCS;SCS_DIAG_SCS_4M2_13]; MATCH_MP_TAC FZIOTEF_UNION THEN MRESAL_TAC STAB_MOD[`scs_4M2`;`4`;`2`][SCS_4M2_IS_SCS;K_SCS_4M2;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`] THEN SYM_ASSUM_TAC THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M2_SCS;SCS_DIAG_SCS_4M2_02]; MRESAL_TAC STAB_MOD[`scs_4M2`;`5`;`3`][SCS_4M2_IS_SCS;K_SCS_4M2;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`] THEN SYM_ASSUM_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M2_SCS;SCS_DIAG_SCS_4M2_13]]);;let PROP_OPP_DIAG_4M2_13=prove_by_refinement(`scs_stab_diag_v39 scs_4M2 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4M2 0 2)) 2 `,[REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;SCS_K_D_A_STAB_EQ;scs_opp_v39] THEN MATCH_MP_TAC scs_inj THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M2_BASIC;STAB_4M2_SCS;SCS_DIAG_SCS_4M2_13;scs_basic;unadorned_v39;peropp;peropp2] THEN SCS_TAC THEN STRIP_TAC; SET_TAC[]; STRIP_TAC THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN REPEAT GEN_TAC THEN ASSUME_TAC (ARITH_RULE`~(4=0)`) THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`] THEN SYM_ASSUM_TAC THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`] THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`] THEN SYM_ASSUM_TAC THEN SYM_ASSUM_TAC THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/ x' MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_4_TAC;PSORT_5_EXPLICIT;ARITH_RULE`4-1=3/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;let STAB_4M2_02_ARROW_4M2_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M2 0 2}{scs_stab_diag_v39 scs_4M2 1 3}`,ASM_SIMP_TAC[PROP_OPP_DIAG_4M2_13] THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4M2 0 2)}` THEN STRIP_TAC THENL[ MATCH_MP_TAC (GEN_ALL YXIONXL2) THEN EXISTS_TAC`4` THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M2;STAB_4M2_SCS;SCS_DIAG_SCS_4M2_02] ; MATCH_MP_TAC(GEN_ALL YXIONXL3) THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS) THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4M2 0 2)` THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M2;STAB_4M2_SCS;SCS_DIAG_SCS_4M2_02]]);;let SCS_4M2_SLICE_13=prove_by_refinement( `scs_arrow_v39 {scs_stab_diag_v39 scs_4M2 1 3 } {scs_prop_equ_v39 scs_3M1 1, scs_3T4 }`,[ MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI) THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M2_13;STAB_4M2_SCS;SCS_K_D_A_STAB_EQ;] THEN EXISTS_TAC`1` THEN EXISTS_TAC`3` THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M2_13] THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ] THEN REPEAT RESA_TAC; REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;] THEN STRIP_TAC THEN MATCH_MP_TAC scs_inj THEN ASM_SIMP_TAC[SCS_3T4_BASIC;SCS_4M2_BASIC;J_SCS_4M2;BASIC_HALF_SLICE_STAB;J_SCS_3T4;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3M1_BASIC;J_SCS_3M1] THEN STRIP_TAC; ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2] THEN ARITH_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2; ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN SCS_TAC THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`] THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`] THEN ASM_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\ 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1) /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\ 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`] THEN SYM_ASSUM_TAC THEN SCS_TAC; ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2] THEN ARITH_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2;scs_3T4_prime;scs_5M3; ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN SCS_TAC THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`] THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`] THEN ASM_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\ 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1) /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\ 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`] THEN SYM_ASSUM_TAC THEN SCS_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN REWRITE_TAC[J_SCS_3M1]; ]);;(***************************)let BNAWVNH =prove_by_refinement(` scs_arrow_v39 { scs_4M2 } ({scs_4M6',scs_3M1, scs_3T4})`,[ MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`({scs_4M6'} UNION {scs_stab_diag_v39 scs_4M2 i j| scs_diag 4 i j})` THEN ASM_REWRITE_TAC[SCS_4M2_ARROW_SCS_4M6_STAB_4M2;SET_RULE`{A,B,C}={A}UNION{B,C}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS]; MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M2 0 2,scs_stab_diag_v39 scs_4M2 1 3}` THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M2] THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M2 1 3,scs_stab_diag_v39 scs_4M2 1 3}` THEN STRIP_TAC; REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_REWRITE_TAC[STAB_4M2_02_ARROW_4M2_13]; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M2_SCS;SCS_DIAG_SCS_4M2_13]; REWRITE_TAC[SET_RULE`{A,A}={A}`] THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3M1 1, scs_3T4 }` THEN ASM_REWRITE_TAC[SCS_4M2_SLICE_13;SET_RULE`{A,B}={A}UNION {B}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC; MRESAS_TAC PRO_EQU_ID1[`scs_3M1`;`1`;`3`][SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`(3 - 1 MOD 3)=2`] THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1 1`;`2`][PROP_EQU_IS_SCS;SCS_3M1_IS_SCS] THEN DICH_TAC 0 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th]) THEN REWRITE_TAC[]; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[SCS_3T4_IS_SCS]]);;let BB_4M3_IMP_BB_4M6=prove (` BBs_v39 scs_4M3' v /\ (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==> BBs_v39 (scs_4M6') v`,SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6] THEN REPEAT RESA_TAC THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`) THEN SCS_TAC THEN THAYTHE_TAC 1[`i`;`j`] THEN DICH_TAC 0 THEN THAYTHE_TAC 2[`i`;`j`] THEN DICH_TAC 0 THEN DICH_TAC 0 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`] THEN SYM_ASSUM_TAC THEN REWRITE_TAC[ADD1] THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`] THEN SYM_ASSUM_TAC THEN MRESA_TAC MOD_ADD_MOD[`j`;`1`;`4`] 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`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 SCS_TAC THEN MP_TAC sqrt8_LE_CSTAB THEN MP_TAC LE_sqrt8_2h0 THEN REWRITE_TAC[cstab;h0] THEN REAL_ARITH_TAC);;let MM_4M3_IMP_4M6=prove( ` MMs_v39 scs_4M3' v /\ (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==> ~(MMs_v39 (scs_4M6') ={})`,STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC` scs_4M3' ` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M3' `;`v`] THEN ASSUME_TAC SCS_4M6_BASIC THEN ASSUME_TAC K_SCS_4M6 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M3_IS_SCS;SCS_4M3_BASIC;K_SCS_4M3;SCS_K_D_A_STAB_EQ;IN; ADD1;BB_4M3_IMP_BB_4M6] THEN SCS_TAC THEN REAL_ARITH_TAC);;let BB_4M3_IMP_BB_STAN_4M3=prove( ` BBs_v39 scs_4M3' v /\ scs_diag 4 i j /\ dist(v i,v j)<= cstab ==> BBs_v39 (scs_stab_diag_v39 scs_4M3' i j) v`,SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6] THEN REPEAT RESA_TAC THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`) 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 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`] THENL[ MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M3'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M3_IS_SCS] THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][] THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][]; MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M3'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M3_IS_SCS] THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][] THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]]);;let MM_4M3_IMP_STAB_4M3=prove(` MMs_v39 scs_4M3' v /\ scs_diag 4 i j /\ dist(v i,v j)<= cstab ==> ~(MMs_v39 (scs_stab_diag_v39 scs_4M3' i j) ={})`,STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC` scs_4M3' ` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M3' `;`v`] THEN ASSUME_TAC SCS_4M3_BASIC THEN ASSUME_TAC K_SCS_4M3 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M3_IS_SCS;SCS_4M3_BASIC;K_SCS_4M3;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M3_13;BB_4M3_IMP_BB_STAN_4M3;STAB_4M3_SCS] THEN SCS_TAC THEN REAL_ARITH_TAC);;let SCS_4M3_ARROW_SCS_4M6_STAB_4M3=prove_by_refinement( ` scs_arrow_v39 { scs_4M3' } ({scs_4M6'} UNION {scs_stab_diag_v39 scs_4M3' i j| scs_diag 4 i j})`,[ 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_4M6_IS_SCS]; ASM_SIMP_TAC[STAB_4M3_SCS;K_SCS_4M3]; DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M3' ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M3' ==> 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_4M6'` THEN ASM_REWRITE_TAC[] THEN MP_TAC MM_4M3_IMP_4M6 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)<=> b<=a`] THEN STRIP_TAC THEN MP_TAC MM_4M3_IMP_STAB_4M3 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_4M3' 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_4M3=prove(`{ scs_stab_diag_v39 scs_4M3' i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M3' (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_4M3'`][SCS_4M3_IS_SCS;K_SCS_4M3]);;let EXPAND_STAB_DIAG_4M3=prove(` {scs_stab_diag_v39 scs_4M3' (i MOD 4) (j MOD 4) | j MOD 4 = (i MOD 4 + 2) MOD 4}= {scs_stab_diag_v39 scs_4M3' (i+2) i| i<4} `,let SET_EQ_DIAG_STAB_4M3=prove_by_refinement( `scs_arrow_v39 { scs_stab_diag_v39 scs_4M3' i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4M3' 0 2,scs_stab_diag_v39 scs_4M3' 1 3}`,[ ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M3;SET_STAB_4M3;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`] THEN REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M3' (i + 2) i |i=0\/i=1\/i=2\/i=3} = {scs_stab_diag_v39 scs_4M3' (0 + 2) 0} UNION {scs_stab_diag_v39 scs_4M3' (1 + 2) 1} UNION {scs_stab_diag_v39 scs_4M3' (2 + 2) 2} UNION {scs_stab_diag_v39 scs_4M3' (3 + 2) 3} `;] THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M3' 0 2,scs_stab_diag_v39 scs_4M3' 1 3}={scs_stab_diag_v39 scs_4M3' 0 2} UNION {scs_stab_diag_v39 scs_4M3' 1 3}UNION {scs_stab_diag_v39 scs_4M3' 0 2} UNION {scs_stab_diag_v39 scs_4M3' 1 3}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`] THEN MRESA_TAC STAB_SYM[`scs_4M3'`;`0`;`2`] THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M3_SCS;SCS_DIAG_SCS_4M3_02]; MATCH_MP_TAC FZIOTEF_UNION THEN MRESA_TAC STAB_SYM[`scs_4M3'`;`1`;`3`] THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M3_SCS;SCS_DIAG_SCS_4M3_13]; MATCH_MP_TAC FZIOTEF_UNION THEN MRESAL_TAC STAB_MOD[`scs_4M3'`;`4`;`2`][SCS_4M3_IS_SCS;K_SCS_4M3;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`] THEN SYM_ASSUM_TAC THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M3_SCS;SCS_DIAG_SCS_4M3_02]; MRESAL_TAC STAB_MOD[`scs_4M3'`;`5`;`3`][SCS_4M3_IS_SCS;K_SCS_4M3;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`] THEN SYM_ASSUM_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M3_SCS;SCS_DIAG_SCS_4M3_13]]);;let PROP_OPP_DIAG_4M3_13=prove_by_refinement(`scs_stab_diag_v39 scs_4M3' 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4M3' 0 2)) 2 `,[REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;SCS_K_D_A_STAB_EQ;scs_opp_v39] THEN MATCH_MP_TAC scs_inj THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M3_BASIC;STAB_4M3_SCS;SCS_DIAG_SCS_4M3_13;scs_basic;unadorned_v39;peropp;peropp2] THEN SCS_TAC THEN STRIP_TAC; SET_TAC[]; STRIP_TAC THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN REPEAT GEN_TAC THEN ASSUME_TAC (ARITH_RULE`~(4=0)`) THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`] THEN SYM_ASSUM_TAC THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`] THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`] THEN SYM_ASSUM_TAC THEN SYM_ASSUM_TAC THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/ x' MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_4_TAC;PSORT_5_EXPLICIT;ARITH_RULE`4-1=3/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;let STAB_4M3_02_ARROW_4M3_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M3' 0 2}{scs_stab_diag_v39 scs_4M3' 1 3}`,ASM_SIMP_TAC[PROP_OPP_DIAG_4M3_13] THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4M3' 0 2)}` THEN STRIP_TAC THENL[ MATCH_MP_TAC (GEN_ALL YXIONXL2) THEN EXISTS_TAC`4` THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M3;STAB_4M3_SCS;SCS_DIAG_SCS_4M3_02] ; MATCH_MP_TAC(GEN_ALL YXIONXL3) THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS) THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4M3' 0 2)` THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M3;STAB_4M3_SCS;SCS_DIAG_SCS_4M3_02]]);;let SCS_4M3_SLICE_13=prove_by_refinement( `scs_arrow_v39 {scs_stab_diag_v39 scs_4M3' 1 3 } {scs_prop_equ_v39 scs_3T1 1, scs_prop_equ_v39 scs_3T6' 2}`,[MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI) THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M3_13;STAB_4M3_SCS;SCS_K_D_A_STAB_EQ;] THEN EXISTS_TAC`1` THEN EXISTS_TAC`3` THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M3_13] THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ] THEN REPEAT RESA_TAC; REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;] THEN STRIP_TAC THEN MATCH_MP_TAC scs_inj THEN ASM_SIMP_TAC[SCS_3T1_BASIC;SCS_4M3_BASIC;J_SCS_4M3;BASIC_HALF_SLICE_STAB;J_SCS_3T1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T6_BASIC;J_SCS_3T6] THEN STRIP_TAC; ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M3] THEN ARITH_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M3; ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN SCS_TAC THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`] THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`] THEN ASM_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\ 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1) /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\ 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`] THEN SYM_ASSUM_TAC THEN SCS_TAC; ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T6;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M3] THEN ARITH_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T6;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M3; ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN SCS_TAC THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`] THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`] THEN ASM_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\ 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1) /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\ 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`] THEN SYM_ASSUM_TAC THEN SCS_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN REWRITE_TAC[J_SCS_3T1]; ]);;(************************************)let RAWZDIB =prove_by_refinement( ` scs_arrow_v39 { scs_4M3' } ({scs_4M6',scs_3T1, scs_3T6'})`,[ MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`({scs_4M6'} UNION {scs_stab_diag_v39 scs_4M3' i j| scs_diag 4 i j})` THEN ASM_REWRITE_TAC[SCS_4M3_ARROW_SCS_4M6_STAB_4M3;SET_RULE`{A,B,C}={A}UNION{B,C}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS]; MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M3' 0 2,scs_stab_diag_v39 scs_4M3' 1 3}` THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M3] THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M3' 1 3,scs_stab_diag_v39 scs_4M3' 1 3}` THEN STRIP_TAC; REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_REWRITE_TAC[STAB_4M3_02_ARROW_4M3_13]; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M3_SCS;SCS_DIAG_SCS_4M3_13]; REWRITE_TAC[SET_RULE`{A,A}={A}`] THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3T1 1, scs_prop_equ_v39 scs_3T6' 2}` THEN ASM_REWRITE_TAC[SCS_4M3_SLICE_13;SET_RULE`{A,B}={A}UNION {B}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC; MRESAS_TAC PRO_EQU_ID1[`scs_3T1`;`1`;`3`][SCS_3T1_IS_SCS;K_SCS_3T1;ARITH_RULE`(3 - 1 MOD 3)=2`] THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T1 1`;`2`][PROP_EQU_IS_SCS;SCS_3T1_IS_SCS] THEN DICH_TAC 0 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th]) THEN REWRITE_TAC[]; MRESAS_TAC PRO_EQU_ID1[`scs_3T6'`;`2`;`3`][SCS_3T6_IS_SCS;K_SCS_3T6;ARITH_RULE`(3 - 2 MOD 3)=1`] THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T6' 2`;`1`][PROP_EQU_IS_SCS;SCS_3T6_IS_SCS] THEN DICH_TAC 0 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th]) THEN REWRITE_TAC[]]);;let BB_4M4_IMP_BB_4M7=prove (` BBs_v39 scs_4M4' v /\ (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==> BBs_v39 (scs_4M7) v`,SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M4;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M4;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7] THEN REPEAT RESA_TAC THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`) THEN SCS_TAC THEN THAYTHE_TAC 1[`i`;`j`] THEN DICH_TAC 0 THEN THAYTHE_TAC 2[`i`;`j`] THEN DICH_TAC 0 THEN DICH_TAC 0 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`] THEN SYM_ASSUM_TAC THEN REWRITE_TAC[ADD1] THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`] THEN SYM_ASSUM_TAC THEN MRESA_TAC MOD_ADD_MOD[`j`;`1`;`4`] 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`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 SCS_TAC THEN MP_TAC sqrt8_LE_CSTAB THEN MP_TAC LE_sqrt8_2h0 THEN REWRITE_TAC[cstab;h0] THEN REAL_ARITH_TAC);;let MM_4M4_IMP_4M7=prove( ` MMs_v39 scs_4M4' v /\ (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==> ~(MMs_v39 (scs_4M7) ={})`,STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC` scs_4M4' ` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M4' `;`v`] THEN ASSUME_TAC SCS_4M7_BASIC THEN ASSUME_TAC K_SCS_4M7 THEN ASM_SIMP_TAC[SCS_4M7_IS_SCS;SCS_4M4_IS_SCS;SCS_4M4_BASIC;K_SCS_4M4;SCS_K_D_A_STAB_EQ;IN; ADD1;BB_4M4_IMP_BB_4M7] THEN SCS_TAC THEN REAL_ARITH_TAC);;let BB_4M4_IMP_BB_STAN_4M4=prove( ` BBs_v39 scs_4M4' v /\ scs_diag 4 i j /\ dist(v i,v j)<= cstab ==> BBs_v39 (scs_stab_diag_v39 scs_4M4' i j) v`,SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M4;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M4;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7] THEN REPEAT RESA_TAC THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`) 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 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`] THENL[ MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M4'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M4;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M4;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7;SCS_4M4_IS_SCS] THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][] THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][]; MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M4'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M4;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M4;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7;SCS_4M4_IS_SCS] THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][] THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]]);;let MM_4M4_IMP_STAB_4M4=prove(` MMs_v39 scs_4M4' v /\ scs_diag 4 i j /\ dist(v i,v j)<= cstab ==> ~(MMs_v39 (scs_stab_diag_v39 scs_4M4' i j) ={})`,STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC` scs_4M4' ` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M4' `;`v`] THEN ASSUME_TAC SCS_4M4_BASIC THEN ASSUME_TAC K_SCS_4M4 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M4_IS_SCS;SCS_4M4_BASIC;K_SCS_4M4;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M4_13;BB_4M4_IMP_BB_STAN_4M4;STAB_4M4_SCS] THEN SCS_TAC THEN REAL_ARITH_TAC);;let SCS_4M4_ARROW_SCS_4M7_STAB_4M4=prove_by_refinement( ` scs_arrow_v39 { scs_4M4' } ({scs_4M7} UNION {scs_stab_diag_v39 scs_4M4' i j| scs_diag 4 i j})`,[ 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_4M7_IS_SCS]; ASM_SIMP_TAC[STAB_4M4_SCS;K_SCS_4M4]; DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M4' ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M4' ==> 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_4M7` THEN ASM_REWRITE_TAC[] THEN MP_TAC MM_4M4_IMP_4M7 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)<=> b<=a`] THEN STRIP_TAC THEN MP_TAC MM_4M4_IMP_STAB_4M4 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_4M4' 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_4M4=prove(`{ scs_stab_diag_v39 scs_4M4' i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M4' (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_4M4'`][SCS_4M4_IS_SCS;K_SCS_4M4]);;let EXPAND_STAB_DIAG_4M4=prove(` {scs_stab_diag_v39 scs_4M4' (i MOD 4) (j MOD 4) | j MOD 4 = (i MOD 4 + 2) MOD 4}= {scs_stab_diag_v39 scs_4M4' (i+2) i| i<4} `,let SET_EQ_DIAG_STAB_4M4=prove_by_refinement( `scs_arrow_v39 { scs_stab_diag_v39 scs_4M4' i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4M4' 0 2,scs_stab_diag_v39 scs_4M4' 1 3}`,[ ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M4;SET_STAB_4M4;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`] THEN REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M4' (i + 2) i |i=0\/i=1\/i=2\/i=3} = {scs_stab_diag_v39 scs_4M4' (0 + 2) 0} UNION {scs_stab_diag_v39 scs_4M4' (1 + 2) 1} UNION {scs_stab_diag_v39 scs_4M4' (2 + 2) 2} UNION {scs_stab_diag_v39 scs_4M4' (3 + 2) 3} `;] THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M4' 0 2,scs_stab_diag_v39 scs_4M4' 1 3}={scs_stab_diag_v39 scs_4M4' 0 2} UNION {scs_stab_diag_v39 scs_4M4' 1 3}UNION {scs_stab_diag_v39 scs_4M4' 0 2} UNION {scs_stab_diag_v39 scs_4M4' 1 3}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`] THEN MRESA_TAC STAB_SYM[`scs_4M4'`;`0`;`2`] THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M4_SCS;SCS_DIAG_SCS_4M4_02]; MATCH_MP_TAC FZIOTEF_UNION THEN MRESA_TAC STAB_SYM[`scs_4M4'`;`1`;`3`] THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M4_SCS;SCS_DIAG_SCS_4M4_13]; MATCH_MP_TAC FZIOTEF_UNION THEN MRESAL_TAC STAB_MOD[`scs_4M4'`;`4`;`2`][SCS_4M4_IS_SCS;K_SCS_4M4;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`] THEN SYM_ASSUM_TAC THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M4_SCS;SCS_DIAG_SCS_4M4_02]; MRESAL_TAC STAB_MOD[`scs_4M4'`;`5`;`3`][SCS_4M4_IS_SCS;K_SCS_4M4;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`] THEN SYM_ASSUM_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M4_SCS;SCS_DIAG_SCS_4M4_13]]);;let SCS_4M4_SLICE_13=prove_by_refinement( `scs_arrow_v39 {scs_stab_diag_v39 scs_4M4' 1 3 } {scs_prop_equ_v39 scs_3T4 2, scs_3T4 }`,[ MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI) THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M4_13;STAB_4M4_SCS;SCS_K_D_A_STAB_EQ;] THEN EXISTS_TAC`1` THEN EXISTS_TAC`3` THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M4_13] THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ] THEN REPEAT RESA_TAC; REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;] THEN STRIP_TAC THEN MATCH_MP_TAC scs_inj THEN ASM_SIMP_TAC[SCS_3T4_BASIC;SCS_4M4_BASIC;J_SCS_4M4;BASIC_HALF_SLICE_STAB;J_SCS_3T4;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T6_BASIC;J_SCS_3T6] THEN STRIP_TAC; ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4] THEN ARITH_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4; ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN SCS_TAC THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`] THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`] THEN ASM_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\ 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1) /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\ 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`] THEN SYM_ASSUM_TAC THEN SCS_TAC; ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4] THEN ARITH_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4; ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN SCS_TAC THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`] THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`] THEN ASM_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\ 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1) /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\ 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`] THEN SYM_ASSUM_TAC THEN SCS_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN REWRITE_TAC[J_SCS_3T4]; ]);;let SCS_4M4_SLICE_02=prove_by_refinement( `scs_arrow_v39 {scs_stab_diag_v39 scs_4M4' 0 2 } { scs_3T3, scs_prop_equ_v39 scs_3M1 1 }`,[ MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI) THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M4_02;STAB_4M4_SCS;SCS_K_D_A_STAB_EQ;] THEN EXISTS_TAC`0` THEN EXISTS_TAC`2` THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M4_02] THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ] THEN REPEAT RESA_TAC; REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;] THEN STRIP_TAC THEN MATCH_MP_TAC scs_inj THEN ASM_SIMP_TAC[SCS_3T3_BASIC;SCS_4M4_BASIC;J_SCS_4M4;BASIC_HALF_SLICE_STAB;J_SCS_3T3;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3M1_BASIC;J_SCS_3M1;J_SCS_3T3_1] THEN STRIP_TAC; ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T3;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4] THEN ARITH_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4; ARITH_RULE`(2 + 1 + 4 - 0) MOD 4= 3/\ 0 MOD 4=0/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN SCS_TAC THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`] THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`] THEN ASM_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\ 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1) /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\ 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`] THEN SYM_ASSUM_TAC THEN SCS_TAC; ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4] THEN ARITH_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4; ARITH_RULE`(0 + 1 + 4 - 2) MOD 4= 3/\ 2 MOD 4=2/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN SCS_TAC THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`] THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`] THEN ASM_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\ 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1) /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\ 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`] THEN SYM_ASSUM_TAC THEN SCS_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN REWRITE_TAC[J_SCS_3T3_1]; ]);;(************************************)let MFKLVDK =prove_by_refinement( ` scs_arrow_v39 { scs_4M4' } ({scs_4M7,scs_3T3, scs_3M1, scs_3T4})`,[ MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`({scs_4M7} UNION {scs_stab_diag_v39 scs_4M4' i j| scs_diag 4 i j})` THEN ASM_REWRITE_TAC[SCS_4M4_ARROW_SCS_4M7_STAB_4M4;SET_RULE`{A,B,C,D}={A}UNION{B,C,D}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[SCS_4M7_IS_SCS]; MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M4' 0 2,scs_stab_diag_v39 scs_4M4' 1 3}` THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M4;SET_RULE`{A,B}={A} UNION {B}/\ {A,B,C}={A,B}UNION {C}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC; REWRITE_TAC[SET_RULE`{A}UNION {B}={A,B}`] THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_3T3, scs_prop_equ_v39 scs_3M1 1}` THEN ASM_SIMP_TAC[SCS_4M4_SLICE_02] THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION {B}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[SCS_3T3_IS_SCS]; MRESAS_TAC PRO_EQU_ID1[`scs_3M1`;`1`;`3`][SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`(3 - 1 MOD 3)=2`] THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1 1`;`2`][PROP_EQU_IS_SCS;SCS_3M1_IS_SCS] THEN DICH_TAC 0 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th]) THEN REWRITE_TAC[]; MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3T4 2, scs_3T4 }` THEN ASM_SIMP_TAC[SCS_4M4_SLICE_13;] THEN ONCE_REWRITE_TAC[SET_RULE`{A}={A}UNION {A}/\ {A,B}={A} UNION {B}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC; MRESAS_TAC PRO_EQU_ID1[`scs_3T4`;`2`;`3`][SCS_3T4_IS_SCS;K_SCS_3T4;ARITH_RULE`(3 - 2 MOD 3)=1`] THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T4 2`;`1`][PROP_EQU_IS_SCS;SCS_3T4_IS_SCS] THEN DICH_TAC 0 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th]) THEN REWRITE_TAC[]; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[SCS_3T4_IS_SCS]]);;let BB_4M5_IMP_BB_4M8=prove (` BBs_v39 scs_4M5' v /\ (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==> BBs_v39 (scs_4M8) v`,SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M5;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M5;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8] THEN REPEAT RESA_TAC THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`) THEN SCS_TAC THEN THAYTHE_TAC 1[`i`;`j`] THEN DICH_TAC 0 THEN THAYTHE_TAC 2[`i`;`j`] THEN DICH_TAC 0 THEN DICH_TAC 0 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`] THEN SYM_ASSUM_TAC THEN REWRITE_TAC[ADD1] THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`] THEN SYM_ASSUM_TAC THEN MRESA_TAC MOD_ADD_MOD[`j`;`1`;`4`] 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`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 SCS_TAC THEN MP_TAC sqrt8_LE_CSTAB THEN MP_TAC LE_sqrt8_2h0 THEN REWRITE_TAC[cstab;h0] THEN REAL_ARITH_TAC);;let MM_4M5_IMP_4M8=prove( ` MMs_v39 scs_4M5' v /\ (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==> ~(MMs_v39 (scs_4M8) ={})`,STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC` scs_4M5' ` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M5' `;`v`] THEN ASSUME_TAC SCS_4M8_BASIC THEN ASSUME_TAC K_SCS_4M8 THEN ASM_SIMP_TAC[SCS_4M8_IS_SCS;SCS_4M5_IS_SCS;SCS_4M5_BASIC;K_SCS_4M5;SCS_K_D_A_STAB_EQ;IN; ADD1;BB_4M5_IMP_BB_4M8] THEN SCS_TAC THEN REAL_ARITH_TAC);;let BB_4M5_IMP_BB_STAN_4M5=prove( ` BBs_v39 scs_4M5' v /\ scs_diag 4 i j /\ dist(v i,v j)<= cstab ==> BBs_v39 (scs_stab_diag_v39 scs_4M5' i j) v`,SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M5;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M5;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8] THEN REPEAT RESA_TAC THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`) 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 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`] THENL[ MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M5'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M5;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M5;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8;SCS_4M5_IS_SCS] THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][] THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][]; MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M5'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M5;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M5;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8;SCS_4M5_IS_SCS] THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][] THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]]);;let MM_4M5_IMP_STAB_4M5=prove(` MMs_v39 scs_4M5' v /\ scs_diag 4 i j /\ dist(v i,v j)<= cstab ==> ~(MMs_v39 (scs_stab_diag_v39 scs_4M5' i j) ={})`,STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC` scs_4M5' ` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M5' `;`v`] THEN ASSUME_TAC SCS_4M5_BASIC THEN ASSUME_TAC K_SCS_4M5 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M5_IS_SCS;SCS_4M5_BASIC;K_SCS_4M5;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M5_13;BB_4M5_IMP_BB_STAN_4M5;STAB_4M5_SCS] THEN SCS_TAC THEN REAL_ARITH_TAC);;let SCS_4M5_ARROW_SCS_4M8_STAB_4M5=prove_by_refinement( ` scs_arrow_v39 { scs_4M5' } ({scs_4M8} UNION {scs_stab_diag_v39 scs_4M5' i j| scs_diag 4 i j})`,[ 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_4M8_IS_SCS]; ASM_SIMP_TAC[STAB_4M5_SCS;K_SCS_4M5]; DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M5' ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M5' ==> 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_4M8` THEN ASM_REWRITE_TAC[] THEN MP_TAC MM_4M5_IMP_4M8 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)<=> b<=a`] THEN STRIP_TAC THEN MP_TAC MM_4M5_IMP_STAB_4M5 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_4M5' 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_4M5=prove(`{ scs_stab_diag_v39 scs_4M5' i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M5' (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_4M5'`][SCS_4M5_IS_SCS;K_SCS_4M5]);;let EXPAND_STAB_DIAG_4M5=prove(` {scs_stab_diag_v39 scs_4M5' (i MOD 4) (j MOD 4) | j MOD 4 = (i MOD 4 + 2) MOD 4}= {scs_stab_diag_v39 scs_4M5' (i+2) i| i<4} `,let SET_EQ_DIAG_STAB_4M5=prove_by_refinement( `scs_arrow_v39 { scs_stab_diag_v39 scs_4M5' i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4M5' 0 2,scs_stab_diag_v39 scs_4M5' 1 3}`,[ ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M5;SET_STAB_4M5;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`] THEN REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M5' (i + 2) i |i=0\/i=1\/i=2\/i=3} = {scs_stab_diag_v39 scs_4M5' (0 + 2) 0} UNION {scs_stab_diag_v39 scs_4M5' (1 + 2) 1} UNION {scs_stab_diag_v39 scs_4M5' (2 + 2) 2} UNION {scs_stab_diag_v39 scs_4M5' (3 + 2) 3} `;] THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M5' 0 2,scs_stab_diag_v39 scs_4M5' 1 3}={scs_stab_diag_v39 scs_4M5' 0 2} UNION {scs_stab_diag_v39 scs_4M5' 1 3}UNION {scs_stab_diag_v39 scs_4M5' 0 2} UNION {scs_stab_diag_v39 scs_4M5' 1 3}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`] THEN MRESA_TAC STAB_SYM[`scs_4M5'`;`0`;`2`] THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M5_SCS;SCS_DIAG_SCS_4M5_02]; MATCH_MP_TAC FZIOTEF_UNION THEN MRESA_TAC STAB_SYM[`scs_4M5'`;`1`;`3`] THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M5_SCS;SCS_DIAG_SCS_4M5_13]; MATCH_MP_TAC FZIOTEF_UNION THEN MRESAL_TAC STAB_MOD[`scs_4M5'`;`4`;`2`][SCS_4M5_IS_SCS;K_SCS_4M5;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`] THEN SYM_ASSUM_TAC THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M5_SCS;SCS_DIAG_SCS_4M5_02]; MRESAL_TAC STAB_MOD[`scs_4M5'`;`5`;`3`][SCS_4M5_IS_SCS;K_SCS_4M5;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`] THEN SYM_ASSUM_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M5_SCS;SCS_DIAG_SCS_4M5_13]]);;let PROP_OPP_DIAG_4M5_13=prove_by_refinement(`scs_stab_diag_v39 scs_4M5' 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4M5' 0 2)) 2 `,[REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;SCS_K_D_A_STAB_EQ;scs_opp_v39] THEN MATCH_MP_TAC scs_inj THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M5_BASIC;STAB_4M5_SCS;SCS_DIAG_SCS_4M5_13;scs_basic;unadorned_v39;peropp;peropp2] THEN SCS_TAC THEN STRIP_TAC; SET_TAC[]; STRIP_TAC THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN REPEAT GEN_TAC THEN ASSUME_TAC (ARITH_RULE`~(4=0)`) THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`] THEN SYM_ASSUM_TAC THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`] THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`] THEN SYM_ASSUM_TAC THEN SYM_ASSUM_TAC THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/ x' MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_4_TAC;PSORT_5_EXPLICIT;ARITH_RULE`4-1=3/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;let STAB_4M5_02_ARROW_4M5_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M5' 0 2}{scs_stab_diag_v39 scs_4M5' 1 3}`,ASM_SIMP_TAC[PROP_OPP_DIAG_4M5_13] THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4M5' 0 2)}` THEN STRIP_TAC THENL[ MATCH_MP_TAC (GEN_ALL YXIONXL2) THEN EXISTS_TAC`4` THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M5;STAB_4M5_SCS;SCS_DIAG_SCS_4M5_02] ; MATCH_MP_TAC(GEN_ALL YXIONXL3) THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS) THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4M5' 0 2)` THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M5;STAB_4M5_SCS;SCS_DIAG_SCS_4M5_02]]);;let SCS_4M5_SLICE_13=prove_by_refinement( `scs_arrow_v39 {scs_stab_diag_v39 scs_4M5' 1 3 } {scs_3T4}`,[ ONCE_REWRITE_TAC[SET_RULE`{scs_3T4}={scs_3T4,scs_3T4}`] THEN MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI) THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M5_13;STAB_4M5_SCS;SCS_K_D_A_STAB_EQ;] THEN EXISTS_TAC`1` THEN EXISTS_TAC`3` THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M5_13] THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ] THEN REPEAT RESA_TAC; REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;] THEN STRIP_TAC THEN MATCH_MP_TAC scs_inj THEN ASM_SIMP_TAC[SCS_3T4_BASIC;SCS_4M5_BASIC;J_SCS_4M5;BASIC_HALF_SLICE_STAB;J_SCS_3T4_1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T6_BASIC;J_SCS_3T6] THEN STRIP_TAC; ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M5] THEN ARITH_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M5; ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN SCS_TAC THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`] THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`] THEN ASM_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\ 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1) /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\ 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`] THEN SYM_ASSUM_TAC THEN SCS_TAC; ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M5] THEN ARITH_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T6;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M5; ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN SCS_TAC THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`] THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`] THEN ASM_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\ 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1) /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\ 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`] THEN SYM_ASSUM_TAC THEN SCS_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN REWRITE_TAC[J_SCS_3T4_1]; ]);;(******** NWDGKXH CASES EQ cstab*******************)let RYPDIXT =prove_by_refinement( ` scs_arrow_v39 { scs_4M5' } ({scs_4M8,scs_3T4})`,[ MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`({scs_4M8} UNION {scs_stab_diag_v39 scs_4M5' i j| scs_diag 4 i j})` THEN ASM_REWRITE_TAC[SCS_4M5_ARROW_SCS_4M8_STAB_4M5;SET_RULE`{A,B}={A}UNION{B}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[SCS_4M8_IS_SCS]; MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M5' 0 2,scs_stab_diag_v39 scs_4M5' 1 3}` THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M5] THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M5' 1 3,scs_stab_diag_v39 scs_4M5' 1 3}` THEN STRIP_TAC; REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_REWRITE_TAC[STAB_4M5_02_ARROW_4M5_13]; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M5_SCS;SCS_DIAG_SCS_4M5_13]; REWRITE_TAC[SET_RULE`{A,A}={A}`;SCS_4M5_SLICE_13]; ]);;let BB_4M6_IMP_4T5=prove(`!v. BBs_v39 (scs_stab_diag_v39 scs_4M6' 1 3) v ==> BBs_v39 (scs_4T5) v`,SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M6;scs_4T5;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;] THEN REPEAT RESA_TAC THEN THAYTHE_TAC 1[`i`;`j`] THEN DICH_TAC 0 THEN MP_TAC(SET_RULE`psort 4 (i,j) = 1,3\/ ~(psort 4 (i,j) = 1,3)`) THEN RESA_TAC THEN MRESAL_TAC Uaghhbm.CASE_PSORT[`i`;`3`;`j`;`1`;`4`][PSORT_5_EXPLICIT;Uxckfpe.ARITH_4_TAC;PAIR_EQ;cstab] THEN DICH_TAC 0 THEN SCS_TAC THEN RESA_TAC THEN SCS_TAC);;let MM_4M6_IMP_4T5=prove( `MMs_v39 (scs_stab_diag_v39 scs_4M6' 1 3) v ==> ~(MMs_v39 (scs_4T5) ={})`,STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC`(scs_stab_diag_v39 scs_4M6' 1 3)` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`(scs_stab_diag_v39 scs_4M6' 1 3)`;`v`] THEN ASSUME_TAC SCS_4T5_BASIC THEN ASSUME_TAC K_SCS_4T5 THEN ASM_SIMP_TAC[SCS_4T5_IS_SCS;STAB_4M6_SCS;K_SCS_4M6;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M6_13;BB_4M6_IMP_4T5] THEN SCS_TAC THEN REAL_ARITH_TAC);;let STAB_4M6_13_ARROW_4T5=prove_by_refinement( ` scs_arrow_v39 { scs_stab_diag_v39 scs_4M6' 1 3 } {scs_4T5}`,[ 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_4T5_IS_SCS]; DISJ_CASES_TAC(SET_RULE`(!s. s = scs_stab_diag_v39 scs_4M6' 1 3 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_stab_diag_v39 scs_4M6' 1 3 ==> 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 REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN] THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN STRIP_TAC THEN EXISTS_TAC`scs_4T5` THEN ASM_REWRITE_TAC[] THEN MP_TAC MM_4M6_IMP_4T5 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN] THEN RESA_TAC]);;let PROP_OPP_DIAG_4M6_13=prove_by_refinement(`scs_stab_diag_v39 scs_4M6' 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4M6' 0 2)) 2 `,[REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;SCS_K_D_A_STAB_EQ;scs_opp_v39] THEN MATCH_MP_TAC scs_inj THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M6_BASIC;STAB_4M6_SCS;SCS_DIAG_SCS_4M6_13;scs_basic;unadorned_v39;peropp;peropp2] THEN SCS_TAC THEN STRIP_TAC; SET_TAC[]; STRIP_TAC THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN REPEAT GEN_TAC THEN ASSUME_TAC (ARITH_RULE`~(4=0)`) THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`] THEN SYM_ASSUM_TAC THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`] THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`] THEN SYM_ASSUM_TAC THEN SYM_ASSUM_TAC THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/ x' MOD 4=3`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_4_TAC;PSORT_5_EXPLICIT;ARITH_RULE`4-1=3/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;let STAB_4M6_02_ARROW_4M6_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M6' 0 2}{scs_stab_diag_v39 scs_4M6' 1 3}`,ASM_SIMP_TAC[PROP_OPP_DIAG_4M6_13] THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4M6' 0 2)}` THEN STRIP_TAC THENL[ MATCH_MP_TAC (GEN_ALL YXIONXL2) THEN EXISTS_TAC`4` THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M6;STAB_4M6_SCS;SCS_DIAG_SCS_4M6_02] ; MATCH_MP_TAC(GEN_ALL YXIONXL3) THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS) THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4M6' 0 2)` THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M6;STAB_4M6_SCS;SCS_DIAG_SCS_4M6_02]]);;let STAB_4M6_02_ARROW_4T5 =prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_4M6' 0 2 } { scs_4T5 }`,MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M6' 1 3}` THEN ASM_SIMP_TAC[STAB_4M6_02_ARROW_4M6_13;STAB_4M6_13_ARROW_4T5]);;let SET_STAB_4M6=prove(`{ scs_stab_diag_v39 scs_4M6' i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M6' (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_4M6'`][SCS_4M6_IS_SCS;K_SCS_4M6]);;let EXPAND_STAB_DIAG_4M6=prove(` {scs_stab_diag_v39 scs_4M6' (i MOD 4) (j MOD 4) | j MOD 4 = (i MOD 4 + 2) MOD 4}= {scs_stab_diag_v39 scs_4M6' (i+2) i| i<4} `,let SET_EQ_DIAG_STAB_4M6=prove_by_refinement(`scs_arrow_v39 { scs_stab_diag_v39 scs_4M6' i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4M6' 0 2,scs_stab_diag_v39 scs_4M6' 1 3}`,[ ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M6;SET_STAB_4M6;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`] THEN REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M6' (i + 2) i |i=0\/i=1\/i=2\/i=3} = {scs_stab_diag_v39 scs_4M6' (0 + 2) 0} UNION {scs_stab_diag_v39 scs_4M6' (1 + 2) 1} UNION {scs_stab_diag_v39 scs_4M6' (2 + 2) 2} UNION {scs_stab_diag_v39 scs_4M6' (3 + 2) 3} `;] THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M6' 0 2,scs_stab_diag_v39 scs_4M6' 1 3}={scs_stab_diag_v39 scs_4M6' 0 2} UNION {scs_stab_diag_v39 scs_4M6' 1 3}UNION {scs_stab_diag_v39 scs_4M6' 0 2} UNION {scs_stab_diag_v39 scs_4M6' 1 3}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`] THEN MRESA_TAC STAB_SYM[`scs_4M6'`;`0`;`2`] THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M6_SCS;SCS_DIAG_SCS_4M6_02]; MATCH_MP_TAC FZIOTEF_UNION THEN MRESA_TAC STAB_SYM[`scs_4M6'`;`1`;`3`] THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M6_SCS;SCS_DIAG_SCS_4M6_13]; MATCH_MP_TAC FZIOTEF_UNION THEN MRESAL_TAC STAB_MOD[`scs_4M6'`;`4`;`2`][SCS_4M6_IS_SCS;K_SCS_4M6;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`] THEN SYM_ASSUM_TAC THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M6_SCS;SCS_DIAG_SCS_4M6_02]; MRESAL_TAC STAB_MOD[`scs_4M6'`;`5`;`3`][SCS_4M6_IS_SCS;K_SCS_4M6;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`] THEN SYM_ASSUM_TAC; MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[STAB_4M6_SCS;SCS_DIAG_SCS_4M6_13]]);;let SET_STAB_4M6_ARROW_4T5=prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_4M6' i j| scs_diag 4 i j } {scs_4T5}`,ONCE_REWRITE_TAC[SET_RULE`{A}={A,A}`] THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M6' 0 2,scs_stab_diag_v39 scs_4M6' 1 3}` THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M6;] THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`;] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_SIMP_TAC[STAB_4M6_02_ARROW_4T5;STAB_4M6_13_ARROW_4T5]);;let BB_4M6_IMP_BB_STAN_4M6=prove(` BBs_v39 scs_4M6' v /\ scs_diag 4 i j /\ dist(v i,v j)<= cstab ==> BBs_v39 (scs_stab_diag_v39 scs_4M6' i j) v`,SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M6;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6] THEN REPEAT RESA_TAC THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`) 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 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`] THENL[ MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M6'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M6;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M6_IS_SCS] THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][] THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][]; MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M6'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M6;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M6_IS_SCS] THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][] THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]]);;end;; (* let check_completeness_claimA_concl = Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) *)let MM_4M6_IMP_STAB_4M6=prove(` MMs_v39 scs_4M6' v /\ scs_diag 4 i j /\ dist(v i,v j)<= cstab ==> ~(MMs_v39 (scs_stab_diag_v39 scs_4M6' i j) ={})`,STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC` scs_4M6' ` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M6' `;`v`] THEN ASSUME_TAC SCS_4M6_BASIC THEN ASSUME_TAC K_SCS_4M6 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M6_13;BB_4M6_IMP_BB_STAN_4M6;STAB_4M6_SCS] THEN SCS_TAC THEN REAL_ARITH_TAC);;