1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
3 (* Section: Conclusions *)
4 (* Chapter: Local Fan *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
10 remaining conclusions from appendix to Local Fan chapter
12 svn 3270 contains deprecated terminal SCS cases
16 module Appendix = struct
23 (* Proved in Lunar_deform.MHAEYJN *)
27 convex_local_fan (V,E,FF) /\
29 deformation f V (a,b) /\
30 interior_angle1 (vec 0) FF v < pi /\
34 (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u') /\
35 (!t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u})
40 IMAGE (IMAGE (\v. f v t)) E,
41 IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\
42 lunar (v,w) (IMAGE (\v. f v t) V)
43 (IMAGE (IMAGE (\v. f v t)) E)))`;;
47 convex_local_fan (V,E,FF) /\
49 deformation f V (a,b) /\
50 (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==>
51 interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi)
56 IMAGE (IMAGE (\v. f v t)) E,
57 IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\
58 generic (IMAGE (\v. f v t) V)
59 (IMAGE (IMAGE (\v. f v t)) E)))`;;
64 {v,x,u,w,w1} SUBSET ball_annulus /\ packing {v,x,u,w,w1} /\ ~(v = x) /\ ~(v = u) /\ ~(v=w)/\ ~(v=w1) /\ ~(x = u)/\ ~(x=w)/\ ~(x=w1)/\ ~(u=w)/\ ~(u=w1) /\ ~(w=w1)
70 ==> ?v1 u1 w2. u1 IN {v,x,u,w,w1}
71 /\ u1 IN {v,x,u,w,w1} /\ w2 IN {v,x,u,w,w1}/\ ~(v1=u1)/\ ~(u1=w2) /\ ~(v1=w2) /\
72 &2 < norm(v1-u1) /\ &2 < norm(v1 - w2)
73 /\ norm(v1-u1) <= &1 + sqrt(&5)/\ norm(v1-w2)<= &1 + sqrt(&5)`;;
75 let arc1553_v39 = new_definition `arc1553_v39 = arclength (&2) (&2) (sqrt(#15.53))`;;
78 let cstab=new_definition ` cstab= #3.01`;;
80 let rho_fun = new_definition `rho_fun y = &1 + (inv (&2 * h0 - &2)) * (inv pi) * sol0 * (y - &2)`;;
82 let rho_rho_fun = prove_by_refinement(
83 `!y. rho_fun y = rho y`,
86 REWRITE_TAC[Sphere.rho;rho_fun;Sphere.const1;Sphere.ly;Sphere.interp];
87 REWRITE_TAC[GSYM Nonlinear_lemma.sol0_EQ_sol_y;Sphere.h0];
88 REWRITE_TAC[arith `a + b = a + c <=> c = b`];
90 MATCH_MP_TAC (arith `(sol0/pi)*(&1 - a) = (sol0/pi)*(c*e) ==> sol0/pi - sol0/pi * a = c * inv pi * sol0 * e`);
96 let tau_fun = new_definition `tau_fun V E f = sum (f) (\e. rho_fun(norm(FST e)) * (azim_in_fan e E)) - (pi + sol0) * &(CARD f -2)`;;
98 let tau3 = new_definition `tau3 (v1:real^3) v2 v3 =
99 rho (norm v1) * dihV (vec 0) v1 v2 v3 + rho(norm v2) * dihV (vec 0) v2 v3 v1 +
100 rho(norm v3) * dihV (vec 0) v3 v1 v2 - (pi + sol0)`;;
103 let standard = new_definition
104 ` standard v w <=> &2 <= norm(v-w) /\ norm (v-w) <= &2 *h0 `;;
106 let protracted = new_definition
107 ` protracted v w <=> &2 * h0 <= norm(v-w) /\ norm (v-w) <= sqrt (&8) `;;
109 let diagonal0 = new_definition
110 ` (diagonal0 (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) <=> ~(v = w) /\ ~({v,w} IN E) `;;
112 let diagonal1 = new_definition
113 ` diagonal1 (V,E) <=> !v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E)
114 ==> &2 * h0 <= norm(v-w) `;;
116 let main_estimate= new_definition
117 ` main_estimate(V,E,f) <=>
118 convex_local_fan(V,E,f) /\
120 V SUBSET ball_annulus /\
127 let torsor = new_definition
128 ` torsor (s:A->bool) k (f:A->A) <=> (!x. x IN s ==> (f x) IN s) /\ (!x1 x2. x1 IN s /\ x2 IN s /\ f x1 = f x2 ==> x1=x2) /\ (!i x. 0 < i /\ i < k /\ x IN s ==> ~((f POWER i) x = x)) /\ (!x. x IN s==> (f POWER k) x = x)
131 let tgt = new_definition `tgt = #1.541`;;
133 let d_tame = new_definition `d_tame n =
134 if n = 3 then &0 else
135 if n = 4 then #0.206 else
136 if n = 5 then #0.4819 else
137 if n = 6 then #0.712 else tgt`;;
139 (* rename d_tame2 -> tame_table_d, for compatibility with the rest of the project. *)
142 let d_tame2 = new_definition `d_tame2 r s =
143 if (r + 2 * s <= 3) then &0
145 #0.103 * (&2 - &s) + #0.2759 * (&r + &2 * &s - &4)`;;
147 let tame_table_d_tame2 = prove_by_refinement(
148 `!r s. tame_table_d r s = if (r + 2 * s <= 3) then &0
150 #0.103 * (&2 - &s) + #0.2759 * (&r + &2 * &s - &4)`,
153 REWRITE_TAC[Sphere.tame_table_d];
154 REPEAT WEAKER_STRIP_TAC;
155 REWRITE_TAC[arith `r + 2 * s > 3 <=> ~(r + 2 * s <= 3)`];
157 BY(ASM_REWRITE_TAC[]);
163 let JEJTVGB_std_concl =
165 convex_local_fan (V,E,FF) /\
167 V SUBSET ball_annulus /\
168 4 <= CARD V /\ CARD V <= 6 /\
169 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w)) /\
170 (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) ==>
171 d_tame (CARD V) <= tau_fun V E FF`;;
173 let JEJTVGB_std3_concl =
178 norm v1 <= &2 * h0 /\
179 norm v2 <= &2 * h0 /\
180 norm v3 <= &2 * h0 /\
184 dist(v1,v2) <= &2 * h0 /\
185 dist(v1,v3) <= &2 * h0 /\
186 dist(v2,v3) <= &2 * h0 ==>
187 &0 <= tau3 v1 v2 v3`;;
189 let JEJTVGB_pent_diag_concl =
191 convex_local_fan (V,E,FF) /\
193 V SUBSET ball_annulus /\
195 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w)) /\
196 (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) ==>
197 #0.616 <= tau_fun V E FF`;;
199 let JEJTVGB_pent_pro_concl =
201 convex_local_fan (V,E,FF) /\
203 V SUBSET ball_annulus /\
205 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w)) /\
207 (!v w. {v,w} IN E /\ ~({v,w} = {v0,w0}) ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\
209 &2 *h0 <= dist(v0,w0) /\ dist(v0,w0) <= sqrt8)
211 #0.616 <= tau_fun V E FF`;;
213 let JEJTVGB_quad_pro_concl =
215 convex_local_fan (V,E,FF) /\
217 V SUBSET ball_annulus /\
219 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w)) /\
221 (!v w. {v,w} IN E /\ ~({v,w} = {v0,w0}) ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\
223 &2 *h0 <= dist(v0,w0) /\ dist(v0,w0) <= sqrt8)
225 #0.477 <= tau_fun V E FF`;;
227 let JEJTVGB_quad_diag_concl =
229 convex_local_fan (V,E,FF) /\
231 V SUBSET ball_annulus /\
233 (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &3 <= dist(v,w)) /\
234 (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) ==>
235 #0.467 <= tau_fun V E FF`;;
238 let co = [JEJTVGB_std_concl;JEJTVGB_std3_concl;JEJTVGB_pent_diag_concl;JEJTVGB_pent_pro_concl;
239 JEJTVGB_quad_pro_concl;JEJTVGB_quad_diag_concl] in
242 let JEJTVGB_assume_v39 = new_definition (mk_eq (`JEJTVGB_assume_v39:bool`,JEJTVGB_concl));;
244 (* I'll use periodic functions to SCSs for now *)
246 let peropp = new_definition `peropp (f:num->A) k i = f (k - SUC(i MOD k))`;;
248 let peropp2 = new_definition `peropp2 (f:num->num->A) k i j = f (k - SUC(i MOD k)) (k - SUC(j MOD k))`;;
250 let peropp_periodic = prove_by_refinement(
251 `!(f:num->A) k. periodic (peropp f k) k`,
254 REPEAT WEAKER_STRIP_TAC;
255 REWRITE_TAC[Oxl_def.periodic;peropp];
256 ONCE_REWRITE_TAC[arith `i + k = 1 * k + i`];
257 BY(REWRITE_TAC[MOD_MULT_ADD])
261 let scs_data = `(k:num,d:real,a,alpha,beta,b,J,lo,hi,str)`;;
263 let scs_exists = MESON[] `?(x: (
269 (num -> num -> real) #
270 (num -> num -> bool) #
273 (num -> bool))). T`;;
275 let scs_v39 = REWRITE_RULE[] (new_type_definition "scs_v39" ("scs_v39", "dest_scs_v39") scs_exists);;
277 let scs_k_v39 = new_definition `scs_k_v39 s = part0 (dest_scs_v39 s)`;;
278 let scs_d_v39 = new_definition `scs_d_v39 s = part1 (dest_scs_v39 s)`;;
280 let scs_a_v39 = new_definition `scs_a_v39 s = part2 (dest_scs_v39 s)`;;
281 let scs_am_v39 = new_definition `scs_am_v39 s = part3 (dest_scs_v39 s)`;;
282 let scs_bm_v39 = new_definition `scs_bm_v39 s = part4 (dest_scs_v39 s)`;;
283 let scs_b_v39 = new_definition `scs_b_v39 s = part5 (dest_scs_v39 s)`;;
285 let scs_J_v39 = new_definition `scs_J_v39 s = part6 (dest_scs_v39 s)`;;
286 let scs_lo_v39 = new_definition `scs_lo_v39 s = part7 (dest_scs_v39 s)`;;
287 let scs_hi_v39 = new_definition `scs_hi_v39 s = part8 (dest_scs_v39 s)`;;
288 let scs_str_v39 = new_definition `scs_str_v39 s = SND(drop3(drop3 (dest_scs_v39 s)))`;;
290 let arcmax_v39 = new_definition `arcmax_v39 s (p1,p2) =
291 arclength (&2) (&2) (scs_bm_v39 s p1 p2)`;;
293 let scs_components = prove_by_refinement(
294 `!s. dest_scs_v39 s = (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s ,scs_bm_v39 s,scs_b_v39 s,scs_J_v39 s,
295 scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s)`,
298 REWRITE_TAC[Wrgcvdr_cizmrrh.PAIR_EQ2;scs_k_v39;scs_d_v39;scs_a_v39;];
299 REWRITE_TAC[scs_am_v39;scs_bm_v39;scs_b_v39;];
300 REWRITE_TAC[scs_J_v39;scs_hi_v39;scs_lo_v39;];
301 REWRITE_TAC[scs_str_v39];
302 BY(REWRITE_TAC[Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.part2;Misc_defs_and_lemmas.part3;Misc_defs_and_lemmas.part4; Misc_defs_and_lemmas.part5;Misc_defs_and_lemmas.part6;Misc_defs_and_lemmas.part7;Misc_defs_and_lemmas.drop0;Misc_defs_and_lemmas.drop3;Misc_defs_and_lemmas.drop1;Misc_defs_and_lemmas.part0;Misc_defs_and_lemmas.part8;Misc_defs_and_lemmas.drop2])
308 let scs_k_v39_explicit = prove_by_refinement(
309 `!k d a b alpha beta J lo str. scs_k_v39 (scs_v39 (k,d,a,alpha,beta,b,J,lo,hi,str)) = k`,
312 BY(REWRITE_TAC[scs_k_v39;scs_v39;Misc_defs_and_lemmas.part0])
316 let scs_d_v39_explicit = prove_by_refinement(
317 `!k d a b alpha beta J lo str. scs_d_v39 (scs_v39 (k,d,a,alpha,beta,b,J,lo,hi,str)) = d`,
320 BY(REWRITE_TAC[scs_d_v39;scs_v39;Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.drop0;FST])
324 let scs_a_v39_explicit = prove_by_refinement(
325 `!k d a b alpha beta J lo str. scs_a_v39 (scs_v39 (k,d,a,alpha,beta,b,J,lo,hi,str)) = a`,
328 BY((REWRITE_TAC[scs_a_v39;scs_v39;Misc_defs_and_lemmas.part2;Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.drop1;FST]))
332 let scs_am_v39_explicit = prove_by_refinement(
333 `!k d a b alpha beta J lo str. scs_am_v39 (scs_v39 (k,d,a,alpha,beta,b,J,lo,hi,str)) = alpha`,
336 BY((REWRITE_TAC[scs_am_v39;scs_v39;Misc_defs_and_lemmas.part3;Misc_defs_and_lemmas.drop2;FST]))
340 let scs_bm_v39_explicit = prove_by_refinement(
341 `!k d a b alpha beta J lo str. scs_bm_v39 (scs_v39 (k,d,a,alpha,beta,b,J,lo,hi,str)) = beta`,
344 ((REWRITE_TAC[scs_bm_v39;scs_v39;Misc_defs_and_lemmas.part4;Misc_defs_and_lemmas.drop3;FST]))
348 let scs_b_v39_explicit = prove_by_refinement(
349 `!k d a b alpha beta J lo str. scs_b_v39 (scs_v39 (k,d,a,alpha,beta,b,J,lo,hi,str)) = b`,
352 ((REWRITE_TAC[scs_b_v39;scs_v39;Misc_defs_and_lemmas.part5;Misc_defs_and_lemmas.drop3;FST]))
356 let scs_J_v39_explicit = prove_by_refinement(
357 `!k d a b alpha beta J lo str. scs_J_v39 (scs_v39 (k,d,a,alpha,beta,b,J,lo,hi,str)) = J`,
360 ((REWRITE_TAC[scs_J_v39;scs_v39;Misc_defs_and_lemmas.part6;Misc_defs_and_lemmas.drop3;FST]))
364 let scs_lo_v39_explicit = prove_by_refinement(
365 `!k d a b alpha beta J lo str. scs_lo_v39 (scs_v39 (k,d,a,alpha,beta,b,J,lo,hi,str)) = lo`,
368 ((REWRITE_TAC[scs_lo_v39;scs_v39;Misc_defs_and_lemmas.part7;Misc_defs_and_lemmas.drop3;FST]))
372 let scs_hi_v39_explicit = prove_by_refinement(
373 `!k d a b alpha beta J lo str. scs_hi_v39 (scs_v39 (k,d,a,alpha,beta,b,J,lo,hi,str)) = hi`,
376 ((REWRITE_TAC[scs_hi_v39;scs_v39;Misc_defs_and_lemmas.part8;Misc_defs_and_lemmas.drop3;FST]))
380 let scs_str_v39_explicit = prove_by_refinement(
381 `!k d a b alpha beta J lo str. scs_str_v39 (scs_v39 (k,d,a,alpha,beta,b,J,lo,hi,str)) = str`,
384 ((REWRITE_TAC[scs_str_v39;scs_v39;Misc_defs_and_lemmas.part7;Misc_defs_and_lemmas.drop3;FST]))
388 let scs_v39_explicit = end_itlist CONJ
389 [scs_k_v39_explicit;scs_d_v39_explicit;
390 scs_a_v39_explicit;scs_am_v39_explicit;
391 scs_b_v39_explicit;scs_bm_v39_explicit;
392 scs_J_v39_explicit;scs_lo_v39_explicit;
394 scs_str_v39_explicit];;
396 let periodic2 = new_definition `periodic2 (f:num->num->A) k = (!i j. f (i + k) j = f i j /\ f i (j + k) = f i j)`;;
398 (* This doesn't specify the form of : symmetric?
399 Let's make it symmetric periodic. is_ear_v... *)
401 let is_scs_v39 = new_definition `is_scs_v39 s = (
402 scs_d_v39 s < #0.9 /\
405 periodic (scs_lo_v39 s) (scs_k_v39 s) /\
406 periodic (scs_hi_v39 s) (scs_k_v39 s) /\
407 periodic (scs_str_v39 s) (scs_k_v39 s) /\
408 periodic (scs_str_v39 s) (scs_k_v39 s) /\
409 periodic2 (scs_a_v39 s) (scs_k_v39 s) /\
410 periodic2 (scs_am_v39 s) (scs_k_v39 s) /\
411 periodic2 (scs_bm_v39 s) (scs_k_v39 s) /\
412 periodic2 (scs_b_v39 s) (scs_k_v39 s) /\
413 periodic2 (scs_J_v39 s) (scs_k_v39 s) /\
414 (!i j. (scs_a_v39 s i j = scs_a_v39 s j i /\ scs_am_v39 s i j = scs_am_v39 s j i /\
415 scs_bm_v39 s i j = scs_bm_v39 s j i /\ scs_b_v39 s i j = scs_b_v39 s j i /\
416 scs_J_v39 s i j = scs_J_v39 s j i)) /\
417 (!i j. scs_a_v39 s i j <= scs_am_v39 s i j /\ scs_am_v39 s i j <= scs_bm_v39 s i j /\
418 scs_bm_v39 s i j <= scs_b_v39 s i j) /\
419 (!i. scs_a_v39 s i i = &0) /\
420 (!i j. (i < scs_k_v39 s) /\ (j < scs_k_v39 s) /\ ~(i = j) ==> &2 <= scs_a_v39 s i j) /\
421 (!i. (scs_k_v39 s = 3) ==> (scs_b_v39 s i (SUC i) < &4)) /\
422 (!i. (3 < scs_k_v39 s) ==> (scs_b_v39 s i (SUC i) <= cstab)) /\
423 (!i j. scs_J_v39 s i j ==> ((j MOD scs_k_v39 s = (SUC i) MOD scs_k_v39 s) \/
424 ((i MOD scs_k_v39 s = (SUC j) MOD scs_k_v39 s)))) /\
425 (!i j. scs_J_v39 s i j ==> scs_a_v39 s i j = sqrt8 /\ scs_b_v39 s i j = cstab) /\
426 CARD { i | i < scs_k_v39 s /\ (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i)) } + scs_k_v39 s <= 6)`;;
431 let unadorned_v39 = new_definition `unadorned_v39 s =
432 (scs_lo_v39 s = {} /\ scs_hi_v39 s = {} /\ scs_str_v39 s = {} /\ scs_a_v39 s = scs_am_v39 s /\ scs_b_v39 s = scs_bm_v39 s)`;;
434 let periodic_empty = prove_by_refinement(
438 REWRITE_TAC[Oxl_def.periodic];
439 BY(ASM_MESON_TAC[NOT_IN_EMPTY;IN])
443 let scs_unadorned = prove_by_refinement(
444 `!s. is_scs_v39 s ==>
445 is_scs_v39 (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_a_v39 s,scs_b_v39 s,scs_b_v39 s,scs_J_v39 s,{},{},{}))`,
448 REWRITE_TAC[is_scs_v39;scs_v39_explicit];
449 REPEAT WEAKER_STRIP_TAC;
450 ASM_REWRITE_TAC[arith `x <= x`;periodic_empty];
451 BY(ASM_MESON_TAC[arith `x <= y /\ y <= z ==> x <= z`])
455 let is_ear_v39 = new_definition `is_ear_v39 s <=>
459 scs_d_v39 s = #0.11 /\
460 (!i. scs_b_v39 s i i = &0) /\
461 (?i. {i | i < 3 /\ scs_J_v39 s i (SUC i)} = {i} /\
462 scs_a_v39 s i (SUC i) = sqrt8 /\ scs_b_v39 s i (SUC i) = cstab /\
463 (!j. j < 3 /\ ~(j = i) ==> scs_a_v39 s j (SUC j) = &2 /\ scs_b_v39 s j (SUC j) = &2 * h0))`;;
465 let BBs_v39 = new_definition `BBs_v39 s vv =
466 (let V = IMAGE vv (:num) in
467 let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
468 let FF = IMAGE (\i. (vv i,vv (SUC i))) (:num) in
469 (V SUBSET ball_annulus /\
470 periodic vv (scs_k_v39 s) /\
471 (!i j. scs_a_v39 s i j <= dist(vv i,vv j) /\ dist(vv i,vv j) <= scs_b_v39 s i j) /\
472 (scs_k_v39 s <= 3 \/ (convex_local_fan (V,E,FF)))))`;;
474 let dsv_v39 = new_definition `dsv_v39 s (vv:num->real^3) =
475 scs_d_v39 s + #0.1 * (if (is_ear_v39 s) then &1 else -- &1) *
476 sum {i | i < scs_k_v39 s /\ scs_J_v39 s i (SUC i)} (\i. cstab - dist(vv i,vv (SUC i)))`;;
478 let dsv_J_empty = prove_by_refinement(
479 `!s vv. scs_J_v39 s = (\i j. F) ==> dsv_v39 s vv = scs_d_v39 s`,
482 REPEAT WEAKER_STRIP_TAC;
483 ASM_REWRITE_TAC[dsv_v39;EMPTY_GSPEC;SUM_CLAUSES];
488 let taustar_v39 = new_definition `taustar_v39 s vv =
489 (let V = IMAGE vv (:num) in
490 let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
491 let FF = IMAGE (\i. (vv i,vv (SUC i))) (:num) in
492 (if (scs_k_v39 s <= 3) then tau3 (vv 0) (vv 1) (vv 2) - dsv_v39 s vv
493 else tau_fun V E FF - dsv_v39 s vv))`;;
495 let mk_unadorned_v39 = new_definition `mk_unadorned_v39 k d a b =
496 scs_v39 (k,d,a,a,b,b,(\i j. F),{},{},{})`;;
498 let cs_adj = new_definition `cs_adj k a1 a2 i j =
499 (if (i MOD k = j MOD k) then &0
500 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2))`;;
502 let psort = new_definition `psort k (u:num#num) =
503 (let i = FST u MOD k in
504 let j = SND u MOD k in
505 if (i <= j) then (i,j) else (j,i))`;;
508 let ASSOCD = new_definition` ASSOCD (a:A) hs (d:D) =
509 if hs = [] then d else ASSOC a hs`;;
512 let ASSOCD_v39 = new_recursive_definition list_RECURSION
513 `ASSOCD_v39 (a:A) [] (d:D) = d /\
514 ASSOCD_v39 a (CONS h t) d = if (a = FST h) then SND h else ASSOCD_v39 a t d`;;
516 let funlist_v39 = new_definition `funlist_v39 data d k i j =
517 (let data' = MAP (\ (u, d). (psort k u,d)) data in
518 if (i MOD k = j MOD k) then (&0)
519 else ASSOCD_v39 (psort k (i,j)) data' d)`;;
521 let funlistA_v39 = new_definition `funlistA_v39 data (diag:A) default k i j =
522 (let data' = MAP (\ (u, d). (psort k u,d)) data in
523 if (i MOD k = j MOD k) then diag
524 else ASSOCD_v39 (psort k (i,j)) data' default)`;;
526 let override = new_definition `override a k u d i j =
527 if psort k u = psort k (i,j) then (d:A) else a i j`;;
529 (* constant 0.467 corrected on 2013-06-03. *)
531 let s_init_list_v39 = new_definition `s_init_list_v39 =
533 let a_pro = (\k p a1 a2 i j.
534 (if (i MOD k = j MOD k) then &0
535 else (if {(i MOD k),(j MOD k)}={0,1} then p
536 else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
537 [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd); // scs_6I1
538 mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd); // scs_5I1
539 mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd); // scs_4I1
540 mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd); // scs_3I1
541 mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (sqrt8)) (cs_adj 5 (&2 * h0) upperbd); // scs_5I2
542 mk_unadorned_v39 4 (#0.467) (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd); // scs_4I2
543 mk_unadorned_v39 5 (#0.616) (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd); // scs_5I3
544 mk_unadorned_v39 4 (#0.477) (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd) // scs_4I3
547 let LENGTH_s_init_list = prove_by_refinement(
548 `LENGTH s_init_list_v39 = 8`,
551 REWRITE_TAC[s_init_list_v39;LET_DEF;LET_END_DEF;LENGTH];
559 `mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (cstab)) (cs_adj 6 (&2) (&6))`;;
562 `mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (cstab)) (cs_adj 5 (&2) (&6))`;;
564 let scs_4T1 = (* terminal_adhoc_quad_5691615370 = *)
565 `mk_unadorned_v39 4 #0.467 (cs_adj 4 (&2) (&3))
566 (cs_adj 4 (&2) (&6))`;;
568 let scs_4T2 = (* terminal_adhoc_quad_9563139965B = *)
569 `mk_unadorned_v39 4 (#0.467) (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2*h0) (&3))`;;
571 let scs_4T3 = (* terminal_adhoc_quad_4680581274 = *)
572 `mk_unadorned_v39 4 (#0.513)
573 (funlist_v39 [(0,1),cstab ; (0,2),cstab ; (1,3),cstab ] (&2) 4)
574 (funlist_v39 [(0,1),cstab ; (0,2),(&6) ; (1,3),(&6) ] (&2) 4)`;;
576 (* deprecated 2013-06-17
577 let terminal_adhoc_quad_7697147739 =
578 `mk_unadorned_v39 4 (#0.616 - #0.11) (funlist_v39 [(0,1),sqrt8 ; (0,2),cstab ; (1,3),cstab ] (&2) 4)
579 (funlist_v39 [(0,1),sqrt8 ; (0,2),(&6) ; (1,3),(&6) ] (&2) 4)`;;
583 `mk_unadorned_v39 4 (#0.477)
584 (funlist_v39 [(0,1),(&2 * h0);(0,2),sqrt8;(1,3),sqrt8] (&2) 4)
585 (funlist_v39 [(0,1),sqrt8 ;(0,2),(&6); (1,3),cstab] (&2 * h0) 4)`;;
588 `mk_unadorned_v39 4 (#0.513)
589 (funlist_v39 [(0,1),(&2 * h0);(0,2),cstab;(1,3),cstab] (&2) 4)
590 (funlist_v39 [(0,1),cstab ;(0,2),(&6); (1,3),cstab] (&2 * h0) 4)`;;
592 (* deprecated 2013-06-17
593 let terminal_tri_7720405539 = `mk_unadorned_v39
595 (#0.5518 / #2.0 - #0.2)
596 (funlist_v39 [(0,1),cstab; (0,2), (&2 * h0); (1,2),(&2)] (&2) 3)
597 (funlist_v39 [(0,1),#3.41; (0,2), (&2 * h0); (1,2),(&2)] (&2) 3)`;;
599 let terminal_tri_2739661360 = `mk_unadorned_v39
601 (#0.5518 / #2.0 + #0.2)
602 (funlist_v39 [(0,1),cstab; (0,2),cstab; (1,2),(&2)] (&2) 3)
603 (funlist_v39 [(0,1), #3.41; (0,2),cstab; (1,2),(&2)] (&2) 3)`;;
605 let terminal_tri_4922521904 = `mk_unadorned_v39
608 (funlist_v39 [(0,1),cstab; (0,2),(&2)*h0; (1,2),(&2)] (&2) 3)
609 (funlist_v39 [(0,1),#3.339; (0,2),(&2)*h0; (1,2),(&2)] (&2) 3)`;;
611 let ear_stab = `mk_unadorned_v39
613 // (#0.11 + #0.1 *(cstab - sqrt8)) corrected 2013-4-20, see check_completeness djz.
615 (funlist_v39 [(0,2),cstab] (&2) 3)
616 (funlist_v39 [(0,2),cstab] (&2*h0) 3)`;;
618 let terminal_ear_3603097872 = ear_cs;;
620 let terminal_tri_7881254908 =
621 `mk_unadorned_v39 3 (#0.696 - #2.0 * #0.11)
622 (funlist_v39 [(0,1),sqrt8;(1,2),sqrt8] (&2*h0) 3)
623 (funlist_v39 [(0,1),cstab;(1,2),cstab] (&2*h0) 3)`;;
628 let scs_3T1 = (* ear_jnull = *)
630 funlist_v39 [(0,1),sqrt8] (&2) 3,
631 funlist_v39 [(0,1),sqrt8] (&2) 3,
632 funlist_v39 [(0,1),cstab] (&2*h0) 3,
633 funlist_v39 [(0,1),cstab] ((&2)*h0) 3,
634 (\i j. F),{},{},{})`;;
636 let scs_3T2 = (* terminal_std_tri_OMKYNLT_3336871894 = *)
640 (funlist_v39 [] (&2) 3)
641 (funlist_v39 [] (&2) 3)`;;
643 (* 3 new additions 2013-06-04 3T3 3T4 3T5 *)
645 let scs_3T3 = (* terminal_tri_4010906068 = *)
648 (funlist_v39 [] (&2*h0) 3)
649 (funlist_v39 [] (cstab) 3)`;;
651 let scs_3T4 = (* terminal_tri_6833979866 = *)
654 (funlist_v39 [(0,1),(&2)] (&2*h0) 3)
655 (funlist_v39 [(0,1),(&2 * h0)] (cstab) 3)`;;
657 let scs_3T5 = (* terminal_tri_5541487347 = *)
660 (funlist_v39 [(0,1),(&2 * h0)] (&2) 3)
661 (funlist_v39 [(0,1),(sqrt8)] (&2 * h0) 3)`;;
663 let scs_3T6 = (* terminal_tri_5026777310a = *)
666 (funlist_v39 [(0,1),sqrt8;(1,2),sqrt8] (&2) 3)
667 (funlist_v39 [(0,1),cstab;(1,2),cstab] (&2*h0) 3)`;;
669 let scs_3T7 = (* terminal_tri_9269152105 = 2468307358 *)
670 `mk_unadorned_v39 3 (#0.2565)
671 (funlist_v39 [(0,1),cstab; (0,2),cstab; (1,2),(&2)] (&2) 3)
672 (funlist_v39 [(0,1),#3.62; (0,2),cstab; (1,2),(&2)] (&2) 3)`;;
694 (* terminal_adhoc_quad_7697147739; *)
696 (* upper echelon cases *)
698 terminal_tri_7720405539;
699 terminal_tri_2739661360;
701 terminal_tri_4922521904;
705 terminal_ear_3603097872;
707 terminal_tri_5405130650;
711 terminal_tri_5026777310a;
712 terminal_tri_7881254908;
713 terminal_std_tri_OMKYNLT_3336871894;
714 terminal_tri_4010906068;
715 terminal_tri_6833979866;
716 terminal_tri_5541487347;
722 (* nonterminal cases *)
726 funlist_v39 [(0,1),sqrt8] (&2) 3,
727 funlist_v39 [(0,1),sqrt8] (&2) 3,
728 funlist_v39 [(0,1),cstab] ((&2)*h0) 3,
729 funlist_v39 [(0,1),cstab] (&2*h0) 3,
730 funlistA_v39 [(0,1),T] F F 3,{},{},{})`;;
732 let terminal_tri_5405130650 = `scs_v39(
735 funlist_v39 [(0,1),sqrt8;(0,2),(&2*h0);(1,2),(&2)] (&2) 3,
736 funlist_v39 [(0,1),sqrt8;(0,2),(&2*h0);(1,2),(&2)] (&2) 3,
737 funlist_v39 [(0,1),cstab;(0,2),sqrt8;(1,2),(&2*h0)] (&2*h0) 3,
738 funlist_v39 [(0,1),cstab;(0,2),sqrt8;(1,2),(&2*h0)] (&2*h0) 3,
739 funlistA_v39 [(0,1),T] F F 3,{},{},{})`;;
742 let scs_terminal_v39 = new_definition (mk_eq (`scs_terminal_v39:(scs_v39)list`,(mk_flist terminal_cs)));;
750 let ZITHLQN_concl = `(!s vv. MEM s s_init_list_v39 /\ vv IN
752 &0 <= taustar_v39 s vv) ==> JEJTVGB_assume_v39`;;
755 let ZITHLQN = prove_by_refinement(
756 `(!s vv. s IN set_of_list s_init_list_v39 /\ vv IN BBs_v39 s ==> &0 <= taustar_v39 s vv) ==> JEJTVGB_assume_v39`,
759 rt[s_init_list_v39;set_of_list;JEJTVGB_assume_v39]
763 rule (rr [taustar_v39])
764 typ `CARD V = 3 \/ CARD V = 4 \/ CARD V = 5 \/ CARD V = 6` (C gthen assume)
765 repeat (fxast `CARD` mp) then ARITH_TAC
770 let BBprime_v39 = new_definition `BBprime_v39 s vv = (BBs_v39 s vv /\
771 (!ww. BBs_v39 s ww ==> taustar_v39 s vv <= taustar_v39 s ww) /\ taustar_v39 s vv < &0)`;;
773 let BBindex_v39 = new_definition `BBindex_v39 s (vv:num->real^3) =
774 CARD { i | i < scs_k_v39 s /\ scs_a_v39 s i (SUC i) = dist(vv i, vv (SUC i)) }`;;
776 let BBindex_min_v39 = new_definition `BBindex_min_v39 s =
777 min_num (IMAGE (BBindex_v39 s) (BBprime_v39 s))`;;
779 let BBprime2_v39 = new_definition `BBprime2_v39 s vv <=>
780 BBprime_v39 s vv /\ BBindex_v39 s vv = BBindex_min_v39 s`;;
782 let MMs_v39 = new_definition `MMs_v39 s vv <=>
784 (!i. scs_str_v39 s i ==> azim (vec 0) (vv i) (vv (SUC i)) (vv (i + (scs_k_v39 s - 1)) ) = pi) /\
785 (!i. scs_lo_v39 s i ==> norm (vv i) = &2) /\
786 (!i. scs_hi_v39 s i ==> norm (vv i) = &2 * h0) /\
787 (!i j. scs_am_v39 s i j <= dist(vv i,vv j)) /\
788 (!i j. dist(vv i,vv j) <= scs_bm_v39 s i j)`;;
790 let unadorned_MMs_concl = `!s.
791 unadorned_v39 s ==> (MMs_v39 s = BBprime2_v39 s)`;;
793 let XWITCCN_concl = `!s vv. MEM s s_init_list_v39 /\ vv IN BBs_v39 s /\
794 taustar_v39 s vv < &0 ==> ~(BBprime_v39 s = {})`;;
796 let XWITCCN2_concl = `!s vv. MEM s s_init_list_v39 /\ vv IN BBs_v39 s /\
797 taustar_v39 s vv < &0 ==> ~(BBprime2_v39 s = {})`;;
799 let AYQJTMD_concl = `!s vv. MEM s s_init_list_v39 /\ vv IN BBs_v39 s /\
800 taustar_v39 s vv < &0 ==> ~(MMs_v39 s = {})`;;
802 let EAPGLE_concl = `(!s. MEM s s_init_list_v39 ==> MMs_v39 s = {}) ==> JEJTVGB_assume_v39`;;
804 let JKQEWGV1_concl = `!s vv. is_scs_v39 s /\ BBs_v39 s vv /\ taustar_v39 s vv < &0 /\
806 (sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
807 (IMAGE (\i. (vv i,vv (SUC i))) (:num)) < pi)`;;
809 let JKQEWGV2_concl = `!s vv. is_scs_v39 s /\ BBs_v39 s vv /\ taustar_v39 s vv < &0 /\
812 let V = IMAGE vv (:num) in
813 let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
816 let JKQEWGV3_concl = `!s vv v w.
817 (let V = IMAGE vv (:num) in
818 let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
819 let FF = IMAGE (\i. (vv i,vv (SUC i))) (:num) in
820 (is_scs_v39 s /\ BBs_v39 s vv /\ taustar_v39 s vv < &0 /\ lunar (v,w) V E /\
822 (interior_angle1 (vec 0) FF v < pi / &2 )))`;;
824 let HFNXPZA_concl = `!s vv.
825 is_scs_v39 s /\ BBs_v39 s vv /\ taustar_v39 s vv < &0 /\ scs_k_v39 s = 3 ==>
826 dihV (vec 0) (vv 0) (vv 1) (vv 2) +
827 dihV (vec 0) (vv 1) (vv 2) (vv 3) +
828 dihV (vec 0) (vv 2) (vv 3) (vv 1) < &2 * pi`;;
830 let restriction_typ1_v39 = new_definition `restriction_typ1_v39 s =
831 (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,scs_bm_v39 s,scs_bm_v39 s,scs_J_v39 s,scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s))`;;
833 let restriction_typ2_v39 = new_definition `restriction_typ2_v39 s =
834 (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_am_v39 s,scs_am_v39 s,
835 scs_am_v39 s,scs_am_v39 s,scs_J_v39 s,scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s))`;;
838 let restriction_typ3_v39 = new_definition `restriction_typ3_v39 s i j a b =
839 ((a <= scs_bm_v39 s i j /\ scs_am_v39 s i j <= b),
840 (let k = scs_k_v39 s in
843 let f = (\i'' j''. { i'' MOD k, j'' MOD k } = {i',j'}) in
844 let a1 = (\i'' j''. if f i'' j'' then a else scs_a_v39 s i j) in
845 let b1 = (\i'' j''. if f i'' j'' then b else scs_b_v39 s i j) in
846 let am = (\i'' j''. if f i'' j'' then max a (scs_am_v39 s i j) else scs_am_v39 s i j) in
847 let bm = (\i'' j''. if f i'' j'' then min b (scs_bm_v39 s i j) else scs_bm_v39 s i j)in
848 (scs_v39 (scs_k_v39 s,scs_d_v39 s,a1,am,
849 bm,b1,scs_J_v39 s,scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s))))`;;
851 let subdivision_v39 = new_definition `subdivision_v39 c i j s =
852 (let precond = ((scs_a_v39 s i j <= c) /\ c <= scs_b_v39 s i j) in
853 let r1 = restriction_typ3_v39 s i j (scs_a_v39 s i j) c in
854 let r2 = restriction_typ3_v39 s i j c (scs_b_v39 s i j) in
855 let cons_if = (\b r rs. if b then CONS r rs else rs) in
856 if precond then (cons_if (FST r1) (SND r1) (cons_if (FST r2) (SND r2) [])) else [])`;;
859 let restriction_cs1_v39 = new_definition `restriction_cs1_v39 s p q c =
860 (let b1 = override (scs_b_v39 s) (scs_k_v39 s) (p,q) c in
861 let bm = if (c < scs_bm_v39 s p q) then
862 override (scs_bm_v39 s) (scs_k_v39 s) (p,q) c else scs_bm_v39 s in
863 (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,
864 bm,b1,scs_J_v39 s,scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s)))`;;
866 let restriction_cs2_v39 = new_definition `restriction_cs2_v39 s p q c =
867 (let a1 = override (scs_a_v39 s) (scs_k_v39 s) (p,q) c in
868 let am = if (scs_am_v39 s p q < c) then
869 override (scs_am_v39 s) (scs_k_v39 s) (p,q) c else scs_am_v39 s in
870 (scs_v39 (scs_k_v39 s,scs_d_v39 s,a1,am,scs_bm_v39 s,scs_b_v39 s,
871 scs_J_v39 s,scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s)))`;;
873 let subdiv_v39 = new_definition `subdiv_v39 s p q c =
874 (if (c <= scs_a_v39 s p q) then [s]
875 else (if (c <= scs_am_v39 s p q) then [restriction_cs2_v39 s p q c]
876 else (if (c < scs_bm_v39 s p q) then [restriction_cs1_v39 s p q c;restriction_cs2_v39 s p q c]
877 else (if (c < scs_b_v39 s p q) then [restriction_cs1_v39 s p q c]
880 let transfer_v39 = new_definition `transfer_v39 s s' <=>
881 (is_ear_v39 s ==> (s = s')) /\
883 (unadorned_v39 s') /\
884 scs_d_v39 s <= scs_d_v39 s' /\
885 (scs_k_v39 s' = scs_k_v39 s) /\
886 (!i j. scs_a_v39 s' i j <= scs_a_v39 s i j) /\
887 (!i j. scs_b_v39 s i j <= scs_b_v39 s' i j) /\
888 (!i j. scs_J_v39 s' i j ==> scs_J_v39 s i j)
891 let scs_prop_equ_v39 = new_definition `scs_prop_equ_v39 s i =
892 (let shift1 = \ (f:num->bool) j. f (i + j) in
893 let shift2 = \ (f:num->num-> real) j j'. (f (i + j) (i + j')) in
894 let shift2b = \ (f:num->num-> bool) j j'. (f (i + j) (i + j')) in
895 (scs_v39 (scs_k_v39 s,scs_d_v39 s,shift2 (scs_a_v39 s),shift2 (scs_am_v39 s),shift2 (scs_bm_v39 s),
896 shift2 (scs_b_v39 s), shift2b (scs_J_v39 s), shift1 (scs_lo_v39 s) ,
897 shift1 (scs_hi_v39 s), shift1 (scs_str_v39 s))))`;;
899 let scs_opp_v39 = new_definition `scs_opp_v39 s =
900 (let k = scs_k_v39 s in
901 scs_v39 (scs_k_v39 s,scs_d_v39 s, peropp2 (scs_a_v39 s) k, peropp2 (scs_am_v39 s) k,
902 peropp2 (scs_bm_v39 s) k,peropp2 (scs_b_v39 s) k,
903 peropp2 (scs_J_v39 s) k, peropp (scs_lo_v39 s) k,
904 peropp(scs_hi_v39 s) k, peropp (scs_str_v39 s) k))`;;
906 (* 0--(p-1) slice: *)
909 let torsor_slice_v39 = new_definition `torsor_slice_v39 s p =
911 let mod1 = \ (f:num->bool) j. f (j MOD p) in
912 let mod2 = \ (f:num->num->real) j j'. f (j MOD p) (j' MOD p) in
913 let mod2b = \ (f:num->num->bool) j j'. f (j MOD p) (j' MOD p) in
914 (scs_v39 (scs_k_v39 s,scs_d_v39 s,mod2 (scs_a_v39 s),mod2 (scs_am_v39 s),mod2 (scs_bm_v39 s),
915 mod2 (scs_b_v39 s), mod2b (scs_J_v39 s), mod1 (scs_lo_v39 s) , mod1 (scs_str_v39 s))))`;;
918 let scs_diag = new_definition `scs_diag k i j <=>
919 ~(i MOD k = j MOD k) /\
920 ~(SUC i MOD k = j MOD k) /\
921 ~(i MOD k = SUC j MOD k)`;;
924 let scs_half_slice_v39 = new_definition `scs_half_slice_v39 s p q d' mkj =
925 (let p' = p MOD (scs_k_v39 s) in
926 let k' = (q + 1 + (scs_k_v39 s - p')) MOD (scs_k_v39 s) in
927 let mod2 = \ (f:num->num->real) j j'. f ((j MOD k')+ p') ((j' MOD k') + p') in
928 let mod2b = \ (f:num->num->bool) j j'. f ((j MOD k')+ p') ((j' MOD k') + p') in
929 let a1 = \ i'' j''. if {i'' MOD k',j'' MOD k'} = {0,k'-1}
930 then scs_am_v39 s p q else mod2 (scs_a_v39 s) i'' j'' in
931 let b1 = \ i'' j''. if {i'' MOD k',j'' MOD k'} = {0,k'-1}
932 then scs_bm_v39 s p q else mod2 (scs_b_v39 s) i'' j'' in
933 let J = \ i'' j''. if {i'' MOD k',j'' MOD k'} = {0,k'-1} then mkj else mod2b (scs_J_v39 s) i'' j'' in
934 scs_v39 (k',d',a1,a1,b1,b1,J,{},{},{}))`;;
936 let scs_slice_v39 = new_definition `scs_slice_v39 s p q d' d'' mkj =
937 (scs_half_slice_v39 s p q d' mkj,
938 scs_half_slice_v39 s q p d'' mkj)`;;
940 let is_scs_slice_v39 = new_definition `is_scs_slice_v39 s s' s'' p q <=>
941 (let d' = scs_d_v39 s' in
942 let d'' = scs_d_v39 s'' in
943 let mkj = scs_J_v39 s' 0 (scs_k_v39 s' - 1) in
944 (((s',s'') = scs_slice_v39 s p q d' d'' mkj) /\
947 scs_d_v39 s <= d' + d'' /\
948 scs_bm_v39 s p q < &4 /\
949 ((scs_k_v39 s = 4) \/ scs_bm_v39 s p q <= cstab) /\
950 (mkj ==> (is_ear_v39 s' \/ is_ear_v39 s''))))`;;
952 let scs_arrow_v39 = new_definition `scs_arrow_v39 S1 S2 <=>
953 (!s. s IN S2 ==> is_scs_v39 s) /\
954 ((!s. s IN S1 ==> MMs_v39 s = {}) \/
955 (?s. s IN S2 /\ ~(MMs_v39 s = {})))`;;
957 (* added definitions 2013-06-17 *)
959 let xrr = new_definition `xrr y1 y2 y6 = &8 * (&1 - (y1 * y1 + y2*y2 - y6*y6)/(&2* y1 * y2))`;;
961 let scs_basic3 = new_definition `scs_basic3 d a01 b01 a02 b02 a12 b12 =
962 (let a = funlist_v39 [(0,1),a01;(0,2),a02;(1,2),a12] (&0) 3 in
963 let b = funlist_v39 [(0,1),b01;(0,2),b02;(1,2),b12] (&0) 3 in
964 mk_unadorned_v39 3 d a b)`;;
966 let scs_basic4 = new_definition `scs_basic4 d a01 b01 a02 b02 a03 b03 a12 b12 a13 b13 a23 b23 =
967 (let a = funlist_v39 [(0,1),a01;(0,2),a02;(0,3),a03;(1,2),a12;(1,3),a13;(2,3),a23] (&0) 4 in
968 let b = funlist_v39 [(0,1),b01;(0,2),b02;(0,3),b03;(1,2),b12;(1,3),b13;(2,3),b23] (&0) 4 in
969 mk_unadorned_v39 4 d a b)`;;
971 (* renamed from scs_is_basic *)
974 let scs_generic = new_definition `scs_generic v <=>
975 generic (IMAGE v (:num))
976 (IMAGE (\i. {v i, v (SUC i)}) (:num))`;;
978 let scs_is_str = new_definition `scs_is_str s vv i <=> (
979 azim (vec 0) (vv i) (vv (SUC i)) (vv (i + (scs_k_v39 s - 1)) ) = pi)`;;
981 let scs_stab_diag_v39 = new_definition `scs_stab_diag_v39 s i j =
983 let k = scs_k_v39 s in
984 let b' = (\i' j'. if psort k (i,j) = psort k (i',j') then cstab else scs_b_v39 s i' j') in
985 (mk_unadorned_v39 k (scs_d_v39 s) (scs_a_v39 s) b'))`;;
987 let scs_basic = new_definition `scs_basic_v39 s <=>
988 unadorned_v39 s /\ (!i j. scs_J_v39 s i j = F)`;;
990 let scs_inj = prove_by_refinement(
991 `!s s'. scs_basic_v39 s /\ scs_basic_v39 s' /\
992 scs_d_v39 s = scs_d_v39 s' /\
993 scs_k_v39 s = scs_k_v39 s' /\
994 (scs_a_v39 s = scs_a_v39 s') /\
995 (scs_b_v39 s = scs_b_v39 s')
1000 REPEAT WEAKER_STRIP_TAC;
1001 REPEAT (FIRST_X_ASSUM_ST `scs_basic_v39` MP_TAC);
1002 REWRITE_TAC[scs_basic;unadorned_v39];
1003 ONCE_REWRITE_TAC[EQ_SYM_EQ];
1004 REWRITE_TAC[SET_RULE `{} = a <=> a = {}`];
1005 REPEAT WEAKER_STRIP_TAC;
1006 ONCE_REWRITE_TAC[GSYM scs_v39];
1008 ASM_REWRITE_TAC[scs_components];
1009 TYPIFY `scs_J_v39 s = scs_J_v39 s'` (C SUBGOAL_THEN SUBST1_TAC);
1010 BY(ASM_REWRITE_TAC[FUN_EQ_THM]);
1016 (* deprecate: only used in Ocbicby.basic_examples: *)
1019 let is_basic = new_definition `is_basic s <=>
1020 is_scs_v39 s /\ unadorned_v39 s /\ (!i j. scs_J_v39 s i j = F)`;;
1025 let mk_simplex = new_definition `mk_simplex v0 v1 v2 x1 x2 x3 x4 x5 x6 =
1026 (let uinv = &1 / ups_x x1 x2 x6 in
1027 let d = delta_x x1 x2 x3 x4 x5 x6 in
1028 let d5 = delta_x5 x1 x2 x3 x4 x5 x6 in
1029 let d6 = delta_x4 x1 x2 x3 x4 x5 x6 in
1030 let vcross = (v1 - v0) cross (v2 - v0) in
1031 v0 + uinv % ((&2 * sqrt d) % vcross + d5 % (v1 - v0) + d6 % (v2 - v0)))`;;
1034 let mk_simplex1 = new_definition `mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6 =
1035 (let uinv = &1 / ups_x x1 x2 x6 in
1036 let d = delta_x x1 x2 x3 x4 x5 x6 in
1037 let d5 = delta_x5 x1 x2 x3 x4 x5 x6 in
1038 let d4 = delta_x4 x1 x2 x3 x4 x5 x6 in
1039 let vcross = (v1 - v0) cross (v2 - v0) in
1040 v0 + uinv % ((&2 * sqrt d) % vcross + d5 % (v1 - v0) + d4 % (v2 - v0)))`;;
1042 let mk_planar2 = new_definition `mk_planar2 v0 v1 v2 x1 x2 x3 x5 x6 s =
1043 (let vcross = (v1 - v0) cross ((v1 - v0) cross (v2 - v0)) in
1044 v0 + ((x1 + x3 - x5) / (&2 * x1)) % (v1 - v0) +
1045 ((s / x1) * sqrt (ups_x x1 x3 x5 / ups_x x1 x2 x6)) % vcross)`;;
1047 let scs_M = new_definition `scs_M s =
1048 { i | i < scs_k_v39 s /\ (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i)) }`;;
1050 let scs_6I1 = new_definition `scs_6I1 =
1051 mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) (&6))`;;
1053 let scs_5I1 = new_definition `scs_5I1 =
1054 mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) (&6))`;;
1056 let scs_4I1 = new_definition `scs_4I1 =
1057 mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) (&6))
1060 let scs_3I1 = new_definition `scs_3I1 =
1061 mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) (&6))
1064 let scs_5I2 = new_definition `scs_5I2 =
1065 mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (sqrt8)) (cs_adj 5 (&2 * h0) (&6))
1068 let scs_4I2 = new_definition `scs_4I2 =
1069 mk_unadorned_v39 4 (#0.467) (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) (&6))
1072 let scs_5I3 = new_definition `scs_5I3 =
1073 mk_unadorned_v39 5 (#0.616)
1074 (funlist_v39 [(0,1),(&2*h0);(0,2),(&2*h0);(0,3),(&2*h0);(1,3),(&2*h0);(1,4),(&2*h0);(2,4),(&2*h0)] (&2) 5)
1075 (funlist_v39 [(0,1),sqrt8;(0,2),(&6);(0,3),(&6);(1,3),(&6);(1,4),(&6);(2,4),(&6)] (&2*h0) 5)`;;
1077 let scs_4I3 = new_definition `scs_4I3 =
1078 mk_unadorned_v39 4 (#0.477)
1079 (funlist_v39 [(0,1),(&2*h0);(0,2),(sqrt8);(1,3),(sqrt8)] (&2) 4)
1080 (funlist_v39 [(0,1),sqrt8;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
1082 (* terminal cases *)
1084 let scs_6T1 = new_definition
1085 `scs_6T1 = mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (cstab)) (cs_adj 6 (&2) (&6))`;;
1087 let scs_5T1 = new_definition
1088 `scs_5T1 = mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (cstab)) (cs_adj 5 (&2) (&6))`;;
1090 let scs_4T1 = (* terminal_adhoc_quad_5691615370 = *) new_definition
1091 `scs_4T1 = mk_unadorned_v39 4 #0.467 (cs_adj 4 (&2) (&3))
1092 (cs_adj 4 (&2) (&6))`;;
1094 let scs_4T2 = (* terminal_adhoc_quad_9563139965B = *) new_definition
1095 `scs_4T2 = mk_unadorned_v39 4 (#0.467) (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2*h0) (&3))`;;
1097 let scs_4T3 = (* terminal_adhoc_quad_4680581274 = *) new_definition
1098 `scs_4T3 = mk_unadorned_v39 4 (#0.513)
1099 (funlist_v39 [(0,1),cstab ; (0,2),cstab ; (1,3),cstab ] (&2) 4)
1100 (funlist_v39 [(0,1),cstab ; (0,2),(&6) ; (1,3),(&6) ] (&2) 4)`;;
1102 let scs_4T4 = new_definition
1103 `scs_4T4 = mk_unadorned_v39 4 (#0.477)
1104 (funlist_v39 [(0,1),(&2 * h0);(0,2),sqrt8;(1,3),sqrt8] (&2) 4)
1105 (funlist_v39 [(0,1),sqrt8 ;(0,2),(&6); (1,3),cstab] (&2 * h0) 4)`;;
1107 let scs_4T5 = new_definition
1108 `scs_4T5 = mk_unadorned_v39 4 (#0.513)
1109 (funlist_v39 [(0,1),(&2 * h0);(0,2),cstab;(1,3),cstab] (&2) 4)
1110 (funlist_v39 [(0,1),cstab ;(0,2),(&6); (1,3),cstab] (&2 * h0) 4)`;;
1112 let scs_3T1_PRELIM = (* ear_jnull = *) new_definition
1113 `scs_3T1 = scs_v39 (3, #0.11,
1114 funlist_v39 [(0,1),sqrt8] (&2) 3,
1115 funlist_v39 [(0,1),sqrt8] (&2) 3,
1116 funlist_v39 [(0,1),cstab] (&2*h0) 3,
1117 funlist_v39 [(0,1),cstab] ((&2)*h0) 3,
1118 (\i j. F),{},{},{})`;;
1120 let scs_3T1 = prove_by_refinement(
1121 `scs_3T1 = mk_unadorned_v39 3 (#0.11)
1122 (funlist_v39 [(0,1),(sqrt8)] (&2) 3)
1123 (funlist_v39 [(0,1),(cstab)] (&2 * h0) 3)`,
1126 BY(REWRITE_TAC[mk_unadorned_v39;scs_3T1_PRELIM]);
1130 let scs_3T2 = (* terminal_std_tri_OMKYNLT_3336871894 = *) new_definition
1131 `scs_3T2 = mk_unadorned_v39
1134 (funlist_v39 [] (&2) 3)
1135 (funlist_v39 [] (&2) 3)`;;
1137 let scs_3T3 = (* terminal_tri_4010906068 = *) new_definition
1138 `scs_3T3 = mk_unadorned_v39 3
1140 (funlist_v39 [] (&2*h0) 3)
1141 (funlist_v39 [] (cstab) 3)`;;
1143 let scs_3T4 = (* terminal_tri_6833979866 = *) new_definition
1144 `scs_3T4 = mk_unadorned_v39 3
1146 (funlist_v39 [(0,1),(&2)] (&2*h0) 3)
1147 (funlist_v39 [(0,1),(&2 * h0)] (cstab) 3)`;;
1149 let scs_3T5 = (* terminal_tri_5541487347 = *) new_definition
1150 `scs_3T5 = mk_unadorned_v39 3
1152 (funlist_v39 [(0,1),(&2 * h0)] (&2) 3)
1153 (funlist_v39 [(0,1),(sqrt8)] (&2 * h0) 3)`;;
1155 let scs_3T6 = (* terminal_tri_5026777310a = *) new_definition
1156 `scs_3T6' = mk_unadorned_v39 3
1158 (funlist_v39 [(0,1),sqrt8;(1,2),sqrt8] (&2) 3)
1159 (funlist_v39 [(0,1),cstab;(1,2),cstab] (&2*h0) 3)`;;
1161 let scs_3T7 = (* terminal_tri_9269152105 = 2468307358 *) new_definition
1162 `scs_3T7 = mk_unadorned_v39 3 (#0.2565)
1163 (funlist_v39 [(0,1),cstab; (0,2),cstab; (1,2),(&2)] (&2) 3)
1164 (funlist_v39 [(0,1),#3.62; (0,2),cstab; (1,2),(&2)] (&2) 3)`;;
1166 let scs_6M1 = new_definition `scs_6M1 =
1167 mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (cstab)) (cs_adj 6 (&2 * h0) (&6))`;;
1169 let scs_5M1 = new_definition
1170 `scs_5M1 = mk_unadorned_v39 5 (#0.616)
1171 (funlist_v39 [(0,1),(&2*h0);(0,2),(&2*h0);(0,3),(&2*h0);(1,3),(&2*h0);(1,4),(&2*h0);(2,4),(&2*h0)] (&2) 5)
1172 (funlist_v39 [(0,1),cstab; (0,2),(&6); (0,3),(&6); (1,3),(&6); (1,4),(&6); (2,4),(&6)] (&2*h0) 5)`;;
1174 let scs_5M2 = new_definition
1175 `scs_5M2 = mk_unadorned_v39 5 (#0.616)
1176 (funlist_v39 [(0,1),(&2);(0,2),(cstab);(0,3),(cstab);(1,3),(cstab);(1,4),(cstab);(2,4),(cstab)] (&2) 5)
1177 (funlist_v39 [(0,1),cstab;(0,2),(&6); (0,3),(&6); (1,3),(&6); (1,4),(&6); (2,4),(&6)] (&2*h0) 5)`;;
1179 let scs_4M1 = new_definition
1180 `scs_4M1 = mk_unadorned_v39 4 (#0.3401)
1181 (funlist_v39 [(0,1),(&2*h0);(0,2),(&2*h0);(1,3),(&2*h0)] (&2) 4)
1182 (funlist_v39 [(0,1),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
1184 let scs_4M2 = new_definition
1185 `scs_4M2 = mk_unadorned_v39 4 (#0.3789)
1186 (funlist_v39 [(0,1),(&2*h0);(0,2),(&2*h0);(1,3),(&2*h0)] (&2) 4)
1187 (funlist_v39 [(0,1),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
1190 let scs_4M3' = new_definition
1191 `scs_4M3' = mk_unadorned_v39 4 (#0.503)
1192 (funlist_v39 [(0,1),(sqrt8);(0,2),(sqrt8);(1,3),(sqrt8)] (&2) 4)
1193 (funlist_v39 [(0,1),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
1195 let scs_4M4 = new_definition
1196 `scs_4M4 = mk_unadorned_v39 4 (#0.503)
1197 (funlist_v39 [(0,1),(&2*h0);(1,2),(&2*h0);(0,2),(&2*h0);(1,3),(&2*h0)] (&2) 4)
1198 (funlist_v39 [(0,1),cstab;(1,2),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
1200 let scs_4M5 = new_definition
1201 `scs_4M5 = mk_unadorned_v39 4 (#0.503)
1202 (funlist_v39 [(0,1),(&2*h0);(2,3),(&2*h0);(0,2),(&2*h0);(1,3),(&2*h0)] (&2) 4)
1203 (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
1205 let scs_4M6 = new_definition
1206 `scs_4M6 = mk_unadorned_v39 4 (#0.503)
1207 (funlist_v39 [(0,1),(&2*h0);(0,2),(cstab);(1,3),(cstab)] (&2) 4)
1208 (funlist_v39 [(0,1),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
1211 let scs_4M3 = new_definition
1212 `scs_4M3' = mk_unadorned_v39 4 (#0.513)
1213 (funlist_v39 [(0,1),(sqrt8);(0,2),(sqrt8);(1,3),(sqrt8)] (&2) 4)
1214 (funlist_v39 [(0,1),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
1216 let scs_4M4 = new_definition
1217 `scs_4M4' = mk_unadorned_v39 4 (#0.513)
1218 (funlist_v39 [(0,1),(&2*h0);(1,2),(&2*h0);(0,2),(&2*h0);(1,3),(&2*h0)] (&2) 4)
1219 (funlist_v39 [(0,1),cstab;(1,2),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
1221 let scs_4M5 = new_definition
1222 `scs_4M5' = mk_unadorned_v39 4 (#0.513)
1223 (funlist_v39 [(0,1),(&2*h0);(2,3),(&2*h0);(0,2),(&2*h0);(1,3),(&2*h0)] (&2) 4)
1224 (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
1226 let scs_4M6 = new_definition
1227 `scs_4M6' = mk_unadorned_v39 4 (#0.513)
1228 (funlist_v39 [(0,1),(&2*h0);(0,2),(cstab);(1,3),(cstab)] (&2) 4)
1229 (funlist_v39 [(0,1),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
1231 let scs_4M7 = new_definition
1232 `scs_4M7 = mk_unadorned_v39 4 (#0.513)
1233 (funlist_v39 [(0,1),(&2*h0);(1,2),(&2*h0);(0,2),(cstab);(1,3),(cstab)] (&2) 4)
1234 (funlist_v39 [(0,1),cstab;(1,2),cstab;(0,2),(&6);(1,3),(&6);(1,3),(&6)] (&2*h0) 4)`;;
1236 let scs_4M8 = new_definition
1237 `scs_4M8 = mk_unadorned_v39 4 (#0.513)
1238 (funlist_v39 [(0,1),(&2*h0);(2,3),(&2*h0);(0,2),(cstab);(1,3),(cstab)] (&2) 4)
1239 (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(&6);(1,3),(&6);(1,3),(&6)] (&2*h0) 4)`;;
1241 let scs_3M1 = new_definition
1242 `scs_3M1 = mk_unadorned_v39 3 (#0.103)
1243 (funlist_v39 [(0,1),(&2 * h0)] (&2) 3)
1244 (funlist_v39 [(0,1),(cstab)] (&2 * h0) 3)`;;
1247 (* Some conclusions *)
1249 let QKNVMLB1_concl = `!s p q d' mkj vv.
1250 (let s' = scs_half_slice_v39 s p q d' mkj in
1251 let vv' = (\i. vv ((i+p) MOD (scs_k_v39 s'))) in
1253 scs_bm_v39 s p q < &4 /\
1254 ((scs_k_v39 s = 4) \/ scs_bm_v39 s p q <= cstab) /\
1255 is_scs_v39 s /\ d' < #0.9 /\ scs_diag (scs_k_v39 s) p q ==>
1258 let QKNVMLB2_concl = `!s p q d' d'' mkj vv.
1259 (let s' = FST (scs_slice_v39 s p q d' d'' mkj) in
1260 let s'' = SND (scs_slice_v39 s p q d' d'' mkj) in
1261 let vv' = (\i. vv ((i+p) MOD (scs_k_v39 s'))) in
1262 let vv'' = (\i. vv ((i+q) MOD (scs_k_v39 s''))) in
1264 is_scs_v39 s /\ scs_diag (scs_k_v39 s) p q /\
1265 is_scs_slice_v39 s s' s'' p q /\
1266 scs_d_v39 s <= d' + d'' ==>
1267 dsv_v39 s vv <= dsv_v39 s' vv' + dsv_v39 s'' vv'')`;;
1269 let QKNVMLB3_concl = `!s p q d' d'' mkj vv.
1270 (let s' = FST (scs_slice_v39 s p q d' d'' mkj) in
1271 let s'' = SND (scs_slice_v39 s p q d' d'' mkj) in
1272 let vv' = (\i. vv ((i+p) MOD (scs_k_v39 s'))) in
1273 let vv'' = (\i. vv ((i+q) MOD (scs_k_v39 s''))) in
1275 is_scs_v39 s /\ scs_diag (scs_k_v39 s) p q /\
1276 is_scs_slice_v39 s s' s'' p q /\
1277 scs_d_v39 s <= d' + d'' ==>
1278 taustar_v39 s' vv' + taustar_v39 s'' vv'' <= taustar_v39 s vv)`;;
1283 let FZIOTEF_REFL = prove_by_refinement(
1284 `!S. (!s. s IN S ==> is_scs_v39 s) ==> scs_arrow_v39 S S`,
1287 REWRITE_TAC[scs_arrow_v39];
1292 let FZIOTEF_TRANS = prove_by_refinement(
1293 `!S1 S2 S3. scs_arrow_v39 S1 S2 /\ scs_arrow_v39 S2 S3 ==>
1294 scs_arrow_v39 S1 S3`,
1297 REWRITE_TAC[scs_arrow_v39];
1298 REPEAT WEAKER_STRIP_TAC;
1304 let EQTTNZI1_concl = `!s. is_scs_v39 s /\
1305 (!i j. scs_J_v39 s i j ==> scs_b_v39 s i j = scs_bm_v39 s i j) /\
1306 (scs_J_v39 s = (\i j. F) \/ 3 < scs_k_v39 s)
1307 ==> scs_arrow_v39 {s} {restriction_typ1_v39 s}`;;
1309 let EQTTNZI2_concl = `!s t. is_scs_v39 s /\
1310 (scs_am_v39 s = scs_bm_v39 s) /\
1311 (t = restriction_typ2_v39 s) /\ (!i j. ~scs_J_v39 s i j) /\
1312 (!i. scs_am_v39 s i i = &0) /\
1313 CARD { i | i < scs_k_v39 t /\ (&2 * h0 < scs_b_v39 t i (SUC i) \/ &2 < scs_a_v39 t i (SUC i)) } + scs_k_v39 t <= 6
1314 ==> scs_arrow_v39 {s} {t}`;;
1316 let UAGHHBM_concl = `!s i j c .
1317 (let k = scs_k_v39 s in
1319 scs_a_v39 s i j <= c /\ c <= scs_b_v39 s i j /\
1321 ~(i MOD k = j MOD k) /\
1322 ~(scs_J_v39 s i j) /\
1323 ((j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) ==> (~(c = scs_am_v39 s i j))) /\
1324 ((j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) ==> (&2 < scs_a_v39 s i j \/ &2 * h0 < scs_b_v39 s i j))
1326 scs_arrow_v39 {s} (set_of_list (subdiv_v39 s i j c))))`;;
1328 let YXIONXL1_concl = `!s t.
1330 transfer_v39 s t ==> scs_arrow_v39 {s} {t}`;;
1332 let YXIONXL2_concl = `!s.
1333 is_scs_v39 s ==> scs_arrow_v39 {s} {scs_opp_v39 s}`;;
1335 let YXIONXL3_concl = `!s i.
1336 is_scs_v39 s ==> scs_arrow_v39 {s} {scs_prop_equ_v39 s i}`;;
1338 let LKGRQUI_concl = `!s s' s'' p q d' d'' mkj.
1339 is_scs_v39 s /\ (s',s'') = scs_slice_v39 s p q d' d'' mkj ==> scs_arrow_v39 {s} {s',s''}`;;
1341 let HXHYTIJ_concl = `!s vv ww.
1343 BBprime2_v39 s vv /\
1345 (taustar_v39 s vv < taustar_v39 s ww \/
1346 BBindex_v39 s vv <= BBindex_v39 s ww)`;;
1348 let ODXLSTCv2_concl = `!s k w l.
1353 (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i) /\
1354 ~(&2 = norm (w l)) /\
1355 (!i. ~(i MOD k = l MOD k) ==> scs_a_v39 s l i < dist(w l,w i)) /\
1356 (!i. ~(scs_J_v39 s l i)) /\
1358 V = IMAGE w (:num) /\
1359 E = IMAGE (\i. {w i, w (SUC i)}) (:num) ==>
1360 ~(lunar (v,(w l)) V E )) ==> F`;;
1362 let IMJXPHRv2_concl = `!s k w l.
1365 azim (vec 0) (w l) (w (SUC l)) (w (l + (scs_k_v39 s - 1)) ) = pi /\
1368 ~(collinear {vec 0,w (SUC l),w (l + (scs_k_v39 s - 1)) })/\
1369 (w l) IN aff_gt {vec 0} {w (SUC l),w (l + (scs_k_v39 s - 1)) }/\
1371 (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i) /\
1372 ~(&2 = norm (w l)) /\
1373 (!i. scs_diag k l i ==> scs_a_v39 s l i < dist(w l,w i)) /\
1374 (!i. ~(scs_J_v39 s l i)) /\
1376 V = IMAGE w (:num) /\
1377 E = IMAGE (\i. {w i, w (SUC i)}) (:num) ==>
1378 ~(lunar (v,(w l)) V E )) ==>
1379 (scs_a_v39 s l (SUC l) = dist (w l, w (SUC l)) /\
1380 (scs_a_v39 s l (l + (k-1)) = dist (w l, w (l + (k-1)))))`;;
1382 let NUXCOEAv2_concl = `!s k w l j.
1385 azim (vec 0) (w l) (w (SUC l)) (w (l + (scs_k_v39 s - 1)) ) = pi /\
1386 ~(collinear {vec 0,w (SUC l),w (l + (scs_k_v39 s - 1)) })/\
1387 (w l) IN aff_gt {vec 0} {w (SUC l),w (l + (scs_k_v39 s - 1)) }/\
1390 (j MOD k = SUC l MOD k \/ SUC j MOD k = l MOD k) /\
1391 (scs_a_v39 s j l = dist(w j,w l)) /\
1392 (scs_a_v39 s j l < scs_b_v39 s j l) /\
1393 (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i) /\
1394 (!i. scs_diag k l i ==> scs_a_v39 s l i < dist(w l,w i)) /\
1395 (!i. ~(scs_J_v39 s l i)) /\
1397 V = IMAGE w (:num) /\
1398 E = IMAGE (\i. {w i, w (SUC i)}) (:num) ==>
1399 ~(lunar (v,(w l)) V E )) ==>
1400 (scs_a_v39 s l (SUC l) = dist (w l, w (SUC l)) /\
1401 (scs_a_v39 s l (l + (k-1)) = dist (w l, w (l + (k-1)))))`;;
1405 let deform_ODXLSTC_concl = `!s k l.
1407 ~(MMs_v39 s = {}) /\
1410 (!i. ~(scs_J_v39 s l i)) /\
1411 ~(scs_lo_v39 s l) /\
1412 (!j. ~(j MOD k = l MOD k) ==> scs_a_v39 s j l < scs_bm_v39 s j l) /\
1413 (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i)
1416 ({(scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,scs_bm_v39 s,
1417 scs_b_v39 s, scs_J_v39 s, {j | j MOD k = l} UNION scs_lo_v39 s ,
1418 scs_hi_v39 s, scs_str_v39 s))} UNION
1419 (IMAGE (\j. (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,
1420 (\i i'. if {i MOD k,i' MOD k} = {j MOD k,l MOD k} then scs_a_v39 s j l
1421 else scs_bm_v39 s i i'), scs_b_v39 s,scs_J_v39 s, scs_lo_v39 s , scs_hi_v39 s, scs_str_v39 s)))
1422 {j | ~(j = l) /\ j < scs_k_v39 s /\ (scs_a_v39 s l j = scs_am_v39 s l j) }))
1425 let deform_IMJXPHR_concl = `!s k p0 p1 p2.
1432 ~(scs_J_v39 s p0 p1) /\
1433 ~(scs_J_v39 s p1 p2) /\
1434 ~(scs_lo_v39 s p1) /\
1435 (!i. scs_diag k p1 i ==> &4 * h0 < scs_b_v39 s p1 i) /\
1436 (!i. scs_diag k p1 i ==> ~(scs_a_v39 s p1 i = scs_bm_v39 s p1 i)) /\
1437 (?q0 q2. ({p0,p2} = {q0,q2}) /\
1438 scs_a_v39 s p1 q0 = scs_bm_v39 s p1 q0 /\
1439 ~(scs_a_v39 s p1 q2 = scs_bm_v39 s p1 q2)) ==>
1441 ({(scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,scs_bm_v39 s,
1442 scs_b_v39 s, scs_J_v39 s,
1443 {j | j MOD k = p1} UNION scs_lo_v39 s , scs_hi_v39 s, scs_str_v39 s))} UNION
1444 (IMAGE (\j. (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,
1445 (\i i'. if {i MOD k,i' MOD k} = {j MOD k,p1 MOD k} then scs_a_v39 s j p1
1446 else scs_bm_v39 s i i'), scs_b_v39 s,scs_J_v39 s, scs_lo_v39 s , scs_hi_v39 s,scs_str_v39 s)))
1447 {j | ~(j = p1) /\ j < scs_k_v39 s /\ (scs_a_v39 s p1 j = scs_am_v39 s p1 j) }))`;;
1449 let deform_NUXCOEA_concl = `!s k p0 p1 p2 p'.
1456 ~(scs_J_v39 s p0 p1) /\
1457 ~(scs_J_v39 s p1 p2) /\
1458 (!i. scs_diag k p1 i ==> &4 * h0 < scs_b_v39 s p1 i) /\
1459 (!i. scs_diag k p1 i ==> ~(scs_a_v39 s p1 i = scs_bm_v39 s p1 i)) /\
1460 (?p''. ({p0,p2} = {p',p''}) /\
1461 scs_a_v39 s p1 p' = scs_bm_v39 s p1 p' /\
1462 ~(scs_a_v39 s p1 p'' = scs_bm_v39 s p1 p'')) ==>
1464 (IMAGE (\j. (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,
1465 (\i i'. if {i MOD k,i' MOD k} = {j MOD k,p1 MOD k} then scs_a_v39 s j p1
1466 else scs_bm_v39 s i i'), scs_b_v39 s,scs_J_v39 s, scs_lo_v39 s , scs_hi_v39 s,scs_str_v39 s)))
1467 {j | ~(j = p1) /\ ~(j = p') /\ j < scs_k_v39 s /\ (scs_a_v39 s p1 j = scs_am_v39 s p1 j) })`;;
1469 let deform_2065952723_A1_single = `!s k p1 p2 p'.
1473 arcmax_v39 s (p1,p2) < arc1553_v39 /\
1474 ~(scs_J_v39 s p1 p2) /\
1475 ~(scs_str_v39 s p1) /\
1476 ~(scs_str_v39 s p2) /\
1477 (!i. scs_diag k p1 i ==> &4 * h0 < scs_b_v39 s p1 i) /\
1478 (!i. scs_diag k p1 i ==> ~(scs_a_v39 s p1 i = scs_bm_v39 s p1 i)) /\
1479 ~(scs_a_v39 s p1 p2 = scs_bm_v39 s p1 p2) /\
1480 ~(scs_b_v39 s p1 p2 = scs_am_v39 s p1 p2) /\
1481 (?p''. ({p0,p2} = {p',p''}) /\
1482 scs_a_v39 s p1 p' = scs_bm_v39 s p1 p' /\
1483 ~(scs_a_v39 s p1 p'' = scs_bm_v39 s p1 p'')) ==>
1485 ({(scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,scs_bm_v39 s,
1486 scs_b_v39 s,scs_J_v39 s,
1487 ({j | j MOD k = p1 MOD k} UNION scs_lo_v39 s) , scs_hi_v39 s,scs_str_v39 s)),
1488 (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,scs_bm_v39 s,
1489 scs_b_v39 s,scs_J_v39 s,
1490 ({j | j MOD k = p2 MOD k} UNION scs_lo_v39 s) , scs_hi_v39 s,scs_str_v39 s))}
1492 (IMAGE (\j. (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,
1493 (\i i'. if {i MOD k,i' MOD k} = {j MOD k,p1 MOD k} then scs_a_v39 s j p1
1494 else scs_bm_v39 s i i'), scs_b_v39 s,scs_J_v39 s, scs_lo_v39 s , scs_hi_v39 s, scs_str_v39 s)))
1495 {j | j < scs_k_v39 s /\ (scs_a_v39 s p1 j = scs_am_v39 s p1 j) })
1497 (IMAGE (\j. (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,
1498 (\i i'. if {i MOD k,i' MOD k} = {j MOD k,p1 MOD k} then scs_a_v39 s j p1
1499 else scs_bm_v39 s i i'), scs_b_v39 s,scs_J_v39 s, scs_lo_v39 s , scs_hi_v39 s,scs_str_v39 s)))
1500 {j | ~(j = p1) /\ ~(j = p') /\ j < scs_k_v39 s /\ (scs_a_v39 s p1 j = scs_am_v39 s p1 j) }))`;;
1504 (* new material 2013-06-17 *)
1507 let DRNDRDV_concl = `!y1 y2 y6.
1508 derived_form (&0 < y1 /\ &0 < y2)
1509 (\q. xrr y1 y2 q) ((&8 * y6) / (y1 * y2)) y6 (:real)`;;
1511 let TBRMXRZ1_concl = `!f f' g h' x y.
1512 derived_form T f f' y (:real) /\
1513 derived_form T (f o g) h' x (:real) /\
1514 g x = y ==> re_eqvl f' h'`;;
1517 let PQCSXWG1_concl = `!v0 v1 v2 v3 x1 x2 x3 x4 x5 x6.
1518 &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\ &0 < x6 /\
1519 ~collinear {v0,v1,v2} /\
1520 x1 = dist(v1,v0) pow 2 /\
1521 x2 = dist(v2,v0) pow 2 /\
1522 x6 = dist(v1,v2) pow 2 /\
1523 &0 < delta_x x1 x2 x3 x4 x5 x6 /\
1524 v3 = mk_simplex v0 v1 v2 x1 x2 x3 x4 x5 x6 ==>
1525 (x3 = dist(v3,v0) pow 2 /\
1526 x5 = dist(v3,v1) pow 2 /\
1527 x4 = dist(v3,v2) pow 2 /\
1528 (v1 - v0) dot ((v2 - v0) cross (v3 - v0)) > &0)`;;
1530 (* some other continuities might be needed *)
1532 let PQCSXWG2_concl = `!(v0:real^3) v1 v2 v3 x1 x2 x3 x4 x5 x6.
1533 &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\ &0 < x6 /\
1534 ~collinear {v0,v1,v2} /\
1535 x1 = dist(v1,v0) pow 2 /\
1536 x2 = dist(v2,v0) pow 2 /\
1537 x6 = dist(v1,v2) pow 2 /\
1538 &0 < delta_x x1 x2 x3 x4 x5 x6 /\
1539 v3 = mk_simplex v0 v1 v2 x1 x2 x3 x4 x5 x6 ==>
1540 (\q. mk_simplex v0 v1 v2 x1 x2 x3 x4 q x6) continuous atreal x5`;;
1543 let PQCSXWG1_concl = `!v0 v1 v2 v3 x1 x2 x3 x4 x5 x6.
1544 &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\ &0 < x6 /\
1545 ~collinear {v0,v1,v2} /\
1546 x1 = dist(v1,v0) pow 2 /\
1547 x2 = dist(v2,v0) pow 2 /\
1548 x6 = dist(v1,v2) pow 2 /\
1549 &0 < delta_x x1 x2 x3 x4 x5 x6 /\
1550 v3 = mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6 ==>
1551 (x3 = dist(v3,v0) pow 2 /\
1552 x5 = dist(v3,v1) pow 2 /\
1553 x4 = dist(v3,v2) pow 2 /\
1554 (v1 - v0) dot ((v2 - v0) cross (v3 - v0)) > &0)`;;
1556 let PQCSXWG2_concl = `!(v0:real^3) v1 v2 v3 x1 x2 x3 x4 x5 x6.
1557 &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\ &0 < x6 /\
1558 ~collinear {v0,v1,v2} /\
1559 x1 = dist(v1,v0) pow 2 /\
1560 x2 = dist(v2,v0) pow 2 /\
1561 x6 = dist(v1,v2) pow 2 /\
1562 &0 < delta_x x1 x2 x3 x4 x5 x6 /\
1563 v3 = mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6 ==>
1564 (\q. mk_simplex1 v0 v1 v2 x1 x2 x3 x4 q x6) continuous atreal x5`;;
1566 let EYYPQDW_concl = `!v0 v1 v2 v3 x1 x2 x3 x5 x6 s.
1567 &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x5 /\ &0 < x6 /\
1568 ~collinear {v0,v1,v2} /\
1569 x1 = dist(v1,v0) pow 2 /\
1570 x2 = dist(v2,v0) pow 2 /\
1571 x6 = dist(v1,v2) pow 2 /\
1572 &0 < ups_x x1 x3 x5 /\
1573 (s = &1 \/ s = -- &1) /\
1574 v3 = mk_planar2 v0 v1 v2 x1 x2 x3 x5 x6 s ==>
1575 (coplanar {v0,v1,v2,v3} /\
1576 x3 = dist(v3,v0) pow 2 /\
1577 x5 = dist(v3,v1) pow 2 /\
1579 t % ((v3- v0) cross (v1- v0)) = ( s % ((v1 - v0) cross (v2 - v0))))`;;
1581 let EYYPQDW2_concl = `!(v0:real^3) v1 v2 x1 x2 x3 x5 x6 s.
1582 &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x5 /\ &0 < x6 /\
1583 ~collinear {v0,v1,v2} /\
1584 x1 = dist(v1,v0) pow 2 /\
1585 x2 = dist(v2,v0) pow 2 /\
1586 x6 = dist(v1,v2) pow 2 /\
1587 &0 < ups_x x1 x3 x5 ==>
1588 (\q. mk_planar v0 v1 v2 x1 x2 q x5 x6 s) continuous atreal x3`;;
1590 let EYYPQDW3_concl = `!(v0:real^3) v1 v2 x1 x2 x3 x5 x6 s.
1591 &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x5 /\ &0 < x6 /\
1592 ~collinear {v0,v1,v2} /\
1593 x1 = dist(v1,v0) pow 2 /\
1594 x2 = dist(v2,v0) pow 2 /\
1595 x6 = dist(v1,v2) pow 2 /\
1596 &0 < ups_x x1 x3 x5 ==>
1597 (\q. mk_planar v0 v1 q x1 x2 x3 x5 x6 s) continuous at v2`;;
1599 let FEKTYIY_concl = `!s v.
1600 is_scs_v39 s /\ v IN MMs_v39 s /\ 3 < scs_k_v39 s ==>
1601 ~coplanar ({vec 0} UNION IMAGE v (:num))`;;
1603 let AURSIPD_concl = `!s v. 3 < scs_k_v39 s /\
1604 is_scs_v39 s /\ scs_generic v /\ v IN MMs_v39 s ==>
1605 3 + CARD { i | i < scs_k_v39 s /\ scs_is_str s vv i} <= scs_k_v39 s`;;
1607 let PPBTYDQ_concl = `!(u:real^3) v p. ~collinear {vec 0,v,p} /\ ~collinear {vec 0,u,p} /\
1608 arcV (vec 0) u p + arcV (vec 0) p v < pi ==> ~(vec 0 IN conv {u,v})`;;
1610 let MXQTIED_concl = `!s s' v.
1611 is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
1612 scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
1613 v IN MMs_v39 s /\ v IN BBs_v39 s' /\ scs_d_v39 s = scs_d_v39 s' /\
1614 (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i)) /\
1615 (!i j. scs_a_v39 s i j <= scs_a_v39 s' i j /\ scs_b_v39 s' i j <= scs_b_v39 s i j) ==>
1618 let SYNQIWN_concl = `!s v i.
1619 is_scs_v39 s /\ v IN BBs_v39 s /\
1620 (norm (v i) = &2 \/ dist(v i,v (i+1)) = &2) /\
1621 (norm (v (i+2)) = &2 \/ dist(v (i+1),v(i+2)) = &2) /\
1622 cstab <= dist(v i,v(i+2)) ==>
1623 pi/ &2 < azim (vec 0) (v (i+1)) (v (i+2)) (v i)`;;
1625 let XWNHLMD_concl = `!s s' v.
1626 is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
1627 scs_k_v39 s = scs_k_v39 s' /\
1628 v IN MMs_v39 s /\ v IN BBs_v39 s' ==>
1629 scs_arrow_v39 {s} {s'}`;;
1631 let OIQKKEP_concl = `!u v c.
1632 u IN ball_annulus /\ v IN ball_annulus /\ c < &4 /\ &2 <= dist(u,v) /\ dist(u,v) <= c ==>
1633 arcV (vec 0) u v <= arclength (&2) (&2) c`;;
1635 let AXJRPNC_concl = `!s (v:num->real^3) i j.
1636 is_scs_v39 s /\ scs_basic_v39 s /\
1638 (!i. scs_b_v39 s i (SUC i) <= cstab) /\
1639 (lunar (v i,v j) (IMAGE v (:num))
1640 (IMAGE (\i. {v i, v (SUC i)}) (:num)) ) ==>
1641 (scs_k_v39 s = 6 /\ v j = v (i + 3))`;;
1643 let RRCWNSJ_concl = `!s (v:num->real^3).
1644 is_scs_v39 s /\ scs_basic_v39 s /\ 3 < scs_k_v39 s /\
1646 (!i j. scs_diag (scs_k_v39 s) i j ==> &4 * h0 < scs_b_v39 s i j) /\
1647 (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j))) /\
1648 (!i. scs_b_v39 s i (SUC i) <= cstab) ==>
1651 let JCYFMRP_concl = `!s (v:num->real^3).
1652 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
1653 (!i j. scs_diag (scs_k_v39 s) i j ==> &4 * h0 < scs_b_v39 s i j) /\
1654 CARD (scs_M s) <= 1 /\ 3 < scs_k_v39 s /\
1655 (!i. scs_a_v39 s i (SUC i) = &2) /\
1656 (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j))) ==>
1657 (?i. dist(v i, v (i+1)) = &2)`;;
1659 let TFITSKC_concl = `!s (v:num->real^3) i.
1660 is_scs_v39 s /\ 3 < scs_k_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
1661 scs_a_v39 s (i+1) (i+2) = &2 /\ scs_b_v39 s (i+1) (i+2) = &2 * h0 /\
1662 dist(v i,v (i+1)) = &2 /\
1663 (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j)) /\
1664 &4 * h0 < scs_b_v39 s i j) /\
1665 &2 < scs_b_v39 s i (i+1) /\ scs_a_v39 s (i+2) (i+3) < scs_b_v39 s (i+2) (i+3) ==>
1666 dist(v (i+1),v(i+2)) = &2`;;
1669 (* 3 < k, aij < bij *)
1672 `!s (v:num->real^3) i.
1673 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
1674 (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j))) ==>
1675 scs_a_v39 s (i) (i+1) = &2 /\ scs_b_v39 s (i) (i+1) = &2 * h0 /\
1676 scs_a_v39 s (i+1) (i+2) = &2 /\ scs_b_v39 s (i+1) (i+2) = &2 * h0 ==>
1677 (dist(v i,v (i+1)) = &2 <=> dist(v(i+1),v(i+2)) = &2)`;;
1679 let JLXFDMJ_concl = `!s (v:num->real^3) i.
1680 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
1681 dist(v i,v (i+1)) = &2 /\
1682 (!i j. scs_diag (scs_k_v39 s) i j ==> &4 * h0 < scs_b_v39 s i j) /\
1683 CARD (scs_M s) <= 1 /\
1684 (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j))) /\
1685 (!i. scs_a_v39 s i (i+1) < scs_b_v39 s i (i+1)) /\
1686 scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1) <= &2 * h0
1688 (!j. ~(j IN scs_M s ) ==> dist(v j , v(j+1)) = &2)`;;
1690 let WKEIDFT_concl = `!s a b a' b' p q p' q'.
1691 (let k = scs_k_v39 s in
1692 (is_scs_v39 s /\ scs_basic_v39 s /\
1693 (!i. scs_a_v39 s i (i + 1) = a) /\
1694 (!i. scs_b_v39 s i (i + 1) = b) /\
1696 (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\
1697 (!i j. scs_diag k i j ==> scs_a_v39 s i j = a') /\
1698 (!i j. scs_diag k i j ==> scs_b_v39 s i j = b') ==>
1699 scs_arrow_v39 {scs_stab_diag_v39 s p q} {scs_stab_diag_v39 s p' q'}))`;;
1701 let PEDSLGV1_concl = `!v i j.
1702 v IN MMs_v39 scs_6I1 /\
1704 dist(v i,v j) <= cstab ==>
1705 v IN MMs_v39 (scs_stab_diag_v39 scs_6I1 i j)`;;
1707 let PEDSLGV2_concl = `!v.
1708 v IN MMs_v39 scs_6I1 /\
1709 (!i j. scs_diag 6 i j ==> cstab <= dist(v i,v j)) ==>
1710 v IN MMs_v39 (scs_6M1)`;;
1712 let AQICLXA_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 2 } { scs_5M1, scs_3M1 }`;;
1714 let FUNOUYH_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 3 } {scs_4M2 }`;;
1716 let OEHDBEN_concl = `scs_arrow_v39 { scs_6I1 } { scs_6T1, scs_5M1, scs_4M2, scs_3T1 }`;;
1718 let OTMTOTJ1_concl = `scs_arrow_v39 { scs_5I1 } { scs_stab_diag_v39 scs_5I1 0 2 , scs_5M2 }`;;
1720 let OTMTOTJ2_concl = `scs_arrow_v39 { scs_5I2 } { scs_stab_diag_v39 scs_5I2 0 2 , scs_5M2 }`;;
1722 (* corrected 2013/08/05 *)
1723 let OTMTOTJ3_concl = `scs_arrow_v39 { scs_5I3 } { scs_stab_diag_v39 scs_5M1 0 2 ,
1724 scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4, scs_5M2 }`;;
1726 let OTMTOTJ4_concl = `scs_arrow_v39 { scs_5M1 } { scs_stab_diag_v39 scs_5M1 0 2 ,
1727 scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4, scs_5M2 }`;;
1729 let HIJQAHA_concl = `scs_arrow_v39 { scs_5M2 } { scs_3T1,scs_3T4,scs_4M6',scs_4M7,scs_4M8,
1730 scs_5T1, scs_stab_diag_v39 scs_5I2 0 2 ,
1731 scs_stab_diag_v39 scs_5M1 0 2 , scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4 }`;;
1733 let CNICGSF1_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_5I1 0 2 }
1734 {scs_4M2, scs_3M1 }`;;
1736 let CNICGSF2_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_5I2 0 2 }
1737 {scs_4M3', scs_3T1 }`;;
1739 let CNICGSF3_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_5M1 0 2 }
1740 {scs_4M2, scs_3T4 }`;;
1742 let CNICGSF4_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_5M1 0 3 }
1743 {scs_4M4', scs_3M1 }`;;
1745 let CNICGSF5_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_5M1 2 4 }
1746 {scs_4M5', scs_3M1 }`;;
1748 let ARDBZYE_concl = `scs_arrow_v39 { scs_4I2 } { scs_4T1, scs_4T2 }`;;
1750 let FYSSVEV_concl = `scs_arrow_v39 { scs_4I1 } {scs_4I2, scs_stab_diag_v39 scs_4I1 0 2 }`;;
1752 let AUEAHEH_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_4I1 0 2 } { scs_3M1 }`;;
1754 let ZNLLLDL_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_4I3 0 2 } { scs_4T4 }`;;
1756 let VQFYMZY_concl = `scs_arrow_v39 { scs_4I3 } { scs_4T4, scs_4M6' }`;;
1758 (* let CNFNTYP_concl = `scs_arrow_v39 { scs_4M1 } { scs_4M2, scs_4M6' }`;; *)
1760 let BNAWVNH_concl = `scs_arrow_v39 { scs_4M2 } { scs_3M1, scs_3T4, scs_4M6' }`;;
1762 let RAWZDIB_concl = `scs_arrow_v39 { scs_4M3' } { scs_3T1, scs_3T6', scs_4M6' }`;;
1764 let MFKLVDK_concl = `scs_arrow_v39 { scs_4M4' } { scs_3M1, scs_3T4, scs_3T3, scs_4M7 }`;;
1766 let RYPDIXT_concl = `scs_arrow_v39 { scs_4M5' } { scs_3T4, scs_4M8 }`;;
1768 let GSXRFWM_concl = `!s v.
1769 is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s ==> scs_generic v`;;
1771 let WGDHPPI_concl = `!s v.
1772 is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s ==>
1773 CARD { i | i < scs_k_v39 s /\ scs_is_str s v i} <= 1`;;
1775 let ASSWPOW_concl = `!s v i.
1776 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
1777 scs_b_v39 s i (i+1) <= &2 * h0 /\ scs_b_v39 s (i+1) (i+2) <= &2 * h0
1778 ==> xrr (norm (v i)) (norm(v(i+2))) (dist(v i,v(i+2))) <= #15.53 `;;
1780 let YEBWJNG_concl = `!s v p.
1781 is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\
1782 (!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) /\
1783 (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
1784 (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
1785 ~scs_is_str s v p /\ ~scs_is_str s v (p+1) /\ scs_a_v39 s p (p+1) = &2
1786 ==> dist(v p,v(p+1)) = &2`;;
1788 let TUAPYYU_concl = `!s v p.
1789 is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\
1790 (!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) /\
1791 (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
1792 (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
1793 ~scs_is_str s v p /\ ~scs_is_str s v (p+1)
1794 ==> 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)`;;
1796 let WKZZEEH_concl = `!s v p.
1797 is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\
1798 (!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) /\
1799 (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
1800 (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
1801 ~scs_is_str s v p /\ ~scs_is_str s v (p+1) /\ ~scs_is_str s v (p+3)
1802 ==> (~(dist(v p,v(p+3)) = cstab /\ dist(v(p),v(p+1)) = cstab))`;;
1804 let PWEIWBZ_concl = `!s v p.
1805 is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\
1806 (!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) /\
1807 (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
1808 (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
1809 scs_a_v39 s p (p+1) = &2
1810 ==> dist(v p,v(p+1)) = &2`;;
1812 let VASYYAU_concl = `!s v p.
1813 is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\
1814 (!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) /\
1815 (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
1816 (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
1818 ==> (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))`;;
1822 let UFGHLP1_concl = `!s v i.
1823 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
1824 (!i. scs_b_v39 s i (i+1) <= cstab) /\
1825 (!i j. scs_diag 4 i j ==> scs_a_v39 s i j < dist(v i,v j)) /\
1826 (scs_is_str s v (i+1)) ==>
1827 ((dist(v i,v(i+1)) = scs_a_v39 s i (i+1) <=> dist(v(i+1),v(i+2)) = scs_a_v39 s (i+1) (i+2)))`;;
1829 let UFGHLP2_concl = `!s v i.
1830 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
1831 (!i. scs_b_v39 s i (i+1) <= cstab) /\
1832 (!i j. scs_diag 4 i j ==> scs_a_v39 s i j < dist(v i,v j)) /\
1833 (scs_is_str s v (i+1)) ==>
1834 ((dist(v i,v(i+1)) = scs_b_v39 s i (i+1) <=> dist(v(i+1),v(i+2)) = scs_b_v39 s (i+1) (i+2)))`;;
1836 let DSZPJSK_concl = `!s v i.
1837 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
1838 (!i. scs_b_v39 s i (i+1) <= cstab) /\
1839 (!i j. scs_diag 4 i j ==> scs_a_v39 s i j < dist(v i,v j)) /\
1840 (scs_is_str s v (i+1)) ==>
1841 (~(dist(v i,v(i+1)) = &2 * h0 /\ dist(v(i+1),v(i+2)) = cstab) /\
1842 ~(dist(v i,v(i+1)) = cstab /\ dist(v(i+1),v(i+2)) = &2 *h0))`;;
1844 let RDLGWIE_concl = `!s v i.
1845 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
1846 (!i. scs_b_v39 s i (i+1) <= cstab) /\
1847 (!i j. scs_diag 4 i j ==> scs_a_v39 s i j < dist(v i,v j)) ==>
1848 (~(dist(v i,v(i+1)) = &2 * h0 /\ dist(v(i+1),v(i+2)) = cstab) /\
1849 ~(dist(v i,v(i+1)) = cstab /\ dist(v(i+1),v(i+2)) = &2 *h0))`;;
1851 let LFYPZPI_concl = `!s v i.
1852 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
1853 (!i. scs_b_v39 s i (i+1) <= cstab) /\
1854 (!i j. scs_diag 4 i j ==> scs_a_v39 s i j < dist(v i,v j)) /\
1855 (dist(v i,v(i+1)) = &2 * h0) /\
1856 (dist(v (i+1),v(i+2)) = &2 * h0) /\
1857 (dist(v (i+2),v(i+3)) = &2 * h0) /\
1858 (scs_b_v39 s i (i+1) = &2 * h0) /\
1859 (scs_b_v39 s (i+1) (i+2) = &2 * h0) /\
1860 (scs_b_v39 s (i+2) (i+3) = &2 * h0) ==> F`;;
1862 let NZBSJXG_concl = `!s v i.
1863 is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
1864 (!i. scs_b_v39 s i (i+1) <= cstab) /\
1865 CARD (scs_M s) <= 1 /\
1866 (!i j. scs_diag 4 i j ==> scs_a_v39 s i j < dist(v i,v j)) /\
1867 (!i. scs_b_v39 s i (i+1) <= &2 * h0 ==> dist(v i,v (i+1)) = &2)`;;
1870 let NWDGKXH_concl = `scs_arrow_v39 {scs_4M6'} {scs_4T3,scs_4T5}`;;
1872 let EFLYGAU_concl = `(?v. v IN MMs_v39 scs_4M7 /\
1873 cstab < dist(v 0,v 2) /\ cstab < dist(v 1, v 3) )
1874 ==> scs_arrow_v39 {scs_4M7} {scs_4M6'}`;;
1876 let YOBIMPP_concl = ` scs_arrow_v39 {scs_4M7} {scs_3M1,scs_3T3,scs_3T4,scs_4M6'}`;;
1878 let BJTDWPS_concl = `(?v. v IN MMs_v39 scs_4M8 /\
1879 cstab < dist(v 0,v 2) /\ cstab < dist(v 1, v 3) ) ==>
1880 scs_arrow_v39 {scs_4M8} {scs_4M6',scs_3T7}`;;
1883 let MIQMCSN1_concl = `(?v. v IN MMs_v39 scs_4M8 /\
1884 (dist(v 0,v 2) = cstab \/ dist(v 1, v 3) = cstab )) ==>
1885 scs_arrow_v39 {scs_4M7} {scs_3T4}`;;
1888 let MIQMCSN_concl = `scs_arrow_v39 {scs_4M8} {scs_4M6',scs_3T7,scs_3T4}`;;
1890 let LFLACKU_concl = `scs_arrow_v39 {scs_3T1} {scs_3T2,scs_3T5}`;;
1892 let CUXVZOZ_concl = `main_nonlinear_terminal_v11 ==>
1894 FF = IMAGE (\i. (v i,v (SUC i))) (:num) /\
1901 &3 <= dist(v (p1+k-1),v (p1+1)) /\
1902 (!i j. scs_diag k i j /\ ~(psort k (i, j) = psort k ((p1+k-1),(p1+1))) ==> scs_a_v39 s i j < dist(v i,v j)) /\
1903 (!i j. scs_diag k i j ==> &4 * h0 < scs_b_v39 s i j) /\
1904 interior_angle1 (vec 0) FF (v p1) < pi /\
1905 (pi/ &2 < interior_angle1 (vec 0) FF (v p1) \/ interior_angle1 (vec 0) FF (v (p1+1)) < pi) /\
1906 scs_a_v39 s p1 (p1+1) = &2 /\
1907 scs_b_v39 s p1 (p1+1) <= &2 * h0 /\
1908 &2 <= dist(v (p1+k-1),v p1) /\
1909 dist(v (p1+k-1), v p1) <= cstab ==>
1910 dist(v p1,v (p1+1)) = &2)`;;
1912 let CJBDXXN_concl = `main_nonlinear_terminal_v11 ==>
1914 FF = IMAGE (\i. (v i,v (SUC i))) (:num) /\
1921 &3 <= dist(v (p1+1),v (p1+k-1)) /\
1922 (!i j. scs_diag k i j /\ ~(psort k (i, j) = psort k ((p1+1),(p1+k-1))) ==> scs_a_v39 s i j < dist(v i,v j)) /\
1923 (!i j. scs_diag k i j ==> &4 * h0 < scs_b_v39 s i j) /\
1924 interior_angle1 (vec 0) FF (v p1) < pi /\
1925 (pi/ &2 < interior_angle1 (vec 0) FF (v p1) \/ interior_angle1 (vec 0) FF (v (p1+k-1)) < pi) /\
1926 scs_a_v39 s p1 (p1+k-1) = &2 /\
1927 scs_b_v39 s p1 (p1+k-1) <= &2 * h0 /\
1928 &2 <= dist(v (p1+1),v p1) /\
1929 dist(v (p1+1), v p1) <= cstab ==>
1930 dist(v p1,v (p1+k-1)) = &2)`;;
1937 scs_diag (scs_k_v39 s) i j /\
1938 scs_a_v39 s i j <= cstab ==>
1939 is_scs_v39 (scs_stab_diag_v39 s i j) /\ scs_basic_v39 (scs_stab_diag_v39 s i j)
1943 `scs_arrow_v39 {scs_3M1} {scs_3T1,scs_3T5}`;;