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