text_formalization/local/AUEAHEH.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Local Fan                                              *)
   5 (* Author: Hoang Le Truong                                        *)
   6 (* Date: 2012-04-01                                                           *)
   7 (* ========================================================================= *)
   8
   9
  10 (*
  11 remaining conclusions from appendix to Local Fan chapter
  12 *)
  13
  14
  15 module Aueaheh = struct
  16
  17
  18
  19 open Polyhedron;;
  20 open Sphere;;
  21 open Topology;;
  22 open Fan_misc;;
  23 open Planarity;;
  24 open Conforming;;
  25 open Hypermap;;
  26 open Fan;;
  27 open Topology;;
  28 open Wrgcvdr_cizmrrh;;
  29 open Local_lemmas;;
  30 open Collect_geom;;
  31 open Dih2k_hypermap;;
  32 open Wjscpro;;
  33 open Tecoxbm;;
  34 open Hdplygy;;
  35 open Nkezbfc_local;;
  36 open Flyspeck_constants;;
  37 open Gbycpxs;;
  38 open Pcrttid;;
  39 open Local_lemmas1;;
  40 open Pack_defs;;
  41
  42 open Hales_tactic;;
  43
  44 open Appendix;;
  45
  46
  47
  48
  49
  50 open Hypermap;;
  51 open Fan;;
  52 open Wrgcvdr_cizmrrh;;
  53 open Local_lemmas;;
  54 open Flyspeck_constants;;
  55 open Pack_defs;;
  56
  57 open Hales_tactic;;
  58
  59 open Appendix;;
  60
  61
  62 open Zithlqn;;
  63
  64
  65 open Xwitccn;;
  66
  67 open Ayqjtmd;;
  68
  69 open Jkqewgv;;
  70
  71
  72 open Mtuwlun;;
  73
  74
  75 open Uxckfpe;;
  76 open Sgtrnaf;;
  77
  78 open Yxionxl;;
  79
  80 open Qknvmlb;;
  81 open Odxlstcv2;;
  82
  83 open Yxionxl2;;
  84 open Eyypqdw;;
  85 open Ocbicby;;
  86 open Imjxphr;;
  87 open Nuxcoea;;
  88 open Aursipd;;
  89 open Cuxvzoz;;
  90 open Rrcwnsj;;
  91 open Tfitskc;;
  92 open Hexagons;;
  93 open Otmtotj;;
  94 open Hijqaha;;
  95 open Cnicgsf;;
  96 open Ardbzye;;
  97
  98
  99
 100 let SCS_DIAG_SCS_4I1_02=prove(`scs_diag (scs_k_v39 scs_4I1) 0 2`,
 101 REWRITE_TAC[K_SCS_4I1;scs_diag]
 102 THEN ARITH_TAC);;
 103
 104
 105
 106 let SCS_4I1_SLICE_02=prove_by_refinement(
 107 `scs_arrow_v39 {scs_stab_diag_v39 scs_4I1 0 2 } { scs_prop_equ_v39 scs_3M1 1}`,
 108 [ONCE_REWRITE_TAC[SET_RULE`{ scs_prop_equ_v39 scs_3M1 1}={ scs_prop_equ_v39 scs_3M1 1, scs_prop_equ_v39 scs_3M1 1}`]
 109 THEN
 110 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
 111 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4I1_02;STAB_4I1_SCS;SCS_K_D_A_STAB_EQ;]
 112 THEN EXISTS_TAC`0`
 113 THEN EXISTS_TAC`2`
 114 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4I1_02]
 115 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
 116 THEN REPEAT RESA_TAC;
 117
 118
 119 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
 120 THEN STRIP_TAC
 121 THEN MATCH_MP_TAC scs_inj
 122 THEN ASM_SIMP_TAC[SCS_3M1_BASIC;SCS_4I1_BASIC;J_SCS_4I1;BASIC_HALF_SLICE_STAB;J_SCS_3M1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4I1_BASIC]
 123 THEN STRIP_TAC;
 124
 125 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4I1]
 126 THEN ARITH_TAC;
 127
 128
 129
 130 STRIP_TAC
 131 THEN
 132 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4I1;scs_3T4_prime;scs_5M3;
 133 ARITH_RULE`(2 + 1 + 4 - 0) MOD 4= 3/\ 0 MOD 4=0/\ a+0=a`;scs_prop_equ_v39]
 134 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 135 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 136 THEN SCS_TAC
 137 THEN REPEAT GEN_TAC
 138 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
 139 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
 140 THEN RESA_TAC
 141 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
 142 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
 143 THEN RESA_TAC
 144 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 145 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
 146 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
 147 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
 148 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
 149 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
 150 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
 151 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
 152 THEN ASM_TAC
 153 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/\
 154 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
 155 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 156 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
 157 THEN REPEAT RESA_TAC
 158 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)
 159 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
 160 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
 161 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
 162 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
 163 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
 164 THEN SYM_ASSUM_TAC
 165 THEN SCS_TAC;
 166
 167
 168 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4I1]
 169 THEN ARITH_TAC;
 170
 171
 172 STRIP_TAC
 173 THEN
 174 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4I1;scs_3T4_prime;scs_5M3;
 175 ARITH_RULE`(0 + 1 + 4 - 2) MOD 4= 3/\ 2 MOD 4=2/\ a+0=a`;scs_prop_equ_v39]
 176 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 177 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 178 THEN SCS_TAC
 179 THEN REPEAT GEN_TAC
 180 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
 181 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
 182 THEN RESA_TAC
 183 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
 184 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
 185 THEN RESA_TAC
 186 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 187 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
 188 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
 189 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
 190 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
 191 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
 192 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
 193 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
 194 THEN ASM_TAC
 195 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/\
 196 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
 197 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 198 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
 199 THEN REPEAT RESA_TAC
 200 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)
 201 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
 202 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
 203 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
 204 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
 205 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
 206 THEN SYM_ASSUM_TAC
 207 THEN SCS_TAC;
 208
 209
 210
 211 SCS_TAC
 212 THEN REAL_ARITH_TAC;
 213
 214
 215
 216 SCS_TAC
 217 THEN REAL_ARITH_TAC;
 218
 219
 220
 221 SCS_TAC
 222 THEN REAL_ARITH_TAC;
 223
 224
 225 SCS_TAC
 226 THEN REWRITE_TAC[cstab]
 227 THEN REAL_ARITH_TAC;
 228
 229
 230
 231 SCS_TAC
 232 THEN REWRITE_TAC[cstab]
 233 THEN REAL_ARITH_TAC;
 234
 235
 236
 237 POP_ASSUM MP_TAC
 238 THEN REWRITE_TAC[J_SCS_3M1];
 239
 240 ]);;
 241
 242
 243
 244 let AUEAHEH=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4I1 0 2 } {scs_3M1}`,
 245 MATCH_MP_TAC FZIOTEF_TRANS
 246 THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_3M1 1}`
 247 THEN ASM_REWRITE_TAC[SCS_4I1_SLICE_02]
 248 THEN MRESAS_TAC PRO_EQU_ID1[`scs_3M1`;`1`;`3`][SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`(3 - 1 MOD 3)=2`]
 249 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1 1`;`2`][PROP_EQU_IS_SCS;SCS_3M1_IS_SCS]
 250 THEN DICH_TAC 0
 251 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
 252 THEN REWRITE_TAC[]);;
 253
 254
 255 (*************************)
 256
 257 let BB_4I3_IMP_4T4=prove(`!v.
 258     BBs_v39 (scs_stab_diag_v39 scs_4I3 1 3) v
 259      ==>
 260     BBs_v39 (scs_4T4) v`,
 261 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4I3;scs_4T4;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;]
 262 THEN REPEAT RESA_TAC
 263 THEN THAYTHE_TAC 1[`i`;`j`]
 264 THEN DICH_TAC 0
 265 THEN MP_TAC(SET_RULE`psort 4 (i,j) = 1,3\/ ~(psort 4 (i,j) = 1,3)`)
 266 THEN RESA_TAC
 267 THEN MRESAL_TAC Uaghhbm.CASE_PSORT[`i`;`3`;`j`;`1`;`4`][PSORT_5_EXPLICIT;Uxckfpe.ARITH_4_TAC;PAIR_EQ;cstab]
 268 THEN DICH_TAC 0
 269 THEN SCS_TAC
 270 THEN RESA_TAC
 271 THEN SCS_TAC);;
 272
 273 let STAB_4I3_SCS=prove(` scs_diag (scs_k_v39 scs_4I3) i j
 274 ==> is_scs_v39 (scs_stab_diag_v39 scs_4I3 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4I3 i j)`,
 275 STRIP_TAC
 276 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
 277 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4I3_IS_SCS;SCS_4I3_BASIC;K_SCS_4I3;
 278 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
 279 THEN SCS_TAC
 280 THEN REWRITE_TAC[h0;cstab]
 281 THEN MP_TAC sqrt8_LE_CSTAB
 282 THEN REAL_ARITH_TAC);;
 283
 284 let STAB_4M2_SCS=prove(` scs_diag (scs_k_v39 scs_4M2) i j
 285 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M2 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M2 i j)`,
 286 STRIP_TAC
 287 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
 288 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M2_IS_SCS;SCS_4M2_BASIC;K_SCS_4M2;
 289 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
 290 THEN SCS_TAC
 291 THEN REWRITE_TAC[h0;cstab]
 292 THEN MP_TAC sqrt8_LE_CSTAB
 293 THEN REAL_ARITH_TAC);;
 294
 295
 296 let STAB_4M3_SCS=prove(` scs_diag (scs_k_v39 scs_4M3') i j
 297 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M3' i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M3' i j)`,
 298 STRIP_TAC
 299 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
 300 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M3_IS_SCS;SCS_4M3_BASIC;K_SCS_4M3;
 301 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
 302 THEN SCS_TAC
 303 THEN REWRITE_TAC[h0;cstab]
 304 THEN MP_TAC sqrt8_LE_CSTAB
 305 THEN MP_TAC LE_sqrt8_2h0
 306 THEN REAL_ARITH_TAC);;
 307
 308 let STAB_4M4_SCS=prove(` scs_diag (scs_k_v39 scs_4M4') i j
 309 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M4' i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M4' i j)`,
 310 STRIP_TAC
 311 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
 312 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M4_IS_SCS;SCS_4M4_BASIC;K_SCS_4M4;
 313 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
 314 THEN SCS_TAC
 315 THEN REWRITE_TAC[h0;cstab]
 316 THEN MP_TAC sqrt8_LE_CSTAB
 317 THEN MP_TAC LE_sqrt8_2h0
 318 THEN REAL_ARITH_TAC);;
 319
 320
 321
 322 let STAB_4M5_SCS=prove(` scs_diag (scs_k_v39 scs_4M5') i j
 323 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M5' i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M5' i j)`,
 324 STRIP_TAC
 325 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
 326 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M5_IS_SCS;SCS_4M5_BASIC;K_SCS_4M5;
 327 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
 328 THEN SCS_TAC
 329 THEN REWRITE_TAC[h0;cstab]
 330 THEN MP_TAC sqrt8_LE_CSTAB
 331 THEN MP_TAC LE_sqrt8_2h0
 332 THEN REAL_ARITH_TAC);;
 333
 334
 335
 336 let STAB_4M6_SCS=prove(` scs_diag (scs_k_v39 scs_4M6') i j
 337 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M6' i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M6' i j)`,
 338 STRIP_TAC
 339 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
 340 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;
 341 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
 342 THEN SCS_TAC
 343 THEN REWRITE_TAC[h0;cstab]
 344 THEN MP_TAC sqrt8_LE_CSTAB
 345 THEN MP_TAC LE_sqrt8_2h0
 346 THEN REAL_ARITH_TAC);;
 347
 348
 349 let STAB_4M7_SCS=prove(` scs_diag (scs_k_v39 scs_4M7) i j
 350 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M7 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M7 i j)`,
 351 STRIP_TAC
 352 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
 353 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M7_IS_SCS;SCS_4M7_BASIC;K_SCS_4M7;
 354 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
 355 THEN SCS_TAC
 356 THEN REWRITE_TAC[h0;cstab]
 357 THEN MP_TAC sqrt8_LE_CSTAB
 358 THEN MP_TAC LE_sqrt8_2h0
 359 THEN REAL_ARITH_TAC);;
 360
 361
 362 let STAB_4M8_SCS=prove(` scs_diag (scs_k_v39 scs_4M8) i j
 363 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M8 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M8 i j)`,
 364 STRIP_TAC
 365 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
 366 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M8_IS_SCS;SCS_4M8_BASIC;K_SCS_4M8;
 367 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
 368 THEN SCS_TAC
 369 THEN REWRITE_TAC[h0;cstab]
 370 THEN MP_TAC sqrt8_LE_CSTAB
 371 THEN MP_TAC LE_sqrt8_2h0
 372 THEN REAL_ARITH_TAC);;
 373
 374 let SCS_DIAG_SCS_4I3_02=prove(`scs_diag (scs_k_v39 scs_4I3) 0 2`,
 375 REWRITE_TAC[K_SCS_4I3;scs_diag]
 376 THEN ARITH_TAC);;
 377
 378 let SCS_DIAG_SCS_4I3_13=prove(`scs_diag (scs_k_v39 scs_4I3) 1 3`,
 379 REWRITE_TAC[K_SCS_4I3;scs_diag]
 380 THEN ARITH_TAC);;
 381
 382
 383 let SCS_DIAG_SCS_4M2_02=prove(`scs_diag (scs_k_v39 scs_4M2) 0 2`,
 384 REWRITE_TAC[K_SCS_4M2;scs_diag]
 385 THEN ARITH_TAC);;
 386
 387 let SCS_DIAG_SCS_4M2_13=prove(`scs_diag (scs_k_v39 scs_4M2) 1 3`,
 388 REWRITE_TAC[K_SCS_4M2;scs_diag]
 389 THEN ARITH_TAC);;
 390
 391
 392 let SCS_DIAG_SCS_4M3_02=prove(`scs_diag (scs_k_v39 scs_4M3') 0 2`,
 393 REWRITE_TAC[K_SCS_4M3;scs_diag]
 394 THEN ARITH_TAC);;
 395
 396 let SCS_DIAG_SCS_4M3_13=prove(`scs_diag (scs_k_v39 scs_4M3') 1 3`,
 397 REWRITE_TAC[K_SCS_4M3;scs_diag]
 398 THEN ARITH_TAC);;
 399
 400 let SCS_DIAG_SCS_4M4_02=prove(`scs_diag (scs_k_v39 scs_4M4') 0 2`,
 401 REWRITE_TAC[K_SCS_4M4;scs_diag]
 402 THEN ARITH_TAC);;
 403
 404 let SCS_DIAG_SCS_4M4_13=prove(`scs_diag (scs_k_v39 scs_4M4') 1 3`,
 405 REWRITE_TAC[K_SCS_4M4;scs_diag]
 406 THEN ARITH_TAC);;
 407
 408 let SCS_DIAG_SCS_4M5_02=prove(`scs_diag (scs_k_v39 scs_4M5') 0 2`,
 409 REWRITE_TAC[K_SCS_4M5;scs_diag]
 410 THEN ARITH_TAC);;
 411
 412 let SCS_DIAG_SCS_4M5_13=prove(`scs_diag (scs_k_v39 scs_4M5') 1 3`,
 413 REWRITE_TAC[K_SCS_4M5;scs_diag]
 414 THEN ARITH_TAC);;
 415
 416 let SCS_DIAG_SCS_4M6_02=prove(`scs_diag (scs_k_v39 scs_4M6') 0 2`,
 417 REWRITE_TAC[K_SCS_4M6;scs_diag]
 418 THEN ARITH_TAC);;
 419
 420 let SCS_DIAG_SCS_4M6_13=prove(`scs_diag (scs_k_v39 scs_4M6') 1 3`,
 421 REWRITE_TAC[K_SCS_4M6;scs_diag]
 422 THEN ARITH_TAC);;
 423
 424
 425 let SCS_DIAG_SCS_4M7_02=prove(`scs_diag (scs_k_v39 scs_4M7) 0 2`,
 426 REWRITE_TAC[K_SCS_4M7;scs_diag]
 427 THEN ARITH_TAC);;
 428
 429 let SCS_DIAG_SCS_4M7_13=prove(`scs_diag (scs_k_v39 scs_4M7) 1 3`,
 430 REWRITE_TAC[K_SCS_4M7;scs_diag]
 431 THEN ARITH_TAC);;
 432
 433 let SCS_DIAG_SCS_4M8_02=prove(`scs_diag (scs_k_v39 scs_4M8) 0 2`,
 434 REWRITE_TAC[K_SCS_4M8;scs_diag]
 435 THEN ARITH_TAC);;
 436
 437 let SCS_DIAG_SCS_4M8_13=prove(`scs_diag (scs_k_v39 scs_4M8) 1 3`,
 438 REWRITE_TAC[K_SCS_4M8;scs_diag]
 439 THEN ARITH_TAC);;
 440
 441
 442 let MM_4I3_IMP_4T4=prove(`MMs_v39 (scs_stab_diag_v39 scs_4I3 1 3) v
 443      ==>
 444     ~(MMs_v39 (scs_4T4) ={})`,
 445 STRIP_TAC
 446 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
 447 THEN EXISTS_TAC`v:num->real^3`
 448 THEN EXISTS_TAC`(scs_stab_diag_v39 scs_4I3 1 3)`
 449 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`(scs_stab_diag_v39 scs_4I3 1 3)`;`v`]
 450 THEN ASSUME_TAC SCS_4T4_BASIC
 451 THEN ASSUME_TAC K_SCS_4T4
 452 THEN ASM_SIMP_TAC[SCS_4T4_IS_SCS;STAB_4I3_SCS;K_SCS_4I3;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4I3_13;BB_4I3_IMP_4T4]
 453 THEN SCS_TAC
 454 THEN REAL_ARITH_TAC);;
 455
 456
 457
 458
 459   let SCS_4I3_ARROW_4T4 =prove_by_refinement(`scs_arrow_v39 { scs_stab_diag_v39 scs_4I3 1 3 } { scs_4T4 }`,
 460 [
 461 REPEAT GEN_TAC
 462 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
 463 THEN ABBREV_TAC`k=scs_k_v39 s`
 464 THEN REPEAT RESA_TAC;
 465
 466 ASM_SIMP_TAC[SCS_4T4_IS_SCS];
 467
 468 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_stab_diag_v39 scs_4I3 1 3 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_stab_diag_v39 scs_4I3 1 3 ==> MMs_v39 s = {}))`);
 469
 470 ASM_REWRITE_TAC[];
 471
 472 ASM_REWRITE_TAC[]
 473 THEN POP_ASSUM MP_TAC
 474 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
 475 THEN REPEAT STRIP_TAC
 476 THEN POP_ASSUM MP_TAC
 477 THEN RESA_TAC
 478 THEN EXISTS_TAC`scs_4T4`
 479 THEN ASM_REWRITE_TAC[]
 480 THEN MATCH_MP_TAC (GEN_ALL MM_4I3_IMP_4T4)
 481 THEN POP_ASSUM MP_TAC
 482 THEN SET_TAC[]]);;
 483
 484
 485
 486 let PROP_OPP_DIAG_4I3_13= prove_by_refinement(`scs_stab_diag_v39 scs_4I3 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4I3 0 2)) 2 `,
 487 [REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;SCS_K_D_A_STAB_EQ;scs_opp_v39]
 488 THEN MATCH_MP_TAC scs_inj
 489 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4I3_BASIC;STAB_4I3_SCS;SCS_DIAG_SCS_4I3_13;scs_basic;unadorned_v39;peropp;peropp2]
 490 THEN SCS_TAC
 491 THEN STRIP_TAC;
 492
 493 SET_TAC[];
 494
 495
 496 STRIP_TAC
 497 THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;]
 498 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
 499 THEN REPEAT GEN_TAC
 500 THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
 501 THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
 502 THEN SYM_ASSUM_TAC
 503 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
 504 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
 505 THEN SYM_ASSUM_TAC
 506 THEN SYM_ASSUM_TAC
 507 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`)
 508 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
 509 THEN RESA_TAC
 510 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`)
 511 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 512 THEN RESA_TAC
 513 THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_4_TAC;PSORT_5_EXPLICIT;ARITH_RULE`4-1=3/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6
 514 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;
 515
 516
 517
 518
 519
 520 let STAB_4I3_02_ARROW_4I3_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4I3 0 2}{scs_stab_diag_v39 scs_4I3 1 3}`,
 521 ASM_SIMP_TAC[PROP_OPP_DIAG_4I3_13]
 522 THEN MATCH_MP_TAC FZIOTEF_TRANS
 523 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4I3 0 2)}`
 524 THEN STRIP_TAC
 525 THENL[
 526 MATCH_MP_TAC (GEN_ALL YXIONXL2)
 527 THEN EXISTS_TAC`4`
 528 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4I3;STAB_4I3_SCS;SCS_DIAG_SCS_4I3_02]
 529 ;
 530
 531 MATCH_MP_TAC(GEN_ALL YXIONXL3)
 532 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
 533 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4I3 0 2)`
 534 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4I3;STAB_4I3_SCS;SCS_DIAG_SCS_4I3_02]]);;
 535
 536
 537
 538 let ZNLLLDL=prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_4I3 0 2 } { scs_4T4 }`,
 539 MATCH_MP_TAC FZIOTEF_TRANS
 540 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4I3 1 3}`
 541 THEN ASM_SIMP_TAC[STAB_4I3_02_ARROW_4I3_13;SCS_4I3_ARROW_4T4]);;
 542
 543
 544 (******************)
 545
 546 let h0_LT_B_SCS_4I3=prove(`
 547 (!i j. scs_diag 4 i j ==> &4 * h0 < scs_b_v39 scs_4I3 i j)
 548 /\ (!i j. scs_diag 4 i j ==> scs_a_v39 scs_4I3 i j <= cstab)`,
 549 SCS_TAC
 550 THEN REWRITE_TAC[h0;SCS_DIAG_4_CASES;cstab]
 551 THEN REPEAT RESA_TAC
 552 THEN ASSUME_TAC(ARITH_RULE`~(4=0)`)
 553 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
 554 THEN SYM_ASSUM_TAC
 555 THEN SCS_TAC
 556 THEN MP_TAC sqrt8_LE_CSTAB
 557 THEN REAL_ARITH_TAC);;
 558
 559
 560 let B_LE_CSTAB_SCS_4I3=prove(
 561 ` (!i.  scs_b_v39 scs_4I3 i (SUC i) <= cstab)`,
 562 SCS_TAC
 563 THEN REWRITE_TAC[h0;scs_diag;cstab]
 564 THEN REPEAT RESA_TAC
 565 THEN ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;]
 566 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
 567 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`SUC i`]
 568 THEN SYM_ASSUM_TAC
 569 THEN REWRITE_TAC[ADD1]
 570 THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`]
 571 THEN SYM_ASSUM_TAC
 572 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
 573 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
 574 THEN RESA_TAC
 575 THEN SCS_TAC
 576 THEN MP_TAC sqrt8_LE_CSTAB
 577 THEN REAL_ARITH_TAC);;
 578
 579
 580
 581 let BB_4I3_IMP_BB_4M6= prove
 582 (`
 583     BBs_v39 scs_4I3 v /\
 584     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) ==>
 585     BBs_v39 (scs_4M6') v`,
 586 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4I3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
 587 THEN REPEAT RESA_TAC
 588 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
 589 THEN SCS_TAC
 590 THEN THAYTHE_TAC 1[`i`;`j`]
 591 THEN DICH_TAC 0
 592 THEN THAYTHE_TAC 2[`i`;`j`]
 593 THEN DICH_TAC 0
 594 THEN DICH_TAC 0
 595 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
 596 THEN SYM_ASSUM_TAC
 597 THEN REWRITE_TAC[ADD1]
 598 THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`]
 599 THEN SYM_ASSUM_TAC
 600 THEN MRESA_TAC MOD_ADD_MOD[`j`;`1`;`4`]
 601 THEN SYM_ASSUM_TAC
 602 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
 603 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
 604 THEN RESA_TAC
 605 THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
 606 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
 607 THEN RESA_TAC
 608 THEN SCS_TAC
 609 THEN MP_TAC sqrt8_LE_CSTAB
 610 THEN REWRITE_TAC[cstab;h0]
 611 THEN REAL_ARITH_TAC);;
 612
 613
 614
 615 let MM_4I3_IMP_4M6=prove(`
 616 MMs_v39 scs_4I3 v /\
 617     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) ==>
 618     ~(MMs_v39 (scs_4M6') ={})`,
 619 STRIP_TAC
 620 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
 621 THEN EXISTS_TAC`v:num->real^3`
 622 THEN EXISTS_TAC` scs_4I3 `
 623 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I3 `;`v`]
 624 THEN ASSUME_TAC SCS_4M6_BASIC
 625 THEN ASSUME_TAC K_SCS_4M6
 626 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4I3_IS_SCS;SCS_4I3_BASIC;K_SCS_4I3;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4I3_13;BB_4I3_IMP_BB_4M6]
 627 THEN SCS_TAC
 628 THEN REAL_ARITH_TAC);;
 629
 630
 631
 632
 633 let BB_4I3_IMP_BB_STAN_4I3= prove(`
 634     BBs_v39 scs_4I3 v /\
 635     scs_diag 4 i j /\
 636    dist(v i,v j)<= cstab ==>
 637     BBs_v39 (scs_stab_diag_v39 scs_4I3 i j) v`,
 638 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4I3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
 639 THEN REPEAT RESA_TAC
 640 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
 641 THEN SCS_TAC
 642 THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
 643 THEN RESA_TAC
 644 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
 645 THENL[
 646 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I3`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4I3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4I3_IS_SCS]
 647 THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
 648 THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
 649
 650 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I3`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4I3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4I3_IS_SCS]
 651 THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
 652 THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
 653 THEN ONCE_REWRITE_TAC[DIST_SYM]
 654 THEN ASM_REWRITE_TAC[]]);;
 655
 656
 657 let MM_4I3_IMP_STAB_4I3=prove(`
 658    MMs_v39 scs_4I3 v /\
 659     scs_diag 4 i j /\
 660    dist(v i,v j)<= cstab ==>
 661     ~(MMs_v39 (scs_stab_diag_v39 scs_4I3 i j) ={})`,
 662 STRIP_TAC
 663 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
 664 THEN EXISTS_TAC`v:num->real^3`
 665 THEN EXISTS_TAC` scs_4I3 `
 666 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I3 `;`v`]
 667 THEN ASSUME_TAC SCS_4I3_BASIC
 668 THEN ASSUME_TAC K_SCS_4I3
 669 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4I3_IS_SCS;SCS_4I3_BASIC;K_SCS_4I3;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4I3_13;BB_4I3_IMP_BB_STAN_4I3;STAB_4I3_SCS]
 670 THEN SCS_TAC
 671 THEN REAL_ARITH_TAC);;
 672
 673 let SCS_4I3_ARROW_SCS_4M6_STAB_4I3=prove_by_refinement(
 674 ` scs_arrow_v39 { scs_4I3 } ({scs_4M6'} UNION {scs_stab_diag_v39 scs_4I3 i j| scs_diag 4 i j})`,
 675 [
 676 REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM]
 677 THEN ABBREV_TAC`k=scs_k_v39 s`
 678 THEN REPEAT RESA_TAC;
 679
 680
 681 ASM_SIMP_TAC[SCS_4M6_IS_SCS];
 682
 683
 684 ASM_SIMP_TAC[STAB_4I3_SCS;K_SCS_4I3];
 685
 686
 687 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4I3 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4I3 ==> MMs_v39 s = {}))`);
 688
 689
 690 ASM_REWRITE_TAC[];
 691
 692
 693
 694 ASM_REWRITE_TAC[]
 695 THEN POP_ASSUM MP_TAC
 696 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
 697 THEN REPEAT STRIP_TAC
 698 THEN POP_ASSUM MP_TAC
 699 THEN RESA_TAC
 700 THEN POP_ASSUM MP_TAC
 701 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
 702 THEN STRIP_TAC;
 703
 704
 705 MP_TAC(SET_RULE`(!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j))\/ ~((!i j. scs_diag 4 i j ==>   cstab < dist((v:num->real^3) i,v j)))`)
 706 THEN RESA_TAC;
 707
 708
 709 EXISTS_TAC`scs_4M6'`
 710 THEN ASM_REWRITE_TAC[]
 711 THEN MP_TAC MM_4I3_IMP_4M6
 712 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
 713 THEN RESA_TAC
 714 THEN MATCH_DICH_TAC 0
 715 THEN ASM_REWRITE_TAC[]
 716 THEN EXISTS_TAC`v:num->real^3`
 717 THEN ASM_REWRITE_TAC[];
 718
 719
 720 POP_ASSUM MP_TAC
 721 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
 722 THEN STRIP_TAC
 723 THEN MP_TAC MM_4I3_IMP_STAB_4I3
 724 THEN RESA_TAC
 725 THEN DICH_TAC 0
 726 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
 727 THEN STRIP_TAC
 728 THEN EXISTS_TAC `scs_stab_diag_v39 scs_4I3 i j`
 729 THEN ASM_REWRITE_TAC[]
 730 THEN STRIP_TAC;
 731
 732 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
 733 THEN EXISTS_TAC`i:num`
 734 THEN EXISTS_TAC`j:num`
 735 THEN ASM_REWRITE_TAC[];
 736
 737
 738 EXISTS_TAC`v':num->real^3`
 739 THEN ASM_REWRITE_TAC[]]);;
 740
 741
 742 let SET_STAB_4I3=prove(`{ scs_stab_diag_v39 scs_4I3 i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4I3 (i MOD 4) (j  MOD 4)| scs_diag 4 (i MOD 4) (j  MOD 4) }`,
 743  ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
 744 THEN MRESAL_TAC STAB_MOD[`scs_4I3`][SCS_4I3_IS_SCS;K_SCS_4I3]);;
 745
 746 let EXPAND_STAB_DIAG_4I3=prove(`
 747 {scs_stab_diag_v39 scs_4I3 (i MOD 4) (j MOD 4) | j MOD 4 =
 748                                                   (i MOD 4 + 2) MOD 4}=
 749 {scs_stab_diag_v39 scs_4I3 (i+2) i| i<4} `,
 750 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4I3_IS_SCS;K_SCS_4I3]);;
 751
 752
 753 let SET_EQ_DIAG_STAB_4I3=prove_by_refinement(
 754 `scs_arrow_v39
 755  { scs_stab_diag_v39 scs_4I3 i j| scs_diag 4 i j }
 756  {scs_stab_diag_v39 scs_4I3 0 2,scs_stab_diag_v39 scs_4I3 1 3}`,
 757 [
 758 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4I3;SET_STAB_4I3;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
 759 THEN
 760 REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4I3 (i + 2) i |i=0\/i=1\/i=2\/i=3}
 761 = {scs_stab_diag_v39 scs_4I3 (0 + 2) 0} UNION
 762 {scs_stab_diag_v39 scs_4I3 (1 + 2) 1} UNION
 763 {scs_stab_diag_v39 scs_4I3 (2 + 2) 2} UNION
 764 {scs_stab_diag_v39 scs_4I3 (3 + 2) 3}
 765 `;]
 766 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4I3 0 2,scs_stab_diag_v39 scs_4I3 1 3}={scs_stab_diag_v39 scs_4I3 0 2} UNION {scs_stab_diag_v39 scs_4I3 1 3}UNION {scs_stab_diag_v39 scs_4I3 0 2} UNION {scs_stab_diag_v39 scs_4I3 1 3}`]
 767 THEN MATCH_MP_TAC FZIOTEF_UNION
 768 THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
 769 THEN MRESA_TAC STAB_SYM[`scs_4I3`;`0`;`2`]
 770 THEN STRIP_TAC;
 771
 772 MATCH_MP_TAC FZIOTEF_REFL
 773 THEN REWRITE_TAC[IN_SING]
 774 THEN REPEAT RESA_TAC
 775 THEN ASM_SIMP_TAC[STAB_4I3_SCS;SCS_DIAG_SCS_4I3_02];
 776
 777 MATCH_MP_TAC FZIOTEF_UNION
 778 THEN MRESA_TAC STAB_SYM[`scs_4I3`;`1`;`3`]
 779 THEN STRIP_TAC;
 780
 781
 782 MATCH_MP_TAC FZIOTEF_REFL
 783 THEN REWRITE_TAC[IN_SING]
 784 THEN REPEAT RESA_TAC
 785 THEN ASM_SIMP_TAC[STAB_4I3_SCS;SCS_DIAG_SCS_4I3_13];
 786
 787 MATCH_MP_TAC FZIOTEF_UNION
 788 THEN MRESAL_TAC STAB_MOD[`scs_4I3`;`4`;`2`][SCS_4I3_IS_SCS;K_SCS_4I3;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
 789 THEN SYM_ASSUM_TAC
 790 THEN STRIP_TAC;
 791
 792 MATCH_MP_TAC FZIOTEF_REFL
 793 THEN REWRITE_TAC[IN_SING]
 794 THEN REPEAT RESA_TAC
 795 THEN ASM_SIMP_TAC[STAB_4I3_SCS;SCS_DIAG_SCS_4I3_02];
 796
 797 MRESAL_TAC STAB_MOD[`scs_4I3`;`5`;`3`][SCS_4I3_IS_SCS;K_SCS_4I3;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
 798 THEN SYM_ASSUM_TAC;
 799
 800 MATCH_MP_TAC FZIOTEF_REFL
 801 THEN REWRITE_TAC[IN_SING]
 802 THEN REPEAT RESA_TAC
 803 THEN ASM_SIMP_TAC[STAB_4I3_SCS;SCS_DIAG_SCS_4I3_13]]);;
 804
 805
 806 let VQFYMZY=prove(` scs_arrow_v39 { scs_4I3 } ({scs_4M6', scs_4T4})`,
 807
 808 MATCH_MP_TAC FZIOTEF_TRANS
 809 THEN EXISTS_TAC`({scs_4M6'} UNION {scs_stab_diag_v39 scs_4I3 i j| scs_diag 4 i j})`
 810 THEN ASM_SIMP_TAC[SCS_4I3_ARROW_SCS_4M6_STAB_4I3;SET_RULE`{a,b}={a}UNION {b}`]
 811 THEN MATCH_MP_TAC FZIOTEF_UNION
 812 THEN STRIP_TAC
 813 THENL[
 814
 815 MATCH_MP_TAC FZIOTEF_REFL
 816 THEN REWRITE_TAC[IN_SING]
 817 THEN REPEAT RESA_TAC
 818 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS];
 819
 820 MATCH_MP_TAC FZIOTEF_TRANS
 821 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4I3 0 2,scs_stab_diag_v39 scs_4I3 1 3}`
 822 THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_4I3;SET_RULE`{a,b}={a}UNION {b}`]
 823 THEN ONCE_REWRITE_TAC[SET_RULE` {scs_4T4}={scs_4T4} UNION {scs_4T4}`]
 824 THEN MATCH_MP_TAC FZIOTEF_UNION
 825 THEN ASM_SIMP_TAC[ZNLLLDL;SCS_4I3_ARROW_4T4]]);;
 826
 827
 828
 829 (***********************)
 830
 831
 832
 833
 834
 835 let BB_4M2_IMP_BB_4M6= prove
 836 (`
 837     BBs_v39 scs_4M2 v /\
 838     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) ==>
 839     BBs_v39 (scs_4M6') v`,
 840 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M2;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M2;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
 841 THEN REPEAT RESA_TAC
 842 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
 843 THEN SCS_TAC
 844 THEN THAYTHE_TAC 1[`i`;`j`]
 845 THEN DICH_TAC 0
 846 THEN THAYTHE_TAC 2[`i`;`j`]
 847 THEN DICH_TAC 0
 848 THEN DICH_TAC 0
 849 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
 850 THEN SYM_ASSUM_TAC
 851 THEN REWRITE_TAC[ADD1]
 852 THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`]
 853 THEN SYM_ASSUM_TAC
 854 THEN MRESA_TAC MOD_ADD_MOD[`j`;`1`;`4`]
 855 THEN SYM_ASSUM_TAC
 856 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
 857 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
 858 THEN RESA_TAC
 859 THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
 860 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
 861 THEN RESA_TAC
 862 THEN SCS_TAC
 863 THEN MP_TAC sqrt8_LE_CSTAB
 864 THEN REWRITE_TAC[cstab;h0]
 865 THEN REAL_ARITH_TAC);;
 866
 867
 868
 869
 870 let MM_4M2_IMP_4M6=prove(
 871 `
 872 MMs_v39 scs_4M2 v /\
 873     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) ==>
 874     ~(MMs_v39 (scs_4M6') ={})`,
 875 STRIP_TAC
 876 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
 877 THEN EXISTS_TAC`v:num->real^3`
 878 THEN EXISTS_TAC` scs_4M2 `
 879 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M2 `;`v`]
 880 THEN ASSUME_TAC SCS_4M6_BASIC
 881 THEN ASSUME_TAC K_SCS_4M6
 882 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M2_IS_SCS;SCS_4M2_BASIC;K_SCS_4M2;SCS_K_D_A_STAB_EQ;IN; ADD1;BB_4M2_IMP_BB_4M6]
 883 THEN SCS_TAC
 884 THEN REAL_ARITH_TAC);;
 885
 886
 887
 888
 889 let BB_4M2_IMP_BB_STAN_4M2= prove(
 890 `
 891     BBs_v39 scs_4M2 v /\
 892     scs_diag 4 i j /\
 893    dist(v i,v j)<= cstab ==>
 894     BBs_v39 (scs_stab_diag_v39 scs_4M2 i j) v`,
 895 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M2;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M2;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
 896 THEN REPEAT RESA_TAC
 897 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
 898 THEN SCS_TAC
 899 THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
 900 THEN RESA_TAC
 901 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
 902 THENL[
 903 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M2`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M2;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M2;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M2_IS_SCS]
 904 THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
 905 THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
 906
 907 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M2`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M2;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M2;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M2_IS_SCS]
 908 THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
 909 THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
 910 THEN ONCE_REWRITE_TAC[DIST_SYM]
 911 THEN ASM_REWRITE_TAC[]]);;
 912
 913
 914 let MM_4M2_IMP_STAB_4M2=prove(`
 915    MMs_v39 scs_4M2 v /\
 916     scs_diag 4 i j /\
 917    dist(v i,v j)<= cstab ==>
 918     ~(MMs_v39 (scs_stab_diag_v39 scs_4M2 i j) ={})`,
 919 STRIP_TAC
 920 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
 921 THEN EXISTS_TAC`v:num->real^3`
 922 THEN EXISTS_TAC` scs_4M2 `
 923 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M2 `;`v`]
 924 THEN ASSUME_TAC SCS_4M2_BASIC
 925 THEN ASSUME_TAC K_SCS_4M2
 926 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M2_IS_SCS;SCS_4M2_BASIC;K_SCS_4M2;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M2_13;BB_4M2_IMP_BB_STAN_4M2;STAB_4M2_SCS]
 927 THEN SCS_TAC
 928 THEN REAL_ARITH_TAC);;
 929
 930
 931
 932 let SCS_4M2_ARROW_SCS_4M6_STAB_4M2=prove_by_refinement(
 933 ` scs_arrow_v39 { scs_4M2 } ({scs_4M6'} UNION {scs_stab_diag_v39 scs_4M2 i j| scs_diag 4 i j})`,
 934 [
 935 REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM]
 936 THEN ABBREV_TAC`k=scs_k_v39 s`
 937 THEN REPEAT RESA_TAC;
 938
 939
 940 ASM_SIMP_TAC[SCS_4M6_IS_SCS];
 941
 942
 943 ASM_SIMP_TAC[STAB_4M2_SCS;K_SCS_4M2];
 944
 945
 946 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M2 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M2 ==> MMs_v39 s = {}))`);
 947
 948
 949 ASM_REWRITE_TAC[];
 950
 951
 952
 953 ASM_REWRITE_TAC[]
 954 THEN POP_ASSUM MP_TAC
 955 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
 956 THEN REPEAT STRIP_TAC
 957 THEN POP_ASSUM MP_TAC
 958 THEN RESA_TAC
 959 THEN POP_ASSUM MP_TAC
 960 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
 961 THEN STRIP_TAC;
 962
 963
 964 MP_TAC(SET_RULE`(!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j))\/ ~((!i j. scs_diag 4 i j ==>   cstab < dist((v:num->real^3) i,v j)))`)
 965 THEN RESA_TAC;
 966
 967
 968 EXISTS_TAC`scs_4M6'`
 969 THEN ASM_REWRITE_TAC[]
 970 THEN MP_TAC MM_4M2_IMP_4M6
 971 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
 972 THEN RESA_TAC
 973 THEN MATCH_DICH_TAC 0
 974 THEN ASM_REWRITE_TAC[]
 975 THEN EXISTS_TAC`v:num->real^3`
 976 THEN ASM_REWRITE_TAC[];
 977
 978
 979 POP_ASSUM MP_TAC
 980 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
 981 THEN STRIP_TAC
 982 THEN MP_TAC MM_4M2_IMP_STAB_4M2
 983 THEN RESA_TAC
 984 THEN DICH_TAC 0
 985 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
 986 THEN STRIP_TAC
 987 THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M2 i j`
 988 THEN ASM_REWRITE_TAC[]
 989 THEN STRIP_TAC;
 990
 991 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
 992 THEN EXISTS_TAC`i:num`
 993 THEN EXISTS_TAC`j:num`
 994 THEN ASM_REWRITE_TAC[];
 995
 996
 997 EXISTS_TAC`v':num->real^3`
 998 THEN ASM_REWRITE_TAC[]]);;
 999
1000
1001
1002 let SET_STAB_4M2=prove(`{ scs_stab_diag_v39 scs_4M2 i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M2 (i MOD 4) (j  MOD 4)| scs_diag 4 (i MOD 4) (j  MOD 4) }`,
1003  ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
1004 THEN MRESAL_TAC STAB_MOD[`scs_4M2`][SCS_4M2_IS_SCS;K_SCS_4M2]);;
1005
1006 let EXPAND_STAB_DIAG_4M2=prove(`
1007 {scs_stab_diag_v39 scs_4M2 (i MOD 4) (j MOD 4) | j MOD 4 =
1008                                                   (i MOD 4 + 2) MOD 4}=
1009 {scs_stab_diag_v39 scs_4M2 (i+2) i| i<4} `,
1010 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M2_IS_SCS;K_SCS_4M2]);;
1011
1012
1013 let SET_EQ_DIAG_STAB_4M2=prove_by_refinement(
1014 `scs_arrow_v39
1015  { scs_stab_diag_v39 scs_4M2 i j| scs_diag 4 i j }
1016  {scs_stab_diag_v39 scs_4M2 0 2,scs_stab_diag_v39 scs_4M2 1 3}`,
1017 [
1018 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M2;SET_STAB_4M2;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
1019 THEN
1020 REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M2 (i + 2) i |i=0\/i=1\/i=2\/i=3}
1021 = {scs_stab_diag_v39 scs_4M2 (0 + 2) 0} UNION
1022 {scs_stab_diag_v39 scs_4M2 (1 + 2) 1} UNION
1023 {scs_stab_diag_v39 scs_4M2 (2 + 2) 2} UNION
1024 {scs_stab_diag_v39 scs_4M2 (3 + 2) 3}
1025 `;]
1026 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M2 0 2,scs_stab_diag_v39 scs_4M2 1 3}={scs_stab_diag_v39 scs_4M2 0 2} UNION {scs_stab_diag_v39 scs_4M2 1 3}UNION {scs_stab_diag_v39 scs_4M2 0 2} UNION {scs_stab_diag_v39 scs_4M2 1 3}`]
1027 THEN MATCH_MP_TAC FZIOTEF_UNION
1028 THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
1029 THEN MRESA_TAC STAB_SYM[`scs_4M2`;`0`;`2`]
1030 THEN STRIP_TAC;
1031
1032 MATCH_MP_TAC FZIOTEF_REFL
1033 THEN REWRITE_TAC[IN_SING]
1034 THEN REPEAT RESA_TAC
1035 THEN ASM_SIMP_TAC[STAB_4M2_SCS;SCS_DIAG_SCS_4M2_02];
1036
1037 MATCH_MP_TAC FZIOTEF_UNION
1038 THEN MRESA_TAC STAB_SYM[`scs_4M2`;`1`;`3`]
1039 THEN STRIP_TAC;
1040
1041
1042 MATCH_MP_TAC FZIOTEF_REFL
1043 THEN REWRITE_TAC[IN_SING]
1044 THEN REPEAT RESA_TAC
1045 THEN ASM_SIMP_TAC[STAB_4M2_SCS;SCS_DIAG_SCS_4M2_13];
1046
1047 MATCH_MP_TAC FZIOTEF_UNION
1048 THEN MRESAL_TAC STAB_MOD[`scs_4M2`;`4`;`2`][SCS_4M2_IS_SCS;K_SCS_4M2;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
1049 THEN SYM_ASSUM_TAC
1050 THEN STRIP_TAC;
1051
1052 MATCH_MP_TAC FZIOTEF_REFL
1053 THEN REWRITE_TAC[IN_SING]
1054 THEN REPEAT RESA_TAC
1055 THEN ASM_SIMP_TAC[STAB_4M2_SCS;SCS_DIAG_SCS_4M2_02];
1056
1057 MRESAL_TAC STAB_MOD[`scs_4M2`;`5`;`3`][SCS_4M2_IS_SCS;K_SCS_4M2;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
1058 THEN SYM_ASSUM_TAC;
1059
1060 MATCH_MP_TAC FZIOTEF_REFL
1061 THEN REWRITE_TAC[IN_SING]
1062 THEN REPEAT RESA_TAC
1063 THEN ASM_SIMP_TAC[STAB_4M2_SCS;SCS_DIAG_SCS_4M2_13]]);;
1064
1065
1066
1067 let PROP_OPP_DIAG_4M2_13= prove_by_refinement(`scs_stab_diag_v39 scs_4M2 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4M2 0 2)) 2 `,
1068 [REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;SCS_K_D_A_STAB_EQ;scs_opp_v39]
1069 THEN MATCH_MP_TAC scs_inj
1070 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M2_BASIC;STAB_4M2_SCS;SCS_DIAG_SCS_4M2_13;scs_basic;unadorned_v39;peropp;peropp2]
1071 THEN SCS_TAC
1072 THEN STRIP_TAC;
1073
1074 SET_TAC[];
1075
1076
1077 STRIP_TAC
1078 THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;]
1079 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
1080 THEN REPEAT GEN_TAC
1081 THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
1082 THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
1083 THEN SYM_ASSUM_TAC
1084 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
1085 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
1086 THEN SYM_ASSUM_TAC
1087 THEN SYM_ASSUM_TAC
1088 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`)
1089 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
1090 THEN RESA_TAC
1091 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`)
1092 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
1093 THEN RESA_TAC
1094 THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_4_TAC;PSORT_5_EXPLICIT;ARITH_RULE`4-1=3/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6
1095 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;
1096
1097
1098 let STAB_4M2_02_ARROW_4M2_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M2 0 2}{scs_stab_diag_v39 scs_4M2 1 3}`,
1099 ASM_SIMP_TAC[PROP_OPP_DIAG_4M2_13]
1100 THEN MATCH_MP_TAC FZIOTEF_TRANS
1101 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4M2 0 2)}`
1102 THEN STRIP_TAC
1103 THENL[
1104 MATCH_MP_TAC (GEN_ALL YXIONXL2)
1105 THEN EXISTS_TAC`4`
1106 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M2;STAB_4M2_SCS;SCS_DIAG_SCS_4M2_02]
1107 ;
1108
1109 MATCH_MP_TAC(GEN_ALL YXIONXL3)
1110 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
1111 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4M2 0 2)`
1112 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M2;STAB_4M2_SCS;SCS_DIAG_SCS_4M2_02]]);;
1113
1114
1115 let SCS_4M2_SLICE_13=prove_by_refinement(
1116 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M2 1 3 } {scs_prop_equ_v39 scs_3M1 1,  scs_3T4 }`,
1117 [
1118 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
1119 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M2_13;STAB_4M2_SCS;SCS_K_D_A_STAB_EQ;]
1120 THEN EXISTS_TAC`1`
1121 THEN EXISTS_TAC`3`
1122 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M2_13]
1123 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
1124 THEN REPEAT RESA_TAC;
1125
1126 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
1127 THEN STRIP_TAC
1128 THEN MATCH_MP_TAC scs_inj
1129 THEN ASM_SIMP_TAC[SCS_3T4_BASIC;SCS_4M2_BASIC;J_SCS_4M2;BASIC_HALF_SLICE_STAB;J_SCS_3T4;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3M1_BASIC;J_SCS_3M1]
1130 THEN STRIP_TAC;
1131
1132
1133 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2]
1134 THEN ARITH_TAC;
1135
1136 STRIP_TAC
1137 THEN
1138 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2;
1139 ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
1140 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1141 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1142 THEN SCS_TAC
1143 THEN REPEAT GEN_TAC
1144 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1145 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1146 THEN RESA_TAC
1147 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1148 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1149 THEN RESA_TAC
1150 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1151 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
1152 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
1153 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
1154 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
1155 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
1156 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
1157 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
1158 THEN ASM_TAC
1159 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/\
1160 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1161 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1162 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1163 THEN REPEAT RESA_TAC
1164 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)
1165 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1166 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1167 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1168 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1169 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1170 THEN SYM_ASSUM_TAC
1171 THEN SCS_TAC;
1172
1173 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2]
1174 THEN ARITH_TAC;
1175
1176 STRIP_TAC
1177 THEN
1178 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2;scs_3T4_prime;scs_5M3;
1179 ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
1180 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1181 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1182 THEN SCS_TAC
1183 THEN REPEAT GEN_TAC
1184 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1185 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1186 THEN RESA_TAC
1187 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1188 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1189 THEN RESA_TAC
1190 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1191 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
1192 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
1193 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
1194 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
1195 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
1196 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
1197 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
1198 THEN ASM_TAC
1199 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/\
1200 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1201 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1202 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1203 THEN REPEAT RESA_TAC
1204 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)
1205 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1206 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1207 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1208 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1209 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1210 THEN SYM_ASSUM_TAC
1211 THEN SCS_TAC;
1212
1213 SCS_TAC
1214 THEN REAL_ARITH_TAC;
1215
1216 SCS_TAC
1217 THEN REAL_ARITH_TAC;
1218
1219 SCS_TAC
1220 THEN REAL_ARITH_TAC;
1221
1222 SCS_TAC
1223 THEN REWRITE_TAC[cstab]
1224 THEN REAL_ARITH_TAC;
1225
1226
1227 SCS_TAC
1228 THEN REWRITE_TAC[cstab]
1229 THEN REAL_ARITH_TAC;
1230
1231
1232
1233 POP_ASSUM MP_TAC
1234 THEN REWRITE_TAC[J_SCS_3M1];
1235
1236 ]);;
1237
1238 let BNAWVNH =prove_by_refinement(` scs_arrow_v39 { scs_4M2 } ({scs_4M6',scs_3M1, scs_3T4})`,
1239 [
1240 MATCH_MP_TAC FZIOTEF_TRANS
1241 THEN EXISTS_TAC`({scs_4M6'} UNION {scs_stab_diag_v39 scs_4M2 i j| scs_diag 4 i j})`
1242 THEN ASM_REWRITE_TAC[SCS_4M2_ARROW_SCS_4M6_STAB_4M2;SET_RULE`{A,B,C}={A}UNION{B,C}`]
1243 THEN MATCH_MP_TAC FZIOTEF_UNION
1244 THEN STRIP_TAC;
1245
1246 MATCH_MP_TAC FZIOTEF_REFL
1247 THEN REWRITE_TAC[IN_SING]
1248 THEN REPEAT RESA_TAC
1249 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS];
1250
1251 MATCH_MP_TAC FZIOTEF_TRANS
1252 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M2 0 2,scs_stab_diag_v39 scs_4M2 1 3}`
1253 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M2]
1254 THEN MATCH_MP_TAC FZIOTEF_TRANS
1255 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M2 1 3,scs_stab_diag_v39 scs_4M2 1 3}`
1256 THEN STRIP_TAC;
1257
1258 REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`]
1259 THEN MATCH_MP_TAC FZIOTEF_UNION
1260 THEN ASM_REWRITE_TAC[STAB_4M2_02_ARROW_4M2_13];
1261
1262 MATCH_MP_TAC FZIOTEF_REFL
1263 THEN REWRITE_TAC[IN_SING]
1264 THEN REPEAT RESA_TAC
1265 THEN ASM_SIMP_TAC[STAB_4M2_SCS;SCS_DIAG_SCS_4M2_13];
1266
1267 REWRITE_TAC[SET_RULE`{A,A}={A}`]
1268 THEN MATCH_MP_TAC FZIOTEF_TRANS
1269 THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3M1 1,  scs_3T4 }`
1270 THEN ASM_REWRITE_TAC[SCS_4M2_SLICE_13;SET_RULE`{A,B}={A}UNION {B}`]
1271 THEN MATCH_MP_TAC FZIOTEF_UNION
1272 THEN STRIP_TAC;
1273
1274 MRESAS_TAC PRO_EQU_ID1[`scs_3M1`;`1`;`3`][SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`(3 - 1 MOD 3)=2`]
1275 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1 1`;`2`][PROP_EQU_IS_SCS;SCS_3M1_IS_SCS]
1276 THEN DICH_TAC 0
1277 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1278 THEN REWRITE_TAC[];
1279
1280 MATCH_MP_TAC FZIOTEF_REFL
1281 THEN REWRITE_TAC[IN_SING]
1282 THEN REPEAT RESA_TAC
1283 THEN ASM_SIMP_TAC[SCS_3T4_IS_SCS]]);;
1284
1285
1286
1287 (***************************)
1288
1289
1290 let BB_4M3_IMP_BB_4M6= prove
1291 (`
1292     BBs_v39 scs_4M3' v /\
1293     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) ==>
1294     BBs_v39 (scs_4M6') v`,
1295 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
1296 THEN REPEAT RESA_TAC
1297 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
1298 THEN SCS_TAC
1299 THEN THAYTHE_TAC 1[`i`;`j`]
1300 THEN DICH_TAC 0
1301 THEN THAYTHE_TAC 2[`i`;`j`]
1302 THEN DICH_TAC 0
1303 THEN DICH_TAC 0
1304 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
1305 THEN SYM_ASSUM_TAC
1306 THEN REWRITE_TAC[ADD1]
1307 THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`]
1308 THEN SYM_ASSUM_TAC
1309 THEN MRESA_TAC MOD_ADD_MOD[`j`;`1`;`4`]
1310 THEN SYM_ASSUM_TAC
1311 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
1312 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
1313 THEN RESA_TAC
1314 THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
1315 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
1316 THEN RESA_TAC
1317 THEN SCS_TAC
1318 THEN MP_TAC sqrt8_LE_CSTAB
1319 THEN MP_TAC LE_sqrt8_2h0
1320 THEN REWRITE_TAC[cstab;h0]
1321 THEN REAL_ARITH_TAC);;
1322
1323
1324
1325
1326 let MM_4M3_IMP_4M6=prove(
1327 `
1328 MMs_v39 scs_4M3' v /\
1329     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) ==>
1330     ~(MMs_v39 (scs_4M6') ={})`,
1331 STRIP_TAC
1332 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
1333 THEN EXISTS_TAC`v:num->real^3`
1334 THEN EXISTS_TAC` scs_4M3' `
1335 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M3' `;`v`]
1336 THEN ASSUME_TAC SCS_4M6_BASIC
1337 THEN ASSUME_TAC K_SCS_4M6
1338 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M3_IS_SCS;SCS_4M3_BASIC;K_SCS_4M3;SCS_K_D_A_STAB_EQ;IN; ADD1;BB_4M3_IMP_BB_4M6]
1339 THEN SCS_TAC
1340 THEN REAL_ARITH_TAC);;
1341
1342
1343
1344
1345 let BB_4M3_IMP_BB_STAN_4M3= prove(
1346 `
1347     BBs_v39 scs_4M3' v /\
1348     scs_diag 4 i j /\
1349    dist(v i,v j)<= cstab ==>
1350     BBs_v39 (scs_stab_diag_v39 scs_4M3' i j) v`,
1351 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
1352 THEN REPEAT RESA_TAC
1353 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
1354 THEN SCS_TAC
1355 THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
1356 THEN RESA_TAC
1357 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
1358 THENL[
1359 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M3'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M3_IS_SCS]
1360 THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
1361 THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
1362
1363 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M3'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M3_IS_SCS]
1364 THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
1365 THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
1366 THEN ONCE_REWRITE_TAC[DIST_SYM]
1367 THEN ASM_REWRITE_TAC[]]);;
1368
1369
1370
1371
1372 let MM_4M3_IMP_STAB_4M3=prove(`
1373    MMs_v39 scs_4M3' v /\
1374     scs_diag 4 i j /\
1375    dist(v i,v j)<= cstab ==>
1376     ~(MMs_v39 (scs_stab_diag_v39 scs_4M3' i j) ={})`,
1377 STRIP_TAC
1378 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
1379 THEN EXISTS_TAC`v:num->real^3`
1380 THEN EXISTS_TAC` scs_4M3' `
1381 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M3' `;`v`]
1382 THEN ASSUME_TAC SCS_4M3_BASIC
1383 THEN ASSUME_TAC K_SCS_4M3
1384 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M3_IS_SCS;SCS_4M3_BASIC;K_SCS_4M3;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M3_13;BB_4M3_IMP_BB_STAN_4M3;STAB_4M3_SCS]
1385 THEN SCS_TAC
1386 THEN REAL_ARITH_TAC);;
1387
1388
1389
1390
1391 let SCS_4M3_ARROW_SCS_4M6_STAB_4M3=prove_by_refinement(
1392 ` scs_arrow_v39 { scs_4M3' } ({scs_4M6'} UNION {scs_stab_diag_v39 scs_4M3' i j| scs_diag 4 i j})`,
1393 [
1394 REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM]
1395 THEN ABBREV_TAC`k=scs_k_v39 s`
1396 THEN REPEAT RESA_TAC;
1397
1398
1399 ASM_SIMP_TAC[SCS_4M6_IS_SCS];
1400
1401
1402 ASM_SIMP_TAC[STAB_4M3_SCS;K_SCS_4M3];
1403
1404
1405 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M3' ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M3' ==> MMs_v39 s = {}))`);
1406
1407
1408 ASM_REWRITE_TAC[];
1409
1410
1411
1412 ASM_REWRITE_TAC[]
1413 THEN POP_ASSUM MP_TAC
1414 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
1415 THEN REPEAT STRIP_TAC
1416 THEN POP_ASSUM MP_TAC
1417 THEN RESA_TAC
1418 THEN POP_ASSUM MP_TAC
1419 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1420 THEN STRIP_TAC;
1421
1422
1423 MP_TAC(SET_RULE`(!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j))\/ ~((!i j. scs_diag 4 i j ==>   cstab < dist((v:num->real^3) i,v j)))`)
1424 THEN RESA_TAC;
1425
1426
1427 EXISTS_TAC`scs_4M6'`
1428 THEN ASM_REWRITE_TAC[]
1429 THEN MP_TAC MM_4M3_IMP_4M6
1430 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1431 THEN RESA_TAC
1432 THEN MATCH_DICH_TAC 0
1433 THEN ASM_REWRITE_TAC[]
1434 THEN EXISTS_TAC`v:num->real^3`
1435 THEN ASM_REWRITE_TAC[];
1436
1437
1438 POP_ASSUM MP_TAC
1439 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
1440 THEN STRIP_TAC
1441 THEN MP_TAC MM_4M3_IMP_STAB_4M3
1442 THEN RESA_TAC
1443 THEN DICH_TAC 0
1444 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1445 THEN STRIP_TAC
1446 THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M3' i j`
1447 THEN ASM_REWRITE_TAC[]
1448 THEN STRIP_TAC;
1449
1450 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
1451 THEN EXISTS_TAC`i:num`
1452 THEN EXISTS_TAC`j:num`
1453 THEN ASM_REWRITE_TAC[];
1454
1455
1456 EXISTS_TAC`v':num->real^3`
1457 THEN ASM_REWRITE_TAC[]]);;
1458
1459
1460
1461
1462 let SET_STAB_4M3=prove(`{ scs_stab_diag_v39 scs_4M3' i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M3' (i MOD 4) (j  MOD 4)| scs_diag 4 (i MOD 4) (j  MOD 4) }`,
1463  ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
1464 THEN MRESAL_TAC STAB_MOD[`scs_4M3'`][SCS_4M3_IS_SCS;K_SCS_4M3]);;
1465
1466 let EXPAND_STAB_DIAG_4M3=prove(`
1467 {scs_stab_diag_v39 scs_4M3' (i MOD 4) (j MOD 4) | j MOD 4 =
1468                                                   (i MOD 4 + 2) MOD 4}=
1469 {scs_stab_diag_v39 scs_4M3' (i+2) i| i<4} `,
1470 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M3_IS_SCS;K_SCS_4M3]);;
1471
1472
1473 let SET_EQ_DIAG_STAB_4M3=prove_by_refinement(
1474 `scs_arrow_v39
1475  { scs_stab_diag_v39 scs_4M3' i j| scs_diag 4 i j }
1476  {scs_stab_diag_v39 scs_4M3' 0 2,scs_stab_diag_v39 scs_4M3' 1 3}`,
1477 [
1478 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M3;SET_STAB_4M3;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
1479 THEN
1480 REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M3' (i + 2) i |i=0\/i=1\/i=2\/i=3}
1481 = {scs_stab_diag_v39 scs_4M3' (0 + 2) 0} UNION
1482 {scs_stab_diag_v39 scs_4M3' (1 + 2) 1} UNION
1483 {scs_stab_diag_v39 scs_4M3' (2 + 2) 2} UNION
1484 {scs_stab_diag_v39 scs_4M3' (3 + 2) 3}
1485 `;]
1486 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M3' 0 2,scs_stab_diag_v39 scs_4M3' 1 3}={scs_stab_diag_v39 scs_4M3' 0 2} UNION {scs_stab_diag_v39 scs_4M3' 1 3}UNION {scs_stab_diag_v39 scs_4M3' 0 2} UNION {scs_stab_diag_v39 scs_4M3' 1 3}`]
1487 THEN MATCH_MP_TAC FZIOTEF_UNION
1488 THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
1489 THEN MRESA_TAC STAB_SYM[`scs_4M3'`;`0`;`2`]
1490 THEN STRIP_TAC;
1491
1492 MATCH_MP_TAC FZIOTEF_REFL
1493 THEN REWRITE_TAC[IN_SING]
1494 THEN REPEAT RESA_TAC
1495 THEN ASM_SIMP_TAC[STAB_4M3_SCS;SCS_DIAG_SCS_4M3_02];
1496
1497 MATCH_MP_TAC FZIOTEF_UNION
1498 THEN MRESA_TAC STAB_SYM[`scs_4M3'`;`1`;`3`]
1499 THEN STRIP_TAC;
1500
1501
1502 MATCH_MP_TAC FZIOTEF_REFL
1503 THEN REWRITE_TAC[IN_SING]
1504 THEN REPEAT RESA_TAC
1505 THEN ASM_SIMP_TAC[STAB_4M3_SCS;SCS_DIAG_SCS_4M3_13];
1506
1507 MATCH_MP_TAC FZIOTEF_UNION
1508 THEN MRESAL_TAC STAB_MOD[`scs_4M3'`;`4`;`2`][SCS_4M3_IS_SCS;K_SCS_4M3;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
1509 THEN SYM_ASSUM_TAC
1510 THEN STRIP_TAC;
1511
1512 MATCH_MP_TAC FZIOTEF_REFL
1513 THEN REWRITE_TAC[IN_SING]
1514 THEN REPEAT RESA_TAC
1515 THEN ASM_SIMP_TAC[STAB_4M3_SCS;SCS_DIAG_SCS_4M3_02];
1516
1517 MRESAL_TAC STAB_MOD[`scs_4M3'`;`5`;`3`][SCS_4M3_IS_SCS;K_SCS_4M3;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
1518 THEN SYM_ASSUM_TAC;
1519
1520 MATCH_MP_TAC FZIOTEF_REFL
1521 THEN REWRITE_TAC[IN_SING]
1522 THEN REPEAT RESA_TAC
1523 THEN ASM_SIMP_TAC[STAB_4M3_SCS;SCS_DIAG_SCS_4M3_13]]);;
1524
1525 let PROP_OPP_DIAG_4M3_13= prove_by_refinement(`scs_stab_diag_v39 scs_4M3' 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4M3' 0 2)) 2 `,
1526 [REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;SCS_K_D_A_STAB_EQ;scs_opp_v39]
1527 THEN MATCH_MP_TAC scs_inj
1528 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M3_BASIC;STAB_4M3_SCS;SCS_DIAG_SCS_4M3_13;scs_basic;unadorned_v39;peropp;peropp2]
1529 THEN SCS_TAC
1530 THEN STRIP_TAC;
1531
1532 SET_TAC[];
1533
1534
1535 STRIP_TAC
1536 THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;]
1537 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
1538 THEN REPEAT GEN_TAC
1539 THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
1540 THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
1541 THEN SYM_ASSUM_TAC
1542 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
1543 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
1544 THEN SYM_ASSUM_TAC
1545 THEN SYM_ASSUM_TAC
1546 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`)
1547 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
1548 THEN RESA_TAC
1549 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`)
1550 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
1551 THEN RESA_TAC
1552 THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_4_TAC;PSORT_5_EXPLICIT;ARITH_RULE`4-1=3/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6
1553 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;
1554
1555
1556 let STAB_4M3_02_ARROW_4M3_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M3' 0 2}{scs_stab_diag_v39 scs_4M3' 1 3}`,
1557 ASM_SIMP_TAC[PROP_OPP_DIAG_4M3_13]
1558 THEN MATCH_MP_TAC FZIOTEF_TRANS
1559 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4M3' 0 2)}`
1560 THEN STRIP_TAC
1561 THENL[
1562 MATCH_MP_TAC (GEN_ALL YXIONXL2)
1563 THEN EXISTS_TAC`4`
1564 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M3;STAB_4M3_SCS;SCS_DIAG_SCS_4M3_02]
1565 ;
1566
1567 MATCH_MP_TAC(GEN_ALL YXIONXL3)
1568 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
1569 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4M3' 0 2)`
1570 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M3;STAB_4M3_SCS;SCS_DIAG_SCS_4M3_02]]);;
1571
1572
1573 let SCS_4M3_SLICE_13=prove_by_refinement(
1574 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M3' 1 3 } {scs_prop_equ_v39 scs_3T1 1,  scs_prop_equ_v39 scs_3T6' 2}`,
1575 [MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
1576 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M3_13;STAB_4M3_SCS;SCS_K_D_A_STAB_EQ;]
1577 THEN EXISTS_TAC`1`
1578 THEN EXISTS_TAC`3`
1579 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M3_13]
1580 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
1581 THEN REPEAT RESA_TAC;
1582
1583
1584 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
1585 THEN STRIP_TAC
1586 THEN MATCH_MP_TAC scs_inj
1587 THEN ASM_SIMP_TAC[SCS_3T1_BASIC;SCS_4M3_BASIC;J_SCS_4M3;BASIC_HALF_SLICE_STAB;J_SCS_3T1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T6_BASIC;J_SCS_3T6]
1588 THEN STRIP_TAC;
1589
1590
1591 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M3]
1592 THEN ARITH_TAC;
1593
1594 STRIP_TAC
1595 THEN
1596 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M3;
1597 ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
1598 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1599 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1600 THEN SCS_TAC
1601 THEN REPEAT GEN_TAC
1602 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1603 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1604 THEN RESA_TAC
1605 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1606 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1607 THEN RESA_TAC
1608 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1609 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
1610 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
1611 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
1612 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
1613 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
1614 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
1615 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
1616 THEN ASM_TAC
1617 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/\
1618 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1619 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1620 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1621 THEN REPEAT RESA_TAC
1622 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)
1623 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1624 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1625 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1626 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1627 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1628 THEN SYM_ASSUM_TAC
1629 THEN SCS_TAC;
1630
1631 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T6;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M3]
1632 THEN ARITH_TAC;
1633
1634
1635 STRIP_TAC
1636 THEN
1637 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T6;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M3;
1638 ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
1639 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1640 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1641 THEN SCS_TAC
1642 THEN REPEAT GEN_TAC
1643 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1644 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1645 THEN RESA_TAC
1646 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1647 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1648 THEN RESA_TAC
1649 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1650 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
1651 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
1652 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
1653 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
1654 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
1655 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
1656 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
1657 THEN ASM_TAC
1658 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/\
1659 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1660 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1661 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1662 THEN REPEAT RESA_TAC
1663 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)
1664 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1665 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1666 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1667 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1668 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1669 THEN SYM_ASSUM_TAC
1670 THEN SCS_TAC;
1671
1672 SCS_TAC
1673 THEN REAL_ARITH_TAC;
1674
1675 SCS_TAC
1676 THEN REAL_ARITH_TAC;
1677
1678 SCS_TAC
1679 THEN REAL_ARITH_TAC;
1680
1681 SCS_TAC
1682 THEN REWRITE_TAC[cstab]
1683 THEN REAL_ARITH_TAC;
1684
1685
1686 SCS_TAC
1687 THEN REWRITE_TAC[cstab]
1688 THEN REAL_ARITH_TAC;
1689
1690
1691
1692 POP_ASSUM MP_TAC
1693 THEN REWRITE_TAC[J_SCS_3T1];
1694
1695 ]);;
1696
1697
1698
1699 let RAWZDIB =prove_by_refinement(
1700 ` scs_arrow_v39 { scs_4M3' } ({scs_4M6',scs_3T1, scs_3T6'})`,
1701 [
1702 MATCH_MP_TAC FZIOTEF_TRANS
1703 THEN EXISTS_TAC`({scs_4M6'} UNION {scs_stab_diag_v39 scs_4M3' i j| scs_diag 4 i j})`
1704 THEN ASM_REWRITE_TAC[SCS_4M3_ARROW_SCS_4M6_STAB_4M3;SET_RULE`{A,B,C}={A}UNION{B,C}`]
1705 THEN MATCH_MP_TAC FZIOTEF_UNION
1706 THEN STRIP_TAC;
1707
1708
1709 MATCH_MP_TAC FZIOTEF_REFL
1710 THEN REWRITE_TAC[IN_SING]
1711 THEN REPEAT RESA_TAC
1712 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS];
1713
1714 MATCH_MP_TAC FZIOTEF_TRANS
1715 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M3' 0 2,scs_stab_diag_v39 scs_4M3' 1 3}`
1716 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M3]
1717 THEN MATCH_MP_TAC FZIOTEF_TRANS
1718 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M3' 1 3,scs_stab_diag_v39 scs_4M3' 1 3}`
1719 THEN STRIP_TAC;
1720
1721 REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`]
1722 THEN MATCH_MP_TAC FZIOTEF_UNION
1723 THEN ASM_REWRITE_TAC[STAB_4M3_02_ARROW_4M3_13];
1724
1725 MATCH_MP_TAC FZIOTEF_REFL
1726 THEN REWRITE_TAC[IN_SING]
1727 THEN REPEAT RESA_TAC
1728 THEN ASM_SIMP_TAC[STAB_4M3_SCS;SCS_DIAG_SCS_4M3_13];
1729
1730 REWRITE_TAC[SET_RULE`{A,A}={A}`]
1731 THEN MATCH_MP_TAC FZIOTEF_TRANS
1732 THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3T1 1,  scs_prop_equ_v39 scs_3T6' 2}`
1733 THEN ASM_REWRITE_TAC[SCS_4M3_SLICE_13;SET_RULE`{A,B}={A}UNION {B}`]
1734 THEN MATCH_MP_TAC FZIOTEF_UNION
1735 THEN STRIP_TAC;
1736
1737 MRESAS_TAC PRO_EQU_ID1[`scs_3T1`;`1`;`3`][SCS_3T1_IS_SCS;K_SCS_3T1;ARITH_RULE`(3 - 1 MOD 3)=2`]
1738 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T1 1`;`2`][PROP_EQU_IS_SCS;SCS_3T1_IS_SCS]
1739 THEN DICH_TAC 0
1740 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1741 THEN REWRITE_TAC[];
1742
1743 MRESAS_TAC PRO_EQU_ID1[`scs_3T6'`;`2`;`3`][SCS_3T6_IS_SCS;K_SCS_3T6;ARITH_RULE`(3 - 2 MOD 3)=1`]
1744 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T6' 2`;`1`][PROP_EQU_IS_SCS;SCS_3T6_IS_SCS]
1745 THEN DICH_TAC 0
1746 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1747 THEN REWRITE_TAC[]]);;
1748
1749
1750 (************************************)
1751
1752 let BB_4M4_IMP_BB_4M7= prove
1753 (`
1754     BBs_v39 scs_4M4' v /\
1755     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) ==>
1756     BBs_v39 (scs_4M7) v`,
1757 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M4;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M4;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7]
1758 THEN REPEAT RESA_TAC
1759 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
1760 THEN SCS_TAC
1761 THEN THAYTHE_TAC 1[`i`;`j`]
1762 THEN DICH_TAC 0
1763 THEN THAYTHE_TAC 2[`i`;`j`]
1764 THEN DICH_TAC 0
1765 THEN DICH_TAC 0
1766 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
1767 THEN SYM_ASSUM_TAC
1768 THEN REWRITE_TAC[ADD1]
1769 THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`]
1770 THEN SYM_ASSUM_TAC
1771 THEN MRESA_TAC MOD_ADD_MOD[`j`;`1`;`4`]
1772 THEN SYM_ASSUM_TAC
1773 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
1774 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
1775 THEN RESA_TAC
1776 THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
1777 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
1778 THEN RESA_TAC
1779 THEN SCS_TAC
1780 THEN MP_TAC sqrt8_LE_CSTAB
1781 THEN MP_TAC LE_sqrt8_2h0
1782 THEN REWRITE_TAC[cstab;h0]
1783 THEN REAL_ARITH_TAC);;
1784
1785
1786 let MM_4M4_IMP_4M7=prove(
1787 `
1788 MMs_v39 scs_4M4' v /\
1789     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) ==>
1790     ~(MMs_v39 (scs_4M7) ={})`,
1791 STRIP_TAC
1792 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
1793 THEN EXISTS_TAC`v:num->real^3`
1794 THEN EXISTS_TAC` scs_4M4' `
1795 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M4' `;`v`]
1796 THEN ASSUME_TAC SCS_4M7_BASIC
1797 THEN ASSUME_TAC K_SCS_4M7
1798 THEN ASM_SIMP_TAC[SCS_4M7_IS_SCS;SCS_4M4_IS_SCS;SCS_4M4_BASIC;K_SCS_4M4;SCS_K_D_A_STAB_EQ;IN; ADD1;BB_4M4_IMP_BB_4M7]
1799 THEN SCS_TAC
1800 THEN REAL_ARITH_TAC);;
1801
1802
1803
1804 let BB_4M4_IMP_BB_STAN_4M4= prove(
1805 `
1806     BBs_v39 scs_4M4' v /\
1807     scs_diag 4 i j /\
1808    dist(v i,v j)<= cstab ==>
1809     BBs_v39 (scs_stab_diag_v39 scs_4M4' i j) v`,
1810 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M4;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M4;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7]
1811 THEN REPEAT RESA_TAC
1812 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
1813 THEN SCS_TAC
1814 THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
1815 THEN RESA_TAC
1816 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
1817 THENL[
1818 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M4'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M4;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M4;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7;SCS_4M4_IS_SCS]
1819 THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
1820 THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
1821
1822 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M4'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M4;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M4;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7;SCS_4M4_IS_SCS]
1823 THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
1824 THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
1825 THEN ONCE_REWRITE_TAC[DIST_SYM]
1826 THEN ASM_REWRITE_TAC[]]);;
1827
1828
1829
1830 let MM_4M4_IMP_STAB_4M4=prove(`
1831    MMs_v39 scs_4M4' v /\
1832     scs_diag 4 i j /\
1833    dist(v i,v j)<= cstab ==>
1834     ~(MMs_v39 (scs_stab_diag_v39 scs_4M4' i j) ={})`,
1835 STRIP_TAC
1836 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
1837 THEN EXISTS_TAC`v:num->real^3`
1838 THEN EXISTS_TAC` scs_4M4' `
1839 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M4' `;`v`]
1840 THEN ASSUME_TAC SCS_4M4_BASIC
1841 THEN ASSUME_TAC K_SCS_4M4
1842 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M4_IS_SCS;SCS_4M4_BASIC;K_SCS_4M4;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M4_13;BB_4M4_IMP_BB_STAN_4M4;STAB_4M4_SCS]
1843 THEN SCS_TAC
1844 THEN REAL_ARITH_TAC);;
1845
1846
1847
1848 let SCS_4M4_ARROW_SCS_4M7_STAB_4M4=prove_by_refinement(
1849 ` scs_arrow_v39 { scs_4M4' } ({scs_4M7} UNION {scs_stab_diag_v39 scs_4M4' i j| scs_diag 4 i j})`,
1850 [
1851 REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM]
1852 THEN ABBREV_TAC`k=scs_k_v39 s`
1853 THEN REPEAT RESA_TAC;
1854
1855
1856 ASM_SIMP_TAC[SCS_4M7_IS_SCS];
1857
1858
1859 ASM_SIMP_TAC[STAB_4M4_SCS;K_SCS_4M4];
1860
1861
1862 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M4' ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M4' ==> MMs_v39 s = {}))`);
1863
1864
1865 ASM_REWRITE_TAC[];
1866
1867
1868
1869 ASM_REWRITE_TAC[]
1870 THEN POP_ASSUM MP_TAC
1871 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
1872 THEN REPEAT STRIP_TAC
1873 THEN POP_ASSUM MP_TAC
1874 THEN RESA_TAC
1875 THEN POP_ASSUM MP_TAC
1876 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1877 THEN STRIP_TAC;
1878
1879
1880 MP_TAC(SET_RULE`(!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j))\/ ~((!i j. scs_diag 4 i j ==>   cstab < dist((v:num->real^3) i,v j)))`)
1881 THEN RESA_TAC;
1882
1883
1884 EXISTS_TAC`scs_4M7`
1885 THEN ASM_REWRITE_TAC[]
1886 THEN MP_TAC MM_4M4_IMP_4M7
1887 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1888 THEN RESA_TAC
1889 THEN MATCH_DICH_TAC 0
1890 THEN ASM_REWRITE_TAC[]
1891 THEN EXISTS_TAC`v:num->real^3`
1892 THEN ASM_REWRITE_TAC[];
1893
1894
1895 POP_ASSUM MP_TAC
1896 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
1897 THEN STRIP_TAC
1898 THEN MP_TAC MM_4M4_IMP_STAB_4M4
1899 THEN RESA_TAC
1900 THEN DICH_TAC 0
1901 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1902 THEN STRIP_TAC
1903 THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M4' i j`
1904 THEN ASM_REWRITE_TAC[]
1905 THEN STRIP_TAC;
1906
1907 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
1908 THEN EXISTS_TAC`i:num`
1909 THEN EXISTS_TAC`j:num`
1910 THEN ASM_REWRITE_TAC[];
1911
1912
1913 EXISTS_TAC`v':num->real^3`
1914 THEN ASM_REWRITE_TAC[]]);;
1915
1916
1917
1918
1919 let SET_STAB_4M4=prove(`{ scs_stab_diag_v39 scs_4M4' i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M4' (i MOD 4) (j  MOD 4)| scs_diag 4 (i MOD 4) (j  MOD 4) }`,
1920  ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
1921 THEN MRESAL_TAC STAB_MOD[`scs_4M4'`][SCS_4M4_IS_SCS;K_SCS_4M4]);;
1922
1923 let EXPAND_STAB_DIAG_4M4=prove(`
1924 {scs_stab_diag_v39 scs_4M4' (i MOD 4) (j MOD 4) | j MOD 4 =
1925                                                   (i MOD 4 + 2) MOD 4}=
1926 {scs_stab_diag_v39 scs_4M4' (i+2) i| i<4} `,
1927 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M4_IS_SCS;K_SCS_4M4]);;
1928
1929
1930 let SET_EQ_DIAG_STAB_4M4=prove_by_refinement(
1931 `scs_arrow_v39
1932  { scs_stab_diag_v39 scs_4M4' i j| scs_diag 4 i j }
1933  {scs_stab_diag_v39 scs_4M4' 0 2,scs_stab_diag_v39 scs_4M4' 1 3}`,
1934 [
1935 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M4;SET_STAB_4M4;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
1936 THEN
1937 REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M4' (i + 2) i |i=0\/i=1\/i=2\/i=3}
1938 = {scs_stab_diag_v39 scs_4M4' (0 + 2) 0} UNION
1939 {scs_stab_diag_v39 scs_4M4' (1 + 2) 1} UNION
1940 {scs_stab_diag_v39 scs_4M4' (2 + 2) 2} UNION
1941 {scs_stab_diag_v39 scs_4M4' (3 + 2) 3}
1942 `;]
1943 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M4' 0 2,scs_stab_diag_v39 scs_4M4' 1 3}={scs_stab_diag_v39 scs_4M4' 0 2} UNION {scs_stab_diag_v39 scs_4M4' 1 3}UNION {scs_stab_diag_v39 scs_4M4' 0 2} UNION {scs_stab_diag_v39 scs_4M4' 1 3}`]
1944 THEN MATCH_MP_TAC FZIOTEF_UNION
1945 THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
1946 THEN MRESA_TAC STAB_SYM[`scs_4M4'`;`0`;`2`]
1947 THEN STRIP_TAC;
1948
1949 MATCH_MP_TAC FZIOTEF_REFL
1950 THEN REWRITE_TAC[IN_SING]
1951 THEN REPEAT RESA_TAC
1952 THEN ASM_SIMP_TAC[STAB_4M4_SCS;SCS_DIAG_SCS_4M4_02];
1953
1954 MATCH_MP_TAC FZIOTEF_UNION
1955 THEN MRESA_TAC STAB_SYM[`scs_4M4'`;`1`;`3`]
1956 THEN STRIP_TAC;
1957
1958
1959 MATCH_MP_TAC FZIOTEF_REFL
1960 THEN REWRITE_TAC[IN_SING]
1961 THEN REPEAT RESA_TAC
1962 THEN ASM_SIMP_TAC[STAB_4M4_SCS;SCS_DIAG_SCS_4M4_13];
1963
1964 MATCH_MP_TAC FZIOTEF_UNION
1965 THEN MRESAL_TAC STAB_MOD[`scs_4M4'`;`4`;`2`][SCS_4M4_IS_SCS;K_SCS_4M4;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
1966 THEN SYM_ASSUM_TAC
1967 THEN STRIP_TAC;
1968
1969 MATCH_MP_TAC FZIOTEF_REFL
1970 THEN REWRITE_TAC[IN_SING]
1971 THEN REPEAT RESA_TAC
1972 THEN ASM_SIMP_TAC[STAB_4M4_SCS;SCS_DIAG_SCS_4M4_02];
1973
1974 MRESAL_TAC STAB_MOD[`scs_4M4'`;`5`;`3`][SCS_4M4_IS_SCS;K_SCS_4M4;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
1975 THEN SYM_ASSUM_TAC;
1976
1977 MATCH_MP_TAC FZIOTEF_REFL
1978 THEN REWRITE_TAC[IN_SING]
1979 THEN REPEAT RESA_TAC
1980 THEN ASM_SIMP_TAC[STAB_4M4_SCS;SCS_DIAG_SCS_4M4_13]]);;
1981
1982 let SCS_4M4_SLICE_13=prove_by_refinement(
1983 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M4' 1 3 } {scs_prop_equ_v39 scs_3T4 2,  scs_3T4 }`,
1984 [
1985 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
1986 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M4_13;STAB_4M4_SCS;SCS_K_D_A_STAB_EQ;]
1987 THEN EXISTS_TAC`1`
1988 THEN EXISTS_TAC`3`
1989 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M4_13]
1990 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
1991 THEN REPEAT RESA_TAC;
1992
1993
1994 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
1995 THEN STRIP_TAC
1996 THEN MATCH_MP_TAC scs_inj
1997 THEN ASM_SIMP_TAC[SCS_3T4_BASIC;SCS_4M4_BASIC;J_SCS_4M4;BASIC_HALF_SLICE_STAB;J_SCS_3T4;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T6_BASIC;J_SCS_3T6]
1998 THEN STRIP_TAC;
1999
2000 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4]
2001 THEN ARITH_TAC;
2002
2003 STRIP_TAC
2004 THEN
2005 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4;
2006 ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
2007 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2008 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2009 THEN SCS_TAC
2010 THEN REPEAT GEN_TAC
2011 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
2012 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
2013 THEN RESA_TAC
2014 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
2015 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
2016 THEN RESA_TAC
2017 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2018 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
2019 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
2020 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
2021 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
2022 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
2023 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
2024 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
2025 THEN ASM_TAC
2026 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/\
2027 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2028 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2029 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2030 THEN REPEAT RESA_TAC
2031 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)
2032 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
2033 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
2034 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
2035 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2036 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
2037 THEN SYM_ASSUM_TAC
2038 THEN SCS_TAC;
2039
2040
2041 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4]
2042 THEN ARITH_TAC;
2043
2044
2045 STRIP_TAC
2046 THEN
2047 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4;
2048 ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
2049 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2050 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2051 THEN SCS_TAC
2052 THEN REPEAT GEN_TAC
2053 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
2054 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
2055 THEN RESA_TAC
2056 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
2057 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
2058 THEN RESA_TAC
2059 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2060 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
2061 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
2062 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
2063 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
2064 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
2065 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
2066 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
2067 THEN ASM_TAC
2068 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/\
2069 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2070 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2071 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2072 THEN REPEAT RESA_TAC
2073 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)
2074 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
2075 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
2076 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
2077 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2078 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
2079 THEN SYM_ASSUM_TAC
2080 THEN SCS_TAC;
2081
2082
2083 SCS_TAC
2084 THEN REAL_ARITH_TAC;
2085
2086 SCS_TAC
2087 THEN REAL_ARITH_TAC;
2088
2089 SCS_TAC
2090 THEN REAL_ARITH_TAC;
2091
2092 SCS_TAC
2093 THEN REWRITE_TAC[cstab]
2094 THEN REAL_ARITH_TAC;
2095
2096
2097 SCS_TAC
2098 THEN REWRITE_TAC[cstab]
2099 THEN REAL_ARITH_TAC;
2100
2101
2102
2103 POP_ASSUM MP_TAC
2104 THEN REWRITE_TAC[J_SCS_3T4];
2105
2106 ]);;
2107
2108
2109 let SCS_4M4_SLICE_02=prove_by_refinement(
2110 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M4' 0 2 } { scs_3T3, scs_prop_equ_v39 scs_3M1 1 }`,
2111 [
2112 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
2113 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M4_02;STAB_4M4_SCS;SCS_K_D_A_STAB_EQ;]
2114 THEN EXISTS_TAC`0`
2115 THEN EXISTS_TAC`2`
2116 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M4_02]
2117 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
2118 THEN REPEAT RESA_TAC;
2119
2120
2121 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
2122 THEN STRIP_TAC
2123 THEN MATCH_MP_TAC scs_inj
2124 THEN ASM_SIMP_TAC[SCS_3T3_BASIC;SCS_4M4_BASIC;J_SCS_4M4;BASIC_HALF_SLICE_STAB;J_SCS_3T3;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3M1_BASIC;J_SCS_3M1;J_SCS_3T3_1]
2125 THEN STRIP_TAC;
2126
2127 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T3;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4]
2128 THEN ARITH_TAC;
2129
2130
2131 STRIP_TAC
2132 THEN
2133 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4;
2134 ARITH_RULE`(2 + 1 + 4 - 0) MOD 4= 3/\ 0 MOD 4=0/\ a+0=a`;scs_prop_equ_v39]
2135 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2136 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2137 THEN SCS_TAC
2138 THEN REPEAT GEN_TAC
2139 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
2140 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
2141 THEN RESA_TAC
2142 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
2143 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
2144 THEN RESA_TAC
2145 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2146 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
2147 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
2148 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
2149 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
2150 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
2151 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
2152 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
2153 THEN ASM_TAC
2154 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/\
2155 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2156 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2157 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2158 THEN REPEAT RESA_TAC
2159 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)
2160 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
2161 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
2162 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
2163 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2164 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
2165 THEN SYM_ASSUM_TAC
2166 THEN SCS_TAC;
2167
2168 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4]
2169 THEN ARITH_TAC;
2170
2171 STRIP_TAC
2172 THEN
2173 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4;
2174 ARITH_RULE`(0 + 1 + 4 - 2) MOD 4= 3/\ 2 MOD 4=2/\ a+0=a`;scs_prop_equ_v39]
2175 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2176 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2177 THEN SCS_TAC
2178 THEN REPEAT GEN_TAC
2179 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
2180 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
2181 THEN RESA_TAC
2182 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
2183 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
2184 THEN RESA_TAC
2185 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2186 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
2187 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
2188 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
2189 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
2190 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
2191 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
2192 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
2193 THEN ASM_TAC
2194 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/\
2195 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2196 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2197 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2198 THEN REPEAT RESA_TAC
2199 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)
2200 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
2201 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
2202 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
2203 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2204 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
2205 THEN SYM_ASSUM_TAC
2206 THEN SCS_TAC;
2207
2208 SCS_TAC
2209 THEN REAL_ARITH_TAC;
2210
2211 SCS_TAC
2212 THEN REAL_ARITH_TAC;
2213
2214 SCS_TAC
2215 THEN REAL_ARITH_TAC;
2216
2217 SCS_TAC
2218 THEN REWRITE_TAC[cstab]
2219 THEN REAL_ARITH_TAC;
2220
2221
2222 SCS_TAC
2223 THEN REWRITE_TAC[cstab]
2224 THEN REAL_ARITH_TAC;
2225
2226
2227
2228 POP_ASSUM MP_TAC
2229 THEN REWRITE_TAC[J_SCS_3T3_1];
2230
2231 ]);;
2232
2233
2234
2235 let MFKLVDK =prove_by_refinement(
2236 ` scs_arrow_v39 { scs_4M4' } ({scs_4M7,scs_3T3, scs_3M1, scs_3T4})`,
2237 [
2238 MATCH_MP_TAC FZIOTEF_TRANS
2239 THEN EXISTS_TAC`({scs_4M7} UNION {scs_stab_diag_v39 scs_4M4' i j| scs_diag 4 i j})`
2240 THEN ASM_REWRITE_TAC[SCS_4M4_ARROW_SCS_4M7_STAB_4M4;SET_RULE`{A,B,C,D}={A}UNION{B,C,D}`]
2241 THEN MATCH_MP_TAC FZIOTEF_UNION
2242 THEN STRIP_TAC;
2243
2244 MATCH_MP_TAC FZIOTEF_REFL
2245 THEN REWRITE_TAC[IN_SING]
2246 THEN REPEAT RESA_TAC
2247 THEN ASM_SIMP_TAC[SCS_4M7_IS_SCS];
2248
2249 MATCH_MP_TAC FZIOTEF_TRANS
2250 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M4' 0 2,scs_stab_diag_v39 scs_4M4' 1 3}`
2251 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M4;SET_RULE`{A,B}={A} UNION {B}/\ {A,B,C}={A,B}UNION {C}`]
2252 THEN MATCH_MP_TAC FZIOTEF_UNION
2253 THEN STRIP_TAC;
2254
2255 REWRITE_TAC[SET_RULE`{A}UNION {B}={A,B}`]
2256 THEN MATCH_MP_TAC FZIOTEF_TRANS
2257 THEN EXISTS_TAC`{scs_3T3, scs_prop_equ_v39 scs_3M1 1}`
2258 THEN ASM_SIMP_TAC[SCS_4M4_SLICE_02]
2259 THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION {B}`]
2260 THEN MATCH_MP_TAC FZIOTEF_UNION
2261 THEN STRIP_TAC;
2262
2263 MATCH_MP_TAC FZIOTEF_REFL
2264 THEN REWRITE_TAC[IN_SING]
2265 THEN REPEAT RESA_TAC
2266 THEN ASM_SIMP_TAC[SCS_3T3_IS_SCS];
2267
2268
2269 MRESAS_TAC PRO_EQU_ID1[`scs_3M1`;`1`;`3`][SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`(3 - 1 MOD 3)=2`]
2270 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1 1`;`2`][PROP_EQU_IS_SCS;SCS_3M1_IS_SCS]
2271 THEN DICH_TAC 0
2272 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
2273 THEN REWRITE_TAC[];
2274
2275
2276
2277 MATCH_MP_TAC FZIOTEF_TRANS
2278 THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3T4 2,  scs_3T4 }`
2279 THEN ASM_SIMP_TAC[SCS_4M4_SLICE_13;]
2280 THEN ONCE_REWRITE_TAC[SET_RULE`{A}={A}UNION {A}/\ {A,B}={A} UNION {B}`]
2281 THEN MATCH_MP_TAC FZIOTEF_UNION
2282 THEN STRIP_TAC;
2283
2284
2285 MRESAS_TAC PRO_EQU_ID1[`scs_3T4`;`2`;`3`][SCS_3T4_IS_SCS;K_SCS_3T4;ARITH_RULE`(3 - 2 MOD 3)=1`]
2286 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T4 2`;`1`][PROP_EQU_IS_SCS;SCS_3T4_IS_SCS]
2287 THEN DICH_TAC 0
2288 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
2289 THEN REWRITE_TAC[];
2290
2291
2292 MATCH_MP_TAC FZIOTEF_REFL
2293 THEN REWRITE_TAC[IN_SING]
2294 THEN REPEAT RESA_TAC
2295 THEN ASM_SIMP_TAC[SCS_3T4_IS_SCS]]);;
2296
2297
2298
2299 (************************************)
2300
2301
2302 let BB_4M5_IMP_BB_4M8= prove
2303 (`
2304     BBs_v39 scs_4M5' v /\
2305     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) ==>
2306     BBs_v39 (scs_4M8) v`,
2307 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M5;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M5;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8]
2308 THEN REPEAT RESA_TAC
2309 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2310 THEN SCS_TAC
2311 THEN THAYTHE_TAC 1[`i`;`j`]
2312 THEN DICH_TAC 0
2313 THEN THAYTHE_TAC 2[`i`;`j`]
2314 THEN DICH_TAC 0
2315 THEN DICH_TAC 0
2316 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
2317 THEN SYM_ASSUM_TAC
2318 THEN REWRITE_TAC[ADD1]
2319 THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`]
2320 THEN SYM_ASSUM_TAC
2321 THEN MRESA_TAC MOD_ADD_MOD[`j`;`1`;`4`]
2322 THEN SYM_ASSUM_TAC
2323 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
2324 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2325 THEN RESA_TAC
2326 THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
2327 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2328 THEN RESA_TAC
2329 THEN SCS_TAC
2330 THEN MP_TAC sqrt8_LE_CSTAB
2331 THEN MP_TAC LE_sqrt8_2h0
2332 THEN REWRITE_TAC[cstab;h0]
2333 THEN REAL_ARITH_TAC);;
2334
2335
2336
2337 let MM_4M5_IMP_4M8=prove(
2338 `
2339 MMs_v39 scs_4M5' v /\
2340     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) ==>
2341     ~(MMs_v39 (scs_4M8) ={})`,
2342 STRIP_TAC
2343 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2344 THEN EXISTS_TAC`v:num->real^3`
2345 THEN EXISTS_TAC` scs_4M5' `
2346 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M5' `;`v`]
2347 THEN ASSUME_TAC SCS_4M8_BASIC
2348 THEN ASSUME_TAC K_SCS_4M8
2349 THEN ASM_SIMP_TAC[SCS_4M8_IS_SCS;SCS_4M5_IS_SCS;SCS_4M5_BASIC;K_SCS_4M5;SCS_K_D_A_STAB_EQ;IN; ADD1;BB_4M5_IMP_BB_4M8]
2350 THEN SCS_TAC
2351 THEN REAL_ARITH_TAC);;
2352
2353
2354
2355 let BB_4M5_IMP_BB_STAN_4M5= prove(
2356 `
2357     BBs_v39 scs_4M5' v /\
2358     scs_diag 4 i j /\
2359    dist(v i,v j)<= cstab ==>
2360     BBs_v39 (scs_stab_diag_v39 scs_4M5' i j) v`,
2361 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M5;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M5;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8]
2362 THEN REPEAT RESA_TAC
2363 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2364 THEN SCS_TAC
2365 THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
2366 THEN RESA_TAC
2367 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
2368 THENL[
2369 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M5'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M5;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M5;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8;SCS_4M5_IS_SCS]
2370 THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
2371 THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
2372
2373 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M5'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M5;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M5;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8;SCS_4M5_IS_SCS]
2374 THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
2375 THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
2376 THEN ONCE_REWRITE_TAC[DIST_SYM]
2377 THEN ASM_REWRITE_TAC[]]);;
2378
2379
2380
2381 let MM_4M5_IMP_STAB_4M5=prove(`
2382    MMs_v39 scs_4M5' v /\
2383     scs_diag 4 i j /\
2384    dist(v i,v j)<= cstab ==>
2385     ~(MMs_v39 (scs_stab_diag_v39 scs_4M5' i j) ={})`,
2386 STRIP_TAC
2387 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2388 THEN EXISTS_TAC`v:num->real^3`
2389 THEN EXISTS_TAC` scs_4M5' `
2390 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M5' `;`v`]
2391 THEN ASSUME_TAC SCS_4M5_BASIC
2392 THEN ASSUME_TAC K_SCS_4M5
2393 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M5_IS_SCS;SCS_4M5_BASIC;K_SCS_4M5;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M5_13;BB_4M5_IMP_BB_STAN_4M5;STAB_4M5_SCS]
2394 THEN SCS_TAC
2395 THEN REAL_ARITH_TAC);;
2396
2397
2398
2399 let SCS_4M5_ARROW_SCS_4M8_STAB_4M5=prove_by_refinement(
2400 ` scs_arrow_v39 { scs_4M5' } ({scs_4M8} UNION {scs_stab_diag_v39 scs_4M5' i j| scs_diag 4 i j})`,
2401 [
2402 REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM]
2403 THEN ABBREV_TAC`k=scs_k_v39 s`
2404 THEN REPEAT RESA_TAC;
2405
2406
2407 ASM_SIMP_TAC[SCS_4M8_IS_SCS];
2408
2409
2410 ASM_SIMP_TAC[STAB_4M5_SCS;K_SCS_4M5];
2411
2412
2413 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M5' ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M5' ==> MMs_v39 s = {}))`);
2414
2415
2416 ASM_REWRITE_TAC[];
2417
2418
2419
2420 ASM_REWRITE_TAC[]
2421 THEN POP_ASSUM MP_TAC
2422 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
2423 THEN REPEAT STRIP_TAC
2424 THEN POP_ASSUM MP_TAC
2425 THEN RESA_TAC
2426 THEN POP_ASSUM MP_TAC
2427 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2428 THEN STRIP_TAC;
2429
2430
2431 MP_TAC(SET_RULE`(!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j))\/ ~((!i j. scs_diag 4 i j ==>   cstab < dist((v:num->real^3) i,v j)))`)
2432 THEN RESA_TAC;
2433
2434
2435 EXISTS_TAC`scs_4M8`
2436 THEN ASM_REWRITE_TAC[]
2437 THEN MP_TAC MM_4M5_IMP_4M8
2438 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2439 THEN RESA_TAC
2440 THEN MATCH_DICH_TAC 0
2441 THEN ASM_REWRITE_TAC[]
2442 THEN EXISTS_TAC`v:num->real^3`
2443 THEN ASM_REWRITE_TAC[];
2444
2445
2446 POP_ASSUM MP_TAC
2447 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
2448 THEN STRIP_TAC
2449 THEN MP_TAC MM_4M5_IMP_STAB_4M5
2450 THEN RESA_TAC
2451 THEN DICH_TAC 0
2452 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2453 THEN STRIP_TAC
2454 THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M5' i j`
2455 THEN ASM_REWRITE_TAC[]
2456 THEN STRIP_TAC;
2457
2458 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
2459 THEN EXISTS_TAC`i:num`
2460 THEN EXISTS_TAC`j:num`
2461 THEN ASM_REWRITE_TAC[];
2462
2463
2464 EXISTS_TAC`v':num->real^3`
2465 THEN ASM_REWRITE_TAC[]]);;
2466
2467
2468
2469
2470 let SET_STAB_4M5=prove(`{ scs_stab_diag_v39 scs_4M5' i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M5' (i MOD 4) (j  MOD 4)| scs_diag 4 (i MOD 4) (j  MOD 4) }`,
2471  ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
2472 THEN MRESAL_TAC STAB_MOD[`scs_4M5'`][SCS_4M5_IS_SCS;K_SCS_4M5]);;
2473
2474 let EXPAND_STAB_DIAG_4M5=prove(`
2475 {scs_stab_diag_v39 scs_4M5' (i MOD 4) (j MOD 4) | j MOD 4 =
2476                                                   (i MOD 4 + 2) MOD 4}=
2477 {scs_stab_diag_v39 scs_4M5' (i+2) i| i<4} `,
2478 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M5_IS_SCS;K_SCS_4M5]);;
2479
2480
2481 let SET_EQ_DIAG_STAB_4M5=prove_by_refinement(
2482 `scs_arrow_v39
2483  { scs_stab_diag_v39 scs_4M5' i j| scs_diag 4 i j }
2484  {scs_stab_diag_v39 scs_4M5' 0 2,scs_stab_diag_v39 scs_4M5' 1 3}`,
2485 [
2486 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M5;SET_STAB_4M5;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
2487 THEN
2488 REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M5' (i + 2) i |i=0\/i=1\/i=2\/i=3}
2489 = {scs_stab_diag_v39 scs_4M5' (0 + 2) 0} UNION
2490 {scs_stab_diag_v39 scs_4M5' (1 + 2) 1} UNION
2491 {scs_stab_diag_v39 scs_4M5' (2 + 2) 2} UNION
2492 {scs_stab_diag_v39 scs_4M5' (3 + 2) 3}
2493 `;]
2494 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M5' 0 2,scs_stab_diag_v39 scs_4M5' 1 3}={scs_stab_diag_v39 scs_4M5' 0 2} UNION {scs_stab_diag_v39 scs_4M5' 1 3}UNION {scs_stab_diag_v39 scs_4M5' 0 2} UNION {scs_stab_diag_v39 scs_4M5' 1 3}`]
2495 THEN MATCH_MP_TAC FZIOTEF_UNION
2496 THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
2497 THEN MRESA_TAC STAB_SYM[`scs_4M5'`;`0`;`2`]
2498 THEN STRIP_TAC;
2499
2500 MATCH_MP_TAC FZIOTEF_REFL
2501 THEN REWRITE_TAC[IN_SING]
2502 THEN REPEAT RESA_TAC
2503 THEN ASM_SIMP_TAC[STAB_4M5_SCS;SCS_DIAG_SCS_4M5_02];
2504
2505 MATCH_MP_TAC FZIOTEF_UNION
2506 THEN MRESA_TAC STAB_SYM[`scs_4M5'`;`1`;`3`]
2507 THEN STRIP_TAC;
2508
2509
2510 MATCH_MP_TAC FZIOTEF_REFL
2511 THEN REWRITE_TAC[IN_SING]
2512 THEN REPEAT RESA_TAC
2513 THEN ASM_SIMP_TAC[STAB_4M5_SCS;SCS_DIAG_SCS_4M5_13];
2514
2515 MATCH_MP_TAC FZIOTEF_UNION
2516 THEN MRESAL_TAC STAB_MOD[`scs_4M5'`;`4`;`2`][SCS_4M5_IS_SCS;K_SCS_4M5;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
2517 THEN SYM_ASSUM_TAC
2518 THEN STRIP_TAC;
2519
2520 MATCH_MP_TAC FZIOTEF_REFL
2521 THEN REWRITE_TAC[IN_SING]
2522 THEN REPEAT RESA_TAC
2523 THEN ASM_SIMP_TAC[STAB_4M5_SCS;SCS_DIAG_SCS_4M5_02];
2524
2525 MRESAL_TAC STAB_MOD[`scs_4M5'`;`5`;`3`][SCS_4M5_IS_SCS;K_SCS_4M5;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
2526 THEN SYM_ASSUM_TAC;
2527
2528 MATCH_MP_TAC FZIOTEF_REFL
2529 THEN REWRITE_TAC[IN_SING]
2530 THEN REPEAT RESA_TAC
2531 THEN ASM_SIMP_TAC[STAB_4M5_SCS;SCS_DIAG_SCS_4M5_13]]);;
2532
2533
2534
2535 let PROP_OPP_DIAG_4M5_13= prove_by_refinement(`scs_stab_diag_v39 scs_4M5' 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4M5' 0 2)) 2 `,
2536 [REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;SCS_K_D_A_STAB_EQ;scs_opp_v39]
2537 THEN MATCH_MP_TAC scs_inj
2538 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M5_BASIC;STAB_4M5_SCS;SCS_DIAG_SCS_4M5_13;scs_basic;unadorned_v39;peropp;peropp2]
2539 THEN SCS_TAC
2540 THEN STRIP_TAC;
2541
2542 SET_TAC[];
2543
2544
2545 STRIP_TAC
2546 THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;]
2547 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
2548 THEN REPEAT GEN_TAC
2549 THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
2550 THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
2551 THEN SYM_ASSUM_TAC
2552 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
2553 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
2554 THEN SYM_ASSUM_TAC
2555 THEN SYM_ASSUM_TAC
2556 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`)
2557 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2558 THEN RESA_TAC
2559 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`)
2560 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
2561 THEN RESA_TAC
2562 THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_4_TAC;PSORT_5_EXPLICIT;ARITH_RULE`4-1=3/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6
2563 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;
2564
2565
2566
2567 let STAB_4M5_02_ARROW_4M5_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M5' 0 2}{scs_stab_diag_v39 scs_4M5' 1 3}`,
2568 ASM_SIMP_TAC[PROP_OPP_DIAG_4M5_13]
2569 THEN MATCH_MP_TAC FZIOTEF_TRANS
2570 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4M5' 0 2)}`
2571 THEN STRIP_TAC
2572 THENL[
2573 MATCH_MP_TAC (GEN_ALL YXIONXL2)
2574 THEN EXISTS_TAC`4`
2575 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M5;STAB_4M5_SCS;SCS_DIAG_SCS_4M5_02]
2576 ;
2577
2578 MATCH_MP_TAC(GEN_ALL YXIONXL3)
2579 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
2580 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4M5' 0 2)`
2581 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M5;STAB_4M5_SCS;SCS_DIAG_SCS_4M5_02]]);;
2582
2583
2584 let SCS_4M5_SLICE_13=prove_by_refinement(
2585 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M5' 1 3 } {scs_3T4}`,
2586 [
2587 ONCE_REWRITE_TAC[SET_RULE`{scs_3T4}={scs_3T4,scs_3T4}`]
2588 THEN MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
2589 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M5_13;STAB_4M5_SCS;SCS_K_D_A_STAB_EQ;]
2590 THEN EXISTS_TAC`1`
2591 THEN EXISTS_TAC`3`
2592 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M5_13]
2593 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
2594 THEN REPEAT RESA_TAC;
2595
2596 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
2597 THEN STRIP_TAC
2598 THEN MATCH_MP_TAC scs_inj
2599 THEN ASM_SIMP_TAC[SCS_3T4_BASIC;SCS_4M5_BASIC;J_SCS_4M5;BASIC_HALF_SLICE_STAB;J_SCS_3T4_1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T6_BASIC;J_SCS_3T6]
2600 THEN STRIP_TAC;
2601
2602 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M5]
2603 THEN ARITH_TAC;
2604
2605 STRIP_TAC
2606 THEN
2607 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M5;
2608 ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
2609 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2610 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2611 THEN SCS_TAC
2612 THEN REPEAT GEN_TAC
2613 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
2614 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
2615 THEN RESA_TAC
2616 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
2617 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
2618 THEN RESA_TAC
2619 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2620 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
2621 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
2622 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
2623 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
2624 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
2625 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
2626 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
2627 THEN ASM_TAC
2628 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/\
2629 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2630 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2631 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2632 THEN REPEAT RESA_TAC
2633 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)
2634 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
2635 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
2636 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
2637 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2638 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
2639 THEN SYM_ASSUM_TAC
2640 THEN SCS_TAC;
2641
2642 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M5]
2643 THEN ARITH_TAC;
2644
2645 STRIP_TAC
2646 THEN
2647 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T6;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M5;
2648 ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
2649 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2650 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2651 THEN SCS_TAC
2652 THEN REPEAT GEN_TAC
2653 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
2654 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
2655 THEN RESA_TAC
2656 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
2657 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
2658 THEN RESA_TAC
2659 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2660 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
2661 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
2662 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
2663 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
2664 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
2665 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
2666 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
2667 THEN ASM_TAC
2668 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/\
2669 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2670 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2671 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2672 THEN REPEAT RESA_TAC
2673 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)
2674 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
2675 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
2676 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
2677 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2678 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
2679 THEN SYM_ASSUM_TAC
2680 THEN SCS_TAC;
2681
2682 SCS_TAC
2683 THEN REAL_ARITH_TAC;
2684
2685 SCS_TAC
2686 THEN REAL_ARITH_TAC;
2687
2688 SCS_TAC
2689 THEN REAL_ARITH_TAC;
2690
2691 SCS_TAC
2692 THEN REWRITE_TAC[cstab]
2693 THEN REAL_ARITH_TAC;
2694
2695
2696 SCS_TAC
2697 THEN REWRITE_TAC[cstab]
2698 THEN REAL_ARITH_TAC;
2699
2700
2701
2702 POP_ASSUM MP_TAC
2703 THEN REWRITE_TAC[J_SCS_3T4_1];
2704
2705 ]);;
2706
2707
2708 let RYPDIXT =prove_by_refinement(
2709 ` scs_arrow_v39 { scs_4M5' } ({scs_4M8,scs_3T4})`,
2710 [
2711 MATCH_MP_TAC FZIOTEF_TRANS
2712 THEN EXISTS_TAC`({scs_4M8} UNION {scs_stab_diag_v39 scs_4M5' i j| scs_diag 4 i j})`
2713 THEN ASM_REWRITE_TAC[SCS_4M5_ARROW_SCS_4M8_STAB_4M5;SET_RULE`{A,B}={A}UNION{B}`]
2714 THEN MATCH_MP_TAC FZIOTEF_UNION
2715 THEN STRIP_TAC;
2716
2717 MATCH_MP_TAC FZIOTEF_REFL
2718 THEN REWRITE_TAC[IN_SING]
2719 THEN REPEAT RESA_TAC
2720 THEN ASM_SIMP_TAC[SCS_4M8_IS_SCS];
2721
2722 MATCH_MP_TAC FZIOTEF_TRANS
2723 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M5' 0 2,scs_stab_diag_v39 scs_4M5' 1 3}`
2724 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M5]
2725 THEN MATCH_MP_TAC FZIOTEF_TRANS
2726 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M5' 1 3,scs_stab_diag_v39 scs_4M5' 1 3}`
2727 THEN STRIP_TAC;
2728
2729 REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`]
2730 THEN MATCH_MP_TAC FZIOTEF_UNION
2731 THEN ASM_REWRITE_TAC[STAB_4M5_02_ARROW_4M5_13];
2732
2733 MATCH_MP_TAC FZIOTEF_REFL
2734 THEN REWRITE_TAC[IN_SING]
2735 THEN REPEAT RESA_TAC
2736 THEN ASM_SIMP_TAC[STAB_4M5_SCS;SCS_DIAG_SCS_4M5_13];
2737
2738 REWRITE_TAC[SET_RULE`{A,A}={A}`;SCS_4M5_SLICE_13];
2739
2740 ]);;
2741
2742
2743 (******** NWDGKXH CASES EQ cstab*******************)
2744
2745
2746 let BB_4M6_IMP_4T5=prove(`!v.
2747     BBs_v39 (scs_stab_diag_v39 scs_4M6' 1 3) v
2748      ==>
2749     BBs_v39 (scs_4T5) v`,
2750 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M6;scs_4T5;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;]
2751 THEN REPEAT RESA_TAC
2752 THEN THAYTHE_TAC 1[`i`;`j`]
2753 THEN DICH_TAC 0
2754 THEN MP_TAC(SET_RULE`psort 4 (i,j) = 1,3\/ ~(psort 4 (i,j) = 1,3)`)
2755 THEN RESA_TAC
2756 THEN MRESAL_TAC Uaghhbm.CASE_PSORT[`i`;`3`;`j`;`1`;`4`][PSORT_5_EXPLICIT;Uxckfpe.ARITH_4_TAC;PAIR_EQ;cstab]
2757 THEN DICH_TAC 0
2758 THEN SCS_TAC
2759 THEN RESA_TAC
2760 THEN SCS_TAC);;
2761
2762
2763 let MM_4M6_IMP_4T5=prove(
2764 `MMs_v39 (scs_stab_diag_v39 scs_4M6' 1 3) v
2765      ==>
2766     ~(MMs_v39 (scs_4T5) ={})`,
2767 STRIP_TAC
2768 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2769 THEN EXISTS_TAC`v:num->real^3`
2770 THEN EXISTS_TAC`(scs_stab_diag_v39 scs_4M6' 1 3)`
2771 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`(scs_stab_diag_v39 scs_4M6' 1 3)`;`v`]
2772 THEN ASSUME_TAC SCS_4T5_BASIC
2773 THEN ASSUME_TAC K_SCS_4T5
2774 THEN ASM_SIMP_TAC[SCS_4T5_IS_SCS;STAB_4M6_SCS;K_SCS_4M6;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M6_13;BB_4M6_IMP_4T5]
2775 THEN SCS_TAC
2776 THEN REAL_ARITH_TAC);;
2777
2778
2779 let STAB_4M6_13_ARROW_4T5=prove_by_refinement(
2780 ` scs_arrow_v39 { scs_stab_diag_v39 scs_4M6' 1 3 } {scs_4T5}`,
2781 [
2782 REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM]
2783 THEN ABBREV_TAC`k=scs_k_v39 s`
2784 THEN REPEAT RESA_TAC;
2785
2786 ASM_SIMP_TAC[SCS_4T5_IS_SCS];
2787
2788 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_stab_diag_v39 scs_4M6' 1 3 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_stab_diag_v39 scs_4M6' 1 3 ==> MMs_v39 s = {}))`);
2789
2790 ASM_REWRITE_TAC[];
2791
2792 ASM_REWRITE_TAC[]
2793 THEN POP_ASSUM MP_TAC
2794 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
2795 THEN REPEAT STRIP_TAC
2796 THEN POP_ASSUM MP_TAC
2797 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2798 THEN RESA_TAC
2799 THEN POP_ASSUM MP_TAC
2800 THEN STRIP_TAC
2801 THEN EXISTS_TAC`scs_4T5`
2802 THEN ASM_REWRITE_TAC[]
2803 THEN MP_TAC MM_4M6_IMP_4T5
2804 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2805 THEN RESA_TAC]);;
2806
2807
2808 let PROP_OPP_DIAG_4M6_13= prove_by_refinement(`scs_stab_diag_v39 scs_4M6' 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4M6' 0 2)) 2 `,
2809 [REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;SCS_K_D_A_STAB_EQ;scs_opp_v39]
2810 THEN MATCH_MP_TAC scs_inj
2811 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M6_BASIC;STAB_4M6_SCS;SCS_DIAG_SCS_4M6_13;scs_basic;unadorned_v39;peropp;peropp2]
2812 THEN SCS_TAC
2813 THEN STRIP_TAC;
2814
2815
2816 SET_TAC[];
2817
2818 STRIP_TAC
2819 THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;]
2820 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
2821 THEN REPEAT GEN_TAC
2822 THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
2823 THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
2824 THEN SYM_ASSUM_TAC
2825 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
2826 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
2827 THEN SYM_ASSUM_TAC
2828 THEN SYM_ASSUM_TAC
2829 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`)
2830 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2831 THEN RESA_TAC
2832 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`)
2833 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
2834 THEN RESA_TAC
2835 THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_4_TAC;PSORT_5_EXPLICIT;ARITH_RULE`4-1=3/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6
2836 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;
2837
2838
2839
2840
2841
2842 let STAB_4M6_02_ARROW_4M6_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M6' 0 2}{scs_stab_diag_v39 scs_4M6' 1 3}`,
2843 ASM_SIMP_TAC[PROP_OPP_DIAG_4M6_13]
2844 THEN MATCH_MP_TAC FZIOTEF_TRANS
2845 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4M6' 0 2)}`
2846 THEN STRIP_TAC
2847 THENL[
2848 MATCH_MP_TAC (GEN_ALL YXIONXL2)
2849 THEN EXISTS_TAC`4`
2850 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M6;STAB_4M6_SCS;SCS_DIAG_SCS_4M6_02]
2851 ;
2852
2853 MATCH_MP_TAC(GEN_ALL YXIONXL3)
2854 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
2855 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4M6' 0 2)`
2856 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M6;STAB_4M6_SCS;SCS_DIAG_SCS_4M6_02]]);;
2857
2858
2859 let STAB_4M6_02_ARROW_4T5 =prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_4M6' 0 2 } { scs_4T5 }`,
2860 MATCH_MP_TAC FZIOTEF_TRANS
2861 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M6' 1 3}`
2862 THEN ASM_SIMP_TAC[STAB_4M6_02_ARROW_4M6_13;STAB_4M6_13_ARROW_4T5]);;
2863
2864
2865 let SET_STAB_4M6=prove(`{ scs_stab_diag_v39 scs_4M6' i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M6' (i MOD 4) (j  MOD 4)| scs_diag 4 (i MOD 4) (j  MOD 4) }`,
2866  ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
2867 THEN MRESAL_TAC STAB_MOD[`scs_4M6'`][SCS_4M6_IS_SCS;K_SCS_4M6]);;
2868
2869 let EXPAND_STAB_DIAG_4M6=prove(`
2870 {scs_stab_diag_v39 scs_4M6' (i MOD 4) (j MOD 4) | j MOD 4 =
2871                                                   (i MOD 4 + 2) MOD 4}=
2872 {scs_stab_diag_v39 scs_4M6' (i+2) i| i<4} `,
2873 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M6_IS_SCS;K_SCS_4M6]);;
2874
2875
2876 let SET_EQ_DIAG_STAB_4M6=prove_by_refinement(`scs_arrow_v39
2877  { scs_stab_diag_v39 scs_4M6' i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4M6' 0 2,scs_stab_diag_v39 scs_4M6' 1 3}`,
2878 [
2879 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M6;SET_STAB_4M6;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
2880 THEN
2881 REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M6' (i + 2) i |i=0\/i=1\/i=2\/i=3}
2882 = {scs_stab_diag_v39 scs_4M6' (0 + 2) 0} UNION
2883 {scs_stab_diag_v39 scs_4M6' (1 + 2) 1} UNION
2884 {scs_stab_diag_v39 scs_4M6' (2 + 2) 2} UNION
2885 {scs_stab_diag_v39 scs_4M6' (3 + 2) 3}
2886 `;]
2887 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M6' 0 2,scs_stab_diag_v39 scs_4M6' 1 3}={scs_stab_diag_v39 scs_4M6' 0 2} UNION {scs_stab_diag_v39 scs_4M6' 1 3}UNION {scs_stab_diag_v39 scs_4M6' 0 2} UNION {scs_stab_diag_v39 scs_4M6' 1 3}`]
2888 THEN MATCH_MP_TAC FZIOTEF_UNION
2889 THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
2890 THEN MRESA_TAC STAB_SYM[`scs_4M6'`;`0`;`2`]
2891 THEN STRIP_TAC;
2892
2893 MATCH_MP_TAC FZIOTEF_REFL
2894 THEN REWRITE_TAC[IN_SING]
2895 THEN REPEAT RESA_TAC
2896 THEN ASM_SIMP_TAC[STAB_4M6_SCS;SCS_DIAG_SCS_4M6_02];
2897
2898 MATCH_MP_TAC FZIOTEF_UNION
2899 THEN MRESA_TAC STAB_SYM[`scs_4M6'`;`1`;`3`]
2900 THEN STRIP_TAC;
2901
2902 MATCH_MP_TAC FZIOTEF_REFL
2903 THEN REWRITE_TAC[IN_SING]
2904 THEN REPEAT RESA_TAC
2905 THEN ASM_SIMP_TAC[STAB_4M6_SCS;SCS_DIAG_SCS_4M6_13];
2906
2907 MATCH_MP_TAC FZIOTEF_UNION
2908 THEN MRESAL_TAC STAB_MOD[`scs_4M6'`;`4`;`2`][SCS_4M6_IS_SCS;K_SCS_4M6;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
2909 THEN SYM_ASSUM_TAC
2910 THEN STRIP_TAC;
2911
2912 MATCH_MP_TAC FZIOTEF_REFL
2913 THEN REWRITE_TAC[IN_SING]
2914 THEN REPEAT RESA_TAC
2915 THEN ASM_SIMP_TAC[STAB_4M6_SCS;SCS_DIAG_SCS_4M6_02];
2916
2917 MRESAL_TAC STAB_MOD[`scs_4M6'`;`5`;`3`][SCS_4M6_IS_SCS;K_SCS_4M6;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
2918 THEN SYM_ASSUM_TAC;
2919
2920 MATCH_MP_TAC FZIOTEF_REFL
2921 THEN REWRITE_TAC[IN_SING]
2922 THEN REPEAT RESA_TAC
2923 THEN ASM_SIMP_TAC[STAB_4M6_SCS;SCS_DIAG_SCS_4M6_13]]);;
2924
2925
2926
2927
2928 let SET_STAB_4M6_ARROW_4T5=prove(`scs_arrow_v39
2929  { scs_stab_diag_v39 scs_4M6' i j| scs_diag 4 i j } {scs_4T5}`,
2930 ONCE_REWRITE_TAC[SET_RULE`{A}={A,A}`]
2931 THEN MATCH_MP_TAC FZIOTEF_TRANS
2932 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M6' 0 2,scs_stab_diag_v39 scs_4M6' 1 3}`
2933 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M6;]
2934 THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`;]
2935 THEN MATCH_MP_TAC FZIOTEF_UNION
2936 THEN ASM_SIMP_TAC[STAB_4M6_02_ARROW_4T5;STAB_4M6_13_ARROW_4T5]);;
2937
2938
2939
2940 let BB_4M6_IMP_BB_STAN_4M6= prove(`
2941     BBs_v39 scs_4M6' v /\
2942     scs_diag 4 i j /\
2943    dist(v i,v j)<= cstab ==>
2944     BBs_v39 (scs_stab_diag_v39 scs_4M6' i j) v`,
2945 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M6;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
2946 THEN REPEAT RESA_TAC
2947 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2948 THEN SCS_TAC
2949 THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
2950 THEN RESA_TAC
2951 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
2952 THENL[
2953 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M6'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M6;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M6_IS_SCS]
2954 THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
2955 THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
2956
2957 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M6'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M6;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M6_IS_SCS]
2958 THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
2959 THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
2960 THEN ONCE_REWRITE_TAC[DIST_SYM]
2961 THEN ASM_REWRITE_TAC[]]);;
2962
2963
2964 let MM_4M6_IMP_STAB_4M6=prove(`
2965    MMs_v39 scs_4M6' v /\
2966     scs_diag 4 i j /\
2967    dist(v i,v j)<= cstab ==>
2968     ~(MMs_v39 (scs_stab_diag_v39 scs_4M6' i j) ={})`,
2969 STRIP_TAC
2970 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2971 THEN EXISTS_TAC`v:num->real^3`
2972 THEN EXISTS_TAC` scs_4M6' `
2973 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M6' `;`v`]
2974 THEN ASSUME_TAC SCS_4M6_BASIC
2975 THEN ASSUME_TAC K_SCS_4M6
2976 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M6_13;BB_4M6_IMP_BB_STAN_4M6;STAB_4M6_SCS]
2977 THEN SCS_TAC
2978 THEN REAL_ARITH_TAC);;
2979
2980
2981
2982
2983
2984  end;;
2985
2986
2987 (*
2988 let check_completeness_claimA_concl =
2989   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
2990 *)
2991
2992
2993
2994