(* DEPRECATED:
   let taud = new_definition `taud y1 y2 y3 y4 y5 y6 = 
      #0.027 * safesqrt(delta_y y1 y2 y3 y4 y5 y6) + sol0 * (y1 - &2 * h0)/(&2 * h0 - &2)`;;

    let taud_v2 = new_definition `taud_v2 y1 y2 y3 y4 y5 y6 = 
      #0.027 * safesqrt(delta_y y1 y2 y3 y4 y5 y6) + sol0 * (y1 - &2 * h0)/(&2 * h0 - &2) +
	safesqrt(delta_y y1 y2 y3 y4 y5 y6) * #0.04 * (#2.52 - y1)`;;

    let taud_v3 = new_definition `taud_v3 y1 y2 y3 y4 y5 y6 = 
      #0.023 * safesqrt(delta_y y1 y2 y3 y4 y5 y6) + sol0 * (y1 - &2 * h0)/(&2 * h0 - &2) +
	safesqrt(delta_y y1 y2 y3 y4 y5 y6) * #0.055 * (#2.52 - y1)`;;

    let edge_flat50 =  new_definition`edge_flat50 y1 y2 y3 y5 y6 = 
      sqrt(quadratic_root_plus (abc_of_quadratic (
	\x4.  &50 - delta_x (y1*y1) (y2*y2)  (y3*y3)  x4 (y5*y5)  (y6*y6))))`;;

    let edge_flat250_x = new_definition `edge_flat250_x x1 x2 x3 x4 x5 x6 =
      (edge_flat (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x5) (sqrt x6)) pow 2`;;  (* x4 dummy *)

    
let edge_flat50_x =  new_definition`edge_flat50_x x1 x2 x3 (x4:real) x5 x6 = 
      edge_flat (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x5) (sqrt x6)`;;
let fn_sub246 = new_definition 
      `fn_sub246 f (x2s:real) (x4s:real) (x6s:real) 
      (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = 
      (f x1 x2s x3 x4s x5 x6s):real`;;
let fn_sub345 = new_definition 
      `fn_sub345 f (x3s:real) (x4s:real) (x5s:real) 
      (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = 
      (f x1 x2 x3s x4s x5s x6):real`;;
let edge_flatD_x1 = new_definition `edge_flatD_x1 d x2 x3 x4 x5 x6 = 
      sqrt(quadratic_root_plus (abc_of_quadratic (
	\x1.  d - delta_x x1 x2 x3 x4 x5 x6)))`;;
let edge_126_x = new_definition `edge_126_x d x4 x5 = 
      compose6 (edge_flatD_x1) (constant6 d) proj_x1 proj_x2 proj_x6 (constant6 x4) (constant6 x5)`;;
let edge_135_x = new_definition `edge_135_x d x4 x6 =
      compose6 (edge_flatD_x1) (constant6 d) proj_x1 proj_x3 proj_x5 (constant6 x4) (constant6 x6)`;;
let flat_term_126_x = new_definition `flat_term_126_x d x4 x5 = 
      uni(flat_term,edge_126_x d x4 x5)`;;
let flat_term_135_x = new_definition `flat_term_135_x d x4 x6 = 
      uni(flat_term,edge_135_x d x4 x6)`;;
let mudd_135_x_v2 = new_definition `mudd_135_x_v2 d x4 x6 = 
      mul6 (compose6 (promote3_to_6 mu_y) (uni(sqrt,edge2_135_x d x4 x6)) proj_y1 proj_y3 dummy6 dummy6 dummy6)
	(constant6 (sqrt d))`;;
let mudd_126_x_v2 = new_definition `mudd_126_x_v2 d x4 x5 = 
      mul6 (compose6 (promote3_to_6 mu_y) (uni(sqrt,edge2_126_x d x4 x5)) proj_y1 proj_y2 dummy6 dummy6 dummy6)
	(constant6 (sqrt d))`;;
let mudt_234_x = new_definition `mudt_234_x d y1 y5 y6 = 
      (mul6 (compose6 (mu6_x) (constant6 (y1*y1)) proj_x2 proj_x3 dummy6 dummy6 dummy6)
	(uni(truncate_sqrt d,(delta_234_x (y1*y1) (y5*y5) (y6*y6)))))`;;
let mudL_234_x = new_definition `mudL_234_x d1 d2 y1 y5 y6 = 
      (mul6 (compose6 (mu6_x) (constant6 (y1*y1)) proj_x2 proj_x3 dummy6 dummy6 dummy6)
	(constant6 (&1/ (sqrt(d1)+sqrt(d2))) * (delta_234_x (y1*y1) (y5*y5) (y6*y6)) + constant6(sqrt(d1))))`;;
*) add { idv="test4"; doc="tau_residual"; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (&2,y5,&2); (&2,y6,&2) ] ( (y_of_x tau_residual_x y1 y2 y3 y4 y5 y6 > #0.027 + #0.04 * (#2.52 - y1)) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test25353"; doc="full hexagon ear calculation. This shows that if (delta hi > 0) and (delta lo >0) we can erase the ear with small penalty. Hence, when we look at a lo ear, we can wrap it in with the hi ear case when the hi ear exists: (delta hi>0). By symmetry, wlog y2 < y3. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,&2); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (&2,y5,&2); (&2,y6,&2) ] ( (taud_v2 y1 y2 y3 y4 y5 y6 > -- #0.013) \/ (y_of_x (delta_sub1_x (#2.52 pow 2)) y1 y2 y3 y4 y5 y6 < &0) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y3 < y2) )`; };; add { idv="taud"; doc=""; tags=[Cfsqp;Xconvert]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (&2,y5,&2); (&2,y6,&2)] ((taum y1 y2 y3 y4 y5 y6 > taud y1 y2 y3 y4 y5 y6 + safesqrt(delta_y y1 y2 y3 y4 y5 y6) * #0.04 * (#2.52 - y1)) \/ (delta_y y1 y2 y3 y4 y5 y6 < &20))`; };; add { idv="local max"; doc="test"; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (#3.01,y1,#3.915); (&2,y2,#2.52); (&2,y3,#2.52); (&2,y4,#2.52); (&2,y5,#2.52); (&2,y6,#2.52) ] (let delta' = delta4_y y1 y2 y3 y4 y5 y6 * (&2 * y4) in let d = delta_y y1 y2 y3 y4 y5 y6 in let delta'' = -- &8 * (y1 * y4) pow 2 + delta4_y y1 y2 y3 y4 y5 y6 * (&2) in let mu = #0.1278 - #0.04 * y4 in let mu' = -- #0.04 in let h' = sol0 / (&2 * h0 - &2) in ( #1.0 < (&2 * mu' * d + mu * delta' + h' * &2 * safesqrt(d)) pow 2 \/ delta_y y1 y2 y3 y4 y5 y6 < &0 \/ mu' * d * delta' - (&1 / &4) * mu * (delta' pow 2) + (&1 / &2) * mu * d * delta'' < -- #1.0 ))`; };; add { idv="local max2"; doc="better local max test"; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (#3.01,y1,#3.915); (&2,y2,#2.52); (&2,y3,#2.52); (&2,y4,#2.52); (&2,y5,#2.52); (&2,y6,#2.52) ] (let d = delta_y y1 y2 y3 y4 y5 y6 in let delta' = delta4_y y1 y2 y3 y4 y5 y6 * (&2 * y4) in let delta'' = -- &8 * (y1 * y4) pow 2 + delta4_y y1 y2 y3 y4 y5 y6 * (&2) in let mu = #0.1278 - #0.04 * y4 in let mu' = -- #0.04 in ( mu' * d * delta' - (&1 / &4) * mu * (delta' pow 2) + (&1 / &2) * mu * d * delta'' < &0 \/ delta_y y1 y2 y3 y4 y5 y6 < &0 ))`; };; add { idv="local max debug"; doc="local max numerical debug"; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (#2.1,y1,#2.1); (#2.2,y2,#2.2); (#2.3,y3,#2.3); (#2.4,y4,#2.4); (#2.5,y5,#2.5); (#2.6,y6,#2.6) ] (let d = delta_y y1 y2 y3 y4 y5 y6 in let delta' = delta4_y y1 y2 y3 y4 y5 y6 * (&2 * y4) in let delta'' = -- &8 * (y1 * y4) pow 2 + delta4_y y1 y2 y3 y4 y5 y6 * (&2) in let mu = #0.1278 - #0.04 * y4 in let mu' = -- #0.04 in ( (mu' * d * delta' - (&1 / &4) * mu * (delta' pow 2) + (&1 / &2) * mu * d * delta'') / (d * safesqrt(d)) > &0 ))`; };; add { idv="5556646409 small domain"; doc="taum 2nd deriv test. "; tags=[Tex;Disallow_derivatives;Widthcutoff 0.004;Penalty(1500.0,5000.0);Cfsqp_branch 2]; ineq = all_forall `ineq [ (&2,y1,#2.52); (#2.0,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.237); (&2,y5,&2); (&2,y6,&2) ] ( (delta_y_LC y1 y2 y3 y4 y5 y6 < &15) \/ (y2 < y3) \/ (mdtau_y_LC y1 y2 y3 y4 y5 y6 > &0) \/ (mdtau_y_LC y1 y2 y3 y4 y5 y6 < &0) \/ (mdtau2uf_y_LC y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="taud pent"; doc="test"; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (&2,y4,#2.52); (&2,y5,#2.52); (#3.01,z2,#3.237); (#3.01,z5,#3.237) ] ( (taum y1 y3 y4 (&2) z5 z2 + taud_v3 y2 y3 y1 z2 (&2) (&2) + taud_v3 y5 y4 y1 z5 (&2) (&2) > #0.616) \/ delta_y y1 y3 y4 (&2) z5 z2 < &0 \/ delta_y y2 y3 y1 z2 (&2) (&2) < &0 \/ delta_y y5 y4 y1 z5 (&2) (&2) < &0 \/ (dih_y y1 y3 y4 (&2) z5 z2 + dih_y y1 y3 y2 (&2) (&2) (z2) + dih_y y1 y4 y5 (&2) (&2) (z5) < #1.75) )`; };; add { idv="taum pent"; doc="test"; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (&2,y4,#2.52); (&2,y5,#2.52); (#3.01,z2,#3.237); (#3.01,z5,#3.237) ] ( (taum y1 y3 y4 (&2) z5 z2 + taum y2 y3 y1 z2 (&2) (&2) + taum y5 y4 y1 z5 (&2) (&2) > #0.616) \/ delta_y y1 y3 y4 (&2) z5 z2 < &0 \/ delta_y y2 y3 y1 z2 (&2) (&2) < &0 \/ delta_y y5 y4 y1 z5 (&2) (&2) < &0 \/ (dih_y y1 y3 y4 (&2) z5 z2 + dih_y y1 y3 y2 (&2) (&2) (z2) + dih_y y1 y4 y5 (&2) (&2) (z5) < #1.75) )`; };; add { idv="taum pent2"; doc="test"; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (&2,y4,#2.52); (&2,y5,#2.52); (#3.01,z2,#3.237); (#3.01,z5,#3.237) ] ( (taum y1 y3 y4 (&2) z5 z2 + taud_v2 y2 y3 y1 z2 (&2) (&2) + taud_v2 y5 y4 y1 z5 (&2) (&2) > #0.616) \/ delta_y y1 y3 y4 (&2) z5 z2 < &0 \/ delta_y y2 y3 y1 z2 (&2) (&2) < &0 \/ delta_y y5 y4 y1 z5 (&2) (&2) < &0 \/ // extra delta constraints delta_y y2 y3 y1 z2 (&2) (&2) > &50 \/ delta_y y5 y4 y1 z5 (&2) (&2) > &50 \/ (dih_y y1 y3 y4 (&2) z5 z2 + dih_y y1 y3 y2 (&2) (&2) (z2) + dih_y y1 y4 y5 (&2) (&2) (z5) < #1.75) )`; };; add { idv="test5"; doc="tau_residual pent"; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.237); (&2,y5,&2); (&2,y6,&2) ] ( (y_of_x tau_residual_x y1 y2 y3 y4 y5 y6 > #0.023 + #0.055 * (#2.52 - y1) ) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test6"; doc="tau_residual pent"; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.1); (&2,y3,#2.52); (#3.01,y4,#3.237); (&2,y5,&2); (&2,y6,&2) ] ( (y_of_x tau_residual_x y1 y2 y3 y4 y5 y6 > #0.018 + #0.07 * (#2.52 - y1) ) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test7"; doc="taum for small delta"; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.237); (&2,y5,&2); (&2,y6,&2) ] ( (taum y1 y2 y3 y4 y5 y6 > &0) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (delta_y y1 y2 y3 y4 y5 y6 > &50) )`; };; add { idv="test8"; doc="taum for small delta"; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = Sphere.all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (&2,y4,&2); (&2,y5,&2); (#3.01,y6,#3.237) ] ( (delta_y y1 y2 y3 y4 y5 y6 > &0) \/ (dih_y y1 y2 y3 y4 y5 y6 < #0.096) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="4184277422"; doc="old name: test10*."; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (&2,y4,#2.52); (&2,y5,#2.52); (#3.01,z2,#3.237); (#3.01,z5,#3.237) ] ( (taum y1 y3 y4 (&2) z5 z2 + taud_v4 y2 y3 y1 z2 (&2) (&2) + taud_v4 y5 y4 y1 z5 (&2) (&2) > #0.616) \/ // delta_y y1 y3 y4 (&2) z5 z2 < &0 \/ delta_y y2 y3 y1 z2 (&2) (&2) < &0 \/ delta_y y2 y3 y1 z2 (&2) (&2) > &20 \/ delta_y y5 y4 y1 z5 (&2) (&2) < &20 )`; };; run { idv="test p"; doc="taum for small delta"; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = Sphere.all_forall `ineq [ (&2,y1,#2.52); (#2.1,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.24); (&2,y5,&2); (&2,y6,&2) ] ( (taum y1 y2 y3 y4 y5 y6 > #0.04) \/ (delta_y y1 y2 y3 y4 y5 y6 < &10) )`; };; skip { idv="1671775772"; doc="old name: local max v4*, WNLKGOQ better local max test. This is the numerator of the 2nd derivative of the function taud. Case delta > 20."; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.237); (&2,y5,&2); (&2,y6,&2) ] (y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/ taum y1 y2 y3 y4 y5 y6 > #0.1 \/ delta_y y1 y2 y3 y4 y5 y6 < &20)`; };; skip { idv="7099408714"; doc="old name: local max v4* better local max test. This is the numerator of the 2nd derivative of the function taud. Old False version."; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (&2,y5,&2); (&2,y6,&2) ] (y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/ delta_y y1 y2 y3 y4 y5 y6 < &0)`; };; skip { idv="2320951108"; doc=" local fan/main estimate/terminal pent LHS(135,y1=2) RHS(126,y1=2.52), extra implicit assumption delta > 20. mu sqrt(delta) >= 0.012 sqrt(&20) > 0.053. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (&2,y4,&2); (#3.01,y5,#3.237); (#3.01,y6,#3.237) ] ( (taum y1 y2 y3 y4 y5 y6 + y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + #0.053 > #0.616) ) `; };; add { idv="test"; doc=" local fan/main estimate/terminal pent LHS(135,y1=2.52) RHS(126,y1=2.52) wlog. LHS delta on ears is >= 20, mu sqrt(delta) >= 0.012 sqrt(&20) > 0.053. If RHS delta >= 20. get 0.541 + 2 (0.053) > 0.616. so wlog. RHS delta on ear is <= 20. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (&2,y4,&2); (#3.01,y5,#3.237); (#3.01,y6,#3.237) ] ( let d = &20 in ((taum y1 y2 y3 y4 y5 y6 + #0.053 > #0.616) \/ y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > d )) `; };; skip { idv="9115820315"; doc="old name: test9* test10* full terminal pentagon test, using taud on ears. assuming delta > 20 at y5."; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (&2,y4,#2.52); // (&2,y5,#2.52); (#3.01,z2,#3.237); (#3.01,z5,#3.237) ] ( (taum y1 y3 y4 (&2) z5 z2 + #0.12 + taud y2 y3 y1 z2 (&2) (&2) // + // test // &0 * taud y5 y4 y1 z5 (&2) (&2) > #0.616) \/ // \/ // delta_y y1 y3 y4 (&2) z5 z2 < &0 \/ delta_y y2 y3 y1 z2 (&2) (&2) < &0 // \/ // delta_y y5 y4 y1 z5 (&2) (&2) < &20 )`; };; skip { idv="test"; doc="pent hi(126-345) hi(135-234) full terminal pentagon test, using taud on ears. assuming delta > 20 both sides."; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (&2,y4,&2); (#3.01,y5,#3.237); (#3.01,y6,#3.237) ] ( (taum y1 y2 y3 y4 y5 y6 + y_of_x (mud_126_x_v1 (&2 * h0) (&2) (&2)) y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_126_x (&2 * h0) (&2) (&2)) y1 y2 y3 y4 y5 y6 + y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_126_x (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 > #0.616) \/ y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &20 \/ y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &20 ) `; };; add { idv="test R"; doc=" "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,&2); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.237); (&2,y5,&2); (&2,y6,&2) ] ( y4 > &2 \/ delta_y y1 y2 y3 y4 y5 y6 > &20) `; };; (* HEX CASES *) let template_hex_ear = `\ y2m y2M y3m y3M y4m y4M d. ineq [ (#2.0,y1,#2.52); (y2m,y2,y2M); (y3m,y3,y3M); (y4m,y4,y4M); (&2,y5,&2); (&2,y6,&2) ] (taud y1 y2 y3 y4 y5 y6 > d \/ delta_y y1 y2 y3 y4 y5 y6 < &0)`;; let mk_ineq_hex_ear i2 i3 i4 d = let x i = List.nth [`&2`;`#2.17`;`#2.34`;`#2.52`] i in let X i = x (i+1) in let y i = List.nth [`#3.01`;`#3.25`;`#3.5`;`#3.75`;`#3.915`] i in let Y i = y (i+1) in Ineq.mk_tplate template_hex [x i2;X i2; x i3;X i3; y i4;Y i4;d];; let make_hex_ear i2 i3 i4 d = { idv = Printf.sprintf "test %d %d %d" i2 i3 i4; ineq = mk_ineq_hex i2 i3 i4 d; doc = "local fan/main estimate/terminal hex/ear."; tags=[Cfsqp;Xconvert;Penalty(50.0,500.0)]; };; let runh (i2,i3,i4,d) = try (run(make_hex_ear i2 i3 i4 d)) with _ -> () ;; (* for i2=0 to 2 do for i3 = 0 to 2 do for i4 = 0 to 3 do runh (i2,i3,i4,`&0`) done done done;; *) map runh ;; let hex_ears = [ (0,0,0,Some `-- #0.2`); (0,0,1,Some `-- #0.552`); (0,0,2,Some `-- #0.552`); (0,0,3,None); (0,1,0,Some `-- #0.05`); (0,1,1,Some `-- #0.443`); (0,1,2,Some `-- #0.552`); (0,1,3,None); (0,2,0,Some `#0.04`); (0,2,1,Some `-- #0.29`); (0,2,2,Some `-- #0.552`); (0,2,3,Some `-- #0.552`); (1,0,0,Some `-- #0.05`); (1,0,1,Some `-- #0.45`); (1,0,2,Some `-- #0.552`); (1,0,3,None); (1,1,0,Some `#0.04`); (1,1,1,Some `-- #0.29`); (1,1,2,Some ` -- #0.552`); (1,1,3,Some ` -- #0.552`); (1,2,0,Some `#0.08`); (1,2,1,Some `-- #0.14`); (1,2,2,Some `-- #0.552`); (1,2,3,Some `-- #0.552`); (2,0,0,Some ` #0.04`); (2,0,1,Some `-- #0.29`); (2,0,2,Some `-- #0.552`); (2,0,3,Some `-- #0.552`); (2,1,0,Some `#0.08`); (2,1,1,Some `-- #0.14`); (2,1,2,Some `-- #0.552`); (2,1,3,Some `-- #0.552`); (2,2,0,Some `#0.11`); (2,2,1,Some `-- #0.017`); (2,2,2,Some `-- #0.45`); (2,2,3,Some `-- #0.552`); ];; let reformat_ear = let f (i,j,k,d) = ((i,j,k),d) in map f hex_ears;; let template_hex = `\ y1m y1M y2m y2M y3m y3M y4m y4M y5m y5M y6m y6M d1 d2 d3. ineq [ (y1m,y1,y1M); (y2m,y2,y2M); (y3m,y3,y3M); (y4m,y4,y4M); (y5m,y5,y5M); (y6m,y6,y6M) ] (taum y1 y2 y3 y4 y5 y6 + d1 + d2 + d3 > #0.712 \/ y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0)`;; let mk_ineq_hex i1 i2 i3 i4 i5 i6 d126 d234 d135 = let x i = List.nth [`&2`;`#2.17`;`#2.34`;`#2.52`] i in let X i = x (i+1) in let y i = List.nth [`#3.01`;`#3.25`;`#3.5`;`#3.75`;`#3.915`] i in let Y i = y (i+1) in Ineq.mk_tplate template_hex [x i1 ; X i1;x i2;X i2; x i3;X i3; y i4;Y i4;y i5;Y i5;y i6;Y i6;d126;d234;d135];; let make_hex_ear i1 i2 i3 i4 i5 i6 = let d126 = assoc (i1,i2,i6) reformat_ear in let d135 = assoc (i1,i3,i5) reformat_ear in let d234 = assoc (i2,i3,i4) reformat_ear in let desome = function | Some x -> x | None -> failwith "none" in let (d126',d135',d234') = (desome d126,desome d135,desome d234) in { idv = Printf.sprintf "test %d %d %d %d %d %d" i1 i2 i3 i4 i5 i6; ineq = mk_ineq_hex i1 i2 i3 i4 i5 i6 d126' d135' d234'; doc = "local fan/main estimate/terminal hex/body"; tags=[Cfsqp;Xconvert;Penalty(50.0,500.0)]; };; let runhh (i1,i2,i3,i4,i5,i6) = try (run(make_hex_ear i1 i2 i3 i4 i5 i6)) with _ -> () ;; runhh(1,1,0,0,0,3);; (* MANY NEGATIVE! for i1=0 to 2 do for i2=0 to 2 do for i3 = 0 to 2 do for i4 = 0 to 3 do for i5 = i4 to 3 do for i6 = i5 to 3 do runhh (i1,i2,i3,i4,i5,i6) done done done done done done;; *) skip { idv="test"; doc="local fan/main estimate/appendix/terminal hex. full hexagon ear calculation. This shows that if (delta hi > 0) and (delta lo >0) we can erase the ear with small penalty. Hence, when we look at a lo ear, we can wrap it in with the hi ear case when the hi ear exists: (delta hi>0). By symmetry, wlog y2 < y3. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,&2); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (&2,y5,&2); (&2,y6,&2) ] ( (taud y1 y2 y3 y4 y5 y6 > -- #0.07) \/ (y_of_x (delta_sub1_x (#2.52 pow 2)) y1 y2 y3 y4 y5 y6 < &0) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y3 < y2) )`; };; add { idv="4328016440"; doc=" local fan/main estimate/appendix/terminal hex. flat-flat-flat full hexagon with three alternating flats. Big alternating central triangle. Symmetries, wlog y1<y2<y3. secs(357) oldname: test 5338748573 2013 "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > #0.712 ) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/ (y2 < y1) \/ (y3 < y2) )`; };; run2 { idv="1156793592"; doc=" local fan/main estimate/appendix/terminal hex. flat-flat-[234:nonflat,tau>=0] Big alternating central triangle. Symmetries, wlog y1<y2<y3. secs(357) oldname: 'test Z1' By symmetry wlog y5 < y6 sec(454). "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/ (y6 < y5) )`; };; run2 { idv="5429733243"; doc=" local fan/main estimate/appendix/terminal hex. flat-flat-[234:nonflat,y1=2,delta>100] Big alternating central triangle. Symmetries, wlog y1<y2<y3. secs(357) oldname: 'test Z2-100' By symmetry wlog y5 < y6 "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Widthcutoff 0.0001]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/ (y6 < y5) \/ ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (mud_234_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 + &0 - sol0 > #0.712) )`; };; run2 { idv="6941393103"; doc=" local fan/main estimate/appendix/terminal hex. flat-flat-[234:nonflat,y1=2,0<delta<100] Big alternating central triangle. Symmetries, wlog y1<y2<y3. secs(357) oldname: 'test Z2<100' By symmetry wlog y5 < y6 "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Widthcutoff 0.0001]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + // y_of_x (mudLs_234_x (sqrt(&15)) (sqrt(&100)) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 + &0 - sol0 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/ (y6 < y5) // ( taum y1 y2 y3 y4 y5 y6 + // y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + // y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + // &0 - sol0 // > #0.712) \/ )`; };; (* run2 { idv="test Z3"; doc=" local fan/main estimate/appendix/terminal hex/ ear234(lo, tau< -0.07 becomes -- sol0) ear135(flat) ear126(flat) full hexagon with two flats, one lo Big alternating central triangle. By symmetry, wlog y5 < y6. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + &0 - sol0 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/ (y6 < y5) )`; };; *) add { idv="test U1"; doc=" local fan/main estimate/appendix/terminal hex/ full hexagon with two flats, one lo Big alternating central triangle. By symmetry, wlog y5 < y6. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + &0 > #0.712) \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/ (y6 < y5) )`; };; add { idv="test U2"; doc=" local fan/main estimate/appendix/terminal hex/ full hexagon with two flats, one lo Big alternating central triangle. By symmetry, wlog y5 < y6. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + &0 > #0.712) \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; run { idv="test U3"; doc=" local fan/main estimate/appendix/terminal hex/ full hexagon with two flats, one lo Big alternating central triangle. By symmetry, wlog y5 < y6. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (mudLs_126_x (#3.8729) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + &0 > #0.712) \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test U4"; doc=" local fan/main estimate/appendix/terminal hex/ full hexagon with two flats, one lo Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + &0 - sol0 + &0 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test U5"; doc=" local fan/main estimate/appendix/terminal hex/ full hexagon with two flats, one lo Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + &0 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/ (y5 < y6) )`; };; add { idv="test U6"; doc=" local fan/main estimate/appendix/terminal hex/ full hexagon with two flats, one lo Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + y_of_x (mudLs_135_x (#3.8729) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + &0 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test U7"; doc=" local fan/main estimate/appendix/terminal hex/ full hexagon with two flats, one lo Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + &0 - sol0 + &0 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test U8"; doc=" local fan/main estimate/appendix/terminal hex/ full hexagon with two flats, one lo Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (mudLs_126_x (#3.8729) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + y_of_x (mudLs_135_x (#3.8729) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + &0 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/ (y5 < y6) )`; };; add { idv="test U9"; doc=" local fan/main estimate/appendix/terminal hex/ full hexagon with two flats, one lo Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (mudLs_126_x (#3.8729) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + &0 - sol0 + &0 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test U10"; doc=" local fan/main estimate/appendix/terminal hex/ full hexagon with two flats, one lo Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + &0 - &2 * sol0 + &0 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/ (y5 < y6) )`; };; add { idv="test V5"; doc=" local fan/main estimate/appendix/terminal hex/ full hexagon with two flats, one lo Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + &0 - sol0 + &0 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test V6"; doc=" local fan/main estimate/appendix/terminal hex/ full hexagon with two flats, one lo Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + &0 - &2 * sol0 + &0 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/ (y5 < y6) )`; };; add { idv="test 3306409086 2013"; doc=" local fan/main estimate/appendix/terminal hex/ ear234(tau >= -0.07) ear135(flat) ear126(flat) full hexagon with two flats, assumption tau-ear(234) >= - 0.07 Big alternating central triangle. By symmetry wlog y5 < y6 secs(500). "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 - #0.07 + y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/ (y6 < y5) )`; };; add { idv="test 9075398267 2013"; doc=" local fan/main estimate/appendix/terminal hex/ ear234(lo, tau< -0.07 becomes -- sol0) ear135(flat) ear126(flat) full hexagon with two flats, one lo Big alternating central triangle. By symmetry, wlog y5 < y6. secs(467) "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( ( taum y1 y2 y3 y4 y5 y6 - sol0 + y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/ (y6 < y5) )`; };; add2 { idv="test 1324821088 2013"; doc=" local fan/main estimate/appendix/terminal hex/ ear234(flat) ear135(nonflat) ear126(nonflat) one tau-nonflat > -0.07, other tau-nonfalt > 0. This includes nonflats not y1=2. full hexagon with one flat, hi,hi, can zero out both ears. By symmetry, wlog y6 > y5. sec(731) "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 - #0.07 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > #0.712) \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/ (y5 < y6) )`; };; add { idv="test 1324821088 2013 b"; doc="full hexagon with one flat, hi,hi, can zero out both ears. Big alternating central triangle. ear234(flat), ear126( extra assumption, ear126 has delta < 50. By symmetry, wlog y4 < y5. The constant 0.013 comes from 2535350075. We add constant in on the hi case, even though it isn't needed here. To permit simplification of the lo case later. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 - &2 * #0.07 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > #0.712) \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &50 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test 1324821088 2013 c"; doc="full hexagon with one flat, hi,hi, can zero out both ears. Big alternating central triangle. ear234(flat), ear126( extra assumption, ear126 has delta > 50. By symmetry, wlog y4 < y5. The constant 0.013 comes from 2535350075. We add constant in on the hi case, even though it isn't needed here. To permit simplification of the lo case later. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 - &2 * #0.07 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > #0.712) \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 > &0 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &50 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test 1324821088 2013 d"; doc="full hexagon with one flat, hi,hi, can zero out both ears. Big alternating central triangle. ear234(flat), ear126( extra assumption, ear126 has delta > 50. By symmetry, wlog y4 < y5. The constant 0.013 comes from 2535350075. We add constant in on the hi case, even though it isn't needed here. To permit simplification of the lo case later. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 - #0.07 - sol0 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > #0.712) \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ // y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 > -- #0.07 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &10 \/ y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test 1324821088 2013 e"; doc="full hexagon with one flat, hi,hi, can zero out both ears. Big alternating central triangle. ear234(flat), ear126( extra assumption, ear126 has delta > 50. By symmetry, wlog y4 < y5. The constant 0.013 comes from 2535350075. We add constant in on the hi case, even though it isn't needed here. To permit simplification of the lo case later. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 - #0.07 + y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > #0.712) \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &10 \/ y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test 1324821088 2013 f"; doc="full hexagon with one flat, hi,hi, can zero out both ears. Big alternating central triangle. ear234(flat), ear126( extra assumption, ear126 has delta > 50. By symmetry, wlog y4 < y5. The constant 0.013 comes from 2535350075. We add constant in on the hi case, even though it isn't needed here. To permit simplification of the lo case later. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 - &2 * sol0 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > #0.712) \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test 1324821088 2013 g"; doc="full hexagon with one flat, hi,hi, can zero out both ears. Big alternating central triangle. ear234(flat), ear126( extra assumption, ear126 has delta > 50. By symmetry, wlog y4 < y5. The constant 0.013 comes from 2535350075. We add constant in on the hi case, even though it isn't needed here. To permit simplification of the lo case later. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 - &2 * sol0 + y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > #0.712) \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add2 { idv="test B"; doc=""; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] ( (taum y1 y2 y3 y4 y5 y6 > #0.712 ) \/ y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0 \/ y4 < y5 \/ y5 < y6 )`; };; add { idv="test B1"; doc="full hexagon tau+, tau+, tau- Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 + &0 - sol0 > #0.712) \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/ (y5 < y6) )`; };; add { idv="test B2"; doc="full hexagon tau+, tau+, tau- Big alternating central triangle. extra assumption, ear126 has delta > 50. sqrt(15)> 3.8729. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 + y_of_x (mudLs_234_x (#3.8729) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 > #0.712) \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test B3"; doc="full hexagon tau+, tau+, tau- Big alternating central triangle. extra assumption, ear126 has delta > 50. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 + y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test C1"; doc="full hexagon tau+, tau-, tau- Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 + &0 - sol0 + &0 - sol0 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test C2"; doc="full hexagon tau+, tau-, tau- Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 + y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + &0 - sol0 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test C3"; doc="full hexagon tau+, tau-, tau- Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 + y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 > #0.712) \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test D1"; doc="full hexagon tau-, tau-, tau- Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 + &0 - &3 * sol0 > #0.712) \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test D2"; doc="full hexagon tau-, tau-, tau- Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 + y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + &0 - &2 * sol0 > #0.712) \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test D3"; doc="full hexagon tau-, tau-, tau- Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 + y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + &0 - &1 * sol0 > #0.712) \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test D4"; doc="full hexagon tau-, tau-, tau- Big alternating central triangle. "; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (#3.01,y5,#3.915); (#3.01,y6,#3.915) ] (( taum y1 y2 y3 y4 y5 y6 + y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 + y_of_x (mud_234_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 > #0.712) \/ y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/ (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) )`; };; add { idv="test"; doc=""; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,&2); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (&2,y5,&2); (&2,y6,&2) ] ( taud y1 y2 y3 y4 y5 y6 > taud (#2.52) y2 y3 y4 y5 y6 \/ delta_y y1 y2 y3 y4 y5 y6 < &0 \/ delta_y (#2.52) y2 y3 y4 y5 y6 < &0 )`; };; add { idv="test"; doc=""; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (#2.0,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (&2,y5,&2); (&2,y6,&2) ] ( (taum y1 y2 y3 y4 y5 y6 > &0 \/ (delta_y y1 y2 y3 y4 y5 y6 > &20) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0) ))`; };; add { idv="test"; doc=""; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (#2.0,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (&2,y5,&2); (&2,y6,&2) ] ( (y4 > #3.01 ) \/ taum y1 y2 y3 y4 y5 y6 > -- #0.337 \/ (delta_y y1 y2 y3 y4 y5 y6 < &0) )`; };; skip { idv="4795451128"; doc="old name: taud hex* test (also works with taud_v2)"; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (&2,y4,#2.52); (&2,y5,#2.52); (&2,y6,#2.52); (#3.01,z1,#3.915); (#3.01,z3,#3.915); (#3.01,z5,#3.915) ] ( (taum y1 y3 y5 z1 z3 z5 + taud y4 y3 y5 z1 (&2) (&2) + taud y6 y5 y1 z3 (&2) (&2) + taud y2 y1 y3 z5 (&2) (&2) > #0.712) \/ delta_y y1 y3 y5 z1 z3 z5 < &0 \/ delta_y y4 y3 y5 z1 (&2) (&2) < &0 \/ delta_y y6 y5 y1 z3 (&2) (&2) < &0 \/ delta_y y2 y1 y3 z5 (&2) (&2) < &0 \/ y_of_x eulerA_x y1 y3 y5 z1 z3 z5 < &0)`; };; run2 { idv="1948775510"; doc="was test Q. local fan/main estimate/terminal pent LHS(135,y1=2.52,delta=>20) RHS(126,delta=0) "; tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (&2,y4,&2); (#3.01,y5,#3.237); (#3.01,y6,#3.237) ] (taum y1 y2 y3 y4 y5 y6 + y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 + y_of_x (mud_135_x_v1 (&2 * h0) (&2) (&2)) y1 y2 y3 y4 y5 y6 > #0.616 \/ y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &20 \/ y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 // \/ // y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 )`; };; run { idv="test-hex-numerical-taud"; doc="For cfsqp only. This is the numerator of the 2nd derivative of the function taud."; tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (&2,y5,&2); (&2,y6,&2) ] (((y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6) pow 2 > &0) \/ (y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/ taud y1 y2 y3 y4 y5 y6 > #0.0 \/ // can adjust this later. delta_y y1 y2 y3 y4 y5 y6 < &15))`; };; run { idv="test 9692636487"; doc="local fan/main estimate/appendix/terminal hex. 2nd derivative test for taud."; tags=[Main_estimate;Flypaper ["LIAULBV"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (&2,y5,&2); (&2,y6,&2) ] ( (y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/ delta_y y1 y2 y3 y4 y5 y6 < &0) \/ delta_y y1 y2 y3 y4 y5 y6 > &15 )`; };; add { idv="2735164514"; doc="l"; tags=[Main_estimate;Flypaper ["LIAULBV"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)]; ineq = all_forall `ineq [ (&2,y1,#2.52); (&2,y2,#2.52); (&2,y3,#2.52); (#3.01,y4,#3.915); (&2,y5,&2); (&2,y6,&2) ] (y_of_x delta_x1 y1 y2 y3 y4 y5 y6 < &0 \/ &0 < y_of_x (delta_sub1_x (&4)) y1 y2 y3 y4 y5 y6 ) `; };; map Scripts.one_cfsqp ["test8"];; map Scripts.one_cfsqp ["taum pent3"];; Ineq.remove "test25353";; Auto_lib.testsplit true "5556646409 small domain";; let flyspeck_needs_status filename (badfile,badmsg,ok) = if not(ok) then (badfile,badmsg,ok) else try (flyspeck_needs filename); (badfile,badmsg,ok) with Failure t -> (filename,t,false);; let flyspeck_needs_list filenames = let (badfile,badmsg,ok) = itlist flyspeck_needs_status filenames ("","",true) in if ok then report "full load completed" else (report ("Failure in file "^badfile); report badmsg);; flyspeck_needs_status "../development/thales/session/test1.hl" ("","",true);; flyspeck_needs_status "../development/thales/session/test2.hl" ("","",true);; map flyspeck_needs ["../development/thales/session/test1.hl"; "../development/thales/session/test2.hl"];; flyspeck_needs_list ["../development/thales/session/test1.hl"; "../development/thales/session/test2.hl"];; flyspeck_needs_list ["../development/thales/session/test1.hl"; "../development/thales/session/test1.hl"];; rflyspeck_needs "../development/thales/session/test1.hl";; Test1.test;;