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 Vasyyau = struct
28 open Wrgcvdr_cizmrrh;;
36 open Flyspeck_constants;;
52 open Wrgcvdr_cizmrrh;;
54 open Flyspeck_constants;;
100 let WGDHPPI= prove(`!s v.
101 is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s ==>
102 CARD { i | i < scs_k_v39 s /\ scs_is_str s v i} <= 1`,
104 THEN MRESA_TAC GSXRFWM[`s`;`v`]
105 THEN MRESAL_TAC Aursipd.AURSIPD[`s`;`v`][ARITH_RULE`3<4`]
109 (************************************)
111 let DIST_V_IN_BB_LE_C=prove(` scs_b_v39 s i (SUC i) <= c/\
113 ==> dist (v i, v (SUC i))<= c`,
114 REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;dist]
116 THEN THAYTHE_TAC 1[`i`;`SUC i`]
118 THEN REAL_ARITH_TAC);;
121 let arclength_lt_1553 = prove_by_refinement(
122 `&2 * arclength (&2) (&2) (&2 * h0) < arclength (&2) (&2)
126 REPEAT (GMATCH_SIMP_TAC Compute_2158872499.ATN_UPS_X_BREAKDOWN1);
127 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
128 REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
129 REWRITE_TAC[arith `x + &2 - &2 = x`];
130 REWRITE_TAC[Sphere.h0];
131 TYPIFY `#3.9 < sqrt (#15.53) /\ sqrt(#15.53) < #3.95` (C
132 SUBGOAL_THEN ASSUME_TAC);
133 GMATCH_SIMP_TAC REAL_LT_RSQRT;
136 MATCH_MP_TAC REAL_LT_LSQRT;
138 TYPIFY_GOAL_THEN `&0 < &2 + &2 * #1.26 - &2 /\ &0 < &2 + &2 - &2 *
139 #1.26 /\ &0 < &2 + &2 + &2 * #1.26 /\ &0 < &2 + sqrt #15.53 - &2 /\
140 &0 < &2 + &2 - sqrt #15.53 /\ &0 < &2 + &2 + sqrt #15.53 /\ &0 <
141 sqrt #15.53 /\ &0 < &2 * #1.26` (unlist REWRITE_TAC);
142 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
143 MP_TAC (Flyspeck_constants.calc `&2 * (pi / &2 + atn (((&2 *
144 #1.26) * &2 * #1.26 - &2 * &2 - &2 * &2) / sqrt ((&2 + &2 + &2 *
145 #1.26) * (&2 + &2 - &2 * #1.26) * (&2 + &2 * #1.26 - &2) *
146 &2 * #1.26))) < pi / &2 + atn ((sqrt #15.53 * sqrt #15.53 - &2
147 * &2 - &2 * &2) / sqrt ((&2 + &2 + sqrt #15.53) * (&2 + &2 - sqrt
148 #15.53) * (&2 + sqrt #15.53 - &2) * sqrt #15.53))` );
154 let ASSWPOW= prove_by_refinement( `!s v i.
155 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
156 scs_b_v39 s i (i+1) <= &2 * h0 /\ scs_b_v39 s (i+1) (i+2) <= &2 * h0
157 ==> xrr (norm (v i)) (norm(v(i+2))) (dist(v i,v(i+2))) <= #15.53 `,
159 REWRITE_TAC[IN;GSYM ADD1;ARITH_RULE`i+2=SUC(SUC i)`]
161 THEN ABBREV_TAC`k= scs_k_v39 s`
162 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
163 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
164 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
166 THEN ASSUME_TAC(ARITH_RULE`3<4`)
167 THEN MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
168 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
169 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
170 THEN MP_TAC Local_lemmas.CVLF_LF_F
177 MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`]
178 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`]
179 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`]
180 THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`]
181 THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`]
182 THEN MRESAL_TAC DIST_V_IN_BB_LE_C[`s`;`v`;`i`;`&2*h0`][dist]
183 THEN MRESAL_TAC DIST_V_IN_BB_LE_C[`s`;`v`;`SUC i`;`&2*h0`][dist]
184 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`&2* h0`][dist;]
185 THEN POP_ASSUM MP_TAC
186 THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
187 THEN REWRITE_TAC[GSYM h0]
189 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`&2* h0`][dist;]
190 THEN POP_ASSUM MP_TAC
191 THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
192 THEN REWRITE_TAC[GSYM h0]
194 THEN DICH_TAC (26-18)
195 THEN DICH_TAC (25-18)
196 THEN DICH_TAC (24-18)
197 THEN REWRITE_TAC[Ckqowsa_3_points.in_ball_annulus]
198 THEN REPEAT STRIP_TAC
199 THEN MRESA_TAC Trigonometry2.ARCV_INEQUALTY[`vec 0:real^3`;`v i`;`v (SUC (SUC i))`;`v(SUC i)`]
200 THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (i)) (v (SUC (i))) <= arclength (&2) (&2) (&2 * h0)
201 /\ arcV (vec 0) ((v:num->real^3) (SUC (i))) (v (SUC (SUC (i)))) <=
202 arclength (&2) (&2) (&2 * h0)
203 /\ &2 * arclength (&2) (&2) (&2 * h0) < arclength (&2) (&2)
205 /\ arcV (vec 0) (v i) (v (SUC (SUC i))) <=
206 arcV (vec 0) (v i) (v (SUC i)) +
207 arcV (vec 0) (v (SUC i)) (v (SUC (SUC i)))
208 ==>arcV (vec 0) (v i) (v (SUC (SUC i)))
209 < arclength (&2) (&2)
211 THEN ASM_SIMP_TAC[arclength_lt_1553]
212 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
213 THEN MRESAS_TAC Planarity.IMP_NORM_FAN[`v (i+0)`;`v(i+2):real^3`][VECTOR_ARITH`A- vec 0=A:real^3`;ARITH_RULE`~(4=0)/\ ~(0 MOD 4 = 2 MOD 4)`;Ocbicby.MOD_EQ_MOD_SHIFT]
214 THEN MRESA_TAC WL_IN_V[`i+0`;`v:num->real^3`]
215 THEN MRESA_TAC WL_IN_V[`i+2`;`v:num->real^3`]
216 THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN;scs_generic]
217 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (i+0)`;`v (i+2)`;`V`]
218 THEN THAYTHES_TAC 0[`v (i+0)`;`v (i+2)`][SET_RULE`a IN {a,b}`;ARITH_RULE`~(4=0)/\ ~(0 MOD 4 = 2 MOD 4)`;Ocbicby.MOD_EQ_MOD_SHIFT]
220 THEN REWRITE_TAC[ARITH_RULE`i+0=i/\ i+2=SUC(SUC i)`]
222 THEN ABBREV_TAC`u=(v:num->real^3) i`
223 THEN ABBREV_TAC`w=(v:num->real^3) (SUC (SUC i))`
224 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`u`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A:real^3`]
225 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`w`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A:real^3`]
226 THEN MRESAL_TAC Collect_geom2.NOT_COL_EQ_UPS_X_POS[`vec 0:real^3`;`u`;`w`][dist;VECTOR_ARITH`vec 0- a= --a:real^3`;NORM_NEG]
227 THEN MRESAL_TAC arclength_xrr[`norm (u)`;`norm w`;`norm (u-w)`][REAL_ARITH`a*a= a pow 2`]
228 THEN MRESA_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`u`;`w`]
229 THEN DICH_TAC (62-45)
230 THEN ASM_SIMP_TAC[dist;VECTOR_ARITH`vec 0- a= --a:real^3`;NORM_NEG]
231 THEN MRESAL_TAC arclength_xrr[`&2`;`&2`;`sqrt #15.53`][REAL_ARITH`a*a= a pow 2/\ &0< &2`]
238 TYPIFY `#3.9 < sqrt (#15.53) /\ sqrt(#15.53) < #3.95` (C
239 SUBGOAL_THEN ASSUME_TAC);
241 GMATCH_SIMP_TAC REAL_LT_RSQRT;
245 MATCH_MP_TAC REAL_LT_LSQRT;
249 TYPIFY_GOAL_THEN `&0 < &2 + &2 * #1.26 - &2 /\ &0 < &2 + &2 - &2 *
250 #1.26 /\ &0 < &2 + &2 + &2 * #1.26 /\ &0 < &2 + sqrt #15.53 - &2 /\
251 &0 < &2 + &2 - sqrt #15.53 /\ &0 < &2 + &2 + sqrt #15.53 /\ &0 <
252 sqrt #15.53 /\ &0 < &2 * #1.26` (unlist REWRITE_TAC);
253 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
254 MP_TAC(REAL_ARITH`#3.9 < sqrt #15.53==> &0 < sqrt #15.53`)
256 THEN MRESAL_TAC SQRT_POW2[`#15.53`][REAL_ARITH`&0<= #15.53`]
257 THEN REWRITE_TAC[ups_x;REAL_ARITH`&0 <
258 --(&2 pow 2) * &2 pow 2 - &2 pow 2 * &2 pow 2 - #15.53 * #15.53 +
259 &2 * &2 pow 2 * #15.53 +
260 &2 * &2 pow 2 * &2 pow 2 +
261 &2 * &2 pow 2 * #15.53`]
263 THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`norm u`;`norm w`;`norm (u-w)`][REAL_ARITH`a*a= a pow 2`]
264 THEN MP_TAC(REAL_ARITH`&0 < xrr (norm u) (norm w) (norm (u-w))/\
265 xrr (norm u) (norm w) (norm (u-w)) < &16
266 ==> abs (&1 - xrr (norm u) (norm w) (norm (u-w:real^3)) / &8) <= &1`)
268 THEN SUBGOAL_THEN`abs (&1 - xrr (&2) (&2) (sqrt #15.53) / &8) <= &1`ASSUME_TAC
273 ASM_REWRITE_TAC[xrr;REAL_ARITH`a*a= a pow 2`]
277 MRESAL_TAC ACS_MONO_LT_EQ[`&1 - xrr (norm u) (norm w) (norm (u-w)) / &8`;`&1 - xrr (&2) (&2) (sqrt #15.53) / &8`][REAL_ARITH`&1- a/ &8< &1- b/ &8<=> b<a`]
278 THEN MATCH_MP_TAC(REAL_ARITH`a<=b==>(c<a==>c<=b)`)
283 ASM_REWRITE_TAC[xrr;REAL_ARITH`a*a= a pow 2`]
292 let YEBWJNG= prove_by_refinement(
293 `main_nonlinear_terminal_v11 ==>
295 is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\
296 (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
297 (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
298 (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
299 ~scs_is_str s v p /\ ~scs_is_str s v (p+1) /\ scs_a_v39 s p (p+1) = &2
300 ==> dist(v p,v(p+1)) = &2)`,
302 REWRITE_TAC[IN;scs_is_str]
304 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
305 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
306 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
309 THEN MP_TAC Cuxvzoz.CUXVZOZ
311 THEN MATCH_DICH_TAC 0
312 THEN EXISTS_TAC`s:scs_v39`
313 THEN EXISTS_TAC`FF:real^3#real^3->bool`
315 THEN ASSUME_TAC(ARITH_RULE`3<4/\ 1<4/\ ~(4=0)`)
317 THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN]
318 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1]
319 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
320 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`s`;`v`]
321 THEN MP_TAC Local_lemmas.CVLF_LF_F
323 THEN MP_TAC SCS_DIAG_A_LE_DIST
326 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
327 THEN MRESA_TAC WL_IN_V[`SUC p`;`v:num->real^3`]
328 THEN MRESA_TAC WL_IN_V[`p+4-1`;`v:num->real^3`]
329 THEN MRESA_TAC WL_IN_V[`SUC p+4-1`;`v:num->real^3`]
330 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
331 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][GSYM ADD1]
332 THEN THAYTHE_TAC 0[`v (p+4-1)`]
333 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
334 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) <= pi
335 /\ ~(azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) = pi)
336 ==> azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) < pi`)
338 THEN REWRITE_TAC[ADD1]
339 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+1)`;`v`;`p+1`;`4`]
340 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][GSYM ADD1]
341 THEN THAYTHE_TAC 0[`v (SUC p+4-1)`]
343 THEN REWRITE_TAC[GSYM ADD1]
345 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) <= pi
346 /\ ~(azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) = pi)
347 ==> azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) < pi`)
349 THEN THAYTHES_TAC(32-26)[`1 * 4 + p`;`p`][MOD_MULT_ADD]
350 THEN MRESAL_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`p+3`][ARITH_RULE`SUC(i+3)=1*4+i/\ p+4-1=p+3`;GSYM dist]
351 THEN SUBGOAL_THEN`!i. scs_b_v39 s i (SUC(i)) <= cstab`ASSUME_TAC;
354 THEN THAYTHE_TAC (33-6)[`i`]
356 THEN REWRITE_TAC[cstab;h0;ADD1]
359 MP_TAC Axjrpnc.NORM_V_IN_BB_LE_CSTAB
361 THEN REWRITE_TAC[GSYM dist]
362 THEN THAYTHES_TAC 0[`p+3`][ARITH_RULE`SUC(i+3)=1*4+i/\ p+4-1=p+3`;GSYM dist]
363 THEN ONCE_REWRITE_TAC[SET_RULE`A/\B<=> B/\A`]
366 THAYTHE_TAC (35-6)[`p`];
369 THEN REWRITE_TAC[ADD1]
376 MRESA_TAC Ardbzye.SCS_DIAG_4_ADD2[`p`]
377 THEN THAYTHE_TAC (36-5)[`p+1`;`p+3`]
378 THEN ONCE_REWRITE_TAC[DIST_SYM]
380 THEN REWRITE_TAC[ADD1;cstab]
381 THEN REAL_ARITH_TAC]);;
383 (************************************)
386 let NOT_MOD_4_CASES=prove(`~(i MOD 4 = (p + 2) MOD 4)<=> i MOD 4 = p MOD 4\/ i MOD 4 = (p + 1) MOD 4
387 \/ i MOD 4 = (p + 3) MOD 4`,
388 MRESAL_TAC MOD_ADD_MOD[`p`;`1`;`4`][ARITH_RULE`~(4=0)`]
390 THEN MRESAL_TAC MOD_ADD_MOD[`p`;`2`;`4`][ARITH_RULE`~(4=0)`]
392 THEN MRESAL_TAC MOD_ADD_MOD[`p`;`3`;`4`][ARITH_RULE`~(4=0)`]
394 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`)
395 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
397 THEN MP_TAC(ARITH_RULE`p MOD 4<4==> p MOD 4=0\/ p MOD 4=1\/ p MOD 4=2\/ p MOD 4=3`)
398 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
405 let NOT_MOD_4_CASES_3=prove(`~(i MOD 4 = (p + 3) MOD 4)<=> i MOD 4 = p MOD 4\/ i MOD 4 = (p + 1) MOD 4
406 \/ i MOD 4 = (p + 2) MOD 4`,
407 MRESAL_TAC MOD_ADD_MOD[`p`;`1`;`4`][ARITH_RULE`~(4=0)`]
409 THEN MRESAL_TAC MOD_ADD_MOD[`p`;`2`;`4`][ARITH_RULE`~(4=0)`]
411 THEN MRESAL_TAC MOD_ADD_MOD[`p`;`3`;`4`][ARITH_RULE`~(4=0)`]
413 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`)
414 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
416 THEN MP_TAC(ARITH_RULE`p MOD 4<4==> p MOD 4=0\/ p MOD 4=1\/ p MOD 4=2\/ p MOD 4=3`)
417 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
424 let SCS_STR_CASES_4= prove_by_refinement(`!s v.
425 is_scs_v39 s /\ scs_k_v39 s = 4 /\ MMs_v39 s v /\
426 ~scs_is_str s v p /\ ~scs_is_str s v (p+1)
427 ==> ~scs_is_str s v (p+3)\/ ~scs_is_str s v (p+2)`,
430 THEN REWRITE_TAC[GSYM DE_MORGAN_THM]
432 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ (4-1) MOD 4= 4-1/\ 1<4`)
433 THEN MRESAL_TAC MMS_IMP_BBS[`s`;`v`][IN]
434 THEN SUBGOAL_THEN`(p +3) MOD 4 IN { i | i < scs_k_v39 s /\ scs_is_str s (v:num->real^3) i}`
437 ASM_REWRITE_TAC[IN_ELIM_THM]
439 THEN SIMP_TAC[scs_is_str;DIVISION;]
441 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
442 THEN THAYTHES_TAC 0[`(p+3) MOD 4`;`p+3:num`][MOD_REFL]
443 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
444 THEN THAYTHES_TAC 0[`SUC((p+3) MOD 4)`;`SUC((p+3) MOD 4)MOD 4`][MOD_REFL;Hypermap.lemma_suc_mod]
445 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
446 THEN THAYTHES_TAC 0[`SUC(p+3) MOD 4`;`SUC(p+3) `][MOD_REFL;Hypermap.lemma_suc_mod]
447 THEN MRESA_TAC MOD_ADD_MOD[`p+3`;`4-1`;`4`]
448 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
449 THEN THAYTHES_TAC 0[`(p + 3) MOD 4 + 4 - 1`;`((p + 3) MOD 4 + 4 - 1)MOD 4`][MOD_REFL;Hypermap.lemma_suc_mod]
450 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
451 THEN THAYTHES_TAC 0[`((p + 3) + 4 - 1) MOD 4`;`(p + 3) + 4 - 1`][MOD_REFL;Hypermap.lemma_suc_mod];
454 SUBGOAL_THEN`(p +2) MOD 4 IN { i | i < scs_k_v39 s /\ scs_is_str s (v:num->real^3) i}`
457 ASM_REWRITE_TAC[IN_ELIM_THM]
459 THEN SIMP_TAC[scs_is_str;DIVISION;]
461 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
462 THEN THAYTHES_TAC 0[`(p+2) MOD 4`;`p+2:num`][MOD_REFL]
463 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
464 THEN THAYTHES_TAC 0[`SUC((p+2) MOD 4)`;`SUC((p+2) MOD 4)MOD 4`][MOD_REFL;Hypermap.lemma_suc_mod]
465 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
466 THEN THAYTHES_TAC 0[`SUC(p+2) MOD 4`;`SUC(p+2) `][MOD_REFL;Hypermap.lemma_suc_mod]
467 THEN MRESA_TAC MOD_ADD_MOD[`p+2`;`4-1`;`4`]
468 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
469 THEN THAYTHES_TAC 0[`(p + 2) MOD 4 + 4 - 1`;`((p + 2) MOD 4 + 4 - 1)MOD 4`][MOD_REFL;Hypermap.lemma_suc_mod]
470 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
471 THEN THAYTHES_TAC 0[`((p + 2) + 4 - 1) MOD 4`;`(p + 2) + 4 - 1`][MOD_REFL;Hypermap.lemma_suc_mod];
473 MP_TAC(SET_RULE`(p + 3) MOD 4 IN {i | i < scs_k_v39 s /\ scs_is_str s v i}/\
474 (p + 2) MOD 4 IN {i | i < scs_k_v39 s /\ scs_is_str s v i}
475 ==> {(p + 3) MOD 4 ,(p + 2) MOD 4 } SUBSET {i | i < scs_k_v39 s /\ scs_is_str s v i}`)
477 THEN MRESA_TAC Qknvmlb.SUC_MOD_NOT_EQ[`4`]
479 THEN THAYTHEL_TAC 0[`p+2`][ARITH_RULE`SUC(p+2)=p+3`]
480 THEN MRESA_TAC Planarity.CARD_2_FAN[`(p + 3) MOD 4`;`(p + 2) MOD 4`]
482 THEN SUBGOAL_THEN`FINITE {i | i < 4 /\ scs_is_str s v i}` ASSUME_TAC;
484 MATCH_MP_TAC FINITE_SUBSET
485 THEN EXISTS_TAC`0..4`
486 THEN ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG;FINITE_NUMSEG]
489 MRESA_TAC CARD_SUBSET[`{(p + 3) MOD 4, (p + 2) MOD 4}`;`{i | i < 4 /\ scs_is_str s v i}`]
490 THEN POP_ASSUM MP_TAC
491 THEN MRESAL_TAC WGDHPPI[`s`;`v`][IN]
498 let NEHXMWH_concl=`main_nonlinear_terminal_v11 ==>
500 IMAGE (\i. (v i,v (SUC i))) (:num) = FF /\
506 (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4 * h0 < scs_b_v39 s i j) /\
507 (!i. ~(i MOD 4 = (p+2) MOD 4) ==> interior_angle1 (vec 0) FF (v i) < pi)
508 ==> (dist(v p,v(p+1)) = scs_a_v39 s p (p+1) \/ dist(v p,v(p+1)) = scs_b_v39 s p (p+1)))`;;
510 let NEHXMWH1_concl=`main_nonlinear_terminal_v11 ==>
512 IMAGE (\i. (v i,v (SUC i))) (:num) = FF /\
518 (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4 * h0 < scs_b_v39 s i j) /\
519 (!i. ~(i MOD 4 = (p+3) MOD 4) ==> interior_angle1 (vec 0) FF (v i) < pi)
520 ==> (dist(v p,v(p+1)) = scs_a_v39 s p (p+1) \/ dist(v p,v(p+1)) = scs_b_v39 s p (p+1)))`;;
524 let TUAPYYU_concl = `
525 main_nonlinear_terminal_v11 ==>
527 is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\
528 (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
529 (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
530 (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
531 ~scs_is_str s v p /\ ~scs_is_str s v (p+1)
532 ==> dist(v p,v(p+1)) = scs_a_v39 s p (p+1) \/ dist(v p,v(p+1)) = scs_b_v39 s p (p+1))`;;
536 let TUAPYYU1= prove_by_refinement((mk_imp(NEHXMWH1_concl,mk_imp(NEHXMWH_concl, TUAPYYU_concl))),
538 REWRITE_TAC[IN;scs_is_str]
540 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
541 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
542 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
545 THEN ASSUME_TAC(ARITH_RULE`3<4/\ 1<4/\ ~(4=0)`)
547 THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN]
548 THEN MRESAL_TAC SCS_STR_CASES_4[`p`;`s`;`v`][scs_is_str]
549 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1]
550 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
551 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`s`;`v`]
552 THEN MP_TAC Local_lemmas.CVLF_LF_F
554 THEN MP_TAC SCS_DIAG_A_LE_DIST
557 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
558 THEN MRESA_TAC WL_IN_V[`SUC p`;`v:num->real^3`]
559 THEN MRESA_TAC WL_IN_V[`p+4-1`;`v:num->real^3`]
560 THEN MRESA_TAC WL_IN_V[`SUC p+4-1`;`v:num->real^3`]
561 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
562 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][GSYM ADD1]
563 THEN THAYTHE_TAC 0[`v (p+4-1)`]
564 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
565 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) <= pi
566 /\ ~(azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) = pi)
567 ==> azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) < pi`)
569 THEN REWRITE_TAC[ADD1]
570 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+1)`;`v`;`p+1`;`4`]
571 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][GSYM ADD1]
572 THEN THAYTHE_TAC 0[`v (SUC p+4-1)`]
574 THEN REWRITE_TAC[GSYM ADD1]
576 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) <= pi
577 /\ ~(azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) = pi)
578 ==> azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) < pi`)
583 THEN REWRITE_TAC[ADD1]
584 THEN MATCH_DICH_TAC 0
585 THEN EXISTS_TAC`FF:real^3#real^3->bool`
587 THEN ASM_REWRITE_TAC[NOT_MOD_4_CASES]
588 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1]
589 THEN REPEAT RESA_TAC;
591 THAYTHEL_TAC(32-25)[`i`;`p`][GSYM ADD1];
594 THAYTHEL_TAC(32-25)[`i`;`p+1`][ADD1]
595 THEN ASM_REWRITE_TAC[GSYM ADD1];
598 MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+3)`;`v`;`p+3`;`4`]
599 THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
600 THEN MRESA_TAC WL_IN_V[`(p+3)+4-1`;`v:num->real^3`]
601 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+3)`][GSYM ADD1]
602 THEN THAYTHE_TAC 0[`v ((p+3)+4-1)`]
603 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p+3)) (v (SUC (p+3))) (v ((p+3) + 4 - 1)) <= pi
604 /\ ~(azim (vec 0) (v (p+3)) (v (SUC (p+3))) (v ((p+3) + 4 - 1)) = pi)
605 ==> azim (vec 0) (v (p+3)) (v (SUC ((p+3)))) (v ((p+3) + 4 - 1)) < pi`)
608 THAYTHEL_TAC(38-25)[`i`;`p+3`][GSYM ADD1];
612 THEN REWRITE_TAC[ADD1]
613 THEN MATCH_DICH_TAC 0
614 THEN EXISTS_TAC`FF:real^3#real^3->bool`
616 THEN ASM_REWRITE_TAC[NOT_MOD_4_CASES_3]
617 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1]
618 THEN REPEAT RESA_TAC;
620 THAYTHEL_TAC(32-25)[`i`;`p`][GSYM ADD1];
623 THAYTHEL_TAC(32-25)[`i`;`p+1`][ADD1]
624 THEN ASM_REWRITE_TAC[GSYM ADD1];
627 MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+2)`;`v`;`p+2`;`4`]
628 THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
629 THEN MRESA_TAC WL_IN_V[`(p+2)+4-1`;`v:num->real^3`]
630 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+2)`][GSYM ADD1]
631 THEN THAYTHE_TAC 0[`v ((p+2)+4-1)`]
632 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p+2)) (v (SUC (p+2))) (v ((p+2) + 4 - 1)) <= pi
633 /\ ~(azim (vec 0) (v (p+2)) (v (SUC (p+2))) (v ((p+2) + 4 - 1)) = pi)
634 ==> azim (vec 0) (v (p+2)) (v (SUC ((p+2)))) (v ((p+2) + 4 - 1)) < pi`)
637 THAYTHEL_TAC(38-25)[`i`;`p+2`][GSYM ADD1]]);;
640 let TUAPYYU=prove( TUAPYYU_concl,
644 THEN MP_TAC Jotswix.NEHXMWH
645 THEN MP_TAC Jotswix.BZQNDMN
646 THEN ASM_REWRITE_TAC[]);;
649 (**************************)
652 let SCS_M_CASES_4_LE_2=prove(`scs_k_v39 s = 4/\ is_scs_v39 s
653 ==> CARD (scs_M s)<=2`,
654 REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;scs_M]
657 THEN ASM_REWRITE_TAC[]
662 let SCS_M_CASES_4_EQ=prove(`scs_k_v39 s = 4/\ is_scs_v39 s /\ {p MOD 4,(p+3)MOD 4} SUBSET scs_M s
663 ==> scs_M s={p MOD 4,(p+3)MOD 4}`,
665 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ ~(0 MOD 4 = 3 MOD 4)`)
666 THEN MRESAS_TAC Planarity.CARD_2_FAN[`(p+0) MOD 4`;`(p+3) MOD 4`][Ocbicby.MOD_EQ_MOD_SHIFT]
668 THEN REWRITE_TAC[ARITH_RULE`p+0=p`]
670 THEN MP_TAC SCS_M_CASES_4_LE_2
672 THEN MP_TAC Jlxfdmj.FINITE_SCS_M
674 THEN MRESA_TAC CARD_SUBSET_LE[`{p MOD 4, (p + 3) MOD 4}`;`scs_M s`]);;
676 let B_LE_2h0_SCS_M_4=prove(`scs_k_v39 s = 4/\ is_scs_v39 s /\ {p MOD 4,(p+3)MOD 4} SUBSET scs_M s
677 ==> scs_b_v39 s (p+1) (p+2)<= &2*h0`,
679 THEN MP_TAC SCS_M_CASES_4_EQ
681 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ ~(1 MOD 4 = 3 MOD 4)/\ 1<4`)
682 THEN SUBGOAL_THEN`~((p+1) MOD 4 IN scs_M s)`ASSUME_TAC
684 ASM_SIMP_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`;Ocbicby.MOD_EQ_MOD_SHIFT]
685 THEN MRESAL_TAC Qknvmlb.SUC_MOD_NOT_EQ[`4`][ADD1];
688 THEN REWRITE_TAC[scs_M;IN_ELIM_THM]
689 THEN ASM_SIMP_TAC[DIVISION]
690 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1) MOD 4`;`SUC ((p + 1) MOD 4)`;`s`;`p+1`;`SUC ((p + 1) MOD 4) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD]
691 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`SUC (p + 1) MOD 4`;`s`;`p+1`;`SUC (p + 1)`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`SUC(p+1)=p+2`]
692 THEN REAL_ARITH_TAC]);;
695 let B_LE_2h0_2_SCS_M_4=prove(`scs_k_v39 s = 4/\ is_scs_v39 s /\ {p MOD 4,(p+3)MOD 4} SUBSET scs_M s
696 ==> scs_b_v39 s (p+2) (p+3)<= &2*h0`,
698 THEN MP_TAC SCS_M_CASES_4_EQ
700 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ ~(2 MOD 4 = 3 MOD 4)/\ ~(2 MOD 4 = 0 MOD 4)/\ 1<4`)
701 THEN SUBGOAL_THEN`~((p+2) MOD 4 IN scs_M s)`ASSUME_TAC
703 ASM_SIMP_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`;Ocbicby.MOD_EQ_MOD_SHIFT]
704 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`2`;`0`;`p`][ARITH_RULE`p+0=p`];
706 THEN REWRITE_TAC[scs_M;IN_ELIM_THM]
707 THEN ASM_SIMP_TAC[DIVISION]
708 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2) MOD 4`;`SUC ((p + 2) MOD 4)`;`s`;`p+2`;`SUC ((p + 2) MOD 4) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD]
709 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2)`;`SUC (p + 2) MOD 4`;`s`;`p+2`;`SUC (p + 2)`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`SUC(p+2)=p+3`]
710 THEN REAL_ARITH_TAC]);;
714 let B_LE_2h0_2_SCS_M_4=prove(`scs_k_v39 s = 4/\ is_scs_v39 s /\ {p MOD 4,(p+3)MOD 4} SUBSET scs_M s
715 ==> scs_b_v39 s (p+1) (p+2)<= &2*h0 /\ scs_b_v39 s (p+2) (p+3)<= &2*h0`,
716 SIMP_TAC[B_LE_2h0_2_SCS_M_4;B_LE_2h0_SCS_M_4]);;
720 let WKZZEEH = prove_by_refinement(`main_nonlinear_terminal_v11 ==>
722 is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ MMs_v39 s v/\
723 (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
724 (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
725 (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
726 ~scs_is_str s v p /\ ~scs_is_str s v (p+1) /\ ~scs_is_str s v (p+3)
727 ==> (~(dist(v p,v(p+3)) = cstab /\ dist(v(p),v(p+1)) = cstab)))`,
731 THEN REWRITE_TAC[DE_MORGAN_THM]
732 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
733 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
734 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
737 THEN ASSUME_TAC(ARITH_RULE`3<4/\ 1<4/\ ~(4=0)`)
739 THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN]
740 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
741 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`s`;`v`]
742 THEN MP_TAC Local_lemmas.CVLF_LF_F
744 THEN SUBGOAL_THEN`!i. dist((v:num->real^3) i, v(SUC i))<= cstab`ASSUME_TAC
749 THEN MATCH_MP_TAC (GEN_ALL Axjrpnc.NORM_V_IN_BB_LE_CSTAB)
750 THEN EXISTS_TAC`s:scs_v39`
751 THEN ASM_REWRITE_TAC[]
753 THEN REWRITE_TAC[ADD1]
754 THEN THAYTHE_TAC (18-6)[`i`]
755 THEN REWRITE_TAC[cstab;h0]
758 THAYTHEL_ASM_TAC 0[`p`][ADD1]
759 THEN THAYTHEL_TAC 0[`p+3`][ARITH_RULE`SUC(p+3)=1*4+p`]
761 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
762 THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
763 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[DIST_SYM]
764 THEN REMOVE_ASSUM_TAC
766 THEN MP_TAC Jotswix.JOTSWIX
768 THEN THAYTHE_TAC 0[`s`;`FF`;`v`;`p`]
770 THEN SUBGOAL_THEN`scs_a_v39 s p (p + 1) < cstab`ASSUME_TAC;
773 THAYTHE_TAC (18-6)[`p`]
774 THEN REWRITE_TAC[cstab;h0]
779 THEN SUBGOAL_THEN`(!i. ~(i MOD 4 = (p + 2) MOD 4) ==> interior_angle1 (vec 0) FF ((v:num->real^3)i) < pi)`ASSUME_TAC;
782 THEN ASM_REWRITE_TAC[NOT_MOD_4_CASES]
783 THEN REPEAT STRIP_TAC;
786 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
787 THEN THAYTHES_TAC 0[`i`;`p`][MOD_MULT_ADD]
789 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1;scs_is_str]
790 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
791 THEN MRESA_TAC WL_IN_V[`SUC p`;`v:num->real^3`]
792 THEN MRESA_TAC WL_IN_V[`p+4-1`;`v:num->real^3`]
793 THEN MRESA_TAC WL_IN_V[`SUC p+4-1`;`v:num->real^3`]
794 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
795 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][GSYM ADD1]
796 THEN THAYTHE_TAC 0[`v (p+4-1)`]
803 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
804 THEN THAYTHES_TAC 0[`i`;`p+1`][MOD_MULT_ADD]
806 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1;scs_is_str]
807 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
808 THEN MRESA_TAC WL_IN_V[`SUC p`;`v:num->real^3`]
809 THEN MRESA_TAC WL_IN_V[`p+4-1`;`v:num->real^3`]
810 THEN MRESA_TAC WL_IN_V[`SUC p+4-1`;`v:num->real^3`]
811 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (SUC p)`;`v`;`(SUC p)`;`4`]
812 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][GSYM ADD1]
813 THEN THAYTHE_TAC 0[`v ((SUC p)+4-1)`]
820 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
821 THEN THAYTHES_TAC 0[`i`;`p+3`][MOD_MULT_ADD]
823 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1;scs_is_str]
824 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
825 THEN MRESA_TAC WL_IN_V[`(p+3)`;`v:num->real^3`]
826 THEN MRESA_TAC WL_IN_V[`p+4-1`;`v:num->real^3`]
827 THEN MRESA_TAC WL_IN_V[`(p+3)+4-1`;`v:num->real^3`]
828 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v ((p+3))`;`v`;`((p+3))`;`4`]
829 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v ((p+3))`][GSYM ADD1]
830 THEN THAYTHE_TAC 0[`v (((p+3))+4-1)`]
836 THEN MP_TAC(REAL_ARITH`dist (v p,v (p + 1)) <= cstab/\
837 dist (v p,v (p + 3)) <= cstab
838 ==> (dist (v p,v (p + 1)) = cstab/\dist (v p,v (p + 3)) = cstab)
839 \/ dist ((v:num->real^3) p,v (p + 1)) < cstab \/ dist (v p,v (p + 3)) < cstab`)
843 SUBGOAL_THEN`p MOD 4 IN scs_M s`ASSUME_TAC;
846 ASM_SIMP_TAC[scs_M;IN_ELIM_THM;DIVISION]
847 THEN MATCH_MP_TAC(SET_RULE`A==> A\/B`)
849 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;]
851 THEN THAYTHE_TAC 0[`p MOD 4`;`SUC(p MOD 4)`]
853 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
854 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
855 THEN THAYTHES_TAC 0[`p MOD 4`;`p`][MOD_REFL]
856 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
857 THEN THAYTHES_TAC 0[`SUC(p MOD 4)`;`SUC(p MOD 4) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD]
858 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
859 THEN THAYTHES_TAC 0[`SUC p MOD 4`;`SUC p`][MOD_REFL;ADD1;cstab;h0]
865 SUBGOAL_THEN`(p+3) MOD 4 IN scs_M s`ASSUME_TAC;
868 THEN ASM_SIMP_TAC[scs_M;IN_ELIM_THM;DIVISION]
869 THEN MATCH_MP_TAC(SET_RULE`A==> A\/B`)
871 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;]
873 THEN THAYTHE_TAC 0[`(p+3) MOD 4`;`SUC((p+3) MOD 4)`]
875 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
876 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
877 THEN THAYTHES_TAC 0[`(p+3) MOD 4`;`(p+3)`][MOD_REFL]
878 THEN ONCE_REWRITE_TAC[DIST_SYM]
879 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
880 THEN THAYTHES_TAC 0[`SUC((p+3) MOD 4)`;`SUC((p+3) MOD 4) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`SUC(p+3)=(1*4+p)`;MOD_MULT_ADD]
881 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
882 THEN THAYTHES_TAC 0[`p MOD 4`;`p`][MOD_REFL;ADD1;cstab;h0]
887 MP_TAC(SET_RULE`p MOD 4 IN scs_M s/\
888 (p + 3) MOD 4 IN scs_M s==>{p MOD 4,(p+3)MOD 4} SUBSET scs_M s`)
890 THEN MP_TAC B_LE_2h0_2_SCS_M_4
892 THEN MRESAL_TAC ASSWPOW[`s`;`v`;`p+1`][IN;ARITH_RULE`(a+1)+1=a+2/\ (a+1)+2=a+3`]
893 THEN POP_ASSUM MP_TAC
895 THEN ONCE_REWRITE_TAC[DIST_SYM]
896 THEN ONCE_REWRITE_TAC[Ocbicby.xrr_sym]
899 THEN ASM_REWRITE_TAC[]
914 (***************************)
915 let BASIC_IMP_NOT_J=prove(`scs_basic_v39 s==> (!p i. ~scs_J_v39 s p i)`,
916 REWRITE_TAC[scs_basic]
919 let CONDTION_A_LT_B=prove(`(!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
920 (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab))
921 ==> (!i. scs_a_v39 s i (i+1)< scs_b_v39 s i (i+1))`,
922 REWRITE_TAC[h0;cstab]
923 THEN REPEAT STRIP_TAC
924 THEN THAYTHE_TAC 0[`i`]
926 THEN REAL_ARITH_TAC);;
928 let A_EQ2_IMP_B=prove(`(!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
929 (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab))
930 /\ scs_a_v39 s p (p+1) = &2
931 ==> scs_b_v39 s p (p+1)= &2 * h0`,
933 THEN THAYTHE_TAC 1[`p`]
935 THEN ASM_REWRITE_TAC[cstab;h0]
936 THEN REAL_ARITH_TAC);;
938 let A_EQ2h0_IMP_B=prove(`(!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
939 (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab))
940 /\ scs_a_v39 s p (p+1) = &2 * h0
941 ==> scs_b_v39 s p (p+1)= cstab`,
943 THEN THAYTHE_TAC 1[`p`]
945 THEN ASM_REWRITE_TAC[cstab;h0]
946 THEN REAL_ARITH_TAC);;
949 let A_NOT_EQ2_IMP_B=prove(`(!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
950 (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab))
951 /\ ~(scs_a_v39 s p (p+1) = &2 )
952 ==> scs_a_v39 s p (p+1) = &2* h0 /\ scs_b_v39 s p (p+1)= cstab`,
954 THEN THAYTHE_TAC 1[`p`]);;
958 let B_LE_2h0_IMP_B=prove(`(!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
959 (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab))
960 /\ scs_b_v39 s p (p+1) <= &2 *h0
961 ==> scs_a_v39 s p (p+1) = &2 /\ scs_b_v39 s p (p+1)= &2*h0`,
964 THEN THAYTHE_TAC 0[`p`]
965 THEN ASM_REWRITE_TAC[cstab;h0]
966 THEN REAL_ARITH_TAC);;
969 let STR_MOD_EQ=prove(`is_scs_v39 s /\ scs_k_v39 s = k /\ v IN MMs_v39 s
971 (scs_is_str s v (p MOD k)<=> scs_is_str s v p)`,
972 REWRITE_TAC[IN;scs_is_str]
973 THEN REPEAT STRIP_TAC
974 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
975 THEN MP_TAC Yrtafyh.PROPERTY_OF_K_SCS
977 THEN MP_TAC(ARITH_RULE`1<k==> k-1<k`)
979 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
980 THEN THAYTHES_TAC 0[`p MOD k`;`p`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;MOD_REFL]
981 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
982 THEN THAYTHES_TAC 0[`SUC(p MOD k)`;`SUC p`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;MOD_REFL;Yxionxl2.MOD_SUC_MOD]
983 THEN MRESAS_TAC MOD_ADD_MOD[`p`;`k-1`;`k`][MOD_LT]
984 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
985 THEN THAYTHES_TAC 0[`(p MOD k)+k-1`;` p+k-1`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;MOD_REFL;Yxionxl2.MOD_SUC_MOD]);;
987 let IN_SCS_STR_CASES_4=prove(`
988 is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\ scs_is_str s v p==>
989 p MOD 4 IN {i | i < 4 /\ scs_is_str s v i}`,
991 THEN REPEAT STRIP_TAC
992 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\1<4/\ 3<4`)
993 THEN ASM_SIMP_TAC[IN_ELIM_THM;DIVISION]
995 THEN MRESAL_TAC STR_MOD_EQ[`4`;`s`;`v`;`p`][IN]);;
998 let FINITE_SET_STR=prove(`FINITE {i | i < k /\ scs_is_str s v i}`,
999 MATCH_MP_TAC FINITE_SUBSET
1000 THEN EXISTS_TAC`0..k`
1001 THEN ASM_REWRITE_TAC[FINITE_NUMSEG;IN_ELIM_THM;IN_NUMSEG;SUBSET]
1004 let NOT_STR_IN_CASES_4=prove(`!s v.
1005 is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\ scs_is_str s v p==>
1006 ~scs_is_str s v (p+1)/\ ~scs_is_str s v (p+2)/\ ~scs_is_str s v (p+3)`,
1009 THEN ASSUME_TAC(ARITH_RULE`~(4=0)`)
1010 THEN MRESA_TAC WGDHPPI[`s`;`v`]
1011 THEN MP_TAC IN_SCS_STR_CASES_4
1013 THEN MRESA_TAC FINITE_SET_STR[`4`;`s`;`v`]
1014 THEN MRESAS_TAC CARD_SUBSET_LE[`{p MOD 4}`;`{i | i < 4 /\ scs_is_str s v i}`][Geomdetail.CARD_SING;SET_RULE`a IN A==> {a} SUBSET A`]
1015 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`2`;`0`;`p`][ARITH_RULE`p+0=p/\ ~(2 MOD 4= 0 MOD 4)`]
1016 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`1`;`0`;`p`][ARITH_RULE`p+0=p/\ ~(1 MOD 4= 0 MOD 4)`]
1017 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`3`;`0`;`p`][ARITH_RULE`p+0=p/\ ~(3 MOD 4= 0 MOD 4)`]
1018 THEN MP_TAC(SET_RULE`{p MOD 4} = {i | i < 4 /\ scs_is_str s v i}/\
1019 ~((p + 2) MOD 4 = p MOD 4)/\
1020 ~((p + 1) MOD 4 = p MOD 4)/\
1021 ~((p + 3) MOD 4 = p MOD 4)
1022 ==> ~((p + 1) MOD 4 IN {i | i < 4 /\ scs_is_str s v i})/\
1023 ~((p + 2) MOD 4 IN {i | i < 4 /\ scs_is_str s v i})/\
1024 ~((p + 3) MOD 4 IN {i | i < 4 /\ scs_is_str s v i})`)
1029 THEN ASM_SIMP_TAC[IN_ELIM_THM; DIVISION;STR_MOD_EQ]);;
1032 let NOT_STR_IN_CASES_4_1=prove(`!s v.
1036 scs_is_str s v (p+1)
1037 ==> ~scs_is_str s v (p ) /\
1038 ~scs_is_str s v (p + 2) /\
1039 ~scs_is_str s v (p + 3)`,
1042 THEN MRESAL_TAC NOT_STR_IN_CASES_4[`p+1`;`s`;`v`][ARITH_RULE`(p+1)+1=p+2/\ (p+1)+2=p+3/\ (p+1)+3=1*4+p`]
1043 THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`1*4+p`][MOD_MULT_ADD]
1044 THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`p`][MOD_MULT_ADD]);;
1047 let PRO_ADD_NOT_IN_SCS_M=prove(`is_scs_v39 s/\ scs_a_v39 s i (i+1) = &2 * h0/\ scs_k_v39 s=k
1048 ==> i MOD k IN scs_M s`,
1049 REWRITE_TAC[IN_ELIM_THM;scs_M]
1051 THEN MP_TAC Yrtafyh.PROPERTY_OF_K_SCS
1053 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`i MOD k`;`SUC(i MOD k)`;`s`;`i`;`SUC(i MOD k) MOD k`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;DIVISION]
1054 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`i`;`SUC i MOD k`;`s`;`i`;`SUC i`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1055 THEN ASM_REWRITE_TAC[ADD1;h0]
1056 THEN REAL_ARITH_TAC);;
1058 let TUAPYYU_IMP_CASES=prove(`
1059 main_nonlinear_terminal_v11 ==>
1061 is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\
1062 (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
1063 (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
1064 (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
1065 ~scs_is_str s v p /\ ~scs_is_str s v (p+1)
1066 ==> dist(v p,v(p+1)) = &2\/ dist(v p,v(p+1)) = &2 * h0 \/ dist(v p,v(p+1)) = cstab)`,
1070 THEN THAYTHEL_TAC 0[`s`;`v`;`p`][]
1071 THEN THAYTHE_TAC 3[`p`]);;
1073 let SCS_M_CASES_4_EQ1=prove(`scs_k_v39 s = 4/\ is_scs_v39 s /\ {(p+1) MOD 4,(p+3)MOD 4} SUBSET scs_M s
1074 ==> scs_M s={(p+1) MOD 4,(p+3)MOD 4}`,
1076 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ ~(1 MOD 4 = 3 MOD 4)`)
1077 THEN MRESAS_TAC Planarity.CARD_2_FAN[`(p+1) MOD 4`;`(p+3) MOD 4`][Ocbicby.MOD_EQ_MOD_SHIFT]
1079 THEN REWRITE_TAC[ARITH_RULE`p+1=p+1`]
1081 THEN MP_TAC SCS_M_CASES_4_LE_2
1083 THEN MP_TAC Jlxfdmj.FINITE_SCS_M
1085 THEN MRESA_TAC CARD_SUBSET_LE[`{(p+1) MOD 4, (p + 3) MOD 4}`;`scs_M s`]);;
1090 let B_LE_2h0_2_SCS_M_4_1=prove(
1091 `scs_k_v39 s = 4/\ is_scs_v39 s /\ {(p+1) MOD 4,(p+3)MOD 4} SUBSET scs_M s
1092 ==> scs_b_v39 s (p+2) (p+3)<= &2*h0`,
1094 THEN MP_TAC SCS_M_CASES_4_EQ1
1096 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ ~(2 MOD 4 = 3 MOD 4)/\ ~(2 MOD 4 = 1 MOD 4)/\ 1<4`)
1097 THEN SUBGOAL_THEN`~((p+2) MOD 4 IN scs_M s)`ASSUME_TAC
1100 ASM_SIMP_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`;Ocbicby.MOD_EQ_MOD_SHIFT]
1101 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`2`;`1`;`p`][ARITH_RULE`p+0=p`];
1104 THEN REWRITE_TAC[scs_M;IN_ELIM_THM]
1105 THEN ASM_SIMP_TAC[DIVISION]
1106 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2) MOD 4`;`SUC ((p + 2) MOD 4)`;`s`;`p+2`;`SUC ((p + 2) MOD 4) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD]
1107 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2)`;`SUC (p + 2) MOD 4`;`s`;`p+2`;`SUC (p + 2)`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`SUC(p+2)=p+3`]
1108 THEN REAL_ARITH_TAC]);;
1111 let SCS_A_SYM=prove(`is_scs_v39 s
1112 ==> scs_a_v39 s i j= scs_a_v39 s j i`,
1113 REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;dist]
1116 let SCS_B_SYM=prove(`is_scs_v39 s
1117 ==> scs_b_v39 s i j= scs_b_v39 s j i`,
1118 REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;dist]
1124 (***************************)
1126 let PWEIWBZ= prove_by_refinement(`
1127 main_nonlinear_terminal_v11 ==>
1129 is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ MMs_v39 s v/\
1130 (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
1131 (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
1132 (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
1133 scs_a_v39 s p (p+1) = &2
1134 ==> dist(v p,v(p+1)) = &2)`,
1136 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
1137 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
1138 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
1140 THEN REPEAT RESA_TAC
1141 THEN ASSUME_TAC(ARITH_RULE`3<4/\ 1<4/\ ~(4=0)/\ 4-1=3/\ SUC (p + 3)= 1*4+p/\ SUC p= p+1`)
1143 THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN;scs_generic]
1144 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
1145 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`s`;`v`]
1146 THEN MP_TAC Local_lemmas.CVLF_LF_F
1148 THEN MP_TAC Tfitskc.SCS_DIAG_A_LE_DIST
1150 THEN MP_TAC(SET_RULE`(~scs_is_str s v p /\ ~scs_is_str s v (p+1))\/ scs_is_str s v p \/ scs_is_str s v (p+1)`)
1156 THEN MATCH_DICH_TAC 0
1157 THEN EXISTS_TAC`s:scs_v39`
1158 THEN ASM_REWRITE_TAC[IN];
1161 MRESAL_TAC NOT_STR_IN_CASES_4[`p`;`s`;`v`][IN]
1163 THEN ASM_REWRITE_TAC[scs_is_str;]
1165 THEN DICH_TAC(21-13)
1166 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;]
1168 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
1169 THEN THAYTHE_TAC 1[`p+3`;`p`]
1173 MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
1174 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
1175 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
1177 THEN POP_ASSUM MP_TAC
1178 THEN REWRITE_TAC[NOT_EXISTS_THM]
1180 THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (p)) V' E')` ASSUME_TAC;
1189 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1190 THEN THAYTHES_TAC 0[`(p+3)+1`;`p`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1192 THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p=(p+3)+1`]
1194 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1195 THEN THAYTHES_TAC 0[`(p+3)+2`;`p+1`][ARITH_RULE`(p+3)+2=1*4+p+1`;MOD_MULT_ADD]
1197 THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p+1=(p+3)+2`]
1199 THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v p`;`v (p+1)`;`(v:num->real^3) (p+3)`]
1200 THEN POP_ASSUM MP_TAC
1201 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
1203 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
1204 THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
1205 THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
1206 THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
1207 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+3)`;`V`]
1208 THEN SUBGOAL_THEN`(!j. ~(v j = v (p + 3)) ==> ~collinear {vec 0, (v:num->real^3) (p + 3), v j})`ASSUME_TAC
1214 THEN MATCH_DICH_TAC 1
1216 THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
1220 MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p+3`][ARITH_RULE`0+2=2`]
1222 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
1224 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1225 THEN THAYTHES_TAC 3[`v (p+1)`;`v(p+3)`][SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 3 MOD 4)`]
1226 THEN MP_TAC CONDTION_A_LT_B
1228 THEN MP_TAC(REAL_ARITH`scs_a_v39 s (p + 3) p <= dist (v (p + 3),v p)
1229 ==> scs_a_v39 s (p + 3) p = dist (v (p + 3),v p)\/ scs_a_v39 s (p + 3) p < dist (v (p + 3),(v:num->real^3) p)`)
1237 SUBGOAL_THEN`dist (v (p + 3),(v:num->real^3) p) < scs_b_v39 s (p + 3) p`
1241 THAYTHE_TAC 1[`p+3`]
1243 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`((p + 3) +1)`;`s`;`p+3`;`((p + 3)+1) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1244 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1245 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1246 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1251 MRESAS_TAC NUXCOEAv2[`s`;`4`;`v`;`p`;`p+3`][MOD_MULT_ADD;BASIC_IMP_NOT_J]
1255 MP_TAC(SET_RULE`~(&2=norm ((v:num->real^3) p))\/ norm (v p)= &2`)
1259 MRESAS_TAC IMJXPHRv2[`s`;`4`;`v`;`p`;][MOD_MULT_ADD;BASIC_IMP_NOT_J]
1262 MP_TAC(SET_RULE`(scs_a_v39 s (p+1) (p+2) = &2 )\/ ~((scs_a_v39 s (p+1) (p+2) = &2 ))`)
1267 SUBGOAL_THEN`scs_a_v39 s (p + 3) p < scs_b_v39 s (p + 3) p`
1271 THAYTHE_TAC (45-42)[`p+3`]
1273 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`((p + 3) +1)`;`s`;`p+3`;`((p + 3)+1) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1274 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1275 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1276 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1283 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][IN;ARITH_RULE`(p+1)+1=p+2`]
1284 THEN ASSUME_TAC(ARITH_RULE`(p+1)+1=p+2/\ (p+2)+1=p+3`)
1285 THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+1`]
1286 THEN THAYTHE_TAC (49-42)[`p+2`]
1287 THEN MP_TAC Cqaoqlr.CQAOQLR
1289 THEN THAYTHES_TAC 0[`s`;`v`;`p`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1290 THEN MATCH_DICH_TAC 0
1291 THEN REWRITE_TAC[h0]
1292 THEN REAL_ARITH_TAC;
1296 ASSUME_TAC(ARITH_RULE`(p+1)+1=p+2/\ (p+2)+1=p+3/\ (p+2)+3=1*4+p+1/\ (p+1)+3=1*4+p/\ (p+3)+1=1*4+p/\ (p+3)+3=1*4+p+2/\ (p+3)+2=1*4+p+1`)
1297 THEN MRESA_TAC A_NOT_EQ2_IMP_B[`s`;`p+1`]
1298 THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`1*4+p+1`][IN;MOD_MULT_ADD]
1299 THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`p+1`][IN;MOD_MULT_ADD;MOD_REFL]
1300 THEN THAYTHES_TAC (50-40)[`1 * 4 + p + 1`;`p+1`][MOD_MULT_ADD]
1303 THEN THAYTHE_TAC 0[`s`;`v`;`p+2`]
1304 THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p+1`;`4`;`s`]
1305 THEN MP_TAC(SET_RULE`scs_a_v39 s (p + 3) p = &2 \/ ~(scs_a_v39 s (p + 3) p = &2 )`)
1308 (**********CASES a 3 0 =2********************)
1312 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][IN];
1315 MP_TAC Jotswix.LEMMA_PWE1
1317 THEN THAYTHEL_TAC 0[`s`;`v`;`p`][scs_generic;IN;REAL_ARITH`a<=a`;scs_is_str]
1318 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1319 THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
1320 THEN MP_TAC Cuxvzoz.CJBDXXN
1322 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+1`;`v`]
1323 THEN ONCE_REWRITE_TAC[DIST_SYM]
1324 THEN MATCH_DICH_TAC 0
1326 THEN REWRITE_TAC[GSYM ADD1]
1327 THEN ASM_REWRITE_TAC[scs_generic]
1328 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1329 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
1330 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+1)`;`v`;`(p+1)`;`4`]
1331 THEN DICH_TAC(58-17)
1332 THEN ASM_REWRITE_TAC[scs_is_str]
1334 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][]
1335 THEN THAYTHE_TAC 0[`v (p)`]
1336 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) <= pi
1337 /\ ~(azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) = pi)
1338 ==> azim (vec 0) (v (p + 1)) (v (p + 2)) ((v:num->real^3) p) < pi`)
1340 THEN ONCE_REWRITE_TAC[DIST_SYM]
1341 THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
1342 &2 * #1.26 <= #3.01`]
1343 THEN REPEAT STRIP_TAC;
1347 THAYTHES_TAC(60-5)[`p`;`p+2`][SCS_DIAG_4_ADD0]
1349 THEN REWRITE_TAC[cstab]
1350 THEN REAL_ARITH_TAC;
1352 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1353 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
1354 THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+2)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 2 MOD 4)`]
1355 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
1356 THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+0)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
1358 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`]
1360 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+1)`;`v(p+2)`;`v p`]
1366 MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1367 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1369 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1370 THEN REPEAT RESA_TAC
1375 MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1376 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1378 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1379 THEN REPEAT RESA_TAC
1380 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;h0]
1381 THEN REAL_ARITH_TAC;
1385 THEN ONCE_REWRITE_TAC[DIST_SYM]
1389 THEN MP_TAC TUAPYYU_IMP_CASES
1391 THEN THAYTHEL_TAC 0[`s`;`v`;`p+2`][IN];
1394 (************CASES 2 3= 2**********)
1396 MP_TAC Jotswix.LEMMA_PWE2
1398 THEN THAYTHEL_TAC 0[`s`;`v`;`p`][scs_generic;IN;REAL_ARITH`a<=a/\ &2 <= &2 * #1.26`;scs_is_str;h0]
1399 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1400 THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
1401 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1402 THEN THAYTHES_TAC 0[`1*4+p+2`;`p+2`][MOD_MULT_ADD]
1403 THEN MP_TAC Cuxvzoz.CUXVZOZ
1405 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+3`;`v`]
1408 THEN REWRITE_TAC[GSYM ADD1]
1409 THEN ASM_REWRITE_TAC[scs_generic]
1410 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1411 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
1412 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+3)`;`v`;`(p+3)`;`4`]
1413 THEN DICH_TAC(60-19)
1414 THEN ASM_REWRITE_TAC[scs_is_str]
1416 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+3)`][]
1417 THEN THAYTHE_TAC 0[`v (p+2)`]
1418 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 3)) (v p) (v (p + 2)) <= pi
1419 /\ ~(azim (vec 0) (v (p + 3)) (v p) (v (p + 2)) = pi)
1420 ==> azim (vec 0) (v (p + 3)) ((v:num->real^3) p) (v (p + 2)) < pi`)
1422 THEN ONCE_REWRITE_TAC[DIST_SYM]
1423 THEN SUBGOAL_THEN`&3 <= dist ((v:num->real^3) p,v (p + 2))`ASSUME_TAC
1429 THAYTHES_TAC(62-5)[`p`;`p+2`][SCS_DIAG_4_ADD0]
1431 THEN REWRITE_TAC[cstab]
1432 THEN REAL_ARITH_TAC;
1434 SUBGOAL_THEN`(pi / &2 < azim (vec 0) (v (p + 3)) (v p) (v (p + 2)) \/
1435 azim (vec 0) (v p) (rho_node1 FF (v p)) (ivs_rho_node1 FF ((v:num->real^3) p)) < pi)`ASSUME_TAC
1442 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1443 THEN THAYTHEL_ASM_TAC(64-37)[`p+0`][]
1444 THEN THAYTHES_TAC(0)[`p+2`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 2 MOD 4)`]
1446 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 0 MOD 4)`]
1447 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`]
1449 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+3)`;`v(p)`;`v (p+2)`]
1453 SUBGOAL_THEN`scs_a_v39 s (p + 3) (1 * 4 + p) = &2`ASSUME_TAC
1458 MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1459 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1461 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1462 THEN REPEAT RESA_TAC
1466 SUBGOAL_THEN`scs_b_v39 s (p + 3) (1 * 4 + p) <= &2 * h0`ASSUME_TAC
1471 MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1472 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1474 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1475 THEN REPEAT RESA_TAC
1476 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;]
1477 THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+3`]
1482 ASM_REWRITE_TAC[cstab;REAL_ARITH`&2 <= #3.01`]
1483 THEN ONCE_REWRITE_TAC[DIST_SYM]
1485 THEN ONCE_REWRITE_TAC[DIST_SYM]
1486 THEN MP_TAC Cqaoqlr.CQAOQLR
1488 THEN THAYTHES_TAC 0[`s`;`v`;`p+3`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1490 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p)`;`(1 * 4 + p+1)`;`s`;`p`;`p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1491 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p)`;`(1 * 4 + p+1)`;`s`;`p`;`p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1492 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p+2)`;`(p+3)`;`s`;`p+2`;`p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1493 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p+2)`;`(p+3)`;`s`;`p+2`;`p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1494 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;`p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1495 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;`p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1496 THEN THAYTHEL_ASM_TAC(73-40)[`p+2`][]
1497 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`( p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1498 THEN THAYTHEL_ASM_TAC(1)[`p+3`][h0;cstab]
1499 THEN REAL_ARITH_TAC;
1501 (************CASES 2 3= 2* H0**********)
1504 MP_TAC Jotswix.LEMMA_PWE2
1506 THEN THAYTHEL_TAC 0[`s`;`v`;`p`][scs_generic;IN;REAL_ARITH`a<=a/\ &2 <= &2 * #1.26`;scs_is_str;h0]
1507 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1508 THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
1509 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1510 THEN THAYTHES_TAC 0[`1*4+p+2`;`p+2`][MOD_MULT_ADD]
1511 THEN MP_TAC Cuxvzoz.CUXVZOZ
1513 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+3`;`v`]
1516 THEN REWRITE_TAC[GSYM ADD1]
1517 THEN ASM_REWRITE_TAC[scs_generic]
1518 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1519 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
1520 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+3)`;`v`;`(p+3)`;`4`]
1521 THEN DICH_TAC(60-19)
1522 THEN ASM_REWRITE_TAC[scs_is_str]
1524 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+3)`][]
1525 THEN THAYTHE_TAC 0[`v (p+2)`]
1526 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 3)) (v p) (v (p + 2)) <= pi
1527 /\ ~(azim (vec 0) (v (p + 3)) (v p) (v (p + 2)) = pi)
1528 ==> azim (vec 0) (v (p + 3)) ((v:num->real^3) p) (v (p + 2)) < pi`)
1530 THEN ONCE_REWRITE_TAC[DIST_SYM]
1531 THEN SUBGOAL_THEN`&3 <= dist ((v:num->real^3) p,v (p + 2))`ASSUME_TAC
1537 THAYTHES_TAC(62-5)[`p`;`p+2`][SCS_DIAG_4_ADD0]
1539 THEN REWRITE_TAC[cstab]
1540 THEN REAL_ARITH_TAC;
1542 SUBGOAL_THEN`(pi / &2 < azim (vec 0) (v (p + 3)) (v p) (v (p + 2)) \/
1543 azim (vec 0) (v p) (rho_node1 FF (v p)) (ivs_rho_node1 FF ((v:num->real^3) p)) < pi)`ASSUME_TAC
1550 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1551 THEN THAYTHEL_ASM_TAC(64-37)[`p+0`][]
1552 THEN THAYTHES_TAC(0)[`p+2`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 2 MOD 4)`]
1554 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 0 MOD 4)`]
1555 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`]
1557 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+3)`;`v(p)`;`v (p+2)`]
1561 SUBGOAL_THEN`scs_a_v39 s (p + 3) (1 * 4 + p) = &2`ASSUME_TAC
1566 MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1567 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1569 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1570 THEN REPEAT RESA_TAC
1574 SUBGOAL_THEN`scs_b_v39 s (p + 3) (1 * 4 + p) <= &2 * h0`ASSUME_TAC
1579 MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1580 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1582 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1583 THEN REPEAT RESA_TAC
1584 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;]
1585 THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+3`]
1590 ASM_REWRITE_TAC[cstab;REAL_ARITH`&2 <= &2 * #1.26 /\ &2 * #1.26 <= #3.01`;h0]
1591 THEN ONCE_REWRITE_TAC[DIST_SYM]
1593 THEN ONCE_REWRITE_TAC[DIST_SYM]
1594 THEN MP_TAC Cqaoqlr.CQAOQLR
1596 THEN THAYTHES_TAC 0[`s`;`v`;`p+3`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1598 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p)`;`(1 * 4 + p+1)`;`s`;`p`;`p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1599 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p)`;`(1 * 4 + p+1)`;`s`;`p`;`p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1600 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p+2)`;`(p+3)`;`s`;`p+2`;`p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1601 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p+2)`;`(p+3)`;`s`;`p+2`;`p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1602 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;`p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1603 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;`p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1604 THEN THAYTHEL_ASM_TAC(73-40)[`p+2`][]
1605 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`( p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1606 THEN THAYTHEL_ASM_TAC(1)[`p+3`][h0;cstab]
1607 THEN REAL_ARITH_TAC;
1611 (*************CASES a 3 0 NOT = 2************)
1614 MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1615 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1616 THEN MRESA_TAC A_NOT_EQ2_IMP_B [`s`;`p+3`]
1617 THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p+3`;`4`;`s`]
1618 THEN MRESAL_TAC B_LE_2h0_2_SCS_M_4_1[`s`;`p`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`]
1619 THEN MRESA_TAC B_LE_2h0_IMP_B[`s`;`p+2`]
1622 THEN THAYTHEL_TAC 0[`s`;`v`;`p+2`][IN];
1628 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][IN];
1631 MP_TAC Jotswix.LEMMA_PWE3
1633 THEN THAYTHEL_TAC 0[`s`;`v`;`p`][scs_generic;IN;REAL_ARITH`a<=a`;scs_is_str]
1634 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1635 THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
1636 THEN MP_TAC Cuxvzoz.CJBDXXN
1638 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+1`;`v`]
1639 THEN ONCE_REWRITE_TAC[DIST_SYM]
1640 THEN MATCH_DICH_TAC 0
1642 THEN REWRITE_TAC[GSYM ADD1]
1643 THEN ASM_REWRITE_TAC[scs_generic]
1644 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1645 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
1646 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+1)`;`v`;`(p+1)`;`4`]
1650 THEN ASM_REWRITE_TAC[scs_is_str]
1652 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][]
1653 THEN THAYTHE_TAC 0[`v (p)`]
1654 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) <= pi
1655 /\ ~(azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) = pi)
1656 ==> azim (vec 0) (v (p + 1)) (v (p + 2)) ((v:num->real^3) p) < pi`)
1658 THEN ONCE_REWRITE_TAC[DIST_SYM]
1659 THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
1660 &2 * #1.26 <= #3.01`]
1661 THEN REPEAT STRIP_TAC;
1665 THAYTHES_TAC(69-5)[`p`;`p+2`][SCS_DIAG_4_ADD0]
1667 THEN REWRITE_TAC[cstab]
1668 THEN REAL_ARITH_TAC;
1670 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1671 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
1672 THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+2)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 2 MOD 4)`]
1673 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
1674 THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+0)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
1676 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`]
1678 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+1)`;`v(p+2)`;`v p`]
1679 THEN ASM_REWRITE_TAC[DIHV_SYM];
1684 MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1685 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1687 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1688 THEN REPEAT RESA_TAC
1693 MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1694 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1696 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1697 THEN REPEAT RESA_TAC
1698 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;h0]
1699 THEN REAL_ARITH_TAC;
1703 (*************CASES 1 2= cstab **************)
1706 MP_TAC Jotswix.LEMMA_PWE3
1708 THEN THAYTHEL_TAC 0[`s`;`v`;`p`][scs_generic;IN;REAL_ARITH`a<=a/\ &2 * #1.26 <= #3.01`;scs_is_str;h0;cstab]
1709 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1710 THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
1711 THEN MP_TAC Cuxvzoz.CJBDXXN
1713 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+1`;`v`]
1714 THEN ONCE_REWRITE_TAC[DIST_SYM]
1715 THEN MATCH_DICH_TAC 0
1717 THEN REWRITE_TAC[GSYM ADD1]
1718 THEN ASM_REWRITE_TAC[scs_generic]
1719 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1720 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
1721 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+1)`;`v`;`(p+1)`;`4`]
1725 THEN ASM_REWRITE_TAC[scs_is_str]
1727 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][]
1728 THEN THAYTHE_TAC 0[`v (p)`]
1729 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) <= pi
1730 /\ ~(azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) = pi)
1731 ==> azim (vec 0) (v (p + 1)) (v (p + 2)) ((v:num->real^3) p) < pi`)
1733 THEN ONCE_REWRITE_TAC[DIST_SYM]
1734 THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
1735 &2 * #1.26 <= #3.01`]
1736 THEN REPEAT STRIP_TAC;
1740 THAYTHES_TAC(69-5)[`p`;`p+2`][SCS_DIAG_4_ADD0]
1742 THEN REWRITE_TAC[cstab]
1743 THEN REAL_ARITH_TAC;
1745 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1746 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
1747 THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+2)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 2 MOD 4)`]
1748 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
1749 THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+0)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
1751 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`]
1753 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+1)`;`v(p+2)`;`v p`]
1754 THEN ASM_REWRITE_TAC[DIHV_SYM];
1759 MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1760 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1762 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1763 THEN REPEAT RESA_TAC
1768 MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1769 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1771 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1772 THEN REPEAT RESA_TAC
1773 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;h0]
1774 THEN REAL_ARITH_TAC;
1784 (*********scs_is_str p+1***********)
1789 MRESAL_TAC NOT_STR_IN_CASES_4_1[`p`;`s`;`v`][IN]
1791 THEN ASM_REWRITE_TAC[scs_is_str;]
1793 THEN DICH_TAC(21-13)
1794 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;]
1796 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
1797 THEN THAYTHE_TAC 1[`p+1`;`(p+2)`]
1801 MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
1802 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
1803 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
1805 THEN POP_ASSUM MP_TAC
1806 THEN REWRITE_TAC[NOT_EXISTS_THM]
1808 THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (p)) V' E')` ASSUME_TAC;
1816 ASSUME_TAC(ARITH_RULE`(p+1)+1=p+2/\ (p+1)+3= 1*4+p/\ (p+3)+1= 1*4+p/\ (p+3)+2= 1*4+p+1/\ (p+3)+3= 1*4+p+2`)
1817 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1818 THEN THAYTHES_TAC 0[`1*4+p`;`p`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1819 THEN DICH_TAC(32-20)
1821 THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v (p+1)`;`v (p+2)`;`(v:num->real^3) (p)`]
1822 THEN POP_ASSUM MP_TAC
1823 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
1825 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
1826 THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
1827 THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
1828 THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
1829 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+2)`;`V`]
1830 THEN SUBGOAL_THEN`(!j. ~(v j = v (p)) ==> ~collinear {vec 0, (v:num->real^3) (p ), v j})`ASSUME_TAC
1836 THEN MATCH_DICH_TAC 1
1838 THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
1842 MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p`][ARITH_RULE`0+2=2`]
1844 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
1846 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1847 THEN THAYTHES_TAC 3[`v (p+0)`;`v(p+2)`][SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(0 MOD 4 = 2 MOD 4)`]
1849 THEN REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
1850 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1852 THEN MP_TAC CONDTION_A_LT_B
1854 THEN MP_TAC(REAL_ARITH`scs_a_v39 s (p+1) (p+2) <= dist (v (p+1),v (p+2))
1855 ==> scs_a_v39 s (p+1) (p+2) = dist (v (p+1),v (p+2))\/ scs_a_v39 s (p+1) (p+2) < dist (v (p+1),(v:num->real^3) (p+2))`)
1863 SUBGOAL_THEN`dist (v (p + 1),(v:num->real^3) (p+2)) < scs_b_v39 s (p + 1) (p+2)`
1867 THAYTHE_TAC 1[`p+1`]
1871 MRESAS_TAC NUXCOEAv2[`s`;`4`;`v`;`p+1`;`p+2`][MOD_MULT_ADD;BASIC_IMP_NOT_J]
1873 THEN ONCE_REWRITE_TAC[DIST_SYM]
1874 THEN MRESA_TAC SCS_A_SYM[`s`;`1*4+p`;`p+1`]
1875 THEN MRESA_TAC SCS_A_SYM[`s`;`p+1`;`p+2`]
1876 THEN MRESA_TAC SCS_B_SYM[`s`;`p+1`;`p+2`]
1877 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;`(p+1)`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1878 THEN ASM_SIMP_TAC[DIST_SYM];
1881 MP_TAC(SET_RULE`~(&2=norm ((v:num->real^3) (p+1)))\/ norm (v (p+1))= &2`)
1885 MRESAS_TAC IMJXPHRv2[`s`;`4`;`v`;`p+1`;][MOD_MULT_ADD;BASIC_IMP_NOT_J]
1887 THEN MRESA_TAC SCS_A_SYM[`s`;`1*4+p`;`p+1`]
1888 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;`(p+1)`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1889 THEN ASM_SIMP_TAC[DIST_SYM];
1897 MP_TAC(SET_RULE`(scs_a_v39 s (p+3) (p) = &2 )\/ ~((scs_a_v39 s (p+3) (p) = &2 ))`)
1902 MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;` p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1903 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;` p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1904 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p+2)`;`(p+3)`;`s`;`p+2`;` p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1905 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;` p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1906 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p+2)`;`(p+3)`;`s`;`p+2`;` p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1907 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;` p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1908 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p)`;`(1 * 4 + p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1909 THEN MRESAL_TAC STR_MOD_EQ[`4`;`s`;`v`;`1*4+p`][IN;MOD_MULT_ADD]
1910 THEN MRESAL_TAC STR_MOD_EQ[`4`;`s`;`v`;`p`][IN;MOD_MULT_ADD]
1913 THEN THAYTHEL_TAC 0[`s`;`v`;`p+3`][IN;ARITH_RULE`(p+1)+1=p+2`]
1914 THEN THAYTHEL_ASM_TAC (55-42)[`p+1`][]
1915 THEN THAYTHEL_TAC 0[`p+2`][ARITH_RULE`(i+2)+1=i+3`]
1916 THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+3`]
1917 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(1 * 4 + p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1918 THEN THAYTHES_TAC (58-40)[`(1 * 4 + p+1)`;`p+1`][MOD_MULT_ADD]
1919 THEN MP_TAC Cqaoqlr.CQAOQLR
1921 THEN THAYTHES_TAC 0[`s`;`v`;`p+3`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1922 THEN MATCH_DICH_TAC 0
1923 THEN REWRITE_TAC[h0]
1924 THEN REAL_ARITH_TAC;
1928 ASSUME_TAC(ARITH_RULE`(p+1)+1=p+2/\ (p+2)+1=p+3/\ (p+2)+3=1*4+p+1/\ (p+1)+3=1*4+p/\ (p+3)+1=1*4+p/\ (p+3)+3=1*4+p+2/\ (p+3)+2=1*4+p+1/\ (p+1)+2=p+3`)
1929 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;` p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1930 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;` p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1931 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p+2)`;`(p+3)`;`s`;`p+2`;` p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1932 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;` p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1933 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p+2)`;`(p+3)`;`s`;`p+2`;` p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1934 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;` p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1935 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p)`;`(1 * 4 + p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1936 THEN MRESA_TAC A_NOT_EQ2_IMP_B[`s`;`p+3`]
1937 THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`1*4+p+2`][IN;MOD_MULT_ADD]
1938 THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`p+2`][IN;MOD_MULT_ADD;MOD_REFL]
1939 THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`1*4+p`][IN;MOD_MULT_ADD]
1940 THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`p`][IN;MOD_MULT_ADD;MOD_REFL]
1943 THAYTHES_TAC (59-40)[`1 * 4 + p + 2`;`p+2`][MOD_MULT_ADD]
1944 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1945 THEN THAYTHES_TAC 0[`1*4+p+1`;`p+1`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1946 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1947 THEN THAYTHES_TAC 0[`1*4+p+3`;`p+3`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1950 THEN THAYTHE_TAC 0[`s`;`v`;`p+3`]
1951 THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p+3`;`4`;`s`]
1952 THEN MP_TAC(SET_RULE`scs_a_v39 s (p + 1) (p+2) = &2 \/ ~(scs_a_v39 s (p + 1) (p+2) = &2 )`)
1955 (**********CASES a 1 2 =2********************)
1960 THEN THAYTHEL_TAC 0[`s`;`v`;`p+3`][IN];
1967 MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1968 THEN MP_TAC Jotswix.LEMMA_PWE2
1970 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][scs_generic;IN;REAL_ARITH`a<=a`;]
1972 THEN ASM_REWRITE_TAC[scs_is_str]
1974 THEN MP_TAC Cuxvzoz.CUXVZOZ
1976 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p`;`v`]
1977 THEN MATCH_DICH_TAC 0
1979 THEN REWRITE_TAC[GSYM ADD1]
1980 THEN ASM_REWRITE_TAC[scs_generic]
1981 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1982 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
1983 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
1987 THEN ASM_REWRITE_TAC[scs_is_str]
1989 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][]
1990 THEN THAYTHE_TAC 0[`v (p+3)`]
1991 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) <= pi
1992 /\ ~(azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) = pi)
1993 ==> azim (vec 0) (v p) (v (p + 1)) ((v:num->real^3) (p + 3)) < pi`)
1995 THEN ONCE_REWRITE_TAC[DIST_SYM]
1996 THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
1997 &2 * #1.26 <= #3.01`]
1998 THEN REPEAT STRIP_TAC;
2002 THAYTHES_TAC(71-5)[`p+1`;`p+3`][SCS_DIAG_4_ADD2]
2004 THEN REWRITE_TAC[cstab]
2005 THEN REAL_ARITH_TAC;
2009 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2010 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+1)`;`V`]
2011 THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+1)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
2013 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
2015 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+3)`;`V`]
2016 THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+3)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 0 MOD 4)`]
2018 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
2020 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v p`;`v(p+1)`;`v (p+3)`]
2032 THEN POP_ASSUM MP_TAC
2033 THEN ONCE_REWRITE_TAC[DIST_SYM]
2035 THEN MP_TAC TUAPYYU_IMP_CASES
2037 THEN THAYTHEL_TAC 0[`s`;`v`;`p+2`][IN];
2040 (************CASES 2 3= 2**********)
2043 MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2044 THEN MP_TAC Jotswix.LEMMA_PWE1
2046 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][scs_generic;IN;REAL_ARITH`a<=a/\ &2 <= &2 * #1.26`;h0]
2048 THEN ASM_REWRITE_TAC[scs_is_str]
2050 THEN MP_TAC Cuxvzoz.CJBDXXN
2052 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+2`;`v`]
2054 THEN ONCE_REWRITE_TAC[DIST_SYM]
2056 THEN REWRITE_TAC[GSYM ADD1]
2057 THEN ASM_REWRITE_TAC[scs_generic]
2058 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
2059 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+2)`;`(1 * 4 + p+1)`;`s`;`p+2`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2060 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2)`;`(1 * 4 + p+1)`;`s`;`p+2`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2061 THEN MRESA_TAC SCS_A_SYM[`s`;`p+1`;`p+2`]
2062 THEN MRESA_TAC SCS_B_SYM[`s`;`p+1`;`p+2`]
2063 THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+1`]
2064 THEN ONCE_REWRITE_TAC[DIST_SYM]
2065 THEN ASM_SIMP_TAC[REAL_ARITH`a<=a`]
2066 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+2)`;`v`;`(p+2)`;`4`]
2070 THEN ASM_REWRITE_TAC[scs_is_str]
2072 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+2)`][]
2073 THEN THAYTHE_TAC 0[`v (p+1)`]
2074 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) <= pi
2075 /\ ~(azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) = pi)
2076 ==> azim (vec 0) (v (p + 2)) (v (p + 3)) ((v:num->real^3) (p + 1)) < pi`)
2078 THEN ONCE_REWRITE_TAC[DIST_SYM]
2079 THEN SUBGOAL_THEN`&3 <= dist ((v:num->real^3) (p+1),v (p + 3))`ASSUME_TAC
2085 THAYTHES_TAC(77-5)[`p+1`;`p+3`][SCS_DIAG_4_ADD2]
2087 THEN REWRITE_TAC[cstab]
2088 THEN REAL_ARITH_TAC;
2090 SUBGOAL_THEN`(pi / &2 < azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) \/
2091 azim (vec 0) ((v:num->real^3) (p + 1)) (rho_node1 FF (v (p + 1)))
2092 (ivs_rho_node1 FF (v (p + 1))) <
2100 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2101 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+2)`;`v (p+1)`;`V`]
2102 THEN THAYTHES_TAC 0[`v (p+2)`;`v (p+1)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 2 MOD 4)`]
2103 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+2)`;`v (p+3)`;`V`]
2104 THEN THAYTHES_TAC 0[`v (p+2)`;`v (p+3)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 2 MOD 4)`]
2105 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+2)`;`v(p+3)`;`v (p+1)`]
2109 ASM_REWRITE_TAC[cstab;REAL_ARITH`&2 <= #3.01`]
2111 THEN MP_TAC Cqaoqlr.CQAOQLR
2113 THEN THAYTHES_TAC 0[`s`;`v`;`p`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
2114 THEN MATCH_DICH_TAC 0
2115 THEN THAYTHEL_ASM_TAC(80-40)[`p+2`][h0;cstab]
2116 THEN REAL_ARITH_TAC;
2118 (************CASES 2 3= 2* H0**********)
2123 MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2124 THEN MP_TAC Jotswix.LEMMA_PWE1
2126 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][scs_generic;IN;REAL_ARITH`a<=a/\ &2 <= &2 * #1.26`;h0]
2128 THEN ASM_REWRITE_TAC[scs_is_str]
2130 THEN MP_TAC Cuxvzoz.CJBDXXN
2132 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+2`;`v`]
2134 THEN ONCE_REWRITE_TAC[DIST_SYM]
2136 THEN REWRITE_TAC[GSYM ADD1]
2137 THEN ASM_REWRITE_TAC[scs_generic]
2138 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
2139 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+2)`;`(1 * 4 + p+1)`;`s`;`p+2`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2140 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2)`;`(1 * 4 + p+1)`;`s`;`p+2`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2141 THEN MRESA_TAC SCS_A_SYM[`s`;`p+1`;`p+2`]
2142 THEN MRESA_TAC SCS_B_SYM[`s`;`p+1`;`p+2`]
2143 THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+1`]
2144 THEN ONCE_REWRITE_TAC[DIST_SYM]
2145 THEN ASM_SIMP_TAC[REAL_ARITH`a<=a`]
2146 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+2)`;`v`;`(p+2)`;`4`]
2150 THEN ASM_REWRITE_TAC[scs_is_str]
2152 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+2)`][]
2153 THEN THAYTHE_TAC 0[`v (p+1)`]
2154 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) <= pi
2155 /\ ~(azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) = pi)
2156 ==> azim (vec 0) (v (p + 2)) (v (p + 3)) ((v:num->real^3) (p + 1)) < pi`)
2158 THEN ONCE_REWRITE_TAC[DIST_SYM]
2159 THEN SUBGOAL_THEN`&3 <= dist ((v:num->real^3) (p+1),v (p + 3))`ASSUME_TAC
2165 THAYTHES_TAC(77-5)[`p+1`;`p+3`][SCS_DIAG_4_ADD2]
2167 THEN REWRITE_TAC[cstab]
2168 THEN REAL_ARITH_TAC;
2170 SUBGOAL_THEN`(pi / &2 < azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) \/
2171 azim (vec 0) ((v:num->real^3) (p + 1)) (rho_node1 FF (v (p + 1)))
2172 (ivs_rho_node1 FF (v (p + 1))) <
2180 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2181 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+2)`;`v (p+1)`;`V`]
2182 THEN THAYTHES_TAC 0[`v (p+2)`;`v (p+1)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 2 MOD 4)`]
2183 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+2)`;`v (p+3)`;`V`]
2184 THEN THAYTHES_TAC 0[`v (p+2)`;`v (p+3)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 2 MOD 4)`]
2185 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+2)`;`v(p+3)`;`v (p+1)`]
2189 ASM_REWRITE_TAC[cstab;REAL_ARITH`&2 <= &2 * #1.26 /\ &2 * #1.26 <= #3.01`;h0]
2191 THEN MP_TAC Cqaoqlr.CQAOQLR
2193 THEN THAYTHES_TAC 0[`s`;`v`;`p`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
2194 THEN MATCH_DICH_TAC 0
2195 THEN THAYTHEL_ASM_TAC(80-40)[`p+2`][h0;cstab]
2196 THEN REAL_ARITH_TAC;
2199 (*************CASES a 1 2 NOT = 2************)
2202 MRESA_TAC A_NOT_EQ2_IMP_B [`s`;`p+1`]
2203 THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p+1`;`4`;`s`]
2204 THEN MRESAL_TAC B_LE_2h0_2_SCS_M_4_1[`s`;`p`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`]
2205 THEN MRESA_TAC B_LE_2h0_IMP_B[`s`;`p+2`]
2208 THEN THAYTHEL_TAC 0[`s`;`v`;`p+2`][IN];
2214 THEN THAYTHEL_TAC 0[`s`;`v`;`p+3`][IN];
2217 MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2218 THEN MP_TAC Jotswix.LEMMA_PWE4
2220 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][scs_generic;IN;REAL_ARITH`a<=a`;]
2222 THEN ONCE_REWRITE_TAC[DIST_SYM]
2223 THEN ASM_REWRITE_TAC[scs_is_str;REAL_ARITH`a<=a`]
2225 THEN ONCE_REWRITE_TAC[DIST_SYM]
2231 MP_TAC Cuxvzoz.CUXVZOZ
2233 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p`;`v`]
2234 THEN MATCH_DICH_TAC 0
2236 THEN REWRITE_TAC[GSYM ADD1]
2237 THEN ASM_REWRITE_TAC[scs_generic]
2238 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
2239 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
2240 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
2244 THEN ASM_REWRITE_TAC[scs_is_str]
2246 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][]
2247 THEN THAYTHE_TAC 0[`v (p+3)`]
2248 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) <= pi
2249 /\ ~(azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) = pi)
2250 ==> azim (vec 0) (v p) (v (p + 1)) ((v:num->real^3) (p + 3)) < pi`)
2252 THEN ONCE_REWRITE_TAC[DIST_SYM]
2253 THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
2254 &2 * #1.26 <= #3.01`]
2255 THEN REPEAT STRIP_TAC;
2259 THAYTHES_TAC(78-5)[`p+1`;`p+3`][SCS_DIAG_4_ADD2]
2261 THEN REWRITE_TAC[cstab]
2262 THEN REAL_ARITH_TAC;
2266 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2267 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+1)`;`V`]
2268 THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+1)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
2270 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
2272 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+3)`;`V`]
2273 THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+3)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 0 MOD 4)`]
2275 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
2277 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v p`;`v(p+1)`;`v (p+3)`]
2282 (*************CASES 0 3= cstab **************)
2286 MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2287 THEN MP_TAC Jotswix.LEMMA_PWE4
2289 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][scs_generic;IN;REAL_ARITH`a<=a`;]
2291 THEN ONCE_REWRITE_TAC[DIST_SYM]
2292 THEN ASM_REWRITE_TAC[scs_is_str;REAL_ARITH`&2 * #1.26 <= #3.01`;h0;cstab]
2294 THEN ONCE_REWRITE_TAC[DIST_SYM]
2297 MP_TAC Cuxvzoz.CUXVZOZ
2299 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p`;`v`]
2300 THEN MATCH_DICH_TAC 0
2302 THEN REWRITE_TAC[GSYM ADD1]
2303 THEN ASM_REWRITE_TAC[scs_generic]
2304 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
2305 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
2306 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
2310 THEN ASM_REWRITE_TAC[scs_is_str]
2312 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][]
2313 THEN THAYTHE_TAC 0[`v (p+3)`]
2314 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) <= pi
2315 /\ ~(azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) = pi)
2316 ==> azim (vec 0) (v p) (v (p + 1)) ((v:num->real^3) (p + 3)) < pi`)
2318 THEN ONCE_REWRITE_TAC[DIST_SYM]
2319 THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
2320 &2 * #1.26 <= #3.01`]
2321 THEN REPEAT STRIP_TAC;
2325 THAYTHES_TAC(78-5)[`p+1`;`p+3`][SCS_DIAG_4_ADD2]
2327 THEN REWRITE_TAC[cstab]
2328 THEN REAL_ARITH_TAC;
2332 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2333 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+1)`;`V`]
2334 THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+1)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
2336 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
2338 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+3)`;`V`]
2339 THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+3)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 0 MOD 4)`]
2341 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
2343 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v p`;`v(p+1)`;`v (p+3)`]
2355 let h0_CSTAB_LT_4=prove(`&2< &2*h0 /\ cstab< &4/\ &2<= &2*h0 /\ cstab<= &4
2356 /\ &2*h0< &4/\ &2< &4`,
2357 REWRITE_TAC[cstab;h0]
2358 THEN REAL_ARITH_TAC);;
2366 let VASYYAU= prove_by_refinement(`
2367 main_nonlinear_terminal_v11 ==>
2369 is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ MMs_v39 s v/\
2370 (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
2371 (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
2372 (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
2374 ==> (dist(v p,v (p+1)) = scs_a_v39 s p (p+1) /\ dist(v p,v (p+3)) = scs_a_v39 s p (p+3)))`,
2378 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
2379 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
2380 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
2382 THEN REPLICATE_TAC 11 (RESA_TAC)
2383 THEN ASSUME_TAC(ARITH_RULE`3<4/\ 1<4/\ ~(4=0)/\ 4-1=3/\ SUC (p + 3)= 1*4+p/\ SUC p= p+1`)
2385 THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN;scs_generic]
2386 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
2387 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`s`;`v`]
2388 THEN MP_TAC Local_lemmas.CVLF_LF_F
2390 THEN MP_TAC Tfitskc.SCS_DIAG_A_LE_DIST
2392 THEN MP_TAC Jlxfdmj.SCS_A_2
2394 THEN THAYTHE_TAC 0[`p`]
2395 THEN MP_TAC(REAL_ARITH`&2 <= scs_a_v39 s p (p + 1)
2396 ==> scs_a_v39 s p (p+1) = &2\/ &2 < scs_a_v39 s p (p + 1)`)
2402 THEN THAYTHE_TAC 0[`s`;`v`;`p`]
2404 THEN ASM_REWRITE_TAC[scs_is_str]
2408 MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
2409 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
2410 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
2412 THEN POP_ASSUM MP_TAC
2413 THEN REWRITE_TAC[NOT_EXISTS_THM]
2415 THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (p)) V' E')` ASSUME_TAC;
2425 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2426 THEN THAYTHES_TAC 0[`(p+3)+1`;`p`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2428 THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p=(p+3)+1`]
2430 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2431 THEN THAYTHES_TAC 0[`(p+3)+2`;`p+1`][ARITH_RULE`(p+3)+2=1*4+p+1`;MOD_MULT_ADD]
2433 THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p+1=(p+3)+2`]
2435 THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v p`;`v (p+1)`;`(v:num->real^3) (p+3)`]
2436 THEN POP_ASSUM MP_TAC
2437 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
2439 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
2440 THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
2441 THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
2442 THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
2443 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+3)`;`V`]
2444 THEN SUBGOAL_THEN`(!j. ~(v j = v (p + 3)) ==> ~collinear {vec 0, (v:num->real^3) (p + 3), v j})`ASSUME_TAC
2451 THEN MATCH_DICH_TAC 1
2453 THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
2458 MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p+3`][ARITH_RULE`0+2=2`]
2460 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
2462 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2463 THEN THAYTHES_TAC 3[`v (p+1)`;`v(p+3)`][SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 3 MOD 4)`]
2464 THEN MP_TAC CONDTION_A_LT_B
2469 MRESAS_TAC NUXCOEAv2[`s`;`4`;`v`;`p`;`p+1`][MOD_MULT_ADD;BASIC_IMP_NOT_J]
2471 THEN MRESA_TAC SCS_A_SYM[`s`;`p`;`p+1`]
2472 THEN MRESA_TAC SCS_B_SYM[`s`;`p`;`p+1`]
2473 THEN ONCE_REWRITE_TAC[DIST_SYM]
2474 THEN ASM_REWRITE_TAC[]
2475 THEN THAYTHE_TAC 2[`p`]
2478 ASSUME_TAC(ARITH_RULE`(p+3)+1=1*4+p/\ (p+1)+1=p+2/\ (p+2)+1=p+3`)
2479 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2480 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2481 THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
2482 THEN MP_TAC Jlxfdmj.SCS_A_2
2484 THEN THAYTHE_TAC 0[`p+3`]
2485 THEN MP_TAC(REAL_ARITH`&2 <= scs_a_v39 s (p + 3) p
2486 ==> scs_a_v39 s (p+3) p = &2\/ &2 < scs_a_v39 s (p + 3) p`)
2492 THEN THAYTHE_TAC 0[`s`;`v`;`p+3`]
2493 THEN MRESA_TAC SCS_A_SYM[`s`;`p+3`;`p`]
2494 THEN ONCE_REWRITE_TAC[DIST_SYM]
2495 THEN ASM_REWRITE_TAC[]
2496 THEN ONCE_REWRITE_TAC[DIST_SYM]
2498 THEN ASM_REWRITE_TAC[scs_is_str]
2502 MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
2503 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
2504 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
2506 THEN POP_ASSUM MP_TAC
2507 THEN REWRITE_TAC[NOT_EXISTS_THM]
2509 THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (p)) V' E')` ASSUME_TAC;
2519 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2520 THEN THAYTHES_TAC 0[`(p+3)+2`;`p+1`][ARITH_RULE`(p+3)+2=1*4+p+1`;MOD_MULT_ADD]
2522 THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p+1=(p+3)+2`]
2524 THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v p`;`v (p+1)`;`(v:num->real^3) (p+3)`]
2525 THEN POP_ASSUM MP_TAC
2526 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
2528 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
2529 THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
2530 THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
2531 THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
2532 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+3)`;`V`]
2533 THEN SUBGOAL_THEN`(!j. ~(v j = v (p + 3)) ==> ~collinear {vec 0, (v:num->real^3) (p + 3), v j})`ASSUME_TAC
2540 THEN MATCH_DICH_TAC 1
2542 THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
2547 MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p+3`][ARITH_RULE`0+2=2`]
2549 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
2551 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2552 THEN THAYTHES_TAC 3[`v (p+1)`;`v(p+3)`][SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 3 MOD 4)`]
2553 THEN MP_TAC CONDTION_A_LT_B
2558 MRESAS_TAC NUXCOEAv2[`s`;`4`;`v`;`p`;`p+3`][MOD_MULT_ADD;BASIC_IMP_NOT_J]
2560 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2561 THEN THAYTHE_TAC 1[`p+3`]
2565 MP_TAC(REAL_ARITH`&2 < scs_a_v39 s p (p + 1)
2566 /\ &2 < scs_a_v39 s (p + 3) p
2567 ==> ~(scs_a_v39 s (p + 3) p = &2)/\ ~(scs_a_v39 s p (p + 1)= &2)`)
2569 THEN MP_TAC A_NOT_EQ2_IMP_B
2571 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2572 THEN MRESA_TAC A_NOT_EQ2_IMP_B[`s`;`p+3`]
2573 THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p`;`4`;`s`]
2574 THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p+3`;`4`;`s`]
2575 THEN MRESAL_TAC B_LE_2h0_2_SCS_M_4[`s`;`p`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`]
2576 THEN MRESA_TAC B_LE_2h0_IMP_B[`s`;`p+1`]
2577 THEN MRESA_TAC B_LE_2h0_IMP_B[`s`;`p+2`]
2578 THEN MRESAL_TAC NOT_STR_IN_CASES_4[`p`;`s`;`v`][IN]
2581 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][IN]
2584 THEN THAYTHEL_TAC 0[`s`;`v`;`p+2`][IN]
2585 THEN DICH_TAC (44-13)
2586 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39]
2588 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
2589 THEN THAYTHEL_ASM_TAC 1[`p`;`p+1`][]
2590 THEN THAYTHE_TAC 0[`p+3`;`p`];
2594 MP_TAC(SET_RULE`~(&2=norm ((v:num->real^3) p))\/ norm (v p)= &2`)
2602 THEN ASM_REWRITE_TAC[scs_is_str]
2606 MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
2607 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
2608 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
2610 THEN POP_ASSUM MP_TAC
2611 THEN REWRITE_TAC[NOT_EXISTS_THM]
2613 THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (p)) V' E')` ASSUME_TAC;
2623 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2624 THEN THAYTHES_TAC 0[`(p+3)+2`;`p+1`][ARITH_RULE`(p+3)+2=1*4+p+1`;MOD_MULT_ADD]
2626 THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p+1=(p+3)+2`]
2628 THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v p`;`v (p+1)`;`(v:num->real^3) (p+3)`]
2629 THEN POP_ASSUM MP_TAC
2630 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
2632 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
2633 THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
2634 THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
2635 THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
2636 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+3)`;`V`]
2637 THEN SUBGOAL_THEN`(!j. ~(v j = v (p + 3)) ==> ~collinear {vec 0, (v:num->real^3) (p + 3), v j})`ASSUME_TAC
2644 THEN MATCH_DICH_TAC 1
2646 THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
2651 MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p+3`][ARITH_RULE`0+2=2`]
2653 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
2655 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2656 THEN THAYTHES_TAC 3[`v (p+1)`;`v(p+3)`][SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 3 MOD 4)`]
2657 THEN MP_TAC CONDTION_A_LT_B
2662 MRESAS_TAC IMJXPHRv2[`s`;`4`;`v`;`p`;][MOD_MULT_ADD;BASIC_IMP_NOT_J]
2667 MRESAS_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`p`][Ckqowsa_3_points.in_ball_annulus;dist]
2668 THEN MRESAS_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`p+1`][Ckqowsa_3_points.in_ball_annulus;dist]
2669 THEN MRESAS_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`p+2`][Ckqowsa_3_points.in_ball_annulus;dist]
2670 THEN MRESAS_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`p+3`][Ckqowsa_3_points.in_ball_annulus;dist]
2671 THEN MRESAL_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`v p`;`v (p+3)`][dist;VECTOR_ARITH`vec 0- A= --A`; NORM_NEG]
2672 THEN MRESAL_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`v (p+1)`;`v (p)`][dist;VECTOR_ARITH`vec 0- A= --A`; NORM_NEG]
2673 THEN MRESAL_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`v (p+1)`;`v (p+2)`][dist;VECTOR_ARITH`vec 0- A= --A`; NORM_NEG]
2674 THEN MRESAL_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`v (p+2)`;`v (p+3)`][dist;VECTOR_ARITH`vec 0- A= --A`; NORM_NEG]
2675 THEN MRESA_TAC Trigonometry.KEITDWB[`vec 0:real^3`;`v (p+1)`;`v (p+3)`;`v (p+2)`];
2681 THEN ASM_REWRITE_TAC[scs_is_str]
2687 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2688 THEN THAYTHES_TAC 0[`(p+3)+2`;`p+1`][ARITH_RULE`(p+3)+2=1*4+p+1`;MOD_MULT_ADD]
2690 THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p+1=(p+3)+2`]
2692 THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v p`;`v (p+1)`;`(v:num->real^3) (p+3)`]
2693 THEN POP_ASSUM MP_TAC
2694 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
2696 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
2697 THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
2698 THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
2699 THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
2700 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+3)`;`V`]
2701 THEN SUBGOAL_THEN`(!j. ~(v j = v (p + 3)) ==> ~collinear {vec 0, (v:num->real^3) (p + 3), v j})`ASSUME_TAC
2708 THEN MATCH_DICH_TAC 1
2710 THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
2715 MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p+3`][ARITH_RULE`0+2=2`]
2717 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
2719 THEN MP_TAC(SET_RULE`v p IN aff_gt {vec 0} {v (p + 1), v (p + 3)}
2720 /\ aff_gt {vec 0} {v (p + 1), v (p + 3)} SUBSET aff_ge {vec 0} {v (p + 1), v (p + 3)}
2721 ==> (v:num->real^3) p IN aff_ge {vec 0} {v (p + 1), v (p + 3)}`)
2722 THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]
2724 THEN MRESA_TAC Iunbuig.ARCV_ADD_AFF_GE[`vec 0:real^3`;`v (p+1)`;`v (p+3)`;`v (p)`]
2725 THEN DICH_TAC(79-67)
2727 THEN REWRITE_TAC[GSYM dist]
2728 THEN ONCE_REWRITE_TAC[DIST_SYM]
2729 THEN ASSUME_TAC(h0_CSTAB_LT_4)
2730 THEN MP_TAC(REAL_ARITH` norm ((v:num->real^3) (p + 1)) <= &2 * h0 /\ &2<= norm (v (p + 1))/\
2731 norm ((v:num->real^3) (p + 3)) <= &2 * h0 /\ &2<= norm (v (p + 3))/\
2732 norm ((v:num->real^3) (p + 2)) <= &2 * h0 /\ &2<= norm (v (p + 2))/\
2733 cstab< &4/\ &2 * h0< &4 /\ &2< &2 *h0
2734 /\ dist (v p,v (p + 1)) <= cstab
2735 /\ &2* h0<= dist (v p,v (p + 1))
2736 /\ dist (v p,v (p + 3)) <= cstab
2737 /\ &2* h0<= dist (v p,v (p + 3))
2738 ==> norm (v (p + 1)) < &4 /\ &0< norm (v (p + 1))/\
2739 norm (v (p + 3)) < &4 /\ &0< norm (v (p + 3))/\
2740 norm (v (p + 2)) < &4 /\ &0< norm (v (p + 2))/\
2741 dist (v p,v (p + 1))< &4/\ &2<= dist (v p,v (p + 1))/\ &0< dist (v p,v (p + 1))/\
2742 dist (v p,v (p + 3))< &4/\ &2<= dist (v p,v (p + 3))/\ &0< dist (v p,v (p + 3))/\
2743 &2< dist (v p,v (p + 1))/\
2744 &2< dist (v p,v (p + 3))/\
2749 THEN ONCE_REWRITE_TAC[DIST_SYM]
2750 THEN ASM_REWRITE_TAC[]
2751 THEN ONCE_REWRITE_TAC[DIST_SYM]
2753 THEN MRESAS_TAC Oxlzlez.DIST_IMP_UPS_X_POS[`vec 0:real^3`;`v (p)`;`v (p+1)`][]
2755 THEN ASM_SIMP_TAC[dist;VECTOR_ARITH`vec 0- A= -- A`; NORM_NEG;REAL_ARITH`a<=b/\ b<c==> a<c`]
2756 THEN REWRITE_TAC[GSYM dist]
2758 THEN MRESAS_TAC Ocbicby.arclength_xrr[`(&2)`;`(norm (v (p + 1)))`;`(dist (v p,v (p + 1)))`][REAL_ARITH`a*a= a pow 2`]
2759 THEN ONCE_REWRITE_TAC[Arc_properties.arc_sym]
2760 THEN ASM_REWRITE_TAC[]
2761 THEN ONCE_REWRITE_TAC[Arc_properties.arc_sym]
2762 THEN MRESAS_TAC Oxlzlez.DIST_IMP_UPS_X_POS[`vec 0:real^3`;`v (p)`;`v (p+3)`][]
2764 THEN ASM_SIMP_TAC[dist;VECTOR_ARITH`vec 0- A= -- A`; NORM_NEG;REAL_ARITH`a<=b/\ b<c==> a<c`]
2765 THEN REWRITE_TAC[GSYM dist]
2767 THEN MRESAS_TAC Ocbicby.arclength_xrr[`(&2)`;`(norm (v (p + 3)))`;`(dist (v p,v (p + 3)))`][REAL_ARITH`a*a= a pow 2`]
2768 THEN ONCE_REWRITE_TAC[DIST_SYM]
2769 THEN ASM_REWRITE_TAC[]
2770 THEN ONCE_REWRITE_TAC[DIST_SYM]
2771 THEN MRESAS_TAC Oxlzlez.DIST_IMP_UPS_X_POS[`vec 0:real^3`;`v (p+2)`;`v (p+3)`][]
2773 THEN ASM_SIMP_TAC[dist;VECTOR_ARITH`vec 0- A= -- A`; NORM_NEG;REAL_ARITH`a<=b/\ b<c==> a<c`]
2774 THEN REWRITE_TAC[GSYM dist]
2776 THEN MRESAS_TAC Ocbicby.arclength_xrr[`(norm (v (p + 2)))`;`(norm (v (p + 3)))`;`(dist (v (p+2),v (p + 3)))`][REAL_ARITH`a*a= a pow 2`]
2777 THEN MRESAS_TAC Oxlzlez.DIST_IMP_UPS_X_POS[`vec 0:real^3`;`v (p+1)`;`v (p+2)`][]
2779 THEN ASM_SIMP_TAC[dist;VECTOR_ARITH`vec 0- A= -- A`; NORM_NEG;REAL_ARITH`a<=b/\ b<c==> a<c`]
2780 THEN REWRITE_TAC[GSYM dist]
2782 THEN MRESAS_TAC Ocbicby.arclength_xrr[`(norm (v (p + 1)))`;`(norm (v (p + 2)))`;`(dist (v (p+1),v (p + 2)))`][REAL_ARITH`a*a= a pow 2`]
2783 THEN MRESAL_TAC Ocbicby.xrr_increasing[`&2`;`(norm (v (p + 1)))`;`&2`;`(dist (v p,v (p + 1)))`][REAL_ARITH`&0<= &2`]
2784 THEN MRESAL_TAC Ocbicby.xrr_increasing[`&2`;`(norm (v (p + 3)))`;`&2`;`(dist (v (p+3),v (p)))`][REAL_ARITH`&0<= &2`]
2786 THEN ONCE_REWRITE_TAC[DIST_SYM]
2787 THEN ASM_REWRITE_TAC[]
2788 THEN ONCE_REWRITE_TAC[DIST_SYM]
2790 THEN MRESA_TAC Ocbicby.xrr_sym[`(norm (v (p + 2)))`;`(norm (v (p + 1)))`;`(dist (v (p+1),v (p+2)))`]
2791 THEN MRESAL_TAC Ocbicby.xrr_decreasing[`&2`;`(norm (v (p + 2)))`;`(norm (v (p + 1)))`;`(dist (v (p+2),v (p+3)))`][REAL_ARITH`&0<= &2`]
2792 THEN MRESAL_TAC Ocbicby.xrr_decreasing[`&2`;`(norm (v (p + 2)))`;`(norm (v (p + 3)))`;`(dist (v (p+1),v (p+2)))`][REAL_ARITH`&0<= &2`]
2793 THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`(&2)`;`(norm (v (p + 1)))`;` (dist (v p,v (p + 1)))`][REAL_ARITH`a*a= a pow 2`]
2794 THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`(&2)`;`(norm (v (p + 3)))`;` (dist (v (p+3),v (p)))`][REAL_ARITH`a*a= a pow 2`]
2796 THEN ONCE_REWRITE_TAC[DIST_SYM]
2797 THEN ASM_REWRITE_TAC[]
2798 THEN ONCE_REWRITE_TAC[DIST_SYM]
2800 THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`(norm (v (p + 1)))`;`(norm (v (p + 2)))`;` (dist (v (p+1),v (p + 2)))`][REAL_ARITH`a*a= a pow 2`]
2801 THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`(norm (v (p + 2)))`;`(norm (v (p + 3)))`;` (dist (v (p+2),v (p + 3)))`][REAL_ARITH`a*a= a pow 2`]
2802 THEN MP_TAC(REAL_ARITH`xrr (&2) (norm ((v:num->real^3) (p + 1))) (&2) <
2803 xrr (&2) (norm (v (p + 1))) (dist (v p,v (p + 1)))/\
2804 xrr (&2) (norm (v (p + 3))) (&2) <
2805 xrr (&2) (norm (v (p + 3))) (dist (v (p + 3),v p))/\
2806 xrr (norm (v (p + 1))) (norm (v (p + 2))) (&2) <=
2807 xrr (&2) (norm (v (p + 1))) (&2)/\
2808 xrr (norm (v (p + 2))) (norm (v (p + 3))) (&2) <=
2809 xrr (&2) (norm (v (p + 3))) (&2)/\
2810 &0 < xrr (&2) (norm (v (p + 1))) (dist (v p,v (p + 1)))/\
2811 xrr (&2) (norm (v (p + 1))) (dist (v p,v (p + 1))) < &16/\
2812 &0 < xrr (&2) (norm (v (p + 3))) (dist (v (p + 3),v p))/\
2813 xrr (&2) (norm (v (p + 3))) (dist (v (p + 3),v p)) < &16/\
2814 &0 < xrr (norm (v (p + 1))) (norm (v (p + 2))) (&2)/\
2815 xrr (norm (v (p + 1))) (norm (v (p + 2))) (&2) < &16/\
2816 &0 < xrr (norm (v (p + 2))) (norm (v (p + 3))) (&2)/\
2817 xrr (norm (v (p + 2))) (norm (v (p + 3))) (&2) < &16
2818 ==> xrr (&2) (norm (v (p + 1))) (dist (v p,v (p + 1))) <= &16 /\
2819 &0 <= xrr (&2) (norm (v (p + 1))) (&2)/\
2820 xrr (&2) (norm (v (p + 3))) (dist (v (p + 3),v p)) <= &16 /\
2821 &0 <= xrr (&2) (norm (v (p + 3))) (&2)/\
2822 xrr (&2) (norm (v (p + 1))) (&2) <= &16 /\
2823 &0 <= xrr (norm (v (p + 1))) (norm (v (p + 2))) (&2)/\
2824 xrr (&2) (norm (v (p + 3))) (&2) <= &16 /\
2825 &0 <= xrr (norm (v (p + 2))) (norm (v (p + 3))) (&2)
2828 THEN MRESAL_TAC ACS_MONO_LT[`&1 - xrr (&2) (norm (v (p + 1))) (dist (v p,v (p + 1))) / &8`;`&1 - xrr (&2) (norm (v (p + 1))) (&2) / &8`]
2829 [REAL_ARITH`&1- a/ &8< &1- b/ &8 <=> b<a`;REAL_ARITH`&1- a/ &8<= &1<=> &0<=a`;
2830 REAL_ARITH`(-- &1) <= &1- a/ &8<=> a<= &16`]
2831 THEN MRESAL_TAC ACS_MONO_LT[`&1 - xrr (&2) (norm (v (p + 3))) (dist (v (p+3),v (p ))) / &8`;`&1 - xrr (&2) (norm (v (p + 3))) (&2) / &8`]
2832 [REAL_ARITH`&1- a/ &8< &1- b/ &8 <=> b<a`;REAL_ARITH`&1- a/ &8<= &1<=> &0<=a`;
2833 REAL_ARITH`(-- &1) <= &1- a/ &8<=> a<= &16`]
2834 THEN MRESAL_TAC ACS_MONO_LE[`&1 - xrr (&2) (norm (v (p + 1))) (&2) / &8`;`&1 - xrr (norm (v (p + 1))) (norm (v (p + 2))) (&2) / &8`]
2835 [REAL_ARITH`&1- a/ &8<= &1- b/ &8 <=> b<=a`;REAL_ARITH`&1- a/ &8<= &1<=> &0<=a`;
2836 REAL_ARITH`(-- &1) <= &1- a/ &8<=> a<= &16`]
2837 THEN MRESAL_TAC ACS_MONO_LE[`&1 - xrr (&2) (norm (v (p + 3))) (&2) / &8`;`&1 - xrr (norm (v (p + 2))) (norm (v (p + 3))) (&2) / &8`]
2838 [REAL_ARITH`&1- a/ &8<= &1- b/ &8 <=> b<=a`;REAL_ARITH`&1- a/ &8<= &1<=> &0<=a`;
2839 REAL_ARITH`(-- &1) <= &1- a/ &8<=> a<= &16`]
2844 THEN REAL_ARITH_TAC;
2855 let check_completeness_claimA_concl =
2856 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)