1 (* inequalities used in the text part of the kepler conjecture *)
3 (* They are not ALL listed here.
5 The following are in kep_inequalities2.ml
16 The following need to be moved here, but they are composites
17 of several inequalites.
48 parse_as_infix("+.",(16,"right"));
49 parse_as_infix("-.",(18,"left"));
50 parse_as_infix("*.",(20,"right"));
51 parse_as_infix("**.",(24,"left"));
52 parse_as_infix("<.",(12,"right"));
53 parse_as_infix("<=.",(12,"right"));
54 parse_as_infix(">.",(12,"right"));
55 parse_as_infix(">=.",(12,"right"));
56 override_interface("+.",`real_add:real->real->real`);
57 override_interface("-.",`real_sub:real->real->real`);
58 override_interface("*.",`real_mul:real->real->real`);
59 override_interface("**.",`real_pow:real->num->real`);
61 override_interface("<.",`real_lt:real->real->bool`);
62 override_interface("<=.",`real_le:real->real->bool`);
63 override_interface(">.",`real_gt:real->real->bool`);
64 override_interface(">=.",`real_ge:real->real->bool`);
66 override_interface("--.",`real_neg:real->real`);
67 override_interface("&.",`real_of_num:num->real`);
68 override_interface("||.",`real_abs:real->real`);;
73 [((#4.0), x1, square_2t0);
74 ((#4.0), x2, (square (#2.168)));
75 ((#4.0), x3, (square (#2.168)));
76 ((#4.0), x4, square_2t0);
77 (square_2t0, x5, square_2t0);
78 (square_2t0, x6, square_4t0)
80 ( (dih_x x1 x2 x3 x4 x5 x6) <. (#1.51) \/
81 (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0)) `;;
86 [((#4.0), x1, square_2t0);
87 ((#4.0), x2, square_2t0)
89 ( (overlap_f (sqrt x1) (sqrt x2)) >. (#0.887))`;;
93 [((#4.0), x1, square_2t0);
94 ((#4.0), x2, (square (#2.168)));
95 ((#4.0), x3, (square (#2.168)));
97 (square_2t0, x5, square_2t0);
98 (square_2t0, x6, square_4t0)
100 ( (dih_x x1 x2 x3 x4 x5 x6) <. (#1.77) \/
101 (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0))`;;
106 [((#4.0), x1, square_2t0);
107 ((#4.0), x2, (square (#2.168)));
108 ((#4.0), x3, (square (#2.168)));
109 (square_2t0, x4, (#8.0));
110 (square_2t0, x5, square_2t0);
111 (square_2t0, x6, square_4t0)
115 ( (tau_0_x x1 x2 x3 x4 x5 x6) -. ( (#0.2529) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (--. (#0.12))) \/
116 ( (dih_x x1 x2 x3 x4 x5 x6) <. (#1.2)) \/
117 (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0))`;;
123 [(square_2t0, x1, (#8.0));
124 ((#4.0), x2, square_2t0);
125 ((#4.0), x3, square_2t0);
126 ((#4.0), x4, square_2t0);
127 ((#4.0), x5, square_2t0);
128 ((#4.0), x6, square_2t0)
130 ( ( (mu_upright_x x1 x2 x3 x4 x5 x6) +.
131 ( (--. (#0.1378)) *. ( (#1.0) +. ( (( --. ) (dih_x x1 x2 x3 x4 x5 x6)) / ( (#2.0) *. pi)))) +.
132 ( (#2.0) *. (#0.0263))) <.
133 (vor_0_x x1 x2 x3 x4 x5 x6))`;;
138 [((#4.0), x1, square_2t0);
139 ((#4.0), x2, square_2t0);
140 ((#4.0), x3, square_2t0);
142 ((#4.0), x4, square_2t0);
143 ((#4.0), x5, square_2t0);
144 ((#4.0), x6, square_2t0)
146 ( (dih_x x1 x2 x3 x4 x5 x6) >. (#0.8638))`;;
152 ((#4.0),x1,square_2t0);
153 ((#4.0),x2,square_2t0);
154 ((#4.0),x3,square_2t0);
156 ((#4.0),x5,square_2t0);
159 (((x1 pow 5)*x4 - (&2)*(x1 pow 4)*x2*x4 + (x1 pow 3)*(x2 pow 2)*x4 - (&2)*(x1 pow 4)*x3*x4 +
160 (&4)*(x1 pow 3)*x2*x3*x4 - (&2)*(x1 pow 2)*(x2 pow 2)*x3*x4 + (x1 pow 3)*(x3 pow 2)*x4 -
161 (&2)*(x1 pow 2)*x2*(x3 pow 2)*x4 + x1*(x2 pow 2)*(x3 pow 2)*x4 - (x1 pow 4)*x2*x5 +
162 (&2)*(x1 pow 3)*(x2 pow 2)*x5 - (x1 pow 2)*(x2 pow 3)*x5 + (x1 pow 4)*x3*x5 -
163 (x1 pow 3)*x2*x3*x5 - (x1 pow 2)*(x2 pow 2)*x3*x5 + x1*(x2 pow 3)*x3*x5 -
164 (x1 pow 3)*(x3 pow 2)*x5 + (&2)*(x1 pow 2)*x2*(x3 pow 2)*x5 -
165 x1*(x2 pow 2)*(x3 pow 2)*x5 - (&2)*(x1 pow 4)*x4*x5 + (&4)*(x1 pow 3)*x2*x4*x5 -
166 (&2)*(x1 pow 2)*(x2 pow 2)*x4*x5 + (&2)*(x1 pow 3)*x2*(x5 pow 2) -
167 (&4)*(x1 pow 2)*(x2 pow 2)*(x5 pow 2) + (&2)*x1*(x2 pow 3)*(x5 pow 2) -
168 (x1 pow 3)*x3*(x5 pow 2) + (&3)*(x1 pow 2)*x2*x3*(x5 pow 2) -
169 (&3)*x1*(x2 pow 2)*x3*(x5 pow 2) + (x2 pow 3)*x3*(x5 pow 2) + (x1 pow 3)*x4*(x5 pow 2) -
170 (&2)*(x1 pow 2)*x2*x4*(x5 pow 2) + x1*(x2 pow 2)*x4*(x5 pow 2) -
171 (x1 pow 2)*x2*(x5 pow 3) + (&2)*x1*(x2 pow 2)*(x5 pow 3) - (x2 pow 3)*(x5 pow 3) +
172 (x1 pow 4)*x2*x6 - (x1 pow 3)*(x2 pow 2)*x6 - (x1 pow 4)*x3*x6 - (x1 pow 3)*x2*x3*x6 +
173 (&2)*(x1 pow 2)*(x2 pow 2)*x3*x6 + (&2)*(x1 pow 3)*(x3 pow 2)*x6 -
174 (x1 pow 2)*x2*(x3 pow 2)*x6 - x1*(x2 pow 2)*(x3 pow 2)*x6 - (x1 pow 2)*(x3 pow 3)*x6 +
175 x1*x2*(x3 pow 3)*x6 - (&2)*(x1 pow 4)*x4*x6 + (&4)*(x1 pow 3)*x3*x4*x6 -
176 (&2)*(x1 pow 2)*(x3 pow 2)*x4*x6 - (x1 pow 3)*x2*x5*x6 + (&3)*(x1 pow 2)*(x2 pow 2)*x5*x6 -
177 (x1 pow 3)*x3*x5*x6 - (&4)*(x1 pow 2)*x2*x3*x5*x6 + x1*(x2 pow 2)*x3*x5*x6 +
178 (&3)*(x1 pow 2)*(x3 pow 2)*x5*x6 + x1*x2*(x3 pow 2)*x5*x6 -
179 (&2)*(x2 pow 2)*(x3 pow 2)*x5*x6 + (&4)*(x1 pow 3)*x4*x5*x6 - (&4)*x1*x2*x3*x4*x5*x6 -
180 (x1 pow 2)*x2*(x5 pow 2)*x6 - (&3)*x1*(x2 pow 2)*(x5 pow 2)*x6 +
181 (&2)*(x1 pow 2)*x3*(x5 pow 2)*x6 + x1*x2*x3*(x5 pow 2)*x6 + (x2 pow 2)*x3*(x5 pow 2)*x6 -
182 (&2)*(x1 pow 2)*x4*(x5 pow 2)*x6 + x1*x2*(x5 pow 3)*x6 + (x2 pow 2)*(x5 pow 3)*x6 -
183 (x1 pow 3)*x2*(x6 pow 2) + (&2)*(x1 pow 3)*x3*(x6 pow 2) +
184 (&3)*(x1 pow 2)*x2*x3*(x6 pow 2) - (&4)*(x1 pow 2)*(x3 pow 2)*(x6 pow 2) -
185 (&3)*x1*x2*(x3 pow 2)*(x6 pow 2) + (&2)*x1*(x3 pow 3)*(x6 pow 2) +
186 x2*(x3 pow 3)*(x6 pow 2) + (x1 pow 3)*x4*(x6 pow 2) - (&2)*(x1 pow 2)*x3*x4*(x6 pow 2) +
187 x1*(x3 pow 2)*x4*(x6 pow 2) + (&2)*(x1 pow 2)*x2*x5*(x6 pow 2) -
188 (x1 pow 2)*x3*x5*(x6 pow 2) + x1*x2*x3*x5*(x6 pow 2) - (&3)*x1*(x3 pow 2)*x5*(x6 pow 2) +
189 x2*(x3 pow 2)*x5*(x6 pow 2) - (&2)*(x1 pow 2)*x4*x5*(x6 pow 2) -
190 x1*x2*(x5 pow 2)*(x6 pow 2) - x1*x3*(x5 pow 2)*(x6 pow 2) -
191 (&2)*x2*x3*(x5 pow 2)*(x6 pow 2) + x1*x4*(x5 pow 2)*(x6 pow 2) -
192 (x1 pow 2)*x3*(x6 pow 3) + (&2)*x1*(x3 pow 2)*(x6 pow 3) - (x3 pow 3)*(x6 pow 3) +
193 x1*x3*x5*(x6 pow 3) + (x3 pow 2)*x5*(x6 pow 3)) < (#0.0))`;;
198 [((#4.0), x1, square_2t0);
199 ((#4.0), x2, square_2t0);
200 ((#4.0), x3, square_2t0);
201 ((square (#2.177303)), x4, square_2t0);
202 ((#4.0), x5, square_2t0);
203 ((#4.0), x6, square_2t0)
205 ( (sigma_qrtet_x x1 x2 x3 x4 x5 x6) <. ( #0.028794285 ))`;;
210 [((#4.0), x1, square_2t0);
211 ((#4.0), x2, (square (#2.168)));
212 ((#4.0), x3, (square (#2.168)));
213 ((#4.0), x4, square_2t0);
214 (square_2t0, x5, (square (#3.488)));
215 (square_2t0, x6, square_2t0)
218 ( (tau_0_x x1 x2 x3 x4 x5 x6) -. ( (#0.2529) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (--. (#0.1453)))`;;
222 [((#4.0), x1, square_2t0);
223 ((#4.0), x2, square_2t0);
224 ((#4.0), x3, square_2t0);
226 (square_2t0, x4, (#8.0));
227 ((#4.0), x5, square_2t0);
228 ((#4.0), x6, square_2t0)
231 ( (gamma_x x1 x2 x3 x4 x5 x6) <=. (#0.0)) \/
232 ( (eta_x x1 x2 x6) >. (#2.0)) \/
233 ( (eta_x x2 x3 x4) >. (#2.0)) \/
234 ( (eta_x x1 x3 x5) >. (#2.0)) \/
235 ( (eta_x x4 x5 x6) >. (#2.0)))`;;
239 [(square_2t0, x1, (#8.0));
240 ((#4.0), x2, square_2t0);
241 ((#4.0), x3, square_2t0);
243 ((#4.0), x4, square_2t0);
244 ((#4.0), x5, square_2t0);
245 ((#4.0), x6, square_2t0)
247 ( (vor_analytic_x x1 x2 x3 x4 x5 x6) <=. (#0.0))`;;
251 [((#4.0), x1, square_2t0);
252 ((#4.0), x2, (square (#2.168)));
253 ((#4.0), x3, (square (#2.168)));
254 ((#4.0), x4, square_2t0);
255 (square_2t0, x5, square_2t0);
256 (square_2t0, x6, square_4t0)
260 ( (tau_0_x x1 x2 x3 x4 x5 x6) -. ( (#0.2529) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (--. (#0.1376))) \/
261 ( (dih_x x1 x2 x3 x4 x5 x6) <. (#1.2)) \/
262 (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0))`;;
267 [(square_2t0, x1, (#8.0));
268 ((#4.0), x2, square_2t0);
269 ((#4.0), x3, square_2t0);
271 ((#4.0), x4, square_2t0);
272 ((#4.0), x5, square_2t0);
273 ((#4.0), x6, square_2t0)
275 ( ( ( (#2.0) *. (gamma_x x1 x2 x3 x4 x5 x6)) +.
276 (vor_0_x x1 x2 x3 x4 x5 x6) +.
277 (( --. ) (vor_0_x_flipped x1 x2 x3 x4 x5 x6))) <=. (#0.0))`;;
282 [((#4.0), x1, square_2t0);
283 ((#4.0), x2, square_2t0);
284 ((#4.0), x3, square_2t0);
285 ((#4.0), x4, square_2t0);
286 ((#4.0), x5, square_2t0);
287 ((#4.0), x6, square_2t0)
289 ( (sigma1_qrtet_x x1 x2 x3 x4 x5 x6) <=. (#0.0))`;;
293 [((square (#2.3)), x1, square_2t0);
294 ((#4.0), x2, square_2t0);
295 ((#4.0), x3, square_2t0);
296 ((#4.0), x4, square_2t0);
297 (square_2t0, x5, (square (#3.02)));
298 (square_2t0, x6, (square (#3.02)))
302 ( (tau_0_x x1 x2 x3 x4 x5 x6) -. ( (#0.2529) *. (dih_x x1 x2 x3 x4 x5 x6))) >.
304 ( (dih_x x1 x2 x3 x4 x5 x6) <. (#1.14)) \/
305 ( (dih_x x1 x2 x3 x4 x5 x6) >. (#1.51)))`;;
310 (square_2t0, x1, (#8.0));
311 ((#4.0), x2, square_2t0);
312 ((#4.0), x3, square_2t0);
313 ((#4.0), x4,square_2t0);
314 ((#4.0), x5, square_2t0);
315 ((#4.0), x6, square_2t0)
317 ( ( (mu_upright_x x1 x2 x3 x4 x5 x6) +. (mu_flipped_x x1 x2 x3 x4 x5 x6) +.
318 ( (crown ( (sqrt x1) / (#2.0))) *. ( (#1.0) +. ( (( --. ) (dih_x x1 x2 x3 x4 x5 x6)) / pi))) +.
319 ( (#2.0) *. (anc (sqrt x1) (sqrt x2) (sqrt x6)))) <.
320 ( (vor_0_x x1 x2 x3 x4 x5 x6) +. (vor_0_x_flipped x1 x2 x3 x4 x5 x6)))`;;
324 [((#4.0), x1, square_2t0);
325 ((square (#2.3)), x2, square_2t0);
326 ((#4.0), x3, square_2t0);
327 (square_2t0, x4, (#8.0));
328 ((#4.0), x5, square_2t0);
329 ((#4.0), x6, square_2t0)
332 ( (tauhat_x x1 x2 x3 x4 x5 x6) -. ( (#0.2529) *. (dih2_x x1 x2 x3 x4 x5 x6))) >.
337 [((square (#2.3)), x1, (#6.3001));
338 ((#4.0), x2, (#6.3001));
339 ((#4.0), x3, (#6.3001));
340 ((#4.0), x4, (#6.3001));
341 ((#4.0), x5, (#6.3001));
342 ((#4.0), x6, (#6.3001))
346 ( (tau_sigma_x x1 x2 x3 x4 x5 x6) -. ( (#0.2529) *. (dih_x x1 x2 x3 x4 x5 x6))) >.
348 ( (dih_x x1 x2 x3 x4 x5 x6) <. (#1.51)))`;;
352 [((#4.0), x1, square_2t0);
353 ((#4.0), x2, (square (#2.168)));
354 ((#4.0), x3, (square (#2.168)));
355 ((#8.0), x4, (#8.0));
356 ((#4.0), x5, square_2t0);
357 (square_2t0, x6, square_4t0)
359 ( (dih_x x1 x2 x3 x4 x5 x6) <. (#1.93) \/
360 (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0))`;;
364 [((#4.0), x1, square_2t0);
365 ((#4.0), x2, square_2t0);
366 ((#4.0), x3, square_2t0);
368 ((#4.0), x4, square_2t0);
369 ((#4.0), x5, square_2t0);
370 ((#4.0), x6, square_2t0)
372 ( (sigma_qrtet_x x1 x2 x3 x4 x5 x6) <=. pt)`;;
376 [((#4.0), x1, square_2t0);
377 ((#4.0), x2, square_2t0);
378 ((#4.0), x3, square_2t0);
380 (square_2t0, x4, (#8.0));
381 (square_2t0, x5, (#8.0));
382 (square_2t0, x6, (#8.0))
385 ( (vor_analytic_x x1 x2 x3 x4 x5 x6) <. (#0.0)) \/
386 ( (eta_x x1 x2 x6) >. (sqrt (#2.0))) \/
387 ( (eta_x x2 x3 x4) >. (sqrt (#2.0))) \/
388 ( (eta_x x1 x3 x5) >. (sqrt (#2.0))) \/
389 ( (eta_x x4 x5 x6) >. (sqrt (#2.0))))`;;
393 [((#4.0), x2, square_2t0);
394 ((#4.0), x3, square_2t0);
395 ((#4.0), x4, square_2t0);
396 (square_2t0, x1, (#8.0));
397 ((#4.0), x5, square_2t0);
398 ((#4.0), x6, square_2t0)
400 (( (vor_analytic_x x1 x2 x3 x4 x5 x6) <=. (#0.0)) \/
401 (chi_x x5 x6 x1 x2 x3 x4 >. (#0.0) ))`;;
405 [((#4.0), x1, square_2t0);
406 ((#4.0), x2, (square (#2.168)));
407 ((#4.0), x3, (square (#2.168)));
408 ((#4.0), x4, (#4.0));
409 (square_2t0, x5, square_2t0);
410 (square_2t0, x6, square_4t0)
412 ( (dih_x x1 x2 x3 x4 x5 x6) <. (#1.16) \/
413 (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0))`;;
419 [((#4.0), x1, square_2t0);
420 ((#4.0), x2, (square (#2.168)));
421 ((#4.0), x3, (square (#2.168)));
422 (square_2t0, x4, (#8.0));
423 ((#4.0), x5, square_2t0);
424 (square_2t0, x6, square_4t0)
428 ( (tau_0_x x1 x2 x3 x4 x5 x6) -. ( (#0.2529) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (--. (#0.266))) \/
429 ( (dih_x x1 x2 x3 x4 x5 x6) <. (#1.2)) \/
430 (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0))`;;
435 [(square_2t0, x1, (#8.0));
436 ((#4.0), x2, square_2t0);
437 ((#4.0), x3, square_2t0);
438 ((#4.0), x4, square_2t0);
440 (square_2t0, x5, (#8.0));
441 ((#4.0), x6, square_2t0)
444 ( (vor_analytic_x x1 x2 x3 x4 x5 x6) <. (#0.0)) \/
445 ( (eta_x x1 x2 x6) >. (sqrt (#2.0))) \/
446 ( (eta_x x2 x3 x4) >. (sqrt (#2.0))) \/
447 ( (eta_x x1 x3 x5) >. (sqrt (#2.0))) \/
448 ( (eta_x x4 x5 x6) >. (sqrt (#2.0))))`;;
453 [((#4.0), x1, square_2t0);
454 ((#4.0), x2, (square (#2.168)));
455 ((#4.0), x3, (square (#2.168)));
456 ((#4.0), x4, square_2t0);
457 ((#4.0), x5, square_2t0);
458 (square_2t0, x6, square_4t0)
462 ( (tau_0_x x1 x2 x3 x4 x5 x6) -. ( (#0.2529) *. (dih_x x1 x2 x3 x4 x5 x6))) >. (--. (#0.2391))) \/
463 ( (dih_x x1 x2 x3 x4 x5 x6) <. (#1.2)) \/
464 (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0))`;;
468 [((#4.0), x1, square_2t0);
469 ((#4.0), x2, (square (#2.168)));
470 ((#4.0), x3, (square (#2.168)));
471 ((#4.0), x4, square_2t0);
472 (square_2t0, x5, square_4t0);
473 ((#4.0), x6, square_2t0)
475 ( ( (dih_x x1 x2 x3 x4 x5 x6) +. ( (#0.5) *. ( (#2.402) -. (sqrt x4)))) <. ( pi / (#2.0)) \/
476 (delta_x x1 x2 x3 x4 x5 x6 < (#0.0)))`;;
478 let I_69064028=I_690646028;; (* because of a typo *)
483 [(square_2t0, x1, (#8.0));
484 ((#4.0), x2, square_2t0);
485 ((#4.0), x6, square_2t0)
487 ( (anc (sqrt x1) (sqrt x2) (sqrt x6)) <. (#0.0263))`;;
491 [((square (#2.3)), x1, (#6.3001));
492 ((#4.0), x2, (#6.3001));
493 ((#4.0), x3, (#6.3001));
494 ((#4.0), x4, (#6.3001));
495 ((#4.0), x5, (#6.3001));
496 ((#8.0), x6, (square (#3.02)))
500 ( (tau_0_x x1 x2 x3 x4 x5 x6) -. ( (#0.2529) *. (dih_x x1 x2 x3 x4 x5 x6))) >.
502 ( (dih_x x1 x2 x3 x4 x5 x6) <. (#1.26)) \/
503 ( (dih_x x1 x2 x3 x4 x5 x6) >. (#1.63)))`;;
510 [((#4.0), x1, square_2t0);
511 ((#4.0), x2, square_2t0);
512 ((#4.0), x3, square_2t0);
513 ((square (#3.2)), x4, (square (#3.2)));
515 (square_2t0, x5, square_2t0);
519 (beta (acs ( (sqrt x1) / (#2.51))) (arclength (sqrt x1) (sqrt x3) (sqrt x5))) <.
520 (dih3_x x1 x2 x3 x4 x5 x6))`;;
524 [((#4.0), x1, square_2t0);
525 ((#4.0), x2, square_2t0);
526 ((#4.0), x3, square_2t0);
528 (square_2t0, x4, (#8.0));
529 (square_2t0, x5, (#8.0));
530 ((#4.0), x6, square_2t0)
533 ( (vor_analytic_x x1 x2 x3 x4 x5 x6) <. (#0.0)) \/
534 ( (eta_x x1 x2 x6) >. (sqrt (#2.0))) \/
535 ( (eta_x x2 x3 x4) >. (sqrt (#2.0))) \/
536 ( (eta_x x1 x3 x5) >. (sqrt (#2.0))) \/
537 ( (eta_x x4 x5 x6) >. (sqrt (#2.0))))`;;
542 [(square_2t0, x1, (square (#2.696)));
543 ((#4.0), x2, (square (#2.168)));
544 ((#4.0), x3, (square (#2.168)));
545 ((#4.0), x4, square_2t0);
546 ((#4.0), x5, square_2t0);
547 ((#4.0), x6, square_2t0)
549 ( (dih2_x x1 x2 x3 x4 x5 x6) >. (#0.74))`;;
553 [((#4.0), x1, square_2t0);
554 ((#4.0), x2, (square (#2.23)));
555 ((#4.0), x3, (square (#2.23)));
556 ((square (#2.77)), x4, (#8.0));
558 ((#4.0), x5, square_2t0);
562 (beta (acs ( (sqrt x1) / (#2.77))) (arclength (sqrt x1) (sqrt x3) (sqrt x5))) <.
563 (dih3_x x1 x2 x3 x4 x5 x6))`;;
568 [((#4.0), x1, (#6.3001));
569 ((#4.0), x2, (square (#2.168)));
570 ((#4.0), x3, (square (#2.168)));
571 ((#4.0), x4, (#6.3001));
572 ((#4.0), x5, (#6.3001));
573 (square_2t0, x6, square_4t0)
575 ( (dih_x x1 x2 x3 x4 x5 x6) <. (#1.63) \/
576 (delta_x x1 x2 x3 x4 x5 x6) <. (#0.0))`;;
580 [((#4.0), x1, square_2t0);
581 ((#4.0), x2, square_2t0);
582 ((#4.0), x3, square_2t0);
584 ((#4.0), x4, (square (#2.177303)));
585 ((#4.0), x5, square_2t0);
586 ((#4.0), x6, square_2t0)
588 ( (sigma_qrtet_x x1 x2 x3 x4 x5 x6) <.
589 ( (#0.31023815) +. ( (--. (#0.207045)) *. (dih_x x1 x2 x3 x4 x5 x6))))`;;
594 [((square (#2.69)), x1, (#8.0));
595 ((#4.0), x2, square_2t0);
596 ((#4.0), x3, square_2t0);
597 ((#4.0), x4, square_2t0);
598 ((#4.0), x5, square_2t0);
599 ((#4.0), x6, square_2t0)
601 ( ( (mu_upright_x x1 x2 x3 x4 x5 x6) +. (mu_flipped_x x1 x2 x3 x4 x5 x6)) <.
602 ( (vor_0_x x1 x2 x3 x4 x5 x6) +. (vor_0_x_flipped x1 x2 x3 x4 x5 x6) +.
603 ( (#0.02) *. ( ( pi / (#2.0)) +. (( --. ) (dih_x x1 x2 x3 x4 x5 x6))))))`;;
607 [(square_2t0, x1, (#8.0));
608 ((#4.0), x2, square_2t0);
609 ((#4.0), x3, square_2t0);
610 ((#4.0), x4, square_2t0);
611 ((#4.0), x5, square_2t0);
612 ((#4.0), x6, square_2t0)
614 ( ( (vor_analytic_x x1 x2 x3 x4 x5 x6) +.
615 (vor_analytic_x_flipped x1 x2 x3 x4 x5 x6) +.
616 (vor_0_x x1 x2 x3 x4 x5 x6) +.
617 (( --. ) (vor_0_x_flipped x1 x2 x3 x4 x5 x6))) <=. (#0.0))`;;
621 [((square (#1.255)), x, (#2.0))
623 ( (crown (sqrt x)) <. (--. (#0.1378)))`;;
627 [(square_2t0, x1, (#8.0));
628 ((#4.0), x2, square_2t0);
629 ((#4.0), x3, square_2t0);
630 ((#4.0), x4, square_2t0);
632 (square_2t0, x5, (#8.0));
633 (square_2t0, x6, (#8.0))
636 ( (vor_analytic_x x1 x2 x3 x4 x5 x6) <. (#0.0)) \/
637 ( (eta_x x1 x2 x6) >. (sqrt (#2.0))) \/
638 ( (eta_x x2 x3 x4) >. (sqrt (#2.0))) \/
639 ( (eta_x x1 x3 x5) >. (sqrt (#2.0))) \/
640 ( (eta_x x4 x5 x6) >. (sqrt (#2.0))))`;;
644 [((#4.0), x1, square_2t0);
645 ((#4.0), x2, square_2t0);
646 ((#4.0), x3, square_2t0);
648 ((#4.0), x4, square_2t0);
649 ((#4.0), x5, square_2t0);
650 ((#4.0), x6, square_2t0)
652 ( (dih_x x1 x2 x3 x4 x5 x6) <. (#1.874445))`;;