(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Chapter: Local Fan *) (* Author: Hoang Le Truong *) (* Date: 2012-04-01 *) (* ========================================================================= *) (* remaining conclusions from appendix to Local Fan chapter *) module Hijqaha = 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;; let SCS_5I1_STAB_DIAG_2h0=prove_by_refinement(`!v i j. BBs_v39 scs_5M2 v/\ scs_diag 5 i j /\ dist(v i,v j) <= cstab/\ (!i. dist(v i, v(i+1))<= &2 * h0) ==> BBs_v39 (scs_stab_diag_v39 scs_5I2 i j) v`, [ REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN DICH_TAC 3 THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASSUME_TAC th THEN MP_TAC th) THEN REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I2;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`;IN;K_SCS_5I2;Terminal.FUNLIST_EXPLICIT;] THEN ASM_SIMP_TAC[] THEN REPEAT RESA_TAC THEN SCS_TAC THEN MP_TAC(SET_RULE`i' MOD 5= j' MOD 5\/ ~(i' MOD 5= j' MOD 5)`) THEN RESA_TAC; THAYTHE_TAC (8-6)[`i'`;`j'`]; MP_TAC(SET_RULE`SUC i' MOD 5= j' MOD 5\/ ~(SUC i' MOD 5= j' MOD 5)`) THEN RESA_TAC; THAYTHE_TAC (9-6)[`i'`;`j'`] THEN DICH_TAC 1 THEN MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`] THEN SYM_ASSUM_TAC THEN DICH_TAC 1 THEN STRIP_TAC THEN SYM_ASSUM_TAC THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i'`;`5`][ARITH_RULE`1<5`] THEN SYM_ASSUM_TAC THEN MP_TAC(ARITH_RULE`i' MOD 5<5==> i' MOD 5=0\/ i' MOD 5=1\/ i' MOD 5=2\/ i' MOD 5=3\/i' MOD 5=4`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN SCS_TAC; MP_TAC(SET_RULE`i' MOD 5= SUC j' MOD 5\/ ~(i' MOD 5= SUC j' MOD 5)`) THEN RESA_TAC; THAYTHE_TAC (10-6)[`i'`;`j'`] THEN DICH_TAC 1 THEN MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`] THEN SYM_ASSUM_TAC THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j'`;`5`][ARITH_RULE`1<5`] THEN SYM_ASSUM_TAC THEN MP_TAC(ARITH_RULE`j' MOD 5<5==> j' MOD 5=0\/ j' MOD 5=1\/ j' MOD 5=2\/ j' MOD 5=3\/j' MOD 5=4`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN SCS_TAC; MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`] THEN THAYTHE_TAC(11-6)[`i'`;`j'`] THEN DICH_TAC 1 THEN REWRITE_TAC[PAIR_EQ;cstab] THEN SCS_TAC THEN MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC; THAYTHE_TAC (8-6)[`i'`;`j'`] THEN DICH_TAC 0 THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; MP_TAC(SET_RULE`SUC i' MOD 5= j' MOD 5\/ ~(SUC i' MOD 5= j' MOD 5)`) THEN RESA_TAC; MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j'`;`v`;`SUC i'`][SCS_5M2_IS_SCS;K_SCS_5M2;] THEN REWRITE_TAC[ADD1] THEN THAYTHE_TAC (10-2)[`i'`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; MP_TAC(SET_RULE`i' MOD 5= SUC j' MOD 5\/ ~(i' MOD 5= SUC j' MOD 5)`) THEN RESA_TAC; MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i'`;`v`;`SUC j'`][SCS_5M2_IS_SCS;K_SCS_5M2;] THEN REWRITE_TAC[ADD1] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN THAYTHE_TAC (11-2)[`j'`] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`) THEN RESA_TAC; MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`5`]; MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i'`;`v`;`i`][SCS_5M2_IS_SCS;K_SCS_5M2;] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j'`;`v`;`j`][SCS_5M2_IS_SCS;K_SCS_5M2;]; MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j'`;`v`;`i`][SCS_5M2_IS_SCS;K_SCS_5M2;] THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i'`;`v`;`j`][SCS_5M2_IS_SCS;K_SCS_5M2;] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]; MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`] THEN THAYTHE_TAC(12-6)[`i'`;`j'`] THEN DICH_TAC 0 THEN REWRITE_TAC[PAIR_EQ;cstab] THEN SCS_TAC]);; let MM_5M2_IMP_MM_STAB_5I2=prove(` MMs_v39 scs_5M2 v /\ scs_diag 5 i j /\ dist(v i,v j) <= cstab/\ (!i. dist(v i, v(i+1))<= &2 * h0) ==> ~(MMs_v39 (scs_stab_diag_v39 scs_5I2 i j)= {})`, STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC`scs_5M2` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`] THEN ASSUME_TAC SCS_5M2_BASIC THEN ASSUME_TAC K_SCS_5M2 THEN ASM_SIMP_TAC[SCS_5M2_IS_SCS;STAB_5I2_SCS;K_SCS_5I2;SCS_K_D_A_STAB_EQ;IN;SCS_5I1_STAB_DIAG_2h0] THEN SCS_TAC THEN REAL_ARITH_TAC);; let SCS_5I1_STAB_DIAG_2h0_sqrt8=prove_by_refinement( `BBs_v39 scs_5M2 v/\ scs_diag 5 i j /\ dist(v i,v j) <= cstab/\ &2* h0 <= dist(v 0, v(1)) /\ dist(v 0, v(1))<= sqrt8 ==> BBs_v39 ((scs_stab_diag_v39 scs_5I3 i j) ) v`, [ REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN DICH_TAC 4 THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASSUME_TAC th THEN MP_TAC th) THEN REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`;IN;K_SCS_5I3;scs_prop_equ_v39;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN ASM_SIMP_TAC[] THEN REPEAT RESA_TAC THEN SCS_TAC THEN MP_TAC(SET_RULE`i' MOD 5= j' MOD 5\/ ~(i' MOD 5= j' MOD 5)`) THEN RESA_TAC; THAYTHES_TAC (8-6)[`i':num`;`j':num`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(5=0)`]; MP_TAC(SET_RULE`SUC i' MOD 5= j' MOD 5\/ ~(SUC i' MOD 5= j' MOD 5)`) THEN RESA_TAC; THAYTHE_TAC (9-6)[`i'`;`j'`] THEN DICH_TAC 1 THEN MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i':num`;`j':num`][ARITH_RULE`~(5=0)`] THEN SYM_ASSUM_TAC THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` (i') MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` (j') MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN DICH_TAC 3 THEN STRIP_TAC THEN SYM_ASSUM_TAC THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i'`;`5`][ARITH_RULE`1<5`] THEN SYM_ASSUM_TAC THEN MP_TAC(ARITH_RULE`i' MOD 5<5==> i' MOD 5=0\/ i' MOD 5=1\/ i' MOD 5=2\/ i' MOD 5=3\/i' MOD 5=4`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`;] THEN RESA_TAC THEN SCS_TAC; MP_TAC(SET_RULE`i' MOD 5=SUC j' MOD 5\/ ~(i' MOD 5=SUC j' MOD 5)`) THEN RESA_TAC; THAYTHE_TAC (10-6)[`i'`;`j'`] THEN DICH_TAC 1 THEN MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i':num`;`j':num`][ARITH_RULE`~(5=0)`] THEN SYM_ASSUM_TAC THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` (i') MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` (j') MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j'`;`5`][ARITH_RULE`1<5`] THEN SYM_ASSUM_TAC THEN MP_TAC(ARITH_RULE`j' MOD 5<5==> j' MOD 5=0\/ j' MOD 5=1\/ j' MOD 5=2\/ j' MOD 5=3\/j' MOD 5=4`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`;] THEN RESA_TAC THEN SCS_TAC THEN ONCE_REWRITE_TAC[DIST_SYM] THEN RESA_TAC; MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`] THEN THAYTHE_TAC(11-6)[`i'`;`j'`] THEN DICH_TAC 1 THEN REWRITE_TAC[PAIR_EQ;cstab;h0] THEN SCS_TAC THEN REAL_ARITH_TAC; THAYTHES_TAC (8-6)[`i':num`;`j':num`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(5=0)`;cstab] THEN DICH_TAC 0 THEN REAL_ARITH_TAC; MP_TAC(SET_RULE`SUC i' MOD 5= j' MOD 5\/ ~(SUC i' MOD 5= j' MOD 5)`) THEN RESA_TAC; THAYTHES_TAC (9-6)[`i':num`;`j':num`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(5=0)`;cstab] THEN DICH_TAC 0 THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`) THEN RESA_TAC; MRESAL_TAC Hexagons.DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`] THEN DICH_TAC 0 THEN ASM_REWRITE_TAC[scs_diag]; SCS_TAC THEN MP_TAC(SET_RULE`psort 5 (i',j') = 0,1\/ ~(psort 5 (i',j') = 0,1)`) THEN RESA_TAC; MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`1`;`j'`;`0`;`5`][PSORT_5_EXPLICIT]; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]; MP_TAC(SET_RULE`i' MOD 5= SUC j' MOD 5\/ ~(i' MOD 5= SUC j' MOD 5)`) THEN RESA_TAC; THAYTHES_TAC (10-6)[`i':num`;`j':num`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(5=0)`;cstab] THEN DICH_TAC 0 THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`) THEN RESA_TAC; MRESAL_TAC Hexagons.DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`] THEN DICH_TAC 0 THEN ASM_REWRITE_TAC[scs_diag]; SCS_TAC THEN MP_TAC(SET_RULE`psort 5 (i',j') = 0,1\/ ~(psort 5 (i',j') = 0,1)`) THEN RESA_TAC; MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`1`;`j'`;`0`;`5`][PSORT_5_EXPLICIT]; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]; MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`) THEN RESA_TAC; MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`j`;`j'`;`i`;`5`][PSORT_5_EXPLICIT]; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]; MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`] THEN THAYTHE_TAC(13-7)[`i'`;`j'`] THEN DICH_TAC 0 THEN REWRITE_TAC[PAIR_EQ;cstab] THEN SCS_TAC]);; let SCS_5M2_EDGE_LE_2H0=prove(`BBs_v39 scs_5M2 v/\ scs_diag 5 i j /\ dist(v i,v j) <= cstab/\ &2* h0 < dist(v l, v (SUC l)) /\ ~(l MOD 5=0) ==> F`, REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`;IN;K_SCS_5I3;scs_prop_equ_v39;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN REPEAT STRIP_TAC THEN THAYTHE_TAC 7[`l`;`SUC l`] THEN DICH_TAC 0 THEN SCS_TAC THEN ASM_SIMP_TAC[Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`~(5=0)`] THEN MRESAL_TAC Hexagons.PSORT_MOD[`5`;`l:num`;`SUC l:num`][ARITH_RULE`~(5=0)`] THEN SYM_ASSUM_TAC THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`l`;`5`][ARITH_RULE`1<5`] THEN SYM_ASSUM_TAC THEN MP_TAC(ARITH_RULE`l MOD 5<5==> l MOD 5=0\/ l MOD 5=1\/ l MOD 5=2\/ l MOD 5=3\/l MOD 5=4`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`;] THEN RESA_TAC THEN SCS_TAC THEN DICH_TAC (10-7) THEN REAL_ARITH_TAC);; let SCS_5M2_EDGE_LE_2H0_IMP_0=prove( `BBs_v39 scs_5M2 v/\ scs_diag 5 i j /\ dist(v i,v j) <= cstab/\ &2* h0 < dist(v l, v (SUC l)) ==> l MOD 5=0`, STRIP_TAC THEN MP_TAC SCS_5M2_EDGE_LE_2H0 THEN RESA_TAC);; let MM_5M2_IMP_MM_STAB_5I3=prove(` MMs_v39 scs_5M2 v /\ scs_diag 5 i j /\ dist(v i,v j) <= cstab/\ &2 * h0< dist(v l, v(l+1)) /\ dist(v l, v(l+1))<= sqrt8 ==> ~(MMs_v39 (scs_stab_diag_v39 scs_5I3 i j)= {})`, STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC`scs_5M2` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`] THEN ASSUME_TAC SCS_5M2_BASIC THEN ASSUME_TAC K_SCS_5M2 THEN ASM_SIMP_TAC[SCS_5M2_IS_SCS;STAB_5I3_SCS;K_SCS_5I3;SCS_K_D_A_STAB_EQ;IN; ADD1] THEN MP_TAC SCS_5M2_EDGE_LE_2H0_IMP_0 THEN REWRITE_TAC[ ADD1] THEN RESA_TAC THEN DICH_TAC 4 THEN DICH_TAC 4 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l:num`;`v`;` l MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l+1:num`;`v`;` (l+1) MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`] THEN MRESAL_TAC MOD_ADD_MOD[`l`;`1`;`5`][ARITH_RULE`~(5=0)/\ 1 MOD 5=1/\ 0+a=a`] THEN SYM_ASSUM_TAC THEN STRIP_TAC THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`&2 * h0 < dist ((v:num->real^3) 0,v 1) ==> &2 * h0 <= dist (v 0,v 1)`) THEN RESA_TAC THEN MP_TAC SCS_5I1_STAB_DIAG_2h0_sqrt8 THEN RESA_TAC THEN SCS_TAC THEN REAL_ARITH_TAC);; let SCS_5I1_STAB_DIAG_sqrt8=prove_by_refinement(`BBs_v39 scs_5M2 v/\ scs_diag 5 i j /\ dist(v i,v j) <= cstab/\ sqrt8 <= dist(v 0, v(1)) ==> BBs_v39 ((scs_stab_diag_v39 scs_5M2 i j) ) v`, [ REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN DICH_TAC 3 THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASSUME_TAC th THEN MP_TAC th) THEN REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`;IN;K_SCS_5I3;scs_prop_equ_v39;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN ASM_SIMP_TAC[] THEN REPEAT RESA_TAC THEN SCS_TAC THEN MP_TAC(SET_RULE`i' MOD 5= j' MOD 5\/ ~(i' MOD 5= j' MOD 5)`) THEN RESA_TAC; THAYTHE_TAC (8-6)[`i'`;`j'`] THEN DICH_TAC 0 THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`) THEN RESA_TAC; MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`j`;`j'`;`i`;`5`][PSORT_5_EXPLICIT]; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]; THAYTHE_TAC(9-6)[`i'`;`j'`] THEN DICH_TAC 0 THEN SCS_TAC]);; let MM_5M2_IMP_MM_STAB_5M2=prove(` MMs_v39 scs_5M2 v /\ scs_diag 5 i j /\ dist(v i,v j) <= cstab/\ sqrt8<= dist(v l, v(l+1)) ==> ~(MMs_v39 (scs_stab_diag_v39 scs_5M2 i j)= {})`, STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC`scs_5M2` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`] THEN ASSUME_TAC SCS_5M2_BASIC THEN ASSUME_TAC K_SCS_5M2 THEN ASM_SIMP_TAC[SCS_5M2_IS_SCS;STAB_5M2_SCS;K_SCS_5I3;SCS_K_D_A_STAB_EQ;IN; ADD1] THEN MP_TAC SCS_5M2_EDGE_LE_2H0_IMP_0 THEN ASM_REWRITE_TAC[ ADD1;h0] THEN MP_TAC LT_sqrt8_2h0 THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`sqrt8 <= dist ((v:num->real^3) l,v (l + 1))/\ &2 * #1.26 < sqrt8==> &2 * #1.26 < dist (v l,v (l + 1))`) THEN RESA_TAC THEN STRIP_TAC THEN DICH_TAC (9-3) THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l:num`;`v`;` l MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l+1:num`;`v`;` (l+1) MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`] THEN MRESAL_TAC MOD_ADD_MOD[`l`;`1`;`5`][ARITH_RULE`~(5=0)/\ 1 MOD 5=1/\ 0+a=a`] THEN SYM_ASSUM_TAC THEN STRIP_TAC THEN MP_TAC SCS_5I1_STAB_DIAG_sqrt8 THEN RESA_TAC THEN SCS_TAC THEN REAL_ARITH_TAC);; (************) (*new definition scs*) (*************************) let SCS_DIAG_SCS_5M2_02=prove(`scs_diag (scs_k_v39 scs_5M2) 0 2`, REWRITE_TAC[K_SCS_5M2;scs_diag] THEN ARITH_TAC);; let SCS_DIAG_SCS_5M2_03=prove(`scs_diag (scs_k_v39 scs_5M2) 0 3`, REWRITE_TAC[K_SCS_5M2;scs_diag] THEN ARITH_TAC);; let SCS_DIAG_SCS_5M2_24=prove(`scs_diag (scs_k_v39 scs_5M2) 2 4`, REWRITE_TAC[K_SCS_5M2;scs_diag] THEN ARITH_TAC);; let scs_5M3 = new_definition`scs_5M3 = mk_unadorned_v39 5 (#0.616) (funlist_v39 [(0,1),(&2*h0);(0,2),(cstab);(0,3),(cstab);(1,3),(cstab);(1,4),(cstab);(2,4),(cstab)] (&2) 5) (funlist_v39 [(0,1),cstab;(0,2),(&6); (0,3),(&6); (1,3),(&6); (1,4),(&6); (2,4),(&6)] (&2*h0) 5)`;; let scs_3T4_prime = (* terminal_tri_6833979866 = *) new_definition `scs_3T4_prime = mk_unadorned_v39 3 (#0.2759) (funlist_v39 [(0,1),(&2);(1,2),cstab] (&2*h0) 3) (funlist_v39 [(0,1),(&2 * h0)] (cstab) 3)`;; let scs_4M6_prime = new_definition `scs_4M6_prime = mk_unadorned_v39 4 (#0.513) (funlist_v39 [(0,1),cstab;(0,2),(cstab);(1,3),(cstab)] (&2) 4) (funlist_v39 [(0,1),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;; let scs_4M7_prime = new_definition `scs_4M7_prime = mk_unadorned_v39 4 (#0.513) (funlist_v39 [(0,1),cstab;(1,2),(&2*h0);(0,2),(cstab);(1,3),(cstab)] (&2) 4) (funlist_v39 [(0,1),cstab;(1,2),cstab;(0,2),(&6);(1,3),(&6);(1,3),(&6)] (&2*h0) 4)`;; let scs_3T1_PRELIM_prime = (* ear_jnull = *) new_definition `scs_3T1_prime = scs_v39 (3, #0.11, funlist_v39 [(0,1),cstab] (&2) 3, funlist_v39 [(0,1),cstab] (&2) 3, funlist_v39 [(0,1),cstab] (&2*h0) 3, funlist_v39 [(0,1),cstab] ((&2)*h0) 3, (\i j. F),{},{},{})`;; let scs_3T1_prime = prove_by_refinement( `scs_3T1_prime = mk_unadorned_v39 3 (#0.11) (funlist_v39 [(0,1),(cstab)] (&2) 3) (funlist_v39 [(0,1),(cstab)] (&2 * h0) 3)`, (* {{{ proof *) [ BY(REWRITE_TAC[mk_unadorned_v39;scs_3T1_PRELIM_prime]); ]);; (* }}} *) let scs_4M8_prime = new_definition `scs_4M8_prime = mk_unadorned_v39 4 (#0.513) (funlist_v39 [(0,1),(&2*h0);(2,3),(cstab);(0,2),(cstab);(1,3),(cstab)] (&2) 4) (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(&6);(1,3),(&6);(1,3),(&6)] (&2*h0) 4)`;; let PSORT_5_EXPLICIT=prove(` psort 5 (0,0)= (0,0)/\ psort 5 (1,1)= (1,1)/\ psort 5 (2,2)= (2,2)/\ psort 5 (3,3)= (3,3)/\ psort 5 (4,4)= (4,4)/\ psort 5 (0,1)= (0,1)/\ psort 5 (0,2)= (0,2)/\ psort 5 (0,3)= (0,3)/\ psort 5 (0,4)= (0,4)/\ psort 5 (1,0)= (0,1)/\ psort 5 (1,2)= (1,2)/\ psort 5 (1,3)= (1,3)/\ psort 5 (1,4)= (1,4)/\ psort 5 (2,0)= (0,2)/\ psort 5 (2,1)= (1,2)/\ psort 5 (2,3)= (2,3)/\ psort 5 (2,4)= (2,4)/\ psort 5 (3,0)= (0,3)/\ psort 5 (3,1)= (1,3)/\ psort 5 (3,2)= (2,3)/\ psort 5 (3,4)= (3,4)/\ psort 5 (4,0)= (0,4)/\ psort 5 (4,1)= (1,4)/\ psort 5 (4,2)= (2,4)/\ psort 5 (4,3)= (3,4)/\ psort 5 (4,5)= (0,4)/\ psort 5 (3,5)= (0,3)/\ psort 5 (2,5)= (0,2)/\ psort 5 (1,5)= (0,1)/\ psort 5 (5,1)= (0,1)/\ psort 5 (5,2)= (0,2)/\ psort 5 (5,3)= (0,3)/\ psort 5 (5,4)= (0,4)/\ psort 5 (5,5)= (0,0)/\ psort 5 (5,6)= (0,1)/\ psort 5 (5,7)= (0,2)/\ psort 5 (4,6)= (1,4)/\ psort 5 (6,4)= (1,4)/\ psort 5 (6,5)= (0,1)/\ psort 5 (6,7)= (1,2)/\ psort 5 (7,5)= (0,2)/\ psort 5 (7,6)= (1,2)/\ psort 5 (7,7)= (2,2)/\ psort 5 (6,6)= (1,1)/\ psort 4 (3,4)= (0,3)/\ psort 3 (2,0)= (0,2)/\ psort 3 (2,1)= (1,2)/\ psort 3 (1,0)= (0,1)`, REWRITE_TAC[psort;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_4_TAC;LET_DEF;LET_END_DEF;MOD_5_EXPLICIT;ARITH_RULE`0<=a/\ ~(1<= 0)/\ ~(2<=0)/\ ~(3<=0)/\ ~(4<=0)/\a<=a/\ ~(2<=1)/\ ~(3<=2)/\ ~(4<=3)/\ ~(3<=1)/\ ~(4<=1)/\ ~(4<=2)/\ 2<=3`]);; let SCS_TAC= ASM_SIMP_TAC[scs_basic;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} j <=> {} i`;periodic2;scs_basic;unadorned_v39;scs_prop_equ_v39;LET_DEF;LET_END_DEF;scs_stab_diag_v39;scs_half_slice_v39; Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_5_TAC; scs_5M1;scs_3M1;scs_6I1;scs_3T1;scs_4M2;scs_6M1;scs_6T1;scs_5I1;scs_5I2;scs_5I3;scs_5M2;scs_4M6;scs_3T4;scs_5M3;scs_3T4_prime;scs_4M6_prime;scs_4M7_prime;scs_4M7;scs_3T1_prime;scs_4M8;scs_4M8_prime;scs_5T1;scs_3T5;scs_4M3;scs_3T6;scs_4M4;scs_4M5; Terminal.FUNLIST_EXPLICIT;Yrtafyh.PSORT_PERIODIC;PSORT_5_EXPLICIT; ARITH_RULE`SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6/\ SUC 6=7/\ SUC 7=8`];; (****************) let SCS_5T1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5T1`, [ REWRITE_TAC[scs_5T1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(5=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=5/\ 5<=6/\a<=a/\ ~(5=4)/\ ~(6=0)`;d_tame;REAL_ARITH`#0.616 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(&2 * #1.26 < &2)/\ ~(a {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`] THEN SUBGOAL_THEN`{i | i < 5 /\ (&2 * #1.26 < (if psort 5 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/ &2 < (if psort 5 (i,SUC i) = 0,1 then &2* #1.26 else &2))} ={0}`ASSUME_TAC; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;h0] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN REAL_ARITH_TAC; MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\ (&2 * h0 < funlist_v39 [(0,1),&2 * h0] cstab 3 i (SUC i) \/ &2 < funlist_v39 [(0,1),&2] (&2 * h0) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`] THEN MATCH_DICH_TAC 0 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC]);; let SCS_3T5_IS_SCS=prove_by_refinement(`is_scs_v39 scs_3T5`, [ SIMP_TAC[scs_3T5;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.103 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN MP_TAC LE_sqrt8_2h0 THEN REAL_ARITH_TAC; SCS_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;h0] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC; DICH_TAC 0 THEN ARITH_TAC; MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\ (&2 * h0 < funlist_v39 [(0,1),sqrt8] (&2 * h0) 3 i (SUC i) \/ &2 < funlist_v39 [(0,1),&2 * h0] (&2) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`] THEN MATCH_DICH_TAC 0 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC; ]);; let SCS_3T6_IS_SCS=prove_by_refinement(`is_scs_v39 scs_3T6'`, [ SIMP_TAC[scs_3T6;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.4348 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC; SCS_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;h0] THEN MP_TAC LE_sqrt8_2 THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN REAL_ARITH_TAC; MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\ (&2 * h0 < funlist_v39 [(0,1),cstab; (1,2),cstab] (&2 * h0) 3 i (SUC i) \/ &2 < funlist_v39 [(0,1),sqrt8; (1,2),sqrt8] (&2) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`] THEN MATCH_DICH_TAC 0 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC; ]);; let SCS_3T1_prime_IS_SCS=prove_by_refinement(`is_scs_v39 scs_3T1_prime`, [SIMP_TAC[scs_3T1_prime;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.11 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN REAL_ARITH_TAC; MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\ (&2 * h0 < funlist_v39 [(0,1),cstab] (&2 * h0) 3 i (SUC i) \/ &2 < funlist_v39 [(0,1),cstab] (&2) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`] THEN MATCH_DICH_TAC 0 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC; ]);; let SCS_3T1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_3T1`, [ SIMP_TAC[scs_3T1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.11 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC; SCS_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;h0;cstab] THEN MP_TAC LE_sqrt8_2 THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN REAL_ARITH_TAC; MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\ (&2 * h0 < funlist_v39 [(0,1),cstab] (&2 * h0) 3 i (SUC i) \/ &2 < funlist_v39 [(0,1),sqrt8] (&2) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`] THEN MATCH_DICH_TAC 0 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC; ]);; let SCS_3T4_prime_IS_SCS=prove_by_refinement( `is_scs_v39 scs_3T4_prime`, [SIMP_TAC[scs_3T4_prime;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.2759 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN REAL_ARITH_TAC; MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\ (&2 * h0 < funlist_v39 [(0,1),&2 * h0] cstab 3 i (SUC i) \/ &2 < funlist_v39 [(0,1),&2; (1,2),cstab] (&2 * h0) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`] THEN MATCH_DICH_TAC 0 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC]);; let SCS_4M6_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M6'`, [ SIMP_TAC[scs_4M6;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`] THEN SUBGOAL_THEN`{i | i < 4 /\ (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/ &2 < (if psort 4 (i,SUC i) = 0,1 then &2 * #1.26 else &2))} ={0}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`] THEN SUBGOAL_THEN`{i | i < 4 /\ (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else if psort 4 (i,SUC i) = 2,3 then #3.01 else &2 * #1.26) \/ &2 < (if psort 4 (i,SUC i) = 0,1 then &2 * #1.26 else if psort 4 (i,SUC i) = 2,3 then &2 * #1.26 else &2))} ={0,2}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a (a=b\/ a=c)`] THEN RESA_TAC THEN SCS_TAC THEN REAL_ARITH_TAC; ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=2)`] THEN ARITH_TAC; ]);; let SCS_4M6_prime_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M6_prime`, [ SIMP_TAC[scs_4M6_prime;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`] THEN SUBGOAL_THEN`{i | i < 4 /\ (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/ &2 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2))} ={0}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`] THEN SUBGOAL_THEN`{i | i < 4 /\ (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else if psort 4 (i,SUC i) = 1,2 then #3.01 else &2 * #1.26) \/ &2 < (if psort 4 (i,SUC i) = 0,1 then &2 * #1.26 else if psort 4 (i,SUC i) = 1,2 then &2 * #1.26 else &2))} ={0,1}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a (a=b\/ a=c)`] THEN RESA_TAC THEN SCS_TAC THEN REAL_ARITH_TAC; ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=1)`] THEN ARITH_TAC; ]);; let SCS_4M3_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M3'`, [ SIMP_TAC[scs_4M3;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN MP_TAC sqrt8_LE_6 THEN MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN MP_TAC LE_sqrt8_2 THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`] THEN SUBGOAL_THEN`{i | i < 4 /\ (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/ &2 < (if psort 4 (i,SUC i) = 0,1 then sqrt8 else &2))} ={0}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`] THEN SUBGOAL_THEN`{i | i < 4 /\ (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else if psort 4 (i,SUC i) = 1,2 then #3.01 else &2 * #1.26) \/ &2 < (if psort 4 (i,SUC i) = 0,1 then &2 * #1.26 else if psort 4 (i,SUC i) = 1,2 then &2 * #1.26 else &2))} ={0,1}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a a=b\/ a=c`] THEN RESA_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a a=b\/ a=c`] ; ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=1)`] THEN ARITH_TAC; ]);; let SCS_4M7_prime_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M7_prime`, [ SIMP_TAC[scs_4M7_prime;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`] THEN SUBGOAL_THEN`{i | i < 4 /\ (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else if psort 4 (i,SUC i) = 1,2 then #3.01 else &2 * #1.26) \/ &2 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else if psort 4 (i,SUC i) = 1,2 then &2 * #1.26 else &2))} ={0,1}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a a=b\/ a=c`] THEN RESA_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a a=b\/ a=c`] ; ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=1)`] THEN ARITH_TAC; ]);; let SCS_4M8_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M8`, [ SIMP_TAC[scs_4M8;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`] THEN SUBGOAL_THEN`{i | i < 4 /\ (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else if psort 4 (i,SUC i) = 2,3 then #3.01 else &2 * #1.26) \/ &2 < (if psort 4 (i,SUC i) = 0,1 then &2 * #1.26 else if psort 4 (i,SUC i) = 2,3 then &2 * #1.26 else &2))} ={0,2}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a a=b\/ a=c`] THEN RESA_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a a=b\/ a=c`] ; ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=2)`] THEN ARITH_TAC; ]);; let SCS_4M8_prime_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M8_prime`, [ SIMP_TAC[scs_4M8_prime;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`] THEN SUBGOAL_THEN`{i | i < 4 /\ (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else if psort 4 (i,SUC i) = 2,3 then #3.01 else &2 * #1.26) \/ &2 < (if psort 4 (i,SUC i) = 0,1 then &2 * #1.26 else if psort 4 (i,SUC i) = 2,3 then #3.01 else &2))} ={0,2}`ASSUME_TAC ; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a a=b\/ a=c`] THEN RESA_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a a=b\/ a=c`] ; ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=2)`] THEN ARITH_TAC; ]);; (****************************) let SCS_5M3_BASIC=prove(`scs_basic_v39 scs_5M3`, SCS_TAC);; let SCS_5T1_BASIC=prove(`scs_basic_v39 scs_5T1`, SCS_TAC);; let SCS_4M6_prime_BASIC=prove(`scs_basic_v39 scs_4M6_prime`, SCS_TAC);; let SCS_4M7_prime_BASIC=prove(`scs_basic_v39 scs_4M7_prime`, SCS_TAC);; let SCS_4M4_BASIC=prove(`scs_basic_v39 scs_4M4'`, SCS_TAC);; let SCS_4M7_BASIC=prove(`scs_basic_v39 scs_4M7`, SCS_TAC);; let SCS_4M3_BASIC=prove(`scs_basic_v39 scs_4M3'`, SCS_TAC);; let SCS_4M5_BASIC=prove(`scs_basic_v39 scs_4M5'`, SCS_TAC);; let SCS_3T4_prime_BASIC=prove(`scs_basic_v39 scs_3T4_prime`, SCS_TAC);; let SCS_3T6_BASIC=prove(`scs_basic_v39 scs_3T6'`, SCS_TAC);; let SCS_3T1_prime_BASIC=prove(`scs_basic_v39 scs_3T1_prime`, SCS_TAC);; let SCS_3T5_BASIC=prove(`scs_basic_v39 scs_3T5`, SCS_TAC);; let SCS_4M8_prime_BASIC=prove(`scs_basic_v39 scs_4M8_prime`, SCS_TAC);; let SCS_4M8_BASIC=prove(`scs_basic_v39 scs_4M8`, SCS_TAC);; let K_SCS_5M3=prove(`scs_k_v39 scs_5M3=5`, SCS_TAC);; let K_SCS_5T1=prove(`scs_k_v39 scs_5T1=5`, SCS_TAC);; let K_SCS_3T4_prime=prove(`scs_k_v39 scs_3T4_prime=3`, SCS_TAC);; let K_SCS_3T5=prove(`scs_k_v39 scs_3T5=3`, SCS_TAC);; let K_SCS_3T6=prove(`scs_k_v39 scs_3T6'=3`, SCS_TAC);; let K_SCS_4M4=prove(`scs_k_v39 scs_4M4'=4`, SCS_TAC);; let K_SCS_4M5=prove(`scs_k_v39 scs_4M5'=4`, SCS_TAC);; let K_SCS_4M3=prove(`scs_k_v39 scs_4M3'=4`, SCS_TAC);; let K_SCS_4M6_prime=prove(`scs_k_v39 scs_4M6_prime=4`, SCS_TAC);; let K_SCS_3T1_prime=prove(`scs_k_v39 scs_3T1_prime=3`, SCS_TAC);; let K_SCS_4M7_prime=prove(`scs_k_v39 scs_4M7_prime=4`, SCS_TAC);; let K_SCS_4M7=prove(`scs_k_v39 scs_4M7=4`, SCS_TAC);; let K_SCS_4M8_prime=prove(`scs_k_v39 scs_4M8_prime=4`, SCS_TAC);; let K_SCS_4M8=prove(`scs_k_v39 scs_4M8=4`, SCS_TAC);; let J_SCS_5M3=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5M3 i) i1 j= F`, SCS_TAC );; let J_SCS_5T1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5T1 i) i1 j= F`, SCS_TAC );; let J_SCS_3T4_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T4_prime i) i1 j= F`, SCS_TAC );; let J_SCS_4M4=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M4' i) i1 j= F`, SCS_TAC );; let J_SCS_4M3=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M3' i) i1 j= F`, SCS_TAC );; let J_SCS_4M5=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M5' i) i1 j= F`, SCS_TAC );; let J_SCS_4M6_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M6_prime i) i1 j= F`, SCS_TAC );; let J_SCS_5M2=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5M2 i) i1 j= F`, SCS_TAC );; let J_SCS_3T1_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T1_prime i) i1 j= F`, SCS_TAC );; let J_SCS_3T1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T1 i) i1 j= F`, SCS_TAC );; let J_SCS_3T6=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T6' i) i1 j= F`, SCS_TAC );; let J_SCS_3T5=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T5 i) i1 j= F`, SCS_TAC );; let J_SCS_4M7_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M7_prime i) i1 j= F`, SCS_TAC );; let J_SCS_4M7=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M7 i) i1 j= F`, SCS_TAC );; let J_SCS_4M8_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M8_prime i) i1 j= F`, SCS_TAC );; let J_SCS_4M8=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M8 i) i1 j= F`, SCS_TAC );; let J_SCS_4M8_prime1=prove(`scs_J_v39 (scs_4M8_prime ) i1 j= F`, SCS_TAC );; let STAB_5I1_SCS=prove(` scs_diag (scs_k_v39 scs_5I1) i j ==> is_scs_v39 (scs_stab_diag_v39 scs_5I1 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5I1 i j)`, STRIP_TAC THEN MATCH_MP_TAC Yrtafyh.YRTAFYH THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5I1_IS_SCS;SCS_5I1_BASIC;K_SCS_5I1; ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab] THEN SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC);; let STAB_5I2_SCS=prove(` scs_diag (scs_k_v39 scs_5I2) i j ==> is_scs_v39 (scs_stab_diag_v39 scs_5I2 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5I2 i j)`, STRIP_TAC THEN MATCH_MP_TAC Yrtafyh.YRTAFYH THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5I2_IS_SCS;SCS_5I2_BASIC;K_SCS_5I2; ARITH_RULE`3<5`;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_5M3_SCS=prove(` scs_diag (scs_k_v39 scs_5M3) i j ==> is_scs_v39 (scs_stab_diag_v39 scs_5M3 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5M3 i j)`, STRIP_TAC THEN MATCH_MP_TAC Yrtafyh.YRTAFYH THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5M3_IS_SCS;SCS_5M3_BASIC;K_SCS_5M3; ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab] THEN SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC);; let STAB_5T1_SCS=prove(` scs_diag (scs_k_v39 scs_5T1) i j ==> is_scs_v39 (scs_stab_diag_v39 scs_5T1 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5T1 i j)`, STRIP_TAC THEN MATCH_MP_TAC Yrtafyh.YRTAFYH THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5T1_IS_SCS;SCS_5T1_BASIC;K_SCS_5T1; ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab] THEN SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC);; (*****************************) let SCS_5M3_STAB_DIAG_sqrt8=prove_by_refinement(`BBs_v39 scs_5M2 v/\ scs_diag 5 i j /\ dist(v i,v j) <= cstab/\ sqrt8 <= dist(v 0, v(1)) ==> BBs_v39 ((scs_stab_diag_v39 scs_5M3 i j) ) v`, [REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN DICH_TAC 3 THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASSUME_TAC th THEN MP_TAC th) THEN REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5M3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`;IN;K_SCS_5M3;scs_prop_equ_v39;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN ASM_SIMP_TAC[] THEN REPEAT RESA_TAC THEN SCS_TAC THEN MP_TAC(SET_RULE`i' MOD 5= j' MOD 5\/ ~(i' MOD 5= j' MOD 5)`) THEN RESA_TAC; THAYTHE_TAC (8-6)[`i'`;`j'`] THEN DICH_TAC 0 THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; MP_TAC(SET_RULE`psort 5 (i',j') = 0,1\/ ~(psort 5 (i',j') = 0,1)`) THEN RESA_TAC; MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`1`;`j'`;`0`;`5`][PSORT_5_EXPLICIT]; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN DICH_TAC(13-2) THEN MP_TAC LE_sqrt8_2h0 THEN REWRITE_TAC[h0] THEN REAL_ARITH_TAC; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN DICH_TAC(13-2) THEN MP_TAC LE_sqrt8_2h0 THEN REWRITE_TAC[h0] THEN REAL_ARITH_TAC; THAYTHE_TAC (9-6)[`i'`;`j'`] THEN DICH_TAC 1 THEN SCS_TAC THEN REWRITE_TAC[cstab;h0]; THAYTHE_TAC (8-6)[`i'`;`j'`] THEN DICH_TAC 0 THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`) THEN RESA_TAC; MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`j`;`j'`;`i`;`5`][PSORT_5_EXPLICIT]; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]; THAYTHE_TAC(9-6)[`i'`;`j'`] THEN DICH_TAC 0 THEN SCS_TAC]);; let SCS_DIAG_SCS_5M3_02=prove(`scs_diag (scs_k_v39 scs_5M3) 0 2`, REWRITE_TAC[K_SCS_5M3;scs_diag] THEN ARITH_TAC);; let SCS_DIAG_SCS_5M3_03=prove(`scs_diag (scs_k_v39 scs_5M3) 0 3`, REWRITE_TAC[K_SCS_5M3;scs_diag] THEN ARITH_TAC);; let SCS_DIAG_SCS_5M3_24=prove(`scs_diag (scs_k_v39 scs_5M3) 2 4`, REWRITE_TAC[K_SCS_5M3;scs_diag] THEN ARITH_TAC);; let MM_5M2_IMP_MM_STAB_5M3=prove( ` MMs_v39 scs_5M2 v /\ scs_diag 5 i j /\ dist(v i,v j) <= cstab/\ sqrt8<= dist(v l, v(l+1)) ==> ~(MMs_v39 (scs_stab_diag_v39 scs_5M3 i j)= {})`, STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC`scs_5M2` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`] THEN ASSUME_TAC SCS_5M2_BASIC THEN ASSUME_TAC K_SCS_5M2 THEN ASM_SIMP_TAC[SCS_5M2_IS_SCS;STAB_5M3_SCS;K_SCS_5M3;SCS_K_D_A_STAB_EQ;IN; ADD1] THEN MP_TAC SCS_5M2_EDGE_LE_2H0_IMP_0 THEN ASM_REWRITE_TAC[ ADD1;h0] THEN MP_TAC LT_sqrt8_2h0 THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`sqrt8 <= dist ((v:num->real^3) l,v (l + 1))/\ &2 * #1.26 < sqrt8==> &2 * #1.26 < dist (v l,v (l + 1))`) THEN RESA_TAC THEN STRIP_TAC THEN DICH_TAC (9-3) THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l:num`;`v`;` l MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`] THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l+1:num`;`v`;` (l+1) MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`] THEN MRESAL_TAC MOD_ADD_MOD[`l`;`1`;`5`][ARITH_RULE`~(5=0)/\ 1 MOD 5=1/\ 0+a=a`] THEN SYM_ASSUM_TAC THEN STRIP_TAC THEN MP_TAC SCS_5M3_STAB_DIAG_sqrt8 THEN RESA_TAC THEN SCS_TAC THEN REAL_ARITH_TAC);; let STAB_5M3_SCS=prove(` scs_diag (scs_k_v39 scs_5M3) i j ==> is_scs_v39 (scs_stab_diag_v39 scs_5M3 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5M3 i j)`, STRIP_TAC THEN MATCH_MP_TAC Yrtafyh.YRTAFYH THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5M3_IS_SCS;SCS_5M3_BASIC;K_SCS_5M3; ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab] THEN SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC);; let BB_3T4_prime_IMP_scs_3T4=prove(`BBs_v39 scs_3T4_prime v ==> BBs_v39 (scs_3T4 ) v`, REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`(3<=3)`;IN;K_SCS_3T4;K_SCS_3T4_prime;scs_prop_equ_v39;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN SCS_TAC THEN REPEAT RESA_TAC THEN THAYTHE_TAC 0[`i`;`j`] THEN DICH_TAC 1 THEN REWRITE_TAC[cstab;h0] THEN REAL_ARITH_TAC);; let MM_3T4_prime_IMP_MM_3T4=prove(`MMs_v39 scs_3T4_prime v ==> ~(MMs_v39 scs_3T4={})`, STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC`scs_3T4_prime` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_3T4_prime`;`v`] THEN ASM_SIMP_TAC[SCS_3T4_BASIC;SCS_3T4_prime_BASIC;SCS_3T4_IS_SCS;SCS_3T4_IS_SCS; SCS_3T4_prime_IS_SCS;K_SCS_3T4;K_SCS_3T4_prime;IN;BB_3T4_prime_IMP_scs_3T4] THEN SCS_TAC THEN REAL_ARITH_TAC);; let SCS_3T4_prime_ARROW_MM_3T4=prove_by_refinement(`scs_arrow_v39 {scs_3T4_prime } { scs_3T4}`, [ 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_3T4_IS_SCS]; DISJ_CASES_TAC(SET_RULE`(!s. s = scs_3T4_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_3T4_prime ==> 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_3T4` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC (GEN_ALL MM_3T4_prime_IMP_MM_3T4) THEN POP_ASSUM MP_TAC THEN SET_TAC[]]);; let BB_4M6_prime_IMP_scs_4M6=prove(`BBs_v39 scs_4M6_prime v ==> BBs_v39 (scs_4M6' ) v`, REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4M6_prime;K_SCS_4M6;scs_prop_equ_v39;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN SCS_TAC THEN REPEAT RESA_TAC THEN THAYTHE_TAC 1[`i`;`j`] THEN DICH_TAC 1 THEN REWRITE_TAC[cstab;h0] THEN REAL_ARITH_TAC);; let MM_4M6_prime_IMP_MM_4M6=prove(`MMs_v39 scs_4M6_prime v ==> ~(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_4M6_prime` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M6_prime`;`v`] THEN ASM_SIMP_TAC[SCS_4M6_BASIC;SCS_4M6_prime_BASIC;SCS_4M6_IS_SCS;SCS_4M6_IS_SCS; SCS_4M6_prime_IS_SCS;K_SCS_4M6;K_SCS_4M6_prime;IN;BB_4M6_prime_IMP_scs_4M6] THEN SCS_TAC THEN REAL_ARITH_TAC);; let SCS_4M6_prime_ARROW_MM_4M6=prove_by_refinement(`scs_arrow_v39 {scs_4M6_prime } { scs_4M6'}`, [ 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_4M6_IS_SCS]; DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M6_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M6_prime ==> 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_4M6'` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC (GEN_ALL MM_4M6_prime_IMP_MM_4M6) THEN POP_ASSUM MP_TAC THEN SET_TAC[]]);; let SCS_5M3_SLICE_02=prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 0 2 } { scs_prop_equ_v39 scs_3T4_prime 2, scs_prop_equ_v39 scs_4M6_prime 1}`, [ MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI) THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_02;STAB_5M3_SCS;SCS_K_D_A_STAB_EQ;] THEN EXISTS_TAC`0` THEN EXISTS_TAC`2` THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_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_5M3_BASIC;SCS_3T4_prime_BASIC;J_SCS_4M6_prime;BASIC_HALF_SLICE_STAB;J_SCS_3T4_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4M6_prime_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_3T4_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M3] 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_5M3;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2;scs_3T4_prime;scs_5M3; ARITH_RULE`(2 + 1 + 5 - 0) MOD 5= 3/\ 0 MOD 5=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`;`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;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M3;K_SCS_4M6_prime] 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_5M3;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M6_prime;scs_3T4_prime;scs_5M3; ARITH_RULE`(0+1 + 5 - 2) MOD 5= 4/\ 2 MOD 5=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 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION] 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[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[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=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_4_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_4_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_4_TAC;Uxckfpe.ARITH_6_TAC] THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+x:num`;`1+x':num`][ARITH_RULE`~(4=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_prime]]);; let SCS_5M3_02_ARROW_3T4_4M6=prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 0 2 } {scs_3T4, scs_4M6'}`, [MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_3T4_prime 2, scs_prop_equ_v39 scs_4M6_prime 1}` THEN ASM_REWRITE_TAC[SCS_5M3_SLICE_02;SET_RULE`{A,B}={A}UNION {B}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_3T4_prime}` THEN ASM_REWRITE_TAC[SCS_3T4_prime_ARROW_MM_3T4] THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T4_prime`;`2`;`3`][SCS_3T4_prime_IS_SCS;K_SCS_3T4_prime;ARITH_RULE`(3 - 2 MOD 3)=1`] THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T4_prime 2`;`1`][PROP_EQU_IS_SCS;SCS_3T4_prime_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_4M6_prime}` THEN ASM_REWRITE_TAC[SCS_4M6_prime_ARROW_MM_4M6] THEN MRESAS_TAC PRO_EQU_ID1[`scs_4M6_prime`;`1`;`4`][SCS_4M6_prime_IS_SCS;K_SCS_4M6_prime;ARITH_RULE`(4 - 1 MOD 4)=3`] THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M6_prime 1`;`3`][PROP_EQU_IS_SCS;SCS_4M6_prime_IS_SCS] THEN DICH_TAC 0 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th]) THEN REWRITE_TAC[]]);; (************03***********) let SCS_5M3_SLICE_03=prove_by_refinement( `scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 0 3 } { scs_prop_equ_v39 scs_4M7_prime 1,scs_prop_equ_v39 scs_3T1_prime 1}`, [ MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI) THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_03;STAB_5M3_SCS;SCS_K_D_A_STAB_EQ;] THEN EXISTS_TAC`0` THEN EXISTS_TAC`3` THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_03] 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_5M3_BASIC;SCS_3T1_prime_BASIC;J_SCS_4M7_prime;BASIC_HALF_SLICE_STAB;J_SCS_3T1_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4M7_prime_BASIC] THEN STRIP_TAC; ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_4M7_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M3] 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_5M3;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7_prime;scs_3T1_prime;scs_5M3; ARITH_RULE`(3+1 + 5 - 0) MOD 5= 4/\ 0 MOD 5=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 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION] 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[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[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=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_4_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_4_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_4_TAC;Uxckfpe.ARITH_6_TAC] THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+x:num`;`1+x':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`] THEN SYM_ASSUM_TAC THEN SCS_TAC; ASM_SIMP_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_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M3;K_SCS_4M7_prime] 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_5M3;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;scs_3T1_prime;scs_5M3; ARITH_RULE`(0 + 1 + 5 - 3) MOD 5= 3/\ 3 MOD 5=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`;`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_4M7_prime]; ]);; let BB_3T1_prime_IMP_scs_3T1=prove( `BBs_v39 scs_3T1_prime v ==> BBs_v39 (scs_3T1 ) v`, REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`((3<=3))`;IN;K_SCS_3T1_prime;K_SCS_3T1;scs_prop_equ_v39;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN SCS_TAC THEN REPEAT RESA_TAC THEN THAYTHE_TAC 0[`i`;`j`] THEN DICH_TAC 1 THEN REWRITE_TAC[cstab;h0] THEN MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC);; let MM_3T1_prime_IMP_MM_3T1=prove( `MMs_v39 scs_3T1_prime v ==> ~(MMs_v39 scs_3T1 ={})`, STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC`scs_3T1_prime` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_3T1_prime`;`v`] THEN ASM_SIMP_TAC[SCS_3T1_BASIC;SCS_3T1_prime_BASIC;SCS_3T1_IS_SCS;SCS_3T1_IS_SCS; SCS_3T1_prime_IS_SCS;K_SCS_3T1;K_SCS_3T1_prime;IN;BB_3T1_prime_IMP_scs_3T1] THEN SCS_TAC THEN REAL_ARITH_TAC);; let SCS_3T1_prime_ARROW_MM_3T1=prove_by_refinement(`scs_arrow_v39 {scs_3T1_prime } { scs_3T1}`, [ 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_3T1_IS_SCS]; DISJ_CASES_TAC(SET_RULE`(!s. s = scs_3T1_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_3T1_prime ==> 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_3T1` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC (GEN_ALL MM_3T1_prime_IMP_MM_3T1) THEN POP_ASSUM MP_TAC THEN SET_TAC[]]);; let BB_4M7_prime_IMP_scs_4M7=prove(`BBs_v39 scs_4M7_prime v ==> BBs_v39 (scs_4M7 ) v`, REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4M7_prime;K_SCS_4M7;scs_prop_equ_v39;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN SCS_TAC THEN REPEAT RESA_TAC THEN THAYTHE_TAC 1[`i`;`j`] THEN DICH_TAC 1 THEN REWRITE_TAC[cstab;h0] THEN REAL_ARITH_TAC);; let MM_4M7_prime_IMP_MM_4M7=prove( `MMs_v39 scs_4M7_prime v ==> ~(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_4M7_prime` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M7_prime`;`v`] THEN ASM_SIMP_TAC[SCS_4M7_BASIC;SCS_4M7_prime_BASIC;SCS_4M7_IS_SCS;SCS_4M7_IS_SCS; SCS_4M7_prime_IS_SCS;K_SCS_4M7;K_SCS_4M7_prime;IN;BB_4M7_prime_IMP_scs_4M7] THEN SCS_TAC THEN REAL_ARITH_TAC);; let SCS_4M7_prime_ARROW_MM_4M7=prove_by_refinement(`scs_arrow_v39 {scs_4M7_prime } { scs_4M7}`, [ 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_4M7_IS_SCS]; DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M7_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M7_prime ==> 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_4M7` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC (GEN_ALL MM_4M7_prime_IMP_MM_4M7) THEN POP_ASSUM MP_TAC THEN SET_TAC[]]);; let SCS_5M3_03_ARROW_3T1_4M7=prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 0 3 } { scs_4M7,scs_3T1}`, [ MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_4M7_prime 1, scs_prop_equ_v39 scs_3T1_prime 1}` THEN ASM_REWRITE_TAC[SCS_5M3_SLICE_03;SET_RULE`{A,B}={A}UNION {B}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_4M7_prime}` THEN ASM_REWRITE_TAC[SCS_4M7_prime_ARROW_MM_4M7] THEN MRESAS_TAC PRO_EQU_ID1[`scs_4M7_prime`;`1`;`4`][SCS_4M7_prime_IS_SCS;K_SCS_4M7_prime;ARITH_RULE`(4 - 1 MOD 4)=3`] THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M7_prime 1`;`3`][PROP_EQU_IS_SCS;SCS_4M7_prime_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_3T1_prime}` THEN ASM_REWRITE_TAC[SCS_3T1_prime_ARROW_MM_3T1] THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T1_prime`;`1`;`3`][SCS_3T1_prime_IS_SCS;K_SCS_3T1_prime;ARITH_RULE`(3 - 1 MOD 3)=2`] THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T1_prime 1`;`2`][PROP_EQU_IS_SCS;SCS_3T1_prime_IS_SCS] THEN DICH_TAC 0 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th]) THEN REWRITE_TAC[]]);; (*************24**************) let SCS_5M3_SLICE_24=prove_by_refinement( `scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 2 4 } {scs_prop_equ_v39 scs_3T1_prime 1,scs_prop_equ_v39 scs_4M8_prime 3}`, [ MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI) THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_24;STAB_5M3_SCS;SCS_K_D_A_STAB_EQ;] THEN EXISTS_TAC`2` THEN EXISTS_TAC`4` THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_24] 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_5M3_BASIC;SCS_3T1_prime_BASIC;J_SCS_4M8_prime1;BASIC_HALF_SLICE_STAB;J_SCS_3T1_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4M8_prime_BASIC] THEN STRIP_TAC; ASM_SIMP_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_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M3] 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_5M3;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;scs_3T1_prime;scs_5M3; ARITH_RULE`(4 + 1 + 5 - 2) MOD 5= 3/\ 2 MOD 5=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; ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_4M8_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M3;K_SCS_4M8_prime] 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_5M3;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_prime;scs_3T1_prime;scs_5M3; ARITH_RULE`(2+1 + 5 - 4) MOD 5= 4/\ 4 MOD 5=4/\ 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 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION] 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[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[`4`;`x`;`0`;`3`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`3`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`3`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`3`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`3`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`3`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`3`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`3`][ARITH_RULE`~(4=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_4_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_4_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_4_TAC;Uxckfpe.ARITH_6_TAC] THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`3+x:num`;`3+x':num`][ARITH_RULE`~(4=0)/\ 3+3=6/\ 3+1=4/\ 4 MOD 3=1/\ 2+4=6/\ 6 MOD 4=2/\ 3+4=7/\ 7 MOD 5=2`] 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_prime]; ]);; let BB_4M8_prime_IMP_scs_4M8=prove(`BBs_v39 scs_4M8_prime v ==> BBs_v39 (scs_4M8 ) v`, REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4M8_prime;K_SCS_4M8;scs_prop_equ_v39;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN SCS_TAC THEN REPEAT RESA_TAC THEN THAYTHE_TAC 1[`i`;`j`] THEN DICH_TAC 1 THEN REWRITE_TAC[cstab;h0] THEN REAL_ARITH_TAC);; let MM_4M8_prime_IMP_MM_4M8=prove( `MMs_v39 scs_4M8_prime v ==> ~(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_4M8_prime` THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8_prime`;`v`] THEN ASM_SIMP_TAC[SCS_4M8_BASIC;SCS_4M8_prime_BASIC;SCS_4M8_IS_SCS;SCS_4M8_IS_SCS; SCS_4M8_prime_IS_SCS;K_SCS_4M8;K_SCS_4M8_prime;IN;BB_4M8_prime_IMP_scs_4M8] THEN SCS_TAC THEN REAL_ARITH_TAC);; let SCS_4M8_prime_ARROW_MM_4M8=prove_by_refinement(`scs_arrow_v39 {scs_4M8_prime } { scs_4M8}`, [ 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_4M8_IS_SCS]; DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M8_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M8_prime ==> 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_4M8` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC (GEN_ALL MM_4M8_prime_IMP_MM_4M8) THEN POP_ASSUM MP_TAC THEN SET_TAC[]]);; let SCS_5M3_24_ARROW_3T1_4M8=prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 2 4 } { scs_3T1,scs_4M8}`, [ MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_3T1_prime 1,scs_prop_equ_v39 scs_4M8_prime 3}` THEN ASM_REWRITE_TAC[SCS_5M3_SLICE_24;SET_RULE`{A,B}={A}UNION {B}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC; MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_3T1_prime}` THEN ASM_REWRITE_TAC[SCS_3T1_prime_ARROW_MM_3T1] THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T1_prime`;`1`;`3`][SCS_3T1_prime_IS_SCS;K_SCS_3T1_prime;ARITH_RULE`(3 - 1 MOD 3)=2`] THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T1_prime 1`;`2`][PROP_EQU_IS_SCS;SCS_3T1_prime_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_4M8_prime}` THEN ASM_REWRITE_TAC[SCS_4M8_prime_ARROW_MM_4M8] THEN MRESAS_TAC PRO_EQU_ID1[`scs_4M8_prime`;`3`;`4`][SCS_4M8_prime_IS_SCS;K_SCS_4M8_prime;ARITH_RULE`(4 - 3 MOD 4)=1`] THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M8_prime 3`;`1`][PROP_EQU_IS_SCS;SCS_4M8_prime_IS_SCS] THEN DICH_TAC 0 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th]) THEN REWRITE_TAC[]]);; (************) let PROP_OPP_DIAG_5M3_03= prove_by_refinement(`scs_stab_diag_v39 scs_5M3 0 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_5M3 1 3)) 3 `, [REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; scs_basic;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_5M3_BASIC] THEN STRIP_TAC; MRESAL_TAC STAB_5M3_SCS[`0`;`3`][K_SCS_5M3;scs_diag;ARITH_RULE`~(0 MOD 5 = 3 MOD 5) /\ ~(SUC 0 MOD 5 = 3 MOD 5) /\ ~(0 MOD 5 = SUC 3 MOD 5)`]; STRIP_TAC; 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 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`~(5=0)`) THEN MRESA_TAC PSORT_MOD[`5`;`x`;`x'`] THEN SYM_ASSUM_TAC THEN MRESA_TAC MOD_ADD_MOD[`3`;`x`;`5`] THEN MRESA_TAC MOD_ADD_MOD[`3`;`x'`;`5`] THEN SYM_ASSUM_TAC THEN SYM_ASSUM_TAC THEN MP_TAC(ARITH_RULE`x MOD 5<5==> x MOD 5=0\/ x MOD 5=1\/ x MOD 5=2\/ x MOD 5=3\/x MOD 5=4`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 5<5==> x' MOD 5=0\/ x' MOD 5=1\/ x' MOD 5=2\/ x' MOD 5=3\/x' MOD 5=4`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;ARITH_RULE`5-1=4/\ 5-2=3/\ 5-3=2/\ 5-4=1/\ 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]]);; let PROP_OPP_DIAG_5M3_02= prove_by_refinement(`scs_stab_diag_v39 scs_5M3 0 2= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_5M3 1 4)) 3 `, [REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; scs_basic;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_5M3_BASIC] THEN STRIP_TAC; MRESAL_TAC STAB_5M3_SCS[`0`;`2`][K_SCS_5M3;scs_diag;ARITH_RULE`~(0 MOD 5 = 2 MOD 5) /\ ~(SUC 0 MOD 5 = 2 MOD 5) /\ ~(0 MOD 5 = SUC 2 MOD 5)`]; STRIP_TAC; 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 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`~(5=0)`) THEN MRESA_TAC PSORT_MOD[`5`;`x`;`x'`] THEN SYM_ASSUM_TAC THEN MRESA_TAC MOD_ADD_MOD[`3`;`x`;`5`] THEN MRESA_TAC MOD_ADD_MOD[`3`;`x'`;`5`] THEN SYM_ASSUM_TAC THEN SYM_ASSUM_TAC THEN MP_TAC(ARITH_RULE`x MOD 5<5==> x MOD 5=0\/ x MOD 5=1\/ x MOD 5=2\/ x MOD 5=3\/x MOD 5=4`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 5<5==> x' MOD 5=0\/ x' MOD 5=1\/ x' MOD 5=2\/ x' MOD 5=3\/x' MOD 5=4`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;ARITH_RULE`5-1=4/\ 5-2=3/\ 5-3=2/\ 5-4=1/\ 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]]);; let SET_STAB_5M3=prove(`{ scs_stab_diag_v39 scs_5M3 i j| scs_diag 5 i j }= { scs_stab_diag_v39 scs_5M3 (i MOD 5) (j MOD 5)| scs_diag 5 (i MOD 5) (j MOD 5) }`, ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(5=0)`;] THEN MRESAL_TAC STAB_MOD[`scs_5M3`][SCS_5M3_IS_SCS;K_SCS_5M3]);; let EXPAND_STAB_DIAG_5M3=prove(`{scs_stab_diag_v39 scs_5M3 (i MOD 5) (j MOD 5) | i MOD 5 = (j MOD 5 + 2) MOD 5 \/ j MOD 5 = (i MOD 5 + 2) MOD 5}= {scs_stab_diag_v39 scs_5M3 (i+2) i| i<5} `, ASM_SIMP_TAC[EXPAND_STAB_DIAG_5;SCS_5M3_IS_SCS;K_SCS_5M3]);; let SET_EQ_DIAG_STAB_5M3= prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 i j | scs_diag 5 i j} {scs_stab_diag_v39 scs_5M3 0 2, scs_stab_diag_v39 scs_5M3 0 3, scs_stab_diag_v39 scs_5M3 2 4}`, [ ONCE_REWRITE_TAC[SET_STAB_5M3] THEN REWRITE_TAC[DIAG_EQ_ADD5;EXPAND_STAB_DIAG_5I3;EXPAND_STAB_DIAG_5M3] THEN REWRITE_TAC[ARITH_RULE`i<5<=> i=0\/i=1\/i=2\/i=3\/i=4`; SET_RULE`{A,B,C} = {A}UNION {B}UNION {C}UNION {B}UNION {A} `;SET_RULE`{scs_stab_diag_v39 scs_5M3 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4} = {scs_stab_diag_v39 scs_5M3 (0 + 2) 0} UNION {scs_stab_diag_v39 scs_5M3 (1 + 2) 1} UNION {scs_stab_diag_v39 scs_5M3 (2 + 2) 2} UNION {scs_stab_diag_v39 scs_5M3 (3 + 2) 3} UNION {scs_stab_diag_v39 scs_5M3 (4 + 2) 4} `;] THEN MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC; REWRITE_TAC[ARITH_RULE`0+2=2`;STAB_SYM] THEN MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN MRESAL_TAC STAB_5M3_SCS[`2`;`0`][scs_diag;K_SCS_5M3;ARITH_RULE`~(2 MOD 5 = 0 MOD 5) /\ ~(SUC 2 MOD 5 = 0 MOD 5) /\ ~(2 MOD 5 = SUC 0 MOD 5)`]; MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC; REWRITE_TAC[ARITH_RULE`1+2=3`;STAB_SYM;PROP_OPP_DIAG_5M3_03] THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_5M3 1 3)}` THEN STRIP_TAC; MATCH_MP_TAC (GEN_ALL YXIONXL2) THEN EXISTS_TAC`5` THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(5<=3)`;K_SCS_5M3] THEN MRESAL_TAC STAB_5M3_SCS[`1`;`3`][scs_diag;K_SCS_5M3;ARITH_RULE`~(1 MOD 5 = 3 MOD 5) /\ ~(SUC 1 MOD 5 = 3 MOD 5) /\ ~(1 MOD 5 = SUC 3 MOD 5)`]; 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_5M3 1 3)` THEN MRESAL_TAC STAB_5M3_SCS[`1`;`3`][scs_diag;K_SCS_5M3;ARITH_RULE`~(1 MOD 5 = 3 MOD 5) /\ ~(SUC 1 MOD 5 = 3 MOD 5) /\ ~(1 MOD 5 = SUC 3 MOD 5)`]; MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC; REWRITE_TAC[ARITH_RULE`2+2=4`;STAB_SYM] THEN MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN MRESAL_TAC STAB_5M3_SCS[`2`;`4`][scs_diag;K_SCS_5M3;ARITH_RULE`~(2 MOD 5 = 4 MOD 5) /\ ~(SUC 2 MOD 5 = 4 MOD 5) /\ ~(2 MOD 5 = SUC 4 MOD 5)`]; MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC; REWRITE_TAC[ARITH_RULE`3+2=5`;STAB_SYM] THEN MRESAL_TAC STAB_MOD[`scs_5M3`;`5`;`3`][SCS_5M3_IS_SCS;K_SCS_5M3;ARITH_RULE`5 MOD 5=0/\ 3 MOD 5=3`] THEN SYM_ASSUM_TAC THEN REWRITE_TAC[ARITH_RULE`3+2=5`;STAB_SYM] THEN MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN MRESAL_TAC STAB_5M3_SCS[`3`;`0`][scs_diag;K_SCS_5M3;ARITH_RULE`~(3 MOD 5 = 0 MOD 5) /\ ~(SUC 3 MOD 5 = 0 MOD 5) /\ ~(3 MOD 5 = SUC 0 MOD 5)`]; REWRITE_TAC[ARITH_RULE`4+2=6`;] THEN MRESAL_TAC STAB_MOD[`scs_5M3`;`6`;`4`][SCS_5M3_IS_SCS;K_SCS_5M3;ARITH_RULE`6 MOD 5=1/\ 4 MOD 5=4`] THEN SYM_ASSUM_TAC THEN REWRITE_TAC[PROP_OPP_DIAG_5M3_02]; MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_5M3 1 4)}` THEN STRIP_TAC; MATCH_MP_TAC (GEN_ALL YXIONXL2) THEN EXISTS_TAC`5` THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(5<=3)`;K_SCS_5M3] THEN MRESAL_TAC STAB_5M3_SCS[`1`;`4`][scs_diag;K_SCS_5M3;ARITH_RULE`~(1 MOD 5 = 4 MOD 5) /\ ~(SUC 1 MOD 5 = 4 MOD 5) /\ ~(1 MOD 5 = SUC 4 MOD 5)`]; 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_5M3 1 4)` THEN MRESAL_TAC STAB_5M3_SCS[`1`;`4`][scs_diag;K_SCS_5M3;ARITH_RULE`~(1 MOD 5 = 4 MOD 5) /\ ~(SUC 1 MOD 5 = 4 MOD 5) /\ ~(1 MOD 5 = SUC 4 MOD 5)`]]);; let SET_EQ_DIAG_STAB_5M3_IMP_SCS_3_4=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 i j | scs_diag 5 i j} {scs_4M6',scs_4M7,scs_4M8,scs_3T1,scs_3T4}`, MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_stab_diag_v39 scs_5M3 0 2, scs_stab_diag_v39 scs_5M3 0 3, scs_stab_diag_v39 scs_5M3 2 4}` THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_5M3;SET_RULE`{scs_4M6', scs_4M7, scs_4M8, scs_3T1, scs_3T4}= {scs_3T4, scs_4M6'}UNION{scs_4M7,scs_3T1}UNION{ scs_3T1,scs_4M8}`] THEN REWRITE_TAC[SET_RULE`{A,B,C}={A}UNION{B}UNION{C}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN REWRITE_TAC[SCS_5M3_02_ARROW_3T4_4M6] THEN MATCH_MP_TAC FZIOTEF_UNION THEN REWRITE_TAC[SCS_5M3_03_ARROW_3T1_4M7;SCS_5M3_24_ARROW_3T1_4M8]);; (**************) let h0_LT_B_SCS_5M2=prove(` (!i j. scs_diag 5 i j ==> &4 * h0 < scs_b_v39 scs_5M2 i j) /\ (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5M2 i j <= cstab)`, SCS_TAC THEN REWRITE_TAC[h0;scs_diag;cstab] THEN REPEAT RESA_TAC THEN MP_TAC DIAG_5_EQU_PSORT THEN RESA_TAC THEN REWRITE_TAC[PAIR_EQ;] THEN SCS_TAC THEN REAL_ARITH_TAC);; let B_LE_CSTAB_5M2=prove(` (!i. scs_b_v39 scs_5M2 i (SUC i) <= cstab)/\ (!i. scs_a_v39 scs_5M2 i (SUC i) = &2) `, SCS_TAC THEN SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;h0;cstab] THEN REPEAT RESA_TAC THEN MRESAS_TAC PSORT_MOD[`5`;`i`;`SUC i`][ARITH_RULE`~(5=0)`] THEN SYM_ASSUM_TAC THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`] THEN SYM_ASSUM_TAC THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN SCS_TAC THEN REAL_ARITH_TAC);; let B_LE_CSTAB_5M2_A_LT_B=prove(` (!i. &2 < scs_b_v39 scs_5M2 i (SUC i)) `, SCS_TAC THEN SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;h0;cstab] THEN REPEAT RESA_TAC THEN MRESAS_TAC PSORT_MOD[`5`;`i`;`SUC i`][ARITH_RULE`~(5=0)`] THEN SYM_ASSUM_TAC THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`] THEN SYM_ASSUM_TAC THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`] THEN RESA_TAC THEN SCS_TAC THEN REAL_ARITH_TAC);; let CARD_SCS_M_5M2=prove(`CARD (scs_M scs_5M2) <= 1`, ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a x=0\/ x=1\/x=2\/ x=3\/ x=4`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a x=0\/ x=1\/x=2\/ x=3\/ x=4`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a(!s (v:num->real^3) i. 3< scs_k_v39 s/\ is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\ ( dist(v i,v (i+1)) = &2) /\ CARD (scs_M s) <= 1 /\ (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j) /\ &4 * h0 < scs_b_v39 s i j)) /\ (!i. scs_a_v39 s i (i+1)< scs_b_v39 s i (i+1)) ==> (?i1. ~(i1 MOD scs_k_v39 s IN scs_M s)/\ dist(v i1, v (i1+1)) = &2))`, [STRIP_TAC THEN REPEAT GEN_TAC THEN ABBREV_TAC`k= scs_k_v39 s` THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)` THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)` THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)` THEN REPEAT RESA_TAC THEN MP_TAC(SET_RULE`i MOD k IN scs_M s\/ ~(i MOD k IN scs_M s)`) THEN RESA_TAC; SUBGOAL_THEN`scs_M s={i MOD k}`ASSUME_TAC; MRESAS_TAC CARD_SUBSET_LE[`{i MOD k}`;`scs_M s`][Jlxfdmj.FINITE_SCS_M;SET_RULE`a IN A==> {a} SUBSET A`;Geomdetail.CARD_SING]; MRESA_TAC Jlxfdmj.SCS_M_EQ_1[`i MOD k`;`s`] THEN THAYTHES_TAC 0[`SUC i`][SET_RULE`(SUC i MOD k = i MOD k)<=> (i MOD k = SUC i MOD k)`;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`3 1 &2 < scs_b_v39 s i (i + 1)`) THEN RESA_TAC THEN STRIP_TAC THEN EXISTS_TAC`SUC i` THEN ASM_SIMP_TAC[Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`3 1 ~(b=a)`;ARITH_RULE`SUC i= i+1/\ (i + 1) + 1= i+2`]; EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[]]);; let JCYFMRP_V2 = prove_by_refinement( `main_nonlinear_terminal_v11 ==>(!s (v:num->real^3) i. 3< scs_k_v39 s/\ is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\ ( dist(v i,v (i+1)) = &2) /\ CARD (scs_M s) <= 1 /\ (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j) /\ &4 * h0 < scs_b_v39 s i j)) /\ (!i. scs_a_v39 s i (i+1)< scs_b_v39 s i (i+1)) ==> (?i1. scs_b_v39 s i1 (SUC i1) <= &2 * h0/\ scs_a_v39 s i1 (SUC i1) = &2/\ dist(v i1, v (i1+1)) = &2))`, [STRIP_TAC THEN REPEAT GEN_TAC THEN ABBREV_TAC`k= scs_k_v39 s` THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)` THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)` THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)` THEN REPEAT RESA_TAC THEN MP_TAC(SET_RULE`i MOD k IN scs_M s\/ ~(i MOD k IN scs_M s)`) THEN RESA_TAC; SUBGOAL_THEN`scs_M s={i MOD k}`ASSUME_TAC; MRESAS_TAC CARD_SUBSET_LE[`{i MOD k}`;`scs_M s`][Jlxfdmj.FINITE_SCS_M;SET_RULE`a IN A==> {a} SUBSET A`;Geomdetail.CARD_SING]; MRESA_TAC Jlxfdmj.SCS_M_EQ_1[`i MOD k`;`s`] THEN THAYTHES_TAC 0[`SUC i`][SET_RULE`(SUC i MOD k = i MOD k)<=> (i MOD k = SUC i MOD k)`;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`3 1 &2 < scs_b_v39 s i (i + 1)`) THEN RESA_TAC THEN STRIP_TAC THEN EXISTS_TAC`SUC i` THEN ASM_SIMP_TAC[Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`3 1 ~(b=a)`;ARITH_RULE`SUC i= i+1/\ (i + 1) + 1= i+2`]; EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`CARD (scs_M s)<= 1==> CARD (scs_M s)= 0\/ CARD (scs_M s)=1`) THEN RESA_TAC; MP_TAC Jlxfdmj.SCS_M_EQ_0 THEN RESA_TAC; MRESAS_TAC Local_lemmas.FINITE_CARD1_IMP_SINGLETON[`scs_M s`][Jlxfdmj.FINITE_SCS_M;SET_RULE`~(a IN {x})<=> ~(a=x)`] THEN STRIP_TAC THEN MP_TAC Jlxfdmj.SCS_M_EQ_1 THEN RESA_TAC THEN THAYTHE_TAC 0[`i`]]);; let JCYFMRP_V3=prove(`main_nonlinear_terminal_v11 ==>(!s (v:num->real^3). 3< scs_k_v39 s/\ is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\ CARD (scs_M s) <= 1 /\ (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j) /\ &4 * h0 < scs_b_v39 s i j)) /\ (!i. scs_a_v39 s i (i+1)< scs_b_v39 s i (i+1)) /\ (!i. scs_a_v39 s i (SUC i) = &2) ==> (?i. scs_b_v39 s i (SUC i) <= &2 * h0/\ scs_a_v39 s i (SUC i) = &2/\ dist(v i, v (i+1)) = &2))`, REPEAT RESA_TAC THEN MP_TAC Jcyfmrp.JCYFMRP THEN RESA_TAC THEN THAYTHE_TAC 0[`s`;`v`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN MP_TAC JCYFMRP_V2 THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN THAYTHE_TAC 0[`s`;`v`;`i`]);; (*********************) let ARC_222=prove(`arclength (&2) (&2) (&2)= pi/ &3`, MRESAS_TAC Trigonometry.PQQDENV[`&2`;`&2`;`&2`][REAL_ARITH`&0 < &2 /\ &0 < &2 /\ &0 <= &2 /\ &2 <= &2 + &2/\ (&2 * &2 + &2 * &2 - &2 * &2) / (&2 * &2 * &2)= &1/ &2`;Nonlinear_lemma.ACS_2]);; let xrr_le_1553=prove(` v IN ball_annulus/\ u IN ball_annulus/\ w IN ball_annulus /\ ~collinear {vec 0, v, u} /\ dist(v,w)= &2/\ dist(w,u)= &2 ==> xrr (norm v) (norm u) (norm(v-u))<= #15.53`, REPEAT RESA_TAC THEN MRESA_TAC Counting_spheres.ckq_in_ball_annulus[`v`] THEN MRESA_TAC Counting_spheres.ckq_in_ball_annulus[`u`] THEN MRESA_TAC Counting_spheres.ckq_in_ball_annulus[`w`] THEN MRESA_TAC Trigonometry2.ARCV_INEQUALTY[`vec 0:real^3`;`v`;`u`;`w`] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v`;`w`;`&2`][REAL_ARITH`&2 < &4 /\ &2 <= &2 `;ARC_222] THEN MRESAL_TAC Ppbtydq.OIQKKEP[`w`;`u`;`&2`][REAL_ARITH`&2 < &4 /\ &2 <= &2 `;ARC_222] THEN MP_TAC(REAL_ARITH`arcV (vec 0) v u <= arcV (vec 0) v w + arcV (vec 0) w u /\ arcV (vec 0) v w <= pi / &3/\ arcV (vec 0) w u <= pi / &3 ==> arcV (vec 0:real^3) v u<= &2 * pi/ &3`) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`v`;`u`] THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- a= --a:real^3`;NORM_NEG] THEN MRESAL_TAC th3[`v`;`vec 0:real^3`;`u:real^3`][GSYM dist;VECTOR_ARITH`v - u = vec 0 <=> v=u:real^3`] THEN DICH_TAC 0 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`] THEN RESA_TAC THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`v`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A:real^3`] THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`u`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A:real^3`] THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`v`;`u:real^3`][VECTOR_ARITH`A- vec 0=A:real^3`] THEN MRESAL_TAC Collect_geom2.NOT_COL_EQ_UPS_X_POS[`vec 0:real^3`;`v`;`u`][dist;VECTOR_ARITH`vec 0- a= --a:real^3`;NORM_NEG] THEN MRESAL_TAC arclength_xrr[`norm v`;`norm u`;`norm (v- u)`][REAL_ARITH`a*a= a pow 2`] THEN STRIP_TAC THEN MRESAL_TAC ACS_NEG[`&1/ &2`][REAL_ARITH`-- &1 <= &1 / &2 /\ &1 / &2 <= &1/\ pi - pi / &3= &2* pi/ &3`;Nonlinear_lemma.ACS_2] THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`norm v`;`norm u`;`norm (v-u)`][REAL_ARITH`a*a= a pow 2`] THEN MP_TAC(REAL_ARITH`&0 < xrr (norm v) (norm u) (norm (v - u))/\ xrr (norm v) (norm u) (norm (v - u)) < &16 ==> abs (&1 - xrr (norm v) (norm u) (norm (v - u:real^3)) / &8) <= &1`) THEN RESA_TAC THEN MRESAL_TAC ACS_MONO_LE_EQ[`&1 - xrr (norm v) (norm u) (norm (v - u)) / &8`;`--( &1/ &2)`][REAL_ARITH`abs (--(&1 / &2)) <= &1`] THEN DICH_TAC 0 THEN REAL_ARITH_TAC);; let xrr_le_1553_BB=prove(`BBs_v39 s v /\ dist(v i, v (i+1))= &2/\ dist( v (i+1), v(i+2))= &2 /\ ~(collinear{vec 0 , v i, v (i+2)}) ==> xrr (norm (v i)) (norm (v (i+2))) (norm(v i- v (i+2)))<= #15.53 `, STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL xrr_le_1553) THEN EXISTS_TAC`(v:num->real^3) (i+1)` THEN ASM_SIMP_TAC[] THEN MRESA_TAC Nuxcoea.WL_IN_BALL_ANNULUS[`s`;`v`;`i`] THEN MRESA_TAC Nuxcoea.WL_IN_BALL_ANNULUS[`s`;`v`;`i+1`] THEN MRESA_TAC Nuxcoea.WL_IN_BALL_ANNULUS[`s`;`v`;`i+2`]);; (******************************) let J_SCS_5M2_0=prove(`(!i j. ~scs_J_v39 scs_5M2 j i)`, SCS_TAC);; let SCS_5M2_IMP_SCS_5T1= prove_by_refinement(`main_nonlinear_terminal_v11 ==>(!v. v IN MMs_v39 scs_5M2 /\ (!i j. scs_diag 5 i j ==> cstab < dist(v i,v j)) ==> ~(MMs_v39 (scs_5T1)={}))`, [ REWRITE_TAC[IN;SET_RULE`~(A={})<=> ?a. a IN A`] THEN REPEAT STRIP_TAC THEN MP_TAC SCS_5M2_IS_SCS THEN STRIP_TAC THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`] THEN ASSUME_TAC SCS_5M2_BASIC THEN ASSUME_TAC K_SCS_5M2 THEN ASSUME_TAC SCS_5T1_BASIC THEN ASSUME_TAC K_SCS_5T1 THEN ASSUME_TAC SCS_5T1_IS_SCS THEN MP_TAC Rrcwnsj.RRCWNSJ THEN RESA_TAC THEN THAYTHES_TAC 0[`scs_5M2`;`v`][ARITH_RULE`3<5`;h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2] THEN MP_TAC JCYFMRP_V3 THEN RESA_TAC THEN THAYTHES_TAC 0[`scs_5M2`;`v`][ARITH_RULE`3<5`;h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2;IN;CARD_SCS_M_5M2;GSYM ADD1;B_LE_CSTAB_5M2_A_LT_B] THEN MP_TAC Jlxfdmj.JLXFDMJ THEN RESA_TAC THEN THAYTHES_TAC 0[`scs_5M2`;`v`;`i`][ARITH_RULE`3<5`;h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2;CARD_SCS_M_5M2;SCS_M_5M2;IN_SING;] THEN DICH_TAC 0 THEN ASM_REWRITE_TAC[IN;GSYM ADD1;B_LE_CSTAB_5M2;B_LE_CSTAB_5M2_A_LT_B] THEN STRIP_TAC THEN ABBREV_TAC`V=(IMAGE (v:num->real^3) (:num))` THEN ABBREV_TAC`E=(IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num))` THEN ABBREV_TAC`FF=IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)` THEN SUBGOAL_THEN`dist((v:num->real^3) 0, v 1)= &2`ASSUME_TAC; ASSUME_TAC(ARITH_RULE`3<5/\ 0+1=1/\ 0+5-1=4`) THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`5`;`scs_5M2`;`v`] THEN MP_TAC Local_lemmas.CVLF_LF_F THEN RESA_TAC THEN MRESA_TAC WL_IN_V[`0`;`v:num->real^3`] THEN MRESA_TAC WL_IN_V[`1`;`v:num->real^3`] THEN MRESA_TAC WL_IN_V[`2`;`v:num->real^3`] THEN MRESA_TAC WL_IN_V[`3`;`v:num->real^3`] THEN MRESA_TAC WL_IN_V[`4`;`v:num->real^3`] THEN MRESAL_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`scs_5M2`;`FF`;`v (0)`;`v`;`0`;`5`][] THEN MRESA_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v 0`] THEN THAYTHE_TAC 0[`v 4`] THEN MP_TAC(REAL_ARITH`azim (vec 0) (v 0) (v 1) (v 4) <= pi ==> azim (vec 0) ((v:num->real^3) 0) (v 1) (v 4) = pi\/ azim (vec 0) (v 0) (v 1) (v 4) < pi`) THEN RESA_TAC; DICH_TAC(29-10) THEN REWRITE_TAC[scs_generic] THEN RESA_TAC THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_5M2`] THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v 1`;`v 4`;`V`] THEN THAYTHEL_ASM_TAC 0[`v 1`;`v 4`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Uxckfpe.ARITH_5_TAC] THEN SUBGOAL_THEN`(!j. ~(j MOD 5 = 4 MOD 5) ==> ~collinear {vec 0, v 4, (v:num->real^3)j})`ASSUME_TAC ; REPEAT RESA_TAC THEN DICH_TAC 0 THEN THAYTHE_TAC 1[`v 4`;`v j`] THEN MATCH_DICH_TAC 0 THEN REWRITE_TAC[SET_RULE`a IN {b,a}`] THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`] ; THAYTHEL_ASM_TAC (33-30)[`4+1`;`0`][ARITH_RULE`( 4+1) MOD 5 = 0 MOD 5`] THEN THAYTHEL_ASM_TAC 0[`4+2`;`1`][ARITH_RULE`( 4+2) MOD 5 = 1 MOD 5`] THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v 0`;`v 1`;`(v:num->real^3) 4`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`] THEN STRIP_TAC THEN MRESA_TAC Iunbuig.coplanar_aff_gt_simple[`scs_5M2`;`5`;`v`;`4`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN STRIP_TAC THEN SUBGOAL_THEN`(!i. scs_diag 5 0 i ==> scs_a_v39 scs_5M2 0 i < dist ((v:num->real^3) 0,v i))`ASSUME_TAC; REPEAT RESA_TAC THEN THAYTHE_TAC(38-2)[`0`;`i'`] THEN MP_TAC h0_LT_B_SCS_5M2 THEN STRIP_TAC THEN THAYTHE_TAC 0[`0`;`i'`] THEN DICH_TAC 0 THEN DICH_TAC 1 THEN REAL_ARITH_TAC; MRESAL_TAC MMS_IMP_BBPRIME[`scs_5M2`;`v`][LET_DEF;LET_END_DEF;BBprime_v39] THEN MRESAL_TAC JKQEWGV2[`scs_5M2`;`v`][LET_DEF;LET_END_DEF;scs_generic] THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH THEN RESA_TAC THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) 0) V E)`ASSUME_TAC ; REPEAT RESA_TAC THEN DICH_TAC 3 THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`v1:real^3` THEN EXISTS_TAC`(v:num->real^3)0` THEN ASM_REWRITE_TAC[] ; MRESAS_TAC NUXCOEAv2[`scs_5M2`;`5`;`v`;`0`;`4`][ARITH_RULE`SUC 0=1/\ SUC 4 MOD 5 = 0 MOD 5`;h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2;J_SCS_5M2_0] THEN DICH_TAC 0 THEN DICH_TAC 0 THEN MATCH_MP_TAC(SET_RULE`(A==> (B/\A1==>C)==>D)==> (A==>(B/\ A1/\A==>C)==>D)`) THEN STRIP_TAC THEN SCS_TAC THEN THAYTHES_TAC(43-12)[`4`][ARITH_RULE`~(4 MOD 5=0)/\ SUC A= A+1`;h0] THEN REAL_ARITH_TAC; ASSUME_TAC(ARITH_RULE`1+1=2/\ 1+5-1=5`) THEN MRESAL_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`scs_5M2`;`FF`;`v (1)`;`v`;`1`;`5`][] THEN MRESA_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v 1`] THEN THAYTHE_TAC 0[`v 0`] THEN MP_TAC(REAL_ARITH`azim (vec 0) (v 1) (v 2) (v 0) <= pi ==> azim (vec 0) ((v:num->real^3) 1) (v 2) (v 0) = pi\/ azim (vec 0) (v 1) (v 2) (v 0) < pi`) THEN RESA_TAC; DICH_TAC(34-10) THEN REWRITE_TAC[scs_generic] THEN RESA_TAC THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_5M2`] THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v 2`;`v 0`;`V`] THEN THAYTHEL_ASM_TAC 0[`v 2`;`v 0`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Uxckfpe.ARITH_5_TAC] THEN SUBGOAL_THEN`(!j. ~(j MOD 5 = 0 MOD 5) ==> ~collinear {vec 0, v 0, (v:num->real^3)j})`ASSUME_TAC ; REPEAT RESA_TAC THEN DICH_TAC 0 THEN THAYTHE_TAC 1[`v 0`;`v j`] THEN MATCH_DICH_TAC 0 THEN REWRITE_TAC[SET_RULE`a IN {b,a}`] THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`] ; MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v 1`;`v 2`;`(v:num->real^3) 0`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`] THEN STRIP_TAC THEN MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`scs_5M2`;`5`;`v`;`0`][ARITH_RULE`0+2=2`]THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN STRIP_TAC THEN SUBGOAL_THEN`(!i. scs_diag 5 1 i ==> scs_a_v39 scs_5M2 1 i < dist ((v:num->real^3) 1,v i))`ASSUME_TAC; REPEAT RESA_TAC THEN THAYTHE_TAC(41-2)[`1`;`i'`] THEN MP_TAC h0_LT_B_SCS_5M2 THEN STRIP_TAC THEN THAYTHE_TAC 0[`1`;`i'`] THEN DICH_TAC 0 THEN DICH_TAC 1 THEN REAL_ARITH_TAC; MRESAL_TAC MMS_IMP_BBPRIME[`scs_5M2`;`v`][LET_DEF;LET_END_DEF;BBprime_v39] THEN MRESAL_TAC JKQEWGV2[`scs_5M2`;`v`][LET_DEF;LET_END_DEF;scs_generic] THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH THEN RESA_TAC THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) 1) V E)`ASSUME_TAC ; REPEAT RESA_TAC THEN DICH_TAC 3 THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`v1:real^3` THEN EXISTS_TAC`(v:num->real^3)1` THEN ASM_REWRITE_TAC[] ; MRESAS_TAC NUXCOEAv2[`scs_5M2`;`5`;`v`;`1`;`2`][ARITH_RULE`SUC 1=2/\ SUC 4 MOD 5 = 0 MOD 5`;h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2;J_SCS_5M2_0] THEN DICH_TAC 0 THEN DICH_TAC 0 THEN THAYTHEL_TAC(45-35)[`5`;`0`][ARITH_RULE`5 MOD 5 = 0 MOD 5`] THEN MATCH_MP_TAC(SET_RULE`(A==> (B/\A1==>C)==>D)==> (A==>(B/\ A1/\A==>C)==>D)`) THEN STRIP_TAC THEN SCS_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC[DIST_SYM] THEN DICH_TAC 0 THEN ONCE_REWRITE_TAC[DIST_SYM] THEN THAYTHES_TAC(46-12)[`1`][ARITH_RULE`~(1 MOD 5=0)/\ SUC A= A+1`;h0] THEN REAL_ARITH_TAC; MP_TAC Iunbuig.IUNBUIG THEN RESA_TAC THEN MATCH_DICH_TAC 0 THEN EXISTS_TAC`scs_5M2` THEN EXISTS_TAC`FF:real^3#real^3->bool` THEN ASM_SIMP_TAC[h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2;GSYM ADD1] THEN SCS_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`a<=a`;interior_angle1;GSYM ivs_rho_node1] THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_5M2`] THEN THAYTHEL_TAC 0[`5`;`0`][ARITH_RULE`5 MOD 5 = 0 MOD 5`] THEN THAYTHEL_ASM_TAC (35-13)[`3`][ARITH_RULE`~(3 MOD 5= 0)/\ SUC 3=4`] THEN THAYTHEL_ASM_TAC (0)[`4`][ARITH_RULE`~(4 MOD 5= 0)/\ SUC 4=5`] THEN THAYTHEL_ASM_TAC (0)[`1`][ARITH_RULE`~(1 MOD 5= 0)/\ SUC 1=2`] THEN THAYTHEL_ASM_TAC (0)[`2`][ARITH_RULE`~(2 MOD 5= 0)/\ SUC 2=3`] THEN DICH_TAC (39-10) THEN REWRITE_TAC[scs_generic] THEN RESA_TAC THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_5M2`] THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v 0`;`v 3`;`V`] THEN THAYTHEL_ASM_TAC 0[`v 3`;`v 0`][SET_RULE`a IN {b,a}`;BB_VV_FUN_EQ;Uxckfpe.ARITH_5_TAC] THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v 1`;`v 3`;`V`] THEN THAYTHEL_ASM_TAC 0[`v 1`;`v 3`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Uxckfpe.ARITH_5_TAC] THEN MRESAL_TAC xrr_le_1553_BB[`scs_5M2`;`v`;`3`][ARITH_RULE`3+1=4/\ 3+2=5`] THEN MRESAL_TAC xrr_le_1553_BB[`scs_5M2`;`v`;`1`][ARITH_RULE`1+1=2/\ 1+2=3`;GSYM dist] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN DICH_TAC 1 THEN REWRITE_TAC[xrr;dist] THEN REAL_ARITH_TAC ; SUBGOAL_THEN`!j. dist ((v:num->real^3) j,v (SUC j)) = &2`ASSUME_TAC ; GEN_TAC THEN MP_TAC(SET_RULE`~(j MOD 5 = 0) \/ (j MOD 5 = 0)`) THEN RESA_TAC; MATCH_DICH_TAC (18-13) THEN ASM_REWRITE_TAC[]; MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_5M2`] THEN THAYTHEL_ASM_TAC 0[`j`;`0`][ARITH_RULE`0 MOD 5=0`] THEN THAYTHES_TAC 0[`SUC j`;`SUC 0`][ARITH_RULE`~(5=0)/\ SUC i= 1+i/\ 0 MOD 5=0`;Ocbicby.MOD_EQ_MOD_SHIFT] THEN ASM_REWRITE_TAC[ARITH_RULE`1+0=1`]; MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM) THEN REWRITE_TAC[IN;SET_RULE`~(A={})<=> ?a. a IN A`] THEN STRIP_TAC THEN MATCH_DICH_TAC 0 THEN EXISTS_TAC`v:num->real^3` THEN EXISTS_TAC`scs_5M2` THEN ASM_SIMP_TAC[SCS_M_5M2] THEN STRIP_TAC ; DICH_TAC(18-4) THEN REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(5<=3))`;IN;K_SCS_4M8_prime;K_SCS_4M8;scs_prop_equ_v39;] THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN SCS_TAC THEN REWRITE_TAC[ARITH_RULE`~(5<=3)`]; REPEAT STRIP_TAC ; MP_TAC(SET_RULE`i' MOD 5 = j MOD 5\/ ~(i' MOD 5 = j MOD 5)`) THEN RESA_TAC; THAYTHE_TAC 2[`i'`;`j`] ; MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`] THEN MP_TAC(SET_RULE`SUC i' MOD 5 = j MOD 5\/ ~(SUC i' MOD 5 = j MOD 5)`) THEN RESA_TAC; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j:num`;`v`;` SUC i'`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`;] THEN REAL_ARITH_TAC; MP_TAC(SET_RULE`i' MOD 5 =SUC j MOD 5\/ ~(i' MOD 5 =SUC j MOD 5)`) THEN RESA_TAC; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` SUC j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`;] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; THAYTHEL_TAC (25-2)[`i'`;`j`][scs_diag] THEN DICH_TAC 0 THEN REAL_ARITH_TAC; MP_TAC(SET_RULE`i' MOD 5 = j MOD 5\/ ~(i' MOD 5 = j MOD 5)`) THEN RESA_TAC; THAYTHE_TAC 2[`i'`;`j`] ; MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`] THEN MP_TAC(SET_RULE`SUC i' MOD 5 = j MOD 5\/ ~(SUC i' MOD 5 = j MOD 5)`) THEN RESA_TAC; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j:num`;`v`;` SUC i'`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`;] THEN REAL_ARITH_TAC; MP_TAC(SET_RULE`i' MOD 5 =SUC j MOD 5\/ ~(i' MOD 5 =SUC j MOD 5)`) THEN RESA_TAC; MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` SUC j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`;] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; THAYTHE_TAC (25-20)[`i'`;`j`] THEN DICH_TAC 0 THEN MP_TAC(SET_RULE`psort 5 (i',j) = 0,1\/ ~(psort 5 (i',j) = 0,1)`) THEN RESA_TAC; MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`1`;`j`;`0`;`5`][PSORT_5_EXPLICIT]; DICH_TAC (28-23) THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ARITH_RULE`1= 1+0`] THEN ASM_SIMP_TAC[ARITH_RULE`SUC i= 1+i`;ARITH_RULE`~(5=0)/\ SUC i= 1+i/\ 0 MOD 5=0`;Ocbicby.MOD_EQ_MOD_SHIFT]; DICH_TAC (28-24) THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ARITH_RULE`1= 1+0`] THEN ASM_SIMP_TAC[ARITH_RULE`SUC i= 1+i`;ARITH_RULE`~(5=0)/\ SUC i= 1+i/\ 0 MOD 5=0`;Ocbicby.MOD_EQ_MOD_SHIFT]; REWRITE_TAC[h0] THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; ]);; let HIJ_STEP_1=prove_by_refinement(`main_nonlinear_terminal_v11 ==> (scs_arrow_v39 {scs_5M2 } ({ scs_5T1} UNION { scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j } UNION { scs_stab_diag_v39 scs_5I3 i j| scs_diag 5 i j } UNION { scs_stab_diag_v39 scs_5M3 i j| scs_diag 5 i j }))`, [ REPEAT GEN_TAC THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION] THEN ABBREV_TAC`k=scs_k_v39 s` THEN REPEAT RESA_TAC; REWRITE_TAC[SCS_5T1_IS_SCS]; ASM_SIMP_TAC[ STAB_5I2_SCS;K_SCS_5I2] ; ASM_SIMP_TAC[ STAB_5I3_SCS;K_SCS_5I3] ; ASM_SIMP_TAC[ STAB_5M3_SCS;K_SCS_5M3] ; DISJ_CASES_TAC(SET_RULE`(!s. s = scs_5M2 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_5M2 ==> 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 5 i j ==> cstab < dist(v i,v j))\/ ~((!i j. scs_diag 5 i j ==> cstab < dist((v:num->real^3) i,v j)))`) THEN RESA_TAC; EXISTS_TAC`scs_5T1` THEN ASM_REWRITE_TAC[] THEN MP_TAC SCS_5M2_IMP_SCS_5T1 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN] THEN RESA_TAC THEN MATCH_DICH_TAC 0 THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`v:num->real^3` THEN ASM_REWRITE_TAC[] ; POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a b<=a`] THEN STRIP_TAC ; MP_TAC(SET_RULE` (!i. dist(v i, v(i+1))<= &2 * h0) \/ ~ (!l. dist((v:num->real^3) l, v(l+1))<= &2 * h0) `) THEN RESA_TAC; EXISTS_TAC`scs_stab_diag_v39 scs_5I2 i j` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC; MATCH_MP_TAC(SET_RULE`A==> B\/A\/C\/D`) THEN EXISTS_TAC`i:num` THEN EXISTS_TAC`j:num` THEN ASM_REWRITE_TAC[] ; MP_TAC MM_5M2_IMP_MM_STAB_5I2 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN] THEN RESA_TAC THEN MATCH_DICH_TAC 0 THEN ASM_REWRITE_TAC[] ; POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<=b)<=> breal^3) l, v(l+1))<= sqrt8\/ sqrt8<= dist(v l, v(l+1))`) THEN RESA_TAC; EXISTS_TAC`scs_stab_diag_v39 scs_5I3 i j` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC; MATCH_MP_TAC(SET_RULE`A==> B\/C\/A\/D`) THEN EXISTS_TAC`i:num` THEN EXISTS_TAC`j:num` THEN ASM_REWRITE_TAC[] ; MP_TAC MM_5M2_IMP_MM_STAB_5I3 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN] THEN RESA_TAC THEN MATCH_DICH_TAC 0 THEN ASM_REWRITE_TAC[] ; EXISTS_TAC`scs_stab_diag_v39 scs_5M3 i j` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC; MATCH_MP_TAC(SET_RULE`A==> B\/C\/D\/A`) THEN EXISTS_TAC`i:num` THEN EXISTS_TAC`j:num` THEN ASM_REWRITE_TAC[] ; MP_TAC MM_5M2_IMP_MM_STAB_5M3 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN] THEN RESA_TAC THEN MATCH_DICH_TAC 0 THEN ASM_REWRITE_TAC[] ; ]);; let HIJQAHA=prove_by_refinement(`main_nonlinear_terminal_v11 ==> (scs_arrow_v39 {scs_5M2 } ({ scs_5T1, scs_stab_diag_v39 scs_5I2 0 2, scs_stab_diag_v39 scs_5M1 0 2, scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4,scs_4M6',scs_4M7,scs_4M8,scs_3T1,scs_3T4 }))`, [ STRIP_TAC THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`({ scs_5T1} UNION { scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j } UNION { scs_stab_diag_v39 scs_5I3 i j| scs_diag 5 i j } UNION { scs_stab_diag_v39 scs_5M3 i j| scs_diag 5 i j })` THEN ASM_SIMP_TAC[HIJ_STEP_1;SET_RULE`{scs_5T1, scs_stab_diag_v39 scs_5I2 0 2, scs_stab_diag_v39 scs_5M1 0 2, scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4, scs_4M6', scs_4M7, scs_4M8, scs_3T1, scs_3T4} ={scs_5T1}UNION{ scs_stab_diag_v39 scs_5I2 0 2}UNION{ scs_stab_diag_v39 scs_5M1 0 2, scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4}UNION{ scs_4M6', scs_4M7, scs_4M8, scs_3T1, scs_3T4}`] 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_REWRITE_TAC[SCS_5T1_IS_SCS]; MATCH_MP_TAC FZIOTEF_UNION THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_5I2]; MATCH_MP_TAC FZIOTEF_UNION THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_5M3_IMP_SCS_3_4] THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{scs_stab_diag_v39 scs_5M1 i j | scs_diag 5 i j}` THEN ASM_REWRITE_TAC[Otmtotj.STAB_5I3_ARROW_STAB_5M1_DIAG;Otmtotj.SET_EQ_DIAG_STAB_5M1]]);; end;; (* let check_completeness_claimA_concl = Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) *)