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


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


module Hexagons = struct


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

open Hales_tactic;;

open Appendix;;





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

open Hales_tactic;;

open Appendix;;


open Zithlqn;;


open Xwitccn;;

open Ayqjtmd;;

open Jkqewgv;;


open Mtuwlun;;


open Uxckfpe;;
open Sgtrnaf;;

open Yxionxl;;

open Qknvmlb;;
open Odxlstcv2;;

open Yxionxl2;;
open Eyypqdw;;
open Ocbicby;;
open Imjxphr;;

open Nuxcoea;;
open Aursipd;;
open Cuxvzoz;;
open Rrcwnsj;;
open Tfitskc;;




let PSORT_5_EXPLICIT=
prove(` psort 5 (0,0)= (0,0)/\ psort 5 (1,1)= (1,1)/\ psort 5 (2,2)= (2,2)/\ psort 5 (3,3)= (3,3)/\ psort 5 (4,4)= (4,4)/\ psort 5 (0,1)= (0,1)/\ psort 5 (0,2)= (0,2)/\ psort 5 (0,3)= (0,3)/\ psort 5 (0,4)= (0,4)/\ psort 5 (1,0)= (0,1)/\ psort 5 (1,2)= (1,2)/\ psort 5 (1,3)= (1,3)/\ psort 5 (1,4)= (1,4)/\ psort 5 (2,0)= (0,2)/\ psort 5 (2,1)= (1,2)/\ psort 5 (2,3)= (2,3)/\ psort 5 (2,4)= (2,4)/\ psort 5 (3,0)= (0,3)/\ psort 5 (3,1)= (1,3)/\ psort 5 (3,2)= (2,3)/\ psort 5 (3,4)= (3,4)/\ psort 5 (4,0)= (0,4)/\ psort 5 (4,1)= (1,4)/\ psort 5 (4,2)= (2,4)/\ psort 5 (4,3)= (3,4)/\ psort 5 (4,5)= (0,4)/\ psort 4 (3,4)= (0,3)/\ psort 3 (2,0)= (0,2)/\ psort 3 (2,1)= (1,2)/\ psort 3 (1,0)= (0,1)`,
REWRITE_TAC[psort;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_4_TAC;LET_DEF;LET_END_DEF;MOD_5_EXPLICIT;ARITH_RULE`0<=a/\ ~(1<= 0)/\ ~(2<=0)/\ ~(3<=0)/\ ~(4<=0)/\a<=a/\ ~(2<=1)/\ ~(3<=2)/\ ~(4<=3)/\ ~(3<=1)/\ ~(4<=1)/\ ~(4<=2)/\ 2<=3`]);;
let scs_5M3 = new_definition`scs_5M3 = mk_unadorned_v39 5 (#0.616) 
    (funlist_v39 [(0,1),(&2*h0);(0,2),(cstab);(0,3),(cstab);(1,3),(cstab);(1,4),(cstab);(2,4),(cstab)] (&2) 5)
    (funlist_v39 [(0,1),cstab;(0,2),(&6);  (0,3),(&6);   (1,3),(&6);   (1,4),(&6);   (2,4),(&6)] (&2*h0) 5)`;;
let SCS_TAC= ASM_SIMP_TAC[scs_basic;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} j <=> {} i`;periodic2;scs_basic;unadorned_v39;scs_prop_equ_v39;LET_DEF;LET_END_DEF;scs_stab_diag_v39;scs_half_slice_v39; Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_5_TAC; scs_5M1;scs_3M1;scs_6I1;scs_3T1;scs_4M2;scs_6M1;scs_6T1;scs_5I1;scs_5I2;scs_5I3;scs_5M2;scs_4M6;scs_3T4;scs_5M3; Terminal.FUNLIST_EXPLICIT;Yrtafyh.PSORT_PERIODIC;PSORT_5_EXPLICIT; ARITH_RULE`SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6/\ SUC 6=7/\ SUC 7=8`];;
let sqrt8_LE_6=
prove(`sqrt8<= &6`,
REWRITE_TAC[sqrt8] THEN MATCH_MP_TAC REAL_LE_LSQRT THEN REAL_ARITH_TAC);;
let sqrt8_LE_CSTAB=
prove(`sqrt8<= #3.01`,
REWRITE_TAC[sqrt8] THEN MATCH_MP_TAC REAL_LE_LSQRT THEN REAL_ARITH_TAC);;
let LE_sqrt8_2=
prove(`&2<=sqrt8`,
REWRITE_TAC[sqrt8] THEN MATCH_MP_TAC REAL_LE_RSQRT THEN REAL_ARITH_TAC);;
let LE_sqrt8_2h0=
prove(`&2* #1.26<=sqrt8`,
REWRITE_TAC[sqrt8] THEN MATCH_MP_TAC REAL_LE_RSQRT THEN REAL_ARITH_TAC);;
let LT_sqrt8_2h0=
prove(`&2* #1.26<sqrt8`,
REWRITE_TAC[sqrt8] THEN MATCH_MP_TAC REAL_LT_RSQRT THEN REAL_ARITH_TAC);;
(******is_scs*********)
let MOD_PERIODIC=
prove(`~(k=0) ==> (i+k) MOD k = i MOD k/\ SUC (i+k) MOD k= SUC i MOD k`,
STRIP_TAC THEN ONCE_REWRITE_TAC[ARITH_RULE`i+k= 1*k+i`;] THEN SIMP_TAC[MOD_MULT_ADD;ARITH_RULE`SUC (1 * k + i) =(1 * k + SUC i)`]);;
let SCS_6I1_IS_SCS=
prove_by_refinement(`is_scs_v39 scs_6I1`,
[ REWRITE_TAC[scs_6I1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;] THEN SIMP_TAC[ARITH_RULE`~(6=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC ; GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; REAL_ARITH_TAC; REWRITE_TAC[h0] THEN REAL_ARITH_TAC; REWRITE_TAC[h0] THEN REAL_ARITH_TAC; ASM_SIMP_TAC[ARITH_RULE`~(6=0)`;MOD_LT;h0] THEN REAL_ARITH_TAC; REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY] THEN ARITH_TAC]);;
let DIST_LE_IMP_A_LE=
prove(`BBs_v39 s v /\ dist(v i,v j) <= a ==> scs_a_v39 s i j<= a`,
REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39] THEN REPEAT RESA_TAC THEN THAYTHE_TAC 2[`i`;`j`] THEN DICH_TAC 1 THEN DICH_TAC 1 THEN REAL_ARITH_TAC);;
let SCS_3M1_IS_SCS=
prove_by_refinement(`is_scs_v39 scs_3M1`,
[SIMP_TAC[scs_3M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.103 < #0.9`;periodic;SET_RULE`{} (i + j) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; ARITH_TAC; SCS_TAC; SCS_TAC; SCS_TAC; SCS_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;h0] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[MOD_LT;cstab;h0] THEN REAL_ARITH_TAC; MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\ (&2 * h0 < funlist_v39 [(0,1),cstab] (&2 * h0) 3 i (SUC i) \/ &2 < funlist_v39 [(0,1),&2 * h0] (&2) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`] THEN MATCH_DICH_TAC 0 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC]);;
let SCS_5M1_IS_SCS=
prove_by_refinement(`is_scs_v39 scs_5M1`,
[ SIMP_TAC[scs_5M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=5/\ 5<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.616 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`] THEN SUBGOAL_THEN`{i | i < 5 /\ (&2 * #1.26 < (if psort 5 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/ &2 < (if psort 5 (i,SUC i) = 0,1 then &2 * #1.26 else &2))} ={0}`ASSUME_TAC; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `]; ASM_REWRITE_TAC[Geomdetail.CARD_SING] THEN ARITH_TAC]);;
let SCS_5I1_IS_SCS=
prove_by_refinement(`is_scs_v39 scs_5I1`,
[ REWRITE_TAC[scs_5I1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(5=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=5/\ 5<=6/\a<=a/\ ~(5=4)/\ ~(6=0)`;d_tame;REAL_ARITH`#0.4819 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY] THEN ARITH_TAC]);;
let SCS_5I2_IS_SCS=
prove_by_refinement(`is_scs_v39 scs_5I2`,
[ REWRITE_TAC[scs_5I2;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(5=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=5/\ 5<=6/\a<=a/\ ~(5=4)/\ ~(6=0)`;d_tame;REAL_ARITH`#0.616 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`] THEN MP_TAC(SET_RULE`(j MOD 5 = SUC i MOD 5 \/ SUC j MOD 5 = i MOD 5)\/ ~(j MOD 5 = SUC i MOD 5 \/ SUC j MOD 5 = i MOD 5)`) THEN RESA_TAC THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`]; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN MP_TAC(SET_RULE`(j = SUC i MOD 5 \/ SUC j MOD 5 = i )\/ ~(j = SUC i MOD 5 \/ SUC j MOD 5 = i)`) THEN RESA_TAC THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2]; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY] THEN ARITH_TAC]);;
let SCS_5I3_IS_SCS=
prove_by_refinement(`is_scs_v39 scs_5I3`,
[ REWRITE_TAC[scs_5I3;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(5=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=5/\ 5<=6/\a<=a/\ ~(5=4)/\ ~(6=0)`;d_tame;REAL_ARITH`#0.616 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN MRESA_TAC Terminal.psort_sym[`5`;`i`;`j`]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN MRESA_TAC Terminal.psort_sym[`5`;`i`;`j`]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN MRESA_TAC Terminal.psort_sym[`5`;`i`;`j`]; SCS_TAC THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`] THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2h0] THEN MP_TAC(SET_RULE`psort 5 (i,j) = 0,1\/ ~(psort 5 (i,j) = 0,1)`) THEN RESA_TAC THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2h0] THEN REAL_ARITH_TAC; SCS_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2h0;MOD_LT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2h0;MOD_LT] THEN MP_TAC(SET_RULE`i MOD 5 = SUC i MOD 5\/ ~(i MOD 5 = SUC i MOD 5)`) THEN RESA_TAC THEN REWRITE_TAC[REAL_ARITH`&0 <= #3.01`] THEN MP_TAC(SET_RULE`psort 5 (i,SUC i) = 0,1\/ ~(psort 5 (i,SUC i) = 0,1)`) THEN RESA_TAC THEN REWRITE_TAC[sqrt8_LE_CSTAB] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`] THEN SUBGOAL_THEN`{i | i < 5 /\ (&2 * #1.26 < (if psort 5 (i,SUC i) = 0,1 then sqrt8 else &2 * #1.26) \/ &2 < (if psort 5 (i,SUC i) = 0,1 then &2 * #1.26 else &2))} ={0}`ASSUME_TAC; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;LT_sqrt8_2h0]; ASM_REWRITE_TAC[Geomdetail.CARD_SING] THEN ARITH_TAC]);;
let SCS_5M2_IS_SCS=
prove_by_refinement(`is_scs_v39 scs_5M2`,
[ SIMP_TAC[scs_5M2;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=5/\ 5<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.616 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`] THEN SUBGOAL_THEN`{i | i < 5 /\ (&2 * #1.26 < (if psort 5 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/ &2 < (if psort 5 (i,SUC i) = 0,1 then &2 else &2))} ={0}`ASSUME_TAC; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `]; ASM_REWRITE_TAC[Geomdetail.CARD_SING] THEN ARITH_TAC]);;
let SCS_4M2_IS_SCS=
prove_by_refinement(`is_scs_v39 scs_4M2`,
[ SIMP_TAC[scs_4M2;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.3789 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN REAL_ARITH_TAC; SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`] THEN SUBGOAL_THEN`{i | i < 4 /\ (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/ &2 < (if psort 4 (i,SUC i) = 0,1 then &2 * #1.26 else &2))} ={0}`ASSUME_TAC; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT]; ASM_REWRITE_TAC[Geomdetail.CARD_SING] THEN ARITH_TAC;]);;
let SCS_6M1_IS_SCS=
prove_by_refinement(`is_scs_v39 scs_6M1`,
[ REWRITE_TAC[scs_6M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;] THEN SIMP_TAC[ARITH_RULE`~(6=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; REAL_ARITH_TAC; REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; ASM_SIMP_TAC[ARITH_RULE`~(6=0)`;MOD_LT;h0;cstab] THEN REAL_ARITH_TAC; REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY] THEN ARITH_TAC]);;
let SCS_6T1_IS_SCS=
prove_by_refinement(`is_scs_v39 scs_6T1`,
[ REWRITE_TAC[scs_6T1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;] THEN REWRITE_TAC[ ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;] THEN SIMP_TAC[periodic;SET_RULE`{} (i + 6) <=> {} i` ;periodic2;ARITH_RULE`~(6=0)`;MOD_PERIODIC] THEN REPEAT RESA_TAC; GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`] THEN REWRITE_TAC[]; REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; ASM_SIMP_TAC[h0;cstab;MOD_LT] THEN REAL_ARITH_TAC; ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;] THEN REWRITE_TAC[REAL_ARITH`~(a<a)/\ ~(&2 * #1.26 < &2)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;h0] THEN ARITH_TAC]);;
(***************)
let SCS_6I1_BASIC=
prove(`scs_basic_v39 scs_6I1`,
SCS_TAC);;
let SCS_6T1_BASIC=
prove(`scs_basic_v39 scs_6T1`,
SCS_TAC);;
let SCS_6M1_BASIC=
prove(`scs_basic_v39 scs_6M1`,
SCS_TAC);;
let SCS_3M1_BASIC=
prove(`scs_basic_v39 scs_3M1`,
SCS_TAC);;
let SCS_3T1_BASIC=
prove(`scs_basic_v39 scs_3T1`,
SCS_TAC);;
let SCS_3T4_BASIC=
prove(`scs_basic_v39 scs_3T4`,
SCS_TAC);;
let SCS_5M1_BASIC=
prove(`scs_basic_v39 scs_5M1`,
SCS_TAC);;
let SCS_5M2_BASIC=
prove(`scs_basic_v39 scs_5M2`,
SCS_TAC);;
let SCS_5I1_BASIC=
prove(`scs_basic_v39 scs_5I1`,
SCS_TAC);;
let SCS_5I2_BASIC=
prove(`scs_basic_v39 scs_5I2`,
SCS_TAC);;
let SCS_5I3_BASIC=
prove(`scs_basic_v39 scs_5I3`,
SCS_TAC);;
let SCS_4M2_BASIC=
prove(`scs_basic_v39 scs_4M2`,
SCS_TAC);;
let SCS_4M6_BASIC=
prove(`scs_basic_v39 scs_4M6'`,
SCS_TAC);;
(******************)
let K_SCS_6I1=
prove(`scs_k_v39 scs_6I1=6`,
SCS_TAC);;
let K_SCS_6T1=
prove(`scs_k_v39 scs_6T1=6`,
SCS_TAC);;
let K_SCS_3M1=
prove(`scs_k_v39 scs_3M1=3`,
SCS_TAC);;
let K_SCS_3T1=
prove(`scs_k_v39 scs_3T1=3`,
SCS_TAC);;
let K_SCS_3T4=
prove(`scs_k_v39 scs_3T4=3`,
SCS_TAC);;
let K_SCS_5M1=
prove(`scs_k_v39 scs_5M1=5`,
SCS_TAC);;
let K_SCS_5M2=
prove(`scs_k_v39 scs_5M2=5`,
SCS_TAC);;
let K_SCS_5I1=
prove(`scs_k_v39 scs_5I1=5`,
SCS_TAC);;
let K_SCS_5I2=
prove(`scs_k_v39 scs_5I2=5`,
SCS_TAC);;
let K_SCS_5I3=
prove(`scs_k_v39 scs_5I3=5`,
SCS_TAC);;
let K_SCS_4M2=
prove(`scs_k_v39 scs_4M2=4`,
SCS_TAC);;
let K_SCS_4M6=
prove(`scs_k_v39 scs_4M6'=4`,
SCS_TAC);;
(******************)
let J_SCS_3M1=
prove(`scs_J_v39 (scs_prop_equ_v39 scs_3M1 i) i1 j= F`,
SCS_TAC);;
let J_SCS_3T4=
prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T4 i) i1 j= F`,
SCS_TAC);;
let J_SCS_5M1=
prove(`scs_J_v39 (scs_prop_equ_v39 scs_5M1 i) i1 j= F`,
SCS_TAC );;
let J_SCS_5I1=
prove(`scs_J_v39 (scs_prop_equ_v39 scs_5I1 i) i1 j= F`,
SCS_TAC );;
let J_SCS_5I2=
prove(`scs_J_v39 (scs_prop_equ_v39 scs_5I2 i) i1 j= F`,
SCS_TAC );;
let J_SCS_5I3=
prove(`scs_J_v39 (scs_prop_equ_v39 scs_5I3 i) i1 j= F`,
SCS_TAC );;
let J_SCS_4M2=
prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M2 i) i1 j= F`,
SCS_TAC );;
let J_SCS_4M6=
prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M6' i) i1 j= F`,
SCS_TAC );;
(*******************)
let BASIC_MM_EQ_BBPRIME2=
prove(`scs_basic_v39 s ==> MMs_v39 s = BBprime2_v39 s `,
SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;MMs_v39;Ayqjtmd.unadorned_MMs]);;
let BASIC_MM_EQ_BBPRIME2_POINT=
prove(`scs_basic_v39 s ==> MMs_v39 s v= BBprime2_v39 s v`,
SIMP_TAC [BASIC_MM_EQ_BBPRIME2]);;
let DIST_PSORT=
prove(`periodic v (k)/\ ~(k=0) /\ psort (k) (i,j) = psort (k) (i',j') ==> dist (v i',v j')= dist (v i,v j)`,
REWRITE_TAC[psort;LET_DEF;LET_END_DEF;] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC(SET_RULE`i MOD k<= j MOD k\/ ~(i MOD k<= j MOD k)`) THEN RESA_TAC THEN MP_TAC(SET_RULE`i' MOD k<= j' MOD k\/ ~(i' MOD k<= j' MOD k)`) THEN RESA_TAC THEN REWRITE_TAC[PAIR_EQ] THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k`;`v`][ARITH_RULE`~(4=0)`;periodic] THEN THAYTHEL_ASM_TAC 0[`i`][] THEN THAYTHEL_ASM_TAC 0[`i'`][] THEN THAYTHEL_ASM_TAC 0[`j`][] THEN THAYTHEL_ASM_TAC 0[`j'`][] THEN SIMP_TAC[DIST_SYM]);;
let STAB_BB=
prove(`is_scs_v39 s/\ dist(v i,v j) <= cstab/\ BBs_v39 s v ==> BBs_v39 (scs_stab_diag_v39 s i j) v`,
SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39] THEN REPEAT RESA_TAC THEN THAYTHE_TAC 1[`i'`;`j'`] THEN DICH_TAC 0 THEN DICH_TAC 4 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j')\/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`) THEN RESA_TAC THEN MP_TAC Wkeidft.PROPERTY_OF_K_SCS THEN RESA_TAC THEN ABBREV_TAC`k= scs_k_v39 s` THEN MRESA_TAC DIST_PSORT[`k`;`i'`;`j'`;`i`;`v`;`j`] THEN RESA_TAC);;
let SCS_K_D_A_STAB_EQ=
prove(`scs_d_v39 (scs_stab_diag_v39 s i j) =scs_d_v39 s /\ scs_k_v39 (scs_stab_diag_v39 s i j) =scs_k_v39 s /\(!i' j'. scs_a_v39 (scs_stab_diag_v39 s i j) i' j'= scs_a_v39 s i' j')`,
let DIAG_SCS_M_EQ=
prove(`is_scs_v39 s/\ scs_diag (scs_k_v39 s) i j==> scs_M s = scs_M (scs_stab_diag_v39 s i j)`,
SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;] THEN STRIP_TAC THEN MP_TAC Wkeidft.PROPERTY_OF_K_SCS THEN RESA_TAC THEN ASM_SIMP_TAC[Yrtafyh.DIAG_NOT_PSORT]);;
let DIAD_PSORT_IMP_DIAD=
prove_by_refinement(`scs_diag k i j /\ ~(k=0) /\ psort k (i',j') = psort k (i,j) ==> scs_diag k i' j'`,
[REWRITE_TAC[scs_diag;psort;LET_DEF;LET_END_DEF] THEN STRIP_TAC THEN DICH_TAC 0 THEN MP_TAC(SET_RULE`i MOD k<= j MOD k\/ ~(i MOD k<= j MOD k)`) THEN RESA_TAC THEN MP_TAC(SET_RULE`i' MOD k<= j' MOD k\/ ~(i' MOD k<= j' MOD k)`) THEN RESA_TAC THEN REWRITE_TAC[PAIR_EQ] THEN RESA_TAC; MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`i`;`k`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`j`;`k`] ; MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`j`;`k`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`i`;`k`] ; MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`j`;`k`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`i`;`k`] ; MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`i`;`k`] THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`j`;`k`] ]);;
let PEDSLGV1= 
prove( `!v i j. v IN MMs_v39 scs_6I1 /\ scs_diag 6 i j /\ dist(v i,v j) <= cstab ==> v IN MMs_v39 (scs_stab_diag_v39 scs_6I1 i j)`,
REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN MP_TAC SCS_6I1_IS_SCS THEN STRIP_TAC THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6I1`;`v`] THEN MRESA_TAC DIST_LE_IMP_A_LE[`v`;`scs_6I1`;`i`;`j`;`cstab`] THEN ASSUME_TAC SCS_6I1_BASIC THEN ASSUME_TAC K_SCS_6I1 THEN MRESAL_TAC Yrtafyh.YRTAFYH[`scs_6I1`;`i`;`j`][ARITH_RULE`3<6`;] THEN MP_TAC Ppbtydq.MXQTIED THEN REWRITE_TAC[IN] THEN STRIP_TAC THEN MATCH_DICH_TAC 0 THEN EXISTS_TAC`scs_6I1` THEN ASM_SIMP_TAC[STAB_BB;SCS_K_D_A_STAB_EQ;DIAG_SCS_M_EQ;REAL_ARITH`a<=a`] THEN REPEAT GEN_TAC THEN REWRITE_TAC[scs_stab_diag_v39;scs_6I1;scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;CS_ADJ] THEN MP_TAC(SET_RULE`psort 6 (i,j) = psort 6 (i',j')\/ ~(psort 6 (i,j) = psort 6 (i',j'))`) THEN RESA_TAC THENL[ MRESAL_TAC DIAD_PSORT_IMP_DIAD[`i`;`j`;`6`;`i'`;`j'`][ARITH_RULE`~(6=0)`] THEN DICH_TAC 0 THEN REWRITE_TAC[scs_diag;cstab] THEN RESA_TAC THEN REAL_ARITH_TAC; REAL_ARITH_TAC]);;
(****************************) (****************************) (****************************) (****************************)
let K_SCS_6M1=
prove(`scs_k_v39 scs_6M1=6/\ scs_d_v39 scs_6M1 = scs_d_v39 scs_6I1`,
REWRITE_TAC[scs_6I1;scs_6M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39]);;
let D_6M1_EQ_6I1=
prove(` scs_d_v39 scs_6M1 = scs_d_v39 scs_6I1 `,
REWRITE_TAC[scs_6I1;scs_6M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39]);;
let A_6M1_EQ_6I1_EDGE=
prove(`(!i j. scs_a_v39 scs_6M1 i (SUC i) = scs_a_v39 scs_6I1 i (SUC i))`,
REWRITE_TAC[scs_6I1;scs_6M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39]);;
let SCS_M_6I1_EQ_6M1=
prove(`scs_M scs_6I1 = scs_M scs_6M1`,
REWRITE_TAC[scs_6I1;scs_6M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39;scs_M]);;
let BB_6I1_IS_BB_6M1=
prove_by_refinement(`BBs_v39 scs_6I1 v/\ (!i j. scs_diag 6 i j ==> cstab <= dist(v i,v j)) ==> BBs_v39 scs_6M1 v`,
[ SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_6I1;scs_6M1;CS_ADJ;scs_diag] THEN REPEAT RESA_TAC THEN MP_TAC(SET_RULE`i MOD 6= j MOD 6\/ ~(i MOD 6= j MOD 6)`) THEN RESA_TAC; THAYTHE_TAC (5-2)[`i`;`j`]; MP_TAC(SET_RULE`SUC i MOD 6= j MOD 6\/ ~(SUC i MOD 6= j MOD 6)`) THEN RESA_TAC; THAYTHE_TAC (6-2)[`i`;`j`]; MP_TAC(SET_RULE`i MOD 6= SUC j MOD 6\/ ~(i MOD 6= SUC j MOD 6)`) THEN RESA_TAC; THAYTHE_TAC (7-2)[`i`;`j`]; THAYTHE_TAC (7-4)[`i`;`j`]; THAYTHE_TAC (5-2)[`i`;`j`]; MP_TAC(SET_RULE`SUC i MOD 6= j MOD 6\/ ~(SUC i MOD 6= j MOD 6)`) THEN RESA_TAC; THAYTHE_TAC (6-2)[`i`;`j`]; MP_TAC(SET_RULE`i MOD 6= SUC j MOD 6\/ ~(i MOD 6= SUC j MOD 6)`) THEN RESA_TAC; THAYTHE_TAC (7-2)[`i`;`j`]; THAYTHE_TAC (7-4)[`i`;`j`]]);;
let A_6I1_LE_A_6M1=
prove(`scs_a_v39 scs_6I1 i j <= scs_a_v39 scs_6M1 i j`,
REWRITE_TAC[scs_6I1;scs_6M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39;h0;cstab] THEN REAL_ARITH_TAC);;
let B_6I1_LE_B_6M1=
prove(`scs_b_v39 scs_6M1 i j = scs_b_v39 scs_6I1 i j`,
REWRITE_TAC[scs_6I1;scs_6M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39;h0;cstab] THEN REAL_ARITH_TAC);;
let PEDSLGV2= 
prove(`!v. v IN MMs_v39 scs_6I1 /\ (!i j. scs_diag 6 i j ==> cstab <= dist(v i,v j)) ==> v IN MMs_v39 (scs_6M1)`,
REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN MP_TAC SCS_6I1_IS_SCS THEN STRIP_TAC THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6I1`;`v`] THEN ASSUME_TAC SCS_6I1_BASIC THEN ASSUME_TAC K_SCS_6I1 THEN ASSUME_TAC SCS_6M1_BASIC THEN ASSUME_TAC K_SCS_6M1 THEN MP_TAC SCS_6M1_IS_SCS THEN STRIP_TAC THEN MP_TAC Ppbtydq.MXQTIED THEN REWRITE_TAC[IN] THEN STRIP_TAC THEN MATCH_DICH_TAC 0 THEN EXISTS_TAC`scs_6I1` THEN ASM_SIMP_TAC[D_6M1_EQ_6I1;A_6M1_EQ_6I1_EDGE;SCS_M_6I1_EQ_6M1;BB_6I1_IS_BB_6M1;A_6I1_LE_A_6M1;B_6I1_LE_B_6M1;REAL_ARITH`a<=a`]);;
(****************************) (****************************) (****************************) (****************************)
let STAB_6I1_SCS=
prove(` scs_diag (scs_k_v39 scs_6I1) i j ==> is_scs_v39 (scs_stab_diag_v39 scs_6I1 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_6I1 i j)`,
STRIP_TAC THEN MATCH_MP_TAC Yrtafyh.YRTAFYH THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_6I1_IS_SCS;SCS_6I1_BASIC;K_SCS_6I1; ARITH_RULE`3<6`;LET_DEF;LET_END_DEF;scs_6I1;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab] THEN REAL_ARITH_TAC);;
let SCS_DIAG_SCS_6I1_02=
prove(`scs_diag (scs_k_v39 scs_6I1) 0 2`,
REWRITE_TAC[K_SCS_6I1;scs_diag] THEN ARITH_TAC);;
let SCS_DIAG_SCS_6I1_03=
prove(`scs_diag (scs_k_v39 scs_6I1) 0 3`,
REWRITE_TAC[K_SCS_6I1;scs_diag] THEN ARITH_TAC);;
let BASIC_HALF_SLICE_STAB=
prove(`scs_basic_v39 s ==> scs_basic_v39 (scs_half_slice_v39 (scs_stab_diag_v39 s i j) p q d' F)`,
let D_HALF_SLICE=
prove(`scs_d_v39 (scs_half_slice_v39 (scs_stab_diag_v39 s i j) p q d' mkj)=d'`,
SCS_TAC);;
let BAISC_PROP_EQU=
prove(`scs_basic_v39 s ==> scs_basic_v39 (scs_prop_equ_v39 s i)`,
SCS_TAC THEN SET_TAC[]);;
let K_SCS_PROP_EUQ=
prove(`scs_k_v39 (scs_prop_equ_v39 s i)= scs_k_v39 s`,
SCS_TAC);;
let AQICLXA_SLICE=
prove_by_refinement(`scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 2 } { scs_prop_equ_v39 scs_3M1 1, scs_prop_equ_v39 scs_5M1 1}`,
[MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI) THEN ASM_SIMP_TAC[SCS_DIAG_SCS_6I1_02;STAB_6I1_SCS;SCS_K_D_A_STAB_EQ;] THEN EXISTS_TAC`0` THEN EXISTS_TAC`2` THEN ASM_SIMP_TAC[SCS_DIAG_SCS_6I1_02] THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ] THEN REPEAT RESA_TAC; REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;] THEN STRIP_TAC THEN MATCH_MP_TAC scs_inj THEN ASM_SIMP_TAC[SCS_3M1_BASIC;SCS_5M1_BASIC;SCS_6I1_BASIC;J_SCS_5M1;BASIC_HALF_SLICE_STAB;J_SCS_3M1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ] THEN STRIP_TAC; ASM_SIMP_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1] THEN ARITH_TAC; STRIP_TAC; ASM_SIMP_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1;scs_6I1;scs_3M1; ARITH_RULE`(2 + 1 + 6 - 0) MOD 6= 3/\ 0 MOD 6=0/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort] THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;] THEN RESA_TAC THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;Uxckfpe.ARITH_3_TAC] THEN SIMP_TAC[ARITH_RULE`~(0=2)/\ ~(0=1)/\ 0<=1/\ ~(1=2)`;SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][Uxckfpe.ARITH_3_TAC] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][Uxckfpe.ARITH_3_TAC] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][Uxckfpe.ARITH_3_TAC] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][Uxckfpe.ARITH_3_TAC] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][Uxckfpe.ARITH_3_TAC] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][Uxckfpe.ARITH_3_TAC] THEN ASM_SIMP_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2`;PAIR_EQ;Uxckfpe.ARITH_3_TAC]; ASM_SIMP_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1;scs_6I1;scs_3M1; ARITH_RULE`(2 + 1 + 6 - 0) MOD 6= 3/\ 0 MOD 6=0/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort] THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;] THEN RESA_TAC THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;Uxckfpe.ARITH_3_TAC] THEN SIMP_TAC[ARITH_RULE`~(0=2)/\ ~(0=1)/\ 0<=1/\ ~(1=2)/\ 0<=2/\ 0<=0`;SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][Uxckfpe.ARITH_3_TAC] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][Uxckfpe.ARITH_3_TAC] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][Uxckfpe.ARITH_3_TAC] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][Uxckfpe.ARITH_3_TAC] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][Uxckfpe.ARITH_3_TAC] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][Uxckfpe.ARITH_3_TAC] THEN ASM_SIMP_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2`;PAIR_EQ;Uxckfpe.ARITH_3_TAC]; ASM_SIMP_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1] THEN ARITH_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1;scs_6I1;scs_3M1; ARITH_RULE`(0 + 1 + 6 - 2) MOD 6= 5/\ 2 MOD 6=2/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort] THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 5<5==> x MOD 5=0\/ x MOD 5=1\/ x MOD 5=2\/ x MOD 5=3\/ x MOD 5=4`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_5_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 5<5==> x' MOD 5=0\/ x' MOD 5=1\/ x' MOD 5=2\/ x' MOD 5=3\/ x' MOD 5=4`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_5_TAC;DIVISION;ARITH_RULE`5-1=4`] THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`0`;`1`][ARITH_RULE`~(5=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`1`;`1`][ARITH_RULE`~(5=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`2`;`1`][ARITH_RULE`~(5=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`3`;`1`][ARITH_RULE`~(5=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`4`;`1`][ARITH_RULE`~(5=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`0`;`1`][ARITH_RULE`~(5=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`1`;`1`][ARITH_RULE`~(5=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`2`;`1`][ARITH_RULE`~(5=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`3`;`1`][ARITH_RULE`~(5=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`4`;`1`][ARITH_RULE`~(5=0)`] THEN ASM_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\ 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC] THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1) /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC]; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[cstab] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN REWRITE_TAC[J_SCS_3M1]]);;
let FZIOTEF_UNION = 
prove_by_refinement( `!S1 S2 S3 S4. scs_arrow_v39 S1 S2 /\ scs_arrow_v39 S3 S4 ==> scs_arrow_v39 (S1 UNION S3) (S2 UNION S4)`,
(* {{{ proof *) [ REWRITE_TAC[scs_arrow_v39;UNION;IN_ELIM_THM]; REPEAT WEAKER_STRIP_TAC; ASM_REWRITE_TAC[]; BY(ASM_MESON_TAC[]) ]);;
(* }}} *)
let  PROP_EQU_IS_SCS=
prove(`is_scs_v39 s ==> is_scs_v39 (scs_prop_equ_v39 s i)`,
MRESA_TAC PROP_EQU_IS_SCS[`scs_k_v39 s`;`s`;`i`;`scs_prop_equ_v39 s i`]);;
let AQICLXA=
prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 2 } { scs_3M1, scs_5M1 }`,
MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_3M1 1, scs_prop_equ_v39 scs_5M1 1}` THEN ASM_SIMP_TAC[AQICLXA_SLICE] THEN REWRITE_TAC[SET_RULE`{a,b}= {a}UNION {b}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC THENL[ MRESAS_TAC PRO_EQU_ID[`scs_3M1`;`3`;`2`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`3-2 MOD 3=1`] THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1 1`;`2`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`3-1=2`] THEN DICH_TAC 0 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]); MRESAS_TAC PRO_EQU_ID[`scs_5M1`;`5`;`4`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_5M1_IS_SCS;K_SCS_5M1;ARITH_RULE`5-4 MOD 5=1`] THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_5M1 1`;`4`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_5M1_IS_SCS;K_SCS_5M1;ARITH_RULE`3-1=2`] THEN DICH_TAC 0 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])]);;
(****************************) (****************************) (****************************) (****************************)
let FUNOUYH_SLICE=
prove_by_refinement(`scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 3 } { scs_prop_equ_v39 scs_4M2 1, scs_prop_equ_v39 scs_4M2 1}`,
[ MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI) THEN ASM_SIMP_TAC[SCS_DIAG_SCS_6I1_03;STAB_6I1_SCS;SCS_K_D_A_STAB_EQ;] THEN EXISTS_TAC`0` THEN EXISTS_TAC`3` THEN ASM_SIMP_TAC[SCS_DIAG_SCS_6I1_03] THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ] THEN REPEAT RESA_TAC; REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;] THEN STRIP_TAC THEN MATCH_MP_TAC scs_inj THEN ASM_SIMP_TAC[BAISC_PROP_EQU;K_SCS_PROP_EUQ;BASIC_HALF_SLICE_STAB;SCS_4M2_BASIC;J_SCS_4M2;D_HALF_SLICE;SCS_6I1_BASIC;K_SCS_4M2] THEN STRIP_TAC; ASM_SIMP_TAC[scs_half_slice_v39;scs_4M2;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1] THEN ARITH_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[scs_half_slice_v39;scs_4M2;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2;scs_6I1;scs_3M1; ARITH_RULE`(3 + 1 + 6 - 0) MOD 6= 4/\ 0 MOD 6=0/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort] THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/ x' MOD 4=3`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`] THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`] THEN ASM_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\ 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC] THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1) /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]; ASM_SIMP_TAC[scs_half_slice_v39;scs_4M2;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1] THEN ARITH_TAC; STRIP_TAC THEN ASM_REWRITE_TAC[scs_half_slice_v39;scs_4M2;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2;scs_6I1;scs_3M1; ARITH_RULE`(0 + 1 + 6 - 3) MOD 6= 4/\ 3 MOD 6=3/\ a+0=a`;scs_prop_equ_v39] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort] THEN REPEAT GEN_TAC THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/ x' MOD 4=3`) THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`] THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`] THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`] THEN ASM_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\ 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC] THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1) /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[cstab;h0] THEN REAL_ARITH_TAC; SCS_TAC THEN REWRITE_TAC[cstab;h0] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN REWRITE_TAC[J_SCS_4M2]]);;
let FZIOTEF=
prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 3 } { scs_4M2}`,
MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_4M2 1, scs_prop_equ_v39 scs_4M2 1}` THEN ASM_SIMP_TAC[FUNOUYH_SLICE] THEN REWRITE_TAC[SET_RULE`{a,a}= {a}`] THEN MRESAS_TAC PRO_EQU_ID[`scs_4M2`;`4`;`3`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_4M2_IS_SCS;K_SCS_4M2;ARITH_RULE`4-3 MOD 4=1`] THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M2 1`;`3`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_4M2_IS_SCS;K_SCS_4M2;ARITH_RULE`3-1=2`] THEN DICH_TAC 0 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]));;
(****************************) (****************************) (****************************) (****************************)
let h0_LT_B_SCS_6M1=
prove(` (!i j. scs_diag 6 i j ==> &4 * h0 < scs_b_v39 scs_6M1 i j) /\ (!i j. scs_diag 6 i j ==> scs_a_v39 scs_6M1 i j <= cstab)`,
SCS_TAC THEN REWRITE_TAC[h0;scs_diag] THEN REPEAT RESA_TAC THEN REAL_ARITH_TAC);;
let h0_LT_B_SCS_6I1=
prove( `(!i j. scs_diag 6 i j ==> &4 * h0 < scs_b_v39 scs_6I1 i j) /\ (!i j. scs_diag 6 i j ==> scs_a_v39 scs_6I1 i j <= cstab)`,
SCS_TAC THEN REWRITE_TAC[h0;scs_diag;cstab] THEN REPEAT RESA_TAC THEN REAL_ARITH_TAC);;
let h0_LT_B_SCS_5I1=
prove(` (!i j. scs_diag 5 i j ==> &4 * h0 < scs_b_v39 scs_5I1 i j) /\ (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5I1 i j <= cstab)`,
SCS_TAC THEN REWRITE_TAC[h0;scs_diag;cstab] THEN REPEAT RESA_TAC THEN REAL_ARITH_TAC);;
let h0_LT_B_SCS_5I2=
prove(` (!i j. scs_diag 5 i j ==> &4 * h0 < scs_b_v39 scs_5I2 i j) /\ (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5I2 i j <= cstab)`,
SCS_TAC THEN REWRITE_TAC[h0;scs_diag;cstab] THEN REPEAT RESA_TAC THEN MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC);;
let h0_LT_B_SCS_5M2=
prove(` (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5M2 i j <= cstab)`,
SCS_TAC THEN REWRITE_TAC[h0;scs_diag;cstab] THEN REPEAT RESA_TAC THEN REAL_ARITH_TAC);;
let h0_LT_B_SCS_5M1=
prove(` (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5M1 i j <= cstab)`,
SCS_TAC THEN REWRITE_TAC[h0;scs_diag;cstab] THEN REPEAT RESA_TAC THEN MP_TAC sqrt8_LE_CSTAB THEN REAL_ARITH_TAC);;
(***************)
let h0_EQ_B_SCS_6I1=
prove( `(!i j. scs_diag 6 i j ==> scs_b_v39 scs_6I1 i j= &6) /\ (!i j. scs_diag 6 i j ==> scs_a_v39 scs_6I1 i j= &2 *h0)`,
SCS_TAC THEN REWRITE_TAC[h0;scs_diag;cstab] THEN REPEAT RESA_TAC);;
let h0_EQ_B_SCS_5I1=
prove( `(!i j. scs_diag 5 i j ==> scs_b_v39 scs_5I1 i j= &6) /\ (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5I1 i j= &2 *h0)`,
SCS_TAC THEN REWRITE_TAC[h0;scs_diag;cstab] THEN REPEAT RESA_TAC);;
let h0_EQ_B_SCS_5I2=
prove( `(!i j. scs_diag 5 i j ==> scs_b_v39 scs_5I2 i j= &6) /\ (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5I2 i j= sqrt8)`,
SCS_TAC THEN REWRITE_TAC[h0;scs_diag;cstab] THEN REPEAT RESA_TAC);;
let B_LE_CSTAB_6M1=
prove(` (!i. scs_b_v39 scs_6M1 i (SUC i) <= cstab)/\ (!i. scs_b_v39 scs_6M1 i (SUC i) <= &2*h0)/\ (!i. &2< scs_b_v39 scs_6M1 i (SUC i) )/\ (!i. scs_a_v39 scs_6M1 i (SUC i) = &2)`,
SCS_TAC THEN SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;h0;cstab] THEN REAL_ARITH_TAC);;
let B_LE_CSTAB_5I1=
prove(` (!i. scs_b_v39 scs_5I1 i (SUC i) <= cstab)/\ (!i. scs_b_v39 scs_5I1 i (SUC i) <= &2*h0)/\ (!i. &2< scs_b_v39 scs_5I1 i (SUC i) )/\ (!i. scs_a_v39 scs_5I1 i (SUC i) = &2) `,
SCS_TAC THEN SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;h0;cstab] THEN REAL_ARITH_TAC);;
(*********CARD scs_M <=1**************)
let CARD_SCS_M_6M1=
prove(`CARD (scs_M scs_6M1) <= 1`,
ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M] THEN SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M] THEN ARITH_TAC);;
let SCS_M_6M1=
prove(`(scs_M scs_6M1) ={}`,
ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M] THEN SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M] THEN ARITH_TAC);;
let SCS_M_6T1=
prove(`(scs_M scs_6T1) ={}`,
ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M] THEN SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)/\ ~(&2 * #1.26 < &2)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M;h0] THEN ARITH_TAC);;
let CARD_SCS_M_5I1=
prove(`CARD (scs_M scs_5I1) <= 1`,
ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M] THEN SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M] THEN ARITH_TAC);;
let SCS_M_5I1=
prove(`scs_M scs_5I1 ={}`,
ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M] THEN SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M] THEN ARITH_TAC);;
let SCS_M_5M2=
prove(`scs_M scs_5M2 ={0}`,
ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M] THEN SCS_TAC THEN ASM_SIMP_TAC[h0;cstab;] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT] THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`] THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `]; );;
(*********************)
let SCS_6M1_IMP_SCS_6T1= 
prove_by_refinement(`main_nonlinear_terminal_v11 ==>(!v. v IN MMs_v39 scs_6M1 /\ (!i j. scs_diag 6 i j ==> cstab < dist(v i,v j)) ==> v IN MMs_v39 (scs_6T1))`,
[REWRITE_TAC[IN] THEN REPEAT STRIP_TAC THEN MP_TAC SCS_6M1_IS_SCS THEN STRIP_TAC THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6M1`;`v`] THEN ASSUME_TAC SCS_6M1_BASIC THEN ASSUME_TAC K_SCS_6M1 THEN ASSUME_TAC SCS_6T1_BASIC THEN ASSUME_TAC K_SCS_6T1 THEN ASSUME_TAC SCS_6T1_IS_SCS THEN MP_TAC RRCWNSJ THEN RESA_TAC THEN THAYTHES_TAC 0[`scs_6M1`;`v`][ARITH_RULE`3<6`;h0_LT_B_SCS_6M1;B_LE_CSTAB_6M1] THEN MP_TAC Jcyfmrp.JCYFMRP THEN RESA_TAC THEN THAYTHES_TAC 0[`scs_6M1`;`v`][ARITH_RULE`3<6`;h0_LT_B_SCS_6M1;B_LE_CSTAB_6M1;IN;CARD_SCS_M_6M1] THEN MP_TAC Jlxfdmj.JLXFDMJ THEN RESA_TAC THEN THAYTHES_TAC 0[`scs_6M1`;`v`;`i`][ARITH_RULE`3<6`;h0_LT_B_SCS_6M1;B_LE_CSTAB_6M1;IN;CARD_SCS_M_6M1;SCS_M_6M1;SET_RULE`(~{} a==> B)<=> B`;ARITH_RULE`i+1=SUC i`] THEN MP_TAC Ppbtydq.MXQTIED THEN REWRITE_TAC[IN] THEN STRIP_TAC THEN MATCH_DICH_TAC 0 THEN EXISTS_TAC`scs_6M1` THEN ASM_SIMP_TAC[SCS_M_6M1;SCS_M_6T1] THEN STRIP_TAC; SCS_TAC; STRIP_TAC; DICH_TAC(12-4) THEN ASM_SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;ARITH_RULE`~(6<=3)`] THEN RESA_TAC; REPEAT GEN_TAC THEN THAYTHE_TAC 1[`i'`;`j`] THEN DICH_TAC 0 THEN DICH_TAC 0 THEN SCS_TAC THEN MP_TAC(SET_RULE`i' MOD 6= j MOD 6\/ ~(i' MOD 6= j MOD 6)`) THEN RESA_TAC THEN MP_TAC(SET_RULE`SUC i' MOD 6= j MOD 6\/ ~(SUC i' MOD 6= j MOD 6)`) THEN RESA_TAC; MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6M1`;`v`] THEN MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_6M1`;`j`;`v:num->real^3`;`SUC i':num`] THEN REAL_ARITH_TAC; MP_TAC(SET_RULE`i' MOD 6=SUC j MOD 6\/ ~( i' MOD 6=SUC j MOD 6)`) THEN RESA_TAC; MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6M1`;`v`] THEN MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_6M1`;`i'`;`v:num->real^3`;`SUC j:num`] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC; STRIP_TAC; SCS_TAC; SCS_TAC THEN REWRITE_TAC[h0;scs_diag] THEN REAL_ARITH_TAC]);;
let SCS_6I1_IMP_SCS_6T1=
prove(`main_nonlinear_terminal_v11 ==>(!v. v IN MMs_v39 scs_6I1 /\ (!i j. scs_diag 6 i j ==> cstab < dist(v i,v j)) ==> v IN MMs_v39 (scs_6T1))`,
REPEAT STRIP_TAC THEN MP_TAC SCS_6M1_IMP_SCS_6T1 THEN RESA_TAC THEN MATCH_DICH_TAC 0 THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC PEDSLGV2 THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN THAYTHE_TAC 1[`i`;`j`] THEN DICH_TAC 0 THEN REAL_ARITH_TAC);;
let SCS_6I1_BERAK_BY_CSTAB= 
prove_by_refinement(`main_nonlinear_terminal_v11 ==> scs_arrow_v39 { scs_6I1 } ({ scs_6T1}UNION { scs_stab_diag_v39 scs_6I1 i j| scs_diag 6 i j })`,
[REPEAT GEN_TAC THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION] THEN ABBREV_TAC`k=scs_k_v39 s` THEN REPEAT RESA_TAC; REWRITE_TAC[SCS_6T1_IS_SCS]; MATCH_MP_TAC Yrtafyh.STAB_IS_SCS THEN ASM_SIMP_TAC[SCS_6I1_IS_SCS;K_SCS_6I1;SCS_6I1_BASIC;ARITH_RULE`3<6`] THEN SCS_TAC THEN REWRITE_TAC[h0;cstab] THEN REAL_ARITH_TAC; DISJ_CASES_TAC(SET_RULE`(!s. s = scs_6I1 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_6I1 ==> MMs_v39 s = {}))`); ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN] THEN STRIP_TAC; MP_TAC(SET_RULE`(!i j. scs_diag 6 i j ==> cstab < dist(v i,v j))\/ ~((!i j. scs_diag 6 i j ==> cstab < dist((v:num->real^3) i,v j)))`) THEN RESA_TAC; EXISTS_TAC`scs_6T1` THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`v:num->real^3` THEN MP_TAC SCS_6I1_IMP_SCS_6T1 THEN REWRITE_TAC[IN] THEN RESA_TAC THEN MATCH_DICH_TAC 0 THEN ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`] THEN STRIP_TAC THEN MRESAL_TAC PEDSLGV1[`v`;`i`;`j`][IN] THEN EXISTS_TAC`scs_stab_diag_v39 scs_6I1 i j` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC; MATCH_MP_TAC(SET_RULE`A==> B\/A`) THEN EXISTS_TAC`i:num` THEN EXISTS_TAC`j:num` THEN ASM_REWRITE_TAC[]; EXISTS_TAC`v:num->real^3` THEN ASM_REWRITE_TAC[]]);;
let PSORT_MOD=
prove(`~(k=0)==> psort k (i MOD k,j MOD k)= psort k (i,j)`,
SIMP_TAC[psort;MOD_REFL]);;
(****************************) (****************************) (****************************) (****************************)
let STAB_MOD=
prove(`is_scs_v39 s ==> scs_stab_diag_v39 s (i MOD (scs_k_v39 s)) (j MOD (scs_k_v39 s))=scs_stab_diag_v39 s i j`,
SCS_TAC THEN STRIP_TAC THEN ABBREV_TAC`k=scs_k_v39 s` THEN ASM_SIMP_TAC[PSORT_MOD;ARITH_RULE`3<=k==> ~(k=0)`]);;
let DIAG_MOD=
prove(`~(k=0)==> scs_diag k (i MOD k) (j MOD k)= scs_diag k i j`,
SIMP_TAC[scs_diag;MOD_REFL;Hypermap.lemma_suc_mod]);;
let SET_STAB_6I1=
prove(`{ scs_stab_diag_v39 scs_6I1 i j| scs_diag 6 i j }= { scs_stab_diag_v39 scs_6I1 (i MOD 6) (j MOD 6)| scs_diag 6 (i MOD 6) (j MOD 6) }`,
ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(6=0)`;] THEN MRESAL_TAC STAB_MOD[`scs_6I1`][SCS_6I1_IS_SCS;K_SCS_6I1]);;
let DIAG_EQ_ADD=
prove(`scs_diag 6 (i MOD 6) (j MOD 6)<=> ((i MOD 6= (j MOD 6+ 2) MOD 6)\/ (i MOD 6= (j MOD 6+ 3) MOD 6)\/ (j MOD 6=(i MOD 6+2) MOD 6)\/ (j MOD 6= (i MOD 6+ 3) MOD 6))`,
REWRITE_TAC[scs_diag] THEN MP_TAC(ARITH_RULE`i MOD 6<6==> i MOD 6= 0 \/ i MOD 6= 1 \/i MOD 6= 2 \/ i MOD 6= 3 \/i MOD 6= 4 \/i MOD 6= 5 `) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`j MOD 6<6==> j MOD 6= 0 \/ j MOD 6= 1 \/j MOD 6= 2 \/ j MOD 6= 3 \/j MOD 6= 4 \/j MOD 6= 5 `) THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`] THEN RESA_TAC THEN ARITH_TAC);;
let PSORT_EQ_SYM=
prove(`psort (scs_k_v39 s) (j,i) = psort (scs_k_v39 s) (j',i') <=> psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (j',i')`,
GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]);;
let PSORT_EQ_SYM1=
prove(`psort (scs_k_v39 s) (j,i) = (j',i') <=> psort (scs_k_v39 s) (i,j) = (j',i')`,
GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym] THEN REWRITE_TAC[]);;
let STAB_SYM=
prove(`scs_stab_diag_v39 s i j = scs_stab_diag_v39 s j i`,
SCS_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[PSORT_EQ_SYM] THEN REWRITE_TAC[]);;
let EXPAND_STAB_DIAG=
prove_by_refinement(`{scs_stab_diag_v39 scs_6I1 (i MOD 6) (j MOD 6) | i MOD 6 = (j MOD 6 + 2) MOD 6 \/ i MOD 6 = (j MOD 6 + 3) MOD 6 \/ j MOD 6 = (i MOD 6 + 2) MOD 6 \/ j MOD 6 = (i MOD 6 + 3) MOD 6}= {scs_stab_diag_v39 scs_6I1 (i+2) i| i<6} UNION {scs_stab_diag_v39 scs_6I1 (i+3) i|i<6} `,
[ REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;UNION] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC; MRESAS_TAC STAB_MOD[`scs_6I1`;`j MOD 6 + 2`;`j MOD 6`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`] THEN MATCH_MP_TAC (SET_RULE`A==> A\/B`) THEN EXISTS_TAC`j MOD 6` THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`]; MRESAS_TAC STAB_MOD[`scs_6I1`;`j MOD 6 + 3`;`j MOD 6`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`] THEN MATCH_MP_TAC (SET_RULE`A==> B\/A`) THEN EXISTS_TAC`j MOD 6` THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`]; MRESAS_TAC STAB_MOD[`scs_6I1`;`i MOD 6`;`i MOD 6 + 2`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`] THEN MATCH_MP_TAC (SET_RULE`A==> A\/B`) THEN EXISTS_TAC`i MOD 6` THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`;STAB_SYM]; MRESAS_TAC STAB_MOD[`scs_6I1`;`i MOD 6`;`i MOD 6 + 3`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`] THEN MATCH_MP_TAC (SET_RULE`A==> B\/A`) THEN EXISTS_TAC`i MOD 6` THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`;STAB_SYM]; EXISTS_TAC`i+2` THEN EXISTS_TAC`i:num` THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`;MOD_LT] THEN MRESAS_TAC STAB_MOD[`scs_6I1`;`i MOD 6 + 2`;`i MOD 6`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`;MOD_LT]; EXISTS_TAC`i+3` THEN EXISTS_TAC`i:num` THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`;MOD_LT] THEN MRESAS_TAC STAB_MOD[`scs_6I1`;`i MOD 6 + 3`;`i MOD 6`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`;MOD_LT]]);;
let EQ_DIAG_STAB_6I1_02=
prove(` scs_arrow_v39 {scs_stab_diag_v39 scs_6I1 (i + 2) i } {scs_stab_diag_v39 scs_6I1 0 2}`,
MRESA_TAC STAB_SYM[`scs_6I1`;`2`;`0`] THEN MP_TAC (GEN_ALL Wkeidft.WKEIDFT) THEN REWRITE_TAC[LET_DEF;LET_END_DEF] THEN STRIP_TAC THEN MATCH_DICH_TAC 0 THEN ASM_SIMP_TAC[ARITH_RULE`2 + i = (i + 2) + 0/\ 3<6/\ i+1= SUC i`;K_SCS_6I1;h0_LT_B_SCS_6I1;h0_EQ_B_SCS_6I1;SCS_6I1_IS_SCS;SCS_6I1_BASIC] THEN SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;] THEN EXISTS_TAC`&0` THEN EXISTS_TAC`&2` THEN EXISTS_TAC`&2 *h0` THEN EXISTS_TAC`&2 *h0` THEN EXISTS_TAC`&6` THEN ASM_SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + 2)= i+3/\ SUC i= i+1/\ 2+1=3`;ARITH_RULE`1<6/\ ~(6=0)`;Qknvmlb.SUC_MOD_NOT_EQ;Ocbicby.MOD_EQ_MOD_SHIFT] THEN SCS_TAC THEN MP_TAC(SET_RULE`i= i+0==> i MOD 6= (i+0) MOD 6`) THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`] THEN RESA_TAC THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`1<6/\ ~(6=0)`] THEN SCS_TAC);;
let EQ_DIAG_STAB_6I1_03=
prove(` scs_arrow_v39 {scs_stab_diag_v39 scs_6I1 (i + 3) i } {scs_stab_diag_v39 scs_6I1 0 3}`,
MRESA_TAC STAB_SYM[`scs_6I1`;`3`;`0`] THEN MP_TAC (GEN_ALL Wkeidft.WKEIDFT) THEN REWRITE_TAC[LET_DEF;LET_END_DEF] THEN STRIP_TAC THEN MATCH_DICH_TAC 0 THEN ASM_SIMP_TAC[ARITH_RULE`3 + i = (i + 3) + 0/\ 3<6/\ i+1= SUC i`;K_SCS_6I1;h0_LT_B_SCS_6I1;h0_EQ_B_SCS_6I1;SCS_6I1_IS_SCS;SCS_6I1_BASIC] THEN SCS_TAC THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;] THEN EXISTS_TAC`&0` THEN EXISTS_TAC`&2` THEN EXISTS_TAC`&2 *h0` THEN EXISTS_TAC`&2 *h0` THEN EXISTS_TAC`&6` THEN ASM_SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + 3)= i+4/\ SUC i= i+1/\ 3+1=4`;ARITH_RULE`1<6/\ ~(6=0)`;Qknvmlb.SUC_MOD_NOT_EQ;] THEN SCS_TAC THEN MP_TAC(SET_RULE`i= i+0==> i MOD 6= (i+0) MOD 6`) THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`] THEN RESA_TAC THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`1<6/\ ~(6=0)`] THEN SCS_TAC);;
let SET_EQ_DIAG_STAB_6I1_02=
prove(` scs_arrow_v39 {scs_stab_diag_v39 scs_6I1 (i + 2) i |i<6} {scs_stab_diag_v39 scs_6I1 0 2}`,
REWRITE_TAC[ARITH_RULE`i<6<=> i=0\/i=1\/i=2\/i=3\/i=4\/i=5`;SET_RULE`{scs_stab_diag_v39 scs_6I1 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4\/i=5} = {scs_stab_diag_v39 scs_6I1 (0 + 2) 0} UNION {scs_stab_diag_v39 scs_6I1 (1 + 2) 1} UNION {scs_stab_diag_v39 scs_6I1 (2 + 2) 2} UNION {scs_stab_diag_v39 scs_6I1 (3 + 2) 3} UNION {scs_stab_diag_v39 scs_6I1 (4 + 2) 4} UNION {scs_stab_diag_v39 scs_6I1 (5 + 2) 5} `;] THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02] THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02] THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02] THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02] THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02]);;
let SET_EQ_DIAG_STAB_6I1_03=
prove(` scs_arrow_v39 {scs_stab_diag_v39 scs_6I1 (i + 3) i |i<6} {scs_stab_diag_v39 scs_6I1 0 3}`,
REWRITE_TAC[ARITH_RULE`i<6<=> i=0\/i=1\/i=2\/i=3\/i=4\/i=5`;SET_RULE`{scs_stab_diag_v39 scs_6I1 (i + 3) i |i=0\/i=1\/i=2\/i=3\/i=4\/i=5} = {scs_stab_diag_v39 scs_6I1 (0 + 3) 0} UNION {scs_stab_diag_v39 scs_6I1 (1 + 3) 1} UNION {scs_stab_diag_v39 scs_6I1 (2 + 3) 2} UNION {scs_stab_diag_v39 scs_6I1 (3 + 3) 3} UNION {scs_stab_diag_v39 scs_6I1 (4 + 3) 4} UNION {scs_stab_diag_v39 scs_6I1 (5 + 3) 5} `;] THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03] THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03] THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03] THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03] THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03]);;
let SET_EQ_DIAG_STAB_6I1=
prove( `scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 i j| scs_diag 6 i j } { scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}`,
let OEHDBEN_PRIME=
prove( ` main_nonlinear_terminal_v11 ==> scs_arrow_v39 { scs_6I1 } { scs_6T1, scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}`,
STRIP_TAC THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{ scs_6T1}UNION { scs_stab_diag_v39 scs_6I1 i j| scs_diag 6 i j }` THEN ASM_SIMP_TAC[SCS_6I1_BERAK_BY_CSTAB;SET_RULE`{scs_6T1, scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3} ={scs_6T1}UNION{ scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_6I1;] THEN MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[SCS_6T1_IS_SCS]);;
let OEHDBEN= 
prove(`main_nonlinear_terminal_v11 ==> scs_arrow_v39 { scs_6I1 } { scs_6T1, scs_5M1, scs_4M2, scs_3M1 }`,
STRIP_TAC THEN MATCH_MP_TAC FZIOTEF_TRANS THEN EXISTS_TAC`{ scs_6T1, scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}` THEN ASM_SIMP_TAC[OEHDBEN_PRIME;SET_RULE`{scs_6T1, scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3} = {scs_6T1} UNION {scs_stab_diag_v39 scs_6I1 0 2} UNION{ scs_stab_diag_v39 scs_6I1 0 3}`; SET_RULE`{ scs_6T1, scs_5M1, scs_4M2, scs_3M1 }={scs_6T1} UNION{ scs_3M1,scs_5M1}UNION {scs_4M2}`] THEN MATCH_MP_TAC FZIOTEF_UNION THEN STRIP_TAC THENL[ MATCH_MP_TAC FZIOTEF_REFL THEN REWRITE_TAC[IN_SING] THEN REPEAT RESA_TAC THEN ASM_REWRITE_TAC[SCS_6T1_IS_SCS]; MATCH_MP_TAC FZIOTEF_UNION THEN ASM_REWRITE_TAC[AQICLXA;FZIOTEF]]);;
end;; (* let check_completeness_claimA_concl = Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) *)