text_formalization/local/pent_hex.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (* Section: Main Estimate - Appendix - Terminal Cases                         *)
   4 (* Chapter: Local Fan                                                         *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2013-05-10                                                           *)
   7 (* ========================================================================== *)
   8
   9 (* Terminal Pent and Hex cases.  *)
  10
  11 (* pent with 5 top edges=2 *)
  12
  13
  14
  15
  16 module Pent_hex = struct
  17
  18
  19   open Hales_tactic;;
  20
  21 (* eventually combine this with the one in Appendix. *)
  22
  23 (*
  24 let pent_hex_get_main_nonlinear =
  25   let is_main = function
  26     | Main_estimate -> true
  27     | _ -> false in
  28   let has_main ind =
  29     exists (is_main) ind.tags in
  30   let main_ineq_data1 =
  31     filter has_main (!Ineq.ineqs) in
  32   let id = map (fun t-> t.idv) main_ineq_data1 in
  33   let main_ineq_data = map (fun t -> hd(Ineq.getexact t)) id in
  34   let ineql = map (fun ind -> ind.ineq) main_ineq_data in
  35   let sl = map (fun ind -> ind.idv) main_ineq_data in
  36   let main_ineq_conj = end_itlist (curry mk_conj) ineql in
  37   let th = new_definition (mk_eq (`main_nonlinear_terminal_v11:bool`,main_ineq_conj)) in
  38   let th1 = UNDISCH (MATCH_MP (TAUT `(a <=> b) ==> (a ==> b)`) th) in
  39   let co1 thm = if (is_conj (concl thm)) then CONJUNCT1 thm else thm in
  40   let tryindex s sl = try index s sl with  _ -> report s; failwith s in
  41     fun s ->
  42       let i = tryindex s sl in
  43       let th2 = funpow i CONJUNCT2 th1 in
  44         co1 th2;;
  45 *)
  46
  47
  48 let UNDISCH2 = repeat UNDISCH;;
  49
  50 let yys = [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`];;
  51
  52
  53 let sqrt_secant_approx = prove_by_refinement(
  54   `!x1 x2 x.  &0 <= x1 /\ x1 <= x /\ x <= x2 ==>
  55     (&1 / (sqrt(x1) + sqrt(x2))) * (x - x1) + sqrt(x1) <= sqrt(x)`,
  56   (* {{{ proof *)
  57   [
  58   REPEAT WEAKER_STRIP_TAC;
  59   ASM_CASES_TAC `x2 = &0`;
  60     TYPIFY `x1 = &0 /\ x = &0` (C SUBGOAL_THEN ASSUME_TAC);
  61       BY(ASM_TAC THEN REAL_ARITH_TAC);
  62     ASM_REWRITE_TAC[];
  63     BY(REAL_ARITH_TAC);
  64   TYPIFY `&0 < sqrt x2` (C SUBGOAL_THEN ASSUME_TAC);
  65     MATCH_MP_TAC SQRT_POS_LT;
  66     BY(ASM_TAC THEN REAL_ARITH_TAC);
  67   TYPIFY `&0 <= sqrt x1` (C SUBGOAL_THEN ASSUME_TAC);
  68     MATCH_MP_TAC SQRT_POS_LE;
  69     BY(ASM_TAC THEN REAL_ARITH_TAC);
  70   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);
  71     Calc_derivative.CALC_ID_TAC;
  72     CONJ2_TAC;
  73       REWRITE_TAC[REAL_DIFFSQ];
  74       REPEAT (GMATCH_SIMP_TAC Functional_equation.sqrt_sqrt);
  75       BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
  76     BY(ASM_TAC THEN REAL_ARITH_TAC);
  77   REWRITE_TAC[arith `x + y <= z <=> x <= &1 * (z - y)`];
  78   MATCH_MP_TAC Real_ext.REAL_PROP_LE_RMUL;
  79   CONJ2_TAC;
  80     REWRITE_TAC[arith `&0 <= x - y <=> y <= x`];
  81     GMATCH_SIMP_TAC SQRT_MONO_LE_EQ;
  82     BY(ASM_TAC THEN REAL_ARITH_TAC);
  83   GMATCH_SIMP_TAC REAL_LE_LDIV_EQ;
  84   CONJ2_TAC;
  85     REWRITE_TAC[arith `&1 * x = x`;arith `x + y <= z + y <=> x <= z`];
  86     GMATCH_SIMP_TAC SQRT_MONO_LE_EQ;
  87     BY(ASM_TAC THEN REAL_ARITH_TAC);
  88   BY(ASM_TAC THEN REAL_ARITH_TAC)
  89   ]);;
  90   (* }}} *)
  91
  92 let flat_term_neg = prove_by_refinement(
  93   `!y. y <= &2 * h0 ==> flat_term y <= &0`,
  94   (* {{{ proof *)
  95   [
  96   REWRITE_TAC[Sphere.flat_term];
  97   REPEAT WEAKER_STRIP_TAC;
  98   REWRITE_TAC[arith `a * b / c <= &0 <=> &0 <= a * (--b) / c `];
  99   GMATCH_SIMP_TAC REAL_LE_MUL;
 100   GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
 101   FIRST_X_ASSUM MP_TAC;
 102   REWRITE_TAC[Sphere.h0];
 103   MP_TAC Flyspeck_constants.bounds;
 104   BY(REAL_ARITH_TAC)
 105   ]);;
 106   (* }}} *)
 107
 108 let mu_y_ft_combine = prove_by_refinement(
 109   `!y y2 y3 sd.
 110     mu_y y y2 y3 * sd + flat_term y =
 111       mu_y (&2 * h0) y2 y3 * sd + (&1 - (&2 * h0 - &2) * #0.07 * sd / sol0) * flat_term y`,
 112   (* {{{ proof *)
 113   [
 114   REWRITE_TAC[Nonlin_def.mu_y;Sphere.flat_term];
 115   REPEAT WEAKER_STRIP_TAC;
 116   Calc_derivative.CALC_ID_TAC;
 117   MP_TAC Flyspeck_constants.bounds;
 118   REWRITE_TAC[Sphere.h0];
 119   BY(REAL_ARITH_TAC)
 120   ]);;
 121   (* }}} *)
 122
 123 let mu_y_ft_combine2 = prove_by_refinement(
 124   `!y y2 y3. y <= &2 * h0 ==>
 125     mu_y (&2 * h0) y2 y3 * sqrt(&20) + #0.705 * flat_term y <=
 126     mu_y y y2 y3 * sqrt(&20) + flat_term y
 127       `,
 128   (* {{{ proof *)
 129   [
 130   REWRITE_TAC[mu_y_ft_combine];
 131   REWRITE_TAC[arith `x + y <= x + z <=> y <= z`];
 132   REPEAT WEAKER_STRIP_TAC;
 133   ONCE_REWRITE_TAC[arith `a * b = (-- a) * (-- b)`];
 134   MATCH_MP_TAC Real_ext.REAL_PROP_LE_RMUL;
 135   CONJ2_TAC;
 136     REWRITE_TAC[arith `&0 <= -- f <=> f <= &0`];
 137     BY(ASM_SIMP_TAC[flat_term_neg]);
 138   REWRITE_TAC[arith `-- x <= -- (&1 - u) <=> &1 - x <= u`];
 139   TYPIFY `#4.472135 <= sqrt(&20)` (C SUBGOAL_THEN MP_TAC);
 140     MATCH_MP_TAC REAL_LE_RSQRT;
 141     BY(REAL_ARITH_TAC);
 142   TYPIFY `#0.551285 < sol0 /\ sol0 < #0.551286` (C SUBGOAL_THEN MP_TAC);
 143     BY(REWRITE_TAC[ Flyspeck_constants.bounds]);
 144   REWRITE_TAC[Sphere.h0];
 145   REWRITE_TAC[arith `a * b * c /d = ((a * b) * c) / d`];
 146   REPEAT WEAKER_STRIP_TAC;
 147   GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
 148   CONJ_TAC;
 149     BY(ASM_TAC THEN REAL_ARITH_TAC);
 150   BY(ASM_TAC THEN REAL_ARITH_TAC)
 151   ]);;
 152   (* }}} *)
 153
 154 let nonfunctional_mu6_x = prove_by_refinement(
 155   `!x1 x2 x3 a b c. mu6_x x1 x2 x3 a b c = mu_y (sqrt x1) (sqrt x2) (sqrt x3)`,
 156   (* {{{ proof *)
 157   [
 158   REWRITE_TAC[Nonlin_def.mu6_x;Nonlin_def.mu_y;];
 159   BY(Functional_equation.F_REWRITE_TAC)
 160   ]);;
 161   (* }}} *)
 162
 163 let tau_x_tau_residual_x_general = prove_by_refinement(
 164   `!x1 x2 x3 x4 x5 x6.
 165     &4 <= x1 /\
 166     sqrt(x1) <= &2 * h0 /\
 167     &0 < x1 /\ &0 < x2 /\ &0 < x3 /\ &0 < x4 /\ &0 < x5 /\  &0 < x6 /\
 168     delta_x4 x1 x2 x3 x4 x5 x6 < &0 /\
 169     &0 < delta_x4 x2 x3 x1 x5 x6 x4  /\
 170     &0 < delta_x4 x3 x1 x2 x6 x4 x5  /\
 171     &0 <= delta_x x1 x2 x3 x4 x5 x6 ==>
 172     taum_x x1 x2 x3 x4 x5 x6 = sqrt(delta_x x1 x2 x3 x4 x5 x6) *
 173         tau_residual_x x1 x2 x3 x4 x5 x6 + flat_term_x x1`,
 174   (* {{{ proof *)
 175   [
 176   REPEAT WEAK_STRIP_TAC;
 177   FIRST_X_ASSUM MP_TAC;
 178   REWRITE_TAC[arith `&0 <= x <=> (&0 = x \/ &0 < x)`];
 179   DISCH_THEN DISJ_CASES_TAC;
 180     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];
 181     ASM_SIMP_TAC[arith `x * x = x pow 2`;SQRT_POW_2;arith `&0 < x ==> &0 <= x`];
 182     SUBGOAL_THEN `delta_x x2 x3 x1 x5 x6 x4 = &0` SUBST1_TAC;
 183       BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC);
 184     SUBGOAL_THEN `delta_x x3 x1 x2 x6 x4 x5 = &0` SUBST1_TAC;
 185       BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC);
 186     FIRST_X_ASSUM (fun t -> SUBST1_TAC (GSYM t));
 187     REWRITE_TAC[arith `x * &0 = &0`;arith `&0 * x = &0`;SQRT_0];
 188     ASM_SIMP_TAC[Merge_ineq.atn2_0;arith `(-- y < &0 <=> &0 < y) /\ ( &0 < -- y <=> y < &0)`];
 189     REWRITE_TAC[Sphere.h0;Nonlinear_lemma.rho_alt;arith `pi/ &2 + pi/ &2 = pi /\ x + -- x = &0 /\ x * &0 = &0`];
 190     REWRITE_TAC[Sphere.flat_term_x;Sphere.flat_term;Nonlinear_lemma.sol0_const1;Sphere.h0];
 191     BY(REAL_ARITH_TAC);
 192   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];
 193   ASM_SIMP_TAC[arith `x * x = x pow 2`;SQRT_POW_2;arith `&0 < x ==> &0 <= x`];
 194   REWRITE_TAC[Nonlin_def.tau_residual_x];
 195   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];
 196   ASM_REWRITE_TAC[];
 197   REWRITE_TAC[arith `a + b + c - d = (a - d) + b + c`];
 198   REWRITE_TAC[arith `a * (b + c) = a * b + a * c`];
 199   ONCE_REWRITE_TAC[arith `(a + b + c) +d = (a + d) + b + c`];
 200   BINOP_TAC;
 201     ASM_SIMP_TAC[Merge_ineq.dih_x_dih_x_div_sqrtdelta_negbranch];
 202     REWRITE_TAC[Sphere.h0;Nonlinear_lemma.rho_alt;Sphere.flat_term;Sphere.flat_term_x;Nonlinear_lemma.sol0_const1;];
 203     BY(REAL_ARITH_TAC);
 204   BINOP_TAC;
 205     ONCE_REWRITE_TAC[arith `a * b * c = b * (a * c)`];
 206     AP_TERM_TAC;
 207     GMATCH_SIMP_TAC Merge_ineq.dih_x_dih_x_div_sqrtdelta_posbranch;
 208     ASM_REWRITE_TAC[];
 209     SUBGOAL_THEN `delta_x x2 x3 x1 x5 x6 x4 = delta_x x1 x2 x3 x4 x5 x6` SUBST1_TAC;
 210       BY(REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC);
 211     BY(ASM_REWRITE_TAC[]);
 212   ONCE_REWRITE_TAC[arith `a * b * c = b * (a * c)`];
 213   AP_TERM_TAC;
 214   GMATCH_SIMP_TAC Merge_ineq.dih_x_dih_x_div_sqrtdelta_posbranch;
 215   ASM_REWRITE_TAC[];
 216   SUBGOAL_THEN `delta_x x3 x1 x2 x6 x4 x5 = delta_x x1 x2 x3 x4 x5 x6` SUBST1_TAC;
 217     BY(REWRITE_TAC[Sphere.delta_x] THEN REAL_ARITH_TAC);
 218   BY(ASM_REWRITE_TAC[])
 219   ]);;
 220   (* }}} *)
 221
 222 let OWZLKVY4 = prove_by_refinement(
 223   ` main_nonlinear_terminal_v11 ==> ( !y1 y2 y3 y4 y5 y6.
 224     &2 <= y1 /\ y1 <= &2 * h0 /\
 225     &2 <= y2 /\ y2 <= &2 * h0 /\
 226     &2 <= y3 /\ y3 <= &2 * h0 /\
 227     cstab <= y4 /\ y4 <= #3.915 /\
 228     y5 = &2 /\
 229     y6 = &2 /\
 230         &0 <= delta_y y1 y2 y3 y4 y5 y6 ==>
 231         taud y1 y2 y3 y4 y5 y6 <= taum y1 y2 y3 y4 y5 y6)`,
 232   (* {{{ proof *)
 233   [
 234   REPEAT WEAKER_STRIP_TAC;
 235   ASM_CASES_TAC `&80 <= delta_y y1 y2 y3 y4 y5 y6`;
 236     INTRO_TAC ((*--*)Terminal.get_main_nonlinear "2314572187") yys;
 237     REWRITE_TAC[Sphere.ineq;TAUT `(a ==> b==> c) <=> (a /\ b) ==> c `;TAUT `(a /\ b) /\ c <=> a /\ b /\ c`];
 238     ANTS_TAC;
 239       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0;Sphere.cstab] THEN REAL_ARITH_TAC);
 240     ASM_SIMP_TAC[arith `n <= d ==> ~(d < n)`;arith `x > y <=> y < x`];
 241     MATCH_MP_TAC (arith `u = v ==> (u < t ==> v <= t)`);
 242     MATCH_MP_TAC Functional_equation.taud_x_taud;
 243     BY(ASM_TAC THEN REAL_ARITH_TAC);
 244   RULE_ASSUM_TAC (REWRITE_RULE[arith `~(n <= d) <=> d < n`]);
 245   GMATCH_SIMP_TAC Terminal.taum_taum_x;
 246   CONJ_TAC;
 247     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[Appendix.cstab] THEN REAL_ARITH_TAC);
 248   REWRITE_TAC[Sphere.y_of_x];
 249   GMATCH_SIMP_TAC tau_x_tau_residual_x_general;
 250   TYPIFY `&0 <= delta_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6)` (C SUBGOAL_THEN ASSUME_TAC);
 251     FIRST_X_ASSUM_ST `&0 <= d` MP_TAC;
 252     BY(REWRITE_TAC[Sphere.delta_y] THEN REAL_ARITH_TAC);
 253   COMMENT "residue hypotheses";
 254   CONJ_TAC;
 255     ASM_REWRITE_TAC[];
 256     GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
 257     GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
 258     REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
 259     INTRO_TAC (UNDISCH Terminal.EAR_DELTA_X4) yys;
 260     ANTS_TAC;
 261       BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
 262     ASM_REWRITE_TAC[];
 263     DISCH_THEN (unlist REWRITE_TAC);
 264     REWRITE_TAC[arith `&4 = &2 * &2`];
 265     REWRITE_TAC[ REAL_OF_NUM_LT];
 266     GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
 267     REWRITE_TAC[arith `0 < 2`];
 268     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[Sphere.delta_y;Sphere.h0;Appendix.cstab] THEN REAL_ARITH_TAC);
 269   REWRITE_TAC[Nonlin_def.taud;Sphere.flat_term_x;Sphere.flat_term];
 270   GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
 271   CONJ_TAC;
 272     BY(ASM_TAC THEN REAL_ARITH_TAC);
 273   REWRITE_TAC[arith `v + u <= w + v <=> u <= w`];
 274   REWRITE_TAC[GSYM Sphere.delta_y];
 275   GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP;
 276   CONJ_TAC;
 277     GMATCH_SIMP_TAC SQRT_POS_LE;
 278     BY(ASM_REWRITE_TAC[Sphere.delta_y]);
 279   INTRO_TAC ((*--*)Terminal.get_main_nonlinear "7796879304") yys;
 280   REWRITE_TAC[Sphere.ineq;Sphere.y_of_x];
 281   REWRITE_TAC[TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
 282   ANTS_TAC;
 283     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[Appendix.cstab;Sphere.h0] THEN REAL_ARITH_TAC);
 284   BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
 285   ]);;
 286   (* }}} *)
 287
 288 let OPEN_REAL_INTERVAL_SING = prove_by_refinement(
 289   `!a b c. ~(real_interval(a,b) = {c})`,
 290   (* {{{ proof *)
 291   [
 292   REWRITE_TAC[EXTENSION;IN_SING;IN_REAL_INTERVAL];
 293   REPEAT WEAKER_STRIP_TAC;
 294   ASM_CASES_TAC `a < b`;
 295     FIRST_ASSUM (C INTRO_TAC [`(a + b)/ &2`]);
 296     FIRST_X_ASSUM (C INTRO_TAC [`(&3 * a + &1 * b)/ &4`]);
 297     BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
 298   FIRST_X_ASSUM_ST `!` MP_TAC;
 299   DISCH_THEN (C INTRO_TAC [`c:real`]);
 300   BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
 301   ]);;
 302   (* }}} *)
 303
 304 (* DERIVATIVES *)
 305
 306   let diff tm rw x s =
 307     let cv rw t = rhs(concl (REWRITE_CONV rw t)) in
 308     let tm2 = cv rw tm in
 309       ( (REWRITE_RULE (map GSYM rw) (Calc_derivative.differentiate tm2 x s)));;
 310
 311
 312 let DERIVED_TAC ttac =
 313   fun gl ->
 314     let (_,[b;f;f';y;s]) = strip_comb (goal_concl gl) in
 315       ttac (Calc_derivative.differentiate f y s) gl;;
 316
 317 let derived_form_F = prove_by_refinement(
 318   `!f f' x s. derived_form F f f' x s`,
 319   (* {{{ proof *)
 320   [
 321   REWRITE_TAC[Calc_derivative.derived_form]
 322   ]);;
 323   (* }}} *)
 324
 325 let derived_form_delta_y = prove_by_refinement(
 326   `!y1 y2 y3 y4 y5 y6. derived_form T (\q. delta_y q y2 y3 y4 y5 y6)
 327     (y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * &2 * y1) y1 (:real) `,
 328   (* {{{ proof *)
 329   [
 330   REPEAT WEAKER_STRIP_TAC;
 331   REWRITE_TAC[Sphere.delta_y;Sphere.delta_x];
 332   DERIVED_TAC MP_TAC;
 333   MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
 334   REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
 335   REWRITE_TAC[Nonlin_def.delta_x1;Sphere.y_of_x];
 336   BY(REAL_ARITH_TAC)
 337   ]);;
 338   (* }}} *)
 339
 340   let derived_form_delta_x = prove_by_refinement(
 341   `!x1 x2 x3 x4 x5 x6 .derived_form T (\q. delta_x q x2 x3 x4 x5 x6)
 342      (delta_x1 x1 x2 x3 x4 x5 x6)
 343      x1
 344      (:real)`,
 345   (* {{{ proof *)
 346   [
 347   REPEAT WEAKER_STRIP_TAC;
 348   MP_TAC (diff `(\q. delta_x q x2 x3 x4 x5 x6)` [Sphere.delta_x] `x1:real` `(:real)`);
 349   MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
 350   REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
 351   REWRITE_TAC[Nonlin_def.delta_x1];
 352   BY(REAL_ARITH_TAC)
 353   ]);;
 354   (* }}} *)
 355
 356 let derived_form_delta_x1 = prove_by_refinement(
 357   `!x1 x2 x3 x4 x5 x6. derived_form T (\q. delta_x1 q x2 x3 x4 x5 x6)
 358     ( -- &2 * x4)
 359      x1
 360     (:real)`,
 361   (* {{{ proof *)
 362   [
 363   REPEAT WEAKER_STRIP_TAC;
 364   MP_TAC (diff `(\q. delta_x1 q x2 x3 x4 x5 x6)` [Nonlin_def.delta_x1] `x1:real` `(:real)`);
 365   MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
 366   REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
 367   REWRITE_TAC[Nonlin_def.delta_x1];
 368   BY(REAL_ARITH_TAC)
 369   ]);;
 370   (* }}} *)
 371
 372 let deriv_form_taud = prove_by_refinement(
 373   `!y1 y2 y3 y4 y5 y6. derived_form (&0 < delta_y y1 y2 y3 y4 y5 y6)
 374     (\q. taud q y2 y3 y4 y5 y6)
 375     ((-- #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 +
 376          (sol0 / (&2 * h0 - &2)) * sqrt(delta_y y1 y2 y3 y4 y5 y6))/ sqrt(delta_y y1 y2 y3 y4 y5 y6))
 377     y1
 378     (:real)`,
 379   (* {{{ proof *)
 380   [
 381   REPEAT WEAKER_STRIP_TAC;
 382   REWRITE_TAC[Nonlin_def.taud;Nonlin_def.mu_y];
 383   DERIVED_TAC (MP_TAC o GEN_ALL o (GENL [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`]));
 384   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`]);
 385   REWRITE_TAC[derived_form_delta_y];
 386   TYPIFY `~(&2 * h0 - &2 = &0)` (C SUBGOAL_THEN ASSUME_TAC);
 387     BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
 388   ASM_REWRITE_TAC[];
 389   MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
 390   ASM_CASES_TAC `(&0 < delta_y y1 y2 y3 y4 y5 y6)`;
 391     ASM_REWRITE_TAC[];
 392     REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
 393     Calc_derivative.CALC_ID_TAC;
 394     ASM_REWRITE_TAC[];
 395     REWRITE_TAC[arith `~(&2 = &0)`];
 396     CONJ_TAC;
 397       GMATCH_SIMP_TAC SQRT_EQ_0;
 398       BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
 399     TYPED_ABBREV_TAC `a = sqrt(delta_y y1 y2 y3 y4 y5 y6)`;
 400     TYPED_ABBREV_TAC `b = y_of_x delta_x1 y1 y2 y3 y4 y5 y6`;
 401     TYPIFY `delta_y y1 y2 y3 y4 y5 y6 = a*a` (C SUBGOAL_THEN SUBST1_TAC);
 402       EXPAND_TAC "a";
 403       GMATCH_SIMP_TAC (GSYM SQRT_MUL);
 404       GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
 405       BY(ASM_TAC THEN REAL_ARITH_TAC);
 406     REWRITE_TAC[GSYM Nonlin_def.mu_y];
 407     TYPED_ABBREV_TAC `c = mu_y y1 y2 y3`;
 408     TYPED_ABBREV_TAC `d = (&2 * h0 - &2)`;
 409     TYPED_ABBREV_TAC `e = #0.07`;
 410     BY(REAL_ARITH_TAC);
 411   ASM_REWRITE_TAC[];
 412   BY(REWRITE_TAC[Calc_derivative.derived_form])
 413   ]);;
 414   (* }}} *)
 415
 416 (* renamed from deriv_form_taud_ALT *)
 417
 418 let derived_form_taud_ALT = prove_by_refinement(
 419   `!y1 y2 y3 y4 y5 y6. derived_form ((&0 < delta_y y1 y2 y3 y4 y5 y6) /\ (&0 <= y1 /\ &0 <= y2 /\ &0 <= y3))
 420     (\q. taud q y2 y3 y4 y5 y6)
 421     (y_of_x taud_D1_num_x y1 y2 y3 y4 y5 y6 / sqrt(delta_y y1 y2 y3 y4 y5 y6))
 422     y1
 423     (:real)`,
 424   (* {{{ proof *)
 425   [
 426   REWRITE_TAC[Sphere.y_of_x;Functional_equation.nonfunctional_taud_D1;LET_DEF;LET_END_DEF];
 427   REPEAT WEAKER_STRIP_TAC;
 428   ASM_CASES_TAC `&0 <= y1 /\ &0 <= y2 /\ &0 <= y3`;
 429     ASM_REWRITE_TAC[];
 430     ASM_SIMP_TAC[GSYM Functional_equation.mu6_x_mu_y];
 431     INTRO_TAC deriv_form_taud yys;
 432     ASM_CASES_TAC `(&0 < delta_y y1 y2 y3 y4 y5 y6)`;
 433       ASM_REWRITE_TAC[];
 434       MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
 435       REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
 436       Calc_derivative.CALC_ID_TAC;
 437       SUBCONJ_TAC;
 438         BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
 439       DISCH_TAC;
 440       REWRITE_TAC[GSYM Sphere.delta_y];
 441       REWRITE_TAC[GSYM Sphere.y_of_x];
 442       REWRITE_TAC[Sphere.h0];
 443       GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
 444       ASM_REWRITE_TAC[];
 445       BY(REAL_ARITH_TAC);
 446     BY(ASM_REWRITE_TAC[Calc_derivative.derived_form]);
 447   BY(ASM_REWRITE_TAC[Calc_derivative.derived_form])
 448   ]);;
 449   (* }}} *)
 450
 451 let deriv_form_taud_D2 = prove_by_refinement(
 452   `!y1 y2 y3 y4 y5 y6. derived_form ((&0 < delta_y y1 y2 y3 y4 y5 y6) /\ (&0 < y1 /\ &0 <= y2 /\ &0 <= y3))
 453     (\q. (y_of_x taud_D1_num_x q y2 y3 y4 y5 y6 / sqrt(delta_y q y2 y3 y4 y5 y6)))
 454     (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)`,
 455   (* {{{ proof *)
 456   [
 457   REWRITE_TAC[Sphere.y_of_x;Functional_equation.nonfunctional_taud_D2;Functional_equation.nonfunctional_taud_D1;LET_DEF;LET_END_DEF];
 458   REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV];
 459   REPEAT WEAKER_STRIP_TAC;
 460   TYPIFY `(~(sqrt (delta_y y1 y2 y3 y4 y5 y6) = &0))` ((C SUBGOAL_THEN ASSUME_TAC));
 461     GMATCH_SIMP_TAC SQRT_EQ_0;
 462     BY(ASM_TAC THEN REAL_ARITH_TAC);
 463   MATCH_MP_TAC Arc_properties.HAS_REAL_DERIVATIVE_LOCAL;
 464   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;
 465   CONJ2_TAC;
 466     TYPIFY `{q | &0 < q}` EXISTS_TAC;
 467     ASM_REWRITE_TAC[arith `!q. &0 < q <=> q > &0`;IN_ELIM_THM];
 468     REWRITE_TAC[REAL_OPEN_HALFSPACE_GT];
 469     REPEAT WEAKER_STRIP_TAC;
 470     REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
 471     RULE_ASSUM_TAC(REWRITE_RULE[arith `y > &0 <=> &0 < y`]);
 472     GMATCH_SIMP_TAC (GSYM Functional_equation.mu6_x_mu_y);
 473     GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
 474     BY(ASM_TAC THEN REAL_ARITH_TAC);
 475   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)`];
 476   REWRITE_TAC[WITHINREAL_UNIV];
 477   DISCH_THEN ((unlist REWRITE_TAC) o GSYM);
 478   DERIVED_TAC (MP_TAC o GEN_ALL o (GENL [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`]));
 479   ASM_REWRITE_TAC[GSYM Sphere.delta_y];
 480   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`]);
 481   REWRITE_TAC[derived_form_delta_y];
 482   TYPIFY_GOAL_THEN `derived_form T (\q. mu_y q y2 y3) (-- #0.07) y1 (:real)` (unlist REWRITE_TAC);
 483     REWRITE_TAC[Nonlin_def.mu_y];
 484     DERIVED_TAC MP_TAC;
 485     MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
 486     REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
 487     BY(REAL_ARITH_TAC);
 488   ASM_REWRITE_TAC[];
 489   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);
 490     REWRITE_TAC[Nonlin_def.delta_x1];
 491     DERIVED_TAC MP_TAC;
 492     MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
 493     REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
 494     BY(REAL_ARITH_TAC);
 495   MATCH_MP_TAC (TAUT `(x <=> y) ==> (x ==> y)`);
 496   REPEAT (AP_THM_TAC ORELSE AP_TERM_TAC);
 497   REWRITE_TAC[GSYM Sphere.y_of_x];
 498   TYPED_ABBREV_TAC `a = sqrt(delta_y y1 y2 y3 y4 y5 y6)`;
 499   TYPED_ABBREV_TAC `b = y_of_x delta_x1 y1 y2 y3 y4 y5 y6`;
 500   GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
 501   ASM_SIMP_TAC[arith `&0 < y ==> &0 <= y`];
 502   TYPIFY `y_of_x mu6_x y1 y2 y3 y4 y5 y6 = mu_y y1 y2 y3` (C SUBGOAL_THEN SUBST1_TAC);
 503     REWRITE_TAC[Sphere.y_of_x];
 504     GMATCH_SIMP_TAC (GSYM Functional_equation.mu6_x_mu_y);
 505     BY(ASM_TAC THEN REAL_ARITH_TAC);
 506   TYPIFY `delta_y y1 y2 y3 y4 y5 y6 = a * a` (C SUBGOAL_THEN SUBST1_TAC);
 507     EXPAND_TAC "a";
 508     GMATCH_SIMP_TAC (GSYM SQRT_MUL);
 509     GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
 510     BY(ASM_TAC THEN REAL_ARITH_TAC);
 511   Calc_derivative.CALC_ID_TAC;
 512   TYPIFY_GOAL_THEN `~(a = &0)` (unlist REWRITE_TAC);
 513     BY(ASM_REWRITE_TAC[]);
 514   BY(REAL_ARITH_TAC)
 515   ]);;
 516   (* }}} *)
 517
 518 let thD3  =
 519   let th1 = (diff `((\q. (-- #0.07 *
 520              delta_y q y2 y3 y4 y5 y6 *
 521              (--(q * q) * y4 * y4 +
 522               (y2 * y2) * y5 * y5 - (y3 * y3) * y5 * y5 - (y2 * y2) * y6 * y6 +
 523               (y3 * y3) * y6 * y6 +
 524               (y4 * y4) *
 525               (--(q * q) + y2 * y2 + y3 * y3 - y4 * y4 + y5 * y5 + y6 * y6)) *
 526              &2 *
 527              sqrt (q * q) -
 528              &1 / &4 *
 529              ( #0.012 +
 530                #0.07 * ( #2.52 - sqrt (q * q)) +
 531                #0.01 * ( #2.52 * &2 - sqrt (y2 * y2) - sqrt (y3 * y3))) *
 532              ((--(q * q) * y4 * y4 +
 533                (y2 * y2) * y5 * y5 -
 534                (y3 * y3) * y5 * y5 -
 535                (y2 * y2) * y6 * y6 +
 536                (y3 * y3) * y6 * y6 +
 537                (y4 * y4) *
 538                (--(q * q) + y2 * y2 + y3 * y3 - y4 * y4 + y5 * y5 + y6 * y6)) *
 539               &2 *
 540               sqrt (q * q)) pow
 541              2 +
 542              &1 / &2 *
 543              ( #0.012 +
 544                #0.07 * ( #2.52 - sqrt (q * q)) +
 545                #0.01 * ( #2.52 * &2 - sqrt (y2 * y2) - sqrt (y3 * y3))) *
 546              delta_y q y2 y3 y4 y5 y6 *
 547              (-- &8 * (q * q) * y4 * y4 +
 548               (--(q * q) * y4 * y4 +
 549                (y2 * y2) * y5 * y5 -
 550                (y3 * y3) * y5 * y5 -
 551                (y2 * y2) * y6 * y6 +
 552                (y3 * y3) * y6 * y6 +
 553                (y4 * y4) *
 554                (--(q * q) + y2 * y2 + y3 * y3 - y4 * y4 + y5 * y5 + y6 * y6)) *
 555               &2)) /
 556             sqrt (delta_y q y2 y3 y4 y5 y6) pow 3)) `  [] `y1:real` `(:real)`) in
 557   let fr = frees  (concl(GENL [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`] th1)) in
 558   let th2 = GENL fr th1 in
 559   let ddelta_y = `(y_of_x delta_x1 y1 y2 y3 y4 y5 y6 * &2 * y1)` in
 560   let th3 = SPECL [ddelta_y;ddelta_y;ddelta_y] th2 in
 561   let th4 = REWRITE_RULE[derived_form_delta_y]  th3 in
 562   let (h,[b;f;f';y;s]) = strip_comb (concl th4) in
 563   let tm = list_mk_comb (h,[b;f;`f':real`;y;s]) in
 564     GENL [`y1:real`;`y2:real`;`y3:real`;`y4:real`;`y5:real`;`y6:real`] ( EXISTS (mk_exists (`f':real`,tm),f') th4);;
 565
 566 let derived_form_taud_D3 = prove_by_refinement(
 567   `!y1 y2 y3 y4 y5 y6. ?f'. derived_form ((&0 < delta_y y1 y2 y3 y4 y5 y6) /\ (&0 < y1 /\ &0 <= y2 /\ &0 <= y3))
 568     (\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)))
 569      f' y1 (:real)`,
 570   (* {{{ proof *)
 571   [
 572   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];
 573   REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV];
 574   REPEAT WEAKER_STRIP_TAC;
 575   REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
 576   REPEAT WEAKER_STRIP_TAC;
 577   INTRO_TAC thD3 yys;
 578   REPEAT WEAKER_STRIP_TAC;
 579   TYPIFY `f'` EXISTS_TAC;
 580   FIRST_X_ASSUM MP_TAC;
 581   REWRITE_TAC[Calc_derivative.derived_form];
 582   ANTS_TAC;
 583     TYPIFY_GOAL_THEN `&0 < y1 * y1` (unlist REWRITE_TAC);
 584       GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
 585       BY(ASM_REWRITE_TAC[]);
 586     ASM_REWRITE_TAC[];
 587     GMATCH_SIMP_TAC SQRT_EQ_0;
 588     BY(ASM_TAC THEN REAL_ARITH_TAC);
 589   BY(REWRITE_TAC[WITHINREAL_UNIV])
 590   ]);;
 591   (* }}} *)
 592
 593 let SECOND_DERIVATIVE_TEST = prove_by_refinement(
 594   `!f f' f'' z s.
 595     z IN s /\ real_open s /\
 596     (!x. x IN s ==> (f has_real_derivative f' x) (atreal x)) /\
 597     (!x. x IN s ==> (f' has_real_derivative f'' x) (atreal x)) /\
 598     (f'' real_continuous atreal z) /\
 599     (!x. x IN s ==> f z <= f x) ==>
 600     (f' z = &0 /\  &0 <= f'' z)`,
 601   (* {{{ proof *)
 602   [
 603   REPEAT WEAKER_STRIP_TAC;
 604   SUBCONJ_TAC;
 605     INTRO_TAC REAL_DERIVATIVE_ZERO_MAXMIN [`f`;`f' z`;`z`;`s`];
 606     DISCH_THEN MATCH_MP_TAC;
 607     ASM_REWRITE_TAC[];
 608     FIRST_X_ASSUM MATCH_MP_TAC;
 609     BY(ASM_REWRITE_TAC[]);
 610   DISCH_TAC;
 611   REWRITE_TAC[arith `&0 <= r <=> ~(r < &0)`];
 612   DISCH_TAC;
 613   RULE_ASSUM_TAC(REWRITE_RULE[real_continuous_atreal]);
 614   FIRST_X_ASSUM_ST `abs` (C INTRO_TAC [`-- f'' z`]);
 615   ANTS_TAC;
 616     BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
 617   REPEAT WEAKER_STRIP_TAC;
 618   TYPED_ABBREV_TAC  `s' = s INTER {x | abs(x - z) < d}` ;
 619   TYPIFY `z IN s'` (C SUBGOAL_THEN ASSUME_TAC);
 620     EXPAND_TAC "s'";
 621     BY(ASM_REWRITE_TAC[IN_INTER;IN_ELIM_THM;arith `z - z = &0`;REAL_ABS_0]);
 622   TYPIFY `real_open s'` (C SUBGOAL_THEN ASSUME_TAC);
 623     EXPAND_TAC "s'";
 624     MATCH_MP_TAC REAL_OPEN_INTER;
 625     ASM_REWRITE_TAC[];
 626     REWRITE_TAC[real_open;IN_ELIM_THM];
 627     REPEAT WEAKER_STRIP_TAC;
 628     TYPIFY `d - abs (x - z)` EXISTS_TAC;
 629     CONJ_TAC;
 630       BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
 631     REPEAT WEAKER_STRIP_TAC;
 632     BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
 633   COMMENT "restrict to an interval";
 634   TYPIFY `?a b. real_interval (a,b) SUBSET s' /\ z IN real_interval(a,b)` (C SUBGOAL_THEN MP_TAC);
 635     RULE_ASSUM_TAC(REWRITE_RULE[real_open]);
 636     FIRST_X_ASSUM (C INTRO_TAC [`z`]);
 637     ASM_REWRITE_TAC[];
 638     REPEAT WEAKER_STRIP_TAC;
 639     GEXISTL_TAC [`z - e`;`z + e`];
 640     REWRITE_TAC[SUBSET;IN_REAL_INTERVAL];
 641     REPEAT WEAKER_STRIP_TAC;
 642     CONJ_TAC;
 643       REPEAT WEAKER_STRIP_TAC;
 644       FIRST_X_ASSUM MATCH_MP_TAC;
 645       BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
 646     BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
 647   REPEAT WEAKER_STRIP_TAC;
 648   INTRO_TAC REAL_OPEN_REAL_INTERVAL [`a`;`b`];
 649   DISCH_TAC;
 650   TYPIFY `!x. x IN s' ==> f'' x < &0` (C SUBGOAL_THEN ASSUME_TAC);
 651     REPEAT WEAKER_STRIP_TAC;
 652     FIRST_X_ASSUM (C INTRO_TAC [`x`]);
 653     ANTS_TAC;
 654       FIRST_X_ASSUM MP_TAC;
 655       EXPAND_TAC "s'";
 656       BY(REWRITE_TAC[IN_INTER;IN_ELIM_THM] THEN REAL_ARITH_TAC);
 657     BY(REAL_ARITH_TAC);
 658   INTRO_TAC Counting_spheres.REAL_CONVEX_ON_SECOND_SECANT [`(\x. -- f x)`;`(\x. -- f' x)`;`(\x. -- f'' x)`;`real_interval (a,b)`];
 659   ANTS_TAC;
 660     REWRITE_TAC[IS_REALINTERVAL_INTERVAL;OPEN_REAL_INTERVAL_SING];
 661     TYPIFY `!x. x IN real_interval(a,b) ==> x IN s` (C SUBGOAL_THEN ASSUME_TAC);
 662       BY(ASM_TAC THEN SET_TAC[]);
 663     CONJ_TAC;
 664       REPEAT WEAKER_STRIP_TAC;
 665       MATCH_MP_TAC HAS_REAL_DERIVATIVE_NEG;
 666       GMATCH_SIMP_TAC HAS_REAL_DERIVATIVE_WITHIN_REAL_OPEN;
 667       BY(ASM_SIMP_TAC[REAL_OPEN_REAL_INTERVAL]);
 668     CONJ_TAC;
 669       REPEAT WEAKER_STRIP_TAC;
 670       MATCH_MP_TAC HAS_REAL_DERIVATIVE_NEG;
 671       GMATCH_SIMP_TAC HAS_REAL_DERIVATIVE_WITHIN_REAL_OPEN;
 672       BY(ASM_SIMP_TAC[REAL_OPEN_REAL_INTERVAL]);
 673     REPEAT WEAKER_STRIP_TAC;
 674     MATCH_MP_TAC (arith `f < &0 ==> &0 <= -- f`);
 675     FIRST_X_ASSUM MATCH_MP_TAC;
 676     BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
 677   DISCH_TAC;
 678   TYPIFY `!x. x IN real_interval(a,b) ==> f x = f z` (C SUBGOAL_THEN ASSUME_TAC);
 679     REPEAT WEAKER_STRIP_TAC;
 680     FIRST_X_ASSUM (C INTRO_TAC [`x`;`z`]);
 681     ASM_REWRITE_TAC[];
 682     FIRST_X_ASSUM_ST `fz <= fx` (C INTRO_TAC [`x`]);
 683     ANTS_TAC;
 684       BY(ASM_TAC THEN SET_TAC[]);
 685     BY(REAL_ARITH_TAC);
 686   TYPIFY `!x. x IN real_interval (a,b) ==> (f has_real_derivative &0) (atreal x)` (C SUBGOAL_THEN ASSUME_TAC);
 687     REPEAT WEAKER_STRIP_TAC;
 688     MATCH_MP_TAC Arc_properties.HAS_REAL_DERIVATIVE_LOCAL;
 689     TYPIFY `(\ (x:real). f z)` EXISTS_TAC;
 690     REWRITE_TAC[];
 691     CONJ_TAC;
 692       BY(REWRITE_TAC[HAS_REAL_DERIVATIVE_CONST]);
 693     TYPIFY `real_interval(a,b)` EXISTS_TAC;
 694     BY(ASM_REWRITE_TAC[REAL_OPEN_REAL_INTERVAL]);
 695   COMMENT "show f' is zero";
 696   TYPIFY `!x. x IN real_interval(a,b) ==> (f' x = &0)` (C SUBGOAL_THEN ASSUME_TAC);
 697     REPEAT WEAKER_STRIP_TAC;
 698     MATCH_MP_TAC REAL_DERIVATIVE_UNIQUE_ATREAL;
 699     GEXISTL_TAC [`f`;`x`];
 700     ASM_SIMP_TAC[];
 701     FIRST_X_ASSUM MATCH_MP_TAC;
 702     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
 703   COMMENT "show f' has zero derivative";
 704   TYPIFY `!x. x IN real_interval (a,b) ==> (f' has_real_derivative &0) (atreal x)` (C SUBGOAL_THEN ASSUME_TAC);
 705     REPEAT WEAKER_STRIP_TAC;
 706     MATCH_MP_TAC Arc_properties.HAS_REAL_DERIVATIVE_LOCAL;
 707     TYPIFY `(\ (x:real).  &0)` EXISTS_TAC;
 708     REWRITE_TAC[];
 709     CONJ_TAC;
 710       BY(REWRITE_TAC[HAS_REAL_DERIVATIVE_CONST]);
 711     TYPIFY `real_interval(a,b)` EXISTS_TAC;
 712     BY(ASM_REWRITE_TAC[REAL_OPEN_REAL_INTERVAL]);
 713   COMMENT "show f'' is zero";
 714   TYPIFY `!x. x IN real_interval(a,b) ==> (f'' x = &0)` (C SUBGOAL_THEN ASSUME_TAC);
 715     REPEAT WEAKER_STRIP_TAC;
 716     MATCH_MP_TAC REAL_DERIVATIVE_UNIQUE_ATREAL;
 717     GEXISTL_TAC [`f'`;`x`];
 718     ASM_SIMP_TAC[];
 719     FIRST_X_ASSUM MATCH_MP_TAC;
 720     BY(REPEAT (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
 721   FIRST_X_ASSUM (C INTRO_TAC [`z`]);
 722   ASM_REWRITE_TAC[];
 723   REPLICATE_TAC 12 (FIRST_X_ASSUM kill);
 724   FIRST_X_ASSUM_ST `f'' z < &0` MP_TAC;
 725   BY(REAL_ARITH_TAC)
 726   ]);;
 727   (* }}} *)
 728
 729 (* END OF DERIVATIVES *)
 730
 731
 732 (* CONTINUITY *)
 733
 734 let continuous_preimage_closed = prove_by_refinement(
 735   `!f s t. real_closed s /\ real_closed t /\ f real_continuous_on s ==>
 736     real_closed { x  | x IN s /\ f x IN t }`,
 737   (* {{{ proof *)
 738   [
 739   REWRITE_TAC[real_continuous_on];
 740   REWRITE_TAC[real_closed;real_open;IN_DIFF;IN_UNIV;IN_ELIM_THM;DE_MORGAN_THM];
 741   REPEAT WEAKER_STRIP_TAC;
 742   FIRST_X_ASSUM DISJ_CASES_TAC;
 743     BY(ASM_MESON_TAC[]);
 744   TYPIFY `~(x IN s)` ASM_CASES_TAC;
 745     BY(ASM_MESON_TAC[]);
 746   FIRST_X_ASSUM (C INTRO_TAC [`x`]);
 747   RULE_ASSUM_TAC(REWRITE_RULE[TAUT `~ ~ x = x`]);
 748   ASM_REWRITE_TAC[];
 749   FIRST_X_ASSUM (C INTRO_TAC [`f x`]);
 750   ASM_REWRITE_TAC[];
 751   REPEAT WEAKER_STRIP_TAC;
 752   FIRST_X_ASSUM (C INTRO_TAC [`e`]);
 753   ASM_REWRITE_TAC[];
 754   REPEAT WEAKER_STRIP_TAC;
 755   TYPIFY `d` EXISTS_TAC;
 756   ASM_REWRITE_TAC[];
 757   REPEAT WEAKER_STRIP_TAC;
 758   TYPIFY `(x' IN s)` ASM_CASES_TAC;
 759     ASM_REWRITE_TAC[];
 760     FIRST_X_ASSUM MATCH_MP_TAC;
 761     FIRST_X_ASSUM MATCH_MP_TAC;
 762     BY(ASM_REWRITE_TAC[]);
 763   BY(ASM_REWRITE_TAC[])
 764   ]);;
 765   (* }}} *)
 766
 767 let continuous_preimage_open = prove_by_refinement(
 768   `!f s t. real_open s /\ real_open t /\ f real_continuous_on s ==>
 769     real_open { x  | x IN s /\ f x IN t }`,
 770   (* {{{ proof *)
 771   [
 772   REWRITE_TAC[real_continuous_on];
 773   REWRITE_TAC[real_closed;real_open;IN_DIFF;IN_UNIV;IN_ELIM_THM;DE_MORGAN_THM];
 774   REPEAT WEAKER_STRIP_TAC;
 775   FIRST_X_ASSUM (C INTRO_TAC [`x`]);
 776   ASM_REWRITE_TAC[];
 777   FIRST_X_ASSUM (C INTRO_TAC [`f x`]);
 778   ASM_REWRITE_TAC[];
 779   REPEAT WEAKER_STRIP_TAC;
 780   FIRST_X_ASSUM_ST `x IN s ==> p` (C INTRO_TAC [`x`]);
 781   ASM_REWRITE_TAC[];
 782   REPEAT WEAKER_STRIP_TAC;
 783   FIRST_X_ASSUM_ST `?` (C INTRO_TAC [`e`]);
 784   ASM_REWRITE_TAC[];
 785   REPEAT WEAKER_STRIP_TAC;
 786   TYPIFY `min d e'` EXISTS_TAC;
 787   CONJ_TAC;
 788     REWRITE_TAC[real_min];
 789     BY(ASM_TAC THEN REAL_ARITH_TAC);
 790   REPEAT WEAKER_STRIP_TAC;
 791   SUBCONJ_TAC;
 792     FIRST_X_ASSUM MATCH_MP_TAC;
 793     BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[real_min] THEN REAL_ARITH_TAC);
 794   DISCH_TAC;
 795   FIRST_X_ASSUM MATCH_MP_TAC;
 796   FIRST_X_ASSUM MATCH_MP_TAC;
 797   ASM_REWRITE_TAC[];
 798   BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[real_min] THEN REAL_ARITH_TAC)
 799   ]);;
 800   (* }}} *)
 801
 802 let delta_y_continuous = prove_by_refinement(
 803   `!y2 y3 y4 y5 y6. (\q. delta_y q y2 y3 y4 y5 y6) real_continuous_on (:real)`,
 804   (* {{{ proof *)
 805   [
 806   REPEAT WEAKER_STRIP_TAC;
 807   GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
 808   REWRITE_TAC[REAL_OPEN_UNIV;IN_UNIV];
 809   GEN_TAC;
 810   INTRO_TAC derived_form_delta_y [`x`;`y2`;`y3`;`y4`;`y5`;`y6`];
 811   REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV];
 812   DISCH_THEN (MP_TAC o (MATCH_MP HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL));
 813   BY(REWRITE_TAC[])
 814   ]);;
 815   (* }}} *)
 816
 817 let taud_continuous = prove_by_refinement(
 818   `!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}`,
 819   (* {{{ proof *)
 820   [
 821   REPEAT WEAKER_STRIP_TAC;
 822   REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN;IN_ELIM_THM];
 823   REPEAT WEAKER_STRIP_TAC;
 824   REWRITE_TAC[Nonlin_def.taud];
 825   REWRITE_TAC[arith `!q. a * (q - b)/ r = (a * inv r) * q + a * (-- b) * inv r`];
 826   REWRITE_TAC[arith `!q. a + b * (c - q) + d = (-- b) * q + (a + b*c + d)`];
 827   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)));
 828   CONJ_TAC;
 829     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)`];
 830     MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_COMPOSE;
 831     REWRITE_TAC[IMAGE;IN_ELIM_THM];
 832     CONJ_TAC;
 833       MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_SUBSET;
 834       TYPIFY `(:real)` EXISTS_TAC;
 835       REWRITE_TAC[delta_y_continuous;SUBSET;IN_UNIV];
 836       INTRO_TAC delta_y_continuous [`y2`;`y3`;`y4`;`y5`;`y6`];
 837       REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN];
 838       DISCH_THEN MATCH_MP_TAC;
 839       BY(REWRITE_TAC[IN_UNIV]);
 840     TYPED_ABBREV_TAC  `u = delta_y x y2 y3 y4 y5 y6` ;
 841     MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_SUBSET;
 842     TYPIFY `{u | &0 <= u}` EXISTS_TAC;
 843     REWRITE_TAC[REAL_CONTINUOUS_WITHIN_SQRT_STRONG];
 844     REWRITE_TAC[SUBSET;IN_ELIM_THM];
 845     BY(MESON_TAC[]);
 846   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))))
 847   ]);;
 848   (* }}} *)
 849
 850 let taud_minimizer = prove_by_refinement(
 851   `!a b d y2 y3 y4 y5 y6.
 852   (let s = real_interval [a,b] INTER { q | d <= delta_y q y2 y3 y4 y5 y6} in
 853     (&0 <= d /\ ~(s = {}) ==>
 854        (?z1. z1 IN s /\ (!y1. y1 IN s ==> taud z1 y2 y3 y4 y5 y6 <= taud y1 y2 y3 y4 y5 y6))))`,
 855   (* {{{ proof *)
 856   [
 857   REWRITE_TAC[LET_DEF;LET_END_DEF];
 858   REPEAT WEAKER_STRIP_TAC;
 859   MATCH_MP_TAC REAL_CONTINUOUS_ATTAINS_INF;
 860   ASM_REWRITE_TAC[];
 861   CONJ2_TAC;
 862     MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET;
 863     TYPIFY `{q | &0 <= delta_y q y2 y3 y4 y5 y6}` EXISTS_TAC;
 864     REWRITE_TAC[taud_continuous];
 865     REWRITE_TAC[SUBSET;IN_INTER;IN_ELIM_THM];
 866     BY(ASM_TAC THEN REAL_ARITH_TAC);
 867   REWRITE_TAC[REAL_COMPACT_EQ_BOUNDED_CLOSED];
 868   CONJ_TAC;
 869     MATCH_MP_TAC REAL_BOUNDED_SUBSET;
 870     TYPIFY `real_interval[a,b]` EXISTS_TAC;
 871     REWRITE_TAC[REAL_BOUNDED_REAL_INTERVAL];
 872     BY(SET_TAC[]);
 873   MATCH_MP_TAC REAL_CLOSED_INTER;
 874   REWRITE_TAC[REAL_CLOSED_REAL_INTERVAL];
 875   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);
 876     BY(REWRITE_TAC[IN_UNIV;IN_ELIM_THM]);
 877   MATCH_MP_TAC continuous_preimage_closed;
 878   REWRITE_TAC[delta_y_continuous];
 879   REWRITE_TAC[REAL_CLOSED_UNIV];
 880   BY(REWRITE_TAC[arith `d <= t <=> t >= d`;REAL_CLOSED_HALFSPACE_GE])
 881   ]);;
 882   (* }}} *)
 883
 884 let taud_minimizer_cases = prove_by_refinement(
 885   `!a b d z1 y2 y3 y4 y5 y6.
 886   (let s = real_interval [a,b] INTER { q | d <= delta_y q y2 y3 y4 y5 y6} in
 887        (&0 <= d /\ &0 <= a /\ &0 <= y2 /\ &0 <= y3 /\ z1 IN s /\
 888           (!y1. y1 IN s ==> taud z1 y2 y3 y4 y5 y6 <= taud y1 y2 y3 y4 y5 y6) ==>
 889           ( z1 = a \/ z1 = b \/ d = delta_y z1 y2 y3 y4 y5 y6 \/
 890               (y_of_x taud_D1_num_x z1 y2 y3 y4 y5 y6 = &0 /\
 891                   &0 <= y_of_x taud_D2_num_x z1 y2 y3 y4 y5 y6) )))`,
 892   (* {{{ proof *)
 893   [
 894   REWRITE_TAC[LET_DEF;LET_END_DEF];
 895   REPEAT WEAKER_STRIP_TAC;
 896   TYPIFY `z1 = a` ASM_CASES_TAC;
 897     BY(ASM_REWRITE_TAC[]);
 898   TYPIFY `z1 = b` ASM_CASES_TAC;
 899     BY(ASM_REWRITE_TAC[]);
 900   TYPIFY `d = delta_y z1 y2 y3 y4 y5 y6` ASM_CASES_TAC;
 901     BY(ASM_REWRITE_TAC[]);
 902   ASM_REWRITE_TAC[];
 903   TYPIFY `a < z1 /\ z1 < b /\ d < delta_y z1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC);
 904     RULE_ASSUM_TAC(REWRITE_RULE[IN_REAL_INTERVAL;IN_INTER;IN_ELIM_THM]);
 905     BY(ASM_TAC THEN REAL_ARITH_TAC);
 906   TYPED_ABBREV_TAC  `s' = (real_interval (a,b) INTER {q | d < delta_y q y2 y3 y4 y5 y6})` ;
 907   TYPIFY `real_open s'` (C SUBGOAL_THEN ASSUME_TAC);
 908     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);
 909       EXPAND_TAC "s'";
 910       BY(REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_INTER]);
 911     MATCH_MP_TAC continuous_preimage_open;
 912     REWRITE_TAC[REAL_OPEN_REAL_INTERVAL];
 913     CONJ_TAC;
 914       BY(REWRITE_TAC[REAL_OPEN_HALFSPACE_GT;arith `d < t <=> t > d`]);
 915     MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET;
 916     TYPIFY `(:real)` EXISTS_TAC;
 917     REWRITE_TAC[delta_y_continuous];
 918     BY(SET_TAC[]);
 919   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'`];
 920   ASM_REWRITE_TAC[];
 921   COMMENT "big ants";
 922   ANTS_TAC;
 923     SUBCONJ_TAC;
 924       EXPAND_TAC "s'";
 925       REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
 926       BY(ASM_REWRITE_TAC[]);
 927     DISCH_TAC;
 928     CONJ_TAC;
 929       REPEAT WEAKER_STRIP_TAC;
 930       INTRO_TAC derived_form_taud_ALT [`x`;`y2`;`y3`;`y4`;`y5`;`y6`];
 931       REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV];
 932       ANTS_TAC;
 933         ASM_REWRITE_TAC[];
 934         FIRST_X_ASSUM MP_TAC;
 935         EXPAND_TAC "s'";
 936         REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
 937         BY(ASM_TAC THEN REAL_ARITH_TAC);
 938       BY(REWRITE_TAC[]);
 939     CONJ_TAC;
 940       REPEAT WEAKER_STRIP_TAC;
 941       INTRO_TAC deriv_form_taud_D2 [`x`;`y2`;`y3`;`y4`;`y5`;`y6`];
 942       REWRITE_TAC[Calc_derivative.derived_form;WITHINREAL_UNIV];
 943       ANTS_TAC;
 944         ASM_REWRITE_TAC[];
 945         FIRST_X_ASSUM MP_TAC;
 946         EXPAND_TAC "s'";
 947         REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
 948         BY(ASM_TAC THEN REAL_ARITH_TAC);
 949       BY(REWRITE_TAC[]);
 950     CONJ2_TAC;
 951       EXPAND_TAC "s'";
 952       REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
 953       REPEAT WEAKER_STRIP_TAC;
 954       FIRST_X_ASSUM MATCH_MP_TAC;
 955       REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
 956       BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
 957     COMMENT "last ant";
 958     MATCH_MP_TAC HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL;
 959     INTRO_TAC derived_form_taud_D3 [`z1`;`y2`;`y3`;`y4`;`y5`;`y6`];
 960     REPEAT WEAKER_STRIP_TAC;
 961     FIRST_X_ASSUM MP_TAC;
 962     REWRITE_TAC[Calc_derivative.derived_form];
 963     ANTS_TAC;
 964       FIRST_X_ASSUM MP_TAC;
 965       EXPAND_TAC "s'";
 966       REWRITE_TAC[IN_INTER;IN_ELIM_THM;IN_REAL_INTERVAL];
 967       BY(ASM_TAC THEN REAL_ARITH_TAC);
 968     REWRITE_TAC[WITHINREAL_UNIV];
 969     BY(MESON_TAC[]);
 970   COMMENT "down to 1";
 971   REPEAT WEAKER_STRIP_TAC;
 972   TYPIFY `&0 < sqrt(delta_y z1 y2 y3 y4 y5 y6)` (C SUBGOAL_THEN ASSUME_TAC);
 973     GMATCH_SIMP_TAC REAL_LT_RSQRT;
 974     BY(ASM_TAC THEN REAL_ARITH_TAC);
 975   CONJ_TAC;
 976     FIRST_X_ASSUM_ST `taud_D1_num_x` MP_TAC;
 977     REWRITE_TAC[REAL_DIV_EQ_0];
 978     BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
 979   FIRST_X_ASSUM_ST `taud_D2_num_x` MP_TAC;
 980   GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
 981   CONJ_TAC;
 982     MATCH_MP_TAC REAL_POW_LT;
 983     BY(ASM_REWRITE_TAC[]);
 984   BY(REAL_ARITH_TAC)
 985   ]);;
 986   (* }}} *)
 987
 988 let taud_minimizer_terminal_pent_cases = prove_by_refinement(
 989   ` main_nonlinear_terminal_v11 ==> (!d y1 y2 y3 y4 y5 y6.
 990   (let s = real_interval [&2,&2 * h0] INTER { q | d <= delta_y q y2 y3 y4 y5 y6} in
 991        (&0 <= d /\ y1 IN s /\ &2 <= y2 /\ y2 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 /\
 992          #3.01 <= y4 /\ y4 <= #3.237 /\ y5 = &2 /\ y6 = &2 ==>
 993           (?z1. z1 IN s /\ taud z1 y2 y3 y4 y5 y6  <= taud y1 y2 y3 y4 y5 y6 /\
 994           ( z1 = &2 \/ z1 = &2 * h0 \/ d = delta_y z1 y2 y3 y4 y5 y6 \/
 995               #0.12 <= taud z1 y2 y3 y4 y5 y6)))))`,
 996   (* {{{ proof *)
 997   [
 998   REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
 999   REPEAT WEAKER_STRIP_TAC;
1000   INTRO_TAC taud_minimizer [`&2`;`&2 * h0`;`d`;`y2`;`y3`;`y4`;`y5`;`y6`];
1001   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];
1002   ANTS_TAC;
1003     BY(ASM_MESON_TAC[]);
1004   REPEAT WEAKER_STRIP_TAC;
1005   TYPIFY `z1` EXISTS_TAC;
1006   CONJ_TAC;
1007     BY(ASM_MESON_TAC[]);
1008   CONJ_TAC;
1009     FIRST_X_ASSUM MATCH_MP_TAC;
1010     BY(ASM_MESON_TAC[]);
1011   INTRO_TAC taud_minimizer_cases [`&2`;`&2 * h0`;`d`;`z1`;`y2`;`y3`;`y4`;`y5`;`y6`];
1012   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];
1013   ANTS_TAC;
1014     BY(ASM_MESON_TAC[arith `&0 <= &2`;arith `&2 <= y ==> &0 <= y`]);
1015   ASM_CASES_TAC `z1 = &2` THEN FIRST_ASSUM (unlist REWRITE_TAC);
1016   ASM_CASES_TAC `z1 = &2 * h0` THEN FIRST_ASSUM (unlist REWRITE_TAC);
1017   ASM_CASES_TAC `d = delta_y z1 y2 y3 y4 y5 y6` THEN FIRST_ASSUM (unlist REWRITE_TAC);
1018   ASM_CASES_TAC `~(delta_y z1 y2 y3 y4 y5 y6 < &20)`;
1019     REPEAT WEAKER_STRIP_TAC;
1020     INTRO_TAC ((*--*)Terminal.get_main_nonlinear "1347067436") [`z1`;`y2`;`y3`;`y4`;`y5`;`y6`];
1021     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1022     ANTS_TAC;
1023       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1024     GMATCH_SIMP_TAC (GSYM Functional_equation.taud_x_taud);
1025     CONJ_TAC;
1026       BY(ASM_TAC THEN REAL_ARITH_TAC);
1027     BY(REPLICATE_TAC 3(FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1028   COMMENT "second get";
1029   DISCH_TAC;
1030   INTRO_TAC ((*--*)Terminal.get_main_nonlinear "6601228004") [`z1`;`y2`;`y3`;`y4`;`y5`;`y6`];
1031   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1032   ANTS_TAC;
1033     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1034   BY(ASM_TAC THEN REAL_ARITH_TAC)
1035   ]);;
1036   (* }}} *)
1037
1038 let taud_mud_126_x = prove_by_refinement(
1039   `!y3' y4' y5' y1 y2 y3 y4 y5 y6.
1040     &0 <= y1 /\ &0 <= y2  ==>
1041     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
1042     `,
1043   (* {{{ proof *)
1044   [
1045   REWRITE_TAC[Nonlin_def.mud_126_x;Nonlin_def.taud;Sphere.flat_term;];
1046   Functional_equation.F_REWRITE_TAC;
1047   REWRITE_TAC[Sphere.delta_126_x;GSYM Sphere.delta_y];
1048   REPEAT WEAKER_STRIP_TAC;
1049   REPEAT (GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx);
1050   ASM_REWRITE_TAC[];
1051   TYPIFY `delta_y y3 y1 y2 y6 y4 y5 = delta_y y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
1052     BY(MESON_TAC[Merge_ineq.delta_y_sym]);
1053   BY(REAL_ARITH_TAC)
1054   ]);;
1055   (* }}} *)
1056
1057 let taud_mud_135_x = prove_by_refinement(
1058   `!y2' y4' y6' y1 y2 y3 y4 y5 y6.
1059     &0 <= y1 /\ &0 <= y3  ==>
1060     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
1061     `,
1062   (* {{{ proof *)
1063   [
1064   REWRITE_TAC[Nonlin_def.mud_135_x;Nonlin_def.taud;Sphere.flat_term;];
1065   Functional_equation.F_REWRITE_TAC;
1066   REWRITE_TAC[Sphere.delta_135_x;GSYM Sphere.delta_y];
1067   REPEAT WEAKER_STRIP_TAC;
1068   REPEAT (GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx);
1069   ASM_REWRITE_TAC[];
1070   TYPIFY `delta_y y2 y1 y3 y5 y4 y6 = delta_y y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
1071     BY(MESON_TAC[Merge_ineq.delta_y_sym]);
1072   BY(REAL_ARITH_TAC)
1073   ]);;
1074   (* }}} *)
1075
1076 let mud_126_135 = prove_by_refinement(
1077   `!y1 y2 y3 y4 y5 y6 y3' y4' y5'. mud_126_x_v1 y3' y4' y5' y1 y2 y3 y4 y5 y6 =
1078     mud_135_x_v1 y3' y4' y5' y1 y3 y2 y4 y6 y5`,
1079   (* {{{ proof *)
1080   [
1081   REWRITE_TAC[Nonlin_def.mud_135_x;Nonlin_def.mud_126_x;];
1082   Functional_equation.F_REWRITE_TAC;
1083   REWRITE_TAC[Sphere.delta_135_x;Sphere.delta_126_x;GSYM Sphere.delta_y];
1084     BY(MESON_TAC[Merge_ineq.delta_x_sym]);
1085   ]);;
1086   (* }}} *)
1087
1088 let flat_term_2 = prove_by_refinement(
1089   `flat_term(&2) = -- sol0`,
1090   (* {{{ proof *)
1091   [
1092   REWRITE_TAC[Sphere.flat_term];
1093   Calc_derivative.CALC_ID_TAC;
1094   BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
1095   ]);;
1096   (* }}} *)
1097
1098 let flat_term_2h0 = prove_by_refinement(
1099   `flat_term(&2 * h0) = &0`,
1100   (* {{{ proof *)
1101   [
1102   REWRITE_TAC[Sphere.flat_term];
1103   BY(REAL_ARITH_TAC)
1104   ]);;
1105   (* }}} *)
1106
1107 let flat_term_sol0 = prove_by_refinement(
1108   `!y. &2 <= y  ==> --sol0 <= flat_term y`,
1109   (* {{{ proof *)
1110   [
1111   REWRITE_TAC[Sphere.flat_term];
1112   REPEAT WEAKER_STRIP_TAC;
1113   TYPIFY `sol0 * (y - &2 * h0)/(&2 * h0 - &2) = -- sol0 + sol0 * (y - &2) / (&2 * h0 - &2)` (C SUBGOAL_THEN SUBST1_TAC);
1114     Calc_derivative.CALC_ID_TAC;
1115     BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1116   MATCH_MP_TAC (arith `&0 <= x ==> h <= h + x`);
1117   GMATCH_SIMP_TAC REAL_LE_MUL;
1118   GMATCH_SIMP_TAC REAL_LE_RDIV_EQ;
1119   MP_TAC Flyspeck_constants.bounds;
1120   BY(REWRITE_TAC[Sphere.h0] THEN FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
1121   ]);;
1122   (* }}} *)
1123
1124 let taud_2h0 = prove_by_refinement(
1125   `!y2 y3 y4 y5 y6.
1126     &0 <= delta_y (&2 * h0) y2 y3 y4 y5 y6 /\
1127     y2 <= &2 * h0 /\ y3 <= &2 * h0 ==>
1128     &0 <= taud (&2 * h0) y2 y3 y4 y5 y6`,
1129   (* {{{ proof *)
1130   [
1131   REWRITE_TAC[Nonlin_def.taud;arith `x - x = &0 /\ &0 / x = &0 /\ x * &0 = &0 /\ &0 + x = x`];
1132   REPEAT WEAKER_STRIP_TAC;
1133   GMATCH_SIMP_TAC REAL_LE_MUL;
1134   CONJ_TAC;
1135     GMATCH_SIMP_TAC SQRT_POS_LE;
1136     BY(ASM_REWRITE_TAC[]);
1137   BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
1138   ]);;
1139   (* }}} *)
1140
1141 let quadratic_root_minus_works = prove_by_refinement(
1142   `!a b c.
1143             ~(a = &0) /\ &0 <= b pow 2 - &4 * a * c
1144             ==> (let x = -- ( b + sqrt(b pow 2 - &4 * a * c))/ (&2 * a) in
1145                  a * x pow 2 + b * x + c = &0)`,
1146   (* {{{ proof *)
1147   [
1148   REWRITE_TAC[LET_DEF;LET_END_DEF];
1149   REPEAT WEAKER_STRIP_TAC;
1150   Calc_derivative.CALC_ID_TAC;
1151   ASM_REWRITE_TAC[arith `~(&2 = &0)`];
1152   TYPED_ABBREV_TAC `d = b pow 2 - &4 * a * c`;
1153   TYPIFY `sqrt d * sqrt d = d` (C SUBGOAL_THEN MP_TAC);
1154     GMATCH_SIMP_TAC (GSYM SQRT_MUL);
1155     GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
1156     BY(ASM_REWRITE_TAC[]);
1157   FIRST_X_ASSUM MP_TAC;
1158   BY(CONV_TAC REAL_RING)
1159   ]);;
1160   (* }}} *)
1161
1162 let quadratic_root_imp_discr_nn = prove_by_refinement(
1163   `!a b c x.  (a * x pow 2 + b * x + c = &0) ==>
1164     &0 <= b pow 2 - &4 * a * c`,
1165   (* {{{ proof *)
1166   [
1167   REPEAT WEAKER_STRIP_TAC;
1168   TYPIFY `b pow 2 - &4 * a * c =  (&2 * a * x + b ) pow 2` (C SUBGOAL_THEN SUBST1_TAC);
1169     FIRST_X_ASSUM MP_TAC;
1170     BY(CONV_TAC REAL_RING);
1171   BY(REWRITE_TAC[ REAL_LE_POW_2])
1172   ]);;
1173   (* }}} *)
1174
1175 let quadratic_root_plus_eq = prove_by_refinement(
1176   `!a b c m x.
1177     (&0 < a) /\ (m <= x) /\ a * x pow 2 + b * x + c = &0 /\
1178     (&0 < &2 * m * a + b \/ (&2 * m * a + b) pow 2 < b pow 2 - &4 * a * c) ==>
1179        quadratic_root_plus (a,b,c) = x`,
1180   (* {{{ proof *)
1181   [
1182   REPEAT WEAKER_STRIP_TAC;
1183   MATCH_MP_TAC Tame_lemmas.quadratic_root_plus_gt_eq;
1184   TYPED_ABBREV_TAC  `y = -- (b + sqrt( b pow 2 - &4 * a * c)) / (&2 * a)` ;
1185   TYPIFY `y` EXISTS_TAC;
1186   ASM_REWRITE_TAC[];
1187   SUBCONJ_TAC;
1188     MATCH_MP_TAC quadratic_root_imp_discr_nn;
1189     BY(ASM_MESON_TAC[]);
1190   DISCH_TAC;
1191   CONJ_TAC;
1192     EXPAND_TAC "y";
1193     MATCH_MP_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] quadratic_root_minus_works);
1194     BY(ASM_REWRITE_TAC[] THEN ASM_TAC THEN REAL_ARITH_TAC);
1195   COMMENT "both cases";
1196   TYPIFY `y < m` ENOUGH_TO_SHOW_TAC;
1197     BY(ASM_TAC THEN REAL_ARITH_TAC);
1198   TYPIFY `&2 * a * y + b < &2 * a * m + b` ENOUGH_TO_SHOW_TAC;
1199     REWRITE_TAC[arith `&2 * a * y + b < &2 * a * m + b <=> a * y < a * m`];
1200     GMATCH_SIMP_TAC REAL_LT_LMUL_EQ;
1201     BY(ASM_REWRITE_TAC[]);
1202   TYPIFY `&2 * a * y + b  = -- sqrt(b pow 2 - &4 * a *c)` (C SUBGOAL_THEN SUBST1_TAC);
1203     EXPAND_TAC "y";
1204     Calc_derivative.CALC_ID_TAC;
1205     BY(ASM_TAC THEN REAL_ARITH_TAC);
1206   COMMENT "first case";
1207   ASM_CASES_TAC `&0 < &2 * m * a + b`;
1208     MATCH_MP_TAC REAL_LET_TRANS;
1209     TYPIFY `&0` EXISTS_TAC;
1210     ASM_REWRITE_TAC[];
1211     REWRITE_TAC[arith `-- x <= &0 <=> &0 <= x`];
1212     GMATCH_SIMP_TAC SQRT_POS_LE;
1213     BY(ASM_TAC THEN REAL_ARITH_TAC);
1214   FIRST_X_ASSUM DISJ_CASES_TAC;
1215     BY(ASM_MESON_TAC[]);
1216   TYPIFY `(&2 * m * a + b) pow 2 < sqrt (b pow 2 - &4 * a * c) pow 2` (C SUBGOAL_THEN MP_TAC);
1217     GMATCH_SIMP_TAC SQRT_POW_2;
1218     BY(ASM_REWRITE_TAC[]);
1219   TYPED_ABBREV_TAC `d = sqrt(b pow 2 - &4 * a * c) `;
1220   ONCE_REWRITE_TAC[arith `-- d < &2 * a * m + b <=> --d < &2 * m * a +b`];
1221   REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS];
1222   TYPIFY `&0 <= d` (C SUBGOAL_THEN MP_TAC);
1223     EXPAND_TAC "d";
1224     GMATCH_SIMP_TAC SQRT_POS_LE;
1225     BY(ASM_REWRITE_TAC[]);
1226   BY(ASM_TAC THEN REAL_ARITH_TAC)
1227   ]);;
1228   (* }}} *)
1229
1230 let edge2_flatD_x1_delta_lemma2 = prove_by_refinement(
1231   `!d x1 x2 x3 x4 x5 x6.
1232     delta_x x1 x2 x3 x4 x5 x6 = d /\
1233     &0 < x4 /\
1234     (delta_x1 x1 x2 x3 x4 x5 x6 < &0)
1235     ==>
1236     edge2_flatD_x1 d x2 x3 x4 x5 x6 = x1`,
1237   (* {{{ proof *)
1238   [
1239   REWRITE_TAC[Nonlin_def.edge2_flatD_x1];
1240   REPEAT WEAKER_STRIP_TAC;
1241   TYPED_ABBREV_TAC `b = (-- delta_x1 (&0) x2 x3 x4 x5 x6)`;
1242   TYPED_ABBREV_TAC `c = (d - delta_x (&0) x2 x3 x4 x5 x6)`;
1243   TYPIFY `!z. d - delta_x z x2 x3 x4 x5 x6 = x4 * z pow 2 + b * z + c` ((C SUBGOAL_THEN ASSUME_TAC));
1244     EXPAND_TAC "c";
1245     EXPAND_TAC "b";
1246     REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1];
1247     BY(REAL_ARITH_TAC);
1248   ASM_REWRITE_TAC[];
1249   REWRITE_TAC[Nonlinear_lemma.abc_quadratic];
1250   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);
1251     EXPAND_TAC "b";
1252     EXPAND_TAC "c";
1253     REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1;Sphere.ups_x];
1254     BY(REAL_ARITH_TAC);
1255   MATCH_MP_TAC quadratic_root_plus_eq;
1256   TYPIFY `x1` EXISTS_TAC;
1257   ASM_REWRITE_TAC[];
1258   REWRITE_TAC[arith `x <= x`];
1259   CONJ_TAC;
1260     FIRST_X_ASSUM (C INTRO_TAC [`x1`]);
1261     BY(ASM_TAC THEN REAL_ARITH_TAC);
1262   DISJ1_TAC;
1263   EXPAND_TAC "b";
1264   FIRST_X_ASSUM_ST `d < &0` MP_TAC;
1265   REWRITE_TAC[Nonlin_def.delta_x1];
1266   BY(REAL_ARITH_TAC)
1267   ]);;
1268   (* }}} *)
1269
1270 let edge2_flatD_x1_delta_lemma3 = prove_by_refinement(
1271   ` main_nonlinear_terminal_v11 ==> (!d y1 y2 y3 y4 y5 y6.
1272     delta_y y1 y2 y3 y4 y5 y6 = d /\
1273     &0 <= d /\ d <= &20 ==>
1274     (ineq     [(&2,y1,#2.52);
1275     (&2,y2,#2.52);
1276     (&2,y3,#2.52);
1277     (#3.01,y4,#3.915);
1278     (&2,y5,&2);
1279     (&2,y6,&2)
1280   ]
1281        (    edge2_flatD_x1 d (y2*y2) (y3*y3) (y4*y4) (y5*y5) (y6*y6) = y1*y1)))`,
1282   (* {{{ proof *)
1283   [
1284   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1285   REPEAT WEAKER_STRIP_TAC;
1286   MATCH_MP_TAC edge2_flatD_x1_delta_lemma2;
1287   INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3078028960") yys;
1288   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1289   ANTS_TAC;
1290     BY(ASM_REWRITE_TAC[]);
1291   ASM_REWRITE_TAC[];
1292   ASM_SIMP_TAC[arith `&0 <= d ==> ~(d < &0)`;arith `d <= &20 ==> ~(d > &20)`];
1293   REWRITE_TAC[Sphere.y_of_x;arith `y1 pow 2 = y1 * y1`];
1294   DISCH_THEN (unlist REWRITE_TAC);
1295   REWRITE_TAC[GSYM Sphere.delta_y];
1296   ASM_REWRITE_TAC[];
1297   GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
1298   BY(ASM_TAC THEN REAL_ARITH_TAC)
1299   ]);;
1300   (* }}} *)
1301
1302 let delta_diff = prove_by_refinement(
1303   `!x1 z1 x2 x3 x4 x5 x6.
1304     delta_x x1 x2 x3 x4 x5 x6 = delta_x z1 x2 x3 x4 x5 x6 +
1305     delta_x1 x1 x2 x3 x4 x5 x6 * (x1 - z1) + x4 * (x1 - z1) pow 2`,
1306   (* {{{ proof *)
1307   [
1308    BY(REWRITE_TAC[Sphere.delta_x;Nonlin_def.delta_x1] THEN REAL_ARITH_TAC)
1309   ]);;
1310   (* }}} *)
1311
1312 let delta_2_nn = prove_by_refinement(
1313   `main_nonlinear_terminal_v11 ==> (!z1 y2 y3 y4.
1314                            &2 <= z1 /\ z1 <= &2 * h0 /\
1315         &2 <= y2 /\ y2 <= &2 * h0 /\
1316         &2 <= y3 /\ y3 <= &2 * h0 /\
1317         #3.01 <= y4 /\ y4 <= #3.915 /\
1318         delta_y z1 y2 y3 y4 (&2) (&2) = &0 ==>
1319         &0 <= delta_y (&2)  y2 y3 y4 (&2) (&2))
1320     `,
1321   (* {{{ proof *)
1322   [
1323   REWRITE_TAC[Sphere.delta_y];
1324   REPEAT WEAKER_STRIP_TAC;
1325   INTRO_TAC (UNDISCH2 (Terminal.get_main_nonlinear "3078028960")) [`&2`;`y2`;`y3`;`y4`;`&2`;`&2`];
1326   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
1327   ANTS_TAC;
1328     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1329   REWRITE_TAC[Sphere.y_of_x;Sphere.delta_y];
1330   ASM_REWRITE_TAC[arith `~(&0 > &20)`];
1331   DISCH_TAC;
1332   FIRST_X_ASSUM DISJ_CASES_TAC;
1333     INTRO_TAC delta_diff [`&2* &2`;`z1 * z1`;`y2*y2`;`y3*y3`;`y4*y4`;`&2* &2`;`&2 * &2`];
1334     ASM_REWRITE_TAC[];
1335     DISCH_THEN SUBST1_TAC;
1336     MATCH_MP_TAC (arith `&0 <= x /\ &0 <= y ==> &0 <= &0 + x + y`);
1337     CONJ_TAC;
1338       ONCE_REWRITE_TAC[arith `&0 <= a * b <=> &0 <= (--a) *(--b)`];
1339       GMATCH_SIMP_TAC REAL_LE_MUL;
1340       CONJ_TAC;
1341         BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1342       TYPIFY `&2 * &2 <= z1 * z1` ENOUGH_TO_SHOW_TAC;
1343         BY(REAL_ARITH_TAC);
1344       GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
1345       BY(ASM_TAC THEN REAL_ARITH_TAC);
1346     GMATCH_SIMP_TAC REAL_LE_MUL;
1347     REWRITE_TAC[ REAL_LE_POW_2];
1348     BY(REWRITE_TAC[ REAL_LE_SQUARE]);
1349   BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
1350   ]);;
1351   (* }}} *)
1352
1353 let delta_mono = prove_by_refinement(
1354   ` main_nonlinear_terminal_v11 ==> (!z1 y1 y2 y3 y4 y5 y6.
1355         &2 <= y1 /\ y1 <= z1 /\ z1 <= &2 * h0 /\
1356         &2 <= y2 /\ y2 <= &2 * h0 /\
1357         &2 <= y3 /\ y3 <= &2 * h0 /\
1358         #3.01 <= y4 /\ y4 <= #3.915 /\
1359         &2 <= y5 /\ y5 <= &2  /\
1360         &2 <= y6 /\ y6 <= &2 /\
1361         &0 <= delta_y y1 y2 y3 y4 y5 y6 /\
1362         delta_y y1 y2 y3 y4 y5 y6 <= &20 ==>
1363         delta_y z1 y2 y3 y4 y5 y6 <= delta_y y1 y2 y3 y4 y5 y6)
1364 `,
1365   (* {{{ proof *)
1366   [
1367   REPEAT WEAKER_STRIP_TAC;
1368   REWRITE_TAC[Sphere.delta_y];
1369   INTRO_TAC delta_diff [`y1*y1`;`z1*z1`;`y2*y2`;`y3*y3`;`y4*y4`;`y5*y5`;`y6*y6`];
1370   DISCH_THEN SUBST1_TAC;
1371   MATCH_MP_TAC (arith `&0 <= b /\ &0 <= c ==> a <= a + b + c`);
1372   CONJ2_TAC;
1373     GMATCH_SIMP_TAC REAL_LE_MUL;
1374     REWRITE_TAC[ REAL_LE_POW_2];
1375     BY(REWRITE_TAC[ REAL_LE_SQUARE]);
1376   INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3078028960") yys;
1377   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
1378   ANTS_TAC;
1379     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1380   ASM_SIMP_TAC[arith `&0 <= d ==> ~(d < &0)`;arith `d <= d1 ==> ~(d > d1)`];
1381   REWRITE_TAC[Sphere.y_of_x];
1382   ONCE_REWRITE_TAC[arith `&0 <= x * y <=> &0 <= (-- x) * (-- y)`];
1383   DISCH_TAC;
1384   GMATCH_SIMP_TAC REAL_LE_MUL;
1385   CONJ_TAC;
1386     BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1387   MATCH_MP_TAC (arith `y1 * y1 <= z1 * z1 ==> &0 <= -- (y1 * y1 - z1 * z1)`);
1388   GMATCH_SIMP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE;
1389   BY(ASM_TAC THEN REAL_ARITH_TAC)
1390   ]);;
1391   (* }}} *)
1392
1393 let flat_term2_126_x_eval = prove_by_refinement(
1394   ` main_nonlinear_terminal_v11 ==> (!d z y1 y2 y3 y4 y5 y6.
1395     delta_y z y1 y2 y6 (&2) (&2) = d /\ &0 <= d /\ d <= &20 /\
1396       &2 <= z /\ z <= &2 * h0 /\ &2 <= y1 /\ y1 <= &2 * h0 /\
1397       &2 <= y2 /\ y2 <= &2 * h0 /\
1398       #3.01 <= y6 /\ y6 <= #3.915 ==>
1399     y_of_x (flat_term2_126_x d (&4) (&4)) y1 y2 y3 y4 y5 y6 = flat_term z)`,
1400   (* {{{ proof *)
1401   [
1402   REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x;Nonlin_def.flat_term2_126_x;Nonlin_def.edge2_126_x];
1403   REWRITE_TAC[Functional_equation.uni;Functional_equation.compose6;Functional_equation.constant6;Functional_equation.proj_x1;Functional_equation.proj_x2;Functional_equation.proj_x6];
1404   REPEAT WEAKER_STRIP_TAC;
1405   INTRO_TAC (UNDISCH2 edge2_flatD_x1_delta_lemma3) [`d`;`z`;`y1`;`y2`;`y6`;`&2`;`&2`];
1406   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
1407   ANTS_TAC;
1408     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1409   REWRITE_TAC[arith `&2 * &2 = &4`];
1410   DISCH_THEN SUBST1_TAC;
1411   REWRITE_TAC[Sphere.flat_term_x];
1412   GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
1413   BY(ASM_TAC THEN REAL_ARITH_TAC)
1414   ]);;
1415   (* }}} *)
1416
1417 let flat_term2_135_x_eval = prove_by_refinement(
1418   ` main_nonlinear_terminal_v11 ==> (!d z y1 y2 y3 y4 y5 y6.
1419     delta_y z y1 y3 y5 (&2) (&2) = d /\ &0 <= d /\ d <= &20 /\
1420       &2 <= z /\ z <= &2 * h0 /\ &2 <= y1 /\ y1 <= &2 * h0 /\
1421       &2 <= y3 /\ y3 <= &2 * h0 /\
1422       #3.01 <= y5 /\ y5 <= #3.915 ==>
1423     y_of_x (flat_term2_135_x d (&4) (&4)) y1 y2 y3 y4 y5 y6 = flat_term z)`,
1424   (* {{{ proof *)
1425   [
1426   REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x;Nonlin_def.flat_term2_135_x;Nonlin_def.edge2_135_x];
1427   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];
1428   REPEAT WEAKER_STRIP_TAC;
1429   INTRO_TAC (UNDISCH2 edge2_flatD_x1_delta_lemma3) [`d`;`z`;`y1`;`y3`;`y5`;`&2`;`&2`];
1430   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
1431   ANTS_TAC;
1432     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1433   REWRITE_TAC[arith `&2 * &2 = &4`];
1434   DISCH_THEN SUBST1_TAC;
1435   REWRITE_TAC[Sphere.flat_term_x];
1436   GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
1437   BY(ASM_TAC THEN REAL_ARITH_TAC)
1438   ]);;
1439   (* }}} *)
1440
1441 let delta_126_135 = prove_by_refinement(
1442   `!a b c y1 y2 y3 y4 y5 y6.
1443     delta_126_x a b c y1 y2 y3 y4 y5 y6 = delta_135_x a b c y1 y3 y2 y4 y6 y5`,
1444   (* {{{ proof *)
1445   [
1446   REWRITE_TAC[Sphere.delta_126_x;Sphere.delta_135_x];
1447   BY(MESON_TAC[Merge_ineq.delta_x_sym])
1448   ]);;
1449   (* }}} *)
1450
1451 let delta_126_x_2h0_le_d = prove_by_refinement(
1452   ` main_nonlinear_terminal_v11 ==> (!d z1 y1 y2 y3 y4 y5 y6.
1453                 &2 <= z1 /\
1454   z1 <= &2 * h0 /\
1455   z1 <= &2 * h0 /\
1456   &2 <= y1 /\
1457   y1 <= &2 * h0 /\
1458   &2 <= y2 /\
1459   y2 <= &2 * h0 /\
1460    #3.01 <= y6 /\
1461   y6 <=  #3.915 /\
1462   &0 <= d /\ d <= &20 /\
1463         delta_y z1 y1 y2 y6 (&2) (&2) = d ==>
1464       y_of_x (delta_126_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 <= d)`,
1465   (* {{{ proof *)
1466   [
1467   REPEAT WEAKER_STRIP_TAC;
1468   REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x];
1469   REWRITE_TAC[arith `&4 * h0 * h0 = (&2 * h0) * (&2 * h0)`];
1470   REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y];
1471   TYPIFY `delta_y y1 y2 (&2 * h0) (&2) (&2) y6 = delta_y (&2 * h0) y1 y2 y6 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC);
1472     BY(MESON_TAC[Merge_ineq.delta_y_sym]);
1473   INTRO_TAC (UNDISCH delta_mono) [`&2 * h0`;`z1`;`y1`;`y2`;`y6`;`&2`;`&2`];
1474   ANTS_TAC;
1475     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1476   BY(ASM_REWRITE_TAC[])
1477   ]);;
1478   (* }}} *)
1479
1480 let delta_135_x_2h0_le_d = prove_by_refinement(
1481   ` main_nonlinear_terminal_v11 ==> (!d z1 y1 y2 y3 y4 y5 y6.
1482                 &2 <= z1 /\
1483   z1 <= &2 * h0 /\
1484   z1 <= &2 * h0 /\
1485   &2 <= y1 /\
1486   y1 <= &2 * h0 /\
1487   &2 <= y3 /\
1488   y3 <= &2 * h0 /\
1489    #3.01 <= y5 /\
1490   y5 <=  #3.915 /\
1491   &0 <= d /\ d <= &20 /\
1492         delta_y z1 y1 y3 y5 (&2) (&2) = d ==>
1493       y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y2 y3 y4 y5 y6 <= d)`,
1494   (* {{{ proof *)
1495   [
1496   REPEAT WEAKER_STRIP_TAC;
1497   REWRITE_TAC[Sphere.y_of_x;Sphere.delta_135_x];
1498   REWRITE_TAC[arith `&4 * h0 * h0 = (&2 * h0) * (&2 * h0)`];
1499   REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y];
1500   TYPIFY `delta_y y1 (&2 * h0) y3 (&2) y5 (&2) = delta_y (&2 * h0) y1 y3 y5 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC);
1501     BY(MESON_TAC[Merge_ineq.delta_y_sym]);
1502   INTRO_TAC (UNDISCH delta_mono) [`&2 * h0`;`z1`;`y1`;`y3`;`y5`;`&2`;`&2`];
1503   ANTS_TAC;
1504     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1505   BY(ASM_REWRITE_TAC[])
1506   ]);;
1507   (* }}} *)
1508
1509 let lemma_5546286427 = prove_by_refinement(
1510   `  main_nonlinear_terminal_v11 ==> (!z1 y1 y2 y3 y4 y5 y6. ineq [
1511     (&2,y1,#2.52);
1512     (&2,y2,#2.52);
1513     (&2,y3,#2.52);
1514     (&2,y4,&2);
1515     (#3.01,y5,#3.237);
1516     (#3.01,y6,#3.237);
1517     (&2,z1,#2.52)
1518   ]
1519 (
1520   &0 = delta_y z1 y1 y2 y6 (&2) (&2) ==>
1521     (taum y1 y2 y3 y4 y5 y6 + flat_term z1 + #0.12 > #0.616)))`,
1522   (* {{{ proof *)
1523   [
1524   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
1525   REPEAT WEAKER_STRIP_TAC;
1526   INTRO_TAC ((*--*)Terminal.get_main_nonlinear "5546286427") yys;
1527   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
1528   ANTS_TAC;
1529     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1530   GMATCH_SIMP_TAC flat_term2_126_x_eval;
1531   TYPIFY `z1` EXISTS_TAC;
1532   CONJ_TAC;
1533     BY(ASM_REWRITE_TAC[] THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1534   COMMENT "remove delta_126_x";
1535   DISCH_THEN DISJ_CASES_TAC;
1536     BY(ASM_REWRITE_TAC[]);
1537   INTRO_TAC (UNDISCH2 delta_126_x_2h0_le_d) [`&0`;`z1`;`y1`;`y2`;`y3`;`y4`;`y5`;`y6`];
1538   ANTS_TAC;
1539     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1540   BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
1541   ]);;
1542   (* }}} *)
1543
1544 let taud_ge_flat_term = prove_by_refinement(
1545   `!y1 y2 y3 y4 y5 y6. y1 <= &2 * h0 /\ y2 <= &2 * h0 /\ y3 <= &2 * h0 /\
1546     &0 <= delta_y y1 y2 y3 y4 y5 y6 ==>
1547     flat_term y1 <= taud y1 y2 y3 y4 y5 y6`,
1548   (* {{{ proof *)
1549   [
1550   REWRITE_TAC[Nonlin_def.taud;Sphere.flat_term];
1551   REPEAT WEAKER_STRIP_TAC;
1552   REWRITE_TAC[arith `a <= a + b <=> &0 <= b`];
1553   GMATCH_SIMP_TAC REAL_LE_MUL;
1554   GMATCH_SIMP_TAC SQRT_POS_LE;
1555   ASM_REWRITE_TAC[];
1556   BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
1557   ]);;
1558   (* }}} *)
1559
1560 let terminal_pent_taum126_012 = prove_by_refinement(
1561   `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
1562       #0.12 <= taud y126 y1 y2 y6 (&2) (&2) /\
1563       &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
1564      (ineq [
1565        (&2,y1,&2 * h0);
1566        (&2,y2,&2 * h0);
1567        (&2,y3,&2 * h0);
1568        (&2,y4,&2);
1569        (#3.01,y5,#3.237);
1570        (#3.01,y6,#3.237);
1571        (&2,y126,&2 * h0);
1572        (&2,y135,&2 * h0)
1573      ]
1574      (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
1575      `,
1576   (* {{{ proof *)
1577   [
1578   REWRITE_TAC[Sphere.ineq];
1579   REPEAT WEAKER_STRIP_TAC;
1580   INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&0`;`y135`;`y1`;`y3`;`y5`;`(&2)`;`&2`];
1581   REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
1582   ANTS_TAC;
1583     BY(ASM_TAC THEN REAL_ARITH_TAC);
1584   REPEAT WEAKER_STRIP_TAC;
1585   INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3665919985") yys;
1586   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1587   ANTS_TAC;
1588     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1589   REWRITE_TAC[arith `x > y <=> y < x`];
1590   DISCH_TAC;
1591   INTRO_TAC (UNDISCH OWZLKVY4) [`y135`;`y1`;`y3`;`y5`;`&2`;`&2`];
1592   ANTS_TAC;
1593     BY(REWRITE_TAC[Sphere.cstab] THEN ASM_TAC THEN REAL_ARITH_TAC);
1594   DISCH_TAC;
1595   INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3665919985") yys;
1596   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1597   ANTS_TAC;
1598     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1599   DISCH_TAC;
1600   COMMENT "case y=2";
1601   FIRST_X_ASSUM (DISJ_CASES_TAC);
1602     INTRO_TAC ((*--*)Terminal.get_main_nonlinear "7903347843") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1603     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1604     ANTS_TAC;
1605       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1606     REWRITE_TAC[Sphere.y_of_x;mud_126_135];
1607     REWRITE_TAC[GSYM Sphere.y_of_x];
1608     TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
1609       BY(MESON_TAC[Terminal.taum_sym]);
1610     GMATCH_SIMP_TAC taud_mud_135_x;
1611     CONJ_TAC;
1612       BY(ASM_TAC THEN REAL_ARITH_TAC);
1613     MATCH_MP_TAC (arith `x <= a + b   ==> t + x > #0.616 ==> #0.616 < a + t + b`);
1614     MATCH_MP_TAC (arith `t2 <= t135 /\ -- s <= f /\ #0.12 <= t126 ==> t2 - f - s + #0.12 <= t126+t135`);
1615     ASM_REWRITE_TAC[];
1616     CONJ_TAC;
1617       FIRST_X_ASSUM_ST `<=` MP_TAC THEN ASM_REWRITE_TAC[];
1618       FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
1619       BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1620     MATCH_MP_TAC flat_term_sol0;
1621     BY(REAL_ARITH_TAC);
1622   COMMENT "case &0 <= tau";
1623   ASM_CASES_TAC `&0 <= taud y135 y1 y3 y5 (&2) (&2)`;
1624     BY(ASM_TAC THEN REAL_ARITH_TAC);
1625   COMMENT "case y=&2*h0";
1626   FIRST_X_ASSUM (DISJ_CASES_TAC);
1627     INTRO_TAC taud_2h0 [`y1`;`y3`;`y5`;`&2`;`&2`];
1628     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1629     FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
1630     ANTS_TAC;
1631       BY(ASM_TAC THEN REAL_ARITH_TAC);
1632     BY(REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1633   COMMENT "case delta=0";
1634   FIRST_X_ASSUM DISJ_CASES_TAC;
1635     INTRO_TAC (UNDISCH lemma_5546286427) [`z1`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1636     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
1637     ANTS_TAC;
1638       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1639     TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
1640       BY(MESON_TAC[Terminal.taum_sym]);
1641     DISCH_TAC;
1642     INTRO_TAC taud_ge_flat_term [`z1`;`y1`;`y3`;`y5`;`&2`;`&2`];
1643     ANTS_TAC;
1644       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1645     BY(ASM_TAC THEN REAL_ARITH_TAC);
1646   COMMENT "final case";
1647   BY(ASM_TAC THEN REAL_ARITH_TAC)
1648   ]);;
1649   (* }}} *)
1650
1651 let terminal_pent_tau135_012 = prove_by_refinement(
1652   `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
1653       #0.12 <= taud y135 y1 y3 y5 (&2) (&2) /\
1654       &0 <= delta_y y126 y1 y2 y6 (&2) (&2) ==>
1655      (ineq [
1656        (&2,y1,&2 * h0);
1657        (&2,y2,&2 * h0);
1658        (&2,y3,&2 * h0);
1659        (&2,y4,&2);
1660        (#3.01,y5,#3.237);
1661        (#3.01,y6,#3.237);
1662        (&2,y126,&2 * h0);
1663        (&2,y135,&2 * h0)
1664      ]
1665      (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
1666      `,
1667   (* {{{ proof *)
1668   [
1669   REWRITE_TAC[Sphere.ineq];
1670   REPEAT WEAKER_STRIP_TAC;
1671   INTRO_TAC (UNDISCH2 terminal_pent_taum126_012) [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`;`y135`;`y126`];
1672   ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1673   TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
1674     BY(REWRITE_TAC[Terminal.taum_sym]);
1675   BY(REAL_ARITH_TAC)
1676   ]);;
1677   (* }}} *)
1678
1679 let sqrt20 = prove_by_refinement(
1680   `#4.47 <= sqrt(&20)`,
1681   (* {{{ proof *)
1682   [
1683   MATCH_MP_TAC REAL_LE_RSQRT;
1684   BY(REAL_ARITH_TAC)
1685   ]);;
1686   (* }}} *)
1687
1688 let taud_053 = prove_by_refinement(
1689   `! y2 y3 y4 y5 y6.
1690     y2 <= &2 * h0 /\
1691     y3 <= &2 * h0 /\
1692     &20 <= delta_y (&2 * h0) y2 y3 y4 y5 y6 ==>
1693     #0.053 <= taud (&2 * h0) y2 y3 y4 y5 y6`,
1694   (* {{{ proof *)
1695   [
1696   REWRITE_TAC[Nonlin_def.taud];
1697   REPEAT WEAKER_STRIP_TAC;
1698   TYPIFY `sol0 * (&2 * h0 - &2 * h0) / (&2 * h0 - &2) = &0` (C SUBGOAL_THEN SUBST1_TAC);
1699     BY(REAL_ARITH_TAC);
1700   TYPIFY `#0.053 = #4.47 * (#0.053 / #4.47)` (C SUBGOAL_THEN SUBST1_TAC);
1701     BY(REAL_ARITH_TAC);
1702   REWRITE_TAC[arith `&0 + x= x`];
1703   MATCH_MP_TAC REAL_LE_MUL2;
1704   CONJ_TAC;
1705     BY(REAL_ARITH_TAC);
1706   CONJ_TAC;
1707     MATCH_MP_TAC REAL_LE_TRANS;
1708     TYPIFY `sqrt(&20)` EXISTS_TAC;
1709     REWRITE_TAC[sqrt20];
1710     GMATCH_SIMP_TAC SQRT_MONO_LE_EQ;
1711     BY(ASM_TAC THEN REAL_ARITH_TAC);
1712   CONJ_TAC;
1713     BY(REAL_ARITH_TAC);
1714   BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
1715   ]);;
1716   (* }}} *)
1717
1718 let terminal_pent_tau126_2 = prove_by_refinement(
1719   `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
1720      y126 = &2 /\
1721       &0 <= delta_y y126 y1 y2 y6 (&2) (&2) /\
1722       &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
1723      (ineq [
1724        (&2,y1,&2 * h0);
1725        (&2,y2,&2 * h0);
1726        (&2,y3,&2 * h0);
1727        (&2,y4,&2);
1728        (#3.01,y5,#3.237);
1729        (#3.01,y6,#3.237);
1730        (&2,y126,&2 * h0);
1731        (&2,y135,&2 * h0)
1732      ]
1733      (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
1734      `,
1735   (* {{{ proof *)
1736   [
1737   REWRITE_TAC[Sphere.ineq];
1738   REPEAT WEAKER_STRIP_TAC;
1739   INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&0`;`y135`;`y1`;`y3`;`y5`;`(&2)`;`&2`];
1740   REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
1741   ANTS_TAC;
1742     BY(ASM_TAC THEN REAL_ARITH_TAC);
1743   REPEAT WEAKER_STRIP_TAC;
1744   TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC);
1745     BY(MESON_TAC[Terminal.taum_sym]);
1746   COMMENT "case tau >= 0.12";
1747   ASM_CASES_TAC `#0.12 <= taud z1 y1 y3 y5 (&2) (&2)`;
1748     INTRO_TAC (UNDISCH2 terminal_pent_tau135_012) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`y135`];
1749     ANTS_TAC;
1750       BY(ASM_TAC THEN REAL_ARITH_TAC);
1751     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1752     ANTS_TAC;
1753       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1754     BY(REWRITE_TAC[]);
1755   COMMENT "case z1= &2";
1756   ASM_CASES_TAC `z1 = &2`;
1757     INTRO_TAC ((*--*)Terminal.get_main_nonlinear "7997589055") yys;
1758     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1759     ANTS_TAC;
1760       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1761     GMATCH_SIMP_TAC taud_mud_126_x;
1762     GMATCH_SIMP_TAC taud_mud_135_x;
1763     REWRITE_TAC[flat_term_2];
1764     TYPIFY_GOAL_THEN ` &0 <= y1 /\ &0 <= y2 /\ &0 <= y3` (unlist REWRITE_TAC);
1765       BY(ASM_TAC THEN REAL_ARITH_TAC);
1766     ASM_REWRITE_TAC[];
1767     REPEAT (FIRST_X_ASSUM_ST `x = &2` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
1768     BY(ASM_TAC THEN REAL_ARITH_TAC);
1769   COMMENT "case delta=0";
1770   ASM_CASES_TAC `&0 = delta_y z1 y1 y3 y5 (&2) (&2)`;
1771     INTRO_TAC ((*--*)Terminal.get_main_nonlinear "2565248885") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1772     REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1773     ANTS_TAC;
1774       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1775     REWRITE_TAC[arith `x > &0 <=> ~(x <= &0)`];
1776     GMATCH_SIMP_TAC (UNDISCH2 delta_126_x_2h0_le_d);
1777     CONJ_TAC;
1778       TYPIFY `z1` EXISTS_TAC;
1779       BY(ASM_TAC THEN REAL_ARITH_TAC);
1780     GMATCH_SIMP_TAC taud_mud_135_x;
1781     REWRITE_TAC[flat_term_2];
1782     GMATCH_SIMP_TAC (UNDISCH2 flat_term2_126_x_eval);
1783     TYPIFY `z1` EXISTS_TAC;
1784     CONJ_TAC;
1785       BY(ASM_TAC THEN REAL_ARITH_TAC);
1786     CONJ_TAC;
1787       BY(ASM_TAC THEN REAL_ARITH_TAC);
1788     INTRO_TAC taud_ge_flat_term [`z1`;`y1`;`y3`;`y5`;`&2`;`&2`];
1789     ANTS_TAC;
1790       BY(ASM_TAC THEN REAL_ARITH_TAC);
1791     REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[];
1792     BY(REAL_ARITH_TAC);
1793   COMMENT "case delta>=20";
1794   TYPIFY `z1 = &2 * h0` (C SUBGOAL_THEN MP_TAC);
1795     BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
1796   DISCH_TAC;
1797   ASM_CASES_TAC `&20 <= delta_y z1 y1 y3 y5 (&2) (&2)`;
1798     INTRO_TAC ((*--*)Terminal.get_main_nonlinear "2320951108") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1799     REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1800     ANTS_TAC;
1801       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1802     GMATCH_SIMP_TAC taud_mud_135_x;
1803     REWRITE_TAC[flat_term_2];
1804     INTRO_TAC taud_053 [`y1`;`y3`;`y5`;`&2`;`&2`];
1805     ANTS_TAC;
1806       FIRST_X_ASSUM MP_TAC;
1807       BY(ASM_REWRITE_TAC[]);
1808     ASM_REWRITE_TAC[];
1809     REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
1810     DISCH_TAC;
1811     CONJ_TAC;
1812       BY(ASM_TAC THEN REAL_ARITH_TAC);
1813     REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC);
1814     BY(REAL_ARITH_TAC);
1815   COMMENT "case delta <= 20";
1816   INTRO_TAC ((*--*)Terminal.get_main_nonlinear "5429238960") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1817   REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1818   ANTS_TAC;
1819     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1820   GMATCH_SIMP_TAC taud_mud_135_x;
1821   REWRITE_TAC[flat_term_2];
1822   CONJ_TAC;
1823     BY(ASM_TAC THEN REAL_ARITH_TAC);
1824   INTRO_TAC (UNDISCH2 delta_126_x_2h0_le_d) [`delta_y z1 y1 y3 y5 (&2) (&2)`;`z1`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1825   ANTS_TAC;
1826     BY(ASM_TAC THEN REAL_ARITH_TAC);
1827   INTRO_TAC taud_2h0 [`y1`;`y3`;`y5`;`&2`;`&2`];
1828   ANTS_TAC;
1829     FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
1830     BY(ASM_TAC THEN REAL_ARITH_TAC);
1831   ASM_REWRITE_TAC[];
1832   REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
1833   BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
1834   ]);;
1835   (* }}} *)
1836
1837 let terminal_pent_tau135_2 = prove_by_refinement(
1838   `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
1839      y135 = &2 /\
1840       &0 <= delta_y y126 y1 y2 y6 (&2) (&2) /\
1841       &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
1842      (ineq [
1843        (&2,y1,&2 * h0);
1844        (&2,y2,&2 * h0);
1845        (&2,y3,&2 * h0);
1846        (&2,y4,&2);
1847        (#3.01,y5,#3.237);
1848        (#3.01,y6,#3.237);
1849        (&2,y126,&2 * h0);
1850        (&2,y135,&2 * h0)
1851      ]
1852      (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
1853      `,
1854   (* {{{ proof *)
1855   [
1856   REWRITE_TAC[Sphere.ineq];
1857   REPEAT WEAKER_STRIP_TAC;
1858   INTRO_TAC (UNDISCH2 terminal_pent_tau126_2) [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`;`y135`;`y126`];
1859   ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1860   TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN SUBST1_TAC);
1861     BY(REWRITE_TAC[Terminal.taum_sym]);
1862   BY(REAL_ARITH_TAC)
1863   ]);;
1864   (* }}} *)
1865
1866 let terminal_pent_tau126_2h0 = prove_by_refinement(
1867   `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
1868      y126 = &2 * h0 /\
1869       &20 <= delta_y y126 y1 y2 y6 (&2) (&2) /\
1870       &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
1871      (ineq [
1872        (&2,y1,&2 * h0);
1873        (&2,y2,&2 * h0);
1874        (&2,y3,&2 * h0);
1875        (&2,y4,&2);
1876        (#3.01,y5,#3.237);
1877        (#3.01,y6,#3.237);
1878        (&2,y126,&2 * h0);
1879        (&2,y135,&2 * h0)
1880      ]
1881      (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
1882      `,
1883   (* {{{ proof *)
1884   [
1885   REWRITE_TAC[Sphere.ineq];
1886   REPEAT WEAKER_STRIP_TAC;
1887   INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&0`;`y135`;`y1`;`y3`;`y5`;`(&2)`;`&2`];
1888   REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
1889   ANTS_TAC;
1890     BY(ASM_TAC THEN REAL_ARITH_TAC);
1891   REPEAT WEAKER_STRIP_TAC;
1892   TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC);
1893     BY(MESON_TAC[Terminal.taum_sym]);
1894   COMMENT "case tau >= 0.12";
1895   ASM_CASES_TAC `#0.12 <= taud z1 y1 y3 y5 (&2) (&2)`;
1896     INTRO_TAC (UNDISCH2 terminal_pent_tau135_012) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`y135`];
1897     ANTS_TAC;
1898       BY(ASM_TAC THEN REAL_ARITH_TAC);
1899     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1900     ANTS_TAC;
1901       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1902     BY(REWRITE_TAC[]);
1903   COMMENT "case z1= &2";
1904   ASM_CASES_TAC `z1 = &2`;
1905     INTRO_TAC (UNDISCH2 terminal_pent_tau135_2) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`z1`];
1906     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1907     ANTS_TAC;
1908       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1909     BY(ASM_TAC THEN REAL_ARITH_TAC);
1910   COMMENT "case delta = 0";
1911   ASM_CASES_TAC `&0 = delta_y z1 y1 y3 y5 (&2) (&2)`;
1912     INTRO_TAC ((*--*)Terminal.get_main_nonlinear "1948775510") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1913     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1914     ANTS_TAC;
1915       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1916     GMATCH_SIMP_TAC (taud_mud_135_x);
1917     CONJ_TAC;
1918       BY(ASM_TAC THEN REAL_ARITH_TAC);
1919     REWRITE_TAC[flat_term_2h0];
1920     GMATCH_SIMP_TAC flat_term2_126_x_eval;
1921     TYPIFY `z1` EXISTS_TAC;
1922     CONJ_TAC;
1923       ASM_REWRITE_TAC[];
1924       BY(ASM_TAC THEN REAL_ARITH_TAC);
1925     INTRO_TAC taud_ge_flat_term [`z1`;`y1`;`y3`;`y5`;`&2`;`&2`];
1926     ANTS_TAC;
1927       BY(ASM_TAC THEN REAL_ARITH_TAC);
1928     INTRO_TAC (UNDISCH2 delta_126_x_2h0_le_d) [`&0`;`z1`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1929     ANTS_TAC;
1930       BY(ASM_TAC THEN REAL_ARITH_TAC);
1931     REWRITE_TAC[arith `x > &0 <=> ~(x <= &0)`] THEN DISCH_THEN (unlist REWRITE_TAC);
1932     REWRITE_TAC[Sphere.delta_135_x;Sphere.y_of_x;arith `&4 * h0 * h0 = (&2 * h0) * (&2 * h0)`];
1933     REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y];
1934     TYPIFY `delta_y y1 (&2 * h0) y2 (&2) y6 (&2) = delta_y y126 y1 y2 y6 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC);
1935       ASM_REWRITE_TAC[];
1936       BY(MESON_TAC[Merge_ineq.delta_y_sym]);
1937     FIRST_X_ASSUM kill;
1938     ASM_REWRITE_TAC[];
1939     REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
1940     BY(ASM_TAC THEN REAL_ARITH_TAC);
1941   COMMENT "case z1=2h0, delta>=20";
1942   TYPIFY `z1 = &2 * h0` (C SUBGOAL_THEN MP_TAC);
1943     BY(ASM_MESON_TAC[]);
1944   DISCH_TAC;
1945   INTRO_TAC taud_053 [`y1`;`y2`;`y6`;`&2`;`&2`];
1946   ANTS_TAC;
1947     ASM_REWRITE_TAC[];
1948     BY(FIRST_X_ASSUM_ST `&20 <= d` MP_TAC THEN ASM_REWRITE_TAC[]);
1949   DISCH_TAC;
1950   ASM_CASES_TAC `&20 <= delta_y z1 y1 y3 y5 (&2) (&2)`;
1951     INTRO_TAC taud_053 [`y1`;`y3`;`y5`;`&2`;`&2`];
1952     ANTS_TAC;
1953       ASM_REWRITE_TAC[];
1954       BY(REPEAT (FIRST_X_ASSUM_ST `&20 <= d` MP_TAC) THEN ASM_REWRITE_TAC[]);
1955     DISCH_TAC;
1956     INTRO_TAC ((*--*)Terminal.get_main_nonlinear "3665919985") yys;
1957     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
1958     ANTS_TAC;
1959       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1960     ASM_REWRITE_TAC[];
1961     REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
1962     REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[];
1963     BY(REAL_ARITH_TAC);
1964   COMMENT "case z1=2h0, delta<=20";
1965   INTRO_TAC ((*--*)Terminal.get_main_nonlinear "5708641738") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1966   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`;LET_DEF;LET_END_DEF];
1967   ANTS_TAC;
1968     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
1969   INTRO_TAC (UNDISCH2 delta_126_x_2h0_le_d) [`delta_y z1 y1 y3 y5 (&2) (&2)`;`z1`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
1970   ANTS_TAC;
1971     BY(ASM_TAC THEN REAL_ARITH_TAC);
1972   ASM_REWRITE_TAC[];
1973   REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
1974   INTRO_TAC taud_2h0 [`y1`;`y3`;`y5`;`&2`;`&2`];
1975   ANTS_TAC;
1976     BY(ASM_TAC THEN ASM_MESON_TAC[]);
1977   BY(ASM_TAC THEN REAL_ARITH_TAC)
1978   ]);;
1979   (* }}} *)
1980
1981 let taud_sqrt20 = prove_by_refinement(
1982   ` main_nonlinear_terminal_v11 ==> (!z1 y1 y2 y3 y4 y5 y6.
1983      &0 <= &20 /\
1984       &20 <= &20 /\
1985       &2 <= z1 /\
1986       z1 <= &2 * h0 /\
1987       &2 <= y1 /\
1988       y1 <= &2 * h0 /\
1989       &2 <= y3 /\
1990       y3 <= &2 * h0 /\
1991        #3.01 <= y5 /\
1992       y5 <=  #3.915 /\
1993     delta_y z1 y1 y3 y5 (&2) (&2) = &20 ==>
1994     y_of_x (flat_term2_135_x (&20) (&4) (&4)) y1 y2 y3 y4 y5 y6 +
1995         (#0.012 +  #0.01 * (#2.52 * &2 - y1 - y3 )) * #4.47 <= taud z1 y1 y3 y5 (&2) (&2))`,
1996   (* {{{ proof *)
1997   [
1998   REPEAT WEAKER_STRIP_TAC;
1999   GMATCH_SIMP_TAC flat_term2_135_x_eval;
2000   TYPIFY `z1` EXISTS_TAC;
2001   ASM_REWRITE_TAC[];
2002   REWRITE_TAC[Nonlin_def.taud;Sphere.flat_term];
2003   REWRITE_TAC[ (arith `u + c * s <= u + s' * c' <=> c * s <= c' * s'`)];
2004   MATCH_MP_TAC REAL_LE_MUL2;
2005   CONJ_TAC;
2006     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2007   ASM_REWRITE_TAC[sqrt20];
2008   BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
2009   ]);;
2010   (* }}} *)
2011
2012 let terminal_pent_tau126_delta20 = prove_by_refinement(
2013   `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
2014       delta_y y126 y1 y2 y6 (&2) (&2) = &20 /\
2015       &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
2016      (ineq [
2017        (&2,y1,&2 * h0);
2018        (&2,y2,&2 * h0);
2019        (&2,y3,&2 * h0);
2020        (&2,y4,&2);
2021        (#3.01,y5,#3.237);
2022        (#3.01,y6,#3.237);
2023        (&2,y126,&2 * h0);
2024        (&2,y135,&2 * h0)
2025      ]
2026      (#0.616 < taud y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taud y135 y1 y3 y5 (&2) (&2))))
2027      `,
2028   (* {{{ proof *)
2029   [
2030   REWRITE_TAC[Sphere.ineq];
2031   REPEAT WEAKER_STRIP_TAC;
2032   INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&0`;`y135`;`y1`;`y3`;`y5`;`(&2)`;`&2`];
2033   REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
2034   ANTS_TAC;
2035     BY(ASM_TAC THEN REAL_ARITH_TAC);
2036   REPEAT WEAKER_STRIP_TAC;
2037   TYPIFY `taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC);
2038     BY(MESON_TAC[Terminal.taum_sym]);
2039   COMMENT "case tau >= 0.12";
2040   ASM_CASES_TAC `#0.12 <= taud z1 y1 y3 y5 (&2) (&2)`;
2041     INTRO_TAC (UNDISCH2 terminal_pent_tau135_012) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`y135`];
2042     ANTS_TAC;
2043       BY(ASM_TAC THEN REAL_ARITH_TAC);
2044     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2045     ANTS_TAC;
2046       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2047     BY(REWRITE_TAC[]);
2048   COMMENT "case z1= &2";
2049   ASM_CASES_TAC `z1 = &2`;
2050     INTRO_TAC (UNDISCH2 terminal_pent_tau135_2) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`y126`;`z1`];
2051     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2052     ANTS_TAC;
2053       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2054     BY(ASM_TAC THEN REAL_ARITH_TAC);
2055   COMMENT "delta issue";
2056   TYPIFY `~( y_of_x (delta_135_x (&4 * h0 * h0) (&4) (&4)) y1 y3 y2 y4 y6 y5 > &20 )` (C SUBGOAL_THEN MP_TAC);
2057     REWRITE_TAC[arith `~(x > d) <=> (x<=d)`];
2058     GMATCH_SIMP_TAC delta_135_x_2h0_le_d;
2059     TYPIFY `y126` EXISTS_TAC;
2060     ASM_REWRITE_TAC[];
2061     BY(ASM_TAC THEN REAL_ARITH_TAC);
2062   DISCH_TAC;
2063   COMMENT "case delta = 0";
2064   ASM_CASES_TAC `&0 = delta_y z1 y1 y3 y5 (&2) (&2)`;
2065     INTRO_TAC ((*--*)Terminal.get_main_nonlinear "1008824382") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
2066     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2067     ANTS_TAC;
2068       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2069     GMATCH_SIMP_TAC flat_term2_126_x_eval;
2070     TYPIFY `z1` EXISTS_TAC;
2071     CONJ_TAC;
2072       ASM_REWRITE_TAC[];
2073       BY(ASM_TAC THEN REAL_ARITH_TAC);
2074     GMATCH_SIMP_TAC flat_term2_135_x_eval;
2075     TYPIFY `y126` EXISTS_TAC;
2076     CONJ_TAC;
2077       FIRST_X_ASSUM_ST `d = &20` SUBST1_TAC;
2078       ASM_REWRITE_TAC[];
2079       BY(ASM_TAC THEN REAL_ARITH_TAC);
2080     INTRO_TAC mu_y_ft_combine2 [`y126`;`y1`;`y2`];
2081     ANTS_TAC;
2082       BY(ASM_REWRITE_TAC[]);
2083     TYPIFY `mu_y y126 y1 y2 * sqrt(&20) + flat_term y126 <= taud y126 y1 y2 y6 (&2) (&2)` (C SUBGOAL_THEN MP_TAC);
2084       REWRITE_TAC[Nonlin_def.taud;Nonlin_def.mu_y;Sphere.flat_term];
2085       REWRITE_TAC[ (arith `c * s + u <= u + s' * c <=> c * s <= c * s'`)];
2086       GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP;
2087       CONJ_TAC;
2088         BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2089       GMATCH_SIMP_TAC SQRT_MONO_LE_EQ;
2090       BY(ASM_TAC THEN REAL_ARITH_TAC);
2091     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);
2092       REWRITE_TAC[Nonlin_def.mu_y];
2093       MATCH_MP_TAC REAL_LE_MUL2;
2094       CONJ_TAC;
2095         BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2096       REWRITE_TAC[sqrt20];
2097       BY(REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2098     INTRO_TAC taud_ge_flat_term [`z1`;`y1`;`y3`;`y5`;`&2`;`&2`];
2099     ANTS_TAC;
2100       BY(ASM_TAC THEN REAL_ARITH_TAC);
2101     FIRST_X_ASSUM_ST `~` (unlist REWRITE_TAC);
2102     REWRITE_TAC[arith `x > &0 <=> ~(x <= &0)`];
2103     GMATCH_SIMP_TAC delta_126_x_2h0_le_d;
2104     CONJ_TAC;
2105       TYPIFY `z1` EXISTS_TAC;
2106       ASM_REWRITE_TAC[];
2107       BY(ASM_TAC THEN REAL_ARITH_TAC);
2108     ASM_REWRITE_TAC[];
2109     REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
2110     REWRITE_TAC[flat_term_2h0];
2111     BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2112   COMMENT "z1=2h0 and delta <=20";
2113   TYPIFY `z1 = &2 * h0` (C SUBGOAL_THEN ASSUME_TAC);
2114     BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
2115   ASM_CASES_TAC `delta_y z1 y1 y3 y5 (&2) (&2) <= &20`;
2116     INTRO_TAC ((*--*)Terminal.get_main_nonlinear "1586903463") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
2117     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2118     ANTS_TAC;
2119       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2120     INTRO_TAC taud_2h0 [`y1`;`y3`;`y5`;`&2`;`&2`];
2121     ANTS_TAC;
2122       BY(REPEAT (FIRST_X_ASSUM_ST `<=` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
2123     INTRO_TAC (UNDISCH2 taud_sqrt20) [`y126`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
2124     ANTS_TAC;
2125       BY(ASM_TAC THEN REAL_ARITH_TAC);
2126     ASM_REWRITE_TAC[];
2127     REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x;arith `&4 * h0 * h0 =  (&2 * h0) * (&2 * h0)`];
2128     REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y];
2129     TYPIFY `delta_y y1 y3 (&2 * h0) (&2) (&2) y5 = delta_y z1 y1 y3 y5 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC);
2130       ASM_REWRITE_TAC[];
2131       BY(MESON_TAC[Merge_ineq.delta_y_sym]);
2132     ASM_REWRITE_TAC[];
2133     REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
2134     BY(ASM_TAC THEN REAL_ARITH_TAC);
2135   COMMENT "z1=2h0 and delta> 20";
2136   INTRO_TAC ((*--*)Terminal.get_main_nonlinear "8875146520") [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
2137   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2138   ANTS_TAC;
2139     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2140   GMATCH_SIMP_TAC taud_mud_126_x;
2141   REWRITE_TAC[flat_term_2h0];
2142   INTRO_TAC (UNDISCH2 taud_sqrt20) [`y126`;`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
2143   ANTS_TAC;
2144     BY(ASM_TAC THEN REAL_ARITH_TAC);
2145   FIRST_X_ASSUM_ST `y_of_x` (unlist REWRITE_TAC);
2146   REWRITE_TAC[Sphere.y_of_x;Sphere.delta_126_x;arith `&4 * h0 * h0 =  (&2 * h0) * (&2 * h0)`];
2147   REWRITE_TAC[arith `&4 = &2 * &2`;GSYM Sphere.delta_y];
2148   TYPIFY `delta_y y1 y3 (&2 * h0) (&2) (&2) y5 = delta_y z1 y1 y3 y5 (&2) (&2)` (C SUBGOAL_THEN SUBST1_TAC);
2149     ASM_REWRITE_TAC[];
2150     BY(MESON_TAC[Merge_ineq.delta_y_sym]);
2151   ASM_REWRITE_TAC[];
2152   REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
2153   BY(ASM_TAC THEN REAL_ARITH_TAC)
2154   ]);;
2155   (* }}} *)
2156
2157 let terminal_pent_taum = prove_by_refinement(
2158   `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y126 y135.
2159       &20 <= delta_y y126 y1 y2 y6 (&2) (&2) /\
2160       &0 <= delta_y y135 y1 y3 y5 (&2) (&2) ==>
2161      (ineq [
2162        (&2,y1,&2 * h0);
2163        (&2,y2,&2 * h0);
2164        (&2,y3,&2 * h0);
2165        (&2,y4,&2);
2166        (#3.01,y5,#3.237);
2167        (#3.01,y6,#3.237);
2168        (&2,y126,&2 * h0);
2169        (&2,y135,&2 * h0)
2170      ]
2171      (#0.616 < taum y126 y1 y2 y6 (&2) (&2) + taum y1 y2 y3 y4 y5 y6 + taum y135 y1 y3 y5 (&2) (&2))))
2172      `,
2173   (* {{{ proof *)
2174   [
2175   REWRITE_TAC[Sphere.ineq];
2176   REPEAT WEAKER_STRIP_TAC;
2177   INTRO_TAC (UNDISCH taud_minimizer_terminal_pent_cases) [`&20`;`y126`;`y1`;`y2`;`y6`;`(&2)`;`&2`];
2178   REWRITE_TAC[LET_DEF;LET_END_DEF;IN_INTER;IN_REAL_INTERVAL;IN_ELIM_THM];
2179   ANTS_TAC;
2180     BY(ASM_TAC THEN REAL_ARITH_TAC);
2181   REPEAT WEAKER_STRIP_TAC;
2182   INTRO_TAC (UNDISCH2 OWZLKVY4) [`y126`;`y1`;`y2`;`y6`;`&2`;`&2`];
2183   ANTS_TAC;
2184     BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC);
2185   INTRO_TAC (UNDISCH2 OWZLKVY4) [`y135`;`y1`;`y3`;`y5`;`&2`;`&2`];
2186   ANTS_TAC;
2187     BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC);
2188   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;
2189     BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2190   COMMENT "case z1=2";
2191   FIRST_X_ASSUM DISJ_CASES_TAC;
2192     INTRO_TAC (UNDISCH2 terminal_pent_tau126_2) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`z1`;`y135`];
2193     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2194     ANTS_TAC;
2195       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2196     BY(REWRITE_TAC[]);
2197   COMMENT "case z1=2h0";
2198   FIRST_X_ASSUM DISJ_CASES_TAC;
2199     INTRO_TAC (UNDISCH2 terminal_pent_tau126_2h0) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`z1`;`y135`];
2200     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2201     ANTS_TAC;
2202       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2203     BY(REWRITE_TAC[]);
2204   COMMENT "case delta=20";
2205   FIRST_X_ASSUM DISJ_CASES_TAC;
2206     INTRO_TAC (UNDISCH2 terminal_pent_tau126_delta20) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`z1`;`y135`];
2207     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2208     ANTS_TAC;
2209       BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2210     BY(REWRITE_TAC[]);
2211   COMMENT "case tau012";
2212   INTRO_TAC (UNDISCH2 terminal_pent_taum126_012) [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`;`z1`;`y135`];
2213   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2214   ANTS_TAC;
2215     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2216   BY(REWRITE_TAC[])
2217   ]);;
2218   (* }}} *)
2219
2220 (* HEXAGON SECTION terminal_hex *)
2221
2222 let taud_minimizer_terminal_hex_cases = prove_by_refinement(
2223   `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4.
2224        (&0 <= delta_y y1 y2 y3 y4 (&2) (&2)  /\
2225         &2 <= y1 /\ y1 <= &2 * h0 /\  &2 <= y2 /\ y2 <= &2 * h0 /\ &2 <= y3 /\ y3 <= &2 * h0 /\
2226          #3.01 <= y4 /\ y4 <= #3.915 /\ taum y1 y2 y3 y4 (&2) (&2) < &0 ==>
2227           (?z1. &0 <= delta_y z1 y2 y3 y4 (&2) (&2) /\
2228            &2 <= z1 /\ z1 <= &2 * h0 /\ taud z1 y2 y3 y4 (&2) (&2)  <= taud y1 y2 y3 y4 (&2) (&2) /\
2229           ( z1 = &2  \/ &0 = delta_y z1 y2 y3 y4 (&2) (&2) ))))`,
2230   (* {{{ proof *)
2231   [
2232   REPEAT WEAKER_STRIP_TAC;
2233   INTRO_TAC taud_minimizer [`&2`;`&2 * h0`;`&0`;`y2`;`y3`;`y4`;`&2`;`&2`];
2234   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];
2235   ANTS_TAC;
2236     REWRITE_TAC[arith `&0 <= &0`;NOT_FORALL_THM];
2237     BY(ASM_MESON_TAC[]);
2238   REPEAT WEAKER_STRIP_TAC;
2239   TYPIFY `z1` EXISTS_TAC;
2240   ASM_REWRITE_TAC[];
2241   CONJ_TAC;
2242     REPEAT (FIRST_X_ASSUM_ST `z = c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE)));
2243     BY(ASM_MESON_TAC[]);
2244   INTRO_TAC taud_minimizer_cases [`&2`;`&2 * h0`;`&0`;`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
2245   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];
2246   ANTS_TAC;
2247     BY(ASM_MESON_TAC[arith `&0 <= &2 /\ &0 <= &0`;arith `&2 <= y ==> &0 <= y`]);
2248   ASM_CASES_TAC `z1 = &2` THEN FIRST_ASSUM (unlist REWRITE_TAC);
2249   ASM_CASES_TAC `&0 = delta_y z1 y2 y3 y4 (&2) (&2)` THEN FIRST_ASSUM (unlist ASM_REWRITE_TAC);
2250   ASM_CASES_TAC `z1 = &2 * h0` THEN ASM_REWRITE_TAC[];
2251     INTRO_TAC (UNDISCH OWZLKVY4 ) [`y1`;`y2`;`y3`;`y4`;`&2`;`&2`];
2252     ANTS_TAC;
2253       BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC);
2254     FIRST_X_ASSUM (C INTRO_TAC [`y1`]);
2255     ANTS_TAC;
2256       BY(ASM_REWRITE_TAC[]);
2257     ASM_REWRITE_TAC[];
2258     FIRST_X_ASSUM_ST `taum` MP_TAC;
2259     INTRO_TAC taud_2h0 [`y2`;`y3`;`y4`;`&2`;`&2`];
2260     ANTS_TAC;
2261       BY(ASM_MESON_TAC[]);
2262     BY(REAL_ARITH_TAC);
2263   COMMENT "derviative cases";
2264   ASM_CASES_TAC `~(delta_y z1 y2 y3 y4 (&2) (&2) < &15)`;
2265     REPEAT WEAKER_STRIP_TAC;
2266     INTRO_TAC (Terminal.get_main_nonlinear "6877738680") [`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
2267     REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2268     ASM_REWRITE_TAC[];
2269     GMATCH_SIMP_TAC Functional_equation.taud_x_taud;
2270     INTRO_TAC (UNDISCH OWZLKVY4) [`y1`;`y2`;`y3`;`y4`;`&2`;`&2`];
2271     ANTS_TAC;
2272       BY(ASM_REWRITE_TAC[Sphere.cstab]);
2273     FIRST_X_ASSUM (C INTRO_TAC [`y1`]);
2274     ANTS_TAC;
2275       BY(ASM_REWRITE_TAC[]);
2276     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2277   INTRO_TAC (Terminal.get_main_nonlinear "9692636487") [`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
2278   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2279   ANTS_TAC;
2280     ASM_REWRITE_TAC[];
2281     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2282   BY(REPEAT (FIRST_X_ASSUM_ST `delta_y` MP_TAC) THEN REAL_ARITH_TAC)
2283   ]);;
2284   (* }}} *)
2285
2286 (* next, de-symmetrize everything,
2287     then combine delta ranges.  *)
2288
2289 let REAL_WLOG_S3_SIMPLEX = prove_by_refinement(
2290   `!(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 /\
2291       P y1 y2 y3 y4 y5 y6 = P y2 y1 y3 y5 y4 y6) /\
2292     (!y1 y2 y3 y4 y5 y6. y4 <= y6 /\ y6 <= y5 ==> P y1 y2 y3 y4 y5 y6) ==>
2293     (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,
2294   (* {{{ proof *)
2295   [
2296   REPEAT WEAK_STRIP_TAC;
2297   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);
2298     BY(REAL_ARITH_TAC);
2299   BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_MESON_TAC[])
2300   ]);;
2301   (* }}} *)
2302
2303 let REAL_WLOG_AAB_SIMPLEX = prove_by_refinement(
2304   `!(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) /\
2305     (!y1 y2 y3 y4 y5 y6. y4 <= y6 ==> P y1 y2 y3 y4 y5 y6) ==>
2306     (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,
2307   (* {{{ proof *)
2308   [
2309   REPEAT WEAK_STRIP_TAC;
2310   TYPIFY `(y4 <= y6 \/ y6 <= y4)` (C SUBGOAL_THEN ASSUME_TAC);
2311     BY(REAL_ARITH_TAC);
2312   BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_MESON_TAC[])
2313   ]);;
2314   (* }}} *)
2315
2316 let REAL_WLOG_ABB_SIMPLEX = prove_by_refinement(
2317   `!(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) /\
2318     (!y1 y2 y3 y4 y5 y6. y6 <= y5 ==> P y1 y2 y3 y4 y5 y6) ==>
2319     (!y1 y2 y3 y4 y5 y6. P y1 y2 y3 y4 y5 y6)`,
2320   (* {{{ proof *)
2321   [
2322   REPEAT WEAK_STRIP_TAC;
2323   TYPIFY `(y5 <= y6 \/ y6 <= y5)` (C SUBGOAL_THEN ASSUME_TAC);
2324     BY(REAL_ARITH_TAC);
2325   BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_MESON_TAC[])
2326   ]);;
2327   (* }}} *)
2328
2329  let delta_y_hex_cases = prove_by_refinement(
2330   `!y1 y2 y3 y5 y6 a b.     (delta_y y1 y2 a (&2) (&2) y6 = delta_y a y1 y2 y6 (&2) (&2) /\
2331           (delta_y y1 b y3 (&2) y5 (&2) = delta_y b y1 y3 y5 (&2) (&2)))`,
2332   (* {{{ proof *)
2333   [
2334   BY(MESON_TAC[Merge_ineq.delta_y_sym])
2335   ]);;
2336   (* }}} *)
2337
2338 let delta_y_sym_cases2 = prove_by_refinement(
2339   `!y1 y2 y3 y4 y5 y6 a.     delta_y a y3 y1 y5 (&2) (&2) = delta_y a y1 y3 y5 (&2) (&2) /\
2340           delta_y a y3 y2 y4 (&2) (&2) = delta_y a y2 y3 y4 (&2) (&2) /\
2341           delta_y a y2 y1 y6 (&2) (&2) = delta_y a y1 y2 y6 (&2) (&2)`,
2342   (* {{{ proof *)
2343   [
2344   BY(MESON_TAC[Merge_ineq.delta_y_sym])
2345   ]);;
2346   (* }}} *)
2347
2348 let taum_sym_cases2 = prove_by_refinement(
2349   `!y1 y2 y3 y4 y5 y6. taum y2 y1 y3 y5 y4 y6 = taum y1 y2 y3 y4 y5 y6 /\
2350     taum y1 y3 y2 y4 y6 y5 = taum y1 y2 y3 y4 y5 y6 /\
2351     taum y3 y1 y2 y6 y4 y5 = taum y1 y2 y3 y4 y5 y6 /\
2352     taum y3 y2 y1 y6 y5 y4 = taum y1 y2 y3 y4 y5 y6`,
2353   (* {{{ proof *)
2354   [
2355   BY(MESON_TAC[Terminal.taum_sym])
2356   ]);;
2357   (* }}} *)
2358
2359 let edge2_flatD_sym = prove_by_refinement(
2360   `!d y1 y2 y3 a. edge2_flatD_x1 d y1 y2 y3 a a = edge2_flatD_x1 d y2 y1 y3 a a`,
2361   (* {{{ proof *)
2362   [
2363   BY(REWRITE_TAC[Nonlin_def.edge2_flatD_x1;Merge_ineq.delta_x_sym])
2364   ]);;
2365   (* }}} *)
2366
2367 let edge2_flatD_x1_sym_cases = prove_by_refinement(
2368   `!y1 y2 y3 y4 y5 y6.
2369     edge2_flatD_x1 (&0) (y3 * y3) (y2 * y2) (y4*y4) (&2 * &2) (&2* &2) =
2370     edge2_flatD_x1 (&0) (y2 * y2) (y3 * y3) (y4*y4) (&2 * &2) (&2* &2) /\
2371     edge2_flatD_x1 (&0) (y3 * y3) (y1 * y1) (y5*y5) (&2 * &2) (&2* &2) =
2372     edge2_flatD_x1 (&0) (y1 * y1) (y3 * y3) (y5*y5) (&2 * &2) (&2* &2) /\
2373     edge2_flatD_x1 (&0) (y2 * y2) (y1 * y1) (y6*y6) (&2 * &2) (&2* &2) =
2374     edge2_flatD_x1 (&0) (y1 * y1) (y2 * y2) (y6*y6) (&2 * &2) (&2* &2)
2375 `,
2376   (* {{{ proof *)
2377   [
2378 BY(REWRITE_TAC[edge2_flatD_sym])
2379   ]);;
2380   (* }}} *)
2381
2382 let eulerA_x_sym_cases = prove_by_refinement(
2383   `!y1 y2 y3 y4 y5 y6.
2384      eulerA_x (y2 * y2) (y1 * y1) (y3 * y3) (y5 * y5) (y4 * y4) (y6 * y6) =
2385    eulerA_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6)  /\
2386    eulerA_x (y3 * y3) (y1 * y1) (y2 * y2) (y6 * y6) (y4 * y4) (y5 * y5)  =
2387    eulerA_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6)  /\
2388    eulerA_x (y3 * y3) (y2 * y2) (y1 * y1) (y6 * y6) (y5 * y5) (y4 * y4)  =
2389    eulerA_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6)  /\
2390    eulerA_x (y1 * y1) (y3 * y3) (y2 * y2) (y4 * y4) (y6 * y6) (y5 * y5)  =
2391    eulerA_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (y6 * y6)   `,
2392   (* {{{ proof *)
2393   [
2394   REWRITE_TAC[Sphere.eulerA_x];
2395   BY(REAL_ARITH_TAC)
2396   ]);;
2397   (* }}} *)
2398
2399 let mu_y_sym = prove_by_refinement(
2400   `!y1 y2 y3. mu_y y1 y2 y3 = mu_y y1 y3 y2`,
2401   (* {{{ proof *)
2402   [
2403   REWRITE_TAC[Nonlin_def.mu_y];
2404   BY(REAL_ARITH_TAC)
2405   ]);;
2406   (* }}} *)
2407
2408 let mu_y_sym_cases = prove_by_refinement(
2409   `!y1 y2 y3. mu_y (&2) (sqrt(y2 * y2)) (sqrt(y1*y1)) =
2410  mu_y (&2) (sqrt(y1 * y1)) (sqrt(y2*y2)) /\
2411  mu_y (&2) (sqrt(y3 * y3)) (sqrt(y2*y2)) =
2412  mu_y (&2) (sqrt(y2 * y2)) (sqrt(y3*y3)) /\
2413  mu_y (&2) (sqrt(y3 * y3)) (sqrt(y1*y1)) =
2414  mu_y (&2) (sqrt(y1 * y1)) (sqrt(y3*y3))
2415 `,
2416   (* {{{ proof *)
2417   [
2418     BY(REWRITE_TAC[mu_y_sym])
2419   ]);;
2420   (* }}} *)
2421
2422 let nonfunctional_mud_126 = prove_by_refinement(
2423   `! 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 =
2424     mu_y a (sqrt(y1 * y1)) (sqrt(y2 * y2))  * sqrt(delta_y a y1 y2 y6 b c)`,
2425   (* {{{ proof *)
2426   [
2427   REWRITE_TAC[Nonlin_def.mud_126_x;];
2428   Functional_equation.F_REWRITE_TAC;
2429   REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_126_x;GSYM Sphere.delta_y];
2430   BY(MESON_TAC[Merge_ineq.delta_y_sym])
2431   ]);;
2432   (* }}} *)
2433
2434 let nonfunctional_mud_234 = prove_by_refinement(
2435   `! 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 =
2436     mu_y a (sqrt(y2 * y2)) (sqrt(y3 * y3))  * sqrt(delta_y a y2 y3 y4 b c)`,
2437   (* {{{ proof *)
2438   [
2439   REWRITE_TAC[Nonlin_def.mud_234_x;];
2440   Functional_equation.F_REWRITE_TAC;
2441   REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_234_x;GSYM Sphere.delta_y];
2442   ]);;
2443   (* }}} *)
2444
2445 let nonfunctional_mud_135 = prove_by_refinement(
2446   `! 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 =
2447     mu_y a (sqrt(y1 * y1)) (sqrt(y3 * y3))  * sqrt(delta_y a y1 y3 y5 b c)`,
2448   (* {{{ proof *)
2449   [
2450   REWRITE_TAC[Nonlin_def.mud_135_x;];
2451   Functional_equation.F_REWRITE_TAC;
2452   REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_135_x;GSYM Sphere.delta_y];
2453   REWRITE_TAC[mu_y_sym];
2454   BY(MESON_TAC[Merge_ineq.delta_y_sym])
2455   ]);;
2456   (* }}} *)
2457
2458 let nonfunctional_flat_term2_126 = prove_by_refinement(
2459   `! d a b x1 x2 x3 x4 x5 x6. (flat_term2_126_x d a b) x1 x2 x3 x4 x5 x6 =
2460    flat_term (sqrt (edge2_flatD_x1 d x1 x2 x6 a b))`,
2461   (* {{{ proof *)
2462   [
2463   REWRITE_TAC[Nonlin_def.flat_term2_126_x];
2464   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])
2465   ]);;
2466   (* }}} *)
2467
2468 let nonfunctional_flat_term2_234 = prove_by_refinement(
2469   `! d a b x1 x2 x3 x4 x5 x6. (flat_term2_234_x d a b) x1 x2 x3 x4 x5 x6 =
2470    flat_term (sqrt (edge2_flatD_x1 d x2 x3 x4 a b))`,
2471   (* {{{ proof *)
2472   [
2473   REWRITE_TAC[Nonlin_def.flat_term2_234_x];
2474   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])
2475   ]);;
2476   (* }}} *)
2477
2478 let nonfunctional_flat_term2_135 = prove_by_refinement(
2479   `! d a b x1 x2 x3 x4 x5 x6. (flat_term2_135_x d a b) x1 x2 x3 x4 x5 x6 =
2480    flat_term (sqrt (edge2_flatD_x1 d x1 x3 x5 a b))`,
2481   (* {{{ proof *)
2482   [
2483   REWRITE_TAC[Nonlin_def.flat_term2_135_x];
2484   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])
2485   ]);;
2486   (* }}} *)
2487
2488 let nonfunctional_mudLs_126 = prove_by_refinement(
2489   `! y1 y2 x3 x4 x5 y6. mudLs_126_x (&4) (&10) (&2) (&2) (&2) (y1*y1) (y2*y2) x3 x4 x5 (y6*y6) =
2490    mu_y (&2) (sqrt (y1 * y1)) (sqrt (y2 * y2)) *
2491      (&1 / &14 * (delta_y (&2) y1 y2 y6 (&2) (&2) - &16) + &4)`,
2492   (* {{{ proof *)
2493   [
2494   REWRITE_TAC[Nonlin_def.mudLs_126_x];
2495   Functional_equation.F_REWRITE_TAC;
2496   REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_126_x;GSYM Sphere.delta_y;delta_y_hex_cases];
2497   REWRITE_TAC[arith `&4 * &4 = &16`;arith `&4 + &10 = &14`];
2498   TYPIFY `sqrt(&2 * &2) = &2` (C SUBGOAL_THEN SUBST1_TAC);
2499     GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2500     BY(REAL_ARITH_TAC);
2501   BY(REWRITE_TAC[])
2502   ]);;
2503   (* }}} *)
2504
2505 let nonfunctional_mudLs_234 = prove_by_refinement(
2506   `! x1 y2 y3 y4 x5 x6. mudLs_234_x (&4) (&10) (&2) (&2) (&2) x1 (y2*y2) (y3*y3) (y4*y4) x5 x6 =
2507    mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) *
2508      (&1 / &14 * (delta_y (&2) y2 y3 y4 (&2) (&2) - &16) + &4)`,
2509   (* {{{ proof *)
2510   [
2511   REWRITE_TAC[Nonlin_def.mudLs_234_x];
2512   Functional_equation.F_REWRITE_TAC;
2513   REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_234_x;GSYM Sphere.delta_y;delta_y_hex_cases];
2514   REWRITE_TAC[arith `&4 * &4 = &16`;arith `&4 + &10 = &14`];
2515   TYPIFY `sqrt(&2 * &2) = &2` (C SUBGOAL_THEN SUBST1_TAC);
2516     GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2517     BY(REAL_ARITH_TAC);
2518   BY(REWRITE_TAC[])
2519   ]);;
2520   (* }}} *)
2521
2522 let nonfunctional_mudLs_135 = prove_by_refinement(
2523   `! y1 x2 y3 x4 y5 x6. mudLs_135_x (&4) (&10) (&2) (&2) (&2) (y1*y1) x2 (y3*y3) x4 (y5*y5) x6 =
2524    mu_y (&2) (sqrt (y1 * y1)) (sqrt (y3 * y3)) *
2525      (&1 / &14 * (delta_y (&2) y1 y3 y5 (&2) (&2) - &16) + &4)`,
2526   (* {{{ proof *)
2527   [
2528   REWRITE_TAC[Nonlin_def.mudLs_135_x];
2529   Functional_equation.F_REWRITE_TAC;
2530   REWRITE_TAC[GSYM Nonlin_def.mu_y;Sphere.delta_135_x;GSYM Sphere.delta_y;delta_y_hex_cases];
2531   REWRITE_TAC[arith `&4 * &4 = &16`;arith `&4 + &10 = &14`];
2532   TYPIFY `sqrt(&2 * &2) = &2` (C SUBGOAL_THEN SUBST1_TAC);
2533     GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2534     BY(REAL_ARITH_TAC);
2535   BY(REWRITE_TAC[])
2536   ]);;
2537   (* }}} *)
2538
2539 let ineq_sym_s3 = prove_by_refinement(
2540   `!y4 y5 y6 p r .
2541       ineq p (r \/ y6 < y4 \/ y5 < y6) ==>
2542    ((y4 <= y6 /\ y6 <= y5) ==> ineq p r)`,
2543   (* {{{ proof *)
2544   [
2545   REPEAT WEAKER_STRIP_TAC;
2546   FIRST_X_ASSUM_ST `ineq` MP_TAC;
2547   BY(ASM_SIMP_TAC [arith `x <= y ==> ~(y < x)`])
2548   ]);;
2549   (* }}} *)
2550
2551 let ineq_sym_s2_aab = prove_by_refinement(
2552   `!y4 y6 p r. ineq p (r \/ y6 < y4) ==>
2553     ((y4 <= y6) ==> ineq p r)`,
2554   (* {{{ proof *)
2555   [
2556   REPEAT WEAKER_STRIP_TAC;
2557   FIRST_X_ASSUM_ST `ineq` MP_TAC;
2558   BY(ASM_SIMP_TAC [arith `x <= y ==> ~(y < x)`])
2559   ]);;
2560   (* }}} *)
2561
2562 let ineq_sym_s2_abb = prove_by_refinement(
2563   `!y5 y6 p r. ineq p (r \/ y5 < y6) ==>
2564     ((y6 <= y5) ==> ineq p r)`,
2565   (* {{{ proof *)
2566   [
2567   REPEAT WEAKER_STRIP_TAC;
2568   FIRST_X_ASSUM_ST `ineq` MP_TAC;
2569   BY(ASM_SIMP_TAC [arith `x <= y ==> ~(y < x)`])
2570   ]);;
2571   (* }}} *)
2572
2573 let clean_ineq = PURE_REWRITE_RULE[Sphere.y_of_x;Sphere.delta_234_x;Sphere.delta_126_x;Sphere.delta_135_x;
2574   arith `#2.52 pow 2 = #2.52 * #2.52 /\ &4 = &2 * &2`;GSYM Sphere.delta_y;delta_y_hex_cases;
2575   nonfunctional_mud_126;nonfunctional_mud_234;nonfunctional_mud_135;
2576   nonfunctional_flat_term2_126;  nonfunctional_flat_term2_234;  nonfunctional_flat_term2_135;
2577   nonfunctional_mudLs_135 ;nonfunctional_mudLs_126 ;nonfunctional_mudLs_234];;
2578
2579 let mk_ineq_hex conv i234 i126 i135 =
2580   let nth = List.nth in
2581   let d234 = nth [`   y_of_x (flat_term2_234_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `;
2582                   `&0`;
2583           `y_of_x (mud_234_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;
2584           `y_of_x (mudLs_234_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;
2585           `&0 - sol0`] i234 in
2586   let d126 = nth [`   y_of_x (flat_term2_126_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `;
2587                   `&0`;
2588           `y_of_x (mud_126_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;
2589           `y_of_x (mudLs_126_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;
2590           `&0 - sol0`] i126 in
2591   let d135 = nth [`   y_of_x (flat_term2_135_x (&0) (&4) (&4)) y1 y2 y3 y4 y5 y6 `;
2592                   `&0`;
2593           `y_of_x (mud_135_x_v1 (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;
2594           `y_of_x (mudLs_135_x (&4) (&10) (&2) (&2) (&2)) y1 y2 y3 y4 y5 y6  -  sol0`;
2595           `&0 - sol0`] i135 in
2596   let c234 = nth [`y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
2597                     y_of_x (delta_234_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`;
2598                   `F`;
2599                       `y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`;
2600                       `y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/
2601                         y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`;
2602                       `y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
2603                         y_of_x (delta_234_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i234 in
2604   let c126 = nth [`y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
2605                     y_of_x (delta_126_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`;
2606                   `F`;
2607                       `y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`;
2608                       `y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/
2609                         y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`;
2610                       `y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
2611                         y_of_x (delta_126_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i126 in
2612   let c135 = nth [`y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
2613                     y_of_x (delta_135_x (#2.52 pow 2) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &0`;
2614                   `F`;
2615                       `y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &100`;
2616                       `y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &16 \/
2617                         y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &100`;
2618                       `y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 < &0 \/
2619                         y_of_x (delta_135_x (&4) (&4) (&4)) y1 y2 y3 y4 y5 y6 > &16`;] i135 in
2620   let s45 = if (i234= i126) then `y6 < y4` else `F` in
2621   let s56 = if (i126= i135) then `y5 < y6` else `F` in
2622  rhs(concl(conv (Ineq.mk_tplate Main_estimate_ineq.template_hex [d234;d126;d135;c234;c126;c135;s45;s56])));;
2623
2624 (*
2625 let tmgg a b c =
2626   let g = mk_ineq_hex (PURE_REWRITE_CONV[]) a b c in
2627   let g' =  (mk_imp (`main_nonlinear_terminal_v11`,concl (clean_ineq (ASSUME g)))) in
2628     g';;
2629 *)
2630
2631 let get_ineq (a,b,c) =
2632   clean_ineq  (Terminal.get_main_nonlinear (Printf.sprintf "7550003505 %d %d %d" a b c));;
2633
2634 let get_ineq_term(a,b,c) =
2635   let g = mk_ineq_hex (PURE_REWRITE_CONV[]) a b c in
2636     concl (clean_ineq (ASSUME g));;
2637
2638 let get_ineq'(a,b,c) =
2639   let g' = mk_imp(`main_nonlinear_terminal_v11`,get_ineq_term(a,b,c)) in
2640     repeat UNDISCH (prove_by_refinement(g',[
2641         DISCH_TAC;
2642   BY(REWRITE_TAC[get_ineq(a,b,c)])]));;
2643
2644 let r755_0 i =
2645   let (yys,tm) =  (strip_forall (concl(get_ineq' (i,i,i)))) in
2646   let tm0 = rhs(concl(PURE_REWRITE_CONV [ASSUME (`y6 < y4 <=> F`);ASSUME (`y5 < y6 <=> F`)] tm)) in
2647   let tm1 = list_mk_forall (yys, tm0) in
2648   let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in
2649 prove_by_refinement(tm2,
2650   (* {{{ proof *)
2651   [
2652   DISCH_TAC;
2653   MATCH_MP_TAC REAL_WLOG_S3_SIMPLEX;
2654   CONJ_TAC;
2655     REPEAT WEAKER_STRIP_TAC;
2656     INTRO_TAC delta_y_sym_cases2 yys;
2657     DISCH_THEN (unlist REWRITE_TAC);
2658     INTRO_TAC taum_sym_cases2 yys;
2659     DISCH_THEN (unlist REWRITE_TAC);
2660     INTRO_TAC edge2_flatD_x1_sym_cases yys;
2661     DISCH_THEN (unlist REWRITE_TAC);
2662     INTRO_TAC eulerA_x_sym_cases yys;
2663     DISCH_THEN (unlist REWRITE_TAC);
2664     INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`];
2665     DISCH_THEN (unlist REWRITE_TAC);
2666     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);
2667       BY(REAL_ARITH_TAC);
2668     BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[]);
2669   REPEAT GEN_TAC;
2670   MATCH_MP_TAC ineq_sym_s3;
2671   INTRO_TAC (get_ineq(i,i,i)) yys;
2672   BY(REWRITE_TAC[TAUT `(a \/ b) \/ c <=> a \/ b \/ c`])
2673   ]);;
2674   (* }}} *)
2675
2676 let r755_diag = map (fun i -> (i, r755_0 i)) [0;1;2;3;4];;
2677
2678
2679 let r755_aab i j=
2680   let (yys,tm) =  (strip_forall (concl(get_ineq' (i,i,j)))) in
2681   let tm0 = rhs(concl(PURE_REWRITE_CONV [ASSUME (`(y6 < y4) <=> F`)] tm)) in
2682   let tm1 = list_mk_forall (yys, tm0) in
2683   let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in
2684 prove_by_refinement(tm2,
2685   (* {{{ proof *)
2686   [
2687   DISCH_TAC;
2688   MATCH_MP_TAC REAL_WLOG_AAB_SIMPLEX;
2689   CONJ_TAC;
2690     REPEAT WEAKER_STRIP_TAC;
2691     INTRO_TAC delta_y_sym_cases2 yys;
2692     DISCH_THEN (unlist REWRITE_TAC);
2693     INTRO_TAC taum_sym_cases2 yys;
2694     DISCH_THEN (unlist REWRITE_TAC);
2695     INTRO_TAC edge2_flatD_x1_sym_cases yys;
2696     DISCH_THEN (unlist REWRITE_TAC);
2697     INTRO_TAC eulerA_x_sym_cases yys;
2698     DISCH_THEN (unlist REWRITE_TAC);
2699     INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`];
2700     DISCH_THEN (unlist REWRITE_TAC);
2701     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);
2702       BY(REAL_ARITH_TAC);
2703     BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[]);
2704   REPEAT GEN_TAC;
2705   MATCH_MP_TAC ineq_sym_s2_aab;
2706   INTRO_TAC (get_ineq(i,i,j)) yys;
2707   BY(REWRITE_TAC[TAUT `(a \/ b) \/ c <=> a \/ b \/ c`])
2708   ]);;
2709   (* }}} *)
2710
2711 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);
2712                                                       (2,3);(2,4);(3,4)];;
2713
2714 let r755_abb i j=
2715   let (yys,tm) =  (strip_forall (concl(get_ineq' (i,j,j)))) in
2716   let tm0 = rhs(concl(PURE_REWRITE_CONV [ASSUME (`(y5 < y6) <=> F`)] tm)) in
2717   let tm1 = list_mk_forall (yys, tm0) in
2718   let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in
2719 prove_by_refinement(tm2,
2720   (* {{{ proof *)
2721   [
2722   DISCH_TAC;
2723   MATCH_MP_TAC REAL_WLOG_ABB_SIMPLEX;
2724   CONJ_TAC;
2725     REPEAT WEAKER_STRIP_TAC;
2726     INTRO_TAC delta_y_sym_cases2 yys;
2727     DISCH_THEN (unlist REWRITE_TAC);
2728     INTRO_TAC taum_sym_cases2 yys;
2729     DISCH_THEN (unlist REWRITE_TAC);
2730     INTRO_TAC edge2_flatD_x1_sym_cases yys;
2731     DISCH_THEN (unlist REWRITE_TAC);
2732     INTRO_TAC eulerA_x_sym_cases yys;
2733     DISCH_THEN (unlist REWRITE_TAC);
2734     INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`];
2735     DISCH_THEN (unlist REWRITE_TAC);
2736     TYPIFY_GOAL_THEN `!f. f y1 y2 y6 + f y1 y3 y5 = f y1 y3 y5 + f y1 y2 y6` (unlist ONCE_REWRITE_TAC);
2737       BY(REAL_ARITH_TAC);
2738     BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[]);
2739   REPEAT GEN_TAC;
2740   MATCH_MP_TAC ineq_sym_s2_abb;
2741   INTRO_TAC (get_ineq(i,j,j)) yys;
2742   BY(REWRITE_TAC[TAUT `(a \/ b) \/ c <=> a \/ b \/ c`])
2743   ]);;
2744   (* }}} *)
2745
2746 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);
2747                                                       (2,3);(2,4);(3,4)];;
2748
2749 let get_ineq2( i, j, k) =
2750   let _ = (i <= j && j <= k) or failwith "get2 out of range" in
2751     if (i = j && j = k) then UNDISCH (assoc i r755_diag)
2752     else if (i = j) then UNDISCH (assoc (i,k) r755_aab_list)
2753     else if (j = k) then UNDISCH (assoc (i,j) r755_abb_list)
2754     else get_ineq'(i,j,k);;
2755
2756 (*
2757 let tmg i j =
2758   let (yys,tm) =  (strip_forall (concl(get_ineq (i,j,j)))) in
2759   let tm0 = rhs(concl(REWRITE_CONV [ASSUME (`~(y5 < y6) /\ ~(y6 < y4)`)] tm)) in
2760   let tm1 = list_mk_forall (yys, tm0) in
2761   let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in
2762     tm2;;
2763 *)
2764
2765 let g755_ i j k =
2766 (*  let inq = (Main_estimate_ineq.make_hex_ear i j k).ineq in
2767   let inq' = concl(clean_ineq (ASSUME inq)) in
2768 *)
2769   let inq' = get_ineq_term (i,j,k) in
2770   let (yys,tm) =  strip_forall inq' in
2771   let tm0 = rhs(concl(PURE_REWRITE_CONV [ASSUME `(y5 < y6) <=> F`;ASSUME `(y6 < y4) <=> F`] tm)) in
2772   let tm1 = list_mk_forall (yys, tm0) in
2773   let tm2 = mk_imp (`main_nonlinear_terminal_v11`,tm1) in
2774     tm2;;
2775
2776 let r755_ikj getter i j k  = prove_by_refinement(
2777   (g755_ i j k),
2778   (* {{{ proof *)
2779   [
2780   REPEAT WEAKER_STRIP_TAC;
2781   INTRO_TAC ( (getter (i, k, j))) [`y1`;`y3`;`y2`;`y4`;`y6`;`y5`];
2782     INTRO_TAC delta_y_sym_cases2 yys;
2783     DISCH_THEN (unlist REWRITE_TAC);
2784     INTRO_TAC taum_sym_cases2 yys;
2785     DISCH_THEN (unlist REWRITE_TAC);
2786     INTRO_TAC edge2_flatD_x1_sym_cases yys;
2787     DISCH_THEN (unlist REWRITE_TAC);
2788     INTRO_TAC eulerA_x_sym_cases yys;
2789     DISCH_THEN (unlist REWRITE_TAC);
2790     INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`];
2791     DISCH_THEN (unlist REWRITE_TAC);
2792   REWRITE_TAC[REAL_ADD_AC];
2793   BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[])
2794   ]);;
2795   (* }}} *)
2796
2797 let rec cross a = function
2798   | [] -> []
2799   | b::bs -> (map (fun i -> (i,b)) a) @ cross a bs;;
2800
2801 let triples = map (fun ((i,j),k)-> (i,j,k)) (cross (cross (0--4) (0--4)) (0--4));;
2802
2803 let r755_ikj_list =
2804   let ls = map (fun (i,j,k) -> ((i,j,k),
2805                   if (i > j or i > k) then TRUTH
2806                   else if (j<= k) then get_ineq2 (i,j,k)
2807                   else r755_ikj get_ineq2 i j k))  in
2808                   ls triples;;
2809
2810 let get_ineq3( i, j, k) =
2811   let _ = (i <= j && i <= k) or failwith (Printf.sprintf "get3 out of range %d %d %d" i j k) in
2812     repeat UNDISCH (assoc (i,j,k) r755_ikj_list);;
2813
2814 let r755_jik i j k  = prove_by_refinement(
2815   (g755_ i j k),
2816   (* {{{ proof *)
2817   [
2818   REPEAT WEAKER_STRIP_TAC;
2819   INTRO_TAC ( (get_ineq3 (j, i, k))) [`y3`;`y2`;`y1`;`y6`;`y5`;`y4`];
2820     INTRO_TAC delta_y_sym_cases2 yys;
2821     DISCH_THEN (unlist REWRITE_TAC);
2822     INTRO_TAC taum_sym_cases2 yys;
2823     DISCH_THEN (unlist REWRITE_TAC);
2824     INTRO_TAC edge2_flatD_x1_sym_cases yys;
2825     DISCH_THEN (unlist REWRITE_TAC);
2826     INTRO_TAC eulerA_x_sym_cases yys;
2827     DISCH_THEN (unlist REWRITE_TAC);
2828     INTRO_TAC mu_y_sym_cases [`y1`;`y2`;`y3`];
2829     DISCH_THEN (unlist REWRITE_TAC);
2830   REWRITE_TAC[REAL_ADD_AC];
2831   BY(REWRITE_TAC[Sphere.ineq] THEN MESON_TAC[])
2832   ]);;
2833   (* }}} *)
2834
2835 let r755_jik_list =
2836   let ls = map (fun (i,j,k) -> ((i,j,k),
2837                   if (k < i && k < j) then TRUTH
2838                   else if (i<= j) then get_ineq3 (i,j,k)
2839                   else r755_jik i j k))  in
2840                   ls triples;;
2841
2842 let get_ineq4( i, j, k) =
2843   let thm =     repeat UNDISCH (assoc (i,j,k) r755_jik_list) in
2844   let _ = (not(thm = TRUTH)) or failwith (Printf.sprintf "get4 out of range %d %d %d" i j k) in
2845     thm;;
2846
2847
2848 let get_ineq5 =
2849   let ls = map (fun (i,j,k) -> ((i,j,k),
2850                                 if (k < i && k < j) then r755_ikj get_ineq4 i j k
2851                                 else get_ineq4 (i,j,k))) in
2852   let r755_ikj_list2 = ls triples in
2853     fun ( i, j, k) ->
2854       repeat UNDISCH (assoc (i,j,k) r755_ikj_list2);;
2855
2856 (*
2857 let _ = (125 = List.length (filter (fun t -> not (snd t = TRUTH)) r755_ikj_list2));;
2858 *)
2859
2860 let taud_mu_clauses = prove_by_refinement(
2861   `main_nonlinear_terminal_v11 ==> (!y2 y3 y4.
2862     (&2 <= y2 /\ y2 <= #2.52 /\ &2 <= y3 /\ y3 <= #2.52 /\ #3.01 <= y4 /\ y4 <= #3.915) ==>
2863     (let d = delta_y (&2) y2 y3 y4 (&2) (&2) in
2864      let t = taud (&2) y2 y3 y4 (&2) (&2) in
2865        ((&0 <= d /\ d <= &16 ==> -- sol0 <= t) /\
2866           (&16 <= d /\ d <= &100 ==> mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) *
2867       (&1 / &14 * (delta_y (&2) y2 y3 y4 (&2) (&2) - &16) + &2 * &2) -
2868       sol0 <= t) /\
2869           (&100 <= d ==> mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) *
2870       sqrt (delta_y (&2) y2 y3 y4 (&2) (&2)) -
2871       sol0 <= t))))`,
2872   (* {{{ proof *)
2873   [
2874   REWRITE_TAC[LET_DEF;LET_END_DEF];
2875   REPEAT WEAKER_STRIP_TAC;
2876   CONJ_TAC;
2877     DISCH_TAC;
2878     INTRO_TAC (taud_ge_flat_term) [`&2`;`y2`;`y3`;`y4`;`&2`;`&2`];
2879     ANTS_TAC;
2880       BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab;Sphere.h0] THEN REAL_ARITH_TAC);
2881     BY(REWRITE_TAC[flat_term_2]);
2882   CONJ_TAC;
2883     REPEAT WEAKER_STRIP_TAC;
2884     REWRITE_TAC[Nonlin_def.taud;GSYM Nonlin_def.mu_y;GSYM Sphere.flat_term;flat_term_2];
2885     GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2886     GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2887     ASM_SIMP_TAC[arith `&2 <= y ==> &0 <= y`];
2888     TYPED_ABBREV_TAC `d = delta_y (&2) y2 y3 y4 (&2) (&2)`;
2889     MATCH_MP_TAC (arith `m* a <= m * a' ==> m * a - s <= --s + a' * m`);
2890     GMATCH_SIMP_TAC Real_ext.REAL_LE_LMUL_IMP;
2891     CONJ_TAC;
2892       REWRITE_TAC[Nonlin_def.mu_y];
2893       BY(ASM_TAC THEN REAL_ARITH_TAC);
2894     TYPIFY `&2 * &2 = sqrt(&16)` (C SUBGOAL_THEN SUBST1_TAC);
2895       MATCH_MP_TAC Upfzbzm_support_lemmas.SQRT_RULE_Euler_lemma;
2896       BY(REAL_ARITH_TAC);
2897     TYPIFY `&14 = sqrt(&16) + sqrt(&100)` (C SUBGOAL_THEN SUBST1_TAC);
2898       TYPIFY `&4 = sqrt(&16) /\ &10 = sqrt(&100)` ENOUGH_TO_SHOW_TAC;
2899         BY(REAL_ARITH_TAC);
2900       CONJ_TAC;
2901         MATCH_MP_TAC Upfzbzm_support_lemmas.SQRT_RULE_Euler_lemma;
2902         BY(REAL_ARITH_TAC);
2903       MATCH_MP_TAC Upfzbzm_support_lemmas.SQRT_RULE_Euler_lemma;
2904       BY(REAL_ARITH_TAC);
2905     MATCH_MP_TAC sqrt_secant_approx;
2906     BY(ASM_TAC THEN REAL_ARITH_TAC);
2907   COMMENT "final case";
2908   GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2909   GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2910   ASM_SIMP_TAC[arith `&2 <= y ==> &0 <= y`];
2911   DISCH_TAC;
2912   REWRITE_TAC[Nonlin_def.taud;GSYM Nonlin_def.mu_y;GSYM Sphere.flat_term;flat_term_2];
2913   BY(REAL_ARITH_TAC)
2914   ]);;
2915   (* }}} *)
2916
2917 let terminal_hex_234_reduction = prove_by_refinement(
2918   `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y234 f1 f2 b1 b2.
2919     (let dom = [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52;  #3.01,y4, #3.915;
2920           #3.01,
2921          y5,
2922           #3.915;  #3.01,y6, #3.915] in
2923        (ineq dom (f1 + flat_term
2924           (sqrt
2925           (edge2_flatD_x1 (&0) (y2 * y2) (y3 * y3) (y4 * y4) (&2 * &2)
2926           (&2 * &2))) + f2 > #0.712 \/ b1 \/ (delta_y (&2) y2 y3 y4 (&2) (&2) < &0 \/
2927            delta_y  #2.52 y2 y3 y4 (&2) (&2) > &0) \/ b2)) /\
2928 (ineq dom (f1 + &0 + f2 > #0.712 \/ b1 \/ F \/ b2)) /\
2929 (ineq dom (f1 + (
2930           mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) *
2931           sqrt (delta_y (&2) y2 y3 y4 (&2) (&2)) -
2932           sol0) + f2 > #0.712 \/ b1 \/ delta_y (&2) y2 y3 y4 (&2) (&2) < &100 \/ b2)) /\
2933 (ineq dom (f1 + (          mu_y (&2) (sqrt (y2 * y2)) (sqrt (y3 * y3)) *
2934           (&1 / &14 * (delta_y (&2) y2 y3 y4 (&2) (&2) - &16) + &2 * &2) -
2935           sol0) + f2 > #0.712 \/
2936    b1 \/ (delta_y (&2) y2 y3 y4 (&2) (&2) < &16 \/
2937            delta_y (&2) y2 y3 y4 (&2) (&2) > &100) \/ b2)) /\
2938 (ineq dom (f1 + ( &0 - sol0) + f2 > #0.712 \/
2939              b1 \/ (delta_y (&2) y2 y3 y4 (&2) (&2) < &0 \/
2940            delta_y (&2) y2 y3 y4 (&2) (&2) > &16) \/ b2))) ==>
2941     (ineq [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52;  #3.01,y4, #3.915;
2942           #3.01,
2943          y5,
2944           #3.915;  #3.01,y6, #3.915;&2,y234,#2.52] ((f1 + taum y234 y2 y3 y4 (&2) (&2)) +  f2 > #0.712 \/
2945            (delta_y y234 y2 y3 y4 (&2) (&2) < &0 \/ b1) \/ b2)))`,
2946   (* {{{ proof *)
2947   [
2948   REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF];
2949   REPEAT WEAKER_STRIP_TAC;
2950   REPEAT (FIRST_X_ASSUM_ST `\/` MP_TAC) THEN ASM_REWRITE_TAC[];
2951   ASM_CASES_TAC `b1:bool`;
2952     BY(ASM_REWRITE_TAC[]);
2953   ASM_REWRITE_TAC[];
2954   ASM_CASES_TAC `b2:bool`;
2955     BY(ASM_REWRITE_TAC[]);
2956   ASM_REWRITE_TAC[];
2957   REWRITE_TAC[arith `f1 + t + f2 > #0.712 <=> t > #0.712 - f1 - f2`;arith `(f1 + t) + f2 > #0.712 <=> t > #0.712 - f1 - f2`];
2958   TYPED_ABBREV_TAC `c = #0.712 - f1 - f2`;
2959   REPEAT WEAKER_STRIP_TAC;
2960   ASM_CASES_TAC `&0 <= taum y234 y2 y3 y4 (&2) (&2)`;
2961     BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2962   ASM_CASES_TAC `delta_y y234 y2 y3 y4 (&2) (&2) < &0`;
2963     BY(ASM_REWRITE_TAC[]);
2964   ASM_REWRITE_TAC[];
2965   INTRO_TAC (UNDISCH taud_minimizer_terminal_hex_cases) [`y234`;`y2`;`y3`;`y4`];
2966   ASM_SIMP_TAC[arith `~(d < &0) ==> &0 <= d`;arith `~(&0 <= t) ==> t < &0`];
2967   ANTS_TAC;
2968     BY(REWRITE_TAC[Sphere.h0] THEN ASM_TAC THEN REAL_ARITH_TAC);
2969   REPEAT WEAKER_STRIP_TAC;
2970   INTRO_TAC (UNDISCH OWZLKVY4) [`y234`;`y2`;`y3`;`y4`;`&2`;`&2`];
2971   ANTS_TAC;
2972     BY(ASM_TAC THEN REWRITE_TAC[Sphere.cstab;Sphere.h0] THEN REAL_ARITH_TAC);
2973   DISCH_TAC;
2974   FIRST_X_ASSUM DISJ_CASES_TAC;
2975     FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
2976     INTRO_TAC (UNDISCH taud_mu_clauses) [`y2`;`y3`;`y4`];
2977     ANTS_TAC;
2978       BY(ASM_REWRITE_TAC[]);
2979     REWRITE_TAC[LET_DEF;LET_END_DEF];
2980     BY(ASM_TAC THEN REAL_ARITH_TAC);
2981   REPEAT (FIRST_X_ASSUM_ST `mu_y` kill);
2982   INTRO_TAC taud_ge_flat_term [`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
2983   ANTS_TAC;
2984     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2985   DISCH_TAC;
2986   INTRO_TAC (UNDISCH edge2_flatD_x1_delta_lemma3) [`&0`;`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
2987   REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> (a /\ b ==> c)`];
2988   ANTS_TAC;
2989     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2990   DISCH_TAC;
2991   FIRST_X_ASSUM_ST `sqrt` MP_TAC;
2992   ASM_REWRITE_TAC[];
2993   GMATCH_SIMP_TAC Nonlinear_lemma.sqrtxx;
2994   ASM_SIMP_TAC [arith `&2 <= z1 ==> &0 <= z1`];
2995   INTRO_TAC (UNDISCH delta_mono) [`&2 * h0`;`z1`;`y2`;`y3`;`y4`;`&2`;`&2`];
2996   ANTS_TAC;
2997     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
2998   INTRO_TAC (UNDISCH delta_2_nn) [`z1`;`y2`;`y3`;`y4`];
2999   ANTS_TAC;
3000     BY(ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC);
3001   BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[Sphere.h0;arith `#2.52 = &2 * #1.26`] THEN REAL_ARITH_TAC)
3002   ]);;
3003   (* }}} *)
3004
3005 let mk_25 j k =
3006   let get_spec i j k = ISPECL yys (get_ineq5(i,j,k)) in
3007   let aa i = get_spec i j k in
3008   let rule = PURE_REWRITE_RULE[LET_DEF;LET_END_DEF;BETA_THM] in
3009     GENL yys (MATCH_MP (rule (UNDISCH terminal_hex_234_reduction)) (end_itlist CONJ (map aa (0--4))));;
3010
3011 (*
3012 let terminal_hex_25  = map (fun (j,k) -> mk_25 j k) (cross (0--4) (0--4));;
3013 *)
3014
3015 let terminal_hex_126_reduction = prove_by_refinement(
3016   `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y234 y126 f1 f2 b1 b2.
3017     (let dom = [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52;  #3.01,y4, #3.915;
3018           #3.01,
3019          y5,
3020           #3.915;  #3.01,y6, #3.915;&2,y234,#2.52 ] in
3021        (ineq dom (f1 + flat_term
3022           (sqrt
3023           (edge2_flatD_x1 (&0) (y1 * y1) (y2 * y2) (y6 * y6) (&2 * &2)
3024           (&2 * &2))) + f2 > #0.712 \/ b1 \/ (delta_y (&2) y1 y2 y6 (&2) (&2) < &0 \/
3025            delta_y  #2.52 y1 y2 y6 (&2) (&2) > &0) \/ b2)) /\
3026 (ineq dom (f1 + &0 + f2 > #0.712 \/ b1 \/ F \/ b2)) /\
3027 (ineq dom (f1 + (
3028           mu_y (&2) (sqrt (y1 * y1)) (sqrt (y2 * y2)) *
3029           sqrt (delta_y (&2) y1 y2 y6 (&2) (&2)) -
3030           sol0) + f2 > #0.712 \/ b1 \/ delta_y (&2) y1 y2 y6 (&2) (&2) < &100 \/ b2)) /\
3031 (ineq dom (f1 + (          mu_y (&2) (sqrt (y1 * y1)) (sqrt (y2 * y2)) *
3032           (&1 / &14 * (delta_y (&2) y1 y2 y6 (&2) (&2) - &16) + &2 * &2) -
3033           sol0) + f2 > #0.712 \/
3034    b1 \/ (delta_y (&2) y1 y2 y6 (&2) (&2) < &16 \/
3035            delta_y (&2) y1 y2 y6 (&2) (&2) > &100) \/ b2)) /\
3036 (ineq dom (f1 + ( &0 - sol0) + f2 > #0.712 \/
3037              b1 \/ (delta_y (&2) y1 y2 y6 (&2) (&2) < &0 \/
3038            delta_y (&2) y1 y2 y6 (&2) (&2) > &16) \/ b2))) ==>
3039     (ineq [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52;  #3.01,y4, #3.915;
3040           #3.01,
3041          y5,
3042           #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 \/
3043            (delta_y y126 y1 y2 y6 (&2) (&2) < &0 \/ b1) \/ b2)))`,
3044   (* {{{ proof *)
3045   [
3046   REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF];
3047   REPEAT WEAKER_STRIP_TAC;
3048   REPEAT (FIRST_X_ASSUM_ST `\/` MP_TAC) THEN ASM_REWRITE_TAC[];
3049   ASM_CASES_TAC `b1:bool`;
3050     BY(ASM_REWRITE_TAC[]);
3051   ASM_REWRITE_TAC[];
3052   ASM_CASES_TAC `b2:bool`;
3053     BY(ASM_REWRITE_TAC[]);
3054   ASM_REWRITE_TAC[];
3055   REPEAT WEAKER_STRIP_TAC;
3056   INTRO_TAC (UNDISCH terminal_hex_234_reduction) [`y3`;`y1`;`y2`;`y6`;`y4`;`y5`;`y126`;`f1`;`f2`;`b1`;`b2`];
3057   BY(ASM_REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF])
3058   ]);;
3059   (* }}} *)
3060
3061 let mk_5 k =
3062   let yys' = yys @ [`y234:real`] in
3063   let get_spec j k = ISPECL (yys') (mk_25 j k) in
3064   let aa j = get_spec j k in
3065   let rule = PURE_REWRITE_RULE[LET_DEF;LET_END_DEF;BETA_THM] in
3066     GENL yys' (MATCH_MP (rule (UNDISCH terminal_hex_126_reduction)) (end_itlist CONJ (map aa (0--4))));;
3067
3068 let terminal_hex_135_reduction = prove_by_refinement(
3069   `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6 y234 y126 y135 f1 b1 b2.
3070     (let dom = [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52;  #3.01,y4, #3.915;
3071           #3.01,
3072          y5,
3073           #3.915;  #3.01,y6, #3.915;&2,y234,#2.52; &2,y126,#2.52 ] in
3074        (ineq dom (f1 + flat_term
3075           (sqrt
3076           (edge2_flatD_x1 (&0) (y1 * y1) (y3 * y3) (y5 * y5) (&2 * &2)
3077           (&2 * &2))) > #0.712 \/ b1 \/ (delta_y (&2) y1 y3 y5 (&2) (&2) < &0 \/
3078            delta_y  #2.52 y1 y3 y5 (&2) (&2) > &0) \/ b2)) /\
3079 (ineq dom (f1 + &0  > #0.712 \/ b1 \/ F \/ b2)) /\
3080 (ineq dom (f1 + (
3081           mu_y (&2) (sqrt (y1 * y1)) (sqrt (y3 * y3)) *
3082           sqrt (delta_y (&2) y1 y3 y5 (&2) (&2)) -
3083           sol0)  > #0.712 \/ b1 \/ delta_y (&2) y1 y3 y5 (&2) (&2) < &100 \/ b2)) /\
3084 (ineq dom (f1 + (          mu_y (&2) (sqrt (y1 * y1)) (sqrt (y3 * y3)) *
3085           (&1 / &14 * (delta_y (&2) y1 y3 y5 (&2) (&2) - &16) + &2 * &2) -
3086           sol0)  > #0.712 \/
3087    b1 \/ (delta_y (&2) y1 y3 y5 (&2) (&2) < &16 \/
3088            delta_y (&2) y1 y3 y5 (&2) (&2) > &100) \/ b2)) /\
3089 (ineq dom (f1 + ( &0 - sol0)  > #0.712 \/
3090              b1 \/ (delta_y (&2) y1 y3 y5 (&2) (&2) < &0 \/
3091            delta_y (&2) y1 y3 y5 (&2) (&2) > &16) \/ b2))) ==>
3092     (ineq [&2,y1, #2.52; &2,y2, #2.52; &2,y3, #2.52;  #3.01,y4, #3.915;
3093           #3.01,
3094          y5,
3095           #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 \/
3096            (delta_y y135 y1 y3 y5 (&2) (&2) < &0 \/ b1) \/ b2)))`,
3097   (* {{{ proof *)
3098   [
3099   REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF];
3100   REPEAT WEAKER_STRIP_TAC;
3101   REPEAT (FIRST_X_ASSUM_ST `==>` MP_TAC) THEN ASM_REWRITE_TAC[];
3102   ASM_CASES_TAC `b1:bool`;
3103     BY(ASM_REWRITE_TAC[]);
3104   ASM_REWRITE_TAC[];
3105   ASM_CASES_TAC `b2:bool`;
3106     BY(ASM_REWRITE_TAC[]);
3107   ASM_REWRITE_TAC[];
3108   REPEAT WEAKER_STRIP_TAC;
3109   INTRO_TAC (UNDISCH terminal_hex_234_reduction) [`y2`;`y1`;`y3`;`y5`;`y4`;`y6`;`y135`;`f1`;`&0`;`b1`;`b2`];
3110   ASM_REWRITE_TAC[Sphere.ineq;LET_DEF;LET_END_DEF];
3111   RULE_ASSUM_TAC (REWRITE_RULE[arith `a + &0 = a`]);
3112   BY(ASM_REWRITE_TAC[arith `a + &0 = a`])
3113   ]);;
3114   (* }}} *)
3115
3116 let terminal_hex_taum  =
3117   let yys' = (yys @ [`y234:real`;`y126:real`]) in
3118   let aa k = ISPECL yys' (mk_5 k) in
3119   let rule1 = PURE_REWRITE_RULE[LET_DEF;LET_END_DEF;BETA_THM] in
3120   let rule2 = REWRITE_RULE[REAL_ADD_AC] in
3121     GENL yys' (rule2(MATCH_MP (rule1 (UNDISCH terminal_hex_135_reduction)) (end_itlist CONJ (map aa (0--4)))));;
3122
3123 end;;