HOL html


(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Local Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2012-04-01                                                           *)
(* ========================================================================= *)


(*
remaining conclusions from appendix to Local Fan chapter
*)


module Hexagons = 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;;




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 4 (3,4)= (0,3)/\ 
psort 3 (2,0)= (0,2)/\
psort 3 (2,1)= (1,2)/\
psort 3 (1,0)= (0,1)`,
REWRITE_TAC[psort;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_4_TAC;LET_DEF;LET_END_DEF;MOD_5_EXPLICIT;ARITH_RULE`0<=a/\ ~(1<= 0)/\ ~(2<=0)/\ ~(3<=0)/\ ~(4<=0)/\a<=a/\ ~(2<=1)/\ ~(3<=2)/\ ~(4<=3)/\ ~(3<=1)/\ ~(4<=1)/\ ~(4<=2)/\ 2<=3`]);;

let scs_5M3 = new_definition`scs_5M3 = mk_unadorned_v39 5 (#0.616) 
    (funlist_v39 [(0,1),(&2*h0);(0,2),(cstab);(0,3),(cstab);(1,3),(cstab);(1,4),(cstab);(2,4),(cstab)] (&2) 5)
    (funlist_v39 [(0,1),cstab;(0,2),(&6);  (0,3),(&6);   (1,3),(&6);   (1,4),(&6);   (2,4),(&6)] (&2*h0) 5)`;;

let SCS_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;
Terminal.FUNLIST_EXPLICIT;Yrtafyh.PSORT_PERIODIC;PSORT_5_EXPLICIT;
ARITH_RULE`SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6/\ SUC 6=7/\ SUC 7=8`];;



let sqrt8_LE_6=prove(`sqrt8<= &6`,
REWRITE_TAC[sqrt8]
THEN MATCH_MP_TAC REAL_LE_LSQRT
THEN REAL_ARITH_TAC);;
let sqrt8_LE_CSTAB=prove(`sqrt8<= #3.01`,
REWRITE_TAC[sqrt8]
THEN MATCH_MP_TAC REAL_LE_LSQRT
THEN REAL_ARITH_TAC);;

let LE_sqrt8_2=prove(`&2<=sqrt8`,
REWRITE_TAC[sqrt8]
THEN MATCH_MP_TAC REAL_LE_RSQRT
THEN REAL_ARITH_TAC);;
let LE_sqrt8_2h0=prove(`&2* #1.26<=sqrt8`,
REWRITE_TAC[sqrt8]
THEN MATCH_MP_TAC REAL_LE_RSQRT
THEN REAL_ARITH_TAC);;

let LT_sqrt8_2h0=prove(`&2* #1.26<sqrt8`,
REWRITE_TAC[sqrt8]
THEN MATCH_MP_TAC REAL_LT_RSQRT
THEN REAL_ARITH_TAC);;


(******is_scs*********)

let MOD_PERIODIC=prove(`~(k=0) ==> (i+k) MOD k = i MOD k/\ SUC (i+k) MOD k= SUC i MOD k`,
STRIP_TAC
THEN ONCE_REWRITE_TAC[ARITH_RULE`i+k= 1*k+i`;]
THEN SIMP_TAC[MOD_MULT_ADD;ARITH_RULE`SUC (1 * k + i) =(1 * k + SUC i)`]);;

let SCS_6I1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_6I1`,
[
REWRITE_TAC[scs_6I1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;]
THEN SIMP_TAC[ARITH_RULE`~(6=0)`;MOD_PERIODIC]
THEN REPEAT RESA_TAC
;

GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
THEN REWRITE_TAC[];

GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
THEN REWRITE_TAC[];

GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
THEN REWRITE_TAC[];

REAL_ARITH_TAC;

REWRITE_TAC[h0]
THEN REAL_ARITH_TAC;

REWRITE_TAC[h0]
THEN REAL_ARITH_TAC;

ASM_SIMP_TAC[ARITH_RULE`~(6=0)`;MOD_LT;h0]
THEN REAL_ARITH_TAC;

REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY]
THEN ARITH_TAC]);;
let DIST_LE_IMP_A_LE=prove(`BBs_v39 s v /\ dist(v i,v j) <= a
==> scs_a_v39 s i j<= a`,
REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39]
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC 2[`i`;`j`]
THEN DICH_TAC 1
THEN DICH_TAC 1
THEN REAL_ARITH_TAC);;


let SCS_3M1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_3M1`,
[SIMP_TAC[scs_3M1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.103 < #0.9`;periodic;SET_RULE`{} (i + j) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
THEN REPEAT RESA_TAC;

ARITH_TAC;

SCS_TAC;
SCS_TAC;
SCS_TAC;
SCS_TAC;
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];

SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

SCS_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[MOD_LT;h0]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
THEN REAL_ARITH_TAC;
SCS_TAC
THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
THEN REAL_ARITH_TAC;

MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
      (&2 * h0 < funlist_v39 [(0,1),cstab] (&2 * h0) 3 i (SUC i) \/
       &2 < funlist_v39 [(0,1),&2 * h0] (&2) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`]
THEN MATCH_DICH_TAC 0
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC]);;

let SCS_5M1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5M1`,
[
SIMP_TAC[scs_5M1;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<=5/\ 5<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.616 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
THEN REPEAT RESA_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];
SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;
SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;
SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
THEN REAL_ARITH_TAC;
POP_ASSUM MP_TAC
THEN ARITH_TAC;
SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN REAL_ARITH_TAC;
SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`]
THEN SUBGOAL_THEN`{i | i < 5 /\
      (&2 * #1.26 < (if psort 5 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/
       &2 < (if psort 5 (i,SUC i) = 0,1 then &2 * #1.26 else &2))} ={0}`ASSUME_TAC;

REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `];

ASM_REWRITE_TAC[Geomdetail.CARD_SING]
THEN ARITH_TAC]);;

let SCS_5I1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5I1`,
[
REWRITE_TAC[scs_5I1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(5=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=5/\ 5<=6/\a<=a/\ ~(5=4)/\ ~(6=0)`;d_tame;REAL_ARITH`#0.4819 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
THEN REPEAT RESA_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
THEN REWRITE_TAC[];

SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
THEN REWRITE_TAC[];

SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
THEN REWRITE_TAC[];

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
THEN REAL_ARITH_TAC;

ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY]
THEN ARITH_TAC]);;

let SCS_5I2_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5I2`,
[
REWRITE_TAC[scs_5I2;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(5=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=5/\ 5<=6/\a<=a/\ ~(5=4)/\ ~(6=0)`;d_tame;REAL_ARITH`#0.616 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
THEN REPEAT RESA_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
THEN REWRITE_TAC[];

SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
THEN REWRITE_TAC[];

SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
THEN REWRITE_TAC[];

SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`]
THEN MP_TAC(SET_RULE`(j MOD 5 = SUC i MOD 5 \/ SUC j MOD 5 = i MOD 5)\/ ~(j MOD 5 = SUC i MOD 5 \/ SUC j MOD 5 = i MOD 5)`)
THEN RESA_TAC
THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`];


SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
THEN MP_TAC(SET_RULE`(j = SUC i MOD 5 \/ SUC j MOD 5 = i )\/ ~(j = SUC i MOD 5 \/ SUC j MOD 5 = i)`)
THEN RESA_TAC
THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2];

SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
THEN REAL_ARITH_TAC;

ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY]
THEN ARITH_TAC]);;


let SCS_5I3_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5I3`,
[
REWRITE_TAC[scs_5I3;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(5=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=5/\ 5<=6/\a<=a/\ ~(5=4)/\ ~(6=0)`;d_tame;REAL_ARITH`#0.616 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
THEN REPEAT RESA_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];

SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN MRESA_TAC Terminal.psort_sym[`5`;`i`;`j`];

SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN MRESA_TAC Terminal.psort_sym[`5`;`i`;`j`];

SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN MRESA_TAC Terminal.psort_sym[`5`;`i`;`j`];

SCS_TAC
THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`]
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2h0]
THEN MP_TAC(SET_RULE`psort 5 (i,j) = 0,1\/ ~(psort 5 (i,j) = 0,1)`)
THEN RESA_TAC
THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2h0]
THEN REAL_ARITH_TAC;

SCS_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2h0;MOD_LT]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2h0;MOD_LT]
THEN MP_TAC(SET_RULE`i MOD 5 = SUC i MOD 5\/ ~(i MOD 5 = SUC i MOD 5)`)
THEN RESA_TAC
THEN REWRITE_TAC[REAL_ARITH`&0 <= #3.01`]
THEN MP_TAC(SET_RULE`psort 5 (i,SUC i) = 0,1\/ ~(psort 5 (i,SUC i) = 0,1)`)
THEN RESA_TAC
THEN REWRITE_TAC[sqrt8_LE_CSTAB]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN REAL_ARITH_TAC;


SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`]
THEN SUBGOAL_THEN`{i | i < 5 /\
      (&2 * #1.26 < (if psort 5 (i,SUC i) = 0,1 then sqrt8 else &2 * #1.26) \/
       &2 < (if psort 5 (i,SUC i) = 0,1 then &2 * #1.26 else &2))}
={0}`ASSUME_TAC;


REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;LT_sqrt8_2h0];

ASM_REWRITE_TAC[Geomdetail.CARD_SING]
THEN ARITH_TAC]);;

let SCS_5M2_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5M2`,
[
SIMP_TAC[scs_5M2;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<=5/\ 5<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.616 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
THEN REPEAT RESA_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];

SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];

SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN ARITH_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`]
THEN SUBGOAL_THEN`{i | i < 5 /\
      (&2 * #1.26 < (if psort 5 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/
       &2 < (if psort 5 (i,SUC i) = 0,1 then &2 else &2))} ={0}`ASSUME_TAC;

REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `];


ASM_REWRITE_TAC[Geomdetail.CARD_SING]
THEN ARITH_TAC]);;



let SCS_4M2_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M2`,
[
SIMP_TAC[scs_4M2;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.3789 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
THEN REPEAT RESA_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];

SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];

SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];


SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];


SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN ARITH_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
THEN REAL_ARITH_TAC;


SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
THEN SUBGOAL_THEN`{i | i < 4 /\
      (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/
       &2 < (if psort 4 (i,SUC i) = 0,1 then &2 * #1.26 else &2))} ={0}`ASSUME_TAC;


REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT];

ASM_REWRITE_TAC[Geomdetail.CARD_SING]
THEN ARITH_TAC;]);;


let SCS_6M1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_6M1`,
[
REWRITE_TAC[scs_6M1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;]
THEN SIMP_TAC[ARITH_RULE`~(6=0)`;MOD_PERIODIC]
THEN REPEAT RESA_TAC;

GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
THEN REWRITE_TAC[];

GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
THEN REWRITE_TAC[];

GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
THEN REWRITE_TAC[];

REAL_ARITH_TAC;

REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

ASM_SIMP_TAC[ARITH_RULE`~(6=0)`;MOD_LT;h0;cstab]
THEN REAL_ARITH_TAC;

REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY]
THEN ARITH_TAC]);;

let SCS_6T1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_6T1`,
[
REWRITE_TAC[scs_6T1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;]
THEN REWRITE_TAC[
ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;]
THEN SIMP_TAC[periodic;SET_RULE`{} (i + 6) <=> {} i`
;periodic2;ARITH_RULE`~(6=0)`;MOD_PERIODIC]
THEN REPEAT RESA_TAC;

GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
THEN REWRITE_TAC[];

GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
THEN REWRITE_TAC[];


GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
THEN REWRITE_TAC[];


REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;


ASM_SIMP_TAC[h0;cstab;MOD_LT]
THEN REAL_ARITH_TAC;


ASM_SIMP_TAC[h0;cstab;MOD_LT]
THEN REAL_ARITH_TAC;


ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN REWRITE_TAC[REAL_ARITH`~(a<a)/\ ~(&2 * #1.26 < &2)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;h0]
THEN ARITH_TAC]);;




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

let SCS_6I1_BASIC=prove(`scs_basic_v39 scs_6I1`,
SCS_TAC);;
let SCS_6T1_BASIC=prove(`scs_basic_v39 scs_6T1`,
SCS_TAC);;
let SCS_6M1_BASIC=prove(`scs_basic_v39 scs_6M1`,
SCS_TAC);;

let SCS_3M1_BASIC=prove(`scs_basic_v39 scs_3M1`,
SCS_TAC);;

let SCS_3T1_BASIC=prove(`scs_basic_v39 scs_3T1`,
SCS_TAC);;
let SCS_3T4_BASIC=prove(`scs_basic_v39 scs_3T4`,
SCS_TAC);;

let SCS_5M1_BASIC=prove(`scs_basic_v39 scs_5M1`,
SCS_TAC);;
let SCS_5M2_BASIC=prove(`scs_basic_v39 scs_5M2`,
SCS_TAC);;


let SCS_5I1_BASIC=prove(`scs_basic_v39 scs_5I1`,
SCS_TAC);;
let SCS_5I2_BASIC=prove(`scs_basic_v39 scs_5I2`,
SCS_TAC);;
let SCS_5I3_BASIC=prove(`scs_basic_v39 scs_5I3`,
SCS_TAC);;
let SCS_4M2_BASIC=prove(`scs_basic_v39 scs_4M2`,
SCS_TAC);;

let SCS_4M6_BASIC=prove(`scs_basic_v39 scs_4M6'`,
SCS_TAC);;

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

let K_SCS_6I1=prove(`scs_k_v39 scs_6I1=6`,
SCS_TAC);;
let K_SCS_6T1=prove(`scs_k_v39 scs_6T1=6`,
SCS_TAC);;

let K_SCS_3M1=prove(`scs_k_v39 scs_3M1=3`,
SCS_TAC);;
let K_SCS_3T1=prove(`scs_k_v39 scs_3T1=3`,
SCS_TAC);;
let K_SCS_3T4=prove(`scs_k_v39 scs_3T4=3`,
SCS_TAC);;

let K_SCS_5M1=prove(`scs_k_v39 scs_5M1=5`,
SCS_TAC);;
let K_SCS_5M2=prove(`scs_k_v39 scs_5M2=5`,
SCS_TAC);;
let K_SCS_5I1=prove(`scs_k_v39 scs_5I1=5`,
SCS_TAC);;

let K_SCS_5I2=prove(`scs_k_v39 scs_5I2=5`,
SCS_TAC);;

let K_SCS_5I3=prove(`scs_k_v39 scs_5I3=5`,
SCS_TAC);;



let K_SCS_4M2=prove(`scs_k_v39 scs_4M2=4`,
SCS_TAC);;
let K_SCS_4M6=prove(`scs_k_v39 scs_4M6'=4`,
SCS_TAC);;

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

let J_SCS_3M1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3M1 i) i1
 j= F`,
SCS_TAC);;
let J_SCS_3T4=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T4 i) i1
 j= F`,
SCS_TAC);;

let J_SCS_5M1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5M1 i) i1 j= F`,
SCS_TAC );;
let J_SCS_5I1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5I1 i) i1 j= F`,
SCS_TAC );;
let J_SCS_5I2=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5I2 i) i1 j= F`,
SCS_TAC );;
let J_SCS_5I3=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5I3 i) i1 j= F`,
SCS_TAC );;

let J_SCS_4M2=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M2 i) i1 j= F`,
SCS_TAC );;
let J_SCS_4M6=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M6' i) i1 j= F`,
SCS_TAC );;

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


let BASIC_MM_EQ_BBPRIME2=prove(`scs_basic_v39 s ==> MMs_v39 s = BBprime2_v39 s `,
SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;MMs_v39;Ayqjtmd.unadorned_MMs]);;

let BASIC_MM_EQ_BBPRIME2_POINT=prove(`scs_basic_v39 s ==> MMs_v39 s v= BBprime2_v39 s v`,
SIMP_TAC [BASIC_MM_EQ_BBPRIME2]);;

let DIST_PSORT=prove(`periodic v (k)/\ ~(k=0) /\ psort (k) (i,j) = psort (k) (i',j')
==>  dist (v i',v j')=  dist (v i,v j)`,
REWRITE_TAC[psort;LET_DEF;LET_END_DEF;]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`i MOD k<= j MOD k\/ ~(i MOD k<= j MOD k)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`i' MOD k<= j' MOD k\/ ~(i' MOD k<= j' MOD k)`)
THEN RESA_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k`;`v`][ARITH_RULE`~(4=0)`;periodic]
THEN THAYTHEL_ASM_TAC 0[`i`][]
THEN THAYTHEL_ASM_TAC 0[`i'`][]
THEN THAYTHEL_ASM_TAC 0[`j`][]
THEN THAYTHEL_ASM_TAC 0[`j'`][]
THEN SIMP_TAC[DIST_SYM]);;

let STAB_BB=prove(`is_scs_v39 s/\  dist(v i,v j) <= cstab/\
BBs_v39 s v
==> 
BBs_v39 (scs_stab_diag_v39 s i j) v`,
SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39]
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC 1[`i'`;`j'`]
THEN DICH_TAC 0
THEN DICH_TAC 4
THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j')\/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
THEN RESA_TAC
THEN MP_TAC Wkeidft.PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN ABBREV_TAC`k= scs_k_v39 s`
THEN MRESA_TAC DIST_PSORT[`k`;`i'`;`j'`;`i`;`v`;`j`]
THEN RESA_TAC);;

let SCS_K_D_A_STAB_EQ=prove(`scs_d_v39 (scs_stab_diag_v39 s i j) =scs_d_v39 s
/\ scs_k_v39 (scs_stab_diag_v39 s i j) =scs_k_v39 s
/\(!i' j'. scs_a_v39 (scs_stab_diag_v39 s i j) i' j'= scs_a_v39 s i' j')`,
SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39]);;

let DIAG_SCS_M_EQ=prove(`is_scs_v39 s/\ scs_diag (scs_k_v39 s) i j==> scs_M s = scs_M (scs_stab_diag_v39 s i j)`,
SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;]
THEN STRIP_TAC
THEN MP_TAC Wkeidft.PROPERTY_OF_K_SCS
THEN RESA_TAC
THEN ASM_SIMP_TAC[Yrtafyh.DIAG_NOT_PSORT]);;

let DIAD_PSORT_IMP_DIAD=prove_by_refinement(`scs_diag k i j /\ ~(k=0)
/\ psort k (i',j') = psort k (i,j)
==> scs_diag k i' j'`,
[REWRITE_TAC[scs_diag;psort;LET_DEF;LET_END_DEF]
THEN STRIP_TAC
THEN DICH_TAC 0
THEN MP_TAC(SET_RULE`i MOD k<= j MOD k\/ ~(i MOD k<= j MOD k)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`i' MOD k<= j' MOD k\/ ~(i' MOD k<= j' MOD k)`)
THEN RESA_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN RESA_TAC;

MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`i`;`k`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`j`;`k`] ;

MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`j`;`k`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`i`;`k`] ;


MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`j`;`k`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`i`;`k`] ;

MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`i`;`k`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`j`;`k`] ]);;
let PEDSLGV1= prove( `!v i j. 
    v IN MMs_v39 scs_6I1 /\
    scs_diag 6 i j /\
    dist(v i,v j) <= cstab ==>
    v IN MMs_v39 (scs_stab_diag_v39 scs_6I1 i j)`,
REWRITE_TAC[IN]
THEN REPEAT STRIP_TAC
THEN MP_TAC SCS_6I1_IS_SCS
THEN STRIP_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6I1`;`v`]
THEN MRESA_TAC DIST_LE_IMP_A_LE[`v`;`scs_6I1`;`i`;`j`;`cstab`]
THEN ASSUME_TAC SCS_6I1_BASIC
THEN ASSUME_TAC K_SCS_6I1
THEN MRESAL_TAC Yrtafyh.YRTAFYH[`scs_6I1`;`i`;`j`][ARITH_RULE`3<6`;]
THEN MP_TAC  Ppbtydq.MXQTIED
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MATCH_DICH_TAC 0
THEN EXISTS_TAC`scs_6I1`
THEN ASM_SIMP_TAC[STAB_BB;SCS_K_D_A_STAB_EQ;DIAG_SCS_M_EQ;REAL_ARITH`a<=a`]
THEN REPEAT GEN_TAC
THEN REWRITE_TAC[scs_stab_diag_v39;scs_6I1;scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;CS_ADJ]
THEN MP_TAC(SET_RULE`psort 6 (i,j) = psort 6 (i',j')\/ ~(psort 6 (i,j) = psort 6 (i',j'))`)
THEN RESA_TAC
THENL[
MRESAL_TAC DIAD_PSORT_IMP_DIAD[`i`;`j`;`6`;`i'`;`j'`][ARITH_RULE`~(6=0)`]
THEN DICH_TAC 0
THEN REWRITE_TAC[scs_diag;cstab]
THEN RESA_TAC 
THEN REAL_ARITH_TAC;
REAL_ARITH_TAC]);;

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




let K_SCS_6M1=prove(`scs_k_v39 scs_6M1=6/\ scs_d_v39 scs_6M1 = scs_d_v39 scs_6I1`,
REWRITE_TAC[scs_6I1;scs_6M1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39]);;

let D_6M1_EQ_6I1=prove(` scs_d_v39 scs_6M1 = scs_d_v39 scs_6I1
`,
REWRITE_TAC[scs_6I1;scs_6M1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39]);;

let A_6M1_EQ_6I1_EDGE=prove(`(!i j. scs_a_v39 scs_6M1 i (SUC i) = scs_a_v39 scs_6I1 i (SUC i))`,
REWRITE_TAC[scs_6I1;scs_6M1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39]);;
let SCS_M_6I1_EQ_6M1=prove(`scs_M scs_6I1 = scs_M scs_6M1`,
REWRITE_TAC[scs_6I1;scs_6M1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39;scs_M]);;


let BB_6I1_IS_BB_6M1=prove_by_refinement(`BBs_v39 scs_6I1 v/\ (!i j. scs_diag 6 i j ==>   cstab <= dist(v i,v j)) ==> BBs_v39 scs_6M1 v`,
[
SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_6I1;scs_6M1;CS_ADJ;scs_diag]
THEN REPEAT RESA_TAC
THEN MP_TAC(SET_RULE`i MOD 6= j MOD 6\/ ~(i MOD 6= j MOD 6)`)
THEN RESA_TAC;

THAYTHE_TAC (5-2)[`i`;`j`];

MP_TAC(SET_RULE`SUC i MOD 6= j MOD 6\/ ~(SUC i MOD 6= j MOD 6)`)
THEN RESA_TAC;

THAYTHE_TAC (6-2)[`i`;`j`];

MP_TAC(SET_RULE`i MOD 6= SUC j MOD 6\/ ~(i MOD 6= SUC j MOD 6)`)
THEN RESA_TAC;

THAYTHE_TAC (7-2)[`i`;`j`];

THAYTHE_TAC (7-4)[`i`;`j`];

THAYTHE_TAC (5-2)[`i`;`j`];

MP_TAC(SET_RULE`SUC i MOD 6= j MOD 6\/ ~(SUC i MOD 6= j MOD 6)`)
THEN RESA_TAC;

THAYTHE_TAC (6-2)[`i`;`j`];

MP_TAC(SET_RULE`i MOD 6= SUC j MOD 6\/ ~(i MOD 6= SUC j MOD 6)`)
THEN RESA_TAC;

THAYTHE_TAC (7-2)[`i`;`j`];

THAYTHE_TAC (7-4)[`i`;`j`]]);;  
let A_6I1_LE_A_6M1=prove(`scs_a_v39 scs_6I1 i j <= scs_a_v39 scs_6M1 i j`,
REWRITE_TAC[scs_6I1;scs_6M1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39;h0;cstab]
THEN REAL_ARITH_TAC);;
let B_6I1_LE_B_6M1=prove(`scs_b_v39 scs_6M1 i j = scs_b_v39 scs_6I1 i j`,
REWRITE_TAC[scs_6I1;scs_6M1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39;h0;cstab]
THEN REAL_ARITH_TAC);;


  let PEDSLGV2= prove(`!v. 
    v IN MMs_v39 scs_6I1 /\
    (!i j. scs_diag 6 i j ==>   cstab <= dist(v i,v j)) ==>
    v IN MMs_v39 (scs_6M1)`,
REWRITE_TAC[IN]
THEN REPEAT STRIP_TAC
THEN MP_TAC SCS_6I1_IS_SCS
THEN STRIP_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6I1`;`v`]
THEN ASSUME_TAC SCS_6I1_BASIC
THEN ASSUME_TAC K_SCS_6I1
THEN ASSUME_TAC SCS_6M1_BASIC
THEN ASSUME_TAC K_SCS_6M1
THEN MP_TAC SCS_6M1_IS_SCS
THEN STRIP_TAC
THEN MP_TAC  Ppbtydq.MXQTIED
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MATCH_DICH_TAC 0
THEN EXISTS_TAC`scs_6I1`
THEN ASM_SIMP_TAC[D_6M1_EQ_6I1;A_6M1_EQ_6I1_EDGE;SCS_M_6I1_EQ_6M1;BB_6I1_IS_BB_6M1;A_6I1_LE_A_6M1;B_6I1_LE_B_6M1;REAL_ARITH`a<=a`]);;




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


let STAB_6I1_SCS=prove(` scs_diag (scs_k_v39 scs_6I1) i j
==> is_scs_v39 (scs_stab_diag_v39 scs_6I1 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_6I1 i j)`,
STRIP_TAC
THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_6I1_IS_SCS;SCS_6I1_BASIC;K_SCS_6I1;
ARITH_RULE`3<6`;LET_DEF;LET_END_DEF;scs_6I1;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
THEN REAL_ARITH_TAC);;


let SCS_DIAG_SCS_6I1_02=prove(`scs_diag (scs_k_v39 scs_6I1) 0 2`,
REWRITE_TAC[K_SCS_6I1;scs_diag]
THEN ARITH_TAC);;

let SCS_DIAG_SCS_6I1_03=prove(`scs_diag (scs_k_v39 scs_6I1) 0 3`,
REWRITE_TAC[K_SCS_6I1;scs_diag]
THEN ARITH_TAC);;


let BASIC_HALF_SLICE_STAB=prove(`scs_basic_v39 s 
==> scs_basic_v39 (scs_half_slice_v39 (scs_stab_diag_v39 s i j) 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_SLICE=prove(`scs_d_v39 (scs_half_slice_v39 (scs_stab_diag_v39 s i j) p q d' mkj)=d'`,
SCS_TAC);;
let BAISC_PROP_EQU=prove(`scs_basic_v39 s ==> scs_basic_v39 (scs_prop_equ_v39 s i)`,
SCS_TAC
THEN SET_TAC[]);;
let K_SCS_PROP_EUQ=prove(`scs_k_v39 (scs_prop_equ_v39 s i)= scs_k_v39 s`,
SCS_TAC);;





let AQICLXA_SLICE=prove_by_refinement(`scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 2 } { scs_prop_equ_v39 scs_3M1 1, scs_prop_equ_v39 scs_5M1 1}`,
[MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_6I1_02;STAB_6I1_SCS;SCS_K_D_A_STAB_EQ;]
THEN EXISTS_TAC`0`
THEN EXISTS_TAC`2`
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_6I1_02]
THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
THEN REPEAT RESA_TAC;

REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC scs_inj
THEN ASM_SIMP_TAC[SCS_3M1_BASIC;SCS_5M1_BASIC;SCS_6I1_BASIC;J_SCS_5M1;BASIC_HALF_SLICE_STAB;J_SCS_3M1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ]
THEN STRIP_TAC;

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;scs_stab_diag_v39;K_SCS_3M1]
THEN ARITH_TAC;

STRIP_TAC;

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;scs_stab_diag_v39;K_SCS_3M1;scs_6I1;scs_3M1;
ARITH_RULE`(2 + 1 + 6 - 0) MOD 6= 3/\ 0 MOD 6=0/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort]
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_3_TAC;DIVISION;]
THEN RESA_TAC
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;Uxckfpe.ARITH_3_TAC]
THEN SIMP_TAC[ARITH_RULE`~(0=2)/\ ~(0=1)/\ 0<=1/\ ~(1=2)`;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]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][Uxckfpe.ARITH_3_TAC]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][Uxckfpe.ARITH_3_TAC]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][Uxckfpe.ARITH_3_TAC]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][Uxckfpe.ARITH_3_TAC]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][Uxckfpe.ARITH_3_TAC]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][Uxckfpe.ARITH_3_TAC]
THEN ASM_SIMP_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2`;PAIR_EQ;Uxckfpe.ARITH_3_TAC];


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;scs_stab_diag_v39;K_SCS_3M1;scs_6I1;scs_3M1;
ARITH_RULE`(2 + 1 + 6 - 0) MOD 6= 3/\ 0 MOD 6=0/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort]
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_3_TAC;DIVISION;]
THEN RESA_TAC
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;Uxckfpe.ARITH_3_TAC]
THEN SIMP_TAC[ARITH_RULE`~(0=2)/\ ~(0=1)/\ 0<=1/\ ~(1=2)/\ 0<=2/\ 0<=0`;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]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][Uxckfpe.ARITH_3_TAC]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][Uxckfpe.ARITH_3_TAC]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][Uxckfpe.ARITH_3_TAC]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][Uxckfpe.ARITH_3_TAC]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][Uxckfpe.ARITH_3_TAC]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][Uxckfpe.ARITH_3_TAC]
THEN ASM_SIMP_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2`;PAIR_EQ;Uxckfpe.ARITH_3_TAC];



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;scs_stab_diag_v39;K_SCS_3M1]
THEN ARITH_TAC;

STRIP_TAC
THEN ASM_REWRITE_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;scs_stab_diag_v39;K_SCS_3M1;scs_6I1;scs_3M1;
ARITH_RULE`(0 + 1 + 6 - 2) MOD 6= 5/\ 2 MOD 6=2/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort]
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 5<5==> x MOD 5=0\/ x MOD 5=1\/ x MOD 5=2\/ x MOD 5=3\/ x MOD 5=4`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_5_TAC;DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 5<5==> x' MOD 5=0\/ x' MOD 5=1\/ x' MOD 5=2\/ x' MOD 5=3\/ x' MOD 5=4`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_5_TAC;DIVISION;ARITH_RULE`5-1=4`]
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_5_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`0`;`1`][ARITH_RULE`~(5=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`1`;`1`][ARITH_RULE`~(5=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`2`;`1`][ARITH_RULE`~(5=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`3`;`1`][ARITH_RULE`~(5=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`4`;`1`][ARITH_RULE`~(5=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`0`;`1`][ARITH_RULE`~(5=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`1`;`1`][ARITH_RULE`~(5=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`2`;`1`][ARITH_RULE`~(5=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`3`;`1`][ARITH_RULE`~(5=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`4`;`1`][ARITH_RULE`~(5=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_5_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_5_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)
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC];

SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[J_SCS_3M1]]);;


let FZIOTEF_UNION = prove_by_refinement(
    `!S1 S2 S3 S4.  scs_arrow_v39 S1 S2 /\ scs_arrow_v39 S3 S4 ==>
      scs_arrow_v39 (S1 UNION S3) (S2 UNION S4)`,
    (* {{{ proof *)
    [
      REWRITE_TAC[scs_arrow_v39;UNION;IN_ELIM_THM];
      REPEAT WEAKER_STRIP_TAC;
      ASM_REWRITE_TAC[];
      BY(ASM_MESON_TAC[])
    ]);;  (* }}} *)

let  PROP_EQU_IS_SCS=prove(`is_scs_v39 s ==> is_scs_v39 (scs_prop_equ_v39 s i)`,
MRESA_TAC PROP_EQU_IS_SCS[`scs_k_v39 s`;`s`;`i`;`scs_prop_equ_v39 s i`]);;

let AQICLXA=prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 2 } { scs_3M1, scs_5M1 }`,
MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_3M1 1, scs_prop_equ_v39 scs_5M1 1}`
THEN ASM_SIMP_TAC[AQICLXA_SLICE]
THEN REWRITE_TAC[SET_RULE`{a,b}= {a}UNION {b}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC
THENL[

MRESAS_TAC PRO_EQU_ID[`scs_3M1`;`3`;`2`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`3-2 MOD 3=1`]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1 1`;`2`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`3-1=2`]
THEN DICH_TAC 0
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);

MRESAS_TAC PRO_EQU_ID[`scs_5M1`;`5`;`4`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_5M1_IS_SCS;K_SCS_5M1;ARITH_RULE`5-4 MOD 5=1`]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_5M1 1`;`4`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_5M1_IS_SCS;K_SCS_5M1;ARITH_RULE`3-1=2`]
THEN DICH_TAC 0
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])]);;

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

let FUNOUYH_SLICE=prove_by_refinement(`scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 3 } { scs_prop_equ_v39 scs_4M2 1, scs_prop_equ_v39 scs_4M2 1}`,
[
MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_6I1_03;STAB_6I1_SCS;SCS_K_D_A_STAB_EQ;]
THEN EXISTS_TAC`0`
THEN EXISTS_TAC`3`
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_6I1_03]
THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
THEN REPEAT RESA_TAC;

REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC scs_inj
THEN ASM_SIMP_TAC[BAISC_PROP_EQU;K_SCS_PROP_EUQ;BASIC_HALF_SLICE_STAB;SCS_4M2_BASIC;J_SCS_4M2;D_HALF_SLICE;SCS_6I1_BASIC;K_SCS_4M2]
THEN STRIP_TAC;


ASM_SIMP_TAC[scs_half_slice_v39;scs_4M2;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;scs_stab_diag_v39;K_SCS_3M1]
THEN ARITH_TAC;


STRIP_TAC
THEN ASM_REWRITE_TAC[scs_half_slice_v39;scs_4M2;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;scs_stab_diag_v39;K_SCS_4M2;scs_6I1;scs_3M1;
ARITH_RULE`(3 + 1 + 6 - 0) MOD 6= 4/\ 0 MOD 6=0/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort]
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/ x' MOD 4=3`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2)
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC];



ASM_SIMP_TAC[scs_half_slice_v39;scs_4M2;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;scs_stab_diag_v39;K_SCS_3M1]
THEN ARITH_TAC;


STRIP_TAC
THEN ASM_REWRITE_TAC[scs_half_slice_v39;scs_4M2;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;scs_stab_diag_v39;K_SCS_4M2;scs_6I1;scs_3M1;
ARITH_RULE`(0 + 1 + 6 - 3) MOD 6= 4/\ 3 MOD 6=3/\ a+0=a`;scs_prop_equ_v39]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort]
THEN REPEAT GEN_TAC
THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/ x' MOD 4=3`)
THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
THEN ASM_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ 
b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
/\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
/\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2)
/\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\
3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_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;h0]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[cstab;h0]
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[J_SCS_4M2]]);;





let FZIOTEF=prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 3 } { scs_4M2}`,
MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_4M2 1, scs_prop_equ_v39 scs_4M2 1}`
THEN ASM_SIMP_TAC[FUNOUYH_SLICE]
THEN REWRITE_TAC[SET_RULE`{a,a}= {a}`]
THEN MRESAS_TAC PRO_EQU_ID[`scs_4M2`;`4`;`3`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_4M2_IS_SCS;K_SCS_4M2;ARITH_RULE`4-3 MOD 4=1`]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M2 1`;`3`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_4M2_IS_SCS;K_SCS_4M2;ARITH_RULE`3-1=2`]
THEN DICH_TAC 0
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]));;

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



let h0_LT_B_SCS_6M1=prove(`
(!i j. scs_diag 6 i j ==> &4 * h0 < scs_b_v39 scs_6M1 i j)
/\ (!i j. scs_diag 6 i j ==> scs_a_v39 scs_6M1 i j <= cstab)`,
SCS_TAC
THEN REWRITE_TAC[h0;scs_diag]
THEN REPEAT RESA_TAC
THEN REAL_ARITH_TAC);;


let h0_LT_B_SCS_6I1=prove(
`(!i j. scs_diag 6 i j ==> &4 * h0 < scs_b_v39 scs_6I1 i j)
/\ (!i j. scs_diag 6 i j ==> scs_a_v39 scs_6I1 i j <= cstab)`,
SCS_TAC
THEN REWRITE_TAC[h0;scs_diag;cstab]
THEN REPEAT RESA_TAC
THEN REAL_ARITH_TAC);;

let h0_LT_B_SCS_5I1=prove(`
(!i j. scs_diag 5 i j ==> &4 * h0 < scs_b_v39 scs_5I1 i j)
/\ (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5I1 i j <= cstab)`,
SCS_TAC
THEN REWRITE_TAC[h0;scs_diag;cstab]
THEN REPEAT RESA_TAC
THEN REAL_ARITH_TAC);;

let h0_LT_B_SCS_5I2=prove(`
(!i j. scs_diag 5 i j ==> &4 * h0 < scs_b_v39 scs_5I2 i j)
/\ (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5I2 i j <= cstab)`,
SCS_TAC
THEN REWRITE_TAC[h0;scs_diag;cstab]
THEN REPEAT RESA_TAC
THEN MP_TAC sqrt8_LE_CSTAB
THEN REAL_ARITH_TAC);;
let h0_LT_B_SCS_5M2=prove(`
 (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5M2 i j <= cstab)`,
SCS_TAC
THEN REWRITE_TAC[h0;scs_diag;cstab]
THEN REPEAT RESA_TAC
THEN REAL_ARITH_TAC);;
let h0_LT_B_SCS_5M1=prove(` (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5M1 i j <= cstab)`,
SCS_TAC
THEN REWRITE_TAC[h0;scs_diag;cstab]
THEN REPEAT RESA_TAC
THEN MP_TAC sqrt8_LE_CSTAB
THEN REAL_ARITH_TAC);;

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


let h0_EQ_B_SCS_6I1=prove(
`(!i j. scs_diag 6 i j ==> scs_b_v39 scs_6I1 i j= &6)
/\ (!i j. scs_diag 6 i j ==>  scs_a_v39 scs_6I1 i j= &2 *h0)`,
SCS_TAC
THEN REWRITE_TAC[h0;scs_diag;cstab]
THEN REPEAT RESA_TAC);;


let h0_EQ_B_SCS_5I1=prove(
`(!i j. scs_diag 5 i j ==> scs_b_v39 scs_5I1 i j= &6)
/\ (!i j. scs_diag 5 i j ==>  scs_a_v39 scs_5I1 i j= &2 *h0)`,
SCS_TAC
THEN REWRITE_TAC[h0;scs_diag;cstab]
THEN REPEAT RESA_TAC);;
let h0_EQ_B_SCS_5I2=prove(
`(!i j. scs_diag 5 i j ==> scs_b_v39 scs_5I2 i j= &6)
/\ (!i j. scs_diag 5 i j ==>  scs_a_v39 scs_5I2 i j= sqrt8)`,
SCS_TAC
THEN REWRITE_TAC[h0;scs_diag;cstab]
THEN REPEAT RESA_TAC);;





let B_LE_CSTAB_6M1=prove(`
(!i. scs_b_v39 scs_6M1 i (SUC i) <= cstab)/\ 
(!i. scs_b_v39 scs_6M1 i (SUC i) <= &2*h0)/\
 (!i. &2< scs_b_v39 scs_6M1 i (SUC i) )/\ 
(!i. scs_a_v39 scs_6M1 i (SUC i) = &2)`,
SCS_TAC
THEN SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;h0;cstab]
THEN REAL_ARITH_TAC);;

let B_LE_CSTAB_5I1=prove(`
(!i. scs_b_v39 scs_5I1 i (SUC i) <= cstab)/\
(!i. scs_b_v39 scs_5I1 i (SUC i) <= &2*h0)/\
 (!i. &2< scs_b_v39 scs_5I1 i (SUC i) )/\ 
(!i. scs_a_v39 scs_5I1 i (SUC i) = &2)
`,
SCS_TAC
THEN SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;h0;cstab]
THEN REAL_ARITH_TAC);;
(*********CARD scs_M <=1**************)

let CARD_SCS_M_6M1=prove(`CARD (scs_M scs_6M1) <= 1`,
ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
THEN SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
THEN ARITH_TAC);;
let SCS_M_6M1=prove(`(scs_M scs_6M1) ={}`,
ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
THEN SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
THEN ARITH_TAC);;


let SCS_M_6T1=prove(`(scs_M scs_6T1) ={}`,
ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
THEN SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)/\ ~(&2 * #1.26 < &2)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M;h0]
THEN ARITH_TAC);;
let CARD_SCS_M_5I1=prove(`CARD (scs_M scs_5I1) <= 1`,
ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
THEN SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
THEN ARITH_TAC);;

let SCS_M_5I1=prove(`scs_M scs_5I1 ={}`,
ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
THEN SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
THEN ARITH_TAC);;

let SCS_M_5M2=prove(`scs_M scs_5M2 ={0}`,
ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
THEN SCS_TAC
THEN ASM_SIMP_TAC[h0;cstab;]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`]
THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `];
);;

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


let SCS_6M1_IMP_SCS_6T1= prove_by_refinement(`main_nonlinear_terminal_v11
==>(!v. 
    v IN MMs_v39 scs_6M1 /\
    (!i j. scs_diag 6 i j ==>   cstab < dist(v i,v j)) ==>
    v IN MMs_v39 (scs_6T1))`,
[REWRITE_TAC[IN]
THEN REPEAT STRIP_TAC
THEN MP_TAC SCS_6M1_IS_SCS
THEN STRIP_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6M1`;`v`]
THEN ASSUME_TAC SCS_6M1_BASIC
THEN ASSUME_TAC K_SCS_6M1
THEN ASSUME_TAC SCS_6T1_BASIC
THEN ASSUME_TAC K_SCS_6T1
THEN ASSUME_TAC SCS_6T1_IS_SCS
THEN MP_TAC RRCWNSJ
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_6M1`;`v`][ARITH_RULE`3<6`;h0_LT_B_SCS_6M1;B_LE_CSTAB_6M1]
THEN MP_TAC Jcyfmrp.JCYFMRP
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_6M1`;`v`][ARITH_RULE`3<6`;h0_LT_B_SCS_6M1;B_LE_CSTAB_6M1;IN;CARD_SCS_M_6M1]
THEN MP_TAC Jlxfdmj.JLXFDMJ
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_6M1`;`v`;`i`][ARITH_RULE`3<6`;h0_LT_B_SCS_6M1;B_LE_CSTAB_6M1;IN;CARD_SCS_M_6M1;SCS_M_6M1;SET_RULE`(~{} a==> B)<=> B`;ARITH_RULE`i+1=SUC i`]
THEN MP_TAC  Ppbtydq.MXQTIED
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MATCH_DICH_TAC 0
THEN EXISTS_TAC`scs_6M1`
THEN ASM_SIMP_TAC[SCS_M_6M1;SCS_M_6T1]
THEN STRIP_TAC;

SCS_TAC;


STRIP_TAC;

DICH_TAC(12-4)
THEN ASM_SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;ARITH_RULE`~(6<=3)`]
THEN RESA_TAC;

REPEAT GEN_TAC
THEN THAYTHE_TAC 1[`i'`;`j`]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN SCS_TAC
THEN MP_TAC(SET_RULE`i' MOD 6= j MOD 6\/ ~(i' MOD 6= j MOD 6)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`SUC i' MOD 6= j MOD 6\/ ~(SUC i' MOD 6= j MOD 6)`)
THEN RESA_TAC;

MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6M1`;`v`]
THEN MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_6M1`;`j`;`v:num->real^3`;`SUC i':num`]
THEN REAL_ARITH_TAC;

MP_TAC(SET_RULE`i' MOD 6=SUC j MOD 6\/ ~( i' MOD 6=SUC j MOD 6)`)
THEN RESA_TAC;

MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6M1`;`v`]
THEN MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_6M1`;`i'`;`v:num->real^3`;`SUC j:num`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC;

STRIP_TAC;

SCS_TAC;

SCS_TAC
THEN REWRITE_TAC[h0;scs_diag]
THEN REAL_ARITH_TAC]);;
let SCS_6I1_IMP_SCS_6T1=prove(`main_nonlinear_terminal_v11
==>(!v. 
    v IN MMs_v39 scs_6I1 /\
    (!i j. scs_diag 6 i j ==>   cstab < dist(v i,v j)) ==>
    v IN MMs_v39 (scs_6T1))`,
REPEAT STRIP_TAC
THEN MP_TAC SCS_6M1_IMP_SCS_6T1
THEN RESA_TAC
THEN MATCH_DICH_TAC 0
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC PEDSLGV2
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN THAYTHE_TAC 1[`i`;`j`]
THEN DICH_TAC 0
THEN REAL_ARITH_TAC);;


let SCS_6I1_BERAK_BY_CSTAB= prove_by_refinement(`main_nonlinear_terminal_v11
==> 
scs_arrow_v39 { scs_6I1 } ({ scs_6T1}UNION { scs_stab_diag_v39 scs_6I1 i j| scs_diag 6 i j })`,
[REPEAT GEN_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;

REWRITE_TAC[SCS_6T1_IS_SCS];

MATCH_MP_TAC Yrtafyh.STAB_IS_SCS
THEN ASM_SIMP_TAC[SCS_6I1_IS_SCS;K_SCS_6I1;SCS_6I1_BASIC;ARITH_RULE`3<6`]
THEN SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

DISJ_CASES_TAC(SET_RULE`(!s. s = scs_6I1 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_6I1 ==> 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 6 i j ==>   cstab < dist(v i,v j))\/ ~((!i j. scs_diag 6 i j ==>   cstab < dist((v:num->real^3) i,v j)))`)
THEN RESA_TAC;

EXISTS_TAC`scs_6T1`
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`v:num->real^3`
THEN MP_TAC SCS_6I1_IMP_SCS_6T1
THEN REWRITE_TAC[IN]
THEN RESA_TAC
THEN MATCH_DICH_TAC 0
THEN ASM_REWRITE_TAC[];

POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
THEN STRIP_TAC
THEN MRESAL_TAC PEDSLGV1[`v`;`i`;`j`][IN]
THEN EXISTS_TAC`scs_stab_diag_v39 scs_6I1 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 PSORT_MOD=prove(`~(k=0)==> psort k (i MOD k,j MOD k)= psort k (i,j)`,
SIMP_TAC[psort;MOD_REFL]);;


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



let STAB_MOD=prove(`is_scs_v39 s
==>   scs_stab_diag_v39 s (i MOD (scs_k_v39 s)) (j MOD (scs_k_v39 s))=scs_stab_diag_v39 s i j`,
SCS_TAC
THEN STRIP_TAC
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN ASM_SIMP_TAC[PSORT_MOD;ARITH_RULE`3<=k==> ~(k=0)`]);;
let DIAG_MOD=prove(`~(k=0)==> scs_diag k (i MOD k) (j MOD k)= scs_diag k i j`,
SIMP_TAC[scs_diag;MOD_REFL;Hypermap.lemma_suc_mod]);;
let SET_STAB_6I1=prove(`{ scs_stab_diag_v39 scs_6I1 i j| scs_diag 6 i j }= { scs_stab_diag_v39 scs_6I1 (i MOD 6) (j  MOD 6)| scs_diag 6 (i MOD 6) (j  MOD 6) }`,
 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(6=0)`;]
THEN MRESAL_TAC STAB_MOD[`scs_6I1`][SCS_6I1_IS_SCS;K_SCS_6I1]);;

let DIAG_EQ_ADD=prove(`scs_diag 6 (i MOD 6) (j MOD 6)<=> 
((i MOD 6= (j MOD 6+ 2) MOD 6)\/ (i MOD 6= (j MOD 6+ 3) MOD 6)\/
(j MOD 6=(i MOD 6+2) MOD 6)\/ (j MOD 6= (i MOD 6+ 3) MOD 6))`,
REWRITE_TAC[scs_diag]
THEN MP_TAC(ARITH_RULE`i MOD 6<6==> i MOD 6= 0 \/ i MOD 6= 1 \/i MOD 6= 2 \/
i MOD 6= 3 \/i MOD 6= 4 \/i MOD 6= 5
`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`j MOD 6<6==> j MOD 6= 0 \/ j MOD 6= 1 \/j MOD 6= 2 \/
j MOD 6= 3 \/j MOD 6= 4 \/j MOD 6= 5
`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`]
THEN RESA_TAC
THEN ARITH_TAC);;

let PSORT_EQ_SYM=prove(`psort (scs_k_v39 s) (j,i) = psort (scs_k_v39 s) (j',i')
<=> psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (j',i')`,
GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[]);;
let PSORT_EQ_SYM1=prove(`psort (scs_k_v39 s) (j,i) = (j',i')
<=> psort (scs_k_v39 s) (i,j) = (j',i')`,
GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[]);;

let STAB_SYM=prove(`scs_stab_diag_v39 s i j =
 scs_stab_diag_v39 s j i`,
SCS_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[PSORT_EQ_SYM]
THEN REWRITE_TAC[]);;

let EXPAND_STAB_DIAG=prove_by_refinement(`{scs_stab_diag_v39 scs_6I1 (i MOD 6) (j MOD 6) | i MOD 6 =
                                                  (j MOD 6 + 2) MOD 6 \/
                                                  i MOD 6 =
                                                  (j MOD 6 + 3) MOD 6 \/
                                                  j MOD 6 =
                                                  (i MOD 6 + 2) MOD 6 \/
                                                  j MOD 6 =
                                                  (i MOD 6 + 3) MOD 6}=
{scs_stab_diag_v39 scs_6I1 (i+2) i| i<6} UNION
{scs_stab_diag_v39 scs_6I1 (i+3) i|i<6} `,
[
REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;UNION]
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC;

MRESAS_TAC STAB_MOD[`scs_6I1`;`j MOD 6 + 2`;`j MOD 6`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`]
THEN MATCH_MP_TAC (SET_RULE`A==> A\/B`)
THEN EXISTS_TAC`j MOD 6`
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`];

MRESAS_TAC STAB_MOD[`scs_6I1`;`j MOD 6 + 3`;`j MOD 6`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`]
THEN MATCH_MP_TAC (SET_RULE`A==> B\/A`)
THEN EXISTS_TAC`j MOD 6`
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`];

MRESAS_TAC STAB_MOD[`scs_6I1`;`i MOD 6`;`i MOD 6 + 2`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`]
THEN MATCH_MP_TAC (SET_RULE`A==> A\/B`)
THEN EXISTS_TAC`i MOD 6`
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`;STAB_SYM];

MRESAS_TAC STAB_MOD[`scs_6I1`;`i MOD 6`;`i MOD 6 + 3`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`]
THEN MATCH_MP_TAC (SET_RULE`A==> B\/A`)
THEN EXISTS_TAC`i MOD 6`
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`;STAB_SYM];

EXISTS_TAC`i+2`
THEN EXISTS_TAC`i:num`
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`;MOD_LT]
THEN MRESAS_TAC STAB_MOD[`scs_6I1`;`i MOD 6 + 2`;`i MOD 6`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`;MOD_LT];

EXISTS_TAC`i+3`
THEN EXISTS_TAC`i:num`
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`;MOD_LT]
THEN MRESAS_TAC STAB_MOD[`scs_6I1`;`i MOD 6 + 3`;`i MOD 6`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`;MOD_LT]]);;

let EQ_DIAG_STAB_6I1_02=prove(`
scs_arrow_v39
 {scs_stab_diag_v39 scs_6I1 (i + 2) i } 
 {scs_stab_diag_v39 scs_6I1 0 2}`,
MRESA_TAC STAB_SYM[`scs_6I1`;`2`;`0`]
THEN MP_TAC (GEN_ALL Wkeidft.WKEIDFT)
THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
THEN STRIP_TAC
THEN MATCH_DICH_TAC 0
THEN ASM_SIMP_TAC[ARITH_RULE`2 + i = (i + 2) + 0/\ 3<6/\ i+1= SUC i`;K_SCS_6I1;h0_LT_B_SCS_6I1;h0_EQ_B_SCS_6I1;SCS_6I1_IS_SCS;SCS_6I1_BASIC]
THEN SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&2`
THEN EXISTS_TAC`&2 *h0`
THEN EXISTS_TAC`&2 *h0`
THEN EXISTS_TAC`&6`
THEN ASM_SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + 2)= i+3/\ SUC i= i+1/\ 2+1=3`;ARITH_RULE`1<6/\ ~(6=0)`;Qknvmlb.SUC_MOD_NOT_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN SCS_TAC
THEN MP_TAC(SET_RULE`i= i+0==> i MOD 6= (i+0) MOD 6`)
THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
THEN RESA_TAC
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`1<6/\ ~(6=0)`]
THEN SCS_TAC);;

let EQ_DIAG_STAB_6I1_03=prove(`
scs_arrow_v39
 {scs_stab_diag_v39 scs_6I1 (i + 3) i } 
 {scs_stab_diag_v39 scs_6I1 0 3}`,
MRESA_TAC STAB_SYM[`scs_6I1`;`3`;`0`]
THEN MP_TAC (GEN_ALL Wkeidft.WKEIDFT)
THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
THEN STRIP_TAC
THEN MATCH_DICH_TAC 0
THEN ASM_SIMP_TAC[ARITH_RULE`3 + i = (i + 3) + 0/\ 3<6/\ i+1= SUC i`;K_SCS_6I1;h0_LT_B_SCS_6I1;h0_EQ_B_SCS_6I1;SCS_6I1_IS_SCS;SCS_6I1_BASIC]
THEN SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&2`
THEN EXISTS_TAC`&2 *h0`
THEN EXISTS_TAC`&2 *h0`
THEN EXISTS_TAC`&6`
THEN ASM_SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + 3)= i+4/\ SUC i= i+1/\ 3+1=4`;ARITH_RULE`1<6/\ ~(6=0)`;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN SCS_TAC
THEN MP_TAC(SET_RULE`i= i+0==> i MOD 6= (i+0) MOD 6`)
THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
THEN RESA_TAC
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`1<6/\ ~(6=0)`]
THEN SCS_TAC);;

let SET_EQ_DIAG_STAB_6I1_02=prove(`
scs_arrow_v39
 {scs_stab_diag_v39 scs_6I1 (i + 2) i |i<6} 
 {scs_stab_diag_v39 scs_6I1 0 2}`,
REWRITE_TAC[ARITH_RULE`i<6<=> i=0\/i=1\/i=2\/i=3\/i=4\/i=5`;SET_RULE`{scs_stab_diag_v39 scs_6I1 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4\/i=5}
= {scs_stab_diag_v39 scs_6I1 (0 + 2) 0} UNION
{scs_stab_diag_v39 scs_6I1 (1 + 2) 1} UNION
{scs_stab_diag_v39 scs_6I1 (2 + 2) 2} UNION
{scs_stab_diag_v39 scs_6I1 (3 + 2) 3} UNION
{scs_stab_diag_v39 scs_6I1 (4 + 2) 4} UNION
{scs_stab_diag_v39 scs_6I1 (5 + 2) 5} 
`;]
THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02]
THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02]
THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02]
THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02]
THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02]);;



let SET_EQ_DIAG_STAB_6I1_03=prove(`
scs_arrow_v39
 {scs_stab_diag_v39 scs_6I1 (i + 3) i |i<6} 
 {scs_stab_diag_v39 scs_6I1 0 3}`,
REWRITE_TAC[ARITH_RULE`i<6<=> i=0\/i=1\/i=2\/i=3\/i=4\/i=5`;SET_RULE`{scs_stab_diag_v39 scs_6I1 (i + 3) i |i=0\/i=1\/i=2\/i=3\/i=4\/i=5}
= {scs_stab_diag_v39 scs_6I1 (0 + 3) 0} UNION
{scs_stab_diag_v39 scs_6I1 (1 + 3) 1} UNION
{scs_stab_diag_v39 scs_6I1 (2 + 3) 2} UNION
{scs_stab_diag_v39 scs_6I1 (3 + 3) 3} UNION
{scs_stab_diag_v39 scs_6I1 (4 + 3) 4} UNION
{scs_stab_diag_v39 scs_6I1 (5 + 3) 5} 
`;]
THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03]
THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03]
THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03]
THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03]
THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03]);;
let SET_EQ_DIAG_STAB_6I1=prove( `scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 i j| scs_diag 6 i j } 
{ scs_stab_diag_v39 scs_6I1 0 2,  scs_stab_diag_v39 scs_6I1 0 3}`,
ONCE_REWRITE_TAC[SET_STAB_6I1]
THEN REWRITE_TAC[DIAG_EQ_ADD;EXPAND_STAB_DIAG;SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}
={scs_stab_diag_v39 scs_6I1 0 2}UNION{ scs_stab_diag_v39 scs_6I1 0 3}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_6I1_02;SET_EQ_DIAG_STAB_6I1_03]);;




let OEHDBEN_PRIME=prove( `
main_nonlinear_terminal_v11
==>
scs_arrow_v39 { scs_6I1 } { scs_6T1, scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}`,
STRIP_TAC
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{ scs_6T1}UNION { scs_stab_diag_v39 scs_6I1 i j| scs_diag 6 i j }`
THEN ASM_SIMP_TAC[SCS_6I1_BERAK_BY_CSTAB;SET_RULE`{scs_6T1, scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}
={scs_6T1}UNION{ scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_6I1;]
THEN MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[SCS_6T1_IS_SCS]);;


let OEHDBEN= prove(`main_nonlinear_terminal_v11
==>
scs_arrow_v39 { scs_6I1 } { scs_6T1, scs_5M1, scs_4M2, scs_3M1 }`,
STRIP_TAC
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{ scs_6T1, scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}`
THEN ASM_SIMP_TAC[OEHDBEN_PRIME;SET_RULE`{scs_6T1, scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}
= {scs_6T1} UNION {scs_stab_diag_v39 scs_6I1 0 2} UNION{ scs_stab_diag_v39 scs_6I1 0 3}`;
SET_RULE`{ scs_6T1, scs_5M1, scs_4M2, scs_3M1 }={scs_6T1} UNION{  scs_3M1,scs_5M1}UNION {scs_4M2}`]
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_REWRITE_TAC[SCS_6T1_IS_SCS];


MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_REWRITE_TAC[AQICLXA;FZIOTEF]]);;





 end;;


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