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 Uxckfpe = struct
26 open Wrgcvdr_cizmrrh;;
34 open Flyspeck_constants;;
50 open Wrgcvdr_cizmrrh;;
52 open Flyspeck_constants;;
70 let NOT_EMPTY_CASE_4_IS_SCS=prove_by_refinement(
71 ` is_scs_v39 s /\ scs_k_v39 s=4 /\ BBs_v39 s vv
72 /\ dimindex(:M)= scs_k_v39 s
73 ==> ~({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 }={})`,
74 [REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;]
76 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`
77 THEN ABBREV_TAC`a=matvec (v:real^3^M) `
78 THEN EXISTS_TAC`a:real^(M,3)finite_product`
79 THEN MATCH_MP_TAC IN_IS_SCS_CASE_4
80 THEN ASM_REWRITE_TAC[]]);;
84 let ARITH_4_TAC =ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=4/\3<=4/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)/\ 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)/\ SUC 1=2/\ SUC 4=5/\ 5 MOD 4=1/\ ~(4=0)/\ 0 MOD 4=0`;;
87 let VV_IN_BALL_ANNULUS_TAC_4=
89 REPLICATE_TAC (31-23)(POP_ASSUM MP_TAC)
90 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
91 THEN MRESAL1_TAC th so[ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=4/\3<=4/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)`;IN])
95 let SCS_A_LE_NORM_4_IS_SCS=
96 fun (so:term) (so1:term)->
97 REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
98 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
99 THEN MRESAL_TAC th [so;so1][ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=4/\3<=4/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)`;IN])
101 THEN REWRITE_TAC[periodic2]
102 THEN REPEAT STRIP_TAC
103 THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
104 THEN POP_ASSUM(fun th->
107 THEN REPEAT STRIP_TAC
108 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
110 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
111 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
112 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(4=0)`;periodic]
113 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`] THEN MRESA1_TAC th`i:num`)
114 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
115 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(4=0)`;periodic]
116 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`])
120 let PROVE_INEQUALITY_TAC_4=
122 MP_TAC(ARITH_RULE`(j MOD 4<4)==> (j MOD 4=0) \/ (j MOD 4=1) \/ (j MOD 4=2)\/ (j MOD 4=3)`)
125 SCS_A_LE_NORM_4_IS_SCS th `4`;
126 SCS_A_LE_NORM_4_IS_SCS th `1`;
127 SCS_A_LE_NORM_4_IS_SCS th `2`;
128 SCS_A_LE_NORM_4_IS_SCS th `3`];;
133 let SCS_B_LE_NORM_4_IS_SCS=
134 fun (so:term) (so1:term)->
135 REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
136 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
137 THEN MRESAL_TAC th [so;so1][ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=4/\3<=4/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)`;IN])
139 THEN REWRITE_TAC[periodic2]
140 THEN REPEAT STRIP_TAC
141 THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
142 THEN POP_ASSUM(fun th->
145 THEN REPEAT STRIP_TAC
146 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
148 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
149 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
150 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(4=0)`;periodic]
151 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`] THEN MRESA1_TAC th`i:num`)
152 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
153 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(4=0)`;periodic]
154 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`])
155 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (4)`][ARITH_RULE`~(4=0)`;periodic]
156 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`])
160 let PROVE_INEQUALITY_TAC_4B=
162 MP_TAC(ARITH_RULE`(j MOD 4<4)==> (j MOD 4=0) \/ (j MOD 4=1) \/ (j MOD 4=2)\/ (j MOD 4=3)`)
165 SCS_B_LE_NORM_4_IS_SCS th `4`;
166 SCS_B_LE_NORM_4_IS_SCS th `1`;
167 SCS_B_LE_NORM_4_IS_SCS th `2`;
168 SCS_B_LE_NORM_4_IS_SCS th `3`];;
173 let V_SY_EQ_IMAGE_VV_TAC4=
177 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`;ARITH_4_TAC];;
180 let PROVE_E_SY_EQ_MOD_TAC_4=
183 THEN ASM_REWRITE_TAC[ARITH_4_TAC]
192 let PROOF_E_EQ_TAC_4=
195 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_4_TAC;]
199 let PROVE_E_SY_EQ_IMAGE_VV_4=
200 fun (so:term) (so1:term)->
201 MRESAL_TAC(GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`x':num`;so1;`scs_k_v39 s`][ARITH_4_TAC]
203 THEN ASM_REWRITE_TAC[ARITH_4_TAC];;
208 let IN_NOT_EMPTY_B1_SY_4_IS_SCS=prove_by_refinement(
209 `is_scs_v39 s /\ scs_k_v39 s=4 /\
210 dimindex(:M) = scs_k_v39 s/\
211 matvec (v:real^3^M) =a/\
212 (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\
213 CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\
216 if i MOD scs_k_v39 s = 0 then row 4 v else
217 if i MOD scs_k_v39 s = 1 then row 1 v else
218 if i MOD scs_k_v39 s = 2 then row 2 v else
220 ==> vv IN BBs_v39 s`,
223 REWRITE_TAC[CONDITION1_SY;CONDITION2_SY;change_type_v3]
224 THEN REPEAT STRIP_TAC
226 THEN REWRITE_TAC[is_scs_v39;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;]
227 THEN REPEAT RESA_TAC;
230 ASM_REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
231 THEN REPEAT STRIP_TAC
232 THEN ASM_REWRITE_TAC[]
233 THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
234 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`)
237 VV_IN_BALL_ANNULUS_TAC_4 `4`;
238 VV_IN_BALL_ANNULUS_TAC_4 `1`;
239 VV_IN_BALL_ANNULUS_TAC_4 `2`;
240 VV_IN_BALL_ANNULUS_TAC_4 `3`];
244 ASM_REWRITE_TAC[periodic]
246 THEN MRESAL_TAC MOD_EQ[`i+4:num`;`i:num`;`4:num`;`1`][ARITH_RULE`1*A=A`];
252 THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 4)` ASSUME_TAC;
255 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
257 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`4`][ARITH_RULE`~(4=0)`];
261 MRESAL_TAC DIVISION[`i:num`;`4`][ARITH_RULE`~(4=0)`]
262 THEN MRESAL_TAC DIVISION[`j:num`;`4`][ARITH_RULE`~(4=0)`]
263 THEN MP_TAC(ARITH_RULE`(i MOD 4<4)==> (i MOD 4=0) \/ (i MOD 4=1) \/ (i MOD 4=2)\/ (i MOD 4=3)`)
266 PROVE_INEQUALITY_TAC_4 `4`;
267 PROVE_INEQUALITY_TAC_4 `1`;
268 PROVE_INEQUALITY_TAC_4 `2`;
269 PROVE_INEQUALITY_TAC_4 `3`]
278 THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 4)` ASSUME_TAC;
281 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
283 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`4`][ARITH_RULE`~(4=0)`];
287 MRESAL_TAC DIVISION[`i:num`;`4`][ARITH_RULE`~(4=0)`]
288 THEN MRESAL_TAC DIVISION[`j:num`;`4`][ARITH_RULE`~(4=0)`]
289 THEN MP_TAC(ARITH_RULE`(i MOD 4<4)==> (i MOD 4=0) \/ (i MOD 4=1) \/ (i MOD 4=2)\/ (i MOD 4=3)`)
292 PROVE_INEQUALITY_TAC_4B `4`;
293 PROVE_INEQUALITY_TAC_4B `1`;
294 PROVE_INEQUALITY_TAC_4B `2`;
295 PROVE_INEQUALITY_TAC_4B `3`]
309 THEN ASM_REWRITE_TAC[ARITH_RULE`~(4<=3)`]
311 THEN SUBGOAL_THEN`V_SY (v:real^3^M) = IMAGE vv (:num)`ASSUME_TAC;
315 ASM_REWRITE_TAC[V_SY;rows;IMAGE;EXTENSION;IN_ELIM_THM]
320 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 4)<=> i= 1\/ i=2 \/ i=3 \/ i=4`]
323 V_SY_EQ_IMAGE_VV_TAC4 `1`;
324 V_SY_EQ_IMAGE_VV_TAC4 `2`;
325 V_SY_EQ_IMAGE_VV_TAC4 `3`;
326 V_SY_EQ_IMAGE_VV_TAC4 `4`];
331 THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
332 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)`)
335 PROVE_E_SY_EQ_MOD_TAC_4 `4`;
336 PROVE_E_SY_EQ_MOD_TAC_4 `1`;
337 PROVE_E_SY_EQ_MOD_TAC_4 `2`;
338 PROVE_E_SY_EQ_MOD_TAC_4 `3`]
347 SUBGOAL_THEN`E_SY (v:real^3^M) = IMAGE (\i. {vv i, vv (SUC i)}) (:num)`ASSUME_TAC;
351 ASM_REWRITE_TAC[E_SY;rows;IMAGE;]
352 THEN ONCE_REWRITE_TAC[EXTENSION;]
353 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
361 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 4)<=> i= 1\/ i=2 \/ i=3 \/ i=4`]
373 THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
374 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)`)
377 PROVE_E_SY_EQ_IMAGE_VV_4 `4` `0`;
378 PROVE_E_SY_EQ_IMAGE_VV_4 `1` `1`;
379 PROVE_E_SY_EQ_IMAGE_VV_4 `2` `2`;
380 PROVE_E_SY_EQ_IMAGE_VV_4 `3` `3`];
384 SUBGOAL_THEN`F_SY (v:real^3^M) = IMAGE (\i. (vv i, vv (SUC i))) (:num)`ASSUME_TAC;
387 ASM_REWRITE_TAC[F_SY;rows;IMAGE;]
388 THEN ONCE_REWRITE_TAC[EXTENSION;]
389 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
397 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 4)<=> i= 1\/ i=2 \/ i=3 \/ i=4`]
409 THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
410 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)`)
413 PROVE_E_SY_EQ_IMAGE_VV_4 `4` `0`;
414 PROVE_E_SY_EQ_IMAGE_VV_4 `1` `1`;
415 PROVE_E_SY_EQ_IMAGE_VV_4 `2` `2`;
416 PROVE_E_SY_EQ_IMAGE_VV_4 `3` `3`];
420 REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
421 THEN ASM_REWRITE_TAC[]
422 THEN REPEAT STRIP_TAC
423 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM th])
424 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
425 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
426 THEN ASM_REWRITE_TAC[];
432 let XWITCCN_CASE_4_IS_SCS=prove_by_refinement(
433 ` is_scs_v39 s /\ BBs_v39 s vv
435 /\ dimindex(:M) =scs_k_v39 s
436 /\ taustar_v39 s vv < &0
437 ==> ~(BBprime_v39 s = {})`,
443 THEN MP_TAC IS_SCS_STABLE_SYSTEM
444 THEN ASM_REWRITE_TAC[ARITH_RULE`3<4`]
446 THEN MP_TAC NOT_EMPTY_CASE_4_IS_SCS
448 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`]
449 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
450 (change_type_v3 (scs_a_v39 s)),
451 (change_type_v3 (scs_b_v39 s)),
452 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
453 (\i. (1 + i) MOD scs_k_v39 s))`
454 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
455 (change_type_v3 (scs_a_v39 s))`;`
456 (change_type_v3 (scs_b_v39 s))`;`
457 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
458 (\i. (1 + i) MOD scs_k_v39 s)`]
459 THEN MRESAL_TAC (GEN_ALL HDPLYGY)[`(scs_k_v39 s)`;`s1:stable_sy`][k_sy;B_SY1;ARITH_RULE`2<4`;]
460 THEN POP_ASSUM (fun th->
462 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
465 THEN REWRITE_TAC[BBprime_v39;IN]
466 THEN ABBREV_TAC`( vv1 i =
467 if i MOD scs_k_v39 s = 0 then row 4 v else
468 if i MOD scs_k_v39 s = 1 then row 1 v else
469 if i MOD scs_k_v39 s = 2 then row 2 v else
471 THEN EXISTS_TAC`vv1:num->real^3`
475 ONCE_REWRITE_TAC[GSYM IN]
476 THEN MATCH_MP_TAC(GEN_ALL IN_NOT_EMPTY_B1_SY_4_IS_SCS)
477 THEN EXISTS_TAC`x:real^(M,3)finite_product`
478 THEN EXISTS_TAC`v:real^3^M`
479 THEN ASM_REWRITE_TAC[]
480 THEN POP_ASSUM MP_TAC
484 SUBGOAL_THEN`vector [ vv1 1; vv1 2; (vv1:num->real^3) 3;vv1 0] = v:real^3^M`
487 POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
488 THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 4=1/\ 2 MOD 4=2/\ 3 MOD 4=3/\ 0 MOD 4=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2)`;]
489 THEN ONCE_REWRITE_TAC[CART_EQ]
490 THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=4 <=>i=1\/ i=2\/ i=3\/ i=4`]
493 ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
494 REWRITE_TAC[num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;]
495 THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA];
502 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN]
503 THEN REPEAT STRIP_TAC
504 THEN MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_4_IS_SCS)
505 [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
506 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
507 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4)
508 [`vector [ww 1; ww 2; ww 3; ww 0]:real^3^M`;`s:scs_v39`;`ww:num->real^3`;`s1:stable_sy`;`matvec(vector [ww 1; ww 2; ww 3; ww 0]:real^3^M):real^(M,3)finite_product`;]
509 THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_4)[`ww:num->real^3`;`vector [ww 1; ww 2; ww 3; ww 0]:real^3^M`;`matvec(vector [ww 1; ww 2; ww 3; ww 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
510 THEN REPLICATE_TAC (27-23) (POP_ASSUM MP_TAC)
511 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
515 THEN POP_ASSUM(fun th-> POP_ASSUM MP_TAC
518 THEN REPLICATE_TAC (26-20) (POP_ASSUM MP_TAC)
519 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
520 THEN MRESA1_TAC th `matvec(vector [ww 1; ww 2; ww 3; ww 0]:real^3^M):real^(M,3)finite_product`);
522 MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_4_IS_SCS)
523 [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
524 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
525 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4)
526 [`vector [vv 1; vv 2; vv 3; vv 0]:real^3^M`;`s:scs_v39`;`vv:num->real^3`;`s1:stable_sy`;`matvec(vector [vv 1; vv 2; vv 3; vv 0]:real^3^M):real^(M,3)finite_product`;]
527 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
528 THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_4)[`vv:num->real^3`;`vector [vv 1; vv 2; vv 3; vv 0]:real^3^M`;`matvec(vector [vv 1; vv 2; vv 3; vv 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
529 THEN ASM_REWRITE_TAC[IN]
531 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
532 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
533 THEN MRESA1_TAC th `matvec(vector [vv 1; vv 2; vv 3; vv 0]:real^3^M):real^(M,3)finite_product`)
534 THEN REPLICATE_TAC (26-4) (POP_ASSUM MP_TAC)
535 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
537 THEN ASM_REWRITE_TAC[]
538 THEN POP_ASSUM MP_TAC
539 THEN POP_ASSUM MP_TAC
545 (*************CASE 5****************)
547 let NOT_EMPTY_CASE_5_IS_SCS=prove_by_refinement(
548 ` is_scs_v39 s /\ scs_k_v39 s=5 /\ BBs_v39 s vv
549 /\ dimindex(:M)= scs_k_v39 s
550 ==> ~({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 }={})`,
551 [REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;]
553 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`
554 THEN ABBREV_TAC`a=matvec (v:real^3^M) `
555 THEN EXISTS_TAC`a:real^(M,3)finite_product`
556 THEN MATCH_MP_TAC IN_IS_SCS_CASE_5
557 THEN ASM_REWRITE_TAC[]]);;
563 let ARITH_5_TAC =ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=5/\3<=5/\5<=5 /\ 4<=5/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)/\ 6 MOD 5=1/\ SUC 0=1/\ 1<=4/\ 4<=4/\ 1+0=1/\ 1 MOD 5=1/\ 1<=1/\ 1<=4/\ 4 MOD 5=4/\ 1+1=2/\ ~(1=0)/\ 2 MOD 5=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=4/\ 1+2=3/\ 3 MOD 5=3/\ 1<=3/\ 3<=4/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ SUC 1=2/\ SUC 4=5/\ 5 MOD 5=0/\ ~(4=0)/\ 0 MOD 5=0
564 /\ 1<=5 /\ ~(4=1)/\ ~(4=2)/\ ~(4=3)/\ SUC 5=6/\ ~(5=0)
569 let VV_IN_BALL_ANNULUS_TAC_5=
571 REPLICATE_TAC (31-23)(POP_ASSUM MP_TAC)
572 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
573 THEN MRESAL1_TAC th so[ARITH_5_TAC;IN])
579 let SCS_A_LE_NORM_5_IS_SCS=
580 fun (so:term) (so1:term)->
581 REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
582 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
583 THEN MRESAL_TAC th [so;so1][ARITH_5_TAC;IN])
585 THEN REWRITE_TAC[periodic2]
586 THEN REPEAT STRIP_TAC
587 THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
588 THEN POP_ASSUM(fun th->
591 THEN REPEAT STRIP_TAC
592 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
594 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(5=0)`;periodic]
595 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
596 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(5=0)`;periodic]
597 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`] THEN MRESA1_TAC th`i:num`)
598 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
599 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(5=0)`;periodic]
600 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`])
604 let PROVE_INEQUALITY_TAC_5=
606 MP_TAC(ARITH_RULE`(j MOD 5<5)==> (j MOD 5=0) \/ (j MOD 5=1) \/ (j MOD 5=2)\/ (j MOD 5=3)\/ (j MOD 5=4)`)
609 SCS_A_LE_NORM_5_IS_SCS th `5`;
610 SCS_A_LE_NORM_5_IS_SCS th `1`;
611 SCS_A_LE_NORM_5_IS_SCS th `2`;
612 SCS_A_LE_NORM_5_IS_SCS th `3`;
613 SCS_A_LE_NORM_5_IS_SCS th `4`];;
620 let SCS_B_LE_NORM_5_IS_SCS=
621 fun (so:term) (so1:term)->
622 REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
623 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
624 THEN MRESAL_TAC th [so;so1][ARITH_5_TAC;IN])
626 THEN REWRITE_TAC[periodic2]
627 THEN REPEAT STRIP_TAC
628 THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
629 THEN POP_ASSUM(fun th->
632 THEN REPEAT STRIP_TAC
633 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
635 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(5=0)`;periodic]
636 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
637 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(5=0)`;periodic]
638 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`] THEN MRESA1_TAC th`i:num`)
639 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
640 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(5=0)`;periodic]
641 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`])
642 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (5)`][ARITH_RULE`~(5=0)`;periodic]
643 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`])
647 let PROVE_INEQUALITY_TAC_5B=
649 MP_TAC(ARITH_RULE`(j MOD 5<5)==> (j MOD 5=0) \/ (j MOD 5=1) \/ (j MOD 5=2)\/ (j MOD 5=3)\/ (j MOD 5=4)`)
652 SCS_B_LE_NORM_5_IS_SCS th `5`;
653 SCS_B_LE_NORM_5_IS_SCS th `1`;
654 SCS_B_LE_NORM_5_IS_SCS th `2`;
655 SCS_B_LE_NORM_5_IS_SCS th `3`;
656 SCS_B_LE_NORM_5_IS_SCS th `4`];;
669 let V_SY_EQ_IMAGE_VV_TAC5=
673 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`;ARITH_5_TAC];;
676 let PROVE_E_SY_EQ_MOD_TAC_5=
679 THEN ASM_REWRITE_TAC[ARITH_5_TAC]
688 let PROOF_E_EQ_TAC_5=
691 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_5_TAC;]
695 let PROVE_E_SY_EQ_IMAGE_VV_5=
696 fun (so:term) (so1:term)->
697 MRESAL_TAC(GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`x':num`;so1;`scs_k_v39 s`][ARITH_5_TAC]
699 THEN ASM_REWRITE_TAC[ARITH_5_TAC];;
704 let IN_NOT_EMPTY_B1_SY_5_IS_SCS=prove_by_refinement(
705 `is_scs_v39 s /\ scs_k_v39 s=5 /\
706 dimindex(:M) = scs_k_v39 s/\
707 matvec (v:real^3^M) =a/\
708 (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\
709 CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\
712 if i MOD scs_k_v39 s = 0 then row 5 v else
713 if i MOD scs_k_v39 s = 1 then row 1 v else
714 if i MOD scs_k_v39 s = 2 then row 2 v else
715 if i MOD scs_k_v39 s = 3 then row 3 v else
717 ==> vv IN BBs_v39 s`,
719 REWRITE_TAC[CONDITION1_SY;CONDITION2_SY;change_type_v3]
720 THEN REPEAT STRIP_TAC
722 THEN REWRITE_TAC[is_scs_v39;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;]
723 THEN REPEAT RESA_TAC;
725 ASM_REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
726 THEN REPEAT STRIP_TAC
727 THEN ASM_REWRITE_TAC[]
728 THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
729 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`)
732 VV_IN_BALL_ANNULUS_TAC_5 `5`;
733 VV_IN_BALL_ANNULUS_TAC_5 `1`;
734 VV_IN_BALL_ANNULUS_TAC_5 `2`;
735 VV_IN_BALL_ANNULUS_TAC_5 `3`;
736 VV_IN_BALL_ANNULUS_TAC_5 `4`];
738 ASM_REWRITE_TAC[periodic]
740 THEN MRESAL_TAC MOD_EQ[`i+5:num`;`i:num`;`5:num`;`1`][ARITH_RULE`1*A=A`];
744 THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 5)` ASSUME_TAC;
746 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
748 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`5`][ARITH_RULE`~(5=0)`];
750 MRESAL_TAC DIVISION[`i:num`;`5`][ARITH_RULE`~(5=0)`]
751 THEN MRESAL_TAC DIVISION[`j:num`;`5`][ARITH_RULE`~(5=0)`]
752 THEN MP_TAC(ARITH_RULE`(i MOD 5<5)==> (i MOD 5=0) \/ (i MOD 5=1) \/ (i MOD 5=2)\/ (i MOD 5=3) \/ (i MOD 5=4)`)
755 PROVE_INEQUALITY_TAC_5 `5`;
756 PROVE_INEQUALITY_TAC_5 `1`;
757 PROVE_INEQUALITY_TAC_5 `2`;
758 PROVE_INEQUALITY_TAC_5 `3`;
759 PROVE_INEQUALITY_TAC_5 `4`];
766 THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 5)` ASSUME_TAC;
768 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
770 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`5`][ARITH_RULE`~(5=0)`];
774 MRESAL_TAC DIVISION[`i:num`;`5`][ARITH_RULE`~(5=0)`]
775 THEN MRESAL_TAC DIVISION[`j:num`;`5`][ARITH_RULE`~(5=0)`]
776 THEN MP_TAC(ARITH_RULE`(i MOD 5<5)==> (i MOD 5=0) \/ (i MOD 5=1) \/ (i MOD 5=2)\/ (i MOD 5=3) \/ (i MOD 5=4)`)
779 PROVE_INEQUALITY_TAC_5B `5`;
780 PROVE_INEQUALITY_TAC_5B `1`;
781 PROVE_INEQUALITY_TAC_5B `2`;
782 PROVE_INEQUALITY_TAC_5B `3`;
783 PROVE_INEQUALITY_TAC_5B `4`];
786 THEN ASM_REWRITE_TAC[ARITH_RULE`~(5<=3)`]
788 THEN SUBGOAL_THEN`V_SY (v:real^3^M) = IMAGE vv (:num)`ASSUME_TAC;
790 ASM_REWRITE_TAC[V_SY;rows;IMAGE;EXTENSION;IN_ELIM_THM]
794 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 5)<=> i= 1\/ i=2 \/ i=3 \/ i=4 \/ i=5`]
797 V_SY_EQ_IMAGE_VV_TAC5 `1`;
798 V_SY_EQ_IMAGE_VV_TAC5 `2`;
799 V_SY_EQ_IMAGE_VV_TAC5 `3`;
800 V_SY_EQ_IMAGE_VV_TAC5 `4`;
801 V_SY_EQ_IMAGE_VV_TAC5 `5`;];
805 THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
806 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)`)
809 PROVE_E_SY_EQ_MOD_TAC_5 `5`;
810 PROVE_E_SY_EQ_MOD_TAC_5 `1`;
811 PROVE_E_SY_EQ_MOD_TAC_5 `2`;
812 PROVE_E_SY_EQ_MOD_TAC_5 `3`;
813 PROVE_E_SY_EQ_MOD_TAC_5 `4`];
816 SUBGOAL_THEN`E_SY (v:real^3^M) = IMAGE (\i. {vv i, vv (SUC i)}) (:num)`ASSUME_TAC;
818 ASM_REWRITE_TAC[E_SY;rows;IMAGE;]
819 THEN ONCE_REWRITE_TAC[EXTENSION;]
820 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
825 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 5)<=> i= 1\/ i=2 \/ i=3 \/ i=4\/ i=5`]
832 PROOF_E_EQ_TAC_5`5`];
836 THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
837 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)`)
840 PROVE_E_SY_EQ_IMAGE_VV_5 `5` `0`;
841 PROVE_E_SY_EQ_IMAGE_VV_5 `1` `1`;
842 PROVE_E_SY_EQ_IMAGE_VV_5 `2` `2`;
843 PROVE_E_SY_EQ_IMAGE_VV_5 `3` `3`;
844 PROVE_E_SY_EQ_IMAGE_VV_5 `4` `4`];
846 SUBGOAL_THEN`F_SY (v:real^3^M) = IMAGE (\i. (vv i, vv (SUC i))) (:num)`ASSUME_TAC;
848 ASM_REWRITE_TAC[F_SY;rows;IMAGE;]
849 THEN ONCE_REWRITE_TAC[EXTENSION;]
850 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
855 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 5)<=> i= 1\/ i=2 \/ i=3 \/ i=4\/ i=5`]
862 PROOF_E_EQ_TAC_5`5`];
866 THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
867 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)`)
870 PROVE_E_SY_EQ_IMAGE_VV_5 `5` `0`;
871 PROVE_E_SY_EQ_IMAGE_VV_5 `1` `1`;
872 PROVE_E_SY_EQ_IMAGE_VV_5 `2` `2`;
873 PROVE_E_SY_EQ_IMAGE_VV_5 `3` `3`;
874 PROVE_E_SY_EQ_IMAGE_VV_5 `4` `4`];
876 REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
877 THEN ASM_REWRITE_TAC[]
878 THEN REPEAT STRIP_TAC
879 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM th])
880 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
881 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
882 THEN ASM_REWRITE_TAC[];
889 let XWITCCN_CASE_5_IS_SCS=prove_by_refinement(
890 ` is_scs_v39 s /\ BBs_v39 s vv
892 /\ dimindex(:M) =scs_k_v39 s
893 /\ taustar_v39 s vv < &0
894 ==> ~(BBprime_v39 s = {})`,
898 THEN MP_TAC IS_SCS_STABLE_SYSTEM
899 THEN ASM_REWRITE_TAC[ARITH_RULE`3<5`]
901 THEN MP_TAC NOT_EMPTY_CASE_5_IS_SCS
903 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`]
904 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
905 (change_type_v3 (scs_a_v39 s)),
906 (change_type_v3 (scs_b_v39 s)),
907 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
908 (\i. (1 + i) MOD scs_k_v39 s))`
909 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
910 (change_type_v3 (scs_a_v39 s))`;`
911 (change_type_v3 (scs_b_v39 s))`;`
912 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
913 (\i. (1 + i) MOD scs_k_v39 s)`]
914 THEN MRESAL_TAC (GEN_ALL HDPLYGY)[`(scs_k_v39 s)`;`s1:stable_sy`][k_sy;B_SY1;ARITH_RULE`2<5`;]
915 THEN POP_ASSUM (fun th->
917 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
920 THEN REWRITE_TAC[BBprime_v39;IN]
921 THEN ABBREV_TAC`( vv1 i =
922 if i MOD scs_k_v39 s = 0 then row 5 v else
923 if i MOD scs_k_v39 s = 1 then row 1 v else
924 if i MOD scs_k_v39 s = 2 then row 2 v else
925 if i MOD scs_k_v39 s = 3 then row 3 v else
927 THEN EXISTS_TAC`vv1:num->real^3`
930 ONCE_REWRITE_TAC[GSYM IN]
931 THEN MATCH_MP_TAC(GEN_ALL IN_NOT_EMPTY_B1_SY_5_IS_SCS)
932 THEN EXISTS_TAC`x:real^(M,3)finite_product`
933 THEN EXISTS_TAC`v:real^3^M`
934 THEN ASM_REWRITE_TAC[]
935 THEN POP_ASSUM MP_TAC;
937 SUBGOAL_THEN`vector [ vv1 1; vv1 2; (vv1:num->real^3) 3;vv1 4; vv1 0] = v:real^3^M`
940 POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
941 THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 5=1/\ 2 MOD 5=2/\ 3 MOD 5=3/\ 0 MOD 5=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2) /\ ~(4=0) /\ ~(4=1) /\ ~(4=2) /\ ~(4=3)/\ 4 MOD 5=4`;]
942 THEN ONCE_REWRITE_TAC[CART_EQ]
943 THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=5 <=>i=1\/ i=2\/ i=3\/ i=4\/ i=5`]
946 ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
947 REWRITE_TAC[num_CONV `4`;num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;]
948 THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA];
954 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN]
955 THEN REPEAT STRIP_TAC
956 THEN MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_5_IS_SCS)
957 [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
958 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
959 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5)
960 [`vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M`;`s:scs_v39`;`ww:num->real^3`;`s1:stable_sy`;`matvec(vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M):real^(M,3)finite_product`;]
961 THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_5)[`ww:num->real^3`;`vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M`;`matvec(vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
962 THEN REPLICATE_TAC (27-23) (POP_ASSUM MP_TAC)
963 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
967 THEN POP_ASSUM(fun th-> POP_ASSUM MP_TAC
970 THEN REPLICATE_TAC (26-20) (POP_ASSUM MP_TAC)
971 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
972 THEN MRESA1_TAC th `matvec(vector [ww 1; ww 2; ww 3; ww 4; ww 0]:real^3^M):real^(M,3)finite_product`);
974 MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_5_IS_SCS)
975 [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
976 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
977 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5)
978 [`vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M`;`s:scs_v39`;`vv:num->real^3`;`s1:stable_sy`;`matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M):real^(M,3)finite_product`;]
979 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
980 THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_5)[`vv:num->real^3`;`vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M`;`matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
981 THEN ASM_REWRITE_TAC[IN]
983 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
984 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
985 THEN MRESA1_TAC th `matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 0]:real^3^M):real^(M,3)finite_product`)
986 THEN REPLICATE_TAC (26-4) (POP_ASSUM MP_TAC)
987 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
989 THEN ASM_REWRITE_TAC[]
990 THEN POP_ASSUM MP_TAC
991 THEN POP_ASSUM MP_TAC
1001 (*************CASE 6****************)
1003 let NOT_EMPTY_CASE_6_IS_SCS=prove_by_refinement(
1004 ` is_scs_v39 s /\ scs_k_v39 s=6 /\ BBs_v39 s vv
1005 /\ dimindex(:M)= scs_k_v39 s
1006 ==> ~({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 }={})`,
1007 [REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;]
1009 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`
1010 THEN ABBREV_TAC`a=matvec (v:real^3^M) `
1011 THEN EXISTS_TAC`a:real^(M,3)finite_product`
1012 THEN MATCH_MP_TAC IN_IS_SCS_CASE_6
1013 THEN ASM_REWRITE_TAC[]]);;
1018 let ARITH_6_TAC =ARITH_RULE`1<=4/\1<=2/\1<=3/\1<=1/\2<=6/\3<=6/\5<=6 /\ 4<=6/\5<=6/\ 6<=6/\ 1<=6 /\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)/\ 6 MOD 5=1/\ SUC 0=1/\ 1<=4/\ 4<=4/\ 1+0=1/\ 1 MOD 6=1/\ 1<=1/\ 1<=4/\ 4 MOD 6=4/\ 1+1=2/\ ~(1=0)/\ 2 MOD 6=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=4/\ 1+2=3/\ 3 MOD 6=3/\ 1<=3/\ 3<=4/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ SUC 1=2/\ SUC 4=5/\ 5 MOD 6=5/\ ~(4=0)/\ 0 MOD 6=0/\ 6 MOD 6=0/\ 7 MOD 6=1 /\ SUC 6=7
1019 /\ 1<=5 /\ ~(4=1)/\ ~(4=2)/\ ~(4=3)/\ SUC 5=6/\ ~(5=0)/\ ~(6=0)
1020 /\ ~(5=1)/\ ~(5=2)/\ ~(5=3)/\ ~(5=4)`;;
1024 let VV_IN_BALL_ANNULUS_TAC_6=
1026 REPLICATE_TAC (31-23)(POP_ASSUM MP_TAC)
1027 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1028 THEN MRESAL1_TAC th so[ARITH_6_TAC;IN])
1034 let SCS_A_LE_NORM_6_IS_SCS=
1035 fun (so:term) (so1:term)->
1036 REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
1037 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1038 THEN MRESAL_TAC th [so;so1][ARITH_6_TAC;IN])
1040 THEN REWRITE_TAC[periodic2]
1041 THEN REPEAT STRIP_TAC
1042 THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
1043 THEN POP_ASSUM(fun th->
1045 THEN REWRITE_TAC[th]
1046 THEN REPEAT STRIP_TAC
1047 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
1049 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(6=0)`;periodic]
1050 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
1051 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(6=0)`;periodic]
1052 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`] THEN MRESA1_TAC th`i:num`)
1053 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
1054 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(6=0)`;periodic]
1055 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`])
1056 THEN REPEAT RESA_TAC
1059 let PROVE_INEQUALITY_TAC_6=
1061 MP_TAC(ARITH_RULE`(j MOD 6<6)==> (j MOD 6=0) \/ (j MOD 6=1) \/ (j MOD 6=2)\/ (j MOD 6=3)\/ (j MOD 6=4) \/ (j MOD 6=5)`)
1064 SCS_A_LE_NORM_6_IS_SCS th `6`;
1065 SCS_A_LE_NORM_6_IS_SCS th `1`;
1066 SCS_A_LE_NORM_6_IS_SCS th `2`;
1067 SCS_A_LE_NORM_6_IS_SCS th `3`;
1068 SCS_A_LE_NORM_6_IS_SCS th `4`;
1069 SCS_A_LE_NORM_6_IS_SCS th `5`];;
1076 let SCS_B_LE_NORM_6_IS_SCS=
1077 fun (so:term) (so1:term)->
1078 REPLICATE_TAC (33-24)(POP_ASSUM MP_TAC)
1079 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1080 THEN MRESAL_TAC th [so;so1][ARITH_6_TAC;IN])
1082 THEN REWRITE_TAC[periodic2]
1083 THEN REPEAT STRIP_TAC
1084 THEN REPLICATE_TAC (34-20)(POP_ASSUM MP_TAC)
1085 THEN POP_ASSUM(fun th->
1087 THEN REWRITE_TAC[th]
1088 THEN REPEAT STRIP_TAC
1089 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
1091 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(6=0)`;periodic]
1092 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
1093 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(6=0)`;periodic]
1094 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`] THEN MRESA1_TAC th`i:num`)
1095 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
1096 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(6=0)`;periodic]
1097 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`])
1098 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (6)`][ARITH_RULE`~(6=0)`;periodic]
1099 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`])
1100 THEN REPEAT RESA_TAC
1103 let PROVE_INEQUALITY_TAC_6B=
1105 MP_TAC(ARITH_RULE`(j MOD 6<6)==> (j MOD 6=0) \/ (j MOD 6=1) \/ (j MOD 6=2)\/ (j MOD 6=3)\/ (j MOD 6=4) \/ (j MOD 6=5)`)
1108 SCS_B_LE_NORM_6_IS_SCS th `6`;
1109 SCS_B_LE_NORM_6_IS_SCS th `1`;
1110 SCS_B_LE_NORM_6_IS_SCS th `2`;
1111 SCS_B_LE_NORM_6_IS_SCS th `3`;
1112 SCS_B_LE_NORM_6_IS_SCS th `4`;
1113 SCS_B_LE_NORM_6_IS_SCS th `5`];;
1126 let V_SY_EQ_IMAGE_VV_TAC6=
1130 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`;ARITH_6_TAC];;
1133 let PROVE_E_SY_EQ_MOD_TAC_6=
1136 THEN ASM_REWRITE_TAC[ARITH_6_TAC]
1145 let PROOF_E_EQ_TAC_6=
1148 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_6_TAC;]
1152 let PROVE_E_SY_EQ_IMAGE_VV_6=
1153 fun (so:term) (so1:term)->
1154 MRESAL_TAC(GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`x':num`;so1;`scs_k_v39 s`][ARITH_6_TAC]
1156 THEN ASM_REWRITE_TAC[ARITH_6_TAC];;
1161 let IN_NOT_EMPTY_B1_SY_6_IS_SCS=prove_by_refinement(`is_scs_v39 s /\ scs_k_v39 s=6 /\
1162 dimindex(:M) = scs_k_v39 s/\
1163 matvec (v:real^3^M) =a/\
1164 (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\
1165 CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\
1168 if i MOD scs_k_v39 s = 0 then row 6 v else
1169 if i MOD scs_k_v39 s = 1 then row 1 v else
1170 if i MOD scs_k_v39 s = 2 then row 2 v else
1171 if i MOD scs_k_v39 s = 3 then row 3 v else
1172 if i MOD scs_k_v39 s = 4 then row 4 v else
1174 ==> vv IN BBs_v39 s`,
1176 REWRITE_TAC[CONDITION1_SY;CONDITION2_SY;change_type_v3]
1177 THEN REPEAT STRIP_TAC
1179 THEN REWRITE_TAC[is_scs_v39;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;]
1180 THEN REPEAT RESA_TAC;
1183 ASM_REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
1184 THEN REPEAT STRIP_TAC
1185 THEN ASM_REWRITE_TAC[]
1186 THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
1187 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`)
1190 VV_IN_BALL_ANNULUS_TAC_6 `6`;
1191 VV_IN_BALL_ANNULUS_TAC_6 `1`;
1192 VV_IN_BALL_ANNULUS_TAC_6 `2`;
1193 VV_IN_BALL_ANNULUS_TAC_6 `3`;
1194 VV_IN_BALL_ANNULUS_TAC_6 `4`;
1195 VV_IN_BALL_ANNULUS_TAC_6 `5`];
1198 ASM_REWRITE_TAC[periodic]
1200 THEN MRESAL_TAC MOD_EQ[`i+6:num`;`i:num`;`6:num`;`1`][ARITH_RULE`1*A=A`];
1205 THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 6)` ASSUME_TAC;
1208 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
1210 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`6`][ARITH_RULE`~(6=0)`];
1213 MRESAL_TAC DIVISION[`i:num`;`6`][ARITH_RULE`~(6=0)`]
1214 THEN MRESAL_TAC DIVISION[`j:num`;`6`][ARITH_RULE`~(6=0)`]
1215 THEN MP_TAC(ARITH_RULE`(i MOD 6<6)==> (i MOD 6=0) \/ (i MOD 6=1) \/ (i MOD 6=2)\/ (i MOD 6=3) \/ (i MOD 6=4) \/ (i MOD 6=5)`)
1218 PROVE_INEQUALITY_TAC_6 `6`;
1219 PROVE_INEQUALITY_TAC_6 `1`;
1220 PROVE_INEQUALITY_TAC_6 `2`;
1221 PROVE_INEQUALITY_TAC_6 `3`;
1222 PROVE_INEQUALITY_TAC_6 `4`;
1223 PROVE_INEQUALITY_TAC_6 `5`];
1231 THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 6)` ASSUME_TAC;
1234 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
1236 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`6`][ARITH_RULE`~(6=0)`];
1239 MRESAL_TAC DIVISION[`i:num`;`6`][ARITH_RULE`~(6=0)`]
1240 THEN MRESAL_TAC DIVISION[`j:num`;`6`][ARITH_RULE`~(6=0)`]
1241 THEN MP_TAC(ARITH_RULE`(i MOD 6<6)==> (i MOD 6=0) \/ (i MOD 6=1) \/ (i MOD 6=2)\/ (i MOD 6=3) \/ (i MOD 6=4) \/ (i MOD 6=5)`)
1244 PROVE_INEQUALITY_TAC_6B `6`;
1245 PROVE_INEQUALITY_TAC_6B `1`;
1246 PROVE_INEQUALITY_TAC_6B `2`;
1247 PROVE_INEQUALITY_TAC_6B `3`;
1248 PROVE_INEQUALITY_TAC_6B `4`;
1249 PROVE_INEQUALITY_TAC_6B `5`];
1254 THEN ASM_REWRITE_TAC[ARITH_RULE`~(5<=3)`]
1256 THEN SUBGOAL_THEN`V_SY (v:real^3^M) = IMAGE vv (:num)`ASSUME_TAC;
1259 ASM_REWRITE_TAC[V_SY;rows;IMAGE;EXTENSION;IN_ELIM_THM]
1264 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 6)<=> i= 1\/ i=2 \/ i=3 \/ i=4 \/ i=5\/ i=6`]
1267 V_SY_EQ_IMAGE_VV_TAC6 `1`;
1268 V_SY_EQ_IMAGE_VV_TAC6 `2`;
1269 V_SY_EQ_IMAGE_VV_TAC6 `3`;
1270 V_SY_EQ_IMAGE_VV_TAC6 `4`;
1271 V_SY_EQ_IMAGE_VV_TAC6 `5`;
1272 V_SY_EQ_IMAGE_VV_TAC6 `6`;];
1276 THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
1277 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)`)
1280 PROVE_E_SY_EQ_MOD_TAC_6 `6`;
1281 PROVE_E_SY_EQ_MOD_TAC_6 `1`;
1282 PROVE_E_SY_EQ_MOD_TAC_6 `2`;
1283 PROVE_E_SY_EQ_MOD_TAC_6 `3`;
1284 PROVE_E_SY_EQ_MOD_TAC_6 `4`;
1285 PROVE_E_SY_EQ_MOD_TAC_6 `5`;];
1289 SUBGOAL_THEN`E_SY (v:real^3^M) = IMAGE (\i. {vv i, vv (SUC i)}) (:num)`ASSUME_TAC;
1292 ASM_REWRITE_TAC[E_SY;rows;IMAGE;]
1293 THEN ONCE_REWRITE_TAC[EXTENSION;]
1294 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1300 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 6)<=> i= 1\/ i=2 \/ i=3 \/ i=4\/ i=5 \/ i=6`]
1303 PROOF_E_EQ_TAC_6`1`;
1304 PROOF_E_EQ_TAC_6`2`;
1305 PROOF_E_EQ_TAC_6`3`;
1306 PROOF_E_EQ_TAC_6`4`;
1307 PROOF_E_EQ_TAC_6`5`;
1308 PROOF_E_EQ_TAC_6`6`];
1313 THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
1314 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)`)
1317 PROVE_E_SY_EQ_IMAGE_VV_6 `6` `0`;
1318 PROVE_E_SY_EQ_IMAGE_VV_6 `1` `1`;
1319 PROVE_E_SY_EQ_IMAGE_VV_6 `2` `2`;
1320 PROVE_E_SY_EQ_IMAGE_VV_6 `3` `3`;
1321 PROVE_E_SY_EQ_IMAGE_VV_6 `4` `4`;
1322 PROVE_E_SY_EQ_IMAGE_VV_6 `5` `5`];
1325 SUBGOAL_THEN`F_SY (v:real^3^M) = IMAGE (\i. (vv i, vv (SUC i))) (:num)`ASSUME_TAC;
1328 ASM_REWRITE_TAC[F_SY;rows;IMAGE;]
1329 THEN ONCE_REWRITE_TAC[EXTENSION;]
1330 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1336 ASM_REWRITE_TAC[ARITH_RULE`(1 <= i /\ i <= 6)<=> i= 1\/ i=2 \/ i=3 \/ i=4\/ i=5 \/ i=6`]
1339 PROOF_E_EQ_TAC_6`1`;
1340 PROOF_E_EQ_TAC_6`2`;
1341 PROOF_E_EQ_TAC_6`3`;
1342 PROOF_E_EQ_TAC_6`4`;
1343 PROOF_E_EQ_TAC_6`5`;
1344 PROOF_E_EQ_TAC_6`6`];
1349 THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
1350 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)`)
1353 PROVE_E_SY_EQ_IMAGE_VV_6 `6` `0`;
1354 PROVE_E_SY_EQ_IMAGE_VV_6 `1` `1`;
1355 PROVE_E_SY_EQ_IMAGE_VV_6 `2` `2`;
1356 PROVE_E_SY_EQ_IMAGE_VV_6 `3` `3`;
1357 PROVE_E_SY_EQ_IMAGE_VV_6 `4` `4`;
1358 PROVE_E_SY_EQ_IMAGE_VV_6 `5` `5`];
1361 REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
1362 THEN ASM_REWRITE_TAC[]
1363 THEN REPEAT STRIP_TAC
1364 THEN POP_ASSUM (fun th->REWRITE_TAC[SYM th])
1365 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1366 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
1367 THEN ASM_REWRITE_TAC[];
1374 let XWITCCN_CASE_6_IS_SCS=prove_by_refinement(
1375 ` is_scs_v39 s /\ BBs_v39 s vv
1377 /\ dimindex(:M) =scs_k_v39 s
1378 /\ taustar_v39 s vv < &0
1379 ==> ~(BBprime_v39 s = {})`,
1383 THEN MP_TAC IS_SCS_STABLE_SYSTEM
1384 THEN ASM_REWRITE_TAC[ARITH_RULE`3<6`]
1386 THEN MP_TAC NOT_EMPTY_CASE_6_IS_SCS
1388 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`]
1389 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
1390 (change_type_v3 (scs_a_v39 s)),
1391 (change_type_v3 (scs_b_v39 s)),
1392 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
1393 (\i. (1 + i) MOD scs_k_v39 s))`
1394 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
1395 (change_type_v3 (scs_a_v39 s))`;`
1396 (change_type_v3 (scs_b_v39 s))`;`
1397 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
1398 (\i. (1 + i) MOD scs_k_v39 s)`]
1399 THEN MRESAL_TAC (GEN_ALL HDPLYGY)[`(scs_k_v39 s)`;`s1:stable_sy`][k_sy;B_SY1;ARITH_RULE`2<6`;]
1400 THEN POP_ASSUM (fun th->
1402 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1405 THEN REWRITE_TAC[BBprime_v39;IN]
1406 THEN ABBREV_TAC`( vv1 i =
1407 if i MOD scs_k_v39 s = 0 then row 6 v else
1408 if i MOD scs_k_v39 s = 1 then row 1 v else
1409 if i MOD scs_k_v39 s = 2 then row 2 v else
1410 if i MOD scs_k_v39 s = 3 then row 3 v else
1411 if i MOD scs_k_v39 s = 4 then row 4 v else
1412 row 5 (v:real^3^M))`
1413 THEN EXISTS_TAC`vv1:num->real^3`
1416 ONCE_REWRITE_TAC[GSYM IN]
1417 THEN MATCH_MP_TAC(GEN_ALL IN_NOT_EMPTY_B1_SY_6_IS_SCS)
1418 THEN EXISTS_TAC`x:real^(M,3)finite_product`
1419 THEN EXISTS_TAC`v:real^3^M`
1420 THEN ASM_REWRITE_TAC[]
1421 THEN POP_ASSUM MP_TAC;
1423 SUBGOAL_THEN`vector [ vv1 1; vv1 2; (vv1:num->real^3) 3;vv1 4; vv1 5; vv1 0] = v:real^3^M`
1426 POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
1427 THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 6=1/\ 2 MOD 6=2/\ 3 MOD 6=3/\ 0 MOD 6
1428 =0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2) /\ ~(4=0) /\ ~(4=1) /\ ~(4=2) /\ ~(4=3)/\ 4 MOD 6=4/\ 5 MOD 6=5/\ ~(1=5)/\ ~(2=5)/\ ~(3=5)/\ ~(4=5)/\ ~(0=5)`;]
1429 THEN ONCE_REWRITE_TAC[CART_EQ]
1430 THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=6
1431 <=>i=1\/ i=2\/ i=3\/ i=4\/ i=5\/ i=6`]
1432 THEN REPEAT RESA_TAC
1434 ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
1435 REWRITE_TAC[num_CONV `4`;num_CONV `5`;num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;]
1436 THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA];
1442 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN]
1443 THEN REPEAT STRIP_TAC
1444 THEN MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_6_IS_SCS)
1445 [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
1446 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
1447 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6)
1448 [`vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M`;`s:scs_v39`;`ww:num->real^3`;`s1:stable_sy`;`matvec(vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M):real^(M,3)finite_product`;]
1449 THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_6)[`ww:num->real^3`;`vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M`;`matvec(vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
1450 THEN REPLICATE_TAC (27-23) (POP_ASSUM MP_TAC)
1451 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
1453 THEN REWRITE_TAC[IN]
1455 THEN POP_ASSUM(fun th-> POP_ASSUM MP_TAC
1456 THEN REWRITE_TAC[th]
1458 THEN REPLICATE_TAC (26-20) (POP_ASSUM MP_TAC)
1459 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1460 THEN MRESA1_TAC th `matvec(vector [ww 1; ww 2; ww 3; ww 4;ww 5; ww 0]:real^3^M):real^(M,3)finite_product`);
1462 MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_6_IS_SCS)
1463 [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
1464 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6)[`v:real^3^M`;`s:scs_v39`;`vv1:num->real^3`;`s1:stable_sy`;`x:real^(M,3)finite_product`]
1465 THEN MRESA_TAC ( GEN_ALL TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6)
1466 [`vector [vv 1; vv 2; vv 3; vv 4; vv 5; vv 0]:real^3^M`;`s:scs_v39`;`vv:num->real^3`;`s1:stable_sy`;`matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 5; vv 0]:real^3^M):real^(M,3)finite_product`;]
1467 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MP_TAC th)
1468 THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_6)[`vv:num->real^3`;`vector [vv 1; vv 2; vv 3; vv 4; vv 5; vv 0]:real^3^M`;`matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 5; vv 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`;]
1469 THEN ASM_REWRITE_TAC[IN]
1471 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
1472 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1473 THEN MRESA1_TAC th `matvec(vector [vv 1; vv 2; vv 3; vv 4; vv 5;vv 0]:real^3^M):real^(M,3)finite_product`)
1474 THEN REPLICATE_TAC (26-4) (POP_ASSUM MP_TAC)
1475 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1477 THEN ASM_REWRITE_TAC[]
1478 THEN POP_ASSUM MP_TAC
1479 THEN POP_ASSUM MP_TAC
1480 THEN REAL_ARITH_TAC;
1486 (****************CASE 3**************)
1488 let IS_SCS_IN_BALL_ANNULUS_3=
1490 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1491 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1492 THEN MP_TAC th THEN REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM])
1494 THEN POP_ASSUM MATCH_MP_TAC
1496 THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ 3<=3/\ 3 MOD 3= 0 /\ 1 MOD 3= 1 /\ 2 MOD 3= 2/\ 3 MOD 3= 0/\ ~(2=1)
1497 /\ 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)`]
1502 let IN_IS_SCS_CASE_3=prove_by_refinement(
1503 ` is_scs_v39 s /\ scs_k_v39 s=3 /\ BBs_v39 s vv
1504 /\ dimindex(:M)= scs_k_v39 s
1505 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 0]:real^3^M= v
1506 /\ matvec (v:real^3^M) =a
1508 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 }`,
1511 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]
1514 EXISTS_TAC`v:real^3^M`
1515 THEN ASM_REWRITE_TAC[]
1518 REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 3)<=> (i=1\/ i=2\/ i=3)`]
1519 THEN REPEAT STRIP_TAC
1521 IS_SCS_IN_BALL_ANNULUS_3 `1`;
1522 IS_SCS_IN_BALL_ANNULUS_3 `2`;
1523 IS_SCS_IN_BALL_ANNULUS_3 `0`];
1525 REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 3)<=> (i=1\/ i=2\/ i=3 )`]
1528 THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 3==> (i=1\/ i=2\/ i=3)`)
1530 THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ 3<=3/\ 3 MOD 3= 0 /\ 1 MOD 3= 1 /\ 2 MOD 3= 2/\ 3 MOD 3= 0/\ ~(2=1)
1531 /\ 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)`]
1533 THEN REWRITE_TAC[is_scs_v39;periodic2]
1535 THEN REPEAT DISCH_TAC
1536 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 1`][periodic;ARITH_RULE`~(3=0)`]
1537 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1538 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1539 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 1`][periodic;ARITH_RULE`~(3=0)`]
1540 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1541 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1542 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 2`][periodic;ARITH_RULE`~(3=0)`]
1543 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1544 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1545 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 2`][periodic;ARITH_RULE`~(3=0)`]
1546 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1547 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1548 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 3`][periodic;ARITH_RULE`~(3=0)`]
1549 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1550 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1551 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 3`][periodic;ARITH_RULE`~(3=0)`]
1552 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1553 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1554 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 0`][periodic;ARITH_RULE`~(3=0)`]
1555 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1556 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1557 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(3=0)`]
1558 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1559 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[ SYM th;NORM_SUB;])
1560 THEN REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0;REAL_ARITH`&0<= &0`];
1562 EXISTS_TAC`v:real^3^M`
1563 THEN ASM_REWRITE_TAC[]
1566 REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 3)<=> (i=1\/ i=2\/ i=3)`]
1567 THEN REPEAT STRIP_TAC
1569 IS_SCS_IN_BALL_ANNULUS_3 `1`;
1570 IS_SCS_IN_BALL_ANNULUS_3 `2`;
1571 IS_SCS_IN_BALL_ANNULUS_3 `0`];
1573 REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 3)<=> (i=1\/ i=2\/ i=3 )`]
1576 THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 3==> (i=1\/ i=2\/ i=3)`)
1578 THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ 3<=3/\ 3 MOD 3= 0 /\ 1 MOD 3= 1 /\ 2 MOD 3= 2/\ 3 MOD 3= 0/\ ~(2=1)
1579 /\ 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)`]
1581 THEN REWRITE_TAC[is_scs_v39;periodic2]
1583 THEN REPEAT DISCH_TAC
1584 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 1`][periodic;ARITH_RULE`~(3=0)`]
1585 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1586 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1587 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 1`][periodic;ARITH_RULE`~(3=0)`]
1588 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1589 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1590 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 2`][periodic;ARITH_RULE`~(3=0)`]
1591 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1592 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1593 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 2`][periodic;ARITH_RULE`~(3=0)`]
1594 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1595 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1596 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 3`][periodic;ARITH_RULE`~(3=0)`]
1597 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1598 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1599 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 3`][periodic;ARITH_RULE`~(3=0)`]
1600 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1601 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1602 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 0`][periodic;ARITH_RULE`~(3=0)`]
1603 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1604 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1605 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(3=0)`]
1606 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3`[ARITH_RULE`3 MOD 3=0`])
1607 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[ SYM th;NORM_SUB;])
1608 THEN REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0;REAL_ARITH`&0<= &0`];
1613 let ARITH_3_TAC =ARITH_RULE`1<=3/\1<=2/\1<=3/\1<=1/\2<=3/\3<=3/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)/\ 0 MOD 3=0/\ 1 MOD 3=1/\ 2 MOD 3=2/\ 3 MOD 3=0/\ SUC 0=1 /\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ 0<3/\ a+0=a/\ 0+a=a/\ 3-1=2/\ 3-2=1/\ 3-0=3/\ 3-3=0`;;
1618 let VV_IN_BALL_ANNULUS_TAC_3=
1620 REPLICATE_TAC (30-23)(POP_ASSUM MP_TAC)
1621 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1622 THEN MRESAL1_TAC th so[ARITH_RULE`1<=3/\1<=2/\1<=3/\1<=1/\2<=3/\3<=3/\4<=4/\ ~(1=0)/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)/\ ~(3=1)/\ ~(3=2)`;IN])
1626 let SCS_A_LE_NORM_3_IS_SCS=
1627 fun (so:term) (so1:term)->
1628 REPLICATE_TAC (32-24)(POP_ASSUM MP_TAC)
1629 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1630 THEN MRESAL_TAC th [so;so1][ARITH_3_TAC;IN])
1632 THEN REWRITE_TAC[periodic2]
1633 THEN REPEAT STRIP_TAC
1634 THEN REPLICATE_TAC (33-20)(POP_ASSUM MP_TAC)
1635 THEN POP_ASSUM(fun th->
1637 THEN REWRITE_TAC[th]
1638 THEN REPEAT STRIP_TAC
1639 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
1641 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
1642 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
1643 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(3=0)`;periodic]
1644 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`] THEN MRESA1_TAC th`i:num`)
1645 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
1646 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(3=0)`;periodic]
1647 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`])
1648 THEN REPEAT RESA_TAC
1651 let PROVE_INEQUALITY_TAC_3=
1653 MP_TAC(ARITH_RULE`(j MOD 3<3)==> (j MOD 3=0) \/ (j MOD 3=1) \/ (j MOD 3=2)`)
1656 SCS_A_LE_NORM_3_IS_SCS th `3`;
1657 SCS_A_LE_NORM_3_IS_SCS th `1`;
1658 SCS_A_LE_NORM_3_IS_SCS th `2`;];;
1663 let SCS_B_LE_NORM_3_IS_SCS=
1664 fun (so:term) (so1:term)->
1665 REPLICATE_TAC (32-24)(POP_ASSUM MP_TAC)
1666 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1667 THEN MRESAL_TAC th [so;so1][ARITH_3_TAC;IN])
1669 THEN REWRITE_TAC[periodic2]
1670 THEN REPEAT STRIP_TAC
1671 THEN REPLICATE_TAC (33-20)(POP_ASSUM MP_TAC)
1672 THEN POP_ASSUM(fun th->
1674 THEN REWRITE_TAC[th]
1675 THEN REPEAT STRIP_TAC
1676 THEN REPLICATE_TAC (2)(POP_ASSUM MP_TAC)
1678 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
1679 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
1680 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][ARITH_RULE`~(3=0)`;periodic]
1681 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`] THEN MRESA1_TAC th`i:num`)
1682 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
1683 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][ARITH_RULE`~(3=0)`;periodic]
1684 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`])
1685 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (3)`][ARITH_RULE`~(3=0)`;periodic]
1686 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`])
1687 THEN REPEAT RESA_TAC
1690 let PROVE_INEQUALITY_TAC_3B=
1692 MP_TAC(ARITH_RULE`(j MOD 3<3)==> (j MOD 3=0) \/ (j MOD 3=1) \/ (j MOD 3=2)`)
1695 SCS_B_LE_NORM_3_IS_SCS th `3`;
1696 SCS_B_LE_NORM_3_IS_SCS th `1`;
1697 SCS_B_LE_NORM_3_IS_SCS th `2`;];;
1701 let IN_NOT_EMPTY_B1_SY_3_IS_SCS=prove_by_refinement(
1702 `is_scs_v39 s /\ scs_k_v39 s=3 /\
1703 dimindex(:M) = scs_k_v39 s/\
1704 matvec (v:real^3^M) =a/\
1705 (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\
1706 CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ (!i. vv i =
1707 if i MOD scs_k_v39 s = 0 then row 3 v else
1708 if i MOD scs_k_v39 s = 1 then row 1 v else
1710 ==> vv IN BBs_v39 s`,
1712 REWRITE_TAC[CONDITION1_SY;CONDITION2_SY;change_type_v3]
1713 THEN REPEAT STRIP_TAC
1715 THEN REWRITE_TAC[is_scs_v39;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;]
1716 THEN REPEAT RESA_TAC;
1718 ASM_REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
1719 THEN REPEAT STRIP_TAC
1720 THEN ASM_REWRITE_TAC[]
1721 THEN MRESAL_TAC DIVISION[`x':num`;`3`][ARITH_RULE`~(3=0)`]
1722 THEN MP_TAC(ARITH_RULE`x' MOD 3<3 ==> x' MOD 3 = 0 \/ x' MOD 3 = 1 \/ x' MOD 3 = 2 `)
1725 VV_IN_BALL_ANNULUS_TAC_3 `3`;
1726 VV_IN_BALL_ANNULUS_TAC_3 `1`;
1727 VV_IN_BALL_ANNULUS_TAC_3 `2`;];
1730 ASM_REWRITE_TAC[periodic]
1732 THEN MRESAL_TAC MOD_EQ[`i+3:num`;`i:num`;`3:num`;`1`][ARITH_RULE`1*A=A`];
1736 THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 3)` ASSUME_TAC;
1738 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
1740 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`3`][ARITH_RULE`~(3=0)`];
1742 MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
1743 THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`]
1744 THEN MP_TAC(ARITH_RULE`(i MOD 3<3)==> (i MOD 3=0) \/ (i MOD 3=1) \/ (i MOD 3=2)`)
1747 PROVE_INEQUALITY_TAC_3 `3`;
1748 PROVE_INEQUALITY_TAC_3 `1`;
1749 PROVE_INEQUALITY_TAC_3 `2`;];
1754 THEN SUBGOAL_THEN`!i. (vv:num->real^3) i= vv (i MOD 3)` ASSUME_TAC;
1756 POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
1758 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`3`][ARITH_RULE`~(3=0)`];
1760 MRESAL_TAC DIVISION[`i:num`;`3`][ARITH_RULE`~(3=0)`]
1761 THEN MRESAL_TAC DIVISION[`j:num`;`3`][ARITH_RULE`~(3=0)`]
1762 THEN MP_TAC(ARITH_RULE`(i MOD 3<3)==> (i MOD 3=0) \/ (i MOD 3=1) \/ (i MOD 3=2)`)
1765 PROVE_INEQUALITY_TAC_3B `3`;
1766 PROVE_INEQUALITY_TAC_3B `1`;
1767 PROVE_INEQUALITY_TAC_3B `2`;];
1769 REWRITE_TAC[ARITH_RULE`3<=3`];
1775 let NOT_EMPTY_CASE_3_IS_SCS=prove_by_refinement(
1776 ` is_scs_v39 s /\ scs_k_v39 s=3 /\ BBs_v39 s vv
1777 /\ dimindex(:M)= scs_k_v39 s
1778 ==> ~({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 }={})`,
1779 [REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;]
1781 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 0]:real^3^M`
1782 THEN ABBREV_TAC`a=matvec (v:real^3^M) `
1783 THEN EXISTS_TAC`a:real^(M,3)finite_product`
1784 THEN MATCH_MP_TAC IN_IS_SCS_CASE_3
1785 THEN ASM_REWRITE_TAC[]]);;
1792 let J1_TS=new_definition `J1_TS (s:tri_sy)= {x| ?i. {i MOD 3,f_ts s (i MOD (3))} IN J_TS s /\ i IN 1..3 /\ x=i,SUC(i MOD (3))}`;;
1797 let d_fun3=new_definition `d_fun3 (s1:scs_v39)(s:tri_sy,l:real^(M,3)finite_product) = (d_ts s) + #0.1 * (if is_ear_v39 s1 then &1 else -- &1) * sum (J1_TS s) (\x. cstab -norm (row (FST x) (vecmats l) - row (SND x) (vecmats l) ))`;;
1801 let FINITE_J1_TS=prove(`!s:tri_sy .
1804 THEN REWRITE_TAC[J1_TS]
1805 THEN MRESAL_TAC FINITE_IMAGE[`(\i. i, SUC(i MOD (3)))`;`1..3`][FINITE_NUMSEG;IMAGE]
1806 THEN MATCH_MP_TAC FINITE_SUBSET
1807 THEN EXISTS_TAC`{y | ?x. x IN 1..(3) /\ y = x,SUC(x MOD (3))}`
1808 THEN ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM]
1809 THEN REPEAT RESA_TAC
1810 THEN EXISTS_TAC`i:num`
1811 THEN ASM_REWRITE_TAC[]);;
1813 let INDEX_J1_TS=prove(`!s:tri_sy .
1814 x IN J1_TS s ==> 1 <= FST x /\ FST x <= 3`,
1815 REWRITE_TAC[J1_TS;IN_ELIM_THM;IN_NUMSEG]
1816 THEN REPEAT STRIP_TAC
1817 THEN ASM_REWRITE_TAC[]);;
1821 let CONTINUOUS_ON_D_FUN3=prove(`!s:tri_sy .
1823 k_ts s =k /\ dimindex(:M) =k/\ I_TS s= 0..k-1 /\ f_ts s=(\i. ((1+i):num MOD k))
1824 ==> lift o(\l:real^(M,3)finite_product. d_fun3 s1 (s,l)) continuous_on (
1825 {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY (a_ts s) (b_ts s) v })`,
1827 THEN REWRITE_TAC[d_fun3;LIFT_ADD;o_DEF;]
1828 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
1829 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;]
1830 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
1831 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
1832 THEN ASSUME_TAC FINITE_J1_TS
1833 THEN POP_ASSUM(fun th -> MRESA1_TAC th`s:tri_sy`)
1834 THEN ASM_SIMP_TAC[LIFT_SUM;o_DEF]
1835 THEN MATCH_MP_TAC CONTINUOUS_ON_VSUM
1836 THEN ASM_REWRITE_TAC[]
1837 THEN REPEAT STRIP_TAC
1838 THEN REWRITE_TAC[LIFT_SUB]
1839 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
1840 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;]
1841 THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE
1842 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
1845 MATCH_MP_TAC CONTINUOUS_ON_ROW
1846 THEN POP_ASSUM MP_TAC
1847 THEN REWRITE_TAC[J1_TS;IN_ELIM_THM;IN_NUMSEG]
1848 THEN REPEAT RESA_TAC;
1850 MATCH_MP_TAC CONTINUOUS_ON_ROW
1851 THEN POP_ASSUM MP_TAC
1852 THEN REWRITE_TAC[J1_TS;IN_ELIM_THM;IN_NUMSEG]
1853 THEN REPEAT RESA_TAC
1854 THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
1855 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
1856 THEN POP_ASSUM MP_TAC
1864 let tri_sy_explicit = prove_by_refinement(
1865 `!k d s a b J f. tri_stable k d s a b J f ==> k_ts (tri_sy (k,d,s, a,b,J,f)) = k/\
1866 d_ts (tri_sy (k,d,s, a,b,J,f)) = d /\
1867 a_ts (tri_sy (k,d,s, a,b,J,f)) = a /\
1868 b_ts (tri_sy (k,d,s, a,b,J,f)) = b /\
1869 J_TS (tri_sy (k,d,s, a,b,J,f)) = J /\
1870 I_TS (tri_sy (k,d,s, a,b,J,f)) = s /\
1871 f_ts (tri_sy (k,d,s, a,b,J,f)) = f `,
1873 [ REWRITE_TAC[k_ts;d_ts;a_ts;b_ts;J_TS;I_TS;f_ts;tri_sy_tybij;]
1874 THEN MP_TAC tri_sy_tybij
1878 THEN POP_ASSUM(fun th->
1879 POP_ASSUM (fun th1-> ASSUME_TAC th THEN MRESA1_TAC th1`(k,d,s,a,b,J,f):(num#real#(num->bool)#(num#num->real)#(num#num->real)#((num->bool)->bool)#(num->num))`))
1886 let IN_B_SY1_COLLINEAR_CASE_3_IS_SCS=prove_by_refinement(
1889 dimindex(:M)= scs_k_v39 s
1891 (!a. 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 }
1892 ==> ~collinear{vec 0, row 1 (vecmats a),row 2 (vecmats a)}/\
1893 ~collinear{vec 0, row 1 (vecmats a),row 3 (vecmats a)}/\
1894 ~collinear{vec 0, row 2 (vecmats a),row 3 (vecmats a)})`,
1897 REWRITE_TAC[IN_ELIM_THM;]
1901 THEN ABBREV_TAC`( vv i =
1902 if i MOD scs_k_v39 s = 0 then row 3 v else
1903 if i MOD scs_k_v39 s = 1 then row 1 v else
1904 row 2 (v:real^3^M))`
1905 THEN MP_TAC IN_NOT_EMPTY_B1_SY_3_IS_SCS
1906 THEN ASM_REWRITE_TAC[]
1907 THEN POP_ASSUM MP_TAC
1908 THEN ASM_REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
1911 THEN MP_TAC IS_SCS_NOT_COLLINEAR_BBs_CASE_3
1914 SUBGOAL_THEN`vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 0]:real^3^M
1917 REPLICATE_TAC 4 (REMOVE_ASSUM_TAC)
1918 THEN POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
1919 THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 3=1/\ 2 MOD 3=2/\ 3 MOD 3=0/\ 0 MOD 3=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2)`;]
1920 THEN ONCE_REWRITE_TAC[CART_EQ]
1921 THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=3 <=>i=1\/ i=2\/ i=3`]
1922 THEN REPEAT RESA_TAC
1924 ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
1925 REWRITE_TAC[num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;]
1926 THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA];
1928 MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`];
1934 let HDPLYGY_CASE_30=prove_by_refinement(
1935 `tri_stable k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M)
1937 /\ ~({matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v } = {}:real^(M,3)finite_product->bool)
1938 /\ (!l. l IN {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v }
1939 ==> ~collinear{vec 0, row 1 (vecmats l),row 2 (vecmats l)}/\
1940 ~collinear{vec 0, row 1 (vecmats l),row 3 (vecmats l)}/\
1941 ~collinear{vec 0, row 2 (vecmats l),row 3 (vecmats l)})
1942 /\ k_ts s = 3 /\ I_TS s = 0..3 - 1 /\ f_ts s = (\i. (1 + i) MOD 3)
1943 /\ a_ts s =a /\ b_ts s =b
1944 ==> ?x:real^(M,3)finite_product. x IN ({matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v })
1945 /\ (!y:real^(M,3)finite_product. y IN ({matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v })
1946 ==> tau3 (row 1 (vecmats (x:real^(M,3)finite_product))) (row 2 (vecmats x)) (row 3 ( vecmats x))
1948 <= tau3 (row 1 (vecmats y)) (row 2 (vecmats y)) (row 3 (vecmats y))
1955 THEN MP_TAC TRI_STABLE_K_EQ_3
1957 THEN MRESA_TAC CONTINUOUS_ATTAINS_INF[`(\x:real^(M,3)finite_product. tau3 (row 1 (vecmats (x:real^(M,3)finite_product))) (row 2 (vecmats x)) (row 3 ( vecmats x))- d_fun3 s1 (s,x))`;`{matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v }:real^(M,3)finite_product->bool`]
1958 THEN POP_ASSUM MATCH_MP_TAC
1961 POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1962 THEN MATCH_MP_TAC COMPACT_TRI_STABLE
1963 THEN ASM_REWRITE_TAC[];
1965 SIMP_TAC[o_DEF;LIFT_SUM;FINITE_NUMSEG; o_DEF;LIFT_SUB;LIFT_SUM;REAL_ARITH`A+B+C-D=((A+B)+C)-D`]
1966 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
1967 THEN ONCE_REWRITE_TAC[SET_RULE`A/\B <=> B/\ A`]
1970 MRESAL_TAC(GEN_ALL CONTINUOUS_ON_D_FUN3)[`k:num`;`s1:scs_v39`;`s:tri_sy`][o_DEF];
1973 THEN REPLICATE_TAC 5(REMOVE_ASSUM_TAC)
1975 THEN SIMP_TAC[o_DEF;LIFT_SUM;FINITE_NUMSEG;tau3; o_DEF;LIFT_SUB;LIFT_SUM;REAL_ARITH`A+B+C-D=((A+B)+C)-D`]
1976 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
1977 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
1978 THEN SIMP_TAC[o_DEF;LIFT_ADD;]
1979 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
1983 SIMP_TAC[o_DEF;LIFT_ADD;]
1984 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
1988 SIMP_TAC[o_DEF;LIFT_CMUL;FINITE_NUMSEG]
1989 THEN REPEAT STRIP_TAC
1990 THEN MATCH_MP_TAC CONTINUOUS_ON_MUL
1994 REWRITE_TAC[rho;o_DEF;LIFT_ADD]
1995 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
1996 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
1997 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
1998 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
1999 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
2000 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
2001 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
2002 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2003 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
2004 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
2005 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
2006 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2007 THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE
2008 THEN MATCH_MP_TAC CONTINUOUS_ON_ROW
2009 THEN ASM_REWRITE_TAC[IN_NUMSEG]
2012 REWRITE_TAC[CONTINUOUS_ON_SEQUENTIALLY;o_DEF]
2013 THEN REPEAT STRIP_TAC
2014 THEN MP_TAC (GEN_ALL SEQUENTIALLY_DIVH)
2015 THEN REWRITE_TAC[o_DEF]
2017 THEN POP_ASSUM MATCH_MP_TAC
2018 THEN MRESAL_TAC (GEN_ALL LIM_VECMAT)[`(\n:num. vecmats ((x:num->real^(M,3)finite_product) n))`;`vecmats(a':real^(M,3)finite_product)`][MATVEC_VECMATS_ID;ETA_AX]
2019 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1`[ARITH_RULE`1<=1/\ 1<=3`]
2020 THEN MRESAL1_TAC th`2`[ARITH_RULE`1<=2/\ 2<=3`]
2021 THEN MRESAL1_TAC th`3`[ARITH_RULE`1<=3/\ 3<=3`])
2022 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
2023 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2024 THEN MRESA1_TAC th `a':real^(M,3)finite_product`
2027 THEN POP_ASSUM(fun th-> MRESA1_TAC th `(x (n:num)):real^(M,3)finite_product`)
2033 SIMP_TAC[o_DEF;LIFT_CMUL;FINITE_NUMSEG]
2034 THEN REPEAT STRIP_TAC
2035 THEN MATCH_MP_TAC CONTINUOUS_ON_MUL
2039 REWRITE_TAC[rho;o_DEF;LIFT_ADD]
2040 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
2041 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2042 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
2043 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2044 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
2045 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
2046 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
2047 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2048 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
2049 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
2050 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
2051 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2052 THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE
2053 THEN MATCH_MP_TAC CONTINUOUS_ON_ROW
2054 THEN ASM_REWRITE_TAC[IN_NUMSEG]
2057 REWRITE_TAC[CONTINUOUS_ON_SEQUENTIALLY;o_DEF]
2058 THEN REPEAT STRIP_TAC
2059 THEN MP_TAC (GEN_ALL SEQUENTIALLY_DIVH)
2060 THEN REWRITE_TAC[o_DEF]
2062 THEN POP_ASSUM MATCH_MP_TAC
2063 THEN MRESAL_TAC (GEN_ALL LIM_VECMAT)[`(\n:num. vecmats ((x:num->real^(M,3)finite_product) n))`;`vecmats(a':real^(M,3)finite_product)`][MATVEC_VECMATS_ID;ETA_AX]
2064 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1`[ARITH_RULE`1<=1/\ 1<=3`]
2065 THEN MRESAL1_TAC th`2`[ARITH_RULE`1<=2/\ 2<=3`]
2066 THEN MRESAL1_TAC th`3`[ARITH_RULE`1<=3/\ 3<=3`])
2067 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
2068 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2069 THEN MRESA1_TAC th `a':real^(M,3)finite_product`
2071 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2072 THEN ASM_REWRITE_TAC[]
2074 THEN POP_ASSUM(fun th-> MRESA1_TAC th `(x (n:num)):real^(M,3)finite_product`)
2075 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2076 THEN ASM_REWRITE_TAC[]
2082 SIMP_TAC[o_DEF;LIFT_CMUL;FINITE_NUMSEG]
2083 THEN REPEAT STRIP_TAC
2084 THEN MATCH_MP_TAC CONTINUOUS_ON_MUL
2088 REWRITE_TAC[rho;o_DEF;LIFT_ADD]
2089 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
2090 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2091 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
2092 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2093 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
2094 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
2095 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
2096 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2097 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
2098 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_ADD;ly;interp;REAL_ARITH`a*b=b*a`;LIFT_CMUL]
2099 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
2100 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB;]
2101 THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE
2102 THEN MATCH_MP_TAC CONTINUOUS_ON_ROW
2103 THEN ASM_REWRITE_TAC[IN_NUMSEG]
2106 REWRITE_TAC[CONTINUOUS_ON_SEQUENTIALLY;o_DEF]
2107 THEN REPEAT STRIP_TAC
2108 THEN MP_TAC (GEN_ALL SEQUENTIALLY_DIVH)
2109 THEN REWRITE_TAC[o_DEF]
2111 THEN POP_ASSUM MATCH_MP_TAC
2112 THEN MRESAL_TAC (GEN_ALL LIM_VECMAT)[`(\n:num. vecmats ((x:num->real^(M,3)finite_product) n))`;`vecmats(a':real^(M,3)finite_product)`][MATVEC_VECMATS_ID;ETA_AX]
2113 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1`[ARITH_RULE`1<=1/\ 1<=3`]
2114 THEN MRESAL1_TAC th`2`[ARITH_RULE`1<=2/\ 2<=3`]
2115 THEN MRESAL1_TAC th`3`[ARITH_RULE`1<=3/\ 3<=3`])
2116 THEN REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
2117 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2118 THEN MRESA1_TAC th `a':real^(M,3)finite_product`
2120 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2121 THEN ASM_REWRITE_TAC[]
2123 THEN POP_ASSUM(fun th-> MRESA1_TAC th `(x (n:num)):real^(M,3)finite_product`)
2124 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2125 THEN ASM_REWRITE_TAC[];
2134 let TAUSTAR_EQ_TAU_STAR_3_IS_SCS=prove_by_refinement(
2135 `is_scs_v39 s /\ BBs_v39 s vv
2138 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 0]:real^3^M= v
2139 /\ matvec (v:real^3^M) =a
2140 /\ tri_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
2141 (change_type_v3 (scs_a_v39 s)),
2142 (change_type_v3 (scs_b_v39 s)),
2143 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
2144 (\i. (1 + i) MOD scs_k_v39 s))=s1
2145 ==> taustar_v39 s vv = tau3 (vv 1) (vv 2) (vv 0) -d_fun3 s (s1,a)`,
2150 THEN ASM_REWRITE_TAC[taustar_v39;tau_star;LET_DEF;LET_END_DEF;ARITH_RULE`3<=3`;]
2151 THEN MATCH_MP_TAC(REAL_ARITH`a=b /\ c=d==> a -c= b- d`)
2156 THEN REAL_ARITH_TAC;
2158 REWRITE_TAC[dsv_v39;d_fun3]
2159 THEN MP_TAC IS_SCS_TRI_STABLE_SYSTEM
2161 THEN MRESA_TAC tri_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
2162 (change_type_v3 (scs_a_v39 s))`;`
2163 (change_type_v3 (scs_b_v39 s))`;`
2164 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
2165 (\i. (1 + i) MOD scs_k_v39 s)`]
2167 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
2168 THEN MATCH_MP_TAC(REAL_ARITH`a=b ==> d+ a=d+b`)
2169 THEN MP_TAC(SET_RULE`is_ear_v39 s \/ ~(is_ear_v39 s)`)
2175 MATCH_MP_TAC(REAL_ARITH`a=b ==> #0.1 * &1 * a= #0.1 * &1 *b`)
2176 THEN ASM_REWRITE_TAC[J1_TS;change_type_v2;IN_ELIM_THM]
2177 THEN MATCH_MP_TAC SUM_EQ_GENERAL
2178 THEN REWRITE_TAC[IN_ELIM_THM;dist]
2179 THEN EXISTS_TAC`(\i. if i MOD 3=0 then 3,1 else i, SUC(i MOD 3))`
2183 REWRITE_TAC[IN_ELIM_THM; IMAGE;EXISTS_UNIQUE;IN_NUMSEG]
2184 THEN REPEAT RESA_TAC
2185 THEN MP_TAC(ARITH_RULE`i<=3==> i=3\/ (i<3)`)
2188 REWRITE_TAC[ARITH_3_TAC]
2190 THEN ASM_REWRITE_TAC[ARITH_3_TAC]
2191 THEN POP_ASSUM(fun th->
2193 THEN REWRITE_TAC[th;ARITH_3_TAC]
2194 THEN REPEAT DISCH_TAC)
2198 MP_TAC(SET_RULE`{0, 1} = {i' MOD 3, j MOD 3} ==> (i' MOD 3=0/\ j MOD 3=1)\/ (i' MOD 3=1/\ j MOD 3=0)`)
2203 THEN REWRITE_TAC[is_scs_v39;periodic2]
2204 THEN REPEAT STRIP_TAC
2205 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
2206 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
2207 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 1`][ARITH_RULE`~(3=0)`;periodic]
2208 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
2213 THEN REWRITE_TAC[is_scs_v39;periodic2]
2214 THEN REPEAT STRIP_TAC
2215 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
2216 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
2217 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 0`][ARITH_RULE`~(3=0)`;periodic]
2218 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
2222 THEN POP_ASSUM MP_TAC
2223 THEN MRESAL_TAC MOD_LT[`y':num`;`3`][ARITH_3_TAC]
2224 THEN MP_TAC(SET_RULE`y' MOD 3=0\/ ~(y' MOD 3=0)`)
2226 THEN REWRITE_TAC[PAIR_EQ]
2228 THEN MRESAL_TAC Ssrnat.eqSS[`y':num`;`0`][ARITH_3_TAC];
2232 THEN ASM_REWRITE_TAC[]
2233 THEN SUBGOAL_THEN`~(i MOD 3=0)`ASSUME_TAC;
2235 MP_TAC(ARITH_RULE`1<=i/\ i<3==> i=1\/ i=2`)
2237 THEN REWRITE_TAC[ARITH_3_TAC]
2244 REPLICATE_TAC (22-17)(POP_ASSUM MP_TAC)
2245 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2247 THEN MRESAL_TAC MOD_LT[`i:num`;`3`][ARITH_3_TAC]
2249 THEN MP_TAC(SET_RULE`{i, (1 + i) MOD 3} = {i' MOD 3, j MOD 3}
2250 ==> (i' MOD 3= i/\ j MOD 3= (1+i) MOD 3)\/ (i' MOD 3= (1+i) MOD 3/\ j MOD 3= i)`)
2255 THEN REWRITE_TAC[is_scs_v39;periodic2]
2256 THEN REPEAT STRIP_TAC
2257 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
2258 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
2259 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((1 + i) MOD 3)`][ARITH_RULE`~(3=0)`;periodic]
2260 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
2261 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
2262 THEN POP_ASSUM (fun th-> MRESA1_TAC th`1+i:num`)
2263 THEN REWRITE_TAC[ADD1;]
2264 THEN ONCE_REWRITE_TAC[ADD_SYM]
2265 THEN ASM_REWRITE_TAC[];
2270 THEN REWRITE_TAC[is_scs_v39;periodic2]
2271 THEN REPEAT STRIP_TAC
2272 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
2273 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
2274 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
2275 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
2276 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
2277 THEN POP_ASSUM (fun th-> MRESA1_TAC th`1+i:num`)
2278 THEN REWRITE_TAC[ADD1;]
2279 THEN ONCE_REWRITE_TAC[ADD_SYM]
2280 THEN ASM_REWRITE_TAC[];
2285 THEN POP_ASSUM MP_TAC
2286 THEN MRESAL_TAC MOD_LT[`y':num`;`3`][ARITH_3_TAC]
2287 THEN MP_TAC(SET_RULE`y'=0\/ ~(y'=0)`)
2291 REWRITE_TAC[PAIR_EQ]
2292 THEN MP_TAC(ARITH_RULE`i<3==> ~(3=i)`)
2295 REWRITE_TAC[PAIR_EQ]
2300 THEN MRESAL_TAC MOD_LT[`x:num`;`3`][ARITH_3_TAC]
2303 MP_TAC(ARITH_RULE`x=0 \/ ~(x=0)`)
2308 THEN ASM_REWRITE_TAC[IN_NUMSEG;ARITH_3_TAC]
2309 THEN EXISTS_TAC`x:num`
2310 THEN EXISTS_TAC`SUC x:num`
2311 THEN ASM_REWRITE_TAC[ARITH_3_TAC];
2314 THEN ASM_REWRITE_TAC[IN_NUMSEG]
2315 THEN MP_TAC(ARITH_RULE`~(x=0) /\ x<3==> 1<=x/\ x<=3`)
2317 THEN EXISTS_TAC`x:num`
2318 THEN EXISTS_TAC`SUC x`
2319 THEN ASM_REWRITE_TAC[]
2320 THEN ONCE_REWRITE_TAC[ADD_SYM]
2321 THEN REWRITE_TAC[ADD1]
2325 MP_TAC(ARITH_RULE`x<3==> x=0 \/ (~(x=0) /\ x=1) \/ (~(x=0) /\ x=2)`)
2327 THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ SUC 0=1/\ SUC 1=2/\ SUC 2=3`]
2329 THEN REWRITE_TAC[BBs_v39;periodic;LET_DEF;LET_END_DEF;]
2330 THEN REPEAT STRIP_TAC
2331 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;periodic]
2332 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_3_TAC])
2337 (*************-1*************)
2339 MATCH_MP_TAC(REAL_ARITH`a=b ==> #0.1 * -- &1 * a= #0.1 * -- &1 *b`)
2340 THEN ASM_REWRITE_TAC[J1_TS;change_type_v2;IN_ELIM_THM]
2341 THEN MATCH_MP_TAC SUM_EQ_GENERAL
2342 THEN REWRITE_TAC[IN_ELIM_THM;dist]
2343 THEN EXISTS_TAC`(\i. if i MOD 3=0 then 3,1 else i, SUC(i MOD 3))`
2347 REWRITE_TAC[IN_ELIM_THM; IMAGE;EXISTS_UNIQUE;IN_NUMSEG]
2348 THEN REPEAT RESA_TAC
2349 THEN MP_TAC(ARITH_RULE`i<=3==> i=3\/ (i<3)`)
2352 REWRITE_TAC[ARITH_3_TAC]
2354 THEN ASM_REWRITE_TAC[ARITH_3_TAC]
2355 THEN POP_ASSUM(fun th->
2357 THEN REWRITE_TAC[th;ARITH_3_TAC]
2358 THEN REPEAT DISCH_TAC)
2362 MP_TAC(SET_RULE`{0, 1} = {i' MOD 3, j MOD 3} ==> (i' MOD 3=0/\ j MOD 3=1)\/ (i' MOD 3=1/\ j MOD 3=0)`)
2367 THEN REWRITE_TAC[is_scs_v39;periodic2]
2368 THEN REPEAT STRIP_TAC
2369 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
2370 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
2371 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 1`][ARITH_RULE`~(3=0)`;periodic]
2372 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
2377 THEN REWRITE_TAC[is_scs_v39;periodic2]
2378 THEN REPEAT STRIP_TAC
2379 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
2380 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
2381 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 0`][ARITH_RULE`~(3=0)`;periodic]
2382 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
2386 THEN POP_ASSUM MP_TAC
2387 THEN MRESAL_TAC MOD_LT[`y':num`;`3`][ARITH_3_TAC]
2388 THEN MP_TAC(SET_RULE`y' MOD 3=0\/ ~(y' MOD 3=0)`)
2390 THEN REWRITE_TAC[PAIR_EQ]
2392 THEN MRESAL_TAC Ssrnat.eqSS[`y':num`;`0`][ARITH_3_TAC];
2396 THEN ASM_REWRITE_TAC[]
2397 THEN SUBGOAL_THEN`~(i MOD 3=0)`ASSUME_TAC;
2399 MP_TAC(ARITH_RULE`1<=i/\ i<3==> i=1\/ i=2`)
2401 THEN REWRITE_TAC[ARITH_3_TAC]
2408 REPLICATE_TAC (22-17)(POP_ASSUM MP_TAC)
2409 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2411 THEN MRESAL_TAC MOD_LT[`i:num`;`3`][ARITH_3_TAC]
2413 THEN MP_TAC(SET_RULE`{i, (1 + i) MOD 3} = {i' MOD 3, j MOD 3}
2414 ==> (i' MOD 3= i/\ j MOD 3= (1+i) MOD 3)\/ (i' MOD 3= (1+i) MOD 3/\ j MOD 3= i)`)
2419 THEN REWRITE_TAC[is_scs_v39;periodic2]
2420 THEN REPEAT STRIP_TAC
2421 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
2422 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
2423 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((1 + i) MOD 3)`][ARITH_RULE`~(3=0)`;periodic]
2424 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
2425 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
2426 THEN POP_ASSUM (fun th-> MRESA1_TAC th`1+i:num`)
2427 THEN REWRITE_TAC[ADD1;]
2428 THEN ONCE_REWRITE_TAC[ADD_SYM]
2429 THEN ASM_REWRITE_TAC[];
2434 THEN REWRITE_TAC[is_scs_v39;periodic2]
2435 THEN REPEAT STRIP_TAC
2436 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][ARITH_RULE`~(3=0)`;periodic]
2437 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`)
2438 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
2439 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i':num`)
2440 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][ARITH_RULE`~(3=0)`;periodic]
2441 THEN POP_ASSUM (fun th-> MRESA1_TAC th`1+i:num`)
2442 THEN REWRITE_TAC[ADD1;]
2443 THEN ONCE_REWRITE_TAC[ADD_SYM]
2444 THEN ASM_REWRITE_TAC[];
2449 THEN POP_ASSUM MP_TAC
2450 THEN MRESAL_TAC MOD_LT[`y':num`;`3`][ARITH_3_TAC]
2451 THEN MP_TAC(SET_RULE`y'=0\/ ~(y'=0)`)
2455 REWRITE_TAC[PAIR_EQ]
2456 THEN MP_TAC(ARITH_RULE`i<3==> ~(3=i)`)
2459 REWRITE_TAC[PAIR_EQ]
2464 THEN MRESAL_TAC MOD_LT[`x:num`;`3`][ARITH_3_TAC]
2467 MP_TAC(ARITH_RULE`x=0 \/ ~(x=0)`)
2472 THEN ASM_REWRITE_TAC[IN_NUMSEG;ARITH_3_TAC]
2473 THEN EXISTS_TAC`x:num`
2474 THEN EXISTS_TAC`SUC x:num`
2475 THEN ASM_REWRITE_TAC[ARITH_3_TAC];
2478 THEN ASM_REWRITE_TAC[IN_NUMSEG]
2479 THEN MP_TAC(ARITH_RULE`~(x=0) /\ x<3==> 1<=x/\ x<=3`)
2481 THEN EXISTS_TAC`x:num`
2482 THEN EXISTS_TAC`SUC x`
2483 THEN ASM_REWRITE_TAC[]
2484 THEN ONCE_REWRITE_TAC[ADD_SYM]
2485 THEN REWRITE_TAC[ADD1]
2489 MP_TAC(ARITH_RULE`x<3==> x=0 \/ (~(x=0) /\ x=1) \/ (~(x=0) /\ x=2)`)
2491 THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3/\ SUC 0=1/\ SUC 1=2/\ SUC 2=3`]
2493 THEN REWRITE_TAC[BBs_v39;periodic;LET_DEF;LET_END_DEF;]
2494 THEN REPEAT STRIP_TAC
2495 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;periodic]
2496 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_3_TAC])
2503 let XWITCCN_CASE_3_IS_SCS=prove_by_refinement(
2504 `is_scs_v39 s /\ BBs_v39 s vv
2506 /\ dimindex(:M) =scs_k_v39 s
2507 /\ taustar_v39 s vv < &0
2508 ==> ~(BBprime_v39 s = {})`,
2513 THEN MP_TAC IS_SCS_TRI_STABLE_SYSTEM
2515 THEN MP_TAC NOT_EMPTY_CASE_3_IS_SCS
2517 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`]
2518 THEN MP_TAC IN_B_SY1_COLLINEAR_CASE_3_IS_SCS
2520 THEN ABBREV_TAC`s1 =tri_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
2521 (change_type_v3 (scs_a_v39 s)),
2522 (change_type_v3 (scs_b_v39 s)),
2523 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
2524 (\i. (1 + i) MOD scs_k_v39 s))`
2525 THEN MRESA_TAC tri_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
2526 (change_type_v3 (scs_a_v39 s))`;`
2527 (change_type_v3 (scs_b_v39 s))`;`
2528 (change_type_v2 (scs_J_v39 s)(scs_k_v39 s))`;`
2529 (\i. (1 + i) MOD scs_k_v39 s)`]
2530 THEN MRESAL_TAC (GEN_ALL HDPLYGY_CASE_30)[`scs_d_v39 s`;`(change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`scs_k_v39 s`;`(change_type_v3 (scs_a_v39 s))`;` (change_type_v3 (scs_b_v39 s))`;`s:scs_v39`;`s1:tri_sy`][ARITH_RULE`2<3`]
2531 THEN POP_ASSUM (fun th->
2533 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
2536 THEN REWRITE_TAC[BBprime_v39;IN]
2537 THEN ABBREV_TAC`( vv1 i =
2538 if i MOD scs_k_v39 s = 0 then row 3 v else
2539 if i MOD scs_k_v39 s = 1 then row 1 v else
2540 row 2 (v:real^3^M))`
2541 THEN EXISTS_TAC`vv1:num->real^3`
2544 ONCE_REWRITE_TAC[GSYM IN]
2545 THEN MATCH_MP_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_3_IS_SCS)
2546 THEN EXISTS_TAC`x:real^(M,3)finite_product`
2547 THEN EXISTS_TAC`v:real^3^M`
2548 THEN ASM_REWRITE_TAC[]
2549 THEN POP_ASSUM MP_TAC
2552 SUBGOAL_THEN`vector [ vv1 1; (vv1:num->real^3) 2;vv1 0] = v:real^3^M`
2555 POP_ASSUM(fun th-> REWRITE_TAC[GSYM th])
2556 THEN ASM_REWRITE_TAC[ARITH_RULE`1 MOD 3=1/\ 2 MOD 3=2/\ 3 MOD 3=0/\ 0 MOD 3=0 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(2=1)/\ ~(3=1)/\ ~(3=2)`;]
2557 THEN ONCE_REWRITE_TAC[CART_EQ]
2558 THEN ASM_REWRITE_TAC[ARITH_RULE`1<=i/\ i<=3 <=>i=1\/ i=2\/ i=3`]
2559 THEN REPEAT RESA_TAC
2561 ASM_SIMP_TAC[row;vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
2562 REWRITE_TAC[num_CONV `3`;num_CONV `2`; num_CONV `1`; EL; HD; TL;]
2563 THEN ASM_SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH;row;LAMBDA_BETA];
2568 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM IN]
2569 THEN REPEAT STRIP_TAC
2570 THEN MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_3_IS_SCS)
2571 [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
2572 THEN POP_ASSUM MP_TAC
2573 THEN POP_ASSUM MP_TAC
2574 THEN REWRITE_TAC[IN]
2575 THEN REPEAT STRIP_TAC
2576 THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_TAU_STAR_3_IS_SCS)[`vector [(vv1:num->real^3) 1; vv1 2; vv1 0]:real^3^M`;`vv1:num->real^3`;`s:scs_v39`;`s1:tri_sy`;`matvec(vector [vv1 1; vv1 2; vv1 0]:real^3^M):real^(M,3)finite_product`]
2577 THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_TAU_STAR_3_IS_SCS)[`vector [(ww:num->real^3) 1; ww 2; ww 0]:real^3^M`;`ww:num->real^3`;`s:scs_v39`;`s1:tri_sy`;`matvec(vector [ww 1; ww 2; ww 0]:real^3^M):real^(M,3)finite_product`]
2578 THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_3)[`ww:num->real^3`;`vector [ww 1; ww 2; ww 0]:real^3^M`;`matvec(vector [ww 1; ww 2; ww 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`]
2579 THEN MRESAL_TAC VECTOR_3_3[`(vv1:num->real^3) 1`;`(vv1:num->real^3) 2`;`(vv1:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`]
2580 THEN MRESAL_TAC VECTOR_3_3[`(ww:num->real^3) 1`;`(ww:num->real^3) 2`;`(ww:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`]
2581 THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
2582 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2583 THEN MRESAL1_TAC th `matvec(vector [ww 1; ww 2; ww 0]:real^3^M):real^(M,3)finite_product`[Dih2k_hypermap.VECMATS_MATVEC_ID]);
2585 MRESA_TAC (GEN_ALL IN_NOT_EMPTY_B1_SY_3_IS_SCS)
2586 [`x:real^(M,3)finite_product`;`v:real^3^M`;`vv1:num->real^3`;`s:scs_v39`]
2587 THEN POP_ASSUM MP_TAC
2588 THEN REWRITE_TAC[IN]
2590 THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_TAU_STAR_3_IS_SCS)[`vector [(vv1:num->real^3) 1; vv1 2; vv1 0]:real^3^M`;`vv1:num->real^3`;`s:scs_v39`;`s1:tri_sy`;`matvec(vector [vv1 1; vv1 2; vv1 0]:real^3^M):real^(M,3)finite_product`]
2591 THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_TAU_STAR_3_IS_SCS)[`vector [(vv:num->real^3) 1; vv 2; vv 0]:real^3^M`;`vv:num->real^3`;`s:scs_v39`;`s1:tri_sy`;`matvec(vector [vv 1; vv 2; vv 0]:real^3^M):real^(M,3)finite_product`]
2592 THEN MRESA_TAC (GEN_ALL IN_IS_SCS_CASE_3)[`vv:num->real^3`;`vector [vv 1; vv 2; vv 0]:real^3^M`;`matvec(vector [vv 1; vv 2; vv 0]:real^3^M):real^(M,3)finite_product`;`s:scs_v39`]
2593 THEN MRESAL_TAC VECTOR_3_3[`(vv1:num->real^3) 1`;`(vv1:num->real^3) 2`;`(vv1:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`]
2594 THEN MRESAL_TAC VECTOR_3_3[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=3/\ 2<=3/\ 3<=3`]
2595 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
2596 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2597 THEN MRESAL1_TAC th `matvec(vector [(vv:num->real^3) 1; vv 2; vv 0]:real^3^M):real^(M,3)finite_product`[Dih2k_hypermap.VECMATS_MATVEC_ID])
2598 THEN REPLICATE_TAC (31-4) (POP_ASSUM MP_TAC)
2599 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2601 THEN ASM_REWRITE_TAC[])
2602 THEN POP_ASSUM MP_TAC
2603 THEN REAL_ARITH_TAC;
2610 let UXCKFPE=prove_by_refinement(
2611 ` !s vv . is_scs_v39 s /\ vv IN BBs_v39 s
2612 /\ taustar_v39 s vv < &0
2613 ==> ~(BBprime_v39 s = {})`,
2618 THEN REWRITE_TAC[IN]
2620 THEN SUBGOAL_THEN`3<= scs_k_v39 s /\ scs_k_v39 s<=6` ASSUME_TAC;
2623 THEN REWRITE_TAC[is_scs_v39]
2626 MP_TAC(ARITH_RULE`3<= scs_k_v39 s /\ scs_k_v39 s<=6 ==> scs_k_v39 s=3 \/ scs_k_v39 s=4 \/ scs_k_v39 s=5 \/ scs_k_v39 s=6`)
2629 MP_TAC(INST_TYPE [`:3`,`:M`]XWITCCN_CASE_3_IS_SCS)
2630 THEN ASM_REWRITE_TAC[DIMINDEX_3]
2633 MP_TAC(INST_TYPE [`:2+2`,`:M`]XWITCCN_CASE_4_IS_SCS)
2634 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_4]
2637 MP_TAC(INST_TYPE [`:2+3`,`:M`]XWITCCN_CASE_5_IS_SCS)
2638 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_5]
2640 MP_TAC(INST_TYPE [`:3+3`,`:M`]XWITCCN_CASE_6_IS_SCS)
2641 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_6]
2650 let check_completeness_claimA_concl =
2651 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)