text_formalization/local/appendix_main_estimate.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (* Section: Conclusions                                                       *)
   4 (* Chapter: Local Fan                                                         *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2013-02-26                                                           *)
   7 (* ========================================================================== *)
   8
   9 (*
  10 remaining conclusions from appendix to Local Fan chapter
  11
  12 svn 3270 contains deprecated terminal SCS cases
  13 *)
  14
  15
  16 module Appendix = struct
  17
  18
  19   open Hales_tactic;;
  20
  21
  22
  23   (* Proved in Lunar_deform.MHAEYJN *)
  24
  25   let MHAEYJN_concl =
  26     `!a b V E FF f v w u.
  27       convex_local_fan (V,E,FF) /\
  28       lunar (v,w) V E /\
  29       deformation f V (a,b) /\
  30       interior_angle1 (vec 0) FF v < pi /\
  31       u IN V /\
  32       ~(u = v) /\
  33       ~(u = w) /\
  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})
  36     ==> (?e. &0 < e /\
  37            (!t. --e < t /\ t < e
  38             ==> convex_local_fan
  39             (IMAGE (\v. f v t) V,
  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)))`;;
  44
  45   let ZLZTHIC_concl =
  46     `!a b V E FF f.
  47       convex_local_fan (V,E,FF) /\
  48       generic V E /\
  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)
  52     ==> (?e. &0 < e /\
  53            (!t. --e < t /\ t < e
  54             ==> convex_local_fan
  55             (IMAGE (\v. f v t) V,
  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)))`;;
  60
  61
  62   let VPWSHTO_concl =
  63     `!v x u w w1.
  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)
  65     /\ norm(v-x)= &2
  66     /\ norm(x-u)= &2
  67     /\ norm(u-w)= &2
  68     /\ norm(w-w1)= &2
  69     /\ norm(w1-v)= &2
  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)`;;
  74
  75   let arc1553_v39 = new_definition `arc1553_v39 = arclength (&2) (&2) (sqrt(#15.53))`;;
  76
  77
  78   let cstab=new_definition ` cstab= #3.01`;;
  79
  80   let rho_fun = new_definition `rho_fun y =  &1 + (inv (&2 * h0 - &2)) * (inv pi) * sol0 * (y - &2)`;;
  81
  82   let rho_rho_fun = prove_by_refinement(
  83     `!y. rho_fun y = rho y`,
  84     (* {{{ proof *)
  85     [
  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`];
  89       GEN_TAC;
  90       MATCH_MP_TAC (arith `(sol0/pi)*(&1 - a) = (sol0/pi)*(c*e) ==> sol0/pi - sol0/pi * a = c * inv pi * sol0 * e`);
  91       AP_TERM_TAC;
  92       BY(REAL_ARITH_TAC)
  93     ]);;
  94   (* }}} *)
  95
  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)`;;
  97
  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)`;;
 101
 102   (*
 103     let standard = new_definition
 104     ` standard v w <=> &2 <= norm(v-w) /\  norm (v-w) <= &2 *h0 `;;
 105
 106     let protracted = new_definition
 107     ` protracted v w <=> &2 * h0 <= norm(v-w) /\  norm (v-w) <= sqrt (&8) `;;
 108
 109     let diagonal0 = new_definition
 110     ` (diagonal0 (E:(real^3->bool)->bool) (v:real^3) (w:real^3))  <=> ~(v = w) /\ ~({v,w} IN E) `;;
 111
 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) `;;
 115
 116     let main_estimate= new_definition
 117     ` main_estimate(V,E,f) <=>
 118     convex_local_fan(V,E,f) /\
 119     packing V /\
 120     V SUBSET ball_annulus /\
 121     diagonal1(V,E) /\
 122     CARD E= CARD f /\
 123     3<= CARD E /\
 124     CARD E <= 6`;;
 125   *)
 126
 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)
 129     /\ s HAS_SIZE k`;;
 130
 131   let tgt = new_definition `tgt = #1.541`;;
 132
 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`;;
 138
 139   (* rename d_tame2 -> tame_table_d, for compatibility with the rest of the project. *)
 140
 141   (*
 142     let d_tame2 = new_definition `d_tame2 r s =
 143     if (r + 2 * s <= 3) then &0
 144     else
 145     #0.103 * (&2 - &s) + #0.2759 * (&r + &2 * &s - &4)`;;
 146
 147     let tame_table_d_tame2 = prove_by_refinement(
 148     `!r s. tame_table_d r s = if (r + 2 * s <= 3) then &0
 149     else
 150     #0.103 * (&2 - &s) + #0.2759 * (&r + &2 * &s - &4)`,
 151   (* {{{ proof *)
 152     [
 153     REWRITE_TAC[Sphere.tame_table_d];
 154     REPEAT WEAKER_STRIP_TAC;
 155     REWRITE_TAC[arith `r + 2 * s > 3 <=> ~(r + 2 * s <= 3)`];
 156     COND_CASES_TAC;
 157     BY(ASM_REWRITE_TAC[]);
 158     BY(REAL_ARITH_TAC)
 159     ]);;
 160   (* }}} *)
 161   *)
 162
 163   let JEJTVGB_std_concl =
 164     `!V E FF.
 165       convex_local_fan (V,E,FF) /\
 166       packing V /\
 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`;;
 172
 173   let JEJTVGB_std3_concl =
 174     `!v1 v2 v3.
 175     &2 <= norm v1 /\
 176     &2 <= norm v2 /\
 177     &2 <= norm v3 /\
 178     norm v1 <= &2 * h0 /\
 179     norm v2 <= &2 * h0 /\
 180     norm v3 <= &2 * h0 /\
 181     &2 <= dist(v1,v2) /\
 182     &2 <= dist(v1,v3) /\
 183     &2 <= dist(v2,v3) /\
 184     dist(v1,v2) <= &2 * h0 /\
 185     dist(v1,v3) <= &2 * h0 /\
 186     dist(v2,v3) <= &2 * h0 ==>
 187     &0 <= tau3 v1 v2 v3`;;
 188
 189   let JEJTVGB_pent_diag_concl =
 190     `!V E FF.
 191       convex_local_fan (V,E,FF) /\
 192       packing V /\
 193       V SUBSET ball_annulus /\
 194       CARD V = 5 /\
 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`;;
 198
 199   let JEJTVGB_pent_pro_concl =
 200     `!V E FF.
 201       convex_local_fan (V,E,FF) /\
 202       packing V /\
 203       V SUBSET ball_annulus /\
 204       CARD V = 5 /\
 205     (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w)) /\
 206     (?v0 w0.
 207        (!v w. {v,w} IN E /\ ~({v,w} = {v0,w0}) ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\
 208        {v0,w0} IN E /\
 209      &2 *h0 <= dist(v0,w0) /\ dist(v0,w0) <= sqrt8)
 210     ==>
 211     #0.616 <= tau_fun V E FF`;;
 212
 213   let JEJTVGB_quad_pro_concl =
 214     `!V E FF.
 215       convex_local_fan (V,E,FF) /\
 216       packing V /\
 217       V SUBSET ball_annulus /\
 218       CARD V = 4 /\
 219     (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w)) /\
 220     (?v0 w0.
 221        (!v w. {v,w} IN E /\ ~({v,w} = {v0,w0}) ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\
 222        {v0,w0} IN E /\
 223      &2 *h0 <= dist(v0,w0) /\ dist(v0,w0) <= sqrt8)
 224     ==>
 225     #0.477 <= tau_fun V E FF`;;
 226
 227   let JEJTVGB_quad_diag_concl =
 228     `!V E FF.
 229       convex_local_fan (V,E,FF) /\
 230       packing V /\
 231       V SUBSET ball_annulus /\
 232       CARD V = 4 /\
 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`;;
 236
 237   let JEJTVGB_concl =
 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
 240       list_mk_conj co;;
 241
 242   let JEJTVGB_assume_v39 =  new_definition (mk_eq (`JEJTVGB_assume_v39:bool`,JEJTVGB_concl));;
 243
 244   (* I'll use periodic functions to SCSs for now *)
 245
 246   let peropp = new_definition `peropp (f:num->A) k i = f (k - SUC(i MOD k))`;;
 247
 248   let peropp2 = new_definition `peropp2 (f:num->num->A) k i j = f (k - SUC(i MOD k)) (k - SUC(j MOD k))`;;
 249
 250   let peropp_periodic = prove_by_refinement(
 251     `!(f:num->A) k.      periodic (peropp f k) k`,
 252     (* {{{ proof *)
 253     [
 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])
 258     ]);;
 259   (* }}} *)
 260
 261   let scs_data = `(k:num,d:real,a,alpha,beta,b,J,lo,hi,str)`;;
 262
 263   let scs_exists =  MESON[]   `?(x: (
 264                                    (num) #
 265                                      (real) #
 266                                      (num->num -> real) #
 267                                      (num->num -> real) #
 268                                      (num-> num-> real) #
 269                                      (num -> num -> real) #
 270                                      (num -> num -> bool) #
 271                                      (num -> bool) #
 272                                      (num -> bool) #
 273                                      (num -> bool))). T`;;
 274
 275   let scs_v39 = REWRITE_RULE[] (new_type_definition "scs_v39" ("scs_v39", "dest_scs_v39") scs_exists);;
 276
 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)`;;
 279
 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)`;;
 284
 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)))`;;
 289
 290   let arcmax_v39 = new_definition `arcmax_v39 s (p1,p2) =
 291     arclength (&2) (&2) (scs_bm_v39 s p1 p2)`;;
 292
 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)`,
 296     (* {{{ proof *)
 297     [
 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])
 303     ]);;
 304   (* }}} *)
 305
 306
 307
 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`,
 310     (* {{{ proof *)
 311     [
 312       BY(REWRITE_TAC[scs_k_v39;scs_v39;Misc_defs_and_lemmas.part0])
 313     ]);;
 314   (* }}} *)
 315
 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`,
 318     (* {{{ proof *)
 319     [
 320       BY(REWRITE_TAC[scs_d_v39;scs_v39;Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.drop0;FST])
 321     ]);;
 322   (* }}} *)
 323
 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`,
 326     (* {{{ proof *)
 327     [
 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]))
 329     ]);;
 330   (* }}} *)
 331
 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`,
 334     (* {{{ proof *)
 335     [
 336       BY((REWRITE_TAC[scs_am_v39;scs_v39;Misc_defs_and_lemmas.part3;Misc_defs_and_lemmas.drop2;FST]))
 337     ]);;
 338   (* }}} *)
 339
 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`,
 342     (* {{{ proof *)
 343     [
 344       ((REWRITE_TAC[scs_bm_v39;scs_v39;Misc_defs_and_lemmas.part4;Misc_defs_and_lemmas.drop3;FST]))
 345     ]);;
 346   (* }}} *)
 347
 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`,
 350     (* {{{ proof *)
 351     [
 352       ((REWRITE_TAC[scs_b_v39;scs_v39;Misc_defs_and_lemmas.part5;Misc_defs_and_lemmas.drop3;FST]))
 353     ]);;
 354   (* }}} *)
 355
 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`,
 358     (* {{{ proof *)
 359     [
 360       ((REWRITE_TAC[scs_J_v39;scs_v39;Misc_defs_and_lemmas.part6;Misc_defs_and_lemmas.drop3;FST]))
 361     ]);;
 362   (* }}} *)
 363
 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`,
 366     (* {{{ proof *)
 367     [
 368       ((REWRITE_TAC[scs_lo_v39;scs_v39;Misc_defs_and_lemmas.part7;Misc_defs_and_lemmas.drop3;FST]))
 369     ]);;
 370   (* }}} *)
 371
 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`,
 374     (* {{{ proof *)
 375     [
 376       ((REWRITE_TAC[scs_hi_v39;scs_v39;Misc_defs_and_lemmas.part8;Misc_defs_and_lemmas.drop3;FST]))
 377     ]);;
 378   (* }}} *)
 379
 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`,
 382     (* {{{ proof *)
 383     [
 384       ((REWRITE_TAC[scs_str_v39;scs_v39;Misc_defs_and_lemmas.part7;Misc_defs_and_lemmas.drop3;FST]))
 385     ]);;
 386   (* }}} *)
 387
 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;
 393      scs_hi_v39_explicit;
 394      scs_str_v39_explicit];;
 395
 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)`;;
 397
 398   (* This doesn't specify the form of : symmetric?
 399      Let's make it symmetric periodic.  is_ear_v... *)
 400
 401   let is_scs_v39 = new_definition `is_scs_v39 s = (
 402     scs_d_v39 s < #0.9 /\
 403       3 <= scs_k_v39 s /\
 404       scs_k_v39 s <= 6 /\
 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)`;;
 427
 428   (*
 429   *)
 430
 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)`;;
 433
 434   let periodic_empty = prove_by_refinement(
 435     `!n. periodic {} n`,
 436     (* {{{ proof *)
 437     [
 438       REWRITE_TAC[Oxl_def.periodic];
 439       BY(ASM_MESON_TAC[NOT_IN_EMPTY;IN])
 440     ]);;
 441   (* }}} *)
 442
 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,{},{},{}))`,
 446     (* {{{ proof *)
 447     [
 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`])
 452     ]);;
 453   (* }}} *)
 454
 455   let is_ear_v39 = new_definition `is_ear_v39 s <=>
 456     is_scs_v39 s /\
 457     unadorned_v39 s /\
 458     scs_k_v39 s = 3 /\
 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))`;;
 464
 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)))))`;;
 473
 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)))`;;
 477
 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`,
 480     (* {{{ proof *)
 481     [
 482       REPEAT WEAKER_STRIP_TAC;
 483       ASM_REWRITE_TAC[dsv_v39;EMPTY_GSPEC;SUM_CLAUSES];
 484       BY(REAL_ARITH_TAC)
 485     ]);;
 486   (* }}} *)
 487
 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))`;;
 494
 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),{},{},{})`;;
 497
 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))`;;
 501
 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))`;;
 506
 507   (*
 508     let ASSOCD = new_definition` ASSOCD (a:A) hs (d:D) =
 509     if hs = [] then d else ASSOC a hs`;;
 510   *)
 511
 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`;;
 515
 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)`;;
 520
 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)`;;
 525
 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`;;
 528
 529   (* constant 0.467 corrected on 2013-06-03. *)
 530
 531   let s_init_list_v39 = new_definition `s_init_list_v39 =
 532     let upperbd = &6 in
 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
 545       ]`;;
 546
 547   let LENGTH_s_init_list = prove_by_refinement(
 548     `LENGTH s_init_list_v39 = 8`,
 549     (* {{{ proof *)
 550     [
 551       REWRITE_TAC[s_init_list_v39;LET_DEF;LET_END_DEF;LENGTH];
 552       BY(ARITH_TAC)
 553     ]);;
 554   (* }}} *)
 555
 556   (* terminal cases *)
 557
 558   let scs_6T1 =
 559     `mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (cstab)) (cs_adj 6 (&2) (&6))`;;
 560
 561   let scs_5T1 =
 562     `mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (cstab)) (cs_adj 5 (&2) (&6))`;;
 563
 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))`;;
 567
 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))`;;
 570
 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)`;;
 575
 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)`;;
 580   *)
 581
 582   let scs_4T4 =
 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)`;;
 586
 587   let scs_4T5 =
 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)`;;
 591
 592   (* deprecated 2013-06-17
 593      let terminal_tri_7720405539 = `mk_unadorned_v39
 594      3
 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)`;;
 598
 599      let terminal_tri_2739661360 = `mk_unadorned_v39
 600      3
 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)`;;
 604
 605      let terminal_tri_4922521904 = `mk_unadorned_v39
 606      3
 607      (#0.5518 / #2.0)
 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)`;;
 610
 611      let ear_stab = `mk_unadorned_v39
 612      3
 613      //  (#0.11 + #0.1 *(cstab - sqrt8))  corrected 2013-4-20, see check_completeness djz.
 614      (#0.11)
 615      (funlist_v39 [(0,2),cstab] (&2) 3)
 616      (funlist_v39 [(0,2),cstab] (&2*h0) 3)`;;
 617
 618      let terminal_ear_3603097872 = ear_cs;;
 619
 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)`;;
 624
 625   *)
 626
 627
 628   let scs_3T1 = (* ear_jnull =  *)
 629     `scs_v39 (3, #0.11,
 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),{},{},{})`;;
 635
 636   let scs_3T2 = (* terminal_std_tri_OMKYNLT_3336871894 =  *)
 637     `mk_unadorned_v39
 638       3
 639       (&0)
 640       (funlist_v39 [] (&2) 3)
 641       (funlist_v39 [] (&2) 3)`;;
 642
 643   (* 3 new additions 2013-06-04 3T3 3T4 3T5 *)
 644
 645   let scs_3T3 = (* terminal_tri_4010906068 =  *)
 646     `mk_unadorned_v39  3
 647       (#0.476)
 648       (funlist_v39 [] (&2*h0) 3)
 649       (funlist_v39 [] (cstab) 3)`;;
 650
 651   let scs_3T4 = (* terminal_tri_6833979866 =  *)
 652     `mk_unadorned_v39  3
 653       (#0.2759)
 654       (funlist_v39 [(0,1),(&2)] (&2*h0) 3)
 655       (funlist_v39 [(0,1),(&2 * h0)] (cstab) 3)`;;
 656
 657   let scs_3T5 = (* terminal_tri_5541487347 =  *)
 658     `mk_unadorned_v39  3
 659       (#0.103)
 660       (funlist_v39 [(0,1),(&2 * h0)] (&2) 3)
 661       (funlist_v39 [(0,1),(sqrt8)] (&2 * h0) 3)`;;
 662
 663   let scs_3T6 = (* terminal_tri_5026777310a =  *)
 664     `mk_unadorned_v39 3
 665       (#0.4348)
 666       (funlist_v39 [(0,1),sqrt8;(1,2),sqrt8] (&2) 3)
 667       (funlist_v39 [(0,1),cstab;(1,2),cstab] (&2*h0) 3)`;;
 668
 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)`;;
 673
 674   let terminal_cs = [
 675     scs_6T1;
 676     scs_5T1;
 677
 678     (* quad cases *)
 679     scs_4T1;
 680     scs_4T2;
 681     scs_4T3;
 682     scs_4T4;
 683     scs_4T5;
 684
 685     (* triangle *)
 686     scs_3T1;
 687     scs_3T2;
 688     scs_3T3;
 689     scs_3T4;
 690     scs_3T5;
 691     scs_3T6;
 692     scs_3T7];;
 693
 694   (* terminal_adhoc_quad_7697147739; *)
 695
 696   (* upper echelon cases *)
 697   (*
 698     terminal_tri_7720405539;
 699     terminal_tri_2739661360;
 700     scs_3T7;
 701     terminal_tri_4922521904;
 702   *)
 703
 704   (* J cases
 705      terminal_ear_3603097872;
 706      scs_3T1;
 707      terminal_tri_5405130650;
 708   *)
 709
 710   (* other triangles
 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;
 717   *)
 718
 719
 720
 721
 722   (* nonterminal cases *)
 723
 724   let ear_cs =
 725     `scs_v39 (3, #0.11,
 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,{},{},{})`;;
 731
 732   let terminal_tri_5405130650 = `scs_v39(
 733     3,
 734     #0.477 -  #0.11,
 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,{},{},{})`;;
 740
 741   (*
 742     let scs_terminal_v39 = new_definition (mk_eq (`scs_terminal_v39:(scs_v39)list`,(mk_flist terminal_cs)));;
 743
 744   *)
 745
 746
 747
 748
 749
 750   let ZITHLQN_concl =  `(!s vv. MEM s  s_init_list_v39 /\ vv IN
 751                            BBs_v39 s ==>
 752                            &0 <= taustar_v39 s vv)  ==> JEJTVGB_assume_v39`;;
 753
 754   (*
 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`,
 757   (* {{{ proof *)
 758     [
 759     rt[s_init_list_v39;set_of_list;JEJTVGB_assume_v39]
 760     st/r
 761     conj
 762     st/r
 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
 766     ]);;
 767   (* }}} *)
 768   *)
 769
 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)`;;
 772
 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)) }`;;
 775
 776   let BBindex_min_v39 = new_definition `BBindex_min_v39 s =
 777     min_num (IMAGE (BBindex_v39 s) (BBprime_v39 s))`;;
 778
 779   let BBprime2_v39 = new_definition `BBprime2_v39 s vv <=>
 780     BBprime_v39 s vv /\ BBindex_v39 s vv = BBindex_min_v39 s`;;
 781
 782   let MMs_v39 = new_definition `MMs_v39 s vv <=>
 783     BBprime2_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)`;;
 789
 790   let unadorned_MMs_concl = `!s.
 791     unadorned_v39 s ==> (MMs_v39 s = BBprime2_v39 s)`;;
 792
 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 = {})`;;
 795
 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 = {})`;;
 798
 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 = {})`;;
 801
 802   let EAPGLE_concl =  `(!s. MEM s s_init_list_v39 ==> MMs_v39 s = {}) ==> JEJTVGB_assume_v39`;;
 803
 804   let JKQEWGV1_concl = `!s vv. is_scs_v39 s /\ BBs_v39 s vv /\ taustar_v39 s vv < &0 /\
 805     3 < scs_k_v39 s ==>
 806     (sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
 807        (IMAGE (\i. (vv i,vv (SUC i))) (:num))  < pi)`;;
 808
 809   let JKQEWGV2_concl = `!s vv. is_scs_v39 s /\ BBs_v39 s vv /\ taustar_v39 s vv < &0 /\
 810     3 < scs_k_v39 s ==>
 811     (
 812       let V = IMAGE vv (:num) in
 813       let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
 814         ~circular V E)`;;
 815
 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 /\
 821           3 < scs_k_v39 s ==>
 822           (interior_angle1 (vec 0) FF v  < pi / &2 )))`;;
 823
 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`;;
 829
 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))`;;
 832
 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))`;;
 836
 837   (* DEPRECATED
 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
 841      let i' =  i MOD k in
 842      let j' = j MOD k 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))))`;;
 850
 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 [])`;;
 857   *)
 858
 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)))`;;
 865
 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)))`;;
 872
 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]
 878                        else [s]))))`
 879
 880   let transfer_v39 = new_definition `transfer_v39 s s' <=>
 881     (is_ear_v39 s ==> (s = s')) /\
 882     (is_scs_v39 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)
 889     `;;
 890
 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))))`;;
 898
 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))`;;
 905
 906   (* 0--(p-1) slice: *)
 907
 908   (*
 909     let torsor_slice_v39 = new_definition `torsor_slice_v39 s p =
 910     (
 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))))`;;
 916   *)
 917
 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)`;;
 922
 923
 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,{},{},{}))`;;
 935
 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)`;;
 939
 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) /\
 945           d' < #0.9 /\
 946           d'' < #0.9 /\
 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''))))`;;
 951
 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 = {})))`;;
 956
 957   (* added definitions 2013-06-17 *)
 958
 959   let xrr = new_definition `xrr y1 y2 y6 = &8 * (&1 - (y1 * y1 + y2*y2 - y6*y6)/(&2* y1 * y2))`;;
 960
 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)`;;
 965
 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)`;;
 970
 971   (* renamed from scs_is_basic *)
 972
 973
 974   let scs_generic = new_definition `scs_generic v <=>
 975     generic (IMAGE v (:num))
 976     (IMAGE (\i. {v i, v (SUC i)}) (:num))`;;
 977
 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)`;;
 980
 981   let scs_stab_diag_v39 = new_definition `scs_stab_diag_v39 s i j =
 982     (
 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'))`;;
 986
 987   let scs_basic = new_definition `scs_basic_v39 s <=>
 988     unadorned_v39 s /\ (!i j. scs_J_v39 s i j = F)`;;
 989
 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')
 996       ==> (s = s')`,
 997
 998     (* {{{ proof *)
 999     [
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];
1007       AP_TERM_TAC;
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]);
1011       BY(REWRITE_TAC[])
1012     ]);;
1013   (* }}} *)
1014
1015
1016   (* deprecate: only used in Ocbicby.basic_examples: *)
1017
1018   (*
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)`;;
1021   *)
1022
1023
1024   (*
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)))`;;
1032   *)
1033
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)))`;;
1041
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)`;;
1046
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)) }`;;
1049
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))`;;
1052
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))`;;
1055
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))
1058       `;;
1059
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))
1062       `;;
1063
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))
1066       `;;
1067
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))
1070       `;;
1071
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)`;;
1076
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)`;;
1081
1082   (* terminal cases *)
1083
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))`;;
1086
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))`;;
1089
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))`;;
1093
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))`;;
1096
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)`;;
1101
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)`;;
1106
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)`;;
1111
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),{},{},{})`;;
1119
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)`,
1124     (* {{{ proof *)
1125     [
1126       BY(REWRITE_TAC[mk_unadorned_v39;scs_3T1_PRELIM]);
1127     ]);;
1128   (* }}} *)
1129
1130   let scs_3T2 = (* terminal_std_tri_OMKYNLT_3336871894 =  *) new_definition
1131     `scs_3T2 = mk_unadorned_v39
1132     3
1133     (&0)
1134     (funlist_v39 [] (&2) 3)
1135     (funlist_v39 [] (&2) 3)`;;
1136
1137   let scs_3T3 = (* terminal_tri_4010906068 =  *) new_definition
1138     `scs_3T3 = mk_unadorned_v39  3
1139     (#0.476)
1140     (funlist_v39 [] (&2*h0) 3)
1141     (funlist_v39 [] (cstab) 3)`;;
1142
1143   let scs_3T4 = (* terminal_tri_6833979866 =  *) new_definition
1144     `scs_3T4 = mk_unadorned_v39  3
1145     (#0.2759)
1146     (funlist_v39 [(0,1),(&2)] (&2*h0) 3)
1147     (funlist_v39 [(0,1),(&2 * h0)] (cstab) 3)`;;
1148
1149   let scs_3T5 = (* terminal_tri_5541487347 =  *) new_definition
1150     `scs_3T5 = mk_unadorned_v39  3
1151     (#0.103)
1152     (funlist_v39 [(0,1),(&2 * h0)] (&2) 3)
1153     (funlist_v39 [(0,1),(sqrt8)] (&2 * h0) 3)`;;
1154
1155   let scs_3T6 = (* terminal_tri_5026777310a =  *) new_definition
1156     `scs_3T6' = mk_unadorned_v39 3
1157     (#0.4348)
1158     (funlist_v39 [(0,1),sqrt8;(1,2),sqrt8] (&2) 3)
1159     (funlist_v39 [(0,1),cstab;(1,2),cstab] (&2*h0) 3)`;;
1160
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)`;;
1165
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))`;;
1168
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)`;;
1173
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)`;;
1178
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)`;;
1183
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)`;;
1188
1189   (*
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)`;;
1194
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)`;;
1199
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)`;;
1204
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)`;;
1209   *)
1210
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)`;;
1215
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)`;;
1220
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)`;;
1225
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)`;;
1230
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)`;;
1235
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)`;;
1240
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)`;;
1245
1246
1247   (* Some conclusions *)
1248
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
1252        MMs_v39 s vv /\
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 ==>
1256          BBs_v39 s' vv')`;;
1257
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
1263        MMs_v39 s vv /\
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'')`;;
1268
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
1274        MMs_v39 s vv /\
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)`;;
1279
1280   (* AZGJNZO *)
1281
1282
1283   let FZIOTEF_REFL = prove_by_refinement(
1284     `!S.  (!s. s IN S ==> is_scs_v39 s) ==> scs_arrow_v39 S S`,
1285     (* {{{ proof *)
1286     [
1287       REWRITE_TAC[scs_arrow_v39];
1288       BY(MESON_TAC[])
1289     ]);;
1290   (* }}} *)
1291
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`,
1295     (* {{{ proof *)
1296     [
1297       REWRITE_TAC[scs_arrow_v39];
1298       REPEAT WEAKER_STRIP_TAC;
1299       ASM_REWRITE_TAC[];
1300       BY(ASM_MESON_TAC[])
1301     ]);;
1302   (* }}} *)
1303
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}`;;
1308
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}`;;
1315
1316   let UAGHHBM_concl = `!s i j c .
1317     (let k = scs_k_v39 s in
1318        (is_scs_v39 s /\
1319           scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
1320           3 < k /\
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))
1325           ==>
1326           scs_arrow_v39 {s} (set_of_list (subdiv_v39 s i j c))))`;;
1327
1328   let YXIONXL1_concl = `!s t.
1329     is_scs_v39 s /\
1330     transfer_v39 s t ==> scs_arrow_v39 {s} {t}`;;
1331
1332   let YXIONXL2_concl = `!s.
1333     is_scs_v39 s ==> scs_arrow_v39 {s} {scs_opp_v39 s}`;;
1334
1335   let YXIONXL3_concl = `!s i.
1336     is_scs_v39 s ==> scs_arrow_v39 {s} {scs_prop_equ_v39 s i}`;;
1337
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''}`;;
1340
1341   let HXHYTIJ_concl = `!s vv ww.
1342     is_scs_v39 s /\
1343     BBprime2_v39 s vv /\
1344     BBs_v39 s ww ==>
1345     (taustar_v39 s vv < taustar_v39 s ww  \/
1346        BBindex_v39 s vv <= BBindex_v39 s ww)`;;
1347
1348   let ODXLSTCv2_concl = `!s k w l.
1349     is_scs_v39 s /\
1350     MMs_v39 s w /\
1351     k = scs_k_v39 s /\
1352     3 < k /\
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)) /\
1357     (!V E v.
1358        V = IMAGE w (:num) /\
1359         E = IMAGE (\i. {w i, w (SUC i)}) (:num) ==>
1360         ~(lunar (v,(w l)) V E )) ==> F`;;
1361
1362   let IMJXPHRv2_concl = `!s k w l.
1363     is_scs_v39 s /\
1364     MMs_v39 s w /\
1365     azim (vec 0) (w l) (w (SUC l)) (w (l + (scs_k_v39 s - 1))  ) = pi /\
1366     k = scs_k_v39 s /\
1367     3 < k /\
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)) }/\
1370
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)) /\
1375     (!V E v.
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)))))`;;
1381
1382   let NUXCOEAv2_concl = `!s k w l j.
1383     is_scs_v39 s /\
1384     MMs_v39 s w /\
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)) }/\
1388     k = scs_k_v39 s /\
1389     3 < k /\
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)) /\
1396     (!V E v.
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)))))`;;
1402
1403
1404   (*
1405     let deform_ODXLSTC_concl = `!s k l.
1406     is_scs_v39 s /\
1407     ~(MMs_v39 s = {}) /\
1408     k = scs_k_v39 s /\
1409     3 < k /\
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)
1414     ==>
1415     scs_arrow_v39 {s}
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) }))
1423     `;;
1424
1425     let deform_IMJXPHR_concl = `!s k p0 p1 p2.
1426     is_scs_v39 s /\
1427     k = scs_k_v39 s /\
1428     3 < k /\
1429     p1 = p0 + 1 /\
1430     p2 = p0 + 2 /\
1431     scs_str_v39 s p1 /\
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)) ==>
1440     scs_arrow_v39 {s}
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) }))`;;
1448
1449     let deform_NUXCOEA_concl = `!s k p0 p1 p2 p'.
1450     is_scs_v39 s /\
1451     k = scs_k_v39 s /\
1452     3 < k /\
1453     p1 = p0 + 1 /\
1454     p2 = p0 + 2 /\
1455     scs_str_v39 s p1 /\
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'')) ==>
1463     scs_arrow_v39 {s}
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) })`;;
1468
1469     let deform_2065952723_A1_single = `!s k p1 p2 p'.
1470     is_scs_v39 s /\
1471     k = scs_k_v39 s /\
1472     p2 = p1 + 1 /\
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'')) ==>
1484     scs_arrow_v39 {s}
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))}
1491     UNION
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) })
1496     UNION
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) }))`;;
1501   *)
1502
1503
1504   (* new material 2013-06-17 *)
1505
1506
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)`;;
1510
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'`;;
1515
1516   (*
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)`;;
1529
1530   (* some other continuities might be needed *)
1531
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`;;
1541   *)
1542
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)`;;
1555
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`;;
1565
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 /\
1578         ?t. &0 < t /\
1579         t % ((v3- v0) cross (v1- v0)) = ( s % ((v1 - v0) cross (v2 - v0))))`;;
1580
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`;;
1589
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`;;
1598
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))`;;
1602
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`;;
1606
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})`;;
1609
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)  ==>
1616     v IN MMs_v39 s'`;;
1617
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)`;;
1624
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'}`;;
1630
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`;;
1634
1635   let AXJRPNC_concl = `!s (v:num->real^3) i j.
1636     is_scs_v39 s /\ scs_basic_v39 s /\
1637     MMs_v39 s v /\
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))`;;
1642
1643   let RRCWNSJ_concl = `!s (v:num->real^3).
1644     is_scs_v39 s /\ scs_basic_v39 s /\ 3 < scs_k_v39 s /\
1645     MMs_v39 s v /\
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) ==>
1649     scs_generic v`;;
1650
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)`;;
1658
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`;;
1667
1668
1669   (* 3 < k, aij < bij  *)
1670
1671   let CQAOQLR_concl =
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)`;;
1678
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
1687     ==>
1688         (!j. ~(j IN scs_M s ) ==>   dist(v j , v(j+1)) = &2)`;;
1689
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) /\
1695            p' + q = p + q' /\
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'}))`;;
1700
1701   let PEDSLGV1_concl = `!v i j.
1702     v IN MMs_v39 scs_6I1 /\
1703     scs_diag 6 i j /\
1704     dist(v i,v j) <= cstab ==>
1705     v IN MMs_v39 (scs_stab_diag_v39 scs_6I1 i j)`;;
1706
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)`;;
1711
1712   let AQICLXA_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 2 } { scs_5M1, scs_3M1 }`;;
1713
1714   let FUNOUYH_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 3 } {scs_4M2 }`;;
1715
1716   let OEHDBEN_concl = `scs_arrow_v39 { scs_6I1 } { scs_6T1, scs_5M1, scs_4M2, scs_3T1 }`;;
1717
1718   let OTMTOTJ1_concl = `scs_arrow_v39 { scs_5I1 } { scs_stab_diag_v39 scs_5I1 0 2 , scs_5M2 }`;;
1719
1720   let OTMTOTJ2_concl = `scs_arrow_v39 { scs_5I2 } { scs_stab_diag_v39 scs_5I2 0 2 , scs_5M2 }`;;
1721
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 }`;;
1725
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 }`;;
1728
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 }`;;
1732
1733   let CNICGSF1_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_5I1 0 2 }
1734     {scs_4M2, scs_3M1 }`;;
1735
1736   let CNICGSF2_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_5I2 0 2 }
1737     {scs_4M3', scs_3T1 }`;;
1738
1739   let CNICGSF3_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_5M1 0 2 }
1740     {scs_4M2, scs_3T4 }`;;
1741
1742   let CNICGSF4_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_5M1 0 3 }
1743     {scs_4M4', scs_3M1 }`;;
1744
1745   let CNICGSF5_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_5M1 2 4 }
1746     {scs_4M5', scs_3M1 }`;;
1747
1748   let ARDBZYE_concl = `scs_arrow_v39 { scs_4I2 } { scs_4T1, scs_4T2 }`;;
1749
1750   let FYSSVEV_concl = `scs_arrow_v39 { scs_4I1 } {scs_4I2, scs_stab_diag_v39 scs_4I1 0 2 }`;;
1751
1752   let AUEAHEH_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_4I1 0 2 } { scs_3M1 }`;;
1753
1754   let ZNLLLDL_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_4I3 0 2 } { scs_4T4 }`;;
1755
1756   let VQFYMZY_concl = `scs_arrow_v39 { scs_4I3 } { scs_4T4, scs_4M6' }`;;
1757
1758   (* let CNFNTYP_concl = `scs_arrow_v39 { scs_4M1 } { scs_4M2, scs_4M6' }`;; *)
1759
1760   let BNAWVNH_concl = `scs_arrow_v39 { scs_4M2 } { scs_3M1, scs_3T4, scs_4M6' }`;;
1761
1762   let RAWZDIB_concl = `scs_arrow_v39 { scs_4M3' } { scs_3T1, scs_3T6', scs_4M6' }`;;
1763
1764   let MFKLVDK_concl = `scs_arrow_v39 { scs_4M4' } { scs_3M1, scs_3T4, scs_3T3, scs_4M7 }`;;
1765
1766   let RYPDIXT_concl = `scs_arrow_v39 { scs_4M5' } { scs_3T4, scs_4M8 }`;;
1767
1768   let GSXRFWM_concl = `!s v.
1769     is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s ==> scs_generic v`;;
1770
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`;;
1774
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 `;;
1779
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`;;
1787
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)`;;
1795
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))`;;
1803
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`;;
1811
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)) /\
1817     scs_is_str s v p
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))`;;
1819
1820 (*
1821
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)))`;;
1828
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)))`;;
1835
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))`;;
1843
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))`;;
1850
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`;;
1861
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)`;;
1868 *)
1869
1870   let NWDGKXH_concl = `scs_arrow_v39 {scs_4M6'} {scs_4T3,scs_4T5}`;;
1871
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'}`;;
1875
1876   let YOBIMPP_concl = ` scs_arrow_v39 {scs_4M7} {scs_3M1,scs_3T3,scs_3T4,scs_4M6'}`;;
1877
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}`;;
1881
1882 (*
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}`;;
1886 *)
1887
1888   let MIQMCSN_concl = `scs_arrow_v39 {scs_4M8} {scs_4M6',scs_3T7,scs_3T4}`;;
1889
1890   let LFLACKU_concl = `scs_arrow_v39 {scs_3T1} {scs_3T2,scs_3T5}`;;
1891
1892   let CUXVZOZ_concl = `main_nonlinear_terminal_v11 ==>
1893     (!s FF k p1 v.
1894        FF = IMAGE (\i. (v i,v (SUC i))) (:num) /\
1895         is_scs_v39 s /\
1896         k = scs_k_v39 s /\
1897         3 < k /\
1898         MMs_v39 s v /\
1899         scs_basic_v39 s /\
1900         scs_generic v /\
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)`;;
1911
1912   let CJBDXXN_concl = `main_nonlinear_terminal_v11 ==>
1913     (!s FF k p1 v.
1914        FF = IMAGE (\i. (v i,v (SUC i))) (:num) /\
1915         is_scs_v39 s /\
1916         k = scs_k_v39 s /\
1917         3 < k /\
1918         MMs_v39 s v /\
1919         scs_basic_v39 s /\
1920         scs_generic v /\
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)`;;
1931
1932   let YRTAFYH_concl =
1933     `!s i j.
1934       is_scs_v39 s /\
1935       scs_basic_v39 s /\
1936       3 < scs_k_v39 s /\
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)
1940       `;;
1941
1942   let BKOSSGE_concl =
1943     `scs_arrow_v39 {scs_3M1} {scs_3T1,scs_3T5}`;;
1944
1945 end;;
1946
1947
1948
1949