(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(* Section: Conclusions                                                       *)
(* Chapter: Local Fan                                                         *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2013-02-26                                                           *)
(* ========================================================================== *)

(*
remaining conclusions from appendix to Local Fan chapter

svn 3270 contains deprecated terminal SCS cases
*)


module Appendix = struct


  open Hales_tactic;;



  (* Proved in Lunar_deform.MHAEYJN *)

  let MHAEYJN_concl = 
    `!a b V E FF f v w u.
      convex_local_fan (V,E,FF) /\
      lunar (v,w) V E /\
      deformation f V (a,b) /\
      interior_angle1 (vec 0) FF v < pi /\
      u IN V /\
      ~(u = v) /\
      ~(u = w) /\
      (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u') /\
      (!t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u})
    ==> (?e. &0 < e /\
           (!t. --e < t /\ t < e
            ==> convex_local_fan
            (IMAGE (\v. f v t) V,
             IMAGE (IMAGE (\v. f v t)) E,
             IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\
            lunar (v,w) (IMAGE (\v. f v t) V)
            (IMAGE (IMAGE (\v. f v t)) E)))`;;

  let ZLZTHIC_concl = 
    `!a b V E FF f.
      convex_local_fan (V,E,FF) /\
      generic V E /\
      deformation f V (a,b) /\
      (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==>
	  interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi)
    ==> (?e. &0 < e /\
           (!t. --e < t /\ t < e
            ==> convex_local_fan
            (IMAGE (\v. f v t) V,
             IMAGE (IMAGE (\v. f v t)) E,
             IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\
            generic (IMAGE (\v. f v t) V)
            (IMAGE (IMAGE (\v. f v t)) E)))`;;


  let VPWSHTO_concl = 
    `!v x u w w1. 
      {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)
    /\ norm(v-x)= &2
    /\ norm(x-u)= &2
    /\ norm(u-w)= &2
    /\ norm(w-w1)= &2
    /\ norm(w1-v)= &2
    ==> ?v1 u1 w2. u1 IN {v,x,u,w,w1}
    /\ u1 IN {v,x,u,w,w1} /\ w2 IN {v,x,u,w,w1}/\ ~(v1=u1)/\ ~(u1=w2) /\ ~(v1=w2) /\
    &2 < norm(v1-u1) /\ &2 < norm(v1 - w2)
    /\ norm(v1-u1) <= &1 + sqrt(&5)/\ norm(v1-w2)<= &1 + sqrt(&5)`;;

  
let arc1553_v39 = new_definition `arc1553_v39 = arclength (&2) (&2) (sqrt(#15.53))`;;

  
let cstab=new_definition ` cstab= #3.01`;;
  
let rho_fun = new_definition `rho_fun y =  &1 + (inv (&2 * h0 - &2)) * (inv pi) * sol0 * (y - &2)`;;
  
let rho_rho_fun = 
prove_by_refinement(
    `!y. rho_fun y = rho y`,

    (* {{{ proof *)
    [
      REWRITE_TAC[Sphere.rho;rho_fun;Sphere.const1;Sphere.ly;Sphere.interp];
      REWRITE_TAC[GSYM Nonlinear_lemma.sol0_EQ_sol_y;Sphere.h0];
      REWRITE_TAC[arith `a + b = a + c <=> c = b`];
      GEN_TAC;
      MATCH_MP_TAC (arith `(sol0/pi)*(&1 - a) = (sol0/pi)*(c*e) ==> sol0/pi - sol0/pi * a = c * inv pi * sol0 * e`);
      AP_TERM_TAC;
      BY(REAL_ARITH_TAC)
    ]);;
  (* }}} *)

  
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)`;;
  
let tau3 = new_definition `tau3 (v1:real^3) v2 v3 = 
    rho (norm v1) * dihV (vec 0) v1 v2 v3 + rho(norm v2) * dihV (vec 0) v2 v3 v1 +
      rho(norm v3) * dihV (vec 0) v3 v1 v2 - (pi + sol0)`;;
  (*
    let standard = new_definition
    ` standard v w <=> &2 <= norm(v-w) /\  norm (v-w) <= &2 *h0 `;;

    let protracted = new_definition
    ` protracted v w <=> &2 * h0 <= norm(v-w) /\  norm (v-w) <= sqrt (&8) `;;

    let diagonal0 = new_definition
    ` (diagonal0 (E:(real^3->bool)->bool) (v:real^3) (w:real^3))  <=> ~(v = w) /\ ~({v,w} IN E) `;;

    let diagonal1 = new_definition
    ` diagonal1 (V,E)  <=> !v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E)
    ==> &2 * h0 <= norm(v-w) `;;

    let main_estimate= new_definition
    ` main_estimate(V,E,f) <=>
    convex_local_fan(V,E,f) /\
    packing V /\
    V SUBSET ball_annulus /\
    diagonal1(V,E) /\
    CARD E= CARD f /\
    3<= CARD E /\
    CARD E <= 6`;;
  *)

  
let torsor = new_definition
    ` 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)
    /\ s HAS_SIZE k`;;
  
let tgt = new_definition `tgt = #1.541`;;
  
let d_tame = new_definition `d_tame n = 
    if n = 3 then &0 else 
      if n = 4 then #0.206 else
	if n = 5 then #0.4819 else 
	  if n = 6 then #0.712 else tgt`;;
  

  (* rename d_tame2 -> tame_table_d, for compatibility with the rest of the project. *)

  (*
    let d_tame2 = new_definition `d_tame2 r s = 
    if (r + 2 * s <= 3) then &0
    else 
    #0.103 * (&2 - &s) + #0.2759 * (&r + &2 * &s - &4)`;;

    let tame_table_d_tame2 = prove_by_refinement(
    `!r s. tame_table_d r s = if (r + 2 * s <= 3) then &0
    else 
    #0.103 * (&2 - &s) + #0.2759 * (&r + &2 * &s - &4)`,
  (* {{{ proof *)
    [
    REWRITE_TAC[Sphere.tame_table_d];
    REPEAT WEAKER_STRIP_TAC;
    REWRITE_TAC[arith `r + 2 * s > 3 <=> ~(r + 2 * s <= 3)`];
    COND_CASES_TAC;
    BY(ASM_REWRITE_TAC[]);
    BY(REAL_ARITH_TAC)
    ]);;
  (* }}} *)
  *)

  let JEJTVGB_std_concl = 
    `!V E FF. 
      convex_local_fan (V,E,FF) /\
      packing V /\
      V SUBSET ball_annulus /\
      4 <= CARD V /\ CARD V <= 6 /\
      (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w)) /\
      (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) ==>
      d_tame (CARD V) <= tau_fun V E FF`;;

  let JEJTVGB_std3_concl = 
    `!v1 v2 v3. 
    &2 <= norm v1 /\
    &2 <= norm v2 /\
    &2 <= norm v3 /\
    norm v1 <= &2 * h0 /\
    norm v2 <= &2 * h0 /\
    norm v3 <= &2 * h0 /\
    &2 <= dist(v1,v2) /\
    &2 <= dist(v1,v3) /\
    &2 <= dist(v2,v3) /\
    dist(v1,v2) <= &2 * h0 /\
    dist(v1,v3) <= &2 * h0 /\
    dist(v2,v3) <= &2 * h0 ==>
    &0 <= tau3 v1 v2 v3`;;

  let JEJTVGB_pent_diag_concl = 
    `!V E FF. 
      convex_local_fan (V,E,FF) /\
      packing V /\
      V SUBSET ball_annulus /\
      CARD V = 5 /\
    (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w)) /\
    (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) ==>
    #0.616 <= tau_fun V E FF`;;

  let JEJTVGB_pent_pro_concl = 
    `!V E FF. 
      convex_local_fan (V,E,FF) /\
      packing V /\
      V SUBSET ball_annulus /\
      CARD V = 5 /\ 
    (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &2 * h0 <= dist(v,w)) /\
    (?v0 w0.
       (!v w. {v,w} IN E /\ ~({v,w} = {v0,w0}) ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\
       {v0,w0} IN E /\
     &2 *h0 <= dist(v0,w0) /\ dist(v0,w0) <= sqrt8)
    ==>
    #0.616 <= tau_fun V E FF`;;

  let JEJTVGB_quad_pro_concl = 
    `!V E FF. 
      convex_local_fan (V,E,FF) /\
      packing V /\
      V SUBSET ball_annulus /\
      CARD V = 4 /\ 
    (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> sqrt8 <= dist(v,w)) /\
    (?v0 w0.
       (!v w. {v,w} IN E /\ ~({v,w} = {v0,w0}) ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) /\
       {v0,w0} IN E /\
     &2 *h0 <= dist(v0,w0) /\ dist(v0,w0) <= sqrt8)
    ==>
    #0.477 <= tau_fun V E FF`;;

  let JEJTVGB_quad_diag_concl = 
    `!V E FF. 
      convex_local_fan (V,E,FF) /\
      packing V /\
      V SUBSET ball_annulus /\
      CARD V = 4 /\
    (!v w. ~(v = w) /\ v IN V /\ w IN V /\ ~({v,w} IN E) ==> &3 <= dist(v,w)) /\
    (!v w. {v,w} IN E ==> &2 <= dist(v,w) /\ dist(v,w) <= &2 * h0) ==>
    #0.467 <= tau_fun V E FF`;;

  let JEJTVGB_concl = 
    let co = [JEJTVGB_std_concl;JEJTVGB_std3_concl;JEJTVGB_pent_diag_concl;JEJTVGB_pent_pro_concl;
	      JEJTVGB_quad_pro_concl;JEJTVGB_quad_diag_concl] in
      list_mk_conj co;;

  
let JEJTVGB_assume_v39 =  new_definition (mk_eq (`JEJTVGB_assume_v39:bool`,JEJTVGB_concl));;
  (* I'll use periodic functions to SCSs for now *)

  
let peropp = new_definition `peropp (f:num->A) k i = f (k - SUC(i MOD k))`;;
  
let peropp2 = new_definition `peropp2 (f:num->num->A) k i j = f (k - SUC(i MOD k)) (k - SUC(j MOD k))`;;
  
let peropp_periodic = 
prove_by_refinement(
    `!(f:num->A) k.      periodic (peropp f k) k`,

    (* {{{ proof *)
    [
      REPEAT WEAKER_STRIP_TAC;
      REWRITE_TAC[Oxl_def.periodic;peropp];
      ONCE_REWRITE_TAC[arith `i + k = 1 * k + i`];
      BY(REWRITE_TAC[MOD_MULT_ADD])
    ]);;
  (* }}} *)

  let scs_data = `(k:num,d:real,a,alpha,beta,b,J,lo,hi,str)`;;

  let scs_exists =  MESON[]   `?(x: ( 
				   (num) #
				     (real) #
				     (num->num -> real) #
				     (num->num -> real) #
				     (num-> num-> real) #
				     (num -> num -> real) #
				     (num -> num -> bool) #
				     (num -> bool) #
				     (num -> bool) #
				     (num -> bool))). T`;;

  let scs_v39 = REWRITE_RULE[] (new_type_definition "scs_v39" ("scs_v39", "dest_scs_v39") scs_exists);;

  
let scs_k_v39 = new_definition `scs_k_v39 s = part0 (dest_scs_v39 s)`;;
  
let scs_d_v39 = new_definition `scs_d_v39 s = part1 (dest_scs_v39 s)`;;
  
let scs_a_v39 = new_definition `scs_a_v39 s = part2 (dest_scs_v39 s)`;;
  
let scs_am_v39 = new_definition `scs_am_v39 s = part3 (dest_scs_v39 s)`;;
  
let scs_bm_v39 = new_definition `scs_bm_v39 s = part4 (dest_scs_v39 s)`;;
  
let scs_b_v39 = new_definition `scs_b_v39 s = part5 (dest_scs_v39 s)`;;
  
let scs_J_v39 = new_definition `scs_J_v39 s = part6 (dest_scs_v39 s)`;;
  
let scs_lo_v39 = new_definition `scs_lo_v39 s = part7 (dest_scs_v39 s)`;;
  
let scs_hi_v39 = new_definition `scs_hi_v39 s = part8 (dest_scs_v39 s)`;;
  
let scs_str_v39 = new_definition `scs_str_v39 s = SND(drop3(drop3 (dest_scs_v39 s)))`;;
  
let arcmax_v39 = new_definition `arcmax_v39 s (p1,p2) = 
    arclength (&2) (&2) (scs_bm_v39 s p1 p2)`;;
  
let scs_components = 
prove_by_refinement(
    `!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,
			   scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s)`,

    (* {{{ proof *)
    [
      REWRITE_TAC[Wrgcvdr_cizmrrh.PAIR_EQ2;scs_k_v39;scs_d_v39;scs_a_v39;];
      REWRITE_TAC[scs_am_v39;scs_bm_v39;scs_b_v39;];
      REWRITE_TAC[scs_J_v39;scs_hi_v39;scs_lo_v39;];
      REWRITE_TAC[scs_str_v39];
      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])
    ]);;
  (* }}} *)



  
let scs_k_v39_explicit = 
prove_by_refinement(
    `!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`,

    (* {{{ proof *)
    [
      BY(REWRITE_TAC[scs_k_v39;scs_v39;Misc_defs_and_lemmas.part0])
    ]);;
  (* }}} *)

  
let scs_d_v39_explicit = 
prove_by_refinement(
    `!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`,

    (* {{{ proof *)
    [
      BY(REWRITE_TAC[scs_d_v39;scs_v39;Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.drop0;FST])
    ]);;
  (* }}} *)

  
let scs_a_v39_explicit = 
prove_by_refinement(
    `!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`,

    (* {{{ proof *)
    [
      BY((REWRITE_TAC[scs_a_v39;scs_v39;Misc_defs_and_lemmas.part2;Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.drop1;FST]))
    ]);;
  (* }}} *)

  
let scs_am_v39_explicit = 
prove_by_refinement(
    `!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`,

    (* {{{ proof *)
    [
      BY((REWRITE_TAC[scs_am_v39;scs_v39;Misc_defs_and_lemmas.part3;Misc_defs_and_lemmas.drop2;FST]))
    ]);;
  (* }}} *)

  
let scs_bm_v39_explicit = 
prove_by_refinement(
    `!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`,

    (* {{{ proof *)
    [
      ((REWRITE_TAC[scs_bm_v39;scs_v39;Misc_defs_and_lemmas.part4;Misc_defs_and_lemmas.drop3;FST]))
    ]);;
  (* }}} *)

  
let scs_b_v39_explicit = 
prove_by_refinement(
    `!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`,

    (* {{{ proof *)
    [
      ((REWRITE_TAC[scs_b_v39;scs_v39;Misc_defs_and_lemmas.part5;Misc_defs_and_lemmas.drop3;FST]))
    ]);;
  (* }}} *)

  
let scs_J_v39_explicit = 
prove_by_refinement(
    `!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`,

    (* {{{ proof *)
    [
      ((REWRITE_TAC[scs_J_v39;scs_v39;Misc_defs_and_lemmas.part6;Misc_defs_and_lemmas.drop3;FST]))
    ]);;
  (* }}} *)

  
let scs_lo_v39_explicit = 
prove_by_refinement(
    `!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`,

    (* {{{ proof *)
    [
      ((REWRITE_TAC[scs_lo_v39;scs_v39;Misc_defs_and_lemmas.part7;Misc_defs_and_lemmas.drop3;FST]))
    ]);;
  (* }}} *)

  
let scs_hi_v39_explicit = 
prove_by_refinement(
    `!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`,

    (* {{{ proof *)
    [
      ((REWRITE_TAC[scs_hi_v39;scs_v39;Misc_defs_and_lemmas.part8;Misc_defs_and_lemmas.drop3;FST]))
    ]);;
  (* }}} *)

  
let scs_str_v39_explicit = 
prove_by_refinement(
    `!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`,

    (* {{{ proof *)
    [
      ((REWRITE_TAC[scs_str_v39;scs_v39;Misc_defs_and_lemmas.part7;Misc_defs_and_lemmas.drop3;FST]))
    ]);;
  (* }}} *)

  let scs_v39_explicit = end_itlist CONJ 
    [scs_k_v39_explicit;scs_d_v39_explicit;
     scs_a_v39_explicit;scs_am_v39_explicit;
     scs_b_v39_explicit;scs_bm_v39_explicit;
     scs_J_v39_explicit;scs_lo_v39_explicit;
     scs_hi_v39_explicit;
     scs_str_v39_explicit];;

  
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)`;;
  (* This doesn't specify the form of : symmetric?
     Let's make it symmetric periodic.  is_ear_v... *)

  
let is_scs_v39 = new_definition `is_scs_v39 s = (
    scs_d_v39 s < #0.9 /\
      3 <= scs_k_v39 s /\
      scs_k_v39 s <= 6 /\
      periodic (scs_lo_v39 s) (scs_k_v39 s) /\
      periodic (scs_hi_v39 s) (scs_k_v39 s) /\
      periodic (scs_str_v39 s) (scs_k_v39 s) /\
      periodic (scs_str_v39 s) (scs_k_v39 s) /\
      periodic2 (scs_a_v39 s) (scs_k_v39 s) /\
      periodic2 (scs_am_v39 s) (scs_k_v39 s) /\
      periodic2 (scs_bm_v39 s) (scs_k_v39 s) /\
      periodic2 (scs_b_v39 s) (scs_k_v39 s) /\
      periodic2 (scs_J_v39 s) (scs_k_v39 s) /\
      (!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 /\ 
	   scs_bm_v39 s i j = scs_bm_v39 s j i /\ scs_b_v39 s i j = scs_b_v39 s j i /\
	   scs_J_v39 s i j = scs_J_v39 s j i)) /\
      (!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 /\ 
	 scs_bm_v39 s i j <= scs_b_v39 s i j) /\
      (!i. scs_a_v39 s i i = &0) /\
      (!i j. (i < scs_k_v39 s) /\ (j < scs_k_v39 s) /\ ~(i = j) ==> &2 <= scs_a_v39 s i j) /\
      (!i. (scs_k_v39 s = 3) ==> (scs_b_v39 s i (SUC i) < &4)) /\
      (!i. (3 < scs_k_v39 s) ==> (scs_b_v39 s i (SUC i) <= cstab)) /\
      (!i j. scs_J_v39 s i j ==> ((j MOD scs_k_v39 s = (SUC i) MOD scs_k_v39 s) \/
				    ((i MOD scs_k_v39 s = (SUC j) MOD scs_k_v39 s)))) /\
      (!i j. scs_J_v39 s i j ==> scs_a_v39 s i j = sqrt8 /\ scs_b_v39 s i j = cstab) /\ 
      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)`;;
  (*
  *)

  
let unadorned_v39 = new_definition `unadorned_v39 s = 
    (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)`;;
  
let periodic_empty = 
prove_by_refinement(
    `!n. periodic {} n`,

    (* {{{ proof *)
    [
      REWRITE_TAC[Oxl_def.periodic];
      BY(ASM_MESON_TAC[NOT_IN_EMPTY;IN])
    ]);;
  (* }}} *)

  
let scs_unadorned = 
prove_by_refinement(
    `!s. is_scs_v39 s ==>
      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,{},{},{}))`,

    (* {{{ proof *)
    [
      REWRITE_TAC[is_scs_v39;scs_v39_explicit];
      REPEAT WEAKER_STRIP_TAC;
      ASM_REWRITE_TAC[arith `x <= x`;periodic_empty];
      BY(ASM_MESON_TAC[arith `x <= y /\ y <= z ==> x <= z`])
    ]);;
  (* }}} *)

  
let is_ear_v39 = new_definition `is_ear_v39 s <=> 
    is_scs_v39 s /\
    unadorned_v39 s /\
    scs_k_v39 s = 3 /\
      scs_d_v39 s = #0.11 /\
      (!i. scs_b_v39 s i i = &0) /\
      (?i. {i | i < 3 /\ scs_J_v39 s i (SUC i)} = {i} /\
	  scs_a_v39 s i (SUC i) = sqrt8 /\ scs_b_v39 s i (SUC i) = cstab /\
	  (!j. j < 3 /\ ~(j = i) ==> scs_a_v39 s j (SUC j) = &2 /\ scs_b_v39 s j (SUC j) = &2 * h0))`;;
  
  
let BBs_v39 = new_definition `BBs_v39 s vv =
    (let V = IMAGE vv (:num) in
     let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
     let FF = IMAGE (\i. (vv i,vv (SUC i))) (:num) in
       (V SUBSET ball_annulus /\
	  periodic vv (scs_k_v39 s) /\
	  (!i j. scs_a_v39 s i j <= dist(vv i,vv j) /\ dist(vv i,vv j) <= scs_b_v39 s i j) /\ 
	  (scs_k_v39 s <= 3  \/ (convex_local_fan (V,E,FF)))))`;;
  
let dsv_v39 = new_definition `dsv_v39 s (vv:num->real^3) = 
    scs_d_v39 s + #0.1 * (if (is_ear_v39 s) then &1 else -- &1) * 
      sum {i | i < scs_k_v39 s /\ scs_J_v39 s i (SUC i)} (\i. cstab - dist(vv i,vv (SUC i)))`;;
  
let dsv_J_empty = 
prove_by_refinement(
    `!s vv. scs_J_v39 s = (\i j. F) ==> dsv_v39 s vv = scs_d_v39 s`,

    (* {{{ proof *)
    [
      REPEAT WEAKER_STRIP_TAC;
      ASM_REWRITE_TAC[dsv_v39;EMPTY_GSPEC;SUM_CLAUSES];
      BY(REAL_ARITH_TAC)
    ]);;
  (* }}} *)

  
let taustar_v39 = new_definition `taustar_v39 s vv = 
    (let V = IMAGE vv (:num) in
     let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
     let FF = IMAGE (\i. (vv i,vv (SUC i))) (:num) in
       (if (scs_k_v39 s <= 3) then tau3 (vv 0) (vv 1) (vv 2) - dsv_v39 s vv
	else tau_fun V E FF - dsv_v39 s vv))`;;
  
let mk_unadorned_v39 = new_definition `mk_unadorned_v39 k d a b = 
    scs_v39 (k,d,a,a,b,b,(\i j. F),{},{},{})`;;
  
let cs_adj = new_definition `cs_adj k a1 a2 i j = 
    (if (i MOD k = j MOD k) then &0
     else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2))`;;
  
let psort = new_definition `psort k (u:num#num) = 
    (let i = FST u MOD k in
     let j = SND u MOD k in
       if (i <= j) then (i,j) else (j,i))`;;
  (*
    let ASSOCD = new_definition` ASSOCD (a:A) hs (d:D) = 
    if hs = [] then d else ASSOC a hs`;;
  *)

  
let ASSOCD_v39 = new_recursive_definition list_RECURSION
    `ASSOCD_v39 (a:A) [] (d:D) = d /\
    ASSOCD_v39 a (CONS h t) d = if (a = FST h) then SND h else ASSOCD_v39 a t d`;;
  
let funlist_v39 = new_definition `funlist_v39 data d k i j =
    (let data' = MAP (\ (u, d). (psort k u,d)) data in
       if (i MOD k = j MOD k) then (&0) 
       else ASSOCD_v39 (psort k (i,j)) data' d)`;;
  
let funlistA_v39 = new_definition `funlistA_v39 data (diag:A) default k i j =
    (let data' = MAP (\ (u, d). (psort k u,d)) data in
       if (i MOD k = j MOD k) then diag
       else ASSOCD_v39 (psort k (i,j)) data' default)`;;
  
let override = new_definition `override a k u d i j = 
    if psort k u = psort k (i,j) then (d:A) else a i j`;;
  
  (* constant 0.467 corrected on 2013-06-03. *)

  
let s_init_list_v39 = new_definition `s_init_list_v39 = 
    let upperbd = &6 in
    let a_pro = (\k p a1 a2 i j. 
		   (if (i MOD k = j MOD k) then &0
		    else (if {(i MOD k),(j MOD k)}={0,1} then p
			  else (if (j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) then a1 else a2)))) in
      [mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) upperbd); // scs_6I1
	 mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) upperbd); // scs_5I1
	   mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) upperbd); // scs_4I1
	     mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) upperbd); // scs_3I1
	       mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (sqrt8)) (cs_adj 5 (&2 * h0) upperbd);     // scs_5I2
		 mk_unadorned_v39 4 (#0.467) (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) upperbd);        // scs_4I2
		   mk_unadorned_v39 5 (#0.616) (a_pro 5 (&2 * h0) (&2) (&2 * h0)) (a_pro 5 sqrt8 (&2 * h0) upperbd); // scs_5I3
		     mk_unadorned_v39 4 (#0.477) (a_pro 4 (&2 * h0) (&2) sqrt8) (a_pro 4 sqrt8 (&2 * h0) upperbd) // scs_4I3
      ]`;;
  
let LENGTH_s_init_list = 
prove_by_refinement(
    `LENGTH s_init_list_v39 = 8`,

    (* {{{ proof *)
    [
      REWRITE_TAC[s_init_list_v39;LET_DEF;LET_END_DEF;LENGTH];
      BY(ARITH_TAC)
    ]);;
  (* }}} *)

  (* terminal cases *)

  let scs_6T1 = 
    `mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (cstab)) (cs_adj 6 (&2) (&6))`;;

  let scs_5T1 = 
    `mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (cstab)) (cs_adj 5 (&2) (&6))`;;

  let scs_4T1 = (* terminal_adhoc_quad_5691615370 =  *)
    `mk_unadorned_v39   4    #0.467    (cs_adj 4 (&2) (&3))
      (cs_adj 4 (&2) (&6))`;;

  let scs_4T2 = (* terminal_adhoc_quad_9563139965B = *)
    `mk_unadorned_v39 4  (#0.467) (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2*h0) (&3))`;;

  let scs_4T3 = (* terminal_adhoc_quad_4680581274 = *)
    `mk_unadorned_v39  4  (#0.513)  
      (funlist_v39 [(0,1),cstab ; (0,2),cstab ; (1,3),cstab ] (&2) 4)
      (funlist_v39 [(0,1),cstab ; (0,2),(&6) ; (1,3),(&6) ] (&2) 4)`;;

  (* deprecated 2013-06-17
     let terminal_adhoc_quad_7697147739 = 
     `mk_unadorned_v39 4  (#0.616 - #0.11)  (funlist_v39 [(0,1),sqrt8 ; (0,2),cstab ; (1,3),cstab ] (&2) 4) 
     (funlist_v39 [(0,1),sqrt8 ; (0,2),(&6) ; (1,3),(&6) ] (&2) 4)`;;
  *)

  let scs_4T4 = 
    `mk_unadorned_v39 4 (#0.477) 
      (funlist_v39 [(0,1),(&2 * h0);(0,2),sqrt8;(1,3),sqrt8] (&2) 4)
      (funlist_v39 [(0,1),sqrt8    ;(0,2),(&6); (1,3),cstab] (&2 * h0) 4)`;;

  let scs_4T5 = 
    `mk_unadorned_v39 4 (#0.513) 
      (funlist_v39 [(0,1),(&2 * h0);(0,2),cstab;(1,3),cstab] (&2) 4)
      (funlist_v39 [(0,1),cstab    ;(0,2),(&6); (1,3),cstab] (&2 * h0) 4)`;;

  (* deprecated 2013-06-17
     let terminal_tri_7720405539 = `mk_unadorned_v39
     3
     (#0.5518 / #2.0 - #0.2)
     (funlist_v39 [(0,1),cstab; (0,2), (&2 * h0); (1,2),(&2)] (&2) 3)
     (funlist_v39 [(0,1),#3.41; (0,2), (&2 * h0); (1,2),(&2)] (&2) 3)`;;
     
     let terminal_tri_2739661360 = `mk_unadorned_v39
     3
     (#0.5518 / #2.0 + #0.2)
     (funlist_v39 [(0,1),cstab; (0,2),cstab; (1,2),(&2)] (&2) 3)
     (funlist_v39 [(0,1), #3.41; (0,2),cstab; (1,2),(&2)] (&2) 3)`;;

     let terminal_tri_4922521904 = `mk_unadorned_v39
     3
     (#0.5518 / #2.0)
     (funlist_v39 [(0,1),cstab; (0,2),(&2)*h0; (1,2),(&2)] (&2) 3)
     (funlist_v39 [(0,1),#3.339; (0,2),(&2)*h0; (1,2),(&2)] (&2) 3)`;;

     let ear_stab = `mk_unadorned_v39 
     3
     //  (#0.11 + #0.1 *(cstab - sqrt8))  corrected 2013-4-20, see check_completeness djz.
     (#0.11)
     (funlist_v39 [(0,2),cstab] (&2) 3)
     (funlist_v39 [(0,2),cstab] (&2*h0) 3)`;;

     let terminal_ear_3603097872 = ear_cs;;

     let terminal_tri_7881254908 = 
     `mk_unadorned_v39 3  (#0.696 - #2.0 * #0.11)
     (funlist_v39 [(0,1),sqrt8;(1,2),sqrt8] (&2*h0) 3)
     (funlist_v39 [(0,1),cstab;(1,2),cstab] (&2*h0) 3)`;;

  *)
  

  let scs_3T1 = (* ear_jnull =  *)
    `scs_v39 (3, #0.11,
	      funlist_v39 [(0,1),sqrt8] (&2) 3,
	      funlist_v39 [(0,1),sqrt8] (&2) 3,
	      funlist_v39 [(0,1),cstab] (&2*h0) 3,
	      funlist_v39 [(0,1),cstab] ((&2)*h0) 3,
	      (\i j.  F),{},{},{})`;;

  let scs_3T2 = (* terminal_std_tri_OMKYNLT_3336871894 =  *)
    `mk_unadorned_v39
      3
      (&0)
      (funlist_v39 [] (&2) 3)
      (funlist_v39 [] (&2) 3)`;;

  (* 3 new additions 2013-06-04 3T3 3T4 3T5 *)

  let scs_3T3 = (* terminal_tri_4010906068 =  *)
    `mk_unadorned_v39  3
      (#0.476)
      (funlist_v39 [] (&2*h0) 3)
      (funlist_v39 [] (cstab) 3)`;;

  let scs_3T4 = (* terminal_tri_6833979866 =  *)
    `mk_unadorned_v39  3
      (#0.2759)
      (funlist_v39 [(0,1),(&2)] (&2*h0) 3)
      (funlist_v39 [(0,1),(&2 * h0)] (cstab) 3)`;;

  let scs_3T5 = (* terminal_tri_5541487347 =  *)
    `mk_unadorned_v39  3
      (#0.103)
      (funlist_v39 [(0,1),(&2 * h0)] (&2) 3)
      (funlist_v39 [(0,1),(sqrt8)] (&2 * h0) 3)`;;

  let scs_3T6 = (* terminal_tri_5026777310a =  *)
    `mk_unadorned_v39 3
      (#0.4348)
      (funlist_v39 [(0,1),sqrt8;(1,2),sqrt8] (&2) 3)
      (funlist_v39 [(0,1),cstab;(1,2),cstab] (&2*h0) 3)`;;

  let scs_3T7 = (* terminal_tri_9269152105 = 2468307358 *)
    `mk_unadorned_v39 3 (#0.2565)
      (funlist_v39 [(0,1),cstab; (0,2),cstab; (1,2),(&2)] (&2) 3)
      (funlist_v39 [(0,1),#3.62; (0,2),cstab; (1,2),(&2)] (&2) 3)`;;

  let terminal_cs = [
    scs_6T1;
    scs_5T1;

    (* quad cases *)
    scs_4T1; 
    scs_4T2; 
    scs_4T3; 
    scs_4T4;
    scs_4T5;

    (* triangle *)
    scs_3T1;
    scs_3T2;
    scs_3T3;
    scs_3T4;
    scs_3T5;
    scs_3T6;
    scs_3T7];;

  (* terminal_adhoc_quad_7697147739; *)

  (* upper echelon cases *)
  (*
    terminal_tri_7720405539; 
    terminal_tri_2739661360; 
    scs_3T7; 
    terminal_tri_4922521904;
  *)

  (* J cases 
     terminal_ear_3603097872; 
     scs_3T1; 
     terminal_tri_5405130650; 
  *)

  (* other triangles 
     terminal_tri_5026777310a; 
     terminal_tri_7881254908; 
     terminal_std_tri_OMKYNLT_3336871894; 
     terminal_tri_4010906068;
     terminal_tri_6833979866;
     terminal_tri_5541487347;
  *)




  (* nonterminal cases *)

  let ear_cs = 
    `scs_v39 (3, #0.11,
	      funlist_v39 [(0,1),sqrt8] (&2) 3,
	      funlist_v39 [(0,1),sqrt8] (&2) 3,
	      funlist_v39 [(0,1),cstab] ((&2)*h0) 3,
	      funlist_v39 [(0,1),cstab] (&2*h0) 3,
	      funlistA_v39 [(0,1),T] F F 3,{},{},{})`;;

  let terminal_tri_5405130650 = `scs_v39(
    3,
    #0.477 -  #0.11,
    funlist_v39 [(0,1),sqrt8;(0,2),(&2*h0);(1,2),(&2)] (&2) 3,
    funlist_v39 [(0,1),sqrt8;(0,2),(&2*h0);(1,2),(&2)] (&2) 3,
    funlist_v39 [(0,1),cstab;(0,2),sqrt8;(1,2),(&2*h0)] (&2*h0) 3,
    funlist_v39 [(0,1),cstab;(0,2),sqrt8;(1,2),(&2*h0)] (&2*h0) 3,
    funlistA_v39 [(0,1),T] F F 3,{},{},{})`;;

  (*
    let scs_terminal_v39 = new_definition (mk_eq (`scs_terminal_v39:(scs_v39)list`,(mk_flist terminal_cs)));;

  *)





  let ZITHLQN_concl =  `(!s vv. MEM s  s_init_list_v39 /\ vv IN
			   BBs_v39 s ==> 
			   &0 <= taustar_v39 s vv)  ==> JEJTVGB_assume_v39`;;

  (*
    let ZITHLQN = prove_by_refinement(
    `(!s vv. s IN set_of_list s_init_list_v39 /\ vv IN BBs_v39 s ==> &0 <= taustar_v39 s vv)  ==> JEJTVGB_assume_v39`,
  (* {{{ proof *)
    [
    rt[s_init_list_v39;set_of_list;JEJTVGB_assume_v39]
    st/r
    conj
    st/r
    rule (rr [taustar_v39])
    typ `CARD V = 3 \/ CARD V = 4 \/ CARD V = 5 \/ CARD V = 6` (C gthen assume)
    repeat (fxast `CARD` mp) then ARITH_TAC
    ]);;
  (* }}} *)
  *)

  
let BBprime_v39 = new_definition `BBprime_v39 s vv = (BBs_v39 s vv /\ 
							  (!ww. BBs_v39 s ww ==> taustar_v39 s vv <= taustar_v39 s ww) /\ taustar_v39 s vv < &0)`;;
  
let BBindex_v39 = new_definition `BBindex_v39 s (vv:num->real^3) = 
    CARD { i | i < scs_k_v39 s /\ scs_a_v39 s i (SUC i) = dist(vv i, vv (SUC i)) }`;;
  
let BBindex_min_v39 = new_definition `BBindex_min_v39 s = 
    min_num (IMAGE (BBindex_v39 s) (BBprime_v39 s))`;;
  
let BBprime2_v39 = new_definition `BBprime2_v39 s vv <=> 
    BBprime_v39 s vv /\ BBindex_v39 s vv = BBindex_min_v39 s`;;
  
let MMs_v39 = new_definition `MMs_v39 s vv <=>
    BBprime2_v39 s vv /\ 
    (!i. scs_str_v39 s i ==> azim (vec 0) (vv i) (vv (SUC i)) (vv (i + (scs_k_v39 s - 1))  ) = pi) /\
    (!i. scs_lo_v39 s i ==> norm (vv i) = &2) /\
    (!i. scs_hi_v39 s i ==> norm (vv i) = &2 * h0) /\
    (!i j. scs_am_v39 s i j <= dist(vv i,vv j)) /\
    (!i j. dist(vv i,vv j) <= scs_bm_v39 s i j)`;;
  let unadorned_MMs_concl = `!s.
    unadorned_v39 s ==> (MMs_v39 s = BBprime2_v39 s)`;;
  
  let XWITCCN_concl = `!s vv. MEM s s_init_list_v39 /\ vv IN BBs_v39 s /\
    taustar_v39 s vv < &0 ==> ~(BBprime_v39 s = {})`;;

  let XWITCCN2_concl = `!s vv. MEM s s_init_list_v39 /\ vv IN BBs_v39 s /\
    taustar_v39 s vv < &0 ==> ~(BBprime2_v39 s = {})`;;

  let AYQJTMD_concl = `!s vv. MEM s s_init_list_v39 /\ vv IN BBs_v39 s /\
    taustar_v39 s vv < &0 ==> ~(MMs_v39 s = {})`;;
  
  let EAPGLE_concl =  `(!s. MEM s s_init_list_v39 ==> MMs_v39 s = {}) ==> JEJTVGB_assume_v39`;;

  let JKQEWGV1_concl = `!s vv. is_scs_v39 s /\ BBs_v39 s vv /\ taustar_v39 s vv < &0 /\
    3 < scs_k_v39 s ==>
    (sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
       (IMAGE (\i. (vv i,vv (SUC i))) (:num))  < pi)`;;

  let JKQEWGV2_concl = `!s vv. is_scs_v39 s /\ BBs_v39 s vv /\ taustar_v39 s vv < &0 /\
    3 < scs_k_v39 s ==>
    (
      let V = IMAGE vv (:num) in
      let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
	~circular V E)`;;

  let JKQEWGV3_concl = `!s vv v w. 
    (let V = IMAGE vv (:num) in
     let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
     let FF = IMAGE (\i. (vv i,vv (SUC i))) (:num) in
       (is_scs_v39 s /\ BBs_v39 s vv /\ taustar_v39 s vv < &0 /\ lunar (v,w) V E /\
	  3 < scs_k_v39 s ==>
	  (interior_angle1 (vec 0) FF v  < pi / &2 )))`;;

  let HFNXPZA_concl = `!s vv.
    is_scs_v39 s /\ BBs_v39 s vv /\ taustar_v39 s vv < &0 /\ scs_k_v39 s = 3 ==>
    dihV (vec 0) (vv 0) (vv 1) (vv 2) +
    dihV (vec 0) (vv 1) (vv 2) (vv 3) +
    dihV (vec 0) (vv 2) (vv 3) (vv 1) < &2 * pi`;;

  
let restriction_typ1_v39 = new_definition `restriction_typ1_v39 s = 
    (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))`;;
  
let restriction_typ2_v39 = new_definition `restriction_typ2_v39 s =
    (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_am_v39 s,scs_am_v39 s,
	      scs_am_v39 s,scs_am_v39 s,scs_J_v39 s,scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s))`;;
  (* DEPRECATED 
     let restriction_typ3_v39 = new_definition `restriction_typ3_v39 s i j a b =
     ((a <= scs_bm_v39 s i j  /\ scs_am_v39 s i j <= b),
     (let k = scs_k_v39 s in
     let i' =  i MOD k in
     let j' = j MOD k in
     let f = (\i'' j''. { i'' MOD k, j'' MOD k } = {i',j'}) in
     let a1 = (\i'' j''. if f i'' j'' then a else scs_a_v39 s i j) in
     let b1 = (\i'' j''. if f i'' j'' then b else scs_b_v39 s i j) in
     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
     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
     (scs_v39 (scs_k_v39 s,scs_d_v39 s,a1,am,
     bm,b1,scs_J_v39 s,scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s))))`;;

     let subdivision_v39 = new_definition `subdivision_v39 c i j s =
     (let precond =   ((scs_a_v39 s i j <= c) /\  c <= scs_b_v39 s i j) in
     let r1 = restriction_typ3_v39 s i j (scs_a_v39 s i j) c in
     let r2 = restriction_typ3_v39 s i j c (scs_b_v39 s i j) in
     let cons_if = (\b r rs. if b then CONS r rs else rs) in
     if precond then (cons_if (FST r1) (SND r1) (cons_if (FST r2) (SND r2) []))  else [])`;;
  *)

  
let restriction_cs1_v39 = new_definition `restriction_cs1_v39 s p q c =
    (let b1 = override (scs_b_v39 s) (scs_k_v39 s) (p,q) c in
     let bm = if (c < scs_bm_v39 s p q) then
       override (scs_bm_v39 s) (scs_k_v39 s) (p,q) c else scs_bm_v39 s in
       (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,
		 bm,b1,scs_J_v39 s,scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s)))`;;
  
let restriction_cs2_v39 = new_definition `restriction_cs2_v39 s p q c =
    (let a1 = override (scs_a_v39 s) (scs_k_v39 s) (p,q) c in
     let am = if (scs_am_v39 s p q < c) then
       override (scs_am_v39 s) (scs_k_v39 s) (p,q) c else scs_am_v39 s in
       (scs_v39 (scs_k_v39 s,scs_d_v39 s,a1,am,scs_bm_v39 s,scs_b_v39 s,
		 scs_J_v39 s,scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s)))`;;
  
let subdiv_v39 = new_definition `subdiv_v39 s p q c = 
    (if (c <= scs_a_v39 s p q) then [s]
     else (if (c <= scs_am_v39 s p q) then [restriction_cs2_v39 s p q c]
	   else (if (c < scs_bm_v39 s p q) then [restriction_cs1_v39 s p q c;restriction_cs2_v39 s p q c]
		 else (if (c < scs_b_v39 s p q) then [restriction_cs1_v39 s p q c]
		       else [s]))))`  

  let transfer_v39 = new_definition `transfer_v39 s s' <=>
    (is_ear_v39 s ==> (s = s')) /\
    (is_scs_v39 s') /\
    (unadorned_v39 s') /\
    scs_d_v39 s <= scs_d_v39 s' /\
    (scs_k_v39 s' = scs_k_v39 s) /\
    (!i j. scs_a_v39 s' i j <= scs_a_v39 s i j) /\
    (!i j. scs_b_v39 s i j <= scs_b_v39 s' i j) /\
    (!i j. scs_J_v39 s' i j ==>  scs_J_v39 s i j)
    `;;
  
let scs_prop_equ_v39 = new_definition `scs_prop_equ_v39 s i =
    (let shift1 = \ (f:num->bool) j. f (i + j) in
     let shift2 = \ (f:num->num-> real) j j'. (f (i + j)  (i + j')) in
     let shift2b = \ (f:num->num-> bool) j j'. (f (i + j)  (i + j')) in
       (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),
		 shift2 (scs_b_v39 s), shift2b (scs_J_v39 s), shift1 (scs_lo_v39 s) , 
		 shift1 (scs_hi_v39 s), shift1 (scs_str_v39 s))))`;;
  
let scs_opp_v39 = new_definition `scs_opp_v39 s =
    (let k = scs_k_v39 s in
       scs_v39 (scs_k_v39 s,scs_d_v39 s, peropp2 (scs_a_v39 s) k, peropp2 (scs_am_v39 s) k,
		peropp2 (scs_bm_v39 s) k,peropp2 (scs_b_v39 s) k,
		peropp2 (scs_J_v39 s) k, peropp (scs_lo_v39 s) k,
		peropp(scs_hi_v39 s) k, peropp (scs_str_v39 s) k))`;;
  (* 0--(p-1) slice: *)

  (*
    let torsor_slice_v39 = new_definition `torsor_slice_v39 s p = 
    (
    let mod1 = \ (f:num->bool) j. f (j MOD p) in
    let mod2 = \ (f:num->num->real) j j'. f (j MOD p) (j' MOD p) in
    let mod2b = \ (f:num->num->bool) j j'. f (j MOD p) (j' MOD p) in
    (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),
    mod2 (scs_b_v39 s), mod2b (scs_J_v39 s), mod1 (scs_lo_v39 s) , mod1 (scs_str_v39 s))))`;;
  *)

  
let scs_diag = new_definition `scs_diag k i j <=>
    ~(i MOD k = j MOD k) /\
    ~(SUC i MOD k = j MOD k) /\
    ~(i MOD k = SUC j MOD k)`;;

  
let scs_half_slice_v39 = new_definition `scs_half_slice_v39 s p q d' mkj = 
    (let p' = p MOD (scs_k_v39 s) in
     let k' = (q + 1 + (scs_k_v39 s - p')) MOD (scs_k_v39 s) in
     let mod2 = \ (f:num->num->real) j j'. f ((j MOD k')+ p') ((j' MOD k') + p') in
     let mod2b = \ (f:num->num->bool) j j'. f ((j MOD k')+ p') ((j' MOD k') + p') in
     let a1 = \ i'' j''. if {i'' MOD k',j'' MOD k'} = {0,k'-1} 
     then scs_am_v39 s p q else mod2 (scs_a_v39 s) i'' j'' in
     let b1 = \ i'' j''. if {i'' MOD k',j'' MOD k'} = {0,k'-1} 
     then scs_bm_v39 s p q else mod2 (scs_b_v39 s) i'' j'' in
     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
       scs_v39 (k',d',a1,a1,b1,b1,J,{},{},{}))`;;
  
let scs_slice_v39 = new_definition `scs_slice_v39 s p q d' d'' mkj = 
    (scs_half_slice_v39 s p q d' mkj,
     scs_half_slice_v39 s q p d'' mkj)`;;
  
let is_scs_slice_v39 = new_definition `is_scs_slice_v39 s s' s'' p q <=>
    (let d' = scs_d_v39 s' in
     let d'' = scs_d_v39 s'' in
     let mkj = scs_J_v39 s' 0 (scs_k_v39 s' - 1) in
       (((s',s'') = scs_slice_v39 s p q d' d'' mkj) /\
	  d' < #0.9 /\
	  d'' < #0.9 /\
	  scs_d_v39 s <= d' + d'' /\
	  scs_bm_v39 s p q < &4 /\
	  ((scs_k_v39 s = 4) \/ scs_bm_v39 s p q <= cstab) /\
	  (mkj ==> (is_ear_v39 s' \/ is_ear_v39 s''))))`;;
  
let scs_arrow_v39 = new_definition `scs_arrow_v39 S1 S2 <=> 
    (!s. s IN S2 ==> is_scs_v39 s) /\
    ((!s. s IN S1 ==> MMs_v39 s = {}) \/ 
       (?s. s IN S2 /\ ~(MMs_v39 s = {})))`;;
  (* added definitions 2013-06-17 *)

  
let xrr = new_definition `xrr y1 y2 y6 = &8 * (&1 - (y1 * y1 + y2*y2 - y6*y6)/(&2* y1 * y2))`;;
  
let scs_basic3 = new_definition `scs_basic3 d a01 b01 a02 b02 a12 b12 = 
    (let a = funlist_v39  [(0,1),a01;(0,2),a02;(1,2),a12] (&0) 3 in
     let b = funlist_v39  [(0,1),b01;(0,2),b02;(1,2),b12] (&0) 3 in
       mk_unadorned_v39 3 d a b)`;;
  
let scs_basic4 = new_definition `scs_basic4 d a01 b01 a02 b02 a03 b03 a12 b12 a13 b13 a23 b23 = 
    (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
     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
       mk_unadorned_v39 4 d a b)`;;
  (* renamed from scs_is_basic *)


  
let scs_generic = new_definition `scs_generic v <=> 
    generic (IMAGE v (:num))
    (IMAGE (\i. {v i, v (SUC i)}) (:num))`;;
  
let scs_is_str = new_definition `scs_is_str s vv i <=> (
    azim (vec 0) (vv i) (vv (SUC i)) (vv (i + (scs_k_v39 s - 1))  ) = pi)`;;
  
let scs_stab_diag_v39 = new_definition `scs_stab_diag_v39 s i j =
    (
      let k = scs_k_v39 s in 
      let b' = (\i' j'. if psort k (i,j) = psort k (i',j') then cstab else scs_b_v39 s i' j') in
	(mk_unadorned_v39 k (scs_d_v39 s) (scs_a_v39 s) b'))`;;
  
let scs_basic = new_definition `scs_basic_v39 s <=>
    unadorned_v39 s /\ (!i j. scs_J_v39 s i j = F)`;;
  
let scs_inj = 
prove_by_refinement(
    `!s s'. scs_basic_v39 s /\  scs_basic_v39 s' /\
      scs_d_v39 s = scs_d_v39 s' /\
      scs_k_v39 s = scs_k_v39 s' /\
      (scs_a_v39 s = scs_a_v39 s') /\ 
      (scs_b_v39 s = scs_b_v39 s')
      ==> (s = s')`,


    (* {{{ proof *)
    [
      REPEAT WEAKER_STRIP_TAC;
      REPEAT (FIRST_X_ASSUM_ST `scs_basic_v39` MP_TAC);
      REWRITE_TAC[scs_basic;unadorned_v39];
      ONCE_REWRITE_TAC[EQ_SYM_EQ];
      REWRITE_TAC[SET_RULE `{} = a <=> a = {}`];
      REPEAT WEAKER_STRIP_TAC;
      ONCE_REWRITE_TAC[GSYM scs_v39];
      AP_TERM_TAC;
      ASM_REWRITE_TAC[scs_components];
      TYPIFY `scs_J_v39 s = scs_J_v39 s'` (C SUBGOAL_THEN SUBST1_TAC);
      BY(ASM_REWRITE_TAC[FUN_EQ_THM]);
      BY(REWRITE_TAC[])
    ]);;
  (* }}} *)


  (* deprecate: only used in Ocbicby.basic_examples: *)

  (*
    let is_basic = new_definition `is_basic s <=>
    is_scs_v39 s /\ unadorned_v39 s /\ (!i j. scs_J_v39 s i j = F)`;;
  *)


  (*
    let mk_simplex = new_definition `mk_simplex v0 v1 v2 x1 x2 x3 x4 x5 x6 = 
    (let uinv = &1 / ups_x x1 x2 x6 in
    let d = delta_x x1 x2 x3 x4 x5 x6 in
    let d5 = delta_x5 x1 x2 x3 x4 x5 x6 in
    let d6 = delta_x4 x1 x2 x3 x4 x5 x6 in
    let vcross =  (v1 - v0) cross (v2 - v0) in
    v0 + uinv % ((&2 * sqrt d) % vcross + d5 % (v1 - v0) + d6 % (v2 - v0)))`;;
  *)

  
let mk_simplex1 = new_definition `mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6 =
    (let uinv = &1 / ups_x x1 x2 x6 in
     let d = delta_x x1 x2 x3 x4 x5 x6 in
     let d5 = delta_x5 x1 x2 x3 x4 x5 x6 in
     let d4 = delta_x4 x1 x2 x3 x4 x5 x6 in
     let vcross =  (v1 - v0) cross (v2 - v0) in
       v0 + uinv % ((&2 * sqrt d) % vcross + d5 % (v1 - v0) + d4 % (v2 - v0)))`;;
  
let mk_planar2 = new_definition `mk_planar2 v0 v1 v2 x1 x2 x3 x5 x6 s = 
    (let vcross = (v1 - v0) cross ((v1 - v0) cross (v2 - v0)) in
       v0 + ((x1 + x3 - x5) / (&2 * x1)) % (v1 - v0) +
	 ((s / x1) * sqrt (ups_x x1 x3 x5 / ups_x x1 x2 x6)) % vcross)`;;
  
let scs_M = new_definition `scs_M s = 
    { i | i < scs_k_v39 s /\ (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i)) }`;;
  
let scs_6I1 = new_definition `scs_6I1 = 
    mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (&2 * h0)) (cs_adj 6 (&2 * h0) (&6))`;;
  
let scs_5I1 = new_definition `scs_5I1 = 
    mk_unadorned_v39 5 (d_tame 5) (cs_adj 5 (&2) (&2 * h0)) (cs_adj 5 (&2 * h0) (&6))`;;
  
let scs_4I1 = new_definition `scs_4I1 = 
    mk_unadorned_v39 4 (d_tame 4) (cs_adj 4 (&2) (&2 * h0)) (cs_adj 4 (&2 * h0) (&6))
      `;;
  
let scs_3I1 = new_definition `scs_3I1 = 
    mk_unadorned_v39 3 (d_tame 3) (cs_adj 3 (&2) (&2 * h0)) (cs_adj 3 (&2 * h0) (&6))
      `;;
  
let scs_5I2 = new_definition `scs_5I2 = 
    mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (sqrt8)) (cs_adj 5 (&2 * h0) (&6))
      `;;
  
let scs_4I2 = new_definition `scs_4I2 = 
    mk_unadorned_v39 4 (#0.467) (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2 * h0) (&6))
      `;;
  
let scs_5I3 = new_definition `scs_5I3 = 
    mk_unadorned_v39 5 (#0.616) 
      (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)
      (funlist_v39 [(0,1),sqrt8;(0,2),(&6);(0,3),(&6);(1,3),(&6);(1,4),(&6);(2,4),(&6)] (&2*h0) 5)`;;
  
let scs_4I3 = new_definition `scs_4I3 = 
    mk_unadorned_v39 4 (#0.477) 
      (funlist_v39 [(0,1),(&2*h0);(0,2),(sqrt8);(1,3),(sqrt8)] (&2) 4)
      (funlist_v39 [(0,1),sqrt8;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
  (* terminal cases *)

  
let scs_6T1 = new_definition
    `scs_6T1 = mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (cstab)) (cs_adj 6 (&2) (&6))`;;
  
let scs_5T1 = new_definition
    `scs_5T1 = mk_unadorned_v39 5 (#0.616) (cs_adj 5 (&2) (cstab)) (cs_adj 5 (&2) (&6))`;;
  let scs_4T1 = (* terminal_adhoc_quad_5691615370 =  *) new_definition
    `scs_4T1 = mk_unadorned_v39   4    #0.467    (cs_adj 4 (&2) (&3))
    (cs_adj 4 (&2) (&6))`;;

  let scs_4T2 = (* terminal_adhoc_quad_9563139965B = *) new_definition
    `scs_4T2 = mk_unadorned_v39 4  (#0.467) (cs_adj 4 (&2) (&3)) (cs_adj 4 (&2*h0) (&3))`;;

  let scs_4T3 = (* terminal_adhoc_quad_4680581274 = *) new_definition
    `scs_4T3 = mk_unadorned_v39  4  (#0.513)  
    (funlist_v39 [(0,1),cstab ; (0,2),cstab ; (1,3),cstab ] (&2) 4)
    (funlist_v39 [(0,1),cstab ; (0,2),(&6) ; (1,3),(&6) ] (&2) 4)`;;

  
let scs_4T4 =  new_definition 
    `scs_4T4 = mk_unadorned_v39 4 (#0.477) 
    (funlist_v39 [(0,1),(&2 * h0);(0,2),sqrt8;(1,3),sqrt8] (&2) 4)
    (funlist_v39 [(0,1),sqrt8    ;(0,2),(&6); (1,3),cstab] (&2 * h0) 4)`;;
  
let scs_4T5 = new_definition 
    `scs_4T5 = mk_unadorned_v39 4 (#0.513) 
    (funlist_v39 [(0,1),(&2 * h0);(0,2),cstab;(1,3),cstab] (&2) 4)
    (funlist_v39 [(0,1),cstab    ;(0,2),(&6); (1,3),cstab] (&2 * h0) 4)`;;
  let scs_3T1_PRELIM = (* ear_jnull =  *) new_definition
    `scs_3T1 = scs_v39 (3, #0.11,
			funlist_v39 [(0,1),sqrt8] (&2) 3,
			funlist_v39 [(0,1),sqrt8] (&2) 3,
			funlist_v39 [(0,1),cstab] (&2*h0) 3,
			funlist_v39 [(0,1),cstab] ((&2)*h0) 3,
			(\i j.  F),{},{},{})`;;

  
let scs_3T1 = 
prove_by_refinement(
    `scs_3T1 = mk_unadorned_v39 3 (#0.11)   
      (funlist_v39 [(0,1),(sqrt8)] (&2) 3)
      (funlist_v39 [(0,1),(cstab)] (&2 * h0) 3)`,

    (* {{{ proof *)
    [
      BY(REWRITE_TAC[mk_unadorned_v39;scs_3T1_PRELIM]);
    ]);;
  (* }}} *)

  let scs_3T2 = (* terminal_std_tri_OMKYNLT_3336871894 =  *) new_definition
    `scs_3T2 = mk_unadorned_v39
    3
    (&0)
    (funlist_v39 [] (&2) 3)
    (funlist_v39 [] (&2) 3)`;;

  let scs_3T3 = (* terminal_tri_4010906068 =  *) new_definition
    `scs_3T3 = mk_unadorned_v39  3
    (#0.476)
    (funlist_v39 [] (&2*h0) 3)
    (funlist_v39 [] (cstab) 3)`;;

  let scs_3T4 = (* terminal_tri_6833979866 =  *) new_definition
    `scs_3T4 = mk_unadorned_v39  3
    (#0.2759)
    (funlist_v39 [(0,1),(&2)] (&2*h0) 3)
    (funlist_v39 [(0,1),(&2 * h0)] (cstab) 3)`;;

  let scs_3T5 = (* terminal_tri_5541487347 =  *) new_definition
    `scs_3T5 = mk_unadorned_v39  3
    (#0.103)
    (funlist_v39 [(0,1),(&2 * h0)] (&2) 3)
    (funlist_v39 [(0,1),(sqrt8)] (&2 * h0) 3)`;;

  let scs_3T6 = (* terminal_tri_5026777310a =  *) new_definition
    `scs_3T6' = mk_unadorned_v39 3
    (#0.4348)
    (funlist_v39 [(0,1),sqrt8;(1,2),sqrt8] (&2) 3)
    (funlist_v39 [(0,1),cstab;(1,2),cstab] (&2*h0) 3)`;;

  let scs_3T7 = (* terminal_tri_9269152105 = 2468307358 *) new_definition
    `scs_3T7 = mk_unadorned_v39 3 (#0.2565)
    (funlist_v39 [(0,1),cstab; (0,2),cstab; (1,2),(&2)] (&2) 3)
    (funlist_v39 [(0,1),#3.62; (0,2),cstab; (1,2),(&2)] (&2) 3)`;;

  
let scs_6M1 = new_definition `scs_6M1 = 
    mk_unadorned_v39 6 (d_tame 6) (cs_adj 6 (&2) (cstab)) (cs_adj 6 (&2 * h0) (&6))`;;
  
let scs_5M1 = new_definition
    `scs_5M1 = mk_unadorned_v39 5 (#0.616) 
    (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)
    (funlist_v39 [(0,1),cstab;  (0,2),(&6);   (0,3),(&6);   (1,3),(&6);   (1,4),(&6);   (2,4),(&6)] (&2*h0) 5)`;;
  
let scs_5M2 = new_definition
    `scs_5M2 = mk_unadorned_v39 5 (#0.616) 
    (funlist_v39 [(0,1),(&2);(0,2),(cstab);(0,3),(cstab);(1,3),(cstab);(1,4),(cstab);(2,4),(cstab)] (&2) 5)
    (funlist_v39 [(0,1),cstab;(0,2),(&6);  (0,3),(&6);   (1,3),(&6);   (1,4),(&6);   (2,4),(&6)] (&2*h0) 5)`;;
  
let scs_4M1 = new_definition
    `scs_4M1 = mk_unadorned_v39 4 (#0.3401)
    (funlist_v39 [(0,1),(&2*h0);(0,2),(&2*h0);(1,3),(&2*h0)] (&2) 4)
    (funlist_v39 [(0,1),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
  
let scs_4M2 = new_definition
    `scs_4M2 = mk_unadorned_v39 4 (#0.3789)
    (funlist_v39 [(0,1),(&2*h0);(0,2),(&2*h0);(1,3),(&2*h0)] (&2) 4)
    (funlist_v39 [(0,1),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
  (*
    let scs_4M3' = new_definition 
    `scs_4M3' = mk_unadorned_v39 4 (#0.503)
    (funlist_v39 [(0,1),(sqrt8);(0,2),(sqrt8);(1,3),(sqrt8)] (&2) 4)
    (funlist_v39 [(0,1),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;

    let scs_4M4 = new_definition
    `scs_4M4 = mk_unadorned_v39 4 (#0.503)
    (funlist_v39 [(0,1),(&2*h0);(1,2),(&2*h0);(0,2),(&2*h0);(1,3),(&2*h0)] (&2) 4)
    (funlist_v39 [(0,1),cstab;(1,2),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;

    let scs_4M5 = new_definition
    `scs_4M5 = mk_unadorned_v39 4 (#0.503)
    (funlist_v39 [(0,1),(&2*h0);(2,3),(&2*h0);(0,2),(&2*h0);(1,3),(&2*h0)] (&2) 4)
    (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;

    let scs_4M6 = new_definition
    `scs_4M6 = mk_unadorned_v39 4 (#0.503)
    (funlist_v39 [(0,1),(&2*h0);(0,2),(cstab);(1,3),(cstab)] (&2) 4)
    (funlist_v39 [(0,1),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
  *)

  
let scs_4M3 = new_definition 
    `scs_4M3' = mk_unadorned_v39 4 (#0.513)
    (funlist_v39 [(0,1),(sqrt8);(0,2),(sqrt8);(1,3),(sqrt8)] (&2) 4)
    (funlist_v39 [(0,1),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
  
let scs_4M4 = new_definition
    `scs_4M4' = mk_unadorned_v39 4 (#0.513)
    (funlist_v39 [(0,1),(&2*h0);(1,2),(&2*h0);(0,2),(&2*h0);(1,3),(&2*h0)] (&2) 4)
    (funlist_v39 [(0,1),cstab;(1,2),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
  
let scs_4M5 = new_definition
    `scs_4M5' = mk_unadorned_v39 4 (#0.513)
    (funlist_v39 [(0,1),(&2*h0);(2,3),(&2*h0);(0,2),(&2*h0);(1,3),(&2*h0)] (&2) 4)
    (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
  
let scs_4M6 = new_definition
    `scs_4M6' = mk_unadorned_v39 4 (#0.513)
    (funlist_v39 [(0,1),(&2*h0);(0,2),(cstab);(1,3),(cstab)] (&2) 4)
    (funlist_v39 [(0,1),cstab;(0,2),(&6);(1,3),(&6)] (&2*h0) 4)`;;
  
let scs_4M7 = new_definition
    `scs_4M7 = mk_unadorned_v39 4 (#0.513)
    (funlist_v39 [(0,1),(&2*h0);(1,2),(&2*h0);(0,2),(cstab);(1,3),(cstab)] (&2) 4)
    (funlist_v39 [(0,1),cstab;(1,2),cstab;(0,2),(&6);(1,3),(&6);(1,3),(&6)] (&2*h0) 4)`;;
  
let scs_4M8 = new_definition
    `scs_4M8 = mk_unadorned_v39 4 (#0.513)
    (funlist_v39 [(0,1),(&2*h0);(2,3),(&2*h0);(0,2),(cstab);(1,3),(cstab)] (&2) 4)
    (funlist_v39 [(0,1),cstab;(2,3),cstab;(0,2),(&6);(1,3),(&6);(1,3),(&6)] (&2*h0) 4)`;;
  
let scs_3M1 = new_definition
    `scs_3M1 = mk_unadorned_v39 3 (#0.103)   
    (funlist_v39 [(0,1),(&2 * h0)] (&2) 3)
    (funlist_v39 [(0,1),(cstab)] (&2 * h0) 3)`;;

  (* Some conclusions *)
  
  let QKNVMLB1_concl = `!s p q d' mkj vv.
    (let s' = scs_half_slice_v39 s p q d' mkj in
     let vv'  = (\i. vv ((i+p) MOD (scs_k_v39 s'))) in
       MMs_v39 s vv /\
	 scs_bm_v39 s p q < &4 /\
	 ((scs_k_v39 s = 4) \/ scs_bm_v39 s p q <= cstab) /\
	 is_scs_v39 s /\ d' < #0.9 /\ scs_diag (scs_k_v39 s) p q ==> 
	 BBs_v39 s' vv')`;;
  
  let QKNVMLB2_concl = `!s p q d' d'' mkj vv.
    (let s' = FST (scs_slice_v39 s p q d' d'' mkj) in
     let s'' = SND (scs_slice_v39 s p q d' d'' mkj) in
     let vv'  = (\i. vv ((i+p) MOD (scs_k_v39 s'))) in
     let vv'' = (\i. vv ((i+q) MOD (scs_k_v39 s''))) in
       MMs_v39 s vv /\
	 is_scs_v39 s /\ scs_diag (scs_k_v39 s) p q /\
	 is_scs_slice_v39 s s' s'' p q /\
	 scs_d_v39 s <= d' + d'' ==>
	 dsv_v39 s vv <= dsv_v39 s' vv' + dsv_v39 s'' vv'')`;;

  let QKNVMLB3_concl = `!s p q d' d'' mkj vv.
    (let s' = FST (scs_slice_v39 s p q d' d'' mkj) in
     let s'' = SND (scs_slice_v39 s p q d' d'' mkj) in
     let vv'  = (\i. vv ((i+p) MOD (scs_k_v39 s'))) in
     let vv'' = (\i. vv ((i+q) MOD (scs_k_v39 s''))) in
       MMs_v39 s vv /\
	 is_scs_v39 s /\ scs_diag (scs_k_v39 s) p q /\
 	 is_scs_slice_v39 s s' s'' p q /\
	 scs_d_v39 s <= d' + d'' ==>
	 taustar_v39 s' vv' + taustar_v39 s'' vv'' <= taustar_v39 s vv)`;;

  (* AZGJNZO *)

  
  
let FZIOTEF_REFL = 
prove_by_refinement(
    `!S.  (!s. s IN S ==> is_scs_v39 s) ==> scs_arrow_v39 S S`,

    (* {{{ proof *)
    [
      REWRITE_TAC[scs_arrow_v39];
      BY(MESON_TAC[])
    ]);;
  (* }}} *)

  
let FZIOTEF_TRANS = 
prove_by_refinement(
    `!S1 S2 S3.  scs_arrow_v39 S1 S2 /\ scs_arrow_v39 S2 S3 ==>
      scs_arrow_v39 S1 S3`,

    (* {{{ proof *)
    [
      REWRITE_TAC[scs_arrow_v39];
      REPEAT WEAKER_STRIP_TAC;
      ASM_REWRITE_TAC[];
      BY(ASM_MESON_TAC[])
    ]);;
  (* }}} *)

  let EQTTNZI1_concl = `!s. is_scs_v39 s /\ 
    (!i j. scs_J_v39 s i j ==> scs_b_v39 s i j = scs_bm_v39 s i j) /\
    (scs_J_v39 s = (\i j. F) \/ 3 < scs_k_v39 s)
    ==> scs_arrow_v39 {s} {restriction_typ1_v39 s}`;;

  let EQTTNZI2_concl = `!s t. is_scs_v39 s /\ 
    (scs_am_v39 s = scs_bm_v39 s) /\
    (t = restriction_typ2_v39 s) /\ (!i j. ~scs_J_v39 s i j) /\
    (!i. scs_am_v39 s i i = &0) /\
    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
    ==> scs_arrow_v39 {s} {t}`;;

  let UAGHHBM_concl = `!s i j c .
    (let k = scs_k_v39 s in
       (is_scs_v39 s /\
	  scs_a_v39 s i j <= c /\  c <= scs_b_v39 s i j /\
	  3 < k /\
	  ~(i MOD k = j MOD k) /\
	  ~(scs_J_v39 s i j) /\
	  ((j MOD k = SUC i MOD k) \/ (SUC j MOD k = i MOD k) ==> (~(c = scs_am_v39 s i j))) /\
	  ((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))
	  ==>
	  scs_arrow_v39 {s} (set_of_list (subdiv_v39 s i j c))))`;;

  let YXIONXL1_concl = `!s t.
    is_scs_v39 s /\
    transfer_v39 s t ==> scs_arrow_v39 {s} {t}`;;

  let YXIONXL2_concl = `!s.
    is_scs_v39 s ==> scs_arrow_v39 {s} {scs_opp_v39 s}`;;

  let YXIONXL3_concl = `!s i.
    is_scs_v39 s ==> scs_arrow_v39 {s} {scs_prop_equ_v39 s i}`;;

  let LKGRQUI_concl = `!s s' s'' p q d' d'' mkj.
    is_scs_v39 s /\ (s',s'') = scs_slice_v39 s p q d' d'' mkj ==> scs_arrow_v39 {s} {s',s''}`;;

  let HXHYTIJ_concl = `!s vv ww.
    is_scs_v39 s /\
    BBprime2_v39 s vv /\
    BBs_v39 s ww ==>
    (taustar_v39 s vv < taustar_v39 s ww  \/
       BBindex_v39 s vv <= BBindex_v39 s ww)`;;

  let ODXLSTCv2_concl = `!s k w l.
    is_scs_v39 s /\
    MMs_v39 s w /\
    k = scs_k_v39 s /\
    3 < k /\ 
    (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i) /\
    ~(&2 = norm (w l)) /\
    (!i. ~(i MOD k = l MOD k) ==> scs_a_v39 s l i < dist(w l,w i)) /\
    (!i. ~(scs_J_v39 s l i)) /\
    (!V E v.
       V = IMAGE w (:num) /\
	E = IMAGE (\i. {w i, w (SUC i)}) (:num) ==>
	~(lunar (v,(w l)) V E )) ==> F`;;

  let IMJXPHRv2_concl = `!s k w l.
    is_scs_v39 s /\
    MMs_v39 s w /\
    azim (vec 0) (w l) (w (SUC l)) (w (l + (scs_k_v39 s - 1))  ) = pi /\
    k = scs_k_v39 s /\
    3 < k /\
    ~(collinear {vec 0,w (SUC l),w (l + (scs_k_v39 s - 1)) })/\
    (w l) IN aff_gt {vec 0} {w (SUC l),w (l + (scs_k_v39 s - 1)) }/\

    (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i) /\
    ~(&2 = norm (w l)) /\
    (!i. scs_diag k l i ==> scs_a_v39 s l i < dist(w l,w i)) /\
    (!i. ~(scs_J_v39 s l i)) /\
    (!V E v.
       V = IMAGE w (:num) /\
	E = IMAGE (\i. {w i, w (SUC i)}) (:num) ==>
	~(lunar (v,(w l)) V E )) ==> 
    (scs_a_v39 s l (SUC l) = dist (w l, w (SUC l)) /\
	(scs_a_v39 s l (l + (k-1)) = dist (w l, w (l + (k-1)))))`;;

  let NUXCOEAv2_concl = `!s k w l j.
    is_scs_v39 s /\
    MMs_v39 s w /\
    azim (vec 0) (w l) (w (SUC l)) (w (l + (scs_k_v39 s - 1))  ) = pi /\
    ~(collinear {vec 0,w (SUC l),w (l + (scs_k_v39 s - 1)) })/\
    (w l) IN aff_gt {vec 0} {w (SUC l),w (l + (scs_k_v39 s - 1)) }/\
    k = scs_k_v39 s /\
    3 < k /\
    (j MOD k = SUC l MOD k \/ SUC j MOD k = l MOD k) /\
    (scs_a_v39 s j l = dist(w j,w l)) /\ 
    (scs_a_v39 s j l < scs_b_v39 s j l) /\
    (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i) /\
    (!i. scs_diag k l i ==> scs_a_v39 s l i < dist(w l,w i)) /\
    (!i. ~(scs_J_v39 s l i)) /\
    (!V E v.
       V = IMAGE w (:num) /\
	E = IMAGE (\i. {w i, w (SUC i)}) (:num) ==>
	~(lunar (v,(w l)) V E )) ==> 
    (scs_a_v39 s l (SUC l) = dist (w l, w (SUC l)) /\
	(scs_a_v39 s l (l + (k-1)) = dist (w l, w (l + (k-1)))))`;;


  (*
    let deform_ODXLSTC_concl = `!s k l.
    is_scs_v39 s /\
    ~(MMs_v39 s = {}) /\
    k = scs_k_v39 s /\
    3 < k /\
    (!i. ~(scs_J_v39 s l i)) /\
    ~(scs_lo_v39 s l) /\
    (!j. ~(j MOD k = l MOD k) ==> scs_a_v39 s j l < scs_bm_v39 s j l) /\
    (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i)
    ==>
    scs_arrow_v39 {s} 
    ({(scs_v39 (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, {j | j MOD k = l} UNION scs_lo_v39 s , 
    scs_hi_v39 s, scs_str_v39 s))} UNION 
    (IMAGE (\j. (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,
    (\i i'. if {i MOD k,i' MOD k} = {j MOD k,l MOD k} then scs_a_v39 s j l
    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)))
    {j | ~(j = l) /\ j < scs_k_v39 s /\ (scs_a_v39 s l j  = scs_am_v39 s l j) }))
    `;;

    let deform_IMJXPHR_concl = `!s k p0 p1 p2.
    is_scs_v39 s /\
    k = scs_k_v39 s /\
    3 < k /\
    p1 = p0 + 1 /\
    p2 = p0 + 2 /\
    scs_str_v39 s p1 /\
    ~(scs_J_v39 s p0 p1) /\
    ~(scs_J_v39 s p1 p2) /\
    ~(scs_lo_v39 s p1) /\
    (!i. scs_diag k p1 i ==> &4 * h0 < scs_b_v39 s p1 i) /\
    (!i. scs_diag k p1 i ==> ~(scs_a_v39 s p1 i = scs_bm_v39 s p1 i)) /\
    (?q0 q2. ({p0,p2} = {q0,q2}) /\  
    scs_a_v39 s p1 q0 = scs_bm_v39 s p1 q0 /\
    ~(scs_a_v39 s p1 q2 = scs_bm_v39 s p1 q2)) ==>
    scs_arrow_v39 {s}
    ({(scs_v39 (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, 
    {j | j MOD k = p1} UNION scs_lo_v39 s , scs_hi_v39 s, scs_str_v39 s))} UNION 
    (IMAGE (\j. (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,
    (\i i'. if {i MOD k,i' MOD k} = {j MOD k,p1 MOD k} then scs_a_v39 s j p1
    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)))
    {j | ~(j = p1) /\ j < scs_k_v39 s /\ (scs_a_v39 s p1 j  = scs_am_v39 s p1 j) }))`;;

    let deform_NUXCOEA_concl = `!s k p0 p1 p2 p'.
    is_scs_v39 s /\
    k = scs_k_v39 s /\
    3 < k /\
    p1 = p0 + 1 /\
    p2 = p0 + 2 /\
    scs_str_v39 s p1 /\
    ~(scs_J_v39 s p0 p1) /\
    ~(scs_J_v39 s p1 p2) /\
    (!i. scs_diag k p1 i ==> &4 * h0 < scs_b_v39 s p1 i) /\
    (!i. scs_diag k p1 i ==> ~(scs_a_v39 s p1 i = scs_bm_v39 s p1 i)) /\
    (?p''. ({p0,p2} = {p',p''}) /\  
    scs_a_v39 s p1 p' = scs_bm_v39 s p1 p' /\
    ~(scs_a_v39 s p1 p'' = scs_bm_v39 s p1 p'')) ==>
    scs_arrow_v39 {s}
    (IMAGE (\j. (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,
    (\i i'. if {i MOD k,i' MOD k} = {j MOD k,p1 MOD k} then scs_a_v39 s j p1
    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)))
    {j | ~(j = p1) /\ ~(j = p') /\ j < scs_k_v39 s /\ (scs_a_v39 s p1 j  = scs_am_v39 s p1 j) })`;;

    let deform_2065952723_A1_single = `!s k p1 p2 p'.
    is_scs_v39 s /\
    k = scs_k_v39 s /\
    p2 = p1 + 1 /\
    arcmax_v39 s (p1,p2) < arc1553_v39 /\
    ~(scs_J_v39 s p1 p2) /\
    ~(scs_str_v39 s p1) /\
    ~(scs_str_v39 s p2) /\
    (!i. scs_diag k p1 i ==> &4 * h0 < scs_b_v39 s p1 i) /\
    (!i. scs_diag k p1 i ==> ~(scs_a_v39 s p1 i = scs_bm_v39 s p1 i)) /\
    ~(scs_a_v39 s p1 p2 = scs_bm_v39 s p1 p2) /\
    ~(scs_b_v39 s p1 p2 = scs_am_v39 s p1 p2) /\
    (?p''. ({p0,p2} = {p',p''}) /\  
    scs_a_v39 s p1 p' = scs_bm_v39 s p1 p' /\
    ~(scs_a_v39 s p1 p'' = scs_bm_v39 s p1 p'')) ==>
    scs_arrow_v39 {s}
    ({(scs_v39 (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,
    ({j | j MOD k = p1 MOD k} UNION scs_lo_v39 s) , scs_hi_v39 s,scs_str_v39 s)),
    (scs_v39 (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,
    ({j | j MOD k = p2 MOD k} UNION scs_lo_v39 s) , scs_hi_v39 s,scs_str_v39 s))}
    UNION
    (IMAGE (\j. (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,
    (\i i'. if {i MOD k,i' MOD k} = {j MOD k,p1 MOD k} then scs_a_v39 s j p1
    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)))
    {j | j < scs_k_v39 s /\ (scs_a_v39 s p1 j  = scs_am_v39 s p1 j) })
    UNION
    (IMAGE (\j. (scs_v39 (scs_k_v39 s,scs_d_v39 s,scs_a_v39 s,scs_am_v39 s,
    (\i i'. if {i MOD k,i' MOD k} = {j MOD k,p1 MOD k} then scs_a_v39 s j p1
    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)))
    {j | ~(j = p1) /\ ~(j = p') /\ j < scs_k_v39 s /\ (scs_a_v39 s p1 j  = scs_am_v39 s p1 j) }))`;;
  *)


  (* new material 2013-06-17 *)


  let DRNDRDV_concl =   `!y1 y2 y6. 
    derived_form (&0 < y1 /\ &0 < y2)
    (\q. xrr y1 y2 q) ((&8 * y6) / (y1 * y2)) y6 (:real)`;;

  let TBRMXRZ1_concl = `!f f' g h' x y.
    derived_form T f f' y (:real) /\
    derived_form T (f o g) h' x (:real) /\
    g x = y ==> re_eqvl f' h'`;;

  (*
    let PQCSXWG1_concl = `!v0 v1 v2 v3 x1 x2 x3 x4 x5 x6.
    &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\ &0 < x6 /\
    ~collinear {v0,v1,v2} /\
    x1 = dist(v1,v0) pow 2 /\
    x2 = dist(v2,v0) pow 2 /\
    x6 = dist(v1,v2) pow 2 /\
    &0 < delta_x x1 x2 x3 x4 x5 x6 /\
    v3 = mk_simplex v0 v1 v2 x1 x2 x3 x4 x5 x6 ==>
    (x3 = dist(v3,v0) pow 2 /\
    x5 = dist(v3,v1) pow 2 /\
    x4 = dist(v3,v2) pow 2 /\
    (v1 - v0) dot ((v2 - v0) cross (v3 - v0)) > &0)`;;

  (* some other continuities might be needed *)

    let PQCSXWG2_concl = `!(v0:real^3) v1 v2 v3 x1 x2 x3 x4 x5 x6.
    &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\ &0 < x6 /\
    ~collinear {v0,v1,v2} /\
    x1 = dist(v1,v0) pow 2 /\
    x2 = dist(v2,v0) pow 2 /\
    x6 = dist(v1,v2) pow 2 /\
    &0 < delta_x x1 x2 x3 x4 x5 x6 /\
    v3 = mk_simplex v0 v1 v2 x1 x2 x3 x4 x5 x6 ==>
    (\q. mk_simplex v0 v1 v2 x1 x2 x3 x4 q x6) continuous atreal x5`;;
  *)

  let PQCSXWG1_concl = `!v0 v1 v2 v3 x1 x2 x3 x4 x5 x6.
    &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\ &0 < x6 /\
    ~collinear {v0,v1,v2} /\
    x1 = dist(v1,v0) pow 2 /\
    x2 = dist(v2,v0) pow 2 /\
    x6 = dist(v1,v2) pow 2 /\
    &0 < delta_x x1 x2 x3 x4 x5 x6 /\
    v3 = mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6 ==>
    (x3 = dist(v3,v0) pow 2 /\
	x5 = dist(v3,v1) pow 2 /\
	x4 = dist(v3,v2) pow 2 /\
	(v1 - v0) dot ((v2 - v0) cross (v3 - v0)) > &0)`;;

  let PQCSXWG2_concl = `!(v0:real^3) v1 v2 v3 x1 x2 x3 x4 x5 x6.
    &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\ &0 < x6 /\
    ~collinear {v0,v1,v2} /\
    x1 = dist(v1,v0) pow 2 /\
    x2 = dist(v2,v0) pow 2 /\
    x6 = dist(v1,v2) pow 2 /\
    &0 < delta_x x1 x2 x3 x4 x5 x6 /\
    v3 = mk_simplex1 v0 v1 v2 x1 x2 x3 x4 x5 x6 ==>
    (\q. mk_simplex1 v0 v1 v2 x1 x2 x3 x4 q x6) continuous atreal x5`;;

  let EYYPQDW_concl = `!v0 v1 v2 v3 x1 x2 x3 x5 x6 s.
    &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x5 /\ &0 < x6 /\
    ~collinear {v0,v1,v2} /\
    x1 = dist(v1,v0) pow 2 /\
    x2 = dist(v2,v0) pow 2 /\
    x6 = dist(v1,v2) pow 2 /\
    &0 < ups_x x1 x3 x5 /\
    (s = &1 \/ s = -- &1) /\
    v3 = mk_planar2 v0 v1 v2 x1 x2 x3 x5 x6 s ==>
    (coplanar {v0,v1,v2,v3} /\
       x3 = dist(v3,v0) pow 2 /\
	x5 = dist(v3,v1) pow 2 /\
	?t. &0 < t /\
	t % ((v3- v0) cross (v1- v0)) = ( s % ((v1 - v0) cross (v2 - v0))))`;;

  let EYYPQDW2_concl =  `!(v0:real^3) v1 v2 x1 x2 x3 x5 x6 s.
    &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x5 /\ &0 < x6 /\
    ~collinear {v0,v1,v2} /\
    x1 = dist(v1,v0) pow 2 /\
    x2 = dist(v2,v0) pow 2 /\
    x6 = dist(v1,v2) pow 2 /\
    &0 < ups_x x1 x3 x5 ==>
    (\q. mk_planar v0 v1 v2 x1 x2 q x5 x6 s) continuous atreal x3`;;

  let EYYPQDW3_concl = `!(v0:real^3) v1 v2 x1 x2 x3 x5 x6 s.
    &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x5 /\ &0 < x6 /\
    ~collinear {v0,v1,v2} /\
    x1 = dist(v1,v0) pow 2 /\
    x2 = dist(v2,v0) pow 2 /\
    x6 = dist(v1,v2) pow 2 /\
    &0 < ups_x x1 x3 x5 ==>
    (\q. mk_planar v0 v1 q x1 x2 x3 x5 x6 s) continuous at v2`;;

  let FEKTYIY_concl = `!s v.
    is_scs_v39 s /\ v IN MMs_v39 s /\ 3 < scs_k_v39 s  ==>
    ~coplanar ({vec 0} UNION IMAGE v (:num))`;;

  let AURSIPD_concl = `!s v. 3 < scs_k_v39 s /\
    is_scs_v39 s /\ scs_generic v /\ v IN MMs_v39 s ==>
    3 + CARD { i | i < scs_k_v39 s /\ scs_is_str s vv i} <= scs_k_v39 s`;;
  
  let PPBTYDQ_concl = `!(u:real^3) v p. ~collinear {vec 0,v,p} /\ ~collinear {vec 0,u,p} /\
    arcV (vec 0) u p + arcV (vec 0) p v < pi ==> ~(vec 0 IN conv {u,v})`;;

  let MXQTIED_concl = `!s s' v.
    is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
    scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
    v IN MMs_v39 s /\ v IN BBs_v39 s' /\ scs_d_v39 s = scs_d_v39 s' /\
    (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i)) /\
    (!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)  ==>
    v IN MMs_v39 s'`;;

  let SYNQIWN_concl = `!s v i.
    is_scs_v39 s /\ v IN BBs_v39 s /\
    (norm (v i) = &2 \/ dist(v i,v (i+1)) = &2) /\
    (norm (v (i+2)) = &2 \/ dist(v (i+1),v(i+2)) = &2) /\
    cstab <= dist(v i,v(i+2)) ==>
    pi/ &2 < azim (vec 0) (v (i+1)) (v (i+2)) (v i)`;;

  let XWNHLMD_concl = `!s s' v.
    is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
    scs_k_v39 s = scs_k_v39 s' /\
    v IN MMs_v39 s /\ v IN BBs_v39 s' ==>
    scs_arrow_v39 {s} {s'}`;;

  let OIQKKEP_concl = `!u v c.
    u IN ball_annulus /\ v IN ball_annulus /\ c < &4 /\ &2 <= dist(u,v) /\ dist(u,v) <= c ==>
    arcV (vec 0) u v <= arclength (&2) (&2) c`;;

  let AXJRPNC_concl = `!s (v:num->real^3) i j.
    is_scs_v39 s /\ scs_basic_v39 s /\
    MMs_v39 s v /\ 
    (!i. scs_b_v39 s i (SUC i) <= cstab) /\
    (lunar (v i,v j) (IMAGE v (:num))
       (IMAGE (\i. {v i, v (SUC i)}) (:num))   ) ==>
    (scs_k_v39 s = 6 /\ v j = v (i + 3))`;;

  let RRCWNSJ_concl = `!s (v:num->real^3).
    is_scs_v39 s /\ scs_basic_v39 s /\ 3 < scs_k_v39 s /\
    MMs_v39 s v /\
    (!i j. scs_diag (scs_k_v39 s) i j ==> &4 * h0 < scs_b_v39 s i j) /\
    (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j))) /\
    (!i. scs_b_v39 s i (SUC i) <= cstab) ==>
    scs_generic v`;;

  let JCYFMRP_concl = `!s (v:num->real^3).
    is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
    (!i j. scs_diag (scs_k_v39 s) i j ==> &4 * h0 < scs_b_v39 s i j) /\
    CARD (scs_M s) <= 1 /\ 3 < scs_k_v39 s /\
    (!i. scs_a_v39 s i (SUC i) = &2) /\
    (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j))) ==>
    (?i. dist(v i, v (i+1)) = &2)`;;

  let TFITSKC_concl = `!s (v:num->real^3) i.
    is_scs_v39 s /\ 3 < scs_k_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
    scs_a_v39 s (i+1) (i+2) = &2 /\ scs_b_v39 s (i+1) (i+2) = &2 * h0 /\
    dist(v i,v (i+1)) = &2 /\
    (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j)) /\
     &4 * h0 < scs_b_v39 s i j) /\
    &2 < scs_b_v39 s i (i+1) /\ scs_a_v39 s (i+2) (i+3) < scs_b_v39 s (i+2) (i+3) ==>
    dist(v (i+1),v(i+2)) = &2`;;


  (* 3 < k, aij < bij  *)

  let CQAOQLR_concl = 
    `!s (v:num->real^3) i.
      is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
      (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j))) ==>
      scs_a_v39 s (i) (i+1) = &2 /\ scs_b_v39 s (i) (i+1) = &2 * h0 /\
	  scs_a_v39 s (i+1) (i+2) = &2 /\ scs_b_v39 s (i+1) (i+2) = &2 * h0  ==>
	  (dist(v i,v (i+1)) = &2 <=> dist(v(i+1),v(i+2)) = &2)`;;

  let JLXFDMJ_concl = `!s (v:num->real^3) i.
    is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
    dist(v i,v (i+1)) = &2 /\
    (!i j. scs_diag (scs_k_v39 s) i j ==> &4 * h0 < scs_b_v39 s i j) /\
    CARD (scs_M s) <= 1 /\
    (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j))) /\
    (!i. scs_a_v39 s i (i+1) < scs_b_v39 s i (i+1)) /\
    scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1) <= &2 * h0 
    ==>
	(!j. ~(j IN scs_M s ) ==>   dist(v j , v(j+1)) = &2)`;;

  let WKEIDFT_concl = `!s a b a' b' p q p' q'.
    (let k = scs_k_v39 s in
       (is_scs_v39 s /\ scs_basic_v39 s /\ 
	  (!i. scs_a_v39 s i (i + 1) = a) /\
	  (!i. scs_b_v39 s i (i + 1) = b) /\
	   p' + q = p + q' /\
	   (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\
	   (!i j. scs_diag k i j ==> scs_a_v39 s i j = a') /\
	   (!i j. scs_diag k i j ==> scs_b_v39 s i j = b') ==>
	   scs_arrow_v39 {scs_stab_diag_v39 s p q} {scs_stab_diag_v39 s p' q'}))`;;

  let PEDSLGV1_concl = `!v i j. 
    v IN MMs_v39 scs_6I1 /\
    scs_diag 6 i j /\
    dist(v i,v j) <= cstab ==>
    v IN MMs_v39 (scs_stab_diag_v39 scs_6I1 i j)`;;

  let PEDSLGV2_concl = `!v. 
    v IN MMs_v39 scs_6I1 /\
    (!i j. scs_diag 6 i j ==>   cstab <= dist(v i,v j)) ==>
    v IN MMs_v39 (scs_6M1)`;;

  let AQICLXA_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 2 } { scs_5M1, scs_3M1 }`;;

  let FUNOUYH_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_6I1 0 3 } {scs_4M2 }`;;

  let OEHDBEN_concl = `scs_arrow_v39 { scs_6I1 } { scs_6T1, scs_5M1, scs_4M2, scs_3T1 }`;;

  let OTMTOTJ1_concl = `scs_arrow_v39 { scs_5I1 } { scs_stab_diag_v39 scs_5I1 0 2 , scs_5M2 }`;;

  let OTMTOTJ2_concl = `scs_arrow_v39 { scs_5I2 } { scs_stab_diag_v39 scs_5I2 0 2 , scs_5M2 }`;;

(* corrected 2013/08/05 *)
  let OTMTOTJ3_concl = `scs_arrow_v39 { scs_5I3 } { scs_stab_diag_v39 scs_5M1 0 2 , 
						    scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4, scs_5M2 }`;;

  let OTMTOTJ4_concl = `scs_arrow_v39 { scs_5M1 } { scs_stab_diag_v39 scs_5M1 0 2 , 
						    scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4, scs_5M2 }`;;

  let HIJQAHA_concl = `scs_arrow_v39 { scs_5M2 } { scs_3T1,scs_3T4,scs_4M6',scs_4M7,scs_4M8,
						   scs_5T1, scs_stab_diag_v39 scs_5I2 0 2 , 
						   scs_stab_diag_v39 scs_5M1 0 2 ,     scs_stab_diag_v39 scs_5M1 0 3, scs_stab_diag_v39 scs_5M1 2 4 }`;;

  let CNICGSF1_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_5I1 0 2 }
    {scs_4M2, scs_3M1 }`;;

  let CNICGSF2_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_5I2 0 2 }
    {scs_4M3', scs_3T1 }`;;

  let CNICGSF3_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_5M1 0 2 }
    {scs_4M2, scs_3T4 }`;;

  let CNICGSF4_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_5M1 0 3 }
    {scs_4M4', scs_3M1 }`;;

  let CNICGSF5_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_5M1 2 4 }
    {scs_4M5', scs_3M1 }`;;

  let ARDBZYE_concl = `scs_arrow_v39 { scs_4I2 } { scs_4T1, scs_4T2 }`;;

  let FYSSVEV_concl = `scs_arrow_v39 { scs_4I1 } {scs_4I2, scs_stab_diag_v39 scs_4I1 0 2 }`;;

  let AUEAHEH_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_4I1 0 2 } { scs_3M1 }`;;

  let ZNLLLDL_concl = `scs_arrow_v39 { scs_stab_diag_v39 scs_4I3 0 2 } { scs_4T4 }`;;

  let VQFYMZY_concl = `scs_arrow_v39 { scs_4I3 } { scs_4T4, scs_4M6' }`;;

  (* let CNFNTYP_concl = `scs_arrow_v39 { scs_4M1 } { scs_4M2, scs_4M6' }`;; *)

  let BNAWVNH_concl = `scs_arrow_v39 { scs_4M2 } { scs_3M1, scs_3T4, scs_4M6' }`;;

  let RAWZDIB_concl = `scs_arrow_v39 { scs_4M3' } { scs_3T1, scs_3T6', scs_4M6' }`;;

  let MFKLVDK_concl = `scs_arrow_v39 { scs_4M4' } { scs_3M1, scs_3T4, scs_3T3, scs_4M7 }`;;

  let RYPDIXT_concl = `scs_arrow_v39 { scs_4M5' } { scs_3T4, scs_4M8 }`;;

  let GSXRFWM_concl = `!s v.
    is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s ==> scs_generic v`;;  

  let WGDHPPI_concl = `!s v.
    is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s ==>
    CARD { i | i < scs_k_v39 s /\ scs_is_str s v i} <= 1`;;

  let ASSWPOW_concl = `!s v i. 
    is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
    scs_b_v39 s i (i+1) <= &2 * h0 /\  scs_b_v39 s (i+1) (i+2) <= &2 * h0
    ==>    xrr (norm (v i)) (norm(v(i+2))) (dist(v i,v(i+2))) <= #15.53 `;;

  let YEBWJNG_concl = `!s v p.
    is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\ 
    (!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) /\
    (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
       (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
    ~scs_is_str s v p /\ ~scs_is_str s v (p+1) /\ scs_a_v39 s p (p+1) = &2 
    ==> dist(v p,v(p+1)) = &2`;;

  let TUAPYYU_concl = `!s v p.
    is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\ 
    (!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) /\
    (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
       (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
    ~scs_is_str s v p /\ ~scs_is_str s v (p+1) 
    ==> 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)`;;

  let WKZZEEH_concl = `!s v p.
    is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\ 
    (!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) /\
    (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
       (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
    ~scs_is_str s v p /\ ~scs_is_str s v (p+1) /\ ~scs_is_str s v (p+3) 
    ==> (~(dist(v p,v(p+3)) = cstab /\ dist(v(p),v(p+1)) = cstab))`;;

  let PWEIWBZ_concl = `!s v p.
    is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\ 
    (!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) /\
    (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
       (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
    scs_a_v39 s p (p+1) = &2
    ==> dist(v p,v(p+1)) = &2`;;

  let VASYYAU_concl = `!s v p.
    is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\ 
    (!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) /\
    (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
       (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
    scs_is_str s v p 
    ==> (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))`;;

(*
  
  let UFGHLP1_concl = `!s v i.
    is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
    (!i. scs_b_v39 s i (i+1) <= cstab) /\
    (!i j. scs_diag 4 i j ==> scs_a_v39 s i j < dist(v i,v j)) /\
    (scs_is_str s v (i+1)) ==>
    ((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)))`;;

  let UFGHLP2_concl = `!s v i.
    is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
    (!i. scs_b_v39 s i (i+1) <= cstab) /\
    (!i j. scs_diag 4 i j ==> scs_a_v39 s i j < dist(v i,v j)) /\
    (scs_is_str s v (i+1)) ==>
    ((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)))`;;

  let DSZPJSK_concl = `!s v i. 
    is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
    (!i. scs_b_v39 s i (i+1) <= cstab) /\
    (!i j. scs_diag 4 i j ==> scs_a_v39 s i j < dist(v i,v j)) /\
    (scs_is_str s v (i+1)) ==>
    (~(dist(v i,v(i+1)) = &2 * h0 /\ dist(v(i+1),v(i+2)) = cstab) /\
       ~(dist(v i,v(i+1)) = cstab /\ dist(v(i+1),v(i+2)) = &2 *h0))`;;

  let RDLGWIE_concl = `!s v i. 
    is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
    (!i. scs_b_v39 s i (i+1) <= cstab) /\
    (!i j. scs_diag 4 i j ==> scs_a_v39 s i j < dist(v i,v j)) ==>
    (~(dist(v i,v(i+1)) = &2 * h0 /\ dist(v(i+1),v(i+2)) = cstab) /\
       ~(dist(v i,v(i+1)) = cstab /\ dist(v(i+1),v(i+2)) = &2 *h0))`;;

  let LFYPZPI_concl = `!s v i. 
    is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
    (!i. scs_b_v39 s i (i+1) <= cstab) /\
    (!i j. scs_diag 4 i j ==> scs_a_v39 s i j < dist(v i,v j)) /\
    (dist(v i,v(i+1)) = &2 * h0) /\
    (dist(v (i+1),v(i+2)) = &2 * h0) /\
    (dist(v (i+2),v(i+3)) = &2 * h0) /\
    (scs_b_v39 s i (i+1) = &2 * h0) /\
    (scs_b_v39 s (i+1) (i+2) = &2 * h0) /\
    (scs_b_v39 s (i+2) (i+3) = &2 * h0) ==> F`;;
  
  let NZBSJXG_concl = `!s v i.
    is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
    (!i. scs_b_v39 s i (i+1) <= cstab) /\
    CARD (scs_M s) <= 1 /\
    (!i j. scs_diag 4 i j ==> scs_a_v39 s i j < dist(v i,v j)) /\
    (!i. scs_b_v39 s i (i+1) <= &2 * h0 ==> dist(v i,v (i+1)) = &2)`;;
*)

  let NWDGKXH_concl = `scs_arrow_v39 {scs_4M6'} {scs_4T3,scs_4T5}`;;
  
  let EFLYGAU_concl = `(?v. v IN MMs_v39 scs_4M7 /\
			  cstab < dist(v 0,v 2) /\ cstab < dist(v 1, v 3) )
    ==> scs_arrow_v39 {scs_4M7} {scs_4M6'}`;;

  let YOBIMPP_concl = ` scs_arrow_v39 {scs_4M7} {scs_3M1,scs_3T3,scs_3T4,scs_4M6'}`;;

  let BJTDWPS_concl = `(?v. v IN MMs_v39 scs_4M8 /\
			  cstab < dist(v 0,v 2) /\ cstab < dist(v 1, v 3) ) ==>
    scs_arrow_v39 {scs_4M8} {scs_4M6',scs_3T7}`;;

(*
  let MIQMCSN1_concl = `(?v. v IN MMs_v39 scs_4M8 /\
			  (dist(v 0,v 2) = cstab \/ dist(v 1, v 3) = cstab )) ==>
    scs_arrow_v39 {scs_4M7} {scs_3T4}`;;
*)

  let MIQMCSN_concl = `scs_arrow_v39 {scs_4M8} {scs_4M6',scs_3T7,scs_3T4}`;; 

  let LFLACKU_concl = `scs_arrow_v39 {scs_3T1} {scs_3T2,scs_3T5}`;;

  let CUXVZOZ_concl = `main_nonlinear_terminal_v11 ==> 
    (!s FF k p1 v.
       FF = IMAGE (\i. (v i,v (SUC i))) (:num) /\
	is_scs_v39 s /\
	k = scs_k_v39 s /\
	3 < k /\
	MMs_v39 s v /\
	scs_basic_v39 s /\
	scs_generic v /\
	&3 <= dist(v (p1+k-1),v (p1+1)) /\
	(!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)) /\
	(!i j. scs_diag k i j ==> &4 * h0 < scs_b_v39 s i j) /\
	interior_angle1 (vec 0) FF (v p1) < pi /\
	(pi/ &2 < interior_angle1 (vec 0) FF (v p1) \/ interior_angle1 (vec 0) FF (v (p1+1)) < pi) /\
	scs_a_v39 s p1 (p1+1) = &2 /\
	    scs_b_v39 s p1 (p1+1) <= &2 * h0 /\
	    &2 <= dist(v (p1+k-1),v p1) /\
	    dist(v (p1+k-1), v p1) <= cstab ==>
	    dist(v p1,v (p1+1)) = &2)`;;

  let CJBDXXN_concl = `main_nonlinear_terminal_v11 ==> 
    (!s FF k p1 v.
       FF = IMAGE (\i. (v i,v (SUC i))) (:num) /\
	is_scs_v39 s /\
	k = scs_k_v39 s /\
	3 < k /\
	MMs_v39 s v /\
	scs_basic_v39 s /\
	scs_generic v /\
	&3 <= dist(v (p1+1),v (p1+k-1)) /\
	(!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)) /\
	(!i j. scs_diag k i j ==> &4 * h0 < scs_b_v39 s i j) /\
	interior_angle1 (vec 0) FF (v p1) < pi /\
	(pi/ &2 < interior_angle1 (vec 0) FF (v p1) \/ interior_angle1 (vec 0) FF (v (p1+k-1)) < pi) /\
	scs_a_v39 s p1 (p1+k-1) = &2 /\
	    scs_b_v39 s p1 (p1+k-1) <= &2 * h0 /\
	    &2 <= dist(v (p1+1),v p1) /\
	    dist(v (p1+1), v p1) <= cstab ==>
	    dist(v p1,v (p1+k-1)) = &2)`;;

  let YRTAFYH_concl = 
    `!s i j.
      is_scs_v39 s /\
      scs_basic_v39 s /\
      3 < scs_k_v39 s /\
      scs_diag (scs_k_v39 s) i j /\
      scs_a_v39 s i j <= cstab ==>
      is_scs_v39 (scs_stab_diag_v39 s i j) /\ scs_basic_v39 (scs_stab_diag_v39 s i j)
      `;;

  let BKOSSGE_concl = 
    `scs_arrow_v39 {scs_3M1} {scs_3T1,scs_3T5}`;;

end;;