legacy/inequalities/kep_inequalities2.ml

   1 (* This file is a continuation of kep_inequalities.ml.\r
   2    It contains the inequalities related to quad clusters.\r
   3    It also contains some particularly long, tricky, or high-dimensional verifications *)\r
   4 \r
   5 \r
   6 \r
   7 (* ----------------------------------------------------------------------- *)\r
   8 (* \r
   9 latex-format comment\r
  10 \r
  11 \section{Notes on Interval Verifications}\r
  12     %{Appendix 2. Interval Verifications}\r
  13     \label{sec:verification-notes}\r
  14 \r
  15 We make a few remarks in this appendix on the verification of the\r
  16 inequalities of Proposition~\ref{calc:quad-bounds} and \ref{calc:d(R)}.\r
  17 The basic method in proving an inequality $f(x)<0$ for $x\in C$, is to\r
  18 use computer-based interval arithmetic to obtain rigorous upper bounds\r
  19 on the second derivatives: $|f_{ij}(x)|\le a_{ij}$, for $x\in C$.  These\r
  20 bounds lead immediately to upper bounds on $f(x)$ through a Taylor\r
  21 approximation with explicit bounds on the error.  We divide the domain\r
  22 $C$ as necessary until the Taylor approximation on each piece is less\r
  23 that the desired bound.\r
  24 \r
  25 Some of the inequalities involve as many as $12$ variables, such as the\r
  26 octahedral cases of Lemma~\ref{calc:d(R)}.  These are not directly\r
  27 accessible by computer.  We describe some reductions we have used, based\r
  28 on linear programming. We start by applying the dimension reduction\r
  29 techniques described in~\cite[Sec.~8.7]{part1}.  We have used these\r
  30 whenever possible.\r
  31 \r
  32 We will describe Lemma~\ref{calc:d(R)} because in various respects these\r
  33 inequalities have been the most difficult to prove, although the\r
  34 verifications of Lemmas~\ref{calc:quad-bounds} and \ref{lemma:1.153} are\r
  35 quite similar. If there is a diagonal of length $\le2\sqrt{2}$, we have\r
  36 two flat quarters $S_1$ and $S_2$.  The score breaks up into\r
  37     $\sigma=\sigma(S_1)+\sigma(S_2)$.  The simplices $S_1$ and\r
  38 $S_2$ share a three-dimensional face.   The inequality we wish to prove\r
  39 has the form\r
  40     $$\sigma \le a(\dih(S_1)+\dih_2(S_1)+\dih_2(S_2))+b.$$\r
  41 We break the shared face into smaller domains on which we have\r
  42     $$\r
  43     \begin{array}{lll}\r
  44     \sigma(S_1)&\le a (\dih(S_1)+\dih_2(S_1)) + b_1,\\\r
  45     \sigma(S_2)&\le a \dih_2(S_1) + b_2,\\\r
  46     \end{array}\r
  47     $$\r
  48 for some $b_1,b_2$ satisfying $b_1+b_2\le b$.  These inequalities are\r
  49 six-dimensional verifications.\r
  50 \r
  51 If the quad cluster is an octahedron with upright diagonal, there are\r
  52 four upright quarters $S_1,\ldots,S_4$. We consider inequalities of the\r
  53 form\r
  54     \begin{equation}\r
  55     \sigma(S_i)\le \sum _{j\ne 4} a_j^i y_j(S_i)\r
  56     + a_7 (\dih_1(S_i)-\pi/2) + \sum_{j=2}^3 a \epsilon^i_j \dih_j(S_i)\r
  57     + b^i.\r
  58     \label{eqn:Xi}\r
  59     \end{equation}\r
  60 If $\sum_{i=1}^4 a_j^i \le0$, $j\ne 4$, and $\sum_i b^i\le b$, then for\r
  61 appropriate $\epsilon^i_j\in\{0,1\}$, these inequalities imply the full\r
  62 inequality for octahedral quad clusters.\r
  63 \r
  64 By linear programming techniques, we were able to divide the domain of\r
  65 all octahedra into about $1200$ pieces and find inequalities of this\r
  66 form on each piece, giving an explicit list of inequalities that imply\r
  67 Lemma~\ref{calc:d(R)}.  The inequalities involve six variables and were\r
  68 verified by interval arithmetic.\r
  69 \r
  70 To find the optimal coefficients $a_j^i$ by linear programming we pose\r
  71 the linear problem\r
  72     $$\r
  73     \begin{array}{lll}\r
  74     &\max t \\\r
  75     &\hbox{such that}\\\r
  76     &\quad X_i,\quad i=1,2,3,4, \ \{S_1,S_2,S_3,S_4\}\in C\\\r
  77     &\quad\sum_i a_j^i \le 0,\\\r
  78     &\quad\sum_i b^i \le b,\r
  79     \end{array}\r
  80     $$\r
  81 where $\{S_1,S_2,S_3,S_4\}$ runs over all octahedra in a given domain\r
  82 $C$. The nonlinear inequalities~\ref{eqn:Xi} are to be regarded as\r
  83 linear conditions on the coefficients $a_j^i$, $b^i$, etc. The nonlinear\r
  84 functions $\sigma(S_i),\dih(S_i)$, $y_j(S_i)$ are to be regarded as the\r
  85 coefficients of the variables $a_j^i,\ldots$ in a system of linear\r
  86 inequalities.  There are infinitely many constraints, because the set\r
  87 $C$ of octahedra is infinite.  In practice we approximate $C$ by a large\r
  88 finite set.  If the maximum of $t$ is positive, then we have a\r
  89 collection of inequalities in small dimensions that imply the inequality\r
  90 for octahedral quad clusters.  Otherwise, we subdivide $C$ into smaller\r
  91 domains and try again.  Eventually, we succeed in partitioning the\r
  92 problem into six-dimensional pieces, which were verified by interval\r
  93 methods.\r
  94 \r
  95 \smallskip\r
  96 If the quad cluster is a mixed case, then Lemma~\ref{lemma:1.04} gives\r
  97     $$\sigma\le \vor_0, -1.04\,\pt,$$ so also\r
  98     $$\sigma \le \frac{3}{4}\vor_0 + \frac{1}{4} (-1.04\,\pt).$$\r
  99 In the pure Voronoi case with no quarters and no enclosed vertices, we\r
 100 have the approximation\r
 101     $$\sigma \le \vor(\cdot,\sqrt2) \le \vor_0.$$\r
 102 If we prove $\vor_0\le a (\dih_1+\dih_2) + b$, the mixed case is\r
 103 established. This is how the first of the Inequalities~\ref{calc:d(R)}\r
 104 was established. Dimension reduction reduces this to a seven-dimensional\r
 105 verification. We draw the shorter of the two diagonals between corners\r
 106 of the quad cluster. As we begin to subdivide this seven-dimensional\r
 107 domain, we are able to separate the quad cluster into two simplices\r
 108 along the diagonal, each scored by $\vor_0$.  This reduces the dimension\r
 109 further, to make it accessible.  The two last two cases of\r
 110 Inequality~\ref{calc:d(R)}, are similar, but we establish the\r
 111 inequalities\r
 112     $$\r
 113     \begin{array}{lll}\r
 114     \frac{3}{4}\vor_0 + \frac{1}{4} (-1.04\,\pt) &\le a (\dih_1+\dih_2) + b,\\\r
 115     \vor(\cdot,\sqrt2)&\le a (\dih_1+\dih_2) + b.\r
 116     \end{array}\r
 117     $$\r
 118 This completes our sketch of how the verifications were made.\r
 119 \r
 120 \r
 121 *)\r
 122 \r
 123 \r
 124 (* now we can list inequalities *)\r
 125 \r
 126 (* SPIII-1998 Lemma 4.1 *)\r
 127 \r
 128 \r
 129 let J_310151857 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 130         ((sigma_quad_approx1 v0 v1 v2 v3 v4) < --(&57906)/(&10000)\r
 131                 + ((&456766)/(&100000))*(dih_or_v v0 v1 v2 v4)))`);;\r
 132 let J_655029773 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 133         ((sigma_quad_approx1 v0 v1 v2 v3 v4) < --(&20749)/(&10000)\r
 134                 + ((&15094)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;\r
 135 let J_73283761 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 136         ((sigma_quad_approx1 v0 v1 v2 v3 v4) < --(&8341)/(&10000)\r
 137                 + ((&5301)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;\r
 138 let J_15141595 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 139         ((sigma_quad_approx1 v0 v1 v2 v3 v4) < --(&6284)/(&10000)\r
 140                 + ((&3878)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;\r
 141 let J_574391221 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 142         ((sigma_quad_approx1 v0 v1 v2 v3 v4) < (&4124)/(&10000)\r
 143                 - ((&1897)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;\r
 144 let J_396281725 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 145         ((sigma_quad_approx1 v0 v1 v2 v3 v4) < (&15707)/(&10000)\r
 146                 - ((&5905)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;\r
 147 let J_166451608 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 148         ((sigma_quad_approx1 v0 v1 v2 v3 v4) < (&41717)/(&100000)\r
 149                 - ((&3)/(&10))*(solid_area_quad_v v0 v1 v2 v3 v4)))`);;\r
 150 let J_539320075 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 151         ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < --(&581446)/(&100000)\r
 152                 + ((&449461)/(&100000))*(dih_or_v v0 v1 v2 v4)))`);;\r
 153 let J_122375455 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 154         ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < --(&2955)/(&1000)\r
 155                 + ((&21406)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;\r
 156 let J_408478278 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 157         ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < --(&6438)/(&10000)\r
 158                 + ((&316)/(&1000))*(dih_or_v v0 v1 v2 v4)))`);;\r
 159 let J_996268658 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 160         ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < --(&1317)/(&10000)))`);;\r
 161 let J_393682353 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 162         ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < (&3825)/(&10000)\r
 163                 - ((&2365)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;\r
 164 let J_775642319 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 165         ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 (&1)) < (&1071)/(&1000)\r
 166                 - ((&4747)/(&10000))*(dih_or_v v0 v1 v2 v4)))`);;\r
 167 let J_616145964 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 168         ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 ((&32)/(&10))) <\r
 169         --(&577942)/(&100000)\r
 170                 + ((&425863)/(&100000))*(dih_or_v v0 v1 v2 v4)))`);;\r
 171 let J_153920401 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 172         ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 ((&32)/(&10)) <\r
 173         --(&4893)/(&1000)\r
 174                 + ((&35294)/(&10000))*(dih_or_v v0 v1 v2 v4))))`);;\r
 175 let J_337637212 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 176         ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 ((&32)/(&10)) <\r
 177         --(&4126)/(&10000))))`);;\r
 178 let J_768057794 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 179         ((sigma_quad_approx1_lambda v0 v1 v2 v3 v4 ((&32)/(&10)) <\r
 180         (&33)/(&100)\r
 181                 - ((&316)/(&1000))*(dih_or_v v0 v1 v2 v4))))`);;\r
 182 let J_465497818 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 183         ((sigma_quad_approx1 v0 v1 v2 v3 v4 <\r
 184         -- ((&419351)/(&1000000))*(solid_area_quad_v v0 v1 v2 v3 v4)\r
 185         - (&5350181)/(&1000000)\r
 186                 + ((&4611391)/(&1000000))*(dih_or_v v0 v1 v2 v4))))`);;\r
 187 let J_18502666 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 188         ((sigma_quad_approx1 v0 v1 v2 v3 v4 <\r
 189         -- ((&419351)/(&1000000))*(solid_area_quad_v v0 v1 v2 v3 v4)\r
 190         - (&166174)/(&100000)\r
 191                 + ((&1582508)/(&1000000))*(dih_or_v v0 v1 v2 v4))))`);;\r
 192 let J_676439533 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 193         ((sigma_quad_approx1 v0 v1 v2 v3 v4 <\r
 194         -- ((&419351)/(&1000000))*(solid_area_quad_v v0 v1 v2 v3 v4)\r
 195         + (&895)/(&10000)\r
 196                 + ((&342747)/(&1000000))*(dih_or_v v0 v1 v2 v4))))`);;\r
 197 let J_974296985 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 198         ((sigma_quad_approx1 v0 v1 v2 v3 v4 <\r
 199         -- ((&419351)/(&1000000))*(solid_area_quad_v v0 v1 v2 v3 v4)\r
 200         + (&336909)/(&100000)\r
 201                 - ((&974137)/(&1000000))*(dih_or_v v0 v1 v2 v4))))`);;\r
 202 \r
 203 let C_940884472 = list_mk_conj[ \r
 204   J_310151857;\r
 205   J_655029773;\r
 206   J_73283761;\r
 207   J_15141595;\r
 208   J_574391221;\r
 209   J_396281725;\r
 210   J_166451608;\r
 211   J_539320075;\r
 212   J_122375455;\r
 213   J_408478278;\r
 214   J_996268658;\r
 215   J_393682353;\r
 216   J_775642319;\r
 217   J_616145964;\r
 218   J_153920401;\r
 219   J_337637212;\r
 220   J_768057794;\r
 221   J_465497818;\r
 222   J_18502666 ;\r
 223   J_676439533;\r
 224   J_974296985;];;\r
 225 \r
 226 \r
 227 (* SPIII-1998 Lemma 4.2 *)\r
 228 \r
 229 let J_322621318 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 230         ((sigma_quad_approx1 v0 v1 v2 v3 v4 <\r
 231         -- (&9494)/(&1000)\r
 232                 + ((&30508)/(&100000))*\r
 233                 ((dih_or_v v0 v1 v2 v4)+\r
 234                 (dih_or_v v0 v2 v3 v1)))))`);;\r
 235 let J_444643063 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 236         ((sigma_quad_approx1 v0 v1 v2 v3 v4 <\r
 237         -- (&10472)/(&100000)\r
 238                 + ((&27605)/(&100000))*\r
 239                 ((dih_or_v v0 v1 v2 v4)+\r
 240                 (dih_or_v v0 v2 v3 v1)))))`);;\r
 241 let J_552698390 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 242         ((sigma_quad_approx1 v0 v1 v2 v3 v4 <\r
 243          (&35926)/(&10000)\r
 244                 - ((&844)/(&1000))*\r
 245                 ((dih_or_v v0 v1 v2 v4)+\r
 246                 (dih_or_v v0 v2 v3 v1)))))`);;\r
 247 \r
 248 (* SPIII-1998 Lemma 4.3 *)\r
 249 \r
 250 let J_657406669 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 251         ((#1.153) < dih_or_v v0 v1 v2 v4))`);;\r
 252 let J_277330628 = (`!v0 v1 v2 v3 v4. ((is_quad_cluster_v v0 v1 v2 v3 v4) ==>\r
 253         ((dih_or_v v0 v1 v2 v4) < (#3.247)))`);;\r
 254 \r
 255 \r
 256 \r
 257 \r
 258 (*\r
 259  \r
 260 LOC: 2002 k.c page 49\r
 261 Five simplices in cyclic order A,B,C,D,E around edge x1.\r
 262 17.20 Group_20\r
 263 \r
 264 Note from text:  If the circumradius of a quasi-regular tetrahedron\r
 265 is >= 1.41, then tau > 1.8 pt and many of the inequalities hold\r
 266 (without further interval arithmetic calculation).\r
 267 \r
 268 *)\r
 269 \r
 270 (* interval verification by Ferguson *)\r
 271 let I_551665569=\r
 272   all_forall \r
 273   `\r
 274 let x6B = x5A in\r
 275 let x2B = x3A in\r
 276 let x6C = x5B in\r
 277 let x2C = x3B in\r
 278 let x6D = x5C in\r
 279 let x2D = x3C in\r
 280 let x6E = x5D in\r
 281 let x2E = x3D in\r
 282 let x6A = x5E in\r
 283 let x2A = x3E in\r
 284    (ineq\r
 285    [((#4.0), x1, square_2t0);\r
 286     ((#4.0), x2A, square_2t0);\r
 287     ((#4.0), x3A, square_2t0);\r
 288     ((#4.0), x4A, square_2t0);\r
 289     ((#4.0), x5A, square_2t0);\r
 290     ((#4.0), x6A, square_2t0);\r
 291     ((#4.0), x2B, square_2t0);\r
 292     ((#4.0), x3B, square_2t0);\r
 293     ((#4.0), x4B, square_2t0);\r
 294     ((#4.0), x5B, square_2t0);\r
 295     ((#4.0), x6B, square_2t0);\r
 296     ((#4.0), x2C, square_2t0);\r
 297     ((#4.0), x3C, square_2t0);\r
 298     ((#8.0), x4C, square_4t0);  // NB\r
 299     ((#4.0), x5C, square_2t0);\r
 300     ((#4.0), x6C, square_2t0);\r
 301     ((#4.0), x2D, square_2t0);\r
 302     ((#4.0), x3D, square_2t0);\r
 303     ((#4.0), x4D, square_2t0);\r
 304     ((#4.0), x5D, square_2t0);\r
 305     ((#4.0), x6D, square_2t0);\r
 306     ((#4.0), x2E, square_2t0);\r
 307     ((#4.0), x3E, square_2t0);\r
 308     ((#8.0), x4E, square_4t0);  // NB\r
 309     ((#4.0), x5E, square_2t0);\r
 310     ((#4.0), x6E, square_2t0)]\r
 311       (((tau_sigma_x x1 x2A x3A x4A x5A x6A) +. \r
 312        (tau_sigma_x x1 x2B x3B x4B x5B x6B) +.\r
 313       (tau_sigma_x x1 x2D x3D x4D x5D x6D) >. (#1.4) *. pt) \/\r
 314        ((dih_x x1 x2A x3A x4A x5A x6A) +.\r
 315           (dih_x x1 x2B x3B x4B x5B x6B) +.\r
 316          (dih_x x1 x2C x3C x4C x5C x6C) +.\r
 317          (dih_x x1 x2D x3D x4D x5D x6D) +.\r
 318          (dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi\r
 319     )))`;;\r
 320 \r
 321 (* interval verification by Ferguson *)\r
 322 let I_824762926=\r
 323   all_forall \r
 324   `\r
 325 let x6B = x5A in\r
 326 let x2B = x3A in\r
 327 let x6C = x5B in\r
 328 let x2C = x3B in\r
 329 let x6D = x5C in\r
 330 let x2D = x3C in\r
 331 let x6E = x5D in\r
 332 let x2E = x3D in\r
 333 let x6A = x5E in\r
 334 let x2A = x3E in\r
 335    (ineq\r
 336    [((#4.0), x1, square_2t0);\r
 337     ((#4.0), x2A, square_2t0);\r
 338     ((#4.0), x3A, square_2t0);\r
 339     ((#4.0), x4A, square_2t0);\r
 340     ((#4.0), x5A, square_2t0);\r
 341     ((#4.0), x6A, square_2t0);\r
 342     ((#4.0), x2B, square_2t0);\r
 343     ((#4.0), x3B, square_2t0);\r
 344     ((#4.0), x4B, square_2t0);\r
 345     ((#4.0), x5B, square_2t0);\r
 346     ((#4.0), x6B, square_2t0);\r
 347     ((#4.0), x2C, square_2t0);\r
 348     ((#4.0), x3C, square_2t0);\r
 349     ((#4.0), x4C, square_2t0);\r
 350     ((#4.0), x5C, square_2t0);\r
 351     ((#4.0), x6C, square_2t0);\r
 352     ((#4.0), x2D, square_2t0);\r
 353     ((#4.0), x3D, square_2t0);\r
 354     ((#8.0), x4D, square_4t0); // NB \r
 355     ((#4.0), x5D, square_2t0);\r
 356     ((#4.0), x6D, square_2t0);\r
 357     ((#4.0), x2E, square_2t0);\r
 358     ((#4.0), x3E, square_2t0);\r
 359     ((#8.0), x4E, square_4t0); // NB \r
 360     ((#4.0), x5E, square_2t0);\r
 361     ((#4.0), x6E, square_2t0)]\r
 362       (((tau_sigma_x x1 x2A x3A x4A x5A x6A) +. \r
 363        (tau_sigma_x x1 x2B x3B x4B x5B x6B) +.\r
 364       (tau_sigma_x x1 x2C x3C x4C x5C x6C) >. (#1.4) *. pt) \/\r
 365        ((dih_x x1 x2A x3A x4A x5A x6A) +.\r
 366           (dih_x x1 x2B x3B x4B x5B x6B) +.\r
 367          (dih_x x1 x2C x3C x4C x5C x6C) +.\r
 368          (dih_x x1 x2D x3D x4D x5D x6D) +.\r
 369          (dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi\r
 370     )))`;;\r
 371 \r
 372 (* interval verification by Ferguson *)\r
 373 let I_675785884=\r
 374   all_forall \r
 375   `\r
 376 let x6B = x5A in\r
 377 let x2B = x3A in\r
 378 let x6C = x5B in\r
 379 let x2C = x3B in\r
 380 let x6D = x5C in\r
 381 let x2D = x3C in\r
 382 let x6E = x5D in\r
 383 let x2E = x3D in\r
 384 let x6A = x5E in\r
 385 let x2A = x3E in\r
 386    (ineq\r
 387    [((#4.0), x1, square_2t0);\r
 388     ((#4.0), x2A, square_2t0);\r
 389     ((#4.0), x3A, square_2t0);\r
 390     ((#4.0), x4A, square_2t0);\r
 391     ((#4.0), x5A, square_2t0);\r
 392     ((#4.0), x6A, square_2t0);\r
 393     ((#4.0), x2B, square_2t0);\r
 394     ((#4.0), x3B, square_2t0);\r
 395     ((#4.0), x4B, square_2t0);\r
 396     ((#4.0), x5B, square_2t0);\r
 397     ((#4.0), x6B, square_2t0);\r
 398     ((#4.0), x2C, square_2t0);\r
 399     ((#4.0), x3C, square_2t0);\r
 400     (square_2t0, x4C, (#8.0));  // NB \r
 401     ((#4.0), x5C, square_2t0);\r
 402     ((#4.0), x6C, square_2t0);\r
 403     ((#4.0), x2D, square_2t0);\r
 404     ((#4.0), x3D, square_2t0);\r
 405     ((#4.0), x4D, square_2t0); \r
 406     ((#4.0), x5D, square_2t0);\r
 407     ((#4.0), x6D, square_2t0);\r
 408     ((#4.0), x2E, square_2t0);\r
 409     ((#4.0), x3E, square_2t0);\r
 410     (square_2t0, x4E, square_4t0); // NB\r
 411     ((#4.0), x5E, square_2t0);\r
 412     ((#4.0), x6E, square_2t0)]\r
 413       (((tau_sigma_x x1 x2A x3A x4A x5A x6A) +. \r
 414        (tau_sigma_x x1 x2B x3B x4B x5B x6B) +.\r
 415       (tauhatpi_x x1 x2C x3C x4C x5C x6C) +.\r
 416           (tau_sigma_x x1 x2D x3D x4D x5D x6D) \r
 417            >. ((#1.4) *. pt +. D31)) \/\r
 418        ((dih_x x1 x2A x3A x4A x5A x6A) +.\r
 419           (dih_x x1 x2B x3B x4B x5B x6B) +.\r
 420          (dih_x x1 x2C x3C x4C x5C x6C) +.\r
 421          (dih_x x1 x2D x3D x4D x5D x6D) +.\r
 422          (dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi ) \/\r
 423       (dih_x x1 x2E x3E x4E x5E x6E <. #1.32 )\r
 424       ))`;;\r
 425 \r
 426 (* interval verification by Ferguson *)\r
 427 let I_193592217=\r
 428   all_forall \r
 429   `\r
 430 let x6B = x5A in\r
 431 let x2B = x3A in\r
 432 let x6C = x5B in\r
 433 let x2C = x3B in\r
 434 let x6D = x5C in\r
 435 let x2D = x3C in\r
 436 let x6E = x5D in\r
 437 let x2E = x3D in\r
 438 let x6A = x5E in\r
 439 let x2A = x3E in\r
 440    (ineq\r
 441    [((#4.0), x1, square_2t0);\r
 442     ((#4.0), x2A, square_2t0);\r
 443     ((#4.0), x3A, square_2t0);\r
 444     ((#4.0), x4A, square_2t0);\r
 445     ((#4.0), x5A, square_2t0);\r
 446     ((#4.0), x6A, square_2t0);\r
 447     ((#4.0), x2B, square_2t0);\r
 448     ((#4.0), x3B, square_2t0);\r
 449     ((#4.0), x4B, square_2t0);\r
 450     ((#4.0), x5B, square_2t0);\r
 451     ((#4.0), x6B, square_2t0);\r
 452     ((#4.0), x2C, square_2t0);\r
 453     ((#4.0), x3C, square_2t0);\r
 454     ((#4.0), x4C, square_2t0);\r
 455     ((#4.0), x5C, square_2t0);\r
 456     ((#4.0), x6C, square_2t0);\r
 457     ((#4.0), x2D, square_2t0);\r
 458     ((#4.0), x3D, square_2t0);\r
 459     (square_2t0, x4D, (#8.0));  // NB  \r
 460     ((#4.0), x5D, square_2t0);\r
 461     ((#4.0), x6D, square_2t0);\r
 462     ((#4.0), x2E, square_2t0);\r
 463     ((#4.0), x3E, square_2t0);\r
 464     (square_2t0, x4E, square_4t0); // NB\r
 465     ((#4.0), x5E, square_2t0);\r
 466     ((#4.0), x6E, square_2t0)]\r
 467       (((tau_sigma_x x1 x2A x3A x4A x5A x6A) +. \r
 468        (tau_sigma_x x1 x2B x3B x4B x5B x6B) +.\r
 469       (tau_sigma_x x1 x2C x3C x4C x5C x6C) +.\r
 470           (tauhatpi_x x1 x2D x3D x4D x5D x6D) \r
 471            >. ((#1.4) *. pt +. D31)) \/\r
 472        ((dih_x x1 x2A x3A x4A x5A x6A) +.\r
 473           (dih_x x1 x2B x3B x4B x5B x6B) +.\r
 474          (dih_x x1 x2C x3C x4C x5C x6C) +.\r
 475          (dih_x x1 x2D x3D x4D x5D x6D) +.\r
 476          (dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi ) \/\r
 477       (dih_x x1 x2E x3E x4E x5E x6E <. #1.32 )\r
 478       ))`;;\r
 479 \r
 480 \r
 481 \r
 482 \r
 483 (*\r
 484  \r
 485 LOC: 2002 k.c page 50\r
 486 17.21 Group_21\r
 487 \r
 488 Note from text: As in Section 17.20, the quasi-regular tetrahedra\r
 489 are generally compression scored.  The constraint sum dih = 2pi\r
 490 is assumed.  \r
 491 [Note 2/17/2004: We relax this constraint to sum dih <= 2 pi.]\r
 492 \r
 493 *)\r
 494 \r
 495 (* interval verification by Ferguson *)\r
 496 let I_325738864=\r
 497   all_forall \r
 498   `\r
 499 let x6B = x5A in\r
 500 let x2B = x3A in\r
 501 let x6C = x5B in\r
 502 let x2C = x3B in\r
 503 let x6D = x5C in\r
 504 let x2D = x3C in\r
 505 let x6E = x5D in\r
 506 let x2E = x3D in\r
 507 let x6A = x5E in\r
 508 let x2A = x3E in\r
 509    (ineq\r
 510    [((#4.0), x1, square_2t0);\r
 511     ((#4.0), x2A, square_2t0);\r
 512     ((#4.0), x3A, square_2t0);\r
 513     ((#4.0), x4A, square_2t0);\r
 514     ((#4.0), x5A, square_2t0);\r
 515     ((#4.0), x6A, square_2t0);\r
 516     ((#4.0), x2B, square_2t0);\r
 517     ((#4.0), x3B, square_2t0);\r
 518     ((#4.0), x4B, square_2t0);\r
 519     ((#4.0), x5B, square_2t0);\r
 520     ((#4.0), x6B, square_2t0);\r
 521     ((#4.0), x2C, square_2t0);\r
 522     ((#4.0), x3C, square_2t0);\r
 523     ((#4.0), x4C, square_2t0);\r
 524     ((#4.0), x5C, square_2t0);\r
 525     ((#4.0), x6C, square_2t0);\r
 526     ((#4.0), x2D, square_2t0);\r
 527     ((#4.0), x3D, square_2t0);\r
 528     ((#4.0), x4D, square_2t0);\r
 529     ((#4.0), x5D, square_2t0);\r
 530     ((#4.0), x6D, square_2t0);\r
 531     ((#4.0), x2E, square_2t0);\r
 532     ((#4.0), x3E, square_2t0);\r
 533     ((#8.0), x4E, square_4t0); // NB\r
 534     ((#4.0), x5E, square_2t0);\r
 535     ((#4.0), x6E, square_2t0)]\r
 536       (((tau_sigma_x x1 x2A x3A x4A x5A x6A) +. \r
 537        (tau_sigma_x x1 x2B x3B x4B x5B x6B) +.\r
 538       (tau_sigma_x x1 x2C x3C x4C x5C x6C) +.\r
 539           (tau_sigma_x x1 x2D x3D x4D x5D x6D) \r
 540            >. ((#1.5) *. pt )) \/\r
 541        ((dih_x x1 x2A x3A x4A x5A x6A) +.\r
 542           (dih_x x1 x2B x3B x4B x5B x6B) +.\r
 543          (dih_x x1 x2C x3C x4C x5C x6C) +.\r
 544          (dih_x x1 x2D x3D x4D x5D x6D) +.\r
 545          (dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi )\r
 546       ))`;;\r
 547 \r
 548 (* interval verification by Ferguson *)\r
 549 let I_314974315=\r
 550   all_forall \r
 551   `\r
 552 let x6B = x5A in\r
 553 let x2B = x3A in\r
 554 let x6C = x5B in\r
 555 let x2C = x3B in\r
 556 let x6D = x5C in\r
 557 let x2D = x3C in\r
 558 let x6E = x5D in\r
 559 let x2E = x3D in\r
 560 let x6A = x5E in\r
 561 let x2A = x3E in\r
 562    (ineq\r
 563    [((#4.0), x1 , square_2t0);\r
 564     ((#4.0), x2A, square_2t0);\r
 565     ((#4.0), x3A, square_2t0);\r
 566     ((#4.0), x4A, square_2t0);\r
 567     ((#4.0), x5A, square_2t0);\r
 568     ((#4.0), x6A, square_2t0);\r
 569     ((#4.0), x2B, square_2t0);\r
 570     ((#4.0), x3B, square_2t0);\r
 571     ((#4.0), x4B, square_2t0);\r
 572     ((#4.0), x5B, square_2t0);\r
 573     ((#4.0), x6B, square_2t0);\r
 574     ((#4.0), x2C, square_2t0);\r
 575     ((#4.0), x3C, square_2t0);\r
 576     ((#4.0), x4C, square_2t0);\r
 577     ((#4.0), x5C, square_2t0);\r
 578     ((#4.0), x6C, square_2t0);\r
 579     ((#4.0), x2D, square_2t0);\r
 580     ((#4.0), x3D, square_2t0);\r
 581     ((#4.0), x4D, square_2t0);\r
 582     ((#4.0), x5D, square_2t0);\r
 583     ((#4.0), x6D, square_2t0);\r
 584     ((#4.0), x2E, square_2t0);\r
 585     ((#4.0), x3E, square_2t0);\r
 586     (square_2t0, x4E, (#8.0)); // NB\r
 587     ((#4.0), x5E, square_2t0);\r
 588     ((#4.0), x6E, square_2t0)]\r
 589       (((tau_sigma_x x1 x2A x3A x4A x5A x6A) +. \r
 590        (tau_sigma_x x1 x2B x3B x4B x5B x6B) +.\r
 591       (tau_sigma_x x1 x2C x3C x4C x5C x6C) +.\r
 592           (tau_sigma_x x1 x2D x3D x4D x5D x6D) +.\r
 593           (tauhatpi_x x1 x2E x3E x4E x5E x6E) \r
 594            >. ((#1.5) *. pt +. D31 )) \/\r
 595        ((dih_x x1 x2A x3A x4A x5A x6A) +.\r
 596           (dih_x x1 x2B x3B x4B x5B x6B) +.\r
 597          (dih_x x1 x2C x3C x4C x5C x6C) +.\r
 598          (dih_x x1 x2D x3D x4D x5D x6D) +.\r
 599          (dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi )\r
 600       ))`;;\r
 601 \r
 602 (*\r
 603  \r
 604 LOC: 2002 k.c page 50\r
 605 17.22 Group_22\r
 606 [The constraint sum dih <= 2pi was not explicitly stated in the text.]\r
 607 *)\r
 608 \r
 609 (* interval verification by Ferguson, I think.  In SPVI-1998, it carries\r
 610 a dagger, which means that Ferguson has done the verification, but the\r
 611 dagger has been commented out in the tex file. -TCH 1/19/2008 *)\r
 612 let I_867359387=\r
 613   all_forall \r
 614   `\r
 615 let x6B = x5A in\r
 616 let x2B = x3A in\r
 617 let x6C = x5B in\r
 618 let x2C = x3B in\r
 619 let x6D = x5C in\r
 620 let x2D = x3C in\r
 621 let x6E = x5D in\r
 622 let x2E = x3D in\r
 623 let x6A = x5E in\r
 624 let x2A = x3E in\r
 625    (ineq\r
 626    [((#4.0), x1 , square_2t0);\r
 627     ((#4.0), x2A, square_2t0);\r
 628     ((#4.0), x3A, square_2t0);\r
 629     ((#4.0), x4A, square_2t0);\r
 630     ((#4.0), x5A, square_2t0);\r
 631     ((#4.0), x6A, square_2t0);\r
 632     ((#4.0), x2B, square_2t0);\r
 633     ((#4.0), x3B, square_2t0);\r
 634     ((#4.0), x4B, square_2t0);\r
 635     ((#4.0), x5B, square_2t0);\r
 636     ((#4.0), x6B, square_2t0);\r
 637     ((#4.0), x2C, square_2t0);\r
 638     ((#4.0), x3C, square_2t0);\r
 639     ((#4.0), x4C, square_2t0);\r
 640     ((#4.0), x5C, square_2t0);\r
 641     ((#4.0), x6C, square_2t0);\r
 642     ((#4.0), x2D, square_2t0);\r
 643     ((#4.0), x3D, square_2t0);\r
 644     ((#4.0), x4D, square_2t0);\r
 645     ((#4.0), x5D, square_2t0);\r
 646     ((#4.0), x6D, square_2t0);\r
 647     ((#4.0), x2E, square_2t0);\r
 648     ((#4.0), x3E, square_2t0);\r
 649     (square_2t0, x4E, (#8.0)); // NB\r
 650     ((#4.0), x5E, square_2t0);\r
 651     ((#4.0), x6E, square_2t0)]\r
 652       (((sigma_qrtet_x x1 x2A x3A x4A x5A x6A) +. \r
 653        (sigma_qrtet_x x1 x2B x3B x4B x5B x6B) +.\r
 654       (sigma_qrtet_x x1 x2C x3C x4C x5C x6C) +.\r
 655           (sigma_qrtet_x x1 x2D x3D x4D x5D x6D) +.\r
 656           (sigmahat_x x1 x2E x3E x4E x5E x6E) \r
 657            <. #0.114) \/\r
 658        ((dih_x x1 x2A x3A x4A x5A x6A) +.\r
 659           (dih_x x1 x2B x3B x4B x5B x6B) +.\r
 660          (dih_x x1 x2C x3C x4C x5C x6C) +.\r
 661          (dih_x x1 x2D x3D x4D x5D x6D) +.\r
 662          (dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi )\r
 663       ))`;;\r
 664 \r
 665 \r
 666 (*\r
 667 LOC: 2002 III, page 15.\r
 668 Sec. 10, Group_4\r
 669 SKIP equation 2.  \r
 670 It asserts that the angle sum around a vertex is 2pi.  \r
 671 This is not an interval calculation.\r
 672 *)\r
 673 \r
 674 (*\r
 675 LOC: 2002 III, page 15.\r
 676 Sec. 10, Group_4\r
 677 equation 3.  Dihedral sum changed to an inequality.\r
 678 *)\r
 679 \r
 680 let J_694278521=\r
 681   all_forall \r
 682   `\r
 683 let x6B = x5A in\r
 684 let x2B = x3A in\r
 685 let x6C = x5B in\r
 686 let x2C = x3B in\r
 687 let x6D = x5C in\r
 688 let x2D = x3C in\r
 689 let x6E = x5D in\r
 690 let x2E = x3D in\r
 691 let x6A = x5E in\r
 692 let x2A = x3E in\r
 693    (ineq\r
 694    [((#4.0), x1, square_2t0);\r
 695     ((#4.0), x2A, square_2t0);\r
 696     ((#4.0), x3A, square_2t0);\r
 697     ((#4.0), x4A, square_2t0);\r
 698     ((#4.0), x5A, square_2t0);\r
 699     ((#4.0), x6A, square_2t0);\r
 700     ((#4.0), x2B, square_2t0);\r
 701     ((#4.0), x3B, square_2t0);\r
 702     ((#4.0), x4B, square_2t0);\r
 703     ((#4.0), x5B, square_2t0);\r
 704     ((#4.0), x6B, square_2t0);\r
 705     ((#4.0), x2C, square_2t0);\r
 706     ((#4.0), x3C, square_2t0);\r
 707     ((#4.0), x4C, square_2t0); \r
 708     ((#4.0), x5C, square_2t0);\r
 709     ((#4.0), x6C, square_2t0);\r
 710     ((#4.0), x2D, square_2t0);\r
 711     ((#4.0), x3D, square_2t0);\r
 712     ((#4.0), x4D, square_2t0);\r
 713     ((#4.0), x5D, square_2t0);\r
 714     ((#4.0), x6D, square_2t0);\r
 715     ((#4.0), x2E, square_2t0);\r
 716     ((#4.0), x3E, square_2t0);\r
 717     ((#4.0), x4E, square_2t0); \r
 718     ((#4.0), x5E, square_2t0);\r
 719     ((#4.0), x6E, square_2t0)]\r
 720       ((\r
 721         ((sigma_qrtet_x x1 x2A x3A x4A x5A x6A) +. \r
 722            #0.419351*. (sol_x x1 x2A x3A x4A x5A x6A)) +.\r
 723         ((sigma_qrtet_x x1 x2B x3B x4B x5B x6B) +. \r
 724            #0.419351*. (sol_x x1 x2B x3B x4B x5B x6B)) +.\r
 725         ((sigma_qrtet_x x1 x2C x3C x4C x5C x6C) +. \r
 726            #0.419351*. (sol_x x1 x2C x3C x4C x5C x6C)) +.\r
 727         ((sigma_qrtet_x x1 x2D x3D x4D x5D x6D) +. \r
 728            #0.419351*. (sol_x x1 x2D x3D x4D x5D x6D)) +.\r
 729         ((sigma_qrtet_x x1 x2E x3E x4E x5E x6E) +. \r
 730            #0.419351*. (sol_x x1 x2E x3E x4E x5E x6E)) \r
 731     <. (#5.0 *. (#0.2856354))) \/\r
 732 \r
 733        ((dih_x x1 x2A x3A x4A x5A x6A) +.\r
 734           (dih_x x1 x2B x3B x4B x5B x6B) +.\r
 735          (dih_x x1 x2C x3C x4C x5C x6C) +.\r
 736          (dih_x x1 x2D x3D x4D x5D x6D) +.\r
 737          (dih_x x1 x2E x3E x4E x5E x6E) >. (#2.0) *. pi\r
 738     )))`;;\r
 739 \r
 740 \r
 741 (*\r
 742  \r
 743 LOC: 2002 III, page 15.\r
 744 Sec. 10, Group_4\r
 745 *)\r
 746 \r
 747 (*\r
 748 equation 1. Dihedral sum changed to inequality.\r
 749 *)\r
 750 \r
 751 let J_895315463=\r
 752   all_forall \r
 753   `\r
 754 let x6B = x5A in\r
 755 let x2B = x3A in\r
 756 let x6C = x5B in\r
 757 let x2C = x3B in\r
 758 let x6D = x5C in\r
 759 let x2D = x3C in\r
 760 let x6A = x5D in\r
 761 let x2A = x3D in\r
 762    (ineq\r
 763    [((#4.0), x1, square_2t0);\r
 764     ((#4.0), x2A, square_2t0);\r
 765     ((#4.0), x3A, square_2t0);\r
 766     ((#4.0), x4A, square_2t0);\r
 767     ((#4.0), x5A, square_2t0);\r
 768     ((#4.0), x6A, square_2t0);\r
 769     ((#4.0), x2B, square_2t0);\r
 770     ((#4.0), x3B, square_2t0);\r
 771     ((#4.0), x4B, square_2t0);\r
 772     ((#4.0), x5B, square_2t0);\r
 773     ((#4.0), x6B, square_2t0);\r
 774     ((#4.0), x2C, square_2t0);\r
 775     ((#4.0), x3C, square_2t0);\r
 776     ((#4.0), x4C, square_2t0);\r
 777     ((#4.0), x5C, square_2t0);\r
 778     ((#4.0), x6C, square_2t0);\r
 779     ((#4.0), x2D, square_2t0);\r
 780     ((#4.0), x3D, square_2t0);\r
 781     ((#4.0), x4D, square_2t0);\r
 782     ((#4.0), x5D, square_2t0);\r
 783     ((#4.0), x6D, square_2t0)]\r
 784       (((sigma_qrtet_x x1 x2A x3A x4A x5A x6A) +. \r
 785        (sigma_qrtet_x x1 x2B x3B x4B x5B x6B) +.\r
 786        (sigma_qrtet_x x1 x2C x3C x4C x5C x6C) +.\r
 787       (sigma_qrtet_x x1 x2D x3D x4D x5D x6D) <. (#0.33) *. pt) \/\r
 788        ((dih_x x1 x2A x3A x4A x5A x6A) +.\r
 789           (dih_x x1 x2B x3B x4B x5B x6B) +.\r
 790          (dih_x x1 x2C x3C x4C x5C x6C) +.\r
 791          (dih_x x1 x2D x3D x4D x5D x6D)  <. (#2.0) *. pi\r
 792     )))`;;\r
 793 \r
 794 (*\r
 795  \r
 796 LOC: 2002 k.c page 52--53\r
 797 17.28 Group_28\r
 798 *)\r
 799 \r
 800 (* interval verification by Ferguson *)\r
 801 let I_615073260=\r
 802   all_forall \r
 803   `\r
 804 let x6B = x5A in\r
 805 let x2B = x3A in\r
 806 let x6C = x5B in\r
 807 let x2C = x3B in\r
 808 let x6D = x5C in\r
 809 let x2D = x3C in\r
 810 let x6E = x5D in\r
 811 let x2E = x3D in\r
 812 let x6A = x5E in\r
 813 let x2A = x3E in\r
 814    (ineq\r
 815    [((#4.0), x1, square_2t0);\r
 816     ((#4.0), x2A, square_2t0);\r
 817     ((#4.0), x3A, square_2t0);\r
 818     ((#4.0), x4A, square_2t0);\r
 819     ((#4.0), x5A, square_2t0);\r
 820     ((#4.0), x6A, square_2t0);\r
 821     ((#4.0), x2B, square_2t0);\r
 822     ((#4.0), x3B, square_2t0);\r
 823     ((#4.0), x4B, square_2t0);\r
 824     ((#4.0), x5B, square_2t0);\r
 825     ((#4.0), x6B, square_2t0);\r
 826     ((#4.0), x2C, square_2t0);\r
 827     ((#4.0), x3C, square_2t0);\r
 828     ((#4.0), x4C, square_2t0); \r
 829     ((#4.0), x5C, square_2t0);\r
 830     ((#4.0), x6C, square_2t0);\r
 831     ((#4.0), x2D, square_2t0);\r
 832     ((#4.0), x3D, square_2t0);\r
 833     ((#4.0), x4D, square_2t0);\r
 834     ((#4.0), x5D, square_2t0);\r
 835     ((#4.0), x6D, square_2t0);\r
 836     ((#4.0), x2E, square_2t0);\r
 837     ((#4.0), x3E, square_2t0);\r
 838     ((square_2t0), x4E, (square_4t0)); // (* NB *) \r
 839     ((#4.0), x5E, square_2t0);\r
 840     ((#4.0), x6E, square_2t0)]\r
 841       ((sqrt x2A) + (sqrt x2B) + (sqrt x2C) + (sqrt x2D) + (sqrt x2E) +\r
 842        (sqrt x6A) + (sqrt x6B) + (sqrt x6C) + (sqrt x6D) + (sqrt x6E) >. (#20.42)))`;;\r
 843 \r
 844 (* interval verification by Ferguson *)\r
 845 let I_844430737=\r
 846   all_forall \r
 847   `\r
 848 let x6B = x5A in\r
 849 let x2B = x3A in\r
 850 let x6C = x5B in\r
 851 let x2C = x3B in\r
 852 let x6D = x5C in\r
 853 let x2D = x3C in\r
 854 let x6E = x5D in\r
 855 let x2E = x3D in\r
 856 let x6A = x5E in\r
 857 let x2A = x3E in\r
 858    (ineq\r
 859    [((#4.0), x1, square_2t0);\r
 860     ((#4.0), x2A, square_2t0);\r
 861     ((#4.0), x3A, square_2t0);\r
 862     ((#4.0), x4A, square_2t0);\r
 863     ((#4.0), x5A, square_2t0);\r
 864     ((#4.0), x6A, square_2t0);\r
 865     ((#4.0), x2B, square_2t0);\r
 866     ((#4.0), x3B, square_2t0);\r
 867     ((#4.0), x4B, square_2t0);\r
 868     ((#4.0), x5B, square_2t0);\r
 869     ((#4.0), x6B, square_2t0);\r
 870     ((#4.0), x2C, square_2t0);\r
 871     ((#4.0), x3C, square_2t0);\r
 872     ((#4.0), x4C, square_2t0); \r
 873     ((#4.0), x5C, square_2t0);\r
 874     ((#4.0), x6C, square_2t0);\r
 875     ((#4.0), x2D, square_2t0);\r
 876     ((#4.0), x3D, square_2t0);\r
 877     ((#4.0), x4D, square_2t0);\r
 878     ((#4.0), x5D, square_2t0);\r
 879     ((#4.0), x6D, square_2t0);\r
 880     ((#4.0), x2E, square_2t0);\r
 881     ((#4.0), x3E, square_2t0);\r
 882     ((#8.0), x4E, (square_4t0)); // (* NB *) \r
 883     ((#4.0), x5E, square_2t0);\r
 884     ((#4.0), x6E, square_2t0)]\r
 885       ((sqrt x2A) + (sqrt x2B) + (sqrt x2C) + (sqrt x2D) + (sqrt x2E) +\r
 886        (sqrt x6A) + (sqrt x6B) + (sqrt x6C) + (sqrt x6D) + (sqrt x6E) >. (#20.76)))`;;\r
 887 \r
 888 \r
 889 (* Duplicate inequality.  This is the same as 413688580 *)\r
 890 (*\r
 891 let J_549774315_1=\r
 892    all_forall `ineq \r
 893     [(square_2t0, x1, (#8.0));\r
 894      ((#4.0), x2, square_2t0);\r
 895      ((#4.0), x3, square_2t0);\r
 896      ((#4.0), x4, square_2t0);\r
 897      ((#4.0), x5, square_2t0);\r
 898      ((#4.0), x6, square_2t0)\r
 899     ]\r
 900     (\r
 901                 ( (nu_x x1 x2 x3 x4 x5 x6) +.  (  (--. (#4.10113)) *.  (dih_x x1 x2 x3 x4 x5 x6))) <.  (--. (#4.3223)))`;;\r
 902 *)\r
 903 \r
 904 \r
 905 (* Duplicate inequality.  This is the same as 805296510 *)\r
 906 (*\r
 907 let J_549774315_2=\r
 908    all_forall `ineq \r
 909     [(square_2t0, x1, (#8.0));\r
 910      ((#4.0), x2, square_2t0);\r
 911      ((#4.0), x3, square_2t0);\r
 912      ((#4.0), x4, square_2t0);\r
 913      ((#4.0), x5, square_2t0);\r
 914      ((#4.0), x6, square_2t0)\r
 915     ]\r
 916     (\r
 917                 ( (nu_x x1 x2 x3 x4 x5 x6) +.  (  (--. (#0.80449)) *.  (dih_x x1 x2 x3 x4 x5 x6))) <.  (--. (#0.9871)))`;;\r
 918 *)\r
 919 \r
 920 (* Duplicate inequality.  This is the same as 136610219 *)\r
 921 (*\r
 922 let J_549774315_3=\r
 923    all_forall `ineq \r
 924     [(square_2t0, x1, (#8.0));\r
 925      ((#4.0), x2, square_2t0);\r
 926      ((#4.0), x3, square_2t0);\r
 927      ((#4.0), x4, square_2t0);\r
 928      ((#4.0), x5, square_2t0);\r
 929      ((#4.0), x6, square_2t0)\r
 930     ]\r
 931     (\r
 932                 ( (nu_x x1 x2 x3 x4 x5 x6) +.  (  (--. (#0.70186)) *.  (dih_x x1 x2 x3 x4 x5 x6))) <.  (--. (#0.8756)))`;;\r
 933 *)\r
 934 \r
 935 (* Duplicate inequality.  This is the same as 379204810 *)\r
 936 (*\r
 937 let J_549774315_4=\r
 938    all_forall `ineq \r
 939     [(square_2t0, x1, (#8.0));\r
 940      ((#4.0), x2, square_2t0);\r
 941      ((#4.0), x3, square_2t0);\r
 942      ((#4.0), x4, square_2t0);\r
 943      ((#4.0), x5, square_2t0);\r
 944      ((#4.0), x6, square_2t0)\r
 945     ]\r
 946     (\r
 947                 ( (nu_x x1 x2 x3 x4 x5 x6) +.  (  (--. (#0.24573)) *.  (dih_x x1 x2 x3 x4 x5 x6))) <.  (--. (#0.3404)))`;;\r
 948 *)\r
 949 \r
 950 (* Duplicate inequality.  This is the same as 878731435 *)\r
 951 (*\r
 952 let J_549774315_5=\r
 953    all_forall `ineq \r
 954     [(square_2t0, x1, (#8.0));\r
 955      ((#4.0), x2, square_2t0);\r
 956      ((#4.0), x3, square_2t0);\r
 957      ((#4.0), x4, square_2t0);\r
 958      ((#4.0), x5, square_2t0);\r
 959      ((#4.0), x6, square_2t0)\r
 960     ]\r
 961     (\r
 962                 ( (nu_x x1 x2 x3 x4 x5 x6) +.  (  (--. (#0.00154)) *.  (dih_x x1 x2 x3 x4 x5 x6))) <.  (--. (#0.0024)))`;;\r
 963 *)\r
 964 \r
 965 (* Duplicate inequality.  This is the same as 891740103 *)\r
 966 (*\r
 967 let J_549774315_6=\r
 968    all_forall `ineq \r
 969     [(square_2t0, x1, (#8.0));\r
 970      ((#4.0), x2, square_2t0);\r
 971      ((#4.0), x3, square_2t0);\r
 972      ((#4.0), x4, square_2t0);\r
 973      ((#4.0), x5, square_2t0);\r
 974      ((#4.0), x6, square_2t0)\r
 975     ]\r
 976     (\r
 977                 ( (nu_x x1 x2 x3 x4 x5 x6) +.  (  (#0.07611) *.  (dih_x x1 x2 x3 x4 x5 x6))) <.  (#0.1196))`;;\r
 978 *)\r
 979 \r
 980 (* Duplicate inequality.  This is the same as 334002329 *)\r
 981 (*\r
 982 let J_574435320_1=\r
 983    all_forall `ineq \r
 984     [(square_2t0, x1, (#8.0));\r
 985      ((#4.0), x2, square_2t0);\r
 986      ((#4.0), x3, square_2t0);\r
 987      ((#4.0), x4, square_2t0);\r
 988      ((#4.0), x5, square_2t0);\r
 989      ((#4.0), x6, square_2t0)\r
 990     ]\r
 991     (\r
 992                 ( (taunu_x x1 x2 x3 x4 x5 x6) +.  (  (#4.16523) *.  (dih_x x1 x2 x3 x4 x5 x6))) >.  (#4.42873))`;;\r
 993 *)\r
 994 \r
 995 (* Duplicate inequality.  This is the same as 883139937 *)\r
 996 (*\r
 997 let J_574435320_2=\r
 998    all_forall `ineq \r
 999     [(square_2t0, x1, (#8.0));\r
1000      ((#4.0), x2, square_2t0);\r
1001      ((#4.0), x3, square_2t0);\r
1002      ((#4.0), x4, square_2t0);\r
1003      ((#4.0), x5, square_2t0);\r
1004      ((#4.0), x6, square_2t0)\r
1005     ]\r
1006     (\r
1007                 ( (taunu_x x1 x2 x3 x4 x5 x6) +.  (  (#0.78701) *.  (dih_x x1 x2 x3 x4 x5 x6))) >.  (#1.01104))`;;\r
1008 *)\r
1009 \r
1010 (* Duplicate inequality.  This is the same as 507989176 *)\r
1011 (*\r
1012 let J_574435320_3=\r
1013    all_forall `ineq \r
1014     [(square_2t0, x1, (#8.0));\r
1015      ((#4.0), x2, square_2t0);\r
1016      ((#4.0), x3, square_2t0);\r
1017      ((#4.0), x4, square_2t0);\r
1018      ((#4.0), x5, square_2t0);\r
1019      ((#4.0), x6, square_2t0)\r
1020     ]\r
1021     (\r
1022                 ( (taunu_x x1 x2 x3 x4 x5 x6) +.  (  (#0.77627) *.  (dih_x x1 x2 x3 x4 x5 x6))) >.  (#0.99937))`;;\r
1023 *)\r
1024 \r
1025 (* Duplicate inequality.  This is the same as 244435805 *)\r
1026 (*\r
1027 let J_574435320_4=\r
1028    all_forall `ineq \r
1029     [(square_2t0, x1, (#8.0));\r
1030      ((#4.0), x2, square_2t0);\r
1031      ((#4.0), x3, square_2t0);\r
1032      ((#4.0), x4, square_2t0);\r
1033      ((#4.0), x5, square_2t0);\r
1034      ((#4.0), x6, square_2t0)\r
1035     ]\r
1036     (\r
1037                 ( (taunu_x x1 x2 x3 x4 x5 x6) +.  (  (#0.21916) *.  (dih_x x1 x2 x3 x4 x5 x6))) >.  (#0.34877))`;;\r
1038 *)\r
1039 \r
1040 (* Duplicate inequality.  This is the same as 930176500 *)\r
1041 (*\r
1042 let J_574435320_5=\r
1043    all_forall `ineq \r
1044     [(square_2t0, x1, (#8.0));\r
1045      ((#4.0), x2, square_2t0);\r
1046      ((#4.0), x3, square_2t0);\r
1047      ((#4.0), x4, square_2t0);\r
1048      ((#4.0), x5, square_2t0);\r
1049      ((#4.0), x6, square_2t0)\r
1050     ]\r
1051     (\r
1052                 ( (taunu_x x1 x2 x3 x4 x5 x6) +.  (  (#0.05107) *.  (dih_x x1 x2 x3 x4 x5 x6))) >.  (#0.11434))`;;\r
1053 *)\r
1054 \r
1055 (* Duplicate inequality.  This is the same as 815681339 *)\r
1056 (*\r
1057 let J_574435320_6=\r
1058    all_forall `ineq \r
1059     [(square_2t0, x1, (#8.0));\r
1060      ((#4.0), x2, square_2t0);\r
1061      ((#4.0), x3, square_2t0);\r
1062      ((#4.0), x4, square_2t0);\r
1063      ((#4.0), x5, square_2t0);\r
1064      ((#4.0), x6, square_2t0)\r
1065     ]\r
1066     (\r
1067                 ( (taunu_x x1 x2 x3 x4 x5 x6) +.  (  (--. (#0.07106)) *.  (dih_x x1 x2 x3 x4 x5 x6))) >.  (--. (#0.07749)))`;;\r
1068 *)\r
1069 \r
1070 (* \r
1071 This was false for strict inequality.\r
1072 gives equality at [8,4,4,8,4,4].\r
1073 It is trivially true when weak inequality is used, because dih(simplex)<=pi\r
1074 without any constraints on the simplex.  So we don't need interval arithmetic\r
1075 for its verification.  Commented out.\r
1076 *)\r
1077 (* \r
1078 let I_853728973_24=\r
1079    all_forall `ineq \r
1080     [(square_2t0, x1, (#8.0));\r
1081      ((#4.0), x2, square_2t0);\r
1082      ((#4.0), x3, square_2t0);\r
1083      (square_2t0, x4, (#8.0));\r
1084      ((#4.0), x5, square_2t0);\r
1085      ((#4.0), x6, square_2t0)\r
1086     ]\r
1087     ( (dih_x x1 x2 x3 x4 x5 x6) <=.  pi)`;;\r
1088 *)\r
1089 \r
1090 \r
1091 \r
1092 (* \r
1093 dih < pi is false\r
1094 gives equality at [8,4,4,8,4,4].\r
1095 See comments for I_853728973_24.\r
1096 *)\r
1097 \r
1098 (*\r
1099 let I_853728973_26=\r
1100    all_forall `ineq \r
1101     [(square_2t0, x1, (#8.0));\r
1102      ((#4.0), x2, square_2t0);\r
1103      ((#4.0), x3, square_2t0);\r
1104      (square_2t0, x4, square_4t0);\r
1105      ((#4.0), x5, square_2t0);\r
1106      ((#4.0), x6, square_2t0)\r
1107     ]\r
1108     ( (dih_x x1 x2 x3 x4 x5 x6) <=.  pi)`;;\r
1109 *)\r
1110 \r
1111 \r
1112 (* \r
1113 dih < pi is false\r
1114 gives equality at [8,4,4,8,4,4].\r
1115 Interval verification not needed.\r
1116 See comments for I_853728973_24.\r
1117 *)\r
1118 \r
1119 (*\r
1120 let I_853728973_28=\r
1121    all_forall `ineq \r
1122     [(square_2t0, x1, (#8.0));\r
1123      ((#4.0), x2, square_2t0);\r
1124      ((#4.0), x3, square_2t0);\r
1125      ((#8.0), x4, square_4t0);\r
1126      ((#4.0), x5, square_2t0);\r
1127      ((#4.0), x6, square_2t0)\r
1128     ]\r
1129     ( (dih_x x1 x2 x3 x4 x5 x6) <=.  pi)`;;\r
1130 *)\r
1131 \r
1132 \r
1133 (* \r
1134 dih > 0 is false\r
1135 gives equality at [4,4,8,4,4,8]\r
1136 Interval verification not needed, \r
1137 since dih is always >= 0.\r
1138 See comments for I_853728973_24.\r
1139 *)\r
1140 \r
1141 (*\r
1142 let I_853728973_33=\r
1143    all_forall `ineq \r
1144     [((#4.0), x1, square_2t0);\r
1145      ((#4.0), x2, square_2t0);\r
1146      (square_2t0, x3, (#8.0));\r
1147      ((#4.0), x4, square_2t0);\r
1148      ((#4.0), x5, square_2t0);\r
1149      (square_2t0, x6, (#8.0))\r
1150     ]\r
1151     ( (dih_x x1 x2 x3 x4 x5 x6) =>.  (#0.0))`;;\r
1152 *)\r