(* PRE MAY 2012 STARTS HERE *)

CE to hexall 5A1:

{4.0367249999999996746,4.0367249999999996746,4.0367249999999996746,5.9464250000000058449,6.3876093749999940385,1.000000000000000222} {4.0367249999999996746,4.0367249999999996746,4.0367249999999996746,5.9464250000000058449,6.3876093749999940385,1.000000000000000222}  isolated point
function 0 value=[2.2566633457319120737,2.2566633457353155734]
T0 partial 0: [21.159337943191999898,21.159337943193165188]
T0 partial 1: [68.637638901404642411,68.63763890140612034]
T0 partial 2: [8.103456502905828529,8.103456502906908554]
T0 partial 3: [-65.817170105080634812,-65.817170105079782161]
T0 partial 4: [52.739287222031975944,52.739287222032274371]
T0 partial 5: [-0,0]
counterexample found 
FAIL


let all_forall = Sphere.all_forall;;
Parse_ineq.execute_cfsqp;;
(* still need pent cases with 2 flats *) 







Parse_ineq.execute_cfsqp  
{
idv = "test 298";
doc = "298 supplement for pent_acute case. No use.";
tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
ineq = all_forall `ineq
 [
   (&2,y1,&2 * h0);
   (&2,y2,&2 * h0);
   (&2,y3,&2 * h0);
   (&2 * h0 ,y4,&4*h0);
   (sqrt(&10),y5,#3.915);
   (&2,y6,&2 * h0)
 ] (
  ( dih3_y y1 y2 y3 y4 y5 y6 < dih_y y3 (#2.52) (&2) (#2.52) (#2.52) (&2) \/   delta4_y y1 y2 y3 y4 y5 y6 < &0
    ))`;
};; 

Parse_ineq.execute_cfsqp  
{
idv = "test 298";
doc = "298 supplement for pent_acute case. No use.";
tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
ineq = all_forall `ineq
 [
   (&2,y1,&2 * h0);
   (&2,y2,&2 * h0);
   (&2,y3,&2 * h0);
   (#3.0 ,y4,&4*h0);
   (sqrt(&10),y5,#3.915);
   (&2,y6,&2 * h0)
 ] (
  ( dih2_y y1 y2 y3 y4 y5 y6  < &0  \/  dih_y y1 y2 y3 y4 y5 y6 < #1.15 \/ delta4_y y1 y2 y3 y4 y5 y6 < &0
    ))`;
};; 


Parse_ineq.execute_cfsqp  
{
idv = "test pent";
doc = "298 supplement for pent case";
tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
ineq = all_forall `ineq
 [
   (&2,y1,&2);
   (&2,y2,&2);
   (&2,y3,&2);
   (&2*h0 ,y4,&4);
   (&2,y5,#3.915);
   (&2,y6,&2 * h0)
 ] (
  ( y4 < #3.416 \/ delta4_y y1 y2 y3 y4 y5 y6 < &0  )
    )`;
};; 


Parse_ineq.execute_cfsqp  
{
idv = "test pent";
doc = "298 supplement for pent case";
tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
ineq = all_forall `ineq
 [
   (&2,y1,&2);
   (&2,y2,&2);
   (&2,y3,&2);
   (&2*h0 ,y4,&4);
   (&2,y5,&2 * h0);
   (&2,y6,&2 * h0)
 ] (
  ( sol_y y1 y2 y3 y4 y5 y6 > #0.46 \/ dih_y y1 y2 y3 y4 y5 y6 > #2.614 )
    )`;
};; 



Parse_ineq.execute_cfsqp  
{
idv = "test pent";
doc = "298 supplement for pent case";
tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
ineq = all_forall `ineq
 [
   (&2,y1,&2 * h0);
   (&2,y2,&2 * h0);
   (&2,y3,&2 * h0);
   (&2*h0 ,y4,&4 * h0);
   (&2,y5,#3.915);
   (&2,y6,&2 * h0);
   (&2,y6,&
 ] (
  ( taum y1 y2 y3 y4 y5 y6 > &0 \/ delta4_y y1 y2 y3 y4 y5 y6 < &0  )
    )`;
};; 




Parse_ineq.execute_cfsqp  
{
idv = "test W";
doc = "";
tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
ineq = all_forall `ineq
 [
   (&2,y1,&2 * h0);
   (&2,y2,&2 * h0);
   (&2,y3,&2 * h0);
   (&2 ,y4,&2);
   (#2.9,y5,#3.47);
   (#2.9,y6,#3.93)
 ] (
  (dih_y y1 y2 y3 y4 y5 y6 < #1.47) 
    )`;
};; 

Parse_ineq.execute_cfsqp  
{
idv = "test W2";
doc = "";
tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
ineq = all_forall `ineq
 [
   (&2,y1,&2 * h0);
   (&2,y2,&2 * h0);
   (&2,y3,&2 * h0);
   (&2 * h0,y4,&2 * h0);
   (#2.9,y5,#3.47);
   (#2.9,y6,#3.47)
 ] (
  (dih_y y1 y2 y3 y4 y5 y6 < #1.64) 
    )`;
};; 

Parse_ineq.execute_cfsqp  
{
idv = "test W3 junk";
doc = "";
tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
ineq = all_forall `ineq
 [
   (&2,y1,&2 * h0);
   (&2,y2,&2 * h0);
   (&2,y3,&2 * h0);
   (&2 * h0,y4,&4 * h0);
   (&2,y5,&2 * h0);
   (&2,y6,&2 * h0)
 ] (
   (arclength y2 y3 y4 > #2.42 - #0.88) \/
  (taum y1 y2 y3 y4 y5 y6 > #0.103) 
    )`;
};; 








1;;



1;;

(* SECTION 1607135856 *)

Parse_ineq.execute_cfsqp
{
idv = "test 1607135856 F";
doc = "
";
tags= [Tex;Cfsqp;Xconvert;Penalty(100.0,10000.0);Flypaper];
ineq = all_forall `ineq
 [
   (&2,y1,&2 * h0);
   (&2,y2,&2 * h0);
   (&2,y3,&2 * h0);
   (&2 * h0,y4,&4 * h0);
   (&2,y5,&2);
   (&2 * h0,y6,&4 * h0)
 ] (
   let costheta = -- #0.915903125 in
   let cos1981 = -- #0.39879 in
   let tan2lower = #0.15043 in
  (delta_y y1 y2 y3 y4 y5 y6 > &14) \/
(&4 * x1_delta_y y1 y2 y3 y4 y5 y6 <  tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6)  \/
    (delta4_y y1 y2 y3 y4 y5 y6 > &0) \/
  (y_of_x (law_cosines_126_x cos1981) y1 y2 y3 y4 y5 y6 > &0) \/
    (y_of_x (law_cosines_234_x costheta) y1 y2 y3 y4 y5 y6  < &0)
    )`;
(* Cos[arc[2,2,3.915]] = -0.915903125
   segment with dih > pi/2.
  (dih_y y1 y2 y3 y4 y5 y6 > pi - #0.37) \/, removed.
  Tan[Pi-0.37]^2 approx 0.150438
 *)
};; 

skip
{
idv = "test 1607135856 F";
doc = "
";
tags= [Tex;Cfsqp;Xconvert;Penalty(100.0,10000.0);Flypaper];
ineq = all_forall `ineq
 [
   (&2,y1,&2 * h0);
   (&2,y2,&2 * h0);
   (&2,y3,&2 * h0);
   (&2 * h0,y4,&4 * h0);
   (&2,y5,&2);
   (&2 * h0,y6,&4 * h0)
 ] (
   let costheta = -- #0.915903125 in
   let cos1981 = -- #0.39879 in
   let tan2lower = #0.15043 in
  (delta_y y1 y2 y3 y4 y5 y6 > &14) \/
(&4 * x1_delta_y y1 y2 y3 y4 y5 y6 <  tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6)  \/
    (delta4_y y1 y2 y3 y4 y5 y6 > &0) \/
  (y_of_x (law_cosines_126_x cos1981) y1 y2 y3 y4 y5 y6 > &0) \/
    (y_of_x (law_cosines_234_x costheta) y1 y2 y3 y4 y5 y6  < &0)
    )`;
(* Cos[arc[2,2,3.915]] = -0.915903125
   segment with dih > pi/2.
  (dih_y y1 y2 y3 y4 y5 y6 > pi - #0.37) \/, removed.
  Tan[Pi-0.37]^2 approx 0.150438
 *)
};; 


Parse_ineq.execute_cfsqp
{
idv = "test 1607135856 G";
doc = "
";
tags= [Tex;Cfsqp;Xconvert;Penalty(50000.0,10000.0);Flypaper];
ineq = all_forall `ineq
 [
   (&2,y1,&2 * h0);
   (&2,y2,&2 * h0);
   (&2,y3,&2 * h0);
   (&2 * h0,y4,&4 * h0);
   (&2,y5,&2);
   (&2 * h0,y6,&4 * h0)
 ] (
   let costheta = -- #0.915903125 in
   let cos1981 = -- #0.39879 in
   let tan2lower = #0.15043 in
   (taum y1 y2 y3 y4 y5 y6 > #0.75) \/
    (y_of_x (law_cosines_234_x costheta) y1 y2 y3 y4 y5 y6  < &0) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &14) \/
(&4 * x1_delta_y y1 y2 y3 y4 y5 y6 <  tan2lower * delta4_squared_y y1 y2 y3 y4 y5 y6)  \/
    (delta4_y y1 y2 y3 y4 y5 y6 > &0) \/
  (y_of_x (law_cosines_126_x cos1981) y1 y2 y3 y4 y5 y6 > &0) 
    )`;
(* arc[2,2,3.915]==2.72855... 
  (dih_y y1 y2 y3 y4 y5 y6 > pi - #0.37) \/   (arclength y2 y3 y4 < #2.7285) , removed *)
};; 



Parse_ineq.execute_cfsqp  
{
idv = "test 1607135856 C extra";
doc = "
";
tags= [Tex;Cfsqp;Xconvert;Penalty(10.0,10000.0);Flypaper];
ineq = all_forall `ineq
 [
   (&2,y1,&2 * h0);
   (&2,y2,&2 * h0);
   (&2,y3,&2 * h0);
   (&2 * h0,y4,&4 * h0);
   (&2,y5,&2);
   (&2,y6,&2)
 ] (
  (dih_y y1 y2 y3 y4 y5 y6 - dih2_y y1 y2 y3 y4 y5 y6 > #1.52) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &36) \/
  (delta4_y y1 y2 y3 y4 y5 y6 > &0) \/
  (dih_y y1 y2 y3 y4 y5 y6 > #2.614) \/
  (dih_y y1 y2 y3 y4 y5 y6 < #2.274)
    )`;
};; 


Parse_ineq.execute_cfsqp  
{
idv = "test 1607135856 extra";
doc = "
";
tags= [Tex;Cfsqp;Xconvert;Penalty(1000.0,10000.0);Flypaper];
ineq = all_forall `ineq
 [
   (&2,y1,&2 * h0);
   (&2,y2,&2 * h0);
   (&2,y3,&2 * h0);
   (&2 * h0,y4,&4 * h0);
   (&2,y5,&2);
   (&2 * h0,y6,&4 * h0)
 ] (
  (arclength y2 y3 y4 < #2.8) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &21) \/
  (dih_y y1 y2 y3 y4 y5 y6 > pi - #0.37) \/
  (dih_y y1 y2 y3 y4 y5 y6 < #1.52) \/
    (arclength y1 y2 y6 > #1.981) 
    )`;
(* Solve[arc[2, 2, y] == 2.793, y]   ==> y <= 3.9395 *)
};; 




1;;
(* SECTION 2986512815 *)


let tt = 
{
idv = "test ineq";
doc = "This is a trivial inequality";
tags=[Cfsqp];
ineq = all_forall `ineq
[
  (&1,x1,&1)
]
(&0 < &1)`;
};;

testsplit_idq true tt;;

Parse_ineq.execute_cfsqp  
{
idv = "test 2986512815";
doc = "The terms have been generated by Mathematica.
";
tags= [Tex;Cfsqp;Eps 1.0e-8;Penalty(1000.0,100000.0);Flypaper];
ineq = all_forall `ineq
 [
    (&1,e1,&1 + sol0/pi);
    (&1,e2,&1 + sol0/pi);
    (&1,e3,&1 + sol0/pi);
    (&1,e4,&1 + sol0/pi);
    ((&2 / h0) pow 2, a2, (&2 * h0) pow 2);
    ((&2 / h0) pow 2, b2, (&2 * h0) pow 2);
    ((&2 / h0) pow 2, c2, (&2 * h0) pow 2);
    (&2 pow 2, d2, #3.915 pow 2);
    (&2 pow 2, y2, #3.915 pow 2)
 ]
 (num1 e1 e2 e3 y2 b2 a2 * num1 e4 e2 e3 y2 c2 d2 > &0 \/
delta_x (&4) (&4) (&4) a2 b2 y2 > &10 \/
delta_x (&4) (&4) (&4) c2 d2 y2 > &10 \/
 delta_x (&4) (&4) (&4) a2 b2 y2 < &0 \/
 delta_x (&4) (&4) (&4) c2 d2 y2 < &0 \/
num2 e4 e2 e3 y2 c2 d2 < &0 \/
eulerA_x (&4) (&4) (&4) c2 d2 y2 < &0 
\/
 (dih_x (&4) (&4) (&4) a2 b2 y2 + dih_x (&4) (&4) (&4) d2 c2 y2 > pi) 
    )`;
};; 



 (* break into 2 cases: d2 <= 3.915, and d2 >= 3.915 *)

(* \/ \/ num2 e1 e2 e3 y2 b2 a2 < &0 

 *)

Parse_ineq.execute_cfsqp  {
idv = "test 2986512815 y";
doc = "The terms have been generated by Mathematica.
";
tags= [Tex;Cfsqp;Eps 1.0e-8;Penalty(1000.0,10000.0);Flypaper;Xconvert];
ineq = all_forall `ineq
 [
    (&1,e1,&1 + sol0/pi);
    (&1,e2,&1 + sol0/pi);
    (&1,e3,&1 + sol0/pi);
    (&1,e4,&1 + sol0/pi);
    (&2 / h0, a, &2 * h0);
    (&2 / h0, b, &2 * h0);
    (&2 / h0, c, &2 * h0);
    (&2, d, #4.0);
    (&2, y, #3.915)
 ]
 (delta_y (&2) (&2) (&2) a b y > &10 \/
 delta_y (&2) (&2) (&2) c d y > &10 \/
 delta_y (&2) (&2) (&2) a b y < &0 \/
 delta_y (&2) (&2) (&2) c d y < &0 \/
 num1 e1 e2 e3 y b a * num1 e4 e2 e3 y c d > &0 \/
  num2 e1 e2 e3 y b a < &0 \/
  (dih_y (&2) (&2) (&2) a b y + dih_y (&2) (&2) (&2) d c y > pi) )`;
};;

  {
idv = "2986512815 XXX";
doc = "";
tags= [Tex;Cfsqp;Eps 1.0e-8;Flypaper;Xconvert;Penalty(1000.0,2000.0)];

ineq = all_forall `ineq
 [
    (&1,e1,&1 + sol0/pi);
    (&1,e2,&1 + sol0/pi);
    (&1,e3,&1 + sol0/pi);
    (&1,e4,&1 + sol0/pi);
   (&0,t1,&1);
   (&0,t2,&1);
    (&2 / h0, a, &2 * h0);
    (&2 / h0, b, &2 * h0);
    (&2 / h0, c, &2 * h0);
    (&2, d, #4.0);
    (&2, y, #3.915)
 ]
((t1 * num1 e1 e2 e3 y b a  / ( y * (&16 - y pow 2)) +
 t2 * num1 e4 e2 e3 y c d  / ( y * (&16 - y pow 2)) > &10)  \/ 
(t1 * num1 e1 e2 e3 y b a  / ( y * (&16 - y pow 2)) +
 t2 * num1 e4 e2 e3 y c d  / ( y * (&16 - y pow 2)) < --  &10)  \/ 
  (t1 pow 3 * num2 e1 e2 e3 y b a  / ( (y * (&16 - y pow 2)) pow 2) +
 t2  pow 3 * num2 e4 e2 e3 y c d  / ( (y * (&16 - y pow 2)) pow 2) < &0) \/
  (delta_y (&2) (&2) (&2) a b y > &1) \/ 
  (delta_y (&2) (&2) (&2) a b y < &0) \/ 
  (delta_y (&2) (&2) (&2) c d y > &1) \/ 
  (delta_y (&2) (&2) (&2) c d y < &0) \/
    (dih_y (&2) (&2) (&2) a b y + dih_y (&2) (&2) (&2) d c y > pi) )`;
};;


Parse_ineq.execute_cfsqp
  {
idv = "2986512815 t0";
doc = "";
tags= [Tex;Cfsqp;Eps 1.0e-8;Flypaper;Xconvert;Penalty(1000.0,2000.0)];

ineq = all_forall `ineq
 [
    (&1,e1,&1 + sol0/pi);
    (&1,e2,&1 + sol0/pi);
    (&1,e3,&1 + sol0/pi);
    (&1,e4,&1 + sol0/pi);
    (&2 / h0, a, &2 * h0);
    (&2 / h0, b, &2 * h0);
    (&2 / h0, c, &2 * h0);
    (&2, d, #4.0);
    (&2, y, #3.915)
 ]
((num1 e1 e2 e3 y b a  / (sqrt(delta_y (&2) (&2) (&2) a b y)  * y * (&16 - y pow 2)) +
 num1 e4 e2 e3 y c d  / (sqrt(delta_y (&2) (&2) (&2) c d y)  * y * (&16 - y pow 2)) > &10)  \/ 
(num1 e1 e2 e3 y b a  / (sqrt(delta_y (&2) (&2) (&2) a b y)  * y * (&16 - y pow 2)) +
 num1 e4 e2 e3 y c d  / (sqrt(delta_y (&2) (&2) (&2) c d y)  * y * (&16 - y pow 2)) < --  &10)  \/ 
  (num2 e1 e2 e3 y b a  / (sqrt(delta_y (&2) (&2) (&2) a b y) pow 3  * (y * (&16 - y pow 2)) pow 2) +
 num2 e4 e2 e3 y c d  / (sqrt(delta_y (&2) (&2) (&2) c d y) pow 3  * (y * (&16 - y pow 2)) pow 2) < &0) \/
  (delta_y (&2) (&2) (&2) a b y < &1) \/ 
  (delta_y (&2) (&2) (&2) c d y < &1) \/ 
  (dih_y (&2) (&2) (&2) a b y + dih_y (&2) (&2) (&2) d c y > pi) )`;
};;

Parse_ineq.execute_cfsqp
  {
idv = "2986512815 t1";
doc = "";
tags= [Tex;Cfsqp;Eps 1.0e-8;Flypaper;Xconvert;Penalty(1000.0,2000.0)];

ineq = all_forall `ineq
 [
    (&1,e1,&1 + sol0/pi);
    (&1,e2,&1 + sol0/pi);
    (&1,e3,&1 + sol0/pi);
    (&1,e4,&1 + sol0/pi);
    (&0,t,&1);
    (&2 / h0, a, &2 * h0);
    (&2 / h0, b, &2 * h0);
    (&2 / h0, c, &2 * h0);
    (&2, d, #4.0);
    (&2, y, #3.915)
 ]
( (num1 e1 e2 e3 y b a  / (  y * (&16 - y pow 2)) +
 t * num1 e4 e2 e3 y c d  / (sqrt(delta_y (&2) (&2) (&2) c d y)  * y * (&16 - y pow 2)) > &10)  \/ 
(num1 e1 e2 e3 y b a  / (y * (&16 - y pow 2)) +
 t* num1 e4 e2 e3 y c d  / (sqrt(delta_y (&2) (&2) (&2) c d y)  * y * (&16 - y pow 2)) < --  &10)  \/ 
  (num2 e1 e2 e3 y b a  / (  (y * (&16 - y pow 2)) pow 2) +
 t pow 3 * num2 e4 e2 e3 y c d  / (sqrt(delta_y (&2) (&2) (&2) c d y) pow 3  * (y * (&16 - y pow 2)) pow 2) < &0) \/
  (delta_y (&2) (&2) (&2) a b y < &0) \/ 
  (delta_y (&2) (&2) (&2) a b y > &1) \/ 
  (delta_y (&2) (&2) (&2) c d y < &1)) `;
};;


Parse_ineq.execute_cfsqp
  {
idv = "2986512815 t2";
doc = "";
tags= [Tex;Cfsqp;Eps 1.0e-8;Flypaper;Xconvert;Penalty(1000.0,2000.0)];

ineq = all_forall `ineq
 [
    (&1,e1,&1 + sol0/pi);
    (&1,e2,&1 + sol0/pi);
    (&1,e3,&1 + sol0/pi);
    (&1,e4,&1 + sol0/pi);
   (&0,t,&1);
    (&2 / h0, a, &2 * h0);
    (&2 / h0, b, &2 * h0);
    (&2 / h0, c, &2 * h0);
    (&2, d, #4.0);
    (&2, y, #3.915)
 ]
((t * num1 e1 e2 e3 y b a  / (sqrt(delta_y (&2) (&2) (&2) a b y)  * y * (&16 - y pow 2)) +
 num1 e4 e2 e3 y c d  / ( y * (&16 - y pow 2)) > &10)  \/ 
(t * num1 e1 e2 e3 y b a  / (sqrt(delta_y (&2) (&2) (&2) a b y)  * y * (&16 - y pow 2)) +
 num1 e4 e2 e3 y c d  / ( y * (&16 - y pow 2)) < --  &10)  \/ 
  (t pow 3 * num2 e1 e2 e3 y b a  / (sqrt(delta_y (&2) (&2) (&2) a b y) pow 3  * (y * (&16 - y pow 2)) pow 2) +
 num2 e4 e2 e3 y c d  / ( (y * (&16 - y pow 2)) pow 2) < &0) \/
  (delta_y (&2) (&2) (&2) a b y < &1) \/ 
  (delta_y (&2) (&2) (&2) c d y > &1) \/ 
  (delta_y (&2) (&2) (&2) c d y < &0) )`;
};;


Parse_ineq.execute_cfsqp  {
idv = "2986512815 test";
doc = "The terms have been generated by Mathematica.
Deprecated. Replaced with u1 below.  (The second derivative is always negative for each
simplex so the sum is negative.)
";
tags= [Tex;Cfsqp;Eps 1.0e-8;Flypaper;Xconvert;Deprecated];
ineq = all_forall `ineq
 [
    (&1,e1,&1 + sol0/pi);
    (&1,e2,&1 + sol0/pi);
    (&1,e3,&1 + sol0/pi);
    (&1,e4,&1 + sol0/pi);
    (&2 / h0, a, &2 * h0);
    (&2 / h0, b, &2 * h0);
    (&2 / h0, c, &2 * h0);
    (&2, d, #4.0);
    (&2, y, #3.915)
 ]
 ((let term1 = ((&4 * ((sqrt ((((-- &4) * (c pow 4)) + (((-- &4) * (((d pow 2) + ((-- &1) * 
(y pow 2))) pow 2)) + ((c pow 2) * ((&8 * (y pow 2)) + ((-- &1) * ((d pow 2) 
* ((-- &8) + (y pow 2)))))))))) * (((-- &1) * ((y pow 2) * ((&8 * e1) + ((&8 
* e3) + (e2 * ((-- &16) + (y pow 2))))))) + (((b pow 2) * ((&8 * e3) + (e1 * 
((-- &8) + (y pow 2))))) + ((a pow 2) * ((&8 * e1) + (e3 * ((-- &8) + (y 
pow 2))))))))) + (&4 * ((sqrt ((((-- &4) * (a pow 4)) + (((-- &4) * (((b pow 
2) + ((-- &1) * (y pow 2))) pow 2)) + ((a pow 2) * ((&8 * (y pow 2)) + ((-- 
&1) * ((b pow 2) * ((-- &8) + (y pow 2)))))))))) * (((-- &1) * ((y pow 2) * 
((&8 * e1) + ((&8 * e3) + (e4 * ((-- &16) + (y pow 2))))))) + (((c pow 2) * 
((&8 * e3) + (e1 * ((-- &8) + (y pow 2))))) + ((d pow 2) * ((&8 * e1) + (e3 * 
((-- &8) + (y pow 2)))))))))) in
  let term2 = ((&4 * (((sqrt ((((-- &4) * (c pow 4)) + (((-- &4) * (((d pow 2) + ((-- &1) * 
(y pow 2))) pow 2)) + ((c pow 2) * ((&8 * (y pow 2)) + ((-- &1) * ((d pow 2) 
* ((-- &8) + (y pow 2)))))))))) pow 3) * (((-- &8) * ((a pow 6) * ((&8 * (e1 
* ((-- &16) + (&3 * (y pow 2))))) + (e3 * (&128 + (((-- &8) * (y pow 2)) + (y 
pow 4))))))) + (((-- &8) * (((b pow 2) + ((-- &1) * (y pow 2))) * (((y pow 4) 
* ((e2 * (((-- &16) + (y pow 2)) pow 2)) + ((&8 * (e1 * ((-- &16) + (&3 * (y 
pow 2))))) + (&8 * (e3 * ((-- &16) + (&3 * (y pow 2)))))))) + (((b pow 2) * 
((y pow 2) * ((&16 * (e3 * (&16 + ((-- &3) * (y pow 2))))) + ((e2 * (((-- 
&16) + (y pow 2)) pow 2)) + (e1 * ((-- &512) + ((&48 * (y pow 2)) + ((-- &3) 
* (y pow 4))))))))) + ((b pow 4) * ((&8 * (e3 * ((-- &16) + (&3 * (y pow 
2))))) + (e1 * (&128 + (((-- &8) * (y pow 2)) + (y pow 4)))))))))) + (((-- 
&4) * ((a pow 2) * ((&6 * ((y pow 4) * ((&8 * (e1 * ((-- &16) + (&3 * (y pow 
2))))) + (e3 * (&128 + (((-- &8) * (y pow 2)) + (y pow 4))))))) + (((-- &4) * 
((b pow 2) * ((y pow 2) * ((e2 * (((-- &16) + (y pow 2)) pow 2)) + ((&4 * (e1 
* ((-- &32) + (((-- &2) * (y pow 2)) + (y pow 4))))) + (&4 * (e3 * ((-- &32) 
+ (((-- &2) * (y pow 2)) + (y pow 4)))))))))) + ((b pow 4) * ((&6 * (e3 * 
(&128 + (((-- &40) * (y pow 2)) + (&3 * (y pow 4)))))) + (e1 * ((-- &768) + 
((&208 * (y pow 2)) + (((-- &20) * (y pow 4)) + (y pow 6))))))))))) + ((-- 
&4) * ((a pow 4) * ((&2 * ((y pow 2) * ((e1 * (&384 + ((-- &72) * (y 
pow 2)))) + ((e2 * (((-- &16) + (y pow 2)) pow 2)) + ((-- &4) * (e3 * (&160 + 
(((-- &14) * (y pow 2)) + (y pow 4))))))))) + ((b pow 2) * ((&6 * (e1 * (&128 
+ (((-- &40) * (y pow 2)) + (&3 * (y pow 4)))))) + (e3 * ((-- &768) + ((&208 
* (y pow 2)) + (((-- &20) * (y pow 4)) + (y pow 6))))))))))))))) + (&4 * 
(((sqrt ((((-- &4) * (a pow 4)) + (((-- &4) * (((b pow 2) + ((-- &1) * (y pow 
2))) pow 2)) + ((a pow 2) * ((&8 * (y pow 2)) + ((-- &1) * ((b pow 2) * ((-- 
&8) + (y pow 2)))))))))) pow 3) * (((-- &8) * ((c pow 6) * ((&8 * (e3 * ((-- 
&16) + (&3 * (y pow 2))))) + (e1 * (&128 + (((-- &8) * (y pow 2)) + (y pow 
4))))))) + (((-- &8) * (((d pow 2) + ((-- &1) * (y pow 2))) * (((y pow 4) * 
((e4 * (((-- &16) + (y pow 2)) pow 2)) + ((&8 * (e1 * ((-- &16) + (&3 * (y 
pow 2))))) + (&8 * (e3 * ((-- &16) + (&3 * (y pow 2)))))))) + (((d pow 2) * 
((y pow 2) * ((e1 * (&256 + ((-- &48) * (y pow 2)))) + ((e4 * (((-- &16) + (y 
pow 2)) pow 2)) + (e3 * ((-- &512) + ((&48 * (y pow 2)) + ((-- &3) * (y pow 
4))))))))) + ((d pow 4) * ((&8 * (e1 * ((-- &16) + (&3 * (y pow 2))))) + (e3 
* (&128 + (((-- &8) * (y pow 2)) + (y pow 4)))))))))) + (((-- &4) * ((c pow 
4) * ((&2 * ((y pow 2) * ((e3 * (&384 + ((-- &72) * (y pow 2)))) + ((e4 * 
(((-- &16) + (y pow 2)) pow 2)) + ((-- &4) * (e1 * (&160 + (((-- &14) * (y 
pow 2)) + (y pow 4))))))))) + ((d pow 2) * ((&6 * (e3 * (&128 + (((-- &40) * 
(y pow 2)) + (&3 * (y pow 4)))))) + (e1 * ((-- &768) + ((&208 * (y pow 2)) + 
(((-- &20) * (y pow 4)) + (y pow 6)))))))))) + ((-- &4) * ((c pow 2) * ((&6 * 
((y pow 4) * ((&8 * (e3 * ((-- &16) + (&3 * (y pow 2))))) + (e1 * (&128 + 
(((-- &8) * (y pow 2)) + (y pow 4))))))) + (((-- &4) * ((d pow 2) * ((y pow 
2) * ((e4 * (((-- &16) + (y pow 2)) pow 2)) + ((&4 * (e1 * ((-- &32) + (((-- 
&2) * (y pow 2)) + (y pow 4))))) + (&4 * (e3 * ((-- &32) + (((-- &2) * (y pow 
2)) + (y pow 4)))))))))) + ((d pow 4) * ((&6 * (e1 * (&128 + (((-- &40) * (y 
pow 2)) + (&3 * (y pow 4)))))) + (e3 * ((-- &768) + ((&208 * (y pow 
2)) + (((-- &20) * (y pow 4)) + (y pow 6))))))))))))))))) in
   term1 * term1 - #0.01 * term2 > &0) \/ 
  (delta_y (&2) (&2) (&2) a b y < &0) \/ 
  (delta_y (&2) (&2) (&2) c d y < &0) \/ 
  (dih_y (&2) (&2) (&2) a b y + dih_y (&2) (&2) (&2) d c y > pi) )`;
};;


(* END SECTION 2986512815 *)

(* SECTION 2065952723 *)

Parse_ineq.execute_cfsqp  
  {
idv = "test 2065952723 A";
doc = "See explanation in 2065952723.  This is the branch when $a_2 \\le 15.99$.
";
tags = [Flypaper;Tex];
ineq = all_forall `ineq
  [
  (&1 , e1, &1 + sol0/ pi);
  (&1 , e2, &1 + sol0/ pi);
  (&1 , e3, &1 + sol0/ pi);
  ((&2 / h0) pow 2, a2, #15.53);
  ((&2 / h0) pow 2, b2, &4 pow 2);
  ((&2 / h0) pow 2, c2, &4 pow 2)
  ]
   (num_combo1 e1 e2 e3 a2 b2 c2 > &0) `;
};;

Parse_ineq.execute_cfsqp  
  {
idv = "2065952723 C-2";
doc = "See explanation in 2065952723.  Used to replace extremal edges with minimal edges in a
    hexagon.";
(* 15.53 > 3.94^2, arc[2,2,3.94] > 2 arc[2,2,2 hmid], to get the upper bound.
    Lower via, arc[2,2,2.9] < arc[2hmid,2hmid,2] 2.  *)
tags = [Flypaper;Tex];
ineq = all_forall `ineq
  [
  (&1 , e1, &1 + sol0/ pi);
  (&1 , e2, &1 + sol0/ pi);
  (&1 , e3, &1 + sol0/ pi);
  ((&2 / h0) pow 2, a2, (&2 * h0) pow 2);
  ((&2 / h0) pow 2, b2, &4);
  (#2.98 pow 2, c2, #15.53)
  ]
   ((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
};;


Parse_ineq.execute_cfsqp
  {
idv = "old test 2065952723 B";
doc = "";
tags = [Flypaper;Tex;Eps 1.0e-8];
ineq = all_forall `ineq
  [
  (&4,x1,&4);
  (&4,x2,&4);
  (&4,x3,&4);
  (#15.99,x4,#16);
  ((&2 / h0) pow 2, x5, &4 pow 2);
  ((&2 / h0) pow 2, x6, &4 pow 2)
  ]
   ( (x5 + x6 > #15.5) \/ (delta_x x1 x2 x3 x4 x5 x6 < &0))`;
};;

Parse_ineq.execute_cfsqp  {
idv = "old test 2065952723 C";
doc = "";
tags = [Flypaper;Tex;Penalty (500.0,50000.0)];
ineq = all_forall `ineq
  [
  (&1 , e1, &1 + sol0/ pi);
  (&1 , e2, &1 + sol0/ pi);
  (&1 , e3, &1 + sol0/ pi);
  (#15.99,a2,#16);
  ((&2 / h0) pow 2, b2, &4 pow 2);
  ((&2 / h0) pow 2, c2, &4 pow 2)
  ]
((((&2 / &25) * (((-- &32) * ((a2 pow 3) * e1)) + ((&2 * ((a2 pow 4) * e1)) +  
((&32 * (a2 * ((b2 pow 2) * e1))) + (((-- &2) * ((a2 pow 2) * ((b2 pow 2) *  
e1))) + (((-- &64) * (a2 * (b2 * (c2 * e1)))) + ((&4 * ((a2 pow 2) * (b2 *  
(c2 * e1)))) + ((&32 * (a2 * ((c2 pow 2) * e1))) + (((-- &2) * ((a2 pow 2) *  
((c2 pow 2) * e1))) + ((&3200 * ((a2 pow 2) * (e1 pow 2))) + (((-- &200) *  
((a2 pow 3) * (e1 pow 2))) + ((&131072 * e2) + ((&8192 * (a2 * e2)) + ((&512  
* ((a2 pow 2) * e2)) + ((&48 * ((a2 pow 3) * e2)) + (((-- &24576) * (b2 *  
e2)) + (((-- &1536) * (a2 * (b2 * e2))) + (((-- &48) * ((a2 pow 2) * (b2 *  
e2))) + (((-- &6) * ((a2 pow 3) * (b2 * e2))) + ((&1536 * ((b2 pow 2) * e2))  
+ ((&16 * (a2 * ((b2 pow 2) * e2))) + ((&8 * ((a2 pow 2) * ((b2 pow 2) *  
e2))) + (((-- &16) * ((b2 pow 3) * e2)) + (((-- &2) * (a2 * ((b2 pow 3) *  
e2))) + (((-- &24576) * (c2 * e2)) + (((-- &1536) * (a2 * (c2 * e2))) + (((--  
&144) * ((a2 pow 2) * (c2 * e2))) + ((&3072 * (b2 * (c2 * e2))) + ((&224 *  
(a2 * (b2 * (c2 * e2)))) + ((&16 * ((a2 pow 2) * (b2 * (c2 * e2)))) + (((--  
&144) * ((b2 pow 2) * (c2 * e2))) + ((&4 * (a2 * ((b2 pow 2) * (c2 * e2)))) +  
(((-- &1) * ((a2 pow 2) * ((b2 pow 2) * (c2 * e2)))) + ((&1536 * ((c2 pow 2)  
* e2)) + ((&144 * (a2 * ((c2 pow 2) * e2))) + (((-- &48) * (b2 * ((c2 pow 2)  
* e2))) + (((-- &18) * (a2 * (b2 * ((c2 pow 2) * e2)))) + (((-- &48) * ((c2  
pow 3) * e2)) + (((-- &3200) * ((a2 pow 2) * (e1 * e2))) + (((-- &3200) * (a2  
* (b2 * (e1 * e2)))) + ((&400 * ((a2 pow 2) * (b2 * (e1 * e2)))) + ((&3200 *  
(a2 * (c2 * (e1 * e2)))) + (((-- &204800) * (e2 pow 2)) + (((-- &12800) * (a2  
* (e2 pow 2))) + ((&25600 * (b2 * (e2 pow 2))) + ((&3200 * (a2 * (b2 * (e2  
pow 2)))) + (((-- &200) * (a2 * ((b2 pow 2) * (e2 pow 2)))) + ((&25600 * (c2  
* (e2 pow 2))) + (((-- &3200) * (b2 * (c2 * (e2 pow 2)))) + ((&131072 * e3) +  
((&8192 * (a2 * e3)) + ((&512 * ((a2 pow 2) * e3)) + ((&48 * ((a2 pow 3) *  
e3)) + (((-- &24576) * (b2 * e3)) + (((-- &1536) * (a2 * (b2 * e3))) + (((--  
&144) * ((a2 pow 2) * (b2 * e3))) + ((&1536 * ((b2 pow 2) * e3)) + ((&144 *  
(a2 * ((b2 pow 2) * e3))) + (((-- &48) * ((b2 pow 3) * e3)) + (((-- &24576) *  
(c2 * e3)) + (((-- &1536) * (a2 * (c2 * e3))) + (((-- &48) * ((a2 pow 2) *  
(c2 * e3))) + (((-- &6) * ((a2 pow 3) * (c2 * e3))) + ((&3072 * (b2 * (c2 *  
e3))) + ((&224 * (a2 * (b2 * (c2 * e3)))) + ((&16 * ((a2 pow 2) * (b2 * (c2 *  
e3)))) + (((-- &48) * ((b2 pow 2) * (c2 * e3))) + (((-- &18) * (a2 * ((b2 pow  
2) * (c2 * e3)))) + ((&1536 * ((c2 pow 2) * e3)) + ((&16 * (a2 * ((c2 pow 2)  
* e3))) + ((&8 * ((a2 pow 2) * ((c2 pow 2) * e3))) + (((-- &144) * (b2 * ((c2  
pow 2) * e3))) + ((&4 * (a2 * (b2 * ((c2 pow 2) * e3)))) + (((-- &1) * ((a2  
pow 2) * (b2 * ((c2 pow 2) * e3)))) + (((-- &16) * ((c2 pow 3) * e3)) + (((--  
&2) * (a2 * ((c2 pow 3) * e3))) + (((-- &3200) * ((a2 pow 2) * (e1 *  
e3))) + ((&3200 * (a2 * (b2 * (e1 * e3)))) + (((-- &3200) * (a2 * (c2 * (e1 *  
e3)))) + ((&400 * ((a2 pow 2) * (c2 * (e1 * e3)))) + (((-- &409600) * (e2 *  
e3)) + (((-- &25600) * (a2 * (e2 * e3))) + ((&51200 * (b2 * (e2 * e3))) +  
((&3200 * (a2 * (b2 * (e2 * e3)))) + (((-- &3200) * ((b2 pow 2) * (e2 * e3)))  
+ ((&51200 * (c2 * (e2 * e3))) + ((&3200 * (a2 * (c2 * (e2 * e3)))) + (((--  
&400) * (a2 * (b2 * (c2 * (e2 * e3))))) + (((-- &3200) * ((c2 pow 2) * (e2 *  
e3))) + (((-- &204800) * (e3 pow 2)) + (((-- &12800) * (a2 * (e3 pow 2))) +  
((&25600 * (b2 * (e3 pow 2))) + ((&25600 * (c2 * (e3 pow 2))) + ((&3200 * (a2  
* (c2 * (e3 pow 2)))) + (((-- &3200) * (b2 * (c2 * (e3 pow 2)))) + ((-- &200) *  
(a2 * ((c2 pow 2) * (e3 pow  
2))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
)))))))))))))))))))))) > &0) \/ (b2 + c2 < #16.0) \/ (b2 + c2 > #16.5))
`;
};;

Parse_ineq.execute_cfsqp  {
idv = "test 2065952723";
doc = "
%See Mathematica numerical calculation.
% old idv: eqn:gg'' calc:Lexell.
The derivatives have been computed in Mathematica and converted to
HOL format.  
This is a
  calculation of the sign of a second derivative to show that the
  function $\\tau$ does not have a interior local minimum as a function of the
  edge lengths.  It initially appears to depend on six variables, but
  the dependence on three of the variables is linear and is
  extremal at the endpoints.

Let
\\[ 
g(s;a,b,c,e_1,e_2,e_3) = \\sum_{i=1}^3 \\dih_i(2,2,2,a+s,b,c) e_i,
\\] 
where $\\dih_i$ is given by Definition~\\ref{def:tau}.
Let $\\Delta = \\Delta(4,4,4,a^2,b^2,c^2)$.
Let primes denote derivatives with respect to the variable $s$.
Assume that
$e_i\\in\\leftclosed1,1+\\sol_0/\\pi\\rightclosed$,  that
$a,b,c\\in\\leftclosed2/\\hm,4\\rightclosed$.
%We restrict $a$ further to $a\\le 3.8$.
Then
\\begin{equation}\\label{eqn:calc:Lexell}
(16-a^2) ^2 a^2(  \\Delta (g'(0;a,b,c,e_1,e_2,e_3))^2 
- 0.01\\Delta^{3/2}g''(0;a,b,c,e_1,e_2,e_3))\\ge 0.
\\end{equation}
(The factors of $\\Delta$ clear the denominator in
(\\ref{eqn:calc:Lexell}) to simplify the inequality to be proved.)
%Sum of squares methods may be the easiest way to prove this inequality near the
%minimum.
%The quantities deriv1 and deriv2 are for reference only.
Variables $e_i$ are linear and variables $a,b,c$ appear in even powers.
";
(*

*)
tags = [Flypaper;Tex;Eps 1.0e-8];
ineq = all_forall `ineq
  [
  (&1 , e1, &1 + sol0/ pi);
  (&1 , e2, &1 + sol0/ pi);
  (&1 , e3, &1 + sol0/ pi);
  ((&2 / h0) pow 2, a2, &4 pow 2);
  ((&2 / h0) pow 2, b2, &4 pow 2);
  ((&2 / h0) pow 2, c2, &4 pow 2)
  ]
   (((num1 e1 e2 e3 a2 b2 c2 ) pow 2 - #0.01 * num2 e1 e2 e3 a2 b2 c2 > &0) \/ (a2 > #15.9))`;
};;

Parse_ineq.execute_cfsqp  
  {
idv = "2065952723 C-1";
doc = "See explanation in 2065952723.  At this point we have a hexagon.
  This is the case when neither $v_4$ nor $v_5$ is flat. 
  ";
(* arc[2,2,3.94] > 2 arc[2,2,2 hmid], to get the upper bound *)
(* bug fixed on domain, 12/30/2010 *)
tags = [Flypaper;Tex;Eps 1.0e-8];
ineq = all_forall `ineq
  [
  (&1 , e1, &1 + sol0/ pi);
  (&1 , e2, &1 + sol0/ pi);
  (&1 , e3, &1 + sol0/ pi);
  ((&2 / h0) pow 2, a2, (&2 * h0) pow 2);
  ( (&2 / h0) pow 2, b2, (&2 * h0) pow 2);
  (#3.4 pow 2, c2, #3.94 pow 2)
  ]
   (num1 e1 e2 e3 a2 b2 c2 > &0) `;
};;

Parse_ineq.execute_cfsqp  
  {
idv = "2065952723 A";
doc = "See explanation in 2065952723.  This is the branch when $a_2 \\le 15.99$.
";
tags = [Flypaper;Tex];
ineq = all_forall `ineq
  [
  (&1 , e1, &1 + sol0/ pi);
  (&1 , e2, &1 + sol0/ pi);
  (&1 , e3, &1 + sol0/ pi);
  ((&2 / h0) pow 2, a2, #15.99);
  ((&2 / h0) pow 2, b2, &4 pow 2);
  ((&2 / h0) pow 2, c2, &4 pow 2)
  ]
   (num_combo1 e1 e2 e3 a2 b2 c2 > &0) `;
};;




Parse_ineq.execute_cfsqp  {
idv = "test  not used";
doc = "";
tags = [Flypaper;Tex;Eps 1.0e-8];
ineq = all_forall `ineq
  [
  (&4,x1,&4);
  (&4,x2,&4);
  (&4,x3,&4);
  (#15.99,x4,#16);
  ((&2 / h0) pow 2, x5, &4 pow 2);
  ((&2 / h0) pow 2, x6, &4 pow 2)
  ]
   ((delta_x x1 x2 x3 x4 x5 x6 < &0) \/ (x5 + x6 < #16.5))`;
};;

(* END SECTION 2065952723 *)

let make_WHW i j = 
  let r = match  i with
   0 -> [`&2`;`&2`;`&2`]
    |1 -> [`&2 * h0`;`&2`;`&2`]
    |2 -> [`&2`;`&2 * h0`;`&2`]
    |3 -> [`&2`;`&2`;`&2 * h0`]
    | _ ->  failwith "make_WHW" in
  let s = match j with
    0 -> [`&2`;`&2 * h0`]
    | 1 -> [`&2 * h0`;`&2`]
    | _ -> failwith "make_WHW j" in
  let t1 = r @ s in
  let t = map (fun x -> let v = mk_comb (`(pow)`,x) in mk_comb(v,`2`) ) t1 in
{
idv = Printf.sprintf "PQFYWHW B'' %d %d" i j;
doc = "Pentagons with two flats 
 (that are not adjacent) satisfy the bound $D[4,1]$.  When $y_{15}=y_{45}=2$ and
  $y_{34} = 2h_0$, then the lines $\\{\\v_2,\\v_3\\}$ and $\\{\\v_4,\\v_5\\}$
are parallel and the dihedral inequality is sharp.
  % The sharp case is i=3, j=0.
The constants $d(5,0)<d(4,1)$.  We prove the stronger inequality with $d(4,1)$.  The case when $\\Delta<16$ is done as a separate calculation.
    ";
(* updated Dec 12, 2010 *)
tags = (if(i+j=0) then [Tex] else []) @ [Flypaper;Eps 1.0e-8;Penalty(1.0,2000.0)];
ineq = Ineq.mk_tplate templateB' t;
};;

map (fun (i,j) -> Ineq.add  (make_WHW i j)) [(0,0);(1,0);(2,0);(3,0);(0,1);(1,1);(2,1);(3,1)];;


testsplit_idq true 
(* Parse_ineq.execute_cfsqp *)
  {
idv = "old test";
doc = "";
tags = [];
ineq = all_forall `ineq
  [
(#0.99999999999999988898,x1, #0.99999999999999988898);
(#1.0438699140229557027,x2, #1.0438699140229557027);
(#1.1316097420688666642,x3, #1.1316097420688666642);
(#15.937380962222855274,x4, #15.99000000000000199);
(#6.705845301083399157,x5, #6.7321743512219729411);
(#9.207105064247926407,x6, #9.2334341143865010793)
  ]
  (let alpha = &0 in 
   (num2 x1 x2 x3 x4 x5 x6 * (#1.0 - alpha) * (-- &1) + num1 x1 x2 x3 x4 x5 x6 * alpha  > &0))`;
};;


Parse_ineq.execute_cfsqp 
  {
idv = "old test";
doc = "";
tags = [Penalty(50.0,5000.0)];
ineq = all_forall `ineq
  [
(#5.8959281250000064034,x1,#5.8959281250000064034);
(#4.0068859374999998835,x2,#4.0068859374999998835);
(#6.2035000000000062315,x3,#6.2035000000000062315);
(#4.0367249999999996746,x4,#4.0367249999999996746);
(#20.069634375000017457,x5,#20.069634375000017457);
(#1.000000000000000222,x6,#1.000000000000000222)
  ]   ( let x12 = &2 pow 2 in
          let x23 = &2 pow 2 in
          let x14 = (&2 * h0) pow 2 in
          let cos242 = -- #0.75 in
          delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6 < &10 \/
          factor345_hexall_x cos242 x1 x2 x3 x4 x5 x6 > &0 \/
          eulerA_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6 < #1.72)`;
};;




(*   *)



Parse_ineq.execute_cfsqp 
  {ineq =
    `!diag y1 y2 y3 y4 y5 y6.
         ineq
         [&2,y1,&2 * h0; &2,y2,&2 * h0; &2,y3,&2 * h0; &2,y4,&2 * h0; 
         &2,
         y5,
         &2 * h0; &2,y6,&2 * h0; &2 * h0,diag,#3.9985]
         (let y23 = &2 in
          let y56 = &2 in
          let y16 = &2 in
          let y34 = &2 in
          let y13 = edge_flat y2 y1 y3 y23 (&2) in
          let y46 = edge_flat y5 y4 y6 y56 (&2) in
          taum y1 y3 y4 y34 diag y13 +
          flat_term y2 +
          taum y4 y6 y1 y16 diag y46 +
          flat_term y5 >
          tame_table_d 6 0 \/
          dih_y y1 y3 y4 y34 diag y13 + dih_y y1 y6 y4 y46 diag y16 <
          dih_y y1 y2 y6 (&2 * h0) y16 (&2) \/
          dih_y y1 y3 y4 y34 diag y13 + dih_y y1 y6 y4 y46 diag y16 > pi \/
          dih_y y6 y1 y4 diag y46 y16 < dih_y y6 y1 y5 (&2 * h0) y56 y16 \/
          dih_y y3 y1 y4 diag y34 y13 < dih_y y3 y2 y4 (&2 * h0) y34 y23 \/
          delta_y y1 y3 y4 y34 diag y13 < &0 \/
          delta_y y4 y6 y1 y16 diag y13 < &0)`;
   idv = "GYQVFXJ hexA 0";
   doc =
    "This inequality is the main hexagon inequality\n  with two flat nodes $\\v_2$ $\\v_5$, at opposite vertices of the hexagon.\n  This is an effective quadrilateral, with variables $y_1,\\ldots,y_6$ and diagonal\n  $y_{14}$.\n  Some reductions are used beyond those mentioned in the flypaper.\n  \\begin{enumerate}\n  \\item $y_{34}=y_{16}=2$.\n  \\item if the diag $y_{14}$ is greater than $3.7$, \n      then $y_{12}=y_{23}=y_{45}=y_{56}=2$.   \n  \\item $y_{14}\\le 3.9985$.\n  \\item By symmetry, we can assume that $y_{12}\\le y_{56}$.\n  \\end{enumerate}\n  The reductions are justified by the preceding calculations.\n  There are three cases, depending on whether the edges at $\\v_2$ and $\\v_5$\n  are as short or as long as possible.\n  ";
   tags = [Tex; Flypaper; Penalty (5., 50.); Xconvert]};;

Parse_ineq.execute_cfsqp 
  {ineq =
    `!diag y1 y2 y3 y4.
         ineq
         [&2,y1,&2 * h0; &2,y2,&2 * h0; &2,y3,&2 * h0; &2,y4,&2 * h0; 
          &2 * h0,diag,#3.75]
         (let y23 = &2 in
          let y34 = &2 in
          let y13 = edge_flat y2 y1 y3 y23 (&2) in
         (( taum y1 y3 y4 y34 diag y13 +
          flat_term y2  >
          (tame_table_d 6 0) / &2 ) \/ (dih_y y1 y2 y4 (&2 * h0) diag (&2) > dih_y y1 y3 y4 y34 diag y13)))`;
   idv = "GYQVFXJ hexA 0 test1";
   doc =
    " ";
   tags = [Tex; Flypaper; Penalty (5., 50.); Xconvert]};;

(* SECTION PROIQUZ *)

Parse_ineq.execute_cfsqp  
  {
ineq =  all_forall `ineq
  [
(&2 pow 2,x1,(&2 *h0) pow 2);
(&2 pow 2,x2,(&2 * h0) pow 2);
(&2 pow 2,x3,(&2 * h0) pow 2);
(&2 pow 2,x4,(&2 *h0) pow 2);
((&2 * h0) pow 2,x5,(&4 * h0) pow 2);
(&1,x6,&1)
  ]
  (
    let x12 = &2 pow 2 in
    let x23 = x12 in
    let x14 = &2 pow 2 in
       (delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > &60) \/ 
       (dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > #2.425) \/
       (dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  < #2.274))`;
   idv = "old PROIQUZ hexall 5A1a-old";
   doc =    "split a hex along a shortish diagonal.   Flat at node 2.  Case $y_5 + 0.1 \\le y_3+y_4$.";
   tags = [Tex; Flypaper; Penalty (2000., 15000.);Widthcutoff 0.01]
  (* 
     This case treats Delta bounded away from 0.
     By the bounds [2.274,2.425] on dihedral, we have delta4 <0.
   The upper bound is the trivial triangle inequality bound: y5 <= y3  + y4 <= 4 h0.  
    This shows that we can apply 206...A1  arc[2,2,Sqrt[15.53]] < 2.79. *)
};;



Parse_ineq.execute_cfsqp  
  {
ineq =  all_forall `ineq
  [
(&2 pow 2,x1,(&2 *h0) pow 2);
(&2 pow 2,x2,(&2 * h0) pow 2);
(&2 pow 2,x3,(&2 * h0) pow 2);
(&2 pow 2,x4,(&2 *h0) pow 2);
((&2 * h0) pow 2,x5,(&4 * h0) pow 2);
(&1,x6,&1)
  ]
  (
    let x12 = &2 pow 2 in
    let x23 = x12 in
    let x14 = &2 pow 2 in
      (arclength_x_345 x1 x2 x3 x4 x5 x6 < #2.79) \/
	 (sqrt(x5) + #0.1 >  sqrt(x3) + sqrt(x4)) \/ 
       (delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  < &10) \/ 
       (dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > #2.425))`;
   idv = "old PROIQUZ hexall 5A1b";
   doc =    "split a hex along a shortish diagonal.   Flat at node 2.  Case $y_5 + 0.1 \\le y_3+y_4$.";
   tags = [Tex; Flypaper; Penalty (2000., 15000.);Widthcutoff 0.01]
  (* 
     This case treats Delta bounded away from 0.
   The upper bound is the trivial triangle inequality bound: y5 <= y3  + y4 <= 4 h0.  
    This shows that we can apply 206...A1  arc[2,2,Sqrt[15.53]] < 2.79. *)
};;

Parse_ineq.execute_cfsqp  
  {
ineq =  all_forall `ineq
  [
(&2 pow 2,x1,(&2 *h0) pow 2);
(&2 pow 2,x2,(&2 * h0) pow 2);
(&2 pow 2,x3,(&2 * h0) pow 2);
(&2 pow 2,x4,(&2 *h0) pow 2);
((&2 * h0) pow 2,x5,(&4 * h0) pow 2);
(&1,x6,&1)
  ]
  (
    let x12 = &2 pow 2 in
    let x23 = x12 in
    let x14 = &2 pow 2 in
    
	 (sqrt(x5) + #0.1 >  sqrt(x3) + sqrt(x4)) \/ 
       (delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  < &10) \/ 
       (dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > #2.425))`;
   idv = "old old PROIQUZ hexall 5A1b";
   doc =    "split a hex along a shortish diagonal.   Flat at node 2.  Case $y_5 + 0.1 \\le y_3+y_4$.";
   tags = [Tex; Flypaper; Penalty (2000., 15000.);Widthcutoff 0.01]
  (* 
     This case treats Delta bounded away from 0.
   The upper bound is the trivial triangle inequality bound: y5 <= y3  + y4 <= 4 h0.  
    This shows that we can apply 206...A1  arc[2,2,Sqrt[15.53]] < 2.79. *)
};;




  {
ineq =  all_forall `ineq
  [
(&2 pow 2,x1,(&2 *h0) pow 2);
(&2 pow 2,x2,(&2 * h0) pow 2);
(&2 pow 2,x3,(&2 * h0) pow 2);
(&2 pow 2,x4,(&2 *h0) pow 2);
((&2 * h0) pow 2,x5,(&4 * h0) pow 2);
(&1,x6,&1)
  ]
  (
    let x12 = &2 pow 2 in
    let x23 = x12 in
    let x14 = &2 pow 2 in
      (arclength_x_345 x1 x2 x3 x4 x5 x6 < #2.79) \/
	 (sqrt(x5) + #0.1 >  sqrt(x3) + sqrt(x4)) \/ 
       (delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  < &10) \/ 
       (dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > #2.425))`;
   idv = "old PROIQUZ hexall 5A1a";
   doc =    "split a hex along a shortish diagonal.   Flat at node 2.  Case $y_5 + 0.1 \\le y_3+y_4$.";
   tags = [Tex; Flypaper; Penalty (2000., 15000.);Widthcutoff 0.01]
  (* 
     This case treats Delta bounded away from 0.
   The upper bound is the trivial triangle inequality bound: y5 <= y3  + y4 <= 4 h0.   *)
};;


let PROQUZ_hexall_5A1_ineq = `\b_loc b2425 b24. 
`ineq
  [
(&2 pow 2,x1,(&2 *h0) pow 2);
(&2 pow 2,x2,(&2 * h0) pow 2);
(&2 pow 2,x3,(&2 * h0) pow 2);
(&2 pow 2,x4,(&2 *h0) pow 2);
((&2 * h0) pow 2,x5,(&4 * h0) pow 2);
(&1,x6,&1)
  ]
  (
    let x12 = &2 pow 2 in
    let x23 = x12 in
    let x14 = &2 pow 2 in
	 (sqrt(x5) + #0.1 >  sqrt(x3) + sqrt(x4)) \/ 
	 (sqrt(x5) + #0.1 <  sqrt(x3) + sqrt(x4) /\ b_loc) \/ 
       (delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  < &10) \/ 
       (taum_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6 > tame_table_d 6 0 / &2) \/
       (dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > #2.425) \/ 
       (dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  < #2.425 /\ b2425) \/ 
      (dih_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6 > &0 ) \/
      (dih_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6 < &0 /\ b24 )
)`;;

let  PROIQUZ_hexall_5A1_idq t i =  {
  ineq =  t;
   idv = Printf.sprintf "old PROIQUZ hexall 5A1 %d" i;
   doc =    "split a hex along a shortish diagonal.   Flat at node 2.  Case $y_5 + 0.1 \\le y_3+y_4$.";
   tags = [Tex; Flypaper; Penalty (5., 500.);Widthcutoff 0.01]
  (* 
     This case treats Delta bounded away from 0.
   The upper bound is the trivial triangle inequality bound: y5 <= y3  + y4 <= 4 h0.   *)
};;



Parse_ineq.execute_cfsqp 
  {
ineq =  all_forall `ineq
  [
(&2,y1,&2 *h0);
(&2,y2,&2 * h0);
(&2,y3,&2 * h0);
(&2,y4,&2 *h0);
(&2 * h0,y34,#3.3);
(&2,y12,&2*h0);
(&2,y14,&2 * h0)
  ]
  (
    let y23 = y12 in
    let y13 = edge_flat y2 y1 y3       y23 y12 in
      (delta4_y y1 y3 y4 y34 y14 y13 > &0) \/ (delta_y y1 y3 y4 y34 y14 y13 > &10) \/
            (arclength y3 y4 y34 > #2.42) 
      )`;
   idv = "old PROIQUZ hexall 1-d";
   doc =    "split a hex along a shortish diagonal.   Flat at y2.  Old version of hexall 1...";
   tags = [Tex; Flypaper; Penalty (5., 50.); Xconvert;Deprecated]
};;


Parse_ineq.execute_cfsqp 
  {
ineq =  all_forall `ineq
  [
(&2,y1,&2 *h0);
(&2,y2,&2 * h0);
(&2,y3,&2 * h0);
(&2,y4,&2 *h0);
(&2,y12,&2*h0);
(&2 * h0,y34,#4.72);
(&2,y14,&2 * h0)
  ]
  (
    let y23 = y12 in
    let y13 = edge_flat y2 y1 y3       y23 y12 in
     (delta_y y1 y3 y4 y34 y14 y13 > &10) \/
     (delta_y y1 y3 y4 y34 y14 y13 < &0) \/
    (delta4_y y1 y3 y4 y34 y14 y13  < &10) \/
      (upper_dih_y y1 y3 y4 y34 y14 y13 < dih_y y1 y2 y4 (&2 * h0) y14 y12) \/
            (arclength y3 y4 y34 > #2.42) 
      )`;
   idv = "old PROIQUZ hexall 1-a";
   doc =    "split a hex along a shortish diagonal.   Flat at y2.  hexall 1...";
   tags = [Tex; Flypaper; Penalty (500., 8000.); Xconvert;Deprecated]
};;

let euler_ap = new_definition `euler_ap y1  y2 y3 y4 y5 y6 = 
  y1*y2*y3 + y1*(y2*y2 + y3*y3 - y4*y4)/ &2 + y2*(y1*y1 + y3*y3 - y5*y5)/ &2 + 
   y3*(y1*y1 + y2*y2 - y6*y6)/ &2`;;
Parse_ineq.execute_cfsqp 
  {
ineq =  all_forall `ineq
  [
(&2,y1,&2 *h0);
(&2,y2,&2 * h0);
(&2,y3,&2 * h0);
(&2,y4,&2 *h0);
(&2,y12,&2*h0);
(&2 * h0,y34,#4.72);
(&2,y14,&2 * h0)
  ]
  (
    let y23 = y12 in
    let cos242 = -- #0.75 in
    let y13 = edge_flat y2 y1 y3       y23 y12 in
     (delta_y y1 y3 y4 y34 y14 y13 > &10) \/
     (delta_y y1 y3 y4 y34 y14 y13 < &0) \/
     (delta4_y y1 y3 y4 y34 y14 y13  >  &10) \/
     (euler_ap y1 y3 y4 y34 y14 y13 < &0) \/
            (y34 pow 2 > y3 pow 2 + y4 pow 2 - &2 * y3 * y4 * cos242)
      )`;
   idv = "old PROIQUZ hexall 1-b";
   doc =    "split a hex along a shortish diagonal.   Flat at y2.  ";
   (*  // upper approximation cos(2.42) *)
   tags = [Tex; Flypaper;Penalty (5., 5000.);  Xconvert;Deprecated]
   (* If euler < 0, and a flat then tau(quad) >= tau(tri) + flatTerm[2] 
       >= (sol+pi) -sol0
      >= 2pi - sol0 >> tameTableD[6,0]/2, and the estimate holds *)
};;

let dih1_hexall_x = new_definition `dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) = 
   dih_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;;




1;;
(*  (dih_y y1 y3 y4 y34 y14 y13 < dih_y y1 y2 y4 (&2 * h0) y14 y12)  *)

for y14=0 to 1 do 
for y2 = 0 to 1 do
for i = 0 to 2 do
   Parse_ineq.execute_cfsqp (make_hexall y14 y2 i) done done done;;



  {
ineq =  all_forall `ineq
  [
(&2 pow 2,x1,(&2 *h0) pow 2);
(&2 pow 2,x2,(&2 * h0) pow 2);
(&2 pow 2,x3,(&2 * h0) pow 2);
(&2 pow 2,x4,(&2 *h0) pow 2);
((&2 * h0) pow 2,x5,(&4 * h0) pow 2);
(&1,x6,&1)
  ]
  (
    let x12 = &2 pow 2 in
    let x23 = x12 in
    let x14 = &2 pow 2 in
       (taum_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6 > tame_table_d 6 0 / &2) \/
       (dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > #2.425) \/ 
       (delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  < &0) \/ 
 (sqrt(x5) + #0.1 >  sqrt(x3) + sqrt(x4)) \/ 
      (dih_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6 > &0 ))`;
   idv = "old PROIQUZ hexall 5A";
   doc =    "split a hex along a shortish diagonal.   Flat at node 2.  Case $y_5 + 0.1 \\le y_3+y_4$.";
   tags = [Tex; Flypaper; Penalty (5., 500.)]
  (* The upper bound is the trivial triangle inequality bound: y5 <= y3  + y4 <= 4 h0.   *)
};;


Parse_ineq.execute_cfsqp
  {
ineq =  all_forall `ineq
  [
(&2 pow 2,x1,(&2 *h0) pow 2);
(&2 pow 2,x2,(&2 * h0) pow 2);
(&2 pow 2,x3,(&2 * h0) pow 2);
(&2 pow 2,x4,(&2 *h0) pow 2);
((&2 * h0) pow 2,x5,(&4 * h0) pow 2);
(&1,x6,&1)
  ]
  (
    let x12 = &2 pow 2 in
    let x23 = x12 in
    let x14 = &2 pow 2 in
 ( #0.871 * delta4_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6 <
             sqrt (&4 * x1 * delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6) \/
       (delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > &10) \/ 
       (delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  < &0) \/ 
       (delta4_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 x6  > &10)
	)
)`;
   idv = "old PROIQUZ hexall 5AZ";
   doc =    "split a hex along a shortish diagonal.   Flat at node 2.  Case $y_5 + 0.1 \\le y_3+y_4$.";
   tags = [Tex; Flypaper; Penalty (50., 5000.)]
  (* The upper bound is the trivial triangle inequality bound: y5 <= y3  + y4 <= 4 h0.   *)
};;




Parse_ineq.execute_cfsqp 
  {
    ineq =   all_forall `ineq
      [
	(&2,y1,&2 *h0);
	(&2,y3,&2 * h0);
	(&2,y4,&2 * h0);
	(#2.52,y34,&4);
	(&2,y13,#4.05)
      ]
      (
	let y12 = &2 in
        let y2  = &2 in
	let y23 = &2 in
	let y14 = &2 in
	  (( arclength y3 y4 y34 < &0) \/
	     (dih_y y1 y3 y4 y34 y14 y13 > #2.588) \/ 
	     (arclength y1 y3 y13 > arclength y1 y2 y12 + arclength y2 y3 y23)  ))`;
    idv = "hexall test5";
    doc =    "";
    tags = [Tex; Flypaper; Penalty (5., 50.); Xconvert]
};;

Parse_ineq.execute_cfsqp 
  {
    ineq =   all_forall `ineq
      [
	(&2,y1,&2 *h0);
	(&2,y3,&2 * h0);
	(&2,y4,&2 * h0);
	(#2.52,y34,&4);
	(&2,y13,#4.05)
      ]
      (
	let y12 = &2 in
        let y2  = &2 in
	let y23 = &2 in
	let y14 = &2 in
	  (( arclength y3 y4 y34 < #2.57573) \/
	     (dih_y y1 y3 y4 y34 y14 y13 > #2.4776) \/ 
	     (arclength y1 y3 y13 > arclength y1 y2 y12 + arclength y2 y3 y23)  ))`;
    idv = "hexall test6";
    doc =    "";
    tags = [Tex; Flypaper; Penalty (5., 50.); Xconvert]
};;


(* end of hex analysis PROIQUZ *)




(* deprecated *)
let sql = new_definition `sql x = 
  if (x < &1)
  then &3/ &8 + (&3*x)/ &4 - x pow 2 / &8 + 
    (&1 - x) pow 3 * ((&12/ &10) * x * (&1 - x) - &4/ &10)
  else sqrt x`;;
(* deprecated (* upper bound when d4 < 0 *)  *)
let upper_dih_x_large = new_definition `upper_dih_x_large x1 x2 x3 x4 x5 x6 =
  (let d = delta_x x1 x2 x3 x4 x5 x6 in
  let d4 = delta_x4 x1 x2 x3 x4 x5 x6 in (
      if (d < &1) then
   pi +  &2 * sqrt x1 * sql d * matan (&4 * x1 * d / (d4 pow 2) ) / d4
      else dih_x x1 x2 x3 x4 x5 x6))`;;


(* deprecated *)
let upper_dih_y_large = new_definition `upper_dih_y_large = y_of_x upper_dih_x_large`;;
(* deprecated *)
let vol_xl = new_definition 
  `vol_xl x1 x2 x3 x4 x5 x6 = sql (delta_x x1 x2 x3 x4 x5 x6) / &12`;;
let vol_yl = new_definition `vol_yl = y_of_x vol_xl`;;
let vol3rl = new_definition `vol3rl y1 y2 y3 r = vol_yl r r r y1 y2 y3`;;
let sol_yu_large = new_definition `sol_yu_large y1 y2 y3 y4 y5 y6 =
         upper_dih_y y1 y2 y3 y4 y5 y6 +
         upper_dih_y y2 y3 y1 y5 y6 y4 +
         upper_dih_y_large y3 y1 y2 y6 y4 y5 - pi`;;
let vol3fu_large = new_definition ` vol3fu_large y1 y2 y3 r f =
         (&2 * mm1 / pi) *
         (sol_yu_large y1 y2 r r r y3 + sol_yu_large y2 y3 r r r y1 + sol_yu_large y3 y1 r r r y2) -
         (&8 * mm2 / pi) *
         (f (y1 / &2) * upper_dih_y y1 y2 r r r y3 +
          f (y2 / &2) * upper_dih_y y2 y3 r r r y1 +
          f (y3 / &2) * upper_dih_y y3 y1 r r r y2)`;;
let gamma3fl_large = new_definition `gamma3fl_large y1 y2 y3 r f = vol3rl y1 y2 y3 r - vol3fu_large y1 y2 y3 r f`;;


(*  tests May 2011 *)

Ineq.add
  {
idv = "test 2065952723 C-3";
doc = "See explanation in 2065952723.  Used to replace extremal edges with minimal edges in a
    hexagon.  Used in hexagons when every oparc >= 2.42, and after it is established that the
    edges (b2) adjacent to the oparc are mimial (via Bp1), this gives that the edge not adjacent to
the oparc is minimal.";
(* 15.53 > 3.94^2, arc[2,2,3.94] > 2 arc[2,2,2 hmid], to get the upper bound.
    Lower via, arc[2,2,2.53]+arc[2,2,2] < 2.42
     *)
tags = [Flypaper["UPONLFY"];Tex];
ineq = all_forall `ineq
  [
  (&1 , e1, &1 + sol0/ pi);
  (&1 , e2, &1 + sol0/ pi);
  (&1 , e3, &1 + sol0/ pi);
  ((&2 / h0) pow 2, a2, (&2 * h0) pow 2);
  ((&2 / h0) pow 2, b2, &4);
  (#2.53 pow 2, c2, #15.53)
  ]
   ((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
};;


(* Tests May 2011 *)





addtex (Section,"Experiments","");;

Parse_ineq.execute_cfsqp
  {
idv = "2065952723  experiment";
doc = "In a pentagon with one long edge, we can contract the long edge, using 2 diags";
tags = [Cfsqp;Tex;Flypaper[];];
ineq = all_forall `ineq
  [
  (&1 , e1, &1 + sol0/ pi);
  (&1 , e2, &1 + sol0/ pi);
  (&1 , e3, &1 + sol0/ pi);
  (&2 pow 2, a2, #3.01 pow 2);
  (#2.38 pow 2, b2, #15.53);
  (#2.38 pow 2, c2, #15.53)
  ]
   ((num1 e1 e2 e3 a2 b2 c2  > &0) ) `;
};;


Parse_ineq.execute_cfsqp
  {
idv = "hex  experiment, reflex vertex.";
doc = "can go reflexive in a hex";
tags = [Cfsqp;Tex;Flypaper[];];
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 > &0 \/
   (delta_y y1 y2 y3 y4 y5 y6 < (#0.24 pow 2) * ups_x (y2 * y2) (y3* y3) (y4*y4)))`;
};;



Parse_ineq.execute_cfsqp
  {
idv = "hex  experiment contraction.";
doc = "another failed experiment";
tags = [Cfsqp;Tex;Flypaper[];];
ineq = all_forall `ineq
  [
  (&1 , e1, &1 + sol0/ pi);
  (&1 , e2, &1 + sol0/ pi);
  (&1 , e3, &1 + sol0/ pi);
  (&1 , e4, &1 + sol0/ pi);
  (#3.35 pow 2, a2, #3.915 pow 2);
  ((&2/ h0) pow 2, b2,&4);
  ((&2/ h0) pow 2, c2,&4);
  (#3.01 pow 2, r2,#3.915 pow 2);
  (#3.01 pow 2, s2,#3.915 pow 2)
  ]
   (( rat1 e1 e2 e3 a2 b2 c2 +  rat1 e4 e2 e3 a2 r2 s2  > &0) 
    \/ delta_x (&4) (&4) (&4) a2 b2 c2 < &0 
    eulerA_x (&4) (&4) (&4) a2 r2 s2 < &0 \/
    (dih_x (&4) (&4) (&4) a2 b2 c2 > #2.588 )) `;
};;


Parse_ineq.execute_cfsqp
  {
idv = "hex  experiment";
doc = "cut away a triangle with penalty 0.08";
tags = [Cfsqp;Tex;Flypaper[];];
ineq = all_forall `ineq
  [
  (&2,y1,#2.52);
  (&2,y2,#2.52);
  (&2,y3,#2.52);
  (#3.01,y4,#3.35);
  (&2,y5,&2);
  (&2,y6,&2)
  ]
  ( taum y1 y2 y3 y4 y5 y6 > -- #0.08 \/
   (dih_y y1 y2 y3 y4 y5 y6 > #2.588))`;
};;


(*

 (e1 * dih_x (&4) (&4) (&4) a2 b2 c2 + e2 * dih_x (&4) (&4) (&4) b2 c2 a2
        + e3 * dih_x (&4) (&4) (&4) c2 a2 b2 - (pi + sol0) > -- #0.2) \/

*)


Parse_ineq.execute_cfsqp
{
  idv = "1928747871-0";
  doc="pure hexagon case";
  tags = [Cfsqp;Xconvert;Tex];
  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 
    >  tame_table_d 6 0   \/ y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0 )`;
};;

Parse_ineq.execute_cfsqp
{
  idv = "1928747871-1";
  doc="pure hexagon case";
  tags = [Cfsqp;Xconvert;Tex];
  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)
  ]
(let y126 = edge_flat y6 y1 (&2)    (&2) y2 in
(let y135 = edge_flat y5 y1 (&2)    (&2) y5 in
(let y234 = edge_flat y4 y2 (&2)    (&2) y3 in
    (taum y1 y2 y3 y4 y5 y6 
  + taum y126 y1 y2 y6 (&2) (&2)
  + taum y135 y1 y3 y5 (&2) (&2)
  + taum y234 y2 y3 y4 (&2) (&2) 
    > &3 * #0.001 + tame_table_d 6 0  ) \/
  y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0 \/  
 (y126 < #2.0 \/ y126 > #2.52 \/
  y135 < #2.0 \/ y135 > #2.52 \/ 
  y234 < #2.0 \/ y234 > #2.52))))`;
};;


Parse_ineq.execute_cfsqp
{
  idv = "1928747871-2";
  doc="pure hexagon case";
  tags = [Cfsqp;Xconvert;Tex];
  ineq = all_forall `ineq [
    (&2,y1,#2.4);
    (&2,y2,#2.4);
    (&2,y3,#2.4);
    (#3.01,y4,#3.47);
    (#3.01,y5,#3.47);
      (#3.01,y6,#3.47)
  ]
((taum y1 y2 y3 y4 y5 y6 > tame_table_d 6 0  ) \/
  y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0)`;
};;


Parse_ineq.execute_cfsqp
{
  idv = "1928747871-(1)";
  doc="pure hexagon case, side triangle";
  tags = [Cfsqp;Xconvert;Tex];
  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)
  ]
(
(let y234 = edge_flat y4 y3 (&2)     (&2) y2 in
(taum y1 y2 y3 y4 y5 y6 + #0.013 > taum y234 y2 y3 y4 y5 y6) \/
(y234 > #2.52) \/ (y234 < #2.0)))`;
};;

Parse_ineq.execute_cfsqp
{
  idv = "1928747871-(2)";
  doc="pure hexagon case, side triangle (2)";
  tags = [Cfsqp;Xconvert;Tex];
  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)
  ]
(
(taum y1 y2 y3 y4 y5 y6 + #0.001 > taum (#2.52) y2 y3 y4 y5 y6) \/
(delta_y (#2.52) y2 y3 y4 y5 y6 < &0) \/ (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
taum (#2.52) y2 y3 y4 y5 y6 > taum (&2) y2 y3 y4 y5 y6 
)`;
};;

  

Parse_ineq.execute_cfsqp
{
  idv = "1928747871-(3)";
  doc="pure hexagon case, side triangle (3)";
  tags = [Cfsqp;Xconvert;Tex];
  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)
  ]
(
  ( taum y1 y2 y3 y4 y5 y6 + #0.09 > taum (&2) y2 y3 y4 y5 y6) \/
  (delta_y (&2) y2 y3 y4 y5 y6 < &0) \/
(delta_y (#2.52) y2 y3 y4 y5 y6 < &0) \/
 (delta_y y1 y2 y3 y4 y5 y6 < &0)
)`;
};;

(* taum (#2.52) y2 y3 y4 y5 y6 > taum (&2) y2 y3 y4 y5 y6 \/

*)



Parse_ineq.execute_cfsqp
{
  idv = "";
  doc="upper bound on minor variable when top edges are 2.
   This has been replaced with  a delta version.";
  tags = [Cfsqp;Penalty(50.0,500.0);Xconvert;Tex;Deprecated];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#4.52)
  ]
((y3 < #3.915) \/ (arclength y1 (&2) (&2) + arclength y2 (&2) (&2) < arclength y1 y2 y3)
 \/ (y3 > y1 + y2) )`;
};;


Parse_ineq.execute_cfsqp
{
  idv = "test temp";
  doc="pure hexagon case";
  tags = [Cfsqp;Xconvert;Tex];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (#3.3,y4,#3.915);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
    (rhazim  y1 y2 y3 y4 y5 y6  + #0.6 * (-- &2 * y1 +  y2 + y3) > &0 \/ delta_y y1 y2 y3 y4 y5 y6 < &0)`;
};;



add  {
idv = "2065952723 C-3z";
doc = "If  minor diag >= 3, then 3/1.26 > 2.38 and we can contract.
          15.53: arc[2,2,2.52]2 < arc[2,2,Sqrt[15.53]].
           Added May 12, 2011.
       Replace May 15, 2011, with an inequality with bigger upper b2 bound.";
tags = [Cfsqp;Tex;Flypaper[];Deprecated];
ineq = all_forall `ineq
  [
  (&1 , e1, &1 + sol0/ pi);
  (&1 , e2, &1 + sol0/ pi);
  (&1 , e3, &1 + sol0/ pi);
  ((&2 / h0) pow 2, a2, (&2 * h0) pow 2);
  ((&2 / h0) pow 2, b2, (&2 * h0) pow 2);
  (#2.38 pow 2, c2, #15.53)
  ]
   ((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
};;


Parse_ineq.execute_cfsqp
  {
idv = "206 ee2";
doc = "FALSE";
tags = [Cfsqp;Tex;Flypaper[];];
ineq = all_forall `ineq
  [
  (&1 , e1, &1 + sol0/ pi);
  (&1 , e2, &1 + sol0/ pi);
  (&1 , e3, &1 + sol0/ pi);
  ((&2 ) pow 2, a2, (#3.01) pow 2);
  ((&2) pow 2, b2, #3.01 pow 2);
  (#2.38 pow 2, c2, #15.53)
  ]
   ((num1 e1 e2 e3 a2 b2 c2 ) > &0) `;
};;


Parse_ineq.execute_cfsqp
{
  idv = "un";
  doc="quad case both diags > 3.01, y5, y9 long";
  tags = [Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.22);
      (#2.52,y5,#2.52);
      (#2.0,y6,&2);
      (#2.0,y7,&2 * h0);
      (#2.0,y8,&2);
      (#2.52,y9,#2.52)]
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;




Parse_ineq.execute_cfsqp
{
  idv = "un";
  doc="quad case both diags > 3.01, y5, y9 long.
    Triangulate if a diagonal <= 3.3.";
  tags = [Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.3,y4,#3.41);
      (#2.52,y5,#2.52);
      (#2.0,y6,&2);
      (#2.0,y7,&2 * h0);
      (#2.0,y8,&2);
      (#3.01,y9,#3.01)]
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.3 ))`;
};;


Parse_ineq.execute_cfsqp
{
  idv = "un";
  doc="quad case both diags > 3.01, y5, y9 long";
  tags = [Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.62);
      (#3.01,y5,#3.01);
      (#2.0,y6,&2);
      (#2.0,y7,&2 * h0);
      (#2.0,y8,&2);
      (#3.01,y9,#3.01)]
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;


Parse_ineq.execute_cfsqp
{
  idv = "un";
  doc="quad case both diags > 3.01, y6, y9 long";
  tags = [Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.18);
      (#2.0,y5,&2);
   (#2.52,y6,#2.52);
      (#2.0,y7,&2 * h0);
       (#2.0,y8,&2);  
      (#2.52,y9,#2.52)]
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;


Parse_ineq.execute_cfsqp
{
  idv = "un";
  doc="quad case both diags > 3.01, y6, y9 long";
  tags = [Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.33);
      (#2.0,y5,&2);
     (#2.52,y6,#2.52);
      (#2.0,y7,&2 * h0);
       (#2.0,y8,&2);
      (#3.01,y9,#3.01)]
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;


Parse_ineq.execute_cfsqp
{
  idv = "un";
  doc="quad case both diags > 3.01, y6, y9 long";
  tags = [Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.47);
      (#2.0,y5,&2);
     (#3.01,y6,#3.01);
      (#2.0,y7,&2 * h0);
       (#2.0,y8,&2);
      (#3.01,y9,#3.01)]
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;



{
  idv="3916387088";
  doc="quad case both diags > 3.01, y8, y9 long
  This case has been deprecated.  We can deform y9 to shorten by 8964099283
  ";
  tags = [Main_estimate;Quad_cluster 0.001;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);
   Deprecated];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.47);
      (#2.0,y5,&2);
       (#2.0,y6,&2);
      (#2.0,y7,&2 * h0);
     (#3.01,y8,#3.01);
      (#3.01,y9,#3.01)]
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;

{
  idv="4033589145";
  doc="quad case both diags > 3.01, y8, y9 long.
   This case is now triangulated with long diagonal.";
  tags = [Main_estimate;Quad_cluster 0.001;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);
	 Deprecated];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.18);
      (#2.0,y5,&2);
       (#2.0,y6,&2);
      (#2.0,y7,&2 * h0);
     (#2.52,y8,#2.52);
      (#2.52,y9,#2.52)]
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;




{
  idv="8035675159";
  doc="quad case both diags > 3.01, y8, y9 long";
  tags = [Main_estimate;Quad_cluster 0.001;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);
    Deprecated];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.33);
      (#2.0,y5,&2);
       (#2.0,y6,&2);
      (#2.0,y7,&2 * h0);
     (#2.52,y8,#2.52);
      (#3.01,y9,#3.01)]
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9    > tame_table_d 2 2) \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;


skip
{
  idv="5501385627";
  doc=" tameTableD[2,2]. 
  Triangulate quad with diagonal y4.
  Case both diags > 3.01, y8, y9 long, short diagonal doesn't separate long edges.
  Shorter diag < 3.15

  This has delta=0 issues that are resolved by using tau_lowform_x.
  Ran overnight May16-17, 2011 several hours and it didn't pass.
  ";
  tags = [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.15);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
  ( y_of_x tau_lowform_x y1 y2 y3 y4 y5 y6 > -- #0.2 ) 
 )`;
};;


skip
{
  idv="8672459448";
  doc=" tameTableD[2,2]. 
  Case both diags > 3.01, y8, y9 long (at 2.52 and 3.01), 
  short diagonal doesn't separate long edges.
  Shorter diag < 3.15
  Triangulate quad with diagonal y4";
  tags = [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.15);
    (#3.01,y5,#3.01);
      (#2.52,y6,#2.52)
  ]
(
  ( taum y1 y2 y3 y4 y5 y6 > tame_table_d 2 2 + #0.2 ) 
 )`;
};;





experiment {
  idv="4680581274 test modification";
  doc="quad case both diags > 3.01, y9 long";
  tags = [Main_estimate;Cfsqp;Quad_cluster 0.001;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.166);
      (#2.0,y5,&2);
      (#2.0,y6,&2);
      (#2.0,y7,&2 * h0);
      (#2.0,y8,&2);
      (#3.01,y9,#3.01)]
((   (let d = delta_y y1 y2 y3 y4 y5 y6  in
    (rho (y1) * pi - (pi + sol0) + 
    sqp d * y_of_x rhazim_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 +
  sqn d * (#0.1 
   - #0.02 * (y2 + y3 - &2 * #2.52) - #0.06 * (y4 - #3.166)) ))
   + taum y7 y2 y3 y4 y8 y9    > #0.696 - #0.11) \/
  delta4_y y1 y2 y3 y4 y5 y6 > -- #11.2 \/
    delta_y y1 y2 y3 y4 y5 y6 < &0 \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;

(*
y_of_x rhazim2_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6
*)

(*
   y_of_x rhazim2_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 +
   y_of_x rhazim3_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 > #0.1 
   - #0.02 * (y2 + y3 - &2 * #2.52) - #0.06 * (y4 - #3.166)
*)



Ineq.add
{
  idv="5501385627 test";
  doc=" tameTableD[2,2]. 
  Triangulate quad with diagonal y4.
  Case both diags > 3.01, y8, y9 long, diagonal doesn't separate long edges.
  Shorter diag < 3.15

  This has delta=0 issues that are resolved by using tau_lowform_x.
  Ran overnight May16-17 several hours and it didn't pass.
  ";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;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.15);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
  ( y_of_x tau_lowform_x y1 y2 y3 y4 y5 y6 > -- #0.2 )  \/
   (delta_y y1 y2 y3 y4 y5 y6 < &5)
 )`;
};;


(* May 22, 2011 experiments *)


experiment {
  idv="";
  doc="";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;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.166);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
   taum y1 y2 y3 y4 y5 y6  > -- #0.08 \/
   delta_y y1 y2 y3 y4 y5 y6 < -- &25
 )`;
};;



experiment {
  idv="";
  doc="";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;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.166);
  (sqrt8,y5,sqrt8);
      (&2,y6,&2)
  ]
(
   taum y1 y2 y3 y4 y5 y6  > #0.696 - #0.11 + #0.08 
 )`;
};;

experiment {
  idv="";
  doc="";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;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);
    (#3.01,y5,#3.915);
      (#3.01,y6,#3.915)
  ]
(  delta_y (#2.52) y2 y3 y4 (&2) (&2) > &0  \/
 (taum y1 y2 y3 y4 y5 y6 )/ &3 - sol0
 + #0.34 * (&2 * y4 - y5 - y6)   >  (#0.6)/ &3  
 )`;
};;

experiment {
  idv="FALSE ONE.";
  doc=" This shows that taum_residual is always negative on the given domain.
  This should be rewritten in terms of the residual.
  ";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;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.36);
    (&2,y5,#2.52);
      (&2,y6,#2.52)
  ]
(
y_of_x tau_residual_x y1 y2 y3 y4 y5 y6 < &0
  \/
  (delta4_y y1 y2 y3 y4 y5 y6 > -- #11.2) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
  (taum y1 y2 y3 y4 y5 y6 > #0.25)
 )`;
};;

(* 
(( taum y1 y2 y3 y4 y5 y6 - ((rho y1) * pi - (pi+sol0)))/ (#0.0001 + sqrt(delta_y y1 y2 y3 y4 y5 y6)) < &0)    
*)

experiment {
  idv="";
  doc="Debug implementation test of tau_lowform ";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (#2.1,y1,#2.1);
    (#2.2,y2,#2.2);
    (#2.3,y3,#2.3);
    (#3.6,y4,#3.6);
    (#2.5,y5,#2.5);
      (#2.6,y6,#2.6)
  ]
(
  ( y_of_x tau_lowform_x y1 y2 y3 y4 y5 y6 > taum y1 y2 y3 y4 y5 y6 - &1 ) 
 )`;
};;

experiment
{
  idv="";
  doc="Aux 734849949. To show for some diag cut, the small delta > 37";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;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.63);
    (#3.01,y5,#3.651);
      (&2,y6,&2)
  ]
(
  dih_y y1 y2 y3 y4 y5 y6 < #2.08 \/
    ((y4 - #3.2) > #0.55 * (y2 + y3 - &4))
 )`;
};;

experiment
{
  idv="";
  doc="Aux 734849949. To show for some diag cut, the small delta > 37.";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (&2,y5,&2);
      (#3.01,y6,#3.651)
  ]
(
  dih_y y1 y2 y3 y4 y5 y6 < #0.51 \/
  delta_y y1 y2 y3 y4 y5 y6 > &37 \/
  delta_y y1 y2 y3 y4 y5 y6 < &0
 )`;
};;

experiment
{
  idv="";
  doc="Aux 734849949. To show for some diag cut, the small delta > 37.";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (&2,y5,&2);
      (#3.01,y6,#3.651)
  ]
(
  taum y1 y2 y3 y4 y5 y6 > &0 \/
  delta_y y1 y2 y3 y4 y5 y6 < &37 
 )`;
};;


experiment
{
  idv="";
  doc="Aux 734849949. To show for some diag cut, the small delta > 37.";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;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.356);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
  dih_y y1 y2 y3 y4 y5 y6 > #2.08 + #0.51 \/
  delta_y y1 y2 y3 y4 y5 y6 > &37 \/
  delta_y y1 y2 y3 y4 y5 y6 < &0
 )`;
};;

experiment
{
  idv="experiment May 18, 2011, 7348498949";
  doc="pentagon case, quad piece, cut along y9.
   Upper bound on diagonal:
   Solve[Delta[x, 2, 2, x, 2, 3.63] == 0, x](*x < 3.356 *) ";
  tags = [Main_estimate;Quad_cluster 0.001;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);
   Widthcutoff 0.08];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.651);
      (#2.0,y5,&2);
      (#2.0,y6,&2);
      (#2.0,y7,&2 * h0);
      (#2.0,y8,&2);
      (#3.01,y9,#3.63);
      (#3.01,cd,#3.651)
]
(( delta_y y1 y2 y3 y4 y5 y6 > &65) \/
   (delta_y y3 y1 y7 cd y8 y5 > &65) \/
  ((y9 - #3.2) > #0.55 * (y2 + y7 - &4)) \/ 
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < cd ))`;
};;


experiment
{
  idv="7348498949 37 616";
  doc="pentagon case, quad piece, cut along y9.
   Upper bound on diagonal:
   Use whichever diagonal produces the (2,2,diag) triangle with largest delta.
   Solve[Delta[x, 2, 2, 3.01, 3.63, 2] == 0, x] (* x < 3.651 *)
   shorter diag (not used):
   Solve[Delta[x, 2, 2, x, 2, 3.63] == 0, x](*x < 3.356 *).
   Experiment May 18, 9am, try 0.616 instead of 0.696. ";
  tags = [Main_estimate;Quad_cluster 0.001;Cfsqp;Xconvert;Tex;Penalty(1500.0,5000.0);
   (* Widthcutoff 0.08 *)];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.651);
      (#2.0,y5,&2);
      (#3.01,y6,#3.63);
      (#2.0,y7,&2 * h0);
      (#2.0,y8,&2);
      (#2.0,y9,&2)
]
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9  > #0.616) \/
  ((y6 - #3.2) > #0.55 * (y2 + y1 - &4)) \/ 
  delta_y y7 y2 y3 y4 y8 y9 < &37  \/
  delta4_y y7 y2 y3 y4 y8 y9 > -- #11.2 \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;

experiment
{
  idv="";
  doc="taum 1st deriv test.";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;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)
  ]
(
  ( tau_m_diff_quotient y1 y2 y3 y4 y5 y6 pow 2 > #0.031) \/
  (delta_y y1 y2 y3 y4 y5 y6 > &15) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0)
 )`;
};;

addtex(Section,"","skinny triangles");;

add
{
  idv="";
  doc="linear bound on taum, 2,2,2.";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(1500.0,5000.0);Deprecated];
  ineq = all_forall `ineq [
    (&2,y1,#2);
    (#2.0,y2,#2);
    (&2,y3,#2);
    (#3.01,y4,#3.915);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
  (y_of_x tau_lowform_x y1 y2 y3 y4 y5 y6 > #4.488 - #1.4579 * y4 ) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0)
 )`;
};;

add
{
  idv="";
  doc="linear bound on taum, 2.52,2,2.";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(1500.0,5000.0);Deprecated];
  ineq = all_forall `ineq [
    (#2.52,y1,#2.52);
    (#2.0,y2,#2);
    (&2,y3,#2);
    (#3.01,y4,#3.915);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
  (y_of_x tau_lowform_x y1 y2 y3 y4 y5 y6 > #4.488 - #1.4579 * y4 ) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0)
 )`;
};;


add
{
  idv="";
  doc="linear bound on taum, flat,2,2.";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(1500.0,5000.0);Deprecated];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2);
    (&2,y3,#2);
    (#3.01,y4,#3.915);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
  (?? > #4.488 - #1.4579 * y4 ) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0)
 )`;
};;



add
{
  idv="test";
  doc="hexagon case, triangulated by large inner triangle.
    Three outer triangles replaced with linear lower bounds.
    Bottom edges 2,2,2.
    ";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,&2);
    (#2.0,y2,&2);
    (&2,y3,&2);
    (#3.01,y4,#3.47);
    (#3.01,y5,#3.47);
      (#3.01,y6,#3.47)
  ]
(
  ( taum y1 y2 y3 y4 y5 y6  
    + #4.488 - #1.4579 * y4
    + #4.488 - #1.4579 * y5
    + #4.488 - #1.4579 * y6
> #0.0) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
  (y_of_x eulerA_x  y1 y2 y3 y4 y5 y6 < &0))`;
};;

add
{
  idv="test";
  doc="hexagon case, triangulated by large inner triangle.
    Three outer triangles replaced with linear lower bounds.
    Bottom edges 2.52,2,2.
    ";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (#2.52,y1,#2.52);
    (#2.0,y2,&2);
    (&2,y3,&2);
    (#3.01,y4,#3.47);
    (#3.01,y5,#3.737);
      (#3.01,y6,#3.737)
  ]
(
  ( taum y1 y2 y3 y4 y5 y6  
    + #4.488 - #1.4579 * y4
    + #3.2139 - #1.009 * y5
    + #3.2139 - #1.009 * y6
> #0.0) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
  (y_of_x eulerA_x  y1 y2 y3 y4 y5 y6 < &0))`;
};;


add
{
  idv="test";
  doc="hexagon case, triangulated by large inner triangle.
    Three outer triangles replaced with linear lower bounds.
    Bottom edges 2.52,2.52,2.
    ";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (#2.52,y1,#2.52);
    (#2.52,y2,#2.52);
    (&2,y3,&2);
    (#3.01,y4,#3.737);
    (#3.01,y5,#3.737);
      (#3.01,y6,#3.915)
  ]
(
  ( taum y1 y2 y3 y4 y5 y6  
    + #3.2139 - #1.009 * y4
    + #3.2139 - #1.009 * y5
    + #3.2883 - #0.98119 * y6
> #0.0) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
  (y_of_x eulerA_x  y1 y2 y3 y4 y5 y6 < &0))`;
};;


add
{
  idv="test";
  doc="hexagon case, triangulated by large inner triangle.
    Three outer triangles replaced with linear lower bounds.
    Bottom edges 2.52,2.52,2.52
    ";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (#2.52,y1,#2.52);
    (#2.52,y2,#2.52);
    (#2.52,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  
    + #3.2883 - #1.009 * y4
    + #3.2883 - #1.009 * y5
    + #3.2883 - #0.98119 * y6
> #0.0) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
  (y_of_x eulerA_x  y1 y2 y3 y4 y5 y6 < &0))`;
};;

(*
We get zeros via y2,y3 in {2,2.52} in
x /. Solve[Delta[2, y2, y3, x, 2, 2] == 0, x] // N // FullForm
{3.01, 3.4641016151377544, 3.7355742827650995, 3.914039468375351}
*)

experiment.
{
  idv="test";
  doc="hexagon case, two oppositely situated flat vertices, making an effective quad.
    Triangulated by short diagonal.
    Bottom edges ?,2,2.
    ";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,&2);
    (&2,y3,&2);
    (#3.01,y4,#3.47);
    (#3.01,y5,#3.47);
      (#3.01,y6,#3.47)
  ]
(
  let plow = (\y. #4.498 - #1.4579 * y) in
  let pmid = (\y. #3.2139 - #1.0009 * y) in
  let phi = (\y. #3.2883 - #0.98119 * y) in
  let psol = (\(y:real). -- #0.552) in
  ( taum y1 y2 y3 y4 y5 y6  + plow y4 + plow y5 + plow y6 > &0) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
  (y_of_x eulerA_x  y1 y2 y3 y4 y5 y6 < &0))`;
};;

(* OLD:
let template_ineq_hexx  = 
`\y2fix y3fix y4max y5min y5max y6min y6max p4 p5 p6.
  ineq [
    (&2,y1,#2.52);
    (y2fix,y2,y2fix);
    (y3fix,y3,y3fix);
    (#3.01,y4,y4max);
    (y5min,y5,y5max);
      (y6min,y6,y6max)
  ]
(  ( taum y1 y2 y3 y4 y5 y6  + p4 y4 + p5 y5 + p6 y6 > #0.723) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
  (y_of_x eulerA_x  y1 y2 y3 y4 y5 y6 < &0))`;;
*)


(* OLD:
let mk_hex i4 i5 i6  = 
  (* we subtract off small correction terms to simplify proofs *)
  let plo = `(\y. #4.498 - #0.02 - #1.4579 * y)` in
  let pmid = `(\y. #3.2139 - #0.025 - #1.0009 * y)` in
  let phi = `(\y. #3.2883 - #0.01 - #0.98119 * y)` in
  let psol = `(\ (y:real). -- sol0 )` in
  let y2fix = List.nth [`&2`;`#2.52`;`#2.52`] i4 in
  let y3fix = List.nth [`&2`;`&2`;`#2.52`] i4 in
  (* round up on these values *)
  let (y3,y34,y37,y39) = (`#3.01`,`#3.46411`,`#3.73558`,`#3.91404`) in
  let (p4,y4max) = List.nth [(plo,y34);(pmid,y37);(phi,y39)] i4 in
  let vlo = [(y3,y34,plo);(y34,y37,psol)] in
  let vhi = [(y3,y37,pmid);(y37,y39,psol)] in
  let (y5min,y5max,p5) =
    let v = if (i4<2) then vlo else vhi in List.nth v i5 in
  let (y6min,y6max,p6) = 
    let v = if (i4<1) then vlo else vhi in List.nth v i6 in
  let inq = 
    mk_tplate template_ineq_hexx 
      [y2fix;y3fix;y4max;y5min;y5max;y6min;y6max;p4;p5;p6] in
  let s = string_of_int in
  let ext = " "^(s i4)^(s i5)^(s i6) in 
    template_record_hexx inq ext;;

*)


(* PENTAGONS, CHaff from May 22-23, 2011. *)


skip
{
  idv="6438897006";
  doc="pentagon case (4,1), quad piece, cut along y9
  The upper bound on the shorter diagonal determined by
  Solve[Delta[x, 2, 2, x, 2, 3.01] == 0, x], (* x < 3.166 *).
  Deprecated because it is a special case of 4680581274.";
  tags = [Main_estimate;Quad_cluster 0.001;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);
   Deprecated];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.166);
      (#2.0,y5,&2);
      (#2.0,y6,&2);
      (#2.0,y7,&2 * h0);
      (#2.0,y8,&2);
      (#3.01,y9,#3.01)]
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9  > tame_table_d 4 1 -  #0.11) \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;


let template_ineq_pent  = 
`\y1fix y2fix y3fix  p5 p6.
  ineq [
    (y1fix,y1,y1fix);
    (y2fix,y2,y2fix);
    (y3fix,y3,y3fix);
    (&2,y4,&2);
    (#3.01,y5,#3.23607);
      (#3.01,y6,#3.23607)
  ]
(
  ( taum y1 y2 y3 y4 y5 y6   + p5 y5 + p6 y6 > #0.616) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
    (dih_y y1 y2 y3 y4 y5 y6 + dih_y y1 y2 (&2) (&2) (&2) y6 +
    dih_y y1 (&2) y3 (&2) y5 (&2) < dih_y y1 y2 y3 (#3.01) (&2) (&2))
)`;;


let template_record_pent inq ext =
{
  idv=("test5"^ext);
  doc="pentagon case, triangulated with a large central triangle.
     Wlog no vertex of the central triangle is flat, so y1,y2,y3 are extremal.
     Outer triangles are removed and replaced with p bounds.";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0)];
  ineq = inq;
};;

  (* we subtract off small correction terms to make things easier to prove *)


(*
pmid: interp[x, {3.01, 
    taumar[2, 2, 2.52, 3.01, 2, 2]}, {3.23607, taumar[2, 2, 2.52, 3.23607, 2,
         2]}] // ExpandAll

phi: interp[x, {3.01, 
    taumar[2, 2.52, 
      2.52, 3.01, 2, 2]}, {3.23607, taumar[2, 2.52, 2.52, 3.23607, 2, 2]}] // 
    ExpandAll
*)

let mk_pent i1 j4  = 
  let plo = `(\y. #4.498 - #0.02 - #1.4579 * y)` in
  let pmid = `(\y. #0.713 - #0.177 * y)` in
  let phi = `(\y. #0.752  - #0.174 * y)` in
  let y1fix = List.nth [`&2`;`#2.52`] i1 in
  let y2fix = List.nth [`&2`;`#2.52`;`#2.52`] j4 in
  let y3fix = List.nth [`&2`;`&2`;`#2.52`] j4 in
  let (p5) = if (i1<1 && j4<1) then plo
  else (if (i1>0 && j4>0) then phi else pmid) in
  let (p6) = if (i1<1 && j4<2) then plo
  else (if (i1>0 && j4>1) then phi else pmid) in
  let inq = 
    mk_tplate template_ineq_pent
      [y1fix;y2fix;y3fix;p5;p6] in
  let s = string_of_int in
  let ext = " "^(s i1)^(s j4) in
    template_record_pent inq ext;;

(* closest case is 2 1 1*)

 for i1=0 to 1 do 
 for j4 = 0 to 2 do
   experiment(mk_pent i1 j4)   done done;;



addtex(Comment,"",
  "
  The context is a pentagon whose top edges are all 2.
  The diagonals are all at least 3.01.
  Since tameTableD[5,0] < 0.696, the tameTableD[5,0] bound is a corollary of 0.696.
  Thus, it is enough to treat 0.696.

  The general strategy is that there must exist a triangle with
  minor diag <= 3.63 and angle <= 2.355.
    The constant 2.355 comes from the tau calculation:
    Solve[5x - 3(Pi + sol0) == 0.696, x]  (* gives 2.354... *)
  The constant 3.63 comes by an ineq that follows.
  This triangle is cut from the pentagon, leaving a quad case that can be done directly.
  The lower bound of tau on the cut triangle is 0.
  ");;

add
{
  idv="8655116269 a";
  doc="pentagon case, clipped smallest angled side triangle.
   If dih clipped < 2.355, then y4 < 3.63.
  ";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#3.63,y4,#3.915);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
(dih_y y1 y2 y3 y4 y5 y6 > #2.355 )\/ 
(delta4_y y1 y2 y3 y4 y5 y6 < &0) )`;
};;


add {
  idv="8655116269 b";
  doc="pentagon case, clipped smallest angled side triangle.
   Case dih > pi/2.
   If dih clipped < 2.355, then y4 < 3.63.
   The dih_y > #2.355 disjunct has been linearized, using delta4 < 0.
  ";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (#2.0,y2,#2.52);
    (&2,y3,#2.52);
    (#3.63,y4,#3.915);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
(  (let tan_sq_lower = &1 in 
    delta4_squared_y y1 y2 y3 y4 y5 y6 * tan_sq_lower > 
    &4 * x1_delta_y  y1 y2 y3 y4 y5 y6 ) \/ 
(delta4_y y1 y2 y3 y4 y5 y6 > &0) \/

  (delta_y y1 y2 y3 y4 y5 y6 < &0)  ))`;
};;


add
{
  idv="3193572903 a";
  doc="pentagon case, clipped smallest angled side triangle.
   If all dih > 2.355, then tau >= 5 (2.355) - 3 (pi + sol0) > 0.696 =largest pent constant";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;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.63);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
  ( taum y1 y2 y3 y4 y5 y6  > #0.0) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
  (delta4_y y1 y2 y3 y4 y5 y6 < &0))`;
};;



add
{
  idv="3193572903 b";
  doc="pentagon case, clipped smallest angled side triangle.
   Case dih > pi/2.
   If all dih > 2.355, then tau >= 5 (2.355) - 3 (pi + sol0) > 0.696 =largest pent constant";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;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.63);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
  ( taum y1 y2 y3 y4 y5 y6  > #0.0) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
(delta4_y y1 y2 y3 y4 y5 y6 > &0) \/
(let tan_sq_lower = &1 in 
    delta4_squared_y y1 y2 y3 y4 y5 y6 * tan_sq_lower > 
    &4 * x1_delta_y  y1 y2 y3 y4 y5 y6 ) )`;
};;


add
{
  idv="2050588100 a";
  doc="pentagon case, clipped smallest angled side triangle.
   Here is an additional linear constraint on edge lengths.";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;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.63);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
  ( (y4 - #3.2) < #0.55 * (y2 + y3 - &4)) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
(delta4_y y1 y2 y3 y4 y5 y6 < &0) )`;
};;

add
{
  idv="2050588100 b";
  doc="pentagon case, clipped smallest angled side triangle.
   Case dih > pi/2.
   Here is an additional linear constraint on edge lengths.
   Tan[Pi - 2.355]^2 is approx 1.00479.
   The disjunct is a reworking of dih_y > 2.355.";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;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.63);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
  ( (y4 - #3.2) < #0.55 * (y2 + y3 - &4)) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
(delta4_y y1 y2 y3 y4 y5 y6 > &0) \/
(let tan_sq_lower = #1.0047 in 
    delta4_squared_y y1 y2 y3 y4 y5 y6 * tan_sq_lower > 
    &4 * x1_delta_y  y1 y2 y3 y4 y5 y6 ) 
 )`;
};;


add
{
  idv="7348498949 37";
  doc="pentagon case, quad piece, cut along y9.
   Upper bound on diagonal:
   Use whichever diagonal produces the (2,2,diag) triangle with largest delta.
   Solve[Delta[x, 2, 2, 3.01, 3.63, 2] == 0, x] (* x < 3.651 *)
   shorter diag calc (not used):
   Solve[Delta[x, 2, 2, x, 2, 3.63] == 0, x](*x < 3.356 *) ;
 
  Pending replacement by 37 616";
  tags = [Main_estimate;Quad_cluster 0.001;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);
   (* Widthcutoff 0.08 *)];
  ineq = all_forall `ineq [
      (#2.0,y1,&2 * h0);
      (#2.0,y2,&2 * h0);
      (#2.0,y3,&2 * h0);
      (#3.01,y4,#3.651);
      (#2.0,y5,&2);
      (#3.01,y6,#3.63);
      (#2.0,y7,&2 * h0);
      (#2.0,y8,&2);
      (#2.0,y9,&2)
]
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9  > #0.696) \/
  ((y6 - #3.2) > #0.55 * (y2 + y1 - &4)) \/ 
  delta_y y7 y2 y3 y4 y8 y9 < &37  \/
  delta4_y y7 y2 y3 y4 y8 y9 > -- #11.2 \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < #3.01 ))`;
};;


add
{
  idv="7348498949 slit";
  doc="";
  tags = [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.356);
    (&2,y5,&2);
      (#3.01,y6,#3.63)
  ]
(  let slit = #0.25 in taum y1 y2 y3 y4 y5 y6  + slit  > #0.696  
 \/
 ((y6 - #3.2) > #0.55 * (y1 + y2 - &4))
)`;
};;


addtex (Section,"Tame Table D","Pentagons table[4,1]");;

addtex(Comment,"",
"
The context is a pentagon with one edge in the range [2.52,3.01], obtained
by a cut on a hexagon.  
All diagonals are at least 3.01.
All noncut top edges are 2.
This constant appears directly in the ad hoc LP inequalities
and as part of the tameTableD[6,0] calculation.
");;

(*
tameTableD[4,1]=0.6548 = tameTableD[6,0]-tameTableD[2,1].
*)


addtex(Comment,"",
"
 We continue to contract the long edge, even make it less than 2.52,
    until it reaches 2, in which case (0) the 0.696 estimate takes over.

    (1) Or until a diagonal hits 3.01, where  the long edge lands in the  triangle,
   leaving a quad with top edges 2,2,2,3.01.  The shortest edge of the quad
   is given by Solve[Delta[x,2,2,x,2,3.01]==0,x], which implies x <= 3.166.
   Cut along this diagonal to triangulate.

    (2) Or until two diagonals hit 3.01, triangulating the pent. 
    There are two diagonals, because after the first hits and is fixed at 3.01 
   assuming the long edge lands in the quad, 
    we can continue contraction on the quad.

  Note: if a flat node develops (with some edge > 2), 
  the usual tricks can be used to dissolve it.
");;

skip
{
  idv="4680581274 slit";
  doc="constant -11.2 was changed to 0, so we no longer need this.";
  tags = [Main_estimate;Cfsqp;Xconvert;Tex;Penalty(50.0,500.0);Deprecated];
  ineq = all_forall `ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (#3.01,y4,#3.166);
    (&2,y5,&2);
      (#3.01,y6,#3.01)
  ]
(  let slit = #0.25 in taum y1 y2 y3 y4 y5 y6  + slit  > #0.696 - #0.11  )`;
};;

skip
{
  idv="2428128897";
  doc=" delta=0 issues.
   VERY GOOD DELTA ISSUE RESOLVER
    If taum > 0.25, we can use the 'split' cases below to break off the skinny triangle.
    If taum <= 0.25 then delta4_y < -- #11.2, which we can then assume everywhere.
    -
    Probably not needed now.
    Actually, we can just use 4559601669, and settle for delta4 < 0, and drop this out.
    Then we don't need slits at all.
  ";
  tags = [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 < -- #11.2) \/
  ( taum y1 y2 y3 y4 y5 y6 > #0.25) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0)
 )`;
};;


skip
{
  idv = "4240815464 b";
  doc="This is a variation of  '4240815464 a' with a relaxed constant to make it quicker to prove.";
  tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Tex;Xconvert;Lp;Penalty(10000.0,500.0);Dim_red_backsym;Quad_cluster 0.05];
  ineq = all_forall `ineq (dart_std4 y1 y2 y3 y4 y5 y6 y7 y8 y9)
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 + 
   #0.7573 *dih_y y1 y2 y3 y4 y5 y6 - #1.432 > #0.0) \/
  ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < sqrt8 ) \/
  (y4 < #3.02) \/
( delta_y y1 y2 y3 y4 y5 y6 < &0) \/
( delta_y y7 y2 y3 y4 y8 y9 < &0)) `;
};;

skip{
  idv = "4240815464 b reduced";
  doc="We can use dimension reduction methods to reduce the number of variables.
  This is the reduced version that occurs when the cross diagonal is minimal.
     See  'Quad convexity justification' comment. ";
  tags = [Cfsqp;Lp_aux "4240815464 b";Tex;Xconvert];
  ineq = all_forall `ineq  [
    (&2,y1,&2 * h0);
    (&2,y2,&2 * h0);
    (&2,y3,&2 * h0);
    (&2,y4,&2 * h0);
    (&2 * h0,y5,sqrt8);
    (&2,y6,&2 * h0)
  ]
( taum y1 y2 y3 y4 y5 y6 + 
   #0.7573 *dih_y y1 y2 y3 y4 y5 y6 - #1.432 / &2 > #0.0)`;
};;

skip{
  idv = "4240815464 front";
  doc="We can use dimension reduction methods to reduce the number of variables.
  This is the reduced version that occurs when the cross diagonal is minimal.
     See  'Quad convexity justification' comment. ";
  tags = [Cfsqp;Lp_aux "4240815464 b";Tex;Xconvert];
  ineq = all_forall `ineq  [
    (&2,y1,&2 * h0);
    (&2,y2,&2 * h0);
    (&2,y3,&2 * h0);
    (&2 * h0,y4,#3.02);
    (&2,y5,&2 * h0);
    (&2,y6,&2 * h0)
  ]
( taum y1 y2 y3 y4 y5 y6 + (#0.101 + #0.12 * (y2 + y3 - &4) ) +
   #0.7573 *dih_y y1 y2 y3 y4 y5 y6 - #1.432 > #0.0)`;
};;

skip{
  idv = "4240815464 back";
  doc="We can use dimension reduction methods to reduce the number of variables.
  This is the reduced version that occurs when the cross diagonal is minimal.
     See  'Quad convexity justification' comment. ";
  tags = [Cfsqp;Lp_aux "4240815464 b";Tex;Xconvert];
  ineq = all_forall `ineq  [
    (&2,y1,&2 * h0);
    (&2,y2,&2 * h0);
    (&2,y3,&2 * h0);
    (&2 * h0,y4,#3.02);
    (&2,y5,&2 * h0);
    (&2,y6,&2 * h0)
  ]
( taum y1 y2 y3 y4 y5 y6  > #0.101 + #0.12 * (y2 + y3 - &4)  )`;
};;



experiment
 {
  idv = "6944699408 b";
  doc="
   Don't use, we were able to get 6944699408 a to run in about 5min without it.
   We can use dimension reduction methods to reduce the number of variables.";
  tags = [Cfsqp;Tablelp;Flypaper["KCBLRQC"];Lp;Xconvert;Tex;Dim_red_backsym;Quad_cluster 0.0005];
  ineq =  all_forall `ineq (dart_std4 y1 y2 y3 y4 y5 y6 y7 y8 y9)
(( tauq y1 y2 y3 y4 y5 y6 y7 y8 y9 + #0.972 * dih_y y1 y2 y3 y4 y5 y6 -  #1.707 > #0.0) \/
   ( enclosed y1 y5 y6 y4 y2 y3 y7 y8 y9 < sqrt8 ) )`;
};;

experiment{
  idv = "6944699408 b reduced";
  doc="   Don't use, we were able to get 6944699408 a to run in about 5min without it.
We can use dimension reduction methods to reduce the number of variables.
  This is the reduced version that occurs when the cross diagonal is minimal.
     See  'Quad convexity justification' comment.
 " ;
  tags = [Cfsqp;Lp_aux  "6944699408 a";Xconvert;Tex];
  ineq =  all_forall `ineq [
    (&2,y1,&2 * h0);
    (&2,y2,&2 * h0);
    (&2,y3,&2 * h0);
    (&2,y4,&2 * h0);
    (&2 * h0,y5,sqrt8);
    (&2,y6,&2 * h0)
  ]
( taum y1 y2 y3 y4 y5 y6 + #0.972 * dih_y y1 y2 y3 y4 y5 y6 -  #1.707 / &2 > #0.0) `;
};;



experiment{
  idv = "6944699408 front";
  doc="   Don't use, we were able to get 6944699408 a to run in about 5min without it.
   We can use dimension reduction methods to reduce the number of variables.
  This is the reduced version that occurs when the cross diagonal is minimal.
     See  'Quad convexity justification' comment.
 " ;
  tags = [Cfsqp;Lp_aux  "6944699408 a";Xconvert;Tex];
  ineq =  all_forall `ineq [
    (&2,y1,&2 * h0);
    (&2,y2,&2 * h0);
    (&2,y3,&2 * h0);
    (&2 * h0,y4,sqrt8);
    (&2,y5,&2 * h0);
    (&2,y6,&2 * h0)
  ]
( taum y1 y2 y3 y4 y5 y6 + ( -- #0.08 * (y4 - #2.52) + #0.15 * (y2 + y3 - &4)) + #0.972 * dih_y y1 y2 y3 y4 y5 y6 -  #1.707 > #0.0) `;
};;

experiment{
  idv = "6944699408 back";
  doc="   Don't use, we were able to get 6944699408 a to run in about 5min without it.
   We can use dimension reduction methods to reduce the number of variables.
  This is the reduced version that occurs when the cross diagonal is minimal.
     See  'Quad convexity justification' comment.
 " ;
  tags = [Cfsqp;Lp_aux  "6944699408 a";Xconvert;Tex];
  ineq =  all_forall `ineq [
    (&2,y1,&2 * h0);
    (&2,y2,&2 * h0);
    (&2,y3,&2 * h0);
    (&2 * h0,y4,sqrt8);
    (&2,y5,&2 * h0);
    (&2,y6,&2 * h0)
  ]
( taum y1 y2 y3 y4 y5 y6 > ( -- #0.08 * (y4 - #2.52) + #0.15 * (y2 + y3 - &4)) )`;
};;


let gamma3f_expand =  new_definition `gamma3f_expand y1 y2 y6 r f = gamma3f y1 y2 y6 r f`;;
let gamma3f_expand_alt = prove_by_refinement `gamma3f_expand y1 y2 y6 r lmfun =
 vol_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - ( XXD)`,
 [
 REWRITE_TAC[gamma3f_expand;Nonlinear_lemma.vol3f_palt;Sphere.gamma3f;Nonlinear_lemma.vol3r_alt];
 ]);;
Nonlinear_lemma.vol3f_palt;;



let all_forall=Sphere.all_forall;;


Parse_ineq.execute_cfsqp
{
  idv="was 5202826650";
  doc="skinny triangle (ear) residual is positive, when y1=2.52, y3=2
   This domain falls within the preconditions of the residual function because of
   4559601669 and 2485876245
    ";
  tags=[Flypaper[];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);
      (&2,y6,&2)
  ]
(
   (y_of_x tau_residual_x y1 y2 y3 y4 y5 y6 > &0) \/
  (delta_y y1 y2 y3 y4 y5 y6 < &0) 
 )`;
};;


Parse_ineq.execute_cfsqp
{
  idv="was 5202826650";
  doc="skinny triangle (ear) residual is positive, when y1=2.52, y3=2
   This domain falls within the preconditions of the residual function because of
   4559601669 and 2485876245
    ";
  tags=[Flypaper[];Main_estimate;Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
  ineq = all_forall `ineq [
    (#2.52,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (#3.5,y4,#3.915);
    (&2,y5,&2);
      (&2,y6,&2)
  ]
(
   (taum y1 y2 y3 y4 y5 y6 > taum (&2) y2 y3 y4 y5 y6) \/
  (delta_y y1 y2 y3 y4 y5 y6 < #0.00001) 
 )`;
};;



Parse_ineq.execute_cfsqp
{
  idv="test ";
  doc="
    ";
  tags=[Flypaper[];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,#4.6);
    (#3.1,y5,#4.6);
      (&2,y6,&2);
	(&2,y12,#2.52)
  ]
(
   (dih_y y1 y2 y3 y4 y5 y6 > &0) \/
   (arclength y2 y3 y4 < #2.42) \/
  (delta_y y1 y2 y12 (&2) (&2) y5 < &0) \/
  (delta_y y1 y2 y3 y4 y5 y6 < #0.00001) 
 )`;
};;


Parse_ineq.execute_cfsqp
{
  idv="test ";
  doc="
    ";
  tags=[Flypaper[];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,#4.6);
      (&2,y6,&2);
      (&2,yh,#2.52)
  ]
(let y5 = edge_flat yh y1 y3     (&2) (&2) in
  (taum y1 y2 y3 y4 y5 y6  + flat_term yh > &0) \/
   (arclength y2 y3 y4 > #2.54) \/
  (dih_y y1 y2 y3 y4 y5 y6 < dih_y y1 yh y2 (#3.01) (&2) (&2)) \/
  (delta_y y1 y2 y3 y4 y5 y6 < #0.00001) 
 )`;
};;



Parse_ineq.execute_cfsqp
{
  idv="test HEX 3 FLATS";
  doc="hexagon with three alternating flats.
    ";
  tags=[Flypaper[];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,y12,#2.52);
      (&2,y23,#2.52);
      (&2,y13,#2.52)
  ]
(let y5 = edge_flat y13 y1 y3     (&2) (&2) in
let y6 = edge_flat y12 y1 y2     (&2) (&2) in
let y4 = edge_flat y23 y2 y3     (&2) (&2) in
  (taum y1 y2 y3 y4 y5 y6  + flat_term y12 + flat_term y23 + flat_term y13 > &0) \/
    ( y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0)
 )`;
};;

Parse_ineq.execute_cfsqp
{
  idv="test HEX 3 FLATS";
  doc="hexagon with three alternating flats.
    Not needed.
    ";
  tags=[Flypaper[];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,y12,#2.52);
      (&2,y23,#2.52);
      (&2,y13,#2.52)
  ]
(let y5 = edge_flat y13 y1 y3     (&2) (&2) in
let y6 = edge_flat y12 y1 y2     (&2) (&2) in
let y4 = edge_flat y23 y2 y3     (&2) (&2) in
  (delta_y y1 y2 y3 y4 y5 y6 > &0) \/
    ( y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0)
 )`;
};;


Parse_ineq.execute_cfsqp
{
idv = "was 298";
doc = "";
tags= [Tex;Cfsqp;Eps 1.0e-8;Penalty(1000.0,10000.0);Flypaper[]];
ineq = all_forall `ineq
 [
    (&1,e1,&1 + sol0/pi);
    (&1,e2,&1 + sol0/pi);
    (&1,e3,&1 + sol0/pi);
    (#2.38 pow 2, a2, #3.7 pow 2);
    (#2.38 pow 2, b2, #3.7 pow 2);
    (#2.38 pow 2, c2, #3.7 pow 2)
 ] (
  (num2 e1 e2 e3 a2 b2 c2 < &0)  \/
 delta_x (&4) (&4) (&4) a2 b2 c2 < &0 \/
 y_of_x eulerA_x (&4) (&4) (&4) a2 b2 c2 < &0 
    )`;
};; 


Parse_ineq.execute_cfsqp
{
idv = "was 298";
doc = "";
tags= [Tex;Cfsqp;Eps 1.0e-8;Penalty(5000.0,50000.0);Flypaper[]];
ineq = all_forall `ineq
 [
   (&2,y1,#2.52);
   (&2,y2,#2.52);
   (&2,y3,#2.52);
   (#3.01,y4,#3.73);
   (#3.01,y5,#3.73);
   (#3.01,y6,#3.73)
 ] (
   let a2 = (&2 * arclength y2 y3 y4) pow 2 in
   let b2 = (&2 * arclength y1 y3 y5) pow 2 in
   let c2 = (&2 * arclength y1 y2 y6) pow 2 in
   let e1 = rho y1 in
   let e2 = rho y2 in
   let e3 = rho y3 in
  (num2 e1 e2 e3 a2 b2 c2 < &0)  \/
 delta_x (&4) (&4) (&4) a2 b2 c2 < &0 \/
 y_of_x eulerA_x (&4) (&4) (&4) a2 b2 c2 < &0 
    )`;
};; 


(* NEW hex SERIES, Jun 2, 2011 *)

(* def's borrowed from sphere.hl *)

let delta_126_x = new_definition 
  `delta_126_x (x3s:real) (x4s:real) (x5s:real) (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = 
     delta_x x1 x2 x3s x4s x5s x6`;;
(* new *)
let delta_234_x = new_definition 
  `delta_234_x (x1s:real) (x5s:real) (x6s:real) (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = 
     delta_x x1s x2 x3 x4 x5s x6s`;;
(* new *)
let delta_135_x = new_definition 
  `delta_135_x (x2s:real) (x4s:real) (x6s:real) (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = 
     delta_x x1 x2s x3 x4s x5 x6s`;;
let taum_sub246_x = new_definition 
 `taum_sub246_x x2s x4s x6s (x1:real) (x2:real) x3 (x4:real) x5 (x6:real) = 
      taum_x x1 x2s x3 x4s x5 x6s`;;
let taum_sub345_x = new_definition 
 `taum_sub345_x x3s x4s x5s (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = 
      taum_x x1 x2 x3s x4s x5s x6`;;
(* new *)
let taum_sub156_x = new_definition 
 `taum_sub156_x x1s x5s x6s (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = 
      taum_x x1s x2 x3 x4 x5s x6s`;;
let taum_3flat_x = new_definition
  `taum_3flat_x x1 x2 x3 x23 x13 x12 = 
let x5 = edge_flat2_x x13 x1 x3 (&0)    (&4) (&4) in
let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
let x4 = edge_flat2_x x23 x2 x3 (&0)    (&4) (&4) in
  (taum_x x1 x2 x3 x4 x5 x6  + flat_term_x x12 + flat_term_x x23 + flat_term_x x13)`;;
let taum_2flat_x = new_definition
  `taum_2flat_x x1 x2 x3 x4 x13 x12 = 
let x5 = edge_flat2_x x13 x1 x3 (&0)    (&4) (&4) in
let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
  (taum_x x1 x2 x3 x4 x5 x6  + flat_term_x x12 +  flat_term_x x13)`;;

let taum_1flat_x = new_definition
  `taum_1flat_x x1 x2 x3 x4 x5 x12 = 
let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
  (taum_x x1 x2 x3 x4 x5 x6  + flat_term_x x12)`;;

let euler_3flat_x = new_definition
  `euler_3flat_x x1 x2 x3 x23 x13 x12 = 
let x5 = edge_flat2_x x13 x1 x3 (&0)    (&4) (&4) in
let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
let x4 = edge_flat2_x x23 x2 x3 (&0)    (&4) (&4) in
  (eulerA_x x1 x2 x3 x4 x5 x6)`;;
let euler_2flat_x = new_definition
"  `euler_2flat_x x1 x2 x3 x4 x13 x12 =" 
let x5 = edge_flat2_x x13 x1 x3 (&0)    (&4) (&4) in
let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
  (eulerA_x x1 x2 x3 x4 x5 x6)`;;
let euler_1flat_x = new_definition
  `euler_1flat_x x1 x2 x3 x4 x5 x12 = 
let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
  (eulerA_x x1 x2 x3 x4 x5 x6)`;;

Parse_ineq.execute_cfsqp
{
  idv="5338748573";
  doc="full hexagon with three alternating flats.
    Big alternating central triangle.
    ";
  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,y12,#2.52);
      (&2,y23,#2.52);
      (&2,y13,#2.52)
  ]
(
  (y_of_x taum_3flat_x y1 y2 y3 y23 y13 y12 > #0.712 ) \/
    (y_of_x euler_3flat_x y1 y2 y3 y23 y13 y12 < &0)
 )`;
};;

Parse_ineq.execute_cfsqp
{
  idv="3306409086";
  doc="full hexagon with two flats, one hi, can zero out the hi ear.
    Big alternating central triangle.
    ";
  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,y12,#2.52);
      (&2,y13,#2.52)
  ]
(
  (y_of_x taum_2flat_x y1 y2 y3 y4 y13 y12
    > #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 y13 y12<  &0) 
 )`;
};;

Parse_ineq.execute_cfsqp
{
  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.
    ";
  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,y12,#2.52);
      (&2,y13,#2.52)
  ]
(
  (y_of_x taum_2flat_x y1 y2 y3 y4 y13 y12
   > #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 y13 y12<  &0) 
 )`;
};;

Parse_ineq.execute_cfsqp
{
  idv="1324821088";
  doc="full hexagon with one flat, hi,hi, can zero out both ears.
    Big alternating central triangle.
    ";
  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,y12,#2.52)
  ]
(
  (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y12  > #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  \/
     ( y_of_x euler_1flat_x y1 y2 y3 y4 y5 y12< &0) 
 )`;
};;

Parse_ineq.execute_cfsqp
{
  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.
    ";
  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,y12,#2.52)
  ]
(
  (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y12 +
 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 y12  > #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 y12< &0) 
 )`;
};;

Parse_ineq.execute_cfsqp
{
  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,y12,#2.52)
  ]
(
  (y_of_x taum_1flat_x y1 y2 y3 y4 y5 y12 +
      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 y12
   > #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 y12< &0) 
 )`;
};;


Parse_ineq.execute_cfsqp
{
  idv="5493250206";
  doc="full hexagon with no flats, three ears: hi,hi,hi, can zero out all ears.
    Big alternating central triangle.
    ";
  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) 
 )`;
};;

Parse_ineq.execute_cfsqp
{
  idv="2283016857";
  doc="full hexagon with no flats, three ears: hi,hi,lo, 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.
    ";
  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) 
 )`;
};;

Parse_ineq.execute_cfsqp
{
  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) 
 )`;
};;

Parse_ineq.execute_cfsqp
{
  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) 
 )`;
};;

Parse_ineq.execute_cfsqp
{
  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).
    ";
  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) \/
    (delta_y (#2.52) y2 y3 y4 y5 y6 < &0) \/
    (delta_y y1 y2 y3 y4 y5 y6 < &0) 
 )`;
};;


(*  PENTAGONS, June reprise *)