text_formalization/local/MIQMCSN.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 Miqmcsn = 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 open Aueaheh;;
  98 open Vasyyau;;
  99
 100
 101
 102 (**************************************************)
 103
 104   let scs_3T4_prime2 = (* terminal_tri_6833979866 =  *) new_definition
 105     `scs_3T4_prime2 = mk_unadorned_v39  3
 106     (#0.2759)
 107     (funlist_v39 [(0,1),(&2);(0,2),cstab] (&2*h0) 3)
 108     (funlist_v39 [(0,1),(&2 * h0)] (cstab) 3)`;;
 109
 110
 111
 112
 113   let scs_3T3_prime = (* terminal_tri_6833979866 =  *) new_definition
 114     `scs_3T3_prime = mk_unadorned_v39  3
 115     (#0.476)
 116     (funlist_v39 [(0,1),cstab] (&2*h0) 3)
 117     (funlist_v39 [] (cstab) 3)`;;
 118
 119
 120
 121
 122 let scs_3M1_prime = new_definition
 123     `scs_3M1_prime = mk_unadorned_v39 3 (#0.103)
 124     (funlist_v39 [(0,1),(cstab)] (&2) 3)
 125     (funlist_v39 [(0,1),(cstab)] (&2 * h0) 3)`;;
 126
 127
 128
 129   let scs_4M8_02 = new_definition
 130     `scs_4M8_02 = mk_unadorned_v39 4 (#0.513)
 131     (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(cstab);(1,3),(cstab)] (&2) 4)
 132     (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(#3.62);(1,3),(&6)] (&2) 4)`;;
 133
 134
 135   let scs_4M8_13 = new_definition
 136     `scs_4M8_13 = mk_unadorned_v39 4 (#0.513)
 137     (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(cstab);(1,3),(cstab)] (&2) 4)
 138     (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(&6);(1,3),(#3.62)] (&2) 4)`;;
 139
 140
 141
 142 let PSORT_5_EXPLICIT=prove(`
 143 psort 5 (0,0)= (0,0)/\
 144 psort 5 (1,1)= (1,1)/\
 145 psort 5 (2,2)= (2,2)/\
 146 psort 5 (3,3)= (3,3)/\
 147 psort 5 (4,4)= (4,4)/\
 148 psort 5 (0,1)= (0,1)/\
 149 psort 5 (0,2)= (0,2)/\
 150 psort 5 (0,3)= (0,3)/\
 151 psort 5 (0,4)= (0,4)/\
 152 psort 5 (1,0)= (0,1)/\
 153 psort 5 (1,2)= (1,2)/\
 154 psort 5 (1,3)= (1,3)/\
 155 psort 5 (1,4)= (1,4)/\
 156 psort 5 (2,0)= (0,2)/\
 157 psort 5 (2,1)= (1,2)/\
 158 psort 5 (2,3)= (2,3)/\
 159 psort 5 (2,4)= (2,4)/\
 160 psort 5 (3,0)= (0,3)/\
 161 psort 5 (3,1)= (1,3)/\
 162 psort 5 (3,2)= (2,3)/\
 163 psort 5 (3,4)= (3,4)/\
 164 psort 5 (4,0)= (0,4)/\
 165 psort 5 (4,1)= (1,4)/\
 166 psort 5 (4,2)= (2,4)/\
 167 psort 5 (4,3)= (3,4)/\
 168 psort 5 (4,5)= (0,4)/\
 169 psort 5 (3,5)= (0,3)/\
 170 psort 5 (2,5)= (0,2)/\
 171 psort 5 (1,5)= (0,1)/\
 172 psort 5 (5,1)= (0,1)/\
 173 psort 5 (5,2)= (0,2)/\
 174 psort 5 (5,3)= (0,3)/\
 175 psort 5 (5,4)= (0,4)/\
 176 psort 5 (5,5)= (0,0)/\
 177 psort 5 (5,6)= (0,1)/\
 178 psort 5 (5,7)= (0,2)/\
 179 psort 5 (4,6)= (1,4)/\
 180 psort 5 (6,4)= (1,4)/\
 181 psort 5 (6,5)= (0,1)/\
 182 psort 5 (6,7)= (1,2)/\
 183 psort 5 (7,5)= (0,2)/\
 184 psort 5 (7,6)= (1,2)/\
 185 psort 5 (7,7)= (2,2)/\
 186 psort 5 (6,6)= (1,1)/\
 187 psort 4 (3,4)= (0,3)/\
 188 psort 3 (2,0)= (0,2)/\
 189 psort 3 (2,1)= (1,2)/\
 190 psort 3 (1,0)= (0,1)/\
 191 psort 4 (0,0)= (0,0)/\
 192 psort 4 (1,1)= (1,1)/\
 193 psort 4 (2,2)= (2,2)/\
 194 psort 4 (3,3)= (3,3)/\
 195 psort 4 (4,3)= (0,3)/\
 196 psort 4 (4,4)= (0,0)/\
 197 psort 4 (0,2)= (0,2)/\
 198 psort 4 (4,5)= (0,1)/\
 199 psort 4 (5,4)= (0,1)/\
 200 psort 4 (5,5)= (1,1)/\
 201 psort 4 (1,4)= (0,1)/\
 202 psort 4 (2,5)= (1,2)/\
 203 psort 4 (3,6)= (2,3)
 204 `,
 205 REWRITE_TAC[psort;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_4_TAC;LET_DEF;LET_END_DEF;MOD_5_EXPLICIT;ARITH_RULE`0<=a/\ ~(1<= 0)/\ ~(2<=0)/\ ~(3<=0)/\ ~(4<=0)/\a<=a/\ ~(2<=1)/\ ~(3<=2)/\ ~(4<=3)/\ ~(3<=1)/\ ~(4<=1)/\ ~(4<=2)/\ 2<=3/\ 6 MOD 4=2`]);;
 206
 207
 208
 209
 210
 211
 212
 213 let SCS_TAC= ASM_SIMP_TAC[scs_basic;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} j <=> {} i`;periodic2;scs_basic;unadorned_v39;scs_prop_equ_v39;LET_DEF;LET_END_DEF;scs_stab_diag_v39;scs_half_slice_v39;
 214 Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_5_TAC;
 215 scs_5M1;scs_3M1;scs_6I1;scs_3T1;scs_4M2;scs_6M1;scs_6T1;scs_5I1;scs_5I2;scs_5I3;scs_5M2;scs_4M6;scs_3T4;scs_5M3;scs_3T4_prime;scs_4M6_prime;scs_4M7_prime;scs_4M7;scs_3T1_prime;scs_4M8;scs_4M8_prime;scs_5T1;scs_3T5;scs_4M3;scs_3T6;scs_4M4;scs_4M5;scs_4I2;scs_4T1;scs_4T2;scs_4I1;scs_4T4;scs_4I3;scs_3T3;scs_4T5;scs_3T4_prime2;scs_3T3_prime;scs_3M1_prime;scs_4T3;scs_4M8_02;scs_4M8_13;scs_3T7;
 216 Terminal.FUNLIST_EXPLICIT;Yrtafyh.PSORT_PERIODIC;PSORT_5_EXPLICIT;
 217 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/\ 6 MOD 4=2`];;
 218
 219
 220 (********************)
 221
 222 let SCS_4T3_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4T3`,
 223 [SIMP_TAC[scs_4T3;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
 224 THEN REPEAT RESA_TAC;
 225
 226 SCS_TAC
 227 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 228
 229 SCS_TAC
 230 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 231
 232 SCS_TAC
 233 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 234
 235 SCS_TAC
 236 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 237
 238 SCS_TAC
 239 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 240
 241
 242 SCS_TAC
 243 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 244
 245
 246
 247 SCS_TAC
 248 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 249
 250
 251
 252 SCS_TAC
 253 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 254
 255
 256
 257 SCS_TAC
 258 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
 259 THEN RESA_TAC
 260 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 261 THEN REWRITE_TAC[];
 262
 263 SCS_TAC
 264 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
 265 THEN RESA_TAC
 266 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 267 THEN REWRITE_TAC[];
 268
 269 SCS_TAC
 270 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
 271 THEN RESA_TAC
 272 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 273 THEN REWRITE_TAC[];
 274
 275 SCS_TAC
 276 THEN REWRITE_TAC[h0;cstab]
 277 THEN REAL_ARITH_TAC;
 278
 279
 280
 281
 282 SCS_TAC
 283 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
 284 THEN REAL_ARITH_TAC;
 285
 286 SCS_TAC
 287 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
 288 THEN REAL_ARITH_TAC;
 289
 290
 291
 292 POP_ASSUM MP_TAC
 293 THEN ARITH_TAC;
 294
 295
 296
 297 SCS_TAC
 298 THEN ASM_SIMP_TAC[h0;cstab;]
 299 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
 300 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
 301 THEN REAL_ARITH_TAC;
 302
 303
 304
 305
 306 SCS_TAC
 307 THEN ASM_SIMP_TAC[h0;cstab;]
 308 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
 309 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
 310 THEN SUBGOAL_THEN`{i | i < 4 /\
 311       (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2 ) \/
 312        &2 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2))} ={0}`ASSUME_TAC
 313 ;
 314
 315 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`]
 316 THEN GEN_TAC
 317 THEN EQ_TAC
 318 THEN RESA_TAC
 319 THEN POP_ASSUM MP_TAC
 320 THEN ASM_SIMP_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01/\ ~(&2 * #1.26 < &2) `;PSORT_5_EXPLICIT;LT_sqrt8_2h0];
 321
 322
 323 ASM_REWRITE_TAC[Geomdetail.CARD_SING]
 324 THEN ARITH_TAC;
 325 ]);;
 326
 327
 328
 329 let SCS_4M8_02_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M8_02`,
 330 [
 331 SIMP_TAC[scs_4M8_02;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
 332 THEN REPEAT RESA_TAC;
 333
 334 SCS_TAC
 335 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 336
 337 SCS_TAC
 338 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 339
 340 SCS_TAC
 341 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 342
 343 SCS_TAC
 344 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 345
 346 SCS_TAC
 347 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 348
 349
 350 SCS_TAC
 351 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 352
 353
 354
 355 SCS_TAC
 356 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 357
 358
 359
 360 SCS_TAC
 361 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 362
 363
 364
 365 SCS_TAC
 366 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
 367 THEN RESA_TAC
 368 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 369 THEN REWRITE_TAC[];
 370
 371 SCS_TAC
 372 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
 373 THEN RESA_TAC
 374 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 375 THEN REWRITE_TAC[];
 376
 377 SCS_TAC
 378 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
 379 THEN RESA_TAC
 380 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 381 THEN REWRITE_TAC[];
 382
 383 SCS_TAC
 384 THEN REWRITE_TAC[h0;cstab]
 385 THEN REAL_ARITH_TAC;
 386
 387
 388
 389
 390 SCS_TAC
 391 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
 392 THEN REAL_ARITH_TAC;
 393
 394 SCS_TAC
 395 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
 396 THEN REAL_ARITH_TAC;
 397
 398
 399
 400 POP_ASSUM MP_TAC
 401 THEN ARITH_TAC;
 402
 403
 404
 405 SCS_TAC
 406 THEN ASM_SIMP_TAC[h0;cstab;]
 407 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
 408 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
 409 THEN REAL_ARITH_TAC;
 410
 411
 412
 413
 414 SCS_TAC
 415 THEN ASM_SIMP_TAC[h0;cstab;]
 416 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
 417 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
 418 THEN SUBGOAL_THEN`{i | i < 4 /\
 419       (&2 * #1.26 <
 420        (if psort 4 (i,SUC i) = 0,1
 421         then #3.01
 422         else if psort 4 (i,SUC i) = 2,3 then #3.01 else &2) \/
 423        &2 <
 424        (if psort 4 (i,SUC i) = 0,1
 425         then #3.01
 426         else if psort 4 (i,SUC i) = 2,3 then #3.01 else &2))} ={0,2}`ASSUME_TAC
 427 ;
 428
 429 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`;SET_RULE`a IN {b,c}<=>a=b\/ a=c`]
 430 THEN GEN_TAC
 431 THEN EQ_TAC
 432 THEN RESA_TAC
 433 THEN POP_ASSUM MP_TAC
 434 THEN ASM_SIMP_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01/\ ~(&2 * #1.26 < &2) `;PSORT_5_EXPLICIT;LT_sqrt8_2h0;];
 435
 436
 437 ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=2)`]
 438 THEN ARITH_TAC;
 439
 440 ]);;
 441
 442
 443 let SCS_4M8_13_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M8_13`,
 444 [
 445 SIMP_TAC[scs_4M8_13;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
 446 THEN REPEAT RESA_TAC;
 447
 448 SCS_TAC
 449 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 450
 451 SCS_TAC
 452 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 453
 454 SCS_TAC
 455 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 456
 457 SCS_TAC
 458 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 459
 460 SCS_TAC
 461 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 462
 463
 464 SCS_TAC
 465 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 466
 467
 468
 469 SCS_TAC
 470 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 471
 472
 473
 474 SCS_TAC
 475 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 476
 477
 478
 479 SCS_TAC
 480 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
 481 THEN RESA_TAC
 482 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 483 THEN REWRITE_TAC[];
 484
 485 SCS_TAC
 486 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
 487 THEN RESA_TAC
 488 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 489 THEN REWRITE_TAC[];
 490
 491 SCS_TAC
 492 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
 493 THEN RESA_TAC
 494 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 495 THEN REWRITE_TAC[];
 496
 497 SCS_TAC
 498 THEN REWRITE_TAC[h0;cstab]
 499 THEN REAL_ARITH_TAC;
 500
 501
 502
 503
 504 SCS_TAC
 505 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
 506 THEN REAL_ARITH_TAC;
 507
 508 SCS_TAC
 509 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
 510 THEN REAL_ARITH_TAC;
 511
 512
 513
 514 POP_ASSUM MP_TAC
 515 THEN ARITH_TAC;
 516
 517
 518
 519 SCS_TAC
 520 THEN ASM_SIMP_TAC[h0;cstab;]
 521 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
 522 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
 523 THEN REAL_ARITH_TAC;
 524
 525
 526
 527
 528 SCS_TAC
 529 THEN ASM_SIMP_TAC[h0;cstab;]
 530 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
 531 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
 532 THEN SUBGOAL_THEN`{i | i < 4 /\
 533       (&2 * #1.26 <
 534        (if psort 4 (i,SUC i) = 0,1
 535         then #3.01
 536         else if psort 4 (i,SUC i) = 2,3 then #3.01 else &2) \/
 537        &2 <
 538        (if psort 4 (i,SUC i) = 0,1
 539         then #3.01
 540         else if psort 4 (i,SUC i) = 2,3 then #3.01 else &2))} ={0,2}`ASSUME_TAC
 541 ;
 542
 543 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`;SET_RULE`a IN {b,c}<=>a=b\/ a=c`]
 544 THEN GEN_TAC
 545 THEN EQ_TAC
 546 THEN RESA_TAC
 547 THEN POP_ASSUM MP_TAC
 548 THEN ASM_SIMP_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01/\ ~(&2 * #1.26 < &2) `;PSORT_5_EXPLICIT;LT_sqrt8_2h0;];
 549
 550
 551 ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=2)`]
 552 THEN ARITH_TAC;
 553
 554 ]);;
 555
 556
 557
 558 let SCS_3T4_prime2_IS_SCS=prove_by_refinement( `is_scs_v39 scs_3T4_prime2`,
 559 [SIMP_TAC[scs_3T4_prime2;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.2759 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
 560 THEN REPEAT RESA_TAC;
 561
 562 SCS_TAC
 563 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 564
 565 SCS_TAC
 566 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 567
 568 SCS_TAC
 569 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 570
 571 SCS_TAC
 572 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 573
 574 SCS_TAC
 575 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 576
 577 SCS_TAC
 578 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 579
 580 SCS_TAC
 581 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 582
 583 SCS_TAC
 584 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 585
 586 SCS_TAC
 587 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
 588 THEN RESA_TAC
 589 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 590 THEN REWRITE_TAC[];
 591
 592 SCS_TAC
 593 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
 594 THEN RESA_TAC
 595 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 596 THEN REWRITE_TAC[];
 597
 598 SCS_TAC
 599 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
 600 THEN RESA_TAC
 601 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 602 THEN REWRITE_TAC[];
 603
 604 SCS_TAC
 605 THEN REWRITE_TAC[h0;cstab]
 606 THEN REAL_ARITH_TAC;
 607
 608 SCS_TAC;
 609
 610 SCS_TAC
 611 THEN ASM_SIMP_TAC[MOD_LT;h0;cstab]
 612 THEN REAL_ARITH_TAC;
 613
 614 SCS_TAC
 615 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
 616 THEN REAL_ARITH_TAC;
 617
 618 SCS_TAC
 619 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
 620 THEN REAL_ARITH_TAC;
 621
 622 MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
 623       (&2 * h0 < funlist_v39 [(0,1),&2 * h0] cstab 3 i (SUC i) \/
 624        &2 < funlist_v39 [(0,1),&2; (0,2),cstab] (&2 * h0) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`]
 625 THEN MATCH_DICH_TAC 0
 626 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
 627 THEN ARITH_TAC]);;
 628
 629
 630 let SCS_3T3_prime_IS_SCS=prove_by_refinement( `is_scs_v39 scs_3T3_prime`,
 631 [SIMP_TAC[scs_3T3_prime;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.476 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
 632 THEN REPEAT RESA_TAC;
 633
 634 SCS_TAC
 635 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 636
 637 SCS_TAC
 638 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 639
 640 SCS_TAC
 641 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 642
 643 SCS_TAC
 644 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 645
 646 SCS_TAC
 647 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 648
 649 SCS_TAC
 650 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 651
 652 SCS_TAC
 653 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 654
 655 SCS_TAC
 656 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 657
 658 SCS_TAC
 659 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
 660 THEN RESA_TAC
 661 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 662 THEN REWRITE_TAC[];
 663
 664 SCS_TAC
 665 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
 666 THEN RESA_TAC
 667 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 668 THEN REWRITE_TAC[];
 669
 670 SCS_TAC
 671 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
 672 THEN RESA_TAC
 673 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 674 THEN REWRITE_TAC[];
 675
 676 SCS_TAC
 677 THEN REWRITE_TAC[h0;cstab]
 678 THEN REAL_ARITH_TAC;
 679
 680 SCS_TAC;
 681
 682 SCS_TAC
 683 THEN ASM_SIMP_TAC[MOD_LT;h0;cstab]
 684 THEN REAL_ARITH_TAC;
 685
 686 SCS_TAC
 687 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
 688 THEN REAL_ARITH_TAC;
 689
 690 SCS_TAC
 691 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
 692 THEN REAL_ARITH_TAC;
 693
 694 MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
 695       (&2 * h0 < funlist_v39 [] cstab 3 i (SUC i) \/
 696        &2 < funlist_v39 [(0,1),cstab] (&2 * h0) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`]
 697 THEN MATCH_DICH_TAC 0
 698 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
 699 THEN ARITH_TAC;
 700 ]);;
 701
 702
 703 let SCS_3M1_prime_IS_SCS=prove_by_refinement( `is_scs_v39 scs_3M1_prime`,
 704 [SIMP_TAC[scs_3M1_prime;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.103 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
 705 THEN REPEAT RESA_TAC;
 706
 707 SCS_TAC
 708 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 709
 710 SCS_TAC
 711 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 712
 713 SCS_TAC
 714 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 715
 716 SCS_TAC
 717 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 718
 719 SCS_TAC
 720 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 721
 722 SCS_TAC
 723 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 724
 725 SCS_TAC
 726 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 727
 728 SCS_TAC
 729 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 730
 731 SCS_TAC
 732 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
 733 THEN RESA_TAC
 734 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 735 THEN REWRITE_TAC[];
 736
 737 SCS_TAC
 738 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
 739 THEN RESA_TAC
 740 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 741 THEN REWRITE_TAC[];
 742
 743 SCS_TAC
 744 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
 745 THEN RESA_TAC
 746 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 747 THEN REWRITE_TAC[];
 748
 749 SCS_TAC
 750 THEN REWRITE_TAC[h0;cstab]
 751 THEN REAL_ARITH_TAC;
 752
 753 SCS_TAC;
 754
 755 SCS_TAC
 756 THEN ASM_SIMP_TAC[MOD_LT;h0;cstab]
 757 THEN REAL_ARITH_TAC;
 758
 759 SCS_TAC
 760 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
 761 THEN REAL_ARITH_TAC;
 762
 763 SCS_TAC
 764 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
 765 THEN REAL_ARITH_TAC;
 766
 767 MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
 768       (&2 * h0 < funlist_v39 [(0,1),cstab] (&2 * h0) 3 i (SUC i) \/
 769        &2 < funlist_v39 [(0,1),cstab] (&2) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`]
 770 THEN MATCH_DICH_TAC 0
 771 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
 772 THEN ARITH_TAC;
 773 ]);;
 774
 775 let SCS_3T7_IS_SCS=prove_by_refinement( `is_scs_v39 scs_3T7`,
 776 [SIMP_TAC[scs_3T7;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.2565 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
 777 THEN REPEAT RESA_TAC;
 778
 779 SCS_TAC
 780 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 781
 782 SCS_TAC
 783 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 784
 785 SCS_TAC
 786 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 787
 788 SCS_TAC
 789 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 790
 791 SCS_TAC
 792 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 793
 794 SCS_TAC
 795 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 796
 797 SCS_TAC
 798 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 799
 800 SCS_TAC
 801 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 802
 803 SCS_TAC
 804 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
 805 THEN RESA_TAC
 806 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 807 THEN REWRITE_TAC[];
 808
 809 SCS_TAC
 810 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
 811 THEN RESA_TAC
 812 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 813 THEN REWRITE_TAC[];
 814
 815 SCS_TAC
 816 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
 817 THEN RESA_TAC
 818 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 819 THEN REWRITE_TAC[];
 820
 821 SCS_TAC
 822 THEN REWRITE_TAC[h0;cstab]
 823 THEN REAL_ARITH_TAC;
 824
 825 SCS_TAC;
 826
 827 SCS_TAC
 828 THEN ASM_SIMP_TAC[MOD_LT;h0;cstab]
 829 THEN REAL_ARITH_TAC;
 830
 831 SCS_TAC
 832 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
 833 THEN REAL_ARITH_TAC;
 834
 835 DICH_TAC 0
 836 THEN ARITH_TAC;
 837
 838 MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
 839       (&2 * h0 <
 840        funlist_v39 [(0,1),#3.62; (0,2),cstab; (1,2),&2] (&2) 3 i (SUC i) \/
 841        &2 < funlist_v39 [(0,1),cstab; (0,2),cstab; (1,2),&2] (&2) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`]
 842 THEN MATCH_DICH_TAC 0
 843 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
 844 THEN ARITH_TAC;
 845 ]);;
 846
 847 (*********************)
 848
 849
 850 let SCS_3T4_prime2_BASIC=prove(`scs_basic_v39 scs_3T4_prime2`,
 851 SCS_TAC);;
 852
 853 let K_SCS_3T4_prime2=prove(`scs_k_v39 scs_3T4_prime2=3`,
 854 SCS_TAC);;
 855
 856 let J_SCS_3T4_prime2=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T4_prime2 i) i1 j= F`,
 857 SCS_TAC );;
 858
 859 let J_SCS_3T4_prime2_1=prove(`scs_J_v39 (scs_3T4_prime2 ) i1 j= F`,
 860 SCS_TAC );;
 861
 862 let SCS_3T7_BASIC=prove(`scs_basic_v39 scs_3T7`,
 863 SCS_TAC);;
 864
 865 let K_SCS_3T7=prove(`scs_k_v39 scs_3T7=3`,
 866 SCS_TAC);;
 867
 868 let J_SCS_3T7=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T7 i) i1 j= F`,
 869 SCS_TAC );;
 870
 871
 872
 873 let J_SCS_3T7_1=prove(`scs_J_v39 (scs_3T7 ) i1 j= F`,
 874 SCS_TAC );;
 875
 876 let SCS_3T3_prime_BASIC=prove(`scs_basic_v39 scs_3T3_prime`,
 877 SCS_TAC);;
 878
 879 let K_SCS_3T3_prime=prove(`scs_k_v39 scs_3T3_prime=3`,
 880 SCS_TAC);;
 881
 882 let J_SCS_3T3_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T3_prime i) i1 j= F`,
 883 SCS_TAC );;
 884
 885
 886 let SCS_3M1_prime_BASIC=prove(`scs_basic_v39 scs_3M1_prime`,
 887 SCS_TAC);;
 888
 889 let K_SCS_3M1_prime=prove(`scs_k_v39 scs_3M1_prime=3`,
 890 SCS_TAC);;
 891
 892 let J_SCS_3M1_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3M1_prime i) i1 j= F`,
 893 SCS_TAC );;
 894
 895
 896 let SCS_4T3_BASIC=prove(`scs_basic_v39 scs_4T3`,
 897 SCS_TAC);;
 898
 899 let K_SCS_4T3=prove(`scs_k_v39 scs_4T3=4`,
 900 SCS_TAC);;
 901
 902 let J_SCS_4T3=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4T3 i) i1 j= F`,
 903 SCS_TAC );;
 904
 905
 906 let SCS_4M8_02_BASIC=prove(`scs_basic_v39 scs_4M8_02`,
 907 SCS_TAC);;
 908
 909 let K_SCS_4M8_02=prove(`scs_k_v39 scs_4M8_02=4`,
 910 SCS_TAC);;
 911
 912 let J_SCS_4M8_02=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M8_02 i) i1 j= F`,
 913 SCS_TAC );;
 914
 915
 916 let SCS_4M8_13_BASIC=prove(`scs_basic_v39 scs_4M8_13`,
 917 SCS_TAC);;
 918
 919 let K_SCS_4M8_13=prove(`scs_k_v39 scs_4M8_13=4`,
 920 SCS_TAC);;
 921
 922 let J_SCS_4M8_13=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M8_13 i) i1 j= F`,
 923 SCS_TAC );;
 924
 925 (***********************)
 926
 927 let BB_3T4_prime2_IMP_scs_3T4=prove(`BBs_v39 scs_3T4_prime2 v
 928      ==>
 929     BBs_v39 (scs_3T4 ) v`,
 930 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`(3<=3)`;IN;K_SCS_3T4;K_SCS_3T4_prime2;scs_prop_equ_v39;]
 931 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
 932 THEN SCS_TAC
 933 THEN REPEAT RESA_TAC
 934 THEN THAYTHE_TAC 0[`i`;`j`]
 935 THEN DICH_TAC 1
 936 THEN REWRITE_TAC[cstab;h0]
 937 THEN REAL_ARITH_TAC);;
 938
 939
 940 let MM_3T4_prime2_IMP_MM_3T4=prove(`MMs_v39 scs_3T4_prime2 v ==> ~(MMs_v39 scs_3T4={})`,
 941 STRIP_TAC
 942 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
 943 THEN EXISTS_TAC`v:num->real^3`
 944 THEN EXISTS_TAC`scs_3T4_prime2`
 945 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_3T4_prime2`;`v`]
 946 THEN ASM_SIMP_TAC[SCS_3T4_BASIC;SCS_3T4_prime2_BASIC;SCS_3T4_IS_SCS;SCS_3T4_IS_SCS;
 947 SCS_3T4_prime2_IS_SCS;K_SCS_3T4;K_SCS_3T4_prime2;IN;BB_3T4_prime2_IMP_scs_3T4]
 948 THEN SCS_TAC
 949 THEN REAL_ARITH_TAC);;
 950
 951
 952 let SCS_3T4_prime2_ARROW_MM_3T4=prove_by_refinement(`scs_arrow_v39 {scs_3T4_prime2 } { scs_3T4}`,
 953 [ REPEAT GEN_TAC
 954 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
 955 THEN ABBREV_TAC`k=scs_k_v39 s`
 956 THEN REPEAT RESA_TAC;
 957
 958 ASM_SIMP_TAC[SCS_3T4_IS_SCS];
 959
 960 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_3T4_prime2 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_3T4_prime2 ==> MMs_v39 s = {}))`);
 961
 962 ASM_REWRITE_TAC[];
 963
 964 ASM_REWRITE_TAC[]
 965 THEN POP_ASSUM MP_TAC
 966 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
 967 THEN REPEAT STRIP_TAC
 968 THEN POP_ASSUM MP_TAC
 969 THEN RESA_TAC
 970 THEN EXISTS_TAC`scs_3T4`
 971 THEN ASM_REWRITE_TAC[]
 972 THEN MATCH_MP_TAC (GEN_ALL MM_3T4_prime2_IMP_MM_3T4)
 973 THEN POP_ASSUM MP_TAC
 974 THEN SET_TAC[]]);;
 975
 976 (************************************)
 977
 978
 979
 980
 981
 982 let BB_3T3_prime_IMP_scs_3T3=prove(`BBs_v39 scs_3T3_prime v
 983      ==>
 984     BBs_v39 (scs_3T3 ) v`,
 985 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`(3<=3)`;IN;K_SCS_3T4;K_SCS_3T3_prime;scs_prop_equ_v39;]
 986 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
 987 THEN SCS_TAC
 988 THEN REPEAT RESA_TAC
 989 THEN THAYTHE_TAC 0[`i`;`j`]
 990 THEN DICH_TAC 1
 991 THEN REWRITE_TAC[cstab;h0]
 992 THEN REAL_ARITH_TAC);;
 993
 994 let MM_3T3_prime_IMP_MM_3T3=prove(`MMs_v39 scs_3T3_prime v ==> ~(MMs_v39 scs_3T3={})`,
 995 STRIP_TAC
 996 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
 997 THEN EXISTS_TAC`v:num->real^3`
 998 THEN EXISTS_TAC`scs_3T3_prime`
 999 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_3T3_prime`;`v`]
1000 THEN ASM_SIMP_TAC[SCS_3T3_BASIC;SCS_3T3_prime_BASIC;SCS_3T3_IS_SCS;SCS_3T3_IS_SCS;
1001 SCS_3T3_prime_IS_SCS;K_SCS_3T3;K_SCS_3T3_prime;IN;BB_3T3_prime_IMP_scs_3T3]
1002 THEN SCS_TAC
1003 THEN REAL_ARITH_TAC);;
1004
1005 let SCS_3T3_prime_ARROW_MM_3T3=prove_by_refinement(`scs_arrow_v39 {scs_3T3_prime } { scs_3T3}`,
1006 [ REPEAT GEN_TAC
1007 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
1008 THEN ABBREV_TAC`k=scs_k_v39 s`
1009 THEN REPEAT RESA_TAC;
1010
1011 ASM_SIMP_TAC[SCS_3T3_IS_SCS];
1012
1013 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_3T3_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_3T3_prime ==> MMs_v39 s = {}))`);
1014
1015 ASM_REWRITE_TAC[];
1016
1017 ASM_REWRITE_TAC[]
1018 THEN POP_ASSUM MP_TAC
1019 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
1020 THEN REPEAT STRIP_TAC
1021 THEN POP_ASSUM MP_TAC
1022 THEN RESA_TAC
1023 THEN EXISTS_TAC`scs_3T3`
1024 THEN ASM_REWRITE_TAC[]
1025 THEN MATCH_MP_TAC (GEN_ALL MM_3T3_prime_IMP_MM_3T3)
1026 THEN POP_ASSUM MP_TAC
1027 THEN SET_TAC[]]);;
1028
1029 (************************)
1030
1031
1032
1033 let BB_3M1_prime_IMP_scs_3M1=prove(`BBs_v39 scs_3M1_prime v
1034      ==>
1035     BBs_v39 (scs_3M1 ) v`,
1036 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`(3<=3)`;IN;K_SCS_3T4;K_SCS_3M1_prime;scs_prop_equ_v39;]
1037 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
1038 THEN SCS_TAC
1039 THEN REPEAT RESA_TAC
1040 THEN THAYTHE_TAC 0[`i`;`j`]
1041 THEN DICH_TAC 1
1042 THEN REWRITE_TAC[cstab;h0]
1043 THEN REAL_ARITH_TAC);;
1044
1045 let MM_3M1_prime_IMP_MM_3M1=prove(`MMs_v39 scs_3M1_prime v ==> ~(MMs_v39 scs_3M1={})`,
1046 STRIP_TAC
1047 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
1048 THEN EXISTS_TAC`v:num->real^3`
1049 THEN EXISTS_TAC`scs_3M1_prime`
1050 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_3M1_prime`;`v`]
1051 THEN ASM_SIMP_TAC[SCS_3M1_BASIC;SCS_3M1_prime_BASIC;SCS_3M1_IS_SCS;SCS_3M1_IS_SCS;
1052 SCS_3M1_prime_IS_SCS;K_SCS_3M1;K_SCS_3M1_prime;IN;BB_3M1_prime_IMP_scs_3M1]
1053 THEN SCS_TAC
1054 THEN REAL_ARITH_TAC);;
1055
1056 let SCS_3M1_prime_ARROW_MM_3M1=prove_by_refinement(`scs_arrow_v39 {scs_3M1_prime } { scs_3M1}`,
1057 [ REPEAT GEN_TAC
1058 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
1059 THEN ABBREV_TAC`k=scs_k_v39 s`
1060 THEN REPEAT RESA_TAC;
1061
1062 ASM_SIMP_TAC[SCS_3M1_IS_SCS];
1063
1064 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_3M1_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_3M1_prime ==> MMs_v39 s = {}))`);
1065
1066 ASM_REWRITE_TAC[];
1067
1068 ASM_REWRITE_TAC[]
1069 THEN POP_ASSUM MP_TAC
1070 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
1071 THEN REPEAT STRIP_TAC
1072 THEN POP_ASSUM MP_TAC
1073 THEN RESA_TAC
1074 THEN EXISTS_TAC`scs_3M1`
1075 THEN ASM_REWRITE_TAC[]
1076 THEN MATCH_MP_TAC (GEN_ALL MM_3M1_prime_IMP_MM_3M1)
1077 THEN POP_ASSUM MP_TAC
1078 THEN SET_TAC[]]);;
1079
1080
1081 (*************************)
1082
1083
1084
1085
1086 let BB_4M7_IMP_BB_STAN_4M7= prove(`
1087     BBs_v39 scs_4M7 v /\
1088     scs_diag 4 i j /\
1089    dist(v i,v j)<= cstab ==>
1090     BBs_v39 (scs_stab_diag_v39 scs_4M7 i j) v`,
1091 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M7;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M7;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7]
1092 THEN REPEAT RESA_TAC
1093 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
1094 THEN SCS_TAC
1095 THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
1096 THEN RESA_TAC
1097 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
1098 THENL[
1099 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M7;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M7;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7;SCS_4M7_IS_SCS]
1100 THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
1101 THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
1102
1103 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M7;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M7;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7;SCS_4M7_IS_SCS]
1104 THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
1105 THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
1106 THEN ONCE_REWRITE_TAC[DIST_SYM]
1107 THEN ASM_REWRITE_TAC[]]);;
1108
1109
1110 let MM_4M7_IMP_STAB_4M7=prove(`
1111    MMs_v39 scs_4M7 v /\
1112     scs_diag 4 i j /\
1113    dist(v i,v j)<= cstab ==>
1114     ~(MMs_v39 (scs_stab_diag_v39 scs_4M7 i j) ={})`,
1115 STRIP_TAC
1116 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
1117 THEN EXISTS_TAC`v:num->real^3`
1118 THEN EXISTS_TAC` scs_4M7 `
1119 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M7 `;`v`]
1120 THEN ASSUME_TAC SCS_4M7_BASIC
1121 THEN ASSUME_TAC K_SCS_4M7
1122 THEN ASM_SIMP_TAC[SCS_4M7_IS_SCS;SCS_4M7_IS_SCS;SCS_4M7_BASIC;K_SCS_4M7;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M7_13;BB_4M7_IMP_BB_STAN_4M7;STAB_4M7_SCS]
1123 THEN SCS_TAC
1124 THEN REAL_ARITH_TAC);;
1125
1126
1127
1128
1129 let SET_STAB_4M7=prove(`{ scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M7 (i MOD 4) (j  MOD 4)| scs_diag 4 (i MOD 4) (j  MOD 4) }`,
1130  ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
1131 THEN MRESAL_TAC STAB_MOD[`scs_4M7`][SCS_4M7_IS_SCS;K_SCS_4M7]);;
1132
1133 let EXPAND_STAB_DIAG_4M7=prove(`
1134 {scs_stab_diag_v39 scs_4M7 (i MOD 4) (j MOD 4) | j MOD 4 =
1135                                                   (i MOD 4 + 2) MOD 4}=
1136 {scs_stab_diag_v39 scs_4M7 (i+2) i| i<4} `,
1137 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M7_IS_SCS;K_SCS_4M7]);;
1138
1139
1140 let SET_EQ_DIAG_STAB_4M7=prove_by_refinement(`scs_arrow_v39
1141  { scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4M7 0 2,scs_stab_diag_v39 scs_4M7 1 3}`,
1142 [
1143 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M7;SET_STAB_4M7;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
1144 THEN
1145 REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M7 (i + 2) i |i=0\/i=1\/i=2\/i=3}
1146 = {scs_stab_diag_v39 scs_4M7 (0 + 2) 0} UNION
1147 {scs_stab_diag_v39 scs_4M7 (1 + 2) 1} UNION
1148 {scs_stab_diag_v39 scs_4M7 (2 + 2) 2} UNION
1149 {scs_stab_diag_v39 scs_4M7 (3 + 2) 3}
1150 `;]
1151 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M7 0 2,scs_stab_diag_v39 scs_4M7 1 3}={scs_stab_diag_v39 scs_4M7 0 2} UNION {scs_stab_diag_v39 scs_4M7 1 3}UNION {scs_stab_diag_v39 scs_4M7 0 2} UNION {scs_stab_diag_v39 scs_4M7 1 3}`]
1152 THEN MATCH_MP_TAC FZIOTEF_UNION
1153 THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
1154 THEN MRESA_TAC STAB_SYM[`scs_4M7`;`0`;`2`]
1155 THEN STRIP_TAC;
1156
1157 MATCH_MP_TAC FZIOTEF_REFL
1158 THEN REWRITE_TAC[IN_SING]
1159 THEN REPEAT RESA_TAC
1160 THEN ASM_SIMP_TAC[STAB_4M7_SCS;SCS_DIAG_SCS_4M7_02];
1161
1162 MATCH_MP_TAC FZIOTEF_UNION
1163 THEN MRESA_TAC STAB_SYM[`scs_4M7`;`1`;`3`]
1164 THEN STRIP_TAC;
1165
1166 MATCH_MP_TAC FZIOTEF_REFL
1167 THEN REWRITE_TAC[IN_SING]
1168 THEN REPEAT RESA_TAC
1169 THEN ASM_SIMP_TAC[STAB_4M7_SCS;SCS_DIAG_SCS_4M7_13];
1170
1171 MATCH_MP_TAC FZIOTEF_UNION
1172 THEN MRESAL_TAC STAB_MOD[`scs_4M7`;`4`;`2`][SCS_4M7_IS_SCS;K_SCS_4M7;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
1173 THEN SYM_ASSUM_TAC
1174 THEN STRIP_TAC;
1175
1176 MATCH_MP_TAC FZIOTEF_REFL
1177 THEN REWRITE_TAC[IN_SING]
1178 THEN REPEAT RESA_TAC
1179 THEN ASM_SIMP_TAC[STAB_4M7_SCS;SCS_DIAG_SCS_4M7_02];
1180
1181 MRESAL_TAC STAB_MOD[`scs_4M7`;`5`;`3`][SCS_4M7_IS_SCS;K_SCS_4M7;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
1182 THEN SYM_ASSUM_TAC;
1183
1184 MATCH_MP_TAC FZIOTEF_REFL
1185 THEN REWRITE_TAC[IN_SING]
1186 THEN REPEAT RESA_TAC
1187 THEN ASM_SIMP_TAC[STAB_4M7_SCS;SCS_DIAG_SCS_4M7_13]]);;
1188
1189
1190
1191 let SCS_4M7_SLICE_13=prove_by_refinement(
1192 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M7 1 3 } {scs_prop_equ_v39 scs_3T4_prime 2,   scs_3T4_prime2  }`,
1193 [
1194
1195 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
1196 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M7_13;STAB_4M7_SCS;SCS_K_D_A_STAB_EQ;]
1197 THEN EXISTS_TAC`1`
1198 THEN EXISTS_TAC`3`
1199 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M7_13]
1200 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
1201 THEN REPEAT RESA_TAC;
1202
1203 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
1204 THEN STRIP_TAC
1205 THEN MATCH_MP_TAC scs_inj
1206 THEN ASM_SIMP_TAC[SCS_3T4_prime_BASIC;SCS_4M7_BASIC;J_SCS_4M7;BASIC_HALF_SLICE_STAB;J_SCS_3T4_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T4_prime2_BASIC;J_SCS_3T4_prime2]
1207 THEN STRIP_TAC;
1208
1209 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_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7]
1210 THEN ARITH_TAC;
1211
1212 STRIP_TAC
1213 THEN
1214 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_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;
1215 ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
1216 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1217 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1218 THEN SCS_TAC
1219 THEN REPEAT GEN_TAC
1220 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1221 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1222 THEN RESA_TAC
1223 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1224 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1225 THEN RESA_TAC
1226 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1227 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]
1228 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
1229 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
1230 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
1231 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
1232 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
1233 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
1234 THEN ASM_TAC
1235 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/\
1236 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1237 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1238 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1239 THEN REPEAT RESA_TAC
1240 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)
1241 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1242 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1243 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1244 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1245 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1246 THEN SYM_ASSUM_TAC
1247 THEN SCS_TAC;
1248
1249 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_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7]
1250 THEN ARITH_TAC;
1251
1252
1253 STRIP_TAC
1254 THEN
1255 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_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;
1256 ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
1257 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1258 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1259 THEN SCS_TAC
1260 THEN REPEAT GEN_TAC
1261 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1262 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1263 THEN RESA_TAC
1264 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1265 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1266 THEN RESA_TAC
1267 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1268 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]
1269 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
1270 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
1271 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
1272 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
1273 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
1274 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
1275 THEN ASM_TAC
1276 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/\
1277 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1278 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1279 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1280 THEN REPEAT RESA_TAC
1281 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)
1282 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1283 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1284 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1285 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1286 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1287 THEN SYM_ASSUM_TAC
1288 THEN SCS_TAC;
1289
1290
1291 SCS_TAC
1292 THEN REAL_ARITH_TAC;
1293
1294 SCS_TAC
1295 THEN REAL_ARITH_TAC;
1296
1297 SCS_TAC
1298 THEN REAL_ARITH_TAC;
1299
1300 SCS_TAC
1301 THEN REWRITE_TAC[cstab]
1302 THEN REAL_ARITH_TAC;
1303
1304
1305 SCS_TAC
1306 THEN REWRITE_TAC[cstab]
1307 THEN REAL_ARITH_TAC;
1308
1309
1310
1311 POP_ASSUM MP_TAC
1312 THEN REWRITE_TAC[J_SCS_3T4_prime];
1313
1314 ]);;
1315
1316
1317 let SCS_4M7_SLICE_13_ARROW_3T4=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M7 1 3 } { scs_3T4}`,
1318 MATCH_MP_TAC FZIOTEF_TRANS
1319 THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3T4_prime 2,   scs_3T4_prime2  }`
1320 THEN ASM_REWRITE_TAC[SCS_4M7_SLICE_13]
1321 THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}/\ {scs_3T4}= {scs_3T4}UNION {scs_3T4}`]
1322 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}/\ {scs_3T4}= {scs_3T4}UNION {scs_3T4}`]
1323 THEN MATCH_MP_TAC FZIOTEF_UNION
1324 THEN ASM_REWRITE_TAC[SCS_3T4_prime2_ARROW_MM_3T4;SCS_3T4_prime_ARROW_MM_3T4]
1325 THEN MATCH_MP_TAC FZIOTEF_TRANS
1326 THEN EXISTS_TAC`{scs_3T4_prime}`
1327 THEN ASM_REWRITE_TAC[SCS_3T4_prime2_ARROW_MM_3T4;SCS_3T4_prime_ARROW_MM_3T4]
1328 THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T4_prime`;`2`;`3`][SCS_3T4_prime_IS_SCS;K_SCS_3T4_prime;ARITH_RULE`(3 - 2 MOD 3)=1`]
1329 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T4_prime 2`;`1`][PROP_EQU_IS_SCS;SCS_3T4_prime_IS_SCS]
1330 THEN DICH_TAC 0
1331 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1332 THEN REWRITE_TAC[]);;
1333
1334
1335 let SCS_4M7_SLICE_02=prove_by_refinement(
1336 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M7 0 2 } {scs_prop_equ_v39 scs_3T3_prime 1,  scs_prop_equ_v39 scs_3M1_prime 1  }`,
1337 [
1338 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
1339 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M7_02;STAB_4M7_SCS;SCS_K_D_A_STAB_EQ;]
1340 THEN EXISTS_TAC`0`
1341 THEN EXISTS_TAC`2`
1342 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M7_02]
1343 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
1344 THEN REPEAT RESA_TAC;
1345
1346
1347 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
1348 THEN STRIP_TAC
1349 THEN MATCH_MP_TAC scs_inj
1350 THEN ASM_SIMP_TAC[SCS_3T3_prime_BASIC;SCS_4M7_BASIC;J_SCS_4M7;BASIC_HALF_SLICE_STAB;J_SCS_3T3_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3M1_prime_BASIC;J_SCS_3M1_prime]
1351 THEN STRIP_TAC;
1352
1353
1354 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_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7]
1355 THEN ARITH_TAC;
1356
1357 STRIP_TAC
1358 THEN
1359 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_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;
1360 ARITH_RULE`(2 + 1 + 4 - 0) MOD 4= 3/\ 0 MOD 4=0/\ a+0=a`;scs_prop_equ_v39]
1361 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1362 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1363 THEN SCS_TAC
1364 THEN REPEAT GEN_TAC
1365 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1366 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1367 THEN RESA_TAC
1368 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1369 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1370 THEN RESA_TAC
1371 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1372 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]
1373 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
1374 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
1375 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
1376 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
1377 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
1378 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
1379 THEN ASM_TAC
1380 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/\
1381 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1382 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1383 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1384 THEN REPEAT RESA_TAC
1385 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)
1386 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1387 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1388 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1389 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1390 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1391 THEN SYM_ASSUM_TAC
1392 THEN SCS_TAC;
1393
1394 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_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7]
1395 THEN ARITH_TAC;
1396
1397
1398 STRIP_TAC
1399 THEN
1400 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_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;
1401 ARITH_RULE`(0 + 1 + 4 - 2) MOD 4= 3/\ 2 MOD 4=2/\ a+0=a`;scs_prop_equ_v39]
1402 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1403 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1404 THEN SCS_TAC
1405 THEN REPEAT GEN_TAC
1406 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1407 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1408 THEN RESA_TAC
1409 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1410 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1411 THEN RESA_TAC
1412 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1413 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]
1414 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
1415 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
1416 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
1417 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
1418 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
1419 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
1420 THEN ASM_TAC
1421 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/\
1422 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1423 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1424 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1425 THEN REPEAT RESA_TAC
1426 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)
1427 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1428 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1429 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1430 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1431 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1432 THEN SYM_ASSUM_TAC
1433 THEN SCS_TAC;
1434
1435
1436 SCS_TAC
1437 THEN REAL_ARITH_TAC;
1438
1439
1440 SCS_TAC
1441 THEN REAL_ARITH_TAC;
1442
1443 SCS_TAC
1444 THEN REAL_ARITH_TAC;
1445
1446 SCS_TAC
1447 THEN REWRITE_TAC[cstab]
1448 THEN REAL_ARITH_TAC;
1449
1450 SCS_TAC
1451 THEN REWRITE_TAC[cstab]
1452 THEN REAL_ARITH_TAC;
1453
1454
1455
1456 POP_ASSUM MP_TAC
1457 THEN REWRITE_TAC[J_SCS_3T3_prime];
1458
1459 ]);;
1460
1461
1462
1463 let SCS_4M7_SLICE_02_ARROW_3T3_3M1=prove(
1464 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M7 0 2 } { scs_3T3,scs_3M1}`,
1465 MATCH_MP_TAC FZIOTEF_TRANS
1466 THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3T3_prime 1, scs_prop_equ_v39 scs_3M1_prime 1}`
1467 THEN ASM_REWRITE_TAC[SCS_4M7_SLICE_02]
1468 THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`]
1469 THEN MATCH_MP_TAC FZIOTEF_UNION
1470 THEN STRIP_TAC
1471 THENL[
1472
1473 MATCH_MP_TAC FZIOTEF_TRANS
1474 THEN EXISTS_TAC`{scs_3T3_prime}`
1475 THEN ASM_REWRITE_TAC[SCS_3T3_prime_ARROW_MM_3T3]
1476 THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T3_prime`;`1`;`3`][SCS_3T3_prime_IS_SCS;K_SCS_3T3_prime;ARITH_RULE`(3 - 1 MOD 3)=2`]
1477 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T3_prime 1`;`2`][PROP_EQU_IS_SCS;SCS_3T3_prime_IS_SCS]
1478 THEN DICH_TAC 0
1479 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1480 THEN REWRITE_TAC[];
1481
1482 MATCH_MP_TAC FZIOTEF_TRANS
1483 THEN EXISTS_TAC`{scs_3M1_prime}`
1484 THEN ASM_REWRITE_TAC[SCS_3M1_prime_ARROW_MM_3M1]
1485 THEN MRESAS_TAC PRO_EQU_ID1[`scs_3M1_prime`;`1`;`3`][SCS_3M1_prime_IS_SCS;K_SCS_3M1_prime;ARITH_RULE`(3 - 1 MOD 3)=2`]
1486 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1_prime 1`;`2`][PROP_EQU_IS_SCS;SCS_3M1_prime_IS_SCS]
1487 THEN DICH_TAC 0
1488 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1489 THEN REWRITE_TAC[]]);;
1490
1491
1492
1493 let STAB_SCS_4M7_ARROW_3T3_3M1_3T4=prove(
1494 `scs_arrow_v39
1495  { scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j } {scs_3T3,scs_3M1,scs_3T4}`,
1496 MATCH_MP_TAC FZIOTEF_TRANS
1497 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M7 0 2,scs_stab_diag_v39 scs_4M7 1 3}`
1498 THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_4M7;SET_RULE`{A,B}={A}UNION {B}`;SET_RULE`{scs_3T3,scs_3M1,scs_3T4}={scs_3T3,scs_3M1} UNION{scs_3T4}`]
1499 THEN MATCH_MP_TAC FZIOTEF_UNION
1500 THEN ASM_REWRITE_TAC[SCS_4M7_SLICE_13_ARROW_3T4;SET_RULE`{A}UNION{B}={A,B}`;SCS_4M7_SLICE_02_ARROW_3T3_3M1]);;
1501
1502
1503
1504 (***************************)
1505
1506 let BB_4M8_IMP_BB_STAN_4M8= prove(`
1507     BBs_v39 scs_4M8 v /\
1508     scs_diag 4 i j /\
1509    dist(v i,v j)<= cstab ==>
1510     BBs_v39 (scs_stab_diag_v39 scs_4M8 i j) v`,
1511 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8]
1512 THEN REPEAT RESA_TAC
1513 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
1514 THEN SCS_TAC
1515 THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
1516 THEN RESA_TAC
1517 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
1518 THENL[
1519 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8;SCS_4M8_IS_SCS]
1520 THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
1521 THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
1522
1523 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8;SCS_4M8_IS_SCS]
1524 THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
1525 THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
1526 THEN ONCE_REWRITE_TAC[DIST_SYM]
1527 THEN ASM_REWRITE_TAC[]]);;
1528
1529
1530 let MM_4M8_IMP_STAB_4M8=prove(`
1531    MMs_v39 scs_4M8 v /\
1532     scs_diag 4 i j /\
1533    dist(v i,v j)<= cstab ==>
1534     ~(MMs_v39 (scs_stab_diag_v39 scs_4M8 i j) ={})`,
1535 STRIP_TAC
1536 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
1537 THEN EXISTS_TAC`v:num->real^3`
1538 THEN EXISTS_TAC` scs_4M8 `
1539 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8 `;`v`]
1540 THEN ASSUME_TAC SCS_4M8_BASIC
1541 THEN ASSUME_TAC K_SCS_4M8
1542 THEN ASM_SIMP_TAC[SCS_4M8_IS_SCS;SCS_4M8_IS_SCS;SCS_4M8_BASIC;K_SCS_4M8;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M8_13;BB_4M8_IMP_BB_STAN_4M8;STAB_4M8_SCS]
1543 THEN SCS_TAC
1544 THEN REAL_ARITH_TAC);;
1545
1546
1547
1548 let SET_STAB_4M8=prove(`{ scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M8 (i MOD 4) (j  MOD 4)| scs_diag 4 (i MOD 4) (j  MOD 4) }`,
1549  ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
1550 THEN MRESAL_TAC STAB_MOD[`scs_4M8`][SCS_4M8_IS_SCS;K_SCS_4M8]);;
1551
1552 let EXPAND_STAB_DIAG_4M8=prove(`
1553 {scs_stab_diag_v39 scs_4M8 (i MOD 4) (j MOD 4) | j MOD 4 =
1554                                                   (i MOD 4 + 2) MOD 4}=
1555 {scs_stab_diag_v39 scs_4M8 (i+2) i| i<4} `,
1556 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M8_IS_SCS;K_SCS_4M8]);;
1557
1558
1559 let SET_EQ_DIAG_STAB_4M8=prove_by_refinement(`scs_arrow_v39
1560  { scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4M8 0 2,scs_stab_diag_v39 scs_4M8 1 3}`,
1561 [
1562 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M8;SET_STAB_4M8;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
1563 THEN
1564 REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M8 (i + 2) i |i=0\/i=1\/i=2\/i=3}
1565 = {scs_stab_diag_v39 scs_4M8 (0 + 2) 0} UNION
1566 {scs_stab_diag_v39 scs_4M8 (1 + 2) 1} UNION
1567 {scs_stab_diag_v39 scs_4M8 (2 + 2) 2} UNION
1568 {scs_stab_diag_v39 scs_4M8 (3 + 2) 3}
1569 `;]
1570 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M8 0 2,scs_stab_diag_v39 scs_4M8 1 3}={scs_stab_diag_v39 scs_4M8 0 2} UNION {scs_stab_diag_v39 scs_4M8 1 3}UNION {scs_stab_diag_v39 scs_4M8 0 2} UNION {scs_stab_diag_v39 scs_4M8 1 3}`]
1571 THEN MATCH_MP_TAC FZIOTEF_UNION
1572 THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
1573 THEN MRESA_TAC STAB_SYM[`scs_4M8`;`0`;`2`]
1574 THEN STRIP_TAC;
1575
1576 MATCH_MP_TAC FZIOTEF_REFL
1577 THEN REWRITE_TAC[IN_SING]
1578 THEN REPEAT RESA_TAC
1579 THEN ASM_SIMP_TAC[STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02];
1580
1581 MATCH_MP_TAC FZIOTEF_UNION
1582 THEN MRESA_TAC STAB_SYM[`scs_4M8`;`1`;`3`]
1583 THEN STRIP_TAC;
1584
1585 MATCH_MP_TAC FZIOTEF_REFL
1586 THEN REWRITE_TAC[IN_SING]
1587 THEN REPEAT RESA_TAC
1588 THEN ASM_SIMP_TAC[STAB_4M8_SCS;SCS_DIAG_SCS_4M8_13];
1589
1590 MATCH_MP_TAC FZIOTEF_UNION
1591 THEN MRESAL_TAC STAB_MOD[`scs_4M8`;`4`;`2`][SCS_4M8_IS_SCS;K_SCS_4M8;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
1592 THEN SYM_ASSUM_TAC
1593 THEN STRIP_TAC;
1594
1595 MATCH_MP_TAC FZIOTEF_REFL
1596 THEN REWRITE_TAC[IN_SING]
1597 THEN REPEAT RESA_TAC
1598 THEN ASM_SIMP_TAC[STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02];
1599
1600 MRESAL_TAC STAB_MOD[`scs_4M8`;`5`;`3`][SCS_4M8_IS_SCS;K_SCS_4M8;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
1601 THEN SYM_ASSUM_TAC;
1602
1603 MATCH_MP_TAC FZIOTEF_REFL
1604 THEN REWRITE_TAC[IN_SING]
1605 THEN REPEAT RESA_TAC
1606 THEN ASM_SIMP_TAC[STAB_4M8_SCS;SCS_DIAG_SCS_4M8_13]]);;
1607
1608
1609
1610
1611
1612 let PROP_OPP_DIAG_4M8_13= prove_by_refinement(`scs_stab_diag_v39 scs_4M8 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4M8 0 2)) 2 `,
1613 [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]
1614 THEN MATCH_MP_TAC scs_inj
1615 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M8_BASIC;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_13;scs_basic;unadorned_v39;peropp;peropp2]
1616 THEN SCS_TAC
1617 THEN STRIP_TAC;
1618
1619
1620 SET_TAC[];
1621
1622 STRIP_TAC
1623 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;]
1624 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
1625 THEN REPEAT GEN_TAC
1626 THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
1627 THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
1628 THEN SYM_ASSUM_TAC
1629 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
1630 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
1631 THEN SYM_ASSUM_TAC
1632 THEN SYM_ASSUM_TAC
1633 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`)
1634 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
1635 THEN RESA_TAC
1636 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`)
1637 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
1638 THEN RESA_TAC
1639 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
1640 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;
1641
1642
1643
1644
1645
1646 let STAB_4M8_02_ARROW_4M8_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M8 0 2}{scs_stab_diag_v39 scs_4M8 1 3}`,
1647 ASM_SIMP_TAC[PROP_OPP_DIAG_4M8_13]
1648 THEN MATCH_MP_TAC FZIOTEF_TRANS
1649 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4M8 0 2)}`
1650 THEN STRIP_TAC
1651 THENL[
1652 MATCH_MP_TAC (GEN_ALL YXIONXL2)
1653 THEN EXISTS_TAC`4`
1654 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M8;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02]
1655 ;
1656
1657 MATCH_MP_TAC(GEN_ALL YXIONXL3)
1658 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
1659 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4M8 0 2)`
1660 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M8;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02]]);;
1661
1662
1663
1664 let SCS_4M8_SLICE_13=prove_by_refinement(
1665 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M8 1 3 } {scs_3T4_prime2  }`,
1666 [
1667 ONCE_REWRITE_TAC[SET_RULE`{scs_3T4_prime2}={scs_3T4_prime2,    scs_3T4_prime2}`]
1668 THEN MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
1669 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_13;STAB_4M8_SCS;SCS_K_D_A_STAB_EQ;]
1670 THEN EXISTS_TAC`1`
1671 THEN EXISTS_TAC`3`
1672 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_13]
1673 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
1674 THEN REPEAT RESA_TAC;
1675
1676 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
1677 THEN STRIP_TAC
1678 THEN MATCH_MP_TAC scs_inj
1679 THEN ASM_SIMP_TAC[SCS_3T4_prime_BASIC;SCS_4M8_BASIC;J_SCS_4M8;BASIC_HALF_SLICE_STAB;J_SCS_3T4_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T4_prime2_BASIC;J_SCS_3T4_prime2_1]
1680 THEN STRIP_TAC;
1681
1682
1683 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_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8]
1684 THEN ARITH_TAC;
1685
1686 STRIP_TAC
1687 THEN
1688 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_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8;
1689 ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
1690 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1691 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1692 THEN SCS_TAC
1693 THEN REPEAT GEN_TAC
1694 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1695 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1696 THEN RESA_TAC
1697 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1698 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1699 THEN RESA_TAC
1700 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1701 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]
1702 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
1703 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
1704 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
1705 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
1706 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
1707 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
1708 THEN ASM_TAC
1709 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/\
1710 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1711 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1712 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1713 THEN REPEAT RESA_TAC
1714 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)
1715 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1716 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1717 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1718 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1719 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1720 THEN SYM_ASSUM_TAC
1721 THEN SCS_TAC;
1722
1723 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_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8]
1724 THEN ARITH_TAC;
1725
1726
1727 STRIP_TAC
1728 THEN
1729 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_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8;
1730 ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
1731 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1732 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1733 THEN SCS_TAC
1734 THEN REPEAT GEN_TAC
1735 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1736 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1737 THEN RESA_TAC
1738 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1739 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1740 THEN RESA_TAC
1741 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1742 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]
1743 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
1744 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
1745 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
1746 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
1747 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
1748 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
1749 THEN ASM_TAC
1750 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/\
1751 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1752 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1753 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1754 THEN REPEAT RESA_TAC
1755 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)
1756 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1757 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1758 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1759 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1760 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1761 THEN SYM_ASSUM_TAC
1762 THEN SCS_TAC;
1763
1764
1765 SCS_TAC
1766 THEN REAL_ARITH_TAC;
1767
1768 SCS_TAC
1769 THEN REAL_ARITH_TAC;
1770
1771 SCS_TAC
1772 THEN REAL_ARITH_TAC;
1773
1774 SCS_TAC
1775 THEN REWRITE_TAC[cstab]
1776 THEN REAL_ARITH_TAC;
1777
1778
1779 SCS_TAC
1780 THEN REWRITE_TAC[cstab]
1781 THEN REAL_ARITH_TAC;
1782
1783
1784
1785 POP_ASSUM MP_TAC
1786 THEN REWRITE_TAC[J_SCS_3T4_prime2_1];
1787
1788 ]);;
1789
1790
1791
1792
1793 let SCS_4M8_SLICE_13_ARROW_3T4=prove(
1794 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M8 1 3 } { scs_3T4}`,
1795 MATCH_MP_TAC FZIOTEF_TRANS
1796 THEN EXISTS_TAC`{ scs_3T4_prime2  }`
1797 THEN ASM_REWRITE_TAC[SCS_4M8_SLICE_13]
1798 THEN ASM_REWRITE_TAC[SCS_3T4_prime2_ARROW_MM_3T4;SCS_3T4_prime_ARROW_MM_3T4]);;
1799
1800
1801 let SCS_4M8_SLICE_02_ARROW_3T4 =prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_4M8 0 2 } { scs_3T4 }`,
1802 MATCH_MP_TAC FZIOTEF_TRANS
1803 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M8 1 3}`
1804 THEN ASM_SIMP_TAC[STAB_4M8_02_ARROW_4M8_13;SCS_4M8_SLICE_13_ARROW_3T4]);;
1805
1806
1807
1808 let SET_STAB_4M8_ARROW_3T4=prove(`scs_arrow_v39
1809  { scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j } {scs_3T4}`,
1810 ONCE_REWRITE_TAC[SET_RULE`{A}={A,A}`]
1811 THEN MATCH_MP_TAC FZIOTEF_TRANS
1812 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M8 0 2,scs_stab_diag_v39 scs_4M8 1 3}`
1813 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M8;]
1814 THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`;]
1815 THEN MATCH_MP_TAC FZIOTEF_UNION
1816 THEN ASM_SIMP_TAC[SCS_4M8_SLICE_02_ARROW_3T4;SCS_4M8_SLICE_13_ARROW_3T4]);;
1817
1818
1819 (*****************)
1820
1821 let h0_LT_B_SCS_4M6=prove(`
1822 (!i j. scs_diag 4 i j ==> &4 * h0 < scs_b_v39 scs_4M6' i j)
1823 /\ (!i j. scs_diag 4 i j ==> scs_a_v39 scs_4M6' i j <= cstab)`,
1824 SCS_TAC
1825 THEN REWRITE_TAC[h0;SCS_DIAG_4_CASES;cstab]
1826 THEN REPEAT RESA_TAC
1827 THEN ASSUME_TAC(ARITH_RULE`~(4=0)`)
1828 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
1829 THEN SYM_ASSUM_TAC
1830 THEN SCS_TAC
1831 THEN MP_TAC sqrt8_LE_CSTAB
1832 THEN REAL_ARITH_TAC);;
1833
1834 let SCS_4M6_STAND_OR_PRO=prove(`!i. scs_a_v39 scs_4M6' i (i + 1) = &2 /\
1835            scs_b_v39 scs_4M6' i (i + 1) = &2 * h0 \/
1836            scs_a_v39 scs_4M6' i (i + 1) = &2 * h0 /\
1837            scs_b_v39 scs_4M6' i (i + 1) = cstab`,
1838 GEN_TAC
1839 THEN SCS_TAC
1840 THEN SIMP_TAC[GSYM ADD1;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
1841 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`SUC i:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
1842 THEN SYM_ASSUM_TAC
1843 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`4`][ARITH_RULE`1<4`]
1844 THEN SYM_ASSUM_TAC
1845 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`)
1846 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
1847 THEN RESA_TAC
1848 THEN SCS_TAC);;
1849
1850
1851
1852
1853 let SCS_4M6_STAND=prove(`scs_a_v39 scs_4M6' 1 2 = &2/\ scs_a_v39 scs_4M6' 2 3 = &2/\ scs_a_v39 scs_4M6'  3 4 = &2/\ scs_a_v39 scs_4M6' 0 1= &2 * h0
1854 /\ scs_a_v39 scs_4M6' 1 4= &2 * h0
1855 /\ scs_b_v39 scs_4M6' 0 1= cstab`,
1856 SCS_TAC);;
1857
1858
1859 let h0_CSTAB_LT_4=prove(`&2< &2*h0 /\ cstab< &4/\ &2<= &2*h0 /\ cstab<= &4
1860 /\ &2*h0< &4/\ &2< &4 /\ ~(&2 * h0 = &2)`,
1861 REWRITE_TAC[cstab;h0]
1862 THEN REAL_ARITH_TAC);;
1863
1864 let EXTREMAL_SCS_4M6=prove_by_refinement(`main_nonlinear_terminal_v11 ==>
1865 (!v.
1866     MMs_v39 scs_4M6' v /\
1867     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) ==>
1868     dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = &2/\dist (v 3,v 0) = &2
1869 /\ dist (v 0,v 1) = cstab)`,
1870 [
1871 STRIP_TAC
1872 THEN GEN_TAC
1873 THEN STRIP_TAC
1874 THEN ASSUME_TAC(SCS_4M6_IS_SCS)
1875 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M6'`;`v`]
1876 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M6'`]
1877 THEN THAYTHES_TAC 0[`4`;`0`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M6]
1878 THEN MP_TAC PWEIWBZ
1879 THEN RESA_TAC
1880 THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`1`][SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;h0_LT_B_SCS_4M6;SCS_4M6_STAND_OR_PRO;ARITH_RULE`1+1=2`;SCS_4M6_STAND]
1881 THEN MP_TAC PWEIWBZ
1882 THEN RESA_TAC
1883 THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`2`][SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;h0_LT_B_SCS_4M6;SCS_4M6_STAND_OR_PRO;ARITH_RULE`2+1=3`;SCS_4M6_STAND]
1884 THEN MP_TAC PWEIWBZ
1885 THEN RESA_TAC
1886 THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`3`][SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;h0_LT_B_SCS_4M6;SCS_4M6_STAND_OR_PRO;ARITH_RULE`3+1=4`;SCS_4M6_STAND]
1887 THEN ASSUME_TAC SCS_4M6_BASIC
1888 THEN ASSUME_TAC K_SCS_4M6
1889 THEN ASSUME_TAC h0_LT_B_SCS_4M6
1890 THEN ASSUME_TAC SCS_4M6_STAND_OR_PRO
1891 THEN ASSUME_TAC SCS_4M6_STAND
1892 THEN ASSUME_TAC h0_CSTAB_LT_4
1893 THEN MP_TAC (SET_RULE`scs_is_str scs_4M6' v 0\/ ~(scs_is_str scs_4M6' v 0 )`)
1894 THEN RESA_TAC;
1895
1896 MP_TAC VASYYAU
1897 THEN RESA_TAC
1898 THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`0`][ARITH_RULE`0+1=1`]
1899 THEN MP_TAC Bkossge.quad_nonexist_849
1900 THEN ASM_REWRITE_TAC[NOT_EXISTS_THM]
1901 THEN STRIP_TAC
1902 THEN THAYTHE_TAC 0[`v 1`;`v 2`;`v 3`;`v 0`;]
1903 THEN DICH_TAC 0
1904 THEN ONCE_REWRITE_TAC[DIST_SYM]
1905 THEN ASM_REWRITE_TAC[DE_MORGAN_THM;REAL_ARITH`~(a<=b)<=> b<a`]
1906 THEN RESA_TAC;
1907
1908
1909 THAYTHEL_TAC (18-2)[`1`;`3`][scs_diag;ARITH_RULE`~(1 MOD 4 = 3 MOD 4) /\
1910       ~(SUC 1 MOD 4 = 3 MOD 4) /\
1911       ~(1 MOD 4 = SUC 3 MOD 4)`]
1912 THEN DICH_TAC 0
1913 THEN ONCE_REWRITE_TAC[DIST_SYM]
1914 THEN DICH_TAC 0
1915 THEN REAL_ARITH_TAC
1916 ;
1917
1918 THAYTHEL_TAC (18-2)[`0`;`2`][scs_diag;ARITH_RULE`~(0 MOD 4 = 2 MOD 4) /\
1919       ~(SUC 0 MOD 4 = 2 MOD 4) /\
1920       ~(0 MOD 4 = SUC 2 MOD 4)`]
1921 THEN DICH_TAC 0
1922 THEN DICH_TAC 0
1923 THEN REAL_ARITH_TAC
1924 ;
1925
1926
1927
1928 MP_TAC (SET_RULE`scs_is_str scs_4M6' v 1\/ ~(scs_is_str scs_4M6' v 1 )`)
1929 THEN RESA_TAC;
1930
1931 MP_TAC VASYYAU
1932 THEN RESA_TAC
1933 THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`1`][ARITH_RULE`1+3=4`]
1934 THEN MP_TAC Bkossge.quad_nonexist_849
1935 THEN ASM_REWRITE_TAC[NOT_EXISTS_THM]
1936 THEN STRIP_TAC
1937 THEN THAYTHE_TAC 0[`v 1`;`v 2`;`v 3`;`v 0`;]
1938 THEN DICH_TAC 0
1939 THEN ONCE_REWRITE_TAC[DIST_SYM]
1940 THEN ASM_REWRITE_TAC[DE_MORGAN_THM;REAL_ARITH`~(a<=b)<=> b<a`]
1941 THEN RESA_TAC;
1942
1943
1944 THAYTHEL_TAC (19-2)[`1`;`3`][scs_diag;ARITH_RULE`~(1 MOD 4 = 3 MOD 4) /\
1945       ~(SUC 1 MOD 4 = 3 MOD 4) /\
1946       ~(1 MOD 4 = SUC 3 MOD 4)`]
1947 THEN DICH_TAC 0
1948 THEN ONCE_REWRITE_TAC[DIST_SYM]
1949 THEN DICH_TAC 0
1950 THEN REAL_ARITH_TAC
1951 ;
1952
1953 THAYTHEL_TAC (19-2)[`0`;`2`][scs_diag;ARITH_RULE`~(0 MOD 4 = 2 MOD 4) /\
1954       ~(SUC 0 MOD 4 = 2 MOD 4) /\
1955       ~(0 MOD 4 = SUC 2 MOD 4)`]
1956 THEN DICH_TAC 0
1957 THEN DICH_TAC 0
1958 THEN REAL_ARITH_TAC
1959 ;
1960
1961
1962 MP_TAC TUAPYYU
1963 THEN RESA_TAC
1964 THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`0`][IN;ARITH_RULE`0+1=1`];
1965
1966
1967
1968
1969 MP_TAC Bkossge.quad_nonexist_849
1970 THEN ASM_REWRITE_TAC[NOT_EXISTS_THM]
1971 THEN STRIP_TAC
1972 THEN THAYTHE_TAC 0[`v 1`;`v 2`;`v 3`;`v 0`;]
1973 THEN DICH_TAC 0
1974 THEN ONCE_REWRITE_TAC[DIST_SYM]
1975 THEN ASM_REWRITE_TAC[DE_MORGAN_THM;REAL_ARITH`~(a<=b)<=> b<a`]
1976 THEN RESA_TAC;
1977
1978
1979 THAYTHEL_TAC (18-2)[`1`;`3`][scs_diag;ARITH_RULE`~(1 MOD 4 = 3 MOD 4) /\
1980       ~(SUC 1 MOD 4 = 3 MOD 4) /\
1981       ~(1 MOD 4 = SUC 3 MOD 4)`]
1982 THEN DICH_TAC 0
1983 THEN ONCE_REWRITE_TAC[DIST_SYM]
1984 THEN DICH_TAC 0
1985 THEN REAL_ARITH_TAC
1986 ;
1987
1988 THAYTHEL_TAC (18-2)[`0`;`2`][scs_diag;ARITH_RULE`~(0 MOD 4 = 2 MOD 4) /\
1989       ~(SUC 0 MOD 4 = 2 MOD 4) /\
1990       ~(0 MOD 4 = SUC 2 MOD 4)`]
1991 THEN DICH_TAC 0
1992 THEN DICH_TAC 0
1993 THEN REAL_ARITH_TAC
1994 ;
1995
1996
1997 ]);;
1998
1999
2000
2001 let BB_4M6_IMP_scs_4T3=prove(
2002 `main_nonlinear_terminal_v11
2003      ==> (!v. MMs_v39 scs_4M6' v /\
2004               (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))
2005               ==> BBs_v39 scs_4T3 v)`,
2006 REPEAT STRIP_TAC
2007 THEN MP_TAC EXTREMAL_SCS_4M6
2008 THEN RESA_TAC
2009 THEN THAYTHE_TAC 0[`v`]
2010 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M6'`;`v`]
2011 THEN DICH_TAC 0
2012 THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4T3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4T3]
2013 THEN REPEAT RESA_TAC
2014 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2015 THEN SCS_TAC
2016 THEN THAYTHE_TAC 2[`i`;`j`]
2017 THEN DICH_TAC 0
2018 THEN DICH_TAC 0
2019 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M6'`;`v`]
2020 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M6'`][SCS_4M6_IS_SCS]
2021 THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M6;MOD_REFL]
2022 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M6'`][SCS_4M6_IS_SCS]
2023 THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M6;MOD_REFL]
2024 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2025 THEN SYM_ASSUM_TAC
2026 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`)
2027 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2028 THEN RESA_TAC
2029 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`)
2030 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2031 THEN RESA_TAC
2032 THEN SCS_TAC
2033 THEN ONCE_REWRITE_TAC[DIST_SYM]
2034 THEN ASM_REWRITE_TAC[]
2035 THEN RESA_TAC);;
2036
2037 (**************)
2038
2039
2040 let MM_4M6_IMP_MM_4T3=prove(`main_nonlinear_terminal_v11
2041      ==> (!v. MMs_v39 scs_4M6' v /\
2042               (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))
2043 ==> ~(MMs_v39 scs_4T3={}))`,
2044 STRIP_TAC
2045 THEN GEN_TAC
2046 THEN STRIP_TAC
2047 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2048 THEN EXISTS_TAC`v:num->real^3`
2049 THEN EXISTS_TAC`scs_4M6'`
2050 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M6'`;`v`]
2051 THEN ASM_SIMP_TAC[SCS_4T3_BASIC;SCS_4M6_BASIC;SCS_4T3_IS_SCS;SCS_4T3_IS_SCS;
2052 SCS_4M6_IS_SCS;K_SCS_4T3;K_SCS_4M6;IN;BB_4M6_IMP_scs_4T3]
2053 THEN SCS_TAC
2054 THEN REAL_ARITH_TAC);;
2055
2056
2057 let SCS_4M6_ARROW_SCS_4T3_STAB_4M6=prove_by_refinement(
2058 `main_nonlinear_terminal_v11
2059 ==> scs_arrow_v39 { scs_4M6' } ({scs_4T3} UNION {scs_stab_diag_v39 scs_4M6' i j| scs_diag 4 i j})`,
2060 [
2061 STRIP_TAC
2062 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM]
2063 THEN ABBREV_TAC`k=scs_k_v39 s`
2064 THEN REPEAT RESA_TAC;
2065
2066 ASM_SIMP_TAC[SCS_4T3_IS_SCS];
2067
2068 ASM_SIMP_TAC[STAB_4M6_SCS;K_SCS_4M6];
2069
2070 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M6' ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M6' ==> MMs_v39 s = {}))`);
2071
2072 ASM_REWRITE_TAC[];
2073
2074
2075 ASM_REWRITE_TAC[]
2076 THEN POP_ASSUM MP_TAC
2077 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
2078 THEN REPEAT STRIP_TAC
2079 THEN POP_ASSUM MP_TAC
2080 THEN RESA_TAC
2081 THEN POP_ASSUM MP_TAC
2082 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2083 THEN STRIP_TAC;
2084
2085 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)))`)
2086 THEN RESA_TAC;
2087
2088 EXISTS_TAC`scs_4T3`
2089 THEN ASM_REWRITE_TAC[]
2090 THEN MP_TAC MM_4M6_IMP_MM_4T3
2091 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2092 THEN RESA_TAC
2093 THEN MATCH_DICH_TAC 0
2094 THEN ASM_REWRITE_TAC[]
2095 THEN EXISTS_TAC`v:num->real^3`
2096 THEN ASM_REWRITE_TAC[];
2097
2098 POP_ASSUM MP_TAC
2099 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
2100 THEN STRIP_TAC
2101 THEN MP_TAC MM_4M6_IMP_STAB_4M6
2102 THEN RESA_TAC
2103 THEN DICH_TAC 0
2104 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2105 THEN STRIP_TAC
2106 THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M6' i j`
2107 THEN ASM_REWRITE_TAC[]
2108 THEN STRIP_TAC;
2109
2110 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
2111 THEN EXISTS_TAC`i:num`
2112 THEN EXISTS_TAC`j:num`
2113 THEN ASM_REWRITE_TAC[];
2114
2115 EXISTS_TAC`v':num->real^3`
2116 THEN ASM_REWRITE_TAC[]]);;
2117
2118
2119 let NWDGKXH=prove(`main_nonlinear_terminal_v11
2120 ==> scs_arrow_v39 { scs_4M6' } ({scs_4T3, scs_4T5})`,
2121 STRIP_TAC
2122 THEN MATCH_MP_TAC FZIOTEF_TRANS
2123 THEN EXISTS_TAC`({scs_4T3} UNION {scs_stab_diag_v39 scs_4M6' i j| scs_diag 4 i j})`
2124 THEN ASM_SIMP_TAC[SCS_4M6_ARROW_SCS_4T3_STAB_4M6]
2125 THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`;]
2126 THEN MATCH_MP_TAC FZIOTEF_UNION
2127 THEN ASM_SIMP_TAC[SET_STAB_4M6_ARROW_4T5]
2128 THEN MATCH_MP_TAC FZIOTEF_REFL
2129 THEN REWRITE_TAC[IN_SING]
2130 THEN REPEAT RESA_TAC
2131 THEN ASM_SIMP_TAC[SCS_4T3_IS_SCS]);;
2132
2133
2134
2135
2136 (*****************)
2137
2138
2139 let h0_LT_B_SCS_4M7=prove(`
2140 (!i j. scs_diag 4 i j ==> &4 * h0 < scs_b_v39 scs_4M7 i j)
2141 /\ (!i j. scs_diag 4 i j ==> scs_a_v39 scs_4M7 i j <= cstab)`,
2142 SCS_TAC
2143 THEN REWRITE_TAC[h0;SCS_DIAG_4_CASES;cstab]
2144 THEN REPEAT RESA_TAC
2145 THEN ASSUME_TAC(ARITH_RULE`~(4=0)`)
2146 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
2147 THEN SYM_ASSUM_TAC
2148 THEN SCS_TAC
2149 THEN MP_TAC sqrt8_LE_CSTAB
2150 THEN REAL_ARITH_TAC);;
2151
2152 let SCS_4M7_STAND_OR_PRO=prove(`!i. scs_a_v39 scs_4M7 i (i + 1) = &2 /\
2153            scs_b_v39 scs_4M7 i (i + 1) = &2 * h0 \/
2154            scs_a_v39 scs_4M7 i (i + 1) = &2 * h0 /\
2155            scs_b_v39 scs_4M7 i (i + 1) = cstab`,
2156 GEN_TAC
2157 THEN SCS_TAC
2158 THEN SIMP_TAC[GSYM ADD1;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
2159 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`SUC i:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2160 THEN SYM_ASSUM_TAC
2161 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`4`][ARITH_RULE`1<4`]
2162 THEN SYM_ASSUM_TAC
2163 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`)
2164 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2165 THEN RESA_TAC
2166 THEN SCS_TAC);;
2167
2168
2169 let SCS_4M7_STAND=prove(
2170 `scs_a_v39 scs_4M7 0 1= &2*h0/\ scs_a_v39 scs_4M7 1 2 = &2 * h0 /\ scs_a_v39 scs_4M7 2 5= &2*h0 /\scs_b_v39 scs_4M7 1 2= cstab /\scs_b_v39 scs_4M7 0 1 = cstab`,
2171 SCS_TAC);;
2172
2173
2174
2175 let MIN_NOT_STAND_4M7=prove_by_refinement(`main_nonlinear_terminal_v11 ==>
2176 (!v.
2177     MMs_v39 scs_4M7 v /\
2178     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) ==>
2179     dist (v 1,v 2) = &2 * h0 \/  dist (v 0,v 1) = &2*h0)`,
2180 [STRIP_TAC
2181 THEN GEN_TAC
2182 THEN STRIP_TAC
2183 THEN ASSUME_TAC(SCS_4M7_IS_SCS)
2184 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M7`;`v`]
2185 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`]
2186 THEN THAYTHES_TAC 0[`4`;`0`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M7]
2187 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`]
2188 THEN THAYTHES_TAC 0[`5`;`1`][ARITH_RULE`5 MOD 4 = 1 MOD 4`;MOD_MULT_ADD;K_SCS_4M7]
2189 THEN ASSUME_TAC h0_LT_B_SCS_4M7
2190 THEN ASSUME_TAC SCS_4M7_STAND_OR_PRO
2191 THEN ASSUME_TAC SCS_4M7_BASIC
2192 THEN ASSUME_TAC K_SCS_4M7
2193 THEN ASSUME_TAC SCS_4M7_STAND
2194 THEN MP_TAC (SET_RULE`scs_is_str scs_4M7 v 0\/ ~(scs_is_str scs_4M7 v 0 )`)
2195 THEN RESA_TAC;
2196
2197 MP_TAC VASYYAU
2198 THEN RESA_TAC
2199 THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`0`][ARITH_RULE`0+1=1`];
2200
2201 MP_TAC (SET_RULE`scs_is_str scs_4M7 v 1\/ ~(scs_is_str scs_4M7 v 1 )`)
2202 THEN RESA_TAC;
2203
2204 MP_TAC VASYYAU
2205 THEN RESA_TAC
2206 THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`1`][ARITH_RULE`1+1=2`];
2207
2208 MP_TAC (SET_RULE`scs_is_str scs_4M7 v 2\/ ~(scs_is_str scs_4M7 v 2 )`)
2209 THEN RESA_TAC;
2210
2211 MP_TAC VASYYAU
2212 THEN RESA_TAC
2213 THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`2`][ARITH_RULE`2+3=5`]
2214 THEN ONCE_REWRITE_TAC[DIST_SYM]
2215 THEN ASM_REWRITE_TAC[];
2216
2217 MP_TAC TUAPYYU
2218 THEN RESA_TAC
2219 THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`1`][IN;ARITH_RULE`1+1=2`]
2220 THEN MP_TAC TUAPYYU
2221 THEN RESA_TAC
2222 THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`0`][IN;ARITH_RULE`0+1=1`]
2223 THEN MRESAL_TAC STR_MOD_EQ[`4`;`scs_4M7`;`v`;`4`][IN;ARITH_RULE`4 MOD 4=0`]
2224 THEN MP_TAC WKZZEEH
2225 THEN RESA_TAC
2226 THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`1`][ARITH_RULE`1+1=2/\ 1+3=4`]
2227 THEN DICH_TAC 0
2228 THEN ONCE_REWRITE_TAC[DIST_SYM]
2229 THEN ASM_REWRITE_TAC[]]);;
2230
2231
2232
2233
2234
2235 let BB_4M7_IMP_4M6_12=prove(`main_nonlinear_terminal_v11 ==>
2236 (!v.
2237     MMs_v39 scs_4M7 v /\
2238     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) /\
2239     dist (v 1,v 2) = &2*h0
2240 ==> BBs_v39 scs_4M6' v)`,
2241 REPEAT STRIP_TAC
2242 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M7`;`v`]
2243 THEN DICH_TAC 0
2244 THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M7;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
2245 THEN REPEAT RESA_TAC
2246 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2247 THEN SCS_TAC
2248 THEN THAYTHE_TAC 2[`i`;`j`]
2249 THEN DICH_TAC 0
2250 THEN DICH_TAC 0
2251 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M7`;`v`]
2252 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][SCS_4M7_IS_SCS]
2253 THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M7;MOD_REFL]
2254 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][SCS_4M7_IS_SCS]
2255 THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M7;MOD_REFL]
2256 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2257 THEN SYM_ASSUM_TAC
2258 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`)
2259 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2260 THEN RESA_TAC
2261 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`)
2262 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2263 THEN RESA_TAC
2264 THEN SCS_TAC
2265 THEN ONCE_REWRITE_TAC[DIST_SYM]
2266 THEN ASM_REWRITE_TAC[h0]
2267 THEN REAL_ARITH_TAC);;
2268
2269
2270
2271 let MM_4M7_IMP_MM_4M6_12=prove(`main_nonlinear_terminal_v11
2272      ==> (!v. MMs_v39 scs_4M7 v /\
2273               (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
2274               dist (v 1,v 2) = &2 * h0
2275 ==> ~(MMs_v39 scs_4M6'={}))`,
2276 STRIP_TAC
2277 THEN GEN_TAC
2278 THEN STRIP_TAC
2279 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2280 THEN EXISTS_TAC`v:num->real^3`
2281 THEN EXISTS_TAC`scs_4M7`
2282 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M7`;`v`]
2283 THEN ASM_SIMP_TAC[SCS_4M6_BASIC;SCS_4M7_BASIC;SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;
2284 SCS_4M7_IS_SCS;K_SCS_4M6;K_SCS_4M7;IN;BB_4M7_IMP_4M6_12]
2285 THEN SCS_TAC
2286 THEN REAL_ARITH_TAC);;
2287
2288
2289
2290
2291
2292 let BB_4M7_IMP_4M6_01=prove(
2293 `main_nonlinear_terminal_v11 ==>
2294 (!v.
2295     MMs_v39 scs_4M7 v /\
2296     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) /\
2297     dist (v 0,v 1) = &2*h0
2298 ==> BBs_v39 (scs_prop_equ_v39(scs_opp_v39 scs_4M6' ) 1) v)`,
2299 REPEAT STRIP_TAC
2300 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M7`;`v`]
2301 THEN DICH_TAC 0
2302 THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M7;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;scs_prop_equ_v39;scs_opp_v39;peropp2]
2303 THEN REPEAT RESA_TAC
2304 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2305 THEN SCS_TAC
2306 THEN THAYTHE_TAC 2[`i`;`j`]
2307 THEN DICH_TAC 0
2308 THEN DICH_TAC 0
2309 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M7`;`v`]
2310 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][SCS_4M7_IS_SCS]
2311 THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M7;MOD_REFL]
2312 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][SCS_4M7_IS_SCS]
2313 THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M7;MOD_REFL]
2314 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+i:num`;`1+j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2315 THEN SYM_ASSUM_TAC
2316 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2317 THEN SYM_ASSUM_TAC
2318 THEN MRESA_TAC MOD_ADD_MOD[`1`;`i`;`4`]
2319 THEN MRESA_TAC MOD_ADD_MOD[`1`;`j`;`4`]
2320 THEN SYM_ASSUM_TAC
2321 THEN SYM_ASSUM_TAC
2322 THEN ASSUME_TAC(ARITH_RULE`4-1=3/\ 4-0=4/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 3+2=5 /\3+3=6/\ 5 MOD 4=1/\ 6 MOD 4=2`)
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 ONCE_REWRITE_TAC[DIST_SYM]
2331 THEN ASM_REWRITE_TAC[h0;REAL_ARITH`a<=a`]
2332 THEN REAL_ARITH_TAC);;
2333
2334
2335
2336 let MM_4M7_IMP_MM_4M6_01=prove_by_refinement(`main_nonlinear_terminal_v11
2337      ==> (!v. MMs_v39 scs_4M7 v /\
2338               (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
2339               dist (v 0,v 1) = &2 * h0
2340 ==> ~(MMs_v39 (scs_prop_equ_v39(scs_opp_v39 scs_4M6' ) 1)={}))`,
2341 [STRIP_TAC
2342 THEN GEN_TAC
2343 THEN STRIP_TAC
2344 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2345 THEN EXISTS_TAC`v:num->real^3`
2346 THEN EXISTS_TAC`scs_4M7`
2347 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M7`;`v`]
2348 THEN ASM_SIMP_TAC[SCS_4M6_BASIC;SCS_4M7_BASIC;SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;
2349 SCS_4M7_IS_SCS;K_SCS_4M6;K_SCS_4M7;IN;BB_4M7_IMP_4M6_01]
2350 THEN STRIP_TAC;
2351
2352 MATCH_MP_TAC PROP_EQU_IS_SCS
2353 THEN MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
2354 THEN EXISTS_TAC`scs_opp_v39 scs_4M6'`
2355 THEN ASM_REWRITE_TAC[SCS_4M6_IS_SCS];
2356
2357 STRIP_TAC;
2358
2359 MATCH_MP_TAC Hexagons.BAISC_PROP_EQU
2360 THEN MATCH_MP_TAC Cqaoqlr.BASIC_OPP
2361 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M6_BASIC];
2362
2363 ASM_REWRITE_TAC[Hexagons.K_SCS_PROP_EUQ]
2364 THEN ASM_REWRITE_TAC[scs_opp_v39;scs_prop_equ_v39]
2365 THEN SCS_TAC
2366 THEN REAL_ARITH_TAC]);;
2367
2368
2369
2370 let SCS_4M7_ARROW_STAB_4M7_4M6=prove_by_refinement(
2371 `main_nonlinear_terminal_v11
2372 ==> scs_arrow_v39 { scs_4M7 } ({scs_4M6', scs_prop_equ_v39(scs_opp_v39 scs_4M6' ) 1} UNION {scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j})`,
2373 [
2374 STRIP_TAC
2375 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM;SET_RULE`a IN {b,c}<=> a= b\/ a=c`]
2376 THEN ABBREV_TAC`k=scs_k_v39 s`
2377 THEN REPEAT RESA_TAC;
2378
2379 ASM_SIMP_TAC[SCS_4M6_IS_SCS];
2380
2381 MATCH_MP_TAC PROP_EQU_IS_SCS
2382 THEN MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
2383 THEN EXISTS_TAC`scs_opp_v39 scs_4M6'`
2384 THEN ASM_REWRITE_TAC[SCS_4M6_IS_SCS];
2385
2386 ASM_SIMP_TAC[STAB_4M7_SCS;K_SCS_4M7];
2387
2388 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M7 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M7 ==> MMs_v39 s = {}))`);
2389
2390 ASM_REWRITE_TAC[];
2391
2392 ASM_REWRITE_TAC[]
2393 THEN POP_ASSUM MP_TAC
2394 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
2395 THEN REPEAT STRIP_TAC
2396 THEN POP_ASSUM MP_TAC
2397 THEN RESA_TAC
2398 THEN POP_ASSUM MP_TAC
2399 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2400 THEN STRIP_TAC;
2401
2402 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)))`)
2403 THEN RESA_TAC;
2404
2405 MP_TAC MIN_NOT_STAND_4M7
2406 THEN RESA_TAC
2407 THEN THAYTHE_TAC 0[`v`];
2408
2409 EXISTS_TAC`scs_4M6'`
2410 THEN ASM_REWRITE_TAC[]
2411 THEN MP_TAC MM_4M7_IMP_MM_4M6_12
2412 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2413 THEN RESA_TAC
2414 THEN MATCH_DICH_TAC 0
2415 THEN ASM_REWRITE_TAC[]
2416 THEN EXISTS_TAC`v:num->real^3`
2417 THEN ASM_REWRITE_TAC[];
2418
2419 EXISTS_TAC`scs_prop_equ_v39 (scs_opp_v39 scs_4M6') 1`
2420 THEN ASM_REWRITE_TAC[]
2421 THEN MP_TAC MM_4M7_IMP_MM_4M6_01
2422 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2423 THEN RESA_TAC
2424 THEN MATCH_DICH_TAC 0
2425 THEN ASM_REWRITE_TAC[]
2426 THEN EXISTS_TAC`v:num->real^3`
2427 THEN ASM_REWRITE_TAC[];
2428
2429 POP_ASSUM MP_TAC
2430 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
2431 THEN STRIP_TAC
2432 THEN MP_TAC MM_4M7_IMP_STAB_4M7
2433 THEN RESA_TAC
2434 THEN DICH_TAC 0
2435 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2436 THEN STRIP_TAC
2437 THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M7 i j`
2438 THEN ASM_REWRITE_TAC[]
2439 THEN STRIP_TAC;
2440
2441 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
2442 THEN EXISTS_TAC`i:num`
2443 THEN EXISTS_TAC`j:num`
2444 THEN ASM_REWRITE_TAC[];
2445
2446 EXISTS_TAC`v':num->real^3`
2447 THEN ASM_REWRITE_TAC[]]);;
2448
2449
2450 (*************)
2451
2452 let K_SCS_OPP_4M6=prove(`scs_k_v39 (scs_opp_v39 scs_4M6') = 4`,
2453 ASM_REWRITE_TAC[scs_opp_v39;scs_prop_equ_v39]
2454 THEN SCS_TAC);;
2455
2456 let SCS_4M6_OPP_IS_SCS=prove(`is_scs_v39 (scs_opp_v39 scs_4M6')`,
2457 MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
2458 THEN EXISTS_TAC`scs_opp_v39 scs_4M6'`
2459 THEN ASM_REWRITE_TAC[SCS_4M6_IS_SCS]);;
2460
2461
2462 let YOBIMPP=prove(`main_nonlinear_terminal_v11
2463 ==> scs_arrow_v39 { scs_4M7 } {scs_4M6',scs_3T3,scs_3M1,scs_3T4}`,
2464
2465 STRIP_TAC
2466 THEN MATCH_MP_TAC FZIOTEF_TRANS
2467 THEN EXISTS_TAC`({scs_4M6', scs_prop_equ_v39(scs_opp_v39 scs_4M6' ) 1} UNION {scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j})`
2468 THEN ASM_SIMP_TAC[SCS_4M7_ARROW_STAB_4M7_4M6;
2469 SET_RULE`{scs_4M6',scs_3T3,scs_3M1,scs_3T4}={scs_4M6',scs_4M6'} UNION{scs_3T3,scs_3M1,scs_3T4}`]
2470 THEN MATCH_MP_TAC FZIOTEF_UNION
2471 THEN ASM_SIMP_TAC[STAB_SCS_4M7_ARROW_3T3_3M1_3T4;SET_RULE`{A,B}={A} UNION {B}`]
2472 THEN MATCH_MP_TAC FZIOTEF_UNION
2473 THEN STRIP_TAC
2474 THENL[
2475
2476 MATCH_MP_TAC FZIOTEF_REFL
2477 THEN REWRITE_TAC[IN_SING]
2478 THEN REPEAT RESA_TAC
2479 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS];
2480
2481
2482 MRESAS_TAC PRO_EQU_ID1[`scs_opp_v39 scs_4M6'`;`1`;`4`][SCS_4M6_IS_SCS;K_SCS_4M6;ARITH_RULE`(4 - 1 MOD 4)=3`;K_SCS_OPP_4M6;SCS_4M6_OPP_IS_SCS]
2483 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 (scs_opp_v39 scs_4M6') 1`;`3`][PROP_EQU_IS_SCS;SCS_4M6_IS_SCS;K_SCS_OPP_4M6;SCS_4M6_OPP_IS_SCS]
2484 THEN DICH_TAC 0
2485 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
2486 THEN REWRITE_TAC[]
2487 THEN STRIP_TAC
2488 THEN MATCH_MP_TAC FZIOTEF_TRANS
2489 THEN EXISTS_TAC`{scs_opp_v39 scs_4M6'}`
2490 THEN ASM_REWRITE_TAC[]
2491 THEN ASSUME_TAC SCS_4M6_IS_SCS
2492 THEN MRESA_TAC Yxionxl2.SCS_OPP_REFL[`scs_4M6'`]
2493 THEN MRESAS_TAC  YXIONXL2[`4`;`scs_opp_v39 scs_4M6'`][K_SCS_OPP_4M6;SCS_4M6_OPP_IS_SCS;ARITH_RULE`~(4<=3)`]]);;
2494
2495
2496 (**************************)
2497
2498
2499
2500 let BB_4M8_IMP_4M6_23=prove(`main_nonlinear_terminal_v11 ==>
2501 (!v.
2502     MMs_v39 scs_4M8 v /\
2503     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) /\
2504     dist (v 2,v 3) = &2*h0
2505 ==> BBs_v39 scs_4M6' v)`,
2506 REPEAT STRIP_TAC
2507 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2508 THEN DICH_TAC 0
2509 THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
2510 THEN REPEAT RESA_TAC
2511 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2512 THEN SCS_TAC
2513 THEN THAYTHE_TAC 2[`i`;`j`]
2514 THEN DICH_TAC 0
2515 THEN DICH_TAC 0
2516 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2517 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
2518 THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
2519 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
2520 THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
2521 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2522 THEN SYM_ASSUM_TAC
2523 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`)
2524 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2525 THEN RESA_TAC
2526 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`)
2527 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2528 THEN RESA_TAC
2529 THEN SCS_TAC
2530 THEN ONCE_REWRITE_TAC[DIST_SYM]
2531 THEN ASM_REWRITE_TAC[h0]
2532 THEN REAL_ARITH_TAC);;
2533
2534
2535
2536 let MM_4M8_IMP_MM_4M6_23=prove(
2537 `main_nonlinear_terminal_v11
2538      ==> (!v. MMs_v39 scs_4M8 v /\
2539               (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
2540               dist (v 2,v 3) = &2 * h0
2541 ==> ~(MMs_v39 scs_4M6'={}))`,
2542 STRIP_TAC
2543 THEN GEN_TAC
2544 THEN STRIP_TAC
2545 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2546 THEN EXISTS_TAC`v:num->real^3`
2547 THEN EXISTS_TAC`scs_4M8`
2548 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8`;`v`]
2549 THEN ASM_SIMP_TAC[SCS_4M6_BASIC;SCS_4M8_BASIC;SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;
2550 SCS_4M8_IS_SCS;K_SCS_4M6;K_SCS_4M8;IN;BB_4M8_IMP_4M6_23]
2551 THEN SCS_TAC
2552 THEN REAL_ARITH_TAC);;
2553
2554
2555
2556
2557 let BB_4M8_IMP_4M6_01=prove(
2558 `main_nonlinear_terminal_v11 ==>
2559 (!v.
2560     MMs_v39 scs_4M8 v /\
2561     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) /\
2562     dist (v 0,v 1) = &2*h0
2563 ==> BBs_v39 ((scs_opp_v39 scs_4M6' ) ) v)`,
2564 REPEAT STRIP_TAC
2565 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2566 THEN DICH_TAC 0
2567 THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;scs_prop_equ_v39;scs_opp_v39;peropp2]
2568 THEN REPEAT RESA_TAC
2569 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2570 THEN SCS_TAC
2571 THEN THAYTHE_TAC 2[`i`;`j`]
2572 THEN DICH_TAC 0
2573 THEN DICH_TAC 0
2574 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2575 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
2576 THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
2577 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
2578 THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
2579 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+i:num`;`1+j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2580 THEN SYM_ASSUM_TAC
2581 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2582 THEN SYM_ASSUM_TAC
2583 THEN MRESA_TAC MOD_ADD_MOD[`1`;`i`;`4`]
2584 THEN MRESA_TAC MOD_ADD_MOD[`1`;`j`;`4`]
2585 THEN SYM_ASSUM_TAC
2586 THEN SYM_ASSUM_TAC
2587 THEN ASSUME_TAC(ARITH_RULE`4-1=3/\ 4-0=4/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 3+2=5 /\3+3=6/\ 5 MOD 4=1/\ 6 MOD 4=2`)
2588 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`)
2589 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2590 THEN RESA_TAC
2591 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`)
2592 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2593 THEN RESA_TAC
2594 THEN SCS_TAC
2595 THEN ONCE_REWRITE_TAC[DIST_SYM]
2596 THEN ASM_REWRITE_TAC[h0;REAL_ARITH`a<=a`]
2597 THEN REAL_ARITH_TAC);;
2598
2599
2600
2601
2602
2603 let MM_4M8_IMP_MM_4M6_01=prove_by_refinement(`main_nonlinear_terminal_v11
2604      ==> (!v. MMs_v39 scs_4M8 v /\
2605               (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
2606               dist (v 0,v 1) = &2 * h0
2607 ==> ~(MMs_v39 ((scs_opp_v39 scs_4M6' ) )={}))`,
2608 [
2609 STRIP_TAC
2610 THEN GEN_TAC
2611 THEN STRIP_TAC
2612 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2613 THEN EXISTS_TAC`v:num->real^3`
2614 THEN EXISTS_TAC`scs_4M8`
2615 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8`;`v`]
2616 THEN ASM_SIMP_TAC[SCS_4M6_BASIC;SCS_4M8_BASIC;SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;
2617 SCS_4M8_IS_SCS;K_SCS_4M6;K_SCS_4M8;IN;BB_4M8_IMP_4M6_01]
2618 THEN STRIP_TAC;
2619
2620 MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
2621 THEN EXISTS_TAC`scs_opp_v39 scs_4M6'`
2622 THEN ASM_REWRITE_TAC[SCS_4M6_IS_SCS];
2623
2624 STRIP_TAC;
2625
2626 MATCH_MP_TAC Cqaoqlr.BASIC_OPP
2627 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M6_BASIC];
2628
2629 ASM_REWRITE_TAC[Hexagons.K_SCS_PROP_EUQ]
2630 THEN ASM_REWRITE_TAC[scs_opp_v39;scs_prop_equ_v39]
2631 THEN SCS_TAC
2632 THEN REAL_ARITH_TAC]);;
2633
2634
2635
2636 let h0_LT_B_SCS_4M8=prove(`
2637 (!i j. scs_diag 4 i j ==> &4 * h0 < scs_b_v39 scs_4M8 i j)
2638 /\ (!i j. scs_diag 4 i j ==> scs_a_v39 scs_4M8 i j <= cstab)`,
2639 SCS_TAC
2640 THEN REWRITE_TAC[h0;SCS_DIAG_4_CASES;cstab]
2641 THEN REPEAT RESA_TAC
2642 THEN ASSUME_TAC(ARITH_RULE`~(4=0)`)
2643 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
2644 THEN SYM_ASSUM_TAC
2645 THEN SCS_TAC
2646 THEN MP_TAC sqrt8_LE_CSTAB
2647 THEN REAL_ARITH_TAC);;
2648
2649 let SCS_4M8_STAND_OR_PRO=prove(`!i. scs_a_v39 scs_4M8 i (i + 1) = &2 /\
2650            scs_b_v39 scs_4M8 i (i + 1) = &2 * h0 \/
2651            scs_a_v39 scs_4M8 i (i + 1) = &2 * h0 /\
2652            scs_b_v39 scs_4M8 i (i + 1) = cstab`,
2653 GEN_TAC
2654 THEN SCS_TAC
2655 THEN SIMP_TAC[GSYM ADD1;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
2656 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`SUC i:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2657 THEN SYM_ASSUM_TAC
2658 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`4`][ARITH_RULE`1<4`]
2659 THEN SYM_ASSUM_TAC
2660 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`)
2661 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2662 THEN RESA_TAC
2663 THEN SCS_TAC);;
2664
2665
2666
2667
2668 let SCS_4M8_STAND=prove(
2669 `scs_a_v39 scs_4M8 0 1= &2*h0/\ scs_a_v39 scs_4M8 1 2 = &2  /\ scs_a_v39 scs_4M8 2 5= &2 /\scs_b_v39 scs_4M8 1 2= &2 *h0 /\scs_b_v39 scs_4M8 0 1 = cstab
2670 /\scs_a_v39 scs_4M8 2 3 = &2 * h0/\ scs_a_v39 scs_4M8 3 4 = &2/\ scs_b_v39 scs_4M8 2 3= cstab/\ scs_a_v39 scs_4M8 1 4= &2* h0/\ scs_a_v39 scs_4M8 3 6= &2 * h0`,
2671 SCS_TAC);;
2672
2673
2674
2675
2676
2677
2678 let MIN_NOT_STAND_4M8=prove_by_refinement(
2679 `main_nonlinear_terminal_v11 ==>
2680 (!v.
2681     MMs_v39 scs_4M8 v /\
2682     (!i j. scs_diag 4 i j ==>   cstab < dist(v i,v j)) ==>
2683     dist (v 2,v 3) = &2 * h0 \/  dist (v 0,v 1) = &2*h0
2684 \/ (dist (v 0,v 1) = cstab/\ dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = cstab/\
2685 dist (v 3,v 0) = &2))`,
2686 [
2687 STRIP_TAC
2688 THEN GEN_TAC
2689 THEN STRIP_TAC
2690 THEN ASSUME_TAC(SCS_4M8_IS_SCS)
2691 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2692 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`]
2693 THEN THAYTHES_TAC 0[`4`;`0`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8]
2694 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`]
2695 THEN THAYTHES_TAC 0[`5`;`1`][ARITH_RULE`5 MOD 4 = 1 MOD 4`;MOD_MULT_ADD;K_SCS_4M8]
2696 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`]
2697 THEN THAYTHES_TAC 0[`6`;`2`][ARITH_RULE`6 MOD 4 = 2 MOD 4`;MOD_MULT_ADD;K_SCS_4M8]
2698 THEN ASSUME_TAC h0_LT_B_SCS_4M8
2699 THEN ASSUME_TAC SCS_4M8_STAND_OR_PRO
2700 THEN ASSUME_TAC SCS_4M8_BASIC
2701 THEN ASSUME_TAC K_SCS_4M8
2702 THEN ASSUME_TAC SCS_4M8_STAND
2703 THEN MP_TAC (SET_RULE`scs_is_str scs_4M8 v 0\/ ~(scs_is_str scs_4M8 v 0 )`)
2704 THEN RESA_TAC;
2705
2706 MP_TAC VASYYAU
2707 THEN RESA_TAC
2708 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`0`][ARITH_RULE`0+1=1`];
2709
2710 MP_TAC (SET_RULE`scs_is_str scs_4M8 v 2\/ ~(scs_is_str scs_4M8 v 2 )`)
2711 THEN RESA_TAC;
2712
2713 MP_TAC VASYYAU
2714 THEN RESA_TAC
2715 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`2`][ARITH_RULE`2+3=5/\ 2+1=3`]
2716 THEN ONCE_REWRITE_TAC[DIST_SYM]
2717 THEN ASM_REWRITE_TAC[];
2718
2719
2720 MP_TAC (SET_RULE`scs_is_str scs_4M8 v 1\/ ~(scs_is_str scs_4M8 v 1 )`)
2721 THEN RESA_TAC;
2722
2723 MP_TAC VASYYAU
2724 THEN RESA_TAC
2725 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`1`][ARITH_RULE`1+1=2/\ 1+3=4`]
2726 THEN MP_TAC PWEIWBZ
2727 THEN RESA_TAC
2728 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`3`][ARITH_RULE`1+1=2/\ 3+1=4`]
2729 THEN MRESAS_TAC NOT_STR_IN_CASES_4_1[`0`;`scs_4M8`;`v`][ARITH_RULE`0+a=a`;IN]
2730 THEN MP_TAC TUAPYYU
2731 THEN RESA_TAC
2732 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`2`][ARITH_RULE`1+1=2/\ 3+1=4/\ 2+1=3`;IN]
2733 THEN ONCE_REWRITE_TAC[DIST_SYM]
2734 THEN ASM_REWRITE_TAC[];
2735
2736 MP_TAC (SET_RULE`scs_is_str scs_4M8 v 3\/ ~(scs_is_str scs_4M8 v 3 )`)
2737 THEN RESA_TAC;
2738
2739 MP_TAC VASYYAU
2740 THEN RESA_TAC
2741 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`3`][ARITH_RULE`3+1=4/\ 3+3=6`]
2742 THEN MP_TAC PWEIWBZ
2743 THEN RESA_TAC
2744 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`1`][ARITH_RULE`1+1=2/\ 3+1=4`]
2745 THEN MP_TAC TUAPYYU
2746 THEN RESA_TAC
2747 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`0`][ARITH_RULE`0+1=1/\ 3+1=4/\ 2+1=3`;IN]
2748 THEN ONCE_REWRITE_TAC[DIST_SYM]
2749 THEN ASM_REWRITE_TAC[];
2750
2751 MP_TAC TUAPYYU
2752 THEN RESA_TAC
2753 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`0`][ARITH_RULE`0+1=1/\ 3+1=4/\ 2+1=3`;IN]
2754 THEN MP_TAC TUAPYYU
2755 THEN RESA_TAC
2756 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`2`][ARITH_RULE`0+1=1/\ 3+1=4/\ 2+1=3`;IN]
2757 THEN MP_TAC YEBWJNG
2758 THEN RESA_TAC
2759 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`1`][ARITH_RULE`1+1=2/\ 3+1=4/\ 2+1=3`;IN]
2760 THEN MRESAL_TAC STR_MOD_EQ[`4`;`scs_4M8`;`v`;`4`][SCS_4M8_IS_SCS;IN;ARITH_RULE`4 MOD 4=0`]
2761 THEN MP_TAC YEBWJNG
2762 THEN RESA_TAC
2763 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`3`][ARITH_RULE`1+1=2/\ 3+1=4/\ 2+1=3`;IN]]);;
2764
2765
2766 let BB_4M8_IMP_scs_4M8_02=prove(
2767 `main_nonlinear_terminal_v11
2768      ==> (!v. MMs_v39 scs_4M8 v /\
2769               (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
2770  dist (v 0,v 1) = cstab/\ dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = cstab/\
2771 dist (v 3,v 0) = &2 /\ dist(v 0, v 2)<= #3.62
2772 ==> BBs_v39 scs_4M8_02 v)`,
2773 STRIP_TAC
2774 THEN GEN_TAC
2775 THEN STRIP_TAC
2776 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2777 THEN DICH_TAC 0
2778 THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8_02;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8_02;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8]
2779 THEN REPEAT RESA_TAC
2780 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2781 THEN SCS_TAC
2782 THEN THAYTHE_TAC 2[`i`;`j`]
2783 THEN DICH_TAC 0
2784 THEN DICH_TAC 0
2785 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2786 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
2787 THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
2788 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
2789 THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
2790 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2791 THEN SYM_ASSUM_TAC
2792 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`)
2793 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2794 THEN RESA_TAC
2795 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`)
2796 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2797 THEN RESA_TAC
2798 THEN SCS_TAC
2799 THEN ONCE_REWRITE_TAC[DIST_SYM]
2800 THEN ASM_REWRITE_TAC[]
2801 THEN RESA_TAC);;
2802
2803
2804
2805 let MM_4M8_IMP_MM_4M8_02=prove(`main_nonlinear_terminal_v11
2806      ==> (!v. MMs_v39 scs_4M8 v /\
2807               (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
2808  dist (v 0,v 1) = cstab/\ dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = cstab/\
2809 dist (v 3,v 0) = &2 /\ dist(v 0, v 2)<= #3.62
2810 ==> ~(MMs_v39 scs_4M8_02={}))`,
2811 STRIP_TAC
2812 THEN GEN_TAC
2813 THEN STRIP_TAC
2814 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2815 THEN EXISTS_TAC`v:num->real^3`
2816 THEN EXISTS_TAC`scs_4M8`
2817 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8`;`v`]
2818 THEN ASM_SIMP_TAC[SCS_4M8_02_BASIC;SCS_4M8_BASIC;SCS_4M8_02_IS_SCS;SCS_4M8_02_IS_SCS;
2819 SCS_4M8_IS_SCS;K_SCS_4M8_02;K_SCS_4M8;IN;BB_4M8_IMP_scs_4M8_02]
2820 THEN SCS_TAC
2821 THEN REAL_ARITH_TAC);;
2822
2823 let BB_4M8_IMP_scs_4M8_13=prove(
2824 `main_nonlinear_terminal_v11
2825      ==> (!v. MMs_v39 scs_4M8 v /\
2826               (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
2827  dist (v 0,v 1) = cstab/\ dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = cstab/\
2828 dist (v 3,v 0) = &2 /\ dist(v 1, v 3)<= #3.62
2829 ==> BBs_v39 scs_4M8_13 v)`,
2830 STRIP_TAC
2831 THEN GEN_TAC
2832 THEN STRIP_TAC
2833 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2834 THEN DICH_TAC 0
2835 THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8_13;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8_13;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8]
2836 THEN REPEAT RESA_TAC
2837 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2838 THEN SCS_TAC
2839 THEN THAYTHE_TAC 2[`i`;`j`]
2840 THEN DICH_TAC 0
2841 THEN DICH_TAC 0
2842 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2843 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
2844 THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
2845 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
2846 THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
2847 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2848 THEN SYM_ASSUM_TAC
2849 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`)
2850 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2851 THEN RESA_TAC
2852 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`)
2853 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2854 THEN RESA_TAC
2855 THEN SCS_TAC
2856 THEN ONCE_REWRITE_TAC[DIST_SYM]
2857 THEN ASM_REWRITE_TAC[]
2858 THEN RESA_TAC);;
2859
2860
2861
2862 let MM_4M8_IMP_MM_4M8_13=prove(`main_nonlinear_terminal_v11
2863      ==> (!v. MMs_v39 scs_4M8 v /\
2864               (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
2865  dist (v 0,v 1) = cstab/\ dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = cstab/\
2866 dist (v 3,v 0) = &2 /\ dist(v 1, v 3)<= #3.62
2867 ==> ~(MMs_v39 scs_4M8_13={}))`,
2868 STRIP_TAC
2869 THEN GEN_TAC
2870 THEN STRIP_TAC
2871 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2872 THEN EXISTS_TAC`v:num->real^3`
2873 THEN EXISTS_TAC`scs_4M8`
2874 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8`;`v`]
2875 THEN ASM_SIMP_TAC[SCS_4M8_13_BASIC;SCS_4M8_BASIC;SCS_4M8_13_IS_SCS;SCS_4M8_13_IS_SCS;
2876 SCS_4M8_IS_SCS;K_SCS_4M8_13;K_SCS_4M8;IN;BB_4M8_IMP_scs_4M8_13]
2877 THEN SCS_TAC
2878 THEN REAL_ARITH_TAC);;
2879
2880
2881
2882
2883 let SCS_4M8_ARROW_STEP_ONE=prove_by_refinement(
2884 `main_nonlinear_terminal_v11
2885 ==> scs_arrow_v39 { scs_4M8 } ({scs_4M6',scs_opp_v39 scs_4M6', scs_4M8_02,scs_4M8_13} UNION {scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j})`,
2886 [STRIP_TAC
2887 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM;SET_RULE`a IN {b,c,d,e}<=> a= b\/ a=c\/ a=d\/ a=e`]
2888 THEN ABBREV_TAC`k=scs_k_v39 s`
2889 THEN REPEAT RESA_TAC;
2890
2891
2892 ASM_SIMP_TAC[SCS_4M6_IS_SCS];
2893
2894 MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
2895 THEN EXISTS_TAC`scs_opp_v39 scs_4M6'`
2896 THEN ASM_REWRITE_TAC[SCS_4M6_IS_SCS];
2897
2898
2899
2900 ASM_SIMP_TAC[SCS_4M8_02_IS_SCS];
2901
2902 ASM_SIMP_TAC[SCS_4M8_13_IS_SCS];
2903
2904
2905 ASM_SIMP_TAC[STAB_4M8_SCS;K_SCS_4M8];
2906
2907
2908 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M8 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M8 ==> MMs_v39 s = {}))`);
2909
2910
2911 ASM_REWRITE_TAC[];
2912
2913
2914 ASM_REWRITE_TAC[]
2915 THEN POP_ASSUM MP_TAC
2916 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
2917 THEN REPEAT STRIP_TAC
2918 THEN POP_ASSUM MP_TAC
2919 THEN RESA_TAC
2920 THEN POP_ASSUM MP_TAC
2921 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2922 THEN STRIP_TAC;
2923
2924
2925 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)))`)
2926 THEN RESA_TAC;
2927
2928
2929 MP_TAC MIN_NOT_STAND_4M8
2930 THEN RESA_TAC
2931 THEN THAYTHE_TAC 0[`v`];
2932
2933
2934 EXISTS_TAC`scs_4M6'`
2935 THEN ASM_REWRITE_TAC[]
2936 THEN MP_TAC MM_4M8_IMP_MM_4M6_23
2937 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2938 THEN RESA_TAC
2939 THEN MATCH_DICH_TAC 0
2940 THEN ASM_REWRITE_TAC[]
2941 THEN EXISTS_TAC`v:num->real^3`
2942 THEN ASM_REWRITE_TAC[];
2943
2944
2945 EXISTS_TAC`(scs_opp_v39 scs_4M6') `
2946 THEN ASM_REWRITE_TAC[]
2947 THEN MP_TAC MM_4M8_IMP_MM_4M6_01
2948 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2949 THEN RESA_TAC
2950 THEN MATCH_DICH_TAC 0
2951 THEN ASM_REWRITE_TAC[]
2952 THEN EXISTS_TAC`v:num->real^3`
2953 THEN ASM_REWRITE_TAC[];
2954
2955 MP_TAC Bkossge.quad_diag_362
2956 THEN RESA_TAC
2957 THEN THAYTHE_TAC 0[`v 1`;`v 2`;`v 3`;`v 0`]
2958 THEN DICH_TAC 0
2959 THEN ONCE_REWRITE_TAC[DIST_SYM]
2960 THEN ASM_REWRITE_TAC[]
2961 THEN ONCE_REWRITE_TAC[DIST_SYM]
2962 THEN STRIP_TAC;
2963
2964
2965 EXISTS_TAC`(scs_4M8_13) `
2966 THEN ASM_REWRITE_TAC[]
2967 THEN MP_TAC MM_4M8_IMP_MM_4M8_13
2968 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2969 THEN RESA_TAC
2970 THEN MATCH_DICH_TAC 0
2971 THEN ASM_REWRITE_TAC[]
2972 THEN EXISTS_TAC`v:num->real^3`
2973 THEN ASM_REWRITE_TAC[];
2974
2975 DICH_TAC 0
2976 THEN ONCE_REWRITE_TAC[DIST_SYM]
2977 THEN STRIP_TAC
2978 THEN EXISTS_TAC`(scs_4M8_02) `
2979 THEN ASM_REWRITE_TAC[]
2980 THEN MP_TAC MM_4M8_IMP_MM_4M8_02
2981 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2982 THEN RESA_TAC
2983 THEN MATCH_DICH_TAC 0
2984 THEN ASM_REWRITE_TAC[]
2985 THEN EXISTS_TAC`v:num->real^3`
2986 THEN ASM_REWRITE_TAC[];
2987
2988
2989
2990 POP_ASSUM MP_TAC
2991 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
2992 THEN STRIP_TAC
2993 THEN MP_TAC MM_4M8_IMP_STAB_4M8
2994 THEN RESA_TAC
2995 THEN DICH_TAC 0
2996 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2997 THEN STRIP_TAC
2998 THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M8 i j`
2999 THEN ASM_REWRITE_TAC[]
3000 THEN STRIP_TAC;
3001
3002
3003 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
3004 THEN EXISTS_TAC`i:num`
3005 THEN EXISTS_TAC`j:num`
3006 THEN ASM_REWRITE_TAC[];
3007
3008
3009 EXISTS_TAC`v':num->real^3`
3010 THEN ASM_REWRITE_TAC[];
3011
3012
3013
3014 ]);;
3015
3016
3017
3018 (****************************)
3019
3020
3021
3022
3023
3024
3025 let SCS_DIAG_SCS_4M8_02_02=prove(`scs_diag (scs_k_v39 scs_4M8_02) 0 2`,
3026 REWRITE_TAC[K_SCS_4M8_02;scs_diag]
3027 THEN ARITH_TAC);;
3028
3029 let SCS_DIAG_SCS_4M8_02_13=prove(`scs_diag (scs_k_v39 scs_4M8_02) 1 3`,
3030 REWRITE_TAC[K_SCS_4M8_02;scs_diag]
3031 THEN ARITH_TAC);;
3032
3033 let SCS_DIAG_SCS_4M8_13_13=prove(`scs_diag (scs_k_v39 scs_4M8_13) 1 3`,
3034 REWRITE_TAC[K_SCS_4M8_13;scs_diag]
3035 THEN ARITH_TAC);;
3036
3037
3038 let STAB_4M8_02_SCS=prove(` scs_diag (scs_k_v39 scs_4M8_02) i j
3039 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M8_02 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M8_02 i j)`,
3040 STRIP_TAC
3041 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
3042 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M8_02_IS_SCS;SCS_4M8_02_BASIC;K_SCS_4M8_02;
3043 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
3044 THEN SCS_TAC
3045 THEN REWRITE_TAC[h0;cstab]
3046 THEN MP_TAC sqrt8_LE_CSTAB
3047 THEN MP_TAC LE_sqrt8_2h0
3048 THEN REAL_ARITH_TAC);;
3049
3050
3051 let STAB_4M8_13_SCS=prove(` scs_diag (scs_k_v39 scs_4M8_13) i j
3052 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M8_13 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M8_13 i j)`,
3053 STRIP_TAC
3054 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
3055 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M8_13_IS_SCS;SCS_4M8_13_BASIC;K_SCS_4M8_13;
3056 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
3057 THEN SCS_TAC
3058 THEN REWRITE_TAC[h0;cstab]
3059 THEN MP_TAC sqrt8_LE_CSTAB
3060 THEN MP_TAC LE_sqrt8_2h0
3061 THEN REAL_ARITH_TAC);;
3062
3063 let BASIC_HALF_SLICE=prove(`scs_basic_v39 s
3064 ==> scs_basic_v39 (scs_half_slice_v39 (s) p q d' F)`,
3065 ASM_SIMP_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39]
3066 THEN SET_TAC[]);;
3067
3068 let D_HALF_SLICE1=prove(`scs_d_v39 (scs_half_slice_v39 (s) p q d' mkj)=d'`,
3069 SCS_TAC);;
3070
3071 let J_SCS_3T7_OPP_PROP=prove(`scs_J_v39 (scs_prop_equ_v39 (scs_opp_v39 scs_3T7) i) i1 j= F`,
3072 REWRITE_TAC[scs_opp_v39;peropp2]
3073 THEN SCS_TAC
3074 THEN REWRITE_TAC[scs_opp_v39;peropp2]);;
3075
3076
3077 let J_SCS_3T7_OPP=prove(`scs_J_v39 ((scs_opp_v39 scs_3T7) ) i1 j= F`,
3078 REWRITE_TAC[scs_opp_v39;peropp2]
3079 THEN SCS_TAC
3080 THEN REWRITE_TAC[scs_opp_v39;peropp2]);;
3081
3082
3083
3084 let SCS_4M8_02_SLICE_02=prove_by_refinement(`scs_arrow_v39 {scs_4M8_02 } {scs_prop_equ_v39
3085 ( scs_opp_v39 scs_3T7) 2 }`,
3086 [
3087
3088 ONCE_REWRITE_TAC[SET_RULE`{scs_prop_equ_v39
3089 ( scs_opp_v39 scs_3T7) 2}={scs_prop_equ_v39
3090 ( scs_opp_v39 scs_3T7) 2, scs_prop_equ_v39
3091 ( scs_opp_v39 scs_3T7) 2 }`]
3092 THEN MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
3093 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_02_13;STAB_4M8_02_SCS;SCS_K_D_A_STAB_EQ;SCS_4M8_02_IS_SCS]
3094 THEN EXISTS_TAC`0`
3095 THEN EXISTS_TAC`2`
3096 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_02_02]
3097 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
3098 THEN REPEAT RESA_TAC;
3099
3100 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
3101 THEN STRIP_TAC
3102 THEN MATCH_MP_TAC scs_inj
3103 THEN ASM_SIMP_TAC[SCS_3T7_BASIC;SCS_4M8_02_BASIC;J_SCS_4M8_02;BASIC_HALF_SLICE_STAB;J_SCS_3T7;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T7_BASIC;J_SCS_3T7_OPP_PROP;BASIC_HALF_SLICE;D_HALF_SLICE1;Cqaoqlr.BASIC_OPP;SCS_3T7_IS_SCS]
3104 THEN STRIP_TAC;
3105
3106 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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_02;scs_opp_v39]
3107 THEN ARITH_TAC;
3108
3109 STRIP_TAC
3110 THEN
3111 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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_02;scs_opp_v39;peropp2;
3112 ARITH_RULE`(2 + 1 + 4 - 0) MOD 4= 3/\ 0 MOD 4=0/\ a+0=a`;scs_prop_equ_v39]
3113 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3114 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3115 THEN SCS_TAC
3116 THEN REPEAT GEN_TAC
3117 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
3118 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;peropp2;]
3119 THEN RESA_TAC
3120 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
3121 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
3122 THEN RESA_TAC
3123 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3124 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]
3125 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
3126 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
3127 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
3128 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
3129 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
3130 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
3131 THEN ASM_TAC
3132 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/\
3133 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3134 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3135 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
3136 THEN REPEAT RESA_TAC
3137 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)
3138 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
3139 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
3140 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3141 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3142 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
3143 THEN SYM_ASSUM_TAC
3144 THEN SCS_TAC;
3145
3146 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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_02;scs_opp_v39]
3147 THEN ARITH_TAC;
3148
3149 STRIP_TAC
3150 THEN
3151 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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_02;peropp2;scs_opp_v39;
3152 ARITH_RULE`(0 + 1 + 4 - 2) MOD 4= 3/\ 2 MOD 4=2/\ a+0=a`;scs_prop_equ_v39]
3153 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3154 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3155 THEN SCS_TAC
3156 THEN REPEAT GEN_TAC
3157 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
3158 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;peropp2]
3159 THEN RESA_TAC
3160 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
3161 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
3162 THEN RESA_TAC
3163 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3164 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]
3165 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
3166 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
3167 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
3168 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
3169 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
3170 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
3171 THEN ASM_TAC
3172 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/\
3173 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3174 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3175 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
3176 THEN REPEAT RESA_TAC
3177 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)
3178 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
3179 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
3180 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3181 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3182 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
3183 THEN SYM_ASSUM_TAC
3184 THEN SCS_TAC;
3185
3186 REWRITE_TAC[scs_opp_v39]
3187 THEN SCS_TAC
3188 THEN REAL_ARITH_TAC;
3189
3190 REWRITE_TAC[scs_opp_v39]
3191 THEN SCS_TAC
3192 THEN REAL_ARITH_TAC;
3193
3194 REWRITE_TAC[scs_opp_v39]
3195 THEN SCS_TAC
3196 THEN REAL_ARITH_TAC;
3197
3198 REWRITE_TAC[scs_opp_v39]
3199 THEN SCS_TAC
3200 THEN REWRITE_TAC[cstab]
3201 THEN REAL_ARITH_TAC;
3202
3203
3204 SCS_TAC
3205 THEN REWRITE_TAC[cstab]
3206 THEN REAL_ARITH_TAC;
3207
3208 POP_ASSUM MP_TAC
3209 THEN REWRITE_TAC[J_SCS_3T7_OPP_PROP];
3210 ]);;
3211
3212
3213
3214
3215
3216 let SCS_4M8_13_SLICE_13=prove_by_refinement(`scs_arrow_v39 {scs_4M8_13 } {scs_prop_equ_v39  scs_3T7 1}`,
3217 [
3218 ONCE_REWRITE_TAC[SET_RULE`{scs_prop_equ_v39
3219 (  scs_3T7) 1}={scs_prop_equ_v39
3220 (  scs_3T7) 1, scs_prop_equ_v39
3221 (  scs_3T7) 1 }`]
3222 THEN MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
3223 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_13_13;STAB_4M8_13_SCS;SCS_K_D_A_STAB_EQ;SCS_4M8_13_IS_SCS]
3224 THEN EXISTS_TAC`1`
3225 THEN EXISTS_TAC`3`
3226 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_13_13]
3227 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
3228 THEN REPEAT RESA_TAC;
3229
3230 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
3231 THEN STRIP_TAC
3232 THEN MATCH_MP_TAC scs_inj
3233 THEN ASM_SIMP_TAC[SCS_3T7_BASIC;SCS_4M8_13_BASIC;J_SCS_4M8_13;BASIC_HALF_SLICE_STAB;J_SCS_3T7;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T7_BASIC;J_SCS_3T7_1;BASIC_HALF_SLICE;D_HALF_SLICE1;Cqaoqlr.BASIC_OPP;SCS_3T7_IS_SCS]
3234 THEN STRIP_TAC;
3235
3236 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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_13;scs_opp_v39]
3237 THEN ARITH_TAC;
3238
3239 STRIP_TAC
3240 THEN
3241 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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_13;scs_opp_v39;peropp2;
3242 ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
3243 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3244 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3245 THEN SCS_TAC
3246 THEN REPEAT GEN_TAC
3247 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
3248 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;peropp2;]
3249 THEN RESA_TAC
3250 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
3251 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
3252 THEN RESA_TAC
3253 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3254 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]
3255 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
3256 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
3257 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
3258 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
3259 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
3260 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
3261 THEN ASM_TAC
3262 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/\
3263 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3264 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3265 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
3266 THEN REPEAT RESA_TAC
3267 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)
3268 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
3269 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
3270 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3271 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3272 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
3273 THEN SYM_ASSUM_TAC
3274 THEN SCS_TAC;
3275
3276 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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_13;scs_opp_v39]
3277 THEN ARITH_TAC;
3278
3279 STRIP_TAC
3280 THEN
3281 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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_13;peropp2;scs_opp_v39;
3282 ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
3283 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3284 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3285 THEN SCS_TAC
3286 THEN REPEAT GEN_TAC
3287 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
3288 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;peropp2]
3289 THEN RESA_TAC
3290 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
3291 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
3292 THEN RESA_TAC
3293 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3294 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]
3295 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
3296 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
3297 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
3298 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
3299 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
3300 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
3301 THEN ASM_TAC
3302 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/\
3303 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3304 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3305 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
3306 THEN REPEAT RESA_TAC
3307 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)
3308 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
3309 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
3310 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3311 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3312 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
3313 THEN SYM_ASSUM_TAC
3314 THEN SCS_TAC;
3315
3316 REWRITE_TAC[scs_opp_v39]
3317 THEN SCS_TAC
3318 THEN REAL_ARITH_TAC;
3319
3320 REWRITE_TAC[scs_opp_v39]
3321 THEN SCS_TAC
3322 THEN REAL_ARITH_TAC;
3323
3324 REWRITE_TAC[scs_opp_v39]
3325 THEN SCS_TAC
3326 THEN REAL_ARITH_TAC;
3327
3328 REWRITE_TAC[scs_opp_v39]
3329 THEN SCS_TAC
3330 THEN REWRITE_TAC[cstab]
3331 THEN REAL_ARITH_TAC;
3332
3333 SCS_TAC
3334 THEN REWRITE_TAC[cstab]
3335 THEN REAL_ARITH_TAC;
3336
3337 POP_ASSUM MP_TAC
3338 THEN REWRITE_TAC[J_SCS_3T7];
3339 ]);;
3340
3341
3342
3343
3344
3345 let SCS_4M8_13_ARROW_3T7=prove(`scs_arrow_v39 {scs_4M8_13 } {scs_3T7 }`,
3346 MATCH_MP_TAC FZIOTEF_TRANS
3347 THEN EXISTS_TAC`{scs_prop_equ_v39  scs_3T7 1}`
3348 THEN ASM_REWRITE_TAC[SCS_4M8_13_SLICE_13]
3349 THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T7`;`1`;`3`][SCS_3T7_IS_SCS;K_SCS_3T7;ARITH_RULE`(3 - 1 MOD 3)=2`]
3350 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T7 1`;`2`][PROP_EQU_IS_SCS;SCS_3T7_IS_SCS]
3351 THEN DICH_TAC 0
3352 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
3353 THEN REWRITE_TAC[]);;
3354
3355 let K_SCS_OPP_3T7=prove(`scs_k_v39 (scs_opp_v39 scs_3T7) = 3`,
3356 ASM_REWRITE_TAC[scs_opp_v39;scs_prop_equ_v39]
3357 THEN SCS_TAC);;
3358
3359 let SCS_3T7_OPP_IS_SCS=prove(`is_scs_v39 (scs_opp_v39 scs_3T7)`,
3360 MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
3361 THEN EXISTS_TAC`scs_opp_v39 scs_3T7`
3362 THEN ASM_REWRITE_TAC[SCS_3T7_IS_SCS]);;
3363
3364
3365
3366 let SCS_4M8_13_ARROW_3T7_OPP=prove(`scs_arrow_v39 {scs_4M8_02 } {scs_opp_v39 scs_3T7}`,
3367 MATCH_MP_TAC FZIOTEF_TRANS
3368 THEN EXISTS_TAC`{scs_prop_equ_v39
3369 ( scs_opp_v39 scs_3T7) 2}`
3370 THEN ASM_REWRITE_TAC[SCS_4M8_02_SLICE_02]
3371 THEN MRESAS_TAC PRO_EQU_ID1[`scs_opp_v39 scs_3T7`;`2`;`3`][SCS_3T7_IS_SCS;K_SCS_3T7;ARITH_RULE`(3 - 2 MOD 3)=1`;K_SCS_OPP_3T7;SCS_3T7_OPP_IS_SCS]
3372 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 (scs_opp_v39 scs_3T7) 2`;`1`][PROP_EQU_IS_SCS;SCS_3T7_IS_SCS;K_SCS_OPP_3T7;SCS_3T7_OPP_IS_SCS]
3373 THEN DICH_TAC 0
3374 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
3375 THEN REWRITE_TAC[]
3376 THEN STRIP_TAC
3377 THEN MATCH_MP_TAC FZIOTEF_TRANS
3378 THEN EXISTS_TAC`{scs_opp_v39 scs_3T7}`
3379 THEN ASM_REWRITE_TAC[]
3380 THEN ASSUME_TAC SCS_3T7_IS_SCS
3381 THEN MRESA_TAC Yxionxl2.SCS_OPP_REFL[`scs_3T7`]
3382 THEN MRESAS_TAC  YXIONXL2[`3`;`scs_opp_v39 scs_3T7`][K_SCS_OPP_3T7;SCS_3T7_OPP_IS_SCS;ARITH_RULE`~(4<=3)`]);;
3383
3384
3385
3386 let PROP_OPP_4M8_13= prove_by_refinement(
3387 `scs_4M8_13= scs_prop_equ_v39(scs_opp_v39 (scs_4M8_02)) 2 `,
3388 [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;scs_4M8_13;scs_4M8_02]
3389 THEN MATCH_MP_TAC scs_inj
3390 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M8_BASIC;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_13;scs_basic;unadorned_v39;peropp;peropp2]
3391 THEN SCS_TAC
3392 THEN STRIP_TAC;
3393
3394 SET_TAC[];
3395
3396 STRIP_TAC
3397 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;]
3398 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
3399 THEN REPEAT GEN_TAC
3400 THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
3401 THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
3402 THEN SYM_ASSUM_TAC
3403 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
3404 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
3405 THEN SYM_ASSUM_TAC
3406 THEN SYM_ASSUM_TAC
3407 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`)
3408 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
3409 THEN RESA_TAC
3410 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`)
3411 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
3412 THEN RESA_TAC
3413 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
3414 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;
3415
3416
3417
3418
3419 let SCS_4M8_02_ARROW_4M8_13=prove(
3420 `scs_arrow_v39 {scs_4M8_02}{scs_4M8_13}`,
3421 ASM_SIMP_TAC[PROP_OPP_4M8_13]
3422 THEN MATCH_MP_TAC FZIOTEF_TRANS
3423 THEN EXISTS_TAC`{scs_opp_v39 (scs_4M8_02)}`
3424 THEN STRIP_TAC
3425 THENL[
3426 MATCH_MP_TAC (GEN_ALL YXIONXL2)
3427 THEN EXISTS_TAC`4`
3428 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M8_02;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02;SCS_4M8_02_IS_SCS];
3429
3430 MATCH_MP_TAC(GEN_ALL YXIONXL3)
3431 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
3432 THEN EXISTS_TAC`scs_opp_v39 ( scs_4M8_02)`
3433 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M8;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02;SCS_4M8_02_IS_SCS];]);;
3434
3435
3436
3437 let SCS_4M8_02_ARROW_3T7 =prove(`scs_arrow_v39 { scs_4M8_02 } { scs_3T7 }`,
3438 MATCH_MP_TAC FZIOTEF_TRANS
3439 THEN EXISTS_TAC`{scs_4M8_13}`
3440 THEN ASM_SIMP_TAC[SCS_4M8_02_ARROW_4M8_13;SCS_4M8_13_ARROW_3T7]);;
3441
3442
3443 (************************************)
3444
3445 let MIQMCSN=prove(`main_nonlinear_terminal_v11
3446 ==> scs_arrow_v39 { scs_4M8 } ({scs_4M6',scs_3T7,scs_3T4})`,
3447 STRIP_TAC
3448 THEN MATCH_MP_TAC FZIOTEF_TRANS
3449 THEN EXISTS_TAC`({scs_4M6',scs_opp_v39 scs_4M6', scs_4M8_02,scs_4M8_13} UNION {scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j})`
3450 THEN ASM_SIMP_TAC[SCS_4M8_ARROW_STEP_ONE;SET_RULE`{scs_4M6', scs_3T7, scs_3T4}={scs_4M6', scs_3T7}UNION{ scs_3T4}`]
3451 THEN MATCH_MP_TAC FZIOTEF_UNION
3452 THEN ASM_REWRITE_TAC[SET_STAB_4M8_ARROW_3T4;]
3453 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_4M6', scs_3T7}={scs_4M6',scs_4M6', scs_3T7,scs_3T7}`]
3454 THEN ASM_REWRITE_TAC[SET_RULE` {A,B,C,D}=({A,B,C}) UNION {D}`]
3455 THEN MATCH_MP_TAC FZIOTEF_UNION
3456 THEN ASM_REWRITE_TAC[SCS_4M8_13_ARROW_3T7;SET_RULE` {A,B,D}=({A,B}) UNION {D}`]
3457 THEN MATCH_MP_TAC FZIOTEF_UNION
3458 THEN ASM_REWRITE_TAC[SCS_4M8_02_ARROW_3T7;SET_RULE` {A,D}=({A}) UNION {D}`]
3459 THEN MATCH_MP_TAC FZIOTEF_UNION
3460 THEN STRIP_TAC
3461 THENL[
3462 MATCH_MP_TAC FZIOTEF_REFL
3463 THEN REWRITE_TAC[IN_SING]
3464 THEN REPEAT RESA_TAC
3465 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS];
3466
3467 ASSUME_TAC(SCS_4M6_IS_SCS)
3468 THEN ASSUME_TAC K_SCS_OPP_4M6
3469 THEN ASSUME_TAC SCS_4M6_OPP_IS_SCS
3470 THEN MRESA_TAC Yxionxl2.SCS_OPP_REFL[`scs_4M6'`]
3471 THEN MRESAL_TAC YXIONXL2[`4`;`scs_opp_v39 scs_4M6'`][ARITH_RULE`~(4<=3)`]]);;
3472
3473
3474  end;;
3475
3476
3477 (*
3478 let check_completeness_claimA_concl =
3479   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
3480 *)
3481
3482
3483
3484