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 Hijqaha = struct
27 open Wrgcvdr_cizmrrh;;
35 open Flyspeck_constants;;
51 open Wrgcvdr_cizmrrh;;
53 open Flyspeck_constants;;
96 let SCS_5I1_STAB_DIAG_2h0=prove_by_refinement(`!v i j.
99 dist(v i,v j) <= cstab/\
100 (!i. dist(v i, v(i+1))<= &2 * h0)
102 BBs_v39 (scs_stab_diag_v39 scs_5I2 i j) v`,
105 THEN REPEAT STRIP_TAC
108 THEN POP_ASSUM(fun th-> ASSUME_TAC th
111 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)`;IN;K_SCS_5I2;Terminal.FUNLIST_EXPLICIT;]
115 THEN MP_TAC(SET_RULE`i' MOD 5= j' MOD 5\/ ~(i' MOD 5= j' MOD 5)`)
119 THAYTHE_TAC (8-6)[`i'`;`j'`];
121 MP_TAC(SET_RULE`SUC i' MOD 5= j' MOD 5\/ ~(SUC i' MOD 5= j' MOD 5)`)
125 THAYTHE_TAC (9-6)[`i'`;`j'`]
127 THEN MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
132 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i'`;`5`][ARITH_RULE`1<5`]
134 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`)
135 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
139 MP_TAC(SET_RULE`i' MOD 5= SUC j' MOD 5\/ ~(i' MOD 5= SUC j' MOD 5)`)
142 THAYTHE_TAC (10-6)[`i'`;`j'`]
144 THEN MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
146 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j'`;`5`][ARITH_RULE`1<5`]
148 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`)
149 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
153 MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`]
154 THEN THAYTHE_TAC(11-6)[`i'`;`j'`]
156 THEN REWRITE_TAC[PAIR_EQ;cstab]
158 THEN MP_TAC sqrt8_LE_CSTAB
161 THAYTHE_TAC (8-6)[`i'`;`j'`]
163 THEN REWRITE_TAC[cstab]
166 MP_TAC(SET_RULE`SUC i' MOD 5= j' MOD 5\/ ~(SUC i' MOD 5= j' MOD 5)`)
169 MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j'`;`v`;`SUC i'`][SCS_5M2_IS_SCS;K_SCS_5M2;]
170 THEN REWRITE_TAC[ADD1]
171 THEN THAYTHE_TAC (10-2)[`i'`]
172 THEN POP_ASSUM MP_TAC
173 THEN REWRITE_TAC[h0;cstab]
176 MP_TAC(SET_RULE`i' MOD 5= SUC j' MOD 5\/ ~(i' MOD 5= SUC j' MOD 5)`)
179 MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i'`;`v`;`SUC j'`][SCS_5M2_IS_SCS;K_SCS_5M2;]
180 THEN REWRITE_TAC[ADD1]
181 THEN ONCE_REWRITE_TAC[DIST_SYM]
182 THEN THAYTHE_TAC (11-2)[`j'`]
183 THEN POP_ASSUM MP_TAC
184 THEN REWRITE_TAC[h0;cstab]
187 MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
190 MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`5`];
192 MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i'`;`v`;`i`][SCS_5M2_IS_SCS;K_SCS_5M2;]
193 THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j'`;`v`;`j`][SCS_5M2_IS_SCS;K_SCS_5M2;];
195 MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j'`;`v`;`i`][SCS_5M2_IS_SCS;K_SCS_5M2;]
196 THEN MRESAL_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i'`;`v`;`j`][SCS_5M2_IS_SCS;K_SCS_5M2;]
197 THEN ONCE_REWRITE_TAC[DIST_SYM]
198 THEN ASM_REWRITE_TAC[];
200 MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`]
201 THEN THAYTHE_TAC(12-6)[`i'`;`j'`]
203 THEN REWRITE_TAC[PAIR_EQ;cstab]
208 let MM_5M2_IMP_MM_STAB_5I2=prove(`
211 dist(v i,v j) <= cstab/\
212 (!i. dist(v i, v(i+1))<= &2 * h0)
214 ~(MMs_v39 (scs_stab_diag_v39 scs_5I2 i j)= {})`,
216 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
217 THEN EXISTS_TAC`v:num->real^3`
218 THEN EXISTS_TAC`scs_5M2`
219 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`]
220 THEN ASSUME_TAC SCS_5M2_BASIC
221 THEN ASSUME_TAC K_SCS_5M2
222 THEN ASM_SIMP_TAC[SCS_5M2_IS_SCS;STAB_5I2_SCS;K_SCS_5I2;SCS_K_D_A_STAB_EQ;IN;SCS_5I1_STAB_DIAG_2h0]
224 THEN REAL_ARITH_TAC);;
228 let SCS_5I1_STAB_DIAG_2h0_sqrt8=prove_by_refinement(
231 dist(v i,v j) <= cstab/\
232 &2* h0 <= dist(v 0, v(1)) /\ dist(v 0, v(1))<= sqrt8
234 BBs_v39 ((scs_stab_diag_v39 scs_5I3 i j) ) v`,
237 THEN REPEAT STRIP_TAC
240 THEN POP_ASSUM(fun th-> ASSUME_TAC th
243 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)`;IN;K_SCS_5I3;scs_prop_equ_v39;]
244 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
248 THEN MP_TAC(SET_RULE`i' MOD 5= j' MOD 5\/ ~(i' MOD 5= j' MOD 5)`)
251 THAYTHES_TAC (8-6)[`i':num`;`j':num`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(5=0)`];
253 MP_TAC(SET_RULE`SUC i' MOD 5= j' MOD 5\/ ~(SUC i' MOD 5= j' MOD 5)`)
256 THAYTHE_TAC (9-6)[`i'`;`j'`]
258 THEN MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i':num`;`j':num`][ARITH_RULE`~(5=0)`]
260 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` (i') MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
261 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` (j') MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
265 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i'`;`5`][ARITH_RULE`1<5`]
267 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`)
268 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`;]
273 MP_TAC(SET_RULE`i' MOD 5=SUC j' MOD 5\/ ~(i' MOD 5=SUC j' MOD 5)`)
277 THAYTHE_TAC (10-6)[`i'`;`j'`]
279 THEN MRESAL_TAC Hexagons.PSORT_MOD[`5`;`i':num`;`j':num`][ARITH_RULE`~(5=0)`]
281 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` (i') MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
282 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` (j') MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
283 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`j'`;`5`][ARITH_RULE`1<5`]
285 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`)
286 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`;]
289 THEN ONCE_REWRITE_TAC[DIST_SYM]
292 MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`]
293 THEN THAYTHE_TAC(11-6)[`i'`;`j'`]
295 THEN REWRITE_TAC[PAIR_EQ;cstab;h0]
299 THAYTHES_TAC (8-6)[`i':num`;`j':num`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(5=0)`;cstab]
303 MP_TAC(SET_RULE`SUC i' MOD 5= j' MOD 5\/ ~(SUC i' MOD 5= j' MOD 5)`)
306 THAYTHES_TAC (9-6)[`i':num`;`j':num`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(5=0)`;cstab]
308 THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
311 MRESAL_TAC Hexagons.DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
313 THEN ASM_REWRITE_TAC[scs_diag];
316 THEN MP_TAC(SET_RULE`psort 5 (i',j') = 0,1\/ ~(psort 5 (i',j') = 0,1)`)
319 MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`1`;`j'`;`0`;`5`][PSORT_5_EXPLICIT];
321 MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
322 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`];
324 MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
325 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
326 THEN ONCE_REWRITE_TAC[DIST_SYM]
327 THEN ASM_REWRITE_TAC[];
329 MP_TAC(SET_RULE`i' MOD 5= SUC j' MOD 5\/ ~(i' MOD 5= SUC j' MOD 5)`)
332 THAYTHES_TAC (10-6)[`i':num`;`j':num`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(5=0)`;cstab]
334 THEN MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
337 MRESAL_TAC Hexagons.DIAD_PSORT_IMP_DIAD[`i`;`j`;`5`;`i'`;`j'`][ARITH_RULE`~(5=0)`]
339 THEN ASM_REWRITE_TAC[scs_diag];
342 THEN MP_TAC(SET_RULE`psort 5 (i',j') = 0,1\/ ~(psort 5 (i',j') = 0,1)`)
345 MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`1`;`j'`;`0`;`5`][PSORT_5_EXPLICIT];
347 MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
348 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`];
350 MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
351 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
352 THEN ONCE_REWRITE_TAC[DIST_SYM]
353 THEN ASM_REWRITE_TAC[];
355 MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
358 MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`j`;`j'`;`i`;`5`][PSORT_5_EXPLICIT];
360 MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
361 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`];
363 MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
364 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
365 THEN ONCE_REWRITE_TAC[DIST_SYM]
366 THEN ASM_REWRITE_TAC[];
369 MRESA_TAC DIAG_5_EQU_PSORT[`i'`;`j'`]
370 THEN THAYTHE_TAC(13-7)[`i'`;`j'`]
372 THEN REWRITE_TAC[PAIR_EQ;cstab]
378 let SCS_5M2_EDGE_LE_2H0=prove(`BBs_v39 scs_5M2 v/\
380 dist(v i,v j) <= cstab/\
381 &2* h0 < dist(v l, v (SUC l))
384 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)`;IN;K_SCS_5I3;scs_prop_equ_v39;]
385 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
386 THEN REPEAT STRIP_TAC
387 THEN THAYTHE_TAC 7[`l`;`SUC l`]
390 THEN ASM_SIMP_TAC[Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`~(5=0)`]
391 THEN MRESAL_TAC Hexagons.PSORT_MOD[`5`;`l:num`;`SUC l:num`][ARITH_RULE`~(5=0)`]
393 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`l`;`5`][ARITH_RULE`1<5`]
395 THEN MP_TAC(ARITH_RULE`l MOD 5<5==> l MOD 5=0\/ l MOD 5=1\/ l MOD 5=2\/ l MOD 5=3\/l MOD 5=4`)
396 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`;]
400 THEN REAL_ARITH_TAC);;
407 let SCS_5M2_EDGE_LE_2H0_IMP_0=prove( `BBs_v39 scs_5M2 v/\
409 dist(v i,v j) <= cstab/\
410 &2* h0 < dist(v l, v (SUC l))
413 THEN MP_TAC SCS_5M2_EDGE_LE_2H0
418 let MM_5M2_IMP_MM_STAB_5I3=prove(` MMs_v39 scs_5M2 v /\
420 dist(v i,v j) <= cstab/\
421 &2 * h0< dist(v l, v(l+1)) /\
422 dist(v l, v(l+1))<= sqrt8
424 ~(MMs_v39 (scs_stab_diag_v39 scs_5I3 i j)= {})`,
426 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
427 THEN EXISTS_TAC`v:num->real^3`
428 THEN EXISTS_TAC`scs_5M2`
429 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`]
430 THEN ASSUME_TAC SCS_5M2_BASIC
431 THEN ASSUME_TAC K_SCS_5M2
432 THEN ASM_SIMP_TAC[SCS_5M2_IS_SCS;STAB_5I3_SCS;K_SCS_5I3;SCS_K_D_A_STAB_EQ;IN; ADD1]
433 THEN MP_TAC SCS_5M2_EDGE_LE_2H0_IMP_0
434 THEN REWRITE_TAC[ ADD1]
438 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l:num`;`v`;` l MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`]
439 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l+1:num`;`v`;` (l+1) MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`]
440 THEN MRESAL_TAC MOD_ADD_MOD[`l`;`1`;`5`][ARITH_RULE`~(5=0)/\ 1 MOD 5=1/\ 0+a=a`] THEN SYM_ASSUM_TAC
443 THEN MP_TAC(REAL_ARITH`&2 * h0 < dist ((v:num->real^3) 0,v 1) ==> &2 * h0 <= dist (v 0,v 1)`)
445 THEN MP_TAC SCS_5I1_STAB_DIAG_2h0_sqrt8
448 THEN REAL_ARITH_TAC);;
451 let SCS_5I1_STAB_DIAG_sqrt8=prove_by_refinement(`BBs_v39 scs_5M2 v/\
453 dist(v i,v j) <= cstab/\
454 sqrt8 <= dist(v 0, v(1))
456 BBs_v39 ((scs_stab_diag_v39 scs_5M2 i j) ) v`,
459 THEN REPEAT STRIP_TAC
462 THEN POP_ASSUM(fun th-> ASSUME_TAC th
465 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)`;IN;K_SCS_5I3;scs_prop_equ_v39;]
466 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
470 THEN MP_TAC(SET_RULE`i' MOD 5= j' MOD 5\/ ~(i' MOD 5= j' MOD 5)`)
473 THAYTHE_TAC (8-6)[`i'`;`j'`]
475 THEN REWRITE_TAC[cstab]
478 MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
481 MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`j`;`j'`;`i`;`5`][PSORT_5_EXPLICIT];
484 MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
485 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`];
487 MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
488 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
489 THEN ONCE_REWRITE_TAC[DIST_SYM]
490 THEN ASM_REWRITE_TAC[];
492 THAYTHE_TAC(9-6)[`i'`;`j'`]
499 let MM_5M2_IMP_MM_STAB_5M2=prove(` MMs_v39 scs_5M2 v /\
501 dist(v i,v j) <= cstab/\
502 sqrt8<= dist(v l, v(l+1))
504 ~(MMs_v39 (scs_stab_diag_v39 scs_5M2 i j)= {})`,
506 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
507 THEN EXISTS_TAC`v:num->real^3`
508 THEN EXISTS_TAC`scs_5M2`
509 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`]
510 THEN ASSUME_TAC SCS_5M2_BASIC
511 THEN ASSUME_TAC K_SCS_5M2
512 THEN ASM_SIMP_TAC[SCS_5M2_IS_SCS;STAB_5M2_SCS;K_SCS_5I3;SCS_K_D_A_STAB_EQ;IN; ADD1]
513 THEN MP_TAC SCS_5M2_EDGE_LE_2H0_IMP_0
514 THEN ASM_REWRITE_TAC[ ADD1;h0]
515 THEN MP_TAC LT_sqrt8_2h0
517 THEN MP_TAC(REAL_ARITH`sqrt8 <= dist ((v:num->real^3) l,v (l + 1))/\ &2 * #1.26 < sqrt8==> &2 * #1.26 < dist (v l,v (l + 1))`)
521 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l:num`;`v`;` l MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`]
522 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l+1:num`;`v`;` (l+1) MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`]
523 THEN MRESAL_TAC MOD_ADD_MOD[`l`;`1`;`5`][ARITH_RULE`~(5=0)/\ 1 MOD 5=1/\ 0+a=a`] THEN SYM_ASSUM_TAC
525 THEN MP_TAC SCS_5I1_STAB_DIAG_sqrt8
528 THEN REAL_ARITH_TAC);;
533 (*new definition scs*)
534 (*************************)
536 let SCS_DIAG_SCS_5M2_02=prove(`scs_diag (scs_k_v39 scs_5M2) 0 2`,
537 REWRITE_TAC[K_SCS_5M2;scs_diag]
540 let SCS_DIAG_SCS_5M2_03=prove(`scs_diag (scs_k_v39 scs_5M2) 0 3`,
541 REWRITE_TAC[K_SCS_5M2;scs_diag]
544 let SCS_DIAG_SCS_5M2_24=prove(`scs_diag (scs_k_v39 scs_5M2) 2 4`,
545 REWRITE_TAC[K_SCS_5M2;scs_diag]
551 let scs_5M3 = new_definition`scs_5M3 = mk_unadorned_v39 5 (#0.616)
552 (funlist_v39 [(0,1),(&2*h0);(0,2),(cstab);(0,3),(cstab);(1,3),(cstab);(1,4),(cstab);(2,4),(cstab)] (&2) 5)
553 (funlist_v39 [(0,1),cstab;(0,2),(&6); (0,3),(&6); (1,3),(&6); (1,4),(&6); (2,4),(&6)] (&2*h0) 5)`;;
556 let scs_3T4_prime = (* terminal_tri_6833979866 = *) new_definition
557 `scs_3T4_prime = mk_unadorned_v39 3
559 (funlist_v39 [(0,1),(&2);(1,2),cstab] (&2*h0) 3)
560 (funlist_v39 [(0,1),(&2 * h0)] (cstab) 3)`;;
562 let scs_4M6_prime = new_definition
563 `scs_4M6_prime = mk_unadorned_v39 4 (#0.513)
564 (funlist_v39 [(0,1),cstab;(0,2),(cstab);(1,3),(cstab)] (&2) 4)
565 (funlist_v39 [(0,1),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
568 let scs_4M7_prime = new_definition
569 `scs_4M7_prime = mk_unadorned_v39 4 (#0.513)
570 (funlist_v39 [(0,1),cstab;(1,2),(&2*h0);(0,2),(cstab);(1,3),(cstab)] (&2) 4)
571 (funlist_v39 [(0,1),cstab;(1,2),cstab;(0,2),(&6);(1,3),(&6);(1,3),(&6)] (&2*h0) 4)`;;
574 let scs_3T1_PRELIM_prime = (* ear_jnull = *) new_definition
575 `scs_3T1_prime = scs_v39 (3, #0.11,
576 funlist_v39 [(0,1),cstab] (&2) 3,
577 funlist_v39 [(0,1),cstab] (&2) 3,
578 funlist_v39 [(0,1),cstab] (&2*h0) 3,
579 funlist_v39 [(0,1),cstab] ((&2)*h0) 3,
580 (\i j. F),{},{},{})`;;
582 let scs_3T1_prime = prove_by_refinement(
583 `scs_3T1_prime = mk_unadorned_v39 3 (#0.11)
584 (funlist_v39 [(0,1),(cstab)] (&2) 3)
585 (funlist_v39 [(0,1),(cstab)] (&2 * h0) 3)`,
588 BY(REWRITE_TAC[mk_unadorned_v39;scs_3T1_PRELIM_prime]);
591 let scs_4M8_prime = new_definition
592 `scs_4M8_prime = mk_unadorned_v39 4 (#0.513)
593 (funlist_v39 [(0,1),(&2*h0);(2,3),(cstab);(0,2),(cstab);(1,3),(cstab)] (&2) 4)
594 (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(&6);(1,3),(&6);(1,3),(&6)] (&2*h0) 4)`;;
598 let PSORT_5_EXPLICIT=prove(`
599 psort 5 (0,0)= (0,0)/\
600 psort 5 (1,1)= (1,1)/\
601 psort 5 (2,2)= (2,2)/\
602 psort 5 (3,3)= (3,3)/\
603 psort 5 (4,4)= (4,4)/\
604 psort 5 (0,1)= (0,1)/\
605 psort 5 (0,2)= (0,2)/\
606 psort 5 (0,3)= (0,3)/\
607 psort 5 (0,4)= (0,4)/\
608 psort 5 (1,0)= (0,1)/\
609 psort 5 (1,2)= (1,2)/\
610 psort 5 (1,3)= (1,3)/\
611 psort 5 (1,4)= (1,4)/\
612 psort 5 (2,0)= (0,2)/\
613 psort 5 (2,1)= (1,2)/\
614 psort 5 (2,3)= (2,3)/\
615 psort 5 (2,4)= (2,4)/\
616 psort 5 (3,0)= (0,3)/\
617 psort 5 (3,1)= (1,3)/\
618 psort 5 (3,2)= (2,3)/\
619 psort 5 (3,4)= (3,4)/\
620 psort 5 (4,0)= (0,4)/\
621 psort 5 (4,1)= (1,4)/\
622 psort 5 (4,2)= (2,4)/\
623 psort 5 (4,3)= (3,4)/\
624 psort 5 (4,5)= (0,4)/\
625 psort 5 (3,5)= (0,3)/\
626 psort 5 (2,5)= (0,2)/\
627 psort 5 (1,5)= (0,1)/\
628 psort 5 (5,1)= (0,1)/\
629 psort 5 (5,2)= (0,2)/\
630 psort 5 (5,3)= (0,3)/\
631 psort 5 (5,4)= (0,4)/\
632 psort 5 (5,5)= (0,0)/\
633 psort 5 (5,6)= (0,1)/\
634 psort 5 (5,7)= (0,2)/\
635 psort 5 (4,6)= (1,4)/\
636 psort 5 (6,4)= (1,4)/\
637 psort 5 (6,5)= (0,1)/\
638 psort 5 (6,7)= (1,2)/\
639 psort 5 (7,5)= (0,2)/\
640 psort 5 (7,6)= (1,2)/\
641 psort 5 (7,7)= (2,2)/\
642 psort 5 (6,6)= (1,1)/\
643 psort 4 (3,4)= (0,3)/\
644 psort 3 (2,0)= (0,2)/\
645 psort 3 (2,1)= (1,2)/\
646 psort 3 (1,0)= (0,1)`,
647 REWRITE_TAC[psort;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_4_TAC;LET_DEF;LET_END_DEF;MOD_5_EXPLICIT;ARITH_RULE`0<=a/\ ~(1<= 0)/\ ~(2<=0)/\ ~(3<=0)/\ ~(4<=0)/\a<=a/\ ~(2<=1)/\ ~(3<=2)/\ ~(4<=3)/\ ~(3<=1)/\ ~(4<=1)/\ ~(4<=2)/\ 2<=3`]);;
650 let SCS_TAC= ASM_SIMP_TAC[scs_basic;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} j <=> {} i`;periodic2;scs_basic;unadorned_v39;scs_prop_equ_v39;LET_DEF;LET_END_DEF;scs_stab_diag_v39;scs_half_slice_v39;
651 Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_5_TAC;
652 scs_5M1;scs_3M1;scs_6I1;scs_3T1;scs_4M2;scs_6M1;scs_6T1;scs_5I1;scs_5I2;scs_5I3;scs_5M2;scs_4M6;scs_3T4;scs_5M3;scs_3T4_prime;scs_4M6_prime;scs_4M7_prime;scs_4M7;scs_3T1_prime;scs_4M8;scs_4M8_prime;scs_5T1;scs_3T5;scs_4M3;scs_3T6;scs_4M4;scs_4M5;
653 Terminal.FUNLIST_EXPLICIT;Yrtafyh.PSORT_PERIODIC;PSORT_5_EXPLICIT;
654 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`];;
669 let SCS_5T1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5T1`,
671 REWRITE_TAC[scs_5T1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(5=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=5/\ 5<=6/\a<=a/\ ~(5=4)/\ ~(6=0)`;d_tame;REAL_ARITH`#0.616 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
672 THEN REPEAT RESA_TAC;
675 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
678 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
681 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
684 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
687 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
690 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
693 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
696 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
699 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
702 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
704 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
705 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
709 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
711 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
712 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
716 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
718 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
719 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
723 THEN REWRITE_TAC[h0;cstab]
727 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
731 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
734 ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(&2 * #1.26 < &2)/\ ~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;h0]
741 let SCS_5M3_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5M3`,
743 SIMP_TAC[scs_5M3;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=5/\ 5<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.616 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
744 THEN REPEAT RESA_TAC;
747 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
750 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
753 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
756 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
759 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
762 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
765 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
768 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
771 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
773 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
777 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
779 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
783 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
785 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
789 THEN REWRITE_TAC[h0;cstab]
793 THEN REWRITE_TAC[h0;cstab]
797 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
804 THEN ASM_SIMP_TAC[h0;cstab;]
805 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
806 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
807 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
808 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
809 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
813 THEN ASM_SIMP_TAC[h0;cstab;]
814 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
815 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
816 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
817 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
818 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`]
819 THEN SUBGOAL_THEN`{i | i < 5 /\
820 (&2 * #1.26 < (if psort 5 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/
821 &2 < (if psort 5 (i,SUC i) = 0,1 then &2* #1.26 else &2))} ={0}`ASSUME_TAC;
823 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`]
827 THEN POP_ASSUM MP_TAC
828 THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `];
830 ASM_REWRITE_TAC[Geomdetail.CARD_SING]
833 let SCS_3T4_IS_SCS=prove_by_refinement(`is_scs_v39 scs_3T4`,
835 SIMP_TAC[scs_3T4;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.2759 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
836 THEN REPEAT RESA_TAC;
839 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
842 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
845 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
848 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
851 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
854 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
857 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
860 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
863 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
865 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
869 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
871 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
875 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
877 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
881 THEN REWRITE_TAC[h0;cstab]
887 THEN ASM_SIMP_TAC[MOD_LT;h0]
891 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
895 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
898 MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
899 (&2 * h0 < funlist_v39 [(0,1),&2 * h0] cstab 3 i (SUC i) \/
900 &2 < funlist_v39 [(0,1),&2] (&2 * h0) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`]
901 THEN MATCH_DICH_TAC 0
902 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
906 let SCS_3T5_IS_SCS=prove_by_refinement(`is_scs_v39 scs_3T5`,
908 SIMP_TAC[scs_3T5;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.103 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
909 THEN REPEAT RESA_TAC;
912 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
915 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
918 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
921 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
924 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
927 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
930 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
933 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
936 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
938 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
942 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
944 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
948 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
950 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
954 THEN REWRITE_TAC[h0;cstab]
955 THEN MP_TAC LE_sqrt8_2h0
961 THEN ASM_SIMP_TAC[MOD_LT;h0]
965 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
966 THEN MP_TAC sqrt8_LE_CSTAB
972 MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
973 (&2 * h0 < funlist_v39 [(0,1),sqrt8] (&2 * h0) 3 i (SUC i) \/
974 &2 < funlist_v39 [(0,1),&2 * h0] (&2) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`]
975 THEN MATCH_DICH_TAC 0
976 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
982 let SCS_3T6_IS_SCS=prove_by_refinement(`is_scs_v39 scs_3T6'`,
984 SIMP_TAC[scs_3T6;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.4348 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
985 THEN REPEAT RESA_TAC;
987 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
989 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
991 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
993 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
995 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
997 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
999 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1001 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1003 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
1005 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1008 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
1010 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1013 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
1015 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1018 THEN REWRITE_TAC[h0;cstab]
1019 THEN MP_TAC sqrt8_LE_CSTAB
1020 THEN REAL_ARITH_TAC;
1023 THEN ASM_SIMP_TAC[MOD_LT;h0]
1024 THEN MP_TAC LE_sqrt8_2
1025 THEN REAL_ARITH_TAC;
1027 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
1028 THEN REAL_ARITH_TAC;
1030 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
1031 THEN REAL_ARITH_TAC;
1032 MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
1033 (&2 * h0 < funlist_v39 [(0,1),cstab; (1,2),cstab] (&2 * h0) 3 i (SUC i) \/
1034 &2 < funlist_v39 [(0,1),sqrt8; (1,2),sqrt8] (&2) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`]
1035 THEN MATCH_DICH_TAC 0
1036 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
1041 let SCS_3T1_prime_IS_SCS=prove_by_refinement(`is_scs_v39 scs_3T1_prime`,
1042 [SIMP_TAC[scs_3T1_prime;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.11 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
1043 THEN REPEAT RESA_TAC;
1047 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1051 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1055 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1058 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1061 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1064 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1067 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1070 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1073 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
1075 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1079 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
1081 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1085 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
1087 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1091 THEN REWRITE_TAC[h0;cstab]
1092 THEN REAL_ARITH_TAC;
1097 THEN ASM_SIMP_TAC[MOD_LT;h0;cstab]
1098 THEN REAL_ARITH_TAC;
1101 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
1102 THEN REAL_ARITH_TAC;
1105 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
1106 THEN REAL_ARITH_TAC;
1108 MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
1109 (&2 * h0 < funlist_v39 [(0,1),cstab] (&2 * h0) 3 i (SUC i) \/
1110 &2 < funlist_v39 [(0,1),cstab] (&2) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`]
1111 THEN MATCH_DICH_TAC 0
1112 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
1117 let SCS_3T1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_3T1`,
1119 SIMP_TAC[scs_3T1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.11 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
1120 THEN REPEAT RESA_TAC;
1124 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1128 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1132 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1135 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1138 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1141 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1144 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1147 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1150 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
1152 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1156 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
1158 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1162 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
1164 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1168 THEN REWRITE_TAC[h0;cstab]
1169 THEN MP_TAC sqrt8_LE_CSTAB
1170 THEN REAL_ARITH_TAC;
1175 THEN ASM_SIMP_TAC[MOD_LT;h0;cstab]
1176 THEN MP_TAC LE_sqrt8_2
1177 THEN REAL_ARITH_TAC;
1180 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
1181 THEN REAL_ARITH_TAC;
1184 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
1185 THEN REAL_ARITH_TAC;
1187 MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
1188 (&2 * h0 < funlist_v39 [(0,1),cstab] (&2 * h0) 3 i (SUC i) \/
1189 &2 < funlist_v39 [(0,1),sqrt8] (&2) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`]
1190 THEN MATCH_DICH_TAC 0
1191 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
1197 let SCS_3T4_prime_IS_SCS=prove_by_refinement( `is_scs_v39 scs_3T4_prime`,
1198 [SIMP_TAC[scs_3T4_prime;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ 3<=3/\ ~(6=0)`;d_tame;REAL_ARITH`#0.2759 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
1199 THEN REPEAT RESA_TAC;
1202 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1205 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1208 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1211 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1214 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1217 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1220 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1223 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
1226 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
1228 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1232 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
1234 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1238 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
1240 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1244 THEN REWRITE_TAC[h0;cstab]
1245 THEN REAL_ARITH_TAC;
1250 THEN ASM_SIMP_TAC[MOD_LT;h0;cstab]
1251 THEN REAL_ARITH_TAC;
1254 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
1255 THEN REAL_ARITH_TAC;
1258 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
1259 THEN REAL_ARITH_TAC;
1261 MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
1262 (&2 * h0 < funlist_v39 [(0,1),&2 * h0] cstab 3 i (SUC i) \/
1263 &2 < funlist_v39 [(0,1),&2; (1,2),cstab] (&2 * h0) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`]
1264 THEN MATCH_DICH_TAC 0
1265 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
1269 let SCS_4M6_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M6'`,
1271 SIMP_TAC[scs_4M6;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
1272 THEN REPEAT RESA_TAC;
1275 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1278 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1281 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1284 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1287 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1290 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1293 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1296 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1299 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1301 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1305 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1307 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1312 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1314 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1319 THEN REWRITE_TAC[h0;cstab]
1320 THEN REAL_ARITH_TAC;
1323 THEN REWRITE_TAC[h0;cstab]
1324 THEN REAL_ARITH_TAC;
1327 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
1328 THEN REAL_ARITH_TAC;
1334 THEN ASM_SIMP_TAC[h0;cstab;]
1335 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1336 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1337 THEN REAL_ARITH_TAC;
1341 THEN ASM_SIMP_TAC[h0;cstab;]
1342 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1343 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
1344 THEN SUBGOAL_THEN`{i | i < 4 /\
1345 (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/
1346 &2 < (if psort 4 (i,SUC i) = 0,1 then &2 * #1.26 else &2))} ={0}`ASSUME_TAC
1349 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`]
1353 THEN POP_ASSUM MP_TAC
1354 THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT];
1356 ASM_REWRITE_TAC[Geomdetail.CARD_SING]
1363 let SCS_4M5_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M5'`,
1365 SIMP_TAC[scs_4M5;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
1366 THEN REPEAT RESA_TAC;
1370 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1374 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1378 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1382 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1386 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1390 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1394 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1398 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1402 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1404 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1409 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1411 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1417 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1419 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1425 THEN REWRITE_TAC[h0;cstab]
1426 THEN REAL_ARITH_TAC;
1430 THEN REWRITE_TAC[h0;cstab]
1431 THEN REAL_ARITH_TAC;
1435 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
1436 THEN REAL_ARITH_TAC;
1444 THEN ASM_SIMP_TAC[h0;cstab;]
1445 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1446 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1447 THEN REAL_ARITH_TAC;
1452 THEN ASM_SIMP_TAC[h0;cstab;]
1453 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1454 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
1455 THEN SUBGOAL_THEN`{i | i < 4 /\
1457 (if psort 4 (i,SUC i) = 0,1
1459 else if psort 4 (i,SUC i) = 2,3 then #3.01 else &2 * #1.26) \/
1461 (if psort 4 (i,SUC i) = 0,1
1463 else if psort 4 (i,SUC i) = 2,3 then &2 * #1.26 else &2))} ={0,2}`ASSUME_TAC
1467 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`]
1471 THEN POP_ASSUM MP_TAC
1472 THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT;SET_RULE`a IN {b,c} <=> (a=b\/ a=c)`]
1475 THEN REAL_ARITH_TAC;
1478 ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=2)`]
1484 let SCS_4M6_prime_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M6_prime`,
1486 SIMP_TAC[scs_4M6_prime;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
1487 THEN REPEAT RESA_TAC;
1490 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1493 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1496 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1499 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1502 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1505 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1508 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1511 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1514 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1516 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1520 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1522 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1527 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1529 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1534 THEN REWRITE_TAC[h0;cstab]
1535 THEN REAL_ARITH_TAC;
1538 THEN REWRITE_TAC[h0;cstab]
1539 THEN REAL_ARITH_TAC;
1542 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
1543 THEN REAL_ARITH_TAC;
1549 THEN ASM_SIMP_TAC[h0;cstab;]
1550 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1551 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1552 THEN REAL_ARITH_TAC;
1556 THEN ASM_SIMP_TAC[h0;cstab;]
1557 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1558 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
1559 THEN SUBGOAL_THEN`{i | i < 4 /\
1560 (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/
1561 &2 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2))} ={0}`ASSUME_TAC
1564 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`]
1568 THEN POP_ASSUM MP_TAC
1569 THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT];
1571 ASM_REWRITE_TAC[Geomdetail.CARD_SING]
1576 let SCS_4M4_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M4'`,
1579 SIMP_TAC[scs_4M4;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
1580 THEN REPEAT RESA_TAC;
1583 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1586 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1589 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1592 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1595 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1598 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1601 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1604 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1607 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1609 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1613 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1615 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1620 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1622 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1627 THEN REWRITE_TAC[h0;cstab]
1628 THEN REAL_ARITH_TAC;
1631 THEN REWRITE_TAC[h0;cstab]
1632 THEN REAL_ARITH_TAC;
1635 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
1636 THEN REAL_ARITH_TAC;
1642 THEN ASM_SIMP_TAC[h0;cstab;]
1643 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1644 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1645 THEN REAL_ARITH_TAC;
1649 THEN ASM_SIMP_TAC[h0;cstab;]
1650 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1651 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
1652 THEN SUBGOAL_THEN`{i | i < 4 /\
1654 (if psort 4 (i,SUC i) = 0,1
1656 else if psort 4 (i,SUC i) = 1,2 then #3.01 else &2 * #1.26) \/
1658 (if psort 4 (i,SUC i) = 0,1
1660 else if psort 4 (i,SUC i) = 1,2 then &2 * #1.26 else &2))} ={0,1}`ASSUME_TAC
1663 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`]
1667 THEN POP_ASSUM MP_TAC
1668 THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT;SET_RULE`a IN {b,c} <=> (a=b\/ a=c)`]
1671 THEN REAL_ARITH_TAC;
1673 ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=1)`]
1677 let SCS_4M3_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M3'`,
1680 SIMP_TAC[scs_4M3;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
1681 THEN REPEAT RESA_TAC;
1684 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1687 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1690 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1693 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1696 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1699 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1702 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1705 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1708 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1710 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1714 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1716 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1721 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1723 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1728 THEN REWRITE_TAC[h0;cstab]
1729 THEN MP_TAC sqrt8_LE_6
1730 THEN MP_TAC sqrt8_LE_CSTAB
1731 THEN REAL_ARITH_TAC;
1734 THEN REWRITE_TAC[h0;cstab]
1735 THEN REAL_ARITH_TAC;
1738 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
1739 THEN MP_TAC LE_sqrt8_2
1740 THEN REAL_ARITH_TAC;
1746 THEN ASM_SIMP_TAC[h0;cstab;]
1747 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1748 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1749 THEN REAL_ARITH_TAC;
1753 THEN ASM_SIMP_TAC[h0;cstab;]
1754 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1755 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
1756 THEN SUBGOAL_THEN`{i | i < 4 /\
1757 (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/
1758 &2 < (if psort 4 (i,SUC i) = 0,1 then sqrt8 else &2))} ={0}`ASSUME_TAC
1761 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`]
1765 THEN POP_ASSUM MP_TAC
1766 THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT];
1768 ASM_REWRITE_TAC[Geomdetail.CARD_SING]
1778 let SCS_4M7_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M7`,
1780 SIMP_TAC[scs_4M7;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
1781 THEN REPEAT RESA_TAC;
1784 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1787 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1790 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1793 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1796 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1799 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1802 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1805 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1808 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1810 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1814 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1816 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1821 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1823 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1828 THEN REWRITE_TAC[h0;cstab]
1829 THEN REAL_ARITH_TAC;
1832 THEN REWRITE_TAC[h0;cstab]
1833 THEN REAL_ARITH_TAC;
1836 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
1837 THEN REAL_ARITH_TAC;
1843 THEN ASM_SIMP_TAC[h0;cstab;]
1844 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1845 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1846 THEN REAL_ARITH_TAC;
1850 THEN ASM_SIMP_TAC[h0;cstab;]
1851 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1852 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
1853 THEN SUBGOAL_THEN`{i | i < 4 /\
1855 (if psort 4 (i,SUC i) = 0,1
1857 else if psort 4 (i,SUC i) = 1,2 then #3.01 else &2 * #1.26) \/
1859 (if psort 4 (i,SUC i) = 0,1
1861 else if psort 4 (i,SUC i) = 1,2 then &2 * #1.26 else &2))} ={0,1}`ASSUME_TAC
1864 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`]
1868 THEN POP_ASSUM MP_TAC
1869 THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT;SET_RULE`a IN {b,c} <=> a=b\/ a=c`]
1871 THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT;SET_RULE`a IN {b,c} <=> a=b\/ a=c`]
1875 ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=1)`]
1882 let SCS_4M7_prime_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M7_prime`,
1884 SIMP_TAC[scs_4M7_prime;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
1885 THEN REPEAT RESA_TAC;
1888 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1891 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1894 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1897 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1900 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1903 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1906 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1909 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1912 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1914 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1918 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1920 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1925 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
1927 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1932 THEN REWRITE_TAC[h0;cstab]
1933 THEN REAL_ARITH_TAC;
1936 THEN REWRITE_TAC[h0;cstab]
1937 THEN REAL_ARITH_TAC;
1940 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
1941 THEN REAL_ARITH_TAC;
1947 THEN ASM_SIMP_TAC[h0;cstab;]
1948 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1949 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1950 THEN REAL_ARITH_TAC;
1954 THEN ASM_SIMP_TAC[h0;cstab;]
1955 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
1956 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
1957 THEN SUBGOAL_THEN`{i | i < 4 /\
1959 (if psort 4 (i,SUC i) = 0,1
1961 else if psort 4 (i,SUC i) = 1,2 then #3.01 else &2 * #1.26) \/
1963 (if psort 4 (i,SUC i) = 0,1
1965 else if psort 4 (i,SUC i) = 1,2 then &2 * #1.26 else &2))} ={0,1}`ASSUME_TAC
1968 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`]
1972 THEN POP_ASSUM MP_TAC
1973 THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT;SET_RULE`a IN {b,c} <=> a=b\/ a=c`]
1975 THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT;SET_RULE`a IN {b,c} <=> a=b\/ a=c`]
1979 ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=1)`]
1984 let SCS_4M8_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M8`,
1986 SIMP_TAC[scs_4M8;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
1987 THEN REPEAT RESA_TAC;
1990 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1993 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1996 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
1999 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
2002 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
2005 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
2008 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
2011 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
2014 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
2016 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
2020 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
2022 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
2027 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
2029 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
2034 THEN REWRITE_TAC[h0;cstab]
2035 THEN REAL_ARITH_TAC;
2038 THEN REWRITE_TAC[h0;cstab]
2039 THEN REAL_ARITH_TAC;
2042 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
2043 THEN REAL_ARITH_TAC;
2049 THEN ASM_SIMP_TAC[h0;cstab;]
2050 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
2051 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
2052 THEN REAL_ARITH_TAC;
2056 THEN ASM_SIMP_TAC[h0;cstab;]
2057 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
2058 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
2059 THEN SUBGOAL_THEN`{i | i < 4 /\
2061 (if psort 4 (i,SUC i) = 0,1
2063 else if psort 4 (i,SUC i) = 2,3 then #3.01 else &2 * #1.26) \/
2065 (if psort 4 (i,SUC i) = 0,1
2067 else if psort 4 (i,SUC i) = 2,3 then &2 * #1.26 else &2))} ={0,2}`ASSUME_TAC
2070 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`]
2074 THEN POP_ASSUM MP_TAC
2075 THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT;SET_RULE`a IN {b,c} <=> a=b\/ a=c`]
2077 THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT;SET_RULE`a IN {b,c} <=> a=b\/ a=c`]
2081 ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=2)`]
2088 let SCS_4M8_prime_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M8_prime`,
2091 SIMP_TAC[scs_4M8_prime;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<=4/\ 4<=6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.513 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
2092 THEN REPEAT RESA_TAC;
2095 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
2098 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
2101 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
2104 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
2107 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
2110 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
2113 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
2116 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
2119 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
2121 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
2125 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
2127 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
2132 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
2134 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
2139 THEN REWRITE_TAC[h0;cstab]
2140 THEN REAL_ARITH_TAC;
2143 THEN REWRITE_TAC[h0;cstab]
2144 THEN REAL_ARITH_TAC;
2147 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
2148 THEN REAL_ARITH_TAC;
2154 THEN ASM_SIMP_TAC[h0;cstab;]
2155 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
2156 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
2157 THEN REAL_ARITH_TAC;
2161 THEN ASM_SIMP_TAC[h0;cstab;]
2162 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
2163 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
2164 THEN SUBGOAL_THEN`{i | i < 4 /\
2166 (if psort 4 (i,SUC i) = 0,1
2168 else if psort 4 (i,SUC i) = 2,3 then #3.01 else &2 * #1.26) \/
2170 (if psort 4 (i,SUC i) = 0,1
2172 else if psort 4 (i,SUC i) = 2,3 then #3.01 else &2))} ={0,2}`ASSUME_TAC
2175 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`]
2179 THEN POP_ASSUM MP_TAC
2180 THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT;SET_RULE`a IN {b,c} <=> a=b\/ a=c`]
2182 THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `;PSORT_5_EXPLICIT;SET_RULE`a IN {b,c} <=> a=b\/ a=c`]
2186 ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=2)`]
2195 (****************************)
2197 let SCS_5M3_BASIC=prove(`scs_basic_v39 scs_5M3`,
2200 let SCS_5T1_BASIC=prove(`scs_basic_v39 scs_5T1`,
2205 let SCS_4M6_prime_BASIC=prove(`scs_basic_v39 scs_4M6_prime`,
2208 let SCS_4M7_prime_BASIC=prove(`scs_basic_v39 scs_4M7_prime`,
2211 let SCS_4M4_BASIC=prove(`scs_basic_v39 scs_4M4'`,
2215 let SCS_4M7_BASIC=prove(`scs_basic_v39 scs_4M7`,
2218 let SCS_4M3_BASIC=prove(`scs_basic_v39 scs_4M3'`,
2221 let SCS_4M5_BASIC=prove(`scs_basic_v39 scs_4M5'`,
2224 let SCS_3T4_prime_BASIC=prove(`scs_basic_v39 scs_3T4_prime`,
2227 let SCS_3T6_BASIC=prove(`scs_basic_v39 scs_3T6'`,
2231 let SCS_3T1_prime_BASIC=prove(`scs_basic_v39 scs_3T1_prime`,
2234 let SCS_3T5_BASIC=prove(`scs_basic_v39 scs_3T5`,
2238 let SCS_4M8_prime_BASIC=prove(`scs_basic_v39 scs_4M8_prime`,
2242 let SCS_4M8_BASIC=prove(`scs_basic_v39 scs_4M8`,
2246 let K_SCS_5M3=prove(`scs_k_v39 scs_5M3=5`,
2249 let K_SCS_5T1=prove(`scs_k_v39 scs_5T1=5`,
2252 let K_SCS_3T4_prime=prove(`scs_k_v39 scs_3T4_prime=3`,
2255 let K_SCS_3T5=prove(`scs_k_v39 scs_3T5=3`,
2258 let K_SCS_3T6=prove(`scs_k_v39 scs_3T6'=3`,
2261 let K_SCS_4M4=prove(`scs_k_v39 scs_4M4'=4`,
2264 let K_SCS_4M5=prove(`scs_k_v39 scs_4M5'=4`,
2267 let K_SCS_4M3=prove(`scs_k_v39 scs_4M3'=4`,
2270 let K_SCS_4M6_prime=prove(`scs_k_v39 scs_4M6_prime=4`,
2273 let K_SCS_3T1_prime=prove(`scs_k_v39 scs_3T1_prime=3`,
2277 let K_SCS_4M7_prime=prove(`scs_k_v39 scs_4M7_prime=4`,
2280 let K_SCS_4M7=prove(`scs_k_v39 scs_4M7=4`,
2284 let K_SCS_4M8_prime=prove(`scs_k_v39 scs_4M8_prime=4`,
2287 let K_SCS_4M8=prove(`scs_k_v39 scs_4M8=4`,
2291 let J_SCS_5M3=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5M3 i) i1 j= F`,
2294 let J_SCS_5T1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5T1 i) i1 j= F`,
2298 let J_SCS_3T4_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T4_prime i) i1 j= F`,
2302 let J_SCS_4M4=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M4' i) i1 j= F`,
2306 let J_SCS_4M3=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M3' i) i1 j= F`,
2309 let J_SCS_4M5=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M5' i) i1 j= F`,
2312 let J_SCS_4M6_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M6_prime i) i1 j= F`,
2315 let J_SCS_5M2=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5M2 i) i1 j= F`,
2318 let J_SCS_3T1_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T1_prime i) i1 j= F`,
2321 let J_SCS_3T1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T1 i) i1 j= F`,
2324 let J_SCS_3T6=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T6' i) i1 j= F`,
2327 let J_SCS_3T5=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T5 i) i1 j= F`,
2331 let J_SCS_4M7_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M7_prime i) i1 j= F`,
2334 let J_SCS_4M7=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M7 i) i1 j= F`,
2337 let J_SCS_4M8_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M8_prime i) i1 j= F`,
2340 let J_SCS_4M8=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M8 i) i1 j= F`,
2343 let J_SCS_4M8_prime1=prove(`scs_J_v39 (scs_4M8_prime ) i1 j= F`,
2349 let STAB_5I1_SCS=prove(` scs_diag (scs_k_v39 scs_5I1) i j
2350 ==> is_scs_v39 (scs_stab_diag_v39 scs_5I1 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5I1 i j)`,
2352 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
2353 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5I1_IS_SCS;SCS_5I1_BASIC;K_SCS_5I1;
2354 ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
2356 THEN REWRITE_TAC[h0;cstab]
2357 THEN REAL_ARITH_TAC);;
2360 let STAB_5I2_SCS=prove(` scs_diag (scs_k_v39 scs_5I2) i j
2361 ==> is_scs_v39 (scs_stab_diag_v39 scs_5I2 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5I2 i j)`,
2363 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
2364 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5I2_IS_SCS;SCS_5I2_BASIC;K_SCS_5I2;
2365 ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
2367 THEN REWRITE_TAC[h0;cstab]
2368 THEN MP_TAC sqrt8_LE_CSTAB
2369 THEN REAL_ARITH_TAC);;
2372 let STAB_5M3_SCS=prove(` scs_diag (scs_k_v39 scs_5M3) i j
2373 ==> is_scs_v39 (scs_stab_diag_v39 scs_5M3 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5M3 i j)`,
2375 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
2376 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5M3_IS_SCS;SCS_5M3_BASIC;K_SCS_5M3;
2377 ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
2379 THEN REWRITE_TAC[h0;cstab]
2380 THEN REAL_ARITH_TAC);;
2383 let STAB_5T1_SCS=prove(` scs_diag (scs_k_v39 scs_5T1) i j
2384 ==> is_scs_v39 (scs_stab_diag_v39 scs_5T1 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5T1 i j)`,
2386 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
2387 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5T1_IS_SCS;SCS_5T1_BASIC;K_SCS_5T1;
2388 ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
2390 THEN REWRITE_TAC[h0;cstab]
2391 THEN REAL_ARITH_TAC);;
2394 (*****************************)
2396 let SCS_5M3_STAB_DIAG_sqrt8=prove_by_refinement(`BBs_v39 scs_5M2 v/\
2398 dist(v i,v j) <= cstab/\
2399 sqrt8 <= dist(v 0, v(1))
2401 BBs_v39 ((scs_stab_diag_v39 scs_5M3 i j) ) v`,
2403 THEN REPEAT STRIP_TAC
2406 THEN POP_ASSUM(fun th-> ASSUME_TAC th
2409 REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_5M3;scs_5M2;CS_ADJ;scs_diag;ARITH_RULE`~(5<=3)`;IN;K_SCS_5M3;scs_prop_equ_v39;]
2410 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
2412 THEN REPEAT RESA_TAC
2414 THEN MP_TAC(SET_RULE`i' MOD 5= j' MOD 5\/ ~(i' MOD 5= j' MOD 5)`)
2417 THAYTHE_TAC (8-6)[`i'`;`j'`]
2419 THEN REWRITE_TAC[cstab]
2420 THEN REAL_ARITH_TAC;
2422 MP_TAC(SET_RULE`psort 5 (i',j') = 0,1\/ ~(psort 5 (i',j') = 0,1)`)
2425 MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`1`;`j'`;`0`;`5`][PSORT_5_EXPLICIT];
2427 MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
2428 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
2430 THEN MP_TAC LE_sqrt8_2h0
2431 THEN REWRITE_TAC[h0]
2432 THEN REAL_ARITH_TAC;
2434 MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` 1`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
2435 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` 0`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
2436 THEN ONCE_REWRITE_TAC[DIST_SYM]
2438 THEN MP_TAC LE_sqrt8_2h0
2439 THEN REWRITE_TAC[h0]
2440 THEN REAL_ARITH_TAC;
2442 THAYTHE_TAC (9-6)[`i'`;`j'`]
2445 THEN REWRITE_TAC[cstab;h0];
2447 THAYTHE_TAC (8-6)[`i'`;`j'`]
2449 THEN REWRITE_TAC[cstab]
2450 THEN REAL_ARITH_TAC;
2452 MP_TAC(SET_RULE`psort 5 (i,j) = psort 5 (i',j')\/ ~(psort 5 (i,j) = psort 5 (i',j'))`)
2455 MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`j`;`j'`;`i`;`5`][PSORT_5_EXPLICIT];
2457 MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
2458 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`];
2460 MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
2461 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j':num`;`v`;` i`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`]
2462 THEN ONCE_REWRITE_TAC[DIST_SYM]
2463 THEN ASM_REWRITE_TAC[];
2465 THAYTHE_TAC(9-6)[`i'`;`j'`]
2470 let SCS_DIAG_SCS_5M3_02=prove(`scs_diag (scs_k_v39 scs_5M3) 0 2`,
2471 REWRITE_TAC[K_SCS_5M3;scs_diag]
2474 let SCS_DIAG_SCS_5M3_03=prove(`scs_diag (scs_k_v39 scs_5M3) 0 3`,
2475 REWRITE_TAC[K_SCS_5M3;scs_diag]
2478 let SCS_DIAG_SCS_5M3_24=prove(`scs_diag (scs_k_v39 scs_5M3) 2 4`,
2479 REWRITE_TAC[K_SCS_5M3;scs_diag]
2483 let MM_5M2_IMP_MM_STAB_5M3=prove(
2484 ` MMs_v39 scs_5M2 v /\
2486 dist(v i,v j) <= cstab/\
2487 sqrt8<= dist(v l, v(l+1))
2489 ~(MMs_v39 (scs_stab_diag_v39 scs_5M3 i j)= {})`,
2491 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2492 THEN EXISTS_TAC`v:num->real^3`
2493 THEN EXISTS_TAC`scs_5M2`
2494 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`]
2495 THEN ASSUME_TAC SCS_5M2_BASIC
2496 THEN ASSUME_TAC K_SCS_5M2
2497 THEN ASM_SIMP_TAC[SCS_5M2_IS_SCS;STAB_5M3_SCS;K_SCS_5M3;SCS_K_D_A_STAB_EQ;IN; ADD1]
2498 THEN MP_TAC SCS_5M2_EDGE_LE_2H0_IMP_0
2499 THEN ASM_REWRITE_TAC[ ADD1;h0]
2500 THEN MP_TAC LT_sqrt8_2h0
2502 THEN MP_TAC(REAL_ARITH`sqrt8 <= dist ((v:num->real^3) l,v (l + 1))/\ &2 * #1.26 < sqrt8==> &2 * #1.26 < dist (v l,v (l + 1))`)
2506 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l:num`;`v`;` l MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`]
2507 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`l+1:num`;`v`;` (l+1) MOD 5`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)/\ 0 MOD 5=0`]
2508 THEN MRESAL_TAC MOD_ADD_MOD[`l`;`1`;`5`][ARITH_RULE`~(5=0)/\ 1 MOD 5=1/\ 0+a=a`] THEN SYM_ASSUM_TAC
2510 THEN MP_TAC SCS_5M3_STAB_DIAG_sqrt8
2513 THEN REAL_ARITH_TAC);;
2519 let STAB_5M3_SCS=prove(` scs_diag (scs_k_v39 scs_5M3) i j
2520 ==> is_scs_v39 (scs_stab_diag_v39 scs_5M3 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_5M3 i j)`,
2522 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
2523 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_5M3_IS_SCS;SCS_5M3_BASIC;K_SCS_5M3;
2524 ARITH_RULE`3<5`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
2526 THEN REWRITE_TAC[h0;cstab]
2527 THEN REAL_ARITH_TAC);;
2530 let BB_3T4_prime_IMP_scs_3T4=prove(`BBs_v39 scs_3T4_prime v
2532 BBs_v39 (scs_3T4 ) v`,
2533 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`(3<=3)`;IN;K_SCS_3T4;K_SCS_3T4_prime;scs_prop_equ_v39;]
2534 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
2536 THEN REPEAT RESA_TAC
2537 THEN THAYTHE_TAC 0[`i`;`j`]
2539 THEN REWRITE_TAC[cstab;h0]
2540 THEN REAL_ARITH_TAC);;
2543 let MM_3T4_prime_IMP_MM_3T4=prove(`MMs_v39 scs_3T4_prime v ==> ~(MMs_v39 scs_3T4={})`,
2545 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2546 THEN EXISTS_TAC`v:num->real^3`
2547 THEN EXISTS_TAC`scs_3T4_prime`
2548 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_3T4_prime`;`v`]
2549 THEN ASM_SIMP_TAC[SCS_3T4_BASIC;SCS_3T4_prime_BASIC;SCS_3T4_IS_SCS;SCS_3T4_IS_SCS;
2550 SCS_3T4_prime_IS_SCS;K_SCS_3T4;K_SCS_3T4_prime;IN;BB_3T4_prime_IMP_scs_3T4]
2552 THEN REAL_ARITH_TAC);;
2555 let SCS_3T4_prime_ARROW_MM_3T4=prove_by_refinement(`scs_arrow_v39 {scs_3T4_prime } { scs_3T4}`,
2557 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
2558 THEN ABBREV_TAC`k=scs_k_v39 s`
2559 THEN REPEAT RESA_TAC;
2561 ASM_SIMP_TAC[SCS_3T4_IS_SCS];
2563 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_3T4_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_3T4_prime ==> MMs_v39 s = {}))`);
2568 THEN POP_ASSUM MP_TAC
2569 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
2570 THEN REPEAT STRIP_TAC
2571 THEN POP_ASSUM MP_TAC
2573 THEN EXISTS_TAC`scs_3T4`
2574 THEN ASM_REWRITE_TAC[]
2575 THEN MATCH_MP_TAC (GEN_ALL MM_3T4_prime_IMP_MM_3T4)
2576 THEN POP_ASSUM MP_TAC
2580 let BB_4M6_prime_IMP_scs_4M6=prove(`BBs_v39 scs_4M6_prime v
2582 BBs_v39 (scs_4M6' ) v`,
2583 REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4M6_prime;K_SCS_4M6;scs_prop_equ_v39;]
2584 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
2586 THEN REPEAT RESA_TAC
2587 THEN THAYTHE_TAC 1[`i`;`j`]
2589 THEN REWRITE_TAC[cstab;h0]
2590 THEN REAL_ARITH_TAC);;
2601 let MM_4M6_prime_IMP_MM_4M6=prove(`MMs_v39 scs_4M6_prime v ==> ~(MMs_v39 scs_4M6' ={})`,
2603 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2604 THEN EXISTS_TAC`v:num->real^3`
2605 THEN EXISTS_TAC`scs_4M6_prime`
2606 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M6_prime`;`v`]
2607 THEN ASM_SIMP_TAC[SCS_4M6_BASIC;SCS_4M6_prime_BASIC;SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;
2608 SCS_4M6_prime_IS_SCS;K_SCS_4M6;K_SCS_4M6_prime;IN;BB_4M6_prime_IMP_scs_4M6]
2610 THEN REAL_ARITH_TAC);;
2614 let SCS_4M6_prime_ARROW_MM_4M6=prove_by_refinement(`scs_arrow_v39 {scs_4M6_prime } { scs_4M6'}`,
2616 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
2617 THEN ABBREV_TAC`k=scs_k_v39 s`
2618 THEN REPEAT RESA_TAC;
2620 ASM_SIMP_TAC[SCS_4M6_IS_SCS];
2622 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M6_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M6_prime ==> MMs_v39 s = {}))`);
2627 THEN POP_ASSUM MP_TAC
2628 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
2629 THEN REPEAT STRIP_TAC
2630 THEN POP_ASSUM MP_TAC
2632 THEN EXISTS_TAC`scs_4M6'`
2633 THEN ASM_REWRITE_TAC[]
2634 THEN MATCH_MP_TAC (GEN_ALL MM_4M6_prime_IMP_MM_4M6)
2635 THEN POP_ASSUM MP_TAC
2640 let SCS_5M3_SLICE_02=prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 0 2 } { scs_prop_equ_v39 scs_3T4_prime 2, scs_prop_equ_v39 scs_4M6_prime 1}`,
2642 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
2643 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_02;STAB_5M3_SCS;SCS_K_D_A_STAB_EQ;]
2646 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_02]
2647 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
2648 THEN REPEAT RESA_TAC;
2650 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
2652 THEN MATCH_MP_TAC scs_inj
2653 THEN ASM_SIMP_TAC[SCS_5M3_BASIC;SCS_3T4_prime_BASIC;J_SCS_4M6_prime;BASIC_HALF_SLICE_STAB;J_SCS_3T4_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4M6_prime_BASIC]
2656 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M6;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M3]
2661 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_5M3;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2;scs_3T4_prime;scs_5M3;
2662 ARITH_RULE`(2 + 1 + 5 - 0) MOD 5= 3/\ 0 MOD 5=0/\ a+0=a`;scs_prop_equ_v39]
2663 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2664 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2667 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
2668 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
2670 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
2671 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
2673 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2674 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
2675 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
2676 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
2677 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
2678 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
2679 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
2680 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
2682 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2683 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2684 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2685 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2686 THEN REPEAT RESA_TAC
2687 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
2688 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
2689 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
2690 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
2691 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2692 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
2696 ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M3;K_SCS_4M6_prime]
2701 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_5M3;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M6_prime;scs_3T4_prime;scs_5M3;
2702 ARITH_RULE`(0+1 + 5 - 2) MOD 5= 4/\ 2 MOD 5=2/\ a+0=a`;scs_prop_equ_v39]
2703 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2704 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2707 THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`)
2708 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION]
2710 THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/x' MOD 4=3`)
2711 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
2713 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2714 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
2715 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
2716 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
2717 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
2718 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
2719 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
2720 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
2721 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
2722 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
2724 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2725 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
2726 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2727 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2728 THEN REPEAT RESA_TAC
2729 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
2730 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
2731 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
2732 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
2733 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
2734 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+x:num`;`1+x':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2739 THEN REAL_ARITH_TAC;
2742 THEN REAL_ARITH_TAC;
2745 THEN REAL_ARITH_TAC;
2748 THEN REWRITE_TAC[cstab]
2749 THEN REAL_ARITH_TAC;
2752 THEN REWRITE_TAC[cstab]
2753 THEN REAL_ARITH_TAC;
2756 THEN REWRITE_TAC[J_SCS_3T4_prime]]);;
2759 let SCS_5M3_02_ARROW_3T4_4M6=prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 0 2 } {scs_3T4, scs_4M6'}`,
2760 [MATCH_MP_TAC FZIOTEF_TRANS
2761 THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_3T4_prime 2, scs_prop_equ_v39 scs_4M6_prime 1}`
2762 THEN ASM_REWRITE_TAC[SCS_5M3_SLICE_02;SET_RULE`{A,B}={A}UNION {B}`]
2763 THEN MATCH_MP_TAC FZIOTEF_UNION
2766 MATCH_MP_TAC FZIOTEF_TRANS
2767 THEN EXISTS_TAC`{scs_3T4_prime}`
2768 THEN ASM_REWRITE_TAC[SCS_3T4_prime_ARROW_MM_3T4]
2769 THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T4_prime`;`2`;`3`][SCS_3T4_prime_IS_SCS;K_SCS_3T4_prime;ARITH_RULE`(3 - 2 MOD 3)=1`]
2770 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T4_prime 2`;`1`][PROP_EQU_IS_SCS;SCS_3T4_prime_IS_SCS]
2772 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
2775 MATCH_MP_TAC FZIOTEF_TRANS
2776 THEN EXISTS_TAC`{scs_4M6_prime}`
2777 THEN ASM_REWRITE_TAC[SCS_4M6_prime_ARROW_MM_4M6]
2778 THEN MRESAS_TAC PRO_EQU_ID1[`scs_4M6_prime`;`1`;`4`][SCS_4M6_prime_IS_SCS;K_SCS_4M6_prime;ARITH_RULE`(4 - 1 MOD 4)=3`]
2779 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M6_prime 1`;`3`][PROP_EQU_IS_SCS;SCS_4M6_prime_IS_SCS]
2781 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
2782 THEN REWRITE_TAC[]]);;
2784 (************03***********)
2788 let SCS_5M3_SLICE_03=prove_by_refinement(
2789 `scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 0 3 } { scs_prop_equ_v39 scs_4M7_prime 1,scs_prop_equ_v39 scs_3T1_prime 1}`,
2792 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
2793 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_03;STAB_5M3_SCS;SCS_K_D_A_STAB_EQ;]
2796 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_03]
2797 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
2798 THEN REPEAT RESA_TAC;
2801 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
2803 THEN MATCH_MP_TAC scs_inj
2804 THEN ASM_SIMP_TAC[SCS_5M3_BASIC;SCS_3T1_prime_BASIC;J_SCS_4M7_prime;BASIC_HALF_SLICE_STAB;J_SCS_3T1_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4M7_prime_BASIC]
2808 ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_4M7_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M3]
2813 THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_5M3;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7_prime;scs_3T1_prime;scs_5M3;
2814 ARITH_RULE`(3+1 + 5 - 0) MOD 5= 4/\ 0 MOD 5=0/\ a+0=a`;scs_prop_equ_v39]
2815 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2816 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2819 THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`)
2820 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION]
2822 THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/x' MOD 4=3`)
2823 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
2825 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2826 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
2827 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
2828 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
2829 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
2830 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
2831 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
2832 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
2833 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
2834 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
2836 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2837 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
2838 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2839 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2840 THEN REPEAT RESA_TAC
2841 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
2842 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
2843 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
2844 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
2845 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
2846 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+x:num`;`1+x':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2851 ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T1_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M3;K_SCS_4M7_prime]
2856 THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_5M3;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;scs_3T1_prime;scs_5M3;
2857 ARITH_RULE`(0 + 1 + 5 - 3) MOD 5= 3/\ 3 MOD 5=3/\ a+0=a`;scs_prop_equ_v39]
2858 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2859 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2862 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
2863 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
2865 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
2866 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
2868 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2869 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
2870 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
2871 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
2872 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
2873 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
2874 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
2875 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
2877 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
2878 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2879 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2880 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2881 THEN REPEAT RESA_TAC
2882 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
2883 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
2884 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
2885 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
2886 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2887 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
2894 THEN REAL_ARITH_TAC;
2898 THEN REAL_ARITH_TAC;
2902 THEN REAL_ARITH_TAC;
2906 THEN REWRITE_TAC[cstab]
2907 THEN REAL_ARITH_TAC;
2911 THEN REWRITE_TAC[cstab]
2912 THEN REAL_ARITH_TAC;
2916 THEN REWRITE_TAC[J_SCS_4M7_prime];
2921 let BB_3T1_prime_IMP_scs_3T1=prove(
2922 `BBs_v39 scs_3T1_prime v
2924 BBs_v39 (scs_3T1 ) v`,
2925 REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`((3<=3))`;IN;K_SCS_3T1_prime;K_SCS_3T1;scs_prop_equ_v39;]
2926 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
2928 THEN REPEAT RESA_TAC
2929 THEN THAYTHE_TAC 0[`i`;`j`]
2931 THEN REWRITE_TAC[cstab;h0]
2932 THEN MP_TAC sqrt8_LE_CSTAB
2933 THEN REAL_ARITH_TAC);;
2936 let MM_3T1_prime_IMP_MM_3T1=prove(
2937 `MMs_v39 scs_3T1_prime v ==> ~(MMs_v39 scs_3T1 ={})`,
2939 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2940 THEN EXISTS_TAC`v:num->real^3`
2941 THEN EXISTS_TAC`scs_3T1_prime`
2942 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_3T1_prime`;`v`]
2943 THEN ASM_SIMP_TAC[SCS_3T1_BASIC;SCS_3T1_prime_BASIC;SCS_3T1_IS_SCS;SCS_3T1_IS_SCS;
2944 SCS_3T1_prime_IS_SCS;K_SCS_3T1;K_SCS_3T1_prime;IN;BB_3T1_prime_IMP_scs_3T1]
2946 THEN REAL_ARITH_TAC);;
2951 let SCS_3T1_prime_ARROW_MM_3T1=prove_by_refinement(`scs_arrow_v39 {scs_3T1_prime } { scs_3T1}`,
2953 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
2954 THEN ABBREV_TAC`k=scs_k_v39 s`
2955 THEN REPEAT RESA_TAC;
2957 ASM_SIMP_TAC[SCS_3T1_IS_SCS];
2959 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_3T1_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_3T1_prime ==> MMs_v39 s = {}))`);
2964 THEN POP_ASSUM MP_TAC
2965 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
2966 THEN REPEAT STRIP_TAC
2967 THEN POP_ASSUM MP_TAC
2969 THEN EXISTS_TAC`scs_3T1`
2970 THEN ASM_REWRITE_TAC[]
2971 THEN MATCH_MP_TAC (GEN_ALL MM_3T1_prime_IMP_MM_3T1)
2972 THEN POP_ASSUM MP_TAC
2978 let BB_4M7_prime_IMP_scs_4M7=prove(`BBs_v39 scs_4M7_prime v
2980 BBs_v39 (scs_4M7 ) v`,
2981 REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4M7_prime;K_SCS_4M7;scs_prop_equ_v39;]
2982 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
2984 THEN REPEAT RESA_TAC
2985 THEN THAYTHE_TAC 1[`i`;`j`]
2987 THEN REWRITE_TAC[cstab;h0]
2988 THEN REAL_ARITH_TAC);;
2992 let MM_4M7_prime_IMP_MM_4M7=prove(
2993 `MMs_v39 scs_4M7_prime v ==> ~(MMs_v39 scs_4M7 ={})`,
2995 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2996 THEN EXISTS_TAC`v:num->real^3`
2997 THEN EXISTS_TAC`scs_4M7_prime`
2998 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M7_prime`;`v`]
2999 THEN ASM_SIMP_TAC[SCS_4M7_BASIC;SCS_4M7_prime_BASIC;SCS_4M7_IS_SCS;SCS_4M7_IS_SCS;
3000 SCS_4M7_prime_IS_SCS;K_SCS_4M7;K_SCS_4M7_prime;IN;BB_4M7_prime_IMP_scs_4M7]
3002 THEN REAL_ARITH_TAC);;
3007 let SCS_4M7_prime_ARROW_MM_4M7=prove_by_refinement(`scs_arrow_v39 {scs_4M7_prime } { scs_4M7}`,
3009 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
3010 THEN ABBREV_TAC`k=scs_k_v39 s`
3011 THEN REPEAT RESA_TAC;
3013 ASM_SIMP_TAC[SCS_4M7_IS_SCS];
3015 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M7_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M7_prime ==> MMs_v39 s = {}))`);
3020 THEN POP_ASSUM MP_TAC
3021 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
3022 THEN REPEAT STRIP_TAC
3023 THEN POP_ASSUM MP_TAC
3025 THEN EXISTS_TAC`scs_4M7`
3026 THEN ASM_REWRITE_TAC[]
3027 THEN MATCH_MP_TAC (GEN_ALL MM_4M7_prime_IMP_MM_4M7)
3028 THEN POP_ASSUM MP_TAC
3032 let SCS_5M3_03_ARROW_3T1_4M7=prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 0 3 } { scs_4M7,scs_3T1}`,
3034 MATCH_MP_TAC FZIOTEF_TRANS
3035 THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_4M7_prime 1, scs_prop_equ_v39 scs_3T1_prime 1}`
3036 THEN ASM_REWRITE_TAC[SCS_5M3_SLICE_03;SET_RULE`{A,B}={A}UNION {B}`]
3037 THEN MATCH_MP_TAC FZIOTEF_UNION
3040 MATCH_MP_TAC FZIOTEF_TRANS
3041 THEN EXISTS_TAC`{scs_4M7_prime}`
3042 THEN ASM_REWRITE_TAC[SCS_4M7_prime_ARROW_MM_4M7]
3043 THEN MRESAS_TAC PRO_EQU_ID1[`scs_4M7_prime`;`1`;`4`][SCS_4M7_prime_IS_SCS;K_SCS_4M7_prime;ARITH_RULE`(4 - 1 MOD 4)=3`]
3044 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M7_prime 1`;`3`][PROP_EQU_IS_SCS;SCS_4M7_prime_IS_SCS]
3046 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
3049 MATCH_MP_TAC FZIOTEF_TRANS
3050 THEN EXISTS_TAC`{scs_3T1_prime}`
3051 THEN ASM_REWRITE_TAC[SCS_3T1_prime_ARROW_MM_3T1]
3052 THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T1_prime`;`1`;`3`][SCS_3T1_prime_IS_SCS;K_SCS_3T1_prime;ARITH_RULE`(3 - 1 MOD 3)=2`]
3053 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T1_prime 1`;`2`][PROP_EQU_IS_SCS;SCS_3T1_prime_IS_SCS]
3055 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
3056 THEN REWRITE_TAC[]]);;
3058 (*************24**************)
3061 let SCS_5M3_SLICE_24=prove_by_refinement(
3062 `scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 2 4 } {scs_prop_equ_v39 scs_3T1_prime 1,scs_prop_equ_v39 scs_4M8_prime 3}`,
3064 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
3065 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_24;STAB_5M3_SCS;SCS_K_D_A_STAB_EQ;]
3068 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M3_24]
3069 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
3070 THEN REPEAT RESA_TAC;
3072 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
3074 THEN MATCH_MP_TAC scs_inj
3075 THEN ASM_SIMP_TAC[SCS_5M3_BASIC;SCS_3T1_prime_BASIC;J_SCS_4M8_prime1;BASIC_HALF_SLICE_STAB;J_SCS_3T1_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4M8_prime_BASIC]
3078 ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T1_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M3]
3083 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_5M3;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;scs_3T1_prime;scs_5M3;
3084 ARITH_RULE`(4 + 1 + 5 - 2) MOD 5= 3/\ 2 MOD 5=2/\ a+0=a`;scs_prop_equ_v39]
3085 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3086 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3089 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
3090 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
3092 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
3093 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
3095 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3096 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
3097 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
3098 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
3099 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
3100 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
3101 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
3102 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
3104 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
3105 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3106 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3107 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
3108 THEN REPEAT RESA_TAC
3109 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
3110 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
3111 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
3112 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3113 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3114 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
3118 ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_4M8_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M3;K_SCS_4M8_prime]
3123 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_5M3;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_prime;scs_3T1_prime;scs_5M3;
3124 ARITH_RULE`(2+1 + 5 - 4) MOD 5= 4/\ 4 MOD 5=4/\ a+0=a`;scs_prop_equ_v39]
3125 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3126 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3129 THEN MP_TAC(ARITH_RULE`x MOD 4<4==> x MOD 4=0\/ x MOD 4=1\/ x MOD 4=2\/ x MOD 4=3`)
3130 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION]
3132 THEN MP_TAC(ARITH_RULE`x' MOD 4<4==> x' MOD 4=0\/ x' MOD 4=1\/ x' MOD 4=2\/x' MOD 4=3`)
3133 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
3135 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3136 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
3137 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`3`][ARITH_RULE`~(4=0)`]
3138 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`3`][ARITH_RULE`~(4=0)`]
3139 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`3`][ARITH_RULE`~(4=0)`]
3140 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`3`][ARITH_RULE`~(4=0)`]
3141 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`3`][ARITH_RULE`~(4=0)`]
3142 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`3`][ARITH_RULE`~(4=0)`]
3143 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`3`][ARITH_RULE`~(4=0)`]
3144 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`3`][ARITH_RULE`~(4=0)`]
3146 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
3147 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
3148 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3149 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
3150 THEN REPEAT RESA_TAC
3151 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
3152 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
3153 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
3154 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3155 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
3156 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`3+x:num`;`3+x':num`][ARITH_RULE`~(4=0)/\ 3+3=6/\ 3+1=4/\ 4 MOD 3=1/\ 2+4=6/\ 6 MOD 4=2/\ 3+4=7/\ 7 MOD 5=2`]
3161 THEN REAL_ARITH_TAC;
3164 THEN REAL_ARITH_TAC;
3167 THEN REAL_ARITH_TAC;
3170 THEN REWRITE_TAC[cstab]
3171 THEN REAL_ARITH_TAC;
3174 THEN REWRITE_TAC[cstab]
3175 THEN REAL_ARITH_TAC;
3178 THEN REWRITE_TAC[J_SCS_3T1_prime];
3183 let BB_4M8_prime_IMP_scs_4M8=prove(`BBs_v39 scs_4M8_prime v
3185 BBs_v39 (scs_4M8 ) v`,
3186 REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(4<=3))`;IN;K_SCS_4M8_prime;K_SCS_4M8;scs_prop_equ_v39;]
3187 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
3189 THEN REPEAT RESA_TAC
3190 THEN THAYTHE_TAC 1[`i`;`j`]
3192 THEN REWRITE_TAC[cstab;h0]
3193 THEN REAL_ARITH_TAC);;
3197 let MM_4M8_prime_IMP_MM_4M8=prove(
3198 `MMs_v39 scs_4M8_prime v ==> ~(MMs_v39 scs_4M8 ={})`,
3200 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
3201 THEN EXISTS_TAC`v:num->real^3`
3202 THEN EXISTS_TAC`scs_4M8_prime`
3203 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8_prime`;`v`]
3204 THEN ASM_SIMP_TAC[SCS_4M8_BASIC;SCS_4M8_prime_BASIC;SCS_4M8_IS_SCS;SCS_4M8_IS_SCS;
3205 SCS_4M8_prime_IS_SCS;K_SCS_4M8;K_SCS_4M8_prime;IN;BB_4M8_prime_IMP_scs_4M8]
3207 THEN REAL_ARITH_TAC);;
3212 let SCS_4M8_prime_ARROW_MM_4M8=prove_by_refinement(`scs_arrow_v39 {scs_4M8_prime } { scs_4M8}`,
3214 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
3215 THEN ABBREV_TAC`k=scs_k_v39 s`
3216 THEN REPEAT RESA_TAC;
3218 ASM_SIMP_TAC[SCS_4M8_IS_SCS];
3220 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M8_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M8_prime ==> MMs_v39 s = {}))`);
3225 THEN POP_ASSUM MP_TAC
3226 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
3227 THEN REPEAT STRIP_TAC
3228 THEN POP_ASSUM MP_TAC
3230 THEN EXISTS_TAC`scs_4M8`
3231 THEN ASM_REWRITE_TAC[]
3232 THEN MATCH_MP_TAC (GEN_ALL MM_4M8_prime_IMP_MM_4M8)
3233 THEN POP_ASSUM MP_TAC
3238 let SCS_5M3_24_ARROW_3T1_4M8=prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 2 4 } { scs_3T1,scs_4M8}`,
3240 MATCH_MP_TAC FZIOTEF_TRANS
3241 THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_3T1_prime 1,scs_prop_equ_v39 scs_4M8_prime 3}`
3242 THEN ASM_REWRITE_TAC[SCS_5M3_SLICE_24;SET_RULE`{A,B}={A}UNION {B}`]
3243 THEN MATCH_MP_TAC FZIOTEF_UNION
3246 MATCH_MP_TAC FZIOTEF_TRANS
3247 THEN EXISTS_TAC`{scs_3T1_prime}`
3248 THEN ASM_REWRITE_TAC[SCS_3T1_prime_ARROW_MM_3T1]
3249 THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T1_prime`;`1`;`3`][SCS_3T1_prime_IS_SCS;K_SCS_3T1_prime;ARITH_RULE`(3 - 1 MOD 3)=2`]
3250 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T1_prime 1`;`2`][PROP_EQU_IS_SCS;SCS_3T1_prime_IS_SCS]
3252 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
3255 MATCH_MP_TAC FZIOTEF_TRANS
3256 THEN EXISTS_TAC`{scs_4M8_prime}`
3257 THEN ASM_REWRITE_TAC[SCS_4M8_prime_ARROW_MM_4M8]
3258 THEN MRESAS_TAC PRO_EQU_ID1[`scs_4M8_prime`;`3`;`4`][SCS_4M8_prime_IS_SCS;K_SCS_4M8_prime;ARITH_RULE`(4 - 3 MOD 4)=1`]
3259 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M8_prime 3`;`1`][PROP_EQU_IS_SCS;SCS_4M8_prime_IS_SCS]
3261 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
3262 THEN REWRITE_TAC[]]);;
3268 let PROP_OPP_DIAG_5M3_03= prove_by_refinement(`scs_stab_diag_v39 scs_5M3 0 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_5M3 1 3)) 3 `,
3270 [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]
3271 THEN MATCH_MP_TAC scs_inj
3272 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_5M3_BASIC]
3275 MRESAL_TAC STAB_5M3_SCS[`0`;`3`][K_SCS_5M3;scs_diag;ARITH_RULE`~(0 MOD 5 = 3 MOD 5) /\
3276 ~(SUC 0 MOD 5 = 3 MOD 5) /\
3277 ~(0 MOD 5 = SUC 3 MOD 5)`];
3281 ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM]
3285 THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;]
3286 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
3288 THEN ASSUME_TAC (ARITH_RULE`~(5=0)`)
3289 THEN MRESA_TAC PSORT_MOD[`5`;`x`;`x'`]
3291 THEN MRESA_TAC MOD_ADD_MOD[`3`;`x`;`5`]
3292 THEN MRESA_TAC MOD_ADD_MOD[`3`;`x'`;`5`]
3295 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`)
3296 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
3298 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`)
3299 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
3301 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
3302 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ]]);;
3307 let PROP_OPP_DIAG_5M3_02= prove_by_refinement(`scs_stab_diag_v39 scs_5M3 0 2= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_5M3 1 4)) 3 `,
3309 [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]
3310 THEN MATCH_MP_TAC scs_inj
3311 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_5M3_BASIC]
3314 MRESAL_TAC STAB_5M3_SCS[`0`;`2`][K_SCS_5M3;scs_diag;ARITH_RULE`~(0 MOD 5 = 2 MOD 5) /\
3315 ~(SUC 0 MOD 5 = 2 MOD 5) /\
3316 ~(0 MOD 5 = SUC 2 MOD 5)`];
3320 ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM]
3324 THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_5M3;mk_unadorned_v39;peropp;peropp2;FUN_EQ_THM;]
3325 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
3327 THEN ASSUME_TAC (ARITH_RULE`~(5=0)`)
3328 THEN MRESA_TAC PSORT_MOD[`5`;`x`;`x'`]
3330 THEN MRESA_TAC MOD_ADD_MOD[`3`;`x`;`5`]
3331 THEN MRESA_TAC MOD_ADD_MOD[`3`;`x'`;`5`]
3334 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`)
3335 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
3337 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`)
3338 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
3340 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
3341 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ]]);;
3344 let SET_STAB_5M3=prove(`{ scs_stab_diag_v39 scs_5M3 i j| scs_diag 5 i j }= { scs_stab_diag_v39 scs_5M3 (i MOD 5) (j MOD 5)| scs_diag 5 (i MOD 5) (j MOD 5) }`,
3345 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(5=0)`;]
3346 THEN MRESAL_TAC STAB_MOD[`scs_5M3`][SCS_5M3_IS_SCS;K_SCS_5M3]);;
3349 let EXPAND_STAB_DIAG_5M3=prove(`{scs_stab_diag_v39 scs_5M3 (i MOD 5) (j MOD 5) | i MOD 5 =
3350 (j MOD 5 + 2) MOD 5 \/
3352 (i MOD 5 + 2) MOD 5}=
3353 {scs_stab_diag_v39 scs_5M3 (i+2) i| i<5} `,
3354 ASM_SIMP_TAC[EXPAND_STAB_DIAG_5;SCS_5M3_IS_SCS;K_SCS_5M3]);;
3357 let SET_EQ_DIAG_STAB_5M3= prove_by_refinement(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 i j | scs_diag 5 i j}
3358 {scs_stab_diag_v39 scs_5M3 0 2, scs_stab_diag_v39 scs_5M3 0 3, scs_stab_diag_v39
3363 ONCE_REWRITE_TAC[SET_STAB_5M3]
3364 THEN REWRITE_TAC[DIAG_EQ_ADD5;EXPAND_STAB_DIAG_5I3;EXPAND_STAB_DIAG_5M3]
3365 THEN REWRITE_TAC[ARITH_RULE`i<5<=> i=0\/i=1\/i=2\/i=3\/i=4`;
3373 `;SET_RULE`{scs_stab_diag_v39 scs_5M3 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4}
3375 {scs_stab_diag_v39 scs_5M3 (0 + 2) 0} UNION
3376 {scs_stab_diag_v39 scs_5M3 (1 + 2) 1} UNION
3377 {scs_stab_diag_v39 scs_5M3 (2 + 2) 2} UNION
3378 {scs_stab_diag_v39 scs_5M3 (3 + 2) 3} UNION
3379 {scs_stab_diag_v39 scs_5M3 (4 + 2) 4}
3381 THEN MATCH_MP_TAC FZIOTEF_UNION
3384 REWRITE_TAC[ARITH_RULE`0+2=2`;STAB_SYM]
3385 THEN MATCH_MP_TAC FZIOTEF_REFL
3386 THEN REWRITE_TAC[IN_SING]
3387 THEN REPEAT RESA_TAC
3388 THEN MRESAL_TAC STAB_5M3_SCS[`2`;`0`][scs_diag;K_SCS_5M3;ARITH_RULE`~(2 MOD 5 = 0 MOD 5) /\
3389 ~(SUC 2 MOD 5 = 0 MOD 5) /\
3390 ~(2 MOD 5 = SUC 0 MOD 5)`];
3392 MATCH_MP_TAC FZIOTEF_UNION
3395 REWRITE_TAC[ARITH_RULE`1+2=3`;STAB_SYM;PROP_OPP_DIAG_5M3_03]
3396 THEN MATCH_MP_TAC FZIOTEF_TRANS
3397 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_5M3 1 3)}`
3400 MATCH_MP_TAC (GEN_ALL YXIONXL2)
3402 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(5<=3)`;K_SCS_5M3]
3403 THEN MRESAL_TAC STAB_5M3_SCS[`1`;`3`][scs_diag;K_SCS_5M3;ARITH_RULE`~(1 MOD 5 = 3 MOD 5) /\
3404 ~(SUC 1 MOD 5 = 3 MOD 5) /\
3405 ~(1 MOD 5 = SUC 3 MOD 5)`];
3407 MATCH_MP_TAC(GEN_ALL YXIONXL3)
3408 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
3409 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_5M3 1 3)`
3410 THEN MRESAL_TAC STAB_5M3_SCS[`1`;`3`][scs_diag;K_SCS_5M3;ARITH_RULE`~(1 MOD 5 = 3 MOD 5) /\
3411 ~(SUC 1 MOD 5 = 3 MOD 5) /\
3412 ~(1 MOD 5 = SUC 3 MOD 5)`];
3414 MATCH_MP_TAC FZIOTEF_UNION
3417 REWRITE_TAC[ARITH_RULE`2+2=4`;STAB_SYM]
3418 THEN MATCH_MP_TAC FZIOTEF_REFL
3419 THEN REWRITE_TAC[IN_SING]
3420 THEN REPEAT RESA_TAC
3421 THEN MRESAL_TAC STAB_5M3_SCS[`2`;`4`][scs_diag;K_SCS_5M3;ARITH_RULE`~(2 MOD 5 = 4 MOD 5) /\
3422 ~(SUC 2 MOD 5 = 4 MOD 5) /\
3423 ~(2 MOD 5 = SUC 4 MOD 5)`];
3425 MATCH_MP_TAC FZIOTEF_UNION
3428 REWRITE_TAC[ARITH_RULE`3+2=5`;STAB_SYM]
3429 THEN MRESAL_TAC STAB_MOD[`scs_5M3`;`5`;`3`][SCS_5M3_IS_SCS;K_SCS_5M3;ARITH_RULE`5 MOD 5=0/\ 3 MOD 5=3`]
3431 THEN REWRITE_TAC[ARITH_RULE`3+2=5`;STAB_SYM]
3432 THEN MATCH_MP_TAC FZIOTEF_REFL
3433 THEN REWRITE_TAC[IN_SING]
3434 THEN REPEAT RESA_TAC
3435 THEN MRESAL_TAC STAB_5M3_SCS[`3`;`0`][scs_diag;K_SCS_5M3;ARITH_RULE`~(3 MOD 5 = 0 MOD 5) /\
3436 ~(SUC 3 MOD 5 = 0 MOD 5) /\
3437 ~(3 MOD 5 = SUC 0 MOD 5)`];
3439 REWRITE_TAC[ARITH_RULE`4+2=6`;]
3440 THEN MRESAL_TAC STAB_MOD[`scs_5M3`;`6`;`4`][SCS_5M3_IS_SCS;K_SCS_5M3;ARITH_RULE`6 MOD 5=1/\ 4 MOD 5=4`]
3442 THEN REWRITE_TAC[PROP_OPP_DIAG_5M3_02];
3444 MATCH_MP_TAC FZIOTEF_TRANS
3445 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_5M3 1 4)}`
3448 MATCH_MP_TAC (GEN_ALL YXIONXL2)
3450 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(5<=3)`;K_SCS_5M3]
3451 THEN MRESAL_TAC STAB_5M3_SCS[`1`;`4`][scs_diag;K_SCS_5M3;ARITH_RULE`~(1 MOD 5 = 4 MOD 5) /\
3452 ~(SUC 1 MOD 5 = 4 MOD 5) /\
3453 ~(1 MOD 5 = SUC 4 MOD 5)`];
3455 MATCH_MP_TAC(GEN_ALL YXIONXL3)
3456 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
3457 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_5M3 1 4)`
3458 THEN MRESAL_TAC STAB_5M3_SCS[`1`;`4`][scs_diag;K_SCS_5M3;ARITH_RULE`~(1 MOD 5 = 4 MOD 5) /\
3459 ~(SUC 1 MOD 5 = 4 MOD 5) /\
3460 ~(1 MOD 5 = SUC 4 MOD 5)`]]);;
3464 let SET_EQ_DIAG_STAB_5M3_IMP_SCS_3_4=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_5M3 i j | scs_diag 5 i j}
3465 {scs_4M6',scs_4M7,scs_4M8,scs_3T1,scs_3T4}`,
3466 MATCH_MP_TAC FZIOTEF_TRANS
3467 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_5M3 0 2, scs_stab_diag_v39 scs_5M3 0 3, scs_stab_diag_v39
3471 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_5M3;SET_RULE`{scs_4M6', scs_4M7, scs_4M8, scs_3T1, scs_3T4}= {scs_3T4, scs_4M6'}UNION{scs_4M7,scs_3T1}UNION{ scs_3T1,scs_4M8}`]
3472 THEN REWRITE_TAC[SET_RULE`{A,B,C}={A}UNION{B}UNION{C}`]
3473 THEN MATCH_MP_TAC FZIOTEF_UNION
3474 THEN REWRITE_TAC[SCS_5M3_02_ARROW_3T4_4M6]
3475 THEN MATCH_MP_TAC FZIOTEF_UNION
3476 THEN REWRITE_TAC[SCS_5M3_03_ARROW_3T1_4M7;SCS_5M3_24_ARROW_3T1_4M8]);;
3480 let h0_LT_B_SCS_5M2=prove(`
3481 (!i j. scs_diag 5 i j ==> &4 * h0 < scs_b_v39 scs_5M2 i j)
3482 /\ (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5M2 i j <= cstab)`,
3484 THEN REWRITE_TAC[h0;scs_diag;cstab]
3485 THEN REPEAT RESA_TAC
3486 THEN MP_TAC DIAG_5_EQU_PSORT
3488 THEN REWRITE_TAC[PAIR_EQ;]
3490 THEN REAL_ARITH_TAC);;
3493 let B_LE_CSTAB_5M2=prove(`
3494 (!i. scs_b_v39 scs_5M2 i (SUC i) <= cstab)/\
3495 (!i. scs_a_v39 scs_5M2 i (SUC i) = &2)
3498 THEN SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;h0;cstab]
3499 THEN REPEAT RESA_TAC
3500 THEN MRESAS_TAC PSORT_MOD[`5`;`i`;`SUC i`][ARITH_RULE`~(5=0)`]
3502 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
3504 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`)
3505 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
3508 THEN REAL_ARITH_TAC);;
3512 let B_LE_CSTAB_5M2_A_LT_B=prove(`
3513 (!i. &2 < scs_b_v39 scs_5M2 i (SUC i))
3516 THEN SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;h0;cstab]
3517 THEN REPEAT RESA_TAC
3518 THEN MRESAS_TAC PSORT_MOD[`5`;`i`;`SUC i`][ARITH_RULE`~(5=0)`]
3520 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`5`][ARITH_RULE`1<5`]
3522 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`)
3523 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
3526 THEN REAL_ARITH_TAC);;
3534 let CARD_SCS_M_5M2=prove(`CARD (scs_M scs_5M2) <= 1`,
3535 ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
3537 THEN ASM_SIMP_TAC[h0;cstab;]
3538 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
3539 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
3540 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
3541 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
3542 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`]
3543 THEN SUBGOAL_THEN`{i | i < 5 /\
3544 (&2 * #1.26 < (if psort 5 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/
3545 &2 < (if psort 5 (i,SUC i) = 0,1 then &2 else &2))} ={0}`ASSUME_TAC
3548 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`]
3552 THEN POP_ASSUM MP_TAC
3553 THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `];
3555 ASM_REWRITE_TAC[Geomdetail.CARD_SING]
3560 let SCS_M_5M2=prove(`scs_M scs_5M2={0}`,
3561 ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
3563 THEN ASM_SIMP_TAC[h0;cstab;]
3564 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
3565 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
3566 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
3567 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
3568 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`]
3570 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`]
3574 THEN POP_ASSUM MP_TAC
3575 THEN ASM_REWRITE_TAC[PSORT_5_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01 `]
3580 let SCS_M_5T1=prove(`scs_M scs_5T1={}`,
3581 ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
3583 THEN ASM_SIMP_TAC[h0;cstab;]
3584 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
3585 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
3586 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
3587 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
3588 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<5`]
3589 THEN ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~((&2 * #1.26 < &2 \/ &2 < &2))`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]);;
3593 (******ADD PROPERTY OF LEMMA JCYFMRP************)
3595 let JCYFMRP_V1 = prove_by_refinement(`main_nonlinear_terminal_v11
3596 ==>(!s (v:num->real^3) i.
3598 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
3599 ( dist(v i,v (i+1)) = &2) /\
3600 CARD (scs_M s) <= 1 /\
3601 (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j) /\ &4 * h0 < scs_b_v39 s i j)) /\
3602 (!i. scs_a_v39 s i (i+1)< scs_b_v39 s i (i+1))
3604 (?i1. ~(i1 MOD scs_k_v39 s IN scs_M s)/\ dist(v i1, v (i1+1)) = &2))`,
3607 THEN ABBREV_TAC`k= scs_k_v39 s`
3608 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
3609 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
3610 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
3611 THEN REPEAT RESA_TAC
3612 THEN MP_TAC(SET_RULE`i MOD k IN scs_M s\/ ~(i MOD k IN scs_M s)`)
3615 SUBGOAL_THEN`scs_M s={i MOD k}`ASSUME_TAC;
3617 MRESAS_TAC CARD_SUBSET_LE[`{i MOD k}`;`scs_M s`][Jlxfdmj.FINITE_SCS_M;SET_RULE`a IN A==> {a} SUBSET A`;Geomdetail.CARD_SING];
3619 MRESA_TAC Jlxfdmj.SCS_M_EQ_1[`i MOD k`;`s`]
3620 THEN THAYTHES_TAC 0[`SUC i`][SET_RULE`(SUC i MOD k = i MOD k)<=> (i MOD k = SUC i MOD k)`;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`3<k==> 1<k`]
3623 THEN REWRITE_TAC[ARITH_RULE`SUC i= i+1/\ (i + 1) + 1= i+2`]
3624 THEN REPEAT STRIP_TAC
3625 THEN MP_TAC Tfitskc.TFITSKC
3627 THEN THAYTHE_TAC 0[`s`;`v`;`i`]
3629 THEN THAYTHEL_ASM_TAC(17-13)[`i+2`][ARITH_RULE`(i+2)+1=i+3`]
3630 THEN THAYTHE_TAC 0[`i`]
3631 THEN MP_TAC Jlxfdmj.SCS_A_2
3633 THEN THAYTHE_TAC 0[`i`]
3634 THEN MP_TAC(REAL_ARITH`scs_a_v39 s i (i + 1) < scs_b_v39 s i (i + 1)
3635 /\ &2<= scs_a_v39 s i (i + 1)
3636 ==> &2 < scs_b_v39 s i (i + 1)`)
3639 THEN EXISTS_TAC`SUC i`
3640 THEN ASM_SIMP_TAC[Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`3<k==> 1<k`;SET_RULE`~(a IN {b})<=> ~(b=a)`;ARITH_RULE`SUC i= i+1/\ (i + 1) + 1= i+2`];
3643 THEN ASM_REWRITE_TAC[]]);;
3648 let JCYFMRP_V2 = prove_by_refinement(
3649 `main_nonlinear_terminal_v11
3650 ==>(!s (v:num->real^3) i.
3652 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
3653 ( dist(v i,v (i+1)) = &2) /\
3654 CARD (scs_M s) <= 1 /\
3655 (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j) /\ &4 * h0 < scs_b_v39 s i j)) /\
3656 (!i. scs_a_v39 s i (i+1)< scs_b_v39 s i (i+1))
3658 (?i1. scs_b_v39 s i1 (SUC i1) <= &2 * h0/\ scs_a_v39 s i1 (SUC i1) = &2/\ dist(v i1, v (i1+1)) = &2))`,
3661 THEN ABBREV_TAC`k= scs_k_v39 s`
3662 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
3663 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
3664 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
3665 THEN REPEAT RESA_TAC
3666 THEN MP_TAC(SET_RULE`i MOD k IN scs_M s\/ ~(i MOD k IN scs_M s)`)
3669 SUBGOAL_THEN`scs_M s={i MOD k}`ASSUME_TAC;
3671 MRESAS_TAC CARD_SUBSET_LE[`{i MOD k}`;`scs_M s`][Jlxfdmj.FINITE_SCS_M;SET_RULE`a IN A==> {a} SUBSET A`;Geomdetail.CARD_SING];
3673 MRESA_TAC Jlxfdmj.SCS_M_EQ_1[`i MOD k`;`s`]
3674 THEN THAYTHES_TAC 0[`SUC i`][SET_RULE`(SUC i MOD k = i MOD k)<=> (i MOD k = SUC i MOD k)`;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`3<k==> 1<k`]
3677 THEN REWRITE_TAC[ARITH_RULE`SUC i= i+1/\ (i + 1) + 1= i+2`]
3678 THEN REPEAT STRIP_TAC
3679 THEN MP_TAC Tfitskc.TFITSKC
3681 THEN THAYTHE_TAC 0[`s`;`v`;`i`]
3683 THEN THAYTHEL_ASM_TAC(17-13)[`i+2`][ARITH_RULE`(i+2)+1=i+3`]
3684 THEN THAYTHE_TAC 0[`i`]
3685 THEN MP_TAC Jlxfdmj.SCS_A_2
3687 THEN THAYTHE_TAC 0[`i`]
3688 THEN MP_TAC(REAL_ARITH`scs_a_v39 s i (i + 1) < scs_b_v39 s i (i + 1)
3689 /\ &2<= scs_a_v39 s i (i + 1)
3690 ==> &2 < scs_b_v39 s i (i + 1)`)
3693 THEN EXISTS_TAC`SUC i`
3694 THEN ASM_SIMP_TAC[Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`3<k==> 1<k`;SET_RULE`~(a IN {b})<=> ~(b=a)`;ARITH_RULE`SUC i= i+1/\ (i + 1) + 1= i+2`];
3697 THEN ASM_REWRITE_TAC[]
3698 THEN POP_ASSUM MP_TAC
3699 THEN MP_TAC(ARITH_RULE`CARD (scs_M s)<= 1==> CARD (scs_M s)= 0\/ CARD (scs_M s)=1`)
3702 MP_TAC Jlxfdmj.SCS_M_EQ_0
3705 MRESAS_TAC Local_lemmas.FINITE_CARD1_IMP_SINGLETON[`scs_M s`][Jlxfdmj.FINITE_SCS_M;SET_RULE`~(a IN {x})<=> ~(a=x)`]
3707 THEN MP_TAC Jlxfdmj.SCS_M_EQ_1
3709 THEN THAYTHE_TAC 0[`i`]]);;
3715 let JCYFMRP_V3=prove(`main_nonlinear_terminal_v11
3716 ==>(!s (v:num->real^3).
3718 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
3719 CARD (scs_M s) <= 1 /\
3720 (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j) /\ &4 * h0 < scs_b_v39 s i j)) /\
3721 (!i. scs_a_v39 s i (i+1)< scs_b_v39 s i (i+1)) /\
3722 (!i. scs_a_v39 s i (SUC i) = &2)
3724 (?i. scs_b_v39 s i (SUC i) <= &2 * h0/\ scs_a_v39 s i (SUC i) = &2/\ dist(v i, v (i+1)) = &2))`,
3726 THEN MP_TAC Jcyfmrp.JCYFMRP
3728 THEN THAYTHE_TAC 0[`s`;`v`]
3729 THEN POP_ASSUM MP_TAC
3732 THEN MP_TAC JCYFMRP_V2
3733 THEN ASM_REWRITE_TAC[]
3735 THEN THAYTHE_TAC 0[`s`;`v`;`i`]);;
3738 (*********************)
3740 let ARC_222=prove(`arclength (&2) (&2) (&2)= pi/ &3`,
3741 MRESAS_TAC Trigonometry.PQQDENV[`&2`;`&2`;`&2`][REAL_ARITH`&0 < &2 /\ &0 < &2 /\ &0 <= &2 /\ &2 <= &2 + &2/\ (&2 * &2 + &2 * &2 - &2 * &2) / (&2 * &2 * &2)= &1/ &2`;Nonlinear_lemma.ACS_2]);;
3745 let xrr_le_1553=prove(` v IN ball_annulus/\ u IN ball_annulus/\ w IN ball_annulus
3746 /\ ~collinear {vec 0, v, u}
3747 /\ dist(v,w)= &2/\ dist(w,u)= &2
3749 xrr (norm v) (norm u) (norm(v-u))<= #15.53`,
3751 THEN MRESA_TAC Counting_spheres.ckq_in_ball_annulus[`v`]
3752 THEN MRESA_TAC Counting_spheres.ckq_in_ball_annulus[`u`]
3753 THEN MRESA_TAC Counting_spheres.ckq_in_ball_annulus[`w`]
3754 THEN MRESA_TAC Trigonometry2.ARCV_INEQUALTY[`vec 0:real^3`;`v`;`u`;`w`]
3755 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v`;`w`;`&2`][REAL_ARITH`&2 < &4 /\ &2 <= &2 `;ARC_222]
3756 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`w`;`u`;`&2`][REAL_ARITH`&2 < &4 /\ &2 <= &2 `;ARC_222]
3757 THEN MP_TAC(REAL_ARITH`arcV (vec 0) v u <= arcV (vec 0) v w + arcV (vec 0) w u
3758 /\ arcV (vec 0) v w <= pi / &3/\ arcV (vec 0) w u <= pi / &3
3759 ==> arcV (vec 0:real^3) v u<= &2 * pi/ &3`)
3761 THEN POP_ASSUM MP_TAC
3762 THEN MRESA_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`v`;`u`]
3763 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- a= --a:real^3`;NORM_NEG]
3764 THEN MRESAL_TAC th3[`v`;`vec 0:real^3`;`u:real^3`][GSYM dist;VECTOR_ARITH`v - u = vec 0
3767 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
3769 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`v`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A:real^3`]
3770 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`u`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A:real^3`]
3771 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`v`;`u:real^3`][VECTOR_ARITH`A- vec 0=A:real^3`]
3772 THEN MRESAL_TAC Collect_geom2.NOT_COL_EQ_UPS_X_POS[`vec 0:real^3`;`v`;`u`][dist;VECTOR_ARITH`vec 0- a= --a:real^3`;NORM_NEG]
3773 THEN MRESAL_TAC arclength_xrr[`norm v`;`norm u`;`norm (v- u)`][REAL_ARITH`a*a= a pow 2`]
3775 THEN MRESAL_TAC ACS_NEG[`&1/ &2`][REAL_ARITH`-- &1 <= &1 / &2 /\ &1 / &2 <= &1/\ pi - pi / &3= &2* pi/ &3`;Nonlinear_lemma.ACS_2]
3776 THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`norm v`;`norm u`;`norm (v-u)`][REAL_ARITH`a*a= a pow 2`]
3777 THEN MP_TAC(REAL_ARITH`&0 < xrr (norm v) (norm u) (norm (v - u))/\
3778 xrr (norm v) (norm u) (norm (v - u)) < &16
3779 ==> abs (&1 - xrr (norm v) (norm u) (norm (v - u:real^3)) / &8) <= &1`)
3781 THEN MRESAL_TAC ACS_MONO_LE_EQ[`&1 - xrr (norm v) (norm u) (norm (v - u)) / &8`;`--( &1/ &2)`][REAL_ARITH`abs (--(&1 / &2)) <= &1`]
3783 THEN REAL_ARITH_TAC);;
3787 let xrr_le_1553_BB=prove(`BBs_v39 s v /\ dist(v i, v (i+1))= &2/\ dist( v (i+1), v(i+2))= &2 /\ ~(collinear{vec 0 , v i, v (i+2)})
3788 ==> xrr (norm (v i)) (norm (v (i+2))) (norm(v i- v (i+2)))<= #15.53 `,
3790 THEN MATCH_MP_TAC (GEN_ALL xrr_le_1553)
3791 THEN EXISTS_TAC`(v:num->real^3) (i+1)`
3793 THEN MRESA_TAC Nuxcoea.WL_IN_BALL_ANNULUS[`s`;`v`;`i`]
3794 THEN MRESA_TAC Nuxcoea.WL_IN_BALL_ANNULUS[`s`;`v`;`i+1`]
3795 THEN MRESA_TAC Nuxcoea.WL_IN_BALL_ANNULUS[`s`;`v`;`i+2`]);;
3799 (******************************)
3802 let J_SCS_5M2_0=prove(`(!i j. ~scs_J_v39 scs_5M2 j i)`,
3807 let SCS_5M2_IMP_SCS_5T1= prove_by_refinement(`main_nonlinear_terminal_v11
3809 v IN MMs_v39 scs_5M2 /\
3810 (!i j. scs_diag 5 i j ==> cstab < dist(v i,v j)) ==>
3811 ~(MMs_v39 (scs_5T1)={}))`,
3813 REWRITE_TAC[IN;SET_RULE`~(A={})<=> ?a. a IN A`]
3814 THEN REPEAT STRIP_TAC
3815 THEN MP_TAC SCS_5M2_IS_SCS
3817 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`]
3818 THEN ASSUME_TAC SCS_5M2_BASIC
3819 THEN ASSUME_TAC K_SCS_5M2
3820 THEN ASSUME_TAC SCS_5T1_BASIC
3821 THEN ASSUME_TAC K_SCS_5T1
3822 THEN ASSUME_TAC SCS_5T1_IS_SCS
3823 THEN MP_TAC Rrcwnsj.RRCWNSJ
3825 THEN THAYTHES_TAC 0[`scs_5M2`;`v`][ARITH_RULE`3<5`;h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2]
3826 THEN MP_TAC JCYFMRP_V3
3828 THEN THAYTHES_TAC 0[`scs_5M2`;`v`][ARITH_RULE`3<5`;h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2;IN;CARD_SCS_M_5M2;GSYM ADD1;B_LE_CSTAB_5M2_A_LT_B]
3829 THEN MP_TAC Jlxfdmj.JLXFDMJ
3831 THEN THAYTHES_TAC 0[`scs_5M2`;`v`;`i`][ARITH_RULE`3<5`;h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2;CARD_SCS_M_5M2;SCS_M_5M2;IN_SING;]
3833 THEN ASM_REWRITE_TAC[IN;GSYM ADD1;B_LE_CSTAB_5M2;B_LE_CSTAB_5M2_A_LT_B]
3835 THEN ABBREV_TAC`V=(IMAGE (v:num->real^3) (:num))`
3836 THEN ABBREV_TAC`E=(IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num))`
3837 THEN ABBREV_TAC`FF=IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
3838 THEN SUBGOAL_THEN`dist((v:num->real^3) 0, v 1)= &2`ASSUME_TAC;
3842 ASSUME_TAC(ARITH_RULE`3<5/\ 0+1=1/\ 0+5-1=4`)
3843 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`5`;`scs_5M2`;`v`]
3844 THEN MP_TAC Local_lemmas.CVLF_LF_F
3846 THEN MRESA_TAC WL_IN_V[`0`;`v:num->real^3`]
3847 THEN MRESA_TAC WL_IN_V[`1`;`v:num->real^3`]
3848 THEN MRESA_TAC WL_IN_V[`2`;`v:num->real^3`]
3849 THEN MRESA_TAC WL_IN_V[`3`;`v:num->real^3`]
3850 THEN MRESA_TAC WL_IN_V[`4`;`v:num->real^3`]
3851 THEN MRESAL_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`scs_5M2`;`FF`;`v (0)`;`v`;`0`;`5`][]
3852 THEN MRESA_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v 0`]
3853 THEN THAYTHE_TAC 0[`v 4`]
3854 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v 0) (v 1) (v 4) <= pi
3855 ==> azim (vec 0) ((v:num->real^3) 0) (v 1) (v 4) = pi\/ azim (vec 0) (v 0) (v 1) (v 4) < pi`)
3864 THEN REWRITE_TAC[scs_generic]
3866 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_5M2`]
3867 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v 1`;`v 4`;`V`]
3868 THEN THAYTHEL_ASM_TAC 0[`v 1`;`v 4`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Uxckfpe.ARITH_5_TAC]
3869 THEN SUBGOAL_THEN`(!j. ~(j MOD 5 = 4 MOD 5) ==> ~collinear {vec 0, v 4, (v:num->real^3)j})`ASSUME_TAC
3875 THEN THAYTHE_TAC 1[`v 4`;`v j`]
3876 THEN MATCH_DICH_TAC 0
3877 THEN REWRITE_TAC[SET_RULE`a IN {b,a}`]
3878 THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
3881 THAYTHEL_ASM_TAC (33-30)[`4+1`;`0`][ARITH_RULE`( 4+1) MOD 5 = 0 MOD 5`]
3882 THEN THAYTHEL_ASM_TAC 0[`4+2`;`1`][ARITH_RULE`( 4+2) MOD 5 = 1 MOD 5`]
3883 THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v 0`;`v 1`;`(v:num->real^3) 4`]
3884 THEN POP_ASSUM MP_TAC
3885 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
3887 THEN MRESA_TAC Iunbuig.coplanar_aff_gt_simple[`scs_5M2`;`5`;`v`;`4`]
3888 THEN POP_ASSUM MP_TAC
3889 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
3891 THEN SUBGOAL_THEN`(!i. scs_diag 5 0 i ==> scs_a_v39 scs_5M2 0 i < dist ((v:num->real^3) 0,v i))`ASSUME_TAC;
3895 THEN THAYTHE_TAC(38-2)[`0`;`i'`]
3896 THEN MP_TAC h0_LT_B_SCS_5M2
3898 THEN THAYTHE_TAC 0[`0`;`i'`]
3901 THEN REAL_ARITH_TAC;
3903 MRESAL_TAC MMS_IMP_BBPRIME[`scs_5M2`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
3904 THEN MRESAL_TAC JKQEWGV2[`scs_5M2`;`v`][LET_DEF;LET_END_DEF;scs_generic]
3905 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
3907 THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) 0) V E)`ASSUME_TAC
3912 THEN ASM_REWRITE_TAC[]
3913 THEN EXISTS_TAC`v1:real^3`
3914 THEN EXISTS_TAC`(v:num->real^3)0`
3915 THEN ASM_REWRITE_TAC[]
3920 MRESAS_TAC NUXCOEAv2[`scs_5M2`;`5`;`v`;`0`;`4`][ARITH_RULE`SUC 0=1/\ SUC 4 MOD 5 = 0 MOD 5`;h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2;J_SCS_5M2_0]
3923 THEN MATCH_MP_TAC(SET_RULE`(A==> (B/\A1==>C)==>D)==> (A==>(B/\ A1/\A==>C)==>D)`)
3926 THEN THAYTHES_TAC(43-12)[`4`][ARITH_RULE`~(4 MOD 5=0)/\ SUC A= A+1`;h0]
3927 THEN REAL_ARITH_TAC;
3933 ASSUME_TAC(ARITH_RULE`1+1=2/\ 1+5-1=5`)
3934 THEN MRESAL_TAC Rrcwnsj.BB_RHO_NODE_IVS[`V`;`E`;`scs_5M2`;`FF`;`v (1)`;`v`;`1`;`5`][]
3935 THEN MRESA_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v 1`]
3936 THEN THAYTHE_TAC 0[`v 0`]
3937 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v 1) (v 2) (v 0) <= pi
3938 ==> azim (vec 0) ((v:num->real^3) 1) (v 2) (v 0) = pi\/ azim (vec 0) (v 1) (v 2) (v 0) < pi`)
3947 THEN REWRITE_TAC[scs_generic]
3949 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_5M2`]
3950 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v 2`;`v 0`;`V`]
3951 THEN THAYTHEL_ASM_TAC 0[`v 2`;`v 0`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Uxckfpe.ARITH_5_TAC]
3952 THEN SUBGOAL_THEN`(!j. ~(j MOD 5 = 0 MOD 5) ==> ~collinear {vec 0, v 0, (v:num->real^3)j})`ASSUME_TAC
3958 THEN THAYTHE_TAC 1[`v 0`;`v j`]
3959 THEN MATCH_DICH_TAC 0
3960 THEN REWRITE_TAC[SET_RULE`a IN {b,a}`]
3961 THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
3964 MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v 1`;`v 2`;`(v:num->real^3) 0`]
3965 THEN POP_ASSUM MP_TAC
3966 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
3968 THEN MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`scs_5M2`;`5`;`v`;`0`][ARITH_RULE`0+2=2`]THEN POP_ASSUM MP_TAC
3969 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
3971 THEN SUBGOAL_THEN`(!i. scs_diag 5 1 i ==> scs_a_v39 scs_5M2 1 i < dist ((v:num->real^3) 1,v i))`ASSUME_TAC;
3975 THEN THAYTHE_TAC(41-2)[`1`;`i'`]
3976 THEN MP_TAC h0_LT_B_SCS_5M2
3978 THEN THAYTHE_TAC 0[`1`;`i'`]
3981 THEN REAL_ARITH_TAC;
3983 MRESAL_TAC MMS_IMP_BBPRIME[`scs_5M2`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
3984 THEN MRESAL_TAC JKQEWGV2[`scs_5M2`;`v`][LET_DEF;LET_END_DEF;scs_generic]
3985 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
3987 THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) 1) V E)`ASSUME_TAC
3992 THEN ASM_REWRITE_TAC[]
3993 THEN EXISTS_TAC`v1:real^3`
3994 THEN EXISTS_TAC`(v:num->real^3)1`
3995 THEN ASM_REWRITE_TAC[]
4000 MRESAS_TAC NUXCOEAv2[`scs_5M2`;`5`;`v`;`1`;`2`][ARITH_RULE`SUC 1=2/\ SUC 4 MOD 5 = 0 MOD 5`;h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2;J_SCS_5M2_0]
4003 THEN THAYTHEL_TAC(45-35)[`5`;`0`][ARITH_RULE`5 MOD 5 = 0 MOD 5`]
4004 THEN MATCH_MP_TAC(SET_RULE`(A==> (B/\A1==>C)==>D)==> (A==>(B/\ A1/\A==>C)==>D)`)
4008 THEN ONCE_REWRITE_TAC[DIST_SYM]
4010 THEN ONCE_REWRITE_TAC[DIST_SYM]
4011 THEN THAYTHES_TAC(46-12)[`1`][ARITH_RULE`~(1 MOD 5=0)/\ SUC A= A+1`;h0]
4012 THEN REAL_ARITH_TAC;
4015 MP_TAC Iunbuig.IUNBUIG
4017 THEN MATCH_DICH_TAC 0
4018 THEN EXISTS_TAC`scs_5M2`
4019 THEN EXISTS_TAC`FF:real^3#real^3->bool`
4020 THEN ASM_SIMP_TAC[h0_LT_B_SCS_5M2;B_LE_CSTAB_5M2;GSYM ADD1]
4022 THEN ASM_REWRITE_TAC[REAL_ARITH`a<=a`;interior_angle1;GSYM ivs_rho_node1]
4023 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_5M2`]
4024 THEN THAYTHEL_TAC 0[`5`;`0`][ARITH_RULE`5 MOD 5 = 0 MOD 5`]
4025 THEN THAYTHEL_ASM_TAC (35-13)[`3`][ARITH_RULE`~(3 MOD 5= 0)/\ SUC 3=4`]
4026 THEN THAYTHEL_ASM_TAC (0)[`4`][ARITH_RULE`~(4 MOD 5= 0)/\ SUC 4=5`]
4027 THEN THAYTHEL_ASM_TAC (0)[`1`][ARITH_RULE`~(1 MOD 5= 0)/\ SUC 1=2`]
4028 THEN THAYTHEL_ASM_TAC (0)[`2`][ARITH_RULE`~(2 MOD 5= 0)/\ SUC 2=3`]
4029 THEN DICH_TAC (39-10)
4030 THEN REWRITE_TAC[scs_generic]
4032 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_5M2`]
4033 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v 0`;`v 3`;`V`]
4034 THEN THAYTHEL_ASM_TAC 0[`v 3`;`v 0`][SET_RULE`a IN {b,a}`;BB_VV_FUN_EQ;Uxckfpe.ARITH_5_TAC]
4035 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v 1`;`v 3`;`V`]
4036 THEN THAYTHEL_ASM_TAC 0[`v 1`;`v 3`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Uxckfpe.ARITH_5_TAC]
4037 THEN MRESAL_TAC xrr_le_1553_BB[`scs_5M2`;`v`;`3`][ARITH_RULE`3+1=4/\ 3+2=5`]
4038 THEN MRESAL_TAC xrr_le_1553_BB[`scs_5M2`;`v`;`1`][ARITH_RULE`1+1=2/\ 1+2=3`;GSYM dist]
4039 THEN ONCE_REWRITE_TAC[DIST_SYM]
4041 THEN REWRITE_TAC[xrr;dist]
4046 SUBGOAL_THEN`!j. dist ((v:num->real^3) j,v (SUC j)) = &2`ASSUME_TAC
4050 THEN MP_TAC(SET_RULE`~(j MOD 5 = 0) \/ (j MOD 5 = 0)`)
4054 MATCH_DICH_TAC (18-13)
4055 THEN ASM_REWRITE_TAC[];
4058 MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_5M2`]
4059 THEN THAYTHEL_ASM_TAC 0[`j`;`0`][ARITH_RULE`0 MOD 5=0`]
4060 THEN THAYTHES_TAC 0[`SUC j`;`SUC 0`][ARITH_RULE`~(5=0)/\ SUC i= 1+i/\ 0 MOD 5=0`;Ocbicby.MOD_EQ_MOD_SHIFT]
4061 THEN ASM_REWRITE_TAC[ARITH_RULE`1+0=1`];
4066 MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
4067 THEN REWRITE_TAC[IN;SET_RULE`~(A={})<=> ?a. a IN A`]
4069 THEN MATCH_DICH_TAC 0
4070 THEN EXISTS_TAC`v:num->real^3`
4071 THEN EXISTS_TAC`scs_5M2`
4072 THEN ASM_SIMP_TAC[SCS_M_5M2]
4079 THEN REWRITE_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;scs_diag;ARITH_RULE`(~(5<=3))`;IN;K_SCS_4M8_prime;K_SCS_4M8;scs_prop_equ_v39;]
4080 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
4082 THEN REWRITE_TAC[ARITH_RULE`~(5<=3)`];
4088 MP_TAC(SET_RULE`i' MOD 5 = j MOD 5\/ ~(i' MOD 5 = j MOD 5)`)
4091 THAYTHE_TAC 2[`i'`;`j`]
4094 MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`]
4095 THEN MP_TAC(SET_RULE`SUC i' MOD 5 = j MOD 5\/ ~(SUC i' MOD 5 = j MOD 5)`)
4099 MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j:num`;`v`;` SUC i'`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`;]
4100 THEN REAL_ARITH_TAC;
4103 MP_TAC(SET_RULE`i' MOD 5 =SUC j MOD 5\/ ~(i' MOD 5 =SUC j MOD 5)`)
4107 MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` SUC j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`;]
4108 THEN ONCE_REWRITE_TAC[DIST_SYM]
4109 THEN ASM_REWRITE_TAC[]
4110 THEN REAL_ARITH_TAC;
4113 THAYTHEL_TAC (25-2)[`i'`;`j`][scs_diag]
4115 THEN REAL_ARITH_TAC;
4119 MP_TAC(SET_RULE`i' MOD 5 = j MOD 5\/ ~(i' MOD 5 = j MOD 5)`)
4122 THAYTHE_TAC 2[`i'`;`j`]
4127 MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_5M2`;`v`]
4128 THEN MP_TAC(SET_RULE`SUC i' MOD 5 = j MOD 5\/ ~(SUC i' MOD 5 = j MOD 5)`)
4132 MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`j:num`;`v`;` SUC i'`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`;]
4133 THEN REAL_ARITH_TAC;
4137 MP_TAC(SET_RULE`i' MOD 5 =SUC j MOD 5\/ ~(i' MOD 5 =SUC j MOD 5)`)
4141 MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_5M2`;`i':num`;`v`;` SUC j`][SCS_5M2_IS_SCS;K_SCS_5M2;MOD_REFL;ARITH_RULE`~(5=0)`;]
4142 THEN ONCE_REWRITE_TAC[DIST_SYM]
4143 THEN ASM_REWRITE_TAC[]
4144 THEN REAL_ARITH_TAC;
4146 THAYTHE_TAC (25-20)[`i'`;`j`]
4148 THEN MP_TAC(SET_RULE`psort 5 (i',j) = 0,1\/ ~(psort 5 (i',j) = 0,1)`)
4152 MRESAL_TAC Uaghhbm.CASE_PSORT[`i'`;`1`;`j`;`0`;`5`][PSORT_5_EXPLICIT];
4156 THEN ASM_REWRITE_TAC[]
4157 THEN ONCE_REWRITE_TAC[ARITH_RULE`1= 1+0`]
4158 THEN ASM_SIMP_TAC[ARITH_RULE`SUC i= 1+i`;ARITH_RULE`~(5=0)/\ SUC i= 1+i/\ 0 MOD 5=0`;Ocbicby.MOD_EQ_MOD_SHIFT];
4162 THEN ASM_REWRITE_TAC[]
4163 THEN ONCE_REWRITE_TAC[ARITH_RULE`1= 1+0`]
4164 THEN ASM_SIMP_TAC[ARITH_RULE`SUC i= 1+i`;ARITH_RULE`~(5=0)/\ SUC i= 1+i/\ 0 MOD 5=0`;Ocbicby.MOD_EQ_MOD_SHIFT];
4167 THEN REAL_ARITH_TAC;
4171 THEN REAL_ARITH_TAC;
4177 let HIJ_STEP_1=prove_by_refinement(`main_nonlinear_terminal_v11
4181 ({ scs_5T1} UNION { scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j }
4182 UNION { scs_stab_diag_v39 scs_5I3 i j| scs_diag 5 i j }
4183 UNION { scs_stab_diag_v39 scs_5M3 i j| scs_diag 5 i j }))`,
4186 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
4187 THEN ABBREV_TAC`k=scs_k_v39 s`
4188 THEN REPEAT RESA_TAC;
4191 REWRITE_TAC[SCS_5T1_IS_SCS];
4193 ASM_SIMP_TAC[ STAB_5I2_SCS;K_SCS_5I2]
4196 ASM_SIMP_TAC[ STAB_5I3_SCS;K_SCS_5I3]
4200 ASM_SIMP_TAC[ STAB_5M3_SCS;K_SCS_5M3]
4205 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_5M2 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_5M2 ==> MMs_v39 s = {}))`);
4212 THEN POP_ASSUM MP_TAC
4213 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
4214 THEN REPEAT STRIP_TAC
4215 THEN POP_ASSUM MP_TAC
4217 THEN POP_ASSUM MP_TAC
4218 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
4223 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)))`)
4228 THEN ASM_REWRITE_TAC[]
4229 THEN MP_TAC SCS_5M2_IMP_SCS_5T1
4230 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
4232 THEN MATCH_DICH_TAC 0
4233 THEN ASM_REWRITE_TAC[]
4234 THEN EXISTS_TAC`v:num->real^3`
4235 THEN ASM_REWRITE_TAC[]
4241 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
4245 MP_TAC(SET_RULE` (!i. dist(v i, v(i+1))<= &2 * h0)
4246 \/ ~ (!l. dist((v:num->real^3) l, v(l+1))<= &2 * h0)
4253 EXISTS_TAC`scs_stab_diag_v39 scs_5I2 i j`
4254 THEN ASM_REWRITE_TAC[]
4257 MATCH_MP_TAC(SET_RULE`A==> B\/A\/C\/D`)
4258 THEN EXISTS_TAC`i:num`
4259 THEN EXISTS_TAC`j:num`
4260 THEN ASM_REWRITE_TAC[]
4263 MP_TAC MM_5M2_IMP_MM_STAB_5I2
4264 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
4266 THEN MATCH_DICH_TAC 0
4267 THEN ASM_REWRITE_TAC[]
4273 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<=b)<=> b<a`]
4279 MP_TAC(REAL_ARITH`dist((v:num->real^3) l, v(l+1))<= sqrt8\/ sqrt8<= dist(v l, v(l+1))`)
4284 EXISTS_TAC`scs_stab_diag_v39 scs_5I3 i j`
4285 THEN ASM_REWRITE_TAC[]
4288 MATCH_MP_TAC(SET_RULE`A==> B\/C\/A\/D`)
4289 THEN EXISTS_TAC`i:num`
4290 THEN EXISTS_TAC`j:num`
4291 THEN ASM_REWRITE_TAC[]
4294 MP_TAC MM_5M2_IMP_MM_STAB_5I3
4295 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
4297 THEN MATCH_DICH_TAC 0
4298 THEN ASM_REWRITE_TAC[]
4304 EXISTS_TAC`scs_stab_diag_v39 scs_5M3 i j`
4305 THEN ASM_REWRITE_TAC[]
4308 MATCH_MP_TAC(SET_RULE`A==> B\/C\/D\/A`)
4309 THEN EXISTS_TAC`i:num`
4310 THEN EXISTS_TAC`j:num`
4311 THEN ASM_REWRITE_TAC[]
4314 MP_TAC MM_5M2_IMP_MM_STAB_5M3
4315 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
4317 THEN MATCH_DICH_TAC 0
4318 THEN ASM_REWRITE_TAC[]
4324 let HIJQAHA=prove_by_refinement(`main_nonlinear_terminal_v11
4328 ({ scs_5T1, scs_stab_diag_v39 scs_5I2 0 2,
4329 scs_stab_diag_v39 scs_5M1 0 2, scs_stab_diag_v39 scs_5M1 0 3,
4330 scs_stab_diag_v39 scs_5M1 2
4331 4,scs_4M6',scs_4M7,scs_4M8,scs_3T1,scs_3T4
4335 THEN MATCH_MP_TAC FZIOTEF_TRANS
4336 THEN EXISTS_TAC`({ scs_5T1} UNION { scs_stab_diag_v39 scs_5I2 i j| scs_diag 5 i j }
4337 UNION { scs_stab_diag_v39 scs_5I3 i j| scs_diag 5 i j }
4338 UNION { scs_stab_diag_v39 scs_5M3 i j| scs_diag 5 i j })`
4339 THEN ASM_SIMP_TAC[HIJ_STEP_1;SET_RULE`{scs_5T1, scs_stab_diag_v39 scs_5I2 0 2, scs_stab_diag_v39 scs_5M1 0 2, scs_stab_diag_v39 scs_5M1 0 3,
4340 scs_stab_diag_v39 scs_5M1 2
4341 4, scs_4M6', scs_4M7, scs_4M8, scs_3T1, scs_3T4}
4342 ={scs_5T1}UNION{ scs_stab_diag_v39 scs_5I2 0 2}UNION{ scs_stab_diag_v39 scs_5M1 0 2, scs_stab_diag_v39 scs_5M1 0 3,
4343 scs_stab_diag_v39 scs_5M1 2
4344 4}UNION{ scs_4M6', scs_4M7, scs_4M8, scs_3T1, scs_3T4}`]
4345 THEN MATCH_MP_TAC FZIOTEF_UNION
4348 MATCH_MP_TAC FZIOTEF_REFL
4349 THEN REWRITE_TAC[IN_SING]
4350 THEN REPEAT RESA_TAC
4351 THEN ASM_REWRITE_TAC[SCS_5T1_IS_SCS];
4353 MATCH_MP_TAC FZIOTEF_UNION
4354 THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_5I2];
4356 MATCH_MP_TAC FZIOTEF_UNION
4357 THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_5M3_IMP_SCS_3_4]
4358 THEN MATCH_MP_TAC FZIOTEF_TRANS
4359 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_5M1 i j | scs_diag 5 i j}`
4360 THEN ASM_REWRITE_TAC[Otmtotj.STAB_5I3_ARROW_STAB_5M1_DIAG;Otmtotj.SET_EQ_DIAG_STAB_5M1]]);;
4367 let check_completeness_claimA_concl =
4368 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)