(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(* Section: Main Estimate - Appendix - Terminal Cases                         *)
(* Chapter: Local Fan                                                         *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2013-05-10                                                           *)
(* ========================================================================== *)

(* Terminal Pent and Hex cases.  *)

(* pent with 5 top edges=2 *)




module Pent_hex = struct


  open Hales_tactic;;

(* eventually combine this with the one in Appendix. *)

(*
let pent_hex_get_main_nonlinear = 
  let is_main = function 
    | Main_estimate -> true
    | _ -> false in
  let has_main ind = 
    exists (is_main) ind.tags in
  let main_ineq_data1 = 
    filter has_main (!Ineq.ineqs) in
  let id = map (fun t-> t.idv) main_ineq_data1 in
  let main_ineq_data = map (fun t -> hd(Ineq.getexact t)) id in
  let ineql = map (fun ind -> ind.ineq) main_ineq_data in
  let sl = map (fun ind -> ind.idv) main_ineq_data in
  let main_ineq_conj = end_itlist (curry mk_conj) ineql in
  let th = new_definition (mk_eq (`main_nonlinear_terminal_v11:bool`,main_ineq_conj)) in
  let th1 = UNDISCH (MATCH_MP (TAUT `(a <=> b) ==> (a ==> b)`) th) in
  let co1 thm = if (is_conj (concl thm)) then CONJUNCT1 thm else thm in
  let tryindex s sl = try index s sl with  _ -> report s; failwith s in
    fun s ->
      let i = tryindex s sl in
      let th2 = funpow i CONJUNCT2 th1 in
	co1 th2;;
*)


let UNDISCH2 = repeat UNDISCH;;

let yys = [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`];;


let sqrt_secant_approx = 
prove_by_refinement(
  `!x1 x2 x.  &0 <= x1 /\ x1 <= x /\ x <= x2 ==>
    (&1 / (sqrt(x1) + sqrt(x2))) * (x - x1) + sqrt(x1) <= sqrt(x)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  ASM_CASES_TAC `x2 = &0`;
    TYPIFY `x1 = &0 /\ x = &0` (C SUBGOAL_THEN ASSUME_TAC);
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    ASM_REWRITE_TAC[];
    BY(REAL_ARITH_TAC);
  TYPIFY `&0 < sqrt x2` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SQRT_POS_LT;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  TYPIFY `&0 <= sqrt x1` (C SUBGOAL_THEN ASSUME_TAC);
    MATCH_MP_TAC SQRT_POS_LE;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  TYPIFY `&1 / (sqrt x1 + sqrt x2) * (x - x1) = ((sqrt x + sqrt x1)/(sqrt x2 + sqrt x1)) * (sqrt x - sqrt x1)` (C SUBGOAL_THEN SUBST1_TAC);
    Calc_derivative.CALC_ID_TAC;
    CONJ2_TAC;
      REWRITE_TAC[REAL_DIFFSQ];
      REPEAT (GMATCH_SIMP_TAC Functional_equation.sqrt_sqrt);
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REWRITE_TAC[arith `x + y <= z <=> x <= &1 * (z - y)`];
  MATCH_MP_TAC Real_ext.REAL_PROP_LE_RMUL;
  CONJ2_TAC;
    REWRITE_TAC[arith `&0 <= x - y <=> y <= x`];
    GMATCH_SIMP_TAC SQRT_MONO_LE_EQ;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  GMATCH_SIMP_TAC REAL_LE_LDIV_EQ;
  CONJ2_TAC;
    REWRITE_TAC[arith `&1 * x = x`;arith `x + y <= z + y <=> x <= z`];
    GMATCH_SIMP_TAC SQRT_MONO_LE_EQ;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let flat_term_neg = 
prove_by_refinement(
  `!y. y <= &2 * h0 ==> flat_term y <= &0`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.flat_term];
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[arith `a * b / c <= &0 <=> &0 <= a * (--b) / c `];
  GMATCH_SIMP_TAC REAL_LE_MUL;
  GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[Sphere.h0];
  MP_TAC Flyspeck_constants.bounds;
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let mu_y_ft_combine = 
prove_by_refinement(
  `!y y2 y3 sd. 
    mu_y y y2 y3 * sd + flat_term y = 
      mu_y (&2 * h0) y2 y3 * sd + (&1 - (&2 * h0 - &2) * #0.07 * sd / sol0) * flat_term y`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.mu_y;Sphere.flat_term];
  REPEAT WEAKER_STRIP_TAC;
  Calc_derivative.CALC_ID_TAC;
  MP_TAC Flyspeck_constants.bounds;
  REWRITE_TAC[Sphere.h0];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let mu_y_ft_combine2 = 
prove_by_refinement(
  `!y y2 y3. y <= &2 * h0 ==>
    mu_y (&2 * h0) y2 y3 * sqrt(&20) + #0.705 * flat_term y <=
    mu_y y y2 y3 * sqrt(&20) + flat_term y
      `,

  (* {{{ proof *)
  [
  REWRITE_TAC[mu_y_ft_combine];
  REWRITE_TAC[arith `x + y <= x + z <=> y <= z`];
  REPEAT WEAKER_STRIP_TAC;
  ONCE_REWRITE_TAC[arith `a * b = (-- a) * (-- b)`];
  MATCH_MP_TAC Real_ext.REAL_PROP_LE_RMUL;
  CONJ2_TAC;
    REWRITE_TAC[arith `&0 <= -- f <=> f <= &0`];
    BY(ASM_SIMP_TAC[flat_term_neg]);
  REWRITE_TAC[arith `-- x <= -- (&1 - u) <=> &1 - x <= u`];
  TYPIFY `#4.472135 <= sqrt(&20)` (C SUBGOAL_THEN MP_TAC);
    MATCH_MP_TAC REAL_LE_RSQRT;
    BY(REAL_ARITH_TAC);
  TYPIFY `#0.551285 < sol0 /\ sol0 < #0.551286` (C SUBGOAL_THEN MP_TAC);
    BY(REWRITE_TAC[ Flyspeck_constants.bounds]);
  REWRITE_TAC[Sphere.h0];
  REWRITE_TAC[arith `a * b * c /d = ((a * b) * c) / d`];
  REPEAT WEAKER_STRIP_TAC;
  GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
  CONJ_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let nonfunctional_mu6_x = 
prove_by_refinement(
  `!x1 x2 x3 a b c. mu6_x x1 x2 x3 a b c = mu_y (sqrt x1) (sqrt x2) (sqrt x3)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.mu6_x;Nonlin_def.mu_y;];
  BY(Functional_equation.F_REWRITE_TAC)
  ]);;
  (* }}} *)

let tau_x_tau_residual_x_general = 
prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6.
    &4 <= x1 /\ 
    sqrt(x1) <= &2 * h0 /\
    &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\  &0 < x6 /\
    delta_x4 x1 x2 x3 x4 x5 x6 < &0 /\
    &0 < delta_x4 x2 x3 x1 x5 x6 x4  /\
    &0 < delta_x4 x3 x1 x2 x6 x4 x5  /\
    &0 <= delta_x x1 x2 x3 x4 x5 x6 ==>
    taum_x x1 x2 x3 x4 x5 x6 = sqrt(delta_x x1 x2 x3 x4 x5 x6) *
	tau_residual_x x1 x2 x3 x4 x5 x6 + flat_term_x x1`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[arith `&0 <= x <=> (&0 = x \/ &0 < x)`];
  DISCH_THEN DISJ_CASES_TAC;
    REWRITE_TAC[Sphere.taum_x;Sphere.rhazim_x;Sphere.rhazim2_x;Sphere.rhazim3_x;Sphere.rhazim;Sphere.rhazim2;Sphere.rhazim3;Sphere.node2_y;Sphere.node3_y;Sphere.dih_y;LET_DEF;LET_END_DEF;Sphere.dih_x];
    ASM_SIMP_TAC[arith `x * x = x pow 2`;SQRT_POW_2;arith `&0 < x ==> &0 <= x`];
    SUBGOAL_THEN `delta_x x2 x3 x1 x5 x6 x4 = &0` SUBST1_TAC;
      BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC);
    SUBGOAL_THEN `delta_x x3 x1 x2 x6 x4 x5 = &0` SUBST1_TAC;
      BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC);
    FIRST_X_ASSUM (fun t -> SUBST1_TAC (GSYM t));
    REWRITE_TAC[arith `x * &0 = &0`;arith `&0 * x = &0`;SQRT_0];
    ASM_SIMP_TAC[Merge_ineq.atn2_0;arith `(-- y < &0 <=> &0 < y) /\ ( &0 < -- y <=> y < &0)`];
    REWRITE_TAC[Sphere.h0;Nonlinear_lemma.rho_alt;arith `pi/ &2 + pi/ &2 = pi /\ x + -- x = &0 /\ x * &0 = &0`];
    REWRITE_TAC[Sphere.flat_term_x;Sphere.flat_term;Nonlinear_lemma.sol0_const1;Sphere.h0];
    BY(REAL_ARITH_TAC);
  REWRITE_TAC[Sphere.taum_x;Sphere.rhazim_x;Sphere.rhazim2_x;Sphere.rhazim3_x;Sphere.rhazim;Sphere.rhazim2;Sphere.rhazim3;Sphere.node2_y;Sphere.node3_y;Sphere.dih_y;LET_DEF;LET_END_DEF];
  ASM_SIMP_TAC[arith `x * x = x pow 2`;SQRT_POW_2;arith `&0 < x ==> &0 <= x`];
  REWRITE_TAC[Nonlin_def.tau_residual_x];
  REWRITE_TAC[Nonlin_def.tau_residual_x;Nonlin_def.rhazim_x_div_sqrtdelta_posbranch;Nonlin_def.rhazim2_x_div_sqrtdelta_posbranch;Nonlin_def.rhazim3_x_div_sqrtdelta_posbranch;Sphere.rotate2;Sphere.rotate3];
  ASM_REWRITE_TAC[];
  REWRITE_TAC[arith `a + b + c - d = (a - d) + b + c`];
  REWRITE_TAC[arith `a * (b + c) = a * b + a * c`];
  ONCE_REWRITE_TAC[arith `(a + b + c) +d = (a + d) + b + c`];
  BINOP_TAC;
    ASM_SIMP_TAC[Merge_ineq.dih_x_dih_x_div_sqrtdelta_negbranch];
    REWRITE_TAC[Sphere.h0;Nonlinear_lemma.rho_alt;Sphere.flat_term;Sphere.flat_term_x;Nonlinear_lemma.sol0_const1;];
    BY(REAL_ARITH_TAC);
  BINOP_TAC;
    ONCE_REWRITE_TAC[arith `a * b * c = b * (a * c)`];
    AP_TERM_TAC;
    GMATCH_SIMP_TAC Merge_ineq.dih_x_dih_x_div_sqrtdelta_posbranch;
    ASM_REWRITE_TAC[];
    SUBGOAL_THEN `delta_x x2 x3 x1 x5 x6 x4 = delta_x x1 x2 x3 x4 x5 x6` SUBST1_TAC;
      BY(REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC);
    BY(ASM_REWRITE_TAC[]);
  ONCE_REWRITE_TAC[arith `a * b * c = b * (a * c)`];
  AP_TERM_TAC;
  GMATCH_SIMP_TAC Merge_ineq.dih_x_dih_x_div_sqrtdelta_posbranch;
  ASM_REWRITE_TAC[];
  SUBGOAL_THEN `delta_x x3 x1 x2 x6 x4 x5 = delta_x x1 x2 x3 x4 x5 x6` SUBST1_TAC;
    BY(REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC);
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let OWZLKVY4 = 
prove_by_refinement(
  ` main_nonlinear_terminal_v11 ==> ( !y1 y2 y3 y4 y5 y6.
    &2 <= y1 /\ y1 <= &2 * h0 /\
    &2 <= y2 /\ y2 <= &2 * h0 /\
    &2 <= y3 /\ y3 <= &2 * h0 /\
    cstab <= y4 /\ y4 <= #3.915 /\
    y5 = &2 /\
    y6 = &2 /\
	&0 <= delta_y y1 y2 y3 y4 y5 y6 ==>
	taud y1 y2 y3 y4 y5 y6 <= taum y1 y2 y3 y4 y5 y6)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  ASM_CASES_TAC `&80 <= delta_y y1 y2 y3 y4 y5 y6`;
    INTRO_TAC ((*--*)Terminal.get_main_nonlinear "2314572187") yys;
    REWRITE_TAC[Sphere.ineq;TAUT `(a ==> b==> c) <=> (a /\ b) ==> c `;TAUT `(a /\ b) /\ c <=> a /\ b /\ c`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0;Sphere.cstab] THEN REAL_ARITH_TAC);
    ASM_SIMP_TAC[arith `n <= d ==> ~(d < n)`;arith `x > y <=> y < x`];
    MATCH_MP_TAC (arith `u = v ==> (u < t ==> v <= t)`);
    MATCH_MP_TAC Functional_equation.taud_x_taud;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  RULE_ASSUM_TAC (REWRITE_RULE[arith `~(n <= d) <=> d < n`]);
  GMATCH_SIMP_TAC Terminal.taum_taum_x;
  CONJ_TAC;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[Appendix.cstab] THEN REAL_ARITH_TAC);
  REWRITE_TAC[Sphere.y_of_x];
  GMATCH_SIMP_TAC tau_x_tau_residual_x_general;
  TYPIFY `&0 <= delta_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6)` (C SUBGOAL_THEN ASSUME_TAC);
    FIRST_X_ASSUM_ST `&0 <= d` MP_TAC;
    BY(REWRITE_TAC[Sphere.delta_y] THEN REAL_ARITH_TAC);
  COMMENT "residue hypotheses";
  CONJ_TAC;
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
    GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
    REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
    INTRO_TAC (UNDISCH Terminal.EAR_DELTA_X4) yys;
    ANTS_TAC;
      BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    ASM_REWRITE_TAC[];
    DISCH_THEN (unlist REWRITE_TAC);
    REWRITE_TAC[arith `&4 = &2 * &2`];
    REWRITE_TAC[ REAL_OF_NUM_LT];
    GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
    REWRITE_TAC[arith `0 < 2`];
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[Sphere.delta_y;Sphere.h0;Appendix.cstab] THEN REAL_ARITH_TAC);
  REWRITE_TAC[Nonlin_def.taud;Sphere.flat_term_x;Sphere.flat_term];
  GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
  CONJ_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REWRITE_TAC[arith `v + u <= w + v <=> u <= w`];
  REWRITE_TAC[GSYM Sphere.delta_y];
  GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP;
  CONJ_TAC;
    GMATCH_SIMP_TAC SQRT_POS_LE;
    BY(ASM_REWRITE_TAC[Sphere.delta_y]);
  INTRO_TAC ((*--*)Terminal.get_main_nonlinear "7796879304") yys;
  REWRITE_TAC[Sphere.ineq;Sphere.y_of_x];
  REWRITE_TAC[TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
  ANTS_TAC;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[Appendix.cstab;Sphere.h0] THEN REAL_ARITH_TAC);
  BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let OPEN_REAL_INTERVAL_SING = 
prove_by_refinement(
  `!a b c. ~(real_interval(a,b) = {c})`,

  (* {{{ proof *)
  [
  REWRITE_TAC[EXTENSION;IN_SING;IN_REAL_INTERVAL];
  REPEAT WEAKER_STRIP_TAC;
  ASM_CASES_TAC `a < b`;
    FIRST_ASSUM (C INTRO_TAC [`(a + b)/ &2`]);
    FIRST_X_ASSUM (C INTRO_TAC [`(&3 * a + &1 * b)/ &4`]);
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  FIRST_X_ASSUM_ST `!` MP_TAC;
  DISCH_THEN (C INTRO_TAC [`c:real`]);
  BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

(* DERIVATIVES *)

  let diff tm rw x s = 
    let cv rw t = rhs(concl (REWRITE_CONV rw t)) in
    let tm2 = cv rw tm in
      ( (REWRITE_RULE (map GSYM rw) (Calc_derivative.differentiate tm2 x s)));;


let DERIVED_TAC ttac = 
  fun gl -> 
    let (_,[b;f;f';y;s]) = strip_comb (goal_concl gl) in
      ttac (Calc_derivative.differentiate f y s) gl;;

let derived_form_F = 
prove_by_refinement(
  `!f f' x s. derived_form F f f' x s`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Calc_derivative.derived_form]
  ]);;
  (* }}} *)

let derived_form_delta_y = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. derived_form T (\q. delta_y q y2 y3 y4 y5 y6)
    (y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * &2 * y1) y1 (:real) `,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[Sphere.delta_y;Sphere.delta_x];
  DERIVED_TAC MP_TAC;
  MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
  REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
  REWRITE_TAC[Nonlin_def.delta_x1;Sphere.y_of_x];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

  
let derived_form_delta_x = 
prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6 .derived_form T (\q. delta_x q x2 x3 x4 x5 x6)
     (delta_x1 x1 x2 x3 x4 x5 x6)
     x1
     (:real)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  MP_TAC (diff `(\q. delta_x q x2 x3 x4 x5 x6)` [Sphere.delta_x] `x1:real` `(:real)`);
  MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
  REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
  REWRITE_TAC[Nonlin_def.delta_x1];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let derived_form_delta_x1 = 
prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6. derived_form T (\q. delta_x1 q x2 x3 x4 x5 x6)
    ( -- &2 * x4)
     x1
    (:real)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  MP_TAC (diff `(\q. delta_x1 q x2 x3 x4 x5 x6)` [Nonlin_def.delta_x1] `x1:real` `(:real)`);
  MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
  REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
  REWRITE_TAC[Nonlin_def.delta_x1];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let deriv_form_taud = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. derived_form (&0 < delta_y y1 y2 y3 y4 y5 y6)
    (\q. taud q y2 y3 y4 y5 y6) 
    ((-- #0.07 * delta_y y1 y2 y3 y4 y5 y6 + mu_y y1 y2 y3 * y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * y1 +
	 (sol0 / (&2 * h0 - &2)) * sqrt(delta_y y1 y2 y3 y4 y5 y6))/ sqrt(delta_y y1 y2 y3 y4 y5 y6))
    y1
    (:real)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[Nonlin_def.taud;Nonlin_def.mu_y];
  DERIVED_TAC (MP_TAC o GEN_ALL o (GENL [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`]));
  DISCH_THEN (C INTRO_TAC [`(y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * &2 * y1)`;`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`]);
  REWRITE_TAC[derived_form_delta_y];
  TYPIFY `~(&2 * h0 - &2 = &0)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  ASM_REWRITE_TAC[];
  MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
  ASM_CASES_TAC `(&0 < delta_y y1 y2 y3 y4 y5 y6)`;
    ASM_REWRITE_TAC[];
    REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
    Calc_derivative.CALC_ID_TAC;
    ASM_REWRITE_TAC[];
    REWRITE_TAC[arith `~(&2 = &0)`];
    CONJ_TAC;
      GMATCH_SIMP_TAC SQRT_EQ_0;
      BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
    TYPED_ABBREV_TAC `a = sqrt(delta_y y1 y2 y3 y4 y5 y6)`;
    TYPED_ABBREV_TAC `b = y_of_x delta_x1 y1 y2 y3 y4 y5 y6`;
    TYPIFY `delta_y y1 y2 y3 y4 y5 y6 = a*a` (C SUBGOAL_THEN SUBST1_TAC);
      EXPAND_TAC "a";
      GMATCH_SIMP_TAC (GSYM SQRT_MUL);
      GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    REWRITE_TAC[GSYM Nonlin_def.mu_y];
    TYPED_ABBREV_TAC `c = mu_y y1 y2 y3`;
    TYPED_ABBREV_TAC `d = (&2 * h0 - &2)`;
    TYPED_ABBREV_TAC `e = #0.07`;
    BY(REAL_ARITH_TAC);
  ASM_REWRITE_TAC[];
  BY(REWRITE_TAC[Calc_derivative.derived_form])
  ]);;
  (* }}} *)

(* renamed from deriv_form_taud_ALT *)

let derived_form_taud_ALT = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. derived_form ((&0 < delta_y y1 y2 y3 y4 y5 y6) /\ (&0 <= y1 /\ &0 <= y2 /\ &0 <= y3))
    (\q. taud q y2 y3 y4 y5 y6) 
    (y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6 / sqrt(delta_y y1 y2 y3 y4 y5 y6))
    y1
    (:real)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.y_of_x;Functional_equation.nonfunctional_taud_D1;LET_DEF;LET_END_DEF];
  REPEAT WEAKER_STRIP_TAC;
  ASM_CASES_TAC `&0 <= y1 /\ &0 <= y2 /\ &0 <= y3`;
    ASM_REWRITE_TAC[];
    ASM_SIMP_TAC[GSYM Functional_equation.mu6_x_mu_y];
    INTRO_TAC deriv_form_taud yys;
    ASM_CASES_TAC `(&0 < delta_y y1 y2 y3 y4 y5 y6)`;
      ASM_REWRITE_TAC[];
      MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
      REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
      Calc_derivative.CALC_ID_TAC;
      SUBCONJ_TAC;
        BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
      DISCH_TAC;
      REWRITE_TAC[GSYM Sphere.delta_y];
      REWRITE_TAC[GSYM Sphere.y_of_x];
      REWRITE_TAC[Sphere.h0];
      GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
      ASM_REWRITE_TAC[];
      BY(REAL_ARITH_TAC);
    BY(ASM_REWRITE_TAC[Calc_derivative.derived_form]);
  BY(ASM_REWRITE_TAC[Calc_derivative.derived_form])
  ]);;
  (* }}} *)

let deriv_form_taud_D2 = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. derived_form ((&0 < delta_y y1 y2 y3 y4 y5 y6) /\ (&0 < y1 /\ &0 <= y2 /\ &0 <= y3))
    (\q. (y_of_x taud_D1_num_x q y2 y3 y4 y5 y6 / sqrt(delta_y q y2 y3 y4 y5 y6)))
    (y_of_x taud_D2_num_x y1 y2 y3 y4 y5 y6 / (sqrt(delta_y y1 y2 y3 y4 y5 y6) pow 3)) y1 (:real)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.y_of_x;Functional_equation.nonfunctional_taud_D2;Functional_equation.nonfunctional_taud_D1;LET_DEF;LET_END_DEF];
  REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `(~(sqrt (delta_y y1 y2 y3 y4 y5 y6) = &0))` ((C SUBGOAL_THEN ASSUME_TAC));
    GMATCH_SIMP_TAC SQRT_EQ_0;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  MATCH_MP_TAC Arc_properties.HAS_REAL_DERIVATIVE_LOCAL;
  TYPIFY `(\q. (-- #0.07 * delta_x (q * q) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) + &1 / &2 * mu_y q y2 y3 * delta_x1 (q * q) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * &2 * q + sol0 / #0.52 * sqrt (delta_x (q * q) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6))) / sqrt (delta_y q y2 y3 y4 y5 y6))` EXISTS_TAC;
  CONJ2_TAC;
    TYPIFY `{q | &0 < q}` EXISTS_TAC;
    ASM_REWRITE_TAC[arith `!q. &0 < q <=> q > &0`;IN_ELIM_THM];
    REWRITE_TAC[REAL_OPEN_HALFSPACE_GT];
    REPEAT WEAKER_STRIP_TAC;
    REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
    RULE_ASSUM_TAC(REWRITE_RULE[arith `y > &0 <=> &0 < y`]);
    GMATCH_SIMP_TAC (GSYM Functional_equation.mu6_x_mu_y);
    GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  INTRO_TAC Calc_derivative.derived_form [`T`;`((\q. (-- #0.07 * delta_x (q * q) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) + &1 / &2 * mu_y q y2 y3 * delta_x1 (q * q) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * &2 * q + sol0 / #0.52 * sqrt (delta_x (q * q) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6))) / sqrt (delta_y q y2 y3 y4 y5 y6)))`;`((-- #0.07 * delta_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * delta_x1 (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * &2 * sqrt (y1 * y1) - &1 / &4 * mu6_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * (delta_x1 (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * &2 * sqrt (y1 * y1)) pow 2 + &1 / &2 * mu6_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * delta_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * (-- &8 * (y1 * y1) * y4 * y4 + delta_x1 (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6) * &2)) / sqrt (delta_y y1 y2 y3 y4 y5 y6) pow 3)`;`y1:real`;`(:real)`];
  REWRITE_TAC[WITHINREAL_UNIV];
  DISCH_THEN ((unlist REWRITE_TAC) o GSYM);
  DERIVED_TAC (MP_TAC o GEN_ALL o (GENL [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`]));
  ASM_REWRITE_TAC[GSYM Sphere.delta_y];
  DISCH_THEN (C INTRO_TAC [`y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * &2 * y1`;`-- &4 * (y4 pow 2) * y1`;`-- #0.07`;`y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * &2 * y1`;`y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * &2 * y1`;`y1`;`y2`;`y3`;`y4`;`y5`;`y6`]);
  REWRITE_TAC[derived_form_delta_y];
  TYPIFY_GOAL_THEN `derived_form T (\q. mu_y q y2 y3) (-- #0.07) y1 (:real)` (unlist REWRITE_TAC);
    REWRITE_TAC[Nonlin_def.mu_y];
    DERIVED_TAC MP_TAC;
    MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
    REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
    BY(REAL_ARITH_TAC);
  ASM_REWRITE_TAC[];
  TYPIFY_GOAL_THEN `derived_form T   (\q. delta_x1 (q * q) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6))  (-- &4 * (y4 pow 2) * y1)  y1  (:real)` (unlist REWRITE_TAC);
    REWRITE_TAC[Nonlin_def.delta_x1];
    DERIVED_TAC MP_TAC;
    MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
    REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
    BY(REAL_ARITH_TAC);
  MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
  REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
  REWRITE_TAC[GSYM Sphere.y_of_x];
  TYPED_ABBREV_TAC `a = sqrt(delta_y y1 y2 y3 y4 y5 y6)`;
  TYPED_ABBREV_TAC `b = y_of_x delta_x1 y1 y2 y3 y4 y5 y6`;
  GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
  ASM_SIMP_TAC[arith `&0 < y ==> &0 <= y`];
  TYPIFY `y_of_x mu6_x y1 y2 y3 y4 y5 y6 = mu_y y1 y2 y3` (C SUBGOAL_THEN SUBST1_TAC);
    REWRITE_TAC[Sphere.y_of_x];
    GMATCH_SIMP_TAC (GSYM Functional_equation.mu6_x_mu_y);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  TYPIFY `delta_y y1 y2 y3 y4 y5 y6 = a * a` (C SUBGOAL_THEN SUBST1_TAC);
    EXPAND_TAC "a";
    GMATCH_SIMP_TAC (GSYM SQRT_MUL);
    GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  Calc_derivative.CALC_ID_TAC;
  TYPIFY_GOAL_THEN `~(a = &0)` (unlist REWRITE_TAC);
    BY(ASM_REWRITE_TAC[]);
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let thD3  = 
  let th1 = (diff `((\q. (-- #0.07 *
             delta_y q y2 y3 y4 y5 y6 *
             (--(q * q) * y4 * y4 +
              (y2 * y2) * y5 * y5 - (y3 * y3) * y5 * y5 - (y2 * y2) * y6 * y6 +
              (y3 * y3) * y6 * y6 +
              (y4 * y4) *
              (--(q * q) + y2 * y2 + y3 * y3 - y4 * y4 + y5 * y5 + y6 * y6)) *
             &2 *
             sqrt (q * q) -
             &1 / &4 *
             ( #0.012 +
               #0.07 * ( #2.52 - sqrt (q * q)) +
               #0.01 * ( #2.52 * &2 - sqrt (y2 * y2) - sqrt (y3 * y3))) *
             ((--(q * q) * y4 * y4 +
               (y2 * y2) * y5 * y5 -
               (y3 * y3) * y5 * y5 -
               (y2 * y2) * y6 * y6 +
               (y3 * y3) * y6 * y6 +
               (y4 * y4) *
               (--(q * q) + y2 * y2 + y3 * y3 - y4 * y4 + y5 * y5 + y6 * y6)) *
              &2 *
              sqrt (q * q)) pow
             2 +
             &1 / &2 *
             ( #0.012 +
               #0.07 * ( #2.52 - sqrt (q * q)) +
               #0.01 * ( #2.52 * &2 - sqrt (y2 * y2) - sqrt (y3 * y3))) *
             delta_y q y2 y3 y4 y5 y6 *
             (-- &8 * (q * q) * y4 * y4 +
              (--(q * q) * y4 * y4 +
               (y2 * y2) * y5 * y5 -
               (y3 * y3) * y5 * y5 -
               (y2 * y2) * y6 * y6 +
               (y3 * y3) * y6 * y6 +
               (y4 * y4) *
               (--(q * q) + y2 * y2 + y3 * y3 - y4 * y4 + y5 * y5 + y6 * y6)) *
              &2)) /
            sqrt (delta_y q y2 y3 y4 y5 y6) pow 3)) `  [] `y1:real` `(:real)`) in
  let fr = frees  (concl(GENL [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`] th1)) in
  let th2 = GENL fr th1 in
  let ddelta_y = `(y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * &2 * y1)` in
  let th3 = SPECL [ddelta_y;ddelta_y;ddelta_y] th2 in
  let th4 = REWRITE_RULE[derived_form_delta_y]  th3 in
  let (h,[b;f;f';y;s]) = strip_comb (concl th4) in
  let tm = list_mk_comb (h,[b;f;`f':real`;y;s]) in
    GENL [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`] ( EXISTS (mk_exists (`f':real`,tm),f') th4);;

let derived_form_taud_D3 = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. ?f'. derived_form ((&0 < delta_y y1 y2 y3 y4 y5 y6) /\ (&0 < y1 /\ &0 <= y2 /\ &0 <= y3))
    (\q. (y_of_x taud_D2_num_x q y2 y3 y4 y5 y6 / (sqrt(delta_y q y2 y3 y4 y5 y6) pow 3)))
     f' y1 (:real)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.y_of_x;Functional_equation.nonfunctional_taud_D2;Nonlin_def.delta_x1;GSYM Sphere.delta_y;nonfunctional_mu6_x;Nonlin_def.mu_y;Functional_equation.nonfunctional_taud_D1;LET_DEF;LET_END_DEF];
  REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV];
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC thD3 yys;
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `f'` EXISTS_TAC;
  FIRST_X_ASSUM MP_TAC;
  REWRITE_TAC[Calc_derivative.derived_form];
  ANTS_TAC;
    TYPIFY_GOAL_THEN `&0 < y1 * y1` (unlist REWRITE_TAC);
      GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
      BY(ASM_REWRITE_TAC[]);
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC SQRT_EQ_0;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  BY(REWRITE_TAC[WITHINREAL_UNIV])
  ]);;
  (* }}} *)

let SECOND_DERIVATIVE_TEST = 
prove_by_refinement(
  `!f f' f'' z s.
    z IN s /\ real_open s /\
    (!x. x IN s ==> (f has_real_derivative f' x) (atreal x)) /\
    (!x. x IN s ==> (f' has_real_derivative f'' x) (atreal x)) /\
    (f'' real_continuous atreal z) /\
    (!x. x IN s ==> f z <= f x) ==>
    (f' z = &0 /\  &0 <= f'' z)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  SUBCONJ_TAC;
    INTRO_TAC REAL_DERIVATIVE_ZERO_MAXMIN [`f`;`f' z`;`z`;`s`];
    DISCH_THEN MATCH_MP_TAC;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[]);
  DISCH_TAC;
  REWRITE_TAC[arith `&0 <= r <=> ~(r < &0)`];
  DISCH_TAC;
  RULE_ASSUM_TAC(REWRITE_RULE[real_continuous_atreal]);
  FIRST_X_ASSUM_ST `abs` (C INTRO_TAC [`-- f'' z`]);
  ANTS_TAC;
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  TYPED_ABBREV_TAC  `s' = s INTER {x | abs(x - z) < d}` ;
  TYPIFY `z IN s'` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "s'";
    BY(ASM_REWRITE_TAC[IN_INTER;IN_ELIM_THM;arith `z - z = &0`;REAL_ABS_0]);
  TYPIFY `real_open s'` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "s'";
    MATCH_MP_TAC REAL_OPEN_INTER;
    ASM_REWRITE_TAC[];
    REWRITE_TAC[real_open;IN_ELIM_THM];
    REPEAT WEAKER_STRIP_TAC;
    TYPIFY `d - abs (x - z)` EXISTS_TAC;
    CONJ_TAC;
      BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
    REPEAT WEAKER_STRIP_TAC;
    BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  COMMENT "restrict to an interval";
  TYPIFY `?a b. real_interval (a,b) SUBSET s' /\ z IN real_interval(a,b)` (C SUBGOAL_THEN MP_TAC);
    RULE_ASSUM_TAC(REWRITE_RULE[real_open]);
    FIRST_X_ASSUM (C INTRO_TAC [`z`]);
    ASM_REWRITE_TAC[];
    REPEAT WEAKER_STRIP_TAC;
    GEXISTL_TAC [`z - e`;`z + e`];
    REWRITE_TAC[SUBSET;IN_REAL_INTERVAL];
    REPEAT WEAKER_STRIP_TAC;
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC REAL_OPEN_REAL_INTERVAL [`a`;`b`];
  DISCH_TAC;
  TYPIFY `!x. x IN s' ==> f'' x < &0` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`x`]);
    ANTS_TAC;
      FIRST_X_ASSUM MP_TAC;
      EXPAND_TAC "s'";
      BY(REWRITE_TAC[IN_INTER;IN_ELIM_THM] THEN REAL_ARITH_TAC);
    BY(REAL_ARITH_TAC);
  INTRO_TAC Counting_spheres.REAL_CONVEX_ON_SECOND_SECANT [`(\x. -- f x)`;`(\x. -- f' x)`;`(\x. -- f'' x)`;`real_interval (a,b)`];
  ANTS_TAC;
    REWRITE_TAC[IS_REALINTERVAL_INTERVAL;OPEN_REAL_INTERVAL_SING];
    TYPIFY `!x. x IN real_interval(a,b) ==> x IN s` (C SUBGOAL_THEN ASSUME_TAC);
      BY(ASM_TAC THEN SET_TAC[]);
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      MATCH_MP_TAC HAS_REAL_DERIVATIVE_NEG;
      GMATCH_SIMP_TAC HAS_REAL_DERIVATIVE_WITHIN_REAL_OPEN;
      BY(ASM_SIMP_TAC[REAL_OPEN_REAL_INTERVAL]);
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      MATCH_MP_TAC HAS_REAL_DERIVATIVE_NEG;
      GMATCH_SIMP_TAC HAS_REAL_DERIVATIVE_WITHIN_REAL_OPEN;
      BY(ASM_SIMP_TAC[REAL_OPEN_REAL_INTERVAL]);
    REPEAT WEAKER_STRIP_TAC;
    MATCH_MP_TAC (arith `f < &0 ==> &0 <= -- f`);
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
  DISCH_TAC;
  TYPIFY `!x. x IN real_interval(a,b) ==> f x = f z` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`x`;`z`]);
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM_ST `fz <= fx` (C INTRO_TAC [`x`]);
    ANTS_TAC;
      BY(ASM_TAC THEN SET_TAC[]);
    BY(REAL_ARITH_TAC);
  TYPIFY `!x. x IN real_interval (a,b) ==> (f has_real_derivative &0) (atreal x)` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    MATCH_MP_TAC Arc_properties.HAS_REAL_DERIVATIVE_LOCAL;
    TYPIFY `(\ (x:real). f z)` EXISTS_TAC;
    REWRITE_TAC[];
    CONJ_TAC;
      BY(REWRITE_TAC[HAS_REAL_DERIVATIVE_CONST]);
    TYPIFY `real_interval(a,b)` EXISTS_TAC;
    BY(ASM_REWRITE_TAC[REAL_OPEN_REAL_INTERVAL]);
  COMMENT "show f' is zero";
  TYPIFY `!x. x IN real_interval(a,b) ==> (f' x = &0)` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    MATCH_MP_TAC REAL_DERIVATIVE_UNIQUE_ATREAL;
    GEXISTL_TAC [`f`;`x`];
    ASM_SIMP_TAC[];
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
  COMMENT "show f' has zero derivative";
  TYPIFY `!x. x IN real_interval (a,b) ==> (f' has_real_derivative &0) (atreal x)` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    MATCH_MP_TAC Arc_properties.HAS_REAL_DERIVATIVE_LOCAL;
    TYPIFY `(\ (x:real).  &0)` EXISTS_TAC;
    REWRITE_TAC[];
    CONJ_TAC;
      BY(REWRITE_TAC[HAS_REAL_DERIVATIVE_CONST]);
    TYPIFY `real_interval(a,b)` EXISTS_TAC;
    BY(ASM_REWRITE_TAC[REAL_OPEN_REAL_INTERVAL]);
  COMMENT "show f'' is zero";
  TYPIFY `!x. x IN real_interval(a,b) ==> (f'' x = &0)` (C SUBGOAL_THEN ASSUME_TAC);
    REPEAT WEAKER_STRIP_TAC;
    MATCH_MP_TAC REAL_DERIVATIVE_UNIQUE_ATREAL;
    GEXISTL_TAC [`f'`;`x`];
    ASM_SIMP_TAC[];
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
  FIRST_X_ASSUM (C INTRO_TAC [`z`]);
  ASM_REWRITE_TAC[];
  REPLICATE_TAC 12 (FIRST_X_ASSUM kill);
  FIRST_X_ASSUM_ST `f'' z < &0` MP_TAC;
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

(* END OF DERIVATIVES *)


(* CONTINUITY *)

let continuous_preimage_closed = 
prove_by_refinement(
  `!f s t. real_closed s /\ real_closed t /\ f real_continuous_on s ==>
    real_closed { x  | x IN s /\ f x IN t }`,

  (* {{{ proof *)
  [
  REWRITE_TAC[real_continuous_on];
  REWRITE_TAC[real_closed;real_open;IN_DIFF;IN_UNIV;IN_ELIM_THM;DE_MORGAN_THM];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM DISJ_CASES_TAC;
    BY(ASM_MESON_TAC[]);
  TYPIFY `~(x IN s)` ASM_CASES_TAC;
    BY(ASM_MESON_TAC[]);
  FIRST_X_ASSUM (C INTRO_TAC [`x`]);
  RULE_ASSUM_TAC(REWRITE_RULE[TAUT `~ ~ x = x`]);
  ASM_REWRITE_TAC[];
  FIRST_X_ASSUM (C INTRO_TAC [`f x`]);
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`e`]);
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `d` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `(x' IN s)` ASM_CASES_TAC;
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM MATCH_MP_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_REWRITE_TAC[]);
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let continuous_preimage_open = 
prove_by_refinement(
  `!f s t. real_open s /\ real_open t /\ f real_continuous_on s ==>
    real_open { x  | x IN s /\ f x IN t }`,

  (* {{{ proof *)
  [
  REWRITE_TAC[real_continuous_on];
  REWRITE_TAC[real_closed;real_open;IN_DIFF;IN_UNIV;IN_ELIM_THM;DE_MORGAN_THM];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM (C INTRO_TAC [`x`]);
  ASM_REWRITE_TAC[];
  FIRST_X_ASSUM (C INTRO_TAC [`f x`]);
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `x IN s ==> p` (C INTRO_TAC [`x`]);
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `?` (C INTRO_TAC [`e`]);
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `min d e'` EXISTS_TAC;
  CONJ_TAC;
    REWRITE_TAC[real_min];
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  SUBCONJ_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[real_min] THEN REAL_ARITH_TAC);
  DISCH_TAC;
  FIRST_X_ASSUM MATCH_MP_TAC;
  FIRST_X_ASSUM MATCH_MP_TAC;
  ASM_REWRITE_TAC[];
  BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[real_min] THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let delta_y_continuous = 
prove_by_refinement(
  `!y2 y3 y4 y5 y6. (\q. delta_y q y2 y3 y4 y5 y6) real_continuous_on (:real)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
  REWRITE_TAC[REAL_OPEN_UNIV;IN_UNIV];
  GEN_TAC;
  INTRO_TAC derived_form_delta_y [`x`;`y2`;`y3`;`y4`;`y5`;`y6`];
  REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV];
  DISCH_THEN (MP_TAC o (MATCH_MP HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL));
  BY(REWRITE_TAC[])
  ]);;
  (* }}} *)

let taud_continuous = 
prove_by_refinement(
  `!y2 y3 y4 y5 y6. (\q. taud q y2 y3 y4 y5 y6) real_continuous_on {q | &0 <= delta_y q y2 y3 y4 y5 y6}`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN;IN_ELIM_THM];
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[Nonlin_def.taud];
  REWRITE_TAC[arith `!q. a * (q - b)/ r = (a * inv r) * q + a * (-- b) * inv r`];
  REWRITE_TAC[arith `!q. a + b * (c - q) + d = (-- b) * q + (a + b*c + d)`];
  REPEAT (TRY CONJ_TAC THEN REWRITE_TAC[REAL_CONTINUOUS_CONST;REAL_CONTINUOUS_WITHIN_ID] THEN ((GMATCH_SIMP_TAC REAL_CONTINUOUS_ADD) ORELSE (GMATCH_SIMP_TAC REAL_CONTINUOUS_LMUL) ORELSE (GMATCH_SIMP_TAC REAL_CONTINUOUS_MUL)));
  CONJ_TAC;
    REWRITE_TAC[MESON [o_THM;FUN_EQ_THM] `(\q. sqrt (delta_y q y2 y3 y4 y5 y6)) = sqrt o (\q. delta_y q y2 y3 y4 y5 y6)`];
    MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_COMPOSE;
    REWRITE_TAC[IMAGE;IN_ELIM_THM];
    CONJ_TAC;
      MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_SUBSET;
      TYPIFY `(:real)` EXISTS_TAC;
      REWRITE_TAC[delta_y_continuous;SUBSET;IN_UNIV];
      INTRO_TAC delta_y_continuous [`y2`;`y3`;`y4`;`y5`;`y6`];
      REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN];
      DISCH_THEN MATCH_MP_TAC;
      BY(REWRITE_TAC[IN_UNIV]);
    TYPED_ABBREV_TAC  `u = delta_y x y2 y3 y4 y5 y6` ;
    MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_SUBSET;
    TYPIFY `{u | &0 <= u}` EXISTS_TAC;
    REWRITE_TAC[REAL_CONTINUOUS_WITHIN_SQRT_STRONG];
    REWRITE_TAC[SUBSET;IN_ELIM_THM];
    BY(MESON_TAC[]);
  BY(REPEAT (TRY CONJ_TAC THEN REWRITE_TAC[REAL_CONTINUOUS_CONST;REAL_CONTINUOUS_WITHIN_ID] THEN ((GMATCH_SIMP_TAC REAL_CONTINUOUS_ADD) ORELSE (GMATCH_SIMP_TAC REAL_CONTINUOUS_LMUL) ORELSE (GMATCH_SIMP_TAC REAL_CONTINUOUS_MUL))))
  ]);;
  (* }}} *)

let taud_minimizer = 
prove_by_refinement(
  `!a b d y2 y3 y4 y5 y6.
  (let s = real_interval [a,b] INTER { q | d <= delta_y q y2 y3 y4 y5 y6} in
    (&0 <= d /\ ~(s = {}) ==>
       (?z1. z1 IN s /\ (!y1. y1 IN s ==> taud z1 y2 y3 y4 y5 y6 <= taud y1 y2 y3 y4 y5 y6))))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[LET_DEF;LET_END_DEF];
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC REAL_CONTINUOUS_ATTAINS_INF;
  ASM_REWRITE_TAC[];
  CONJ2_TAC;
    MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET;
    TYPIFY `{q | &0 <= delta_y q y2 y3 y4 y5 y6}` EXISTS_TAC;
    REWRITE_TAC[taud_continuous];
    REWRITE_TAC[SUBSET;IN_INTER;IN_ELIM_THM];
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REWRITE_TAC[REAL_COMPACT_EQ_BOUNDED_CLOSED];
  CONJ_TAC;
    MATCH_MP_TAC REAL_BOUNDED_SUBSET;
    TYPIFY `real_interval[a,b]` EXISTS_TAC;
    REWRITE_TAC[REAL_BOUNDED_REAL_INTERVAL];
    BY(SET_TAC[]);
  MATCH_MP_TAC REAL_CLOSED_INTER;
  REWRITE_TAC[REAL_CLOSED_REAL_INTERVAL];
  TYPIFY_GOAL_THEN `!q. d <= delta_y q y2 y3 y4 y5 y6 <=> q IN (:real) /\ ((\q. delta_y q y2 y3 y4 y5 y6) q IN { t | d <= t})` (unlist REWRITE_TAC);
    BY(REWRITE_TAC[IN_UNIV;IN_ELIM_THM]);
  MATCH_MP_TAC continuous_preimage_closed;
  REWRITE_TAC[delta_y_continuous];
  REWRITE_TAC[REAL_CLOSED_UNIV];
  BY(REWRITE_TAC[arith `d <= t <=> t >= d`;REAL_CLOSED_HALFSPACE_GE])
  ]);;
  (* }}} *)

let taud_minimizer_cases = 
prove_by_refinement(
  `!a b d z1 y2 y3 y4 y5 y6.
  (let s = real_interval [a,b] INTER { q | d <= delta_y q y2 y3 y4 y5 y6} in
       (&0 <= d /\ &0 <= a /\ &0 <= y2 /\ &0 <= y3 /\ z1 IN s /\
	  (!y1. y1 IN s ==> taud z1 y2 y3 y4 y5 y6 <= taud y1 y2 y3 y4 y5 y6) ==>
	  ( z1 = a \/ z1 = b \/ d = delta_y z1 y2 y3 y4 y5 y6 \/
	      (y_of_x taud_D1_num_x z1 y2 y3 y4 y5 y6 = &0 /\
		  &0 <= y_of_x taud_D2_num_x z1 y2 y3 y4 y5 y6) )))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[LET_DEF;LET_END_DEF];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `z1 = a` ASM_CASES_TAC;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `z1 = b` ASM_CASES_TAC;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `d = delta_y z1 y2 y3 y4 y5 y6` ASM_CASES_TAC;
    BY(ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  TYPIFY `a < z1 /\ z1 < b /\ d < delta_y z1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC);
    RULE_ASSUM_TAC(REWRITE_RULE[IN_REAL_INTERVAL;IN_INTER;IN_ELIM_THM]);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  TYPED_ABBREV_TAC  `s' = (real_interval (a,b) INTER {q | d < delta_y q y2 y3 y4 y5 y6})` ;
  TYPIFY `real_open s'` (C SUBGOAL_THEN ASSUME_TAC);
    TYPIFY_GOAL_THEN `s' = { q | q IN real_interval (a,b) /\ (delta_y q y2 y3 y4 y5 y6 IN { t | d < t}) }` (unlist ONCE_REWRITE_TAC);
      EXPAND_TAC "s'";
      BY(REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_INTER]);
    MATCH_MP_TAC continuous_preimage_open;
    REWRITE_TAC[REAL_OPEN_REAL_INTERVAL];
    CONJ_TAC;
      BY(REWRITE_TAC[REAL_OPEN_HALFSPACE_GT;arith `d < t <=> t > d`]);
    MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET;
    TYPIFY `(:real)` EXISTS_TAC;
    REWRITE_TAC[delta_y_continuous];
    BY(SET_TAC[]);
  INTRO_TAC SECOND_DERIVATIVE_TEST [`(\q. taud q y2 y3 y4 y5 y6)`;`(\q. y_of_x taud_D1_num_x q y2 y3 y4 y5 y6 / sqrt(delta_y q y2 y3 y4 y5 y6))`;`(\q. y_of_x taud_D2_num_x q y2 y3 y4 y5 y6 / (sqrt(delta_y q y2 y3 y4 y5 y6)) pow 3)`;`z1`;`s'`];
  ASM_REWRITE_TAC[];
  COMMENT "big ants";
  ANTS_TAC;
    SUBCONJ_TAC;
      EXPAND_TAC "s'";
      REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
      BY(ASM_REWRITE_TAC[]);
    DISCH_TAC;
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      INTRO_TAC derived_form_taud_ALT [`x`;`y2`;`y3`;`y4`;`y5`;`y6`];
      REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV];
      ANTS_TAC;
        ASM_REWRITE_TAC[];
        FIRST_X_ASSUM MP_TAC;
        EXPAND_TAC "s'";
        REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
        BY(ASM_TAC THEN REAL_ARITH_TAC);
      BY(REWRITE_TAC[]);
    CONJ_TAC;
      REPEAT WEAKER_STRIP_TAC;
      INTRO_TAC deriv_form_taud_D2 [`x`;`y2`;`y3`;`y4`;`y5`;`y6`];
      REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV];
      ANTS_TAC;
        ASM_REWRITE_TAC[];
        FIRST_X_ASSUM MP_TAC;
        EXPAND_TAC "s'";
        REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
        BY(ASM_TAC THEN REAL_ARITH_TAC);
      BY(REWRITE_TAC[]);
    CONJ2_TAC;
      EXPAND_TAC "s'";
      REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
      REPEAT WEAKER_STRIP_TAC;
      FIRST_X_ASSUM MATCH_MP_TAC;
      REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
      BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    COMMENT "last ant";
    MATCH_MP_TAC HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL;
    INTRO_TAC derived_form_taud_D3 [`z1`;`y2`;`y3`;`y4`;`y5`;`y6`];
    REPEAT WEAKER_STRIP_TAC;
    FIRST_X_ASSUM MP_TAC;
    REWRITE_TAC[Calc_derivative.derived_form];
    ANTS_TAC;
      FIRST_X_ASSUM MP_TAC;
      EXPAND_TAC "s'";
      REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    REWRITE_TAC[WITHINREAL_UNIV];
    BY(MESON_TAC[]);
  COMMENT "down to 1";
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `&0 < sqrt(delta_y z1 y2 y3 y4 y5 y6)` (C SUBGOAL_THEN ASSUME_TAC);
    GMATCH_SIMP_TAC REAL_LT_RSQRT;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  CONJ_TAC;
    FIRST_X_ASSUM_ST `taud_D1_num_x` MP_TAC;
    REWRITE_TAC[REAL_DIV_EQ_0];
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  FIRST_X_ASSUM_ST `taud_D2_num_x` MP_TAC;
  GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
  CONJ_TAC;
    MATCH_MP_TAC REAL_POW_LT;
    BY(ASM_REWRITE_TAC[]);
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let taud_minimizer_terminal_pent_cases = 
prove_by_refinement(
  ` main_nonlinear_terminal_v11 ==> (!d y1 y2 y3 y4 y5 y6.
  (let s = real_interval [&2,&2 * h0] INTER { q | d <= delta_y q y2 y3 y4 y5 y6} in
       (&0 <= d /\ y1 IN s /\ &2 <= y2 /\ y2 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 /\
	 #3.01 <= y4 /\ y4 <= #3.237 /\ y5 = &2 /\ y6 = &2 ==> 
	  (?z1. z1 IN s /\ taud z1 y2 y3 y4 y5 y6  <= taud y1 y2 y3 y4 y5 y6 /\
	  ( z1 = &2 \/ z1 = &2 * h0 \/ d = delta_y z1 y2 y3 y4 y5 y6 \/
	      #0.12 <= taud z1 y2 y3 y4 y5 y6)))))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC taud_minimizer [`&2`;`&2 * h0`;`d`;`y2`;`y3`;`y4`;`y5`;`y6`];
  REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM;EXTENSION;IN_INTER;NOT_IN_EMPTY;IN_REAL_INTERVAL;IN_ELIM_THM];
  ANTS_TAC;
    BY(ASM_MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `z1` EXISTS_TAC;
  CONJ_TAC;
    BY(ASM_MESON_TAC[]);
  CONJ_TAC;
    FIRST_X_ASSUM MATCH_MP_TAC;
    BY(ASM_MESON_TAC[]);
  INTRO_TAC taud_minimizer_cases [`&2`;`&2 * h0`;`d`;`z1`;`y2`;`y3`;`y4`;`y5`;`y6`];
  REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM;EXTENSION;IN_INTER;NOT_IN_EMPTY;IN_REAL_INTERVAL;IN_ELIM_THM];
  ANTS_TAC;
    BY(ASM_MESON_TAC[arith `&0 <= &2`;arith `&2 <= y ==> &0 <= y`]);
  ASM_CASES_TAC `z1 = &2` THEN FIRST_ASSUM (unlist REWRITE_TAC);
  ASM_CASES_TAC `z1 = &2 * h0` THEN FIRST_ASSUM (unlist REWRITE_TAC);
  ASM_CASES_TAC `d = delta_y z1 y2 y3 y4 y5 y6` THEN FIRST_ASSUM (unlist REWRITE_TAC);
  ASM_CASES_TAC `~(delta_y z1 y2 y3 y4 y5 y6 < &20)`;
    REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC ((*--*)Terminal.get_main_nonlinear "1347067436") [`z1`;`y2`;`y3`;`y4`;`y5`;`y6`];
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    GMATCH_SIMP_TAC (GSYM Functional_equation.taud_x_taud);
    CONJ_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    BY(REPLICATE_TAC 3(FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  COMMENT "second get";
  DISCH_TAC;
  INTRO_TAC ((*--*)Terminal.get_main_nonlinear "6601228004") [`z1`;`y2`;`y3`;`y4`;`y5`;`y6`];
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let taud_mud_126_x = 
prove_by_refinement(
  `!y3' y4' y5' y1 y2 y3 y4 y5 y6. 
    &0 <= y1 /\ &0 <= y2  ==> 
    y_of_x (mud_126_x_v1 y3 y4 y5) y1 y2 y3' y4' y5' y6 = taud y3 y1 y2 y6 y4 y5 - flat_term y3 
    `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.mud_126_x;Nonlin_def.taud;Sphere.flat_term;];
  Functional_equation.F_REWRITE_TAC;
  REWRITE_TAC[Sphere.delta_126_x;GSYM Sphere.delta_y];
  REPEAT WEAKER_STRIP_TAC;
  REPEAT (GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx);
  ASM_REWRITE_TAC[];
  TYPIFY `delta_y y3 y1 y2 y6 y4 y5 = delta_y y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
    BY(MESON_TAC[Merge_ineq.delta_y_sym]);
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let taud_mud_135_x = 
prove_by_refinement(
  `!y2' y4' y6' y1 y2 y3 y4 y5 y6. 
    &0 <= y1 /\ &0 <= y3  ==>  
    y_of_x (mud_135_x_v1 y2 y4 y6) y1 y2' y3 y4' y5 y6' = taud y2 y1 y3 y5 y4 y6 - flat_term y2
    `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.mud_135_x;Nonlin_def.taud;Sphere.flat_term;];
  Functional_equation.F_REWRITE_TAC;
  REWRITE_TAC[Sphere.delta_135_x;GSYM Sphere.delta_y];
  REPEAT WEAKER_STRIP_TAC;
  REPEAT (GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx);
  ASM_REWRITE_TAC[];
  TYPIFY `delta_y y2 y1 y3 y5 y4 y6 = delta_y y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
    BY(MESON_TAC[Merge_ineq.delta_y_sym]);
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let mud_126_135 = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6 y3' y4' y5'. mud_126_x_v1 y3' y4' y5' y1 y2 y3 y4 y5 y6 = 
    mud_135_x_v1 y3' y4' y5' y1 y3 y2 y4 y6 y5`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.mud_135_x;Nonlin_def.mud_126_x;];
  Functional_equation.F_REWRITE_TAC;
  REWRITE_TAC[Sphere.delta_135_x;Sphere.delta_126_x;GSYM Sphere.delta_y];
    BY(MESON_TAC[Merge_ineq.delta_x_sym]);
  ]);;
  (* }}} *)

let flat_term_2 = 
prove_by_refinement(
  `flat_term(&2) = -- sol0`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.flat_term];
  Calc_derivative.CALC_ID_TAC;
  BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let flat_term_2h0 = 
prove_by_refinement(
  `flat_term(&2 * h0) = &0`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.flat_term];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let flat_term_sol0 = 
prove_by_refinement(
  `!y. &2 <= y  ==> --sol0 <= flat_term y`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.flat_term];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `sol0 * (y - &2 * h0)/(&2 * h0 - &2) = -- sol0 + sol0 * (y - &2) / (&2 * h0 - &2)` (C SUBGOAL_THEN SUBST1_TAC);
    Calc_derivative.CALC_ID_TAC;
    BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  MATCH_MP_TAC (arith `&0 <= x ==> h <= h + x`);
  GMATCH_SIMP_TAC REAL_LE_MUL;
  GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
  MP_TAC Flyspeck_constants.bounds;
  BY(REWRITE_TAC[Sphere.h0] THEN FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let taud_2h0 = 
prove_by_refinement(
  `!y2 y3 y4 y5 y6.
    &0 <= delta_y (&2 * h0) y2 y3 y4 y5 y6 /\
    y2 <= &2 * h0 /\ y3 <= &2 * h0 ==>
    &0 <= taud (&2 * h0) y2 y3 y4 y5 y6`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.taud;arith `x - x = &0 /\ &0 / x = &0 /\ x * &0 = &0 /\ &0 + x = x`];
  REPEAT WEAKER_STRIP_TAC;
  GMATCH_SIMP_TAC REAL_LE_MUL;
  CONJ_TAC;
    GMATCH_SIMP_TAC SQRT_POS_LE;
    BY(ASM_REWRITE_TAC[]);
  BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let quadratic_root_minus_works = 
prove_by_refinement(
  `!a b c.
            ~(a = &0) /\ &0 <= b pow 2 - &4 * a * c
            ==> (let x = -- ( b + sqrt(b pow 2 - &4 * a * c))/ (&2 * a) in
                 a * x pow 2 + b * x + c = &0)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[LET_DEF;LET_END_DEF];
  REPEAT WEAKER_STRIP_TAC;
  Calc_derivative.CALC_ID_TAC;
  ASM_REWRITE_TAC[arith `~(&2 = &0)`];
  TYPED_ABBREV_TAC `d = b pow 2 - &4 * a * c`;
  TYPIFY `sqrt d * sqrt d = d` (C SUBGOAL_THEN MP_TAC);
    GMATCH_SIMP_TAC (GSYM SQRT_MUL);
    GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
    BY(ASM_REWRITE_TAC[]);
  FIRST_X_ASSUM MP_TAC;
  BY(CONV_TAC REAL_RING)
  ]);;
  (* }}} *)

let quadratic_root_imp_discr_nn = 
prove_by_refinement(
  `!a b c x.  (a * x pow 2 + b * x + c = &0) ==>
    &0 <= b pow 2 - &4 * a * c`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `b pow 2 - &4 * a * c =  (&2 * a * x + b ) pow 2` (C SUBGOAL_THEN SUBST1_TAC);
    FIRST_X_ASSUM MP_TAC;
    BY(CONV_TAC REAL_RING);
  BY(REWRITE_TAC[ REAL_LE_POW_2])
  ]);;
  (* }}} *)

let quadratic_root_plus_eq = 
prove_by_refinement(
  `!a b c m x. 
    (&0 < a) /\ (m <= x) /\ a * x pow 2 + b * x + c = &0 /\
    (&0 < &2 * m * a + b \/ (&2 * m * a + b) pow 2 < b pow 2 - &4 * a * c) ==>
       quadratic_root_plus (a,b,c) = x`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC Tame_lemmas.quadratic_root_plus_gt_eq;
  TYPED_ABBREV_TAC  `y = -- (b + sqrt( b pow 2 - &4 * a * c)) / (&2 * a)` ;
  TYPIFY `y` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  SUBCONJ_TAC;
    MATCH_MP_TAC quadratic_root_imp_discr_nn;
    BY(ASM_MESON_TAC[]);
  DISCH_TAC;
  CONJ_TAC;
    EXPAND_TAC "y";
    MATCH_MP_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] quadratic_root_minus_works);
    BY(ASM_REWRITE_TAC[] THEN ASM_TAC THEN REAL_ARITH_TAC);
  COMMENT "both cases";
  TYPIFY `y < m` ENOUGH_TO_SHOW_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  TYPIFY `&2 * a * y + b < &2 * a * m + b` ENOUGH_TO_SHOW_TAC;
    REWRITE_TAC[arith `&2 * a * y + b < &2 * a * m + b <=> a * y < a * m`];
    GMATCH_SIMP_TAC REAL_LT_LMUL_EQ;
    BY(ASM_REWRITE_TAC[]);
  TYPIFY `&2 * a * y + b  = -- sqrt(b pow 2 - &4 * a *c)` (C SUBGOAL_THEN SUBST1_TAC);
    EXPAND_TAC "y";
    Calc_derivative.CALC_ID_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  COMMENT "first case";
  ASM_CASES_TAC `&0 < &2 * m * a + b`;
    MATCH_MP_TAC REAL_LET_TRANS;
    TYPIFY `&0` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    REWRITE_TAC[arith `-- x <= &0 <=> &0 <= x`];
    GMATCH_SIMP_TAC SQRT_POS_LE;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  FIRST_X_ASSUM DISJ_CASES_TAC;
    BY(ASM_MESON_TAC[]);
  TYPIFY `(&2 * m * a + b) pow 2 < sqrt (b pow 2 - &4 * a * c) pow 2` (C SUBGOAL_THEN MP_TAC);
    GMATCH_SIMP_TAC SQRT_POW_2;
    BY(ASM_REWRITE_TAC[]);
  TYPED_ABBREV_TAC `d = sqrt(b pow 2 - &4 * a * c) `;
  ONCE_REWRITE_TAC[arith `-- d < &2 * a * m + b <=> --d < &2 * m * a +b`];
  REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS];
  TYPIFY `&0 <= d` (C SUBGOAL_THEN MP_TAC);
    EXPAND_TAC "d";
    GMATCH_SIMP_TAC SQRT_POS_LE;
    BY(ASM_REWRITE_TAC[]);
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let edge2_flatD_x1_delta_lemma2 = 
prove_by_refinement(
  `!d x1 x2 x3 x4 x5 x6. 
    delta_x x1 x2 x3 x4 x5 x6 = d /\
    &0 < x4 /\
    (delta_x1 x1 x2 x3 x4 x5 x6 < &0)
    ==> 
    edge2_flatD_x1 d x2 x3 x4 x5 x6 = x1`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.edge2_flatD_x1];
  REPEAT WEAKER_STRIP_TAC;
  TYPED_ABBREV_TAC `b = (-- delta_x1 (&0) x2 x3 x4 x5 x6)`;
  TYPED_ABBREV_TAC `c = (d - delta_x (&0) x2 x3 x4 x5 x6)`;
  TYPIFY `!z. d - delta_x z x2 x3 x4 x5 x6 = x4 * z pow 2 + b * z + c` ((C SUBGOAL_THEN ASSUME_TAC));
    EXPAND_TAC "c";
    EXPAND_TAC "b";
    REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1];
    BY(REAL_ARITH_TAC);
  ASM_REWRITE_TAC[];
  REWRITE_TAC[Nonlinear_lemma.abc_quadratic];
  TYPIFY `b pow 2 - &4 * x4 * c = ups_x x2 x3 x4 * ups_x x4 x5 x6 - &4 * x4 * d` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "b";
    EXPAND_TAC "c";
    REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1;Sphere.ups_x];
    BY(REAL_ARITH_TAC);
  MATCH_MP_TAC quadratic_root_plus_eq;
  TYPIFY `x1` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[arith `x <= x`];
  CONJ_TAC;
    FIRST_X_ASSUM (C INTRO_TAC [`x1`]);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  DISJ1_TAC;
  EXPAND_TAC "b";
  FIRST_X_ASSUM_ST `d < &0` MP_TAC;
  REWRITE_TAC[Nonlin_def.delta_x1];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let edge2_flatD_x1_delta_lemma3 = 
prove_by_refinement(
  ` main_nonlinear_terminal_v11 ==> (!d y1 y2 y3 y4 y5 y6.
    delta_y y1 y2 y3 y4 y5 y6 = d /\
    &0 <= d /\ d <= &20 ==>
    (ineq     [(&2,y1,#2.52);
    (&2,y2,#2.52); 
    (&2,y3,#2.52);
    (#3.01,y4,#3.915);
    (&2,y5,&2);
    (&2,y6,&2)
  ]
       (    edge2_flatD_x1 d (y2*y2) (y3*y3) (y4*y4) (y5*y5) (y6*y6) = y1*y1)))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
  REPEAT WEAKER_STRIP_TAC;
  MATCH_MP_TAC edge2_flatD_x1_delta_lemma2;
  INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3078028960") yys;
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
  ANTS_TAC;
    BY(ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  ASM_SIMP_TAC[arith `&0 <= d ==> ~(d < &0)`;arith `d <= &20 ==> ~(d > &20)`];
  REWRITE_TAC[Sphere.y_of_x;arith `y1 pow 2 = y1 * y1`];
  DISCH_THEN (unlist REWRITE_TAC);
  REWRITE_TAC[GSYM Sphere.delta_y];
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let delta_diff = 
prove_by_refinement(
  `!x1 z1 x2 x3 x4 x5 x6.
    delta_x x1 x2 x3 x4 x5 x6 = delta_x z1 x2 x3 x4 x5 x6 + 
    delta_x1 x1 x2 x3 x4 x5 x6 * (x1 - z1) + x4 * (x1 - z1) pow 2`,

  (* {{{ proof *)
  [
   BY(REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1] THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let delta_2_nn = 
prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> (!z1 y2 y3 y4.
			   &2 <= z1 /\ z1 <= &2 * h0 /\
	&2 <= y2 /\ y2 <= &2 * h0 /\
	&2 <= y3 /\ y3 <= &2 * h0 /\
	#3.01 <= y4 /\ y4 <= #3.915 /\
        delta_y z1 y2 y3 y4 (&2) (&2) = &0 ==>
	&0 <= delta_y (&2)  y2 y3 y4 (&2) (&2))
    `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.delta_y];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (UNDISCH2 (Terminal.get_main_nonlinear "3078028960")) [`&2`;`y2`;`y3`;`y4`;`&2`;`&2`];
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  REWRITE_TAC[Sphere.y_of_x;Sphere.delta_y];
  ASM_REWRITE_TAC[arith `~(&0 > &20)`];
  DISCH_TAC;
  FIRST_X_ASSUM DISJ_CASES_TAC;
    INTRO_TAC delta_diff [`&2* &2`;`z1 * z1`;`y2*y2`;`y3*y3`;`y4*y4`;`&2* &2`;`&2 * &2`];
    ASM_REWRITE_TAC[];
    DISCH_THEN SUBST1_TAC;
    MATCH_MP_TAC (arith `&0 <= x /\ &0 <= y ==> &0 <= &0 + x + y`);
    CONJ_TAC;
      ONCE_REWRITE_TAC[arith `&0 <= a * b <=> &0 <= (--a) *(--b)`];
      GMATCH_SIMP_TAC REAL_LE_MUL;
      CONJ_TAC;
        BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
      TYPIFY `&2 * &2 <= z1 * z1` ENOUGH_TO_SHOW_TAC;
        BY(REAL_ARITH_TAC);
      GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    GMATCH_SIMP_TAC REAL_LE_MUL;
    REWRITE_TAC[ REAL_LE_POW_2];
    BY(REWRITE_TAC[ REAL_LE_SQUARE]);
  BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let delta_mono = 
prove_by_refinement(
  ` main_nonlinear_terminal_v11 ==> (!z1 y1 y2 y3 y4 y5 y6. 
	&2 <= y1 /\ y1 <= z1 /\ z1 <= &2 * h0 /\
	&2 <= y2 /\ y2 <= &2 * h0 /\
	&2 <= y3 /\ y3 <= &2 * h0 /\
	#3.01 <= y4 /\ y4 <= #3.915 /\
	&2 <= y5 /\ y5 <= &2  /\
	&2 <= y6 /\ y6 <= &2 /\
	&0 <= delta_y y1 y2 y3 y4 y5 y6 /\
	delta_y y1 y2 y3 y4 y5 y6 <= &20 ==>
	delta_y z1 y2 y3 y4 y5 y6 <= delta_y y1 y2 y3 y4 y5 y6)
`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[Sphere.delta_y];
  INTRO_TAC delta_diff [`y1*y1`;`z1*z1`;`y2*y2`;`y3*y3`;`y4*y4`;`y5*y5`;`y6*y6`];
  DISCH_THEN SUBST1_TAC;
  MATCH_MP_TAC (arith `&0 <= b /\ &0 <= c ==> a <= a + b + c`);
  CONJ2_TAC;
    GMATCH_SIMP_TAC REAL_LE_MUL;
    REWRITE_TAC[ REAL_LE_POW_2];
    BY(REWRITE_TAC[ REAL_LE_SQUARE]);
  INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3078028960") yys;
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  ASM_SIMP_TAC[arith `&0 <= d ==> ~(d < &0)`;arith `d <= d1 ==> ~(d > d1)`];
  REWRITE_TAC[Sphere.y_of_x];
  ONCE_REWRITE_TAC[arith `&0 <= x * y <=> &0 <= (-- x) * (-- y)`];
  DISCH_TAC;
  GMATCH_SIMP_TAC REAL_LE_MUL;
  CONJ_TAC;
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  MATCH_MP_TAC (arith `y1 * y1 <= z1 * z1 ==> &0 <= -- (y1 * y1 - z1 * z1)`);
  GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let flat_term2_126_x_eval = 
prove_by_refinement(
  ` main_nonlinear_terminal_v11 ==> (!d z y1 y2 y3 y4 y5 y6.
    delta_y z y1 y2 y6 (&2) (&2) = d /\ &0 <= d /\ d <= &20 /\
      &2 <= z /\ z <= &2 * h0 /\ &2 <= y1 /\ y1 <= &2 * h0 /\
      &2 <= y2 /\ y2 <= &2 * h0 /\
      #3.01 <= y6 /\ y6 <= #3.915 ==>
    y_of_x (flat_term2_126_x d (&4) (&4)) y1 y2 y3 y4 y5 y6 = flat_term z)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x;Nonlin_def.flat_term2_126_x;Nonlin_def.edge2_126_x];
  REWRITE_TAC[Functional_equation.uni;Functional_equation.compose6;Functional_equation.constant6;Functional_equation.proj_x1;Functional_equation.proj_x2;Functional_equation.proj_x6];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (UNDISCH2 edge2_flatD_x1_delta_lemma3) [`d`;`z`;`y1`;`y2`;`y6`;`&2`;`&2`];
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  REWRITE_TAC[arith `&2 * &2 = &4`];
  DISCH_THEN SUBST1_TAC;
  REWRITE_TAC[Sphere.flat_term_x];
  GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let flat_term2_135_x_eval = 
prove_by_refinement(
  ` main_nonlinear_terminal_v11 ==> (!d z y1 y2 y3 y4 y5 y6.
    delta_y z y1 y3 y5 (&2) (&2) = d /\ &0 <= d /\ d <= &20 /\
      &2 <= z /\ z <= &2 * h0 /\ &2 <= y1 /\ y1 <= &2 * h0 /\
      &2 <= y3 /\ y3 <= &2 * h0 /\
      #3.01 <= y5 /\ y5 <= #3.915 ==>
    y_of_x (flat_term2_135_x d (&4) (&4)) y1 y2 y3 y4 y5 y6 = flat_term z)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x;Nonlin_def.flat_term2_135_x;Nonlin_def.edge2_135_x];
  REWRITE_TAC[Functional_equation.uni;Functional_equation.compose6;Functional_equation.constant6;Functional_equation.proj_x1;Functional_equation.proj_x2;Functional_equation.proj_x6;Functional_equation.proj_x5;Functional_equation.proj_x3];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (UNDISCH2 edge2_flatD_x1_delta_lemma3) [`d`;`z`;`y1`;`y3`;`y5`;`&2`;`&2`];
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  REWRITE_TAC[arith `&2 * &2 = &4`];
  DISCH_THEN SUBST1_TAC;
  REWRITE_TAC[Sphere.flat_term_x];
  GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let delta_126_135 = 
prove_by_refinement(
  `!a b c y1 y2 y3 y4 y5 y6.
    delta_126_x a b c y1 y2 y3 y4 y5 y6 = delta_135_x a b c y1 y3 y2 y4 y6 y5`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.delta_126_x;Sphere.delta_135_x];
  BY(MESON_TAC[Merge_ineq.delta_x_sym])
  ]);;
  (* }}} *)

let delta_126_x_2h0_le_d = 
prove_by_refinement(
  ` main_nonlinear_terminal_v11 ==> (!d z1 y1 y2 y3 y4 y5 y6.
		&2 <= z1 /\
  z1 <= &2 * h0 /\
  z1 <= &2 * h0 /\
  &2 <= y1 /\
  y1 <= &2 * h0 /\
  &2 <= y2 /\
  y2 <= &2 * h0 /\
   #3.01 <= y6 /\
  y6 <=  #3.915 /\
  &0 <= d /\ d <= &20 /\
	delta_y z1 y1 y2 y6 (&2) (&2) = d ==>
      y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 <= d)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x];
  REWRITE_TAC[arith `&4 * h0 * h0 = (&2 * h0) * (&2 * h0)`];
  REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y];
  TYPIFY `delta_y y1 y2 (&2 * h0) (&2) (&2) y6 = delta_y (&2 * h0) y1 y2 y6 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC);
    BY(MESON_TAC[Merge_ineq.delta_y_sym]);
  INTRO_TAC (UNDISCH delta_mono) [`&2 * h0`;`z1`;`y1`;`y2`;`y6`;`&2`;`&2`];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let delta_135_x_2h0_le_d = 
prove_by_refinement(
  ` main_nonlinear_terminal_v11 ==> (!d z1 y1 y2 y3 y4 y5 y6.
		&2 <= z1 /\
  z1 <= &2 * h0 /\
  z1 <= &2 * h0 /\
  &2 <= y1 /\
  y1 <= &2 * h0 /\
  &2 <= y3 /\
  y3 <= &2 * h0 /\
   #3.01 <= y5 /\
  y5 <=  #3.915 /\
  &0 <= d /\ d <= &20 /\
	delta_y z1 y1 y3 y5 (&2) (&2) = d ==>
      y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 <= d)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[Sphere.y_of_x;Sphere.delta_135_x];
  REWRITE_TAC[arith `&4 * h0 * h0 = (&2 * h0) * (&2 * h0)`];
  REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y];
  TYPIFY `delta_y y1 (&2 * h0) y3 (&2) y5 (&2) = delta_y (&2 * h0) y1 y3 y5 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC);
    BY(MESON_TAC[Merge_ineq.delta_y_sym]);
  INTRO_TAC (UNDISCH delta_mono) [`&2 * h0`;`z1`;`y1`;`y3`;`y5`;`&2`;`&2`];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  BY(ASM_REWRITE_TAC[])
  ]);;
  (* }}} *)

let lemma_5546286427 = 
prove_by_refinement(
  `  main_nonlinear_terminal_v11 ==> (!z1 y1 y2 y3 y4 y5 y6. ineq [
    (&2,y1,#2.52);
    (&2,y2,#2.52);
    (&2,y3,#2.52);
    (&2,y4,&2);
    (#3.01,y5,#3.237);
    (#3.01,y6,#3.237);
    (&2,z1,#2.52)
  ]
(
  &0 = delta_y z1 y1 y2 y6 (&2) (&2) ==>
    (taum y1 y2 y3 y4 y5 y6 + flat_term z1 + #0.12 > #0.616)))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC ((*--*)Terminal.get_main_nonlinear "5546286427") yys;
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  GMATCH_SIMP_TAC flat_term2_126_x_eval;
  TYPIFY `z1` EXISTS_TAC;
  CONJ_TAC;
    BY(ASM_REWRITE_TAC[] THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  COMMENT "remove delta_126_x";
  DISCH_THEN DISJ_CASES_TAC;
    BY(ASM_REWRITE_TAC[]);
  INTRO_TAC (UNDISCH2 delta_126_x_2h0_le_d) [`&0`;`z1`;`y1`;`y2`;`y3`;`y4`;`y5`;`y6`];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let taud_ge_flat_term = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 /\ y2 <= &2 * h0 /\ y3 <= &2 * h0 /\
    &0 <= delta_y y1 y2 y3 y4 y5 y6 ==>
    flat_term y1 <= taud y1 y2 y3 y4 y5 y6`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.taud;Sphere.flat_term];
  REPEAT WEAKER_STRIP_TAC;
  REWRITE_TAC[arith `a <= a + b <=> &0 <= b`];
  GMATCH_SIMP_TAC REAL_LE_MUL;
  GMATCH_SIMP_TAC SQRT_POS_LE;
  ASM_REWRITE_TAC[];
  BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let terminal_pent_taum126_012 = 
prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
      #0.12 <= taud y126 y1 y2 y6 (&2) (&2) /\
      &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
     (ineq [
       (&2,y1,&2 * h0);
       (&2,y2,&2 * h0);
       (&2,y3,&2 * h0);
       (&2,y4,&2);
       (#3.01,y5,#3.237);
       (#3.01,y6,#3.237);
       (&2,y126,&2 * h0);
       (&2,y135,&2 * h0)
     ]
     (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
     `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.ineq];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&0`;`y135`;`y1`;`y3`;`y5`;`(&2)`;`&2`];
  REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
  ANTS_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3665919985") yys;
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  REWRITE_TAC[arith `x > y <=> y < x`];
  DISCH_TAC;
  INTRO_TAC (UNDISCH OWZLKVY4) [`y135`;`y1`;`y3`;`y5`;`&2`;`&2`];
  ANTS_TAC;
    BY(REWRITE_TAC[Sphere.cstab] THEN ASM_TAC THEN REAL_ARITH_TAC);
  DISCH_TAC;
  INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3665919985") yys;
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  DISCH_TAC;
  COMMENT "case y=2";
  FIRST_X_ASSUM (DISJ_CASES_TAC);
    INTRO_TAC ((*--*)Terminal.get_main_nonlinear "7903347843") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    REWRITE_TAC[Sphere.y_of_x;mud_126_135];
    REWRITE_TAC[GSYM Sphere.y_of_x];
    TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
      BY(MESON_TAC[Terminal.taum_sym]);
    GMATCH_SIMP_TAC taud_mud_135_x;
    CONJ_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    MATCH_MP_TAC (arith `x <= a + b   ==> t + x > #0.616 ==> #0.616 < a + t + b`);
    MATCH_MP_TAC (arith `t2 <= t135 /\ -- s <= f /\ #0.12 <= t126 ==> t2 - f - s + #0.12 <= t126+t135`);
    ASM_REWRITE_TAC[];
    CONJ_TAC;
      FIRST_X_ASSUM_ST `<=` MP_TAC THEN ASM_REWRITE_TAC[];
      FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
      BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
    MATCH_MP_TAC flat_term_sol0;
    BY(REAL_ARITH_TAC);
  COMMENT "case &0 <= tau";
  ASM_CASES_TAC `&0 <= taud y135 y1 y3 y5 (&2) (&2)`;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  COMMENT "case y=&2*h0";
  FIRST_X_ASSUM (DISJ_CASES_TAC);
    INTRO_TAC taud_2h0 [`y1`;`y3`;`y5`;`&2`;`&2`];
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
    ANTS_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    BY(REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  COMMENT "case delta=0";
  FIRST_X_ASSUM DISJ_CASES_TAC;
    INTRO_TAC (UNDISCH lemma_5546286427) [`z1`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
      BY(MESON_TAC[Terminal.taum_sym]);
    DISCH_TAC;
    INTRO_TAC taud_ge_flat_term [`z1`;`y1`;`y3`;`y5`;`&2`;`&2`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  COMMENT "final case";
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let terminal_pent_tau135_012 = 
prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
      #0.12 <= taud y135 y1 y3 y5 (&2) (&2) /\
      &0 <= delta_y y126 y1 y2 y6 (&2) (&2) ==>
     (ineq [
       (&2,y1,&2 * h0);
       (&2,y2,&2 * h0);
       (&2,y3,&2 * h0);
       (&2,y4,&2);
       (#3.01,y5,#3.237);
       (#3.01,y6,#3.237);
       (&2,y126,&2 * h0);
       (&2,y135,&2 * h0)
     ]
     (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
     `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.ineq];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (UNDISCH2 terminal_pent_taum126_012) [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`;`y135`;`y126`];
  ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
  TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REWRITE_TAC[Terminal.taum_sym]);
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let sqrt20 = 
prove_by_refinement(
  `#4.47 <= sqrt(&20)`,

  (* {{{ proof *)
  [
  MATCH_MP_TAC REAL_LE_RSQRT;
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let taud_053 = 
prove_by_refinement(
  `! y2 y3 y4 y5 y6.
    y2 <= &2 * h0 /\
    y3 <= &2 * h0 /\
    &20 <= delta_y (&2 * h0) y2 y3 y4 y5 y6 ==>
    #0.053 <= taud (&2 * h0) y2 y3 y4 y5 y6`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.taud];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `sol0 * (&2 * h0 - &2 * h0) / (&2 * h0 - &2) = &0` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REAL_ARITH_TAC);
  TYPIFY `#0.053 = #4.47 * (#0.053 / #4.47)` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REAL_ARITH_TAC);
  REWRITE_TAC[arith `&0 + x= x`];
  MATCH_MP_TAC REAL_LE_MUL2;
  CONJ_TAC;
    BY(REAL_ARITH_TAC);
  CONJ_TAC;
    MATCH_MP_TAC REAL_LE_TRANS;
    TYPIFY `sqrt(&20)` EXISTS_TAC;
    REWRITE_TAC[sqrt20];
    GMATCH_SIMP_TAC SQRT_MONO_LE_EQ;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  CONJ_TAC;
    BY(REAL_ARITH_TAC);
  BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let terminal_pent_tau126_2 = 
prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
     y126 = &2 /\
      &0 <= delta_y y126 y1 y2 y6 (&2) (&2) /\
      &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
     (ineq [
       (&2,y1,&2 * h0);
       (&2,y2,&2 * h0);
       (&2,y3,&2 * h0);
       (&2,y4,&2);
       (#3.01,y5,#3.237);
       (#3.01,y6,#3.237);
       (&2,y126,&2 * h0);
       (&2,y135,&2 * h0)
     ]
     (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
     `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.ineq];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&0`;`y135`;`y1`;`y3`;`y5`;`(&2)`;`&2`];
  REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
  ANTS_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC);
    BY(MESON_TAC[Terminal.taum_sym]);
  COMMENT "case tau >= 0.12";
  ASM_CASES_TAC `#0.12 <= taud z1 y1 y3 y5 (&2) (&2)`;
    INTRO_TAC (UNDISCH2 terminal_pent_tau135_012) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`y135`];
    ANTS_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    BY(REWRITE_TAC[]);
  COMMENT "case z1= &2";
  ASM_CASES_TAC `z1 = &2`;
    INTRO_TAC ((*--*)Terminal.get_main_nonlinear "7997589055") yys;
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    GMATCH_SIMP_TAC taud_mud_126_x;
    GMATCH_SIMP_TAC taud_mud_135_x;
    REWRITE_TAC[flat_term_2];
    TYPIFY_GOAL_THEN ` &0 <= y1 /\ &0 <= y2 /\ &0 <= y3` (unlist REWRITE_TAC);
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    ASM_REWRITE_TAC[];
    REPEAT (FIRST_X_ASSUM_ST `x = &2` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  COMMENT "case delta=0";
  ASM_CASES_TAC `&0 = delta_y z1 y1 y3 y5 (&2) (&2)`;
    INTRO_TAC ((*--*)Terminal.get_main_nonlinear "2565248885") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
    REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    REWRITE_TAC[arith `x > &0 <=> ~(x <= &0)`];
    GMATCH_SIMP_TAC (UNDISCH2 delta_126_x_2h0_le_d);
    CONJ_TAC;
      TYPIFY `z1` EXISTS_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    GMATCH_SIMP_TAC taud_mud_135_x;
    REWRITE_TAC[flat_term_2];
    GMATCH_SIMP_TAC (UNDISCH2 flat_term2_126_x_eval);
    TYPIFY `z1` EXISTS_TAC;
    CONJ_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    CONJ_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    INTRO_TAC taud_ge_flat_term [`z1`;`y1`;`y3`;`y5`;`&2`;`&2`];
    ANTS_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[];
    BY(REAL_ARITH_TAC);
  COMMENT "case delta>=20";
  TYPIFY `z1 = &2 * h0` (C SUBGOAL_THEN MP_TAC);
    BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
  DISCH_TAC;
  ASM_CASES_TAC `&20 <= delta_y z1 y1 y3 y5 (&2) (&2)`;
    INTRO_TAC ((*--*)Terminal.get_main_nonlinear "2320951108") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
    REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    GMATCH_SIMP_TAC taud_mud_135_x;
    REWRITE_TAC[flat_term_2];
    INTRO_TAC taud_053 [`y1`;`y3`;`y5`;`&2`;`&2`];
    ANTS_TAC;
      FIRST_X_ASSUM MP_TAC;
      BY(ASM_REWRITE_TAC[]);
    ASM_REWRITE_TAC[];
    REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
    DISCH_TAC;
    CONJ_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC);
    BY(REAL_ARITH_TAC);
  COMMENT "case delta <= 20";
  INTRO_TAC ((*--*)Terminal.get_main_nonlinear "5429238960") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
  REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  GMATCH_SIMP_TAC taud_mud_135_x;
  REWRITE_TAC[flat_term_2];
  CONJ_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  INTRO_TAC (UNDISCH2 delta_126_x_2h0_le_d) [`delta_y z1 y1 y3 y5 (&2) (&2)`;`z1`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
  ANTS_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  INTRO_TAC taud_2h0 [`y1`;`y3`;`y5`;`&2`;`&2`];
  ANTS_TAC;
    FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  ASM_REWRITE_TAC[];
  REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
  BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let terminal_pent_tau135_2 = 
prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
     y135 = &2 /\
      &0 <= delta_y y126 y1 y2 y6 (&2) (&2) /\
      &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
     (ineq [
       (&2,y1,&2 * h0);
       (&2,y2,&2 * h0);
       (&2,y3,&2 * h0);
       (&2,y4,&2);
       (#3.01,y5,#3.237);
       (#3.01,y6,#3.237);
       (&2,y126,&2 * h0);
       (&2,y135,&2 * h0)
     ]
     (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
     `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.ineq];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (UNDISCH2 terminal_pent_tau126_2) [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`;`y135`;`y126`];
  ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
  TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REWRITE_TAC[Terminal.taum_sym]);
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let terminal_pent_tau126_2h0 = 
prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
     y126 = &2 * h0 /\
      &20 <= delta_y y126 y1 y2 y6 (&2) (&2) /\
      &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
     (ineq [
       (&2,y1,&2 * h0);
       (&2,y2,&2 * h0);
       (&2,y3,&2 * h0);
       (&2,y4,&2);
       (#3.01,y5,#3.237);
       (#3.01,y6,#3.237);
       (&2,y126,&2 * h0);
       (&2,y135,&2 * h0)
     ]
     (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
     `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.ineq];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&0`;`y135`;`y1`;`y3`;`y5`;`(&2)`;`&2`];
  REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
  ANTS_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC);
    BY(MESON_TAC[Terminal.taum_sym]);
  COMMENT "case tau >= 0.12";
  ASM_CASES_TAC `#0.12 <= taud z1 y1 y3 y5 (&2) (&2)`;
    INTRO_TAC (UNDISCH2 terminal_pent_tau135_012) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`y135`];
    ANTS_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    BY(REWRITE_TAC[]);
  COMMENT "case z1= &2";
  ASM_CASES_TAC `z1 = &2`;
    INTRO_TAC (UNDISCH2 terminal_pent_tau135_2) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`z1`];
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  COMMENT "case delta = 0";
  ASM_CASES_TAC `&0 = delta_y z1 y1 y3 y5 (&2) (&2)`;
    INTRO_TAC ((*--*)Terminal.get_main_nonlinear "1948775510") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    GMATCH_SIMP_TAC (taud_mud_135_x);
    CONJ_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    REWRITE_TAC[flat_term_2h0];
    GMATCH_SIMP_TAC flat_term2_126_x_eval;
    TYPIFY `z1` EXISTS_TAC;
    CONJ_TAC;
      ASM_REWRITE_TAC[];
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    INTRO_TAC taud_ge_flat_term [`z1`;`y1`;`y3`;`y5`;`&2`;`&2`];
    ANTS_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    INTRO_TAC (UNDISCH2 delta_126_x_2h0_le_d) [`&0`;`z1`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
    ANTS_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    REWRITE_TAC[arith `x > &0 <=> ~(x <= &0)`] THEN DISCH_THEN (unlist REWRITE_TAC);
    REWRITE_TAC[Sphere.delta_135_x;Sphere.y_of_x;arith `&4 * h0 * h0 = (&2 * h0) * (&2 * h0)`];
    REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y];
    TYPIFY `delta_y y1 (&2 * h0) y2 (&2) y6 (&2) = delta_y y126 y1 y2 y6 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC);
      ASM_REWRITE_TAC[];
      BY(MESON_TAC[Merge_ineq.delta_y_sym]);
    FIRST_X_ASSUM kill;
    ASM_REWRITE_TAC[];
    REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  COMMENT "case z1=2h0, delta>=20";
  TYPIFY `z1 = &2 * h0` (C SUBGOAL_THEN MP_TAC);
    BY(ASM_MESON_TAC[]);
  DISCH_TAC;
  INTRO_TAC taud_053 [`y1`;`y2`;`y6`;`&2`;`&2`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    BY(FIRST_X_ASSUM_ST `&20 <= d` MP_TAC THEN ASM_REWRITE_TAC[]);
  DISCH_TAC;
  ASM_CASES_TAC `&20 <= delta_y z1 y1 y3 y5 (&2) (&2)`;
    INTRO_TAC taud_053 [`y1`;`y3`;`y5`;`&2`;`&2`];
    ANTS_TAC;
      ASM_REWRITE_TAC[];
      BY(REPEAT (FIRST_X_ASSUM_ST `&20 <= d` MP_TAC) THEN ASM_REWRITE_TAC[]);
    DISCH_TAC;
    INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3665919985") yys;
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    ASM_REWRITE_TAC[];
    REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
    REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[];
    BY(REAL_ARITH_TAC);
  COMMENT "case z1=2h0, delta<=20";
  INTRO_TAC ((*--*)Terminal.get_main_nonlinear "5708641738") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  INTRO_TAC (UNDISCH2 delta_126_x_2h0_le_d) [`delta_y z1 y1 y3 y5 (&2) (&2)`;`z1`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
  ANTS_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  ASM_REWRITE_TAC[];
  REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
  INTRO_TAC taud_2h0 [`y1`;`y3`;`y5`;`&2`;`&2`];
  ANTS_TAC;
    BY(ASM_TAC THEN ASM_MESON_TAC[]);
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let taud_sqrt20 = 
prove_by_refinement(
  ` main_nonlinear_terminal_v11 ==> (!z1 y1 y2 y3 y4 y5 y6.
     &0 <= &20 /\
      &20 <= &20 /\
      &2 <= z1 /\
      z1 <= &2 * h0 /\
      &2 <= y1 /\
      y1 <= &2 * h0 /\
      &2 <= y3 /\
      y3 <= &2 * h0 /\
       #3.01 <= y5 /\
      y5 <=  #3.915 /\
    delta_y z1 y1 y3 y5 (&2) (&2) = &20 ==>
    y_of_x (flat_term2_135_x (&20) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
	(#0.012 +  #0.01 * (#2.52 * &2 - y1 - y3 )) * #4.47 <= taud z1 y1 y3 y5 (&2) (&2))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  GMATCH_SIMP_TAC flat_term2_135_x_eval;
  TYPIFY `z1` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[Nonlin_def.taud;Sphere.flat_term];
  REWRITE_TAC[ (arith `u + c * s <= u + s' * c' <=> c * s <= c' * s'`)];
  MATCH_MP_TAC REAL_LE_MUL2;
  CONJ_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  ASM_REWRITE_TAC[sqrt20];
  BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let terminal_pent_tau126_delta20 = 
prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
      delta_y y126 y1 y2 y6 (&2) (&2) = &20 /\
      &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
     (ineq [
       (&2,y1,&2 * h0);
       (&2,y2,&2 * h0);
       (&2,y3,&2 * h0);
       (&2,y4,&2);
       (#3.01,y5,#3.237);
       (#3.01,y6,#3.237);
       (&2,y126,&2 * h0);
       (&2,y135,&2 * h0)
     ]
     (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
     `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.ineq];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&0`;`y135`;`y1`;`y3`;`y5`;`(&2)`;`&2`];
  REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
  ANTS_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC);
    BY(MESON_TAC[Terminal.taum_sym]);
  COMMENT "case tau >= 0.12";
  ASM_CASES_TAC `#0.12 <= taud z1 y1 y3 y5 (&2) (&2)`;
    INTRO_TAC (UNDISCH2 terminal_pent_tau135_012) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`y135`];
    ANTS_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    BY(REWRITE_TAC[]);
  COMMENT "case z1= &2";
  ASM_CASES_TAC `z1 = &2`;
    INTRO_TAC (UNDISCH2 terminal_pent_tau135_2) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`z1`];
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  COMMENT "delta issue";
  TYPIFY `~( y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y3 y2 y4 y6 y5 > &20 )` (C SUBGOAL_THEN MP_TAC);
    REWRITE_TAC[arith `~(x > d) <=> (x<=d)`];
    GMATCH_SIMP_TAC delta_135_x_2h0_le_d;
    TYPIFY `y126` EXISTS_TAC;
    ASM_REWRITE_TAC[];
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  DISCH_TAC;
  COMMENT "case delta = 0";
  ASM_CASES_TAC `&0 = delta_y z1 y1 y3 y5 (&2) (&2)`;
    INTRO_TAC ((*--*)Terminal.get_main_nonlinear "1008824382") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    GMATCH_SIMP_TAC flat_term2_126_x_eval;
    TYPIFY `z1` EXISTS_TAC;
    CONJ_TAC;
      ASM_REWRITE_TAC[];
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    GMATCH_SIMP_TAC flat_term2_135_x_eval;
    TYPIFY `y126` EXISTS_TAC;
    CONJ_TAC;
      FIRST_X_ASSUM_ST `d = &20` SUBST1_TAC;
      ASM_REWRITE_TAC[];
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    INTRO_TAC mu_y_ft_combine2 [`y126`;`y1`;`y2`];
    ANTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    TYPIFY `mu_y y126 y1 y2 * sqrt(&20) + flat_term y126 <= taud y126 y1 y2 y6 (&2) (&2)` (C SUBGOAL_THEN MP_TAC);
      REWRITE_TAC[Nonlin_def.taud;Nonlin_def.mu_y;Sphere.flat_term];
      REWRITE_TAC[ (arith `c * s + u <= u + s' * c <=> c * s <= c * s'`)];
      GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP;
      CONJ_TAC;
        BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
      GMATCH_SIMP_TAC SQRT_MONO_LE_EQ;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    TYPIFY `(#0.012 + #0.01 * ( #2.52 * &2 - y1 - y2)) *  #4.47  <= mu_y (&2 * h0) y1 y2 * sqrt(&20)` (C SUBGOAL_THEN MP_TAC);
      REWRITE_TAC[Nonlin_def.mu_y];
      MATCH_MP_TAC REAL_LE_MUL2;
      CONJ_TAC;
        BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
      REWRITE_TAC[sqrt20];
      BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    INTRO_TAC taud_ge_flat_term [`z1`;`y1`;`y3`;`y5`;`&2`;`&2`];
    ANTS_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    FIRST_X_ASSUM_ST `~` (unlist REWRITE_TAC);
    REWRITE_TAC[arith `x > &0 <=> ~(x <= &0)`];
    GMATCH_SIMP_TAC delta_126_x_2h0_le_d;
    CONJ_TAC;
      TYPIFY `z1` EXISTS_TAC;
      ASM_REWRITE_TAC[];
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    ASM_REWRITE_TAC[];
    REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
    REWRITE_TAC[flat_term_2h0];
    BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  COMMENT "z1=2h0 and delta <=20";
  TYPIFY `z1 = &2 * h0` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
  ASM_CASES_TAC `delta_y z1 y1 y3 y5 (&2) (&2) <= &20`;
    INTRO_TAC ((*--*)Terminal.get_main_nonlinear "1586903463") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    INTRO_TAC taud_2h0 [`y1`;`y3`;`y5`;`&2`;`&2`];
    ANTS_TAC;
      BY(REPEAT (FIRST_X_ASSUM_ST `<=` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
    INTRO_TAC (UNDISCH2 taud_sqrt20) [`y126`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
    ANTS_TAC;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    ASM_REWRITE_TAC[];
    REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x;arith `&4 * h0 * h0 =  (&2 * h0) * (&2 * h0)`];
    REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y];
    TYPIFY `delta_y y1 y3 (&2 * h0) (&2) (&2) y5 = delta_y z1 y1 y3 y5 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC);
      ASM_REWRITE_TAC[];
      BY(MESON_TAC[Merge_ineq.delta_y_sym]);
    ASM_REWRITE_TAC[];
    REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  COMMENT "z1=2h0 and delta> 20";
  INTRO_TAC ((*--*)Terminal.get_main_nonlinear "8875146520") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  GMATCH_SIMP_TAC taud_mud_126_x;
  REWRITE_TAC[flat_term_2h0];
  INTRO_TAC (UNDISCH2 taud_sqrt20) [`y126`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
  ANTS_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  FIRST_X_ASSUM_ST `y_of_x` (unlist REWRITE_TAC);
  REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x;arith `&4 * h0 * h0 =  (&2 * h0) * (&2 * h0)`];
  REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y];
  TYPIFY `delta_y y1 y3 (&2 * h0) (&2) (&2) y5 = delta_y z1 y1 y3 y5 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC);
    ASM_REWRITE_TAC[];
    BY(MESON_TAC[Merge_ineq.delta_y_sym]);
  ASM_REWRITE_TAC[];
  REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let terminal_pent_taum = 
prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
      &20 <= delta_y y126 y1 y2 y6 (&2) (&2) /\
      &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
     (ineq [
       (&2,y1,&2 * h0);
       (&2,y2,&2 * h0);
       (&2,y3,&2 * h0);
       (&2,y4,&2);
       (#3.01,y5,#3.237);
       (#3.01,y6,#3.237);
       (&2,y126,&2 * h0);
       (&2,y135,&2 * h0)
     ]
     (#0.616 < taum y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taum y135 y1 y3 y5 (&2) (&2))))
     `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.ineq];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&20`;`y126`;`y1`;`y2`;`y6`;`(&2)`;`&2`];
  REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
  ANTS_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (UNDISCH2 OWZLKVY4) [`y126`;`y1`;`y2`;`y6`;`&2`;`&2`];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC);
  INTRO_TAC (UNDISCH2 OWZLKVY4) [`y135`;`y1`;`y3`;`y5`;`&2`;`&2`];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC);
  TYPIFY `#0.616 <      taud z1 y1 y2 y6 (&2) (&2) +     taum y1 y2 y3 y4 y5 y6 +     taud y135 y1 y3 y5 (&2) (&2)` ENOUGH_TO_SHOW_TAC;
    BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  COMMENT "case z1=2";
  FIRST_X_ASSUM DISJ_CASES_TAC;
    INTRO_TAC (UNDISCH2 terminal_pent_tau126_2) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`z1`;`y135`];
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    BY(REWRITE_TAC[]);
  COMMENT "case z1=2h0";
  FIRST_X_ASSUM DISJ_CASES_TAC;
    INTRO_TAC (UNDISCH2 terminal_pent_tau126_2h0) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`z1`;`y135`];
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    BY(REWRITE_TAC[]);
  COMMENT "case delta=20";
  FIRST_X_ASSUM DISJ_CASES_TAC;
    INTRO_TAC (UNDISCH2 terminal_pent_tau126_delta20) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`z1`;`y135`];
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
    BY(REWRITE_TAC[]);
  COMMENT "case tau012";
  INTRO_TAC (UNDISCH2 terminal_pent_taum126_012) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`z1`;`y135`];
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  BY(REWRITE_TAC[])
  ]);;
  (* }}} *)

(* HEXAGON SECTION terminal_hex *)

let taud_minimizer_terminal_hex_cases = 
prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4.
       (&0 <= delta_y y1 y2 y3 y4 (&2) (&2)  /\
	&2 <= y1 /\ y1 <= &2 * h0 /\  &2 <= y2 /\ y2 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 /\
	 #3.01 <= y4 /\ y4 <= #3.915 /\ taum y1 y2 y3 y4 (&2) (&2) < &0 ==> 
	  (?z1. &0 <= delta_y z1 y2 y3 y4 (&2) (&2) /\
	   &2 <= z1 /\ z1 <= &2 * h0 /\ taud z1 y2 y3 y4 (&2) (&2)  <= taud y1 y2 y3 y4 (&2) (&2) /\
	  ( z1 = &2  \/ &0 = delta_y z1 y2 y3 y4 (&2) (&2) ))))`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC taud_minimizer [`&2`;`&2 * h0`;`&0`;`y2`;`y3`;`y4`;`&2`;`&2`];
  REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM;EXTENSION;IN_INTER;NOT_IN_EMPTY;IN_REAL_INTERVAL;IN_ELIM_THM];
  ANTS_TAC;
    REWRITE_TAC[arith `&0 <= &0`;NOT_FORALL_THM];
    BY(ASM_MESON_TAC[]);
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `z1` EXISTS_TAC;
  ASM_REWRITE_TAC[];
  CONJ_TAC;
    REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
    BY(ASM_MESON_TAC[]);
  INTRO_TAC taud_minimizer_cases [`&2`;`&2 * h0`;`&0`;`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
  REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM;EXTENSION;IN_INTER;NOT_IN_EMPTY;IN_REAL_INTERVAL;IN_ELIM_THM];
  ANTS_TAC;
    BY(ASM_MESON_TAC[arith `&0 <= &2 /\ &0 <= &0`;arith `&2 <= y ==> &0 <= y`]);
  ASM_CASES_TAC `z1 = &2` THEN FIRST_ASSUM (unlist REWRITE_TAC);
  ASM_CASES_TAC `&0 = delta_y z1 y2 y3 y4 (&2) (&2)` THEN FIRST_ASSUM (unlist ASM_REWRITE_TAC);
  ASM_CASES_TAC `z1 = &2 * h0` THEN ASM_REWRITE_TAC[];
    INTRO_TAC (UNDISCH OWZLKVY4 ) [`y1`;`y2`;`y3`;`y4`;`&2`;`&2`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC);
    FIRST_X_ASSUM (C INTRO_TAC [`y1`]);
    ANTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    ASM_REWRITE_TAC[];
    FIRST_X_ASSUM_ST `taum` MP_TAC;
    INTRO_TAC taud_2h0 [`y2`;`y3`;`y4`;`&2`;`&2`];
    ANTS_TAC;
      BY(ASM_MESON_TAC[]);
    BY(REAL_ARITH_TAC);
  COMMENT "derviative cases";
  ASM_CASES_TAC `~(delta_y z1 y2 y3 y4 (&2) (&2) < &15)`;
    REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC (Terminal.get_main_nonlinear "6877738680") [`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
    REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC Functional_equation.taud_x_taud;
    INTRO_TAC (UNDISCH OWZLKVY4) [`y1`;`y2`;`y3`;`y4`;`&2`;`&2`];
    ANTS_TAC;
      BY(ASM_REWRITE_TAC[Sphere.cstab]);
    FIRST_X_ASSUM (C INTRO_TAC [`y1`]);
    ANTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  INTRO_TAC (Terminal.get_main_nonlinear "9692636487") [`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  BY(REPEAT (FIRST_X_ASSUM_ST `delta_y` MP_TAC) THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

(* next, de-symmetrize everything, 
    then combine delta ranges.  *)

let REAL_WLOG_S3_SIMPLEX = 
prove_by_refinement(
  `!(P:A->A->A->real->real->real->bool). (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6 = P y3 y1 y2 y6 y4 y5 /\
      P y1 y2 y3 y4 y5 y6 = P y2 y1 y3 y5 y4 y6) /\
    (!y1 y2 y3 y4 y5 y6. y4 <= y6 /\ y6 <= y5 ==> P y1 y2 y3 y4 y5 y6) ==>
    (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `(y4 <= y5 /\ y5 <= y6) \/ (y4 <= y6 /\ y6 <= y5) \/ (y5 <= y4 /\ y4 <= y6) \/ (y5 <= y6 /\ y6 <= y4) \/ (y6 <= y5 /\ y5 <= y4) \/ (y6 <= y4 /\ y4 <= y5)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REAL_ARITH_TAC);
  BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let REAL_WLOG_AAB_SIMPLEX = 
prove_by_refinement(
  `!(P:A->A->A->real->real->real->bool). (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6 = P y3 y2 y1 y6 y5 y4) /\
    (!y1 y2 y3 y4 y5 y6. y4 <= y6 ==> P y1 y2 y3 y4 y5 y6) ==>
    (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `(y4 <= y6 \/ y6 <= y4)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REAL_ARITH_TAC);
  BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let REAL_WLOG_ABB_SIMPLEX = 
prove_by_refinement(
  `!(P:A->A->A->real->real->real->bool). (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6 = P y1 y3 y2 y4 y6 y5) /\
    (!y1 y2 y3 y4 y5 y6. y6 <= y5 ==> P y1 y2 y3 y4 y5 y6) ==>
    (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,

  (* {{{ proof *)
  [
  REPEAT WEAK_STRIP_TAC;
  TYPIFY `(y5 <= y6 \/ y6 <= y5)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REAL_ARITH_TAC);
  BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_MESON_TAC[])
  ]);;
  (* }}} *)

 
let delta_y_hex_cases = 
prove_by_refinement(
  `!y1 y2 y3 y5 y6 a b.     (delta_y y1 y2 a (&2) (&2) y6 = delta_y a y1 y2 y6 (&2) (&2) /\
          (delta_y y1 b y3 (&2) y5 (&2) = delta_y b y1 y3 y5 (&2) (&2)))`,

  (* {{{ proof *)
  [
  BY(MESON_TAC[Merge_ineq.delta_y_sym])
  ]);;
  (* }}} *)

let delta_y_sym_cases2 = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6 a.     delta_y a y3 y1 y5 (&2) (&2) = delta_y a y1 y3 y5 (&2) (&2) /\
          delta_y a y3 y2 y4 (&2) (&2) = delta_y a y2 y3 y4 (&2) (&2) /\
          delta_y a y2 y1 y6 (&2) (&2) = delta_y a y1 y2 y6 (&2) (&2)`,

  (* {{{ proof *)
  [
  BY(MESON_TAC[Merge_ineq.delta_y_sym])
  ]);;
  (* }}} *)

let taum_sym_cases2 = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. taum y2 y1 y3 y5 y4 y6 = taum y1 y2 y3 y4 y5 y6 /\
    taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6 /\
    taum y3 y1 y2 y6 y4 y5 = taum y1 y2 y3 y4 y5 y6 /\
    taum y3 y2 y1 y6 y5 y4 = taum y1 y2 y3 y4 y5 y6`,

  (* {{{ proof *)
  [
  BY(MESON_TAC[Terminal.taum_sym])
  ]);;
  (* }}} *)

let edge2_flatD_sym = 
prove_by_refinement(
  `!d y1 y2 y3 a. edge2_flatD_x1 d y1 y2 y3 a a = edge2_flatD_x1 d y2 y1 y3 a a`,

  (* {{{ proof *)
  [
  BY(REWRITE_TAC[Nonlin_def.edge2_flatD_x1;Merge_ineq.delta_x_sym])
  ]);;
  (* }}} *)

let edge2_flatD_x1_sym_cases = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. 
    edge2_flatD_x1 (&0) (y3 * y3) (y2 * y2) (y4*y4) (&2 * &2) (&2* &2) = 
    edge2_flatD_x1 (&0) (y2 * y2) (y3 * y3) (y4*y4) (&2 * &2) (&2* &2) /\
    edge2_flatD_x1 (&0) (y3 * y3) (y1 * y1) (y5*y5) (&2 * &2) (&2* &2) = 
    edge2_flatD_x1 (&0) (y1 * y1) (y3 * y3) (y5*y5) (&2 * &2) (&2* &2) /\
    edge2_flatD_x1 (&0) (y2 * y2) (y1 * y1) (y6*y6) (&2 * &2) (&2* &2) = 
    edge2_flatD_x1 (&0) (y1 * y1) (y2 * y2) (y6*y6) (&2 * &2) (&2* &2)
`,

  (* {{{ proof *)
  [
BY(REWRITE_TAC[edge2_flatD_sym])
  ]);;
  (* }}} *)

let eulerA_x_sym_cases = 
prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6.
     eulerA_x (y2 * y2) (y1 * y1) (y3 * y3) (y5 * y5) (y4 * y4) (y6 * y6) =
   eulerA_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6)  /\
   eulerA_x (y3 * y3) (y1 * y1) (y2 * y2) (y6 * y6) (y4 * y4) (y5 * y5)  =
   eulerA_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6)  /\
   eulerA_x (y3 * y3) (y2 * y2) (y1 * y1) (y6 * y6) (y5 * y5) (y4 * y4)  =
   eulerA_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6)  /\
   eulerA_x (y1 * y1) (y3 * y3) (y2 * y2) (y4 * y4) (y6 * y6) (y5 * y5)  =
   eulerA_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6)   `,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.eulerA_x];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let mu_y_sym = 
prove_by_refinement(
  `!y1 y2 y3. mu_y y1 y2 y3 = mu_y y1 y3 y2`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.mu_y];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let mu_y_sym_cases = 
prove_by_refinement(
  `!y1 y2 y3. mu_y (&2) (sqrt(y2 * y2)) (sqrt(y1*y1)) = 
 mu_y (&2) (sqrt(y1 * y1)) (sqrt(y2*y2)) /\ 
 mu_y (&2) (sqrt(y3 * y3)) (sqrt(y2*y2)) = 
 mu_y (&2) (sqrt(y2 * y2)) (sqrt(y3*y3)) /\ 
 mu_y (&2) (sqrt(y3 * y3)) (sqrt(y1*y1)) = 
 mu_y (&2) (sqrt(y1 * y1)) (sqrt(y3*y3)) 
`,

  (* {{{ proof *)
  [
    BY(REWRITE_TAC[mu_y_sym])
  ]);;
  (* }}} *)

let nonfunctional_mud_126 = 
prove_by_refinement(
  `! a b c y1 y2 y3 y4 y5 y6. y_of_x (mud_126_x_v1 a b c) y1 y2 y3 y4 y5 y6 = 
    mu_y a (sqrt(y1 * y1)) (sqrt(y2 * y2))  * sqrt(delta_y a y1 y2 y6 b c)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.mud_126_x;];
  Functional_equation.F_REWRITE_TAC;
  REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_126_x;GSYM Sphere.delta_y];
  BY(MESON_TAC[Merge_ineq.delta_y_sym])
  ]);;
  (* }}} *)

let nonfunctional_mud_234 = 
prove_by_refinement(
  `! a b c y1 y2 y3 y4 y5 y6. y_of_x (mud_234_x_v1 a b c) y1 y2 y3 y4 y5 y6 = 
    mu_y a (sqrt(y2 * y2)) (sqrt(y3 * y3))  * sqrt(delta_y a y2 y3 y4 b c)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.mud_234_x;];
  Functional_equation.F_REWRITE_TAC;
  REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_234_x;GSYM Sphere.delta_y];
  ]);;
  (* }}} *)

let nonfunctional_mud_135 = 
prove_by_refinement(
  `! a b c y1 y2 y3 y4 y5 y6. y_of_x (mud_135_x_v1 a b c) y1 y2 y3 y4 y5 y6 = 
    mu_y a (sqrt(y1 * y1)) (sqrt(y3 * y3))  * sqrt(delta_y a y1 y3 y5 b c)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.mud_135_x;];
  Functional_equation.F_REWRITE_TAC;
  REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_135_x;GSYM Sphere.delta_y];
  REWRITE_TAC[mu_y_sym];
  BY(MESON_TAC[Merge_ineq.delta_y_sym])
  ]);;
  (* }}} *)

let nonfunctional_flat_term2_126 = 
prove_by_refinement(
  `! d a b x1 x2 x3 x4 x5 x6. (flat_term2_126_x d a b) x1 x2 x3 x4 x5 x6 = 
   flat_term (sqrt (edge2_flatD_x1 d x1 x2 x6 a b))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.flat_term2_126_x];
  BY(REWRITE_TAC[Functional_equation.uni;Sphere.flat_term_x;Nonlin_def.edge2_126_x;Functional_equation.constant6;Functional_equation.proj_x1;Functional_equation.proj_x2;Functional_equation.proj_x6;Functional_equation.compose6])
  ]);;
  (* }}} *)

let nonfunctional_flat_term2_234 = 
prove_by_refinement(
  `! d a b x1 x2 x3 x4 x5 x6. (flat_term2_234_x d a b) x1 x2 x3 x4 x5 x6 = 
   flat_term (sqrt (edge2_flatD_x1 d x2 x3 x4 a b))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.flat_term2_234_x];
  BY(REWRITE_TAC[Functional_equation.uni;Sphere.flat_term_x;Nonlin_def.edge2_234_x;Functional_equation.constant6;Functional_equation.proj_x2;Functional_equation.proj_x3;Functional_equation.proj_x4;Functional_equation.compose6])
  ]);;
  (* }}} *)

let nonfunctional_flat_term2_135 = 
prove_by_refinement(
  `! d a b x1 x2 x3 x4 x5 x6. (flat_term2_135_x d a b) x1 x2 x3 x4 x5 x6 = 
   flat_term (sqrt (edge2_flatD_x1 d x1 x3 x5 a b))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.flat_term2_135_x];
  BY(REWRITE_TAC[Functional_equation.uni;Sphere.flat_term_x;Nonlin_def.edge2_135_x;Functional_equation.constant6;Functional_equation.proj_x1;Functional_equation.proj_x3;Functional_equation.proj_x5;Functional_equation.compose6])
  ]);;
  (* }}} *)

let nonfunctional_mudLs_126 = 
prove_by_refinement(
  `! y1 y2 x3 x4 x5 y6. mudLs_126_x (&4) (&10) (&2) (&2) (&2) (y1*y1) (y2*y2) x3 x4 x5 (y6*y6) = 
   mu_y (&2) (sqrt (y1 * y1)) (sqrt (y2 * y2)) *
     (&1 / &14 * (delta_y (&2) y1 y2 y6 (&2) (&2) - &16) + &4)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.mudLs_126_x];
  Functional_equation.F_REWRITE_TAC;
  REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_126_x;GSYM Sphere.delta_y;delta_y_hex_cases];
  REWRITE_TAC[arith `&4 * &4 = &16`;arith `&4 + &10 = &14`];
  TYPIFY `sqrt(&2 * &2) = &2` (C SUBGOAL_THEN SUBST1_TAC);
    GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
    BY(REAL_ARITH_TAC);
  BY(REWRITE_TAC[])
  ]);;
  (* }}} *)

let nonfunctional_mudLs_234 = 
prove_by_refinement(
  `! x1 y2 y3 y4 x5 x6. mudLs_234_x (&4) (&10) (&2) (&2) (&2) x1 (y2*y2) (y3*y3) (y4*y4) x5 x6 = 
   mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) *
     (&1 / &14 * (delta_y (&2) y2 y3 y4 (&2) (&2) - &16) + &4)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.mudLs_234_x];
  Functional_equation.F_REWRITE_TAC;
  REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_234_x;GSYM Sphere.delta_y;delta_y_hex_cases];
  REWRITE_TAC[arith `&4 * &4 = &16`;arith `&4 + &10 = &14`];
  TYPIFY `sqrt(&2 * &2) = &2` (C SUBGOAL_THEN SUBST1_TAC);
    GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
    BY(REAL_ARITH_TAC);
  BY(REWRITE_TAC[])
  ]);;
  (* }}} *)

let nonfunctional_mudLs_135 = 
prove_by_refinement(
  `! y1 x2 y3 x4 y5 x6. mudLs_135_x (&4) (&10) (&2) (&2) (&2) (y1*y1) x2 (y3*y3) x4 (y5*y5) x6 =
   mu_y (&2) (sqrt (y1 * y1)) (sqrt (y3 * y3)) *
     (&1 / &14 * (delta_y (&2) y1 y3 y5 (&2) (&2) - &16) + &4)`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Nonlin_def.mudLs_135_x];
  Functional_equation.F_REWRITE_TAC;
  REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_135_x;GSYM Sphere.delta_y;delta_y_hex_cases];
  REWRITE_TAC[arith `&4 * &4 = &16`;arith `&4 + &10 = &14`];
  TYPIFY `sqrt(&2 * &2) = &2` (C SUBGOAL_THEN SUBST1_TAC);
    GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
    BY(REAL_ARITH_TAC);
  BY(REWRITE_TAC[])
  ]);;
  (* }}} *)

let ineq_sym_s3 = 
prove_by_refinement(
  `!y4 y5 y6 p r . 
      ineq p (r \/ y6 < y4 \/ y5 < y6) ==>
   ((y4 <= y6 /\ y6 <= y5) ==> ineq p r)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `ineq` MP_TAC;
  BY(ASM_SIMP_TAC [arith `x <= y ==> ~(y < x)`])
  ]);;
  (* }}} *)

let ineq_sym_s2_aab = 
prove_by_refinement(
  `!y4 y6 p r. ineq p (r \/ y6 < y4) ==>
    ((y4 <= y6) ==> ineq p r)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `ineq` MP_TAC;
  BY(ASM_SIMP_TAC [arith `x <= y ==> ~(y < x)`])
  ]);;
  (* }}} *)

let ineq_sym_s2_abb = 
prove_by_refinement(
  `!y5 y6 p r. ineq p (r \/ y5 < y6) ==>
    ((y6 <= y5) ==> ineq p r)`,

  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  FIRST_X_ASSUM_ST `ineq` MP_TAC;
  BY(ASM_SIMP_TAC [arith `x <= y ==> ~(y < x)`])
  ]);;
  (* }}} *)

let clean_ineq = PURE_REWRITE_RULE[Sphere.y_of_x;Sphere.delta_234_x;Sphere.delta_126_x;Sphere.delta_135_x;
  arith `#2.52 pow 2 = #2.52 * #2.52 /\ &4 = &2 * &2`;GSYM Sphere.delta_y;delta_y_hex_cases;
  nonfunctional_mud_126;nonfunctional_mud_234;nonfunctional_mud_135;
  nonfunctional_flat_term2_126;  nonfunctional_flat_term2_234;  nonfunctional_flat_term2_135;
  nonfunctional_mudLs_135 ;nonfunctional_mudLs_126 ;nonfunctional_mudLs_234];;

let mk_ineq_hex conv i234 i126 i135 = 
  let nth = List.nth in
  let d234 = nth [`   y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `;
		  `&0`;
          `y_of_x (mud_234_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;  
          `y_of_x (mudLs_234_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;  
	  `&0 - sol0`] i234 in
  let d126 = nth [`   y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `;
		  `&0`;
          `y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;  
          `y_of_x (mudLs_126_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;  
	  `&0 - sol0`] i126 in
  let d135 = nth [`   y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `;
		  `&0`;
          `y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;  
          `y_of_x (mudLs_135_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;  
	  `&0 - sol0`] i135 in
  let c234 = nth [`y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ 
		    y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`;
		  `F`;
		      `y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`;
		      `y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/
			y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`;
		      `y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
			y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i234 in
  let c126 = nth [`y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ 
		    y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`;
		  `F`;
		      `y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`;
		      `y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/
			y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`;
		      `y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
			y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i126 in
  let c135 = nth [`y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/ 
		    y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`;
		  `F`;
		      `y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`;
		      `y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/
			y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`;
		      `y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
			y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i135 in
  let s45 = if (i234= i126) then `y6 < y4` else `F` in
  let s56 = if (i126= i135) then `y5 < y6` else `F` in
 rhs(concl(conv (Ineq.mk_tplate Main_estimate_ineq.template_hex [d234;d126;d135;c234;c126;c135;s45;s56])));;

(*
let tmgg a b c = 
  let g = mk_ineq_hex (PURE_REWRITE_CONV[]) a b c in
  let g' =  (mk_imp (`main_nonlinear_terminal_v11`,concl (clean_ineq (ASSUME g)))) in
    g';;
*)

let get_ineq (a,b,c) = 
  clean_ineq  (Terminal.get_main_nonlinear (Printf.sprintf "7550003505 %d %d %d" a b c));;

let get_ineq_term(a,b,c) = 
  let g = mk_ineq_hex (PURE_REWRITE_CONV[]) a b c in
    concl (clean_ineq (ASSUME g));;

let get_ineq'(a,b,c) = 
  let g' = mk_imp(`main_nonlinear_terminal_v11`,get_ineq_term(a,b,c)) in
    repeat UNDISCH (prove_by_refinement(g',[					
        DISCH_TAC;
  BY(REWRITE_TAC[get_ineq(a,b,c)])]));;

let r755_0 i = 
  let (yys,tm) =  (strip_forall (concl(get_ineq' (i,i,i)))) in
  let tm0 = rhs(concl(PURE_REWRITE_CONV [ASSUME (`y6 < y4 <=> F`);ASSUME (`y5 < y6 <=> F`)] tm)) in
  let tm1 = list_mk_forall (yys, tm0) in
  let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in
prove_by_refinement(tm2,
  (* {{{ proof *)
  [
  DISCH_TAC;
  MATCH_MP_TAC REAL_WLOG_S3_SIMPLEX;
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC delta_y_sym_cases2 yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC taum_sym_cases2 yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC edge2_flatD_x1_sym_cases yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC eulerA_x_sym_cases yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`];
    DISCH_THEN (unlist REWRITE_TAC);
    TYPIFY_GOAL_THEN `!f. f y1 y2 y6 + f y1 y3 y5 + f y2 y3 y4 = f y2 y3 y4 + f y1 y2 y6 + f y1 y3 y5 /\ f y1 y3 y5 + f y1 y2 y6 + f y2 y3 y4 = f y2 y3 y4 + f y1 y2 y6 + f y1 y3 y5` (unlist ONCE_REWRITE_TAC);
      BY(REAL_ARITH_TAC);
    BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[]);
  REPEAT GEN_TAC;
  MATCH_MP_TAC ineq_sym_s3;
  INTRO_TAC (get_ineq(i,i,i)) yys;
  BY(REWRITE_TAC[TAUT `(a \/ b) \/ c <=> a \/ b \/ c`])
  ]);;
  (* }}} *)

let r755_diag = map (fun i -> (i, r755_0 i)) [0;1;2;3;4];;


let r755_aab i j= 
  let (yys,tm) =  (strip_forall (concl(get_ineq' (i,i,j)))) in
  let tm0 = rhs(concl(PURE_REWRITE_CONV [ASSUME (`(y6 < y4) <=> F`)] tm)) in
  let tm1 = list_mk_forall (yys, tm0) in
  let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in
prove_by_refinement(tm2,
  (* {{{ proof *)
  [
  DISCH_TAC;
  MATCH_MP_TAC REAL_WLOG_AAB_SIMPLEX;
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC delta_y_sym_cases2 yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC taum_sym_cases2 yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC edge2_flatD_x1_sym_cases yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC eulerA_x_sym_cases yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`];
    DISCH_THEN (unlist REWRITE_TAC);
    TYPIFY_GOAL_THEN `!f b. f y1 y2 y6 + f y2 y3 y4 + b = f y2 y3 y4 + f y1 y2 y6 + b` (unlist ONCE_REWRITE_TAC);
      BY(REAL_ARITH_TAC);
    BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[]);
  REPEAT GEN_TAC;
  MATCH_MP_TAC ineq_sym_s2_aab;
  INTRO_TAC (get_ineq(i,i,j)) yys;
  BY(REWRITE_TAC[TAUT `(a \/ b) \/ c <=> a \/ b \/ c`])
  ]);;
  (* }}} *)

let r755_aab_list = map (fun (i,j) -> ((i,j),r755_aab i j)) [(0,1);(0,2);(0,3);(0,4);(1,2);(1,3);(1,4);
						      (2,3);(2,4);(3,4)];;

let r755_abb i j= 
  let (yys,tm) =  (strip_forall (concl(get_ineq' (i,j,j)))) in
  let tm0 = rhs(concl(PURE_REWRITE_CONV [ASSUME (`(y5 < y6) <=> F`)] tm)) in
  let tm1 = list_mk_forall (yys, tm0) in
  let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in
prove_by_refinement(tm2,
  (* {{{ proof *)
  [
  DISCH_TAC;
  MATCH_MP_TAC REAL_WLOG_ABB_SIMPLEX;
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    INTRO_TAC delta_y_sym_cases2 yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC taum_sym_cases2 yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC edge2_flatD_x1_sym_cases yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC eulerA_x_sym_cases yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`];
    DISCH_THEN (unlist REWRITE_TAC);
    TYPIFY_GOAL_THEN `!f. f y1 y2 y6 + f y1 y3 y5 = f y1 y3 y5 + f y1 y2 y6` (unlist ONCE_REWRITE_TAC);
      BY(REAL_ARITH_TAC);
    BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[]);
  REPEAT GEN_TAC;
  MATCH_MP_TAC ineq_sym_s2_abb;
  INTRO_TAC (get_ineq(i,j,j)) yys;
  BY(REWRITE_TAC[TAUT `(a \/ b) \/ c <=> a \/ b \/ c`])
  ]);;
  (* }}} *)

let r755_abb_list = map (fun (i,j) -> ((i,j),r755_abb i j)) [(0,1);(0,2);(0,3);(0,4);(1,2);(1,3);(1,4);
						      (2,3);(2,4);(3,4)];;

let get_ineq2( i, j, k) =
  let _ = (i <= j && j <= k) or failwith "get2 out of range" in
    if (i = j && j = k) then UNDISCH (assoc i r755_diag)
    else if (i = j) then UNDISCH (assoc (i,k) r755_aab_list)
    else if (j = k) then UNDISCH (assoc (i,j) r755_abb_list)
    else get_ineq'(i,j,k);;

(*
let tmg i j = 
  let (yys,tm) =  (strip_forall (concl(get_ineq (i,j,j)))) in
  let tm0 = rhs(concl(REWRITE_CONV [ASSUME (`~(y5 < y6) /\ ~(y6 < y4)`)] tm)) in
  let tm1 = list_mk_forall (yys, tm0) in
  let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in
    tm2;;
*)

let g755_ i j k = 
(*  let inq = (Main_estimate_ineq.make_hex_ear i j k).ineq in
  let inq' = concl(clean_ineq (ASSUME inq)) in
*)
  let inq' = get_ineq_term (i,j,k) in
  let (yys,tm) =  strip_forall inq' in 
  let tm0 = rhs(concl(PURE_REWRITE_CONV [ASSUME `(y5 < y6) <=> F`;ASSUME `(y6 < y4) <=> F`] tm)) in
  let tm1 = list_mk_forall (yys, tm0) in
  let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in
    tm2;;

let r755_ikj getter i j k  = prove_by_refinement(
  (g755_ i j k),
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC ( (getter (i, k, j))) [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
    INTRO_TAC delta_y_sym_cases2 yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC taum_sym_cases2 yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC edge2_flatD_x1_sym_cases yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC eulerA_x_sym_cases yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`];
    DISCH_THEN (unlist REWRITE_TAC);
  REWRITE_TAC[REAL_ADD_AC];
  BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[])
  ]);;
  (* }}} *)

let rec cross a = function
  | [] -> []
  | b::bs -> (map (fun i -> (i,b)) a) @ cross a bs;;

let triples = map (fun ((i,j),k)-> (i,j,k)) (cross (cross (0--4) (0--4)) (0--4));;

let r755_ikj_list = 
  let ls = map (fun (i,j,k) -> ((i,j,k),
		  if (i > j or i > k) then TRUTH
		  else if (j<= k) then get_ineq2 (i,j,k)
		  else r755_ikj get_ineq2 i j k))  in
		  ls triples;;

let get_ineq3( i, j, k) =
  let _ = (i <= j && i <= k) or failwith (Printf.sprintf "get3 out of range %d %d %d" i j k) in
    repeat UNDISCH (assoc (i,j,k) r755_ikj_list);;

let r755_jik i j k  = prove_by_refinement(
  (g755_ i j k),
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC ( (get_ineq3 (j, i, k))) [`y3`;`y2`;`y1`;`y6`;`y5`;`y4`];
    INTRO_TAC delta_y_sym_cases2 yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC taum_sym_cases2 yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC edge2_flatD_x1_sym_cases yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC eulerA_x_sym_cases yys;
    DISCH_THEN (unlist REWRITE_TAC);
    INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`];
    DISCH_THEN (unlist REWRITE_TAC);
  REWRITE_TAC[REAL_ADD_AC];
  BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[])
  ]);;
  (* }}} *)

let r755_jik_list = 
  let ls = map (fun (i,j,k) -> ((i,j,k),
		  if (k < i && k < j) then TRUTH
		  else if (i<= j) then get_ineq3 (i,j,k)
		  else r755_jik i j k))  in
		  ls triples;;
	 
let get_ineq4( i, j, k) =
  let thm =     repeat UNDISCH (assoc (i,j,k) r755_jik_list) in
  let _ = (not(thm = TRUTH)) or failwith (Printf.sprintf "get4 out of range %d %d %d" i j k) in
    thm;;

	 
let get_ineq5 =
  let ls = map (fun (i,j,k) -> ((i,j,k),
				if (k < i && k < j) then r755_ikj get_ineq4 i j k
				else get_ineq4 (i,j,k))) in
  let r755_ikj_list2 = ls triples in
    fun ( i, j, k) ->
      repeat UNDISCH (assoc (i,j,k) r755_ikj_list2);;

(*
let _ = (125 = List.length (filter (fun t -> not (snd t = TRUTH)) r755_ikj_list2));;
*)

let taud_mu_clauses = 
prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> (!y2 y3 y4.
    (&2 <= y2 /\ y2 <= #2.52 /\ &2 <= y3 /\ y3 <= #2.52 /\ #3.01 <= y4 /\ y4 <= #3.915) ==>
    (let d = delta_y (&2) y2 y3 y4 (&2) (&2) in
     let t = taud (&2) y2 y3 y4 (&2) (&2) in
       ((&0 <= d /\ d <= &16 ==> -- sol0 <= t) /\
	  (&16 <= d /\ d <= &100 ==> mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) *
      (&1 / &14 * (delta_y (&2) y2 y3 y4 (&2) (&2) - &16) + &2 * &2) -
      sol0 <= t) /\
	  (&100 <= d ==> mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) *
      sqrt (delta_y (&2) y2 y3 y4 (&2) (&2)) -
      sol0 <= t))))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[LET_DEF;LET_END_DEF];
  REPEAT WEAKER_STRIP_TAC;
  CONJ_TAC;
    DISCH_TAC;
    INTRO_TAC (taud_ge_flat_term) [`&2`;`y2`;`y3`;`y4`;`&2`;`&2`];
    ANTS_TAC;
      BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab;Sphere.h0] THEN REAL_ARITH_TAC);
    BY(REWRITE_TAC[flat_term_2]);
  CONJ_TAC;
    REPEAT WEAKER_STRIP_TAC;
    REWRITE_TAC[Nonlin_def.taud;GSYM Nonlin_def.mu_y;GSYM Sphere.flat_term;flat_term_2];
    GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
    GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
    ASM_SIMP_TAC[arith `&2 <= y ==> &0 <= y`];
    TYPED_ABBREV_TAC `d = delta_y (&2) y2 y3 y4 (&2) (&2)`;
    MATCH_MP_TAC (arith `m* a <= m * a' ==> m * a - s <= --s + a' * m`);
    GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP;
    CONJ_TAC;
      REWRITE_TAC[Nonlin_def.mu_y];
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    TYPIFY `&2 * &2 = sqrt(&16)` (C SUBGOAL_THEN SUBST1_TAC);
      MATCH_MP_TAC Upfzbzm_support_lemmas.SQRT_RULE_Euler_lemma;
      BY(REAL_ARITH_TAC);
    TYPIFY `&14 = sqrt(&16) + sqrt(&100)` (C SUBGOAL_THEN SUBST1_TAC);
      TYPIFY `&4 = sqrt(&16) /\ &10 = sqrt(&100)` ENOUGH_TO_SHOW_TAC;
        BY(REAL_ARITH_TAC);
      CONJ_TAC;
        MATCH_MP_TAC Upfzbzm_support_lemmas.SQRT_RULE_Euler_lemma;
        BY(REAL_ARITH_TAC);
      MATCH_MP_TAC Upfzbzm_support_lemmas.SQRT_RULE_Euler_lemma;
      BY(REAL_ARITH_TAC);
    MATCH_MP_TAC sqrt_secant_approx;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  COMMENT "final case";
  GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
  GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
  ASM_SIMP_TAC[arith `&2 <= y ==> &0 <= y`];
  DISCH_TAC;
  REWRITE_TAC[Nonlin_def.taud;GSYM Nonlin_def.mu_y;GSYM Sphere.flat_term;flat_term_2];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let terminal_hex_234_reduction = 
prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y234 f1 f2 b1 b2.  
    (let dom = [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52;  #3.01,y4, #3.915; 
          #3.01,
         y5,
          #3.915;  #3.01,y6, #3.915] in 
       (ineq dom (f1 + flat_term
          (sqrt
          (edge2_flatD_x1 (&0) (y2 * y2) (y3 * y3) (y4 * y4) (&2 * &2)
          (&2 * &2))) + f2 > #0.712 \/ b1 \/ (delta_y (&2) y2 y3 y4 (&2) (&2) < &0 \/
           delta_y  #2.52 y2 y3 y4 (&2) (&2) > &0) \/ b2)) /\
(ineq dom (f1 + &0 + f2 > #0.712 \/ b1 \/ F \/ b2)) /\
(ineq dom (f1 + (
          mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) *
          sqrt (delta_y (&2) y2 y3 y4 (&2) (&2)) -
          sol0) + f2 > #0.712 \/ b1 \/ delta_y (&2) y2 y3 y4 (&2) (&2) < &100 \/ b2)) /\
(ineq dom (f1 + (          mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) *
          (&1 / &14 * (delta_y (&2) y2 y3 y4 (&2) (&2) - &16) + &2 * &2) -
          sol0) + f2 > #0.712 \/ 
   b1 \/ (delta_y (&2) y2 y3 y4 (&2) (&2) < &16 \/
           delta_y (&2) y2 y3 y4 (&2) (&2) > &100) \/ b2)) /\
(ineq dom (f1 + ( &0 - sol0) + f2 > #0.712 \/ 
	     b1 \/ (delta_y (&2) y2 y3 y4 (&2) (&2) < &0 \/
           delta_y (&2) y2 y3 y4 (&2) (&2) > &16) \/ b2))) ==>
    (ineq [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52;  #3.01,y4, #3.915; 
          #3.01,
         y5,
          #3.915;  #3.01,y6, #3.915;&2,y234,#2.52] ((f1 + taum y234 y2 y3 y4 (&2) (&2)) +  f2 > #0.712 \/
	   (delta_y y234 y2 y3 y4 (&2) (&2) < &0 \/ b1) \/ b2)))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF];
  REPEAT WEAKER_STRIP_TAC;
  REPEAT (FIRST_X_ASSUM_ST `\/` MP_TAC) THEN ASM_REWRITE_TAC[];
  ASM_CASES_TAC `b1:bool`;
    BY(ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  ASM_CASES_TAC `b2:bool`;
    BY(ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  REWRITE_TAC[arith `f1 + t + f2 > #0.712 <=> t > #0.712 - f1 - f2`;arith `(f1 + t) + f2 > #0.712 <=> t > #0.712 - f1 - f2`];
  TYPED_ABBREV_TAC `c = #0.712 - f1 - f2`;
  REPEAT WEAKER_STRIP_TAC;
  ASM_CASES_TAC `&0 <= taum y234 y2 y3 y4 (&2) (&2)`;
    BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  ASM_CASES_TAC `delta_y y234 y2 y3 y4 (&2) (&2) < &0`;
    BY(ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  INTRO_TAC (UNDISCH taud_minimizer_terminal_hex_cases) [`y234`;`y2`;`y3`;`y4`];
  ASM_SIMP_TAC[arith `~(d < &0) ==> &0 <= d`;arith `~(&0 <= t) ==> t < &0`];
  ANTS_TAC;
    BY(REWRITE_TAC[Sphere.h0] THEN ASM_TAC THEN REAL_ARITH_TAC);
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (UNDISCH OWZLKVY4) [`y234`;`y2`;`y3`;`y4`;`&2`;`&2`];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab;Sphere.h0] THEN REAL_ARITH_TAC);
  DISCH_TAC;
  FIRST_X_ASSUM DISJ_CASES_TAC;
    FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
    INTRO_TAC (UNDISCH taud_mu_clauses) [`y2`;`y3`;`y4`];
    ANTS_TAC;
      BY(ASM_REWRITE_TAC[]);
    REWRITE_TAC[LET_DEF;LET_END_DEF];
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REPEAT (FIRST_X_ASSUM_ST `mu_y` kill);
  INTRO_TAC taud_ge_flat_term [`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  DISCH_TAC;
  INTRO_TAC (UNDISCH edge2_flatD_x1_delta_lemma3) [`&0`;`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  DISCH_TAC;
  FIRST_X_ASSUM_ST `sqrt` MP_TAC;
  ASM_REWRITE_TAC[];
  GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
  ASM_SIMP_TAC [arith `&2 <= z1 ==> &0 <= z1`];
  INTRO_TAC (UNDISCH delta_mono) [`&2 * h0`;`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  INTRO_TAC (UNDISCH delta_2_nn) [`z1`;`y2`;`y3`;`y4`];
  ANTS_TAC;
    BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
  BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[Sphere.h0;arith `#2.52 = &2 * #1.26`] THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let mk_25 j k = 
  let get_spec i j k = ISPECL yys (get_ineq5(i,j,k)) in
  let aa i = get_spec i j k in
  let rule = PURE_REWRITE_RULE[LET_DEF;LET_END_DEF;BETA_THM] in
    GENL yys (MATCH_MP (rule (UNDISCH terminal_hex_234_reduction)) (end_itlist CONJ (map aa (0--4))));;

(*
let terminal_hex_25  = map (fun (j,k) -> mk_25 j k) (cross (0--4) (0--4));;
*)

let terminal_hex_126_reduction = 
prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y234 y126 f1 f2 b1 b2.  
    (let dom = [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52;  #3.01,y4, #3.915; 
          #3.01,
         y5,
          #3.915;  #3.01,y6, #3.915;&2,y234,#2.52 ] in 
       (ineq dom (f1 + flat_term
          (sqrt
          (edge2_flatD_x1 (&0) (y1 * y1) (y2 * y2) (y6 * y6) (&2 * &2)
          (&2 * &2))) + f2 > #0.712 \/ b1 \/ (delta_y (&2) y1 y2 y6 (&2) (&2) < &0 \/
           delta_y  #2.52 y1 y2 y6 (&2) (&2) > &0) \/ b2)) /\
(ineq dom (f1 + &0 + f2 > #0.712 \/ b1 \/ F \/ b2)) /\
(ineq dom (f1 + (
          mu_y (&2) (sqrt (y1 * y1)) (sqrt (y2 * y2)) *
          sqrt (delta_y (&2) y1 y2 y6 (&2) (&2)) -
          sol0) + f2 > #0.712 \/ b1 \/ delta_y (&2) y1 y2 y6 (&2) (&2) < &100 \/ b2)) /\
(ineq dom (f1 + (          mu_y (&2) (sqrt (y1 * y1)) (sqrt (y2 * y2)) *
          (&1 / &14 * (delta_y (&2) y1 y2 y6 (&2) (&2) - &16) + &2 * &2) -
          sol0) + f2 > #0.712 \/ 
   b1 \/ (delta_y (&2) y1 y2 y6 (&2) (&2) < &16 \/
           delta_y (&2) y1 y2 y6 (&2) (&2) > &100) \/ b2)) /\
(ineq dom (f1 + ( &0 - sol0) + f2 > #0.712 \/ 
	     b1 \/ (delta_y (&2) y1 y2 y6 (&2) (&2) < &0 \/
           delta_y (&2) y1 y2 y6 (&2) (&2) > &16) \/ b2))) ==>
    (ineq [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52;  #3.01,y4, #3.915; 
          #3.01,
         y5,
          #3.915;  #3.01,y6, #3.915;&2,y234,#2.52;&2,y126,#2.52] ((f1 + taum y126 y1 y2 y6 (&2) (&2)) +  f2 > #0.712 \/
	   (delta_y y126 y1 y2 y6 (&2) (&2) < &0 \/ b1) \/ b2)))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF];
  REPEAT WEAKER_STRIP_TAC;
  REPEAT (FIRST_X_ASSUM_ST `\/` MP_TAC) THEN ASM_REWRITE_TAC[];
  ASM_CASES_TAC `b1:bool`;
    BY(ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  ASM_CASES_TAC `b2:bool`;
    BY(ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (UNDISCH terminal_hex_234_reduction) [`y3`;`y1`;`y2`;`y6`;`y4`;`y5`;`y126`;`f1`;`f2`;`b1`;`b2`];
  BY(ASM_REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF])
  ]);;
  (* }}} *)

let mk_5 k = 
  let yys' = yys @ [`y234:real`] in
  let get_spec j k = ISPECL (yys') (mk_25 j k) in
  let aa j = get_spec j k in
  let rule = PURE_REWRITE_RULE[LET_DEF;LET_END_DEF;BETA_THM] in
    GENL yys' (MATCH_MP (rule (UNDISCH terminal_hex_126_reduction)) (end_itlist CONJ (map aa (0--4))));;

let terminal_hex_135_reduction = 
prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y234 y126 y135 f1 b1 b2.  
    (let dom = [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52;  #3.01,y4, #3.915; 
          #3.01,
         y5,
          #3.915;  #3.01,y6, #3.915;&2,y234,#2.52; &2,y126,#2.52 ] in 
       (ineq dom (f1 + flat_term
          (sqrt
          (edge2_flatD_x1 (&0) (y1 * y1) (y3 * y3) (y5 * y5) (&2 * &2)
          (&2 * &2))) > #0.712 \/ b1 \/ (delta_y (&2) y1 y3 y5 (&2) (&2) < &0 \/
           delta_y  #2.52 y1 y3 y5 (&2) (&2) > &0) \/ b2)) /\
(ineq dom (f1 + &0  > #0.712 \/ b1 \/ F \/ b2)) /\
(ineq dom (f1 + (
          mu_y (&2) (sqrt (y1 * y1)) (sqrt (y3 * y3)) *
          sqrt (delta_y (&2) y1 y3 y5 (&2) (&2)) -
          sol0)  > #0.712 \/ b1 \/ delta_y (&2) y1 y3 y5 (&2) (&2) < &100 \/ b2)) /\
(ineq dom (f1 + (          mu_y (&2) (sqrt (y1 * y1)) (sqrt (y3 * y3)) *
          (&1 / &14 * (delta_y (&2) y1 y3 y5 (&2) (&2) - &16) + &2 * &2) -
          sol0)  > #0.712 \/ 
   b1 \/ (delta_y (&2) y1 y3 y5 (&2) (&2) < &16 \/
           delta_y (&2) y1 y3 y5 (&2) (&2) > &100) \/ b2)) /\
(ineq dom (f1 + ( &0 - sol0)  > #0.712 \/ 
	     b1 \/ (delta_y (&2) y1 y3 y5 (&2) (&2) < &0 \/
           delta_y (&2) y1 y3 y5 (&2) (&2) > &16) \/ b2))) ==>
    (ineq [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52;  #3.01,y4, #3.915; 
          #3.01,
         y5,
          #3.915;  #3.01,y6, #3.915;&2,y234,#2.52;&2,y126,#2.52;&2,y135,#2.52] ((f1 + taum y135 y1 y3 y5 (&2) (&2)) > #0.712 \/
	   (delta_y y135 y1 y3 y5 (&2) (&2) < &0 \/ b1) \/ b2)))`,

  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF];
  REPEAT WEAKER_STRIP_TAC;
  REPEAT (FIRST_X_ASSUM_ST `==>` MP_TAC) THEN ASM_REWRITE_TAC[];
  ASM_CASES_TAC `b1:bool`;
    BY(ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  ASM_CASES_TAC `b2:bool`;
    BY(ASM_REWRITE_TAC[]);
  ASM_REWRITE_TAC[];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (UNDISCH terminal_hex_234_reduction) [`y2`;`y1`;`y3`;`y5`;`y4`;`y6`;`y135`;`f1`;`&0`;`b1`;`b2`];
  ASM_REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF];
  RULE_ASSUM_TAC (REWRITE_RULE[arith `a + &0 = a`]);
  BY(ASM_REWRITE_TAC[arith `a + &0 = a`])
  ]);;
  (* }}} *)

let terminal_hex_taum  = 
  let yys' = (yys @ [`y234:real`;`y126:real`]) in
  let aa k = ISPECL yys' (mk_5 k) in
  let rule1 = PURE_REWRITE_RULE[LET_DEF;LET_END_DEF;BETA_THM] in
  let rule2 = REWRITE_RULE[REAL_ADD_AC] in
    GENL yys' (rule2(MATCH_MP (rule1 (UNDISCH terminal_hex_135_reduction)) (end_itlist CONJ (map aa (0--4)))));;

end;;