addtex(Comment,"","
The actual definitions of these functions need to be supplied.
For now, the functions only get used in cfsqp and interval verifications.

The LC functions are implemented in intervals as locally constant functions.
");;

(* true definitions in mdtau.hl *)


let mdtau_fake = new_definition
  `mdtau (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real)  = &0`;;
let mdtau2_fake = new_definition
  `mdtau2 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real)  = &0`;;
addtex (Section,"Main Estimate","Ears, top edges 2,2,long");;


add
{
  idv="4322269127";
  doc="taum 1st deriv test. 
   This shows that the first derivative of tau (wrt y1) is nonzero.  
  Thus the  optimal configuration has delta > 15 or (y1 minimal = 2)
   It is implemented in interval code, using locally constant structures (LC).";
  tags=[Flypaper["TNNOPSI"];Main_estimate;Tex;Disallow_derivatives;Penalty(50.0,500.0);];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.915);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
  ( mdtau_y_LC y1 y2 y3 y4 y5 y6  > &0) \/
  ( mdtau_y_LC y1 y2 y3 y4 y5 y6  < &0) \/
  (delta_y_LC y1 y2 y3 y4 y5 y6 > &15) \/
  (delta_y_LC y1 y2 y3 y4 y5 y6 < &0)
 )`;
};;

skip
{
  idv="4322269127 cfsqp version";
  doc="taum 1st deriv test.  This is the cfsqp version of 4322269127.
    It is not to be proved, only used as numerical evidence.";
  tags=[Flypaper["TNNOPSI"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.915);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
  ( mdtau y1 y2 y3 y4 y5 y6 pow 2 > #0.47) \/ // fake
  (delta_y y1 y2 y3 y4 y5 y6 > &15) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0)
 )`;
};;


add
{
  idv="5556646409";
  doc="taum 2nd deriv test.  This is a key inequality.
   It asserts that taum has no local minimum on the given domain.
   If the derivative is zero, then the second derivative is negative.
   By symmetry, wlog y2 < y3.
   The C++ code has been customized for this particular inequality.
   The C++ has an embedded assumption that mdtau2_y_LC is on the domain delta>=15.
   Case delta<=15 is done in 4322269127.
   ";
  tags=[Flypaper["TNNOPSI"];Main_estimate;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.915);
    (&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) 
 )`;
};;

skip
{
  idv="5556646409 cfsqp version";
  doc="taum 2nd deriv test. Cfsqp version -- only for testing.";
  tags=[Flypaper["TNNOPSI"];Main_estimate;Cfsqp;Tex;Penalty(1500.0,5000.0);Deprecated];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.915);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
  (mdtau y1 y2 y3 y4 y5 y6 pow 2 > #0.004) \/ // fake
  (mdtau2 y1 y2 y3 y4 y5 y6 < -- #0.004) \/  // fake
  (delta_y y1 y2 y3 y4 y5 y6 < &15)
 )`;
};;

skip
{
  idv="5132343267";
  doc="delta monotonicity.
   In the interval code for 5556646409,
   the interval implementation of delta_y_LC assumes this  monotonicity
    results.  This calculation is not cited explicitly in the code, but still needed.
  -
   Deprecated.  This is a consequence of 4559601669, which asserts that
   the wide angle of a skinny triangle (ear) is obtuse.";
  tags=[Flypaper["TNNOPSI"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.915);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
  ( delta4_y y1 y2 y3 y4 y5 y6 < &0)
 )`;
};;

skip
{
  idv="7479785942";
  doc="delta monotonicity (for edge y5 and by symmetry y6).
   In the interval code for 5556646409,
   the interval implementation of delta_y_LC assumes various  monotonicity
    results.  This is among them.
    -
   This is a consequence of 2485876245. No separate verification is needed.
  ";
  tags=[Flypaper["TNNOPSI"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,&2);
    (&2,y3,&2);
    (&2,y4,#2.52);
    (#3.01,y5,#3.915);
      (&2,y6,#2.52)
  ]
(
  ( delta4_y y1 y2 y3 y4 y5 y6 > &0)
 )`;
};;

addtex (Section,"Main Estimate","June Hexagons, top edges all 2.");;

addtex(Comment,"Main Estimate",
"
");;

add
{
  idv="5338748573";
  doc="full hexagon with three alternating flats.
    Big alternating central triangle.
    Symmetries, wlog y1<y2<y3.
    y4 y5 y6 are non-standard indexing of variables.
    They are the heights of the enclosed flat nodes.
    ";
  tags=[Flypaper["SAUZWSD"];Main_estimate;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)
  ]
(
  (y_of_x taum_3flat_x y1 y2 y3 y4 y5 y6 > #0.712 ) \/
    (y_of_x euler_3flat_x y1 y2 y3 y4 y5 y6 < &0) \/
    (y2 < y1) \/ (y3 < y2)
 )`;
};;

add
{
  idv="3306409086";
  doc="full hexagon with two flats, one hi, can zero out the hi ear.
    Big alternating central triangle.
    By symmetry wlog y5 < y6
    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=[Flypaper["SAUZWSD"];Main_estimate;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.52);
    (&2,y6,#2.52)
  ]
(
  (y_of_x taum_2flat_x y1 y2 y3 y4 y5 y6
    > #0.712 + #0.013) \/
   y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ 
     (y_of_x euler_2flat_x y1 y2 y3 y4 y5 y6<  &0)  \/
   (y6 < y5)
 )`;
};;

add
{
  idv="9075398267";
  doc="full hexagon with two flats, one lo
    Big alternating central triangle.
   To stabilize near delta=0, we  erases and takes a penalty.
    By symmetry, wlog  y5 < y6.
    The constant 0.013 comes from 2535350075.
    The extra disjuncts are justified by that calc and by
    the stronger ineq proved in '3306...'
    ";
  tags=[Flypaper["SAUZWSD"];Main_estimate;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.52);
    (&2,y6,#2.52)
   ]
(
  (y_of_x taum_2flat_x y1 y2 y3 y4 y5 y6
   > #0.712 + sol0) \/
  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 euler_2flat_x y1 y2 y3 y4 y5 y6<  &0) \/
   (y6 < y5)
 )`;
};;

add
{
  idv="1324821088";
  doc="full hexagon with one flat, hi,hi, can zero out both ears.
    Big alternating central triangle.
    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=[Flypaper["SAUZWSD"];Main_estimate;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);
      (&2,y6,#2.52)
  ]
(
  (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y6  > #0.712 + &2 * #0.013) \/
  y_of_x (delta_234_x (#2.52 pow 2) (&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  \/
  y5 < y4 \/
     ( y_of_x euler_1flat_x y1 y2 y3 y4 y5 y6< &0) 
 )`;
};;

add
{
  idv="4108834026";
  doc="full hexagon with one flat, ears: hi,lo, can zero  out hi ear.
    Big alternating central triangle.
   To stabilize near delta=0, we add  a disjunct that erases and takes a penalty.
    The constant 0.013 comes from 2535350075.
    The extra disjuncts are justified by that calc and by
    the stronger ineq proved in '132482...'
    ";
  tags=[Flypaper["SAUZWSD"];Main_estimate;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);
      (&2,y6,#2.52)
  ]
(
  (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y6 +
 y_of_x (taum_sub246_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  > #0.712 + #0.013) \/
 (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y6  > #0.712 + #0.013 + sol0) \/
  y_of_x (delta_234_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 euler_1flat_x y1 y2 y3 y4 y5 y6< &0) 
 )`;
};;

add
{
  idv="6388508112";
  doc="full hexagon with one flat, ears: lo,lo
    Big alternating central triangle.
    If delta hi>0, take the penalty and erase.
    By symmetry, wlog 0  < delta234 < delta135
    To stabilize near delta=0, we add  disjuncts that erase and take a penalty.
    ";
  tags=[Flypaper["SAUZWSD"];Main_estimate;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);
      (&2,y6,#2.52)
  ]
(
  (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y6 +
      y_of_x (taum_sub246_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > 
   #0.712 + sol0) \/
  (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y6
   > #0.712 + &2 * sol0) \/
  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_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  < 
 y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  \/
    y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  \/
     ( y_of_x euler_1flat_x y1 y2 y3 y4 y5 y6< &0) 
 )`;
};;


add
{
  idv="5493250206";
  doc="full hexagon with no flats, three ears: hi,hi,hi, can zero out all ears.
    Big alternating central triangle.
    By symmetry y1 < y2 < y3
    ";
  tags=[Flypaper["SAUZWSD"];Main_estimate;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 + &3 * #0.013) \/
   y_of_x (delta_234_x (#2.52 pow 2) (&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_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) \/
    (y2 < y1) \/ (y3 < y2)
 )`;
};;

add
{
  idv="2283016857";
  doc="full hexagon with no flats, three ears: hi,hi,lo=126, zero out hi ears.
    Big alternating central triangle, extremal ears.
    To stabilize near delta=0, we add  a disjunct that erases and takes a penalty.
    By symmetry, y4<y5.
    ";
  tags=[Flypaper["SAUZWSD"];Main_estimate;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 (taum_sub345_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6
    > #0.712 + &2 * #0.013) \/
 (taum y1 y2 y3 y4 y5 y6  
    > #0.712 + &2 * #0.013 + sol0) \/
    y_of_x (delta_234_x (#2.52 pow 2) (&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_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 eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/ (y5 < y4)
 )`;
};;

add
{
  idv="4872337467";
  doc="full hexagon with no flats, three ears: hi,lo,lo, zero out hi  ear.
    Big alternating central triangle, extremal ears.
    By symmetry, wlog 0  < delta135 < delta126
    To stabilize near delta=0, we add  disjuncts that erase and take a penalty.
    ";
  tags=[Flypaper["SAUZWSD"];Main_estimate;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 (taum_sub345_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6
    > #0.712 + #0.013 + sol0) \/
 (taum y1 y2 y3 y4 y5 y6 
    > #0.712 + #0.013 + &2 * sol0) \/
     y_of_x (delta_234_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_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 <   
 y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  \/
     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="3615835903";
  doc="full hexagon with no flats, three ears: low, low, low
    Big alternating central triangle, extremal ears.
    By symmetry, wlog, we may order the delta terms.
    0 < delta234 < delta135 < delta126
    To stabilize near delta=0, we add  disjuncts that erase and take a penalty.
    ";
  tags=[Flypaper["SAUZWSD"];Main_estimate;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 (taum_sub345_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6
    > #0.712 + &2 * sol0) \/
(taum y1 y2 y3 y4 y5 y6  
    > #0.712 + &3 * sol0) \/
    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_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 <  y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6   \/
     y_of_x (delta_135_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 <   
  y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6  \/
    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="2535350075";
  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=[Flypaper["SAUZWSD"];Main_estimate;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)
  ]
( 
 (taum 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)
 )`;
};;

addtex (Section,"Main Estimate","Pentagons, all top edges 2");;
(* New Pentagons,  June 3, 2011.
 This section completely treats all kinds of
   pentagons, modulo cases with a diagonal <= 3.01.  *)


add
{
  idv="7067938795";
  doc="A pentagon cannot have two straights.  This is the A-piece dihedral bound.
    If a pentagon has two straights then
     pi /2 < dih y1 _ _ 3.01 2 2 < dih_y.  This is impossible, by this calc.
    This estimate also gets used on straight+hi.";
  tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (#3.01,y5,#3.24);
      (#3.01,y6,#3.24)
  ]
(
  ( dih_y y1 y2 y3 y4 y5 y6 < pi / &2 - #0.46)
 )`;
};;


add
{
  idv="9459075374";
  doc="(EAR) A bound on the delta of an ear in a pent, when the pent has a straight on the other side.
   The disjunct   (dih_y y1 y2 y3 y4 y5 y6 < #0.46)  has been 'linearized'. 
   Tan[0.46]^2 = 0.245469...
   In more detail, this calc shows that delta > 30.2 or dih < 0.46.
   By obtuse calcs, we know that the combined angle at the node is
   at least pi/2.  If we have a straight node, and dih < 0.46, then
   the combined angle is less than 0 + 0.46 + (pi/2 - 0.46) =pi/2 by
   '7067938795'.  Hence a flat on the other side ==> delta of this ear > 30.2.
   ";
  tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.52,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
     (#3.01,y5,#3.24);
      (&2,y6,#2.52)
  ]
(let tan2lower = #0.245468 in
   (delta_y y1 y2 y3 y4 y5 y6 > #30.2) \/
  (&4 * x1_delta_y y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6)
 )`;
};;


add
{
  idv="2559885109";
  doc="(EAR) A pentagon lo ear bound";
  tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);];
  ineq = all_forall `ineq [
    (&2,y1,&2);
    (&2,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)
 )`;
};;

add
{
  idv="9861833891";
  doc="pent+hi+something that we can zero out.
    This and '8199484193' do the case of no straight nodes.
    ";
  tags=[Flypaper["EDZEPIH"];Main_estimate;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.24);
      (#3.01,y6,#3.24)
  ]
( taum y1 y2 y3 y4 y5 y6 +
    y_of_x (taum_sub345_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6  > #0.616 \/
  taum y1 y2 y3 y4 y5 y6   > #0.616
 )`;
};;

add
{
  idv="8199484193";
  doc="pent+lo+something that we can zero out.
    (We can zero out anything but a straight node.)
    This and '9861833891' do the case of no straight nodes.
    ";
  tags=[Flypaper["EDZEPIH"];Main_estimate;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.24);
      (#3.01,y6,#3.24)
  ]
( taum y1 y2 y3 y4 y5 y6 +
   y_of_x (taum_sub345_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6
   > #0.616
 )`;
};;


add
{
  idv="3980286827";
  doc="pent+straight126+lo
  The delta_pent >0 iff  edge_flat y6 y1 y2  _   (&2) (&2) > #3.24 
  The straight goes along 126.
  the low is placed along 135.
  The variable called y6 is in fact the ht of enclosed straight node
  along the (1,2,6) face.  The edge |v1-v2| is computed by taum_1flat.
   delta_pent_x = delta_x x1 x2 x6 4 4 3.24^2.
    ";
  tags=[Flypaper["EDZEPIH"];Main_estimate;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.24);
      (&2,y6,#2.52)
  ]
( y_of_x taum_1flat_x y1 y2 y3 y4 y5 y6 + 
   y_of_x (taum_sub246_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6
     > #0.616 \/
   y_of_x (delta_pent_x) y1 y2 y3 y4 y5 y6 > &0
 )`;
};;

add
{
  idv="3221740746 a";
  doc="pent+straight126+hi
   delta_pent_x = delta_x x1 x2 x6 4 4 3.24^2.
    has non-standard ordering of variables, x3<->x6.
    y6 = ht of the straight node on the y1-y2-* face.
    ";
  tags=[Flypaper["EDZEPIH"];Main_estimate;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.24);
      (&2,y6,#2.52)
  ]
( y_of_x taum_1flat_x y1 y2 y3 y4 y5 y6 + 
     y_of_x (taum_sub246_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > #0.616 \/
    (y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 < #30.2) \/
    y_of_x (delta_pent_x) y1 y2 y3 y4 y5 y6 > &0
 )`;
};;

(* We have finished the main part of the verification of pents.
   These last calculations show that none of the three nodes on
   the big inner triangle can be straight.  So we don't need to
   worry about this, when making calculations. *)

add
{
  idv="8520556953";
  doc="(EAR) no straights on vertices of big inner triangle of pent.  
  This is the skinny triangle (ear) bound.
   Upper bound on y6 is 1+Sqrt[5].
   Need to do a dih replacement.
   Tan[1.001]^2 > 2.43621.
   The disjunct implies dih < #1.001.
    Combine this with '9977174768'
    ";
  tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = 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.23607)
  ]
(
  let tan2lower = #2.43621 in
  ( &4 * x1_delta_y  y1 y2 y3 y4 y5 y6 < tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) 
 )`;
};;

add
{
  idv="9977174768";
  doc="no straight nodes on big inner triangle of pent.
   Upper bound on y6 is 1+Sqrt[5].
      Tan[1.001]^2 > 2.43621.
   The disjunct implies dih < pi - #1.001.
   Combine this with '8520556953'.
    ";
  tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.23607);
    (&2,y5,&2);
      (#3.01,y6,#3.23607)
  ]
( dih_y y1 y2 y3 y4 y5 y6 < pi - #1.001)`;
};;


skip
{
  idv="6281973111";
  doc="no straight node on big inner triangle of pent.
   Upper bound on y6 is 1+Sqrt[5].
   Moved to skipped May 26, 2012.  It is a special case of '7067938795'
   This is used to prove that the node of the pentagon with three
   triangles is not straight:
     (pi - 2 1.001) + 1.001 + 1.001 <= pi.)
    ";
  tags=[Flypaper["EDZEPIH"];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (#3.01,y5,#3.23607);
      (#3.01,y6,#3.23607)
  ]
(
  ( dih_y y1 y2 y3 y4 y5 y6 < pi - &2 * #1.001) 
 )`;
};;

Functional_equation.functional_overload();;

(* May 9, 2013. taud function.  taud_v4 seems to be the version that
   works in all cases (pent and hex).  *)


    let add = Ineq.add;;

    let skip = Ineq.skip;;

    let all_forall = Sphere.all_forall;;


run
{
  idv="test";
  doc="
    local fan/main estimate/terminal pent
    LHS(135,delta=20) RHS(126,delta=0)
    ";
  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 (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
       y_of_x mu6_x 
//       y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0
     > #0.616) \/
      y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > d ))
`;
};;





(* Scratch area *)

(*
let runhh i234 i126 i135 = try (run(make_hex_ear i234 i126 i135)) with _ -> () ;;
let run2hh i234 i126 i135 = try (
  let _ = run2(make_hex_ear i234 i126 i135) in ()) with _ -> () ;;

*)



let install_functions () = 
  let _ = map Parse_ineq.autogen_add [mu_y;delta_x1;taud;] in
  let _ = map Parse_ineq.macro_add[ mud_135_x;
			      mud_126_x;mud_234_x;mudLs_234_x;mudLs_135_x;mudLs_126_x;
			      taud_x;nonfunctional_mu6_x;nonfunctional_taud_D1;
			    nonfunctional_taud_D2;
			    nonfunctional_edge2_126_x;
			    nonfunctional_edge2_135_x;
			    nonfunctional_edge2_234_x;
			    flat_term2_126_x;
				       flat_term2_135_x;flat_term2_234_x] in
  let _ = map Function_list.function_add
    [ functional_delta_x1;mu6_x;taud_x_ALT;taud_D2_num_x;taud_D1_num_x;
    functional_mud_135_x;functional_mud_126_x;functional_mud_234_x;mudLs_234_x;mudLs_126_x;mudLs_135_x;
    ups_126;
    functional_edge2_126_x;functional_edge2_135_x;functional_edge2_234_x;
    flat_term2_126_x;flat_term2_135_x;flat_term2_234_x] in
    "remember to reload Auto_lib, etc.";;

(*
    map Parse_ineq.autogen_remove [edge_flatD_x1;taud_v4_D2_num;taud;taud_D2_num_x];; 
    map Parse_ineq.macro_remove [taud_D2_num_x;edge_126_x;edge_135_x;
				 functional_edge_135_x;flat_term_126_x;flat_term_135_x;
				functional_edge_126_x;mudd_135_x;mudd_126_x;			   
      mudd_135_x_v2;mudd_126_x_v2;
];; 

   map Function_list.function_remove [mu_y;taud_x;delta_x1;functional_edge_126_x;
				       functional_edge_135_x;];; 
*)


Parse_ineq.autogen_remove mudL_234_x;;
Function_list.function_remove mudL_234_x;;
1;;    


(*

flyspeck_needs "nonlinear/scripts.hl";;

    let run s = 
      let _ = Ineq.add s in
	Scripts.one_cfsqp s.idv;;

    rflyspeck_needs   "nonlinear/auto_lib.hl";;

    let run2 s = 
      let _ = Ineq.add s in
	Auto_lib.testsplit true s.idv;;

    let run2f s = 
      let _ = Ineq.add s in
	Auto_lib.testsplit false s.idv;;



Auto_lib.testsplit true "7796879304";;
map (Auto_lib.testsplit true)  cases;;
  

map Scripts.one_cfsqp cases;;
*)

map (Auto_lib.testsplit true) ["test U1";"test U2";"test U3";
"test U4";"test U5";"test U6";
"test U7";"test U8";"test U9";
"test U10";];;