(* 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;;