text_formalization/local/hexagons.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 Hexagons = struct
  16
  17
  18 open Polyhedron;;
  19 open Sphere;;
  20 open Topology;;
  21 open Fan_misc;;
  22 open Planarity;;
  23 open Conforming;;
  24 open Hypermap;;
  25 open Fan;;
  26 open Topology;;
  27 open Wrgcvdr_cizmrrh;;
  28 open Local_lemmas;;
  29 open Collect_geom;;
  30 open Dih2k_hypermap;;
  31 open Wjscpro;;
  32 open Tecoxbm;;
  33 open Hdplygy;;
  34 open Nkezbfc_local;;
  35 open Flyspeck_constants;;
  36 open Gbycpxs;;
  37 open Pcrttid;;
  38 open Local_lemmas1;;
  39 open Pack_defs;;
  40
  41 open Hales_tactic;;
  42
  43 open Appendix;;
  44
  45
  46
  47
  48
  49 open Hypermap;;
  50 open Fan;;
  51 open Wrgcvdr_cizmrrh;;
  52 open Local_lemmas;;
  53 open Flyspeck_constants;;
  54 open Pack_defs;;
  55
  56 open Hales_tactic;;
  57
  58 open Appendix;;
  59
  60
  61 open Zithlqn;;
  62
  63
  64 open Xwitccn;;
  65
  66 open Ayqjtmd;;
  67
  68 open Jkqewgv;;
  69
  70
  71 open Mtuwlun;;
  72
  73
  74 open Uxckfpe;;
  75 open Sgtrnaf;;
  76
  77 open Yxionxl;;
  78
  79 open Qknvmlb;;
  80 open Odxlstcv2;;
  81
  82 open Yxionxl2;;
  83 open Eyypqdw;;
  84 open Ocbicby;;
  85 open Imjxphr;;
  86
  87 open Nuxcoea;;
  88 open Aursipd;;
  89 open Cuxvzoz;;
  90 open Rrcwnsj;;
  91 open Tfitskc;;
  92
  93
  94
  95
  96 let PSORT_5_EXPLICIT=prove(`
  97 psort 5 (0,0)= (0,0)/\
  98 psort 5 (1,1)= (1,1)/\
  99 psort 5 (2,2)= (2,2)/\
 100 psort 5 (3,3)= (3,3)/\
 101 psort 5 (4,4)= (4,4)/\
 102 psort 5 (0,1)= (0,1)/\
 103 psort 5 (0,2)= (0,2)/\
 104 psort 5 (0,3)= (0,3)/\
 105 psort 5 (0,4)= (0,4)/\
 106 psort 5 (1,0)= (0,1)/\
 107 psort 5 (1,2)= (1,2)/\
 108 psort 5 (1,3)= (1,3)/\
 109 psort 5 (1,4)= (1,4)/\
 110 psort 5 (2,0)= (0,2)/\
 111 psort 5 (2,1)= (1,2)/\
 112 psort 5 (2,3)= (2,3)/\
 113 psort 5 (2,4)= (2,4)/\
 114 psort 5 (3,0)= (0,3)/\
 115 psort 5 (3,1)= (1,3)/\
 116 psort 5 (3,2)= (2,3)/\
 117 psort 5 (3,4)= (3,4)/\
 118 psort 5 (4,0)= (0,4)/\
 119 psort 5 (4,1)= (1,4)/\
 120 psort 5 (4,2)= (2,4)/\
 121 psort 5 (4,3)= (3,4)/\
 122 psort 5 (4,5)= (0,4)/\
 123 psort 4 (3,4)= (0,3)/\
 124 psort 3 (2,0)= (0,2)/\
 125 psort 3 (2,1)= (1,2)/\
 126 psort 3 (1,0)= (0,1)`,
 127 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`]);;
 128
 129
 130 let scs_5M3 = new_definition`scs_5M3 = mk_unadorned_v39 5 (#0.616)
 131     (funlist_v39 [(0,1),(&2*h0);(0,2),(cstab);(0,3),(cstab);(1,3),(cstab);(1,4),(cstab);(2,4),(cstab)] (&2) 5)
 132     (funlist_v39 [(0,1),cstab;(0,2),(&6);  (0,3),(&6);   (1,3),(&6);   (1,4),(&6);   (2,4),(&6)] (&2*h0) 5)`;;
 133
 134
 135 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;
 136 Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_5_TAC;
 137 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;
 138 Terminal.FUNLIST_EXPLICIT;Yrtafyh.PSORT_PERIODIC;PSORT_5_EXPLICIT;
 139 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`];;
 140
 141
 142
 143 let sqrt8_LE_6=prove(`sqrt8<= &6`,
 144 REWRITE_TAC[sqrt8]
 145 THEN MATCH_MP_TAC REAL_LE_LSQRT
 146 THEN REAL_ARITH_TAC);;
 147
 148 let sqrt8_LE_CSTAB=prove(`sqrt8<= #3.01`,
 149 REWRITE_TAC[sqrt8]
 150 THEN MATCH_MP_TAC REAL_LE_LSQRT
 151 THEN REAL_ARITH_TAC);;
 152
 153
 154 let LE_sqrt8_2=prove(`&2<=sqrt8`,
 155 REWRITE_TAC[sqrt8]
 156 THEN MATCH_MP_TAC REAL_LE_RSQRT
 157 THEN REAL_ARITH_TAC);;
 158
 159 let LE_sqrt8_2h0=prove(`&2* #1.26<=sqrt8`,
 160 REWRITE_TAC[sqrt8]
 161 THEN MATCH_MP_TAC REAL_LE_RSQRT
 162 THEN REAL_ARITH_TAC);;
 163
 164
 165 let LT_sqrt8_2h0=prove(`&2* #1.26<sqrt8`,
 166 REWRITE_TAC[sqrt8]
 167 THEN MATCH_MP_TAC REAL_LT_RSQRT
 168 THEN REAL_ARITH_TAC);;
 169
 170
 171
 172 (******is_scs*********)
 173
 174 let MOD_PERIODIC=prove(`~(k=0) ==> (i+k) MOD k = i MOD k/\ SUC (i+k) MOD k= SUC i MOD k`,
 175 STRIP_TAC
 176 THEN ONCE_REWRITE_TAC[ARITH_RULE`i+k= 1*k+i`;]
 177 THEN SIMP_TAC[MOD_MULT_ADD;ARITH_RULE`SUC (1 * k + i) =(1 * k + SUC i)`]);;
 178
 179
 180 let SCS_6I1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_6I1`,
 181 [
 182 REWRITE_TAC[scs_6I1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;]
 183 THEN SIMP_TAC[ARITH_RULE`~(6=0)`;MOD_PERIODIC]
 184 THEN REPEAT RESA_TAC
 185 ;
 186
 187 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
 188 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
 189 THEN REWRITE_TAC[];
 190
 191 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
 192 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
 193 THEN REWRITE_TAC[];
 194
 195 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
 196 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
 197 THEN REWRITE_TAC[];
 198
 199 REAL_ARITH_TAC;
 200
 201 REWRITE_TAC[h0]
 202 THEN REAL_ARITH_TAC;
 203
 204 REWRITE_TAC[h0]
 205 THEN REAL_ARITH_TAC;
 206
 207 ASM_SIMP_TAC[ARITH_RULE`~(6=0)`;MOD_LT;h0]
 208 THEN REAL_ARITH_TAC;
 209
 210 REWRITE_TAC[h0;cstab]
 211 THEN REAL_ARITH_TAC;
 212
 213 ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY]
 214 THEN ARITH_TAC]);;
 215
 216 let DIST_LE_IMP_A_LE=prove(`BBs_v39 s v /\ dist(v i,v j) <= a
 217 ==> scs_a_v39 s i j<= a`,
 218 REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39]
 219 THEN REPEAT RESA_TAC
 220 THEN THAYTHE_TAC 2[`i`;`j`]
 221 THEN DICH_TAC 1
 222 THEN DICH_TAC 1
 223 THEN REAL_ARITH_TAC);;
 224
 225
 226
 227 let SCS_3M1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_3M1`,
 228 [SIMP_TAC[scs_3M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.103 < #0.9`;periodic;SET_RULE`{} (i + j) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
 229 THEN REPEAT RESA_TAC;
 230
 231 ARITH_TAC;
 232
 233 SCS_TAC;
 234 SCS_TAC;
 235 SCS_TAC;
 236 SCS_TAC;
 237 SCS_TAC
 238 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 239 SCS_TAC
 240 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 241 SCS_TAC
 242 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 243 SCS_TAC
 244 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 245 SCS_TAC
 246 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 247 SCS_TAC
 248 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 249 SCS_TAC
 250 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 251 SCS_TAC
 252 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
 253 SCS_TAC
 254 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
 255 THEN RESA_TAC
 256 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 257 THEN REWRITE_TAC[];
 258 SCS_TAC
 259 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
 260 THEN RESA_TAC
 261 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 262 THEN REWRITE_TAC[];
 263
 264 SCS_TAC
 265 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
 266 THEN RESA_TAC
 267 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 268 THEN REWRITE_TAC[];
 269
 270 SCS_TAC
 271 THEN REWRITE_TAC[h0;cstab]
 272 THEN REAL_ARITH_TAC;
 273
 274 SCS_TAC;
 275
 276 SCS_TAC
 277 THEN ASM_SIMP_TAC[MOD_LT;h0]
 278 THEN REAL_ARITH_TAC;
 279
 280 SCS_TAC
 281 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
 282 THEN REAL_ARITH_TAC;
 283 SCS_TAC
 284 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
 285 THEN REAL_ARITH_TAC;
 286
 287 MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
 288       (&2 * h0 < funlist_v39 [(0,1),cstab] (&2 * h0) 3 i (SUC i) \/
 289        &2 < funlist_v39 [(0,1),&2 * h0] (&2) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`]
 290 THEN MATCH_DICH_TAC 0
 291 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
 292 THEN ARITH_TAC]);;
 293
 294
 295 let SCS_5M1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5M1`,
 296 [
 297 SIMP_TAC[scs_5M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=5/\ 5<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.616 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
 298 THEN REPEAT RESA_TAC;
 299
 300 SCS_TAC
 301 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 302
 303 SCS_TAC
 304 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 305
 306 SCS_TAC
 307 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 308
 309 SCS_TAC
 310 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 311
 312 SCS_TAC
 313 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 314 SCS_TAC
 315 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 316 SCS_TAC
 317 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 318 SCS_TAC
 319 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 320 SCS_TAC
 321 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 322 THEN RESA_TAC
 323 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 324 THEN REWRITE_TAC[];
 325 SCS_TAC
 326 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 327 THEN RESA_TAC
 328 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 329 THEN REWRITE_TAC[];
 330 SCS_TAC
 331 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 332 THEN RESA_TAC
 333 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 334 THEN REWRITE_TAC[];
 335 SCS_TAC
 336 THEN REWRITE_TAC[h0;cstab]
 337 THEN REAL_ARITH_TAC;
 338 SCS_TAC
 339 THEN REWRITE_TAC[h0;cstab]
 340 THEN REAL_ARITH_TAC;
 341 SCS_TAC
 342 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
 343 THEN REAL_ARITH_TAC;
 344 POP_ASSUM MP_TAC
 345 THEN ARITH_TAC;
 346 SCS_TAC
 347 THEN ASM_SIMP_TAC[h0;cstab;]
 348 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 349 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 350 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 351 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 352 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 353 THEN REAL_ARITH_TAC;
 354 SCS_TAC
 355 THEN ASM_SIMP_TAC[h0;cstab;]
 356 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 357 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 358 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 359 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 360 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`]
 361 THEN SUBGOAL_THEN`{i | i < 5 /\
 362       (&2 * #1.26 < (if psort 5 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/
 363        &2 < (if psort 5 (i,SUC i) = 0,1 then &2 * #1.26 else &2))} ={0}`ASSUME_TAC;
 364
 365 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`]
 366 THEN GEN_TAC
 367 THEN EQ_TAC
 368 THEN RESA_TAC
 369 THEN POP_ASSUM MP_TAC
 370 THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `];
 371
 372 ASM_REWRITE_TAC[Geomdetail.CARD_SING]
 373 THEN ARITH_TAC]);;
 374
 375
 376 let SCS_5I1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5I1`,
 377 [
 378 REWRITE_TAC[scs_5I1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(5=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=5/\ 5<=6/\a<=a/\ ~(5=4)/\ ~(6=0)`;d_tame;REAL_ARITH`#0.4819 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
 379 THEN REPEAT RESA_TAC;
 380
 381 SCS_TAC
 382 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 383
 384 SCS_TAC
 385 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 386
 387 SCS_TAC
 388 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 389
 390 SCS_TAC
 391 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 392
 393 SCS_TAC
 394 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 395
 396 SCS_TAC
 397 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 398
 399 SCS_TAC
 400 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 401
 402 SCS_TAC
 403 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 404
 405 SCS_TAC
 406 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 407
 408 SCS_TAC
 409 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 410 THEN RESA_TAC
 411 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
 412 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
 413 THEN REWRITE_TAC[];
 414
 415 SCS_TAC
 416 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 417 THEN RESA_TAC
 418 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
 419 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
 420 THEN REWRITE_TAC[];
 421
 422 SCS_TAC
 423 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 424 THEN RESA_TAC
 425 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
 426 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
 427 THEN REWRITE_TAC[];
 428
 429 SCS_TAC
 430 THEN REWRITE_TAC[h0;cstab]
 431 THEN REAL_ARITH_TAC;
 432
 433 SCS_TAC
 434 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
 435 THEN REAL_ARITH_TAC;
 436
 437 SCS_TAC
 438 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
 439 THEN REAL_ARITH_TAC;
 440
 441 ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY]
 442 THEN ARITH_TAC]);;
 443
 444
 445 let SCS_5I2_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5I2`,
 446 [
 447 REWRITE_TAC[scs_5I2;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(5=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=5/\ 5<=6/\a<=a/\ ~(5=4)/\ ~(6=0)`;d_tame;REAL_ARITH`#0.616 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
 448 THEN REPEAT RESA_TAC;
 449
 450 SCS_TAC
 451 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 452
 453 SCS_TAC
 454 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 455
 456 SCS_TAC
 457 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 458
 459 SCS_TAC
 460 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 461
 462 SCS_TAC
 463 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 464
 465 SCS_TAC
 466 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 467
 468 SCS_TAC
 469 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 470
 471 SCS_TAC
 472 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 473
 474 SCS_TAC
 475 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 476 THEN RESA_TAC
 477 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
 478 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
 479 THEN REWRITE_TAC[];
 480
 481 SCS_TAC
 482 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 483 THEN RESA_TAC
 484 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
 485 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
 486 THEN REWRITE_TAC[];
 487
 488 SCS_TAC
 489 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 490 THEN RESA_TAC
 491 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
 492 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
 493 THEN REWRITE_TAC[];
 494
 495 SCS_TAC
 496 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 497 THEN RESA_TAC
 498 THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`]
 499 THEN MP_TAC(SET_RULE`(j MOD 5 = SUC i MOD 5 \/ SUC j MOD 5 = i MOD 5)\/ ~(j MOD 5 = SUC i MOD 5 \/ SUC j MOD 5 = i MOD 5)`)
 500 THEN RESA_TAC
 501 THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`];
 502
 503
 504 SCS_TAC
 505 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
 506 THEN MP_TAC(SET_RULE`(j = SUC i MOD 5 \/ SUC j MOD 5 = i )\/ ~(j = SUC i MOD 5 \/ SUC j MOD 5 = i)`)
 507 THEN RESA_TAC
 508 THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2];
 509
 510 SCS_TAC
 511 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
 512 THEN REAL_ARITH_TAC;
 513
 514 ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY]
 515 THEN ARITH_TAC]);;
 516
 517
 518
 519 let SCS_5I3_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5I3`,
 520 [
 521 REWRITE_TAC[scs_5I3;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(5=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=5/\ 5<=6/\a<=a/\ ~(5=4)/\ ~(6=0)`;d_tame;REAL_ARITH`#0.616 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
 522 THEN REPEAT RESA_TAC;
 523
 524 SCS_TAC
 525 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 526
 527 SCS_TAC
 528 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 529
 530 SCS_TAC
 531 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 532
 533 SCS_TAC
 534 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 535
 536 SCS_TAC
 537 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 538
 539 SCS_TAC
 540 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 541
 542 SCS_TAC
 543 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 544
 545 SCS_TAC
 546 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
 547
 548 SCS_TAC
 549 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 550 THEN RESA_TAC
 551 THEN MRESA_TAC Terminal.psort_sym[`5`;`i`;`j`];
 552
 553 SCS_TAC
 554 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 555 THEN RESA_TAC
 556 THEN MRESA_TAC Terminal.psort_sym[`5`;`i`;`j`];
 557
 558 SCS_TAC
 559 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 560 THEN RESA_TAC
 561 THEN MRESA_TAC Terminal.psort_sym[`5`;`i`;`j`];
 562
 563 SCS_TAC
 564 THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`]
 565 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 566 THEN RESA_TAC
 567 THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2h0]
 568 THEN MP_TAC(SET_RULE`psort 5 (i,j) = 0,1\/ ~(psort 5 (i,j) = 0,1)`)
 569 THEN RESA_TAC
 570 THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2h0]
 571 THEN REAL_ARITH_TAC;
 572
 573 SCS_TAC;
 574
 575 SCS_TAC
 576 THEN ASM_SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2h0;MOD_LT]
 577 THEN REAL_ARITH_TAC;
 578
 579 SCS_TAC
 580 THEN ASM_SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2h0;MOD_LT]
 581 THEN MP_TAC(SET_RULE`i MOD 5 = SUC i MOD 5\/ ~(i MOD 5 = SUC i MOD 5)`)
 582 THEN RESA_TAC
 583 THEN REWRITE_TAC[REAL_ARITH`&0 <= #3.01`]
 584 THEN MP_TAC(SET_RULE`psort 5 (i,SUC i) = 0,1\/ ~(psort 5 (i,SUC i) = 0,1)`)
 585 THEN RESA_TAC
 586 THEN REWRITE_TAC[sqrt8_LE_CSTAB]
 587 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 588 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 589 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 590 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 591 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 592 THEN REAL_ARITH_TAC;
 593
 594
 595 SCS_TAC
 596 THEN ASM_SIMP_TAC[h0;cstab;]
 597 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 598 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 599 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 600 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 601 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`]
 602 THEN SUBGOAL_THEN`{i | i < 5 /\
 603       (&2 * #1.26 < (if psort 5 (i,SUC i) = 0,1 then sqrt8 else &2 * #1.26) \/
 604        &2 < (if psort 5 (i,SUC i) = 0,1 then &2 * #1.26 else &2))}
 605 ={0}`ASSUME_TAC;
 606
 607
 608 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`]
 609 THEN GEN_TAC
 610 THEN EQ_TAC
 611 THEN RESA_TAC
 612 THEN POP_ASSUM MP_TAC
 613 THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;LT_sqrt8_2h0];
 614
 615 ASM_REWRITE_TAC[Geomdetail.CARD_SING]
 616 THEN ARITH_TAC]);;
 617
 618
 619 let SCS_5M2_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5M2`,
 620 [
 621 SIMP_TAC[scs_5M2;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=5/\ 5<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.616 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
 622 THEN REPEAT RESA_TAC;
 623
 624 SCS_TAC
 625 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 626
 627 SCS_TAC
 628 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 629
 630 SCS_TAC
 631 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 632
 633 SCS_TAC
 634 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 635
 636 SCS_TAC
 637 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 638
 639 SCS_TAC
 640 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 641
 642 SCS_TAC
 643 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 644
 645 SCS_TAC
 646 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
 647
 648 SCS_TAC
 649 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 650 THEN RESA_TAC
 651 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 652 THEN REWRITE_TAC[];
 653
 654 SCS_TAC
 655 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 656 THEN RESA_TAC
 657 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 658 THEN REWRITE_TAC[];
 659
 660 SCS_TAC
 661 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
 662 THEN RESA_TAC
 663 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 664 THEN REWRITE_TAC[];
 665
 666 SCS_TAC
 667 THEN REWRITE_TAC[h0;cstab]
 668 THEN REAL_ARITH_TAC;
 669
 670 SCS_TAC
 671 THEN REWRITE_TAC[h0;cstab]
 672 THEN REAL_ARITH_TAC;
 673
 674 SCS_TAC
 675 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
 676 THEN REAL_ARITH_TAC;
 677
 678 POP_ASSUM MP_TAC
 679 THEN ARITH_TAC;
 680
 681 SCS_TAC
 682 THEN ASM_SIMP_TAC[h0;cstab;]
 683 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 684 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 685 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 686 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 687 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 688 THEN REAL_ARITH_TAC;
 689
 690 SCS_TAC
 691 THEN ASM_SIMP_TAC[h0;cstab;]
 692 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 693 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 694 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 695 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
 696 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`]
 697 THEN SUBGOAL_THEN`{i | i < 5 /\
 698       (&2 * #1.26 < (if psort 5 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/
 699        &2 < (if psort 5 (i,SUC i) = 0,1 then &2 else &2))} ={0}`ASSUME_TAC;
 700
 701 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`]
 702 THEN GEN_TAC
 703 THEN EQ_TAC
 704 THEN RESA_TAC
 705 THEN POP_ASSUM MP_TAC
 706 THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `];
 707
 708
 709 ASM_REWRITE_TAC[Geomdetail.CARD_SING]
 710 THEN ARITH_TAC]);;
 711
 712
 713
 714
 715 let SCS_4M2_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M2`,
 716 [
 717 SIMP_TAC[scs_4M2;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.3789 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
 718 THEN REPEAT RESA_TAC;
 719
 720 SCS_TAC
 721 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 722
 723 SCS_TAC
 724 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 725
 726 SCS_TAC
 727 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 728
 729 SCS_TAC
 730 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 731
 732 SCS_TAC
 733 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 734
 735 SCS_TAC
 736 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 737
 738 SCS_TAC
 739 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 740
 741 SCS_TAC
 742 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
 743
 744 SCS_TAC
 745 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
 746 THEN RESA_TAC
 747 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 748 THEN REWRITE_TAC[];
 749
 750 SCS_TAC
 751 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
 752 THEN RESA_TAC
 753 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 754 THEN REWRITE_TAC[];
 755
 756
 757 SCS_TAC
 758 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
 759 THEN RESA_TAC
 760 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
 761 THEN REWRITE_TAC[];
 762
 763
 764 SCS_TAC
 765 THEN REWRITE_TAC[h0;cstab]
 766 THEN REAL_ARITH_TAC;
 767
 768 SCS_TAC
 769 THEN REWRITE_TAC[h0;cstab]
 770 THEN REAL_ARITH_TAC;
 771
 772 SCS_TAC
 773 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
 774 THEN REAL_ARITH_TAC;
 775
 776 POP_ASSUM MP_TAC
 777 THEN ARITH_TAC;
 778
 779 SCS_TAC
 780 THEN ASM_SIMP_TAC[h0;cstab;]
 781 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
 782 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
 783 THEN REAL_ARITH_TAC;
 784
 785
 786 SCS_TAC
 787 THEN ASM_SIMP_TAC[h0;cstab;]
 788 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
 789 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`]
 790 THEN SUBGOAL_THEN`{i | i < 4 /\
 791       (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/
 792        &2 < (if psort 4 (i,SUC i) = 0,1 then &2 * #1.26 else &2))} ={0}`ASSUME_TAC;
 793
 794
 795 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`]
 796 THEN GEN_TAC
 797 THEN EQ_TAC
 798 THEN RESA_TAC
 799 THEN POP_ASSUM MP_TAC
 800 THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT];
 801
 802 ASM_REWRITE_TAC[Geomdetail.CARD_SING]
 803 THEN ARITH_TAC;]);;
 804
 805
 806
 807 let SCS_6M1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_6M1`,
 808 [
 809 REWRITE_TAC[scs_6M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;]
 810 THEN SIMP_TAC[ARITH_RULE`~(6=0)`;MOD_PERIODIC]
 811 THEN REPEAT RESA_TAC;
 812
 813 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
 814 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
 815 THEN REWRITE_TAC[];
 816
 817 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
 818 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
 819 THEN REWRITE_TAC[];
 820
 821 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
 822 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
 823 THEN REWRITE_TAC[];
 824
 825 REAL_ARITH_TAC;
 826
 827 REWRITE_TAC[h0;cstab]
 828 THEN REAL_ARITH_TAC;
 829
 830 REWRITE_TAC[h0;cstab]
 831 THEN REAL_ARITH_TAC;
 832
 833 ASM_SIMP_TAC[ARITH_RULE`~(6=0)`;MOD_LT;h0;cstab]
 834 THEN REAL_ARITH_TAC;
 835
 836 REWRITE_TAC[h0;cstab]
 837 THEN REAL_ARITH_TAC;
 838
 839 ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY]
 840 THEN ARITH_TAC]);;
 841
 842
 843 let SCS_6T1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_6T1`,
 844 [
 845 REWRITE_TAC[scs_6T1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;]
 846 THEN REWRITE_TAC[
 847 ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;]
 848 THEN SIMP_TAC[periodic;SET_RULE`{} (i + 6) <=> {} i`
 849 ;periodic2;ARITH_RULE`~(6=0)`;MOD_PERIODIC]
 850 THEN REPEAT RESA_TAC;
 851
 852 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
 853 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
 854 THEN REWRITE_TAC[];
 855
 856 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
 857 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
 858 THEN REWRITE_TAC[];
 859
 860
 861 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
 862 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
 863 THEN REWRITE_TAC[];
 864
 865
 866 REWRITE_TAC[h0;cstab]
 867 THEN REAL_ARITH_TAC;
 868
 869
 870 ASM_SIMP_TAC[h0;cstab;MOD_LT]
 871 THEN REAL_ARITH_TAC;
 872
 873
 874 ASM_SIMP_TAC[h0;cstab;MOD_LT]
 875 THEN REAL_ARITH_TAC;
 876
 877
 878 ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
 879 THEN REWRITE_TAC[REAL_ARITH`~(a<a)/\ ~(&2 * #1.26 < &2)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;h0]
 880 THEN ARITH_TAC]);;
 881
 882
 883
 884
 885
 886 (***************)
 887
 888 let SCS_6I1_BASIC=prove(`scs_basic_v39 scs_6I1`,
 889 SCS_TAC);;
 890
 891 let SCS_6T1_BASIC=prove(`scs_basic_v39 scs_6T1`,
 892 SCS_TAC);;
 893
 894 let SCS_6M1_BASIC=prove(`scs_basic_v39 scs_6M1`,
 895 SCS_TAC);;
 896
 897
 898 let SCS_3M1_BASIC=prove(`scs_basic_v39 scs_3M1`,
 899 SCS_TAC);;
 900
 901
 902 let SCS_3T1_BASIC=prove(`scs_basic_v39 scs_3T1`,
 903 SCS_TAC);;
 904
 905 let SCS_3T4_BASIC=prove(`scs_basic_v39 scs_3T4`,
 906 SCS_TAC);;
 907
 908
 909 let SCS_5M1_BASIC=prove(`scs_basic_v39 scs_5M1`,
 910 SCS_TAC);;
 911
 912 let SCS_5M2_BASIC=prove(`scs_basic_v39 scs_5M2`,
 913 SCS_TAC);;
 914
 915
 916
 917 let SCS_5I1_BASIC=prove(`scs_basic_v39 scs_5I1`,
 918 SCS_TAC);;
 919
 920 let SCS_5I2_BASIC=prove(`scs_basic_v39 scs_5I2`,
 921 SCS_TAC);;
 922
 923 let SCS_5I3_BASIC=prove(`scs_basic_v39 scs_5I3`,
 924 SCS_TAC);;
 925
 926 let SCS_4M2_BASIC=prove(`scs_basic_v39 scs_4M2`,
 927 SCS_TAC);;
 928
 929
 930 let SCS_4M6_BASIC=prove(`scs_basic_v39 scs_4M6'`,
 931 SCS_TAC);;
 932
 933
 934 (******************)
 935
 936 let K_SCS_6I1=prove(`scs_k_v39 scs_6I1=6`,
 937 SCS_TAC);;
 938
 939 let K_SCS_6T1=prove(`scs_k_v39 scs_6T1=6`,
 940 SCS_TAC);;
 941
 942
 943 let K_SCS_3M1=prove(`scs_k_v39 scs_3M1=3`,
 944 SCS_TAC);;
 945
 946 let K_SCS_3T1=prove(`scs_k_v39 scs_3T1=3`,
 947 SCS_TAC);;
 948
 949 let K_SCS_3T4=prove(`scs_k_v39 scs_3T4=3`,
 950 SCS_TAC);;
 951
 952
 953 let K_SCS_5M1=prove(`scs_k_v39 scs_5M1=5`,
 954 SCS_TAC);;
 955
 956 let K_SCS_5M2=prove(`scs_k_v39 scs_5M2=5`,
 957 SCS_TAC);;
 958
 959 let K_SCS_5I1=prove(`scs_k_v39 scs_5I1=5`,
 960 SCS_TAC);;
 961
 962
 963 let K_SCS_5I2=prove(`scs_k_v39 scs_5I2=5`,
 964 SCS_TAC);;
 965
 966
 967 let K_SCS_5I3=prove(`scs_k_v39 scs_5I3=5`,
 968 SCS_TAC);;
 969
 970
 971
 972
 973 let K_SCS_4M2=prove(`scs_k_v39 scs_4M2=4`,
 974 SCS_TAC);;
 975
 976 let K_SCS_4M6=prove(`scs_k_v39 scs_4M6'=4`,
 977 SCS_TAC);;
 978
 979
 980 (******************)
 981
 982 let J_SCS_3M1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3M1 i) i1
 983  j= F`,
 984 SCS_TAC);;
 985
 986 let J_SCS_3T4=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T4 i) i1
 987  j= F`,
 988 SCS_TAC);;
 989
 990
 991 let J_SCS_5M1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5M1 i) i1 j= F`,
 992 SCS_TAC );;
 993
 994 let J_SCS_5I1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5I1 i) i1 j= F`,
 995 SCS_TAC );;
 996
 997 let J_SCS_5I2=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5I2 i) i1 j= F`,
 998 SCS_TAC );;
 999
1000 let J_SCS_5I3=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5I3 i) i1 j= F`,
1001 SCS_TAC );;
1002
1003
1004 let J_SCS_4M2=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M2 i) i1 j= F`,
1005 SCS_TAC );;
1006
1007 let J_SCS_4M6=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M6' i) i1 j= F`,
1008 SCS_TAC );;
1009
1010
1011 (*******************)
1012
1013
1014 let BASIC_MM_EQ_BBPRIME2=prove(`scs_basic_v39 s ==> MMs_v39 s = BBprime2_v39 s `,
1015 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;MMs_v39;Ayqjtmd.unadorned_MMs]);;
1016
1017
1018 let BASIC_MM_EQ_BBPRIME2_POINT=prove(`scs_basic_v39 s ==> MMs_v39 s v= BBprime2_v39 s v`,
1019 SIMP_TAC [BASIC_MM_EQ_BBPRIME2]);;
1020
1021
1022 let DIST_PSORT=prove(`periodic v (k)/\ ~(k=0) /\ psort (k) (i,j) = psort (k) (i',j')
1023 ==>  dist (v i',v j')=  dist (v i,v j)`,
1024 REWRITE_TAC[psort;LET_DEF;LET_END_DEF;]
1025 THEN REPEAT STRIP_TAC
1026 THEN POP_ASSUM MP_TAC
1027 THEN MP_TAC(SET_RULE`i MOD k<= j MOD k\/ ~(i MOD k<= j MOD k)`)
1028 THEN RESA_TAC
1029 THEN MP_TAC(SET_RULE`i' MOD k<= j' MOD k\/ ~(i' MOD k<= j' MOD k)`)
1030 THEN RESA_TAC
1031 THEN REWRITE_TAC[PAIR_EQ]
1032 THEN RESA_TAC
1033 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k`;`v`][ARITH_RULE`~(4=0)`;periodic]
1034 THEN THAYTHEL_ASM_TAC 0[`i`][]
1035 THEN THAYTHEL_ASM_TAC 0[`i'`][]
1036 THEN THAYTHEL_ASM_TAC 0[`j`][]
1037 THEN THAYTHEL_ASM_TAC 0[`j'`][]
1038 THEN SIMP_TAC[DIST_SYM]);;
1039
1040
1041 let STAB_BB=prove(`is_scs_v39 s/\  dist(v i,v j) <= cstab/\
1042 BBs_v39 s v
1043 ==>
1044 BBs_v39 (scs_stab_diag_v39 s i j) v`,
1045 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39]
1046 THEN REPEAT RESA_TAC
1047 THEN THAYTHE_TAC 1[`i'`;`j'`]
1048 THEN DICH_TAC 0
1049 THEN DICH_TAC 4
1050 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j')\/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
1051 THEN RESA_TAC
1052 THEN MP_TAC Wkeidft.PROPERTY_OF_K_SCS
1053 THEN RESA_TAC
1054 THEN ABBREV_TAC`k= scs_k_v39 s`
1055 THEN MRESA_TAC DIST_PSORT[`k`;`i'`;`j'`;`i`;`v`;`j`]
1056 THEN RESA_TAC);;
1057
1058
1059 let SCS_K_D_A_STAB_EQ=prove(`scs_d_v39 (scs_stab_diag_v39 s i j) =scs_d_v39 s
1060 /\ scs_k_v39 (scs_stab_diag_v39 s i j) =scs_k_v39 s
1061 /\(!i' j'. scs_a_v39 (scs_stab_diag_v39 s i j) i' j'= scs_a_v39 s i' j')`,
1062 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39]);;
1063
1064
1065 let DIAG_SCS_M_EQ=prove(`is_scs_v39 s/\ scs_diag (scs_k_v39 s) i j==> scs_M s = scs_M (scs_stab_diag_v39 s i j)`,
1066 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;]
1067 THEN STRIP_TAC
1068 THEN MP_TAC Wkeidft.PROPERTY_OF_K_SCS
1069 THEN RESA_TAC
1070 THEN ASM_SIMP_TAC[Yrtafyh.DIAG_NOT_PSORT]);;
1071
1072
1073 let DIAD_PSORT_IMP_DIAD=prove_by_refinement(`scs_diag k i j /\ ~(k=0)
1074 /\ psort k (i',j') = psort k (i,j)
1075 ==> scs_diag k i' j'`,
1076 [REWRITE_TAC[scs_diag;psort;LET_DEF;LET_END_DEF]
1077 THEN STRIP_TAC
1078 THEN DICH_TAC 0
1079 THEN MP_TAC(SET_RULE`i MOD k<= j MOD k\/ ~(i MOD k<= j MOD k)`)
1080 THEN RESA_TAC
1081 THEN MP_TAC(SET_RULE`i' MOD k<= j' MOD k\/ ~(i' MOD k<= j' MOD k)`)
1082 THEN RESA_TAC
1083 THEN REWRITE_TAC[PAIR_EQ]
1084 THEN RESA_TAC;
1085
1086 MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`i`;`k`]
1087 THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`j`;`k`] ;
1088
1089 MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`j`;`k`]
1090 THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`i`;`k`] ;
1091
1092
1093 MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`j`;`k`]
1094 THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`i`;`k`] ;
1095
1096 MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`i`;`k`]
1097 THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`j`;`k`] ]);;
1098
1099 let PEDSLGV1= prove( `!v i j.
1100     v IN MMs_v39 scs_6I1 /\
1101     scs_diag 6 i j /\
1102     dist(v i,v j) <= cstab ==>
1103     v IN MMs_v39 (scs_stab_diag_v39 scs_6I1 i j)`,
1104 REWRITE_TAC[IN]
1105 THEN REPEAT STRIP_TAC
1106 THEN MP_TAC SCS_6I1_IS_SCS
1107 THEN STRIP_TAC
1108 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6I1`;`v`]
1109 THEN MRESA_TAC DIST_LE_IMP_A_LE[`v`;`scs_6I1`;`i`;`j`;`cstab`]
1110 THEN ASSUME_TAC SCS_6I1_BASIC
1111 THEN ASSUME_TAC K_SCS_6I1
1112 THEN MRESAL_TAC Yrtafyh.YRTAFYH[`scs_6I1`;`i`;`j`][ARITH_RULE`3<6`;]
1113 THEN MP_TAC  Ppbtydq.MXQTIED
1114 THEN REWRITE_TAC[IN]
1115 THEN STRIP_TAC
1116 THEN MATCH_DICH_TAC 0
1117 THEN EXISTS_TAC`scs_6I1`
1118 THEN ASM_SIMP_TAC[STAB_BB;SCS_K_D_A_STAB_EQ;DIAG_SCS_M_EQ;REAL_ARITH`a<=a`]
1119 THEN REPEAT GEN_TAC
1120 THEN REWRITE_TAC[scs_stab_diag_v39;scs_6I1;scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;CS_ADJ]
1121 THEN MP_TAC(SET_RULE`psort 6 (i,j) = psort 6 (i',j')\/ ~(psort 6 (i,j) = psort 6 (i',j'))`)
1122 THEN RESA_TAC
1123 THENL[
1124 MRESAL_TAC DIAD_PSORT_IMP_DIAD[`i`;`j`;`6`;`i'`;`j'`][ARITH_RULE`~(6=0)`]
1125 THEN DICH_TAC 0
1126 THEN REWRITE_TAC[scs_diag;cstab]
1127 THEN RESA_TAC
1128 THEN REAL_ARITH_TAC;
1129 REAL_ARITH_TAC]);;
1130
1131
1132 (****************************)
1133 (****************************)
1134 (****************************)
1135 (****************************)
1136
1137
1138
1139
1140 let K_SCS_6M1=prove(`scs_k_v39 scs_6M1=6/\ scs_d_v39 scs_6M1 = scs_d_v39 scs_6I1`,
1141 REWRITE_TAC[scs_6I1;scs_6M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39]);;
1142
1143
1144 let D_6M1_EQ_6I1=prove(` scs_d_v39 scs_6M1 = scs_d_v39 scs_6I1
1145 `,
1146 REWRITE_TAC[scs_6I1;scs_6M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39]);;
1147
1148
1149 let A_6M1_EQ_6I1_EDGE=prove(`(!i j. scs_a_v39 scs_6M1 i (SUC i) = scs_a_v39 scs_6I1 i (SUC i))`,
1150 REWRITE_TAC[scs_6I1;scs_6M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39]);;
1151
1152 let SCS_M_6I1_EQ_6M1=prove(`scs_M scs_6I1 = scs_M scs_6M1`,
1153 REWRITE_TAC[scs_6I1;scs_6M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39;scs_M]);;
1154
1155
1156
1157 let BB_6I1_IS_BB_6M1=prove_by_refinement(`BBs_v39 scs_6I1 v/\ (!i j. scs_diag 6 i j ==>   cstab <= dist(v i,v j)) ==> BBs_v39 scs_6M1 v`,
1158 [
1159 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_6I1;scs_6M1;CS_ADJ;scs_diag]
1160 THEN REPEAT RESA_TAC
1161 THEN MP_TAC(SET_RULE`i MOD 6= j MOD 6\/ ~(i MOD 6= j MOD 6)`)
1162 THEN RESA_TAC;
1163
1164 THAYTHE_TAC (5-2)[`i`;`j`];
1165
1166 MP_TAC(SET_RULE`SUC i MOD 6= j MOD 6\/ ~(SUC i MOD 6= j MOD 6)`)
1167 THEN RESA_TAC;
1168
1169 THAYTHE_TAC (6-2)[`i`;`j`];
1170
1171 MP_TAC(SET_RULE`i MOD 6= SUC j MOD 6\/ ~(i MOD 6= SUC j MOD 6)`)
1172 THEN RESA_TAC;
1173
1174 THAYTHE_TAC (7-2)[`i`;`j`];
1175
1176 THAYTHE_TAC (7-4)[`i`;`j`];
1177
1178 THAYTHE_TAC (5-2)[`i`;`j`];
1179
1180 MP_TAC(SET_RULE`SUC i MOD 6= j MOD 6\/ ~(SUC i MOD 6= j MOD 6)`)
1181 THEN RESA_TAC;
1182
1183 THAYTHE_TAC (6-2)[`i`;`j`];
1184
1185 MP_TAC(SET_RULE`i MOD 6= SUC j MOD 6\/ ~(i MOD 6= SUC j MOD 6)`)
1186 THEN RESA_TAC;
1187
1188 THAYTHE_TAC (7-2)[`i`;`j`];
1189
1190 THAYTHE_TAC (7-4)[`i`;`j`]]);;
1191
1192 let A_6I1_LE_A_6M1=prove(`scs_a_v39 scs_6I1 i j <= scs_a_v39 scs_6M1 i j`,
1193 REWRITE_TAC[scs_6I1;scs_6M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39;h0;cstab]
1194 THEN REAL_ARITH_TAC);;
1195
1196 let B_6I1_LE_B_6M1=prove(`scs_b_v39 scs_6M1 i j = scs_b_v39 scs_6I1 i j`,
1197 REWRITE_TAC[scs_6I1;scs_6M1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39;h0;cstab]
1198 THEN REAL_ARITH_TAC);;
1199
1200
1201
1202   let PEDSLGV2= prove(`!v.
1203     v IN MMs_v39 scs_6I1 /\
1204     (!i j. scs_diag 6 i j ==>   cstab <= dist(v i,v j)) ==>
1205     v IN MMs_v39 (scs_6M1)`,
1206 REWRITE_TAC[IN]
1207 THEN REPEAT STRIP_TAC
1208 THEN MP_TAC SCS_6I1_IS_SCS
1209 THEN STRIP_TAC
1210 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6I1`;`v`]
1211 THEN ASSUME_TAC SCS_6I1_BASIC
1212 THEN ASSUME_TAC K_SCS_6I1
1213 THEN ASSUME_TAC SCS_6M1_BASIC
1214 THEN ASSUME_TAC K_SCS_6M1
1215 THEN MP_TAC SCS_6M1_IS_SCS
1216 THEN STRIP_TAC
1217 THEN MP_TAC  Ppbtydq.MXQTIED
1218 THEN REWRITE_TAC[IN]
1219 THEN STRIP_TAC
1220 THEN MATCH_DICH_TAC 0
1221 THEN EXISTS_TAC`scs_6I1`
1222 THEN ASM_SIMP_TAC[D_6M1_EQ_6I1;A_6M1_EQ_6I1_EDGE;SCS_M_6I1_EQ_6M1;BB_6I1_IS_BB_6M1;A_6I1_LE_A_6M1;B_6I1_LE_B_6M1;REAL_ARITH`a<=a`]);;
1223
1224
1225
1226
1227
1228 (****************************)
1229 (****************************)
1230 (****************************)
1231 (****************************)
1232
1233
1234 let STAB_6I1_SCS=prove(` scs_diag (scs_k_v39 scs_6I1) i j
1235 ==> is_scs_v39 (scs_stab_diag_v39 scs_6I1 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_6I1 i j)`,
1236 STRIP_TAC
1237 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
1238 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_6I1_IS_SCS;SCS_6I1_BASIC;K_SCS_6I1;
1239 ARITH_RULE`3<6`;LET_DEF;LET_END_DEF;scs_6I1;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
1240 THEN REAL_ARITH_TAC);;
1241
1242
1243
1244 let SCS_DIAG_SCS_6I1_02=prove(`scs_diag (scs_k_v39 scs_6I1) 0 2`,
1245 REWRITE_TAC[K_SCS_6I1;scs_diag]
1246 THEN ARITH_TAC);;
1247
1248
1249 let SCS_DIAG_SCS_6I1_03=prove(`scs_diag (scs_k_v39 scs_6I1) 0 3`,
1250 REWRITE_TAC[K_SCS_6I1;scs_diag]
1251 THEN ARITH_TAC);;
1252
1253
1254
1255 let BASIC_HALF_SLICE_STAB=prove(`scs_basic_v39 s
1256 ==> scs_basic_v39 (scs_half_slice_v39 (scs_stab_diag_v39 s i j) p q d' F)`,
1257 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]
1258 THEN SET_TAC[]);;
1259
1260
1261
1262
1263
1264
1265
1266
1267 let D_HALF_SLICE=prove(`scs_d_v39 (scs_half_slice_v39 (scs_stab_diag_v39 s i j) p q d' mkj)=d'`,
1268 SCS_TAC);;
1269
1270 let BAISC_PROP_EQU=prove(`scs_basic_v39 s ==> scs_basic_v39 (scs_prop_equ_v39 s i)`,
1271 SCS_TAC
1272 THEN SET_TAC[]);;
1273
1274 let K_SCS_PROP_EUQ=prove(`scs_k_v39 (scs_prop_equ_v39 s i)= scs_k_v39 s`,
1275 SCS_TAC);;
1276
1277
1278
1279
1280
1281
1282 let AQICLXA_SLICE=prove_by_refinement(`scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 2 } { scs_prop_equ_v39 scs_3M1 1, scs_prop_equ_v39 scs_5M1 1}`,
1283 [MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
1284 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_6I1_02;STAB_6I1_SCS;SCS_K_D_A_STAB_EQ;]
1285 THEN EXISTS_TAC`0`
1286 THEN EXISTS_TAC`2`
1287 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_6I1_02]
1288 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
1289 THEN REPEAT RESA_TAC;
1290
1291 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
1292 THEN STRIP_TAC
1293 THEN MATCH_MP_TAC scs_inj
1294 THEN ASM_SIMP_TAC[SCS_3M1_BASIC;SCS_5M1_BASIC;SCS_6I1_BASIC;J_SCS_5M1;BASIC_HALF_SLICE_STAB;J_SCS_3M1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ]
1295 THEN STRIP_TAC;
1296
1297 ASM_SIMP_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1]
1298 THEN ARITH_TAC;
1299
1300 STRIP_TAC;
1301
1302 ASM_SIMP_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1;scs_6I1;scs_3M1;
1303 ARITH_RULE`(2 + 1 + 6 - 0) MOD 6= 3/\ 0 MOD 6=0/\ a+0=a`;scs_prop_equ_v39]
1304 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1305 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1306 THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort]
1307 THEN REPEAT GEN_TAC
1308 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1309 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1310 THEN RESA_TAC
1311 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1312 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;]
1313 THEN RESA_TAC
1314 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;Uxckfpe.ARITH_3_TAC]
1315 THEN SIMP_TAC[ARITH_RULE`~(0=2)/\ ~(0=1)/\ 0<=1/\ ~(1=2)`;SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1316 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][Uxckfpe.ARITH_3_TAC]
1317 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][Uxckfpe.ARITH_3_TAC]
1318 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][Uxckfpe.ARITH_3_TAC]
1319 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][Uxckfpe.ARITH_3_TAC]
1320 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][Uxckfpe.ARITH_3_TAC]
1321 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][Uxckfpe.ARITH_3_TAC]
1322 THEN ASM_SIMP_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2`;PAIR_EQ;Uxckfpe.ARITH_3_TAC];
1323
1324
1325 ASM_SIMP_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1;scs_6I1;scs_3M1;
1326 ARITH_RULE`(2 + 1 + 6 - 0) MOD 6= 3/\ 0 MOD 6=0/\ a+0=a`;scs_prop_equ_v39]
1327 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1328 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1329 THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort]
1330 THEN REPEAT GEN_TAC
1331 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1332 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1333 THEN RESA_TAC
1334 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1335 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;]
1336 THEN RESA_TAC
1337 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;Uxckfpe.ARITH_3_TAC]
1338 THEN SIMP_TAC[ARITH_RULE`~(0=2)/\ ~(0=1)/\ 0<=1/\ ~(1=2)/\ 0<=2/\ 0<=0`;SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ]
1339 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][Uxckfpe.ARITH_3_TAC]
1340 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][Uxckfpe.ARITH_3_TAC]
1341 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][Uxckfpe.ARITH_3_TAC]
1342 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][Uxckfpe.ARITH_3_TAC]
1343 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][Uxckfpe.ARITH_3_TAC]
1344 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][Uxckfpe.ARITH_3_TAC]
1345 THEN ASM_SIMP_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2`;PAIR_EQ;Uxckfpe.ARITH_3_TAC];
1346
1347
1348
1349 ASM_SIMP_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1]
1350 THEN ARITH_TAC;
1351
1352 STRIP_TAC
1353 THEN ASM_REWRITE_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1;scs_6I1;scs_3M1;
1354 ARITH_RULE`(0 + 1 + 6 - 2) MOD 6= 5/\ 2 MOD 6=2/\ a+0=a`;scs_prop_equ_v39]
1355 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1356 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1357 THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort]
1358 THEN REPEAT GEN_TAC
1359 THEN MP_TAC(ARITH_RULE`x MOD 5<5==> x MOD 5=0\/ x MOD 5=1\/ x MOD 5=2\/ x MOD 5=3\/ x MOD 5=4`)
1360 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_5_TAC;DIVISION]
1361 THEN RESA_TAC
1362 THEN MP_TAC(ARITH_RULE`x' MOD 5<5==> x' MOD 5=0\/ x' MOD 5=1\/ x' MOD 5=2\/ x' MOD 5=3\/ x' MOD 5=4`)
1363 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_5_TAC;DIVISION;ARITH_RULE`5-1=4`]
1364 THEN RESA_TAC
1365 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1366 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1367 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`0`;`1`][ARITH_RULE`~(5=0)`]
1368 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`1`;`1`][ARITH_RULE`~(5=0)`]
1369 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`2`;`1`][ARITH_RULE`~(5=0)`]
1370 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`3`;`1`][ARITH_RULE`~(5=0)`]
1371 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`4`;`1`][ARITH_RULE`~(5=0)`]
1372 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`0`;`1`][ARITH_RULE`~(5=0)`]
1373 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`1`;`1`][ARITH_RULE`~(5=0)`]
1374 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`2`;`1`][ARITH_RULE`~(5=0)`]
1375 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`3`;`1`][ARITH_RULE`~(5=0)`]
1376 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`4`;`1`][ARITH_RULE`~(5=0)`]
1377 THEN ASM_TAC
1378 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/\
1379 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC]
1380 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1381 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1382 THEN REPEAT RESA_TAC
1383 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)
1384 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1385 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2)
1386 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC];
1387
1388 SCS_TAC
1389 THEN REAL_ARITH_TAC;
1390
1391 SCS_TAC
1392 THEN REAL_ARITH_TAC;
1393
1394 SCS_TAC
1395 THEN REAL_ARITH_TAC;
1396
1397 SCS_TAC
1398 THEN REWRITE_TAC[cstab]
1399 THEN REAL_ARITH_TAC;
1400
1401 SCS_TAC
1402 THEN REWRITE_TAC[cstab]
1403 THEN REAL_ARITH_TAC;
1404
1405 POP_ASSUM MP_TAC
1406 THEN REWRITE_TAC[J_SCS_3M1]]);;
1407
1408
1409
1410 let FZIOTEF_UNION = prove_by_refinement(
1411     `!S1 S2 S3 S4.  scs_arrow_v39 S1 S2 /\ scs_arrow_v39 S3 S4 ==>
1412       scs_arrow_v39 (S1 UNION S3) (S2 UNION S4)`,
1413     (* {{{ proof *)
1414     [
1415       REWRITE_TAC[scs_arrow_v39;UNION;IN_ELIM_THM];
1416       REPEAT WEAKER_STRIP_TAC;
1417       ASM_REWRITE_TAC[];
1418       BY(ASM_MESON_TAC[])
1419     ]);;
1420   (* }}} *)
1421
1422 let  PROP_EQU_IS_SCS=prove(`is_scs_v39 s ==> is_scs_v39 (scs_prop_equ_v39 s i)`,
1423 MRESA_TAC PROP_EQU_IS_SCS[`scs_k_v39 s`;`s`;`i`;`scs_prop_equ_v39 s i`]);;
1424
1425
1426 let AQICLXA=prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 2 } { scs_3M1, scs_5M1 }`,
1427 MATCH_MP_TAC FZIOTEF_TRANS
1428 THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_3M1 1, scs_prop_equ_v39 scs_5M1 1}`
1429 THEN ASM_SIMP_TAC[AQICLXA_SLICE]
1430 THEN REWRITE_TAC[SET_RULE`{a,b}= {a}UNION {b}`]
1431 THEN MATCH_MP_TAC FZIOTEF_UNION
1432 THEN STRIP_TAC
1433 THENL[
1434
1435 MRESAS_TAC PRO_EQU_ID[`scs_3M1`;`3`;`2`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`3-2 MOD 3=1`]
1436 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1 1`;`2`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`3-1=2`]
1437 THEN DICH_TAC 0
1438 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
1439
1440 MRESAS_TAC PRO_EQU_ID[`scs_5M1`;`5`;`4`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_5M1_IS_SCS;K_SCS_5M1;ARITH_RULE`5-4 MOD 5=1`]
1441 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_5M1 1`;`4`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_5M1_IS_SCS;K_SCS_5M1;ARITH_RULE`3-1=2`]
1442 THEN DICH_TAC 0
1443 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])]);;
1444
1445
1446 (****************************)
1447 (****************************)
1448 (****************************)
1449 (****************************)
1450
1451 let FUNOUYH_SLICE=prove_by_refinement(`scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 3 } { scs_prop_equ_v39 scs_4M2 1, scs_prop_equ_v39 scs_4M2 1}`,
1452 [
1453 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
1454 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_6I1_03;STAB_6I1_SCS;SCS_K_D_A_STAB_EQ;]
1455 THEN EXISTS_TAC`0`
1456 THEN EXISTS_TAC`3`
1457 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_6I1_03]
1458 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
1459 THEN REPEAT RESA_TAC;
1460
1461 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
1462 THEN STRIP_TAC
1463 THEN MATCH_MP_TAC scs_inj
1464 THEN ASM_SIMP_TAC[BAISC_PROP_EQU;K_SCS_PROP_EUQ;BASIC_HALF_SLICE_STAB;SCS_4M2_BASIC;J_SCS_4M2;D_HALF_SLICE;SCS_6I1_BASIC;K_SCS_4M2]
1465 THEN STRIP_TAC;
1466
1467
1468 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M2;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1]
1469 THEN ARITH_TAC;
1470
1471
1472 STRIP_TAC
1473 THEN ASM_REWRITE_TAC[scs_half_slice_v39;scs_4M2;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2;scs_6I1;scs_3M1;
1474 ARITH_RULE`(3 + 1 + 6 - 0) MOD 6= 4/\ 0 MOD 6=0/\ a+0=a`;scs_prop_equ_v39]
1475 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1476 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1477 THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort]
1478 THEN REPEAT GEN_TAC
1479 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`)
1480 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION]
1481 THEN RESA_TAC
1482 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`)
1483 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1484 THEN RESA_TAC
1485 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1486 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1487 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
1488 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
1489 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
1490 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
1491 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
1492 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
1493 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
1494 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
1495 THEN ASM_TAC
1496 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/\
1497 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
1498 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1499 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1500 THEN REPEAT RESA_TAC
1501 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)
1502 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1503 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2)
1504 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC];
1505
1506
1507
1508 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M2;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1]
1509 THEN ARITH_TAC;
1510
1511
1512 STRIP_TAC
1513 THEN ASM_REWRITE_TAC[scs_half_slice_v39;scs_4M2;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2;scs_6I1;scs_3M1;
1514 ARITH_RULE`(0 + 1 + 6 - 3) MOD 6= 4/\ 3 MOD 6=3/\ a+0=a`;scs_prop_equ_v39]
1515 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1516 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1517 THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort]
1518 THEN REPEAT GEN_TAC
1519 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`)
1520 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION]
1521 THEN RESA_TAC
1522 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`)
1523 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1524 THEN RESA_TAC
1525 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1526 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1527 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
1528 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
1529 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
1530 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
1531 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
1532 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
1533 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
1534 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
1535 THEN ASM_TAC
1536 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/\
1537 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
1538 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1539 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1540 THEN REPEAT RESA_TAC
1541 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)
1542 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1543 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2)
1544 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\
1545 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC];
1546
1547
1548 SCS_TAC
1549 THEN REAL_ARITH_TAC;
1550
1551 SCS_TAC
1552 THEN REAL_ARITH_TAC;
1553
1554 SCS_TAC
1555 THEN REAL_ARITH_TAC;
1556
1557 SCS_TAC
1558 THEN REWRITE_TAC[cstab;h0]
1559 THEN REAL_ARITH_TAC;
1560
1561 SCS_TAC
1562 THEN REWRITE_TAC[cstab;h0]
1563 THEN REAL_ARITH_TAC;
1564
1565 POP_ASSUM MP_TAC
1566 THEN REWRITE_TAC[J_SCS_4M2]]);;
1567
1568
1569
1570
1571
1572
1573 let FZIOTEF=prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 3 } { scs_4M2}`,
1574 MATCH_MP_TAC FZIOTEF_TRANS
1575 THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_4M2 1, scs_prop_equ_v39 scs_4M2 1}`
1576 THEN ASM_SIMP_TAC[FUNOUYH_SLICE]
1577 THEN REWRITE_TAC[SET_RULE`{a,a}= {a}`]
1578 THEN MRESAS_TAC PRO_EQU_ID[`scs_4M2`;`4`;`3`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_4M2_IS_SCS;K_SCS_4M2;ARITH_RULE`4-3 MOD 4=1`]
1579 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M2 1`;`3`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_4M2_IS_SCS;K_SCS_4M2;ARITH_RULE`3-1=2`]
1580 THEN DICH_TAC 0
1581 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]));;
1582
1583
1584 (****************************)
1585 (****************************)
1586 (****************************)
1587 (****************************)
1588
1589
1590
1591 let h0_LT_B_SCS_6M1=prove(`
1592 (!i j. scs_diag 6 i j ==> &4 * h0 < scs_b_v39 scs_6M1 i j)
1593 /\ (!i j. scs_diag 6 i j ==> scs_a_v39 scs_6M1 i j <= cstab)`,
1594 SCS_TAC
1595 THEN REWRITE_TAC[h0;scs_diag]
1596 THEN REPEAT RESA_TAC
1597 THEN REAL_ARITH_TAC);;
1598
1599
1600
1601 let h0_LT_B_SCS_6I1=prove(
1602 `(!i j. scs_diag 6 i j ==> &4 * h0 < scs_b_v39 scs_6I1 i j)
1603 /\ (!i j. scs_diag 6 i j ==> scs_a_v39 scs_6I1 i j <= cstab)`,
1604 SCS_TAC
1605 THEN REWRITE_TAC[h0;scs_diag;cstab]
1606 THEN REPEAT RESA_TAC
1607 THEN REAL_ARITH_TAC);;
1608
1609
1610 let h0_LT_B_SCS_5I1=prove(`
1611 (!i j. scs_diag 5 i j ==> &4 * h0 < scs_b_v39 scs_5I1 i j)
1612 /\ (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5I1 i j <= cstab)`,
1613 SCS_TAC
1614 THEN REWRITE_TAC[h0;scs_diag;cstab]
1615 THEN REPEAT RESA_TAC
1616 THEN REAL_ARITH_TAC);;
1617
1618
1619 let h0_LT_B_SCS_5I2=prove(`
1620 (!i j. scs_diag 5 i j ==> &4 * h0 < scs_b_v39 scs_5I2 i j)
1621 /\ (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5I2 i j <= cstab)`,
1622 SCS_TAC
1623 THEN REWRITE_TAC[h0;scs_diag;cstab]
1624 THEN REPEAT RESA_TAC
1625 THEN MP_TAC sqrt8_LE_CSTAB
1626 THEN REAL_ARITH_TAC);;
1627
1628 let h0_LT_B_SCS_5M2=prove(`
1629  (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5M2 i j <= cstab)`,
1630 SCS_TAC
1631 THEN REWRITE_TAC[h0;scs_diag;cstab]
1632 THEN REPEAT RESA_TAC
1633 THEN REAL_ARITH_TAC);;
1634
1635 let h0_LT_B_SCS_5M1=prove(` (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5M1 i j <= cstab)`,
1636 SCS_TAC
1637 THEN REWRITE_TAC[h0;scs_diag;cstab]
1638 THEN REPEAT RESA_TAC
1639 THEN MP_TAC sqrt8_LE_CSTAB
1640 THEN REAL_ARITH_TAC);;
1641
1642
1643 (***************)
1644
1645
1646 let h0_EQ_B_SCS_6I1=prove(
1647 `(!i j. scs_diag 6 i j ==> scs_b_v39 scs_6I1 i j= &6)
1648 /\ (!i j. scs_diag 6 i j ==>  scs_a_v39 scs_6I1 i j= &2 *h0)`,
1649 SCS_TAC
1650 THEN REWRITE_TAC[h0;scs_diag;cstab]
1651 THEN REPEAT RESA_TAC);;
1652
1653
1654
1655 let h0_EQ_B_SCS_5I1=prove(
1656 `(!i j. scs_diag 5 i j ==> scs_b_v39 scs_5I1 i j= &6)
1657 /\ (!i j. scs_diag 5 i j ==>  scs_a_v39 scs_5I1 i j= &2 *h0)`,
1658 SCS_TAC
1659 THEN REWRITE_TAC[h0;scs_diag;cstab]
1660 THEN REPEAT RESA_TAC);;
1661
1662 let h0_EQ_B_SCS_5I2=prove(
1663 `(!i j. scs_diag 5 i j ==> scs_b_v39 scs_5I2 i j= &6)
1664 /\ (!i j. scs_diag 5 i j ==>  scs_a_v39 scs_5I2 i j= sqrt8)`,
1665 SCS_TAC
1666 THEN REWRITE_TAC[h0;scs_diag;cstab]
1667 THEN REPEAT RESA_TAC);;
1668
1669
1670
1671
1672
1673
1674 let B_LE_CSTAB_6M1=prove(`
1675 (!i. scs_b_v39 scs_6M1 i (SUC i) <= cstab)/\
1676 (!i. scs_b_v39 scs_6M1 i (SUC i) <= &2*h0)/\
1677  (!i. &2< scs_b_v39 scs_6M1 i (SUC i) )/\
1678 (!i. scs_a_v39 scs_6M1 i (SUC i) = &2)`,
1679 SCS_TAC
1680 THEN SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;h0;cstab]
1681 THEN REAL_ARITH_TAC);;
1682
1683
1684 let B_LE_CSTAB_5I1=prove(`
1685 (!i. scs_b_v39 scs_5I1 i (SUC i) <= cstab)/\
1686 (!i. scs_b_v39 scs_5I1 i (SUC i) <= &2*h0)/\
1687  (!i. &2< scs_b_v39 scs_5I1 i (SUC i) )/\
1688 (!i. scs_a_v39 scs_5I1 i (SUC i) = &2)
1689 `,
1690 SCS_TAC
1691 THEN SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;h0;cstab]
1692 THEN REAL_ARITH_TAC);;
1693
1694 (*********CARD scs_M <=1**************)
1695
1696 let CARD_SCS_M_6M1=prove(`CARD (scs_M scs_6M1) <= 1`,
1697 ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
1698 THEN SCS_TAC
1699 THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
1700 THEN ARITH_TAC);;
1701
1702 let SCS_M_6M1=prove(`(scs_M scs_6M1) ={}`,
1703 ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
1704 THEN SCS_TAC
1705 THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
1706 THEN ARITH_TAC);;
1707
1708
1709
1710 let SCS_M_6T1=prove(`(scs_M scs_6T1) ={}`,
1711 ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
1712 THEN SCS_TAC
1713 THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)/\ ~(&2 * #1.26 < &2)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M;h0]
1714 THEN ARITH_TAC);;
1715
1716 let CARD_SCS_M_5I1=prove(`CARD (scs_M scs_5I1) <= 1`,
1717 ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
1718 THEN SCS_TAC
1719 THEN ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
1720 THEN ARITH_TAC);;
1721
1722
1723 let SCS_M_5I1=prove(`scs_M scs_5I1 ={}`,
1724 ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
1725 THEN SCS_TAC
1726 THEN ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
1727 THEN ARITH_TAC);;
1728
1729
1730 let SCS_M_5M2=prove(`scs_M scs_5M2 ={0}`,
1731 ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
1732 THEN SCS_TAC
1733 THEN ASM_SIMP_TAC[h0;cstab;]
1734 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
1735 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
1736 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
1737 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
1738 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`]
1739 THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`]
1740 THEN GEN_TAC
1741 THEN EQ_TAC
1742 THEN RESA_TAC
1743 THEN POP_ASSUM MP_TAC
1744 THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `];
1745 );;
1746
1747
1748 (*********************)
1749
1750
1751 let SCS_6M1_IMP_SCS_6T1= prove_by_refinement(`main_nonlinear_terminal_v11
1752 ==>(!v.
1753     v IN MMs_v39 scs_6M1 /\
1754     (!i j. scs_diag 6 i j ==>   cstab < dist(v i,v j)) ==>
1755     v IN MMs_v39 (scs_6T1))`,
1756 [REWRITE_TAC[IN]
1757 THEN REPEAT STRIP_TAC
1758 THEN MP_TAC SCS_6M1_IS_SCS
1759 THEN STRIP_TAC
1760 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6M1`;`v`]
1761 THEN ASSUME_TAC SCS_6M1_BASIC
1762 THEN ASSUME_TAC K_SCS_6M1
1763 THEN ASSUME_TAC SCS_6T1_BASIC
1764 THEN ASSUME_TAC K_SCS_6T1
1765 THEN ASSUME_TAC SCS_6T1_IS_SCS
1766 THEN MP_TAC RRCWNSJ
1767 THEN RESA_TAC
1768 THEN THAYTHES_TAC 0[`scs_6M1`;`v`][ARITH_RULE`3<6`;h0_LT_B_SCS_6M1;B_LE_CSTAB_6M1]
1769 THEN MP_TAC Jcyfmrp.JCYFMRP
1770 THEN RESA_TAC
1771 THEN THAYTHES_TAC 0[`scs_6M1`;`v`][ARITH_RULE`3<6`;h0_LT_B_SCS_6M1;B_LE_CSTAB_6M1;IN;CARD_SCS_M_6M1]
1772 THEN MP_TAC Jlxfdmj.JLXFDMJ
1773 THEN RESA_TAC
1774 THEN THAYTHES_TAC 0[`scs_6M1`;`v`;`i`][ARITH_RULE`3<6`;h0_LT_B_SCS_6M1;B_LE_CSTAB_6M1;IN;CARD_SCS_M_6M1;SCS_M_6M1;SET_RULE`(~{} a==> B)<=> B`;ARITH_RULE`i+1=SUC i`]
1775 THEN MP_TAC  Ppbtydq.MXQTIED
1776 THEN REWRITE_TAC[IN]
1777 THEN STRIP_TAC
1778 THEN MATCH_DICH_TAC 0
1779 THEN EXISTS_TAC`scs_6M1`
1780 THEN ASM_SIMP_TAC[SCS_M_6M1;SCS_M_6T1]
1781 THEN STRIP_TAC;
1782
1783 SCS_TAC;
1784
1785
1786 STRIP_TAC;
1787
1788 DICH_TAC(12-4)
1789 THEN ASM_SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;ARITH_RULE`~(6<=3)`]
1790 THEN RESA_TAC;
1791
1792 REPEAT GEN_TAC
1793 THEN THAYTHE_TAC 1[`i'`;`j`]
1794 THEN DICH_TAC 0
1795 THEN DICH_TAC 0
1796 THEN SCS_TAC
1797 THEN MP_TAC(SET_RULE`i' MOD 6= j MOD 6\/ ~(i' MOD 6= j MOD 6)`)
1798 THEN RESA_TAC
1799 THEN MP_TAC(SET_RULE`SUC i' MOD 6= j MOD 6\/ ~(SUC i' MOD 6= j MOD 6)`)
1800 THEN RESA_TAC;
1801
1802 MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6M1`;`v`]
1803 THEN MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_6M1`;`j`;`v:num->real^3`;`SUC i':num`]
1804 THEN REAL_ARITH_TAC;
1805
1806 MP_TAC(SET_RULE`i' MOD 6=SUC j MOD 6\/ ~( i' MOD 6=SUC j MOD 6)`)
1807 THEN RESA_TAC;
1808
1809 MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6M1`;`v`]
1810 THEN MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_6M1`;`i'`;`v:num->real^3`;`SUC j:num`]
1811 THEN ONCE_REWRITE_TAC[DIST_SYM]
1812 THEN ASM_REWRITE_TAC[]
1813 THEN REAL_ARITH_TAC;
1814
1815 STRIP_TAC;
1816
1817 SCS_TAC;
1818
1819 SCS_TAC
1820 THEN REWRITE_TAC[h0;scs_diag]
1821 THEN REAL_ARITH_TAC]);;
1822
1823 let SCS_6I1_IMP_SCS_6T1=prove(`main_nonlinear_terminal_v11
1824 ==>(!v.
1825     v IN MMs_v39 scs_6I1 /\
1826     (!i j. scs_diag 6 i j ==>   cstab < dist(v i,v j)) ==>
1827     v IN MMs_v39 (scs_6T1))`,
1828 REPEAT STRIP_TAC
1829 THEN MP_TAC SCS_6M1_IMP_SCS_6T1
1830 THEN RESA_TAC
1831 THEN MATCH_DICH_TAC 0
1832 THEN ASM_REWRITE_TAC[]
1833 THEN MATCH_MP_TAC PEDSLGV2
1834 THEN ASM_REWRITE_TAC[]
1835 THEN REPEAT STRIP_TAC
1836 THEN THAYTHE_TAC 1[`i`;`j`]
1837 THEN DICH_TAC 0
1838 THEN REAL_ARITH_TAC);;
1839
1840
1841
1842 let SCS_6I1_BERAK_BY_CSTAB= prove_by_refinement(`main_nonlinear_terminal_v11
1843 ==>
1844 scs_arrow_v39 { scs_6I1 } ({ scs_6T1}UNION { scs_stab_diag_v39 scs_6I1 i j| scs_diag 6 i j })`,
1845 [REPEAT GEN_TAC
1846 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
1847 THEN ABBREV_TAC`k=scs_k_v39 s`
1848 THEN REPEAT RESA_TAC;
1849
1850 REWRITE_TAC[SCS_6T1_IS_SCS];
1851
1852 MATCH_MP_TAC Yrtafyh.STAB_IS_SCS
1853 THEN ASM_SIMP_TAC[SCS_6I1_IS_SCS;K_SCS_6I1;SCS_6I1_BASIC;ARITH_RULE`3<6`]
1854 THEN SCS_TAC
1855 THEN REWRITE_TAC[h0;cstab]
1856 THEN REAL_ARITH_TAC;
1857
1858 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_6I1 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_6I1 ==> MMs_v39 s = {}))`);
1859
1860 ASM_REWRITE_TAC[];
1861
1862 ASM_REWRITE_TAC[]
1863 THEN POP_ASSUM MP_TAC
1864 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
1865 THEN REPEAT STRIP_TAC
1866 THEN POP_ASSUM MP_TAC
1867 THEN RESA_TAC
1868 THEN POP_ASSUM MP_TAC
1869 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1870 THEN STRIP_TAC;
1871
1872
1873 MP_TAC(SET_RULE`(!i j. scs_diag 6 i j ==>   cstab < dist(v i,v j))\/ ~((!i j. scs_diag 6 i j ==>   cstab < dist((v:num->real^3) i,v j)))`)
1874 THEN RESA_TAC;
1875
1876 EXISTS_TAC`scs_6T1`
1877 THEN ASM_REWRITE_TAC[]
1878 THEN EXISTS_TAC`v:num->real^3`
1879 THEN MP_TAC SCS_6I1_IMP_SCS_6T1
1880 THEN REWRITE_TAC[IN]
1881 THEN RESA_TAC
1882 THEN MATCH_DICH_TAC 0
1883 THEN ASM_REWRITE_TAC[];
1884
1885 POP_ASSUM MP_TAC
1886 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
1887 THEN STRIP_TAC
1888 THEN MRESAL_TAC PEDSLGV1[`v`;`i`;`j`][IN]
1889 THEN EXISTS_TAC`scs_stab_diag_v39 scs_6I1 i j`
1890 THEN ASM_REWRITE_TAC[]
1891 THEN STRIP_TAC;
1892
1893 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
1894 THEN EXISTS_TAC`i:num`
1895 THEN EXISTS_TAC`j:num`
1896 THEN ASM_REWRITE_TAC[];
1897
1898 EXISTS_TAC`v:num->real^3`
1899 THEN ASM_REWRITE_TAC[]]);;
1900
1901
1902 let PSORT_MOD=prove(`~(k=0)==> psort k (i MOD k,j MOD k)= psort k (i,j)`,
1903 SIMP_TAC[psort;MOD_REFL]);;
1904
1905
1906
1907 (****************************)
1908 (****************************)
1909 (****************************)
1910 (****************************)
1911
1912
1913
1914 let STAB_MOD=prove(`is_scs_v39 s
1915 ==>   scs_stab_diag_v39 s (i MOD (scs_k_v39 s)) (j MOD (scs_k_v39 s))=scs_stab_diag_v39 s i j`,
1916 SCS_TAC
1917 THEN STRIP_TAC
1918 THEN ABBREV_TAC`k=scs_k_v39 s`
1919 THEN ASM_SIMP_TAC[PSORT_MOD;ARITH_RULE`3<=k==> ~(k=0)`]);;
1920
1921 let DIAG_MOD=prove(`~(k=0)==> scs_diag k (i MOD k) (j MOD k)= scs_diag k i j`,
1922 SIMP_TAC[scs_diag;MOD_REFL;Hypermap.lemma_suc_mod]);;
1923
1924 let SET_STAB_6I1=prove(`{ scs_stab_diag_v39 scs_6I1 i j| scs_diag 6 i j }= { scs_stab_diag_v39 scs_6I1 (i MOD 6) (j  MOD 6)| scs_diag 6 (i MOD 6) (j  MOD 6) }`,
1925  ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(6=0)`;]
1926 THEN MRESAL_TAC STAB_MOD[`scs_6I1`][SCS_6I1_IS_SCS;K_SCS_6I1]);;
1927
1928
1929 let DIAG_EQ_ADD=prove(`scs_diag 6 (i MOD 6) (j MOD 6)<=>
1930 ((i MOD 6= (j MOD 6+ 2) MOD 6)\/ (i MOD 6= (j MOD 6+ 3) MOD 6)\/
1931 (j MOD 6=(i MOD 6+2) MOD 6)\/ (j MOD 6= (i MOD 6+ 3) MOD 6))`,
1932 REWRITE_TAC[scs_diag]
1933 THEN MP_TAC(ARITH_RULE`i MOD 6<6==> i MOD 6= 0 \/ i MOD 6= 1 \/i MOD 6= 2 \/
1934 i MOD 6= 3 \/i MOD 6= 4 \/i MOD 6= 5
1935 `)
1936 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`]
1937 THEN RESA_TAC
1938 THEN MP_TAC(ARITH_RULE`j MOD 6<6==> j MOD 6= 0 \/ j MOD 6= 1 \/j MOD 6= 2 \/
1939 j MOD 6= 3 \/j MOD 6= 4 \/j MOD 6= 5
1940 `)
1941 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`]
1942 THEN RESA_TAC
1943 THEN ARITH_TAC);;
1944
1945
1946 let PSORT_EQ_SYM=prove(`psort (scs_k_v39 s) (j,i) = psort (scs_k_v39 s) (j',i')
1947 <=> psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (j',i')`,
1948 GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1949 THEN REWRITE_TAC[]);;
1950
1951 let PSORT_EQ_SYM1=prove(`psort (scs_k_v39 s) (j,i) = (j',i')
1952 <=> psort (scs_k_v39 s) (i,j) = (j',i')`,
1953 GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1954 THEN REWRITE_TAC[]);;
1955
1956
1957 let STAB_SYM=prove(`scs_stab_diag_v39 s i j =
1958  scs_stab_diag_v39 s j i`,
1959 SCS_TAC
1960 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[PSORT_EQ_SYM]
1961 THEN REWRITE_TAC[]);;
1962
1963
1964 let EXPAND_STAB_DIAG=prove_by_refinement(`{scs_stab_diag_v39 scs_6I1 (i MOD 6) (j MOD 6) | i MOD 6 =
1965                                                   (j MOD 6 + 2) MOD 6 \/
1966                                                   i MOD 6 =
1967                                                   (j MOD 6 + 3) MOD 6 \/
1968                                                   j MOD 6 =
1969                                                   (i MOD 6 + 2) MOD 6 \/
1970                                                   j MOD 6 =
1971                                                   (i MOD 6 + 3) MOD 6}=
1972 {scs_stab_diag_v39 scs_6I1 (i+2) i| i<6} UNION
1973 {scs_stab_diag_v39 scs_6I1 (i+3) i|i<6} `,
1974 [
1975 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;UNION]
1976 THEN GEN_TAC
1977 THEN EQ_TAC
1978 THEN RESA_TAC;
1979
1980 MRESAS_TAC STAB_MOD[`scs_6I1`;`j MOD 6 + 2`;`j MOD 6`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`]
1981 THEN MATCH_MP_TAC (SET_RULE`A==> A\/B`)
1982 THEN EXISTS_TAC`j MOD 6`
1983 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`];
1984
1985 MRESAS_TAC STAB_MOD[`scs_6I1`;`j MOD 6 + 3`;`j MOD 6`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`]
1986 THEN MATCH_MP_TAC (SET_RULE`A==> B\/A`)
1987 THEN EXISTS_TAC`j MOD 6`
1988 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`];
1989
1990 MRESAS_TAC STAB_MOD[`scs_6I1`;`i MOD 6`;`i MOD 6 + 2`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`]
1991 THEN MATCH_MP_TAC (SET_RULE`A==> A\/B`)
1992 THEN EXISTS_TAC`i MOD 6`
1993 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`;STAB_SYM];
1994
1995 MRESAS_TAC STAB_MOD[`scs_6I1`;`i MOD 6`;`i MOD 6 + 3`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`]
1996 THEN MATCH_MP_TAC (SET_RULE`A==> B\/A`)
1997 THEN EXISTS_TAC`i MOD 6`
1998 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`;STAB_SYM];
1999
2000 EXISTS_TAC`i+2`
2001 THEN EXISTS_TAC`i:num`
2002 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`;MOD_LT]
2003 THEN MRESAS_TAC STAB_MOD[`scs_6I1`;`i MOD 6 + 2`;`i MOD 6`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`;MOD_LT];
2004
2005 EXISTS_TAC`i+3`
2006 THEN EXISTS_TAC`i:num`
2007 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`;MOD_LT]
2008 THEN MRESAS_TAC STAB_MOD[`scs_6I1`;`i MOD 6 + 3`;`i MOD 6`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`;MOD_LT]]);;
2009
2010
2011 let EQ_DIAG_STAB_6I1_02=prove(`
2012 scs_arrow_v39
2013  {scs_stab_diag_v39 scs_6I1 (i + 2) i }
2014  {scs_stab_diag_v39 scs_6I1 0 2}`,
2015 MRESA_TAC STAB_SYM[`scs_6I1`;`2`;`0`]
2016 THEN MP_TAC (GEN_ALL Wkeidft.WKEIDFT)
2017 THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
2018 THEN STRIP_TAC
2019 THEN MATCH_DICH_TAC 0
2020 THEN ASM_SIMP_TAC[ARITH_RULE`2 + i = (i + 2) + 0/\ 3<6/\ i+1= SUC i`;K_SCS_6I1;h0_LT_B_SCS_6I1;h0_EQ_B_SCS_6I1;SCS_6I1_IS_SCS;SCS_6I1_BASIC]
2021 THEN SCS_TAC
2022 THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
2023 THEN EXISTS_TAC`&0`
2024 THEN EXISTS_TAC`&2`
2025 THEN EXISTS_TAC`&2 *h0`
2026 THEN EXISTS_TAC`&2 *h0`
2027 THEN EXISTS_TAC`&6`
2028 THEN ASM_SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + 2)= i+3/\ SUC i= i+1/\ 2+1=3`;ARITH_RULE`1<6/\ ~(6=0)`;Qknvmlb.SUC_MOD_NOT_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2029 THEN SCS_TAC
2030 THEN MP_TAC(SET_RULE`i= i+0==> i MOD 6= (i+0) MOD 6`)
2031 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
2032 THEN RESA_TAC
2033 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`1<6/\ ~(6=0)`]
2034 THEN SCS_TAC);;
2035
2036
2037 let EQ_DIAG_STAB_6I1_03=prove(`
2038 scs_arrow_v39
2039  {scs_stab_diag_v39 scs_6I1 (i + 3) i }
2040  {scs_stab_diag_v39 scs_6I1 0 3}`,
2041 MRESA_TAC STAB_SYM[`scs_6I1`;`3`;`0`]
2042 THEN MP_TAC (GEN_ALL Wkeidft.WKEIDFT)
2043 THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
2044 THEN STRIP_TAC
2045 THEN MATCH_DICH_TAC 0
2046 THEN ASM_SIMP_TAC[ARITH_RULE`3 + i = (i + 3) + 0/\ 3<6/\ i+1= SUC i`;K_SCS_6I1;h0_LT_B_SCS_6I1;h0_EQ_B_SCS_6I1;SCS_6I1_IS_SCS;SCS_6I1_BASIC]
2047 THEN SCS_TAC
2048 THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
2049 THEN EXISTS_TAC`&0`
2050 THEN EXISTS_TAC`&2`
2051 THEN EXISTS_TAC`&2 *h0`
2052 THEN EXISTS_TAC`&2 *h0`
2053 THEN EXISTS_TAC`&6`
2054 THEN ASM_SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + 3)= i+4/\ SUC i= i+1/\ 3+1=4`;ARITH_RULE`1<6/\ ~(6=0)`;Qknvmlb.SUC_MOD_NOT_EQ;]
2055 THEN SCS_TAC
2056 THEN MP_TAC(SET_RULE`i= i+0==> i MOD 6= (i+0) MOD 6`)
2057 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
2058 THEN RESA_TAC
2059 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`1<6/\ ~(6=0)`]
2060 THEN SCS_TAC);;
2061
2062
2063 let SET_EQ_DIAG_STAB_6I1_02=prove(`
2064 scs_arrow_v39
2065  {scs_stab_diag_v39 scs_6I1 (i + 2) i |i<6}
2066  {scs_stab_diag_v39 scs_6I1 0 2}`,
2067 REWRITE_TAC[ARITH_RULE`i<6<=> i=0\/i=1\/i=2\/i=3\/i=4\/i=5`;SET_RULE`{scs_stab_diag_v39 scs_6I1 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4\/i=5}
2068 = {scs_stab_diag_v39 scs_6I1 (0 + 2) 0} UNION
2069 {scs_stab_diag_v39 scs_6I1 (1 + 2) 1} UNION
2070 {scs_stab_diag_v39 scs_6I1 (2 + 2) 2} UNION
2071 {scs_stab_diag_v39 scs_6I1 (3 + 2) 3} UNION
2072 {scs_stab_diag_v39 scs_6I1 (4 + 2) 4} UNION
2073 {scs_stab_diag_v39 scs_6I1 (5 + 2) 5}
2074 `;]
2075 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`]
2076 THEN MATCH_MP_TAC FZIOTEF_UNION
2077 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02]
2078 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`]
2079 THEN MATCH_MP_TAC FZIOTEF_UNION
2080 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02]
2081 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`]
2082 THEN MATCH_MP_TAC FZIOTEF_UNION
2083 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02]
2084 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`]
2085 THEN MATCH_MP_TAC FZIOTEF_UNION
2086 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02]
2087 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`]
2088 THEN MATCH_MP_TAC FZIOTEF_UNION
2089 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02]);;
2090
2091
2092
2093
2094 let SET_EQ_DIAG_STAB_6I1_03=prove(`
2095 scs_arrow_v39
2096  {scs_stab_diag_v39 scs_6I1 (i + 3) i |i<6}
2097  {scs_stab_diag_v39 scs_6I1 0 3}`,
2098 REWRITE_TAC[ARITH_RULE`i<6<=> i=0\/i=1\/i=2\/i=3\/i=4\/i=5`;SET_RULE`{scs_stab_diag_v39 scs_6I1 (i + 3) i |i=0\/i=1\/i=2\/i=3\/i=4\/i=5}
2099 = {scs_stab_diag_v39 scs_6I1 (0 + 3) 0} UNION
2100 {scs_stab_diag_v39 scs_6I1 (1 + 3) 1} UNION
2101 {scs_stab_diag_v39 scs_6I1 (2 + 3) 2} UNION
2102 {scs_stab_diag_v39 scs_6I1 (3 + 3) 3} UNION
2103 {scs_stab_diag_v39 scs_6I1 (4 + 3) 4} UNION
2104 {scs_stab_diag_v39 scs_6I1 (5 + 3) 5}
2105 `;]
2106 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`]
2107 THEN MATCH_MP_TAC FZIOTEF_UNION
2108 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03]
2109 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`]
2110 THEN MATCH_MP_TAC FZIOTEF_UNION
2111 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03]
2112 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`]
2113 THEN MATCH_MP_TAC FZIOTEF_UNION
2114 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03]
2115 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`]
2116 THEN MATCH_MP_TAC FZIOTEF_UNION
2117 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03]
2118 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`]
2119 THEN MATCH_MP_TAC FZIOTEF_UNION
2120 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03]);;
2121
2122 let SET_EQ_DIAG_STAB_6I1=prove( `scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 i j| scs_diag 6 i j }
2123 { scs_stab_diag_v39 scs_6I1 0 2,  scs_stab_diag_v39 scs_6I1 0 3}`,
2124 ONCE_REWRITE_TAC[SET_STAB_6I1]
2125 THEN REWRITE_TAC[DIAG_EQ_ADD;EXPAND_STAB_DIAG;SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}
2126 ={scs_stab_diag_v39 scs_6I1 0 2}UNION{ scs_stab_diag_v39 scs_6I1 0 3}`]
2127 THEN MATCH_MP_TAC FZIOTEF_UNION
2128 THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_6I1_02;SET_EQ_DIAG_STAB_6I1_03]);;
2129
2130
2131
2132
2133
2134 let OEHDBEN_PRIME=prove( `
2135 main_nonlinear_terminal_v11
2136 ==>
2137 scs_arrow_v39 { scs_6I1 } { scs_6T1, scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}`,
2138 STRIP_TAC
2139 THEN MATCH_MP_TAC FZIOTEF_TRANS
2140 THEN EXISTS_TAC`{ scs_6T1}UNION { scs_stab_diag_v39 scs_6I1 i j| scs_diag 6 i j }`
2141 THEN ASM_SIMP_TAC[SCS_6I1_BERAK_BY_CSTAB;SET_RULE`{scs_6T1, scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}
2142 ={scs_6T1}UNION{ scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}`]
2143 THEN MATCH_MP_TAC FZIOTEF_UNION
2144 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_6I1;]
2145 THEN MATCH_MP_TAC FZIOTEF_REFL
2146 THEN REWRITE_TAC[IN_SING]
2147 THEN REPEAT RESA_TAC
2148 THEN ASM_REWRITE_TAC[SCS_6T1_IS_SCS]);;
2149
2150
2151
2152 let OEHDBEN= prove(`main_nonlinear_terminal_v11
2153 ==>
2154 scs_arrow_v39 { scs_6I1 } { scs_6T1, scs_5M1, scs_4M2, scs_3M1 }`,
2155 STRIP_TAC
2156 THEN MATCH_MP_TAC FZIOTEF_TRANS
2157 THEN EXISTS_TAC`{ scs_6T1, scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}`
2158 THEN ASM_SIMP_TAC[OEHDBEN_PRIME;SET_RULE`{scs_6T1, scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}
2159 = {scs_6T1} UNION {scs_stab_diag_v39 scs_6I1 0 2} UNION{ scs_stab_diag_v39 scs_6I1 0 3}`;
2160 SET_RULE`{ scs_6T1, scs_5M1, scs_4M2, scs_3M1 }={scs_6T1} UNION{  scs_3M1,scs_5M1}UNION {scs_4M2}`]
2161 THEN MATCH_MP_TAC FZIOTEF_UNION
2162 THEN STRIP_TAC
2163 THENL[
2164 MATCH_MP_TAC FZIOTEF_REFL
2165 THEN REWRITE_TAC[IN_SING]
2166 THEN REPEAT RESA_TAC
2167 THEN ASM_REWRITE_TAC[SCS_6T1_IS_SCS];
2168
2169
2170 MATCH_MP_TAC FZIOTEF_UNION
2171 THEN ASM_REWRITE_TAC[AQICLXA;FZIOTEF]]);;
2172
2173
2174
2175
2176
2177
2178  end;;
2179
2180
2181 (*
2182 let check_completeness_claimA_concl =
2183   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
2184 *)
2185
2186
2187
2188