(* ========================================================================= *)
(* FLYSPECK - BOOK FORMALIZATION                                             *)
(*                                                                           *)
(* Chapter: nonlinear inequalities                                           *)
(* Author:  Thomas Hales      *)
(* Date: 2012-05-20                                                          *)
(* ========================================================================= *)


(* May 2012 functional equational definitions of 
   inequality functions.

   This code is to be used in automated generation of C++ 
   taylorFunctions.

   scripts.hl generates ocaml Sphere2 module based on these lemmas.

   June 2012: truncate_* are all deprecated.  They can be deleted.

autogen:
   see functional_* lemmas in this file.
   see functional1_* lemmas in this file for univariate functions.

native_c:
	unit,x1,x2,x3,x4,x5,x6,
		y1,y2,y3,y4,y5,y6,
	  delta_x,delta_x4,
	  dih_x, sol_x,rad2_x,	
   	  num1,
	  norm2hh_x,

 *)

(* failwith "moodule";; *)

 module Functional_equation = struct  

  open Hales_tactic;;
  open Nonlinear_lemma;;

  let GMATCH = GMATCH_SIMP_TAC;;

let uni = new_definition `uni (f,x) x1 x2 x3 x4 x5 x6 = 
  (f:A->B) ( x x1 x2 x3 x4 x5 x6)`;;

let constant6 = new_definition `constant6 c x1 x2 x3 x4 x5 x6 = c`;;

let promote3_to_6 = new_definition
    `promote3_to_6 f x1 x2 x3 x4 x5 x6 = f x1 x2 x3`;;

let promote1_to_6 = new_definition
  `promote1_to_6 f x1 x2 x3 x4 x5 x6 = f x1`;;

let functional_proj_x1 = prove_by_refinement(
  `proj_x1 = promote1_to_6 I`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;promote1_to_6;proj_x1;I_DEF];
  ]);;
  (* }}} *)

(* these are circular, because we will define rotatek
   as a composition of proj_xm *)

let functional_proj_x2 = prove_by_refinement(
  `proj_x2 = rotate2 proj_x1`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;proj_x1;proj_x2;Sphere.rotate2];
  ]);;
  (* }}} *)

let functional_proj_x3 = prove_by_refinement(
  `proj_x3 = rotate3 proj_x1`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;proj_x1;proj_x3;Sphere.rotate3];
  ]);;
  (* }}} *)

let functional_proj_x4 = prove_by_refinement(
  `proj_x4 = rotate4 proj_x1`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;proj_x1;proj_x4;Sphere.rotate4];
  ]);;
  (* }}} *)

let functional_proj_x5 = prove_by_refinement(
  `proj_x5 = rotate5 proj_x1`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;proj_x1;proj_x5;Sphere.rotate5];
  ]);;
  (* }}} *)

let functional_proj_x6 = prove_by_refinement(
  `proj_x6 = rotate6 proj_x1`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;proj_x1;proj_x6;Sphere.rotate6];
  ]);;
  (* }}} *)

let rh0 = new_definition `rh0 = &1/(h0 - &1)`;;

let two6 = new_definition `two6 = constant6 ( &2)`;;

let zero6 = new_definition `zero6 = constant6 ( &0)`;;

let dummy6 = new_definition `dummy6 = constant6 ( &0)`;;

let four6 = new_definition `four6 = constant6 ( &4)`;;

let mk_126 = new_definition `mk_126 f =
  compose6 f proj_x1 proj_x2 two6 two6 two6 proj_x6`;;

let mk_456 = new_definition `mk_456 f =
  compose6 f two6 two6 two6 proj_x4 proj_x5 proj_x6`;;

let mk_135 = new_definition `mk_135 f = 
  compose6 f proj_x1 two6 proj_x3 two6 proj_x5 two6`;;

let add6 = new_definition `add6 f g x1 x2 x3 x4 x5 x6 = 
  f x1 x2 x3 x4 x5 x6 + g x1 x2 x3 x4 x5 x6`;;

let scalar6 = new_definition `scalar6 f r x1 x2 x3 x4 x5 x6 = 
  (f x1 x2 x3 x4 x5 x6) * (r:real)`;;

let mul6 = new_definition `mul6 f g x1 x2 x3 x4 x5 x6 = 
  f x1 x2 x3 x4 x5 x6 * g x1 x2 x3 x4 x5 x6`;;

let div6 = new_definition `div6 f g x1 x2 x3 x4 x5 x6 = 
  f x1 x2 x3 x4 x5 x6 / g x1 x2 x3 x4 x5 x6`;;

let sub6 = new_definition `sub6 f g x1 x2 x3 x4 x5 x6 = 
  f x1 x2 x3 x4 x5 x6  -  g x1 x2 x3 x4 x5 x6`;;

let proj_y1 = new_definition `proj_y1 x1 x2 x3 x4 x5 x6 = 
  sqrt(x1)`;;

let proj_y2 = new_definition `proj_y2 x1 x2 x3 x4 x5 x6 = 
  sqrt(x2)`;;

let proj_y3 = new_definition `proj_y3 x1 x2 x3 x4 x5 x6 = 
  sqrt(x3)`;;

let proj_y4 = new_definition `proj_y4 x1 x2 x3 x4 x5 x6 = 
  sqrt(x4)`;;

let proj_y5 = new_definition `proj_y5 x1 x2 x3 x4 x5 x6 = 
  sqrt(x5)`;;

let proj_y6 = new_definition `proj_y6 x1 x2 x3 x4 x5 x6 = 
  sqrt(x6)`;;


let domain6 = new_definition `domain6 h f g = 
  (!x1 x2 x3 x4 x5 x6. h x1 x2 x3 x4 x5 x6 ==>
      (f x1 x2 x3 x4 x5 x6 = g x1 x2 x3 x4 x5 x6))`;;

(* should be called something different, because we project out 3 coords *)

let rotate234 = new_definition `rotate234 f = 
  compose6 f proj_x2 proj_x3 proj_x4 unit6 unit6 unit6`;;

let rotate126 = new_definition `rotate126 f = 
  compose6 f proj_x1 proj_x2 proj_x6 unit6 unit6 unit6`;;

let rotate345 = new_definition `rotate345 f = 
  compose6 f proj_x3 proj_x4 proj_x5 unit6 unit6 unit6`;;

let functional_overload() = (
  overload_interface ("+",`add6`);
  overload_interface ("-",`sub6`);
  overload_interface ("/",`div6`);
  overload_interface ("*",`mul6`));;

let _ = functional_overload();;

let proj_x1 = Nonlinear_lemma.proj_x1;;
let proj_x2 = Nonlinear_lemma.proj_x2;;
let proj_x3 = Nonlinear_lemma.proj_x3;;
let proj_x4 = Nonlinear_lemma.proj_x4;;
let proj_x5 = Nonlinear_lemma.proj_x5;;
let proj_x6 = Nonlinear_lemma.proj_x6;;
let unit6 = Nonlinear_lemma.unit6;;
let compose6 = Nonlinear_lemma.compose6;;

let h0cut = new_definition `h0cut y = if (y <= &2 * h0) then &1 else &0`;;

let functional_proj_y1 = prove_by_refinement(
  `proj_y1 = promote1_to_6 sqrt`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;promote1_to_6;proj_y1];
  ]);;
  (* }}} *)

let functional_proj_y2 = prove_by_refinement(
  `proj_y2 = rotate2 proj_y1`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;proj_y1;proj_y2;Sphere.rotate2];
  ]);;
  (* }}} *)

let functional_proj_y3 = prove_by_refinement(
  `proj_y3 = rotate3 proj_y1`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;proj_y1;proj_y3;Sphere.rotate3];
  ]);;
  (* }}} *)

let functional_proj_y4 = prove_by_refinement(
  `proj_y4 = rotate4 proj_y1`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;proj_y1;proj_y4;Sphere.rotate4];
  ]);;
  (* }}} *)

let functional_proj_y5 = prove_by_refinement(
  `proj_y5 = rotate5 proj_y1`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;proj_y1;proj_y5;Sphere.rotate5];
  ]);;
  (* }}} *)

let functional_proj_y6 = prove_by_refinement(
  `proj_y6 = rotate6 proj_y1`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;proj_y1;proj_y6;Sphere.rotate6];
  ]);;
  (* }}} *)

let sqrt_sqrt = prove_by_refinement(
  `!x. &0 <= x ==> (sqrt x * sqrt x = x)`,
  (* {{{ proof *)
  [
  MESON_TAC[arith `&0 pow 2 = &0`;(SPEC `&0` Nonlinear_lemma.sq_pow2)];
  ]);;
  (* }}} *)

let functional_norm2hh_x = prove_by_refinement(
  `norm2hh_x = uni(pow2,(proj_y1 - constant6 (hminus + hplus))) +
    uni(pow2, proj_y2 - two6) + uni(pow2,proj_y3 - two6) +
    uni(pow2, proj_y4 - two6) + uni(pow2,proj_y5 - two6) +
    uni(pow2, proj_y6 - two6)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM; add6; sub6; uni;proj_y1;Nonlinear_lemma.pow2; two6;Sphere.norm2hh_x;Sphere.norm2hh;proj_y1;proj_y2;proj_y3;proj_y4;proj_y5;proj_y6;constant6];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let functional_eta2_126 = prove_by_refinement(
  `domain6
    (\x1 x2 x3 x4 x5 x6.
       (&0 <= x1 /\ &0 <= x2 /\ &0 <= x6))
    eta2_126  (uni(pow2,rotate126 (promote3_to_6 eta_x)))`,
  (* {{{ proof *)
  [
 REWRITE_TAC[domain6;Sphere.eta2_126;Sphere.eta_y; uni; rotate126;compose6;promote3_to_6;proj_x1;proj_x2;proj_x6;unit6;LET_END_DEF;LET_DEF;Nonlinear_lemma.pow2];
  BY(ASM_SIMP_TAC[sqrt_sqrt])
  ]);;
  (* }}} *)


let functional_rotate2 = prove_by_refinement(
  `!f. rotate2 f = compose6 f proj_x2 proj_x3 proj_x1 proj_x5 proj_x6 proj_x4`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[Sphere.rotate2;FUN_EQ_THM;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6]);
  ]);;
  (* }}} *)

let functional_rotate3 = prove_by_refinement(
  `!f. rotate3 f = compose6 f proj_x3 proj_x1 proj_x2 proj_x6 proj_x4 proj_x5`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[Sphere.rotate3;FUN_EQ_THM;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6]);
  ]);;
  (* }}} *)

let functional_rotate4 = prove_by_refinement(
  `!f. rotate4 f = compose6 f proj_x4 proj_x2 proj_x6 proj_x1 proj_x5 proj_x3`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[Sphere.rotate4;FUN_EQ_THM;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6]);
  ]);;
  (* }}} *)

let functional_rotate5 = prove_by_refinement(
  `!f. rotate5 f = compose6 f proj_x5 proj_x3 proj_x4 proj_x2 proj_x6 proj_x1`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[Sphere.rotate5;FUN_EQ_THM;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6]);
  ]);;
  (* }}} *)

let functional_rotate6 = prove_by_refinement(
  `!f. rotate6 f = compose6 f proj_x6 proj_x1 proj_x5 proj_x3 proj_x4 proj_x2`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[Sphere.rotate6;FUN_EQ_THM;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6]);
  ]);;
  (* }}} *)

let functional_x1_delta_x = prove_by_refinement(
  `x1_delta_x = proj_x1 * delta_x`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM];
   BY(REWRITE_TAC[proj_x1;Sphere.x1_delta_x;mul6])
  ]);;
  (* }}} *)

let functional_delta4_squared_x = prove_by_refinement(
  `delta4_squared_x = uni(pow2,delta_x4)`,
  (* {{{ proof *)
  [
BY(REWRITE_TAC[FUN_EQ_THM;uni;Nonlinear_lemma.pow2;Sphere.delta4_squared_x])
  ]);;
  (* }}} *)

let functional_vol_x = prove_by_refinement(
  `vol_x = scalar6 (uni(sqrt,delta_x)) (&1 / &12)`,
  (* {{{ proof *)
  [
  (REWRITE_TAC[FUN_EQ_THM;uni;Sphere.vol_x;scalar6]);
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let functional_dih2_x = prove_by_refinement(
  `dih2_x = rotate2 dih_x`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM];
  REWRITE_TAC[Sphere.dih2_x;Sphere.rotate2];
  BY(MESON_TAC[Nonlinear_lemma.dih_x_sym])
  ]);;
  (* }}} *)

let functional_dih3_x = prove_by_refinement(
  `dih3_x = rotate3 dih_x`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM];
  REWRITE_TAC[Sphere.dih3_x;Sphere.rotate3];
  ]);;
  (* }}} *)

let functional_dih4_x = prove_by_refinement(
  `domain6 (\x1 x2 x3 x4 x5 x6.
   &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\
       &0 <= x4 /\ &0 <= x5 /\ &0 <= x6)
	      dih4_x  (rotate4 dih_x)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[domain6];
    REWRITE_TAC[Sphere.dih4_x; Sphere.rotate4;Sphere.dih4_y; Sphere.dih_y; LET_DEF;LET_END_DEF];
  REPEAT WEAK_STRIP_TAC;
  REPEAT( GMATCH_SIMP_TAC (ISPEC `&0` Nonlinear_lemma.sq_pow2));
  BY(ASM_REWRITE_TAC[REAL_ARITH `&0 pow 2 = &0`])
  ]);;
  (* }}} *)

let functional_dih5_x = prove_by_refinement(
  `domain6 (\x1 x2 x3 x4 x5 x6.
   &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\
       &0 <= x4 /\ &0 <= x5 /\ &0 <= x6)
	      dih5_x  (rotate5 dih_x)`,
  (* {{{ proof *)
  [
    REWRITE_TAC[domain6];
    REWRITE_TAC[Sphere.dih5_x; Sphere.rotate5;Sphere.dih5_y; Sphere.dih_y; LET_DEF;LET_END_DEF];
    REPEAT WEAK_STRIP_TAC;
    REPEAT( GMATCH_SIMP_TAC (ISPEC `&0` Nonlinear_lemma.sq_pow2));
    (ASM_REWRITE_TAC[REAL_ARITH `&0 pow 2 = &0`]);
    MESON_TAC[Nonlinear_lemma.dih_x_sym;Nonlinear_lemma.dih_x_sym2];
  ]);;
  (* }}} *)

let functional_dih6_x = prove_by_refinement(
  `domain6 (\x1 x2 x3 x4 x5 x6.
   &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\
       &0 <= x4 /\ &0 <= x5 /\ &0 <= x6)
	      dih6_x  (rotate6 dih_x)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[domain6];
    REWRITE_TAC[Sphere.dih6_x; Sphere.rotate6;Sphere.dih6_y;Sphere.dih_y; LET_DEF;LET_END_DEF];
  REPEAT WEAK_STRIP_TAC;
  REPEAT( GMATCH_SIMP_TAC (ISPEC `&0` Nonlinear_lemma.sq_pow2));
  (ASM_REWRITE_TAC[REAL_ARITH `&0 pow 2 = &0`]);
  ]);;
  (* }}} *)

(*

let dih6_x' = new_definition `dih6_x' = rotate6 dih_x`;;

let ldih6_x' = new_definition `!x1 x2 x3 x4 x5 x6.
            ldih6_x' x1 x2 x3 x4 x5 x6 =
            lfun (sqrt x6 / &2) * dih6_x' x1 x2 x3 x4 x5 x6`;;

let gchi6_x' = new_definition `!x1 x2 x3 x4 x5 x6.
            gchi6_x x1 x2 x3 x4 x5 x6 =
            gchi (sqrt x6) * dih6_x' x1 x2 x3 x4 x5 x6`;;

*)

let functional_lfun_y1 = prove_by_refinement(
  `lfun_y1 = scalar6 (scalar6 unit6 h0 - proj_x1) rh0`,
  (* {{{ proof *)
  [
    REWRITE_TAC[FUN_EQ_THM];
    REWRITE_TAC[add6;scalar6;mul6;div6;sub6;constant6;rh0];
    REWRITE_TAC[Sphere.lfun_y1;Sphere.lfun;		Nonlinear_lemma.unit6;Nonlinear_lemma.proj_x1];
REAL_ARITH_TAC;
  ]);;
  (* }}} *)

let functional_ldih_x = prove_by_refinement(
  `ldih_x = 
    (scalar6 (scalar6 unit6 h0 - scalar6 proj_y1 (#0.5)) rh0) * dih_x`,
  (* {{{ proof *)
  [
     REWRITE_TAC[FUN_EQ_THM];
    REWRITE_TAC[add6;mul6;div6;sub6;constant6;rh0;scalar6];
    REWRITE_TAC[proj_y1;Sphere.ldih_x;Nonlinear_lemma.unit6;Sphere.lfun];
    REAL_ARITH_TAC;
  ]);;
  (* }}} *)

let functional_ldih2_x = prove_by_refinement(
  `ldih2_x = rotate2 ldih_x`,
  (* {{{ proof *)
  [
    REWRITE_TAC[FUN_EQ_THM];
  REWRITE_TAC[Sphere.rotate2;Sphere.ldih2_x;Sphere.ldih_x;Sphere.dih2_x];
  MESON_TAC[Nonlinear_lemma.dih_x_sym];
  ]);;
  (* }}} *)

let functional_ldih3_x = prove_by_refinement(
  `ldih3_x = rotate3 ldih_x`,
  (* {{{ proof *)
  [
    REWRITE_TAC[FUN_EQ_THM];
  REWRITE_TAC[Sphere.rotate3;Sphere.ldih3_x;Sphere.ldih_x;Sphere.dih3_x];
  ]);;
  (* }}} *)

let functional_ldih6_x = prove_by_refinement(
  `domain6 
    (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\
       &0 <= x4 /\ &0 <= x5 /\ &0 <= x6)
    ldih6_x 
    (rotate6 ldih_x)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[domain6 ];
  REWRITE_TAC[Sphere.rotate6;Sphere.ldih6_x;Sphere.ldih_x;Sphere.dih6_x;Sphere.dih6_y; Sphere.dih_y;LET_DEF;LET_END_DEF];
  BY(ASM_SIMP_TAC[sqrt_sqrt])
  ]);;
  (* }}} *)

let functional_eulerA_x = prove_by_refinement(
  `eulerA_x = proj_y1 * proj_y2 * proj_y3 +
     scalar6 (proj_y1 * (proj_x2 + proj_x3 - proj_x4)) (#0.5) +
     scalar6 (proj_y2 * (proj_x1 + proj_x3 - proj_x5)) (#0.5) +
     scalar6 (proj_y3 * (proj_x1 + proj_x2 - proj_x6)) (#0.5)
    `,
  (* {{{ proof *)
  [
    REWRITE_TAC[FUN_EQ_THM;mul6;add6; sub6;proj_y1;proj_y2;proj_y3;scalar6; constant6;proj_x1;proj_x2; proj_x3;proj_x4; proj_x5;proj_x6;Sphere.eulerA_x];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let functional_gchi1_x = prove_by_refinement(
  `gchi1_x = uni (gchi,proj_y1) * dih_x`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi1_x;uni;proj_y1;mul6]);
  ]);;
  (* }}} *)

let functional_gchi2_x = prove_by_refinement(
  `gchi2_x = uni (gchi,proj_y2) * dih2_x`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi2_x;uni;proj_y2;mul6]);
  ]);;
  (* }}} *)

let functional_gchi3_x = prove_by_refinement(
  `gchi3_x = uni (gchi,proj_y3) * dih3_x`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi3_x;uni;proj_y3;mul6]);
  ]);;
  (* }}} *)

let functional_gchi4_x = prove_by_refinement(
  `gchi4_x = uni (gchi,proj_y4) * dih4_x`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi4_x;uni;proj_y4;mul6]);
  ]);;
  (* }}} *)

let functional_gchi5_x = prove_by_refinement(
  `gchi5_x = uni (gchi,proj_y5) * dih5_x`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi5_x;uni;proj_y5;mul6]);
  ]);;
  (* }}} *)

let functional_gchi6_x = prove_by_refinement(
  `gchi6_x = uni (gchi,proj_y6) * dih6_x`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[FUN_EQ_THM;Sphere.gchi6_x;uni;proj_y6;mul6]);
  ]);;
  (* }}} *)

let functional_eta2_135 = prove_by_refinement(
  `eta2_135 = rotate3 eta2_126`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;Sphere.rotate3;Sphere.eta2_135;Sphere.eta2_126];
  BY(MESON_TAC[Collect_geom.ETA_Y_SYYM])
  ]);;
  (* }}} *)

let functional_eta2_456 = prove_by_refinement(
  `eta2_456 = rotate4 eta2_135`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;Sphere.rotate4;Sphere.eta2_456;Sphere.eta2_135;Sphere.rotate3;Sphere.eta2_126];
  BY(MESON_TAC[Collect_geom.ETA_Y_SYYM])
  ]);;
  (* }}} *)

let functional_vol3_x_sqrt = prove_by_refinement(
  `domain6
    (\x1 x2 x3 x4 x5 x6.
       &0 <= x1 /\ &0 <= x2 /\ &0 <=x6)
    vol3_x_sqrt 
    (mk_126 vol_x)`,
  (* {{{ proof *)
  [
BY(REWRITE_TAC[domain6;mk_126;two6;constant6;proj_x1;proj_x2;proj_x6;compose6;Nonlinear_lemma.vol3_vol_x])
  ]);;
  (* }}} *)

let functional_vol3f_x_lfun = prove_by_refinement(
  `domain6
       (\x1 x2 x3 x4 x5 x6.
	&0 <= x1 /\ &0 <= x2 /\ &0 <=x6)
       vol3f_x_lfun
       (constant6 ( &2 * mm1 / pi ) *
    (two6 * mk_126  dih_x + two6 * mk_126 dih2_x + two6 * mk_126 dih6_x +
       mk_126 dih3_x + mk_126 dih4_x + mk_126 dih5_x -
       constant6 ( &3 * pi)) 
    - (constant6 (&8 * mm2 / pi)) *
     (mk_126 ldih_x + 	mk_126 ldih2_x + mk_126 ldih6_x ))
    `,
  (* {{{ proof *)
  [
    REWRITE_TAC[LET_DEF;LET_END_DEF;mk_126; 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_vol3f_x_sqrt2_lmplus = prove_by_refinement(
  `    (domain6
       (\x1 x2 x3 x4 x5 x6.
	(&2 * h0) pow 2 <= x1 /\ &0 <= x2 /\ &0 <=x6)
       vol3f_x_sqrt2_lmplus
       (constant6 ( &2 * mm1 / pi ) *
    (two6 * mk_126 dih_x  +
       two6 * mk_126 dih2_x +
       two6 * mk_126 dih6_x +
       mk_126 dih3_x +
        mk_126 dih4_x +
        mk_126 dih5_x -
       constant6 ( &3 * pi)) 
    - (constant6 (&8 * mm2 / pi)) *
     (mk_126 ldih2_x + 
	mk_126 ldih6_x)))`,
  (* {{{ proof *)
  [
    REWRITE_TAC[LET_DEF;LET_END_DEF;mk_126;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 cos797 = new_definition `cos797 = cos(#0.797)`;;

let functional_asn797k = prove_by_refinement(
  `asn797k = 
    proj_x1 * uni(asn,constant6 (cos797) * 
		     uni(sin, constant6(pi) / proj_x1))`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[FUN_EQ_THM;mul6;div6;uni;cos797;constant6;proj_x1;Sphere.asn797k]);
  ]);;
  (* }}} *)

let functional_asnFnhk = prove_by_refinement(
  `asnFnhk = 
    proj_x2 * uni(asn,(proj_x1 * constant6 (sqrt3 / #4.0) +
		     (uni(sqrt,unit6 - 
			     uni(pow2,(proj_x1 * constant6 (#0.5))))) *
		     constant6 (#0.5)) * uni(sin,constant6(pi)/proj_x2))`,
  (* {{{ proof *)
  [
    (REWRITE_TAC[FUN_EQ_THM;sub6;mul6; div6;Nonlinear_lemma.pow2;add6;unit6; uni;constant6;proj_x1; proj_x2;Sphere.asnFnhk]);
  BY(REWRITE_TAC[REAL_ARITH `x * #0.5 = x/ &2`])
  ]);;
  (* }}} *)

let functional_acs_sqrt_x1_d4 = prove_by_refinement(
  `acs_sqrt_x1_d4 = uni(acs,scalar6 proj_y1 (#0.25))`,
  (* {{{ proof *)
  [
    BY(REWRITE_TAC[FUN_EQ_THM;uni;mul6;constant6;scalar6;proj_y1; Sphere.acs_sqrt_x1_d4;arith `x * #0.25 = x/ &4`])
  ]);;
  (* }}} *)

let functional_acs_sqrt_x2_d4 = prove_by_refinement(
  `acs_sqrt_x2_d4 = uni(acs,scalar6 proj_y2 (#0.25))`,
  (* {{{ proof *)
  [
    BY(REWRITE_TAC[FUN_EQ_THM;uni;mul6;constant6;scalar6;proj_y2; Sphere.acs_sqrt_x2_d4;arith `x * #0.25 = x/ &4`])
  ]);;
  (* }}} *)

(* ldih5_x ldih6_x not in HOL Light*)

let functional_arclength_x_123 = prove_by_refinement(
  `let al_num = proj_x1 + proj_x2 - proj_x3  in
  let al_den = uni(sqrt,scalar6 (proj_x1 * proj_x2) ( &4)) in
  let domain = 
    (\x1 x2 x3 x4 x5 x6. (&0 < x1 /\ &0 < x2 /\ &0 <= x3) /\
     (sqrt  x3 <= sqrt x1 + sqrt x2 /\ sqrt x1 <= sqrt x2 + sqrt x3 /\ 
      sqrt x2 <= sqrt x3 + sqrt x1)) in
    domain6 domain (arclength_x_123)  ( uni(acs, al_num / al_den ) )`,
  (* {{{ proof *)
  [
    REWRITE_TAC[LET_DEF;LET_END_DEF;];
     REWRITE_TAC[domain6];
    REWRITE_TAC[add6;mul6;div6;sub6;scalar6;constant6;uni];
    REWRITE_TAC[proj_x1;proj_x2;proj_x3;Sphere.arclength_x_123;];
    REPEAT STRIP_TAC;
    GMATCH_SIMP_TAC Trigonometry1.ACS_ARCLENGTH;
   ASM_REWRITE_TAC[];
   ASM_SIMP_TAC[SQRT_POS_LT;SQRT_POS_LE];
   AP_TERM_TAC;
   REPEAT(   GMATCH_SIMP_TAC (ISPEC `&0` Nonlinear_lemma.sq_pow2));
   ASM_SIMP_TAC[REAL_ARITH `&0 pow 2 = &0`;REAL_ARITH `&0 < x ==> &0 <= x`;REAL_ARITH `u + x * -- &1 = u - x`];
   AP_TERM_TAC;
   MATCH_MP_TAC EQ_SYM;
   REWRITE_TAC[REAL_ARITH `(x1 * x2)* &4 = x1 * (x2 * (&2 pow 2))`];
   REPEAT (GMATCH SQRT_MUL);
   GMATCH Euler_complement.SQRT_OF_POW_2_LE;
   REPEAT (GMATCH Real_ext.REAL_PROP_NN_MUL2);
   ASM_SIMP_TAC[REAL_ARITH `&0 <= &2 pow 2 /\ &0 <= &2`;REAL_ARITH `&0 < x ==> &0 <= x`];
   REAL_ARITH_TAC;
  ]);;
  (* }}} *)

let functional_arclength_234 = prove_by_refinement(
  `arclength_x_234 = rotate234 arclength_x_123`,
  (* {{{ proof *)
  [
  REWRITE_TAC[rotate234;Sphere.arclength_x_123];
    REWRITE_TAC[FUN_EQ_THM];
    REWRITE_TAC[add6;mul6;div6;sub6; constant6;Nonlinear_lemma.compose6;uni;Nonlinear_lemma.arclength_x_234; Sphere.arclength_x_123;];
    REWRITE_TAC[proj_x1;proj_x2;proj_x3;proj_x4];
  ]);;
  (* }}} *)

let functional_arclength_126 = prove_by_refinement(
  `arclength_x_126 = rotate126 arclength_x_123`,
  (* {{{ proof *)
  [
  REWRITE_TAC[rotate126];
    REWRITE_TAC[FUN_EQ_THM];
    REWRITE_TAC[add6;mul6;div6;sub6; constant6;Nonlinear_lemma.compose6;uni; Nonlinear_lemma.arclength_x_126; Sphere.arclength_x_123;];
    REWRITE_TAC[proj_x1;proj_x2;proj_x3;proj_x6];
  ]);;
  (* }}} *)
 
let functional_sol_euler_x_divsqrtdelta = prove_by_refinement(
  `domain6
    (\x1 x2 x3 x4 x5 x6.
       (&0 <= x1 /\ &0 <= x2 /\ &0 <= x3))
    sol_euler_x_div_sqrtdelta
	((uni(matan,(delta_x / (scalar6 (eulerA_x * eulerA_x) (&4))))) / eulerA_x)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[domain6];
  REWRITE_TAC[uni;scalar6;Nonlin_def.sol_euler_x_div_sqrtdelta; functional_eulerA_x;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/ &2 = x * (#0.5)) /\ ((a*b)*(c:real) = a*b*c)`;REAL_ARITH `&4 * a pow 2 = a* a * &4`;LET_DEF;LET_END_DEF];
  REPEAT STRIP_TAC;
  BY(ASM_SIMP_TAC[SQRT_MUL;Real_ext.REAL_PROP_NN_MUL2])
  ]);;
  (* }}} *)


let functional_sol246_euler_x_div_sqrtdelta = prove_by_refinement(
  `sol_euler246_x_div_sqrtdelta = rotate4 sol_euler_x_div_sqrtdelta`,
  (* {{{ proof *)
  [
    REWRITE_TAC[FUN_EQ_THM];
    BY(REWRITE_TAC[Sphere.rotate4; Nonlin_def.sol_euler246_x_div_sqrtdelta])
  ]);;
  (* }}} *)

let functional_sol345_euler_x_div_sqrtdelta = prove_by_refinement(
  `sol_euler345_x_div_sqrtdelta = rotate5 sol_euler_x_div_sqrtdelta`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM];
  BY(REWRITE_TAC[Sphere.rotate5;Nonlin_def.sol_euler345_x_div_sqrtdelta])
  ]);;
  (* }}} *)

let functional_sol156_euler_x_div_sqrtdelta = prove_by_refinement(
  `sol_euler156_x_div_sqrtdelta = rotate6 sol_euler_x_div_sqrtdelta`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM];
  BY(REWRITE_TAC[Sphere.rotate6;Nonlin_def.sol_euler156_x_div_sqrtdelta])
  ]);;
  (* }}} *)

let functional_dih_x_div_sqrtdelta_posbranch = prove_by_refinement(
  `domain6 (\x1 x2 x3 x4 x5 x6. (&0 <= x1))
    dih_x_div_sqrtdelta_posbranch
    ((scalar6 proj_y1 (&2)) / (delta_x4) *
      uni(matan, (scalar6 (proj_x1 * delta_x) (&4)) / (uni(pow2,delta_x4))))`,
  (* {{{ proof *)
  [
  REWRITE_TAC[domain6];
  REWRITE_TAC[proj_y1;constant6;proj_x1;uni;scalar6;mul6;div6;Nonlin_def.dih_x_div_sqrtdelta_posbranch;];
  REWRITE_TAC[LET_DEF;LET_END_DEF;Nonlinear_lemma.pow2;arith `&4 * x * y = (x*y)* &4`];
  REPEAT WEAK_STRIP_TAC;
  ASM_SIMP_TAC[SQRT_MUL;arith `&0 <= &4`];
  (REWRITE_TAC[Collect_geom2.SQRT4_EQ2]);
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)


(* dih2_x_div_sqrtdelta_posbranch not defined in HOL-Light *)

let functional_dih3_x_div_sqrtdelta_posbranch = prove_by_refinement(
  `dih3_x_div_sqrtdelta_posbranch = rotate3 dih_x_div_sqrtdelta_posbranch`,
  (* {{{ proof *)
  [
BY(REWRITE_TAC[FUN_EQ_THM;Sphere.rotate3;Nonlin_def.dih3_x_div_sqrtdelta_posbranch]);
  ]);;
  (* }}} *)

let functional_dih4_x_div_sqrtdelta_posbranch = 
  Nonlin_def.dih4_x_div_sqrtdelta_posbranch;;

let functional_dih5_x_div_sqrtdelta_posbranch = prove_by_refinement(
  `dih5_x_div_sqrtdelta_posbranch = rotate5 dih_x_div_sqrtdelta_posbranch`,
  (* {{{ proof *)
  [
BY(REWRITE_TAC[FUN_EQ_THM;Sphere.rotate5;Nonlin_def.dih5_x_div_sqrtdelta_posbranch]);
  ]);;
  (* }}} *)

let functional_edge_flat2_x = prove_by_refinement(
  `domain6
   (\x1 x2 x3 x4 x5 x6.
            &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\ &0 <= x5 /\ &0 <= x6)
    edge_flat2_x
    (uni(pow2,(uni(sqrt,
		   compose6(promote3_to_6 quadratic_root_plus_curry)
		     proj_x1
		 (proj_x1 * proj_x1 + 
		    (proj_x3 - proj_x5) * (proj_x2 - proj_x6) - 
		    proj_x1 * (proj_x2 + proj_x3 + proj_x5 + proj_x6))
(                 proj_x1 * proj_x3 * proj_x5 +
                 proj_x1 * proj_x2 * proj_x6 -
                 proj_x3 * (proj_x1 + proj_x2 - proj_x3 + proj_x5 - proj_x6) *
		 proj_x6 -
                 proj_x2 * proj_x5 * (proj_x1 - proj_x2 + proj_x3 - 
					proj_x5 + proj_x6))
		     zero6 zero6 zero6))))
    `,
  (* {{{ proof *)
  [
    BY(REWRITE_TAC[domain6; Nonlinear_lemma.edge_flat2_x_rewrite; compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6; zero6;constant6;add6;mul6; sub6;uni;promote3_to_6; Nonlinear_lemma.quadratic_root_plus_curry; Nonlinear_lemma.pow2])
  ]);;
  (* }}} *)

let functional_ldih_x_div_sqrtdelta_posbranch = prove_by_refinement(
  `ldih_x_div_sqrtdelta_posbranch = 
    (scalar6 (constant6 h0 - scalar6 proj_y1 ( #0.5))  rh0)
    * dih_x_div_sqrtdelta_posbranch`,
  (* {{{ proof *)
[
  REWRITE_TAC[FUN_EQ_THM;mul6;scalar6;rh0;Nonlin_def.ldih_x_div_sqrtdelta_posbranch;Sphere.lfun;constant6;mul6;sub6;proj_y1;];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let functional_ldih2_x_div_sqrtdelta_posbranch = 
  Nonlin_def.ldih2_x_div_sqrtdelta_posbranch;;

let functional_ldih3_x_div_sqrtdelta_posbranch = 
  Nonlin_def.ldih3_x_div_sqrtdelta_posbranch;;


let functional_ldih5_x_div_sqrtdelta_posbranch = 
  Nonlin_def.ldih5_x_div_sqrtdelta_posbranch;;

let functional_ldih6_x_div_sqrtdelta_posbranch = 
  Nonlin_def.ldih6_x_div_sqrtdelta_posbranch;;


let functional1_rho = prove_by_refinement(
  `!y. rho y = y * (const1 * rh0 * (#0.5)) + (&1 - const1 * rh0)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlinear_lemma.rho_alt;Sphere.h0;rh0];
  REPEAT WEAK_STRIP_TAC;
  BY(CONV_TAC REAL_RING)
  ]);;
  (* }}} *)

let functional1_flat_term_x = prove_by_refinement(
  `!y. flat_term_x y = (sqrt y - &2 * h0) * rh0 * sol0 * (#0.5)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.flat_term_x;Sphere.flat_term;Sphere.h0;rh0];
  REPEAT WEAK_STRIP_TAC;
  BY(BY(CONV_TAC REAL_RING))
  ]);;
  (* }}} *)

let functional1_lfun = prove_by_refinement(
  `!y. lfun y = ( h0 - y)*rh0`,
  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.lfun;rh0];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)


let functional_rhazim_x = prove_by_refinement(
  `domain6
    (\x1 x2 x3 x4 x5 x6. &0 <= x1 /\ &0 <= x2 /\ &0 <= x3 /\
       &0 <= x4 /\ &0 <= x5 /\ &0 <= x6)
    rhazim_x  
    (uni (rho,proj_y1) * dih_x)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[domain6];
  REWRITE_TAC[Sphere.rhazim_x;Sphere.rhazim;uni;proj_y1;mul6;Sphere.dih_y;LET_DEF;LET_END_DEF];
  REPEAT WEAK_STRIP_TAC;
  AP_TERM_TAC;
  REPEAT( GMATCH_SIMP_TAC (ISPEC `&0` Nonlinear_lemma.sq_pow2));
  BY(ASM_REWRITE_TAC[REAL_ARITH `&0 pow 2 = &0`;])
  ]);;
  (* }}} *)

let functional_rhazim2_x = prove_by_refinement(
  `rhazim2_x = rotate2 rhazim_x`,
  (* {{{ proof *)
  [
 REWRITE_TAC[FUN_EQ_THM];
  BY(REWRITE_TAC[Sphere.node2_y;Sphere.rotate2;Sphere.rhazim2_x;Sphere.rhazim_x;Sphere.rhazim2])
  ]);;
  (* }}} *)

let functional_rhazim3_x = prove_by_refinement(
  `rhazim3_x = rotate3 rhazim_x`,
  (* {{{ proof *)
  [
 REWRITE_TAC[FUN_EQ_THM];
  BY(REWRITE_TAC[Sphere.node3_y;Sphere.rotate3;Sphere.rhazim3_x;Sphere.rhazim_x;Sphere.rhazim3])
  ]);;
  (* }}} *)

let functional_taum_x = prove_by_refinement(
  `taum_x = rhazim_x + rhazim2_x +
    rhazim3_x - constant6 ((&1 + const1)*pi)`,
  (* {{{ proof *)
  [
 REWRITE_TAC[FUN_EQ_THM];
  (REWRITE_TAC[Sphere.taum_x;add6;sub6;mul6;constant6;unit6]);
  ]);;
  (* }}} *)

(* extra parameter cases *)

let functional_arclength_x1 = prove_by_refinement(
  `!a b.
    domain6    (\x1 x2 x3 x4 x5 x6. &0 <= a /\ &0 <= b) 
    (arclength_x1 a b) 
    (compose6
       arclength_x_123 proj_x1 (constant6 (a*a)) (constant6 (b*b))
       dummy6 dummy6 dummy6)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[domain6;Sphere.arclength_x_123; compose6; Sphere.arclength_x1;proj_x1;constant6;dummy6; Sphere.arclength_y1];
  BY(BY(SIMP_TAC[Nonlinear_lemma.sqrtxx]))
  ]);;
  (* }}} *)

let functional_arclength_x2 = prove_by_refinement(
  `!a b.
    domain6    (\x1 x2 x3 x4 x5 x6. &0 <= a /\ &0 <= b) 
    (arclength_x2 a b) 
    (compose6
       arclength_x_123 proj_x2 (constant6 (a*a))  (constant6 (b*b))
       dummy6 dummy6 dummy6)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[domain6;Sphere.arclength_x_123; compose6; Sphere.arclength_x2;proj_x2;constant6;dummy6; Sphere.arclength_y2];
  BY(BY(SIMP_TAC[Nonlinear_lemma.sqrtxx]))
  ]);;
  (* }}} *)

let functional_delta_126_x = prove_by_refinement(
  `!a b c. delta_126_x a b c = compose6 delta_x proj_x1 proj_x2 
    (constant6 a) (constant6 b) (constant6 c) proj_x6`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[FUN_EQ_THM; Sphere.delta_126_x;constant6;compose6;proj_x1;proj_x2;proj_x6 ])
  ]);;
  (* }}} *)

let functional_delta_234_x = prove_by_refinement(
  `!a b c. delta_234_x a b c = compose6 delta_x 
    (constant6 a) proj_x2 proj_x3 proj_x4 (constant6 b) (constant6 c)`,
  (* {{{ proof *)
  [
  (REWRITE_TAC[FUN_EQ_THM; Sphere.delta_234_x;constant6;compose6;proj_x2;proj_x3;proj_x4 ])
  ]);;
  (* }}} *)

let functional_delta_135_x = prove_by_refinement(
  `!a b c. delta_135_x a b c = compose6 delta_x 
    proj_x1 (constant6 a) proj_x3 (constant6 b) proj_x5 (constant6 c)`,
  (* {{{ proof *)
  [
  (REWRITE_TAC[FUN_EQ_THM; Sphere.delta_135_x;constant6;compose6;proj_x1;proj_x3;proj_x5 ])
  ]);;
  (* }}} *)

let functional_rhazim_x_div_sqrt_delta_posbranch = prove_by_refinement(
  `rhazim_x_div_sqrtdelta_posbranch = 
    uni(rho,proj_y1) * dih_x_div_sqrtdelta_posbranch`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[FUN_EQ_THM;Nonlin_def.rhazim_x_div_sqrtdelta_posbranch;mul6;uni;proj_y1;]);
  ]);;
  (* }}} *)

let functional_rhazim2_x_div_sqrt_delta_posbranch = prove_by_refinement(
  `rhazim2_x_div_sqrtdelta_posbranch = 
    rotate2 rhazim_x_div_sqrtdelta_posbranch`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[FUN_EQ_THM;Nonlin_def.rhazim2_x_div_sqrtdelta_posbranch;mul6;uni;proj_y1;]);
  ]);;
  (* }}} *)

let functional_rhazim3_x_div_sqrt_delta_posbranch = prove_by_refinement(
  `rhazim3_x_div_sqrtdelta_posbranch = 
    rotate3 rhazim_x_div_sqrtdelta_posbranch`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[FUN_EQ_THM;Nonlin_def.rhazim3_x_div_sqrtdelta_posbranch;mul6;uni;proj_y1;]);
  ]);;
  (* }}} *)

let functional_tau_residual = prove_by_refinement(
  `tau_residual_x = rhazim_x_div_sqrtdelta_posbranch +
    rhazim2_x_div_sqrtdelta_posbranch + rhazim3_x_div_sqrtdelta_posbranch `,
  (* {{{ proof *)
  [
  (REWRITE_TAC[FUN_EQ_THM;Nonlin_def.tau_residual_x;add6]);
  ]);;
  (* }}} *)

let functional_halfbump_x1 = prove_by_refinement(
  `halfbump_x1 = promote1_to_6 halfbump_x`,
  (* {{{ proof *)
  [
  REWRITE_TAC[promote1_to_6;Nonlinear_lemma.halfbump_x1;FUN_EQ_THM];
  ]);;
  (* }}} *)

let functional_halfbump_x4 = prove_by_refinement(
  `halfbump_x4 = rotate4 halfbump_x1`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[Sphere.rotate4;Nonlinear_lemma.halfbump_x4;Nonlinear_lemma.halfbump_x1;FUN_EQ_THM])
  ]);;
  (* }}} *)

(* two repeated defs =gamma2= deprecated. *)
let gamma2_x_div_azim =  (* same as truncate_gamma2_x *)
  new_definition `gamma2_x_div_azim m x = (&8 - x)* sqrt x / (&24) -
  ( (&2 * mm1/ pi) * (&1 - sqrt x / sqrt8) - 
      (&8 * mm2 / pi) * m * lfun (sqrt x / &2))`;;

let gamma2_x1_div_a = new_definition `gamma2_x1_div_a m = 
  promote1_to_6 (gamma2_x_div_azim m)`;;

let nonf_gamma2_x1_div_a = prove_by_refinement(
  `!(m:real) (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real).
    gamma2_x1_div_a m x1 x2 x3 x4 x5 x6 = gamma2_x_div_azim m x1`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[FUN_EQ_THM;promote1_to_6;gamma2_x1_div_a])
  ]);;
  (* }}} *)

let nonf_gamma2_x1_div_a_v2 = prove_by_refinement(
  `!(m:real) (x1:real) (x2:real) (x3:real) (x4:real) (x5:real) (x6:real).
    gamma2_x1_div_a_v2 m x1 x2 x3 x4 x5 x6 = gamma2_x_div_azim_v2 m x1`,
  (* {{{ proof *)
  [
  BY(REWRITE_TAC[FUN_EQ_THM;promote1_to_6;Nonlin_def.gamma2_x1_div_a_v2])
  ]);;
  (* }}} *)

let gamma3f_x_div_sqrtdelta = new_definition `gamma3f_x_div_sqrtdelta m4 m5 m6  = 
  constant6 (&1/ &12)  - 
    (scalar6 ( mk_456 (rotate5 (sol_euler_x_div_sqrtdelta)) +
		mk_456 (rotate6 (sol_euler_x_div_sqrtdelta)) + 
		mk_456 (rotate4 (sol_euler_x_div_sqrtdelta)) 
	       )  (&2 * mm1/ pi)    
    -       
      scalar6 (
	(scalar6 (uni(lfun,(scalar6 proj_y4  #0.5))) m4) * 
	  mk_456 (rotate4 (dih_x_div_sqrtdelta_posbranch)) +
	(scalar6 (uni(lfun,(scalar6 proj_y5  #0.5))) m5) * 
	  mk_456 (rotate5 (dih_x_div_sqrtdelta_posbranch)) +
	(scalar6 (uni(lfun,(scalar6 proj_y6  #0.5))) m6) * 
	  mk_456 (rotate6 (dih_x_div_sqrtdelta_posbranch))
      )  (&8 * mm2 / pi))`;;

let shift_scalar6 = prove_by_refinement(
  `!f g m. (scalar6 f m) * g = f * (scalar6 g m)`,
  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  REWRITE_TAC[FUN_EQ_THM];
  REWRITE_TAC[mul6;scalar6];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let gamma3f_x_div_sqrtdelta_alt = prove_by_refinement(
  `!m4 m5 m6. gamma3f_x_div_sqrtdelta m4 m5 m6  = 
  constant6 (&1/ &12)  - 
    (scalar6 ( mk_456 (rotate5 (sol_euler_x_div_sqrtdelta)) +
		mk_456 (rotate6 (sol_euler_x_div_sqrtdelta)) + 
		mk_456 (rotate4 (sol_euler_x_div_sqrtdelta)) 
	       )  (&2 * mm1/ pi)    
    -       
      scalar6 (
	( (uni(lfun,(scalar6 proj_y4  #0.5))) ) * 
	  (scalar6 (mk_456 (rotate4 (dih_x_div_sqrtdelta_posbranch))) m4) +
	( (uni(lfun,(scalar6 proj_y5  #0.5))) ) * 
	  (scalar6 ( mk_456 (rotate5 (dih_x_div_sqrtdelta_posbranch))) m5) +
	( (uni(lfun,(scalar6 proj_y6  #0.5)))) * 
	  (scalar6 (mk_456 (rotate6 (dih_x_div_sqrtdelta_posbranch))) m6)
      )  (&8 * mm2 / pi)) `,
  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  REWRITE_TAC[gamma3f_x_div_sqrtdelta];
  BY(REWRITE_TAC[shift_scalar6])
  ]);;
  (* }}} *)

let vol3f_456 = new_definition `vol3f_456 m4 = 
  scalar6 ( mk_456 (rotate5 sol_x) +
		mk_456 (rotate6 sol_x) + 
		mk_456 (rotate4 sol_x) 
	       )  (&2 * mm1/ pi)    
    -       
      scalar6 (
	(scalar6 (uni(lfun,(scalar6 proj_y4  #0.5))) m4) * 
	  mk_456 (rotate4 dih_x) +
	(uni(lfun,(scalar6 proj_y5  #0.5))) * 
	  mk_456 (rotate5 dih_x) +
	(uni(lfun,(scalar6 proj_y6  #0.5))) * 
	  mk_456 (rotate6 dih_x)
      )  (&8 * mm2 / pi)`;;

let gamma3_x = new_definition `gamma3_x m4  = 
  mk_456 vol_x  -     vol3f_456 m4`;;

let gamma23_full8_x = new_definition `gamma23_full8_x m1 =
     (compose6 (gamma3_x m1) 
       dummy6 dummy6 dummy6 proj_x1 proj_x2 proj_x6) + 
     (compose6 (gamma3_x m1) 
       dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5) +
       scalar6 (dih_x -(mk_126 dih_x + mk_135 dih_x)) (#0.008)`;;

let gamma23_keep135_x = new_definition `gamma23_keep135_x m1 =
     (compose6 (gamma3_x m1) 
       dummy6 dummy6 dummy6 proj_x1 proj_x3 proj_x5) +
       scalar6 (dih_x - mk_135 dih_x) (#0.008)`;;

let nonf_gamma3_x = prove_by_refinement(
  `!m1 x1 x2 x3 x4 x5 x6.
    gamma3_x m1 x1 x2 x3 x4 x5 x6 =  vol_x (&2) (&2) (&2) x4 x5 x6 -
     ((sol_x x5 (&2) x4 (&2) x6 (&2) +
       sol_x x6 (&2) x5 (&2) x4 (&2) +
       sol_x x4 (&2) x6 (&2) x5 (&2)) *
      &2 *
      mm1 / pi -
      ((lfun (sqrt x4 * #0.5) * m1) * dih_x x4 (&2) x6 (&2) x5 (&2) +
       lfun (sqrt x5 * #0.5) * dih_x x5 (&2) x4 (&2) x6 (&2) +
       lfun (sqrt x6 * #0.5) * dih_x x6 (&2) x5 (&2) x4 (&2)) *
      &8 *
      mm2 / pi)`,
  (* {{{ proof *)
  [
(REWRITE_TAC[gamma3_x;vol3f_456;mk_456;Sphere.rotate5;Sphere.rotate6;Sphere.rotate4;scalar6;sub6;add6;mul6;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;two6;uni;proj_y4;proj_y5;proj_y6;dummy6;mk_126;mk_135])
  ]);;
  (* }}} *)

let nonf_gamma23_full8_x = prove_by_refinement(
  `!m1 x1 x2 x3 x4 x5 x6.
    gamma23_full8_x m1 x1 x2 x3 x4 x5 x6 =  
    gamma3_x m1 (&0) (&0) (&0) x1 x2 x6 +
     gamma3_x m1 (&0) (&0) (&0) x1 x3 x5 +
     (dih_x x1 x2 x3 x4 x5 x6 -
      (dih_x x1 x2 (&2) (&2) (&2) x6 + dih_x x1 (&2) x3 (&2) x5 (&2))) *
     #0.008`,
  (* {{{ proof *)
  [
(REWRITE_TAC[gamma23_full8_x;mk_456;Sphere.rotate5;Sphere.rotate6;Sphere.rotate4;scalar6;sub6;add6;mul6;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;two6;uni;proj_y4;proj_y5;proj_y6;dummy6;mk_126;mk_135])
  ]);;
  (* }}} *)

let nonf_gamma23_keep135_x = prove_by_refinement(
  `!m1 x1 x2 x3 x4 x5 x6.
    gamma23_keep135_x m1 x1 x2 x3 x4 x5 x6 = 
  gamma3_x m1 (&0) (&0) (&0) x1 x3 x5 +
     (dih_x x1 x2 x3 x4 x5 x6 - dih_x x1 (&2) x3 (&2) x5 (&2)) * #0.008
    `,
  (* {{{ proof *)
  [
(REWRITE_TAC[gamma23_keep135_x;mk_456;Sphere.rotate5;Sphere.rotate6;Sphere.rotate4;scalar6;sub6;add6;mul6;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;two6;uni;proj_y4;proj_y5;proj_y6;dummy6;mk_126;mk_135])
  ]);;
  (* }}} *)

let nonf_gamma3f_x_div_sqrtdelta = prove_by_refinement(
  `!m4 m5 m6 x1 x2 x3 x4 x5 x6.
    gamma3f_x_div_sqrtdelta m4 m5 m6 x1 x2 x3 x4 x5 x6 = &1 / &12 -
     ((sol_euler_x_div_sqrtdelta x5 (&2) x4 (&2) x6 (&2) +
       sol_euler_x_div_sqrtdelta x6 (&2) x5 (&2) x4 (&2) +
       sol_euler_x_div_sqrtdelta x4 (&2) x6 (&2) x5 (&2)) *
      &2 *
      mm1 / pi -
      ((lfun (sqrt x4 * #0.5) * m4) *
       dih_x_div_sqrtdelta_posbranch x4 (&2) x6 (&2) x5 (&2) +
       (lfun (sqrt x5 * #0.5) * m5) *
       dih_x_div_sqrtdelta_posbranch x5 (&2) x4 (&2) x6 (&2) +
       (lfun (sqrt x6 * #0.5) * m6) *
       dih_x_div_sqrtdelta_posbranch x6 (&2) x5 (&2) x4 (&2)) *
      &8 *
      mm2 / pi)`,
  (* {{{ proof *)
  [
BY(REWRITE_TAC[gamma3f_x_div_sqrtdelta;mk_456;Sphere.rotate5;Sphere.rotate6;Sphere.rotate4;scalar6;sub6;add6;mul6;constant6;compose6;proj_x1;proj_x2;proj_x3;proj_x4;proj_x5;proj_x6;two6;uni;proj_y4;proj_y5;proj_y6])
  ]);;
  (* }}} *)


(*
extra parameter cases scratch
*)

(* added 2013-May *)

    let F_REWRITE_TAC = REWRITE_TAC[
      Nonlin_def.mud_126_x;Nonlin_def.mu6_x;Nonlin_def.mu_y;Nonlin_def.taud;Nonlin_def.taud_x;
				    Nonlin_def.ups_126;Nonlin_def.edge2_126_x;Nonlin_def.edge2_flatD_x1;
				    Nonlin_def.edge2_135_x;Nonlin_def.edge2_234_x;
				    Nonlin_def.mud_135_x;Nonlin_def.mud_126_x;Nonlin_def.mud_234_x;
				    Nonlin_def.mudLs_234_x;Nonlin_def.mudLs_126_x;Nonlin_def.mudLs_135_x;
				    LET_DEF;LET_END_DEF;
				    Sphere.delta_y;
	Sphere.y_of_x;Sphere.flat_term_x;Sphere.flat_term;
	compose6;promote3_to_6;
	promote1_to_6;	domain6;
	constant6;
	uni;
	add6;mul6;
	sub6;div6;
	proj_y1;proj_y2;
	proj_y3;proj_y4;
	proj_y5;proj_y6;
	dummy6;	zero6;
	proj_x1;proj_x2;
	proj_x4;proj_x3;
	proj_x5;	proj_x6;
];;

    let taud_x_taud = prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. 
    &0 <= y1 /\ &0 <= y2 /\ &0 <= y3 ==>
    y_of_x taud_x y1 y2 y3 y4 y5 y6 = taud y1 y2 y3 y4 y5 y6`,
  (* {{{ proof *)
  [
    F_REWRITE_TAC;
  REPEAT WEAKER_STRIP_TAC;
  BY(ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx])
  ]);;
  (* }}} *)

let mu6_x_mu_y = prove_by_refinement(
  `!y1 y2 y3 x4 x5 x6. &0 <= y1 /\ &0 <= y2 /\ &0 <= y3 ==>
    mu_y y1 y2 y3 = mu6_x (y1 * y1) ( y2 * y2) (y3 * y3) x4 x5 x6 `,
  (* {{{ proof *)
  [
  F_REWRITE_TAC;
  REPEAT WEAKER_STRIP_TAC;
  BY(ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx])
  ]);;
  (* }}} *)

let taud_x_ALT = prove_by_refinement(
  `domain6
    (\x1 x2 x3 x4 x5 x6.
       (&0 <= x1 /\ &0 <= x2 /\ &0 <= x3))
    taud_x ( (promote1_to_6 flat_term_x) +
	 (uni(sqrt,delta_x)) * mu6_x)`,
  (* {{{ proof *)
  [
    F_REWRITE_TAC;
  ]);;
  (* }}} *)

let functional_edge2_126_x = prove_by_refinement(
  `!d x4 x5. 
    (edge2_126_x d x4 x5) =
    (let a =  proj_x6 in
     let c4 = constant6 x4 in
     let c5 = constant6 x5 in
     let b = constant6(-- &1) * compose6 delta_x1 zero6 proj_x2 proj_x1 proj_x6 (c5) (c4) in
     let c = constant6 ( d) - compose6 delta_x proj_x1 proj_x2 zero6 (c4) (c5)  proj_x6  in
     let ups_456 = compose6 ups_126 (c4) (c5) dummy6 dummy6 dummy6 proj_x6 in
     let discr = ups_456 * ups_126 + constant6( -- &4*d) * a in
        (uni(sqrt,discr) - b) /  (constant6 (&2) * a))`,
  (* {{{ proof *)
  [
    REWRITE_TAC[FUN_EQ_THM];
    F_REWRITE_TAC;
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY_GOAL_THEN `!x1 x2 x3 x4 x5 x6.  d - delta_x x3 x1 x2 x6 x4 x5 = (x6) * x3 pow 2 + ( -- delta_x1 (&0) x2 x1 x6 x5 x4) * x3 + (d - delta_x (&0) x2 x1 x6 x5 x4)` (unlist ONCE_REWRITE_TAC);
    REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1];
    BY(REAL_ARITH_TAC);
  REWRITE_TAC[Nonlinear_lemma.abc_quadratic;Sphere.quadratic_root_plus];
  AP_THM_TAC;
  AP_TERM_TAC;
  MATCH_MP_TAC (arith `s1 = s2 ==> -- -- d + s1 = s2 - -- &1 * d`);
  AP_TERM_TAC;
  REWRITE_TAC[Nonlin_def.delta_x1;Sphere.ups_x;Sphere.delta_x];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let functional_edge2_135_x = prove_by_refinement(
  `!d x4 x6. 
    (edge2_135_x d x4 x6) =
    compose6 (edge2_126_x d x4 x6) (proj_x1) (proj_x3) (dummy6) (dummy6) (dummy6) (proj_x5)`,
  (* {{{ proof *)
  [
    REWRITE_TAC[FUN_EQ_THM];
    F_REWRITE_TAC;
  ]);;
  (* }}} *)

let functional_edge2_234_x = prove_by_refinement(
  `!d x5 x6.
    edge2_234_x d x5 x6 = 
    compose6 (edge2_126_x d x5 x6) (proj_x2) (proj_x3) (dummy6) (dummy6) (dummy6) (proj_x4)`,
  (* {{{ proof *)
  [
    REWRITE_TAC[FUN_EQ_THM];
    F_REWRITE_TAC;
  ]);;
  (* }}} *)

let nonfunctional_edge2_126_x = prove_by_refinement(
  `!d x1 x2 a b c x4 x5 x6. 
    (edge2_126_x d x4 x5) x1 x2 a b c x6 = 
     ((sqrt (ups_x x4 x5 x6 * ups_x x1 x2 x6 + (-- &4 * d) * x6) -
       -- &1 * delta_x1 (&0) x2 x1 x6 x5 x4) /
      (&2 * x6))`,
  (* {{{ proof *)
  [
    REWRITE_TAC[FUN_EQ_THM;functional_edge2_126_x];
        F_REWRITE_TAC;
  ]);;
  (* }}} *)

let nonfunctional_edge2_135_x = prove_by_refinement(
  `!d x1 x3 x5 x4 x6 a b c. 
    (edge2_135_x d x4 x6) x1 a x3 b x5 c = (sqrt (ups_x x4 x6 x5 * ups_x x1 x3 x5 + (-- &4 * d) * x5) -
      -- &1 * delta_x1 (&0) x3 x1 x5 x6 x4) /
     (&2 * x5)`,
  (* {{{ proof *)
  [
    REWRITE_TAC[FUN_EQ_THM;functional_edge2_126_x;functional_edge2_135_x];
        F_REWRITE_TAC;
  ]);;
  (* }}} *)

let nonfunctional_edge2_234_x = prove_by_refinement(
  `!d x2 x3 x4 x5 x6 a b c. 
    (edge2_234_x d x5 x6) a x2 x3 x4 b c = 
    (sqrt (ups_x x5 x6 x4 * ups_x x2 x3 x4 + (-- &4 * d) * x4) -
      -- &1 * delta_x1 (&0) x3 x2 x4 x6 x5) /
     (&2 * x4)`,
  (* {{{ proof *)
  [
    REWRITE_TAC[FUN_EQ_THM;functional_edge2_126_x;functional_edge2_234_x];
        F_REWRITE_TAC;
  ]);;
  (* }}} *)

let functional_mud_135_x = prove_by_refinement(
  `!y2 y4 y6. (domain6 (\ x1 x2 x3 x4 x5 x6. &0 <= y2)) 
    (mud_135_x_v1 y2 y4 y6) 
      (mul6 (compose6 (mu6_x) (constant6 (y2*y2)) proj_x1 proj_x3 dummy6 dummy6 dummy6)
	(uni(sqrt,(delta_135_x (y2*y2) (y4*y4) (y6*y6)))))`,
  (* {{{ proof *)
  [
    F_REWRITE_TAC;
  REPEAT WEAKER_STRIP_TAC;
  BY(ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx])
  ]);;
  (* }}} *)

let functional_mud_126_x = prove_by_refinement(
  `!y3 y4 y5. (domain6 (\ x1 x2 x3 x4 x5 x6. &0 <= y3)) 
    (mud_126_x_v1 y3 y4 y5) 
      (mul6 (compose6 (mu6_x) (constant6 (y3*y3)) proj_x1 proj_x2 dummy6 dummy6 dummy6)
	(uni(sqrt,(delta_126_x (y3*y3) (y4*y4) (y5*y5)))))`,
  (* {{{ proof *)
  [
    F_REWRITE_TAC;
  REPEAT WEAKER_STRIP_TAC;
  BY(ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx])
  ]);;
  (* }}} *)

let functional_mud_234_x = prove_by_refinement(
  `!y1 y5 y6. (domain6 (\ x1 x2 x3 x4 x5 x6. &0 <= y1)) 
    (mud_234_x_v1 y1 y5 y6) 
      (mul6 (compose6 (mu6_x) (constant6 (y1*y1)) proj_x2 proj_x3 dummy6 dummy6 dummy6)
	(uni(sqrt,(delta_234_x (y1*y1) (y5*y5) (y6*y6)))))`,
  (* {{{ proof *)
  [
    F_REWRITE_TAC;
  REPEAT WEAKER_STRIP_TAC;
  BY(ASM_SIMP_TAC[Nonlinear_lemma.sqrtxx])
  ]);;
  (* }}} *)

let nonfunctional_taud_D2 = prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6. taud_D2_num_x x1 x2 x3 x4 x5 x6 = -- #0.07 *
     delta_x x1 x2 x3 x4 x5 x6 *
     delta_x1 x1 x2 x3 x4 x5 x6 *
     &2 *
     sqrt x1 -
     &1 / &4 *
     mu6_x x1 x2 x3 x4 x5 x6 *
     (delta_x1 x1 x2 x3 x4 x5 x6 * &2 * sqrt x1) pow 2 +
     &1 / &2 *
     mu6_x x1 x2 x3 x4 x5 x6 *
     delta_x x1 x2 x3 x4 x5 x6 *
     (-- &8 * x1 * x4 + delta_x1 x1 x2 x3 x4 x5 x6 * &2)`,
  (* {{{ proof *)
  [
    REWRITE_TAC[Nonlin_def.taud_D2_num_x];
      F_REWRITE_TAC;
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let nonfunctional_taud_D1 = prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6. taud_D1_num_x x1 x2 x3 x4 x5 x6 = 
     -- #0.07 * delta_x x1 x2 x3 x4 x5 x6 +
     &1 / &2 *
     mu6_x x1 x2 x3 x4 x5 x6 *
     delta_x1 x1 x2 x3 x4 x5 x6 *
     &2 *
     sqrt x1 +
     sol0 /  #0.52 * sqrt (delta_x x1 x2 x3 x4 x5 x6)`,
  (* {{{ proof *)
  [
    REWRITE_TAC[Nonlin_def.taud_D1_num_x];
    F_REWRITE_TAC;
  ]);;
  (* }}} *)

let nonfunctional_mu6_x = prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6.
    mu6_x x1 x2 x3 x4 x5 x6 = 
     (#0.012 + #0.07 * (#2.52 - sqrt(x1)) + #0.01 * (#2.52 * &2 - sqrt(x2) - sqrt(x3) ))`,
  (* {{{ proof *)
  [
    F_REWRITE_TAC;
  ]);;
  (* }}} *)

let functional_delta_x1 = prove_by_refinement(
  `delta_x1 = rotate4 delta_x4`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;Sphere.rotate4;Nonlin_def.delta_x1;Sphere.delta_x4];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let functional_dnum1 = prove_by_refinement(
  `dnum1 = (constant6 (&16) - constant6 (&2) * proj_x4) * proj_x1 +
    (proj_x5 - constant6 (&8)) * proj_x2 + (proj_x6 - constant6(&8)) * proj_x3`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;Nonlin_def.dnum1];
  BY(F_REWRITE_TAC)
  ]);;
  (* }}} *)

let functional_ups_126 = prove_by_refinement(
  `ups_126=  two6 * proj_x1 * proj_x6 + two6 * proj_x2 * proj_x6 + two6 * proj_x1 * proj_x2
    - proj_x1 * proj_x1 - proj_x2 * proj_x2 - proj_x6 * proj_x6`,
  (* {{{ proof *)
  [
  REWRITE_TAC[FUN_EQ_THM;two6];
  F_REWRITE_TAC;
  REWRITE_TAC[Sphere.ups_x];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let nonf_ups_126 = prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6. ups_126 x1 x2 x3 x4 x5 x6 = ups_x x1 x2 x6`,
  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.ups_126];
  BY(F_REWRITE_TAC)
  ]);;
  (* }}} *)


let nonf_gamma3f_x_div_sqrt_delta = prove_by_refinement(
  `!p1 p2 p3 x1 x2 x3 x4 x5 x6.
    gamma3f_x_div_sqrtdelta p1 p2 p3 x1 x2 x3 x4 x5 x6 = &1 / &12 -
 ((sol_euler_x_div_sqrtdelta x5 (&2) x4 (&2) x6 (&2) +
   sol_euler_x_div_sqrtdelta x6 (&2) x5 (&2) x4 (&2) +
   sol_euler_x_div_sqrtdelta x4 (&2) x6 (&2) x5 (&2)) *
  &2 *
  mm1 / pi -
  ((lfun (sqrt x4 *  #0.5) * p1) *
   dih_x_div_sqrtdelta_posbranch x4 (&2) x6 (&2) x5 (&2) +
   (lfun (sqrt x5 *  #0.5) * p2) *
   dih_x_div_sqrtdelta_posbranch x5 (&2) x4 (&2) x6 (&2) +
   (lfun (sqrt x6 *  #0.5) * p3) *
   dih_x_div_sqrtdelta_posbranch x6 (&2) x5 (&2) x4 (&2)) *
  &8 *
  mm2 / pi)`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[Nonlin_def.gamma3f_x_div_sqrtdelta];
  F_REWRITE_TAC;
  REWRITE_TAC[Nonlin_def.scalar6];
  F_REWRITE_TAC;
  REWRITE_TAC[Nonlin_def.mk_456;Nonlin_def.scalar6];
  F_REWRITE_TAC;
  BY(REWRITE_TAC[Nonlin_def.two6;Nonlin_def.scalar6;Sphere.rotate5;Sphere.rotate6;Sphere.rotate4;Nonlin_def.constant6;Nonlin_def.proj_y4;Nonlin_def.proj_y5;Nonlin_def.proj_y6])
  ]);;
  (* }}} *)


 end;;