(* ========================================================================== *)
(* 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<a)/\ &2 * #1.26 < #3.01/\ ~(&2 * #1.26 < &2) `;PSORT_5_EXPLICIT;LT_sqrt8_2h0]; ASM_REWRITE_TAC[Geomdetail.CARD_SING] THEN ARITH_TAC; ]);;
let SCS_4M8_02_IS_SCS=
prove_by_refinement(`is_scs_v39 scs_4M8_02`,
[ SIMP_TAC[scs_4M8_02;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 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<a)/\ &2 * #1.26 < #3.01/\ ~(&2 * #1.26 < &2) `;PSORT_5_EXPLICIT;LT_sqrt8_2h0;]; ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=2)`] THEN ARITH_TAC; ]);;
let SCS_4M8_13_IS_SCS=
prove_by_refinement(`is_scs_v39 scs_4M8_13`,
[ SIMP_TAC[scs_4M8_13;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 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<a)/\ &2 * #1.26 < #3.01/\ ~(&2 * #1.26 < &2) `;PSORT_5_EXPLICIT;LT_sqrt8_2h0;]; ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=2)`] THEN ARITH_TAC; ]);;
let SCS_3T4_prime2_IS_SCS=
prove_by_refinement( `is_scs_v39 scs_3T4_prime2`,
[SIMP_TAC[scs_3T4_prime2;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.2759 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN REAL_ARITH_TAC; MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\ (&2 * h0 < funlist_v39 [(0,1),&2 * h0] cstab 3 i (SUC i) \/ &2 < funlist_v39 [(0,1),&2; (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} `,
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} `,
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<a`] THEN RESA_TAC; THAYTHEL_TAC (18-2)[`1`;`3`][scs_diag;ARITH_RULE`~(1 MOD 4 = 3 MOD 4) /\ ~(SUC 1 MOD 4 = 3 MOD 4) /\ ~(1 MOD 4 = SUC 3 MOD 4)`] THEN DICH_TAC 0 THEN ONCE_REWRITE_TAC[DIST_SYM] THEN DICH_TAC 0 THEN REAL_ARITH_TAC ; THAYTHEL_TAC (18-2)[`0`;`2`][scs_diag;ARITH_RULE`~(0 MOD 4 = 2 MOD 4) /\ ~(SUC 0 MOD 4 = 2 MOD 4) /\ ~(0 MOD 4 = SUC 2 MOD 4)`] THEN DICH_TAC 0 THEN DICH_TAC 0 THEN REAL_ARITH_TAC ; MP_TAC (SET_RULE`scs_is_str scs_4M6' v 1\/ ~(scs_is_str scs_4M6' v 1 )`) THEN RESA_TAC; MP_TAC VASYYAU THEN RESA_TAC THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`1`][ARITH_RULE`1+3=4`] 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<a`] THEN RESA_TAC; THAYTHEL_TAC (19-2)[`1`;`3`][scs_diag;ARITH_RULE`~(1 MOD 4 = 3 MOD 4) /\ ~(SUC 1 MOD 4 = 3 MOD 4) /\ ~(1 MOD 4 = SUC 3 MOD 4)`] THEN DICH_TAC 0 THEN ONCE_REWRITE_TAC[DIST_SYM] THEN DICH_TAC 0 THEN REAL_ARITH_TAC ; THAYTHEL_TAC (19-2)[`0`;`2`][scs_diag;ARITH_RULE`~(0 MOD 4 = 2 MOD 4) /\ ~(SUC 0 MOD 4 = 2 MOD 4) /\ ~(0 MOD 4 = SUC 2 MOD 4)`] THEN DICH_TAC 0 THEN DICH_TAC 0 THEN REAL_ARITH_TAC ; MP_TAC TUAPYYU THEN RESA_TAC THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`0`][IN;ARITH_RULE`0+1=1`]; 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<a`] THEN RESA_TAC; THAYTHEL_TAC (18-2)[`1`;`3`][scs_diag;ARITH_RULE`~(1 MOD 4 = 3 MOD 4) /\ ~(SUC 1 MOD 4 = 3 MOD 4) /\ ~(1 MOD 4 = SUC 3 MOD 4)`] THEN DICH_TAC 0 THEN ONCE_REWRITE_TAC[DIST_SYM] THEN DICH_TAC 0 THEN REAL_ARITH_TAC ; THAYTHEL_TAC (18-2)[`0`;`2`][scs_diag;ARITH_RULE`~(0 MOD 4 = 2 MOD 4) /\ ~(SUC 0 MOD 4 = 2 MOD 4) /\ ~(0 MOD 4 = SUC 2 MOD 4)`] THEN DICH_TAC 0 THEN DICH_TAC 0 THEN REAL_ARITH_TAC ; ]);;
let BB_4M6_IMP_scs_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)) ==> 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)<=> 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)<=> 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)<=> 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)`,
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) *)