1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Local Fan *)
5 (* Author: Hoang Le Truong *)
7 (* ========================================================================= *)
11 remaining conclusions from appendix to Local Fan chapter
15 module Uaghhbm = struct
28 open Wrgcvdr_cizmrrh;;
36 open Flyspeck_constants;;
52 open Wrgcvdr_cizmrrh;;
54 open Flyspeck_constants;;
84 let PERIODIC_PSORT=prove(`~(k=0)==>psort (k) (i + k,j) = psort (k) (i,j)/\
85 psort (k) (i,j+k) = psort (k) (i,j) `,
86 REWRITE_TAC[psort;LET_DEF;LET_END_DEF;]
88 THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]
89 THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`]);;
92 let CASE_PSORT=prove(`psort (k) (i,j) = psort (k) (i',j')
93 ==> (i MOD k=i' MOD k/\ j MOD k= j' MOD k)\/(i MOD k=j' MOD k/\ j MOD k= i' MOD k)`,
94 REWRITE_TAC[psort;LET_DEF;LET_END_DEF;]
95 THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k \/ ~(i MOD k <= j MOD k)`)
97 THEN MP_TAC(ARITH_RULE`i' MOD k <= j' MOD k \/ ~(i' MOD k <= j' MOD k)`)
99 THEN REWRITE_TAC[PAIR_EQ]
102 let C_LE_2_IS_SCS=prove(`is_scs_v39 s /\ ~(i MOD scs_k_v39 s=j MOD scs_k_v39 s)
103 /\ scs_a_v39 s i j <= c
105 REWRITE_TAC[is_scs_v39;periodic2]
106 THEN ABBREV_TAC`k=scs_k_v39 s`
107 THEN REPEAT STRIP_TAC
108 THEN POP_ASSUM MP_TAC
109 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
111 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
112 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
113 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
114 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
115 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
116 THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
117 THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
118 THEN REPLICATE_TAC (27-15)(POP_ASSUM MP_TAC)
119 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
120 THEN MRESA_TAC th[`i MOD k`;`j MOD k`])
121 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
122 THEN REAL_ARITH_TAC);;
126 let C_LT_2_IS_SCS=prove(`is_scs_v39 s /\ ~(i MOD scs_k_v39 s=j MOD scs_k_v39 s)
127 /\ scs_a_v39 s i j < c
129 REWRITE_TAC[is_scs_v39;periodic2]
130 THEN ABBREV_TAC`k=scs_k_v39 s`
131 THEN REPEAT STRIP_TAC
132 THEN POP_ASSUM MP_TAC
133 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
135 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
136 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
137 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
138 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
139 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
140 THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
141 THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
142 THEN REPLICATE_TAC (27-15)(POP_ASSUM MP_TAC)
143 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
144 THEN MRESA_TAC th[`i MOD k`;`j MOD k`])
145 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
146 THEN REAL_ARITH_TAC);;
150 let A_LE_A_OVERRIDE=prove_by_refinement(
153 ==> scs_a_v39 s i' j' <= override (scs_a_v39 s) (scs_k_v39 s) (i,j) c i' j' `,
156 ASM_REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;TRIV_OR_FORALL_THM]
157 THEN MP_TAC(SET_RULE`~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j')) \/ (psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
162 REWRITE_TAC[is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
163 THEN ABBREV_TAC`k=scs_k_v39 s`
164 THEN REPEAT STRIP_TAC
165 THEN POP_ASSUM MP_TAC
166 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
169 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
171 THEN REWRITE_TAC[periodic2]
172 THEN REPEAT STRIP_TAC
173 THEN POP_ASSUM MP_TAC
174 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
175 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
176 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
177 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
178 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
179 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
180 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
181 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])]);;
189 let B_OVERRIDE_LE_B=prove_by_refinement(
192 ==> override (scs_b_v39 s) (scs_k_v39 s) (i,j) c i' j' <= scs_b_v39 s i' j'`,
194 ASM_REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;TRIV_OR_FORALL_THM]
195 THEN MP_TAC(SET_RULE`~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j')) \/ (psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
200 REWRITE_TAC[is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
201 THEN ABBREV_TAC`k=scs_k_v39 s`
202 THEN REPEAT STRIP_TAC
203 THEN POP_ASSUM MP_TAC
204 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
207 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
209 THEN REWRITE_TAC[periodic2]
210 THEN REPEAT STRIP_TAC
211 THEN POP_ASSUM MP_TAC
212 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
213 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
214 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
215 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
216 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
217 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
218 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
219 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])]);;
223 let BB_EQ_UNION_BB_SUBDIVISION=prove_by_refinement(`
225 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j
227 BBs_v39 s = BBs_v39 (restriction_cs1_v39 s i j c) UNION BBs_v39 (restriction_cs2_v39 s i j c)`,
229 REWRITE_TAC[is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
230 THEN ABBREV_TAC`k=scs_k_v39 s`
231 THEN REPEAT STRIP_TAC
232 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
236 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;restriction_cs1_v39;restriction_cs2_v39]
241 ASM_REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;TRIV_OR_FORALL_THM]
242 THEN MP_TAC(SET_RULE`(!i' j'.
243 dist ((x:num->real^3) i',x j') <=
244 (if psort k (i,j) = psort k (i',j') then c else scs_b_v39 s i' j'))\/
247 (if psort k (i,j) = psort k (i',j') then c else scs_b_v39 s i' j'))`)
251 THEN REWRITE_TAC[NOT_FORALL_THM]
257 THEN MP_TAC(SET_RULE`~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j')) \/ (psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
263 THEN POP_ASSUM MP_TAC
264 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i'',j'') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i'',j''))`)
267 MRESA_TAC(GEN_ALL CASE_PSORT)[`i':num`;`j'':num`;`j':num`;`i'':num`;`k:num`];
269 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`x:num->real^3`][ARITH_RULE`~(4=0)`;]
270 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
271 THEN MRESAL1_TAC th`i'':num`[ARITH_RULE`4 MOD 4=0`]
272 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`]
273 THEN MRESAL1_TAC th`j'':num`[ARITH_RULE`4 MOD 4=0`])
278 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`x:num->real^3`][ARITH_RULE`~(4=0)`;]
279 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
280 THEN MRESAL1_TAC th`i'':num`[ARITH_RULE`4 MOD 4=0`]
281 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`]
282 THEN MRESAL1_TAC th`j'':num`[ARITH_RULE`4 MOD 4=0`])
284 THEN ONCE_REWRITE_TAC[DIST_SYM]
285 THEN POP_ASSUM MP_TAC
292 ASM_REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;TRIV_OR_FORALL_THM]
293 THEN MP_TAC(SET_RULE`(!i' j'.
294 dist ((x:num->real^3) i',x j') <=
295 (if psort k (i,j) = psort k (i',j') then c else scs_b_v39 s i' j'))\/
298 (if psort k (i,j) = psort k (i',j') then c else scs_b_v39 s i' j'))`)
302 THEN REWRITE_TAC[NOT_FORALL_THM]
308 THEN MP_TAC(SET_RULE`~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j')) \/ (psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
312 THEN POP_ASSUM MP_TAC
313 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i'',j'') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i'',j''))`)
316 MRESA_TAC(GEN_ALL CASE_PSORT)[`i':num`;`j'':num`;`j':num`;`i'':num`;`k:num`];
318 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`x:num->real^3`][ARITH_RULE`~(4=0)`;]
319 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
320 THEN MRESAL1_TAC th`i'':num`[ARITH_RULE`4 MOD 4=0`]
321 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`]
322 THEN MRESAL1_TAC th`j'':num`[ARITH_RULE`4 MOD 4=0`])
327 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`x:num->real^3`][ARITH_RULE`~(4=0)`;]
328 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
329 THEN MRESAL1_TAC th`i'':num`[ARITH_RULE`4 MOD 4=0`]
330 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`]
331 THEN MRESAL1_TAC th`j'':num`[ARITH_RULE`4 MOD 4=0`])
333 THEN ONCE_REWRITE_TAC[DIST_SYM]
334 THEN POP_ASSUM MP_TAC
340 THEN REMOVE_ASSUM_TAC
341 THEN POP_ASSUM(fun th-> MRESA_TAC th[`i':num`;`j':num`])
342 THEN MP_TAC B_OVERRIDE_LE_B
343 THEN ASM_REWRITE_TAC[is_scs_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
344 THEN REPLICATE_TAC (27-18)(POP_ASSUM MP_TAC)
345 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
346 THEN POP_ASSUM MP_TAC
347 THEN POP_ASSUM MP_TAC
353 THEN REMOVE_ASSUM_TAC
354 THEN POP_ASSUM(fun th-> MRESA_TAC th[`i':num`;`j':num`])
355 THEN MP_TAC B_OVERRIDE_LE_B
356 THEN ASM_REWRITE_TAC[is_scs_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
357 THEN REPLICATE_TAC (27-18)(POP_ASSUM MP_TAC)
358 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
359 THEN POP_ASSUM MP_TAC
360 THEN POP_ASSUM MP_TAC
366 THEN REMOVE_ASSUM_TAC
367 THEN POP_ASSUM(fun th-> MRESA_TAC th[`i':num`;`j':num`])
368 THEN REMOVE_ASSUM_TAC
369 THEN MP_TAC A_LE_A_OVERRIDE
370 THEN ASM_REWRITE_TAC[is_scs_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
371 THEN REPLICATE_TAC (26-18)(POP_ASSUM MP_TAC)
372 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
373 THEN POP_ASSUM MP_TAC
374 THEN POP_ASSUM MP_TAC
380 THEN REMOVE_ASSUM_TAC
381 THEN POP_ASSUM(fun th-> MRESA_TAC th[`i':num`;`j':num`])
382 THEN REMOVE_ASSUM_TAC
383 THEN MP_TAC A_LE_A_OVERRIDE
384 THEN ASM_REWRITE_TAC[is_scs_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
385 THEN REPLICATE_TAC (26-18)(POP_ASSUM MP_TAC)
386 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
387 THEN POP_ASSUM MP_TAC
388 THEN POP_ASSUM MP_TAC
395 let SUBDIVISION_IS_NOT_EAR=prove(`3< scs_k_v39 s
397 ~(is_ear_v39 s)/\ ~(is_ear_v39 (restriction_cs1_v39 s i j c)) /\ ~(is_ear_v39 (restriction_cs2_v39 s i j c))`,
398 REWRITE_TAC[is_scs_v39;is_ear_v39;restriction_cs1_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;unadorned_v39;restriction_cs2_v39]
400 THEN MP_TAC(ARITH_RULE`3< scs_k_v39 s ==> ~(scs_k_v39 s =3)`)
405 let SUBDIVISION_CS1_DSV_EQ=prove(`
408 dsv_v39 (restriction_cs1_v39 s i j c) ww =dsv_v39 s ww
409 /\ dsv_v39 (restriction_cs2_v39 s i j c) ww =dsv_v39 s ww`,
411 THEN MP_TAC SUBDIVISION_IS_NOT_EAR
413 THEN ASM_REWRITE_TAC[dsv_v39]
414 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;dsv_v39;restriction_cs1_v39;restriction_cs2_v39]);;
417 let SUBDIVISION_CS1_TAUSTAR_EQ=prove(`
420 taustar_v39 (restriction_cs1_v39 s i j c) ww =taustar_v39 s ww /\
421 taustar_v39 (restriction_cs2_v39 s i j c) ww =taustar_v39 s ww`,
423 THEN MP_TAC SUBDIVISION_CS1_DSV_EQ
425 THEN ASM_REWRITE_TAC[taustar_v39]
426 THEN MP_TAC(ARITH_RULE`3< scs_k_v39 s ==> ~(scs_k_v39 s <=3)`)
428 THEN ASM_REWRITE_TAC[MMs_v39;BBprime2_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;taustar_v39;restriction_cs1_v39;restriction_cs2_v39]);;
432 let BBPRIME_SUBSET_SUBDIVISION_UNION=prove_by_refinement(`
433 is_scs_v39 s /\ 3< scs_k_v39 s /\
434 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
437 ww IN BBprime_v39 (restriction_cs1_v39 s i j c) UNION BBprime_v39 (restriction_cs2_v39 s i j c)`,
440 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
444 REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
445 THEN ABBREV_TAC`k=scs_k_v39 s`
446 THEN REPEAT STRIP_TAC
447 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
451 THEN ASM_REWRITE_TAC[BBprime_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;]
452 THEN POP_ASSUM MP_TAC
453 THEN POP_ASSUM (fun th-> STRIP_TAC
454 THEN MRESAL1_TAC th`ww:num->real^3`[IN]
455 THEN ASSUME_TAC(th));
457 MATCH_MP_TAC(SET_RULE`A==> A\/B`)
458 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
460 THEN REMOVE_ASSUM_TAC
461 THEN REMOVE_ASSUM_TAC
462 THEN POP_ASSUM(fun th-> STRIP_TAC
463 THEN MRESAL1_TAC th`ww':num->real^3`[IN])
464 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
465 THEN REPLICATE_TAC (32-25)(POP_ASSUM MP_TAC)
466 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
467 THEN MATCH_MP_TAC th)
468 THEN ASM_REWRITE_TAC[];
470 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
471 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
473 THEN REMOVE_ASSUM_TAC
474 THEN REMOVE_ASSUM_TAC
475 THEN POP_ASSUM(fun th-> STRIP_TAC
476 THEN MRESAL1_TAC th`ww':num->real^3`[IN])
477 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
478 THEN REPLICATE_TAC (32-25)(POP_ASSUM MP_TAC)
479 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
480 THEN MATCH_MP_TAC th)
481 THEN ASM_REWRITE_TAC[]]);;
485 let BBPRIME_SUBSET_BBPRIME_SUBDIVISION_UNION = prove(
486 `is_scs_v39 s /\ 3< scs_k_v39 s /\
487 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j
488 ==> BBprime_v39 s SUBSET BBprime_v39 (restriction_cs1_v39 s i j c) UNION BBprime_v39 (restriction_cs2_v39 s i j c)`,
490 THEN REPEAT STRIP_TAC
491 THEN MATCH_MP_TAC BBPRIME_SUBSET_SUBDIVISION_UNION
492 THEN ASM_REWRITE_TAC[]
493 THEN POP_ASSUM MP_TAC
494 THEN REWRITE_TAC[IN]);;
497 (**********c< norm(ww i- ww j)*********)
499 let BBINDEX_EQ_SUBDIVISION=prove_by_refinement(
501 is_scs_v39 s /\ 3< scs_k_v39 s /\
502 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
503 BBs_v39 s ww /\ c< norm(ww i- ww j)
505 BBindex_v39 s ww = BBindex_v39 (restriction_cs2_v39 s i j c) ww`,
508 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
511 THEN REWRITE_TAC[BBindex_v39]
513 REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs2_v39]
514 THEN ABBREV_TAC`k=scs_k_v39 s`
515 THEN REPEAT STRIP_TAC
516 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
519 MATCH_MP_TAC CARD_IMAGE_INJ_EQ
520 THEN REWRITE_TAC[IN_ELIM_THM]
521 THEN EXISTS_TAC`(\i:num. i)`
524 MATCH_MP_TAC FINITE_SUBSET
525 THEN EXISTS_TAC`0..k`
526 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
532 THEN POP_ASSUM MP_TAC
533 THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
536 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`];
539 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
540 THEN REPEAT STRIP_TAC
541 THEN REPLICATE_TAC (32-25)(POP_ASSUM MP_TAC)
542 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
544 THEN POP_ASSUM MP_TAC
545 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
546 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
547 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
548 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
549 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;dist])
553 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
554 THEN REPEAT STRIP_TAC
555 THEN REPLICATE_TAC (32-25)(POP_ASSUM MP_TAC)
556 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
558 THEN POP_ASSUM MP_TAC
559 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
560 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
561 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
562 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
563 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
564 THEN ONCE_REWRITE_TAC[DIST_SYM]
565 THEN REWRITE_TAC[dist]
570 REWRITE_TAC[EXISTS_UNIQUE]
571 THEN EXISTS_TAC`y:num`
572 THEN ASM_REWRITE_TAC[]
574 THEN POP_ASSUM MP_TAC
575 THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (y,SUC y) \/ ~(psort k (i,j) = psort k (y,SUC y))`)
578 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC y:num`;`j:num`;`y:num`;`k:num`];
581 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
582 THEN REPEAT STRIP_TAC
583 THEN REPLICATE_TAC (32-25)(POP_ASSUM MP_TAC)
584 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
586 THEN POP_ASSUM MP_TAC
587 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
588 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
589 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
590 THEN MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`]
591 THEN MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`;])
592 THEN REPLICATE_TAC (37-22)(POP_ASSUM MP_TAC)
593 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
596 THEN REWRITE_TAC[periodic2]
597 THEN REPEAT DISCH_TAC
598 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
599 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
600 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
601 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
602 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
603 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
604 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
605 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
606 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
607 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`;dist])
611 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
612 THEN REPEAT STRIP_TAC
613 THEN REPLICATE_TAC (35-28)(POP_ASSUM MP_TAC)
614 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
616 THEN POP_ASSUM MP_TAC
617 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
618 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
619 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
620 THEN MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`]
621 THEN MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`;])
622 THEN REPLICATE_TAC (37-22)(POP_ASSUM MP_TAC)
623 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
626 THEN REWRITE_TAC[periodic2]
627 THEN REPEAT DISCH_TAC
628 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
629 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
630 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
631 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
632 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
633 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
634 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
635 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
636 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
637 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`;])
638 THEN ONCE_REWRITE_TAC[DIST_SYM]
639 THEN REWRITE_TAC[dist]
640 THEN REAL_ARITH_TAC;]);;
643 let BB_INTER_BBPRIME_SUBDIVISION2= prove_by_refinement(`
644 is_scs_v39 s /\ 3< scs_k_v39 s /\
645 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j
647 (BBprime_v39 s) INTER (BBs_v39 (restriction_cs2_v39 s i j c)) SUBSET
648 (BBprime_v39 (restriction_cs2_v39 s i j c))`,
651 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
653 THEN REWRITE_TAC[INTER;EXTENSION;IN_ELIM_THM;SUBSET]
656 REWRITE_TAC[SUBSET;UNION;IN_ELIM_THM;]
657 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
659 REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;BBprime_v39;IN]
660 THEN ASM_REWRITE_TAC[]
661 THEN REPEAT RESA_TAC;
663 REPLICATE_TAC (11-6)(POP_ASSUM MP_TAC)
664 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
665 THEN MRESA1_TAC th`ww':num->real^3`)
666 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
667 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
668 THEN REPLICATE_TAC (13-5)(POP_ASSUM MP_TAC)
669 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
670 THEN MATCH_MP_TAC th)
671 THEN ASM_REWRITE_TAC[];
673 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`];
675 REPLICATE_TAC (10-6)(POP_ASSUM MP_TAC)
676 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
677 THEN MRESA1_TAC th`ww':num->real^3`)
678 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
679 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
680 THEN REPLICATE_TAC (14-7)(POP_ASSUM MP_TAC)
681 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
682 THEN MATCH_MP_TAC th)
683 THEN ASM_REWRITE_TAC[];
685 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]]);;
690 let CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION= prove_by_refinement(`
691 is_scs_v39 s /\ 3< scs_k_v39 s /\
692 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
693 BBprime_v39 s ww /\ c< norm(ww i- ww j)
695 BBs_v39 (restriction_cs2_v39 s i j c) ww`,
697 REWRITE_TAC[MMs_v39;BBs_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;restriction_cs2_v39]
698 THEN ABBREV_TAC`k=scs_k_v39 s`
700 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
701 THEN REPEAT RESA_TAC;
704 THEN POP_ASSUM(fun th-> STRIP_TAC
706 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
709 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];
711 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
712 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
713 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
714 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
715 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
718 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
719 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
720 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
721 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
722 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
723 THEN ONCE_REWRITE_TAC[DIST_SYM]
724 THEN REWRITE_TAC[dist]
728 THEN POP_ASSUM(fun th-> STRIP_TAC
730 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
733 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];
735 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
736 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
737 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
738 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
739 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
742 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
743 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
744 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
745 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
746 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
747 THEN ONCE_REWRITE_TAC[DIST_SYM]
748 THEN REWRITE_TAC[dist]
749 THEN REAL_ARITH_TAC]);;
751 let BBPRIME_SUBDIVISION2_SUBSET_BBPRIME=prove_by_refinement(`
752 is_scs_v39 s /\ 3< scs_k_v39 s /\
753 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
754 BBprime_v39 s ww /\ c< norm(ww i- ww j)
756 (BBprime_v39 (restriction_cs2_v39 s i j c)) SUBSET (BBprime_v39 s) `,
759 THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION
761 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
762 THEN ASM_REWRITE_TAC[EXTENSION;IN]
764 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
765 THEN ABBREV_TAC`k=scs_k_v39 s`
766 THEN REPEAT RESA_TAC;
768 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
769 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
770 THEN REPLICATE_TAC (37-31)(POP_ASSUM MP_TAC)
771 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
772 THEN MRESA1_TAC th`ww:num->real^3`)
773 THEN REPLICATE_TAC (37-29)(POP_ASSUM MP_TAC)
774 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
775 THEN MRESA1_TAC th`ww':num->real^3`)
776 THEN REPLICATE_TAC (37-25)(POP_ASSUM MP_TAC)
777 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
778 THEN MRESA1_TAC th`ww':num->real^3`)
779 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
782 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
783 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
784 THEN REPLICATE_TAC (37-31)(POP_ASSUM MP_TAC)
785 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
786 THEN MRESA1_TAC th`ww:num->real^3`)
787 THEN REPLICATE_TAC (37-29)(POP_ASSUM MP_TAC)
788 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
789 THEN MRESA1_TAC th`ww':num->real^3`)
790 THEN REPLICATE_TAC (37-25)(POP_ASSUM MP_TAC)
791 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
792 THEN MRESA1_TAC th`ww':num->real^3`)
793 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
797 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]]);;
801 let IN_BBPRIME_SUBDIVISION=prove_by_refinement(`
802 is_scs_v39 s /\ 3< scs_k_v39 s /\
803 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
804 BBprime_v39 s ww /\ c< norm(ww i- ww j)
806 BBprime_v39 (restriction_cs2_v39 s i j c) ww`,
809 THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION
811 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
812 THEN ASM_REWRITE_TAC[EXTENSION;UNION;IN_ELIM_THM]
815 THEN ASM_REWRITE_TAC[BBprime_v39]
816 THEN REPEAT RESA_TAC;
819 THEN POP_ASSUM (fun th -> STRIP_TAC
820 THEN MRESA1_TAC th`ww':num->real^3`)
821 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
822 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
824 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
826 THEN REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
827 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
828 THEN MRESA1_TAC th`ww':num->real^3`);
830 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
832 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
833 THEN REPEAT RESA_TAC]);;
837 let MIN_NUM_SUBSET=prove(
838 `X SUBSET Y/\ a IN X==> min_num Y<= min_num X`,
841 THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`X:num->bool`;`a:num`]
842 THEN MP_TAC(SET_RULE`X (min_num X) /\ X SUBSET Y==> Y (min_num X)`)
844 THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`Y:num->bool`;`min_num X`]);;
847 let BBINDEX_MIN_S_LE_SUBDIVISION2=prove_by_refinement(`
848 is_scs_v39 s /\ 3< scs_k_v39 s /\
849 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
850 BBprime_v39 s ww /\ c< norm(ww i- ww j)
852 BBindex_min_v39 s <= min_num
853 (IMAGE (BBindex_v39 s)
854 (BBprime_v39 (restriction_cs2_v39 s i j c)))`,
857 THEN MP_TAC BBPRIME_SUBSET_BBPRIME_SUBDIVISION_UNION
859 THEN REWRITE_TAC[BBindex_min_v39]
860 THEN MATCH_MP_TAC(GEN_ALL MIN_NUM_SUBSET)
861 THEN EXISTS_TAC`BBindex_v39 s ww`
864 MATCH_MP_TAC IMAGE_SUBSET
865 THEN MP_TAC BBPRIME_SUBDIVISION2_SUBSET_BBPRIME
868 REWRITE_TAC[IMAGE;IN_ELIM_THM]
869 THEN EXISTS_TAC`ww:num->real^3`
871 THEN MP_TAC IN_BBPRIME_SUBDIVISION
875 let BBINDEX_BBPRIME_LE_SUBDIVISION2=prove_by_refinement(`
876 is_scs_v39 s /\ 3< scs_k_v39 s /\
877 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
878 BBprime_v39 s ww /\ c< norm(ww i- ww j)/\
879 BBprime_v39 (restriction_cs2_v39 s i j c) vv
881 BBindex_v39 s vv<= BBindex_v39 (restriction_cs2_v39 s i j c) vv`,
885 THEN REWRITE_TAC[BBindex_v39]
888 REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs2_v39;IN;BBs_v39]
889 THEN ABBREV_TAC`k=scs_k_v39 s`
890 THEN REPEAT STRIP_TAC
891 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
896 MATCH_MP_TAC CARD_SUBSET
897 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
898 THEN REPEAT RESA_TAC;
901 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
906 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
907 THEN REPLICATE_TAC (41-33)(POP_ASSUM MP_TAC)
908 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
909 THEN MRESA_TAC th[`x:num`;`SUC x`])
910 THEN REMOVE_ASSUM_TAC
911 THEN REPLICATE_TAC (41-37)(POP_ASSUM MP_TAC)
912 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
914 THEN REPLICATE_TAC (40-22)(POP_ASSUM MP_TAC)
915 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
917 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
918 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
919 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
920 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
921 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
922 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
924 THEN REWRITE_TAC[periodic2]
925 THEN REPEAT DISCH_TAC
926 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
927 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
928 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
929 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
930 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
931 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
932 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
933 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
934 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
935 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
941 MATCH_MP_TAC FINITE_SUBSET
942 THEN EXISTS_TAC`0..k`
943 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
951 MATCH_MP_TAC CARD_SUBSET
952 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
953 THEN REPEAT RESA_TAC;
956 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
961 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
962 THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
963 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
964 THEN MRESA_TAC th[`x:num`;`SUC x`])
965 THEN REMOVE_ASSUM_TAC
966 THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
967 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
969 THEN REPLICATE_TAC (41-22)(POP_ASSUM MP_TAC)
970 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
972 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
973 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
974 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
975 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
976 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
977 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
979 THEN REWRITE_TAC[periodic2]
980 THEN REPEAT DISCH_TAC
981 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
982 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
983 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
984 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
985 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
986 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
987 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
988 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
989 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
990 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
996 MATCH_MP_TAC FINITE_SUBSET
997 THEN EXISTS_TAC`0..k`
998 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
1007 MATCH_MP_TAC CARD_SUBSET
1008 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
1009 THEN REPEAT RESA_TAC;
1012 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
1017 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
1018 THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
1019 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1020 THEN MRESA_TAC th[`x:num`;`SUC x`])
1021 THEN REMOVE_ASSUM_TAC
1022 THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
1023 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1025 THEN REPLICATE_TAC (41-22)(POP_ASSUM MP_TAC)
1026 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1028 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
1029 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
1030 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1031 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1032 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
1033 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
1035 THEN REWRITE_TAC[periodic2]
1036 THEN REPEAT DISCH_TAC
1037 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
1038 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
1039 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
1040 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
1041 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
1042 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1043 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
1044 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
1045 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
1046 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
1047 THEN REAL_ARITH_TAC;
1052 MATCH_MP_TAC FINITE_SUBSET
1053 THEN EXISTS_TAC`0..k`
1054 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
1059 MATCH_MP_TAC CARD_SUBSET
1060 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
1061 THEN REPEAT RESA_TAC;
1064 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
1069 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
1070 THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
1071 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1072 THEN MRESA_TAC th[`x:num`;`SUC x`])
1073 THEN REMOVE_ASSUM_TAC
1074 THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
1075 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1077 THEN REPLICATE_TAC (41-22)(POP_ASSUM MP_TAC)
1078 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1080 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
1081 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
1082 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1083 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1084 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
1085 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
1087 THEN REWRITE_TAC[periodic2]
1088 THEN REPEAT DISCH_TAC
1089 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
1090 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
1091 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
1092 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
1093 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
1094 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1095 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
1096 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
1097 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
1098 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
1099 THEN REAL_ARITH_TAC;
1104 MATCH_MP_TAC FINITE_SUBSET
1105 THEN EXISTS_TAC`0..k`
1106 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
1115 let MIN_NUM_LE_IMAGE=prove_by_refinement(`
1116 (a:A) IN s/\ (!x. x IN s==> f x <= g x) ==> min_num (IMAGE f s)<= min_num (IMAGE g s)`,
1119 THEN SUBGOAL_THEN `g (a:A) IN ((IMAGE g s):num->bool)`ASSUME_TAC;
1121 ASM_REWRITE_TAC[IN_ELIM_THM;IMAGE]
1122 THEN EXISTS_TAC`a:A`
1126 THEN REWRITE_TAC[IN]
1128 THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`(IMAGE g (s:A->bool)):num->bool`;`(g (a:A)):num`]
1129 THEN SUBGOAL_THEN`(min_num (IMAGE g s)) IN IMAGE g (s:A->bool)`ASSUME_TAC;
1131 ASM_REWRITE_TAC[IN];
1134 THEN REWRITE_TAC[IN_ELIM_THM;IMAGE]
1136 THEN REPLICATE_TAC (6-1)(POP_ASSUM MP_TAC)
1137 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1138 THEN MRESA1_TAC th`x:A`)
1139 THEN POP_ASSUM MP_TAC
1140 THEN SUBGOAL_THEN `f (x:A) IN ((IMAGE f s):num->bool)`ASSUME_TAC;
1142 ASM_REWRITE_TAC[IN_ELIM_THM;IMAGE]
1143 THEN EXISTS_TAC`x:A`
1147 THEN REWRITE_TAC[IN]
1149 THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`(IMAGE f (s:A->bool)):num->bool`;`(f:A->num) (x:A)`]
1150 THEN POP_ASSUM MP_TAC
1151 THEN REWRITE_TAC[IMAGE;IN]
1155 let CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION2=prove(`
1156 is_scs_v39 s /\ 3< scs_k_v39 s /\
1157 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1158 BBprime_v39 s ww /\ c< norm(ww i- ww j)
1161 (IMAGE (BBindex_v39 s)
1162 (BBprime_v39 (restriction_cs2_v39 s i j c)))
1164 (IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c))
1165 (BBprime_v39 (restriction_cs2_v39 s i j c)))`,
1167 THEN MATCH_MP_TAC (GEN_ALL MIN_NUM_LE_IMAGE)
1168 THEN EXISTS_TAC`ww:num->real^3`
1169 THEN MP_TAC IN_BBPRIME_SUBDIVISION
1170 THEN ASM_REWRITE_TAC[IN]
1172 THEN REPEAT STRIP_TAC
1173 THEN MATCH_MP_TAC BBINDEX_BBPRIME_LE_SUBDIVISION2
1174 THEN ASM_REWRITE_TAC[]);;
1177 let BBindex_min_LE_SUBDIVISION2=prove(`
1178 is_scs_v39 s /\ 3< scs_k_v39 s /\
1179 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1180 BBprime_v39 s ww /\ c< norm(ww i- ww j)
1182 BBindex_min_v39 s <= BBindex_min_v39 (restriction_cs2_v39 s i j c)`,
1184 THEN MP_TAC CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION2
1186 THEN MP_TAC BBINDEX_MIN_S_LE_SUBDIVISION2
1188 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
1189 THEN REWRITE_TAC[BBindex_min_v39]
1193 let BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION=prove_by_refinement(`
1194 is_scs_v39 s /\ 3< scs_k_v39 s /\
1195 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1196 MMs_v39 s ww /\ c< norm(ww i- ww j)
1198 ww IN BBprime2_v39 (restriction_cs2_v39 s i j c)`,
1201 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
1205 REWRITE_TAC[MMs_v39;BBprime2_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
1206 THEN ABBREV_TAC`k=scs_k_v39 s`
1207 THEN REPEAT STRIP_TAC
1208 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
1212 THEN ASM_REWRITE_TAC[BBprime2_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;]
1213 THEN MP_TAC IN_BBPRIME_SUBDIVISION
1215 THEN SUBGOAL_THEN`BBs_v39 s ww` ASSUME_TAC;
1218 THEN REWRITE_TAC[BBprime_v39;LET_DEF;LET_END_DEF]
1219 THEN REPEAT RESA_TAC;
1221 MP_TAC BBINDEX_EQ_SUBDIVISION
1223 THEN MP_TAC BBindex_min_LE_SUBDIVISION2
1225 THEN POP_ASSUM MP_TAC
1226 THEN REWRITE_TAC[BBindex_min_v39]
1227 THEN SUBGOAL_THEN`(BBindex_v39 (restriction_cs2_v39 s i j c) ww)
1228 IN IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c))
1229 (BBprime_v39 (restriction_cs2_v39 s i j c))`ASSUME_TAC;
1231 REWRITE_TAC[IN_ELIM_THM;IMAGE]
1232 THEN EXISTS_TAC`ww:num->real^3`
1233 THEN ASM_REWRITE_TAC[IN];
1236 THEN REWRITE_TAC[IN]
1238 THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c)) (BBprime_v39 (restriction_cs2_v39 s i j c))`;`BBindex_v39 (restriction_cs2_v39 s i j c) ww`]
1239 THEN POP_ASSUM MP_TAC
1244 let MM_IS_NOT_2EMPTY_SUBDIVISION=prove_by_refinement(`
1245 is_scs_v39 s /\ 3< scs_k_v39 s /\
1246 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1247 scs_am_v39 s i j < c/\
1248 MMs_v39 s ww /\ c< norm(ww i- ww j)
1250 ww IN MMs_v39 (restriction_cs2_v39 s i j c)`,
1253 THEN MP_TAC BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION
1256 THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39]
1257 THEN REPEAT RESA_TAC
1258 THEN REWRITE_TAC[override]
1259 THEN ABBREV_TAC`k=scs_k_v39 s`
1260 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
1262 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
1266 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];
1270 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
1271 THEN REPEAT STRIP_TAC;
1274 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1275 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1277 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1278 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1279 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1280 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1281 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
1282 THEN REAL_ARITH_TAC;
1285 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1286 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1288 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1289 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1290 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1291 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1292 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
1293 THEN REAL_ARITH_TAC;
1295 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1296 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1298 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1299 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1300 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1301 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1302 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
1303 THEN REAL_ARITH_TAC;
1306 REPLICATE_TAC (27-17)(POP_ASSUM MP_TAC)
1307 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1309 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1310 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1311 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1312 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1313 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
1314 THEN REAL_ARITH_TAC;
1317 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
1318 THEN REPEAT STRIP_TAC;
1320 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1321 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1323 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1324 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1325 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1326 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1327 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1328 THEN ONCE_REWRITE_TAC[DIST_SYM]
1329 THEN REWRITE_TAC[dist]
1330 THEN REAL_ARITH_TAC;
1332 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1333 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1335 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1336 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1337 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1338 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1339 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1340 THEN ONCE_REWRITE_TAC[DIST_SYM]
1341 THEN REWRITE_TAC[dist]
1342 THEN REAL_ARITH_TAC;
1344 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1345 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1347 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1348 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1349 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1350 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1351 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1352 THEN ONCE_REWRITE_TAC[DIST_SYM]
1353 THEN REWRITE_TAC[dist]
1354 THEN REAL_ARITH_TAC;
1356 REPLICATE_TAC (27-17)(POP_ASSUM MP_TAC)
1357 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1359 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1360 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1361 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1362 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1363 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1364 THEN ONCE_REWRITE_TAC[DIST_SYM]
1365 THEN REWRITE_TAC[dist]
1366 THEN REAL_ARITH_TAC]);;
1370 let MM_IS_NOT_1EMPTY_SUBDIVISION=prove_by_refinement(
1372 is_scs_v39 s /\ 3< scs_k_v39 s /\
1373 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1374 c<= scs_am_v39 s i j /\
1375 MMs_v39 s ww /\ c< norm(ww i- ww j)
1377 ww IN MMs_v39 (restriction_cs2_v39 s i j c)`,
1379 THEN MP_TAC BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION
1382 THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39]
1383 THEN REPEAT RESA_TAC
1384 THEN REWRITE_TAC[override]
1385 THEN ABBREV_TAC`k=scs_k_v39 s`
1386 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
1388 THEN MP_TAC(REAL_ARITH`c<= scs_am_v39 s i j==> ~(scs_am_v39 s i j<c)`)
1393 (********************************)
1397 let BBINDEX_EQ_SUBDIVISION1=prove_by_refinement(
1399 is_scs_v39 s /\ 3< scs_k_v39 s /\
1400 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1401 BBs_v39 s ww /\ dist(ww i,ww j) <= c
1403 BBindex_v39 s ww = BBindex_v39 (restriction_cs1_v39 s i j c) ww`,
1405 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
1408 THEN REWRITE_TAC[BBindex_v39]
1410 REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs1_v39]
1411 THEN ABBREV_TAC`k=scs_k_v39 s`
1412 THEN REPEAT STRIP_TAC
1413 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
1417 let CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION1= prove_by_refinement(
1419 is_scs_v39 s /\ 3< scs_k_v39 s /\
1420 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1421 BBprime_v39 s ww /\ dist(ww i,ww j) <= c
1423 BBs_v39 (restriction_cs1_v39 s i j c) ww`,
1425 REWRITE_TAC[MMs_v39;BBs_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;restriction_cs1_v39]
1426 THEN ABBREV_TAC`k=scs_k_v39 s`
1428 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
1429 THEN REPEAT RESA_TAC;
1432 THEN POP_ASSUM(fun th-> STRIP_TAC
1434 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
1437 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];
1439 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1440 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1441 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1442 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1443 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
1444 THEN REAL_ARITH_TAC;
1446 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1447 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1448 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1449 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1450 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1452 THEN ONCE_REWRITE_TAC[DIST_SYM]
1456 THEN POP_ASSUM(fun th-> STRIP_TAC
1458 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
1461 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];
1463 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1464 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1465 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1466 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1467 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
1468 THEN REAL_ARITH_TAC;
1470 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1471 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1472 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1473 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1474 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1476 THEN ONCE_REWRITE_TAC[DIST_SYM]
1482 let IN_BBPRIME_SUBDIVISION1=prove_by_refinement(
1484 is_scs_v39 s /\ 3< scs_k_v39 s /\
1485 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1486 BBprime_v39 s ww /\ dist(ww i,ww j) <= c
1488 BBprime_v39 (restriction_cs1_v39 s i j c) ww`,
1491 THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION1
1493 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
1494 THEN ASM_REWRITE_TAC[EXTENSION;UNION;IN_ELIM_THM]
1495 THEN REWRITE_TAC[IN]
1497 THEN ASM_REWRITE_TAC[BBprime_v39]
1498 THEN REPEAT RESA_TAC;
1501 THEN POP_ASSUM (fun th -> STRIP_TAC
1502 THEN MRESA1_TAC th`ww':num->real^3`)
1503 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
1504 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
1506 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
1507 THEN REPEAT RESA_TAC
1508 THEN REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
1509 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1510 THEN MRESA1_TAC th`ww':num->real^3`);
1512 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
1514 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
1515 THEN REPEAT RESA_TAC]);;
1521 let BBPRIME_SUBDIVISION2_SUBSET_BBPRIME1=prove_by_refinement(
1523 is_scs_v39 s /\ 3< scs_k_v39 s /\
1524 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1525 BBprime_v39 s ww /\ dist(ww i,ww j) <= c
1527 (BBprime_v39 (restriction_cs1_v39 s i j c)) SUBSET (BBprime_v39 s) `,
1530 THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION1
1532 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
1533 THEN ASM_REWRITE_TAC[EXTENSION;IN]
1535 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
1536 THEN ABBREV_TAC`k=scs_k_v39 s`
1537 THEN REPEAT RESA_TAC;
1540 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
1541 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
1542 THEN REPLICATE_TAC (36-30)(POP_ASSUM MP_TAC)
1543 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1544 THEN MRESA1_TAC th`ww':num->real^3`);
1547 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
1548 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
1549 THEN REPLICATE_TAC (37-29)(POP_ASSUM MP_TAC)
1550 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1551 THEN MRESA1_TAC th`ww':num->real^3`)
1552 THEN REPLICATE_TAC (37-25)(POP_ASSUM MP_TAC)
1553 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1554 THEN MRESA1_TAC th`ww':num->real^3`)
1555 THEN REPLICATE_TAC (37-29)(POP_ASSUM MP_TAC)
1556 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1557 THEN MRESA1_TAC th`ww:num->real^3`)
1558 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
1559 THEN REAL_ARITH_TAC;
1562 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]]);;
1568 let BBINDEX_MIN_S_LE_SUBDIVISION1=prove_by_refinement(
1570 is_scs_v39 s /\ 3< scs_k_v39 s /\
1571 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1572 BBprime_v39 s ww /\ dist(ww i,ww j) <= c
1574 BBindex_min_v39 s <= min_num
1575 (IMAGE (BBindex_v39 s)
1576 (BBprime_v39 (restriction_cs1_v39 s i j c)))`,
1579 THEN MP_TAC BBPRIME_SUBSET_BBPRIME_SUBDIVISION_UNION
1581 THEN REWRITE_TAC[BBindex_min_v39]
1582 THEN MATCH_MP_TAC(GEN_ALL MIN_NUM_SUBSET)
1583 THEN EXISTS_TAC`BBindex_v39 s ww`
1586 MATCH_MP_TAC IMAGE_SUBSET
1587 THEN MP_TAC BBPRIME_SUBDIVISION2_SUBSET_BBPRIME1
1590 REWRITE_TAC[IMAGE;IN_ELIM_THM]
1591 THEN EXISTS_TAC`ww:num->real^3`
1592 THEN REWRITE_TAC[IN]
1593 THEN MP_TAC IN_BBPRIME_SUBDIVISION1
1601 let BBINDEX_BBPRIME_LE_SUBDIVISION1=prove_by_refinement(
1603 is_scs_v39 s /\ 3< scs_k_v39 s /\
1604 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1605 BBprime_v39 s ww /\ dist(ww i,ww j) <= c/\
1606 BBprime_v39 (restriction_cs1_v39 s i j c) vv
1608 BBindex_v39 s vv= BBindex_v39 (restriction_cs1_v39 s i j c) vv`,
1610 THEN REWRITE_TAC[BBindex_v39]
1613 REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs1_v39;IN;BBs_v39]
1614 THEN ABBREV_TAC`k=scs_k_v39 s`
1615 THEN REPEAT STRIP_TAC
1616 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
1622 let CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION1=prove(`
1623 is_scs_v39 s /\ 3< scs_k_v39 s /\
1624 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1625 BBprime_v39 s ww /\ dist(ww i,ww j) <= c
1628 (IMAGE (BBindex_v39 s)
1629 (BBprime_v39 (restriction_cs1_v39 s i j c)))
1631 (IMAGE (BBindex_v39 (restriction_cs1_v39 s i j c))
1632 (BBprime_v39 (restriction_cs1_v39 s i j c)))`,
1634 THEN MATCH_MP_TAC (GEN_ALL MIN_NUM_LE_IMAGE)
1635 THEN EXISTS_TAC`ww:num->real^3`
1636 THEN MP_TAC IN_BBPRIME_SUBDIVISION1
1637 THEN ASM_REWRITE_TAC[IN]
1639 THEN REPEAT STRIP_TAC
1640 THEN MRESA_TAC(GEN_ALL BBINDEX_BBPRIME_LE_SUBDIVISION1)[`ww:num->real^3`;`s:scs_v39`;`i:num`;`j:num`;`c:real`;`x:num->real^3`]
1645 let BBindex_min_LE_SUBDIVISION1=prove(`
1646 is_scs_v39 s /\ 3< scs_k_v39 s /\
1647 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1648 BBprime_v39 s ww /\ dist(ww i,ww j) <= c
1650 BBindex_min_v39 s <= BBindex_min_v39 (restriction_cs1_v39 s i j c)`,
1652 THEN MP_TAC CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION1
1654 THEN MP_TAC BBINDEX_MIN_S_LE_SUBDIVISION1
1656 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
1657 THEN REWRITE_TAC[BBindex_min_v39]
1662 let BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION1=prove_by_refinement(
1664 is_scs_v39 s /\ 3< scs_k_v39 s /\
1665 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1666 MMs_v39 s ww /\ dist(ww i,ww j) <= c
1668 ww IN BBprime2_v39 (restriction_cs1_v39 s i j c)`,
1671 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
1675 REWRITE_TAC[MMs_v39;BBprime2_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
1676 THEN ABBREV_TAC`k=scs_k_v39 s`
1677 THEN REPEAT STRIP_TAC
1678 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
1682 THEN ASM_REWRITE_TAC[BBprime2_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;]
1683 THEN MP_TAC IN_BBPRIME_SUBDIVISION1
1685 THEN SUBGOAL_THEN`BBs_v39 s ww` ASSUME_TAC;
1688 THEN REWRITE_TAC[BBprime_v39;LET_DEF;LET_END_DEF]
1689 THEN REPEAT RESA_TAC;
1691 MP_TAC BBINDEX_EQ_SUBDIVISION1
1693 THEN MP_TAC BBindex_min_LE_SUBDIVISION1
1695 THEN POP_ASSUM MP_TAC
1696 THEN REWRITE_TAC[BBindex_min_v39]
1697 THEN SUBGOAL_THEN`(BBindex_v39 (restriction_cs1_v39 s i j c) ww)
1698 IN IMAGE (BBindex_v39 (restriction_cs1_v39 s i j c))
1699 (BBprime_v39 (restriction_cs1_v39 s i j c))`ASSUME_TAC;
1701 REWRITE_TAC[IN_ELIM_THM;IMAGE]
1702 THEN EXISTS_TAC`ww:num->real^3`
1703 THEN ASM_REWRITE_TAC[IN];
1706 THEN REWRITE_TAC[IN]
1708 THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`IMAGE (BBindex_v39 (restriction_cs1_v39 s i j c)) (BBprime_v39 (restriction_cs1_v39 s i j c))`;`BBindex_v39 (restriction_cs1_v39 s i j c) ww`]
1709 THEN POP_ASSUM MP_TAC
1715 let MM_IS_NOT_2EMPTY_SUBDIVISION1=prove_by_refinement(
1717 is_scs_v39 s /\ 3< scs_k_v39 s /\
1718 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1719 c < scs_bm_v39 s i j/\
1720 MMs_v39 s ww /\ dist(ww i,ww j) <= c
1722 ww IN MMs_v39 (restriction_cs1_v39 s i j c)`,
1724 THEN MP_TAC BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION1
1727 THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs1_v39]
1728 THEN REPEAT RESA_TAC
1729 THEN REWRITE_TAC[override]
1730 THEN ABBREV_TAC`k=scs_k_v39 s`
1731 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
1733 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
1738 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];
1742 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
1743 THEN REPEAT STRIP_TAC;
1746 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1747 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1749 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1750 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1751 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1752 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1753 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1754 THEN REAL_ARITH_TAC;
1758 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1759 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1761 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1762 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1763 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1764 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1765 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1766 THEN REAL_ARITH_TAC;
1768 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1769 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1771 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1772 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1773 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1774 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1775 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
1776 THEN REAL_ARITH_TAC;
1779 REPLICATE_TAC (27-17)(POP_ASSUM MP_TAC)
1780 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1782 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1783 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1784 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1785 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1786 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
1787 THEN REAL_ARITH_TAC;
1790 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
1791 THEN REPEAT STRIP_TAC;
1793 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1794 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1796 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1797 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1798 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1799 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1800 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1802 THEN ONCE_REWRITE_TAC[DIST_SYM]
1805 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1806 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1808 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1809 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1810 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1811 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1812 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1814 THEN ONCE_REWRITE_TAC[DIST_SYM]
1817 REPLICATE_TAC (28-17)(POP_ASSUM MP_TAC)
1818 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1820 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1821 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1822 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1823 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1824 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1826 THEN ONCE_REWRITE_TAC[DIST_SYM]
1829 REPLICATE_TAC (27-17)(POP_ASSUM MP_TAC)
1830 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1832 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1833 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1834 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1835 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
1836 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
1838 THEN ONCE_REWRITE_TAC[DIST_SYM]
1843 let MM_IS_NOT_1EMPTY_SUBDIVISION1=prove_by_refinement(
1845 is_scs_v39 s /\ 3< scs_k_v39 s /\
1846 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1847 scs_bm_v39 s i j <=c /\
1848 MMs_v39 s ww /\ dist(ww i,ww j) <= c
1850 ww IN MMs_v39 (restriction_cs1_v39 s i j c)`,
1852 THEN MP_TAC BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION1
1855 THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs1_v39]
1856 THEN REPEAT RESA_TAC
1857 THEN REWRITE_TAC[override]
1858 THEN ABBREV_TAC`k=scs_k_v39 s`
1859 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
1861 THEN MP_TAC(REAL_ARITH`scs_bm_v39 s i j <= c==> ~(c< scs_bm_v39 s i j)`)
1867 let BBINDEX_EQ_SUBDIVISION_C_EQ_AM=prove_by_refinement(
1869 is_scs_v39 s /\ 3< scs_k_v39 s /\
1870 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1871 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j))) /\
1872 BBs_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c
1874 BBindex_v39 s ww = BBindex_v39 (restriction_cs2_v39 s i j c) ww`,
1877 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
1880 THEN REWRITE_TAC[BBindex_v39]
1882 REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs2_v39]
1883 THEN ABBREV_TAC`k=scs_k_v39 s`
1884 THEN REPEAT STRIP_TAC
1885 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
1888 MATCH_MP_TAC CARD_IMAGE_INJ_EQ
1889 THEN REWRITE_TAC[IN_ELIM_THM]
1890 THEN EXISTS_TAC`(\i:num. i)`
1893 MATCH_MP_TAC FINITE_SUBSET
1894 THEN EXISTS_TAC`0..k`
1895 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
1901 THEN POP_ASSUM MP_TAC
1902 THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
1905 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`];
1908 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
1909 THEN REPEAT STRIP_TAC
1910 THEN REPLICATE_TAC (37-24)(POP_ASSUM MP_TAC)
1911 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1913 THEN POP_ASSUM MP_TAC
1914 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1915 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1916 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1917 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
1918 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;dist])
1919 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x:num`;`i:num`;`k:num`][];
1922 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
1923 THEN REPEAT STRIP_TAC
1924 THEN REPLICATE_TAC (37-24)(POP_ASSUM MP_TAC)
1925 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1927 THEN POP_ASSUM MP_TAC
1928 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1929 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1930 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1931 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
1932 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;dist])
1933 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x:num`;`j:num`;`k:num`][];
1937 REWRITE_TAC[EXISTS_UNIQUE]
1938 THEN EXISTS_TAC`y:num`
1939 THEN ASM_REWRITE_TAC[]
1940 THEN REPEAT RESA_TAC
1941 THEN POP_ASSUM MP_TAC
1942 THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (y,SUC y) \/ ~(psort k (i,j) = psort k (y,SUC y))`)
1945 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC y:num`;`j:num`;`y:num`;`k:num`];
1948 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
1949 THEN REPEAT STRIP_TAC
1950 THEN REPLICATE_TAC (37-24)(POP_ASSUM MP_TAC)
1951 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1953 THEN POP_ASSUM MP_TAC
1954 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1955 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1956 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1957 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
1958 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;dist])
1959 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`y:num`;`i:num`;`k:num`][];
1962 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
1963 THEN REPEAT STRIP_TAC
1964 THEN REPLICATE_TAC (37-24)(POP_ASSUM MP_TAC)
1965 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
1967 THEN POP_ASSUM MP_TAC
1968 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
1969 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
1970 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
1971 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
1972 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;dist])
1973 THEN MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`y:num`;`j:num`;`k:num`][]]);;
1977 let CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION_C_EQ_AM= prove_by_refinement(`
1978 is_scs_v39 s /\ 3< scs_k_v39 s /\
1979 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1980 BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
1981 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
1983 BBs_v39 (restriction_cs2_v39 s i j c) ww`,
1985 REWRITE_TAC[MMs_v39;BBs_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;restriction_cs2_v39]
1986 THEN ABBREV_TAC`k=scs_k_v39 s`
1988 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
1989 THEN REPEAT RESA_TAC;
1991 REPLICATE_TAC (33-30)(POP_ASSUM MP_TAC)
1992 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1994 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
1997 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];
1999 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
2000 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
2001 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
2002 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
2003 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
2004 THEN REAL_ARITH_TAC;
2006 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
2007 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
2008 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
2009 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
2010 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
2012 THEN ONCE_REWRITE_TAC[DIST_SYM]
2013 THEN POP_ASSUM MP_TAC
2014 THEN REAL_ARITH_TAC;
2016 REPLICATE_TAC (33-30)(POP_ASSUM MP_TAC)
2017 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2019 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
2022 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`];
2024 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
2025 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
2026 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
2027 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
2028 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;dist])
2029 THEN REAL_ARITH_TAC;
2031 MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`ww:num->real^3 `][ARITH_RULE`~(4=0)`;]
2032 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
2033 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
2034 THEN MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`]
2035 THEN MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`;])
2037 THEN ONCE_REWRITE_TAC[DIST_SYM]
2038 THEN POP_ASSUM MP_TAC
2039 THEN REAL_ARITH_TAC]);;
2044 let BBPRIME_SUBDIVISION2_SUBSET_BBPRIME_C_EQ_AM=prove_by_refinement(`
2045 is_scs_v39 s /\ 3< scs_k_v39 s /\
2046 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
2047 BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
2048 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
2050 (BBprime_v39 (restriction_cs2_v39 s i j c)) SUBSET (BBprime_v39 s) `,
2053 THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION_C_EQ_AM
2055 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
2056 THEN ASM_REWRITE_TAC[EXTENSION;IN]
2058 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
2059 THEN ABBREV_TAC`k=scs_k_v39 s`
2060 THEN REPEAT RESA_TAC;
2062 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
2063 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
2064 THEN REPLICATE_TAC (39-33)(POP_ASSUM MP_TAC)
2065 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2066 THEN MRESA1_TAC th`ww:num->real^3`)
2067 THEN REPLICATE_TAC (39-31)(POP_ASSUM MP_TAC)
2068 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2069 THEN MRESA1_TAC th`ww':num->real^3`)
2070 THEN REPLICATE_TAC (39-25)(POP_ASSUM MP_TAC)
2071 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2072 THEN MRESA1_TAC th`ww':num->real^3`)
2073 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
2074 THEN REAL_ARITH_TAC;
2076 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
2077 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]
2078 THEN REPLICATE_TAC (39-33)(POP_ASSUM MP_TAC)
2079 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2080 THEN MRESA1_TAC th`ww:num->real^3`)
2081 THEN REPLICATE_TAC (39-31)(POP_ASSUM MP_TAC)
2082 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2083 THEN MRESA1_TAC th`ww':num->real^3`)
2084 THEN REPLICATE_TAC (39-25)(POP_ASSUM MP_TAC)
2085 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2086 THEN MRESA1_TAC th`ww':num->real^3`)
2087 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
2088 THEN REAL_ARITH_TAC;
2091 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`x:num->real^3`]]);;
2096 let IN_BBPRIME_SUBDIVISION_C_EQ_AM=prove_by_refinement(
2098 is_scs_v39 s /\ 3< scs_k_v39 s /\
2099 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
2100 BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
2101 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
2103 BBprime_v39 (restriction_cs2_v39 s i j c) ww`,
2106 THEN MP_TAC CONDITION_BBPRIME_SUBSET_BBPRIME_SUBDIVISION_C_EQ_AM
2108 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
2109 THEN ASM_REWRITE_TAC[EXTENSION;UNION;IN_ELIM_THM]
2110 THEN REWRITE_TAC[IN]
2112 THEN ASM_REWRITE_TAC[BBprime_v39]
2113 THEN REPEAT RESA_TAC;
2116 THEN POP_ASSUM (fun th -> STRIP_TAC
2117 THEN MRESA1_TAC th`ww':num->real^3`)
2118 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
2119 THEN MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww':num->real^3`]
2121 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
2122 THEN REPEAT RESA_TAC
2123 THEN REPLICATE_TAC (35-24)(POP_ASSUM MP_TAC)
2124 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2125 THEN MRESA1_TAC th`ww':num->real^3`);
2127 MRESA_TAC (GEN_ALL SUBDIVISION_CS1_TAUSTAR_EQ)[`i:num`;`j:num`;`c:real`;`s:scs_v39`;`ww:num->real^3`]
2129 THEN REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;SUBSET;IN]
2130 THEN REPEAT RESA_TAC]);;
2135 let BBINDEX_MIN_S_LE_SUBDIVISION2_C_EQ_AM=prove_by_refinement(`
2136 is_scs_v39 s /\ 3< scs_k_v39 s /\
2137 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
2138 BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
2139 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
2141 BBindex_min_v39 s <= min_num
2142 (IMAGE (BBindex_v39 s)
2143 (BBprime_v39 (restriction_cs2_v39 s i j c)))`,
2146 THEN MP_TAC BBPRIME_SUBSET_BBPRIME_SUBDIVISION_UNION
2148 THEN REWRITE_TAC[BBindex_min_v39]
2149 THEN MATCH_MP_TAC(GEN_ALL MIN_NUM_SUBSET)
2150 THEN EXISTS_TAC`BBindex_v39 s ww`
2153 MATCH_MP_TAC IMAGE_SUBSET
2154 THEN MP_TAC BBPRIME_SUBDIVISION2_SUBSET_BBPRIME_C_EQ_AM
2157 REWRITE_TAC[IMAGE;IN_ELIM_THM]
2158 THEN EXISTS_TAC`ww:num->real^3`
2159 THEN REWRITE_TAC[IN]
2160 THEN MP_TAC IN_BBPRIME_SUBDIVISION_C_EQ_AM
2167 let BBINDEX_BBPRIME_LE_SUBDIVISION2_C_EQ_AM=prove_by_refinement(
2169 is_scs_v39 s /\ 3< scs_k_v39 s /\
2170 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
2171 BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
2172 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j))) /\
2173 BBprime_v39 (restriction_cs2_v39 s i j c) vv
2175 BBindex_v39 s vv<= BBindex_v39 (restriction_cs2_v39 s i j c) vv`,
2179 THEN REWRITE_TAC[BBindex_v39]
2182 REWRITE_TAC[MMs_v39;BBprime2_v39;BBprime_v39;is_scs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM;restriction_cs2_v39;IN;BBs_v39]
2183 THEN ABBREV_TAC`k=scs_k_v39 s`
2184 THEN REPEAT STRIP_TAC
2185 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
2191 MATCH_MP_TAC CARD_SUBSET
2192 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
2193 THEN REPEAT RESA_TAC;
2197 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
2203 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
2204 THEN REPLICATE_TAC (41-33)(POP_ASSUM MP_TAC)
2205 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2206 THEN MRESA_TAC th[`x:num`;`SUC x`])
2207 THEN REMOVE_ASSUM_TAC
2208 THEN REPLICATE_TAC (41-37)(POP_ASSUM MP_TAC)
2209 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2211 THEN REPLICATE_TAC (42-22)(POP_ASSUM MP_TAC)
2212 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2214 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
2215 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
2216 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
2217 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
2218 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
2219 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
2221 THEN REWRITE_TAC[periodic2]
2222 THEN REPEAT DISCH_TAC
2223 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
2224 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2225 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2226 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2227 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2228 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2229 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
2230 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
2231 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2232 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
2233 THEN REAL_ARITH_TAC;
2239 MATCH_MP_TAC FINITE_SUBSET
2240 THEN EXISTS_TAC`0..k`
2241 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
2250 MATCH_MP_TAC CARD_SUBSET
2251 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
2252 THEN REPEAT RESA_TAC;
2256 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
2262 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
2263 THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
2264 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2265 THEN MRESA_TAC th[`x:num`;`SUC x`])
2266 THEN REMOVE_ASSUM_TAC
2267 THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
2268 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2270 THEN REPLICATE_TAC (43-22)(POP_ASSUM MP_TAC)
2271 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2273 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
2274 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
2275 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
2276 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
2277 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
2278 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
2280 THEN REWRITE_TAC[periodic2]
2281 THEN REPEAT DISCH_TAC
2282 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
2283 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2284 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2285 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2286 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2287 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2288 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
2289 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
2290 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2291 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
2292 THEN REAL_ARITH_TAC;
2298 MATCH_MP_TAC FINITE_SUBSET
2299 THEN EXISTS_TAC`0..k`
2300 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
2310 MATCH_MP_TAC CARD_SUBSET
2311 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
2312 THEN REPEAT RESA_TAC;
2316 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
2322 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
2323 THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
2324 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2325 THEN MRESA_TAC th[`x:num`;`SUC x`])
2326 THEN REMOVE_ASSUM_TAC
2327 THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
2328 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2330 THEN REPLICATE_TAC (43-22)(POP_ASSUM MP_TAC)
2331 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2333 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
2334 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
2335 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
2336 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
2337 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
2338 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
2340 THEN REWRITE_TAC[periodic2]
2341 THEN REPEAT DISCH_TAC
2342 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
2343 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2344 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2345 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2346 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2347 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2348 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
2349 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
2350 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2351 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
2352 THEN REAL_ARITH_TAC;
2358 MATCH_MP_TAC FINITE_SUBSET
2359 THEN EXISTS_TAC`0..k`
2360 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
2366 MATCH_MP_TAC CARD_SUBSET
2367 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
2368 THEN REPEAT RESA_TAC;
2372 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
2378 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
2379 THEN REPLICATE_TAC (42-33)(POP_ASSUM MP_TAC)
2380 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2381 THEN MRESA_TAC th[`x:num`;`SUC x`])
2382 THEN REMOVE_ASSUM_TAC
2383 THEN REPLICATE_TAC (42-37)(POP_ASSUM MP_TAC)
2384 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2386 THEN REPLICATE_TAC (43-22)(POP_ASSUM MP_TAC)
2387 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2389 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
2390 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3 `][ARITH_RULE`~(4=0)`;]
2391 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
2392 THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
2393 THEN MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`]
2394 THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`;])
2396 THEN REWRITE_TAC[periodic2]
2397 THEN REPEAT DISCH_TAC
2398 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
2399 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2400 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2401 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2402 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2403 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2404 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
2405 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
2406 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2407 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`;])
2408 THEN REAL_ARITH_TAC;
2414 MATCH_MP_TAC FINITE_SUBSET
2415 THEN EXISTS_TAC`0..k`
2416 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
2425 let CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION2_C_EQ_AM=prove(
2427 is_scs_v39 s /\ 3< scs_k_v39 s /\
2428 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
2429 BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
2430 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
2433 (IMAGE (BBindex_v39 s)
2434 (BBprime_v39 (restriction_cs2_v39 s i j c)))
2436 (IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c))
2437 (BBprime_v39 (restriction_cs2_v39 s i j c)))`,
2439 THEN MATCH_MP_TAC (GEN_ALL MIN_NUM_LE_IMAGE)
2440 THEN EXISTS_TAC`ww:num->real^3`
2441 THEN MP_TAC IN_BBPRIME_SUBDIVISION_C_EQ_AM
2442 THEN ASM_REWRITE_TAC[IN]
2444 THEN REPEAT STRIP_TAC
2445 THEN MATCH_MP_TAC BBINDEX_BBPRIME_LE_SUBDIVISION2_C_EQ_AM
2446 THEN ASM_REWRITE_TAC[]);;
2450 let BBindex_min_LE_SUBDIVISION2_C_EQ_AM=prove(`
2451 is_scs_v39 s /\ 3< scs_k_v39 s /\
2452 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
2453 BBprime_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
2454 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
2456 BBindex_min_v39 s <= BBindex_min_v39 (restriction_cs2_v39 s i j c)`,
2458 THEN MP_TAC CLAIM_BBINDEX_BBPRIME_LE_SUBDIVISION2_C_EQ_AM
2460 THEN MP_TAC BBINDEX_MIN_S_LE_SUBDIVISION2_C_EQ_AM
2462 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
2463 THEN REWRITE_TAC[BBindex_min_v39]
2469 let BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION_C_EQ_AM=prove_by_refinement(`
2470 is_scs_v39 s /\ 3< scs_k_v39 s /\
2471 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
2472 MMs_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
2473 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
2475 ww IN BBprime2_v39 (restriction_cs2_v39 s i j c)`,
2478 THEN MP_TAC BB_EQ_UNION_BB_SUBDIVISION
2482 REWRITE_TAC[MMs_v39;BBprime2_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;EXTENSION;UNION;IN_ELIM_THM]
2483 THEN ABBREV_TAC`k=scs_k_v39 s`
2484 THEN REPEAT STRIP_TAC
2485 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
2487 THEN REPEAT RESA_TAC;
2490 THEN ASM_REWRITE_TAC[BBprime2_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;]
2491 THEN MP_TAC IN_BBPRIME_SUBDIVISION_C_EQ_AM
2493 THEN SUBGOAL_THEN`BBs_v39 s ww` ASSUME_TAC;
2496 THEN REWRITE_TAC[BBprime_v39;LET_DEF;LET_END_DEF]
2497 THEN REPEAT RESA_TAC;
2499 MP_TAC BBINDEX_EQ_SUBDIVISION_C_EQ_AM
2501 THEN MP_TAC BBindex_min_LE_SUBDIVISION2_C_EQ_AM
2503 THEN POP_ASSUM MP_TAC
2504 THEN REWRITE_TAC[BBindex_min_v39]
2505 THEN SUBGOAL_THEN`(BBindex_v39 (restriction_cs2_v39 s i j c) ww)
2506 IN IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c))
2507 (BBprime_v39 (restriction_cs2_v39 s i j c))`ASSUME_TAC;
2509 REWRITE_TAC[IN_ELIM_THM;IMAGE]
2510 THEN EXISTS_TAC`ww:num->real^3`
2511 THEN ASM_REWRITE_TAC[IN];
2514 THEN REWRITE_TAC[IN]
2516 THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`IMAGE (BBindex_v39 (restriction_cs2_v39 s i j c)) (BBprime_v39 (restriction_cs2_v39 s i j c))`;`BBindex_v39 (restriction_cs2_v39 s i j c) ww`]
2517 THEN POP_ASSUM MP_TAC
2523 let MM_IS_NOT_2EMPTY_SUBDIVISION_C_EQ_AM=prove_by_refinement(
2525 is_scs_v39 s /\ 3< scs_k_v39 s /\
2526 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
2527 MMs_v39 s ww /\ dist(ww i,ww j) = c /\ scs_am_v39 s i j = c /\
2528 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
2530 ww IN MMs_v39 (restriction_cs2_v39 s i j c)`,
2533 THEN MP_TAC BBPRIME2_IS_NOT_2EMPTY_SUBDIVISION_C_EQ_AM
2536 THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39]
2537 THEN REPEAT RESA_TAC
2538 THEN REWRITE_TAC[override;REAL_ARITH`~(c<c)`]
2539 THEN ABBREV_TAC`k=scs_k_v39 s`
2540 THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
2542 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
2548 let UAGHHBM=prove_by_refinement(
2550 is_scs_v39 s /\ ~(i MOD scs_k_v39 s=j MOD scs_k_v39 s)/\
2551 ~(scs_J_v39 s i j) /\
2552 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j/\
2553 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (&2 < scs_a_v39 s i j \/ &2 * h0 < scs_b_v39 s i j))
2554 /\ 3< scs_k_v39 s /\
2555 ((j MOD scs_k_v39 s = SUC i MOD scs_k_v39 s) \/ (SUC j MOD scs_k_v39 s = i MOD scs_k_v39 s) ==> (~(c = scs_am_v39 s i j)))
2557 scs_arrow_v39 {s} (set_of_list (subdiv_v39 s i j c))`,
2560 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;subdiv_v39;PAIR_EQ;LET_DEF;LET_END_DEF;]
2561 THEN ABBREV_TAC`k=scs_k_v39 s`
2562 THEN REPEAT RESA_TAC
2568 THEN REMOVE_ASSUM_TAC
2569 THEN REMOVE_ASSUM_TAC
2570 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;]
2571 THEN MP_TAC(SET_RULE`c <= scs_a_v39 s i j \/ ~(c <= scs_a_v39 s i j)`)
2575 ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1]
2580 MP_TAC(SET_RULE`c <= scs_am_v39 s i j \/ ~(c <= scs_am_v39 s i j)`)
2584 ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;restriction_cs2_v39;LET_DEF;LET_END_DEF;]
2587 THEN REWRITE_TAC[is_scs_v39;scs_v39_explicit;override]
2590 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
2592 THEN REPEAT RESA_TAC;
2597 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
2599 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
2603 MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
2608 THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
2611 THEN REWRITE_TAC[periodic2]
2612 THEN REPEAT DISCH_TAC
2613 THEN ASM_REWRITE_TAC[];
2617 MP_TAC(REAL_ARITH`c <= scs_am_v39 s i j==> ~(scs_am_v39 s i j < c)`)
2622 MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
2627 MP_TAC(REAL_ARITH`c <= scs_am_v39 s i j==> ~(scs_am_v39 s i j < c)`)
2632 MP_TAC(REAL_ARITH`c <= scs_am_v39 s i j==> ~(scs_am_v39 s i j < c)`)
2634 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
2639 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
2641 THEN REWRITE_TAC[periodic2]
2642 THEN REPEAT STRIP_TAC
2643 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2644 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2645 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2646 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2647 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
2648 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
2649 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2650 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
2651 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);
2656 MP_TAC(REAL_ARITH`c <= scs_am_v39 s i j==> ~(scs_am_v39 s i j < c)`)
2662 MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',i'))`)
2666 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`i':num`;`j:num`;`i':num`;`k:num`]
2667 THEN POP_ASSUM(fun th-> MP_TAC (SYM th))
2668 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);
2672 MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
2676 MP_TAC C_LE_2_IS_SCS
2677 THEN REWRITE_TAC[is_scs_v39]
2679 THEN REPEAT RESA_TAC
2685 REPLICATE_TAC (33-15)(POP_ASSUM MP_TAC)
2686 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2687 THEN MRESA_TAC th[`i':num`;`j':num`])
2692 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
2697 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
2699 THEN REWRITE_TAC[periodic2]
2700 THEN REPEAT STRIP_TAC
2701 THEN POP_ASSUM MP_TAC
2702 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2703 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2704 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2705 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2706 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
2707 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
2708 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2709 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
2715 THEN REPLICATE_TAC (31-19)(POP_ASSUM MP_TAC)
2716 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2717 THEN MRESA_TAC th[`i':num`;`j':num`])
2722 REPLICATE_TAC (30-19)(POP_ASSUM MP_TAC)
2723 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2724 THEN MRESA_TAC th[`i':num`;`j':num`])
2732 (&2 * h0 < scs_b_v39 s i' (SUC i') \/
2734 (if psort k (i,j) = psort k (i',SUC i')
2736 else scs_a_v39 s i' (SUC i')))}
2739 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
2744 MATCH_MP_TAC CARD_IMAGE_INJ_EQ
2745 THEN REWRITE_TAC[IN_ELIM_THM]
2746 THEN EXISTS_TAC`(\i:num. i)`
2751 MATCH_MP_TAC FINITE_SUBSET
2752 THEN EXISTS_TAC`0..k`
2753 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
2764 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
2770 MP_TAC(REAL_ARITH`~(c <= scs_a_v39 s i j)==> scs_a_v39 s i j < c`)
2772 THEN MP_TAC C_LT_2_IS_SCS
2773 THEN REWRITE_TAC[is_scs_v39]
2775 THEN REPEAT RESA_TAC
2785 REWRITE_TAC[EXISTS_UNIQUE]
2786 THEN EXISTS_TAC`y:num`
2787 THEN ASM_REWRITE_TAC[]
2788 THEN REPEAT RESA_TAC
2793 REWRITE_TAC[EXISTS_UNIQUE]
2794 THEN EXISTS_TAC`y:num`
2795 THEN ASM_REWRITE_TAC[]
2796 THEN POP_ASSUM MP_TAC
2797 THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (y,SUC y) \/ ~(psort k (i,j) = psort k (y,SUC y))`)
2805 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC y:num`;`j:num`;`y:num`;`k:num`]
2810 THEN MRESA_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`y:num`;`i:num`;`k:num`]
2812 THEN REPLICATE_TAC (34-26)(POP_ASSUM MP_TAC)
2813 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2821 THEN REWRITE_TAC[periodic2]
2822 THEN REPEAT DISCH_TAC
2823 THEN POP_ASSUM MP_TAC
2824 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2825 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2826 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2827 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2828 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2829 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
2830 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
2831 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2832 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
2833 THEN REPEAT RESA_TAC
2841 THEN REWRITE_TAC[periodic2]
2842 THEN REPEAT DISCH_TAC
2843 THEN POP_ASSUM MP_TAC
2844 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2845 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2846 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2847 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2848 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2849 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
2850 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
2851 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2852 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
2853 THEN REPEAT RESA_TAC
2860 THEN POP_ASSUM(fun th-> STRIP_TAC
2862 THEN MRESA_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`y:num`;`j:num`;`k:num`]
2864 THEN REPLICATE_TAC (34-26)(POP_ASSUM MP_TAC)
2865 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2873 THEN REWRITE_TAC[periodic2]
2874 THEN REPEAT DISCH_TAC
2875 THEN POP_ASSUM MP_TAC
2876 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2877 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2878 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2879 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2880 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2881 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
2882 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
2883 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2884 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
2885 THEN REPEAT RESA_TAC
2893 THEN REWRITE_TAC[periodic2]
2894 THEN REPEAT DISCH_TAC
2895 THEN POP_ASSUM MP_TAC
2896 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
2897 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
2898 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2899 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
2900 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2901 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
2902 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
2903 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
2904 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
2905 THEN REPEAT RESA_TAC
2919 (**********c < scs_bm_v39 s i j *******)
2921 MP_TAC(SET_RULE`c < scs_bm_v39 s i j \/ ~(c < scs_bm_v39 s i j)`)
2926 ASM_REWRITE_TAC[Basics.set_of_list2_explicit;SET_RULE`A IN{B,C}<=> A=B \/ A=C`]
2930 (**********restriction_cs1_v39 s i j c *******)
2935 THEN REWRITE_TAC[is_scs_v39;scs_v39_explicit;override;restriction_cs1_v39;LET_DEF;LET_END_DEF;]
2938 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
2940 THEN REPEAT RESA_TAC;
2944 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
2946 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
2950 MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
2955 THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
2958 THEN REWRITE_TAC[periodic2]
2959 THEN REPEAT DISCH_TAC
2960 THEN ASM_REWRITE_TAC[];
2966 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
2968 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
2972 MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
2977 THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
2980 THEN REWRITE_TAC[periodic2]
2981 THEN REPEAT DISCH_TAC
2982 THEN ASM_REWRITE_TAC[];
2987 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
2988 THEN MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
2993 MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
2998 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
2999 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
3003 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
3004 THEN MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j) ==> scs_am_v39 s i j<= c`)
3010 THEN REWRITE_TAC[periodic2]
3011 THEN REPEAT DISCH_TAC
3012 THEN POP_ASSUM MP_TAC
3013 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3014 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3015 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3016 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3017 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3018 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3019 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
3020 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3021 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3028 THEN REWRITE_TAC[periodic2]
3029 THEN REPEAT DISCH_TAC
3030 THEN POP_ASSUM MP_TAC
3031 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3032 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3033 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3034 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3035 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3036 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3037 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
3038 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_am_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3039 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3044 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
3045 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
3054 POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
3055 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i'))`)
3061 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC i':num`;`j:num`;`i':num`;`k:num`]
3062 THEN REPLICATE_TAC (34-16)(POP_ASSUM MP_TAC)
3063 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3064 THEN MRESA1_TAC th`i':num`)
3066 THEN REWRITE_TAC[periodic2]
3067 THEN REPEAT DISCH_TAC
3068 THEN POP_ASSUM MP_TAC
3069 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3070 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC i':num`[ARITH_RULE`4 MOD 4=0`])
3071 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3072 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3073 THEN REPLICATE_TAC (35-24)(POP_ASSUM MP_TAC)
3074 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3076 THEN POP_ASSUM MP_TAC
3077 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3078 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3079 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3080 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3081 THEN REAL_ARITH_TAC;
3086 REPLICATE_TAC (32-16)(POP_ASSUM MP_TAC)
3087 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3088 THEN MRESA1_TAC th`i':num`)
3094 MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i'))`)
3100 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC i':num`;`j:num`;`i':num`;`k:num`]
3101 THEN REPLICATE_TAC (34-17)(POP_ASSUM MP_TAC)
3102 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3103 THEN MRESA1_TAC th`i':num`)
3105 THEN REWRITE_TAC[periodic2]
3106 THEN REPEAT DISCH_TAC
3107 THEN POP_ASSUM MP_TAC
3108 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3109 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC i':num`[ARITH_RULE`4 MOD 4=0`])
3110 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3111 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3112 THEN REPLICATE_TAC (35-24)(POP_ASSUM MP_TAC)
3113 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3115 THEN POP_ASSUM MP_TAC
3116 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3117 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3118 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3119 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3120 THEN REAL_ARITH_TAC;
3123 REPLICATE_TAC (32-17)(POP_ASSUM MP_TAC)
3124 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3125 THEN MRESA1_TAC th`i':num`)
3131 REPLICATE_TAC (31-19)(POP_ASSUM MP_TAC)
3132 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3133 THEN MRESA_TAC th[`i':num`;`j':num`])
3138 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
3144 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
3146 THEN REWRITE_TAC[periodic2]
3147 THEN REPEAT DISCH_TAC
3148 THEN POP_ASSUM MP_TAC
3149 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3150 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3151 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3152 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3153 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3154 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
3155 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3156 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3162 REPLICATE_TAC (31-19)(POP_ASSUM MP_TAC)
3163 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3164 THEN MRESA_TAC th[`i':num`;`j':num`])
3173 (if psort k (i,j) = psort k (i',SUC i')
3175 else scs_b_v39 s i' (SUC i')) \/
3176 &2 < scs_a_v39 s i' (SUC i'))}
3180 (scs_b_v39 s i' (SUC i')) \/
3181 &2 < scs_a_v39 s i' (SUC i'))}`ASSUME_TAC
3188 MATCH_MP_TAC CARD_SUBSET
3189 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
3199 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (x,SUC x) \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (x,SUC x))`)
3205 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
3206 THEN REPLICATE_TAC (34-25)(POP_ASSUM MP_TAC)
3207 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3210 THEN REWRITE_TAC[periodic2]
3211 THEN REPEAT DISCH_TAC
3212 THEN POP_ASSUM MP_TAC
3213 THEN POP_ASSUM MP_TAC
3214 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3215 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3216 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3217 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3218 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
3219 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
3220 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3221 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`])
3222 THEN REAL_ARITH_TAC;
3229 MATCH_MP_TAC FINITE_SUBSET
3230 THEN EXISTS_TAC`0..k`
3231 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
3236 REPLICATE_TAC (31-20)(POP_ASSUM MP_TAC)
3237 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3239 THEN POP_ASSUM MP_TAC
3245 (**********restriction_cs2_v39 s i j c *******)
3249 THEN REWRITE_TAC[is_scs_v39;scs_v39_explicit;override;restriction_cs2_v39;LET_DEF;LET_END_DEF;]
3252 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
3254 THEN REPEAT RESA_TAC;
3259 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
3261 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
3265 MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
3270 THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
3273 THEN REWRITE_TAC[periodic2]
3274 THEN REPEAT DISCH_TAC
3275 THEN ASM_REWRITE_TAC[];
3282 MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j)==> (scs_am_v39 s i j < c)`)
3290 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
3292 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
3296 MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
3301 THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
3304 THEN REWRITE_TAC[periodic2]
3305 THEN REPEAT DISCH_TAC
3306 THEN ASM_REWRITE_TAC[];
3311 MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
3316 MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j)==> (scs_am_v39 s i j < c)`)
3322 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
3323 THEN MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
3328 MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j)==> (scs_am_v39 s i j < c)`)
3330 THEN REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
3331 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
3340 MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j)==> (scs_am_v39 s i j < c)`)
3342 THEN REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
3343 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
3350 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
3352 THEN REWRITE_TAC[periodic2]
3353 THEN REPEAT STRIP_TAC
3354 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3355 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3356 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3357 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3358 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3359 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
3360 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3361 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3362 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
3363 THEN MP_TAC(REAL_ARITH`c < scs_bm_v39 s i j ==> c <= scs_bm_v39 s i j`)
3370 MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',i'))`)
3374 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`i':num`;`j:num`;`i':num`;`k:num`]
3375 THEN POP_ASSUM(fun th-> MP_TAC (SYM th))
3376 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);
3380 MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
3384 MP_TAC C_LE_2_IS_SCS
3385 THEN REWRITE_TAC[is_scs_v39]
3387 THEN REPEAT RESA_TAC
3393 REPLICATE_TAC (34-15)(POP_ASSUM MP_TAC)
3394 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
3395 THEN MRESA_TAC th[`i':num`;`j':num`])
3400 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
3405 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
3407 THEN REWRITE_TAC[periodic2]
3408 THEN REPEAT STRIP_TAC
3409 THEN POP_ASSUM MP_TAC
3410 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3411 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3412 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3413 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3414 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3415 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
3416 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3417 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3423 THEN REPLICATE_TAC (32-19)(POP_ASSUM MP_TAC)
3424 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
3425 THEN MRESA_TAC th[`i':num`;`j':num`])
3430 REPLICATE_TAC (31-19)(POP_ASSUM MP_TAC)
3431 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
3432 THEN MRESA_TAC th[`i':num`;`j':num`])
3440 (&2 * h0 < scs_b_v39 s i' (SUC i') \/
3442 (if psort k (i,j) = psort k (i',SUC i')
3444 else scs_a_v39 s i' (SUC i')))}
3447 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
3452 MATCH_MP_TAC CARD_IMAGE_INJ_EQ
3453 THEN REWRITE_TAC[IN_ELIM_THM]
3454 THEN EXISTS_TAC`(\i:num. i)`
3459 MATCH_MP_TAC FINITE_SUBSET
3460 THEN EXISTS_TAC`0..k`
3461 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
3472 MP_TAC(SET_RULE`psort k (i,j) = psort k (x,SUC x) \/ ~(psort k (i,j) = psort k (x,SUC x))`)
3478 MP_TAC(REAL_ARITH`~(c <= scs_a_v39 s i j)==> scs_a_v39 s i j < c`)
3480 THEN MP_TAC C_LT_2_IS_SCS
3481 THEN REWRITE_TAC[is_scs_v39]
3483 THEN REPEAT RESA_TAC
3493 REWRITE_TAC[EXISTS_UNIQUE]
3494 THEN EXISTS_TAC`y:num`
3495 THEN ASM_REWRITE_TAC[]
3496 THEN REPEAT RESA_TAC
3501 REWRITE_TAC[EXISTS_UNIQUE]
3502 THEN EXISTS_TAC`y:num`
3503 THEN ASM_REWRITE_TAC[]
3504 THEN POP_ASSUM MP_TAC
3505 THEN MP_TAC(SET_RULE`psort k (i,j) = psort k (y,SUC y) \/ ~(psort k (i,j) = psort k (y,SUC y))`)
3513 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC y:num`;`j:num`;`y:num`;`k:num`]
3518 THEN MRESA_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`y:num`;`i:num`;`k:num`]
3520 THEN REPLICATE_TAC (35-26)(POP_ASSUM MP_TAC)
3521 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3529 THEN REWRITE_TAC[periodic2]
3530 THEN REPEAT DISCH_TAC
3531 THEN POP_ASSUM MP_TAC
3532 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3533 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3534 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3535 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3536 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3537 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
3538 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
3539 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3540 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
3541 THEN REPEAT RESA_TAC
3549 THEN REWRITE_TAC[periodic2]
3550 THEN REPEAT DISCH_TAC
3551 THEN POP_ASSUM MP_TAC
3552 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3553 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3554 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3555 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3556 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3557 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
3558 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
3559 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3560 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
3561 THEN REPEAT RESA_TAC
3568 THEN POP_ASSUM(fun th-> STRIP_TAC
3570 THEN MRESA_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`y:num`;`j:num`;`k:num`]
3572 THEN REPLICATE_TAC (35-26)(POP_ASSUM MP_TAC)
3573 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3581 THEN REWRITE_TAC[periodic2]
3582 THEN REPEAT DISCH_TAC
3583 THEN POP_ASSUM MP_TAC
3584 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3585 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3586 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3587 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3588 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3589 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
3590 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
3591 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (SUC j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3592 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
3593 THEN REPEAT RESA_TAC
3601 THEN REWRITE_TAC[periodic2]
3602 THEN REPEAT DISCH_TAC
3603 THEN POP_ASSUM MP_TAC
3604 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3605 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3606 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (y MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3607 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3608 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3609 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s y`][ARITH_RULE`~(4=0)`;periodic]
3610 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC y:num`[ARITH_RULE`4 MOD 4=0`])
3611 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3612 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y:num`[ARITH_RULE`4 MOD 4=0`])
3613 THEN REPEAT RESA_TAC
3627 (**********restriction_cs1_v39 s i j c *******)
3629 MP_TAC(SET_RULE`c < scs_b_v39 s i j \/ ~(c < scs_b_v39 s i j)`)
3634 ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;restriction_cs1_v39;LET_DEF;LET_END_DEF;]
3637 THEN REWRITE_TAC[is_scs_v39;scs_v39_explicit;override]
3640 THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
3642 THEN REPEAT RESA_TAC;
3646 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
3648 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i' + scs_k_v39 s,j'))`)
3652 MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
3657 THEN MRESA_TAC (GEN_ALL PERIODIC_PSORT)[`k:num`;`i':num`;`j':num`]
3660 THEN REWRITE_TAC[periodic2]
3661 THEN REPEAT DISCH_TAC
3662 THEN ASM_REWRITE_TAC[];
3670 MRESA_TAC Terminal.psort_sym[`k:num`;`i':num`;`j':num`]
3677 REWRITE_TAC[override;periodic2;LET_DEF;LET_END_DEF;]
3678 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
3682 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
3683 THEN MP_TAC(REAL_ARITH`~(c < scs_bm_v39 s i j) ==> scs_bm_v39 s i j<= c`)
3689 THEN REWRITE_TAC[periodic2]
3690 THEN REPEAT DISCH_TAC
3691 THEN POP_ASSUM MP_TAC
3692 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3693 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3694 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3695 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3696 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3697 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3698 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
3699 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3700 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3707 THEN REWRITE_TAC[periodic2]
3708 THEN REPEAT DISCH_TAC
3709 THEN POP_ASSUM MP_TAC
3710 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3711 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3712 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3713 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3714 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3715 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3716 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
3717 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_bm_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3718 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3724 POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
3725 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i'))`)
3731 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC i':num`;`j:num`;`i':num`;`k:num`]
3732 THEN REPLICATE_TAC (35-16)(POP_ASSUM MP_TAC)
3733 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3734 THEN MRESA1_TAC th`i':num`)
3736 THEN REWRITE_TAC[periodic2]
3737 THEN REPEAT DISCH_TAC
3738 THEN POP_ASSUM MP_TAC
3739 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3740 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC i':num`[ARITH_RULE`4 MOD 4=0`])
3741 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3742 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3743 THEN REPLICATE_TAC (36-24)(POP_ASSUM MP_TAC)
3744 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3746 THEN POP_ASSUM MP_TAC
3747 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3748 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3749 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3750 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3751 THEN REAL_ARITH_TAC;
3756 REPLICATE_TAC (33-16)(POP_ASSUM MP_TAC)
3757 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3758 THEN MRESA1_TAC th`i':num`)
3764 MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',SUC i'))`)
3770 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC i':num`;`j:num`;`i':num`;`k:num`]
3771 THEN REPLICATE_TAC (35-17)(POP_ASSUM MP_TAC)
3772 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3773 THEN MRESA1_TAC th`i':num`)
3775 THEN REWRITE_TAC[periodic2]
3776 THEN REPEAT DISCH_TAC
3777 THEN POP_ASSUM MP_TAC
3778 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3779 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC i':num`[ARITH_RULE`4 MOD 4=0`])
3780 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC i' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3781 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3782 THEN REPLICATE_TAC (36-24)(POP_ASSUM MP_TAC)
3783 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3785 THEN POP_ASSUM MP_TAC
3786 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3787 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3788 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3789 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3790 THEN REAL_ARITH_TAC;
3793 REPLICATE_TAC (33-17)(POP_ASSUM MP_TAC)
3794 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3795 THEN MRESA1_TAC th`i':num`)
3801 REPLICATE_TAC (32-19)(POP_ASSUM MP_TAC)
3802 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3803 THEN MRESA_TAC th[`i':num`;`j':num`])
3808 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j') \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
3814 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`j':num`;`j:num`;`i':num`;`k:num`]
3816 THEN REWRITE_TAC[periodic2]
3817 THEN REPEAT DISCH_TAC
3818 THEN POP_ASSUM MP_TAC
3819 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3820 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3821 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3822 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3823 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(4=0)`;periodic]
3824 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j':num`[ARITH_RULE`4 MOD 4=0`])
3825 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3826 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i':num`[ARITH_RULE`4 MOD 4=0`])
3832 REPLICATE_TAC (32-19)(POP_ASSUM MP_TAC)
3833 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3834 THEN MRESA_TAC th[`i':num`;`j':num`])
3843 (if psort k (i,j) = psort k (i',SUC i')
3845 else scs_b_v39 s i' (SUC i')) \/
3846 &2 < scs_a_v39 s i' (SUC i'))}
3850 (scs_b_v39 s i' (SUC i')) \/
3851 &2 < scs_a_v39 s i' (SUC i'))}`ASSUME_TAC
3858 MATCH_MP_TAC CARD_SUBSET
3859 THEN REWRITE_TAC[IN_ELIM_THM;SUBSET]
3869 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (x,SUC x) \/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (x,SUC x))`)
3875 MRESA_TAC(GEN_ALL CASE_PSORT)[`i:num`;`SUC x:num`;`j:num`;`x:num`;`k:num`]
3876 THEN REPLICATE_TAC (35-25)(POP_ASSUM MP_TAC)
3877 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3880 THEN REWRITE_TAC[periodic2]
3881 THEN REPEAT DISCH_TAC
3882 THEN POP_ASSUM MP_TAC
3883 THEN POP_ASSUM MP_TAC
3884 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
3885 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
3886 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3887 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
3888 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s x`][ARITH_RULE`~(4=0)`;periodic]
3889 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
3890 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (SUC x MOD k)`][ARITH_RULE`~(4=0)`;periodic]
3891 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num`[ARITH_RULE`4 MOD 4=0`])
3892 THEN REAL_ARITH_TAC;
3899 MATCH_MP_TAC FINITE_SUBSET
3900 THEN EXISTS_TAC`0..k`
3901 THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
3906 REPLICATE_TAC (32-20)(POP_ASSUM MP_TAC)
3907 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3909 THEN POP_ASSUM MP_TAC
3915 ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;restriction_cs1_v39;LET_DEF;LET_END_DEF;]
3921 DISJ_CASES_TAC(SET_RULE`(!s'. s' = s ==> MMs_v39 s' = {}) \/ ~((!s'. s' = s ==> MMs_v39 s' = {}))`);
3930 THEN POP_ASSUM MP_TAC
3931 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
3932 THEN REPEAT STRIP_TAC
3933 THEN POP_ASSUM MP_TAC
3935 THEN POP_ASSUM MP_TAC
3936 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[SET_RULE`~(A={})<=> ?ww. A ww`;]
3938 THEN MP_TAC(SET_RULE`c <= scs_a_v39 s i j \/ ~(c <= scs_a_v39 s i j)`)
3943 ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1]
3944 THEN EXISTS_TAC`s:scs_v39`
3945 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;IN]
3946 THEN EXISTS_TAC`ww:num->real^3`
3947 THEN ASM_REWRITE_TAC[];
3951 MP_TAC(SET_RULE`c <= scs_am_v39 s i j \/ ~(c <= scs_am_v39 s i j)`)
3955 SUBGOAL_THEN`c<= norm(ww i- (ww:num->real^3) j)` ASSUME_TAC;
3961 THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39;BBprime2_v39;BBprime_v39; BBs_v39;]
3962 THEN REPEAT RESA_TAC
3963 THEN REPLICATE_TAC (22-19)(POP_ASSUM MP_TAC)
3964 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3965 THEN MRESAL_TAC th[`i:num`;`j:num`][dist])
3966 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
3974 MP_TAC(REAL_ARITH`c <= norm ((ww:num->real^3) i - ww j)==> c = norm (ww i - ww j)\/ c < norm (ww i - ww j)`)
3979 SUBGOAL_THEN`c=scs_am_v39 s i j` ASSUME_TAC
3986 THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39;BBprime2_v39;BBprime_v39; BBs_v39;]
3987 THEN REPEAT RESA_TAC
3988 THEN REPLICATE_TAC (25-20)(POP_ASSUM MP_TAC)
3989 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
3990 THEN MRESAL_TAC th[`i:num`;`j:num`][dist])
3991 THEN REPLICATE_TAC (1)(POP_ASSUM MP_TAC)
3992 THEN POP_ASSUM(fun th-> REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
3993 THEN REWRITE_TAC[th])
3994 THEN REAL_ARITH_TAC;
3999 REPLICATE_TAC (15-8)(POP_ASSUM MP_TAC)
4000 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
4003 THEN POP_ASSUM MP_TAC
4004 THEN POP_ASSUM(fun th-> MP_TAC th)
4007 THEN MP_TAC MM_IS_NOT_2EMPTY_SUBDIVISION_C_EQ_AM
4009 THEN POP_ASSUM MP_TAC
4010 THEN REWRITE_TAC[dist;]
4012 THEN ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;LET_DEF;LET_END_DEF;]
4013 THEN EXISTS_TAC`restriction_cs2_v39 s i j c`
4014 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;]
4015 THEN EXISTS_TAC`ww:num->real^3`
4016 THEN ASM_REWRITE_TAC[]
4017 THEN POP_ASSUM MATCH_MP_TAC
4018 THEN ASM_REWRITE_TAC[];
4025 ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;LET_DEF;LET_END_DEF;]
4026 THEN EXISTS_TAC`restriction_cs2_v39 s i j c`
4027 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;]
4028 THEN EXISTS_TAC`ww:num->real^3`
4029 THEN ASM_REWRITE_TAC[]
4030 THEN MP_TAC MM_IS_NOT_1EMPTY_SUBDIVISION
4038 MP_TAC(REAL_ARITH`~(c <= scs_am_v39 s i j)==> scs_am_v39 s i j<c`)
4040 THEN MP_TAC(REAL_ARITH`c < scs_bm_v39 s i j \/ scs_bm_v39 s i j <=c`)
4047 ASM_REWRITE_TAC[Basics.set_of_list2_explicit;SET_RULE`A IN{B,C}<=> A=B \/ A=C`]
4048 THEN MP_TAC(ARITH_RULE` c< norm(ww i- (ww:num->real^3) j) \/ norm(ww i- (ww:num->real^3) j)<=c` )
4056 EXISTS_TAC`restriction_cs2_v39 s i j c`
4057 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;]
4058 THEN EXISTS_TAC`ww:num->real^3`
4059 THEN ASM_REWRITE_TAC[]
4060 THEN MP_TAC MM_IS_NOT_2EMPTY_SUBDIVISION
4065 EXISTS_TAC`restriction_cs1_v39 s i j c`
4066 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;]
4067 THEN EXISTS_TAC`ww:num->real^3`
4068 THEN ASM_REWRITE_TAC[]
4069 THEN MP_TAC MM_IS_NOT_2EMPTY_SUBDIVISION1
4070 THEN ASM_REWRITE_TAC[dist]
4076 MP_TAC(REAL_ARITH`scs_bm_v39 s i j <= c ==> ~(c<scs_bm_v39 s i j)`)
4078 THEN MP_TAC(REAL_ARITH`c < scs_b_v39 s i j \/ scs_b_v39 s i j<= c`)
4084 MP_TAC(ARITH_RULE` c< norm(ww i- (ww:num->real^3) j) \/ norm(ww i- (ww:num->real^3) j)<=c` )
4092 THEN REWRITE_TAC[IN;MMs_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs2_v39;BBprime2_v39;BBprime_v39; BBs_v39;]
4093 THEN REPEAT RESA_TAC
4094 THEN REPLICATE_TAC (28-21)(POP_ASSUM MP_TAC)
4095 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
4096 THEN MRESAL_TAC th[`i:num`;`j:num`][dist])
4097 THEN REPLICATE_TAC (28-23)(POP_ASSUM MP_TAC)
4098 THEN REAL_ARITH_TAC;
4108 MP_TAC MM_IS_NOT_1EMPTY_SUBDIVISION1
4110 THEN POP_ASSUM MP_TAC
4111 THEN ASM_REWRITE_TAC[dist]
4113 THEN EXISTS_TAC`restriction_cs1_v39 s i j c`
4114 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. ww IN A`;]
4115 THEN ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;LET_DEF;LET_END_DEF;]
4116 THEN EXISTS_TAC`ww:num->real^3`
4117 THEN ASM_REWRITE_TAC[]
4122 MP_TAC(REAL_ARITH`scs_b_v39 s i j <= c==> ~(c< scs_b_v39 s i j )`)
4124 THEN ASM_REWRITE_TAC[IN_SET_OF_LIST;set_of_list;Seq.mem_seq1;LET_DEF;LET_END_DEF;]
4125 THEN EXISTS_TAC`s:scs_v39`
4126 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?ww. A ww`;]
4127 THEN EXISTS_TAC`ww:num->real^3`
4128 THEN ASM_REWRITE_TAC[]
4147 let check_completeness_claimA_concl =
4148 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)