(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Local Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2012-04-01                                                           *)
(* ========================================================================= *)


(*
remaining conclusions from appendix to Local Fan chapter
*)


module Ppbtydq = struct


open Polyhedron;;
open Sphere;;
open Topology;;		
open Fan_misc;;
open Planarity;; 
open Conforming;;
open Hypermap;;
open Fan;;
open Topology;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Collect_geom;;
open Dih2k_hypermap;;
open Wjscpro;;
open Tecoxbm;;
open Hdplygy;;
open Nkezbfc_local;;
open Flyspeck_constants;;
open Gbycpxs;;
open Pcrttid;;
open Local_lemmas1;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;





open Hypermap;;
open Fan;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Flyspeck_constants;;
open Pack_defs;;

open Hales_tactic;;

open Appendix;;


open Zithlqn;;


open Xwitccn;;

open Ayqjtmd;;

open Jkqewgv;;


open Mtuwlun;;


open Uxckfpe;;
open Sgtrnaf;;

open Yxionxl;;

open Qknvmlb;;
open Odxlstcv2;;

open Yxionxl2;;
open Eyypqdw;;
open Ocbicby;;
open Imjxphr;;

open Nuxcoea;;
open Fektyiy;;



let PPBTYDQ_concl = `!(u:real^3) v p. ~collinear {vec 0,v,p} /\ ~collinear {vec 0,u,p} /\
  arcV (vec 0) u p + arcV (vec 0) p v < pi ==> ~(vec 0 IN conv{u,v})`;;



let PPBTYDQ= prove_by_refinement((PPBTYDQ_concl),
[REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ABBREV_TAC `e= u cross (p:real^3)`
THEN SUBGOAL_THEN`orthogonal e (u:real^3)`ASSUME_TAC;

EXPAND_TAC "e"
THEN REWRITE_TAC[orthogonal;DOT_CROSS_SELF];


SUBGOAL_THEN`orthogonal e (p:real^3)`ASSUME_TAC;

EXPAND_TAC "e"
THEN REWRITE_TAC[orthogonal;DOT_CROSS_SELF];


REWRITE_TAC[Collect_geom.CONV_SET2;IN_ELIM_THM;VECTOR_ARITH`vec 0 = a % u + b % v<=> b % v = (--a) % u `]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC(REAL_ARITH`&0<=b==> b= &0\/ &0< b`)
THEN RESA_TAC;


REWRITE_TAC[VECTOR_ARITH`&0 % v = --a % u<=> a % u= vec 0`;VECTOR_MUL_EQ_0;REAL_ARITH`a + &0= &1<=> a= &1`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`~(&1= &0)`]
THEN MRESA_TAC th3[`vec 0:real^3`;`u`;`p`];


MP_TAC(REAL_ARITH`&0<=a==> a= &0\/ &0< a`)
THEN RESA_TAC;


REWRITE_TAC[VECTOR_ARITH`b % v = -- &0 % u<=> b % v= vec 0`;VECTOR_MUL_EQ_0;REAL_ARITH` &0+a= &1<=> a= &1`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`~(&1= &0)`]
THEN MRESA_TAC th3[`vec 0:real^3`;`v`;`p`];

REPEAT STRIP_TAC
THEN MP_TAC(SET_RULE`b % v = --a % u
==> (inv b) %b % v = (inv b) % --a % u:real^3`)
THEN REWRITE_TAC[VECTOR_ARITH`a%b%c=(a*b)%c`]
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`&0< b==> ~(b= &0)`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[REAL_MUL_LINV;VECTOR_ARITH`&1 %v= v`]
THEN SUBGOAL_THEN`(inv b * --a)< &0` ASSUME_TAC;

MATCH_MP_TAC(REAL_ARITH`&0<(inv b *a)==> (inv b * --a)< &0`)
THEN MATCH_MP_TAC REAL_LT_MUL
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC REAL_LT_INV
THEN ASM_REWRITE_TAC[];

ABBREV_TAC `v'=(inv b * --a)`
THEN STRIP_TAC
THEN DICH_TAC (15-5)
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC th3[`vec 0:real^3`;`u`;`p`];




MRESA_TAC Local_lemmas1.ARCV_PI_OPPOSITE[`v'`;`u`;`vec 0:real^3`]
THEN POP_ASSUM MP_TAC
THEN REDUCE_VECTOR_TAC
THEN STRIP_TAC
THEN SYM_ASSUM_TAC
THEN REWRITE_TAC[REAL_ARITH`~(a<b)<=> b<=a`]
THEN MATCH_MP_TAC Trigonometry.KEITDWB
THEN MRESAL_TAC th3[`vec 0:real^3`;`v`;`p`][VECTOR_ARITH`&0 % a= vec 0`]]);;

let OIQKKEP_concl = `!u v c.
  u IN ball_annulus /\ v IN ball_annulus /\ c < &4 /\ dist(u,v) <= c /\ &2<= dist(u,v)==>
  arcV (vec 0) u v <= arclength (&2) (&2) c`;;


let OIQKKEP = prove_by_refinement(
 OIQKKEP_concl,
[
REWRITE_TAC[Ckqowsa_3_points.in_ball_annulus;dist]
THEN REPEAT STRIP_TAC
THEN MRESAL_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`u`;`v`][dist;VECTOR_ARITH`vec 0- A= --A`; NORM_NEG]
THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`u`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A`]
THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`v`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A`]
THEN MRESAL_TAC NORM_TRIANGLE[`u:real^3`;`-- v:real^3`][VECTOR_ARITH`a+ --b=a-b:real^3`;NORM_NEG]
THEN MRESAL_TAC NORM_TRIANGLE[`v:real^3`;`u- v:real^3`][VECTOR_ARITH`a+ b-a=b:real^3`;NORM_NEG]
THEN MRESAL_TAC NORM_TRIANGLE[`u-v:real^3`;`-- u:real^3`][VECTOR_ARITH`a- b+ --a= --b:real^3`;NORM_NEG]
THEN MRESAL_TAC Trigonometry1.ACS_ARCLENGTH[`norm (u)`;`norm v`;`norm(u-v)`]
[NORM_POS_LE]
THEN MP_TAC(REAL_ARITH`norm (u - v:real^3) <= c /\ c< &4 /\ &0<= norm (u - v)
==> &0 <= c /\ c <= &2 + &2 /\ &2 <= &2 + c /\ &2 <= c + &2 /\ c<= &4`)
THEN ASM_REWRITE_TAC[NORM_POS_LE]
THEN RESA_TAC
THEN MRESAL_TAC Trigonometry1.ACS_ARCLENGTH[`&2`;`&2`;`c:real`]
[NORM_POS_LE;REAL_ARITH`&0< &2`]
THEN MATCH_MP_TAC ACS_MONO_LE
THEN STRIP_TAC;


REWRITE_TAC[REAL_ARITH`-- &1 <= (&2 * &2 + &2 * &2 - c * c) / (&2 * &2 * &2)
<=> c*c<= &4* &4`]
THEN MATCH_MP_TAC Misc_defs_and_lemmas.ABS_SQUARE_LE
THEN MRESA_TAC REAL_ABS_REFL[`c`];

STRIP_TAC;

MRESAL_TAC Imjxphr.xrr_increasing_le[`&2`;`&2`;`norm(u-v)`;`c`][NORM_POS_LE;REAL_ARITH`&0< &2`]
THEN MRESAL_TAC Ocbicby.xrr_decreasing[`&2`;`norm u`;`&2`;`norm(u-v)`]
[NORM_POS_LE;REAL_ARITH`&2<= &2/\ &2 <= &2 * #1.26`;h0]
THEN MRESAL_TAC Ocbicby.xrr_decreasing[`&2`;`norm v`;`norm u`;`norm(u-v)`]
[NORM_POS_LE;REAL_ARITH`&2<= &2/\ &2 <= &2 * #1.26`;h0;]
THEN POP_ASSUM MP_TAC
THEN ONCE_REWRITE_TAC[Ocbicby.xrr_sym]
THEN STRIP_TAC 
THEN MP_TAC(REAL_ARITH`xrr (&2) (&2) (norm (u - v)) <= xrr (&2) (&2) c
/\ xrr (norm u) (&2) (norm (u - v)) <= xrr (&2) (&2) (norm (u - v))
/\ xrr (norm u) (norm v) (norm (u - v)) <= xrr (norm u) (&2) (norm (u - v:real^3))
==> xrr (norm u) (norm v) (norm (u - v))<= xrr (&2) (&2) c`)
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[xrr]
THEN REAL_ARITH_TAC;

MRESAL_TAC Trigonometry1.TRI_SQUARES_BOUNDS[`norm u`;`norm v`;`norm(u-v)`]
[NORM_POS_LE]]);;




let MXQTIED_concl = `!s s' v.
  is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
  scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
 scs_d_v39 s'= scs_d_v39 s /\
  v IN MMs_v39 s /\ v IN BBs_v39 s' /\
  (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i)) 
/\ (!i j. scs_a_v39 s i j<= scs_a_v39 s' i j/\ scs_b_v39 s' i j<= scs_b_v39 s i j) ==>
    v IN MMs_v39 s'`;;


let MXQTIED_PRIME2_concl = `
  is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
  scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
 scs_d_v39 s'= scs_d_v39 s /\
  v IN MMs_v39 s /\ v IN BBs_v39 s' /\
  (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i)) 
/\ (!i j. scs_a_v39 s i j<= scs_a_v39 s' i j/\ scs_b_v39 s' i j<= scs_b_v39 s i j) ==>
    BBprime2_v39 s' v`;;



let MXQTIED_PRIME_concl = `
  is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
  scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
 scs_d_v39 s'= scs_d_v39 s /\
  v IN BBprime_v39 s /\ v IN BBs_v39 s' /\
  (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i)) 
/\ (!i j. scs_a_v39 s i j<= scs_a_v39 s' i j/\ scs_b_v39 s' i j<= scs_b_v39 s i j) ==>
    BBprime_v39 s' v`;;





let MXQTIED_TAU_concl = `
  is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
  scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
 scs_d_v39 s'= scs_d_v39 s /\
  (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i)) ==>
    taustar_v39 s' v= taustar_v39 s v`;;


let MXQTIED_TAU_DSV_concl = `
  is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
  scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
 scs_d_v39 s'= scs_d_v39 s /\
  (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i)) 
==>
    dsv_v39 s' v= dsv_v39 s v`;;


let MXQTIED_BB_concl = `!s s' v.
  is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
  scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
 scs_d_v39 s'= scs_d_v39 s /\
   v IN BBs_v39 s' /\
  (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i))
/\ (!i j. scs_a_v39 s i j<= scs_a_v39 s' i j/\ scs_b_v39 s' i j<= scs_b_v39 s i j) ==>
     BBs_v39 s v`;;







let MXQTIED_INDEX_concl = `
  is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
  scs_M s = scs_M s' /\ scs_k_v39 s = scs_k_v39 s' /\
 scs_d_v39 s'= scs_d_v39 s /\
   v IN BBs_v39 s' /\
  (!i. scs_a_v39 s' i (SUC i) = scs_a_v39 s i (SUC i))
/\ (!i j. scs_a_v39 s i j<= scs_a_v39 s' i j/\ scs_b_v39 s' i j<= scs_b_v39 s i j) ==>
     BBindex_v39 s' v= BBindex_v39 s v`;;



let MXQTIED_INDEX=prove( MXQTIED_INDEX_concl,
REWRITE_TAC[IN;BBindex_v39]
THEN REPEAT RESA_TAC);;





let  MXQTIED_BB=prove_by_refinement( MXQTIED_BB_concl,
[REWRITE_TAC[IN;scs_basic]
THEN REPEAT STRIP_TAC
THEN DICH_TAC 2
THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;taustar_v39;dsv_v39;SET_RULE`{i| F}={}`;SUM_CLAUSES;REAL_ARITH`a* &0= &0`]
THEN REPEAT RESA_TAC;

THAYTHE_TAC 1[`i`;`j:num`]
THEN THAYTHE_TAC (15-10)[`i`;`j`]
THEN DICH_TAC 1
THEN DICH_TAC 2
THEN REAL_ARITH_TAC;

THAYTHE_TAC 1[`i`;`j:num`]
THEN THAYTHE_TAC (15-10)[`i`;`j`]
THEN DICH_TAC 0
THEN DICH_TAC 1
THEN REAL_ARITH_TAC;

THAYTHE_TAC 1[`i`;`j:num`]
THEN THAYTHE_TAC (15-10)[`i`;`j`]
THEN DICH_TAC 1
THEN DICH_TAC 2
THEN REAL_ARITH_TAC;

THAYTHE_TAC 1[`i`;`j:num`]
THEN THAYTHE_TAC (15-10)[`i`;`j`]
THEN DICH_TAC 0
THEN DICH_TAC 1
THEN REAL_ARITH_TAC]);;


let MXQTIED_TAU_DSV =prove(MXQTIED_TAU_DSV_concl,
REWRITE_TAC[IN;scs_basic]
THEN REPEAT STRIP_TAC
THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;taustar_v39;dsv_v39;SET_RULE`{i| F}={}`;SUM_CLAUSES;REAL_ARITH`a* &0= &0`]
THEN REPEAT STRIP_TAC);;


let MXQTIED_TAU =prove(MXQTIED_TAU_concl,
REWRITE_TAC[IN;scs_basic]
THEN REPEAT STRIP_TAC
THEN MP_TAC MXQTIED_TAU_DSV
THEN REWRITE_TAC[IN;scs_basic]
THEN RESA_TAC THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;taustar_v39;]
THEN REPEAT STRIP_TAC);;



let MXQTIED_PRIME=prove_by_refinement( 
 MXQTIED_PRIME_concl,
[
REWRITE_TAC[IN;scs_basic]
THEN REPEAT STRIP_TAC
THEN MP_TAC MXQTIED_TAU_DSV
THEN REWRITE_TAC[IN;scs_basic]
THEN RESA_TAC THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;]
THEN REPEAT STRIP_TAC;

MP_TAC MXQTIED_TAU
THEN REWRITE_TAC[IN;scs_basic]
THEN RESA_TAC
THEN MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`ww`][IN;scs_basic]
THEN DICH_TAC (16-9)
THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;]
THEN REPEAT RESA_TAC
THEN MATCH_DICH_TAC (18-17)
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC MXQTIED_BB
THEN ASM_REWRITE_TAC[IN;scs_basic]
THEN EXISTS_TAC`s':scs_v39`
THEN ASM_REWRITE_TAC[];

MP_TAC MXQTIED_TAU
THEN REWRITE_TAC[IN;scs_basic]
THEN RESA_TAC
THEN DICH_TAC (14-9)
THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;]
THEN REPEAT RESA_TAC]);;


let BBPRIME_IMP_BB=
prove(`BBprime_v39 s' w ==> BBs_v39 s' w`,

ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime_v39;]
THEN RESA_TAC);;


let MXQTIED_PRIME2=prove_by_refinement( MXQTIED_PRIME2_concl,
[
REWRITE_TAC[IN;scs_basic]
THEN REPEAT STRIP_TAC
THEN MRESA_TAC(GEN_ALL Nuxcoea.MMS_IMP_BBPRIME)[`s`;`v`]
THEN MP_TAC MXQTIED_PRIME
THEN REWRITE_TAC[IN;scs_basic]
THEN RESA_TAC THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;]
THEN REPEAT STRIP_TAC
THEN MP_TAC MXQTIED_INDEX
THEN REWRITE_TAC[IN;scs_basic]
THEN RESA_TAC
THEN MP_TAC(SET_RULE`(?w. BBprime_v39 (s':scs_v39) w /\ BBindex_v39 s w< BBindex_v39 s v) \/ ~(?w.  BBprime_v39 s' w /\ BBindex_v39 s w< BBindex_v39 s v)`)
THEN RESA_TAC;

MP_TAC BBPRIME_IMP_BB
THEN RESA_TAC
THEN MRESAL_TAC MXQTIED_BB[`s`;`s'`;`w`][scs_basic;IN]
THEN DICH_TAC (19-9)
THEN ASM_REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;]
THEN RESA_TAC
THEN DICH_TAC(24-19)
THEN REWRITE_TAC[BBindex_min_v39]
THEN SUBGOAL_THEN`BBprime_v39 s (w:num->real^3)`ASSUME_TAC;

ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBprime_v39;]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`w`][scs_basic;IN]
THEN MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`ww:num->real^3`][scs_basic;IN]
THEN SYM_ASSUM_TAC
THEN SYM_ASSUM_TAC
THEN DICH_TAC (28-19)
THEN STRIP_TAC;

THAYTHE_TAC 0[`v`]
THEN THAYTHE_TAC (28-13)[`ww`]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`v`][scs_basic;IN]
THEN MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`ww`][scs_basic;IN]
THEN REAL_ARITH_TAC;

MRESAL_TAC MXQTIED_TAU[`s'`;`s`;`w`][scs_basic;IN];

SUBGOAL_THEN`BBindex_v39 s w IN IMAGE (BBindex_v39 s) (BBprime_v39 s)`ASSUME_TAC;

REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN REWRITE_TAC[IN]
THEN EXISTS_TAC`w:num->real^3`
THEN ASM_REWRITE_TAC[];

MRESA_TAC Nuxcoea.MIN_LEAST[`(IMAGE (BBindex_v39 s) (BBprime_v39 s))`;`BBindex_v39 s w`]
THEN STRIP_TAC
THEN DICH_TAC(28-16)
THEN DICH_TAC 1
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;


POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_EXISTS_THM;BBindex_min_v39]
THEN STRIP_TAC
THEN SUBGOAL_THEN`BBindex_v39 s v IN IMAGE (BBindex_v39 s') (BBprime_v39 s')`ASSUME_TAC;

REWRITE_TAC[IN_ELIM_THM;IMAGE]
THEN REWRITE_TAC[IN]
THEN EXISTS_TAC`v:num->real^3`
THEN ASM_REWRITE_TAC[];

MRESA_TAC Nuxcoea.MIN_LEAST[`(IMAGE (BBindex_v39 s') (BBprime_v39 s'))`;`BBindex_v39 s v`]
THEN MP_TAC(ARITH_RULE`min_num (IMAGE (BBindex_v39 s') (BBprime_v39 s')) <= BBindex_v39 s v
==> min_num (IMAGE (BBindex_v39 s') (BBprime_v39 s')) < BBindex_v39 s v
\/ min_num (IMAGE (BBindex_v39 s') (BBprime_v39 s')) = BBindex_v39 s v`)
THEN RESA_TAC;

DICH_TAC 2
THEN REWRITE_TAC[GSYM BBindex_min_v39]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN REWRITE_TAC[IN]
THEN RESA_TAC 
THEN THAYTHE_TAC(21-16)[`x`]
THEN POP_ASSUM MP_TAC
THEN DICH_TAC 2
THEN ASM_REWRITE_TAC[GSYM BBindex_min_v39]
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC BBPRIME_IMP_BB[`s'`;`x`]
THEN MRESAL_TAC MXQTIED_INDEX[`s'`;`s`;`x`][IN;scs_basic]
THEN RESA_TAC]);;




let MXQTIED=prove(MXQTIED_concl,
REWRITE_TAC[IN;scs_basic;]
THEN REPEAT STRIP_TAC
THEN MP_TAC MXQTIED_PRIME2
THEN REWRITE_TAC[IN;scs_basic;]
THEN RESA_TAC
THEN MRESA_TAC Ayqjtmd.unadorned_MMs[`s'`]);;






let SCS_BASIC_DSV=
prove(`  is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
  scs_k_v39 s = scs_k_v39 s' /\ scs_d_v39 s<= scs_d_v39 s' ==>
dsv_v39 s v <= dsv_v39  s' v`,

REWRITE_TAC[taustar_v39;LET_DEF;LET_END_DEF;IN;dsv_v39;scs_basic;SET_RULE`{i| F}={}`;SUM_CLAUSES;REAL_ARITH`a* &0= &0`]
THEN RESA_TAC
THEN ASM_REWRITE_TAC[SET_RULE`{i| F}={}`;SUM_CLAUSES;REAL_ARITH`a* &0= &0/\ a+ &0=a`]);;






let SCS_BASIC_TAUSTAR=
prove(`  is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
  scs_k_v39 s = scs_k_v39 s' 
/\ scs_d_v39 s<= scs_d_v39 s' 
==> taustar_v39 s' v <= taustar_v39  s v`,

STRIP_TAC
THEN MP_TAC SCS_BASIC_DSV
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[taustar_v39;LET_DEF;LET_END_DEF]
THEN MP_TAC(SET_RULE`scs_k_v39 s' <= 3 \/ ~(scs_k_v39 s' <= 3)`)
THEN RESA_TAC
THEN REAL_ARITH_TAC);;

let TAUSTAR_LE_0_XWNHLMD=
prove(`  is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
  scs_k_v39 s = scs_k_v39 s' /\
  v IN MMs_v39 s /\ v IN BBs_v39 s' /\ scs_d_v39 s<= scs_d_v39 s' 
  ==> taustar_v39 s' v< &0`,

REWRITE_TAC[IN;LET_DEF;LET_END_DEF;MMs_v39;BBprime2_v39;BBprime_v39]
THEN STRIP_TAC
THEN MP_TAC SCS_BASIC_TAUSTAR
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN DICH_TAC(15-7)
THEN REAL_ARITH_TAC);;





let XWNHLMD_MM=
prove(`  is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
  scs_k_v39 s = scs_k_v39 s' /\
  v IN MMs_v39 s /\ v IN BBs_v39 s' /\ scs_d_v39 s<= scs_d_v39 s' 
==> ~(MMs_v39 s' ={})`,

STRIP_TAC
THEN MP_TAC TAUSTAR_LE_0_XWNHLMD
THEN RESA_TAC
THEN MATCH_MP_TAC SGTRNAF
THEN EXISTS_TAC`v:num->real^3`
THEN ASM_REWRITE_TAC[]
THEN ASM_TAC
THEN REWRITE_TAC[scs_basic]
THEN REPEAT RESA_TAC);;
let XWNHLMD_concl = `!s s' v.
  is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
  scs_k_v39 s = scs_k_v39 s' /\ scs_d_v39 s<= scs_d_v39 s' /\  
  v IN MMs_v39 s /\ v IN BBs_v39 s' ==>
  scs_arrow_v39 {s} {s'}`;;




let XWNHLMD=prove_by_refinement(XWNHLMD_concl,
[REPEAT GEN_TAC
THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;IN]
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN REPEAT RESA_TAC;

DISJ_CASES_TAC(SET_RULE`(!s'. s' = s ==> MMs_v39 s' = {}) \/ ~((!s'. s' = s ==> MMs_v39 s' = {}))`);

ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
THEN REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN RESA_TAC
THEN EXISTS_TAC`s':scs_v39`
THEN ASM_REWRITE_TAC[]
THEN MATCH_MP_TAC XWNHLMD_MM
THEN ASM_REWRITE_TAC[IN]]);;
 end;;


(*
let check_completeness_claimA_concl = 
  Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) 
*)