(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(* Section: Appendix, Main Estimate, check_completeness                       *)
(* Chapter: Local Fan                                                         *)
(* Lemma: BKOSSGE                                                             *)
(* Author: Thomas Hales                                                       *)
(* Date: 2013-08-07                                                           *)
(* ========================================================================== *)

module Bkossge = struct 

  open Hales_tactic;;

let cos_bounds_0_pi = prove_by_refinement(
  `!z. &0 < z /\ z < pi ==> -- &1 < cos z /\ cos z < &1`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `(&0 < z /\ z < pi / &2) \/ z = pi / &2 \/ (&0 < pi - z /\ pi - z < pi / &2)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC);
      BY(ASM_MESON_TAC[Counting_spheres.cos_bounds_0_Pi2;arith `&0 < x ==> -- &1 < x`]);
    ASM_REWRITE_TAC[COS_PI2];
    BY(REAL_ARITH_TAC);
  TYPIFY `-- &1 < --cos z /\ --cos z < &1` ENOUGH_TO_SHOW_TAC;
    BY(REAL_ARITH_TAC);
  ONCE_REWRITE_TAC[GSYM COS_NEG];
  REWRITE_TAC[GSYM COS_PERIODIC_PI;arith `--z + pi = pi - z`];
  BY(ASM_MESON_TAC[Counting_spheres.cos_bounds_0_Pi2;arith `&0 < x ==> -- &1 < x`])
  ]);;
  (* }}} *)

let ear_acute = prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> (!y1 y2 y3 y4 y5 y6. 
    &2 <= y1 /\ y1 <= &2 * h0 /\
    &2 <= y2 /\ y2 <= &2 * h0 /\
    &2 <= y3 /\ y3 <= &2 * h0 /\
    &2 <= y4 /\ y4 <= &2 * h0 /\
    &2 <= y6 /\ y6 <= &2 * h0 /\
    &3 <= y5 /\
    &0 < ups_x (y1*y1) (y3*y3) (y5*y5) 
    ==> dih_y y1 y2 y3 y4 y5 y6 < pi / &2)
`,
  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.h0;arith `&2 * #1.26  = #2.52`;Trigonometry.IHIQXLM];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (Terminal.get_main_nonlinear "2485876245a") [`y1`;`y2`;`y3`;`y4`;`y5`;`y6`];
  ASM_REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;arith `#3.0 = &3`;];
  ANTS_TAC;
    REWRITE_TAC[arith `x <= y <=> ~(y < x)`];
    DISCH_TAC;
    FIRST_X_ASSUM_ST `&16` MP_TAC THEN REWRITE_TAC[arith `a * b * c = (a * b) * c`];
    REWRITE_TAC[arith `~(&0 < x * y) <=> &0 <= x * (-- y)`];
    REPEAT (GMATCH_SIMP_TAC REAL_LE_MUL_EQ);
    REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REWRITE_TAC[Nonlinear_lemma.dih_x_alt;Sphere.dih_y;LET_THM;GSYM Sphere.delta_y];
  REWRITE_TAC[GSYM Sphere.delta4_y;GSYM Sphere.y_of_x];
  REWRITE_TAC[arith `pi2 + a < pi2 <=> a < &0`];
  DISCH_TAC;
  GMATCH_SIMP_TAC Tskajxy.ATN2_Y_NEG;
  CONJ_TAC;
    BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
  BY(REWRITE_TAC[arith `p - a = p + -- a`;GSYM ATN_NEG;arith `-- p + a < &0 <=> a < p`;ATN_BOUNDS])
  ]);;
  (* }}} *)

let quad_nonexist_849 = prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> ~(?(v1:real^3) v2 v3 v4.
      dist(v1,v2) = &2 /\ dist(v2,v3) = &2 /\ dist(v3,v4) = &2 /\ dist(v1,v4)= &2 * h0 /\
      cstab <= dist(v1,v3) /\ cstab <= dist(v2,v4))`,
  (* {{{ proof *)
  [
  REWRITE_TAC[NOT_EXISTS_THM;Sphere.cstab];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (Terminal.get_main_nonlinear "8495326405") [`dist(v3,v4)`;`dist(v2,v3)`;`dist(v1,v3)`;`dist(v1,v2)`;`dist(v1,v4)`;`dist(v2,v4)`];
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;arith `x <= x`];
  DISCH_THEN MP_TAC THEN ANTS_TAC;
    ASM_REWRITE_TAC[arith `x <= x`];
    TYPIFY `!w1 w3 w2. dist(w1,w2) = &2 /\ dist(w2,w3) = &2 ==> dist((w1:real^3),w3) <= &6` ENOUGH_TO_SHOW_TAC;
      BY(DISCH_TAC THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[DIST_SYM]);
    REPEAT GEN_TAC THEN (INTRO_TAC DIST_TRIANGLE[`w1`;`w2`;`w3`]);
    BY(REAL_ARITH_TAC);
  REWRITE_TAC[arith `~(x < &0) <=> &0 <= x`];
  BY(INTRO_TAC Terminal.DELTA_Y_POS_4POINTS [`v3`;`v4`;`v2`;`v1`] THEN REWRITE_TAC[DIST_SYM])
  ]);;
  (* }}} *)

(* shortest diag < 3.62 *)

let quad_diag_362 = prove_by_refinement(
  `main_nonlinear_terminal_v11 ==> (!(v1:real^3) v2 v3 v4.
      dist(v1,v2) = &2 /\ dist(v2,v3) = cstab /\ dist(v3,v4) = &2 /\ dist(v1,v4)= cstab ==>
      (dist(v1,v3) <= #3.62 \/ dist(v2,v4) <= #3.62))`,
  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.cstab;arith `x <= y <=> ~(y < x)`;GSYM DE_MORGAN_THM];
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC (Terminal.get_main_nonlinear "2171548893") [`dist(v3,v4)`;`dist(v2,v3)`;`dist(v1,v3)`;`dist(v1,v2)`;`dist(v1,v4)`;`dist(v2,v4)`];
  REWRITE_TAC[Sphere.ineq;TAUT `a ==> b ==> c <=> a /\ b ==> c`;arith `x <= x`];
  DISCH_THEN MP_TAC THEN ANTS_TAC;
    ASM_REWRITE_TAC[arith `x <= x`];
    ASM_SIMP_TAC[arith `x < y ==> x <= y`];
    TYPIFY `!w1 w3 w2. dist(w1,w2) = &2 /\ dist(w2,w3) = #3.01 ==> dist((w1:real^3),w3) <= &6` ENOUGH_TO_SHOW_TAC;
      BY(DISCH_TAC THEN CONJ_TAC THENL [ALL_TAC;ONCE_REWRITE_TAC[DIST_SYM]] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[DIST_SYM]);
    REPEAT GEN_TAC THEN (INTRO_TAC DIST_TRIANGLE[`w1`;`w2`;`w3`]);
    BY(REAL_ARITH_TAC);
  REWRITE_TAC[arith `~(x < &0) <=> &0 <= x`];
  BY(INTRO_TAC Terminal.DELTA_Y_POS_4POINTS [`v3`;`v4`;`v2`;`v1`] THEN REWRITE_TAC[DIST_SYM])
  ]);;
  (* }}} *)

let INV_ARCLENGTH = prove_by_refinement(
  `!y1 y3 z. 
   &0 < z /\ z < pi /\ &0 < y1 /\ &0 < y3 ==>
    &0 < y1 pow 2 + y3 pow 2 - &2 * y1  *y3 * cos z /\
    z = arclength y1 y3 (sqrt (y1 pow 2 + y3 pow 2 - &2 * y1 *y3 * cos z))`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC cos_bounds_0_pi [`z`];
  ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
  SUBCONJ_TAC;
    REWRITE_TAC[arith `y1 pow 2 + y3 pow 2 - &2 * y1 * y3 * cos z = (y1 - y3) pow 2 + &2 * y1 *y3 * (&1 - cos z)`];
    MATCH_MP_TAC (arith `&0 <= a /\ &0 < b ==> &0 < a + b`);
    REWRITE_TAC[ REAL_LE_POW_2];
    REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  DISCH_TAC;
  TYPED_ABBREV_TAC `c = sqrt (y1 pow 2 + y3 pow 2 - &2 * y1 * y3 * cos z)`;
  GMATCH_SIMP_TAC Trigonometry1.ACS_ARCLENGTH;
  TYPIFY `c*c = y1 pow 2 + y3 pow 2 - &2 * y1 * y3 * cos z` (C SUBGOAL_THEN ASSUME_TAC);
    EXPAND_TAC "c";
    GMATCH_SIMP_TAC Merge_ineq.sqrtpow2;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  TYPED_ABBREV_TAC `r = (y1 * y1 + y3 * y3 - c * c) / (&2 * y1 * y3)`;
  CONJ2_TAC;
    TYPIFY `r = cos z` ENOUGH_TO_SHOW_TAC;
      DISCH_THEN SUBST1_TAC;
      GMATCH_SIMP_TAC ACS_COS;
      BY(ASM_TAC THEN REAL_ARITH_TAC);
    EXPAND_TAC "r";
    FIRST_X_ASSUM_ST `c * c = s` (SUBST1_TAC);
    Calc_derivative.CALC_ID_TAC;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  ASM_REWRITE_TAC[];
  SUBCONJ_TAC;
    EXPAND_TAC "c";
    GMATCH_SIMP_TAC SQRT_POS_LE;
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  DISCH_TAC;
  TYPIFY `c pow 2 <= (y1 + y3) pow 2 /\ (abs(y1 - y3)) pow 2 <= c pow 2` ENOUGH_TO_SHOW_TAC;
    GMATCH_SIMP_TAC (GSYM Trigonometry2.POW2_COND);
    GMATCH_SIMP_TAC (GSYM Trigonometry2.POW2_COND);
    BY(ASM_TAC THEN REAL_ARITH_TAC);
  REWRITE_TAC[REAL_POW2_ABS];
  ASM_REWRITE_TAC[arith `c pow 2  = c * c`];
  TYPIFY `-- &2 * y1 * y3 * cos z <= &2 * y1 * y3 /\ -- &2 * y1 * y3 <= -- &2 * y1 * y3 * cos z` ENOUGH_TO_SHOW_TAC;
    BY(REAL_ARITH_TAC);
  REWRITE_TAC[arith ` -- &2 * y1 * y3 * cos z <= &2 * y1 *y3 <=> &0 <= &2 * y1 * y3 * (&1 + cos z)`;arith `-- &2 * y1 * y3 <= -- &2 * y1 * y3 * cos z <=> &0 <= &2 * y1 * y3 * (&1 - cos z)`];
  GMATCH_SIMP_TAC REAL_LE_MUL;
  REPEAT (GMATCH_SIMP_TAC REAL_LE_MUL);
  BY(ASM_TAC THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let taum_dih_y = prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6.
    taum y1 y2 y3 y4 y5 y6 = 
    rho y1 * dih_y y1 y2 y3 y4 y5 y6 +
      rho y2 * dih_y y2 y3 y1 y5 y6 y4 +
      rho y3 * dih_y y3 y1 y2 y6 y4 y5 - (pi + sol0)`,
  (* {{{ proof *)
  [
  REWRITE_TAC[Sphere.taum;Sphere.sol_y;Sphere.lnazim;Sphere.rho;Nonlinear_lemma.sol0_const1];
  BY(REAL_ARITH_TAC)
  ]);;
  (* }}} *)

let real_continuous_dih_y_wrt4 = prove_by_refinement(
 `!y1 y2 y3 y4 y5 y6.
     &0 < delta_y y1 y2 y3 y4 y5 y6 /\
     &0 < y1 /\
     &0 < ups_x (y1 * y1) (y2 * y2) (y6 * y6) /\
     &0 < ups_x (y1 * y1) (y3 * y3) (y5 * y5)
     ==> (\q. dih_y y1 y2 y3 q y5 y6) real_continuous atreal y4`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Ocbicby.derived_form_dih_x_wrt_x4 [`y1*y1`;`y2*y2`;`y3*y3`;`y4*y4`;`y5*y5`;`y6*y6`];
  REWRITE_TAC[Calc_derivative.derived_form;Sphere.dih_y;LET_THM];
  REWRITE_TAC[WITHINREAL_UNIV];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
    BY(ASM_REWRITE_TAC[GSYM Sphere.delta_y]);
  DISCH_TAC;
  TYPIFY `(\q. dih_x (y1 * y1) (y2 * y2) (y3 * y3) (q * q) (y5 * y5) (y6 * y6)) = (\q. dih_x (y1 * y1) (y2 * y2) (y3 * y3) (q) (y5 * y5) (y6 * y6)) o (\t. t pow 2)` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REWRITE_TAC[FUN_EQ_THM;o_THM;arith `x*x = x pow 2`]);
  MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_COMPOSE;
  CONJ_TAC;
    MATCH_MP_TAC REAL_CONTINUOUS_POW;
    BY(REWRITE_TAC[REAL_CONTINUOUS_AT_ID]);
  REWRITE_TAC[arith `y4 pow 2 = y4 * y4`];
  MATCH_MP_TAC HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL;
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let real_continuous_dih_y_wrt5 = prove_by_refinement(
 `!y1 y2 y3 y4 y5 y6.
     &0 < delta_y y1 y2 y3 y4 y5 y6 /\
     &0 < y1 /\
     &0 < ups_x (y1 * y1) (y2 * y2) (y6 * y6) /\
     &0 < ups_x (y1 * y1) (y3 * y3) (y5 * y5)
     ==> (\q. dih_y y1 y2 y3 y4 q y6) real_continuous atreal y5`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Ocbicby.derived_form_dih_x_wrt_x5 [`y1*y1`;`y2*y2`;`y3*y3`;`y4*y4`;`y5*y5`;`y6*y6`];
  REWRITE_TAC[Calc_derivative.derived_form;Sphere.dih_y;LET_THM];
  REWRITE_TAC[WITHINREAL_UNIV];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
    BY(ASM_REWRITE_TAC[GSYM Sphere.delta_y]);
  DISCH_TAC;
  TYPIFY `(\q. dih_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (q * q) (y6 * y6)) = (\q. dih_x (y1 * y1) (y2 * y2) (y3 * y3) (y4*y4) (q) (y6 * y6)) o (\t. t pow 2)` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REWRITE_TAC[FUN_EQ_THM;o_THM;arith `x*x = x pow 2`]);
  MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_COMPOSE;
  CONJ_TAC;
    MATCH_MP_TAC REAL_CONTINUOUS_POW;
    BY(REWRITE_TAC[REAL_CONTINUOUS_AT_ID]);
  REWRITE_TAC[arith `y5 pow 2 = y5 * y5`];
  MATCH_MP_TAC HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL;
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let real_continuous_dih_y_wrt6 = prove_by_refinement(
 `!y1 y2 y3 y4 y5 y6.
     &0 < delta_y y1 y2 y3 y4 y5 y6 /\
     &0 < y1 /\
     &0 < ups_x (y1 * y1) (y2 * y2) (y6 * y6) /\
     &0 < ups_x (y1 * y1) (y3 * y3) (y5 * y5)
     ==> (\q. dih_y y1 y2 y3 y4 y5 q) real_continuous atreal y6`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC Ocbicby.derived_form_dih_x_wrt_x6 [`y1*y1`;`y2*y2`;`y3*y3`;`y4*y4`;`y5*y5`;`y6*y6`];
  REWRITE_TAC[Calc_derivative.derived_form;Sphere.dih_y;LET_THM];
  REWRITE_TAC[WITHINREAL_UNIV];
  ANTS_TAC;
    ASM_REWRITE_TAC[];
    GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
    BY(ASM_REWRITE_TAC[GSYM Sphere.delta_y]);
  DISCH_TAC;
  TYPIFY `(\q. dih_x (y1 * y1) (y2 * y2) (y3 * y3) (y4 * y4) (y5 * y5) (q*q)) = (\q. dih_x (y1 * y1) (y2 * y2) (y3 * y3) (y4*y4) (y5 * y5) (q)) o (\t. t pow 2)` (C SUBGOAL_THEN SUBST1_TAC);
    BY(REWRITE_TAC[FUN_EQ_THM;o_THM;arith `x*x = x pow 2`]);
  MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_COMPOSE;
  CONJ_TAC;
    MATCH_MP_TAC REAL_CONTINUOUS_POW;
    BY(REWRITE_TAC[REAL_CONTINUOUS_AT_ID]);
  REWRITE_TAC[arith `y6 pow 2 = y6 * y6`];
  MATCH_MP_TAC HAS_REAL_DERIVATIVE_IMP_CONTINUOUS_ATREAL;
  BY(ASM_MESON_TAC[])
  ]);;
  (* }}} *)

let real_continuous_taum = prove_by_refinement(
  `!y1 y2 y3 y4 y5 y6. 
         &0 < delta_y y1 y2 y3 y4 y5 y6 /\
         &0 < y1 /\ &0 < y2 /\ &0 < y3 /\
         &0 < ups_x (y1 * y1) (y2 * y2) (y6 * y6) /\
         &0 < ups_x (y2 * y2) (y3 * y3) (y4 * y4) /\
         &0 < ups_x (y1 * y1) (y3 * y3) (y5 * y5) ==>
     (\q. taum y1 y2 y3 q y5 y6) real_continuous atreal y4`,
  (* {{{ proof *)
  [
  REWRITE_TAC[taum_dih_y];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `delta_y y3 y1 y2 y6 y4 y5 = delta_y y1 y2 y3 y4 y5 y6 /\ delta_y y2 y3 y1 y5 y6 y4 = delta_y y1 y2 y3 y4 y5 y6` (C SUBGOAL_THEN ASSUME_TAC);
    BY(MESON_TAC[Merge_ineq.delta_y_sym]);
  TYPIFY `ups_x (y3 * y3) (y1 * y1) (y5 * y5) = ups_x (y1 * y1) (y3 * y3) (y5 * y5) /\ ups_x (y3 * y3) (y2 * y2) (y4 * y4) = ups_x (y2 * y2) (y3 * y3) (y4 * y4) /\ ups_x (y2 * y2) (y1 * y1) (y6 * y6) = ups_x (y1 * y1) (y2 * y2) (y6 * y6)` (C SUBGOAL_THEN ASSUME_TAC);
    BY(REWRITE_TAC[Merge_ineq.ups_x_sym]);
  BY((REPEAT (REPEAT CONJ_TAC THEN (MATCH_MP_TAC REAL_CONTINUOUS_ADD ORELSE MATCH_MP_TAC REAL_CONTINUOUS_MUL ORELSE MATCH_MP_TAC REAL_CONTINUOUS_POW ORELSE MATCH_MP_TAC REAL_CONTINUOUS_SUB ORELSE MATCH_MP_TAC real_continuous_dih_y_wrt6 ORELSE MATCH_MP_TAC real_continuous_dih_y_wrt5 ORELSE MATCH_MP_TAC real_continuous_dih_y_wrt4 THEN ASM_REWRITE_TAC[REAL_CONTINUOUS_CONST]))))
  ]);;
  (* }}} *)

let UPS_X_STD_POS = prove_by_refinement(
  `!y1 y2 y3. 	&2 <= y1 /\ y1 <= &2 * h0 /\
	&2 <= y2 /\ y2 <= &2 * h0 /\
	&2 <= y3 /\ y3 <= &2 * h0 ==> &0 < ups_x (y1 * y1) (y2 * y2) (y3 * y3)`,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  BY(MATCH_MP_TAC Ysskqoy.TRI_UPS_X_STRICT_POS THEN ASM_TAC THEN REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC)
  ]);;
  (* }}} *)



let BKOSSGE = prove_by_refinement(
  `scs_arrow_v39 {scs_3M1} {scs_3T1, scs_3T5}`,
  (* {{{ proof *)
  [
  REWRITE_TAC[Appendix.scs_arrow_v39;IN_SING;IN_INSERT;NOT_IN_EMPTY];
  CONJ_TAC;
    BY(MESON_TAC[Ocbicby.is_scs_examples]);
  REWRITE_TAC[TAUT `(a \/ b) <=> (~a ==> b)`;NOT_FORALL_THM];
  REWRITE_TAC[TAUT `~(a ==> b) <=> (a /\ ~b)`];
  REWRITE_TAC[IN;NOT_FORALL_THM];
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `?v. MMs_v39 s v /\ dist(v 0,v 1) <= sqrt8` ASM_CASES_TAC;
    FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
    TYPIFY `scs_3T5` EXISTS_TAC;
    REWRITE_TAC[];
    MATCH_MP_TAC Ppbtydq.XWNHLMD_MM;
    ASM_REWRITE_TAC[];
    REWRITE_TAC[Ocbicby.is_scs_examples;Ocbicby.basic_examples];
    nCONJ_TAC 1;
      BY(ASM_MESON_TAC[IN]);
    CONJ_TAC;
      BY(REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_3T5;Appendix.scs_k_v39_explicit;Appendix.mk_unadorned_v39]);
    ASM_REWRITE_TAC[];
    CONJ2_TAC;
      REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_3T5;Appendix.scs_d_v39_explicit;Appendix.mk_unadorned_v39];
      BY(REAL_ARITH_TAC);
    REWRITE_TAC[IN;Appendix.BBs_v39];
    REPEAT LET_TAC;
    REWRITE_TAC[Appendix.scs_3T5;Appendix.scs_v39_explicit;Terminal.scs_unadorned_explicit];
    TYPIFY `BBs_v39 scs_3M1 v` (C SUBGOAL_THEN MP_TAC);
      MATCH_MP_TAC Nuxcoea.MMS_IMP_BBS;
      BY(ASM_MESON_TAC[IN]);
    REWRITE_TAC[IN;Appendix.BBs_v39];
    ASM_REWRITE_TAC[];
    REWRITE_TAC[LET_THM];
    REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_v39_explicit;Terminal.scs_unadorned_explicit];
    REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[];
    MATCH_MP_TAC Terminal.periodic2_mod_reduce;
    TYPIFY `3` EXISTS_TAC;
    REWRITE_TAC[arith `~(3 =0)`];
    CONJ_TAC;
      FIRST_X_ASSUM_ST `periodic` MP_TAC;
      REWRITE_TAC[Appendix.periodic2;Oxl_def.periodic];
      DISCH_THEN (unlist REWRITE_TAC);
      BY(MESON_TAC[Terminal.periodic2_funlist;Appendix.periodic2]);
    REWRITE_TAC[arith `i < 3 <=> i = 0 \/ i = 1 \/ i = 2 `];
    REWRITE_TAC[TAUT ` ((a \/ b) /\ c) <=> ((a /\ c) \/ (b /\ c))`;TAUT `(a /\ (b \/ c)) <=> ((a /\ b) \/ (a /\ c))`];
    BY(REPEAT STRIP_TAC THEN (FIRST_X_ASSUM (C INTRO_TAC [`i`;`j`])) THEN ASM_REWRITE_TAC[] THEN NUM_REDUCE_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN NUM_REDUCE_TAC THEN REWRITE_TAC[Appendix.psort;LET_THM;Terminal.FUNLIST_EXPLICIT] THEN NUM_REDUCE_TAC THEN FIRST_X_ASSUM_ST `sqrt8` MP_TAC THEN REWRITE_TAC[DIST_SYM;PAIR_EQ] THEN NUM_REDUCE_TAC THEN TRY REAL_ARITH_TAC);
  COMMENT "second half";
  TYPIFY `?v. MMs_v39 s v /\ sqrt8 <= dist(v 0,v 1)` (C SUBGOAL_THEN MP_TAC);
    FIRST_X_ASSUM_ST `{}` MP_TAC THEN REWRITE_TAC[EXTENSION;NOT_IN_EMPTY];
    BY(REWRITE_TAC[IN] THEN ASM_MESON_TAC[arith `~(x <= y) ==> (y <= x)`]);
  POP_ASSUM kill;
  REPEAT WEAKER_STRIP_TAC;
  TYPIFY `scs_3T1` EXISTS_TAC;
  REWRITE_TAC[];
  MATCH_MP_TAC Ppbtydq.XWNHLMD_MM;
  ASM_REWRITE_TAC[];
  REWRITE_TAC[Ocbicby.is_scs_examples;Ocbicby.basic_examples];
  nCONJ_TAC 1;
    BY(ASM_MESON_TAC[IN]);
  CONJ_TAC;
    BY(REWRITE_TAC[Appendix.scs_3T1;Appendix.scs_3M1;Appendix.scs_k_v39_explicit;Appendix.mk_unadorned_v39]);
  ASM_REWRITE_TAC[];
  CONJ2_TAC;
    REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_3T1;Appendix.scs_d_v39_explicit;Appendix.mk_unadorned_v39];
    BY(REAL_ARITH_TAC);
  REWRITE_TAC[IN;Appendix.BBs_v39];
  REPEAT LET_TAC;
  REWRITE_TAC[Appendix.scs_3T1;Appendix.scs_v39_explicit;Terminal.scs_unadorned_explicit];
  TYPIFY `BBs_v39 scs_3M1 v` (C SUBGOAL_THEN MP_TAC);
    MATCH_MP_TAC Nuxcoea.MMS_IMP_BBS;
    BY(ASM_MESON_TAC[IN]);
  REWRITE_TAC[IN;Appendix.BBs_v39];
  ASM_REWRITE_TAC[];
  REWRITE_TAC[LET_THM];
  REWRITE_TAC[Appendix.scs_3M1;Appendix.scs_v39_explicit;Terminal.scs_unadorned_explicit];
  REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[];
  MATCH_MP_TAC Terminal.periodic2_mod_reduce;
  TYPIFY `3` EXISTS_TAC;
  REWRITE_TAC[arith `~(3 =0)`];
  CONJ_TAC;
    FIRST_X_ASSUM_ST `periodic` MP_TAC;
    REWRITE_TAC[Appendix.periodic2;Oxl_def.periodic];
    DISCH_THEN (unlist REWRITE_TAC);
    BY(MESON_TAC[Terminal.periodic2_funlist;Appendix.periodic2]);
  REWRITE_TAC[arith `i < 3 <=> i = 0 \/ i = 1 \/ i = 2 `];
  REWRITE_TAC[TAUT ` ((a \/ b) /\ c) <=> ((a /\ c) \/ (b /\ c))`;TAUT `(a /\ (b \/ c)) <=> ((a /\ b) \/ (a /\ c))`];
  BY(REPEAT STRIP_TAC THEN (FIRST_X_ASSUM (C INTRO_TAC [`i`;`j`])) THEN ASM_REWRITE_TAC[] THEN NUM_REDUCE_TAC THEN ASM_REWRITE_TAC[Terminal.FUNLIST_EXPLICIT] THEN NUM_REDUCE_TAC THEN REWRITE_TAC[Appendix.psort;LET_THM;Terminal.FUNLIST_EXPLICIT] THEN NUM_REDUCE_TAC THEN FIRST_X_ASSUM_ST `sqrt8` MP_TAC THEN REWRITE_TAC[DIST_SYM;PAIR_EQ] THEN NUM_REDUCE_TAC THEN TRY REAL_ARITH_TAC)
  ]);;
  (* }}} *)

end;;