(*
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 nonf_truncate_gamma23_x_A = prove_by_refinement(
`!iw1 m1 m2 m6 x1 x2 x3 x4 x5 x6.
truncate_gamma23_x_A iw1 m1 m2 m6 x1 x2 x3 x4 x5 x6 =
truncate_gamma3f_x #0.14 m1 m2 m6 (&0) (&0) (&0) x1 x2 x6 * iw1 +
(dih_x x1 x2 x3 x4 x5 x6 -
(truncate_dih_x #0.14 x1 x2 (&2) (&2) (&2) x6 + #0.08)) *
truncate_gamma2_x m1 x1`,
(* {{{ proof *)
[
REWRITE_TAC[truncate_gamma23_x_A;add6;scalar6;compose6;sub6;mul6;mk_126;mk_135;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;dummy6;constant6;two6;uni]
]);;
(* }}} *)
*)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(*
let promote_pow3r = INST_TYPE [(`:real`,`:A`);(`:real`,`:B`);(`:real`,`:C`);(`:real`,`:D`);(`:real`,`:E`)] promote_pow3;;
*)
(*
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 ineq_square = prove_by_refinement(
`((!y1 y2 y3 y4 y5 y6.
ineq
[(a1,y1,b1);(a2,y2,b2);(a3,y3,b3);(a4,y4,b4);(a5,y5,b5);(a6,y6,b6)]
(P y1 y2 y3 y4 y5 y6)) ==>
((&0 <= a1 /\ &0 <= a2 /\ &0 <= a3 /\ &0 <= a4 /\ &0 <= a5 /\ &0 <= a6 /\
&0 <= b1 /\ &0 <= b2 /\ &0 <= b3 /\ &0 <= b4 /\ &0 <= b5 /\ &0 <= b6 )) ==>
(!x1 x2 x3 x4 x5 x6.
ineq [(a1 pow 2,x1,b1 pow 2);(a2 pow 2,x2,b2 pow 2);(a3 pow 2,x3,b3 pow 2);
(a4 pow 2,x4,b4 pow 2);(a5 pow 2,x5,b5 pow 2);(a6 pow 2,x6,b6 pow 2)]
(P (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6))))`,
(* {{{ proof *)
[
REWRITE_TAC[ineq];
REPEAT STRIP_TAC;
FIRST_X_ASSUM (fun t-> MP_TAC (SPECL [`sqrt x1`;`sqrt x2`;`sqrt x3`;`sqrt x4`;`sqrt x5`;`sqrt x6`] t));
ASM_MESON_TAC[ineq_lemma];
]);;
(* }}} *)
*)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
let rr f s = REWRITE_RULE[Sphere.y_of_x] (f s);;
let lmdih_n0 = rr prove_by_refinement(
`!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y1 ) ==>(y_of_x lmdih_x_n y1 y2 y3 y4 y5 y6 = &0 )`,
(* {{{ proof *)
[
REWRITE_TAC[Sphere.y_of_x;lmdih_x_n];
REPEAT STRIP_TAC;
ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih0];
REAL_ARITH_TAC;
]);;
(* }}} *)
let lmdih2_n0 = rr prove_by_refinement(
`!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y2 ) ==>(y_of_x lmdih2_x_n y1 y2 y3 y4 y5 y6 = &0 )`,
(* {{{ proof *)
[
REWRITE_TAC[Sphere.y_of_x;lmdih_x_n;lmdih2_x_n;Sphere.lmdih2_x_div_sqrtdelta_posbranch;Sphere.rotate2];
REPEAT STRIP_TAC;
ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih0];
REAL_ARITH_TAC;
]);;
let lmdih3_n0 = rr prove_by_refinement(
`!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y3 ) ==>(y_of_x lmdih3_x_n y1 y2 y3 y4 y5 y6 = &0 )`,
(* {{{ proof *)
[
REWRITE_TAC[Sphere.y_of_x;lmdih_x_n;lmdih3_x_n;Sphere.lmdih3_x_div_sqrtdelta_posbranch;Sphere.rotate3];
REPEAT STRIP_TAC;
ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih0];
REAL_ARITH_TAC;
]);;
let lmdih5_n0 = rr prove_by_refinement(
`!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y5 ) ==>(y_of_x lmdih5_x_n y1 y2 y3 y4 y5 y6 = &0 )`,
(* {{{ proof *)
[
REWRITE_TAC[Sphere.y_of_x;lmdih_x_n;lmdih5_x_n;Sphere.lmdih5_x_div_sqrtdelta_posbranch;Sphere.rotate5];
REPEAT STRIP_TAC;
ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih0];
REAL_ARITH_TAC;
]);;
let lmdih6_n0 = rr prove_by_refinement(
`!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y6 ) ==>(y_of_x lmdih6_x_n y1 y2 y3 y4 y5 y6 = &0 )`,
(* {{{ proof *)
[
REWRITE_TAC[Sphere.y_of_x;lmdih_x_n;lmdih6_x_n;Sphere.lmdih6_x_div_sqrtdelta_posbranch;Sphere.rotate6];
REPEAT STRIP_TAC;
ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih0];
REAL_ARITH_TAC;
]);;
let lmdih_ldih_n = rr prove_by_refinement(
`!y1 y2 y3 y4 y5 y6. (&0 <= y1 /\ y1 <= &2 * h0) ==>(y_of_x lmdih_x_n y1 y2 y3 y4 y5 y6 = y_of_x ldih_x_n y1 y2 y3 y4 y5 y6)`,
(* {{{ proof *)
[
REWRITE_TAC[Sphere.y_of_x;lmdih_x_n;ldih_x_n];
REPEAT STRIP_TAC;
ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih_ldih];
]);;
(* }}} *)
let lmdih2_ldih2_n = rr prove_by_refinement(
`!y1 y2 y3 y4 y5 y6. (&0 <= y2 /\ y2 <= &2 * h0) ==>(y_of_x lmdih2_x_n y1 y2 y3 y4 y5 y6 = y_of_x ldih2_x_n y1 y2 y3 y4 y5 y6)`,
(* {{{ proof *)
[
REWRITE_TAC[Sphere.y_of_x;Sphere.lmdih2_x_div_sqrtdelta_posbranch;Sphere.rotate2;Sphere.ldih2_x_div_sqrtdelta_posbranch;lmdih2_x_n;ldih2_x_n];
REPEAT STRIP_TAC;
ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih_ldih];
]);;
(* }}} *)
let lmdih3_ldih3_n = rr prove_by_refinement(
`!y1 y2 y3 y4 y5 y6. (&0 <= y3 /\ y3 <= &2 * h0) ==>(y_of_x lmdih3_x_n y1 y2 y3 y4 y5 y6 = y_of_x ldih3_x_n y1 y2 y3 y4 y5 y6)`,
(* {{{ proof *)
[
REWRITE_TAC[Sphere.y_of_x;Sphere.lmdih3_x_div_sqrtdelta_posbranch;Sphere.rotate3;Sphere.ldih3_x_div_sqrtdelta_posbranch;lmdih3_x_n;ldih3_x_n];
REPEAT STRIP_TAC;
ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih_ldih];
]);;
(* }}} *)
let lmdih5_ldih5_n = rr prove_by_refinement(
`!y1 y2 y3 y4 y5 y6. (&0 <= y5 /\ y5 <= &2 * h0) ==>(y_of_x lmdih5_x_n y1 y2 y3 y4 y5 y6 = y_of_x ldih5_x_n y1 y2 y3 y4 y5 y6)`,
(* {{{ proof *)
[
REWRITE_TAC[Sphere.y_of_x;Sphere.lmdih5_x_div_sqrtdelta_posbranch;Sphere.rotate5;Sphere.ldih5_x_div_sqrtdelta_posbranch;lmdih5_x_n;ldih5_x_n];
REPEAT STRIP_TAC;
ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih_ldih];
]);;
(* }}} *)
let lmdih6_ldih6_n = rr prove_by_refinement(
`!y1 y2 y3 y4 y5 y6. (&0 <= y6 /\ y6 <= &2 * h0) ==>(y_of_x lmdih6_x_n y1 y2 y3 y4 y5 y6 = y_of_x ldih6_x_n y1 y2 y3 y4 y5 y6)`,
(* {{{ proof *)
[
REWRITE_TAC[Sphere.y_of_x;Sphere.lmdih6_x_div_sqrtdelta_posbranch;Sphere.rotate6;Sphere.ldih6_x_div_sqrtdelta_posbranch;lmdih6_x_n;ldih6_x_n];
REPEAT STRIP_TAC;
ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih_ldih];
]);;
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
let gamma3f_126_expand = prove_by_refinement(
`!y1 y2 y3 y4 y5 y6.
gamma3f_126 y1 y2 y3 y4 y5 y6 f =
vol3r y1 y2 y6 sqrt2 - ((&2 * mm1 /
pi) *
(&2 *
dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 + &2 *
dih2_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
&2 *
dih6_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
dih3_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
dih4_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
dih5_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - &3 *
pi) -
(&8 * mm2 /
pi) *
(f (y1 / &2) *
dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
f (y2 / &2) *
dih2_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
f (y6 / &2) *
dih6_y y1 y2 sqrt2 sqrt2 sqrt2 y6))`,
(* {{{ proof *)
[
REPEAT STRIP_TAC;
REWRITE_TAC[
gamma3f_126;Sphere.gamma3f;];
MESON_TAC[
vol3f_palt];
]);;
(* }}} *)
let gamma3f_135_expand = prove_by_refinement(
`!y1 y2 y3 y4 y5 y6.
gamma3f_135 y1 y2 y3 y4 y5 y6 f =
vol3r y1 y3 y5 sqrt2 - ( (&2 * mm1 /
pi) *
(&2 *
dih_y y1 sqrt2 y3 sqrt2 y5 sqrt2 + &2 *
dih3_y y1 sqrt2 y3 sqrt2 y5 sqrt2 +
&2 *
dih5_y y1 sqrt2 y3 sqrt2 y5 sqrt2 +
dih2_y y1 sqrt2 y3 sqrt2 y5 sqrt2 +
dih4_y y1 sqrt2 y3 sqrt2 y5 sqrt2 +
dih6_y y1 sqrt2 y3 sqrt2 y5 sqrt2 - &3 *
pi) -
(&8 * mm2 /
pi) *
(f (y1 / &2) *
dih_y y1 sqrt2 y3 sqrt2 y5 sqrt2 +
f (y3 / &2) *
dih3_y y1 sqrt2 y3 sqrt2 y5 sqrt2 +
f (y5 / &2) *
dih5_y y1 sqrt2 y3 sqrt2 y5 sqrt2))`,
(* }}} *)
dih_x_135_s2];
]);;
(* }}} *)
(*
let taum_template_B_x_alt = prove_by_refinement(
`!x1 x12 x15 x2 x3 x34 x4 x45 x5 x6.
taum_template_B_x x15 x45 x34 x12 x1 x2 x3 x4 x5 x6 =
taum_x x1 x3 x4 x34 (edge_flat2_x x5 x1 x4 (&0) x45 x15)
(edge_flat2_x x2 x1 x3 (&0) x12 x12) +
flat_term_x x2 +
flat_term_x x5 `,
(* {{{ proof *)
[
REWRITE_TAC[Sphere.taum_template_B_x];
REPEAT LET_TAC;
ASM_MESON_TAC[];
]);;
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
*)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* function delta_top_x is deprecated:
let delta_top_x_alt = prove_by_refinement(
`!a. delta_y (sqrt x4) (sqrt x9) (sqrt x6) a (sqrt x5) (sqrt x8) =
delta_top_x (a:real) (x1:real) (x2:real) (x3:real) (x4:real)
(x5:real) (x6:real) (x7:real) (x8:real) (x9:real)
`,
(* {{{ proof *)
[
REWRITE_TAC[Sphere.delta_top_x];
]);;
(* }}} *)
*)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* this differs from C++ code? *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
let functional_taum_x1 = prove_by_refinement(
`!a b.
domain6
(\x1 x2 x3 x4 x5 x6. &0 <= a /\ &0 <= b)
(
taum_x1 a b)
(compose6
taum_x four6 four6 four6
(constant6 (a*a)) (constant6 (b*b))
proj_x1)`,
(* {{{ proof *)
[
REWRITE_TAC[domain6;compose6;four6;constant6;Sphere.taum_x1; Sphere.taum_y1;Sphere.taum_x;Nonlinear_lemma.taum_123;
proj_x1; Sphere.rhazim_x;Sphere.rhazim2_x; Collect_geom2.SQRT4_EQ2; Sphere.rhazim3_x];
BY(SIMP_TAC[Nonlinear_lemma.sqrtxx])
]);;
(* }}} *)
let functional_taum_x2 = prove_by_refinement(
`!a b.
domain6
(\x1 x2 x3 x4 x5 x6. &0 <= a /\ &0 <= b)
(
taum_x2 a b)
(compose6
taum_x four6 four6 four6
(constant6 (a*a)) (constant6 (b*b))
proj_x2)`,
(* {{{ proof *)
[
REWRITE_TAC[domain6;compose6;four6;constant6;Sphere.taum_x2; Sphere.taum_y2;Sphere.taum_x;Nonlinear_lemma.taum_123;
proj_x2; Sphere.rhazim_x;Sphere.rhazim2_x; Collect_geom2.SQRT4_EQ2; Sphere.rhazim3_x];
BY(SIMP_TAC[Nonlinear_lemma.sqrtxx])
]);;
(* }}} *)
let functional_taum_x1_x2 = prove_by_refinement(
`!a.
domain6
(\x1 x2 x3 x4 x5 x6. &0 <= a)
(
taum_x1_x2 a)
(compose6
taum_x four6 four6 four6
(constant6 (a*a))
proj_x1 proj_x2)`,
(* {{{ proof *)
[
REWRITE_TAC[domain6;compose6;four6;constant6;Sphere.taum_x1_x2; Sphere.taum_y1_y2;Sphere.taum_x;Nonlinear_lemma.taum_123;
proj_x2;
proj_x1;Sphere.rhazim_x;Sphere.rhazim2_x; Collect_geom2.SQRT4_EQ2; Sphere.rhazim3_x];
BY(SIMP_TAC[Nonlinear_lemma.sqrtxx])
]);;
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(* }}} *)
(*
let functional1_vol2r_x =
new_definition `vol2r_x x = &2 * pi * (&2 - (x / &4)) / &3`;;
let functional_vol2r_x1 =
new_definition `vol2r_x1 = promote1_to_6 vol2r_x`;;
(*
let functional1_vol2_x =
new_definition `vol2_x x = &2 * pi * (&2 - (sqrt x) / &4) / &3`;;
let functional_vol2_x1 =
new_definition `vol2_x1 = promote1_to_6 vol2_x`;;
*)
let functional_gamma3f_x_v_lfun = prove_by_refinement(
`
let vv_term_m1 = scalar6 (unit6 - scalar6
proj_y1 (&1 / sqrt8)) (&4 * mm1) in
let (vv_term_m2) =
(scalar6 (uni(
flat_term_x,
proj_x1)) (-- &16 * mm2 /sol0)) in
domain6
(\x1 x2 x3 x4 x5 x6.
&0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x4 /\ &0 <= x5 /\ &0 <= x6)
gamma3f_x_v_lfun ((
dih_x - constant6 (&2 * #0.03)) *
((vol2r_x1 - vv_term_m1 ) + vv_term_m2))`,
(* {{{ proof *)
[
rt[domain6;
LET_DEF;
LET_END_DEF;Nonlinear_lemma.gamma3f_x_v_lfun;mul6;sub6;Nonlinear_lemma.gamma3f_v_lfun;constant6;Sphere.vol2r;functional_vol2_x1;functional1_vol2_x;
promote1_to_6;mul6;add6;scalar6;uni;
proj_x1;Sphere.dih_y;Nonlinear_lemma.sqrt2_sqrt2;
proj_y1;functional_vol2r_x1;functional1_vol2r_x;Sphere.lfun;unit6;Sphere.flat_term_x;Sphere.flat_term;Nonlinear_lemma.sqrt8_sqrt2];
simp[
sqrt_sqrt]
st/r
AP_TERM_TAC
sgthen `(
sqrt x1 / &2) pow 2 = x1 / &4` SUBST1_TAC
rt[arith `(
sqrt x1 / &2) pow 2 = (
sqrt x1 *
sqrt x1) / &4`]
asimp[
sqrt_sqrt]
ABBREV_TAC `a = &2 *
pi * (&2 - x1/ &4) / &3`
rt[arith `((a:real) - b + c = a - (b - c))`]
AP_TERM_TAC
]);;
(* }}} *)
1;;
*)
(*
let taud_D2_num_x_y = prove_by_refinement(
`!y1 y2 y3 y4 y5 y6.
&0 <= y1 /\ &0 <= y2 /\ &0 <= y3 ==>
taud_v4_D2_num y1 y2 y3 y4 y5 y6 = y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6`,
(* {{{ proof *)
[
REWRITE_TAC[Nonlin_def.taud_v4_D2_num;Nonlin_def.taud_D2_num_x];
F_REWRITE_TAC;
REWRITE_TAC[GSYM mu_y];
REWRITE_TAC[GSYM Sphere.delta_y];
ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx];
BY(REAL_ARITH_TAC)
]);;
(* }}} *)
*)
(* arclength_x_345 deprecated *)
(* this could be rewriten further with eulerA_x *)
(*
let functional_sol_euler_x_divsqrtdelta = prove_by_refinement(
`let a = uni(sqrt,proj_x1 * proj_x2 * proj_x3) +
proj_y1 * (proj_x2 + proj_x3 - proj_x4) * constant6 (#0.5) +
proj_y2 * (proj_x1 + proj_x3 - proj_x5) * constant6 (#0.5) +
proj_y3 * (proj_x1 + proj_x2 - proj_x6) * constant6 (#0.5) in
(sol_euler_x_div_sqrtdelta =
(uni(matan,(delta_x / (a * a * constant6 (&4))))) / a)`,
(* {{{ proof *)
[
LET_TAC;
FIRST_X_ASSUM MP_TAC;
REWRITE_TAC[FUN_EQ_THM];
REWRITE_TAC[uni;Sphere.sol_euler_x_div_sqrtdelta; div6;mul6;add6;sub6;constant6;proj_y1;proj_y2; proj_y3;proj_x1;proj_x2;proj_x3; proj_x4;proj_x5;proj_x6];
REWRITE_TAC[REAL_ARITH `x * #0.5 = x/ &2`;REAL_ARITH `&4 * a pow 2 = a* a * &4`];
REPEAT STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC o (ISPECL [`x:real`;`x':real`; `x'':real`;`x''':real`;`x'''':real`; `x''''':real`]));
ASM_REWRITE_TAC[];
REWRITE_TAC[LET_DEF;LET_END_DEF];
]);;
(* }}} *)
*)
(*
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 * compose6 dih_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
two6 * compose6 dih2_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
two6 * compose6 dih6_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
compose6 dih3_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
compose6 dih4_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
compose6 dih5_x proj_x1 proj_x2 two6 two6 two6 proj_x6 -
constant6 ( &3 * pi))
- (constant6 (&8 * mm2 / pi)) *
(compose6 ldih2_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
compose6 ldih6_x proj_x1 proj_x2 two6 two6 two6 proj_x6)))`,
(* {{{ proof *)
[
REWRITE_TAC[LET_DEF;LET_END_DEF;domain6; two6;constant6;mul6;add6;sub6;proj_x1;compose6;proj_x2; proj_x3;proj_x4;proj_x5;proj_x6];
BY(REWRITE_TAC[Nonlinear_lemma.vol3f_x_sqrt2_lmplus_alt])
]);;
(* }}} *)
*)
(*
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 * compose6 dih_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
two6 * compose6 dih2_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
two6 * compose6 dih6_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
compose6 dih3_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
compose6 dih4_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
compose6 dih5_x proj_x1 proj_x2 two6 two6 two6 proj_x6 -
constant6 ( &3 * pi))
- (constant6 (&8 * mm2 / pi)) *
(compose6 ldih_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
compose6 ldih2_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
compose6 ldih6_x proj_x1 proj_x2 two6 two6 two6 proj_x6)))
`,
(* {{{ proof *)
[
REWRITE_TAC[LET_DEF;LET_END_DEF; two6; domain6;constant6;mul6;add6;sub6;proj_x1; compose6;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6];
BY(REWRITE_TAC[Nonlinear_lemma.vol3f_x_lfun_alt])
]);;
(* }}} *)
*)
(*
let functional_ldih_x = prove_by_refinement(
`ldih_x =
(unit6 * constant6 h0 + proj_y1 * constant6 ( -- #0.5))*
(unit6 / (constant6 h0 - unit6)) * dih_x`,
(* {{{ proof *)
[
REWRITE_TAC[FUN_EQ_THM];
REWRITE_TAC[add6;mul6;div6;sub6;constant6];
REWRITE_TAC[proj_y1;Sphere.ldih_x;Nonlinear_lemma.unit6;Sphere.lfun];
REAL_ARITH_TAC;
]);;
(* }}} *)
*)
(*
let functional_lfun_y1 = prove_by_refinement(
`lfun_y1 = (unit6 * constant6 h0 + proj_x1 * constant6 (-- &1))*
(unit6 / (constant6 h0 - unit6))`,
(* {{{ proof *)
[
REWRITE_TAC[FUN_EQ_THM];
REWRITE_TAC[add6;mul6;div6;sub6;constant6];
REWRITE_TAC[Sphere.lfun_y1;Sphere.lfun; Nonlinear_lemma.unit6;Nonlinear_lemma.proj_x1];
REAL_ARITH_TAC;
]);;
(* }}} *)
*)
(*
let functional_vol_x = prove_by_refinement(
`vol_x = uni(sqrt,delta_x) / constant6 (&12)`,
(* {{{ proof *)
[
BY(REWRITE_TAC[FUN_EQ_THM;uni;Sphere.vol_x;constant6;div6]);
]);;
(* }}} *)
*)
(* }}} *)