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 Otmtotj = struct
27 open Wrgcvdr_cizmrrh;;
35 open Flyspeck_constants;;
51 open Wrgcvdr_cizmrrh;;
53 open Flyspeck_constants;;
92 let SCSE_TAC= ASM_REWRITE_TAC[scs_basic;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} j <=> {} i`;periodic2;scs_basic;unadorned_v39;scs_prop_equ_v39;LET_DEF;LET_END_DEF;scs_stab_diag_v39;scs_half_slice_v39;
93 Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_5_TAC;
94 scs_5M1;scs_3M1;scs_6I1;scs_3T1;scs_4M2;scs_6M1;scs_6T1;scs_5I1;scs_5I2;scs_5I3;scs_5M2;
95 Terminal.FUNLIST_EXPLICIT;Yrtafyh.PSORT_PERIODIC;PSORT_5_EXPLICIT;
96 ARITH_RULE`SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6/\ SUC 6=7/\ SUC 7=8`];;
100 let DIAG_5_EQU_PSORT=prove(`~(i MOD 5 = j MOD 5) /\
101 ~(SUC i MOD 5 = j MOD 5) /\
102 ~(i MOD 5 = SUC j MOD 5)
103 <=> psort 5 (i,j) = 0,2\/ psort 5 (i,j) = 0,3\/ psort 5 (i,j) = 1,3
104 \/ psort 5 (i,j) = 1,4\/ psort 5 (i,j) = 2,4`,
105 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
107 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
109 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
111 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
112 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
114 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
115 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
118 THEN REWRITE_TAC[PSORT_5_EXPLICIT;PAIR_EQ]
123 let BB_5I1_IS_BB_5M2=prove_by_refinement(`BBs_v39 scs_5I1 v/\ (!i j. scs_diag 5 i j ==> cstab <= dist(v i,v j)) ==> BBs_v39 scs_5M2 v`,
125 REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I1;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`]
128 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
131 THAYTHE_TAC (5-2)[`i`;`j`];
133 MP_TAC(SET_RULE`SUC i MOD 5= j MOD 5\/ ~(SUC i MOD 5= j MOD 5)`)
136 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
137 THEN THAYTHE_TAC (7-2)[`i`;`j`]
144 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
146 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
147 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
152 MP_TAC(SET_RULE`i MOD 5= SUC j MOD 5\/ ~(i MOD 5= SUC j MOD 5)`)
155 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
156 THEN THAYTHE_TAC (8-2)[`i`;`j`]
160 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
162 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
163 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
167 MP_TAC DIAG_5_EQU_PSORT
169 THEN REWRITE_TAC[PAIR_EQ]
173 THAYTHE_TAC (5-2)[`i`;`j`];
175 MP_TAC(SET_RULE`SUC i MOD 5= j MOD 5\/ ~(SUC i MOD 5= j MOD 5)`)
178 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
179 THEN THAYTHE_TAC (7-2)[`i`;`j`]
186 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
188 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
189 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
193 THEN REWRITE_TAC[h0;cstab]
196 MP_TAC(SET_RULE`i MOD 5= SUC j MOD 5\/ ~(i MOD 5= SUC j MOD 5)`)
199 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
200 THEN THAYTHE_TAC (8-2)[`i`;`j`]
204 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
206 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
207 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
211 THEN REWRITE_TAC[h0;cstab]
214 MP_TAC DIAG_5_EQU_PSORT
216 THEN REWRITE_TAC[PAIR_EQ]
218 THEN THAYTHE_TAC(8-2)[`i`;`j`]]);;
221 let MM_5I1_IMP_MM_5M2=prove(`MMs_v39 scs_5I1 v/\ (!i j. scs_diag 5 i j ==> cstab <= dist(v i,v j)) ==> ~(MMs_v39 scs_5M2 ={})`,
223 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
224 THEN EXISTS_TAC`v:num->real^3`
225 THEN EXISTS_TAC`scs_5I1`
226 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I1`;`v`]
227 THEN ASSUME_TAC SCS_5I1_BASIC
228 THEN ASSUME_TAC K_SCS_5I1
229 THEN ASSUME_TAC SCS_5M2_BASIC
230 THEN ASSUME_TAC K_SCS_5M2
231 THEN ASSUME_TAC SCS_5M2_IS_SCS
232 THEN ASM_SIMP_TAC[BB_5I1_IS_BB_5M2;IN;SCS_5I1_IS_SCS]
234 THEN REAL_ARITH_TAC);;
237 let BB_5I2_IS_BB_5M2=prove_by_refinement(`BBs_v39 scs_5I2 v/\ (!i j. scs_diag 5 i j ==> cstab <= dist(v i,v j)) ==> BBs_v39 scs_5M2 v`,
239 REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I2;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`]
242 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
245 THAYTHE_TAC (5-2)[`i`;`j`];
247 MP_TAC(SET_RULE`SUC i MOD 5= j MOD 5\/ ~(SUC i MOD 5= j MOD 5)`)
250 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
251 THEN THAYTHE_TAC (7-2)[`i`;`j`]
258 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
260 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
261 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
266 MP_TAC(SET_RULE`i MOD 5= SUC j MOD 5\/ ~(i MOD 5= SUC j MOD 5)`)
269 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
270 THEN THAYTHE_TAC (8-2)[`i`;`j`]
274 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
276 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
277 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
281 MP_TAC DIAG_5_EQU_PSORT
283 THEN REWRITE_TAC[PAIR_EQ]
287 THAYTHE_TAC (5-2)[`i`;`j`];
289 MP_TAC(SET_RULE`SUC i MOD 5= j MOD 5\/ ~(SUC i MOD 5= j MOD 5)`)
292 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
293 THEN THAYTHE_TAC (7-2)[`i`;`j`]
300 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
302 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
303 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
307 THEN REWRITE_TAC[h0;cstab]
310 MP_TAC(SET_RULE`i MOD 5= SUC j MOD 5\/ ~(i MOD 5= SUC j MOD 5)`)
313 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
314 THEN THAYTHE_TAC (8-2)[`i`;`j`]
318 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
320 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
321 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
325 THEN REWRITE_TAC[h0;cstab]
328 MP_TAC DIAG_5_EQU_PSORT
330 THEN REWRITE_TAC[PAIR_EQ]
332 THEN THAYTHE_TAC(8-2)[`i`;`j`]]);;
335 let MM_5I2_IMP_MM_5M2=prove(`MMs_v39 scs_5I2 v/\ (!i j. scs_diag 5 i j ==> cstab <= dist(v i,v j)) ==> ~(MMs_v39 scs_5M2 ={})`,
337 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
338 THEN EXISTS_TAC`v:num->real^3`
339 THEN EXISTS_TAC`scs_5I2`
340 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I2`;`v`]
341 THEN ASSUME_TAC SCS_5I2_BASIC
342 THEN ASSUME_TAC K_SCS_5I2
343 THEN ASSUME_TAC SCS_5M2_BASIC
344 THEN ASSUME_TAC K_SCS_5M2
345 THEN ASSUME_TAC SCS_5M2_IS_SCS
346 THEN ASM_SIMP_TAC[BB_5I2_IS_BB_5M2;IN;SCS_5I2_IS_SCS]
348 THEN REAL_ARITH_TAC);;
352 let BB_5I3_IS_BB_5M2=prove_by_refinement(`BBs_v39 scs_5I3 v/\ (!i j. scs_diag 5 i j ==> cstab <= dist(v i,v j)) ==> BBs_v39 scs_5M2 v`,
354 REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`]
358 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
361 THAYTHE_TAC (5-2)[`i`;`j`];
363 MP_TAC(SET_RULE`SUC i MOD 5= j MOD 5\/ ~(SUC i MOD 5= j MOD 5)`)
366 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
367 THEN THAYTHE_TAC (7-2)[`i`;`j`]
375 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
377 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
378 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
381 THEN REWRITE_TAC[h0;cstab]
384 MP_TAC(SET_RULE`i MOD 5= SUC j MOD 5\/ ~(i MOD 5= SUC j MOD 5)`)
387 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
388 THEN THAYTHE_TAC (8-2)[`i`;`j`]
393 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
395 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
396 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
399 THEN REWRITE_TAC[h0;cstab]
402 MP_TAC DIAG_5_EQU_PSORT
404 THEN REWRITE_TAC[PAIR_EQ]
407 THAYTHE_TAC (5-2)[`i`;`j`];
409 MP_TAC(SET_RULE`SUC i MOD 5= j MOD 5\/ ~(SUC i MOD 5= j MOD 5)`)
412 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
413 THEN THAYTHE_TAC (7-2)[`i`;`j`]
421 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
423 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
424 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
427 THEN REWRITE_TAC[h0;cstab]
428 THEN MP_TAC sqrt8_LE_CSTAB
431 MP_TAC(SET_RULE`i MOD 5= SUC j MOD 5\/ ~(i MOD 5= SUC j MOD 5)`)
434 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
435 THEN THAYTHE_TAC (8-2)[`i`;`j`]
440 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
442 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
443 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
446 THEN REWRITE_TAC[h0;cstab]
447 THEN MP_TAC sqrt8_LE_CSTAB
450 MP_TAC DIAG_5_EQU_PSORT
452 THEN REWRITE_TAC[PAIR_EQ]
454 THEN THAYTHE_TAC(8-2)[`i`;`j`]
456 THEN REWRITE_TAC[PAIR_EQ]
460 let MM_5I3_IMP_MM_5M2=prove(`MMs_v39 scs_5I3 v/\ (!i j. scs_diag 5 i j ==> cstab <= dist(v i,v j)) ==> ~(MMs_v39 scs_5M2 ={})`,
462 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
463 THEN EXISTS_TAC`v:num->real^3`
464 THEN EXISTS_TAC`scs_5I3`
465 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I3`;`v`]
466 THEN ASSUME_TAC SCS_5I3_BASIC
467 THEN ASSUME_TAC K_SCS_5I3
468 THEN ASSUME_TAC SCS_5M2_BASIC
469 THEN ASSUME_TAC K_SCS_5M2
470 THEN ASSUME_TAC SCS_5M2_IS_SCS
471 THEN ASM_SIMP_TAC[BB_5I3_IS_BB_5M2;IN;SCS_5I3_IS_SCS]
473 THEN REAL_ARITH_TAC);;
476 let BB_5M1_IS_BB_5M2=prove_by_refinement(`BBs_v39 scs_5M1 v/\ (!i j. scs_diag 5 i j ==> cstab <= dist(v i,v j)) ==> BBs_v39 scs_5M2 v`,
478 REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5M1;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`]
482 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
485 THAYTHE_TAC (5-2)[`i`;`j`];
487 MP_TAC(SET_RULE`SUC i MOD 5= j MOD 5\/ ~(SUC i MOD 5= j MOD 5)`)
490 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
491 THEN THAYTHE_TAC (7-2)[`i`;`j`]
499 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
501 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5=0\/ i MOD 5=1\/ i MOD 5=2\/ i MOD 5=3\/i MOD 5=4`)
502 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
505 THEN REWRITE_TAC[h0;cstab]
508 MP_TAC(SET_RULE`i MOD 5= SUC j MOD 5\/ ~(i MOD 5= SUC j MOD 5)`)
511 MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i`;`j`][ARITH_RULE`~(5=0)`]
512 THEN THAYTHE_TAC (8-2)[`i`;`j`]
517 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j`;`5`][ARITH_RULE`1<5`]
519 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5=0\/ j MOD 5=1\/ j MOD 5=2\/ j MOD 5=3\/j MOD 5=4`)
520 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
523 THEN REWRITE_TAC[h0;cstab]
526 MP_TAC DIAG_5_EQU_PSORT
528 THEN REWRITE_TAC[PAIR_EQ]
533 let MM_5M1_IMP_MM_5M2=prove(`MMs_v39 scs_5M1 v/\ (!i j. scs_diag 5 i j ==> cstab <= dist(v i,v j)) ==> ~(MMs_v39 scs_5M2 ={})`,
535 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
536 THEN EXISTS_TAC`v:num->real^3`
537 THEN EXISTS_TAC`scs_5M1`
538 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M1`;`v`]
539 THEN ASSUME_TAC SCS_5M1_BASIC
540 THEN ASSUME_TAC K_SCS_5M1
541 THEN ASSUME_TAC SCS_5M2_BASIC
542 THEN ASSUME_TAC K_SCS_5M2
543 THEN ASSUME_TAC SCS_5M2_IS_SCS
544 THEN ASM_SIMP_TAC[BB_5M1_IS_BB_5M2;IN;SCS_5M1_IS_SCS]
546 THEN REAL_ARITH_TAC);;
548 (***********DIST<= cstab*************)
551 let SCS_5I1_STAB_DIAG= prove(
553 v IN MMs_v39 scs_5I1 /\
555 dist(v i,v j) <= cstab ==>
556 v IN MMs_v39 (scs_stab_diag_v39 scs_5I1 i j)`,
558 THEN REPEAT STRIP_TAC
559 THEN MP_TAC SCS_5I1_IS_SCS
561 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I1`;`v`]
562 THEN MRESA_TAC DIST_LE_IMP_A_LE[`v`;`scs_5I1`;`i`;`j`;`cstab`]
563 THEN ASSUME_TAC SCS_5I1_BASIC
564 THEN ASSUME_TAC K_SCS_5I1
565 THEN MRESAL_TAC Yrtafyh.YRTAFYH[`scs_5I1`;`i`;`j`][ARITH_RULE`3<5`;]
566 THEN MP_TAC Ppbtydq.MXQTIED
569 THEN MATCH_DICH_TAC 0
570 THEN EXISTS_TAC`scs_5I1`
571 THEN ASM_SIMP_TAC[STAB_BB;SCS_K_D_A_STAB_EQ;DIAG_SCS_M_EQ;REAL_ARITH`a<=a`]
573 THEN REWRITE_TAC[scs_stab_diag_v39;scs_5I1;scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;CS_ADJ]
575 THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
578 MRESAL_TAC DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
580 THEN REWRITE_TAC[scs_diag;cstab;h0]
585 let SCS_5I2_STAB_DIAG= prove( `!v i j.
586 v IN MMs_v39 scs_5I2 /\
588 dist(v i,v j) <= cstab ==>
589 v IN MMs_v39 (scs_stab_diag_v39 scs_5I2 i j)`,
591 THEN REPEAT STRIP_TAC
592 THEN MP_TAC SCS_5I2_IS_SCS
594 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I2`;`v`]
595 THEN MRESA_TAC DIST_LE_IMP_A_LE[`v`;`scs_5I2`;`i`;`j`;`cstab`]
596 THEN ASSUME_TAC SCS_5I2_BASIC
597 THEN ASSUME_TAC K_SCS_5I2
598 THEN MRESAL_TAC Yrtafyh.YRTAFYH[`scs_5I2`;`i`;`j`][ARITH_RULE`3<5`;]
599 THEN MP_TAC Ppbtydq.MXQTIED
602 THEN MATCH_DICH_TAC 0
603 THEN EXISTS_TAC`scs_5I2`
604 THEN ASM_SIMP_TAC[STAB_BB;SCS_K_D_A_STAB_EQ;DIAG_SCS_M_EQ;REAL_ARITH`a<=a`]
606 THEN REWRITE_TAC[scs_stab_diag_v39;scs_5I2;scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;CS_ADJ]
608 THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
611 MRESAL_TAC DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
613 THEN REWRITE_TAC[scs_diag;cstab;h0]
620 let SCS_5I3_STAB_DIAG= prove( `!v i j.
621 v IN MMs_v39 scs_5I3 /\
623 dist(v i,v j) <= cstab ==>
624 v IN MMs_v39 (scs_stab_diag_v39 scs_5I3 i j)`,
626 THEN REPEAT STRIP_TAC
627 THEN MP_TAC SCS_5I3_IS_SCS
629 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5I3`;`v`]
630 THEN MRESA_TAC DIST_LE_IMP_A_LE[`v`;`scs_5I3`;`i`;`j`;`cstab`]
631 THEN ASSUME_TAC SCS_5I3_BASIC
632 THEN ASSUME_TAC K_SCS_5I3
633 THEN MRESAL_TAC Yrtafyh.YRTAFYH[`scs_5I3`;`i`;`j`][ARITH_RULE`3<5`;]
634 THEN MP_TAC Ppbtydq.MXQTIED
637 THEN MATCH_DICH_TAC 0
638 THEN EXISTS_TAC`scs_5I3`
639 THEN ASM_SIMP_TAC[STAB_BB;SCS_K_D_A_STAB_EQ;DIAG_SCS_M_EQ;REAL_ARITH`a<=a`]
641 THEN REWRITE_TAC[scs_stab_diag_v39;scs_5I3;scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;CS_ADJ]
643 THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
646 MRESAL_TAC DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
648 THEN REWRITE_TAC[scs_diag;cstab;h0]
650 THEN MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`]
651 THEN REWRITE_TAC[PAIR_EQ]
657 let SCS_5M1_STAB_DIAG= prove( `!v i j.
658 v IN MMs_v39 scs_5M1 /\
660 dist(v i,v j) <= cstab ==>
661 v IN MMs_v39 (scs_stab_diag_v39 scs_5M1 i j)`,
663 THEN REPEAT STRIP_TAC
664 THEN MP_TAC SCS_5M1_IS_SCS
666 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M1`;`v`]
667 THEN MRESA_TAC DIST_LE_IMP_A_LE[`v`;`scs_5M1`;`i`;`j`;`cstab`]
668 THEN ASSUME_TAC SCS_5M1_BASIC
669 THEN ASSUME_TAC K_SCS_5M1
670 THEN MRESAL_TAC Yrtafyh.YRTAFYH[`scs_5M1`;`i`;`j`][ARITH_RULE`3<5`;]
671 THEN MP_TAC Ppbtydq.MXQTIED
674 THEN MATCH_DICH_TAC 0
675 THEN EXISTS_TAC`scs_5M1`
676 THEN ASM_SIMP_TAC[STAB_BB;SCS_K_D_A_STAB_EQ;DIAG_SCS_M_EQ;REAL_ARITH`a<=a`]
678 THEN REWRITE_TAC[scs_stab_diag_v39;scs_5M1;scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;CS_ADJ]
680 THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
683 MRESAL_TAC DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
685 THEN REWRITE_TAC[scs_diag;cstab;h0]
687 THEN MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`]
688 THEN REWRITE_TAC[PAIR_EQ]
697 let SCS_5I1_BERAK_BY_CSTAB= prove_by_refinement( `scs_arrow_v39 { scs_5I1 } ({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I1 i j| scs_diag 5 i j })`,
700 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
701 THEN ABBREV_TAC`k=scs_k_v39 s`
702 THEN REPEAT RESA_TAC;
704 REWRITE_TAC[SCS_5M2_IS_SCS];
706 MATCH_MP_TAC Yrtafyh.STAB_IS_SCS
707 THEN ASM_SIMP_TAC[SCS_5I1_IS_SCS;K_SCS_5I1;SCS_5I1_BASIC;ARITH_RULE`3<5`]
709 THEN REWRITE_TAC[h0;cstab]
712 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_5I1 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_5I1 ==> MMs_v39 s = {}))`);
717 THEN POP_ASSUM MP_TAC
718 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
719 THEN REPEAT STRIP_TAC
720 THEN POP_ASSUM MP_TAC
722 THEN POP_ASSUM MP_TAC
723 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
726 MP_TAC(SET_RULE`(!i j. scs_diag 5 i j ==> cstab < dist(v i,v j))\/ ~((!i j. scs_diag 5 i j ==> cstab < dist((v:num->real^3) i,v j)))`)
730 THEN ASM_REWRITE_TAC[]
731 THEN MP_TAC MM_5I1_IMP_MM_5M2
733 THEN POP_ASSUM MP_TAC
734 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
736 THEN MATCH_DICH_TAC 0
737 THEN REPEAT STRIP_TAC
738 THEN THAYTHE_TAC 1[`i`;`j`]
739 THEN POP_ASSUM MP_TAC
743 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
745 THEN EXISTS_TAC`scs_stab_diag_v39 scs_5I1 i j`
746 THEN ASM_REWRITE_TAC[]
749 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
750 THEN EXISTS_TAC`i:num`
751 THEN EXISTS_TAC`j:num`
752 THEN ASM_REWRITE_TAC[];
754 MRESAL_TAC SCS_5I1_STAB_DIAG[`v`;`i`;`j`][IN]
755 THEN EXISTS_TAC`v:num->real^3`
756 THEN ASM_REWRITE_TAC[];]);;
759 let SCS_5I2_BERAK_BY_CSTAB= prove_by_refinement(
760 `scs_arrow_v39 { scs_5I2 } ({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j })`,
763 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
764 THEN ABBREV_TAC`k=scs_k_v39 s`
765 THEN REPEAT RESA_TAC;
767 REWRITE_TAC[SCS_5M2_IS_SCS];
769 MATCH_MP_TAC Yrtafyh.STAB_IS_SCS
770 THEN ASM_SIMP_TAC[SCS_5I2_IS_SCS;K_SCS_5I2;SCS_5I2_BASIC;ARITH_RULE`3<5`]
772 THEN REWRITE_TAC[h0;cstab]
773 THEN MP_TAC sqrt8_LE_CSTAB
776 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_5I2 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_5I2 ==> MMs_v39 s = {}))`);
781 THEN POP_ASSUM MP_TAC
782 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
783 THEN REPEAT STRIP_TAC
784 THEN POP_ASSUM MP_TAC
786 THEN POP_ASSUM MP_TAC
787 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
790 MP_TAC(SET_RULE`(!i j. scs_diag 5 i j ==> cstab < dist(v i,v j))\/ ~((!i j. scs_diag 5 i j ==> cstab < dist((v:num->real^3) i,v j)))`)
794 THEN ASM_REWRITE_TAC[]
795 THEN MP_TAC MM_5I2_IMP_MM_5M2
797 THEN POP_ASSUM MP_TAC
798 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
800 THEN MATCH_DICH_TAC 0
801 THEN REPEAT STRIP_TAC
802 THEN THAYTHE_TAC 1[`i`;`j`]
803 THEN POP_ASSUM MP_TAC
807 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
809 THEN EXISTS_TAC`scs_stab_diag_v39 scs_5I2 i j`
810 THEN ASM_REWRITE_TAC[]
813 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
814 THEN EXISTS_TAC`i:num`
815 THEN EXISTS_TAC`j:num`
816 THEN ASM_REWRITE_TAC[];
818 MRESAL_TAC SCS_5I2_STAB_DIAG[`v`;`i`;`j`][IN]
819 THEN EXISTS_TAC`v:num->real^3`
820 THEN ASM_REWRITE_TAC[]]);;
824 let SCS_5I3_BERAK_BY_CSTAB= prove_by_refinement(
825 `scs_arrow_v39 { scs_5I3 } ({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I3 i j| scs_diag 5 i j })`,
828 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
829 THEN ABBREV_TAC`k=scs_k_v39 s`
830 THEN REPEAT RESA_TAC;
832 REWRITE_TAC[SCS_5M2_IS_SCS];
834 MATCH_MP_TAC Yrtafyh.STAB_IS_SCS
835 THEN ASM_SIMP_TAC[SCS_5I3_IS_SCS;K_SCS_5I3;SCS_5I3_BASIC;ARITH_RULE`3<5`]
837 THEN REWRITE_TAC[h0;cstab]
838 THEN MP_TAC sqrt8_LE_CSTAB
841 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_5I3 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_5I3 ==> MMs_v39 s = {}))`);
846 THEN POP_ASSUM MP_TAC
847 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
848 THEN REPEAT STRIP_TAC
849 THEN POP_ASSUM MP_TAC
851 THEN POP_ASSUM MP_TAC
852 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
855 MP_TAC(SET_RULE`(!i j. scs_diag 5 i j ==> cstab < dist(v i,v j))\/ ~((!i j. scs_diag 5 i j ==> cstab < dist((v:num->real^3) i,v j)))`)
859 THEN ASM_REWRITE_TAC[]
860 THEN MP_TAC MM_5I3_IMP_MM_5M2
862 THEN POP_ASSUM MP_TAC
863 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
865 THEN MATCH_DICH_TAC 0
866 THEN REPEAT STRIP_TAC
867 THEN THAYTHE_TAC 1[`i`;`j`]
868 THEN POP_ASSUM MP_TAC
872 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
874 THEN EXISTS_TAC`scs_stab_diag_v39 scs_5I3 i j`
875 THEN ASM_REWRITE_TAC[]
878 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
879 THEN EXISTS_TAC`i:num`
880 THEN EXISTS_TAC`j:num`
881 THEN ASM_REWRITE_TAC[];
883 MRESAL_TAC SCS_5I3_STAB_DIAG[`v`;`i`;`j`][IN]
884 THEN EXISTS_TAC`v:num->real^3`
885 THEN ASM_REWRITE_TAC[]]);;
888 let SCS_5M1_BERAK_BY_CSTAB= prove_by_refinement(`scs_arrow_v39 { scs_5M1 } ({ scs_5M2}UNION { scs_stab_diag_v39 scs_5M1 i j| scs_diag 5 i j })`,
891 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
892 THEN ABBREV_TAC`k=scs_k_v39 s`
893 THEN REPEAT RESA_TAC;
895 REWRITE_TAC[SCS_5M2_IS_SCS];
897 MATCH_MP_TAC Yrtafyh.STAB_IS_SCS
898 THEN ASM_SIMP_TAC[SCS_5M1_IS_SCS;K_SCS_5M1;SCS_5M1_BASIC;ARITH_RULE`3<5`]
900 THEN REWRITE_TAC[h0;cstab]
901 THEN MP_TAC sqrt8_LE_CSTAB
904 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_5M1 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_5M1 ==> MMs_v39 s = {}))`);
909 THEN POP_ASSUM MP_TAC
910 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
911 THEN REPEAT STRIP_TAC
912 THEN POP_ASSUM MP_TAC
914 THEN POP_ASSUM MP_TAC
915 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
918 MP_TAC(SET_RULE`(!i j. scs_diag 5 i j ==> cstab < dist(v i,v j))\/ ~((!i j. scs_diag 5 i j ==> cstab < dist((v:num->real^3) i,v j)))`)
922 THEN ASM_REWRITE_TAC[]
923 THEN MP_TAC MM_5M1_IMP_MM_5M2
925 THEN POP_ASSUM MP_TAC
926 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
928 THEN MATCH_DICH_TAC 0
929 THEN REPEAT STRIP_TAC
930 THEN THAYTHE_TAC 1[`i`;`j`]
931 THEN POP_ASSUM MP_TAC
935 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
937 THEN EXISTS_TAC`scs_stab_diag_v39 scs_5M1 i j`
938 THEN ASM_REWRITE_TAC[]
941 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
942 THEN EXISTS_TAC`i:num`
943 THEN EXISTS_TAC`j:num`
944 THEN ASM_REWRITE_TAC[];
946 MRESAL_TAC SCS_5M1_STAB_DIAG[`v`;`i`;`j`][IN]
947 THEN EXISTS_TAC`v:num->real^3`
948 THEN ASM_REWRITE_TAC[]]);;
951 (**********************)
953 let DIAG_EQ_ADD5=prove(`scs_diag 5 (i MOD 5) (j MOD 5)<=>
954 ((i MOD 5= (j MOD 5+ 2) MOD 5)\/
955 (j MOD 5=(i MOD 5+2) MOD 5))`,
956 REWRITE_TAC[scs_diag]
957 THEN MP_TAC(ARITH_RULE`i MOD 5<5==> i MOD 5= 0 \/ i MOD 5= 1 \/i MOD 5= 2 \/
958 i MOD 5= 3 \/i MOD 5= 4 `)
959 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
961 THEN MP_TAC(ARITH_RULE`j MOD 5<5==> j MOD 5= 0 \/ j MOD 5= 1 \/j MOD 5= 2 \/
962 j MOD 5= 3 \/j MOD 5= 4
964 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
969 let EXPAND_STAB_DIAG_5=prove_by_refinement(`is_scs_v39 s /\scs_k_v39 s=5==>
970 {scs_stab_diag_v39 s (i MOD 5) (j MOD 5) | i MOD 5 =
971 (j MOD 5 + 2) MOD 5 \/
973 (i MOD 5 + 2) MOD 5}=
974 {scs_stab_diag_v39 s (i+2) i| i<5} `,
975 [REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;UNION]
981 MRESAS_TAC STAB_MOD[`s`;`j MOD 5 + 2`;`j MOD 5`][SCS_5I1_IS_SCS;K_SCS_5I1;MOD_REFL;ARITH_RULE`~(5=0)`]
982 THEN EXISTS_TAC`j MOD 5`
983 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`];
985 MRESAS_TAC STAB_MOD[`s`;`i MOD 5`;`i MOD 5 + 2`][SCS_5I1_IS_SCS;K_SCS_5I1;MOD_REFL;ARITH_RULE`~(5=0)`]
986 THEN EXISTS_TAC`i MOD 5`
987 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`;STAB_SYM];
990 THEN EXISTS_TAC`i:num`
991 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`;MOD_LT]
992 THEN MRESAS_TAC STAB_MOD[`s`;`(i + 2)`;`i`][SCS_5I1_IS_SCS;K_SCS_5I1;MOD_REFL;ARITH_RULE`~(5=0)`;MOD_LT]]);;
995 let EXPAND_STAB_DIAG_5I1=prove(`{scs_stab_diag_v39 scs_5I1 (i MOD 5) (j MOD 5) | i MOD 5 =
996 (j MOD 5 + 2) MOD 5 \/
998 (i MOD 5 + 2) MOD 5}=
999 {scs_stab_diag_v39 scs_5I1 (i+2) i| i<5} `,
1000 ASM_SIMP_TAC[EXPAND_STAB_DIAG_5;SCS_5I1_IS_SCS;K_SCS_5I1]);;
1003 let EXPAND_STAB_DIAG_5I2=prove(`{scs_stab_diag_v39 scs_5I2 (i MOD 5) (j MOD 5) | i MOD 5 =
1004 (j MOD 5 + 2) MOD 5 \/
1006 (i MOD 5 + 2) MOD 5}=
1007 {scs_stab_diag_v39 scs_5I2 (i+2) i| i<5} `,
1008 ASM_SIMP_TAC[EXPAND_STAB_DIAG_5;SCS_5I2_IS_SCS;K_SCS_5I2]);;
1012 let EXPAND_STAB_DIAG_5I3=prove(`{scs_stab_diag_v39 scs_5I3 (i MOD 5) (j MOD 5) | i MOD 5 =
1013 (j MOD 5 + 2) MOD 5 \/
1015 (i MOD 5 + 2) MOD 5}=
1016 {scs_stab_diag_v39 scs_5I3 (i+2) i| i<5} `,
1017 ASM_SIMP_TAC[EXPAND_STAB_DIAG_5;SCS_5I3_IS_SCS;K_SCS_5I3]);;
1020 let EXPAND_STAB_DIAG_5M1=prove(`{scs_stab_diag_v39 scs_5M1 (i MOD 5) (j MOD 5) | i MOD 5 =
1021 (j MOD 5 + 2) MOD 5 \/
1023 (i MOD 5 + 2) MOD 5}=
1024 {scs_stab_diag_v39 scs_5M1 (i+2) i| i<5} `,
1025 ASM_SIMP_TAC[EXPAND_STAB_DIAG_5;SCS_5M1_IS_SCS;K_SCS_5M1]);;
1032 let EQ_DIAG_STAB_5I1_02=prove(`scs_arrow_v39
1033 {scs_stab_diag_v39 scs_5I1 (i + 2) i }
1034 {scs_stab_diag_v39 scs_5I1 0 2}`,
1035 MRESA_TAC STAB_SYM[`scs_5I1`;`2`;`0`]
1036 THEN MP_TAC (GEN_ALL Wkeidft.WKEIDFT)
1037 THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
1039 THEN MATCH_DICH_TAC 0
1040 THEN ASM_SIMP_TAC[ARITH_RULE`2 + i = (i + 2) + 0/\ 3<6/\ i+1= SUC i`;K_SCS_5I1;h0_LT_B_SCS_5I1;h0_EQ_B_SCS_5I1;SCS_5I1_IS_SCS;SCS_5I1_BASIC]
1042 THEN ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;]
1045 THEN EXISTS_TAC`&2 *h0`
1046 THEN EXISTS_TAC`&2 *h0`
1048 THEN ASM_SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + 2)= i+3/\ SUC i= i+1/\ 2+1=3`;ARITH_RULE`1<5/\ ~(5=0)`;Qknvmlb.SUC_MOD_NOT_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1050 THEN MP_TAC(SET_RULE`i= i+0==> i MOD 5= (i+0) MOD 5`)
1051 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
1053 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`1<5/\ ~(5=0)/\ 3<5`]
1058 let EQ_DIAG_STAB_5I2_02=prove(`scs_arrow_v39
1059 {scs_stab_diag_v39 scs_5I2 (i + 2) i }
1060 {scs_stab_diag_v39 scs_5I2 0 2}`,
1061 MRESA_TAC STAB_SYM[`scs_5I2`;`2`;`0`]
1062 THEN MP_TAC (GEN_ALL Wkeidft.WKEIDFT)
1063 THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
1065 THEN MATCH_DICH_TAC 0
1066 THEN ASM_SIMP_TAC[ARITH_RULE`2 + i = (i + 2) + 0/\ 3<6/\ i+1= SUC i`;K_SCS_5I2;h0_LT_B_SCS_5I2;h0_EQ_B_SCS_5I2;SCS_5I2_IS_SCS;SCS_5I2_BASIC]
1068 THEN ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;]
1071 THEN EXISTS_TAC`&2 *h0`
1072 THEN EXISTS_TAC`sqrt8`
1074 THEN ASM_SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + 2)= i+3/\ SUC i= i+1/\ 2+1=3`;ARITH_RULE`1<5/\ ~(5=0)`;Qknvmlb.SUC_MOD_NOT_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1076 THEN MP_TAC(SET_RULE`i= i+0==> i MOD 5= (i+0) MOD 5`)
1077 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
1079 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`1<5/\ ~(5=0)/\ 3<5`]
1083 let SET_EQ_DIAG_STAB_5I1_02=prove(`scs_arrow_v39
1084 {scs_stab_diag_v39 scs_5I1 (i + 2) i |i<5}
1085 {scs_stab_diag_v39 scs_5I1 0 2}`,
1086 REWRITE_TAC[ARITH_RULE`i<5<=> i=0\/i=1\/i=2\/i=3\/i=4`;SET_RULE`{scs_stab_diag_v39 scs_5I1 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
1088 {scs_stab_diag_v39 scs_5I1 (0 + 2) 0} UNION
1089 {scs_stab_diag_v39 scs_5I1 (1 + 2) 1} UNION
1090 {scs_stab_diag_v39 scs_5I1 (2 + 2) 2} UNION
1091 {scs_stab_diag_v39 scs_5I1 (3 + 2) 3} UNION
1092 {scs_stab_diag_v39 scs_5I1 (4 + 2) 4}
1094 THEN REPEAT(ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_5I1 0 2}={scs_stab_diag_v39 scs_5I1 0 2} UNION {scs_stab_diag_v39 scs_5I1 0 2}`]
1095 THEN MATCH_MP_TAC FZIOTEF_UNION
1096 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_5I1_02]));;
1100 let SET_EQ_DIAG_STAB_5I2_02=prove(`scs_arrow_v39
1101 {scs_stab_diag_v39 scs_5I2 (i + 2) i |i<5}
1102 {scs_stab_diag_v39 scs_5I2 0 2}`,
1103 REWRITE_TAC[ARITH_RULE`i<5<=> i=0\/i=1\/i=2\/i=3\/i=4`;SET_RULE`{scs_stab_diag_v39 scs_5I2 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
1105 {scs_stab_diag_v39 scs_5I2 (0 + 2) 0} UNION
1106 {scs_stab_diag_v39 scs_5I2 (1 + 2) 1} UNION
1107 {scs_stab_diag_v39 scs_5I2 (2 + 2) 2} UNION
1108 {scs_stab_diag_v39 scs_5I2 (3 + 2) 3} UNION
1109 {scs_stab_diag_v39 scs_5I2 (4 + 2) 4}
1111 THEN REPEAT(ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_5I2 0 2}={scs_stab_diag_v39 scs_5I2 0 2} UNION {scs_stab_diag_v39 scs_5I2 0 2}`]
1112 THEN MATCH_MP_TAC FZIOTEF_UNION
1113 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_5I2_02]));;
1117 (*******************)
1119 let SET_STAB_5I1=prove(`{ scs_stab_diag_v39 scs_5I1 i j| scs_diag 5 i j }= { scs_stab_diag_v39 scs_5I1 (i MOD 5) (j MOD 5)| scs_diag 5 (i MOD 5) (j MOD 5) }`,
1120 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(5=0)`;]
1121 THEN MRESAL_TAC STAB_MOD[`scs_5I1`][SCS_5I1_IS_SCS;K_SCS_5I1]);;
1124 let SET_STAB_5I2=prove(`{ scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j }= { scs_stab_diag_v39 scs_5I2 (i MOD 5) (j MOD 5)| scs_diag 5 (i MOD 5) (j MOD 5) }`,
1125 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(5=0)`;]
1126 THEN MRESAL_TAC STAB_MOD[`scs_5I2`][SCS_5I2_IS_SCS;K_SCS_5I2]);;
1129 let SET_STAB_5I3=prove(`{ scs_stab_diag_v39 scs_5I3 i j| scs_diag 5 i j }= { scs_stab_diag_v39 scs_5I3 (i MOD 5) (j MOD 5)| scs_diag 5 (i MOD 5) (j MOD 5) }`,
1130 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(5=0)`;]
1131 THEN MRESAL_TAC STAB_MOD[`scs_5I3`][SCS_5I3_IS_SCS;K_SCS_5I3]);;
1134 let SET_STAB_5M1=prove(`{ scs_stab_diag_v39 scs_5M1 i j| scs_diag 5 i j }= { scs_stab_diag_v39 scs_5M1 (i MOD 5) (j MOD 5)| scs_diag 5 (i MOD 5) (j MOD 5) }`,
1135 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(5=0)`;]
1136 THEN MRESAL_TAC STAB_MOD[`scs_5M1`][SCS_5M1_IS_SCS;K_SCS_5M1]);;
1139 let SET_EQ_DIAG_STAB_5I1=prove( `scs_arrow_v39 { scs_stab_diag_v39 scs_5I1 i j| scs_diag 5 i j }
1140 { scs_stab_diag_v39 scs_5I1 0 2}`,
1141 ONCE_REWRITE_TAC[SET_STAB_5I1]
1142 THEN REWRITE_TAC[DIAG_EQ_ADD5;EXPAND_STAB_DIAG_5I1]
1143 THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_5I1_02;]);;
1146 let SET_EQ_DIAG_STAB_5I2=prove( `scs_arrow_v39 { scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j }
1147 { scs_stab_diag_v39 scs_5I2 0 2}`,
1148 ONCE_REWRITE_TAC[SET_STAB_5I2]
1149 THEN REWRITE_TAC[DIAG_EQ_ADD5;EXPAND_STAB_DIAG_5I2]
1150 THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_5I2_02;]);;
1154 let OTMTOTJ1= prove(`scs_arrow_v39 { scs_5I1 } { scs_stab_diag_v39 scs_5I1 0 2 , scs_5M2 }`,
1155 MATCH_MP_TAC FZIOTEF_TRANS
1156 THEN EXISTS_TAC`({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I1 i j| scs_diag 5 i j })`
1157 THEN ASM_SIMP_TAC[SCS_5I1_BERAK_BY_CSTAB]
1158 THEN REWRITE_TAC[SET_RULE`{A,B}={B} UNION {A}`]
1159 THEN MATCH_MP_TAC FZIOTEF_UNION
1160 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_5I1]
1161 THEN MATCH_MP_TAC FZIOTEF_REFL
1162 THEN REWRITE_TAC[IN_SING]
1163 THEN REPEAT RESA_TAC
1164 THEN ASM_REWRITE_TAC[SCS_5M2_IS_SCS]);;
1167 let OTMTOTJ2= prove(`scs_arrow_v39 { scs_5I2 } { scs_stab_diag_v39 scs_5I2 0 2 , scs_5M2 }`,
1168 MATCH_MP_TAC FZIOTEF_TRANS
1169 THEN EXISTS_TAC`({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j })`
1170 THEN ASM_SIMP_TAC[SCS_5I2_BERAK_BY_CSTAB]
1171 THEN REWRITE_TAC[SET_RULE`{A,B}={B} UNION {A}`]
1172 THEN MATCH_MP_TAC FZIOTEF_UNION
1173 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_5I2]
1174 THEN MATCH_MP_TAC FZIOTEF_REFL
1175 THEN REWRITE_TAC[IN_SING]
1176 THEN REPEAT RESA_TAC
1177 THEN ASM_REWRITE_TAC[SCS_5M2_IS_SCS]);;
1179 (*************************)
1182 let BB_5I3_IS_BB_5M1=prove( ` BBs_v39 (scs_stab_diag_v39 scs_5I3 i j) v==> BBs_v39 (scs_stab_diag_v39 scs_5M1 i j) v`,
1183 REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5I3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`]
1185 THEN REPEAT RESA_TAC
1186 THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
1188 THEN THAYTHE_TAC 2[`i'`;`j'`]
1190 THEN MP_TAC sqrt8_LE_CSTAB
1191 THEN REWRITE_TAC[h0;cstab]
1192 THEN REAL_ARITH_TAC);;
1194 (***********SCS_BAISC************)
1197 let STAB_5I3_SCS=prove(` scs_diag (scs_k_v39 scs_5I3) i j
1198 ==> is_scs_v39 (scs_stab_diag_v39 scs_5I3 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5I3 i j)`,
1200 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
1201 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5I3_IS_SCS;SCS_5I3_BASIC;K_SCS_5I3;
1202 ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_5I3;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
1204 THEN REAL_ARITH_TAC);;
1208 let STAB_5I2_SCS=prove(` scs_diag (scs_k_v39 scs_5I2) i j
1209 ==> is_scs_v39 (scs_stab_diag_v39 scs_5I2 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5I2 i j)`,
1211 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
1212 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5I2_IS_SCS;SCS_5I2_BASIC;K_SCS_5I2;
1213 ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_5I3;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
1215 THEN MP_TAC sqrt8_LE_CSTAB
1216 THEN REAL_ARITH_TAC);;
1221 let STAB_5M1_SCS=prove(` scs_diag (scs_k_v39 scs_5M1) i j
1222 ==> is_scs_v39 (scs_stab_diag_v39 scs_5M1 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5M1 i j)`,
1224 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
1225 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5M1_IS_SCS;SCS_5M1_BASIC;K_SCS_5M1;
1226 ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_5I3;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
1228 THEN REWRITE_TAC[h0]
1229 THEN REAL_ARITH_TAC);;
1231 let STAB_5M2_SCS=prove(` scs_diag (scs_k_v39 scs_5M2) i j
1232 ==> is_scs_v39 (scs_stab_diag_v39 scs_5M2 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5M2 i j)`,
1234 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
1235 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5M2_IS_SCS;SCS_5M2_BASIC;K_SCS_5M2;
1236 ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_5I3;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
1238 THEN REWRITE_TAC[h0;cstab]
1239 THEN REAL_ARITH_TAC);;
1246 let MM_5I3_IMP_MM_5M1=prove(`scs_diag 5 i j /\ MMs_v39 (scs_stab_diag_v39 scs_5I3 i j) v ==> ~(MMs_v39 ((scs_stab_diag_v39 scs_5M1 i j)) ={})`,
1248 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
1249 THEN EXISTS_TAC`v:num->real^3`
1250 THEN EXISTS_TAC`(scs_stab_diag_v39 scs_5I3 i j)`
1251 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`(scs_stab_diag_v39 scs_5I3 i j)`;`v`]
1252 THEN ASSUME_TAC SCS_5M1_BASIC
1253 THEN ASSUME_TAC K_SCS_5M1
1254 THEN ASM_SIMP_TAC[BB_5I3_IS_BB_5M1;IN;SCS_5M1_IS_SCS;SCS_K_D_A_STAB_EQ;K_SCS_5I3;STAB_5M1_SCS;STAB_5I3_SCS]
1256 THEN REAL_ARITH_TAC);;
1259 let STAB_5I3_ARROW_STAB_5M1=prove_by_refinement(`scs_diag 5 i j
1260 ==> scs_arrow_v39 { scs_stab_diag_v39 scs_5I3 i j} { scs_stab_diag_v39 scs_5M1 i j}`,
1263 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
1264 THEN ABBREV_TAC`k=scs_k_v39 s`
1265 THEN REPEAT RESA_TAC;
1267 ASM_SIMP_TAC[BB_5I3_IS_BB_5M1;IN;SCS_5M1_IS_SCS;SCS_K_D_A_STAB_EQ;K_SCS_5I3;STAB_5M1_SCS;STAB_5I3_SCS;K_SCS_5M1];
1269 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_stab_diag_v39 scs_5I3 i j==> MMs_v39 s = {}) \/ ~((!s. s = scs_stab_diag_v39 scs_5I3 i j ==> MMs_v39 s = {}))`);
1275 THEN POP_ASSUM MP_TAC
1276 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
1277 THEN REPEAT STRIP_TAC
1278 THEN POP_ASSUM MP_TAC
1280 THEN POP_ASSUM MP_TAC
1281 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1283 THEN EXISTS_TAC`scs_stab_diag_v39 scs_5M1 i j`
1284 THEN ASM_REWRITE_TAC[]
1285 THEN MP_TAC MM_5I3_IMP_MM_5M1
1287 THEN POP_ASSUM MP_TAC
1288 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1290 THEN MATCH_DICH_TAC 0
1291 THEN REPEAT STRIP_TAC]);;
1294 let h0_EQ_B_SCS_5M2=prove(`(!i j. scs_diag 5 i j ==> scs_b_v39 scs_5M2 i j= &6)
1295 /\ (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5M2 i j= cstab)`,
1297 THEN REWRITE_TAC[h0;scs_diag;cstab]
1298 THEN REPEAT RESA_TAC
1299 THEN MP_TAC DIAG_5_EQU_PSORT
1301 THEN REWRITE_TAC[PAIR_EQ]
1305 let h0_EQ_B_SCS_5M1=prove(`(!i j. scs_diag 5 i j ==> scs_b_v39 scs_5M1 i j= &6)
1306 /\ (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5M1 i j= &2 * h0)`,
1308 THEN REWRITE_TAC[h0;scs_diag;cstab]
1309 THEN REPEAT RESA_TAC
1310 THEN MP_TAC DIAG_5_EQU_PSORT
1312 THEN REWRITE_TAC[PAIR_EQ]
1317 let PROP_OPP_DIAG_5M1_03= prove_by_refinement(`scs_stab_diag_v39 scs_5M1 0 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_5M1 1 3)) 3 `,
1319 [REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; scs_basic;SCS_K_D_A_STAB_EQ;scs_opp_v39]
1320 THEN MATCH_MP_TAC scs_inj
1321 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_5M1_BASIC]
1324 MRESAL_TAC STAB_5M1_SCS[`0`;`3`][K_SCS_5M1;scs_diag;ARITH_RULE`~(0 MOD 5 = 3 MOD 5) /\
1325 ~(SUC 0 MOD 5 = 3 MOD 5) /\
1326 ~(0 MOD 5 = SUC 3 MOD 5)`];
1330 ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M1;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM]
1334 THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M1;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;]
1335 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
1337 THEN ASSUME_TAC (ARITH_RULE`~(5=0)`)
1338 THEN MRESA_TAC PSORT_MOD[`5`;`x`;`x'`]
1340 THEN MRESA_TAC MOD_ADD_MOD[`3`;`x`;`5`]
1341 THEN MRESA_TAC MOD_ADD_MOD[`3`;`x'`;`5`]
1344 THEN MP_TAC(ARITH_RULE`x MOD 5<5==> x MOD 5=0\/ x MOD 5=1\/ x MOD 5=2\/ x MOD 5=3\/x MOD 5=4`)
1345 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
1347 THEN MP_TAC(ARITH_RULE`x' MOD 5<5==> x' MOD 5=0\/ x' MOD 5=1\/ x' MOD 5=2\/ x' MOD 5=3\/x' MOD 5=4`)
1348 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
1350 THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;ARITH_RULE`5-1=4/\ 5-2=3/\ 5-3=2/\ 5-4=1/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6
1351 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ]]);;
1355 let PROP_OPP_DIAG_5M1_02= prove_by_refinement(`scs_stab_diag_v39 scs_5M1 0 2= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_5M1 1 4)) 3 `,
1357 [REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; scs_basic;SCS_K_D_A_STAB_EQ;scs_opp_v39]
1358 THEN MATCH_MP_TAC scs_inj
1359 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_5M1_BASIC]
1362 MRESAL_TAC STAB_5M1_SCS[`0`;`2`][K_SCS_5M1;scs_diag;ARITH_RULE`~(0 MOD 5 = 2 MOD 5) /\
1363 ~(SUC 0 MOD 5 = 2 MOD 5) /\
1364 ~(0 MOD 5 = SUC 2 MOD 5)`];
1368 ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M1;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM]
1372 THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M1;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;]
1373 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
1375 THEN ASSUME_TAC (ARITH_RULE`~(5=0)`)
1376 THEN MRESA_TAC PSORT_MOD[`5`;`x`;`x'`]
1378 THEN MRESA_TAC MOD_ADD_MOD[`3`;`x`;`5`]
1379 THEN MRESA_TAC MOD_ADD_MOD[`3`;`x'`;`5`]
1382 THEN MP_TAC(ARITH_RULE`x MOD 5<5==> x MOD 5=0\/ x MOD 5=1\/ x MOD 5=2\/ x MOD 5=3\/x MOD 5=4`)
1383 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
1385 THEN MP_TAC(ARITH_RULE`x' MOD 5<5==> x' MOD 5=0\/ x' MOD 5=1\/ x' MOD 5=2\/ x' MOD 5=3\/x' MOD 5=4`)
1386 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
1388 THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;ARITH_RULE`5-1=4/\ 5-2=3/\ 5-3=2/\ 5-4=1/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6
1389 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ]]);;
1393 let STAB_5I3_ARROW_STAB_5M1_DIAG=prove( `scs_arrow_v39 {scs_stab_diag_v39 scs_5I3 i j | scs_diag 5 i j}
1394 {scs_stab_diag_v39 scs_5M1 i j | scs_diag 5 i j}`,
1395 ONCE_REWRITE_TAC[SET_STAB_5I3]
1396 THEN ONCE_REWRITE_TAC[SET_STAB_5M1]
1397 THEN REWRITE_TAC[DIAG_EQ_ADD5;EXPAND_STAB_DIAG_5I3;EXPAND_STAB_DIAG_5M1]
1398 THEN REWRITE_TAC[ARITH_RULE`i<5<=> i=0\/i=1\/i=2\/i=3\/i=4`;SET_RULE`{scs_stab_diag_v39 scs_5I3 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
1400 {scs_stab_diag_v39 scs_5I3 (0 + 2) 0} UNION
1401 {scs_stab_diag_v39 scs_5I3 (1 + 2) 1} UNION
1402 {scs_stab_diag_v39 scs_5I3 (2 + 2) 2} UNION
1403 {scs_stab_diag_v39 scs_5I3 (3 + 2) 3} UNION
1404 {scs_stab_diag_v39 scs_5I3 (4 + 2) 4}
1405 `;SET_RULE`{scs_stab_diag_v39 scs_5M1 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
1407 {scs_stab_diag_v39 scs_5M1 (0 + 2) 0} UNION
1408 {scs_stab_diag_v39 scs_5M1 (1 + 2) 1} UNION
1409 {scs_stab_diag_v39 scs_5M1 (2 + 2) 2} UNION
1410 {scs_stab_diag_v39 scs_5M1 (3 + 2) 3} UNION
1411 {scs_stab_diag_v39 scs_5M1 (4 + 2) 4}
1413 THEN REPEAT(MATCH_MP_TAC FZIOTEF_UNION
1415 THENL[MATCH_MP_TAC STAB_5I3_ARROW_STAB_5M1
1416 THEN REWRITE_TAC[scs_diag;ARITH_RULE`3+2=5/\ 2+2=4`]
1419 THEN MATCH_MP_TAC STAB_5I3_ARROW_STAB_5M1
1420 THEN REWRITE_TAC[scs_diag;ARITH_RULE`4+2=6/\ 7 MOD 5=2`]
1422 THEN REWRITE_TAC[scs_diag;ARITH_RULE`4+2=6/\ 7 MOD 5=2/\ ~(2=4)`]);;
1427 let SET_EQ_DIAG_STAB_5M1= prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M1 i j | scs_diag 5 i j}
1428 {scs_stab_diag_v39 scs_5M1 0 2, scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39
1433 ONCE_REWRITE_TAC[SET_STAB_5M1]
1434 THEN REWRITE_TAC[DIAG_EQ_ADD5;EXPAND_STAB_DIAG_5I3;EXPAND_STAB_DIAG_5M1]
1435 THEN REWRITE_TAC[ARITH_RULE`i<5<=> i=0\/i=1\/i=2\/i=3\/i=4`;
1443 `;SET_RULE`{scs_stab_diag_v39 scs_5M1 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
1445 {scs_stab_diag_v39 scs_5M1 (0 + 2) 0} UNION
1446 {scs_stab_diag_v39 scs_5M1 (1 + 2) 1} UNION
1447 {scs_stab_diag_v39 scs_5M1 (2 + 2) 2} UNION
1448 {scs_stab_diag_v39 scs_5M1 (3 + 2) 3} UNION
1449 {scs_stab_diag_v39 scs_5M1 (4 + 2) 4}
1451 THEN MATCH_MP_TAC FZIOTEF_UNION
1454 REWRITE_TAC[ARITH_RULE`0+2=2`;STAB_SYM]
1455 THEN MATCH_MP_TAC FZIOTEF_REFL
1456 THEN REWRITE_TAC[IN_SING]
1457 THEN REPEAT RESA_TAC
1458 THEN MRESAL_TAC STAB_5M1_SCS[`2`;`0`][scs_diag;K_SCS_5M1;ARITH_RULE`~(2 MOD 5 = 0 MOD 5) /\
1459 ~(SUC 2 MOD 5 = 0 MOD 5) /\
1460 ~(2 MOD 5 = SUC 0 MOD 5)`];
1462 MATCH_MP_TAC FZIOTEF_UNION
1465 REWRITE_TAC[ARITH_RULE`1+2=3`;STAB_SYM;PROP_OPP_DIAG_5M1_03]
1466 THEN MATCH_MP_TAC FZIOTEF_TRANS
1467 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_5M1 1 3)}`
1470 MATCH_MP_TAC (GEN_ALL YXIONXL2)
1472 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(5<=3)`;K_SCS_5M1]
1473 THEN MRESAL_TAC STAB_5M1_SCS[`1`;`3`][scs_diag;K_SCS_5M1;ARITH_RULE`~(1 MOD 5 = 3 MOD 5) /\
1474 ~(SUC 1 MOD 5 = 3 MOD 5) /\
1475 ~(1 MOD 5 = SUC 3 MOD 5)`];
1477 MATCH_MP_TAC(GEN_ALL YXIONXL3)
1478 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
1479 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_5M1 1 3)`
1480 THEN MRESAL_TAC STAB_5M1_SCS[`1`;`3`][scs_diag;K_SCS_5M1;ARITH_RULE`~(1 MOD 5 = 3 MOD 5) /\
1481 ~(SUC 1 MOD 5 = 3 MOD 5) /\
1482 ~(1 MOD 5 = SUC 3 MOD 5)`];
1484 MATCH_MP_TAC FZIOTEF_UNION
1487 REWRITE_TAC[ARITH_RULE`2+2=4`;STAB_SYM]
1488 THEN MATCH_MP_TAC FZIOTEF_REFL
1489 THEN REWRITE_TAC[IN_SING]
1490 THEN REPEAT RESA_TAC
1491 THEN MRESAL_TAC STAB_5M1_SCS[`2`;`4`][scs_diag;K_SCS_5M1;ARITH_RULE`~(2 MOD 5 = 4 MOD 5) /\
1492 ~(SUC 2 MOD 5 = 4 MOD 5) /\
1493 ~(2 MOD 5 = SUC 4 MOD 5)`];
1495 MATCH_MP_TAC FZIOTEF_UNION
1498 REWRITE_TAC[ARITH_RULE`3+2=5`;STAB_SYM]
1499 THEN MRESAL_TAC STAB_MOD[`scs_5M1`;`5`;`3`][SCS_5M1_IS_SCS;K_SCS_5M1;ARITH_RULE`5 MOD 5=0/\ 3 MOD 5=3`]
1501 THEN REWRITE_TAC[ARITH_RULE`3+2=5`;STAB_SYM]
1502 THEN MATCH_MP_TAC FZIOTEF_REFL
1503 THEN REWRITE_TAC[IN_SING]
1504 THEN REPEAT RESA_TAC
1505 THEN MRESAL_TAC STAB_5M1_SCS[`3`;`0`][scs_diag;K_SCS_5M1;ARITH_RULE`~(3 MOD 5 = 0 MOD 5) /\
1506 ~(SUC 3 MOD 5 = 0 MOD 5) /\
1507 ~(3 MOD 5 = SUC 0 MOD 5)`];
1509 REWRITE_TAC[ARITH_RULE`4+2=6`;]
1510 THEN MRESAL_TAC STAB_MOD[`scs_5M1`;`6`;`4`][SCS_5M1_IS_SCS;K_SCS_5M1;ARITH_RULE`6 MOD 5=1/\ 4 MOD 5=4`]
1512 THEN REWRITE_TAC[PROP_OPP_DIAG_5M1_02];
1514 MATCH_MP_TAC FZIOTEF_TRANS
1515 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_5M1 1 4)}`
1518 MATCH_MP_TAC (GEN_ALL YXIONXL2)
1520 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(5<=3)`;K_SCS_5M1]
1521 THEN MRESAL_TAC STAB_5M1_SCS[`1`;`4`][scs_diag;K_SCS_5M1;ARITH_RULE`~(1 MOD 5 = 4 MOD 5) /\
1522 ~(SUC 1 MOD 5 = 4 MOD 5) /\
1523 ~(1 MOD 5 = SUC 4 MOD 5)`];
1525 MATCH_MP_TAC(GEN_ALL YXIONXL3)
1526 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
1527 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_5M1 1 4)`
1528 THEN MRESAL_TAC STAB_5M1_SCS[`1`;`4`][scs_diag;K_SCS_5M1;ARITH_RULE`~(1 MOD 5 = 4 MOD 5) /\
1529 ~(SUC 1 MOD 5 = 4 MOD 5) /\
1530 ~(1 MOD 5 = SUC 4 MOD 5)`]]);;
1532 let OTMTOTJ3= prove_by_refinement(`scs_arrow_v39 { scs_5I3 } { scs_stab_diag_v39 scs_5M1 0 2 , scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4, scs_5M2 }`,
1534 [MATCH_MP_TAC FZIOTEF_TRANS
1535 THEN EXISTS_TAC`({ scs_5M2}UNION { scs_stab_diag_v39 scs_5I3 i j| scs_diag 5 i j })`
1536 THEN ASM_SIMP_TAC[SCS_5I3_BERAK_BY_CSTAB;SET_RULE`{A,B,C,D}={D} UNION {A,B,C}`]
1537 THEN MATCH_MP_TAC FZIOTEF_UNION
1540 MATCH_MP_TAC FZIOTEF_REFL
1541 THEN REWRITE_TAC[IN_SING]
1542 THEN REPEAT RESA_TAC
1543 THEN ASM_REWRITE_TAC[SCS_5M2_IS_SCS];
1545 MATCH_MP_TAC FZIOTEF_TRANS
1546 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_5M1 i j | scs_diag 5 i j}`
1547 THEN ASM_REWRITE_TAC[STAB_5I3_ARROW_STAB_5M1_DIAG];
1549 ASM_SIMP_TAC[SET_EQ_DIAG_STAB_5M1]]);;
1552 let OTMTOTJ4= prove(`scs_arrow_v39 { scs_5M1 } { scs_stab_diag_v39 scs_5M1 0 2 , scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4, scs_5M2 }`,
1553 MATCH_MP_TAC FZIOTEF_TRANS
1554 THEN EXISTS_TAC`({ scs_5M2}UNION { scs_stab_diag_v39 scs_5M1 i j| scs_diag 5 i j })`
1555 THEN ASM_SIMP_TAC[SCS_5M1_BERAK_BY_CSTAB;SET_RULE`{A,B,C,D}={D} UNION {A,B,C}`]
1556 THEN MATCH_MP_TAC FZIOTEF_UNION
1557 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_5M1]
1558 THEN MATCH_MP_TAC FZIOTEF_REFL
1559 THEN REWRITE_TAC[IN_SING]
1560 THEN REPEAT RESA_TAC
1561 THEN ASM_REWRITE_TAC[SCS_5M2_IS_SCS]);;
1568 let check_completeness_claimA_concl =
1569 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)