(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Chapter: Local Fan *)
(* Author: Hoang Le Truong *)
(* Date: 2012-04-01 *)
(* ========================================================================= *)
(*
remaining conclusions from appendix to Local Fan chapter
*)
module Miqmcsn = struct
open Polyhedron;;
open Sphere;;
open Topology;;
open Fan_misc;;
open Planarity;;
open Conforming;;
open Hypermap;;
open Fan;;
open Topology;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Collect_geom;;
open Dih2k_hypermap;;
open Wjscpro;;
open Tecoxbm;;
open Hdplygy;;
open Nkezbfc_local;;
open Flyspeck_constants;;
open Gbycpxs;;
open Pcrttid;;
open Local_lemmas1;;
open Pack_defs;;
open Hales_tactic;;
open Appendix;;
open Hypermap;;
open Fan;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Flyspeck_constants;;
open Pack_defs;;
open Hales_tactic;;
open Appendix;;
open Zithlqn;;
open Xwitccn;;
open Ayqjtmd;;
open Jkqewgv;;
open Mtuwlun;;
open Uxckfpe;;
open Sgtrnaf;;
open Yxionxl;;
open Qknvmlb;;
open Odxlstcv2;;
open Yxionxl2;;
open Eyypqdw;;
open Ocbicby;;
open Imjxphr;;
open Nuxcoea;;
open Aursipd;;
open Cuxvzoz;;
open Rrcwnsj;;
open Tfitskc;;
open Hexagons;;
open Otmtotj;;
open Hijqaha;;
open Cnicgsf;;
open Ardbzye;;
open Aueaheh;;
open Vasyyau;;
(**************************************************)
let scs_3T4_prime2 = (* terminal_tri_6833979866 = *) new_definition
`scs_3T4_prime2 = mk_unadorned_v39 3
(#0.2759)
(funlist_v39 [(0,1),(&2);(0,2),cstab] (&2*h0) 3)
(funlist_v39 [(0,1),(&2 * h0)] (cstab) 3)`;;
let scs_3T3_prime = (* terminal_tri_6833979866 = *) new_definition
`scs_3T3_prime = mk_unadorned_v39 3
(#0.476)
(funlist_v39 [(0,1),cstab] (&2*h0) 3)
(funlist_v39 [] (cstab) 3)`;;
let scs_3M1_prime = new_definition
`scs_3M1_prime = mk_unadorned_v39 3 (#0.103)
(funlist_v39 [(0,1),(cstab)] (&2) 3)
(funlist_v39 [(0,1),(cstab)] (&2 * h0) 3)`;;
let scs_4M8_02 = new_definition
`scs_4M8_02 = mk_unadorned_v39 4 (#0.513)
(funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(cstab);(1,3),(cstab)] (&2) 4)
(funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(#3.62);(1,3),(&6)] (&2) 4)`;;
let scs_4M8_13 = new_definition
`scs_4M8_13 = mk_unadorned_v39 4 (#0.513)
(funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(cstab);(1,3),(cstab)] (&2) 4)
(funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(&6);(1,3),(#3.62)] (&2) 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)/\
psort 4 (0,0)= (0,0)/\
psort 4 (1,1)= (1,1)/\
psort 4 (2,2)= (2,2)/\
psort 4 (3,3)= (3,3)/\
psort 4 (4,3)= (0,3)/\
psort 4 (4,4)= (0,0)/\
psort 4 (0,2)= (0,2)/\
psort 4 (4,5)= (0,1)/\
psort 4 (5,4)= (0,1)/\
psort 4 (5,5)= (1,1)/\
psort 4 (1,4)= (0,1)/\
psort 4 (2,5)= (1,2)/\
psort 4 (3,6)= (2,3)
`,
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/\ 6 MOD 4=2`]);;
let SCS_TAC= ASM_SIMP_TAC[scs_basic;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} j <=> {} i`;periodic2;scs_basic;unadorned_v39;scs_prop_equ_v39;LET_DEF;LET_END_DEF;scs_stab_diag_v39;scs_half_slice_v39;
Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_5_TAC;
scs_5M1;scs_3M1;scs_6I1;scs_3T1;scs_4M2;scs_6M1;scs_6T1;scs_5I1;scs_5I2;scs_5I3;scs_5M2;scs_4M6;scs_3T4;scs_5M3;scs_3T4_prime;scs_4M6_prime;scs_4M7_prime;scs_4M7;scs_3T1_prime;scs_4M8;scs_4M8_prime;scs_5T1;scs_3T5;scs_4M3;scs_3T6;scs_4M4;scs_4M5;scs_4I2;scs_4T1;scs_4T2;scs_4I1;scs_4T4;scs_4I3;scs_3T3;scs_4T5;scs_3T4_prime2;scs_3T3_prime;scs_3M1_prime;scs_4T3;scs_4M8_02;scs_4M8_13;scs_3T7;
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/\ 6 MOD 4=2`];;
(********************)
let SCS_4T3_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4T3`,
[SIMP_TAC[scs_4T3;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 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;
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 ) \/
&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_SIMP_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
THEN REPEAT RESA_TAC;
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];
SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN 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;
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) \/
&2 <
(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))} ={0,2}`ASSUME_TAC
;
REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`;SET_RULE`a IN {b,c}<=>a=b\/ a=c`]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
THEN REPEAT RESA_TAC;
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];
SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN 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;
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) \/
&2 <
(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))} ={0,2}`ASSUME_TAC
;
REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`;SET_RULE`a IN {b,c}<=>a=b\/ a=c`]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
THEN REPEAT RESA_TAC;
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];
SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;
SCS_TAC;
SCS_TAC
THEN ASM_SIMP_TAC[MOD_LT;h0;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; (0,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_3T3_prime_IS_SCS=prove_by_refinement( `is_scs_v39 scs_3T3_prime`,
[SIMP_TAC[scs_3T3_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.476 < #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 [] cstab 3 i (SUC i) \/
&2 < funlist_v39 [(0,1),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_3M1_prime_IS_SCS=prove_by_refinement( `is_scs_v39 scs_3M1_prime`,
[SIMP_TAC[scs_3M1_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.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 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_3T7_IS_SCS=prove_by_refinement( `is_scs_v39 scs_3T7`,
[SIMP_TAC[scs_3T7;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.2565 < #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;
DICH_TAC 0
THEN ARITH_TAC;
MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
(&2 * h0 <
funlist_v39 [(0,1),#3.62; (0,2),cstab; (1,2),&2] (&2) 3 i (SUC i) \/
&2 < funlist_v39 [(0,1),cstab; (0,2),cstab; (1,2),&2] (&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_prime2_BASIC=prove(`scs_basic_v39 scs_3T4_prime2`,
SCS_TAC);;
let K_SCS_3T4_prime2=prove(`scs_k_v39 scs_3T4_prime2=3`,
SCS_TAC);;
let J_SCS_3T4_prime2=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T4_prime2 i) i1 j= F`,
SCS_TAC );;
let J_SCS_3T4_prime2_1=prove(`scs_J_v39 (scs_3T4_prime2 ) i1 j= F`,
SCS_TAC );;
let SCS_3T7_BASIC=prove(`scs_basic_v39 scs_3T7`,
SCS_TAC);;
let K_SCS_3T7=prove(`scs_k_v39 scs_3T7=3`,
SCS_TAC);;
let J_SCS_3T7=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T7 i) i1 j= F`,
SCS_TAC );;
let J_SCS_3T7_1=prove(`scs_J_v39 (scs_3T7 ) i1 j= F`,
SCS_TAC );;
let SCS_3T3_prime_BASIC=prove(`scs_basic_v39 scs_3T3_prime`,
SCS_TAC);;
let K_SCS_3T3_prime=prove(`scs_k_v39 scs_3T3_prime=3`,
SCS_TAC);;
let J_SCS_3T3_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T3_prime i) i1 j= F`,
SCS_TAC );;
let SCS_3M1_prime_BASIC=prove(`scs_basic_v39 scs_3M1_prime`,
SCS_TAC);;
let K_SCS_3M1_prime=prove(`scs_k_v39 scs_3M1_prime=3`,
SCS_TAC);;
let J_SCS_3M1_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3M1_prime i) i1 j= F`,
SCS_TAC );;
let SCS_4T3_BASIC=prove(`scs_basic_v39 scs_4T3`,
SCS_TAC);;
let K_SCS_4T3=prove(`scs_k_v39 scs_4T3=4`,
SCS_TAC);;
let J_SCS_4T3=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4T3 i) i1 j= F`,
SCS_TAC );;
let SCS_4M8_02_BASIC=prove(`scs_basic_v39 scs_4M8_02`,
SCS_TAC);;
let K_SCS_4M8_02=prove(`scs_k_v39 scs_4M8_02=4`,
SCS_TAC);;
let J_SCS_4M8_02=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M8_02 i) i1 j= F`,
SCS_TAC );;
let SCS_4M8_13_BASIC=prove(`scs_basic_v39 scs_4M8_13`,
SCS_TAC);;
let K_SCS_4M8_13=prove(`scs_k_v39 scs_4M8_13=4`,
SCS_TAC);;
let J_SCS_4M8_13=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M8_13 i) i1 j= F`,
SCS_TAC );;
(***********************)
let BB_3T4_prime2_IMP_scs_3T4=prove(`BBs_v39 scs_3T4_prime2 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_prime2;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_prime2_IMP_MM_3T4=prove(`MMs_v39 scs_3T4_prime2 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_prime2`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_3T4_prime2`;`v`]
THEN ASM_SIMP_TAC[SCS_3T4_BASIC;SCS_3T4_prime2_BASIC;SCS_3T4_IS_SCS;SCS_3T4_IS_SCS;
SCS_3T4_prime2_IS_SCS;K_SCS_3T4;K_SCS_3T4_prime2;IN;BB_3T4_prime2_IMP_scs_3T4]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;
let SCS_3T4_prime2_ARROW_MM_3T4=prove_by_refinement(`scs_arrow_v39 {scs_3T4_prime2 } { 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_prime2 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_3T4_prime2 ==> 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_prime2_IMP_MM_3T4)
THEN POP_ASSUM MP_TAC
THEN SET_TAC[]]);;
(************************************)
let BB_3T3_prime_IMP_scs_3T3=prove(`BBs_v39 scs_3T3_prime v
==>
BBs_v39 (scs_3T3 ) 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_3T3_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_3T3_prime_IMP_MM_3T3=prove(`MMs_v39 scs_3T3_prime v ==> ~(MMs_v39 scs_3T3={})`,
STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_3T3_prime`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_3T3_prime`;`v`]
THEN ASM_SIMP_TAC[SCS_3T3_BASIC;SCS_3T3_prime_BASIC;SCS_3T3_IS_SCS;SCS_3T3_IS_SCS;
SCS_3T3_prime_IS_SCS;K_SCS_3T3;K_SCS_3T3_prime;IN;BB_3T3_prime_IMP_scs_3T3]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;
let SCS_3T3_prime_ARROW_MM_3T3=prove_by_refinement(`scs_arrow_v39 {scs_3T3_prime } { scs_3T3}`,
[ 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_3T3_IS_SCS];
DISJ_CASES_TAC(SET_RULE`(!s. s = scs_3T3_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_3T3_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_3T3`
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC (GEN_ALL MM_3T3_prime_IMP_MM_3T3)
THEN POP_ASSUM MP_TAC
THEN SET_TAC[]]);;
(************************)
let BB_3M1_prime_IMP_scs_3M1=prove(`BBs_v39 scs_3M1_prime v
==>
BBs_v39 (scs_3M1 ) 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_3M1_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_3M1_prime_IMP_MM_3M1=prove(`MMs_v39 scs_3M1_prime v ==> ~(MMs_v39 scs_3M1={})`,
STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_3M1_prime`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_3M1_prime`;`v`]
THEN ASM_SIMP_TAC[SCS_3M1_BASIC;SCS_3M1_prime_BASIC;SCS_3M1_IS_SCS;SCS_3M1_IS_SCS;
SCS_3M1_prime_IS_SCS;K_SCS_3M1;K_SCS_3M1_prime;IN;BB_3M1_prime_IMP_scs_3M1]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;
let SCS_3M1_prime_ARROW_MM_3M1=prove_by_refinement(`scs_arrow_v39 {scs_3M1_prime } { scs_3M1}`,
[ 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_3M1_IS_SCS];
DISJ_CASES_TAC(SET_RULE`(!s. s = scs_3M1_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_3M1_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_3M1`
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC (GEN_ALL MM_3M1_prime_IMP_MM_3M1)
THEN POP_ASSUM MP_TAC
THEN SET_TAC[]]);;
(*************************)
let BB_4M7_IMP_BB_STAN_4M7= prove(`
BBs_v39 scs_4M7 v /\
scs_diag 4 i j /\
dist(v i,v j)<= cstab ==>
BBs_v39 (scs_stab_diag_v39 scs_4M7 i j) v`,
SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M7;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M7;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7]
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
THEN SCS_TAC
THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
THEN RESA_TAC
THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
THENL[
MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M7;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M7;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7;SCS_4M7_IS_SCS]
THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M7;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M7;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7;SCS_4M7_IS_SCS]
THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]]);;
let MM_4M7_IMP_STAB_4M7=prove(`
MMs_v39 scs_4M7 v /\
scs_diag 4 i j /\
dist(v i,v j)<= cstab ==>
~(MMs_v39 (scs_stab_diag_v39 scs_4M7 i j) ={})`,
STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC` scs_4M7 `
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M7 `;`v`]
THEN ASSUME_TAC SCS_4M7_BASIC
THEN ASSUME_TAC K_SCS_4M7
THEN ASM_SIMP_TAC[SCS_4M7_IS_SCS;SCS_4M7_IS_SCS;SCS_4M7_BASIC;K_SCS_4M7;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M7_13;BB_4M7_IMP_BB_STAN_4M7;STAB_4M7_SCS]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;
let SET_STAB_4M7=prove(`{ scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M7 (i MOD 4) (j MOD 4)| scs_diag 4 (i MOD 4) (j MOD 4) }`,
ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
THEN MRESAL_TAC STAB_MOD[`scs_4M7`][SCS_4M7_IS_SCS;K_SCS_4M7]);;
let EXPAND_STAB_DIAG_4M7=prove(`
{scs_stab_diag_v39 scs_4M7 (i MOD 4) (j MOD 4) | j MOD 4 =
(i MOD 4 + 2) MOD 4}=
{scs_stab_diag_v39 scs_4M7 (i+2) i| i<4} `,
ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M7_IS_SCS;K_SCS_4M7]);;
let SET_EQ_DIAG_STAB_4M7=prove_by_refinement(`scs_arrow_v39
{ scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4M7 0 2,scs_stab_diag_v39 scs_4M7 1 3}`,
[
ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M7;SET_STAB_4M7;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
THEN
REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M7 (i + 2) i |i=0\/i=1\/i=2\/i=3}
= {scs_stab_diag_v39 scs_4M7 (0 + 2) 0} UNION
{scs_stab_diag_v39 scs_4M7 (1 + 2) 1} UNION
{scs_stab_diag_v39 scs_4M7 (2 + 2) 2} UNION
{scs_stab_diag_v39 scs_4M7 (3 + 2) 3}
`;]
THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M7 0 2,scs_stab_diag_v39 scs_4M7 1 3}={scs_stab_diag_v39 scs_4M7 0 2} UNION {scs_stab_diag_v39 scs_4M7 1 3}UNION {scs_stab_diag_v39 scs_4M7 0 2} UNION {scs_stab_diag_v39 scs_4M7 1 3}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
THEN MRESA_TAC STAB_SYM[`scs_4M7`;`0`;`2`]
THEN STRIP_TAC;
MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[STAB_4M7_SCS;SCS_DIAG_SCS_4M7_02];
MATCH_MP_TAC FZIOTEF_UNION
THEN MRESA_TAC STAB_SYM[`scs_4M7`;`1`;`3`]
THEN STRIP_TAC;
MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[STAB_4M7_SCS;SCS_DIAG_SCS_4M7_13];
MATCH_MP_TAC FZIOTEF_UNION
THEN MRESAL_TAC STAB_MOD[`scs_4M7`;`4`;`2`][SCS_4M7_IS_SCS;K_SCS_4M7;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
THEN SYM_ASSUM_TAC
THEN STRIP_TAC;
MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[STAB_4M7_SCS;SCS_DIAG_SCS_4M7_02];
MRESAL_TAC STAB_MOD[`scs_4M7`;`5`;`3`][SCS_4M7_IS_SCS;K_SCS_4M7;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
THEN SYM_ASSUM_TAC;
MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[STAB_4M7_SCS;SCS_DIAG_SCS_4M7_13]]);;
let SCS_4M7_SLICE_13=prove_by_refinement(
`scs_arrow_v39 {scs_stab_diag_v39 scs_4M7 1 3 } {scs_prop_equ_v39 scs_3T4_prime 2, scs_3T4_prime2 }`,
[
MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M7_13;STAB_4M7_SCS;SCS_K_D_A_STAB_EQ;]
THEN EXISTS_TAC`1`
THEN EXISTS_TAC`3`
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M7_13]
THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
THEN REPEAT RESA_TAC;
REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC scs_inj
THEN ASM_SIMP_TAC[SCS_3T4_prime_BASIC;SCS_4M7_BASIC;J_SCS_4M7;BASIC_HALF_SLICE_STAB;J_SCS_3T4_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T4_prime2_BASIC;J_SCS_3T4_prime2]
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_4M7]
THEN ARITH_TAC;
STRIP_TAC
THEN
ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;
ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7]
THEN ARITH_TAC;
STRIP_TAC
THEN
ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;
ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN REWRITE_TAC[J_SCS_3T4_prime];
]);;
let SCS_4M7_SLICE_13_ARROW_3T4=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M7 1 3 } { scs_3T4}`,
MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3T4_prime 2, scs_3T4_prime2 }`
THEN ASM_REWRITE_TAC[SCS_4M7_SLICE_13]
THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}/\ {scs_3T4}= {scs_3T4}UNION {scs_3T4}`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}/\ {scs_3T4}= {scs_3T4}UNION {scs_3T4}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_REWRITE_TAC[SCS_3T4_prime2_ARROW_MM_3T4;SCS_3T4_prime_ARROW_MM_3T4]
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_3T4_prime}`
THEN ASM_REWRITE_TAC[SCS_3T4_prime2_ARROW_MM_3T4;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[]);;
let SCS_4M7_SLICE_02=prove_by_refinement(
`scs_arrow_v39 {scs_stab_diag_v39 scs_4M7 0 2 } {scs_prop_equ_v39 scs_3T3_prime 1, scs_prop_equ_v39 scs_3M1_prime 1 }`,
[
MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M7_02;STAB_4M7_SCS;SCS_K_D_A_STAB_EQ;]
THEN EXISTS_TAC`0`
THEN EXISTS_TAC`2`
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M7_02]
THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
THEN REPEAT RESA_TAC;
REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC scs_inj
THEN ASM_SIMP_TAC[SCS_3T3_prime_BASIC;SCS_4M7_BASIC;J_SCS_4M7;BASIC_HALF_SLICE_STAB;J_SCS_3T3_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3M1_prime_BASIC;J_SCS_3M1_prime]
THEN STRIP_TAC;
ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T3_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7]
THEN ARITH_TAC;
STRIP_TAC
THEN
ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;
ARITH_RULE`(2 + 1 + 4 - 0) MOD 4= 3/\ 0 MOD 4=0/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7]
THEN ARITH_TAC;
STRIP_TAC
THEN
ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;
ARITH_RULE`(0 + 1 + 4 - 2) MOD 4= 3/\ 2 MOD 4=2/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN REWRITE_TAC[J_SCS_3T3_prime];
]);;
let SCS_4M7_SLICE_02_ARROW_3T3_3M1=prove(
`scs_arrow_v39 {scs_stab_diag_v39 scs_4M7 0 2 } { scs_3T3,scs_3M1}`,
MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3T3_prime 1, scs_prop_equ_v39 scs_3M1_prime 1}`
THEN ASM_REWRITE_TAC[SCS_4M7_SLICE_02]
THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC
THENL[
MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_3T3_prime}`
THEN ASM_REWRITE_TAC[SCS_3T3_prime_ARROW_MM_3T3]
THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T3_prime`;`1`;`3`][SCS_3T3_prime_IS_SCS;K_SCS_3T3_prime;ARITH_RULE`(3 - 1 MOD 3)=2`]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T3_prime 1`;`2`][PROP_EQU_IS_SCS;SCS_3T3_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_3M1_prime}`
THEN ASM_REWRITE_TAC[SCS_3M1_prime_ARROW_MM_3M1]
THEN MRESAS_TAC PRO_EQU_ID1[`scs_3M1_prime`;`1`;`3`][SCS_3M1_prime_IS_SCS;K_SCS_3M1_prime;ARITH_RULE`(3 - 1 MOD 3)=2`]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1_prime 1`;`2`][PROP_EQU_IS_SCS;SCS_3M1_prime_IS_SCS]
THEN DICH_TAC 0
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN REWRITE_TAC[]]);;
let STAB_SCS_4M7_ARROW_3T3_3M1_3T4=prove(
`scs_arrow_v39
{ scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j } {scs_3T3,scs_3M1,scs_3T4}`,
MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M7 0 2,scs_stab_diag_v39 scs_4M7 1 3}`
THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_4M7;SET_RULE`{A,B}={A}UNION {B}`;SET_RULE`{scs_3T3,scs_3M1,scs_3T4}={scs_3T3,scs_3M1} UNION{scs_3T4}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_REWRITE_TAC[SCS_4M7_SLICE_13_ARROW_3T4;SET_RULE`{A}UNION{B}={A,B}`;SCS_4M7_SLICE_02_ARROW_3T3_3M1]);;
(***************************)
let BB_4M8_IMP_BB_STAN_4M8= prove(`
BBs_v39 scs_4M8 v /\
scs_diag 4 i j /\
dist(v i,v j)<= cstab ==>
BBs_v39 (scs_stab_diag_v39 scs_4M8 i j) v`,
SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8]
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
THEN SCS_TAC
THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
THEN RESA_TAC
THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
THENL[
MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8;SCS_4M8_IS_SCS]
THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8;SCS_4M8_IS_SCS]
THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]]);;
let MM_4M8_IMP_STAB_4M8=prove(`
MMs_v39 scs_4M8 v /\
scs_diag 4 i j /\
dist(v i,v j)<= cstab ==>
~(MMs_v39 (scs_stab_diag_v39 scs_4M8 i j) ={})`,
STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC` scs_4M8 `
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8 `;`v`]
THEN ASSUME_TAC SCS_4M8_BASIC
THEN ASSUME_TAC K_SCS_4M8
THEN ASM_SIMP_TAC[SCS_4M8_IS_SCS;SCS_4M8_IS_SCS;SCS_4M8_BASIC;K_SCS_4M8;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M8_13;BB_4M8_IMP_BB_STAN_4M8;STAB_4M8_SCS]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;
let SET_STAB_4M8=prove(`{ scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M8 (i MOD 4) (j MOD 4)| scs_diag 4 (i MOD 4) (j MOD 4) }`,
ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
THEN MRESAL_TAC STAB_MOD[`scs_4M8`][SCS_4M8_IS_SCS;K_SCS_4M8]);;
let EXPAND_STAB_DIAG_4M8=prove(`
{scs_stab_diag_v39 scs_4M8 (i MOD 4) (j MOD 4) | j MOD 4 =
(i MOD 4 + 2) MOD 4}=
{scs_stab_diag_v39 scs_4M8 (i+2) i| i<4} `,
ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M8_IS_SCS;K_SCS_4M8]);;
let SET_EQ_DIAG_STAB_4M8=prove_by_refinement(`scs_arrow_v39
{ scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4M8 0 2,scs_stab_diag_v39 scs_4M8 1 3}`,
[
ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M8;SET_STAB_4M8;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
THEN
REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M8 (i + 2) i |i=0\/i=1\/i=2\/i=3}
= {scs_stab_diag_v39 scs_4M8 (0 + 2) 0} UNION
{scs_stab_diag_v39 scs_4M8 (1 + 2) 1} UNION
{scs_stab_diag_v39 scs_4M8 (2 + 2) 2} UNION
{scs_stab_diag_v39 scs_4M8 (3 + 2) 3}
`;]
THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M8 0 2,scs_stab_diag_v39 scs_4M8 1 3}={scs_stab_diag_v39 scs_4M8 0 2} UNION {scs_stab_diag_v39 scs_4M8 1 3}UNION {scs_stab_diag_v39 scs_4M8 0 2} UNION {scs_stab_diag_v39 scs_4M8 1 3}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
THEN MRESA_TAC STAB_SYM[`scs_4M8`;`0`;`2`]
THEN STRIP_TAC;
MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02];
MATCH_MP_TAC FZIOTEF_UNION
THEN MRESA_TAC STAB_SYM[`scs_4M8`;`1`;`3`]
THEN STRIP_TAC;
MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[STAB_4M8_SCS;SCS_DIAG_SCS_4M8_13];
MATCH_MP_TAC FZIOTEF_UNION
THEN MRESAL_TAC STAB_MOD[`scs_4M8`;`4`;`2`][SCS_4M8_IS_SCS;K_SCS_4M8;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
THEN SYM_ASSUM_TAC
THEN STRIP_TAC;
MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02];
MRESAL_TAC STAB_MOD[`scs_4M8`;`5`;`3`][SCS_4M8_IS_SCS;K_SCS_4M8;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
THEN SYM_ASSUM_TAC;
MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[STAB_4M8_SCS;SCS_DIAG_SCS_4M8_13]]);;
let PROP_OPP_DIAG_4M8_13= prove_by_refinement(`scs_stab_diag_v39 scs_4M8 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4M8 0 2)) 2 `,
[REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;SCS_K_D_A_STAB_EQ;scs_opp_v39]
THEN MATCH_MP_TAC scs_inj
THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M8_BASIC;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_13;scs_basic;unadorned_v39;peropp;peropp2]
THEN SCS_TAC
THEN STRIP_TAC;
SET_TAC[];
STRIP_TAC
THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;]
THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
THEN REPEAT GEN_TAC
THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
THEN SYM_ASSUM_TAC
THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
THEN SYM_ASSUM_TAC
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/ x' MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_4_TAC;PSORT_5_EXPLICIT;ARITH_RULE`4-1=3/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6
/\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;
let STAB_4M8_02_ARROW_4M8_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M8 0 2}{scs_stab_diag_v39 scs_4M8 1 3}`,
ASM_SIMP_TAC[PROP_OPP_DIAG_4M8_13]
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4M8 0 2)}`
THEN STRIP_TAC
THENL[
MATCH_MP_TAC (GEN_ALL YXIONXL2)
THEN EXISTS_TAC`4`
THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M8;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02]
;
MATCH_MP_TAC(GEN_ALL YXIONXL3)
THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4M8 0 2)`
THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M8;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02]]);;
let SCS_4M8_SLICE_13=prove_by_refinement(
`scs_arrow_v39 {scs_stab_diag_v39 scs_4M8 1 3 } {scs_3T4_prime2 }`,
[
ONCE_REWRITE_TAC[SET_RULE`{scs_3T4_prime2}={scs_3T4_prime2, scs_3T4_prime2}`]
THEN MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_13;STAB_4M8_SCS;SCS_K_D_A_STAB_EQ;]
THEN EXISTS_TAC`1`
THEN EXISTS_TAC`3`
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_13]
THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
THEN REPEAT RESA_TAC;
REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC scs_inj
THEN ASM_SIMP_TAC[SCS_3T4_prime_BASIC;SCS_4M8_BASIC;J_SCS_4M8;BASIC_HALF_SLICE_STAB;J_SCS_3T4_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T4_prime2_BASIC;J_SCS_3T4_prime2_1]
THEN STRIP_TAC;
ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8]
THEN ARITH_TAC;
STRIP_TAC
THEN
ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8;
ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8]
THEN ARITH_TAC;
STRIP_TAC
THEN
ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8;
ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN REWRITE_TAC[J_SCS_3T4_prime2_1];
]);;
let SCS_4M8_SLICE_13_ARROW_3T4=prove(
`scs_arrow_v39 {scs_stab_diag_v39 scs_4M8 1 3 } { scs_3T4}`,
MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{ scs_3T4_prime2 }`
THEN ASM_REWRITE_TAC[SCS_4M8_SLICE_13]
THEN ASM_REWRITE_TAC[SCS_3T4_prime2_ARROW_MM_3T4;SCS_3T4_prime_ARROW_MM_3T4]);;
let SCS_4M8_SLICE_02_ARROW_3T4 =prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_4M8 0 2 } { scs_3T4 }`,
MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M8 1 3}`
THEN ASM_SIMP_TAC[STAB_4M8_02_ARROW_4M8_13;SCS_4M8_SLICE_13_ARROW_3T4]);;
let SET_STAB_4M8_ARROW_3T4=prove(`scs_arrow_v39
{ scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j } {scs_3T4}`,
ONCE_REWRITE_TAC[SET_RULE`{A}={A,A}`]
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M8 0 2,scs_stab_diag_v39 scs_4M8 1 3}`
THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M8;]
THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`;]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[SCS_4M8_SLICE_02_ARROW_3T4;SCS_4M8_SLICE_13_ARROW_3T4]);;
(*****************)
let h0_LT_B_SCS_4M6=prove(`
(!i j. scs_diag 4 i j ==> &4 * h0 < scs_b_v39 scs_4M6' i j)
/\ (!i j. scs_diag 4 i j ==> scs_a_v39 scs_4M6' i j <= cstab)`,
SCS_TAC
THEN REWRITE_TAC[h0;SCS_DIAG_4_CASES;cstab]
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)`)
THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC
THEN MP_TAC sqrt8_LE_CSTAB
THEN REAL_ARITH_TAC);;
let SCS_4M6_STAND_OR_PRO=prove(`!i. scs_a_v39 scs_4M6' i (i + 1) = &2 /\
scs_b_v39 scs_4M6' i (i + 1) = &2 * h0 \/
scs_a_v39 scs_4M6' i (i + 1) = &2 * h0 /\
scs_b_v39 scs_4M6' i (i + 1) = cstab`,
GEN_TAC
THEN SCS_TAC
THEN SIMP_TAC[GSYM ADD1;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`SUC i:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`4`][ARITH_RULE`1<4`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN SCS_TAC);;
let SCS_4M6_STAND=prove(`scs_a_v39 scs_4M6' 1 2 = &2/\ scs_a_v39 scs_4M6' 2 3 = &2/\ scs_a_v39 scs_4M6' 3 4 = &2/\ scs_a_v39 scs_4M6' 0 1= &2 * h0
/\ scs_a_v39 scs_4M6' 1 4= &2 * h0
/\ scs_b_v39 scs_4M6' 0 1= cstab`,
SCS_TAC);;
let h0_CSTAB_LT_4=prove(`&2< &2*h0 /\ cstab< &4/\ &2<= &2*h0 /\ cstab<= &4
/\ &2*h0< &4/\ &2< &4 /\ ~(&2 * h0 = &2)`,
REWRITE_TAC[cstab;h0]
THEN REAL_ARITH_TAC);;
let EXTREMAL_SCS_4M6=prove_by_refinement(`main_nonlinear_terminal_v11 ==>
(!v.
MMs_v39 scs_4M6' v /\
(!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==>
dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = &2/\dist (v 3,v 0) = &2
/\ dist (v 0,v 1) = cstab)`,
[
STRIP_TAC
THEN GEN_TAC
THEN STRIP_TAC
THEN ASSUME_TAC(SCS_4M6_IS_SCS)
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M6'`;`v`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M6'`]
THEN THAYTHES_TAC 0[`4`;`0`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M6]
THEN MP_TAC PWEIWBZ
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`1`][SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;h0_LT_B_SCS_4M6;SCS_4M6_STAND_OR_PRO;ARITH_RULE`1+1=2`;SCS_4M6_STAND]
THEN MP_TAC PWEIWBZ
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`2`][SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;h0_LT_B_SCS_4M6;SCS_4M6_STAND_OR_PRO;ARITH_RULE`2+1=3`;SCS_4M6_STAND]
THEN MP_TAC PWEIWBZ
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`3`][SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;h0_LT_B_SCS_4M6;SCS_4M6_STAND_OR_PRO;ARITH_RULE`3+1=4`;SCS_4M6_STAND]
THEN ASSUME_TAC SCS_4M6_BASIC
THEN ASSUME_TAC K_SCS_4M6
THEN ASSUME_TAC h0_LT_B_SCS_4M6
THEN ASSUME_TAC SCS_4M6_STAND_OR_PRO
THEN ASSUME_TAC SCS_4M6_STAND
THEN ASSUME_TAC h0_CSTAB_LT_4
THEN MP_TAC (SET_RULE`scs_is_str scs_4M6' v 0\/ ~(scs_is_str scs_4M6' v 0 )`)
THEN RESA_TAC;
MP_TAC VASYYAU
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`0`][ARITH_RULE`0+1=1`]
THEN MP_TAC Bkossge.quad_nonexist_849
THEN ASM_REWRITE_TAC[NOT_EXISTS_THM]
THEN STRIP_TAC
THEN THAYTHE_TAC 0[`v 1`;`v 2`;`v 3`;`v 0`;]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[DE_MORGAN_THM;REAL_ARITH`~(a<=b)<=> b b b (!v. MMs_v39 scs_4M6' v /\
(!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))
==> BBs_v39 scs_4T3 v)`,
REPEAT STRIP_TAC
THEN MP_TAC EXTREMAL_SCS_4M6
THEN RESA_TAC
THEN THAYTHE_TAC 0[`v`]
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M6'`;`v`]
THEN DICH_TAC 0
THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4T3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4T3]
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
THEN SCS_TAC
THEN THAYTHE_TAC 2[`i`;`j`]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M6'`;`v`]
THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M6'`][SCS_4M6_IS_SCS]
THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M6;MOD_REFL]
THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M6'`][SCS_4M6_IS_SCS]
THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M6;MOD_REFL]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN SCS_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN RESA_TAC);;
(**************)
let MM_4M6_IMP_MM_4T3=prove(`main_nonlinear_terminal_v11
==> (!v. MMs_v39 scs_4M6' v /\
(!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))
==> ~(MMs_v39 scs_4T3={}))`,
STRIP_TAC
THEN GEN_TAC
THEN STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_4M6'`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M6'`;`v`]
THEN ASM_SIMP_TAC[SCS_4T3_BASIC;SCS_4M6_BASIC;SCS_4T3_IS_SCS;SCS_4T3_IS_SCS;
SCS_4M6_IS_SCS;K_SCS_4T3;K_SCS_4M6;IN;BB_4M6_IMP_scs_4T3]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;
let SCS_4M6_ARROW_SCS_4T3_STAB_4M6=prove_by_refinement(
`main_nonlinear_terminal_v11
==> scs_arrow_v39 { scs_4M6' } ({scs_4T3} UNION {scs_stab_diag_v39 scs_4M6' i j| scs_diag 4 i j})`,
[
STRIP_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;
ASM_SIMP_TAC[SCS_4T3_IS_SCS];
ASM_SIMP_TAC[STAB_4M6_SCS;K_SCS_4M6];
DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M6' ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M6' ==> MMs_v39 s = {}))`);
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN STRIP_TAC;
MP_TAC(SET_RULE`(!i j. scs_diag 4 i j ==> cstab < dist(v i,v j))\/ ~((!i j. scs_diag 4 i j ==> cstab < dist((v:num->real^3) i,v j)))`)
THEN RESA_TAC;
EXISTS_TAC`scs_4T3`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC MM_4M6_IMP_MM_4T3
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN RESA_TAC
THEN MATCH_DICH_TAC 0
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`v:num->real^3`
THEN ASM_REWRITE_TAC[];
POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a b<=a`]
THEN STRIP_TAC
THEN MP_TAC MM_4M6_IMP_STAB_4M6
THEN RESA_TAC
THEN DICH_TAC 0
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN STRIP_TAC
THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M6' i j`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;
MATCH_MP_TAC(SET_RULE`A==> B\/A`)
THEN EXISTS_TAC`i:num`
THEN EXISTS_TAC`j:num`
THEN ASM_REWRITE_TAC[];
EXISTS_TAC`v':num->real^3`
THEN ASM_REWRITE_TAC[]]);;
let NWDGKXH=prove(`main_nonlinear_terminal_v11
==> scs_arrow_v39 { scs_4M6' } ({scs_4T3, scs_4T5})`,
STRIP_TAC
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`({scs_4T3} UNION {scs_stab_diag_v39 scs_4M6' i j| scs_diag 4 i j})`
THEN ASM_SIMP_TAC[SCS_4M6_ARROW_SCS_4T3_STAB_4M6]
THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`;]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[SET_STAB_4M6_ARROW_4T5]
THEN MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[SCS_4T3_IS_SCS]);;
(*****************)
let h0_LT_B_SCS_4M7=prove(`
(!i j. scs_diag 4 i j ==> &4 * h0 < scs_b_v39 scs_4M7 i j)
/\ (!i j. scs_diag 4 i j ==> scs_a_v39 scs_4M7 i j <= cstab)`,
SCS_TAC
THEN REWRITE_TAC[h0;SCS_DIAG_4_CASES;cstab]
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)`)
THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC
THEN MP_TAC sqrt8_LE_CSTAB
THEN REAL_ARITH_TAC);;
let SCS_4M7_STAND_OR_PRO=prove(`!i. scs_a_v39 scs_4M7 i (i + 1) = &2 /\
scs_b_v39 scs_4M7 i (i + 1) = &2 * h0 \/
scs_a_v39 scs_4M7 i (i + 1) = &2 * h0 /\
scs_b_v39 scs_4M7 i (i + 1) = cstab`,
GEN_TAC
THEN SCS_TAC
THEN SIMP_TAC[GSYM ADD1;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`SUC i:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`4`][ARITH_RULE`1<4`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN SCS_TAC);;
let SCS_4M7_STAND=prove(
`scs_a_v39 scs_4M7 0 1= &2*h0/\ scs_a_v39 scs_4M7 1 2 = &2 * h0 /\ scs_a_v39 scs_4M7 2 5= &2*h0 /\scs_b_v39 scs_4M7 1 2= cstab /\scs_b_v39 scs_4M7 0 1 = cstab`,
SCS_TAC);;
let MIN_NOT_STAND_4M7=prove_by_refinement(`main_nonlinear_terminal_v11 ==>
(!v.
MMs_v39 scs_4M7 v /\
(!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==>
dist (v 1,v 2) = &2 * h0 \/ dist (v 0,v 1) = &2*h0)`,
[STRIP_TAC
THEN GEN_TAC
THEN STRIP_TAC
THEN ASSUME_TAC(SCS_4M7_IS_SCS)
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M7`;`v`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`]
THEN THAYTHES_TAC 0[`4`;`0`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M7]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`]
THEN THAYTHES_TAC 0[`5`;`1`][ARITH_RULE`5 MOD 4 = 1 MOD 4`;MOD_MULT_ADD;K_SCS_4M7]
THEN ASSUME_TAC h0_LT_B_SCS_4M7
THEN ASSUME_TAC SCS_4M7_STAND_OR_PRO
THEN ASSUME_TAC SCS_4M7_BASIC
THEN ASSUME_TAC K_SCS_4M7
THEN ASSUME_TAC SCS_4M7_STAND
THEN MP_TAC (SET_RULE`scs_is_str scs_4M7 v 0\/ ~(scs_is_str scs_4M7 v 0 )`)
THEN RESA_TAC;
MP_TAC VASYYAU
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`0`][ARITH_RULE`0+1=1`];
MP_TAC (SET_RULE`scs_is_str scs_4M7 v 1\/ ~(scs_is_str scs_4M7 v 1 )`)
THEN RESA_TAC;
MP_TAC VASYYAU
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`1`][ARITH_RULE`1+1=2`];
MP_TAC (SET_RULE`scs_is_str scs_4M7 v 2\/ ~(scs_is_str scs_4M7 v 2 )`)
THEN RESA_TAC;
MP_TAC VASYYAU
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`2`][ARITH_RULE`2+3=5`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[];
MP_TAC TUAPYYU
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`1`][IN;ARITH_RULE`1+1=2`]
THEN MP_TAC TUAPYYU
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`0`][IN;ARITH_RULE`0+1=1`]
THEN MRESAL_TAC STR_MOD_EQ[`4`;`scs_4M7`;`v`;`4`][IN;ARITH_RULE`4 MOD 4=0`]
THEN MP_TAC WKZZEEH
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`1`][ARITH_RULE`1+1=2/\ 1+3=4`]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]]);;
let BB_4M7_IMP_4M6_12=prove(`main_nonlinear_terminal_v11 ==>
(!v.
MMs_v39 scs_4M7 v /\
(!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) /\
dist (v 1,v 2) = &2*h0
==> BBs_v39 scs_4M6' v)`,
REPEAT STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M7`;`v`]
THEN DICH_TAC 0
THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M7;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
THEN SCS_TAC
THEN THAYTHE_TAC 2[`i`;`j`]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M7`;`v`]
THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][SCS_4M7_IS_SCS]
THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M7;MOD_REFL]
THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][SCS_4M7_IS_SCS]
THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M7;MOD_REFL]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN SCS_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[h0]
THEN REAL_ARITH_TAC);;
let MM_4M7_IMP_MM_4M6_12=prove(`main_nonlinear_terminal_v11
==> (!v. MMs_v39 scs_4M7 v /\
(!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
dist (v 1,v 2) = &2 * h0
==> ~(MMs_v39 scs_4M6'={}))`,
STRIP_TAC
THEN GEN_TAC
THEN STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_4M7`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M7`;`v`]
THEN ASM_SIMP_TAC[SCS_4M6_BASIC;SCS_4M7_BASIC;SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;
SCS_4M7_IS_SCS;K_SCS_4M6;K_SCS_4M7;IN;BB_4M7_IMP_4M6_12]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;
let BB_4M7_IMP_4M6_01=prove(
`main_nonlinear_terminal_v11 ==>
(!v.
MMs_v39 scs_4M7 v /\
(!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) /\
dist (v 0,v 1) = &2*h0
==> BBs_v39 (scs_prop_equ_v39(scs_opp_v39 scs_4M6' ) 1) v)`,
REPEAT STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M7`;`v`]
THEN DICH_TAC 0
THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M7;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;scs_prop_equ_v39;scs_opp_v39;peropp2]
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
THEN SCS_TAC
THEN THAYTHE_TAC 2[`i`;`j`]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M7`;`v`]
THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][SCS_4M7_IS_SCS]
THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M7;MOD_REFL]
THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][SCS_4M7_IS_SCS]
THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M7;MOD_REFL]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+i:num`;`1+j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN MRESA_TAC MOD_ADD_MOD[`1`;`i`;`4`]
THEN MRESA_TAC MOD_ADD_MOD[`1`;`j`;`4`]
THEN SYM_ASSUM_TAC
THEN SYM_ASSUM_TAC
THEN ASSUME_TAC(ARITH_RULE`4-1=3/\ 4-0=4/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 3+2=5 /\3+3=6/\ 5 MOD 4=1/\ 6 MOD 4=2`)
THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN SCS_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[h0;REAL_ARITH`a<=a`]
THEN REAL_ARITH_TAC);;
let MM_4M7_IMP_MM_4M6_01=prove_by_refinement(`main_nonlinear_terminal_v11
==> (!v. MMs_v39 scs_4M7 v /\
(!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
dist (v 0,v 1) = &2 * h0
==> ~(MMs_v39 (scs_prop_equ_v39(scs_opp_v39 scs_4M6' ) 1)={}))`,
[STRIP_TAC
THEN GEN_TAC
THEN STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_4M7`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M7`;`v`]
THEN ASM_SIMP_TAC[SCS_4M6_BASIC;SCS_4M7_BASIC;SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;
SCS_4M7_IS_SCS;K_SCS_4M6;K_SCS_4M7;IN;BB_4M7_IMP_4M6_01]
THEN STRIP_TAC;
MATCH_MP_TAC PROP_EQU_IS_SCS
THEN MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
THEN EXISTS_TAC`scs_opp_v39 scs_4M6'`
THEN ASM_REWRITE_TAC[SCS_4M6_IS_SCS];
STRIP_TAC;
MATCH_MP_TAC Hexagons.BAISC_PROP_EQU
THEN MATCH_MP_TAC Cqaoqlr.BASIC_OPP
THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M6_BASIC];
ASM_REWRITE_TAC[Hexagons.K_SCS_PROP_EUQ]
THEN ASM_REWRITE_TAC[scs_opp_v39;scs_prop_equ_v39]
THEN SCS_TAC
THEN REAL_ARITH_TAC]);;
let SCS_4M7_ARROW_STAB_4M7_4M6=prove_by_refinement(
`main_nonlinear_terminal_v11
==> scs_arrow_v39 { scs_4M7 } ({scs_4M6', scs_prop_equ_v39(scs_opp_v39 scs_4M6' ) 1} UNION {scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j})`,
[
STRIP_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM;SET_RULE`a IN {b,c}<=> a= b\/ a=c`]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;
ASM_SIMP_TAC[SCS_4M6_IS_SCS];
MATCH_MP_TAC PROP_EQU_IS_SCS
THEN MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
THEN EXISTS_TAC`scs_opp_v39 scs_4M6'`
THEN ASM_REWRITE_TAC[SCS_4M6_IS_SCS];
ASM_SIMP_TAC[STAB_4M7_SCS;K_SCS_4M7];
DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M7 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M7 ==> MMs_v39 s = {}))`);
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN STRIP_TAC;
MP_TAC(SET_RULE`(!i j. scs_diag 4 i j ==> cstab < dist(v i,v j))\/ ~((!i j. scs_diag 4 i j ==> cstab < dist((v:num->real^3) i,v j)))`)
THEN RESA_TAC;
MP_TAC MIN_NOT_STAND_4M7
THEN RESA_TAC
THEN THAYTHE_TAC 0[`v`];
EXISTS_TAC`scs_4M6'`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC MM_4M7_IMP_MM_4M6_12
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[];
EXISTS_TAC`scs_prop_equ_v39 (scs_opp_v39 scs_4M6') 1`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC MM_4M7_IMP_MM_4M6_01
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN RESA_TAC
THEN MATCH_DICH_TAC 0
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`v:num->real^3`
THEN ASM_REWRITE_TAC[];
POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a b<=a`]
THEN STRIP_TAC
THEN MP_TAC MM_4M7_IMP_STAB_4M7
THEN RESA_TAC
THEN DICH_TAC 0
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN STRIP_TAC
THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M7 i j`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;
MATCH_MP_TAC(SET_RULE`A==> B\/A`)
THEN EXISTS_TAC`i:num`
THEN EXISTS_TAC`j:num`
THEN ASM_REWRITE_TAC[];
EXISTS_TAC`v':num->real^3`
THEN ASM_REWRITE_TAC[]]);;
(*************)
let K_SCS_OPP_4M6=prove(`scs_k_v39 (scs_opp_v39 scs_4M6') = 4`,
ASM_REWRITE_TAC[scs_opp_v39;scs_prop_equ_v39]
THEN SCS_TAC);;
let SCS_4M6_OPP_IS_SCS=prove(`is_scs_v39 (scs_opp_v39 scs_4M6')`,
MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
THEN EXISTS_TAC`scs_opp_v39 scs_4M6'`
THEN ASM_REWRITE_TAC[SCS_4M6_IS_SCS]);;
let YOBIMPP=prove(`main_nonlinear_terminal_v11
==> scs_arrow_v39 { scs_4M7 } {scs_4M6',scs_3T3,scs_3M1,scs_3T4}`,
STRIP_TAC
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`({scs_4M6', scs_prop_equ_v39(scs_opp_v39 scs_4M6' ) 1} UNION {scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j})`
THEN ASM_SIMP_TAC[SCS_4M7_ARROW_STAB_4M7_4M6;
SET_RULE`{scs_4M6',scs_3T3,scs_3M1,scs_3T4}={scs_4M6',scs_4M6'} UNION{scs_3T3,scs_3M1,scs_3T4}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[STAB_SCS_4M7_ARROW_3T3_3M1_3T4;SET_RULE`{A,B}={A} UNION {B}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC
THENL[
MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS];
MRESAS_TAC PRO_EQU_ID1[`scs_opp_v39 scs_4M6'`;`1`;`4`][SCS_4M6_IS_SCS;K_SCS_4M6;ARITH_RULE`(4 - 1 MOD 4)=3`;K_SCS_OPP_4M6;SCS_4M6_OPP_IS_SCS]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 (scs_opp_v39 scs_4M6') 1`;`3`][PROP_EQU_IS_SCS;SCS_4M6_IS_SCS;K_SCS_OPP_4M6;SCS_4M6_OPP_IS_SCS]
THEN DICH_TAC 0
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN REWRITE_TAC[]
THEN STRIP_TAC
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_opp_v39 scs_4M6'}`
THEN ASM_REWRITE_TAC[]
THEN ASSUME_TAC SCS_4M6_IS_SCS
THEN MRESA_TAC Yxionxl2.SCS_OPP_REFL[`scs_4M6'`]
THEN MRESAS_TAC YXIONXL2[`4`;`scs_opp_v39 scs_4M6'`][K_SCS_OPP_4M6;SCS_4M6_OPP_IS_SCS;ARITH_RULE`~(4<=3)`]]);;
(**************************)
let BB_4M8_IMP_4M6_23=prove(`main_nonlinear_terminal_v11 ==>
(!v.
MMs_v39 scs_4M8 v /\
(!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) /\
dist (v 2,v 3) = &2*h0
==> BBs_v39 scs_4M6' v)`,
REPEAT STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
THEN DICH_TAC 0
THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
THEN SCS_TAC
THEN THAYTHE_TAC 2[`i`;`j`]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN SCS_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[h0]
THEN REAL_ARITH_TAC);;
let MM_4M8_IMP_MM_4M6_23=prove(
`main_nonlinear_terminal_v11
==> (!v. MMs_v39 scs_4M8 v /\
(!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
dist (v 2,v 3) = &2 * h0
==> ~(MMs_v39 scs_4M6'={}))`,
STRIP_TAC
THEN GEN_TAC
THEN STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_4M8`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8`;`v`]
THEN ASM_SIMP_TAC[SCS_4M6_BASIC;SCS_4M8_BASIC;SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;
SCS_4M8_IS_SCS;K_SCS_4M6;K_SCS_4M8;IN;BB_4M8_IMP_4M6_23]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;
let BB_4M8_IMP_4M6_01=prove(
`main_nonlinear_terminal_v11 ==>
(!v.
MMs_v39 scs_4M8 v /\
(!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) /\
dist (v 0,v 1) = &2*h0
==> BBs_v39 ((scs_opp_v39 scs_4M6' ) ) v)`,
REPEAT STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
THEN DICH_TAC 0
THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;scs_prop_equ_v39;scs_opp_v39;peropp2]
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
THEN SCS_TAC
THEN THAYTHE_TAC 2[`i`;`j`]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+i:num`;`1+j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN MRESA_TAC MOD_ADD_MOD[`1`;`i`;`4`]
THEN MRESA_TAC MOD_ADD_MOD[`1`;`j`;`4`]
THEN SYM_ASSUM_TAC
THEN SYM_ASSUM_TAC
THEN ASSUME_TAC(ARITH_RULE`4-1=3/\ 4-0=4/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 3+2=5 /\3+3=6/\ 5 MOD 4=1/\ 6 MOD 4=2`)
THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN SCS_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[h0;REAL_ARITH`a<=a`]
THEN REAL_ARITH_TAC);;
let MM_4M8_IMP_MM_4M6_01=prove_by_refinement(`main_nonlinear_terminal_v11
==> (!v. MMs_v39 scs_4M8 v /\
(!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
dist (v 0,v 1) = &2 * h0
==> ~(MMs_v39 ((scs_opp_v39 scs_4M6' ) )={}))`,
[
STRIP_TAC
THEN GEN_TAC
THEN STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_4M8`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8`;`v`]
THEN ASM_SIMP_TAC[SCS_4M6_BASIC;SCS_4M8_BASIC;SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;
SCS_4M8_IS_SCS;K_SCS_4M6;K_SCS_4M8;IN;BB_4M8_IMP_4M6_01]
THEN STRIP_TAC;
MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
THEN EXISTS_TAC`scs_opp_v39 scs_4M6'`
THEN ASM_REWRITE_TAC[SCS_4M6_IS_SCS];
STRIP_TAC;
MATCH_MP_TAC Cqaoqlr.BASIC_OPP
THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M6_BASIC];
ASM_REWRITE_TAC[Hexagons.K_SCS_PROP_EUQ]
THEN ASM_REWRITE_TAC[scs_opp_v39;scs_prop_equ_v39]
THEN SCS_TAC
THEN REAL_ARITH_TAC]);;
let h0_LT_B_SCS_4M8=prove(`
(!i j. scs_diag 4 i j ==> &4 * h0 < scs_b_v39 scs_4M8 i j)
/\ (!i j. scs_diag 4 i j ==> scs_a_v39 scs_4M8 i j <= cstab)`,
SCS_TAC
THEN REWRITE_TAC[h0;SCS_DIAG_4_CASES;cstab]
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)`)
THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC
THEN MP_TAC sqrt8_LE_CSTAB
THEN REAL_ARITH_TAC);;
let SCS_4M8_STAND_OR_PRO=prove(`!i. scs_a_v39 scs_4M8 i (i + 1) = &2 /\
scs_b_v39 scs_4M8 i (i + 1) = &2 * h0 \/
scs_a_v39 scs_4M8 i (i + 1) = &2 * h0 /\
scs_b_v39 scs_4M8 i (i + 1) = cstab`,
GEN_TAC
THEN SCS_TAC
THEN SIMP_TAC[GSYM ADD1;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`SUC i:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`4`][ARITH_RULE`1<4`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN SCS_TAC);;
let SCS_4M8_STAND=prove(
`scs_a_v39 scs_4M8 0 1= &2*h0/\ scs_a_v39 scs_4M8 1 2 = &2 /\ scs_a_v39 scs_4M8 2 5= &2 /\scs_b_v39 scs_4M8 1 2= &2 *h0 /\scs_b_v39 scs_4M8 0 1 = cstab
/\scs_a_v39 scs_4M8 2 3 = &2 * h0/\ scs_a_v39 scs_4M8 3 4 = &2/\ scs_b_v39 scs_4M8 2 3= cstab/\ scs_a_v39 scs_4M8 1 4= &2* h0/\ scs_a_v39 scs_4M8 3 6= &2 * h0`,
SCS_TAC);;
let MIN_NOT_STAND_4M8=prove_by_refinement(
`main_nonlinear_terminal_v11 ==>
(!v.
MMs_v39 scs_4M8 v /\
(!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==>
dist (v 2,v 3) = &2 * h0 \/ dist (v 0,v 1) = &2*h0
\/ (dist (v 0,v 1) = cstab/\ dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = cstab/\
dist (v 3,v 0) = &2))`,
[
STRIP_TAC
THEN GEN_TAC
THEN STRIP_TAC
THEN ASSUME_TAC(SCS_4M8_IS_SCS)
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`]
THEN THAYTHES_TAC 0[`4`;`0`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`]
THEN THAYTHES_TAC 0[`5`;`1`][ARITH_RULE`5 MOD 4 = 1 MOD 4`;MOD_MULT_ADD;K_SCS_4M8]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`]
THEN THAYTHES_TAC 0[`6`;`2`][ARITH_RULE`6 MOD 4 = 2 MOD 4`;MOD_MULT_ADD;K_SCS_4M8]
THEN ASSUME_TAC h0_LT_B_SCS_4M8
THEN ASSUME_TAC SCS_4M8_STAND_OR_PRO
THEN ASSUME_TAC SCS_4M8_BASIC
THEN ASSUME_TAC K_SCS_4M8
THEN ASSUME_TAC SCS_4M8_STAND
THEN MP_TAC (SET_RULE`scs_is_str scs_4M8 v 0\/ ~(scs_is_str scs_4M8 v 0 )`)
THEN RESA_TAC;
MP_TAC VASYYAU
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`0`][ARITH_RULE`0+1=1`];
MP_TAC (SET_RULE`scs_is_str scs_4M8 v 2\/ ~(scs_is_str scs_4M8 v 2 )`)
THEN RESA_TAC;
MP_TAC VASYYAU
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`2`][ARITH_RULE`2+3=5/\ 2+1=3`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[];
MP_TAC (SET_RULE`scs_is_str scs_4M8 v 1\/ ~(scs_is_str scs_4M8 v 1 )`)
THEN RESA_TAC;
MP_TAC VASYYAU
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`1`][ARITH_RULE`1+1=2/\ 1+3=4`]
THEN MP_TAC PWEIWBZ
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`3`][ARITH_RULE`1+1=2/\ 3+1=4`]
THEN MRESAS_TAC NOT_STR_IN_CASES_4_1[`0`;`scs_4M8`;`v`][ARITH_RULE`0+a=a`;IN]
THEN MP_TAC TUAPYYU
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`2`][ARITH_RULE`1+1=2/\ 3+1=4/\ 2+1=3`;IN]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[];
MP_TAC (SET_RULE`scs_is_str scs_4M8 v 3\/ ~(scs_is_str scs_4M8 v 3 )`)
THEN RESA_TAC;
MP_TAC VASYYAU
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`3`][ARITH_RULE`3+1=4/\ 3+3=6`]
THEN MP_TAC PWEIWBZ
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`1`][ARITH_RULE`1+1=2/\ 3+1=4`]
THEN MP_TAC TUAPYYU
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`0`][ARITH_RULE`0+1=1/\ 3+1=4/\ 2+1=3`;IN]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[];
MP_TAC TUAPYYU
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`0`][ARITH_RULE`0+1=1/\ 3+1=4/\ 2+1=3`;IN]
THEN MP_TAC TUAPYYU
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`2`][ARITH_RULE`0+1=1/\ 3+1=4/\ 2+1=3`;IN]
THEN MP_TAC YEBWJNG
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`1`][ARITH_RULE`1+1=2/\ 3+1=4/\ 2+1=3`;IN]
THEN MRESAL_TAC STR_MOD_EQ[`4`;`scs_4M8`;`v`;`4`][SCS_4M8_IS_SCS;IN;ARITH_RULE`4 MOD 4=0`]
THEN MP_TAC YEBWJNG
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`3`][ARITH_RULE`1+1=2/\ 3+1=4/\ 2+1=3`;IN]]);;
let BB_4M8_IMP_scs_4M8_02=prove(
`main_nonlinear_terminal_v11
==> (!v. MMs_v39 scs_4M8 v /\
(!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
dist (v 0,v 1) = cstab/\ dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = cstab/\
dist (v 3,v 0) = &2 /\ dist(v 0, v 2)<= #3.62
==> BBs_v39 scs_4M8_02 v)`,
STRIP_TAC
THEN GEN_TAC
THEN STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
THEN DICH_TAC 0
THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8_02;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8_02;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8]
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
THEN SCS_TAC
THEN THAYTHE_TAC 2[`i`;`j`]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN SCS_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN RESA_TAC);;
let MM_4M8_IMP_MM_4M8_02=prove(`main_nonlinear_terminal_v11
==> (!v. MMs_v39 scs_4M8 v /\
(!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
dist (v 0,v 1) = cstab/\ dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = cstab/\
dist (v 3,v 0) = &2 /\ dist(v 0, v 2)<= #3.62
==> ~(MMs_v39 scs_4M8_02={}))`,
STRIP_TAC
THEN GEN_TAC
THEN STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_4M8`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8`;`v`]
THEN ASM_SIMP_TAC[SCS_4M8_02_BASIC;SCS_4M8_BASIC;SCS_4M8_02_IS_SCS;SCS_4M8_02_IS_SCS;
SCS_4M8_IS_SCS;K_SCS_4M8_02;K_SCS_4M8;IN;BB_4M8_IMP_scs_4M8_02]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;
let BB_4M8_IMP_scs_4M8_13=prove(
`main_nonlinear_terminal_v11
==> (!v. MMs_v39 scs_4M8 v /\
(!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
dist (v 0,v 1) = cstab/\ dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = cstab/\
dist (v 3,v 0) = &2 /\ dist(v 1, v 3)<= #3.62
==> BBs_v39 scs_4M8_13 v)`,
STRIP_TAC
THEN GEN_TAC
THEN STRIP_TAC
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
THEN DICH_TAC 0
THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8_13;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8_13;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8]
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
THEN SCS_TAC
THEN THAYTHE_TAC 2[`i`;`j`]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN SCS_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN RESA_TAC);;
let MM_4M8_IMP_MM_4M8_13=prove(`main_nonlinear_terminal_v11
==> (!v. MMs_v39 scs_4M8 v /\
(!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
dist (v 0,v 1) = cstab/\ dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = cstab/\
dist (v 3,v 0) = &2 /\ dist(v 1, v 3)<= #3.62
==> ~(MMs_v39 scs_4M8_13={}))`,
STRIP_TAC
THEN GEN_TAC
THEN STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_4M8`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8`;`v`]
THEN ASM_SIMP_TAC[SCS_4M8_13_BASIC;SCS_4M8_BASIC;SCS_4M8_13_IS_SCS;SCS_4M8_13_IS_SCS;
SCS_4M8_IS_SCS;K_SCS_4M8_13;K_SCS_4M8;IN;BB_4M8_IMP_scs_4M8_13]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;
let SCS_4M8_ARROW_STEP_ONE=prove_by_refinement(
`main_nonlinear_terminal_v11
==> scs_arrow_v39 { scs_4M8 } ({scs_4M6',scs_opp_v39 scs_4M6', scs_4M8_02,scs_4M8_13} UNION {scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j})`,
[STRIP_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM;SET_RULE`a IN {b,c,d,e}<=> a= b\/ a=c\/ a=d\/ a=e`]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;
ASM_SIMP_TAC[SCS_4M6_IS_SCS];
MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
THEN EXISTS_TAC`scs_opp_v39 scs_4M6'`
THEN ASM_REWRITE_TAC[SCS_4M6_IS_SCS];
ASM_SIMP_TAC[SCS_4M8_02_IS_SCS];
ASM_SIMP_TAC[SCS_4M8_13_IS_SCS];
ASM_SIMP_TAC[STAB_4M8_SCS;K_SCS_4M8];
DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M8 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M8 ==> MMs_v39 s = {}))`);
ASM_REWRITE_TAC[];
ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN STRIP_TAC;
MP_TAC(SET_RULE`(!i j. scs_diag 4 i j ==> cstab < dist(v i,v j))\/ ~((!i j. scs_diag 4 i j ==> cstab < dist((v:num->real^3) i,v j)))`)
THEN RESA_TAC;
MP_TAC MIN_NOT_STAND_4M8
THEN RESA_TAC
THEN THAYTHE_TAC 0[`v`];
EXISTS_TAC`scs_4M6'`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC MM_4M8_IMP_MM_4M6_23
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[];
EXISTS_TAC`(scs_opp_v39 scs_4M6') `
THEN ASM_REWRITE_TAC[]
THEN MP_TAC MM_4M8_IMP_MM_4M6_01
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[];
MP_TAC Bkossge.quad_diag_362
THEN RESA_TAC
THEN THAYTHE_TAC 0[`v 1`;`v 2`;`v 3`;`v 0`]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN STRIP_TAC;
EXISTS_TAC`(scs_4M8_13) `
THEN ASM_REWRITE_TAC[]
THEN MP_TAC MM_4M8_IMP_MM_4M8_13
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[];
DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN STRIP_TAC
THEN EXISTS_TAC`(scs_4M8_02) `
THEN ASM_REWRITE_TAC[]
THEN MP_TAC MM_4M8_IMP_MM_4M8_02
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN RESA_TAC
THEN MATCH_DICH_TAC 0
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`v:num->real^3`
THEN ASM_REWRITE_TAC[];
POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a b<=a`]
THEN STRIP_TAC
THEN MP_TAC MM_4M8_IMP_STAB_4M8
THEN RESA_TAC
THEN DICH_TAC 0
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN STRIP_TAC
THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M8 i j`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;
MATCH_MP_TAC(SET_RULE`A==> B\/A`)
THEN EXISTS_TAC`i:num`
THEN EXISTS_TAC`j:num`
THEN ASM_REWRITE_TAC[];
EXISTS_TAC`v':num->real^3`
THEN ASM_REWRITE_TAC[];
]);;
(****************************)
let SCS_DIAG_SCS_4M8_02_02=prove(`scs_diag (scs_k_v39 scs_4M8_02) 0 2`,
REWRITE_TAC[K_SCS_4M8_02;scs_diag]
THEN ARITH_TAC);;
let SCS_DIAG_SCS_4M8_02_13=prove(`scs_diag (scs_k_v39 scs_4M8_02) 1 3`,
REWRITE_TAC[K_SCS_4M8_02;scs_diag]
THEN ARITH_TAC);;
let SCS_DIAG_SCS_4M8_13_13=prove(`scs_diag (scs_k_v39 scs_4M8_13) 1 3`,
REWRITE_TAC[K_SCS_4M8_13;scs_diag]
THEN ARITH_TAC);;
let STAB_4M8_02_SCS=prove(` scs_diag (scs_k_v39 scs_4M8_02) i j
==> is_scs_v39 (scs_stab_diag_v39 scs_4M8_02 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M8_02 i j)`,
STRIP_TAC
THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M8_02_IS_SCS;SCS_4M8_02_BASIC;K_SCS_4M8_02;
ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
THEN SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN MP_TAC sqrt8_LE_CSTAB
THEN MP_TAC LE_sqrt8_2h0
THEN REAL_ARITH_TAC);;
let STAB_4M8_13_SCS=prove(` scs_diag (scs_k_v39 scs_4M8_13) i j
==> is_scs_v39 (scs_stab_diag_v39 scs_4M8_13 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M8_13 i j)`,
STRIP_TAC
THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M8_13_IS_SCS;SCS_4M8_13_BASIC;K_SCS_4M8_13;
ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
THEN SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN MP_TAC sqrt8_LE_CSTAB
THEN MP_TAC LE_sqrt8_2h0
THEN REAL_ARITH_TAC);;
let BASIC_HALF_SLICE=prove(`scs_basic_v39 s
==> scs_basic_v39 (scs_half_slice_v39 (s) p q d' F)`,
ASM_SIMP_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39]
THEN SET_TAC[]);;
let D_HALF_SLICE1=prove(`scs_d_v39 (scs_half_slice_v39 (s) p q d' mkj)=d'`,
SCS_TAC);;
let J_SCS_3T7_OPP_PROP=prove(`scs_J_v39 (scs_prop_equ_v39 (scs_opp_v39 scs_3T7) i) i1 j= F`,
REWRITE_TAC[scs_opp_v39;peropp2]
THEN SCS_TAC
THEN REWRITE_TAC[scs_opp_v39;peropp2]);;
let J_SCS_3T7_OPP=prove(`scs_J_v39 ((scs_opp_v39 scs_3T7) ) i1 j= F`,
REWRITE_TAC[scs_opp_v39;peropp2]
THEN SCS_TAC
THEN REWRITE_TAC[scs_opp_v39;peropp2]);;
let SCS_4M8_02_SLICE_02=prove_by_refinement(`scs_arrow_v39 {scs_4M8_02 } {scs_prop_equ_v39
( scs_opp_v39 scs_3T7) 2 }`,
[
ONCE_REWRITE_TAC[SET_RULE`{scs_prop_equ_v39
( scs_opp_v39 scs_3T7) 2}={scs_prop_equ_v39
( scs_opp_v39 scs_3T7) 2, scs_prop_equ_v39
( scs_opp_v39 scs_3T7) 2 }`]
THEN MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_02_13;STAB_4M8_02_SCS;SCS_K_D_A_STAB_EQ;SCS_4M8_02_IS_SCS]
THEN EXISTS_TAC`0`
THEN EXISTS_TAC`2`
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_02_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_3T7_BASIC;SCS_4M8_02_BASIC;J_SCS_4M8_02;BASIC_HALF_SLICE_STAB;J_SCS_3T7;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T7_BASIC;J_SCS_3T7_OPP_PROP;BASIC_HALF_SLICE;D_HALF_SLICE1;Cqaoqlr.BASIC_OPP;SCS_3T7_IS_SCS]
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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_02;scs_opp_v39]
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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_02;scs_opp_v39;peropp2;
ARITH_RULE`(2 + 1 + 4 - 0) MOD 4= 3/\ 0 MOD 4=0/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;peropp2;]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_02;scs_opp_v39]
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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_02;peropp2;scs_opp_v39;
ARITH_RULE`(0 + 1 + 4 - 2) MOD 4= 3/\ 2 MOD 4=2/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;peropp2]
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;
REWRITE_TAC[scs_opp_v39]
THEN SCS_TAC
THEN REAL_ARITH_TAC;
REWRITE_TAC[scs_opp_v39]
THEN SCS_TAC
THEN REAL_ARITH_TAC;
REWRITE_TAC[scs_opp_v39]
THEN SCS_TAC
THEN REAL_ARITH_TAC;
REWRITE_TAC[scs_opp_v39]
THEN 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_3T7_OPP_PROP];
]);;
let SCS_4M8_13_SLICE_13=prove_by_refinement(`scs_arrow_v39 {scs_4M8_13 } {scs_prop_equ_v39 scs_3T7 1}`,
[
ONCE_REWRITE_TAC[SET_RULE`{scs_prop_equ_v39
( scs_3T7) 1}={scs_prop_equ_v39
( scs_3T7) 1, scs_prop_equ_v39
( scs_3T7) 1 }`]
THEN MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_13_13;STAB_4M8_13_SCS;SCS_K_D_A_STAB_EQ;SCS_4M8_13_IS_SCS]
THEN EXISTS_TAC`1`
THEN EXISTS_TAC`3`
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_13_13]
THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
THEN REPEAT RESA_TAC;
REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC scs_inj
THEN ASM_SIMP_TAC[SCS_3T7_BASIC;SCS_4M8_13_BASIC;J_SCS_4M8_13;BASIC_HALF_SLICE_STAB;J_SCS_3T7;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T7_BASIC;J_SCS_3T7_1;BASIC_HALF_SLICE;D_HALF_SLICE1;Cqaoqlr.BASIC_OPP;SCS_3T7_IS_SCS]
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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_13;scs_opp_v39]
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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_13;scs_opp_v39;peropp2;
ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;peropp2;]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;
ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_13;scs_opp_v39]
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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_13;peropp2;scs_opp_v39;
ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;peropp2]
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;
REWRITE_TAC[scs_opp_v39]
THEN SCS_TAC
THEN REAL_ARITH_TAC;
REWRITE_TAC[scs_opp_v39]
THEN SCS_TAC
THEN REAL_ARITH_TAC;
REWRITE_TAC[scs_opp_v39]
THEN SCS_TAC
THEN REAL_ARITH_TAC;
REWRITE_TAC[scs_opp_v39]
THEN 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_3T7];
]);;
let SCS_4M8_13_ARROW_3T7=prove(`scs_arrow_v39 {scs_4M8_13 } {scs_3T7 }`,
MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3T7 1}`
THEN ASM_REWRITE_TAC[SCS_4M8_13_SLICE_13]
THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T7`;`1`;`3`][SCS_3T7_IS_SCS;K_SCS_3T7;ARITH_RULE`(3 - 1 MOD 3)=2`]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T7 1`;`2`][PROP_EQU_IS_SCS;SCS_3T7_IS_SCS]
THEN DICH_TAC 0
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN REWRITE_TAC[]);;
let K_SCS_OPP_3T7=prove(`scs_k_v39 (scs_opp_v39 scs_3T7) = 3`,
ASM_REWRITE_TAC[scs_opp_v39;scs_prop_equ_v39]
THEN SCS_TAC);;
let SCS_3T7_OPP_IS_SCS=prove(`is_scs_v39 (scs_opp_v39 scs_3T7)`,
MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
THEN EXISTS_TAC`scs_opp_v39 scs_3T7`
THEN ASM_REWRITE_TAC[SCS_3T7_IS_SCS]);;
let SCS_4M8_13_ARROW_3T7_OPP=prove(`scs_arrow_v39 {scs_4M8_02 } {scs_opp_v39 scs_3T7}`,
MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_prop_equ_v39
( scs_opp_v39 scs_3T7) 2}`
THEN ASM_REWRITE_TAC[SCS_4M8_02_SLICE_02]
THEN MRESAS_TAC PRO_EQU_ID1[`scs_opp_v39 scs_3T7`;`2`;`3`][SCS_3T7_IS_SCS;K_SCS_3T7;ARITH_RULE`(3 - 2 MOD 3)=1`;K_SCS_OPP_3T7;SCS_3T7_OPP_IS_SCS]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 (scs_opp_v39 scs_3T7) 2`;`1`][PROP_EQU_IS_SCS;SCS_3T7_IS_SCS;K_SCS_OPP_3T7;SCS_3T7_OPP_IS_SCS]
THEN DICH_TAC 0
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN REWRITE_TAC[]
THEN STRIP_TAC
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_opp_v39 scs_3T7}`
THEN ASM_REWRITE_TAC[]
THEN ASSUME_TAC SCS_3T7_IS_SCS
THEN MRESA_TAC Yxionxl2.SCS_OPP_REFL[`scs_3T7`]
THEN MRESAS_TAC YXIONXL2[`3`;`scs_opp_v39 scs_3T7`][K_SCS_OPP_3T7;SCS_3T7_OPP_IS_SCS;ARITH_RULE`~(4<=3)`]);;
let PROP_OPP_4M8_13= prove_by_refinement(
`scs_4M8_13= scs_prop_equ_v39(scs_opp_v39 (scs_4M8_02)) 2 `,
[REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;SCS_K_D_A_STAB_EQ;scs_opp_v39;scs_4M8_13;scs_4M8_02]
THEN MATCH_MP_TAC scs_inj
THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M8_BASIC;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_13;scs_basic;unadorned_v39;peropp;peropp2]
THEN SCS_TAC
THEN STRIP_TAC;
SET_TAC[];
STRIP_TAC
THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;]
THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
THEN REPEAT GEN_TAC
THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
THEN SYM_ASSUM_TAC
THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
THEN SYM_ASSUM_TAC
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/ x' MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_4_TAC;PSORT_5_EXPLICIT;ARITH_RULE`4-1=3/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6
/\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;
let SCS_4M8_02_ARROW_4M8_13=prove(
`scs_arrow_v39 {scs_4M8_02}{scs_4M8_13}`,
ASM_SIMP_TAC[PROP_OPP_4M8_13]
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_opp_v39 (scs_4M8_02)}`
THEN STRIP_TAC
THENL[
MATCH_MP_TAC (GEN_ALL YXIONXL2)
THEN EXISTS_TAC`4`
THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M8_02;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02;SCS_4M8_02_IS_SCS];
MATCH_MP_TAC(GEN_ALL YXIONXL3)
THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
THEN EXISTS_TAC`scs_opp_v39 ( scs_4M8_02)`
THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M8;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02;SCS_4M8_02_IS_SCS];]);;
let SCS_4M8_02_ARROW_3T7 =prove(`scs_arrow_v39 { scs_4M8_02 } { scs_3T7 }`,
MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_4M8_13}`
THEN ASM_SIMP_TAC[SCS_4M8_02_ARROW_4M8_13;SCS_4M8_13_ARROW_3T7]);;
(************************************)
let MIQMCSN=prove(`main_nonlinear_terminal_v11
==> scs_arrow_v39 { scs_4M8 } ({scs_4M6',scs_3T7,scs_3T4})`,
STRIP_TAC
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`({scs_4M6',scs_opp_v39 scs_4M6', scs_4M8_02,scs_4M8_13} UNION {scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j})`
THEN ASM_SIMP_TAC[SCS_4M8_ARROW_STEP_ONE;SET_RULE`{scs_4M6', scs_3T7, scs_3T4}={scs_4M6', scs_3T7}UNION{ scs_3T4}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_REWRITE_TAC[SET_STAB_4M8_ARROW_3T4;]
THEN ONCE_REWRITE_TAC[SET_RULE`{scs_4M6', scs_3T7}={scs_4M6',scs_4M6', scs_3T7,scs_3T7}`]
THEN ASM_REWRITE_TAC[SET_RULE` {A,B,C,D}=({A,B,C}) UNION {D}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_REWRITE_TAC[SCS_4M8_13_ARROW_3T7;SET_RULE` {A,B,D}=({A,B}) UNION {D}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_REWRITE_TAC[SCS_4M8_02_ARROW_3T7;SET_RULE` {A,D}=({A}) UNION {D}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC
THENL[
MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS];
ASSUME_TAC(SCS_4M6_IS_SCS)
THEN ASSUME_TAC K_SCS_OPP_4M6
THEN ASSUME_TAC SCS_4M6_OPP_IS_SCS
THEN MRESA_TAC Yxionxl2.SCS_OPP_REFL[`scs_4M6'`]
THEN MRESAL_TAC YXIONXL2[`4`;`scs_opp_v39 scs_4M6'`][ARITH_RULE`~(4<=3)`]]);;
end;;
(*
let check_completeness_claimA_concl =
Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
*)