(* ========================================================================== *)
(* 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} `,

ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M7_IS_SCS;K_SCS_4M7]);;

let SET_EQ_DIAG_STAB_4M7=
prove_by_refinement(`scs_arrow_v39
 { scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4M7 0 2,scs_stab_diag_v39 scs_4M7 1 3}`,

[
ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M7;SET_STAB_4M7;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
THEN 
REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M7 (i + 2) i |i=0\/i=1\/i=2\/i=3}
= {scs_stab_diag_v39 scs_4M7 (0 + 2) 0} UNION
{scs_stab_diag_v39 scs_4M7 (1 + 2) 1} UNION
{scs_stab_diag_v39 scs_4M7 (2 + 2) 2} UNION
{scs_stab_diag_v39 scs_4M7 (3 + 2) 3} 
`;]
THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M7 0 2,scs_stab_diag_v39 scs_4M7 1 3}={scs_stab_diag_v39 scs_4M7 0 2} UNION {scs_stab_diag_v39 scs_4M7 1 3}UNION {scs_stab_diag_v39 scs_4M7 0 2} UNION {scs_stab_diag_v39 scs_4M7 1 3}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
THEN MRESA_TAC STAB_SYM[`scs_4M7`;`0`;`2`]
THEN STRIP_TAC;

MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[STAB_4M7_SCS;SCS_DIAG_SCS_4M7_02];

MATCH_MP_TAC FZIOTEF_UNION
THEN MRESA_TAC STAB_SYM[`scs_4M7`;`1`;`3`]
THEN STRIP_TAC;

MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[STAB_4M7_SCS;SCS_DIAG_SCS_4M7_13];

MATCH_MP_TAC FZIOTEF_UNION
THEN MRESAL_TAC STAB_MOD[`scs_4M7`;`4`;`2`][SCS_4M7_IS_SCS;K_SCS_4M7;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
THEN SYM_ASSUM_TAC
THEN STRIP_TAC;

MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[STAB_4M7_SCS;SCS_DIAG_SCS_4M7_02];

MRESAL_TAC STAB_MOD[`scs_4M7`;`5`;`3`][SCS_4M7_IS_SCS;K_SCS_4M7;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
THEN SYM_ASSUM_TAC;

MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[STAB_4M7_SCS;SCS_DIAG_SCS_4M7_13]]);;


let SCS_4M7_SLICE_13=
prove_by_refinement(
`scs_arrow_v39 {scs_stab_diag_v39 scs_4M7 1 3 } {scs_prop_equ_v39 scs_3T4_prime 2,   scs_3T4_prime2  }`,

[

MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M7_13;STAB_4M7_SCS;SCS_K_D_A_STAB_EQ;]
THEN EXISTS_TAC`1`
THEN EXISTS_TAC`3`
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M7_13]
THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
THEN REPEAT RESA_TAC;

REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC scs_inj
THEN ASM_SIMP_TAC[SCS_3T4_prime_BASIC;SCS_4M7_BASIC;J_SCS_4M7;BASIC_HALF_SLICE_STAB;J_SCS_3T4_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T4_prime2_BASIC;J_SCS_3T4_prime2]
THEN STRIP_TAC;

ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7]
THEN ARITH_TAC;

STRIP_TAC
THEN 
ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;
ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;

ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7]
THEN ARITH_TAC;


STRIP_TAC
THEN 
ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;
ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;


SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;


SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;



POP_ASSUM MP_TAC
THEN REWRITE_TAC[J_SCS_3T4_prime];

]);;

let SCS_4M7_SLICE_13_ARROW_3T4=
prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M7 1 3 } { scs_3T4}`,

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3T4_prime 2,   scs_3T4_prime2  }`
THEN ASM_REWRITE_TAC[SCS_4M7_SLICE_13]
THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}/\ {scs_3T4}= {scs_3T4}UNION {scs_3T4}`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}/\ {scs_3T4}= {scs_3T4}UNION {scs_3T4}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_REWRITE_TAC[SCS_3T4_prime2_ARROW_MM_3T4;SCS_3T4_prime_ARROW_MM_3T4]
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_3T4_prime}`
THEN ASM_REWRITE_TAC[SCS_3T4_prime2_ARROW_MM_3T4;SCS_3T4_prime_ARROW_MM_3T4]
THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T4_prime`;`2`;`3`][SCS_3T4_prime_IS_SCS;K_SCS_3T4_prime;ARITH_RULE`(3 - 2 MOD 3)=1`]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T4_prime 2`;`1`][PROP_EQU_IS_SCS;SCS_3T4_prime_IS_SCS]
THEN DICH_TAC 0
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN REWRITE_TAC[]);;

let SCS_4M7_SLICE_02=
prove_by_refinement(
`scs_arrow_v39 {scs_stab_diag_v39 scs_4M7 0 2 } {scs_prop_equ_v39 scs_3T3_prime 1,  scs_prop_equ_v39 scs_3M1_prime 1  }`,

[
MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M7_02;STAB_4M7_SCS;SCS_K_D_A_STAB_EQ;]
THEN EXISTS_TAC`0`
THEN EXISTS_TAC`2`
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M7_02]
THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
THEN REPEAT RESA_TAC;


REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC scs_inj
THEN ASM_SIMP_TAC[SCS_3T3_prime_BASIC;SCS_4M7_BASIC;J_SCS_4M7;BASIC_HALF_SLICE_STAB;J_SCS_3T3_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3M1_prime_BASIC;J_SCS_3M1_prime]
THEN STRIP_TAC;


ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T3_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7]
THEN ARITH_TAC;

STRIP_TAC
THEN 
ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;
ARITH_RULE`(2 + 1 + 4 - 0) MOD 4= 3/\ 0 MOD 4=0/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;

ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7]
THEN ARITH_TAC;


STRIP_TAC
THEN 
ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;
ARITH_RULE`(0 + 1 + 4 - 2) MOD 4= 3/\ 2 MOD 4=2/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;


SCS_TAC
THEN REAL_ARITH_TAC;


SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;



POP_ASSUM MP_TAC
THEN REWRITE_TAC[J_SCS_3T3_prime];

]);;


let SCS_4M7_SLICE_02_ARROW_3T3_3M1=
prove(
`scs_arrow_v39 {scs_stab_diag_v39 scs_4M7 0 2 } { scs_3T3,scs_3M1}`,

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3T3_prime 1, scs_prop_equ_v39 scs_3M1_prime 1}`
THEN ASM_REWRITE_TAC[SCS_4M7_SLICE_02]
THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC
THENL[

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_3T3_prime}`
THEN ASM_REWRITE_TAC[SCS_3T3_prime_ARROW_MM_3T3]
THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T3_prime`;`1`;`3`][SCS_3T3_prime_IS_SCS;K_SCS_3T3_prime;ARITH_RULE`(3 - 1 MOD 3)=2`]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T3_prime 1`;`2`][PROP_EQU_IS_SCS;SCS_3T3_prime_IS_SCS]
THEN DICH_TAC 0
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN REWRITE_TAC[];

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_3M1_prime}`
THEN ASM_REWRITE_TAC[SCS_3M1_prime_ARROW_MM_3M1]
THEN MRESAS_TAC PRO_EQU_ID1[`scs_3M1_prime`;`1`;`3`][SCS_3M1_prime_IS_SCS;K_SCS_3M1_prime;ARITH_RULE`(3 - 1 MOD 3)=2`]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1_prime 1`;`2`][PROP_EQU_IS_SCS;SCS_3M1_prime_IS_SCS]
THEN DICH_TAC 0
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN REWRITE_TAC[]]);;


let STAB_SCS_4M7_ARROW_3T3_3M1_3T4=
prove(
`scs_arrow_v39
 { scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j } {scs_3T3,scs_3M1,scs_3T4}`,

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M7 0 2,scs_stab_diag_v39 scs_4M7 1 3}`
THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_4M7;SET_RULE`{A,B}={A}UNION {B}`;SET_RULE`{scs_3T3,scs_3M1,scs_3T4}={scs_3T3,scs_3M1} UNION{scs_3T4}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_REWRITE_TAC[SCS_4M7_SLICE_13_ARROW_3T4;SET_RULE`{A}UNION{B}={A,B}`;SCS_4M7_SLICE_02_ARROW_3T3_3M1]);;


(***************************)

let BB_4M8_IMP_BB_STAN_4M8= 
prove(`
    BBs_v39 scs_4M8 v /\
    scs_diag 4 i j /\
   dist(v i,v j)<= cstab ==>
    BBs_v39 (scs_stab_diag_v39 scs_4M8 i j) v`,

SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8]
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
THEN SCS_TAC
THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
THEN RESA_TAC
THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
THENL[
MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8;SCS_4M8_IS_SCS]
THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];

MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8;SCS_4M8_IS_SCS]
THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]]);;

let MM_4M8_IMP_STAB_4M8=
prove(`
   MMs_v39 scs_4M8 v /\
    scs_diag 4 i j /\
   dist(v i,v j)<= cstab ==>
    ~(MMs_v39 (scs_stab_diag_v39 scs_4M8 i j) ={})`,

STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC` scs_4M8 `
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8 `;`v`]
THEN ASSUME_TAC SCS_4M8_BASIC
THEN ASSUME_TAC K_SCS_4M8
THEN ASM_SIMP_TAC[SCS_4M8_IS_SCS;SCS_4M8_IS_SCS;SCS_4M8_BASIC;K_SCS_4M8;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M8_13;BB_4M8_IMP_BB_STAN_4M8;STAB_4M8_SCS]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;


let SET_STAB_4M8=
prove(`{ scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M8 (i MOD 4) (j  MOD 4)| scs_diag 4 (i MOD 4) (j  MOD 4) }`,

 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
THEN MRESAL_TAC STAB_MOD[`scs_4M8`][SCS_4M8_IS_SCS;K_SCS_4M8]);;
let EXPAND_STAB_DIAG_4M8=
prove(`
{scs_stab_diag_v39 scs_4M8 (i MOD 4) (j MOD 4) | j MOD 4 =
                                                  (i MOD 4 + 2) MOD 4}=
{scs_stab_diag_v39 scs_4M8 (i+2) i| i<4} `,

ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M8_IS_SCS;K_SCS_4M8]);;

let SET_EQ_DIAG_STAB_4M8=
prove_by_refinement(`scs_arrow_v39
 { scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4M8 0 2,scs_stab_diag_v39 scs_4M8 1 3}`,

[
ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M8;SET_STAB_4M8;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
THEN 
REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M8 (i + 2) i |i=0\/i=1\/i=2\/i=3}
= {scs_stab_diag_v39 scs_4M8 (0 + 2) 0} UNION
{scs_stab_diag_v39 scs_4M8 (1 + 2) 1} UNION
{scs_stab_diag_v39 scs_4M8 (2 + 2) 2} UNION
{scs_stab_diag_v39 scs_4M8 (3 + 2) 3} 
`;]
THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M8 0 2,scs_stab_diag_v39 scs_4M8 1 3}={scs_stab_diag_v39 scs_4M8 0 2} UNION {scs_stab_diag_v39 scs_4M8 1 3}UNION {scs_stab_diag_v39 scs_4M8 0 2} UNION {scs_stab_diag_v39 scs_4M8 1 3}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
THEN MRESA_TAC STAB_SYM[`scs_4M8`;`0`;`2`]
THEN STRIP_TAC;

MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02];

MATCH_MP_TAC FZIOTEF_UNION
THEN MRESA_TAC STAB_SYM[`scs_4M8`;`1`;`3`]
THEN STRIP_TAC;

MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[STAB_4M8_SCS;SCS_DIAG_SCS_4M8_13];

MATCH_MP_TAC FZIOTEF_UNION
THEN MRESAL_TAC STAB_MOD[`scs_4M8`;`4`;`2`][SCS_4M8_IS_SCS;K_SCS_4M8;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
THEN SYM_ASSUM_TAC
THEN STRIP_TAC;

MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02];

MRESAL_TAC STAB_MOD[`scs_4M8`;`5`;`3`][SCS_4M8_IS_SCS;K_SCS_4M8;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
THEN SYM_ASSUM_TAC;

MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[STAB_4M8_SCS;SCS_DIAG_SCS_4M8_13]]);;




let PROP_OPP_DIAG_4M8_13= 
prove_by_refinement(`scs_stab_diag_v39 scs_4M8 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4M8 0 2)) 2 `,

[REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;SCS_K_D_A_STAB_EQ;scs_opp_v39]
THEN MATCH_MP_TAC scs_inj
THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M8_BASIC;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_13;scs_basic;unadorned_v39;peropp;peropp2]
THEN SCS_TAC
THEN STRIP_TAC;


SET_TAC[];

STRIP_TAC
THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;]
THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
THEN REPEAT GEN_TAC
THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
THEN SYM_ASSUM_TAC
THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
THEN SYM_ASSUM_TAC
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/ x' MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_4_TAC;PSORT_5_EXPLICIT;ARITH_RULE`4-1=3/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6
/\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;




let STAB_4M8_02_ARROW_4M8_13=
prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M8 0 2}{scs_stab_diag_v39 scs_4M8 1 3}`,

ASM_SIMP_TAC[PROP_OPP_DIAG_4M8_13]
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4M8 0 2)}`
THEN STRIP_TAC
THENL[
MATCH_MP_TAC (GEN_ALL YXIONXL2)
THEN EXISTS_TAC`4`
THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M8;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02]
;

MATCH_MP_TAC(GEN_ALL YXIONXL3)
THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4M8 0 2)`
THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M8;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02]]);;


let SCS_4M8_SLICE_13=
prove_by_refinement(
`scs_arrow_v39 {scs_stab_diag_v39 scs_4M8 1 3 } {scs_3T4_prime2  }`,

[
ONCE_REWRITE_TAC[SET_RULE`{scs_3T4_prime2}={scs_3T4_prime2,    scs_3T4_prime2}`]
THEN MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_13;STAB_4M8_SCS;SCS_K_D_A_STAB_EQ;]
THEN EXISTS_TAC`1`
THEN EXISTS_TAC`3`
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_13]
THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
THEN REPEAT RESA_TAC;

REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC scs_inj
THEN ASM_SIMP_TAC[SCS_3T4_prime_BASIC;SCS_4M8_BASIC;J_SCS_4M8;BASIC_HALF_SLICE_STAB;J_SCS_3T4_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T4_prime2_BASIC;J_SCS_3T4_prime2_1]
THEN STRIP_TAC;


ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8]
THEN ARITH_TAC;

STRIP_TAC
THEN 
ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8;
ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;

ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8]
THEN ARITH_TAC;


STRIP_TAC
THEN 
ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8;
ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;


SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;


SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;



POP_ASSUM MP_TAC
THEN REWRITE_TAC[J_SCS_3T4_prime2_1];

]);;



let SCS_4M8_SLICE_13_ARROW_3T4=
prove(
`scs_arrow_v39 {scs_stab_diag_v39 scs_4M8 1 3 } { scs_3T4}`,

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{ scs_3T4_prime2  }`
THEN ASM_REWRITE_TAC[SCS_4M8_SLICE_13]
THEN ASM_REWRITE_TAC[SCS_3T4_prime2_ARROW_MM_3T4;SCS_3T4_prime_ARROW_MM_3T4]);;

let SCS_4M8_SLICE_02_ARROW_3T4 =
prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_4M8 0 2 } { scs_3T4 }`,

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M8 1 3}`
THEN ASM_SIMP_TAC[STAB_4M8_02_ARROW_4M8_13;SCS_4M8_SLICE_13_ARROW_3T4]);;


let SET_STAB_4M8_ARROW_3T4=
prove(`scs_arrow_v39
 { scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j } {scs_3T4}`,

ONCE_REWRITE_TAC[SET_RULE`{A}={A,A}`]
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M8 0 2,scs_stab_diag_v39 scs_4M8 1 3}`
THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M8;]
THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`;]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[SCS_4M8_SLICE_02_ARROW_3T4;SCS_4M8_SLICE_13_ARROW_3T4]);;

(*****************)

let h0_LT_B_SCS_4M6=
prove(`
(!i j. scs_diag 4 i j ==> &4 * h0 < scs_b_v39 scs_4M6' i j)
/\ (!i j. scs_diag 4 i j ==> scs_a_v39 scs_4M6' i j <= cstab)`,

SCS_TAC
THEN REWRITE_TAC[h0;SCS_DIAG_4_CASES;cstab]
THEN REPEAT RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`~(4=0)`)
THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC
THEN MP_TAC sqrt8_LE_CSTAB
THEN REAL_ARITH_TAC);;
let SCS_4M6_STAND_OR_PRO=
prove(`!i. scs_a_v39 scs_4M6' i (i + 1) = &2 /\
           scs_b_v39 scs_4M6' i (i + 1) = &2 * h0 \/
           scs_a_v39 scs_4M6' i (i + 1) = &2 * h0 /\
           scs_b_v39 scs_4M6' i (i + 1) = cstab`,

GEN_TAC
THEN SCS_TAC
THEN SIMP_TAC[GSYM ADD1;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`SUC i:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`4`][ARITH_RULE`1<4`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN SCS_TAC);;



let SCS_4M6_STAND=
prove(`scs_a_v39 scs_4M6' 1 2 = &2/\ scs_a_v39 scs_4M6' 2 3 = &2/\ scs_a_v39 scs_4M6'  3 4 = &2/\ scs_a_v39 scs_4M6' 0 1= &2 * h0
/\ scs_a_v39 scs_4M6' 1 4= &2 * h0
/\ scs_b_v39 scs_4M6' 0 1= cstab`,

SCS_TAC);;

let h0_CSTAB_LT_4=
prove(`&2< &2*h0 /\ cstab< &4/\ &2<= &2*h0 /\ cstab<= &4
/\ &2*h0< &4/\ &2< &4 /\ ~(&2 * h0 = &2)`,

REWRITE_TAC[cstab;h0]
THEN REAL_ARITH_TAC);;
let EXTREMAL_SCS_4M6=
prove_by_refinement(`main_nonlinear_terminal_v11 ==>
(!v. 
    MMs_v39 scs_4M6' v /\
    (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) ==>
    dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = &2/\dist (v 3,v 0) = &2
/\ dist (v 0,v 1) = cstab)`,

[
STRIP_TAC
THEN GEN_TAC
THEN STRIP_TAC
THEN ASSUME_TAC(SCS_4M6_IS_SCS)
THEN MRESA_TAC MMS_IMP_BBS[`scs_4M6'`;`v`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M6'`]
THEN THAYTHES_TAC 0[`4`;`0`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M6]
THEN MP_TAC PWEIWBZ
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`1`][SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;h0_LT_B_SCS_4M6;SCS_4M6_STAND_OR_PRO;ARITH_RULE`1+1=2`;SCS_4M6_STAND]
THEN MP_TAC PWEIWBZ
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`2`][SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;h0_LT_B_SCS_4M6;SCS_4M6_STAND_OR_PRO;ARITH_RULE`2+1=3`;SCS_4M6_STAND]
THEN MP_TAC PWEIWBZ
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`3`][SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;h0_LT_B_SCS_4M6;SCS_4M6_STAND_OR_PRO;ARITH_RULE`3+1=4`;SCS_4M6_STAND]
THEN ASSUME_TAC SCS_4M6_BASIC
THEN ASSUME_TAC K_SCS_4M6
THEN ASSUME_TAC h0_LT_B_SCS_4M6
THEN ASSUME_TAC SCS_4M6_STAND_OR_PRO
THEN ASSUME_TAC SCS_4M6_STAND
THEN ASSUME_TAC h0_CSTAB_LT_4
THEN MP_TAC (SET_RULE`scs_is_str scs_4M6' v 0\/ ~(scs_is_str scs_4M6' v 0 )`)
THEN RESA_TAC;

MP_TAC VASYYAU
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`0`][ARITH_RULE`0+1=1`]
THEN MP_TAC Bkossge.quad_nonexist_849
THEN ASM_REWRITE_TAC[NOT_EXISTS_THM]
THEN STRIP_TAC
THEN THAYTHE_TAC 0[`v 1`;`v 2`;`v 3`;`v 0`;]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[DE_MORGAN_THM;REAL_ARITH`~(a<=b)<=> b<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)`,

ASM_SIMP_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39]
THEN SET_TAC[]);;
let D_HALF_SLICE1=
prove(`scs_d_v39 (scs_half_slice_v39 (s) p q d' mkj)=d'`,

SCS_TAC);;
let J_SCS_3T7_OPP_PROP=
prove(`scs_J_v39 (scs_prop_equ_v39 (scs_opp_v39 scs_3T7) i) i1 j= F`,

REWRITE_TAC[scs_opp_v39;peropp2]
THEN SCS_TAC 
THEN REWRITE_TAC[scs_opp_v39;peropp2]);;

let J_SCS_3T7_OPP=
prove(`scs_J_v39 ((scs_opp_v39 scs_3T7) ) i1 j= F`,

REWRITE_TAC[scs_opp_v39;peropp2]
THEN SCS_TAC 
THEN REWRITE_TAC[scs_opp_v39;peropp2]);;


let SCS_4M8_02_SLICE_02=
prove_by_refinement(`scs_arrow_v39 {scs_4M8_02 } {scs_prop_equ_v39 
( scs_opp_v39 scs_3T7) 2 }`,

[

ONCE_REWRITE_TAC[SET_RULE`{scs_prop_equ_v39 
( scs_opp_v39 scs_3T7) 2}={scs_prop_equ_v39 
( scs_opp_v39 scs_3T7) 2, scs_prop_equ_v39 
( scs_opp_v39 scs_3T7) 2 }`]
THEN MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_02_13;STAB_4M8_02_SCS;SCS_K_D_A_STAB_EQ;SCS_4M8_02_IS_SCS]
THEN EXISTS_TAC`0`
THEN EXISTS_TAC`2`
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_02_02]
THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
THEN REPEAT RESA_TAC;

REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC scs_inj
THEN ASM_SIMP_TAC[SCS_3T7_BASIC;SCS_4M8_02_BASIC;J_SCS_4M8_02;BASIC_HALF_SLICE_STAB;J_SCS_3T7;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T7_BASIC;J_SCS_3T7_OPP_PROP;BASIC_HALF_SLICE;D_HALF_SLICE1;Cqaoqlr.BASIC_OPP;SCS_3T7_IS_SCS]
THEN STRIP_TAC;

ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_02;scs_opp_v39]
THEN ARITH_TAC;

STRIP_TAC
THEN 
ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_02;scs_opp_v39;peropp2;
ARITH_RULE`(2 + 1 + 4 - 0) MOD 4= 3/\ 0 MOD 4=0/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;peropp2;]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;

ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_02;scs_opp_v39]
THEN ARITH_TAC;

STRIP_TAC
THEN 
ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_02;peropp2;scs_opp_v39;
ARITH_RULE`(0 + 1 + 4 - 2) MOD 4= 3/\ 2 MOD 4=2/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;peropp2]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;

REWRITE_TAC[scs_opp_v39]
THEN SCS_TAC
THEN REAL_ARITH_TAC;

REWRITE_TAC[scs_opp_v39]
THEN SCS_TAC
THEN REAL_ARITH_TAC;

REWRITE_TAC[scs_opp_v39]
THEN SCS_TAC
THEN REAL_ARITH_TAC;

REWRITE_TAC[scs_opp_v39]
THEN SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;


SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[J_SCS_3T7_OPP_PROP];
]);;




let SCS_4M8_13_SLICE_13=
prove_by_refinement(`scs_arrow_v39 {scs_4M8_13 } {scs_prop_equ_v39  scs_3T7 1}`,

[
ONCE_REWRITE_TAC[SET_RULE`{scs_prop_equ_v39 
(  scs_3T7) 1}={scs_prop_equ_v39 
(  scs_3T7) 1, scs_prop_equ_v39 
(  scs_3T7) 1 }`]
THEN MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_13_13;STAB_4M8_13_SCS;SCS_K_D_A_STAB_EQ;SCS_4M8_13_IS_SCS]
THEN EXISTS_TAC`1`
THEN EXISTS_TAC`3`
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_13_13]
THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
THEN REPEAT RESA_TAC;

REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC scs_inj
THEN ASM_SIMP_TAC[SCS_3T7_BASIC;SCS_4M8_13_BASIC;J_SCS_4M8_13;BASIC_HALF_SLICE_STAB;J_SCS_3T7;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T7_BASIC;J_SCS_3T7_1;BASIC_HALF_SLICE;D_HALF_SLICE1;Cqaoqlr.BASIC_OPP;SCS_3T7_IS_SCS]
THEN STRIP_TAC;

ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_13;scs_opp_v39]
THEN ARITH_TAC;

STRIP_TAC
THEN 
ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_13;scs_opp_v39;peropp2;
ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;peropp2;]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;

ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_13;scs_opp_v39]
THEN ARITH_TAC;

STRIP_TAC
THEN 
ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_13;peropp2;scs_opp_v39;
ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN SCS_TAC
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;peropp2]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN SCS_TAC;

REWRITE_TAC[scs_opp_v39]
THEN SCS_TAC
THEN REAL_ARITH_TAC;

REWRITE_TAC[scs_opp_v39]
THEN SCS_TAC
THEN REAL_ARITH_TAC;

REWRITE_TAC[scs_opp_v39]
THEN SCS_TAC
THEN REAL_ARITH_TAC;

REWRITE_TAC[scs_opp_v39]
THEN SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[J_SCS_3T7];
]);;




let SCS_4M8_13_ARROW_3T7=
prove(`scs_arrow_v39 {scs_4M8_13 } {scs_3T7 }`,

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_prop_equ_v39  scs_3T7 1}`
THEN ASM_REWRITE_TAC[SCS_4M8_13_SLICE_13]
THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T7`;`1`;`3`][SCS_3T7_IS_SCS;K_SCS_3T7;ARITH_RULE`(3 - 1 MOD 3)=2`]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T7 1`;`2`][PROP_EQU_IS_SCS;SCS_3T7_IS_SCS]
THEN DICH_TAC 0
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN REWRITE_TAC[]);;
let K_SCS_OPP_3T7=
prove(`scs_k_v39 (scs_opp_v39 scs_3T7) = 3`,

ASM_REWRITE_TAC[scs_opp_v39;scs_prop_equ_v39]
THEN SCS_TAC);;
let SCS_3T7_OPP_IS_SCS=
prove(`is_scs_v39 (scs_opp_v39 scs_3T7)`,

MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
THEN EXISTS_TAC`scs_opp_v39 scs_3T7`
THEN ASM_REWRITE_TAC[SCS_3T7_IS_SCS]);;


let SCS_4M8_13_ARROW_3T7_OPP=
prove(`scs_arrow_v39 {scs_4M8_02 } {scs_opp_v39 scs_3T7}`,

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_prop_equ_v39 
( scs_opp_v39 scs_3T7) 2}`
THEN ASM_REWRITE_TAC[SCS_4M8_02_SLICE_02]
THEN MRESAS_TAC PRO_EQU_ID1[`scs_opp_v39 scs_3T7`;`2`;`3`][SCS_3T7_IS_SCS;K_SCS_3T7;ARITH_RULE`(3 - 2 MOD 3)=1`;K_SCS_OPP_3T7;SCS_3T7_OPP_IS_SCS]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 (scs_opp_v39 scs_3T7) 2`;`1`][PROP_EQU_IS_SCS;SCS_3T7_IS_SCS;K_SCS_OPP_3T7;SCS_3T7_OPP_IS_SCS]
THEN DICH_TAC 0
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN REWRITE_TAC[]
THEN STRIP_TAC
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_opp_v39 scs_3T7}`
THEN ASM_REWRITE_TAC[]
THEN ASSUME_TAC SCS_3T7_IS_SCS
THEN MRESA_TAC Yxionxl2.SCS_OPP_REFL[`scs_3T7`]
THEN MRESAS_TAC  YXIONXL2[`3`;`scs_opp_v39 scs_3T7`][K_SCS_OPP_3T7;SCS_3T7_OPP_IS_SCS;ARITH_RULE`~(4<=3)`]);;


let PROP_OPP_4M8_13= 
prove_by_refinement(
`scs_4M8_13= scs_prop_equ_v39(scs_opp_v39 (scs_4M8_02)) 2 `,

[REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;SCS_K_D_A_STAB_EQ;scs_opp_v39;scs_4M8_13;scs_4M8_02]
THEN MATCH_MP_TAC scs_inj
THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M8_BASIC;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_13;scs_basic;unadorned_v39;peropp;peropp2]
THEN SCS_TAC
THEN STRIP_TAC;

SET_TAC[];

STRIP_TAC
THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;]
THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
THEN REPEAT GEN_TAC
THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
THEN SYM_ASSUM_TAC
THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
THEN SYM_ASSUM_TAC
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/ x' MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_4_TAC;PSORT_5_EXPLICIT;ARITH_RULE`4-1=3/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6
/\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;



let SCS_4M8_02_ARROW_4M8_13=
prove(
`scs_arrow_v39 {scs_4M8_02}{scs_4M8_13}`,

ASM_SIMP_TAC[PROP_OPP_4M8_13]
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_opp_v39 (scs_4M8_02)}`
THEN STRIP_TAC
THENL[
MATCH_MP_TAC (GEN_ALL YXIONXL2)
THEN EXISTS_TAC`4`
THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M8_02;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02;SCS_4M8_02_IS_SCS];

MATCH_MP_TAC(GEN_ALL YXIONXL3)
THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
THEN EXISTS_TAC`scs_opp_v39 ( scs_4M8_02)`
THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M8;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02;SCS_4M8_02_IS_SCS];]);;


let SCS_4M8_02_ARROW_3T7 =
prove(`scs_arrow_v39 { scs_4M8_02 } { scs_3T7 }`,

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_4M8_13}`
THEN ASM_SIMP_TAC[SCS_4M8_02_ARROW_4M8_13;SCS_4M8_13_ARROW_3T7]);;

(************************************)

let MIQMCSN=
prove(`main_nonlinear_terminal_v11
==> scs_arrow_v39 { scs_4M8 } ({scs_4M6',scs_3T7,scs_3T4})`,

STRIP_TAC
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`({scs_4M6',scs_opp_v39 scs_4M6', scs_4M8_02,scs_4M8_13} UNION {scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j})`
THEN ASM_SIMP_TAC[SCS_4M8_ARROW_STEP_ONE;SET_RULE`{scs_4M6', scs_3T7, scs_3T4}={scs_4M6', scs_3T7}UNION{ scs_3T4}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_REWRITE_TAC[SET_STAB_4M8_ARROW_3T4;]
THEN ONCE_REWRITE_TAC[SET_RULE`{scs_4M6', scs_3T7}={scs_4M6',scs_4M6', scs_3T7,scs_3T7}`]
THEN ASM_REWRITE_TAC[SET_RULE` {A,B,C,D}=({A,B,C}) UNION {D}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_REWRITE_TAC[SCS_4M8_13_ARROW_3T7;SET_RULE` {A,B,D}=({A,B}) UNION {D}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_REWRITE_TAC[SCS_4M8_02_ARROW_3T7;SET_RULE` {A,D}=({A}) UNION {D}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC
THENL[
MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS];

ASSUME_TAC(SCS_4M6_IS_SCS)
THEN ASSUME_TAC K_SCS_OPP_4M6
THEN ASSUME_TAC SCS_4M6_OPP_IS_SCS
THEN MRESA_TAC Yxionxl2.SCS_OPP_REFL[`scs_4M6'`]
THEN MRESAL_TAC YXIONXL2[`4`;`scs_opp_v39 scs_4M6'`][ARITH_RULE`~(4<=3)`]]);;

 end;;


(*
let check_completeness_claimA_concl = 
  Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) 
*)