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


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


module Tfitskc = 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 Aursipd;;
open Cuxvzoz;;
open Rrcwnsj;;



let SCS_DIAG_A_LE_DIST=prove(`(!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j)/\ &4 * h0 < scs_b_v39 s i j))
==>  (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j < dist(v i, (v:num->real^3) j)))`,
REPEAT RESA_TAC
THEN THAYTHE_TAC 1[`i`;`j`]
THEN ASM_TAC
THEN REAL_ARITH_TAC);;


let DIST_EQ_2_IMP_A_EQ_2=prove(`is_scs_v39 s/\ BBs_v39 s v /\ dist (v i,v (SUC i)) = &2
==> scs_a_v39 s i (SUC i) = &2`,
REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;is_scs_v39]
THEN RESA_TAC
THEN ABBREV_TAC`k= scs_k_v39 s`
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD k`;`SUC i MOD k `;`s:scs_v39`;`i`;`SUC i`][MOD_REFL;MOD_MULT_ADD;ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`;is_scs_v39]
THEN THAYTHES_TAC (26-14)[`i MOD k`;`SUC i MOD k`][DIVISION;ARITH_RULE`3<=k==> ~(k=0)/\ 1<k`;Qknvmlb.SUC_MOD_NOT_EQ]
THEN DICH_TAC 0
THEN THAYTHE_TAC 4[`i`;`SUC i`]
THEN DICH_TAC 1
THEN REAL_ARITH_TAC);;


let SCS_DIAG_2=prove(`3<k==> scs_diag k i (SUC (SUC i))`,
STRIP_TAC
THEN REWRITE_TAC[scs_diag;ADD1]
THEN MP_TAC(ARITH_RULE`3<k==> (i+1)+1=i+2/\ (i+2)+1=i+3/\ ~(k=0)/\ k-1<k
/\ (i+1)+1=i+2 /\ 1<k /\ 2<k/\ 0<k/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`i= i+0==> i MOD k= (i+0) MOD k`)
THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
THEN RESA_TAC
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]);;


let TFITSKCv1_concl = `
main_nonlinear_terminal_v11
==> (!s (v:num->real^3) i.
(!i'. ~scs_J_v39 s (SUC (SUC i)) i')/\
 scs_a_v39 s (SUC (SUC i)) (SUC(SUC(SUC i)))< scs_b_v39 s (SUC (SUC i)) (SUC(SUC(SUC i))) /\
3< scs_k_v39 s  /\
is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
  scs_a_v39 s (i+1) (i+2) = &2 /\ scs_b_v39 s (i+1) (i+2) <= &2 * h0 /\
  dist(v i,v (i+1)) = &2 /\ dist(v i,v (i+1))< scs_b_v39 s i (i+1) /\
  (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j)/\ &4 * h0 < scs_b_v39 s i j)) ==>
  dist(v (i+1),v(i+2)) = &2)`;;






let TFITSKCv1=prove_by_refinement(  TFITSKCv1_concl,
[
STRIP_TAC
THEN REWRITE_TAC[IN;GSYM ADD1;ARITH_RULE`i+2=SUC(SUC i)`;scs_generic]
THEN REPEAT GEN_TAC
THEN STRIP_TAC
THEN ABBREV_TAC`k=scs_k_v39 s`
THEN ABBREV_TAC`V=(IMAGE (v:num->real^3) (:num))`
THEN ABBREV_TAC`E=(IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num))`
THEN ABBREV_TAC`FF=IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k`;`s`;`v`]
THEN MP_TAC Local_lemmas.CVLF_LF_F
THEN RESA_TAC
THEN MP_TAC SCS_DIAG_A_LE_DIST
THEN RESA_TAC
THEN MRESAL_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`][ARITH_RULE`SUC(i+1)=i+2`;GSYM dist]
THEN MP_TAC(REAL_ARITH`&2 <= dist (v (SUC i),v (SUC(SUC i)))
==> dist (v (SUC i),v (SUC(SUC i))) = &2 \/ &2 < dist (v (SUC i),(v:num->real^3) (SUC(SUC i)))`)
THEN RESA_TAC
THEN MRESA_TAC WL_IN_V[`i`;`v:num->real^3`]
THEN MRESA_TAC WL_IN_V[`SUC i`;`v:num->real^3`]
THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (SUC i)`;`v`;`SUC i`;`k`]
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (SUC i)`][GSYM ADD1]
THEN THAYTHE_TAC 0[`v i`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (SUC i)) (v (SUC (SUC i))) (v i) <= pi
==> azim (vec 0) (v (SUC i)) (v (SUC (SUC i))) (v i) = pi
\/ azim (vec 0) (v (SUC i)) (v (SUC (SUC i))) ((v:num->real^3) i) < pi`)
THEN RESA_TAC;



MP_TAC Jcyfmrp.J_EMPY_CASES_A_EQ_2_V1
THEN DICH_TAC 0
THEN REWRITE_TAC[SET_RULE`(a = {})<=> !i. ~ (a i)`]
THEN STRIP_TAC
THEN MP_TAC DIST_EQ_2_IMP_A_EQ_2
THEN RESA_TAC
THEN STRIP_TAC
THEN MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
THEN MRESA_TAC Imjxphr.EQ_W_L_IN_BBS[`s`;`k`;`v`;`i`]
THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_EXISTS_THM]
THEN STRIP_TAC
THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (SUC i)) V' E')` ASSUME_TAC;



REPEAT RESA_TAC
;



SUBGOAL_THEN`~collinear {vec 0, (v:num->real^3) (SUC (SUC i)), v (i)}`
ASSUME_TAC;


MRESAS_TAC WL_IN_V[`SUC (SUC i)`;`v:num->real^3`][BB_VV_FUN_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (SUC(SUC i))`;`v i`;`V`]
THEN THAYTHES_TAC 0[`v (SUC(SUC i))`;`v i`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;ARITH_RULE`SUC (SUC x)=x+2`;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MATCH_DICH_TAC 0
THEN MP_TAC(SET_RULE`i= i+0==> i MOD k= (i+0) MOD k`)
THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 0<k/\ 2<k/\ ~(2=0)`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT];





SUBGOAL_THEN`(v:num->real^3) (SUC i) IN aff_gt {vec 0} {v (SUC (SUC i)), v (i)}`
ASSUME_TAC;




MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v ((SUC i))`;`v i`;`V`]
THEN THAYTHES_TAC 0[`v (SUC i)`;`v i`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;ADD1]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`i= i+0==> i MOD k= (i+0) MOD k`)
THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 0<k/\ 1<k/\ 2<k /\ ~(1=0)/\ ~(2=1)`)
THEN RESA_TAC
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
THEN MRESAL_TAC WL_IN_V[`SUC (SUC i)`;`v:num->real^3`][] 
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (SUC (SUC i))`;`v (SUC i)`;`V`]
THEN THAYTHES_TAC 0[`(v:num->real^3) (SUC(SUC i))`;`v (SUC i)`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;ADD1;ARITH_RULE`(i+1)+1=i+2`;MOD_LT]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`i+2=(i+1)+1`;GSYM ADD1]
THEN REPEAT STRIP_TAC
THEN DICH_TAC 1
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN RESA_TAC
THEN DICH_TAC (45-3)
THEN REWRITE_TAC[GSYM ADD1;generic]
THEN STRIP_TAC
THEN MRESAL_TAC WL_IN_E[`SUC i`;`v:num->real^3`][] 
THEN THAYTHE_TAC 1[`v (SUC i)`;`v(SUC(SUC i))`;`v i`]
THEN MRESAS_TAC Polar_fan.GENERIC_LOCAL_FAN_STRAIGHT_AFF_GE[`v i`;`v (SUC i)`;`v(SUC(SUC i))`;][]
THEN DICH_TAC 0
THEN MRESA_TAC th3[`vec 0:real^3`;`v (SUC(SUC i))`;`v i`]
THEN MRESAS_TAC Local_lemmas.FAN_IMP_NOT_IN_AFF_GE[`E`;`V`;`v (SUC i)`;`vec 0:real^3`;`v i`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`;BB_VV_FUN_EQ;ADD1]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`i= i+0==> i MOD k= (i+0) MOD k`)
THEN GEN_REWRITE_TAC( LAND_CONV o LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
THEN MRESAS_TAC Local_lemmas.FAN_IMP_NOT_IN_AFF_GE[`E`;`V`;`v (SUC i)`;`vec 0:real^3`;`v (SUC(SUC i))`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`;BB_VV_FUN_EQ;ADD1;ARITH_RULE`(i+1)+1=i+2`;MOD_LT;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[ARITH_RULE`i+2=(i+1)+1`;GSYM ADD1]
THEN STRIP_TAC
THEN STRIP_TAC
THEN MRESAL_TAC Wrgcvdr_cizmrrh.AFF_GE_TO_AFF_GT2_GE1[`v i`;`vec 0:real^3`;`v (SUC(SUC i))`][UNION;IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[];




MRESAS_TAC NUXCOEAv2[`s`;`k`;`v`;`SUC i`;`i`][ARITH_RULE`SUC i + k - 1=SUC (i + k - 1)`];




MRESAL_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`][Fnjlbxs.in_ball_annulus]
THEN MP_TAC(REAL_ARITH`&2 <= norm (v (SUC(SUC i)))
==>  norm (v (SUC(SUC i)))= &2\/ &2 < norm ((v:num->real^3) (SUC(SUC i)))`)
THEN RESA_TAC;





MRESA_TAC Imjxphr.EQ_W_L_IN_BBS[`s`;`k`;`v`;`i`]
THEN MP_TAC SYNQIWN
THEN RESA_TAC
THEN THAYTHES_TAC 0[`s`;`v`;`SUC i`;`k`][Imjxphr.EQ_W_L_IN_BBS;ARITH_RULE`SUC i + k - 1=SUC( i + k - 1)`]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_REWRITE_TAC[]
THEN SUBGOAL_THEN`dist (v (SUC (SUC i)),(v:num->real^3) (SUC i)) <= &2 * h0`ASSUME_TAC;



REPLICATE_TAC (31-1) (POP_ASSUM MP_TAC)
THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)`)
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39;BBs_v39]
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC (52-36)[`SUC(SUC i)`;`SUC i`]THEN DICH_TAC (56-29)
THEN DICH_TAC 0
THEN REAL_ARITH_TAC;


ASM_REWRITE_TAC[]
THEN REWRITE_TAC[h0;REAL_ARITH`&2<= &2* #1.26`]
THEN SUBGOAL_THEN`cstab <= dist (v i,(v:num->real^3) (SUC (SUC i)))`ASSUME_TAC
;


MP_TAC(ARITH_RULE`3<k==> SUC (i + k - 1)= i+ 1*k+0/\ ~(k<=3)/\ ~(k=0)/\ k-1<k
/\ (i+1)+1=i+2 /\ 1<k /\ 2<k/\ 0<k/\ ~(2=0)/\ ~(2=1)/\ ~(3=0)`)
THEN RESA_TAC
THEN THAYTHES_TAC (43-10)[`SUC(SUC i)`;`i`][scs_diag;ADD1;ARITH_RULE`(i+1)+1=i+2/\(i+2)+1= i+3`;Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`i= i+0==> i MOD k= (i+0) MOD k`)
THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
THEN RESA_TAC
THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN DICH_TAC 1
THEN REAL_ARITH_TAC;

ASM_REWRITE_TAC[]
THEN STRIP_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN MP_TAC(ARITH_RULE`3<k==> SUC i+k-1=SUC(i+k-1)`)
THEN RESA_TAC 
;


MP_TAC Cuxvzoz.CUXVZOZ
THEN RESA_TAC
THEN THAYTHEL_TAC 0[`s`;`FF`;`k`;`SUC i`;`v`][scs_generic;GSYM ADD1;]
THEN MATCH_DICH_TAC 0
THEN STRIP_TAC;


THAYTHES_TAC (35-10)[`i`;`SUC(SUC i)`][SCS_DIAG_2]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;


REWRITE_TAC[REAL_ARITH`a<= a/\ &2<= #3.01`;cstab]
THEN STRIP_TAC;


REPEAT RESA_TAC
THEN THAYTHE_TAC (37-10)[`i'`;`j`]
THEN DICH_TAC 1
THEN DICH_TAC 1
THEN REAL_ARITH_TAC;


STRIP_TAC
;


REPEAT RESA_TAC
THEN THAYTHE_TAC (36-10)[`i'`;`j`]
;

STRIP_TAC
;



ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1]
;



ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1]
;


MP_TAC(REAL_ARITH`&2 < norm ((v:num->real^3) (SUC (SUC i))) ==> ~(&2 = norm (v (SUC (SUC i))))`)
THEN RESA_TAC
THEN SUBGOAL_THEN`(!i'. scs_diag k (SUC (SUC i)) i'
              ==> &4 * h0 < scs_b_v39 s (SUC (SUC i)) i')`ASSUME_TAC
;


REPEAT RESA_TAC
THEN THAYTHE_TAC(33-11)[`SUC(SUC i)`;`i'`]
;




MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_EXISTS_THM]
THEN STRIP_TAC
THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (SUC (SUC i))) V' E')` ASSUME_TAC;



REPEAT RESA_TAC;

MRESA_TAC ODXLSTCv2[`s`;`k`;`v`;`SUC(SUC i)`]
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
THEN STRIP_TAC
THEN THAYTHEL_ASM_TAC (41-21)[`SUC(SUC i)`;`i'`][scs_diag;]
THEN DICH_TAC 1
THEN REWRITE_TAC[DE_MORGAN_THM]
THEN ONCE_REWRITE_TAC[SET_RULE`A\/B<=> B\/A`]
THEN STRIP_TAC;



POP_ASSUM MP_TAC
THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+1=1+i`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`3<k==> ~(k=0)`]
THEN REWRITE_TAC[ARITH_RULE`1+i= SUC i`]
THEN STRIP_TAC
THEN DICH_TAC 2
THEN MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i'`;`v:num->real^3`;`SUC i:num`]
THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC(SUC i)`;`i' `;`s:scs_v39`;`SUC(SUC i)`;`SUC i`][]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN ASM_TAC
THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT RESA_TAC
;



SUBGOAL_THEN`scs_a_v39 s  (SUC (SUC (SUC i))) (SUC (SUC i))=  dist ((v:num->real^3) (SUC (SUC (SUC i))),v (SUC (SUC i)))`ASSUME_TAC
;


DICH_TAC 2
THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC(SUC i)`;`i' `;`s:scs_v39`;`SUC(SUC i)`;`SUC (SUC(SUC i))`][]
THEN MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i'`;`v:num->real^3`;`SUC (SUC(SUC i)):num`]
THEN DICH_TAC(43-17)
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT RESA_TAC
THEN THAYTHE_TAC 1[`SUC(SUC i)`;`SUC(SUC(SUC i))`]
THEN DICH_TAC 1
THEN DICH_TAC 1
THEN DICH_TAC(45-4)
THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT RESA_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN DICH_TAC 0
THEN DICH_TAC 0
THEN REAL_ARITH_TAC;





MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (SUC (SUC i))`;`v`;`SUC (SUC i)`;`k`]
THEN MRESA_TAC WL_IN_V[`SUC (SUC i)`;`v:num->real^3`]
THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (SUC (SUC i))`][GSYM ADD1]
THEN THAYTHE_TAC 0[`v (SUC i)`]
THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (SUC (SUC i))) (v (SUC (SUC (SUC i)))) (v (SUC i)) <= pi
==> azim (vec 0) (v (SUC (SUC i))) (v (SUC (SUC (SUC i)))) (v (SUC i)) = pi
\/ azim (vec 0) (v (SUC (SUC i))) (v (SUC (SUC (SUC i)))) ((v:num->real^3) (SUC i)) < pi`)
THEN RESA_TAC;



MRESA_TAC Imjxphr.EQ_W_L_IN_BBS[`s`;`k`;`v`;`SUC i`]
THEN SUBGOAL_THEN`dist ((v:num->real^3) (SUC (SUC (SUC i))),v (SUC (SUC i))) <
      scs_b_v39 s (SUC (SUC (SUC i))) (SUC (SUC i))` ASSUME_TAC;




DICH_TAC(49-43)
THEN STRIP_TAC
THEN SYM_ASSUM_TAC
THEN DICH_TAC(48-4)
THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
THEN REPEAT RESA_TAC
;


SUBGOAL_THEN`~collinear {vec 0, (v:num->real^3) (SUC (SUC (SUC i))), v ((SUC i))}`
ASSUME_TAC;


MRESAS_TAC WL_IN_V[`SUC (SUC (SUC i))`;`v:num->real^3`][BB_VV_FUN_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 1<k/\ 2<k/\ ~(3=1)`)
THEN RESA_TAC
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (SUC(SUC (SUC i)))`;`v (SUC i)`;`V`]
THEN THAYTHES_TAC 0[`v (SUC(SUC (SUC i)))`;`v (SUC i)`][SET_RULE`a IN {a,b}`;ADD1;BB_VV_FUN_EQ;ARITH_RULE`SUC (SUC (SUC x))=x+3`;Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
;


SUBGOAL_THEN`(v:num->real^3) (SUC (SUC i)) IN aff_gt {vec 0} {v (SUC (SUC (SUC i))), v (SUC i)}`
ASSUME_TAC;



MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 0<k/\ 1<k/\ 2<k /\ ~(3=2)/\ ~(2=1)`)
THEN RESA_TAC
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v ((SUC (SUC i)))`;`v (SUC i)`;`V`]
THEN THAYTHES_TAC 0[`v (SUC (SUC i))`;`v (SUC i)`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;ADD1;ARITH_RULE`(i+1)+1=i+2/\ (i+2)+1=i+3`;MOD_LT]
THEN MRESAL_TAC WL_IN_V[`SUC (SUC (SUC i))`;`v:num->real^3`][] 
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (SUC (SUC (SUC i)))`;`v (SUC (SUC i))`;`V`]
THEN THAYTHES_TAC 0[`(v:num->real^3) (SUC(SUC (SUC i)))`;`v (SUC (SUC i))`][SET_RULE`a IN {a,b}`;BB_VV_FUN_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;ADD1;ARITH_RULE`(i+1)+1=i+2/\ (i+2)+1=i+3`;MOD_LT]
THEN DICH_TAC (60-6)
THEN REWRITE_TAC[GSYM ADD1;generic]
THEN STRIP_TAC
THEN MRESAL_TAC WL_IN_E[`SUC (SUC i)`;`v:num->real^3`][] 
THEN THAYTHE_TAC 1[`v (SUC (SUC i))`;`v(SUC(SUC (SUC i)))`;`v (SUC i)`]
THEN MRESAS_TAC Polar_fan.GENERIC_LOCAL_FAN_STRAIGHT_AFF_GE[`v (SUC i)`;`v (SUC (SUC i))`;`v(SUC(SUC (SUC i)))`;][ARITH_RULE`SUC(SUC i)=i+2/\ SUC i= i+1/\ SUC(SUC(SUC i))=i+3`]
THEN DICH_TAC 0
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
THEN RESA_TAC
THEN DICH_TAC 0
THEN MRESA_TAC th3[`vec 0:real^3`;`v (SUC(SUC (SUC i)))`;`v (SUC i)`]
THEN MRESAS_TAC Local_lemmas.FAN_IMP_NOT_IN_AFF_GE[`E`;`V`;`v (SUC (SUC i))`;`vec 0:real^3`;`v (SUC i)`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`;BB_VV_FUN_EQ;ADD1;ARITH_RULE`SUC(SUC i)=i+2/\ SUC i= i+1/\ SUC(SUC(SUC i))=i+3`;Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
THEN MRESAS_TAC Local_lemmas.FAN_IMP_NOT_IN_AFF_GE[`E`;`V`;`v (SUC (SUC i))`;`vec 0:real^3`;`v (SUC(SUC (SUC i)))`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`;BB_VV_FUN_EQ;ADD1;ARITH_RULE`SUC(SUC i)=i+2/\ SUC i= i+1/\ SUC(SUC(SUC i))=i+3`;Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
THEN MRESAL_TAC Wrgcvdr_cizmrrh.AFF_GE_TO_AFF_GT2_GE1[`v (SUC i)`;`vec 0:real^3`;`(v:num->real^3) (SUC(SUC (SUC i)))`][UNION;IN_ELIM_THM;ARITH_RULE`SUC(SUC i)=i+2/\ SUC i= i+1/\ SUC(SUC(SUC i))=i+3`]
THEN REPEAT STRIP_TAC
THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
THEN ASM_REWRITE_TAC[]
;


MRESAS_TAC NUXCOEAv2[`s`;`k`;`v`;`SUC (SUC i)`;`SUC (SUC (SUC i))`][ARITH_RULE`SUC (SUC i) + k - 1=SUC (SUC i + k - 1)`]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN SYM_ASSUM_TAC
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC(SUC i)`;`SUC(SUC i+k-1)`;`s:scs_v39`;`SUC(SUC i)`;`SUC(SUC i+k-1) MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`;]
THEN ASM_SIMP_TAC[ARITH_RULE`3<k==> SUC (SUC i + k - 1) = 1*k+SUC i `;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC(SUC i)`;`SUC i MOD k`;`s:scs_v39`;`SUC(SUC i)`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`;]
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC
;




ONCE_REWRITE_TAC[DIST_SYM]
THEN MP_TAC(ARITH_RULE`3<k==> SUC i+k-1=SUC(i+k-1)`)
THEN RESA_TAC 
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`SUC (SUC i)+k-1`;`v:num->real^3`;`(SUC (SUC i)+k-1)MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`;ARITH_RULE`3<k==> SUC (SUC i) + k - 1 = 1*k+SUC i `;]
THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`(SUC i) MOD k`;`v:num->real^3`;`(SUC i)`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`;ARITH_RULE`3<k==> SUC (SUC i) + k - 1 = 1*k+SUC i `;]
;



MP_TAC Cuxvzoz.CJBDXXN
THEN RESA_TAC
THEN THAYTHES_TAC 0[`s`;`FF`;`k`;`SUC(SUC i)`;`v`][scs_generic;MOD_MULT_ADD;ARITH_RULE`3<k==> SUC (SUC i) + k - 1 = 1*k+SUC i `;]
THEN MATCH_DICH_TAC 0
THEN STRIP_TAC;



ASM_REWRITE_TAC[GSYM ADD1]
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN MRESA_TAC SCS_DIAG_2[`k`;`SUC i`]
THEN THAYTHE_TAC (52-12)[`SUC i`;`SUC(SUC(SUC i))`]
THEN DICH_TAC 1
THEN REWRITE_TAC[cstab]
THEN REAL_ARITH_TAC;


STRIP_TAC
;


ASM_SIMP_TAC[interior_angle1;GSYM ivs_rho_node1;ARITH_RULE`3<k==> SUC (SUC i) + k - 1 = 1*k+SUC i `;MOD_MULT_ADD;GSYM ADD1]
;


STRIP_TAC
;


ASM_SIMP_TAC[interior_angle1;GSYM ivs_rho_node1;ARITH_RULE`3<k==> SUC (SUC i) + k - 1 = 1*k+SUC i `;MOD_MULT_ADD;GSYM ADD1]
THEN MRESA_TAC Rrcwnsj.BB_F_SUC_PRE[`s`;`v`;`i`]
;



STRIP_TAC
;


MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC(SUC i)`;`(1*k+SUC i) `;`s:scs_v39`;`SUC(SUC i)`;`(1*k+SUC i)MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC(SUC i)`;`(SUC i)  MOD k`;`s:scs_v39`;`SUC(SUC i)`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`;MOD_MULT_ADD]
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC
;



STRIP_TAC
;



MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`SUC(SUC i)`;`(1*k+SUC i) `;`s:scs_v39`;`SUC(SUC i)`;`(1*k+SUC i)MOD k`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`;MOD_MULT_ADD]
THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`SUC(SUC i)`;`(SUC i)  MOD k`;`s:scs_v39`;`SUC(SUC i)`;`SUC i`][MOD_REFL;ARITH_RULE`3<k==> ~(k=0)`;MOD_MULT_ADD]
THEN ASM_TAC
THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
THEN REPEAT RESA_TAC
THEN REAL_ARITH_TAC;


REWRITE_TAC[GSYM ADD1]
THEN ONCE_REWRITE_TAC[DIST_SYM];

MRESAL_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC(SUC i)`][GSYM dist];


DICH_TAC (52-4)
THEN ASM_REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
THEN STRIP_TAC
THEN THAYTHE_TAC (71-68)[`SUC(SUC i)`]
THEN DICH_TAC(71-16)
THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF]
THEN STRIP_TAC
THEN THAYTHE_TAC 0[`SUC(SUC i)`;`SUC(SUC(SUC i))`]
THEN POP_ASSUM MP_TAC
THEN DICH_TAC 3
THEN REAL_ARITH_TAC;



]);;




let TFITSKC_concl = `
main_nonlinear_terminal_v11
==> (!s (v:num->real^3) i.
 scs_a_v39 s (i+2) (i+3)< scs_b_v39 s (i+2) (i+3) /\
3< scs_k_v39 s  /\
is_scs_v39 s /\ v IN MMs_v39 s /\ scs_generic v /\ scs_basic_v39 s /\
  scs_a_v39 s (i+1) (i+2) = &2 /\ scs_b_v39 s (i+1) (i+2) <= &2 * h0 /\
  dist(v i,v (i+1)) = &2 /\ &2< scs_b_v39 s i (i+1) /\
  (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab < dist(v i, v j)/\ &4 * h0 < scs_b_v39 s i j)) ==>
  dist(v (i+1),v(i+2)) = &2)`;;



let TFITSKC=prove( TFITSKC_concl,
STRIP_TAC
THEN REPEAT STRIP_TAC
THEN MP_TAC TFITSKCv1
THEN RESA_TAC
THEN POP_ASSUM MATCH_MP_TAC 
THEN EXISTS_TAC`s:scs_v39`
THEN ASM_REWRITE_TAC[ARITH_RULE`SUC(SUC i)=i+2/\ SUC i+2=i+3`]
THEN ASM_TAC
THEN REWRITE_TAC[scs_basic]
THEN REPEAT RESA_TAC);;



 end;;


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