legacy/general/deprecated_sphere.hl

   1 (*
   2    May 2012, definitions no longer needed in
   3    primary verifications of flyspeck.
   4 *)
   5
   6 (*
   7 deprecated May 2012:
   8
   9 arclength_x_345
  10 taum_hexall_x
  11 dih_hexall_x
  12  dih1_hexall_x
  13  upper_dih_hexall_x
  14  delta_hexall_x
  15 delta4_hexall_x
  16 eulerA_hexall_x
  17 factor345_hexall_x
  18 law_cosines_234_x
  19 law_cosines_126_x
  20 delta_template_B_x
  21 dih_template_B_x
  22 taum_template_B_x
  23 delta_top_x
  24 tau_lowform_x
  25 tau_m_diff_quotient
  26 tau_m_diff_quotient2
  27
  28 *)
  29
  30
  31 (*
  32 7/29/2009:
  33   * normball deprecated. Replace normball x r with ball(x,r)
  34   * rect deprecated. Use interval instead.
  35   * wedge is now defined by Harrison using azim.  He has proved a lemma giving the equivalence with the previous definition.
  36   * azim in defined by Harrison.
  37   * directed_angle is now defined through complex Arg.
  38   * definition of polar cycle has been changed (again).
  39   * a lemma is needed relating atn2 to Arg.
  40   * cone -> cone0
  41   * deprecated: volume_props.
  42 *)
  43
  44
  45 (* deleted obsolete definitions 2/7/2010 svn 1471:
  46     obsolete definitions:
  47     obsolete: rad2_y, d3, mk_vec3, real3_of_triple, triple_of_real3,
  48     obsolete: conv, radius -> norm(vector[x;y]),
  49     obsolete: polar_angle -> Arg(vector[x;y]),
  50     obsolete: polar_c, less_polar, min_polar,
  51     obsolete: iter_SPEC, iter -> ITER,
  52     obsolete: azim_cycle_hyp_def, azim_cycle_spec, azim_cycle_def,
  53     obsolete: rogers, rogers0, azim_hyp_def, azim_spec, azim_def,
  54
  55     2011-08-01.
  56     obsolete: polar_cycle
  57 *)
  58
  59 (* terms moved to Harrison's flyspeck.ml
  60 NULLSET_RULES,
  61 solid_triangle, ellipsoid, conic_cap, frustum, frustt,
  62 primitive, MEASURABLE_RULES, solid, coplanar, cross, wedge, azim,
  63 *)
  64
  65
  66 (* (now voronoi_open) let voronoi = new_definition `voronoi v S = { x | !w. ((S w) /\ ~(w=v)) ==> (dist( x, v) < dist( x, w)) }`;; *)
  67
  68
  69 (*  DEPRECATED, 2011-08-01, not used
  70
  71 let directed_angle = new_definition `directed_angle (x,y) (x',y') =
  72   Arg (complex(x',y') / complex(x,y))`;;
  73
  74 let cyclic_order = new_definition `cyclic_order v u w =
  75     ((directed_angle v u < directed_angle v w) \/
  76     ((directed_angle v u = directed_angle v w) /\ (radius u <= radius w)))`;;
  77
  78 let polar_cycle = new_definition `polar_cycle V v =
  79    if (V SUBSET {v}) then v else (@ u. ~(u=v) /\ V u /\
  80   (!w.  ~(w = v) /\ V w   ==> cyclic_order v u w))`;;
  81 *)
  82
  83
  84 (*
  85 let sol_euler_y =  `sol_euler_y y1 y2 y3 y4 y5 y6 =
  86   (let a = y1*y2*y3 + y1*(y2*y2 + y3*y3 - y4*y4)/ &2 +
  87      y2*(y1*y1 + y3*y3 - y5*y5)/ &2 + y3*(y1*y1 + y2*y2 - y6*y6)/ &2 in
  88   &2 * atn2( &2 * a, sqrt (delta_y y1 y2 y3 y4 y5 y6)))`;;
  89
  90 let sol_euler_y =  `sol_euler_y = y_of_x sol_euler_x`;;
  91 *)
  92
  93
  94 (*
  95 let acs_sqrt_x1 = new_definition `acs_sqrt_x1 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
  96   acs (sqrt(x1))`;;
  97
  98 let acs_sqrt_x2 = new_definition `acs_sqrt_x2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
  99   acs (sqrt(x2))`;;
 100 *)
 101
 102
 103 (* deprecated
 104
 105 let solRy = new_definition `solRy y1 y2 y6 c = solR (y1/ &2) (eta_y y1 y2 y6) c`;;
 106
 107 let dihRy = new_definition `dihRy y1 y2 y6 c = dihR (y1/ &2) (eta_y y1 y2 y6) c`;;
 108 *)
 109
 110 (* deprecated *)
 111
 112 let arclength_x_345 = new_definition `arclength_x_345  (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) = arclength (sqrt x3) (sqrt x4) (sqrt x5)`;;
 113
 114
 115 (*
 116 let tauq_x = new_definition
 117   `tauq_x x1 x2 x3 x4 x5 x6 x7 x8 x9 =
 118     tauq (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) (sqrt x7)  (sqrt x8)  (sqrt x9)`;;
 119 *)
 120
 121
 122 let taum_hexall_x = new_definition
 123   `taum_hexall_x  x14 x12 x23  x1 x2 x3 x4 x5 (x6:real) =
 124    taum_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12) +
 125      flat_term_x x2`;;
 126
 127
 128 (* deprecated *)
 129
 130 let dih_hexall_x = new_definition `dih_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) =
 131    dih_x x1 x2 x4 ((&2 * h0) pow 2) x14 x12 -
 132    dih_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;;
 133
 134 let dih1_hexall_x = new_definition `dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) =
 135    dih_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;;
 136
 137 let upper_dih_hexall_x = new_definition `upper_dih_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) =
 138    dih_x x1 x2 x4 ((&2 * h0) pow 2) x14 x12 -
 139    upper_dih_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;;
 140
 141 let delta_hexall_x = new_definition `delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) =
 142    delta_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;;
 143
 144 let delta4_hexall_x = new_definition `delta4_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) =
 145    delta_x4 x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;;
 146
 147 (*
 148 let euler_ap = new_definition `euler_ap y1  y2 y3 y4 y5 y6 =
 149   y1*y2*y3 + y1*(y2*y2 + y3*y3 - y4*y4)/ &2 + y2*(y1*y1 + y3*y3 - y5*y5)/ &2 +
 150    y3*(y1*y1 + y2*y2 - y6*y6)/ &2`;;
 151 *)
 152
 153 let eulerA_hexall_x = new_definition `eulerA_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) =
 154    eulerA_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;;
 155
 156
 157 let factor345_hexall_x = new_definition `factor345_hexall_x c (x1:real) (x2:real) x3 x4 x5 (x6:real) =
 158    x5 -x3 -x4 + &2 * c * sqrt(x3) * sqrt(x4)`;;
 159
 160 let law_cosines_234_x = new_definition
 161  `law_cosines_234_x c (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
 162    x4 -x2 -x3 + &2 * c * sqrt(x2) * sqrt(x3)`;;
 163
 164 let law_cosines_126_x = new_definition
 165  `law_cosines_126_x c (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
 166    x6 -x1 -x2 + &2 * c * sqrt(x1) * sqrt(x2)`;;
 167
 168 (* -- not used
 169 let taum_sub156_x = new_definition
 170  `taum_sub156_x x1s x5s x6s (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
 171       taum_x x1s x2 x3 x4 x5s x6s`;;
 172 *)
 173
 174
 175 (* DEPRECATED.
 176 let tau_nullform_x = new_definition
 177   `tau_nullform_x x1 x2 x3 x4 x5 x6 =
 178     rho (sqrt x1) * pi - (pi + sol0) +
 179     sqp(delta_x x1 x2 x3 x4 x5 x6) * tau_residual_x x1 x2 x3 x4 x5 x6`;;
 180 *)
 181
 182
 183 (* deprecated *)
 184
 185 let delta_template_B_x = new_definition
 186  `delta_template_B_x x15 x45 x34 x12      x1 x2 x3 x4 x5 (x6:real) =
 187   (let x23 = x12 in
 188     let x13 = edge_flat2_x x2 x1 x3  (&0)   x23 x12 in
 189     let x14 = edge_flat2_x x5 x1 x4  (&0)   x45 x15 in
 190       (delta_x x1 x3 x4 x34 x14 x13))`;;
 191
 192
 193 let dih_template_B_x = new_definition
 194  `dih_template_B_x x15 x45 x34 x12 x25      x1 x2 x3 x4 x5 (x6:real) =
 195   (let x23 = x12 in
 196     let x13 = edge_flat2_x x2 x1 x3  (&0)   x23 x12 in
 197     let x14 = edge_flat2_x x5 x1 x4  (&0)   x45 x15 in
 198       (dih_x x1 x2 x5 x25 x15 x12 - dih_x x1 x3 x4 x34 x14 x13))`;;
 199
 200 let taum_template_B_x = new_definition
 201  `taum_template_B_x x15 x45 x34 x12      x1 x2 x3 x4 x5 (x6:real) =
 202   (let x23 = x12 in
 203     let x13 = edge_flat2_x x2 x1 x3  (&0)   x23 x12 in
 204     let x14 = edge_flat2_x x5 x1 x4  (&0)   x45 x15 in
 205       (taum_x x1 x3 x4 x34 x14 x13 +flat_term_x x2 + flat_term_x x5))`;;
 206
 207
 208
 209 (* No longer needed.... deprecated. *)
 210 let delta_top_x = new_definition
 211   `delta_top_x (a:real) (x1:real) (x2:real) (x3:real) (x4:real)
 212     (x5:real) (x6:real) (x7:real) (x8:real) (x9:real)   =
 213    delta_y (sqrt x4) (sqrt x9) (sqrt x6) a (sqrt x5) (sqrt x8)`;;
 214
 215
 216 (* tau_lowform_x intended for use when dih1 > pi/2, dih2, dih3 < pi/2,
 217    tau_residual <0,
 218    Then tau_lowform_x is a lower bound on tau (that is graceful when delta->0).
 219 *)
 220
 221 let tau_lowform_x = new_definition
 222   `tau_lowform_x x1 x2 x3 x4 x5 x6 =
 223   (let d = delta_x x1 x2 x3 x4 x5 x6 in
 224     (rho (sqrt x1) * pi - (pi + sol0) +
 225     sqp d * rhazim_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 +
 226     sqn d * rhazim2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 +
 227     sqn d * rhazim3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6))`;;
 228
 229
 230 let tau_m_diff_quotient = new_definition
 231   `tau_m_diff_quotient (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real)  =
 232     (let eps = #0.000001 in
 233     (taum (y1 + eps) y2 y3 y4 y5 y6 - taum y1 y2 y3 y4 y5 y6)/eps)`;;
 234
 235 let tau_m_diff_quotient2 = new_definition
 236   `tau_m_diff_quotient2 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real)  =
 237   (let eps = #0.000001 in
 238    (taum (y1 + eps) y2 y3 y4 y5 y6 - taum y1 y2 y3 y4 y5 y6
 239     + taum (y1 - eps) y2 y3 y4 y5 y6)/(eps pow 2))`;;
 240
 241 (* deleted 2013-08-18 *)
 242
 243 let delta_y_LC = new_definition
 244 `delta_y_LC (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) =
 245   delta_y y1 y2 y3 y4 y5 y6`;;
 246
 247 let mardih_x = new_definition `mardih_x x1 x2 x3 x4 x5 x6 =
 248   marchal_quartic (sqrt x1 / #2.0) * dih_x x1 x2 x3 x4 x5 x6`;;
 249
 250 let mardih2_x = new_definition `mardih2_x x1 x2 x3 x4 x5 x6 =
 251   marchal_quartic (sqrt x2 / #2.0) * dih2_x x1 x2 x3 x4 x5 x6`;;
 252
 253 let mardih3_x = new_definition `mardih3_x x1 x2 x3 x4 x5 x6 =
 254   marchal_quartic (sqrt x3 / #2.0) * dih3_x x1 x2 x3 x4 x5 x6`;;
 255
 256 let mardih4_x = new_definition `mardih4_x x1 x2 x3 x4 x5 x6 =
 257   marchal_quartic (sqrt x4 / #2.0) * dih4_x x1 x2 x3 x4 x5 x6`;;
 258
 259 let mardih5_x = new_definition `mardih5_x x1 x2 x3 x4 x5 x6 =
 260   marchal_quartic (sqrt x5 / #2.0) * dih5_x x1 x2 x3 x4 x5 x6`;;
 261
 262 let mardih6_x = new_definition `mardih6_x x1 x2 x3 x4 x5 x6 =
 263   marchal_quartic (sqrt x6 / #2.0) * dih6_x x1 x2 x3 x4 x5 x6`;;
 264
 265 (* c++ associations:
 266   ("mardih_x","marchalDih");  ("mardih2_x","marchalDih2");
 267   ("mardih3_x","marchalDih3");
 268   ("mardih4_x","marchalDih4");  ("mardih5_x","marchalDih5");
 269   ("mardih6_x","marchalDih6");
 270 *)
 271
 272 (*
 273 (*
 274 num1 is based on the following Mathematica calculation. It is the
 275 numerator of the a-partial derivative of taumarE.
 276 num2 is the numerator of second a-partial
 277 formal proof: derived_form_sum_dih444
 278 *)
 279
 280 taumarE = e1 Dihedral[2, 2, 2, a, b, c] + e2 Dihedral[2, 2, 2, b, c, a] +
 281           e3 Dihedral[2, 2, 2, c, a, b];
 282
 283 afac = a (16 - a^2);
 284 sd = Sqrt[Delta[2, 2, 2, a, b, c]];
 285 abcsub = {a -> 2.1, b -> 2.2, c -> 2.3, e1 -> 5.5, e2 -> 5.6,
 286     e3 -> 5.7, ssd -> sd, aafac -> afac};
 287 abcsq = {a -> Sqrt[a2], b -> Sqrt[b2], c -> Sqrt[c2]};
 288
 289
 290 taumarE1 = 4 a afac e1/(aafac ssd);
 291 taumarE2 = 4 (-8 b^2 + a^2 (-8 + b^2) + 8 c^2) e2/(aafac ssd) ;
 292 taumarE3 = 4 (-8 c^2 + a^2 (-8 + c^2) + 8 b^2) e3/(aafac ssd);
 293 (D[taumarE, a] - taumarE1 - taumarE2 - taumarE3 //. abcsub) // Chop (*0*)
 294
 295 num1e = aafac ssd (taumarE1 + taumarE2 + taumarE3) // Together // Simplify;
 296 num1sqI = -4*(a2^2*e1 + 8*(
 297     b2 - c2)*(e2 - e3) - a2*(16*e1 + (-8 + b2)*e2 + (-8 + c2)*e3)); (* num1
 298     in sphere.hl *)
 299 (num1e /. abcsq) - num1sqI (*0*)
 300
 301 (* second derivatives *)
 302 taumarE1D2calc = D[Dihedral[2, 2, 2, a, b, c], {a,
 303     2}] // Together // Simplify;
 304 taumarE1D2 = -(16*(-a^4 + (b^2 - c^2)^2)) afac^2 /(aafac^2 ssd^3);
 305 (taumarE1D2calc - taumarE1D2 //. abcsub) // Chop
 306
 307
 308
 309 taumarE2D2calc = D[Dihedral[2, 2, 2, b, c, a], {a, 2}] // Together //
 310              Simplify;
 311 taumarE2D2 = -(8*(6*a^8*(-8 + b^2) + 256*(
 312       b^2 - c^2)^3 + a^6*(b^4*(-8 + c^2) - 16*b^2*(3 + c^2) + 16*(
 313                   16 + 9*c^2)) - 16*a^2*(b^6 + b^4*(
 314                 80 - 13*c^2) - 3*c^4*(16 + c^2) + b^2*
 315                 c^2*(-32 +
 316                   15*c^2)) + 2*a^4*(b^6 + b^4*(56 -
 317                       10*c^2) - 24*c^2*(16 + 3*c^2) + b^2*(
 318                       384 + 16*c^2 + 9*c^4))))/(aafac^2 ssd^3);
 319 (taumarE2D2calc - taumarE2D2 //. abcsub) // Chop
 320
 321 taumarE3D2calc = D[Dihedral[2, 2, 2, c, a, b], {a,
 322                       2}] // Together // Simplify;
 323 taumarE3D2 = -(8*(-256*(b^2 - c^2)^3 + 6*a^8*(-8 + c^2) + 16*a^2*
 324                    (3*b^6 + b^4*(48 - 15*c^2) - c^4*(80 + c^2) + b^2*
 325                       c^2*(32 + 13*c^2)) +
 326                 a^6*(b^2*(144 - 16*c^2 + c^4) - 8*(-32 + 6*c^2 + c^4)) + 2*
 327 a^4*(9*b^4*(-8 + c^2) + c^2*(384 + 56*c^2 + c^4) - 2*b^2*(192 - 8*
 328       c^2 + 5*c^4))))/(aafac^2 ssd^3);
 329 (taumarE3D2calc - taumarE3D2 //. abcsub) // Chop
 330
 331 taumarD2num = (e1 taumarE1D2 + e2 taumarE2D2 + e3
 332             taumarE3D2) (aafac^2 ssd^3) // Simplify
 333 taumarD2numDef = (taumarD2num /. abcsq) // HolForm;  (* num2 in sphere.hl *)
 334
 335 (((D[taumarE, {a, 2}]) aafac^2 ssd^3 - taumarD2num) //. abcsub) // Chop
 336
 337 (* analysis near a2 -> 16 *)
 338 {"near a2->16", DeltaX[4,
 339        4, 4, 16, b2, c2] // Factor, (num1sqI /. a2 -> 16) // Factor,
 340   ((taumarD2num /. abcsq) /. a2 -> 16) // Factor}
 341
 342
 343 *)
 344 let num2 = new_definition `num2 e1 e2 e3 a2 b2 c2 =
 345   (&8 * ((&2 * ((a2 pow 5) * e1)) + (((-- &256) * (((b2 + ((-- &1) * c2)) pow 3)
 346  * (e2 + ((-- &1) * e3)))) + (((-- &1) * ((a2 pow 3) * ((&2 * (((-- &256) +
 347  ((b2 pow 2) + (((-- &2) * (b2 * c2)) + (c2 pow 2)))) * e1)) + (((((b2 pow 2)
 348  * ((-- &8) + c2)) + (((-- &16) * (b2 * (&3 + c2))) + (&16 * (&16 + (&9 *
 349  c2))))) * e2) + (((b2 * (&144 + (((-- &16) * c2) + (c2 pow 2)))) + ((-- &8) *
 350  ((-- &32) + ((&6 * c2) + (c2 pow 2))))) * e3))))) + (((a2 pow 4) * (((-- &64)
 351  * e1) + ((-- &6) * ((((-- &8) + b2) * e2) + (((-- &8) + c2) * e3))))) + (((--
 352  &2) * ((a2 pow 2) * ((b2 + ((-- &1) * c2)) * (((b2 pow 2) * e2) + ((&8 * (c2
 353  * ((&4 * e1) + ((&9 * e2) + ((-- &7) * e3))))) + ((&384 * (e2 + ((-- &1) *
 354  e3))) + (((-- &1) * ((c2 pow 2) * e3)) + (b2 * (((-- &32) * e1) + (((&56 +
 355  ((-- &9) * c2)) * e2) + (&9 * (((-- &8) + c2) * e3)))))))))))) + (&16 * (a2 *
 356  ((b2 + ((-- &1) * c2)) * (((b2 pow 2) * (e2 + ((-- &3) * e3))) + (((-- &4) *
 357  (b2 * ((&8 * e1) + ((((-- &20) + (&3 * c2)) * e2) + ((-- &3) * (((-- &4) +
 358  c2) * e3)))))) + (c2 * ((&32 * e1) + ((&3 * ((&16 + c2) * e2)) + ((-- &1) *
 359  ((&80 + c2) * e3))))))))))))))))`;;
 360
 361 let rat1 = new_definition `rat1 e1 e2 e3 a2 b2 c2 =
 362   num1 e1 e2 e3 a2 b2 c2 /
 363     (sqrt(delta_x (&4) (&4) (&4) a2 b2 c2) * sqrt(a2) * (&16 - a2))`;;
 364
 365 let rat2 = new_definition `rat2 e1 e2 e3 a2 b2 c2 =
 366   num2 e1 e2 e3 a2 b2 c2 /
 367     (((sqrt(delta_x (&4) (&4) (&4) a2 b2 c2)) pow 3) * a2 * ((&16 - a2) pow 2))`;;
 368
 369 (* num1^2 - #0.01 * num2 *)
 370
 371 let num_combo1 = new_definition `num_combo1 e1 e2 e3 a2 b2 c2 =
 372 ((&2 / &25) * (((-- &2) * ((a2 pow 5) * e1)) + ((&256 * (((b2 + ((-- &1) *
 373 c2)) pow 3) * (e2 + ((-- &1) * e3)))) + (((a2 pow 3) * ((&2 * (((-- &256) +
 374 ((b2 pow 2) + (((-- &2) * (b2 * c2)) + (c2 pow 2)))) * e1)) + (((((b2 pow 2)
 375 * ((-- &8) + c2)) + (((-- &16) * (b2 * (&3 + c2))) + (&16 * (&16 + (&9 *
 376 c2))))) * e2) + (((b2 * (&144 + (((-- &16) * c2) + (c2 pow 2)))) + ((-- &8) *
 377 ((-- &32) + ((&6 * c2) + (c2 pow 2))))) * e3)))) + ((&2 * ((a2 pow 4) * ((&32
 378 * e1) + (&3 * ((((-- &8) + b2) * e2) + (((-- &8) + c2) * e3)))))) + ((&200 *
 379 ((((a2 pow 2) * e1) + ((&8 * ((b2 + ((-- &1) * c2)) * (e2 + ((-- &1) * e3))))
 380 + ((-- &1) * (a2 * ((&16 * e1) + ((((-- &8) + b2) * e2) + (((-- &8) + c2) *
 381 e3))))))) pow 2)) + ((&2 * ((a2 pow 2) * ((b2 + ((-- &1) * c2)) * (((b2 pow 2)
 382 * e2) + ((&8 * (c2 * ((&4 * e1) + ((&9 * e2) + ((-- &7) * e3))))) + ((&384 *
 383 (e2 + ((-- &1) * e3))) + (((-- &1) * ((c2 pow 2) * e3)) + (b2 * (((-- &32) *
 384 e1) + (((&56 + ((-- &9) * c2)) * e2) + (&9 * (((-- &8) + c2) *
 385 e3)))))))))))) + ((-- &16) * (a2 * ((b2 + ((-- &1) * c2)) * (((b2 pow 2) *
 386 (e2 + ((-- &3) * e3))) + (((-- &4) * (b2 * ((&8 * e1) + ((((-- &20) + (&3 *
 387 c2)) * e2) + ((-- &3) * (((-- &4) + c2) * e3)))))) + (c2 * ((&32 * e1) + ((&3
 388 * ((&16 + c2) * e2)) + ((-- &1) * ((&80 + c2) * e3)))))))))))))))))`;;
 389
 390 (* x_A is a special case of x_C: *)
 391
 392 (*
 393 let truncate_gamma23_x_A = new_definition `truncate_gamma23_x_A iw1 m1 m2 m6 =
 394   scalar6
 395     (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
 396        dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
 397     iw1
 398   + (dih_x - (mk_126 (truncate_dih_x (#0.14)) + constant6 (#0.08))) *
 399        uni((truncate_gamma2_x m1), proj_x1)`;;
 400 *)
 401
 402 let truncate_gamma23_x_C = new_definition `truncate_gamma23_x_C d iw1 m1 m2 m6 =
 403   scalar6
 404     (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
 405        dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
 406     iw1
 407   + (dih_x - (mk_126 (truncate_dih_x (#0.14)) + constant6 (d))) *
 408        uni((truncate_gamma2_x m1), proj_x1)`;;
 409
 410
 411 let truncate_gamma23_x_B = new_definition
 412   `truncate_gamma23_x_B m1  =
 413        (dih_x  - constant6 (&2 * #0.08)) *
 414          uni((truncate_gamma2_x m1),proj_x1)`;;
 415
 416 (* function truncate_gamma2_x deprecated.  It is incorrect.  See gamma2_x_div_azim_v2 *)
 417 let truncate_gamma2_x =
 418   new_definition `truncate_gamma2_x m x = (&8 - x)* sqrt x / (&24) -
 419   ( (&2 * mm1/ pi) * (&1 - sqrt x / sqrt8) -
 420       (&8 * mm2 / pi) * m * lfun (sqrt x / &2))`;;
 421
 422 let truncate_gamma3f_x = new_definition `truncate_gamma3f_x d m4 m5 m6  =
 423   truncate_vol3r_456 d  -
 424     truncate_vol3f d m4 m5 m6`;;
 425
 426 let truncate_gamma23_x = new_definition `truncate_gamma23_x iw1 iw2 m1 m2 m3 m5 m6 =
 427   scalar6
 428     (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
 429        dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
 430     iw1  +
 431     scalar6
 432     (compose6 (truncate_gamma3f_x (#0.14) m1 m3 m5)
 433        dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5)
 434     iw2
 435   + (dih_x -
 436        (mk_126 (truncate_dih_x (#0.14)) +
 437           mk_135 (truncate_dih_x (#0.14)))) *
 438     uni((truncate_gamma2_x m1),proj_x1)`;;
 439
 440 (* version for large azimuth angles *)
 441 let truncate_gamma23a_x = new_definition   `
 442     truncate_gamma23a_x iw1 iw2 m1 m2 m3 m5 m6 x1 x2 x3 az4 x5 x6 =
 443   truncate_gamma3f_x (&0) m1 m2 m6 (&0) (&0) (&0) x1 x2 x6 * iw1 +
 444     truncate_gamma3f_x (&0) m1 m3 m5 (&0) (&0) (&0) x1 x3 x5 * iw2 +
 445     (az4 -
 446        (dih_x x1 x2 (&2) (&2) (&2) x6 +
 447           dih_x x1 (&2) x3 (&2) x5 (&2))) *
 448     truncate_gamma2_x m1 x1`;;
 449
 450 let truncate_gamma2_x =
 451   new_definition `truncate_gamma2_x m x = (&8 - x)* sqrt x / (&24) -
 452   ( (&2 * mm1/ pi) * (&1 - sqrt x / sqrt8) -
 453       (&8 * mm2 / pi) * m * lfun (sqrt x / &2))`;;
 454
 455 let truncate_gamma3f_x = new_definition `truncate_gamma3f_x d m4 m5 m6  =
 456   truncate_vol3r_456 d  -
 457     truncate_vol3f d m4 m5 m6`;;
 458
 459 let truncate_gamma23_x = new_definition `truncate_gamma23_x iw1 iw2 m1 m2 m3 m5 m6 =
 460   scalar6
 461     (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
 462        dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
 463     iw1  +
 464     scalar6
 465     (compose6 (truncate_gamma3f_x (#0.14) m1 m3 m5)
 466        dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5)
 467     iw2
 468   + (dih_x -
 469        (mk_126 (truncate_dih_x (#0.14)) +
 470           mk_135 (truncate_dih_x (#0.14)))) *
 471     uni((truncate_gamma2_x m1),proj_x1)`;;
 472
 473 (* version for large azimuth angles *)
 474 let truncate_gamma23a_x = new_definition   `
 475     truncate_gamma23a_x iw1 iw2 m1 m2 m3 m5 m6 x1 x2 x3 az4 x5 x6 =
 476   truncate_gamma3f_x (&0) m1 m2 m6 (&0) (&0) (&0) x1 x2 x6 * iw1 +
 477     truncate_gamma3f_x (&0) m1 m3 m5 (&0) (&0) (&0) x1 x3 x5 * iw2 +
 478     (az4 -
 479        (dih_x x1 x2 (&2) (&2) (&2) x6 +
 480           dih_x x1 (&2) x3 (&2) x5 (&2))) *
 481     truncate_gamma2_x m1 x1`;;
 482
 483 let truncate_sqrt  = new_definition `
 484   truncate_sqrt c x = if (x <= c) then sqrt(c) else sqrt(x)`;;
 485
 486 let truncate_dih_x = new_definition(`truncate_dih_x c x1 x2 x3 x4 x5 x6 =
 487        let d_x4 = delta_x4 x1 x2 x3 x4 x5 x6 in
 488        let d = delta_x x1 x2 x3 x4 x5 x6 in
 489        pi/ (&2) +  atn2( (sqrt ((&4) * x1) * truncate_sqrt c d),--  d_x4)`);;
 490
 491 let truncate_sol_x = new_definition
 492   `truncate_sol_x c = truncate_dih_x c +
 493      (rotate2 (truncate_dih_x c)) +
 494      (rotate3 (truncate_dih_x c)) - constant6 (pi)`;;
 495
 496
 497
 498
 499
 500 let truncate_vol_x  =new_definition
 501   `truncate_vol_x c = scalar6 (uni((truncate_sqrt c),delta_x)) (&1 / &12)`;;
 502
 503 let truncate_vol3r_456 = new_definition `truncate_vol3r_456 c =
 504   mk_456 (truncate_vol_x c)`;;
 505
 506 (* new 6/18 *)
 507
 508 let truncate_vol3f = new_definition `truncate_vol3f c m4 m5 m6 =
 509   scalar6 ( mk_456 (rotate5 (truncate_sol_x c)) +
 510                 mk_456 (rotate6 (truncate_sol_x c)) +
 511                 mk_456 (rotate4 (truncate_sol_x c))
 512                )  (&2 * mm1/ pi)
 513     -
 514       scalar6 (
 515         (scalar6 (uni(lfun,(scalar6 proj_y4  #0.5))) m4) *
 516           mk_456 (rotate4 (truncate_dih_x c)) +
 517         (scalar6 (uni(lfun,(scalar6 proj_y5  #0.5))) m5) *
 518           mk_456 (rotate5 (truncate_dih_x c)) +
 519         (scalar6 (uni(lfun,(scalar6 proj_y6  #0.5))) m6) *
 520           mk_456 (rotate6 (truncate_dih_x c))
 521       )  (&8 * mm2 / pi)`;;
 522
 523 let truncate_sqrt  = new_definition `
 524   truncate_sqrt c x = if (x <= c) then sqrt(c) else sqrt(x)`;;
 525
 526 let truncate_dih_x = new_definition(`truncate_dih_x c x1 x2 x3 x4 x5 x6 =
 527        let d_x4 = delta_x4 x1 x2 x3 x4 x5 x6 in
 528        let d = delta_x x1 x2 x3 x4 x5 x6 in
 529        pi/ (&2) +  atn2( (sqrt ((&4) * x1) * truncate_sqrt c d),--  d_x4)`);;
 530
 531 let truncate_sol_x = new_definition
 532   `truncate_sol_x c = truncate_dih_x c +
 533      (rotate2 (truncate_dih_x c)) +
 534      (rotate3 (truncate_dih_x c)) - constant6 (pi)`;;
 535
 536 let truncate_vol_x  =new_definition
 537   `truncate_vol_x c = scalar6 (uni((truncate_sqrt c),delta_x)) (&1 / &12)`;;
 538
 539 let truncate_vol3r_456 = new_definition `truncate_vol3r_456 c =
 540   mk_456 (truncate_vol_x c)`;;
 541
 542
 543 (* new 6/18 *)
 544
 545 let truncate_vol3f = new_definition `truncate_vol3f c m4 m5 m6 =
 546   scalar6 ( mk_456 (rotate5 (truncate_sol_x c)) +
 547                 mk_456 (rotate6 (truncate_sol_x c)) +
 548                 mk_456 (rotate4 (truncate_sol_x c))
 549                )  (&2 * mm1/ pi)
 550     -
 551       scalar6 (
 552         (scalar6 (uni(lfun,(scalar6 proj_y4  #0.5))) m4) *
 553           mk_456 (rotate4 (truncate_dih_x c)) +
 554         (scalar6 (uni(lfun,(scalar6 proj_y5  #0.5))) m5) *
 555           mk_456 (rotate5 (truncate_dih_x c)) +
 556         (scalar6 (uni(lfun,(scalar6 proj_y6  #0.5))) m6) *
 557           mk_456 (rotate6 (truncate_dih_x c))
 558       )  (&8 * mm2 / pi)`;;
 559
 560 (* in delta_pent_x: nonstandard ordering of variables, x6 swapped with x3 *)
 561
 562 let delta_pent_x = new_definition
 563   `delta_pent_x  (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
 564      delta_x x1 x2 x6 (&4) (&4) (#3.24 pow 2)`;;
 565
 566
 567
 568
 569
 570 (*
 571
 572 Upper approximation to Sqrt on [0,1]:
 573
 574 sqp = 3/8 + (3*x)/4 - x^2/8  + (1 - x)^3  (0.7 x - 0.25);
 575
 576 Sqp[x_]:= If[x<1,3/8 + (3*x)/4 - x^2/8  + (1 - x)^3  (0.7 x - 0.25),Sqrt[x]];
 577
 578 DeltaX4[x1_, x2_, x3_, x4_, x5_, x6_] := -(x2*x3) - x1*x4 +
 579       x2*x5 + x3*x6 - x5*x6 + x1*(-x1 + x2 + x3 - x4 + x5 + x6);
 580
 581 Matan[x_] := ArcTan[Sqrt[x]]/Sqrt[x];
 582
 583 UpperDihX[x1_, x2_, x3_, x4_, x5_, x6_] :=  Module[{d, d4},
 584       d = DeltaX[x1, x2, x3, x4, x5, x6];
 585       d4 = DeltaX4[x1, x2, x3, x4, x5, x6];
 586       2 Sqrt[x1] Sqp[d]/d4  * Matan[4 x1 d/d4^2]];
 587
 588 UpperDihY[y1_, y2_, y3_, y4_, y5_, y6_] :=
 589         UpperDihX @@ ({y1, y2, y3, y4, y5, y6}^2);
 590
 591 Lower approx to sqrt on [0,1]:
 592
 593 sqn = 3/8 + (3*x)/4 - x^2/8 + (1 - x)^3 (1.3 x (1 - x) - 3/8) - 0.3 x^2(1 - x)^3;
 594
 595 Thm: if y1,y2,y3 >= 2, then Dihedral[sqrt2,y1,y2,y3,sqrt2,sqrt2] >= pi/2,
 596   (and delta_x4 <= 0).  Proof: Imagine the cube of side sqrt2. qed.
 597   The case of equality delta_x4=0 occurs when y3=2, and y1 or y2=2.
 598 Thm: if y1,y2,y3 in [2,sqrt8], then Dihedral[y1,y2,sqrt2,sqrt2,sqrt2,y6] <= pi/2
 599   (and delta_x4 >= 0).  Proof. The triangle y1,y2,y3 is acute, so the circumcenter lands inside.
 600 *)
 601
 602 let sqp = new_definition `sqp x =
 603     if (x < &1) then
 604        &3 / &8 +  (&1 - x) pow 3 * (-- #0.25 + #0.7 * x) +
 605          &3 * x / &4 - x * x/ &8 else sqrt x`;;
 606
 607 let sqn = new_definition `sqn x =
 608   if (x < &1)
 609   then #0.375 + (&3*x)/ &4  - (x pow 2)/ &8 -   #0.3*((&1 - x) pow 3)*(x pow 2) +
 610    ((&1 - x) pow 3)*(-- #0.375 + #1.3*(&1 - x)*x)
 611   else sqrt x`;;
 612
 613 (* upper bound on dih (when delta_x4 > 0), useful when delta is near 0 and angle is near 0.
 614     Also pi + upper_dih_x is a lower bound on dih when (delta_x4 < 0), useful when delta is
 615     near 0 and angle is near pi.  *)
 616
 617 let upper_dih_x = new_definition `upper_dih_x x1 x2 x3 x4 x5 x6 =
 618   (let d = delta_x x1 x2 x3 x4 x5 x6 in
 619   let d4 = delta_x4 x1 x2 x3 x4 x5 x6 in (
 620    &2 * sqrt x1 * sqp d *
 621     matan (&4 * x1 * d / (d4 pow 2) ) / d4))`;;
 622
 623 let upper_dih_y = new_definition `upper_dih_y = y_of_x upper_dih_x`;;
 624
 625 let gamma3f_135_n = new_definition `gamma3f_135_n y1 y2 y3 y4 y5 y6 =
 626     sqn(delta_y y1 y2 y3 y4 y5 y6) * (&1 / &12 -
 627    ( (&2 * mm1 / pi) *
 628          (y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6
 629           + y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 +
 630           y_of_x sol_euler345_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) -
 631          (&8 * mm2 / pi) *
 632          (y_of_x lmdih_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 +
 633           y_of_x lmdih3_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 +
 634           y_of_x lmdih5_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6)
 635    ))`;;
 636
 637 let gamma3f_126_n = new_definition `gamma3f_126_n y1 y2 y3 y4 y5 y6 =
 638     sqn(delta_y y1 y2 y3 y4 y5 y6) * (&1 / &12 -
 639    ( (&2 * mm1 / pi) *
 640          (y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6
 641           + y_of_x sol_euler246_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 +
 642           y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) -
 643          (&8 * mm2 / pi) *
 644          (y_of_x lmdih_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 +
 645           y_of_x lmdih2_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 +
 646           y_of_x lmdih6_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6)
 647    ))`;;
 648
 649 let gamma23f_n = new_definition `gamma23f_n y1 y2 y3 y4 y5 y6 w1 w2 r f =
 650          gamma3f_126_n y1 y2 sqrt2 sqrt2 sqrt2 y6 / &w1 +
 651          gamma3f_135_n y1 sqrt2 y3 sqrt2 y5 sqrt2 / &w2 +
 652          (dih_y y1 y2 y3 y4 y5 y6 -
 653           upper_dih_y y1 y2 r r r y6 -
 654           upper_dih_y y1 y3 r r r y5) *
 655          (vol2r y1 r - vol2f y1 r f) / (&2 * pi)`;;
 656
 657 let gamma23f_126_03_n = new_definition
 658   `gamma23f_126_03_n y1 y2 y3 y4 y5 y6 w1 r f =
 659          gamma3f_126_n y1 y2 sqrt2 sqrt2 sqrt2 y6 / &w1 +
 660          (dih_y y1 y2 y3 y4 y5 y6 - upper_dih_y y1 y2 r r r y6 - #0.03) *
 661          (vol2r y1 r - vol2f y1 r f) / (&2 * pi)`;;
 662
 663
 664 let euler_3flat_x = new_definition
 665   `euler_3flat_x x1 x2 x3 x23 x13 x12 =
 666 let x5 = edge_flat2_x x13 x1 x3 (&0)    (&4) (&4) in
 667 let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
 668 let x4 = edge_flat2_x x23 x2 x3 (&0)    (&4) (&4) in
 669   (eulerA_x x1 x2 x3 x4 x5 x6)`;;
 670
 671 let euler_2flat_x = new_definition
 672   `euler_2flat_x x1 x2 x3 x4 x13 x12 =
 673 let x5 = edge_flat2_x x13 x1 x3 (&0)    (&4) (&4) in
 674 let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
 675   (eulerA_x x1 x2 x3 x4 x5 x6)`;;
 676
 677 let euler_1flat_x = new_definition
 678   `euler_1flat_x x1 x2 x3 x4 x5 x12 =
 679 let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
 680   (eulerA_x x1 x2 x3 x4 x5 x6)`;;
 681
 682 let taum_3flat_x = new_definition
 683   `taum_3flat_x x1 x2 x3 x23 x13 x12 =
 684 let x5 = edge_flat2_x x13 x1 x3 (&0)    (&4) (&4) in
 685 let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
 686 let x4 = edge_flat2_x x23 x2 x3 (&0)    (&4) (&4) in
 687   (taum_x x1 x2 x3 x4 x5 x6  + flat_term_x x12 + flat_term_x x23 + flat_term_x x13)`;;
 688
 689 let taum_2flat_x = new_definition
 690   `taum_2flat_x x1 x2 x3 x4 x13 x12 =
 691 let x5 = edge_flat2_x x13 x1 x3 (&0)    (&4) (&4) in
 692 let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
 693   (taum_x x1 x2 x3 x4 x5 x6  + flat_term_x x12 +  flat_term_x x13)`;;
 694
 695 let taum_1flat_x = new_definition
 696   `taum_1flat_x x1 x2 x3 x4 x5 x12 =
 697 let x6 = edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) in
 698   (taum_x x1 x2 x3 x4 x5 x6  + flat_term_x x12)`;;
 699
 700 (* DEPRECATED 2013-05-25.
 701 let sphere= new_definition`sphere x=(?(v:real^3)(r:real). (r> &0)/\ (x={w:real^3 | norm (w-v)= r}))`;;
 702 *)
 703
 704 (* deprecated 2013-2-13.
 705 let beta = new_definition(`beta psi theta =
 706         let arg = ((cos psi)*(cos psi) -  (cos theta)*(cos theta))/
 707         ((&1) -  (cos theta)*(cos theta))  in
 708         (acs (sqrt arg))`);;
 709 *)
 710
 711 (* deprecated 2013-2-13.
 712 let radius = new_definition `radius (x,y) = sqrt((x pow 2) + (y pow 2))`;;
 713 *)
 714
 715
 716
 717
 718 (* DEPRECATED added May 11, 2013. x4 st. delta_x = 50, removed May 24, 2013.
 719 let edge_flat50 =  new_definition`edge_flat50 y1 y2 y3 y5 y6 =
 720  sqrt(quadratic_root_plus (abc_of_quadratic (
 721    \x4.  &50 - delta_x (y1*y1) (y2*y2)  (y3*y3)  x4 (y5*y5)  (y6*y6))))`;;
 722
 723 let edge_flat250_x = new_definition `edge_flat250_x x1 x2 x3 x4 x5 x6 =
 724   (edge_flat (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x5) (sqrt x6)) pow 2`;;  (* x4 dummy *)
 725
 726 let edge_flat50_x =  new_definition`edge_flat50_x x1 x2 x3 (x4:real) x5 x6 =
 727  edge_flat (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x5) (sqrt x6)`;;
 728 *)
 729
 730 (* deprecated, Dec 1, 2012 , replaced with beta_bumpA_y *)
 731
 732 (*
 733 let beta_bump_y = new_definition `beta_bump_y y1 y2 y3 y4 y5 y6 =
 734   (if critical_edge_y y1 then &1 else &0) *
 735   (if critical_edge_y y2 then &0 else &1) *
 736   (if critical_edge_y y3 then &0 else &1) *
 737   (if critical_edge_y y4 then &1 else &0) *
 738   (if critical_edge_y y5 then &0 else &1) *
 739   (if critical_edge_y y6 then &0 else &1) *
 740     (bump (y1/ &2) - bump (y4 / &2))`;;
 741 *)
 742
 743
 744
 745 (*
 746     let delta_x6 = new_definition
 747       `delta_x6 x1 x2 x3 x4 x5 x6 = -- x1 *x2 + x1 *x4 + x2* x5 - x4* x5 + x3* (x1 + x2 - x3 + x4 + x5 - x6) -
 748       x3 * x6`;;
 749 *)
 750
 751
 752
 753 let gamma3f_135_s_n = new_definition `gamma3f_135_s_n y1 y2 y3 y4 y5 y6 =
 754   sqn(delta_y y1 y2 y3 y4 y5 y6) *  (&1 / &12 -
 755     (&2 * mm1 / pi) *
 756          (y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6
 757           + y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 +
 758           y_of_x sol_euler345_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) )`;;
 759
 760 let gamma3f_126_s_n = new_definition `gamma3f_126_s_n y1 y2 y3 y4 y5 y6 =
 761   sqn(delta_y y1 y2 y3 y4 y5 y6) *  (&1 / &12 -
 762     (&2 * mm1 / pi) *
 763          (y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6
 764           + y_of_x sol_euler246_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 +
 765           y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) )`;;
 766
 767 let lmdih_x_n = new_definition `lmdih_x_n x1 x2 x3 x4 x5 x6 =
 768   sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
 769
 770 let lmdih2_x_n = new_definition `lmdih2_x_n x1 x2 x3 x4 x5 x6 =
 771   sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
 772
 773 let lmdih3_x_n = new_definition `lmdih3_x_n x1 x2 x3 x4 x5 x6 =
 774   sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
 775
 776 let lmdih5_x_n = new_definition `lmdih5_x_n x1 x2 x3 x4 x5 x6 =
 777   sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih5_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
 778
 779 let lmdih6_x_n = new_definition `lmdih6_x_n x1 x2 x3 x4 x5 x6 =
 780   sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih6_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
 781
 782 let gamma3f_vLR_n = new_definition `gamma3f_vLR_n y1 y2 y3 y4 y5 y6 f =
 783       (dih_y y1 y2 y3 y4 y5 y6 -
 784           upper_dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 -
 785           upper_dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
 786          (vol2r y1 sqrt2 - vol2f y1 sqrt2 f) / (&2 * pi)`;;
 787
 788 let gamma3f_vL_n = new_definition `gamma3f_vL_n y1 y2 y3 y4 y5 y6 f =
 789   (dih_y y1 y2 y3 y4 y5 y6 - upper_dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) *
 790          (vol2r y1 sqrt2 - vol2f y1 sqrt2 f) / (&2 * pi)`;;
 791
 792 let gamma3f_vLR_n0 = new_definition `gamma3f_vLR_n0 y1 y2 y3 y4 y5 y6 =
 793    gamma3f_vLR_n y1 y2 y3 y4 y5 y6 (\x. &0)`;;
 794
 795 let gamma3f_vLR_nlfun = new_definition `gamma3f_vLR_nlfun y1 y2 y3 y4 y5 y6 =
 796   gamma3f_vLR_n y1 y2 y3 y4 y5 y6 lfun`;;
 797
 798 let  gamma3f_vL_n0 = new_definition `gamma3f_vL_n0 y1 y2 y3 y4 y5 y6 =
 799   gamma3f_vL_n y1 y2 y3 y4 y5 y6 (\x. &0)`;;
 800
 801 let gamma3f_vL_nlfun = new_definition `gamma3f_vL_nlfun y1 y2 y3 y4 y5 y6 =
 802   gamma3f_vL_n y1 y2 y3 y4 y5 y6 lfun`;;
 803
 804 let ldih_x_n = new_definition `ldih_x_n x1 x2 x3 x4 x5 x6 =
 805   sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
 806
 807 let ldih2_x_n = new_definition `ldih2_x_n x1 x2 x3 x4 x5 x6 =
 808   sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
 809
 810 let ldih3_x_n = new_definition `ldih3_x_n x1 x2 x3 x4 x5 x6 =
 811   sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
 812
 813 let ldih5_x_n = new_definition `ldih5_x_n x1 x2 x3 x4 x5 x6 =
 814   sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih5_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
 815
 816 let ldih6_x_n = new_definition `ldih6_x_n x1 x2 x3 x4 x5 x6 =
 817   sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih6_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
 818
 819 let gamma3f_vLR_x_nlfun = new_definition `gamma3f_vLR_x_nlfun x1 x2 x3 x4 x5 x6=
 820     gamma3f_vLR_nlfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
 821
 822 let gamma3f_vL_x_nlfun = new_definition `gamma3f_vL_x_nlfun x1 x2 x3 x4 x5 x6=
 823     gamma3f_vL_nlfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
 824
 825 let gamma3f_vLR_x_n0 = new_definition `gamma3f_vLR_x_n0 x1 x2 x3 x4 x5 x6=
 826     gamma3f_vLR_n0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
 827
 828 let gamma3f_vL_x_n0 = new_definition `gamma3f_vL_x_n0 x1 x2 x3 x4 x5 x6=
 829     gamma3f_vL_n0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
 830
 831 let gamma3f_135_x_s_n = new_definition
 832   `gamma3f_135_x_s_n x1 (x2:real) x3 (x4:real) x5 (x6:real) =
 833     gamma3f_135_s_n (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
 834
 835 let gamma3f_126_x_s_n = new_definition
 836   `gamma3f_126_x_s_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
 837    gamma3f_126_s_n (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
 838
 839 let rr22 = REWRITE_RULE[GSYM sqrt2_sqrt2];;
 840
 841 let ldih_x_126_n = rr22 (new_definition `ldih_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 =
 842    ldih_x_n x1 x2 (&2) (&2) (&2) x6`);;
 843
 844 (*
 845 let ldih2_x_126_n = rr22 (new_definition
 846 `ldih2_x_126_n_ x1 x2 (x3:real) (x4:real) (x5:real) x6 =
 847    ldih2_x_n x1 x2 (&2) (&2) (&2) x6`);;
 848 *)
 849
 850 let ldih2_x_126_n = rr22 (new_definition
 851 `ldih2_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 =
 852    ldih2_x_n x1 x2 (&2) (&2) (&2) x6`);;
 853
 854 let ldih6_x_126_n = rr22 (new_definition
 855  `ldih6_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 =
 856    ldih6_x_n x1 x2 (&2) (&2) (&2) x6`);;
 857
 858 let ldih_x_135_n = rr22 (new_definition
 859  `ldih_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
 860    ldih_x_n x1  (&2) x3 (&2) x5 (&2)`);;
 861
 862 let ldih3_x_135_n = rr22 (new_definition
 863 `ldih3_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
 864    ldih3_x_n x1  (&2) x3 (&2) x5 (&2)`);;
 865
 866 let ldih5_x_135_n = rr22 (new_definition
 867  `ldih5_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
 868    ldih5_x_n x1  (&2) x3 (&2) x5 (&2)`);;
 869
 870 (*
 871 let vol3f_sqrt2_lfun = new_definition
 872   `vol3f_sqrt2_lfun y1 y2 (y3:real) (y4:real) (y5:real) y6 =
 873     vol3f y1 y2 y6 sqrt2 lfun`;;
 874 *)
 875
 876 (* remaining splits *)
 877
 878 let gamma3f_126 = new_definition
 879  `gamma3f_126 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f =
 880    gamma3f y1 y2 y6 sqrt2 f`;;
 881
 882 let gamma3f_135 = new_definition
 883  `gamma3f_135 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f  =
 884    gamma3f y1 y3 y5 sqrt2 f`;;
 885
 886 let gamma3f_vLR = new_definition
 887  `gamma3f_vLR (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f  =
 888   (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
 889   (vol2r y1 sqrt2 - vol2f y1 sqrt2 f)/(&2 * pi)`;;
 890
 891 let gamma3f_vL = new_definition
 892  `gamma3f_vL (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f  =
 893   (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) * (vol2r y1 sqrt2 - vol2f y1 sqrt2 f)/(&2 * pi)`;;
 894
 895 let gamma3f_v = new_definition
 896  `gamma3f_v (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f  =
 897   (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 sqrt2 - vol2f y1 sqrt2 f)/(&2 * pi)`;;
 898
 899
 900 let gamma23f_126_03 = new_definition `gamma23f_126_03 y1 y2 y3 y4 y5 y6 w1 r f =
 901       (gamma3f y1 y2 y6 r f / &w1
 902       + (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 r r r y6 - #0.03) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)) `;;
 903
 904 let gamma23f_red_03 = new_definition `gamma23f_red_03 y1 y2 y3 y4 y5 y6 r f =
 905        (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)`;;
 906
 907 let gamma3f_vLR0 = new_definition `gamma3f_vLR0 y1 y2 y3 y4 y5 y6 =
 908    (dih_y y1 y2 y3 y4 y5 y6 -
 909   dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 -
 910   dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
 911  (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
 912  (&2 * pi)`;;
 913
 914 let gamma3f_vLR_lfun = new_definition `gamma3f_vLR_lfun y1 y2 y3 y4 y5 y6 =
 915 (dih_y y1 y2 y3 y4 y5 y6 -
 916   dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 -
 917   dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
 918  (vol2r y1 sqrt2 -
 919   ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
 920    (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
 921  (&2 * pi) `;;
 922
 923
 924 let  gamma3f_vL0 = new_definition `gamma3f_vL0 y1 y2 y3 y4 y5 y6 =
 925 (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) *
 926  (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
 927  (&2 * pi)   `;;
 928
 929
 930 let gamma3f_vL_lfun = new_definition `gamma3f_vL_lfun y1 y2 y3 y4 y5 y6 =
 931  (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) *
 932  (vol2r y1 sqrt2 -
 933   ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
 934    (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
 935  (&2 * pi)`;;
 936
 937 let  gamma3f_v0 = new_definition `gamma3f_v0 y1 y2 y3 y4 y5 y6 =
 938   (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) *
 939     (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
 940     (&2 * pi)`;;
 941
 942
 943 let gamma3f_v_lfun = new_definition `gamma3f_v_lfun y1 y2 y3 y4 y5 y6 =
 944    (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) *
 945  (vol2r y1 sqrt2 -
 946   ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
 947    (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
 948  (&2 * pi)`;;
 949
 950 let dih_x_126_s2 = new_definition `dih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
 951    dih_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
 952
 953 let dih2_x_126_s2 = new_definition `dih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
 954    dih2_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
 955
 956 let dih3_x_126_s2 = new_definition `dih3_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
 957    dih3_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
 958
 959 let dih4_x_126_s2 = new_definition `dih4_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
 960    dih4_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
 961
 962 let dih5_x_126_s2 = new_definition `dih5_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
 963    dih5_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
 964
 965 let dih6_x_126_s2 = new_definition `dih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
 966    dih6_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
 967
 968 let ldih_x_126_s2 = new_definition `ldih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
 969    lfun (sqrt x1 / #2.0) * dih_x_126_s2 x1 x2 x3 x4 x5 x6`;;
 970
 971 let ldih2_x_126_s2 = new_definition `ldih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
 972    lfun (sqrt x2 / #2.0) * dih2_x_126_s2 x1 x2 x3 x4 x5 x6`;;
 973
 974 let ldih6_x_126_s2 = new_definition `ldih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
 975    lfun (sqrt x6 / #2.0) * dih6_x_126_s2 x1 x2 x3 x4 x5 x6`;;
 976
 977 let dih_x_135_s2 = new_definition `dih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
 978    dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
 979
 980 let dih2_x_135_s2 = new_definition `dih2_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
 981    dih2_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
 982
 983 let dih3_x_135_s2 = new_definition `dih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
 984    dih3_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
 985
 986 let dih4_x_135_s2 = new_definition `dih4_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
 987    dih4_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
 988
 989 let dih5_x_135_s2 = new_definition `dih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
 990    dih5_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
 991
 992 let dih6_x_135_s2 = new_definition `dih6_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
 993    dih6_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
 994
 995 let ldih_x_135_s2' = new_definition `ldih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
 996    lfun (sqrt x1/ #2.0) * dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
 997
 998 let ldih3_x_135_s2 = new_definition `ldih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
 999    lfun (sqrt x3/ #2.0) * dih3_x_135_s2 x1 x2 x3 x4 x5 x6 `;;
1000
1001 let ldih5_x_135_s2 = new_definition `ldih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1002    lfun (sqrt x5/ #2.0) * dih5_x_135_s2 x1 x2 x3 x4 x5 x6 `;;
1003
1004
1005 let delta_x_126_s2 = new_definition
1006   `delta_x_126_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1007     delta_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
1008
1009 let delta_x_135_s2 = new_definition
1010   `delta_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1011     delta_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
1012
1013 let gamma3f_x_vLR_lfun = new_definition
1014 `gamma3f_x_vLR_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1015     gamma3f_vLR_lfun  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1016       (sqrt x6)`;;
1017
1018 let gamma3f_x_vLR0 = new_definition
1019 `gamma3f_x_vLR0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1020     gamma3f_vLR0  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1021       (sqrt x6)`;;
1022
1023 let gamma3f_x_vL_lfun = new_definition
1024 `gamma3f_x_vL_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1025     gamma3f_vL_lfun  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1026       (sqrt x6)`;;
1027
1028 let gamma3f_x_vL0 = new_definition
1029 `gamma3f_x_vL0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1030     gamma3f_vL0  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1031       (sqrt x6)`;;
1032
1033 let gamma3f_x_v_lfun = new_definition
1034 `gamma3f_x_v_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1035     gamma3f_v_lfun  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1036       (sqrt x6)`;;
1037
1038 let gamma3f_x_v0 = new_definition
1039 `gamma3f_x_v0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1040     gamma3f_v0  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1041       (sqrt x6)`;;
1042
1043 let vol3_x_135_s2 = new_definition
1044 `vol3_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1045  vol3r (sqrt x1) (sqrt x3) (sqrt x5) sqrt2`;;
1046
1047 let x1cube = new_definition `x1cube = proj_x1 * proj_x1 * proj_x1`;;
1048
1049 let x1cube = new_definition `x1cube = proj_x1 * proj_x1 * proj_x1`;;
1050
1051
1052
1053 let gamma23f_126_03 = new_definition `gamma23f_126_03 y1 y2 y3 y4 y5 y6 w1 r f =
1054       (gamma3f y1 y2 y6 r f / &w1
1055       + (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 r r r y6 - #0.03) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)) `;;
1056
1057 let gamma23f_red_03 = new_definition `gamma23f_red_03 y1 y2 y3 y4 y5 y6 r f =
1058        (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)`;;
1059
1060 let gamma3f_vLR0 = new_definition `gamma3f_vLR0 y1 y2 y3 y4 y5 y6 =
1061    (dih_y y1 y2 y3 y4 y5 y6 -
1062   dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 -
1063   dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
1064  (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
1065  (&2 * pi)`;;
1066
1067 let gamma3f_vLR_lfun = new_definition `gamma3f_vLR_lfun y1 y2 y3 y4 y5 y6 =
1068 (dih_y y1 y2 y3 y4 y5 y6 -
1069   dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 -
1070   dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
1071  (vol2r y1 sqrt2 -
1072   ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
1073    (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
1074  (&2 * pi) `;;
1075
1076
1077 let  gamma3f_vL0 = new_definition `gamma3f_vL0 y1 y2 y3 y4 y5 y6 =
1078 (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) *
1079  (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
1080  (&2 * pi)   `;;
1081
1082
1083 let gamma3f_vL_lfun = new_definition `gamma3f_vL_lfun y1 y2 y3 y4 y5 y6 =
1084  (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) *
1085  (vol2r y1 sqrt2 -
1086   ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
1087    (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
1088  (&2 * pi)`;;
1089
1090 let  gamma3f_v0 = new_definition `gamma3f_v0 y1 y2 y3 y4 y5 y6 =
1091   (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) *
1092     (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
1093     (&2 * pi)`;;
1094
1095
1096 let gamma3f_v_lfun = new_definition `gamma3f_v_lfun y1 y2 y3 y4 y5 y6 =
1097    (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) *
1098  (vol2r y1 sqrt2 -
1099   ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
1100    (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
1101  (&2 * pi)`;;
1102
1103 let dih_x_126_s2 = new_definition `dih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1104    dih_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
1105
1106 let dih2_x_126_s2 = new_definition `dih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1107    dih2_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
1108
1109 let dih3_x_126_s2 = new_definition `dih3_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1110    dih3_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
1111
1112 let dih4_x_126_s2 = new_definition `dih4_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1113    dih4_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
1114
1115 let dih5_x_126_s2 = new_definition `dih5_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1116    dih5_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
1117
1118 let dih6_x_126_s2 = new_definition `dih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1119    dih6_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
1120
1121 let ldih_x_126_s2 = new_definition `ldih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1122    lfun (sqrt x1 / #2.0) * dih_x_126_s2 x1 x2 x3 x4 x5 x6`;;
1123
1124 let ldih2_x_126_s2 = new_definition `ldih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1125    lfun (sqrt x2 / #2.0) * dih2_x_126_s2 x1 x2 x3 x4 x5 x6`;;
1126
1127 let ldih6_x_126_s2 = new_definition `ldih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1128    lfun (sqrt x6 / #2.0) * dih6_x_126_s2 x1 x2 x3 x4 x5 x6`;;
1129
1130 let dih_x_135_s2 = new_definition `dih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1131    dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
1132
1133 let dih2_x_135_s2 = new_definition `dih2_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1134    dih2_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
1135
1136 let dih3_x_135_s2 = new_definition `dih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1137    dih3_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
1138
1139 let dih4_x_135_s2 = new_definition `dih4_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1140    dih4_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
1141
1142 let dih5_x_135_s2 = new_definition `dih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1143    dih5_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
1144
1145 let dih6_x_135_s2 = new_definition `dih6_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1146    dih6_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
1147
1148 let ldih_x_135_s2' = new_definition `ldih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1149    lfun (sqrt x1/ #2.0) * dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
1150
1151 let ldih3_x_135_s2 = new_definition `ldih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1152    lfun (sqrt x3/ #2.0) * dih3_x_135_s2 x1 x2 x3 x4 x5 x6 `;;
1153
1154 let ldih5_x_135_s2 = new_definition `ldih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1155    lfun (sqrt x5/ #2.0) * dih5_x_135_s2 x1 x2 x3 x4 x5 x6 `;;
1156
1157
1158 let delta_x_126_s2 = new_definition
1159   `delta_x_126_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1160     delta_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
1161
1162 let delta_x_135_s2 = new_definition
1163   `delta_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1164     delta_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
1165
1166 let gamma3f_x_vLR_lfun = new_definition
1167 `gamma3f_x_vLR_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1168     gamma3f_vLR_lfun  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1169       (sqrt x6)`;;
1170
1171 let gamma3f_x_vLR0 = new_definition
1172 `gamma3f_x_vLR0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1173     gamma3f_vLR0  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1174       (sqrt x6)`;;
1175
1176 let gamma3f_x_vL_lfun = new_definition
1177 `gamma3f_x_vL_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1178     gamma3f_vL_lfun  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1179       (sqrt x6)`;;
1180
1181 let gamma3f_x_vL0 = new_definition
1182 `gamma3f_x_vL0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1183     gamma3f_vL0  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1184       (sqrt x6)`;;
1185
1186 let gamma3f_x_v_lfun = new_definition
1187 `gamma3f_x_v_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1188     gamma3f_v_lfun  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1189       (sqrt x6)`;;
1190
1191 let gamma3f_x_v0 = new_definition
1192 `gamma3f_x_v0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1193     gamma3f_v0  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1194       (sqrt x6)`;;
1195
1196 let vol3_x_135_s2 = new_definition
1197 `vol3_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1198  vol3r (sqrt x1) (sqrt x3) (sqrt x5) sqrt2`;;
1199
1200
1201 (*
1202 let arclength6_x  = new_definition `arclength6_x x1 x2 x3 x4 x5 x6 = arclength (sqrt x1) (sqrt x2) (sqrt x3)`;;
1203 *)
1204
1205 let x1cube = new_definition `x1cube = proj_x1 * proj_x1 * proj_x1`;;
1206
1207
1208
1209 let gamma3f_135_s_n = new_definition `gamma3f_135_s_n y1 y2 y3 y4 y5 y6 =
1210   sqn(delta_y y1 y2 y3 y4 y5 y6) *  (&1 / &12 -
1211     (&2 * mm1 / pi) *
1212          (y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6
1213           + y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 +
1214           y_of_x sol_euler345_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) )`;;
1215
1216 let gamma3f_126_s_n = new_definition `gamma3f_126_s_n y1 y2 y3 y4 y5 y6 =
1217   sqn(delta_y y1 y2 y3 y4 y5 y6) *  (&1 / &12 -
1218     (&2 * mm1 / pi) *
1219          (y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6
1220           + y_of_x sol_euler246_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 +
1221           y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) )`;;
1222
1223 let lmdih_x_n = new_definition `lmdih_x_n x1 x2 x3 x4 x5 x6 =
1224   sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
1225
1226 let lmdih2_x_n = new_definition `lmdih2_x_n x1 x2 x3 x4 x5 x6 =
1227   sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
1228
1229 let lmdih3_x_n = new_definition `lmdih3_x_n x1 x2 x3 x4 x5 x6 =
1230   sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
1231
1232 let lmdih5_x_n = new_definition `lmdih5_x_n x1 x2 x3 x4 x5 x6 =
1233   sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih5_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
1234
1235 let lmdih6_x_n = new_definition `lmdih6_x_n x1 x2 x3 x4 x5 x6 =
1236   sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih6_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
1237
1238 let gamma3f_vLR_n = new_definition `gamma3f_vLR_n y1 y2 y3 y4 y5 y6 f =
1239       (dih_y y1 y2 y3 y4 y5 y6 -
1240           upper_dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 -
1241           upper_dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
1242          (vol2r y1 sqrt2 - vol2f y1 sqrt2 f) / (&2 * pi)`;;
1243
1244 let gamma3f_vL_n = new_definition `gamma3f_vL_n y1 y2 y3 y4 y5 y6 f =
1245   (dih_y y1 y2 y3 y4 y5 y6 - upper_dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) *
1246          (vol2r y1 sqrt2 - vol2f y1 sqrt2 f) / (&2 * pi)`;;
1247
1248 let gamma3f_vLR_n0 = new_definition `gamma3f_vLR_n0 y1 y2 y3 y4 y5 y6 =
1249    gamma3f_vLR_n y1 y2 y3 y4 y5 y6 (\x. &0)`;;
1250
1251 let gamma3f_vLR_nlfun = new_definition `gamma3f_vLR_nlfun y1 y2 y3 y4 y5 y6 =
1252   gamma3f_vLR_n y1 y2 y3 y4 y5 y6 lfun`;;
1253
1254 let  gamma3f_vL_n0 = new_definition `gamma3f_vL_n0 y1 y2 y3 y4 y5 y6 =
1255   gamma3f_vL_n y1 y2 y3 y4 y5 y6 (\x. &0)`;;
1256
1257 let gamma3f_vL_nlfun = new_definition `gamma3f_vL_nlfun y1 y2 y3 y4 y5 y6 =
1258   gamma3f_vL_n y1 y2 y3 y4 y5 y6 lfun`;;
1259
1260 let ldih_x_n = new_definition `ldih_x_n x1 x2 x3 x4 x5 x6 =
1261   sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
1262
1263 let ldih2_x_n = new_definition `ldih2_x_n x1 x2 x3 x4 x5 x6 =
1264   sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
1265
1266 let ldih3_x_n = new_definition `ldih3_x_n x1 x2 x3 x4 x5 x6 =
1267   sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
1268
1269 let ldih5_x_n = new_definition `ldih5_x_n x1 x2 x3 x4 x5 x6 =
1270   sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih5_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
1271
1272 let ldih6_x_n = new_definition `ldih6_x_n x1 x2 x3 x4 x5 x6 =
1273   sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih6_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
1274
1275 let gamma3f_vLR_x_nlfun = new_definition `gamma3f_vLR_x_nlfun x1 x2 x3 x4 x5 x6=
1276     gamma3f_vLR_nlfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
1277
1278 let gamma3f_vL_x_nlfun = new_definition `gamma3f_vL_x_nlfun x1 x2 x3 x4 x5 x6=
1279     gamma3f_vL_nlfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
1280
1281 let gamma3f_vLR_x_n0 = new_definition `gamma3f_vLR_x_n0 x1 x2 x3 x4 x5 x6=
1282     gamma3f_vLR_n0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
1283
1284 let gamma3f_vL_x_n0 = new_definition `gamma3f_vL_x_n0 x1 x2 x3 x4 x5 x6=
1285     gamma3f_vL_n0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
1286
1287 let gamma3f_135_x_s_n = new_definition
1288   `gamma3f_135_x_s_n x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1289     gamma3f_135_s_n (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
1290
1291 let gamma3f_126_x_s_n = new_definition
1292   `gamma3f_126_x_s_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1293    gamma3f_126_s_n (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
1294
1295 let rr22 = REWRITE_RULE[GSYM sqrt2_sqrt2];;
1296
1297 let ldih_x_126_n = rr22 (new_definition `ldih_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1298    ldih_x_n x1 x2 (&2) (&2) (&2) x6`);;
1299
1300 (*
1301 let ldih2_x_126_n = rr22 (new_definition
1302 `ldih2_x_126_n_ x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1303    ldih2_x_n x1 x2 (&2) (&2) (&2) x6`);;
1304 *)
1305
1306 let ldih2_x_126_n = rr22 (new_definition
1307 `ldih2_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1308    ldih2_x_n x1 x2 (&2) (&2) (&2) x6`);;
1309
1310 let ldih6_x_126_n = rr22 (new_definition
1311  `ldih6_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1312    ldih6_x_n x1 x2 (&2) (&2) (&2) x6`);;
1313
1314 let ldih_x_135_n = rr22 (new_definition
1315  `ldih_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1316    ldih_x_n x1  (&2) x3 (&2) x5 (&2)`);;
1317
1318 let ldih3_x_135_n = rr22 (new_definition
1319 `ldih3_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1320    ldih3_x_n x1  (&2) x3 (&2) x5 (&2)`);;
1321
1322 let ldih5_x_135_n = rr22 (new_definition
1323  `ldih5_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1324    ldih5_x_n x1  (&2) x3 (&2) x5 (&2)`);;
1325
1326 (*
1327 let vol3f_sqrt2_lfun = new_definition
1328   `vol3f_sqrt2_lfun y1 y2 (y3:real) (y4:real) (y5:real) y6 =
1329     vol3f y1 y2 y6 sqrt2 lfun`;;
1330 *)
1331
1332 (* remaining splits *)
1333
1334 let gamma3f_126 = new_definition
1335  `gamma3f_126 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f =
1336    gamma3f y1 y2 y6 sqrt2 f`;;
1337
1338 let gamma3f_135 = new_definition
1339  `gamma3f_135 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f  =
1340    gamma3f y1 y3 y5 sqrt2 f`;;
1341
1342 let gamma3f_vLR = new_definition
1343  `gamma3f_vLR (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f  =
1344   (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
1345   (vol2r y1 sqrt2 - vol2f y1 sqrt2 f)/(&2 * pi)`;;
1346
1347 let gamma3f_vL = new_definition
1348  `gamma3f_vL (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f  =
1349   (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) * (vol2r y1 sqrt2 - vol2f y1 sqrt2 f)/(&2 * pi)`;;
1350
1351 let gamma3f_v = new_definition
1352  `gamma3f_v (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f  =
1353   (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 sqrt2 - vol2f y1 sqrt2 f)/(&2 * pi)`;;
1354
1355 let gamma23f = new_definition `gamma23f y1 y2 y3 y4 y5 y6 w1 w2 r f =
1356       (gamma3f y1 y2 y6 r f / &w1 + gamma3f y1 y3 y5 r f / &w2
1357       + (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 r r r y6 - dih_y y1 y3 r r r y5) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)) `;;
1358
1359 let gamma23f_126_03 = new_definition `gamma23f_126_03 y1 y2 y3 y4 y5 y6 w1 r f =
1360       (gamma3f y1 y2 y6 r f / &w1
1361       + (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 r r r y6 - #0.03) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)) `;;
1362
1363 let gamma23f_red_03 = new_definition `gamma23f_red_03 y1 y2 y3 y4 y5 y6 r f =
1364        (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)`;;
1365
1366 let gamma3f_vLR0 = new_definition `gamma3f_vLR0 y1 y2 y3 y4 y5 y6 =
1367    (dih_y y1 y2 y3 y4 y5 y6 -
1368   dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 -
1369   dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
1370  (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
1371  (&2 * pi)`;;
1372
1373 let gamma3f_vLR_lfun = new_definition `gamma3f_vLR_lfun y1 y2 y3 y4 y5 y6 =
1374 (dih_y y1 y2 y3 y4 y5 y6 -
1375   dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 -
1376   dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
1377  (vol2r y1 sqrt2 -
1378   ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
1379    (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
1380  (&2 * pi) `;;
1381
1382
1383 let  gamma3f_vL0 = new_definition `gamma3f_vL0 y1 y2 y3 y4 y5 y6 =
1384 (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) *
1385  (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
1386  (&2 * pi)   `;;
1387
1388
1389 let gamma3f_vL_lfun = new_definition `gamma3f_vL_lfun y1 y2 y3 y4 y5 y6 =
1390  (dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) *
1391  (vol2r y1 sqrt2 -
1392   ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
1393    (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
1394  (&2 * pi)`;;
1395
1396 let  gamma3f_v0 = new_definition `gamma3f_v0 y1 y2 y3 y4 y5 y6 =
1397   (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) *
1398     (vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
1399     (&2 * pi)`;;
1400
1401
1402 let gamma3f_v_lfun = new_definition `gamma3f_v_lfun y1 y2 y3 y4 y5 y6 =
1403    (dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) *
1404  (vol2r y1 sqrt2 -
1405   ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
1406    (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
1407  (&2 * pi)`;;
1408
1409 let dih_x_126_s2 = new_definition `dih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1410    dih_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
1411
1412 let dih2_x_126_s2 = new_definition `dih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1413    dih2_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
1414
1415 let dih3_x_126_s2 = new_definition `dih3_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1416    dih3_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
1417
1418 let dih4_x_126_s2 = new_definition `dih4_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1419    dih4_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
1420
1421 let dih5_x_126_s2 = new_definition `dih5_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1422    dih5_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
1423
1424 let dih6_x_126_s2 = new_definition `dih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1425    dih6_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
1426
1427 let ldih_x_126_s2 = new_definition `ldih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1428    lfun (sqrt x1 / #2.0) * dih_x_126_s2 x1 x2 x3 x4 x5 x6`;;
1429
1430 let ldih2_x_126_s2 = new_definition `ldih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1431    lfun (sqrt x2 / #2.0) * dih2_x_126_s2 x1 x2 x3 x4 x5 x6`;;
1432
1433 let ldih6_x_126_s2 = new_definition `ldih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
1434    lfun (sqrt x6 / #2.0) * dih6_x_126_s2 x1 x2 x3 x4 x5 x6`;;
1435
1436 let dih_x_135_s2 = new_definition `dih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1437    dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
1438
1439 let dih2_x_135_s2 = new_definition `dih2_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1440    dih2_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
1441
1442 let dih3_x_135_s2 = new_definition `dih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1443    dih3_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
1444
1445 let dih4_x_135_s2 = new_definition `dih4_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1446    dih4_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
1447
1448 let dih5_x_135_s2 = new_definition `dih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1449    dih5_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
1450
1451 let dih6_x_135_s2 = new_definition `dih6_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1452    dih6_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
1453
1454 let ldih_x_135_s2' = new_definition `ldih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1455    lfun (sqrt x1/ #2.0) * dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2  (sqrt x5) sqrt2`;;
1456
1457 let ldih3_x_135_s2 = new_definition `ldih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1458    lfun (sqrt x3/ #2.0) * dih3_x_135_s2 x1 x2 x3 x4 x5 x6 `;;
1459
1460 let ldih5_x_135_s2 = new_definition `ldih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
1461    lfun (sqrt x5/ #2.0) * dih5_x_135_s2 x1 x2 x3 x4 x5 x6 `;;
1462
1463
1464 let delta_x_126_s2 = new_definition
1465   `delta_x_126_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1466     delta_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
1467
1468 let delta_x_135_s2 = new_definition
1469   `delta_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1470     delta_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
1471
1472 let gamma3f_x_vLR_lfun = new_definition
1473 `gamma3f_x_vLR_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1474     gamma3f_vLR_lfun  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1475       (sqrt x6)`;;
1476
1477 let gamma3f_x_vLR0 = new_definition
1478 `gamma3f_x_vLR0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1479     gamma3f_vLR0  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1480       (sqrt x6)`;;
1481
1482 let gamma3f_x_vL_lfun = new_definition
1483 `gamma3f_x_vL_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1484     gamma3f_vL_lfun  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1485       (sqrt x6)`;;
1486
1487 let gamma3f_x_vL0 = new_definition
1488 `gamma3f_x_vL0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1489     gamma3f_vL0  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1490       (sqrt x6)`;;
1491
1492 let gamma3f_x_v_lfun = new_definition
1493 `gamma3f_x_v_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1494     gamma3f_v_lfun  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1495       (sqrt x6)`;;
1496
1497 let gamma3f_x_v0 = new_definition
1498 `gamma3f_x_v0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1499     gamma3f_v0  (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
1500       (sqrt x6)`;;
1501
1502 let vol3_x_135_s2 = new_definition
1503 `vol3_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
1504  vol3r (sqrt x1) (sqrt x3) (sqrt x5) sqrt2`;;
1505
1506 (*
1507 let dih_y_div_sqrtdelta_posbranch = new_definition
1508   `dih_y_div_sqrtdelta_posbranch  = y_of_x dih_x_div_sqrtdelta_posbranch`;;
1509 *)
1510
1511
1512 (*
1513 let rhof_x = define `rhof_x x = rho (sqrt x)`;;
1514 *)
1515
1516
1517 (*
1518 let ineq_lemma = prove_by_refinement(
1519   `!a x b. &0 <= a  /\  &0 <= b /\  a pow 2 <= x /\ x <= b pow 2 ==> a <= sqrt x /\ sqrt x <= b`,
1520   (* {{{ proof *)
1521   [
1522   REPEAT GEN_TAC;
1523     STRIP_TAC;
1524     SUBGOAL_THEN `&0 <= x` MP_TAC;
1525   ASM_MESON_TAC [REAL_LE_TRANS;Collect_geom.REAL_LE_SQUARE_POW];
1526   ASM_MESON_TAC[Collect_geom.POW2_COND;SQRT_WORKS];
1527   ]);;
1528   (* }}} *)
1529 *)
1530
1531 (*
1532 let arclength6_x  = new_definition `arclength6_x x1 x2 x3 x4 x5 x6 = arclength (sqrt x1) (sqrt x2) (sqrt x3)`;;
1533 *)
1534
1535 (*
1536
1537 let sqrt_x8 = define `sqrt_x8 (x7:real) (x2:real) (x3:real) (x4:real) (x8:real) (x9:real) = sqrt x8`;;
1538
1539 let sqrt_x9 = define `sqrt_x9 (x7:real) (x2:real) (x3:real) (x4:real) (x8:real) (x9:real) = sqrt x9`;;
1540
1541 *)
1542
1543
1544
1545
1546