text_formalization/local/UAGHHBM.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 Uaghhbm = 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
  81
  82
  83
  84 let PERIODIC_PSORT=prove(`~(k=0)==>psort (k) (i + k,j) = psort (k) (i,j)/\
  85 psort (k) (i,j+k) = psort (k) (i,j) `,
  86 REWRITE_TAC[psort;LET_DEF;LET_END_DEF;]
  87 THEN STRIP_TAC
  88 THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
  89 THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]);;
  90
  91
  92 let CASE_PSORT=prove(`psort (k) (i,j) = psort (k) (i',j')
  93 ==> (i MOD k=i' MOD k/\ j MOD k= j' MOD k)\/(i MOD k=j' MOD k/\ j MOD k= i' MOD k)`,
  94 REWRITE_TAC[psort;LET_DEF;LET_END_DEF;]
  95 THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k \/ ~(i MOD k <= j MOD k)`)
  96 THEN RESA_TAC
  97 THEN MP_TAC(ARITH_RULE`i' MOD k <= j' MOD k \/ ~(i' MOD k <= j' MOD k)`)
  98 THEN RESA_TAC
  99 THEN REWRITE_TAC[PAIR_EQ]
 100 THEN SET_TAC[]);;
 101
 102 let C_LE_2_IS_SCS=prove(`is_scs_v39 s /\ ~(i MOD scs_k_v39 s=j MOD scs_k_v39 s)
 103 /\ scs_a_v39 s i j <= c
 104 ==> &2<= c`,
 105 REWRITE_TAC[is_scs_v39;periodic2]
 106 THEN ABBREV_TAC`k=scs_k_v39 s`
 107 THEN REPEAT STRIP_TAC
 108 THEN POP_ASSUM MP_TAC
 109 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
 110 THEN RESA_TAC
 111 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
 112 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
 113 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
 114 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
 115 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 116 THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
 117 THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
 118 THEN REPLICATE_TAC (27-15)(POP_ASSUM MP_TAC)
 119 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 120 THEN MRESA_TAC th[`i MOD k`;`j MOD k`])
 121 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
 122 THEN REAL_ARITH_TAC);;
 123
 124
 125
 126 let C_LT_2_IS_SCS=prove(`is_scs_v39 s /\ ~(i MOD scs_k_v39 s=j MOD scs_k_v39 s)
 127 /\ scs_a_v39 s i j < c
 128 ==> &2< c`,
 129 REWRITE_TAC[is_scs_v39;periodic2]
 130 THEN ABBREV_TAC`k=scs_k_v39 s`
 131 THEN REPEAT STRIP_TAC
 132 THEN POP_ASSUM MP_TAC
 133 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
 134 THEN RESA_TAC
 135 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
 136 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
 137 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
 138 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
 139 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 140 THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
 141 THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
 142 THEN REPLICATE_TAC (27-15)(POP_ASSUM MP_TAC)
 143 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 144 THEN MRESA_TAC th[`i MOD k`;`j MOD k`])
 145 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
 146 THEN REAL_ARITH_TAC);;
 147
 148
 149
 150 let A_LE_A_OVERRIDE=prove_by_refinement(
 151 `is_scs_v39 s/\
 152     scs_a_v39 s i j <= c
 153 ==> scs_a_v39 s i' j' <= override (scs_a_v39 s) (scs_k_v39 s) (i,j) c i' j' `,
 154 [
 155
 156 ASM_REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;TRIV_OR_FORALL_THM]
 157 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'))`)
 158 THEN RESA_TAC;
 159
 160 REAL_ARITH_TAC;
 161
 162 REWRITE_TAC[is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
 163 THEN ABBREV_TAC`k=scs_k_v39 s`
 164 THEN REPEAT STRIP_TAC
 165 THEN POP_ASSUM MP_TAC
 166 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
 167 THEN RESA_TAC;
 168
 169 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
 170 THEN ASM_TAC
 171 THEN REWRITE_TAC[periodic2]
 172 THEN REPEAT STRIP_TAC
 173 THEN POP_ASSUM MP_TAC
 174 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
 175 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
 176 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
 177 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
 178 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
 179 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
 180 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
 181 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])]);;
 182
 183
 184
 185
 186
 187
 188
 189 let B_OVERRIDE_LE_B=prove_by_refinement(
 190 `is_scs_v39 s/\
 191   c <= scs_b_v39 s i j
 192 ==> override (scs_b_v39 s) (scs_k_v39 s) (i,j) c i' j' <= scs_b_v39 s i' j'`,
 193 [
 194 ASM_REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;TRIV_OR_FORALL_THM]
 195 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'))`)
 196 THEN RESA_TAC;
 197
 198 REAL_ARITH_TAC;
 199
 200 REWRITE_TAC[is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
 201 THEN ABBREV_TAC`k=scs_k_v39 s`
 202 THEN REPEAT STRIP_TAC
 203 THEN POP_ASSUM MP_TAC
 204 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
 205 THEN RESA_TAC;
 206
 207 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
 208 THEN ASM_TAC
 209 THEN REWRITE_TAC[periodic2]
 210 THEN REPEAT STRIP_TAC
 211 THEN POP_ASSUM MP_TAC
 212 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
 213 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
 214 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
 215 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
 216 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
 217 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
 218 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
 219 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])]);;
 220
 221
 222
 223 let BB_EQ_UNION_BB_SUBDIVISION=prove_by_refinement(`
 224     is_scs_v39 s /\
 225     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j
 226 ==>
 227 BBs_v39 s = BBs_v39 (restriction_cs1_v39 s i j c) UNION BBs_v39 (restriction_cs2_v39 s i j c)`,
 228 [
 229 REWRITE_TAC[is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
 230 THEN ABBREV_TAC`k=scs_k_v39 s`
 231 THEN REPEAT STRIP_TAC
 232 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
 233 THEN RESA_TAC;
 234
 235 REWRITE_TAC[IN]
 236 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;restriction_cs1_v39;restriction_cs2_v39]
 237 THEN EQ_TAC;
 238
 239 RESA_TAC;
 240
 241 ASM_REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;TRIV_OR_FORALL_THM]
 242 THEN MP_TAC(SET_RULE`(!i' j'.
 243       dist ((x:num->real^3) i',x j') <=
 244       (if psort k (i,j) = psort k (i',j') then c else scs_b_v39 s i' j'))\/
 245 ~(!i' j'.
 246       dist (x i',x j') <=
 247       (if psort k (i,j) = psort k (i',j') then c else scs_b_v39 s i' j'))`)
 248 THEN RESA_TAC;
 249
 250 POP_ASSUM MP_TAC
 251 THEN REWRITE_TAC[NOT_FORALL_THM]
 252 THEN RESA_TAC;
 253
 254
 255
 256 POP_ASSUM MP_TAC
 257 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'))`)
 258 THEN RESA_TAC;
 259
 260
 261
 262 REPEAT STRIP_TAC
 263 THEN POP_ASSUM MP_TAC
 264 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''))`)
 265 THEN RESA_TAC;
 266
 267 MRESA_TAC(GEN_ALL CASE_PSORT)[`i':num`;`j'':num`;`j':num`;`i'':num`;`k:num`];
 268
 269 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`x:num->real^3`][ARITH_RULE`~(4=0)`;]
 270 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
 271 THEN MRESAL1_TAC th`i'':num`[ARITH_RULE`4 MOD 4=0`]
 272 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`]
 273 THEN MRESAL1_TAC th`j'':num`[ARITH_RULE`4 MOD 4=0`])
 274 THEN REAL_ARITH_TAC
 275 ;
 276
 277
 278 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`x:num->real^3`][ARITH_RULE`~(4=0)`;]
 279 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
 280 THEN MRESAL1_TAC th`i'':num`[ARITH_RULE`4 MOD 4=0`]
 281 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`]
 282 THEN MRESAL1_TAC th`j'':num`[ARITH_RULE`4 MOD 4=0`])
 283 THEN STRIP_TAC
 284 THEN ONCE_REWRITE_TAC[DIST_SYM]
 285 THEN POP_ASSUM MP_TAC
 286 THEN REAL_ARITH_TAC;
 287
 288
 289
 290
 291
 292 ASM_REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;TRIV_OR_FORALL_THM]
 293 THEN MP_TAC(SET_RULE`(!i' j'.
 294       dist ((x:num->real^3) i',x j') <=
 295       (if psort k (i,j) = psort k (i',j') then c else scs_b_v39 s i' j'))\/
 296 ~(!i' j'.
 297       dist (x i',x j') <=
 298       (if psort k (i,j) = psort k (i',j') then c else scs_b_v39 s i' j'))`)
 299 THEN RESA_TAC;
 300
 301 POP_ASSUM MP_TAC
 302 THEN REWRITE_TAC[NOT_FORALL_THM]
 303 THEN RESA_TAC;
 304
 305
 306
 307 POP_ASSUM MP_TAC
 308 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'))`)
 309 THEN RESA_TAC;
 310
 311 REPEAT STRIP_TAC
 312 THEN POP_ASSUM MP_TAC
 313 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''))`)
 314 THEN RESA_TAC;
 315
 316 MRESA_TAC(GEN_ALL CASE_PSORT)[`i':num`;`j'':num`;`j':num`;`i'':num`;`k:num`];
 317
 318 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`x:num->real^3`][ARITH_RULE`~(4=0)`;]
 319 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
 320 THEN MRESAL1_TAC th`i'':num`[ARITH_RULE`4 MOD 4=0`]
 321 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`]
 322 THEN MRESAL1_TAC th`j'':num`[ARITH_RULE`4 MOD 4=0`])
 323 THEN REAL_ARITH_TAC
 324 ;
 325
 326
 327 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`x:num->real^3`][ARITH_RULE`~(4=0)`;]
 328 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
 329 THEN MRESAL1_TAC th`i'':num`[ARITH_RULE`4 MOD 4=0`]
 330 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`]
 331 THEN MRESAL1_TAC th`j'':num`[ARITH_RULE`4 MOD 4=0`])
 332 THEN STRIP_TAC
 333 THEN ONCE_REWRITE_TAC[DIST_SYM]
 334 THEN POP_ASSUM MP_TAC
 335 THEN REAL_ARITH_TAC;
 336
 337 RESA_TAC;
 338
 339 REPEAT GEN_TAC
 340 THEN REMOVE_ASSUM_TAC
 341 THEN POP_ASSUM(fun th-> MRESA_TAC th[`i':num`;`j':num`])
 342 THEN MP_TAC B_OVERRIDE_LE_B
 343 THEN ASM_REWRITE_TAC[is_scs_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
 344 THEN REPLICATE_TAC (27-18)(POP_ASSUM MP_TAC)
 345 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 346 THEN POP_ASSUM MP_TAC
 347 THEN POP_ASSUM MP_TAC
 348 THEN MP_TAC th
 349 THEN RESA_TAC)
 350 THEN REAL_ARITH_TAC;
 351
 352 REPEAT GEN_TAC
 353 THEN REMOVE_ASSUM_TAC
 354 THEN POP_ASSUM(fun th-> MRESA_TAC th[`i':num`;`j':num`])
 355 THEN MP_TAC B_OVERRIDE_LE_B
 356 THEN ASM_REWRITE_TAC[is_scs_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
 357 THEN REPLICATE_TAC (27-18)(POP_ASSUM MP_TAC)
 358 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 359 THEN POP_ASSUM MP_TAC
 360 THEN POP_ASSUM MP_TAC
 361 THEN MP_TAC th
 362 THEN RESA_TAC)
 363 THEN REAL_ARITH_TAC;
 364
 365 REPEAT GEN_TAC
 366 THEN REMOVE_ASSUM_TAC
 367 THEN POP_ASSUM(fun th-> MRESA_TAC th[`i':num`;`j':num`])
 368 THEN REMOVE_ASSUM_TAC
 369 THEN MP_TAC A_LE_A_OVERRIDE
 370 THEN ASM_REWRITE_TAC[is_scs_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
 371 THEN REPLICATE_TAC (26-18)(POP_ASSUM MP_TAC)
 372 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 373 THEN POP_ASSUM MP_TAC
 374 THEN POP_ASSUM MP_TAC
 375 THEN MP_TAC th
 376 THEN RESA_TAC)
 377 THEN REAL_ARITH_TAC
 378 ;
 379 REPEAT GEN_TAC
 380 THEN REMOVE_ASSUM_TAC
 381 THEN POP_ASSUM(fun th-> MRESA_TAC th[`i':num`;`j':num`])
 382 THEN REMOVE_ASSUM_TAC
 383 THEN MP_TAC A_LE_A_OVERRIDE
 384 THEN ASM_REWRITE_TAC[is_scs_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
 385 THEN REPLICATE_TAC (26-18)(POP_ASSUM MP_TAC)
 386 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 387 THEN POP_ASSUM MP_TAC
 388 THEN POP_ASSUM MP_TAC
 389 THEN MP_TAC th
 390 THEN RESA_TAC)
 391 THEN REAL_ARITH_TAC;
 392 ]);;
 393
 394
 395 let SUBDIVISION_IS_NOT_EAR=prove(`3< scs_k_v39 s
 396 ==>
 397 ~(is_ear_v39 s)/\ ~(is_ear_v39 (restriction_cs1_v39 s i j c)) /\ ~(is_ear_v39 (restriction_cs2_v39 s i j c))`,
 398 REWRITE_TAC[is_scs_v39;is_ear_v39;restriction_cs1_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;unadorned_v39;restriction_cs2_v39]
 399 THEN RESA_TAC
 400 THEN MP_TAC(ARITH_RULE`3< scs_k_v39 s ==> ~(scs_k_v39 s =3)`)
 401 THEN RESA_TAC);;
 402
 403
 404
 405 let SUBDIVISION_CS1_DSV_EQ=prove(`
 406    3< scs_k_v39 s
 407 ==>
 408 dsv_v39 (restriction_cs1_v39 s i j c) ww =dsv_v39 s ww
 409 /\ dsv_v39 (restriction_cs2_v39 s i j c) ww =dsv_v39 s ww`,
 410 STRIP_TAC
 411 THEN MP_TAC SUBDIVISION_IS_NOT_EAR
 412 THEN RESA_TAC
 413 THEN ASM_REWRITE_TAC[dsv_v39]
 414 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;dsv_v39;restriction_cs1_v39;restriction_cs2_v39]);;
 415
 416
 417 let SUBDIVISION_CS1_TAUSTAR_EQ=prove(`
 418    3< scs_k_v39 s
 419 ==>
 420 taustar_v39 (restriction_cs1_v39 s i j c) ww =taustar_v39 s ww /\
 421 taustar_v39 (restriction_cs2_v39 s i j c) ww =taustar_v39 s ww`,
 422 STRIP_TAC
 423 THEN MP_TAC SUBDIVISION_CS1_DSV_EQ
 424 THEN RESA_TAC
 425 THEN ASM_REWRITE_TAC[taustar_v39]
 426 THEN MP_TAC(ARITH_RULE`3< scs_k_v39 s ==> ~(scs_k_v39 s <=3)`)
 427 THEN RESA_TAC
 428 THEN ASM_REWRITE_TAC[MMs_v39;BBprime2_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;taustar_v39;restriction_cs1_v39;restriction_cs2_v39]);;
 429
 430
 431
 432 let BBPRIME_SUBSET_SUBDIVISION_UNION=prove_by_refinement(`
 433     is_scs_v39 s /\    3< scs_k_v39 s /\
 434     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
 435     BBprime_v39 s ww
 436 ==>
 437  ww IN BBprime_v39 (restriction_cs1_v39 s i j c) UNION BBprime_v39 (restriction_cs2_v39 s i j c)`,
 438 [
 439 STRIP_TAC
 440 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
 441 THEN RESA_TAC
 442 THEN ASM_TAC
 443 THEN
 444 REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
 445 THEN ABBREV_TAC`k=scs_k_v39 s`
 446 THEN REPEAT STRIP_TAC
 447 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
 448 THEN RESA_TAC;
 449
 450 REWRITE_TAC[IN]
 451 THEN ASM_REWRITE_TAC[BBprime_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;]
 452 THEN POP_ASSUM MP_TAC
 453 THEN POP_ASSUM (fun th-> STRIP_TAC
 454 THEN MRESAL1_TAC th`ww:num->real^3`[IN]
 455 THEN ASSUME_TAC(th));
 456
 457 MATCH_MP_TAC(SET_RULE`A==> A\/B`)
 458 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
 459 THEN GEN_TAC
 460 THEN REMOVE_ASSUM_TAC
 461 THEN REMOVE_ASSUM_TAC
 462 THEN POP_ASSUM(fun th-> STRIP_TAC
 463 THEN MRESAL1_TAC th`ww':num->real^3`[IN])
 464 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
 465 THEN REPLICATE_TAC (32-25)(POP_ASSUM MP_TAC)
 466 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 467 THEN MATCH_MP_TAC th)
 468 THEN ASM_REWRITE_TAC[];
 469
 470 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
 471 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
 472 THEN GEN_TAC
 473 THEN REMOVE_ASSUM_TAC
 474 THEN REMOVE_ASSUM_TAC
 475 THEN POP_ASSUM(fun th-> STRIP_TAC
 476 THEN MRESAL1_TAC th`ww':num->real^3`[IN])
 477 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
 478 THEN REPLICATE_TAC (32-25)(POP_ASSUM MP_TAC)
 479 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 480 THEN MATCH_MP_TAC th)
 481 THEN ASM_REWRITE_TAC[]]);;
 482
 483
 484
 485 let BBPRIME_SUBSET_BBPRIME_SUBDIVISION_UNION = prove(
 486 `is_scs_v39 s /\    3< scs_k_v39 s /\
 487     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j
 488  ==>   BBprime_v39 s SUBSET BBprime_v39 (restriction_cs1_v39 s i j c) UNION BBprime_v39 (restriction_cs2_v39 s i j c)`,
 489 REWRITE_TAC[SUBSET]
 490 THEN REPEAT STRIP_TAC
 491 THEN MATCH_MP_TAC  BBPRIME_SUBSET_SUBDIVISION_UNION
 492 THEN ASM_REWRITE_TAC[]
 493 THEN POP_ASSUM MP_TAC
 494 THEN REWRITE_TAC[IN]);;
 495
 496
 497 (**********c< norm(ww i- ww j)*********)
 498
 499 let BBINDEX_EQ_SUBDIVISION=prove_by_refinement(
 500 `
 501     is_scs_v39 s /\    3< scs_k_v39 s /\
 502     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
 503     BBs_v39 s ww /\ c< norm(ww i- ww j)
 504 ==>
 505 BBindex_v39 s ww = BBindex_v39 (restriction_cs2_v39 s i j c) ww`,
 506 [
 507 STRIP_TAC
 508 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
 509 THEN RESA_TAC
 510 THEN ASM_TAC
 511 THEN REWRITE_TAC[BBindex_v39]
 512 THEN
 513 REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs2_v39]
 514 THEN ABBREV_TAC`k=scs_k_v39 s`
 515 THEN REPEAT STRIP_TAC
 516 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
 517 THEN RESA_TAC;
 518
 519 MATCH_MP_TAC CARD_IMAGE_INJ_EQ
 520 THEN REWRITE_TAC[IN_ELIM_THM]
 521 THEN EXISTS_TAC`(\i:num. i)`
 522 THEN STRIP_TAC;
 523
 524 MATCH_MP_TAC FINITE_SUBSET
 525 THEN EXISTS_TAC`0..k`
 526 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
 527 THEN ARITH_TAC;
 528
 529 STRIP_TAC;
 530
 531 REPEAT RESA_TAC
 532 THEN POP_ASSUM MP_TAC
 533 THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
 534 THEN RESA_TAC;
 535
 536 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`];
 537
 538 ASM_TAC
 539 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
 540 THEN REPEAT STRIP_TAC
 541 THEN REPLICATE_TAC (32-25)(POP_ASSUM MP_TAC)
 542 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 543 THEN MP_TAC th)
 544 THEN POP_ASSUM MP_TAC
 545 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
 546 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
 547 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
 548 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
 549 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;dist])
 550 THEN REAL_ARITH_TAC;
 551
 552 ASM_TAC
 553 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
 554 THEN REPEAT STRIP_TAC
 555 THEN REPLICATE_TAC (32-25)(POP_ASSUM MP_TAC)
 556 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 557 THEN MP_TAC th)
 558 THEN POP_ASSUM MP_TAC
 559 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
 560 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
 561 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
 562 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
 563 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
 564 THEN ONCE_REWRITE_TAC[DIST_SYM]
 565 THEN REWRITE_TAC[dist]
 566 THEN REAL_ARITH_TAC;
 567
 568 REPEAT RESA_TAC;
 569
 570 REWRITE_TAC[EXISTS_UNIQUE]
 571 THEN EXISTS_TAC`y:num`
 572 THEN ASM_REWRITE_TAC[]
 573 THEN REPEAT RESA_TAC
 574 THEN POP_ASSUM MP_TAC
 575 THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (y,SUC y) \/ ~(psort k (i,j) = psort k (y,SUC y))`)
 576 THEN RESA_TAC;
 577
 578 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC y:num`;`j:num`;`y:num`;`k:num`];
 579
 580 ASM_TAC
 581 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
 582 THEN REPEAT STRIP_TAC
 583 THEN REPLICATE_TAC (32-25)(POP_ASSUM MP_TAC)
 584 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 585 THEN MP_TAC th)
 586 THEN POP_ASSUM MP_TAC
 587 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
 588 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
 589 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
 590 THEN MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`]
 591 THEN MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`;])
 592 THEN REPLICATE_TAC (37-22)(POP_ASSUM MP_TAC)
 593 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 594 THEN MP_TAC th)
 595 THEN ASM_TAC
 596 THEN REWRITE_TAC[periodic2]
 597 THEN REPEAT DISCH_TAC
 598 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
 599 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
 600 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
 601 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
 602 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
 603 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 604 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
 605 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
 606 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
 607 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`;dist])
 608 THEN REAL_ARITH_TAC;
 609
 610 ASM_TAC
 611 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
 612 THEN REPEAT STRIP_TAC
 613 THEN REPLICATE_TAC (35-28)(POP_ASSUM MP_TAC)
 614 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 615 THEN MP_TAC th)
 616 THEN POP_ASSUM MP_TAC
 617 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
 618 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
 619 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
 620 THEN MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`]
 621 THEN MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`;])
 622 THEN REPLICATE_TAC (37-22)(POP_ASSUM MP_TAC)
 623 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 624 THEN MP_TAC th)
 625 THEN ASM_TAC
 626 THEN REWRITE_TAC[periodic2]
 627 THEN REPEAT DISCH_TAC
 628 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
 629 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
 630 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
 631 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
 632 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
 633 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 634 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
 635 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
 636 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
 637 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`;])
 638 THEN ONCE_REWRITE_TAC[DIST_SYM]
 639 THEN REWRITE_TAC[dist]
 640 THEN REAL_ARITH_TAC;]);;
 641
 642
 643 let BB_INTER_BBPRIME_SUBDIVISION2= prove_by_refinement(`
 644     is_scs_v39 s /\    3< scs_k_v39 s /\
 645     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j
 646 ==>
 647 (BBprime_v39 s) INTER (BBs_v39 (restriction_cs2_v39 s i j c)) SUBSET
 648 (BBprime_v39 (restriction_cs2_v39 s i j c))`,
 649 [
 650 STRIP_TAC
 651 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
 652 THEN RESA_TAC
 653 THEN REWRITE_TAC[INTER;EXTENSION;IN_ELIM_THM;SUBSET]
 654 THEN GEN_TAC;
 655
 656 REWRITE_TAC[SUBSET;UNION;IN_ELIM_THM;]
 657 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
 658 THEN
 659 REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;BBprime_v39;IN]
 660 THEN ASM_REWRITE_TAC[]
 661 THEN REPEAT RESA_TAC;
 662
 663 REPLICATE_TAC (11-6)(POP_ASSUM MP_TAC)
 664 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 665 THEN MRESA1_TAC th`ww':num->real^3`)
 666 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
 667 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
 668 THEN REPLICATE_TAC (13-5)(POP_ASSUM MP_TAC)
 669 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 670 THEN MATCH_MP_TAC th)
 671 THEN ASM_REWRITE_TAC[];
 672
 673 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`];
 674
 675 REPLICATE_TAC (10-6)(POP_ASSUM MP_TAC)
 676 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 677 THEN MRESA1_TAC th`ww':num->real^3`)
 678 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
 679 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
 680 THEN REPLICATE_TAC (14-7)(POP_ASSUM MP_TAC)
 681 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 682 THEN MATCH_MP_TAC th)
 683 THEN ASM_REWRITE_TAC[];
 684
 685 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]]);;
 686
 687
 688
 689
 690 let CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION= prove_by_refinement(`
 691     is_scs_v39 s /\    3< scs_k_v39 s /\
 692     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
 693 BBprime_v39 s ww /\ c< norm(ww i- ww j)
 694 ==>
 695 BBs_v39 (restriction_cs2_v39 s i j c) ww`,
 696 [
 697 REWRITE_TAC[MMs_v39;BBs_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;restriction_cs2_v39]
 698 THEN ABBREV_TAC`k=scs_k_v39 s`
 699 THEN RESA_TAC
 700 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
 701 THEN REPEAT RESA_TAC;
 702
 703 POP_ASSUM MP_TAC
 704 THEN POP_ASSUM(fun th-> STRIP_TAC
 705 THEN MP_TAC th)
 706 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'))`)
 707 THEN RESA_TAC;
 708
 709 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];
 710
 711 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
 712 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
 713 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
 714 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
 715 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
 716 THEN REAL_ARITH_TAC;
 717
 718 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
 719 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
 720 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
 721 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
 722 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
 723 THEN ONCE_REWRITE_TAC[DIST_SYM]
 724 THEN REWRITE_TAC[dist]
 725 THEN REAL_ARITH_TAC;
 726
 727 POP_ASSUM MP_TAC
 728 THEN POP_ASSUM(fun th-> STRIP_TAC
 729 THEN MP_TAC th)
 730 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'))`)
 731 THEN RESA_TAC;
 732
 733 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];
 734
 735 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
 736 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
 737 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
 738 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
 739 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
 740 THEN REAL_ARITH_TAC;
 741
 742 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
 743 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
 744 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
 745 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
 746 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
 747 THEN ONCE_REWRITE_TAC[DIST_SYM]
 748 THEN REWRITE_TAC[dist]
 749 THEN REAL_ARITH_TAC]);;
 750
 751 let BBPRIME_SUBDIVISION2_SUBSET_BBPRIME=prove_by_refinement(`
 752     is_scs_v39 s /\    3< scs_k_v39 s /\
 753     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
 754 BBprime_v39 s ww /\ c< norm(ww i- ww j)
 755 ==>
 756 (BBprime_v39 (restriction_cs2_v39 s i j c)) SUBSET (BBprime_v39 s)  `,
 757 [
 758 STRIP_TAC
 759 THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION
 760 THEN RESA_TAC
 761 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
 762 THEN ASM_REWRITE_TAC[EXTENSION;IN]
 763 THEN ASM_TAC
 764 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
 765 THEN ABBREV_TAC`k=scs_k_v39 s`
 766 THEN REPEAT RESA_TAC;
 767
 768 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
 769 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
 770 THEN REPLICATE_TAC (37-31)(POP_ASSUM MP_TAC)
 771 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 772 THEN MRESA1_TAC th`ww:num->real^3`)
 773 THEN REPLICATE_TAC (37-29)(POP_ASSUM MP_TAC)
 774 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 775 THEN MRESA1_TAC th`ww':num->real^3`)
 776 THEN REPLICATE_TAC (37-25)(POP_ASSUM MP_TAC)
 777 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 778 THEN MRESA1_TAC th`ww':num->real^3`)
 779 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
 780 THEN REAL_ARITH_TAC;
 781
 782 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
 783 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
 784 THEN REPLICATE_TAC (37-31)(POP_ASSUM MP_TAC)
 785 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 786 THEN MRESA1_TAC th`ww:num->real^3`)
 787 THEN REPLICATE_TAC (37-29)(POP_ASSUM MP_TAC)
 788 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 789 THEN MRESA1_TAC th`ww':num->real^3`)
 790 THEN REPLICATE_TAC (37-25)(POP_ASSUM MP_TAC)
 791 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 792 THEN MRESA1_TAC th`ww':num->real^3`)
 793 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
 794 THEN REAL_ARITH_TAC;
 795
 796 POP_ASSUM MP_TAC
 797 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]]);;
 798
 799
 800
 801 let IN_BBPRIME_SUBDIVISION=prove_by_refinement(`
 802     is_scs_v39 s /\    3< scs_k_v39 s /\
 803     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
 804 BBprime_v39 s ww /\ c< norm(ww i- ww j)
 805 ==>
 806 BBprime_v39 (restriction_cs2_v39 s i j c) ww`,
 807 [
 808 STRIP_TAC
 809 THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION
 810 THEN RESA_TAC
 811 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
 812 THEN ASM_REWRITE_TAC[EXTENSION;UNION;IN_ELIM_THM]
 813 THEN REWRITE_TAC[IN]
 814 THEN STRIP_TAC
 815 THEN ASM_REWRITE_TAC[BBprime_v39]
 816 THEN REPEAT RESA_TAC;
 817
 818 POP_ASSUM MP_TAC
 819 THEN POP_ASSUM (fun th -> STRIP_TAC
 820 THEN MRESA1_TAC th`ww':num->real^3`)
 821 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
 822 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
 823 THEN ASM_TAC
 824 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
 825 THEN REPEAT RESA_TAC
 826 THEN REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
 827 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 828 THEN MRESA1_TAC th`ww':num->real^3`);
 829
 830 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
 831 THEN ASM_TAC
 832 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
 833 THEN REPEAT RESA_TAC]);;
 834
 835
 836
 837 let MIN_NUM_SUBSET=prove(
 838 `X SUBSET Y/\ a IN X==> min_num Y<= min_num X`,
 839 REWRITE_TAC[IN]
 840 THEN STRIP_TAC
 841 THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`X:num->bool`;`a:num`]
 842 THEN MP_TAC(SET_RULE`X (min_num X) /\ X SUBSET Y==> Y (min_num X)`)
 843 THEN RESA_TAC
 844 THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`Y:num->bool`;`min_num X`]);;
 845
 846
 847 let BBINDEX_MIN_S_LE_SUBDIVISION2=prove_by_refinement(`
 848     is_scs_v39 s /\    3< scs_k_v39 s /\
 849     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
 850     BBprime_v39 s ww /\ c< norm(ww i- ww j)
 851 ==>
 852 BBindex_min_v39 s <= min_num
 853  (IMAGE (BBindex_v39 s)
 854  (BBprime_v39 (restriction_cs2_v39 s i j c)))`,
 855 [
 856 STRIP_TAC
 857 THEN MP_TAC BBPRIME_SUBSET_BBPRIME_SUBDIVISION_UNION
 858 THEN RESA_TAC
 859 THEN REWRITE_TAC[BBindex_min_v39]
 860 THEN MATCH_MP_TAC(GEN_ALL  MIN_NUM_SUBSET)
 861 THEN EXISTS_TAC`BBindex_v39 s ww`
 862 THEN STRIP_TAC;
 863
 864 MATCH_MP_TAC IMAGE_SUBSET
 865 THEN MP_TAC BBPRIME_SUBDIVISION2_SUBSET_BBPRIME
 866 THEN RESA_TAC;
 867
 868 REWRITE_TAC[IMAGE;IN_ELIM_THM]
 869 THEN EXISTS_TAC`ww:num->real^3`
 870 THEN REWRITE_TAC[IN]
 871 THEN MP_TAC IN_BBPRIME_SUBDIVISION
 872 THEN RESA_TAC]);;
 873
 874
 875 let BBINDEX_BBPRIME_LE_SUBDIVISION2=prove_by_refinement(`
 876     is_scs_v39 s /\    3< scs_k_v39 s /\
 877     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
 878     BBprime_v39 s ww /\ c< norm(ww i- ww j)/\
 879    BBprime_v39 (restriction_cs2_v39 s i j c) vv
 880 ==>
 881  BBindex_v39 s vv<= BBindex_v39 (restriction_cs2_v39 s i j c) vv`,
 882 [
 883
 884 STRIP_TAC
 885 THEN REWRITE_TAC[BBindex_v39]
 886 THEN ASM_TAC
 887 THEN
 888 REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs2_v39;IN;BBs_v39]
 889 THEN ABBREV_TAC`k=scs_k_v39 s`
 890 THEN REPEAT STRIP_TAC
 891 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
 892 THEN RESA_TAC;
 893
 894
 895
 896 MATCH_MP_TAC CARD_SUBSET
 897 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
 898 THEN REPEAT RESA_TAC;
 899
 900
 901 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
 902 THEN RESA_TAC;
 903
 904
 905
 906 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
 907 THEN REPLICATE_TAC (41-33)(POP_ASSUM MP_TAC)
 908 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 909 THEN MRESA_TAC th[`x:num`;`SUC x`])
 910 THEN REMOVE_ASSUM_TAC
 911 THEN REPLICATE_TAC (41-37)(POP_ASSUM MP_TAC)
 912 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 913 THEN MP_TAC th)
 914 THEN REPLICATE_TAC (40-22)(POP_ASSUM MP_TAC)
 915 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 916 THEN MP_TAC th)
 917 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
 918 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
 919 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
 920 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
 921 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
 922 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
 923 THEN ASM_TAC
 924 THEN REWRITE_TAC[periodic2]
 925 THEN REPEAT DISCH_TAC
 926 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
 927 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
 928 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
 929 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
 930 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
 931 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 932 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
 933 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
 934 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
 935 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
 936 THEN REAL_ARITH_TAC;
 937
 938
 939
 940
 941 MATCH_MP_TAC FINITE_SUBSET
 942 THEN EXISTS_TAC`0..k`
 943 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
 944 THEN ARITH_TAC;
 945
 946
 947
 948
 949
 950
 951 MATCH_MP_TAC CARD_SUBSET
 952 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
 953 THEN REPEAT RESA_TAC;
 954
 955
 956 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
 957 THEN RESA_TAC;
 958
 959
 960
 961 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
 962 THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
 963 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 964 THEN MRESA_TAC th[`x:num`;`SUC x`])
 965 THEN REMOVE_ASSUM_TAC
 966 THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
 967 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 968 THEN MP_TAC th)
 969 THEN REPLICATE_TAC (41-22)(POP_ASSUM MP_TAC)
 970 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 971 THEN MP_TAC th)
 972 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
 973 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
 974 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
 975 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
 976 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
 977 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
 978 THEN ASM_TAC
 979 THEN REWRITE_TAC[periodic2]
 980 THEN REPEAT DISCH_TAC
 981 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
 982 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
 983 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
 984 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
 985 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
 986 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 987 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
 988 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
 989 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
 990 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
 991 THEN REAL_ARITH_TAC;
 992
 993
 994
 995
 996 MATCH_MP_TAC FINITE_SUBSET
 997 THEN EXISTS_TAC`0..k`
 998 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
 999 THEN ARITH_TAC;
1000
1001
1002
1003
1004
1005
1006
1007 MATCH_MP_TAC CARD_SUBSET
1008 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
1009 THEN REPEAT RESA_TAC;
1010
1011
1012 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
1013 THEN RESA_TAC;
1014
1015
1016
1017 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
1018 THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
1019 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1020 THEN MRESA_TAC th[`x:num`;`SUC x`])
1021 THEN REMOVE_ASSUM_TAC
1022 THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
1023 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1024 THEN MP_TAC th)
1025 THEN REPLICATE_TAC (41-22)(POP_ASSUM MP_TAC)
1026 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1027 THEN MP_TAC th)
1028 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
1029 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
1030 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1031 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1032 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
1033 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
1034 THEN ASM_TAC
1035 THEN REWRITE_TAC[periodic2]
1036 THEN REPEAT DISCH_TAC
1037 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
1038 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
1039 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
1040 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
1041 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
1042 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1043 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
1044 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
1045 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
1046 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
1047 THEN REAL_ARITH_TAC;
1048
1049
1050
1051
1052 MATCH_MP_TAC FINITE_SUBSET
1053 THEN EXISTS_TAC`0..k`
1054 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
1055 THEN ARITH_TAC;
1056
1057
1058
1059 MATCH_MP_TAC CARD_SUBSET
1060 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
1061 THEN REPEAT RESA_TAC;
1062
1063
1064 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
1065 THEN RESA_TAC;
1066
1067
1068
1069 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
1070 THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
1071 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1072 THEN MRESA_TAC th[`x:num`;`SUC x`])
1073 THEN REMOVE_ASSUM_TAC
1074 THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
1075 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1076 THEN MP_TAC th)
1077 THEN REPLICATE_TAC (41-22)(POP_ASSUM MP_TAC)
1078 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1079 THEN MP_TAC th)
1080 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
1081 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
1082 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1083 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1084 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
1085 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
1086 THEN ASM_TAC
1087 THEN REWRITE_TAC[periodic2]
1088 THEN REPEAT DISCH_TAC
1089 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
1090 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
1091 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
1092 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
1093 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
1094 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1095 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
1096 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
1097 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
1098 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
1099 THEN REAL_ARITH_TAC;
1100
1101
1102
1103
1104 MATCH_MP_TAC FINITE_SUBSET
1105 THEN EXISTS_TAC`0..k`
1106 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
1107 THEN ARITH_TAC;
1108
1109
1110
1111
1112 ]);;
1113
1114
1115 let MIN_NUM_LE_IMAGE=prove_by_refinement(`
1116 (a:A) IN s/\ (!x. x IN s==> f x <= g x) ==> min_num (IMAGE f s)<= min_num (IMAGE g s)`,
1117 [
1118 STRIP_TAC
1119 THEN SUBGOAL_THEN `g (a:A) IN ((IMAGE g s):num->bool)`ASSUME_TAC;
1120
1121 ASM_REWRITE_TAC[IN_ELIM_THM;IMAGE]
1122 THEN EXISTS_TAC`a:A`
1123 THEN RESA_TAC;
1124
1125 POP_ASSUM MP_TAC
1126 THEN REWRITE_TAC[IN]
1127 THEN STRIP_TAC
1128 THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`(IMAGE g (s:A->bool)):num->bool`;`(g (a:A)):num`]
1129 THEN SUBGOAL_THEN`(min_num (IMAGE g s)) IN IMAGE g (s:A->bool)`ASSUME_TAC;
1130
1131 ASM_REWRITE_TAC[IN];
1132
1133 POP_ASSUM MP_TAC
1134 THEN REWRITE_TAC[IN_ELIM_THM;IMAGE]
1135 THEN STRIP_TAC
1136 THEN REPLICATE_TAC (6-1)(POP_ASSUM MP_TAC)
1137 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1138 THEN MRESA1_TAC th`x:A`)
1139 THEN POP_ASSUM MP_TAC
1140 THEN SUBGOAL_THEN `f (x:A) IN ((IMAGE f s):num->bool)`ASSUME_TAC;
1141
1142 ASM_REWRITE_TAC[IN_ELIM_THM;IMAGE]
1143 THEN EXISTS_TAC`x:A`
1144 THEN RESA_TAC;
1145
1146 POP_ASSUM MP_TAC
1147 THEN REWRITE_TAC[IN]
1148 THEN STRIP_TAC
1149  THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`(IMAGE f (s:A->bool)):num->bool`;`(f:A->num) (x:A)`]
1150 THEN POP_ASSUM MP_TAC
1151 THEN REWRITE_TAC[IMAGE;IN]
1152 THEN ARITH_TAC]);;
1153
1154
1155 let CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION2=prove(`
1156     is_scs_v39 s /\    3< scs_k_v39 s /\
1157     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1158     BBprime_v39 s ww /\ c< norm(ww i- ww j)
1159 ==>
1160 min_num
1161  (IMAGE (BBindex_v39 s)
1162  (BBprime_v39 (restriction_cs2_v39 s i j c)))
1163 <= min_num
1164  (IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c))
1165  (BBprime_v39 (restriction_cs2_v39 s i j c)))`,
1166 STRIP_TAC
1167 THEN MATCH_MP_TAC (GEN_ALL MIN_NUM_LE_IMAGE)
1168 THEN EXISTS_TAC`ww:num->real^3`
1169 THEN MP_TAC IN_BBPRIME_SUBDIVISION
1170 THEN ASM_REWRITE_TAC[IN]
1171 THEN RESA_TAC
1172 THEN REPEAT STRIP_TAC
1173 THEN MATCH_MP_TAC BBINDEX_BBPRIME_LE_SUBDIVISION2
1174 THEN ASM_REWRITE_TAC[]);;
1175
1176
1177 let BBindex_min_LE_SUBDIVISION2=prove(`
1178     is_scs_v39 s /\    3< scs_k_v39 s /\
1179     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1180     BBprime_v39 s ww /\ c< norm(ww i- ww j)
1181 ==>
1182 BBindex_min_v39 s <= BBindex_min_v39 (restriction_cs2_v39 s i j c)`,
1183 STRIP_TAC
1184 THEN MP_TAC CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION2
1185 THEN RESA_TAC
1186 THEN MP_TAC BBINDEX_MIN_S_LE_SUBDIVISION2
1187 THEN RESA_TAC
1188 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
1189 THEN REWRITE_TAC[BBindex_min_v39]
1190 THEN ARITH_TAC);;
1191
1192
1193 let BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION=prove_by_refinement(`
1194     is_scs_v39 s /\    3< scs_k_v39 s /\
1195     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1196     MMs_v39 s ww /\ c< norm(ww i- ww j)
1197 ==>
1198  ww IN BBprime2_v39 (restriction_cs2_v39 s i j c)`,
1199 [
1200 STRIP_TAC
1201 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
1202 THEN RESA_TAC
1203 THEN ASM_TAC
1204 THEN
1205 REWRITE_TAC[MMs_v39;BBprime2_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
1206 THEN ABBREV_TAC`k=scs_k_v39 s`
1207 THEN REPEAT STRIP_TAC
1208 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
1209 THEN RESA_TAC;
1210
1211 REWRITE_TAC[IN]
1212 THEN ASM_REWRITE_TAC[BBprime2_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;]
1213 THEN MP_TAC IN_BBPRIME_SUBDIVISION
1214 THEN RESA_TAC
1215 THEN SUBGOAL_THEN`BBs_v39 s ww` ASSUME_TAC;
1216
1217 ASM_TAC
1218 THEN REWRITE_TAC[BBprime_v39;LET_DEF;LET_END_DEF]
1219 THEN REPEAT RESA_TAC;
1220
1221 MP_TAC BBINDEX_EQ_SUBDIVISION
1222 THEN RESA_TAC
1223 THEN MP_TAC BBindex_min_LE_SUBDIVISION2
1224 THEN RESA_TAC
1225 THEN POP_ASSUM MP_TAC
1226 THEN REWRITE_TAC[BBindex_min_v39]
1227 THEN SUBGOAL_THEN`(BBindex_v39 (restriction_cs2_v39 s i j c) ww)
1228 IN IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c))
1229       (BBprime_v39 (restriction_cs2_v39 s i j c))`ASSUME_TAC;
1230
1231 REWRITE_TAC[IN_ELIM_THM;IMAGE]
1232 THEN EXISTS_TAC`ww:num->real^3`
1233 THEN ASM_REWRITE_TAC[IN];
1234
1235 POP_ASSUM MP_TAC
1236 THEN REWRITE_TAC[IN]
1237 THEN STRIP_TAC
1238 THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c)) (BBprime_v39 (restriction_cs2_v39 s i j c))`;`BBindex_v39 (restriction_cs2_v39 s i j c) ww`]
1239 THEN POP_ASSUM MP_TAC
1240 THEN ARITH_TAC]);;
1241
1242
1243
1244 let MM_IS_NOT_2EMPTY_SUBDIVISION=prove_by_refinement(`
1245    is_scs_v39 s /\    3< scs_k_v39 s /\
1246     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1247 scs_am_v39 s i j < c/\
1248     MMs_v39 s ww /\ c< norm(ww i- ww j)
1249 ==>
1250  ww IN MMs_v39 (restriction_cs2_v39 s i j c)`,
1251 [
1252 STRIP_TAC
1253 THEN MP_TAC BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION
1254 THEN RESA_TAC
1255 THEN ASM_TAC
1256 THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39]
1257 THEN REPEAT RESA_TAC
1258 THEN REWRITE_TAC[override]
1259 THEN ABBREV_TAC`k=scs_k_v39 s`
1260 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
1261 THEN RESA_TAC
1262 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'))`)
1263 THEN RESA_TAC;
1264
1265
1266 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];
1267
1268
1269 ASM_TAC
1270 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
1271 THEN REPEAT STRIP_TAC;
1272
1273
1274 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1275 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1276 THEN MP_TAC th)
1277 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1278 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1279 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1280 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1281 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
1282 THEN REAL_ARITH_TAC;
1283
1284
1285 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1286 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1287 THEN MP_TAC th)
1288 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1289 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1290 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1291 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1292 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
1293 THEN REAL_ARITH_TAC;
1294
1295 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1296 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1297 THEN MP_TAC th)
1298 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1299 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1300 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1301 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1302 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
1303 THEN REAL_ARITH_TAC;
1304
1305
1306 REPLICATE_TAC (27-17)(POP_ASSUM MP_TAC)
1307 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1308 THEN MP_TAC th)
1309 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1310 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1311 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1312 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1313 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
1314 THEN REAL_ARITH_TAC;
1315
1316 ASM_TAC
1317 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
1318 THEN REPEAT STRIP_TAC;
1319
1320 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1321 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1322 THEN MP_TAC th)
1323 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1324 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1325 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1326 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1327 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1328 THEN ONCE_REWRITE_TAC[DIST_SYM]
1329 THEN REWRITE_TAC[dist]
1330 THEN REAL_ARITH_TAC;
1331
1332 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1333 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1334 THEN MP_TAC th)
1335 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1336 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1337 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1338 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1339 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1340 THEN ONCE_REWRITE_TAC[DIST_SYM]
1341 THEN REWRITE_TAC[dist]
1342 THEN REAL_ARITH_TAC;
1343
1344 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1345 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1346 THEN MP_TAC th)
1347 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1348 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1349 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1350 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1351 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1352 THEN ONCE_REWRITE_TAC[DIST_SYM]
1353 THEN REWRITE_TAC[dist]
1354 THEN REAL_ARITH_TAC;
1355
1356 REPLICATE_TAC (27-17)(POP_ASSUM MP_TAC)
1357 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1358 THEN MP_TAC th)
1359 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1360 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1361 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1362 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1363 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1364 THEN ONCE_REWRITE_TAC[DIST_SYM]
1365 THEN REWRITE_TAC[dist]
1366 THEN REAL_ARITH_TAC]);;
1367
1368
1369
1370 let MM_IS_NOT_1EMPTY_SUBDIVISION=prove_by_refinement(
1371 `
1372    is_scs_v39 s /\    3< scs_k_v39 s /\
1373     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1374 c<= scs_am_v39 s i j /\
1375     MMs_v39 s ww /\ c< norm(ww i- ww j)
1376 ==>
1377  ww IN MMs_v39 (restriction_cs2_v39 s i j c)`,
1378 [STRIP_TAC
1379 THEN MP_TAC BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION
1380 THEN RESA_TAC
1381 THEN ASM_TAC
1382 THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39]
1383 THEN REPEAT RESA_TAC
1384 THEN REWRITE_TAC[override]
1385 THEN ABBREV_TAC`k=scs_k_v39 s`
1386 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
1387 THEN RESA_TAC
1388 THEN MP_TAC(REAL_ARITH`c<= scs_am_v39 s i j==> ~(scs_am_v39 s i j<c)`)
1389 THEN RESA_TAC]);;
1390
1391
1392
1393 (********************************)
1394
1395
1396
1397 let BBINDEX_EQ_SUBDIVISION1=prove_by_refinement(
1398 `
1399     is_scs_v39 s /\    3< scs_k_v39 s /\
1400     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1401     BBs_v39 s ww /\ dist(ww i,ww j) <= c
1402 ==>
1403 BBindex_v39 s ww = BBindex_v39 (restriction_cs1_v39 s i j c) ww`,
1404 [STRIP_TAC
1405 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
1406 THEN RESA_TAC
1407 THEN ASM_TAC
1408 THEN REWRITE_TAC[BBindex_v39]
1409 THEN
1410 REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs1_v39]
1411 THEN ABBREV_TAC`k=scs_k_v39 s`
1412 THEN REPEAT STRIP_TAC
1413 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
1414 THEN RESA_TAC]);;
1415
1416
1417 let CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION1= prove_by_refinement(
1418 `
1419     is_scs_v39 s /\    3< scs_k_v39 s /\
1420     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1421 BBprime_v39 s ww /\ dist(ww i,ww j) <= c
1422 ==>
1423 BBs_v39 (restriction_cs1_v39 s i j c) ww`,
1424 [
1425 REWRITE_TAC[MMs_v39;BBs_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;restriction_cs1_v39]
1426 THEN ABBREV_TAC`k=scs_k_v39 s`
1427 THEN RESA_TAC
1428 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
1429 THEN REPEAT RESA_TAC;
1430
1431 POP_ASSUM MP_TAC
1432 THEN POP_ASSUM(fun th-> STRIP_TAC
1433 THEN MP_TAC th)
1434 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'))`)
1435 THEN RESA_TAC;
1436
1437 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];
1438
1439 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1440 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1441 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1442 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1443 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
1444 THEN REAL_ARITH_TAC;
1445
1446 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1447 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1448 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1449 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1450 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1451 THEN STRIP_TAC
1452 THEN ONCE_REWRITE_TAC[DIST_SYM]
1453 THEN RESA_TAC;
1454
1455 POP_ASSUM MP_TAC
1456 THEN POP_ASSUM(fun th-> STRIP_TAC
1457 THEN MP_TAC th)
1458 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'))`)
1459 THEN RESA_TAC;
1460
1461 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];
1462
1463 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1464 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1465 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1466 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1467 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
1468 THEN REAL_ARITH_TAC;
1469
1470 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1471 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1472 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1473 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1474 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1475 THEN STRIP_TAC
1476 THEN ONCE_REWRITE_TAC[DIST_SYM]
1477 THEN RESA_TAC]);;
1478
1479
1480
1481
1482 let IN_BBPRIME_SUBDIVISION1=prove_by_refinement(
1483 `
1484     is_scs_v39 s /\    3< scs_k_v39 s /\
1485     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1486 BBprime_v39 s ww /\ dist(ww i,ww j) <= c
1487 ==>
1488 BBprime_v39 (restriction_cs1_v39 s i j c) ww`,
1489 [
1490 STRIP_TAC
1491 THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION1
1492 THEN RESA_TAC
1493 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
1494 THEN ASM_REWRITE_TAC[EXTENSION;UNION;IN_ELIM_THM]
1495 THEN REWRITE_TAC[IN]
1496 THEN STRIP_TAC
1497 THEN ASM_REWRITE_TAC[BBprime_v39]
1498 THEN REPEAT RESA_TAC;
1499
1500 POP_ASSUM MP_TAC
1501 THEN POP_ASSUM (fun th -> STRIP_TAC
1502 THEN MRESA1_TAC th`ww':num->real^3`)
1503 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
1504 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
1505 THEN ASM_TAC
1506 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
1507 THEN REPEAT RESA_TAC
1508 THEN REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
1509 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1510 THEN MRESA1_TAC th`ww':num->real^3`);
1511
1512 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
1513 THEN ASM_TAC
1514 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
1515 THEN REPEAT RESA_TAC]);;
1516
1517
1518
1519
1520
1521 let BBPRIME_SUBDIVISION2_SUBSET_BBPRIME1=prove_by_refinement(
1522 `
1523     is_scs_v39 s /\    3< scs_k_v39 s /\
1524     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1525 BBprime_v39 s ww /\ dist(ww i,ww j) <= c
1526 ==>
1527 (BBprime_v39 (restriction_cs1_v39 s i j c)) SUBSET (BBprime_v39 s)  `,
1528 [
1529 STRIP_TAC
1530 THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION1
1531 THEN RESA_TAC
1532 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
1533 THEN ASM_REWRITE_TAC[EXTENSION;IN]
1534 THEN ASM_TAC
1535 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
1536 THEN ABBREV_TAC`k=scs_k_v39 s`
1537 THEN REPEAT RESA_TAC;
1538
1539
1540 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
1541 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
1542 THEN REPLICATE_TAC (36-30)(POP_ASSUM MP_TAC)
1543 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1544 THEN MRESA1_TAC th`ww':num->real^3`);
1545
1546
1547 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
1548 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
1549 THEN REPLICATE_TAC (37-29)(POP_ASSUM MP_TAC)
1550 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1551 THEN MRESA1_TAC th`ww':num->real^3`)
1552 THEN REPLICATE_TAC (37-25)(POP_ASSUM MP_TAC)
1553 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1554 THEN MRESA1_TAC th`ww':num->real^3`)
1555 THEN REPLICATE_TAC (37-29)(POP_ASSUM MP_TAC)
1556 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1557 THEN MRESA1_TAC th`ww:num->real^3`)
1558 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
1559 THEN REAL_ARITH_TAC;
1560
1561 POP_ASSUM MP_TAC
1562 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]]);;
1563
1564
1565
1566
1567
1568 let BBINDEX_MIN_S_LE_SUBDIVISION1=prove_by_refinement(
1569 `
1570     is_scs_v39 s /\    3< scs_k_v39 s /\
1571     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1572     BBprime_v39 s ww /\ dist(ww i,ww j) <= c
1573 ==>
1574 BBindex_min_v39 s <= min_num
1575  (IMAGE (BBindex_v39 s)
1576  (BBprime_v39 (restriction_cs1_v39 s i j c)))`,
1577 [
1578 STRIP_TAC
1579 THEN MP_TAC BBPRIME_SUBSET_BBPRIME_SUBDIVISION_UNION
1580 THEN RESA_TAC
1581 THEN REWRITE_TAC[BBindex_min_v39]
1582 THEN MATCH_MP_TAC(GEN_ALL  MIN_NUM_SUBSET)
1583 THEN EXISTS_TAC`BBindex_v39 s ww`
1584 THEN STRIP_TAC;
1585
1586 MATCH_MP_TAC IMAGE_SUBSET
1587 THEN MP_TAC BBPRIME_SUBDIVISION2_SUBSET_BBPRIME1
1588 THEN RESA_TAC;
1589
1590 REWRITE_TAC[IMAGE;IN_ELIM_THM]
1591 THEN EXISTS_TAC`ww:num->real^3`
1592 THEN REWRITE_TAC[IN]
1593 THEN MP_TAC IN_BBPRIME_SUBDIVISION1
1594 THEN RESA_TAC;]);;
1595
1596
1597
1598
1599
1600
1601 let BBINDEX_BBPRIME_LE_SUBDIVISION1=prove_by_refinement(
1602 `
1603     is_scs_v39 s /\    3< scs_k_v39 s /\
1604     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1605     BBprime_v39 s ww /\ dist(ww i,ww j) <= c/\
1606    BBprime_v39 (restriction_cs1_v39 s i j c) vv
1607 ==>
1608  BBindex_v39 s vv= BBindex_v39 (restriction_cs1_v39 s i j c) vv`,
1609 [STRIP_TAC
1610 THEN REWRITE_TAC[BBindex_v39]
1611 THEN ASM_TAC
1612 THEN
1613 REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs1_v39;IN;BBs_v39]
1614 THEN ABBREV_TAC`k=scs_k_v39 s`
1615 THEN REPEAT STRIP_TAC
1616 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
1617 THEN RESA_TAC]);;
1618
1619
1620
1621
1622 let CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION1=prove(`
1623     is_scs_v39 s /\    3< scs_k_v39 s /\
1624     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1625     BBprime_v39 s ww /\ dist(ww i,ww j) <= c
1626 ==>
1627 min_num
1628  (IMAGE (BBindex_v39 s)
1629  (BBprime_v39 (restriction_cs1_v39 s i j c)))
1630 <= min_num
1631  (IMAGE (BBindex_v39 (restriction_cs1_v39 s i j c))
1632  (BBprime_v39 (restriction_cs1_v39 s i j c)))`,
1633 STRIP_TAC
1634 THEN MATCH_MP_TAC (GEN_ALL MIN_NUM_LE_IMAGE)
1635 THEN EXISTS_TAC`ww:num->real^3`
1636 THEN MP_TAC IN_BBPRIME_SUBDIVISION1
1637 THEN ASM_REWRITE_TAC[IN]
1638 THEN RESA_TAC
1639 THEN REPEAT STRIP_TAC
1640 THEN MRESA_TAC(GEN_ALL BBINDEX_BBPRIME_LE_SUBDIVISION1)[`ww:num->real^3`;`s:scs_v39`;`i:num`;`j:num`;`c:real`;`x:num->real^3`]
1641 THEN ARITH_TAC);;
1642
1643
1644
1645 let BBindex_min_LE_SUBDIVISION1=prove(`
1646     is_scs_v39 s /\    3< scs_k_v39 s /\
1647     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1648     BBprime_v39 s ww /\ dist(ww i,ww j) <= c
1649 ==>
1650 BBindex_min_v39 s <= BBindex_min_v39 (restriction_cs1_v39 s i j c)`,
1651 STRIP_TAC
1652 THEN MP_TAC CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION1
1653 THEN RESA_TAC
1654 THEN MP_TAC BBINDEX_MIN_S_LE_SUBDIVISION1
1655 THEN RESA_TAC
1656 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
1657 THEN REWRITE_TAC[BBindex_min_v39]
1658 THEN ARITH_TAC);;
1659
1660
1661
1662 let BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION1=prove_by_refinement(
1663 `
1664     is_scs_v39 s /\    3< scs_k_v39 s /\
1665     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1666     MMs_v39 s ww /\ dist(ww i,ww j) <= c
1667 ==>
1668  ww IN BBprime2_v39 (restriction_cs1_v39 s i j c)`,
1669 [
1670 STRIP_TAC
1671 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
1672 THEN RESA_TAC
1673 THEN ASM_TAC
1674 THEN
1675 REWRITE_TAC[MMs_v39;BBprime2_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
1676 THEN ABBREV_TAC`k=scs_k_v39 s`
1677 THEN REPEAT STRIP_TAC
1678 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
1679 THEN RESA_TAC;
1680
1681 REWRITE_TAC[IN]
1682 THEN ASM_REWRITE_TAC[BBprime2_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;]
1683 THEN MP_TAC IN_BBPRIME_SUBDIVISION1
1684 THEN RESA_TAC
1685 THEN SUBGOAL_THEN`BBs_v39 s ww` ASSUME_TAC;
1686
1687 ASM_TAC
1688 THEN REWRITE_TAC[BBprime_v39;LET_DEF;LET_END_DEF]
1689 THEN REPEAT RESA_TAC;
1690
1691 MP_TAC BBINDEX_EQ_SUBDIVISION1
1692 THEN RESA_TAC
1693 THEN MP_TAC BBindex_min_LE_SUBDIVISION1
1694 THEN RESA_TAC
1695 THEN POP_ASSUM MP_TAC
1696 THEN REWRITE_TAC[BBindex_min_v39]
1697 THEN SUBGOAL_THEN`(BBindex_v39 (restriction_cs1_v39 s i j c) ww)
1698 IN IMAGE (BBindex_v39 (restriction_cs1_v39 s i j c))
1699       (BBprime_v39 (restriction_cs1_v39 s i j c))`ASSUME_TAC;
1700
1701 REWRITE_TAC[IN_ELIM_THM;IMAGE]
1702 THEN EXISTS_TAC`ww:num->real^3`
1703 THEN ASM_REWRITE_TAC[IN];
1704
1705 POP_ASSUM MP_TAC
1706 THEN REWRITE_TAC[IN]
1707 THEN STRIP_TAC
1708 THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`IMAGE (BBindex_v39 (restriction_cs1_v39 s i j c)) (BBprime_v39 (restriction_cs1_v39 s i j c))`;`BBindex_v39 (restriction_cs1_v39 s i j c) ww`]
1709 THEN POP_ASSUM MP_TAC
1710 THEN ARITH_TAC]);;
1711
1712
1713
1714
1715 let MM_IS_NOT_2EMPTY_SUBDIVISION1=prove_by_refinement(
1716 `
1717    is_scs_v39 s /\    3< scs_k_v39 s /\
1718     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1719 c < scs_bm_v39 s i j/\
1720     MMs_v39 s ww /\ dist(ww i,ww j) <= c
1721 ==>
1722  ww IN MMs_v39 (restriction_cs1_v39 s i j c)`,
1723 [STRIP_TAC
1724 THEN MP_TAC BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION1
1725 THEN RESA_TAC
1726 THEN ASM_TAC
1727 THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs1_v39]
1728 THEN REPEAT RESA_TAC
1729 THEN REWRITE_TAC[override]
1730 THEN ABBREV_TAC`k=scs_k_v39 s`
1731 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
1732 THEN RESA_TAC
1733 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'))`)
1734 THEN RESA_TAC;
1735
1736
1737
1738 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];
1739
1740
1741 ASM_TAC
1742 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
1743 THEN REPEAT STRIP_TAC;
1744
1745
1746 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1747 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1748 THEN MP_TAC th)
1749 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1750 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1751 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1752 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1753 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1754 THEN REAL_ARITH_TAC;
1755
1756
1757
1758 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1759 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1760 THEN MP_TAC th)
1761 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1762 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1763 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1764 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1765 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1766 THEN REAL_ARITH_TAC;
1767
1768 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1769 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1770 THEN MP_TAC th)
1771 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1772 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1773 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1774 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1775 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
1776 THEN REAL_ARITH_TAC;
1777
1778
1779 REPLICATE_TAC (27-17)(POP_ASSUM MP_TAC)
1780 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1781 THEN MP_TAC th)
1782 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1783 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1784 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1785 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1786 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
1787 THEN REAL_ARITH_TAC;
1788
1789 ASM_TAC
1790 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
1791 THEN REPEAT STRIP_TAC;
1792
1793 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1794 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1795 THEN MP_TAC th)
1796 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1797 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1798 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1799 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1800 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1801 THEN STRIP_TAC
1802 THEN ONCE_REWRITE_TAC[DIST_SYM]
1803 THEN RESA_TAC;
1804
1805 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1806 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1807 THEN MP_TAC th)
1808 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1809 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1810 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1811 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1812 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1813 THEN STRIP_TAC
1814 THEN ONCE_REWRITE_TAC[DIST_SYM]
1815 THEN RESA_TAC;
1816
1817 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1818 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1819 THEN MP_TAC th)
1820 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1821 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1822 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1823 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1824 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1825 THEN STRIP_TAC
1826 THEN ONCE_REWRITE_TAC[DIST_SYM]
1827 THEN RESA_TAC;
1828
1829 REPLICATE_TAC (27-17)(POP_ASSUM MP_TAC)
1830 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1831 THEN MP_TAC th)
1832 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1833 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1834 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1835 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1836 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1837 THEN STRIP_TAC
1838 THEN ONCE_REWRITE_TAC[DIST_SYM]
1839 THEN RESA_TAC;
1840 ]);;
1841
1842
1843 let MM_IS_NOT_1EMPTY_SUBDIVISION1=prove_by_refinement(
1844 `
1845    is_scs_v39 s /\    3< scs_k_v39 s /\
1846     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1847  scs_bm_v39 s i j <=c /\
1848     MMs_v39 s ww /\ dist(ww i,ww j) <= c
1849 ==>
1850  ww IN MMs_v39 (restriction_cs1_v39 s i j c)`,
1851 [STRIP_TAC
1852 THEN MP_TAC BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION1
1853 THEN RESA_TAC
1854 THEN ASM_TAC
1855 THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs1_v39]
1856 THEN REPEAT RESA_TAC
1857 THEN REWRITE_TAC[override]
1858 THEN ABBREV_TAC`k=scs_k_v39 s`
1859 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
1860 THEN RESA_TAC
1861 THEN MP_TAC(REAL_ARITH`scs_bm_v39 s i j <= c==> ~(c< scs_bm_v39 s i j)`)
1862 THEN RESA_TAC]);;
1863
1864
1865
1866
1867 let BBINDEX_EQ_SUBDIVISION_C_EQ_AM=prove_by_refinement(
1868 `
1869     is_scs_v39 s /\    3< scs_k_v39 s /\
1870     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1871 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j))) /\
1872     BBs_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c
1873 ==>
1874 BBindex_v39 s ww = BBindex_v39 (restriction_cs2_v39 s i j c) ww`,
1875 [
1876 STRIP_TAC
1877 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
1878 THEN RESA_TAC
1879 THEN ASM_TAC
1880 THEN REWRITE_TAC[BBindex_v39]
1881 THEN
1882 REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs2_v39]
1883 THEN ABBREV_TAC`k=scs_k_v39 s`
1884 THEN REPEAT STRIP_TAC
1885 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
1886 THEN RESA_TAC;
1887
1888 MATCH_MP_TAC CARD_IMAGE_INJ_EQ
1889 THEN REWRITE_TAC[IN_ELIM_THM]
1890 THEN EXISTS_TAC`(\i:num. i)`
1891 THEN STRIP_TAC;
1892
1893 MATCH_MP_TAC FINITE_SUBSET
1894 THEN EXISTS_TAC`0..k`
1895 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
1896 THEN ARITH_TAC;
1897
1898 STRIP_TAC;
1899
1900 REPEAT RESA_TAC
1901 THEN POP_ASSUM MP_TAC
1902 THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
1903 THEN RESA_TAC;
1904
1905 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`];
1906
1907 ASM_TAC
1908 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
1909 THEN REPEAT STRIP_TAC
1910 THEN REPLICATE_TAC (37-24)(POP_ASSUM MP_TAC)
1911 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1912 THEN MP_TAC th)
1913 THEN POP_ASSUM MP_TAC
1914 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1915 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1916 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1917 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
1918 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;dist])
1919 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x:num`;`i:num`;`k:num`][];
1920
1921 ASM_TAC
1922 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
1923 THEN REPEAT STRIP_TAC
1924 THEN REPLICATE_TAC (37-24)(POP_ASSUM MP_TAC)
1925 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1926 THEN MP_TAC th)
1927 THEN POP_ASSUM MP_TAC
1928 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1929 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1930 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1931 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
1932 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;dist])
1933 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x:num`;`j:num`;`k:num`][];
1934
1935 REPEAT RESA_TAC;
1936
1937 REWRITE_TAC[EXISTS_UNIQUE]
1938 THEN EXISTS_TAC`y:num`
1939 THEN ASM_REWRITE_TAC[]
1940 THEN REPEAT RESA_TAC
1941 THEN POP_ASSUM MP_TAC
1942 THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (y,SUC y) \/ ~(psort k (i,j) = psort k (y,SUC y))`)
1943 THEN RESA_TAC;
1944
1945 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC y:num`;`j:num`;`y:num`;`k:num`];
1946
1947 ASM_TAC
1948 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
1949 THEN REPEAT STRIP_TAC
1950 THEN REPLICATE_TAC (37-24)(POP_ASSUM MP_TAC)
1951 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1952 THEN MP_TAC th)
1953 THEN POP_ASSUM MP_TAC
1954 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1955 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1956 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1957 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
1958 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;dist])
1959 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`y:num`;`i:num`;`k:num`][];
1960
1961 ASM_TAC
1962 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
1963 THEN REPEAT STRIP_TAC
1964 THEN REPLICATE_TAC (37-24)(POP_ASSUM MP_TAC)
1965 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1966 THEN MP_TAC th)
1967 THEN POP_ASSUM MP_TAC
1968 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1969 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1970 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1971 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
1972 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;dist])
1973 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`y:num`;`j:num`;`k:num`][]]);;
1974
1975
1976
1977 let CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION_C_EQ_AM= prove_by_refinement(`
1978     is_scs_v39 s /\    3< scs_k_v39 s /\
1979     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1980 BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
1981 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
1982 ==>
1983 BBs_v39 (restriction_cs2_v39 s i j c) ww`,
1984 [
1985 REWRITE_TAC[MMs_v39;BBs_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;restriction_cs2_v39]
1986 THEN ABBREV_TAC`k=scs_k_v39 s`
1987 THEN RESA_TAC
1988 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
1989 THEN REPEAT RESA_TAC;
1990
1991 REPLICATE_TAC (33-30)(POP_ASSUM MP_TAC)
1992 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1993 THEN MP_TAC th)
1994 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'))`)
1995 THEN RESA_TAC;
1996
1997 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];
1998
1999 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
2000 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
2001 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
2002 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
2003 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
2004 THEN REAL_ARITH_TAC;
2005
2006 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
2007 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
2008 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
2009 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
2010 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
2011 THEN STRIP_TAC
2012 THEN ONCE_REWRITE_TAC[DIST_SYM]
2013 THEN POP_ASSUM MP_TAC
2014 THEN REAL_ARITH_TAC;
2015
2016 REPLICATE_TAC (33-30)(POP_ASSUM MP_TAC)
2017 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2018 THEN MP_TAC th)
2019 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'))`)
2020 THEN RESA_TAC;
2021
2022 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];
2023
2024 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
2025 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
2026 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
2027 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
2028 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
2029 THEN REAL_ARITH_TAC;
2030
2031 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
2032 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
2033 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
2034 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
2035 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
2036 THEN STRIP_TAC
2037 THEN ONCE_REWRITE_TAC[DIST_SYM]
2038 THEN POP_ASSUM MP_TAC
2039 THEN REAL_ARITH_TAC]);;
2040
2041
2042
2043
2044 let BBPRIME_SUBDIVISION2_SUBSET_BBPRIME_C_EQ_AM=prove_by_refinement(`
2045     is_scs_v39 s /\    3< scs_k_v39 s /\
2046     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
2047 BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
2048 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
2049 ==>
2050 (BBprime_v39 (restriction_cs2_v39 s i j c)) SUBSET (BBprime_v39 s)  `,
2051 [
2052 STRIP_TAC
2053 THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION_C_EQ_AM
2054 THEN RESA_TAC
2055 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
2056 THEN ASM_REWRITE_TAC[EXTENSION;IN]
2057 THEN ASM_TAC
2058 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
2059 THEN ABBREV_TAC`k=scs_k_v39 s`
2060 THEN REPEAT RESA_TAC;
2061
2062 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
2063 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
2064 THEN REPLICATE_TAC (39-33)(POP_ASSUM MP_TAC)
2065 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2066 THEN MRESA1_TAC th`ww:num->real^3`)
2067 THEN REPLICATE_TAC (39-31)(POP_ASSUM MP_TAC)
2068 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2069 THEN MRESA1_TAC th`ww':num->real^3`)
2070 THEN REPLICATE_TAC (39-25)(POP_ASSUM MP_TAC)
2071 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2072 THEN MRESA1_TAC th`ww':num->real^3`)
2073 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
2074 THEN REAL_ARITH_TAC;
2075
2076 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
2077 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
2078 THEN REPLICATE_TAC (39-33)(POP_ASSUM MP_TAC)
2079 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2080 THEN MRESA1_TAC th`ww:num->real^3`)
2081 THEN REPLICATE_TAC (39-31)(POP_ASSUM MP_TAC)
2082 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2083 THEN MRESA1_TAC th`ww':num->real^3`)
2084 THEN REPLICATE_TAC (39-25)(POP_ASSUM MP_TAC)
2085 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2086 THEN MRESA1_TAC th`ww':num->real^3`)
2087 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
2088 THEN REAL_ARITH_TAC;
2089
2090 POP_ASSUM MP_TAC
2091 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]]);;
2092
2093
2094
2095
2096 let IN_BBPRIME_SUBDIVISION_C_EQ_AM=prove_by_refinement(
2097 `
2098     is_scs_v39 s /\    3< scs_k_v39 s /\
2099     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
2100 BBprime_v39 s ww  /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
2101 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
2102 ==>
2103 BBprime_v39 (restriction_cs2_v39 s i j c) ww`,
2104 [
2105 STRIP_TAC
2106 THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION_C_EQ_AM
2107 THEN RESA_TAC
2108 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
2109 THEN ASM_REWRITE_TAC[EXTENSION;UNION;IN_ELIM_THM]
2110 THEN REWRITE_TAC[IN]
2111 THEN STRIP_TAC
2112 THEN ASM_REWRITE_TAC[BBprime_v39]
2113 THEN REPEAT RESA_TAC;
2114
2115 POP_ASSUM MP_TAC
2116 THEN POP_ASSUM (fun th -> STRIP_TAC
2117 THEN MRESA1_TAC th`ww':num->real^3`)
2118 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
2119 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
2120 THEN ASM_TAC
2121 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
2122 THEN REPEAT RESA_TAC
2123 THEN REPLICATE_TAC (35-24)(POP_ASSUM MP_TAC)
2124 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2125 THEN MRESA1_TAC th`ww':num->real^3`);
2126
2127 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
2128 THEN ASM_TAC
2129 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
2130 THEN REPEAT RESA_TAC]);;
2131
2132
2133
2134
2135 let BBINDEX_MIN_S_LE_SUBDIVISION2_C_EQ_AM=prove_by_refinement(`
2136     is_scs_v39 s /\    3< scs_k_v39 s /\
2137     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
2138     BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
2139 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
2140 ==>
2141 BBindex_min_v39 s <= min_num
2142  (IMAGE (BBindex_v39 s)
2143  (BBprime_v39 (restriction_cs2_v39 s i j c)))`,
2144 [
2145 STRIP_TAC
2146 THEN MP_TAC BBPRIME_SUBSET_BBPRIME_SUBDIVISION_UNION
2147 THEN RESA_TAC
2148 THEN REWRITE_TAC[BBindex_min_v39]
2149 THEN MATCH_MP_TAC(GEN_ALL  MIN_NUM_SUBSET)
2150 THEN EXISTS_TAC`BBindex_v39 s ww`
2151 THEN STRIP_TAC;
2152
2153 MATCH_MP_TAC IMAGE_SUBSET
2154 THEN MP_TAC BBPRIME_SUBDIVISION2_SUBSET_BBPRIME_C_EQ_AM
2155 THEN RESA_TAC;
2156
2157 REWRITE_TAC[IMAGE;IN_ELIM_THM]
2158 THEN EXISTS_TAC`ww:num->real^3`
2159 THEN REWRITE_TAC[IN]
2160 THEN MP_TAC IN_BBPRIME_SUBDIVISION_C_EQ_AM
2161 THEN RESA_TAC]);;
2162
2163
2164
2165
2166
2167 let BBINDEX_BBPRIME_LE_SUBDIVISION2_C_EQ_AM=prove_by_refinement(
2168 `
2169     is_scs_v39 s /\    3< scs_k_v39 s /\
2170     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
2171     BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
2172 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j))) /\
2173    BBprime_v39 (restriction_cs2_v39 s i j c) vv
2174 ==>
2175  BBindex_v39 s vv<= BBindex_v39 (restriction_cs2_v39 s i j c) vv`,
2176 [
2177
2178 STRIP_TAC
2179 THEN REWRITE_TAC[BBindex_v39]
2180 THEN ASM_TAC
2181 THEN
2182 REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs2_v39;IN;BBs_v39]
2183 THEN ABBREV_TAC`k=scs_k_v39 s`
2184 THEN REPEAT STRIP_TAC
2185 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
2186 THEN RESA_TAC;
2187
2188
2189
2190
2191 MATCH_MP_TAC CARD_SUBSET
2192 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
2193 THEN REPEAT RESA_TAC;
2194
2195
2196
2197 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
2198 THEN RESA_TAC;
2199
2200
2201
2202
2203 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
2204 THEN REPLICATE_TAC (41-33)(POP_ASSUM MP_TAC)
2205 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2206 THEN MRESA_TAC th[`x:num`;`SUC x`])
2207 THEN REMOVE_ASSUM_TAC
2208 THEN REPLICATE_TAC (41-37)(POP_ASSUM MP_TAC)
2209 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2210 THEN MP_TAC th)
2211 THEN REPLICATE_TAC (42-22)(POP_ASSUM MP_TAC)
2212 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2213 THEN MP_TAC th)
2214 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
2215 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
2216 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
2217 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
2218 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
2219 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
2220 THEN ASM_TAC
2221 THEN REWRITE_TAC[periodic2]
2222 THEN REPEAT DISCH_TAC
2223 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
2224 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2225 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2226 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2227 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2228 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2229 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
2230 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
2231 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2232 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
2233 THEN REAL_ARITH_TAC;
2234
2235
2236
2237
2238
2239 MATCH_MP_TAC FINITE_SUBSET
2240 THEN EXISTS_TAC`0..k`
2241 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
2242 THEN ARITH_TAC;
2243
2244
2245
2246
2247
2248
2249
2250 MATCH_MP_TAC CARD_SUBSET
2251 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
2252 THEN REPEAT RESA_TAC;
2253
2254
2255
2256 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
2257 THEN RESA_TAC;
2258
2259
2260
2261
2262 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
2263 THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
2264 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2265 THEN MRESA_TAC th[`x:num`;`SUC x`])
2266 THEN REMOVE_ASSUM_TAC
2267 THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
2268 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2269 THEN MP_TAC th)
2270 THEN REPLICATE_TAC (43-22)(POP_ASSUM MP_TAC)
2271 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2272 THEN MP_TAC th)
2273 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
2274 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
2275 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
2276 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
2277 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
2278 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
2279 THEN ASM_TAC
2280 THEN REWRITE_TAC[periodic2]
2281 THEN REPEAT DISCH_TAC
2282 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
2283 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2284 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2285 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2286 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2287 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2288 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
2289 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
2290 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2291 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
2292 THEN REAL_ARITH_TAC;
2293
2294
2295
2296
2297
2298 MATCH_MP_TAC FINITE_SUBSET
2299 THEN EXISTS_TAC`0..k`
2300 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
2301 THEN ARITH_TAC;
2302
2303
2304
2305
2306
2307
2308
2309
2310 MATCH_MP_TAC CARD_SUBSET
2311 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
2312 THEN REPEAT RESA_TAC;
2313
2314
2315
2316 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
2317 THEN RESA_TAC;
2318
2319
2320
2321
2322 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
2323 THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
2324 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2325 THEN MRESA_TAC th[`x:num`;`SUC x`])
2326 THEN REMOVE_ASSUM_TAC
2327 THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
2328 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2329 THEN MP_TAC th)
2330 THEN REPLICATE_TAC (43-22)(POP_ASSUM MP_TAC)
2331 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2332 THEN MP_TAC th)
2333 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
2334 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
2335 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
2336 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
2337 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
2338 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
2339 THEN ASM_TAC
2340 THEN REWRITE_TAC[periodic2]
2341 THEN REPEAT DISCH_TAC
2342 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
2343 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2344 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2345 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2346 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2347 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2348 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
2349 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
2350 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2351 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
2352 THEN REAL_ARITH_TAC;
2353
2354
2355
2356
2357
2358 MATCH_MP_TAC FINITE_SUBSET
2359 THEN EXISTS_TAC`0..k`
2360 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
2361 THEN ARITH_TAC;
2362
2363
2364
2365
2366 MATCH_MP_TAC CARD_SUBSET
2367 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
2368 THEN REPEAT RESA_TAC;
2369
2370
2371
2372 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
2373 THEN RESA_TAC;
2374
2375
2376
2377
2378 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
2379 THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
2380 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2381 THEN MRESA_TAC th[`x:num`;`SUC x`])
2382 THEN REMOVE_ASSUM_TAC
2383 THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
2384 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2385 THEN MP_TAC th)
2386 THEN REPLICATE_TAC (43-22)(POP_ASSUM MP_TAC)
2387 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2388 THEN MP_TAC th)
2389 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
2390 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
2391 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
2392 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
2393 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
2394 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
2395 THEN ASM_TAC
2396 THEN REWRITE_TAC[periodic2]
2397 THEN REPEAT DISCH_TAC
2398 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
2399 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2400 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2401 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2402 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2403 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2404 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
2405 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
2406 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2407 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
2408 THEN REAL_ARITH_TAC;
2409
2410
2411
2412
2413
2414 MATCH_MP_TAC FINITE_SUBSET
2415 THEN EXISTS_TAC`0..k`
2416 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
2417 THEN ARITH_TAC;
2418 ]);;
2419
2420
2421
2422
2423
2424
2425 let CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION2_C_EQ_AM=prove(
2426 `
2427     is_scs_v39 s /\    3< scs_k_v39 s /\
2428     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
2429     BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
2430 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
2431 ==>
2432 min_num
2433  (IMAGE (BBindex_v39 s)
2434  (BBprime_v39 (restriction_cs2_v39 s i j c)))
2435 <= min_num
2436  (IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c))
2437  (BBprime_v39 (restriction_cs2_v39 s i j c)))`,
2438 STRIP_TAC
2439 THEN MATCH_MP_TAC (GEN_ALL MIN_NUM_LE_IMAGE)
2440 THEN EXISTS_TAC`ww:num->real^3`
2441 THEN MP_TAC IN_BBPRIME_SUBDIVISION_C_EQ_AM
2442 THEN ASM_REWRITE_TAC[IN]
2443 THEN RESA_TAC
2444 THEN REPEAT STRIP_TAC
2445 THEN MATCH_MP_TAC BBINDEX_BBPRIME_LE_SUBDIVISION2_C_EQ_AM
2446 THEN ASM_REWRITE_TAC[]);;
2447
2448
2449
2450 let BBindex_min_LE_SUBDIVISION2_C_EQ_AM=prove(`
2451     is_scs_v39 s /\    3< scs_k_v39 s /\
2452     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
2453     BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
2454 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
2455 ==>
2456 BBindex_min_v39 s <= BBindex_min_v39 (restriction_cs2_v39 s i j c)`,
2457 STRIP_TAC
2458 THEN MP_TAC CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION2_C_EQ_AM
2459 THEN RESA_TAC
2460 THEN MP_TAC BBINDEX_MIN_S_LE_SUBDIVISION2_C_EQ_AM
2461 THEN RESA_TAC
2462 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
2463 THEN REWRITE_TAC[BBindex_min_v39]
2464 THEN ARITH_TAC);;
2465
2466
2467
2468
2469 let BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION_C_EQ_AM=prove_by_refinement(`
2470     is_scs_v39 s /\    3< scs_k_v39 s /\
2471     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
2472     MMs_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
2473 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
2474 ==>
2475  ww IN BBprime2_v39 (restriction_cs2_v39 s i j c)`,
2476 [
2477 STRIP_TAC
2478 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
2479 THEN RESA_TAC
2480 THEN ASM_TAC
2481 THEN
2482 REWRITE_TAC[MMs_v39;BBprime2_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
2483 THEN ABBREV_TAC`k=scs_k_v39 s`
2484 THEN REPEAT STRIP_TAC
2485 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
2486 THEN ASM_TAC
2487 THEN REPEAT RESA_TAC;
2488
2489 REWRITE_TAC[IN]
2490 THEN ASM_REWRITE_TAC[BBprime2_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;]
2491 THEN MP_TAC IN_BBPRIME_SUBDIVISION_C_EQ_AM
2492 THEN RESA_TAC
2493 THEN SUBGOAL_THEN`BBs_v39 s ww` ASSUME_TAC;
2494
2495 ASM_TAC
2496 THEN REWRITE_TAC[BBprime_v39;LET_DEF;LET_END_DEF]
2497 THEN REPEAT RESA_TAC;
2498
2499 MP_TAC BBINDEX_EQ_SUBDIVISION_C_EQ_AM
2500 THEN RESA_TAC
2501 THEN MP_TAC BBindex_min_LE_SUBDIVISION2_C_EQ_AM
2502 THEN RESA_TAC
2503 THEN POP_ASSUM MP_TAC
2504 THEN REWRITE_TAC[BBindex_min_v39]
2505 THEN SUBGOAL_THEN`(BBindex_v39 (restriction_cs2_v39 s i j c) ww)
2506 IN IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c))
2507       (BBprime_v39 (restriction_cs2_v39 s i j c))`ASSUME_TAC;
2508
2509 REWRITE_TAC[IN_ELIM_THM;IMAGE]
2510 THEN EXISTS_TAC`ww:num->real^3`
2511 THEN ASM_REWRITE_TAC[IN];
2512
2513 POP_ASSUM MP_TAC
2514 THEN REWRITE_TAC[IN]
2515 THEN STRIP_TAC
2516 THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c)) (BBprime_v39 (restriction_cs2_v39 s i j c))`;`BBindex_v39 (restriction_cs2_v39 s i j c) ww`]
2517 THEN POP_ASSUM MP_TAC
2518 THEN ARITH_TAC]);;
2519
2520
2521
2522
2523 let MM_IS_NOT_2EMPTY_SUBDIVISION_C_EQ_AM=prove_by_refinement(
2524 `
2525    is_scs_v39 s /\    3< scs_k_v39 s /\
2526     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
2527     MMs_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
2528 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
2529 ==>
2530  ww IN MMs_v39 (restriction_cs2_v39 s i j c)`,
2531 [
2532 STRIP_TAC
2533 THEN MP_TAC BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION_C_EQ_AM
2534 THEN RESA_TAC
2535 THEN ASM_TAC
2536 THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39]
2537 THEN REPEAT RESA_TAC
2538 THEN REWRITE_TAC[override;REAL_ARITH`~(c<c)`]
2539 THEN ABBREV_TAC`k=scs_k_v39 s`
2540 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
2541 THEN RESA_TAC
2542 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'))`)
2543 THEN RESA_TAC]);;
2544
2545
2546
2547
2548 let UAGHHBM=prove_by_refinement(
2549 `!s i j c .
2550     is_scs_v39 s /\ ~(i MOD scs_k_v39 s=j MOD scs_k_v39 s)/\
2551     ~(scs_J_v39 s i j) /\
2552     scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j/\
2553 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (&2 < scs_a_v39 s i j \/ &2 * h0 < scs_b_v39 s i j))
2554 /\ 3< scs_k_v39 s  /\
2555 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
2556 ==>
2557     scs_arrow_v39 {s} (set_of_list (subdiv_v39 s i j c))`,
2558 [
2559 REPEAT GEN_TAC
2560 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;subdiv_v39;PAIR_EQ;LET_DEF;LET_END_DEF;]
2561 THEN ABBREV_TAC`k=scs_k_v39 s`
2562 THEN REPEAT RESA_TAC
2563 ;
2564
2565
2566
2567 POP_ASSUM MP_TAC
2568 THEN REMOVE_ASSUM_TAC
2569 THEN REMOVE_ASSUM_TAC
2570 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;]
2571 THEN MP_TAC(SET_RULE`c <= scs_a_v39 s i j \/ ~(c <= scs_a_v39 s i j)`)
2572 THEN RESA_TAC;
2573
2574
2575 ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1]
2576 THEN RESA_TAC;
2577
2578
2579
2580 MP_TAC(SET_RULE`c <= scs_am_v39 s i j \/ ~(c <= scs_am_v39 s i j)`)
2581 THEN RESA_TAC;
2582
2583
2584 ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;restriction_cs2_v39;LET_DEF;LET_END_DEF;]
2585 THEN RESA_TAC
2586 THEN ASM_TAC
2587 THEN REWRITE_TAC[is_scs_v39;scs_v39_explicit;override]
2588 THEN RESA_TAC
2589 THEN RESA_TAC
2590 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
2591 THEN RESA_TAC
2592 THEN REPEAT RESA_TAC;
2593
2594
2595
2596
2597 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
2598 THEN REPEAT GEN_TAC
2599 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
2600 THEN RESA_TAC;
2601
2602
2603 MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
2604 ;
2605
2606
2607 POP_ASSUM MP_TAC
2608 THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
2609 THEN RESA_TAC
2610 THEN ASM_TAC
2611 THEN REWRITE_TAC[periodic2]
2612 THEN REPEAT DISCH_TAC
2613 THEN ASM_REWRITE_TAC[];
2614
2615
2616
2617 MP_TAC(REAL_ARITH`c <= scs_am_v39 s i j==> ~(scs_am_v39 s i j < c)`)
2618 THEN RESA_TAC
2619 ;
2620
2621
2622 MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
2623 ;
2624
2625
2626
2627 MP_TAC(REAL_ARITH`c <= scs_am_v39 s i j==> ~(scs_am_v39 s i j < c)`)
2628 THEN RESA_TAC
2629 ;
2630
2631
2632 MP_TAC(REAL_ARITH`c <= scs_am_v39 s i j==> ~(scs_am_v39 s i j < c)`)
2633 THEN RESA_TAC
2634 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'))`)
2635 THEN RESA_TAC
2636 ;
2637
2638
2639 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
2640 THEN ASM_TAC
2641 THEN REWRITE_TAC[periodic2]
2642 THEN REPEAT STRIP_TAC
2643 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2644 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2645 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2646 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2647 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
2648 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
2649 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2650 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
2651 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);
2652
2653
2654
2655
2656 MP_TAC(REAL_ARITH`c <= scs_am_v39 s i j==> ~(scs_am_v39 s i j < c)`)
2657 THEN RESA_TAC
2658 ;
2659
2660
2661
2662 MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',i'))`)
2663 THEN RESA_TAC;
2664
2665
2666 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`i':num`;`j:num`;`i':num`;`k:num`]
2667 THEN POP_ASSUM(fun th-> MP_TAC (SYM th))
2668 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);
2669
2670
2671
2672 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'))`)
2673 THEN RESA_TAC;
2674
2675
2676 MP_TAC C_LE_2_IS_SCS
2677 THEN REWRITE_TAC[is_scs_v39]
2678 THEN ASM_TAC
2679 THEN REPEAT RESA_TAC
2680 ;
2681
2682
2683
2684
2685 REPLICATE_TAC (33-15)(POP_ASSUM MP_TAC)
2686 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2687 THEN MRESA_TAC th[`i':num`;`j':num`])
2688 ;
2689
2690
2691 POP_ASSUM MP_TAC
2692 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'))`)
2693 THEN RESA_TAC;
2694
2695
2696
2697 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
2698 THEN ASM_TAC
2699 THEN REWRITE_TAC[periodic2]
2700 THEN REPEAT STRIP_TAC
2701 THEN POP_ASSUM MP_TAC
2702 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2703 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2704 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2705 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2706 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
2707 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
2708 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2709 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
2710 ;
2711
2712
2713
2714 STRIP_TAC
2715 THEN REPLICATE_TAC (31-19)(POP_ASSUM MP_TAC)
2716 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2717 THEN MRESA_TAC th[`i':num`;`j':num`])
2718 ;
2719
2720
2721
2722 REPLICATE_TAC (30-19)(POP_ASSUM MP_TAC)
2723 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2724 THEN MRESA_TAC th[`i':num`;`j':num`])
2725 ;
2726
2727
2728
2729
2730 SUBGOAL_THEN`CARD
2731  {i' | i' < k /\
2732        (&2 * h0 < scs_b_v39 s i' (SUC i') \/
2733         &2 <
2734         (if psort k (i,j) = psort k (i',SUC i')
2735          then c
2736          else scs_a_v39 s i' (SUC i')))}
2737 = CARD
2738       {i | i < k /\
2739            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
2740 ASSUME_TAC;
2741
2742
2743
2744 MATCH_MP_TAC CARD_IMAGE_INJ_EQ
2745 THEN REWRITE_TAC[IN_ELIM_THM]
2746 THEN EXISTS_TAC`(\i:num. i)`
2747 THEN STRIP_TAC;
2748
2749
2750
2751 MATCH_MP_TAC FINITE_SUBSET
2752 THEN EXISTS_TAC`0..k`
2753 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
2754 THEN ARITH_TAC;
2755
2756
2757 STRIP_TAC;
2758
2759
2760 REPEAT RESA_TAC
2761 ;
2762
2763
2764 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
2765 THEN RESA_TAC
2766 ;
2767
2768
2769
2770 MP_TAC(REAL_ARITH`~(c <= scs_a_v39 s i j)==> scs_a_v39 s i j < c`)
2771 THEN RESA_TAC
2772 THEN MP_TAC C_LT_2_IS_SCS
2773 THEN REWRITE_TAC[is_scs_v39]
2774 THEN ASM_TAC
2775 THEN REPEAT RESA_TAC
2776 ;
2777
2778
2779
2780
2781 REPEAT RESA_TAC
2782 ;
2783
2784
2785 REWRITE_TAC[EXISTS_UNIQUE]
2786 THEN EXISTS_TAC`y:num`
2787 THEN ASM_REWRITE_TAC[]
2788 THEN REPEAT RESA_TAC
2789 ;
2790
2791
2792
2793 REWRITE_TAC[EXISTS_UNIQUE]
2794 THEN EXISTS_TAC`y:num`
2795 THEN ASM_REWRITE_TAC[]
2796 THEN POP_ASSUM MP_TAC
2797 THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (y,SUC y) \/ ~(psort k (i,j) = psort k (y,SUC y))`)
2798 THEN RESA_TAC
2799 ;
2800
2801
2802
2803
2804
2805 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC y:num`;`j:num`;`y:num`;`k:num`]
2806 ;
2807
2808
2809 POP_ASSUM MP_TAC
2810 THEN MRESA_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`y:num`;`i:num`;`k:num`]
2811 THEN STRIP_TAC
2812 THEN REPLICATE_TAC (34-26)(POP_ASSUM MP_TAC)
2813 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2814 THEN MP_TAC th
2815 THEN RESA_TAC)
2816 ;
2817
2818
2819
2820 ASM_TAC
2821 THEN REWRITE_TAC[periodic2]
2822 THEN REPEAT DISCH_TAC
2823 THEN POP_ASSUM MP_TAC
2824 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2825 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2826 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2827 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2828 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2829 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
2830 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
2831 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2832 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
2833 THEN REPEAT RESA_TAC
2834 ;
2835
2836
2837
2838
2839
2840 ASM_TAC
2841 THEN REWRITE_TAC[periodic2]
2842 THEN REPEAT DISCH_TAC
2843 THEN POP_ASSUM MP_TAC
2844 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2845 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2846 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2847 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2848 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2849 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
2850 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
2851 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2852 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
2853 THEN REPEAT RESA_TAC
2854 ;
2855
2856
2857
2858
2859 POP_ASSUM MP_TAC
2860 THEN POP_ASSUM(fun th-> STRIP_TAC
2861 THEN MP_TAC th)
2862 THEN MRESA_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`y:num`;`j:num`;`k:num`]
2863 THEN STRIP_TAC
2864 THEN REPLICATE_TAC (34-26)(POP_ASSUM MP_TAC)
2865 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2866 THEN MP_TAC th
2867 THEN RESA_TAC)
2868 ;
2869
2870
2871
2872 ASM_TAC
2873 THEN REWRITE_TAC[periodic2]
2874 THEN REPEAT DISCH_TAC
2875 THEN POP_ASSUM MP_TAC
2876 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2877 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2878 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2879 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2880 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2881 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
2882 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
2883 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2884 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
2885 THEN REPEAT RESA_TAC
2886 ;
2887
2888
2889
2890
2891
2892 ASM_TAC
2893 THEN REWRITE_TAC[periodic2]
2894 THEN REPEAT DISCH_TAC
2895 THEN POP_ASSUM MP_TAC
2896 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2897 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2898 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2899 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2900 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2901 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
2902 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
2903 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2904 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
2905 THEN REPEAT RESA_TAC
2906 ;
2907
2908
2909 REPEAT RESA_TAC
2910 ;
2911
2912
2913
2914 ASM_REWRITE_TAC[]
2915 ;
2916
2917
2918
2919 (**********c < scs_bm_v39 s i j *******)
2920
2921 MP_TAC(SET_RULE`c < scs_bm_v39 s i j \/ ~(c < scs_bm_v39 s i j)`)
2922 THEN RESA_TAC;
2923
2924
2925
2926 ASM_REWRITE_TAC[Basics.set_of_list2_explicit;SET_RULE`A IN{B,C}<=> A=B \/ A=C`]
2927 THEN RESA_TAC;
2928
2929
2930 (**********restriction_cs1_v39 s i j c *******)
2931
2932
2933
2934 ASM_TAC
2935 THEN REWRITE_TAC[is_scs_v39;scs_v39_explicit;override;restriction_cs1_v39;LET_DEF;LET_END_DEF;]
2936 THEN RESA_TAC
2937 THEN RESA_TAC
2938 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
2939 THEN RESA_TAC
2940 THEN REPEAT RESA_TAC;
2941
2942
2943
2944 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
2945 THEN REPEAT GEN_TAC
2946 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
2947 THEN RESA_TAC;
2948
2949
2950 MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
2951 ;
2952
2953
2954 POP_ASSUM MP_TAC
2955 THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
2956 THEN RESA_TAC
2957 THEN ASM_TAC
2958 THEN REWRITE_TAC[periodic2]
2959 THEN REPEAT DISCH_TAC
2960 THEN ASM_REWRITE_TAC[];
2961
2962
2963
2964
2965
2966 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
2967 THEN REPEAT GEN_TAC
2968 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
2969 THEN RESA_TAC;
2970
2971
2972 MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
2973 ;
2974
2975
2976 POP_ASSUM MP_TAC
2977 THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
2978 THEN RESA_TAC
2979 THEN ASM_TAC
2980 THEN REWRITE_TAC[periodic2]
2981 THEN REPEAT DISCH_TAC
2982 THEN ASM_REWRITE_TAC[];
2983
2984
2985
2986
2987 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
2988 THEN MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
2989 ;
2990
2991
2992
2993 MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
2994 ;
2995
2996
2997
2998 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
2999 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'))`)
3000 THEN RESA_TAC;
3001
3002
3003 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
3004 THEN MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j) ==>  scs_am_v39 s i j<= c`)
3005 THEN RESA_TAC
3006 ;
3007
3008
3009 ASM_TAC
3010 THEN REWRITE_TAC[periodic2]
3011 THEN REPEAT DISCH_TAC
3012 THEN POP_ASSUM MP_TAC
3013 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3014 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3015 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3016 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3017 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3018 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3019 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
3020 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3021 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3022 ;
3023
3024
3025
3026
3027 ASM_TAC
3028 THEN REWRITE_TAC[periodic2]
3029 THEN REPEAT DISCH_TAC
3030 THEN POP_ASSUM MP_TAC
3031 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3032 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3033 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3034 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3035 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3036 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3037 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
3038 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3039 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3040 ;
3041
3042
3043
3044 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
3045 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'))`)
3046 THEN RESA_TAC;
3047
3048
3049 REAL_ARITH_TAC
3050 ;
3051
3052
3053
3054 POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
3055 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i'))`)
3056 THEN RESA_TAC;
3057
3058
3059
3060
3061 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC i':num`;`j:num`;`i':num`;`k:num`]
3062 THEN REPLICATE_TAC (34-16)(POP_ASSUM MP_TAC)
3063 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3064 THEN MRESA1_TAC th`i':num`)
3065 THEN ASM_TAC
3066 THEN REWRITE_TAC[periodic2]
3067 THEN REPEAT DISCH_TAC
3068 THEN POP_ASSUM MP_TAC
3069 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3070 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC i':num`[ARITH_RULE`4 MOD 4=0`])
3071 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3072 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3073 THEN REPLICATE_TAC (35-24)(POP_ASSUM MP_TAC)
3074 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3075 THEN MP_TAC th)
3076 THEN POP_ASSUM MP_TAC
3077 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3078 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3079 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3080 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3081 THEN REAL_ARITH_TAC;
3082
3083
3084
3085
3086 REPLICATE_TAC (32-16)(POP_ASSUM MP_TAC)
3087 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3088 THEN MRESA1_TAC th`i':num`)
3089 ;
3090
3091
3092
3093
3094 MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i'))`)
3095 THEN RESA_TAC;
3096
3097
3098
3099
3100 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC i':num`;`j:num`;`i':num`;`k:num`]
3101 THEN REPLICATE_TAC (34-17)(POP_ASSUM MP_TAC)
3102 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3103 THEN MRESA1_TAC th`i':num`)
3104 THEN ASM_TAC
3105 THEN REWRITE_TAC[periodic2]
3106 THEN REPEAT DISCH_TAC
3107 THEN POP_ASSUM MP_TAC
3108 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3109 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC i':num`[ARITH_RULE`4 MOD 4=0`])
3110 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3111 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3112 THEN REPLICATE_TAC (35-24)(POP_ASSUM MP_TAC)
3113 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3114 THEN MP_TAC th)
3115 THEN POP_ASSUM MP_TAC
3116 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3117 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3118 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3119 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3120 THEN REAL_ARITH_TAC;
3121
3122
3123 REPLICATE_TAC (32-17)(POP_ASSUM MP_TAC)
3124 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3125 THEN MRESA1_TAC th`i':num`)
3126 ;
3127
3128
3129
3130
3131 REPLICATE_TAC (31-19)(POP_ASSUM MP_TAC)
3132 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3133 THEN MRESA_TAC th[`i':num`;`j':num`])
3134 ;
3135
3136
3137 POP_ASSUM MP_TAC
3138 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'))`)
3139 THEN RESA_TAC
3140 ;
3141
3142
3143
3144 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
3145 THEN ASM_TAC
3146 THEN REWRITE_TAC[periodic2]
3147 THEN REPEAT DISCH_TAC
3148 THEN POP_ASSUM MP_TAC
3149 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3150 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3151 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3152 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3153 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3154 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
3155 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3156 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3157 ;
3158
3159
3160
3161
3162 REPLICATE_TAC (31-19)(POP_ASSUM MP_TAC)
3163 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3164 THEN MRESA_TAC th[`i':num`;`j':num`])
3165 ;
3166
3167
3168
3169
3170 SUBGOAL_THEN`CARD
3171  {i' | i' < k /\
3172        (&2 * h0 <
3173         (if psort k (i,j) = psort k (i',SUC i')
3174          then c
3175          else scs_b_v39 s i' (SUC i')) \/
3176         &2 < scs_a_v39 s i' (SUC i'))}
3177 <= CARD
3178  {i' | i' < k /\
3179        (&2 * h0 <
3180         (scs_b_v39 s i' (SUC i')) \/
3181         &2 < scs_a_v39 s i' (SUC i'))}`ASSUME_TAC
3182 ;
3183
3184
3185
3186
3187
3188 MATCH_MP_TAC CARD_SUBSET
3189 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
3190 THEN STRIP_TAC;
3191
3192
3193
3194 REPEAT RESA_TAC
3195 ;
3196
3197
3198 POP_ASSUM MP_TAC
3199 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (x,SUC x) \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (x,SUC x))`)
3200 THEN RESA_TAC
3201 ;
3202
3203
3204
3205 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
3206 THEN REPLICATE_TAC (34-25)(POP_ASSUM MP_TAC)
3207 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3208 THEN MP_TAC th)
3209 THEN ASM_TAC
3210 THEN REWRITE_TAC[periodic2]
3211 THEN REPEAT DISCH_TAC
3212 THEN POP_ASSUM MP_TAC
3213 THEN POP_ASSUM MP_TAC
3214 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3215 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3216 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3217 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3218 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
3219 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
3220 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3221 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`])
3222 THEN REAL_ARITH_TAC;
3223
3224
3225 RESA_TAC;
3226
3227
3228
3229 MATCH_MP_TAC FINITE_SUBSET
3230 THEN EXISTS_TAC`0..k`
3231 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
3232 THEN ARITH_TAC;
3233
3234
3235
3236 REPLICATE_TAC (31-20)(POP_ASSUM MP_TAC)
3237 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3238 THEN MP_TAC th)
3239 THEN POP_ASSUM MP_TAC
3240 THEN ARITH_TAC
3241 ;
3242
3243
3244
3245 (**********restriction_cs2_v39 s i j c *******)
3246
3247
3248 ASM_TAC
3249 THEN REWRITE_TAC[is_scs_v39;scs_v39_explicit;override;restriction_cs2_v39;LET_DEF;LET_END_DEF;]
3250 THEN RESA_TAC
3251 THEN RESA_TAC
3252 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
3253 THEN RESA_TAC
3254 THEN REPEAT RESA_TAC;
3255
3256
3257
3258
3259 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
3260 THEN REPEAT GEN_TAC
3261 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
3262 THEN RESA_TAC;
3263
3264
3265 MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
3266 ;
3267
3268
3269 POP_ASSUM MP_TAC
3270 THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
3271 THEN RESA_TAC
3272 THEN ASM_TAC
3273 THEN REWRITE_TAC[periodic2]
3274 THEN REPEAT DISCH_TAC
3275 THEN ASM_REWRITE_TAC[];
3276
3277
3278
3279
3280
3281
3282 MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j)==> (scs_am_v39 s i j < c)`)
3283 THEN RESA_TAC
3284 ;
3285
3286
3287
3288
3289
3290 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
3291 THEN REPEAT GEN_TAC
3292 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
3293 THEN RESA_TAC;
3294
3295
3296 MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
3297 ;
3298
3299
3300 POP_ASSUM MP_TAC
3301 THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
3302 THEN RESA_TAC
3303 THEN ASM_TAC
3304 THEN REWRITE_TAC[periodic2]
3305 THEN REPEAT DISCH_TAC
3306 THEN ASM_REWRITE_TAC[];
3307
3308
3309
3310
3311 MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
3312 ;
3313
3314
3315
3316 MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j)==> (scs_am_v39 s i j < c)`)
3317 THEN RESA_TAC
3318 ;
3319
3320
3321
3322 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
3323 THEN MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
3324 ;
3325
3326
3327
3328 MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j)==> (scs_am_v39 s i j < c)`)
3329 THEN RESA_TAC
3330 THEN REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
3331 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'))`)
3332 THEN RESA_TAC
3333 ;
3334
3335
3336 REAL_ARITH_TAC;
3337
3338
3339
3340 MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j)==> (scs_am_v39 s i j < c)`)
3341 THEN RESA_TAC
3342 THEN REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
3343 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'))`)
3344 THEN RESA_TAC;
3345
3346
3347
3348
3349
3350 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
3351 THEN ASM_TAC
3352 THEN REWRITE_TAC[periodic2]
3353 THEN REPEAT STRIP_TAC
3354 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3355 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3356 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3357 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3358 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3359 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
3360 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3361 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3362 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
3363 THEN MP_TAC(REAL_ARITH`c < scs_bm_v39 s i j ==> c <= scs_bm_v39 s i j`)
3364 THEN RESA_TAC;
3365
3366
3367
3368
3369
3370 MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',i'))`)
3371 THEN RESA_TAC;
3372
3373
3374 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`i':num`;`j:num`;`i':num`;`k:num`]
3375 THEN POP_ASSUM(fun th-> MP_TAC (SYM th))
3376 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);
3377
3378
3379
3380 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'))`)
3381 THEN RESA_TAC;
3382
3383
3384 MP_TAC C_LE_2_IS_SCS
3385 THEN REWRITE_TAC[is_scs_v39]
3386 THEN ASM_TAC
3387 THEN REPEAT RESA_TAC
3388 ;
3389
3390
3391
3392
3393 REPLICATE_TAC (34-15)(POP_ASSUM MP_TAC)
3394 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
3395 THEN MRESA_TAC th[`i':num`;`j':num`])
3396 ;
3397
3398
3399 POP_ASSUM MP_TAC
3400 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'))`)
3401 THEN RESA_TAC;
3402
3403
3404
3405 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
3406 THEN ASM_TAC
3407 THEN REWRITE_TAC[periodic2]
3408 THEN REPEAT STRIP_TAC
3409 THEN POP_ASSUM MP_TAC
3410 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3411 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3412 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3413 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3414 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3415 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
3416 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3417 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3418 ;
3419
3420
3421
3422 STRIP_TAC
3423 THEN REPLICATE_TAC (32-19)(POP_ASSUM MP_TAC)
3424 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
3425 THEN MRESA_TAC th[`i':num`;`j':num`])
3426 ;
3427
3428
3429
3430 REPLICATE_TAC (31-19)(POP_ASSUM MP_TAC)
3431 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
3432 THEN MRESA_TAC th[`i':num`;`j':num`])
3433 ;
3434
3435
3436
3437
3438 SUBGOAL_THEN`CARD
3439  {i' | i' < k /\
3440        (&2 * h0 < scs_b_v39 s i' (SUC i') \/
3441         &2 <
3442         (if psort k (i,j) = psort k (i',SUC i')
3443          then c
3444          else scs_a_v39 s i' (SUC i')))}
3445 = CARD
3446       {i | i < k /\
3447            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
3448 ASSUME_TAC;
3449
3450
3451
3452 MATCH_MP_TAC CARD_IMAGE_INJ_EQ
3453 THEN REWRITE_TAC[IN_ELIM_THM]
3454 THEN EXISTS_TAC`(\i:num. i)`
3455 THEN STRIP_TAC;
3456
3457
3458
3459 MATCH_MP_TAC FINITE_SUBSET
3460 THEN EXISTS_TAC`0..k`
3461 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
3462 THEN ARITH_TAC;
3463
3464
3465 STRIP_TAC;
3466
3467
3468 REPEAT RESA_TAC
3469 ;
3470
3471
3472 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
3473 THEN RESA_TAC
3474 ;
3475
3476
3477
3478 MP_TAC(REAL_ARITH`~(c <= scs_a_v39 s i j)==> scs_a_v39 s i j < c`)
3479 THEN RESA_TAC
3480 THEN MP_TAC C_LT_2_IS_SCS
3481 THEN REWRITE_TAC[is_scs_v39]
3482 THEN ASM_TAC
3483 THEN REPEAT RESA_TAC
3484 ;
3485
3486
3487
3488
3489 REPEAT RESA_TAC
3490 ;
3491
3492
3493 REWRITE_TAC[EXISTS_UNIQUE]
3494 THEN EXISTS_TAC`y:num`
3495 THEN ASM_REWRITE_TAC[]
3496 THEN REPEAT RESA_TAC
3497 ;
3498
3499
3500
3501 REWRITE_TAC[EXISTS_UNIQUE]
3502 THEN EXISTS_TAC`y:num`
3503 THEN ASM_REWRITE_TAC[]
3504 THEN POP_ASSUM MP_TAC
3505 THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (y,SUC y) \/ ~(psort k (i,j) = psort k (y,SUC y))`)
3506 THEN RESA_TAC
3507 ;
3508
3509
3510
3511
3512
3513 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC y:num`;`j:num`;`y:num`;`k:num`]
3514 ;
3515
3516
3517 POP_ASSUM MP_TAC
3518 THEN MRESA_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`y:num`;`i:num`;`k:num`]
3519 THEN STRIP_TAC
3520 THEN REPLICATE_TAC (35-26)(POP_ASSUM MP_TAC)
3521 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3522 THEN MP_TAC th
3523 THEN RESA_TAC)
3524 ;
3525
3526
3527
3528 ASM_TAC
3529 THEN REWRITE_TAC[periodic2]
3530 THEN REPEAT DISCH_TAC
3531 THEN POP_ASSUM MP_TAC
3532 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3533 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3534 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3535 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3536 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3537 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
3538 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
3539 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3540 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
3541 THEN REPEAT RESA_TAC
3542 ;
3543
3544
3545
3546
3547
3548 ASM_TAC
3549 THEN REWRITE_TAC[periodic2]
3550 THEN REPEAT DISCH_TAC
3551 THEN POP_ASSUM MP_TAC
3552 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3553 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3554 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3555 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3556 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3557 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
3558 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
3559 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3560 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
3561 THEN REPEAT RESA_TAC
3562 ;
3563
3564
3565
3566
3567 POP_ASSUM MP_TAC
3568 THEN POP_ASSUM(fun th-> STRIP_TAC
3569 THEN MP_TAC th)
3570 THEN MRESA_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`y:num`;`j:num`;`k:num`]
3571 THEN STRIP_TAC
3572 THEN REPLICATE_TAC (35-26)(POP_ASSUM MP_TAC)
3573 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3574 THEN MP_TAC th
3575 THEN RESA_TAC)
3576 ;
3577
3578
3579
3580 ASM_TAC
3581 THEN REWRITE_TAC[periodic2]
3582 THEN REPEAT DISCH_TAC
3583 THEN POP_ASSUM MP_TAC
3584 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3585 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3586 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3587 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3588 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3589 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
3590 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
3591 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3592 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
3593 THEN REPEAT RESA_TAC
3594 ;
3595
3596
3597
3598
3599
3600 ASM_TAC
3601 THEN REWRITE_TAC[periodic2]
3602 THEN REPEAT DISCH_TAC
3603 THEN POP_ASSUM MP_TAC
3604 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3605 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3606 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3607 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3608 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3609 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
3610 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
3611 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3612 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
3613 THEN REPEAT RESA_TAC
3614 ;
3615
3616
3617 REPEAT RESA_TAC
3618 ;
3619
3620
3621
3622 ASM_REWRITE_TAC[]
3623 ;
3624
3625
3626
3627 (**********restriction_cs1_v39 s i j c *******)
3628
3629 MP_TAC(SET_RULE`c < scs_b_v39 s i j \/ ~(c < scs_b_v39 s i j)`)
3630 THEN RESA_TAC;
3631
3632
3633
3634 ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;restriction_cs1_v39;LET_DEF;LET_END_DEF;]
3635 THEN RESA_TAC
3636 THEN ASM_TAC
3637 THEN REWRITE_TAC[is_scs_v39;scs_v39_explicit;override]
3638 THEN RESA_TAC
3639 THEN RESA_TAC
3640 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
3641 THEN RESA_TAC
3642 THEN REPEAT RESA_TAC;
3643
3644
3645
3646 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
3647 THEN REPEAT GEN_TAC
3648 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
3649 THEN RESA_TAC;
3650
3651
3652 MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
3653 ;
3654
3655
3656 POP_ASSUM MP_TAC
3657 THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
3658 THEN RESA_TAC
3659 THEN ASM_TAC
3660 THEN REWRITE_TAC[periodic2]
3661 THEN REPEAT DISCH_TAC
3662 THEN ASM_REWRITE_TAC[];
3663
3664
3665
3666
3667
3668
3669
3670  MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
3671 ;
3672
3673
3674
3675
3676
3677 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
3678 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'))`)
3679 THEN RESA_TAC;
3680
3681
3682 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
3683 THEN MP_TAC(REAL_ARITH`~(c < scs_bm_v39 s i j) ==>  scs_bm_v39 s i j<= c`)
3684 THEN RESA_TAC
3685 ;
3686
3687
3688 ASM_TAC
3689 THEN REWRITE_TAC[periodic2]
3690 THEN REPEAT DISCH_TAC
3691 THEN POP_ASSUM MP_TAC
3692 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3693 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3694 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3695 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3696 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3697 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3698 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
3699 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3700 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3701 ;
3702
3703
3704
3705
3706 ASM_TAC
3707 THEN REWRITE_TAC[periodic2]
3708 THEN REPEAT DISCH_TAC
3709 THEN POP_ASSUM MP_TAC
3710 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3711 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3712 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3713 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3714 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3715 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3716 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
3717 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3718 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3719 ;
3720
3721
3722
3723
3724 POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
3725 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i'))`)
3726 THEN RESA_TAC;
3727
3728
3729
3730
3731 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC i':num`;`j:num`;`i':num`;`k:num`]
3732 THEN REPLICATE_TAC (35-16)(POP_ASSUM MP_TAC)
3733 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3734 THEN MRESA1_TAC th`i':num`)
3735 THEN ASM_TAC
3736 THEN REWRITE_TAC[periodic2]
3737 THEN REPEAT DISCH_TAC
3738 THEN POP_ASSUM MP_TAC
3739 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3740 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC i':num`[ARITH_RULE`4 MOD 4=0`])
3741 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3742 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3743 THEN REPLICATE_TAC (36-24)(POP_ASSUM MP_TAC)
3744 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3745 THEN MP_TAC th)
3746 THEN POP_ASSUM MP_TAC
3747 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3748 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3749 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3750 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3751 THEN REAL_ARITH_TAC;
3752
3753
3754
3755
3756 REPLICATE_TAC (33-16)(POP_ASSUM MP_TAC)
3757 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3758 THEN MRESA1_TAC th`i':num`)
3759 ;
3760
3761
3762
3763
3764 MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i'))`)
3765 THEN RESA_TAC;
3766
3767
3768
3769
3770 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC i':num`;`j:num`;`i':num`;`k:num`]
3771 THEN REPLICATE_TAC (35-17)(POP_ASSUM MP_TAC)
3772 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3773 THEN MRESA1_TAC th`i':num`)
3774 THEN ASM_TAC
3775 THEN REWRITE_TAC[periodic2]
3776 THEN REPEAT DISCH_TAC
3777 THEN POP_ASSUM MP_TAC
3778 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3779 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC i':num`[ARITH_RULE`4 MOD 4=0`])
3780 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3781 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3782 THEN REPLICATE_TAC (36-24)(POP_ASSUM MP_TAC)
3783 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3784 THEN MP_TAC th)
3785 THEN POP_ASSUM MP_TAC
3786 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3787 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3788 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3789 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3790 THEN REAL_ARITH_TAC;
3791
3792
3793 REPLICATE_TAC (33-17)(POP_ASSUM MP_TAC)
3794 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3795 THEN MRESA1_TAC th`i':num`)
3796 ;
3797
3798
3799
3800
3801 REPLICATE_TAC (32-19)(POP_ASSUM MP_TAC)
3802 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3803 THEN MRESA_TAC th[`i':num`;`j':num`])
3804 ;
3805
3806
3807 POP_ASSUM MP_TAC
3808 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'))`)
3809 THEN RESA_TAC
3810 ;
3811
3812
3813
3814 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
3815 THEN ASM_TAC
3816 THEN REWRITE_TAC[periodic2]
3817 THEN REPEAT DISCH_TAC
3818 THEN POP_ASSUM MP_TAC
3819 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3820 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3821 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3822 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3823 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3824 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
3825 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3826 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3827 ;
3828
3829
3830
3831
3832 REPLICATE_TAC (32-19)(POP_ASSUM MP_TAC)
3833 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3834 THEN MRESA_TAC th[`i':num`;`j':num`])
3835 ;
3836
3837
3838
3839
3840 SUBGOAL_THEN`CARD
3841  {i' | i' < k /\
3842        (&2 * h0 <
3843         (if psort k (i,j) = psort k (i',SUC i')
3844          then c
3845          else scs_b_v39 s i' (SUC i')) \/
3846         &2 < scs_a_v39 s i' (SUC i'))}
3847 <= CARD
3848  {i' | i' < k /\
3849        (&2 * h0 <
3850         (scs_b_v39 s i' (SUC i')) \/
3851         &2 < scs_a_v39 s i' (SUC i'))}`ASSUME_TAC
3852 ;
3853
3854
3855
3856
3857
3858 MATCH_MP_TAC CARD_SUBSET
3859 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
3860 THEN STRIP_TAC;
3861
3862
3863
3864 REPEAT RESA_TAC
3865 ;
3866
3867
3868 POP_ASSUM MP_TAC
3869 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (x,SUC x) \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (x,SUC x))`)
3870 THEN RESA_TAC
3871 ;
3872
3873
3874
3875 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
3876 THEN REPLICATE_TAC (35-25)(POP_ASSUM MP_TAC)
3877 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3878 THEN MP_TAC th)
3879 THEN ASM_TAC
3880 THEN REWRITE_TAC[periodic2]
3881 THEN REPEAT DISCH_TAC
3882 THEN POP_ASSUM MP_TAC
3883 THEN POP_ASSUM MP_TAC
3884 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3885 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3886 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3887 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3888 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
3889 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
3890 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3891 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`])
3892 THEN REAL_ARITH_TAC;
3893
3894
3895 RESA_TAC;
3896
3897
3898
3899 MATCH_MP_TAC FINITE_SUBSET
3900 THEN EXISTS_TAC`0..k`
3901 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
3902 THEN ARITH_TAC;
3903
3904
3905
3906 REPLICATE_TAC (32-20)(POP_ASSUM MP_TAC)
3907 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3908 THEN MP_TAC th)
3909 THEN POP_ASSUM MP_TAC
3910 THEN ARITH_TAC
3911 ;
3912
3913
3914
3915 ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;restriction_cs1_v39;LET_DEF;LET_END_DEF;]
3916 THEN RESA_TAC
3917 ;
3918
3919
3920
3921 DISJ_CASES_TAC(SET_RULE`(!s'. s' = s ==> MMs_v39 s' = {}) \/ ~((!s'. s' = s ==> MMs_v39 s' = {}))`);
3922
3923
3924 ASM_REWRITE_TAC[]
3925 ;
3926
3927
3928
3929 ASM_REWRITE_TAC[]
3930 THEN POP_ASSUM MP_TAC
3931 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
3932 THEN REPEAT STRIP_TAC
3933 THEN POP_ASSUM MP_TAC
3934 THEN RESA_TAC
3935 THEN POP_ASSUM MP_TAC
3936 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[SET_RULE`~(A={})<=> ?ww. A ww`;]
3937 THEN STRIP_TAC
3938 THEN MP_TAC(SET_RULE`c <= scs_a_v39 s i j \/ ~(c <= scs_a_v39 s i j)`)
3939 THEN RESA_TAC;
3940
3941
3942
3943 ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1]
3944 THEN EXISTS_TAC`s:scs_v39`
3945 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;IN]
3946 THEN EXISTS_TAC`ww:num->real^3`
3947 THEN ASM_REWRITE_TAC[];
3948
3949
3950
3951 MP_TAC(SET_RULE`c <= scs_am_v39 s i j \/ ~(c <= scs_am_v39 s i j)`)
3952 THEN RESA_TAC;
3953
3954
3955 SUBGOAL_THEN`c<= norm(ww i- (ww:num->real^3) j)` ASSUME_TAC;
3956
3957
3958
3959
3960 ASM_TAC
3961 THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39;BBprime2_v39;BBprime_v39; BBs_v39;]
3962 THEN REPEAT RESA_TAC
3963 THEN REPLICATE_TAC (22-19)(POP_ASSUM MP_TAC)
3964 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3965 THEN MRESAL_TAC th[`i:num`;`j:num`][dist])
3966 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
3967 THEN REAL_ARITH_TAC
3968 ;
3969
3970
3971
3972
3973
3974 MP_TAC(REAL_ARITH`c <= norm ((ww:num->real^3) i - ww j)==> c = norm (ww i - ww j)\/ c < norm (ww i - ww j)`)
3975 THEN RESA_TAC;
3976
3977
3978
3979 SUBGOAL_THEN`c=scs_am_v39 s i j` ASSUME_TAC
3980 ;
3981
3982
3983
3984
3985 ASM_TAC
3986 THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39;BBprime2_v39;BBprime_v39; BBs_v39;]
3987 THEN REPEAT RESA_TAC
3988 THEN REPLICATE_TAC (25-20)(POP_ASSUM MP_TAC)
3989 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3990 THEN MRESAL_TAC th[`i:num`;`j:num`][dist])
3991 THEN REPLICATE_TAC (1)(POP_ASSUM MP_TAC)
3992 THEN POP_ASSUM(fun th-> REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
3993 THEN REWRITE_TAC[th])
3994 THEN REAL_ARITH_TAC;
3995
3996
3997
3998
3999 REPLICATE_TAC (15-8)(POP_ASSUM MP_TAC)
4000 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
4001 THEN MP_TAC th)
4002 THEN RESA_TAC
4003 THEN POP_ASSUM MP_TAC
4004 THEN POP_ASSUM(fun th-> MP_TAC th)
4005 THEN RESA_TAC
4006 THEN STRIP_TAC
4007 THEN MP_TAC MM_IS_NOT_2EMPTY_SUBDIVISION_C_EQ_AM
4008 THEN RESA_TAC
4009 THEN POP_ASSUM MP_TAC
4010 THEN REWRITE_TAC[dist;]
4011 THEN STRIP_TAC
4012 THEN ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;LET_DEF;LET_END_DEF;]
4013 THEN EXISTS_TAC`restriction_cs2_v39 s i j c`
4014 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;]
4015 THEN EXISTS_TAC`ww:num->real^3`
4016 THEN ASM_REWRITE_TAC[]
4017 THEN POP_ASSUM MATCH_MP_TAC
4018 THEN ASM_REWRITE_TAC[];
4019
4020
4021
4022
4023
4024
4025 ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;LET_DEF;LET_END_DEF;]
4026 THEN EXISTS_TAC`restriction_cs2_v39 s i j c`
4027 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;]
4028 THEN EXISTS_TAC`ww:num->real^3`
4029 THEN ASM_REWRITE_TAC[]
4030 THEN MP_TAC MM_IS_NOT_1EMPTY_SUBDIVISION
4031 THEN RESA_TAC;
4032
4033
4034
4035
4036
4037
4038 MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j)==>  scs_am_v39 s i j<c`)
4039 THEN RESA_TAC
4040 THEN MP_TAC(REAL_ARITH`c < scs_bm_v39 s i j \/ scs_bm_v39 s i j <=c`)
4041 THEN RESA_TAC
4042 ;
4043
4044
4045
4046
4047 ASM_REWRITE_TAC[Basics.set_of_list2_explicit;SET_RULE`A IN{B,C}<=> A=B \/ A=C`]
4048 THEN MP_TAC(ARITH_RULE` c< norm(ww i- (ww:num->real^3) j) \/ norm(ww i- (ww:num->real^3) j)<=c` )
4049 THEN RESA_TAC;
4050
4051
4052
4053
4054
4055
4056 EXISTS_TAC`restriction_cs2_v39 s i j c`
4057 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;]
4058 THEN EXISTS_TAC`ww:num->real^3`
4059 THEN ASM_REWRITE_TAC[]
4060 THEN MP_TAC MM_IS_NOT_2EMPTY_SUBDIVISION
4061 THEN RESA_TAC;
4062
4063
4064
4065 EXISTS_TAC`restriction_cs1_v39 s i j c`
4066 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;]
4067 THEN EXISTS_TAC`ww:num->real^3`
4068 THEN ASM_REWRITE_TAC[]
4069 THEN MP_TAC MM_IS_NOT_2EMPTY_SUBDIVISION1
4070 THEN ASM_REWRITE_TAC[dist]
4071 ;
4072
4073
4074
4075
4076 MP_TAC(REAL_ARITH`scs_bm_v39 s i j <= c ==> ~(c<scs_bm_v39 s i j)`)
4077 THEN RESA_TAC
4078 THEN MP_TAC(REAL_ARITH`c < scs_b_v39 s i j \/ scs_b_v39 s i j<= c`)
4079 THEN RESA_TAC;
4080
4081
4082
4083
4084 MP_TAC(ARITH_RULE` c< norm(ww i- (ww:num->real^3) j) \/ norm(ww i- (ww:num->real^3) j)<=c` )
4085 THEN RESA_TAC;
4086
4087
4088
4089
4090
4091 ASM_TAC
4092 THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39;BBprime2_v39;BBprime_v39; BBs_v39;]
4093 THEN REPEAT RESA_TAC
4094 THEN REPLICATE_TAC (28-21)(POP_ASSUM MP_TAC)
4095 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
4096 THEN MRESAL_TAC th[`i:num`;`j:num`][dist])
4097 THEN REPLICATE_TAC (28-23)(POP_ASSUM MP_TAC)
4098 THEN REAL_ARITH_TAC;
4099
4100
4101
4102
4103
4104
4105
4106
4107
4108 MP_TAC MM_IS_NOT_1EMPTY_SUBDIVISION1
4109 THEN RESA_TAC
4110 THEN POP_ASSUM MP_TAC
4111 THEN ASM_REWRITE_TAC[dist]
4112 THEN STRIP_TAC
4113 THEN EXISTS_TAC`restriction_cs1_v39 s i j c`
4114 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;]
4115 THEN ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;LET_DEF;LET_END_DEF;]
4116 THEN EXISTS_TAC`ww:num->real^3`
4117 THEN ASM_REWRITE_TAC[]
4118 ;
4119
4120
4121
4122 MP_TAC(REAL_ARITH`scs_b_v39 s i j <= c==> ~(c< scs_b_v39 s i j )`)
4123 THEN RESA_TAC
4124 THEN ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;LET_DEF;LET_END_DEF;]
4125 THEN EXISTS_TAC`s:scs_v39`
4126 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. A ww`;]
4127 THEN EXISTS_TAC`ww:num->real^3`
4128 THEN ASM_REWRITE_TAC[]
4129  ;
4130
4131
4132 ]);;
4133
4134
4135
4136
4137
4138
4139
4140
4141
4142
4143  end;;
4144
4145
4146 (*
4147 let check_completeness_claimA_concl =
4148   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
4149 *)
4150
4151
4152
4153