(* ========================================================================= *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Chapter: nonlinear inequalities *) (* Author: Thomas Hales *) (* Date: 2012-05-20 *) (* ========================================================================= *) (* May 2012 functional equational definitions of inequality functions. This code is to be used in automated generation of C++ taylorFunctions. scripts.hl generates ocaml Sphere2 module based on these lemmas. June 2012: truncate_* are all deprecated. They can be deleted. autogen: see functional_* lemmas in this file. see functional1_* lemmas in this file for univariate functions. native_c: unit,x1,x2,x3,x4,x5,x6, y1,y2,y3,y4,y5,y6, delta_x,delta_x4, dih_x, sol_x,rad2_x, num1, norm2hh_x, *) (* failwith "moodule";; *) module Functional_equation = struct open Hales_tactic;; open Nonlinear_lemma;; let GMATCH = GMATCH_SIMP_TAC;;let uni = new_definition `uni (f,x) x1 x2 x3 x4 x5 x6 = (f:A->B) ( x x1 x2 x3 x4 x5 x6)`;;let constant6 = new_definition `constant6 c x1 x2 x3 x4 x5 x6 = c`;;let promote3_to_6 = new_definition `promote3_to_6 f x1 x2 x3 x4 x5 x6 = f x1 x2 x3`;;(* }}} *) (* these are circular, because we will define rotatek as a composition of proj_xm *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *)let promote1_to_6 = new_definition `promote1_to_6 f x1 x2 x3 x4 x5 x6 = f x1`;;let rh0 = new_definition `rh0 = &1/(h0 - &1)`;;let two6 = new_definition `two6 = constant6 ( &2)`;;let zero6 = new_definition `zero6 = constant6 ( &0)`;;let dummy6 = new_definition `dummy6 = constant6 ( &0)`;;let four6 = new_definition `four6 = constant6 ( &4)`;;let add6 = new_definition `add6 f g x1 x2 x3 x4 x5 x6 = f x1 x2 x3 x4 x5 x6 + g x1 x2 x3 x4 x5 x6`;;let scalar6 = new_definition `scalar6 f r x1 x2 x3 x4 x5 x6 = (f x1 x2 x3 x4 x5 x6) * (r:real)`;;let mul6 = new_definition `mul6 f g x1 x2 x3 x4 x5 x6 = f x1 x2 x3 x4 x5 x6 * g x1 x2 x3 x4 x5 x6`;;let div6 = new_definition `div6 f g x1 x2 x3 x4 x5 x6 = f x1 x2 x3 x4 x5 x6 / g x1 x2 x3 x4 x5 x6`;;let sub6 = new_definition `sub6 f g x1 x2 x3 x4 x5 x6 = f x1 x2 x3 x4 x5 x6 - g x1 x2 x3 x4 x5 x6`;;(* should be called something different, because we project out 3 coords *)let domain6 = new_definition `domain6 h f g = (!x1 x2 x3 x4 x5 x6. h x1 x2 x3 x4 x5 x6 ==> (f x1 x2 x3 x4 x5 x6 = g x1 x2 x3 x4 x5 x6))`;;let rotate234 = new_definition `rotate234 f = compose6 f proj_x2 proj_x3 proj_x4 unit6 unit6 unit6`;;let rotate126 = new_definition `rotate126 f = compose6 f proj_x1 proj_x2 proj_x6 unit6 unit6 unit6`;;let functional_overload() = ( overload_interface ("+",`add6`); overload_interface ("-",`sub6`); overload_interface ("/",`div6`); overload_interface ("*",`mul6`));; let _ = functional_overload();; let proj_x1 = Nonlinear_lemma.proj_x1;; let proj_x2 = Nonlinear_lemma.proj_x2;; let proj_x3 = Nonlinear_lemma.proj_x3;; let proj_x4 = Nonlinear_lemma.proj_x4;; let proj_x5 = Nonlinear_lemma.proj_x5;; let proj_x6 = Nonlinear_lemma.proj_x6;; let unit6 = Nonlinear_lemma.unit6;; let compose6 = Nonlinear_lemma.compose6;;let rotate345 = new_definition `rotate345 f = compose6 f proj_x3 proj_x4 proj_x5 unit6 unit6 unit6`;;(* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *)let h0cut = new_definition `h0cut y = if (y <= &2 * h0) then &1 else &0`;;(* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *)let functional_eta2_126 =prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. (&0 <= x1 /\ &0 <= x2 /\ &0 <= x6)) eta2_126 (uni(pow2,rotate126 (promote3_to_6 eta_x)))`,(* }}} *)let functional_dih4_x =prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x4 /\ &0 <= x5 /\ &0 <= x6) dih4_x (rotate4 dih_x)`,(* }}} *)let functional_dih5_x =prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x4 /\ &0 <= x5 /\ &0 <= x6) dih5_x (rotate5 dih_x)`,(* }}} *) (* let dih6_x' = new_definition `dih6_x' = rotate6 dih_x`;; let ldih6_x' = new_definition `!x1 x2 x3 x4 x5 x6. ldih6_x' x1 x2 x3 x4 x5 x6 = lfun (sqrt x6 / &2) * dih6_x' x1 x2 x3 x4 x5 x6`;; let gchi6_x' = new_definition `!x1 x2 x3 x4 x5 x6. gchi6_x x1 x2 x3 x4 x5 x6 = gchi (sqrt x6) * dih6_x' x1 x2 x3 x4 x5 x6`;; *) (* }}} *) (* }}} *) (* }}} *) (* }}} *)let functional_dih6_x =prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x4 /\ &0 <= x5 /\ &0 <= x6) dih6_x (rotate6 dih_x)`,(* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *)let functional_ldih6_x =prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x4 /\ &0 <= x5 /\ &0 <= x6) ldih6_x (rotate6 ldih_x)`,(* }}} *)let functional_vol3_x_sqrt =prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <=x6) vol3_x_sqrt (mk_126 vol_x)`,(* }}} *)let functional_vol3f_x_lfun =prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <=x6) vol3f_x_lfun (constant6 ( &2 * mm1 / pi ) * (two6 * mk_126 dih_x + two6 * mk_126 dih2_x + two6 * mk_126 dih6_x + mk_126 dih3_x + mk_126 dih4_x + mk_126 dih5_x - constant6 ( &3 * pi)) - (constant6 (&8 * mm2 / pi)) * (mk_126 ldih_x + mk_126 ldih2_x + mk_126 ldih6_x )) `,(* }}} *)let functional_vol3f_x_sqrt2_lmplus =prove_by_refinement( ` (domain6 (\x1 x2 x3 x4 x5 x6. (&2 * h0) pow 2 <= x1 /\ &0 <= x2 /\ &0 <=x6) vol3f_x_sqrt2_lmplus (constant6 ( &2 * mm1 / pi ) * (two6 * mk_126 dih_x + two6 * mk_126 dih2_x + two6 * mk_126 dih6_x + mk_126 dih3_x + mk_126 dih4_x + mk_126 dih5_x - constant6 ( &3 * pi)) - (constant6 (&8 * mm2 / pi)) * (mk_126 ldih2_x + mk_126 ldih6_x)))`,(* }}} *) (* }}} *) (* }}} *) (* }}} *) (* ldih5_x ldih6_x not in HOL Light*)let cos797 = new_definition `cos797 = cos(#0.797)`;;(* }}} *) (* }}} *) (* }}} *)let functional_arclength_x_123 =prove_by_refinement( `let al_num = proj_x1 + proj_x2 - proj_x3 in let al_den = uni(sqrt,scalar6 (proj_x1 * proj_x2) ( &4)) in let domain = (\x1 x2 x3 x4 x5 x6. (&0 < x1 /\ &0 < x2 /\ &0 <= x3) /\ (sqrt x3 <= sqrt x1 + sqrt x2 /\ sqrt x1 <= sqrt x2 + sqrt x3 /\ sqrt x2 <= sqrt x3 + sqrt x1)) in domain6 domain (arclength_x_123) ( uni(acs, al_num / al_den ) )`,(* }}} *) (* }}} *) (* }}} *) (* }}} *)let functional_sol_euler_x_divsqrtdelta =prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. (&0 <= x1 /\ &0 <= x2 /\ &0 <= x3)) sol_euler_x_div_sqrtdelta ((uni(matan,(delta_x / (scalar6 (eulerA_x * eulerA_x) (&4))))) / eulerA_x)`,(* }}} *) (* dih2_x_div_sqrtdelta_posbranch not defined in HOL-Light *) (* }}} *) let functional_dih4_x_div_sqrtdelta_posbranch = Nonlin_def.dih4_x_div_sqrtdelta_posbranch;; (* }}} *)let functional_dih_x_div_sqrtdelta_posbranch =prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. (&0 <= x1)) dih_x_div_sqrtdelta_posbranch ((scalar6 proj_y1 (&2)) / (delta_x4) * uni(matan, (scalar6 (proj_x1 * delta_x) (&4)) / (uni(pow2,delta_x4))))`,(* }}} *)let functional_edge_flat2_x =prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x5 /\ &0 <= x6) edge_flat2_x (uni(pow2,(uni(sqrt, compose6(promote3_to_6 quadratic_root_plus_curry) proj_x1 (proj_x1 * proj_x1 + (proj_x3 - proj_x5) * (proj_x2 - proj_x6) - proj_x1 * (proj_x2 + proj_x3 + proj_x5 + proj_x6)) ( proj_x1 * proj_x3 * proj_x5 + proj_x1 * proj_x2 * proj_x6 - proj_x3 * (proj_x1 + proj_x2 - proj_x3 + proj_x5 - proj_x6) * proj_x6 - proj_x2 * proj_x5 * (proj_x1 - proj_x2 + proj_x3 - proj_x5 + proj_x6)) zero6 zero6 zero6)))) `,(* }}} *) let functional_ldih2_x_div_sqrtdelta_posbranch = Nonlin_def.ldih2_x_div_sqrtdelta_posbranch;; let functional_ldih3_x_div_sqrtdelta_posbranch = Nonlin_def.ldih3_x_div_sqrtdelta_posbranch;; let functional_ldih5_x_div_sqrtdelta_posbranch = Nonlin_def.ldih5_x_div_sqrtdelta_posbranch;; let functional_ldih6_x_div_sqrtdelta_posbranch = Nonlin_def.ldih6_x_div_sqrtdelta_posbranch;;let functional_ldih_x_div_sqrtdelta_posbranch =prove_by_refinement( `ldih_x_div_sqrtdelta_posbranch = (scalar6 (constant6 h0 - scalar6 proj_y1 ( #0.5)) rh0) * dih_x_div_sqrtdelta_posbranch`,(* }}} *) (* }}} *)let functional1_rho =prove_by_refinement( `!y. rho y = y * (const1 * rh0 * (#0.5)) + (&1 - const1 * rh0)`,(* }}} *)let functional1_lfun =prove_by_refinement( `!y. lfun y = ( h0 - y)*rh0`,(* }}} *) (* }}} *) (* }}} *) (* }}} *) (* extra parameter cases *)let functional_rhazim_x =prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x4 /\ &0 <= x5 /\ &0 <= x6) rhazim_x (uni (rho,proj_y1) * dih_x)`,(* }}} *)let functional_arclength_x1 =prove_by_refinement( `!a b. domain6 (\x1 x2 x3 x4 x5 x6. &0 <= a /\ &0 <= b) (arclength_x1 a b) (compose6 arclength_x_123 proj_x1 (constant6 (a*a)) (constant6 (b*b)) dummy6 dummy6 dummy6)`,(* }}} *)let functional_arclength_x2 =prove_by_refinement( `!a b. domain6 (\x1 x2 x3 x4 x5 x6. &0 <= a /\ &0 <= b) (arclength_x2 a b) (compose6 arclength_x_123 proj_x2 (constant6 (a*a)) (constant6 (b*b)) dummy6 dummy6 dummy6)`,(* }}} *)let functional_delta_126_x =prove_by_refinement( `!a b c. delta_126_x a b c = compose6 delta_x proj_x1 proj_x2 (constant6 a) (constant6 b) (constant6 c) proj_x6`,(* }}} *)let functional_delta_234_x =prove_by_refinement( `!a b c. delta_234_x a b c = compose6 delta_x (constant6 a) proj_x2 proj_x3 proj_x4 (constant6 b) (constant6 c)`,(* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *) (* two repeated defs =gamma2= deprecated. *) let gamma2_x_div_azim = (* same as truncate_gamma2_x *) new_definition `gamma2_x_div_azim m x = (&8 - x)* sqrt x / (&24) - ( (&2 * mm1/ pi) * (&1 - sqrt x / sqrt8) - (&8 * mm2 / pi) * m * lfun (sqrt x / &2))`;;let functional_delta_135_x =prove_by_refinement( `!a b c. delta_135_x a b c = compose6 delta_x proj_x1 (constant6 a) proj_x3 (constant6 b) proj_x5 (constant6 c)`,let gamma2_x1_div_a = new_definition `gamma2_x1_div_a m = promote1_to_6 (gamma2_x_div_azim m)`;;(* }}} *)let nonf_gamma2_x1_div_a =prove_by_refinement( `!(m:real) (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real). gamma2_x1_div_a m x1 x2 x3 x4 x5 x6 = gamma2_x_div_azim m x1`,(* }}} *)let nonf_gamma2_x1_div_a_v2 =prove_by_refinement( `!(m:real) (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real). gamma2_x1_div_a_v2 m x1 x2 x3 x4 x5 x6 = gamma2_x_div_azim_v2 m x1`,let gamma3f_x_div_sqrtdelta = new_definition `gamma3f_x_div_sqrtdelta m4 m5 m6 = constant6 (&1/ &12) - (scalar6 ( mk_456 (rotate5 (sol_euler_x_div_sqrtdelta)) + mk_456 (rotate6 (sol_euler_x_div_sqrtdelta)) + mk_456 (rotate4 (sol_euler_x_div_sqrtdelta)) ) (&2 * mm1/ pi) - scalar6 ( (scalar6 (uni(lfun,(scalar6 proj_y4 #0.5))) m4) * mk_456 (rotate4 (dih_x_div_sqrtdelta_posbranch)) + (scalar6 (uni(lfun,(scalar6 proj_y5 #0.5))) m5) * mk_456 (rotate5 (dih_x_div_sqrtdelta_posbranch)) + (scalar6 (uni(lfun,(scalar6 proj_y6 #0.5))) m6) * mk_456 (rotate6 (dih_x_div_sqrtdelta_posbranch)) ) (&8 * mm2 / pi))`;;(* }}} *)let shift_scalar6 =prove_by_refinement( `!f g m. (scalar6 f m) * g = f * (scalar6 g m)`,(* }}} *)let gamma3f_x_div_sqrtdelta_alt =prove_by_refinement( `!m4 m5 m6. gamma3f_x_div_sqrtdelta m4 m5 m6 = constant6 (&1/ &12) - (scalar6 ( mk_456 (rotate5 (sol_euler_x_div_sqrtdelta)) + mk_456 (rotate6 (sol_euler_x_div_sqrtdelta)) + mk_456 (rotate4 (sol_euler_x_div_sqrtdelta)) ) (&2 * mm1/ pi) - scalar6 ( ( (uni(lfun,(scalar6 proj_y4 #0.5))) ) * (scalar6 (mk_456 (rotate4 (dih_x_div_sqrtdelta_posbranch))) m4) + ( (uni(lfun,(scalar6 proj_y5 #0.5))) ) * (scalar6 ( mk_456 (rotate5 (dih_x_div_sqrtdelta_posbranch))) m5) + ( (uni(lfun,(scalar6 proj_y6 #0.5)))) * (scalar6 (mk_456 (rotate6 (dih_x_div_sqrtdelta_posbranch))) m6) ) (&8 * mm2 / pi)) `,let vol3f_456 = new_definition `vol3f_456 m4 = scalar6 ( mk_456 (rotate5 sol_x) + mk_456 (rotate6 sol_x) + mk_456 (rotate4 sol_x) ) (&2 * mm1/ pi) - scalar6 ( (scalar6 (uni(lfun,(scalar6 proj_y4 #0.5))) m4) * mk_456 (rotate4 dih_x) + (uni(lfun,(scalar6 proj_y5 #0.5))) * mk_456 (rotate5 dih_x) + (uni(lfun,(scalar6 proj_y6 #0.5))) * mk_456 (rotate6 dih_x) ) (&8 * mm2 / pi)`;;let gamma23_full8_x = new_definition `gamma23_full8_x m1 = (compose6 (gamma3_x m1) dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6) + (compose6 (gamma3_x m1) dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5) + scalar6 (dih_x -(mk_126 dih_x + mk_135 dih_x)) (#0.008)`;;let gamma23_keep135_x = new_definition `gamma23_keep135_x m1 = (compose6 (gamma3_x m1) dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5) + scalar6 (dih_x - mk_135 dih_x) (#0.008)`;;(* }}} *)let nonf_gamma3_x =prove_by_refinement( `!m1 x1 x2 x3 x4 x5 x6. gamma3_x m1 x1 x2 x3 x4 x5 x6 = vol_x (&2) (&2) (&2) x4 x5 x6 - ((sol_x x5 (&2) x4 (&2) x6 (&2) + sol_x x6 (&2) x5 (&2) x4 (&2) + sol_x x4 (&2) x6 (&2) x5 (&2)) * &2 * mm1 / pi - ((lfun (sqrt x4 * #0.5) * m1) * dih_x x4 (&2) x6 (&2) x5 (&2) + lfun (sqrt x5 * #0.5) * dih_x x5 (&2) x4 (&2) x6 (&2) + lfun (sqrt x6 * #0.5) * dih_x x6 (&2) x5 (&2) x4 (&2)) * &8 * mm2 / pi)`,(* }}} *)let nonf_gamma23_full8_x =prove_by_refinement( `!m1 x1 x2 x3 x4 x5 x6. gamma23_full8_x m1 x1 x2 x3 x4 x5 x6 = gamma3_x m1 (&0) (&0) (&0) x1 x2 x6 + gamma3_x m1 (&0) (&0) (&0) x1 x3 x5 + (dih_x x1 x2 x3 x4 x5 x6 - (dih_x x1 x2 (&2) (&2) (&2) x6 + dih_x x1 (&2) x3 (&2) x5 (&2))) * #0.008`,(* }}} *)let nonf_gamma23_keep135_x =prove_by_refinement( `!m1 x1 x2 x3 x4 x5 x6. gamma23_keep135_x m1 x1 x2 x3 x4 x5 x6 = gamma3_x m1 (&0) (&0) (&0) x1 x3 x5 + (dih_x x1 x2 x3 x4 x5 x6 - dih_x x1 (&2) x3 (&2) x5 (&2)) * #0.008 `,(* }}} *) (* extra parameter cases scratch *) (* added 2013-May *) let F_REWRITE_TAC = REWRITE_TAC[ Nonlin_def.mud_126_x;Nonlin_def.mu6_x;Nonlin_def.mu_y;Nonlin_def.taud;Nonlin_def.taud_x; Nonlin_def.ups_126;Nonlin_def.edge2_126_x;Nonlin_def.edge2_flatD_x1; Nonlin_def.edge2_135_x;Nonlin_def.edge2_234_x; Nonlin_def.mud_135_x;Nonlin_def.mud_126_x;Nonlin_def.mud_234_x; Nonlin_def.mudLs_234_x;Nonlin_def.mudLs_126_x;Nonlin_def.mudLs_135_x; LET_DEF;LET_END_DEF; Sphere.delta_y; Sphere.y_of_x;Sphere.flat_term_x;Sphere.flat_term; compose6;promote3_to_6; promote1_to_6; domain6; constant6; uni; add6;mul6; sub6;div6; proj_y1;proj_y2; proj_y3;proj_y4; proj_y5;proj_y6; dummy6; zero6; proj_x1;proj_x2; proj_x4;proj_x3; proj_x5; proj_x6; ];;let nonf_gamma3f_x_div_sqrtdelta =prove_by_refinement( `!m4 m5 m6 x1 x2 x3 x4 x5 x6. gamma3f_x_div_sqrtdelta m4 m5 m6 x1 x2 x3 x4 x5 x6 = &1 / &12 - ((sol_euler_x_div_sqrtdelta x5 (&2) x4 (&2) x6 (&2) + sol_euler_x_div_sqrtdelta x6 (&2) x5 (&2) x4 (&2) + sol_euler_x_div_sqrtdelta x4 (&2) x6 (&2) x5 (&2)) * &2 * mm1 / pi - ((lfun (sqrt x4 * #0.5) * m4) * dih_x_div_sqrtdelta_posbranch x4 (&2) x6 (&2) x5 (&2) + (lfun (sqrt x5 * #0.5) * m5) * dih_x_div_sqrtdelta_posbranch x5 (&2) x4 (&2) x6 (&2) + (lfun (sqrt x6 * #0.5) * m6) * dih_x_div_sqrtdelta_posbranch x6 (&2) x5 (&2) x4 (&2)) * &8 * mm2 / pi)`,(* }}} *)let taud_x_taud =prove_by_refinement( `!y1 y2 y3 y4 y5 y6. &0 <= y1 /\ &0 <= y2 /\ &0 <= y3 ==> y_of_x taud_x y1 y2 y3 y4 y5 y6 = taud y1 y2 y3 y4 y5 y6`,(* }}} *)let mu6_x_mu_y =prove_by_refinement( `!y1 y2 y3 x4 x5 x6. &0 <= y1 /\ &0 <= y2 /\ &0 <= y3 ==> mu_y y1 y2 y3 = mu6_x (y1 * y1) ( y2 * y2) (y3 * y3) x4 x5 x6 `,(* }}} *)let taud_x_ALT =prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. (&0 <= x1 /\ &0 <= x2 /\ &0 <= x3)) taud_x ( (promote1_to_6 flat_term_x) + (uni(sqrt,delta_x)) * mu6_x)`,(* }}} *)let functional_edge2_126_x =prove_by_refinement( `!d x4 x5. (edge2_126_x d x4 x5) = (let a = proj_x6 in let c4 = constant6 x4 in let c5 = constant6 x5 in let b = constant6(-- &1) * compose6 delta_x1 zero6 proj_x2 proj_x1 proj_x6 (c5) (c4) in let c = constant6 ( d) - compose6 delta_x proj_x1 proj_x2 zero6 (c4) (c5) proj_x6 in let ups_456 = compose6 ups_126 (c4) (c5) dummy6 dummy6 dummy6 proj_x6 in let discr = ups_456 * ups_126 + constant6( -- &4*d) * a in (uni(sqrt,discr) - b) / (constant6 (&2) * a))`,(* }}} *)let functional_edge2_135_x =prove_by_refinement( `!d x4 x6. (edge2_135_x d x4 x6) = compose6 (edge2_126_x d x4 x6) (proj_x1) (proj_x3) (dummy6) (dummy6) (dummy6) (proj_x5)`,(* }}} *)let functional_edge2_234_x =prove_by_refinement( `!d x5 x6. edge2_234_x d x5 x6 = compose6 (edge2_126_x d x5 x6) (proj_x2) (proj_x3) (dummy6) (dummy6) (dummy6) (proj_x4)`,(* }}} *)let nonfunctional_edge2_126_x =prove_by_refinement( `!d x1 x2 a b c x4 x5 x6. (edge2_126_x d x4 x5) x1 x2 a b c x6 = ((sqrt (ups_x x4 x5 x6 * ups_x x1 x2 x6 + (-- &4 * d) * x6) - -- &1 * delta_x1 (&0) x2 x1 x6 x5 x4) / (&2 * x6))`,(* }}} *)let nonfunctional_edge2_135_x =prove_by_refinement( `!d x1 x3 x5 x4 x6 a b c. (edge2_135_x d x4 x6) x1 a x3 b x5 c = (sqrt (ups_x x4 x6 x5 * ups_x x1 x3 x5 + (-- &4 * d) * x5) - -- &1 * delta_x1 (&0) x3 x1 x5 x6 x4) / (&2 * x5)`,(* }}} *)let nonfunctional_edge2_234_x =prove_by_refinement( `!d x2 x3 x4 x5 x6 a b c. (edge2_234_x d x5 x6) a x2 x3 x4 b c = (sqrt (ups_x x5 x6 x4 * ups_x x2 x3 x4 + (-- &4 * d) * x4) - -- &1 * delta_x1 (&0) x3 x2 x4 x6 x5) / (&2 * x4)`,(* }}} *)let functional_mud_135_x =prove_by_refinement( `!y2 y4 y6. (domain6 (\ x1 x2 x3 x4 x5 x6. &0 <= y2)) (mud_135_x_v1 y2 y4 y6) (mul6 (compose6 (mu6_x) (constant6 (y2*y2)) proj_x1 proj_x3 dummy6 dummy6 dummy6) (uni(sqrt,(delta_135_x (y2*y2) (y4*y4) (y6*y6)))))`,(* }}} *)let functional_mud_126_x =prove_by_refinement( `!y3 y4 y5. (domain6 (\ x1 x2 x3 x4 x5 x6. &0 <= y3)) (mud_126_x_v1 y3 y4 y5) (mul6 (compose6 (mu6_x) (constant6 (y3*y3)) proj_x1 proj_x2 dummy6 dummy6 dummy6) (uni(sqrt,(delta_126_x (y3*y3) (y4*y4) (y5*y5)))))`,(* }}} *)let functional_mud_234_x =prove_by_refinement( `!y1 y5 y6. (domain6 (\ x1 x2 x3 x4 x5 x6. &0 <= y1)) (mud_234_x_v1 y1 y5 y6) (mul6 (compose6 (mu6_x) (constant6 (y1*y1)) proj_x2 proj_x3 dummy6 dummy6 dummy6) (uni(sqrt,(delta_234_x (y1*y1) (y5*y5) (y6*y6)))))`,(* }}} *)let nonfunctional_taud_D2 =prove_by_refinement( `!x1 x2 x3 x4 x5 x6. taud_D2_num_x x1 x2 x3 x4 x5 x6 = -- #0.07 * delta_x x1 x2 x3 x4 x5 x6 * delta_x1 x1 x2 x3 x4 x5 x6 * &2 * sqrt x1 - &1 / &4 * mu6_x x1 x2 x3 x4 x5 x6 * (delta_x1 x1 x2 x3 x4 x5 x6 * &2 * sqrt x1) pow 2 + &1 / &2 * mu6_x x1 x2 x3 x4 x5 x6 * delta_x x1 x2 x3 x4 x5 x6 * (-- &8 * x1 * x4 + delta_x1 x1 x2 x3 x4 x5 x6 * &2)`,(* }}} *)let nonfunctional_taud_D1 =prove_by_refinement( `!x1 x2 x3 x4 x5 x6. taud_D1_num_x x1 x2 x3 x4 x5 x6 = -- #0.07 * delta_x x1 x2 x3 x4 x5 x6 + &1 / &2 * mu6_x x1 x2 x3 x4 x5 x6 * delta_x1 x1 x2 x3 x4 x5 x6 * &2 * sqrt x1 + sol0 / #0.52 * sqrt (delta_x x1 x2 x3 x4 x5 x6)`,(* }}} *) (* }}} *) (* }}} *) (* }}} *) (* }}} *)let nonfunctional_mu6_x =prove_by_refinement( `!x1 x2 x3 x4 x5 x6. mu6_x x1 x2 x3 x4 x5 x6 = (#0.012 + #0.07 * (#2.52 - sqrt(x1)) + #0.01 * (#2.52 * &2 - sqrt(x2) - sqrt(x3) ))`,(* }}} *) end;;let nonf_gamma3f_x_div_sqrt_delta =prove_by_refinement( `!p1 p2 p3 x1 x2 x3 x4 x5 x6. gamma3f_x_div_sqrtdelta p1 p2 p3 x1 x2 x3 x4 x5 x6 = &1 / &12 - ((sol_euler_x_div_sqrtdelta x5 (&2) x4 (&2) x6 (&2) + sol_euler_x_div_sqrtdelta x6 (&2) x5 (&2) x4 (&2) + sol_euler_x_div_sqrtdelta x4 (&2) x6 (&2) x5 (&2)) * &2 * mm1 / pi - ((lfun (sqrt x4 * #0.5) * p1) * dih_x_div_sqrtdelta_posbranch x4 (&2) x6 (&2) x5 (&2) + (lfun (sqrt x5 * #0.5) * p2) * dih_x_div_sqrtdelta_posbranch x5 (&2) x4 (&2) x6 (&2) + (lfun (sqrt x6 * #0.5) * p3) * dih_x_div_sqrtdelta_posbranch x6 (&2) x5 (&2) x4 (&2)) * &8 * mm2 / pi)`,