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



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

open Hales_tactic;;

open Appendix;;





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

open Hales_tactic;;

open Appendix;;


open Zithlqn;;


open Xwitccn;;

open Ayqjtmd;;

open Jkqewgv;;


open Mtuwlun;;


open Uxckfpe;;
open Sgtrnaf;;

open Yxionxl;;

open Qknvmlb;;
open Odxlstcv2;;

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


let GSXRFWM1= prove_by_refinement(`!s v.
    is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\
    (!i. scs_b_v39 s i (i+1) <= cstab) ==> scs_generic v`,
[
REWRITE_TAC[IN;GSYM ADD1]
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 ASSUME_TAC(ARITH_RULE`3<4`)
THEN MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
THEN RESA_TAC
THEN MRESA_TAC LUNAR_IN_V[`E`;`v'`;`w`;`V`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN EXPAND_TAC "V"
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN REPEAT RESA_TAC
;

DICH_TAC(21-17)
THEN DICH_TAC(20-16)
THEN RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`3<6/\ ~(4<=3)`)
THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v x`;`v`;`x`]
THEN MRESA_TAC(GEN_ALL CARD_V_EQ_SCS_K1)[`s:scs_v39`;`v:num->real^3`;`IMAGE (v:num->real^3) (:num)`;`k:num`]
THEN MRESA_TAC Local_lemmas.NEXT_OPOSITE_POINT_IS_NOT_IN_AFF_GT2[`E`;`v x'`;`V`;`FF`;`v x`]
THEN MP_TAC(ARITH_RULE`i+1<4/\ ~(i=0)/\ ~(i=1)==> i=2`)
THEN RESA_TAC;






MP_TAC Axjrpnc.DIST_LE2_BB_CASSE_4
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`x`;`v`]
THEN MRESA_TAC Localization.LOFA_IMP_LT_CARD_SET_V_ALT[`V`;`E`;`FF`;`v x`]
THEN MRESA_TAC WL_IN_V[`i'`;`v`]
THEN POP_ASSUM MP_TAC
THEN SYM_ASSUM_TAC
THEN REWRITE_TAC[IN_ELIM_THM]
THEN RESA_TAC
THEN MRESA_TAC Nuxcoea.W_IN_BB_FUN_EQ[`v:num->real^3`;`i':num`;`n+x:num`;`s`]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`n+x:num`;`k`][ARITH_RULE`~(4=0)`]
THEN MRESA_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`SUC i':num`;`v:num->real^3`;`SUC (n+x)`]
THEN MP_TAC(ARITH_RULE`n<4==> n=0\/ n=1\/ n=2\/ n=3`)
THEN RESA_TAC;


POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th;ARITH_RULE`0+a=a`]
THEN REPEAT RESA_TAC)
THEN DICH_TAC (37-31)
THEN RESA_TAC
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`x`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC x`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC x)`]
THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`x`]
THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC x`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v x`;`v (SUC x)`;`&2* h0`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
THEN REWRITE_TAC[GSYM h0]
THEN STRIP_TAC
THEN MP_TAC Axjrpnc.NORM_V_IN_BB_LE_CSTAB
THEN RESA_TAC
THEN THAYTHE_TAC 0[`SUC x`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC x)`;`v (SUC(SUC x))`;`cstab`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
THEN REWRITE_TAC[GSYM cstab]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (x)) (v (SUC (x))) <= arclength (&2) (&2) (&2 * h0)
/\ arcV (vec 0) ((v:num->real^3) (SUC (x))) (v (SUC (SUC (x)))) <=
      arclength (&2) (&2) (cstab)
/\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
==>arcV (vec 0) (v ((x))) (v ((SUC (x))))+ arcV (vec 0) (v (SUC (x))) (v (SUC (SUC (x)))) 
 < pi`)
THEN ASM_SIMP_TAC[Axjrpnc.arclength_2h0_cstab]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_FF[`(x)`;`v`]
THEN MRESA_TAC WL_IN_FF[`SUC (x)`;`v`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (x), v (SUC (x))`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (x)), v (SUC (SUC (x)))`]
THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (x)`;`v (SUC(SUC (x)))`;`v (SUC (x))`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`]
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v x`;`v(x')`]
THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v x, v (2+x)}`]
;




POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th;ARITH_RULE`1+a=SUC a`]
THEN REPEAT RESA_TAC)
THEN DICH_TAC (37-31)
THEN RESA_TAC
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`x`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC x`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC x)`]
THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`x`]
THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC x`]
THEN MP_TAC Axjrpnc.NORM_V_IN_BB_LE_CSTAB
THEN RESA_TAC
THEN THAYTHE_TAC 0[`x`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v x`;`v (SUC x)`;`cstab`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
THEN REWRITE_TAC[GSYM cstab]
THEN STRIP_TAC
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC x)`;`v (SUC(SUC x))`;`&2* h0`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
THEN REWRITE_TAC[GSYM h0]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (x)) (v (SUC (x))) <= arclength (&2) (&2) (cstab)
/\ arcV (vec 0) ((v:num->real^3) (SUC (x))) (v (SUC (SUC (x)))) <=
      arclength (&2) (&2) (&2 * h0)
/\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
==>arcV (vec 0) (v ((x))) (v ((SUC (x))))+ arcV (vec 0) (v (SUC (x))) (v (SUC (SUC (x)))) 
 < pi`)
THEN ASM_SIMP_TAC[Axjrpnc.arclength_2h0_cstab]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_FF[`(x)`;`v`]
THEN MRESA_TAC WL_IN_FF[`SUC (x)`;`v`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (x), v (SUC (x))`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC (x)), v (SUC (SUC (x)))`]
THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v (x)`;`v (SUC(SUC (x)))`;`v (SUC (x))`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`]
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v x`;`v(x')`]
THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v x, v (2+x)}`]
;




POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th;ARITH_RULE`0+a=a`]
THEN REPEAT RESA_TAC)
THEN DICH_TAC (37-31)
THEN RESA_TAC
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`(2+x)`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (2+x)`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (2+x))`]
THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(2+x)`]
THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (2+x)`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (2+x)`;`v (SUC (2+x))`;`&2* h0`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
THEN REWRITE_TAC[GSYM h0]
THEN STRIP_TAC
THEN MP_TAC Axjrpnc.NORM_V_IN_BB_LE_CSTAB
THEN RESA_TAC
THEN THAYTHE_TAC 0[`SUC (2+x)`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (2+x))`;`v (SUC(SUC (2+x)))`;`cstab`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
THEN REWRITE_TAC[GSYM cstab]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v ((2+x))) (v (SUC ((2+x)))) <= arclength (&2) (&2) (&2 * h0)
/\ arcV (vec 0) ((v:num->real^3) (SUC ((2+x)))) (v (SUC (SUC ((2+x))))) <=
      arclength (&2) (&2) (cstab)
/\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
==>arcV (vec 0) (v (((2+x)))) (v ((SUC ((2+x)))))+ arcV (vec 0) (v (SUC ((2+x)))) (v (SUC (SUC ((2+x))))) 
 < pi`)
THEN ASM_SIMP_TAC[Axjrpnc.arclength_2h0_cstab]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_FF[`((2+x))`;`v`]
THEN MRESA_TAC WL_IN_FF[`SUC ((2+x))`;`v`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v ((2+x)), v (SUC ((2+x)))`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC ((2+x))), v (SUC (SUC ((2+x))))`]
THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v ((2+x))`;`v (SUC(SUC ((2+x))))`;`v (SUC ((2+x)))`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`]
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v x`;`v(x')`]
THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v (2+x), v (2+(2+x))}`]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[ARITH_RULE`2+2+i= 1*4+i`]
THEN MRESAS_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(1*4+x):num`;`v:num->real^3`;`(1*4+x) MOD k`][MOD_REFL;ARITH_RULE`~(4=0)`;MOD_MULT_ADD]
THEN MRESAS_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(x MOD k):num`;`v:num->real^3`;`x`][MOD_REFL;ARITH_RULE`~(4=0)`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC;



POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th;ARITH_RULE`3+a=SUC(2+a)`]
THEN REPEAT RESA_TAC)
THEN DICH_TAC (36-31)
THEN RESA_TAC
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`(2+x)`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC (2+x)`]
THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC (2+x))`]
THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`(2+x)`]
THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC (2+x)`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC (2+x))`;`v (SUC(SUC (2+x)))`;`&2* h0`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
THEN REWRITE_TAC[GSYM h0]
THEN STRIP_TAC
THEN MP_TAC Axjrpnc.NORM_V_IN_BB_LE_CSTAB
THEN RESA_TAC
THEN THAYTHE_TAC 0[`(2+x)`]
THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (2+x)`;`v (SUC (2+x))`;`cstab`][dist;]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[cstab;REAL_ARITH`#3.01 < &4`]
THEN REWRITE_TAC[GSYM cstab]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v ((2+x))) (v (SUC ((2+x)))) <= arclength (&2) (&2) (cstab)
/\ arcV (vec 0) ((v:num->real^3) (SUC ((2+x)))) (v (SUC (SUC ((2+x))))) <=
      arclength (&2) (&2)  (&2 * h0)
/\ arclength (&2) (&2) (&2 * h0) +      arclength (&2) (&2) (cstab) < pi
==>arcV (vec 0) (v (((2+x)))) (v ((SUC ((2+x)))))+ arcV (vec 0) (v (SUC ((2+x)))) (v (SUC (SUC ((2+x))))) 
 < pi`)
THEN ASM_SIMP_TAC[Axjrpnc.arclength_2h0_cstab]
THEN STRIP_TAC
THEN MRESA_TAC WL_IN_FF[`((2+x))`;`v`]
THEN MRESA_TAC WL_IN_FF[`SUC ((2+x))`;`v`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v ((2+x)), v (SUC ((2+x)))`]
THEN MRESA_TAC Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR[`V`;`E`;`FF`;`v (SUC ((2+x))), v (SUC (SUC ((2+x))))`]
THEN MRESA_TAC Ppbtydq.PPBTYDQ[`v ((2+x))`;`v (SUC(SUC ((2+x))))`;`v (SUC ((2+x)))`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC(i))= 2+i`]
THEN STRIP_TAC
THEN MRESA_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI[`E`;`V`;`FF`;`v x`;`v(x')`]
THEN MRESA_TAC Local_lemmas.CONV0_SUB_CONV[`vec 0:real^3`;`{v (2+x), v (2+(2+x))}`]
THEN DICH_TAC 0
THEN ASM_REWRITE_TAC[ARITH_RULE`2+2+i= 1*4+i`]
THEN MRESAS_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(1*4+x):num`;`v:num->real^3`;`(1*4+x) MOD k`][MOD_REFL;ARITH_RULE`~(4=0)`;MOD_MULT_ADD]
THEN MRESAS_TAC (GEN_ALL CHANGE_W_IN_BBS_MOD_IS_SCS)[`s:scs_v39`;`(x MOD k):num`;`v:num->real^3`;`x`][MOD_REFL;ARITH_RULE`~(4=0)`]
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN RESA_TAC;

]);;

let SCS_B_LE_CSTAB=prove(`!s v.
    is_scs_v39 s /\ scs_k_v39 s = 4 
==>     (!i. scs_b_v39 s i (i+1) <= cstab)`,
REPEAT RESA_TAC
THEN DICH_TAC 1
THEN ASM_SIMP_TAC[is_scs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`3<4`;ADD1]);;



let GSXRFWM= prove(`!s v.
    is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s 
     ==> scs_generic v`,
REPEAT STRIP_TAC
THEN MATCH_MP_TAC GSXRFWM1
THEN EXISTS_TAC`s:scs_v39`
THEN ASM_SIMP_TAC[GSXRFWM1;SCS_B_LE_CSTAB]);;
(************************)

let PSORT_5_EXPLICIT=prove(`
psort 5 (0,0)= (0,0)/\ 
psort 5 (1,1)= (1,1)/\
psort 5 (2,2)= (2,2)/\ 
psort 5 (3,3)= (3,3)/\ 
psort 5 (4,4)= (4,4)/\ 
psort 5 (0,1)= (0,1)/\ 
psort 5 (0,2)= (0,2)/\
psort 5 (0,3)= (0,3)/\
psort 5 (0,4)= (0,4)/\
psort 5 (1,0)= (0,1)/\
psort 5 (1,2)= (1,2)/\
psort 5 (1,3)= (1,3)/\
psort 5 (1,4)= (1,4)/\
psort 5 (2,0)= (0,2)/\
psort 5 (2,1)= (1,2)/\
psort 5 (2,3)= (2,3)/\
psort 5 (2,4)= (2,4)/\
psort 5 (3,0)= (0,3)/\
psort 5 (3,1)= (1,3)/\
psort 5 (3,2)= (2,3)/\
psort 5 (3,4)= (3,4)/\
psort 5 (4,0)= (0,4)/\
psort 5 (4,1)= (1,4)/\
psort 5 (4,2)= (2,4)/\
psort 5 (4,3)= (3,4)/\
psort 5 (4,5)= (0,4)/\
psort 5 (3,5)= (0,3)/\
psort 5 (2,5)= (0,2)/\
psort 5 (1,5)= (0,1)/\
psort 5 (5,1)= (0,1)/\
psort 5 (5,2)= (0,2)/\
psort 5 (5,3)= (0,3)/\
psort 5 (5,4)= (0,4)/\
psort 5 (5,5)= (0,0)/\
psort 5 (5,6)= (0,1)/\
psort 5 (5,7)= (0,2)/\
psort 5 (4,6)= (1,4)/\
psort 5 (6,4)= (1,4)/\
psort 5 (6,5)= (0,1)/\
psort 5 (6,7)= (1,2)/\
psort 5 (7,5)= (0,2)/\
psort 5 (7,6)= (1,2)/\
psort 5 (7,7)= (2,2)/\
psort 5 (6,6)= (1,1)/\
psort 4 (3,4)= (0,3)/\ 
psort 3 (2,0)= (0,2)/\
psort 3 (2,1)= (1,2)/\
psort 3 (1,0)= (0,1)/\
psort 4 (0,0)= (0,0)/\
psort 4 (1,1)= (1,1)/\
psort 4 (2,2)= (2,2)/\
psort 4 (3,3)= (3,3)/\
psort 4 (4,3)= (0,3)/\
psort 4 (4,4)= (0,0)/\
psort 4 (0,2)= (0,2)/\
psort 4 (4,5)= (0,1)/\
psort 4 (5,4)= (0,1)/\
psort 4 (5,5)= (1,1)
`,
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;scs_4I2;scs_4T1;scs_4T2;scs_4I1;scs_4T4;scs_4I3;scs_3T3;scs_4T5;
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_4I2_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4I2`,
[
SIMP_TAC[scs_4I2;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.467 < #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)[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 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
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 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
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;



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;




ASM_SIMP_TAC[ARITH_RULE`1<4`;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_4I1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4I1`,
[
SIMP_TAC[scs_4I1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(4=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.206 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
THEN REPEAT RESA_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)[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 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
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 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
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<4`;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_4T1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4T1`,
[
SIMP_TAC[scs_4T1;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.467 < #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)[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 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
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 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
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;



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;




ASM_SIMP_TAC[ARITH_RULE`1<4`;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_4T2_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4T2`,
[
SIMP_TAC[scs_4T2;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.467 < #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)[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 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
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 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
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;



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;




ASM_SIMP_TAC[ARITH_RULE`1<4`;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_4T4_IS_SCS=prove_by_refinement(
`is_scs_v39 scs_4T4`,
[
SIMP_TAC[scs_4T4;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.477 < #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 LT_sqrt8_2h0
THEN MP_TAC sqrt8_LE_6
THEN MP_TAC sqrt8_LE_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 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 MP_TAC sqrt8_LE_CSTAB
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 sqrt8 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_SIMP_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT;LT_sqrt8_2h0];

ASM_REWRITE_TAC[Geomdetail.CARD_SING]
THEN ARITH_TAC;

]);;

let SCS_4T5_IS_SCS=prove_by_refinement(
`is_scs_v39 scs_4T5`,

[
SIMP_TAC[scs_4T5;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 LT_sqrt8_2h0
THEN MP_TAC sqrt8_LE_6
THEN MP_TAC sqrt8_LE_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 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 MP_TAC sqrt8_LE_CSTAB
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_SIMP_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT;LT_sqrt8_2h0];

ASM_REWRITE_TAC[Geomdetail.CARD_SING]
THEN ARITH_TAC;

]);;

let SCS_4I3_IS_SCS=prove_by_refinement(
`is_scs_v39 scs_4I3`,
[
SIMP_TAC[scs_4I3;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.477 < #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 LT_sqrt8_2h0
THEN MP_TAC sqrt8_LE_6
THEN MP_TAC sqrt8_LE_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 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 MP_TAC sqrt8_LE_CSTAB
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 sqrt8 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_SIMP_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT;LT_sqrt8_2h0];

ASM_REWRITE_TAC[Geomdetail.CARD_SING]
THEN ARITH_TAC;

]);;


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


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


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


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


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


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


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


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


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


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


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


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


SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;


SCS_TAC;


SCS_TAC
THEN ASM_SIMP_TAC[MOD_LT;h0]
THEN REAL_ARITH_TAC;


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


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


MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
      (&2 * h0 < funlist_v39 [] cstab 3 i (SUC i) \/
       &2 < funlist_v39 [] (&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_4I2_BASIC=prove(`scs_basic_v39 scs_4I2`,
SCS_TAC);;
let K_SCS_4I2=prove(`scs_k_v39 scs_4I2=4`,
SCS_TAC);;
let J_SCS_4I2=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4I2 i) i1 j= F`,
SCS_TAC );;
let SCS_4I1_BASIC=prove(`scs_basic_v39 scs_4I1`,
SCS_TAC);;
let K_SCS_4I1=prove(`scs_k_v39 scs_4I1=4`,
SCS_TAC);;
let J_SCS_4I1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4I1 i) i1 j= F`,
SCS_TAC );;

let SCS_4T1_BASIC=prove(`scs_basic_v39 scs_4T1`,
SCS_TAC);;
let K_SCS_4T1=prove(`scs_k_v39 scs_4T1=4`,
SCS_TAC);;
let J_SCS_4T1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4T1 i) i1 j= F`,
SCS_TAC );;

let SCS_4T2_BASIC=prove(`scs_basic_v39 scs_4T2`,
SCS_TAC);;
let K_SCS_4T2=prove(`scs_k_v39 scs_4T2=4`,
SCS_TAC);;
let J_SCS_4T2=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4T2 i) i1 j= F`,
SCS_TAC );;
let SCS_4T4_BASIC=prove(`scs_basic_v39 scs_4T4`,
SCS_TAC);;
let K_SCS_4T4=prove(`scs_k_v39 scs_4T4=4`,
SCS_TAC);;
let J_SCS_4T4=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4T4 i) i1 j= F`,
SCS_TAC );;
let J_SCS_3T4_1=prove(`scs_J_v39 (scs_3T4 ) i1 j= F`,
SCS_TAC );;

let SCS_4I3_BASIC=prove(`scs_basic_v39 scs_4I3`,
SCS_TAC);;
let K_SCS_4I3=prove(`scs_k_v39 scs_4I3=4`,
SCS_TAC);;
let J_SCS_4I3=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4I3 i) i1 j= F`,
SCS_TAC );;

let SCS_3T3_BASIC=prove(`scs_basic_v39 scs_3T3`,
SCS_TAC);;
let K_SCS_3T3=prove(`scs_k_v39 scs_3T3=3`,
SCS_TAC);;
let J_SCS_3T3=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T3 i) i1 j= F`,
SCS_TAC );;
let J_SCS_3T3_1=prove(`scs_J_v39 (scs_3T3 ) i1 j= F`,
SCS_TAC );;


let SCS_4T5_BASIC=prove(`scs_basic_v39 scs_4T5`,
SCS_TAC);;
let K_SCS_4T5=prove(`scs_k_v39 scs_4T5=4`,
SCS_TAC);;
let J_SCS_4T5=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4T5 i) i1 j= F`,
SCS_TAC );;

let B_LE_CSTAB_SCS_4I2=prove(` (!i.  scs_b_v39 scs_4I2 i (SUC i) <= cstab)/\
(!i. scs_a_v39 scs_4I2 i (SUC i) = &2 /\
      scs_b_v39 scs_4I2 i (SUC i) <= &2 * h0)`,
SCS_TAC
THEN REWRITE_TAC[h0;scs_diag;cstab]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN REAL_ARITH_TAC);;
let B_LE_CSTAB_SCS_4I1=prove(` (!i.  scs_b_v39 scs_4I1 i (SUC i) <= cstab)`,
SCS_TAC
THEN REWRITE_TAC[h0;scs_diag;cstab]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN REAL_ARITH_TAC);;


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





let SCS_4I2_GENERIC=prove( `!v.
     v IN MMs_v39 scs_4I2  ==> scs_generic v`,
REPEAT STRIP_TAC
THEN MATCH_MP_TAC GSXRFWM
THEN EXISTS_TAC`scs_4I2`
THEN ASM_SIMP_TAC[GSYM ADD1;SCS_4I2_IS_SCS;K_SCS_4I2;B_LE_CSTAB_SCS_4I2]);;

let A_LT_B_4I2=prove(
`(!i. &2 < scs_b_v39 scs_4I2 i (SUC i)) /\
      (!i. scs_a_v39 scs_4I2 i (SUC i) = &2)`,
SCS_TAC
THEN ASM_SIMP_TAC[h0;scs_diag;cstab;ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN REPEAT RESA_TAC
THEN REAL_ARITH_TAC);;
let A_LT_B_4I1=prove(
`(!i. &2 < scs_b_v39 scs_4I1 i (SUC i)) /\
      (!i. scs_a_v39 scs_4I1 i (SUC i) = &2)`,
SCS_TAC
THEN ASM_SIMP_TAC[h0;scs_diag;cstab;ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN REPEAT RESA_TAC
THEN REAL_ARITH_TAC);;

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

let SCS_M_4I2=prove(`(scs_M scs_4I2) ={}`,
ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
THEN SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
THEN ARITH_TAC);;
let CARD_SCS_M_4I1=prove(`CARD (scs_M scs_4I1) <= 1`,
ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
THEN SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
THEN ARITH_TAC);;
let SCS_M_4I1=prove(`(scs_M scs_4I1) ={}`,
ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
THEN SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
THEN ARITH_TAC);;


let SCS_4I2_IMP_SCS_4T1= prove_by_refinement
(`main_nonlinear_terminal_v11
==>(!v. 
    v IN MMs_v39 scs_4I2 /\
    (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) ==>
    ~(MMs_v39 (scs_4T1)={}))`,
[REWRITE_TAC[IN;SET_RULE`~(A={})<=> ?a. a IN A`]
THEN REPEAT STRIP_TAC
THEN MP_TAC SCS_4I2_IS_SCS
THEN STRIP_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN ASSUME_TAC SCS_4I2_BASIC
THEN ASSUME_TAC K_SCS_4I2
THEN ASSUME_TAC SCS_4T1_BASIC
THEN ASSUME_TAC K_SCS_4T1
THEN ASSUME_TAC SCS_4T1_IS_SCS
THEN MP_TAC Rrcwnsj.RRCWNSJ
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4I2`;`v`][ARITH_RULE`3<4`;h0_LT_B_SCS_4I2;B_LE_CSTAB_SCS_4I2]
THEN MP_TAC JCYFMRP_V3
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4I2`;`v`][ARITH_RULE`3<4`;h0_LT_B_SCS_4I2;B_LE_CSTAB_SCS_4I2;IN;CARD_SCS_M_4I2;GSYM ADD1;A_LT_B_4I2]
THEN MP_TAC Jlxfdmj.JLXFDMJ
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4I2`;`v`;`i`][ARITH_RULE`3<4`;h0_LT_B_SCS_4I2;B_LE_CSTAB_SCS_4I2;IN;CARD_SCS_M_4I2;GSYM ADD1;A_LT_B_4I2;SCS_M_4I2;SET_RULE`~{} (j MOD 4)<=> T`]
THEN 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_4I2`
THEN ASM_SIMP_TAC[SCS_M_4I2]
THEN STRIP_TAC;

DICH_TAC(12-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_4I2;K_SCS_4T1;scs_prop_equ_v39;]
THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
THEN SCS_TAC
THEN REWRITE_TAC[ARITH_RULE`~(4<=3)`]
THEN REPEAT STRIP_TAC;

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



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


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


MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`j:num`;`v`;` SUC i'`][SCS_4I2_IS_SCS;K_SCS_4I2;MOD_REFL;ARITH_RULE`~(4=0)`;]
THEN REAL_ARITH_TAC;


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

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


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


SCS_TAC
THEN REAL_ARITH_TAC]);;







let SCS_DIAG_4_CASES=prove(`scs_diag 4 i j<=> ((i MOD 4= 0 /\ j MOD 4=2)\/ (i MOD 4= 1 /\ j MOD 4=3)\/
(j MOD 4= 0 /\ i MOD 4=2)\/ (j MOD 4= 1 /\ i MOD 4=3))`,
REWRITE_TAC[scs_diag]
THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`4`][ARITH_RULE`1<4`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`4`][ARITH_RULE`1<4`]
THEN SYM_ASSUM_TAC
THEN ARITH_TAC);;

let WLOG_4_BB_SCS=prove_by_refinement(` is_scs_v39 s/\
v IN BBs_v39 s /\ 
  scs_k_v39 s=4/\
    scs_diag 4 i j /\
  (!i j. (P (v i) (v j)<=> P (v j) (v i)))/\
   P (v i) (v j)
==> P (v 0) (v 2)\/ P (v 1) (v 3)`,
[REWRITE_TAC[SCS_DIAG_4_CASES;IN]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC;

MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v`;`0`][ARITH_RULE`0 MOD 4=0`]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j`;`v`;`2`][ARITH_RULE`2 MOD 4=2`]
THEN RESA_TAC;

MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v`;`1`][ARITH_RULE`1 MOD 4=1`]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j`;`v`;`3`][ARITH_RULE`3 MOD 4=3`]
THEN RESA_TAC;

MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v`;`2`][ARITH_RULE`2 MOD 4=2`]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j`;`v`;`0`][ARITH_RULE`0 MOD 4=0`]
THEN RESA_TAC;

MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j`;`v`;`1`][ARITH_RULE`1 MOD 4=1`]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v`;`3`][ARITH_RULE`3 MOD 4=3`]
THEN RESA_TAC]);;

let DIST_DIAG_2_CASES=prove(`v IN MMs_v39 scs_4I2 /\
    scs_diag 4 i j /\
   dist(v i,v j)<= cstab
==> dist(v 0,v 2)<= cstab\/ dist(v 1,v 3)<= cstab`,
REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC  (INST[`scs_4I2`,`s:scs_v39`;`i:num`,`i:num`;`j:num`,`j:num`;`(\i:real^3. (\j:real^3. dist(i,j)<= cstab))`,`P:real^3->real^3->bool`;`v:num->real^3`,`v:num->real^3`]WLOG_4_BB_SCS
)[`i`;`j`;`v`]
THEN MATCH_DICH_TAC 0
THEN SIMP_TAC[DIST_SYM;K_SCS_4I2;SCS_4I2_IS_SCS;IN]
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]);;

let WLOG_4_BB_SCS_DIAG=prove_by_refinement(` is_scs_v39 s/\
v IN BBs_v39 s /\ 
  scs_k_v39 s=4/\
    scs_diag 4 i j /\
  (!i j i1 j1. P i j i1 j1 <=> P j i i1 j1)/\
(!i j i1 j1. P i j i1 j1 <=> P i j j1 i1)/\
   P (v i) (v j) (v (i+1)) (v (j+1))
==> P (v 0) (v 2) (v 1) (v 3) \/ P (v 1) (v 3) (v 0) (v 2)`,
[REWRITE_TAC[SCS_DIAG_4_CASES;IN]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC;

ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0`)
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v`;`0`][ARITH_RULE`0 MOD 4=0`;GSYM ADD1]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j`;`v`;`2`][ARITH_RULE`2 MOD 4=2`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`0`;`4`]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i`;`v`;`1`][ARITH_RULE`2 MOD 4=2`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`2`;`4`]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j`;`v`;`3`][ARITH_RULE`2 MOD 4=2`]
THEN RESA_TAC;

ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0`)
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v`;`1`][ARITH_RULE`0 MOD 4=0`;GSYM ADD1]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j`;`v`;`3`][ARITH_RULE`2 MOD 4=2`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`1`;`4`]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i`;`v`;`2`][ARITH_RULE`2 MOD 4=2`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`3`;`4`]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j`;`v`;`4`][ARITH_RULE`2 MOD 4=2`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHE_TAC 0[`4`;`0`]
THEN RESA_TAC;

ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0`)
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j`;`v`;`0`][ARITH_RULE`0 MOD 4=0`;GSYM ADD1]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v`;`2`][ARITH_RULE`2 MOD 4=2`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`0`;`4`]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j`;`v`;`1`][ARITH_RULE`2 MOD 4=2`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`2`;`4`]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i`;`v`;`3`][ARITH_RULE`2 MOD 4=2`]
THEN RESA_TAC;

ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0`)
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`j`;`v`;`1`][ARITH_RULE`0 MOD 4=0`;GSYM ADD1]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v`;`3`][ARITH_RULE`2 MOD 4=2`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`1`;`4`]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC j`;`v`;`2`][ARITH_RULE`2 MOD 4=2`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`3`;`4`]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC i`;`v`;`4`][ARITH_RULE`2 MOD 4=2`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
THEN THAYTHE_TAC 0[`4`;`0`]
THEN RESA_TAC;]);;


let DIST_DIAG_2_CASES_EQ_3=prove( `v IN MMs_v39 scs_4I2 /\
    scs_diag 4 i j /\
   dist(v i,v j)= &3 /\ dist(v (i+1),v (j+1))= &3
==> dist(v 0,v 2)= &3 /\ dist(v 1,v 3)= &3`,
REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC  (INST[`scs_4I2`,`s:scs_v39`;`i:num`,`i:num`;`j:num`,`j:num`;`(\i:real^3. (\j:real^3. (\i1:real^3. (\j1:real^3. dist(i,j)= &3/\ dist(i1,j1)= &3))))`,`P:real^3->real^3->real^3->real^3->bool`;`v:num->real^3`,`v:num->real^3`]WLOG_4_BB_SCS_DIAG
)[`i`;`j`;`v`]
THEN DICH_TAC 0
THEN SIMP_TAC[DIST_SYM;K_SCS_4I2;SCS_4I2_IS_SCS;IN]
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN RESA_TAC);;



let DIST_DIAG_2_CASES_3_LE=prove( `MMs_v39 scs_4I2 v /\
    scs_diag 4 i j /\
   &3<= dist(v i,v j) /\ &3<= dist(v (i+1),v (j+1))
==> &3<= dist(v 0,v 2) /\ &3<= dist(v 1,v 3)`,
REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC  (INST[`scs_4I2`,`s:scs_v39`;`i:num`,`i:num`;`j:num`,`j:num`;`(\i:real^3. (\j:real^3. (\i1:real^3. (\j1:real^3. &3<= dist(i,j)/\ &3<= dist(i1,j1)))))`,`P:real^3->real^3->real^3->real^3->bool`;`v:num->real^3`,`v:num->real^3`]WLOG_4_BB_SCS_DIAG
)[`i`;`j`;`v`]
THEN DICH_TAC 0
THEN SIMP_TAC[DIST_SYM;K_SCS_4I2;SCS_4I2_IS_SCS;IN]
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN RESA_TAC);;

let DIST_DIAG_2_CASES_3_LT=prove( `MMs_v39 scs_4I2 v /\
    scs_diag 4 i j /\
   &3<= dist(v i,v j) /\ &3< dist(v (i+1),v (j+1))
==> (&3<= dist(v 0,v 2) /\ &3< dist(v 1,v 3))\/ (&3<= dist(v 1,v 3) /\ &3< dist(v 0,v 2))`,
REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MRESA_TAC  (INST[`scs_4I2`,`s:scs_v39`;`i:num`,`i:num`;`j:num`,`j:num`;`(\i:real^3. (\j:real^3. (\i1:real^3. (\j1:real^3. &3<= dist(i,j)/\ &3< dist(i1,j1)))))`,`P:real^3->real^3->real^3->real^3->bool`;`v:num->real^3`,`v:num->real^3`]WLOG_4_BB_SCS_DIAG
)[`i`;`j`;`v`]
THEN DICH_TAC 0
THEN SIMP_TAC[DIST_SYM;K_SCS_4I2;SCS_4I2_IS_SCS;IN]
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN RESA_TAC);;





let WLOG_ASSUME_MIN=prove(`((a<=c /\ a<=b)\/ (c<=a /\ c<=b) ==> Q)
==> (a<=b \/ c<=b ==> Q)`,
REPEAT STRIP_TAC
THEN MATCH_DICH_TAC 1
THEN DICH_TAC 0
THEN REAL_ARITH_TAC);;


let ASSUME_MIN_DIAG= prove_by_refinement(`
(!i j. 
    MMs_v39 scs_4I2 v/\
    scs_diag 4 i j /\
   dist(v i,v j)<= cstab/\
  dist(v i,v j)<= dist(v (i+1),v (j+1))
 ==>
   ~(MMs_v39 (scs_4T1)={})\/ ~(MMs_v39 (scs_4T2)={}))
==>(!i j.
    MMs_v39 scs_4I2 v /\
    scs_diag 4 i j /\
   dist(v i,v j)<= cstab ==>
    ~(MMs_v39 (scs_4T1)={})\/ ~(MMs_v39 (scs_4T2)={}))`,
[
REPEAT RESA_TAC
THEN MP_TAC(SET_RULE`  dist(v i,v j)<= dist(v (i+1),v (j+1))
\/  ~( dist(v i,v j)<= dist(v (i+1),(v:num->real^3) (j+1)))
`)
THEN RESA_TAC;

MATCH_DICH_TAC 4
THEN EXISTS_TAC`i:num`
THEN EXISTS_TAC`j:num`
THEN ASM_REWRITE_TAC[];

MATCH_DICH_TAC 4
THEN EXISTS_TAC`i+1:num`
THEN EXISTS_TAC`j+1:num`
THEN ASM_REWRITE_TAC[]
THEN DICH_TAC 2
THEN ASM_REWRITE_TAC[SCS_DIAG_4_CASES]
THEN RESA_TAC
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`4`][ARITH_RULE`1<4`;GSYM ADD1]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`4`][ARITH_RULE`1<4`]
THEN SYM_ASSUM_TAC
THEN STRIP_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN ASSUME_TAC SCS_4I2_IS_SCS
THEN ASSUME_TAC K_SCS_4I2;

ARITH_TAC;

ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0`)
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`0`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`1`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`2`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC j`;`3`;`4`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`]
THEN THAYTHEL_ASM_TAC 0[`SUC i`;`1`][]
THEN THAYTHEL_ASM_TAC 0[`SUC j`;`3`][]
THEN THAYTHEL_ASM_TAC 0[`SUC(SUC j)`;`4`][]
THEN THAYTHEL_ASM_TAC 0[`SUC(SUC i)`;`2`][]
THEN THAYTHEL_ASM_TAC 0[`4`;`0`][]
THEN THAYTHEL_ASM_TAC 0[`i`;`0`][]
THEN THAYTHEL_ASM_TAC 0[`j`;`2`][]
THEN DICH_TAC(20-1)
THEN DICH_TAC(19-1)
THEN ASM_SIMP_TAC[GSYM ADD1]
THEN MRESA_TAC DIST_SYM[`v 2`;`v 0`]
THEN REAL_ARITH_TAC;

ARITH_TAC;

ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ SUC 4=5/\ 5 MOD 4=1`)
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`1`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`2`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`3`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC j`;`4`;`4`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`]
THEN THAYTHEL_ASM_TAC 0[`SUC i`;`2`][]
THEN THAYTHEL_ASM_TAC 0[`SUC j`;`4`][]
THEN THAYTHEL_ASM_TAC 0[`SUC(SUC j)`;`1`][]
THEN THAYTHEL_ASM_TAC 0[`SUC(SUC i)`;`3`][]
THEN THAYTHEL_ASM_TAC 0[`4`;`0`][]
THEN THAYTHEL_ASM_TAC 0[`i`;`1`][]
THEN THAYTHEL_ASM_TAC 0[`j`;`3`][]
THEN DICH_TAC(20-1)
THEN DICH_TAC(19-1)
THEN ASM_SIMP_TAC[GSYM ADD1]
THEN MRESA_TAC DIST_SYM[`v 3`;`v 1`]
THEN REAL_ARITH_TAC;

ARITH_TAC;

ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0`)
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`2`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`3`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`0`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC j`;`1`;`4`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`]
THEN THAYTHEL_ASM_TAC 0[`SUC i`;`3`][]
THEN THAYTHEL_ASM_TAC 0[`SUC j`;`1`][]
THEN THAYTHEL_ASM_TAC 0[`SUC(SUC j)`;`2`][]
THEN THAYTHEL_ASM_TAC 0[`SUC(SUC i)`;`4`][]
THEN THAYTHEL_ASM_TAC 0[`4`;`0`][]
THEN THAYTHEL_ASM_TAC 0[`i`;`2`][]
THEN THAYTHEL_ASM_TAC 0[`j`;`0`][]
THEN DICH_TAC(20-1)
THEN DICH_TAC(19-1)
THEN ASM_SIMP_TAC[GSYM ADD1]
THEN MRESA_TAC DIST_SYM[`v 0`;`v 2`]
THEN REAL_ARITH_TAC;

ARITH_TAC;

ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ SUC 4=5/\ 5 MOD 4=1`)
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`3`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`4`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`1`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC j`;`2`;`4`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`]
THEN THAYTHEL_ASM_TAC 0[`SUC i`;`4`][]
THEN THAYTHEL_ASM_TAC 0[`SUC j`;`2`][]
THEN THAYTHEL_ASM_TAC 0[`SUC(SUC j)`;`3`][]
THEN THAYTHEL_ASM_TAC 0[`SUC(SUC i)`;`1`][]
THEN THAYTHEL_ASM_TAC 0[`4`;`0`][]
THEN THAYTHEL_ASM_TAC 0[`i`;`3`][]
THEN THAYTHEL_ASM_TAC 0[`j`;`1`][]
THEN DICH_TAC(20-1)
THEN DICH_TAC(19-1)
THEN ASM_SIMP_TAC[GSYM ADD1]
THEN MRESA_TAC DIST_SYM[`v 1`;`v 3`]
THEN REAL_ARITH_TAC]);;

let SCS_4I2_3_LE_A=prove_by_refinement(` BBs_v39 scs_4I2 v/\
scs_diag 4 i j
==> &3<= dist(v i,v j)`,
[
REWRITE_TAC[IN]
THEN REPEAT RESA_TAC
THEN DICH_TAC 0
THEN REWRITE_TAC[SCS_DIAG_4_CASES]
THEN RESA_TAC;

ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ ~(0=1)/\ ~(1=2)/\ ~(3=0)`)
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`i`;`v`;`0`][ARITH_RULE`0 MOD 4=0`;SCS_4I2_IS_SCS;K_SCS_4I2]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`j`;`v`;`2`][ARITH_RULE`2 MOD 4=2`;SCS_4I2_IS_SCS;K_SCS_4I2]
THEN DICH_TAC 5
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;mk_unadorned_v39;scs_v39_explicit;scs_4I2;CS_ADJ;ARITH_RULE`~(4<=3)`]
THEN RESA_TAC
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`0`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`2`;`4`]
THEN THAYTHES_TAC 3[`i`;`j`][ARITH_RULE`~(0=2)`];


ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ ~(0=1)/\ ~(1=2)/\ ~(3=0)/\ ~(1=3)/\ ~(2=3)`)
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`i`;`v`;`1`][ARITH_RULE`0 MOD 4=0`;SCS_4I2_IS_SCS;K_SCS_4I2]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`j`;`v`;`3`][ARITH_RULE`2 MOD 4=2`;SCS_4I2_IS_SCS;K_SCS_4I2]
THEN DICH_TAC 5
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;mk_unadorned_v39;scs_v39_explicit;scs_4I2;CS_ADJ;ARITH_RULE`~(4<=3)`]
THEN RESA_TAC
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`1`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`3`;`4`]
THEN THAYTHES_TAC 3[`i`;`j`][ARITH_RULE`~(0=2)`];

ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ ~(0=1)/\ ~(1=2)/\ ~(3=0)`)
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`j`;`v`;`0`][ARITH_RULE`0 MOD 4=0`;SCS_4I2_IS_SCS;K_SCS_4I2]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`i`;`v`;`2`][ARITH_RULE`2 MOD 4=2`;SCS_4I2_IS_SCS;K_SCS_4I2]
THEN DICH_TAC 5
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;mk_unadorned_v39;scs_v39_explicit;scs_4I2;CS_ADJ;ARITH_RULE`~(4<=3)`]
THEN RESA_TAC
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`0`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`2`;`4`]
THEN THAYTHES_TAC 3[`i`;`j`][ARITH_RULE`~(0=2)`];

ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ ~(0=1)/\ ~(1=2)/\ ~(3=0)/\ ~(1=3)/\ ~(2=3)`)
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`j`;`v`;`1`][ARITH_RULE`0 MOD 4=0`;SCS_4I2_IS_SCS;K_SCS_4I2]
THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_4I2`;`i`;`v`;`3`][ARITH_RULE`2 MOD 4=2`;SCS_4I2_IS_SCS;K_SCS_4I2]
THEN DICH_TAC 5
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;mk_unadorned_v39;scs_v39_explicit;scs_4I2;CS_ADJ;ARITH_RULE`~(4<=3)`]
THEN RESA_TAC
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`1`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`3`;`4`]
THEN THAYTHES_TAC 3[`i`;`j`][ARITH_RULE`~(0=2)`]]);;



let SCS_DIAG_ADD1=prove_by_refinement(`scs_diag 4 i j==> scs_diag 4 (i+1) (j+1)`,
[REWRITE_TAC[SCS_DIAG_4_CASES;GSYM ADD1]
THEN RESA_TAC;

ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ ~(0=1)/\ ~(1=2)/\ ~(3=0)/\ ~(1=3)/\ ~(2=3)`)
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`0`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`2`;`4`];

ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ ~(0=1)/\ ~(1=2)/\ ~(3=0)/\ ~(1=3)/\ ~(2=3)`)
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`1`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`3`;`4`];

ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ ~(0=1)/\ ~(1=2)/\ ~(3=0)/\ ~(1=3)/\ ~(2=3)`)
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`0`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`2`;`4`];

ASSUME_TAC(ARITH_RULE`~(4=0)/\ 0 MOD 4=0/\ 1 MOD 4=1/\ SUC 0=1/\ SUC 1=2/\ 2 MOD 4=2/\ SUC 2=3 /\3 MOD 4=3/\ SUC 3=4/\ 4 MOD 4=0/\ ~(0=1)/\ ~(1=2)/\ ~(3=0)/\ ~(1=3)/\ ~(2=3)`)
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j`;`1`;`4`]
THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`3`;`4`]]);;

let ear_acute = prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6. 
    &2 <= y1 /\ y1 <= &2 * h0 /\
    &2 <= y2 /\ y2 <= &2 * h0 /\
    &2 <= y3 /\ y3 <= &2 * h0 /\
    &2 <= y4 /\ y4 <= &2 * h0 /\
    &2 <= y6 /\ y6 <= &2 * h0 /\
    &3 <= y5 /\
    &0 < ups_x (y1*y1) (y3*y3) (y5*y5) 
    ==> dih_y y1 y2 y3 y4 y5 y6 < pi / &2)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.h0;arith `&2 * #1.26  = #2.52`;Trigonometry.IHIQXLM];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (Terminal.get_main_nonlinear "2485876245a") [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`];
  ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;arith `#3.0 = &3`;];
  ANTS_TAC;
    REWRITE_TAC[arith `x <= y <=> ~(y < x)`];
    DISCH_TAC;
    FIRST_X_ASSUM_ST `&16` MP_TAC THEN REWRITE_TAC[arith `a * b * c = (a * b) * c`];
    REWRITE_TAC[arith `~(&0 < x * y) <=> &0 <= x * (-- y)`];
    REPEAT (GMATCH_SIMP_TAC REAL_LE_MUL_EQ);
    REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REWRITE_TAC[Nonlinear_lemma.dih_x_alt;Sphere.dih_y;LET_THM;GSYM Sphere.delta_y];
  REWRITE_TAC[GSYM Sphere.delta4_y;GSYM Sphere.y_of_x];
  REWRITE_TAC[arith `pi2 + a < pi2 <=> a < &0`];
  DISCH_TAC;
  GMATCH_SIMP_TAC Tskajxy.ATN2_Y_NEG;
  CONJ_TAC;
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  BY(REWRITE_TAC[arith `p - a = p + -- a`;GSYM ATN_NEG;arith `-- p + a < &0 <=> a < p`;ATN_BOUNDS])
  ]);;  (* }}} *)


let SCS_DIAG_4_ADD2=prove(`scs_diag 4 (i+1) (i+3)`,
SIMP_TAC[scs_diag;ARITH_RULE`~(4=0)/\ SUC(i+1)= i+2/\ SUC (i+3)=i+4`;Ocbicby.MOD_EQ_MOD_SHIFT;]
THEN ARITH_TAC);;

let SCS_DIAG_4_ADD0=prove(`scs_diag 4 (i) (i+2)`,
SIMP_TAC[scs_diag;ARITH_RULE`~(4=0)/\ SUC(i)= i+1/\ SUC (i+2)=i+3`;Ocbicby.MOD_EQ_MOD_SHIFT;]
THEN MP_TAC(SET_RULE`i= i+0==> i MOD 4= (i+0) MOD 4`)
THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`i+0=i`]
THEN RESA_TAC
THEN SIMP_TAC[scs_diag;ARITH_RULE`~(4=0)/\ SUC(i)= i+1/\ SUC (i+2)=i+3`;Ocbicby.MOD_EQ_MOD_SHIFT;]
THEN ARITH_TAC);;

let EDGE_4I2_LE_2H0=prove(`BBs_v39 scs_4I2 v
==> dist(v i, v (i+1))<= &2* h0/\ &2<= dist(v i, v (i+1))`,
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_4I2;K_SCS_4T1;scs_prop_equ_v39;]
THEN STRIP_TAC
THEN THAYTHE_TAC 1[`i`;`i+1`]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN SCS_TAC
THEN ASM_SIMP_TAC[GSYM ADD1;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]);;


let SCS_4I2_STRAIGHT= prove_by_refinement(`main_nonlinear_terminal_v11
==>(!i. MMs_v39 scs_4I2 v
==> azim (vec 0) (v i) (v (i+1)) (v (i+3))<pi)`,
[
REPEAT STRIP_TAC
THEN MP_TAC SCS_DIAG_ADD1
THEN RESA_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN MRESAL_TAC SCS_4I2_3_LE_A[`i+1`;`v`;`i+3`][SCS_DIAG_4_ADD2]
THEN MRESAL_TAC SCS_4I2_3_LE_A[`i`;`v`;`i+2`][SCS_DIAG_4_ADD0]
THEN MRESAL_TAC Nuxcoea.WL_IN_BALL_ANNULUS[`scs_4I2`;`v`;`i`][Ckqowsa_3_points.in_ball_annulus]
THEN MRESAL_TAC Nuxcoea.WL_IN_BALL_ANNULUS[`scs_4I2`;`v`;`i+1`][Ckqowsa_3_points.in_ball_annulus]
THEN MRESAL_TAC Nuxcoea.WL_IN_BALL_ANNULUS[`scs_4I2`;`v`;`i+3`][Ckqowsa_3_points.in_ball_annulus]
THEN MRESAL_TAC Nuxcoea.WL_IN_BALL_ANNULUS[`scs_4I2`;`v`;`i+2`][Ckqowsa_3_points.in_ball_annulus]
THEN MRESA_TAC EDGE_4I2_LE_2H0[`v`;`i`]
THEN MRESAL_TAC EDGE_4I2_LE_2H0[`v`;`i+1`][ARITH_RULE`(i+1)+1=i+2`]
THEN MRESAL_TAC EDGE_4I2_LE_2H0[`v`;`i+2`][ARITH_RULE`(i+2)+1=i+3`]
THEN ASSUME_TAC(SCS_4I2_IS_SCS)
THEN ASSUME_TAC(K_SCS_4I2)
THEN ASSUME_TAC(ARITH_RULE`i+4= 1*4+i`)
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`]
THEN THAYTHES_TAC 0[`i+4`;`i`][MOD_MULT_ADD]
THEN MRESAL_TAC EDGE_4I2_LE_2H0[`v`;`i+3`][ARITH_RULE`(i+3)+1=i+4`]
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 MRESAL_TAC SCS_4I2_GENERIC[`v`][IN;scs_generic]
THEN ASSUME_TAC(ARITH_RULE`3<4`)
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`scs_4I2`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`(i+1)`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`i+3`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`i`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`i+2`;`v:num->real^3`]
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`]
THEN MP_TAC(SET_RULE`i= i+0==> i MOD 4= (i+0) MOD 4`)
THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`i+0=i`]
THEN RESA_TAC
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v i`;`v (i+2)`;`V`]
THEN THAYTHES_TAC 0[`v i`;`v (i+2)`][SET_RULE`a IN {a,b}`;ARITH_RULE`~(4=0)/\ ~(0 MOD 4 = 2 MOD 4)`;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (i+1)`;`v (i+3)`;`V`]
THEN THAYTHES_TAC 0[`v (i+3)`;`v (i)`][SET_RULE`a IN {b,a}`;ARITH_RULE`~(4=0)/\ ~(0 MOD 4 = 3 MOD 4)`;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN STRIP_TAC
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (i+1)`;`v (i+3)`;`V`]
THEN THAYTHES_TAC 0[`v (i+1)`;`v (i)`][SET_RULE`a IN {a,b}`;ARITH_RULE`~(4=0)/\ ~(0 MOD 4 = 1 MOD 4)`;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN STRIP_TAC
THEN MRESAL_TAC Collect_geom2.NOT_COL_EQ_UPS_X_POS[`vec 0:real^3`;`v (i)`;`v(i+2)`][dist;VECTOR_ARITH`vec 0-A= --A`;NORM_NEG]
THEN DICH_TAC 0
THEN REWRITE_TAC[GSYM dist]
THEN RESA_TAC
THEN MRESA_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`scs_4I2`;`FF`;`v i`;`v`;`i`;`4`]
THEN MRESA_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v i`]
THEN THAYTHE_TAC 0[`v(i+2)`]
THEN MP_TAC ear_acute
THEN RESA_TAC
THEN THAYTHES_TAC 0[`norm (v (i))`;`norm (v (i+1))`;`norm (v (i+2))`;`dist(v (i+1),v (i+2))`;`dist(v (i),v(i+2))`;`dist(v i, v(i+1))`][REAL_ARITH`a*a= a pow 2`]
THEN DICH_TAC 0
THEN MRESAL_TAC Iunbuig.azim_dih_y[`vec 0:real^3`;`v i`;`v (i+1)`;`v(i+2)`][dist;VECTOR_ARITH`vec 0-A= --A`;NORM_NEG]
THEN SYM_ASSUM_TAC
THEN MRESA_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v i`]
THEN THAYTHE_TAC 0[`v(i+3)`]
THEN MRESAL_TAC Terminal.vv_split_azim_generic[`v`;`4`;`i`;`2`;`3`][LET_DEF;LET_END_DEF;ARITH_RULE`3<=4/\0<2/\ 2<3`]
THEN DICH_TAC 0
THEN SUBGOAL_THEN`(!i j. i < 4 /\ j < 4 /\ i MOD 4 = j MOD 4 ==> i = j)`ASSUME_TAC;

REPEAT RESA_TAC
THEN DICH_TAC 0
THEN ASM_SIMP_TAC[ARITH_RULE`~(4=0)`;MOD_LT];

ASM_REWRITE_TAC[]
THEN DICH_TAC(54-5)
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;K_SCS_4I2;ARITH_RULE`~(4<=3)`;ADD1]
THEN RESA_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v i) (v (i + 1)) (v (i + 3)) <= pi/\
azim (vec 0) (v i) (v (i + 1)) (v (i + 3)) =
      azim (vec 0) (v i) (v (i + 1)) (v (i + 2)) +
      azim (vec 0) (v i) (v (i + 2)) (v (i + 3))
/\ &0<= azim (vec 0) (v i) (v (i + 1)) (v (i + 2))
==> azim (vec 0) (v i) (v (i + 2)) (v (i + 3))<= pi
 `)
THEN ASM_REWRITE_TAC[azim]
THEN STRIP_TAC
THEN MP_TAC ear_acute
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`norm (v (i))`;`norm (v (i+3))`;`norm (v (i+2))`;`dist(v (i+2),v (i+3))`;`dist(v (i),v(i+2))`;`dist(v i, v(i+3))`][REAL_ARITH`a*a= a pow 2`]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN MATCH_MP_TAC(REAL_ARITH`a<c/ &2 /\ b<c/ &2 ==> a+b< c`)
THEN ASM_REWRITE_TAC[]
THEN MRESAL_TAC Iunbuig.azim_dih_y[`vec 0:real^3`;`v i`;`v (i+2)`;`v(i+3)`][dist;VECTOR_ARITH`vec 0-A= --A`;NORM_NEG]
THEN ONCE_REWRITE_TAC[Nonlinear_lemma.dih_y_sym]
THEN REWRITE_TAC[GSYM dist]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]]);;


let SCS_4I2_STRAIGHT_ALL= prove_by_refinement(`main_nonlinear_terminal_v11
==>( 
    MMs_v39 scs_4I2 v==>
azim (vec 0) (v 0) (v 1) (v 3) < pi 
/\ azim (vec 0) (v 1) (v 2) (v 0) < pi 
/\ azim (vec 0) (v 2) (v 3) (v 1) < pi 
/\ azim (vec 0) (v 3) (v 0) (v 2) < pi )`,
[REPEAT STRIP_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN ASSUME_TAC(SCS_4I2_IS_SCS)
THEN ASSUME_TAC(K_SCS_4I2)
THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`]
THEN MP_TAC SCS_4I2_STRAIGHT
THEN RESA_TAC;

THAYTHEL_TAC 0[`0`][ARITH_RULE`0+a=a`];

THAYTHEL_TAC 1[`4`;`0`][ARITH_RULE`4 MOD 4 = 0 MOD 4`]
THEN THAYTHEL_TAC 1[`1`][ARITH_RULE`1+1=2/\1+3=4`];

THAYTHEL_TAC 1[`5`;`1`][ARITH_RULE`5 MOD 4 = 1 MOD 4`]
THEN THAYTHEL_TAC 1[`2`][ARITH_RULE`2+1=3/\2+3=5`];

THAYTHEL_ASM_TAC 1[`4`;`0`][ARITH_RULE`4 MOD 4 = 0 MOD 4`]
THEN THAYTHEL_TAC 0[`6`;`2`][ARITH_RULE`6 MOD 4 = 2 MOD 4`]
THEN THAYTHEL_TAC 2[`3`][ARITH_RULE`3+1=4/\3+3=6`]]);;

let EXPAND_DIAG_4=prove_by_refinement(`scs_diag 4 i j ==> j MOD 4= (i+2) MOD 4`,
[REWRITE_TAC[SCS_DIAG_4_CASES;ARITH_RULE`i+2=SUC(SUC i)`]
THEN RESA_TAC;

MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`0`;`4`][Uxckfpe.ARITH_4_TAC]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`1`;`4`][Uxckfpe.ARITH_4_TAC];

MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`1`;`4`][Uxckfpe.ARITH_4_TAC]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`2`;`4`][Uxckfpe.ARITH_4_TAC];

MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`2`;`4`][Uxckfpe.ARITH_4_TAC]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`3`;`4`][Uxckfpe.ARITH_4_TAC];

MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`3`;`4`][Uxckfpe.ARITH_4_TAC]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`4`;`4`][Uxckfpe.ARITH_4_TAC]]);;


let EDGE_EQ_2_4I2=prove_by_refinement(`main_nonlinear_terminal_v11
==>(!i j. MMs_v39 scs_4I2 v/\
scs_diag 4 i j
/\ &3 <= dist (v i,v j) /\
&3 < dist (v (i + 1),v (j + 1))
==> dist(v (SUC i), v(SUC (SUC i)))= &2 )`,
[REPEAT RESA_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 ASSUME_TAC(ARITH_RULE`3<4/\ 0 + 4 - 1= 3/\ 0+1=1/\ SUC 0=1/\ SUC i + 4 - 1=i+4/\ ~(4=0)/\ 2 MOD 4=2/\ 0 MOD 4=0/\ (i + 1) + 2= i+3/\ 2+2=4/\ 3+2=5
/\ 3+1=4/\ 3+3=6/\ 6 MOD 4=2/\ 1 MOD 4=1/\ 3 MOD 4=3
/\ 2+1=3/\ 2+3=5`)
THEN ASSUME_TAC(ARITH_RULE`i+4= 1*4+i/\ SUC i+1=i+2/\ SUC i + 3= i+4`)
THEN ASSUME_TAC(SCS_4I2_IS_SCS)
THEN ASSUME_TAC(K_SCS_4I2)
THEN ASSUME_TAC(SCS_4I2_BASIC)
THEN ASSUME_TAC(h0_LT_B_SCS_4I2)
THEN MRESAL_TAC SCS_4I2_GENERIC[`v`][IN]
THEN MP_TAC CUXVZOZ
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`scs_4I2`;`FF`;`4`;`i+1`;`v`][GSYM ADD1;B_LE_CSTAB_SCS_4I2]
THEN MATCH_DICH_TAC 0
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHEL_TAC 0[`i+4`;`i`][MOD_MULT_ADD;]
THEN DICH_TAC 1
THEN REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4M8_prime;K_SCS_4M8;scs_prop_equ_v39;K_SCS_4I2]
THEN STRIP_TAC
THEN THAYTHEL_TAC 1[`i`;`SUC i`][B_LE_CSTAB_SCS_4I2]
THEN MP_TAC(REAL_ARITH`scs_b_v39 scs_4I2 i (SUC i) <= cstab
/\ dist (v i,v (SUC i)) <= scs_b_v39 scs_4I2 i (SUC i)
==> dist (v i,(v:num->real^3) (SUC i)) <= cstab`)
THEN ASM_SIMP_TAC[B_LE_CSTAB_SCS_4I2]
THEN STRIP_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN MRESAL_TAC SCS_4I2_3_LE_A[`i`;`v`;`i+2`][SCS_DIAG_4_ADD0]
THEN MP_TAC SCS_4I2_STRAIGHT
THEN RESA_TAC
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1]
THEN MRESA_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`scs_4I2`;`FF`;`v (SUC i)`;`v`;`SUC i`;`4`]
THEN THAYTHEL_ASM_TAC 2[`SUC i`][]
THEN MRESA_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`scs_4I2`;`FF`;`v (SUC(SUC i))`;`v`;`SUC (SUC i)`;`4`]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHEL_TAC 0[`1 * 4 + SUC i`;`SUC i`][MOD_MULT_ADD;]
THEN THAYTHEL_ASM_TAC (29-26)[`SUC (SUC i)`][]
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC i)=i+2`]
THEN REPEAT GEN_TAC
THEN REWRITE_TAC[SCS_DIAG_4_CASES;]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i':num`;`j':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN MRESAS_TAC Hexagons.PSORT_MOD[`4`;`1*4+i:num`;`i+2:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`;MOD_MULT_ADD]
THEN SYM_ASSUM_TAC
THEN MRESA_TAC MOD_ADD_MOD[`i`;`2`;`4`]
THEN SYM_ASSUM_TAC
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHEL_TAC 0[`i'`;`i' MOD 4`][MOD_MULT_ADD;]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHEL_TAC 0[`j'`;`j' MOD 4`][MOD_MULT_ADD;]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHES_TAC 0[`i+1`;`(i+1) MOD 4`][MOD_REFL;]
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`]
THEN SYM_ASSUM_TAC
THEN STRIP_TAC
THEN MP_TAC SCS_DIAG_ADD1
THEN RESA_TAC
THEN MRESA_TAC EXPAND_DIAG_4[`j+1`;`i+1`]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHES_TAC 0[`j+1`;`(i+3) MOD 4`][MOD_REFL;]
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC MOD_ADD_MOD[`i`;`3`;`4`]
THEN SYM_ASSUM_TAC
THEN STRIP_TAC
THEN DICH_TAC(39-4)
THEN ASM_REWRITE_TAC[];


MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`0+2=2`]
THEN SCS_TAC
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`0`;`4`][Uxckfpe.ARITH_4_TAC]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`2`;`4`][Uxckfpe.ARITH_4_TAC]
THEN ASM_SIMP_TAC[DIST_SYM];


MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`0+2=2`]
THEN SCS_TAC
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`1`;`4`][Uxckfpe.ARITH_4_TAC]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`3`;`4`][Uxckfpe.ARITH_4_TAC]
THEN ASM_SIMP_TAC[DIST_SYM];

MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`0+2=2`]
THEN SCS_TAC
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`2`;`4`][Uxckfpe.ARITH_4_TAC]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`0`;`4`][Uxckfpe.ARITH_4_TAC]
THEN ASM_SIMP_TAC[DIST_SYM];

MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`0+2=2`]
THEN SCS_TAC
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`3`;`4`][Uxckfpe.ARITH_4_TAC]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`1`;`4`][Uxckfpe.ARITH_4_TAC]
THEN ASM_SIMP_TAC[DIST_SYM]]);;


let EXPAND_DIAG_4_DIST=prove_by_refinement(`main_nonlinear_terminal_v11
==>(!i j. MMs_v39 scs_4I2 v/\
scs_diag 4 i j
/\ &3 <= dist (v i,v j) /\
&3 < dist (v (i + 1),v (j + 1))
==> &3 <= dist (v i,v (i+2)) /\
&3 < dist (v (i + 1),v (i + 3)))`,
[
REPEAT RESA_TAC
THEN MP_TAC EXPAND_DIAG_4
THEN RESA_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`];

MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHES_TAC 0[`i+2`;`j `][MOD_REFL;];

MP_TAC SCS_DIAG_ADD1
THEN RESA_TAC
THEN MRESA_TAC EXPAND_DIAG_4[`j+1`;`i+1`]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHES_TAC 0[`(i+3)`;`j+1`][MOD_REFL;ARITH_RULE`(i + 1) + 2= i+3`]]);;

let B_LE_CSTAB_SCS_4I2_prime=prove(`scs_a_v39 scs_4I2 (SUC i) (1 * 4 + i) = &2 /\
 scs_b_v39 scs_4I2 (SUC i) (1 * 4 + i) <= &2 * h0`,
SCS_TAC
THEN ASM_SIMP_TAC[MOD_MULT_ADD]
THEN REWRITE_TAC[h0;scs_diag;cstab]
THEN REPEAT RESA_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`SUC (1 * 4 + i)= 1 * 4 + SUC i`;MOD_MULT_ADD]
THEN REAL_ARITH_TAC);;


let EDGE_EQ_2_4I2_1=prove_by_refinement(`main_nonlinear_terminal_v11
==>(!i j. MMs_v39 scs_4I2 v/\
scs_diag 4 i j
/\ &3 <= dist (v i,v j) /\
&3 < dist (v (i + 1),v (j + 1))
==> dist(v (i), v((SUC i)))= &2 )`,
[REPEAT RESA_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 ASSUME_TAC(ARITH_RULE`3<4/\ 0 + 4 - 1= 3/\ 0+1=1/\ SUC 0=1/\ SUC i + 4 - 1=i+4/\ ~(4=0)/\ 2 MOD 4=2/\ 0 MOD 4=0/\ (i + 1) + 2= i+3/\ 2+2=4/\ 3+2=5
/\ 3+1=4/\ 3+3=6/\ 6 MOD 4=2/\ 1 MOD 4=1/\ 3 MOD 4=3
/\ 2+1=3/\ 2+3=5`)
THEN ASSUME_TAC(ARITH_RULE`i+4= 1*4+i/\ SUC i+1=i+2/\ SUC i + 3= i+4`)
THEN ASSUME_TAC(SCS_4I2_IS_SCS)
THEN ASSUME_TAC(K_SCS_4I2)
THEN ASSUME_TAC(SCS_4I2_BASIC)
THEN ASSUME_TAC(h0_LT_B_SCS_4I2)
THEN MRESAL_TAC SCS_4I2_GENERIC[`v`][IN]
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHEL_TAC 0[`i+4`;`i`][MOD_MULT_ADD;]
THEN MP_TAC CJBDXXN
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`scs_4I2`;`FF`;`4`;`i+1`;`v`][GSYM ADD1;B_LE_CSTAB_SCS_4I2]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN MATCH_DICH_TAC 0
THEN DICH_TAC 1
THEN REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4M8_prime;K_SCS_4M8;scs_prop_equ_v39;K_SCS_4I2]
THEN STRIP_TAC
THEN THAYTHEL_TAC 1[`SUC i`;`SUC(SUC i)`;][B_LE_CSTAB_SCS_4I2]
THEN MP_TAC(REAL_ARITH`scs_b_v39 scs_4I2 (SUC i) (SUC(SUC i)) <= cstab
/\ dist (v (SUC i), v(SUC(SUC i))) <= scs_b_v39 scs_4I2 (SUC i) (SUC(SUC i))
==> dist ((v:num->real^3) (SUC i),v(SUC(SUC i))) <= cstab`)
THEN ASM_SIMP_TAC[B_LE_CSTAB_SCS_4I2]
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[B_LE_CSTAB_SCS_4I2_prime]
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN MRESAL_TAC SCS_4I2_3_LE_A[`i`;`v`;`i+2`][SCS_DIAG_4_ADD0;ARITH_RULE`SUC(SUC i)=i+2`]
THEN MP_TAC SCS_4I2_STRAIGHT
THEN RESA_TAC
THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1]
THEN MRESA_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`scs_4I2`;`FF`;`v (SUC i)`;`v`;`SUC i`;`4`]
THEN THAYTHEL_ASM_TAC 2[`SUC i`][]
THEN MRESAL_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`scs_4I2`;`FF`;`v i`;`v`;`i`;`4`][ARITH_RULE`i+4-1=i+3`]
THEN REPEAT GEN_TAC
THEN REWRITE_TAC[SCS_DIAG_4_CASES;]
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i':num`;`j':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
THEN SYM_ASSUM_TAC
THEN MRESAS_TAC Hexagons.PSORT_MOD[`4`;`i+2:num`;`1*4+i:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`;MOD_MULT_ADD]
THEN SYM_ASSUM_TAC
THEN MRESA_TAC MOD_ADD_MOD[`i`;`2`;`4`]
THEN SYM_ASSUM_TAC
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHEL_TAC 0[`i'`;`i' MOD 4`][MOD_MULT_ADD;]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHEL_TAC 0[`j'`;`j' MOD 4`][MOD_MULT_ADD;]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHES_TAC 0[`i+1`;`(i+1) MOD 4`][MOD_REFL;]
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`]
THEN SYM_ASSUM_TAC
THEN STRIP_TAC
THEN MP_TAC SCS_DIAG_ADD1
THEN RESA_TAC
THEN MRESA_TAC EXPAND_DIAG_4[`j+1`;`i+1`]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHES_TAC 0[`j+1`;`(i+3) MOD 4`][MOD_REFL;]
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC MOD_ADD_MOD[`i`;`3`;`4`]
THEN SYM_ASSUM_TAC
THEN STRIP_TAC
THEN DICH_TAC(37-4)
THEN ASM_REWRITE_TAC[];


MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`0+2=2`]
THEN SCS_TAC
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`0`;`4`][Uxckfpe.ARITH_4_TAC]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`2`;`4`][Uxckfpe.ARITH_4_TAC]
THEN ASM_SIMP_TAC[DIST_SYM];


MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`0+2=2`]
THEN SCS_TAC
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`1`;`4`][Uxckfpe.ARITH_4_TAC]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`3`;`4`][Uxckfpe.ARITH_4_TAC]
THEN ASM_SIMP_TAC[DIST_SYM];

MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`0+2=2`]
THEN SCS_TAC
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`2`;`4`][Uxckfpe.ARITH_4_TAC]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`0`;`4`][Uxckfpe.ARITH_4_TAC]
THEN ASM_SIMP_TAC[DIST_SYM];


MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`0+2=2`]
THEN SCS_TAC
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`3`;`4`][Uxckfpe.ARITH_4_TAC]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`1`;`4`][Uxckfpe.ARITH_4_TAC]
THEN ASM_SIMP_TAC[DIST_SYM]]);;
let EDGE_EQ_2_4I2_2=prove(`main_nonlinear_terminal_v11
==>(!i j. MMs_v39 scs_4I2 v/\
scs_diag 4 i j
/\ &3 <= dist (v i,v j) /\
&3 < dist (v (i + 1),v (j + 1))
==>  dist (v (i+2) ,v (i + 3))= &2)`,
REPEAT STRIP_TAC
THEN MP_TAC EXPAND_DIAG_4_DIST
THEN RESA_TAC
THEN THAYTHE_TAC 0[`i`;`j`]
THEN MP_TAC EDGE_EQ_2_4I2_1
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`i+2`;`i`][ARITH_RULE`SUC(i+2)=i+3/\ (i+2)+1= i+3`]
THEN MATCH_DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN MP_TAC SCS_DIAG_4_ADD0
THEN REWRITE_TAC[scs_diag]
THEN RESA_TAC);;

let EDGE_EQ_2_4I2_3=prove(`main_nonlinear_terminal_v11
==>(!i j. MMs_v39 scs_4I2 v/\
scs_diag 4 i j
/\ &3 <= dist (v i,v j) /\
&3 < dist (v (i + 1),v (j + 1))
==>  dist (v (i) ,v (i + 3))= &2)`,
REPEAT STRIP_TAC
THEN MP_TAC EXPAND_DIAG_4_DIST
THEN RESA_TAC
THEN THAYTHE_TAC 0[`i`;`j`]
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHES_TAC 0[`1*4+i`;`i`][MOD_MULT_ADD]
THEN MP_TAC EDGE_EQ_2_4I2
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`i+2`;`i`][ARITH_RULE`SUC(SUC(i+2))=1*4+i/\ SUC (i+2)= i+3/\ (i+2)+1=i+3`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN MATCH_DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN MP_TAC SCS_DIAG_4_ADD0
THEN REWRITE_TAC[scs_diag]
THEN RESA_TAC);;


let EDGE_EQ_2_4I2_ALL=prove(`main_nonlinear_terminal_v11
==>( MMs_v39 scs_4I2 v/\
scs_diag 4 i j
/\ &3 <= dist (v i,v j) /\
&3 < dist (v (i + 1),v (j + 1))
==> (!i. dist (v (i) ,v (i+1))= &2))`,
REPEAT RESA_TAC
THEN MP_TAC EDGE_EQ_2_4I2_3
THEN RESA_TAC
THEN THAYTHE_TAC 0[`i`;`j`]
THEN MP_TAC EDGE_EQ_2_4I2_2
THEN RESA_TAC
THEN THAYTHE_TAC 0[`i`;`j`]
THEN MP_TAC EDGE_EQ_2_4I2_1
THEN RESA_TAC
THEN THAYTHE_TAC 0[`i`;`j`]
THEN MP_TAC EDGE_EQ_2_4I2
THEN RESA_TAC
THEN THAYTHE_TAC 0[`i`;`j`]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN REWRITE_TAC[ARITH_RULE`SUC i=i+1/\ (i + 1) + 1= i+2`]
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHES_TAC 0[`i`;`i MOD 4`][MOD_REFL;ARITH_RULE`~(4=0)`]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHES_TAC 0[`i+1`;`(i+1) MOD 4`][MOD_REFL;ARITH_RULE`~(4=0)`]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHES_TAC 0[`i+2`;`(i+2) MOD 4`][MOD_REFL;ARITH_RULE`~(4=0)`]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHES_TAC 0[`i+3`;`(i+3) MOD 4`][MOD_REFL;ARITH_RULE`~(4=0)`]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHES_TAC 0[`i'+1`;`(i'+1) MOD 4`][MOD_REFL;ARITH_RULE`~(4=0)`]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHES_TAC 0[`i'`;`(i') MOD 4`][MOD_REFL;ARITH_RULE`~(4=0)`]
THEN MRESAL_TAC MOD_ADD_MOD[`i`;`1`;`4`][ARITH_RULE`~(4=0)`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC MOD_ADD_MOD[`i'`;`1`;`4`][ARITH_RULE`~(4=0)`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC MOD_ADD_MOD[`i`;`2`;`4`][ARITH_RULE`~(4=0)`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC MOD_ADD_MOD[`i`;`3`;`4`][ARITH_RULE`~(4=0)`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`i' MOD 4<4==> i' MOD 4=0\/ i' MOD 4=1\/ i' MOD 4=2\/ i' MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC
THEN ASSUME_TAC(ARITH_RULE`2+1=3/\ 3+1=4/\ 2+3=5/\ 2+2=4/\ 3+3=6/\ 3+2=5/\ 6 MOD 4=2`)
THEN SCS_TAC
THEN ASM_SIMP_TAC[DIST_SYM]);;


let MM_4I2_IMP_4T2_4T1=prove_by_refinement (`main_nonlinear_terminal_v11
==>(!i j. 
    MMs_v39 scs_4I2 v/\
    scs_diag 4 i j /\
   dist(v i,v j)<= cstab ==>
    ~(MMs_v39 (scs_4T1)={})\/ ~(MMs_v39 (scs_4T2)={}))`,
[STRIP_TAC
THEN MATCH_MP_TAC ASSUME_MIN_DIAG
THEN REPEAT RESA_TAC
THEN MP_TAC SCS_DIAG_ADD1
THEN RESA_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN MRESA_TAC SCS_4I2_3_LE_A[`i`;`v`;`j`]
THEN MRESA_TAC SCS_4I2_3_LE_A[`i+1`;`v`;`j+1`]
THEN MP_TAC SCS_4I2_STRAIGHT_ALL
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`&3 <= dist ((v:num->real^3) (i + 1),v (j + 1))
==>  dist (v (i + 1),v (j + 1))= &3\/ &3< dist (v (i + 1),v (j + 1))`)
THEN RESA_TAC;


MP_TAC(REAL_ARITH`dist (v i,v j) <= dist (v (i + 1),v (j + 1))/\
&3 <= dist ((v:num->real^3) i,v j)/\ dist (v (i + 1),v (j + 1)) = &3
==> dist ((v:num->real^3) i,v j)= &3`)
THEN RESA_TAC
THEN MATCH_MP_TAC (SET_RULE`A==> B\/A`)
THEN 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_4I2`
THEN ASM_SIMP_TAC[SCS_4T2_IS_SCS;SCS_4I2_IS_SCS;SCS_4I2_BASIC;SCS_4T2_BASIC;K_SCS_4I2;K_SCS_4T2]
THEN STRIP_TAC
;




DICH_TAC(14-6)
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`(~(4<=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`~(4<=3)`]
THEN REPEAT STRIP_TAC
THEN MP_TAC DIST_DIAG_2_CASES_EQ_3
THEN ASM_REWRITE_TAC[IN]
THEN DISCH_TAC
THEN MP_TAC(SET_RULE`i' MOD 4 = j' MOD 4\/ ~(i' MOD 4 = j' MOD 4)`)
THEN RESA_TAC;


THAYTHE_TAC 3[`i':num`;`j':num`]
;


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

THAYTHE_TAC 4[`i':num`;`j':num`]
;



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

THAYTHE_TAC 5[`i':num`;`j':num`]
;

MRESAL_TAC SCS_DIAG_4_CASES[`i'`;`j'`][scs_diag]
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
;


THAYTHEL_ASM_TAC 0[`j'`;`0`][ARITH_RULE`0 MOD 4=0`]
THEN THAYTHEL_ASM_TAC 0[`i'`;`2`][ARITH_RULE`2 MOD 4=2`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[REAL_ARITH`a<=a`];


THAYTHEL_ASM_TAC 0[`j'`;`1`][ARITH_RULE`1 MOD 4=1`]
THEN THAYTHEL_ASM_TAC 0[`i'`;`3`][ARITH_RULE`3 MOD 4=3`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[REAL_ARITH`a<=a`];


THAYTHEL_ASM_TAC 0[`i'`;`0`][ARITH_RULE`0 MOD 4=0`]
THEN THAYTHEL_ASM_TAC 0[`j'`;`2`][ARITH_RULE`2 MOD 4=2`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[REAL_ARITH`a<=a`];


THAYTHEL_ASM_TAC 0[`i'`;`1`][ARITH_RULE`1 MOD 4=1`]
THEN THAYTHEL_ASM_TAC 0[`j'`;`3`][ARITH_RULE`3 MOD 4=3`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[REAL_ARITH`a<=a`];


SCS_TAC
THEN REAL_ARITH_TAC;


MATCH_MP_TAC(SET_RULE`A==> A\/ B`)
THEN MP_TAC EDGE_EQ_2_4I2_ALL
THEN RESA_TAC
THEN 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_4I2`
THEN ASM_SIMP_TAC[SCS_4T1_IS_SCS;SCS_4I2_IS_SCS;SCS_4I2_BASIC;SCS_4T1_BASIC;K_SCS_4I2;K_SCS_4T1]
THEN STRIP_TAC
;




DICH_TAC(14-6)
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`(~(4<=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`~(4<=3)`]
THEN REPEAT STRIP_TAC
THEN MP_TAC(SET_RULE`i' MOD 4 = j' MOD 4\/ ~(i' MOD 4 = j' MOD 4)`)
THEN RESA_TAC;


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


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


MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHES_TAC 0[`j'`;`SUC i'`][MOD_REFL;ARITH_RULE`~(4=0)`;ADD1;REAL_ARITH`a<=a`]
;




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



MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I2`;`v`]
THEN MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I2`][SCS_4I2_IS_SCS;K_SCS_4I2]
THEN THAYTHES_TAC 0[`i'`;`SUC j'`][MOD_REFL;ARITH_RULE`~(4=0)`;ADD1;REAL_ARITH`a<=a`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[REAL_ARITH`a<=a`]
;

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



SCS_TAC
THEN REAL_ARITH_TAC
;

]);;


let ARDBZYE=prove_by_refinement(`main_nonlinear_terminal_v11
==> scs_arrow_v39 { scs_4I2 } { scs_4T1, scs_4T2 }`,
[
STRIP_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;SET_RULE`a IN {b,c}<=> a=b\/ a=c`]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;

ASM_SIMP_TAC[SCS_4T1_IS_SCS;SCS_4T2_IS_SCS];

ASM_SIMP_TAC[SCS_4T1_IS_SCS;SCS_4T2_IS_SCS];

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

ASM_REWRITE_TAC[];

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

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

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

POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
THEN STRIP_TAC
THEN MP_TAC MM_4I2_IMP_4T2_4T1
THEN RESA_TAC
THEN THAYTHE_TAC 0[`i`;`j`]
THEN DICH_TAC 0
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN STRIP_TAC;

EXISTS_TAC`scs_4T1`
THEN REWRITE_TAC[]
THEN EXISTS_TAC`v':num->real^3`
THEN ASM_REWRITE_TAC[];

EXISTS_TAC`scs_4T2`
THEN REWRITE_TAC[]
THEN EXISTS_TAC`v':num->real^3`
THEN ASM_REWRITE_TAC[]]);;


let SCS_4I1_IMP_SCS_4I2= prove_by_refinement
(`main_nonlinear_terminal_v11
==>(!v. 
    v IN MMs_v39 scs_4I1 /\
    (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) ==>
    ~(MMs_v39 (scs_4I2)={}))`,
[
REWRITE_TAC[IN;SET_RULE`~(A={})<=> ?a. a IN A`]
THEN REPEAT STRIP_TAC
THEN MP_TAC SCS_4I1_IS_SCS
THEN STRIP_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I1`;`v`]
THEN ASSUME_TAC SCS_4I1_BASIC
THEN ASSUME_TAC K_SCS_4I1
THEN ASSUME_TAC SCS_4I2_BASIC
THEN ASSUME_TAC K_SCS_4I2
THEN ASSUME_TAC SCS_4I2_IS_SCS
THEN MP_TAC Rrcwnsj.RRCWNSJ
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4I1`;`v`][ARITH_RULE`3<4`;h0_LT_B_SCS_4I1;B_LE_CSTAB_SCS_4I1]
THEN MP_TAC JCYFMRP_V3
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4I1`;`v`][ARITH_RULE`3<4`;h0_LT_B_SCS_4I1;B_LE_CSTAB_SCS_4I1;IN;CARD_SCS_M_4I1;GSYM ADD1;A_LT_B_4I1]
THEN MP_TAC Jlxfdmj.JLXFDMJ
THEN RESA_TAC
THEN THAYTHES_TAC 0[`scs_4I1`;`v`;`i`][ARITH_RULE`3<4`;h0_LT_B_SCS_4I1;B_LE_CSTAB_SCS_4I1;IN;CARD_SCS_M_4I1;GSYM ADD1;A_LT_B_4I1;SCS_M_4I1;SET_RULE`~{} (j MOD 4)<=> T`]
THEN 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_4I1`
THEN ASM_SIMP_TAC[SCS_M_4I1]
THEN STRIP_TAC;


DICH_TAC(13-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`(~(4<=3))`;IN;K_SCS_4I1;K_SCS_4I2;scs_prop_equ_v39;]
THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
THEN SCS_TAC
THEN REWRITE_TAC[ARITH_RULE`~(4<=3)`]
THEN REPEAT STRIP_TAC;

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

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

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

THAYTHE_TAC (19-15)[`i'`;`j`];

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

THAYTHE_TAC (20-15)[`i'`;`j`];

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

SCS_TAC
THEN REAL_ARITH_TAC]);;

let SCS_4I1_STAB_DIAG=prove_by_refinement(`!v i j. 
     BBs_v39 scs_4I1 v/\
    scs_diag 4 i j /\
    dist(v i,v j) <= cstab
     ==>
    BBs_v39 (scs_stab_diag_v39 scs_4I1 i j) v`,
[
REWRITE_TAC[IN]
THEN REPEAT STRIP_TAC
THEN DICH_TAC 2
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_4I1;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I1;Terminal.FUNLIST_EXPLICIT;]
THEN ASM_SIMP_TAC[]
THEN REPEAT RESA_TAC
THEN SCS_TAC
THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
THEN RESA_TAC;

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

MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4I1`][SCS_4I1_IS_SCS;K_SCS_4I1]
THEN THAYTHE_TAC 0[`i'`;`i`]
THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4I1`][SCS_4I1_IS_SCS;K_SCS_4I1]
THEN THAYTHE_TAC 0[`j'`;`j`];

MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4I1`][SCS_4I1_IS_SCS;K_SCS_4I1]
THEN THAYTHE_TAC 0[`j'`;`i`]
THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4I1`][SCS_4I1_IS_SCS;K_SCS_4I1]
THEN THAYTHE_TAC 0[`i'`;`j`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]]);;


let STAB_4I1_SCS=prove(` scs_diag (scs_k_v39 scs_4I1) i j
==> is_scs_v39 (scs_stab_diag_v39 scs_4I1 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4I1 i j)`,
STRIP_TAC
THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4I1_IS_SCS;SCS_4I1_BASIC;K_SCS_4I1;
ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
THEN SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC);;
let MM_4I1_IMP_STAB_4I1=prove(`
     MMs_v39 scs_4I1 v/\
    scs_diag 4 i j /\
    dist(v i,v j) <= cstab
     ==>
    ~(MMs_v39 (scs_stab_diag_v39 scs_4I1 i j) ={})`,

STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_4I1`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I1`;`v`]
THEN ASSUME_TAC SCS_4I1_BASIC
THEN ASSUME_TAC K_SCS_4I1
THEN ASM_SIMP_TAC[SCS_4I1_IS_SCS;STAB_4I1_SCS;K_SCS_4I1;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_4I1_STAB_DIAG]
THEN REAL_ARITH_TAC);;

let SCS_4I1_ARROW_SCS_4I2_STAB_4I1=prove_by_refinement(
`main_nonlinear_terminal_v11
==> scs_arrow_v39 { scs_4I1 } ({scs_4I2} UNION {scs_stab_diag_v39 scs_4I1 i j| scs_diag 4 i j})`,
[STRIP_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;

ASM_SIMP_TAC[SCS_4I2_IS_SCS];

ASM_SIMP_TAC[STAB_4I1_SCS;K_SCS_4I1];

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

ASM_REWRITE_TAC[];


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

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

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

POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
THEN STRIP_TAC
THEN MP_TAC MM_4I1_IMP_STAB_4I1
THEN RESA_TAC
THEN DICH_TAC 0
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN STRIP_TAC
THEN EXISTS_TAC `scs_stab_diag_v39 scs_4I1 i j`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;

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

EXISTS_TAC`v':num->real^3`
THEN ASM_REWRITE_TAC[]]);;

let SET_STAB_4I1=prove(`{ scs_stab_diag_v39 scs_4I1 i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4I1 (i MOD 4) (j  MOD 4)| scs_diag 4 (i MOD 4) (j  MOD 4) }`,
 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
THEN MRESAL_TAC STAB_MOD[`scs_4I1`][SCS_4I1_IS_SCS;K_SCS_4I1]);;
let EXPAND_DIAG_4V=prove_by_refinement(
`scs_diag 4 i j <=> j MOD 4= (i+2) MOD 4`,
[ 
EQ_TAC
THEN ASM_SIMP_TAC[EXPAND_DIAG_4;]
THEN REWRITE_TAC[SCS_DIAG_4_CASES;ARITH_RULE`i+2=SUC(SUC i)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
THEN RESA_TAC;

MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`0`;`4`][Uxckfpe.ARITH_4_TAC]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`1`;`4`][Uxckfpe.ARITH_4_TAC];
                
MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`1`;`4`][Uxckfpe.ARITH_4_TAC]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`2`;`4`][Uxckfpe.ARITH_4_TAC];

MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`2`;`4`][Uxckfpe.ARITH_4_TAC]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`3`;`4`][Uxckfpe.ARITH_4_TAC];

MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`i`;`3`;`4`][Uxckfpe.ARITH_4_TAC]
THEN MRESAL_TAC Zithlqn.IMP_SUC_MOD_EQ[`SUC i`;`4`;`4`][Uxckfpe.ARITH_4_TAC]]);;

let EXPAND_STAB_DIAG_4=prove_by_refinement(`is_scs_v39 s /\scs_k_v39 s=4==>
{scs_stab_diag_v39 s (i MOD 4) (j MOD 4) | j MOD 4 =
                                                  (i MOD 4 + 2) MOD 4}=
{scs_stab_diag_v39 s (i+2) i| i<4} `,
[REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;UNION]
THEN STRIP_TAC
THEN GEN_TAC
THEN EQ_TAC
THEN RESA_TAC;

MRESAS_TAC STAB_MOD[`s`;`i MOD 4`;`i MOD 4 + 2`][MOD_REFL;ARITH_RULE`~(4=0)`]
THEN EXISTS_TAC`i MOD 4`
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`;STAB_SYM];

EXISTS_TAC`i+2`
THEN EXISTS_TAC`i:num`
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`;MOD_LT]
THEN MRESAS_TAC STAB_MOD[`s`;`(i + 2)`;`i`][SCS_5I1_IS_SCS;K_SCS_5I1;MOD_REFL;ARITH_RULE`~(4=0)`;MOD_LT]
THEN MRESAS_TAC MOD_ADD_MOD[`i+2`;`2`;`4`][ARITH_RULE`~(4=0)/\ 2 MOD 4=2/\ (i + 2) + 2= 1*4+i`;MOD_MULT_ADD;MOD_LT]]);;


let EXPAND_STAB_DIAG_4I1=prove(`
{scs_stab_diag_v39 scs_4I1 (i MOD 4) (j MOD 4) | j MOD 4 =
                                                  (i MOD 4 + 2) MOD 4}=
{scs_stab_diag_v39 scs_4I1 (i+2) i| i<4} `,
ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4I1_IS_SCS;K_SCS_4I1]);;


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


let EQ_DIAG_STAB_4I1_02=prove(`scs_arrow_v39
 {scs_stab_diag_v39 scs_4I1 (i + 2) i } 
 {scs_stab_diag_v39 scs_4I1 0 2}`,
MRESA_TAC STAB_SYM[`scs_4I1`;`2`;`0`]
THEN MP_TAC (GEN_ALL Wkeidft.WKEIDFT)
THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
THEN STRIP_TAC
THEN MATCH_DICH_TAC 0
THEN ASM_SIMP_TAC[ARITH_RULE`2 + i = (i + 2) + 0/\ 3<6/\ i+1= SUC i`;K_SCS_4I1
;h0_LT_B_SCS_4I1;h0_EQ_B_SCS_4I1;SCS_4I1_IS_SCS;SCS_4I1_BASIC]
THEN SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&2`
THEN EXISTS_TAC`&2 *h0`
THEN EXISTS_TAC`&2 *h0`
THEN EXISTS_TAC`&6`
THEN ASM_SIMP_TAC[]
THEN MP_TAC  SCS_DIAG_4_ADD0
THEN ASM_REWRITE_TAC[scs_diag]
THEN RESA_TAC
THEN ARITH_TAC);;


let SET_EQ_DIAG_STAB_4I1_02=prove(`scs_arrow_v39
 {scs_stab_diag_v39 scs_4I1 (i + 2) i |i<4} 
 {scs_stab_diag_v39 scs_4I1 0 2}`,
REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4I1 (i + 2) i |i=0\/i=1\/i=2\/i=3}
= {scs_stab_diag_v39 scs_4I1 (0 + 2) 0} UNION
{scs_stab_diag_v39 scs_4I1 (1 + 2) 1} UNION
{scs_stab_diag_v39 scs_4I1 (2 + 2) 2} UNION
{scs_stab_diag_v39 scs_4I1 (3 + 2) 3} 
`;]
THEN REPEAT (ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4I1 0 2}={scs_stab_diag_v39 scs_4I1 0 2} UNION {scs_stab_diag_v39 scs_4I1 0 2}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[EQ_DIAG_STAB_4I1_02]));;


let SET_EQ_DIAG_STAB_4I1=prove(`scs_arrow_v39
 { scs_stab_diag_v39 scs_4I1 i j| scs_diag 4 i j }
 {scs_stab_diag_v39 scs_4I1 0 2}`,
ASM_SIMP_TAC[SET_STAB_4I1]
THEN ASM_SIMP_TAC[EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`;EXPAND_STAB_DIAG_4I1;SET_EQ_DIAG_STAB_4I1_02]);;
let FYSSVEV= prove(`
main_nonlinear_terminal_v11
     ==>
scs_arrow_v39 { scs_4I1 } {scs_4I2, scs_stab_diag_v39 scs_4I1 0 2 }`,
STRIP_TAC
THEN MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`({scs_4I2} UNION {scs_stab_diag_v39 scs_4I1 i j| scs_diag 4 i j})`
THEN ASM_SIMP_TAC[SCS_4I1_ARROW_SCS_4I2_STAB_4I1;SET_RULE`{A,B}={A}UNION {B}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_4I1]
THEN MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[SCS_4I2_IS_SCS]);;

 end;;


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