(*
May 2012, definitions no longer needed in
primary verifications of flyspeck.
*)
(*
deprecated May 2012:
arclength_x_345
taum_hexall_x
dih_hexall_x
dih1_hexall_x
upper_dih_hexall_x
delta_hexall_x
delta4_hexall_x
eulerA_hexall_x
factor345_hexall_x
law_cosines_234_x
law_cosines_126_x
delta_template_B_x
dih_template_B_x
taum_template_B_x
delta_top_x
tau_lowform_x
tau_m_diff_quotient
tau_m_diff_quotient2
*)
(*
7/29/2009:
* normball deprecated. Replace normball x r with ball(x,r)
* rect deprecated. Use interval instead.
* wedge is now defined by Harrison using azim. He has proved a lemma giving the equivalence with the previous definition.
* azim in defined by Harrison.
* directed_angle is now defined through complex Arg.
* definition of polar cycle has been changed (again).
* a lemma is needed relating atn2 to Arg.
* cone -> cone0
* deprecated: volume_props.
*)
(* deleted obsolete definitions 2/7/2010 svn 1471:
obsolete definitions:
obsolete: rad2_y, d3, mk_vec3, real3_of_triple, triple_of_real3,
obsolete: conv, radius -> norm(vector[x;y]),
obsolete: polar_angle -> Arg(vector[x;y]),
obsolete: polar_c, less_polar, min_polar,
obsolete: iter_SPEC, iter -> ITER,
obsolete: azim_cycle_hyp_def, azim_cycle_spec, azim_cycle_def,
obsolete: rogers, rogers0, azim_hyp_def, azim_spec, azim_def,
2011-08-01.
obsolete: polar_cycle
*)
(* terms moved to Harrison's flyspeck.ml
NULLSET_RULES,
solid_triangle, ellipsoid, conic_cap, frustum, frustt,
primitive, MEASURABLE_RULES, solid, coplanar, cross, wedge, azim,
*)
(* (now voronoi_open) let voronoi = new_definition `voronoi v S = { x | !w. ((S w) /\ ~(w=v)) ==> (dist( x, v) < dist( x, w)) }`;; *)
(* DEPRECATED, 2011-08-01, not used
let directed_angle = new_definition `directed_angle (x,y) (x',y') =
Arg (complex(x',y') / complex(x,y))`;;
let cyclic_order = new_definition `cyclic_order v u w =
((directed_angle v u < directed_angle v w) \/
((directed_angle v u = directed_angle v w) /\ (radius u <= radius w)))`;;
let polar_cycle = new_definition `polar_cycle V v =
if (V SUBSET {v}) then v else (@ u. ~(u=v) /\ V u /\
(!w. ~(w = v) /\ V w ==> cyclic_order v u w))`;;
*)
(*
let sol_euler_y = `sol_euler_y y1 y2 y3 y4 y5 y6 =
(let a = y1*y2*y3 + y1*(y2*y2 + y3*y3 - y4*y4)/ &2 +
y2*(y1*y1 + y3*y3 - y5*y5)/ &2 + y3*(y1*y1 + y2*y2 - y6*y6)/ &2 in
&2 * atn2( &2 * a, sqrt (delta_y y1 y2 y3 y4 y5 y6)))`;;
let sol_euler_y = `sol_euler_y = y_of_x sol_euler_x`;;
*)
(*
let acs_sqrt_x1 = new_definition `acs_sqrt_x1 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
acs (sqrt(x1))`;;
let acs_sqrt_x2 = new_definition `acs_sqrt_x2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
acs (sqrt(x2))`;;
*)
(* deprecated
let solRy = new_definition `solRy y1 y2 y6 c = solR (y1/ &2) (eta_y y1 y2 y6) c`;;
let dihRy = new_definition `dihRy y1 y2 y6 c = dihR (y1/ &2) (eta_y y1 y2 y6) c`;;
*)
(* deprecated *)
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)`;;
(*
let tauq_x = new_definition
`tauq_x x1 x2 x3 x4 x5 x6 x7 x8 x9 =
tauq (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) (sqrt x7) (sqrt x8) (sqrt x9)`;;
*)
let taum_hexall_x = new_definition
`taum_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) =
taum_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12) +
flat_term_x x2`;;
(* deprecated *)
let dih_hexall_x = new_definition `dih_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) =
dih_x x1 x2 x4 ((&2 * h0) pow 2) x14 x12 -
dih_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;;
let dih1_hexall_x = new_definition `dih1_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) =
dih_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;;
let upper_dih_hexall_x = new_definition `upper_dih_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) =
dih_x x1 x2 x4 ((&2 * h0) pow 2) x14 x12 -
upper_dih_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;;
let delta_hexall_x = new_definition `delta_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) =
delta_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;;
let delta4_hexall_x = new_definition `delta4_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) =
delta_x4 x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;;
(*
let euler_ap = new_definition `euler_ap y1 y2 y3 y4 y5 y6 =
y1*y2*y3 + y1*(y2*y2 + y3*y3 - y4*y4)/ &2 + y2*(y1*y1 + y3*y3 - y5*y5)/ &2 +
y3*(y1*y1 + y2*y2 - y6*y6)/ &2`;;
*)
let eulerA_hexall_x = new_definition `eulerA_hexall_x x14 x12 x23 x1 x2 x3 x4 x5 (x6:real) =
eulerA_x x1 x3 x4 x5 x14 (edge_flat2_x x2 x1 x3 (&0) x23 x12)`;;
let factor345_hexall_x = new_definition `factor345_hexall_x c (x1:real) (x2:real) x3 x4 x5 (x6:real) =
x5 -x3 -x4 + &2 * c * sqrt(x3) * sqrt(x4)`;;
let law_cosines_234_x = new_definition
`law_cosines_234_x c (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
x4 -x2 -x3 + &2 * c * sqrt(x2) * sqrt(x3)`;;
let law_cosines_126_x = new_definition
`law_cosines_126_x c (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
x6 -x1 -x2 + &2 * c * sqrt(x1) * sqrt(x2)`;;
(* -- not used
let taum_sub156_x = new_definition
`taum_sub156_x x1s x5s x6s (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
taum_x x1s x2 x3 x4 x5s x6s`;;
*)
(* DEPRECATED.
let tau_nullform_x = new_definition
`tau_nullform_x x1 x2 x3 x4 x5 x6 =
rho (sqrt x1) * pi - (pi + sol0) +
sqp(delta_x x1 x2 x3 x4 x5 x6) * tau_residual_x x1 x2 x3 x4 x5 x6`;;
*)
(* deprecated *)
let delta_template_B_x = new_definition
`delta_template_B_x x15 x45 x34 x12 x1 x2 x3 x4 x5 (x6:real) =
(let x23 = x12 in
let x13 = edge_flat2_x x2 x1 x3 (&0) x23 x12 in
let x14 = edge_flat2_x x5 x1 x4 (&0) x45 x15 in
(delta_x x1 x3 x4 x34 x14 x13))`;;
let dih_template_B_x = new_definition
`dih_template_B_x x15 x45 x34 x12 x25 x1 x2 x3 x4 x5 (x6:real) =
(let x23 = x12 in
let x13 = edge_flat2_x x2 x1 x3 (&0) x23 x12 in
let x14 = edge_flat2_x x5 x1 x4 (&0) x45 x15 in
(dih_x x1 x2 x5 x25 x15 x12 - dih_x x1 x3 x4 x34 x14 x13))`;;
let taum_template_B_x = new_definition
`taum_template_B_x x15 x45 x34 x12 x1 x2 x3 x4 x5 (x6:real) =
(let x23 = x12 in
let x13 = edge_flat2_x x2 x1 x3 (&0) x23 x12 in
let x14 = edge_flat2_x x5 x1 x4 (&0) x45 x15 in
(taum_x x1 x3 x4 x34 x14 x13 +flat_term_x x2 + flat_term_x x5))`;;
(* No longer needed.... deprecated. *)
let delta_top_x = new_definition
`delta_top_x (a:real) (x1:real) (x2:real) (x3:real) (x4:real)
(x5:real) (x6:real) (x7:real) (x8:real) (x9:real) =
delta_y (sqrt x4) (sqrt x9) (sqrt x6) a (sqrt x5) (sqrt x8)`;;
(* tau_lowform_x intended for use when dih1 > pi/2, dih2, dih3 < pi/2,
tau_residual <0,
Then tau_lowform_x is a lower bound on tau (that is graceful when delta->0).
*)
let tau_lowform_x = new_definition
`tau_lowform_x x1 x2 x3 x4 x5 x6 =
(let d = delta_x x1 x2 x3 x4 x5 x6 in
(rho (sqrt x1) * pi - (pi + sol0) +
sqp d * rhazim_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 +
sqn d * rhazim2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 +
sqn d * rhazim3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6))`;;
let tau_m_diff_quotient = new_definition
`tau_m_diff_quotient (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) =
(let eps = #0.000001 in
(taum (y1 + eps) y2 y3 y4 y5 y6 - taum y1 y2 y3 y4 y5 y6)/eps)`;;
let tau_m_diff_quotient2 = new_definition
`tau_m_diff_quotient2 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) =
(let eps = #0.000001 in
(taum (y1 + eps) y2 y3 y4 y5 y6 - taum y1 y2 y3 y4 y5 y6
+ taum (y1 - eps) y2 y3 y4 y5 y6)/(eps pow 2))`;;
(* deleted 2013-08-18 *)
let delta_y_LC = new_definition
`delta_y_LC (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) =
delta_y y1 y2 y3 y4 y5 y6`;;
let mardih_x = new_definition `mardih_x x1 x2 x3 x4 x5 x6 =
marchal_quartic (sqrt x1 / #2.0) * dih_x x1 x2 x3 x4 x5 x6`;;
let mardih2_x = new_definition `mardih2_x x1 x2 x3 x4 x5 x6 =
marchal_quartic (sqrt x2 / #2.0) * dih2_x x1 x2 x3 x4 x5 x6`;;
let mardih3_x = new_definition `mardih3_x x1 x2 x3 x4 x5 x6 =
marchal_quartic (sqrt x3 / #2.0) * dih3_x x1 x2 x3 x4 x5 x6`;;
let mardih4_x = new_definition `mardih4_x x1 x2 x3 x4 x5 x6 =
marchal_quartic (sqrt x4 / #2.0) * dih4_x x1 x2 x3 x4 x5 x6`;;
let mardih5_x = new_definition `mardih5_x x1 x2 x3 x4 x5 x6 =
marchal_quartic (sqrt x5 / #2.0) * dih5_x x1 x2 x3 x4 x5 x6`;;
let mardih6_x = new_definition `mardih6_x x1 x2 x3 x4 x5 x6 =
marchal_quartic (sqrt x6 / #2.0) * dih6_x x1 x2 x3 x4 x5 x6`;;
(* c++ associations:
("mardih_x","marchalDih"); ("mardih2_x","marchalDih2");
("mardih3_x","marchalDih3");
("mardih4_x","marchalDih4"); ("mardih5_x","marchalDih5");
("mardih6_x","marchalDih6");
*)
(*
(*
num1 is based on the following Mathematica calculation. It is the
numerator of the a-partial derivative of taumarE.
num2 is the numerator of second a-partial
formal proof: derived_form_sum_dih444
*)
taumarE = e1 Dihedral[2, 2, 2, a, b, c] + e2 Dihedral[2, 2, 2, b, c, a] +
e3 Dihedral[2, 2, 2, c, a, b];
afac = a (16 - a^2);
sd = Sqrt[Delta[2, 2, 2, a, b, c]];
abcsub = {a -> 2.1, b -> 2.2, c -> 2.3, e1 -> 5.5, e2 -> 5.6,
e3 -> 5.7, ssd -> sd, aafac -> afac};
abcsq = {a -> Sqrt[a2], b -> Sqrt[b2], c -> Sqrt[c2]};
taumarE1 = 4 a afac e1/(aafac ssd);
taumarE2 = 4 (-8 b^2 + a^2 (-8 + b^2) + 8 c^2) e2/(aafac ssd) ;
taumarE3 = 4 (-8 c^2 + a^2 (-8 + c^2) + 8 b^2) e3/(aafac ssd);
(D[taumarE, a] - taumarE1 - taumarE2 - taumarE3 //. abcsub) // Chop (*0*)
num1e = aafac ssd (taumarE1 + taumarE2 + taumarE3) // Together // Simplify;
num1sqI = -4*(a2^2*e1 + 8*(
b2 - c2)*(e2 - e3) - a2*(16*e1 + (-8 + b2)*e2 + (-8 + c2)*e3)); (* num1
in sphere.hl *)
(num1e /. abcsq) - num1sqI (*0*)
(* second derivatives *)
taumarE1D2calc = D[Dihedral[2, 2, 2, a, b, c], {a,
2}] // Together // Simplify;
taumarE1D2 = -(16*(-a^4 + (b^2 - c^2)^2)) afac^2 /(aafac^2 ssd^3);
(taumarE1D2calc - taumarE1D2 //. abcsub) // Chop
taumarE2D2calc = D[Dihedral[2, 2, 2, b, c, a], {a, 2}] // Together //
Simplify;
taumarE2D2 = -(8*(6*a^8*(-8 + b^2) + 256*(
b^2 - c^2)^3 + a^6*(b^4*(-8 + c^2) - 16*b^2*(3 + c^2) + 16*(
16 + 9*c^2)) - 16*a^2*(b^6 + b^4*(
80 - 13*c^2) - 3*c^4*(16 + c^2) + b^2*
c^2*(-32 +
15*c^2)) + 2*a^4*(b^6 + b^4*(56 -
10*c^2) - 24*c^2*(16 + 3*c^2) + b^2*(
384 + 16*c^2 + 9*c^4))))/(aafac^2 ssd^3);
(taumarE2D2calc - taumarE2D2 //. abcsub) // Chop
taumarE3D2calc = D[Dihedral[2, 2, 2, c, a, b], {a,
2}] // Together // Simplify;
taumarE3D2 = -(8*(-256*(b^2 - c^2)^3 + 6*a^8*(-8 + c^2) + 16*a^2*
(3*b^6 + b^4*(48 - 15*c^2) - c^4*(80 + c^2) + b^2*
c^2*(32 + 13*c^2)) +
a^6*(b^2*(144 - 16*c^2 + c^4) - 8*(-32 + 6*c^2 + c^4)) + 2*
a^4*(9*b^4*(-8 + c^2) + c^2*(384 + 56*c^2 + c^4) - 2*b^2*(192 - 8*
c^2 + 5*c^4))))/(aafac^2 ssd^3);
(taumarE3D2calc - taumarE3D2 //. abcsub) // Chop
taumarD2num = (e1 taumarE1D2 + e2 taumarE2D2 + e3
taumarE3D2) (aafac^2 ssd^3) // Simplify
taumarD2numDef = (taumarD2num /. abcsq) // HolForm; (* num2 in sphere.hl *)
(((D[taumarE, {a, 2}]) aafac^2 ssd^3 - taumarD2num) //. abcsub) // Chop
(* analysis near a2 -> 16 *)
{"near a2->16", DeltaX[4,
4, 4, 16, b2, c2] // Factor, (num1sqI /. a2 -> 16) // Factor,
((taumarD2num /. abcsq) /. a2 -> 16) // Factor}
*)
let num2 = new_definition `num2 e1 e2 e3 a2 b2 c2 =
(&8 * ((&2 * ((a2 pow 5) * e1)) + (((-- &256) * (((b2 + ((-- &1) * c2)) pow 3)
* (e2 + ((-- &1) * e3)))) + (((-- &1) * ((a2 pow 3) * ((&2 * (((-- &256) +
((b2 pow 2) + (((-- &2) * (b2 * c2)) + (c2 pow 2)))) * e1)) + (((((b2 pow 2)
* ((-- &8) + c2)) + (((-- &16) * (b2 * (&3 + c2))) + (&16 * (&16 + (&9 *
c2))))) * e2) + (((b2 * (&144 + (((-- &16) * c2) + (c2 pow 2)))) + ((-- &8) *
((-- &32) + ((&6 * c2) + (c2 pow 2))))) * e3))))) + (((a2 pow 4) * (((-- &64)
* e1) + ((-- &6) * ((((-- &8) + b2) * e2) + (((-- &8) + c2) * e3))))) + (((--
&2) * ((a2 pow 2) * ((b2 + ((-- &1) * c2)) * (((b2 pow 2) * e2) + ((&8 * (c2
* ((&4 * e1) + ((&9 * e2) + ((-- &7) * e3))))) + ((&384 * (e2 + ((-- &1) *
e3))) + (((-- &1) * ((c2 pow 2) * e3)) + (b2 * (((-- &32) * e1) + (((&56 +
((-- &9) * c2)) * e2) + (&9 * (((-- &8) + c2) * e3)))))))))))) + (&16 * (a2 *
((b2 + ((-- &1) * c2)) * (((b2 pow 2) * (e2 + ((-- &3) * e3))) + (((-- &4) *
(b2 * ((&8 * e1) + ((((-- &20) + (&3 * c2)) * e2) + ((-- &3) * (((-- &4) +
c2) * e3)))))) + (c2 * ((&32 * e1) + ((&3 * ((&16 + c2) * e2)) + ((-- &1) *
((&80 + c2) * e3))))))))))))))))`;;
let rat1 = new_definition `rat1 e1 e2 e3 a2 b2 c2 =
num1 e1 e2 e3 a2 b2 c2 /
(sqrt(delta_x (&4) (&4) (&4) a2 b2 c2) * sqrt(a2) * (&16 - a2))`;;
let rat2 = new_definition `rat2 e1 e2 e3 a2 b2 c2 =
num2 e1 e2 e3 a2 b2 c2 /
(((sqrt(delta_x (&4) (&4) (&4) a2 b2 c2)) pow 3) * a2 * ((&16 - a2) pow 2))`;;
(* num1^2 - #0.01 * num2 *)
let num_combo1 = new_definition `num_combo1 e1 e2 e3 a2 b2 c2 =
((&2 / &25) * (((-- &2) * ((a2 pow 5) * e1)) + ((&256 * (((b2 + ((-- &1) *
c2)) pow 3) * (e2 + ((-- &1) * e3)))) + (((a2 pow 3) * ((&2 * (((-- &256) +
((b2 pow 2) + (((-- &2) * (b2 * c2)) + (c2 pow 2)))) * e1)) + (((((b2 pow 2)
* ((-- &8) + c2)) + (((-- &16) * (b2 * (&3 + c2))) + (&16 * (&16 + (&9 *
c2))))) * e2) + (((b2 * (&144 + (((-- &16) * c2) + (c2 pow 2)))) + ((-- &8) *
((-- &32) + ((&6 * c2) + (c2 pow 2))))) * e3)))) + ((&2 * ((a2 pow 4) * ((&32
* e1) + (&3 * ((((-- &8) + b2) * e2) + (((-- &8) + c2) * e3)))))) + ((&200 *
((((a2 pow 2) * e1) + ((&8 * ((b2 + ((-- &1) * c2)) * (e2 + ((-- &1) * e3))))
+ ((-- &1) * (a2 * ((&16 * e1) + ((((-- &8) + b2) * e2) + (((-- &8) + c2) *
e3))))))) pow 2)) + ((&2 * ((a2 pow 2) * ((b2 + ((-- &1) * c2)) * (((b2 pow 2)
* e2) + ((&8 * (c2 * ((&4 * e1) + ((&9 * e2) + ((-- &7) * e3))))) + ((&384 *
(e2 + ((-- &1) * e3))) + (((-- &1) * ((c2 pow 2) * e3)) + (b2 * (((-- &32) *
e1) + (((&56 + ((-- &9) * c2)) * e2) + (&9 * (((-- &8) + c2) *
e3)))))))))))) + ((-- &16) * (a2 * ((b2 + ((-- &1) * c2)) * (((b2 pow 2) *
(e2 + ((-- &3) * e3))) + (((-- &4) * (b2 * ((&8 * e1) + ((((-- &20) + (&3 *
c2)) * e2) + ((-- &3) * (((-- &4) + c2) * e3)))))) + (c2 * ((&32 * e1) + ((&3
* ((&16 + c2) * e2)) + ((-- &1) * ((&80 + c2) * e3)))))))))))))))))`;;
(* x_A is a special case of x_C: *)
(*
let truncate_gamma23_x_A = new_definition `truncate_gamma23_x_A iw1 m1 m2 m6 =
scalar6
(compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
iw1
+ (dih_x - (mk_126 (truncate_dih_x (#0.14)) + constant6 (#0.08))) *
uni((truncate_gamma2_x m1), proj_x1)`;;
*)
let truncate_gamma23_x_C = new_definition `truncate_gamma23_x_C d iw1 m1 m2 m6 =
scalar6
(compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
iw1
+ (dih_x - (mk_126 (truncate_dih_x (#0.14)) + constant6 (d))) *
uni((truncate_gamma2_x m1), proj_x1)`;;
let truncate_gamma23_x_B = new_definition
`truncate_gamma23_x_B m1 =
(dih_x - constant6 (&2 * #0.08)) *
uni((truncate_gamma2_x m1),proj_x1)`;;
(* function truncate_gamma2_x deprecated. It is incorrect. See gamma2_x_div_azim_v2 *)
let truncate_gamma2_x =
new_definition `truncate_gamma2_x m x = (&8 - x)* sqrt x / (&24) -
( (&2 * mm1/ pi) * (&1 - sqrt x / sqrt8) -
(&8 * mm2 / pi) * m * lfun (sqrt x / &2))`;;
let truncate_gamma3f_x = new_definition `truncate_gamma3f_x d m4 m5 m6 =
truncate_vol3r_456 d -
truncate_vol3f d m4 m5 m6`;;
let truncate_gamma23_x = new_definition `truncate_gamma23_x iw1 iw2 m1 m2 m3 m5 m6 =
scalar6
(compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
iw1 +
scalar6
(compose6 (truncate_gamma3f_x (#0.14) m1 m3 m5)
dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5)
iw2
+ (dih_x -
(mk_126 (truncate_dih_x (#0.14)) +
mk_135 (truncate_dih_x (#0.14)))) *
uni((truncate_gamma2_x m1),proj_x1)`;;
(* version for large azimuth angles *)
let truncate_gamma23a_x = new_definition `
truncate_gamma23a_x iw1 iw2 m1 m2 m3 m5 m6 x1 x2 x3 az4 x5 x6 =
truncate_gamma3f_x (&0) m1 m2 m6 (&0) (&0) (&0) x1 x2 x6 * iw1 +
truncate_gamma3f_x (&0) m1 m3 m5 (&0) (&0) (&0) x1 x3 x5 * iw2 +
(az4 -
(dih_x x1 x2 (&2) (&2) (&2) x6 +
dih_x x1 (&2) x3 (&2) x5 (&2))) *
truncate_gamma2_x m1 x1`;;
let truncate_gamma2_x =
new_definition `truncate_gamma2_x m x = (&8 - x)* sqrt x / (&24) -
( (&2 * mm1/ pi) * (&1 - sqrt x / sqrt8) -
(&8 * mm2 / pi) * m * lfun (sqrt x / &2))`;;
let truncate_gamma3f_x = new_definition `truncate_gamma3f_x d m4 m5 m6 =
truncate_vol3r_456 d -
truncate_vol3f d m4 m5 m6`;;
let truncate_gamma23_x = new_definition `truncate_gamma23_x iw1 iw2 m1 m2 m3 m5 m6 =
scalar6
(compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
iw1 +
scalar6
(compose6 (truncate_gamma3f_x (#0.14) m1 m3 m5)
dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5)
iw2
+ (dih_x -
(mk_126 (truncate_dih_x (#0.14)) +
mk_135 (truncate_dih_x (#0.14)))) *
uni((truncate_gamma2_x m1),proj_x1)`;;
(* version for large azimuth angles *)
let truncate_gamma23a_x = new_definition `
truncate_gamma23a_x iw1 iw2 m1 m2 m3 m5 m6 x1 x2 x3 az4 x5 x6 =
truncate_gamma3f_x (&0) m1 m2 m6 (&0) (&0) (&0) x1 x2 x6 * iw1 +
truncate_gamma3f_x (&0) m1 m3 m5 (&0) (&0) (&0) x1 x3 x5 * iw2 +
(az4 -
(dih_x x1 x2 (&2) (&2) (&2) x6 +
dih_x x1 (&2) x3 (&2) x5 (&2))) *
truncate_gamma2_x m1 x1`;;
let truncate_sqrt = new_definition `
truncate_sqrt c x = if (x <= c) then sqrt(c) else sqrt(x)`;;
let truncate_dih_x = new_definition(`truncate_dih_x c x1 x2 x3 x4 x5 x6 =
let d_x4 = delta_x4 x1 x2 x3 x4 x5 x6 in
let d = delta_x x1 x2 x3 x4 x5 x6 in
pi/ (&2) + atn2( (sqrt ((&4) * x1) * truncate_sqrt c d),-- d_x4)`);;
let truncate_sol_x = new_definition
`truncate_sol_x c = truncate_dih_x c +
(rotate2 (truncate_dih_x c)) +
(rotate3 (truncate_dih_x c)) - constant6 (pi)`;;
let truncate_vol_x =new_definition
`truncate_vol_x c = scalar6 (uni((truncate_sqrt c),delta_x)) (&1 / &12)`;;
let truncate_vol3r_456 = new_definition `truncate_vol3r_456 c =
mk_456 (truncate_vol_x c)`;;
(* new 6/18 *)
let truncate_vol3f = new_definition `truncate_vol3f c m4 m5 m6 =
scalar6 ( mk_456 (rotate5 (truncate_sol_x c)) +
mk_456 (rotate6 (truncate_sol_x c)) +
mk_456 (rotate4 (truncate_sol_x c))
) (&2 * mm1/ pi)
-
scalar6 (
(scalar6 (uni(lfun,(scalar6 proj_y4 #0.5))) m4) *
mk_456 (rotate4 (truncate_dih_x c)) +
(scalar6 (uni(lfun,(scalar6 proj_y5 #0.5))) m5) *
mk_456 (rotate5 (truncate_dih_x c)) +
(scalar6 (uni(lfun,(scalar6 proj_y6 #0.5))) m6) *
mk_456 (rotate6 (truncate_dih_x c))
) (&8 * mm2 / pi)`;;
let truncate_sqrt = new_definition `
truncate_sqrt c x = if (x <= c) then sqrt(c) else sqrt(x)`;;
let truncate_dih_x = new_definition(`truncate_dih_x c x1 x2 x3 x4 x5 x6 =
let d_x4 = delta_x4 x1 x2 x3 x4 x5 x6 in
let d = delta_x x1 x2 x3 x4 x5 x6 in
pi/ (&2) + atn2( (sqrt ((&4) * x1) * truncate_sqrt c d),-- d_x4)`);;
let truncate_sol_x = new_definition
`truncate_sol_x c = truncate_dih_x c +
(rotate2 (truncate_dih_x c)) +
(rotate3 (truncate_dih_x c)) - constant6 (pi)`;;
let truncate_vol_x =new_definition
`truncate_vol_x c = scalar6 (uni((truncate_sqrt c),delta_x)) (&1 / &12)`;;
let truncate_vol3r_456 = new_definition `truncate_vol3r_456 c =
mk_456 (truncate_vol_x c)`;;
(* new 6/18 *)
let truncate_vol3f = new_definition `truncate_vol3f c m4 m5 m6 =
scalar6 ( mk_456 (rotate5 (truncate_sol_x c)) +
mk_456 (rotate6 (truncate_sol_x c)) +
mk_456 (rotate4 (truncate_sol_x c))
) (&2 * mm1/ pi)
-
scalar6 (
(scalar6 (uni(lfun,(scalar6 proj_y4 #0.5))) m4) *
mk_456 (rotate4 (truncate_dih_x c)) +
(scalar6 (uni(lfun,(scalar6 proj_y5 #0.5))) m5) *
mk_456 (rotate5 (truncate_dih_x c)) +
(scalar6 (uni(lfun,(scalar6 proj_y6 #0.5))) m6) *
mk_456 (rotate6 (truncate_dih_x c))
) (&8 * mm2 / pi)`;;
(* in delta_pent_x: nonstandard ordering of variables, x6 swapped with x3 *)
let delta_pent_x = new_definition
`delta_pent_x (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
delta_x x1 x2 x6 (&4) (&4) (#3.24 pow 2)`;;
(*
Upper approximation to Sqrt on [0,1]:
sqp = 3/8 + (3*x)/4 - x^2/8 + (1 - x)^3 (0.7 x - 0.25);
Sqp[x_]:= If[x<1,3/8 + (3*x)/4 - x^2/8 + (1 - x)^3 (0.7 x - 0.25),Sqrt[x]];
DeltaX4[x1_, x2_, x3_, x4_, x5_, x6_] := -(x2*x3) - x1*x4 +
x2*x5 + x3*x6 - x5*x6 + x1*(-x1 + x2 + x3 - x4 + x5 + x6);
Matan[x_] := ArcTan[Sqrt[x]]/Sqrt[x];
UpperDihX[x1_, x2_, x3_, x4_, x5_, x6_] := Module[{d, d4},
d = DeltaX[x1, x2, x3, x4, x5, x6];
d4 = DeltaX4[x1, x2, x3, x4, x5, x6];
2 Sqrt[x1] Sqp[d]/d4 * Matan[4 x1 d/d4^2]];
UpperDihY[y1_, y2_, y3_, y4_, y5_, y6_] :=
UpperDihX @@ ({y1, y2, y3, y4, y5, y6}^2);
Lower approx to sqrt on [0,1]:
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;
Thm: if y1,y2,y3 >= 2, then Dihedral[sqrt2,y1,y2,y3,sqrt2,sqrt2] >= pi/2,
(and delta_x4 <= 0). Proof: Imagine the cube of side sqrt2. qed.
The case of equality delta_x4=0 occurs when y3=2, and y1 or y2=2.
Thm: if y1,y2,y3 in [2,sqrt8], then Dihedral[y1,y2,sqrt2,sqrt2,sqrt2,y6] <= pi/2
(and delta_x4 >= 0). Proof. The triangle y1,y2,y3 is acute, so the circumcenter lands inside.
*)
let sqp = new_definition `sqp x =
if (x < &1) then
&3 / &8 + (&1 - x) pow 3 * (-- #0.25 + #0.7 * x) +
&3 * x / &4 - x * x/ &8 else sqrt x`;;
let sqn = new_definition `sqn x =
if (x < &1)
then #0.375 + (&3*x)/ &4 - (x pow 2)/ &8 - #0.3*((&1 - x) pow 3)*(x pow 2) +
((&1 - x) pow 3)*(-- #0.375 + #1.3*(&1 - x)*x)
else sqrt x`;;
(* upper bound on dih (when delta_x4 > 0), useful when delta is near 0 and angle is near 0.
Also pi + upper_dih_x is a lower bound on dih when (delta_x4 < 0), useful when delta is
near 0 and angle is near pi. *)
let upper_dih_x = new_definition `upper_dih_x x1 x2 x3 x4 x5 x6 =
(let d = delta_x x1 x2 x3 x4 x5 x6 in
let d4 = delta_x4 x1 x2 x3 x4 x5 x6 in (
&2 * sqrt x1 * sqp d *
matan (&4 * x1 * d / (d4 pow 2) ) / d4))`;;
let upper_dih_y = new_definition `upper_dih_y = y_of_x upper_dih_x`;;
let gamma3f_135_n = new_definition `gamma3f_135_n y1 y2 y3 y4 y5 y6 =
sqn(delta_y y1 y2 y3 y4 y5 y6) * (&1 / &12 -
( (&2 * mm1 / pi) *
(y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6
+ y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 +
y_of_x sol_euler345_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) -
(&8 * mm2 / pi) *
(y_of_x lmdih_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 +
y_of_x lmdih3_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 +
y_of_x lmdih5_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6)
))`;;
let gamma3f_126_n = new_definition `gamma3f_126_n y1 y2 y3 y4 y5 y6 =
sqn(delta_y y1 y2 y3 y4 y5 y6) * (&1 / &12 -
( (&2 * mm1 / pi) *
(y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6
+ y_of_x sol_euler246_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 +
y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) -
(&8 * mm2 / pi) *
(y_of_x lmdih_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 +
y_of_x lmdih2_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6 +
y_of_x lmdih6_x_div_sqrtdelta_posbranch y1 y2 y3 y4 y5 y6)
))`;;
let gamma23f_n = new_definition `gamma23f_n y1 y2 y3 y4 y5 y6 w1 w2 r f =
gamma3f_126_n y1 y2 sqrt2 sqrt2 sqrt2 y6 / &w1 +
gamma3f_135_n y1 sqrt2 y3 sqrt2 y5 sqrt2 / &w2 +
(dih_y y1 y2 y3 y4 y5 y6 -
upper_dih_y y1 y2 r r r y6 -
upper_dih_y y1 y3 r r r y5) *
(vol2r y1 r - vol2f y1 r f) / (&2 * pi)`;;
let gamma23f_126_03_n = new_definition
`gamma23f_126_03_n y1 y2 y3 y4 y5 y6 w1 r f =
gamma3f_126_n y1 y2 sqrt2 sqrt2 sqrt2 y6 / &w1 +
(dih_y y1 y2 y3 y4 y5 y6 - upper_dih_y y1 y2 r r r y6 - #0.03) *
(vol2r y1 r - vol2f y1 r f) / (&2 * pi)`;;
let euler_3flat_x = new_definition
`euler_3flat_x x1 x2 x3 x23 x13 x12 =
let x5 = edge_flat2_x x13 x1 x3 (&0) (&4) (&4) in
let x6 = edge_flat2_x x12 x1 x2 (&0) (&4) (&4) in
let x4 = edge_flat2_x x23 x2 x3 (&0) (&4) (&4) in
(eulerA_x x1 x2 x3 x4 x5 x6)`;;
let euler_2flat_x = new_definition
`euler_2flat_x x1 x2 x3 x4 x13 x12 =
let x5 = edge_flat2_x x13 x1 x3 (&0) (&4) (&4) in
let x6 = edge_flat2_x x12 x1 x2 (&0) (&4) (&4) in
(eulerA_x x1 x2 x3 x4 x5 x6)`;;
let euler_1flat_x = new_definition
`euler_1flat_x x1 x2 x3 x4 x5 x12 =
let x6 = edge_flat2_x x12 x1 x2 (&0) (&4) (&4) in
(eulerA_x x1 x2 x3 x4 x5 x6)`;;
let taum_3flat_x = new_definition
`taum_3flat_x x1 x2 x3 x23 x13 x12 =
let x5 = edge_flat2_x x13 x1 x3 (&0) (&4) (&4) in
let x6 = edge_flat2_x x12 x1 x2 (&0) (&4) (&4) in
let x4 = edge_flat2_x x23 x2 x3 (&0) (&4) (&4) in
(taum_x x1 x2 x3 x4 x5 x6 + flat_term_x x12 + flat_term_x x23 + flat_term_x x13)`;;
let taum_2flat_x = new_definition
`taum_2flat_x x1 x2 x3 x4 x13 x12 =
let x5 = edge_flat2_x x13 x1 x3 (&0) (&4) (&4) in
let x6 = edge_flat2_x x12 x1 x2 (&0) (&4) (&4) in
(taum_x x1 x2 x3 x4 x5 x6 + flat_term_x x12 + flat_term_x x13)`;;
let taum_1flat_x = new_definition
`taum_1flat_x x1 x2 x3 x4 x5 x12 =
let x6 = edge_flat2_x x12 x1 x2 (&0) (&4) (&4) in
(taum_x x1 x2 x3 x4 x5 x6 + flat_term_x x12)`;;
(* DEPRECATED 2013-05-25.
let sphere= new_definition`sphere x=(?(v:real^3)(r:real). (r> &0)/\ (x={w:real^3 | norm (w-v)= r}))`;;
*)
(* deprecated 2013-2-13.
let beta = new_definition(`beta psi theta =
let arg = ((cos psi)*(cos psi) - (cos theta)*(cos theta))/
((&1) - (cos theta)*(cos theta)) in
(acs (sqrt arg))`);;
*)
(* deprecated 2013-2-13.
let radius = new_definition `radius (x,y) = sqrt((x pow 2) + (y pow 2))`;;
*)
(* DEPRECATED added May 11, 2013. x4 st. delta_x = 50, removed May 24, 2013.
let edge_flat50 = new_definition`edge_flat50 y1 y2 y3 y5 y6 =
sqrt(quadratic_root_plus (abc_of_quadratic (
\x4. &50 - delta_x (y1*y1) (y2*y2) (y3*y3) x4 (y5*y5) (y6*y6))))`;;
let edge_flat250_x = new_definition `edge_flat250_x x1 x2 x3 x4 x5 x6 =
(edge_flat (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x5) (sqrt x6)) pow 2`;; (* x4 dummy *)
let edge_flat50_x = new_definition`edge_flat50_x x1 x2 x3 (x4:real) x5 x6 =
edge_flat (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x5) (sqrt x6)`;;
*)
(* deprecated, Dec 1, 2012 , replaced with beta_bumpA_y *)
(*
let beta_bump_y = new_definition `beta_bump_y y1 y2 y3 y4 y5 y6 =
(if critical_edge_y y1 then &1 else &0) *
(if critical_edge_y y2 then &0 else &1) *
(if critical_edge_y y3 then &0 else &1) *
(if critical_edge_y y4 then &1 else &0) *
(if critical_edge_y y5 then &0 else &1) *
(if critical_edge_y y6 then &0 else &1) *
(bump (y1/ &2) - bump (y4 / &2))`;;
*)
(*
let delta_x6 = new_definition
`delta_x6 x1 x2 x3 x4 x5 x6 = -- x1 *x2 + x1 *x4 + x2* x5 - x4* x5 + x3* (x1 + x2 - x3 + x4 + x5 - x6) -
x3 * x6`;;
*)
let gamma3f_135_s_n = new_definition `gamma3f_135_s_n y1 y2 y3 y4 y5 y6 =
sqn(delta_y y1 y2 y3 y4 y5 y6) * (&1 / &12 -
(&2 * mm1 / pi) *
(y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6
+ y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 +
y_of_x sol_euler345_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) )`;;
let gamma3f_126_s_n = new_definition `gamma3f_126_s_n y1 y2 y3 y4 y5 y6 =
sqn(delta_y y1 y2 y3 y4 y5 y6) * (&1 / &12 -
(&2 * mm1 / pi) *
(y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6
+ y_of_x sol_euler246_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 +
y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) )`;;
let lmdih_x_n = new_definition `lmdih_x_n x1 x2 x3 x4 x5 x6 =
sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let lmdih2_x_n = new_definition `lmdih2_x_n x1 x2 x3 x4 x5 x6 =
sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let lmdih3_x_n = new_definition `lmdih3_x_n x1 x2 x3 x4 x5 x6 =
sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let lmdih5_x_n = new_definition `lmdih5_x_n x1 x2 x3 x4 x5 x6 =
sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih5_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let lmdih6_x_n = new_definition `lmdih6_x_n x1 x2 x3 x4 x5 x6 =
sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih6_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let gamma3f_vLR_n = new_definition `gamma3f_vLR_n y1 y2 y3 y4 y5 y6 f =
(dih_y y1 y2 y3 y4 y5 y6 -
upper_dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 -
upper_dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
(vol2r y1 sqrt2 - vol2f y1 sqrt2 f) / (&2 * pi)`;;
let gamma3f_vL_n = new_definition `gamma3f_vL_n y1 y2 y3 y4 y5 y6 f =
(dih_y y1 y2 y3 y4 y5 y6 - upper_dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) *
(vol2r y1 sqrt2 - vol2f y1 sqrt2 f) / (&2 * pi)`;;
let gamma3f_vLR_n0 = new_definition `gamma3f_vLR_n0 y1 y2 y3 y4 y5 y6 =
gamma3f_vLR_n y1 y2 y3 y4 y5 y6 (\x. &0)`;;
let gamma3f_vLR_nlfun = new_definition `gamma3f_vLR_nlfun y1 y2 y3 y4 y5 y6 =
gamma3f_vLR_n y1 y2 y3 y4 y5 y6 lfun`;;
let gamma3f_vL_n0 = new_definition `gamma3f_vL_n0 y1 y2 y3 y4 y5 y6 =
gamma3f_vL_n y1 y2 y3 y4 y5 y6 (\x. &0)`;;
let gamma3f_vL_nlfun = new_definition `gamma3f_vL_nlfun y1 y2 y3 y4 y5 y6 =
gamma3f_vL_n y1 y2 y3 y4 y5 y6 lfun`;;
let ldih_x_n = new_definition `ldih_x_n x1 x2 x3 x4 x5 x6 =
sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let ldih2_x_n = new_definition `ldih2_x_n x1 x2 x3 x4 x5 x6 =
sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let ldih3_x_n = new_definition `ldih3_x_n x1 x2 x3 x4 x5 x6 =
sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let ldih5_x_n = new_definition `ldih5_x_n x1 x2 x3 x4 x5 x6 =
sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih5_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let ldih6_x_n = new_definition `ldih6_x_n x1 x2 x3 x4 x5 x6 =
sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih6_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let gamma3f_vLR_x_nlfun = new_definition `gamma3f_vLR_x_nlfun x1 x2 x3 x4 x5 x6=
gamma3f_vLR_nlfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
let gamma3f_vL_x_nlfun = new_definition `gamma3f_vL_x_nlfun x1 x2 x3 x4 x5 x6=
gamma3f_vL_nlfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
let gamma3f_vLR_x_n0 = new_definition `gamma3f_vLR_x_n0 x1 x2 x3 x4 x5 x6=
gamma3f_vLR_n0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
let gamma3f_vL_x_n0 = new_definition `gamma3f_vL_x_n0 x1 x2 x3 x4 x5 x6=
gamma3f_vL_n0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
let gamma3f_135_x_s_n = new_definition
`gamma3f_135_x_s_n x1 (x2:real) x3 (x4:real) x5 (x6:real) =
gamma3f_135_s_n (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let gamma3f_126_x_s_n = new_definition
`gamma3f_126_x_s_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_126_s_n (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let rr22 = REWRITE_RULE[GSYM sqrt2_sqrt2];;
let ldih_x_126_n = rr22 (new_definition `ldih_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 =
ldih_x_n x1 x2 (&2) (&2) (&2) x6`);;
(*
let ldih2_x_126_n = rr22 (new_definition
`ldih2_x_126_n_ x1 x2 (x3:real) (x4:real) (x5:real) x6 =
ldih2_x_n x1 x2 (&2) (&2) (&2) x6`);;
*)
let ldih2_x_126_n = rr22 (new_definition
`ldih2_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 =
ldih2_x_n x1 x2 (&2) (&2) (&2) x6`);;
let ldih6_x_126_n = rr22 (new_definition
`ldih6_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 =
ldih6_x_n x1 x2 (&2) (&2) (&2) x6`);;
let ldih_x_135_n = rr22 (new_definition
`ldih_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
ldih_x_n x1 (&2) x3 (&2) x5 (&2)`);;
let ldih3_x_135_n = rr22 (new_definition
`ldih3_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
ldih3_x_n x1 (&2) x3 (&2) x5 (&2)`);;
let ldih5_x_135_n = rr22 (new_definition
`ldih5_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
ldih5_x_n x1 (&2) x3 (&2) x5 (&2)`);;
(*
let vol3f_sqrt2_lfun = new_definition
`vol3f_sqrt2_lfun y1 y2 (y3:real) (y4:real) (y5:real) y6 =
vol3f y1 y2 y6 sqrt2 lfun`;;
*)
(* remaining splits *)
let gamma3f_126 = new_definition
`gamma3f_126 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f =
gamma3f y1 y2 y6 sqrt2 f`;;
let gamma3f_135 = new_definition
`gamma3f_135 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f =
gamma3f y1 y3 y5 sqrt2 f`;;
let gamma3f_vLR = new_definition
`gamma3f_vLR (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f =
(dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
(vol2r y1 sqrt2 - vol2f y1 sqrt2 f)/(&2 * pi)`;;
let gamma3f_vL = new_definition
`gamma3f_vL (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f =
(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)`;;
let gamma3f_v = new_definition
`gamma3f_v (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f =
(dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 sqrt2 - vol2f y1 sqrt2 f)/(&2 * pi)`;;
let gamma23f_126_03 = new_definition `gamma23f_126_03 y1 y2 y3 y4 y5 y6 w1 r f =
(gamma3f y1 y2 y6 r f / &w1
+ (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)) `;;
let gamma23f_red_03 = new_definition `gamma23f_red_03 y1 y2 y3 y4 y5 y6 r f =
(dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)`;;
let gamma3f_vLR0 = new_definition `gamma3f_vLR0 y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 -
dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 -
dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
(vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
(&2 * pi)`;;
let gamma3f_vLR_lfun = new_definition `gamma3f_vLR_lfun y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 -
dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 -
dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
(vol2r y1 sqrt2 -
((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
(&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
(&2 * pi) `;;
let gamma3f_vL0 = new_definition `gamma3f_vL0 y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) *
(vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
(&2 * pi) `;;
let gamma3f_vL_lfun = new_definition `gamma3f_vL_lfun y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) *
(vol2r y1 sqrt2 -
((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
(&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
(&2 * pi)`;;
let gamma3f_v0 = new_definition `gamma3f_v0 y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) *
(vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
(&2 * pi)`;;
let gamma3f_v_lfun = new_definition `gamma3f_v_lfun y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) *
(vol2r y1 sqrt2 -
((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
(&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
(&2 * pi)`;;
let dih_x_126_s2 = new_definition `dih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let dih2_x_126_s2 = new_definition `dih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih2_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let dih3_x_126_s2 = new_definition `dih3_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih3_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let dih4_x_126_s2 = new_definition `dih4_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih4_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let dih5_x_126_s2 = new_definition `dih5_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih5_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let dih6_x_126_s2 = new_definition `dih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih6_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let ldih_x_126_s2 = new_definition `ldih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
lfun (sqrt x1 / #2.0) * dih_x_126_s2 x1 x2 x3 x4 x5 x6`;;
let ldih2_x_126_s2 = new_definition `ldih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
lfun (sqrt x2 / #2.0) * dih2_x_126_s2 x1 x2 x3 x4 x5 x6`;;
let ldih6_x_126_s2 = new_definition `ldih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
lfun (sqrt x6 / #2.0) * dih6_x_126_s2 x1 x2 x3 x4 x5 x6`;;
let dih_x_135_s2 = new_definition `dih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let dih2_x_135_s2 = new_definition `dih2_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih2_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let dih3_x_135_s2 = new_definition `dih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih3_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let dih4_x_135_s2 = new_definition `dih4_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih4_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let dih5_x_135_s2 = new_definition `dih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih5_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let dih6_x_135_s2 = new_definition `dih6_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih6_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let ldih_x_135_s2' = new_definition `ldih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
lfun (sqrt x1/ #2.0) * dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let ldih3_x_135_s2 = new_definition `ldih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
lfun (sqrt x3/ #2.0) * dih3_x_135_s2 x1 x2 x3 x4 x5 x6 `;;
let ldih5_x_135_s2 = new_definition `ldih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
lfun (sqrt x5/ #2.0) * dih5_x_135_s2 x1 x2 x3 x4 x5 x6 `;;
let delta_x_126_s2 = new_definition
`delta_x_126_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
delta_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let delta_x_135_s2 = new_definition
`delta_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
delta_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let gamma3f_x_vLR_lfun = new_definition
`gamma3f_x_vLR_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_vLR_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let gamma3f_x_vLR0 = new_definition
`gamma3f_x_vLR0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_vLR0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let gamma3f_x_vL_lfun = new_definition
`gamma3f_x_vL_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_vL_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let gamma3f_x_vL0 = new_definition
`gamma3f_x_vL0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_vL0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let gamma3f_x_v_lfun = new_definition
`gamma3f_x_v_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_v_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let gamma3f_x_v0 = new_definition
`gamma3f_x_v0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_v0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let vol3_x_135_s2 = new_definition
`vol3_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
vol3r (sqrt x1) (sqrt x3) (sqrt x5) sqrt2`;;
let x1cube = new_definition `x1cube = proj_x1 * proj_x1 * proj_x1`;;
let x1cube = new_definition `x1cube = proj_x1 * proj_x1 * proj_x1`;;
let gamma23f_126_03 = new_definition `gamma23f_126_03 y1 y2 y3 y4 y5 y6 w1 r f =
(gamma3f y1 y2 y6 r f / &w1
+ (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)) `;;
let gamma23f_red_03 = new_definition `gamma23f_red_03 y1 y2 y3 y4 y5 y6 r f =
(dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)`;;
let gamma3f_vLR0 = new_definition `gamma3f_vLR0 y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 -
dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 -
dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
(vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
(&2 * pi)`;;
let gamma3f_vLR_lfun = new_definition `gamma3f_vLR_lfun y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 -
dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 -
dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
(vol2r y1 sqrt2 -
((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
(&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
(&2 * pi) `;;
let gamma3f_vL0 = new_definition `gamma3f_vL0 y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) *
(vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
(&2 * pi) `;;
let gamma3f_vL_lfun = new_definition `gamma3f_vL_lfun y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) *
(vol2r y1 sqrt2 -
((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
(&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
(&2 * pi)`;;
let gamma3f_v0 = new_definition `gamma3f_v0 y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) *
(vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
(&2 * pi)`;;
let gamma3f_v_lfun = new_definition `gamma3f_v_lfun y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) *
(vol2r y1 sqrt2 -
((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
(&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
(&2 * pi)`;;
let dih_x_126_s2 = new_definition `dih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let dih2_x_126_s2 = new_definition `dih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih2_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let dih3_x_126_s2 = new_definition `dih3_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih3_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let dih4_x_126_s2 = new_definition `dih4_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih4_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let dih5_x_126_s2 = new_definition `dih5_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih5_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let dih6_x_126_s2 = new_definition `dih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih6_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let ldih_x_126_s2 = new_definition `ldih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
lfun (sqrt x1 / #2.0) * dih_x_126_s2 x1 x2 x3 x4 x5 x6`;;
let ldih2_x_126_s2 = new_definition `ldih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
lfun (sqrt x2 / #2.0) * dih2_x_126_s2 x1 x2 x3 x4 x5 x6`;;
let ldih6_x_126_s2 = new_definition `ldih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
lfun (sqrt x6 / #2.0) * dih6_x_126_s2 x1 x2 x3 x4 x5 x6`;;
let dih_x_135_s2 = new_definition `dih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let dih2_x_135_s2 = new_definition `dih2_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih2_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let dih3_x_135_s2 = new_definition `dih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih3_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let dih4_x_135_s2 = new_definition `dih4_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih4_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let dih5_x_135_s2 = new_definition `dih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih5_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let dih6_x_135_s2 = new_definition `dih6_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih6_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let ldih_x_135_s2' = new_definition `ldih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
lfun (sqrt x1/ #2.0) * dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let ldih3_x_135_s2 = new_definition `ldih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
lfun (sqrt x3/ #2.0) * dih3_x_135_s2 x1 x2 x3 x4 x5 x6 `;;
let ldih5_x_135_s2 = new_definition `ldih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
lfun (sqrt x5/ #2.0) * dih5_x_135_s2 x1 x2 x3 x4 x5 x6 `;;
let delta_x_126_s2 = new_definition
`delta_x_126_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
delta_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let delta_x_135_s2 = new_definition
`delta_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
delta_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let gamma3f_x_vLR_lfun = new_definition
`gamma3f_x_vLR_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_vLR_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let gamma3f_x_vLR0 = new_definition
`gamma3f_x_vLR0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_vLR0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let gamma3f_x_vL_lfun = new_definition
`gamma3f_x_vL_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_vL_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let gamma3f_x_vL0 = new_definition
`gamma3f_x_vL0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_vL0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let gamma3f_x_v_lfun = new_definition
`gamma3f_x_v_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_v_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let gamma3f_x_v0 = new_definition
`gamma3f_x_v0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_v0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let vol3_x_135_s2 = new_definition
`vol3_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
vol3r (sqrt x1) (sqrt x3) (sqrt x5) sqrt2`;;
(*
let arclength6_x = new_definition `arclength6_x x1 x2 x3 x4 x5 x6 = arclength (sqrt x1) (sqrt x2) (sqrt x3)`;;
*)
let x1cube = new_definition `x1cube = proj_x1 * proj_x1 * proj_x1`;;
let gamma3f_135_s_n = new_definition `gamma3f_135_s_n y1 y2 y3 y4 y5 y6 =
sqn(delta_y y1 y2 y3 y4 y5 y6) * (&1 / &12 -
(&2 * mm1 / pi) *
(y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6
+ y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 +
y_of_x sol_euler345_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) )`;;
let gamma3f_126_s_n = new_definition `gamma3f_126_s_n y1 y2 y3 y4 y5 y6 =
sqn(delta_y y1 y2 y3 y4 y5 y6) * (&1 / &12 -
(&2 * mm1 / pi) *
(y_of_x sol_euler_x_div_sqrtdelta y1 y2 y3 y4 y5 y6
+ y_of_x sol_euler246_x_div_sqrtdelta y1 y2 y3 y4 y5 y6 +
y_of_x sol_euler156_x_div_sqrtdelta y1 y2 y3 y4 y5 y6) )`;;
let lmdih_x_n = new_definition `lmdih_x_n x1 x2 x3 x4 x5 x6 =
sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let lmdih2_x_n = new_definition `lmdih2_x_n x1 x2 x3 x4 x5 x6 =
sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let lmdih3_x_n = new_definition `lmdih3_x_n x1 x2 x3 x4 x5 x6 =
sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let lmdih5_x_n = new_definition `lmdih5_x_n x1 x2 x3 x4 x5 x6 =
sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih5_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let lmdih6_x_n = new_definition `lmdih6_x_n x1 x2 x3 x4 x5 x6 =
sqn (delta_x x1 x2 x3 x4 x5 x6) * lmdih6_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let gamma3f_vLR_n = new_definition `gamma3f_vLR_n y1 y2 y3 y4 y5 y6 f =
(dih_y y1 y2 y3 y4 y5 y6 -
upper_dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 -
upper_dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
(vol2r y1 sqrt2 - vol2f y1 sqrt2 f) / (&2 * pi)`;;
let gamma3f_vL_n = new_definition `gamma3f_vL_n y1 y2 y3 y4 y5 y6 f =
(dih_y y1 y2 y3 y4 y5 y6 - upper_dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) *
(vol2r y1 sqrt2 - vol2f y1 sqrt2 f) / (&2 * pi)`;;
let gamma3f_vLR_n0 = new_definition `gamma3f_vLR_n0 y1 y2 y3 y4 y5 y6 =
gamma3f_vLR_n y1 y2 y3 y4 y5 y6 (\x. &0)`;;
let gamma3f_vLR_nlfun = new_definition `gamma3f_vLR_nlfun y1 y2 y3 y4 y5 y6 =
gamma3f_vLR_n y1 y2 y3 y4 y5 y6 lfun`;;
let gamma3f_vL_n0 = new_definition `gamma3f_vL_n0 y1 y2 y3 y4 y5 y6 =
gamma3f_vL_n y1 y2 y3 y4 y5 y6 (\x. &0)`;;
let gamma3f_vL_nlfun = new_definition `gamma3f_vL_nlfun y1 y2 y3 y4 y5 y6 =
gamma3f_vL_n y1 y2 y3 y4 y5 y6 lfun`;;
let ldih_x_n = new_definition `ldih_x_n x1 x2 x3 x4 x5 x6 =
sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let ldih2_x_n = new_definition `ldih2_x_n x1 x2 x3 x4 x5 x6 =
sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let ldih3_x_n = new_definition `ldih3_x_n x1 x2 x3 x4 x5 x6 =
sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let ldih5_x_n = new_definition `ldih5_x_n x1 x2 x3 x4 x5 x6 =
sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih5_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let ldih6_x_n = new_definition `ldih6_x_n x1 x2 x3 x4 x5 x6 =
sqn(delta_x x1 x2 x3 x4 x5 x6) * ldih6_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`;;
let gamma3f_vLR_x_nlfun = new_definition `gamma3f_vLR_x_nlfun x1 x2 x3 x4 x5 x6=
gamma3f_vLR_nlfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
let gamma3f_vL_x_nlfun = new_definition `gamma3f_vL_x_nlfun x1 x2 x3 x4 x5 x6=
gamma3f_vL_nlfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
let gamma3f_vLR_x_n0 = new_definition `gamma3f_vLR_x_n0 x1 x2 x3 x4 x5 x6=
gamma3f_vLR_n0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
let gamma3f_vL_x_n0 = new_definition `gamma3f_vL_x_n0 x1 x2 x3 x4 x5 x6=
gamma3f_vL_n0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6)`;;
let gamma3f_135_x_s_n = new_definition
`gamma3f_135_x_s_n x1 (x2:real) x3 (x4:real) x5 (x6:real) =
gamma3f_135_s_n (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let gamma3f_126_x_s_n = new_definition
`gamma3f_126_x_s_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_126_s_n (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let rr22 = REWRITE_RULE[GSYM sqrt2_sqrt2];;
let ldih_x_126_n = rr22 (new_definition `ldih_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 =
ldih_x_n x1 x2 (&2) (&2) (&2) x6`);;
(*
let ldih2_x_126_n = rr22 (new_definition
`ldih2_x_126_n_ x1 x2 (x3:real) (x4:real) (x5:real) x6 =
ldih2_x_n x1 x2 (&2) (&2) (&2) x6`);;
*)
let ldih2_x_126_n = rr22 (new_definition
`ldih2_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 =
ldih2_x_n x1 x2 (&2) (&2) (&2) x6`);;
let ldih6_x_126_n = rr22 (new_definition
`ldih6_x_126_n x1 x2 (x3:real) (x4:real) (x5:real) x6 =
ldih6_x_n x1 x2 (&2) (&2) (&2) x6`);;
let ldih_x_135_n = rr22 (new_definition
`ldih_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
ldih_x_n x1 (&2) x3 (&2) x5 (&2)`);;
let ldih3_x_135_n = rr22 (new_definition
`ldih3_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
ldih3_x_n x1 (&2) x3 (&2) x5 (&2)`);;
let ldih5_x_135_n = rr22 (new_definition
`ldih5_x_135_n x1 (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
ldih5_x_n x1 (&2) x3 (&2) x5 (&2)`);;
(*
let vol3f_sqrt2_lfun = new_definition
`vol3f_sqrt2_lfun y1 y2 (y3:real) (y4:real) (y5:real) y6 =
vol3f y1 y2 y6 sqrt2 lfun`;;
*)
(* remaining splits *)
let gamma3f_126 = new_definition
`gamma3f_126 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f =
gamma3f y1 y2 y6 sqrt2 f`;;
let gamma3f_135 = new_definition
`gamma3f_135 (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f =
gamma3f y1 y3 y5 sqrt2 f`;;
let gamma3f_vLR = new_definition
`gamma3f_vLR (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f =
(dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
(vol2r y1 sqrt2 - vol2f y1 sqrt2 f)/(&2 * pi)`;;
let gamma3f_vL = new_definition
`gamma3f_vL (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f =
(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)`;;
let gamma3f_v = new_definition
`gamma3f_v (y1:real) (y2:real) (y3:real) (y4:real) (y5:real) (y6:real) f =
(dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 sqrt2 - vol2f y1 sqrt2 f)/(&2 * pi)`;;
let gamma23f = new_definition `gamma23f y1 y2 y3 y4 y5 y6 w1 w2 r f =
(gamma3f y1 y2 y6 r f / &w1 + gamma3f y1 y3 y5 r f / &w2
+ (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)) `;;
let gamma23f_126_03 = new_definition `gamma23f_126_03 y1 y2 y3 y4 y5 y6 w1 r f =
(gamma3f y1 y2 y6 r f / &w1
+ (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)) `;;
let gamma23f_red_03 = new_definition `gamma23f_red_03 y1 y2 y3 y4 y5 y6 r f =
(dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) * (vol2r y1 r - vol2f y1 r f)/(&2 * pi)`;;
let gamma3f_vLR0 = new_definition `gamma3f_vLR0 y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 -
dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 -
dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
(vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
(&2 * pi)`;;
let gamma3f_vLR_lfun = new_definition `gamma3f_vLR_lfun y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 -
dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 -
dih_y y1 y3 sqrt2 sqrt2 sqrt2 y5) *
(vol2r y1 sqrt2 -
((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
(&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
(&2 * pi) `;;
let gamma3f_vL0 = new_definition `gamma3f_vL0 y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) *
(vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
(&2 * pi) `;;
let gamma3f_vL_lfun = new_definition `gamma3f_vL_lfun y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 - dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - #0.03) *
(vol2r y1 sqrt2 -
((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
(&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
(&2 * pi)`;;
let gamma3f_v0 = new_definition `gamma3f_v0 y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) *
(vol2r y1 sqrt2 - (&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2))) /
(&2 * pi)`;;
let gamma3f_v_lfun = new_definition `gamma3f_v_lfun y1 y2 y3 y4 y5 y6 =
(dih_y y1 y2 y3 y4 y5 y6 - &2 * #0.03) *
(vol2r y1 sqrt2 -
((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
(&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
(&2 * pi)`;;
let dih_x_126_s2 = new_definition `dih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let dih2_x_126_s2 = new_definition `dih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih2_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let dih3_x_126_s2 = new_definition `dih3_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih3_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let dih4_x_126_s2 = new_definition `dih4_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih4_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let dih5_x_126_s2 = new_definition `dih5_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih5_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let dih6_x_126_s2 = new_definition `dih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
dih6_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let ldih_x_126_s2 = new_definition `ldih_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
lfun (sqrt x1 / #2.0) * dih_x_126_s2 x1 x2 x3 x4 x5 x6`;;
let ldih2_x_126_s2 = new_definition `ldih2_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
lfun (sqrt x2 / #2.0) * dih2_x_126_s2 x1 x2 x3 x4 x5 x6`;;
let ldih6_x_126_s2 = new_definition `ldih6_x_126_s2 x1 x2 (x3:real) (x4:real) (x5:real) x6 =
lfun (sqrt x6 / #2.0) * dih6_x_126_s2 x1 x2 x3 x4 x5 x6`;;
let dih_x_135_s2 = new_definition `dih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let dih2_x_135_s2 = new_definition `dih2_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih2_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let dih3_x_135_s2 = new_definition `dih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih3_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let dih4_x_135_s2 = new_definition `dih4_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih4_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let dih5_x_135_s2 = new_definition `dih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih5_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let dih6_x_135_s2 = new_definition `dih6_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
dih6_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let ldih_x_135_s2' = new_definition `ldih_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
lfun (sqrt x1/ #2.0) * dih_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let ldih3_x_135_s2 = new_definition `ldih3_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
lfun (sqrt x3/ #2.0) * dih3_x_135_s2 x1 x2 x3 x4 x5 x6 `;;
let ldih5_x_135_s2 = new_definition `ldih5_x_135_s2 x1 (x2:real) x3 (x4:real) x5 (x6:real) =
lfun (sqrt x5/ #2.0) * dih5_x_135_s2 x1 x2 x3 x4 x5 x6 `;;
let delta_x_126_s2 = new_definition
`delta_x_126_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
delta_y (sqrt x1) (sqrt x2) sqrt2 sqrt2 sqrt2 (sqrt x6)`;;
let delta_x_135_s2 = new_definition
`delta_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
delta_y (sqrt x1) sqrt2 (sqrt x3) sqrt2 (sqrt x5) sqrt2`;;
let gamma3f_x_vLR_lfun = new_definition
`gamma3f_x_vLR_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_vLR_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let gamma3f_x_vLR0 = new_definition
`gamma3f_x_vLR0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_vLR0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let gamma3f_x_vL_lfun = new_definition
`gamma3f_x_vL_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_vL_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let gamma3f_x_vL0 = new_definition
`gamma3f_x_vL0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_vL0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let gamma3f_x_v_lfun = new_definition
`gamma3f_x_v_lfun (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_v_lfun (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let gamma3f_x_v0 = new_definition
`gamma3f_x_v0 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
gamma3f_v0 (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5)
(sqrt x6)`;;
let vol3_x_135_s2 = new_definition
`vol3_x_135_s2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
vol3r (sqrt x1) (sqrt x3) (sqrt x5) sqrt2`;;
(*
let dih_y_div_sqrtdelta_posbranch = new_definition
`dih_y_div_sqrtdelta_posbranch = y_of_x dih_x_div_sqrtdelta_posbranch`;;
*)
(*
let rhof_x = define `rhof_x x = rho (sqrt x)`;;
*)
(*
let ineq_lemma = prove_by_refinement(
`!a x b. &0 <= a /\ &0 <= b /\ a pow 2 <= x /\ x <= b pow 2 ==> a <= sqrt x /\ sqrt x <= b`,
(* {{{ proof *)
[
REPEAT GEN_TAC;
STRIP_TAC;
SUBGOAL_THEN `&0 <= x` MP_TAC;
ASM_MESON_TAC [REAL_LE_TRANS;Collect_geom.REAL_LE_SQUARE_POW];
ASM_MESON_TAC[Collect_geom.POW2_COND;SQRT_WORKS];
]);;
(* }}} *)
*)
(*
let arclength6_x = new_definition `arclength6_x x1 x2 x3 x4 x5 x6 = arclength (sqrt x1) (sqrt x2) (sqrt x3)`;;
*)
(*
let sqrt_x8 = define `sqrt_x8 (x7:real) (x2:real) (x3:real) (x4:real) (x8:real) (x9:real) = sqrt x8`;;
let sqrt_x9 = define `sqrt_x9 (x7:real) (x2:real) (x3:real) (x4:real) (x8:real) (x9:real) = sqrt x9`;;
*)