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 Aueaheh = struct
28 open Wrgcvdr_cizmrrh;;
36 open Flyspeck_constants;;
52 open Wrgcvdr_cizmrrh;;
54 open Flyspeck_constants;;
100 let SCS_DIAG_SCS_4I1_02=prove(`scs_diag (scs_k_v39 scs_4I1) 0 2`,
101 REWRITE_TAC[K_SCS_4I1;scs_diag]
106 let SCS_4I1_SLICE_02=prove_by_refinement(
107 `scs_arrow_v39 {scs_stab_diag_v39 scs_4I1 0 2 } { scs_prop_equ_v39 scs_3M1 1}`,
108 [ONCE_REWRITE_TAC[SET_RULE`{ scs_prop_equ_v39 scs_3M1 1}={ scs_prop_equ_v39 scs_3M1 1, scs_prop_equ_v39 scs_3M1 1}`]
110 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
111 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4I1_02;STAB_4I1_SCS;SCS_K_D_A_STAB_EQ;]
114 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4I1_02]
115 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
116 THEN REPEAT RESA_TAC;
119 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
121 THEN MATCH_MP_TAC scs_inj
122 THEN ASM_SIMP_TAC[SCS_3M1_BASIC;SCS_4I1_BASIC;J_SCS_4I1;BASIC_HALF_SLICE_STAB;J_SCS_3M1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4I1_BASIC]
125 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4I1]
132 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4I1;scs_3T4_prime;scs_5M3;
133 ARITH_RULE`(2 + 1 + 4 - 0) MOD 4= 3/\ 0 MOD 4=0/\ a+0=a`;scs_prop_equ_v39]
134 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
135 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
138 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
139 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
141 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
142 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
144 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
145 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]
146 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
147 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
148 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
149 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
150 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
151 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
153 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/\
154 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
155 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
156 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
158 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)
159 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
160 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
161 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
162 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
163 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
168 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4I1]
174 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4I1;scs_3T4_prime;scs_5M3;
175 ARITH_RULE`(0 + 1 + 4 - 2) MOD 4= 3/\ 2 MOD 4=2/\ a+0=a`;scs_prop_equ_v39]
176 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
177 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
180 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
181 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
183 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
184 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
186 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
187 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]
188 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
189 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
190 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
191 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
192 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
193 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
195 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/\
196 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
197 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
198 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
200 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)
201 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
202 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
203 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
204 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
205 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
226 THEN REWRITE_TAC[cstab]
232 THEN REWRITE_TAC[cstab]
238 THEN REWRITE_TAC[J_SCS_3M1];
244 let AUEAHEH=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4I1 0 2 } {scs_3M1}`,
245 MATCH_MP_TAC FZIOTEF_TRANS
246 THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_3M1 1}`
247 THEN ASM_REWRITE_TAC[SCS_4I1_SLICE_02]
248 THEN MRESAS_TAC PRO_EQU_ID1[`scs_3M1`;`1`;`3`][SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`(3 - 1 MOD 3)=2`]
249 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1 1`;`2`][PROP_EQU_IS_SCS;SCS_3M1_IS_SCS]
251 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
252 THEN REWRITE_TAC[]);;
255 (*************************)
257 let BB_4I3_IMP_4T4=prove(`!v.
258 BBs_v39 (scs_stab_diag_v39 scs_4I3 1 3) v
260 BBs_v39 (scs_4T4) v`,
261 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4I3;scs_4T4;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;]
263 THEN THAYTHE_TAC 1[`i`;`j`]
265 THEN MP_TAC(SET_RULE`psort 4 (i,j) = 1,3\/ ~(psort 4 (i,j) = 1,3)`)
267 THEN MRESAL_TAC Uaghhbm.CASE_PSORT[`i`;`3`;`j`;`1`;`4`][PSORT_5_EXPLICIT;Uxckfpe.ARITH_4_TAC;PAIR_EQ;cstab]
273 let STAB_4I3_SCS=prove(` scs_diag (scs_k_v39 scs_4I3) i j
274 ==> is_scs_v39 (scs_stab_diag_v39 scs_4I3 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4I3 i j)`,
276 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
277 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4I3_IS_SCS;SCS_4I3_BASIC;K_SCS_4I3;
278 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
280 THEN REWRITE_TAC[h0;cstab]
281 THEN MP_TAC sqrt8_LE_CSTAB
282 THEN REAL_ARITH_TAC);;
284 let STAB_4M2_SCS=prove(` scs_diag (scs_k_v39 scs_4M2) i j
285 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M2 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M2 i j)`,
287 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
288 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M2_IS_SCS;SCS_4M2_BASIC;K_SCS_4M2;
289 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
291 THEN REWRITE_TAC[h0;cstab]
292 THEN MP_TAC sqrt8_LE_CSTAB
293 THEN REAL_ARITH_TAC);;
296 let STAB_4M3_SCS=prove(` scs_diag (scs_k_v39 scs_4M3') i j
297 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M3' i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M3' i j)`,
299 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
300 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M3_IS_SCS;SCS_4M3_BASIC;K_SCS_4M3;
301 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
303 THEN REWRITE_TAC[h0;cstab]
304 THEN MP_TAC sqrt8_LE_CSTAB
305 THEN MP_TAC LE_sqrt8_2h0
306 THEN REAL_ARITH_TAC);;
308 let STAB_4M4_SCS=prove(` scs_diag (scs_k_v39 scs_4M4') i j
309 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M4' i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M4' i j)`,
311 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
312 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M4_IS_SCS;SCS_4M4_BASIC;K_SCS_4M4;
313 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
315 THEN REWRITE_TAC[h0;cstab]
316 THEN MP_TAC sqrt8_LE_CSTAB
317 THEN MP_TAC LE_sqrt8_2h0
318 THEN REAL_ARITH_TAC);;
322 let STAB_4M5_SCS=prove(` scs_diag (scs_k_v39 scs_4M5') i j
323 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M5' i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M5' i j)`,
325 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
326 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M5_IS_SCS;SCS_4M5_BASIC;K_SCS_4M5;
327 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
329 THEN REWRITE_TAC[h0;cstab]
330 THEN MP_TAC sqrt8_LE_CSTAB
331 THEN MP_TAC LE_sqrt8_2h0
332 THEN REAL_ARITH_TAC);;
336 let STAB_4M6_SCS=prove(` scs_diag (scs_k_v39 scs_4M6') i j
337 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M6' i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M6' i j)`,
339 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
340 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;
341 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
343 THEN REWRITE_TAC[h0;cstab]
344 THEN MP_TAC sqrt8_LE_CSTAB
345 THEN MP_TAC LE_sqrt8_2h0
346 THEN REAL_ARITH_TAC);;
349 let STAB_4M7_SCS=prove(` scs_diag (scs_k_v39 scs_4M7) i j
350 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M7 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M7 i j)`,
352 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
353 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M7_IS_SCS;SCS_4M7_BASIC;K_SCS_4M7;
354 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
356 THEN REWRITE_TAC[h0;cstab]
357 THEN MP_TAC sqrt8_LE_CSTAB
358 THEN MP_TAC LE_sqrt8_2h0
359 THEN REAL_ARITH_TAC);;
362 let STAB_4M8_SCS=prove(` scs_diag (scs_k_v39 scs_4M8) i j
363 ==> is_scs_v39 (scs_stab_diag_v39 scs_4M8 i j)/\ scs_basic_v39 (scs_stab_diag_v39 scs_4M8 i j)`,
365 THEN MATCH_MP_TAC Yrtafyh.YRTAFYH
366 THEN ASM_REWRITE_TAC[SCS_K_D_A_STAB_EQ;SCS_4M8_IS_SCS;SCS_4M8_BASIC;K_SCS_4M8;
367 ARITH_RULE`3<4`;LET_DEF;LET_END_DEF;scs_v39_explicit;mk_unadorned_v39;CS_ADJ;h0;cstab]
369 THEN REWRITE_TAC[h0;cstab]
370 THEN MP_TAC sqrt8_LE_CSTAB
371 THEN MP_TAC LE_sqrt8_2h0
372 THEN REAL_ARITH_TAC);;
374 let SCS_DIAG_SCS_4I3_02=prove(`scs_diag (scs_k_v39 scs_4I3) 0 2`,
375 REWRITE_TAC[K_SCS_4I3;scs_diag]
378 let SCS_DIAG_SCS_4I3_13=prove(`scs_diag (scs_k_v39 scs_4I3) 1 3`,
379 REWRITE_TAC[K_SCS_4I3;scs_diag]
383 let SCS_DIAG_SCS_4M2_02=prove(`scs_diag (scs_k_v39 scs_4M2) 0 2`,
384 REWRITE_TAC[K_SCS_4M2;scs_diag]
387 let SCS_DIAG_SCS_4M2_13=prove(`scs_diag (scs_k_v39 scs_4M2) 1 3`,
388 REWRITE_TAC[K_SCS_4M2;scs_diag]
392 let SCS_DIAG_SCS_4M3_02=prove(`scs_diag (scs_k_v39 scs_4M3') 0 2`,
393 REWRITE_TAC[K_SCS_4M3;scs_diag]
396 let SCS_DIAG_SCS_4M3_13=prove(`scs_diag (scs_k_v39 scs_4M3') 1 3`,
397 REWRITE_TAC[K_SCS_4M3;scs_diag]
400 let SCS_DIAG_SCS_4M4_02=prove(`scs_diag (scs_k_v39 scs_4M4') 0 2`,
401 REWRITE_TAC[K_SCS_4M4;scs_diag]
404 let SCS_DIAG_SCS_4M4_13=prove(`scs_diag (scs_k_v39 scs_4M4') 1 3`,
405 REWRITE_TAC[K_SCS_4M4;scs_diag]
408 let SCS_DIAG_SCS_4M5_02=prove(`scs_diag (scs_k_v39 scs_4M5') 0 2`,
409 REWRITE_TAC[K_SCS_4M5;scs_diag]
412 let SCS_DIAG_SCS_4M5_13=prove(`scs_diag (scs_k_v39 scs_4M5') 1 3`,
413 REWRITE_TAC[K_SCS_4M5;scs_diag]
416 let SCS_DIAG_SCS_4M6_02=prove(`scs_diag (scs_k_v39 scs_4M6') 0 2`,
417 REWRITE_TAC[K_SCS_4M6;scs_diag]
420 let SCS_DIAG_SCS_4M6_13=prove(`scs_diag (scs_k_v39 scs_4M6') 1 3`,
421 REWRITE_TAC[K_SCS_4M6;scs_diag]
425 let SCS_DIAG_SCS_4M7_02=prove(`scs_diag (scs_k_v39 scs_4M7) 0 2`,
426 REWRITE_TAC[K_SCS_4M7;scs_diag]
429 let SCS_DIAG_SCS_4M7_13=prove(`scs_diag (scs_k_v39 scs_4M7) 1 3`,
430 REWRITE_TAC[K_SCS_4M7;scs_diag]
433 let SCS_DIAG_SCS_4M8_02=prove(`scs_diag (scs_k_v39 scs_4M8) 0 2`,
434 REWRITE_TAC[K_SCS_4M8;scs_diag]
437 let SCS_DIAG_SCS_4M8_13=prove(`scs_diag (scs_k_v39 scs_4M8) 1 3`,
438 REWRITE_TAC[K_SCS_4M8;scs_diag]
442 let MM_4I3_IMP_4T4=prove(`MMs_v39 (scs_stab_diag_v39 scs_4I3 1 3) v
444 ~(MMs_v39 (scs_4T4) ={})`,
446 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
447 THEN EXISTS_TAC`v:num->real^3`
448 THEN EXISTS_TAC`(scs_stab_diag_v39 scs_4I3 1 3)`
449 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`(scs_stab_diag_v39 scs_4I3 1 3)`;`v`]
450 THEN ASSUME_TAC SCS_4T4_BASIC
451 THEN ASSUME_TAC K_SCS_4T4
452 THEN ASM_SIMP_TAC[SCS_4T4_IS_SCS;STAB_4I3_SCS;K_SCS_4I3;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4I3_13;BB_4I3_IMP_4T4]
454 THEN REAL_ARITH_TAC);;
459 let SCS_4I3_ARROW_4T4 =prove_by_refinement(`scs_arrow_v39 { scs_stab_diag_v39 scs_4I3 1 3 } { scs_4T4 }`,
462 THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
463 THEN ABBREV_TAC`k=scs_k_v39 s`
464 THEN REPEAT RESA_TAC;
466 ASM_SIMP_TAC[SCS_4T4_IS_SCS];
468 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_stab_diag_v39 scs_4I3 1 3 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_stab_diag_v39 scs_4I3 1 3 ==> MMs_v39 s = {}))`);
473 THEN POP_ASSUM MP_TAC
474 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
475 THEN REPEAT STRIP_TAC
476 THEN POP_ASSUM MP_TAC
478 THEN EXISTS_TAC`scs_4T4`
479 THEN ASM_REWRITE_TAC[]
480 THEN MATCH_MP_TAC (GEN_ALL MM_4I3_IMP_4T4)
481 THEN POP_ASSUM MP_TAC
486 let PROP_OPP_DIAG_4I3_13= prove_by_refinement(`scs_stab_diag_v39 scs_4I3 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4I3 0 2)) 2 `,
487 [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]
488 THEN MATCH_MP_TAC scs_inj
489 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4I3_BASIC;STAB_4I3_SCS;SCS_DIAG_SCS_4I3_13;scs_basic;unadorned_v39;peropp;peropp2]
497 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;]
498 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
500 THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
501 THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
503 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
504 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
507 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`)
508 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
510 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`)
511 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
513 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
514 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;
520 let STAB_4I3_02_ARROW_4I3_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4I3 0 2}{scs_stab_diag_v39 scs_4I3 1 3}`,
521 ASM_SIMP_TAC[PROP_OPP_DIAG_4I3_13]
522 THEN MATCH_MP_TAC FZIOTEF_TRANS
523 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4I3 0 2)}`
526 MATCH_MP_TAC (GEN_ALL YXIONXL2)
528 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4I3;STAB_4I3_SCS;SCS_DIAG_SCS_4I3_02]
531 MATCH_MP_TAC(GEN_ALL YXIONXL3)
532 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
533 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4I3 0 2)`
534 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4I3;STAB_4I3_SCS;SCS_DIAG_SCS_4I3_02]]);;
538 let ZNLLLDL=prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_4I3 0 2 } { scs_4T4 }`,
539 MATCH_MP_TAC FZIOTEF_TRANS
540 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4I3 1 3}`
541 THEN ASM_SIMP_TAC[STAB_4I3_02_ARROW_4I3_13;SCS_4I3_ARROW_4T4]);;
546 let h0_LT_B_SCS_4I3=prove(`
547 (!i j. scs_diag 4 i j ==> &4 * h0 < scs_b_v39 scs_4I3 i j)
548 /\ (!i j. scs_diag 4 i j ==> scs_a_v39 scs_4I3 i j <= cstab)`,
550 THEN REWRITE_TAC[h0;SCS_DIAG_4_CASES;cstab]
552 THEN ASSUME_TAC(ARITH_RULE`~(4=0)`)
553 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
556 THEN MP_TAC sqrt8_LE_CSTAB
557 THEN REAL_ARITH_TAC);;
560 let B_LE_CSTAB_SCS_4I3=prove(
561 ` (!i. scs_b_v39 scs_4I3 i (SUC i) <= cstab)`,
563 THEN REWRITE_TAC[h0;scs_diag;cstab]
565 THEN ASM_SIMP_TAC[ARITH_RULE`1<4`;Qknvmlb.SUC_MOD_NOT_EQ;]
566 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
567 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`SUC i`]
569 THEN REWRITE_TAC[ADD1]
570 THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`]
572 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`)
573 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
576 THEN MP_TAC sqrt8_LE_CSTAB
577 THEN REAL_ARITH_TAC);;
581 let BB_4I3_IMP_BB_4M6= prove
584 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==>
585 BBs_v39 (scs_4M6') v`,
586 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4I3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
588 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
590 THEN THAYTHE_TAC 1[`i`;`j`]
592 THEN THAYTHE_TAC 2[`i`;`j`]
595 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
597 THEN REWRITE_TAC[ADD1]
598 THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`]
600 THEN MRESA_TAC MOD_ADD_MOD[`j`;`1`;`4`]
602 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`)
603 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
605 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`)
606 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
609 THEN MP_TAC sqrt8_LE_CSTAB
610 THEN REWRITE_TAC[cstab;h0]
611 THEN REAL_ARITH_TAC);;
615 let MM_4I3_IMP_4M6=prove(`
617 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==>
618 ~(MMs_v39 (scs_4M6') ={})`,
620 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
621 THEN EXISTS_TAC`v:num->real^3`
622 THEN EXISTS_TAC` scs_4I3 `
623 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I3 `;`v`]
624 THEN ASSUME_TAC SCS_4M6_BASIC
625 THEN ASSUME_TAC K_SCS_4M6
626 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4I3_IS_SCS;SCS_4I3_BASIC;K_SCS_4I3;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4I3_13;BB_4I3_IMP_BB_4M6]
628 THEN REAL_ARITH_TAC);;
633 let BB_4I3_IMP_BB_STAN_4I3= prove(`
636 dist(v i,v j)<= cstab ==>
637 BBs_v39 (scs_stab_diag_v39 scs_4I3 i j) v`,
638 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4I3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
640 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
642 THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
644 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
646 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I3`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4I3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4I3_IS_SCS]
647 THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
648 THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
650 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4I3`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4I3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4I3_IS_SCS]
651 THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
652 THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
653 THEN ONCE_REWRITE_TAC[DIST_SYM]
654 THEN ASM_REWRITE_TAC[]]);;
657 let MM_4I3_IMP_STAB_4I3=prove(`
660 dist(v i,v j)<= cstab ==>
661 ~(MMs_v39 (scs_stab_diag_v39 scs_4I3 i j) ={})`,
663 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
664 THEN EXISTS_TAC`v:num->real^3`
665 THEN EXISTS_TAC` scs_4I3 `
666 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4I3 `;`v`]
667 THEN ASSUME_TAC SCS_4I3_BASIC
668 THEN ASSUME_TAC K_SCS_4I3
669 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4I3_IS_SCS;SCS_4I3_BASIC;K_SCS_4I3;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4I3_13;BB_4I3_IMP_BB_STAN_4I3;STAB_4I3_SCS]
671 THEN REAL_ARITH_TAC);;
673 let SCS_4I3_ARROW_SCS_4M6_STAB_4I3=prove_by_refinement(
674 ` scs_arrow_v39 { scs_4I3 } ({scs_4M6'} UNION {scs_stab_diag_v39 scs_4I3 i j| scs_diag 4 i j})`,
676 REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM]
677 THEN ABBREV_TAC`k=scs_k_v39 s`
678 THEN REPEAT RESA_TAC;
681 ASM_SIMP_TAC[SCS_4M6_IS_SCS];
684 ASM_SIMP_TAC[STAB_4I3_SCS;K_SCS_4I3];
687 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4I3 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4I3 ==> MMs_v39 s = {}))`);
695 THEN POP_ASSUM MP_TAC
696 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
697 THEN REPEAT STRIP_TAC
698 THEN POP_ASSUM MP_TAC
700 THEN POP_ASSUM MP_TAC
701 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
705 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)))`)
710 THEN ASM_REWRITE_TAC[]
711 THEN MP_TAC MM_4I3_IMP_4M6
712 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
714 THEN MATCH_DICH_TAC 0
715 THEN ASM_REWRITE_TAC[]
716 THEN EXISTS_TAC`v:num->real^3`
717 THEN ASM_REWRITE_TAC[];
721 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
723 THEN MP_TAC MM_4I3_IMP_STAB_4I3
726 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
728 THEN EXISTS_TAC `scs_stab_diag_v39 scs_4I3 i j`
729 THEN ASM_REWRITE_TAC[]
732 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
733 THEN EXISTS_TAC`i:num`
734 THEN EXISTS_TAC`j:num`
735 THEN ASM_REWRITE_TAC[];
738 EXISTS_TAC`v':num->real^3`
739 THEN ASM_REWRITE_TAC[]]);;
742 let SET_STAB_4I3=prove(`{ scs_stab_diag_v39 scs_4I3 i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4I3 (i MOD 4) (j MOD 4)| scs_diag 4 (i MOD 4) (j MOD 4) }`,
743 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
744 THEN MRESAL_TAC STAB_MOD[`scs_4I3`][SCS_4I3_IS_SCS;K_SCS_4I3]);;
746 let EXPAND_STAB_DIAG_4I3=prove(`
747 {scs_stab_diag_v39 scs_4I3 (i MOD 4) (j MOD 4) | j MOD 4 =
748 (i MOD 4 + 2) MOD 4}=
749 {scs_stab_diag_v39 scs_4I3 (i+2) i| i<4} `,
750 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4I3_IS_SCS;K_SCS_4I3]);;
753 let SET_EQ_DIAG_STAB_4I3=prove_by_refinement(
755 { scs_stab_diag_v39 scs_4I3 i j| scs_diag 4 i j }
756 {scs_stab_diag_v39 scs_4I3 0 2,scs_stab_diag_v39 scs_4I3 1 3}`,
758 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4I3;SET_STAB_4I3;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
760 REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4I3 (i + 2) i |i=0\/i=1\/i=2\/i=3}
761 = {scs_stab_diag_v39 scs_4I3 (0 + 2) 0} UNION
762 {scs_stab_diag_v39 scs_4I3 (1 + 2) 1} UNION
763 {scs_stab_diag_v39 scs_4I3 (2 + 2) 2} UNION
764 {scs_stab_diag_v39 scs_4I3 (3 + 2) 3}
766 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4I3 0 2,scs_stab_diag_v39 scs_4I3 1 3}={scs_stab_diag_v39 scs_4I3 0 2} UNION {scs_stab_diag_v39 scs_4I3 1 3}UNION {scs_stab_diag_v39 scs_4I3 0 2} UNION {scs_stab_diag_v39 scs_4I3 1 3}`]
767 THEN MATCH_MP_TAC FZIOTEF_UNION
768 THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
769 THEN MRESA_TAC STAB_SYM[`scs_4I3`;`0`;`2`]
772 MATCH_MP_TAC FZIOTEF_REFL
773 THEN REWRITE_TAC[IN_SING]
775 THEN ASM_SIMP_TAC[STAB_4I3_SCS;SCS_DIAG_SCS_4I3_02];
777 MATCH_MP_TAC FZIOTEF_UNION
778 THEN MRESA_TAC STAB_SYM[`scs_4I3`;`1`;`3`]
782 MATCH_MP_TAC FZIOTEF_REFL
783 THEN REWRITE_TAC[IN_SING]
785 THEN ASM_SIMP_TAC[STAB_4I3_SCS;SCS_DIAG_SCS_4I3_13];
787 MATCH_MP_TAC FZIOTEF_UNION
788 THEN MRESAL_TAC STAB_MOD[`scs_4I3`;`4`;`2`][SCS_4I3_IS_SCS;K_SCS_4I3;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
792 MATCH_MP_TAC FZIOTEF_REFL
793 THEN REWRITE_TAC[IN_SING]
795 THEN ASM_SIMP_TAC[STAB_4I3_SCS;SCS_DIAG_SCS_4I3_02];
797 MRESAL_TAC STAB_MOD[`scs_4I3`;`5`;`3`][SCS_4I3_IS_SCS;K_SCS_4I3;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
800 MATCH_MP_TAC FZIOTEF_REFL
801 THEN REWRITE_TAC[IN_SING]
803 THEN ASM_SIMP_TAC[STAB_4I3_SCS;SCS_DIAG_SCS_4I3_13]]);;
806 let VQFYMZY=prove(` scs_arrow_v39 { scs_4I3 } ({scs_4M6', scs_4T4})`,
808 MATCH_MP_TAC FZIOTEF_TRANS
809 THEN EXISTS_TAC`({scs_4M6'} UNION {scs_stab_diag_v39 scs_4I3 i j| scs_diag 4 i j})`
810 THEN ASM_SIMP_TAC[SCS_4I3_ARROW_SCS_4M6_STAB_4I3;SET_RULE`{a,b}={a}UNION {b}`]
811 THEN MATCH_MP_TAC FZIOTEF_UNION
815 MATCH_MP_TAC FZIOTEF_REFL
816 THEN REWRITE_TAC[IN_SING]
818 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS];
820 MATCH_MP_TAC FZIOTEF_TRANS
821 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4I3 0 2,scs_stab_diag_v39 scs_4I3 1 3}`
822 THEN ASM_SIMP_TAC[SET_EQ_DIAG_STAB_4I3;SET_RULE`{a,b}={a}UNION {b}`]
823 THEN ONCE_REWRITE_TAC[SET_RULE` {scs_4T4}={scs_4T4} UNION {scs_4T4}`]
824 THEN MATCH_MP_TAC FZIOTEF_UNION
825 THEN ASM_SIMP_TAC[ZNLLLDL;SCS_4I3_ARROW_4T4]]);;
829 (***********************)
835 let BB_4M2_IMP_BB_4M6= prove
838 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==>
839 BBs_v39 (scs_4M6') v`,
840 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M2;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M2;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
842 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
844 THEN THAYTHE_TAC 1[`i`;`j`]
846 THEN THAYTHE_TAC 2[`i`;`j`]
849 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
851 THEN REWRITE_TAC[ADD1]
852 THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`]
854 THEN MRESA_TAC MOD_ADD_MOD[`j`;`1`;`4`]
856 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`)
857 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
859 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`)
860 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
863 THEN MP_TAC sqrt8_LE_CSTAB
864 THEN REWRITE_TAC[cstab;h0]
865 THEN REAL_ARITH_TAC);;
870 let MM_4M2_IMP_4M6=prove(
873 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==>
874 ~(MMs_v39 (scs_4M6') ={})`,
876 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
877 THEN EXISTS_TAC`v:num->real^3`
878 THEN EXISTS_TAC` scs_4M2 `
879 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M2 `;`v`]
880 THEN ASSUME_TAC SCS_4M6_BASIC
881 THEN ASSUME_TAC K_SCS_4M6
882 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M2_IS_SCS;SCS_4M2_BASIC;K_SCS_4M2;SCS_K_D_A_STAB_EQ;IN; ADD1;BB_4M2_IMP_BB_4M6]
884 THEN REAL_ARITH_TAC);;
889 let BB_4M2_IMP_BB_STAN_4M2= prove(
893 dist(v i,v j)<= cstab ==>
894 BBs_v39 (scs_stab_diag_v39 scs_4M2 i j) v`,
895 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M2;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M2;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
897 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
899 THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
901 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
903 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M2`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M2;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M2;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M2_IS_SCS]
904 THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
905 THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
907 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M2`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M2;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M2;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M2_IS_SCS]
908 THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
909 THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
910 THEN ONCE_REWRITE_TAC[DIST_SYM]
911 THEN ASM_REWRITE_TAC[]]);;
914 let MM_4M2_IMP_STAB_4M2=prove(`
917 dist(v i,v j)<= cstab ==>
918 ~(MMs_v39 (scs_stab_diag_v39 scs_4M2 i j) ={})`,
920 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
921 THEN EXISTS_TAC`v:num->real^3`
922 THEN EXISTS_TAC` scs_4M2 `
923 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M2 `;`v`]
924 THEN ASSUME_TAC SCS_4M2_BASIC
925 THEN ASSUME_TAC K_SCS_4M2
926 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M2_IS_SCS;SCS_4M2_BASIC;K_SCS_4M2;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M2_13;BB_4M2_IMP_BB_STAN_4M2;STAB_4M2_SCS]
928 THEN REAL_ARITH_TAC);;
932 let SCS_4M2_ARROW_SCS_4M6_STAB_4M2=prove_by_refinement(
933 ` scs_arrow_v39 { scs_4M2 } ({scs_4M6'} UNION {scs_stab_diag_v39 scs_4M2 i j| scs_diag 4 i j})`,
935 REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM]
936 THEN ABBREV_TAC`k=scs_k_v39 s`
937 THEN REPEAT RESA_TAC;
940 ASM_SIMP_TAC[SCS_4M6_IS_SCS];
943 ASM_SIMP_TAC[STAB_4M2_SCS;K_SCS_4M2];
946 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M2 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M2 ==> MMs_v39 s = {}))`);
954 THEN POP_ASSUM MP_TAC
955 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
956 THEN REPEAT STRIP_TAC
957 THEN POP_ASSUM MP_TAC
959 THEN POP_ASSUM MP_TAC
960 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
964 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)))`)
969 THEN ASM_REWRITE_TAC[]
970 THEN MP_TAC MM_4M2_IMP_4M6
971 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
973 THEN MATCH_DICH_TAC 0
974 THEN ASM_REWRITE_TAC[]
975 THEN EXISTS_TAC`v:num->real^3`
976 THEN ASM_REWRITE_TAC[];
980 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
982 THEN MP_TAC MM_4M2_IMP_STAB_4M2
985 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
987 THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M2 i j`
988 THEN ASM_REWRITE_TAC[]
991 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
992 THEN EXISTS_TAC`i:num`
993 THEN EXISTS_TAC`j:num`
994 THEN ASM_REWRITE_TAC[];
997 EXISTS_TAC`v':num->real^3`
998 THEN ASM_REWRITE_TAC[]]);;
1002 let SET_STAB_4M2=prove(`{ scs_stab_diag_v39 scs_4M2 i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M2 (i MOD 4) (j MOD 4)| scs_diag 4 (i MOD 4) (j MOD 4) }`,
1003 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
1004 THEN MRESAL_TAC STAB_MOD[`scs_4M2`][SCS_4M2_IS_SCS;K_SCS_4M2]);;
1006 let EXPAND_STAB_DIAG_4M2=prove(`
1007 {scs_stab_diag_v39 scs_4M2 (i MOD 4) (j MOD 4) | j MOD 4 =
1008 (i MOD 4 + 2) MOD 4}=
1009 {scs_stab_diag_v39 scs_4M2 (i+2) i| i<4} `,
1010 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M2_IS_SCS;K_SCS_4M2]);;
1013 let SET_EQ_DIAG_STAB_4M2=prove_by_refinement(
1015 { scs_stab_diag_v39 scs_4M2 i j| scs_diag 4 i j }
1016 {scs_stab_diag_v39 scs_4M2 0 2,scs_stab_diag_v39 scs_4M2 1 3}`,
1018 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M2;SET_STAB_4M2;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
1020 REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M2 (i + 2) i |i=0\/i=1\/i=2\/i=3}
1021 = {scs_stab_diag_v39 scs_4M2 (0 + 2) 0} UNION
1022 {scs_stab_diag_v39 scs_4M2 (1 + 2) 1} UNION
1023 {scs_stab_diag_v39 scs_4M2 (2 + 2) 2} UNION
1024 {scs_stab_diag_v39 scs_4M2 (3 + 2) 3}
1026 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M2 0 2,scs_stab_diag_v39 scs_4M2 1 3}={scs_stab_diag_v39 scs_4M2 0 2} UNION {scs_stab_diag_v39 scs_4M2 1 3}UNION {scs_stab_diag_v39 scs_4M2 0 2} UNION {scs_stab_diag_v39 scs_4M2 1 3}`]
1027 THEN MATCH_MP_TAC FZIOTEF_UNION
1028 THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
1029 THEN MRESA_TAC STAB_SYM[`scs_4M2`;`0`;`2`]
1032 MATCH_MP_TAC FZIOTEF_REFL
1033 THEN REWRITE_TAC[IN_SING]
1034 THEN REPEAT RESA_TAC
1035 THEN ASM_SIMP_TAC[STAB_4M2_SCS;SCS_DIAG_SCS_4M2_02];
1037 MATCH_MP_TAC FZIOTEF_UNION
1038 THEN MRESA_TAC STAB_SYM[`scs_4M2`;`1`;`3`]
1042 MATCH_MP_TAC FZIOTEF_REFL
1043 THEN REWRITE_TAC[IN_SING]
1044 THEN REPEAT RESA_TAC
1045 THEN ASM_SIMP_TAC[STAB_4M2_SCS;SCS_DIAG_SCS_4M2_13];
1047 MATCH_MP_TAC FZIOTEF_UNION
1048 THEN MRESAL_TAC STAB_MOD[`scs_4M2`;`4`;`2`][SCS_4M2_IS_SCS;K_SCS_4M2;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
1052 MATCH_MP_TAC FZIOTEF_REFL
1053 THEN REWRITE_TAC[IN_SING]
1054 THEN REPEAT RESA_TAC
1055 THEN ASM_SIMP_TAC[STAB_4M2_SCS;SCS_DIAG_SCS_4M2_02];
1057 MRESAL_TAC STAB_MOD[`scs_4M2`;`5`;`3`][SCS_4M2_IS_SCS;K_SCS_4M2;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
1060 MATCH_MP_TAC FZIOTEF_REFL
1061 THEN REWRITE_TAC[IN_SING]
1062 THEN REPEAT RESA_TAC
1063 THEN ASM_SIMP_TAC[STAB_4M2_SCS;SCS_DIAG_SCS_4M2_13]]);;
1067 let PROP_OPP_DIAG_4M2_13= prove_by_refinement(`scs_stab_diag_v39 scs_4M2 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4M2 0 2)) 2 `,
1068 [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]
1069 THEN MATCH_MP_TAC scs_inj
1070 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M2_BASIC;STAB_4M2_SCS;SCS_DIAG_SCS_4M2_13;scs_basic;unadorned_v39;peropp;peropp2]
1078 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;]
1079 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
1081 THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
1082 THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
1084 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
1085 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
1088 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`)
1089 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
1091 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`)
1092 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
1094 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
1095 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;
1098 let STAB_4M2_02_ARROW_4M2_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M2 0 2}{scs_stab_diag_v39 scs_4M2 1 3}`,
1099 ASM_SIMP_TAC[PROP_OPP_DIAG_4M2_13]
1100 THEN MATCH_MP_TAC FZIOTEF_TRANS
1101 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4M2 0 2)}`
1104 MATCH_MP_TAC (GEN_ALL YXIONXL2)
1106 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M2;STAB_4M2_SCS;SCS_DIAG_SCS_4M2_02]
1109 MATCH_MP_TAC(GEN_ALL YXIONXL3)
1110 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
1111 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4M2 0 2)`
1112 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M2;STAB_4M2_SCS;SCS_DIAG_SCS_4M2_02]]);;
1115 let SCS_4M2_SLICE_13=prove_by_refinement(
1116 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M2 1 3 } {scs_prop_equ_v39 scs_3M1 1, scs_3T4 }`,
1118 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
1119 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M2_13;STAB_4M2_SCS;SCS_K_D_A_STAB_EQ;]
1122 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M2_13]
1123 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
1124 THEN REPEAT RESA_TAC;
1126 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
1128 THEN MATCH_MP_TAC scs_inj
1129 THEN ASM_SIMP_TAC[SCS_3T4_BASIC;SCS_4M2_BASIC;J_SCS_4M2;BASIC_HALF_SLICE_STAB;J_SCS_3T4;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3M1_BASIC;J_SCS_3M1]
1133 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2]
1138 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2;
1139 ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
1140 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1141 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1144 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1145 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1147 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1148 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1150 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1151 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]
1152 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
1153 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
1154 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
1155 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
1156 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
1157 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
1159 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/\
1160 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1161 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1162 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1163 THEN REPEAT RESA_TAC
1164 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)
1165 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1166 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1167 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1168 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1169 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1173 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2]
1178 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2;scs_3T4_prime;scs_5M3;
1179 ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
1180 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1181 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1184 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1185 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1187 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1188 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1190 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1191 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]
1192 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
1193 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
1194 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
1195 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
1196 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
1197 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
1199 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/\
1200 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1201 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1202 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1203 THEN REPEAT RESA_TAC
1204 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)
1205 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1206 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1207 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1208 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1209 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1214 THEN REAL_ARITH_TAC;
1217 THEN REAL_ARITH_TAC;
1220 THEN REAL_ARITH_TAC;
1223 THEN REWRITE_TAC[cstab]
1224 THEN REAL_ARITH_TAC;
1228 THEN REWRITE_TAC[cstab]
1229 THEN REAL_ARITH_TAC;
1234 THEN REWRITE_TAC[J_SCS_3M1];
1238 let BNAWVNH =prove_by_refinement(` scs_arrow_v39 { scs_4M2 } ({scs_4M6',scs_3M1, scs_3T4})`,
1240 MATCH_MP_TAC FZIOTEF_TRANS
1241 THEN EXISTS_TAC`({scs_4M6'} UNION {scs_stab_diag_v39 scs_4M2 i j| scs_diag 4 i j})`
1242 THEN ASM_REWRITE_TAC[SCS_4M2_ARROW_SCS_4M6_STAB_4M2;SET_RULE`{A,B,C}={A}UNION{B,C}`]
1243 THEN MATCH_MP_TAC FZIOTEF_UNION
1246 MATCH_MP_TAC FZIOTEF_REFL
1247 THEN REWRITE_TAC[IN_SING]
1248 THEN REPEAT RESA_TAC
1249 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS];
1251 MATCH_MP_TAC FZIOTEF_TRANS
1252 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M2 0 2,scs_stab_diag_v39 scs_4M2 1 3}`
1253 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M2]
1254 THEN MATCH_MP_TAC FZIOTEF_TRANS
1255 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M2 1 3,scs_stab_diag_v39 scs_4M2 1 3}`
1258 REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`]
1259 THEN MATCH_MP_TAC FZIOTEF_UNION
1260 THEN ASM_REWRITE_TAC[STAB_4M2_02_ARROW_4M2_13];
1262 MATCH_MP_TAC FZIOTEF_REFL
1263 THEN REWRITE_TAC[IN_SING]
1264 THEN REPEAT RESA_TAC
1265 THEN ASM_SIMP_TAC[STAB_4M2_SCS;SCS_DIAG_SCS_4M2_13];
1267 REWRITE_TAC[SET_RULE`{A,A}={A}`]
1268 THEN MATCH_MP_TAC FZIOTEF_TRANS
1269 THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3M1 1, scs_3T4 }`
1270 THEN ASM_REWRITE_TAC[SCS_4M2_SLICE_13;SET_RULE`{A,B}={A}UNION {B}`]
1271 THEN MATCH_MP_TAC FZIOTEF_UNION
1274 MRESAS_TAC PRO_EQU_ID1[`scs_3M1`;`1`;`3`][SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`(3 - 1 MOD 3)=2`]
1275 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1 1`;`2`][PROP_EQU_IS_SCS;SCS_3M1_IS_SCS]
1277 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1280 MATCH_MP_TAC FZIOTEF_REFL
1281 THEN REWRITE_TAC[IN_SING]
1282 THEN REPEAT RESA_TAC
1283 THEN ASM_SIMP_TAC[SCS_3T4_IS_SCS]]);;
1287 (***************************)
1290 let BB_4M3_IMP_BB_4M6= prove
1292 BBs_v39 scs_4M3' v /\
1293 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==>
1294 BBs_v39 (scs_4M6') v`,
1295 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
1296 THEN REPEAT RESA_TAC
1297 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
1299 THEN THAYTHE_TAC 1[`i`;`j`]
1301 THEN THAYTHE_TAC 2[`i`;`j`]
1304 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
1306 THEN REWRITE_TAC[ADD1]
1307 THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`]
1309 THEN MRESA_TAC MOD_ADD_MOD[`j`;`1`;`4`]
1311 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`)
1312 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
1314 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`)
1315 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
1318 THEN MP_TAC sqrt8_LE_CSTAB
1319 THEN MP_TAC LE_sqrt8_2h0
1320 THEN REWRITE_TAC[cstab;h0]
1321 THEN REAL_ARITH_TAC);;
1326 let MM_4M3_IMP_4M6=prove(
1328 MMs_v39 scs_4M3' v /\
1329 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==>
1330 ~(MMs_v39 (scs_4M6') ={})`,
1332 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
1333 THEN EXISTS_TAC`v:num->real^3`
1334 THEN EXISTS_TAC` scs_4M3' `
1335 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M3' `;`v`]
1336 THEN ASSUME_TAC SCS_4M6_BASIC
1337 THEN ASSUME_TAC K_SCS_4M6
1338 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M3_IS_SCS;SCS_4M3_BASIC;K_SCS_4M3;SCS_K_D_A_STAB_EQ;IN; ADD1;BB_4M3_IMP_BB_4M6]
1340 THEN REAL_ARITH_TAC);;
1345 let BB_4M3_IMP_BB_STAN_4M3= prove(
1347 BBs_v39 scs_4M3' v /\
1349 dist(v i,v j)<= cstab ==>
1350 BBs_v39 (scs_stab_diag_v39 scs_4M3' i j) v`,
1351 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
1352 THEN REPEAT RESA_TAC
1353 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
1355 THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
1357 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
1359 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M3'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M3_IS_SCS]
1360 THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
1361 THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
1363 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M3'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M3;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M3;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M3_IS_SCS]
1364 THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
1365 THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
1366 THEN ONCE_REWRITE_TAC[DIST_SYM]
1367 THEN ASM_REWRITE_TAC[]]);;
1372 let MM_4M3_IMP_STAB_4M3=prove(`
1373 MMs_v39 scs_4M3' v /\
1375 dist(v i,v j)<= cstab ==>
1376 ~(MMs_v39 (scs_stab_diag_v39 scs_4M3' i j) ={})`,
1378 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
1379 THEN EXISTS_TAC`v:num->real^3`
1380 THEN EXISTS_TAC` scs_4M3' `
1381 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M3' `;`v`]
1382 THEN ASSUME_TAC SCS_4M3_BASIC
1383 THEN ASSUME_TAC K_SCS_4M3
1384 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M3_IS_SCS;SCS_4M3_BASIC;K_SCS_4M3;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M3_13;BB_4M3_IMP_BB_STAN_4M3;STAB_4M3_SCS]
1386 THEN REAL_ARITH_TAC);;
1391 let SCS_4M3_ARROW_SCS_4M6_STAB_4M3=prove_by_refinement(
1392 ` scs_arrow_v39 { scs_4M3' } ({scs_4M6'} UNION {scs_stab_diag_v39 scs_4M3' i j| scs_diag 4 i j})`,
1394 REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM]
1395 THEN ABBREV_TAC`k=scs_k_v39 s`
1396 THEN REPEAT RESA_TAC;
1399 ASM_SIMP_TAC[SCS_4M6_IS_SCS];
1402 ASM_SIMP_TAC[STAB_4M3_SCS;K_SCS_4M3];
1405 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M3' ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M3' ==> MMs_v39 s = {}))`);
1413 THEN POP_ASSUM MP_TAC
1414 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
1415 THEN REPEAT STRIP_TAC
1416 THEN POP_ASSUM MP_TAC
1418 THEN POP_ASSUM MP_TAC
1419 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1423 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)))`)
1427 EXISTS_TAC`scs_4M6'`
1428 THEN ASM_REWRITE_TAC[]
1429 THEN MP_TAC MM_4M3_IMP_4M6
1430 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1432 THEN MATCH_DICH_TAC 0
1433 THEN ASM_REWRITE_TAC[]
1434 THEN EXISTS_TAC`v:num->real^3`
1435 THEN ASM_REWRITE_TAC[];
1439 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
1441 THEN MP_TAC MM_4M3_IMP_STAB_4M3
1444 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1446 THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M3' i j`
1447 THEN ASM_REWRITE_TAC[]
1450 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
1451 THEN EXISTS_TAC`i:num`
1452 THEN EXISTS_TAC`j:num`
1453 THEN ASM_REWRITE_TAC[];
1456 EXISTS_TAC`v':num->real^3`
1457 THEN ASM_REWRITE_TAC[]]);;
1462 let SET_STAB_4M3=prove(`{ scs_stab_diag_v39 scs_4M3' i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M3' (i MOD 4) (j MOD 4)| scs_diag 4 (i MOD 4) (j MOD 4) }`,
1463 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
1464 THEN MRESAL_TAC STAB_MOD[`scs_4M3'`][SCS_4M3_IS_SCS;K_SCS_4M3]);;
1466 let EXPAND_STAB_DIAG_4M3=prove(`
1467 {scs_stab_diag_v39 scs_4M3' (i MOD 4) (j MOD 4) | j MOD 4 =
1468 (i MOD 4 + 2) MOD 4}=
1469 {scs_stab_diag_v39 scs_4M3' (i+2) i| i<4} `,
1470 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M3_IS_SCS;K_SCS_4M3]);;
1473 let SET_EQ_DIAG_STAB_4M3=prove_by_refinement(
1475 { scs_stab_diag_v39 scs_4M3' i j| scs_diag 4 i j }
1476 {scs_stab_diag_v39 scs_4M3' 0 2,scs_stab_diag_v39 scs_4M3' 1 3}`,
1478 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M3;SET_STAB_4M3;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
1480 REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M3' (i + 2) i |i=0\/i=1\/i=2\/i=3}
1481 = {scs_stab_diag_v39 scs_4M3' (0 + 2) 0} UNION
1482 {scs_stab_diag_v39 scs_4M3' (1 + 2) 1} UNION
1483 {scs_stab_diag_v39 scs_4M3' (2 + 2) 2} UNION
1484 {scs_stab_diag_v39 scs_4M3' (3 + 2) 3}
1486 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M3' 0 2,scs_stab_diag_v39 scs_4M3' 1 3}={scs_stab_diag_v39 scs_4M3' 0 2} UNION {scs_stab_diag_v39 scs_4M3' 1 3}UNION {scs_stab_diag_v39 scs_4M3' 0 2} UNION {scs_stab_diag_v39 scs_4M3' 1 3}`]
1487 THEN MATCH_MP_TAC FZIOTEF_UNION
1488 THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
1489 THEN MRESA_TAC STAB_SYM[`scs_4M3'`;`0`;`2`]
1492 MATCH_MP_TAC FZIOTEF_REFL
1493 THEN REWRITE_TAC[IN_SING]
1494 THEN REPEAT RESA_TAC
1495 THEN ASM_SIMP_TAC[STAB_4M3_SCS;SCS_DIAG_SCS_4M3_02];
1497 MATCH_MP_TAC FZIOTEF_UNION
1498 THEN MRESA_TAC STAB_SYM[`scs_4M3'`;`1`;`3`]
1502 MATCH_MP_TAC FZIOTEF_REFL
1503 THEN REWRITE_TAC[IN_SING]
1504 THEN REPEAT RESA_TAC
1505 THEN ASM_SIMP_TAC[STAB_4M3_SCS;SCS_DIAG_SCS_4M3_13];
1507 MATCH_MP_TAC FZIOTEF_UNION
1508 THEN MRESAL_TAC STAB_MOD[`scs_4M3'`;`4`;`2`][SCS_4M3_IS_SCS;K_SCS_4M3;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
1512 MATCH_MP_TAC FZIOTEF_REFL
1513 THEN REWRITE_TAC[IN_SING]
1514 THEN REPEAT RESA_TAC
1515 THEN ASM_SIMP_TAC[STAB_4M3_SCS;SCS_DIAG_SCS_4M3_02];
1517 MRESAL_TAC STAB_MOD[`scs_4M3'`;`5`;`3`][SCS_4M3_IS_SCS;K_SCS_4M3;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
1520 MATCH_MP_TAC FZIOTEF_REFL
1521 THEN REWRITE_TAC[IN_SING]
1522 THEN REPEAT RESA_TAC
1523 THEN ASM_SIMP_TAC[STAB_4M3_SCS;SCS_DIAG_SCS_4M3_13]]);;
1525 let PROP_OPP_DIAG_4M3_13= prove_by_refinement(`scs_stab_diag_v39 scs_4M3' 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4M3' 0 2)) 2 `,
1526 [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]
1527 THEN MATCH_MP_TAC scs_inj
1528 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M3_BASIC;STAB_4M3_SCS;SCS_DIAG_SCS_4M3_13;scs_basic;unadorned_v39;peropp;peropp2]
1536 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;]
1537 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
1539 THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
1540 THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
1542 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
1543 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
1546 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`)
1547 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
1549 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`)
1550 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
1552 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
1553 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;
1556 let STAB_4M3_02_ARROW_4M3_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M3' 0 2}{scs_stab_diag_v39 scs_4M3' 1 3}`,
1557 ASM_SIMP_TAC[PROP_OPP_DIAG_4M3_13]
1558 THEN MATCH_MP_TAC FZIOTEF_TRANS
1559 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4M3' 0 2)}`
1562 MATCH_MP_TAC (GEN_ALL YXIONXL2)
1564 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M3;STAB_4M3_SCS;SCS_DIAG_SCS_4M3_02]
1567 MATCH_MP_TAC(GEN_ALL YXIONXL3)
1568 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
1569 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4M3' 0 2)`
1570 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M3;STAB_4M3_SCS;SCS_DIAG_SCS_4M3_02]]);;
1573 let SCS_4M3_SLICE_13=prove_by_refinement(
1574 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M3' 1 3 } {scs_prop_equ_v39 scs_3T1 1, scs_prop_equ_v39 scs_3T6' 2}`,
1575 [MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
1576 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M3_13;STAB_4M3_SCS;SCS_K_D_A_STAB_EQ;]
1579 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M3_13]
1580 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
1581 THEN REPEAT RESA_TAC;
1584 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
1586 THEN MATCH_MP_TAC scs_inj
1587 THEN ASM_SIMP_TAC[SCS_3T1_BASIC;SCS_4M3_BASIC;J_SCS_4M3;BASIC_HALF_SLICE_STAB;J_SCS_3T1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T6_BASIC;J_SCS_3T6]
1591 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_3T1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M3]
1596 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_3T1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M3;
1597 ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
1598 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1599 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1602 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1603 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1605 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1606 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1608 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1609 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]
1610 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
1611 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
1612 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
1613 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
1614 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
1615 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
1617 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/\
1618 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1619 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1620 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1621 THEN REPEAT RESA_TAC
1622 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)
1623 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1624 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1625 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1626 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1627 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1631 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_3T6;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M3]
1637 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_3T6;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M3;
1638 ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
1639 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1640 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
1643 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
1644 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
1646 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
1647 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
1649 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1650 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]
1651 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
1652 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
1653 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
1654 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
1655 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
1656 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
1658 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/\
1659 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1660 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
1661 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
1662 THEN REPEAT RESA_TAC
1663 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)
1664 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
1665 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
1666 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
1667 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
1668 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
1673 THEN REAL_ARITH_TAC;
1676 THEN REAL_ARITH_TAC;
1679 THEN REAL_ARITH_TAC;
1682 THEN REWRITE_TAC[cstab]
1683 THEN REAL_ARITH_TAC;
1687 THEN REWRITE_TAC[cstab]
1688 THEN REAL_ARITH_TAC;
1693 THEN REWRITE_TAC[J_SCS_3T1];
1699 let RAWZDIB =prove_by_refinement(
1700 ` scs_arrow_v39 { scs_4M3' } ({scs_4M6',scs_3T1, scs_3T6'})`,
1702 MATCH_MP_TAC FZIOTEF_TRANS
1703 THEN EXISTS_TAC`({scs_4M6'} UNION {scs_stab_diag_v39 scs_4M3' i j| scs_diag 4 i j})`
1704 THEN ASM_REWRITE_TAC[SCS_4M3_ARROW_SCS_4M6_STAB_4M3;SET_RULE`{A,B,C}={A}UNION{B,C}`]
1705 THEN MATCH_MP_TAC FZIOTEF_UNION
1709 MATCH_MP_TAC FZIOTEF_REFL
1710 THEN REWRITE_TAC[IN_SING]
1711 THEN REPEAT RESA_TAC
1712 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS];
1714 MATCH_MP_TAC FZIOTEF_TRANS
1715 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M3' 0 2,scs_stab_diag_v39 scs_4M3' 1 3}`
1716 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M3]
1717 THEN MATCH_MP_TAC FZIOTEF_TRANS
1718 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M3' 1 3,scs_stab_diag_v39 scs_4M3' 1 3}`
1721 REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`]
1722 THEN MATCH_MP_TAC FZIOTEF_UNION
1723 THEN ASM_REWRITE_TAC[STAB_4M3_02_ARROW_4M3_13];
1725 MATCH_MP_TAC FZIOTEF_REFL
1726 THEN REWRITE_TAC[IN_SING]
1727 THEN REPEAT RESA_TAC
1728 THEN ASM_SIMP_TAC[STAB_4M3_SCS;SCS_DIAG_SCS_4M3_13];
1730 REWRITE_TAC[SET_RULE`{A,A}={A}`]
1731 THEN MATCH_MP_TAC FZIOTEF_TRANS
1732 THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3T1 1, scs_prop_equ_v39 scs_3T6' 2}`
1733 THEN ASM_REWRITE_TAC[SCS_4M3_SLICE_13;SET_RULE`{A,B}={A}UNION {B}`]
1734 THEN MATCH_MP_TAC FZIOTEF_UNION
1737 MRESAS_TAC PRO_EQU_ID1[`scs_3T1`;`1`;`3`][SCS_3T1_IS_SCS;K_SCS_3T1;ARITH_RULE`(3 - 1 MOD 3)=2`]
1738 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T1 1`;`2`][PROP_EQU_IS_SCS;SCS_3T1_IS_SCS]
1740 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1743 MRESAS_TAC PRO_EQU_ID1[`scs_3T6'`;`2`;`3`][SCS_3T6_IS_SCS;K_SCS_3T6;ARITH_RULE`(3 - 2 MOD 3)=1`]
1744 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T6' 2`;`1`][PROP_EQU_IS_SCS;SCS_3T6_IS_SCS]
1746 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1747 THEN REWRITE_TAC[]]);;
1750 (************************************)
1752 let BB_4M4_IMP_BB_4M7= prove
1754 BBs_v39 scs_4M4' v /\
1755 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==>
1756 BBs_v39 (scs_4M7) v`,
1757 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M4;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M4;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7]
1758 THEN REPEAT RESA_TAC
1759 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
1761 THEN THAYTHE_TAC 1[`i`;`j`]
1763 THEN THAYTHE_TAC 2[`i`;`j`]
1766 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
1768 THEN REWRITE_TAC[ADD1]
1769 THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`]
1771 THEN MRESA_TAC MOD_ADD_MOD[`j`;`1`;`4`]
1773 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`)
1774 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
1776 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`)
1777 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
1780 THEN MP_TAC sqrt8_LE_CSTAB
1781 THEN MP_TAC LE_sqrt8_2h0
1782 THEN REWRITE_TAC[cstab;h0]
1783 THEN REAL_ARITH_TAC);;
1786 let MM_4M4_IMP_4M7=prove(
1788 MMs_v39 scs_4M4' v /\
1789 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==>
1790 ~(MMs_v39 (scs_4M7) ={})`,
1792 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
1793 THEN EXISTS_TAC`v:num->real^3`
1794 THEN EXISTS_TAC` scs_4M4' `
1795 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M4' `;`v`]
1796 THEN ASSUME_TAC SCS_4M7_BASIC
1797 THEN ASSUME_TAC K_SCS_4M7
1798 THEN ASM_SIMP_TAC[SCS_4M7_IS_SCS;SCS_4M4_IS_SCS;SCS_4M4_BASIC;K_SCS_4M4;SCS_K_D_A_STAB_EQ;IN; ADD1;BB_4M4_IMP_BB_4M7]
1800 THEN REAL_ARITH_TAC);;
1804 let BB_4M4_IMP_BB_STAN_4M4= prove(
1806 BBs_v39 scs_4M4' v /\
1808 dist(v i,v j)<= cstab ==>
1809 BBs_v39 (scs_stab_diag_v39 scs_4M4' i j) v`,
1810 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M4;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M4;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7]
1811 THEN REPEAT RESA_TAC
1812 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
1814 THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
1816 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
1818 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M4'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M4;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M4;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7;SCS_4M4_IS_SCS]
1819 THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
1820 THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
1822 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M4'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M4;scs_4M7;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M4;Terminal.FUNLIST_EXPLICIT;K_SCS_4M7;SCS_4M4_IS_SCS]
1823 THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
1824 THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
1825 THEN ONCE_REWRITE_TAC[DIST_SYM]
1826 THEN ASM_REWRITE_TAC[]]);;
1830 let MM_4M4_IMP_STAB_4M4=prove(`
1831 MMs_v39 scs_4M4' v /\
1833 dist(v i,v j)<= cstab ==>
1834 ~(MMs_v39 (scs_stab_diag_v39 scs_4M4' i j) ={})`,
1836 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
1837 THEN EXISTS_TAC`v:num->real^3`
1838 THEN EXISTS_TAC` scs_4M4' `
1839 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M4' `;`v`]
1840 THEN ASSUME_TAC SCS_4M4_BASIC
1841 THEN ASSUME_TAC K_SCS_4M4
1842 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M4_IS_SCS;SCS_4M4_BASIC;K_SCS_4M4;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M4_13;BB_4M4_IMP_BB_STAN_4M4;STAB_4M4_SCS]
1844 THEN REAL_ARITH_TAC);;
1848 let SCS_4M4_ARROW_SCS_4M7_STAB_4M4=prove_by_refinement(
1849 ` scs_arrow_v39 { scs_4M4' } ({scs_4M7} UNION {scs_stab_diag_v39 scs_4M4' i j| scs_diag 4 i j})`,
1851 REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM]
1852 THEN ABBREV_TAC`k=scs_k_v39 s`
1853 THEN REPEAT RESA_TAC;
1856 ASM_SIMP_TAC[SCS_4M7_IS_SCS];
1859 ASM_SIMP_TAC[STAB_4M4_SCS;K_SCS_4M4];
1862 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M4' ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M4' ==> MMs_v39 s = {}))`);
1870 THEN POP_ASSUM MP_TAC
1871 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
1872 THEN REPEAT STRIP_TAC
1873 THEN POP_ASSUM MP_TAC
1875 THEN POP_ASSUM MP_TAC
1876 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1880 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)))`)
1885 THEN ASM_REWRITE_TAC[]
1886 THEN MP_TAC MM_4M4_IMP_4M7
1887 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1889 THEN MATCH_DICH_TAC 0
1890 THEN ASM_REWRITE_TAC[]
1891 THEN EXISTS_TAC`v:num->real^3`
1892 THEN ASM_REWRITE_TAC[];
1896 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
1898 THEN MP_TAC MM_4M4_IMP_STAB_4M4
1901 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
1903 THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M4' i j`
1904 THEN ASM_REWRITE_TAC[]
1907 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
1908 THEN EXISTS_TAC`i:num`
1909 THEN EXISTS_TAC`j:num`
1910 THEN ASM_REWRITE_TAC[];
1913 EXISTS_TAC`v':num->real^3`
1914 THEN ASM_REWRITE_TAC[]]);;
1919 let SET_STAB_4M4=prove(`{ scs_stab_diag_v39 scs_4M4' i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M4' (i MOD 4) (j MOD 4)| scs_diag 4 (i MOD 4) (j MOD 4) }`,
1920 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
1921 THEN MRESAL_TAC STAB_MOD[`scs_4M4'`][SCS_4M4_IS_SCS;K_SCS_4M4]);;
1923 let EXPAND_STAB_DIAG_4M4=prove(`
1924 {scs_stab_diag_v39 scs_4M4' (i MOD 4) (j MOD 4) | j MOD 4 =
1925 (i MOD 4 + 2) MOD 4}=
1926 {scs_stab_diag_v39 scs_4M4' (i+2) i| i<4} `,
1927 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M4_IS_SCS;K_SCS_4M4]);;
1930 let SET_EQ_DIAG_STAB_4M4=prove_by_refinement(
1932 { scs_stab_diag_v39 scs_4M4' i j| scs_diag 4 i j }
1933 {scs_stab_diag_v39 scs_4M4' 0 2,scs_stab_diag_v39 scs_4M4' 1 3}`,
1935 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M4;SET_STAB_4M4;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
1937 REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M4' (i + 2) i |i=0\/i=1\/i=2\/i=3}
1938 = {scs_stab_diag_v39 scs_4M4' (0 + 2) 0} UNION
1939 {scs_stab_diag_v39 scs_4M4' (1 + 2) 1} UNION
1940 {scs_stab_diag_v39 scs_4M4' (2 + 2) 2} UNION
1941 {scs_stab_diag_v39 scs_4M4' (3 + 2) 3}
1943 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M4' 0 2,scs_stab_diag_v39 scs_4M4' 1 3}={scs_stab_diag_v39 scs_4M4' 0 2} UNION {scs_stab_diag_v39 scs_4M4' 1 3}UNION {scs_stab_diag_v39 scs_4M4' 0 2} UNION {scs_stab_diag_v39 scs_4M4' 1 3}`]
1944 THEN MATCH_MP_TAC FZIOTEF_UNION
1945 THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
1946 THEN MRESA_TAC STAB_SYM[`scs_4M4'`;`0`;`2`]
1949 MATCH_MP_TAC FZIOTEF_REFL
1950 THEN REWRITE_TAC[IN_SING]
1951 THEN REPEAT RESA_TAC
1952 THEN ASM_SIMP_TAC[STAB_4M4_SCS;SCS_DIAG_SCS_4M4_02];
1954 MATCH_MP_TAC FZIOTEF_UNION
1955 THEN MRESA_TAC STAB_SYM[`scs_4M4'`;`1`;`3`]
1959 MATCH_MP_TAC FZIOTEF_REFL
1960 THEN REWRITE_TAC[IN_SING]
1961 THEN REPEAT RESA_TAC
1962 THEN ASM_SIMP_TAC[STAB_4M4_SCS;SCS_DIAG_SCS_4M4_13];
1964 MATCH_MP_TAC FZIOTEF_UNION
1965 THEN MRESAL_TAC STAB_MOD[`scs_4M4'`;`4`;`2`][SCS_4M4_IS_SCS;K_SCS_4M4;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
1969 MATCH_MP_TAC FZIOTEF_REFL
1970 THEN REWRITE_TAC[IN_SING]
1971 THEN REPEAT RESA_TAC
1972 THEN ASM_SIMP_TAC[STAB_4M4_SCS;SCS_DIAG_SCS_4M4_02];
1974 MRESAL_TAC STAB_MOD[`scs_4M4'`;`5`;`3`][SCS_4M4_IS_SCS;K_SCS_4M4;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
1977 MATCH_MP_TAC FZIOTEF_REFL
1978 THEN REWRITE_TAC[IN_SING]
1979 THEN REPEAT RESA_TAC
1980 THEN ASM_SIMP_TAC[STAB_4M4_SCS;SCS_DIAG_SCS_4M4_13]]);;
1982 let SCS_4M4_SLICE_13=prove_by_refinement(
1983 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M4' 1 3 } {scs_prop_equ_v39 scs_3T4 2, scs_3T4 }`,
1985 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
1986 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M4_13;STAB_4M4_SCS;SCS_K_D_A_STAB_EQ;]
1989 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M4_13]
1990 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
1991 THEN REPEAT RESA_TAC;
1994 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
1996 THEN MATCH_MP_TAC scs_inj
1997 THEN ASM_SIMP_TAC[SCS_3T4_BASIC;SCS_4M4_BASIC;J_SCS_4M4;BASIC_HALF_SLICE_STAB;J_SCS_3T4;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T6_BASIC;J_SCS_3T6]
2000 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4]
2005 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4;
2006 ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
2007 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2008 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2011 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
2012 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
2014 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
2015 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
2017 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2018 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]
2019 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
2020 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
2021 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
2022 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
2023 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
2024 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
2026 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/\
2027 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2028 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2029 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2030 THEN REPEAT RESA_TAC
2031 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)
2032 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
2033 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
2034 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
2035 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2036 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
2041 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4]
2047 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4;
2048 ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
2049 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2050 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2053 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
2054 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
2056 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
2057 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
2059 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2060 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]
2061 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
2062 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
2063 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
2064 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
2065 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
2066 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
2068 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/\
2069 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2070 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2071 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2072 THEN REPEAT RESA_TAC
2073 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)
2074 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
2075 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
2076 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
2077 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2078 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
2084 THEN REAL_ARITH_TAC;
2087 THEN REAL_ARITH_TAC;
2090 THEN REAL_ARITH_TAC;
2093 THEN REWRITE_TAC[cstab]
2094 THEN REAL_ARITH_TAC;
2098 THEN REWRITE_TAC[cstab]
2099 THEN REAL_ARITH_TAC;
2104 THEN REWRITE_TAC[J_SCS_3T4];
2109 let SCS_4M4_SLICE_02=prove_by_refinement(
2110 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M4' 0 2 } { scs_3T3, scs_prop_equ_v39 scs_3M1 1 }`,
2112 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
2113 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M4_02;STAB_4M4_SCS;SCS_K_D_A_STAB_EQ;]
2116 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M4_02]
2117 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
2118 THEN REPEAT RESA_TAC;
2121 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
2123 THEN MATCH_MP_TAC scs_inj
2124 THEN ASM_SIMP_TAC[SCS_3T3_BASIC;SCS_4M4_BASIC;J_SCS_4M4;BASIC_HALF_SLICE_STAB;J_SCS_3T3;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3M1_BASIC;J_SCS_3M1;J_SCS_3T3_1]
2127 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4]
2133 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4;
2134 ARITH_RULE`(2 + 1 + 4 - 0) MOD 4= 3/\ 0 MOD 4=0/\ a+0=a`;scs_prop_equ_v39]
2135 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2136 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2139 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
2140 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
2142 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
2143 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
2145 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2146 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]
2147 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
2148 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
2149 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
2150 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
2151 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
2152 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
2154 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/\
2155 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2156 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2157 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2158 THEN REPEAT RESA_TAC
2159 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)
2160 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
2161 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
2162 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
2163 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2164 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
2168 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4]
2173 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4;
2174 ARITH_RULE`(0 + 1 + 4 - 2) MOD 4= 3/\ 2 MOD 4=2/\ a+0=a`;scs_prop_equ_v39]
2175 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2176 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2179 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
2180 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
2182 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
2183 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
2185 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2186 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]
2187 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
2188 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
2189 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
2190 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
2191 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
2192 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
2194 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/\
2195 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2196 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2197 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2198 THEN REPEAT RESA_TAC
2199 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)
2200 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
2201 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
2202 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
2203 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2204 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
2209 THEN REAL_ARITH_TAC;
2212 THEN REAL_ARITH_TAC;
2215 THEN REAL_ARITH_TAC;
2218 THEN REWRITE_TAC[cstab]
2219 THEN REAL_ARITH_TAC;
2223 THEN REWRITE_TAC[cstab]
2224 THEN REAL_ARITH_TAC;
2229 THEN REWRITE_TAC[J_SCS_3T3_1];
2235 let MFKLVDK =prove_by_refinement(
2236 ` scs_arrow_v39 { scs_4M4' } ({scs_4M7,scs_3T3, scs_3M1, scs_3T4})`,
2238 MATCH_MP_TAC FZIOTEF_TRANS
2239 THEN EXISTS_TAC`({scs_4M7} UNION {scs_stab_diag_v39 scs_4M4' i j| scs_diag 4 i j})`
2240 THEN ASM_REWRITE_TAC[SCS_4M4_ARROW_SCS_4M7_STAB_4M4;SET_RULE`{A,B,C,D}={A}UNION{B,C,D}`]
2241 THEN MATCH_MP_TAC FZIOTEF_UNION
2244 MATCH_MP_TAC FZIOTEF_REFL
2245 THEN REWRITE_TAC[IN_SING]
2246 THEN REPEAT RESA_TAC
2247 THEN ASM_SIMP_TAC[SCS_4M7_IS_SCS];
2249 MATCH_MP_TAC FZIOTEF_TRANS
2250 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M4' 0 2,scs_stab_diag_v39 scs_4M4' 1 3}`
2251 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M4;SET_RULE`{A,B}={A} UNION {B}/\ {A,B,C}={A,B}UNION {C}`]
2252 THEN MATCH_MP_TAC FZIOTEF_UNION
2255 REWRITE_TAC[SET_RULE`{A}UNION {B}={A,B}`]
2256 THEN MATCH_MP_TAC FZIOTEF_TRANS
2257 THEN EXISTS_TAC`{scs_3T3, scs_prop_equ_v39 scs_3M1 1}`
2258 THEN ASM_SIMP_TAC[SCS_4M4_SLICE_02]
2259 THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION {B}`]
2260 THEN MATCH_MP_TAC FZIOTEF_UNION
2263 MATCH_MP_TAC FZIOTEF_REFL
2264 THEN REWRITE_TAC[IN_SING]
2265 THEN REPEAT RESA_TAC
2266 THEN ASM_SIMP_TAC[SCS_3T3_IS_SCS];
2269 MRESAS_TAC PRO_EQU_ID1[`scs_3M1`;`1`;`3`][SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`(3 - 1 MOD 3)=2`]
2270 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1 1`;`2`][PROP_EQU_IS_SCS;SCS_3M1_IS_SCS]
2272 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
2277 MATCH_MP_TAC FZIOTEF_TRANS
2278 THEN EXISTS_TAC`{scs_prop_equ_v39 scs_3T4 2, scs_3T4 }`
2279 THEN ASM_SIMP_TAC[SCS_4M4_SLICE_13;]
2280 THEN ONCE_REWRITE_TAC[SET_RULE`{A}={A}UNION {A}/\ {A,B}={A} UNION {B}`]
2281 THEN MATCH_MP_TAC FZIOTEF_UNION
2285 MRESAS_TAC PRO_EQU_ID1[`scs_3T4`;`2`;`3`][SCS_3T4_IS_SCS;K_SCS_3T4;ARITH_RULE`(3 - 2 MOD 3)=1`]
2286 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T4 2`;`1`][PROP_EQU_IS_SCS;SCS_3T4_IS_SCS]
2288 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
2292 MATCH_MP_TAC FZIOTEF_REFL
2293 THEN REWRITE_TAC[IN_SING]
2294 THEN REPEAT RESA_TAC
2295 THEN ASM_SIMP_TAC[SCS_3T4_IS_SCS]]);;
2299 (************************************)
2302 let BB_4M5_IMP_BB_4M8= prove
2304 BBs_v39 scs_4M5' v /\
2305 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==>
2306 BBs_v39 (scs_4M8) v`,
2307 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M5;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M5;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8]
2308 THEN REPEAT RESA_TAC
2309 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2311 THEN THAYTHE_TAC 1[`i`;`j`]
2313 THEN THAYTHE_TAC 2[`i`;`j`]
2316 THEN MRESA_TAC PSORT_MOD[`4`;`i`;`j`]
2318 THEN REWRITE_TAC[ADD1]
2319 THEN MRESA_TAC MOD_ADD_MOD[`i`;`1`;`4`]
2321 THEN MRESA_TAC MOD_ADD_MOD[`j`;`1`;`4`]
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 MP_TAC sqrt8_LE_CSTAB
2331 THEN MP_TAC LE_sqrt8_2h0
2332 THEN REWRITE_TAC[cstab;h0]
2333 THEN REAL_ARITH_TAC);;
2337 let MM_4M5_IMP_4M8=prove(
2339 MMs_v39 scs_4M5' v /\
2340 (!i j. scs_diag 4 i j ==> cstab < dist(v i,v j)) ==>
2341 ~(MMs_v39 (scs_4M8) ={})`,
2343 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2344 THEN EXISTS_TAC`v:num->real^3`
2345 THEN EXISTS_TAC` scs_4M5' `
2346 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M5' `;`v`]
2347 THEN ASSUME_TAC SCS_4M8_BASIC
2348 THEN ASSUME_TAC K_SCS_4M8
2349 THEN ASM_SIMP_TAC[SCS_4M8_IS_SCS;SCS_4M5_IS_SCS;SCS_4M5_BASIC;K_SCS_4M5;SCS_K_D_A_STAB_EQ;IN; ADD1;BB_4M5_IMP_BB_4M8]
2351 THEN REAL_ARITH_TAC);;
2355 let BB_4M5_IMP_BB_STAN_4M5= prove(
2357 BBs_v39 scs_4M5' v /\
2359 dist(v i,v j)<= cstab ==>
2360 BBs_v39 (scs_stab_diag_v39 scs_4M5' i j) v`,
2361 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M5;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M5;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8]
2362 THEN REPEAT RESA_TAC
2363 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2365 THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
2367 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
2369 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M5'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M5;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M5;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8;SCS_4M5_IS_SCS]
2370 THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
2371 THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
2373 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M5'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M5;scs_4M8;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M5;Terminal.FUNLIST_EXPLICIT;K_SCS_4M8;SCS_4M5_IS_SCS]
2374 THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
2375 THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
2376 THEN ONCE_REWRITE_TAC[DIST_SYM]
2377 THEN ASM_REWRITE_TAC[]]);;
2381 let MM_4M5_IMP_STAB_4M5=prove(`
2382 MMs_v39 scs_4M5' v /\
2384 dist(v i,v j)<= cstab ==>
2385 ~(MMs_v39 (scs_stab_diag_v39 scs_4M5' i j) ={})`,
2387 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2388 THEN EXISTS_TAC`v:num->real^3`
2389 THEN EXISTS_TAC` scs_4M5' `
2390 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M5' `;`v`]
2391 THEN ASSUME_TAC SCS_4M5_BASIC
2392 THEN ASSUME_TAC K_SCS_4M5
2393 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M5_IS_SCS;SCS_4M5_BASIC;K_SCS_4M5;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M5_13;BB_4M5_IMP_BB_STAN_4M5;STAB_4M5_SCS]
2395 THEN REAL_ARITH_TAC);;
2399 let SCS_4M5_ARROW_SCS_4M8_STAB_4M5=prove_by_refinement(
2400 ` scs_arrow_v39 { scs_4M5' } ({scs_4M8} UNION {scs_stab_diag_v39 scs_4M5' i j| scs_diag 4 i j})`,
2402 REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM]
2403 THEN ABBREV_TAC`k=scs_k_v39 s`
2404 THEN REPEAT RESA_TAC;
2407 ASM_SIMP_TAC[SCS_4M8_IS_SCS];
2410 ASM_SIMP_TAC[STAB_4M5_SCS;K_SCS_4M5];
2413 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_4M5' ==> MMs_v39 s = {}) \/ ~((!s. s = scs_4M5' ==> MMs_v39 s = {}))`);
2421 THEN POP_ASSUM MP_TAC
2422 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
2423 THEN REPEAT STRIP_TAC
2424 THEN POP_ASSUM MP_TAC
2426 THEN POP_ASSUM MP_TAC
2427 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2431 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)))`)
2436 THEN ASM_REWRITE_TAC[]
2437 THEN MP_TAC MM_4M5_IMP_4M8
2438 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2440 THEN MATCH_DICH_TAC 0
2441 THEN ASM_REWRITE_TAC[]
2442 THEN EXISTS_TAC`v:num->real^3`
2443 THEN ASM_REWRITE_TAC[];
2447 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;REAL_ARITH`~(a<b)<=> b<=a`]
2449 THEN MP_TAC MM_4M5_IMP_STAB_4M5
2452 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2454 THEN EXISTS_TAC `scs_stab_diag_v39 scs_4M5' i j`
2455 THEN ASM_REWRITE_TAC[]
2458 MATCH_MP_TAC(SET_RULE`A==> B\/A`)
2459 THEN EXISTS_TAC`i:num`
2460 THEN EXISTS_TAC`j:num`
2461 THEN ASM_REWRITE_TAC[];
2464 EXISTS_TAC`v':num->real^3`
2465 THEN ASM_REWRITE_TAC[]]);;
2470 let SET_STAB_4M5=prove(`{ scs_stab_diag_v39 scs_4M5' i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M5' (i MOD 4) (j MOD 4)| scs_diag 4 (i MOD 4) (j MOD 4) }`,
2471 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
2472 THEN MRESAL_TAC STAB_MOD[`scs_4M5'`][SCS_4M5_IS_SCS;K_SCS_4M5]);;
2474 let EXPAND_STAB_DIAG_4M5=prove(`
2475 {scs_stab_diag_v39 scs_4M5' (i MOD 4) (j MOD 4) | j MOD 4 =
2476 (i MOD 4 + 2) MOD 4}=
2477 {scs_stab_diag_v39 scs_4M5' (i+2) i| i<4} `,
2478 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M5_IS_SCS;K_SCS_4M5]);;
2481 let SET_EQ_DIAG_STAB_4M5=prove_by_refinement(
2483 { scs_stab_diag_v39 scs_4M5' i j| scs_diag 4 i j }
2484 {scs_stab_diag_v39 scs_4M5' 0 2,scs_stab_diag_v39 scs_4M5' 1 3}`,
2486 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M5;SET_STAB_4M5;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
2488 REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M5' (i + 2) i |i=0\/i=1\/i=2\/i=3}
2489 = {scs_stab_diag_v39 scs_4M5' (0 + 2) 0} UNION
2490 {scs_stab_diag_v39 scs_4M5' (1 + 2) 1} UNION
2491 {scs_stab_diag_v39 scs_4M5' (2 + 2) 2} UNION
2492 {scs_stab_diag_v39 scs_4M5' (3 + 2) 3}
2494 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M5' 0 2,scs_stab_diag_v39 scs_4M5' 1 3}={scs_stab_diag_v39 scs_4M5' 0 2} UNION {scs_stab_diag_v39 scs_4M5' 1 3}UNION {scs_stab_diag_v39 scs_4M5' 0 2} UNION {scs_stab_diag_v39 scs_4M5' 1 3}`]
2495 THEN MATCH_MP_TAC FZIOTEF_UNION
2496 THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
2497 THEN MRESA_TAC STAB_SYM[`scs_4M5'`;`0`;`2`]
2500 MATCH_MP_TAC FZIOTEF_REFL
2501 THEN REWRITE_TAC[IN_SING]
2502 THEN REPEAT RESA_TAC
2503 THEN ASM_SIMP_TAC[STAB_4M5_SCS;SCS_DIAG_SCS_4M5_02];
2505 MATCH_MP_TAC FZIOTEF_UNION
2506 THEN MRESA_TAC STAB_SYM[`scs_4M5'`;`1`;`3`]
2510 MATCH_MP_TAC FZIOTEF_REFL
2511 THEN REWRITE_TAC[IN_SING]
2512 THEN REPEAT RESA_TAC
2513 THEN ASM_SIMP_TAC[STAB_4M5_SCS;SCS_DIAG_SCS_4M5_13];
2515 MATCH_MP_TAC FZIOTEF_UNION
2516 THEN MRESAL_TAC STAB_MOD[`scs_4M5'`;`4`;`2`][SCS_4M5_IS_SCS;K_SCS_4M5;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
2520 MATCH_MP_TAC FZIOTEF_REFL
2521 THEN REWRITE_TAC[IN_SING]
2522 THEN REPEAT RESA_TAC
2523 THEN ASM_SIMP_TAC[STAB_4M5_SCS;SCS_DIAG_SCS_4M5_02];
2525 MRESAL_TAC STAB_MOD[`scs_4M5'`;`5`;`3`][SCS_4M5_IS_SCS;K_SCS_4M5;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
2528 MATCH_MP_TAC FZIOTEF_REFL
2529 THEN REWRITE_TAC[IN_SING]
2530 THEN REPEAT RESA_TAC
2531 THEN ASM_SIMP_TAC[STAB_4M5_SCS;SCS_DIAG_SCS_4M5_13]]);;
2535 let PROP_OPP_DIAG_4M5_13= prove_by_refinement(`scs_stab_diag_v39 scs_4M5' 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4M5' 0 2)) 2 `,
2536 [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]
2537 THEN MATCH_MP_TAC scs_inj
2538 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M5_BASIC;STAB_4M5_SCS;SCS_DIAG_SCS_4M5_13;scs_basic;unadorned_v39;peropp;peropp2]
2546 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;]
2547 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
2549 THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
2550 THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
2552 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
2553 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
2556 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`)
2557 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2559 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`)
2560 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
2562 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
2563 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;
2567 let STAB_4M5_02_ARROW_4M5_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M5' 0 2}{scs_stab_diag_v39 scs_4M5' 1 3}`,
2568 ASM_SIMP_TAC[PROP_OPP_DIAG_4M5_13]
2569 THEN MATCH_MP_TAC FZIOTEF_TRANS
2570 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4M5' 0 2)}`
2573 MATCH_MP_TAC (GEN_ALL YXIONXL2)
2575 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M5;STAB_4M5_SCS;SCS_DIAG_SCS_4M5_02]
2578 MATCH_MP_TAC(GEN_ALL YXIONXL3)
2579 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
2580 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4M5' 0 2)`
2581 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M5;STAB_4M5_SCS;SCS_DIAG_SCS_4M5_02]]);;
2584 let SCS_4M5_SLICE_13=prove_by_refinement(
2585 `scs_arrow_v39 {scs_stab_diag_v39 scs_4M5' 1 3 } {scs_3T4}`,
2587 ONCE_REWRITE_TAC[SET_RULE`{scs_3T4}={scs_3T4,scs_3T4}`]
2588 THEN MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
2589 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M5_13;STAB_4M5_SCS;SCS_K_D_A_STAB_EQ;]
2592 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_4M5_13]
2593 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
2594 THEN REPEAT RESA_TAC;
2596 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
2598 THEN MATCH_MP_TAC scs_inj
2599 THEN ASM_SIMP_TAC[SCS_3T4_BASIC;SCS_4M5_BASIC;J_SCS_4M5;BASIC_HALF_SLICE_STAB;J_SCS_3T4_1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_3T6_BASIC;J_SCS_3T6]
2602 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M5]
2607 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_3T1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M5;
2608 ARITH_RULE`(3 + 1 + 4 - 1) MOD 4= 3/\ 1 MOD 4=1/\ a+0=a`;scs_prop_equ_v39]
2609 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2610 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2613 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
2614 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
2616 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
2617 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
2619 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2620 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]
2621 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
2622 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
2623 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
2624 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
2625 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
2626 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
2628 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/\
2629 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2630 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2631 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2632 THEN REPEAT RESA_TAC
2633 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)
2634 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
2635 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
2636 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
2637 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2638 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
2642 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;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M5]
2647 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_3T6;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M5;
2648 ARITH_RULE`(1 + 1 + 4 - 3) MOD 4= 3/\ 3 MOD 4=3/\ a+0=a`;scs_prop_equ_v39]
2649 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2650 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
2653 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
2654 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
2656 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
2657 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
2659 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2660 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]
2661 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`0`][ARITH_RULE`~(3=0)`]
2662 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`0`][ARITH_RULE`~(3=0)`]
2663 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`0`][ARITH_RULE`~(3=0)`]
2664 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`0`][ARITH_RULE`~(3=0)`]
2665 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`0`][ARITH_RULE`~(3=0)`]
2666 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`0`][ARITH_RULE`~(3=0)`]
2668 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/\
2669 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2670 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
2671 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
2672 THEN REPEAT RESA_TAC
2673 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)
2674 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
2675 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
2676 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
2677 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
2678 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`x:num`;`x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
2683 THEN REAL_ARITH_TAC;
2686 THEN REAL_ARITH_TAC;
2689 THEN REAL_ARITH_TAC;
2692 THEN REWRITE_TAC[cstab]
2693 THEN REAL_ARITH_TAC;
2697 THEN REWRITE_TAC[cstab]
2698 THEN REAL_ARITH_TAC;
2703 THEN REWRITE_TAC[J_SCS_3T4_1];
2708 let RYPDIXT =prove_by_refinement(
2709 ` scs_arrow_v39 { scs_4M5' } ({scs_4M8,scs_3T4})`,
2711 MATCH_MP_TAC FZIOTEF_TRANS
2712 THEN EXISTS_TAC`({scs_4M8} UNION {scs_stab_diag_v39 scs_4M5' i j| scs_diag 4 i j})`
2713 THEN ASM_REWRITE_TAC[SCS_4M5_ARROW_SCS_4M8_STAB_4M5;SET_RULE`{A,B}={A}UNION{B}`]
2714 THEN MATCH_MP_TAC FZIOTEF_UNION
2717 MATCH_MP_TAC FZIOTEF_REFL
2718 THEN REWRITE_TAC[IN_SING]
2719 THEN REPEAT RESA_TAC
2720 THEN ASM_SIMP_TAC[SCS_4M8_IS_SCS];
2722 MATCH_MP_TAC FZIOTEF_TRANS
2723 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M5' 0 2,scs_stab_diag_v39 scs_4M5' 1 3}`
2724 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M5]
2725 THEN MATCH_MP_TAC FZIOTEF_TRANS
2726 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M5' 1 3,scs_stab_diag_v39 scs_4M5' 1 3}`
2729 REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`]
2730 THEN MATCH_MP_TAC FZIOTEF_UNION
2731 THEN ASM_REWRITE_TAC[STAB_4M5_02_ARROW_4M5_13];
2733 MATCH_MP_TAC FZIOTEF_REFL
2734 THEN REWRITE_TAC[IN_SING]
2735 THEN REPEAT RESA_TAC
2736 THEN ASM_SIMP_TAC[STAB_4M5_SCS;SCS_DIAG_SCS_4M5_13];
2738 REWRITE_TAC[SET_RULE`{A,A}={A}`;SCS_4M5_SLICE_13];
2743 (******** NWDGKXH CASES EQ cstab*******************)
2746 let BB_4M6_IMP_4T5=prove(`!v.
2747 BBs_v39 (scs_stab_diag_v39 scs_4M6' 1 3) v
2749 BBs_v39 (scs_4T5) v`,
2750 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M6;scs_4T5;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4I3;Terminal.FUNLIST_EXPLICIT;]
2751 THEN REPEAT RESA_TAC
2752 THEN THAYTHE_TAC 1[`i`;`j`]
2754 THEN MP_TAC(SET_RULE`psort 4 (i,j) = 1,3\/ ~(psort 4 (i,j) = 1,3)`)
2756 THEN MRESAL_TAC Uaghhbm.CASE_PSORT[`i`;`3`;`j`;`1`;`4`][PSORT_5_EXPLICIT;Uxckfpe.ARITH_4_TAC;PAIR_EQ;cstab]
2763 let MM_4M6_IMP_4T5=prove(
2764 `MMs_v39 (scs_stab_diag_v39 scs_4M6' 1 3) v
2766 ~(MMs_v39 (scs_4T5) ={})`,
2768 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2769 THEN EXISTS_TAC`v:num->real^3`
2770 THEN EXISTS_TAC`(scs_stab_diag_v39 scs_4M6' 1 3)`
2771 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`(scs_stab_diag_v39 scs_4M6' 1 3)`;`v`]
2772 THEN ASSUME_TAC SCS_4T5_BASIC
2773 THEN ASSUME_TAC K_SCS_4T5
2774 THEN ASM_SIMP_TAC[SCS_4T5_IS_SCS;STAB_4M6_SCS;K_SCS_4M6;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M6_13;BB_4M6_IMP_4T5]
2776 THEN REAL_ARITH_TAC);;
2779 let STAB_4M6_13_ARROW_4T5=prove_by_refinement(
2780 ` scs_arrow_v39 { scs_stab_diag_v39 scs_4M6' 1 3 } {scs_4T5}`,
2782 REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;UNION;IN_ELIM_THM]
2783 THEN ABBREV_TAC`k=scs_k_v39 s`
2784 THEN REPEAT RESA_TAC;
2786 ASM_SIMP_TAC[SCS_4T5_IS_SCS];
2788 DISJ_CASES_TAC(SET_RULE`(!s. s = scs_stab_diag_v39 scs_4M6' 1 3 ==> MMs_v39 s = {}) \/ ~((!s. s = scs_stab_diag_v39 scs_4M6' 1 3 ==> MMs_v39 s = {}))`);
2793 THEN POP_ASSUM MP_TAC
2794 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
2795 THEN REPEAT STRIP_TAC
2796 THEN POP_ASSUM MP_TAC
2797 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2799 THEN POP_ASSUM MP_TAC
2801 THEN EXISTS_TAC`scs_4T5`
2802 THEN ASM_REWRITE_TAC[]
2803 THEN MP_TAC MM_4M6_IMP_4T5
2804 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?v. v IN A`;IN]
2808 let PROP_OPP_DIAG_4M6_13= prove_by_refinement(`scs_stab_diag_v39 scs_4M6' 1 3= scs_prop_equ_v39(scs_opp_v39 (scs_stab_diag_v39 scs_4M6' 0 2)) 2 `,
2809 [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]
2810 THEN MATCH_MP_TAC scs_inj
2811 THEN SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;SCS_4M6_BASIC;STAB_4M6_SCS;SCS_DIAG_SCS_4M6_13;scs_basic;unadorned_v39;peropp;peropp2]
2819 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;]
2820 THEN REWRITE_TAC[Terminal.FUNLIST_EXPLICIT]
2822 THEN ASSUME_TAC (ARITH_RULE`~(4=0)`)
2823 THEN MRESA_TAC PSORT_MOD[`4`;`x`;`x'`]
2825 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x`;`4`]
2826 THEN MRESA_TAC MOD_ADD_MOD[`2`;`x'`;`4`]
2829 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`)
2830 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
2832 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`)
2833 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(5=0)`]
2835 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
2836 /\ 3+0=3/\ 3+1=4/\ 3+2=5/\ 3+3=6/\ 3+4=7/\ 7 MOD 5=2`;PAIR_EQ;Terminal.FUNLIST_EXPLICIT;]]);;
2842 let STAB_4M6_02_ARROW_4M6_13=prove(`scs_arrow_v39 {scs_stab_diag_v39 scs_4M6' 0 2}{scs_stab_diag_v39 scs_4M6' 1 3}`,
2843 ASM_SIMP_TAC[PROP_OPP_DIAG_4M6_13]
2844 THEN MATCH_MP_TAC FZIOTEF_TRANS
2845 THEN EXISTS_TAC`{scs_opp_v39 (scs_stab_diag_v39 scs_4M6' 0 2)}`
2848 MATCH_MP_TAC (GEN_ALL YXIONXL2)
2850 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M6;STAB_4M6_SCS;SCS_DIAG_SCS_4M6_02]
2853 MATCH_MP_TAC(GEN_ALL YXIONXL3)
2854 THEN MATCH_MP_TAC (GEN_ALL OPP_IS_SCS)
2855 THEN EXISTS_TAC`scs_opp_v39 (scs_stab_diag_v39 scs_4M6' 0 2)`
2856 THEN ASM_SIMP_TAC[SCS_K_D_A_STAB_EQ;ARITH_RULE`~(4<=3)`;K_SCS_4M6;STAB_4M6_SCS;SCS_DIAG_SCS_4M6_02]]);;
2859 let STAB_4M6_02_ARROW_4T5 =prove(`scs_arrow_v39 { scs_stab_diag_v39 scs_4M6' 0 2 } { scs_4T5 }`,
2860 MATCH_MP_TAC FZIOTEF_TRANS
2861 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M6' 1 3}`
2862 THEN ASM_SIMP_TAC[STAB_4M6_02_ARROW_4M6_13;STAB_4M6_13_ARROW_4T5]);;
2865 let SET_STAB_4M6=prove(`{ scs_stab_diag_v39 scs_4M6' i j| scs_diag 4 i j }= { scs_stab_diag_v39 scs_4M6' (i MOD 4) (j MOD 4)| scs_diag 4 (i MOD 4) (j MOD 4) }`,
2866 ASM_SIMP_TAC[STAB_MOD;DIAG_MOD;EXTENSION;IN_ELIM_THM;ARITH_RULE`~(4=0)`;]
2867 THEN MRESAL_TAC STAB_MOD[`scs_4M6'`][SCS_4M6_IS_SCS;K_SCS_4M6]);;
2869 let EXPAND_STAB_DIAG_4M6=prove(`
2870 {scs_stab_diag_v39 scs_4M6' (i MOD 4) (j MOD 4) | j MOD 4 =
2871 (i MOD 4 + 2) MOD 4}=
2872 {scs_stab_diag_v39 scs_4M6' (i+2) i| i<4} `,
2873 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4;SCS_4M6_IS_SCS;K_SCS_4M6]);;
2876 let SET_EQ_DIAG_STAB_4M6=prove_by_refinement(`scs_arrow_v39
2877 { scs_stab_diag_v39 scs_4M6' i j| scs_diag 4 i j } {scs_stab_diag_v39 scs_4M6' 0 2,scs_stab_diag_v39 scs_4M6' 1 3}`,
2879 ASM_SIMP_TAC[EXPAND_STAB_DIAG_4M6;SET_STAB_4M6;EXPAND_DIAG_4V;MOD_REFL;ARITH_RULE`~(4=0)`]
2881 REWRITE_TAC[ARITH_RULE`i<4<=> i=0\/i=1\/i=2\/i=3`;SET_RULE`{scs_stab_diag_v39 scs_4M6' (i + 2) i |i=0\/i=1\/i=2\/i=3}
2882 = {scs_stab_diag_v39 scs_4M6' (0 + 2) 0} UNION
2883 {scs_stab_diag_v39 scs_4M6' (1 + 2) 1} UNION
2884 {scs_stab_diag_v39 scs_4M6' (2 + 2) 2} UNION
2885 {scs_stab_diag_v39 scs_4M6' (3 + 2) 3}
2887 THEN ONCE_REWRITE_TAC[SET_RULE`{scs_stab_diag_v39 scs_4M6' 0 2,scs_stab_diag_v39 scs_4M6' 1 3}={scs_stab_diag_v39 scs_4M6' 0 2} UNION {scs_stab_diag_v39 scs_4M6' 1 3}UNION {scs_stab_diag_v39 scs_4M6' 0 2} UNION {scs_stab_diag_v39 scs_4M6' 1 3}`]
2888 THEN MATCH_MP_TAC FZIOTEF_UNION
2889 THEN REWRITE_TAC[ARITH_RULE`0+2=2/\ 1+2=3/\2+2=4/\ 3+2=5`]
2890 THEN MRESA_TAC STAB_SYM[`scs_4M6'`;`0`;`2`]
2893 MATCH_MP_TAC FZIOTEF_REFL
2894 THEN REWRITE_TAC[IN_SING]
2895 THEN REPEAT RESA_TAC
2896 THEN ASM_SIMP_TAC[STAB_4M6_SCS;SCS_DIAG_SCS_4M6_02];
2898 MATCH_MP_TAC FZIOTEF_UNION
2899 THEN MRESA_TAC STAB_SYM[`scs_4M6'`;`1`;`3`]
2902 MATCH_MP_TAC FZIOTEF_REFL
2903 THEN REWRITE_TAC[IN_SING]
2904 THEN REPEAT RESA_TAC
2905 THEN ASM_SIMP_TAC[STAB_4M6_SCS;SCS_DIAG_SCS_4M6_13];
2907 MATCH_MP_TAC FZIOTEF_UNION
2908 THEN MRESAL_TAC STAB_MOD[`scs_4M6'`;`4`;`2`][SCS_4M6_IS_SCS;K_SCS_4M6;ARITH_RULE`4 MOD 4=0/\ 2 MOD 4=2`]
2912 MATCH_MP_TAC FZIOTEF_REFL
2913 THEN REWRITE_TAC[IN_SING]
2914 THEN REPEAT RESA_TAC
2915 THEN ASM_SIMP_TAC[STAB_4M6_SCS;SCS_DIAG_SCS_4M6_02];
2917 MRESAL_TAC STAB_MOD[`scs_4M6'`;`5`;`3`][SCS_4M6_IS_SCS;K_SCS_4M6;ARITH_RULE`5 MOD 4=1/\ 3 MOD 4=3`]
2920 MATCH_MP_TAC FZIOTEF_REFL
2921 THEN REWRITE_TAC[IN_SING]
2922 THEN REPEAT RESA_TAC
2923 THEN ASM_SIMP_TAC[STAB_4M6_SCS;SCS_DIAG_SCS_4M6_13]]);;
2928 let SET_STAB_4M6_ARROW_4T5=prove(`scs_arrow_v39
2929 { scs_stab_diag_v39 scs_4M6' i j| scs_diag 4 i j } {scs_4T5}`,
2930 ONCE_REWRITE_TAC[SET_RULE`{A}={A,A}`]
2931 THEN MATCH_MP_TAC FZIOTEF_TRANS
2932 THEN EXISTS_TAC`{scs_stab_diag_v39 scs_4M6' 0 2,scs_stab_diag_v39 scs_4M6' 1 3}`
2933 THEN ASM_REWRITE_TAC[SET_EQ_DIAG_STAB_4M6;]
2934 THEN REWRITE_TAC[SET_RULE`{A,B}={A}UNION{B}`;]
2935 THEN MATCH_MP_TAC FZIOTEF_UNION
2936 THEN ASM_SIMP_TAC[STAB_4M6_02_ARROW_4T5;STAB_4M6_13_ARROW_4T5]);;
2940 let BB_4M6_IMP_BB_STAN_4M6= prove(`
2941 BBs_v39 scs_4M6' v /\
2943 dist(v i,v j)<= cstab ==>
2944 BBs_v39 (scs_stab_diag_v39 scs_4M6' i j) v`,
2945 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M6;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6]
2946 THEN REPEAT RESA_TAC
2947 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ 2+1=3/\ 3+1=4`)
2949 THEN MP_TAC(SET_RULE`psort 4 (i,j) = psort 4 (i',j')\/ ~(psort 4 (i,j) = psort 4 (i',j'))`)
2951 THEN MRESA_TAC Uaghhbm.CASE_PSORT[`i`;`j'`;`j`;`i'`;`4`]
2953 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M6'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M6;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M6_IS_SCS]
2954 THEN THAYTHEL_ASM_TAC 0[`i'`;`i`][]
2955 THEN THAYTHEL_ASM_TAC 0[`j'`;`j`][];
2957 MRESAS_TAC BB_VV_FUN_EQ[`v`;`scs_4M6'`][scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39;scs_4M6;scs_4M6;CS_ADJ;scs_diag;ARITH_RULE`~(4<=3)`;IN;K_SCS_4M6;Terminal.FUNLIST_EXPLICIT;K_SCS_4M6;SCS_4M6_IS_SCS]
2958 THEN THAYTHEL_ASM_TAC 0[`i'`;`j`][]
2959 THEN THAYTHEL_ASM_TAC 0[`j'`;`i`][]
2960 THEN ONCE_REWRITE_TAC[DIST_SYM]
2961 THEN ASM_REWRITE_TAC[]]);;
2964 let MM_4M6_IMP_STAB_4M6=prove(`
2965 MMs_v39 scs_4M6' v /\
2967 dist(v i,v j)<= cstab ==>
2968 ~(MMs_v39 (scs_stab_diag_v39 scs_4M6' i j) ={})`,
2970 THEN MATCH_MP_TAC (GEN_ALL Ppbtydq.XWNHLMD_MM)
2971 THEN EXISTS_TAC`v:num->real^3`
2972 THEN EXISTS_TAC` scs_4M6' `
2973 THEN MRESA_TAC Nuxcoea.MMS_IMP_BBS[`scs_4M6' `;`v`]
2974 THEN ASSUME_TAC SCS_4M6_BASIC
2975 THEN ASSUME_TAC K_SCS_4M6
2976 THEN ASM_SIMP_TAC[SCS_4M6_IS_SCS;SCS_4M6_IS_SCS;SCS_4M6_BASIC;K_SCS_4M6;SCS_K_D_A_STAB_EQ;IN; ADD1;SCS_DIAG_SCS_4M6_13;BB_4M6_IMP_BB_STAN_4M6;STAB_4M6_SCS]
2978 THEN REAL_ARITH_TAC);;
2988 let check_completeness_claimA_concl =
2989 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)