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 Miqmcsn = struct
28 open Wrgcvdr_cizmrrh;;
36 open Flyspeck_constants;;
52 open Wrgcvdr_cizmrrh;;
54 open Flyspeck_constants;;
102 (**************************************************)
104 let scs_3T4_prime2 = (* terminal_tri_6833979866 = *) new_definition
105 `scs_3T4_prime2 = mk_unadorned_v39 3
107 (funlist_v39 [(0,1),(&2);(0,2),cstab] (&2*h0) 3)
108 (funlist_v39 [(0,1),(&2 * h0)] (cstab) 3)`;;
113 let scs_3T3_prime = (* terminal_tri_6833979866 = *) new_definition
114 `scs_3T3_prime = mk_unadorned_v39 3
116 (funlist_v39 [(0,1),cstab] (&2*h0) 3)
117 (funlist_v39 [] (cstab) 3)`;;
122 let scs_3M1_prime = new_definition
123 `scs_3M1_prime = mk_unadorned_v39 3 (#0.103)
124 (funlist_v39 [(0,1),(cstab)] (&2) 3)
125 (funlist_v39 [(0,1),(cstab)] (&2 * h0) 3)`;;
129 let scs_4M8_02 = new_definition
130 `scs_4M8_02 = mk_unadorned_v39 4 (#0.513)
131 (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(cstab);(1,3),(cstab)] (&2) 4)
132 (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(#3.62);(1,3),(&6)] (&2) 4)`;;
135 let scs_4M8_13 = new_definition
136 `scs_4M8_13 = mk_unadorned_v39 4 (#0.513)
137 (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(cstab);(1,3),(cstab)] (&2) 4)
138 (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(&6);(1,3),(#3.62)] (&2) 4)`;;
142 let PSORT_5_EXPLICIT=prove(`
143 psort 5 (0,0)= (0,0)/\
144 psort 5 (1,1)= (1,1)/\
145 psort 5 (2,2)= (2,2)/\
146 psort 5 (3,3)= (3,3)/\
147 psort 5 (4,4)= (4,4)/\
148 psort 5 (0,1)= (0,1)/\
149 psort 5 (0,2)= (0,2)/\
150 psort 5 (0,3)= (0,3)/\
151 psort 5 (0,4)= (0,4)/\
152 psort 5 (1,0)= (0,1)/\
153 psort 5 (1,2)= (1,2)/\
154 psort 5 (1,3)= (1,3)/\
155 psort 5 (1,4)= (1,4)/\
156 psort 5 (2,0)= (0,2)/\
157 psort 5 (2,1)= (1,2)/\
158 psort 5 (2,3)= (2,3)/\
159 psort 5 (2,4)= (2,4)/\
160 psort 5 (3,0)= (0,3)/\
161 psort 5 (3,1)= (1,3)/\
162 psort 5 (3,2)= (2,3)/\
163 psort 5 (3,4)= (3,4)/\
164 psort 5 (4,0)= (0,4)/\
165 psort 5 (4,1)= (1,4)/\
166 psort 5 (4,2)= (2,4)/\
167 psort 5 (4,3)= (3,4)/\
168 psort 5 (4,5)= (0,4)/\
169 psort 5 (3,5)= (0,3)/\
170 psort 5 (2,5)= (0,2)/\
171 psort 5 (1,5)= (0,1)/\
172 psort 5 (5,1)= (0,1)/\
173 psort 5 (5,2)= (0,2)/\
174 psort 5 (5,3)= (0,3)/\
175 psort 5 (5,4)= (0,4)/\
176 psort 5 (5,5)= (0,0)/\
177 psort 5 (5,6)= (0,1)/\
178 psort 5 (5,7)= (0,2)/\
179 psort 5 (4,6)= (1,4)/\
180 psort 5 (6,4)= (1,4)/\
181 psort 5 (6,5)= (0,1)/\
182 psort 5 (6,7)= (1,2)/\
183 psort 5 (7,5)= (0,2)/\
184 psort 5 (7,6)= (1,2)/\
185 psort 5 (7,7)= (2,2)/\
186 psort 5 (6,6)= (1,1)/\
187 psort 4 (3,4)= (0,3)/\
188 psort 3 (2,0)= (0,2)/\
189 psort 3 (2,1)= (1,2)/\
190 psort 3 (1,0)= (0,1)/\
191 psort 4 (0,0)= (0,0)/\
192 psort 4 (1,1)= (1,1)/\
193 psort 4 (2,2)= (2,2)/\
194 psort 4 (3,3)= (3,3)/\
195 psort 4 (4,3)= (0,3)/\
196 psort 4 (4,4)= (0,0)/\
197 psort 4 (0,2)= (0,2)/\
198 psort 4 (4,5)= (0,1)/\
199 psort 4 (5,4)= (0,1)/\
200 psort 4 (5,5)= (1,1)/\
201 psort 4 (1,4)= (0,1)/\
202 psort 4 (2,5)= (1,2)/\
205 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/\ 6 MOD 4=2`]);;
213 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;
214 Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_5_TAC;
215 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;scs_4I2;scs_4T1;scs_4T2;scs_4I1;scs_4T4;scs_4I3;scs_3T3;scs_4T5;scs_3T4_prime2;scs_3T3_prime;scs_3M1_prime;scs_4T3;scs_4M8_02;scs_4M8_13;scs_3T7;
216 Terminal.FUNLIST_EXPLICIT;Yrtafyh.PSORT_PERIODIC;PSORT_5_EXPLICIT;
217 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/\ 6 MOD 4=2`];;
220 (********************)
222 let SCS_4T3_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4T3`,
223 [SIMP_TAC[scs_4T3;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]
224 THEN REPEAT RESA_TAC;
227 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
230 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
233 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
236 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
239 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
243 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
248 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
253 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
258 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
260 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
264 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
266 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
270 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
272 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
276 THEN REWRITE_TAC[h0;cstab]
283 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
287 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
298 THEN ASM_SIMP_TAC[h0;cstab;]
299 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
300 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
307 THEN ASM_SIMP_TAC[h0;cstab;]
308 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
309 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`]
310 THEN SUBGOAL_THEN`{i | i < 4 /\
311 (&2 * #1.26 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2 ) \/
312 &2 < (if psort 4 (i,SUC i) = 0,1 then #3.01 else &2))} ={0}`ASSUME_TAC
315 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`]
319 THEN POP_ASSUM MP_TAC
320 THEN ASM_SIMP_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01/\ ~(&2 * #1.26 < &2) `;PSORT_5_EXPLICIT;LT_sqrt8_2h0];
323 ASM_REWRITE_TAC[Geomdetail.CARD_SING]
329 let SCS_4M8_02_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M8_02`,
331 SIMP_TAC[scs_4M8_02;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]
332 THEN REPEAT RESA_TAC;
335 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
338 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
341 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
344 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
347 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
351 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
356 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
361 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
366 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
368 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
372 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
374 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
378 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
380 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
384 THEN REWRITE_TAC[h0;cstab]
391 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
395 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
406 THEN ASM_SIMP_TAC[h0;cstab;]
407 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
408 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
415 THEN ASM_SIMP_TAC[h0;cstab;]
416 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
417 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`]
418 THEN SUBGOAL_THEN`{i | i < 4 /\
420 (if psort 4 (i,SUC i) = 0,1
422 else if psort 4 (i,SUC i) = 2,3 then #3.01 else &2) \/
424 (if psort 4 (i,SUC i) = 0,1
426 else if psort 4 (i,SUC i) = 2,3 then #3.01 else &2))} ={0,2}`ASSUME_TAC
429 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`;SET_RULE`a IN {b,c}<=>a=b\/ a=c`]
433 THEN POP_ASSUM MP_TAC
434 THEN ASM_SIMP_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01/\ ~(&2 * #1.26 < &2) `;PSORT_5_EXPLICIT;LT_sqrt8_2h0;];
437 ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=2)`]
443 let SCS_4M8_13_IS_SCS=prove_by_refinement(`is_scs_v39 scs_4M8_13`,
445 SIMP_TAC[scs_4M8_13;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]
446 THEN REPEAT RESA_TAC;
449 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
452 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
455 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
458 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
461 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
465 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
470 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
475 THEN ASM_SIMP_TAC[ARITH_RULE`i+4= 1*4+i/\ ~(3=0)`;MOD_MULT_ADD];
480 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
482 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
486 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
488 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
492 THEN MP_TAC(SET_RULE`i MOD 4= j MOD 4\/ ~(i MOD 4= j MOD 4)`)
494 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
498 THEN REWRITE_TAC[h0;cstab]
505 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
509 THEN ASM_SIMP_TAC[h0;cstab;MOD_LT]
520 THEN ASM_SIMP_TAC[h0;cstab;]
521 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
522 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`1`;`3`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
529 THEN ASM_SIMP_TAC[h0;cstab;]
530 THEN MRESAS_TAC Yrtafyh.DIAG_NOT_PSORT[`0`;`2`;`4`][scs_diag;Uxckfpe.ARITH_4_TAC;Terminal.FUNLIST_EXPLICIT]
531 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`]
532 THEN SUBGOAL_THEN`{i | i < 4 /\
534 (if psort 4 (i,SUC i) = 0,1
536 else if psort 4 (i,SUC i) = 2,3 then #3.01 else &2) \/
538 (if psort 4 (i,SUC i) = 0,1
540 else if psort 4 (i,SUC i) = 2,3 then #3.01 else &2))} ={0,2}`ASSUME_TAC
543 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING;ARITH_RULE`x<4<=> x=0\/ x=1\/x=2\/ x=3`;SET_RULE`a IN {b,c}<=>a=b\/ a=c`]
547 THEN POP_ASSUM MP_TAC
548 THEN ASM_SIMP_TAC[Terminal.FUNLIST_EXPLICIT;ARITH_RULE`SUC 1=2`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;REAL_ARITH`~(a<a)/\ &2 * #1.26 < #3.01/\ ~(&2 * #1.26 < &2) `;PSORT_5_EXPLICIT;LT_sqrt8_2h0;];
551 ASM_SIMP_TAC[Planarity.CARD_2_FAN;ARITH_RULE`~(0=2)`]
558 let SCS_3T4_prime2_IS_SCS=prove_by_refinement( `is_scs_v39 scs_3T4_prime2`,
559 [SIMP_TAC[scs_3T4_prime2;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]
560 THEN REPEAT RESA_TAC;
563 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
566 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
569 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
572 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
575 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
578 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
581 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
584 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
587 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
589 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
593 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
595 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
599 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
601 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
605 THEN REWRITE_TAC[h0;cstab]
611 THEN ASM_SIMP_TAC[MOD_LT;h0;cstab]
615 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
619 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
622 MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
623 (&2 * h0 < funlist_v39 [(0,1),&2 * h0] cstab 3 i (SUC i) \/
624 &2 < funlist_v39 [(0,1),&2; (0,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)`]
625 THEN MATCH_DICH_TAC 0
626 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
630 let SCS_3T3_prime_IS_SCS=prove_by_refinement( `is_scs_v39 scs_3T3_prime`,
631 [SIMP_TAC[scs_3T3_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.476 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
632 THEN REPEAT RESA_TAC;
635 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
638 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
641 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
644 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
647 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
650 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
653 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
656 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
659 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
661 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
665 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
667 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
671 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
673 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
677 THEN REWRITE_TAC[h0;cstab]
683 THEN ASM_SIMP_TAC[MOD_LT;h0;cstab]
687 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
691 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
694 MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
695 (&2 * h0 < funlist_v39 [] cstab 3 i (SUC i) \/
696 &2 < funlist_v39 [(0,1),cstab] (&2 * h0) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`]
697 THEN MATCH_DICH_TAC 0
698 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
703 let SCS_3M1_prime_IS_SCS=prove_by_refinement( `is_scs_v39 scs_3M1_prime`,
704 [SIMP_TAC[scs_3M1_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.103 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
705 THEN REPEAT RESA_TAC;
708 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
711 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
714 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
717 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
720 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
723 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
726 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
729 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
732 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
734 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
738 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
740 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
744 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
746 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
750 THEN REWRITE_TAC[h0;cstab]
756 THEN ASM_SIMP_TAC[MOD_LT;h0;cstab]
760 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
764 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
767 MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
768 (&2 * h0 < funlist_v39 [(0,1),cstab] (&2 * h0) 3 i (SUC i) \/
769 &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)`]
770 THEN MATCH_DICH_TAC 0
771 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
775 let SCS_3T7_IS_SCS=prove_by_refinement( `is_scs_v39 scs_3T7`,
776 [SIMP_TAC[scs_3T7;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.2565 < #0.9`;periodic;SET_RULE`{} (i + 3) <=> {} i`;periodic2;ARITH_RULE`~(3=0)`;MOD_PERIODIC]
777 THEN REPEAT RESA_TAC;
780 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
783 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
786 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
789 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
792 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
795 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
798 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
801 THEN ASM_SIMP_TAC[ARITH_RULE`i+3= 1*3+i/\ ~(3=0)`;MOD_MULT_ADD];
804 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
806 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
810 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
812 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
816 THEN MP_TAC(SET_RULE`i MOD 3= j MOD 3\/ ~(i MOD 3= j MOD 3)`)
818 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[Terminal.psort_sym]
822 THEN REWRITE_TAC[h0;cstab]
828 THEN ASM_SIMP_TAC[MOD_LT;h0;cstab]
832 THEN ASM_SIMP_TAC[MOD_LT;cstab;h0]
838 MRESAS_TAC CARD_SUBSET[`{i | i < 3 /\
840 funlist_v39 [(0,1),#3.62; (0,2),cstab; (1,2),&2] (&2) 3 i (SUC i) \/
841 &2 < funlist_v39 [(0,1),cstab; (0,2),cstab; (1,2),&2] (&2) 3 i (SUC i))}`;`0..2`][FINITE_NUMSEG;CARD_NUMSEG;ARITH_RULE`(2+1)-0=3/\ (a+3<=6 <=> a<=3)`]
842 THEN MATCH_DICH_TAC 0
843 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG]
847 (*********************)
850 let SCS_3T4_prime2_BASIC=prove(`scs_basic_v39 scs_3T4_prime2`,
853 let K_SCS_3T4_prime2=prove(`scs_k_v39 scs_3T4_prime2=3`,
856 let J_SCS_3T4_prime2=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T4_prime2 i) i1 j= F`,
859 let J_SCS_3T4_prime2_1=prove(`scs_J_v39 (scs_3T4_prime2 ) i1 j= F`,
862 let SCS_3T7_BASIC=prove(`scs_basic_v39 scs_3T7`,
865 let K_SCS_3T7=prove(`scs_k_v39 scs_3T7=3`,
868 let J_SCS_3T7=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T7 i) i1 j= F`,
873 let J_SCS_3T7_1=prove(`scs_J_v39 (scs_3T7 ) i1 j= F`,
876 let SCS_3T3_prime_BASIC=prove(`scs_basic_v39 scs_3T3_prime`,
879 let K_SCS_3T3_prime=prove(`scs_k_v39 scs_3T3_prime=3`,
882 let J_SCS_3T3_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3T3_prime i) i1 j= F`,
886 let SCS_3M1_prime_BASIC=prove(`scs_basic_v39 scs_3M1_prime`,
889 let K_SCS_3M1_prime=prove(`scs_k_v39 scs_3M1_prime=3`,
892 let J_SCS_3M1_prime=prove(`scs_J_v39 (scs_prop_equ_v39 scs_3M1_prime i) i1 j= F`,
896 let SCS_4T3_BASIC=prove(`scs_basic_v39 scs_4T3`,
899 let K_SCS_4T3=prove(`scs_k_v39 scs_4T3=4`,
902 let J_SCS_4T3=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4T3 i) i1 j= F`,
906 let SCS_4M8_02_BASIC=prove(`scs_basic_v39 scs_4M8_02`,
909 let K_SCS_4M8_02=prove(`scs_k_v39 scs_4M8_02=4`,
912 let J_SCS_4M8_02=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M8_02 i) i1 j= F`,
916 let SCS_4M8_13_BASIC=prove(`scs_basic_v39 scs_4M8_13`,
919 let K_SCS_4M8_13=prove(`scs_k_v39 scs_4M8_13=4`,
922 let J_SCS_4M8_13=prove(`scs_J_v39 (scs_prop_equ_v39 scs_4M8_13 i) i1 j= F`,
925 (***********************)
927 let BB_3T4_prime2_IMP_scs_3T4=prove(`BBs_v39 scs_3T4_prime2 v
929 BBs_v39 (scs_3T4 ) v`,
930 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_prime2;scs_prop_equ_v39;]
931 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
934 THEN THAYTHE_TAC 0[`i`;`j`]
936 THEN REWRITE_TAC[cstab;h0]
937 THEN REAL_ARITH_TAC);;
940 let MM_3T4_prime2_IMP_MM_3T4=prove(`MMs_v39 scs_3T4_prime2 v ==> ~(MMs_v39 scs_3T4={})`,
942 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
943 THEN EXISTS_TAC`v:num->real^3`
944 THEN EXISTS_TAC`scs_3T4_prime2`
945 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_3T4_prime2`;`v`]
946 THEN ASM_SIMP_TAC[SCS_3T4_BASIC;SCS_3T4_prime2_BASIC;SCS_3T4_IS_SCS;SCS_3T4_IS_SCS;
947 SCS_3T4_prime2_IS_SCS;K_SCS_3T4;K_SCS_3T4_prime2;IN;BB_3T4_prime2_IMP_scs_3T4]
949 THEN REAL_ARITH_TAC);;
952 let SCS_3T4_prime2_ARROW_MM_3T4=prove_by_refinement(`scs_arrow_v39 {scs_3T4_prime2 } { scs_3T4}`,
954 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
955 THEN ABBREV_TAC`k=scs_k_v39 s`
956 THEN REPEAT RESA_TAC;
958 ASM_SIMP_TAC[SCS_3T4_IS_SCS];
960 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_3T4_prime2 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_3T4_prime2 ==> MMs_v39 s = {}))`);
965 THEN POP_ASSUM MP_TAC
966 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
967 THEN REPEAT STRIP_TAC
968 THEN POP_ASSUM MP_TAC
970 THEN EXISTS_TAC`scs_3T4`
971 THEN ASM_REWRITE_TAC[]
972 THEN MATCH_MP_TAC (GEN_ALL MM_3T4_prime2_IMP_MM_3T4)
973 THEN POP_ASSUM MP_TAC
976 (************************************)
982 let BB_3T3_prime_IMP_scs_3T3=prove(`BBs_v39 scs_3T3_prime v
984 BBs_v39 (scs_3T3 ) v`,
985 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_3T3_prime;scs_prop_equ_v39;]
986 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
989 THEN THAYTHE_TAC 0[`i`;`j`]
991 THEN REWRITE_TAC[cstab;h0]
992 THEN REAL_ARITH_TAC);;
994 let MM_3T3_prime_IMP_MM_3T3=prove(`MMs_v39 scs_3T3_prime v ==> ~(MMs_v39 scs_3T3={})`,
996 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
997 THEN EXISTS_TAC`v:num->real^3`
998 THEN EXISTS_TAC`scs_3T3_prime`
999 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_3T3_prime`;`v`]
1000 THEN ASM_SIMP_TAC[SCS_3T3_BASIC;SCS_3T3_prime_BASIC;SCS_3T3_IS_SCS;SCS_3T3_IS_SCS;
1001 SCS_3T3_prime_IS_SCS;K_SCS_3T3;K_SCS_3T3_prime;IN;BB_3T3_prime_IMP_scs_3T3]
1003 THEN REAL_ARITH_TAC);;
1005 let SCS_3T3_prime_ARROW_MM_3T3=prove_by_refinement(`scs_arrow_v39 {scs_3T3_prime } { scs_3T3}`,
1007 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
1008 THEN ABBREV_TAC`k=scs_k_v39 s`
1009 THEN REPEAT RESA_TAC;
1011 ASM_SIMP_TAC[SCS_3T3_IS_SCS];
1013 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_3T3_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_3T3_prime ==> MMs_v39 s = {}))`);
1018 THEN POP_ASSUM MP_TAC
1019 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
1020 THEN REPEAT STRIP_TAC
1021 THEN POP_ASSUM MP_TAC
1023 THEN EXISTS_TAC`scs_3T3`
1024 THEN ASM_REWRITE_TAC[]
1025 THEN MATCH_MP_TAC (GEN_ALL MM_3T3_prime_IMP_MM_3T3)
1026 THEN POP_ASSUM MP_TAC
1029 (************************)
1033 let BB_3M1_prime_IMP_scs_3M1=prove(`BBs_v39 scs_3M1_prime v
1035 BBs_v39 (scs_3M1 ) v`,
1036 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_3M1_prime;scs_prop_equ_v39;]
1037 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
1039 THEN REPEAT RESA_TAC
1040 THEN THAYTHE_TAC 0[`i`;`j`]
1042 THEN REWRITE_TAC[cstab;h0]
1043 THEN REAL_ARITH_TAC);;
1045 let MM_3M1_prime_IMP_MM_3M1=prove(`MMs_v39 scs_3M1_prime v ==> ~(MMs_v39 scs_3M1={})`,
1047 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
1048 THEN EXISTS_TAC`v:num->real^3`
1049 THEN EXISTS_TAC`scs_3M1_prime`
1050 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_3M1_prime`;`v`]
1051 THEN ASM_SIMP_TAC[SCS_3M1_BASIC;SCS_3M1_prime_BASIC;SCS_3M1_IS_SCS;SCS_3M1_IS_SCS;
1052 SCS_3M1_prime_IS_SCS;K_SCS_3M1;K_SCS_3M1_prime;IN;BB_3M1_prime_IMP_scs_3M1]
1054 THEN REAL_ARITH_TAC);;
1056 let SCS_3M1_prime_ARROW_MM_3M1=prove_by_refinement(`scs_arrow_v39 {scs_3M1_prime } { scs_3M1}`,
1058 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
1059 THEN ABBREV_TAC`k=scs_k_v39 s`
1060 THEN REPEAT RESA_TAC;
1062 ASM_SIMP_TAC[SCS_3M1_IS_SCS];
1064 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_3M1_prime ==> MMs_v39 s = {}) \/ ~((!s. s = scs_3M1_prime ==> MMs_v39 s = {}))`);
1069 THEN POP_ASSUM MP_TAC
1070 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
1071 THEN REPEAT STRIP_TAC
1072 THEN POP_ASSUM MP_TAC
1074 THEN EXISTS_TAC`scs_3M1`
1075 THEN ASM_REWRITE_TAC[]
1076 THEN MATCH_MP_TAC (GEN_ALL MM_3M1_prime_IMP_MM_3M1)
1077 THEN POP_ASSUM MP_TAC
1081 (*************************)
1086 let BB_4M7_IMP_BB_STAN_4M7= prove(`
1087 BBs_v39 scs_4M7 v /\
1089 dist(v i,v j)<= cstab ==>
1090 BBs_v39 (scs_stab_diag_v39 scs_4M7 i j) v`,
1091 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M7;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M7;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7]
1092 THEN REPEAT RESA_TAC
1093 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
1095 THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
1097 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
1099 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M7;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M7;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7;SCS_4M7_IS_SCS]
1100 THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
1101 THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
1103 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M7;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M7;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7;SCS_4M7_IS_SCS]
1104 THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
1105 THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
1106 THEN ONCE_REWRITE_TAC[DIST_SYM]
1107 THEN ASM_REWRITE_TAC[]]);;
1110 let MM_4M7_IMP_STAB_4M7=prove(`
1111 MMs_v39 scs_4M7 v /\
1113 dist(v i,v j)<= cstab ==>
1114 ~(MMs_v39 (scs_stab_diag_v39 scs_4M7 i j) ={})`,
1116 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
1117 THEN EXISTS_TAC`v:num->real^3`
1118 THEN EXISTS_TAC` scs_4M7 `
1119 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M7 `;`v`]
1120 THEN ASSUME_TAC SCS_4M7_BASIC
1121 THEN ASSUME_TAC K_SCS_4M7
1122 THEN ASM_SIMP_TAC[SCS_4M7_IS_SCS;SCS_4M7_IS_SCS;SCS_4M7_BASIC;K_SCS_4M7;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M7_13;BB_4M7_IMP_BB_STAN_4M7;STAB_4M7_SCS]
1124 THEN REAL_ARITH_TAC);;
1129 let SET_STAB_4M7=prove(`{ scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M7 (i MOD 4) (j MOD 4)| scs_diag 4 (i MOD 4) (j MOD 4) }`,
1130 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
1131 THEN MRESAL_TAC STAB_MOD[`scs_4M7`][SCS_4M7_IS_SCS;K_SCS_4M7]);;
1133 let EXPAND_STAB_DIAG_4M7=prove(`
1134 {scs_stab_diag_v39 scs_4M7 (i MOD 4) (j MOD 4) | j MOD 4 =
1135 (i MOD 4 + 2) MOD 4}=
1136 {scs_stab_diag_v39 scs_4M7 (i+2) i| i<4} `,
1137 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M7_IS_SCS;K_SCS_4M7]);;
1140 let SET_EQ_DIAG_STAB_4M7=prove_by_refinement(`scs_arrow_v39
1141 { scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4M7 0 2,scs_stab_diag_v39 scs_4M7 1 3}`,
1143 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M7;SET_STAB_4M7;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
1145 REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M7 (i + 2) i |i=0\/i=1\/i=2\/i=3}
1146 = {scs_stab_diag_v39 scs_4M7 (0 + 2) 0} UNION
1147 {scs_stab_diag_v39 scs_4M7 (1 + 2) 1} UNION
1148 {scs_stab_diag_v39 scs_4M7 (2 + 2) 2} UNION
1149 {scs_stab_diag_v39 scs_4M7 (3 + 2) 3}
1151 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M7 0 2,scs_stab_diag_v39 scs_4M7 1 3}={scs_stab_diag_v39 scs_4M7 0 2} UNION {scs_stab_diag_v39 scs_4M7 1 3}UNION {scs_stab_diag_v39 scs_4M7 0 2} UNION {scs_stab_diag_v39 scs_4M7 1 3}`]
1152 THEN MATCH_MP_TAC FZIOTEF_UNION
1153 THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
1154 THEN MRESA_TAC STAB_SYM[`scs_4M7`;`0`;`2`]
1157 MATCH_MP_TAC FZIOTEF_REFL
1158 THEN REWRITE_TAC[IN_SING]
1159 THEN REPEAT RESA_TAC
1160 THEN ASM_SIMP_TAC[STAB_4M7_SCS;SCS_DIAG_SCS_4M7_02];
1162 MATCH_MP_TAC FZIOTEF_UNION
1163 THEN MRESA_TAC STAB_SYM[`scs_4M7`;`1`;`3`]
1166 MATCH_MP_TAC FZIOTEF_REFL
1167 THEN REWRITE_TAC[IN_SING]
1168 THEN REPEAT RESA_TAC
1169 THEN ASM_SIMP_TAC[STAB_4M7_SCS;SCS_DIAG_SCS_4M7_13];
1171 MATCH_MP_TAC FZIOTEF_UNION
1172 THEN MRESAL_TAC STAB_MOD[`scs_4M7`;`4`;`2`][SCS_4M7_IS_SCS;K_SCS_4M7;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
1176 MATCH_MP_TAC FZIOTEF_REFL
1177 THEN REWRITE_TAC[IN_SING]
1178 THEN REPEAT RESA_TAC
1179 THEN ASM_SIMP_TAC[STAB_4M7_SCS;SCS_DIAG_SCS_4M7_02];
1181 MRESAL_TAC STAB_MOD[`scs_4M7`;`5`;`3`][SCS_4M7_IS_SCS;K_SCS_4M7;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
1184 MATCH_MP_TAC FZIOTEF_REFL
1185 THEN REWRITE_TAC[IN_SING]
1186 THEN REPEAT RESA_TAC
1187 THEN ASM_SIMP_TAC[STAB_4M7_SCS;SCS_DIAG_SCS_4M7_13]]);;
1191 let SCS_4M7_SLICE_13=prove_by_refinement(
1192 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M7 1 3 } {scs_prop_equ_v39 scs_3T4_prime 2, scs_3T4_prime2 }`,
1195 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
1196 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M7_13;STAB_4M7_SCS;SCS_K_D_A_STAB_EQ;]
1199 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M7_13]
1200 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
1201 THEN REPEAT RESA_TAC;
1203 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
1205 THEN MATCH_MP_TAC scs_inj
1206 THEN ASM_SIMP_TAC[SCS_3T4_prime_BASIC;SCS_4M7_BASIC;J_SCS_4M7;BASIC_HALF_SLICE_STAB;J_SCS_3T4_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T4_prime2_BASIC;J_SCS_3T4_prime2]
1209 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_4M7]
1214 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_3T4_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;
1215 ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
1216 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1217 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1220 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1221 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1223 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1224 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1226 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1227 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]
1228 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
1229 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
1230 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
1231 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
1232 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
1233 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
1235 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/\
1236 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1237 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1238 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1239 THEN REPEAT RESA_TAC
1240 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)
1241 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1242 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1243 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1244 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1245 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1249 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_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7]
1255 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_3T4_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;
1256 ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
1257 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1258 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1261 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1262 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1264 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1265 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1267 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1268 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]
1269 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
1270 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
1271 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
1272 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
1273 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
1274 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
1276 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/\
1277 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1278 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1279 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1280 THEN REPEAT RESA_TAC
1281 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)
1282 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1283 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1284 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1285 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1286 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1292 THEN REAL_ARITH_TAC;
1295 THEN REAL_ARITH_TAC;
1298 THEN REAL_ARITH_TAC;
1301 THEN REWRITE_TAC[cstab]
1302 THEN REAL_ARITH_TAC;
1306 THEN REWRITE_TAC[cstab]
1307 THEN REAL_ARITH_TAC;
1312 THEN REWRITE_TAC[J_SCS_3T4_prime];
1317 let SCS_4M7_SLICE_13_ARROW_3T4=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M7 1 3 } { scs_3T4}`,
1318 MATCH_MP_TAC FZIOTEF_TRANS
1319 THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3T4_prime 2, scs_3T4_prime2 }`
1320 THEN ASM_REWRITE_TAC[SCS_4M7_SLICE_13]
1321 THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}/\ {scs_3T4}= {scs_3T4}UNION {scs_3T4}`]
1322 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}/\ {scs_3T4}= {scs_3T4}UNION {scs_3T4}`]
1323 THEN MATCH_MP_TAC FZIOTEF_UNION
1324 THEN ASM_REWRITE_TAC[SCS_3T4_prime2_ARROW_MM_3T4;SCS_3T4_prime_ARROW_MM_3T4]
1325 THEN MATCH_MP_TAC FZIOTEF_TRANS
1326 THEN EXISTS_TAC`{scs_3T4_prime}`
1327 THEN ASM_REWRITE_TAC[SCS_3T4_prime2_ARROW_MM_3T4;SCS_3T4_prime_ARROW_MM_3T4]
1328 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`]
1329 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T4_prime 2`;`1`][PROP_EQU_IS_SCS;SCS_3T4_prime_IS_SCS]
1331 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1332 THEN REWRITE_TAC[]);;
1335 let SCS_4M7_SLICE_02=prove_by_refinement(
1336 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M7 0 2 } {scs_prop_equ_v39 scs_3T3_prime 1, scs_prop_equ_v39 scs_3M1_prime 1 }`,
1338 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
1339 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M7_02;STAB_4M7_SCS;SCS_K_D_A_STAB_EQ;]
1342 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M7_02]
1343 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
1344 THEN REPEAT RESA_TAC;
1347 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
1349 THEN MATCH_MP_TAC scs_inj
1350 THEN ASM_SIMP_TAC[SCS_3T3_prime_BASIC;SCS_4M7_BASIC;J_SCS_4M7;BASIC_HALF_SLICE_STAB;J_SCS_3T3_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3M1_prime_BASIC;J_SCS_3M1_prime]
1354 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_3T3_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7]
1359 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_3T4_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;
1360 ARITH_RULE`(2 + 1 + 4 - 0) MOD 4= 3/\ 0 MOD 4=0/\ a+0=a`;scs_prop_equ_v39]
1361 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1362 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1365 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1366 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1368 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1369 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1371 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1372 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]
1373 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
1374 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
1375 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
1376 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
1377 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
1378 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
1380 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/\
1381 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1382 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1383 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1384 THEN REPEAT RESA_TAC
1385 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)
1386 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1387 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1388 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1389 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1390 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1394 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_3M1_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7]
1400 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_3M1_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M7;
1401 ARITH_RULE`(0 + 1 + 4 - 2) MOD 4= 3/\ 2 MOD 4=2/\ a+0=a`;scs_prop_equ_v39]
1402 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1403 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1406 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1407 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1409 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1410 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1412 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1413 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]
1414 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
1415 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
1416 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
1417 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
1418 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
1419 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
1421 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/\
1422 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1423 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1424 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1425 THEN REPEAT RESA_TAC
1426 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)
1427 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1428 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1429 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1430 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1431 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1437 THEN REAL_ARITH_TAC;
1441 THEN REAL_ARITH_TAC;
1444 THEN REAL_ARITH_TAC;
1447 THEN REWRITE_TAC[cstab]
1448 THEN REAL_ARITH_TAC;
1451 THEN REWRITE_TAC[cstab]
1452 THEN REAL_ARITH_TAC;
1457 THEN REWRITE_TAC[J_SCS_3T3_prime];
1463 let SCS_4M7_SLICE_02_ARROW_3T3_3M1=prove(
1464 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M7 0 2 } { scs_3T3,scs_3M1}`,
1465 MATCH_MP_TAC FZIOTEF_TRANS
1466 THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3T3_prime 1, scs_prop_equ_v39 scs_3M1_prime 1}`
1467 THEN ASM_REWRITE_TAC[SCS_4M7_SLICE_02]
1468 THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`]
1469 THEN MATCH_MP_TAC FZIOTEF_UNION
1473 MATCH_MP_TAC FZIOTEF_TRANS
1474 THEN EXISTS_TAC`{scs_3T3_prime}`
1475 THEN ASM_REWRITE_TAC[SCS_3T3_prime_ARROW_MM_3T3]
1476 THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T3_prime`;`1`;`3`][SCS_3T3_prime_IS_SCS;K_SCS_3T3_prime;ARITH_RULE`(3 - 1 MOD 3)=2`]
1477 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T3_prime 1`;`2`][PROP_EQU_IS_SCS;SCS_3T3_prime_IS_SCS]
1479 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1482 MATCH_MP_TAC FZIOTEF_TRANS
1483 THEN EXISTS_TAC`{scs_3M1_prime}`
1484 THEN ASM_REWRITE_TAC[SCS_3M1_prime_ARROW_MM_3M1]
1485 THEN MRESAS_TAC PRO_EQU_ID1[`scs_3M1_prime`;`1`;`3`][SCS_3M1_prime_IS_SCS;K_SCS_3M1_prime;ARITH_RULE`(3 - 1 MOD 3)=2`]
1486 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1_prime 1`;`2`][PROP_EQU_IS_SCS;SCS_3M1_prime_IS_SCS]
1488 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1489 THEN REWRITE_TAC[]]);;
1493 let STAB_SCS_4M7_ARROW_3T3_3M1_3T4=prove(
1495 { scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j } {scs_3T3,scs_3M1,scs_3T4}`,
1496 MATCH_MP_TAC FZIOTEF_TRANS
1497 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M7 0 2,scs_stab_diag_v39 scs_4M7 1 3}`
1498 THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_4M7;SET_RULE`{A,B}={A}UNION {B}`;SET_RULE`{scs_3T3,scs_3M1,scs_3T4}={scs_3T3,scs_3M1} UNION{scs_3T4}`]
1499 THEN MATCH_MP_TAC FZIOTEF_UNION
1500 THEN ASM_REWRITE_TAC[SCS_4M7_SLICE_13_ARROW_3T4;SET_RULE`{A}UNION{B}={A,B}`;SCS_4M7_SLICE_02_ARROW_3T3_3M1]);;
1504 (***************************)
1506 let BB_4M8_IMP_BB_STAN_4M8= prove(`
1507 BBs_v39 scs_4M8 v /\
1509 dist(v i,v j)<= cstab ==>
1510 BBs_v39 (scs_stab_diag_v39 scs_4M8 i j) v`,
1511 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8]
1512 THEN REPEAT RESA_TAC
1513 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
1515 THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
1517 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
1519 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8;SCS_4M8_IS_SCS]
1520 THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
1521 THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
1523 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8;SCS_4M8_IS_SCS]
1524 THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
1525 THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
1526 THEN ONCE_REWRITE_TAC[DIST_SYM]
1527 THEN ASM_REWRITE_TAC[]]);;
1530 let MM_4M8_IMP_STAB_4M8=prove(`
1531 MMs_v39 scs_4M8 v /\
1533 dist(v i,v j)<= cstab ==>
1534 ~(MMs_v39 (scs_stab_diag_v39 scs_4M8 i j) ={})`,
1536 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
1537 THEN EXISTS_TAC`v:num->real^3`
1538 THEN EXISTS_TAC` scs_4M8 `
1539 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8 `;`v`]
1540 THEN ASSUME_TAC SCS_4M8_BASIC
1541 THEN ASSUME_TAC K_SCS_4M8
1542 THEN ASM_SIMP_TAC[SCS_4M8_IS_SCS;SCS_4M8_IS_SCS;SCS_4M8_BASIC;K_SCS_4M8;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M8_13;BB_4M8_IMP_BB_STAN_4M8;STAB_4M8_SCS]
1544 THEN REAL_ARITH_TAC);;
1548 let SET_STAB_4M8=prove(`{ scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M8 (i MOD 4) (j MOD 4)| scs_diag 4 (i MOD 4) (j MOD 4) }`,
1549 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
1550 THEN MRESAL_TAC STAB_MOD[`scs_4M8`][SCS_4M8_IS_SCS;K_SCS_4M8]);;
1552 let EXPAND_STAB_DIAG_4M8=prove(`
1553 {scs_stab_diag_v39 scs_4M8 (i MOD 4) (j MOD 4) | j MOD 4 =
1554 (i MOD 4 + 2) MOD 4}=
1555 {scs_stab_diag_v39 scs_4M8 (i+2) i| i<4} `,
1556 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M8_IS_SCS;K_SCS_4M8]);;
1559 let SET_EQ_DIAG_STAB_4M8=prove_by_refinement(`scs_arrow_v39
1560 { scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4M8 0 2,scs_stab_diag_v39 scs_4M8 1 3}`,
1562 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M8;SET_STAB_4M8;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
1564 REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M8 (i + 2) i |i=0\/i=1\/i=2\/i=3}
1565 = {scs_stab_diag_v39 scs_4M8 (0 + 2) 0} UNION
1566 {scs_stab_diag_v39 scs_4M8 (1 + 2) 1} UNION
1567 {scs_stab_diag_v39 scs_4M8 (2 + 2) 2} UNION
1568 {scs_stab_diag_v39 scs_4M8 (3 + 2) 3}
1570 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M8 0 2,scs_stab_diag_v39 scs_4M8 1 3}={scs_stab_diag_v39 scs_4M8 0 2} UNION {scs_stab_diag_v39 scs_4M8 1 3}UNION {scs_stab_diag_v39 scs_4M8 0 2} UNION {scs_stab_diag_v39 scs_4M8 1 3}`]
1571 THEN MATCH_MP_TAC FZIOTEF_UNION
1572 THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
1573 THEN MRESA_TAC STAB_SYM[`scs_4M8`;`0`;`2`]
1576 MATCH_MP_TAC FZIOTEF_REFL
1577 THEN REWRITE_TAC[IN_SING]
1578 THEN REPEAT RESA_TAC
1579 THEN ASM_SIMP_TAC[STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02];
1581 MATCH_MP_TAC FZIOTEF_UNION
1582 THEN MRESA_TAC STAB_SYM[`scs_4M8`;`1`;`3`]
1585 MATCH_MP_TAC FZIOTEF_REFL
1586 THEN REWRITE_TAC[IN_SING]
1587 THEN REPEAT RESA_TAC
1588 THEN ASM_SIMP_TAC[STAB_4M8_SCS;SCS_DIAG_SCS_4M8_13];
1590 MATCH_MP_TAC FZIOTEF_UNION
1591 THEN MRESAL_TAC STAB_MOD[`scs_4M8`;`4`;`2`][SCS_4M8_IS_SCS;K_SCS_4M8;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
1595 MATCH_MP_TAC FZIOTEF_REFL
1596 THEN REWRITE_TAC[IN_SING]
1597 THEN REPEAT RESA_TAC
1598 THEN ASM_SIMP_TAC[STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02];
1600 MRESAL_TAC STAB_MOD[`scs_4M8`;`5`;`3`][SCS_4M8_IS_SCS;K_SCS_4M8;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
1603 MATCH_MP_TAC FZIOTEF_REFL
1604 THEN REWRITE_TAC[IN_SING]
1605 THEN REPEAT RESA_TAC
1606 THEN ASM_SIMP_TAC[STAB_4M8_SCS;SCS_DIAG_SCS_4M8_13]]);;
1612 let PROP_OPP_DIAG_4M8_13= prove_by_refinement(`scs_stab_diag_v39 scs_4M8 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4M8 0 2)) 2 `,
1613 [REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;SCS_K_D_A_STAB_EQ;scs_opp_v39]
1614 THEN MATCH_MP_TAC scs_inj
1615 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M8_BASIC;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_13;scs_basic;unadorned_v39;peropp;peropp2]
1623 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;]
1624 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
1626 THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
1627 THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
1629 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
1630 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
1633 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`)
1634 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
1636 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`)
1637 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
1639 THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_4_TAC;PSORT_5_EXPLICIT;ARITH_RULE`4-1=3/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6
1640 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;
1646 let STAB_4M8_02_ARROW_4M8_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M8 0 2}{scs_stab_diag_v39 scs_4M8 1 3}`,
1647 ASM_SIMP_TAC[PROP_OPP_DIAG_4M8_13]
1648 THEN MATCH_MP_TAC FZIOTEF_TRANS
1649 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4M8 0 2)}`
1652 MATCH_MP_TAC (GEN_ALL YXIONXL2)
1654 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M8;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02]
1657 MATCH_MP_TAC(GEN_ALL YXIONXL3)
1658 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
1659 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4M8 0 2)`
1660 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M8;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02]]);;
1664 let SCS_4M8_SLICE_13=prove_by_refinement(
1665 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M8 1 3 } {scs_3T4_prime2 }`,
1667 ONCE_REWRITE_TAC[SET_RULE`{scs_3T4_prime2}={scs_3T4_prime2, scs_3T4_prime2}`]
1668 THEN MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
1669 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_13;STAB_4M8_SCS;SCS_K_D_A_STAB_EQ;]
1672 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_13]
1673 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
1674 THEN REPEAT RESA_TAC;
1676 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
1678 THEN MATCH_MP_TAC scs_inj
1679 THEN ASM_SIMP_TAC[SCS_3T4_prime_BASIC;SCS_4M8_BASIC;J_SCS_4M8;BASIC_HALF_SLICE_STAB;J_SCS_3T4_prime;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T4_prime2_BASIC;J_SCS_3T4_prime2_1]
1683 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_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8]
1688 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_3T4_prime;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8;
1689 ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
1690 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1691 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1694 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1695 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1697 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1698 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1700 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1701 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]
1702 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
1703 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
1704 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
1705 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
1706 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
1707 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
1709 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/\
1710 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1711 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1712 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1713 THEN REPEAT RESA_TAC
1714 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)
1715 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1716 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1717 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1718 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1719 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1723 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_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8]
1729 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_3T4_prime2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8;
1730 ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
1731 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1732 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1735 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1736 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1738 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1739 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1741 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1742 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]
1743 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
1744 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
1745 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
1746 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
1747 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
1748 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
1750 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/\
1751 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1752 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1753 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1754 THEN REPEAT RESA_TAC
1755 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)
1756 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1757 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1758 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1759 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1760 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1766 THEN REAL_ARITH_TAC;
1769 THEN REAL_ARITH_TAC;
1772 THEN REAL_ARITH_TAC;
1775 THEN REWRITE_TAC[cstab]
1776 THEN REAL_ARITH_TAC;
1780 THEN REWRITE_TAC[cstab]
1781 THEN REAL_ARITH_TAC;
1786 THEN REWRITE_TAC[J_SCS_3T4_prime2_1];
1793 let SCS_4M8_SLICE_13_ARROW_3T4=prove(
1794 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M8 1 3 } { scs_3T4}`,
1795 MATCH_MP_TAC FZIOTEF_TRANS
1796 THEN EXISTS_TAC`{ scs_3T4_prime2 }`
1797 THEN ASM_REWRITE_TAC[SCS_4M8_SLICE_13]
1798 THEN ASM_REWRITE_TAC[SCS_3T4_prime2_ARROW_MM_3T4;SCS_3T4_prime_ARROW_MM_3T4]);;
1801 let SCS_4M8_SLICE_02_ARROW_3T4 =prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_4M8 0 2 } { scs_3T4 }`,
1802 MATCH_MP_TAC FZIOTEF_TRANS
1803 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M8 1 3}`
1804 THEN ASM_SIMP_TAC[STAB_4M8_02_ARROW_4M8_13;SCS_4M8_SLICE_13_ARROW_3T4]);;
1808 let SET_STAB_4M8_ARROW_3T4=prove(`scs_arrow_v39
1809 { scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j } {scs_3T4}`,
1810 ONCE_REWRITE_TAC[SET_RULE`{A}={A,A}`]
1811 THEN MATCH_MP_TAC FZIOTEF_TRANS
1812 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M8 0 2,scs_stab_diag_v39 scs_4M8 1 3}`
1813 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M8;]
1814 THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`;]
1815 THEN MATCH_MP_TAC FZIOTEF_UNION
1816 THEN ASM_SIMP_TAC[SCS_4M8_SLICE_02_ARROW_3T4;SCS_4M8_SLICE_13_ARROW_3T4]);;
1821 let h0_LT_B_SCS_4M6=prove(`
1822 (!i j. scs_diag 4 i j ==> &4 * h0 < scs_b_v39 scs_4M6' i j)
1823 /\ (!i j. scs_diag 4 i j ==> scs_a_v39 scs_4M6' i j <= cstab)`,
1825 THEN REWRITE_TAC[h0;SCS_DIAG_4_CASES;cstab]
1826 THEN REPEAT RESA_TAC
1827 THEN ASSUME_TAC(ARITH_RULE`~(4=0)`)
1828 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
1831 THEN MP_TAC sqrt8_LE_CSTAB
1832 THEN REAL_ARITH_TAC);;
1834 let SCS_4M6_STAND_OR_PRO=prove(`!i. scs_a_v39 scs_4M6' i (i + 1) = &2 /\
1835 scs_b_v39 scs_4M6' i (i + 1) = &2 * h0 \/
1836 scs_a_v39 scs_4M6' i (i + 1) = &2 * h0 /\
1837 scs_b_v39 scs_4M6' i (i + 1) = cstab`,
1840 THEN SIMP_TAC[GSYM ADD1;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
1841 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`SUC i:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
1843 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`4`][ARITH_RULE`1<4`]
1845 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
1846 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
1853 let SCS_4M6_STAND=prove(`scs_a_v39 scs_4M6' 1 2 = &2/\ scs_a_v39 scs_4M6' 2 3 = &2/\ scs_a_v39 scs_4M6' 3 4 = &2/\ scs_a_v39 scs_4M6' 0 1= &2 * h0
1854 /\ scs_a_v39 scs_4M6' 1 4= &2 * h0
1855 /\ scs_b_v39 scs_4M6' 0 1= cstab`,
1859 let h0_CSTAB_LT_4=prove(`&2< &2*h0 /\ cstab< &4/\ &2<= &2*h0 /\ cstab<= &4
1860 /\ &2*h0< &4/\ &2< &4 /\ ~(&2 * h0 = &2)`,
1861 REWRITE_TAC[cstab;h0]
1862 THEN REAL_ARITH_TAC);;
1864 let EXTREMAL_SCS_4M6=prove_by_refinement(`main_nonlinear_terminal_v11 ==>
1866 MMs_v39 scs_4M6' v /\
1867 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==>
1868 dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = &2/\dist (v 3,v 0) = &2
1869 /\ dist (v 0,v 1) = cstab)`,
1874 THEN ASSUME_TAC(SCS_4M6_IS_SCS)
1875 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M6'`;`v`]
1876 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M6'`]
1877 THEN THAYTHES_TAC 0[`4`;`0`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M6]
1880 THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`1`][SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;h0_LT_B_SCS_4M6;SCS_4M6_STAND_OR_PRO;ARITH_RULE`1+1=2`;SCS_4M6_STAND]
1883 THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`2`][SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;h0_LT_B_SCS_4M6;SCS_4M6_STAND_OR_PRO;ARITH_RULE`2+1=3`;SCS_4M6_STAND]
1886 THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`3`][SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;h0_LT_B_SCS_4M6;SCS_4M6_STAND_OR_PRO;ARITH_RULE`3+1=4`;SCS_4M6_STAND]
1887 THEN ASSUME_TAC SCS_4M6_BASIC
1888 THEN ASSUME_TAC K_SCS_4M6
1889 THEN ASSUME_TAC h0_LT_B_SCS_4M6
1890 THEN ASSUME_TAC SCS_4M6_STAND_OR_PRO
1891 THEN ASSUME_TAC SCS_4M6_STAND
1892 THEN ASSUME_TAC h0_CSTAB_LT_4
1893 THEN MP_TAC (SET_RULE`scs_is_str scs_4M6' v 0\/ ~(scs_is_str scs_4M6' v 0 )`)
1898 THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`0`][ARITH_RULE`0+1=1`]
1899 THEN MP_TAC Bkossge.quad_nonexist_849
1900 THEN ASM_REWRITE_TAC[NOT_EXISTS_THM]
1902 THEN THAYTHE_TAC 0[`v 1`;`v 2`;`v 3`;`v 0`;]
1904 THEN ONCE_REWRITE_TAC[DIST_SYM]
1905 THEN ASM_REWRITE_TAC[DE_MORGAN_THM;REAL_ARITH`~(a<=b)<=> b<a`]
1909 THAYTHEL_TAC (18-2)[`1`;`3`][scs_diag;ARITH_RULE`~(1 MOD 4 = 3 MOD 4) /\
1910 ~(SUC 1 MOD 4 = 3 MOD 4) /\
1911 ~(1 MOD 4 = SUC 3 MOD 4)`]
1913 THEN ONCE_REWRITE_TAC[DIST_SYM]
1918 THAYTHEL_TAC (18-2)[`0`;`2`][scs_diag;ARITH_RULE`~(0 MOD 4 = 2 MOD 4) /\
1919 ~(SUC 0 MOD 4 = 2 MOD 4) /\
1920 ~(0 MOD 4 = SUC 2 MOD 4)`]
1928 MP_TAC (SET_RULE`scs_is_str scs_4M6' v 1\/ ~(scs_is_str scs_4M6' v 1 )`)
1933 THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`1`][ARITH_RULE`1+3=4`]
1934 THEN MP_TAC Bkossge.quad_nonexist_849
1935 THEN ASM_REWRITE_TAC[NOT_EXISTS_THM]
1937 THEN THAYTHE_TAC 0[`v 1`;`v 2`;`v 3`;`v 0`;]
1939 THEN ONCE_REWRITE_TAC[DIST_SYM]
1940 THEN ASM_REWRITE_TAC[DE_MORGAN_THM;REAL_ARITH`~(a<=b)<=> b<a`]
1944 THAYTHEL_TAC (19-2)[`1`;`3`][scs_diag;ARITH_RULE`~(1 MOD 4 = 3 MOD 4) /\
1945 ~(SUC 1 MOD 4 = 3 MOD 4) /\
1946 ~(1 MOD 4 = SUC 3 MOD 4)`]
1948 THEN ONCE_REWRITE_TAC[DIST_SYM]
1953 THAYTHEL_TAC (19-2)[`0`;`2`][scs_diag;ARITH_RULE`~(0 MOD 4 = 2 MOD 4) /\
1954 ~(SUC 0 MOD 4 = 2 MOD 4) /\
1955 ~(0 MOD 4 = SUC 2 MOD 4)`]
1964 THEN THAYTHES_TAC 0[`scs_4M6'`;`v`;`0`][IN;ARITH_RULE`0+1=1`];
1969 MP_TAC Bkossge.quad_nonexist_849
1970 THEN ASM_REWRITE_TAC[NOT_EXISTS_THM]
1972 THEN THAYTHE_TAC 0[`v 1`;`v 2`;`v 3`;`v 0`;]
1974 THEN ONCE_REWRITE_TAC[DIST_SYM]
1975 THEN ASM_REWRITE_TAC[DE_MORGAN_THM;REAL_ARITH`~(a<=b)<=> b<a`]
1979 THAYTHEL_TAC (18-2)[`1`;`3`][scs_diag;ARITH_RULE`~(1 MOD 4 = 3 MOD 4) /\
1980 ~(SUC 1 MOD 4 = 3 MOD 4) /\
1981 ~(1 MOD 4 = SUC 3 MOD 4)`]
1983 THEN ONCE_REWRITE_TAC[DIST_SYM]
1988 THAYTHEL_TAC (18-2)[`0`;`2`][scs_diag;ARITH_RULE`~(0 MOD 4 = 2 MOD 4) /\
1989 ~(SUC 0 MOD 4 = 2 MOD 4) /\
1990 ~(0 MOD 4 = SUC 2 MOD 4)`]
2001 let BB_4M6_IMP_scs_4T3=prove(
2002 `main_nonlinear_terminal_v11
2003 ==> (!v. MMs_v39 scs_4M6' v /\
2004 (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))
2005 ==> BBs_v39 scs_4T3 v)`,
2007 THEN MP_TAC EXTREMAL_SCS_4M6
2009 THEN THAYTHE_TAC 0[`v`]
2010 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M6'`;`v`]
2012 THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4T3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4T3]
2013 THEN REPEAT RESA_TAC
2014 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2016 THEN THAYTHE_TAC 2[`i`;`j`]
2019 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M6'`;`v`]
2020 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M6'`][SCS_4M6_IS_SCS]
2021 THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M6;MOD_REFL]
2022 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M6'`][SCS_4M6_IS_SCS]
2023 THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M6;MOD_REFL]
2024 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2026 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
2027 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2029 THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
2030 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2033 THEN ONCE_REWRITE_TAC[DIST_SYM]
2034 THEN ASM_REWRITE_TAC[]
2040 let MM_4M6_IMP_MM_4T3=prove(`main_nonlinear_terminal_v11
2041 ==> (!v. MMs_v39 scs_4M6' v /\
2042 (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))
2043 ==> ~(MMs_v39 scs_4T3={}))`,
2047 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2048 THEN EXISTS_TAC`v:num->real^3`
2049 THEN EXISTS_TAC`scs_4M6'`
2050 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M6'`;`v`]
2051 THEN ASM_SIMP_TAC[SCS_4T3_BASIC;SCS_4M6_BASIC;SCS_4T3_IS_SCS;SCS_4T3_IS_SCS;
2052 SCS_4M6_IS_SCS;K_SCS_4T3;K_SCS_4M6;IN;BB_4M6_IMP_scs_4T3]
2054 THEN REAL_ARITH_TAC);;
2057 let SCS_4M6_ARROW_SCS_4T3_STAB_4M6=prove_by_refinement(
2058 `main_nonlinear_terminal_v11
2059 ==> scs_arrow_v39 { scs_4M6' } ({scs_4T3} UNION {scs_stab_diag_v39 scs_4M6' i j| scs_diag 4 i j})`,
2062 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM]
2063 THEN ABBREV_TAC`k=scs_k_v39 s`
2064 THEN REPEAT RESA_TAC;
2066 ASM_SIMP_TAC[SCS_4T3_IS_SCS];
2068 ASM_SIMP_TAC[STAB_4M6_SCS;K_SCS_4M6];
2070 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M6' ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M6' ==> MMs_v39 s = {}))`);
2076 THEN POP_ASSUM MP_TAC
2077 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
2078 THEN REPEAT STRIP_TAC
2079 THEN POP_ASSUM MP_TAC
2081 THEN POP_ASSUM MP_TAC
2082 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2085 MP_TAC(SET_RULE`(!i j. scs_diag 4 i j ==> cstab < dist(v i,v j))\/ ~((!i j. scs_diag 4 i j ==> cstab < dist((v:num->real^3) i,v j)))`)
2089 THEN ASM_REWRITE_TAC[]
2090 THEN MP_TAC MM_4M6_IMP_MM_4T3
2091 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2093 THEN MATCH_DICH_TAC 0
2094 THEN ASM_REWRITE_TAC[]
2095 THEN EXISTS_TAC`v:num->real^3`
2096 THEN ASM_REWRITE_TAC[];
2099 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
2101 THEN MP_TAC MM_4M6_IMP_STAB_4M6
2104 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2106 THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M6' i j`
2107 THEN ASM_REWRITE_TAC[]
2110 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
2111 THEN EXISTS_TAC`i:num`
2112 THEN EXISTS_TAC`j:num`
2113 THEN ASM_REWRITE_TAC[];
2115 EXISTS_TAC`v':num->real^3`
2116 THEN ASM_REWRITE_TAC[]]);;
2119 let NWDGKXH=prove(`main_nonlinear_terminal_v11
2120 ==> scs_arrow_v39 { scs_4M6' } ({scs_4T3, scs_4T5})`,
2122 THEN MATCH_MP_TAC FZIOTEF_TRANS
2123 THEN EXISTS_TAC`({scs_4T3} UNION {scs_stab_diag_v39 scs_4M6' i j| scs_diag 4 i j})`
2124 THEN ASM_SIMP_TAC[SCS_4M6_ARROW_SCS_4T3_STAB_4M6]
2125 THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`;]
2126 THEN MATCH_MP_TAC FZIOTEF_UNION
2127 THEN ASM_SIMP_TAC[SET_STAB_4M6_ARROW_4T5]
2128 THEN MATCH_MP_TAC FZIOTEF_REFL
2129 THEN REWRITE_TAC[IN_SING]
2130 THEN REPEAT RESA_TAC
2131 THEN ASM_SIMP_TAC[SCS_4T3_IS_SCS]);;
2139 let h0_LT_B_SCS_4M7=prove(`
2140 (!i j. scs_diag 4 i j ==> &4 * h0 < scs_b_v39 scs_4M7 i j)
2141 /\ (!i j. scs_diag 4 i j ==> scs_a_v39 scs_4M7 i j <= cstab)`,
2143 THEN REWRITE_TAC[h0;SCS_DIAG_4_CASES;cstab]
2144 THEN REPEAT RESA_TAC
2145 THEN ASSUME_TAC(ARITH_RULE`~(4=0)`)
2146 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
2149 THEN MP_TAC sqrt8_LE_CSTAB
2150 THEN REAL_ARITH_TAC);;
2152 let SCS_4M7_STAND_OR_PRO=prove(`!i. scs_a_v39 scs_4M7 i (i + 1) = &2 /\
2153 scs_b_v39 scs_4M7 i (i + 1) = &2 * h0 \/
2154 scs_a_v39 scs_4M7 i (i + 1) = &2 * h0 /\
2155 scs_b_v39 scs_4M7 i (i + 1) = cstab`,
2158 THEN SIMP_TAC[GSYM ADD1;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
2159 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`SUC i:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2161 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`4`][ARITH_RULE`1<4`]
2163 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
2164 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2169 let SCS_4M7_STAND=prove(
2170 `scs_a_v39 scs_4M7 0 1= &2*h0/\ scs_a_v39 scs_4M7 1 2 = &2 * h0 /\ scs_a_v39 scs_4M7 2 5= &2*h0 /\scs_b_v39 scs_4M7 1 2= cstab /\scs_b_v39 scs_4M7 0 1 = cstab`,
2175 let MIN_NOT_STAND_4M7=prove_by_refinement(`main_nonlinear_terminal_v11 ==>
2177 MMs_v39 scs_4M7 v /\
2178 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==>
2179 dist (v 1,v 2) = &2 * h0 \/ dist (v 0,v 1) = &2*h0)`,
2183 THEN ASSUME_TAC(SCS_4M7_IS_SCS)
2184 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M7`;`v`]
2185 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`]
2186 THEN THAYTHES_TAC 0[`4`;`0`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M7]
2187 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`]
2188 THEN THAYTHES_TAC 0[`5`;`1`][ARITH_RULE`5 MOD 4 = 1 MOD 4`;MOD_MULT_ADD;K_SCS_4M7]
2189 THEN ASSUME_TAC h0_LT_B_SCS_4M7
2190 THEN ASSUME_TAC SCS_4M7_STAND_OR_PRO
2191 THEN ASSUME_TAC SCS_4M7_BASIC
2192 THEN ASSUME_TAC K_SCS_4M7
2193 THEN ASSUME_TAC SCS_4M7_STAND
2194 THEN MP_TAC (SET_RULE`scs_is_str scs_4M7 v 0\/ ~(scs_is_str scs_4M7 v 0 )`)
2199 THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`0`][ARITH_RULE`0+1=1`];
2201 MP_TAC (SET_RULE`scs_is_str scs_4M7 v 1\/ ~(scs_is_str scs_4M7 v 1 )`)
2206 THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`1`][ARITH_RULE`1+1=2`];
2208 MP_TAC (SET_RULE`scs_is_str scs_4M7 v 2\/ ~(scs_is_str scs_4M7 v 2 )`)
2213 THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`2`][ARITH_RULE`2+3=5`]
2214 THEN ONCE_REWRITE_TAC[DIST_SYM]
2215 THEN ASM_REWRITE_TAC[];
2219 THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`1`][IN;ARITH_RULE`1+1=2`]
2222 THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`0`][IN;ARITH_RULE`0+1=1`]
2223 THEN MRESAL_TAC STR_MOD_EQ[`4`;`scs_4M7`;`v`;`4`][IN;ARITH_RULE`4 MOD 4=0`]
2226 THEN THAYTHES_TAC 0[`scs_4M7`;`v`;`1`][ARITH_RULE`1+1=2/\ 1+3=4`]
2228 THEN ONCE_REWRITE_TAC[DIST_SYM]
2229 THEN ASM_REWRITE_TAC[]]);;
2235 let BB_4M7_IMP_4M6_12=prove(`main_nonlinear_terminal_v11 ==>
2237 MMs_v39 scs_4M7 v /\
2238 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) /\
2239 dist (v 1,v 2) = &2*h0
2240 ==> BBs_v39 scs_4M6' v)`,
2242 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M7`;`v`]
2244 THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M7;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
2245 THEN REPEAT RESA_TAC
2246 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2248 THEN THAYTHE_TAC 2[`i`;`j`]
2251 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M7`;`v`]
2252 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][SCS_4M7_IS_SCS]
2253 THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M7;MOD_REFL]
2254 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][SCS_4M7_IS_SCS]
2255 THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M7;MOD_REFL]
2256 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2258 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
2259 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2261 THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
2262 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2265 THEN ONCE_REWRITE_TAC[DIST_SYM]
2266 THEN ASM_REWRITE_TAC[h0]
2267 THEN REAL_ARITH_TAC);;
2271 let MM_4M7_IMP_MM_4M6_12=prove(`main_nonlinear_terminal_v11
2272 ==> (!v. MMs_v39 scs_4M7 v /\
2273 (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
2274 dist (v 1,v 2) = &2 * h0
2275 ==> ~(MMs_v39 scs_4M6'={}))`,
2279 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2280 THEN EXISTS_TAC`v:num->real^3`
2281 THEN EXISTS_TAC`scs_4M7`
2282 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M7`;`v`]
2283 THEN ASM_SIMP_TAC[SCS_4M6_BASIC;SCS_4M7_BASIC;SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;
2284 SCS_4M7_IS_SCS;K_SCS_4M6;K_SCS_4M7;IN;BB_4M7_IMP_4M6_12]
2286 THEN REAL_ARITH_TAC);;
2292 let BB_4M7_IMP_4M6_01=prove(
2293 `main_nonlinear_terminal_v11 ==>
2295 MMs_v39 scs_4M7 v /\
2296 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) /\
2297 dist (v 0,v 1) = &2*h0
2298 ==> BBs_v39 (scs_prop_equ_v39(scs_opp_v39 scs_4M6' ) 1) v)`,
2300 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M7`;`v`]
2302 THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M7;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;scs_prop_equ_v39;scs_opp_v39;peropp2]
2303 THEN REPEAT RESA_TAC
2304 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2306 THEN THAYTHE_TAC 2[`i`;`j`]
2309 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M7`;`v`]
2310 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][SCS_4M7_IS_SCS]
2311 THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M7;MOD_REFL]
2312 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M7`][SCS_4M7_IS_SCS]
2313 THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M7;MOD_REFL]
2314 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+i:num`;`1+j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2316 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2318 THEN MRESA_TAC MOD_ADD_MOD[`1`;`i`;`4`]
2319 THEN MRESA_TAC MOD_ADD_MOD[`1`;`j`;`4`]
2322 THEN ASSUME_TAC(ARITH_RULE`4-1=3/\ 4-0=4/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 3+2=5 /\3+3=6/\ 5 MOD 4=1/\ 6 MOD 4=2`)
2323 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
2324 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2326 THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
2327 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2330 THEN ONCE_REWRITE_TAC[DIST_SYM]
2331 THEN ASM_REWRITE_TAC[h0;REAL_ARITH`a<=a`]
2332 THEN REAL_ARITH_TAC);;
2336 let MM_4M7_IMP_MM_4M6_01=prove_by_refinement(`main_nonlinear_terminal_v11
2337 ==> (!v. MMs_v39 scs_4M7 v /\
2338 (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
2339 dist (v 0,v 1) = &2 * h0
2340 ==> ~(MMs_v39 (scs_prop_equ_v39(scs_opp_v39 scs_4M6' ) 1)={}))`,
2344 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2345 THEN EXISTS_TAC`v:num->real^3`
2346 THEN EXISTS_TAC`scs_4M7`
2347 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M7`;`v`]
2348 THEN ASM_SIMP_TAC[SCS_4M6_BASIC;SCS_4M7_BASIC;SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;
2349 SCS_4M7_IS_SCS;K_SCS_4M6;K_SCS_4M7;IN;BB_4M7_IMP_4M6_01]
2352 MATCH_MP_TAC PROP_EQU_IS_SCS
2353 THEN MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
2354 THEN EXISTS_TAC`scs_opp_v39 scs_4M6'`
2355 THEN ASM_REWRITE_TAC[SCS_4M6_IS_SCS];
2359 MATCH_MP_TAC Hexagons.BAISC_PROP_EQU
2360 THEN MATCH_MP_TAC Cqaoqlr.BASIC_OPP
2361 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M6_BASIC];
2363 ASM_REWRITE_TAC[Hexagons.K_SCS_PROP_EUQ]
2364 THEN ASM_REWRITE_TAC[scs_opp_v39;scs_prop_equ_v39]
2366 THEN REAL_ARITH_TAC]);;
2370 let SCS_4M7_ARROW_STAB_4M7_4M6=prove_by_refinement(
2371 `main_nonlinear_terminal_v11
2372 ==> scs_arrow_v39 { scs_4M7 } ({scs_4M6', scs_prop_equ_v39(scs_opp_v39 scs_4M6' ) 1} UNION {scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j})`,
2375 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM;SET_RULE`a IN {b,c}<=> a= b\/ a=c`]
2376 THEN ABBREV_TAC`k=scs_k_v39 s`
2377 THEN REPEAT RESA_TAC;
2379 ASM_SIMP_TAC[SCS_4M6_IS_SCS];
2381 MATCH_MP_TAC PROP_EQU_IS_SCS
2382 THEN MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
2383 THEN EXISTS_TAC`scs_opp_v39 scs_4M6'`
2384 THEN ASM_REWRITE_TAC[SCS_4M6_IS_SCS];
2386 ASM_SIMP_TAC[STAB_4M7_SCS;K_SCS_4M7];
2388 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M7 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M7 ==> MMs_v39 s = {}))`);
2393 THEN POP_ASSUM MP_TAC
2394 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
2395 THEN REPEAT STRIP_TAC
2396 THEN POP_ASSUM MP_TAC
2398 THEN POP_ASSUM MP_TAC
2399 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2402 MP_TAC(SET_RULE`(!i j. scs_diag 4 i j ==> cstab < dist(v i,v j))\/ ~((!i j. scs_diag 4 i j ==> cstab < dist((v:num->real^3) i,v j)))`)
2405 MP_TAC MIN_NOT_STAND_4M7
2407 THEN THAYTHE_TAC 0[`v`];
2409 EXISTS_TAC`scs_4M6'`
2410 THEN ASM_REWRITE_TAC[]
2411 THEN MP_TAC MM_4M7_IMP_MM_4M6_12
2412 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2414 THEN MATCH_DICH_TAC 0
2415 THEN ASM_REWRITE_TAC[]
2416 THEN EXISTS_TAC`v:num->real^3`
2417 THEN ASM_REWRITE_TAC[];
2419 EXISTS_TAC`scs_prop_equ_v39 (scs_opp_v39 scs_4M6') 1`
2420 THEN ASM_REWRITE_TAC[]
2421 THEN MP_TAC MM_4M7_IMP_MM_4M6_01
2422 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2424 THEN MATCH_DICH_TAC 0
2425 THEN ASM_REWRITE_TAC[]
2426 THEN EXISTS_TAC`v:num->real^3`
2427 THEN ASM_REWRITE_TAC[];
2430 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
2432 THEN MP_TAC MM_4M7_IMP_STAB_4M7
2435 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2437 THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M7 i j`
2438 THEN ASM_REWRITE_TAC[]
2441 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
2442 THEN EXISTS_TAC`i:num`
2443 THEN EXISTS_TAC`j:num`
2444 THEN ASM_REWRITE_TAC[];
2446 EXISTS_TAC`v':num->real^3`
2447 THEN ASM_REWRITE_TAC[]]);;
2452 let K_SCS_OPP_4M6=prove(`scs_k_v39 (scs_opp_v39 scs_4M6') = 4`,
2453 ASM_REWRITE_TAC[scs_opp_v39;scs_prop_equ_v39]
2456 let SCS_4M6_OPP_IS_SCS=prove(`is_scs_v39 (scs_opp_v39 scs_4M6')`,
2457 MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
2458 THEN EXISTS_TAC`scs_opp_v39 scs_4M6'`
2459 THEN ASM_REWRITE_TAC[SCS_4M6_IS_SCS]);;
2462 let YOBIMPP=prove(`main_nonlinear_terminal_v11
2463 ==> scs_arrow_v39 { scs_4M7 } {scs_4M6',scs_3T3,scs_3M1,scs_3T4}`,
2466 THEN MATCH_MP_TAC FZIOTEF_TRANS
2467 THEN EXISTS_TAC`({scs_4M6', scs_prop_equ_v39(scs_opp_v39 scs_4M6' ) 1} UNION {scs_stab_diag_v39 scs_4M7 i j| scs_diag 4 i j})`
2468 THEN ASM_SIMP_TAC[SCS_4M7_ARROW_STAB_4M7_4M6;
2469 SET_RULE`{scs_4M6',scs_3T3,scs_3M1,scs_3T4}={scs_4M6',scs_4M6'} UNION{scs_3T3,scs_3M1,scs_3T4}`]
2470 THEN MATCH_MP_TAC FZIOTEF_UNION
2471 THEN ASM_SIMP_TAC[STAB_SCS_4M7_ARROW_3T3_3M1_3T4;SET_RULE`{A,B}={A} UNION {B}`]
2472 THEN MATCH_MP_TAC FZIOTEF_UNION
2476 MATCH_MP_TAC FZIOTEF_REFL
2477 THEN REWRITE_TAC[IN_SING]
2478 THEN REPEAT RESA_TAC
2479 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS];
2482 MRESAS_TAC PRO_EQU_ID1[`scs_opp_v39 scs_4M6'`;`1`;`4`][SCS_4M6_IS_SCS;K_SCS_4M6;ARITH_RULE`(4 - 1 MOD 4)=3`;K_SCS_OPP_4M6;SCS_4M6_OPP_IS_SCS]
2483 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 (scs_opp_v39 scs_4M6') 1`;`3`][PROP_EQU_IS_SCS;SCS_4M6_IS_SCS;K_SCS_OPP_4M6;SCS_4M6_OPP_IS_SCS]
2485 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
2488 THEN MATCH_MP_TAC FZIOTEF_TRANS
2489 THEN EXISTS_TAC`{scs_opp_v39 scs_4M6'}`
2490 THEN ASM_REWRITE_TAC[]
2491 THEN ASSUME_TAC SCS_4M6_IS_SCS
2492 THEN MRESA_TAC Yxionxl2.SCS_OPP_REFL[`scs_4M6'`]
2493 THEN MRESAS_TAC YXIONXL2[`4`;`scs_opp_v39 scs_4M6'`][K_SCS_OPP_4M6;SCS_4M6_OPP_IS_SCS;ARITH_RULE`~(4<=3)`]]);;
2496 (**************************)
2500 let BB_4M8_IMP_4M6_23=prove(`main_nonlinear_terminal_v11 ==>
2502 MMs_v39 scs_4M8 v /\
2503 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) /\
2504 dist (v 2,v 3) = &2*h0
2505 ==> BBs_v39 scs_4M6' v)`,
2507 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2509 THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
2510 THEN REPEAT RESA_TAC
2511 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2513 THEN THAYTHE_TAC 2[`i`;`j`]
2516 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2517 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
2518 THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
2519 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
2520 THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
2521 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2523 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
2524 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2526 THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
2527 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2530 THEN ONCE_REWRITE_TAC[DIST_SYM]
2531 THEN ASM_REWRITE_TAC[h0]
2532 THEN REAL_ARITH_TAC);;
2536 let MM_4M8_IMP_MM_4M6_23=prove(
2537 `main_nonlinear_terminal_v11
2538 ==> (!v. MMs_v39 scs_4M8 v /\
2539 (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
2540 dist (v 2,v 3) = &2 * h0
2541 ==> ~(MMs_v39 scs_4M6'={}))`,
2545 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2546 THEN EXISTS_TAC`v:num->real^3`
2547 THEN EXISTS_TAC`scs_4M8`
2548 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8`;`v`]
2549 THEN ASM_SIMP_TAC[SCS_4M6_BASIC;SCS_4M8_BASIC;SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;
2550 SCS_4M8_IS_SCS;K_SCS_4M6;K_SCS_4M8;IN;BB_4M8_IMP_4M6_23]
2552 THEN REAL_ARITH_TAC);;
2557 let BB_4M8_IMP_4M6_01=prove(
2558 `main_nonlinear_terminal_v11 ==>
2560 MMs_v39 scs_4M8 v /\
2561 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) /\
2562 dist (v 0,v 1) = &2*h0
2563 ==> BBs_v39 ((scs_opp_v39 scs_4M6' ) ) v)`,
2565 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2567 THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;scs_prop_equ_v39;scs_opp_v39;peropp2]
2568 THEN REPEAT RESA_TAC
2569 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2571 THEN THAYTHE_TAC 2[`i`;`j`]
2574 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2575 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
2576 THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
2577 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
2578 THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
2579 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+i:num`;`1+j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2581 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2583 THEN MRESA_TAC MOD_ADD_MOD[`1`;`i`;`4`]
2584 THEN MRESA_TAC MOD_ADD_MOD[`1`;`j`;`4`]
2587 THEN ASSUME_TAC(ARITH_RULE`4-1=3/\ 4-0=4/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 3+2=5 /\3+3=6/\ 5 MOD 4=1/\ 6 MOD 4=2`)
2588 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
2589 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2591 THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
2592 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2595 THEN ONCE_REWRITE_TAC[DIST_SYM]
2596 THEN ASM_REWRITE_TAC[h0;REAL_ARITH`a<=a`]
2597 THEN REAL_ARITH_TAC);;
2603 let MM_4M8_IMP_MM_4M6_01=prove_by_refinement(`main_nonlinear_terminal_v11
2604 ==> (!v. MMs_v39 scs_4M8 v /\
2605 (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
2606 dist (v 0,v 1) = &2 * h0
2607 ==> ~(MMs_v39 ((scs_opp_v39 scs_4M6' ) )={}))`,
2612 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2613 THEN EXISTS_TAC`v:num->real^3`
2614 THEN EXISTS_TAC`scs_4M8`
2615 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8`;`v`]
2616 THEN ASM_SIMP_TAC[SCS_4M6_BASIC;SCS_4M8_BASIC;SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;
2617 SCS_4M8_IS_SCS;K_SCS_4M6;K_SCS_4M8;IN;BB_4M8_IMP_4M6_01]
2620 MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
2621 THEN EXISTS_TAC`scs_opp_v39 scs_4M6'`
2622 THEN ASM_REWRITE_TAC[SCS_4M6_IS_SCS];
2626 MATCH_MP_TAC Cqaoqlr.BASIC_OPP
2627 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M6_BASIC];
2629 ASM_REWRITE_TAC[Hexagons.K_SCS_PROP_EUQ]
2630 THEN ASM_REWRITE_TAC[scs_opp_v39;scs_prop_equ_v39]
2632 THEN REAL_ARITH_TAC]);;
2636 let h0_LT_B_SCS_4M8=prove(`
2637 (!i j. scs_diag 4 i j ==> &4 * h0 < scs_b_v39 scs_4M8 i j)
2638 /\ (!i j. scs_diag 4 i j ==> scs_a_v39 scs_4M8 i j <= cstab)`,
2640 THEN REWRITE_TAC[h0;SCS_DIAG_4_CASES;cstab]
2641 THEN REPEAT RESA_TAC
2642 THEN ASSUME_TAC(ARITH_RULE`~(4=0)`)
2643 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
2646 THEN MP_TAC sqrt8_LE_CSTAB
2647 THEN REAL_ARITH_TAC);;
2649 let SCS_4M8_STAND_OR_PRO=prove(`!i. scs_a_v39 scs_4M8 i (i + 1) = &2 /\
2650 scs_b_v39 scs_4M8 i (i + 1) = &2 * h0 \/
2651 scs_a_v39 scs_4M8 i (i + 1) = &2 * h0 /\
2652 scs_b_v39 scs_4M8 i (i + 1) = cstab`,
2655 THEN SIMP_TAC[GSYM ADD1;Qknvmlb.SUC_MOD_NOT_EQ;ARITH_RULE`1<4`]
2656 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`SUC i:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2658 THEN MRESAL_TAC Yxionxl2.MOD_SUC_MOD[`i`;`4`][ARITH_RULE`1<4`]
2660 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
2661 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2668 let SCS_4M8_STAND=prove(
2669 `scs_a_v39 scs_4M8 0 1= &2*h0/\ scs_a_v39 scs_4M8 1 2 = &2 /\ scs_a_v39 scs_4M8 2 5= &2 /\scs_b_v39 scs_4M8 1 2= &2 *h0 /\scs_b_v39 scs_4M8 0 1 = cstab
2670 /\scs_a_v39 scs_4M8 2 3 = &2 * h0/\ scs_a_v39 scs_4M8 3 4 = &2/\ scs_b_v39 scs_4M8 2 3= cstab/\ scs_a_v39 scs_4M8 1 4= &2* h0/\ scs_a_v39 scs_4M8 3 6= &2 * h0`,
2678 let MIN_NOT_STAND_4M8=prove_by_refinement(
2679 `main_nonlinear_terminal_v11 ==>
2681 MMs_v39 scs_4M8 v /\
2682 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==>
2683 dist (v 2,v 3) = &2 * h0 \/ dist (v 0,v 1) = &2*h0
2684 \/ (dist (v 0,v 1) = cstab/\ dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = cstab/\
2685 dist (v 3,v 0) = &2))`,
2690 THEN ASSUME_TAC(SCS_4M8_IS_SCS)
2691 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2692 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`]
2693 THEN THAYTHES_TAC 0[`4`;`0`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8]
2694 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`]
2695 THEN THAYTHES_TAC 0[`5`;`1`][ARITH_RULE`5 MOD 4 = 1 MOD 4`;MOD_MULT_ADD;K_SCS_4M8]
2696 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`]
2697 THEN THAYTHES_TAC 0[`6`;`2`][ARITH_RULE`6 MOD 4 = 2 MOD 4`;MOD_MULT_ADD;K_SCS_4M8]
2698 THEN ASSUME_TAC h0_LT_B_SCS_4M8
2699 THEN ASSUME_TAC SCS_4M8_STAND_OR_PRO
2700 THEN ASSUME_TAC SCS_4M8_BASIC
2701 THEN ASSUME_TAC K_SCS_4M8
2702 THEN ASSUME_TAC SCS_4M8_STAND
2703 THEN MP_TAC (SET_RULE`scs_is_str scs_4M8 v 0\/ ~(scs_is_str scs_4M8 v 0 )`)
2708 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`0`][ARITH_RULE`0+1=1`];
2710 MP_TAC (SET_RULE`scs_is_str scs_4M8 v 2\/ ~(scs_is_str scs_4M8 v 2 )`)
2715 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`2`][ARITH_RULE`2+3=5/\ 2+1=3`]
2716 THEN ONCE_REWRITE_TAC[DIST_SYM]
2717 THEN ASM_REWRITE_TAC[];
2720 MP_TAC (SET_RULE`scs_is_str scs_4M8 v 1\/ ~(scs_is_str scs_4M8 v 1 )`)
2725 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`1`][ARITH_RULE`1+1=2/\ 1+3=4`]
2728 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`3`][ARITH_RULE`1+1=2/\ 3+1=4`]
2729 THEN MRESAS_TAC NOT_STR_IN_CASES_4_1[`0`;`scs_4M8`;`v`][ARITH_RULE`0+a=a`;IN]
2732 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`2`][ARITH_RULE`1+1=2/\ 3+1=4/\ 2+1=3`;IN]
2733 THEN ONCE_REWRITE_TAC[DIST_SYM]
2734 THEN ASM_REWRITE_TAC[];
2736 MP_TAC (SET_RULE`scs_is_str scs_4M8 v 3\/ ~(scs_is_str scs_4M8 v 3 )`)
2741 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`3`][ARITH_RULE`3+1=4/\ 3+3=6`]
2744 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`1`][ARITH_RULE`1+1=2/\ 3+1=4`]
2747 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`0`][ARITH_RULE`0+1=1/\ 3+1=4/\ 2+1=3`;IN]
2748 THEN ONCE_REWRITE_TAC[DIST_SYM]
2749 THEN ASM_REWRITE_TAC[];
2753 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`0`][ARITH_RULE`0+1=1/\ 3+1=4/\ 2+1=3`;IN]
2756 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`2`][ARITH_RULE`0+1=1/\ 3+1=4/\ 2+1=3`;IN]
2759 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`1`][ARITH_RULE`1+1=2/\ 3+1=4/\ 2+1=3`;IN]
2760 THEN MRESAL_TAC STR_MOD_EQ[`4`;`scs_4M8`;`v`;`4`][SCS_4M8_IS_SCS;IN;ARITH_RULE`4 MOD 4=0`]
2763 THEN THAYTHES_TAC 0[`scs_4M8`;`v`;`3`][ARITH_RULE`1+1=2/\ 3+1=4/\ 2+1=3`;IN]]);;
2766 let BB_4M8_IMP_scs_4M8_02=prove(
2767 `main_nonlinear_terminal_v11
2768 ==> (!v. MMs_v39 scs_4M8 v /\
2769 (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
2770 dist (v 0,v 1) = cstab/\ dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = cstab/\
2771 dist (v 3,v 0) = &2 /\ dist(v 0, v 2)<= #3.62
2772 ==> BBs_v39 scs_4M8_02 v)`,
2776 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2778 THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8_02;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8_02;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8]
2779 THEN REPEAT RESA_TAC
2780 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2782 THEN THAYTHE_TAC 2[`i`;`j`]
2785 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2786 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
2787 THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
2788 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
2789 THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
2790 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2792 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
2793 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2795 THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
2796 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2799 THEN ONCE_REWRITE_TAC[DIST_SYM]
2800 THEN ASM_REWRITE_TAC[]
2805 let MM_4M8_IMP_MM_4M8_02=prove(`main_nonlinear_terminal_v11
2806 ==> (!v. MMs_v39 scs_4M8 v /\
2807 (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
2808 dist (v 0,v 1) = cstab/\ dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = cstab/\
2809 dist (v 3,v 0) = &2 /\ dist(v 0, v 2)<= #3.62
2810 ==> ~(MMs_v39 scs_4M8_02={}))`,
2814 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2815 THEN EXISTS_TAC`v:num->real^3`
2816 THEN EXISTS_TAC`scs_4M8`
2817 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8`;`v`]
2818 THEN ASM_SIMP_TAC[SCS_4M8_02_BASIC;SCS_4M8_BASIC;SCS_4M8_02_IS_SCS;SCS_4M8_02_IS_SCS;
2819 SCS_4M8_IS_SCS;K_SCS_4M8_02;K_SCS_4M8;IN;BB_4M8_IMP_scs_4M8_02]
2821 THEN REAL_ARITH_TAC);;
2823 let BB_4M8_IMP_scs_4M8_13=prove(
2824 `main_nonlinear_terminal_v11
2825 ==> (!v. MMs_v39 scs_4M8 v /\
2826 (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
2827 dist (v 0,v 1) = cstab/\ dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = cstab/\
2828 dist (v 3,v 0) = &2 /\ dist(v 1, v 3)<= #3.62
2829 ==> BBs_v39 scs_4M8_13 v)`,
2833 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2835 THEN SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M8_13;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M8_13;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8]
2836 THEN REPEAT RESA_TAC
2837 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2839 THEN THAYTHE_TAC 2[`i`;`j`]
2842 THEN MRESA_TAC MMS_IMP_BBS[`scs_4M8`;`v`]
2843 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
2844 THEN THAYTHES_TAC 0[`i`;`i MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
2845 THEN MRESAL_TAC BB_VV_FUN_EQ[`v`;`scs_4M8`][SCS_4M8_IS_SCS]
2846 THEN THAYTHES_TAC 0[`j`;`j MOD 4`][ARITH_RULE`4 MOD 4 = 0 MOD 4`;MOD_MULT_ADD;K_SCS_4M8;MOD_REFL]
2847 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`i:num`;`j:num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
2849 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
2850 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2852 THEN MP_TAC(ARITH_RULE`j MOD 4<4==> j MOD 4=0\/ j MOD 4=1\/ j MOD 4=2\/ j MOD 4=3`)
2853 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2856 THEN ONCE_REWRITE_TAC[DIST_SYM]
2857 THEN ASM_REWRITE_TAC[]
2862 let MM_4M8_IMP_MM_4M8_13=prove(`main_nonlinear_terminal_v11
2863 ==> (!v. MMs_v39 scs_4M8 v /\
2864 (!i j. scs_diag 4 i j ==> cstab < dist (v i,v j))/\
2865 dist (v 0,v 1) = cstab/\ dist (v 1,v 2) = &2 /\ dist (v 2,v 3) = cstab/\
2866 dist (v 3,v 0) = &2 /\ dist(v 1, v 3)<= #3.62
2867 ==> ~(MMs_v39 scs_4M8_13={}))`,
2871 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2872 THEN EXISTS_TAC`v:num->real^3`
2873 THEN EXISTS_TAC`scs_4M8`
2874 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M8`;`v`]
2875 THEN ASM_SIMP_TAC[SCS_4M8_13_BASIC;SCS_4M8_BASIC;SCS_4M8_13_IS_SCS;SCS_4M8_13_IS_SCS;
2876 SCS_4M8_IS_SCS;K_SCS_4M8_13;K_SCS_4M8;IN;BB_4M8_IMP_scs_4M8_13]
2878 THEN REAL_ARITH_TAC);;
2883 let SCS_4M8_ARROW_STEP_ONE=prove_by_refinement(
2884 `main_nonlinear_terminal_v11
2885 ==> scs_arrow_v39 { scs_4M8 } ({scs_4M6',scs_opp_v39 scs_4M6', scs_4M8_02,scs_4M8_13} UNION {scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j})`,
2887 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM;SET_RULE`a IN {b,c,d,e}<=> a= b\/ a=c\/ a=d\/ a=e`]
2888 THEN ABBREV_TAC`k=scs_k_v39 s`
2889 THEN REPEAT RESA_TAC;
2892 ASM_SIMP_TAC[SCS_4M6_IS_SCS];
2894 MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
2895 THEN EXISTS_TAC`scs_opp_v39 scs_4M6'`
2896 THEN ASM_REWRITE_TAC[SCS_4M6_IS_SCS];
2900 ASM_SIMP_TAC[SCS_4M8_02_IS_SCS];
2902 ASM_SIMP_TAC[SCS_4M8_13_IS_SCS];
2905 ASM_SIMP_TAC[STAB_4M8_SCS;K_SCS_4M8];
2908 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M8 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M8 ==> MMs_v39 s = {}))`);
2915 THEN POP_ASSUM MP_TAC
2916 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
2917 THEN REPEAT STRIP_TAC
2918 THEN POP_ASSUM MP_TAC
2920 THEN POP_ASSUM MP_TAC
2921 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2925 MP_TAC(SET_RULE`(!i j. scs_diag 4 i j ==> cstab < dist(v i,v j))\/ ~((!i j. scs_diag 4 i j ==> cstab < dist((v:num->real^3) i,v j)))`)
2929 MP_TAC MIN_NOT_STAND_4M8
2931 THEN THAYTHE_TAC 0[`v`];
2934 EXISTS_TAC`scs_4M6'`
2935 THEN ASM_REWRITE_TAC[]
2936 THEN MP_TAC MM_4M8_IMP_MM_4M6_23
2937 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2939 THEN MATCH_DICH_TAC 0
2940 THEN ASM_REWRITE_TAC[]
2941 THEN EXISTS_TAC`v:num->real^3`
2942 THEN ASM_REWRITE_TAC[];
2945 EXISTS_TAC`(scs_opp_v39 scs_4M6') `
2946 THEN ASM_REWRITE_TAC[]
2947 THEN MP_TAC MM_4M8_IMP_MM_4M6_01
2948 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2950 THEN MATCH_DICH_TAC 0
2951 THEN ASM_REWRITE_TAC[]
2952 THEN EXISTS_TAC`v:num->real^3`
2953 THEN ASM_REWRITE_TAC[];
2955 MP_TAC Bkossge.quad_diag_362
2957 THEN THAYTHE_TAC 0[`v 1`;`v 2`;`v 3`;`v 0`]
2959 THEN ONCE_REWRITE_TAC[DIST_SYM]
2960 THEN ASM_REWRITE_TAC[]
2961 THEN ONCE_REWRITE_TAC[DIST_SYM]
2965 EXISTS_TAC`(scs_4M8_13) `
2966 THEN ASM_REWRITE_TAC[]
2967 THEN MP_TAC MM_4M8_IMP_MM_4M8_13
2968 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2970 THEN MATCH_DICH_TAC 0
2971 THEN ASM_REWRITE_TAC[]
2972 THEN EXISTS_TAC`v:num->real^3`
2973 THEN ASM_REWRITE_TAC[];
2976 THEN ONCE_REWRITE_TAC[DIST_SYM]
2978 THEN EXISTS_TAC`(scs_4M8_02) `
2979 THEN ASM_REWRITE_TAC[]
2980 THEN MP_TAC MM_4M8_IMP_MM_4M8_02
2981 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2983 THEN MATCH_DICH_TAC 0
2984 THEN ASM_REWRITE_TAC[]
2985 THEN EXISTS_TAC`v:num->real^3`
2986 THEN ASM_REWRITE_TAC[];
2991 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
2993 THEN MP_TAC MM_4M8_IMP_STAB_4M8
2996 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2998 THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M8 i j`
2999 THEN ASM_REWRITE_TAC[]
3003 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
3004 THEN EXISTS_TAC`i:num`
3005 THEN EXISTS_TAC`j:num`
3006 THEN ASM_REWRITE_TAC[];
3009 EXISTS_TAC`v':num->real^3`
3010 THEN ASM_REWRITE_TAC[];
3018 (****************************)
3025 let SCS_DIAG_SCS_4M8_02_02=prove(`scs_diag (scs_k_v39 scs_4M8_02) 0 2`,
3026 REWRITE_TAC[K_SCS_4M8_02;scs_diag]
3029 let SCS_DIAG_SCS_4M8_02_13=prove(`scs_diag (scs_k_v39 scs_4M8_02) 1 3`,
3030 REWRITE_TAC[K_SCS_4M8_02;scs_diag]
3033 let SCS_DIAG_SCS_4M8_13_13=prove(`scs_diag (scs_k_v39 scs_4M8_13) 1 3`,
3034 REWRITE_TAC[K_SCS_4M8_13;scs_diag]
3038 let STAB_4M8_02_SCS=prove(` scs_diag (scs_k_v39 scs_4M8_02) i j
3039 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M8_02 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M8_02 i j)`,
3041 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
3042 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M8_02_IS_SCS;SCS_4M8_02_BASIC;K_SCS_4M8_02;
3043 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
3045 THEN REWRITE_TAC[h0;cstab]
3046 THEN MP_TAC sqrt8_LE_CSTAB
3047 THEN MP_TAC LE_sqrt8_2h0
3048 THEN REAL_ARITH_TAC);;
3051 let STAB_4M8_13_SCS=prove(` scs_diag (scs_k_v39 scs_4M8_13) i j
3052 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M8_13 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M8_13 i j)`,
3054 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
3055 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M8_13_IS_SCS;SCS_4M8_13_BASIC;K_SCS_4M8_13;
3056 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
3058 THEN REWRITE_TAC[h0;cstab]
3059 THEN MP_TAC sqrt8_LE_CSTAB
3060 THEN MP_TAC LE_sqrt8_2h0
3061 THEN REAL_ARITH_TAC);;
3063 let BASIC_HALF_SLICE=prove(`scs_basic_v39 s
3064 ==> scs_basic_v39 (scs_half_slice_v39 (s) p q d' F)`,
3065 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]
3068 let D_HALF_SLICE1=prove(`scs_d_v39 (scs_half_slice_v39 (s) p q d' mkj)=d'`,
3071 let J_SCS_3T7_OPP_PROP=prove(`scs_J_v39 (scs_prop_equ_v39 (scs_opp_v39 scs_3T7) i) i1 j= F`,
3072 REWRITE_TAC[scs_opp_v39;peropp2]
3074 THEN REWRITE_TAC[scs_opp_v39;peropp2]);;
3077 let J_SCS_3T7_OPP=prove(`scs_J_v39 ((scs_opp_v39 scs_3T7) ) i1 j= F`,
3078 REWRITE_TAC[scs_opp_v39;peropp2]
3080 THEN REWRITE_TAC[scs_opp_v39;peropp2]);;
3084 let SCS_4M8_02_SLICE_02=prove_by_refinement(`scs_arrow_v39 {scs_4M8_02 } {scs_prop_equ_v39
3085 ( scs_opp_v39 scs_3T7) 2 }`,
3088 ONCE_REWRITE_TAC[SET_RULE`{scs_prop_equ_v39
3089 ( scs_opp_v39 scs_3T7) 2}={scs_prop_equ_v39
3090 ( scs_opp_v39 scs_3T7) 2, scs_prop_equ_v39
3091 ( scs_opp_v39 scs_3T7) 2 }`]
3092 THEN MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
3093 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_02_13;STAB_4M8_02_SCS;SCS_K_D_A_STAB_EQ;SCS_4M8_02_IS_SCS]
3096 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_02_02]
3097 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
3098 THEN REPEAT RESA_TAC;
3100 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
3102 THEN MATCH_MP_TAC scs_inj
3103 THEN ASM_SIMP_TAC[SCS_3T7_BASIC;SCS_4M8_02_BASIC;J_SCS_4M8_02;BASIC_HALF_SLICE_STAB;J_SCS_3T7;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T7_BASIC;J_SCS_3T7_OPP_PROP;BASIC_HALF_SLICE;D_HALF_SLICE1;Cqaoqlr.BASIC_OPP;SCS_3T7_IS_SCS]
3106 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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_02;scs_opp_v39]
3111 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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_02;scs_opp_v39;peropp2;
3112 ARITH_RULE`(2 + 1 + 4 - 0) MOD 4= 3/\ 0 MOD 4=0/\ a+0=a`;scs_prop_equ_v39]
3113 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3114 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3117 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
3118 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;peropp2;]
3120 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
3121 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
3123 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3124 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]
3125 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
3126 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
3127 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
3128 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
3129 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
3130 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
3132 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/\
3133 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3134 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3135 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
3136 THEN REPEAT RESA_TAC
3137 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)
3138 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
3139 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
3140 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3141 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3142 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
3146 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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_02;scs_opp_v39]
3151 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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_02;peropp2;scs_opp_v39;
3152 ARITH_RULE`(0 + 1 + 4 - 2) MOD 4= 3/\ 2 MOD 4=2/\ a+0=a`;scs_prop_equ_v39]
3153 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3154 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3157 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
3158 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;peropp2]
3160 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
3161 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
3163 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3164 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]
3165 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
3166 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
3167 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
3168 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
3169 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
3170 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
3172 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/\
3173 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3174 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3175 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
3176 THEN REPEAT RESA_TAC
3177 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)
3178 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
3179 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
3180 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3181 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3182 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
3186 REWRITE_TAC[scs_opp_v39]
3188 THEN REAL_ARITH_TAC;
3190 REWRITE_TAC[scs_opp_v39]
3192 THEN REAL_ARITH_TAC;
3194 REWRITE_TAC[scs_opp_v39]
3196 THEN REAL_ARITH_TAC;
3198 REWRITE_TAC[scs_opp_v39]
3200 THEN REWRITE_TAC[cstab]
3201 THEN REAL_ARITH_TAC;
3205 THEN REWRITE_TAC[cstab]
3206 THEN REAL_ARITH_TAC;
3209 THEN REWRITE_TAC[J_SCS_3T7_OPP_PROP];
3216 let SCS_4M8_13_SLICE_13=prove_by_refinement(`scs_arrow_v39 {scs_4M8_13 } {scs_prop_equ_v39 scs_3T7 1}`,
3218 ONCE_REWRITE_TAC[SET_RULE`{scs_prop_equ_v39
3219 ( scs_3T7) 1}={scs_prop_equ_v39
3220 ( scs_3T7) 1, scs_prop_equ_v39
3222 THEN MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
3223 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_13_13;STAB_4M8_13_SCS;SCS_K_D_A_STAB_EQ;SCS_4M8_13_IS_SCS]
3226 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M8_13_13]
3227 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
3228 THEN REPEAT RESA_TAC;
3230 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
3232 THEN MATCH_MP_TAC scs_inj
3233 THEN ASM_SIMP_TAC[SCS_3T7_BASIC;SCS_4M8_13_BASIC;J_SCS_4M8_13;BASIC_HALF_SLICE_STAB;J_SCS_3T7;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T7_BASIC;J_SCS_3T7_1;BASIC_HALF_SLICE;D_HALF_SLICE1;Cqaoqlr.BASIC_OPP;SCS_3T7_IS_SCS]
3236 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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_13;scs_opp_v39]
3241 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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_13;scs_opp_v39;peropp2;
3242 ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
3243 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3244 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3247 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
3248 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;peropp2;]
3250 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
3251 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
3253 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3254 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]
3255 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
3256 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
3257 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
3258 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
3259 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
3260 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
3262 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/\
3263 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3264 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3265 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
3266 THEN REPEAT RESA_TAC
3267 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)
3268 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
3269 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
3270 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3271 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3272 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
3276 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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_13;scs_opp_v39]
3281 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_3T7;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M8_13;peropp2;scs_opp_v39;
3282 ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
3283 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3284 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
3287 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
3288 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION;peropp2]
3290 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
3291 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
3293 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3294 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]
3295 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
3296 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
3297 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
3298 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
3299 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
3300 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
3302 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/\
3303 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3304 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
3305 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
3306 THEN REPEAT RESA_TAC
3307 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)
3308 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
3309 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
3310 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
3311 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
3312 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
3316 REWRITE_TAC[scs_opp_v39]
3318 THEN REAL_ARITH_TAC;
3320 REWRITE_TAC[scs_opp_v39]
3322 THEN REAL_ARITH_TAC;
3324 REWRITE_TAC[scs_opp_v39]
3326 THEN REAL_ARITH_TAC;
3328 REWRITE_TAC[scs_opp_v39]
3330 THEN REWRITE_TAC[cstab]
3331 THEN REAL_ARITH_TAC;
3334 THEN REWRITE_TAC[cstab]
3335 THEN REAL_ARITH_TAC;
3338 THEN REWRITE_TAC[J_SCS_3T7];
3345 let SCS_4M8_13_ARROW_3T7=prove(`scs_arrow_v39 {scs_4M8_13 } {scs_3T7 }`,
3346 MATCH_MP_TAC FZIOTEF_TRANS
3347 THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3T7 1}`
3348 THEN ASM_REWRITE_TAC[SCS_4M8_13_SLICE_13]
3349 THEN MRESAS_TAC PRO_EQU_ID1[`scs_3T7`;`1`;`3`][SCS_3T7_IS_SCS;K_SCS_3T7;ARITH_RULE`(3 - 1 MOD 3)=2`]
3350 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T7 1`;`2`][PROP_EQU_IS_SCS;SCS_3T7_IS_SCS]
3352 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
3353 THEN REWRITE_TAC[]);;
3355 let K_SCS_OPP_3T7=prove(`scs_k_v39 (scs_opp_v39 scs_3T7) = 3`,
3356 ASM_REWRITE_TAC[scs_opp_v39;scs_prop_equ_v39]
3359 let SCS_3T7_OPP_IS_SCS=prove(`is_scs_v39 (scs_opp_v39 scs_3T7)`,
3360 MATCH_MP_TAC(GEN_ALL OPP_IS_SCS)
3361 THEN EXISTS_TAC`scs_opp_v39 scs_3T7`
3362 THEN ASM_REWRITE_TAC[SCS_3T7_IS_SCS]);;
3366 let SCS_4M8_13_ARROW_3T7_OPP=prove(`scs_arrow_v39 {scs_4M8_02 } {scs_opp_v39 scs_3T7}`,
3367 MATCH_MP_TAC FZIOTEF_TRANS
3368 THEN EXISTS_TAC`{scs_prop_equ_v39
3369 ( scs_opp_v39 scs_3T7) 2}`
3370 THEN ASM_REWRITE_TAC[SCS_4M8_02_SLICE_02]
3371 THEN MRESAS_TAC PRO_EQU_ID1[`scs_opp_v39 scs_3T7`;`2`;`3`][SCS_3T7_IS_SCS;K_SCS_3T7;ARITH_RULE`(3 - 2 MOD 3)=1`;K_SCS_OPP_3T7;SCS_3T7_OPP_IS_SCS]
3372 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 (scs_opp_v39 scs_3T7) 2`;`1`][PROP_EQU_IS_SCS;SCS_3T7_IS_SCS;K_SCS_OPP_3T7;SCS_3T7_OPP_IS_SCS]
3374 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
3377 THEN MATCH_MP_TAC FZIOTEF_TRANS
3378 THEN EXISTS_TAC`{scs_opp_v39 scs_3T7}`
3379 THEN ASM_REWRITE_TAC[]
3380 THEN ASSUME_TAC SCS_3T7_IS_SCS
3381 THEN MRESA_TAC Yxionxl2.SCS_OPP_REFL[`scs_3T7`]
3382 THEN MRESAS_TAC YXIONXL2[`3`;`scs_opp_v39 scs_3T7`][K_SCS_OPP_3T7;SCS_3T7_OPP_IS_SCS;ARITH_RULE`~(4<=3)`]);;
3386 let PROP_OPP_4M8_13= prove_by_refinement(
3387 `scs_4M8_13= scs_prop_equ_v39(scs_opp_v39 (scs_4M8_02)) 2 `,
3388 [REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39;SCS_K_D_A_STAB_EQ;scs_opp_v39;scs_4M8_13;scs_4M8_02]
3389 THEN MATCH_MP_TAC scs_inj
3390 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M8_BASIC;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_13;scs_basic;unadorned_v39;peropp;peropp2]
3397 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;]
3398 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
3400 THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
3401 THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
3403 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
3404 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
3407 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`)
3408 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
3410 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`)
3411 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
3413 THEN ASM_REWRITE_TAC[Uxckfpe.ARITH_4_TAC;PSORT_5_EXPLICIT;ARITH_RULE`4-1=3/\ 4-2=2/\ 4-3=1/\ 4-4=0/\ 5-5=0/\ 2+0=2/\ 2+1=3/\ 2+2=4/\ 2+3=5/\2+4=6
3414 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;
3419 let SCS_4M8_02_ARROW_4M8_13=prove(
3420 `scs_arrow_v39 {scs_4M8_02}{scs_4M8_13}`,
3421 ASM_SIMP_TAC[PROP_OPP_4M8_13]
3422 THEN MATCH_MP_TAC FZIOTEF_TRANS
3423 THEN EXISTS_TAC`{scs_opp_v39 (scs_4M8_02)}`
3426 MATCH_MP_TAC (GEN_ALL YXIONXL2)
3428 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M8_02;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02;SCS_4M8_02_IS_SCS];
3430 MATCH_MP_TAC(GEN_ALL YXIONXL3)
3431 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
3432 THEN EXISTS_TAC`scs_opp_v39 ( scs_4M8_02)`
3433 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M8;STAB_4M8_SCS;SCS_DIAG_SCS_4M8_02;SCS_4M8_02_IS_SCS];]);;
3437 let SCS_4M8_02_ARROW_3T7 =prove(`scs_arrow_v39 { scs_4M8_02 } { scs_3T7 }`,
3438 MATCH_MP_TAC FZIOTEF_TRANS
3439 THEN EXISTS_TAC`{scs_4M8_13}`
3440 THEN ASM_SIMP_TAC[SCS_4M8_02_ARROW_4M8_13;SCS_4M8_13_ARROW_3T7]);;
3443 (************************************)
3445 let MIQMCSN=prove(`main_nonlinear_terminal_v11
3446 ==> scs_arrow_v39 { scs_4M8 } ({scs_4M6',scs_3T7,scs_3T4})`,
3448 THEN MATCH_MP_TAC FZIOTEF_TRANS
3449 THEN EXISTS_TAC`({scs_4M6',scs_opp_v39 scs_4M6', scs_4M8_02,scs_4M8_13} UNION {scs_stab_diag_v39 scs_4M8 i j| scs_diag 4 i j})`
3450 THEN ASM_SIMP_TAC[SCS_4M8_ARROW_STEP_ONE;SET_RULE`{scs_4M6', scs_3T7, scs_3T4}={scs_4M6', scs_3T7}UNION{ scs_3T4}`]
3451 THEN MATCH_MP_TAC FZIOTEF_UNION
3452 THEN ASM_REWRITE_TAC[SET_STAB_4M8_ARROW_3T4;]
3453 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_4M6', scs_3T7}={scs_4M6',scs_4M6', scs_3T7,scs_3T7}`]
3454 THEN ASM_REWRITE_TAC[SET_RULE` {A,B,C,D}=({A,B,C}) UNION {D}`]
3455 THEN MATCH_MP_TAC FZIOTEF_UNION
3456 THEN ASM_REWRITE_TAC[SCS_4M8_13_ARROW_3T7;SET_RULE` {A,B,D}=({A,B}) UNION {D}`]
3457 THEN MATCH_MP_TAC FZIOTEF_UNION
3458 THEN ASM_REWRITE_TAC[SCS_4M8_02_ARROW_3T7;SET_RULE` {A,D}=({A}) UNION {D}`]
3459 THEN MATCH_MP_TAC FZIOTEF_UNION
3462 MATCH_MP_TAC FZIOTEF_REFL
3463 THEN REWRITE_TAC[IN_SING]
3464 THEN REPEAT RESA_TAC
3465 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS];
3467 ASSUME_TAC(SCS_4M6_IS_SCS)
3468 THEN ASSUME_TAC K_SCS_OPP_4M6
3469 THEN ASSUME_TAC SCS_4M6_OPP_IS_SCS
3470 THEN MRESA_TAC Yxionxl2.SCS_OPP_REFL[`scs_4M6'`]
3471 THEN MRESAL_TAC YXIONXL2[`4`;`scs_opp_v39 scs_4M6'`][ARITH_RULE`~(4<=3)`]]);;
3478 let check_completeness_claimA_concl =
3479 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)