2 May 2012, definitions no longer needed in
3 primary verifications of flyspeck.
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.
41 * deprecated: volume_props.
45 (* deleted obsolete definitions 2/7/2010 svn 1471:
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,
59 (* terms moved to Harrison's flyspeck.ml
61 solid_triangle, ellipsoid, conic_cap, frustum, frustt,
62 primitive, MEASURABLE_RULES, solid, coplanar, cross, wedge, azim,
66 (* (now voronoi_open) let voronoi = new_definition `voronoi v S = { x | !w. ((S w) /\ ~(w=v)) ==> (dist( x, v) < dist( x, w)) }`;; *)
69 (* DEPRECATED, 2011-08-01, not used
71 let directed_angle = new_definition `directed_angle (x,y) (x',y') =
72 Arg (complex(x',y') / complex(x,y))`;;
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)))`;;
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))`;;
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)))`;;
90 let sol_euler_y = `sol_euler_y = y_of_x sol_euler_x`;;
95 let acs_sqrt_x1 = new_definition `acs_sqrt_x1 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
98 let acs_sqrt_x2 = new_definition `acs_sqrt_x2 (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real) =
105 let solRy = new_definition `solRy y1 y2 y6 c = solR (y1/ &2) (eta_y y1 y2 y6) c`;;
107 let dihRy = new_definition `dihRy y1 y2 y6 c = dihR (y1/ &2) (eta_y y1 y2 y6) c`;;
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)`;;
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)`;;
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) +
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)`;;
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)`;;
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)`;;
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)`;;
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)`;;
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`;;
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)`;;
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)`;;
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)`;;
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)`;;
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`;;
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`;;
185 let delta_template_B_x = new_definition
186 `delta_template_B_x x15 x45 x34 x12 x1 x2 x3 x4 x5 (x6:real) =
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))`;;
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) =
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))`;;
200 let taum_template_B_x = new_definition
201 `taum_template_B_x x15 x45 x34 x12 x1 x2 x3 x4 x5 (x6:real) =
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))`;;
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)`;;
216 (* tau_lowform_x intended for use when dih1 > pi/2, dih2, dih3 < pi/2,
218 Then tau_lowform_x is a lower bound on tau (that is graceful when delta->0).
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))`;;
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)`;;
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))`;;
241 (* deleted 2013-08-18 *)
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
266 ("mardih_x","marchalDih"); ("mardih2_x","marchalDih2");
267 ("mardih3_x","marchalDih3");
268 ("mardih4_x","marchalDih4"); ("mardih5_x","marchalDih5");
269 ("mardih6_x","marchalDih6");
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
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];
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]};
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*)
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
299 (num1e /. abcsq) - num1sqI (*0*)
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
309 taumarE2D2calc = D[Dihedral[2, 2, 2, b, c, a], {a, 2}] // Together //
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*
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
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*
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
331 taumarD2num = (e1 taumarE1D2 + e2 taumarE2D2 + e3
332 taumarE3D2) (aafac^2 ssd^3) // Simplify
333 taumarD2numDef = (taumarD2num /. abcsq) // HolForm; (* num2 in sphere.hl *)
335 (((D[taumarE, {a, 2}]) aafac^2 ssd^3 - taumarD2num) //. abcsub) // Chop
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}
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))))))))))))))))`;;
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))`;;
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))`;;
369 (* num1^2 - #0.01 * num2 *)
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)))))))))))))))))`;;
390 (* x_A is a special case of x_C: *)
393 let truncate_gamma23_x_A = new_definition `truncate_gamma23_x_A iw1 m1 m2 m6 =
395 (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
396 dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
398 + (dih_x - (mk_126 (truncate_dih_x (#0.14)) + constant6 (#0.08))) *
399 uni((truncate_gamma2_x m1), proj_x1)`;;
402 let truncate_gamma23_x_C = new_definition `truncate_gamma23_x_C d iw1 m1 m2 m6 =
404 (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
405 dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
407 + (dih_x - (mk_126 (truncate_dih_x (#0.14)) + constant6 (d))) *
408 uni((truncate_gamma2_x m1), proj_x1)`;;
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)`;;
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))`;;
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`;;
426 let truncate_gamma23_x = new_definition `truncate_gamma23_x iw1 iw2 m1 m2 m3 m5 m6 =
428 (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
429 dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
432 (compose6 (truncate_gamma3f_x (#0.14) m1 m3 m5)
433 dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5)
436 (mk_126 (truncate_dih_x (#0.14)) +
437 mk_135 (truncate_dih_x (#0.14)))) *
438 uni((truncate_gamma2_x m1),proj_x1)`;;
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 +
446 (dih_x x1 x2 (&2) (&2) (&2) x6 +
447 dih_x x1 (&2) x3 (&2) x5 (&2))) *
448 truncate_gamma2_x m1 x1`;;
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))`;;
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`;;
459 let truncate_gamma23_x = new_definition `truncate_gamma23_x iw1 iw2 m1 m2 m3 m5 m6 =
461 (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
462 dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
465 (compose6 (truncate_gamma3f_x (#0.14) m1 m3 m5)
466 dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5)
469 (mk_126 (truncate_dih_x (#0.14)) +
470 mk_135 (truncate_dih_x (#0.14)))) *
471 uni((truncate_gamma2_x m1),proj_x1)`;;
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 +
479 (dih_x x1 x2 (&2) (&2) (&2) x6 +
480 dih_x x1 (&2) x3 (&2) x5 (&2))) *
481 truncate_gamma2_x m1 x1`;;
483 let truncate_sqrt = new_definition `
484 truncate_sqrt c x = if (x <= c) then sqrt(c) else sqrt(x)`;;
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)`);;
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)`;;
500 let truncate_vol_x =new_definition
501 `truncate_vol_x c = scalar6 (uni((truncate_sqrt c),delta_x)) (&1 / &12)`;;
503 let truncate_vol3r_456 = new_definition `truncate_vol3r_456 c =
504 mk_456 (truncate_vol_x c)`;;
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))
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))
523 let truncate_sqrt = new_definition `
524 truncate_sqrt c x = if (x <= c) then sqrt(c) else sqrt(x)`;;
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)`);;
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)`;;
536 let truncate_vol_x =new_definition
537 `truncate_vol_x c = scalar6 (uni((truncate_sqrt c),delta_x)) (&1 / &12)`;;
539 let truncate_vol3r_456 = new_definition `truncate_vol3r_456 c =
540 mk_456 (truncate_vol_x c)`;;
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))
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))
560 (* in delta_pent_x: nonstandard ordering of variables, x6 swapped with x3 *)
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)`;;
572 Upper approximation to Sqrt on [0,1]:
574 sqp = 3/8 + (3*x)/4 - x^2/8 + (1 - x)^3 (0.7 x - 0.25);
576 Sqp[x_]:= If[x<1,3/8 + (3*x)/4 - x^2/8 + (1 - x)^3 (0.7 x - 0.25),Sqrt[x]];
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);
581 Matan[x_] := ArcTan[Sqrt[x]]/Sqrt[x];
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]];
588 UpperDihY[y1_, y2_, y3_, y4_, y5_, y6_] :=
589 UpperDihX @@ ({y1, y2, y3, y4, y5, y6}^2);
591 Lower approx to sqrt on [0,1]:
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;
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.
602 let sqp = new_definition `sqp x =
604 &3 / &8 + (&1 - x) pow 3 * (-- #0.25 + #0.7 * x) +
605 &3 * x / &4 - x * x/ &8 else sqrt x`;;
607 let sqn = new_definition `sqn x =
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)
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. *)
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))`;;
623 let upper_dih_y = new_definition `upper_dih_y = y_of_x upper_dih_x`;;
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 -
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) -
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)
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 -
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) -
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)
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)`;;
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)`;;
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)`;;
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)`;;
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)`;;
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)`;;
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)`;;
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)`;;
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}))`;;
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
711 (* deprecated 2013-2-13.
712 let radius = new_definition `radius (x,y) = sqrt((x pow 2) + (y pow 2))`;;
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))))`;;
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 *)
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)`;;
730 (* deprecated, Dec 1, 2012 , replaced with beta_bumpA_y *)
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))`;;
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) -
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 -
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) )`;;
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 -
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) )`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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)`;;
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)`;;
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)`;;
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`;;
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)`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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)`;;
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)`;;
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)`;;
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)`;;
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`;;
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)`;;
839 let rr22 = REWRITE_RULE[GSYM sqrt2_sqrt2];;
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`);;
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`);;
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`);;
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`);;
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)`);;
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)`);;
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)`);;
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`;;
876 (* remaining splits *)
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`;;
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`;;
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)`;;
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)`;;
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)`;;
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)) `;;
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)`;;
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))) /
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) *
919 ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
920 (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
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))) /
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) *
933 ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
934 (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
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))) /
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) *
946 ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
947 (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
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)`;;
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)`;;
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)`;;
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)`;;
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)`;;
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)`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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 `;;
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 `;;
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)`;;
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`;;
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)
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)
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)
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)
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)
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)
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`;;
1047 let x1cube = new_definition `x1cube = proj_x1 * proj_x1 * proj_x1`;;
1049 let x1cube = new_definition `x1cube = proj_x1 * proj_x1 * proj_x1`;;
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)) `;;
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)`;;
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))) /
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) *
1072 ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
1073 (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
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))) /
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) *
1086 ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
1087 (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
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))) /
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) *
1099 ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
1100 (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
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)`;;
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)`;;
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)`;;
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)`;;
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)`;;
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)`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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 `;;
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 `;;
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)`;;
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`;;
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)
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)
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)
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)
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)
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)
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`;;
1202 let arclength6_x = new_definition `arclength6_x x1 x2 x3 x4 x5 x6 = arclength (sqrt x1) (sqrt x2) (sqrt x3)`;;
1205 let x1cube = new_definition `x1cube = proj_x1 * proj_x1 * proj_x1`;;
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 -
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) )`;;
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 -
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) )`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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)`;;
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)`;;
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)`;;
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`;;
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)`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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)`;;
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)`;;
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)`;;
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)`;;
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`;;
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)`;;
1295 let rr22 = REWRITE_RULE[GSYM sqrt2_sqrt2];;
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`);;
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`);;
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`);;
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`);;
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)`);;
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)`);;
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)`);;
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`;;
1332 (* remaining splits *)
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`;;
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`;;
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)`;;
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)`;;
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)`;;
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)) `;;
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)) `;;
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)`;;
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))) /
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) *
1378 ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
1379 (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
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))) /
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) *
1392 ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
1393 (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
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))) /
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) *
1405 ((&2 * mm1 / pi) * &2 * pi * (&1 - y1 / (sqrt2 * &2)) -
1406 (&8 * mm2 / pi) * &2 * pi * lfun (y1 / &2))) /
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)`;;
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)`;;
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)`;;
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)`;;
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)`;;
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)`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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 `;;
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 `;;
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)`;;
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`;;
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)
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)
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)
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)
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)
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)
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`;;
1507 let dih_y_div_sqrtdelta_posbranch = new_definition
1508 `dih_y_div_sqrtdelta_posbranch = y_of_x dih_x_div_sqrtdelta_posbranch`;;
1513 let rhof_x = define `rhof_x x = rho (sqrt x)`;;
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`,
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];
1532 let arclength6_x = new_definition `arclength6_x x1 x2 x3 x4 x5 x6 = arclength (sqrt x1) (sqrt x2) (sqrt x3)`;;
1537 let sqrt_x8 = define `sqrt_x8 (x7:real) (x2:real) (x3:real) (x4:real) (x8:real) (x9:real) = sqrt x8`;;
1539 let sqrt_x9 = define `sqrt_x9 (x7:real) (x2:real) (x3:real) (x4:real) (x8:real) (x9:real) = sqrt x9`;;