(* let truncate_gamma23_x_A = new_definition `truncate_gamma23_x_A iw1 m1 m2 m6 = scalar6 (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6) dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6) iw1 + (dih_x - (mk_126 (truncate_dih_x (#0.14)) + constant6 (#0.08))) * uni((truncate_gamma2_x m1), proj_x1)`;; *) let truncate_gamma23_x_C = new_definition `truncate_gamma23_x_C d iw1 m1 m2 m6 = scalar6 (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6) dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6) iw1 + (dih_x - (mk_126 (truncate_dih_x (#0.14)) + constant6 (d))) * uni((truncate_gamma2_x m1), proj_x1)`;; let truncate_gamma23_x_B = new_definition `truncate_gamma23_x_B m1 = (dih_x - constant6 (&2 * #0.08)) * uni((truncate_gamma2_x m1),proj_x1)`;; (* 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 nonf_truncate_gamma23_x_B = prove_by_refinement( `! m1 x1 x2 x3 x4 x5 x6. truncate_gamma23_x_B m1 x1 x2 x3 x4 x5 x6 = (dih_x x1 x2 x3 x4 x5 x6 - &2 * #0.08) * truncate_gamma2_x m1 x1 `, (* {{{ proof *) [ REWRITE_TAC[truncate_gamma23_x_B;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 nonf_truncate_gamma23_x_C = prove_by_refinement( `!iw1 m1 m2 m6 x1 x2 x3 x4 x5 x6. truncate_gamma23_x_C d 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 + d)) * truncate_gamma2_x m1 x1`, (* {{{ proof *) [ REWRITE_TAC[truncate_gamma23_x_C;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 nonf_truncate_gamma3f_x = prove_by_refinement( `!d m4 m5 m6 x1 x2 x3 x4 x5 x6. truncate_gamma3f_x d m4 m5 m6 x1 x2 x3 x4 x5 x6 = truncate_vol3r_456 d x1 x2 x3 x4 x5 x6 - truncate_vol3f d m4 m5 m6 x1 x2 x3 x4 x5 x6`, (* {{{ proof *) [ BY(REWRITE_TAC[truncate_gamma3f_x;sub6]) ]);; (* }}} *) let nonf_truncate_gamma23_x = prove_by_refinement( `!iw1 iw2 m1 m2 m3 m5 m6 x1 x2 x3 x4 x5 x6. truncate_gamma23_x iw1 iw2 m1 m2 m3 m5 m6 x1 x2 x3 x4 x5 x6 = truncate_gamma3f_x #0.14 m1 m2 m6 (&0) (&0) (&0) x1 x2 x6 * iw1 + truncate_gamma3f_x #0.14 m1 m3 m5 (&0) (&0) (&0) x1 x3 x5 * iw2 + (dih_x x1 x2 x3 x4 x5 x6 - (truncate_dih_x #0.14 x1 x2 (&2) (&2) (&2) x6 + truncate_dih_x #0.14 x1 (&2) x3 (&2) x5 (&2))) * truncate_gamma2_x m1 x1`, (* {{{ proof *) [ BY(REWRITE_TAC[truncate_gamma23_x;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 nonf_truncate_sol_x = prove_by_refinement( `!c x1 x2 x3 x4 x5 x6. truncate_sol_x c x1 x2 x3 x4 x5 x6 = truncate_dih_x c x1 x2 x3 x4 x5 x6 + truncate_dih_x c x2 x3 x1 x5 x6 x4 + truncate_dih_x c x3 x1 x2 x6 x4 x5 - pi`, (* {{{ proof *) [ BY(REWRITE_TAC[truncate_sol_x;add6;sub6;constant6;Sphere.rotate2;Sphere.rotate3]) ]);; (* }}} *) let nonf_truncate_vol_x = prove_by_refinement( `!c x1 x2 x3 x4 x5 x6. truncate_vol_x c x1 x2 x3 x4 x5 x6 = (truncate_sqrt c (delta_x x1 x2 x3 x4 x5 x6)) / &12`, (* {{{ proof *) [ REWRITE_TAC[truncate_vol_x;scalar6;uni;]; BY(REAL_ARITH_TAC) ]);; (* }}} *) let nonf_truncate_vol3r_456 = prove_by_refinement( `!c x1 x2 x3 x4 x5 x6. truncate_vol3r_456 c x1 x2 x3 x4 x5 x6 = truncate_vol_x c (&2) (&2) (&2) x4 x5 x6`, (* {{{ proof *) [ BY(REWRITE_TAC[mk_456;truncate_vol3r_456;compose6;two6;proj_x4;proj_x5;proj_x6;constant6]) ]);; (* }}} *) let nonf_truncate_vol3f = prove_by_refinement( `!c m4 m5 m6 x1 x2 x3 x4 x5 x6. truncate_vol3f c m4 m5 m6 x1 x2 x3 x4 x5 x6 = ((truncate_sol_x c x5 (&2) x4 (&2) x6 (&2) + truncate_sol_x c x6 (&2) x5 (&2) x4 (&2) + truncate_sol_x c x4 (&2) x6 (&2) x5 (&2)) * &2 * mm1 / pi - ((lfun (sqrt x4 * #0.5) * m4) * truncate_dih_x c x4 (&2) x6 (&2) x5 (&2) + (lfun (sqrt x5 * #0.5) * m5) * truncate_dih_x c x5 (&2) x4 (&2) x6 (&2) + (lfun (sqrt x6 * #0.5) * m6) * truncate_dih_x c x6 (&2) x5 (&2) x4 (&2)) * &8 * mm2 / pi )`, (* {{{ proof *) [ BY(REWRITE_TAC[truncate_vol3f;add6;scalar6;mul6;uni;proj_y4;proj_y5;proj_y6;Sphere.rotate5;Sphere.rotate6;Sphere.rotate4;sub6;mk_456;compose6;two6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;constant6]) ]);; (* }}} *) let functional_delta_pent_x = prove_by_refinement( `delta_pent_x = compose6 delta_x proj_x1 proj_x2 proj_x6 four6 four6 (constant6 (#10.4976))`, (* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;Sphere.delta_pent_x;proj_x1;proj_x2;proj_x6;four6;constant6;compose6]; REPEAT WEAK_STRIP_TAC; AP_TERM_TAC; BY(REAL_ARITH_TAC) ]);; (* }}} *) (* 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 gamma3f_135_n_alt = prove_by_refinement( `!y1 y2 y3 y4 y5 y6. gamma3f_135_n y1 y2 y3 y4 y5 y6 = gamma3f_135_s_n y1 y2 y3 y4 y5 y6 + (&8 * mm2/ pi) * (y_of_x lmdih_x_n y1 y2 y3 y4 y5 y6 + y_of_x lmdih3_x_n y1 y2 y3 y4 y5 y6 + y_of_x lmdih5_x_n y1 y2 y3 y4 y5 y6)`, (* {{{ proof *) [ REWRITE_TAC[Sphere.gamma3f_135_n;gamma3f_135_s_n;lmdih_x_n;lmdih3_x_n;lmdih5_x_n;Sphere.y_of_x;Sphere.delta_y]; REAL_ARITH_TAC; ]);; (* }}} *) let gamma3f_126_n_alt = prove_by_refinement( `!y1 y2 y3 y4 y5 y6. gamma3f_126_n y1 y2 y3 y4 y5 y6 = gamma3f_126_s_n y1 y2 y3 y4 y5 y6 + (&8 * mm2/ pi) * (y_of_x lmdih_x_n y1 y2 y3 y4 y5 y6 + y_of_x lmdih2_x_n y1 y2 y3 y4 y5 y6 + y_of_x lmdih6_x_n y1 y2 y3 y4 y5 y6)`, (* {{{ proof *) [ REWRITE_TAC[Sphere.gamma3f_126_n;gamma3f_126_s_n;lmdih_x_n;lmdih2_x_n;lmdih6_x_n;Sphere.y_of_x;Sphere.delta_y]; REAL_ARITH_TAC; ]);; (* }}} *) let gamma23f_n_alt = prove_by_refinement( `!y1 y2 y3 y4 y5 y6 w1 w2 f. gamma23f_n y1 y2 y3 y4 y5 y6 w1 w2 sqrt2 f = gamma3f_126_n y1 y2 sqrt2 sqrt2 sqrt2 y6 / &w1 + gamma3f_135_n y1 sqrt2 y3 sqrt2 y5 sqrt2 / &w2 + gamma3f_vLR_n y1 y2 y3 y4 y5 y6 f`, (* {{{ proof *) [ REWRITE_TAC[gamma3f_vLR_n;Sphere.gamma23f_n]; ]);; (* }}} *) let gamma23f_126_03_n_alt = prove_by_refinement( `!y1 y2 y3 y4 y5 y6 f. gamma23f_126_03_n y1 y2 y3 y4 y5 y6 w1 sqrt2 f = gamma3f_126_n y1 y2 sqrt2 sqrt2 sqrt2 y6 / &w1 + gamma3f_vL_n y1 y2 y3 y4 y5 y6 f`, (* {{{ proof *) [ REWRITE_TAC[gamma3f_vL_n;Sphere.gamma23f_126_03_n]; ]);; (* }}} *) let gamma3f_vLR_n0_case = prove_by_refinement( `!y1 y2 y3 y4 y5 y6. &2 * h0 <= y1 ==> gamma3f_vLR_n y1 y2 y3 y4 y5 y6 lmfun = gamma3f_vLR_n0 y1 y2 y3 y4 y5 y6`, (* {{{ proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[gamma3f_vLR_n;gamma3f_vLR_n0;Sphere.vol2f;]; ASM_SIMP_TAC[lmfun0;REAL_MUL_RZERO;REAL_SUB_RZERO]; ]);; (* }}} *) let gamma3f_vLR_nlfun_case = prove_by_refinement( `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 ==> gamma3f_vLR_n y1 y2 y3 y4 y5 y6 lmfun = gamma3f_vLR_nlfun y1 y2 y3 y4 y5 y6`, (* {{{ proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[gamma3f_vLR_n;Sphere.vol2f;gamma3f_vLR_nlfun]; ASM_SIMP_TAC[lmfun_lfun]; ]);; (* }}} *) let gamma3f_vL_n0_case = prove_by_refinement( `!y1 y2 y3 y4 y5 y6. &2 * h0 <= y1 ==> gamma3f_vL_n y1 y2 y3 y4 y5 y6 lmfun = gamma3f_vL_n0 y1 y2 y3 y4 y5 y6`, (* {{{ proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[gamma3f_vL_n;Sphere.vol2f;gamma3f_vL_n0]; ASM_SIMP_TAC[lmfun0;REAL_MUL_RZERO;REAL_SUB_RZERO]; ]);; (* }}} *) let gamma3f_vL_nlfun_case = prove_by_refinement( `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 ==> gamma3f_vL_n y1 y2 y3 y4 y5 y6 lmfun = gamma3f_vL_nlfun y1 y2 y3 y4 y5 y6`, (* {{{ proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[gamma3f_vL_n;Sphere.vol2f;gamma3f_vL_nlfun]; ASM_SIMP_TAC[lmfun_lfun]; ]);; (* }}} *) 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 gamma23f' = prove_by_refinement( `!y1 y2 y3 y4 y5 y6 w1 w2 f. gamma23f y1 y2 y3 y4 y5 y6 w1 w2 sqrt2 f = gamma3f_126 y1 y2 y3 y4 y5 y6 f / &w1 + gamma3f_135 y1 y2 y3 y4 y5 y6 f / &w2 + gamma3f_vLR y1 y2 y3 y4 y5 y6 f `, (* {{{ proof *) [ REWRITE_TAC[gamma23f;gamma3f_126;gamma3f_135;gamma3f_vLR]; ]);; (* }}} *) let gamma23f_126_03' = prove_by_refinement( `!y1 y2 y3 y4 y5 y6 w1 f. gamma23f_126_03 y1 y2 y3 y4 y5 y6 w1 sqrt2 f = gamma3f_126 y1 y2 y3 y4 y5 y6 f / &w1 + gamma3f_vL y1 y2 y3 y4 y5 y6 f `, (* {{{ proof *) [ REWRITE_TAC[gamma23f_126_03;gamma3f_126;gamma3f_vL]; ]);; (* }}} *) let gamma23f_v' = prove_by_refinement( `!y1 y2 y3 y4 y5 y6 w1 f. gamma23f_red_03 y1 y2 y3 y4 y5 y6 sqrt2 f = gamma3f_v y1 y2 y3 y4 y5 y6 f `, (* {{{ proof *) [ REWRITE_TAC[gamma23f_red_03;gamma3f_v]; ]);; (* }}} *) let gamma3f_vLR0_case = prove_by_refinement( `!y1 y2 y3 y4 y5 y6. &2 * h0 <= y1 ==> gamma3f_vLR y1 y2 y3 y4 y5 y6 lmfun = gamma3f_vLR0 y1 y2 y3 y4 y5 y6`, (* {{{ proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[gamma3f_vLR;Sphere.vol2f;gamma3f_vLR0]; ASM_SIMP_TAC[lmfun0;REAL_MUL_RZERO;REAL_SUB_RZERO]; ]);; (* }}} *) let gamma3f_vLR_lfun_case = prove_by_refinement( `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 ==> gamma3f_vLR y1 y2 y3 y4 y5 y6 lmfun = gamma3f_vLR_lfun y1 y2 y3 y4 y5 y6`, (* {{{ proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[gamma3f_vLR;Sphere.vol2f;gamma3f_vLR_lfun]; ASM_SIMP_TAC[lmfun_lfun]; ]);; (* }}} *) let gamma3f_vL0_case = prove_by_refinement( `!y1 y2 y3 y4 y5 y6. &2 * h0 <= y1 ==> gamma3f_vL y1 y2 y3 y4 y5 y6 lmfun = gamma3f_vL0 y1 y2 y3 y4 y5 y6`, (* {{{ proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[gamma3f_vL;Sphere.vol2f;gamma3f_vL0]; ASM_SIMP_TAC[lmfun0;REAL_MUL_RZERO;REAL_SUB_RZERO]; ]);; (* }}} *) let gamma3f_vL_lfun_case = prove_by_refinement( `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 ==> gamma3f_vL y1 y2 y3 y4 y5 y6 lmfun = gamma3f_vL_lfun y1 y2 y3 y4 y5 y6`, (* {{{ proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[gamma3f_vL;Sphere.vol2f;gamma3f_vL_lfun]; ASM_SIMP_TAC[lmfun_lfun]; ]);; (* }}} *) let gamma3f_v0_case = prove_by_refinement( `!y1 y2 y3 y4 y5 y6. &2 * h0 <= y1 ==> gamma3f_v y1 y2 y3 y4 y5 y6 lmfun = gamma3f_v0 y1 y2 y3 y4 y5 y6`, (* {{{ proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[gamma3f_v;Sphere.vol2f;gamma3f_v0]; ASM_SIMP_TAC[lmfun0;REAL_MUL_RZERO;REAL_SUB_RZERO]; ]);; (* }}} *) let gamma3f_v_lfun_case = prove_by_refinement( `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 ==> gamma3f_v y1 y2 y3 y4 y5 y6 lmfun = gamma3f_v_lfun y1 y2 y3 y4 y5 y6`, (* {{{ proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[gamma3f_v;Sphere.vol2f;gamma3f_v_lfun]; ASM_SIMP_TAC[lmfun_lfun]; ]);; (* }}} *) 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))`, (* {{{ proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[gamma3f_135;Sphere.gamma3f;]; MESON_TAC[vol3f_135_palt]; ]);; (* }}} *) let ldih_x_135_s2 = prove_by_refinement( `!x1 x2 x3 x4 x5 x6. ldih_x_135_s2 x1 x2 x3 x4 x5 x6 = lfun (sqrt x1 / #2.0) * dih_x_135_s2 x1 x2 x3 x4 x5 x6`, (* {{{ proof *) [ REWRITE_TAC[ldih_x_135_s2';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[]; ]);; (* }}} *) let dih_template_B_x_alt = prove_by_refinement( `!x6 x25 x34 x5 x4 x45 x15 x2 x1 x3 x12. dih_template_B_x x15 x45 x34 x12 x25 x1 x2 x3 x4 x5 x6 = dih_x x1 x2 x5 x25 x15 x12 - dih_x x1 x3 x4 x34 (edge_flat2_x x5 x1 x4 (&0) x45 x15) (edge_flat2_x x2 x1 x3 (&0) x12 x12)`, (* {{{ proof *) [ REWRITE_TAC[Sphere.dih_template_B_x]; REPEAT LET_TAC; ASM_MESON_TAC[]; ]);; (* }}} *) let delta_template_B_x_alt = prove_by_refinement( `!x6 x25 x34 x5 x4 x45 x15 x2 x1 x3 x12. delta_template_B_x x15 x45 x34 x12 x1 x2 x3 x4 x5 x6 = delta_x x1 x3 x4 x34 (edge_flat2_x x5 x1 x4 (&0) x45 x15) (edge_flat2_x x2 x1 x3 (&0) x12 x12)`, (* {{{ proof *) [ REWRITE_TAC[Sphere.delta_template_B_x]; REPEAT LET_TAC; ASM_MESON_TAC[]; ]);; (* }}} *) let tau_lowform_x_alt = prove_by_refinement( `!x1 x2 x3 x4 x5 x6. tau_lowform_x x1 x2 x3 x4 x5 x6 = rho (sqrt x1) * pi - (pi + sol0) + sqp (delta_x x1 x2 x3 x4 x5 x6) * rhazim_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 + sqn (delta_x x1 x2 x3 x4 x5 x6) * rhazim2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 + sqn (delta_x x1 x2 x3 x4 x5 x6) * rhazim3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`, (* {{{ proof *) [ REWRITE_TAC[tau_lowform_x]; REPEAT LET_TAC; ASM_MESON_TAC[]; ]);; (* }}} *) *) let taum_3flat_x_alt = prove_by_refinement( `!x1 x2 x3 x23 x13 x12. taum_3flat_x x1 x2 x3 x23 x13 x12 = (taum_x x1 x2 x3 ( edge_flat2_x x23 x2 x3 (&0) (&4) (&4) ) ( edge_flat2_x x13 x1 x3 (&0) (&4) (&4) ) ( edge_flat2_x x12 x1 x2 (&0) (&4) (&4) ) + flat_term_x x12 + flat_term_x x23 + flat_term_x x13)`, (* {{{ proof *) [ REWRITE_TAC[Sphere.taum_3flat_x]; REPEAT LET_TAC; ASM_MESON_TAC[]; ]);; (* }}} *) let taum_2flat_x_alt = prove_by_refinement( `!x1 x2 x3 x4 x13 x12. taum_2flat_x x1 x2 x3 x4 x13 x12 = (taum_x x1 x2 x3 x4 ( edge_flat2_x x13 x1 x3 (&0) (&4) (&4) ) ( edge_flat2_x x12 x1 x2 (&0) (&4) (&4) ) + flat_term_x x12 + flat_term_x x13)`, (* {{{ proof *) [ REWRITE_TAC[Sphere.taum_2flat_x]; REPEAT LET_TAC; ASM_MESON_TAC[]; ]);; (* }}} *) let taum_1flat_x_alt = prove_by_refinement( `!x1 x2 x3 x4 x5 x12. taum_1flat_x x1 x2 x3 x4 x5 x12 = (taum_x x1 x2 x3 x4 x5 ( edge_flat2_x x12 x1 x2 (&0) (&4) (&4) ) + flat_term_x x12)`, (* {{{ proof *) [ REWRITE_TAC[Sphere.taum_1flat_x]; REPEAT LET_TAC; ASM_MESON_TAC[]; ]);; (* }}} *) let euler_3flat_x_alt = prove_by_refinement( `!x1 x2 x3 x23 x13 x12. euler_3flat_x x1 x2 x3 x23 x13 x12 = (eulerA_x x1 x2 x3 ( edge_flat2_x x23 x2 x3 (&0) (&4) (&4) ) ( edge_flat2_x x13 x1 x3 (&0) (&4) (&4) ) ( edge_flat2_x x12 x1 x2 (&0) (&4) (&4) ) )`, (* {{{ proof *) [ REWRITE_TAC[Sphere.euler_3flat_x]; REPEAT LET_TAC; ASM_MESON_TAC[]; ]);; (* }}} *) let euler_2flat_x_alt = prove_by_refinement( `!x1 x2 x3 x4 x13 x12. euler_2flat_x x1 x2 x3 x4 x13 x12 = (eulerA_x x1 x2 x3 x4 ( edge_flat2_x x13 x1 x3 (&0) (&4) (&4) ) ( edge_flat2_x x12 x1 x2 (&0) (&4) (&4) ) )`, (* {{{ proof *) [ REWRITE_TAC[Sphere.euler_2flat_x]; REPEAT LET_TAC; ASM_MESON_TAC[]; ]);; (* }}} *) let euler_1flat_x_alt = prove_by_refinement( `!x1 x2 x3 x4 x5 x12. euler_1flat_x x1 x2 x3 x4 x5 x12 = (eulerA_x x1 x2 x3 x4 x5 ( edge_flat2_x x12 x1 x2 (&0) (&4) (&4) ) )`, (* {{{ proof *) [ REWRITE_TAC[Sphere.euler_1flat_x]; REPEAT LET_TAC; ASM_MESON_TAC[]; ]);; (* }}} *) let upper_dih_x_y = prove_by_refinement( `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6. (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\ (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==> (upper_dih_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) = upper_dih_x x1 x2 x3 x4 x5 x6)`, (* {{{ proof *) [ REWRITE_TAC[Sphere.upper_dih_y;Sphere.y_of_x;LET_DEF;LET_END_DEF]; ASM_MESON_TAC[sq_pow2]; ]);; (* }}} *) (* 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]; ]);; (* }}} *) *) let functional_euler_3flat_x = prove_by_refinement( `let x4r = compose6 edge_flat2_x proj_x4 proj_x2 proj_x3 zero6 four6 four6 in let x5r = compose6 edge_flat2_x proj_x5 proj_x1 proj_x3 zero6 four6 four6 in let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in ( euler_3flat_x = compose6 eulerA_x proj_x1 proj_x2 proj_x3 x4r x5r x6r)`, (* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Sphere.euler_3flat_x;compose6;four6;zero6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;constant6;LET_DEF;LET_END_DEF]) ]);; (* }}} *) let functional_euler_2flat_x = prove_by_refinement( ` let x5r = compose6 edge_flat2_x proj_x5 proj_x1 proj_x3 zero6 four6 four6 in let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in ( euler_2flat_x = compose6 eulerA_x proj_x1 proj_x2 proj_x3 proj_x4 x5r x6r)`, (* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Sphere.euler_2flat_x;compose6;four6;zero6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;constant6;LET_DEF;LET_END_DEF]) ]);; (* }}} *) let functional_euler_1flat_x = prove_by_refinement( ` let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in ( euler_1flat_x = compose6 eulerA_x proj_x1 proj_x2 proj_x3 proj_x4 proj_x5 x6r)`, (* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Sphere.euler_1flat_x;compose6;four6;zero6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;constant6;LET_DEF;LET_END_DEF]) ]);; (* }}} *) let functional_taum_3flat_x = prove_by_refinement( `let x4r = compose6 edge_flat2_x proj_x4 proj_x2 proj_x3 zero6 four6 four6 in let x5r = compose6 edge_flat2_x proj_x5 proj_x1 proj_x3 zero6 four6 four6 in let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in ( taum_3flat_x = compose6 taum_x proj_x1 proj_x2 proj_x3 x4r x5r x6r + uni(flat_term_x,proj_x4) + uni(flat_term_x,proj_x5) + uni(flat_term_x,proj_x6))`, (* {{{ proof *) [ (REWRITE_TAC[FUN_EQ_THM;Sphere.taum_3flat_x;compose6;four6;add6;uni;zero6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;constant6;LET_DEF;LET_END_DEF]); BY(REAL_ARITH_TAC) ]);; (* }}} *) let functional_taum_2flat_x = prove_by_refinement( ` let x5r = compose6 edge_flat2_x proj_x5 proj_x1 proj_x3 zero6 four6 four6 in let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in ( taum_2flat_x = compose6 taum_x proj_x1 proj_x2 proj_x3 proj_x4 x5r x6r + uni(flat_term_x,proj_x5) + uni(flat_term_x,proj_x6))`, (* {{{ proof *) [ (REWRITE_TAC[FUN_EQ_THM;Sphere.taum_2flat_x;compose6;four6;add6;uni;zero6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;constant6;LET_DEF;LET_END_DEF]); BY(REAL_ARITH_TAC) ]);; (* }}} *) let functional_taum_1flat_x = prove_by_refinement( ` let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in ( taum_1flat_x = compose6 taum_x proj_x1 proj_x2 proj_x3 proj_x4 proj_x5 x6r + uni(flat_term_x,proj_x6))`, (* {{{ proof *) [ (REWRITE_TAC[FUN_EQ_THM;Sphere.taum_1flat_x;compose6;four6;add6;uni;zero6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;constant6;LET_DEF;LET_END_DEF]); ]);; (* }}} *) let functional_delta_x_126_s2 = prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x6) delta_x_126_s2 ( mk_126 delta_x)`, (* {{{ proof *) [ REWRITE_TAC[domain6;Nonlinear_lemma.delta_x_126_s2;Sphere.delta_y;mk_126;compose6;proj_x1;proj_x2;proj_x6;two6;constant6;Nonlinear_lemma.sqrt2_sqrt2]; BY(ASM_SIMP_TAC[sqrt_sqrt]) ]);; (* }}} *) let functional_delta_x_135_s2 = prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x3 /\ &0 <= x5) delta_x_135_s2 ( mk_135 delta_x)`, (* {{{ proof *) [ REWRITE_TAC[domain6;Nonlinear_lemma.delta_x_135_s2;Sphere.delta_y;mk_135;compose6;proj_x1;proj_x3;proj_x5;two6;constant6;Nonlinear_lemma.sqrt2_sqrt2]; BY(ASM_SIMP_TAC[sqrt_sqrt]) ]);; (* }}} *) let functional_vol3_x_135_s2 = prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x3 /\ &0 <= x5) vol3_x_135_s2 ( mk_135 vol_x)`, (* {{{ proof *) [ REWRITE_TAC[domain6;Nonlinear_lemma.vol3_x_135_s2;mk_135;Sphere.vol3r;compose6;proj_x1;proj_x3;proj_x5;two6;constant6;Sphere.vol_y;Sphere.y_of_x;Nonlinear_lemma.sqrt2_sqrt2]; ASM_SIMP_TAC[sqrt_sqrt]; REPEAT WEAK_STRIP_TAC; REWRITE_TAC[Sphere.vol_x;Sphere.delta_x]; REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC); BY(REAL_ARITH_TAC) ]);; (* }}} *) let functional_dih_x_126_s2 = prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x6) dih_x_126_s2 (mk_126 dih_x)`, (* {{{ proof *) [ REWRITE_TAC[domain6;Nonlinear_lemma.dih_x_126_s2;constant6;compose6;mk_126;two6;proj_x1;proj_x2;proj_x6;Sphere.dih_y;LET_DEF;LET_END_DEF;Nonlinear_lemma.sqrt2_sqrt2]; BY(ASM_SIMP_TAC[sqrt_sqrt]) ]);; (* }}} *) let functional_dih2_x_126_s2 = prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x6) dih2_x_126_s2 ( mk_126 dih2_x)`, (* {{{ proof *) [ REWRITE_TAC[domain6;Nonlinear_lemma.dih2_x_126_s2;mk_126;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2]; REPEAT WEAK_STRIP_TAC; GMATCH (ISPECL (replicate `&0` 6) Nonlinear_lemma.dih2_x_y); REPEAT (POP_ASSUM MP_TAC); BY(REAL_ARITH_TAC) ]);; (* }}} *) let functional_dih3_x_126_s2 = prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x6) dih3_x_126_s2 ( mk_126 dih3_x)`, (* {{{ proof *) [ REWRITE_TAC[domain6;Nonlinear_lemma.dih3_x_126_s2; mk_126;compose6;proj_x1;proj_x2;two6;proj_x6; constant6;Sphere.sqrt2]; REPEAT WEAK_STRIP_TAC; GMATCH (ISPECL (replicate `&0` 6) Nonlinear_lemma.dih3_x_y); REPEAT (POP_ASSUM MP_TAC); BY(REAL_ARITH_TAC) ]);; (* }}} *) let functional_dih4_x_126_s2 = prove_by_refinement( ` dih4_x_126_s2= ( mk_126 dih4_x)`, (* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.dih4_x_126_s2;mk_126;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2;Sphere.dih4_x]; ]);; (* }}} *) let functional_dih5_x_126_s2 = prove_by_refinement( ` dih5_x_126_s2= ( mk_126 dih5_x)`, (* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.dih5_x_126_s2; mk_126;compose6;proj_x1;proj_x2; two6;proj_x6;constant6; Sphere.sqrt2;Sphere.dih5_x]; ]);; (* }}} *) let functional_dih6_x_126_s2 = prove_by_refinement( ` dih6_x_126_s2= ( mk_126 dih6_x)`, (* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.dih6_x_126_s2;mk_126;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2;Sphere.dih6_x]; ]);; (* }}} *) let functional_dih_x_135_s2 = prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x3 /\ &0 <= x5) dih_x_135_s2 (mk_135 dih_x)`, (* {{{ proof *) [ REWRITE_TAC[domain6;Nonlinear_lemma.dih_x_135_s2;constant6;compose6;mk_135;two6;proj_x1;proj_x3;proj_x5;Sphere.dih_y;LET_DEF;LET_END_DEF;Nonlinear_lemma.sqrt2_sqrt2]; BY(ASM_SIMP_TAC[sqrt_sqrt]) ]);; (* }}} *) let functional_dih2_x_135_s2 = prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x3 /\ &0 <= x5) dih2_x_135_s2 ( mk_135 dih2_x)`, (* {{{ proof *) [ REWRITE_TAC[domain6;Nonlinear_lemma.dih2_x_135_s2;mk_135;compose6;proj_x1;proj_x3;two6;proj_x5;constant6;Sphere.sqrt2]; REPEAT WEAK_STRIP_TAC; GMATCH (ISPECL (replicate `&0` 6) Nonlinear_lemma.dih2_x_y); REPEAT (POP_ASSUM MP_TAC); BY(REAL_ARITH_TAC) ]);; (* }}} *) let functional_dih3_x_135_s2 = prove_by_refinement( `domain6 (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x3 /\ &0 <= x5) dih3_x_135_s2 ( mk_135 dih3_x)`, (* {{{ proof *) [ REWRITE_TAC[domain6;Nonlinear_lemma.dih3_x_135_s2;mk_135;compose6;proj_x1;proj_x3;two6;proj_x5;constant6;Sphere.sqrt2]; REPEAT WEAK_STRIP_TAC; GMATCH (ISPECL (replicate `&0` 6) Nonlinear_lemma.dih3_x_y); REPEAT (POP_ASSUM MP_TAC); BY(REAL_ARITH_TAC) ]);; (* }}} *) let functional_dih4_x_135_s2 = prove_by_refinement( ` dih4_x_135_s2= ( mk_135 dih4_x)`, (* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.dih4_x_135_s2;mk_135;compose6;proj_x1;proj_x3;two6;proj_x5;constant6;Sphere.sqrt2;Sphere.dih4_x]; ]);; (* }}} *) let functional_dih5_x_135_s2 = prove_by_refinement( ` dih5_x_135_s2= ( mk_135 dih5_x)`, (* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.dih5_x_135_s2;mk_135;compose6;proj_x1;proj_x3;two6;proj_x5;constant6;Sphere.sqrt2;Sphere.dih5_x]; ]);; (* }}} *) let functional_dih6_x_135_s2 = prove_by_refinement( ` dih6_x_135_s2= ( mk_135 dih6_x)`, (* {{{ proof *) [ REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.dih6_x_135_s2;mk_135;compose6;proj_x1;proj_x3;two6;proj_x5;constant6;Sphere.sqrt2;Sphere.dih6_x]; ]);; (* }}} *) let functional_ldih_x_126_s2 = prove_by_refinement( ` ldih_x_126_s2= uni (lfun, (proj_y1 / two6)) * dih_x_126_s2`, (* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih_x_126_s2;mk_126;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2;uni;mul6;div6;proj_y1;arith `&2 = #2.0`]) ]);; (* }}} *) let functional_ldih2_x_126_s2 = prove_by_refinement( ` ldih2_x_126_s2= uni (lfun, (proj_y2 / two6)) * dih2_x_126_s2`, (* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih2_x_126_s2;mk_126;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2;uni;mul6;div6;proj_y2;arith `&2 = #2.0`]) ]);; (* }}} *) let functional_ldih6_x_126_s2 = prove_by_refinement( ` ldih6_x_126_s2= uni (lfun, (proj_y6 / two6)) * dih6_x_126_s2`, (* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih6_x_126_s2;mk_126;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2;uni;mul6;div6;proj_y6;arith `&2 = #2.0`]) ]);; (* }}} *) let functional_ldih_x_135_s2 = prove_by_refinement( ` ldih_x_135_s2= uni (lfun, (proj_y1 / two6)) * dih_x_135_s2`, (* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih_x_135_s2;mk_135;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2;uni;mul6;div6;proj_y1;arith `&2 = #2.0`]) ]);; (* }}} *) let functional_ldih3_x_135_s2 = prove_by_refinement( ` ldih3_x_135_s2= uni (lfun, (proj_y3 / two6)) * dih3_x_135_s2`, (* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih3_x_135_s2;mk_135;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2;uni;mul6;div6;proj_y3;arith `&2 = #2.0`]) ]);; (* }}} *) let functional_ldih5_x_135_s2 = prove_by_refinement( ` ldih5_x_135_s2= uni (lfun, (proj_y5 / two6)) * dih5_x_135_s2`, (* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih5_x_135_s2;mk_135;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2;uni;mul6;div6;proj_y5;arith `&2 = #2.0`]) ]);; (* }}} *) let functional_ldih_x_126_n = prove_by_refinement( `ldih_x_126_n = mk_126 ldih_x_n`, (* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih_x_126_n;mk_126;Nonlinear_lemma.sqrt2_sqrt2;proj_x1;proj_x2;proj_x6;compose6;two6;constant6]) ]);; (* }}} *) (* this differs from C++ code? *) let functional_ldih2_x_126_n = prove_by_refinement( `ldih2_x_126_n = mk_126 (rotate2 ldih_x_n)`, (* {{{ proof *) [ (REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih2_x_126_n;functional_ldih_x_126_n;mk_126;Sphere.rotate2;Nonlinear_lemma.sqrt2_sqrt2;proj_x1;proj_x2;proj_x6;compose6;two6;constant6]); REWRITE_TAC[Nonlinear_lemma.ldih2_x_n;Nonlinear_lemma.ldih_x_n;Sphere.ldih2_x_div_sqrtdelta_posbranch;Sphere.rotate2]; REPEAT WEAK_STRIP_TAC; REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC); REWRITE_TAC[Sphere.delta_x]; BY(REAL_ARITH_TAC) ]);; (* }}} *) let functional_ldih6_x_126_n = prove_by_refinement( `ldih6_x_126_n = mk_126 (rotate6 ldih_x_n)`, (* {{{ proof *) [ (REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih6_x_126_n;functional_ldih_x_126_n;mk_126;Sphere.rotate6;Nonlinear_lemma.sqrt2_sqrt2;proj_x1;proj_x2;proj_x6;compose6;two6;constant6]); REWRITE_TAC[Nonlinear_lemma.ldih6_x_n;Nonlinear_lemma.ldih_x_n;Sphere.ldih6_x_div_sqrtdelta_posbranch;Sphere.rotate6]; REPEAT WEAK_STRIP_TAC; REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC); REWRITE_TAC[Sphere.delta_x]; BY(REAL_ARITH_TAC) ]);; (* }}} *) let functional_ldih_x_135_n = prove_by_refinement( `ldih_x_135_n = mk_135 ldih_x_n`, (* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih_x_135_n;mk_135;Nonlinear_lemma.sqrt2_sqrt2;proj_x1;proj_x3;proj_x5;compose6;two6;constant6]) ]);; (* }}} *) let functional_ldih3_x_135_n = prove_by_refinement( `ldih3_x_135_n = mk_135 (rotate3 ldih_x_n)`, (* {{{ proof *) [ (REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih3_x_135_n;functional_ldih_x_135_n;mk_135;Sphere.rotate2;Nonlinear_lemma.sqrt2_sqrt2;proj_x1;proj_x3;proj_x5;compose6;two6;constant6]); REWRITE_TAC[Nonlinear_lemma.ldih3_x_n;Nonlinear_lemma.ldih_x_n;Sphere.ldih3_x_div_sqrtdelta_posbranch;Sphere.rotate3]; REPEAT WEAK_STRIP_TAC; REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC); REWRITE_TAC[Sphere.delta_x]; BY(REAL_ARITH_TAC) ]);; (* }}} *) let functional_ldih5_x_135_n = prove_by_refinement( `ldih5_x_135_n = mk_135 (rotate5 ldih_x_n)`, (* {{{ proof *) [ (REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih5_x_135_n;functional_ldih_x_135_n;mk_135;Sphere.rotate5;Nonlinear_lemma.sqrt2_sqrt2;proj_x1;proj_x3;proj_x5;compose6;two6;constant6]); REWRITE_TAC[Nonlinear_lemma.ldih5_x_n;Nonlinear_lemma.ldih_x_n;Sphere.ldih5_x_div_sqrtdelta_posbranch;Sphere.rotate5]; REPEAT WEAK_STRIP_TAC; REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC); REWRITE_TAC[Sphere.delta_x]; BY(REAL_ARITH_TAC) ]);; (* }}} *) 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 functional_delta_sub1_x = prove_by_refinement( `!a. delta_sub1_x a = compose6 delta_x (constant6 a) proj_x2 proj_x3 proj_x4 proj_x5 proj_x6`, (* {{{ proof *) [ (REWRITE_TAC[FUN_EQ_THM; Sphere.delta_sub1_x;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6 ]) ]);; (* }}} *) let functional_taum_sub1_x = prove_by_refinement( `!a. taum_sub1_x a = compose6 taum_x (constant6 a) proj_x2 proj_x3 proj_x4 proj_x5 proj_x6`, (* {{{ proof *) [ (REWRITE_TAC[FUN_EQ_THM; Sphere.taum_sub1_x;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6 ]) ]);; (* }}} *) let functional_taum_sub246_x = prove_by_refinement( `!a b c. taum_sub246_x a b c = compose6 taum_x proj_x1 (constant6 a) proj_x3 (constant6 b) proj_x5 (constant6 c)`, (* {{{ proof *) [ (REWRITE_TAC[FUN_EQ_THM; Sphere.taum_sub246_x;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6 ]) ]);; (* }}} *) let functional_taum_sub345_x = prove_by_refinement( `!a b c. taum_sub345_x a b c = compose6 taum_x proj_x1 proj_x2 (constant6 a) (constant6 b) (constant6 c) proj_x6`, (* {{{ proof *) [ (REWRITE_TAC[FUN_EQ_THM; Sphere.taum_sub345_x;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6 ]) ]);; (* }}} *) (* 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]); ]);; (* }}} *) *) let x1cube = new_definition `x1cube = proj_x1 * proj_x1 * proj_x1`;; let functional_ldih_x_n = prove_by_refinement( `ldih_x_n = uni(sqn,delta_x) * ldih_x_div_sqrtdelta_posbranch`, (* {{{ proof *) [ BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih_x_n;mul6;uni]) ]);; (* }}} *)