legacy/oldnonlinear/cutlemmas.hl

   1 (*
   2 let truncate_gamma23_x_A = new_definition `truncate_gamma23_x_A iw1 m1 m2 m6 =
   3   scalar6
   4     (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
   5        dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
   6     iw1
   7   + (dih_x - (mk_126 (truncate_dih_x (#0.14)) + constant6 (#0.08))) *
   8        uni((truncate_gamma2_x m1), proj_x1)`;;
   9 *)
  10
  11 let truncate_gamma23_x_C = new_definition `truncate_gamma23_x_C d iw1 m1 m2 m6 =
  12   scalar6
  13     (compose6 (truncate_gamma3f_x (#0.14) m1 m2 m6)
  14        dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6)
  15     iw1
  16   + (dih_x - (mk_126 (truncate_dih_x (#0.14)) + constant6 (d))) *
  17        uni((truncate_gamma2_x m1), proj_x1)`;;
  18
  19
  20 let truncate_gamma23_x_B = new_definition
  21   `truncate_gamma23_x_B m1  =
  22        (dih_x  - constant6 (&2 * #0.08)) *
  23          uni((truncate_gamma2_x m1),proj_x1)`;;
  24
  25 (*
  26 let nonf_truncate_gamma23_x_A = prove_by_refinement(
  27   `!iw1 m1 m2 m6 x1 x2 x3 x4 x5 x6.
  28     truncate_gamma23_x_A iw1 m1 m2 m6 x1 x2 x3 x4 x5 x6 =
  29   truncate_gamma3f_x #0.14 m1 m2 m6 (&0) (&0) (&0) x1 x2 x6 * iw1 +
  30      (dih_x x1 x2 x3 x4 x5 x6 -
  31       (truncate_dih_x #0.14 x1 x2 (&2) (&2) (&2) x6 + #0.08)) *
  32      truncate_gamma2_x m1 x1`,
  33   (* {{{ proof *)
  34   [
  35 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]
  36   ]);;
  37   (* }}} *)
  38 *)
  39
  40 let nonf_truncate_gamma23_x_B = prove_by_refinement(
  41   `! m1 x1 x2 x3 x4 x5 x6.
  42     truncate_gamma23_x_B m1 x1 x2 x3 x4 x5 x6 =
  43     (dih_x x1 x2 x3 x4 x5 x6 - &2 * #0.08) * truncate_gamma2_x m1 x1 `,
  44   (* {{{ proof *)
  45   [
  46 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]
  47   ]);;
  48   (* }}} *)
  49
  50 let nonf_truncate_gamma23_x_C = prove_by_refinement(
  51   `!iw1 m1 m2 m6 x1 x2 x3 x4 x5 x6.
  52     truncate_gamma23_x_C d iw1 m1 m2 m6 x1 x2 x3 x4 x5 x6 =
  53   truncate_gamma3f_x #0.14 m1 m2 m6 (&0) (&0) (&0) x1 x2 x6 * iw1 +
  54      (dih_x x1 x2 x3 x4 x5 x6 -
  55       (truncate_dih_x #0.14 x1 x2 (&2) (&2) (&2) x6 + d)) *
  56      truncate_gamma2_x m1 x1`,
  57   (* {{{ proof *)
  58   [
  59 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]
  60   ]);;
  61   (* }}} *)
  62
  63 let nonf_truncate_gamma3f_x = prove_by_refinement(
  64   `!d m4 m5 m6 x1 x2 x3 x4 x5 x6.
  65     truncate_gamma3f_x d m4 m5 m6 x1 x2 x3 x4 x5 x6 =
  66     truncate_vol3r_456 d x1 x2 x3 x4 x5 x6 -
  67       truncate_vol3f d m4 m5 m6 x1 x2 x3 x4 x5 x6`,
  68   (* {{{ proof *)
  69   [
  70   BY(REWRITE_TAC[truncate_gamma3f_x;sub6])
  71   ]);;
  72   (* }}} *)
  73
  74 let nonf_truncate_gamma23_x = prove_by_refinement(
  75   `!iw1 iw2 m1 m2 m3 m5 m6 x1 x2 x3 x4 x5 x6.
  76     truncate_gamma23_x iw1 iw2 m1 m2 m3 m5 m6 x1 x2 x3 x4 x5 x6 =
  77 truncate_gamma3f_x #0.14 m1 m2 m6 (&0) (&0) (&0) x1 x2 x6 * iw1 +
  78      truncate_gamma3f_x #0.14 m1 m3 m5 (&0) (&0) (&0) x1 x3 x5 * iw2 +
  79      (dih_x x1 x2 x3 x4 x5 x6 -
  80       (truncate_dih_x #0.14 x1 x2 (&2) (&2) (&2) x6 +
  81        truncate_dih_x #0.14 x1 (&2) x3 (&2) x5 (&2))) *
  82      truncate_gamma2_x m1 x1`,
  83   (* {{{ proof *)
  84   [
  85  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])
  86   ]);;
  87   (* }}} *)
  88
  89 let nonf_truncate_sol_x = prove_by_refinement(
  90   `!c x1 x2 x3 x4 x5 x6.
  91     truncate_sol_x c x1 x2 x3 x4 x5 x6 = truncate_dih_x c x1 x2 x3 x4 x5 x6 +
  92     truncate_dih_x c x2 x3 x1 x5 x6 x4 + truncate_dih_x c x3 x1 x2 x6 x4 x5 - pi`,
  93   (* {{{ proof *)
  94   [
  95   BY(REWRITE_TAC[truncate_sol_x;add6;sub6;constant6;Sphere.rotate2;Sphere.rotate3])
  96   ]);;
  97   (* }}} *)
  98
  99 let nonf_truncate_vol_x = prove_by_refinement(
 100   `!c x1 x2 x3 x4 x5 x6.
 101     truncate_vol_x c x1 x2 x3 x4 x5 x6 = (truncate_sqrt c (delta_x x1 x2 x3 x4 x5 x6)) / &12`,
 102   (* {{{ proof *)
 103   [
 104   REWRITE_TAC[truncate_vol_x;scalar6;uni;];
 105   BY(REAL_ARITH_TAC)
 106   ]);;
 107   (* }}} *)
 108
 109 let nonf_truncate_vol3r_456 = prove_by_refinement(
 110   `!c x1 x2 x3 x4 x5 x6.
 111     truncate_vol3r_456 c x1 x2 x3 x4 x5 x6 =
 112     truncate_vol_x c (&2) (&2) (&2) x4 x5 x6`,
 113   (* {{{ proof *)
 114   [
 115   BY(REWRITE_TAC[mk_456;truncate_vol3r_456;compose6;two6;proj_x4;proj_x5;proj_x6;constant6])
 116   ]);;
 117   (* }}} *)
 118
 119 let nonf_truncate_vol3f = prove_by_refinement(
 120   `!c m4 m5 m6 x1 x2 x3 x4 x5 x6.
 121     truncate_vol3f c m4 m5 m6 x1 x2 x3 x4 x5 x6 =
 122    ((truncate_sol_x c x5 (&2) x4 (&2) x6 (&2) +
 123       truncate_sol_x c x6 (&2) x5 (&2) x4 (&2) +
 124       truncate_sol_x c x4 (&2) x6 (&2) x5 (&2)) *
 125      &2 *
 126      mm1 / pi -
 127      ((lfun (sqrt x4 * #0.5) * m4) * truncate_dih_x c x4 (&2) x6 (&2) x5 (&2) +
 128       (lfun (sqrt x5 * #0.5) * m5) * truncate_dih_x c x5 (&2) x4 (&2) x6 (&2) +
 129       (lfun (sqrt x6 * #0.5) * m6) * truncate_dih_x c x6 (&2) x5 (&2) x4 (&2)) *
 130      &8 *
 131      mm2 / pi )`,
 132   (* {{{ proof *)
 133   [
 134  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])
 135   ]);;
 136   (* }}} *)
 137
 138 let functional_delta_pent_x = prove_by_refinement(
 139   `delta_pent_x = compose6
 140     delta_x proj_x1 proj_x2 proj_x6 four6 four6 (constant6 (#10.4976))`,
 141   (* {{{ proof *)
 142   [
 143   REWRITE_TAC[FUN_EQ_THM;Sphere.delta_pent_x;proj_x1;proj_x2;proj_x6;four6;constant6;compose6];
 144   REPEAT WEAK_STRIP_TAC;
 145   AP_TERM_TAC;
 146   BY(REAL_ARITH_TAC)
 147   ]);;
 148   (* }}} *)
 149
 150 (*
 151 let promote_pow3r = INST_TYPE [(`:real`,`:A`);(`:real`,`:B`);(`:real`,`:C`);(`:real`,`:D`);(`:real`,`:E`)] promote_pow3;;
 152 *)
 153
 154
 155 (*
 156 let dih_y_div_sqrtdelta_posbranch = new_definition
 157   `dih_y_div_sqrtdelta_posbranch  = y_of_x dih_x_div_sqrtdelta_posbranch`;;
 158 *)
 159
 160
 161 (*
 162 let rhof_x = define `rhof_x x = rho (sqrt x)`;;
 163 *)
 164
 165
 166 (*
 167 let ineq_lemma = prove_by_refinement(
 168   `!a x b. &0 <= a  /\  &0 <= b /\  a pow 2 <= x /\ x <= b pow 2 ==> a <= sqrt x /\ sqrt x <= b`,
 169   (* {{{ proof *)
 170   [
 171   REPEAT GEN_TAC;
 172     STRIP_TAC;
 173     SUBGOAL_THEN `&0 <= x` MP_TAC;
 174   ASM_MESON_TAC [REAL_LE_TRANS;Collect_geom.REAL_LE_SQUARE_POW];
 175   ASM_MESON_TAC[Collect_geom.POW2_COND;SQRT_WORKS];
 176   ]);;
 177   (* }}} *)
 178 *)
 179
 180
 181
 182 (*
 183 let ineq_square  = prove_by_refinement(
 184   `((!y1 y2 y3 y4 y5 y6.
 185       ineq
 186         [(a1,y1,b1);(a2,y2,b2);(a3,y3,b3);(a4,y4,b4);(a5,y5,b5);(a6,y6,b6)]
 187           (P y1 y2 y3 y4 y5 y6)) ==>
 188       ((&0 <= a1 /\ &0 <= a2 /\ &0 <= a3 /\ &0 <= a4 /\ &0 <= a5 /\ &0 <= a6 /\
 189       &0 <= b1 /\ &0 <= b2 /\ &0 <= b3 /\ &0 <= b4 /\ &0 <= b5 /\ &0 <= b6 )) ==>
 190     (!x1 x2 x3 x4 x5 x6.
 191        ineq [(a1 pow 2,x1,b1 pow 2);(a2 pow 2,x2,b2 pow 2);(a3 pow 2,x3,b3 pow 2);
 192         (a4 pow 2,x4,b4 pow 2);(a5 pow 2,x5,b5 pow 2);(a6 pow 2,x6,b6 pow 2)]
 193           (P (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6))))`,
 194   (* {{{ proof *)
 195   [
 196   REWRITE_TAC[ineq];
 197   REPEAT STRIP_TAC;
 198   FIRST_X_ASSUM (fun t-> MP_TAC (SPECL [`sqrt x1`;`sqrt x2`;`sqrt x3`;`sqrt x4`;`sqrt x5`;`sqrt x6`] t));
 199   ASM_MESON_TAC[ineq_lemma];
 200   ]);;
 201   (* }}} *)
 202 *)
 203
 204
 205
 206
 207 let gamma3f_135_n_alt = prove_by_refinement(
 208   `!y1 y2 y3 y4 y5 y6.
 209    gamma3f_135_n y1 y2 y3 y4 y5 y6 = gamma3f_135_s_n y1 y2 y3 y4 y5 y6 +
 210    (&8 * mm2/ pi) *
 211     (y_of_x lmdih_x_n y1 y2 y3 y4 y5 y6 +
 212      y_of_x lmdih3_x_n y1 y2 y3 y4 y5 y6 +
 213      y_of_x lmdih5_x_n y1 y2 y3 y4 y5 y6)`,
 214   (* {{{ proof *)
 215   [
 216   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];
 217   REAL_ARITH_TAC;
 218   ]);;
 219   (* }}} *)
 220
 221 let gamma3f_126_n_alt = prove_by_refinement(
 222   `!y1 y2 y3 y4 y5 y6.
 223    gamma3f_126_n y1 y2 y3 y4 y5 y6 = gamma3f_126_s_n y1 y2 y3 y4 y5 y6 +
 224    (&8 * mm2/ pi) *
 225     (y_of_x lmdih_x_n y1 y2 y3 y4 y5 y6 +
 226      y_of_x lmdih2_x_n y1 y2 y3 y4 y5 y6 +
 227      y_of_x lmdih6_x_n y1 y2 y3 y4 y5 y6)`,
 228   (* {{{ proof *)
 229   [
 230   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];
 231   REAL_ARITH_TAC;
 232   ]);;
 233   (* }}} *)
 234
 235 let gamma23f_n_alt = prove_by_refinement(
 236   `!y1 y2 y3 y4 y5 y6 w1 w2 f. gamma23f_n y1 y2 y3 y4 y5 y6 w1 w2 sqrt2 f =
 237     gamma3f_126_n y1 y2 sqrt2 sqrt2 sqrt2 y6 / &w1 +
 238          gamma3f_135_n y1 sqrt2 y3 sqrt2 y5 sqrt2 / &w2 +
 239     gamma3f_vLR_n y1 y2 y3 y4 y5 y6 f`,
 240   (* {{{ proof *)
 241   [
 242   REWRITE_TAC[gamma3f_vLR_n;Sphere.gamma23f_n];
 243   ]);;
 244   (* }}} *)
 245
 246 let gamma23f_126_03_n_alt = prove_by_refinement(
 247   `!y1 y2 y3 y4 y5 y6 f. gamma23f_126_03_n y1 y2 y3 y4 y5 y6 w1 sqrt2 f =
 248          gamma3f_126_n y1 y2 sqrt2 sqrt2 sqrt2 y6 / &w1 +
 249    gamma3f_vL_n y1 y2 y3 y4 y5 y6 f`,
 250   (* {{{ proof *)
 251   [
 252   REWRITE_TAC[gamma3f_vL_n;Sphere.gamma23f_126_03_n];
 253   ]);;
 254   (* }}} *)
 255
 256 let gamma3f_vLR_n0_case = prove_by_refinement(
 257   `!y1 y2 y3 y4 y5 y6. &2 * h0 <= y1 ==> gamma3f_vLR_n y1 y2 y3 y4 y5 y6 lmfun =
 258     gamma3f_vLR_n0 y1 y2 y3 y4 y5 y6`,
 259   (* {{{ proof *)
 260   [
 261   REPEAT STRIP_TAC;
 262   REWRITE_TAC[gamma3f_vLR_n;gamma3f_vLR_n0;Sphere.vol2f;];
 263   ASM_SIMP_TAC[lmfun0;REAL_MUL_RZERO;REAL_SUB_RZERO];
 264   ]);;
 265   (* }}} *)
 266
 267 let gamma3f_vLR_nlfun_case = prove_by_refinement(
 268   `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 ==> gamma3f_vLR_n y1 y2 y3 y4 y5 y6 lmfun =
 269     gamma3f_vLR_nlfun y1 y2 y3 y4 y5 y6`,
 270   (* {{{ proof *)
 271   [
 272   REPEAT STRIP_TAC;
 273   REWRITE_TAC[gamma3f_vLR_n;Sphere.vol2f;gamma3f_vLR_nlfun];
 274   ASM_SIMP_TAC[lmfun_lfun];
 275   ]);;
 276   (* }}} *)
 277
 278 let gamma3f_vL_n0_case = prove_by_refinement(
 279   `!y1 y2 y3 y4 y5 y6. &2 * h0 <= y1 ==> gamma3f_vL_n y1 y2 y3 y4 y5 y6 lmfun =
 280     gamma3f_vL_n0 y1 y2 y3 y4 y5 y6`,
 281   (* {{{ proof *)
 282   [
 283   REPEAT STRIP_TAC;
 284   REWRITE_TAC[gamma3f_vL_n;Sphere.vol2f;gamma3f_vL_n0];
 285   ASM_SIMP_TAC[lmfun0;REAL_MUL_RZERO;REAL_SUB_RZERO];
 286   ]);;
 287   (* }}} *)
 288
 289 let gamma3f_vL_nlfun_case = prove_by_refinement(
 290   `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 ==> gamma3f_vL_n y1 y2 y3 y4 y5 y6 lmfun =
 291     gamma3f_vL_nlfun y1 y2 y3 y4 y5 y6`,
 292   (* {{{ proof *)
 293   [
 294   REPEAT STRIP_TAC;
 295   REWRITE_TAC[gamma3f_vL_n;Sphere.vol2f;gamma3f_vL_nlfun];
 296   ASM_SIMP_TAC[lmfun_lfun];
 297   ]);;
 298   (* }}} *)
 299
 300
 301 let rr f s = REWRITE_RULE[Sphere.y_of_x] (f s);;
 302
 303 let lmdih_n0 = rr prove_by_refinement(
 304   `!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y1 ) ==>(y_of_x lmdih_x_n y1 y2 y3 y4 y5 y6 =  &0 )`,
 305   (* {{{ proof *)
 306   [
 307   REWRITE_TAC[Sphere.y_of_x;lmdih_x_n];
 308     REPEAT STRIP_TAC;
 309     ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih0];
 310   REAL_ARITH_TAC;
 311   ]);;
 312   (* }}} *)
 313
 314 let lmdih2_n0 = rr prove_by_refinement(
 315   `!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y2 ) ==>(y_of_x lmdih2_x_n y1 y2 y3 y4 y5 y6 =  &0 )`,
 316   (* {{{ proof *)
 317   [
 318   REWRITE_TAC[Sphere.y_of_x;lmdih_x_n;lmdih2_x_n;Sphere.lmdih2_x_div_sqrtdelta_posbranch;Sphere.rotate2];
 319     REPEAT STRIP_TAC;
 320     ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih0];
 321   REAL_ARITH_TAC;
 322   ]);;
 323
 324 let lmdih3_n0 = rr prove_by_refinement(
 325   `!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y3 ) ==>(y_of_x lmdih3_x_n y1 y2 y3 y4 y5 y6 =  &0 )`,
 326   (* {{{ proof *)
 327   [
 328   REWRITE_TAC[Sphere.y_of_x;lmdih_x_n;lmdih3_x_n;Sphere.lmdih3_x_div_sqrtdelta_posbranch;Sphere.rotate3];
 329     REPEAT STRIP_TAC;
 330     ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih0];
 331   REAL_ARITH_TAC;
 332   ]);;
 333
 334 let lmdih5_n0 = rr prove_by_refinement(
 335   `!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y5 ) ==>(y_of_x lmdih5_x_n y1 y2 y3 y4 y5 y6 =  &0 )`,
 336   (* {{{ proof *)
 337   [
 338   REWRITE_TAC[Sphere.y_of_x;lmdih_x_n;lmdih5_x_n;Sphere.lmdih5_x_div_sqrtdelta_posbranch;Sphere.rotate5];
 339     REPEAT STRIP_TAC;
 340     ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih0];
 341   REAL_ARITH_TAC;
 342   ]);;
 343
 344 let lmdih6_n0 = rr prove_by_refinement(
 345   `!y1 y2 y3 y4 y5 y6. (&2 * h0 <= y6 ) ==>(y_of_x lmdih6_x_n y1 y2 y3 y4 y5 y6 =  &0 )`,
 346   (* {{{ proof *)
 347   [
 348   REWRITE_TAC[Sphere.y_of_x;lmdih_x_n;lmdih6_x_n;Sphere.lmdih6_x_div_sqrtdelta_posbranch;Sphere.rotate6];
 349     REPEAT STRIP_TAC;
 350     ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih0];
 351   REAL_ARITH_TAC;
 352   ]);;
 353
 354
 355 let lmdih_ldih_n = rr prove_by_refinement(
 356   `!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)`,
 357   (* {{{ proof *)
 358   [
 359   REWRITE_TAC[Sphere.y_of_x;lmdih_x_n;ldih_x_n];
 360   REPEAT STRIP_TAC;
 361   ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih_ldih];
 362   ]);;
 363   (* }}} *)
 364
 365 let lmdih2_ldih2_n = rr prove_by_refinement(
 366   `!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)`,
 367   (* {{{ proof *)
 368   [
 369   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];
 370   REPEAT STRIP_TAC;
 371   ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih_ldih];
 372   ]);;
 373   (* }}} *)
 374
 375 let lmdih3_ldih3_n = rr prove_by_refinement(
 376   `!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)`,
 377   (* {{{ proof *)
 378   [
 379   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];
 380   REPEAT STRIP_TAC;
 381   ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih_ldih];
 382   ]);;
 383   (* }}} *)
 384
 385 let lmdih5_ldih5_n = rr prove_by_refinement(
 386   `!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)`,
 387   (* {{{ proof *)
 388   [
 389   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];
 390   REPEAT STRIP_TAC;
 391   ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih_ldih];
 392   ]);;
 393   (* }}} *)
 394
 395 let lmdih6_ldih6_n = rr prove_by_refinement(
 396   `!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)`,
 397   (* {{{ proof *)
 398   [
 399   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];
 400   REPEAT STRIP_TAC;
 401   ASM_SIMP_TAC[REWRITE_RULE[Sphere.y_of_x] lmdih_ldih];
 402   ]);;
 403   (* }}} *)
 404
 405
 406
 407
 408
 409
 410 let gamma23f' = prove_by_refinement(
 411   `!y1 y2 y3 y4 y5 y6 w1 w2 f. gamma23f y1 y2 y3 y4 y5 y6 w1 w2 sqrt2 f =
 412      gamma3f_126 y1 y2 y3 y4 y5 y6 f / &w1 + gamma3f_135 y1 y2 y3 y4 y5 y6 f / &w2 +
 413      gamma3f_vLR y1 y2 y3 y4 y5 y6 f `,
 414   (* {{{ proof *)
 415   [
 416   REWRITE_TAC[gamma23f;gamma3f_126;gamma3f_135;gamma3f_vLR];
 417   ]);;
 418   (* }}} *)
 419
 420 let gamma23f_126_03' = prove_by_refinement(
 421   `!y1 y2 y3 y4 y5 y6 w1 f. gamma23f_126_03 y1 y2 y3 y4 y5 y6 w1 sqrt2 f =
 422      gamma3f_126 y1 y2 y3 y4 y5 y6 f / &w1 +   gamma3f_vL y1 y2 y3 y4 y5 y6 f `,
 423   (* {{{ proof *)
 424   [
 425   REWRITE_TAC[gamma23f_126_03;gamma3f_126;gamma3f_vL];
 426   ]);;
 427   (* }}} *)
 428
 429 let gamma23f_v' = prove_by_refinement(
 430   `!y1 y2 y3 y4 y5 y6 w1 f. gamma23f_red_03 y1 y2 y3 y4 y5 y6 sqrt2 f =
 431      gamma3f_v y1 y2 y3 y4 y5 y6 f `,
 432   (* {{{ proof *)
 433   [
 434   REWRITE_TAC[gamma23f_red_03;gamma3f_v];
 435   ]);;
 436   (* }}} *)
 437
 438
 439 let gamma3f_vLR0_case = prove_by_refinement(
 440   `!y1 y2 y3 y4 y5 y6. &2 * h0 <= y1 ==> gamma3f_vLR y1 y2 y3 y4 y5 y6 lmfun =
 441     gamma3f_vLR0 y1 y2 y3 y4 y5 y6`,
 442   (* {{{ proof *)
 443   [
 444   REPEAT STRIP_TAC;
 445   REWRITE_TAC[gamma3f_vLR;Sphere.vol2f;gamma3f_vLR0];
 446   ASM_SIMP_TAC[lmfun0;REAL_MUL_RZERO;REAL_SUB_RZERO];
 447   ]);;
 448   (* }}} *)
 449
 450
 451 let gamma3f_vLR_lfun_case = prove_by_refinement(
 452   `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 ==> gamma3f_vLR y1 y2 y3 y4 y5 y6 lmfun =
 453     gamma3f_vLR_lfun y1 y2 y3 y4 y5 y6`,
 454   (* {{{ proof *)
 455   [
 456   REPEAT STRIP_TAC;
 457   REWRITE_TAC[gamma3f_vLR;Sphere.vol2f;gamma3f_vLR_lfun];
 458   ASM_SIMP_TAC[lmfun_lfun];
 459   ]);;
 460   (* }}} *)
 461
 462 let gamma3f_vL0_case = prove_by_refinement(
 463   `!y1 y2 y3 y4 y5 y6. &2 * h0 <= y1 ==> gamma3f_vL y1 y2 y3 y4 y5 y6 lmfun =
 464     gamma3f_vL0 y1 y2 y3 y4 y5 y6`,
 465   (* {{{ proof *)
 466   [
 467   REPEAT STRIP_TAC;
 468   REWRITE_TAC[gamma3f_vL;Sphere.vol2f;gamma3f_vL0];
 469   ASM_SIMP_TAC[lmfun0;REAL_MUL_RZERO;REAL_SUB_RZERO];
 470   ]);;
 471   (* }}} *)
 472
 473 let gamma3f_vL_lfun_case = prove_by_refinement(
 474   `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 ==> gamma3f_vL y1 y2 y3 y4 y5 y6 lmfun =
 475     gamma3f_vL_lfun y1 y2 y3 y4 y5 y6`,
 476   (* {{{ proof *)
 477   [
 478   REPEAT STRIP_TAC;
 479   REWRITE_TAC[gamma3f_vL;Sphere.vol2f;gamma3f_vL_lfun];
 480   ASM_SIMP_TAC[lmfun_lfun];
 481   ]);;
 482   (* }}} *)
 483
 484
 485 let gamma3f_v0_case = prove_by_refinement(
 486   `!y1 y2 y3 y4 y5 y6. &2 * h0 <= y1 ==> gamma3f_v y1 y2 y3 y4 y5 y6 lmfun =
 487     gamma3f_v0 y1 y2 y3 y4 y5 y6`,
 488   (* {{{ proof *)
 489   [
 490   REPEAT STRIP_TAC;
 491   REWRITE_TAC[gamma3f_v;Sphere.vol2f;gamma3f_v0];
 492   ASM_SIMP_TAC[lmfun0;REAL_MUL_RZERO;REAL_SUB_RZERO];
 493   ]);;
 494   (* }}} *)
 495
 496 let gamma3f_v_lfun_case = prove_by_refinement(
 497   `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 ==> gamma3f_v y1 y2 y3 y4 y5 y6 lmfun =
 498     gamma3f_v_lfun y1 y2 y3 y4 y5 y6`,
 499   (* {{{ proof *)
 500   [
 501   REPEAT STRIP_TAC;
 502   REWRITE_TAC[gamma3f_v;Sphere.vol2f;gamma3f_v_lfun];
 503   ASM_SIMP_TAC[lmfun_lfun];
 504   ]);;
 505   (* }}} *)
 506
 507 let gamma3f_126_expand = prove_by_refinement(
 508   `!y1 y2 y3 y4 y5 y6. gamma3f_126 y1 y2 y3 y4 y5 y6 f =
 509      vol3r y1 y2 y6 sqrt2 - ((&2 * mm1 / pi) *
 510          (&2 * dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 + &2 * dih2_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
 511           &2 * dih6_y y1 y2 sqrt2 sqrt2 sqrt2 y6 + dih3_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
 512           dih4_y y1 y2 sqrt2 sqrt2 sqrt2 y6 + dih5_y y1 y2 sqrt2 sqrt2 sqrt2 y6 - &3 * pi) -
 513          (&8 * mm2 / pi) *
 514          (f (y1 / &2) * dih_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
 515           f (y2 / &2) * dih2_y y1 y2 sqrt2 sqrt2 sqrt2 y6 +
 516           f (y6 / &2) * dih6_y y1 y2 sqrt2 sqrt2 sqrt2 y6))`,
 517   (* {{{ proof *)
 518   [
 519   REPEAT STRIP_TAC;
 520   REWRITE_TAC[gamma3f_126;Sphere.gamma3f;];
 521   MESON_TAC[vol3f_palt];
 522   ]);;
 523   (* }}} *)
 524
 525
 526
 527
 528 let gamma3f_135_expand = prove_by_refinement(
 529   `!y1 y2 y3 y4 y5 y6. gamma3f_135 y1 y2 y3 y4 y5 y6 f =
 530      vol3r y1 y3 y5 sqrt2 - (  (&2 * mm1 / pi) *
 531          (&2 * dih_y y1 sqrt2 y3 sqrt2 y5 sqrt2 + &2 * dih3_y y1 sqrt2 y3 sqrt2 y5 sqrt2 +
 532           &2 * dih5_y y1 sqrt2 y3 sqrt2 y5 sqrt2 + dih2_y y1 sqrt2 y3 sqrt2 y5 sqrt2 +
 533           dih4_y y1 sqrt2 y3 sqrt2 y5 sqrt2 + dih6_y y1 sqrt2 y3 sqrt2 y5 sqrt2 - &3 * pi) -
 534          (&8 * mm2 / pi) *
 535          (f (y1 / &2) * dih_y y1 sqrt2 y3 sqrt2 y5 sqrt2 +
 536           f (y3 / &2) * dih3_y y1 sqrt2 y3 sqrt2 y5 sqrt2 +
 537           f (y5 / &2) * dih5_y y1 sqrt2 y3 sqrt2 y5 sqrt2))`,
 538   (* {{{ proof *)
 539   [
 540   REPEAT STRIP_TAC;
 541   REWRITE_TAC[gamma3f_135;Sphere.gamma3f;];
 542   MESON_TAC[vol3f_135_palt];
 543   ]);;
 544   (* }}} *)
 545
 546
 547 let ldih_x_135_s2 = prove_by_refinement(
 548   `!x1 x2 x3 x4 x5 x6. ldih_x_135_s2 x1 x2 x3 x4 x5 x6 =
 549       lfun (sqrt x1 / #2.0) * dih_x_135_s2 x1 x2 x3 x4 x5 x6`,
 550   (* {{{ proof *)
 551   [
 552   REWRITE_TAC[ldih_x_135_s2';dih_x_135_s2];
 553   ]);;
 554   (* }}} *)
 555
 556
 557
 558
 559 (*
 560 let taum_template_B_x_alt = prove_by_refinement(
 561   `!x1  x12  x15  x2  x3  x34  x4  x45  x5  x6.
 562     taum_template_B_x  x15 x45 x34 x12 x1 x2 x3 x4 x5 x6 =
 563     taum_x x1 x3 x4 x34 (edge_flat2_x x5 x1 x4 (&0) x45 x15)
 564       (edge_flat2_x x2 x1 x3 (&0) x12 x12) +
 565       flat_term_x x2 +
 566       flat_term_x x5 `,
 567   (* {{{ proof *)
 568
 569   [
 570   REWRITE_TAC[Sphere.taum_template_B_x];
 571   REPEAT  LET_TAC;
 572   ASM_MESON_TAC[];
 573   ]);;
 574
 575   (* }}} *)
 576
 577 let dih_template_B_x_alt = prove_by_refinement(
 578   `!x6 x25 x34 x5 x4 x45 x15 x2 x1 x3 x12.
 579     dih_template_B_x  x15 x45 x34 x12 x25 x1 x2 x3 x4 x5 x6 =
 580    dih_x x1 x2 x5 x25 x15 x12 -
 581      dih_x x1 x3 x4 x34 (edge_flat2_x x5 x1 x4 (&0) x45 x15)
 582      (edge_flat2_x x2 x1 x3 (&0) x12 x12)`,
 583   (* {{{ proof *)
 584   [
 585   REWRITE_TAC[Sphere.dih_template_B_x];
 586   REPEAT  LET_TAC;
 587   ASM_MESON_TAC[];
 588   ]);;
 589   (* }}} *)
 590
 591 let delta_template_B_x_alt = prove_by_refinement(
 592   `!x6 x25 x34 x5 x4 x45 x15 x2 x1 x3 x12.
 593     delta_template_B_x  x15 x45 x34 x12 x1 x2 x3 x4 x5 x6 =
 594      delta_x x1 x3 x4 x34 (edge_flat2_x x5 x1 x4 (&0) x45 x15)
 595      (edge_flat2_x x2 x1 x3 (&0) x12 x12)`,
 596   (* {{{ proof *)
 597   [
 598   REWRITE_TAC[Sphere.delta_template_B_x];
 599   REPEAT  LET_TAC;
 600   ASM_MESON_TAC[];
 601   ]);;
 602   (* }}} *)
 603
 604
 605 let tau_lowform_x_alt = prove_by_refinement(
 606   `!x1 x2 x3 x4 x5 x6.
 607     tau_lowform_x  x1 x2 x3 x4 x5 x6 =
 608    rho (sqrt x1) * pi - (pi + sol0) +
 609           sqp (delta_x x1 x2 x3 x4 x5 x6) * rhazim_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 +
 610           sqn  (delta_x x1 x2 x3 x4 x5 x6) * rhazim2_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6 +
 611           sqn  (delta_x x1 x2 x3 x4 x5 x6) * rhazim3_x_div_sqrtdelta_posbranch x1 x2 x3 x4 x5 x6`,
 612   (* {{{ proof *)
 613   [
 614   REWRITE_TAC[tau_lowform_x];
 615   REPEAT  LET_TAC;
 616   ASM_MESON_TAC[];
 617   ]);;
 618   (* }}} *)
 619
 620 *)
 621
 622 let taum_3flat_x_alt = prove_by_refinement(
 623   `!x1 x2 x3 x23 x13 x12.
 624     taum_3flat_x x1 x2 x3 x23 x13 x12 =
 625   (taum_x x1 x2 x3
 626   ( edge_flat2_x x23 x2 x3 (&0)    (&4) (&4) )
 627   ( edge_flat2_x x13 x1 x3 (&0)    (&4) (&4) )
 628   (  edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) )   +
 629    flat_term_x x12 + flat_term_x x23 + flat_term_x x13)`,
 630   (* {{{ proof *)
 631   [
 632   REWRITE_TAC[Sphere.taum_3flat_x];
 633   REPEAT  LET_TAC;
 634   ASM_MESON_TAC[];
 635   ]);;
 636   (* }}} *)
 637
 638
 639 let taum_2flat_x_alt = prove_by_refinement(
 640   `!x1 x2 x3 x4 x13 x12.
 641     taum_2flat_x x1 x2 x3 x4 x13 x12 =
 642   (taum_x x1 x2 x3 x4
 643   ( edge_flat2_x x13 x1 x3 (&0)    (&4) (&4) )
 644   (  edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) )   +
 645    flat_term_x x12 + flat_term_x x13)`,
 646   (* {{{ proof *)
 647   [
 648   REWRITE_TAC[Sphere.taum_2flat_x];
 649   REPEAT  LET_TAC;
 650   ASM_MESON_TAC[];
 651   ]);;
 652   (* }}} *)
 653
 654
 655 let taum_1flat_x_alt = prove_by_refinement(
 656   `!x1 x2 x3 x4 x5 x12.
 657     taum_1flat_x x1 x2 x3 x4 x5 x12 =
 658   (taum_x x1 x2 x3 x4 x5
 659   (  edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) )   +
 660    flat_term_x x12)`,
 661   (* {{{ proof *)
 662   [
 663   REWRITE_TAC[Sphere.taum_1flat_x];
 664   REPEAT  LET_TAC;
 665   ASM_MESON_TAC[];
 666   ]);;
 667   (* }}} *)
 668
 669
 670 let euler_3flat_x_alt = prove_by_refinement(
 671   `!x1 x2 x3 x23 x13 x12.
 672     euler_3flat_x x1 x2 x3 x23 x13 x12 =
 673   (eulerA_x x1 x2 x3
 674   ( edge_flat2_x x23 x2 x3 (&0)    (&4) (&4) )
 675   ( edge_flat2_x x13 x1 x3 (&0)    (&4) (&4) )
 676   (  edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) )  )`,
 677   (* {{{ proof *)
 678   [
 679   REWRITE_TAC[Sphere.euler_3flat_x];
 680   REPEAT  LET_TAC;
 681   ASM_MESON_TAC[];
 682   ]);;
 683   (* }}} *)
 684
 685
 686 let euler_2flat_x_alt = prove_by_refinement(
 687   `!x1 x2 x3 x4 x13 x12.
 688     euler_2flat_x x1 x2 x3 x4 x13 x12 =
 689   (eulerA_x x1 x2 x3 x4
 690   ( edge_flat2_x x13 x1 x3 (&0)    (&4) (&4) )
 691   (  edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) ) )`,
 692   (* {{{ proof *)
 693   [
 694   REWRITE_TAC[Sphere.euler_2flat_x];
 695   REPEAT  LET_TAC;
 696   ASM_MESON_TAC[];
 697   ]);;
 698   (* }}} *)
 699
 700
 701 let euler_1flat_x_alt = prove_by_refinement(
 702   `!x1 x2 x3 x4 x5 x12.
 703     euler_1flat_x x1 x2 x3 x4 x5 x12 =
 704   (eulerA_x x1 x2 x3 x4 x5
 705   (  edge_flat2_x x12 x1 x2 (&0)    (&4) (&4) )  )`,
 706   (* {{{ proof *)
 707   [
 708   REWRITE_TAC[Sphere.euler_1flat_x];
 709   REPEAT  LET_TAC;
 710   ASM_MESON_TAC[];
 711   ]);;
 712   (* }}} *)
 713
 714 let upper_dih_x_y = prove_by_refinement(
 715   `!a1 a2 a3 a4 a5 a6 x1 x2 x3 x4 x5 x6.
 716     (a1 pow 2 <= x1) /\ (a2 pow 2 <= x2) /\ (a3 pow 2 <= x3) /\ (a4 pow 2 <= x4) /\
 717     (a5 pow 2 <= x5) /\ (a6 pow 2 <= x6) ==>
 718     (upper_dih_y (sqrt x1) (sqrt x2) (sqrt x3) (sqrt x4) (sqrt x5) (sqrt x6) =
 719          upper_dih_x x1 x2 x3 x4 x5 x6)`,
 720   (* {{{ proof *)
 721   [
 722   REWRITE_TAC[Sphere.upper_dih_y;Sphere.y_of_x;LET_DEF;LET_END_DEF];
 723   ASM_MESON_TAC[sq_pow2];
 724   ]);;
 725   (* }}} *)
 726
 727
 728 (* function delta_top_x is deprecated:
 729 let delta_top_x_alt = prove_by_refinement(
 730   `!a. delta_y (sqrt x4) (sqrt x9) (sqrt x6) a (sqrt x5) (sqrt x8) =
 731     delta_top_x (a:real) (x1:real) (x2:real) (x3:real) (x4:real)
 732     (x5:real) (x6:real) (x7:real) (x8:real) (x9:real)
 733    `,
 734   (* {{{ proof *)
 735   [
 736   REWRITE_TAC[Sphere.delta_top_x];
 737   ]);;
 738   (* }}} *)
 739 *)
 740
 741
 742 let functional_euler_3flat_x = prove_by_refinement(
 743   `let x4r = compose6 edge_flat2_x proj_x4 proj_x2 proj_x3 zero6 four6 four6 in
 744   let x5r = compose6 edge_flat2_x proj_x5 proj_x1 proj_x3 zero6 four6 four6 in
 745   let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in
 746   ( euler_3flat_x =
 747     compose6 eulerA_x proj_x1 proj_x2 proj_x3 x4r x5r x6r)`,
 748   (* {{{ proof *)
 749   [
 750 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])
 751   ]);;
 752   (* }}} *)
 753
 754 let functional_euler_2flat_x = prove_by_refinement(
 755   `
 756   let x5r = compose6 edge_flat2_x proj_x5 proj_x1 proj_x3 zero6 four6 four6 in
 757   let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in
 758   ( euler_2flat_x =
 759     compose6 eulerA_x proj_x1 proj_x2 proj_x3 proj_x4 x5r x6r)`,
 760   (* {{{ proof *)
 761   [
 762 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])
 763   ]);;
 764   (* }}} *)
 765
 766 let functional_euler_1flat_x = prove_by_refinement(
 767   `
 768   let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in
 769   ( euler_1flat_x =
 770     compose6 eulerA_x proj_x1 proj_x2 proj_x3 proj_x4 proj_x5 x6r)`,
 771   (* {{{ proof *)
 772   [
 773 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])
 774   ]);;
 775   (* }}} *)
 776
 777
 778 let functional_taum_3flat_x = prove_by_refinement(
 779   `let x4r = compose6 edge_flat2_x proj_x4 proj_x2 proj_x3 zero6 four6 four6 in
 780   let x5r = compose6 edge_flat2_x proj_x5 proj_x1 proj_x3 zero6 four6 four6 in
 781   let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in
 782   ( taum_3flat_x =
 783       compose6 taum_x proj_x1 proj_x2 proj_x3 x4r x5r x6r +
 784     uni(flat_term_x,proj_x4) +
 785         uni(flat_term_x,proj_x5) +
 786         uni(flat_term_x,proj_x6))`,
 787   (* {{{ proof *)
 788   [
 789 (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]);
 790   BY(REAL_ARITH_TAC)
 791   ]);;
 792   (* }}} *)
 793
 794
 795 let functional_taum_2flat_x = prove_by_refinement(
 796   `
 797   let x5r = compose6 edge_flat2_x proj_x5 proj_x1 proj_x3 zero6 four6 four6 in
 798   let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in
 799   ( taum_2flat_x =
 800       compose6 taum_x proj_x1 proj_x2 proj_x3 proj_x4 x5r x6r +
 801         uni(flat_term_x,proj_x5) +
 802         uni(flat_term_x,proj_x6))`,
 803   (* {{{ proof *)
 804   [
 805 (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]);
 806   BY(REAL_ARITH_TAC)
 807   ]);;
 808   (* }}} *)
 809
 810
 811 let functional_taum_1flat_x = prove_by_refinement(
 812   `
 813    let x6r = compose6 edge_flat2_x proj_x6 proj_x1 proj_x2 zero6 four6 four6 in
 814   ( taum_1flat_x =
 815       compose6 taum_x proj_x1 proj_x2 proj_x3 proj_x4 proj_x5 x6r +
 816         uni(flat_term_x,proj_x6))`,
 817   (* {{{ proof *)
 818   [
 819 (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]);
 820   ]);;
 821   (* }}} *)
 822
 823 let functional_delta_x_126_s2 = prove_by_refinement(
 824   `domain6
 825      (\x1 x2 x3 x4 x5 x6.
 826      &0 <= x1 /\ &0 <= x2 /\ &0 <= x6)
 827   delta_x_126_s2 ( mk_126 delta_x)`,
 828   (* {{{ proof *)
 829   [
 830   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];
 831   BY(ASM_SIMP_TAC[sqrt_sqrt])
 832   ]);;
 833   (* }}} *)
 834
 835
 836 let functional_delta_x_135_s2 = prove_by_refinement(
 837   `domain6
 838      (\x1 x2 x3 x4 x5 x6.
 839      &0 <= x1 /\ &0 <= x3 /\ &0 <= x5)
 840   delta_x_135_s2 ( mk_135 delta_x)`,
 841   (* {{{ proof *)
 842   [
 843   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];
 844   BY(ASM_SIMP_TAC[sqrt_sqrt])
 845   ]);;
 846   (* }}} *)
 847
 848 let functional_vol3_x_135_s2 = prove_by_refinement(
 849   `domain6
 850      (\x1 x2 x3 x4 x5 x6.
 851      &0 <= x1 /\ &0 <= x3 /\ &0 <= x5)
 852   vol3_x_135_s2 ( mk_135 vol_x)`,
 853   (* {{{ proof *)
 854   [
 855 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];
 856   ASM_SIMP_TAC[sqrt_sqrt];
 857   REPEAT WEAK_STRIP_TAC;
 858   REWRITE_TAC[Sphere.vol_x;Sphere.delta_x];
 859   REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
 860   BY(REAL_ARITH_TAC)
 861   ]);;
 862   (* }}} *)
 863
 864
 865
 866 let functional_dih_x_126_s2 = prove_by_refinement(
 867   `domain6
 868     (\x1 x2 x3 x4 x5 x6.
 869      &0 <= x1 /\ &0 <= x2 /\ &0 <= x6)
 870     dih_x_126_s2  (mk_126 dih_x)`,
 871   (* {{{ proof *)
 872   [
 873 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];
 874   BY(ASM_SIMP_TAC[sqrt_sqrt])
 875   ]);;
 876   (* }}} *)
 877
 878 let functional_dih2_x_126_s2 = prove_by_refinement(
 879   `domain6
 880      (\x1 x2 x3 x4 x5 x6.
 881      &0 <= x1 /\ &0 <= x2 /\ &0 <= x6)
 882    dih2_x_126_s2 ( mk_126 dih2_x)`,
 883   (* {{{ proof *)
 884   [
 885 REWRITE_TAC[domain6;Nonlinear_lemma.dih2_x_126_s2;mk_126;compose6;proj_x1;proj_x2;two6;proj_x6;constant6;Sphere.sqrt2];
 886   REPEAT WEAK_STRIP_TAC;
 887 GMATCH (ISPECL (replicate `&0` 6)   Nonlinear_lemma.dih2_x_y);
 888   REPEAT (POP_ASSUM MP_TAC);
 889   BY(REAL_ARITH_TAC)
 890   ]);;
 891   (* }}} *)
 892
 893
 894 let functional_dih3_x_126_s2 = prove_by_refinement(
 895   `domain6
 896      (\x1 x2 x3 x4 x5 x6.
 897      &0 <= x1 /\ &0 <= x2 /\ &0 <= x6)
 898    dih3_x_126_s2 ( mk_126 dih3_x)`,
 899   (* {{{ proof *)
 900   [
 901     REWRITE_TAC[domain6;Nonlinear_lemma.dih3_x_126_s2; mk_126;compose6;proj_x1;proj_x2;two6;proj_x6; constant6;Sphere.sqrt2];
 902   REPEAT WEAK_STRIP_TAC;
 903 GMATCH (ISPECL (replicate `&0` 6)   Nonlinear_lemma.dih3_x_y);
 904   REPEAT (POP_ASSUM MP_TAC);
 905   BY(REAL_ARITH_TAC)
 906   ]);;
 907   (* }}} *)
 908
 909
 910 let functional_dih4_x_126_s2 = prove_by_refinement(
 911   `   dih4_x_126_s2= ( mk_126 dih4_x)`,
 912   (* {{{ proof *)
 913   [
 914 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];
 915   ]);;
 916   (* }}} *)
 917
 918
 919 let functional_dih5_x_126_s2 = prove_by_refinement(
 920   `   dih5_x_126_s2= ( mk_126 dih5_x)`,
 921   (* {{{ proof *)
 922   [
 923     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];
 924   ]);;
 925   (* }}} *)
 926
 927
 928 let functional_dih6_x_126_s2 = prove_by_refinement(
 929   `   dih6_x_126_s2= ( mk_126 dih6_x)`,
 930   (* {{{ proof *)
 931   [
 932 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];
 933   ]);;
 934   (* }}} *)
 935
 936 let functional_dih_x_135_s2 = prove_by_refinement(
 937   `domain6
 938     (\x1 x2 x3 x4 x5 x6.
 939      &0 <= x1 /\ &0 <= x3 /\ &0 <= x5)
 940     dih_x_135_s2  (mk_135 dih_x)`,
 941   (* {{{ proof *)
 942   [
 943 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];
 944   BY(ASM_SIMP_TAC[sqrt_sqrt])
 945   ]);;
 946   (* }}} *)
 947
 948
 949 let functional_dih2_x_135_s2 = prove_by_refinement(
 950   `domain6
 951      (\x1 x2 x3 x4 x5 x6.
 952      &0 <= x1 /\ &0 <= x3 /\ &0 <= x5)
 953    dih2_x_135_s2 ( mk_135 dih2_x)`,
 954   (* {{{ proof *)
 955   [
 956 REWRITE_TAC[domain6;Nonlinear_lemma.dih2_x_135_s2;mk_135;compose6;proj_x1;proj_x3;two6;proj_x5;constant6;Sphere.sqrt2];
 957   REPEAT WEAK_STRIP_TAC;
 958 GMATCH (ISPECL (replicate `&0` 6)   Nonlinear_lemma.dih2_x_y);
 959   REPEAT (POP_ASSUM MP_TAC);
 960   BY(REAL_ARITH_TAC)
 961   ]);;
 962   (* }}} *)
 963
 964
 965 let functional_dih3_x_135_s2 = prove_by_refinement(
 966   `domain6
 967      (\x1 x2 x3 x4 x5 x6.
 968      &0 <= x1 /\ &0 <= x3 /\ &0 <= x5)
 969    dih3_x_135_s2 ( mk_135 dih3_x)`,
 970   (* {{{ proof *)
 971   [
 972 REWRITE_TAC[domain6;Nonlinear_lemma.dih3_x_135_s2;mk_135;compose6;proj_x1;proj_x3;two6;proj_x5;constant6;Sphere.sqrt2];
 973   REPEAT WEAK_STRIP_TAC;
 974 GMATCH (ISPECL (replicate `&0` 6)   Nonlinear_lemma.dih3_x_y);
 975   REPEAT (POP_ASSUM MP_TAC);
 976   BY(REAL_ARITH_TAC)
 977   ]);;
 978   (* }}} *)
 979
 980
 981 let functional_dih4_x_135_s2 = prove_by_refinement(
 982   `   dih4_x_135_s2= ( mk_135 dih4_x)`,
 983   (* {{{ proof *)
 984   [
 985 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];
 986   ]);;
 987   (* }}} *)
 988
 989
 990 let functional_dih5_x_135_s2 = prove_by_refinement(
 991   `   dih5_x_135_s2= ( mk_135 dih5_x)`,
 992   (* {{{ proof *)
 993   [
 994 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];
 995   ]);;
 996   (* }}} *)
 997
 998
 999 let functional_dih6_x_135_s2 = prove_by_refinement(
1000   `   dih6_x_135_s2= ( mk_135 dih6_x)`,
1001   (* {{{ proof *)
1002   [
1003 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];
1004   ]);;
1005   (* }}} *)
1006
1007
1008
1009 let functional_ldih_x_126_s2 = prove_by_refinement(
1010   `   ldih_x_126_s2= uni (lfun, (proj_y1 / two6)) * dih_x_126_s2`,
1011   (* {{{ proof *)
1012   [
1013 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`])
1014   ]);;
1015   (* }}} *)
1016
1017 let functional_ldih2_x_126_s2 = prove_by_refinement(
1018   `   ldih2_x_126_s2= uni (lfun, (proj_y2 / two6)) * dih2_x_126_s2`,
1019   (* {{{ proof *)
1020   [
1021 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`])
1022   ]);;
1023   (* }}} *)
1024
1025
1026 let functional_ldih6_x_126_s2 = prove_by_refinement(
1027   `   ldih6_x_126_s2= uni (lfun, (proj_y6 / two6)) * dih6_x_126_s2`,
1028   (* {{{ proof *)
1029   [
1030 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`])
1031   ]);;
1032   (* }}} *)
1033
1034
1035 let functional_ldih_x_135_s2 = prove_by_refinement(
1036   `   ldih_x_135_s2= uni (lfun, (proj_y1 / two6)) * dih_x_135_s2`,
1037   (* {{{ proof *)
1038   [
1039 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`])
1040   ]);;
1041   (* }}} *)
1042
1043 let functional_ldih3_x_135_s2 = prove_by_refinement(
1044   `   ldih3_x_135_s2= uni (lfun, (proj_y3 / two6)) * dih3_x_135_s2`,
1045   (* {{{ proof *)
1046   [
1047 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`])
1048   ]);;
1049   (* }}} *)
1050
1051
1052 let functional_ldih5_x_135_s2 = prove_by_refinement(
1053   `   ldih5_x_135_s2= uni (lfun, (proj_y5 / two6)) * dih5_x_135_s2`,
1054   (* {{{ proof *)
1055   [
1056 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`])
1057   ]);;
1058   (* }}} *)
1059
1060 let functional_ldih_x_126_n = prove_by_refinement(
1061   `ldih_x_126_n = mk_126 ldih_x_n`,
1062   (* {{{ proof *)
1063   [
1064 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])
1065   ]);;
1066   (* }}} *)
1067
1068 (* this differs from C++ code? *)
1069
1070 let functional_ldih2_x_126_n = prove_by_refinement(
1071   `ldih2_x_126_n = mk_126 (rotate2 ldih_x_n)`,
1072   (* {{{ proof *)
1073   [
1074 (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]);
1075   REWRITE_TAC[Nonlinear_lemma.ldih2_x_n;Nonlinear_lemma.ldih_x_n;Sphere.ldih2_x_div_sqrtdelta_posbranch;Sphere.rotate2];
1076   REPEAT WEAK_STRIP_TAC;
1077   REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
1078   REWRITE_TAC[Sphere.delta_x];
1079   BY(REAL_ARITH_TAC)
1080   ]);;
1081   (* }}} *)
1082
1083
1084 let functional_ldih6_x_126_n = prove_by_refinement(
1085   `ldih6_x_126_n = mk_126 (rotate6 ldih_x_n)`,
1086   (* {{{ proof *)
1087   [
1088 (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]);
1089   REWRITE_TAC[Nonlinear_lemma.ldih6_x_n;Nonlinear_lemma.ldih_x_n;Sphere.ldih6_x_div_sqrtdelta_posbranch;Sphere.rotate6];
1090   REPEAT WEAK_STRIP_TAC;
1091   REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
1092   REWRITE_TAC[Sphere.delta_x];
1093   BY(REAL_ARITH_TAC)
1094   ]);;
1095   (* }}} *)
1096
1097 let functional_ldih_x_135_n = prove_by_refinement(
1098   `ldih_x_135_n = mk_135 ldih_x_n`,
1099   (* {{{ proof *)
1100   [
1101 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])
1102   ]);;
1103   (* }}} *)
1104
1105
1106 let functional_ldih3_x_135_n = prove_by_refinement(
1107   `ldih3_x_135_n = mk_135 (rotate3 ldih_x_n)`,
1108   (* {{{ proof *)
1109   [
1110 (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]);
1111   REWRITE_TAC[Nonlinear_lemma.ldih3_x_n;Nonlinear_lemma.ldih_x_n;Sphere.ldih3_x_div_sqrtdelta_posbranch;Sphere.rotate3];
1112   REPEAT WEAK_STRIP_TAC;
1113   REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
1114   REWRITE_TAC[Sphere.delta_x];
1115   BY(REAL_ARITH_TAC)
1116   ]);;
1117   (* }}} *)
1118
1119 let functional_ldih5_x_135_n = prove_by_refinement(
1120   `ldih5_x_135_n = mk_135 (rotate5 ldih_x_n)`,
1121   (* {{{ proof *)
1122   [
1123 (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]);
1124   REWRITE_TAC[Nonlinear_lemma.ldih5_x_n;Nonlinear_lemma.ldih_x_n;Sphere.ldih5_x_div_sqrtdelta_posbranch;Sphere.rotate5];
1125   REPEAT WEAK_STRIP_TAC;
1126   REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
1127   REWRITE_TAC[Sphere.delta_x];
1128   BY(REAL_ARITH_TAC)
1129   ]);;
1130   (* }}} *)
1131
1132 let functional_taum_x1 = prove_by_refinement(
1133   `!a b.
1134     domain6
1135     (\x1 x2 x3 x4 x5 x6. &0 <= a /\ &0 <= b)
1136     (taum_x1 a b)
1137     (compose6 taum_x four6 four6 four6
1138        (constant6 (a*a)) (constant6 (b*b)) proj_x1)`,
1139   (* {{{ proof *)
1140   [
1141   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];
1142   BY(SIMP_TAC[Nonlinear_lemma.sqrtxx])
1143   ]);;
1144   (* }}} *)
1145
1146 let functional_taum_x2 = prove_by_refinement(
1147   `!a b.
1148     domain6
1149     (\x1 x2 x3 x4 x5 x6. &0 <= a /\ &0 <= b)
1150     (taum_x2 a b)
1151     (compose6 taum_x four6 four6 four6
1152        (constant6 (a*a)) (constant6 (b*b)) proj_x2)`,
1153   (* {{{ proof *)
1154   [
1155   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];
1156   BY(SIMP_TAC[Nonlinear_lemma.sqrtxx])
1157   ]);;
1158   (* }}} *)
1159
1160
1161 let functional_taum_x1_x2 = prove_by_refinement(
1162   `!a.
1163     domain6
1164     (\x1 x2 x3 x4 x5 x6. &0 <= a)
1165     (taum_x1_x2 a)
1166     (compose6 taum_x four6 four6 four6
1167        (constant6 (a*a)) proj_x1 proj_x2)`,
1168   (* {{{ proof *)
1169   [
1170   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];
1171   BY(SIMP_TAC[Nonlinear_lemma.sqrtxx])
1172   ]);;
1173   (* }}} *)
1174
1175 let functional_delta_sub1_x = prove_by_refinement(
1176   `!a. delta_sub1_x a = compose6 delta_x
1177     (constant6 a) proj_x2 proj_x3 proj_x4 proj_x5 proj_x6`,
1178   (* {{{ proof *)
1179   [
1180   (REWRITE_TAC[FUN_EQ_THM; Sphere.delta_sub1_x;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6 ])
1181   ]);;
1182   (* }}} *)
1183
1184 let functional_taum_sub1_x = prove_by_refinement(
1185   `!a. taum_sub1_x a = compose6 taum_x
1186     (constant6 a) proj_x2 proj_x3 proj_x4 proj_x5 proj_x6`,
1187   (* {{{ proof *)
1188   [
1189   (REWRITE_TAC[FUN_EQ_THM; Sphere.taum_sub1_x;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6 ])
1190   ]);;
1191   (* }}} *)
1192
1193
1194
1195 let functional_taum_sub246_x = prove_by_refinement(
1196   `!a b c. taum_sub246_x a b c = compose6 taum_x
1197     proj_x1 (constant6 a) proj_x3 (constant6 b) proj_x5 (constant6 c)`,
1198   (* {{{ proof *)
1199   [
1200   (REWRITE_TAC[FUN_EQ_THM; Sphere.taum_sub246_x;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6 ])
1201   ]);;
1202   (* }}} *)
1203
1204 let functional_taum_sub345_x = prove_by_refinement(
1205   `!a b c. taum_sub345_x a b c = compose6 taum_x
1206     proj_x1 proj_x2 (constant6 a) (constant6 b) (constant6 c) proj_x6`,
1207   (* {{{ proof *)
1208   [
1209   (REWRITE_TAC[FUN_EQ_THM; Sphere.taum_sub345_x;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6 ])
1210   ]);;
1211   (* }}} *)
1212
1213
1214 (*
1215 let functional1_vol2r_x =
1216   new_definition `vol2r_x x = &2 * pi * (&2 - (x / &4)) / &3`;;
1217
1218 let functional_vol2r_x1 =
1219   new_definition `vol2r_x1 = promote1_to_6 vol2r_x`;;
1220
1221
1222 (*
1223 let functional1_vol2_x =
1224   new_definition `vol2_x x = &2 * pi * (&2 - (sqrt x) / &4) / &3`;;
1225
1226 let functional_vol2_x1 =
1227   new_definition `vol2_x1 = promote1_to_6 vol2_x`;;
1228 *)
1229
1230 let functional_gamma3f_x_v_lfun = prove_by_refinement(
1231   `
1232   let vv_term_m1 = scalar6 (unit6 - scalar6 proj_y1 (&1 / sqrt8)) (&4 * mm1) in
1233   let (vv_term_m2) =
1234     (scalar6 (uni(flat_term_x,proj_x1)) (-- &16 * mm2 /sol0)) in
1235     domain6
1236       (\x1 x2 x3 x4 x5 x6.
1237          &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x4 /\ &0 <= x5 /\ &0 <= x6)
1238     gamma3f_x_v_lfun ((dih_x - constant6 (&2 * #0.03)) *
1239     ((vol2r_x1 - vv_term_m1 ) + vv_term_m2))`,
1240   (* {{{ proof *)
1241   [
1242   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];
1243     simp[sqrt_sqrt]
1244       st/r
1245       AP_TERM_TAC
1246 sgthen `(sqrt x1 / &2) pow 2 = x1 / &4` SUBST1_TAC
1247 rt[arith `(sqrt x1 / &2) pow 2 = (sqrt x1 * sqrt x1) / &4`]
1248 asimp[sqrt_sqrt]
1249 ABBREV_TAC `a = &2 * pi * (&2 - x1/ &4) / &3`
1250 rt[arith `((a:real) - b + c = a - (b - c))`]
1251 AP_TERM_TAC
1252   ]);;
1253   (* }}} *)
1254 1;;
1255 *)
1256
1257  (*
1258 let taud_D2_num_x_y = prove_by_refinement(
1259   `!y1 y2 y3 y4 y5 y6.
1260     &0 <= y1 /\ &0 <= y2 /\ &0 <= y3 ==>
1261     taud_v4_D2_num y1 y2 y3 y4 y5 y6 = y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6`,
1262   (* {{{ proof *)
1263   [
1264     REWRITE_TAC[Nonlin_def.taud_v4_D2_num;Nonlin_def.taud_D2_num_x];
1265     F_REWRITE_TAC;
1266   REWRITE_TAC[GSYM mu_y];
1267   REWRITE_TAC[GSYM Sphere.delta_y];
1268   ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx];
1269   BY(REAL_ARITH_TAC)
1270   ]);;
1271   (* }}} *)
1272  *)
1273
1274 (* arclength_x_345 deprecated *)
1275
1276 (* this could be rewriten further with eulerA_x *)
1277
1278 (*
1279 let functional_sol_euler_x_divsqrtdelta = prove_by_refinement(
1280   `let a = uni(sqrt,proj_x1 * proj_x2 * proj_x3) +
1281      proj_y1 * (proj_x2 + proj_x3 - proj_x4) * constant6 (#0.5) +
1282      proj_y2 * (proj_x1 + proj_x3 - proj_x5) * constant6 (#0.5) +
1283      proj_y3 * (proj_x1 + proj_x2 - proj_x6) * constant6 (#0.5) in
1284     (sol_euler_x_div_sqrtdelta  =
1285         (uni(matan,(delta_x / (a * a * constant6 (&4))))) / a)`,
1286   (* {{{ proof *)
1287   [
1288     LET_TAC;
1289     FIRST_X_ASSUM MP_TAC;
1290     REWRITE_TAC[FUN_EQ_THM];
1291     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];
1292     REWRITE_TAC[REAL_ARITH `x * #0.5 = x/ &2`;REAL_ARITH `&4 * a pow 2 = a* a * &4`];
1293   REPEAT    STRIP_TAC;
1294   FIRST_X_ASSUM (ASSUME_TAC o (ISPECL [`x:real`;`x':real`; `x'':real`;`x''':real`;`x'''':real`; `x''''':real`]));
1295     ASM_REWRITE_TAC[];
1296     REWRITE_TAC[LET_DEF;LET_END_DEF];
1297   ]);;
1298   (* }}} *)
1299 *)
1300
1301 (*
1302 let functional_vol3f_x_sqrt2_lmplus = prove_by_refinement(
1303   `    (domain6
1304        (\x1 x2 x3 x4 x5 x6.
1305         (&2 * h0) pow 2 <= x1 /\ &0 <= x2 /\ &0 <=x6)
1306        vol3f_x_sqrt2_lmplus
1307        (constant6 ( &2 * mm1 / pi ) *
1308     (two6 * compose6 dih_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1309        two6 * compose6 dih2_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1310        two6 * compose6 dih6_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1311        compose6 dih3_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1312        compose6 dih4_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1313        compose6 dih5_x proj_x1 proj_x2 two6 two6 two6 proj_x6 -
1314        constant6 ( &3 * pi))
1315     - (constant6 (&8 * mm2 / pi)) *
1316      (compose6 ldih2_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1317         compose6 ldih6_x proj_x1 proj_x2 two6 two6 two6 proj_x6)))`,
1318   (* {{{ proof *)
1319   [
1320     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];
1321   BY(REWRITE_TAC[Nonlinear_lemma.vol3f_x_sqrt2_lmplus_alt])
1322   ]);;
1323   (* }}} *)
1324 *)
1325
1326
1327
1328 (*
1329 let functional_vol3f_x_lfun = prove_by_refinement(
1330   `    (domain6
1331        (\x1 x2 x3 x4 x5 x6.
1332         &0 <= x1 /\ &0 <= x2 /\ &0 <=x6)
1333        vol3f_x_lfun
1334        (constant6 ( &2 * mm1 / pi ) *
1335     (two6 * compose6 dih_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1336        two6 * compose6 dih2_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1337        two6 * compose6 dih6_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1338        compose6 dih3_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1339        compose6 dih4_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1340        compose6 dih5_x proj_x1 proj_x2 two6 two6 two6 proj_x6 -
1341        constant6 ( &3 * pi))
1342     - (constant6 (&8 * mm2 / pi)) *
1343      (compose6 ldih_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1344         compose6 ldih2_x proj_x1 proj_x2 two6 two6 two6 proj_x6 +
1345         compose6 ldih6_x proj_x1 proj_x2 two6 two6 two6 proj_x6)))
1346     `,
1347   (* {{{ proof *)
1348   [
1349     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];
1350   BY(REWRITE_TAC[Nonlinear_lemma.vol3f_x_lfun_alt])
1351   ]);;
1352   (* }}} *)
1353 *)
1354
1355
1356 (*
1357 let functional_ldih_x = prove_by_refinement(
1358   `ldih_x =
1359     (unit6 * constant6 h0 + proj_y1 * constant6 ( -- #0.5))*
1360     (unit6 / (constant6 h0 - unit6)) * dih_x`,
1361   (* {{{ proof *)
1362   [
1363      REWRITE_TAC[FUN_EQ_THM];
1364     REWRITE_TAC[add6;mul6;div6;sub6;constant6];
1365     REWRITE_TAC[proj_y1;Sphere.ldih_x;Nonlinear_lemma.unit6;Sphere.lfun];
1366     REAL_ARITH_TAC;
1367   ]);;
1368   (* }}} *)
1369 *)
1370
1371
1372 (*
1373 let functional_lfun_y1 = prove_by_refinement(
1374   `lfun_y1 = (unit6 * constant6 h0 + proj_x1 * constant6 (-- &1))*
1375   (unit6 / (constant6 h0 - unit6))`,
1376   (* {{{ proof *)
1377   [
1378     REWRITE_TAC[FUN_EQ_THM];
1379     REWRITE_TAC[add6;mul6;div6;sub6;constant6];
1380     REWRITE_TAC[Sphere.lfun_y1;Sphere.lfun;             Nonlinear_lemma.unit6;Nonlinear_lemma.proj_x1];
1381 REAL_ARITH_TAC;
1382   ]);;
1383   (* }}} *)
1384 *)
1385
1386 (*
1387 let functional_vol_x = prove_by_refinement(
1388   `vol_x = uni(sqrt,delta_x) / constant6 (&12)`,
1389   (* {{{ proof *)
1390   [
1391   BY(REWRITE_TAC[FUN_EQ_THM;uni;Sphere.vol_x;constant6;div6]);
1392   ]);;
1393   (* }}} *)
1394 *)
1395
1396 let x1cube = new_definition `x1cube = proj_x1 * proj_x1 * proj_x1`;;
1397
1398 let functional_ldih_x_n = prove_by_refinement(
1399   `ldih_x_n = uni(sqn,delta_x) * ldih_x_div_sqrtdelta_posbranch`,
1400   (* {{{ proof *)
1401   [
1402   BY(REWRITE_TAC[FUN_EQ_THM;Nonlinear_lemma.ldih_x_n;mul6;uni])
1403   ]);;
1404   (* }}} *)
1405
1406