legacy/oldnonlinear/nonlinear/test_may2013_terminal_pent_hex_series.hl

   1
   2 (* DEPRECATED:
   3    let taud = new_definition `taud y1 y2 y3 y4 y5 y6 =
   4       #0.027 * safesqrt(delta_y y1 y2 y3 y4 y5 y6) + sol0 * (y1 - &2 * h0)/(&2 * h0 - &2)`;;
   5
   6     let taud_v2 = new_definition `taud_v2 y1 y2 y3 y4 y5 y6 =
   7       #0.027 * safesqrt(delta_y y1 y2 y3 y4 y5 y6) + sol0 * (y1 - &2 * h0)/(&2 * h0 - &2) +
   8         safesqrt(delta_y y1 y2 y3 y4 y5 y6) * #0.04 * (#2.52 - y1)`;;
   9
  10     let taud_v3 = new_definition `taud_v3 y1 y2 y3 y4 y5 y6 =
  11       #0.023 * safesqrt(delta_y y1 y2 y3 y4 y5 y6) + sol0 * (y1 - &2 * h0)/(&2 * h0 - &2) +
  12         safesqrt(delta_y y1 y2 y3 y4 y5 y6) * #0.055 * (#2.52 - y1)`;;
  13
  14     let edge_flat50 =  new_definition`edge_flat50 y1 y2 y3 y5 y6 =
  15       sqrt(quadratic_root_plus (abc_of_quadratic (
  16         \x4.  &50 - delta_x (y1*y1) (y2*y2)  (y3*y3)  x4 (y5*y5)  (y6*y6))))`;;
  17
  18     let edge_flat250_x = new_definition `edge_flat250_x x1 x2 x3 x4 x5 x6 =
  19       (edge_flat (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x5) (sqrt x6)) pow 2`;;  (* x4 dummy *)
  20
  21     let edge_flat50_x =  new_definition`edge_flat50_x x1 x2 x3 (x4:real) x5 x6 =
  22       edge_flat (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x5) (sqrt x6)`;;
  23
  24
  25     let fn_sub246 = new_definition
  26       `fn_sub246 f (x2s:real) (x4s:real) (x6s:real)
  27       (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
  28       (f x1 x2s x3 x4s x5 x6s):real`;;
  29
  30     let fn_sub345 = new_definition
  31       `fn_sub345 f (x3s:real) (x4s:real) (x5s:real)
  32       (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
  33       (f x1 x2 x3s x4s x5s x6):real`;;
  34
  35     let edge_flatD_x1 = new_definition `edge_flatD_x1 d x2 x3 x4 x5 x6 =
  36       sqrt(quadratic_root_plus (abc_of_quadratic (
  37         \x1.  d - delta_x x1 x2 x3 x4 x5 x6)))`;;
  38
  39     let edge_126_x = new_definition `edge_126_x d x4 x5 =
  40       compose6 (edge_flatD_x1) (constant6 d) proj_x1 proj_x2 proj_x6 (constant6 x4) (constant6 x5)`;;
  41
  42     let edge_135_x = new_definition `edge_135_x d x4 x6 =
  43       compose6 (edge_flatD_x1) (constant6 d) proj_x1 proj_x3 proj_x5 (constant6 x4) (constant6 x6)`;;
  44
  45     let flat_term_126_x = new_definition `flat_term_126_x d x4 x5 =
  46       uni(flat_term,edge_126_x d x4 x5)`;;
  47
  48     let flat_term_135_x = new_definition `flat_term_135_x d x4 x6 =
  49       uni(flat_term,edge_135_x d x4 x6)`;;
  50
  51     let mudd_135_x_v2 = new_definition `mudd_135_x_v2 d x4 x6 =
  52       mul6 (compose6 (promote3_to_6 mu_y) (uni(sqrt,edge2_135_x d x4 x6)) proj_y1 proj_y3 dummy6 dummy6 dummy6)
  53         (constant6 (sqrt d))`;;
  54
  55     let mudd_126_x_v2 = new_definition `mudd_126_x_v2 d x4 x5 =
  56       mul6 (compose6 (promote3_to_6 mu_y) (uni(sqrt,edge2_126_x d x4 x5)) proj_y1 proj_y2 dummy6 dummy6 dummy6)
  57         (constant6 (sqrt d))`;;
  58
  59     let mudt_234_x = new_definition `mudt_234_x d y1 y5 y6 =
  60       (mul6 (compose6 (mu6_x) (constant6 (y1*y1)) proj_x2 proj_x3 dummy6 dummy6 dummy6)
  61         (uni(truncate_sqrt d,(delta_234_x (y1*y1) (y5*y5) (y6*y6)))))`;;
  62
  63     let mudL_234_x = new_definition `mudL_234_x d1 d2 y1 y5 y6 =
  64       (mul6 (compose6 (mu6_x) (constant6 (y1*y1)) proj_x2 proj_x3 dummy6 dummy6 dummy6)
  65         (constant6 (&1/ (sqrt(d1)+sqrt(d2))) * (delta_234_x (y1*y1) (y5*y5) (y6*y6)) + constant6(sqrt(d1))))`;;
  66
  67
  68
  69 *)
  70
  71
  72
  73
  74 add
  75 {
  76   idv="test4";
  77   doc="tau_residual";
  78   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
  79   ineq = all_forall `ineq [
  80     (&2,y1,#2.52);
  81     (&2,y2,#2.52);
  82     (&2,y3,#2.52);
  83     (#3.01,y4,#3.915);
  84     (&2,y5,&2);
  85       (&2,y6,&2)
  86   ]
  87 (
  88    (y_of_x tau_residual_x y1 y2 y3 y4 y5 y6 > #0.027 + #0.04 * (#2.52 - y1)) \/
  89   (delta_y y1 y2 y3 y4 y5 y6 < &0)
  90  )`;
  91 };;
  92
  93
  94 add
  95 {
  96   idv="test25353";
  97   doc="full hexagon ear calculation.
  98    This shows that if (delta hi > 0) and (delta lo >0) we can erase the ear with small penalty.
  99    Hence, when we look at a lo ear, we can wrap it in with the hi ear case when
 100    the hi ear exists: (delta hi>0).
 101    By symmetry, wlog y2 < y3.
 102     ";
 103   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 104   ineq = all_forall `ineq [
 105     (&2,y1,&2);
 106     (&2,y2,#2.52);
 107     (&2,y3,#2.52);
 108     (#3.01,y4,#3.915);
 109     (&2,y5,&2);
 110     (&2,y6,&2)
 111   ]
 112 (
 113  (taud_v2 y1 y2 y3 y4 y5 y6   > -- #0.013) \/
 114     (y_of_x (delta_sub1_x (#2.52 pow 2)) y1 y2 y3 y4 y5 y6 < &0) \/
 115     (delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y3 < y2)
 116  )`;
 117 };;
 118 add
 119 {
 120   idv="taud";
 121   doc="";
 122   tags=[Cfsqp;Xconvert];
 123   ineq = all_forall `ineq [
 124       (&2,y1,#2.52);
 125       (&2,y2,#2.52);
 126       (&2,y3,#2.52);
 127       (#3.01,y4,#3.915);
 128       (&2,y5,&2);
 129       (&2,y6,&2)]
 130 ((taum y1 y2 y3 y4 y5 y6    > taud y1 y2 y3 y4 y5 y6
 131    + safesqrt(delta_y y1 y2 y3 y4 y5 y6) * #0.04 * (#2.52 - y1)) \/ (delta_y y1 y2 y3 y4 y5 y6 < &20))`;
 132 };;
 133
 134
 135 add
 136 {
 137   idv="local max";
 138   doc="test";
 139   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 140   ineq = all_forall `ineq [
 141     (#3.01,y1,#3.915);
 142     (&2,y2,#2.52);
 143     (&2,y3,#2.52);
 144     (&2,y4,#2.52);
 145     (&2,y5,#2.52);
 146     (&2,y6,#2.52)
 147   ]
 148     (let delta' = delta4_y y1 y2 y3 y4 y5 y6 * (&2 * y4) in
 149      let d = delta_y y1 y2 y3 y4 y5 y6 in
 150      let delta'' = -- &8 * (y1 * y4) pow 2 + delta4_y y1 y2 y3 y4 y5 y6 * (&2) in
 151      let mu = #0.1278 - #0.04 * y4 in
 152      let mu' = -- #0.04 in
 153      let h' = sol0 / (&2 * h0 - &2) in
 154 (
 155   #1.0 < (&2 * mu' * d + mu * delta' + h' * &2 * safesqrt(d)) pow 2 \/
 156   delta_y y1 y2 y3 y4 y5 y6 < &0 \/
 157     mu' * d * delta' - (&1 / &4) * mu * (delta' pow 2) + (&1 / &2) * mu * d * delta'' < -- #1.0
 158 ))`;
 159 };;
 160
 161
 162
 163 add
 164 {
 165   idv="local max2";
 166   doc="better local max test";
 167   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 168   ineq = all_forall `ineq [
 169     (#3.01,y1,#3.915);
 170     (&2,y2,#2.52);
 171     (&2,y3,#2.52);
 172     (&2,y4,#2.52);
 173     (&2,y5,#2.52);
 174     (&2,y6,#2.52)
 175   ]
 176     (let d = delta_y y1 y2 y3 y4 y5 y6 in
 177      let delta' = delta4_y y1 y2 y3 y4 y5 y6 * (&2 * y4) in
 178      let delta'' = -- &8 * (y1 * y4) pow 2  + delta4_y y1 y2 y3 y4 y5 y6 * (&2) in
 179      let mu = #0.1278 - #0.04 * y4 in
 180      let mu' = -- #0.04 in
 181 (
 182     mu' * d * delta' - (&1 / &4) * mu * (delta' pow 2) + (&1 / &2) * mu * d * delta'' < &0 \/
 183   delta_y y1 y2 y3 y4 y5 y6 < &0
 184 ))`;
 185 };;
 186
 187 add
 188 {
 189   idv="local max debug";
 190   doc="local max numerical debug";
 191   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 192   ineq = all_forall `ineq [
 193     (#2.1,y1,#2.1);
 194     (#2.2,y2,#2.2);
 195     (#2.3,y3,#2.3);
 196     (#2.4,y4,#2.4);
 197     (#2.5,y5,#2.5);
 198     (#2.6,y6,#2.6)
 199   ]
 200     (let d = delta_y y1 y2 y3 y4 y5 y6 in
 201      let delta' = delta4_y y1 y2 y3 y4 y5 y6 * (&2 * y4) in
 202      let delta'' = -- &8 * (y1 * y4) pow 2  + delta4_y y1 y2 y3 y4 y5 y6 * (&2) in
 203      let mu = #0.1278 - #0.04 * y4 in
 204      let mu' = -- #0.04 in
 205 (
 206     (mu' * d * delta' - (&1 / &4) * mu * (delta' pow 2) + (&1 / &2) * mu * d * delta'')
 207       / (d * safesqrt(d)) > &0
 208 ))`;
 209 };;
 210 add
 211 {
 212   idv="5556646409 small domain";
 213   doc="taum 2nd deriv test.
 214    ";
 215   tags=[Tex;Disallow_derivatives;Widthcutoff 0.004;Penalty(1500.0,5000.0);Cfsqp_branch 2];
 216   ineq = all_forall `ineq [
 217     (&2,y1,#2.52);
 218     (#2.0,y2,#2.52);
 219     (&2,y3,#2.52);
 220     (#3.01,y4,#3.237);
 221     (&2,y5,&2);
 222       (&2,y6,&2)
 223   ]
 224 (
 225   (delta_y_LC y1 y2 y3 y4 y5 y6 < &15) \/
 226  (y2 < y3) \/
 227   (mdtau_y_LC  y1 y2 y3 y4 y5 y6  > &0) \/
 228   (mdtau_y_LC  y1 y2 y3 y4 y5 y6  < &0) \/
 229   (mdtau2uf_y_LC y1 y2 y3 y4 y5 y6 < &0)
 230  )`;
 231 };;
 232 add
 233 {
 234   idv="taud pent";
 235   doc="test";
 236   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 237   ineq = all_forall `ineq [
 238     (&2,y1,#2.52);
 239     (&2,y2,#2.52);
 240     (&2,y3,#2.52);
 241     (&2,y4,#2.52);
 242     (&2,y5,#2.52);
 243     (#3.01,z2,#3.237);
 244     (#3.01,z5,#3.237)
 245   ]
 246 (  (taum y1 y3 y4 (&2) z5 z2 +
 247       taud_v3 y2 y3 y1 z2 (&2) (&2) +
 248       taud_v3 y5 y4 y1 z5 (&2) (&2)
 249 > #0.616) \/
 250      delta_y y1 y3 y4 (&2) z5 z2 < &0 \/
 251      delta_y y2 y3 y1 z2 (&2) (&2) < &0 \/
 252       delta_y y5 y4 y1 z5 (&2) (&2) < &0 \/
 253    (dih_y y1 y3 y4 (&2) z5 z2 +
 254       dih_y y1 y3 y2 (&2) (&2) (z2) +
 255       dih_y y1 y4 y5 (&2) (&2) (z5) < #1.75)
 256 )`;
 257 };;
 258 add
 259 {
 260   idv="taum pent";
 261   doc="test";
 262   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 263   ineq = all_forall `ineq [
 264     (&2,y1,#2.52);
 265     (&2,y2,#2.52);
 266     (&2,y3,#2.52);
 267     (&2,y4,#2.52);
 268     (&2,y5,#2.52);
 269     (#3.01,z2,#3.237);
 270     (#3.01,z5,#3.237)
 271   ]
 272 (  (taum y1 y3 y4 (&2) z5 z2 +
 273       taum y2 y3 y1 z2 (&2) (&2) +
 274       taum y5 y4 y1 z5 (&2) (&2)
 275 > #0.616) \/
 276      delta_y y1 y3 y4 (&2) z5 z2 < &0 \/
 277      delta_y y2 y3 y1 z2 (&2) (&2) < &0 \/
 278       delta_y y5 y4 y1 z5 (&2) (&2) < &0 \/
 279    (dih_y y1 y3 y4 (&2) z5 z2 +
 280       dih_y y1 y3 y2 (&2) (&2) (z2) +
 281       dih_y y1 y4 y5 (&2) (&2) (z5) < #1.75)
 282 )`;
 283 };;
 284 add
 285 {
 286   idv="taum pent2";
 287   doc="test";
 288   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 289   ineq = all_forall `ineq [
 290     (&2,y1,#2.52);
 291     (&2,y2,#2.52);
 292     (&2,y3,#2.52);
 293     (&2,y4,#2.52);
 294     (&2,y5,#2.52);
 295     (#3.01,z2,#3.237);
 296     (#3.01,z5,#3.237)
 297   ]
 298 (  (taum y1 y3 y4 (&2) z5 z2 +
 299       taud_v2 y2 y3 y1 z2 (&2) (&2) +
 300       taud_v2 y5 y4 y1 z5 (&2) (&2)
 301  > #0.616) \/
 302      delta_y y1 y3 y4 (&2) z5 z2 < &0 \/
 303      delta_y y2 y3 y1 z2 (&2) (&2) < &0 \/
 304       delta_y y5 y4 y1 z5 (&2) (&2) < &0 \/
 305       // extra delta constraints
 306      delta_y y2 y3 y1 z2 (&2) (&2) > &50 \/
 307       delta_y y5 y4 y1 z5 (&2) (&2) > &50 \/
 308    (dih_y y1 y3 y4 (&2) z5 z2 +
 309       dih_y y1 y3 y2 (&2) (&2) (z2) +
 310       dih_y y1 y4 y5 (&2) (&2) (z5) < #1.75)
 311 )`;
 312 };;
 313
 314 add
 315 {
 316   idv="test5";
 317   doc="tau_residual pent";
 318   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 319   ineq = all_forall `ineq [
 320     (&2,y1,#2.52);
 321     (&2,y2,#2.52);
 322     (&2,y3,#2.52);
 323     (#3.01,y4,#3.237);
 324     (&2,y5,&2);
 325       (&2,y6,&2)
 326   ]
 327 (
 328    (y_of_x tau_residual_x y1 y2 y3 y4 y5 y6 > #0.023 + #0.055 * (#2.52 - y1) ) \/
 329   (delta_y y1 y2 y3 y4 y5 y6 < &0)
 330  )`;
 331 };;
 332
 333 add
 334 {
 335   idv="test6";
 336   doc="tau_residual pent";
 337   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 338   ineq = all_forall `ineq [
 339     (&2,y1,#2.52);
 340     (&2,y2,#2.1);
 341     (&2,y3,#2.52);
 342     (#3.01,y4,#3.237);
 343     (&2,y5,&2);
 344       (&2,y6,&2)
 345   ]
 346 (
 347    (y_of_x tau_residual_x y1 y2 y3 y4 y5 y6 > #0.018 + #0.07 * (#2.52 - y1) ) \/
 348   (delta_y y1 y2 y3 y4 y5 y6 < &0)
 349  )`;
 350 };;
 351
 352 add
 353 {
 354   idv="test7";
 355   doc="taum for small delta";
 356   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 357   ineq = all_forall `ineq [
 358     (&2,y1,#2.52);
 359     (&2,y2,#2.52);
 360     (&2,y3,#2.52);
 361     (#3.01,y4,#3.237);
 362     (&2,y5,&2);
 363       (&2,y6,&2)
 364   ]
 365 (
 366    (taum y1 y2 y3 y4 y5 y6 > &0) \/
 367   (delta_y y1 y2 y3 y4 y5 y6 < &0) \/
 368   (delta_y y1 y2 y3 y4 y5 y6 > &50)
 369  )`;
 370 };;
 371
 372 add
 373 {
 374   idv="test8";
 375   doc="taum for small delta";
 376   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 377   ineq = Sphere.all_forall `ineq [
 378     (&2,y1,#2.52);
 379     (&2,y2,#2.52);
 380     (&2,y3,#2.52);
 381     (&2,y4,&2);
 382       (&2,y5,&2);
 383     (#3.01,y6,#3.237)
 384   ]
 385 (
 386   (delta_y y1 y2 y3 y4 y5 y6 > &0) \/
 387      (dih_y y1 y2 y3 y4 y5 y6 < #0.096) \/
 388   (delta_y y1 y2 y3 y4 y5 y6 < &0)
 389  )`;
 390 };;
 391
 392 add
 393 {
 394   idv="4184277422";
 395   doc="old name: test10*.";
 396   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 397   ineq = all_forall `ineq [
 398     (&2,y1,#2.52);
 399     (&2,y2,#2.52);
 400     (&2,y3,#2.52);
 401     (&2,y4,#2.52);
 402     (&2,y5,#2.52);
 403     (#3.01,z2,#3.237);
 404     (#3.01,z5,#3.237)
 405   ]
 406 (  (taum y1 y3 y4 (&2) z5 z2 +
 407       taud_v4 y2 y3 y1 z2 (&2) (&2) +
 408        taud_v4 y5 y4 y1 z5 (&2) (&2)
 409 > #0.616) \/
 410  //    delta_y y1 y3 y4 (&2) z5 z2 < &0 \/
 411      delta_y y2 y3 y1 z2 (&2) (&2) < &0 \/
 412      delta_y y2 y3 y1 z2 (&2) (&2) > &20 \/
 413       delta_y y5 y4 y1 z5 (&2) (&2) < &20
 414 )`;
 415 };;
 416
 417 run
 418 {
 419   idv="test p";
 420   doc="taum for small delta";
 421   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 422   ineq = Sphere.all_forall `ineq [
 423     (&2,y1,#2.52);
 424     (#2.1,y2,#2.52);
 425     (&2,y3,#2.52);
 426     (#3.01,y4,#3.24);
 427       (&2,y5,&2);
 428     (&2,y6,&2)
 429   ]
 430 (
 431      (taum y1 y2 y3 y4 y5 y6 > #0.04) \/
 432   (delta_y y1 y2 y3 y4 y5 y6 < &10)
 433  )`;
 434 };;
 435
 436
 437 skip
 438 {
 439   idv="1671775772";
 440   doc="old name: local max v4*, WNLKGOQ
 441     better local max test.
 442     This is the numerator of the 2nd derivative of the function taud.
 443     Case delta > 20.";
 444   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
 445   ineq = all_forall `ineq [
 446     (&2,y1,#2.52);
 447     (&2,y2,#2.52);
 448     (&2,y3,#2.52);
 449     (#3.01,y4,#3.237);
 450     (&2,y5,&2);
 451     (&2,y6,&2)
 452   ]
 453     (y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6  > &0 \/
 454     y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6  < &0 \/
 455     y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
 456        taum y1 y2 y3 y4 y5 y6 > #0.1 \/
 457   delta_y y1 y2 y3 y4 y5 y6 < &20)`;
 458 };;
 459
 460 skip
 461 {
 462   idv="7099408714";
 463   doc="old name: local max v4*
 464     better local max test.
 465     This is the numerator of the 2nd derivative of the function taud.
 466      Old False version.";
 467   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
 468   ineq = all_forall `ineq [
 469     (&2,y1,#2.52);
 470     (&2,y2,#2.52);
 471     (&2,y3,#2.52);
 472     (#3.01,y4,#3.915);
 473     (&2,y5,&2);
 474     (&2,y6,&2)
 475   ]
 476     (y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
 477   delta_y y1 y2 y3 y4 y5 y6 < &0)`;
 478 };;
 479
 480
 481 skip
 482 {
 483   idv="2320951108";
 484   doc="
 485     local fan/main estimate/terminal pent
 486     LHS(135,y1=2) RHS(126,y1=2.52), extra implicit assumption delta > 20.
 487     mu sqrt(delta) >= 0.012 sqrt(&20) > 0.053.
 488     ";
 489   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
 490   ineq = all_forall `ineq [
 491     (&2,y1,#2.52);
 492     (&2,y2,#2.52);
 493     (&2,y3,#2.52);
 494     (&2,y4,&2);
 495     (#3.01,y5,#3.237);
 496     (#3.01,y6,#3.237)
 497   ]
 498 (
 499     (taum y1 y2 y3 y4 y5 y6 +
 500        y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0
 501        + #0.053
 502      > #0.616)
 503 )
 504 `;
 505 };;
 506
 507
 508
 509
 510
 511 add
 512 {
 513   idv="test";
 514   doc="
 515     local fan/main estimate/terminal pent
 516     LHS(135,y1=2.52) RHS(126,y1=2.52)
 517     wlog. LHS delta on ears is >= 20,
 518     mu sqrt(delta) >= 0.012 sqrt(&20) > 0.053.
 519     If RHS delta >= 20.  get 0.541 + 2 (0.053) > 0.616.
 520     so wlog. RHS delta on ear is <= 20.
 521     ";
 522   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
 523   ineq = all_forall `ineq [
 524     (&2,y1,#2.52);
 525     (&2,y2,#2.52);
 526     (&2,y3,#2.52);
 527     (&2,y4,&2);
 528     (#3.01,y5,#3.237);
 529     (#3.01,y6,#3.237)
 530   ]
 531 (
 532   let d = &20 in
 533     ((taum y1 y2 y3 y4 y5 y6 +
 534         #0.053
 535      > #0.616) \/
 536       y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > d ))
 537 `;
 538 };;
 539
 540
 541 skip
 542 {
 543   idv="9115820315";
 544   doc="old name: test9* test10*
 545     full terminal pentagon test, using taud on ears.
 546     assuming delta > 20 at y5.";
 547   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 548   ineq = all_forall `ineq [
 549     (&2,y1,#2.52);
 550     (&2,y2,#2.52);
 551     (&2,y3,#2.52);
 552     (&2,y4,#2.52);
 553 //    (&2,y5,#2.52);
 554     (#3.01,z2,#3.237);
 555     (#3.01,z5,#3.237)
 556   ]
 557 (  (taum y1 y3 y4 (&2) z5 z2
 558     + #0.12 +
 559      taud y2 y3 y1 z2 (&2) (&2) // + // test
 560     //  &0 * taud y5 y4 y1 z5 (&2) (&2)
 561 > #0.616) \/
 562 // \/
 563 //     delta_y y1 y3 y4 (&2) z5 z2 < &0 \/
 564      delta_y y2 y3 y1 z2 (&2) (&2) < &0 // \/
 565 //      delta_y y5 y4 y1 z5 (&2) (&2) < &20
 566 )`;
 567 };;
 568
 569 skip
 570 {
 571   idv="test";
 572   doc="pent hi(126-345) hi(135-234)
 573     full terminal pentagon test, using taud on ears.
 574     assuming delta > 20 both sides.";
 575   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 576   ineq = all_forall `ineq [
 577     (&2,y1,#2.52);
 578     (&2,y2,#2.52);
 579     (&2,y3,#2.52);
 580     (&2,y4,&2);
 581     (#3.01,y5,#3.237);
 582     (#3.01,y6,#3.237)
 583   ]
 584 (
 585     (taum y1 y2 y3 y4 y5 y6 +
 586        y_of_x (mud_126_x_v1 (&2 * h0) (&2) (&2)) y1 y2 y3 y4 y5 y6 +
 587        y_of_x (flat_term2_126_x (&2 * h0) (&2) (&2)) y1 y2 y3 y4 y5 y6 +
 588        y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 +
 589        y_of_x (flat_term2_126_x (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6
 590      > #0.616) \/
 591       y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &20 \/
 592       y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &20 )
 593 `;
 594 };;
 595
 596 add
 597 {
 598   idv="test R";
 599   doc="
 600     ";
 601   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 602   ineq = all_forall `ineq [
 603     (&2,y1,&2);
 604     (&2,y2,#2.52);
 605     (&2,y3,#2.52);
 606     (#3.01,y4,#3.237);
 607     (&2,y5,&2);
 608     (&2,y6,&2)
 609   ]
 610 (
 611   y4 > &2 \/
 612     delta_y y1 y2 y3 y4 y5 y6 > &20)
 613 `;
 614 };;
 615
 616 (* HEX CASES *)
 617
 618 let template_hex_ear = `\ y2m y2M y3m y3M y4m y4M d. ineq
 619    [
 620     (#2.0,y1,#2.52);
 621     (y2m,y2,y2M);
 622     (y3m,y3,y3M);
 623     (y4m,y4,y4M);
 624     (&2,y5,&2);
 625       (&2,y6,&2)
 626    ]
 627     (taud y1 y2 y3 y4 y5 y6 > d \/
 628     delta_y y1 y2 y3 y4 y5 y6 < &0)`;;
 629
 630 let mk_ineq_hex_ear i2 i3 i4 d =
 631   let x i = List.nth [`&2`;`#2.17`;`#2.34`;`#2.52`] i in
 632   let X i = x (i+1) in
 633   let y i = List.nth [`#3.01`;`#3.25`;`#3.5`;`#3.75`;`#3.915`] i in
 634   let Y i = y (i+1) in
 635  Ineq.mk_tplate template_hex [x i2;X i2; x i3;X i3; y i4;Y i4;d];;
 636
 637 let make_hex_ear i2 i3 i4 d =
 638    {
 639     idv = Printf.sprintf "test %d %d %d" i2 i3 i4;
 640     ineq = mk_ineq_hex i2 i3 i4 d;
 641     doc = "local fan/main estimate/terminal hex/ear.";
 642     tags=[Cfsqp;Xconvert;Penalty(50.0,500.0)];
 643   };;
 644
 645
 646 let runh (i2,i3,i4,d) = try (run(make_hex_ear i2 i3 i4 d)) with _ -> () ;;
 647
 648 (*
 649 for i2=0 to 2 do
 650   for i3 = 0 to 2 do
 651     for i4 = 0 to 3 do
 652       runh (i2,i3,i4,`&0`) done done done;;
 653 *)
 654
 655 map runh ;;
 656
 657 let hex_ears =  [
 658 (0,0,0,Some `-- #0.2`);
 659 (0,0,1,Some `-- #0.552`);
 660 (0,0,2,Some `-- #0.552`);
 661 (0,0,3,None);
 662 (0,1,0,Some `-- #0.05`);
 663 (0,1,1,Some `-- #0.443`);
 664 (0,1,2,Some `-- #0.552`);
 665 (0,1,3,None);
 666 (0,2,0,Some `#0.04`);
 667 (0,2,1,Some `-- #0.29`);
 668 (0,2,2,Some `-- #0.552`);
 669 (0,2,3,Some `-- #0.552`);
 670 (1,0,0,Some `-- #0.05`);
 671 (1,0,1,Some `-- #0.45`);
 672 (1,0,2,Some `-- #0.552`);
 673 (1,0,3,None);
 674 (1,1,0,Some `#0.04`);
 675 (1,1,1,Some `-- #0.29`);
 676 (1,1,2,Some ` -- #0.552`);
 677 (1,1,3,Some ` -- #0.552`);
 678 (1,2,0,Some `#0.08`);
 679 (1,2,1,Some `-- #0.14`);
 680 (1,2,2,Some `-- #0.552`);
 681 (1,2,3,Some `-- #0.552`);
 682 (2,0,0,Some ` #0.04`);
 683 (2,0,1,Some `-- #0.29`);
 684 (2,0,2,Some `-- #0.552`);
 685 (2,0,3,Some `-- #0.552`);
 686 (2,1,0,Some `#0.08`);
 687 (2,1,1,Some `-- #0.14`);
 688 (2,1,2,Some `-- #0.552`);
 689 (2,1,3,Some `-- #0.552`);
 690 (2,2,0,Some `#0.11`);
 691 (2,2,1,Some `-- #0.017`);
 692 (2,2,2,Some `-- #0.45`);
 693 (2,2,3,Some `-- #0.552`);
 694 ];;
 695
 696 let reformat_ear =
 697   let f (i,j,k,d) = ((i,j,k),d) in
 698     map f hex_ears;;
 699
 700 let template_hex = `\ y1m y1M y2m y2M y3m y3M y4m y4M y5m y5M y6m y6M d1 d2 d3. ineq
 701    [
 702     (y1m,y1,y1M);
 703     (y2m,y2,y2M);
 704     (y3m,y3,y3M);
 705     (y4m,y4,y4M);
 706     (y5m,y5,y5M);
 707       (y6m,y6,y6M)
 708    ]
 709     (taum y1 y2 y3 y4 y5 y6 + d1 + d2 + d3 > #0.712  \/
 710       y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0)`;;
 711
 712 let mk_ineq_hex i1 i2 i3 i4 i5 i6 d126 d234 d135 =
 713   let x i = List.nth [`&2`;`#2.17`;`#2.34`;`#2.52`] i in
 714   let X i = x (i+1) in
 715   let y i = List.nth [`#3.01`;`#3.25`;`#3.5`;`#3.75`;`#3.915`] i in
 716   let Y i = y (i+1) in
 717  Ineq.mk_tplate template_hex [x i1 ; X i1;x i2;X i2; x i3;X i3; y i4;Y i4;y i5;Y i5;y i6;Y i6;d126;d234;d135];;
 718
 719 let make_hex_ear i1 i2 i3 i4 i5 i6  =
 720   let d126 = assoc (i1,i2,i6) reformat_ear in
 721   let d135 = assoc (i1,i3,i5) reformat_ear in
 722   let d234 = assoc (i2,i3,i4) reformat_ear in
 723   let desome = function
 724     | Some x -> x
 725     | None -> failwith "none" in
 726   let (d126',d135',d234') = (desome d126,desome d135,desome d234) in
 727    {
 728     idv = Printf.sprintf "test %d %d %d %d %d %d" i1 i2 i3 i4 i5 i6;
 729     ineq = mk_ineq_hex i1 i2 i3 i4 i5 i6 d126' d135' d234';
 730     doc = "local fan/main estimate/terminal hex/body";
 731     tags=[Cfsqp;Xconvert;Penalty(50.0,500.0)];
 732   };;
 733
 734 let runhh (i1,i2,i3,i4,i5,i6) = try (run(make_hex_ear i1 i2 i3 i4 i5 i6)) with _ -> () ;;
 735
 736 runhh(1,1,0,0,0,3);;
 737
 738 (* MANY NEGATIVE!
 739 for i1=0 to 2 do
 740 for i2=0 to 2 do
 741   for i3 = 0 to 2 do
 742     for i4 = 0 to 3 do
 743     for i5 = i4 to 3 do
 744     for i6 = i5 to 3 do
 745       runhh (i1,i2,i3,i4,i5,i6) done done done done done done;;
 746 *)
 747
 748 skip
 749 {
 750   idv="test";
 751   doc="local fan/main estimate/appendix/terminal hex.
 752    full hexagon ear calculation.
 753    This shows that if (delta hi > 0) and (delta lo >0) we can erase the ear with small penalty.
 754    Hence, when we look at a lo ear, we can wrap it in with the hi ear case when
 755    the hi ear exists: (delta hi>0).
 756    By symmetry, wlog y2 < y3.
 757     ";
 758   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 759   ineq = all_forall `ineq [
 760     (&2,y1,&2);
 761     (&2,y2,#2.52);
 762     (&2,y3,#2.52);
 763     (#3.01,y4,#3.915);
 764     (&2,y5,&2);
 765     (&2,y6,&2)
 766   ]
 767 (
 768  (taud y1 y2 y3 y4 y5 y6   > -- #0.07) \/
 769     (y_of_x (delta_sub1_x (#2.52 pow 2)) y1 y2 y3 y4 y5 y6 < &0) \/
 770     (delta_y y1 y2 y3 y4 y5 y6 < &0) \/ (y3 < y2)
 771  )`;
 772 };;
 773
 774 add
 775 {
 776   idv="4328016440";
 777   doc="
 778     local fan/main estimate/appendix/terminal hex.
 779     flat-flat-flat
 780     full hexagon with three alternating flats.
 781     Big alternating central triangle.
 782     Symmetries, wlog y1<y2<y3.
 783     secs(357)
 784     oldname: test 5338748573 2013
 785     ";
 786   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 787   ineq = all_forall `ineq [
 788     (&2,y1,#2.52);
 789     (&2,y2,#2.52);
 790     (&2,y3,#2.52);
 791     (#3.01,y4,#3.915);
 792     (#3.01,y5,#3.915);
 793     (#3.01,y6,#3.915)
 794   ]
 795 (
 796   ( taum y1 y2 y3 y4 y5 y6 +
 797    y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 798    y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 799    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6
 800    > #0.712 ) \/
 801     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 802     y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
 803     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 804     y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
 805     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 806     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
 807     (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0) \/
 808     (y2 < y1) \/ (y3 < y2)
 809  )`;
 810 };;
 811
 812 run2
 813 {
 814   idv="1156793592";
 815   doc="
 816     local fan/main estimate/appendix/terminal hex.
 817     flat-flat-[234:nonflat,tau>=0]
 818     Big alternating central triangle.
 819     Symmetries, wlog y1<y2<y3.
 820     secs(357)
 821     oldname: 'test Z1'
 822     By symmetry wlog y5 < y6
 823     sec(454).
 824     ";
 825   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 826   ineq = all_forall `ineq [
 827     (&2,y1,#2.52);
 828     (&2,y2,#2.52);
 829     (&2,y3,#2.52);
 830       (#3.01,y4,#3.915);
 831       (#3.01,y5,#3.915);
 832     (#3.01,y6,#3.915)
 833   ]
 834 (
 835   ( taum y1 y2 y3 y4 y5 y6 +
 836    y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 837    y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6
 838     > #0.712) \/
 839     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 840     y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
 841     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 842     y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
 843      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)  \/
 844    (y6 < y5)
 845  )`;
 846 };;
 847
 848 run2
 849 {
 850   idv="5429733243";
 851   doc="
 852     local fan/main estimate/appendix/terminal hex.
 853     flat-flat-[234:nonflat,y1=2,delta>100]
 854     Big alternating central triangle.
 855     Symmetries, wlog y1<y2<y3.
 856     secs(357)
 857     oldname: 'test Z2-100'
 858     By symmetry wlog y5 < y6
 859     ";
 860   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Widthcutoff 0.0001];
 861   ineq = all_forall `ineq [
 862     (&2,y1,#2.52);
 863     (&2,y2,#2.52);
 864     (&2,y3,#2.52);
 865       (#3.01,y4,#3.915);
 866      (#3.01,y5,#3.915);
 867     (#3.01,y6,#3.915)
 868    ]
 869 (
 870     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 871     y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
 872     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 873     y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
 874     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100 \/
 875      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)  \/
 876    (y6 < y5) \/
 877     ( taum y1 y2 y3 y4 y5 y6 +
 878    y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 879    y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 880    y_of_x (mud_234_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 +
 881    &0 - sol0
 882     > #0.712)
 883  )`;
 884 };;
 885
 886 run2
 887 {
 888   idv="6941393103";
 889   doc="
 890     local fan/main estimate/appendix/terminal hex.
 891     flat-flat-[234:nonflat,y1=2,0<delta<100]
 892     Big alternating central triangle.
 893     Symmetries, wlog y1<y2<y3.
 894     secs(357)
 895     oldname: 'test Z2<100'
 896     By symmetry wlog y5 < y6
 897     ";
 898   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Widthcutoff 0.0001];
 899   ineq = all_forall `ineq [
 900     (&2,y1,#2.52);
 901     (&2,y2,#2.52);
 902     (&2,y3,#2.52);
 903       (#3.01,y4,#3.915);
 904      (#3.01,y5,#3.915);
 905     (#3.01,y6,#3.915)
 906    ]
 907 (
 908     ( taum y1 y2 y3 y4 y5 y6 +
 909    y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 910    y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 911 //   y_of_x (mudLs_234_x (sqrt(&15)) (sqrt(&100)) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 +
 912    &0 - sol0
 913     > #0.712) \/
 914     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 915     y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
 916     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 917     y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
 918     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 919     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100 \/
 920      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)  \/
 921    (y6 < y5)
 922  //   ( taum y1 y2 y3 y4 y5 y6 +
 923  //  y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 924  //  y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 925  //  &0 - sol0
 926  //   > #0.712)  \/
 927  )`;
 928 };;
 929
 930 (*
 931 run2
 932 {
 933   idv="test Z3";
 934   doc="
 935        local fan/main estimate/appendix/terminal hex/
 936        ear234(lo, tau< -0.07 becomes -- sol0) ear135(flat) ear126(flat)
 937     full hexagon with two flats, one lo
 938     Big alternating central triangle.
 939     By symmetry, wlog  y5 < y6.
 940     ";
 941   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
 942   ineq = all_forall `ineq [
 943     (&2,y1,#2.52);
 944     (&2,y2,#2.52);
 945     (&2,y3,#2.52);
 946       (#3.01,y4,#3.915);
 947      (#3.01,y5,#3.915);
 948     (#3.01,y6,#3.915)
 949    ]
 950 (
 951   ( taum y1 y2 y3 y4 y5 y6 +
 952    y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 953    y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 954    &0 - sol0
 955     > #0.712) \/
 956     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 957     y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
 958     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 959     y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
 960     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 961     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
 962      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)  \/
 963    (y6 < y5)
 964  )`;
 965 };;
 966 *)
 967
 968
 969 add
 970 {
 971   idv="test U1";
 972   doc="
 973        local fan/main estimate/appendix/terminal hex/
 974     full hexagon with two flats, one lo
 975     Big alternating central triangle.
 976     By symmetry, wlog  y5 < y6.
 977     ";
 978   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
 979   ineq = all_forall `ineq [
 980     (&2,y1,#2.52);
 981     (&2,y2,#2.52);
 982     (&2,y3,#2.52);
 983       (#3.01,y4,#3.915);
 984      (#3.01,y5,#3.915);
 985     (#3.01,y6,#3.915)
 986    ]
 987 (
 988   ( taum y1 y2 y3 y4 y5 y6 +
 989    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
 990    &0
 991     > #0.712) \/
 992     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
 993     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
 994      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)  \/
 995    (y6 < y5)
 996  )`;
 997 };;
 998
 999 add
1000 {
1001   idv="test U2";
1002   doc="
1003        local fan/main estimate/appendix/terminal hex/
1004     full hexagon with two flats, one lo
1005     Big alternating central triangle.
1006     By symmetry, wlog  y5 < y6.
1007     ";
1008   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1009   ineq = all_forall `ineq [
1010     (&2,y1,#2.52);
1011     (&2,y2,#2.52);
1012     (&2,y3,#2.52);
1013       (#3.01,y4,#3.915);
1014      (#3.01,y5,#3.915);
1015     (#3.01,y6,#3.915)
1016    ]
1017 (
1018   ( taum y1 y2 y3 y4 y5 y6 +
1019    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
1020    y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 +
1021    &0
1022     > #0.712) \/
1023     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1024     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1025     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100 \/
1026      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1027  )`;
1028 };;
1029
1030 run
1031 {
1032   idv="test U3";
1033   doc="
1034        local fan/main estimate/appendix/terminal hex/
1035     full hexagon with two flats, one lo
1036     Big alternating central triangle.
1037     By symmetry, wlog  y5 < y6.
1038     ";
1039   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1040   ineq = all_forall `ineq [
1041     (&2,y1,#2.52);
1042     (&2,y2,#2.52);
1043     (&2,y3,#2.52);
1044       (#3.01,y4,#3.915);
1045      (#3.01,y5,#3.915);
1046     (#3.01,y6,#3.915)
1047    ]
1048 (
1049   ( taum y1 y2 y3 y4 y5 y6 +
1050    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
1051    y_of_x (mudLs_126_x (#3.8729) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 +
1052    &0
1053     > #0.712) \/
1054     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1055     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1056     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1057     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100 \/
1058      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1059  )`;
1060 };;
1061
1062 add
1063 {
1064   idv="test U4";
1065   doc="
1066        local fan/main estimate/appendix/terminal hex/
1067     full hexagon with two flats, one lo
1068     Big alternating central triangle.
1069     ";
1070   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1071   ineq = all_forall `ineq [
1072     (&2,y1,#2.52);
1073     (&2,y2,#2.52);
1074     (&2,y3,#2.52);
1075       (#3.01,y4,#3.915);
1076      (#3.01,y5,#3.915);
1077     (#3.01,y6,#3.915)
1078    ]
1079 (
1080   ( taum y1 y2 y3 y4 y5 y6 +
1081    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
1082    &0  - sol0  +
1083    &0
1084     > #0.712) \/
1085     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1086     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1087     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1088     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1089      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1090  )`;
1091 };;
1092
1093 add
1094 {
1095   idv="test U5";
1096   doc="
1097        local fan/main estimate/appendix/terminal hex/
1098     full hexagon with two flats, one lo
1099     Big alternating central triangle.
1100     ";
1101   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1102   ineq = all_forall `ineq [
1103     (&2,y1,#2.52);
1104     (&2,y2,#2.52);
1105     (&2,y3,#2.52);
1106       (#3.01,y4,#3.915);
1107      (#3.01,y5,#3.915);
1108     (#3.01,y6,#3.915)
1109    ]
1110 (
1111   ( taum y1 y2 y3 y4 y5 y6 +
1112    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
1113    y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 +
1114    y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 +
1115    &0
1116     > #0.712) \/
1117     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100 \/
1118     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100 \/
1119     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1120     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1121      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)  \/
1122     (y5 < y6)
1123  )`;
1124 };;
1125
1126 add
1127 {
1128   idv="test U6";
1129   doc="
1130        local fan/main estimate/appendix/terminal hex/
1131     full hexagon with two flats, one lo
1132     Big alternating central triangle.
1133     ";
1134   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1135   ineq = all_forall `ineq [
1136     (&2,y1,#2.52);
1137     (&2,y2,#2.52);
1138     (&2,y3,#2.52);
1139       (#3.01,y4,#3.915);
1140      (#3.01,y5,#3.915);
1141     (#3.01,y6,#3.915)
1142    ]
1143 (
1144   ( taum y1 y2 y3 y4 y5 y6 +
1145    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
1146    y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 +
1147    y_of_x (mudLs_135_x (#3.8729) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 +
1148    &0
1149     > #0.712) \/
1150     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100 \/
1151     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1152     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100 \/
1153     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1154     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1155      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1156  )`;
1157 };;
1158
1159 add
1160 {
1161   idv="test U7";
1162   doc="
1163        local fan/main estimate/appendix/terminal hex/
1164     full hexagon with two flats, one lo
1165     Big alternating central triangle.
1166     ";
1167   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1168   ineq = all_forall `ineq [
1169     (&2,y1,#2.52);
1170     (&2,y2,#2.52);
1171     (&2,y3,#2.52);
1172       (#3.01,y4,#3.915);
1173      (#3.01,y5,#3.915);
1174     (#3.01,y6,#3.915)
1175    ]
1176 (
1177   ( taum y1 y2 y3 y4 y5 y6 +
1178    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
1179    y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 +
1180    &0 - sol0 +
1181    &0
1182     > #0.712) \/
1183     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100 \/
1184     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1185     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1186     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1187     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1188      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1189  )`;
1190 };;
1191
1192 add
1193 {
1194   idv="test U8";
1195   doc="
1196        local fan/main estimate/appendix/terminal hex/
1197     full hexagon with two flats, one lo
1198     Big alternating central triangle.
1199     ";
1200   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1201   ineq = all_forall `ineq [
1202     (&2,y1,#2.52);
1203     (&2,y2,#2.52);
1204     (&2,y3,#2.52);
1205       (#3.01,y4,#3.915);
1206      (#3.01,y5,#3.915);
1207     (#3.01,y6,#3.915)
1208    ]
1209 (
1210   ( taum y1 y2 y3 y4 y5 y6 +
1211    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
1212    y_of_x (mudLs_126_x (#3.8729) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 +
1213    y_of_x (mudLs_135_x (#3.8729) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 +
1214    &0
1215     > #0.712) \/
1216     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1217     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100 \/
1218     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1219     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100 \/
1220     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1221     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1222      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)  \/
1223     (y5 < y6)
1224  )`;
1225 };;
1226
1227 add
1228 {
1229   idv="test U9";
1230   doc="
1231        local fan/main estimate/appendix/terminal hex/
1232     full hexagon with two flats, one lo
1233     Big alternating central triangle.
1234     ";
1235   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1236   ineq = all_forall `ineq [
1237     (&2,y1,#2.52);
1238     (&2,y2,#2.52);
1239     (&2,y3,#2.52);
1240       (#3.01,y4,#3.915);
1241      (#3.01,y5,#3.915);
1242     (#3.01,y6,#3.915)
1243    ]
1244 (
1245   ( taum y1 y2 y3 y4 y5 y6 +
1246    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
1247    y_of_x (mudLs_126_x (#3.8729) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 +
1248     &0  - sol0 +
1249    &0
1250     > #0.712) \/
1251     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1252     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100 \/
1253     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1254     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1255     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1256     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1257      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1258  )`;
1259 };;
1260
1261 add
1262 {
1263   idv="test U10";
1264   doc="
1265        local fan/main estimate/appendix/terminal hex/
1266     full hexagon with two flats, one lo
1267     Big alternating central triangle.
1268     ";
1269   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1270   ineq = all_forall `ineq [
1271     (&2,y1,#2.52);
1272     (&2,y2,#2.52);
1273     (&2,y3,#2.52);
1274       (#3.01,y4,#3.915);
1275      (#3.01,y5,#3.915);
1276     (#3.01,y6,#3.915)
1277    ]
1278 (
1279   ( taum y1 y2 y3 y4 y5 y6 +
1280    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
1281     &0  - &2 * sol0 +
1282    &0
1283     > #0.712) \/
1284     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1285     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1286     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1287     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1288     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1289     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1290      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)  \/
1291     (y5 < y6)
1292  )`;
1293 };;
1294
1295
1296
1297 add
1298 {
1299   idv="test V5";
1300   doc="
1301        local fan/main estimate/appendix/terminal hex/
1302     full hexagon with two flats, one lo
1303     Big alternating central triangle.
1304     ";
1305   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1306   ineq = all_forall `ineq [
1307     (&2,y1,#2.52);
1308     (&2,y2,#2.52);
1309     (&2,y3,#2.52);
1310       (#3.01,y4,#3.915);
1311      (#3.01,y5,#3.915);
1312     (#3.01,y6,#3.915)
1313    ]
1314 (
1315   ( taum y1 y2 y3 y4 y5 y6 +
1316    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
1317    y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 +
1318    &0 - sol0 +
1319    &0
1320     > #0.712) \/
1321     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1322     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1323     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1324     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1325     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1326      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1327  )`;
1328 };;
1329
1330 add
1331 {
1332   idv="test V6";
1333   doc="
1334        local fan/main estimate/appendix/terminal hex/
1335     full hexagon with two flats, one lo
1336     Big alternating central triangle.
1337     ";
1338   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1339   ineq = all_forall `ineq [
1340     (&2,y1,#2.52);
1341     (&2,y2,#2.52);
1342     (&2,y3,#2.52);
1343       (#3.01,y4,#3.915);
1344      (#3.01,y5,#3.915);
1345     (#3.01,y6,#3.915)
1346    ]
1347 (
1348   ( taum y1 y2 y3 y4 y5 y6 +
1349    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
1350    &0 - &2 * sol0 +
1351    &0
1352     > #0.712) \/
1353     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1354     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1355     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1356     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1357     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1358     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1359      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0) \/
1360     (y5 < y6)
1361  )`;
1362 };;
1363
1364
1365 add
1366 {
1367   idv="test 3306409086 2013";
1368   doc="
1369     local fan/main estimate/appendix/terminal hex/
1370     ear234(tau >= -0.07) ear135(flat) ear126(flat)
1371     full hexagon with two flats,
1372     assumption tau-ear(234) >= - 0.07
1373     Big alternating central triangle.
1374     By symmetry wlog y5 < y6
1375     secs(500).
1376     ";
1377   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1378   ineq = all_forall `ineq [
1379     (&2,y1,#2.52);
1380     (&2,y2,#2.52);
1381     (&2,y3,#2.52);
1382       (#3.01,y4,#3.915);
1383       (#3.01,y5,#3.915);
1384     (#3.01,y6,#3.915)
1385   ]
1386 (
1387   ( taum y1 y2 y3 y4 y5 y6 - #0.07 +
1388    y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
1389    y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6
1390     > #0.712) \/
1391     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1392     y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1393     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1394     y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1395      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)  \/
1396    (y6 < y5)
1397  )`;
1398 };;
1399
1400 add
1401 {
1402   idv="test 9075398267 2013";
1403   doc="
1404        local fan/main estimate/appendix/terminal hex/
1405        ear234(lo, tau< -0.07 becomes -- sol0) ear135(flat) ear126(flat)
1406     full hexagon with two flats, one lo
1407     Big alternating central triangle.
1408     By symmetry, wlog  y5 < y6.
1409    secs(467)
1410     ";
1411   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1412   ineq = all_forall `ineq [
1413     (&2,y1,#2.52);
1414     (&2,y2,#2.52);
1415     (&2,y3,#2.52);
1416       (#3.01,y4,#3.915);
1417      (#3.01,y5,#3.915);
1418     (#3.01,y6,#3.915)
1419    ]
1420 (
1421   ( taum y1 y2 y3 y4 y5 y6 - sol0 +
1422    y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
1423    y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6
1424     > #0.712) \/
1425     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1426     y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1427     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1428     y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1429     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1430     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1431      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)  \/
1432    (y6 < y5)
1433  )`;
1434 };;
1435
1436 add2
1437 {
1438   idv="test 1324821088 2013";
1439   doc="
1440        local fan/main estimate/appendix/terminal hex/
1441        ear234(flat) ear135(nonflat) ear126(nonflat)
1442     one tau-nonflat > -0.07, other tau-nonfalt > 0.
1443     This includes nonflats not y1=2.
1444     full hexagon with one flat, hi,hi, can zero out both ears.
1445     By symmetry, wlog y6 > y5.
1446     sec(731)
1447     ";
1448   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1449   ineq = all_forall `ineq [
1450     (&2,y1,#2.52);
1451     (&2,y2,#2.52);
1452     (&2,y3,#2.52);
1453       (#3.01,y4,#3.915);
1454    (#3.01,y5,#3.915);
1455       (#3.01,y6,#3.915)
1456   ]
1457   (( taum y1 y2 y3 y4 y5 y6 - #0.07 +
1458    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6
1459     > #0.712) \/
1460     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1461     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1462      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0) \/
1463      (y5 < y6)
1464 )`;
1465 };;
1466
1467 add
1468 {
1469   idv="test 1324821088 2013 b";
1470   doc="full hexagon with one flat, hi,hi, can zero out both ears.
1471     Big alternating central triangle.
1472     ear234(flat), ear126(
1473     extra assumption, ear126 has delta < 50.
1474     By symmetry, wlog y4 < y5.
1475    The constant 0.013 comes from 2535350075.
1476     We add constant in on the hi case, even though it isn't needed here.
1477     To permit simplification of the lo case later.
1478     ";
1479   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1480   ineq = all_forall `ineq [
1481     (&2,y1,#2.52);
1482     (&2,y2,#2.52);
1483     (&2,y3,#2.52);
1484       (#3.01,y4,#3.915);
1485    (#3.01,y5,#3.915);
1486       (#3.01,y6,#3.915)
1487   ]
1488   (( taum y1 y2 y3 y4 y5 y6 - &2 * #0.07 +
1489    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6
1490     > #0.712) \/
1491     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1492     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1493     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &50 \/
1494      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1495 )`;
1496 };;
1497
1498 add
1499 {
1500   idv="test 1324821088 2013 c";
1501   doc="full hexagon with one flat, hi,hi, can zero out both ears.
1502     Big alternating central triangle.
1503     ear234(flat), ear126(
1504     extra assumption, ear126 has delta > 50.
1505     By symmetry, wlog y4 < y5.
1506    The constant 0.013 comes from 2535350075.
1507     We add constant in on the hi case, even though it isn't needed here.
1508     To permit simplification of the lo case later.
1509     ";
1510   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1511   ineq = all_forall `ineq [
1512     (&2,y1,#2.52);
1513     (&2,y2,#2.52);
1514     (&2,y3,#2.52);
1515       (#3.01,y4,#3.915);
1516    (#3.01,y5,#3.915);
1517       (#3.01,y6,#3.915)
1518   ]
1519   (( taum y1 y2 y3 y4 y5 y6 - &2 * #0.07 +
1520    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6
1521     > #0.712) \/
1522     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1523     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1524    y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 > &0 \/
1525    y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &50 \/
1526      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1527 )`;
1528 };;
1529
1530 add
1531 {
1532   idv="test 1324821088 2013 d";
1533   doc="full hexagon with one flat, hi,hi, can zero out both ears.
1534     Big alternating central triangle.
1535     ear234(flat), ear126(
1536     extra assumption, ear126 has delta > 50.
1537     By symmetry, wlog y4 < y5.
1538    The constant 0.013 comes from 2535350075.
1539     We add constant in on the hi case, even though it isn't needed here.
1540     To permit simplification of the lo case later.
1541     ";
1542   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1543   ineq = all_forall `ineq [
1544     (&2,y1,#2.52);
1545     (&2,y2,#2.52);
1546     (&2,y3,#2.52);
1547       (#3.01,y4,#3.915);
1548    (#3.01,y5,#3.915);
1549       (#3.01,y6,#3.915)
1550   ]
1551   (( taum y1 y2 y3 y4 y5 y6 - #0.07 - sol0 +
1552    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6
1553     > #0.712) \/
1554     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1555     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1556 //    y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 > -- #0.07 \/
1557
1558     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1559     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &10 \/
1560     y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1561
1562      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1563 )`;
1564 };;
1565
1566 add
1567 {
1568   idv="test 1324821088 2013 e";
1569   doc="full hexagon with one flat, hi,hi, can zero out both ears.
1570     Big alternating central triangle.
1571     ear234(flat), ear126(
1572     extra assumption, ear126 has delta > 50.
1573     By symmetry, wlog y4 < y5.
1574    The constant 0.013 comes from 2535350075.
1575     We add constant in on the hi case, even though it isn't needed here.
1576     To permit simplification of the lo case later.
1577     ";
1578   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1579   ineq = all_forall `ineq [
1580     (&2,y1,#2.52);
1581     (&2,y2,#2.52);
1582     (&2,y3,#2.52);
1583       (#3.01,y4,#3.915);
1584    (#3.01,y5,#3.915);
1585       (#3.01,y6,#3.915)
1586   ]
1587   (( taum y1 y2 y3 y4 y5 y6 - #0.07 +
1588      y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6 - sol0 +
1589    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6
1590     > #0.712) \/
1591     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1592     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1593     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &10 \/
1594     y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1595      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1596 )`;
1597 };;
1598
1599 add
1600 {
1601   idv="test 1324821088 2013 f";
1602   doc="full hexagon with one flat, hi,hi, can zero out both ears.
1603     Big alternating central triangle.
1604     ear234(flat), ear126(
1605     extra assumption, ear126 has delta > 50.
1606     By symmetry, wlog y4 < y5.
1607    The constant 0.013 comes from 2535350075.
1608     We add constant in on the hi case, even though it isn't needed here.
1609     To permit simplification of the lo case later.
1610     ";
1611   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1612   ineq = all_forall `ineq [
1613     (&2,y1,#2.52);
1614     (&2,y2,#2.52);
1615     (&2,y3,#2.52);
1616       (#3.01,y4,#3.915);
1617    (#3.01,y5,#3.915);
1618       (#3.01,y6,#3.915)
1619   ]
1620   (( taum y1 y2 y3 y4 y5 y6 - &2 * sol0 +
1621    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6
1622     > #0.712) \/
1623     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1624     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1625     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1626     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1627     y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1628     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1629     y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1630      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1631 )`;
1632 };;
1633
1634 add
1635 {
1636   idv="test 1324821088 2013 g";
1637   doc="full hexagon with one flat, hi,hi, can zero out both ears.
1638     Big alternating central triangle.
1639     ear234(flat), ear126(
1640     extra assumption, ear126 has delta > 50.
1641     By symmetry, wlog y4 < y5.
1642    The constant 0.013 comes from 2535350075.
1643     We add constant in on the hi case, even though it isn't needed here.
1644     To permit simplification of the lo case later.
1645     ";
1646   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1647   ineq = all_forall `ineq [
1648     (&2,y1,#2.52);
1649     (&2,y2,#2.52);
1650     (&2,y3,#2.52);
1651       (#3.01,y4,#3.915);
1652    (#3.01,y5,#3.915);
1653       (#3.01,y6,#3.915)
1654   ]
1655   (( taum y1 y2 y3 y4 y5 y6 - &2 * sol0 +
1656      y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  +
1657    y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6
1658     > #0.712) \/
1659     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1660     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1661     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1662     y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1663     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1664     y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0 \/
1665      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1666 )`;
1667 };;
1668
1669
1670 add2
1671 {
1672   idv="test B";
1673   doc="";
1674   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1675   ineq = all_forall `ineq [
1676     (&2,y1,#2.52);
1677     (&2,y2,#2.52);
1678     (&2,y3,#2.52);
1679     (#3.01,y4,#3.915);
1680     (#3.01,y5,#3.915);
1681     (#3.01,y6,#3.915)
1682   ]
1683 (  (taum y1 y2 y3 y4 y5 y6   > #0.712 ) \/
1684       y_of_x eulerA_x y1 y2 y3 y4 y5 y6 < &0 \/
1685       y4 < y5 \/ y5 < y6
1686 )`;
1687 };;
1688
1689 add
1690 {
1691   idv="test B1";
1692   doc="full hexagon tau+, tau+, tau-
1693     Big alternating central triangle.
1694     ";
1695   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1696   ineq = all_forall `ineq [
1697     (&2,y1,#2.52);
1698     (&2,y2,#2.52);
1699     (&2,y3,#2.52);
1700       (#3.01,y4,#3.915);
1701    (#3.01,y5,#3.915);
1702       (#3.01,y6,#3.915)
1703   ]
1704   (( taum y1 y2 y3 y4 y5 y6 +
1705           &0  -  sol0
1706     > #0.712) \/
1707     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1708     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1709      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0) \/
1710           (y5 < y6)
1711 )`;
1712 };;
1713
1714 add
1715 {
1716   idv="test B2";
1717   doc="full hexagon tau+, tau+, tau-
1718     Big alternating central triangle.
1719     extra assumption, ear126 has delta > 50.
1720     sqrt(15)> 3.8729.
1721     ";
1722   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1723   ineq = all_forall `ineq [
1724     (&2,y1,#2.52);
1725     (&2,y2,#2.52);
1726     (&2,y3,#2.52);
1727       (#3.01,y4,#3.915);
1728    (#3.01,y5,#3.915);
1729       (#3.01,y6,#3.915)
1730   ]
1731   (( taum y1 y2 y3 y4 y5 y6 +
1732           y_of_x (mudLs_234_x (#3.8729) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0
1733     > #0.712) \/
1734     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1735     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100 \/
1736      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1737 )`;
1738 };;
1739
1740 add
1741 {
1742   idv="test B3";
1743   doc="full hexagon tau+, tau+, tau-
1744     Big alternating central triangle.
1745     extra assumption, ear126 has delta > 50.
1746     ";
1747   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1748   ineq = all_forall `ineq [
1749     (&2,y1,#2.52);
1750     (&2,y2,#2.52);
1751     (&2,y3,#2.52);
1752       (#3.01,y4,#3.915);
1753    (#3.01,y5,#3.915);
1754       (#3.01,y6,#3.915)
1755   ]
1756   (( taum y1 y2 y3 y4 y5 y6 +
1757           y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0
1758     > #0.712) \/
1759     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100 \/
1760      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1761 )`;
1762 };;
1763
1764
1765 add
1766 {
1767   idv="test C1";
1768   doc="full hexagon tau+, tau-, tau-
1769     Big alternating central triangle.
1770     ";
1771   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1772   ineq = all_forall `ineq [
1773     (&2,y1,#2.52);
1774     (&2,y2,#2.52);
1775     (&2,y3,#2.52);
1776       (#3.01,y4,#3.915);
1777    (#3.01,y5,#3.915);
1778       (#3.01,y6,#3.915)
1779   ]
1780   (( taum y1 y2 y3 y4 y5 y6 +
1781           &0  -  sol0 +
1782           &0  -  sol0
1783     > #0.712) \/
1784     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1785     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1786     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1787     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1788      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1789 )`;
1790 };;
1791
1792 add
1793 {
1794   idv="test C2";
1795   doc="full hexagon tau+, tau-, tau-
1796     Big alternating central triangle.
1797     ";
1798   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1799   ineq = all_forall `ineq [
1800     (&2,y1,#2.52);
1801     (&2,y2,#2.52);
1802     (&2,y3,#2.52);
1803       (#3.01,y4,#3.915);
1804    (#3.01,y5,#3.915);
1805       (#3.01,y6,#3.915)
1806   ]
1807   (( taum y1 y2 y3 y4 y5 y6 +
1808           y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0  +
1809           &0  -  sol0
1810     > #0.712) \/
1811     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1812     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1813     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1814      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1815 )`;
1816 };;
1817
1818 add
1819 {
1820   idv="test C3";
1821   doc="full hexagon tau+, tau-, tau-
1822     Big alternating central triangle.
1823     ";
1824   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1825   ineq = all_forall `ineq [
1826     (&2,y1,#2.52);
1827     (&2,y2,#2.52);
1828     (&2,y3,#2.52);
1829       (#3.01,y4,#3.915);
1830    (#3.01,y5,#3.915);
1831       (#3.01,y6,#3.915)
1832   ]
1833   (( taum y1 y2 y3 y4 y5 y6 +
1834           y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0  +
1835           y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0
1836     > #0.712) \/
1837     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1838     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1839      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1840 )`;
1841 };;
1842
1843 add
1844 {
1845   idv="test D1";
1846   doc="full hexagon tau-, tau-, tau-
1847     Big alternating central triangle.
1848     ";
1849   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1850   ineq = all_forall `ineq [
1851     (&2,y1,#2.52);
1852     (&2,y2,#2.52);
1853     (&2,y3,#2.52);
1854       (#3.01,y4,#3.915);
1855    (#3.01,y5,#3.915);
1856       (#3.01,y6,#3.915)
1857   ]
1858   (( taum y1 y2 y3 y4 y5 y6 +
1859        &0 - &3 * sol0
1860     > #0.712) \/
1861     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1862     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1863     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1864     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1865     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1866     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1867      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1868 )`;
1869 };;
1870
1871 add
1872 {
1873   idv="test D2";
1874   doc="full hexagon tau-, tau-, tau-
1875     Big alternating central triangle.
1876     ";
1877   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1878   ineq = all_forall `ineq [
1879     (&2,y1,#2.52);
1880     (&2,y2,#2.52);
1881     (&2,y3,#2.52);
1882       (#3.01,y4,#3.915);
1883    (#3.01,y5,#3.915);
1884       (#3.01,y6,#3.915)
1885   ]
1886   (( taum y1 y2 y3 y4 y5 y6 +
1887           y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0  +
1888        &0 - &2 * sol0
1889     > #0.712) \/
1890     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1891     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1892     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1893     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1894     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1895      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1896 )`;
1897 };;
1898
1899 add
1900 {
1901   idv="test D3";
1902   doc="full hexagon tau-, tau-, tau-
1903     Big alternating central triangle.
1904     ";
1905   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1906   ineq = all_forall `ineq [
1907     (&2,y1,#2.52);
1908     (&2,y2,#2.52);
1909     (&2,y3,#2.52);
1910       (#3.01,y4,#3.915);
1911    (#3.01,y5,#3.915);
1912       (#3.01,y6,#3.915)
1913   ]
1914   (( taum y1 y2 y3 y4 y5 y6 +
1915           y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0  +
1916           y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0  +
1917        &0 - &1 * sol0
1918     > #0.712) \/
1919     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
1920     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &15 \/
1921     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1922     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1923      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1924 )`;
1925 };;
1926
1927 add
1928 {
1929   idv="test D4";
1930   doc="full hexagon tau-, tau-, tau-
1931     Big alternating central triangle.
1932     ";
1933   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1934   ineq = all_forall `ineq [
1935     (&2,y1,#2.52);
1936     (&2,y2,#2.52);
1937     (&2,y3,#2.52);
1938       (#3.01,y4,#3.915);
1939    (#3.01,y5,#3.915);
1940       (#3.01,y6,#3.915)
1941   ]
1942   (( taum y1 y2 y3 y4 y5 y6 +
1943           y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0  +
1944           y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0  +
1945           y_of_x (mud_234_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0
1946     > #0.712) \/
1947     y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1948     y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1949     y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &15 \/
1950      (y_of_x eulerA_x y1 y2 y3 y4 y5 y6 <  &0)
1951 )`;
1952 };;
1953
1954
1955 add
1956 {
1957   idv="test";
1958   doc="";
1959   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1960   ineq = all_forall `ineq [
1961     (&2,y1,&2);
1962     (&2,y2,#2.52);
1963     (&2,y3,#2.52);
1964     (#3.01,y4,#3.915);
1965     (&2,y5,&2);
1966     (&2,y6,&2)
1967   ]
1968 (
1969   taud y1 y2 y3 y4 y5 y6 > taud (#2.52) y2 y3 y4 y5 y6 \/
1970 delta_y y1 y2 y3 y4 y5 y6 < &0 \/
1971  delta_y (#2.52) y2 y3 y4 y5 y6 < &0
1972 )`;
1973 };;
1974
1975
1976
1977 add
1978 {
1979   idv="test";
1980   doc="";
1981   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
1982   ineq = all_forall `ineq [
1983     (#2.0,y1,#2.52);
1984     (&2,y2,#2.52);
1985     (&2,y3,#2.52);
1986     (#3.01,y4,#3.915);
1987     (&2,y5,&2);
1988       (&2,y6,&2)
1989   ]
1990 (
1991    (taum y1 y2 y3 y4 y5 y6 > &0 \/
1992     (delta_y y1 y2 y3 y4 y5 y6 > &20)  \/
1993     (delta_y y1 y2 y3 y4 y5 y6 < &0)
1994  ))`;
1995 };;
1996
1997 add
1998 {
1999   idv="test";
2000   doc="";
2001   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
2002   ineq = all_forall `ineq [
2003     (#2.0,y1,#2.52);
2004     (&2,y2,#2.52);
2005     (&2,y3,#2.52);
2006     (#3.01,y4,#3.915);
2007     (&2,y5,&2);
2008       (&2,y6,&2)
2009   ]
2010 (
2011   (y4  > #3.01 ) \/
2012    taum y1 y2 y3 y4 y5 y6 > -- #0.337 \/
2013     (delta_y y1 y2 y3 y4 y5 y6 < &0)
2014  )`;
2015 };;
2016
2017 skip
2018 {
2019   idv="4795451128";
2020   doc="old name: taud hex*
2021    test (also works with taud_v2)";
2022   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
2023   ineq = all_forall `ineq [
2024     (&2,y1,#2.52);
2025     (&2,y2,#2.52);
2026     (&2,y3,#2.52);
2027     (&2,y4,#2.52);
2028     (&2,y5,#2.52);
2029     (&2,y6,#2.52);
2030     (#3.01,z1,#3.915);
2031     (#3.01,z3,#3.915);
2032     (#3.01,z5,#3.915)
2033   ]
2034 (  (taum y1 y3 y5 z1 z3 z5 +
2035       taud y4 y3 y5 z1 (&2) (&2) +
2036       taud y6 y5 y1 z3 (&2) (&2) +
2037       taud y2 y1 y3 z5 (&2) (&2) > #0.712) \/
2038      delta_y y1 y3 y5 z1 z3 z5 < &0 \/
2039      delta_y y4 y3 y5 z1 (&2) (&2) < &0 \/
2040       delta_y y6 y5 y1 z3 (&2) (&2) < &0 \/
2041       delta_y y2 y1 y3 z5 (&2) (&2) < &0 \/
2042       y_of_x eulerA_x y1 y3 y5 z1 z3 z5 < &0)`;
2043 };;
2044
2045 run2
2046 {
2047   idv="1948775510";
2048   doc="was test Q.
2049     local fan/main estimate/terminal pent
2050     LHS(135,y1=2.52,delta=>20) RHS(126,delta=0)
2051     ";
2052   tags=[Main_estimate;Flypaper ["XFZFSWT"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
2053   ineq = all_forall `ineq [
2054     (&2,y1,#2.52);
2055     (&2,y2,#2.52);
2056     (&2,y3,#2.52);
2057     (&2,y4,&2);
2058     (#3.01,y5,#3.237);
2059     (#3.01,y6,#3.237)
2060   ]
2061 (taum y1 y2 y3 y4 y5 y6 +
2062        y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
2063        y_of_x (mud_135_x_v1 (&2 * h0) (&2) (&2)) y1 y2 y3 y4 y5 y6
2064  > #0.616 \/
2065    y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &20 \/
2066    y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0  // \/
2067 //   y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0
2068 )`;
2069 };;
2070
2071 run
2072 {
2073   idv="test-hex-numerical-taud";
2074   doc="For cfsqp only.
2075     This is the numerator of the 2nd derivative of the function taud.";
2076   tags=[Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0);Deprecated];
2077   ineq = all_forall `ineq [
2078     (&2,y1,#2.52);
2079     (&2,y2,#2.52);
2080     (&2,y3,#2.52);
2081     (#3.01,y4,#3.915);
2082     (&2,y5,&2);
2083     (&2,y6,&2)
2084   ]
2085     (((y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6) pow 2 > &0) \/
2086     (y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
2087        taud y1 y2 y3 y4 y5 y6 > #0.0 \/ // can adjust this later.
2088   delta_y y1 y2 y3 y4 y5 y6 < &15))`;
2089 };;
2090
2091
2092
2093 run
2094 {
2095   idv="test 9692636487";
2096   doc="local fan/main estimate/appendix/terminal hex.
2097     2nd derivative test for taud.";
2098   tags=[Main_estimate;Flypaper ["LIAULBV"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
2099   ineq = all_forall `ineq [
2100     (&2,y1,#2.52);
2101     (&2,y2,#2.52);
2102     (&2,y3,#2.52);
2103     (#3.01,y4,#3.915);
2104     (&2,y5,&2);
2105     (&2,y6,&2)
2106   ]
2107     (
2108     (y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 < &0 \/
2109   delta_y y1 y2 y3 y4 y5 y6 < &0) \/
2110   delta_y y1 y2 y3 y4 y5 y6 > &15
2111 )`;
2112 };;
2113
2114 add
2115 {
2116   idv="2735164514";
2117   doc="l";
2118   tags=[Main_estimate;Flypaper ["LIAULBV"];Cfsqp;Xconvert;Tex;Penalty(500.0,5000.0)];
2119   ineq = all_forall `ineq [
2120     (&2,y1,#2.52);
2121     (&2,y2,#2.52);
2122     (&2,y3,#2.52);
2123     (#3.01,y4,#3.915);
2124     (&2,y5,&2);
2125     (&2,y6,&2)
2126   ]
2127 (y_of_x delta_x1 y1 y2 y3 y4 y5 y6 < &0  \/
2128 &0 < y_of_x (delta_sub1_x  (&4)) y1 y2 y3 y4 y5 y6 )
2129 `;
2130 };;
2131
2132
2133
2134
2135 map Scripts.one_cfsqp ["test8"];;
2136 map Scripts.one_cfsqp ["taum pent3"];;
2137 Ineq.remove "test25353";;
2138 Auto_lib.testsplit true "5556646409 small domain";;
2139
2140     let flyspeck_needs_status filename (badfile,badmsg,ok) =
2141       if not(ok) then (badfile,badmsg,ok)
2142       else
2143         try     (flyspeck_needs filename); (badfile,badmsg,ok)
2144         with Failure t ->  (filename,t,false);;
2145
2146     let flyspeck_needs_list filenames =
2147       let (badfile,badmsg,ok) = itlist flyspeck_needs_status filenames ("","",true) in
2148         if ok then report "full load completed"
2149         else (report ("Failure in file "^badfile); report badmsg);;
2150
2151 flyspeck_needs_status "../development/thales/session/test1.hl" ("","",true);;
2152 flyspeck_needs_status "../development/thales/session/test2.hl" ("","",true);;
2153
2154 map flyspeck_needs ["../development/thales/session/test1.hl"; "../development/thales/session/test2.hl"];;
2155 flyspeck_needs_list ["../development/thales/session/test1.hl"; "../development/thales/session/test2.hl"];;
2156 flyspeck_needs_list ["../development/thales/session/test1.hl"; "../development/thales/session/test1.hl"];;
2157 rflyspeck_needs "../development/thales/session/test1.hl";;
2158 Test1.test;;