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 Hijqaha = struct


open Polyhedron;;
open Sphere;;
open Topology;;		
open Fan_misc;;
open Planarity;; 
open Conforming;;
open Hypermap;;
open Fan;;
open Topology;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Collect_geom;;
open Dih2k_hypermap;;
open Wjscpro;;
open Tecoxbm;;
open Hdplygy;;
open Nkezbfc_local;;
open Flyspeck_constants;;
open Gbycpxs;;
open Pcrttid;;
open Local_lemmas1;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;





open Hypermap;;
open Fan;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Flyspeck_constants;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;


open Zithlqn;;


open Xwitccn;;

open Ayqjtmd;;

open Jkqewgv;;


open Mtuwlun;;


open Uxckfpe;;
open Sgtrnaf;;

open Yxionxl;;

open Qknvmlb;;
open Odxlstcv2;;

open Yxionxl2;;
open Eyypqdw;;
open Ocbicby;;
open Imjxphr;;
open Nuxcoea;;
open Aursipd;;
open Cuxvzoz;;
open Rrcwnsj;;
open Tfitskc;;
open Hexagons;;
open Otmtotj;;



let SCS_5I1_STAB_DIAG_2h0=prove_by_refinement(`!v i j. 
     BBs_v39 scs_5M2 v/\
    scs_diag 5 i j /\
    dist(v i,v j) <= cstab/\
    (!i. dist(v i, v(i+1))<= &2 * h0)
     ==>
    BBs_v39 (scs_stab_diag_v39 scs_5I2 i j) v`,
[
REWRITE_TAC[IN]
THEN REPEAT STRIP_TAC
THEN DICH_TAC 3
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASSUME_TAC th
THEN MP_TAC th)
THEN
REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I2;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`;IN;K_SCS_5I2;Terminal.FUNLIST_EXPLICIT;]
THEN ASM_SIMP_TAC[]
THEN REPEAT RESA_TAC
THEN SCS_TAC
THEN MP_TAC(SET_RULE`i' MOD 5= j' MOD 5\/ ~(i' MOD 5= j' MOD 5)`)
THEN RESA_TAC;


THAYTHE_TAC (8-6)[`i'`;`j'`];

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


THAYTHE_TAC (9-6)[`i'`;`j'`]
THEN DICH_TAC 1
THEN MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
THEN SYM_ASSUM_TAC
THEN DICH_TAC 1
THEN STRIP_TAC
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i'`;`5`][ARITH_RULE`1<5`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i' MOD 5<5==> i' MOD 5=0\/ i' MOD 5=1\/ i' MOD 5=2\/ i' MOD 5=3\/i' MOD 5=4`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
THEN RESA_TAC
THEN SCS_TAC;

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

THAYTHE_TAC (10-6)[`i'`;`j'`]
THEN DICH_TAC 1
THEN MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j'`;`5`][ARITH_RULE`1<5`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`j' MOD 5<5==> j' MOD 5=0\/ j' MOD 5=1\/ j' MOD 5=2\/ j' MOD 5=3\/j' MOD 5=4`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
THEN RESA_TAC
THEN SCS_TAC;

MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`]
THEN THAYTHE_TAC(11-6)[`i'`;`j'`]
THEN DICH_TAC 1
THEN REWRITE_TAC[PAIR_EQ;cstab]
THEN SCS_TAC
THEN MP_TAC sqrt8_LE_CSTAB
THEN REAL_ARITH_TAC;

THAYTHE_TAC (8-6)[`i'`;`j'`]
THEN DICH_TAC 0
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

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

MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j'`;`v`;`SUC i'`][SCS_5M2_IS_SCS;K_SCS_5M2;]
THEN REWRITE_TAC[ADD1]
THEN THAYTHE_TAC (10-2)[`i'`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

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

MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i'`;`v`;`SUC j'`][SCS_5M2_IS_SCS;K_SCS_5M2;]
THEN REWRITE_TAC[ADD1]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN THAYTHE_TAC (11-2)[`j'`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
THEN RESA_TAC;

MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`5`];

MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i'`;`v`;`i`][SCS_5M2_IS_SCS;K_SCS_5M2;]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j'`;`v`;`j`][SCS_5M2_IS_SCS;K_SCS_5M2;];

MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j'`;`v`;`i`][SCS_5M2_IS_SCS;K_SCS_5M2;]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i'`;`v`;`j`][SCS_5M2_IS_SCS;K_SCS_5M2;]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[];

MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`]
THEN THAYTHE_TAC(12-6)[`i'`;`j'`]
THEN DICH_TAC 0
THEN REWRITE_TAC[PAIR_EQ;cstab]
THEN SCS_TAC]);;


let MM_5M2_IMP_MM_STAB_5I2=prove(`
    MMs_v39 scs_5M2 v /\
    scs_diag 5 i j /\
    dist(v i,v j) <= cstab/\
    (!i. dist(v i, v(i+1))<= &2 * h0)
     ==>
    ~(MMs_v39 (scs_stab_diag_v39 scs_5I2 i j)= {})`,
STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_5M2`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`]
THEN ASSUME_TAC SCS_5M2_BASIC
THEN ASSUME_TAC K_SCS_5M2
THEN ASM_SIMP_TAC[SCS_5M2_IS_SCS;STAB_5I2_SCS;K_SCS_5I2;SCS_K_D_A_STAB_EQ;IN;SCS_5I1_STAB_DIAG_2h0]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;


let SCS_5I1_STAB_DIAG_2h0_sqrt8=prove_by_refinement(
`BBs_v39 scs_5M2 v/\
    scs_diag 5 i j /\
    dist(v i,v j) <= cstab/\
    &2* h0 <= dist(v 0, v(1)) /\ dist(v 0, v(1))<= sqrt8
     ==>
    BBs_v39 ((scs_stab_diag_v39 scs_5I3 i j) ) v`,
[
REWRITE_TAC[IN]
THEN REPEAT STRIP_TAC
THEN DICH_TAC 4
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASSUME_TAC th
THEN MP_TAC th)
THEN
REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`;IN;K_SCS_5I3;scs_prop_equ_v39;]
THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
THEN ASM_SIMP_TAC[]
THEN REPEAT RESA_TAC
THEN SCS_TAC
THEN MP_TAC(SET_RULE`i' MOD 5= j' MOD 5\/ ~(i' MOD 5= j' MOD 5)`)
THEN RESA_TAC;

THAYTHES_TAC (8-6)[`i':num`;`j':num`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(5=0)`];

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

THAYTHE_TAC (9-6)[`i'`;`j'`]
THEN DICH_TAC 1
THEN MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i':num`;`j':num`][ARITH_RULE`~(5=0)`]
THEN SYM_ASSUM_TAC
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` (i') MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` (j') MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN DICH_TAC 3
THEN STRIP_TAC
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i'`;`5`][ARITH_RULE`1<5`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i' MOD 5<5==> i' MOD 5=0\/ i' MOD 5=1\/ i' MOD 5=2\/ i' MOD 5=3\/i' MOD 5=4`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`;]
THEN RESA_TAC
THEN SCS_TAC;


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


THAYTHE_TAC (10-6)[`i'`;`j'`]
THEN DICH_TAC 1
THEN MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i':num`;`j':num`][ARITH_RULE`~(5=0)`]
THEN SYM_ASSUM_TAC
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` (i') MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` (j') MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j'`;`5`][ARITH_RULE`1<5`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`j' MOD 5<5==> j' MOD 5=0\/ j' MOD 5=1\/ j' MOD 5=2\/ j' MOD 5=3\/j' MOD 5=4`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`;]
THEN RESA_TAC
THEN SCS_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN RESA_TAC;

MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`]
THEN THAYTHE_TAC(11-6)[`i'`;`j'`]
THEN DICH_TAC 1
THEN REWRITE_TAC[PAIR_EQ;cstab;h0]
THEN SCS_TAC
THEN REAL_ARITH_TAC;

THAYTHES_TAC (8-6)[`i':num`;`j':num`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(5=0)`;cstab]
THEN DICH_TAC 0
THEN REAL_ARITH_TAC;

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

THAYTHES_TAC (9-6)[`i':num`;`j':num`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(5=0)`;cstab]
THEN DICH_TAC 0
THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
THEN RESA_TAC;

MRESAL_TAC Hexagons.DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[scs_diag];

SCS_TAC
THEN MP_TAC(SET_RULE`psort 5 (i',j') = 0,1\/ ~(psort 5 (i',j') = 0,1)`)
THEN RESA_TAC;

MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`1`;`j'`;`0`;`5`][PSORT_5_EXPLICIT];

MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`];

MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[];

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

THAYTHES_TAC (10-6)[`i':num`;`j':num`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(5=0)`;cstab]
THEN DICH_TAC 0
THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
THEN RESA_TAC;

MRESAL_TAC Hexagons.DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[scs_diag];

SCS_TAC
THEN MP_TAC(SET_RULE`psort 5 (i',j') = 0,1\/ ~(psort 5 (i',j') = 0,1)`)
THEN RESA_TAC;

MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`1`;`j'`;`0`;`5`][PSORT_5_EXPLICIT];

MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`];

MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[];

MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
THEN RESA_TAC;

MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`j`;`j'`;`i`;`5`][PSORT_5_EXPLICIT];

MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`];

MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[];


MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`]
THEN THAYTHE_TAC(13-7)[`i'`;`j'`]
THEN DICH_TAC 0
THEN REWRITE_TAC[PAIR_EQ;cstab]
THEN SCS_TAC]);;



let SCS_5M2_EDGE_LE_2H0=prove(`BBs_v39 scs_5M2 v/\
    scs_diag 5 i j /\
    dist(v i,v j) <= cstab/\
    &2* h0 < dist(v l, v (SUC l))
/\ ~(l MOD 5=0)
     ==> F`,
REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`;IN;K_SCS_5I3;scs_prop_equ_v39;]
THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
THEN REPEAT STRIP_TAC
THEN THAYTHE_TAC 7[`l`;`SUC l`]
THEN DICH_TAC 0
THEN SCS_TAC
THEN ASM_SIMP_TAC[Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`~(5=0)`]
THEN MRESAL_TAC Hexagons.PSORT_MOD[`5`;`l:num`;`SUC l:num`][ARITH_RULE`~(5=0)`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`l`;`5`][ARITH_RULE`1<5`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`l MOD 5<5==> l MOD 5=0\/ l MOD 5=1\/ l MOD 5=2\/ l MOD 5=3\/l MOD 5=4`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`;]
THEN RESA_TAC
THEN SCS_TAC
THEN DICH_TAC (10-7)
THEN REAL_ARITH_TAC);;





let SCS_5M2_EDGE_LE_2H0_IMP_0=prove( `BBs_v39 scs_5M2 v/\
    scs_diag 5 i j /\
    dist(v i,v j) <= cstab/\
    &2* h0 < dist(v l, v (SUC l))
==> l MOD 5=0`,
STRIP_TAC
THEN MP_TAC SCS_5M2_EDGE_LE_2H0
THEN RESA_TAC);;


let MM_5M2_IMP_MM_STAB_5I3=prove(`  MMs_v39 scs_5M2 v /\
    scs_diag 5 i j /\
    dist(v i,v j) <= cstab/\
     &2 * h0< dist(v l, v(l+1)) /\
     dist(v l, v(l+1))<= sqrt8
     ==>
    ~(MMs_v39 (scs_stab_diag_v39 scs_5I3 i j)= {})`,
STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_5M2`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`]
THEN ASSUME_TAC SCS_5M2_BASIC
THEN ASSUME_TAC K_SCS_5M2
THEN ASM_SIMP_TAC[SCS_5M2_IS_SCS;STAB_5I3_SCS;K_SCS_5I3;SCS_K_D_A_STAB_EQ;IN; ADD1]
THEN MP_TAC SCS_5M2_EDGE_LE_2H0_IMP_0
THEN REWRITE_TAC[ ADD1]
THEN RESA_TAC
THEN DICH_TAC 4
THEN DICH_TAC 4
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l:num`;`v`;` l MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l+1:num`;`v`;` (l+1) MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`]
THEN MRESAL_TAC MOD_ADD_MOD[`l`;`1`;`5`][ARITH_RULE`~(5=0)/\ 1 MOD 5=1/\ 0+a=a`] THEN SYM_ASSUM_TAC
THEN STRIP_TAC
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&2 * h0 < dist ((v:num->real^3) 0,v 1) ==> &2 * h0 <= dist (v 0,v 1)`)
THEN RESA_TAC
THEN MP_TAC SCS_5I1_STAB_DIAG_2h0_sqrt8
THEN RESA_TAC
THEN SCS_TAC
THEN REAL_ARITH_TAC);;

let SCS_5I1_STAB_DIAG_sqrt8=prove_by_refinement(`BBs_v39 scs_5M2 v/\
    scs_diag 5 i j /\
    dist(v i,v j) <= cstab/\
    sqrt8 <= dist(v 0, v(1)) 
     ==>
    BBs_v39 ((scs_stab_diag_v39 scs_5M2 i j) ) v`,
[
REWRITE_TAC[IN]
THEN REPEAT STRIP_TAC
THEN DICH_TAC 3
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASSUME_TAC th
THEN MP_TAC th)
THEN
REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`;IN;K_SCS_5I3;scs_prop_equ_v39;]
THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
THEN ASM_SIMP_TAC[]
THEN REPEAT RESA_TAC
THEN SCS_TAC
THEN MP_TAC(SET_RULE`i' MOD 5= j' MOD 5\/ ~(i' MOD 5= j' MOD 5)`)
THEN RESA_TAC;

THAYTHE_TAC (8-6)[`i'`;`j'`]
THEN DICH_TAC 0
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
THEN RESA_TAC;

MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`j`;`j'`;`i`;`5`][PSORT_5_EXPLICIT];


MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`];

MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[];

THAYTHE_TAC(9-6)[`i'`;`j'`]
THEN DICH_TAC 0
THEN SCS_TAC]);;



let MM_5M2_IMP_MM_STAB_5M2=prove(`  MMs_v39 scs_5M2 v /\
    scs_diag 5 i j /\
    dist(v i,v j) <= cstab/\
     sqrt8<= dist(v l, v(l+1)) 
     ==>
    ~(MMs_v39 (scs_stab_diag_v39 scs_5M2 i j)= {})`,
STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_5M2`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`]
THEN ASSUME_TAC SCS_5M2_BASIC
THEN ASSUME_TAC K_SCS_5M2
THEN ASM_SIMP_TAC[SCS_5M2_IS_SCS;STAB_5M2_SCS;K_SCS_5I3;SCS_K_D_A_STAB_EQ;IN; ADD1]
THEN MP_TAC SCS_5M2_EDGE_LE_2H0_IMP_0
THEN ASM_REWRITE_TAC[ ADD1;h0]
THEN MP_TAC LT_sqrt8_2h0
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`sqrt8 <= dist ((v:num->real^3) l,v (l + 1))/\ &2 * #1.26 < sqrt8==> &2 * #1.26 < dist (v l,v (l + 1))`)
THEN RESA_TAC
THEN STRIP_TAC
THEN DICH_TAC (9-3)
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l:num`;`v`;` l MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l+1:num`;`v`;` (l+1) MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`]
THEN MRESAL_TAC MOD_ADD_MOD[`l`;`1`;`5`][ARITH_RULE`~(5=0)/\ 1 MOD 5=1/\ 0+a=a`] THEN SYM_ASSUM_TAC
THEN STRIP_TAC
THEN MP_TAC SCS_5I1_STAB_DIAG_sqrt8
THEN RESA_TAC
THEN SCS_TAC
THEN REAL_ARITH_TAC);;


(************)
(*new definition scs*)
(*************************)

let SCS_DIAG_SCS_5M2_02=prove(`scs_diag (scs_k_v39 scs_5M2) 0 2`,
REWRITE_TAC[K_SCS_5M2;scs_diag]
THEN ARITH_TAC);;
let SCS_DIAG_SCS_5M2_03=prove(`scs_diag (scs_k_v39 scs_5M2) 0 3`,
REWRITE_TAC[K_SCS_5M2;scs_diag]
THEN ARITH_TAC);;
let SCS_DIAG_SCS_5M2_24=prove(`scs_diag (scs_k_v39 scs_5M2) 2 4`,
REWRITE_TAC[K_SCS_5M2;scs_diag]
THEN ARITH_TAC);;



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

  let scs_3T4_prime = (* terminal_tri_6833979866 =  *) new_definition
    `scs_3T4_prime = mk_unadorned_v39  3
    (#0.2759)
    (funlist_v39 [(0,1),(&2);(1,2),cstab] (&2*h0) 3)
    (funlist_v39 [(0,1),(&2 * h0)] (cstab) 3)`;;

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

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

let scs_3T1_PRELIM_prime = (* ear_jnull =  *) new_definition
    `scs_3T1_prime = scs_v39 (3, #0.11,
			funlist_v39 [(0,1),cstab] (&2) 3,
			funlist_v39 [(0,1),cstab] (&2) 3,
			funlist_v39 [(0,1),cstab] (&2*h0) 3,
			funlist_v39 [(0,1),cstab] ((&2)*h0) 3,
			(\i j.  F),{},{},{})`;;

  let scs_3T1_prime = prove_by_refinement(
    `scs_3T1_prime = mk_unadorned_v39 3 (#0.11)   
      (funlist_v39 [(0,1),(cstab)] (&2) 3)
      (funlist_v39 [(0,1),(cstab)] (&2 * h0) 3)`,
    (* {{{ proof *)
    [
      BY(REWRITE_TAC[mk_unadorned_v39;scs_3T1_PRELIM_prime]);
    ]);;  (* }}} *)
  let scs_4M8_prime = new_definition
    `scs_4M8_prime = mk_unadorned_v39 4 (#0.513)
    (funlist_v39 [(0,1),(&2*h0);(2,3),(cstab);(0,2),(cstab);(1,3),(cstab)] (&2) 4)
    (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(&6);(1,3),(&6);(1,3),(&6)] (&2*h0) 4)`;;


let PSORT_5_EXPLICIT=prove(`
psort 5 (0,0)= (0,0)/\ 
psort 5 (1,1)= (1,1)/\
psort 5 (2,2)= (2,2)/\ 
psort 5 (3,3)= (3,3)/\ 
psort 5 (4,4)= (4,4)/\ 
psort 5 (0,1)= (0,1)/\ 
psort 5 (0,2)= (0,2)/\
psort 5 (0,3)= (0,3)/\
psort 5 (0,4)= (0,4)/\
psort 5 (1,0)= (0,1)/\
psort 5 (1,2)= (1,2)/\
psort 5 (1,3)= (1,3)/\
psort 5 (1,4)= (1,4)/\
psort 5 (2,0)= (0,2)/\
psort 5 (2,1)= (1,2)/\
psort 5 (2,3)= (2,3)/\
psort 5 (2,4)= (2,4)/\
psort 5 (3,0)= (0,3)/\
psort 5 (3,1)= (1,3)/\
psort 5 (3,2)= (2,3)/\
psort 5 (3,4)= (3,4)/\
psort 5 (4,0)= (0,4)/\
psort 5 (4,1)= (1,4)/\
psort 5 (4,2)= (2,4)/\
psort 5 (4,3)= (3,4)/\
psort 5 (4,5)= (0,4)/\
psort 5 (3,5)= (0,3)/\
psort 5 (2,5)= (0,2)/\
psort 5 (1,5)= (0,1)/\
psort 5 (5,1)= (0,1)/\
psort 5 (5,2)= (0,2)/\
psort 5 (5,3)= (0,3)/\
psort 5 (5,4)= (0,4)/\
psort 5 (5,5)= (0,0)/\
psort 5 (5,6)= (0,1)/\
psort 5 (5,7)= (0,2)/\
psort 5 (4,6)= (1,4)/\
psort 5 (6,4)= (1,4)/\
psort 5 (6,5)= (0,1)/\
psort 5 (6,7)= (1,2)/\
psort 5 (7,5)= (0,2)/\
psort 5 (7,6)= (1,2)/\
psort 5 (7,7)= (2,2)/\
psort 5 (6,6)= (1,1)/\
psort 4 (3,4)= (0,3)/\ 
psort 3 (2,0)= (0,2)/\
psort 3 (2,1)= (1,2)/\
psort 3 (1,0)= (0,1)`,
REWRITE_TAC[psort;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_4_TAC;LET_DEF;LET_END_DEF;MOD_5_EXPLICIT;ARITH_RULE`0<=a/\ ~(1<= 0)/\ ~(2<=0)/\ ~(3<=0)/\ ~(4<=0)/\a<=a/\ ~(2<=1)/\ ~(3<=2)/\ ~(4<=3)/\ ~(3<=1)/\ ~(4<=1)/\ ~(4<=2)/\ 2<=3`]);;

let SCS_TAC= ASM_SIMP_TAC[scs_basic;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} j <=> {} i`;periodic2;scs_basic;unadorned_v39;scs_prop_equ_v39;LET_DEF;LET_END_DEF;scs_stab_diag_v39;scs_half_slice_v39;
Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_5_TAC;
scs_5M1;scs_3M1;scs_6I1;scs_3T1;scs_4M2;scs_6M1;scs_6T1;scs_5I1;scs_5I2;scs_5I3;scs_5M2;scs_4M6;scs_3T4;scs_5M3;scs_3T4_prime;scs_4M6_prime;scs_4M7_prime;scs_4M7;scs_3T1_prime;scs_4M8;scs_4M8_prime;scs_5T1;scs_3T5;scs_4M3;scs_3T6;scs_4M4;scs_4M5;
Terminal.FUNLIST_EXPLICIT;Yrtafyh.PSORT_PERIODIC;PSORT_5_EXPLICIT;
ARITH_RULE`SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6/\ SUC 6=7/\ SUC 7=8`];;











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


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

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

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

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

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

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

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

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

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

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

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

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

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

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

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

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

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

]);;


let SCS_5M3_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5M3`,
[
SIMP_TAC[scs_5M3;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_3T4_IS_SCS=prove_by_refinement(`is_scs_v39 scs_3T4`,
[
SIMP_TAC[scs_3T4;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]
THEN REAL_ARITH_TAC;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN MP_TAC LE_sqrt8_2h0
THEN REAL_ARITH_TAC;

SCS_TAC;

SCS_TAC
THEN ASM_SIMP_TAC[MOD_LT;h0]
THEN REAL_ARITH_TAC;

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

DICH_TAC 0
THEN ARITH_TAC;

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

]);;

let SCS_3T6_IS_SCS=prove_by_refinement(`is_scs_v39 scs_3T6'`,
[
SIMP_TAC[scs_3T6;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.4348 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
THEN REPEAT RESA_TAC;
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];
SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
THEN RESA_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
THEN REWRITE_TAC[];
SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN MP_TAC sqrt8_LE_CSTAB
THEN REAL_ARITH_TAC;
SCS_TAC;
SCS_TAC
THEN ASM_SIMP_TAC[MOD_LT;h0]
THEN MP_TAC LE_sqrt8_2
THEN REAL_ARITH_TAC;
SCS_TAC
THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
THEN REAL_ARITH_TAC;
SCS_TAC
THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
THEN REAL_ARITH_TAC;
MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
      (&2 * h0 < funlist_v39 [(0,1),cstab; (1,2),cstab] (&2 * h0) 3 i (SUC i) \/
       &2 < funlist_v39 [(0,1),sqrt8; (1,2),sqrt8] (&2) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`]
THEN MATCH_DICH_TAC 0
THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
THEN ARITH_TAC;
]);;

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


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


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


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

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

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

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

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

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

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

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

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

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

SCS_TAC;

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

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

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

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

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


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


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


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

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

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

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

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

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

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

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

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

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN MP_TAC sqrt8_LE_CSTAB
THEN REAL_ARITH_TAC;

SCS_TAC;

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

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

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

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

]);;

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

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

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

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

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

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

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

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

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

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

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

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

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

SCS_TAC;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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


SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

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

POP_ASSUM MP_TAC
THEN ARITH_TAC;

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


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

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

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



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


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


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


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


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


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


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


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


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


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


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



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



SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;


SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;


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


POP_ASSUM MP_TAC
THEN ARITH_TAC;


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



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


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


ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=2)`]
THEN ARITH_TAC;

]);;

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

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

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

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

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

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

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

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

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

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

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


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


SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

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

POP_ASSUM MP_TAC
THEN ARITH_TAC;

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


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

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

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

let SCS_4M4_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M4'`,
[

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

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

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

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

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

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

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

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

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

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

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


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


SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

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

POP_ASSUM MP_TAC
THEN ARITH_TAC;

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


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

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

ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=1)`]
THEN ARITH_TAC;
]);;
let SCS_4M3_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M3'`,
[

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

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

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

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

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

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

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

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

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

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

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


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


SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN MP_TAC sqrt8_LE_6
THEN MP_TAC sqrt8_LE_CSTAB
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

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

POP_ASSUM MP_TAC
THEN ARITH_TAC;

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


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

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

ASM_REWRITE_TAC[Geomdetail.CARD_SING]
THEN ARITH_TAC;



]);;



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

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

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

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

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

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

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

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

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

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

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


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


SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

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

POP_ASSUM MP_TAC
THEN ARITH_TAC;

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


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

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


ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=1)`]
THEN ARITH_TAC;

]);;


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

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

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

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

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

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

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

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

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

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

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


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


SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

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

POP_ASSUM MP_TAC
THEN ARITH_TAC;

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


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

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


ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=1)`]
THEN ARITH_TAC;

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

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

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

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

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

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

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

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

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

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

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


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


SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

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

POP_ASSUM MP_TAC
THEN ARITH_TAC;

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


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

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


ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=2)`]
THEN ARITH_TAC;

]);;


let SCS_4M8_prime_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M8_prime`,
[

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

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

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

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

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

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

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

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

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

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

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


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


SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

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

POP_ASSUM MP_TAC
THEN ARITH_TAC;

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


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

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


ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=2)`]
THEN ARITH_TAC;


]);;



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

let SCS_5M3_BASIC=prove(`scs_basic_v39 scs_5M3`,
SCS_TAC);;
let SCS_5T1_BASIC=prove(`scs_basic_v39 scs_5T1`,
SCS_TAC);;


let SCS_4M6_prime_BASIC=prove(`scs_basic_v39 scs_4M6_prime`,
SCS_TAC);;
let SCS_4M7_prime_BASIC=prove(`scs_basic_v39 scs_4M7_prime`,
SCS_TAC);;
let SCS_4M4_BASIC=prove(`scs_basic_v39 scs_4M4'`,
SCS_TAC);;

let SCS_4M7_BASIC=prove(`scs_basic_v39 scs_4M7`,
SCS_TAC);;
let SCS_4M3_BASIC=prove(`scs_basic_v39 scs_4M3'`,
SCS_TAC);;
let SCS_4M5_BASIC=prove(`scs_basic_v39 scs_4M5'`,
SCS_TAC);;
let SCS_3T4_prime_BASIC=prove(`scs_basic_v39 scs_3T4_prime`,
SCS_TAC);;
let SCS_3T6_BASIC=prove(`scs_basic_v39 scs_3T6'`,
SCS_TAC);;

let SCS_3T1_prime_BASIC=prove(`scs_basic_v39 scs_3T1_prime`,
SCS_TAC);;
let SCS_3T5_BASIC=prove(`scs_basic_v39 scs_3T5`,
SCS_TAC);;

let SCS_4M8_prime_BASIC=prove(`scs_basic_v39 scs_4M8_prime`,
SCS_TAC);;

let SCS_4M8_BASIC=prove(`scs_basic_v39 scs_4M8`,
SCS_TAC);;

let K_SCS_5M3=prove(`scs_k_v39 scs_5M3=5`,
SCS_TAC);;
let K_SCS_5T1=prove(`scs_k_v39 scs_5T1=5`,
SCS_TAC);;
let K_SCS_3T4_prime=prove(`scs_k_v39 scs_3T4_prime=3`,
SCS_TAC);;
let K_SCS_3T5=prove(`scs_k_v39 scs_3T5=3`,
SCS_TAC);;
let K_SCS_3T6=prove(`scs_k_v39 scs_3T6'=3`,
SCS_TAC);;
let K_SCS_4M4=prove(`scs_k_v39 scs_4M4'=4`,
SCS_TAC);;
let K_SCS_4M5=prove(`scs_k_v39 scs_4M5'=4`,
SCS_TAC);;
let K_SCS_4M3=prove(`scs_k_v39 scs_4M3'=4`,
SCS_TAC);;
let K_SCS_4M6_prime=prove(`scs_k_v39 scs_4M6_prime=4`,
SCS_TAC);;
let K_SCS_3T1_prime=prove(`scs_k_v39 scs_3T1_prime=3`,
SCS_TAC);;

let K_SCS_4M7_prime=prove(`scs_k_v39 scs_4M7_prime=4`,
SCS_TAC);;
let K_SCS_4M7=prove(`scs_k_v39 scs_4M7=4`,
SCS_TAC);;

let K_SCS_4M8_prime=prove(`scs_k_v39 scs_4M8_prime=4`,
SCS_TAC);;
let K_SCS_4M8=prove(`scs_k_v39 scs_4M8=4`,
SCS_TAC);;

let J_SCS_5M3=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5M3 i) i1 j= F`,
SCS_TAC );;
let J_SCS_5T1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5T1 i) i1 j= F`,
SCS_TAC );;

let J_SCS_3T4_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T4_prime i) i1 j= F`,
SCS_TAC );;

let J_SCS_4M4=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M4' i) i1 j= F`,
SCS_TAC );;

let J_SCS_4M3=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M3' i) i1 j= F`,
SCS_TAC );;
let J_SCS_4M5=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M5' i) i1 j= F`,
SCS_TAC );;
let J_SCS_4M6_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M6_prime i) i1 j= F`,
SCS_TAC );;
let J_SCS_5M2=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5M2 i) i1 j= F`,
SCS_TAC );;
let J_SCS_3T1_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T1_prime i) i1 j= F`,
SCS_TAC );;
let J_SCS_3T1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T1 i) i1 j= F`,
SCS_TAC );;
let J_SCS_3T6=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T6' i) i1 j= F`,
SCS_TAC );;
let J_SCS_3T5=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T5 i) i1 j= F`,
SCS_TAC );;

let J_SCS_4M7_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M7_prime i) i1 j= F`,
SCS_TAC );;
let J_SCS_4M7=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M7 i) i1 j= F`,
SCS_TAC );;
let J_SCS_4M8_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M8_prime i) i1 j= F`,
SCS_TAC );;
let J_SCS_4M8=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M8 i) i1 j= F`,
SCS_TAC );;
let J_SCS_4M8_prime1=prove(`scs_J_v39 (scs_4M8_prime ) i1 j= F`,
SCS_TAC );;



let STAB_5I1_SCS=prove(` scs_diag (scs_k_v39 scs_5I1) i j
==> is_scs_v39 (scs_stab_diag_v39 scs_5I1 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5I1 i j)`,
STRIP_TAC
THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5I1_IS_SCS;SCS_5I1_BASIC;K_SCS_5I1;
ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
THEN SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC);;

let STAB_5I2_SCS=prove(` scs_diag (scs_k_v39 scs_5I2) i j
==> is_scs_v39 (scs_stab_diag_v39 scs_5I2 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5I2 i j)`,
STRIP_TAC
THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5I2_IS_SCS;SCS_5I2_BASIC;K_SCS_5I2;
ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
THEN SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN MP_TAC sqrt8_LE_CSTAB
THEN REAL_ARITH_TAC);;

let STAB_5M3_SCS=prove(` scs_diag (scs_k_v39 scs_5M3) i j
==> is_scs_v39 (scs_stab_diag_v39 scs_5M3 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5M3 i j)`,
STRIP_TAC
THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5M3_IS_SCS;SCS_5M3_BASIC;K_SCS_5M3;
ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
THEN SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC);;

let STAB_5T1_SCS=prove(` scs_diag (scs_k_v39 scs_5T1) i j
==> is_scs_v39 (scs_stab_diag_v39 scs_5T1 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5T1 i j)`,
STRIP_TAC
THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5T1_IS_SCS;SCS_5T1_BASIC;K_SCS_5T1;
ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
THEN SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC);;

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

let SCS_5M3_STAB_DIAG_sqrt8=prove_by_refinement(`BBs_v39 scs_5M2 v/\
    scs_diag 5 i j /\
    dist(v i,v j) <= cstab/\
    sqrt8 <= dist(v 0, v(1)) 
     ==>
    BBs_v39 ((scs_stab_diag_v39 scs_5M3 i j) ) v`,
[REWRITE_TAC[IN]
THEN REPEAT STRIP_TAC
THEN DICH_TAC 3
THEN STRIP_TAC
THEN POP_ASSUM(fun th-> ASSUME_TAC th
THEN MP_TAC th)
THEN
REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5M3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`;IN;K_SCS_5M3;scs_prop_equ_v39;]
THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
THEN ASM_SIMP_TAC[]
THEN REPEAT RESA_TAC
THEN SCS_TAC
THEN MP_TAC(SET_RULE`i' MOD 5= j' MOD 5\/ ~(i' MOD 5= j' MOD 5)`)
THEN RESA_TAC;

THAYTHE_TAC (8-6)[`i'`;`j'`]
THEN DICH_TAC 0
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

MP_TAC(SET_RULE`psort 5 (i',j') = 0,1\/ ~(psort 5 (i',j') = 0,1)`)
THEN RESA_TAC;

MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`1`;`j'`;`0`;`5`][PSORT_5_EXPLICIT];

MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN DICH_TAC(13-2)
THEN MP_TAC LE_sqrt8_2h0
THEN REWRITE_TAC[h0]
THEN REAL_ARITH_TAC;

MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN DICH_TAC(13-2)
THEN MP_TAC LE_sqrt8_2h0
THEN REWRITE_TAC[h0]
THEN REAL_ARITH_TAC;

THAYTHE_TAC (9-6)[`i'`;`j'`]
THEN DICH_TAC 1
THEN SCS_TAC
THEN REWRITE_TAC[cstab;h0];

THAYTHE_TAC (8-6)[`i'`;`j'`]
THEN DICH_TAC 0
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
THEN RESA_TAC;

MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`j`;`j'`;`i`;`5`][PSORT_5_EXPLICIT];

MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`];

MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[];

THAYTHE_TAC(9-6)[`i'`;`j'`]
THEN DICH_TAC 0
THEN SCS_TAC]);;

let SCS_DIAG_SCS_5M3_02=prove(`scs_diag (scs_k_v39 scs_5M3) 0 2`,
REWRITE_TAC[K_SCS_5M3;scs_diag]
THEN ARITH_TAC);;
let SCS_DIAG_SCS_5M3_03=prove(`scs_diag (scs_k_v39 scs_5M3) 0 3`,
REWRITE_TAC[K_SCS_5M3;scs_diag]
THEN ARITH_TAC);;
let SCS_DIAG_SCS_5M3_24=prove(`scs_diag (scs_k_v39 scs_5M3) 2 4`,
REWRITE_TAC[K_SCS_5M3;scs_diag]
THEN ARITH_TAC);;

let MM_5M2_IMP_MM_STAB_5M3=prove(
`  MMs_v39 scs_5M2 v /\
    scs_diag 5 i j /\
    dist(v i,v j) <= cstab/\
     sqrt8<= dist(v l, v(l+1)) 
     ==>
    ~(MMs_v39 (scs_stab_diag_v39 scs_5M3 i j)= {})`,
STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_5M2`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`]
THEN ASSUME_TAC SCS_5M2_BASIC
THEN ASSUME_TAC K_SCS_5M2
THEN ASM_SIMP_TAC[SCS_5M2_IS_SCS;STAB_5M3_SCS;K_SCS_5M3;SCS_K_D_A_STAB_EQ;IN; ADD1]
THEN MP_TAC SCS_5M2_EDGE_LE_2H0_IMP_0
THEN ASM_REWRITE_TAC[ ADD1;h0]
THEN MP_TAC LT_sqrt8_2h0
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`sqrt8 <= dist ((v:num->real^3) l,v (l + 1))/\ &2 * #1.26 < sqrt8==> &2 * #1.26 < dist (v l,v (l + 1))`)
THEN RESA_TAC
THEN STRIP_TAC
THEN DICH_TAC (9-3)
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l:num`;`v`;` l MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l+1:num`;`v`;` (l+1) MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`]
THEN MRESAL_TAC MOD_ADD_MOD[`l`;`1`;`5`][ARITH_RULE`~(5=0)/\ 1 MOD 5=1/\ 0+a=a`] THEN SYM_ASSUM_TAC
THEN STRIP_TAC
THEN MP_TAC SCS_5M3_STAB_DIAG_sqrt8
THEN RESA_TAC
THEN SCS_TAC
THEN REAL_ARITH_TAC);;




let STAB_5M3_SCS=prove(` scs_diag (scs_k_v39 scs_5M3) i j
==> is_scs_v39 (scs_stab_diag_v39 scs_5M3 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5M3 i j)`,
STRIP_TAC
THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5M3_IS_SCS;SCS_5M3_BASIC;K_SCS_5M3;
ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
THEN SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC);;

let BB_3T4_prime_IMP_scs_3T4=prove(`BBs_v39 scs_3T4_prime v
     ==>
    BBs_v39 (scs_3T4 ) v`,
REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`(3<=3)`;IN;K_SCS_3T4;K_SCS_3T4_prime;scs_prop_equ_v39;]
THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
THEN SCS_TAC
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC 0[`i`;`j`]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab;h0]
THEN REAL_ARITH_TAC);;

let MM_3T4_prime_IMP_MM_3T4=prove(`MMs_v39 scs_3T4_prime v ==> ~(MMs_v39 scs_3T4={})`,
STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_3T4_prime`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_3T4_prime`;`v`]
THEN ASM_SIMP_TAC[SCS_3T4_BASIC;SCS_3T4_prime_BASIC;SCS_3T4_IS_SCS;SCS_3T4_IS_SCS;
SCS_3T4_prime_IS_SCS;K_SCS_3T4;K_SCS_3T4_prime;IN;BB_3T4_prime_IMP_scs_3T4]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;

let SCS_3T4_prime_ARROW_MM_3T4=prove_by_refinement(`scs_arrow_v39 {scs_3T4_prime } { scs_3T4}`,
[ REPEAT GEN_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;

ASM_SIMP_TAC[SCS_3T4_IS_SCS];

DISJ_CASES_TAC(SET_RULE`(!s. s = scs_3T4_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_3T4_prime ==> MMs_v39 s = {}))`);

ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN EXISTS_TAC`scs_3T4`
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC (GEN_ALL MM_3T4_prime_IMP_MM_3T4)
THEN POP_ASSUM MP_TAC
THEN SET_TAC[]]);;

let BB_4M6_prime_IMP_scs_4M6=prove(`BBs_v39 scs_4M6_prime v
     ==>
    BBs_v39 (scs_4M6' ) v`,
REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4M6_prime;K_SCS_4M6;scs_prop_equ_v39;]
THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
THEN SCS_TAC
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC 1[`i`;`j`]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab;h0]
THEN REAL_ARITH_TAC);;









let MM_4M6_prime_IMP_MM_4M6=prove(`MMs_v39 scs_4M6_prime v ==> ~(MMs_v39 scs_4M6' ={})`,
STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_4M6_prime`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M6_prime`;`v`]
THEN ASM_SIMP_TAC[SCS_4M6_BASIC;SCS_4M6_prime_BASIC;SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;
SCS_4M6_prime_IS_SCS;K_SCS_4M6;K_SCS_4M6_prime;IN;BB_4M6_prime_IMP_scs_4M6]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;


let SCS_4M6_prime_ARROW_MM_4M6=prove_by_refinement(`scs_arrow_v39 {scs_4M6_prime } { scs_4M6'}`,
[ REPEAT GEN_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;

ASM_SIMP_TAC[SCS_4M6_IS_SCS];

DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M6_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M6_prime ==> MMs_v39 s = {}))`);

ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN EXISTS_TAC`scs_4M6'`
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC (GEN_ALL MM_4M6_prime_IMP_MM_4M6)
THEN POP_ASSUM MP_TAC
THEN SET_TAC[]]);;


let SCS_5M3_SLICE_02=prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 0 2 } { scs_prop_equ_v39 scs_3T4_prime 2, scs_prop_equ_v39 scs_4M6_prime 1}`,
[
MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_02;STAB_5M3_SCS;SCS_K_D_A_STAB_EQ;]
THEN EXISTS_TAC`0`
THEN EXISTS_TAC`2`
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_02]
THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
THEN REPEAT RESA_TAC;

REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC scs_inj
THEN ASM_SIMP_TAC[SCS_5M3_BASIC;SCS_3T4_prime_BASIC;J_SCS_4M6_prime;BASIC_HALF_SLICE_STAB;J_SCS_3T4_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4M6_prime_BASIC]
THEN STRIP_TAC;

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

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

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

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

SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[J_SCS_3T4_prime]]);;

let SCS_5M3_02_ARROW_3T4_4M6=prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 0 2 } {scs_3T4,  scs_4M6'}`,
[MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_3T4_prime 2, scs_prop_equ_v39 scs_4M6_prime 1}`
THEN ASM_REWRITE_TAC[SCS_5M3_SLICE_02;SET_RULE`{A,B}={A}UNION {B}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC;

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

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_4M6_prime}`
THEN ASM_REWRITE_TAC[SCS_4M6_prime_ARROW_MM_4M6]
THEN MRESAS_TAC PRO_EQU_ID1[`scs_4M6_prime`;`1`;`4`][SCS_4M6_prime_IS_SCS;K_SCS_4M6_prime;ARITH_RULE`(4 - 1 MOD 4)=3`]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M6_prime 1`;`3`][PROP_EQU_IS_SCS;SCS_4M6_prime_IS_SCS]
THEN DICH_TAC 0
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN REWRITE_TAC[]]);;
(************03***********)



let SCS_5M3_SLICE_03=prove_by_refinement(
`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 0 3 } {  scs_prop_equ_v39 scs_4M7_prime 1,scs_prop_equ_v39 scs_3T1_prime 1}`,
[

MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_03;STAB_5M3_SCS;SCS_K_D_A_STAB_EQ;]
THEN EXISTS_TAC`0`
THEN EXISTS_TAC`3`
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_03]
THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
THEN REPEAT RESA_TAC;


REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC scs_inj
THEN ASM_SIMP_TAC[SCS_5M3_BASIC;SCS_3T1_prime_BASIC;J_SCS_4M7_prime;BASIC_HALF_SLICE_STAB;J_SCS_3T1_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4M7_prime_BASIC]
THEN STRIP_TAC;


ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_4M7_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M3]
THEN ARITH_TAC;


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


ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T1_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M3;K_SCS_4M7_prime]
THEN ARITH_TAC;


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



SCS_TAC
THEN REAL_ARITH_TAC;


SCS_TAC
THEN REAL_ARITH_TAC;


SCS_TAC
THEN REAL_ARITH_TAC;


SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;


SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;


POP_ASSUM MP_TAC
THEN REWRITE_TAC[J_SCS_4M7_prime];

]);;

let BB_3T1_prime_IMP_scs_3T1=prove(
`BBs_v39 scs_3T1_prime v
     ==>
    BBs_v39 (scs_3T1 ) v`,
REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`((3<=3))`;IN;K_SCS_3T1_prime;K_SCS_3T1;scs_prop_equ_v39;]
THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
THEN SCS_TAC
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC 0[`i`;`j`]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab;h0]
THEN MP_TAC sqrt8_LE_CSTAB
THEN REAL_ARITH_TAC);;

let MM_3T1_prime_IMP_MM_3T1=prove(
`MMs_v39 scs_3T1_prime v ==> ~(MMs_v39 scs_3T1 ={})`,
STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_3T1_prime`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_3T1_prime`;`v`]
THEN ASM_SIMP_TAC[SCS_3T1_BASIC;SCS_3T1_prime_BASIC;SCS_3T1_IS_SCS;SCS_3T1_IS_SCS;
SCS_3T1_prime_IS_SCS;K_SCS_3T1;K_SCS_3T1_prime;IN;BB_3T1_prime_IMP_scs_3T1]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;



let SCS_3T1_prime_ARROW_MM_3T1=prove_by_refinement(`scs_arrow_v39 {scs_3T1_prime } { scs_3T1}`,
[ REPEAT GEN_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;

ASM_SIMP_TAC[SCS_3T1_IS_SCS];

DISJ_CASES_TAC(SET_RULE`(!s. s = scs_3T1_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_3T1_prime ==> MMs_v39 s = {}))`);

ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN EXISTS_TAC`scs_3T1`
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC (GEN_ALL MM_3T1_prime_IMP_MM_3T1)
THEN POP_ASSUM MP_TAC
THEN SET_TAC[]]);;



let BB_4M7_prime_IMP_scs_4M7=prove(`BBs_v39 scs_4M7_prime v
     ==>
    BBs_v39 (scs_4M7 ) v`,
REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4M7_prime;K_SCS_4M7;scs_prop_equ_v39;]
THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
THEN SCS_TAC
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC 1[`i`;`j`]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab;h0]
THEN REAL_ARITH_TAC);;


let MM_4M7_prime_IMP_MM_4M7=prove(
`MMs_v39 scs_4M7_prime v ==> ~(MMs_v39 scs_4M7 ={})`,
STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_4M7_prime`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M7_prime`;`v`]
THEN ASM_SIMP_TAC[SCS_4M7_BASIC;SCS_4M7_prime_BASIC;SCS_4M7_IS_SCS;SCS_4M7_IS_SCS;
SCS_4M7_prime_IS_SCS;K_SCS_4M7;K_SCS_4M7_prime;IN;BB_4M7_prime_IMP_scs_4M7]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;



let SCS_4M7_prime_ARROW_MM_4M7=prove_by_refinement(`scs_arrow_v39 {scs_4M7_prime } { scs_4M7}`,
[ REPEAT GEN_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;

ASM_SIMP_TAC[SCS_4M7_IS_SCS];

DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M7_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M7_prime ==> MMs_v39 s = {}))`);

ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN EXISTS_TAC`scs_4M7`
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC (GEN_ALL MM_4M7_prime_IMP_MM_4M7)
THEN POP_ASSUM MP_TAC
THEN SET_TAC[]]);;

let SCS_5M3_03_ARROW_3T1_4M7=prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 0 3 } {  scs_4M7,scs_3T1}`,
[
MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_4M7_prime 1, scs_prop_equ_v39 scs_3T1_prime 1}`
THEN ASM_REWRITE_TAC[SCS_5M3_SLICE_03;SET_RULE`{A,B}={A}UNION {B}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC;

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_4M7_prime}`
THEN ASM_REWRITE_TAC[SCS_4M7_prime_ARROW_MM_4M7]
THEN MRESAS_TAC PRO_EQU_ID1[`scs_4M7_prime`;`1`;`4`][SCS_4M7_prime_IS_SCS;K_SCS_4M7_prime;ARITH_RULE`(4 - 1 MOD 4)=3`]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M7_prime 1`;`3`][PROP_EQU_IS_SCS;SCS_4M7_prime_IS_SCS]
THEN DICH_TAC 0
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN REWRITE_TAC[];

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_3T1_prime}`
THEN ASM_REWRITE_TAC[SCS_3T1_prime_ARROW_MM_3T1]
THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T1_prime`;`1`;`3`][SCS_3T1_prime_IS_SCS;K_SCS_3T1_prime;ARITH_RULE`(3 - 1 MOD 3)=2`]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T1_prime 1`;`2`][PROP_EQU_IS_SCS;SCS_3T1_prime_IS_SCS]
THEN DICH_TAC 0
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN REWRITE_TAC[]]);;
(*************24**************)


let SCS_5M3_SLICE_24=prove_by_refinement(
`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 2 4 } {scs_prop_equ_v39 scs_3T1_prime 1,scs_prop_equ_v39 scs_4M8_prime 3}`,
[
MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_24;STAB_5M3_SCS;SCS_K_D_A_STAB_EQ;]
THEN EXISTS_TAC`2`
THEN EXISTS_TAC`4`
THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_24]
THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
THEN REPEAT RESA_TAC;

REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
THEN STRIP_TAC
THEN MATCH_MP_TAC scs_inj
THEN ASM_SIMP_TAC[SCS_5M3_BASIC;SCS_3T1_prime_BASIC;J_SCS_4M8_prime1;BASIC_HALF_SLICE_STAB;J_SCS_3T1_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4M8_prime_BASIC]
THEN STRIP_TAC;

ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T1_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M3]
THEN ARITH_TAC;

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

ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_4M8_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M3;K_SCS_4M8_prime]
THEN ARITH_TAC;

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

SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

SCS_TAC
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;

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


let BB_4M8_prime_IMP_scs_4M8=prove(`BBs_v39 scs_4M8_prime v
     ==>
    BBs_v39 (scs_4M8 ) v`,
REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4M8_prime;K_SCS_4M8;scs_prop_equ_v39;]
THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
THEN SCS_TAC
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC 1[`i`;`j`]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab;h0]
THEN REAL_ARITH_TAC);;


let MM_4M8_prime_IMP_MM_4M8=prove(
`MMs_v39 scs_4M8_prime v ==> ~(MMs_v39 scs_4M8 ={})`,
STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_4M8_prime`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8_prime`;`v`]
THEN ASM_SIMP_TAC[SCS_4M8_BASIC;SCS_4M8_prime_BASIC;SCS_4M8_IS_SCS;SCS_4M8_IS_SCS;
SCS_4M8_prime_IS_SCS;K_SCS_4M8;K_SCS_4M8_prime;IN;BB_4M8_prime_IMP_scs_4M8]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;



let SCS_4M8_prime_ARROW_MM_4M8=prove_by_refinement(`scs_arrow_v39 {scs_4M8_prime } { scs_4M8}`,
[ REPEAT GEN_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;

ASM_SIMP_TAC[SCS_4M8_IS_SCS];

DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M8_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M8_prime ==> MMs_v39 s = {}))`);

ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN EXISTS_TAC`scs_4M8`
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC (GEN_ALL MM_4M8_prime_IMP_MM_4M8)
THEN POP_ASSUM MP_TAC
THEN SET_TAC[]]);;


let SCS_5M3_24_ARROW_3T1_4M8=prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 2 4 } {  scs_3T1,scs_4M8}`,
[
MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{  scs_prop_equ_v39 scs_3T1_prime 1,scs_prop_equ_v39 scs_4M8_prime 3}`
THEN ASM_REWRITE_TAC[SCS_5M3_SLICE_24;SET_RULE`{A,B}={A}UNION {B}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC;

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

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_4M8_prime}`
THEN ASM_REWRITE_TAC[SCS_4M8_prime_ARROW_MM_4M8]
THEN MRESAS_TAC PRO_EQU_ID1[`scs_4M8_prime`;`3`;`4`][SCS_4M8_prime_IS_SCS;K_SCS_4M8_prime;ARITH_RULE`(4 - 3 MOD 4)=1`]
THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M8_prime 3`;`1`][PROP_EQU_IS_SCS;SCS_4M8_prime_IS_SCS]
THEN DICH_TAC 0
THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
THEN REWRITE_TAC[]]);;


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

let PROP_OPP_DIAG_5M3_03= prove_by_refinement(`scs_stab_diag_v39 scs_5M3 0 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_5M3 1 3)) 3 `,

[REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; scs_basic;SCS_K_D_A_STAB_EQ;scs_opp_v39]
THEN MATCH_MP_TAC scs_inj
THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_5M3_BASIC]
THEN STRIP_TAC;

MRESAL_TAC  STAB_5M3_SCS[`0`;`3`][K_SCS_5M3;scs_diag;ARITH_RULE`~(0 MOD 5 = 3 MOD 5) /\
      ~(SUC 0 MOD 5 = 3 MOD 5) /\
      ~(0 MOD 5 = SUC 3 MOD 5)`];

STRIP_TAC;

ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM]
THEN SET_TAC[];

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



let PROP_OPP_DIAG_5M3_02= prove_by_refinement(`scs_stab_diag_v39 scs_5M3 0 2= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_5M3 1 4)) 3 `,

[REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; scs_basic;SCS_K_D_A_STAB_EQ;scs_opp_v39]
THEN MATCH_MP_TAC scs_inj
THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_5M3_BASIC]
THEN STRIP_TAC;

MRESAL_TAC  STAB_5M3_SCS[`0`;`2`][K_SCS_5M3;scs_diag;ARITH_RULE`~(0 MOD 5 = 2 MOD 5) /\
      ~(SUC 0 MOD 5 = 2 MOD 5) /\
      ~(0 MOD 5 = SUC 2 MOD 5)`];

STRIP_TAC;

ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM]
THEN SET_TAC[];

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

let SET_STAB_5M3=prove(`{ scs_stab_diag_v39 scs_5M3 i j| scs_diag 5 i j }= { scs_stab_diag_v39 scs_5M3 (i MOD 5) (j  MOD 5)| scs_diag 5 (i MOD 5) (j  MOD 5) }`,
 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(5=0)`;]
THEN MRESAL_TAC STAB_MOD[`scs_5M3`][SCS_5M3_IS_SCS;K_SCS_5M3]);;

let EXPAND_STAB_DIAG_5M3=prove(`{scs_stab_diag_v39 scs_5M3 (i MOD 5) (j MOD 5) | i MOD 5 =
                                                  (j MOD 5 + 2) MOD 5 \/
                                                  j MOD 5 =
                                                  (i MOD 5 + 2) MOD 5}=
{scs_stab_diag_v39 scs_5M3 (i+2) i| i<5} `,
ASM_SIMP_TAC[EXPAND_STAB_DIAG_5;SCS_5M3_IS_SCS;K_SCS_5M3]);;

let SET_EQ_DIAG_STAB_5M3= prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 i j | scs_diag 5 i j}
 {scs_stab_diag_v39 scs_5M3 0 2, scs_stab_diag_v39 scs_5M3 0 3, scs_stab_diag_v39
                                                                scs_5M3
                                                                2
                                                                4}`,
[
ONCE_REWRITE_TAC[SET_STAB_5M3]
THEN REWRITE_TAC[DIAG_EQ_ADD5;EXPAND_STAB_DIAG_5I3;EXPAND_STAB_DIAG_5M3]
THEN REWRITE_TAC[ARITH_RULE`i<5<=> i=0\/i=1\/i=2\/i=3\/i=4`;
SET_RULE`{A,B,C}
= 
{A}UNION
{B}UNION
{C}UNION
{B}UNION
{A}
`;SET_RULE`{scs_stab_diag_v39 scs_5M3 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
= 
{scs_stab_diag_v39 scs_5M3 (0 + 2) 0} UNION
{scs_stab_diag_v39 scs_5M3 (1 + 2) 1} UNION
{scs_stab_diag_v39 scs_5M3 (2 + 2) 2} UNION
{scs_stab_diag_v39 scs_5M3 (3 + 2) 3} UNION
{scs_stab_diag_v39 scs_5M3 (4 + 2) 4} 
`;]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC;

REWRITE_TAC[ARITH_RULE`0+2=2`;STAB_SYM]
THEN MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC  STAB_5M3_SCS[`2`;`0`][scs_diag;K_SCS_5M3;ARITH_RULE`~(2 MOD 5 = 0 MOD 5) /\
      ~(SUC 2 MOD 5 = 0 MOD 5) /\
      ~(2 MOD 5 = SUC 0 MOD 5)`];

MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC;

REWRITE_TAC[ARITH_RULE`1+2=3`;STAB_SYM;PROP_OPP_DIAG_5M3_03]
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_5M3 1 3)}`
THEN STRIP_TAC;

MATCH_MP_TAC (GEN_ALL YXIONXL2)
THEN EXISTS_TAC`5`
THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(5<=3)`;K_SCS_5M3]
THEN MRESAL_TAC  STAB_5M3_SCS[`1`;`3`][scs_diag;K_SCS_5M3;ARITH_RULE`~(1 MOD 5 = 3 MOD 5) /\
      ~(SUC 1 MOD 5 = 3 MOD 5) /\
      ~(1 MOD 5 = SUC 3 MOD 5)`];

MATCH_MP_TAC(GEN_ALL YXIONXL3)
THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_5M3 1 3)`
THEN MRESAL_TAC  STAB_5M3_SCS[`1`;`3`][scs_diag;K_SCS_5M3;ARITH_RULE`~(1 MOD 5 = 3 MOD 5) /\
      ~(SUC 1 MOD 5 = 3 MOD 5) /\
      ~(1 MOD 5 = SUC 3 MOD 5)`];

MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC;

REWRITE_TAC[ARITH_RULE`2+2=4`;STAB_SYM]
THEN MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC  STAB_5M3_SCS[`2`;`4`][scs_diag;K_SCS_5M3;ARITH_RULE`~(2 MOD 5 = 4 MOD 5) /\
      ~(SUC 2 MOD 5 = 4 MOD 5) /\
      ~(2 MOD 5 = SUC 4 MOD 5)`];

MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC;

REWRITE_TAC[ARITH_RULE`3+2=5`;STAB_SYM]
THEN MRESAL_TAC STAB_MOD[`scs_5M3`;`5`;`3`][SCS_5M3_IS_SCS;K_SCS_5M3;ARITH_RULE`5 MOD 5=0/\ 3 MOD 5=3`]
THEN SYM_ASSUM_TAC
THEN REWRITE_TAC[ARITH_RULE`3+2=5`;STAB_SYM]
THEN MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC  STAB_5M3_SCS[`3`;`0`][scs_diag;K_SCS_5M3;ARITH_RULE`~(3 MOD 5 = 0 MOD 5) /\
      ~(SUC 3 MOD 5 = 0 MOD 5) /\
      ~(3 MOD 5 = SUC 0 MOD 5)`];

REWRITE_TAC[ARITH_RULE`4+2=6`;]
THEN MRESAL_TAC STAB_MOD[`scs_5M3`;`6`;`4`][SCS_5M3_IS_SCS;K_SCS_5M3;ARITH_RULE`6 MOD 5=1/\ 4 MOD 5=4`]
THEN SYM_ASSUM_TAC
THEN REWRITE_TAC[PROP_OPP_DIAG_5M3_02];

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_5M3 1 4)}`
THEN STRIP_TAC;

MATCH_MP_TAC (GEN_ALL YXIONXL2)
THEN EXISTS_TAC`5`
THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(5<=3)`;K_SCS_5M3]
THEN MRESAL_TAC  STAB_5M3_SCS[`1`;`4`][scs_diag;K_SCS_5M3;ARITH_RULE`~(1 MOD 5 = 4 MOD 5) /\
      ~(SUC 1 MOD 5 = 4 MOD 5) /\
      ~(1 MOD 5 = SUC 4 MOD 5)`];

MATCH_MP_TAC(GEN_ALL YXIONXL3)
THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_5M3 1 4)`
THEN MRESAL_TAC  STAB_5M3_SCS[`1`;`4`][scs_diag;K_SCS_5M3;ARITH_RULE`~(1 MOD 5 = 4 MOD 5) /\
      ~(SUC 1 MOD 5 = 4 MOD 5) /\
      ~(1 MOD 5 = SUC 4 MOD 5)`]]);;


let SET_EQ_DIAG_STAB_5M3_IMP_SCS_3_4=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 i j | scs_diag 5 i j}
{scs_4M6',scs_4M7,scs_4M8,scs_3T1,scs_3T4}`,
MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_stab_diag_v39 scs_5M3 0 2, scs_stab_diag_v39 scs_5M3 0 3, scs_stab_diag_v39
                                                                scs_5M3
                                                                2
                                                                4}`
THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_5M3;SET_RULE`{scs_4M6', scs_4M7, scs_4M8, scs_3T1, scs_3T4}= {scs_3T4,  scs_4M6'}UNION{scs_4M7,scs_3T1}UNION{  scs_3T1,scs_4M8}`]
THEN REWRITE_TAC[SET_RULE`{A,B,C}={A}UNION{B}UNION{C}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN REWRITE_TAC[SCS_5M3_02_ARROW_3T4_4M6]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN REWRITE_TAC[SCS_5M3_03_ARROW_3T1_4M7;SCS_5M3_24_ARROW_3T1_4M8]);;
(**************)

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

let B_LE_CSTAB_5M2=prove(`
(!i. scs_b_v39 scs_5M2 i (SUC i) <= cstab)/\
(!i. scs_a_v39 scs_5M2 i (SUC i) = &2)
`,
SCS_TAC
THEN SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;h0;cstab]
THEN REPEAT RESA_TAC
THEN MRESAS_TAC PSORT_MOD[`5`;`i`;`SUC i`][ARITH_RULE`~(5=0)`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
THEN RESA_TAC
THEN SCS_TAC
THEN REAL_ARITH_TAC);;


let B_LE_CSTAB_5M2_A_LT_B=prove(`
(!i. &2 < scs_b_v39 scs_5M2 i (SUC i))
`,
SCS_TAC
THEN SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;h0;cstab]
THEN REPEAT RESA_TAC
THEN MRESAS_TAC PSORT_MOD[`5`;`i`;`SUC i`][ARITH_RULE`~(5=0)`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
THEN RESA_TAC
THEN SCS_TAC
THEN REAL_ARITH_TAC);;






let CARD_SCS_M_5M2=prove(`CARD (scs_M scs_5M2) <= 1`,
ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<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 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
THENL[

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_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_M_5T1=prove(`scs_M scs_5T1={}`,
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 ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~((&2 * #1.26 < &2 \/ &2 < &2))`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]);;


(******ADD PROPERTY OF LEMMA JCYFMRP************)

let JCYFMRP_V1 = prove_by_refinement(`main_nonlinear_terminal_v11
==>(!s (v:num->real^3) i.
  3< scs_k_v39 s/\ 
  is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
  (  dist(v i,v (i+1)) = &2) /\
  CARD (scs_M s) <= 1 /\
  (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j) /\ &4 * h0 < scs_b_v39 s i j)) /\
(!i. scs_a_v39 s i (i+1)< scs_b_v39 s i (i+1)) 
==>
  (?i1. ~(i1 MOD scs_k_v39 s IN scs_M s)/\ dist(v i1, v (i1+1)) = &2))`,
[STRIP_TAC
THEN REPEAT GEN_TAC
THEN ABBREV_TAC`k= scs_k_v39 s`
THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
THEN REPEAT RESA_TAC
THEN MP_TAC(SET_RULE`i MOD k IN scs_M s\/ ~(i MOD k IN scs_M s)`)
THEN RESA_TAC;

SUBGOAL_THEN`scs_M s={i MOD k}`ASSUME_TAC;

MRESAS_TAC CARD_SUBSET_LE[`{i MOD k}`;`scs_M s`][Jlxfdmj.FINITE_SCS_M;SET_RULE`a IN A==> {a} SUBSET A`;Geomdetail.CARD_SING];

MRESA_TAC Jlxfdmj.SCS_M_EQ_1[`i MOD k`;`s`]
THEN THAYTHES_TAC 0[`SUC i`][SET_RULE`(SUC i MOD k = i MOD k)<=> (i MOD k = SUC i MOD k)`;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`3<k==> 1<k`]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN REWRITE_TAC[ARITH_RULE`SUC i= i+1/\ (i + 1) + 1= i+2`]
THEN REPEAT STRIP_TAC
THEN MP_TAC Tfitskc.TFITSKC
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`v`;`i`]
THEN DICH_TAC 0
THEN THAYTHEL_ASM_TAC(17-13)[`i+2`][ARITH_RULE`(i+2)+1=i+3`]
THEN THAYTHE_TAC 0[`i`]
THEN MP_TAC Jlxfdmj.SCS_A_2
THEN RESA_TAC
THEN THAYTHE_TAC 0[`i`]
THEN MP_TAC(REAL_ARITH`scs_a_v39 s i (i + 1) < scs_b_v39 s i (i + 1)
/\ &2<= scs_a_v39 s i (i + 1)
==> &2 < scs_b_v39 s i (i + 1)`)
THEN RESA_TAC
THEN STRIP_TAC
THEN EXISTS_TAC`SUC i`
THEN ASM_SIMP_TAC[Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`3<k==> 1<k`;SET_RULE`~(a IN {b})<=> ~(b=a)`;ARITH_RULE`SUC i= i+1/\ (i + 1) + 1= i+2`];

EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]]);;



let JCYFMRP_V2 = prove_by_refinement(
`main_nonlinear_terminal_v11
==>(!s (v:num->real^3) i.
  3< scs_k_v39 s/\ 
  is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
  (  dist(v i,v (i+1)) = &2) /\
  CARD (scs_M s) <= 1 /\
  (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j) /\ &4 * h0 < scs_b_v39 s i j)) /\
(!i. scs_a_v39 s i (i+1)< scs_b_v39 s i (i+1)) 
==>
  (?i1. scs_b_v39 s i1 (SUC i1) <= &2 * h0/\ scs_a_v39 s i1 (SUC i1) = &2/\ dist(v i1, v (i1+1)) = &2))`,
[STRIP_TAC
THEN REPEAT GEN_TAC
THEN ABBREV_TAC`k= scs_k_v39 s`
THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
THEN REPEAT RESA_TAC
THEN MP_TAC(SET_RULE`i MOD k IN scs_M s\/ ~(i MOD k IN scs_M s)`)
THEN RESA_TAC;

SUBGOAL_THEN`scs_M s={i MOD k}`ASSUME_TAC;

MRESAS_TAC CARD_SUBSET_LE[`{i MOD k}`;`scs_M s`][Jlxfdmj.FINITE_SCS_M;SET_RULE`a IN A==> {a} SUBSET A`;Geomdetail.CARD_SING];

MRESA_TAC Jlxfdmj.SCS_M_EQ_1[`i MOD k`;`s`]
THEN THAYTHES_TAC 0[`SUC i`][SET_RULE`(SUC i MOD k = i MOD k)<=> (i MOD k = SUC i MOD k)`;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`3<k==> 1<k`]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN REWRITE_TAC[ARITH_RULE`SUC i= i+1/\ (i + 1) + 1= i+2`]
THEN REPEAT STRIP_TAC
THEN MP_TAC Tfitskc.TFITSKC
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`v`;`i`]
THEN DICH_TAC 0
THEN THAYTHEL_ASM_TAC(17-13)[`i+2`][ARITH_RULE`(i+2)+1=i+3`]
THEN THAYTHE_TAC 0[`i`]
THEN MP_TAC Jlxfdmj.SCS_A_2
THEN RESA_TAC
THEN THAYTHE_TAC 0[`i`]
THEN MP_TAC(REAL_ARITH`scs_a_v39 s i (i + 1) < scs_b_v39 s i (i + 1)
/\ &2<= scs_a_v39 s i (i + 1)
==> &2 < scs_b_v39 s i (i + 1)`)
THEN RESA_TAC
THEN STRIP_TAC
THEN EXISTS_TAC`SUC i`
THEN ASM_SIMP_TAC[Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`3<k==> 1<k`;SET_RULE`~(a IN {b})<=> ~(b=a)`;ARITH_RULE`SUC i= i+1/\ (i + 1) + 1= i+2`];

EXISTS_TAC`i:num`
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(ARITH_RULE`CARD (scs_M s)<= 1==> CARD (scs_M s)= 0\/ CARD (scs_M s)=1`)
THEN RESA_TAC;

MP_TAC Jlxfdmj.SCS_M_EQ_0
THEN RESA_TAC;

MRESAS_TAC Local_lemmas.FINITE_CARD1_IMP_SINGLETON[`scs_M s`][Jlxfdmj.FINITE_SCS_M;SET_RULE`~(a IN {x})<=> ~(a=x)`]
THEN STRIP_TAC
THEN MP_TAC Jlxfdmj.SCS_M_EQ_1
THEN RESA_TAC
THEN THAYTHE_TAC 0[`i`]]);;




let JCYFMRP_V3=prove(`main_nonlinear_terminal_v11
==>(!s (v:num->real^3).
  3< scs_k_v39 s/\ 
  is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
  CARD (scs_M s) <= 1 /\
  (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j) /\ &4 * h0 < scs_b_v39 s i j)) /\
(!i. scs_a_v39 s i (i+1)< scs_b_v39 s i (i+1)) /\
(!i. scs_a_v39 s i (SUC i) = &2) 
==>
  (?i. scs_b_v39 s i (SUC i) <= &2 * h0/\ scs_a_v39 s i (SUC i) = &2/\ dist(v i, v (i+1)) = &2))`,
REPEAT RESA_TAC
THEN MP_TAC Jcyfmrp.JCYFMRP
THEN RESA_TAC
THEN THAYTHE_TAC 0[`s`;`v`]
THEN POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[]
THEN STRIP_TAC
THEN MP_TAC JCYFMRP_V2
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN THAYTHE_TAC 0[`s`;`v`;`i`]);;

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

let ARC_222=prove(`arclength (&2) (&2) (&2)= pi/ &3`,
MRESAS_TAC Trigonometry.PQQDENV[`&2`;`&2`;`&2`][REAL_ARITH`&0 < &2 /\ &0 < &2 /\ &0 <= &2 /\ &2 <= &2 + &2/\ (&2 * &2 + &2 * &2 - &2 * &2) / (&2 * &2 * &2)= &1/ &2`;Nonlinear_lemma.ACS_2]);;


let xrr_le_1553=prove(` v IN ball_annulus/\ u IN ball_annulus/\ w IN ball_annulus
/\ ~collinear {vec 0, v, u}
/\ dist(v,w)= &2/\ dist(w,u)= &2
==>
xrr (norm v) (norm u) (norm(v-u))<= #15.53`,
REPEAT RESA_TAC
THEN MRESA_TAC Counting_spheres.ckq_in_ball_annulus[`v`]
THEN MRESA_TAC Counting_spheres.ckq_in_ball_annulus[`u`]
THEN MRESA_TAC Counting_spheres.ckq_in_ball_annulus[`w`]
THEN MRESA_TAC Trigonometry2.ARCV_INEQUALTY[`vec 0:real^3`;`v`;`u`;`w`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v`;`w`;`&2`][REAL_ARITH`&2 < &4 /\ &2 <= &2 `;ARC_222]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`w`;`u`;`&2`][REAL_ARITH`&2 < &4 /\ &2 <= &2 `;ARC_222]
THEN MP_TAC(REAL_ARITH`arcV (vec 0) v u <= arcV (vec 0) v w + arcV (vec 0) w u
/\ arcV (vec 0) v w <= pi / &3/\ arcV (vec 0) w u <= pi / &3
==>  arcV (vec 0:real^3) v u<= &2 * pi/ &3`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`v`;`u`]
THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- a= --a:real^3`;NORM_NEG]
THEN MRESAL_TAC th3[`v`;`vec 0:real^3`;`u:real^3`][GSYM dist;VECTOR_ARITH`v - u = vec 0
<=> v=u:real^3`]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
THEN RESA_TAC
THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`v`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A:real^3`]
THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`u`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A:real^3`]
THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`v`;`u:real^3`][VECTOR_ARITH`A- vec 0=A:real^3`]
THEN MRESAL_TAC Collect_geom2.NOT_COL_EQ_UPS_X_POS[`vec 0:real^3`;`v`;`u`][dist;VECTOR_ARITH`vec 0- a= --a:real^3`;NORM_NEG]
THEN MRESAL_TAC arclength_xrr[`norm v`;`norm u`;`norm (v- u)`][REAL_ARITH`a*a= a pow 2`]
THEN STRIP_TAC
THEN MRESAL_TAC ACS_NEG[`&1/ &2`][REAL_ARITH`-- &1 <= &1 / &2 /\ &1 / &2 <= &1/\ pi - pi / &3= &2* pi/ &3`;Nonlinear_lemma.ACS_2]
THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`norm v`;`norm u`;`norm (v-u)`][REAL_ARITH`a*a= a pow 2`]
THEN MP_TAC(REAL_ARITH`&0 < xrr (norm v) (norm u) (norm (v - u))/\
xrr (norm v) (norm u) (norm (v - u)) < &16
==> abs (&1 - xrr (norm v) (norm u) (norm (v - u:real^3)) / &8) <= &1`)
THEN RESA_TAC
THEN MRESAL_TAC ACS_MONO_LE_EQ[`&1 - xrr (norm v) (norm u) (norm (v - u)) / &8`;`--( &1/ &2)`][REAL_ARITH`abs (--(&1 / &2)) <= &1`]
THEN DICH_TAC 0
THEN REAL_ARITH_TAC);;


let xrr_le_1553_BB=prove(`BBs_v39 s v /\ dist(v i, v (i+1))= &2/\ dist( v (i+1), v(i+2))= &2 /\ ~(collinear{vec 0 , v i, v (i+2)})
==> xrr (norm (v i)) (norm (v (i+2))) (norm(v i- v (i+2)))<= #15.53 `,
STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL xrr_le_1553)
THEN EXISTS_TAC`(v:num->real^3) (i+1)`
THEN ASM_SIMP_TAC[]
THEN MRESA_TAC Nuxcoea.WL_IN_BALL_ANNULUS[`s`;`v`;`i`]
THEN MRESA_TAC Nuxcoea.WL_IN_BALL_ANNULUS[`s`;`v`;`i+1`]
THEN MRESA_TAC Nuxcoea.WL_IN_BALL_ANNULUS[`s`;`v`;`i+2`]);;


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


let J_SCS_5M2_0=prove(`(!i j. ~scs_J_v39 scs_5M2 j i)`,
SCS_TAC);;


let SCS_5M2_IMP_SCS_5T1= prove_by_refinement(`main_nonlinear_terminal_v11
==>(!v. 
    v IN MMs_v39 scs_5M2 /\
    (!i j. scs_diag 5 i j ==>   cstab < dist(v i,v j)) ==>
    ~(MMs_v39 (scs_5T1)={}))`,
[
REWRITE_TAC[IN;SET_RULE`~(A={})<=> ?a. a IN A`]
THEN REPEAT STRIP_TAC
THEN MP_TAC SCS_5M2_IS_SCS
THEN STRIP_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`]
THEN ASSUME_TAC SCS_5M2_BASIC
THEN ASSUME_TAC K_SCS_5M2
THEN ASSUME_TAC SCS_5T1_BASIC
THEN ASSUME_TAC K_SCS_5T1
THEN ASSUME_TAC SCS_5T1_IS_SCS
THEN MP_TAC Rrcwnsj.RRCWNSJ
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_5M2`;`v`][ARITH_RULE`3<5`;h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2]
THEN MP_TAC JCYFMRP_V3
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_5M2`;`v`][ARITH_RULE`3<5`;h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2;IN;CARD_SCS_M_5M2;GSYM ADD1;B_LE_CSTAB_5M2_A_LT_B]
THEN MP_TAC Jlxfdmj.JLXFDMJ
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_5M2`;`v`;`i`][ARITH_RULE`3<5`;h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2;CARD_SCS_M_5M2;SCS_M_5M2;IN_SING;]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[IN;GSYM ADD1;B_LE_CSTAB_5M2;B_LE_CSTAB_5M2_A_LT_B]
THEN STRIP_TAC
THEN ABBREV_TAC`V=(IMAGE (v:num->real^3) (:num))`
THEN ABBREV_TAC`E=(IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num))`
THEN ABBREV_TAC`FF=IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
THEN SUBGOAL_THEN`dist((v:num->real^3) 0, v 1)= &2`ASSUME_TAC;



ASSUME_TAC(ARITH_RULE`3<5/\ 0+1=1/\ 0+5-1=4`)
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`5`;`scs_5M2`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`0`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`1`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`2`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`3`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`4`;`v:num->real^3`]
THEN MRESAL_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`scs_5M2`;`FF`;`v (0)`;`v`;`0`;`5`][]
THEN MRESA_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v 0`]
THEN THAYTHE_TAC 0[`v 4`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v 0) (v 1) (v 4) <= pi
==> azim (vec 0) ((v:num->real^3) 0) (v 1) (v 4) = pi\/ azim (vec 0) (v 0) (v 1) (v 4) < pi`)
THEN RESA_TAC;






DICH_TAC(29-10)
THEN REWRITE_TAC[scs_generic]
THEN RESA_TAC
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_5M2`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v 1`;`v 4`;`V`]
THEN THAYTHEL_ASM_TAC 0[`v 1`;`v 4`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Uxckfpe.ARITH_5_TAC]
THEN SUBGOAL_THEN`(!j. ~(j MOD 5 = 4 MOD 5) ==> ~collinear {vec 0, v 4, (v:num->real^3)j})`ASSUME_TAC
;


REPEAT RESA_TAC
THEN DICH_TAC 0
THEN THAYTHE_TAC 1[`v 4`;`v j`]
THEN MATCH_DICH_TAC 0
THEN REWRITE_TAC[SET_RULE`a IN {b,a}`]
THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
;

THAYTHEL_ASM_TAC (33-30)[`4+1`;`0`][ARITH_RULE`( 4+1) MOD 5 = 0 MOD 5`]
THEN THAYTHEL_ASM_TAC 0[`4+2`;`1`][ARITH_RULE`( 4+2) MOD 5 = 1 MOD 5`]
THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v 0`;`v 1`;`(v:num->real^3) 4`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
THEN STRIP_TAC
THEN MRESA_TAC Iunbuig.coplanar_aff_gt_simple[`scs_5M2`;`5`;`v`;`4`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN STRIP_TAC
THEN SUBGOAL_THEN`(!i. scs_diag 5 0 i ==> scs_a_v39 scs_5M2 0 i < dist ((v:num->real^3) 0,v i))`ASSUME_TAC;


REPEAT RESA_TAC
THEN THAYTHE_TAC(38-2)[`0`;`i'`]
THEN MP_TAC h0_LT_B_SCS_5M2
THEN STRIP_TAC
THEN THAYTHE_TAC 0[`0`;`i'`]
THEN DICH_TAC 0
THEN DICH_TAC 1
THEN REAL_ARITH_TAC;

MRESAL_TAC MMS_IMP_BBPRIME[`scs_5M2`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
THEN MRESAL_TAC JKQEWGV2[`scs_5M2`;`v`][LET_DEF;LET_END_DEF;scs_generic]
THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
THEN RESA_TAC
THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) 0) V E)`ASSUME_TAC
;

REPEAT RESA_TAC
THEN DICH_TAC 3
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`v1:real^3`
THEN EXISTS_TAC`(v:num->real^3)0`
THEN ASM_REWRITE_TAC[]
;



MRESAS_TAC NUXCOEAv2[`scs_5M2`;`5`;`v`;`0`;`4`][ARITH_RULE`SUC 0=1/\ SUC 4 MOD 5 = 0 MOD 5`;h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2;J_SCS_5M2_0]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN MATCH_MP_TAC(SET_RULE`(A==> (B/\A1==>C)==>D)==> (A==>(B/\ A1/\A==>C)==>D)`)
THEN STRIP_TAC
THEN SCS_TAC
THEN THAYTHES_TAC(43-12)[`4`][ARITH_RULE`~(4 MOD 5=0)/\ SUC A= A+1`;h0]
THEN REAL_ARITH_TAC;





ASSUME_TAC(ARITH_RULE`1+1=2/\ 1+5-1=5`)
THEN MRESAL_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`scs_5M2`;`FF`;`v (1)`;`v`;`1`;`5`][]
THEN MRESA_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v 1`]
THEN THAYTHE_TAC 0[`v 0`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v 1) (v 2) (v 0) <= pi
==> azim (vec 0) ((v:num->real^3) 1) (v 2) (v 0) = pi\/ azim (vec 0) (v 1) (v 2) (v 0) < pi`)
THEN RESA_TAC;






DICH_TAC(34-10)
THEN REWRITE_TAC[scs_generic]
THEN RESA_TAC
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_5M2`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v 2`;`v 0`;`V`]
THEN THAYTHEL_ASM_TAC 0[`v 2`;`v 0`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Uxckfpe.ARITH_5_TAC]
THEN SUBGOAL_THEN`(!j. ~(j MOD 5 = 0 MOD 5) ==> ~collinear {vec 0, v 0, (v:num->real^3)j})`ASSUME_TAC
;


REPEAT RESA_TAC
THEN DICH_TAC 0
THEN THAYTHE_TAC 1[`v 0`;`v j`]
THEN MATCH_DICH_TAC 0
THEN REWRITE_TAC[SET_RULE`a IN {b,a}`]
THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
;

MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v 1`;`v 2`;`(v:num->real^3) 0`]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
THEN STRIP_TAC
THEN MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`scs_5M2`;`5`;`v`;`0`][ARITH_RULE`0+2=2`]THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN STRIP_TAC
THEN SUBGOAL_THEN`(!i. scs_diag 5 1 i ==> scs_a_v39 scs_5M2 1 i < dist ((v:num->real^3) 1,v i))`ASSUME_TAC;


REPEAT RESA_TAC
THEN THAYTHE_TAC(41-2)[`1`;`i'`]
THEN MP_TAC h0_LT_B_SCS_5M2
THEN STRIP_TAC
THEN THAYTHE_TAC 0[`1`;`i'`]
THEN DICH_TAC 0
THEN DICH_TAC 1
THEN REAL_ARITH_TAC;

MRESAL_TAC MMS_IMP_BBPRIME[`scs_5M2`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
THEN MRESAL_TAC JKQEWGV2[`scs_5M2`;`v`][LET_DEF;LET_END_DEF;scs_generic]
THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
THEN RESA_TAC
THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) 1) V E)`ASSUME_TAC
;

REPEAT RESA_TAC
THEN DICH_TAC 3
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`v1:real^3`
THEN EXISTS_TAC`(v:num->real^3)1`
THEN ASM_REWRITE_TAC[]
;



MRESAS_TAC NUXCOEAv2[`scs_5M2`;`5`;`v`;`1`;`2`][ARITH_RULE`SUC 1=2/\ SUC 4 MOD 5 = 0 MOD 5`;h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2;J_SCS_5M2_0]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN THAYTHEL_TAC(45-35)[`5`;`0`][ARITH_RULE`5 MOD 5 = 0 MOD 5`]
THEN MATCH_MP_TAC(SET_RULE`(A==> (B/\A1==>C)==>D)==> (A==>(B/\ A1/\A==>C)==>D)`)
THEN STRIP_TAC
THEN SCS_TAC
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN THAYTHES_TAC(46-12)[`1`][ARITH_RULE`~(1 MOD 5=0)/\ SUC A= A+1`;h0]
THEN REAL_ARITH_TAC;


MP_TAC Iunbuig.IUNBUIG
THEN RESA_TAC
THEN MATCH_DICH_TAC 0
THEN EXISTS_TAC`scs_5M2`
THEN EXISTS_TAC`FF:real^3#real^3->bool`
THEN ASM_SIMP_TAC[h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2;GSYM ADD1]
THEN SCS_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`a<=a`;interior_angle1;GSYM ivs_rho_node1]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_5M2`]
THEN THAYTHEL_TAC 0[`5`;`0`][ARITH_RULE`5 MOD 5 = 0 MOD 5`]
THEN THAYTHEL_ASM_TAC (35-13)[`3`][ARITH_RULE`~(3 MOD 5= 0)/\ SUC 3=4`]
THEN THAYTHEL_ASM_TAC (0)[`4`][ARITH_RULE`~(4 MOD 5= 0)/\ SUC 4=5`]
THEN THAYTHEL_ASM_TAC (0)[`1`][ARITH_RULE`~(1 MOD 5= 0)/\ SUC 1=2`]
THEN THAYTHEL_ASM_TAC (0)[`2`][ARITH_RULE`~(2 MOD 5= 0)/\ SUC 2=3`]
THEN DICH_TAC (39-10)
THEN REWRITE_TAC[scs_generic]
THEN RESA_TAC
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_5M2`]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v 0`;`v 3`;`V`]
THEN THAYTHEL_ASM_TAC 0[`v 3`;`v 0`][SET_RULE`a IN {b,a}`;BB_VV_FUN_EQ;Uxckfpe.ARITH_5_TAC]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v 1`;`v 3`;`V`]
THEN THAYTHEL_ASM_TAC 0[`v 1`;`v 3`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Uxckfpe.ARITH_5_TAC]
THEN MRESAL_TAC xrr_le_1553_BB[`scs_5M2`;`v`;`3`][ARITH_RULE`3+1=4/\ 3+2=5`]
THEN MRESAL_TAC xrr_le_1553_BB[`scs_5M2`;`v`;`1`][ARITH_RULE`1+1=2/\ 1+2=3`;GSYM dist]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN DICH_TAC 1
THEN REWRITE_TAC[xrr;dist]
THEN REAL_ARITH_TAC
;


SUBGOAL_THEN`!j. dist ((v:num->real^3) j,v (SUC j)) = &2`ASSUME_TAC
;

GEN_TAC
THEN MP_TAC(SET_RULE`~(j MOD 5 = 0) \/ (j MOD 5 = 0)`)
THEN RESA_TAC;


MATCH_DICH_TAC (18-13)
THEN ASM_REWRITE_TAC[];


MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_5M2`]
THEN THAYTHEL_ASM_TAC 0[`j`;`0`][ARITH_RULE`0 MOD 5=0`]
THEN THAYTHES_TAC 0[`SUC j`;`SUC 0`][ARITH_RULE`~(5=0)/\ SUC i= 1+i/\ 0 MOD 5=0`;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN ASM_REWRITE_TAC[ARITH_RULE`1+0=1`];




MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN REWRITE_TAC[IN;SET_RULE`~(A={})<=> ?a. a IN A`]
THEN STRIP_TAC
THEN MATCH_DICH_TAC 0
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_5M2`
THEN ASM_SIMP_TAC[SCS_M_5M2]
THEN STRIP_TAC
;



DICH_TAC(18-4)
THEN REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(5<=3))`;IN;K_SCS_4M8_prime;K_SCS_4M8;scs_prop_equ_v39;]
THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
THEN SCS_TAC
THEN REWRITE_TAC[ARITH_RULE`~(5<=3)`];

REPEAT STRIP_TAC
;


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

THAYTHE_TAC 2[`i'`;`j`]
;

MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`]
THEN MP_TAC(SET_RULE`SUC i' MOD 5 = j MOD 5\/ ~(SUC i' MOD 5 = j MOD 5)`)
THEN RESA_TAC;


MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j:num`;`v`;` SUC i'`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`;]
THEN REAL_ARITH_TAC;


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


MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` SUC j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`;]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC;


THAYTHEL_TAC (25-2)[`i'`;`j`][scs_diag]
THEN DICH_TAC 0
THEN REAL_ARITH_TAC;



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

THAYTHE_TAC 2[`i'`;`j`]
;



MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`]
THEN MP_TAC(SET_RULE`SUC i' MOD 5 = j MOD 5\/ ~(SUC i' MOD 5 = j MOD 5)`)
THEN RESA_TAC;


MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j:num`;`v`;` SUC i'`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`;]
THEN REAL_ARITH_TAC;



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


MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` SUC j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`;]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN REAL_ARITH_TAC;

THAYTHE_TAC (25-20)[`i'`;`j`]
THEN DICH_TAC 0
THEN MP_TAC(SET_RULE`psort 5 (i',j) = 0,1\/ ~(psort 5 (i',j) = 0,1)`)
THEN RESA_TAC;


MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`1`;`j`;`0`;`5`][PSORT_5_EXPLICIT];


DICH_TAC (28-23)
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[ARITH_RULE`1= 1+0`]
THEN ASM_SIMP_TAC[ARITH_RULE`SUC i= 1+i`;ARITH_RULE`~(5=0)/\ SUC i= 1+i/\ 0 MOD 5=0`;Ocbicby.MOD_EQ_MOD_SHIFT];


DICH_TAC (28-24)
THEN ASM_REWRITE_TAC[]
THEN ONCE_REWRITE_TAC[ARITH_RULE`1= 1+0`]
THEN ASM_SIMP_TAC[ARITH_RULE`SUC i= 1+i`;ARITH_RULE`~(5=0)/\ SUC i= 1+i/\ 0 MOD 5=0`;Ocbicby.MOD_EQ_MOD_SHIFT];

REWRITE_TAC[h0]
THEN REAL_ARITH_TAC;


SCS_TAC
THEN REAL_ARITH_TAC;

]);;


let HIJ_STEP_1=prove_by_refinement(`main_nonlinear_terminal_v11
     ==>
(scs_arrow_v39
 {scs_5M2 } 
({ scs_5T1} UNION { scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j }
UNION { scs_stab_diag_v39 scs_5I3 i j| scs_diag 5 i j }
UNION { scs_stab_diag_v39 scs_5M3 i j| scs_diag 5 i j }))`,
[
REPEAT GEN_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;


REWRITE_TAC[SCS_5T1_IS_SCS];

ASM_SIMP_TAC[ STAB_5I2_SCS;K_SCS_5I2]
;

ASM_SIMP_TAC[ STAB_5I3_SCS;K_SCS_5I3]
;


ASM_SIMP_TAC[ STAB_5M3_SCS;K_SCS_5M3]
;



DISJ_CASES_TAC(SET_RULE`(!s. s = scs_5M2 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_5M2 ==> MMs_v39 s = {}))`);


ASM_REWRITE_TAC[];


ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN STRIP_TAC;



MP_TAC(SET_RULE`(!i j. scs_diag 5 i j ==>   cstab < dist(v i,v j))\/ ~((!i j. scs_diag 5 i j ==>   cstab < dist((v:num->real^3) i,v j)))`)
THEN RESA_TAC;


EXISTS_TAC`scs_5T1`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC SCS_5M2_IMP_SCS_5T1
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN RESA_TAC
THEN MATCH_DICH_TAC 0
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`v:num->real^3`
THEN ASM_REWRITE_TAC[]
;



POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
THEN STRIP_TAC
;

MP_TAC(SET_RULE`    (!i. dist(v i, v(i+1))<= &2 * h0)
\/ ~    (!l. dist((v:num->real^3) l, v(l+1))<= &2 * h0)
`)
THEN RESA_TAC;




EXISTS_TAC`scs_stab_diag_v39 scs_5I2 i j`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;

MATCH_MP_TAC(SET_RULE`A==> B\/A\/C\/D`)
THEN EXISTS_TAC`i:num`
THEN EXISTS_TAC`j:num`
THEN ASM_REWRITE_TAC[]
;

MP_TAC MM_5M2_IMP_MM_STAB_5I2
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN RESA_TAC
THEN MATCH_DICH_TAC 0
THEN ASM_REWRITE_TAC[]
;



POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<=b)<=> b<a`]
THEN STRIP_TAC
;



MP_TAC(REAL_ARITH`dist((v:num->real^3) l, v(l+1))<= sqrt8\/ sqrt8<= dist(v l, v(l+1))`)
THEN RESA_TAC;



EXISTS_TAC`scs_stab_diag_v39 scs_5I3 i j`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;

MATCH_MP_TAC(SET_RULE`A==> B\/C\/A\/D`)
THEN EXISTS_TAC`i:num`
THEN EXISTS_TAC`j:num`
THEN ASM_REWRITE_TAC[]
;

MP_TAC MM_5M2_IMP_MM_STAB_5I3
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN RESA_TAC
THEN MATCH_DICH_TAC 0
THEN ASM_REWRITE_TAC[]
;




EXISTS_TAC`scs_stab_diag_v39 scs_5M3 i j`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;

MATCH_MP_TAC(SET_RULE`A==> B\/C\/D\/A`)
THEN EXISTS_TAC`i:num`
THEN EXISTS_TAC`j:num`
THEN ASM_REWRITE_TAC[]
;

MP_TAC MM_5M2_IMP_MM_STAB_5M3
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN RESA_TAC
THEN MATCH_DICH_TAC 0
THEN ASM_REWRITE_TAC[]
;
]);;


let HIJQAHA=prove_by_refinement(`main_nonlinear_terminal_v11
     ==>
(scs_arrow_v39
 {scs_5M2 } 
({ scs_5T1, scs_stab_diag_v39 scs_5I2 0 2,
scs_stab_diag_v39 scs_5M1 0 2, scs_stab_diag_v39 scs_5M1 0 3, 
       scs_stab_diag_v39 scs_5M1 2
       4,scs_4M6',scs_4M7,scs_4M8,scs_3T1,scs_3T4
}))`,
[
STRIP_TAC
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`({ scs_5T1} UNION { scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j }
UNION { scs_stab_diag_v39 scs_5I3 i j| scs_diag 5 i j }
UNION { scs_stab_diag_v39 scs_5M3 i j| scs_diag 5 i j })`
THEN ASM_SIMP_TAC[HIJ_STEP_1;SET_RULE`{scs_5T1, scs_stab_diag_v39 scs_5I2 0 2, scs_stab_diag_v39 scs_5M1 0 2, scs_stab_diag_v39 scs_5M1 0 3, 
       scs_stab_diag_v39 scs_5M1 2
       4, scs_4M6', scs_4M7, scs_4M8, scs_3T1, scs_3T4}
={scs_5T1}UNION{ scs_stab_diag_v39 scs_5I2 0 2}UNION{ scs_stab_diag_v39 scs_5M1 0 2, scs_stab_diag_v39 scs_5M1 0 3, 
       scs_stab_diag_v39 scs_5M1 2
       4}UNION{ scs_4M6', scs_4M7, scs_4M8, scs_3T1, scs_3T4}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC;

MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[SCS_5T1_IS_SCS];

MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_5I2];

MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_5M3_IMP_SCS_3_4]
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_stab_diag_v39 scs_5M1 i j | scs_diag 5 i j}`
THEN ASM_REWRITE_TAC[Otmtotj.STAB_5I3_ARROW_STAB_5M1_DIAG;Otmtotj.SET_EQ_DIAG_STAB_5M1]]);;

 end;;


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