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


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


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


let SCSE_TAC= ASM_REWRITE_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;
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 DIAG_5_EQU_PSORT=
prove(`~(i MOD 5 = j MOD 5) /\
          ~(SUC i MOD 5 = j MOD 5) /\
          ~(i MOD 5 = SUC j MOD 5)
<=> psort 5 (i,j) = 0,2\/ psort 5 (i,j) = 0,3\/ psort 5 (i,j) = 1,3
\/ psort 5 (i,j) = 1,4\/ psort 5 (i,j) = 2,4`,

MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
THEN SYM_ASSUM_TAC
THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
THEN SYM_ASSUM_TAC
THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
THEN RESA_TAC
THEN SCS_TAC
THEN REWRITE_TAC[PSORT_5_EXPLICIT;PAIR_EQ]
THEN ARITH_TAC);;


let BB_5I1_IS_BB_5M2=
prove_by_refinement(`BBs_v39 scs_5I1 v/\ (!i j. scs_diag 5 i j ==>   cstab <= dist(v i,v j)) ==> BBs_v39 scs_5M2 v`,

[
REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I1;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`]
THEN REPEAT RESA_TAC
THEN SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC;

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

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

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


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

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

MP_TAC DIAG_5_EQU_PSORT
THEN RESA_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN SCS_TAC;


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

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

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

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

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

MP_TAC DIAG_5_EQU_PSORT
THEN RESA_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN SCS_TAC
THEN THAYTHE_TAC(8-2)[`i`;`j`]]);;

let MM_5I1_IMP_MM_5M2=
prove(`MMs_v39 scs_5I1 v/\ (!i j. scs_diag 5 i j ==>   cstab <= dist(v i,v j)) ==> ~(MMs_v39 scs_5M2 ={})`,

STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_5I1`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I1`;`v`]
THEN ASSUME_TAC SCS_5I1_BASIC
THEN ASSUME_TAC K_SCS_5I1
THEN ASSUME_TAC SCS_5M2_BASIC
THEN ASSUME_TAC K_SCS_5M2
THEN ASSUME_TAC SCS_5M2_IS_SCS
THEN ASM_SIMP_TAC[BB_5I1_IS_BB_5M2;IN;SCS_5I1_IS_SCS]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;

let BB_5I2_IS_BB_5M2=
prove_by_refinement(`BBs_v39 scs_5I2 v/\ (!i j. scs_diag 5 i j ==>   cstab <= dist(v i,v j)) ==> BBs_v39 scs_5M2 v`,

[
REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I2;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`]
THEN REPEAT RESA_TAC
THEN SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC;

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

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

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


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

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

MP_TAC DIAG_5_EQU_PSORT
THEN RESA_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN SCS_TAC;


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

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

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

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

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

MP_TAC DIAG_5_EQU_PSORT
THEN RESA_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN SCS_TAC
THEN THAYTHE_TAC(8-2)[`i`;`j`]]);;

let MM_5I2_IMP_MM_5M2=
prove(`MMs_v39 scs_5I2 v/\ (!i j. scs_diag 5 i j ==>   cstab <= dist(v i,v j)) ==> ~(MMs_v39 scs_5M2 ={})`,

STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_5I2`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I2`;`v`]
THEN ASSUME_TAC SCS_5I2_BASIC
THEN ASSUME_TAC K_SCS_5I2
THEN ASSUME_TAC SCS_5M2_BASIC
THEN ASSUME_TAC K_SCS_5M2
THEN ASSUME_TAC SCS_5M2_IS_SCS
THEN ASM_SIMP_TAC[BB_5I2_IS_BB_5M2;IN;SCS_5I2_IS_SCS]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;


let BB_5I3_IS_BB_5M2=
prove_by_refinement(`BBs_v39 scs_5I3 v/\ (!i j. scs_diag 5 i j ==>   cstab <= dist(v i,v j)) ==> BBs_v39 scs_5M2 v`,

[
REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`]
THEN SCS_TAC
THEN REPEAT RESA_TAC
THEN SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC;

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

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

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

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

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

MP_TAC DIAG_5_EQU_PSORT
THEN RESA_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN SCS_TAC;

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

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

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

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

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

MP_TAC DIAG_5_EQU_PSORT
THEN RESA_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN SCS_TAC
THEN THAYTHE_TAC(8-2)[`i`;`j`]
THEN DICH_TAC 0
THEN REWRITE_TAC[PAIR_EQ]
THEN SCS_TAC]);;

let MM_5I3_IMP_MM_5M2=
prove(`MMs_v39 scs_5I3 v/\ (!i j. scs_diag 5 i j ==>   cstab <= dist(v i,v j)) ==> ~(MMs_v39 scs_5M2 ={})`,

STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_5I3`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I3`;`v`]
THEN ASSUME_TAC SCS_5I3_BASIC
THEN ASSUME_TAC K_SCS_5I3
THEN ASSUME_TAC SCS_5M2_BASIC
THEN ASSUME_TAC K_SCS_5M2
THEN ASSUME_TAC SCS_5M2_IS_SCS
THEN ASM_SIMP_TAC[BB_5I3_IS_BB_5M2;IN;SCS_5I3_IS_SCS]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;

let BB_5M1_IS_BB_5M2=
prove_by_refinement(`BBs_v39 scs_5M1 v/\ (!i j. scs_diag 5 i j ==>   cstab <= dist(v i,v j)) ==> BBs_v39 scs_5M2 v`,

[
REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5M1;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`]
THEN SCS_TAC
THEN REPEAT RESA_TAC
THEN SCS_TAC
THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
THEN RESA_TAC;

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

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

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

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

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

MP_TAC DIAG_5_EQU_PSORT
THEN RESA_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN SCS_TAC]);;


let MM_5M1_IMP_MM_5M2=
prove(`MMs_v39 scs_5M1 v/\ (!i j. scs_diag 5 i j ==>   cstab <= dist(v i,v j)) ==> ~(MMs_v39 scs_5M2 ={})`,

STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`scs_5M1`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M1`;`v`]
THEN ASSUME_TAC SCS_5M1_BASIC
THEN ASSUME_TAC K_SCS_5M1
THEN ASSUME_TAC SCS_5M2_BASIC
THEN ASSUME_TAC K_SCS_5M2
THEN ASSUME_TAC SCS_5M2_IS_SCS
THEN ASM_SIMP_TAC[BB_5M1_IS_BB_5M2;IN;SCS_5M1_IS_SCS]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;
(***********DIST<= cstab*************)


let SCS_5I1_STAB_DIAG= 
prove( 
`!v i j. 
    v IN MMs_v39 scs_5I1 /\
    scs_diag 5 i j /\
    dist(v i,v j) <= cstab ==>
    v IN MMs_v39 (scs_stab_diag_v39 scs_5I1 i j)`,

REWRITE_TAC[IN]
THEN REPEAT STRIP_TAC
THEN MP_TAC SCS_5I1_IS_SCS
THEN STRIP_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I1`;`v`]
THEN MRESA_TAC DIST_LE_IMP_A_LE[`v`;`scs_5I1`;`i`;`j`;`cstab`]
THEN ASSUME_TAC SCS_5I1_BASIC
THEN ASSUME_TAC K_SCS_5I1
THEN MRESAL_TAC Yrtafyh.YRTAFYH[`scs_5I1`;`i`;`j`][ARITH_RULE`3<5`;]
THEN MP_TAC  Ppbtydq.MXQTIED
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MATCH_DICH_TAC 0
THEN EXISTS_TAC`scs_5I1`
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_5I1;scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;CS_ADJ]
THEN SCS_TAC
THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
THEN RESA_TAC
THENL[
MRESAL_TAC DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
THEN DICH_TAC 0
THEN REWRITE_TAC[scs_diag;cstab;h0]
THEN RESA_TAC 
THEN REAL_ARITH_TAC;
REAL_ARITH_TAC]);;
let SCS_5I2_STAB_DIAG= 
prove( `!v i j. 
    v IN MMs_v39 scs_5I2 /\
    scs_diag 5 i j /\
    dist(v i,v j) <= cstab ==>
    v IN MMs_v39 (scs_stab_diag_v39 scs_5I2 i j)`,

REWRITE_TAC[IN]
THEN REPEAT STRIP_TAC
THEN MP_TAC SCS_5I2_IS_SCS
THEN STRIP_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I2`;`v`]
THEN MRESA_TAC DIST_LE_IMP_A_LE[`v`;`scs_5I2`;`i`;`j`;`cstab`]
THEN ASSUME_TAC SCS_5I2_BASIC
THEN ASSUME_TAC K_SCS_5I2
THEN MRESAL_TAC Yrtafyh.YRTAFYH[`scs_5I2`;`i`;`j`][ARITH_RULE`3<5`;]
THEN MP_TAC  Ppbtydq.MXQTIED
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MATCH_DICH_TAC 0
THEN EXISTS_TAC`scs_5I2`
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_5I2;scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;CS_ADJ]
THEN SCS_TAC
THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
THEN RESA_TAC
THENL[
MRESAL_TAC DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
THEN DICH_TAC 0
THEN REWRITE_TAC[scs_diag;cstab;h0]
THEN RESA_TAC 
THEN REAL_ARITH_TAC;
REAL_ARITH_TAC]);;


let SCS_5I3_STAB_DIAG= 
prove( `!v i j. 
    v IN MMs_v39 scs_5I3 /\
    scs_diag 5 i j /\
    dist(v i,v j) <= cstab ==>
    v IN MMs_v39 (scs_stab_diag_v39 scs_5I3 i j)`,

REWRITE_TAC[IN]
THEN REPEAT STRIP_TAC
THEN MP_TAC SCS_5I3_IS_SCS
THEN STRIP_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I3`;`v`]
THEN MRESA_TAC DIST_LE_IMP_A_LE[`v`;`scs_5I3`;`i`;`j`;`cstab`]
THEN ASSUME_TAC SCS_5I3_BASIC
THEN ASSUME_TAC K_SCS_5I3
THEN MRESAL_TAC Yrtafyh.YRTAFYH[`scs_5I3`;`i`;`j`][ARITH_RULE`3<5`;]
THEN MP_TAC  Ppbtydq.MXQTIED
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MATCH_DICH_TAC 0
THEN EXISTS_TAC`scs_5I3`
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_5I3;scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;CS_ADJ]
THEN SCS_TAC
THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
THEN RESA_TAC
THENL[
MRESAL_TAC DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
THEN DICH_TAC 0
THEN REWRITE_TAC[scs_diag;cstab;h0]
THEN RESA_TAC 
THEN MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`]
THEN REWRITE_TAC[PAIR_EQ]
THEN SCS_TAC
THEN REAL_ARITH_TAC;
REAL_ARITH_TAC]);;

let SCS_5M1_STAB_DIAG= 
prove( `!v i j. 
    v IN MMs_v39 scs_5M1 /\
    scs_diag 5 i j /\
    dist(v i,v j) <= cstab ==>
    v IN MMs_v39 (scs_stab_diag_v39 scs_5M1 i j)`,

REWRITE_TAC[IN]
THEN REPEAT STRIP_TAC
THEN MP_TAC SCS_5M1_IS_SCS
THEN STRIP_TAC
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M1`;`v`]
THEN MRESA_TAC DIST_LE_IMP_A_LE[`v`;`scs_5M1`;`i`;`j`;`cstab`]
THEN ASSUME_TAC SCS_5M1_BASIC
THEN ASSUME_TAC K_SCS_5M1
THEN MRESAL_TAC Yrtafyh.YRTAFYH[`scs_5M1`;`i`;`j`][ARITH_RULE`3<5`;]
THEN MP_TAC  Ppbtydq.MXQTIED
THEN REWRITE_TAC[IN]
THEN STRIP_TAC
THEN MATCH_DICH_TAC 0
THEN EXISTS_TAC`scs_5M1`
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_5M1;scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;CS_ADJ]
THEN SCS_TAC
THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
THEN RESA_TAC
THENL[
MRESAL_TAC DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
THEN DICH_TAC 0
THEN REWRITE_TAC[scs_diag;cstab;h0]
THEN RESA_TAC 
THEN MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`]
THEN REWRITE_TAC[PAIR_EQ]
THEN SCS_TAC
THEN REAL_ARITH_TAC;
REAL_ARITH_TAC]);;

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


let SCS_5I1_BERAK_BY_CSTAB= 
prove_by_refinement( `scs_arrow_v39 { scs_5I1 } ({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I1 i j| scs_diag 5 i j })`,

[
REPEAT GEN_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;

REWRITE_TAC[SCS_5M2_IS_SCS];

MATCH_MP_TAC Yrtafyh.STAB_IS_SCS
THEN ASM_SIMP_TAC[SCS_5I1_IS_SCS;K_SCS_5I1;SCS_5I1_BASIC;ARITH_RULE`3<5`]
THEN SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC;

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

ASM_REWRITE_TAC[];

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

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

EXISTS_TAC`scs_5M2`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC MM_5I1_IMP_MM_5M2
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN STRIP_TAC
THEN MATCH_DICH_TAC 0
THEN REPEAT STRIP_TAC
THEN THAYTHE_TAC 1[`i`;`j`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
THEN STRIP_TAC
THEN EXISTS_TAC`scs_stab_diag_v39 scs_5I1 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[];

MRESAL_TAC SCS_5I1_STAB_DIAG[`v`;`i`;`j`][IN]
THEN EXISTS_TAC`v:num->real^3`
THEN ASM_REWRITE_TAC[];]);;

let SCS_5I2_BERAK_BY_CSTAB= 
prove_by_refinement(
`scs_arrow_v39 { scs_5I2 } ({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j })`,

[
REPEAT GEN_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;

REWRITE_TAC[SCS_5M2_IS_SCS];

MATCH_MP_TAC Yrtafyh.STAB_IS_SCS
THEN ASM_SIMP_TAC[SCS_5I2_IS_SCS;K_SCS_5I2;SCS_5I2_BASIC;ARITH_RULE`3<5`]
THEN SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN MP_TAC sqrt8_LE_CSTAB
THEN REAL_ARITH_TAC;

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

ASM_REWRITE_TAC[];

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

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

EXISTS_TAC`scs_5M2`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC MM_5I2_IMP_MM_5M2
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN STRIP_TAC
THEN MATCH_DICH_TAC 0
THEN REPEAT STRIP_TAC
THEN THAYTHE_TAC 1[`i`;`j`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
THEN STRIP_TAC
THEN EXISTS_TAC`scs_stab_diag_v39 scs_5I2 i j`
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC;

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

MRESAL_TAC SCS_5I2_STAB_DIAG[`v`;`i`;`j`][IN]
THEN EXISTS_TAC`v:num->real^3`
THEN ASM_REWRITE_TAC[]]);;


let SCS_5I3_BERAK_BY_CSTAB= 
prove_by_refinement(
`scs_arrow_v39 { scs_5I3 } ({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I3 i j| scs_diag 5 i j })`,

[
REPEAT GEN_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;

REWRITE_TAC[SCS_5M2_IS_SCS];

MATCH_MP_TAC Yrtafyh.STAB_IS_SCS
THEN ASM_SIMP_TAC[SCS_5I3_IS_SCS;K_SCS_5I3;SCS_5I3_BASIC;ARITH_RULE`3<5`]
THEN SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN MP_TAC sqrt8_LE_CSTAB
THEN REAL_ARITH_TAC;

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

ASM_REWRITE_TAC[];

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

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

EXISTS_TAC`scs_5M2`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC MM_5I3_IMP_MM_5M2
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN STRIP_TAC
THEN MATCH_DICH_TAC 0
THEN REPEAT STRIP_TAC
THEN THAYTHE_TAC 1[`i`;`j`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
THEN STRIP_TAC
THEN EXISTS_TAC`scs_stab_diag_v39 scs_5I3 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[];

MRESAL_TAC SCS_5I3_STAB_DIAG[`v`;`i`;`j`][IN]
THEN EXISTS_TAC`v:num->real^3`
THEN ASM_REWRITE_TAC[]]);;

let SCS_5M1_BERAK_BY_CSTAB= 
prove_by_refinement(`scs_arrow_v39 { scs_5M1 } ({ scs_5M2}UNION { scs_stab_diag_v39 scs_5M1 i j| scs_diag 5 i j })`,

[
REPEAT GEN_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;

REWRITE_TAC[SCS_5M2_IS_SCS];

MATCH_MP_TAC Yrtafyh.STAB_IS_SCS
THEN ASM_SIMP_TAC[SCS_5M1_IS_SCS;K_SCS_5M1;SCS_5M1_BASIC;ARITH_RULE`3<5`]
THEN SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN MP_TAC sqrt8_LE_CSTAB
THEN REAL_ARITH_TAC;

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

ASM_REWRITE_TAC[];

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

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

EXISTS_TAC`scs_5M2`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC MM_5M1_IMP_MM_5M2
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN STRIP_TAC
THEN MATCH_DICH_TAC 0
THEN REPEAT STRIP_TAC
THEN THAYTHE_TAC 1[`i`;`j`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
THEN STRIP_TAC
THEN EXISTS_TAC`scs_stab_diag_v39 scs_5M1 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[];

MRESAL_TAC SCS_5M1_STAB_DIAG[`v`;`i`;`j`][IN]
THEN EXISTS_TAC`v:num->real^3`
THEN ASM_REWRITE_TAC[]]);;

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

let DIAG_EQ_ADD5=
prove(`scs_diag 5 (i MOD 5) (j MOD 5)<=> 
((i MOD 5= (j MOD 5+ 2) MOD 5)\/
(j MOD 5=(i MOD 5+2) MOD 5))`,

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

let EXPAND_STAB_DIAG_5=
prove_by_refinement(`is_scs_v39 s /\scs_k_v39 s=5==>
{scs_stab_diag_v39 s (i MOD 5) (j MOD 5) | i MOD 5 =
                                                  (j MOD 5 + 2) MOD 5 \/
                                                  j MOD 5 =
                                                  (i MOD 5 + 2) MOD 5}=
{scs_stab_diag_v39 s (i+2) i| i<5} `,

[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`;`j MOD 5 + 2`;`j MOD 5`][SCS_5I1_IS_SCS;K_SCS_5I1;MOD_REFL;ARITH_RULE`~(5=0)`]
THEN EXISTS_TAC`j MOD 5`
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`];

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

EXISTS_TAC`i+2`
THEN EXISTS_TAC`i:num`
THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`;MOD_LT]
THEN MRESAS_TAC STAB_MOD[`s`;`(i + 2)`;`i`][SCS_5I1_IS_SCS;K_SCS_5I1;MOD_REFL;ARITH_RULE`~(5=0)`;MOD_LT]]);;

let EXPAND_STAB_DIAG_5I1=
prove(`{scs_stab_diag_v39 scs_5I1 (i MOD 5) (j MOD 5) | i MOD 5 =
                                                  (j MOD 5 + 2) MOD 5 \/
                                                  j MOD 5 =
                                                  (i MOD 5 + 2) MOD 5}=
{scs_stab_diag_v39 scs_5I1 (i+2) i| i<5} `,

ASM_SIMP_TAC[EXPAND_STAB_DIAG_5;SCS_5I1_IS_SCS;K_SCS_5I1]);;

let EXPAND_STAB_DIAG_5I2=
prove(`{scs_stab_diag_v39 scs_5I2 (i MOD 5) (j MOD 5) | i MOD 5 =
                                                  (j MOD 5 + 2) MOD 5 \/
                                                  j MOD 5 =
                                                  (i MOD 5 + 2) MOD 5}=
{scs_stab_diag_v39 scs_5I2 (i+2) i| i<5} `,

ASM_SIMP_TAC[EXPAND_STAB_DIAG_5;SCS_5I2_IS_SCS;K_SCS_5I2]);;


let EXPAND_STAB_DIAG_5I3=
prove(`{scs_stab_diag_v39 scs_5I3 (i MOD 5) (j MOD 5) | i MOD 5 =
                                                  (j MOD 5 + 2) MOD 5 \/
                                                  j MOD 5 =
                                                  (i MOD 5 + 2) MOD 5}=
{scs_stab_diag_v39 scs_5I3 (i+2) i| i<5} `,

ASM_SIMP_TAC[EXPAND_STAB_DIAG_5;SCS_5I3_IS_SCS;K_SCS_5I3]);;

let EXPAND_STAB_DIAG_5M1=
prove(`{scs_stab_diag_v39 scs_5M1 (i MOD 5) (j MOD 5) | i MOD 5 =
                                                  (j MOD 5 + 2) MOD 5 \/
                                                  j MOD 5 =
                                                  (i MOD 5 + 2) MOD 5}=
{scs_stab_diag_v39 scs_5M1 (i+2) i| i<5} `,

ASM_SIMP_TAC[EXPAND_STAB_DIAG_5;SCS_5M1_IS_SCS;K_SCS_5M1]);;





let EQ_DIAG_STAB_5I1_02=
prove(`scs_arrow_v39
 {scs_stab_diag_v39 scs_5I1 (i + 2) i } 
 {scs_stab_diag_v39 scs_5I1 0 2}`,

MRESA_TAC STAB_SYM[`scs_5I1`;`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_5I1;h0_LT_B_SCS_5I1;h0_EQ_B_SCS_5I1;SCS_5I1_IS_SCS;SCS_5I1_BASIC]
THEN SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`1<5`;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<5/\ ~(5=0)`;Qknvmlb.SUC_MOD_NOT_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN SCS_TAC
THEN MP_TAC(SET_RULE`i= i+0==> i MOD 5= (i+0) MOD 5`)
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<5/\ ~(5=0)/\ 3<5`]
THEN SCS_TAC);;


let EQ_DIAG_STAB_5I2_02=
prove(`scs_arrow_v39
 {scs_stab_diag_v39 scs_5I2 (i + 2) i } 
 {scs_stab_diag_v39 scs_5I2 0 2}`,

MRESA_TAC STAB_SYM[`scs_5I2`;`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_5I2;h0_LT_B_SCS_5I2;h0_EQ_B_SCS_5I2;SCS_5I2_IS_SCS;SCS_5I2_BASIC]
THEN SCS_TAC
THEN ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;]
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&2`
THEN EXISTS_TAC`&2 *h0`
THEN EXISTS_TAC`sqrt8`
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<5/\ ~(5=0)`;Qknvmlb.SUC_MOD_NOT_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN SCS_TAC
THEN MP_TAC(SET_RULE`i= i+0==> i MOD 5= (i+0) MOD 5`)
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<5/\ ~(5=0)/\ 3<5`]
THEN SCS_TAC);;

let SET_EQ_DIAG_STAB_5I1_02=
prove(`scs_arrow_v39
 {scs_stab_diag_v39 scs_5I1 (i + 2) i |i<5} 
 {scs_stab_diag_v39 scs_5I1 0 2}`,

REWRITE_TAC[ARITH_RULE`i<5<=> i=0\/i=1\/i=2\/i=3\/i=4`;SET_RULE`{scs_stab_diag_v39 scs_5I1 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
= 
{scs_stab_diag_v39 scs_5I1 (0 + 2) 0} UNION
{scs_stab_diag_v39 scs_5I1 (1 + 2) 1} UNION
{scs_stab_diag_v39 scs_5I1 (2 + 2) 2} UNION
{scs_stab_diag_v39 scs_5I1 (3 + 2) 3} UNION
{scs_stab_diag_v39 scs_5I1 (4 + 2) 4} 
`;]
THEN REPEAT(ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_5I1 0 2}={scs_stab_diag_v39 scs_5I1 0 2} UNION {scs_stab_diag_v39 scs_5I1 0 2}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[EQ_DIAG_STAB_5I1_02]));;


let SET_EQ_DIAG_STAB_5I2_02=
prove(`scs_arrow_v39
 {scs_stab_diag_v39 scs_5I2 (i + 2) i |i<5} 
 {scs_stab_diag_v39 scs_5I2 0 2}`,

REWRITE_TAC[ARITH_RULE`i<5<=> i=0\/i=1\/i=2\/i=3\/i=4`;SET_RULE`{scs_stab_diag_v39 scs_5I2 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
= 
{scs_stab_diag_v39 scs_5I2 (0 + 2) 0} UNION
{scs_stab_diag_v39 scs_5I2 (1 + 2) 1} UNION
{scs_stab_diag_v39 scs_5I2 (2 + 2) 2} UNION
{scs_stab_diag_v39 scs_5I2 (3 + 2) 3} UNION
{scs_stab_diag_v39 scs_5I2 (4 + 2) 4} 
`;]
THEN REPEAT(ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_5I2 0 2}={scs_stab_diag_v39 scs_5I2 0 2} UNION {scs_stab_diag_v39 scs_5I2 0 2}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_SIMP_TAC[EQ_DIAG_STAB_5I2_02]));;


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

let SET_STAB_5I1=
prove(`{ scs_stab_diag_v39 scs_5I1 i j| scs_diag 5 i j }= { scs_stab_diag_v39 scs_5I1 (i MOD 5) (j  MOD 5)| scs_diag 5 (i MOD 5) (j  MOD 5) }`,

 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(5=0)`;]
THEN MRESAL_TAC STAB_MOD[`scs_5I1`][SCS_5I1_IS_SCS;K_SCS_5I1]);;

let SET_STAB_5I2=
prove(`{ scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j }= { scs_stab_diag_v39 scs_5I2 (i MOD 5) (j  MOD 5)| scs_diag 5 (i MOD 5) (j  MOD 5) }`,

 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(5=0)`;]
THEN MRESAL_TAC STAB_MOD[`scs_5I2`][SCS_5I2_IS_SCS;K_SCS_5I2]);;

let SET_STAB_5I3=
prove(`{ scs_stab_diag_v39 scs_5I3 i j| scs_diag 5 i j }= { scs_stab_diag_v39 scs_5I3 (i MOD 5) (j  MOD 5)| scs_diag 5 (i MOD 5) (j  MOD 5) }`,

 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(5=0)`;]
THEN MRESAL_TAC STAB_MOD[`scs_5I3`][SCS_5I3_IS_SCS;K_SCS_5I3]);;

let SET_STAB_5M1=
prove(`{ scs_stab_diag_v39 scs_5M1 i j| scs_diag 5 i j }= { scs_stab_diag_v39 scs_5M1 (i MOD 5) (j  MOD 5)| scs_diag 5 (i MOD 5) (j  MOD 5) }`,

 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(5=0)`;]
THEN MRESAL_TAC STAB_MOD[`scs_5M1`][SCS_5M1_IS_SCS;K_SCS_5M1]);;

let SET_EQ_DIAG_STAB_5I1=
prove( `scs_arrow_v39 { scs_stab_diag_v39 scs_5I1 i j| scs_diag 5 i j } 
{ scs_stab_diag_v39 scs_5I1 0 2}`,

ONCE_REWRITE_TAC[SET_STAB_5I1]
THEN REWRITE_TAC[DIAG_EQ_ADD5;EXPAND_STAB_DIAG_5I1]
THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_5I1_02;]);;

let SET_EQ_DIAG_STAB_5I2=
prove( `scs_arrow_v39 { scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j } 
{ scs_stab_diag_v39 scs_5I2 0 2}`,

ONCE_REWRITE_TAC[SET_STAB_5I2]
THEN REWRITE_TAC[DIAG_EQ_ADD5;EXPAND_STAB_DIAG_5I2]
THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_5I2_02;]);;


let OTMTOTJ1= 
prove(`scs_arrow_v39 { scs_5I1 } { scs_stab_diag_v39 scs_5I1 0 2 , scs_5M2 }`,

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I1 i j| scs_diag 5 i j })`
THEN ASM_SIMP_TAC[SCS_5I1_BERAK_BY_CSTAB]
THEN REWRITE_TAC[SET_RULE`{A,B}={B} UNION {A}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_5I1]
THEN MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[SCS_5M2_IS_SCS]);;

let OTMTOTJ2= 
prove(`scs_arrow_v39 { scs_5I2 } { scs_stab_diag_v39 scs_5I2 0 2 , scs_5M2 }`,

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j })`
THEN ASM_SIMP_TAC[SCS_5I2_BERAK_BY_CSTAB]
THEN REWRITE_TAC[SET_RULE`{A,B}={B} UNION {A}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_5I2]
THEN MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[SCS_5M2_IS_SCS]);;
(*************************)


let BB_5I3_IS_BB_5M1=
prove( ` BBs_v39 (scs_stab_diag_v39 scs_5I3 i j) v==> BBs_v39 (scs_stab_diag_v39 scs_5M1 i j) v`,

REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`]
THEN SCS_TAC
THEN REPEAT RESA_TAC
THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
THEN RESA_TAC
THEN THAYTHE_TAC 2[`i'`;`j'`]
THEN DICH_TAC 0
THEN MP_TAC sqrt8_LE_CSTAB
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC);;
(***********SCS_BAISC************)


let STAB_5I3_SCS=
prove(` scs_diag (scs_k_v39 scs_5I3) i j
==> is_scs_v39 (scs_stab_diag_v39 scs_5I3 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5I3 i j)`,

STRIP_TAC
THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5I3_IS_SCS;SCS_5I3_BASIC;K_SCS_5I3;
ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_5I3;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;


let STAB_5I2_SCS=
prove(` scs_diag (scs_k_v39 scs_5I2) i j
==> is_scs_v39 (scs_stab_diag_v39 scs_5I2 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5I2 i j)`,

STRIP_TAC
THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5I2_IS_SCS;SCS_5I2_BASIC;K_SCS_5I2;
ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_5I3;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
THEN SCS_TAC
THEN MP_TAC sqrt8_LE_CSTAB
THEN REAL_ARITH_TAC);;



let STAB_5M1_SCS=
prove(` scs_diag (scs_k_v39 scs_5M1) i j
==> is_scs_v39 (scs_stab_diag_v39 scs_5M1 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5M1 i j)`,

STRIP_TAC
THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5M1_IS_SCS;SCS_5M1_BASIC;K_SCS_5M1;
ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_5I3;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
THEN SCS_TAC
THEN REWRITE_TAC[h0]
THEN REAL_ARITH_TAC);;
let STAB_5M2_SCS=
prove(` scs_diag (scs_k_v39 scs_5M2) i j
==> is_scs_v39 (scs_stab_diag_v39 scs_5M2 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5M2 i j)`,

STRIP_TAC
THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5M2_IS_SCS;SCS_5M2_BASIC;K_SCS_5M2;
ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_5I3;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
THEN SCS_TAC
THEN REWRITE_TAC[h0;cstab]
THEN REAL_ARITH_TAC);;


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


let MM_5I3_IMP_MM_5M1=
prove(`scs_diag 5 i j /\ MMs_v39 (scs_stab_diag_v39 scs_5I3 i j) v ==> ~(MMs_v39 ((scs_stab_diag_v39 scs_5M1 i j)) ={})`,

STRIP_TAC
THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
THEN EXISTS_TAC`v:num->real^3`
THEN EXISTS_TAC`(scs_stab_diag_v39 scs_5I3 i j)`
THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`(scs_stab_diag_v39 scs_5I3 i j)`;`v`]
THEN ASSUME_TAC SCS_5M1_BASIC
THEN ASSUME_TAC K_SCS_5M1
THEN ASM_SIMP_TAC[BB_5I3_IS_BB_5M1;IN;SCS_5M1_IS_SCS;SCS_K_D_A_STAB_EQ;K_SCS_5I3;STAB_5M1_SCS;STAB_5I3_SCS]
THEN SCS_TAC
THEN REAL_ARITH_TAC);;

let STAB_5I3_ARROW_STAB_5M1=
prove_by_refinement(`scs_diag 5 i j
==> scs_arrow_v39 { scs_stab_diag_v39 scs_5I3 i j} { scs_stab_diag_v39 scs_5M1 i j}`,

[
STRIP_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;

ASM_SIMP_TAC[BB_5I3_IS_BB_5M1;IN;SCS_5M1_IS_SCS;SCS_K_D_A_STAB_EQ;K_SCS_5I3;STAB_5M1_SCS;STAB_5I3_SCS;K_SCS_5M1];

DISJ_CASES_TAC(SET_RULE`(!s. s = scs_stab_diag_v39 scs_5I3 i j==> MMs_v39 s = {}) \/ ~((!s. s = scs_stab_diag_v39 scs_5I3 i j ==> 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
THEN EXISTS_TAC`scs_stab_diag_v39 scs_5M1 i j`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC MM_5I3_IMP_MM_5M1
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
THEN STRIP_TAC
THEN MATCH_DICH_TAC 0
THEN REPEAT STRIP_TAC]);;

let h0_EQ_B_SCS_5M2=
prove(`(!i j. scs_diag 5 i j ==> scs_b_v39 scs_5M2 i j= &6)
/\ (!i j. scs_diag 5 i j ==>  scs_a_v39 scs_5M2 i j= cstab)`,

SCS_TAC
THEN REWRITE_TAC[h0;scs_diag;cstab]
THEN REPEAT RESA_TAC
THEN MP_TAC DIAG_5_EQU_PSORT
THEN RESA_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN SCS_TAC);;

let h0_EQ_B_SCS_5M1=
prove(`(!i j. scs_diag 5 i j ==> scs_b_v39 scs_5M1 i j= &6)
/\ (!i j. scs_diag 5 i j ==>  scs_a_v39 scs_5M1 i j= &2 * h0)`,

SCS_TAC
THEN REWRITE_TAC[h0;scs_diag;cstab]
THEN REPEAT RESA_TAC
THEN MP_TAC DIAG_5_EQU_PSORT
THEN RESA_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN SCS_TAC);;


let PROP_OPP_DIAG_5M1_03= 
prove_by_refinement(`scs_stab_diag_v39 scs_5M1 0 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_5M1 1 3)) 3 `,


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

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

STRIP_TAC;

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

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


let PROP_OPP_DIAG_5M1_02= 
prove_by_refinement(`scs_stab_diag_v39 scs_5M1 0 2= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_5M1 1 4)) 3 `,


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

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

STRIP_TAC;

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

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


let STAB_5I3_ARROW_STAB_5M1_DIAG=
prove( `scs_arrow_v39 {scs_stab_diag_v39 scs_5I3 i j | scs_diag 5 i j}
 {scs_stab_diag_v39 scs_5M1 i j | scs_diag 5 i j}`,

ONCE_REWRITE_TAC[SET_STAB_5I3]
THEN ONCE_REWRITE_TAC[SET_STAB_5M1]
THEN REWRITE_TAC[DIAG_EQ_ADD5;EXPAND_STAB_DIAG_5I3;EXPAND_STAB_DIAG_5M1]
THEN REWRITE_TAC[ARITH_RULE`i<5<=> i=0\/i=1\/i=2\/i=3\/i=4`;SET_RULE`{scs_stab_diag_v39 scs_5I3 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
= 
{scs_stab_diag_v39 scs_5I3 (0 + 2) 0} UNION
{scs_stab_diag_v39 scs_5I3 (1 + 2) 1} UNION
{scs_stab_diag_v39 scs_5I3 (2 + 2) 2} UNION
{scs_stab_diag_v39 scs_5I3 (3 + 2) 3} UNION
{scs_stab_diag_v39 scs_5I3 (4 + 2) 4} 
`;SET_RULE`{scs_stab_diag_v39 scs_5M1 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
= 
{scs_stab_diag_v39 scs_5M1 (0 + 2) 0} UNION
{scs_stab_diag_v39 scs_5M1 (1 + 2) 1} UNION
{scs_stab_diag_v39 scs_5M1 (2 + 2) 2} UNION
{scs_stab_diag_v39 scs_5M1 (3 + 2) 3} UNION
{scs_stab_diag_v39 scs_5M1 (4 + 2) 4} 
`;]
THEN REPEAT(MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC
THENL[MATCH_MP_TAC STAB_5I3_ARROW_STAB_5M1
THEN REWRITE_TAC[scs_diag;ARITH_RULE`3+2=5/\ 2+2=4`]
THEN SCS_TAC;
ALL_TAC])
THEN MATCH_MP_TAC STAB_5I3_ARROW_STAB_5M1
THEN REWRITE_TAC[scs_diag;ARITH_RULE`4+2=6/\ 7 MOD 5=2`]
THEN SCS_TAC
THEN REWRITE_TAC[scs_diag;ARITH_RULE`4+2=6/\ 7 MOD 5=2/\ ~(2=4)`]);;



let SET_EQ_DIAG_STAB_5M1= 
prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M1 i j | scs_diag 5 i j}
 {scs_stab_diag_v39 scs_5M1 0 2, scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39
                                                                scs_5M1
                                                                2
                                                                4}`,

[
ONCE_REWRITE_TAC[SET_STAB_5M1]
THEN REWRITE_TAC[DIAG_EQ_ADD5;EXPAND_STAB_DIAG_5I3;EXPAND_STAB_DIAG_5M1]
THEN REWRITE_TAC[ARITH_RULE`i<5<=> i=0\/i=1\/i=2\/i=3\/i=4`;
SET_RULE`{A,B,C}
= 
{A}UNION
{B}UNION
{C}UNION
{B}UNION
{A}
`;SET_RULE`{scs_stab_diag_v39 scs_5M1 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
= 
{scs_stab_diag_v39 scs_5M1 (0 + 2) 0} UNION
{scs_stab_diag_v39 scs_5M1 (1 + 2) 1} UNION
{scs_stab_diag_v39 scs_5M1 (2 + 2) 2} UNION
{scs_stab_diag_v39 scs_5M1 (3 + 2) 3} UNION
{scs_stab_diag_v39 scs_5M1 (4 + 2) 4} 
`;]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC;

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

MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC;

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

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

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

MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC;

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

MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC;

REWRITE_TAC[ARITH_RULE`3+2=5`;STAB_SYM]
THEN MRESAL_TAC STAB_MOD[`scs_5M1`;`5`;`3`][SCS_5M1_IS_SCS;K_SCS_5M1;ARITH_RULE`5 MOD 5=0/\ 3 MOD 5=3`]
THEN SYM_ASSUM_TAC
THEN REWRITE_TAC[ARITH_RULE`3+2=5`;STAB_SYM]
THEN MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC  STAB_5M1_SCS[`3`;`0`][scs_diag;K_SCS_5M1;ARITH_RULE`~(3 MOD 5 = 0 MOD 5) /\
      ~(SUC 3 MOD 5 = 0 MOD 5) /\
      ~(3 MOD 5 = SUC 0 MOD 5)`];

REWRITE_TAC[ARITH_RULE`4+2=6`;]
THEN MRESAL_TAC STAB_MOD[`scs_5M1`;`6`;`4`][SCS_5M1_IS_SCS;K_SCS_5M1;ARITH_RULE`6 MOD 5=1/\ 4 MOD 5=4`]
THEN SYM_ASSUM_TAC
THEN REWRITE_TAC[PROP_OPP_DIAG_5M1_02];

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

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

MATCH_MP_TAC(GEN_ALL YXIONXL3)
THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_5M1 1 4)`
THEN MRESAL_TAC  STAB_5M1_SCS[`1`;`4`][scs_diag;K_SCS_5M1;ARITH_RULE`~(1 MOD 5 = 4 MOD 5) /\
      ~(SUC 1 MOD 5 = 4 MOD 5) /\
      ~(1 MOD 5 = SUC 4 MOD 5)`]]);;
let OTMTOTJ3= 
prove_by_refinement(`scs_arrow_v39 { scs_5I3 } { scs_stab_diag_v39 scs_5M1 0 2 ,     scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4, scs_5M2 }`,


[MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I3 i j| scs_diag 5 i j })`
THEN ASM_SIMP_TAC[SCS_5I3_BERAK_BY_CSTAB;SET_RULE`{A,B,C,D}={D} UNION {A,B,C}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN STRIP_TAC;

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

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`{scs_stab_diag_v39 scs_5M1 i j | scs_diag 5 i j}`
THEN ASM_REWRITE_TAC[STAB_5I3_ARROW_STAB_5M1_DIAG];

ASM_SIMP_TAC[SET_EQ_DIAG_STAB_5M1]]);;

let OTMTOTJ4= 
prove(`scs_arrow_v39 { scs_5M1 } { scs_stab_diag_v39 scs_5M1 0 2 ,     scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4, scs_5M2 }`,

MATCH_MP_TAC FZIOTEF_TRANS
THEN EXISTS_TAC`({ scs_5M2}UNION { scs_stab_diag_v39 scs_5M1 i j| scs_diag 5 i j })`
THEN ASM_SIMP_TAC[SCS_5M1_BERAK_BY_CSTAB;SET_RULE`{A,B,C,D}={D} UNION {A,B,C}`]
THEN MATCH_MP_TAC FZIOTEF_UNION
THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_5M1]
THEN MATCH_MP_TAC FZIOTEF_REFL
THEN REWRITE_TAC[IN_SING]
THEN REPEAT RESA_TAC
THEN ASM_REWRITE_TAC[SCS_5M2_IS_SCS]);;

 end;;


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