text_formalization/local/OTMTOTJ.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 Otmtotj = struct
  16
  17
  18 open Polyhedron;;
  19 open Sphere;;
  20 open Topology;;
  21 open Fan_misc;;
  22 open Planarity;;
  23 open Conforming;;
  24 open Hypermap;;
  25 open Fan;;
  26 open Topology;;
  27 open Wrgcvdr_cizmrrh;;
  28 open Local_lemmas;;
  29 open Collect_geom;;
  30 open Dih2k_hypermap;;
  31 open Wjscpro;;
  32 open Tecoxbm;;
  33 open Hdplygy;;
  34 open Nkezbfc_local;;
  35 open Flyspeck_constants;;
  36 open Gbycpxs;;
  37 open Pcrttid;;
  38 open Local_lemmas1;;
  39 open Pack_defs;;
  40
  41 open Hales_tactic;;
  42
  43 open Appendix;;
  44
  45
  46
  47
  48
  49 open Hypermap;;
  50 open Fan;;
  51 open Wrgcvdr_cizmrrh;;
  52 open Local_lemmas;;
  53 open Flyspeck_constants;;
  54 open Pack_defs;;
  55
  56 open Hales_tactic;;
  57
  58 open Appendix;;
  59
  60
  61 open Zithlqn;;
  62
  63
  64 open Xwitccn;;
  65
  66 open Ayqjtmd;;
  67
  68 open Jkqewgv;;
  69
  70
  71 open Mtuwlun;;
  72
  73
  74 open Uxckfpe;;
  75 open Sgtrnaf;;
  76
  77 open Yxionxl;;
  78
  79 open Qknvmlb;;
  80 open Odxlstcv2;;
  81
  82 open Yxionxl2;;
  83 open Eyypqdw;;
  84 open Ocbicby;;
  85 open Imjxphr;;
  86
  87 open Nuxcoea;;
  88 open Fektyiy;;
  89 open Hexagons;;
  90
  91
  92 let SCSE_TAC= ASM_REWRITE_TAC[scs_basic;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} j <=> {} i`;periodic2;scs_basic;unadorned_v39;scs_prop_equ_v39;LET_DEF;LET_END_DEF;scs_stab_diag_v39;scs_half_slice_v39;
  93 Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_5_TAC;
  94 scs_5M1;scs_3M1;scs_6I1;scs_3T1;scs_4M2;scs_6M1;scs_6T1;scs_5I1;scs_5I2;scs_5I3;scs_5M2;
  95 Terminal.FUNLIST_EXPLICIT;Yrtafyh.PSORT_PERIODIC;PSORT_5_EXPLICIT;
  96 ARITH_RULE`SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6/\ SUC 6=7/\ SUC 7=8`];;
  97
  98
  99
 100 let DIAG_5_EQU_PSORT=prove(`~(i MOD 5 = j MOD 5) /\
 101           ~(SUC i MOD 5 = j MOD 5) /\
 102           ~(i MOD 5 = SUC j MOD 5)
 103 <=> psort 5 (i,j) = 0,2\/ psort 5 (i,j) = 0,3\/ psort 5 (i,j) = 1,3
 104 \/ psort 5 (i,j) = 1,4\/ psort 5 (i,j) = 2,4`,
 105 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
 106 THEN SYM_ASSUM_TAC
 107 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
 108 THEN SYM_ASSUM_TAC
 109 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
 110 THEN SYM_ASSUM_TAC
 111 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
 112 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 113 THEN RESA_TAC
 114 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
 115 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 116 THEN RESA_TAC
 117 THEN SCS_TAC
 118 THEN REWRITE_TAC[PSORT_5_EXPLICIT;PAIR_EQ]
 119 THEN ARITH_TAC);;
 120
 121
 122
 123 let BB_5I1_IS_BB_5M2=prove_by_refinement(`BBs_v39 scs_5I1 v/\ (!i j. scs_diag 5 i j ==>   cstab <= dist(v i,v j)) ==> BBs_v39 scs_5M2 v`,
 124 [
 125 REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I1;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`]
 126 THEN REPEAT RESA_TAC
 127 THEN SCS_TAC
 128 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 129 THEN RESA_TAC;
 130
 131 THAYTHE_TAC (5-2)[`i`;`j`];
 132
 133 MP_TAC(SET_RULE`SUC i MOD 5= j MOD 5\/ ~(SUC i MOD 5= j MOD 5)`)
 134 THEN RESA_TAC;
 135
 136 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
 137 THEN THAYTHE_TAC (7-2)[`i`;`j`]
 138 THEN DICH_TAC 2
 139 THEN DICH_TAC 2
 140 THEN STRIP_TAC
 141 THEN STRIP_TAC
 142 THEN SYM_ASSUM_TAC
 143 THEN SYM_ASSUM_TAC
 144 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
 145 THEN SYM_ASSUM_TAC
 146 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
 147 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 148 THEN RESA_TAC
 149 THEN SCS_TAC;
 150
 151
 152 MP_TAC(SET_RULE`i MOD 5= SUC j MOD 5\/ ~(i MOD 5= SUC j MOD 5)`)
 153 THEN RESA_TAC;
 154
 155 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
 156 THEN THAYTHE_TAC (8-2)[`i`;`j`]
 157 THEN DICH_TAC 2
 158 THEN STRIP_TAC
 159 THEN SYM_ASSUM_TAC
 160 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
 161 THEN SYM_ASSUM_TAC
 162 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
 163 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 164 THEN RESA_TAC
 165 THEN SCS_TAC;
 166
 167 MP_TAC DIAG_5_EQU_PSORT
 168 THEN RESA_TAC
 169 THEN REWRITE_TAC[PAIR_EQ]
 170 THEN SCS_TAC;
 171
 172
 173 THAYTHE_TAC (5-2)[`i`;`j`];
 174
 175 MP_TAC(SET_RULE`SUC i MOD 5= j MOD 5\/ ~(SUC i MOD 5= j MOD 5)`)
 176 THEN RESA_TAC;
 177
 178 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
 179 THEN THAYTHE_TAC (7-2)[`i`;`j`]
 180 THEN DICH_TAC 2
 181 THEN DICH_TAC 2
 182 THEN STRIP_TAC
 183 THEN STRIP_TAC
 184 THEN SYM_ASSUM_TAC
 185 THEN SYM_ASSUM_TAC
 186 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
 187 THEN SYM_ASSUM_TAC
 188 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
 189 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 190 THEN RESA_TAC
 191 THEN SCS_TAC
 192 THEN DICH_TAC 1
 193 THEN REWRITE_TAC[h0;cstab]
 194 THEN REAL_ARITH_TAC;
 195
 196 MP_TAC(SET_RULE`i MOD 5= SUC j MOD 5\/ ~(i MOD 5= SUC j MOD 5)`)
 197 THEN RESA_TAC;
 198
 199 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
 200 THEN THAYTHE_TAC (8-2)[`i`;`j`]
 201 THEN DICH_TAC 2
 202 THEN STRIP_TAC
 203 THEN SYM_ASSUM_TAC
 204 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
 205 THEN SYM_ASSUM_TAC
 206 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
 207 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 208 THEN RESA_TAC
 209 THEN SCS_TAC
 210 THEN DICH_TAC 1
 211 THEN REWRITE_TAC[h0;cstab]
 212 THEN REAL_ARITH_TAC;
 213
 214 MP_TAC DIAG_5_EQU_PSORT
 215 THEN RESA_TAC
 216 THEN REWRITE_TAC[PAIR_EQ]
 217 THEN SCS_TAC
 218 THEN THAYTHE_TAC(8-2)[`i`;`j`]]);;
 219
 220
 221 let MM_5I1_IMP_MM_5M2=prove(`MMs_v39 scs_5I1 v/\ (!i j. scs_diag 5 i j ==>   cstab <= dist(v i,v j)) ==> ~(MMs_v39 scs_5M2 ={})`,
 222 STRIP_TAC
 223 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
 224 THEN EXISTS_TAC`v:num->real^3`
 225 THEN EXISTS_TAC`scs_5I1`
 226 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I1`;`v`]
 227 THEN ASSUME_TAC SCS_5I1_BASIC
 228 THEN ASSUME_TAC K_SCS_5I1
 229 THEN ASSUME_TAC SCS_5M2_BASIC
 230 THEN ASSUME_TAC K_SCS_5M2
 231 THEN ASSUME_TAC SCS_5M2_IS_SCS
 232 THEN ASM_SIMP_TAC[BB_5I1_IS_BB_5M2;IN;SCS_5I1_IS_SCS]
 233 THEN SCS_TAC
 234 THEN REAL_ARITH_TAC);;
 235
 236
 237 let BB_5I2_IS_BB_5M2=prove_by_refinement(`BBs_v39 scs_5I2 v/\ (!i j. scs_diag 5 i j ==>   cstab <= dist(v i,v j)) ==> BBs_v39 scs_5M2 v`,
 238 [
 239 REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I2;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`]
 240 THEN REPEAT RESA_TAC
 241 THEN SCS_TAC
 242 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 243 THEN RESA_TAC;
 244
 245 THAYTHE_TAC (5-2)[`i`;`j`];
 246
 247 MP_TAC(SET_RULE`SUC i MOD 5= j MOD 5\/ ~(SUC i MOD 5= j MOD 5)`)
 248 THEN RESA_TAC;
 249
 250 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
 251 THEN THAYTHE_TAC (7-2)[`i`;`j`]
 252 THEN DICH_TAC 2
 253 THEN DICH_TAC 2
 254 THEN STRIP_TAC
 255 THEN STRIP_TAC
 256 THEN SYM_ASSUM_TAC
 257 THEN SYM_ASSUM_TAC
 258 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
 259 THEN SYM_ASSUM_TAC
 260 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
 261 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 262 THEN RESA_TAC
 263 THEN SCS_TAC;
 264
 265
 266 MP_TAC(SET_RULE`i MOD 5= SUC j MOD 5\/ ~(i MOD 5= SUC j MOD 5)`)
 267 THEN RESA_TAC;
 268
 269 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
 270 THEN THAYTHE_TAC (8-2)[`i`;`j`]
 271 THEN DICH_TAC 2
 272 THEN STRIP_TAC
 273 THEN SYM_ASSUM_TAC
 274 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
 275 THEN SYM_ASSUM_TAC
 276 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
 277 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 278 THEN RESA_TAC
 279 THEN SCS_TAC;
 280
 281 MP_TAC DIAG_5_EQU_PSORT
 282 THEN RESA_TAC
 283 THEN REWRITE_TAC[PAIR_EQ]
 284 THEN SCS_TAC;
 285
 286
 287 THAYTHE_TAC (5-2)[`i`;`j`];
 288
 289 MP_TAC(SET_RULE`SUC i MOD 5= j MOD 5\/ ~(SUC i MOD 5= j MOD 5)`)
 290 THEN RESA_TAC;
 291
 292 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
 293 THEN THAYTHE_TAC (7-2)[`i`;`j`]
 294 THEN DICH_TAC 2
 295 THEN DICH_TAC 2
 296 THEN STRIP_TAC
 297 THEN STRIP_TAC
 298 THEN SYM_ASSUM_TAC
 299 THEN SYM_ASSUM_TAC
 300 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
 301 THEN SYM_ASSUM_TAC
 302 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
 303 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 304 THEN RESA_TAC
 305 THEN SCS_TAC
 306 THEN DICH_TAC 1
 307 THEN REWRITE_TAC[h0;cstab]
 308 THEN REAL_ARITH_TAC;
 309
 310 MP_TAC(SET_RULE`i MOD 5= SUC j MOD 5\/ ~(i MOD 5= SUC j MOD 5)`)
 311 THEN RESA_TAC;
 312
 313 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
 314 THEN THAYTHE_TAC (8-2)[`i`;`j`]
 315 THEN DICH_TAC 2
 316 THEN STRIP_TAC
 317 THEN SYM_ASSUM_TAC
 318 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
 319 THEN SYM_ASSUM_TAC
 320 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
 321 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 322 THEN RESA_TAC
 323 THEN SCS_TAC
 324 THEN DICH_TAC 1
 325 THEN REWRITE_TAC[h0;cstab]
 326 THEN REAL_ARITH_TAC;
 327
 328 MP_TAC DIAG_5_EQU_PSORT
 329 THEN RESA_TAC
 330 THEN REWRITE_TAC[PAIR_EQ]
 331 THEN SCS_TAC
 332 THEN THAYTHE_TAC(8-2)[`i`;`j`]]);;
 333
 334
 335 let MM_5I2_IMP_MM_5M2=prove(`MMs_v39 scs_5I2 v/\ (!i j. scs_diag 5 i j ==>   cstab <= dist(v i,v j)) ==> ~(MMs_v39 scs_5M2 ={})`,
 336 STRIP_TAC
 337 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
 338 THEN EXISTS_TAC`v:num->real^3`
 339 THEN EXISTS_TAC`scs_5I2`
 340 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I2`;`v`]
 341 THEN ASSUME_TAC SCS_5I2_BASIC
 342 THEN ASSUME_TAC K_SCS_5I2
 343 THEN ASSUME_TAC SCS_5M2_BASIC
 344 THEN ASSUME_TAC K_SCS_5M2
 345 THEN ASSUME_TAC SCS_5M2_IS_SCS
 346 THEN ASM_SIMP_TAC[BB_5I2_IS_BB_5M2;IN;SCS_5I2_IS_SCS]
 347 THEN SCS_TAC
 348 THEN REAL_ARITH_TAC);;
 349
 350
 351
 352 let BB_5I3_IS_BB_5M2=prove_by_refinement(`BBs_v39 scs_5I3 v/\ (!i j. scs_diag 5 i j ==>   cstab <= dist(v i,v j)) ==> BBs_v39 scs_5M2 v`,
 353 [
 354 REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`]
 355 THEN SCS_TAC
 356 THEN REPEAT RESA_TAC
 357 THEN SCS_TAC
 358 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 359 THEN RESA_TAC;
 360
 361 THAYTHE_TAC (5-2)[`i`;`j`];
 362
 363 MP_TAC(SET_RULE`SUC i MOD 5= j MOD 5\/ ~(SUC i MOD 5= j MOD 5)`)
 364 THEN RESA_TAC;
 365
 366 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
 367 THEN THAYTHE_TAC (7-2)[`i`;`j`]
 368 THEN DICH_TAC 1
 369 THEN DICH_TAC 1
 370 THEN DICH_TAC 1
 371 THEN STRIP_TAC
 372 THEN STRIP_TAC
 373 THEN SYM_ASSUM_TAC
 374 THEN SYM_ASSUM_TAC
 375 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
 376 THEN SYM_ASSUM_TAC
 377 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
 378 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 379 THEN RESA_TAC
 380 THEN SCS_TAC
 381 THEN REWRITE_TAC[h0;cstab]
 382 THEN REAL_ARITH_TAC;
 383
 384 MP_TAC(SET_RULE`i MOD 5= SUC j MOD 5\/ ~(i MOD 5= SUC j MOD 5)`)
 385 THEN RESA_TAC;
 386
 387 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
 388 THEN THAYTHE_TAC (8-2)[`i`;`j`]
 389 THEN DICH_TAC 1
 390 THEN DICH_TAC 1
 391 THEN STRIP_TAC
 392 THEN SYM_ASSUM_TAC
 393 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
 394 THEN SYM_ASSUM_TAC
 395 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
 396 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 397 THEN RESA_TAC
 398 THEN SCS_TAC
 399 THEN REWRITE_TAC[h0;cstab]
 400 THEN REAL_ARITH_TAC;
 401
 402 MP_TAC DIAG_5_EQU_PSORT
 403 THEN RESA_TAC
 404 THEN REWRITE_TAC[PAIR_EQ]
 405 THEN SCS_TAC;
 406
 407 THAYTHE_TAC (5-2)[`i`;`j`];
 408
 409 MP_TAC(SET_RULE`SUC i MOD 5= j MOD 5\/ ~(SUC i MOD 5= j MOD 5)`)
 410 THEN RESA_TAC;
 411
 412 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
 413 THEN THAYTHE_TAC (7-2)[`i`;`j`]
 414 THEN DICH_TAC 0
 415 THEN DICH_TAC 1
 416 THEN DICH_TAC 1
 417 THEN STRIP_TAC
 418 THEN STRIP_TAC
 419 THEN SYM_ASSUM_TAC
 420 THEN SYM_ASSUM_TAC
 421 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
 422 THEN SYM_ASSUM_TAC
 423 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
 424 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 425 THEN RESA_TAC
 426 THEN SCS_TAC
 427 THEN REWRITE_TAC[h0;cstab]
 428 THEN MP_TAC sqrt8_LE_CSTAB
 429 THEN REAL_ARITH_TAC;
 430
 431 MP_TAC(SET_RULE`i MOD 5= SUC j MOD 5\/ ~(i MOD 5= SUC j MOD 5)`)
 432 THEN RESA_TAC;
 433
 434 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
 435 THEN THAYTHE_TAC (8-2)[`i`;`j`]
 436 THEN DICH_TAC 0
 437 THEN DICH_TAC 1
 438 THEN STRIP_TAC
 439 THEN SYM_ASSUM_TAC
 440 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
 441 THEN SYM_ASSUM_TAC
 442 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
 443 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 444 THEN RESA_TAC
 445 THEN SCS_TAC
 446 THEN REWRITE_TAC[h0;cstab]
 447 THEN MP_TAC sqrt8_LE_CSTAB
 448 THEN REAL_ARITH_TAC;
 449
 450 MP_TAC DIAG_5_EQU_PSORT
 451 THEN RESA_TAC
 452 THEN REWRITE_TAC[PAIR_EQ]
 453 THEN SCS_TAC
 454 THEN THAYTHE_TAC(8-2)[`i`;`j`]
 455 THEN DICH_TAC 0
 456 THEN REWRITE_TAC[PAIR_EQ]
 457 THEN SCS_TAC]);;
 458
 459
 460 let MM_5I3_IMP_MM_5M2=prove(`MMs_v39 scs_5I3 v/\ (!i j. scs_diag 5 i j ==>   cstab <= dist(v i,v j)) ==> ~(MMs_v39 scs_5M2 ={})`,
 461 STRIP_TAC
 462 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
 463 THEN EXISTS_TAC`v:num->real^3`
 464 THEN EXISTS_TAC`scs_5I3`
 465 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I3`;`v`]
 466 THEN ASSUME_TAC SCS_5I3_BASIC
 467 THEN ASSUME_TAC K_SCS_5I3
 468 THEN ASSUME_TAC SCS_5M2_BASIC
 469 THEN ASSUME_TAC K_SCS_5M2
 470 THEN ASSUME_TAC SCS_5M2_IS_SCS
 471 THEN ASM_SIMP_TAC[BB_5I3_IS_BB_5M2;IN;SCS_5I3_IS_SCS]
 472 THEN SCS_TAC
 473 THEN REAL_ARITH_TAC);;
 474
 475
 476 let BB_5M1_IS_BB_5M2=prove_by_refinement(`BBs_v39 scs_5M1 v/\ (!i j. scs_diag 5 i j ==>   cstab <= dist(v i,v j)) ==> BBs_v39 scs_5M2 v`,
 477 [
 478 REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5M1;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`]
 479 THEN SCS_TAC
 480 THEN REPEAT RESA_TAC
 481 THEN SCS_TAC
 482 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 483 THEN RESA_TAC;
 484
 485 THAYTHE_TAC (5-2)[`i`;`j`];
 486
 487 MP_TAC(SET_RULE`SUC i MOD 5= j MOD 5\/ ~(SUC i MOD 5= j MOD 5)`)
 488 THEN RESA_TAC;
 489
 490 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
 491 THEN THAYTHE_TAC (7-2)[`i`;`j`]
 492 THEN DICH_TAC 1
 493 THEN DICH_TAC 1
 494 THEN DICH_TAC 1
 495 THEN STRIP_TAC
 496 THEN STRIP_TAC
 497 THEN SYM_ASSUM_TAC
 498 THEN SYM_ASSUM_TAC
 499 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
 500 THEN SYM_ASSUM_TAC
 501 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
 502 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 503 THEN RESA_TAC
 504 THEN SCS_TAC
 505 THEN REWRITE_TAC[h0;cstab]
 506 THEN REAL_ARITH_TAC;
 507
 508 MP_TAC(SET_RULE`i MOD 5= SUC j MOD 5\/ ~(i MOD 5= SUC j MOD 5)`)
 509 THEN RESA_TAC;
 510
 511 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
 512 THEN THAYTHE_TAC (8-2)[`i`;`j`]
 513 THEN DICH_TAC 1
 514 THEN DICH_TAC 1
 515 THEN STRIP_TAC
 516 THEN SYM_ASSUM_TAC
 517 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
 518 THEN SYM_ASSUM_TAC
 519 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
 520 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 521 THEN RESA_TAC
 522 THEN SCS_TAC
 523 THEN REWRITE_TAC[h0;cstab]
 524 THEN REAL_ARITH_TAC;
 525
 526 MP_TAC DIAG_5_EQU_PSORT
 527 THEN RESA_TAC
 528 THEN REWRITE_TAC[PAIR_EQ]
 529 THEN SCS_TAC]);;
 530
 531
 532
 533 let MM_5M1_IMP_MM_5M2=prove(`MMs_v39 scs_5M1 v/\ (!i j. scs_diag 5 i j ==>   cstab <= dist(v i,v j)) ==> ~(MMs_v39 scs_5M2 ={})`,
 534 STRIP_TAC
 535 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
 536 THEN EXISTS_TAC`v:num->real^3`
 537 THEN EXISTS_TAC`scs_5M1`
 538 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M1`;`v`]
 539 THEN ASSUME_TAC SCS_5M1_BASIC
 540 THEN ASSUME_TAC K_SCS_5M1
 541 THEN ASSUME_TAC SCS_5M2_BASIC
 542 THEN ASSUME_TAC K_SCS_5M2
 543 THEN ASSUME_TAC SCS_5M2_IS_SCS
 544 THEN ASM_SIMP_TAC[BB_5M1_IS_BB_5M2;IN;SCS_5M1_IS_SCS]
 545 THEN SCS_TAC
 546 THEN REAL_ARITH_TAC);;
 547
 548 (***********DIST<= cstab*************)
 549
 550
 551 let SCS_5I1_STAB_DIAG= prove(
 552 `!v i j.
 553     v IN MMs_v39 scs_5I1 /\
 554     scs_diag 5 i j /\
 555     dist(v i,v j) <= cstab ==>
 556     v IN MMs_v39 (scs_stab_diag_v39 scs_5I1 i j)`,
 557 REWRITE_TAC[IN]
 558 THEN REPEAT STRIP_TAC
 559 THEN MP_TAC SCS_5I1_IS_SCS
 560 THEN STRIP_TAC
 561 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I1`;`v`]
 562 THEN MRESA_TAC DIST_LE_IMP_A_LE[`v`;`scs_5I1`;`i`;`j`;`cstab`]
 563 THEN ASSUME_TAC SCS_5I1_BASIC
 564 THEN ASSUME_TAC K_SCS_5I1
 565 THEN MRESAL_TAC Yrtafyh.YRTAFYH[`scs_5I1`;`i`;`j`][ARITH_RULE`3<5`;]
 566 THEN MP_TAC  Ppbtydq.MXQTIED
 567 THEN REWRITE_TAC[IN]
 568 THEN STRIP_TAC
 569 THEN MATCH_DICH_TAC 0
 570 THEN EXISTS_TAC`scs_5I1`
 571 THEN ASM_SIMP_TAC[STAB_BB;SCS_K_D_A_STAB_EQ;DIAG_SCS_M_EQ;REAL_ARITH`a<=a`]
 572 THEN REPEAT GEN_TAC
 573 THEN REWRITE_TAC[scs_stab_diag_v39;scs_5I1;scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;CS_ADJ]
 574 THEN SCS_TAC
 575 THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
 576 THEN RESA_TAC
 577 THENL[
 578 MRESAL_TAC DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
 579 THEN DICH_TAC 0
 580 THEN REWRITE_TAC[scs_diag;cstab;h0]
 581 THEN RESA_TAC
 582 THEN REAL_ARITH_TAC;
 583 REAL_ARITH_TAC]);;
 584
 585 let SCS_5I2_STAB_DIAG= prove( `!v i j.
 586     v IN MMs_v39 scs_5I2 /\
 587     scs_diag 5 i j /\
 588     dist(v i,v j) <= cstab ==>
 589     v IN MMs_v39 (scs_stab_diag_v39 scs_5I2 i j)`,
 590 REWRITE_TAC[IN]
 591 THEN REPEAT STRIP_TAC
 592 THEN MP_TAC SCS_5I2_IS_SCS
 593 THEN STRIP_TAC
 594 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I2`;`v`]
 595 THEN MRESA_TAC DIST_LE_IMP_A_LE[`v`;`scs_5I2`;`i`;`j`;`cstab`]
 596 THEN ASSUME_TAC SCS_5I2_BASIC
 597 THEN ASSUME_TAC K_SCS_5I2
 598 THEN MRESAL_TAC Yrtafyh.YRTAFYH[`scs_5I2`;`i`;`j`][ARITH_RULE`3<5`;]
 599 THEN MP_TAC  Ppbtydq.MXQTIED
 600 THEN REWRITE_TAC[IN]
 601 THEN STRIP_TAC
 602 THEN MATCH_DICH_TAC 0
 603 THEN EXISTS_TAC`scs_5I2`
 604 THEN ASM_SIMP_TAC[STAB_BB;SCS_K_D_A_STAB_EQ;DIAG_SCS_M_EQ;REAL_ARITH`a<=a`]
 605 THEN REPEAT GEN_TAC
 606 THEN REWRITE_TAC[scs_stab_diag_v39;scs_5I2;scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;CS_ADJ]
 607 THEN SCS_TAC
 608 THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
 609 THEN RESA_TAC
 610 THENL[
 611 MRESAL_TAC DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
 612 THEN DICH_TAC 0
 613 THEN REWRITE_TAC[scs_diag;cstab;h0]
 614 THEN RESA_TAC
 615 THEN REAL_ARITH_TAC;
 616 REAL_ARITH_TAC]);;
 617
 618
 619
 620 let SCS_5I3_STAB_DIAG= prove( `!v i j.
 621     v IN MMs_v39 scs_5I3 /\
 622     scs_diag 5 i j /\
 623     dist(v i,v j) <= cstab ==>
 624     v IN MMs_v39 (scs_stab_diag_v39 scs_5I3 i j)`,
 625 REWRITE_TAC[IN]
 626 THEN REPEAT STRIP_TAC
 627 THEN MP_TAC SCS_5I3_IS_SCS
 628 THEN STRIP_TAC
 629 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I3`;`v`]
 630 THEN MRESA_TAC DIST_LE_IMP_A_LE[`v`;`scs_5I3`;`i`;`j`;`cstab`]
 631 THEN ASSUME_TAC SCS_5I3_BASIC
 632 THEN ASSUME_TAC K_SCS_5I3
 633 THEN MRESAL_TAC Yrtafyh.YRTAFYH[`scs_5I3`;`i`;`j`][ARITH_RULE`3<5`;]
 634 THEN MP_TAC  Ppbtydq.MXQTIED
 635 THEN REWRITE_TAC[IN]
 636 THEN STRIP_TAC
 637 THEN MATCH_DICH_TAC 0
 638 THEN EXISTS_TAC`scs_5I3`
 639 THEN ASM_SIMP_TAC[STAB_BB;SCS_K_D_A_STAB_EQ;DIAG_SCS_M_EQ;REAL_ARITH`a<=a`]
 640 THEN REPEAT GEN_TAC
 641 THEN REWRITE_TAC[scs_stab_diag_v39;scs_5I3;scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;CS_ADJ]
 642 THEN SCS_TAC
 643 THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
 644 THEN RESA_TAC
 645 THENL[
 646 MRESAL_TAC DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
 647 THEN DICH_TAC 0
 648 THEN REWRITE_TAC[scs_diag;cstab;h0]
 649 THEN RESA_TAC
 650 THEN MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`]
 651 THEN REWRITE_TAC[PAIR_EQ]
 652 THEN SCS_TAC
 653 THEN REAL_ARITH_TAC;
 654 REAL_ARITH_TAC]);;
 655
 656
 657 let SCS_5M1_STAB_DIAG= prove( `!v i j.
 658     v IN MMs_v39 scs_5M1 /\
 659     scs_diag 5 i j /\
 660     dist(v i,v j) <= cstab ==>
 661     v IN MMs_v39 (scs_stab_diag_v39 scs_5M1 i j)`,
 662 REWRITE_TAC[IN]
 663 THEN REPEAT STRIP_TAC
 664 THEN MP_TAC SCS_5M1_IS_SCS
 665 THEN STRIP_TAC
 666 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M1`;`v`]
 667 THEN MRESA_TAC DIST_LE_IMP_A_LE[`v`;`scs_5M1`;`i`;`j`;`cstab`]
 668 THEN ASSUME_TAC SCS_5M1_BASIC
 669 THEN ASSUME_TAC K_SCS_5M1
 670 THEN MRESAL_TAC Yrtafyh.YRTAFYH[`scs_5M1`;`i`;`j`][ARITH_RULE`3<5`;]
 671 THEN MP_TAC  Ppbtydq.MXQTIED
 672 THEN REWRITE_TAC[IN]
 673 THEN STRIP_TAC
 674 THEN MATCH_DICH_TAC 0
 675 THEN EXISTS_TAC`scs_5M1`
 676 THEN ASM_SIMP_TAC[STAB_BB;SCS_K_D_A_STAB_EQ;DIAG_SCS_M_EQ;REAL_ARITH`a<=a`]
 677 THEN REPEAT GEN_TAC
 678 THEN REWRITE_TAC[scs_stab_diag_v39;scs_5M1;scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;CS_ADJ]
 679 THEN SCS_TAC
 680 THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
 681 THEN RESA_TAC
 682 THENL[
 683 MRESAL_TAC DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
 684 THEN DICH_TAC 0
 685 THEN REWRITE_TAC[scs_diag;cstab;h0]
 686 THEN RESA_TAC
 687 THEN MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`]
 688 THEN REWRITE_TAC[PAIR_EQ]
 689 THEN SCS_TAC
 690 THEN REAL_ARITH_TAC;
 691 REAL_ARITH_TAC]);;
 692
 693
 694 (*****************)
 695
 696
 697 let SCS_5I1_BERAK_BY_CSTAB= prove_by_refinement( `scs_arrow_v39 { scs_5I1 } ({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I1 i j| scs_diag 5 i j })`,
 698 [
 699 REPEAT GEN_TAC
 700 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
 701 THEN ABBREV_TAC`k=scs_k_v39 s`
 702 THEN REPEAT RESA_TAC;
 703
 704 REWRITE_TAC[SCS_5M2_IS_SCS];
 705
 706 MATCH_MP_TAC Yrtafyh.STAB_IS_SCS
 707 THEN ASM_SIMP_TAC[SCS_5I1_IS_SCS;K_SCS_5I1;SCS_5I1_BASIC;ARITH_RULE`3<5`]
 708 THEN SCS_TAC
 709 THEN REWRITE_TAC[h0;cstab]
 710 THEN REAL_ARITH_TAC;
 711
 712 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_5I1 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_5I1 ==> MMs_v39 s = {}))`);
 713
 714 ASM_REWRITE_TAC[];
 715
 716 ASM_REWRITE_TAC[]
 717 THEN POP_ASSUM MP_TAC
 718 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
 719 THEN REPEAT STRIP_TAC
 720 THEN POP_ASSUM MP_TAC
 721 THEN RESA_TAC
 722 THEN POP_ASSUM MP_TAC
 723 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
 724 THEN STRIP_TAC;
 725
 726 MP_TAC(SET_RULE`(!i j. scs_diag 5 i j ==>   cstab < dist(v i,v j))\/ ~((!i j. scs_diag 5 i j ==>   cstab < dist((v:num->real^3) i,v j)))`)
 727 THEN RESA_TAC;
 728
 729 EXISTS_TAC`scs_5M2`
 730 THEN ASM_REWRITE_TAC[]
 731 THEN MP_TAC MM_5I1_IMP_MM_5M2
 732 THEN RESA_TAC
 733 THEN POP_ASSUM MP_TAC
 734 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
 735 THEN STRIP_TAC
 736 THEN MATCH_DICH_TAC 0
 737 THEN REPEAT STRIP_TAC
 738 THEN THAYTHE_TAC 1[`i`;`j`]
 739 THEN POP_ASSUM MP_TAC
 740 THEN REAL_ARITH_TAC;
 741
 742 POP_ASSUM MP_TAC
 743 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
 744 THEN STRIP_TAC
 745 THEN EXISTS_TAC`scs_stab_diag_v39 scs_5I1 i j`
 746 THEN ASM_REWRITE_TAC[]
 747 THEN STRIP_TAC;
 748
 749 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
 750 THEN EXISTS_TAC`i:num`
 751 THEN EXISTS_TAC`j:num`
 752 THEN ASM_REWRITE_TAC[];
 753
 754 MRESAL_TAC SCS_5I1_STAB_DIAG[`v`;`i`;`j`][IN]
 755 THEN EXISTS_TAC`v:num->real^3`
 756 THEN ASM_REWRITE_TAC[];]);;
 757
 758
 759 let SCS_5I2_BERAK_BY_CSTAB= prove_by_refinement(
 760 `scs_arrow_v39 { scs_5I2 } ({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j })`,
 761 [
 762 REPEAT GEN_TAC
 763 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
 764 THEN ABBREV_TAC`k=scs_k_v39 s`
 765 THEN REPEAT RESA_TAC;
 766
 767 REWRITE_TAC[SCS_5M2_IS_SCS];
 768
 769 MATCH_MP_TAC Yrtafyh.STAB_IS_SCS
 770 THEN ASM_SIMP_TAC[SCS_5I2_IS_SCS;K_SCS_5I2;SCS_5I2_BASIC;ARITH_RULE`3<5`]
 771 THEN SCS_TAC
 772 THEN REWRITE_TAC[h0;cstab]
 773 THEN MP_TAC sqrt8_LE_CSTAB
 774 THEN REAL_ARITH_TAC;
 775
 776 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_5I2 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_5I2 ==> MMs_v39 s = {}))`);
 777
 778 ASM_REWRITE_TAC[];
 779
 780 ASM_REWRITE_TAC[]
 781 THEN POP_ASSUM MP_TAC
 782 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
 783 THEN REPEAT STRIP_TAC
 784 THEN POP_ASSUM MP_TAC
 785 THEN RESA_TAC
 786 THEN POP_ASSUM MP_TAC
 787 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
 788 THEN STRIP_TAC;
 789
 790 MP_TAC(SET_RULE`(!i j. scs_diag 5 i j ==>   cstab < dist(v i,v j))\/ ~((!i j. scs_diag 5 i j ==>   cstab < dist((v:num->real^3) i,v j)))`)
 791 THEN RESA_TAC;
 792
 793 EXISTS_TAC`scs_5M2`
 794 THEN ASM_REWRITE_TAC[]
 795 THEN MP_TAC MM_5I2_IMP_MM_5M2
 796 THEN RESA_TAC
 797 THEN POP_ASSUM MP_TAC
 798 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
 799 THEN STRIP_TAC
 800 THEN MATCH_DICH_TAC 0
 801 THEN REPEAT STRIP_TAC
 802 THEN THAYTHE_TAC 1[`i`;`j`]
 803 THEN POP_ASSUM MP_TAC
 804 THEN REAL_ARITH_TAC;
 805
 806 POP_ASSUM MP_TAC
 807 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
 808 THEN STRIP_TAC
 809 THEN EXISTS_TAC`scs_stab_diag_v39 scs_5I2 i j`
 810 THEN ASM_REWRITE_TAC[]
 811 THEN STRIP_TAC;
 812
 813 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
 814 THEN EXISTS_TAC`i:num`
 815 THEN EXISTS_TAC`j:num`
 816 THEN ASM_REWRITE_TAC[];
 817
 818 MRESAL_TAC SCS_5I2_STAB_DIAG[`v`;`i`;`j`][IN]
 819 THEN EXISTS_TAC`v:num->real^3`
 820 THEN ASM_REWRITE_TAC[]]);;
 821
 822
 823
 824 let SCS_5I3_BERAK_BY_CSTAB= prove_by_refinement(
 825 `scs_arrow_v39 { scs_5I3 } ({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I3 i j| scs_diag 5 i j })`,
 826 [
 827 REPEAT GEN_TAC
 828 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
 829 THEN ABBREV_TAC`k=scs_k_v39 s`
 830 THEN REPEAT RESA_TAC;
 831
 832 REWRITE_TAC[SCS_5M2_IS_SCS];
 833
 834 MATCH_MP_TAC Yrtafyh.STAB_IS_SCS
 835 THEN ASM_SIMP_TAC[SCS_5I3_IS_SCS;K_SCS_5I3;SCS_5I3_BASIC;ARITH_RULE`3<5`]
 836 THEN SCS_TAC
 837 THEN REWRITE_TAC[h0;cstab]
 838 THEN MP_TAC sqrt8_LE_CSTAB
 839 THEN REAL_ARITH_TAC;
 840
 841 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_5I3 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_5I3 ==> MMs_v39 s = {}))`);
 842
 843 ASM_REWRITE_TAC[];
 844
 845 ASM_REWRITE_TAC[]
 846 THEN POP_ASSUM MP_TAC
 847 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
 848 THEN REPEAT STRIP_TAC
 849 THEN POP_ASSUM MP_TAC
 850 THEN RESA_TAC
 851 THEN POP_ASSUM MP_TAC
 852 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
 853 THEN STRIP_TAC;
 854
 855 MP_TAC(SET_RULE`(!i j. scs_diag 5 i j ==>   cstab < dist(v i,v j))\/ ~((!i j. scs_diag 5 i j ==>   cstab < dist((v:num->real^3) i,v j)))`)
 856 THEN RESA_TAC;
 857
 858 EXISTS_TAC`scs_5M2`
 859 THEN ASM_REWRITE_TAC[]
 860 THEN MP_TAC MM_5I3_IMP_MM_5M2
 861 THEN RESA_TAC
 862 THEN POP_ASSUM MP_TAC
 863 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
 864 THEN STRIP_TAC
 865 THEN MATCH_DICH_TAC 0
 866 THEN REPEAT STRIP_TAC
 867 THEN THAYTHE_TAC 1[`i`;`j`]
 868 THEN POP_ASSUM MP_TAC
 869 THEN REAL_ARITH_TAC;
 870
 871 POP_ASSUM MP_TAC
 872 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
 873 THEN STRIP_TAC
 874 THEN EXISTS_TAC`scs_stab_diag_v39 scs_5I3 i j`
 875 THEN ASM_REWRITE_TAC[]
 876 THEN STRIP_TAC;
 877
 878 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
 879 THEN EXISTS_TAC`i:num`
 880 THEN EXISTS_TAC`j:num`
 881 THEN ASM_REWRITE_TAC[];
 882
 883 MRESAL_TAC SCS_5I3_STAB_DIAG[`v`;`i`;`j`][IN]
 884 THEN EXISTS_TAC`v:num->real^3`
 885 THEN ASM_REWRITE_TAC[]]);;
 886
 887
 888 let SCS_5M1_BERAK_BY_CSTAB= prove_by_refinement(`scs_arrow_v39 { scs_5M1 } ({ scs_5M2}UNION { scs_stab_diag_v39 scs_5M1 i j| scs_diag 5 i j })`,
 889 [
 890 REPEAT GEN_TAC
 891 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
 892 THEN ABBREV_TAC`k=scs_k_v39 s`
 893 THEN REPEAT RESA_TAC;
 894
 895 REWRITE_TAC[SCS_5M2_IS_SCS];
 896
 897 MATCH_MP_TAC Yrtafyh.STAB_IS_SCS
 898 THEN ASM_SIMP_TAC[SCS_5M1_IS_SCS;K_SCS_5M1;SCS_5M1_BASIC;ARITH_RULE`3<5`]
 899 THEN SCS_TAC
 900 THEN REWRITE_TAC[h0;cstab]
 901 THEN MP_TAC sqrt8_LE_CSTAB
 902 THEN REAL_ARITH_TAC;
 903
 904 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_5M1 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_5M1 ==> MMs_v39 s = {}))`);
 905
 906 ASM_REWRITE_TAC[];
 907
 908 ASM_REWRITE_TAC[]
 909 THEN POP_ASSUM MP_TAC
 910 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
 911 THEN REPEAT STRIP_TAC
 912 THEN POP_ASSUM MP_TAC
 913 THEN RESA_TAC
 914 THEN POP_ASSUM MP_TAC
 915 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
 916 THEN STRIP_TAC;
 917
 918 MP_TAC(SET_RULE`(!i j. scs_diag 5 i j ==>   cstab < dist(v i,v j))\/ ~((!i j. scs_diag 5 i j ==>   cstab < dist((v:num->real^3) i,v j)))`)
 919 THEN RESA_TAC;
 920
 921 EXISTS_TAC`scs_5M2`
 922 THEN ASM_REWRITE_TAC[]
 923 THEN MP_TAC MM_5M1_IMP_MM_5M2
 924 THEN RESA_TAC
 925 THEN POP_ASSUM MP_TAC
 926 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
 927 THEN STRIP_TAC
 928 THEN MATCH_DICH_TAC 0
 929 THEN REPEAT STRIP_TAC
 930 THEN THAYTHE_TAC 1[`i`;`j`]
 931 THEN POP_ASSUM MP_TAC
 932 THEN REAL_ARITH_TAC;
 933
 934 POP_ASSUM MP_TAC
 935 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
 936 THEN STRIP_TAC
 937 THEN EXISTS_TAC`scs_stab_diag_v39 scs_5M1 i j`
 938 THEN ASM_REWRITE_TAC[]
 939 THEN STRIP_TAC;
 940
 941 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
 942 THEN EXISTS_TAC`i:num`
 943 THEN EXISTS_TAC`j:num`
 944 THEN ASM_REWRITE_TAC[];
 945
 946 MRESAL_TAC SCS_5M1_STAB_DIAG[`v`;`i`;`j`][IN]
 947 THEN EXISTS_TAC`v:num->real^3`
 948 THEN ASM_REWRITE_TAC[]]);;
 949
 950
 951 (**********************)
 952
 953 let DIAG_EQ_ADD5=prove(`scs_diag 5 (i MOD 5) (j MOD 5)<=>
 954 ((i MOD 5= (j MOD 5+ 2) MOD 5)\/
 955 (j MOD 5=(i MOD 5+2) MOD 5))`,
 956 REWRITE_TAC[scs_diag]
 957 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5= 0 \/ i MOD 5= 1 \/i MOD 5= 2 \/
 958 i MOD 5= 3 \/i MOD 5= 4 `)
 959 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 960 THEN RESA_TAC
 961 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5= 0 \/ j MOD 5= 1 \/j MOD 5= 2 \/
 962 j MOD 5= 3 \/j MOD 5= 4
 963 `)
 964 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
 965 THEN RESA_TAC
 966 THEN ARITH_TAC);;
 967
 968
 969 let EXPAND_STAB_DIAG_5=prove_by_refinement(`is_scs_v39 s /\scs_k_v39 s=5==>
 970 {scs_stab_diag_v39 s (i MOD 5) (j MOD 5) | i MOD 5 =
 971                                                   (j MOD 5 + 2) MOD 5 \/
 972                                                   j MOD 5 =
 973                                                   (i MOD 5 + 2) MOD 5}=
 974 {scs_stab_diag_v39 s (i+2) i| i<5} `,
 975 [REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;UNION]
 976 THEN STRIP_TAC
 977 THEN GEN_TAC
 978 THEN EQ_TAC
 979 THEN RESA_TAC;
 980
 981 MRESAS_TAC STAB_MOD[`s`;`j MOD 5 + 2`;`j MOD 5`][SCS_5I1_IS_SCS;K_SCS_5I1;MOD_REFL;ARITH_RULE`~(5=0)`]
 982 THEN EXISTS_TAC`j MOD 5`
 983 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`];
 984
 985 MRESAS_TAC STAB_MOD[`s`;`i MOD 5`;`i MOD 5 + 2`][SCS_5I1_IS_SCS;K_SCS_5I1;MOD_REFL;ARITH_RULE`~(5=0)`]
 986 THEN EXISTS_TAC`i MOD 5`
 987 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`;STAB_SYM];
 988
 989 EXISTS_TAC`i+2`
 990 THEN EXISTS_TAC`i:num`
 991 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`;MOD_LT]
 992 THEN MRESAS_TAC STAB_MOD[`s`;`(i + 2)`;`i`][SCS_5I1_IS_SCS;K_SCS_5I1;MOD_REFL;ARITH_RULE`~(5=0)`;MOD_LT]]);;
 993
 994
 995 let EXPAND_STAB_DIAG_5I1=prove(`{scs_stab_diag_v39 scs_5I1 (i MOD 5) (j MOD 5) | i MOD 5 =
 996                                                   (j MOD 5 + 2) MOD 5 \/
 997                                                   j MOD 5 =
 998                                                   (i MOD 5 + 2) MOD 5}=
 999 {scs_stab_diag_v39 scs_5I1 (i+2) i| i<5} `,
1000 ASM_SIMP_TAC[EXPAND_STAB_DIAG_5;SCS_5I1_IS_SCS;K_SCS_5I1]);;
1001
1002
1003 let EXPAND_STAB_DIAG_5I2=prove(`{scs_stab_diag_v39 scs_5I2 (i MOD 5) (j MOD 5) | i MOD 5 =
1004                                                   (j MOD 5 + 2) MOD 5 \/
1005                                                   j MOD 5 =
1006                                                   (i MOD 5 + 2) MOD 5}=
1007 {scs_stab_diag_v39 scs_5I2 (i+2) i| i<5} `,
1008 ASM_SIMP_TAC[EXPAND_STAB_DIAG_5;SCS_5I2_IS_SCS;K_SCS_5I2]);;
1009
1010
1011
1012 let EXPAND_STAB_DIAG_5I3=prove(`{scs_stab_diag_v39 scs_5I3 (i MOD 5) (j MOD 5) | i MOD 5 =
1013                                                   (j MOD 5 + 2) MOD 5 \/
1014                                                   j MOD 5 =
1015                                                   (i MOD 5 + 2) MOD 5}=
1016 {scs_stab_diag_v39 scs_5I3 (i+2) i| i<5} `,
1017 ASM_SIMP_TAC[EXPAND_STAB_DIAG_5;SCS_5I3_IS_SCS;K_SCS_5I3]);;
1018
1019
1020 let EXPAND_STAB_DIAG_5M1=prove(`{scs_stab_diag_v39 scs_5M1 (i MOD 5) (j MOD 5) | i MOD 5 =
1021                                                   (j MOD 5 + 2) MOD 5 \/
1022                                                   j MOD 5 =
1023                                                   (i MOD 5 + 2) MOD 5}=
1024 {scs_stab_diag_v39 scs_5M1 (i+2) i| i<5} `,
1025 ASM_SIMP_TAC[EXPAND_STAB_DIAG_5;SCS_5M1_IS_SCS;K_SCS_5M1]);;
1026
1027
1028
1029
1030
1031
1032 let EQ_DIAG_STAB_5I1_02=prove(`scs_arrow_v39
1033  {scs_stab_diag_v39 scs_5I1 (i + 2) i }
1034  {scs_stab_diag_v39 scs_5I1 0 2}`,
1035 MRESA_TAC STAB_SYM[`scs_5I1`;`2`;`0`]
1036 THEN MP_TAC (GEN_ALL Wkeidft.WKEIDFT)
1037 THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
1038 THEN STRIP_TAC
1039 THEN MATCH_DICH_TAC 0
1040 THEN ASM_SIMP_TAC[ARITH_RULE`2 + i = (i + 2) + 0/\ 3<6/\ i+1= SUC i`;K_SCS_5I1;h0_LT_B_SCS_5I1;h0_EQ_B_SCS_5I1;SCS_5I1_IS_SCS;SCS_5I1_BASIC]
1041 THEN SCS_TAC
1042 THEN ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;]
1043 THEN EXISTS_TAC`&0`
1044 THEN EXISTS_TAC`&2`
1045 THEN EXISTS_TAC`&2 *h0`
1046 THEN EXISTS_TAC`&2 *h0`
1047 THEN EXISTS_TAC`&6`
1048 THEN ASM_SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + 2)= i+3/\ SUC i= i+1/\ 2+1=3`;ARITH_RULE`1<5/\ ~(5=0)`;Qknvmlb.SUC_MOD_NOT_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1049 THEN SCS_TAC
1050 THEN MP_TAC(SET_RULE`i= i+0==> i MOD 5= (i+0) MOD 5`)
1051 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
1052 THEN RESA_TAC
1053 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`1<5/\ ~(5=0)/\ 3<5`]
1054 THEN SCS_TAC);;
1055
1056
1057
1058 let EQ_DIAG_STAB_5I2_02=prove(`scs_arrow_v39
1059  {scs_stab_diag_v39 scs_5I2 (i + 2) i }
1060  {scs_stab_diag_v39 scs_5I2 0 2}`,
1061 MRESA_TAC STAB_SYM[`scs_5I2`;`2`;`0`]
1062 THEN MP_TAC (GEN_ALL Wkeidft.WKEIDFT)
1063 THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
1064 THEN STRIP_TAC
1065 THEN MATCH_DICH_TAC 0
1066 THEN ASM_SIMP_TAC[ARITH_RULE`2 + i = (i + 2) + 0/\ 3<6/\ i+1= SUC i`;K_SCS_5I2;h0_LT_B_SCS_5I2;h0_EQ_B_SCS_5I2;SCS_5I2_IS_SCS;SCS_5I2_BASIC]
1067 THEN SCS_TAC
1068 THEN ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;]
1069 THEN EXISTS_TAC`&0`
1070 THEN EXISTS_TAC`&2`
1071 THEN EXISTS_TAC`&2 *h0`
1072 THEN EXISTS_TAC`sqrt8`
1073 THEN EXISTS_TAC`&6`
1074 THEN ASM_SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + 2)= i+3/\ SUC i= i+1/\ 2+1=3`;ARITH_RULE`1<5/\ ~(5=0)`;Qknvmlb.SUC_MOD_NOT_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1075 THEN SCS_TAC
1076 THEN MP_TAC(SET_RULE`i= i+0==> i MOD 5= (i+0) MOD 5`)
1077 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
1078 THEN RESA_TAC
1079 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`1<5/\ ~(5=0)/\ 3<5`]
1080 THEN SCS_TAC);;
1081
1082
1083 let SET_EQ_DIAG_STAB_5I1_02=prove(`scs_arrow_v39
1084  {scs_stab_diag_v39 scs_5I1 (i + 2) i |i<5}
1085  {scs_stab_diag_v39 scs_5I1 0 2}`,
1086 REWRITE_TAC[ARITH_RULE`i<5<=> i=0\/i=1\/i=2\/i=3\/i=4`;SET_RULE`{scs_stab_diag_v39 scs_5I1 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
1087 =
1088 {scs_stab_diag_v39 scs_5I1 (0 + 2) 0} UNION
1089 {scs_stab_diag_v39 scs_5I1 (1 + 2) 1} UNION
1090 {scs_stab_diag_v39 scs_5I1 (2 + 2) 2} UNION
1091 {scs_stab_diag_v39 scs_5I1 (3 + 2) 3} UNION
1092 {scs_stab_diag_v39 scs_5I1 (4 + 2) 4}
1093 `;]
1094 THEN REPEAT(ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_5I1 0 2}={scs_stab_diag_v39 scs_5I1 0 2} UNION {scs_stab_diag_v39 scs_5I1 0 2}`]
1095 THEN MATCH_MP_TAC FZIOTEF_UNION
1096 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_5I1_02]));;
1097
1098
1099
1100 let SET_EQ_DIAG_STAB_5I2_02=prove(`scs_arrow_v39
1101  {scs_stab_diag_v39 scs_5I2 (i + 2) i |i<5}
1102  {scs_stab_diag_v39 scs_5I2 0 2}`,
1103 REWRITE_TAC[ARITH_RULE`i<5<=> i=0\/i=1\/i=2\/i=3\/i=4`;SET_RULE`{scs_stab_diag_v39 scs_5I2 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
1104 =
1105 {scs_stab_diag_v39 scs_5I2 (0 + 2) 0} UNION
1106 {scs_stab_diag_v39 scs_5I2 (1 + 2) 1} UNION
1107 {scs_stab_diag_v39 scs_5I2 (2 + 2) 2} UNION
1108 {scs_stab_diag_v39 scs_5I2 (3 + 2) 3} UNION
1109 {scs_stab_diag_v39 scs_5I2 (4 + 2) 4}
1110 `;]
1111 THEN REPEAT(ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_5I2 0 2}={scs_stab_diag_v39 scs_5I2 0 2} UNION {scs_stab_diag_v39 scs_5I2 0 2}`]
1112 THEN MATCH_MP_TAC FZIOTEF_UNION
1113 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_5I2_02]));;
1114
1115
1116
1117 (*******************)
1118
1119 let SET_STAB_5I1=prove(`{ scs_stab_diag_v39 scs_5I1 i j| scs_diag 5 i j }= { scs_stab_diag_v39 scs_5I1 (i MOD 5) (j  MOD 5)| scs_diag 5 (i MOD 5) (j  MOD 5) }`,
1120  ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(5=0)`;]
1121 THEN MRESAL_TAC STAB_MOD[`scs_5I1`][SCS_5I1_IS_SCS;K_SCS_5I1]);;
1122
1123
1124 let SET_STAB_5I2=prove(`{ scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j }= { scs_stab_diag_v39 scs_5I2 (i MOD 5) (j  MOD 5)| scs_diag 5 (i MOD 5) (j  MOD 5) }`,
1125  ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(5=0)`;]
1126 THEN MRESAL_TAC STAB_MOD[`scs_5I2`][SCS_5I2_IS_SCS;K_SCS_5I2]);;
1127
1128
1129 let SET_STAB_5I3=prove(`{ scs_stab_diag_v39 scs_5I3 i j| scs_diag 5 i j }= { scs_stab_diag_v39 scs_5I3 (i MOD 5) (j  MOD 5)| scs_diag 5 (i MOD 5) (j  MOD 5) }`,
1130  ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(5=0)`;]
1131 THEN MRESAL_TAC STAB_MOD[`scs_5I3`][SCS_5I3_IS_SCS;K_SCS_5I3]);;
1132
1133
1134 let SET_STAB_5M1=prove(`{ scs_stab_diag_v39 scs_5M1 i j| scs_diag 5 i j }= { scs_stab_diag_v39 scs_5M1 (i MOD 5) (j  MOD 5)| scs_diag 5 (i MOD 5) (j  MOD 5) }`,
1135  ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(5=0)`;]
1136 THEN MRESAL_TAC STAB_MOD[`scs_5M1`][SCS_5M1_IS_SCS;K_SCS_5M1]);;
1137
1138
1139 let SET_EQ_DIAG_STAB_5I1=prove( `scs_arrow_v39 { scs_stab_diag_v39 scs_5I1 i j| scs_diag 5 i j }
1140 { scs_stab_diag_v39 scs_5I1 0 2}`,
1141 ONCE_REWRITE_TAC[SET_STAB_5I1]
1142 THEN REWRITE_TAC[DIAG_EQ_ADD5;EXPAND_STAB_DIAG_5I1]
1143 THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_5I1_02;]);;
1144
1145
1146 let SET_EQ_DIAG_STAB_5I2=prove( `scs_arrow_v39 { scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j }
1147 { scs_stab_diag_v39 scs_5I2 0 2}`,
1148 ONCE_REWRITE_TAC[SET_STAB_5I2]
1149 THEN REWRITE_TAC[DIAG_EQ_ADD5;EXPAND_STAB_DIAG_5I2]
1150 THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_5I2_02;]);;
1151
1152
1153
1154 let OTMTOTJ1= prove(`scs_arrow_v39 { scs_5I1 } { scs_stab_diag_v39 scs_5I1 0 2 , scs_5M2 }`,
1155 MATCH_MP_TAC FZIOTEF_TRANS
1156 THEN EXISTS_TAC`({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I1 i j| scs_diag 5 i j })`
1157 THEN ASM_SIMP_TAC[SCS_5I1_BERAK_BY_CSTAB]
1158 THEN REWRITE_TAC[SET_RULE`{A,B}={B} UNION {A}`]
1159 THEN MATCH_MP_TAC FZIOTEF_UNION
1160 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_5I1]
1161 THEN MATCH_MP_TAC FZIOTEF_REFL
1162 THEN REWRITE_TAC[IN_SING]
1163 THEN REPEAT RESA_TAC
1164 THEN ASM_REWRITE_TAC[SCS_5M2_IS_SCS]);;
1165
1166
1167 let OTMTOTJ2= prove(`scs_arrow_v39 { scs_5I2 } { scs_stab_diag_v39 scs_5I2 0 2 , scs_5M2 }`,
1168 MATCH_MP_TAC FZIOTEF_TRANS
1169 THEN EXISTS_TAC`({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j })`
1170 THEN ASM_SIMP_TAC[SCS_5I2_BERAK_BY_CSTAB]
1171 THEN REWRITE_TAC[SET_RULE`{A,B}={B} UNION {A}`]
1172 THEN MATCH_MP_TAC FZIOTEF_UNION
1173 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_5I2]
1174 THEN MATCH_MP_TAC FZIOTEF_REFL
1175 THEN REWRITE_TAC[IN_SING]
1176 THEN REPEAT RESA_TAC
1177 THEN ASM_REWRITE_TAC[SCS_5M2_IS_SCS]);;
1178
1179 (*************************)
1180
1181
1182 let BB_5I3_IS_BB_5M1=prove( ` BBs_v39 (scs_stab_diag_v39 scs_5I3 i j) v==> BBs_v39 (scs_stab_diag_v39 scs_5M1 i j) v`,
1183 REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`]
1184 THEN SCS_TAC
1185 THEN REPEAT RESA_TAC
1186 THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
1187 THEN RESA_TAC
1188 THEN THAYTHE_TAC 2[`i'`;`j'`]
1189 THEN DICH_TAC 0
1190 THEN MP_TAC sqrt8_LE_CSTAB
1191 THEN REWRITE_TAC[h0;cstab]
1192 THEN REAL_ARITH_TAC);;
1193
1194 (***********SCS_BAISC************)
1195
1196
1197 let STAB_5I3_SCS=prove(` scs_diag (scs_k_v39 scs_5I3) i j
1198 ==> is_scs_v39 (scs_stab_diag_v39 scs_5I3 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5I3 i j)`,
1199 STRIP_TAC
1200 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
1201 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5I3_IS_SCS;SCS_5I3_BASIC;K_SCS_5I3;
1202 ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_5I3;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
1203 THEN SCS_TAC
1204 THEN REAL_ARITH_TAC);;
1205
1206
1207
1208 let STAB_5I2_SCS=prove(` scs_diag (scs_k_v39 scs_5I2) i j
1209 ==> is_scs_v39 (scs_stab_diag_v39 scs_5I2 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5I2 i j)`,
1210 STRIP_TAC
1211 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
1212 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5I2_IS_SCS;SCS_5I2_BASIC;K_SCS_5I2;
1213 ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_5I3;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
1214 THEN SCS_TAC
1215 THEN MP_TAC sqrt8_LE_CSTAB
1216 THEN REAL_ARITH_TAC);;
1217
1218
1219
1220
1221 let STAB_5M1_SCS=prove(` scs_diag (scs_k_v39 scs_5M1) i j
1222 ==> is_scs_v39 (scs_stab_diag_v39 scs_5M1 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5M1 i j)`,
1223 STRIP_TAC
1224 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
1225 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5M1_IS_SCS;SCS_5M1_BASIC;K_SCS_5M1;
1226 ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_5I3;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
1227 THEN SCS_TAC
1228 THEN REWRITE_TAC[h0]
1229 THEN REAL_ARITH_TAC);;
1230
1231 let STAB_5M2_SCS=prove(` scs_diag (scs_k_v39 scs_5M2) i j
1232 ==> is_scs_v39 (scs_stab_diag_v39 scs_5M2 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5M2 i j)`,
1233 STRIP_TAC
1234 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
1235 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5M2_IS_SCS;SCS_5M2_BASIC;K_SCS_5M2;
1236 ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_5I3;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
1237 THEN SCS_TAC
1238 THEN REWRITE_TAC[h0;cstab]
1239 THEN REAL_ARITH_TAC);;
1240
1241
1242
1243 (*****************)
1244
1245
1246 let MM_5I3_IMP_MM_5M1=prove(`scs_diag 5 i j /\ MMs_v39 (scs_stab_diag_v39 scs_5I3 i j) v ==> ~(MMs_v39 ((scs_stab_diag_v39 scs_5M1 i j)) ={})`,
1247 STRIP_TAC
1248 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
1249 THEN EXISTS_TAC`v:num->real^3`
1250 THEN EXISTS_TAC`(scs_stab_diag_v39 scs_5I3 i j)`
1251 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`(scs_stab_diag_v39 scs_5I3 i j)`;`v`]
1252 THEN ASSUME_TAC SCS_5M1_BASIC
1253 THEN ASSUME_TAC K_SCS_5M1
1254 THEN ASM_SIMP_TAC[BB_5I3_IS_BB_5M1;IN;SCS_5M1_IS_SCS;SCS_K_D_A_STAB_EQ;K_SCS_5I3;STAB_5M1_SCS;STAB_5I3_SCS]
1255 THEN SCS_TAC
1256 THEN REAL_ARITH_TAC);;
1257
1258
1259 let STAB_5I3_ARROW_STAB_5M1=prove_by_refinement(`scs_diag 5 i j
1260 ==> scs_arrow_v39 { scs_stab_diag_v39 scs_5I3 i j} { scs_stab_diag_v39 scs_5M1 i j}`,
1261 [
1262 STRIP_TAC
1263 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
1264 THEN ABBREV_TAC`k=scs_k_v39 s`
1265 THEN REPEAT RESA_TAC;
1266
1267 ASM_SIMP_TAC[BB_5I3_IS_BB_5M1;IN;SCS_5M1_IS_SCS;SCS_K_D_A_STAB_EQ;K_SCS_5I3;STAB_5M1_SCS;STAB_5I3_SCS;K_SCS_5M1];
1268
1269 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_stab_diag_v39 scs_5I3 i j==> MMs_v39 s = {}) \/ ~((!s. s = scs_stab_diag_v39 scs_5I3 i j ==> MMs_v39 s = {}))`);
1270
1271 ASM_REWRITE_TAC[];
1272
1273
1274 ASM_REWRITE_TAC[]
1275 THEN POP_ASSUM MP_TAC
1276 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
1277 THEN REPEAT STRIP_TAC
1278 THEN POP_ASSUM MP_TAC
1279 THEN RESA_TAC
1280 THEN POP_ASSUM MP_TAC
1281 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1282 THEN STRIP_TAC
1283 THEN EXISTS_TAC`scs_stab_diag_v39 scs_5M1 i j`
1284 THEN ASM_REWRITE_TAC[]
1285 THEN MP_TAC MM_5I3_IMP_MM_5M1
1286 THEN RESA_TAC
1287 THEN POP_ASSUM MP_TAC
1288 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1289 THEN STRIP_TAC
1290 THEN MATCH_DICH_TAC 0
1291 THEN REPEAT STRIP_TAC]);;
1292
1293
1294 let h0_EQ_B_SCS_5M2=prove(`(!i j. scs_diag 5 i j ==> scs_b_v39 scs_5M2 i j= &6)
1295 /\ (!i j. scs_diag 5 i j ==>  scs_a_v39 scs_5M2 i j= cstab)`,
1296 SCS_TAC
1297 THEN REWRITE_TAC[h0;scs_diag;cstab]
1298 THEN REPEAT RESA_TAC
1299 THEN MP_TAC DIAG_5_EQU_PSORT
1300 THEN RESA_TAC
1301 THEN REWRITE_TAC[PAIR_EQ]
1302 THEN SCS_TAC);;
1303
1304
1305 let h0_EQ_B_SCS_5M1=prove(`(!i j. scs_diag 5 i j ==> scs_b_v39 scs_5M1 i j= &6)
1306 /\ (!i j. scs_diag 5 i j ==>  scs_a_v39 scs_5M1 i j= &2 * h0)`,
1307 SCS_TAC
1308 THEN REWRITE_TAC[h0;scs_diag;cstab]
1309 THEN REPEAT RESA_TAC
1310 THEN MP_TAC DIAG_5_EQU_PSORT
1311 THEN RESA_TAC
1312 THEN REWRITE_TAC[PAIR_EQ]
1313 THEN SCS_TAC);;
1314
1315
1316
1317 let PROP_OPP_DIAG_5M1_03= prove_by_refinement(`scs_stab_diag_v39 scs_5M1 0 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_5M1 1 3)) 3 `,
1318
1319 [REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; scs_basic;SCS_K_D_A_STAB_EQ;scs_opp_v39]
1320 THEN MATCH_MP_TAC scs_inj
1321 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_5M1_BASIC]
1322 THEN STRIP_TAC;
1323
1324 MRESAL_TAC  STAB_5M1_SCS[`0`;`3`][K_SCS_5M1;scs_diag;ARITH_RULE`~(0 MOD 5 = 3 MOD 5) /\
1325       ~(SUC 0 MOD 5 = 3 MOD 5) /\
1326       ~(0 MOD 5 = SUC 3 MOD 5)`];
1327
1328 STRIP_TAC;
1329
1330 ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M1;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM]
1331 THEN SET_TAC[];
1332
1333 STRIP_TAC
1334 THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M1;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;]
1335 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
1336 THEN REPEAT GEN_TAC
1337 THEN ASSUME_TAC (ARITH_RULE`~(5=0)`)
1338 THEN MRESA_TAC PSORT_MOD[`5`;`x`;`x'`]
1339 THEN SYM_ASSUM_TAC
1340 THEN MRESA_TAC MOD_ADD_MOD[`3`;`x`;`5`]
1341 THEN MRESA_TAC MOD_ADD_MOD[`3`;`x'`;`5`]
1342 THEN SYM_ASSUM_TAC
1343 THEN SYM_ASSUM_TAC
1344 THEN MP_TAC(ARITH_RULE`x MOD 5<5==> x MOD 5=0\/ x MOD 5=1\/ x MOD 5=2\/ x MOD 5=3\/x MOD 5=4`)
1345 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
1346 THEN RESA_TAC
1347 THEN MP_TAC(ARITH_RULE`x' MOD 5<5==> x' MOD 5=0\/ x' MOD 5=1\/ x' MOD 5=2\/ x' MOD 5=3\/x' MOD 5=4`)
1348 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
1349 THEN RESA_TAC
1350 THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;ARITH_RULE`5-1=4/\ 5-2=3/\ 5-3=2/\ 5-4=1/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6
1351 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ]]);;
1352
1353
1354
1355 let PROP_OPP_DIAG_5M1_02= prove_by_refinement(`scs_stab_diag_v39 scs_5M1 0 2= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_5M1 1 4)) 3 `,
1356
1357 [REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; scs_basic;SCS_K_D_A_STAB_EQ;scs_opp_v39]
1358 THEN MATCH_MP_TAC scs_inj
1359 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_5M1_BASIC]
1360 THEN STRIP_TAC;
1361
1362 MRESAL_TAC  STAB_5M1_SCS[`0`;`2`][K_SCS_5M1;scs_diag;ARITH_RULE`~(0 MOD 5 = 2 MOD 5) /\
1363       ~(SUC 0 MOD 5 = 2 MOD 5) /\
1364       ~(0 MOD 5 = SUC 2 MOD 5)`];
1365
1366 STRIP_TAC;
1367
1368 ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M1;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM]
1369 THEN SET_TAC[];
1370
1371 STRIP_TAC
1372 THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M1;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;]
1373 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
1374 THEN REPEAT GEN_TAC
1375 THEN ASSUME_TAC (ARITH_RULE`~(5=0)`)
1376 THEN MRESA_TAC PSORT_MOD[`5`;`x`;`x'`]
1377 THEN SYM_ASSUM_TAC
1378 THEN MRESA_TAC MOD_ADD_MOD[`3`;`x`;`5`]
1379 THEN MRESA_TAC MOD_ADD_MOD[`3`;`x'`;`5`]
1380 THEN SYM_ASSUM_TAC
1381 THEN SYM_ASSUM_TAC
1382 THEN MP_TAC(ARITH_RULE`x MOD 5<5==> x MOD 5=0\/ x MOD 5=1\/ x MOD 5=2\/ x MOD 5=3\/x MOD 5=4`)
1383 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
1384 THEN RESA_TAC
1385 THEN MP_TAC(ARITH_RULE`x' MOD 5<5==> x' MOD 5=0\/ x' MOD 5=1\/ x' MOD 5=2\/ x' MOD 5=3\/x' MOD 5=4`)
1386 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
1387 THEN RESA_TAC
1388 THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;ARITH_RULE`5-1=4/\ 5-2=3/\ 5-3=2/\ 5-4=1/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6
1389 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ]]);;
1390
1391
1392
1393 let STAB_5I3_ARROW_STAB_5M1_DIAG=prove( `scs_arrow_v39 {scs_stab_diag_v39 scs_5I3 i j | scs_diag 5 i j}
1394  {scs_stab_diag_v39 scs_5M1 i j | scs_diag 5 i j}`,
1395 ONCE_REWRITE_TAC[SET_STAB_5I3]
1396 THEN ONCE_REWRITE_TAC[SET_STAB_5M1]
1397 THEN REWRITE_TAC[DIAG_EQ_ADD5;EXPAND_STAB_DIAG_5I3;EXPAND_STAB_DIAG_5M1]
1398 THEN REWRITE_TAC[ARITH_RULE`i<5<=> i=0\/i=1\/i=2\/i=3\/i=4`;SET_RULE`{scs_stab_diag_v39 scs_5I3 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
1399 =
1400 {scs_stab_diag_v39 scs_5I3 (0 + 2) 0} UNION
1401 {scs_stab_diag_v39 scs_5I3 (1 + 2) 1} UNION
1402 {scs_stab_diag_v39 scs_5I3 (2 + 2) 2} UNION
1403 {scs_stab_diag_v39 scs_5I3 (3 + 2) 3} UNION
1404 {scs_stab_diag_v39 scs_5I3 (4 + 2) 4}
1405 `;SET_RULE`{scs_stab_diag_v39 scs_5M1 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
1406 =
1407 {scs_stab_diag_v39 scs_5M1 (0 + 2) 0} UNION
1408 {scs_stab_diag_v39 scs_5M1 (1 + 2) 1} UNION
1409 {scs_stab_diag_v39 scs_5M1 (2 + 2) 2} UNION
1410 {scs_stab_diag_v39 scs_5M1 (3 + 2) 3} UNION
1411 {scs_stab_diag_v39 scs_5M1 (4 + 2) 4}
1412 `;]
1413 THEN REPEAT(MATCH_MP_TAC FZIOTEF_UNION
1414 THEN STRIP_TAC
1415 THENL[MATCH_MP_TAC STAB_5I3_ARROW_STAB_5M1
1416 THEN REWRITE_TAC[scs_diag;ARITH_RULE`3+2=5/\ 2+2=4`]
1417 THEN SCS_TAC;
1418 ALL_TAC])
1419 THEN MATCH_MP_TAC STAB_5I3_ARROW_STAB_5M1
1420 THEN REWRITE_TAC[scs_diag;ARITH_RULE`4+2=6/\ 7 MOD 5=2`]
1421 THEN SCS_TAC
1422 THEN REWRITE_TAC[scs_diag;ARITH_RULE`4+2=6/\ 7 MOD 5=2/\ ~(2=4)`]);;
1423
1424
1425
1426
1427 let SET_EQ_DIAG_STAB_5M1= prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M1 i j | scs_diag 5 i j}
1428  {scs_stab_diag_v39 scs_5M1 0 2, scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39
1429                                                                 scs_5M1
1430                                                                 2
1431                                                                 4}`,
1432 [
1433 ONCE_REWRITE_TAC[SET_STAB_5M1]
1434 THEN REWRITE_TAC[DIAG_EQ_ADD5;EXPAND_STAB_DIAG_5I3;EXPAND_STAB_DIAG_5M1]
1435 THEN REWRITE_TAC[ARITH_RULE`i<5<=> i=0\/i=1\/i=2\/i=3\/i=4`;
1436 SET_RULE`{A,B,C}
1437 =
1438 {A}UNION
1439 {B}UNION
1440 {C}UNION
1441 {B}UNION
1442 {A}
1443 `;SET_RULE`{scs_stab_diag_v39 scs_5M1 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
1444 =
1445 {scs_stab_diag_v39 scs_5M1 (0 + 2) 0} UNION
1446 {scs_stab_diag_v39 scs_5M1 (1 + 2) 1} UNION
1447 {scs_stab_diag_v39 scs_5M1 (2 + 2) 2} UNION
1448 {scs_stab_diag_v39 scs_5M1 (3 + 2) 3} UNION
1449 {scs_stab_diag_v39 scs_5M1 (4 + 2) 4}
1450 `;]
1451 THEN MATCH_MP_TAC FZIOTEF_UNION
1452 THEN STRIP_TAC;
1453
1454 REWRITE_TAC[ARITH_RULE`0+2=2`;STAB_SYM]
1455 THEN MATCH_MP_TAC FZIOTEF_REFL
1456 THEN REWRITE_TAC[IN_SING]
1457 THEN REPEAT RESA_TAC
1458 THEN MRESAL_TAC  STAB_5M1_SCS[`2`;`0`][scs_diag;K_SCS_5M1;ARITH_RULE`~(2 MOD 5 = 0 MOD 5) /\
1459       ~(SUC 2 MOD 5 = 0 MOD 5) /\
1460       ~(2 MOD 5 = SUC 0 MOD 5)`];
1461
1462 MATCH_MP_TAC FZIOTEF_UNION
1463 THEN STRIP_TAC;
1464
1465 REWRITE_TAC[ARITH_RULE`1+2=3`;STAB_SYM;PROP_OPP_DIAG_5M1_03]
1466 THEN MATCH_MP_TAC FZIOTEF_TRANS
1467 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_5M1 1 3)}`
1468 THEN STRIP_TAC;
1469
1470 MATCH_MP_TAC (GEN_ALL YXIONXL2)
1471 THEN EXISTS_TAC`5`
1472 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(5<=3)`;K_SCS_5M1]
1473 THEN MRESAL_TAC  STAB_5M1_SCS[`1`;`3`][scs_diag;K_SCS_5M1;ARITH_RULE`~(1 MOD 5 = 3 MOD 5) /\
1474       ~(SUC 1 MOD 5 = 3 MOD 5) /\
1475       ~(1 MOD 5 = SUC 3 MOD 5)`];
1476
1477 MATCH_MP_TAC(GEN_ALL YXIONXL3)
1478 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
1479 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_5M1 1 3)`
1480 THEN MRESAL_TAC  STAB_5M1_SCS[`1`;`3`][scs_diag;K_SCS_5M1;ARITH_RULE`~(1 MOD 5 = 3 MOD 5) /\
1481       ~(SUC 1 MOD 5 = 3 MOD 5) /\
1482       ~(1 MOD 5 = SUC 3 MOD 5)`];
1483
1484 MATCH_MP_TAC FZIOTEF_UNION
1485 THEN STRIP_TAC;
1486
1487 REWRITE_TAC[ARITH_RULE`2+2=4`;STAB_SYM]
1488 THEN MATCH_MP_TAC FZIOTEF_REFL
1489 THEN REWRITE_TAC[IN_SING]
1490 THEN REPEAT RESA_TAC
1491 THEN MRESAL_TAC  STAB_5M1_SCS[`2`;`4`][scs_diag;K_SCS_5M1;ARITH_RULE`~(2 MOD 5 = 4 MOD 5) /\
1492       ~(SUC 2 MOD 5 = 4 MOD 5) /\
1493       ~(2 MOD 5 = SUC 4 MOD 5)`];
1494
1495 MATCH_MP_TAC FZIOTEF_UNION
1496 THEN STRIP_TAC;
1497
1498 REWRITE_TAC[ARITH_RULE`3+2=5`;STAB_SYM]
1499 THEN MRESAL_TAC STAB_MOD[`scs_5M1`;`5`;`3`][SCS_5M1_IS_SCS;K_SCS_5M1;ARITH_RULE`5 MOD 5=0/\ 3 MOD 5=3`]
1500 THEN SYM_ASSUM_TAC
1501 THEN REWRITE_TAC[ARITH_RULE`3+2=5`;STAB_SYM]
1502 THEN MATCH_MP_TAC FZIOTEF_REFL
1503 THEN REWRITE_TAC[IN_SING]
1504 THEN REPEAT RESA_TAC
1505 THEN MRESAL_TAC  STAB_5M1_SCS[`3`;`0`][scs_diag;K_SCS_5M1;ARITH_RULE`~(3 MOD 5 = 0 MOD 5) /\
1506       ~(SUC 3 MOD 5 = 0 MOD 5) /\
1507       ~(3 MOD 5 = SUC 0 MOD 5)`];
1508
1509 REWRITE_TAC[ARITH_RULE`4+2=6`;]
1510 THEN MRESAL_TAC STAB_MOD[`scs_5M1`;`6`;`4`][SCS_5M1_IS_SCS;K_SCS_5M1;ARITH_RULE`6 MOD 5=1/\ 4 MOD 5=4`]
1511 THEN SYM_ASSUM_TAC
1512 THEN REWRITE_TAC[PROP_OPP_DIAG_5M1_02];
1513
1514 MATCH_MP_TAC FZIOTEF_TRANS
1515 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_5M1 1 4)}`
1516 THEN STRIP_TAC;
1517
1518 MATCH_MP_TAC (GEN_ALL YXIONXL2)
1519 THEN EXISTS_TAC`5`
1520 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(5<=3)`;K_SCS_5M1]
1521 THEN MRESAL_TAC  STAB_5M1_SCS[`1`;`4`][scs_diag;K_SCS_5M1;ARITH_RULE`~(1 MOD 5 = 4 MOD 5) /\
1522       ~(SUC 1 MOD 5 = 4 MOD 5) /\
1523       ~(1 MOD 5 = SUC 4 MOD 5)`];
1524
1525 MATCH_MP_TAC(GEN_ALL YXIONXL3)
1526 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
1527 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_5M1 1 4)`
1528 THEN MRESAL_TAC  STAB_5M1_SCS[`1`;`4`][scs_diag;K_SCS_5M1;ARITH_RULE`~(1 MOD 5 = 4 MOD 5) /\
1529       ~(SUC 1 MOD 5 = 4 MOD 5) /\
1530       ~(1 MOD 5 = SUC 4 MOD 5)`]]);;
1531
1532 let OTMTOTJ3= prove_by_refinement(`scs_arrow_v39 { scs_5I3 } { scs_stab_diag_v39 scs_5M1 0 2 ,     scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4, scs_5M2 }`,
1533
1534 [MATCH_MP_TAC FZIOTEF_TRANS
1535 THEN EXISTS_TAC`({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I3 i j| scs_diag 5 i j })`
1536 THEN ASM_SIMP_TAC[SCS_5I3_BERAK_BY_CSTAB;SET_RULE`{A,B,C,D}={D} UNION {A,B,C}`]
1537 THEN MATCH_MP_TAC FZIOTEF_UNION
1538 THEN STRIP_TAC;
1539
1540 MATCH_MP_TAC FZIOTEF_REFL
1541 THEN REWRITE_TAC[IN_SING]
1542 THEN REPEAT RESA_TAC
1543 THEN ASM_REWRITE_TAC[SCS_5M2_IS_SCS];
1544
1545 MATCH_MP_TAC FZIOTEF_TRANS
1546 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_5M1 i j | scs_diag 5 i j}`
1547 THEN ASM_REWRITE_TAC[STAB_5I3_ARROW_STAB_5M1_DIAG];
1548
1549 ASM_SIMP_TAC[SET_EQ_DIAG_STAB_5M1]]);;
1550
1551
1552 let OTMTOTJ4= prove(`scs_arrow_v39 { scs_5M1 } { scs_stab_diag_v39 scs_5M1 0 2 ,     scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4, scs_5M2 }`,
1553 MATCH_MP_TAC FZIOTEF_TRANS
1554 THEN EXISTS_TAC`({ scs_5M2}UNION { scs_stab_diag_v39 scs_5M1 i j| scs_diag 5 i j })`
1555 THEN ASM_SIMP_TAC[SCS_5M1_BERAK_BY_CSTAB;SET_RULE`{A,B,C,D}={D} UNION {A,B,C}`]
1556 THEN MATCH_MP_TAC FZIOTEF_UNION
1557 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_5M1]
1558 THEN MATCH_MP_TAC FZIOTEF_REFL
1559 THEN REWRITE_TAC[IN_SING]
1560 THEN REPEAT RESA_TAC
1561 THEN ASM_REWRITE_TAC[SCS_5M2_IS_SCS]);;
1562
1563
1564  end;;
1565
1566
1567 (*
1568 let check_completeness_claimA_concl =
1569   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
1570 *)
1571
1572
1573
1574