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 Jkqewgv = struct
26 open Wrgcvdr_cizmrrh;;
34 open Flyspeck_constants;;
47 open Wrgcvdr_cizmrrh;;
49 open Flyspeck_constants;;
65 let IS_SCS_STABLE_SYSTEM=prove_by_refinement(
66 `is_scs_v39 s /\ 3< scs_k_v39 s
68 stable_system (scs_k_v39 s) (scs_d_v39 s) (0..(scs_k_v39 s)-1)
69 (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s))
70 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)) (\i. ((1+i):num MOD (scs_k_v39 s)))
74 REWRITE_TAC[is_scs_v39;stable_system;constraint_system;torsor;change_type_v2;change_type_v3]
77 THEN MP_TAC (ARITH_RULE`3<= scs_k_v39 s==> (scs_k_v39 s - 1 +1)-0= scs_k_v39 s
78 /\ (scs_k_v39 s - 1 +1)= scs_k_v39 s/\ 1< scs_k_v39 s /\ 1<= scs_k_v39 s /\ 1<= scs_k_v39 s -1/\ ~(scs_k_v39 s=0)`)
80 THEN MRESA_TAC HAS_SIZE_NUMSEG[`0`;`scs_k_v39 s -1`]
81 THEN REPLICATE_TAC 23 (POP_ASSUM MP_TAC)
90 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
91 THEN MRESAL1_TAC Hypermap.LE_MOD_SUC`scs_k_v39 s -1`[ADD1];
95 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
97 THEN MP_TAC(ARITH_RULE`x1 <= scs_k_v39 s - 1 /\
99 ==> 1+ x1 <= scs_k_v39 s -1 +1 /\ 1+ x2 <= scs_k_v39 s - 1+1`)
101 THEN MRESAL_TAC (GEN_ALL MOD_IMP_EQ)[`scs_k_v39 s`;`1+x1`;`1+x2`][ARITH_RULE`1<= 1+A /\ (1+A<=4<=> A<=3)`]
102 THEN POP_ASSUM MP_TAC
107 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
108 THEN REPEAT STRIP_TAC
109 THEN POP_ASSUM MP_TAC
110 THEN MP_TAC(ARITH_RULE`0<i==> 1<= i`)
112 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s:num`;`x:num`;`i:num`]
113 THEN MP_TAC(ARITH_RULE`3<= scs_k_v39 s/\ scs_k_v39 s<=6
114 ==> scs_k_v39 s=3 \/ scs_k_v39 s=4 \/ scs_k_v39 s=5 \/ scs_k_v39 s= 6`)
116 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT DISCH_TAC
117 THEN POP_ASSUM MP_TAC);
119 MP_TAC(ARITH_RULE`0<i /\ i< 3==> i=1 \/ i=2 `)
121 THEN MP_TAC(ARITH_RULE`x<= 3-1==> x=0 \/ x=1 \/ x=2 `)
122 THEN ASM_REWRITE_TAC[]
126 MP_TAC(ARITH_RULE`0<i /\ i< 4==> i=1 \/ i=2 \/ i=3`)
128 THEN MP_TAC(ARITH_RULE`x<= 4-1==> x=0 \/ x=1 \/ x=2 \/ x=3`)
129 THEN ASM_REWRITE_TAC[]
133 MP_TAC(ARITH_RULE`0<i /\ i< 5==> i=1 \/ i=2 \/ i=3\/ i=4`)
135 THEN MP_TAC(ARITH_RULE`x<= 5-1==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4`)
136 THEN ASM_REWRITE_TAC[]
140 MP_TAC(ARITH_RULE`0<i /\ i< 6==> i=1 \/ i=2 \/ i=3\/ i=4\/ i=5`)
142 THEN MP_TAC(ARITH_RULE`x<= 6-1==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4\/ x=5`)
143 THEN ASM_REWRITE_TAC[]
147 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
148 THEN REPEAT STRIP_TAC
149 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s:num`;`x:num`;`scs_k_v39 s:num`]
150 THEN MRESAL_TAC MOD_MULT_ADD[`1`;`scs_k_v39 s`;`x:num`][ARITH_RULE`1*A=A`]
151 THEN MP_TAC(ARITH_RULE`x<=scs_k_v39 s -1 /\ 3<= scs_k_v39 s ==> x< scs_k_v39 s`)
153 THEN MRESA_TAC MOD_LT[`x:num`;`scs_k_v39 s`];
157 REPLICATE_TAC 15 (REMOVE_ASSUM_TAC)
158 THEN REPEAT STRIP_TAC
159 THEN POP_ASSUM(fun th-> MRESA_TAC th[`i:num`;`j:num`])
160 THEN REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
166 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s`;`j:num`;`scs_k_v39 s`]
167 THEN MRESAL_TAC MOD_MULT_ADD[`1`;`scs_k_v39 s`;`j:num`][ARITH_RULE`1*A=A`]
168 THEN MRESAL_TAC MOD_MOD_REFL[`j:num`;`scs_k_v39 s`][ARITH_RULE`~(5=0)`]
170 THEN REWRITE_TAC[periodic2]
171 THEN REPEAT DISCH_TAC
172 THEN ONCE_REWRITE_TAC[SET_RULE`A=B <=> B=A`]
175 MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s i`][periodic];
177 MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s i`][periodic];
182 THEN REWRITE_TAC[periodic2;SUBSET;IN_ELIM_THM]
183 THEN REPEAT DISCH_TAC
184 THEN REPEAT STRIP_TAC
185 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
186 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
187 THEN MRESAL_TAC th[`i:num`;`j:num`][ADD1;ARITH_RULE`1+i=i+1`]);
189 EXISTS_TAC`i MOD scs_k_v39 s`
190 THEN REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
191 THEN MRESA_TAC DIVISION[`i:num`;`scs_k_v39 s`]
192 THEN MP_TAC(ARITH_RULE`i MOD scs_k_v39 s < scs_k_v39 s
194 ==> i MOD scs_k_v39 s <= scs_k_v39 s-1`)
196 THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
197 THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1];
199 EXISTS_TAC`j MOD scs_k_v39 s`
200 THEN REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
201 THEN MRESA_TAC DIVISION[`j:num`;`scs_k_v39 s`]
202 THEN MP_TAC(ARITH_RULE`j MOD scs_k_v39 s < scs_k_v39 s
204 ==> j MOD scs_k_v39 s <= scs_k_v39 s-1`)
206 THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
207 THEN MRESAL_TAC MOD_ADD_MOD[`j:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
210 SUBGOAL_THEN`{{i MOD scs_k_v39 s, j MOD scs_k_v39 s} | i,j | scs_J_v39 s i j}
211 SUBSET {{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
212 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
215 REWRITE_TAC[SUBSET;IN_ELIM_THM]
218 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
219 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
220 THEN MRESAL_TAC th[`i:num`;`j:num`][ADD1;ARITH_RULE`1+i=i+1`]);
222 EXISTS_TAC`i:num MOD scs_k_v39 s`
223 THEN ASM_REWRITE_TAC[]
224 THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
225 THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
226 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0)`]
227 THEN MRESA_TAC DIVISION[`i:num`;`scs_k_v39 s`]
229 THEN REWRITE_TAC[periodic;periodic2]
230 THEN REPEAT DISCH_TAC
231 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][periodic]
232 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j:num`)
233 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][periodic]
234 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(i MOD scs_k_v39 s) +1:num`)
235 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
236 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][periodic]
237 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(i MOD scs_k_v39 s) +1:num`)
238 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
239 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + 1) MOD scs_k_v39 s)`][periodic]
240 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
241 THEN REPLICATE_TAC 19 (POP_ASSUM MP_TAC)
242 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
243 THEN MRESA_TAC th[`(i MOD scs_k_v39 s)`; `((i + 1) MOD scs_k_v39 s)`])
244 THEN REWRITE_TAC[h0;cstab;sqrt8]
247 EXISTS_TAC`j:num MOD scs_k_v39 s`
248 THEN ASM_REWRITE_TAC[]
249 THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
250 THEN MRESAL_TAC MOD_ADD_MOD[`j:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
251 THEN MRESAL_TAC MOD_MOD_REFL[`j:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0)`]
252 THEN MRESA_TAC DIVISION[`j:num`;`scs_k_v39 s`]
254 THEN REWRITE_TAC[periodic;periodic2;SET_RULE`{A,B}={B,A}`]
255 THEN REPEAT DISCH_TAC
256 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s j`][periodic]
257 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
258 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][periodic]
259 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(j MOD scs_k_v39 s) +1:num`)
260 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
261 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][periodic]
262 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(j MOD scs_k_v39 s) +1:num`)
263 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
264 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((j + 1) MOD scs_k_v39 s)`][periodic]
265 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j:num`)
266 THEN REPLICATE_TAC 19 (POP_ASSUM MP_TAC)
267 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
268 THEN MRESA_TAC th[`(j MOD scs_k_v39 s)`; `((j + 1) MOD scs_k_v39 s)`])
269 THEN REWRITE_TAC[h0;cstab;sqrt8]
272 SUBGOAL_THEN`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
274 scs_b_v39 s i (SUC i) \/
276 scs_a_v39 s i (SUC i))}
277 SUBSET IMAGE (\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s}) {i | i < scs_k_v39 s /\
278 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
281 REWRITE_TAC[IN_ELIM_THM;IMAGE;SUBSET];
283 SUBGOAL_THEN` {i | i < scs_k_v39 s /\
284 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}
285 SUBSET 0.. scs_k_v39 s`
288 REWRITE_TAC[IN_ELIM_THM;SUBSET;IN_NUMSEG]
291 MRESAL_TAC CARD_SUBSET[`{i | i < scs_k_v39 s /\
292 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
293 `0.. scs_k_v39 s`][FINITE_NUMSEG]
294 THEN MRESAL_TAC FINITE_SUBSET[`{i | i < scs_k_v39 s /\
295 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
296 `0.. scs_k_v39 s`][FINITE_NUMSEG]
297 THEN MRESAL_TAC CARD_SUBSET_IMAGE
298 [`(\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s})`;`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
300 scs_b_v39 s i (SUC i) \/
302 scs_a_v39 s i (SUC i))}`;`{i | i < scs_k_v39 s /\
303 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
305 THEN MRESAL_TAC FINITE_IMAGE
306 [`(\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s})`;`{i | i < scs_k_v39 s /\
307 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
309 THEN MRESAL_TAC FINITE_SUBSET[`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
311 scs_b_v39 s i (SUC i) \/
313 scs_a_v39 s i (SUC i))}`;
314 `IMAGE (\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s}) {i | i < scs_k_v39 s /\
315 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`][FINITE_NUMSEG]
316 THEN MRESAL_TAC CARD_SUBSET[`{{i MOD scs_k_v39 s, j MOD scs_k_v39 s} | i,j | scs_J_v39 s i j}`;
317 `{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
319 scs_b_v39 s i (SUC i) \/
321 scs_a_v39 s i (SUC i))}`][FINITE_NUMSEG]
322 THEN POP_ASSUM MP_TAC
323 THEN REPLICATE_TAC 2 (REMOVE_ASSUM_TAC)
324 THEN POP_ASSUM MP_TAC
325 THEN REPLICATE_TAC 13(REMOVE_ASSUM_TAC)
326 THEN POP_ASSUM MP_TAC
331 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
332 THEN REPEAT STRIP_TAC
333 THEN REPLICATE_TAC 16 (POP_ASSUM MP_TAC)
334 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
335 THEN MATCH_MP_TAC th)
336 THEN ASM_REWRITE_TAC[]
337 THEN REMOVE_ASSUM_TAC
338 THEN POP_ASSUM MP_TAC
339 THEN POP_ASSUM MP_TAC
340 THEN REPLICATE_TAC 24 (REMOVE_ASSUM_TAC)
341 THEN POP_ASSUM MP_TAC
346 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`;]
347 THEN REPEAT STRIP_TAC
348 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
349 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
350 THEN MRESAL1_TAC th`i:num`[ADD1])
352 THEN REWRITE_TAC[periodic2]
353 THEN REPEAT STRIP_TAC
354 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][periodic]
355 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
356 THEN ASM_REWRITE_TAC[ARITH_RULE`1+i=i+1`]
357 THEN REMOVE_ASSUM_TAC
358 THEN POP_ASSUM MP_TAC
361 REWRITE_TAC[IN_ELIM_THM]
362 THEN REPEAT STRIP_TAC
363 THEN ASM_REWRITE_TAC[]
364 THEN MP_TAC(SET_RULE`{i, j} = {i' MOD scs_k_v39 s, j' MOD scs_k_v39 s}
365 ==> (i = i' MOD scs_k_v39 s /\ j= j' MOD scs_k_v39 s)\/
366 (j = i' MOD scs_k_v39 s /\ i= j' MOD scs_k_v39 s)`)
367 THEN ASM_REWRITE_TAC[]
369 THEN ASM_REWRITE_TAC[]
371 THEN REWRITE_TAC[periodic2]
372 THEN REPEAT STRIP_TAC
373 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][periodic]
374 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j':num`)
375 THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC)
376 THEN POP_ASSUM(fun th-> MRESA_TAC th[`i':num`;`(j' MOD scs_k_v39 s)`]
377 THEN MRESA_TAC th[`i' MOD scs_k_v39 s:num`;`(j' MOD scs_k_v39 s)`])
378 THEN REPEAT STRIP_TAC
379 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD scs_k_v39 s)`][periodic;]
380 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i':num`)
381 THEN REPLICATE_TAC 15 (POP_ASSUM MP_TAC)
382 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
383 THEN MRESA_TAC th[`(i' MOD scs_k_v39 s)`;`(j' MOD scs_k_v39 s)`])
384 THEN REWRITE_TAC[sqrt8]
409 let IS_SCS_TRI_STABLE_SYSTEM=prove_by_refinement(
410 `is_scs_v39 s /\ scs_k_v39 s=3
412 tri_stable (scs_k_v39 s) (scs_d_v39 s) (0..(scs_k_v39 s)-1)
413 (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s))
414 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)) (\i. ((1+i):num MOD (scs_k_v39 s)))
417 REWRITE_TAC[is_scs_v39;tri_stable;constraint_system;torsor;change_type_v2;change_type_v3]
420 THEN MP_TAC (ARITH_RULE`3<= scs_k_v39 s==> (scs_k_v39 s - 1 +1)-0= scs_k_v39 s
421 /\ (scs_k_v39 s - 1 +1)= scs_k_v39 s/\ 1< scs_k_v39 s /\ 1<= scs_k_v39 s /\ 1<= scs_k_v39 s -1/\ ~(scs_k_v39 s=0)/\ 3-0=3`)
423 THEN MRESA_TAC HAS_SIZE_NUMSEG[`0`;`scs_k_v39 s -1`]
424 THEN REPLICATE_TAC 23 (POP_ASSUM MP_TAC)
425 THEN REMOVE_ASSUM_TAC
426 THEN REPEAT DISCH_TAC
431 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
432 THEN MRESAL1_TAC Hypermap.LE_MOD_SUC`scs_k_v39 s -1`[ADD1];
436 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
437 THEN REPEAT STRIP_TAC
438 THEN MP_TAC(ARITH_RULE`x1 <= scs_k_v39 s - 1 /\
439 x2 <= scs_k_v39 s - 1
440 ==> 1+ x1 <= scs_k_v39 s -1 +1 /\ 1+ x2 <= scs_k_v39 s - 1+1`)
442 THEN MRESAL_TAC (GEN_ALL MOD_IMP_EQ)[`scs_k_v39 s`;`1+x1`;`1+x2`][ARITH_RULE`1<= 1+A /\ (1+A<=4<=> A<=3)`]
443 THEN POP_ASSUM MP_TAC
448 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
449 THEN REPEAT STRIP_TAC
450 THEN POP_ASSUM MP_TAC
451 THEN MP_TAC(ARITH_RULE`0<i==> 1<= i`)
453 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s:num`;`x:num`;`i:num`]
454 THEN MP_TAC(ARITH_RULE`0<i /\ i< 3==> i=1 \/ i=2 `)
456 THEN MP_TAC(ARITH_RULE`x<= 3-1==> x=0 \/ x=1 \/ x=2 `)
457 THEN ASM_REWRITE_TAC[]
461 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
462 THEN REPEAT STRIP_TAC
463 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s:num`;`x:num`;`scs_k_v39 s:num`]
464 THEN MRESAL_TAC MOD_MULT_ADD[`1`;`scs_k_v39 s`;`x:num`][ARITH_RULE`1*A=A`]
465 THEN MP_TAC(ARITH_RULE`x<=scs_k_v39 s -1 /\ 3<= scs_k_v39 s ==> x< scs_k_v39 s`)
467 THEN MRESA_TAC MOD_LT[`x:num`;`scs_k_v39 s`];
471 REPLICATE_TAC 16 (REMOVE_ASSUM_TAC)
472 THEN REPEAT STRIP_TAC
473 THEN POP_ASSUM(fun th-> MRESA_TAC th[`i:num`;`j:num`])
474 THEN REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
480 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s`;`j:num`;`scs_k_v39 s`]
481 THEN MRESAL_TAC MOD_MULT_ADD[`1`;`scs_k_v39 s`;`j:num`][ARITH_RULE`1*A=A`]
482 THEN MRESAL_TAC MOD_MOD_REFL[`j:num`;`scs_k_v39 s`][ARITH_RULE`~(5=0)`]
484 THEN REWRITE_TAC[periodic2]
485 THEN REPEAT DISCH_TAC
486 THEN ONCE_REWRITE_TAC[SET_RULE`A=B <=> B=A`]
489 MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s i`][periodic];
491 MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s i`][periodic];
496 THEN REWRITE_TAC[periodic2;SUBSET;IN_ELIM_THM]
497 THEN REPEAT DISCH_TAC
498 THEN REPEAT STRIP_TAC
499 THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
500 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
501 THEN MRESAL_TAC th[`i:num`;`j:num`][ADD1;ARITH_RULE`1+i=i+1`]);
503 EXISTS_TAC`i MOD scs_k_v39 s`
504 THEN REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
505 THEN MRESA_TAC DIVISION[`i:num`;`scs_k_v39 s`]
506 THEN MP_TAC(ARITH_RULE`i MOD scs_k_v39 s < scs_k_v39 s
508 ==> i MOD scs_k_v39 s <= scs_k_v39 s-1`)
510 THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
511 THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1];
513 EXISTS_TAC`j MOD scs_k_v39 s`
514 THEN REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
515 THEN MRESA_TAC DIVISION[`j:num`;`scs_k_v39 s`]
516 THEN MP_TAC(ARITH_RULE`j MOD scs_k_v39 s < scs_k_v39 s
518 ==> j MOD scs_k_v39 s <= scs_k_v39 s-1`)
520 THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
521 THEN MRESAL_TAC MOD_ADD_MOD[`j:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
524 SUBGOAL_THEN`{{i MOD scs_k_v39 s, j MOD scs_k_v39 s} | i,j | scs_J_v39 s i j}
525 SUBSET {{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
526 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
529 REWRITE_TAC[SUBSET;IN_ELIM_THM]
532 THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
533 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
534 THEN MRESAL_TAC th[`i:num`;`j:num`][ADD1;ARITH_RULE`1+i=i+1`]);
536 EXISTS_TAC`i:num MOD scs_k_v39 s`
537 THEN ASM_REWRITE_TAC[]
538 THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
539 THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
540 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0)`]
541 THEN MRESA_TAC DIVISION[`i:num`;`scs_k_v39 s`]
543 THEN REWRITE_TAC[periodic;periodic2]
544 THEN REPEAT DISCH_TAC
545 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][periodic]
546 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j:num`)
547 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][periodic]
548 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(i MOD scs_k_v39 s) +1:num`)
549 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
550 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][periodic]
551 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(i MOD scs_k_v39 s) +1:num`)
552 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
553 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + 1) MOD scs_k_v39 s)`][periodic]
554 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
555 THEN REPLICATE_TAC 20 (POP_ASSUM MP_TAC)
556 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
557 THEN MRESA_TAC th[`(i MOD scs_k_v39 s)`; `((i + 1) MOD scs_k_v39 s)`])
558 THEN REWRITE_TAC[h0;cstab;sqrt8]
561 EXISTS_TAC`j:num MOD scs_k_v39 s`
562 THEN ASM_REWRITE_TAC[]
563 THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
564 THEN MRESAL_TAC MOD_ADD_MOD[`j:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
565 THEN MRESAL_TAC MOD_MOD_REFL[`j:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0)`]
566 THEN MRESA_TAC DIVISION[`j:num`;`scs_k_v39 s`]
568 THEN REWRITE_TAC[periodic;periodic2;SET_RULE`{A,B}={B,A}`]
569 THEN REPEAT DISCH_TAC
570 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s j`][periodic]
571 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
572 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][periodic]
573 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(j MOD scs_k_v39 s) +1:num`)
574 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
575 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][periodic]
576 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(j MOD scs_k_v39 s) +1:num`)
577 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
578 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((j + 1) MOD scs_k_v39 s)`][periodic]
579 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j:num`)
580 THEN REPLICATE_TAC 20 (POP_ASSUM MP_TAC)
581 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
582 THEN MRESA_TAC th[`(j MOD scs_k_v39 s)`; `((j + 1) MOD scs_k_v39 s)`])
583 THEN REWRITE_TAC[h0;cstab;sqrt8]
586 SUBGOAL_THEN`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
588 scs_b_v39 s i (SUC i) \/
590 scs_a_v39 s i (SUC i))}
591 SUBSET IMAGE (\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s}) {i | i < scs_k_v39 s /\
592 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
595 REWRITE_TAC[IN_ELIM_THM;IMAGE;SUBSET];
597 SUBGOAL_THEN` {i | i < scs_k_v39 s /\
598 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}
599 SUBSET 0.. scs_k_v39 s`
602 REWRITE_TAC[IN_ELIM_THM;SUBSET;IN_NUMSEG]
607 MRESAL_TAC CARD_SUBSET[`{i | i < scs_k_v39 s /\
608 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
609 `0.. scs_k_v39 s`][FINITE_NUMSEG]
610 THEN MRESAL_TAC FINITE_SUBSET[`{i | i < scs_k_v39 s /\
611 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
612 `0.. scs_k_v39 s`][FINITE_NUMSEG]
613 THEN MRESAL_TAC CARD_SUBSET_IMAGE
614 [`(\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s})`;`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
616 scs_b_v39 s i (SUC i) \/
618 scs_a_v39 s i (SUC i))}`;`{i | i < scs_k_v39 s /\
619 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
621 THEN MRESAL_TAC FINITE_IMAGE
622 [`(\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s})`;`{i | i < scs_k_v39 s /\
623 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
625 THEN MRESAL_TAC FINITE_SUBSET[`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
627 scs_b_v39 s i (SUC i) \/
629 scs_a_v39 s i (SUC i))}`;
630 `IMAGE (\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s}) {i | i < scs_k_v39 s /\
631 (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`][FINITE_NUMSEG]
632 THEN MRESAL_TAC CARD_SUBSET[`{{i MOD scs_k_v39 s, j MOD scs_k_v39 s} | i,j | scs_J_v39 s i j}`;
633 `{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
635 scs_b_v39 s i (SUC i) \/
637 scs_a_v39 s i (SUC i))}`][FINITE_NUMSEG]
638 THEN POP_ASSUM MP_TAC
639 THEN REPLICATE_TAC 2 (REMOVE_ASSUM_TAC)
640 THEN POP_ASSUM MP_TAC
641 THEN REPLICATE_TAC 13(REMOVE_ASSUM_TAC)
642 THEN POP_ASSUM (fun th->
644 THEN ASM_REWRITE_TAC[th])
648 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
649 THEN REPEAT STRIP_TAC
650 THEN REPLICATE_TAC 17 (POP_ASSUM MP_TAC)
651 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
652 THEN MATCH_MP_TAC th)
653 THEN ASM_REWRITE_TAC[]
654 THEN REMOVE_ASSUM_TAC
655 THEN POP_ASSUM MP_TAC
656 THEN POP_ASSUM MP_TAC
657 THEN REPLICATE_TAC 25 (REMOVE_ASSUM_TAC)
658 THEN POP_ASSUM MP_TAC
664 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`;]
665 THEN REPEAT STRIP_TAC
666 THEN REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
667 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
668 THEN MRESAL1_TAC th`i:num`[ADD1])
670 THEN REWRITE_TAC[periodic2]
671 THEN REPEAT STRIP_TAC
672 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][periodic]
673 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
674 THEN ASM_REWRITE_TAC[ARITH_RULE`1+i=i+1`]
675 THEN POP_ASSUM MP_TAC;
677 REWRITE_TAC[IN_ELIM_THM]
678 THEN REPEAT STRIP_TAC
679 THEN ASM_REWRITE_TAC[]
680 THEN MP_TAC(SET_RULE`{i, j} = {i' MOD scs_k_v39 s, j' MOD scs_k_v39 s}
681 ==> (i = i' MOD scs_k_v39 s /\ j= j' MOD scs_k_v39 s)\/
682 (j = i' MOD scs_k_v39 s /\ i= j' MOD scs_k_v39 s)`)
683 THEN ASM_REWRITE_TAC[]
685 THEN ASM_REWRITE_TAC[]
687 THEN REWRITE_TAC[periodic2]
688 THEN REPEAT STRIP_TAC
689 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][periodic]
690 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j':num`)
691 THEN REPLICATE_TAC 22 (POP_ASSUM MP_TAC)
692 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
693 THEN MRESA_TAC th[`i':num`;`(j' MOD scs_k_v39 s)`]
694 THEN MRESA_TAC th[`i' MOD scs_k_v39 s:num`;`(j' MOD scs_k_v39 s)`])
695 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD scs_k_v39 s)`][periodic;]
696 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i':num`)
697 THEN REPLICATE_TAC (42 -16) (POP_ASSUM MP_TAC)
698 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
699 THEN MRESA_TAC th[`(i' MOD scs_k_v39 s)`;`(j' MOD scs_k_v39 s)`])
700 THEN REWRITE_TAC[sqrt8];
707 let IS_SCS_IN_BALL_ANNULUS_4=
709 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
710 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
711 THEN MP_TAC th THEN REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM])
713 THEN POP_ASSUM MATCH_MP_TAC
715 THEN MRESAL_TAC VECTOR_3_4[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=4/\ 2<=4/\ 3<=4/\ 4<=4/\ 4 MOD 4= 0 /\ 1 MOD 4= 1 /\ 2 MOD 4= 2/\ 3 MOD 4= 3/\ ~(2=1)
716 /\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)`;SET_RULE`(a:num) IN (:num)`]
721 let IS_SCS_IN_V_SY_4=
724 THEN MRESAL_TAC VECTOR_3_4[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=4/\ 2<=4/\ 3<=4/\ 4<=4/\ 4 MOD 4= 0 /\ 1 MOD 4= 1 /\ 2 MOD 4= 2/\ 3 MOD 4= 3/\ ~(2=1)
725 /\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)/\ 1<=1/\ 1<=2 /\ 1<=3/\ SUC 1=2/\ SUC 2=3 /\ SUC 3=4/\ SUC 0=1`;SET_RULE`(a:num) IN (:num)`]
729 let PROVE_E_SY_INV_TAC_4=
731 MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x':num`;th;`4`][ARITH_RULE`~(4=0)/\ 4 MOD 4=0/\ SUC 0 MOD 4=1/\ 1 MOD 4=1 /\ 2 MOD 4=2 /\ 3 MOD 4=3`]
733 THEN MRESAL_TAC VECTOR_3_4[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=4/\ 2<=4/\ 3<=4/\ 4<=4/\ 4 MOD 4= 0 /\ 1 MOD 4= 1 /\ 2 MOD 4= 2/\ 3 MOD 4= 3/\ ~(2=1)
734 /\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)/\ SUC 1=2/\ SUC 0=1 /\ SUC 2= 3/\ SUC 3=4/\ 1<=1 /\ 1<=2 /\ 1<=3`];;
739 let V_E_FF_IS_SCS_CASES_4=prove_by_refinement(
740 ` is_scs_v39 s /\ scs_k_v39 s=4 /\ vv IN BBs_v39 s
741 /\ dimindex(:M)=scs_k_v39 s
742 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 0]:real^3^M= v
743 /\ matvec (v:real^3^M) =a
745 V_SY (v:real^3^M)=IMAGE vv (:num)/\
746 E_SY (v:real^3^M)=IMAGE (\i. {vv i, vv (SUC i)}) (:num)/\
747 F_SY (v:real^3^M)=IMAGE (\i. vv i,vv (SUC i)) (:num)`
752 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
753 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;IN;mk_unadorned_v39]
754 THEN REPEAT STRIP_TAC;
756 REWRITE_TAC[V_SY;rows]
757 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`]
758 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
759 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`]
768 IS_SCS_IN_V_SY_4`0`];
771 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4)<=> (1<= i /\ i<= 4)`]
772 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`4`;`vv:num-> real^3`][ARITH_RULE`~(4=0)`]
773 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`)
774 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
775 THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
776 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`)
782 IS_SCS_IN_V_SY_4`3`];
784 REWRITE_TAC[E_SY;rows]
785 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
786 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`]
788 THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
796 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`4`;`vv:num-> real^3`][ARITH_RULE`~(4=0)`]
797 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 3`[ARITH_RULE`SUC 3 MOD 4=0/\ SUC 3=4`])
798 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
799 IS_SCS_IN_V_SY_4`0`];
802 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4)<=> (1<= i /\ i<= 4)`]
803 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`4`;`vv:num-> real^3`][ARITH_RULE`~(4=0)`]
804 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
805 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
806 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
807 THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
808 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`)
811 PROVE_E_SY_INV_TAC_4 `4`;
812 PROVE_E_SY_INV_TAC_4 `1`;
813 PROVE_E_SY_INV_TAC_4 `2`;
814 PROVE_E_SY_INV_TAC_4 `3`];
816 REWRITE_TAC[F_SY;rows]
817 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
818 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`]
820 THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
828 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`4`;`vv:num-> real^3`][ARITH_RULE`~(4=0)`]
829 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 3`[ARITH_RULE`SUC 3 MOD 4=0/\ SUC 3=4`])
830 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
831 IS_SCS_IN_V_SY_4`0`];
834 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4)<=> (1<= i /\ i<= 4)`]
835 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`4`;`vv:num-> real^3`][ARITH_RULE`~(4=0)`]
836 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
837 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
838 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
839 THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
840 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`)
843 PROVE_E_SY_INV_TAC_4 `4`;
844 PROVE_E_SY_INV_TAC_4 `1`;
845 PROVE_E_SY_INV_TAC_4 `2`;
846 PROVE_E_SY_INV_TAC_4 `3`]]);;
851 let IN_IS_SCS_CASE_4=prove_by_refinement(
852 ` is_scs_v39 s /\ scs_k_v39 s=4 /\ BBs_v39 s vv
853 /\ dimindex(:M)= scs_k_v39 s
854 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 0]:real^3^M= v
855 /\ matvec (v:real^3^M) =a
857 a IN {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v }`
861 REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;IN_ELIM_THM;CONDITION1_SY;CONDITION2_SY;BBs_v39;LET_DEF;LET_END_DEF;change_type_v3;dist]
864 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
865 THEN ASM_REWRITE_TAC[]
868 EXISTS_TAC`v:real^3^M`
869 THEN ASM_REWRITE_TAC[]
872 REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`]
873 THEN REPEAT STRIP_TAC
875 IS_SCS_IN_BALL_ANNULUS_4 `1`;
876 IS_SCS_IN_BALL_ANNULUS_4 `2`;
877 IS_SCS_IN_BALL_ANNULUS_4 `3`;
878 IS_SCS_IN_BALL_ANNULUS_4 `0`];
882 REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`]
885 THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 4==> (i=1\/ i=2\/ i=3 \/ i=4)`)
887 THEN MRESAL_TAC VECTOR_3_4[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=4/\ 2<=4/\ 3<=4/\ 4<=4/\ 4 MOD 4= 0 /\ 1 MOD 4= 1 /\ 2 MOD 4= 2/\ 3 MOD 4= 3/\ ~(2=1)
888 /\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)`;SET_RULE`(a:num) IN (:num)`]
890 THEN REWRITE_TAC[is_scs_v39;periodic2]
892 THEN REPEAT DISCH_TAC
893 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 1`][periodic;ARITH_RULE`~(4=0)`]
894 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
895 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
896 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 1`][periodic;ARITH_RULE`~(4=0)`]
897 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
898 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
899 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 2`][periodic;ARITH_RULE`~(4=0)`]
900 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
901 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
902 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 2`][periodic;ARITH_RULE`~(4=0)`]
903 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
904 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
905 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 3`][periodic;ARITH_RULE`~(4=0)`]
906 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
907 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
908 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 3`][periodic;ARITH_RULE`~(4=0)`]
909 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
910 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
911 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 4`][periodic;ARITH_RULE`~(4=0)`]
912 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
913 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
914 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 4`][periodic;ARITH_RULE`~(4=0)`]
915 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
916 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
917 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 0`][periodic;ARITH_RULE`~(4=0)`]
918 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
919 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
920 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(4=0)`]
921 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
922 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
923 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
924 THEN POP_ASSUM(fun th-> MRESA_TAC th[`0`;`0`]);
926 MP_TAC V_E_FF_IS_SCS_CASES_4
927 THEN ASM_REWRITE_TAC[]
928 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;IN_ELIM_THM;CONDITION1_SY;CONDITION2_SY;BBs_v39;LET_DEF;LET_END_DEF;change_type_v3;dist;IN]
935 let IS_EAR_V25_EQ_EAR_SY=prove(`is_scs_v39 s /\ 3< scs_k_v39 s
936 /\ stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
937 (change_type_v3 (scs_a_v39 s)),
938 (change_type_v3 (scs_b_v39 s)),
939 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
940 (\i. (1 + i) MOD scs_k_v39 s))=s1
942 (is_ear_v39 s <=> ear_sy s1)`,
944 THEN MP_TAC IS_SCS_STABLE_SYSTEM
945 THEN ASM_REWRITE_TAC[]
947 THEN REWRITE_TAC[is_ear_v39;ear_sy]
948 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
949 (change_type_v3 (scs_a_v39 s))`;`
950 (change_type_v3 (scs_b_v39 s))`;`
951 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
952 (\i. (1 + i) MOD scs_k_v39 s)`]
953 THEN MP_TAC (ARITH_RULE`3< scs_k_v39 s==> (scs_k_v39 s - 1 +1)-0= scs_k_v39 s
954 /\ ~(scs_k_v39 s=3)`)
956 THEN MRESAL_TAC HAS_SIZE_NUMSEG[`0`;`scs_k_v39 s -1`][HAS_SIZE]);;
967 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`1 MOD 4=1 /\ SUC 1=2/\ 1+1=2 /\ 2 MOD 4=2/\ 1+2=3 /\ 3 MOD 4=3/\ 1+3=4 /\ 4 MOD 4=0/\ 1+0=1`]
968 THEN REPEAT STRIP_TAC)
971 THEN REWRITE_TAC[ARITH_RULE`1 MOD 4=1 /\ SUC 1=2/\ 1<4/\ ~(1=0)/\ 2<4 /\ 2 MOD 4=2 /\ ~(2=0)/\ SUC 2=3/\ 3<4/\ 3 MOD 4=3 /\ ~(3=0)/\ SUC 3=4/\ 0 MOD 4=0/\ 0<4/\ SUC 0=1`]
973 THEN REWRITE_TAC[periodic;periodic2;is_scs_v39]
974 THEN REPEAT STRIP_TAC
975 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][periodic;ARITH_RULE`1 MOD 4=1 /\ SUC 1=2/\ 1<4/\ ~(4=0)`]
976 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j:num`)
977 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD 4)`][periodic;ARITH_RULE`1 MOD 4=1 /\ SUC 1=2/\ 1<4/\ ~(4=0)`]
978 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i':num`)
979 THEN POP_ASSUM MP_TAC
980 THEN MP_TAC(SET_RULE`{1, 2} = {i' MOD 4, j MOD 4}
981 ==> (1 =i' MOD 4 /\ 2= j MOD 4)\/ (2 =i' MOD 4 /\ 1= j MOD 4)`)
983 THEN MP_TAC(SET_RULE`{2, 3} = {i' MOD 4, j MOD 4}
984 ==> (2 =i' MOD 4 /\ 3= j MOD 4)\/ (3 =i' MOD 4 /\ 2= j MOD 4)`)
986 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 3`][periodic;ARITH_RULE`1 MOD 4=1 /\ SUC 1=2/\ 1<4/\ ~(4=0)`]
987 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`])
988 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
989 THEN ASM_REWRITE_TAC[]
990 THEN MP_TAC(SET_RULE`{3,0} = {i' MOD 4, j MOD 4}
991 ==> (3 =i' MOD 4 /\ 0= j MOD 4)\/ (0 =i' MOD 4 /\ 3= j MOD 4)`)
993 THEN MP_TAC(SET_RULE`{0,1} = {i' MOD 4, j MOD 4}
994 ==> (i' MOD 4=1 /\ j MOD 4=0)\/ (i' MOD 4=0 /\ j MOD 4=1)`)
997 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
998 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
999 THEN MATCH_MP_TAC th)
1000 THEN ASM_REWRITE_TAC[]];;
1003 let EXISTS_SCS_J_TAC=
1004 fun (so:term) (so1:term) (so2:term)->
1006 THEN REWRITE_TAC[ARITH_RULE`0 MOD 4=0/\SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4`]
1009 THEN ASM_REWRITE_TAC[ARITH_RULE`4 MOD 4=0/\ SUC 0=1/\ 1<=4/\ 4<=4/\ 1+0=1/\ 1 MOD 4=1/\ 1<=1/\ 1<=4/\ 1 MOD 4=1/\ 1+1=2/\ ~(1=0)/\ 2 MOD 4=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=4/\ 1+2=3/\ 3 MOD 4=3/\ 1<=3/\ 3<=4/\ 1+3=4/\ SUC 3=4/\ ~(3=0)`]
1012 THEN ASM_REWRITE_TAC[ARITH_RULE`0 MOD 4=0/\ 1 MOD 4=1/\ 2 MOD 4=2/\ 3 MOD 4=3/\ 4 MOD 4=0`]
1018 let TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4=prove_by_refinement(
1019 `is_scs_v39 s /\ scs_k_v39 s=4
1021 /\ dimindex(:M)=scs_k_v39 s
1022 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 0]:real^3^M= v
1023 /\ matvec (v:real^3^M) =a
1024 /\ stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
1025 (change_type_v3 (scs_a_v39 s)),
1026 (change_type_v3 (scs_b_v39 s)),
1027 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
1028 (\i. (1 + i) MOD scs_k_v39 s))=s1
1029 ==> taustar_v39 s vv = tau_star s1 a`
1034 THEN POP_ASSUM MP_TAC
1035 THEN MP_TAC V_E_FF_IS_SCS_CASES_4
1036 THEN ASM_REWRITE_TAC[IN]
1039 THEN MP_TAC IS_SCS_STABLE_SYSTEM
1040 THEN ASM_REWRITE_TAC[ARITH_RULE`3<4`]
1042 THEN ASM_REWRITE_TAC[taustar_v39;tau_star]
1043 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;IN;mk_unadorned_v39;]
1044 THEN ASM_SIMP_TAC[dsv_J_empty]
1046 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
1047 THEN ASM_REWRITE_TAC[REAL_ARITH`A-B=A-C<=>B=C`;dsv_v39;d_fun]
1048 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
1049 (change_type_v3 (scs_a_v39 s))`;`
1050 (change_type_v3 (scs_b_v39 s))`;`
1051 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
1052 (\i. (1 + i) MOD scs_k_v39 s)`]
1053 THEN ASM_REWRITE_TAC[REAL_ARITH`A+B=A+C<=>B=C`;sigma_sy]
1054 THEN MP_TAC IS_EAR_V25_EQ_EAR_SY
1055 THEN ASM_REWRITE_TAC[ARITH_RULE`3<4`]
1057 THEN ASM_REWRITE_TAC[REAL_EQ_MUL_LCANCEL;REAL_ARITH`~(#0.1 = &0)`]
1058 THEN SUBGOAL_THEN`~((if ear_sy s1 then &1 else -- &1) = &0)` ASSUME_TAC;
1060 MP_TAC(SET_RULE`(ear_sy s1)\/ ~(ear_sy s1)`)
1062 THEN REAL_ARITH_TAC;
1064 ASM_REWRITE_TAC[J1_SY ]
1065 THEN MATCH_MP_TAC SUM_EQ_GENERAL
1066 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1067 THEN ABBREV_TAC`h =(\i. if (i MOD 4 = 0) then (4,1)
1068 else (i MOD 4, SUC(i MOD 4)))`
1069 THEN SUBGOAL_THEN`(!x x'.
1070 (x < 4 /\ scs_J_v39 s x (SUC x)) /\
1071 (x' < 4 /\ scs_J_v39 s x' (SUC x')) /\
1072 h x' = (h:num->num #num) x
1073 ==> x = x')` ASSUME_TAC;
1076 THEN POP_ASSUM MP_TAC
1077 THEN MP_TAC(ARITH_RULE` x< 4 ==> x=0\/ x=1\/ x=2 \/ x=3 `)
1079 THEN MP_TAC(ARITH_RULE` x'< 4 ==> x'=0\/ x'=1\/ x'=2 \/ x'=3 `)
1082 THEN REWRITE_TAC[ARITH_RULE`1 MOD 4=1 /\ 0 MOD 4=0/\ 2 MOD 4=2/\ 3 MOD 4=3 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ SUC 1=2/\ ~(1=4)/\ ~(2=4)/\ ~(3=4)`;ARITH_RULE`A=B <=> B=A:num`;PAIR_EQ;DE_MORGAN_THM]
1085 EXISTS_TAC`h:num->(num#num)`
1086 THEN ASM_REWRITE_TAC[change_type_v2;IN_ELIM_THM;IN_NUMSEG]
1088 THEN REPEAT STRIP_TAC;
1090 ASM_REWRITE_TAC[EXISTS_UNIQUE_THM]
1091 THEN MP_TAC(ARITH_RULE`1<= i/\ i<=4 ==> i=1\/ i=2 \/ i=3 \/ i=4`)
1100 THEN MP_TAC(ARITH_RULE`x<4 ==> x=0 \/ x=1 \/ x=2 \/ x=3`)
1103 EXISTS_SCS_J_TAC `4` `0` `1`;
1104 EXISTS_SCS_J_TAC `1` `1` `2`;
1105 EXISTS_SCS_J_TAC `2` `2` `3`;
1106 EXISTS_SCS_J_TAC `3` `3` `4`];
1109 THEN MP_TAC(ARITH_RULE`x<4 ==> x=0 \/ x=1 \/ x=2 \/ x=3`)
1112 THEN REWRITE_TAC[ARITH_RULE`0 MOD 4=0/\ SUC 0=1`]
1114 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
1115 THEN MRESAL_TAC VECTOR_3_4[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 0`][ARITH_RULE`1<=4/\ 2<=4/\ 3<=4/\ 4<=4/\ 4 MOD 4= 0 /\ 1 MOD 4= 1 /\ 2 MOD 4= 2/\ 3 MOD 4= 3/\ ~(2=1)/\ ~(2=0)
1116 /\ ~(3=0)/\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)/\ SUC 1=2/\ SUC 0=1 /\ SUC 2= 3/\ SUC 3=4 /\ SUC 4=5`;SET_RULE`(a:num)IN (:num)`;dist]
1117 THEN REPLICATE_TAC 25 (POP_ASSUM MP_TAC)
1118 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1120 THEN ASM_REWRITE_TAC[IN;BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`]
1121 THEN REPEAT STRIP_TAC
1122 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(4=0)`]
1123 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])]);;
1128 let JKQEWGV1_CASE_4=prove(
1129 `!s vv. is_scs_v39 s /\ scs_k_v39 s=4 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
1130 /\ dimindex(:M)=scs_k_v39 s
1132 (sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
1133 (IMAGE (\i. (vv i,vv (SUC i))) (:num)) < pi)`,
1136 THEN MP_TAC IS_SCS_STABLE_SYSTEM
1138 THEN POP_ASSUM MP_TAC
1139 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<4`]
1141 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
1142 (change_type_v3 (scs_a_v39 s)),
1143 (change_type_v3 (scs_b_v39 s)),
1144 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
1145 (\i. (1 + i) MOD scs_k_v39 s))`
1146 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
1147 (change_type_v3 (scs_a_v39 s))`;`
1148 (change_type_v3 (scs_b_v39 s))`;`
1149 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
1150 (\i. (1 + i) MOD scs_k_v39 s)`]
1151 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 0]:real^3^M`
1152 THEN ABBREV_TAC`a=matvec (v:real^3^M)`
1153 THEN MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4
1155 THEN POP_ASSUM MP_TAC
1156 THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
1158 THEN MP_TAC IN_IS_SCS_CASE_4
1160 THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<4`;]
1161 THEN REMOVE_ASSUM_TAC
1162 THEN POP_ASSUM MP_TAC
1164 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
1165 THEN MP_TAC V_E_FF_IS_SCS_CASES_4
1166 THEN ASM_REWRITE_TAC[IN]
1169 THEN ASM_REWRITE_TAC[is_scs_v39;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;IN;mk_unadorned_v39]
1170 THEN REPEAT RESA_TAC
1171 THEN POP_ASSUM MP_TAC
1172 THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
1174 THEN MP_TAC(REAL_ARITH`pi <=
1175 sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
1176 (IMAGE (\i. vv i,vv (SUC i)) (:num)) \/
1177 sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
1178 (IMAGE (\i. vv i,vv (SUC i)) (:num))< pi`)
1180 THEN REPLICATE_TAC 19 REMOVE_ASSUM_TAC
1181 THEN POP_ASSUM MP_TAC
1182 THEN REAL_ARITH_TAC);;
1186 let IS_SCS_IN_V_SY_5=
1189 THEN MRESAL_TAC VECTOR_3_5[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 4 MOD 5= 4/\ 5 MOD 5=0 /\ 1 MOD 5= 1 /\ 2 MOD 5= 2/\ 3 MOD 5= 3 /\ ~(2=1)/\ SUC 5 MOD 5=1
1190 /\ SUC 4 MOD 5= 0 /\ SUC 1 MOD 5= 2 /\ SUC 2 MOD 5= 3/\ SUC 3 MOD 5= 4/\ ~(3=1)/\ ~(1=0)/\ 5<=5/\ 1<=1 /\ 1<=2 /\ 1<= 3 /\ 1<=4 /\ 1<=5
1191 /\ SUC 1=2 /\ SUC 0 =1/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5 `; SET_RULE`(a:num) IN (:num)`]
1195 let PROVE_E_SY_INV_TAC_5=
1197 MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x':num`;th;`5`][ARITH_RULE`~(5=0)/\ 4 MOD 5=4/\ SUC 0 MOD 5=1/\ 1 MOD 5=1 /\ 2 MOD 5=2 /\ 3 MOD 5=3/\ 5 MOD 5=0`]
1199 THEN MRESAL_TAC VECTOR_3_5[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 4 MOD 5= 4/\ 5 MOD 5=0 /\ 1 MOD 5= 1 /\ 2 MOD 5= 2/\ 3 MOD 5= 3 /\ ~(2=1)/\ SUC 5 MOD 5=1
1200 /\ SUC 4 MOD 5= 0 /\ SUC 1 MOD 5= 2 /\ SUC 2 MOD 5= 3/\ SUC 3 MOD 5= 4/\ ~(3=1)/\ ~(1=0)/\ 5<=5/\ 1<=1 /\ 1<=2 /\ 1<= 3 /\ 1<=4 /\ 1<=5
1201 /\ SUC 1=2 /\ SUC 0 =1/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5 `; SET_RULE`(a:num) IN (:num)`]
1211 let V_E_FF_IS_SCS_CASES_5=prove_by_refinement(
1212 ` is_scs_v39 s /\ scs_k_v39 s=5 /\ vv IN BBs_v39 s
1213 /\ dimindex(:M)=scs_k_v39 s
1214 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 0]:real^3^M= v
1215 /\ matvec (v:real^3^M) =a
1217 V_SY (v:real^3^M)=IMAGE vv (:num)/\
1218 E_SY (v:real^3^M)=IMAGE (\i. {vv i, vv (SUC i)}) (:num)/\
1219 F_SY (v:real^3^M)=IMAGE (\i. vv i,vv (SUC i)) (:num)`,
1224 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1225 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(5<=3)`;IN;mk_unadorned_v39]
1226 THEN REPEAT STRIP_TAC;
1228 REWRITE_TAC[V_SY;rows]
1229 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5)`]
1230 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
1231 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5)`]
1237 IS_SCS_IN_V_SY_5`1`;
1238 IS_SCS_IN_V_SY_5`2`;
1239 IS_SCS_IN_V_SY_5`3`;
1240 IS_SCS_IN_V_SY_5`4`;
1241 IS_SCS_IN_V_SY_5`0`];
1244 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)<=> (1<= i /\ i<= 5)`]
1245 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`5`;`vv:num-> real^3`][ARITH_RULE`~(5=0)`]
1246 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`)
1247 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1248 THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
1249 THEN MP_TAC(ARITH_RULE`x' MOD 5 < 5==> x' MOD 5 =0 \/ x' MOD 5 = 1\/ x' MOD 5 = 2 \/ x' MOD 5 =3\/ x' MOD 5 =4`)
1252 IS_SCS_IN_V_SY_5`5`;
1253 IS_SCS_IN_V_SY_5`1`;
1254 IS_SCS_IN_V_SY_5`2`;
1255 IS_SCS_IN_V_SY_5`3`;
1256 IS_SCS_IN_V_SY_5`4`];
1258 REWRITE_TAC[E_SY;rows]
1259 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
1260 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)`]
1262 THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
1267 IS_SCS_IN_V_SY_5`1`;
1268 IS_SCS_IN_V_SY_5`2`;
1269 IS_SCS_IN_V_SY_5`3`;
1271 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`5`;`vv:num-> real^3`][ARITH_RULE`~(5=0)`]
1272 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 4`[ARITH_RULE`SUC 4 MOD 5=0/\ SUC 4=5`])
1273 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
1274 IS_SCS_IN_V_SY_5`0`];
1277 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5)<=> (1<= i /\ i<= 5)`]
1278 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`5`;`vv:num-> real^3`][ARITH_RULE`~(5=0)`]
1279 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
1280 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1281 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1282 THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
1283 THEN MP_TAC(ARITH_RULE`x' MOD 5 < 5==> x' MOD 5 =0 \/ x' MOD 5 = 1\/ x' MOD 5 = 2 \/ x' MOD 5 =3 \/ x' MOD 5 =4`)
1286 PROVE_E_SY_INV_TAC_5 `5`;
1287 PROVE_E_SY_INV_TAC_5 `1`;
1288 PROVE_E_SY_INV_TAC_5 `2`;
1289 PROVE_E_SY_INV_TAC_5 `3`;
1290 PROVE_E_SY_INV_TAC_5 `4`];
1292 REWRITE_TAC[F_SY;rows]
1293 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
1294 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)`]
1296 THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
1301 IS_SCS_IN_V_SY_5`1`;
1302 IS_SCS_IN_V_SY_5`2`;
1303 IS_SCS_IN_V_SY_5`3`;
1305 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`5`;`vv:num-> real^3`][ARITH_RULE`~(5=0)`]
1306 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 4`[ARITH_RULE`SUC 4 MOD 5=0/\ SUC 4=5`])
1307 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
1308 IS_SCS_IN_V_SY_5`0`];
1311 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5)<=> (1<= i /\ i<= 5)`]
1312 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`5`;`vv:num-> real^3`][ARITH_RULE`~(5=0)`]
1313 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
1314 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1315 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1316 THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
1317 THEN MP_TAC(ARITH_RULE`x' MOD 5 < 5==> x' MOD 5 =0 \/ x' MOD 5 = 1\/ x' MOD 5 = 2 \/ x' MOD 5 =3 \/ x' MOD 5 =4`)
1320 PROVE_E_SY_INV_TAC_5 `5`;
1321 PROVE_E_SY_INV_TAC_5 `1`;
1322 PROVE_E_SY_INV_TAC_5 `2`;
1323 PROVE_E_SY_INV_TAC_5 `3`;
1324 PROVE_E_SY_INV_TAC_5 `4`];
1329 let IS_SCS_IN_BALL_ANNULUS_5=
1331 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1332 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1333 THEN MP_TAC th THEN REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM])
1335 THEN POP_ASSUM MATCH_MP_TAC
1337 THEN MRESAL_TAC VECTOR_3_5[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 4 MOD 5= 4/\ 5 MOD 5=0 /\ 1 MOD 5= 1 /\ 2 MOD 5= 2/\ 3 MOD 5= 3 /\ ~(2=1)/\ SUC 5 MOD 5=1
1338 /\ SUC 4 MOD 5= 0 /\ SUC 1 MOD 5= 2 /\ SUC 2 MOD 5= 3/\ SUC 3 MOD 5= 4/\ ~(3=1)/\ ~(1=0)/\ 5<=5/\ 1<=1 /\ 1<=2 /\ 1<= 3 /\ 1<=4 /\ 1<=5
1339 /\ SUC 1=2 /\ SUC 0 =1/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5 `; SET_RULE`(a:num) IN (:num)`]
1345 let IN_IS_SCS_CASE_5=prove_by_refinement(
1346 ` is_scs_v39 s /\ scs_k_v39 s=5 /\ BBs_v39 s vv
1347 /\ dimindex(:M)= scs_k_v39 s
1348 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 0]:real^3^M= v
1349 /\ matvec (v:real^3^M) =a
1351 a IN {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v }`,
1355 REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;IN_ELIM_THM;CONDITION1_SY;CONDITION2_SY;BBs_v39;LET_DEF;LET_END_DEF;change_type_v3;dist]
1358 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1359 THEN ASM_REWRITE_TAC[]
1362 EXISTS_TAC`v:real^3^M`
1363 THEN ASM_REWRITE_TAC[]
1366 REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)`]
1367 THEN REPEAT STRIP_TAC
1369 IS_SCS_IN_BALL_ANNULUS_5 `1`;
1370 IS_SCS_IN_BALL_ANNULUS_5 `2`;
1371 IS_SCS_IN_BALL_ANNULUS_5 `3`;
1372 IS_SCS_IN_BALL_ANNULUS_5 `4`;
1373 IS_SCS_IN_BALL_ANNULUS_5 `0`];
1377 REWRITE_TAC[ARITH_RULE`(1<=i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)`]
1380 THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 5==> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)`)
1382 THEN MRESAL_TAC VECTOR_3_5[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 4 MOD 5= 4/\ 5 MOD 5=0 /\ 1 MOD 5= 1 /\ 2 MOD 5= 2/\ 3 MOD 5= 3 /\ ~(2=1)/\ SUC 5 MOD 5=1
1383 /\ SUC 4 MOD 5= 0 /\ SUC 1 MOD 5= 2 /\ SUC 2 MOD 5= 3/\ SUC 3 MOD 5= 4/\ ~(3=1)/\ ~(1=0)/\ 5<=5/\ 1<=1 /\ 1<=2 /\ 1<= 3 /\ 1<=4 /\ 1<=5
1384 /\ SUC 1=2 /\ SUC 0 =1/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5 `; SET_RULE`(a:num) IN (:num)`]
1386 THEN REWRITE_TAC[is_scs_v39;periodic2]
1388 THEN REPEAT DISCH_TAC
1389 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 1`][periodic;ARITH_RULE`~(5=0)`]
1390 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1391 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1392 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 1`][periodic;ARITH_RULE`~(5=0)`]
1393 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1394 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1395 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 2`][periodic;ARITH_RULE`~(5=0)`]
1396 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1397 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1398 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 2`][periodic;ARITH_RULE`~(5=0)`]
1399 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1400 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1401 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 3`][periodic;ARITH_RULE`~(5=0)`]
1402 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1403 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1404 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 3`][periodic;ARITH_RULE`~(5=0)`]
1405 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1406 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1407 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 4`][periodic;ARITH_RULE`~(5=0)`]
1408 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1409 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1410 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 4`][periodic;ARITH_RULE`~(5=0)`]
1411 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1412 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1413 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 5`][periodic;ARITH_RULE`~(5=0)`]
1414 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1415 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1416 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 5`][periodic;ARITH_RULE`~(5=0)`]
1417 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1418 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1419 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 0`][periodic;ARITH_RULE`~(5=0)`]
1420 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1421 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
1422 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(5=0)`]
1423 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1424 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
1425 THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
1426 THEN POP_ASSUM(fun th-> MRESA_TAC th[`0`;`0`]);
1428 MP_TAC V_E_FF_IS_SCS_CASES_5
1429 THEN ASM_REWRITE_TAC[]
1430 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;IN_ELIM_THM;CONDITION1_SY;CONDITION2_SY;BBs_v39;LET_DEF;LET_END_DEF;change_type_v3;dist;IN]
1440 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`1 MOD 5=1 /\ SUC 1=2/\ 1+1=2 /\ 2 MOD 5=2/\ 1+2=3 /\ 3 MOD 5=3/\ 1+3=4 /\ 5 MOD 5=0/\ 1+0=1/\ 1+4=5 /\ 4 MOD 5=4`]
1441 THEN REPEAT STRIP_TAC)
1444 THEN REWRITE_TAC[ARITH_RULE`1 MOD 5=1 /\ SUC 1=2/\ 1<5/\ ~(1=0)/\ 2<5 /\ 2 MOD 5=2 /\ ~(2=0)/\ SUC 2=3/\ 3<5/\ 3 MOD 5=3 /\ ~(3=0)/\ SUC 3=4/\ 0 MOD 5=0/\ 0<5/\ SUC 0=1/\4<5 /\ SUC 4=5/\ ~(4=0)/\ 4 MOD 5=4`]
1446 THEN REWRITE_TAC[periodic;periodic2;is_scs_v39]
1447 THEN REPEAT STRIP_TAC
1448 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][periodic;ARITH_RULE`1 MOD 5=1 /\ SUC 1=2/\ 1<5/\ ~(5=0)`]
1449 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j:num`)
1450 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD 5)`][periodic;ARITH_RULE`1 MOD 5=1 /\ SUC 1=2/\ 1<5/\ ~(5=0)`]
1451 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i':num`)
1452 THEN POP_ASSUM MP_TAC
1453 THEN MP_TAC(SET_RULE`{1, 2} = {i' MOD 5, j MOD 5}
1454 ==> (1 =i' MOD 5 /\ 2= j MOD 5)\/ (2 =i' MOD 5 /\ 1= j MOD 5)`)
1456 THEN MP_TAC(SET_RULE`{2, 3} = {i' MOD 5, j MOD 5}
1457 ==> (2 =i' MOD 5 /\ 3= j MOD 5)\/ (3 =i' MOD 5 /\ 2= j MOD 5)`)
1459 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 4`][periodic;ARITH_RULE`1 MOD 5=1 /\ SUC 1=2/\ 1<5/\ ~(5=0)`]
1460 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`])
1461 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
1462 THEN ASM_REWRITE_TAC[]
1463 THEN MP_TAC(SET_RULE`{3,4} = {i' MOD 5, j MOD 5}
1464 ==> (3 =i' MOD 5 /\ 4= j MOD 5)\/ (4 =i' MOD 5 /\ 3= j MOD 5)`)
1466 THEN MP_TAC(SET_RULE`{4,0} = {i' MOD 5, j MOD 5}
1467 ==> (4=i' MOD 5 /\ 0=j MOD 5)\/ (0=i' MOD 5 /\ 4=j MOD 5)`)
1469 THEN MP_TAC(SET_RULE`{0,1} = {i' MOD 5, j MOD 5}
1470 ==> (i' MOD 5=1 /\ j MOD 5=0)\/ (i' MOD 5=0 /\ j MOD 5=1)`)
1473 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
1474 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1475 THEN MATCH_MP_TAC th)
1476 THEN ASM_REWRITE_TAC[]];;
1482 let EXISTS_SCS_J_TAC=
1483 fun (so:term) (so1:term) (so2:term)->
1485 THEN REWRITE_TAC[ARITH_RULE`0 MOD 5=0/\SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5`]
1488 THEN ASM_REWRITE_TAC[ARITH_RULE`5 MOD 5=0/\ SUC 0=1/\ 1<=5/\ 5<=5/\ 1+0=1/\ 1 MOD 5=1/\ 1<=1/\ 1<=5/\ 1 MOD 5=1/\ 1+1=2/\ ~(1=0)/\ 2 MOD 5=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=5/\ 1+2=3/\ 3 MOD 5=3/\ 1<=3/\ 3<=5/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ ~(4=0)/\ 1<=4/\ 4<=5/\ SUC 4=5/\ 4 MOD 5=4/\ 1+4=5`]
1491 THEN ASM_REWRITE_TAC[ARITH_RULE`0 MOD 5=0/\ 1 MOD 5=1/\ 2 MOD 5=2/\ 3 MOD 5=3/\ 5 MOD 5=0/\ 4 MOD 5=4`]
1498 let TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5=prove_by_refinement(
1499 `is_scs_v39 s /\ scs_k_v39 s=5
1501 /\ dimindex(:M)=scs_k_v39 s
1502 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 0]:real^3^M= v
1503 /\ matvec (v:real^3^M) =a
1504 /\ stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
1505 (change_type_v3 (scs_a_v39 s)),
1506 (change_type_v3 (scs_b_v39 s)),
1507 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
1508 (\i. (1 + i) MOD scs_k_v39 s))=s1
1509 ==> taustar_v39 s vv = tau_star s1 a`,
1513 THEN POP_ASSUM MP_TAC
1514 THEN MP_TAC V_E_FF_IS_SCS_CASES_5
1515 THEN ASM_REWRITE_TAC[IN]
1518 THEN MP_TAC IS_SCS_STABLE_SYSTEM
1519 THEN ASM_REWRITE_TAC[ARITH_RULE`3<5`]
1521 THEN ASM_REWRITE_TAC[taustar_v39;tau_star]
1522 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(5<=3)`;IN;mk_unadorned_v39;]
1523 THEN ASM_SIMP_TAC[dsv_J_empty]
1525 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
1526 THEN ASM_REWRITE_TAC[REAL_ARITH`A-B=A-C<=>B=C`;dsv_v39;d_fun]
1527 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
1528 (change_type_v3 (scs_a_v39 s))`;`
1529 (change_type_v3 (scs_b_v39 s))`;`
1530 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
1531 (\i. (1 + i) MOD scs_k_v39 s)`]
1532 THEN ASM_REWRITE_TAC[REAL_ARITH`A+B=A+C<=>B=C`;sigma_sy]
1533 THEN MP_TAC IS_EAR_V25_EQ_EAR_SY
1534 THEN ASM_REWRITE_TAC[ARITH_RULE`3<5`]
1536 THEN ASM_REWRITE_TAC[REAL_EQ_MUL_LCANCEL;REAL_ARITH`~(#0.1 = &0)`]
1537 THEN SUBGOAL_THEN`~((if ear_sy s1 then &1 else -- &1) = &0)` ASSUME_TAC;
1539 MP_TAC(SET_RULE`(ear_sy s1)\/ ~(ear_sy s1)`)
1541 THEN REAL_ARITH_TAC;
1543 ASM_REWRITE_TAC[J1_SY ]
1544 THEN MATCH_MP_TAC SUM_EQ_GENERAL
1545 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1546 THEN ABBREV_TAC`h =(\i. if (i MOD 5 = 0) then (5,1)
1547 else (i MOD 5, SUC(i MOD 5)))`
1548 THEN SUBGOAL_THEN`(!x x'.
1549 (x < 5 /\ scs_J_v39 s x (SUC x)) /\
1550 (x' < 5 /\ scs_J_v39 s x' (SUC x')) /\
1551 h x' = (h:num->num #num) x
1552 ==> x = x')` ASSUME_TAC;
1555 THEN POP_ASSUM MP_TAC
1556 THEN MP_TAC(ARITH_RULE` x< 5 ==> x=0\/ x=1\/ x=2 \/ x=3\/ x=4 `)
1558 THEN MP_TAC(ARITH_RULE` x'< 5 ==> x'=0\/ x'=1\/ x'=2 \/ x'=3 \/ x'=4`)
1561 THEN REWRITE_TAC[ARITH_RULE`1 MOD 5=1 /\ 0 MOD 5=0/\ 2 MOD 5=2/\ 3 MOD 5=3 /\ 4 MOD 5=4/\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(4=0)/\ SUC 1=2/\ ~(1=5)/\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`;ARITH_RULE`A=B <=> B=A:num`;PAIR_EQ;DE_MORGAN_THM]
1564 EXISTS_TAC`h:num->(num#num)`
1565 THEN ASM_REWRITE_TAC[change_type_v2;IN_ELIM_THM;IN_NUMSEG]
1567 THEN REPEAT STRIP_TAC;
1569 ASM_REWRITE_TAC[EXISTS_UNIQUE_THM]
1570 THEN MP_TAC(ARITH_RULE`1<= i/\ i<=5 ==> i=1\/ i=2 \/ i=3 \/ i=4 \/i=5 `)
1580 THEN MP_TAC(ARITH_RULE`x<5 ==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4`)
1583 EXISTS_SCS_J_TAC `5` `0` `1`;
1584 EXISTS_SCS_J_TAC `1` `1` `2`;
1585 EXISTS_SCS_J_TAC `2` `2` `3`;
1586 EXISTS_SCS_J_TAC `3` `3` `4`;
1587 EXISTS_SCS_J_TAC `4` `4` `5`];
1590 THEN MP_TAC(ARITH_RULE`x<5 ==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4`)
1593 THEN REWRITE_TAC[ARITH_RULE`0 MOD 5=0/\ SUC 0=1`]
1595 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
1596 THEN MRESAL_TAC VECTOR_3_5[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 4 MOD 5= 4/\ 5 MOD 5=0 /\ 1 MOD 5= 1 /\ 2 MOD 5= 2/\ 3 MOD 5= 3 /\ ~(2=1)/\ SUC 5 MOD 5=1/\ ~(2=0) /\ ~(3=0)/\ ~(4=0)
1597 /\ SUC 4 MOD 5= 0 /\ SUC 1 MOD 5= 2 /\ SUC 2 MOD 5= 3/\ SUC 3 MOD 5= 4/\ ~(3=1)/\ ~(1=0)/\ 5<=5/\ 1<=1 /\ 1<=2 /\ 1<= 3 /\ 1<=4 /\ 1<=5
1598 /\ SUC 1=2 /\ SUC 0 =1/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5 `; SET_RULE`(a:num) IN (:num)`;dist]
1599 THEN REPLICATE_TAC 26 (POP_ASSUM MP_TAC)
1600 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1602 THEN ASM_REWRITE_TAC[IN;BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`]
1603 THEN REPEAT STRIP_TAC
1604 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(5=0)`]
1605 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`]);]);;
1610 let JKQEWGV1_CASE_5=prove(`!s vv. is_scs_v39 s /\ scs_k_v39 s=5 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
1611 /\ dimindex(:M)=scs_k_v39 s
1613 (sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
1614 (IMAGE (\i. (vv i,vv (SUC i))) (:num)) < pi)`,
1617 THEN MP_TAC IS_SCS_STABLE_SYSTEM
1619 THEN POP_ASSUM MP_TAC
1620 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<5`]
1622 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
1623 (change_type_v3 (scs_a_v39 s)),
1624 (change_type_v3 (scs_b_v39 s)),
1625 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
1626 (\i. (1 + i) MOD scs_k_v39 s))`
1627 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
1628 (change_type_v3 (scs_a_v39 s))`;`
1629 (change_type_v3 (scs_b_v39 s))`;`
1630 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
1631 (\i. (1 + i) MOD scs_k_v39 s)`]
1632 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 0]:real^3^M`
1633 THEN ABBREV_TAC`a=matvec (v:real^3^M)`
1634 THEN MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5
1636 THEN POP_ASSUM MP_TAC
1637 THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
1639 THEN MP_TAC IN_IS_SCS_CASE_5
1641 THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<5`;]
1642 THEN REMOVE_ASSUM_TAC
1643 THEN POP_ASSUM MP_TAC
1645 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
1646 THEN MP_TAC V_E_FF_IS_SCS_CASES_5
1647 THEN ASM_REWRITE_TAC[IN]
1650 THEN ASM_REWRITE_TAC[is_scs_v39;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(5<=3)`;IN;mk_unadorned_v39]
1651 THEN REPEAT RESA_TAC
1652 THEN POP_ASSUM MP_TAC
1653 THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
1655 THEN MP_TAC(REAL_ARITH`pi <=
1656 sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
1657 (IMAGE (\i. vv i,vv (SUC i)) (:num)) \/
1658 sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
1659 (IMAGE (\i. vv i,vv (SUC i)) (:num))< pi`)
1661 THEN REPLICATE_TAC 19 REMOVE_ASSUM_TAC
1662 THEN POP_ASSUM MP_TAC
1663 THEN REAL_ARITH_TAC);;
1668 let IS_SCS_IN_V_SY_6=
1671 THEN MRESAL_TAC VECTOR_3_6[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 5`;`(vv:num->real^3) 0`][ARITH_RULE`1<=6/\ 2<=6/\ 3<=6/\ 4<=6/\ 5<=6 /\ 6<=6 /\ 0 MOD 6= 0 /\ 1 MOD 6= 1 /\ 2 MOD 6= 2/\ 3 MOD 6= 3 /\ 4 MOD 6= 4 /\ 5 MOD 6=5 /\ 6 MOD 6=0 /\ ~(2=1)
1672 /\ SUC 0 MOD 6= 1 /\ SUC 1 MOD 6= 2 /\ SUC 2 MOD 6= 3/\ SUC 3 MOD 6= 4
1673 /\ SUC 4 MOD 6= 5 /\ SUC 5 MOD 6 = 0 /\ SUC 6 MOD 6 =1 /\ ~(3=1)/\ ~(1=0)
1674 /\ 1<=1 /\1<=2/\ 1<=3/\ 1<=4/\1<=5
1675 /\ SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`; SET_RULE`(a:num) IN (:num)`]
1679 let PROVE_E_SY_INV_TAC_6=
1681 MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x':num`;th;`6`][ARITH_RULE`~(6=0)/\ 4 MOD 6=4/\ SUC 0 MOD 6=1/\ 1 MOD 6=1 /\ 2 MOD 6=2 /\ 3 MOD 6=3/\ 6 MOD 6=0/\ 5 MOD 6=5`]
1683 THEN MRESAL_TAC VECTOR_3_6[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 5`;`(vv:num->real^3) 0`][ARITH_RULE`1<=6/\ 2<=6/\ 3<=6/\ 4<=6/\ 5<=6 /\ 6<=6 /\ 0 MOD 6= 0 /\ 1 MOD 6= 1 /\ 2 MOD 6= 2/\ 3 MOD 6= 3 /\ 4 MOD 6= 4 /\ 5 MOD 6=5 /\ 6 MOD 6=0 /\ ~(2=1)
1684 /\ SUC 0 MOD 6= 1 /\ SUC 1 MOD 6= 2 /\ SUC 2 MOD 6= 3/\ SUC 3 MOD 6= 4
1685 /\ SUC 4 MOD 6= 5 /\ SUC 5 MOD 6 = 0 /\ SUC 6 MOD 6 =1 /\ ~(3=1)/\ ~(1=0)
1686 /\ 1<=1 /\1<=2/\ 1<=3/\ 1<=4/\1<=5
1687 /\ SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`; SET_RULE`(a:num) IN (:num)`]
1697 let V_E_FF_IS_SCS_CASES_6=prove_by_refinement(
1698 ` is_scs_v39 s /\ scs_k_v39 s=6 /\ vv IN BBs_v39 s
1699 /\ dimindex(:M)=scs_k_v39 s
1700 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 5;(vv:num->real^3) 0]:real^3^M= v
1701 /\ matvec (v:real^3^M) =a
1703 V_SY (v:real^3^M)=IMAGE vv (:num)/\
1704 E_SY (v:real^3^M)=IMAGE (\i. {vv i, vv (SUC i)}) (:num)/\
1705 F_SY (v:real^3^M)=IMAGE (\i. vv i,vv (SUC i)) (:num)`,
1709 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1710 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`;IN;mk_unadorned_v39]
1711 THEN REPEAT STRIP_TAC;
1713 REWRITE_TAC[V_SY;rows]
1714 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5\/ i=6)`]
1715 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
1716 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5\/ i=6)`]
1722 IS_SCS_IN_V_SY_6`1`;
1723 IS_SCS_IN_V_SY_6`2`;
1724 IS_SCS_IN_V_SY_6`3`;
1725 IS_SCS_IN_V_SY_6`4`;
1726 IS_SCS_IN_V_SY_6`5`;
1727 IS_SCS_IN_V_SY_6`0`];
1730 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)<=> (1<= i /\ i<= 6)`]
1731 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`6`;`vv:num-> real^3`][ARITH_RULE`~(6=0)`]
1732 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`)
1733 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1734 THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
1735 THEN MP_TAC(ARITH_RULE`x' MOD 6 < 6==> x' MOD 6 =0 \/ x' MOD 6 = 1\/ x' MOD 6 = 2 \/ x' MOD 6 =3\/ x' MOD 6 =4\/ x' MOD 6=5`)
1738 IS_SCS_IN_V_SY_6`6`;
1739 IS_SCS_IN_V_SY_6`1`;
1740 IS_SCS_IN_V_SY_6`2`;
1741 IS_SCS_IN_V_SY_6`3`;
1742 IS_SCS_IN_V_SY_6`4`;
1743 IS_SCS_IN_V_SY_6`5`];
1745 REWRITE_TAC[E_SY;rows]
1746 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
1747 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)`]
1749 THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
1754 IS_SCS_IN_V_SY_6`1`;
1755 IS_SCS_IN_V_SY_6`2`;
1756 IS_SCS_IN_V_SY_6`3`;
1757 IS_SCS_IN_V_SY_6`4`;
1759 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`6`;`vv:num-> real^3`][ARITH_RULE`~(6=0)`]
1760 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 5`[ARITH_RULE`SUC 5 MOD 6=0/\ SUC 5=6`])
1761 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
1762 IS_SCS_IN_V_SY_6`0`];
1765 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5\/ i=6)<=> (1<= i /\ i<= 6)`]
1766 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`6`;`vv:num-> real^3`][ARITH_RULE`~(6=0)`]
1767 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
1768 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1769 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1770 THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
1771 THEN MP_TAC(ARITH_RULE`x' MOD 6 < 6==> x' MOD 6 =0 \/ x' MOD 6 = 1\/ x' MOD 6 = 2 \/ x' MOD 6 =3 \/ x' MOD 6 =4\/ x' MOD 6=5`)
1774 PROVE_E_SY_INV_TAC_6 `6`;
1775 PROVE_E_SY_INV_TAC_6 `1`;
1776 PROVE_E_SY_INV_TAC_6 `2`;
1777 PROVE_E_SY_INV_TAC_6 `3`;
1778 PROVE_E_SY_INV_TAC_6 `4`;
1779 PROVE_E_SY_INV_TAC_6 `5`;];
1781 REWRITE_TAC[F_SY;rows]
1782 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
1783 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)`]
1785 THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
1790 IS_SCS_IN_V_SY_6`1`;
1791 IS_SCS_IN_V_SY_6`2`;
1792 IS_SCS_IN_V_SY_6`3`;
1793 IS_SCS_IN_V_SY_6`4`;
1795 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`6`;`vv:num-> real^3`][ARITH_RULE`~(6=0)`]
1796 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 5`[ARITH_RULE`SUC 5 MOD 6=0/\ SUC 5=6`])
1797 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
1798 IS_SCS_IN_V_SY_6`0`];
1801 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5\/ i=6)<=> (1<= i /\ i<= 6)`]
1802 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`6`;`vv:num-> real^3`][ARITH_RULE`~(6=0)`]
1803 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
1804 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1805 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1806 THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
1807 THEN MP_TAC(ARITH_RULE`x' MOD 6 < 6==> x' MOD 6 =0 \/ x' MOD 6 = 1\/ x' MOD 6 = 2 \/ x' MOD 6 =3 \/ x' MOD 6 =4\/ x' MOD 6=5`)
1810 PROVE_E_SY_INV_TAC_6 `6`;
1811 PROVE_E_SY_INV_TAC_6 `1`;
1812 PROVE_E_SY_INV_TAC_6 `2`;
1813 PROVE_E_SY_INV_TAC_6 `3`;
1814 PROVE_E_SY_INV_TAC_6 `4`;
1815 PROVE_E_SY_INV_TAC_6 `5`;]]);;
1822 let IS_SCS_IN_BALL_ANNULUS_6=
1824 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1825 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1826 THEN MP_TAC th THEN REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM])
1828 THEN POP_ASSUM MATCH_MP_TAC
1830 THEN MRESAL_TAC VECTOR_3_6[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 5`;`(vv:num->real^3) 0`][ARITH_RULE`1<=6/\ 2<=6/\ 3<=6/\ 4<=6/\ 5<=6 /\ 6<=6 /\ 0 MOD 6= 0 /\ 1 MOD 6= 1 /\ 2 MOD 6= 2/\ 3 MOD 6= 3 /\ 4 MOD 6= 4 /\ 5 MOD 6=5 /\ 6 MOD 6=0 /\ ~(2=1)
1831 /\ SUC 0 MOD 6= 1 /\ SUC 1 MOD 6= 2 /\ SUC 2 MOD 6= 3/\ SUC 3 MOD 6= 4
1832 /\ SUC 4 MOD 6= 5 /\ SUC 5 MOD 6 = 0 /\ SUC 6 MOD 6 =1 /\ ~(3=1)/\ ~(1=0)
1833 /\ 1<=1 /\1<=2/\ 1<=3/\ 1<=4/\1<=5
1834 /\ SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`; SET_RULE`(a:num) IN (:num)`]
1840 let IN_IS_SCS_CASE_6=prove_by_refinement(
1841 ` is_scs_v39 s /\ scs_k_v39 s=6 /\ BBs_v39 s vv
1842 /\ dimindex(:M)= scs_k_v39 s
1843 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 5;(vv:num->real^3) 0]:real^3^M= v
1844 /\ matvec (v:real^3^M) =a
1846 a IN {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v }`,
1849 REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;IN_ELIM_THM;CONDITION1_SY;CONDITION2_SY;BBs_v39;LET_DEF;LET_END_DEF;change_type_v3;dist]
1852 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1853 THEN ASM_REWRITE_TAC[]
1856 EXISTS_TAC`v:real^3^M`
1857 THEN ASM_REWRITE_TAC[]
1860 REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)`]
1861 THEN REPEAT STRIP_TAC
1863 IS_SCS_IN_BALL_ANNULUS_6 `1`;
1864 IS_SCS_IN_BALL_ANNULUS_6 `2`;
1865 IS_SCS_IN_BALL_ANNULUS_6 `3`;
1866 IS_SCS_IN_BALL_ANNULUS_6 `4`;
1867 IS_SCS_IN_BALL_ANNULUS_6 `5`;
1868 IS_SCS_IN_BALL_ANNULUS_6 `0`];
1872 REWRITE_TAC[ARITH_RULE`(1<=i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)`]
1875 THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 6==> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)`)
1877 THEN MRESAL_TAC VECTOR_3_6[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 5`;`(vv:num->real^3) 0`][ARITH_RULE`1<=6/\ 2<=6/\ 3<=6/\ 4<=6/\ 5<=6 /\ 6<=6 /\ 0 MOD 6= 0 /\ 1 MOD 6= 1 /\ 2 MOD 6= 2/\ 3 MOD 6= 3 /\ 4 MOD 6= 4 /\ 5 MOD 6=5 /\ 6 MOD 6=0 /\ ~(2=1)
1878 /\ SUC 0 MOD 6= 1 /\ SUC 1 MOD 6= 2 /\ SUC 2 MOD 6= 3/\ SUC 3 MOD 6= 4
1879 /\ SUC 4 MOD 6= 5 /\ SUC 5 MOD 6 = 0 /\ SUC 6 MOD 6 =1 /\ ~(3=1)/\ ~(1=0)
1880 /\ 1<=1 /\1<=2/\ 1<=3/\ 1<=4/\1<=5
1881 /\ SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`; SET_RULE`(a:num) IN (:num)`]
1883 THEN REWRITE_TAC[is_scs_v39;periodic2]
1885 THEN REPEAT DISCH_TAC
1886 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 1`][periodic;ARITH_RULE`~(6=0)`]
1887 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1888 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1889 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 1`][periodic;ARITH_RULE`~(6=0)`]
1890 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1891 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1892 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 2`][periodic;ARITH_RULE`~(6=0)`]
1893 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1894 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1895 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 2`][periodic;ARITH_RULE`~(6=0)`]
1896 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1897 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1898 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 3`][periodic;ARITH_RULE`~(6=0)`]
1899 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1900 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1901 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 3`][periodic;ARITH_RULE`~(6=0)`]
1902 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1903 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1904 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 4`][periodic;ARITH_RULE`~(6=0)`]
1905 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1906 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1907 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 4`][periodic;ARITH_RULE`~(6=0)`]
1908 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1909 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1910 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 5`][periodic;ARITH_RULE`~(6=0)`]
1911 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1912 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1913 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 5`][periodic;ARITH_RULE`~(6=0)`]
1914 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1915 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1916 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 6`][periodic;ARITH_RULE`~(6=0)`]
1917 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1918 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1919 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 6`][periodic;ARITH_RULE`~(6=0)`]
1920 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1921 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1922 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 0`][periodic;ARITH_RULE`~(6=0)`]
1923 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1924 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
1925 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(6=0)`]
1926 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1927 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
1928 THEN REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
1929 THEN POP_ASSUM(fun th-> MRESA_TAC th[`0`;`0`]);
1931 MP_TAC V_E_FF_IS_SCS_CASES_6
1932 THEN ASM_REWRITE_TAC[]
1933 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;IN_ELIM_THM;CONDITION1_SY;CONDITION2_SY;BBs_v39;LET_DEF;LET_END_DEF;change_type_v3;dist;IN]
1943 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`1 MOD 6=1 /\ SUC 1=2/\ 1+1=2 /\ 2 MOD 6=2/\ 1+2=3 /\ 3 MOD 6=3/\ 1+3=4 /\ 6 MOD 6=0/\ 1+0=1/\ 1+4=5 /\ 4 MOD 6=4/\ 1+5=6/\ 5 MOD 6=5`]
1944 THEN REPEAT STRIP_TAC)
1947 THEN REWRITE_TAC[ARITH_RULE`1 MOD 6=1 /\ SUC 1=2/\ 1<6/\ ~(1=0)/\ 2<6 /\ 2 MOD 6=2 /\ ~(2=0)/\ SUC 2=3/\ 3<6/\ 3 MOD 6=3 /\ ~(3=0)/\ SUC 3=4/\ 0 MOD 6=0/\ 0<6/\ SUC 0=1/\4<6 /\ SUC 4=5/\ ~(4=0)/\ 4 MOD 6=4/\ SUC 5=6/\ ~(5=0)/\ 5 MOD 6=5/\ 5<6`]
1949 THEN REWRITE_TAC[periodic;periodic2;is_scs_v39]
1950 THEN REPEAT STRIP_TAC
1951 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][periodic;ARITH_RULE`1 MOD 6=1 /\ SUC 1=2/\ 1<6/\ ~(6=0)`]
1952 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j:num`)
1953 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD 6)`][periodic;ARITH_RULE`1 MOD 6=1 /\ SUC 1=2/\ 1<6/\ ~(6=0)`]
1954 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i':num`)
1955 THEN POP_ASSUM MP_TAC
1956 THEN MP_TAC(SET_RULE`{1, 2} = {i' MOD 6, j MOD 6}
1957 ==> (1 =i' MOD 6 /\ 2= j MOD 6)\/ (2 =i' MOD 6 /\ 1= j MOD 6)`)
1959 THEN MP_TAC(SET_RULE`{2, 3} = {i' MOD 6, j MOD 6}
1960 ==> (2 =i' MOD 6 /\ 3= j MOD 6)\/ (3 =i' MOD 6 /\ 2= j MOD 6)`)
1962 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 5`][periodic;ARITH_RULE`1 MOD 6=1 /\ SUC 1=2/\ 1<6/\ ~(6=0)`]
1963 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`])
1964 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
1965 THEN ASM_REWRITE_TAC[]
1966 THEN MP_TAC(SET_RULE`{3,4} = {i' MOD 6, j MOD 6}
1967 ==> (3 =i' MOD 6 /\ 4= j MOD 6)\/ (4 =i' MOD 6 /\ 3= j MOD 6)`)
1969 THEN MP_TAC(SET_RULE`{4,5} = {i' MOD 6, j MOD 6}
1970 ==> (4=i' MOD 6 /\ 5=j MOD 6)\/ (5=i' MOD 6 /\ 4=j MOD 6)`)
1972 THEN MP_TAC(SET_RULE`{5,0} = {i' MOD 6, j MOD 6}
1973 ==> (5=i' MOD 6 /\ 0=j MOD 6)\/ (0=i' MOD 6 /\ 5=j MOD 6)`)
1975 THEN MP_TAC(SET_RULE`{0,1} = {i' MOD 6, j MOD 6}
1976 ==> (i' MOD 6=1 /\ j MOD 6=0)\/ (i' MOD 6=0 /\ j MOD 6=1)`)
1979 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
1980 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1981 THEN MATCH_MP_TAC th)
1982 THEN ASM_REWRITE_TAC[]];;
1993 let EXISTS_SCS_J_TAC=
1994 fun (so:term) (so1:term) (so2:term)->
1996 THEN REWRITE_TAC[ARITH_RULE`0 MOD 6=0/\SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`]
1999 THEN ASM_REWRITE_TAC[ARITH_RULE`6 MOD 6=0/\ SUC 0=1/\ 1<=6/\ 6<=6/\ 1+0=1/\ 1 MOD 6=1/\ 1<=1/\ 1<=6/\ 1 MOD 6=1/\ 1+1=2/\ ~(1=0)/\ 2 MOD 6=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=6/\ 1+2=3/\ 3 MOD 6=3/\ 1<=3/\ 3<=6/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ ~(4=0)/\ 1<=4/\ 4<=6/\ SUC 4=5/\ 4 MOD 6=4/\ 1+4=5
2000 /\ ~(5=0)/\ 1<=5/\ 5<=6/\ SUC 5=6/\ 5 MOD 6=5/\ 1+5=6`]
2003 THEN ASM_REWRITE_TAC[ARITH_RULE`0 MOD 6=0/\ 1 MOD 6=1/\ 2 MOD 6=2/\ 3 MOD 6=3/\ 6 MOD 6=0/\ 4 MOD 6=4/\ 5 MOD 6=5`]
2016 let TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6=prove_by_refinement(
2017 `is_scs_v39 s /\ scs_k_v39 s=6
2019 /\ dimindex(:M)=scs_k_v39 s
2020 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 5;(vv:num->real^3) 0]:real^3^M= v
2021 /\ matvec (v:real^3^M) =a
2022 /\ stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
2023 (change_type_v3 (scs_a_v39 s)),
2024 (change_type_v3 (scs_b_v39 s)),
2025 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
2026 (\i. (1 + i) MOD scs_k_v39 s))=s1
2027 ==> taustar_v39 s vv = tau_star s1 a`,
2031 THEN POP_ASSUM MP_TAC
2032 THEN MP_TAC V_E_FF_IS_SCS_CASES_6
2033 THEN ASM_REWRITE_TAC[IN]
2036 THEN MP_TAC IS_SCS_STABLE_SYSTEM
2037 THEN ASM_REWRITE_TAC[ARITH_RULE`3<6`]
2039 THEN ASM_REWRITE_TAC[taustar_v39;tau_star]
2040 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`;IN;mk_unadorned_v39;]
2041 THEN ASM_SIMP_TAC[dsv_J_empty]
2043 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
2044 THEN ASM_REWRITE_TAC[REAL_ARITH`A-B=A-C<=>B=C`;dsv_v39;d_fun]
2045 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
2046 (change_type_v3 (scs_a_v39 s))`;`
2047 (change_type_v3 (scs_b_v39 s))`;`
2048 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
2049 (\i. (1 + i) MOD scs_k_v39 s)`]
2050 THEN ASM_REWRITE_TAC[REAL_ARITH`A+B=A+C<=>B=C`;sigma_sy]
2051 THEN MP_TAC IS_EAR_V25_EQ_EAR_SY
2052 THEN ASM_REWRITE_TAC[ARITH_RULE`3<6`]
2054 THEN ASM_REWRITE_TAC[REAL_EQ_MUL_LCANCEL;REAL_ARITH`~(#0.1 = &0)`]
2055 THEN SUBGOAL_THEN`~((if ear_sy s1 then &1 else -- &1) = &0)` ASSUME_TAC;
2057 MP_TAC(SET_RULE`(ear_sy s1)\/ ~(ear_sy s1)`)
2059 THEN REAL_ARITH_TAC;
2061 ASM_REWRITE_TAC[J1_SY ]
2062 THEN MATCH_MP_TAC SUM_EQ_GENERAL
2063 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
2064 THEN ABBREV_TAC`h =(\i. if (i MOD 6 = 0) then (6,1)
2065 else (i MOD 6, SUC(i MOD 6)))`
2066 THEN SUBGOAL_THEN`(!x x'.
2067 (x < 6 /\ scs_J_v39 s x (SUC x)) /\
2068 (x' < 6 /\ scs_J_v39 s x' (SUC x')) /\
2069 h x' = (h:num->num #num) x
2070 ==> x = x')` ASSUME_TAC;
2073 THEN POP_ASSUM MP_TAC
2074 THEN MP_TAC(ARITH_RULE` x< 6 ==> x=0\/ x=1\/ x=2 \/ x=3\/ x=4\/ x=5 `)
2076 THEN MP_TAC(ARITH_RULE` x'< 6 ==> x'=0\/ x'=1\/ x'=2 \/ x'=3 \/ x'=4\/ x'=5`)
2079 THEN REWRITE_TAC[ARITH_RULE`1 MOD 6=1 /\ 0 MOD 6=0/\ 2 MOD 6=2/\ 3 MOD 6=3 /\ 4 MOD 6=4/\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(4=0)/\ SUC 1=2/\ ~(1=6)/\ ~(2=6)/\ ~(3=6)/\ ~(4=6)/\ ~(5=0)/\ 5 MOD 6=5 /\ SUC 5=6`;ARITH_RULE`A=B <=> B=A:num`;PAIR_EQ;DE_MORGAN_THM]
2082 EXISTS_TAC`h:num->(num#num)`
2083 THEN ASM_REWRITE_TAC[change_type_v2;IN_ELIM_THM;IN_NUMSEG]
2085 THEN REPEAT STRIP_TAC;
2087 ASM_REWRITE_TAC[EXISTS_UNIQUE_THM]
2088 THEN MP_TAC(ARITH_RULE`1<= i/\ i<=6 ==> i=1\/ i=2 \/ i=3 \/ i=4 \/i=5 \/ i=6`)
2099 THEN MP_TAC(ARITH_RULE`x<6 ==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4\/ x=5`)
2102 EXISTS_SCS_J_TAC `6` `0` `1`;
2103 EXISTS_SCS_J_TAC `1` `1` `2`;
2104 EXISTS_SCS_J_TAC `2` `2` `3`;
2105 EXISTS_SCS_J_TAC `3` `3` `4`;
2106 EXISTS_SCS_J_TAC `4` `4` `5`;
2107 EXISTS_SCS_J_TAC `5` `5` `6`];
2110 THEN MP_TAC(ARITH_RULE`x<6 ==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4\/ x=5`)
2113 THEN REWRITE_TAC[ARITH_RULE`0 MOD 6=0/\ SUC 0=1`]
2115 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
2116 THEN MRESAL_TAC VECTOR_3_6[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 5`;`(vv:num->real^3) 0`][ARITH_RULE`1<=6/\ 2<=6/\ 3<=6/\ 4<=6/\ 5<=6 /\ 6<=6 /\ 0 MOD 6= 0 /\ 1 MOD 6= 1 /\ 2 MOD 6= 2/\ 3 MOD 6= 3 /\ 4 MOD 6= 4 /\ 5 MOD 6=5 /\ 6 MOD 6=0 /\ ~(2=1)/\ ~(2=0)/\ ~(3=0)/\ ~(4=0)/\ ~(5=0)
2117 /\ SUC 0 MOD 6= 1 /\ SUC 1 MOD 6= 2 /\ SUC 2 MOD 6= 3/\ SUC 3 MOD 6= 4
2118 /\ SUC 4 MOD 6= 5 /\ SUC 5 MOD 6 = 0 /\ SUC 6 MOD 6 =1 /\ ~(3=1)/\ ~(1=0)
2119 /\ 1<=1 /\1<=2/\ 1<=3/\ 1<=4/\1<=5
2120 /\ SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`; SET_RULE`(a:num) IN (:num)`;dist]
2121 THEN REPLICATE_TAC 27 (POP_ASSUM MP_TAC)
2122 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2124 THEN ASM_REWRITE_TAC[IN;BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`]
2125 THEN REPEAT STRIP_TAC
2126 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(6=0)`]
2127 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])]);;
2132 let JKQEWGV1_CASE_6=prove(
2133 `!s vv. is_scs_v39 s /\ scs_k_v39 s=6 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
2134 /\ dimindex(:M)=scs_k_v39 s
2136 (sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
2137 (IMAGE (\i. (vv i,vv (SUC i))) (:num)) < pi)`,
2140 THEN MP_TAC IS_SCS_STABLE_SYSTEM
2142 THEN POP_ASSUM MP_TAC
2143 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<6`]
2145 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
2146 (change_type_v3 (scs_a_v39 s)),
2147 (change_type_v3 (scs_b_v39 s)),
2148 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
2149 (\i. (1 + i) MOD scs_k_v39 s))`
2150 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
2151 (change_type_v3 (scs_a_v39 s))`;`
2152 (change_type_v3 (scs_b_v39 s))`;`
2153 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
2154 (\i. (1 + i) MOD scs_k_v39 s)`]
2155 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 5;(vv:num->real^3) 0]:real^3^M`
2156 THEN ABBREV_TAC`a=matvec (v:real^3^M)`
2157 THEN MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6
2159 THEN POP_ASSUM MP_TAC
2160 THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
2162 THEN MP_TAC IN_IS_SCS_CASE_6
2164 THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<6`;]
2165 THEN REMOVE_ASSUM_TAC
2166 THEN POP_ASSUM MP_TAC
2168 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
2169 THEN MP_TAC V_E_FF_IS_SCS_CASES_6
2170 THEN ASM_REWRITE_TAC[IN]
2173 THEN ASM_REWRITE_TAC[is_scs_v39;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`;IN;mk_unadorned_v39]
2174 THEN REPEAT RESA_TAC
2175 THEN POP_ASSUM MP_TAC
2176 THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
2178 THEN MP_TAC(REAL_ARITH`pi <=
2179 sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
2180 (IMAGE (\i. vv i,vv (SUC i)) (:num)) \/
2181 sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
2182 (IMAGE (\i. vv i,vv (SUC i)) (:num))< pi`)
2184 THEN REPLICATE_TAC 19 REMOVE_ASSUM_TAC
2185 THEN POP_ASSUM MP_TAC
2186 THEN REAL_ARITH_TAC);;
2191 let IN_IMAGE_VV_EQ_3 =
2193 MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x':num`;th;`3`][ARITH_RULE`~(3=0)/\ 0 MOD 3=0/\ SUC 0 MOD 3=1/\ 1 MOD 3=1/\ SUC 1=2 /\ 2 MOD 3=2 /\ 3 MOD 3=0/\ SUC 2=3`]
2194 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`]
2195 THEN POP_ASSUM(fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x'`)
2196 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2197 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;SET_RULE`A IN {A,B,C} /\ B IN {A,B,C}/\ C IN {A,B,C} `])
2203 let V_E_FF_IS_SCS_CASES_3=prove_by_refinement(
2204 ` scs_k_v39 s=3/\ is_scs_v39 s /\ BBs_v39 s vv
2205 /\ dimindex(:M)=scs_k_v39 s
2207 ((IMAGE (\i. {vv i, vv (SUC i)}) (:num) ={{vv 0,vv 1},{vv 1, vv 2},{vv 2, vv 0}})
2208 /\ (IMAGE (\i. (vv i,vv (SUC i))) (:num)= {(vv 0,vv 1),(vv 1, vv 2),(vv 2, vv 0)}) )`,
2212 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
2213 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;IN;mk_unadorned_v39]
2215 THEN REWRITE_TAC[ARITH_RULE`3<=3`]
2216 THEN REPEAT STRIP_TAC;
2221 ONCE_REWRITE_TAC[EXTENSION]
2222 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;]
2227 THEN MRESAL_TAC DIVISION[`x':num`;`3`][ARITH_RULE`~(3=0)`]
2228 THEN MP_TAC(ARITH_RULE`x' MOD 3 < 3==> x' MOD 3 =0 \/ x' MOD 3 =1\/ x' MOD 3 =2`)
2231 IN_IMAGE_VV_EQ_3 `0`;
2232 IN_IMAGE_VV_EQ_3 `1`;
2233 IN_IMAGE_VV_EQ_3 `2`];
2236 REWRITE_TAC[SET_RULE`X IN {A,B,C}<=> X=A \/ X=B\/ X=C`]
2240 THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 0=1`];
2243 THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 1=2`];
2246 THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 2=3`]
2247 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`]
2248 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`])
2252 ONCE_REWRITE_TAC[EXTENSION]
2253 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;]
2258 THEN MRESAL_TAC DIVISION[`x':num`;`3`][ARITH_RULE`~(3=0)`]
2259 THEN MP_TAC(ARITH_RULE`x' MOD 3 < 3==> x' MOD 3 =0 \/ x' MOD 3 =1\/ x' MOD 3 =2`)
2262 IN_IMAGE_VV_EQ_3 `0`;
2263 IN_IMAGE_VV_EQ_3 `1`;
2264 IN_IMAGE_VV_EQ_3 `2`];
2267 REWRITE_TAC[SET_RULE`X IN {A,B,C}<=> X=A \/ X=B\/ X=C`]
2272 THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 0=1`];
2275 THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 1=2`];
2278 THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 2=3`]
2279 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`]
2280 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`]);
2285 let IS_SCS_POINT_IN_BBS_IS_NOT_0_3=prove_by_refinement(
2286 `scs_k_v39 s=3/\ is_scs_v39 s
2288 ==> ~(vv 1= vec 0)/\ ~(vv 2= vec 0) /\ ~(vv 0= vec 0)`,
2293 THEN POP_ASSUM MP_TAC
2294 THEN POP_ASSUM MP_TAC
2295 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;IMAGE;SUBSET;IN_ELIM_THM;is_scs_v39]
2298 THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv 0 = (vv:num->real^3) x)`ASSUME_TAC;
2300 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2301 SUBGOAL_THEN`(?x. x IN (:num) /\ vv 1 = (vv:num->real^3) x)`ASSUME_TAC;
2303 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2304 SUBGOAL_THEN`(?x. x IN (:num) /\ vv 2 = (vv:num->real^3) x)`ASSUME_TAC;
2306 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2307 REPLICATE_TAC 5(POP_ASSUM MP_TAC)
2308 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2309 THEN MRESAL1_TAC th`(vv:num->real^3) 0`[ball_annulus;IN_ELIM_THM;DIFF;ball]
2310 THEN MRESAL1_TAC th`(vv:num->real^3) 1`[ball_annulus;IN_ELIM_THM;DIFF;ball]
2311 THEN MRESAL1_TAC th`(vv:num->real^3) 2`[ball_annulus;IN_ELIM_THM;DIFF;ball;])
2314 THEN POP_ASSUM(fun th-> ASM_TAC
2315 THEN REWRITE_TAC[th;DIST_REFL;REAL_ARITH`(&0< &2)`]);
2318 THEN POP_ASSUM(fun th-> ASM_TAC
2319 THEN REWRITE_TAC[th;DIST_REFL;REAL_ARITH`(&0< &2)`]);
2321 THEN POP_ASSUM(fun th-> ASM_TAC
2322 THEN REWRITE_TAC[th;DIST_REFL;REAL_ARITH`(&0< &2)`])
2328 let IS_SCS_NOT_COLLINEAR_BBs_CASE_3=prove_by_refinement(
2329 `scs_k_v39 s=3/\ is_scs_v39 s
2331 ==> ~collinear{vec 0, vv 1 ,vv 2}/\
2332 ~collinear{vec 0, vv 1 ,vv 0}/\
2333 ~collinear{vec 0, vv 2 ,vv 0}`,
2338 REWRITE_TAC[Local_lemmas.collinear_fan22;aff;AFFINE_HULL_2;IN_ELIM_THM;VECTOR_ARITH`A % vec 0+B=B`]
2340 THEN MP_TAC IS_SCS_POINT_IN_BBS_IS_NOT_0_3
2343 THEN REWRITE_TAC[IN]
2345 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;is_scs_v39]
2346 THEN POP_ASSUM(fun th->
2349 THEN REPEAT STRIP_TAC;
2351 REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
2352 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2353 THEN MRESAL_TAC th[`1`;`2`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
2354 ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0/\ 1<3/\ 2<3`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
2355 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
2356 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2357 THEN MRESAL_TAC th[`1`;`2`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
2358 ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
2359 THEN REPLICATE_TAC 9(POP_ASSUM MP_TAC)
2360 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2362 THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv 1 = (vv:num->real^3) x)`ASSUME_TAC;
2366 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2368 SUBGOAL_THEN`(?x. x IN (:num) /\ vv 2 = (vv:num->real^3) x)`ASSUME_TAC;
2372 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2375 REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
2377 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`(vv:num->real^3) 2`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`]
2378 THEN MRESAL1_TAC th`(vv:num->real^3) 1`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`])
2379 THEN MP_TAC(REAL_ARITH`&0<= &1-v\/ &0<= --( &1-v)`)
2384 MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
2389 MRESA1_TAC Trigonometry2.ABS_REFL `v:real`
2390 THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
2391 THEN POP_ASSUM(fun th-> ASM_TAC
2392 THEN REWRITE_TAC[th]
2393 THEN REPEAT STRIP_TAC)
2394 THEN POP_ASSUM(fun th-> ASM_TAC
2395 THEN REWRITE_TAC[th]
2396 THEN REPEAT STRIP_TAC)
2397 THEN MP_TAC(REAL_ARITH`&2 <=scs_a_v39 s 2 1/\ scs_a_v39 s 2 1<= (&1 - v) * norm (vv 1)
2398 /\ &2 <= v * norm (vv 1) ==> &4<= norm ((vv:num->real^3) 1)`)
2399 THEN REPLICATE_TAC 4(POP_ASSUM MP_TAC)
2400 THEN ASM_REWRITE_TAC[h0]
2407 MRESAL1_TAC Trigonometry2.ABS_REFL `-- v:real`[REAL_ABS_NEG]
2408 THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
2409 THEN POP_ASSUM(fun th-> ASM_TAC
2410 THEN REWRITE_TAC[th]
2411 THEN REPEAT STRIP_TAC)
2412 THEN POP_ASSUM(fun th-> ASM_TAC
2413 THEN REWRITE_TAC[th; ]
2414 THEN REPEAT STRIP_TAC)
2415 THEN MP_TAC(REAL_ARITH`&2 <= --v * norm (vv 1)
2416 /\ &2 <= norm (vv 1) ==> &4<=(&1- v) *norm ((vv:num->real^3) 1)`)
2417 THEN ASM_REWRITE_TAC[]
2418 THEN REPLICATE_TAC 8(POP_ASSUM MP_TAC)
2419 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2420 THEN POP_ASSUM MP_TAC
2421 THEN REWRITE_TAC[SYM th])
2422 THEN REPLICATE_TAC 23(POP_ASSUM MP_TAC)
2423 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2424 THEN MRESAL1_TAC th`1`[ARITH_RULE`SUC 1=2`])
2425 THEN POP_ASSUM MP_TAC
2426 THEN POP_ASSUM MP_TAC
2427 THEN REPLICATE_TAC 9(REMOVE_ASSUM_TAC)
2428 THEN POP_ASSUM MP_TAC
2429 THEN REAL_ARITH_TAC;
2434 MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
2444 MRESAL1_TAC Trigonometry2.ABS_REFL ` v:real`[REAL_ABS_NEG]
2445 THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
2446 THEN POP_ASSUM(fun th-> ASM_TAC
2447 THEN REWRITE_TAC[th]
2448 THEN REPEAT STRIP_TAC)
2449 THEN POP_ASSUM(fun th-> ASM_TAC
2450 THEN REWRITE_TAC[th; ]
2451 THEN REPEAT STRIP_TAC)
2452 THEN MP_TAC(REAL_ARITH`&2 <= norm (vv 1)
2453 /\ &2 <= scs_a_v39 s 2 1/\ scs_a_v39 s 2 1<= --(&1 - v) * norm (vv 1) ==> &4<= v *norm ((vv:num->real^3) 1)`)
2454 THEN ASM_REWRITE_TAC[]
2455 THEN REPLICATE_TAC 5(POP_ASSUM MP_TAC)
2456 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2458 THEN POP_ASSUM MP_TAC
2459 THEN ASM_REWRITE_TAC[h0]
2464 MRESAL1_TAC Trigonometry2.ABS_REFL ` --v:real`[REAL_ABS_NEG]
2465 THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
2466 THEN POP_ASSUM(fun th-> ASM_TAC
2467 THEN REWRITE_TAC[th]
2468 THEN REPEAT STRIP_TAC)
2469 THEN POP_ASSUM(fun th-> ASM_TAC
2470 THEN REWRITE_TAC[th; ]
2471 THEN REPEAT STRIP_TAC)
2472 THEN MP_TAC(REAL_ARITH`&2 <= norm (vv 1)
2473 /\ &2 <= --v * norm (vv 1) ==> &4<= (&1-v) *norm ((vv:num->real^3) 1)`)
2474 THEN ASM_REWRITE_TAC[REAL_ARITH`~(a<= b) <=> b<a`]
2475 THEN REPLICATE_TAC 12(POP_ASSUM MP_TAC)
2476 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2478 THEN REPLICATE_TAC 11(POP_ASSUM MP_TAC)
2479 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2481 THEN POP_ASSUM MP_TAC
2482 THEN ASM_REWRITE_TAC[]
2483 THEN REAL_ARITH_TAC;
2489 REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
2490 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2491 THEN MRESAL_TAC th[`0`;`1`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
2492 ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0/\ 1<3/\ 2<3/\ 0<3 /\ ~(0=1)`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
2493 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
2494 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2495 THEN MRESAL_TAC th[`0`;`1`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
2496 ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0`;dist;VECTOR_ARITH`B%A - A= --((&1-B)%A)`;NORM_MUL;NORM_NEG])
2497 THEN REPLICATE_TAC 9(POP_ASSUM MP_TAC)
2498 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2500 THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv 1 = (vv:num->real^3) x)`ASSUME_TAC;
2504 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2506 SUBGOAL_THEN`(?x. x IN (:num) /\ vv 0 = (vv:num->real^3) x)`ASSUME_TAC;
2510 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2513 REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
2515 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`(vv:num->real^3) 0`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`]
2516 THEN MRESAL1_TAC th`(vv:num->real^3) 1`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`])
2517 THEN MP_TAC(REAL_ARITH`&0<= &1-v\/ &0<= --( &1-v)`)
2522 MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
2527 MRESA1_TAC Trigonometry2.ABS_REFL `v:real`
2528 THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
2529 THEN POP_ASSUM(fun th-> ASM_TAC
2530 THEN REWRITE_TAC[th]
2531 THEN REPEAT STRIP_TAC)
2532 THEN POP_ASSUM(fun th-> ASM_TAC
2533 THEN REWRITE_TAC[th]
2534 THEN REPEAT STRIP_TAC)
2535 THEN MP_TAC(REAL_ARITH`&2 <=scs_a_v39 s 1 0/\ scs_a_v39 s 1 0<= (&1 - v) * norm (vv 1)
2536 /\ &2 <= v * norm (vv 1) ==> &4<= norm ((vv:num->real^3) 1)`)
2537 THEN REPLICATE_TAC 4(POP_ASSUM MP_TAC)
2538 THEN ASM_REWRITE_TAC[h0]
2539 THEN REAL_ARITH_TAC;
2541 MRESAL1_TAC Trigonometry2.ABS_REFL `-- v:real`[REAL_ABS_NEG]
2542 THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
2543 THEN POP_ASSUM(fun th-> ASM_TAC
2544 THEN REWRITE_TAC[th]
2545 THEN REPEAT STRIP_TAC)
2546 THEN POP_ASSUM(fun th-> ASM_TAC
2547 THEN REWRITE_TAC[th; ]
2548 THEN REPEAT STRIP_TAC)
2549 THEN MP_TAC(REAL_ARITH`&2 <= --v * norm (vv 1)
2550 /\ &2 <= norm (vv 1) ==> &4<=(&1- v) *norm ((vv:num->real^3) 1)`)
2551 THEN ASM_REWRITE_TAC[]
2552 THEN REPLICATE_TAC 8(POP_ASSUM MP_TAC)
2553 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2554 THEN POP_ASSUM MP_TAC
2555 THEN REWRITE_TAC[SYM th])
2556 THEN REPLICATE_TAC 23(POP_ASSUM MP_TAC)
2557 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2558 THEN MRESAL1_TAC th`0`[ARITH_RULE`SUC 0=1`])
2559 THEN POP_ASSUM MP_TAC
2560 THEN POP_ASSUM MP_TAC
2561 THEN REPLICATE_TAC 9(REMOVE_ASSUM_TAC)
2562 THEN POP_ASSUM MP_TAC
2563 THEN REAL_ARITH_TAC;
2565 MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
2569 MRESAL1_TAC Trigonometry2.ABS_REFL ` v:real`[REAL_ABS_NEG]
2570 THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
2571 THEN POP_ASSUM(fun th-> ASM_TAC
2572 THEN REWRITE_TAC[th]
2573 THEN REPEAT STRIP_TAC)
2574 THEN POP_ASSUM(fun th-> ASM_TAC
2575 THEN REWRITE_TAC[th; ]
2576 THEN REPEAT STRIP_TAC)
2577 THEN MP_TAC(REAL_ARITH`&2 <= norm (vv 1)
2578 /\ &2 <= scs_a_v39 s 1 0/\ scs_a_v39 s 1 0<= --(&1 - v) * norm (vv 1) ==> &4<= v *norm ((vv:num->real^3) 1)`)
2579 THEN ASM_REWRITE_TAC[]
2580 THEN REPLICATE_TAC 5(POP_ASSUM MP_TAC)
2581 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2583 THEN POP_ASSUM MP_TAC
2584 THEN ASM_REWRITE_TAC[h0]
2589 MRESAL1_TAC Trigonometry2.ABS_REFL ` --v:real`[REAL_ABS_NEG]
2590 THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
2591 THEN POP_ASSUM(fun th-> ASM_TAC
2592 THEN REWRITE_TAC[th]
2593 THEN REPEAT STRIP_TAC)
2594 THEN POP_ASSUM(fun th-> ASM_TAC
2595 THEN REWRITE_TAC[th; ]
2596 THEN REPEAT STRIP_TAC)
2597 THEN MP_TAC(REAL_ARITH`&2 <= norm (vv 1)
2598 /\ &2 <= --v * norm (vv 1) ==> &4<= (&1-v) *norm ((vv:num->real^3) 1)`)
2599 THEN ASM_REWRITE_TAC[REAL_ARITH`~(a<= b) <=> b<a`]
2600 THEN REPLICATE_TAC 12(POP_ASSUM MP_TAC)
2601 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2603 THEN REPLICATE_TAC 11(POP_ASSUM MP_TAC)
2604 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2606 THEN POP_ASSUM MP_TAC
2607 THEN ASM_REWRITE_TAC[]
2608 THEN REAL_ARITH_TAC;
2612 REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
2613 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2614 THEN MRESAL_TAC th[`0`;`2`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
2615 ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0/\ 1<3/\ 2<3/\ 0<3 /\ ~(0=1)/\ ~(0=2)`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
2616 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
2617 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2618 THEN MRESAL_TAC th[`0`;`2`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
2619 ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0`;dist;VECTOR_ARITH`B%A - A= --((&1-B)%A)`;NORM_MUL;NORM_NEG])
2620 THEN REPLICATE_TAC 9(POP_ASSUM MP_TAC)
2621 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2623 THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv 2 = (vv:num->real^3) x)`ASSUME_TAC;
2627 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2629 SUBGOAL_THEN`(?x. x IN (:num) /\ vv 0 = (vv:num->real^3) x)`ASSUME_TAC;
2633 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2636 REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
2638 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`(vv:num->real^3) 0`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`]
2639 THEN MRESAL1_TAC th`(vv:num->real^3) 2`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`])
2640 THEN MP_TAC(REAL_ARITH`&0<= &1-v\/ &0<= --( &1-v)`)
2645 MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
2650 MRESA1_TAC Trigonometry2.ABS_REFL `v:real`
2651 THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
2652 THEN POP_ASSUM(fun th-> ASM_TAC
2653 THEN REWRITE_TAC[th]
2654 THEN REPEAT STRIP_TAC)
2655 THEN POP_ASSUM(fun th-> ASM_TAC
2656 THEN REWRITE_TAC[th]
2657 THEN REPEAT STRIP_TAC)
2658 THEN MP_TAC(REAL_ARITH`&2 <=scs_a_v39 s 2 0/\ scs_a_v39 s 2 0<= (&1 - v) * norm (vv 2)
2659 /\ &2 <= v * norm (vv 2) ==> &4<= norm ((vv:num->real^3) 2)`)
2660 THEN REPLICATE_TAC 4(POP_ASSUM MP_TAC)
2661 THEN ASM_REWRITE_TAC[h0]
2668 MRESAL1_TAC Trigonometry2.ABS_REFL `-- v:real`[REAL_ABS_NEG]
2669 THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
2670 THEN POP_ASSUM(fun th-> ASM_TAC
2671 THEN REWRITE_TAC[th]
2672 THEN REPEAT STRIP_TAC)
2673 THEN POP_ASSUM(fun th-> ASM_TAC
2674 THEN REWRITE_TAC[th; ]
2675 THEN REPEAT STRIP_TAC)
2676 THEN MP_TAC(REAL_ARITH`&2 <= --v * norm (vv 2)
2677 /\ &2 <= norm (vv 2) ==> &4<=(&1- v) *norm ((vv:num->real^3) 2)`)
2678 THEN ASM_REWRITE_TAC[]
2679 THEN REPLICATE_TAC 8(POP_ASSUM MP_TAC)
2680 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2681 THEN POP_ASSUM MP_TAC
2682 THEN REWRITE_TAC[SYM th])
2683 THEN REPLICATE_TAC 23(POP_ASSUM MP_TAC)
2684 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2685 THEN MRESAL1_TAC th`2`[ARITH_RULE`SUC 2=3`])
2686 THEN POP_ASSUM MP_TAC
2687 THEN POP_ASSUM MP_TAC
2688 THEN REPLICATE_TAC 9(REMOVE_ASSUM_TAC)
2690 THEN REWRITE_TAC[periodic2]
2691 THEN REPEAT STRIP_TAC
2692 THEN POP_ASSUM MP_TAC
2693 THEN POP_ASSUM MP_TAC
2694 THEN POP_ASSUM MP_TAC
2695 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s 2`][ARITH_RULE`~(3=0)`;periodic]
2696 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`])
2697 THEN REAL_ARITH_TAC;
2702 MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
2712 MRESAL1_TAC Trigonometry2.ABS_REFL ` v:real`[REAL_ABS_NEG]
2713 THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
2714 THEN POP_ASSUM(fun th-> ASM_TAC
2715 THEN REWRITE_TAC[th]
2716 THEN REPEAT STRIP_TAC)
2717 THEN POP_ASSUM(fun th-> ASM_TAC
2718 THEN REWRITE_TAC[th; ]
2719 THEN REPEAT STRIP_TAC)
2720 THEN MP_TAC(REAL_ARITH`&2 <= norm (vv 2)
2721 /\ &2 <= scs_a_v39 s 2 0/\ scs_a_v39 s 2 0<= --(&1 - v) * norm (vv 2) ==> &4<= v *norm ((vv:num->real^3) 2)`)
2722 THEN ASM_REWRITE_TAC[]
2723 THEN REPLICATE_TAC 5(POP_ASSUM MP_TAC)
2724 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2726 THEN POP_ASSUM MP_TAC
2727 THEN ASM_REWRITE_TAC[h0]
2732 MRESAL1_TAC Trigonometry2.ABS_REFL ` --v:real`[REAL_ABS_NEG]
2733 THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
2734 THEN POP_ASSUM(fun th-> ASM_TAC
2735 THEN REWRITE_TAC[th]
2736 THEN REPEAT STRIP_TAC)
2737 THEN POP_ASSUM(fun th-> ASM_TAC
2738 THEN REWRITE_TAC[th; ]
2739 THEN REPEAT STRIP_TAC)
2740 THEN MP_TAC(REAL_ARITH`&2 <= norm (vv 2)
2741 /\ &2 <= --v * norm (vv 2) ==> &4<= (&1-v) *norm ((vv:num->real^3) 2)`)
2742 THEN ASM_REWRITE_TAC[REAL_ARITH`~(a<= b) <=> b<a`]
2743 THEN REPLICATE_TAC 12(POP_ASSUM MP_TAC)
2744 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2746 THEN REPLICATE_TAC 11(POP_ASSUM MP_TAC)
2747 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2749 THEN POP_ASSUM MP_TAC
2750 THEN ASM_REWRITE_TAC[]
2751 THEN REAL_ARITH_TAC;
2758 let IS_SCS_POINT_IN_BBS_IS_NOT_0_LE_3=prove_by_refinement(
2759 `3<scs_k_v39 s/\ is_scs_v39 s
2761 ==> ~(vv i= vec 0)`,
2764 THEN POP_ASSUM MP_TAC
2765 THEN POP_ASSUM MP_TAC
2766 THEN MP_TAC(ARITH_RULE`3<scs_k_v39 s==> ~(scs_k_v39 s<=3)`)
2768 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ;IMAGE;SUBSET;IN_ELIM_THM;is_scs_v39]
2771 THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv i= (vv:num->real^3) x)`ASSUME_TAC;
2773 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2774 REPLICATE_TAC 4(POP_ASSUM MP_TAC)
2775 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2776 THEN MRESAL1_TAC th`(vv:num->real^3) i`[ball_annulus;IN_ELIM_THM;DIFF;ball])
2777 THEN POP_ASSUM MP_TAC
2778 THEN REWRITE_TAC[DIST_REFL;REAL_ARITH`(&0< &2)`]
2785 let IS_SCS_NOT_COLLINEAR_BBs_CASE_LE_3=prove_by_refinement(
2786 `3< scs_k_v39 s/\ is_scs_v39 s
2788 /\ ~(i MOD (scs_k_v39 s)=j MOD (scs_k_v39 s))
2789 /\ dist(vv (i MOD (scs_k_v39 s)) ,vv (j MOD (scs_k_v39 s))) <= cstab
2790 ==> ~collinear{vec 0, vv (i MOD (scs_k_v39 s)) ,vv (j MOD (scs_k_v39 s))}`,
2792 REWRITE_TAC[Local_lemmas.collinear_fan22;aff;AFFINE_HULL_2;IN_ELIM_THM;VECTOR_ARITH`A % vec 0+B=B`;cstab]
2794 THEN MRESA_TAC( GEN_ALL IS_SCS_POINT_IN_BBS_IS_NOT_0_LE_3)[`s:scs_v39`;`vv:num->real^3`;`i MOD scs_k_v39 s`]
2797 THEN REWRITE_TAC[IN]
2799 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;is_scs_v39]
2800 THEN POP_ASSUM(fun th->
2803 THEN REPEAT STRIP_TAC;
2805 MP_TAC(ARITH_RULE`3 < scs_k_v39 s==> ~(scs_k_v39 s <= 3)`)
2809 ABBREV_TAC`k=scs_k_v39 s`
2810 THEN POP_ASSUM MP_TAC
2811 THEN MP_TAC(ARITH_RULE`3<=k ==> ~(k=0)`)
2814 THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
2815 THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
2816 THEN REPLICATE_TAC (35-14) (POP_ASSUM MP_TAC)
2817 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2818 THEN MRESAL_TAC th[`i MOD k`;`j MOD k`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
2819 ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0/\ 1<3/\ 2<3`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
2820 THEN REPLICATE_TAC (35-25)(POP_ASSUM MP_TAC)
2821 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2823 THEN REPLICATE_TAC (34-22) (POP_ASSUM MP_TAC)
2824 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2825 THEN POP_ASSUM MP_TAC
2826 THEN MRESAL_TAC th[`i MOD k`;`j MOD k`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
2827 ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
2828 THEN REPLICATE_TAC (35-20)(POP_ASSUM MP_TAC)
2829 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2831 THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv (i MOD k) = (vv:num->real^3) x)`ASSUME_TAC;
2834 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2836 SUBGOAL_THEN`(?x. x IN (:num) /\ vv (j MOD k) = (vv:num->real^3) x)`ASSUME_TAC;
2839 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2841 REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
2843 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`(vv:num->real^3) (i MOD k)`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`]
2844 THEN MRESAL1_TAC th`(vv:num->real^3) (j MOD k)`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`])
2845 THEN MP_TAC(REAL_ARITH`&0<= &1-v\/ &0<= --( &1-v)`)
2848 MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
2851 MRESA1_TAC Trigonometry2.ABS_REFL `v:real`
2852 THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
2853 THEN POP_ASSUM(fun th-> ASM_TAC
2854 THEN REWRITE_TAC[th]
2855 THEN REPEAT STRIP_TAC)
2856 THEN POP_ASSUM(fun th-> ASM_TAC
2857 THEN REWRITE_TAC[th]
2858 THEN REPEAT STRIP_TAC)
2859 THEN MP_TAC(REAL_ARITH`&2 <=scs_a_v39 s (i MOD k) (j MOD k)/\ scs_a_v39 s (i MOD k) (j MOD k)<= (&1 - v) * norm (vv (i MOD k))
2860 /\ &2 <= v * norm (vv (i MOD k)) ==> &4<= norm ((vv:num->real^3) (i MOD k))`)
2861 THEN REPLICATE_TAC 6(POP_ASSUM MP_TAC)
2862 THEN ASM_REWRITE_TAC[h0]
2863 THEN REAL_ARITH_TAC;
2866 MRESAL1_TAC Trigonometry2.ABS_REFL `-- v:real`[REAL_ABS_NEG]
2867 THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
2868 THEN POP_ASSUM(fun th-> ASM_TAC
2869 THEN REWRITE_TAC[th]
2870 THEN REPEAT STRIP_TAC)
2871 THEN POP_ASSUM(fun th-> ASM_TAC
2872 THEN REWRITE_TAC[th; ]
2873 THEN REPEAT STRIP_TAC)
2874 THEN MP_TAC(REAL_ARITH`&2 <= --v * norm (vv (i MOD k))
2875 /\ &2 <= norm (vv (i MOD k)) ==> &4<=(&1- v) *norm ((vv:num->real^3) (i MOD k) )`)
2876 THEN ASM_REWRITE_TAC[]
2877 THEN REPLICATE_TAC (45-35)(POP_ASSUM MP_TAC)
2878 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2879 THEN POP_ASSUM MP_TAC
2881 THEN ASM_REWRITE_TAC[])
2882 THEN REAL_ARITH_TAC;
2884 MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
2888 MRESAL1_TAC Trigonometry2.ABS_REFL ` v:real`[REAL_ABS_NEG]
2889 THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
2890 THEN POP_ASSUM(fun th-> ASM_TAC
2891 THEN REWRITE_TAC[th]
2892 THEN REPEAT STRIP_TAC)
2893 THEN POP_ASSUM(fun th-> ASM_TAC
2894 THEN REWRITE_TAC[th; ]
2895 THEN REPEAT STRIP_TAC)
2896 THEN MP_TAC(REAL_ARITH`&2 <= norm (vv (i MOD k))
2897 /\ &2 <= scs_a_v39 s (i MOD k) (j MOD k)/\ scs_a_v39 s (i MOD k) (j MOD k)<= --(&1 - v) * norm (vv (i MOD k)) ==> &4<= v *norm ((vv:num->real^3) (i MOD k))`)
2898 THEN ASM_REWRITE_TAC[]
2899 THEN REPLICATE_TAC 3(POP_ASSUM MP_TAC)
2900 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2902 THEN POP_ASSUM MP_TAC
2903 THEN ASM_REWRITE_TAC[h0]
2904 THEN REAL_ARITH_TAC;
2906 MRESAL1_TAC Trigonometry2.ABS_REFL ` --v:real`[REAL_ABS_NEG]
2907 THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
2908 THEN POP_ASSUM(fun th-> ASM_TAC
2909 THEN REWRITE_TAC[th]
2910 THEN REPEAT STRIP_TAC)
2911 THEN POP_ASSUM(fun th-> ASM_TAC
2912 THEN REWRITE_TAC[th; ]
2913 THEN REPEAT STRIP_TAC)
2914 THEN MP_TAC(REAL_ARITH`&2 <= norm (vv (i MOD k))
2915 /\ &2 <= --v * norm (vv (i MOD k)) ==> &4<= (&1-v) *norm ((vv:num->real^3) (i MOD k))`)
2916 THEN ASM_REWRITE_TAC[REAL_ARITH`~(a<= b) <=> b<a`]
2917 THEN REPLICATE_TAC (45-32)(POP_ASSUM MP_TAC)
2918 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2920 THEN REPLICATE_TAC (44-32)(POP_ASSUM MP_TAC)
2921 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2923 THEN POP_ASSUM MP_TAC
2924 THEN ASM_REWRITE_TAC[]
2925 THEN REAL_ARITH_TAC;
2941 `!s vv. is_scs_v39 s /\ 3< scs_k_v39 s /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
2943 (sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
2944 (IMAGE (\i. (vv i,vv (SUC i))) (:num)) < pi)`,
2948 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2950 THEN REWRITE_TAC[is_scs_v39]
2953 THEN MP_TAC(ARITH_RULE`3< scs_k_v39 s /\ scs_k_v39 s<=6 ==> scs_k_v39 s = 4\/ scs_k_v39 s = 5 \/ scs_k_v39 s =6`)
2956 MP_TAC(INST_TYPE [`:2+2`,`:M`]JKQEWGV1_CASE_4)
2957 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_4]
2959 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]);
2961 MP_TAC(INST_TYPE [`:2+3`,`:M`]JKQEWGV1_CASE_5)
2962 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_5]
2964 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]);
2966 MP_TAC(INST_TYPE [`:3+3`,`:M`]JKQEWGV1_CASE_6)
2967 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_6]
2969 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])]);;
2974 let JKQEWGV2_CASE_4=prove(`!s vv. is_scs_v39 s /\ scs_k_v39 s=4 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
2975 /\ dimindex(:M)=scs_k_v39 s
2978 let V = IMAGE vv (:num) in
2979 let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
2983 THEN MP_TAC IS_SCS_STABLE_SYSTEM
2985 THEN POP_ASSUM MP_TAC
2986 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<4`]
2988 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
2989 (change_type_v3 (scs_a_v39 s)),
2990 (change_type_v3 (scs_b_v39 s)),
2991 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
2992 (\i. (1 + i) MOD scs_k_v39 s))`
2993 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
2994 (change_type_v3 (scs_a_v39 s))`;`
2995 (change_type_v3 (scs_b_v39 s))`;`
2996 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
2997 (\i. (1 + i) MOD scs_k_v39 s)`]
2998 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 0]:real^3^M`
2999 THEN ABBREV_TAC`a=matvec (v:real^3^M)`
3000 THEN MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4
3002 THEN POP_ASSUM MP_TAC
3003 THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
3005 THEN MP_TAC IN_IS_SCS_CASE_4
3007 THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<4`;]
3008 THEN POP_ASSUM MP_TAC
3010 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
3011 THEN MP_TAC V_E_FF_IS_SCS_CASES_4
3012 THEN ASM_REWRITE_TAC[IN]
3015 THEN ASM_REWRITE_TAC[is_scs_v39;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;IN;mk_unadorned_v39]
3016 THEN REPEAT RESA_TAC
3017 THEN POP_ASSUM MP_TAC
3019 THEN POP_ASSUM MATCH_MP_TAC
3020 THEN MP_TAC(REAL_ARITH`taustar_v39 s vv < &0 ==> taustar_v39 s vv <= &0`)
3022 THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
3027 let JKQEWGV2_CASE_5=prove(`!s vv. is_scs_v39 s /\ scs_k_v39 s=5 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
3028 /\ dimindex(:M)=scs_k_v39 s
3031 let V = IMAGE vv (:num) in
3032 let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
3036 THEN MP_TAC IS_SCS_STABLE_SYSTEM
3038 THEN POP_ASSUM MP_TAC
3039 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<5`]
3041 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
3042 (change_type_v3 (scs_a_v39 s)),
3043 (change_type_v3 (scs_b_v39 s)),
3044 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
3045 (\i. (1 + i) MOD scs_k_v39 s))`
3046 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
3047 (change_type_v3 (scs_a_v39 s))`;`
3048 (change_type_v3 (scs_b_v39 s))`;`
3049 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
3050 (\i. (1 + i) MOD scs_k_v39 s)`]
3051 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 0]:real^3^M`
3052 THEN ABBREV_TAC`a=matvec (v:real^3^M)`
3053 THEN MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5
3055 THEN POP_ASSUM MP_TAC
3056 THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
3058 THEN MP_TAC IN_IS_SCS_CASE_5
3060 THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<5`;]
3061 THEN POP_ASSUM MP_TAC
3063 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
3064 THEN MP_TAC V_E_FF_IS_SCS_CASES_5
3065 THEN ASM_REWRITE_TAC[IN]
3068 THEN ASM_REWRITE_TAC[is_scs_v39;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(5<=3)`;IN;mk_unadorned_v39]
3069 THEN REPEAT RESA_TAC
3070 THEN POP_ASSUM MP_TAC
3072 THEN POP_ASSUM MATCH_MP_TAC
3073 THEN MP_TAC(REAL_ARITH`taustar_v39 s vv < &0 ==> taustar_v39 s vv <= &0`)
3075 THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
3082 let JKQEWGV2_CASE_6=prove(`!s vv. is_scs_v39 s /\ scs_k_v39 s=6 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
3083 /\ dimindex(:M)=scs_k_v39 s
3086 let V = IMAGE vv (:num) in
3087 let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
3091 THEN MP_TAC IS_SCS_STABLE_SYSTEM
3093 THEN POP_ASSUM MP_TAC
3094 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<6`]
3096 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
3097 (change_type_v3 (scs_a_v39 s)),
3098 (change_type_v3 (scs_b_v39 s)),
3099 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
3100 (\i. (1 + i) MOD scs_k_v39 s))`
3101 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
3102 (change_type_v3 (scs_a_v39 s))`;`
3103 (change_type_v3 (scs_b_v39 s))`;`
3104 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
3105 (\i. (1 + i) MOD scs_k_v39 s)`]
3106 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 5;(vv:num->real^3) 0]:real^3^M`
3107 THEN ABBREV_TAC`a=matvec (v:real^3^M)`
3108 THEN MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6
3110 THEN POP_ASSUM MP_TAC
3111 THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
3113 THEN MP_TAC IN_IS_SCS_CASE_6
3115 THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<6`;]
3116 THEN POP_ASSUM MP_TAC
3118 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
3119 THEN MP_TAC V_E_FF_IS_SCS_CASES_6
3120 THEN ASM_REWRITE_TAC[IN]
3123 THEN ASM_REWRITE_TAC[is_scs_v39;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`;IN;mk_unadorned_v39]
3124 THEN REPEAT RESA_TAC
3125 THEN POP_ASSUM MP_TAC
3127 THEN POP_ASSUM MATCH_MP_TAC
3128 THEN MP_TAC(REAL_ARITH`taustar_v39 s vv < &0 ==> taustar_v39 s vv <= &0`)
3130 THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
3137 `!s vv. is_scs_v39 s /\ 3< scs_k_v39 s /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
3140 let V = IMAGE vv (:num) in
3141 let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
3146 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
3148 THEN REWRITE_TAC[is_scs_v39]
3151 THEN MP_TAC(ARITH_RULE`3< scs_k_v39 s /\ scs_k_v39 s<=6 ==> scs_k_v39 s = 4\/ scs_k_v39 s = 5 \/ scs_k_v39 s =6`)
3154 MP_TAC(INST_TYPE [`:2+2`,`:M`]JKQEWGV2_CASE_4)
3155 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_4]
3157 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]);
3159 MP_TAC(INST_TYPE [`:2+3`,`:M`]JKQEWGV2_CASE_5)
3160 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_5]
3162 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]);
3164 MP_TAC(INST_TYPE [`:3+3`,`:M`]JKQEWGV2_CASE_6)
3165 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_6]
3167 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])]);;
3173 let JKQEWGV3 = prove_by_refinement(
3175 (let V = IMAGE vv (:num) in
3176 let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
3177 let FF = IMAGE (\i. (vv i,vv (SUC i))) (:num) in
3178 (is_scs_v39 s /\ BBs_v39 s vv /\ 3< scs_k_v39 s /\ taustar_v39 s vv < &0 /\ lunar (v,w) V E ==>
3179 (interior_angle1 (vec 0) FF v < pi / &2 )))`,
3182 REWRITE_TAC[LET_DEF;LET_END_DEF;]
3183 THEN REPEAT STRIP_TAC
3184 THEN POP_ASSUM(fun th-> MP_TAC th
3185 THEN REWRITE_TAC[lunar]
3187 THEN ABBREV_TAC`V= IMAGE (vv:num->real^3) (:num)`
3188 THEN ABBREV_TAC`E= IMAGE (\i. {vv i,(vv:num->real^3) (SUC i)}) (:num)`
3189 THEN ABBREV_TAC`FF= IMAGE (\i. (vv i,(vv:num->real^3) (SUC i))) (:num)`
3190 THEN MRESA_TAC (GEN_ALL HKIRPEP)[`E:(real^3->bool)->bool`;`w:real^3`;`FF:real^3#real^3->bool`;`v:real^3`;`V:real^3->bool`]
3194 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th
3195 THEN MP_TAC(ARITH_RULE`3< scs_k_v39 s==> ~( scs_k_v39 s<= 3)`)
3197 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;]
3200 THEN MP_TAC(SET_RULE`{v, w:real^3} SUBSET V ==> v IN V /\ w IN V`)
3202 THEN MRESA_TAC(GEN_ALL Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS)
3203 [`IMAGE (\i. {vv i, (vv:num->real^3) (SUC i)}) (:num)`;`IMAGE ((vv:num->real^3)) (:num)`;`IMAGE (\i. ((vv:num->real^3) i,vv (SUC i))) (:num)`]
3204 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
3205 THEN MRESA_TAC JKQEWGV1[`s:scs_v39`;`vv:num->real^3`]
3206 THEN POP_ASSUM MP_TAC
3207 THEN REWRITE_TAC[sol_local]
3208 THEN REPLICATE_TAC 8 (POP_ASSUM MP_TAC)
3209 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
3210 THEN POP_ASSUM MP_TAC
3212 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
3213 THEN POP_ASSUM(fun th-> REPLICATE_TAC 3 STRIP_TAC
3214 THEN MP_TAC Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM
3215 THEN REWRITE_TAC[th]
3218 THEN REWRITE_TAC[convex_local_fan]
3219 THEN REPEAT STRIP_TAC)
3220 THEN POP_ASSUM MP_TAC
3221 THEN MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF
3223 THEN MP_TAC Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2
3225 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`
3226 THEN MRESA1_TAC th`w:real^3`)
3227 THEN MP_TAC(SET_RULE`v,rho_node1 FF v IN FF/\
3228 w,rho_node1 FF w IN FF ==>
3229 {(v,rho_node1 FF v ),(w,rho_node1 FF w)} SUBSET FF`)
3231 THEN MRESA_TAC SUM_DIFF[`(\e:real^3#real^3. azim_in_fan e E - pi)`;`FF:real^3#real^3->bool`;`{(v,rho_node1 FF v),(w,rho_node1 FF w)}`]
3232 THEN POP_ASSUM MP_TAC
3233 THEN REWRITE_TAC[REAL_ARITH`A=B-C<=> B=A+C`]
3235 THEN MRESAL_TAC Geomdetail.SUM_DIS2[`(v,rho_node1 FF v)`;`(w,rho_node1 FF w)`;`(\e:real^3#real^3. azim_in_fan e E - pi)`][PAIR_EQ]
3236 THEN SUBGOAL_THEN`sum (FF DIFF {(v,rho_node1 FF v), (w,rho_node1 FF w)})
3237 (\e. azim_in_fan e E - pi)= &0` ASSUME_TAC;
3239 MATCH_MP_TAC SUM_EQ_0
3240 THEN REWRITE_TAC[DIFF;IN_ELIM_THM;SET_RULE`~(a IN {b,c}) <=> ~(a=b) /\ ~(a=c)`]
3241 THEN REPEAT STRIP_TAC
3242 THEN REPLICATE_TAC 8 (POP_ASSUM MP_TAC)
3243 THEN POP_ASSUM(fun th-> REPLICATE_TAC 8 STRIP_TAC
3244 THEN MRESA1_TAC th`x:real^3#real^3`)
3245 THEN POP_ASSUM(fun th-> REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
3246 THEN ONCE_REWRITE_TAC[th]
3247 THEN REWRITE_TAC[PAIR_EQ])
3248 THEN REPEAT STRIP_TAC
3249 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)
3250 [`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`FST (x:real^3#real^3)`;`rho_node1 FF (FST (x:real^3#real^3))`;`V:real^3->bool`]
3251 THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
3252 THEN POP_ASSUM(fun th-> REPLICATE_TAC 13 STRIP_TAC
3253 THEN MRESA1_TAC th`FST (x:real^3#real^3)`)
3254 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3255 THEN SUBGOAL_THEN`FST (x:real^3#real^3) IN V DIFF {v,w}`ASSUME_TAC;
3257 ASM_REWRITE_TAC[DIFF;IN_ELIM_THM;SET_RULE`~(a IN {b,c}) <=> ~(a=b) /\ ~(a=c)`]
3258 THEN REMOVE_ASSUM_TAC
3259 THEN REMOVE_ASSUM_TAC
3260 THEN POP_ASSUM MP_TAC
3261 THEN POP_ASSUM MP_TAC
3264 REPLICATE_TAC (34-7) (POP_ASSUM MP_TAC)
3265 THEN POP_ASSUM(fun th-> REPLICATE_TAC (34-7) STRIP_TAC
3268 THEN REPLICATE_TAC (47-34) (REMOVE_ASSUM_TAC)
3269 THEN POP_ASSUM (fun th-> MRESA1_TAC th`FST (x:real^3#real^3)`)
3270 THEN REAL_ARITH_TAC;
3273 THEN REPLICATE_TAC 10 (POP_ASSUM MP_TAC)
3274 THEN POP_ASSUM(fun th-> REPLICATE_TAC 10 STRIP_TAC
3275 THEN MRESA1_TAC th`v:real^3`
3276 THEN MRESA1_TAC th`w:real^3`)
3277 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3278 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3279 THEN REPLICATE_TAC (30-7) (POP_ASSUM MP_TAC)
3280 THEN POP_ASSUM(fun th-> REPLICATE_TAC (30-7) STRIP_TAC
3282 THEN REPLICATE_TAC (12) (POP_ASSUM MP_TAC)
3283 THEN POP_ASSUM(fun th-> REPLICATE_TAC (12) STRIP_TAC
3284 THEN REWRITE_TAC[th])
3286 THEN REPLICATE_TAC (10) (REMOVE_ASSUM_TAC)
3287 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3288 THEN ASM_REWRITE_TAC[]
3289 THEN REAL_ARITH_TAC]);;
3301 let check_completeness_claimA_concl =
3302 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)