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 Hexagons = struct
27 open Wrgcvdr_cizmrrh;;
35 open Flyspeck_constants;;
51 open Wrgcvdr_cizmrrh;;
53 open Flyspeck_constants;;
96 let PSORT_5_EXPLICIT=prove(`
97 psort 5 (0,0)= (0,0)/\
98 psort 5 (1,1)= (1,1)/\
99 psort 5 (2,2)= (2,2)/\
100 psort 5 (3,3)= (3,3)/\
101 psort 5 (4,4)= (4,4)/\
102 psort 5 (0,1)= (0,1)/\
103 psort 5 (0,2)= (0,2)/\
104 psort 5 (0,3)= (0,3)/\
105 psort 5 (0,4)= (0,4)/\
106 psort 5 (1,0)= (0,1)/\
107 psort 5 (1,2)= (1,2)/\
108 psort 5 (1,3)= (1,3)/\
109 psort 5 (1,4)= (1,4)/\
110 psort 5 (2,0)= (0,2)/\
111 psort 5 (2,1)= (1,2)/\
112 psort 5 (2,3)= (2,3)/\
113 psort 5 (2,4)= (2,4)/\
114 psort 5 (3,0)= (0,3)/\
115 psort 5 (3,1)= (1,3)/\
116 psort 5 (3,2)= (2,3)/\
117 psort 5 (3,4)= (3,4)/\
118 psort 5 (4,0)= (0,4)/\
119 psort 5 (4,1)= (1,4)/\
120 psort 5 (4,2)= (2,4)/\
121 psort 5 (4,3)= (3,4)/\
122 psort 5 (4,5)= (0,4)/\
123 psort 4 (3,4)= (0,3)/\
124 psort 3 (2,0)= (0,2)/\
125 psort 3 (2,1)= (1,2)/\
126 psort 3 (1,0)= (0,1)`,
127 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`]);;
130 let scs_5M3 = new_definition`scs_5M3 = mk_unadorned_v39 5 (#0.616)
131 (funlist_v39 [(0,1),(&2*h0);(0,2),(cstab);(0,3),(cstab);(1,3),(cstab);(1,4),(cstab);(2,4),(cstab)] (&2) 5)
132 (funlist_v39 [(0,1),cstab;(0,2),(&6); (0,3),(&6); (1,3),(&6); (1,4),(&6); (2,4),(&6)] (&2*h0) 5)`;;
135 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;
136 Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_5_TAC;
137 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;
138 Terminal.FUNLIST_EXPLICIT;Yrtafyh.PSORT_PERIODIC;PSORT_5_EXPLICIT;
139 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`];;
143 let sqrt8_LE_6=prove(`sqrt8<= &6`,
145 THEN MATCH_MP_TAC REAL_LE_LSQRT
146 THEN REAL_ARITH_TAC);;
148 let sqrt8_LE_CSTAB=prove(`sqrt8<= #3.01`,
150 THEN MATCH_MP_TAC REAL_LE_LSQRT
151 THEN REAL_ARITH_TAC);;
154 let LE_sqrt8_2=prove(`&2<=sqrt8`,
156 THEN MATCH_MP_TAC REAL_LE_RSQRT
157 THEN REAL_ARITH_TAC);;
159 let LE_sqrt8_2h0=prove(`&2* #1.26<=sqrt8`,
161 THEN MATCH_MP_TAC REAL_LE_RSQRT
162 THEN REAL_ARITH_TAC);;
165 let LT_sqrt8_2h0=prove(`&2* #1.26<sqrt8`,
167 THEN MATCH_MP_TAC REAL_LT_RSQRT
168 THEN REAL_ARITH_TAC);;
172 (******is_scs*********)
174 let MOD_PERIODIC=prove(`~(k=0) ==> (i+k) MOD k = i MOD k/\ SUC (i+k) MOD k= SUC i MOD k`,
176 THEN ONCE_REWRITE_TAC[ARITH_RULE`i+k= 1*k+i`;]
177 THEN SIMP_TAC[MOD_MULT_ADD;ARITH_RULE`SUC (1 * k + i) =(1 * k + SUC i)`]);;
180 let SCS_6I1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_6I1`,
182 REWRITE_TAC[scs_6I1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;]
183 THEN SIMP_TAC[ARITH_RULE`~(6=0)`;MOD_PERIODIC]
187 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
188 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
191 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
192 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
195 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
196 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
207 ASM_SIMP_TAC[ARITH_RULE`~(6=0)`;MOD_LT;h0]
210 REWRITE_TAC[h0;cstab]
213 ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY]
216 let DIST_LE_IMP_A_LE=prove(`BBs_v39 s v /\ dist(v i,v j) <= a
217 ==> scs_a_v39 s i j<= a`,
218 REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39]
220 THEN THAYTHE_TAC 2[`i`;`j`]
223 THEN REAL_ARITH_TAC);;
227 let SCS_3M1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_3M1`,
228 [SIMP_TAC[scs_3M1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.103 < #0.9`;periodic;SET_RULE`{} (i + j) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
229 THEN REPEAT RESA_TAC;
238 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
240 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
242 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
244 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
246 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
248 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
250 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
252 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
254 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
256 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
259 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
261 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
265 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
267 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
271 THEN REWRITE_TAC[h0;cstab]
277 THEN ASM_SIMP_TAC[MOD_LT;h0]
281 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
284 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
287 MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
288 (&2 * h0 < funlist_v39 [(0,1),cstab] (&2 * h0) 3 i (SUC i) \/
289 &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)`]
290 THEN MATCH_DICH_TAC 0
291 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
295 let SCS_5M1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5M1`,
297 SIMP_TAC[scs_5M1;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]
298 THEN REPEAT RESA_TAC;
301 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
304 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
307 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
310 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
313 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
315 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
317 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
319 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
321 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
323 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
326 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
328 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
331 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
333 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
336 THEN REWRITE_TAC[h0;cstab]
339 THEN REWRITE_TAC[h0;cstab]
342 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
347 THEN ASM_SIMP_TAC[h0;cstab;]
348 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
349 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
350 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
351 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
352 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
355 THEN ASM_SIMP_TAC[h0;cstab;]
356 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
357 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
358 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
359 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
360 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`]
361 THEN SUBGOAL_THEN`{i | i < 5 /\
362 (&2 * #1.26 < (if psort 5 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/
363 &2 < (if psort 5 (i,SUC i) = 0,1 then &2 * #1.26 else &2))} ={0}`ASSUME_TAC;
365 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`]
369 THEN POP_ASSUM MP_TAC
370 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 `];
372 ASM_REWRITE_TAC[Geomdetail.CARD_SING]
376 let SCS_5I1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5I1`,
378 REWRITE_TAC[scs_5I1;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.4819 < #0.9`;periodic;SET_RULE`{} (i + 5) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
379 THEN REPEAT RESA_TAC;
382 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
385 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
388 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
391 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
394 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
397 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
400 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
403 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
406 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
409 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
411 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
412 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
416 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
418 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
419 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
423 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
425 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
426 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
430 THEN REWRITE_TAC[h0;cstab]
434 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
438 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
441 ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY]
445 let SCS_5I2_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5I2`,
447 REWRITE_TAC[scs_5I2;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]
448 THEN REPEAT RESA_TAC;
451 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
454 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
457 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
460 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
463 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
466 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
469 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
472 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
475 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
477 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
478 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
482 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
484 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
485 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
489 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
491 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
492 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
496 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
498 THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`]
499 THEN MP_TAC(SET_RULE`(j MOD 5 = SUC i MOD 5 \/ SUC j MOD 5 = i MOD 5)\/ ~(j MOD 5 = SUC i MOD 5 \/ SUC j MOD 5 = i MOD 5)`)
501 THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`];
505 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
506 THEN MP_TAC(SET_RULE`(j = SUC i MOD 5 \/ SUC j MOD 5 = i )\/ ~(j = SUC i MOD 5 \/ SUC j MOD 5 = i)`)
508 THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2];
511 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
514 ASM_SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY]
519 let SCS_5I3_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5I3`,
521 REWRITE_TAC[scs_5I3;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]
522 THEN REPEAT RESA_TAC;
525 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
528 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
531 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
534 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
537 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
540 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
543 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
546 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)/\ SUC (1 * 5 + i)= 1*5+ SUC i`;MOD_MULT_ADD];
549 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
551 THEN MRESA_TAC Terminal.psort_sym[`5`;`i`;`j`];
554 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
556 THEN MRESA_TAC Terminal.psort_sym[`5`;`i`;`j`];
559 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
561 THEN MRESA_TAC Terminal.psort_sym[`5`;`i`;`j`];
564 THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`]
565 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
567 THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2h0]
568 THEN MP_TAC(SET_RULE`psort 5 (i,j) = 0,1\/ ~(psort 5 (i,j) = 0,1)`)
570 THEN SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2h0]
576 THEN ASM_SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2h0;MOD_LT]
580 THEN ASM_SIMP_TAC[h0;cstab;sqrt8_LE_6;REAL_ARITH`&2<= &2 * #1.26/\ a<=a`;LE_sqrt8_2h0;MOD_LT]
581 THEN MP_TAC(SET_RULE`i MOD 5 = SUC i MOD 5\/ ~(i MOD 5 = SUC i MOD 5)`)
583 THEN REWRITE_TAC[REAL_ARITH`&0 <= #3.01`]
584 THEN MP_TAC(SET_RULE`psort 5 (i,SUC i) = 0,1\/ ~(psort 5 (i,SUC i) = 0,1)`)
586 THEN REWRITE_TAC[sqrt8_LE_CSTAB]
587 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
588 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
589 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
590 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
591 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
596 THEN ASM_SIMP_TAC[h0;cstab;]
597 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
598 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
599 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
600 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
601 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`]
602 THEN SUBGOAL_THEN`{i | i < 5 /\
603 (&2 * #1.26 < (if psort 5 (i,SUC i) = 0,1 then sqrt8 else &2 * #1.26) \/
604 &2 < (if psort 5 (i,SUC i) = 0,1 then &2 * #1.26 else &2))}
608 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`]
612 THEN POP_ASSUM MP_TAC
613 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 `;LT_sqrt8_2h0];
615 ASM_REWRITE_TAC[Geomdetail.CARD_SING]
619 let SCS_5M2_IS_SCS=prove_by_refinement(`is_scs_v39 scs_5M2`,
621 SIMP_TAC[scs_5M2;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]
622 THEN REPEAT RESA_TAC;
625 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
628 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
631 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
634 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
637 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
640 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
643 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
646 THEN ASM_SIMP_TAC[ARITH_RULE`i+5= 1*5+i/\ ~(3=0)`;MOD_MULT_ADD];
649 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
651 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
655 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
657 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
661 THEN MP_TAC(SET_RULE`i MOD 5= j MOD 5\/ ~(i MOD 5= j MOD 5)`)
663 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
667 THEN REWRITE_TAC[h0;cstab]
671 THEN REWRITE_TAC[h0;cstab]
675 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
682 THEN ASM_SIMP_TAC[h0;cstab;]
683 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
684 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
685 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
686 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
687 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`2`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
691 THEN ASM_SIMP_TAC[h0;cstab;]
692 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
693 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
694 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
695 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
696 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`]
697 THEN SUBGOAL_THEN`{i | i < 5 /\
698 (&2 * #1.26 < (if psort 5 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/
699 &2 < (if psort 5 (i,SUC i) = 0,1 then &2 else &2))} ={0}`ASSUME_TAC;
701 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`]
705 THEN POP_ASSUM MP_TAC
706 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 `];
709 ASM_REWRITE_TAC[Geomdetail.CARD_SING]
715 let SCS_4M2_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M2`,
717 SIMP_TAC[scs_4M2;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.3789 < #0.9`;periodic;SET_RULE`{} (i + 4) <=> {} i`;periodic2;ARITH_RULE`~(4=0)`;MOD_PERIODIC]
718 THEN REPEAT RESA_TAC;
721 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
724 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
727 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
730 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
733 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
736 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
739 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
742 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
745 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
747 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
751 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
753 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
758 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
760 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
765 THEN REWRITE_TAC[h0;cstab]
769 THEN REWRITE_TAC[h0;cstab]
773 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
780 THEN ASM_SIMP_TAC[h0;cstab;]
781 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
782 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
787 THEN ASM_SIMP_TAC[h0;cstab;]
788 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
789 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`]
790 THEN SUBGOAL_THEN`{i | i < 4 /\
791 (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2 * #1.26) \/
792 &2 < (if psort 4 (i,SUC i) = 0,1 then &2 * #1.26 else &2))} ={0}`ASSUME_TAC;
795 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`]
799 THEN POP_ASSUM MP_TAC
800 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];
802 ASM_REWRITE_TAC[Geomdetail.CARD_SING]
807 let SCS_6M1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_6M1`,
809 REWRITE_TAC[scs_6M1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;]
810 THEN SIMP_TAC[ARITH_RULE`~(6=0)`;MOD_PERIODIC]
811 THEN REPEAT RESA_TAC;
813 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
814 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
817 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
818 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
821 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
822 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
827 REWRITE_TAC[h0;cstab]
830 REWRITE_TAC[h0;cstab]
833 ASM_SIMP_TAC[ARITH_RULE`~(6=0)`;MOD_LT;h0;cstab]
836 REWRITE_TAC[h0;cstab]
839 ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY]
843 let SCS_6T1_IS_SCS=prove_by_refinement(`is_scs_v39 scs_6T1`,
845 REWRITE_TAC[scs_6T1;is_scs_v39;mk_unadorned_v39;scs_v39_explicit;CS_ADJ;]
847 ARITH_RULE`~(6=3)/\ 6-1=5/\ 3<=6/\ 6<=6/\ ~(6=4)/\ ~(6=5)/\ 3<6/\a<=a/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;]
848 THEN SIMP_TAC[periodic;SET_RULE`{} (i + 6) <=> {} i`
849 ;periodic2;ARITH_RULE`~(6=0)`;MOD_PERIODIC]
850 THEN REPEAT RESA_TAC;
852 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
853 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
856 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
857 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
861 GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a=b<=> b=a`]
862 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`a\/b<=> b\/a`]
866 REWRITE_TAC[h0;cstab]
870 ASM_SIMP_TAC[h0;cstab;MOD_LT]
874 ASM_SIMP_TAC[h0;cstab;MOD_LT]
878 ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
879 THEN REWRITE_TAC[REAL_ARITH`~(a<a)/\ ~(&2 * #1.26 < &2)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;h0]
888 let SCS_6I1_BASIC=prove(`scs_basic_v39 scs_6I1`,
891 let SCS_6T1_BASIC=prove(`scs_basic_v39 scs_6T1`,
894 let SCS_6M1_BASIC=prove(`scs_basic_v39 scs_6M1`,
898 let SCS_3M1_BASIC=prove(`scs_basic_v39 scs_3M1`,
902 let SCS_3T1_BASIC=prove(`scs_basic_v39 scs_3T1`,
905 let SCS_3T4_BASIC=prove(`scs_basic_v39 scs_3T4`,
909 let SCS_5M1_BASIC=prove(`scs_basic_v39 scs_5M1`,
912 let SCS_5M2_BASIC=prove(`scs_basic_v39 scs_5M2`,
917 let SCS_5I1_BASIC=prove(`scs_basic_v39 scs_5I1`,
920 let SCS_5I2_BASIC=prove(`scs_basic_v39 scs_5I2`,
923 let SCS_5I3_BASIC=prove(`scs_basic_v39 scs_5I3`,
926 let SCS_4M2_BASIC=prove(`scs_basic_v39 scs_4M2`,
930 let SCS_4M6_BASIC=prove(`scs_basic_v39 scs_4M6'`,
936 let K_SCS_6I1=prove(`scs_k_v39 scs_6I1=6`,
939 let K_SCS_6T1=prove(`scs_k_v39 scs_6T1=6`,
943 let K_SCS_3M1=prove(`scs_k_v39 scs_3M1=3`,
946 let K_SCS_3T1=prove(`scs_k_v39 scs_3T1=3`,
949 let K_SCS_3T4=prove(`scs_k_v39 scs_3T4=3`,
953 let K_SCS_5M1=prove(`scs_k_v39 scs_5M1=5`,
956 let K_SCS_5M2=prove(`scs_k_v39 scs_5M2=5`,
959 let K_SCS_5I1=prove(`scs_k_v39 scs_5I1=5`,
963 let K_SCS_5I2=prove(`scs_k_v39 scs_5I2=5`,
967 let K_SCS_5I3=prove(`scs_k_v39 scs_5I3=5`,
973 let K_SCS_4M2=prove(`scs_k_v39 scs_4M2=4`,
976 let K_SCS_4M6=prove(`scs_k_v39 scs_4M6'=4`,
982 let J_SCS_3M1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3M1 i) i1
986 let J_SCS_3T4=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T4 i) i1
991 let J_SCS_5M1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5M1 i) i1 j= F`,
994 let J_SCS_5I1=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5I1 i) i1 j= F`,
997 let J_SCS_5I2=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5I2 i) i1 j= F`,
1000 let J_SCS_5I3=prove(`scs_J_v39 (scs_prop_equ_v39 scs_5I3 i) i1 j= F`,
1004 let J_SCS_4M2=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M2 i) i1 j= F`,
1007 let J_SCS_4M6=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M6' i) i1 j= F`,
1011 (*******************)
1014 let BASIC_MM_EQ_BBPRIME2=prove(`scs_basic_v39 s ==> MMs_v39 s = BBprime2_v39 s `,
1015 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;MMs_v39;Ayqjtmd.unadorned_MMs]);;
1018 let BASIC_MM_EQ_BBPRIME2_POINT=prove(`scs_basic_v39 s ==> MMs_v39 s v= BBprime2_v39 s v`,
1019 SIMP_TAC [BASIC_MM_EQ_BBPRIME2]);;
1022 let DIST_PSORT=prove(`periodic v (k)/\ ~(k=0) /\ psort (k) (i,j) = psort (k) (i',j')
1023 ==> dist (v i',v j')= dist (v i,v j)`,
1024 REWRITE_TAC[psort;LET_DEF;LET_END_DEF;]
1025 THEN REPEAT STRIP_TAC
1026 THEN POP_ASSUM MP_TAC
1027 THEN MP_TAC(SET_RULE`i MOD k<= j MOD k\/ ~(i MOD k<= j MOD k)`)
1029 THEN MP_TAC(SET_RULE`i' MOD k<= j' MOD k\/ ~(i' MOD k<= j' MOD k)`)
1031 THEN REWRITE_TAC[PAIR_EQ]
1033 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k`;`v`][ARITH_RULE`~(4=0)`;periodic]
1034 THEN THAYTHEL_ASM_TAC 0[`i`][]
1035 THEN THAYTHEL_ASM_TAC 0[`i'`][]
1036 THEN THAYTHEL_ASM_TAC 0[`j`][]
1037 THEN THAYTHEL_ASM_TAC 0[`j'`][]
1038 THEN SIMP_TAC[DIST_SYM]);;
1041 let STAB_BB=prove(`is_scs_v39 s/\ dist(v i,v j) <= cstab/\
1044 BBs_v39 (scs_stab_diag_v39 s i j) v`,
1045 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39]
1046 THEN REPEAT RESA_TAC
1047 THEN THAYTHE_TAC 1[`i'`;`j'`]
1050 THEN MP_TAC(SET_RULE`psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j')\/ ~(psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (i',j'))`)
1052 THEN MP_TAC Wkeidft.PROPERTY_OF_K_SCS
1054 THEN ABBREV_TAC`k= scs_k_v39 s`
1055 THEN MRESA_TAC DIST_PSORT[`k`;`i'`;`j'`;`i`;`v`;`j`]
1059 let SCS_K_D_A_STAB_EQ=prove(`scs_d_v39 (scs_stab_diag_v39 s i j) =scs_d_v39 s
1060 /\ scs_k_v39 (scs_stab_diag_v39 s i j) =scs_k_v39 s
1061 /\(!i' j'. scs_a_v39 (scs_stab_diag_v39 s i j) i' j'= scs_a_v39 s i' j')`,
1062 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39]);;
1065 let DIAG_SCS_M_EQ=prove(`is_scs_v39 s/\ scs_diag (scs_k_v39 s) i j==> scs_M s = scs_M (scs_stab_diag_v39 s i j)`,
1066 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;]
1068 THEN MP_TAC Wkeidft.PROPERTY_OF_K_SCS
1070 THEN ASM_SIMP_TAC[Yrtafyh.DIAG_NOT_PSORT]);;
1073 let DIAD_PSORT_IMP_DIAD=prove_by_refinement(`scs_diag k i j /\ ~(k=0)
1074 /\ psort k (i',j') = psort k (i,j)
1075 ==> scs_diag k i' j'`,
1076 [REWRITE_TAC[scs_diag;psort;LET_DEF;LET_END_DEF]
1079 THEN MP_TAC(SET_RULE`i MOD k<= j MOD k\/ ~(i MOD k<= j MOD k)`)
1081 THEN MP_TAC(SET_RULE`i' MOD k<= j' MOD k\/ ~(i' MOD k<= j' MOD k)`)
1083 THEN REWRITE_TAC[PAIR_EQ]
1086 MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`i`;`k`]
1087 THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`j`;`k`] ;
1089 MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`j`;`k`]
1090 THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`i`;`k`] ;
1093 MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`j`;`k`]
1094 THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`i`;`k`] ;
1096 MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`i'`;`i`;`k`]
1097 THEN MRESA_TAC Zithlqn.IMP_SUC_MOD_EQ[`j'`;`j`;`k`] ]);;
1099 let PEDSLGV1= prove( `!v i j.
1100 v IN MMs_v39 scs_6I1 /\
1102 dist(v i,v j) <= cstab ==>
1103 v IN MMs_v39 (scs_stab_diag_v39 scs_6I1 i j)`,
1105 THEN REPEAT STRIP_TAC
1106 THEN MP_TAC SCS_6I1_IS_SCS
1108 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6I1`;`v`]
1109 THEN MRESA_TAC DIST_LE_IMP_A_LE[`v`;`scs_6I1`;`i`;`j`;`cstab`]
1110 THEN ASSUME_TAC SCS_6I1_BASIC
1111 THEN ASSUME_TAC K_SCS_6I1
1112 THEN MRESAL_TAC Yrtafyh.YRTAFYH[`scs_6I1`;`i`;`j`][ARITH_RULE`3<6`;]
1113 THEN MP_TAC Ppbtydq.MXQTIED
1114 THEN REWRITE_TAC[IN]
1116 THEN MATCH_DICH_TAC 0
1117 THEN EXISTS_TAC`scs_6I1`
1118 THEN ASM_SIMP_TAC[STAB_BB;SCS_K_D_A_STAB_EQ;DIAG_SCS_M_EQ;REAL_ARITH`a<=a`]
1120 THEN REWRITE_TAC[scs_stab_diag_v39;scs_6I1;scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_M;CS_ADJ]
1121 THEN MP_TAC(SET_RULE`psort 6 (i,j) = psort 6 (i',j')\/ ~(psort 6 (i,j) = psort 6 (i',j'))`)
1124 MRESAL_TAC DIAD_PSORT_IMP_DIAD[`i`;`j`;`6`;`i'`;`j'`][ARITH_RULE`~(6=0)`]
1126 THEN REWRITE_TAC[scs_diag;cstab]
1128 THEN REAL_ARITH_TAC;
1132 (****************************)
1133 (****************************)
1134 (****************************)
1135 (****************************)
1140 let K_SCS_6M1=prove(`scs_k_v39 scs_6M1=6/\ scs_d_v39 scs_6M1 = scs_d_v39 scs_6I1`,
1141 REWRITE_TAC[scs_6I1;scs_6M1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39]);;
1144 let D_6M1_EQ_6I1=prove(` scs_d_v39 scs_6M1 = scs_d_v39 scs_6I1
1146 REWRITE_TAC[scs_6I1;scs_6M1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39]);;
1149 let A_6M1_EQ_6I1_EDGE=prove(`(!i j. scs_a_v39 scs_6M1 i (SUC i) = scs_a_v39 scs_6I1 i (SUC i))`,
1150 REWRITE_TAC[scs_6I1;scs_6M1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39]);;
1152 let SCS_M_6I1_EQ_6M1=prove(`scs_M scs_6I1 = scs_M scs_6M1`,
1153 REWRITE_TAC[scs_6I1;scs_6M1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39;scs_M]);;
1157 let BB_6I1_IS_BB_6M1=prove_by_refinement(`BBs_v39 scs_6I1 v/\ (!i j. scs_diag 6 i j ==> cstab <= dist(v i,v j)) ==> BBs_v39 scs_6M1 v`,
1159 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_6I1;scs_6M1;CS_ADJ;scs_diag]
1160 THEN REPEAT RESA_TAC
1161 THEN MP_TAC(SET_RULE`i MOD 6= j MOD 6\/ ~(i MOD 6= j MOD 6)`)
1164 THAYTHE_TAC (5-2)[`i`;`j`];
1166 MP_TAC(SET_RULE`SUC i MOD 6= j MOD 6\/ ~(SUC i MOD 6= j MOD 6)`)
1169 THAYTHE_TAC (6-2)[`i`;`j`];
1171 MP_TAC(SET_RULE`i MOD 6= SUC j MOD 6\/ ~(i MOD 6= SUC j MOD 6)`)
1174 THAYTHE_TAC (7-2)[`i`;`j`];
1176 THAYTHE_TAC (7-4)[`i`;`j`];
1178 THAYTHE_TAC (5-2)[`i`;`j`];
1180 MP_TAC(SET_RULE`SUC i MOD 6= j MOD 6\/ ~(SUC i MOD 6= j MOD 6)`)
1183 THAYTHE_TAC (6-2)[`i`;`j`];
1185 MP_TAC(SET_RULE`i MOD 6= SUC j MOD 6\/ ~(i MOD 6= SUC j MOD 6)`)
1188 THAYTHE_TAC (7-2)[`i`;`j`];
1190 THAYTHE_TAC (7-4)[`i`;`j`]]);;
1192 let A_6I1_LE_A_6M1=prove(`scs_a_v39 scs_6I1 i j <= scs_a_v39 scs_6M1 i j`,
1193 REWRITE_TAC[scs_6I1;scs_6M1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39;h0;cstab]
1194 THEN REAL_ARITH_TAC);;
1196 let B_6I1_LE_B_6M1=prove(`scs_b_v39 scs_6M1 i j = scs_b_v39 scs_6I1 i j`,
1197 REWRITE_TAC[scs_6I1;scs_6M1;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/\ ~(6=0)`;d_tame;REAL_ARITH`#0.712 < #0.9`;periodic;SET_RULE`{} (i + 6) <=> {} i`;periodic2;scs_basic;unadorned_v39;h0;cstab]
1198 THEN REAL_ARITH_TAC);;
1202 let PEDSLGV2= prove(`!v.
1203 v IN MMs_v39 scs_6I1 /\
1204 (!i j. scs_diag 6 i j ==> cstab <= dist(v i,v j)) ==>
1205 v IN MMs_v39 (scs_6M1)`,
1207 THEN REPEAT STRIP_TAC
1208 THEN MP_TAC SCS_6I1_IS_SCS
1210 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6I1`;`v`]
1211 THEN ASSUME_TAC SCS_6I1_BASIC
1212 THEN ASSUME_TAC K_SCS_6I1
1213 THEN ASSUME_TAC SCS_6M1_BASIC
1214 THEN ASSUME_TAC K_SCS_6M1
1215 THEN MP_TAC SCS_6M1_IS_SCS
1217 THEN MP_TAC Ppbtydq.MXQTIED
1218 THEN REWRITE_TAC[IN]
1220 THEN MATCH_DICH_TAC 0
1221 THEN EXISTS_TAC`scs_6I1`
1222 THEN ASM_SIMP_TAC[D_6M1_EQ_6I1;A_6M1_EQ_6I1_EDGE;SCS_M_6I1_EQ_6M1;BB_6I1_IS_BB_6M1;A_6I1_LE_A_6M1;B_6I1_LE_B_6M1;REAL_ARITH`a<=a`]);;
1228 (****************************)
1229 (****************************)
1230 (****************************)
1231 (****************************)
1234 let STAB_6I1_SCS=prove(` scs_diag (scs_k_v39 scs_6I1) i j
1235 ==> is_scs_v39 (scs_stab_diag_v39 scs_6I1 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_6I1 i j)`,
1237 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
1238 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_6I1_IS_SCS;SCS_6I1_BASIC;K_SCS_6I1;
1239 ARITH_RULE`3<6`;LET_DEF;LET_END_DEF;scs_6I1;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
1240 THEN REAL_ARITH_TAC);;
1244 let SCS_DIAG_SCS_6I1_02=prove(`scs_diag (scs_k_v39 scs_6I1) 0 2`,
1245 REWRITE_TAC[K_SCS_6I1;scs_diag]
1249 let SCS_DIAG_SCS_6I1_03=prove(`scs_diag (scs_k_v39 scs_6I1) 0 3`,
1250 REWRITE_TAC[K_SCS_6I1;scs_diag]
1255 let BASIC_HALF_SLICE_STAB=prove(`scs_basic_v39 s
1256 ==> scs_basic_v39 (scs_half_slice_v39 (scs_stab_diag_v39 s i j) p q d' F)`,
1257 ASM_SIMP_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39]
1267 let D_HALF_SLICE=prove(`scs_d_v39 (scs_half_slice_v39 (scs_stab_diag_v39 s i j) p q d' mkj)=d'`,
1270 let BAISC_PROP_EQU=prove(`scs_basic_v39 s ==> scs_basic_v39 (scs_prop_equ_v39 s i)`,
1274 let K_SCS_PROP_EUQ=prove(`scs_k_v39 (scs_prop_equ_v39 s i)= scs_k_v39 s`,
1282 let AQICLXA_SLICE=prove_by_refinement(`scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 2 } { scs_prop_equ_v39 scs_3M1 1, scs_prop_equ_v39 scs_5M1 1}`,
1283 [MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
1284 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_6I1_02;STAB_6I1_SCS;SCS_K_D_A_STAB_EQ;]
1287 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_6I1_02]
1288 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
1289 THEN REPEAT RESA_TAC;
1291 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
1293 THEN MATCH_MP_TAC scs_inj
1294 THEN ASM_SIMP_TAC[SCS_3M1_BASIC;SCS_5M1_BASIC;SCS_6I1_BASIC;J_SCS_5M1;BASIC_HALF_SLICE_STAB;J_SCS_3M1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ]
1297 ASM_SIMP_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1]
1302 ASM_SIMP_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1;scs_6I1;scs_3M1;
1303 ARITH_RULE`(2 + 1 + 6 - 0) MOD 6= 3/\ 0 MOD 6=0/\ a+0=a`;scs_prop_equ_v39]
1304 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1305 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1306 THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort]
1308 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1309 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1311 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1312 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;]
1314 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;Uxckfpe.ARITH_3_TAC]
1315 THEN SIMP_TAC[ARITH_RULE`~(0=2)/\ ~(0=1)/\ 0<=1/\ ~(1=2)`;SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1316 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][Uxckfpe.ARITH_3_TAC]
1317 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][Uxckfpe.ARITH_3_TAC]
1318 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][Uxckfpe.ARITH_3_TAC]
1319 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][Uxckfpe.ARITH_3_TAC]
1320 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][Uxckfpe.ARITH_3_TAC]
1321 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][Uxckfpe.ARITH_3_TAC]
1322 THEN ASM_SIMP_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2`;PAIR_EQ;Uxckfpe.ARITH_3_TAC];
1325 ASM_SIMP_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1;scs_6I1;scs_3M1;
1326 ARITH_RULE`(2 + 1 + 6 - 0) MOD 6= 3/\ 0 MOD 6=0/\ a+0=a`;scs_prop_equ_v39]
1327 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1328 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1329 THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort]
1331 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1332 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1334 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1335 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;]
1337 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;Uxckfpe.ARITH_3_TAC]
1338 THEN SIMP_TAC[ARITH_RULE`~(0=2)/\ ~(0=1)/\ 0<=1/\ ~(1=2)/\ 0<=2/\ 0<=0`;SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ]
1339 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][Uxckfpe.ARITH_3_TAC]
1340 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][Uxckfpe.ARITH_3_TAC]
1341 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][Uxckfpe.ARITH_3_TAC]
1342 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][Uxckfpe.ARITH_3_TAC]
1343 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][Uxckfpe.ARITH_3_TAC]
1344 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][Uxckfpe.ARITH_3_TAC]
1345 THEN ASM_SIMP_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2`;PAIR_EQ;Uxckfpe.ARITH_3_TAC];
1349 ASM_SIMP_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1]
1353 THEN ASM_REWRITE_TAC[scs_half_slice_v39;scs_5M1;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1;scs_6I1;scs_3M1;
1354 ARITH_RULE`(0 + 1 + 6 - 2) MOD 6= 5/\ 2 MOD 6=2/\ a+0=a`;scs_prop_equ_v39]
1355 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1356 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1357 THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort]
1359 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`)
1360 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_5_TAC;DIVISION]
1362 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`)
1363 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_5_TAC;DIVISION;ARITH_RULE`5-1=4`]
1365 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1366 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1367 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`0`;`1`][ARITH_RULE`~(5=0)`]
1368 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`1`;`1`][ARITH_RULE`~(5=0)`]
1369 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`2`;`1`][ARITH_RULE`~(5=0)`]
1370 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`3`;`1`][ARITH_RULE`~(5=0)`]
1371 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x`;`4`;`1`][ARITH_RULE`~(5=0)`]
1372 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`0`;`1`][ARITH_RULE`~(5=0)`]
1373 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`1`;`1`][ARITH_RULE`~(5=0)`]
1374 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`2`;`1`][ARITH_RULE`~(5=0)`]
1375 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`3`;`1`][ARITH_RULE`~(5=0)`]
1376 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`5`;`x'`;`4`;`1`][ARITH_RULE`~(5=0)`]
1378 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/\
1379 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC]
1380 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1381 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1382 THEN REPEAT RESA_TAC
1383 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)
1384 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1385 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2)
1386 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC];
1389 THEN REAL_ARITH_TAC;
1392 THEN REAL_ARITH_TAC;
1395 THEN REAL_ARITH_TAC;
1398 THEN REWRITE_TAC[cstab]
1399 THEN REAL_ARITH_TAC;
1402 THEN REWRITE_TAC[cstab]
1403 THEN REAL_ARITH_TAC;
1406 THEN REWRITE_TAC[J_SCS_3M1]]);;
1410 let FZIOTEF_UNION = prove_by_refinement(
1411 `!S1 S2 S3 S4. scs_arrow_v39 S1 S2 /\ scs_arrow_v39 S3 S4 ==>
1412 scs_arrow_v39 (S1 UNION S3) (S2 UNION S4)`,
1415 REWRITE_TAC[scs_arrow_v39;UNION;IN_ELIM_THM];
1416 REPEAT WEAKER_STRIP_TAC;
1422 let PROP_EQU_IS_SCS=prove(`is_scs_v39 s ==> is_scs_v39 (scs_prop_equ_v39 s i)`,
1423 MRESA_TAC PROP_EQU_IS_SCS[`scs_k_v39 s`;`s`;`i`;`scs_prop_equ_v39 s i`]);;
1426 let AQICLXA=prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 2 } { scs_3M1, scs_5M1 }`,
1427 MATCH_MP_TAC FZIOTEF_TRANS
1428 THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_3M1 1, scs_prop_equ_v39 scs_5M1 1}`
1429 THEN ASM_SIMP_TAC[AQICLXA_SLICE]
1430 THEN REWRITE_TAC[SET_RULE`{a,b}= {a}UNION {b}`]
1431 THEN MATCH_MP_TAC FZIOTEF_UNION
1435 MRESAS_TAC PRO_EQU_ID[`scs_3M1`;`3`;`2`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`3-2 MOD 3=1`]
1436 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1 1`;`2`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`3-1=2`]
1438 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
1440 MRESAS_TAC PRO_EQU_ID[`scs_5M1`;`5`;`4`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_5M1_IS_SCS;K_SCS_5M1;ARITH_RULE`5-4 MOD 5=1`]
1441 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_5M1 1`;`4`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_5M1_IS_SCS;K_SCS_5M1;ARITH_RULE`3-1=2`]
1443 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])]);;
1446 (****************************)
1447 (****************************)
1448 (****************************)
1449 (****************************)
1451 let FUNOUYH_SLICE=prove_by_refinement(`scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 3 } { scs_prop_equ_v39 scs_4M2 1, scs_prop_equ_v39 scs_4M2 1}`,
1453 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
1454 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_6I1_03;STAB_6I1_SCS;SCS_K_D_A_STAB_EQ;]
1457 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_6I1_03]
1458 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
1459 THEN REPEAT RESA_TAC;
1461 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
1463 THEN MATCH_MP_TAC scs_inj
1464 THEN ASM_SIMP_TAC[BAISC_PROP_EQU;K_SCS_PROP_EUQ;BASIC_HALF_SLICE_STAB;SCS_4M2_BASIC;J_SCS_4M2;D_HALF_SLICE;SCS_6I1_BASIC;K_SCS_4M2]
1468 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M2;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1]
1473 THEN ASM_REWRITE_TAC[scs_half_slice_v39;scs_4M2;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2;scs_6I1;scs_3M1;
1474 ARITH_RULE`(3 + 1 + 6 - 0) MOD 6= 4/\ 0 MOD 6=0/\ a+0=a`;scs_prop_equ_v39]
1475 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1476 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1477 THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort]
1479 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`)
1480 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION]
1482 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`)
1483 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1485 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1486 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1487 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
1488 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
1489 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
1490 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
1491 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
1492 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
1493 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
1494 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
1496 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/\
1497 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
1498 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1499 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1500 THEN REPEAT RESA_TAC
1501 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)
1502 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1503 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2)
1504 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC];
1508 ASM_SIMP_TAC[scs_half_slice_v39;scs_4M2;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1]
1513 THEN ASM_REWRITE_TAC[scs_half_slice_v39;scs_4M2;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_6I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2;scs_6I1;scs_3M1;
1514 ARITH_RULE`(0 + 1 + 6 - 3) MOD 6= 4/\ 3 MOD 6=3/\ a+0=a`;scs_prop_equ_v39]
1515 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1516 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1517 THEN ASM_SIMP_TAC[funlist_v39;LET_DEF;LET_END_DEF;CS_ADJ;Uxckfpe.ARITH_6_TAC;psort]
1519 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`)
1520 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION]
1522 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`)
1523 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1525 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1526 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_5_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1527 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
1528 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
1529 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
1530 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
1531 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
1532 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
1533 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
1534 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
1536 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/\
1537 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
1538 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1539 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1540 THEN REPEAT RESA_TAC
1541 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)
1542 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1543 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2)
1544 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\
1545 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC];
1549 THEN REAL_ARITH_TAC;
1552 THEN REAL_ARITH_TAC;
1555 THEN REAL_ARITH_TAC;
1558 THEN REWRITE_TAC[cstab;h0]
1559 THEN REAL_ARITH_TAC;
1562 THEN REWRITE_TAC[cstab;h0]
1563 THEN REAL_ARITH_TAC;
1566 THEN REWRITE_TAC[J_SCS_4M2]]);;
1573 let FZIOTEF=prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 3 } { scs_4M2}`,
1574 MATCH_MP_TAC FZIOTEF_TRANS
1575 THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_4M2 1, scs_prop_equ_v39 scs_4M2 1}`
1576 THEN ASM_SIMP_TAC[FUNOUYH_SLICE]
1577 THEN REWRITE_TAC[SET_RULE`{a,a}= {a}`]
1578 THEN MRESAS_TAC PRO_EQU_ID[`scs_4M2`;`4`;`3`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_4M2_IS_SCS;K_SCS_4M2;ARITH_RULE`4-3 MOD 4=1`]
1579 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M2 1`;`3`][PROP_EQU_IS_SCS;PROP_EQU_IS_SCS;SCS_4M2_IS_SCS;K_SCS_4M2;ARITH_RULE`3-1=2`]
1581 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]));;
1584 (****************************)
1585 (****************************)
1586 (****************************)
1587 (****************************)
1591 let h0_LT_B_SCS_6M1=prove(`
1592 (!i j. scs_diag 6 i j ==> &4 * h0 < scs_b_v39 scs_6M1 i j)
1593 /\ (!i j. scs_diag 6 i j ==> scs_a_v39 scs_6M1 i j <= cstab)`,
1595 THEN REWRITE_TAC[h0;scs_diag]
1596 THEN REPEAT RESA_TAC
1597 THEN REAL_ARITH_TAC);;
1601 let h0_LT_B_SCS_6I1=prove(
1602 `(!i j. scs_diag 6 i j ==> &4 * h0 < scs_b_v39 scs_6I1 i j)
1603 /\ (!i j. scs_diag 6 i j ==> scs_a_v39 scs_6I1 i j <= cstab)`,
1605 THEN REWRITE_TAC[h0;scs_diag;cstab]
1606 THEN REPEAT RESA_TAC
1607 THEN REAL_ARITH_TAC);;
1610 let h0_LT_B_SCS_5I1=prove(`
1611 (!i j. scs_diag 5 i j ==> &4 * h0 < scs_b_v39 scs_5I1 i j)
1612 /\ (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5I1 i j <= cstab)`,
1614 THEN REWRITE_TAC[h0;scs_diag;cstab]
1615 THEN REPEAT RESA_TAC
1616 THEN REAL_ARITH_TAC);;
1619 let h0_LT_B_SCS_5I2=prove(`
1620 (!i j. scs_diag 5 i j ==> &4 * h0 < scs_b_v39 scs_5I2 i j)
1621 /\ (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5I2 i j <= cstab)`,
1623 THEN REWRITE_TAC[h0;scs_diag;cstab]
1624 THEN REPEAT RESA_TAC
1625 THEN MP_TAC sqrt8_LE_CSTAB
1626 THEN REAL_ARITH_TAC);;
1628 let h0_LT_B_SCS_5M2=prove(`
1629 (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5M2 i j <= cstab)`,
1631 THEN REWRITE_TAC[h0;scs_diag;cstab]
1632 THEN REPEAT RESA_TAC
1633 THEN REAL_ARITH_TAC);;
1635 let h0_LT_B_SCS_5M1=prove(` (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5M1 i j <= cstab)`,
1637 THEN REWRITE_TAC[h0;scs_diag;cstab]
1638 THEN REPEAT RESA_TAC
1639 THEN MP_TAC sqrt8_LE_CSTAB
1640 THEN REAL_ARITH_TAC);;
1646 let h0_EQ_B_SCS_6I1=prove(
1647 `(!i j. scs_diag 6 i j ==> scs_b_v39 scs_6I1 i j= &6)
1648 /\ (!i j. scs_diag 6 i j ==> scs_a_v39 scs_6I1 i j= &2 *h0)`,
1650 THEN REWRITE_TAC[h0;scs_diag;cstab]
1651 THEN REPEAT RESA_TAC);;
1655 let h0_EQ_B_SCS_5I1=prove(
1656 `(!i j. scs_diag 5 i j ==> scs_b_v39 scs_5I1 i j= &6)
1657 /\ (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5I1 i j= &2 *h0)`,
1659 THEN REWRITE_TAC[h0;scs_diag;cstab]
1660 THEN REPEAT RESA_TAC);;
1662 let h0_EQ_B_SCS_5I2=prove(
1663 `(!i j. scs_diag 5 i j ==> scs_b_v39 scs_5I2 i j= &6)
1664 /\ (!i j. scs_diag 5 i j ==> scs_a_v39 scs_5I2 i j= sqrt8)`,
1666 THEN REWRITE_TAC[h0;scs_diag;cstab]
1667 THEN REPEAT RESA_TAC);;
1674 let B_LE_CSTAB_6M1=prove(`
1675 (!i. scs_b_v39 scs_6M1 i (SUC i) <= cstab)/\
1676 (!i. scs_b_v39 scs_6M1 i (SUC i) <= &2*h0)/\
1677 (!i. &2< scs_b_v39 scs_6M1 i (SUC i) )/\
1678 (!i. scs_a_v39 scs_6M1 i (SUC i) = &2)`,
1680 THEN SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;h0;cstab]
1681 THEN REAL_ARITH_TAC);;
1684 let B_LE_CSTAB_5I1=prove(`
1685 (!i. scs_b_v39 scs_5I1 i (SUC i) <= cstab)/\
1686 (!i. scs_b_v39 scs_5I1 i (SUC i) <= &2*h0)/\
1687 (!i. &2< scs_b_v39 scs_5I1 i (SUC i) )/\
1688 (!i. scs_a_v39 scs_5I1 i (SUC i) = &2)
1691 THEN SIMP_TAC[ARITH_RULE`1<5`;Qknvmlb.SUC_MOD_NOT_EQ;h0;cstab]
1692 THEN REAL_ARITH_TAC);;
1694 (*********CARD scs_M <=1**************)
1696 let CARD_SCS_M_6M1=prove(`CARD (scs_M scs_6M1) <= 1`,
1697 ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
1699 THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
1702 let SCS_M_6M1=prove(`(scs_M scs_6M1) ={}`,
1703 ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
1705 THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
1710 let SCS_M_6T1=prove(`(scs_M scs_6T1) ={}`,
1711 ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M]
1713 THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;REAL_ARITH`~(a<a)/\ ~(&2 * #1.26 < &2)`;SET_RULE`{i | F}={}`;Oxl_2012.CARD_EMPTY;scs_M;h0]
1716 let CARD_SCS_M_5I1=prove(`CARD (scs_M scs_5I1) <= 1`,
1717 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]
1719 THEN 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]
1723 let SCS_M_5I1=prove(`scs_M scs_5I1 ={}`,
1724 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]
1726 THEN 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]
1730 let SCS_M_5M2=prove(`scs_M scs_5M2 ={0}`,
1731 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]
1733 THEN ASM_SIMP_TAC[h0;cstab;]
1734 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
1735 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
1736 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`4`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
1737 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`5`][scs_diag;Uxckfpe.ARITH_5_TAC;PSORT_5_EXPLICIT]
1738 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`]
1739 THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<5<=> x=0\/ x=1\/x=2\/ x=3\/ x=4`]
1743 THEN POP_ASSUM MP_TAC
1744 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 `];
1748 (*********************)
1751 let SCS_6M1_IMP_SCS_6T1= prove_by_refinement(`main_nonlinear_terminal_v11
1753 v IN MMs_v39 scs_6M1 /\
1754 (!i j. scs_diag 6 i j ==> cstab < dist(v i,v j)) ==>
1755 v IN MMs_v39 (scs_6T1))`,
1757 THEN REPEAT STRIP_TAC
1758 THEN MP_TAC SCS_6M1_IS_SCS
1760 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6M1`;`v`]
1761 THEN ASSUME_TAC SCS_6M1_BASIC
1762 THEN ASSUME_TAC K_SCS_6M1
1763 THEN ASSUME_TAC SCS_6T1_BASIC
1764 THEN ASSUME_TAC K_SCS_6T1
1765 THEN ASSUME_TAC SCS_6T1_IS_SCS
1768 THEN THAYTHES_TAC 0[`scs_6M1`;`v`][ARITH_RULE`3<6`;h0_LT_B_SCS_6M1;B_LE_CSTAB_6M1]
1769 THEN MP_TAC Jcyfmrp.JCYFMRP
1771 THEN THAYTHES_TAC 0[`scs_6M1`;`v`][ARITH_RULE`3<6`;h0_LT_B_SCS_6M1;B_LE_CSTAB_6M1;IN;CARD_SCS_M_6M1]
1772 THEN MP_TAC Jlxfdmj.JLXFDMJ
1774 THEN THAYTHES_TAC 0[`scs_6M1`;`v`;`i`][ARITH_RULE`3<6`;h0_LT_B_SCS_6M1;B_LE_CSTAB_6M1;IN;CARD_SCS_M_6M1;SCS_M_6M1;SET_RULE`(~{} a==> B)<=> B`;ARITH_RULE`i+1=SUC i`]
1775 THEN MP_TAC Ppbtydq.MXQTIED
1776 THEN REWRITE_TAC[IN]
1778 THEN MATCH_DICH_TAC 0
1779 THEN EXISTS_TAC`scs_6M1`
1780 THEN ASM_SIMP_TAC[SCS_M_6M1;SCS_M_6T1]
1789 THEN ASM_SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;ARITH_RULE`~(6<=3)`]
1793 THEN THAYTHE_TAC 1[`i'`;`j`]
1797 THEN MP_TAC(SET_RULE`i' MOD 6= j MOD 6\/ ~(i' MOD 6= j MOD 6)`)
1799 THEN MP_TAC(SET_RULE`SUC i' MOD 6= j MOD 6\/ ~(SUC i' MOD 6= j MOD 6)`)
1802 MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6M1`;`v`]
1803 THEN MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_6M1`;`j`;`v:num->real^3`;`SUC i':num`]
1804 THEN REAL_ARITH_TAC;
1806 MP_TAC(SET_RULE`i' MOD 6=SUC j MOD 6\/ ~( i' MOD 6=SUC j MOD 6)`)
1809 MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_6M1`;`v`]
1810 THEN MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`scs_6M1`;`i'`;`v:num->real^3`;`SUC j:num`]
1811 THEN ONCE_REWRITE_TAC[DIST_SYM]
1812 THEN ASM_REWRITE_TAC[]
1813 THEN REAL_ARITH_TAC;
1820 THEN REWRITE_TAC[h0;scs_diag]
1821 THEN REAL_ARITH_TAC]);;
1823 let SCS_6I1_IMP_SCS_6T1=prove(`main_nonlinear_terminal_v11
1825 v IN MMs_v39 scs_6I1 /\
1826 (!i j. scs_diag 6 i j ==> cstab < dist(v i,v j)) ==>
1827 v IN MMs_v39 (scs_6T1))`,
1829 THEN MP_TAC SCS_6M1_IMP_SCS_6T1
1831 THEN MATCH_DICH_TAC 0
1832 THEN ASM_REWRITE_TAC[]
1833 THEN MATCH_MP_TAC PEDSLGV2
1834 THEN ASM_REWRITE_TAC[]
1835 THEN REPEAT STRIP_TAC
1836 THEN THAYTHE_TAC 1[`i`;`j`]
1838 THEN REAL_ARITH_TAC);;
1842 let SCS_6I1_BERAK_BY_CSTAB= prove_by_refinement(`main_nonlinear_terminal_v11
1844 scs_arrow_v39 { scs_6I1 } ({ scs_6T1}UNION { scs_stab_diag_v39 scs_6I1 i j| scs_diag 6 i j })`,
1846 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN_ELIM_THM;UNION]
1847 THEN ABBREV_TAC`k=scs_k_v39 s`
1848 THEN REPEAT RESA_TAC;
1850 REWRITE_TAC[SCS_6T1_IS_SCS];
1852 MATCH_MP_TAC Yrtafyh.STAB_IS_SCS
1853 THEN ASM_SIMP_TAC[SCS_6I1_IS_SCS;K_SCS_6I1;SCS_6I1_BASIC;ARITH_RULE`3<6`]
1855 THEN REWRITE_TAC[h0;cstab]
1856 THEN REAL_ARITH_TAC;
1858 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_6I1 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_6I1 ==> MMs_v39 s = {}))`);
1863 THEN POP_ASSUM MP_TAC
1864 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
1865 THEN REPEAT STRIP_TAC
1866 THEN POP_ASSUM MP_TAC
1868 THEN POP_ASSUM MP_TAC
1869 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1873 MP_TAC(SET_RULE`(!i j. scs_diag 6 i j ==> cstab < dist(v i,v j))\/ ~((!i j. scs_diag 6 i j ==> cstab < dist((v:num->real^3) i,v j)))`)
1877 THEN ASM_REWRITE_TAC[]
1878 THEN EXISTS_TAC`v:num->real^3`
1879 THEN MP_TAC SCS_6I1_IMP_SCS_6T1
1880 THEN REWRITE_TAC[IN]
1882 THEN MATCH_DICH_TAC 0
1883 THEN ASM_REWRITE_TAC[];
1886 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
1888 THEN MRESAL_TAC PEDSLGV1[`v`;`i`;`j`][IN]
1889 THEN EXISTS_TAC`scs_stab_diag_v39 scs_6I1 i j`
1890 THEN ASM_REWRITE_TAC[]
1893 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
1894 THEN EXISTS_TAC`i:num`
1895 THEN EXISTS_TAC`j:num`
1896 THEN ASM_REWRITE_TAC[];
1898 EXISTS_TAC`v:num->real^3`
1899 THEN ASM_REWRITE_TAC[]]);;
1902 let PSORT_MOD=prove(`~(k=0)==> psort k (i MOD k,j MOD k)= psort k (i,j)`,
1903 SIMP_TAC[psort;MOD_REFL]);;
1907 (****************************)
1908 (****************************)
1909 (****************************)
1910 (****************************)
1914 let STAB_MOD=prove(`is_scs_v39 s
1915 ==> scs_stab_diag_v39 s (i MOD (scs_k_v39 s)) (j MOD (scs_k_v39 s))=scs_stab_diag_v39 s i j`,
1918 THEN ABBREV_TAC`k=scs_k_v39 s`
1919 THEN ASM_SIMP_TAC[PSORT_MOD;ARITH_RULE`3<=k==> ~(k=0)`]);;
1921 let DIAG_MOD=prove(`~(k=0)==> scs_diag k (i MOD k) (j MOD k)= scs_diag k i j`,
1922 SIMP_TAC[scs_diag;MOD_REFL;Hypermap.lemma_suc_mod]);;
1924 let SET_STAB_6I1=prove(`{ scs_stab_diag_v39 scs_6I1 i j| scs_diag 6 i j }= { scs_stab_diag_v39 scs_6I1 (i MOD 6) (j MOD 6)| scs_diag 6 (i MOD 6) (j MOD 6) }`,
1925 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(6=0)`;]
1926 THEN MRESAL_TAC STAB_MOD[`scs_6I1`][SCS_6I1_IS_SCS;K_SCS_6I1]);;
1929 let DIAG_EQ_ADD=prove(`scs_diag 6 (i MOD 6) (j MOD 6)<=>
1930 ((i MOD 6= (j MOD 6+ 2) MOD 6)\/ (i MOD 6= (j MOD 6+ 3) MOD 6)\/
1931 (j MOD 6=(i MOD 6+2) MOD 6)\/ (j MOD 6= (i MOD 6+ 3) MOD 6))`,
1932 REWRITE_TAC[scs_diag]
1933 THEN MP_TAC(ARITH_RULE`i MOD 6<6==> i MOD 6= 0 \/ i MOD 6= 1 \/i MOD 6= 2 \/
1934 i MOD 6= 3 \/i MOD 6= 4 \/i MOD 6= 5
1936 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`]
1938 THEN MP_TAC(ARITH_RULE`j MOD 6<6==> j MOD 6= 0 \/ j MOD 6= 1 \/j MOD 6= 2 \/
1939 j MOD 6= 3 \/j MOD 6= 4 \/j MOD 6= 5
1941 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`]
1946 let PSORT_EQ_SYM=prove(`psort (scs_k_v39 s) (j,i) = psort (scs_k_v39 s) (j',i')
1947 <=> psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (j',i')`,
1948 GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1949 THEN REWRITE_TAC[]);;
1951 let PSORT_EQ_SYM1=prove(`psort (scs_k_v39 s) (j,i) = (j',i')
1952 <=> psort (scs_k_v39 s) (i,j) = (j',i')`,
1953 GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
1954 THEN REWRITE_TAC[]);;
1957 let STAB_SYM=prove(`scs_stab_diag_v39 s i j =
1958 scs_stab_diag_v39 s j i`,
1960 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[PSORT_EQ_SYM]
1961 THEN REWRITE_TAC[]);;
1964 let EXPAND_STAB_DIAG=prove_by_refinement(`{scs_stab_diag_v39 scs_6I1 (i MOD 6) (j MOD 6) | i MOD 6 =
1965 (j MOD 6 + 2) MOD 6 \/
1967 (j MOD 6 + 3) MOD 6 \/
1969 (i MOD 6 + 2) MOD 6 \/
1971 (i MOD 6 + 3) MOD 6}=
1972 {scs_stab_diag_v39 scs_6I1 (i+2) i| i<6} UNION
1973 {scs_stab_diag_v39 scs_6I1 (i+3) i|i<6} `,
1975 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;UNION]
1980 MRESAS_TAC STAB_MOD[`scs_6I1`;`j MOD 6 + 2`;`j MOD 6`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`]
1981 THEN MATCH_MP_TAC (SET_RULE`A==> A\/B`)
1982 THEN EXISTS_TAC`j MOD 6`
1983 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`];
1985 MRESAS_TAC STAB_MOD[`scs_6I1`;`j MOD 6 + 3`;`j MOD 6`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`]
1986 THEN MATCH_MP_TAC (SET_RULE`A==> B\/A`)
1987 THEN EXISTS_TAC`j MOD 6`
1988 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`];
1990 MRESAS_TAC STAB_MOD[`scs_6I1`;`i MOD 6`;`i MOD 6 + 2`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`]
1991 THEN MATCH_MP_TAC (SET_RULE`A==> A\/B`)
1992 THEN EXISTS_TAC`i MOD 6`
1993 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`;STAB_SYM];
1995 MRESAS_TAC STAB_MOD[`scs_6I1`;`i MOD 6`;`i MOD 6 + 3`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`]
1996 THEN MATCH_MP_TAC (SET_RULE`A==> B\/A`)
1997 THEN EXISTS_TAC`i MOD 6`
1998 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`;STAB_SYM];
2001 THEN EXISTS_TAC`i:num`
2002 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`;MOD_LT]
2003 THEN MRESAS_TAC STAB_MOD[`scs_6I1`;`i MOD 6 + 2`;`i MOD 6`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`;MOD_LT];
2006 THEN EXISTS_TAC`i:num`
2007 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(6=0)`;MOD_LT]
2008 THEN MRESAS_TAC STAB_MOD[`scs_6I1`;`i MOD 6 + 3`;`i MOD 6`][SCS_6I1_IS_SCS;K_SCS_6I1;MOD_REFL;ARITH_RULE`~(6=0)`;MOD_LT]]);;
2011 let EQ_DIAG_STAB_6I1_02=prove(`
2013 {scs_stab_diag_v39 scs_6I1 (i + 2) i }
2014 {scs_stab_diag_v39 scs_6I1 0 2}`,
2015 MRESA_TAC STAB_SYM[`scs_6I1`;`2`;`0`]
2016 THEN MP_TAC (GEN_ALL Wkeidft.WKEIDFT)
2017 THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
2019 THEN MATCH_DICH_TAC 0
2020 THEN ASM_SIMP_TAC[ARITH_RULE`2 + i = (i + 2) + 0/\ 3<6/\ i+1= SUC i`;K_SCS_6I1;h0_LT_B_SCS_6I1;h0_EQ_B_SCS_6I1;SCS_6I1_IS_SCS;SCS_6I1_BASIC]
2022 THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
2025 THEN EXISTS_TAC`&2 *h0`
2026 THEN EXISTS_TAC`&2 *h0`
2028 THEN ASM_SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + 2)= i+3/\ SUC i= i+1/\ 2+1=3`;ARITH_RULE`1<6/\ ~(6=0)`;Qknvmlb.SUC_MOD_NOT_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2030 THEN MP_TAC(SET_RULE`i= i+0==> i MOD 6= (i+0) MOD 6`)
2031 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
2033 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`1<6/\ ~(6=0)`]
2037 let EQ_DIAG_STAB_6I1_03=prove(`
2039 {scs_stab_diag_v39 scs_6I1 (i + 3) i }
2040 {scs_stab_diag_v39 scs_6I1 0 3}`,
2041 MRESA_TAC STAB_SYM[`scs_6I1`;`3`;`0`]
2042 THEN MP_TAC (GEN_ALL Wkeidft.WKEIDFT)
2043 THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
2045 THEN MATCH_DICH_TAC 0
2046 THEN ASM_SIMP_TAC[ARITH_RULE`3 + i = (i + 3) + 0/\ 3<6/\ i+1= SUC i`;K_SCS_6I1;h0_LT_B_SCS_6I1;h0_EQ_B_SCS_6I1;SCS_6I1_IS_SCS;SCS_6I1_BASIC]
2048 THEN ASM_SIMP_TAC[ARITH_RULE`1<6`;Qknvmlb.SUC_MOD_NOT_EQ;]
2051 THEN EXISTS_TAC`&2 *h0`
2052 THEN EXISTS_TAC`&2 *h0`
2054 THEN ASM_SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + 3)= i+4/\ SUC i= i+1/\ 3+1=4`;ARITH_RULE`1<6/\ ~(6=0)`;Qknvmlb.SUC_MOD_NOT_EQ;]
2056 THEN MP_TAC(SET_RULE`i= i+0==> i MOD 6= (i+0) MOD 6`)
2057 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
2059 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`1<6/\ ~(6=0)`]
2063 let SET_EQ_DIAG_STAB_6I1_02=prove(`
2065 {scs_stab_diag_v39 scs_6I1 (i + 2) i |i<6}
2066 {scs_stab_diag_v39 scs_6I1 0 2}`,
2067 REWRITE_TAC[ARITH_RULE`i<6<=> i=0\/i=1\/i=2\/i=3\/i=4\/i=5`;SET_RULE`{scs_stab_diag_v39 scs_6I1 (i + 2) i |i=0\/i=1\/i=2\/i=3\/i=4\/i=5}
2068 = {scs_stab_diag_v39 scs_6I1 (0 + 2) 0} UNION
2069 {scs_stab_diag_v39 scs_6I1 (1 + 2) 1} UNION
2070 {scs_stab_diag_v39 scs_6I1 (2 + 2) 2} UNION
2071 {scs_stab_diag_v39 scs_6I1 (3 + 2) 3} UNION
2072 {scs_stab_diag_v39 scs_6I1 (4 + 2) 4} UNION
2073 {scs_stab_diag_v39 scs_6I1 (5 + 2) 5}
2075 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`]
2076 THEN MATCH_MP_TAC FZIOTEF_UNION
2077 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02]
2078 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`]
2079 THEN MATCH_MP_TAC FZIOTEF_UNION
2080 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02]
2081 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`]
2082 THEN MATCH_MP_TAC FZIOTEF_UNION
2083 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02]
2084 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`]
2085 THEN MATCH_MP_TAC FZIOTEF_UNION
2086 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02]
2087 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2}={scs_stab_diag_v39 scs_6I1 0 2} UNION {scs_stab_diag_v39 scs_6I1 0 2}`]
2088 THEN MATCH_MP_TAC FZIOTEF_UNION
2089 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_02]);;
2094 let SET_EQ_DIAG_STAB_6I1_03=prove(`
2096 {scs_stab_diag_v39 scs_6I1 (i + 3) i |i<6}
2097 {scs_stab_diag_v39 scs_6I1 0 3}`,
2098 REWRITE_TAC[ARITH_RULE`i<6<=> i=0\/i=1\/i=2\/i=3\/i=4\/i=5`;SET_RULE`{scs_stab_diag_v39 scs_6I1 (i + 3) i |i=0\/i=1\/i=2\/i=3\/i=4\/i=5}
2099 = {scs_stab_diag_v39 scs_6I1 (0 + 3) 0} UNION
2100 {scs_stab_diag_v39 scs_6I1 (1 + 3) 1} UNION
2101 {scs_stab_diag_v39 scs_6I1 (2 + 3) 2} UNION
2102 {scs_stab_diag_v39 scs_6I1 (3 + 3) 3} UNION
2103 {scs_stab_diag_v39 scs_6I1 (4 + 3) 4} UNION
2104 {scs_stab_diag_v39 scs_6I1 (5 + 3) 5}
2106 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`]
2107 THEN MATCH_MP_TAC FZIOTEF_UNION
2108 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03]
2109 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`]
2110 THEN MATCH_MP_TAC FZIOTEF_UNION
2111 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03]
2112 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`]
2113 THEN MATCH_MP_TAC FZIOTEF_UNION
2114 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03]
2115 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`]
2116 THEN MATCH_MP_TAC FZIOTEF_UNION
2117 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03]
2118 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_6I1 0 3}={scs_stab_diag_v39 scs_6I1 0 3} UNION {scs_stab_diag_v39 scs_6I1 0 3}`]
2119 THEN MATCH_MP_TAC FZIOTEF_UNION
2120 THEN ASM_SIMP_TAC[EQ_DIAG_STAB_6I1_03]);;
2122 let SET_EQ_DIAG_STAB_6I1=prove( `scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 i j| scs_diag 6 i j }
2123 { scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}`,
2124 ONCE_REWRITE_TAC[SET_STAB_6I1]
2125 THEN REWRITE_TAC[DIAG_EQ_ADD;EXPAND_STAB_DIAG;SET_RULE`{scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}
2126 ={scs_stab_diag_v39 scs_6I1 0 2}UNION{ scs_stab_diag_v39 scs_6I1 0 3}`]
2127 THEN MATCH_MP_TAC FZIOTEF_UNION
2128 THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_6I1_02;SET_EQ_DIAG_STAB_6I1_03]);;
2134 let OEHDBEN_PRIME=prove( `
2135 main_nonlinear_terminal_v11
2137 scs_arrow_v39 { scs_6I1 } { scs_6T1, scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}`,
2139 THEN MATCH_MP_TAC FZIOTEF_TRANS
2140 THEN EXISTS_TAC`{ scs_6T1}UNION { scs_stab_diag_v39 scs_6I1 i j| scs_diag 6 i j }`
2141 THEN ASM_SIMP_TAC[SCS_6I1_BERAK_BY_CSTAB;SET_RULE`{scs_6T1, scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}
2142 ={scs_6T1}UNION{ scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}`]
2143 THEN MATCH_MP_TAC FZIOTEF_UNION
2144 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_6I1;]
2145 THEN MATCH_MP_TAC FZIOTEF_REFL
2146 THEN REWRITE_TAC[IN_SING]
2147 THEN REPEAT RESA_TAC
2148 THEN ASM_REWRITE_TAC[SCS_6T1_IS_SCS]);;
2152 let OEHDBEN= prove(`main_nonlinear_terminal_v11
2154 scs_arrow_v39 { scs_6I1 } { scs_6T1, scs_5M1, scs_4M2, scs_3M1 }`,
2156 THEN MATCH_MP_TAC FZIOTEF_TRANS
2157 THEN EXISTS_TAC`{ scs_6T1, scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}`
2158 THEN ASM_SIMP_TAC[OEHDBEN_PRIME;SET_RULE`{scs_6T1, scs_stab_diag_v39 scs_6I1 0 2, scs_stab_diag_v39 scs_6I1 0 3}
2159 = {scs_6T1} UNION {scs_stab_diag_v39 scs_6I1 0 2} UNION{ scs_stab_diag_v39 scs_6I1 0 3}`;
2160 SET_RULE`{ scs_6T1, scs_5M1, scs_4M2, scs_3M1 }={scs_6T1} UNION{ scs_3M1,scs_5M1}UNION {scs_4M2}`]
2161 THEN MATCH_MP_TAC FZIOTEF_UNION
2164 MATCH_MP_TAC FZIOTEF_REFL
2165 THEN REWRITE_TAC[IN_SING]
2166 THEN REPEAT RESA_TAC
2167 THEN ASM_REWRITE_TAC[SCS_6T1_IS_SCS];
2170 MATCH_MP_TAC FZIOTEF_UNION
2171 THEN ASM_REWRITE_TAC[AQICLXA;FZIOTEF]]);;
2182 let check_completeness_claimA_concl =
2183 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)