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


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


module  Odxlstcv2 = 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;;





let ww_defor=new_definition`ww_defor w v t = if v= w then (&1-t) % w else v`;;
let FUN_WW_DEFOR=
prove(`ww_defor w v =(\t. if v= w then (&1-t) % w else v)`,

REWRITE_TAC[FUN_EQ_THM;ww_defor]);;

let WW_DEFOR_DEFORMATION=
prove_by_refinement(`&0<e1==>deformation (ww_defor (w:real^3)) V (-- e1,e1)`,

[
REWRITE_TAC[deformation;real_interval;IN_ELIM_THM;REAL_ARITH`(-- &1 < &0 /\ &0 < &1)`]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&0< e1==> -- e1< &0`)
THEN RESA_TAC
THEN STRIP_TAC;

REPEAT STRIP_TAC
THEN REWRITE_TAC[FUN_WW_DEFOR]
THEN MP_TAC(SET_RULE`v=w:real^3\/ ~(v=w)`)
THEN RESA_TAC;

REWRITE_TAC[continuous_atreal]
THEN REPEAT STRIP_TAC
THEN REWRITE_TAC[dist;VECTOR_ARITH`(&1 - x') % w - (&1 - r) % w = -- ((x' -r) %w)`;NORM_MUL;NORM_NEG]
THEN MRESA_TAC NORM_POS_LE[`w:real^3`]
THEN MP_TAC(REAL_ARITH`&0 <= norm (w:real^3)==>  norm w = &0\/ &0 < norm w`)
THEN RESA_TAC;

EXISTS_TAC`&1`
THEN ASM_REWRITE_TAC[REAL_ARITH`A * &0= &0/\ &0< &1`];

EXISTS_TAC`inv(norm (w:real^3)) * e/ &2`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(REAL_ARITH`&0<norm(w:real^3)==> ~(norm w= &0)`)
THEN RESA_TAC
THEN MRESA1_TAC NORM_EQ_0`w:real^3`
THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`w:real^3`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A`]
THEN MRESA_TAC REAL_LT_MUL[`inv(norm (w:real^3))`;`e:real`]
THEN MP_TAC(REAL_ARITH`&0< inv (norm (w:real^3)) * e==> &0< inv (norm w) * e/ &2`)
THEN RESA_TAC
THEN REPEAT STRIP_TAC
THEN MRESA_TAC REAL_LT_RMUL[`abs (x' - r)`;`inv (norm (w:real^3)) * e / &2`;`norm (w:real^3)`]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`(A*B/ &2) *C= (A*C) * B/ &2`]
THEN ASM_TAC
THEN REAL_ARITH_TAC;

REWRITE_TAC[continuous_atreal;DIST_REFL]
THEN REPEAT STRIP_TAC
THEN EXISTS_TAC`&1`
THEN ASM_REWRITE_TAC[REAL_ARITH`&0< &1`];

REPEAT STRIP_TAC
THEN REWRITE_TAC[ww_defor;VECTOR_ARITH`(&1 - &0) % w= w`]
THEN MP_TAC(SET_RULE`v=w:real^3\/ ~(v=w)`)
THEN RESA_TAC]);;







let DEFORMATION_IN_BALL_ANNULUS=
prove(
`  ~(&2 = norm (w:real^3)) /\ w IN ball_annulus
==> ?e.  &0< e/\ !t. &0 < t /\ t < e ==> (&1- t) %w IN ball_annulus`,

REWRITE_TAC[ball_annulus;cball;DIFF;ball;IN_ELIM_THM;dist; VECTOR_ARITH`vec 0 -A= --A`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b)<=> b<= a`]
THEN STRIP_TAC
THEN EXISTS_TAC`inv(norm w) * (norm (w:real^3) - &2)/ &2`
THEN MP_TAC(REAL_ARITH`&2<=norm(w:real^3)/\ ~(&2 = norm w)==> ~(norm w= &0)/\ norm w - &2< norm w/\ &0< norm w- &2`)
THEN RESA_TAC
THEN MRESA1_TAC NORM_EQ_0`w:real^3`
THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`w:real^3`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A`]
THEN MRESA_TAC REAL_LT_MUL[`inv(norm(w:real^3))`;`norm(w:real^3)- &2`]
THEN MP_TAC(REAL_ARITH`&0 < inv (norm w) * (norm w - &2)
==> &0 < inv (norm w) * (norm (w:real^3) - &2)/ &2`)
THEN RESA_TAC
THEN REPEAT STRIP_TAC
THEN MRESA_TAC REAL_LT_LMUL[`inv(norm (w:real^3))`;`(norm (w:real^3) - &2)`;`norm(w:real^3)`]
THEN MP_TAC(REAL_ARITH`&0< t/\t < inv (norm (w:real^3)) * (norm w - &2) / &2
/\ inv (norm w) * (norm w - &2) < &1
==> t< &1 /\ &0<= &1- t/\ &1 - t< &1/\ t < inv (norm (w:real^3)) * (norm w - &2)`)
THEN RESA_TAC
THEN MRESA1_TAC REAL_ABS_REFL`&1- t`
THENL[
MRESA_TAC REAL_LT_RMUL[`&1 -t`;`&1:real`;`norm(w:real^3)`]
THEN ASM_TAC
THEN REAL_ARITH_TAC;
REWRITE_TAC[REAL_ARITH`&2 <= (&1 - t) * norm w <=> t * norm w<= norm w - &2`]
THEN MRESA_TAC REAL_LT_RMUL[`t:real`;`inv(norm (w:real^3))*(norm (w:real^3) - &2)`;`norm(w:real^3)`]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`(inv (norm w) * (norm w - &2)) * norm w= 
(inv (norm w) * (norm w)) * (norm w - &2)`]
THEN REAL_ARITH_TAC]);;


let DEFORMATION_DIST_LE_A=
prove(`a< dist(w,v:real^3)
==> ?e. &0< e /\ (!t. &0< t /\ t< e==> a< dist ((&1-t)% w,v) )`,

REWRITE_TAC[dist;VECTOR_ARITH`(&1 - t) % w - v =(w-v) - t %w`]
THEN MRESA_TAC NORM_POS_LE[`w:real^3`]
THEN MP_TAC(REAL_ARITH`&0 <= norm (w:real^3) ==> norm w = &0 \/ (&0 < norm w/\ ~(norm w= &0))`)
THEN RESA_TAC
THENL[MRESA1_TAC NORM_EQ_0`w:real^3`
THEN REWRITE_TAC[VECTOR_ARITH`vec 0- v= -- v/\ vec 0 - v - t % vec 0 = -- v`]
THEN STRIP_TAC
THEN EXISTS_TAC`&1`
THEN ASM_REWRITE_TAC[REAL_ARITH`&0< &1`];
STRIP_TAC
THEN EXISTS_TAC`inv(norm (w:real^3)) * (norm (w-v)- a)/ &2`
THEN MRESA1_TAC NORM_EQ_0`w:real^3`
THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`w:real^3`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A`]
THEN MP_TAC(REAL_ARITH`a < norm (w - v) ==> &0< norm (w - v:real^3) - a`)
THEN RESA_TAC
THEN MRESA_TAC REAL_LT_MUL[`inv(norm(w:real^3))`;`norm(w:real^3 -v)- a`]
THEN MP_TAC(REAL_ARITH`&0 < inv (norm w) * (norm (w-v) - a) 
==> &0 < inv (norm w) * (norm (w:real^3-v) - a)/ &2`)
THEN RESA_TAC
THEN REPEAT STRIP_TAC
THEN MRESA_TAC REAL_LT_RMUL[`t:real`;`inv(norm (w:real^3))*(norm (w:real^3-v) - a)/ &2`;`norm(w:real^3)`]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`(inv (norm w) * (norm (w-v) - a)/ &2) * norm w= 
(inv (norm w) * (norm w)) * (norm (w- v) - a)/ &2/\ &1 *A=A`]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&0< t==> &0<= t`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`t * norm w < (norm (w - v) - a) / &2
/\ a< norm(w-v:real^3)
==> a< norm (w-v)- t* norm w`)
THEN ASM_REWRITE_TAC[]
THEN MRESA1_TAC REAL_ABS_REFL`t:real`
THEN MRESA_TAC NORM_MUL[`t:real`;`w:real^3`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC NORM_TRIANGLE[`w- v - t % w:real^3`;`t % w:real^3`][VECTOR_ARITH`w - v - t % w + t % w= w-v`]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC]);;


let DEFORMATION_DIST_LE_ALL=
prove(`is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<k/\ 
  (!i. ~(i MOD k = l MOD k) ==> scs_a_v39 s l i < dist(w l,w i)) 
==>
(!i. ~(i MOD k = l MOD k) ==> ?e. &0< e/\
(!t. &0< t/\ t< e  ==> scs_a_v39 s l i < dist((&1-t) %(w l),w i)))`,

REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MRESA_TAC th[`i:num`])
THEN MRESA_TAC(GEN_ALL DEFORMATION_DIST_LE_A)[`scs_a_v39 s l i`;`(w:num->real^3) l`;`(w:num->real^3) i`]);;



let DEFORMATION_DIST_LE_ALL_COM=
prove_by_refinement(`is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<k/\ 
  (!i. ~(i MOD k = l MOD k) ==> scs_a_v39 s l i < dist(w l,w i)) 
==>
 ?e. &0< e/\
(!t i. &0< t/\ t< e  /\ ~(i MOD k = l MOD k) ==> scs_a_v39 s l i < dist((&1-t) %(w l),w i))`,

[REPEAT STRIP_TAC
THEN MP_TAC DEFORMATION_DIST_LE_ALL
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[RIGHT_IMP_EXISTS_THM]
THEN REWRITE_TAC[SKOLEM_THM]
THEN STRIP_TAC
THEN ABBREV_TAC`e1= inf {(e:num->real) i|  i < k/\  ~(i= l MOD k)}`
THEN EXISTS_TAC`e1:real`
THEN SUBGOAL_THEN`FINITE {(e:num->real) i | i < k /\ ~(i = l MOD k)}`ASSUME_TAC;

MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`IMAGE (e:num->real) (0..k)`
THEN STRIP_TAC;

MATCH_MP_TAC FINITE_IMAGE
THEN REWRITE_TAC[FINITE_NUMSEG];

REWRITE_TAC[SUBSET;IMAGE;IN_ELIM_THM;IN_NUMSEG]
THEN REPEAT RESA_TAC
THEN EXISTS_TAC`i:num`
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;

SUBGOAL_THEN`~({(e:num->real) i | i < k /\ ~(i = l MOD k)} = {})`ASSUME_TAC;


REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;IN_ELIM_THM]
THEN MP_TAC(SET_RULE`l MOD k=0\/ ~(0=l MOD k )`)
THEN RESA_TAC;

EXISTS_TAC`(e:num->real)1`
THEN EXISTS_TAC`1`
THEN ASM_REWRITE_TAC[ARITH_RULE`~(1=0)`]
THEN MP_TAC(ARITH_RULE`3<k==> 1<k `)
THEN RESA_TAC;

EXISTS_TAC`(e:num->real)0`
THEN EXISTS_TAC`0`
THEN ASM_REWRITE_TAC[ARITH_RULE`~(1=0)`]
THEN MP_TAC(ARITH_RULE`3<k==> 0<k `)
THEN RESA_TAC;

STRIP_TAC;

MRESA_TAC REAL_LT_INF_FINITE[`{(e:num->real) i|  i < k/\  ~(i= l MOD k)}`;`&0`]
THEN REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT RESA_TAC
THEN MRESA_TAC MOD_LT[`i:num`;`k:num`]
THEN REPLICATE_TAC (13-5) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i:num`]);

REPEAT STRIP_TAC
THEN MRESA_TAC REAL_LT_INF_FINITE[`{(e:num->real) i|  i < k/\  ~(i= l MOD k)}`;`t:real`]
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`e (i MOD k) IN {(e:num->real) i | i < k /\ ~(i = l MOD k)}`ASSUME_TAC;

REWRITE_TAC[IN_ELIM_THM]
THEN EXISTS_TAC`i MOD k`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`i:num`;`k:num`];

STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA1_TAC th`(e:num->real) (i MOD k)`)
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC MOD_REFL[`i:num`;`k:num`]
THEN REPLICATE_TAC (15-5) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i:num MOD k`])
THEN POP_ASSUM(fun th-> MRESA1_TAC th`t:real`)
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s l`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])]);;



let DEFORMATION_DIST_LE_B=
prove(
` dist(w,v:real^3) < a
==> ?e. &0< e /\ (!t. &0< t /\ t< e==>  dist ((&1-t)% w,v) <a)`,

REWRITE_TAC[dist;VECTOR_ARITH`(&1 - t) % w - v =(w-v) - t %w`]
THEN MRESA_TAC NORM_POS_LE[`w:real^3`]
THEN MP_TAC(REAL_ARITH`&0 <= norm (w:real^3) ==> norm w = &0 \/ (&0 < norm w/\ ~(norm w= &0))`)
THEN RESA_TAC
THENL[
MRESA1_TAC NORM_EQ_0`w:real^3`
THEN REWRITE_TAC[VECTOR_ARITH`vec 0- v= -- v/\ vec 0 - v - t % vec 0 = -- v`]
THEN STRIP_TAC
THEN EXISTS_TAC`&1`
THEN ASM_REWRITE_TAC[REAL_ARITH`&0< &1`];
STRIP_TAC
THEN EXISTS_TAC`inv(norm (w:real^3)) * (a- norm (w-v))/ &2`
THEN MRESA1_TAC NORM_EQ_0`w:real^3`
THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`w:real^3`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A`]
THEN MP_TAC(REAL_ARITH`norm (w - v) < a ==> &0<a- norm (w - v:real^3)`)
THEN RESA_TAC
THEN MRESA_TAC REAL_LT_MUL[`inv(norm(w:real^3))`;`a- norm(w:real^3 -v)`]
THEN MP_TAC(REAL_ARITH`&0 < inv (norm w) * (a- norm (w-v)) 
==> &0 < inv (norm w) * (a- norm (w:real^3-v) )/ &2`)
THEN RESA_TAC
THEN REPEAT STRIP_TAC
THEN MRESA_TAC REAL_LT_RMUL[`t:real`;`inv(norm (w:real^3))*(a-norm (w:real^3-v) )/ &2`;`norm(w:real^3)`]
THEN POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`(inv (norm w) * (a-norm (w-v))/ &2) * norm w= 
(inv (norm w) * (norm w)) * (a-norm (w- v))/ &2/\ &1 *A=A`]
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&0< t==> &0<= t`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`t * norm w < (a-norm (w - v)) / &2
/\  norm(w-v:real^3)<a
==> norm (w-v)+ t* norm w<a`)
THEN ASM_REWRITE_TAC[]
THEN MRESA1_TAC REAL_ABS_REFL`t:real`
THEN MRESA_TAC NORM_MUL[`t:real`;`w:real^3`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN MRESAL_TAC NORM_TRIANGLE[`w- v :real^3`;`-- (t % w):real^3`][VECTOR_ARITH`w - v + --(t%w)= w-v - t %w`;NORM_NEG]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC]);;





let DEFORMATION_DIST_LE_BLL=
prove_by_refinement(`is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<k/\ 
  (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i) 
==>
(!i. scs_diag k l i ==> ?e. &0< e/\
(!t. &0< t/\ t< e  ==> dist((&1-t) %(w l),w i)<scs_b_v39 s l i ) )`,

[
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MRESA_TAC th[`i:num`])
THEN SUBGOAL_THEN`dist((w:num->real^3) l,w i)< scs_b_v39 s l i`ASSUME_TAC;

MRESAL_TAC DIST_TRIANGLE[`(w:num->real^3) l`;`vec 0:real^3`;`(w:num->real^3) i`][]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;IMAGE;IN_ELIM_THM;SUBSET;ball_annulus;DIFF;cball]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) l = w x) `ASSUME_TAC;

EXISTS_TAC `l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];


SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) i = w x) `ASSUME_TAC;

EXISTS_TAC `i:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

REPLICATE_TAC (36-20) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN REPLICATE_TAC (2) (POP_ASSUM MP_TAC)
THEN MRESA_TAC th[`(w:num->real^3) i`]
THEN MRESA_TAC th[`(w:num->real^3) l`])
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[dist;VECTOR_ARITH`a- vec 0= a/\ vec 0 - a= --a`;NORM_NEG]
THEN REAL_ARITH_TAC;


EXISTS_TAC `l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) i = w x) `ASSUME_TAC;

EXISTS_TAC `i:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

REPLICATE_TAC (36-20) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN REPLICATE_TAC (2) (POP_ASSUM MP_TAC)
THEN MRESA_TAC th[`(w:num->real^3) i`]
THEN MRESA_TAC th[`(w:num->real^3) l`])
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[dist;VECTOR_ARITH`a- vec 0= a/\ vec 0 - a= --a`;NORM_NEG]
THEN REAL_ARITH_TAC;

MRESA_TAC(GEN_ALL DEFORMATION_DIST_LE_B)[`(w:num->real^3) l`;`(w:num->real^3) i`;`scs_b_v39 s l i`;]]);;







let DEFORMATION_DIST_LE_BLL_EDGE=
prove_by_refinement(`is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<k
==>(!i. l MOD k= SUC i MOD k 
==>
?e. &0< e/\
(!t. &0< t/\ t< e  ==> dist((&1-t) %(w l),w i)<scs_b_v39 s l i )) `,

[
REPEAT STRIP_TAC
THEN REWRITE_TAC[dist;VECTOR_ARITH`(&1 - t) % w - w1  = --(t % w-(w-w1))`;NORM_NEG]
THEN SUBGOAL_THEN`((w:num->real^3) l- w i) dot -- (w:num->real^3) l< &0` ASSUME_TAC;

MRESAL_TAC DOT_NORM[`(w:num->real^3) l- w i`;`-- (w:num->real^3) l`][VECTOR_ARITH`wl - wi + (-- wl)= --wi:real^3`;NORM_NEG]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;IMAGE;SUBSET;IN_ELIM_THM;ball_annulus;cball;DIFF;ball]
THEN REPEAT RESA_TAC
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) l = w x) `ASSUME_TAC;

EXISTS_TAC `l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) i = w x) `ASSUME_TAC;

EXISTS_TAC `i:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

REPLICATE_TAC (37-20) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`(w:num->real^3) i`]
THEN MRESA_TAC th[`(w:num->real^3) l`])
THEN REPLICATE_TAC (4) (POP_ASSUM MP_TAC)
THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (40-21) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num`;`i:num`][dist])
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 1< k`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`SUC i`;`k:num`]
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MP_TAC Qknvmlb.SUC_MOD_NOT_EQ
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
THEN REPLICATE_TAC (48-14) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num MOD k`;`i MOD k:num`][dist])
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s l`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&2 <= scs_a_v39 s i l
/\ scs_a_v39 s i l <= norm (w l - (w:num->real^3)i)/\ ~(norm (w l) < &2)
==> &2<= norm (w l - (w:num->real^3)i) /\ &2<= norm (w l)`)
THEN RESA_TAC
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`&2`;`norm ((w:num->real^3) l)`][ARITH_RULE`abs (&2)= &2`;REAL_ABS_NORM]
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`&2`;`norm (w l - (w:num->real^3)i)`][ARITH_RULE`abs (&2)= &2`;REAL_ABS_NORM]
THEN ASM_TAC
THEN REWRITE_TAC[h0]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`norm ((w:num->real^3) i)`;`&2* h0`;][ARITH_RULE`abs (&2 * #1.26)= &2 * #1.26`;REAL_ABS_NORM;h0]
THEN REPLICATE_TAC (3) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;

EXISTS_TAC `l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) i = w x) `ASSUME_TAC;

EXISTS_TAC `i:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

REPLICATE_TAC (37-20) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`(w:num->real^3) i`]
THEN MRESA_TAC th[`(w:num->real^3) l`])
THEN REPLICATE_TAC (4) (POP_ASSUM MP_TAC)
THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (40-21) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num`;`i:num`][dist])
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 1< k`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`SUC i`;`k:num`]
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MP_TAC Qknvmlb.SUC_MOD_NOT_EQ
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
THEN REPLICATE_TAC (48-14) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num MOD k`;`i MOD k:num`][dist])
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s l`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&2 <= scs_a_v39 s i l
/\ scs_a_v39 s i l <= norm (w l - (w:num->real^3)i)/\ ~(norm (w l) < &2)
==> &2<= norm (w l - (w:num->real^3)i) /\ &2<= norm (w l)`)
THEN RESA_TAC
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`&2`;`norm ((w:num->real^3) l)`][ARITH_RULE`abs (&2)= &2`;REAL_ABS_NORM]
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`&2`;`norm (w l - (w:num->real^3)i)`][ARITH_RULE`abs (&2)= &2`;REAL_ABS_NORM]
THEN ASM_TAC
THEN REWRITE_TAC[h0]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`norm ((w:num->real^3) i)`;`&2* h0`;][ARITH_RULE`abs (&2 * #1.26)= &2 * #1.26`;REAL_ABS_NORM;h0]
THEN REPLICATE_TAC (3) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;


POP_ASSUM MP_TAC
THEN REWRITE_TAC[DOT_RNEG;REAL_ARITH`-- a< &0 <=> a> &0`]
THEN STRIP_TAC
THEN MRESA_TAC CLOSER_POINTS_LEMMA[`(w:num->real^3) l- w i`;`(w:num->real^3) l`]
THEN EXISTS_TAC `u:real`
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC(REAL_ARITH`t< u==> t<= u`)
THEN RESA_TAC
THEN MRESA_TAC th[`t:real`])
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;IMAGE;SUBSET;IN_ELIM_THM;ball_annulus;cball;DIFF;ball]
THEN REPEAT RESA_TAC
THEN REPLICATE_TAC (40-22) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num`;`i:num`][dist])
THEN REPLICATE_TAC (3) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC]);;






let DEFORMATION_DIST_LE_BLL_EDGE2=
prove_by_refinement(
`is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<k
==>(!i.  i MOD k= SUC l MOD k 
==>
?e. &0< e/\
(!t. &0< t/\ t< e  ==> dist((&1-t) %(w l),w i)<scs_b_v39 s l i ) )`,

[
REPEAT STRIP_TAC
THEN REWRITE_TAC[dist;VECTOR_ARITH`(&1 - t) % w - w1  = --(t % w-(w-w1))`;NORM_NEG]
THEN SUBGOAL_THEN`((w:num->real^3) l- w i) dot -- (w:num->real^3) l< &0` ASSUME_TAC;

MRESAL_TAC DOT_NORM[`(w:num->real^3) l- w i`;`-- (w:num->real^3) l`][VECTOR_ARITH`wl - wi + (-- wl)= --wi:real^3`;NORM_NEG]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;IMAGE;SUBSET;IN_ELIM_THM;ball_annulus;cball;DIFF;ball]
THEN REPEAT RESA_TAC
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) l = w x) `ASSUME_TAC;

EXISTS_TAC `l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) i = w x) `ASSUME_TAC;

EXISTS_TAC `i:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

REPLICATE_TAC (37-20) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`(w:num->real^3) i`]
THEN MRESA_TAC th[`(w:num->real^3) l`])
THEN REPLICATE_TAC (4) (POP_ASSUM MP_TAC)
THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (40-21) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num`;`i:num`][dist])
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 1< k`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`l:num`;`k:num`]
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MP_TAC Qknvmlb.SUC_MOD_NOT_EQ
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`l:num`)
THEN REPLICATE_TAC (48-14) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num MOD k`;`i MOD k:num`][dist])
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s l`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&2 <= scs_a_v39 s i l
/\ scs_a_v39 s i l <= norm (w l - (w:num->real^3)i)/\ ~(norm (w l) < &2)
==> &2<= norm (w l - (w:num->real^3)i) /\ &2<= norm (w l)`)
THEN RESA_TAC
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`&2`;`norm ((w:num->real^3) l)`][ARITH_RULE`abs (&2)= &2`;REAL_ABS_NORM]
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`&2`;`norm (w l - (w:num->real^3)i)`][ARITH_RULE`abs (&2)= &2`;REAL_ABS_NORM]
THEN ASM_TAC
THEN REWRITE_TAC[h0]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`norm ((w:num->real^3) i)`;`&2* h0`;][ARITH_RULE`abs (&2 * #1.26)= &2 * #1.26`;REAL_ABS_NORM;h0]
THEN REPLICATE_TAC (3) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;


EXISTS_TAC `l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) i = w x) `ASSUME_TAC;

EXISTS_TAC `i:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

REPLICATE_TAC (37-20) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`(w:num->real^3) i`]
THEN MRESA_TAC th[`(w:num->real^3) l`])
THEN REPLICATE_TAC (4) (POP_ASSUM MP_TAC)
THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (40-21) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num`;`i:num`][dist])
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)/\ 1< k`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`l:num`;`k:num`]
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MP_TAC Qknvmlb.SUC_MOD_NOT_EQ
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`l:num`)
THEN REPLICATE_TAC (48-14) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num MOD k`;`i MOD k:num`][dist])
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s l`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&2 <= scs_a_v39 s i l
/\ scs_a_v39 s i l <= norm (w l - (w:num->real^3)i)/\ ~(norm (w l) < &2)
==> &2<= norm (w l - (w:num->real^3)i) /\ &2<= norm (w l)`)
THEN RESA_TAC
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`&2`;`norm ((w:num->real^3) l)`][ARITH_RULE`abs (&2)= &2`;REAL_ABS_NORM]
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`&2`;`norm (w l - (w:num->real^3)i)`][ARITH_RULE`abs (&2)= &2`;REAL_ABS_NORM]
THEN ASM_TAC
THEN REWRITE_TAC[h0]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`norm ((w:num->real^3) i)`;`&2* h0`;][ARITH_RULE`abs (&2 * #1.26)= &2 * #1.26`;REAL_ABS_NORM;h0]
THEN REPLICATE_TAC (3) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[DOT_RNEG;REAL_ARITH`-- a< &0 <=> a> &0`]
THEN STRIP_TAC
THEN MRESA_TAC CLOSER_POINTS_LEMMA[`(w:num->real^3) l- w i`;`(w:num->real^3) l`]
THEN EXISTS_TAC `u:real`
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC(REAL_ARITH`t< u==> t<= u`)
THEN RESA_TAC
THEN MRESA_TAC th[`t:real`])
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;IMAGE;SUBSET;IN_ELIM_THM;ball_annulus;cball;DIFF;ball]
THEN REPEAT RESA_TAC
THEN REPLICATE_TAC (40-22) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num`;`i:num`][dist])
THEN REPLICATE_TAC (3) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC]);;


let DEFORMATION_DIST_LE_BLL_PRIME=
prove_by_refinement(`is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<k/\ 
  (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i) 
==>
(!i. ~(i MOD k = l MOD k) ==> ?e. &0< e/\
(!t. &0< t/\ t< e  ==> dist((&1-t) %(w l),w i)<scs_b_v39 s l i ) )`,

[
REPEAT STRIP_TAC
THEN MP_TAC(SET_RULE`l MOD k = SUC i MOD k \/ ~(SUC i MOD k= l MOD k)`)
THEN RESA_TAC;

MP_TAC DEFORMATION_DIST_LE_BLL_EDGE
THEN RESA_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_REWRITE_TAC[];

MP_TAC(SET_RULE`i MOD k= SUC l MOD k  \/ ~(i MOD k= SUC l MOD k )`)
THEN RESA_TAC;

MP_TAC DEFORMATION_DIST_LE_BLL_EDGE2
THEN RESA_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_REWRITE_TAC[];

MP_TAC DEFORMATION_DIST_LE_BLL
THEN RESA_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_REWRITE_TAC[scs_diag]]);;


let DEFORMATION_DIST_LE_BLL_COM=
prove_by_refinement(`is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<k/\ 
  (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i) 
==>
 ?e. &0< e/\
(!t i. &0< t/\ t< e  /\ ~(i MOD k = l MOD k) ==> dist((&1-t) %(w l),w i)< scs_b_v39 s l i) `,

[REPEAT STRIP_TAC
THEN MP_TAC DEFORMATION_DIST_LE_BLL_PRIME
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[RIGHT_IMP_EXISTS_THM]
THEN REWRITE_TAC[SKOLEM_THM]
THEN STRIP_TAC
THEN ABBREV_TAC`e1= inf {(e:num->real) i|  i < k/\  ~(i= l MOD k)}`
THEN EXISTS_TAC`e1:real`
THEN SUBGOAL_THEN`FINITE {(e:num->real) i | i < k /\ ~(i = l MOD k)}`ASSUME_TAC;


MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`IMAGE (e:num->real) (0..k)`
THEN STRIP_TAC;

MATCH_MP_TAC FINITE_IMAGE
THEN REWRITE_TAC[FINITE_NUMSEG];

REWRITE_TAC[SUBSET;IMAGE;IN_ELIM_THM;IN_NUMSEG]
THEN REPEAT RESA_TAC
THEN EXISTS_TAC`i:num`
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;

SUBGOAL_THEN`~({(e:num->real) i | i < k /\ ~(i = l MOD k)} = {})`ASSUME_TAC;

REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;IN_ELIM_THM]
THEN MP_TAC(SET_RULE`l MOD k=0\/ ~(0=l MOD k )`)
THEN RESA_TAC;


EXISTS_TAC`(e:num->real)1`
THEN EXISTS_TAC`1`
THEN ASM_REWRITE_TAC[ARITH_RULE`~(1=0)`]
THEN MP_TAC(ARITH_RULE`3<k==> 1<k `)
THEN RESA_TAC;


EXISTS_TAC`(e:num->real)0`
THEN EXISTS_TAC`0`
THEN ASM_REWRITE_TAC[ARITH_RULE`~(1=0)`]
THEN MP_TAC(ARITH_RULE`3<k==> 0<k `)
THEN RESA_TAC;


STRIP_TAC;

MRESA_TAC REAL_LT_INF_FINITE[`{(e:num->real) i|  i < k/\  ~(i= l MOD k)}`;`&0`]
THEN REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT RESA_TAC
THEN MRESA_TAC MOD_LT[`i:num`;`k:num`]
THEN REPLICATE_TAC (13-5) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i:num`]);

REPEAT STRIP_TAC
THEN MRESA_TAC REAL_LT_INF_FINITE[`{(e:num->real) i|  i < k/\  ~(i= l MOD k)}`;`t:real`]
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`e (i MOD k) IN {(e:num->real) i | i < k /\ ~(i = l MOD k)}`ASSUME_TAC;

REWRITE_TAC[IN_ELIM_THM]
THEN EXISTS_TAC`i MOD k`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`i:num`;`k:num`];

STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA1_TAC th`(e:num->real) (i MOD k)`)
THEN MP_TAC(ARITH_RULE`3<k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC MOD_REFL[`i:num`;`k:num`]
THEN REPLICATE_TAC (15-5) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i:num MOD k`])
THEN POP_ASSUM(fun th-> MRESA1_TAC th`t:real`)
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s l`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])]);;


let IMAGE_WW_DEFOR=
prove_by_refinement(`!w:num->real^3.
 IMAGE (\i. ww_defor (w l) (w i) t) (:num)= ((IMAGE w (:num)) DIFF {w l}) UNION {ww_defor (w l) (w l) t}`,

[
REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;DIFF;UNION;EXTENSION;IN_SING]
THEN GEN_TAC
THEN EQ_TAC;

RESA_TAC
THEN REWRITE_TAC[ww_defor]
THEN MP_TAC(SET_RULE`(w:num->real^3) l= w x' \/ ~((w:num->real^3) l= w x' )`)
THEN RESA_TAC;

MATCH_MP_TAC(SET_RULE`A==> A\/B`)
THEN EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num) IN (:num)`];

REPEAT RESA_TAC
THEN REWRITE_TAC[ww_defor];

EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num) IN (:num)`]
THEN POP_ASSUM MP_TAC
THEN RESA_TAC;

EXISTS_TAC`l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num) IN (:num)`]]);;



let WW_DEFOR_FF1=
prove_by_refinement(`(!x. x IN FF==> ~(FST x= SND x)/\ ~((&1 - t) % v = FST x)/\ ~((&1 - t) % v = SND x))
==>(!w.
ww_defor (v:real^3) v t,(w:real^3) IN
      IMAGE (\uv. ww_defor v (FST uv) t,ww_defor v (SND uv) t) FF
<=> v,w IN FF)`,

[REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;ww_defor]
THEN EQ_TAC;

RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN MP_TAC(SET_RULE`v=FST (x:real^3#real^3)\/ ~(FST x = v:real^3)`)
THEN RESA_TAC
THEN REPLICATE_TAC (2) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> STRIP_TAC THEN STRIP_TAC
THEN MRESA_TAC th[`x:real^3#real^3`])
THEN RESA_TAC;

RESA_TAC
THEN EXISTS_TAC`v:real^3,w:real^3`
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MRESA1_TAC th`v:real^3,w:real^3`)]);;



let WW_DEFOR_rho_node1=
prove(`(!x. x IN FF==> ~(FST x= SND x)/\ ~((&1 - t) % v = FST x) /\ ~((&1 - t) % v = SND x))
==>(rho_node1 (IMAGE (\uv. ww_defor v (FST uv) t,ww_defor v (SND uv) t) FF) (ww_defor (v:real^3) v t)= rho_node1 FF v)`,

STRIP_TAC
THEN REWRITE_TAC[rho_node1]
THEN MP_TAC WW_DEFOR_FF1
THEN RESA_TAC);;



let WW_DEFOR_FF2=
prove_by_refinement(
`(!x. x IN FF==> ~(FST x= SND x)/\ ~((&1 - t) % v = FST x)/\ ~((&1 - t) % v = SND x))
==>(!w.
(w:real^3),ww_defor (v:real^3) v t IN
      IMAGE (\uv. ww_defor v (FST uv) t,ww_defor v (SND uv) t) FF
<=> w,v IN FF)`,

[REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;ww_defor]
THEN EQ_TAC;

RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN MP_TAC(SET_RULE`v=SND (x:real^3#real^3)\/ ~(SND x = v:real^3)`)
THEN RESA_TAC
THEN REPLICATE_TAC (2) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> STRIP_TAC THEN STRIP_TAC
THEN MRESA_TAC th[`x:real^3#real^3`])
THEN RESA_TAC;

RESA_TAC
THEN EXISTS_TAC`w:real^3,v:real^3`
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MRESA1_TAC th`w:real^3,v:real^3`)]);;



let WW_DEFOR_APHA=
prove(`(!x. x IN FF==> ~(FST x= SND x)/\ ~((&1 - t) % v = FST x)/\ ~((&1 - t) % v = SND x))
==>(@w.
(w:real^3),ww_defor (v:real^3) v t IN
      IMAGE (\uv. ww_defor v (FST uv) t,ww_defor v (SND uv) t) FF)
= (@w. w,v IN FF)`,

STRIP_TAC
THEN MP_TAC WW_DEFOR_FF2
THEN RESA_TAC);;



let WW_DEFOR_AZIM=
prove(`(!x. x IN FF==> ~(FST x= SND x)/\ ~((&1 - t) % v = FST x)/\ ~((&1 - t) % v = SND x))/\ t< &1
==>
azim (vec 0) (ww_defor v v t)
 (rho_node1 (IMAGE (\uv. ww_defor v (FST uv) t,ww_defor v (SND uv) t) FF)
 (ww_defor v v t))
 (@a. a,ww_defor v v t IN
      IMAGE (\uv. ww_defor v (FST uv) t,ww_defor v (SND uv) t) FF)
=azim (vec 0) v (rho_node1 FF v) (@a. a,v IN FF)`,

REPEAT STRIP_TAC
THEN MP_TAC(REAL_ARITH`t< &1==> &0< &1-t`)
THEN RESA_TAC
THEN MP_TAC WW_DEFOR_APHA
THEN RESA_TAC
THEN MP_TAC WW_DEFOR_rho_node1
THEN RESA_TAC
THEN REWRITE_TAC[ww_defor]
THEN ASM_SIMP_TAC[AZIM_SPECIAL_SCALE]);;

let GENERIC_HYPOTHESIS_WW_DEFOR=
prove_by_refinement(` local_fan(V,E,FF)/\ ~(t= &0)/\ v IN V /\ generic V E
==>
(!x. x IN FF==> ~(FST x= SND x)/\ ~((&1 - t) % v = FST x)/\ ~((&1 - t) % v = SND x))`,

[REPEAT STRIP_TAC;

MP_TAC Local_lemmas.LOCAL_FAN_IN_FF_DISTINCT
THEN RESA_TAC;

POP_ASSUM MP_TAC
THEN MP_TAC Local_lemmas.LOFA_IMP_V_DIFF
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`v:real^3`])
THEN MP_TAC(SET_RULE`FST x = v\/ ~(FST (x:real^3#real^3)=v)`)
THEN RESA_TAC;

REWRITE_TAC[VECTOR_ARITH`(&1 - t) % v = v<=> t %v= vec 0`;VECTOR_MUL_EQ_0]
THEN ASM_REWRITE_TAC[];


MP_TAC Local_lemmas.LOCAL_FAN_IMP_IN_V2
THEN RESA_TAC
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`]
THEN POP_ASSUM (fun th-> MRESA_TAC th[`FST (x:real^3#real^3)`])
THEN MRESAL_TAC th3[`vec 0:real^3`;`v:real^3`;`FST (x:real^3#real^3)`][Trigonometry2.AFF2;IN_ELIM_THM;VECTOR_ARITH`A % vec 0+B= B`]
THEN POP_ASSUM (fun th->
STRIP_TAC
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`t:real`
THEN ASM_REWRITE_TAC[];

POP_ASSUM MP_TAC
THEN MP_TAC Local_lemmas.LOFA_IMP_V_DIFF
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`v:real^3`])
THEN MP_TAC(SET_RULE`SND x = v\/ ~(SND (x:real^3#real^3)=v)`)
THEN RESA_TAC;

REWRITE_TAC[VECTOR_ARITH`(&1 - t) % v = v<=> t %v= vec 0`;VECTOR_MUL_EQ_0]
THEN ASM_REWRITE_TAC[];

MP_TAC Local_lemmas.LOCAL_FAN_IMP_IN_V2
THEN RESA_TAC
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`]
THEN POP_ASSUM (fun th-> MRESA_TAC th[`SND (x:real^3#real^3)`])
THEN MRESAL_TAC th3[`vec 0:real^3`;`v:real^3`;`SND (x:real^3#real^3)`][Trigonometry2.AFF2;IN_ELIM_THM;VECTOR_ARITH`A % vec 0+B= B`]
THEN POP_ASSUM (fun th->
STRIP_TAC
THEN MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`t:real`
THEN ASM_REWRITE_TAC[]]);;






let WW_DEFOR_0_ID=
prove(`ww_defor v w (&0)= w:real^3`,

REWRITE_TAC[ww_defor;VECTOR_ARITH`(&1- &0) %v= v`]
THEN MP_TAC(SET_RULE`~(v=w:real^3)\/ v=w`)
THEN RESA_TAC);;
let AZIM_0_WW_DEFOR=
prove(`t= &0
==>
azim (vec 0) (ww_defor v v t)
 (rho_node1 (IMAGE (\uv. ww_defor v (FST uv) t,ww_defor v (SND uv) t) FF)
 (ww_defor v v t))
 (@a. a,ww_defor v v t IN
      IMAGE (\uv. ww_defor v (FST uv) t,ww_defor v (SND uv) t) FF)
=azim (vec 0) v (rho_node1 FF v) (@a. a,v IN FF)`,

RESA_TAC
THEN REWRITE_TAC[WW_DEFOR_0_ID;IMAGE_ID]);;



let GENEIRC_WW_DEFOR_AZIM=
prove(`local_fan(V,E,FF)/\  v IN V /\ generic V E /\ t< &1
==>
azim (vec 0) (ww_defor v v t)
 (rho_node1 (IMAGE (\uv. ww_defor v (FST uv) t,ww_defor v (SND uv) t) FF)
 (ww_defor v v t))
 (@a. a,ww_defor v v t IN
      IMAGE (\uv. ww_defor v (FST uv) t,ww_defor v (SND uv) t) FF)
=azim (vec 0) v (rho_node1 FF v) (@a. a,v IN FF)`,

STRIP_TAC
THEN MP_TAC(SET_RULE`t= &0\/ ~(t= &0)`)
THEN RESA_TAC
THENL[
ASM_REWRITE_TAC[WW_DEFOR_0_ID;IMAGE_ID];

MP_TAC GENERIC_HYPOTHESIS_WW_DEFOR
THEN RESA_TAC
THEN MP_TAC WW_DEFOR_AZIM
THEN RESA_TAC
]);;



let WW_DEFOR_FF3=
prove_by_refinement(
`(!x. x IN FF==> ~(FST x= SND x)/\ ~((&1 - t) % w1 = FST x)/\ ~((&1 - t) % w1 = SND x)) /\ w1,v IN FF /\ ~(v,w1 IN FF)/\ ~(t= &0)
==>(!w.
ww_defor (w1:real^3) v t,(w:real^3) IN
      IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF
<=> v,w IN FF)`,


[

REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;ww_defor]
THEN REPLICATE_TAC (3) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`w1:real^3,v:real^3`
THEN ASSUME_TAC th)
THEN EQ_TAC;

RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN MP_TAC(SET_RULE`FST (x:real^3#real^3)=w1\/ ~(FST x = w1:real^3)`)
THEN RESA_TAC;

REPLICATE_TAC (2) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPLICATE_TAC (2)  STRIP_TAC
THEN MRESA_TAC th[`x:real^3#real^3`])
THEN RESA_TAC
THEN MP_TAC(SET_RULE`w1= SND (x:real^3#real^3)\/ ~(SND x = w1:real^3)`)
THEN RESA_TAC;

SUBGOAL_THEN`v,w1 IN (FF:real^3#real^3->bool)` ASSUME_TAC;

ASM_TAC
THEN STRIP_TAC
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN REPEAT RESA_TAC;

POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[];

STRIP_TAC
THEN EXISTS_TAC`v:real^3,w:real^3`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC (1) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPLICATE_TAC (1)  STRIP_TAC
THEN MRESA1_TAC th`v:real^3,w:real^3`)
THEN ASM_TAC
THEN MP_TAC(SET_RULE`(w=w1:real^3)\/ ~(w=w1)`)
THEN REPEAT RESA_TAC]);;


let WW_DEFOR_RHO_NODE1=
prove(`(!x. x IN FF==> ~(FST x= SND x)/\ ~((&1 - t) % w1 = FST x)/\ ~((&1 - t) % w1 = SND x)) /\ w1,v IN FF /\ ~(v,w1 IN FF)/\ ~(t= &0)
==> rho_node1(
      IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF) (ww_defor (w1:real^3) v t)
= rho_node1 FF v`,

STRIP_TAC
THEN REWRITE_TAC[rho_node1]
THEN MP_TAC WW_DEFOR_FF3
THEN RESA_TAC);;


let GENERIC_WW_DEFOR_RHO_NODE1=
prove(`local_fan(V,E,FF)/\ generic V E  /\ w1,v IN FF /\ ~(t= &0)
==> rho_node1(
      IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF) (ww_defor (w1:real^3) v t)
= rho_node1 FF v`,

RESA_TAC
THEN MATCH_MP_TAC WW_DEFOR_RHO_NODE1
THEN ASM_REWRITE_TAC[]
THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V2)[`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`w1:real^3,v:real^3`;`V:real^3->bool`;]
THEN MRESA_TAC(GEN_ALL GENERIC_HYPOTHESIS_WW_DEFOR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`t:real`;`w1:real^3`]
THEN STRIP_TAC
THEN MRESA_TAC (GEN_ALL Local_lemmas.IVS_RHO_NODE1_DETE)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`v:real^3`;`w1:real^3`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.DETER_RHO_NODE)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`v:real^3`;`w1:real^3`]
THEN MRESAL_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`v:real^3`][SET_RULE`{a,a}={a}`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.DETER_RHO_NODE)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`w1:real^3`;`v:real^3`]
THEN MRESAL_TAC(GEN_ALL Local_lemmas.LOFA_CARD_EE_V_2)[`V:real^3->bool`;`(FF:real^3#real^3->bool)`;`w1:real^3`;`v:real^3`;`E:(real^3->bool)->bool`][Geomdetail.CARD_SING;ARITH_RULE`~(1=2)`]);;


let WW_DEFOR_ALPHA3=
prove_by_refinement(
`local_fan(V,E,FF)/\ generic V E  /\ w1,v IN FF /\ ~(t= &0)
==>(@w.
(w:real^3),ww_defor (w1:real^3) v t IN
      IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF)
= (&1-t) %w1`,

[
REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;ww_defor]
THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V2)[`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`w1:real^3,v:real^3`;`V:real^3->bool`;]
THEN MRESA_TAC(GEN_ALL GENERIC_HYPOTHESIS_WW_DEFOR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`t:real`;`w1:real^3`]
THEN MATCH_MP_TAC Hypermap_and_fan.CHOICE_LEMMA
THEN STRIP_TAC;

EXISTS_TAC`(&1-t)%w1:real^3`THEN EXISTS_TAC`w1:real^3,v:real^3`
THEN ASM_REWRITE_TAC[];

REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN MP_TAC(SET_RULE`(FST (x:real^3#real^3)=w1)\/ ~((FST (x:real^3#real^3)=w1))`)
THEN RESA_TAC;

RESA_TAC;

REPLICATE_TAC (2) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPLICATE_TAC (2)  STRIP_TAC
THEN MRESA_TAC th[`(w1,v):real^3#real^3`])
THEN MP_TAC(SET_RULE`(SND (x:real^3#real^3)=w1)\/ ~((SND (x:real^3#real^3)=w1))`)
THEN RESA_TAC;

STRIP_TAC
THEN SUBGOAL_THEN`w,v IN (FF:real^3#real^3->bool)` ASSUME_TAC;

ASM_TAC
THEN STRIP_TAC
THEN STRIP_TAC
THEN REPEAT RESA_TAC;

MRESA_TAC(GEN_ALL Local_lemmas.FST_EQ_IF_SAME_SND)
[`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`(FF:real^3#real^3->bool)`;`w:real^3`;`w1:real^3`]]);;



let AZIM_DEFOR_EDGE1=
prove(`local_fan(V,E,FF)/\ generic V E  /\ w1,v IN FF /\ t< &1
==>
azim (vec 0) (ww_defor w1 v t)
 (rho_node1 (IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF)
 (ww_defor w1 v t))
 (@a. a,ww_defor w1 v t IN
      IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF)
=azim (vec 0) v (rho_node1 FF v) (@a. a,v IN FF)`,

REPEAT STRIP_TAC
THEN MP_TAC(SET_RULE`t= &0 \/ ~(t= &0)`)
THEN RESA_TAC
THENL[

ASM_REWRITE_TAC[WW_DEFOR_0_ID;IMAGE_ID];

MP_TAC WW_DEFOR_ALPHA3
THEN RESA_TAC
THEN MP_TAC GENERIC_WW_DEFOR_RHO_NODE1
THEN RESA_TAC
THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V2)[`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`w1:real^3,v:real^3`;`V:real^3->bool`;]
THEN MRESA_TAC(GEN_ALL GENERIC_HYPOTHESIS_WW_DEFOR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`t:real`;`w1:real^3`]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`w1:real^3,v:real^3`)
THEN ASM_REWRITE_TAC[ww_defor]
THEN MRESAL_TAC (GEN_ALL Local_lemmas.IVS_RHO_NODE1_DETE)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`v:real^3`;`w1:real^3`][ivs_rho_node1]
THEN MP_TAC(REAL_ARITH`t< &1==> &0< &1- t`)
THEN RESA_TAC
THEN MRESAL_TAC (GEN_ALL AZIM_SCALE_ALL)[`&1`;`&1-t`;`&1`;`v:real^3`;`rho_node1 FF v`;`w1:real^3`][VECTOR_ARITH`&1 % v=v`;REAL_ARITH`&0< &1`]]);;

(******************)



let WW_DEFOR_FF4=
prove_by_refinement(`local_fan(V,E,FF)/\ generic V E  /\ v,w1 IN FF /\ ~(t= &0)
==>(!w.
(w:real^3),ww_defor (w1:real^3) v t IN
      IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF
<=> w,v IN FF)`,

[
REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;ww_defor]
THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V2)[`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3,w1:real^3`;`V:real^3->bool`;]
THEN MRESA_TAC(GEN_ALL GENERIC_HYPOTHESIS_WW_DEFOR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`t:real`;`w1:real^3`]
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA1_TAC th`v:real^3,w1:real^3`
THEN ASSUME_TAC th)
THEN EQ_TAC;


RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN MP_TAC(SET_RULE`w1=FST (x:real^3#real^3)\/ ~(FST x = w1:real^3)`)
THEN RESA_TAC;


REPLICATE_TAC (2) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPLICATE_TAC (2)  STRIP_TAC
THEN MRESA_TAC th[`x:real^3#real^3`])
THEN RESA_TAC;

SUBGOAL_THEN`w1,v IN (FF:real^3#real^3->bool)` ASSUME_TAC;

ASM_TAC
THEN STRIP_TAC
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN REPEAT RESA_TAC;


MRESA_TAC (GEN_ALL Local_lemmas.IVS_RHO_NODE1_DETE)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`v:real^3`;`w1:real^3`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.DETER_RHO_NODE)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`v:real^3`;`w1:real^3`]
THEN MRESAL_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`v:real^3`][SET_RULE`{a,a}={a}`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.DETER_RHO_NODE)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`w1:real^3`;`v:real^3`]
THEN MRESAL_TAC(GEN_ALL Local_lemmas.LOFA_CARD_EE_V_2)[`V:real^3->bool`;`(FF:real^3#real^3->bool)`;`w1:real^3`;`v:real^3`;`E:(real^3->bool)->bool`][Geomdetail.CARD_SING;ARITH_RULE`~(1=2)`];



MP_TAC(SET_RULE`w1= SND (x:real^3#real^3)\/ ~(SND x = w1:real^3)`)
THEN RESA_TAC;


STRIP_TAC
THEN SUBGOAL_THEN`w,w1 IN (FF:real^3#real^3->bool)` ASSUME_TAC;

ASM_TAC
THEN STRIP_TAC
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN REPEAT RESA_TAC;


MRESA_TAC(GEN_ALL Local_lemmas.FST_EQ_IF_SAME_SND)
[`V:real^3->bool`;`E:(real^3->bool)->bool`;`w1:real^3`;`(FF:real^3#real^3->bool)`;`w:real^3`;`v:real^3`]
THEN REPLICATE_TAC (16-9) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT  STRIP_TAC
THEN MRESA_TAC th[`x:real^3#real^3`]);

STRIP_TAC
THEN EXISTS_TAC`w:real^3,v:real^3`
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC (1) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPLICATE_TAC (1)  STRIP_TAC
THEN MRESA1_TAC th`w:real^3,v:real^3`)
THEN ASM_TAC
THEN MP_TAC(SET_RULE`(w=w1:real^3)\/ ~(w=w1)`)
THEN REPEAT RESA_TAC;

MRESA_TAC (GEN_ALL Local_lemmas.IVS_RHO_NODE1_DETE)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`v:real^3`;`w1:real^3`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.DETER_RHO_NODE)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`v:real^3`;`w1:real^3`]
THEN MRESAL_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`v:real^3`][SET_RULE`{a,a}={a}`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.DETER_RHO_NODE)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`w1:real^3`;`v:real^3`]
THEN MRESAL_TAC(GEN_ALL Local_lemmas.LOFA_CARD_EE_V_2)[`V:real^3->bool`;`(FF:real^3#real^3->bool)`;`w1:real^3`;`v:real^3`;`E:(real^3->bool)->bool`][Geomdetail.CARD_SING;ARITH_RULE`~(1=2)`];
]);;


let WW_DEFOR_RHO_NODE2=
prove(`local_fan(V,E,FF)/\ generic V E  /\ v,w1 IN FF /\ ~(t= &0)
==> (@w. w,ww_defor w1 v t IN
              IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF) =
  (@w.            w,v IN FF)`,

STRIP_TAC
THEN REWRITE_TAC[rho_node1]
THEN MP_TAC WW_DEFOR_FF4
THEN RESA_TAC);;


let GENERIC_WW_DEFOR_RHO_NODE2=
prove_by_refinement(
`local_fan(V,E,FF)/\ generic V E  /\ v,w1 IN FF /\ ~(t= &0)
==> rho_node1(
      IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF) (ww_defor (w1:real^3) v t)
= (&1-t) %w1`,

[
REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;ww_defor;rho_node1]
THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V2)[`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3,w1:real^3`;`V:real^3->bool`;]
THEN MRESA_TAC(GEN_ALL GENERIC_HYPOTHESIS_WW_DEFOR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`t:real`;`w1:real^3`]
THEN MATCH_MP_TAC Hypermap_and_fan.CHOICE_LEMMA
THEN STRIP_TAC;

EXISTS_TAC`(&1-t)%w1:real^3`THEN EXISTS_TAC`v:real^3,w1:real^3`
THEN ASM_REWRITE_TAC[];

REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN MP_TAC(SET_RULE`(FST (x:real^3#real^3)=w1)\/ ~((FST (x:real^3#real^3)=w1))`)
THEN RESA_TAC;

REPLICATE_TAC (2) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPLICATE_TAC (2)  STRIP_TAC
THEN MRESA_TAC th[`(v,w1):real^3#real^3`]);

REPLICATE_TAC (2) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPLICATE_TAC (2)  STRIP_TAC
THEN MRESA_TAC th[`(v,w1):real^3#real^3`])
THEN MP_TAC(SET_RULE`(SND (x:real^3#real^3)=w1)\/ ~((SND (x:real^3#real^3)=w1))`)
THEN RESA_TAC;

RESA_TAC;

STRIP_TAC
THEN SUBGOAL_THEN`v,w IN (FF:real^3#real^3->bool)` ASSUME_TAC;

ASM_TAC
THEN STRIP_TAC
THEN STRIP_TAC
THEN REPEAT RESA_TAC;

MRESA_TAC (GEN_ALL Local_lemmas.DETER_RHO_NODE)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`v:real^3`;`w1:real^3`]
THEN MRESA_TAC (GEN_ALL Local_lemmas.DETER_RHO_NODE)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`v:real^3`;`w:real^3`]]);;



let AZIM_DEFOR_EDGE2=
prove(`local_fan(V,E,FF)/\ generic V E  /\ v,w1 IN FF /\ t< &1
==>
azim (vec 0) (ww_defor w1 v t)
 (rho_node1 (IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF)
 (ww_defor w1 v t))
 (@a. a,ww_defor w1 v t IN
      IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF)
=azim (vec 0) v (rho_node1 FF v) (@a. a,v IN FF)`,

REPEAT STRIP_TAC
THEN MP_TAC(SET_RULE`t= &0 \/ ~(t= &0)`)
THEN RESA_TAC
THENL[
ASM_REWRITE_TAC[WW_DEFOR_0_ID;IMAGE_ID];
MP_TAC WW_DEFOR_RHO_NODE2
THEN RESA_TAC
THEN MP_TAC GENERIC_WW_DEFOR_RHO_NODE2
THEN RESA_TAC
THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V2)[`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3,w1:real^3`;`V:real^3->bool`;]
THEN MRESA_TAC(GEN_ALL GENERIC_HYPOTHESIS_WW_DEFOR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`t:real`;`w1:real^3`]
THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3,w1:real^3`)
THEN ASM_REWRITE_TAC[ww_defor]
THEN MP_TAC(REAL_ARITH`t< &1==> &0< &1- t`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL Local_lemmas.DETER_RHO_NODE)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`v:real^3`;`w1:real^3`]
THEN MRESAL_TAC (GEN_ALL AZIM_SCALE_ALL)[`&1-t`;`&1`;`&1`;`v:real^3`;`w1:real^3`;`(@a:real^3. a,(v:real^3) IN FF)`][VECTOR_ARITH`&1 % v=v`;REAL_ARITH`&0< &1`]]);;


let WW_DEFOR_FF5=
prove_by_refinement(
`local_fan(V,E,FF)/\ generic V E /\ ~(v=w1)/\ ~(w1,v IN FF) /\ ~(v,w1 IN FF)/\ ~(t= &0)/\ v IN V/\ w1 IN V
==>(!w.
ww_defor (w1:real^3) v t,(w:real^3) IN
      IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF
<=> v,w IN FF)`,

[
REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;ww_defor]
THEN EQ_TAC;

RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN MP_TAC(SET_RULE`FST (x:real^3#real^3)=w1\/ ~(FST x = w1:real^3)`)
THEN RESA_TAC;

MRESA_TAC(GEN_ALL GENERIC_HYPOTHESIS_WW_DEFOR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`t:real`;`w1:real^3`]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`x:real^3#real^3`])
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`w1:real^3`]
THEN POP_ASSUM (fun th-> MRESA_TAC th[`v:real^3`])
THEN MRESAL_TAC th3[`vec 0:real^3`;`w1:real^3`;`v:real^3`][Trigonometry2.AFF2;IN_ELIM_THM;VECTOR_ARITH`A % vec 0+B= B`]
THEN POP_ASSUM (fun th->
STRIP_TAC
THEN MP_TAC th)
THEN SUBGOAL_THEN`?t. v = (&1 - t) % w1:real^3`ASSUME_TAC;

EXISTS_TAC`t:real`
THEN ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[];


MP_TAC(SET_RULE`w1= SND (x:real^3#real^3)\/ ~(SND x = w1:real^3)`)
THEN RESA_TAC;

STRIP_TAC
THEN SUBGOAL_THEN`v,w1 IN (FF:real^3#real^3->bool)` ASSUME_TAC;

ASM_TAC
THEN REPLICATE_TAC (5) STRIP_TAC
THEN REPLICATE_TAC (5) REMOVE_ASSUM_TAC
THEN REPEAT RESA_TAC;

POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[];

STRIP_TAC
THEN EXISTS_TAC`v:real^3,w:real^3`
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`(w=w1:real^3)\/ ~(w=w1)`)
THEN REPEAT RESA_TAC]);;




let GENERIC_WW_DEFOR_RHO_NODE1_NOT_EDGE=
prove(
`local_fan(V,E,FF)/\ generic V E /\ ~(v=w1)/\ ~(w1,v IN FF) /\ ~(v,w1 IN FF)/\ ~(t= &0)/\ v IN V/\ w1 IN V
==> rho_node1(
      IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF) (ww_defor (w1:real^3) v t)
= rho_node1 FF v`,

RESA_TAC
THEN MP_TAC WW_DEFOR_FF5
THEN ASM_REWRITE_TAC[rho_node1]
THEN RESA_TAC);;






let WW_DEFOR_FF6=
prove_by_refinement(`local_fan(V,E,FF)/\ generic V E /\ ~(v=w1)/\ ~(w1,v IN FF) /\ ~(v,w1 IN FF)/\ ~(t= &0)/\ v IN V/\ w1 IN V
==>(!w.
(w:real^3),ww_defor (w1:real^3) v t IN
      IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF
<=> w,v IN FF)`,

[REPEAT STRIP_TAC
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;ww_defor]
THEN EQ_TAC;

RESA_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[PAIR_EQ]
THEN MP_TAC(SET_RULE`SND (x:real^3#real^3)=w1\/ ~(SND x = w1:real^3)`)
THEN RESA_TAC;

MRESA_TAC(GEN_ALL GENERIC_HYPOTHESIS_WW_DEFOR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`(FF:real^3#real^3->bool)`;`t:real`;`w1:real^3`]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`x:real^3#real^3`])
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`w1:real^3`]
THEN POP_ASSUM (fun th-> MRESA_TAC th[`v:real^3`])
THEN MRESAL_TAC th3[`vec 0:real^3`;`w1:real^3`;`v:real^3`][Trigonometry2.AFF2;IN_ELIM_THM;VECTOR_ARITH`A % vec 0+B= B`]
THEN POP_ASSUM (fun th->
STRIP_TAC THEN STRIP_TAC
THEN MP_TAC th)
THEN SUBGOAL_THEN`?t. v = (&1 - t) % w1:real^3`ASSUME_TAC;

EXISTS_TAC`t:real`
THEN ASM_REWRITE_TAC[];

ASM_REWRITE_TAC[];

MP_TAC(SET_RULE`w1= FST (x:real^3#real^3)\/ ~(FST x = w1:real^3)`)
THEN RESA_TAC;

STRIP_TAC
THEN SUBGOAL_THEN`w1,v IN (FF:real^3#real^3->bool)` ASSUME_TAC;


ASM_TAC
THEN REPLICATE_TAC (5) STRIP_TAC
THEN REPLICATE_TAC (5) REMOVE_ASSUM_TAC
THEN REPEAT RESA_TAC;

POP_ASSUM MP_TAC
THEN ASM_REWRITE_TAC[];

STRIP_TAC
THEN EXISTS_TAC`w:real^3,v:real^3`
THEN ASM_REWRITE_TAC[]
THEN POP_ASSUM MP_TAC
THEN MP_TAC(SET_RULE`(w=w1:real^3)\/ ~(w=w1)`)
THEN REPEAT RESA_TAC;]);;


let GENERIC_WW_DEFOR_RHO_NODE1_NOT_EDGE2=
prove(`local_fan(V,E,FF)/\ generic V E /\ ~(v=w1)/\ ~(w1,v IN FF) /\ ~(v,w1 IN FF)/\ ~(t= &0)/\ v IN V/\ w1 IN V
==>(@w.
(w:real^3),ww_defor (w1:real^3) v t IN
      IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF)=(@w. w,v IN FF)`,

RESA_TAC
THEN MP_TAC WW_DEFOR_FF6
THEN ASM_REWRITE_TAC[rho_node1]
THEN RESA_TAC);;




let AZIM_DEFOR_EDGE3=
prove(`local_fan(V,E,FF)/\ generic V E /\ ~(v=w1)/\ ~(w1,v IN FF) /\ ~(v,w1 IN FF)/\ v IN V/\ w1 IN V
==>
azim (vec 0) (ww_defor w1 v t)
 (rho_node1 (IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF)
 (ww_defor w1 v t))
 (@a. a,ww_defor w1 v t IN
      IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF)
=azim (vec 0) v (rho_node1 FF v) (@a. a,v IN FF)`,

REPEAT STRIP_TAC
THEN MP_TAC(SET_RULE`t= &0 \/ ~(t= &0)`)
THEN RESA_TAC
THENL[
ASM_REWRITE_TAC[WW_DEFOR_0_ID;IMAGE_ID];

MP_TAC GENERIC_WW_DEFOR_RHO_NODE1_NOT_EDGE2
THEN RESA_TAC
THEN MP_TAC GENERIC_WW_DEFOR_RHO_NODE1_NOT_EDGE
THEN RESA_TAC
THEN ASM_REWRITE_TAC[ww_defor]
THEN ASM_SIMP_TAC[AZIM_SPECIAL_SCALE]]);;





let AZIM_DEFORMATION_GENERIC=
prove_by_refinement(`local_fan(V,E,FF)/\ generic V E /\  v IN V/\ w1 IN V/\ t< &1
==>
azim (vec 0) (ww_defor w1 v t)
 (rho_node1 (IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF)
 (ww_defor w1 v t))
 (@a. a,ww_defor w1 v t IN
      IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) FF)
=azim (vec 0) v (rho_node1 FF v) (@a. a,v IN FF)`,

[STRIP_TAC
THEN MP_TAC(SET_RULE`w1=v:real^3\/ ~(w1=v)`)
THEN RESA_TAC;

MP_TAC GENEIRC_WW_DEFOR_AZIM
THEN RESA_TAC;

MP_TAC (SET_RULE`w1,v IN FF \/ v,w1 IN FF\/ (~(w1,v IN FF)/\ ~(v,w1 IN (FF:real^3#real^3->bool)))`)
THEN RESA_TAC;

MP_TAC AZIM_DEFOR_EDGE1
THEN RESA_TAC;

MP_TAC AZIM_DEFOR_EDGE2
THEN RESA_TAC;

MP_TAC AZIM_DEFOR_EDGE3
THEN RESA_TAC]);;


let V_DEFORMATION_WW_DEFOR=
prove(`IMAGE (\v. ww_defor w1 v t) (IMAGE w (:num))
=IMAGE (\i. ww_defor w1 (w i) t) (:num)`,

REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION]
THEN SET_TAC[]);;


let E_DEFORMATION_WW_DEFOR=
prove_by_refinement(`IMAGE (\i. {ww_defor w1 ((w:num->real^3) i) t, ww_defor w1 (w (SUC i)) t}) (:num)
= IMAGE (IMAGE (\v. ww_defor w1 v t)) (IMAGE (\i. {w i, w (SUC i)}) (:num))`,

[REWRITE_TAC[EXTENSION]
THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC;
RESA_TAC
THEN EXISTS_TAC`{(w:num->real^3) x', w (SUC x')}`
THEN STRIP_TAC;

EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[];
SET_TAC[];
RESA_TAC
THEN EXISTS_TAC`x'':num`
THEN ASM_REWRITE_TAC[]
THEN SET_TAC[]]);;
let F_DEFORMATION_WW_DEFOR=
prove(`IMAGE (\i. ww_defor w1 ((w:num->real^3) i) t,ww_defor w1 (w (SUC i)) t) (:num)
= IMAGE (\uv. ww_defor w1 (FST uv) t,ww_defor w1 (SND uv) t) (IMAGE (\i. w i,w (SUC i)) (:num))`,

REWRITE_TAC[EXTENSION;IMAGE;IN_ELIM_THM]
THEN GEN_TAC
THEN EQ_TAC
THENL[
RESA_TAC
THEN EXISTS_TAC`(w:num->real^3) x',w (SUC x')`
THEN ASM_REWRITE_TAC[]
THEN EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[];
RESA_TAC
THEN EXISTS_TAC`x'':num`
THEN ASM_REWRITE_TAC[]]);;




let WW_DEFOR_AFFINE_HULL=
prove(`!t. t IN real_interval (--e,e)
           ==> ww_defor w1 w1 t IN affine hull {vec 0, v, w', w1}`,

STRIP_TAC
THEN REWRITE_TAC[ww_defor;real_interval;IN_ELIM_THM;Collect_geom2.AFFINE_HULL_4]
THEN STRIP_TAC
THEN EXISTS_TAC`t:real`
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&0`
THEN EXISTS_TAC`&1-t:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`t+ &0+ &0+ &1-t= &1`]
THEN VECTOR_ARITH_TAC);;



(***concl ***)


let MHAEYJN_concl = 
`!a b V E FF f v w u.
     convex_local_fan (V,E,FF) /\
     lunar (v,w) V E /\
     deformation f V (a,b) /\
     interior_angle1 (vec 0) FF v < pi /\
     u IN V /\
     ~(u = v) /\
     ~(u = w) /\
     (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u') /\
     (!t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u})
     ==> (?e. &0 < e /\
              (!t. --e < t /\ t < e
                   ==> convex_local_fan
                       (IMAGE (\v. f v t) V,
                        IMAGE (IMAGE (\v. f v t)) E,
                        IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\
                       lunar (v,w) (IMAGE (\v. f v t) V)
                       (IMAGE (IMAGE (\v. f v t)) E)))`;;
let ZLZTHIC_concl = 
`!a b V E FF f.
     convex_local_fan (V,E,FF) /\
     generic V E /\
     deformation f V (a,b) /\
     (!v t. v IN V /\ t IN real_interval (a,b)/\ interior_angle1 (vec 0) FF v = pi ==> interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi)
     ==> (?e. &0 < e /\
              (!t. --e < t /\ t < e
                   ==> convex_local_fan
                       (IMAGE (\v. f v t) V,
                        IMAGE (IMAGE (\v. f v t)) E,
                        IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\
                       generic (IMAGE (\v. f v t) V)
                       (IMAGE (IMAGE (\v. f v t)) E)))`;;





let ODXLSTCv2_concl = `!s k w l.
  is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<k/\ 
  (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i) /\
  ~(&2 = norm (w l)) /\
  (!i. ~(i MOD k = l MOD k) ==> scs_a_v39 s l i < dist(w l,w i)) /\
  (!i. ~(scs_J_v39 s l i)) /\
  (!V E v.
     V = IMAGE w (:num) /\
      E = IMAGE (\i. {w i, w (SUC i)}) (:num) ==>
      ~(lunar (v,(w l)) V E )) ==> F`;;



let LEMMA1_concl = `!s k w l.
  is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<k/\ 
  (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i) /\
  ~(&2 = norm (w l)) /\
  (!i. ~(i MOD k = l MOD k) ==> scs_a_v39 s l i < dist(w l,w i)) /\
  (!i. ~(scs_J_v39 s l i)) /\
  (!V E v.
     V = IMAGE w (:num) /\
      E = IMAGE (\i. {w i, w (SUC i)}) (:num) ==>
      ~(lunar (v,(w l)) V E )) ==> 
(?e. &0 < e /\
              (!t. --e < t /\ t < e
                   ==> convex_local_fan
 (IMAGE (\i. ww_defor (w l) (w i) t) (:num),
  IMAGE (\i. {ww_defor (w l) (w i) t, ww_defor (w l) (w (SUC i)) t}) (:num),
  IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) (w (SUC i)) t) (:num))
))`;;





let TAUSTAR_WW_DEFOR_concl = `!s k w l.
  is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<k/\ 
  (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i) /\
  ~(&2 = norm (w l)) /\
  (!i. ~(i MOD k = l MOD k) ==> scs_a_v39 s l i < dist(w l,w i)) /\
  (!i. ~(scs_J_v39 s l i)) /\
(!t. &0 < t /\ t < e1 ==> BBs_v39 s (\i. ww_defor (w l) (w i) t))/\
&0< e1/\ e1< &1/\
  (!V E v.
     V = IMAGE w (:num) /\
      E = IMAGE (\i. {w i, w (SUC i)}) (:num) ==>
      ~(lunar (v,(w l)) V E )) ==> 
(?e. &0 < e /\
              (!t. &0 < t /\ t < e
                   ==> taustar_v39 s (\i. ww_defor (w l) (w i) t)< taustar_v39 s w 
))`;;

(***********)

let WW_DEFORMATION_CONVEX_LOCAL_FAN=prove_by_refinement((mk_imp(ZLZTHIC_concl, mk_imp (MHAEYJN_concl, LEMMA1_concl))),
[

REPEAT STRIP_TAC
THEN REPLICATE_TAC (9-2)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC th
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
THEN ASSUME_TAC th
THEN STRIP_TAC)
THEN ABBREV_TAC`V= IMAGE (w:num->real^3) (:num)`
THEN ABBREV_TAC`E = IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`
THEN ABBREV_TAC`FF = IMAGE (\i. ((w:num->real^3) i, w (SUC i))) (:num)`
THEN MRESAL_TAC JKQEWGV2[`s:scs_v39`;`w:num->real^3`][LET_DEF;LET_END_DEF;]
THEN MRESAL_TAC (GEN_ALL WW_DEFOR_DEFORMATION)[`(w:num->real^3) l`;`V:real^3->bool`;`&1`][REAL_ARITH`&0< &1`]
THEN SUBGOAL_THEN `convex_local_fan ((V:real^3->bool),(E:(real^3->bool)->bool),FF)` ASSUME_TAC;

ASM_TAC
THEN REPLICATE_TAC 5 (STRIP_TAC)
THEN MP_TAC(ARITH_RULE`3< k==> ~(k<=3)`)
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
THEN REPEAT RESA_TAC
THEN REPLICATE_TAC (25-12) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th
THEN ASM_REWRITE_TAC[])
THEN RESA_TAC;

POP_ASSUM(fun th-> MP_TAC th
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[convex_local_fan;]
THEN STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th1-> STRIP_TAC
THEN MP_TAC th1
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[local_fan;LET_DEF;LET_END_DEF]
THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
THEN STRIP_TAC
THEN REPLICATE_TAC (3) (REMOVE_ASSUM_TAC)
THEN ASSUME_TAC th1)
THEN ASSUME_TAC th)
THEN MRESA_TAC Deformation.XRECQNS[`-- &1`;`&1`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`ww_defor ((w:num->real^3) l)`]
THEN MRESAL_TAC (GEN_ALL WW_DEFOR_DEFORMATION)[`(w:num->real^3) l`;`V:real^3->bool`;`e:real`][REAL_ARITH`&0< &1`]
THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
THEN RESA_TAC;

ABBREV_TAC`e1= (min e (&1))/ &2`
THEN MP_TAC(REAL_ARITH`e1= (min e (&1))/ &2/\ &0< e==> &0< e1/\ e1< &1/\ e1< e `)
THEN RESA_TAC
THEN SUBGOAL_THEN`(w:num->real^3) l IN ball_annulus` ASSUME_TAC;

ASM_TAC
THEN REPLICATE_TAC 4 (STRIP_TAC)
THEN MP_TAC(ARITH_RULE`3< k==> ~(k<=3)`)
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;IMAGE;IN_ELIM_THM;SUBSET]
THEN REPEAT RESA_TAC
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) l= w x)`ASSUME_TAC;

EXISTS_TAC`l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];

REPLICATE_TAC (41-11) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`(w:num->real^3) l`);

EXISTS_TAC`l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];

REPLICATE_TAC (41-11) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`(w:num->real^3) l`);

ABBREV_TAC`w1= (w:num->real^3) l`
THEN SUBGOAL_THEN`(w1:real^3) IN V`ASSUME_TAC;

EXPAND_TAC"V"
THEN REWRITE_TAC[IN_ELIM_THM;IMAGE]
THEN EXISTS_TAC`l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];

SUBGOAL_THEN`(!v t.
           v IN V /\ t IN real_interval (-- e1, e1)/\ interior_angle1 (vec 0) FF v = pi
           ==>interior_angle1 (vec 0)
               (IMAGE
                (\uv. ww_defor ((w:num->real^3) l) (FST uv) t,ww_defor (w l) (SND uv) t)
               FF)
               (ww_defor (w l) v t) <=
               pi)`ASSUME_TAC;

REWRITE_TAC[interior_angle1;real_interval;IN_ELIM_THM]
THEN REPEAT RESA_TAC
THEN MP_TAC(REAL_ARITH`t< e1/\ e1< &1==> t< &1`)
THEN RESA_TAC
THEN MP_TAC AZIM_DEFORMATION_GENERIC
THEN RESA_TAC
THEN REAL_ARITH_TAC;

MRESAL_TAC (GEN_ALL WW_DEFOR_DEFORMATION)[`(w:num->real^3) l`;`V:real^3->bool`;`e1:real`][REAL_ARITH`&0< &1`]
THEN REPLICATE_TAC (41-0) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC th[`-- e1`;`e1:real`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`ww_defor ((w:num->real^3) l)`])
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN EXISTS_TAC`e':real`
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MRESAL_TAC th[`t:real`;][GSYM(GEN_ALL V_DEFORMATION_WW_DEFOR); E_DEFORMATION_WW_DEFOR;F_DEFORMATION_WW_DEFOR]);

(***lunar case**)


ABBREV_TAC`e1= (min e (&1))/ &2`
THEN MP_TAC(REAL_ARITH`e1= (min e (&1))/ &2/\ &0< e==> &0< e1/\ e1< &1/\ e1< e `)
THEN RESA_TAC
THEN SUBGOAL_THEN`(w:num->real^3) l IN ball_annulus` ASSUME_TAC;

ASM_TAC
THEN REPLICATE_TAC 4 (STRIP_TAC)
THEN MP_TAC(ARITH_RULE`3< k==> ~(k<=3)`)
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;IMAGE;IN_ELIM_THM;SUBSET]
THEN REPEAT RESA_TAC
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) l= w x)`ASSUME_TAC;

EXISTS_TAC`l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];

REPLICATE_TAC (41-11) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`(w:num->real^3) l`);

EXISTS_TAC`l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];

REPLICATE_TAC (41-11) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`(w:num->real^3) l`);

ABBREV_TAC`w1= (w:num->real^3) l`
THEN SUBGOAL_THEN`(w1:real^3) IN V`ASSUME_TAC;

EXPAND_TAC"V"
THEN REWRITE_TAC[IN_ELIM_THM;IMAGE]
THEN EXISTS_TAC`l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];

MRESAL_TAC JKQEWGV3[`s:scs_v39`;`w:num->real^3`;`v:real^3`;`w':real^3`][LET_DEF;LET_END_DEF;]
THEN MP_TAC(REAL_ARITH`interior_angle1 (vec 0) FF v < pi / &2/\ &0< pi
==> interior_angle1 (vec 0) FF v < pi`)
THEN ASM_REWRITE_TAC[PI_WORKS]
THEN RESA_TAC
THEN STRIP_TAC
THEN SUBGOAL_THEN`~(w1=v:real^3)`ASSUME_TAC;

POP_ASSUM(fun th-> MRESA_TAC th[`V:real^3->bool`;`E:(real^3->bool)->bool`;`w':real^3`])
THEN STRIP_TAC
THEN POP_ASSUM(fun th->
ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT RESA_TAC)
THEN ASM_REWRITE_TAC[Local_lemmas.LUNAR_COMM];

SUBGOAL_THEN`~(w1=w':real^3)`ASSUME_TAC;

REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`])
THEN STRIP_TAC
THEN POP_ASSUM(fun th->
ASM_TAC
THEN REWRITE_TAC[th]
THEN REPEAT RESA_TAC);

POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th)
THEN SUBGOAL_THEN`(!u' t.
           u' IN V /\ ~(w1 = u':real^3) /\ t IN real_interval (--e,e)
           ==> ww_defor w1 u' t = u')`ASSUME_TAC;

REPEAT STRIP_TAC
THEN REWRITE_TAC[ww_defor]
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM(fun th-> REWRITE_TAC[th]);

REPLICATE_TAC (44-1) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC th[`-- e`;`e:real`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`ww_defor ((w:num->real^3) l)`;`v:real^3`;`w':real^3`;`w1:real^3`])
THEN POP_ASSUM MP_TAC
THEN MRESA_TAC (GEN_ALL WW_DEFOR_AFFINE_HULL)[`e:real`;`v:real^3`;`w':real^3`;`w1:real^3`;]
THEN RESA_TAC
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN EXISTS_TAC`e':real`
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MRESAL_TAC th[`t:real`;][GSYM(GEN_ALL V_DEFORMATION_WW_DEFOR); E_DEFORMATION_WW_DEFOR;F_DEFORMATION_WW_DEFOR])]);;


let CARD_V_EQ_SCS_K1=
prove_by_refinement(
`  scs_k_v39 s =k /\
 IMAGE (vv:num->real^3) (:num)=V/\
 	is_scs_v39 s /\
3< k/\
	BBs_v39 s vv 
==> CARD V=k`,

[
REPEAT STRIP_TAC
THEN MP_TAC IS_SCS_STABLE_SYSTEM
THEN ASM_REWRITE_TAC[ARITH_RULE`3<4`]
THEN MP_TAC Qknvmlb.SCS_K_LE_6
THEN RESA_TAC
THEN STRIP_TAC
THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
         (change_type_v3 (scs_a_v39 s)),
         (change_type_v3 (scs_b_v39 s)),
         (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
         (\i. (1 + i) MOD scs_k_v39 s))`
THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
         (change_type_v3 (scs_a_v39 s))`;`
         (change_type_v3 (scs_b_v39 s))`;`
         (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
         (\i. (1 + i) MOD scs_k_v39 s)`]
THEN MP_TAC(ARITH_RULE`3 < scs_k_v39 s /\ scs_k_v39 s<=6 ==>  scs_k_v39 s=4 \/
scs_k_v39 s=5 \/ scs_k_v39 s=6`)
THEN RESA_TAC;

POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN ASSUME_TAC th)
THEN REPEAT STRIP_TAC
THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 0]:real^3^(2+2)`
THEN ABBREV_TAC`a=matvec (v:real^3^(2+2))`
THEN MP_TAC(INST_TYPE [`:2+2`,`:M`]V_E_FF_IS_SCS_CASES_4)
THEN ASM_REWRITE_TAC[Basics.DIMINDEX_4;IN]
THEN STRIP_TAC 
THEN MRESAL_TAC (INST_TYPE [`:2+2`,`:M`]VECTOR_3_4)[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 0`][ARITH_RULE`1<=4/\ 2<=4/\ 3<=4/\ 4<=4/\ 4 MOD 4= 0 /\ 1 MOD 4= 1 /\ 2 MOD 4= 2/\ 3 MOD 4= 3/\ ~(2=1)
/\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)`;Basics.DIMINDEX_4]
THEN EXPAND_TAC "V"
THEN REWRITE_TAC[V_SY;rows;Basics.DIMINDEX_4;ARITH_RULE`1<=i /\ i<=4 <=> i=1\/ i=2\/ i=3 \/ i=4`;SET_RULE`{row i v | i = 1 \/ i = 2 \/ i = 3 \/ i = 4}={row 1 v, row 2 v, row 3 v,row 4 v}`]
THEN ASM_REWRITE_TAC[]
THEN MP_TAC VV_INJ
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`1`;`2`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ 0<4/\ 1<4/\ 2<4/\ 3<4`]
THEN MRESAL_TAC th[`1`;`3`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ 0<4/\ 1<4/\ 2<4/\ 3<4`]
THEN MRESAL_TAC th[`1`;`0`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ 0<4/\ 1<4/\ 2<4/\ 3<4`]
THEN MRESAL_TAC th[`2`;`0`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ 0<4/\ 1<4/\ 2<4/\ 3<4`]
THEN MRESAL_TAC th[`3`;`0`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ 0<4/\ 1<4/\ 2<4/\ 3<4`]
THEN MRESAL_TAC th[`2`;`3`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ 0<4/\ 1<4/\ 2<4/\ 3<4`])
THEN  SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
                 IN_INSERT; NOT_IN_EMPTY]
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;

POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN ASSUME_TAC th)
THEN REPEAT STRIP_TAC
THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 0]:real^3^(2+3)`
THEN ABBREV_TAC`a=matvec (v:real^3^(2+3))`
THEN MP_TAC(INST_TYPE [`:2+3`,`:M`]V_E_FF_IS_SCS_CASES_5)
THEN ASM_REWRITE_TAC[Basics.DIMINDEX_5;IN]
THEN STRIP_TAC 
THEN MRESAL_TAC (INST_TYPE [`:2+3`,`:M`]VECTOR_3_5)[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 5<=5/\ 0 MOD 5= 0 /\ 1 MOD 5= 1 /\ 2 MOD 5= 2/\ 3 MOD 5= 3 /\ 4 MOD 5= 4 /\ 5 MOD 5=0 /\ ~(2=1)
/\ SUC 0 MOD 5= 1 /\ SUC 1 MOD 5= 2 /\ SUC 2 MOD 5= 3/\ SUC 3 MOD 5= 4
/\ SUC 4 MOD 5= 0 /\ SUC 5 MOD 5 = 1 /\ ~(3=1)/\ ~(1=0)`;SET_RULE`(a:num) IN (:num)`;Basics.DIMINDEX_5]
THEN EXPAND_TAC "V"
THEN REWRITE_TAC[V_SY;rows;Basics.DIMINDEX_5;ARITH_RULE`1<=i /\ i<=5 <=> i=1\/ i=2\/ i=3 \/ i=4 \/ i=5`;SET_RULE`{row i v | i = 1 \/ i = 2 \/ i = 3 \/ i = 4\/ i=5}={row 1 v, row 2 v, row 3 v,row 4 v, row 5 v}`]
THEN ASM_REWRITE_TAC[]
THEN MP_TAC VV_INJ
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`1`;`2`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ 0<5/\ 1<5/\ 2<5/\ 3<5/\ 4<5 /\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)`]
THEN MRESAL_TAC th[`1`;`3`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ 0<5/\ 1<5/\ 2<5/\ 3<5/\ 4<5 /\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)`]
THEN MRESAL_TAC th[`1`;`0`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ 0<5/\ 1<5/\ 2<5/\ 3<5/\ 4<5 /\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)`]
THEN MRESAL_TAC th[`2`;`0`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ 0<5/\ 1<5/\ 2<5/\ 3<5/\ 4<5 /\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)`]
THEN MRESAL_TAC th[`3`;`0`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ 0<5/\ 1<5/\ 2<5/\ 3<5/\ 4<5 /\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)`]
THEN MRESAL_TAC th[`2`;`3`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ 0<5/\ 1<5/\ 2<5/\ 3<5/\ 4<5 /\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)`]
THEN MRESAL_TAC th[`1`;`4`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ 0<5/\ 1<5/\ 2<5/\ 3<5/\ 4<5 /\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)`]
THEN MRESAL_TAC th[`2`;`4`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ 0<5/\ 1<5/\ 2<5/\ 3<5/\ 4<5 /\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)`]
THEN MRESAL_TAC th[`3`;`4`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ 0<5/\ 1<5/\ 2<5/\ 3<5/\ 4<5 /\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)`]
THEN MRESAL_TAC th[`0`;`4`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ 0<5/\ 1<5/\ 2<5/\ 3<5/\ 4<5 /\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)`])
THEN  SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
                 IN_INSERT; NOT_IN_EMPTY]
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC;

POP_ASSUM(fun th-> ASM_TAC
THEN REWRITE_TAC[th]
THEN ASSUME_TAC th)
THEN REPEAT STRIP_TAC
THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 5;(vv:num->real^3) 0]:real^3^(3+3)`
THEN ABBREV_TAC`a=matvec (v:real^3^(3+3))`
THEN MP_TAC(INST_TYPE [`:3+3`,`:M`]V_E_FF_IS_SCS_CASES_6)
THEN ASM_REWRITE_TAC[Basics.DIMINDEX_6;IN]
THEN STRIP_TAC 
THEN MRESAL_TAC (INST_TYPE [`:3+3`,`:M`]VECTOR_3_6)[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 5`;`(vv:num->real^3) 0`][ARITH_RULE`1<=6/\ 2<=6/\ 3<=6/\ 4<=6/\ 5<=6 /\ 6<=6 /\ 0 MOD 6= 0 /\ 1 MOD 6= 1 /\ 2 MOD 6= 2/\ 3 MOD 6= 3 /\ 4 MOD 6= 4 /\ 5 MOD 6=5 /\ 6 MOD 6=0 /\ ~(2=1)
/\ SUC 0 MOD 6= 1 /\ SUC 1 MOD 6= 2 /\ SUC 2 MOD 6= 3/\ SUC 3 MOD 6= 4
/\ SUC 4 MOD 6= 5 /\ SUC 5 MOD 6 = 0 /\ SUC 6 MOD 6 =1 /\ ~(3=1)/\ ~(1=0)`;Basics.DIMINDEX_6]
THEN EXPAND_TAC "V"
THEN REWRITE_TAC[V_SY;rows;Basics.DIMINDEX_6;ARITH_RULE`1<=i /\ i<=6 <=> i=1\/ i=2\/ i=3 \/ i=4 \/ i=5\/ i=6`;SET_RULE`{row i v | i = 1 \/ i = 2 \/ i = 3 \/ i = 4\/ i=5 \/ i=6}={row 1 v, row 2 v, row 3 v,row 4 v, row 5 v, row 6 v}`]
THEN ASM_REWRITE_TAC[]
THEN MP_TAC VV_INJ
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`1`;`2`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0) /\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)/\ 0<6/\ 1<6/\ 2<6/\ 3<6/\ 4<6/\ 5<6 /\ ~(0=5) /\ ~(1=5) /\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`]
THEN MRESAL_TAC th[`1`;`3`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)/\ 0<6/\ 1<6/\ 2<6/\ 3<6/\ 4<6/\ 5<6 /\ ~(0=5) /\ ~(1=5) /\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`]
THEN MRESAL_TAC th[`1`;`0`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)/\ 0<6/\ 1<6/\ 2<6/\ 3<6/\ 4<6/\ 5<6 /\ ~(0=5) /\ ~(1=5) /\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`]
THEN MRESAL_TAC th[`2`;`0`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)/\ 0<6/\ 1<6/\ 2<6/\ 3<6/\ 4<6/\ 5<6 /\ ~(0=5) /\ ~(1=5) /\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`]
THEN MRESAL_TAC th[`3`;`0`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)/\ 0<6/\ 1<6/\ 2<6/\ 3<6/\ 4<6/\ 5<6 /\ ~(0=5) /\ ~(1=5) /\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`]
THEN MRESAL_TAC th[`2`;`3`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)/\ 0<6/\ 1<6/\ 2<6/\ 3<6/\ 4<6/\ 5<6 /\ ~(0=5) /\ ~(1=5) /\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`]
THEN MRESAL_TAC th[`1`;`4`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)/\ 0<6/\ 1<6/\ 2<6/\ 3<6/\ 4<6/\ 5<6 /\ ~(0=5) /\ ~(1=5) /\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`]
THEN MRESAL_TAC th[`2`;`4`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)/\ 0<6/\ 1<6/\ 2<6/\ 3<6/\ 4<6/\ 5<6 /\ ~(0=5) /\ ~(1=5) /\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`]
THEN MRESAL_TAC th[`3`;`4`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)/\ 0<6/\ 1<6/\ 2<6/\ 3<6/\ 4<6/\ 5<6 /\ ~(0=5) /\ ~(1=5) /\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`]
THEN MRESAL_TAC th[`0`;`4`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)/\ 0<6/\ 1<6/\ 2<6/\ 3<6/\ 4<6/\ 5<6 /\ ~(0=5) /\ ~(1=5) /\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`]
THEN MRESAL_TAC th[`1`;`5`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)/\ 0<6/\ 1<6/\ 2<6/\ 3<6/\ 4<6/\ 5<6 /\ ~(0=5) /\ ~(1=5) /\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`]
THEN MRESAL_TAC th[`2`;`5`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)/\ 0<6/\ 1<6/\ 2<6/\ 3<6/\ 4<6/\ 5<6 /\ ~(0=5) /\ ~(1=5) /\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`]
THEN MRESAL_TAC th[`3`;`5`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)/\ 0<6/\ 1<6/\ 2<6/\ 3<6/\ 4<6/\ 5<6 /\ ~(0=5) /\ ~(1=5) /\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`]
THEN MRESAL_TAC th[`0`;`5`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)/\ 0<6/\ 1<6/\ 2<6/\ 3<6/\ 4<6/\ 5<6 /\ ~(0=5) /\ ~(1=5) /\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`]
THEN MRESAL_TAC th[`4`;`5`][ARITH_RULE`~(1=2)/\ ~(1=0) /\ ~(1=3)/\ ~(2=3)/\ ~(2=0)/\ ~(3=0)/\ ~(3=4)/\ ~(1=4)/\ ~(2=4)/\ ~(0=4)/\ 0<6/\ 1<6/\ 2<6/\ 3<6/\ 4<6/\ 5<6 /\ ~(0=5) /\ ~(1=5) /\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`])
THEN  SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
                 IN_INSERT; NOT_IN_EMPTY]
THEN ASM_REWRITE_TAC[]
THEN ARITH_TAC]);;




let CARD_FF_EQ_WW_DEFORMATION=
prove(`
scs_k_v39 s =k /\
 IMAGE (w:num->real^3) (:num)=V/\
 	is_scs_v39 s /\
3< k/\
	BBs_v39 s w /\(!t. &0 < t /\ t < e1 ==> BBs_v39 s (\i. ww_defor (w l) (w i) t))
==> (!t. &0< t/\ t< e1==>
CARD               (IMAGE
                      (\i. ww_defor ((w:num->real^3) l) (w i) t,
                           ww_defor (w l) (w (SUC i)) t)
                     (:num))
=CARD(IMAGE (\i. w i,w (SUC i)) (:num)))`,


STRIP_TAC
THEN GEN_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MRESA_TAC th[`t:real`])
THEN MRESA_TAC(GEN_ALL CARD_V_EQ_SCS_K1)[`s:scs_v39`;`w:num->real^3`;`IMAGE (w:num->real^3) (:num)`;`k:num`]
THEN MRESA_TAC(GEN_ALL CARD_V_EQ_SCS_K1)[`s:scs_v39`;`(\i. ww_defor ((w:num->real^3) l) (w i) t)`;`IMAGE ((\i. ww_defor ((w:num->real^3) l) (w i) t)) (:num)`;`k:num`]
THEN MP_TAC(ARITH_RULE`3<k==> ~(k<= 3)`)
THEN RESA_TAC
THEN POP_ASSUM(fun th-> ASM_TAC
THEN ASSUME_TAC(th)
THEN REPEAT RESA_TAC)
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39;convex_local_fan]
THEN REPEAT RESA_TAC
THEN MRESA_TAC(GEN_ALL Local_lemmas.LOFA_IMP_CARD_FF_V_EQ)
[`IMAGE (\i. {ww_defor ((w:num->real^3) l) (w i) t, ww_defor (w l) (w (SUC i)) t})
       (:num)`;`IMAGE (\i. ww_defor ((w:num->real^3) l) (w i) t,ww_defor (w l) (w (SUC i)) t) (:num)`;`IMAGE (\i. ww_defor (w l) ((w:num->real^3) i) t) (:num)`]
THEN MRESA_TAC(GEN_ALL Local_lemmas.LOFA_IMP_CARD_FF_V_EQ)
[`IMAGE (\i. {w i, (w:num->real^3) (SUC i)}) (:num)`;`IMAGE (\i. w i,(w:num->real^3) (SUC i)) (:num)`;`V:real^3->bool`]);;




let DSV_WW_DEFOR_EQ=
prove_by_refinement(`
scs_k_v39 s=k/\
  is_scs_v39 s /\
  BBs_v39 s w /\
(!i. ~(scs_J_v39 s l i))
==>
dsv_v39 s (\i. ww_defor (w l) (w i) t) = dsv_v39 s w`,

[
REWRITE_TAC[dsv_v39]
THEN STRIP_TAC
THEN MATCH_MP_TAC(REAL_ARITH`a=b==> c+a=c+b`)
THEN MP_TAC(SET_RULE`is_ear_v39 s\/ ~(is_ear_v39 s)`)
THEN RESA_TAC
THEN MATCH_MP_TAC(REAL_ARITH`a=b==> #0.1*a= #0.1*b`);

REWRITE_TAC[REAL_ARITH`&1 *a=a`]
THEN MATCH_MP_TAC SUM_EQ
THEN REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN MP_TAC(SET_RULE`(w:num->real^3) l= w x\/ ~(w l =w x)`)
THEN RESA_TAC;

MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`w:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;is_scs_v39]
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`3<=k ==> ~(k=0)`)
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESA_TAC DIVISION[`l:num`;`scs_k_v39 s`]
THEN REPLICATE_TAC (4) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`l MOD k:num`;`x:num`])
THEN REPLICATE_TAC (34-25) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`SUC x:num`;])
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (SUC x)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`]);

MP_TAC(SET_RULE`(w:num->real^3) l= w (SUC x)\/ ~(w l =w (SUC x))`)
THEN RESA_TAC;


MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`w:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;is_scs_v39]
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`3<=k ==> ~(k=0)`)
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`]
THEN POP_ASSUM MP_TAC
THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN MRESA_TAC DIVISION[`l:num`;`scs_k_v39 s`]
THEN MRESA_TAC DIVISION[`SUC x:num`;`scs_k_v39 s`]
THEN REPLICATE_TAC (6) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`l MOD k:num`;`SUC x MOD k:num`])
THEN REPLICATE_TAC (37-25) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`x:num`;])
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (x)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> 
MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);

ASM_REWRITE_TAC[ww_defor];


REWRITE_TAC[REAL_ARITH`-- &1 *a= -- &1 * b<=> a=b`]
THEN MATCH_MP_TAC SUM_EQ
THEN REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT STRIP_TAC
THEN MP_TAC(SET_RULE`(w:num->real^3) l= w x\/ ~(w l =w x)`)
THEN RESA_TAC;

MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`w:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;is_scs_v39]
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`3<=k ==> ~(k=0)`)
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESA_TAC DIVISION[`l:num`;`scs_k_v39 s`]
THEN REPLICATE_TAC (4) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`l MOD k:num`;`x:num`])
THEN REPLICATE_TAC (34-25) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`SUC x:num`;])
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (SUC x)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`]);

MP_TAC(SET_RULE`(w:num->real^3) l= w (SUC x)\/ ~(w l =w (SUC x))`)
THEN RESA_TAC;


MRESA_TAC (GEN_ALL VV_INJ)[`s:scs_v39`;`k:num`;`w:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;is_scs_v39]
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`3<=k ==> ~(k=0)`)
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`]
THEN POP_ASSUM MP_TAC
THEN MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN MRESA_TAC DIVISION[`l:num`;`scs_k_v39 s`]
THEN MRESA_TAC DIVISION[`SUC x:num`;`scs_k_v39 s`]
THEN REPLICATE_TAC (6) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`l MOD k:num`;`SUC x MOD k:num`])
THEN REPLICATE_TAC (37-25) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`x:num`;])
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (x)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> 
MRESAL1_TAC th`SUC x:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);


ASM_REWRITE_TAC[ww_defor]]);;



let INTERIOR_ANGLE_SAME_WW_DEFOR0=
prove_by_refinement(`
3<k/\
is_scs_v39 s/\
scs_k_v39 s = k/\
BBs_v39 s w/\
BBs_v39 s (\i. ww_defor (w l) (w i) t)/\
IMAGE (\i. w i,w (SUC i)) (:num) = FF/\
t< &1
==> 
interior_angle1 (vec 0)
 (IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) (w (SUC i)) t) (:num))
 (ww_defor (w l) (w (l MOD k)) t) =
 interior_angle1 (vec 0) FF (w (l MOD k))`,

[
STRIP_TAC
THEN ASM_TAC
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)`)
THEN RESA_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39]
THEN REPEAT RESA_TAC
THEN SUBGOAL_THEN`w (l MOD k) IN IMAGE (w:num->real^3) (:num)`ASSUME_TAC;

REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`l MOD k`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];

REPLICATE_TAC (14-7)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th
THEN REWRITE_TAC[convex_local_fan;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
THEN ASSUME_TAC th
THEN STRIP_TAC)
THEN REPLICATE_TAC (16-10)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th
THEN REWRITE_TAC[convex_local_fan;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
THEN ASSUME_TAC th
THEN STRIP_TAC)
THEN MRESAL_TAC(GEN_ALL CARD_V_EQ_SCS_K1)[`s:scs_v39`;`w:num->real^3`;`IMAGE (w:num->real^3) (:num)`;`k:num`][MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39]
THEN MRESAL_TAC(GEN_ALL CARD_V_EQ_SCS_K1)[`s:scs_v39`;`(\i. ww_defor ((w:num->real^3) l) (w i) t)`;`IMAGE ((\i. ww_defor ((w:num->real^3) l) (w i) t)) (:num)`;`k:num`][MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39]
THEN MRESA_TAC(GEN_ALL Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS)
[`IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`;`IMAGE (w:num->real^3) (:num)`;`IMAGE (\i. w i,(w:num->real^3) (SUC i)) (:num)`]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`(w:num->real^3) (l MOD k)`])
THEN  MRESA_TAC (GEN_ALL Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1)[`IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`;`IMAGE (w:num->real^3) (:num)`;`IMAGE (\i. w i,(w:num->real^3) (SUC i)) (:num)`]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`(w:num->real^3) (l MOD k)`])
THEN MRESAL_TAC (GEN_ALL Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME)[`IMAGE (w:num->real^3) (:num)`;`IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`;`k:num`;`s:scs_v39`;`IMAGE (\i. w i,(w:num->real^3) (SUC i)) (:num)`;`(w:num->real^3) (l MOD k)`;`w:num->real^3`;`l MOD k:num`][MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39]
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`SUC 0`][ITER] THEN MRESA_TAC th[`k-1`])
THEN SUBGOAL_THEN`(&1-t) %((w:num->real^3) (l MOD k)) IN IMAGE (\i. ww_defor (w l) (w i) t) (:num)`ASSUME_TAC;

REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`l MOD k`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ww_defor]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;is_scs_v39]
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`3<k ==> ~(k=0)`)
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;];

SUBGOAL_THEN`ww_defor (w l) (w (l MOD k)) t =(&1-t) %((w:num->real^3) (l MOD k))` ASSUME_TAC;

ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ww_defor]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;is_scs_v39]
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`3<k ==> ~(k=0)`)
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;];

MRESA_TAC(GEN_ALL Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS)
[`IMAGE (\i. {ww_defor (w l) (w i) t, ww_defor ((w:num->real^3) l) (w (SUC i)) t}) (:num)`;`IMAGE (\i. ww_defor (w l) ((w:num->real^3) i) t) (:num)`;`IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) ((w:num->real^3) (SUC i)) t) (:num)`]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`(&1-t) %((w:num->real^3) (l MOD k))`])
THEN  MRESA_TAC (GEN_ALL Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1)
[`IMAGE (\i. {ww_defor (w l) (w i) t, ww_defor ((w:num->real^3) l) (w (SUC i)) t}) (:num)`;`IMAGE (\i. ww_defor (w l) ((w:num->real^3) i) t) (:num)`;`IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) ((w:num->real^3) (SUC i)) t) (:num)`]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`(&1-t) %((w:num->real^3) (l MOD k))`])
THEN MRESAL_TAC (GEN_ALL Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME)
[`IMAGE (\i. ww_defor (w l) ((w:num->real^3) i) t) (:num)`;`IMAGE (\i. {ww_defor (w l) (w i) t, ww_defor ((w:num->real^3) l) (w (SUC i)) t}) (:num)`;`k:num`;`s:scs_v39`;`IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) ((w:num->real^3) (SUC i)) t) (:num)`;`(\i. ww_defor (w l) ((w:num->real^3) i) t) (l MOD k)`;`(\i. ww_defor (w l) ((w:num->real^3) i) t)`;`l MOD k`]
[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39]
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`SUC 0`][ITER] THEN MRESA_TAC th[`k-1`])
THEN MP_TAC(ARITH_RULE`3<k==> 1<k/\ k-1<k/\ 0< k-1/\ ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_DIS_ELMS23)
[`IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`;`IMAGE (w:num->real^3) (:num)`;`IMAGE (\i. w i,(w:num->real^3) (SUC i)) (:num)`;`(w:num->real^3) (l MOD k)`]
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`0:num`;`SUC 0`][ITER;ARITH_RULE`0< SUC 0/\ SUC 0=1`]
THEN MRESAL_TAC th[`0`;`k-1`][ITER])
THEN ASM_REWRITE_TAC[ww_defor]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN MRESAL_TAC (GEN_ALL AZIM_SCALE_ALL)[`&1`;`&1`;`&1-t`;`(w:num->real^3) (l MOD k)`;`(w:num->real^3) (1+l MOD k)`;`(w:num->real^3) (k-1+l MOD k)`][VECTOR_ARITH`&1 % v=v`;REAL_ARITH`&0< &1/\ (&0< &1-t<=> t< &1)`]]);;



let INTERIOR_ANGLE_SAME_WW_DEFOR1=
prove_by_refinement(`
3<k/\
is_scs_v39 s/\
scs_k_v39 s = k/\
BBs_v39 s w/\
BBs_v39 s (\i. ww_defor (w l) (w i) t)/\
IMAGE (\i. w i,w (SUC i)) (:num) = FF/\
t< &1 /\ 1<=i /\ i< k
==> 
interior_angle1 (vec 0)
      (IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) (w (SUC i)) t)
      (:num))
      (ITER i
       (rho_node1
       (IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) (w (SUC i)) t)
       (:num)))
      (ww_defor (w l) (w (l MOD k)) t)) =
interior_angle1 (vec 0) FF (ITER i (rho_node1 FF) (w (l MOD k)))`,

[
STRIP_TAC
THEN ASM_TAC
THEN STRIP_TAC
THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)`)
THEN RESA_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39]
THEN REPEAT RESA_TAC
THEN SUBGOAL_THEN`w (l MOD k) IN IMAGE (w:num->real^3) (:num)`ASSUME_TAC;

REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`l MOD k`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];

REPLICATE_TAC (16-7)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th
THEN REWRITE_TAC[convex_local_fan;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
THEN ASSUME_TAC th
THEN STRIP_TAC)
THEN REPLICATE_TAC (18-10)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th
THEN REWRITE_TAC[convex_local_fan;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
THEN ASSUME_TAC th
THEN STRIP_TAC)
THEN MRESAL_TAC(GEN_ALL CARD_V_EQ_SCS_K1)[`s:scs_v39`;`w:num->real^3`;`IMAGE (w:num->real^3) (:num)`;`k:num`][MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39]
THEN MRESAL_TAC(GEN_ALL CARD_V_EQ_SCS_K1)[`s:scs_v39`;`(\i. ww_defor ((w:num->real^3) l) (w i) t)`;`IMAGE ((\i. ww_defor ((w:num->real^3) l) (w i) t)) (:num)`;`k:num`][MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39]
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V)
[`IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`;`IMAGE (\i. w i,(w:num->real^3) (SUC i)) (:num)`;`(w:num->real^3)(l MOD k)`;`IMAGE (w:num->real^3) (:num)`;]
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`])
THEN MRESA_TAC(GEN_ALL Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS)
[`IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`;`IMAGE (w:num->real^3) (:num)`;`IMAGE (\i. w i,(w:num->real^3) (SUC i)) (:num)`]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`ITER i (rho_node1 FF)((w:num->real^3) (l MOD k))`])
THEN  MRESA_TAC (GEN_ALL Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1)[`IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`;`IMAGE (w:num->real^3) (:num)`;`IMAGE (\i. w i,(w:num->real^3) (SUC i)) (:num)`]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`ITER i (rho_node1 FF)((w:num->real^3) (l MOD k))`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;ITER_ADD])
THEN MRESAL_TAC (GEN_ALL Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME)[`IMAGE (w:num->real^3) (:num)`;`IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`;`k:num`;`s:scs_v39`;`IMAGE (\i. w i,(w:num->real^3) (SUC i)) (:num)`;`(w:num->real^3) (l MOD k)`;`w:num->real^3`;`l MOD k:num`][MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`i:num`] THEN MRESAL_TAC th[`SUC(i)`][ITER] THEN MRESA_TAC th[`k-1+i`] THEN MRESA_TAC th[`SUC i:num`] THEN MRESA_TAC th[`k-2:num`]
THEN MRESA_TAC th[`i-1:num`])
THEN SUBGOAL_THEN`(&1-t) %((w:num->real^3) (l MOD k)) IN IMAGE (\i. ww_defor (w l) (w i) t) (:num)`ASSUME_TAC;

REWRITE_TAC[IMAGE;IN_ELIM_THM]
THEN EXISTS_TAC`l MOD k`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ww_defor]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;is_scs_v39]
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`3<k ==> ~(k=0)`)
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;];

SUBGOAL_THEN`ww_defor (w l) (w (l MOD k)) t =(&1-t) %((w:num->real^3) (l MOD k))` ASSUME_TAC;

ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ww_defor]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;is_scs_v39]
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`3<k ==> ~(k=0)`)
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;];


MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V)
[`IMAGE (\i. {ww_defor (w l) (w i) t, ww_defor ((w:num->real^3) l) (w (SUC i)) t}) (:num)`;`IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) ((w:num->real^3) (SUC i)) t) (:num)`;`(&1 - t) % (w:num->real^3) (l MOD k)`;`IMAGE (\i. ww_defor (w l) ((w:num->real^3) i) t) (:num)`]
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`])
THEN MRESA_TAC(GEN_ALL Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS)
[`IMAGE (\i. {ww_defor (w l) (w i) t, ww_defor ((w:num->real^3) l) (w (SUC i)) t}) (:num)`;`IMAGE (\i. ww_defor (w l) ((w:num->real^3) i) t) (:num)`;`IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) ((w:num->real^3) (SUC i)) t) (:num)`]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`(ITER i
  (rho_node1
  (IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) (w (SUC i)) t) (:num)))
 ((&1 - t) % w (l MOD k)))
`])
THEN  MRESA_TAC (GEN_ALL Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1)
[`IMAGE (\i. {ww_defor (w l) (w i) t, ww_defor ((w:num->real^3) l) (w (SUC i)) t}) (:num)`;`IMAGE (\i. ww_defor (w l) ((w:num->real^3) i) t) (:num)`;`IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) ((w:num->real^3) (SUC i)) t) (:num)`]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`(ITER i
  (rho_node1
  (IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) (w (SUC i)) t) (:num)))
 ((&1 - t) % w (l MOD k)))
`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;ITER_ADD])
THEN MRESAL_TAC (GEN_ALL Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME)
[`IMAGE (\i. ww_defor (w l) ((w:num->real^3) i) t) (:num)`;`IMAGE (\i. {ww_defor (w l) (w i) t, ww_defor ((w:num->real^3) l) (w (SUC i)) t}) (:num)`;`k:num`;`s:scs_v39`;`IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) ((w:num->real^3) (SUC i)) t) (:num)`;`(\i. ww_defor (w l) ((w:num->real^3) i) t) (l MOD k)`;`(\i. ww_defor (w l) ((w:num->real^3) i) t)`;`l MOD k`]
[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`i:num`] THEN MRESAL_TAC th[`SUC(i)`][ITER] THEN MRESA_TAC th[`k-1+i`])
THEN MP_TAC(ARITH_RULE`3<k==> k-1+1=k/\ k-1<k/\ 0< k-1/\ ~(k=0)/\ 1<k/\ 2<k/\ SUC(k-1)=k/\ 0< k-2/\ k-2<k/\ k-1+k-1=k+(k-2)`)
THEN RESA_TAC
THEN MP_TAC(ARITH_RULE`1<=i/\ i<k /\ 3<k==> i=1\/ i=k-1\/ (1<i/\ i< k-1)`)
THEN RESA_TAC;


MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_DIS_ELMS23)
[`IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`;`IMAGE (w:num->real^3) (:num)`;`IMAGE (\i. w i,(w:num->real^3) (SUC i)) (:num)`;`(w:num->real^3) (l MOD k)`]
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`0:num`;`i:num `][ITER;ARITH_RULE`0< 1/\ SUC 0=1`]
THEN MRESAL_TAC th[`0`;`SUC(i)`][ARITH_RULE`SUC 1=2/\ 0<2`;ITER])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`(k-1+ i) + l MOD k:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`l MOD k`][ARITH_RULE`1*k=k/\ SUC 1=2`]
THEN MRESA_TAC MOD_MOD_REFL[`l:num`;`k:num`]
THEN ASM_REWRITE_TAC[ww_defor]
THEN MRESAL_TAC (GEN_ALL AZIM_SCALE_ALL)[`&1`;`&1-t`;`&1`;`(w:num->real^3) (1+l MOD k)`;`(w:num->real^3) (2+l MOD k)`;`(w:num->real^3) (l MOD k)`][VECTOR_ARITH`&1 % v=v`;REAL_ARITH`&0< &1/\ (&0< &1-t<=> t< &1)`];


MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_DIS_ELMS23)
[`IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`;`IMAGE (w:num->real^3) (:num)`;`IMAGE (\i. w i,(w:num->real^3) (SUC i)) (:num)`;`(w:num->real^3) (l MOD k)`]
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`0:num`;`i:num `][ITER;ARITH_RULE`0< 1/\ SUC 0=1`]
THEN MRESAL_TAC th[`0`;`k-2`][ARITH_RULE`SUC 1=2/\ 0<2`;ITER])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> 
MRESAL1_TAC th`k-2 + l MOD k:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`(k-1+ k-1) + l MOD k:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`k + l MOD k:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`l MOD k`][ARITH_RULE`1*k=k/\ SUC 1=2`]
THEN MRESA_TAC MOD_MOD_REFL[`l:num`;`k:num`]
THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`k-2+l MOD k`][ARITH_RULE`1*k=k/\ SUC 1=2`;ARITH_RULE`(k + k - 2) + l MOD k=k + k - 2 + l MOD k`]
THEN ASM_REWRITE_TAC[ww_defor]
THEN MRESAL_TAC (GEN_ALL AZIM_SCALE_ALL)[`&1-t`;`&1`;`&1`;`(w:num->real^3) (k-1+l MOD k)`;`(w:num->real^3) (l MOD k)`;`(w:num->real^3) (k-2+l MOD k)`][VECTOR_ARITH`&1 % v=v`;REAL_ARITH`&0< &1/\ (&0< &1-t<=> t< &1)`];

MP_TAC(ARITH_RULE`1<i/\ i< k-1==> 0<i-1/\ i-1<k/\ 0<i/\ 0< SUC i/\ SUC i< k/\ (k - 1 + i) + l MOD k= k+(i-1)+l MOD k`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_DIS_ELMS23)
[`IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`;`IMAGE (w:num->real^3) (:num)`;`IMAGE (\i. w i,(w:num->real^3) (SUC i)) (:num)`;`(w:num->real^3) (l MOD k)`]
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`0:num`;`i:num `][ITER;ARITH_RULE`0< 1/\ SUC 0=1`]
THEN MRESAL_TAC th[`0`;`SUC i`][ARITH_RULE`SUC 1=2/\ 0<2`;ITER]
THEN MRESAL_TAC th[`0`;`i-1`][ARITH_RULE`SUC 1=2/\ 0<2`;ITER])
THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`i-1+l MOD k`][ARITH_RULE`1*k=k/\ SUC 1=2`]
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> 
MRESAL1_TAC th`i-1 + l MOD k:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`k+i-1 + l MOD k:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
THEN ASM_REWRITE_TAC[ww_defor]]);;



let INTERIOR_ANGLE_SAME_WW_DEFOR=
prove(`3<k/\
is_scs_v39 s/\
scs_k_v39 s = k/\
BBs_v39 s w/\
BBs_v39 s (\i. ww_defor (w l) (w i) t)/\
IMAGE (\i. w i,w (SUC i)) (:num) = FF/\
t< &1 /\  i< k
==> 
interior_angle1 (vec 0)
      (IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) (w (SUC i)) t)
      (:num))
      (ITER i
       (rho_node1
       (IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) (w (SUC i)) t)
       (:num)))
      (ww_defor (w l) (w (l MOD k)) t)) =
interior_angle1 (vec 0) FF (ITER i (rho_node1 FF) (w (l MOD k)))`,


REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`i=0\/ 1<=i`)
THEN RESA_TAC
THENL[
REWRITE_TAC[ITER]
THEN MP_TAC INTERIOR_ANGLE_SAME_WW_DEFOR0
THEN RESA_TAC;

MP_TAC INTERIOR_ANGLE_SAME_WW_DEFOR1
THEN RESA_TAC]);;


let rho_fun_decreasing=
prove_by_refinement(`
 &0< t/\ t< &1/\ ~(wl= vec 0)
==> rho_fun (norm (ww_defor (wl) (wl) t))
<  rho_fun (norm (wl))`,

[
STRIP_TAC
THEN REWRITE_TAC[rho_fun;h0;]
THEN MATCH_MP_TAC(REAL_ARITH`a<b==> c+a<c+ b`)
THEN MATCH_MP_TAC REAL_LT_LMUL
THEN STRIP_TAC;

MATCH_MP_TAC REAL_LT_INV
THEN REAL_ARITH_TAC;

MATCH_MP_TAC REAL_LT_LMUL
THEN STRIP_TAC;

MATCH_MP_TAC REAL_LT_INV
THEN REWRITE_TAC[PI_WORKS];

MATCH_MP_TAC REAL_LT_LMUL
THEN REWRITE_TAC[Gbycpxs.SOL0_POS]
THEN MATCH_MP_TAC(REAL_ARITH`a<b==> a-c<b-c`)
THEN REWRITE_TAC[ww_defor;NORM_MUL]
THEN MP_TAC(REAL_ARITH`t< &1==> &0<= &1- t`)
THEN RESA_TAC
THEN MRESA_TAC REAL_ABS_REFL[`&1-t`]
THEN REWRITE_TAC[REAL_ARITH`(&1 - t) * norm wl < norm wl<=> &0< t *norm wl`]
THEN MATCH_MP_TAC REAL_LT_MUL
THEN ASM_REWRITE_TAC[NORM_POS_LT]]);;





let TAUSTAR_WW_DEFOR=prove_by_refinement((mk_imp(ZLZTHIC_concl, mk_imp (MHAEYJN_concl, TAUSTAR_WW_DEFOR_concl))),
[
REPEAT STRIP_TAC
THEN REPLICATE_TAC (12-2)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC th
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
THEN ASSUME_TAC th
THEN STRIP_TAC)
THEN ABBREV_TAC`V= IMAGE (w:num->real^3) (:num)`
THEN ABBREV_TAC`E = IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`
THEN ABBREV_TAC`FF = IMAGE (\i. ((w:num->real^3) i, w (SUC i))) (:num)`
THEN MRESAL_TAC JKQEWGV2[`s:scs_v39`;`w:num->real^3`][LET_DEF;LET_END_DEF;]
THEN MRESAL_TAC (GEN_ALL WW_DEFOR_DEFORMATION)[`(w:num->real^3) l`;`V:real^3->bool`;`&1`][REAL_ARITH`&0< &1`]
THEN MP_TAC(ARITH_RULE`3<k==> ~(k<= 3)`)
THEN RESA_TAC
THEN ASM_REWRITE_TAC[taustar_v39;LET_DEF;LET_END_DEF;tau_fun]
THEN STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN EXISTS_TAC`e1:real`
THEN ASM_REWRITE_TAC[]
THEN REPEAT STRIP_TAC
THEN MP_TAC CARD_FF_EQ_WW_DEFORMATION
THEN RESA_TAC
THEN POP_ASSUM(fun th->MRESA1_TAC th`t:real`)
THEN MP_TAC DSV_WW_DEFOR_EQ
THEN RESA_TAC
THEN MATCH_MP_TAC(REAL_ARITH`a<b==> a-c< b-c`)
THEN MATCH_MP_TAC(REAL_ARITH`a<b==> a-c< b-c`)
THEN MRESA_TAC(GEN_ALL Qknvmlb.SUM_AZIM_EQ_ANGLE_LE4)[`V:real^3->bool`;`w:num->real^3`;`l:num`;`s:scs_v39`;`(w:num->real^3) (l MOD scs_k_v39 s)`;`FF:real^3#real^3->bool`;`E:(real^3->bool)->bool`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN REPLICATE_TAC (31-9)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`t:real`])
THEN MRESA_TAC(GEN_ALL Qknvmlb.SUM_AZIM_EQ_ANGLE_LE4)[`IMAGE (\i. ww_defor (w l) ((w:num->real^3) i) t) (:num)`;`(\i. ww_defor (w l) ((w:num->real^3) i) t)`;`l:num`;`s:scs_v39`;`(\i. ww_defor (w l) ((w:num->real^3) i) t) (l MOD scs_k_v39 s)`;`IMAGE (\i. ww_defor ((w:num->real^3) l) (w i) t,ww_defor (w l) (w (SUC i)) t) (:num)`;`IMAGE (\i. {ww_defor (w l) ((w:num->real^3) i) t, ww_defor (w l) (w (SUC i)) t}) (:num)`]
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN SUBGOAL_THEN`{i|i<k:num}= 0..(k-1)`ASSUME_TAC;

REWRITE_TAC[IN_ELIM_THM;IN_NUMSEG;EXTENSION]
THEN REPLICATE_TAC (30-24)(POP_ASSUM MP_TAC)
THEN ARITH_TAC;


ASM_REWRITE_TAC[]
THEN MRESAL_TAC SUM_ADD_SPLIT[`(\i. rho_fun (norm (w (i + l MOD k))) *
      interior_angle1 (vec 0) FF (ITER i (rho_node1 FF) (w (l MOD k))))`;`0`;`0`;`k-1`][ARITH_RULE`0<=0+1/\ 0+A=A`]
THEN MRESAL_TAC SUM_ADD_SPLIT[`(\i. rho_fun (norm (ww_defor (w l) (w (i + l MOD k)) t)) *
      interior_angle1 (vec 0)
      (IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) (w (SUC i)) t)
      (:num))
      (ITER i
       (rho_node1
       (IMAGE (\i. ww_defor (w l) (w i) t,ww_defor (w l) (w (SUC i)) t)
       (:num)))
      (ww_defor (w l) (w (l MOD k)) t)))`;`0`;`0`;`k-1`][ARITH_RULE`0<=0+1/\ 0+A=A`]
THEN MATCH_MP_TAC(REAL_ARITH`a<b/\ c=d==> a+c<b+d`)
THEN REWRITE_TAC[SUM_SING_NUMSEG;ITER]
THEN MP_TAC(REAL_ARITH`t< e1 /\ e1< &1==> t< &1`)
THEN RESA_TAC
THEN MP_TAC INTERIOR_ANGLE_SAME_WW_DEFOR0
THEN RESA_TAC
THEN STRIP_TAC;

REWRITE_TAC[ARITH_RULE`0+A=A`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;is_scs_v39;convex_local_fan]
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`3<k==> ~(k= 0)`)
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN SUBGOAL_THEN`(w:num->real^3) l IN V`ASSUME_TAC;


EXPAND_TAC"V"
THEN REWRITE_TAC[IN_ELIM_THM;IMAGE]
THEN EXISTS_TAC`l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(l:num)IN(:num)`];

REPLICATE_TAC (65-33)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MP_TAC th
THEN RESA_TAC)
THEN MP_TAC Local_lemmas.LOFA_IMP_V_DIFF
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`(w:num->real^3) l`])
THEN MATCH_MP_TAC REAL_LT_RMUL
THEN STRIP_TAC;


MATCH_MP_TAC rho_fun_decreasing
THEN ASM_REWRITE_TAC[];

MRESA_TAC (GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`(w:num->real^3) (l MOD scs_k_v39 s)`];

MATCH_MP_TAC SUM_EQ
THEN REWRITE_TAC[IN_NUMSEG]
THEN REPEAT STRIP_TAC
THEN MP_TAC(ARITH_RULE`x<=k-1/\ 3< k==> x< k`)
THEN RESA_TAC
THEN MRESA_TAC(GEN_ALL INTERIOR_ANGLE_SAME_WW_DEFOR1)
[`s:scs_v39`;`t:real`;`x:num`;`FF:real^3#real^3->bool`;`w:num->real^3`;`l:num`;`k:num`]
THEN REWRITE_TAC[REAL_EQ_MUL_RCANCEL]
THEN MATCH_MP_TAC (SET_RULE`A==> A\/ B`)
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;is_scs_v39;convex_local_fan]
THEN REPEAT RESA_TAC
THEN MP_TAC(ARITH_RULE`3<k==> ~(k= 0)`)
THEN RESA_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN SUBGOAL_THEN`(w:num->real^3) l IN V`ASSUME_TAC;

EXPAND_TAC"V"
THEN REWRITE_TAC[IN_ELIM_THM;IMAGE]
THEN EXISTS_TAC`l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(l:num)IN(:num)`];

MRESAL_TAC(GEN_ALL CARD_V_EQ_SCS_K1)[`s:scs_v39`;`w:num->real^3`;`IMAGE (w:num->real^3) (:num)`;`k:num`][MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39;convex_local_fan;is_scs_v39;periodic2]
THEN MRESAL_TAC (GEN_ALL Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME)[`IMAGE (w:num->real^3) (:num)`;`IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`;`k:num`;`s:scs_v39`;`IMAGE (\i. w i,(w:num->real^3) (SUC i)) (:num)`;`(w:num->real^3) (l MOD k)`;`w:num->real^3`;`l MOD k:num`][MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39;convex_local_fan;is_scs_v39;periodic2]
THEN POP_ASSUM(fun th-> MRESA_TAC th[`x:num`] )
THEN MP_TAC(ARITH_RULE`1<=x==> 0<x`)
THEN RESA_TAC
THEN 
MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_DIS_ELMS23)
[`IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`;`IMAGE (w:num->real^3) (:num)`;`IMAGE (\i. w i,(w:num->real^3) (SUC i)) (:num)`;`(w:num->real^3) (l MOD k)`]
THEN POP_ASSUM(fun th-> MRESAL_TAC th[`0:num`;`x:num`][ITER;ww_defor] )]);;






let ODXLSTCv2 =prove_by_refinement((mk_imp(ZLZTHIC_concl, mk_imp (MHAEYJN_concl, ODXLSTCv2_concl))),
[
REPEAT STRIP_TAC
THEN REPLICATE_TAC (9-2)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC th
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
THEN ASSUME_TAC th
THEN STRIP_TAC)
THEN ABBREV_TAC`V= IMAGE (w:num->real^3) (:num)`
THEN ABBREV_TAC`E = IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`
THEN ABBREV_TAC`FF = IMAGE (\i. ((w:num->real^3) i, w (SUC i))) (:num)`
THEN MRESAL_TAC JKQEWGV2[`s:scs_v39`;`w:num->real^3`][LET_DEF;LET_END_DEF;]
THEN MRESAL_TAC (GEN_ALL WW_DEFOR_DEFORMATION)[`(w:num->real^3) l`;`V:real^3->bool`;`&1`][REAL_ARITH`&0< &1`]
THEN SUBGOAL_THEN `convex_local_fan ((V:real^3->bool),(E:(real^3->bool)->bool),FF)` ASSUME_TAC;

ASM_TAC
THEN REPLICATE_TAC 5 (STRIP_TAC)
THEN MP_TAC(ARITH_RULE`3< k==> ~(k<=3)`)
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
THEN REPEAT RESA_TAC
THEN REPLICATE_TAC (27-14) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC th
THEN ASM_REWRITE_TAC[])
THEN RESA_TAC;


SUBGOAL_THEN`(w:num->real^3) l IN ball_annulus` ASSUME_TAC;

ASM_TAC
THEN REPLICATE_TAC 5 (STRIP_TAC)
THEN MP_TAC(ARITH_RULE`3< k==> ~(k<=3)`)
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;IMAGE;IN_ELIM_THM;SUBSET]
THEN REPEAT RESA_TAC
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) l= w x)`ASSUME_TAC;

EXISTS_TAC`l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];

REPLICATE_TAC (29-11) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`(w:num->real^3) l`);

MRESA_TAC (GEN_ALL DEFORMATION_IN_BALL_ANNULUS)[`(w:num->real^3) l`]
THEN MP_TAC DEFORMATION_DIST_LE_ALL_COM
THEN RESA_TAC
THEN MP_TAC DEFORMATION_DIST_LE_BLL_COM
THEN RESA_TAC
THEN MP_TAC WW_DEFORMATION_CONVEX_LOCAL_FAN
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`k:num`;`w:num->real^3`;`l:num`])
THEN POP_ASSUM MP_TAC
THEN MATCH_MP_TAC(SET_RULE`(A==> ~(B))==>((A==>B)==> ~A)`)
THEN STRIP_TAC
THEN POP_ASSUM(fun th->
STRIP_TAC
THEN MP_TAC th)
THEN ABBREV_TAC`e1=(min (min (min (min e e') e'') e''') (&1))/ &2`
THEN MP_TAC(REAL_ARITH`e1=(min (min (min (min e e') e'') e''') (&1))/ &2 /\ &0< e/\ &0< e'/\ &0< e''/\ &0<e'''==>  &0<e1 /\ e1< e/\ e1< e'/\ e1< e''/\ e1< e'''/\ e1< &1`)
THEN RESA_TAC
THEN SUBGOAL_THEN`!t. &0 < t /\ t < e1
==> BBs_v39 s (\i. ww_defor ((w:num->real^3) l) ((w:num->real^3) i) t)` ASSUME_TAC;

REMOVE_ASSUM_TAC
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
THEN REPEAT STRIP_TAC;




ASM_REWRITE_TAC[SUBSET;IMAGE;IN_ELIM_THM;ww_defor]
THEN REPEAT RESA_TAC
THEN MP_TAC(SET_RULE`((w:num->real^3) x' = w l)\/ ~(w x' = w l)`)
THEN RESA_TAC
;


REPLICATE_TAC (44-27) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MATCH_MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC (42-27) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;





ASM_TAC
THEN REPLICATE_TAC 5 (STRIP_TAC)
THEN MP_TAC(ARITH_RULE`3< k==> ~(k<=3)`)
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;IMAGE;IN_ELIM_THM;SUBSET]
THEN REPEAT RESA_TAC
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) x'= w x)`ASSUME_TAC;

EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`]
;


REPLICATE_TAC (49-11) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`(w:num->real^3) x'`)
;



ASM_TAC
THEN REPLICATE_TAC 5 (STRIP_TAC)
THEN MP_TAC(ARITH_RULE`3< k==> ~(k<=3)`)
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;periodic;ww_defor]
THEN REPEAT RESA_TAC
;


ASM_REWRITE_TAC[ww_defor]
THEN MP_TAC(ARITH_RULE`3< k==> ~(k=0)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`(w:num->real^3) i =w l \/ ~(w i = w l)`)
THEN RESA_TAC;


MP_TAC(SET_RULE`(w:num->real^3) j =w l \/ ~(w j = w l)`)
THEN RESA_TAC;


MRESA_TAC (GEN_ALL Qknvmlb.VV_INJ)[`s:scs_v39`;`k:num`;`w:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i MOD k`;`j MOD k`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s j`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;DIST_POS_LE]);




MRESA_TAC (GEN_ALL Qknvmlb.VV_INJ)[`s:scs_v39`;`k:num`;`w:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
THEN MRESA_TAC DIVISION[`l:num`;`k:num`]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i MOD k`;`l MOD k`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s j`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;DIST_POS_LE])
THEN MP_TAC(SET_RULE`j MOD k = l MOD k==> (w:num->real^3)(j MOD k)=(w:num->real^3)(l MOD k)`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`t< e1/\ e1< e'==> t< e'`)
THEN RESA_TAC
THEN REPLICATE_TAC (77-50) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`t:real`;`j:num`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s j`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC ;




MP_TAC(SET_RULE`(w:num->real^3) j =w l \/ ~(w j = w l)`)
THEN RESA_TAC;





MRESA_TAC (GEN_ALL Qknvmlb.VV_INJ)[`s:scs_v39`;`k:num`;`w:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
THEN MRESA_TAC DIVISION[`l:num`;`k:num`]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC th[`j MOD k`;`l MOD k`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;DIST_POS_LE])
THEN MP_TAC(SET_RULE`i MOD k = l MOD k==> (w:num->real^3)(i MOD k)=(w:num->real^3)(l MOD k)`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`t< e1/\ e1< e'==> t< e'`)
THEN RESA_TAC
THEN REPLICATE_TAC (77-50) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`t:real`;`i:num`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN REMOVE_ASSUM_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC ;


ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
;




ASM_REWRITE_TAC[ww_defor]
THEN MP_TAC(ARITH_RULE`3< k==> ~(k=0)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`(w:num->real^3) i =w l \/ ~(w i = w l)`)
THEN RESA_TAC;


MP_TAC(SET_RULE`(w:num->real^3) j =w l \/ ~(w j = w l)`)
THEN RESA_TAC;




MRESA_TAC (GEN_ALL Qknvmlb.VV_INJ)[`s:scs_v39`;`k:num`;`w:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i MOD k`;`j MOD k`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s j`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`;DIST_REFL])
THEN REPLICATE_TAC (72-12) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i:num`;`j:num`])
THEN REPLICATE_TAC (3) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;







MRESA_TAC (GEN_ALL Qknvmlb.VV_INJ)[`s:scs_v39`;`k:num`;`w:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
THEN MRESA_TAC DIVISION[`l:num`;`k:num`]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i MOD k`;`l MOD k`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s j`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;DIST_POS_LE])
THEN MP_TAC(SET_RULE`j MOD k = l MOD k==> (w:num->real^3)(j MOD k)=(w:num->real^3)(l MOD k)`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`t< e1/\ e1< e''==> t< e''`)
THEN RESA_TAC
THEN REPLICATE_TAC (77-52) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`t:real`;`j:num`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s j`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC ;






MP_TAC(SET_RULE`(w:num->real^3) j =w l \/ ~(w j = w l)`)
THEN RESA_TAC;





MRESA_TAC (GEN_ALL Qknvmlb.VV_INJ)[`s:scs_v39`;`k:num`;`w:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
THEN MRESA_TAC DIVISION[`l:num`;`k:num`]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC th[`j MOD k`;`l MOD k`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;DIST_POS_LE])
THEN MP_TAC(SET_RULE`i MOD k = l MOD k==> (w:num->real^3)(i MOD k)=(w:num->real^3)(l MOD k)`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`t< e1/\ e1< e''==> t< e''`)
THEN RESA_TAC
THEN REPLICATE_TAC (77-52) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`t:real`;`i:num`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN REMOVE_ASSUM_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC ;


ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
;


ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`t< e1/\ e1< e'''/\ &0< t/\ &0< e'''==> t< e'''/\ --e'''< t`)
THEN RESA_TAC
THEN REPLICATE_TAC (44-33) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`t:real`;])
;




MP_TAC TAUSTAR_WW_DEFOR
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`k:num`;`w:num->real^3`;`l:num`])
THEN POP_ASSUM MP_TAC
THEN MATCH_MP_TAC(SET_RULE`(A==> ~(B))==>((A==>B)==> ~A)`)
THEN STRIP_TAC
THEN POP_ASSUM(fun th->
STRIP_TAC
THEN MP_TAC th)
THEN ABBREV_TAC`e2= (min e1 e'''')/ &2`
THEN MP_TAC(REAL_ARITH`e2= (min e1 e'''')/ &2 /\ &0< e1/\ &0< e''''
==> &0< e2/\ e2< e1/\ e2< e''''`)
THEN RESA_TAC
THEN REPLICATE_TAC (47-43)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`e2:real`])
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[REAL_ARITH`~(a<b)<=> b<=a`]
THEN REPLICATE_TAC (47-41)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`e2:real`])
;

])
;;


(*********CASE k = 3************)



let DEFORMATION_DIST_LE_ALL_LE3=
prove(`is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<=k/\ 
  (!i. ~(i MOD k = l MOD k) ==> scs_a_v39 s l i < dist(w l,w i)) 
==>
(!i. ~(i MOD k = l MOD k) ==> ?e. &0< e/\
(!t. &0< t/\ t< e  ==> scs_a_v39 s l i < dist((&1-t) %(w l),w i)))`,

REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MRESA_TAC th[`i:num`])
THEN MRESA_TAC(GEN_ALL DEFORMATION_DIST_LE_A)[`scs_a_v39 s l i`;`(w:num->real^3) l`;`(w:num->real^3) i`]);;


let DEFORMATION_DIST_LE_ALL_COM_LE3=
prove_by_refinement(`is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<=k/\ 
  (!i. ~(i MOD k = l MOD k) ==> scs_a_v39 s l i < dist(w l,w i)) 
==>
 ?e. &0< e/\
(!t i. &0< t/\ t< e  /\ ~(i MOD k = l MOD k) ==> scs_a_v39 s l i < dist((&1-t) %(w l),w i))`,

[REPEAT STRIP_TAC
THEN MP_TAC DEFORMATION_DIST_LE_ALL_LE3
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[RIGHT_IMP_EXISTS_THM]
THEN REWRITE_TAC[SKOLEM_THM]
THEN STRIP_TAC
THEN ABBREV_TAC`e1= inf {(e:num->real) i|  i < k/\  ~(i= l MOD k)}`
THEN EXISTS_TAC`e1:real`
THEN SUBGOAL_THEN`FINITE {(e:num->real) i | i < k /\ ~(i = l MOD k)}`ASSUME_TAC;

MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`IMAGE (e:num->real) (0..k)`
THEN STRIP_TAC;

MATCH_MP_TAC FINITE_IMAGE
THEN REWRITE_TAC[FINITE_NUMSEG];

REWRITE_TAC[SUBSET;IMAGE;IN_ELIM_THM;IN_NUMSEG]
THEN REPEAT RESA_TAC
THEN EXISTS_TAC`i:num`
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;

SUBGOAL_THEN`~({(e:num->real) i | i < k /\ ~(i = l MOD k)} = {})`ASSUME_TAC;


REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;IN_ELIM_THM]
THEN MP_TAC(SET_RULE`l MOD k=0\/ ~(0=l MOD k )`)
THEN RESA_TAC;

EXISTS_TAC`(e:num->real)1`
THEN EXISTS_TAC`1`
THEN ASM_REWRITE_TAC[ARITH_RULE`~(1=0)`]
THEN MP_TAC(ARITH_RULE`3<=k==> 1<k `)
THEN RESA_TAC;

EXISTS_TAC`(e:num->real)0`
THEN EXISTS_TAC`0`
THEN ASM_REWRITE_TAC[ARITH_RULE`~(1=0)`]
THEN MP_TAC(ARITH_RULE`3<=k==> 0<k `)
THEN RESA_TAC;

STRIP_TAC;

MRESA_TAC REAL_LT_INF_FINITE[`{(e:num->real) i|  i < k/\  ~(i= l MOD k)}`;`&0`]
THEN REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT RESA_TAC
THEN MRESA_TAC MOD_LT[`i:num`;`k:num`]
THEN REPLICATE_TAC (13-5) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i:num`]);

REPEAT STRIP_TAC
THEN MRESA_TAC REAL_LT_INF_FINITE[`{(e:num->real) i|  i < k/\  ~(i= l MOD k)}`;`t:real`]
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`e (i MOD k) IN {(e:num->real) i | i < k /\ ~(i = l MOD k)}`ASSUME_TAC;

REWRITE_TAC[IN_ELIM_THM]
THEN EXISTS_TAC`i MOD k`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`i:num`;`k:num`];

STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA1_TAC th`(e:num->real) (i MOD k)`)
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC MOD_REFL[`i:num`;`k:num`]
THEN REPLICATE_TAC (15-5) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i:num MOD k`])
THEN POP_ASSUM(fun th-> MRESA1_TAC th`t:real`)
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s l`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])]);;


let DEFORMATION_DIST_LE_BLL_LE3=
prove_by_refinement(`is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<=k/\ 
  (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i) 
==>
(!i. scs_diag k l i ==> ?e. &0< e/\
(!t. &0< t/\ t< e  ==> dist((&1-t) %(w l),w i)<scs_b_v39 s l i ) )`,

[
REPEAT STRIP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM(fun th-> STRIP_TAC
THEN MRESA_TAC th[`i:num`])
THEN SUBGOAL_THEN`dist((w:num->real^3) l,w i)< scs_b_v39 s l i`ASSUME_TAC;

MRESAL_TAC DIST_TRIANGLE[`(w:num->real^3) l`;`vec 0:real^3`;`(w:num->real^3) i`][]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;IMAGE;IN_ELIM_THM;SUBSET;ball_annulus;DIFF;cball]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) l = w x) `ASSUME_TAC;

EXISTS_TAC `l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];


SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) i = w x) `ASSUME_TAC;

EXISTS_TAC `i:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

REPLICATE_TAC (36-20) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN REPLICATE_TAC (2) (POP_ASSUM MP_TAC)
THEN MRESA_TAC th[`(w:num->real^3) i`]
THEN MRESA_TAC th[`(w:num->real^3) l`])
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[dist;VECTOR_ARITH`a- vec 0= a/\ vec 0 - a= --a`;NORM_NEG]
THEN REAL_ARITH_TAC;


EXISTS_TAC `l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) i = w x) `ASSUME_TAC;

EXISTS_TAC `i:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

REPLICATE_TAC (36-20) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN REPLICATE_TAC (2) (POP_ASSUM MP_TAC)
THEN MRESA_TAC th[`(w:num->real^3) i`]
THEN MRESA_TAC th[`(w:num->real^3) l`])
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REWRITE_TAC[dist;VECTOR_ARITH`a- vec 0= a/\ vec 0 - a= --a`;NORM_NEG]
THEN REAL_ARITH_TAC;

MRESA_TAC(GEN_ALL DEFORMATION_DIST_LE_B)[`(w:num->real^3) l`;`(w:num->real^3) i`;`scs_b_v39 s l i`;]]);;


let DEFORMATION_DIST_LE_BLL_EDGE_LE3=
prove_by_refinement(`is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<=k
==>(!i. l MOD k= SUC i MOD k 
==>
?e. &0< e/\
(!t. &0< t/\ t< e  ==> dist((&1-t) %(w l),w i)<scs_b_v39 s l i )) `,

[
REPEAT STRIP_TAC
THEN REWRITE_TAC[dist;VECTOR_ARITH`(&1 - t) % w - w1  = --(t % w-(w-w1))`;NORM_NEG]
THEN SUBGOAL_THEN`((w:num->real^3) l- w i) dot -- (w:num->real^3) l< &0` ASSUME_TAC;

MRESAL_TAC DOT_NORM[`(w:num->real^3) l- w i`;`-- (w:num->real^3) l`][VECTOR_ARITH`wl - wi + (-- wl)= --wi:real^3`;NORM_NEG]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;IMAGE;SUBSET;IN_ELIM_THM;ball_annulus;cball;DIFF;ball]
THEN REPEAT RESA_TAC
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) l = w x) `ASSUME_TAC;

EXISTS_TAC `l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) i = w x) `ASSUME_TAC;

EXISTS_TAC `i:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

REPLICATE_TAC (37-20) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`(w:num->real^3) i`]
THEN MRESA_TAC th[`(w:num->real^3) l`])
THEN REPLICATE_TAC (4) (POP_ASSUM MP_TAC)
THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (40-21) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num`;`i:num`][dist])
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1< k`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`SUC i`;`k:num`]
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MP_TAC Qknvmlb.SUC_MOD_NOT_EQ
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
THEN REPLICATE_TAC (48-14) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num MOD k`;`i MOD k:num`][dist])
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s l`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&2 <= scs_a_v39 s i l
/\ scs_a_v39 s i l <= norm (w l - (w:num->real^3)i)/\ ~(norm (w l) < &2)
==> &2<= norm (w l - (w:num->real^3)i) /\ &2<= norm (w l)`)
THEN RESA_TAC
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`&2`;`norm ((w:num->real^3) l)`][ARITH_RULE`abs (&2)= &2`;REAL_ABS_NORM]
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`&2`;`norm (w l - (w:num->real^3)i)`][ARITH_RULE`abs (&2)= &2`;REAL_ABS_NORM]
THEN ASM_TAC
THEN REWRITE_TAC[h0]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`norm ((w:num->real^3) i)`;`&2* h0`;][ARITH_RULE`abs (&2 * #1.26)= &2 * #1.26`;REAL_ABS_NORM;h0]
THEN REPLICATE_TAC (3) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;

EXISTS_TAC `l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) i = w x) `ASSUME_TAC;

EXISTS_TAC `i:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

REPLICATE_TAC (37-20) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`(w:num->real^3) i`]
THEN MRESA_TAC th[`(w:num->real^3) l`])
THEN REPLICATE_TAC (4) (POP_ASSUM MP_TAC)
THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (40-21) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num`;`i:num`][dist])
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1< k`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`SUC i`;`k:num`]
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MP_TAC Qknvmlb.SUC_MOD_NOT_EQ
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
THEN REPLICATE_TAC (48-14) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num MOD k`;`i MOD k:num`][dist])
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s l`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&2 <= scs_a_v39 s i l
/\ scs_a_v39 s i l <= norm (w l - (w:num->real^3)i)/\ ~(norm (w l) < &2)
==> &2<= norm (w l - (w:num->real^3)i) /\ &2<= norm (w l)`)
THEN RESA_TAC
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`&2`;`norm ((w:num->real^3) l)`][ARITH_RULE`abs (&2)= &2`;REAL_ABS_NORM]
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`&2`;`norm (w l - (w:num->real^3)i)`][ARITH_RULE`abs (&2)= &2`;REAL_ABS_NORM]
THEN ASM_TAC
THEN REWRITE_TAC[h0]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`norm ((w:num->real^3) i)`;`&2* h0`;][ARITH_RULE`abs (&2 * #1.26)= &2 * #1.26`;REAL_ABS_NORM;h0]
THEN REPLICATE_TAC (3) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;


POP_ASSUM MP_TAC
THEN REWRITE_TAC[DOT_RNEG;REAL_ARITH`-- a< &0 <=> a> &0`]
THEN STRIP_TAC
THEN MRESA_TAC CLOSER_POINTS_LEMMA[`(w:num->real^3) l- w i`;`(w:num->real^3) l`]
THEN EXISTS_TAC `u:real`
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC(REAL_ARITH`t< u==> t<= u`)
THEN RESA_TAC
THEN MRESA_TAC th[`t:real`])
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;IMAGE;SUBSET;IN_ELIM_THM;ball_annulus;cball;DIFF;ball]
THEN REPEAT RESA_TAC
THEN REPLICATE_TAC (40-22) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num`;`i:num`][dist])
THEN REPLICATE_TAC (3) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC]);;



let DEFORMATION_DIST_LE_BLL_EDGE2_LE3=
prove_by_refinement(
`is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<=k
==>(!i.  i MOD k= SUC l MOD k 
==>
?e. &0< e/\
(!t. &0< t/\ t< e  ==> dist((&1-t) %(w l),w i)<scs_b_v39 s l i ) )`,

[
REPEAT STRIP_TAC
THEN REWRITE_TAC[dist;VECTOR_ARITH`(&1 - t) % w - w1  = --(t % w-(w-w1))`;NORM_NEG]
THEN SUBGOAL_THEN`((w:num->real^3) l- w i) dot -- (w:num->real^3) l< &0` ASSUME_TAC;

MRESAL_TAC DOT_NORM[`(w:num->real^3) l- w i`;`-- (w:num->real^3) l`][VECTOR_ARITH`wl - wi + (-- wl)= --wi:real^3`;NORM_NEG]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;IMAGE;SUBSET;IN_ELIM_THM;ball_annulus;cball;DIFF;ball]
THEN REPEAT RESA_TAC
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) l = w x) `ASSUME_TAC;

EXISTS_TAC `l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) i = w x) `ASSUME_TAC;

EXISTS_TAC `i:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

REPLICATE_TAC (37-20) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`(w:num->real^3) i`]
THEN MRESA_TAC th[`(w:num->real^3) l`])
THEN REPLICATE_TAC (4) (POP_ASSUM MP_TAC)
THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (40-21) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num`;`i:num`][dist])
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1< k`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`l:num`;`k:num`]
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MP_TAC Qknvmlb.SUC_MOD_NOT_EQ
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`l:num`)
THEN REPLICATE_TAC (48-14) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num MOD k`;`i MOD k:num`][dist])
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s l`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&2 <= scs_a_v39 s i l
/\ scs_a_v39 s i l <= norm (w l - (w:num->real^3)i)/\ ~(norm (w l) < &2)
==> &2<= norm (w l - (w:num->real^3)i) /\ &2<= norm (w l)`)
THEN RESA_TAC
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`&2`;`norm ((w:num->real^3) l)`][ARITH_RULE`abs (&2)= &2`;REAL_ABS_NORM]
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`&2`;`norm (w l - (w:num->real^3)i)`][ARITH_RULE`abs (&2)= &2`;REAL_ABS_NORM]
THEN ASM_TAC
THEN REWRITE_TAC[h0]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`norm ((w:num->real^3) i)`;`&2* h0`;][ARITH_RULE`abs (&2 * #1.26)= &2 * #1.26`;REAL_ABS_NORM;h0]
THEN REPLICATE_TAC (3) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;


EXISTS_TAC `l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) i = w x) `ASSUME_TAC;

EXISTS_TAC `i:num`
THEN ASM_REWRITE_TAC[SET_RULE`(x:num)IN (:num)`];

REPLICATE_TAC (37-20) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA_TAC th[`(w:num->real^3) i`]
THEN MRESA_TAC th[`(w:num->real^3) l`])
THEN REPLICATE_TAC (4) (POP_ASSUM MP_TAC)
THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG]
THEN REPEAT STRIP_TAC
THEN REPLICATE_TAC (40-21) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num`;`i:num`][dist])
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1< k`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`l:num`;`k:num`]
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MP_TAC Qknvmlb.SUC_MOD_NOT_EQ
THEN RESA_TAC
THEN POP_ASSUM(fun th-> MRESA1_TAC th`l:num`)
THEN REPLICATE_TAC (48-14) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num MOD k`;`i MOD k:num`][dist])
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s l`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`SUC i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
THEN STRIP_TAC
THEN MP_TAC(REAL_ARITH`&2 <= scs_a_v39 s i l
/\ scs_a_v39 s i l <= norm (w l - (w:num->real^3)i)/\ ~(norm (w l) < &2)
==> &2<= norm (w l - (w:num->real^3)i) /\ &2<= norm (w l)`)
THEN RESA_TAC
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`&2`;`norm ((w:num->real^3) l)`][ARITH_RULE`abs (&2)= &2`;REAL_ABS_NORM]
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`&2`;`norm (w l - (w:num->real^3)i)`][ARITH_RULE`abs (&2)= &2`;REAL_ABS_NORM]
THEN ASM_TAC
THEN REWRITE_TAC[h0]
THEN REPEAT RESA_TAC
THEN MRESAL_TAC REAL_LE_SQUARE_ABS[`norm ((w:num->real^3) i)`;`&2* h0`;][ARITH_RULE`abs (&2 * #1.26)= &2 * #1.26`;REAL_ABS_NORM;h0]
THEN REPLICATE_TAC (3) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;

POP_ASSUM MP_TAC
THEN REWRITE_TAC[DOT_RNEG;REAL_ARITH`-- a< &0 <=> a> &0`]
THEN STRIP_TAC
THEN MRESA_TAC CLOSER_POINTS_LEMMA[`(w:num->real^3) l- w i`;`(w:num->real^3) l`]
THEN EXISTS_TAC `u:real`
THEN ASM_REWRITE_TAC[]
THEN GEN_TAC
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MP_TAC(REAL_ARITH`t< u==> t<= u`)
THEN RESA_TAC
THEN MRESA_TAC th[`t:real`])
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2;IMAGE;SUBSET;IN_ELIM_THM;ball_annulus;cball;DIFF;ball]
THEN REPEAT RESA_TAC
THEN REPLICATE_TAC (40-22) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESAL_TAC th[`l:num`;`i:num`][dist])
THEN REPLICATE_TAC (3) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC]);;


let DEFORMATION_DIST_LE_BLL_PRIME_LE3=
prove_by_refinement(`is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<=k/\ 
  (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i) 
==>
(!i. ~(i MOD k = l MOD k) ==> ?e. &0< e/\
(!t. &0< t/\ t< e  ==> dist((&1-t) %(w l),w i)<scs_b_v39 s l i ) )`,

[
REPEAT STRIP_TAC
THEN MP_TAC(SET_RULE`l MOD k = SUC i MOD k \/ ~(SUC i MOD k= l MOD k)`)
THEN RESA_TAC;

MP_TAC DEFORMATION_DIST_LE_BLL_EDGE_LE3
THEN RESA_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_REWRITE_TAC[];

MP_TAC(SET_RULE`i MOD k= SUC l MOD k  \/ ~(i MOD k= SUC l MOD k )`)
THEN RESA_TAC;

MP_TAC DEFORMATION_DIST_LE_BLL_EDGE2_LE3
THEN RESA_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_REWRITE_TAC[];

MP_TAC DEFORMATION_DIST_LE_BLL_LE3
THEN RESA_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_REWRITE_TAC[scs_diag]]);;

let DEFORMATION_DIST_LE_BLL_COM_LE3=
prove_by_refinement(`is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3<=k/\ 
  (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i) 
==>
 ?e. &0< e/\
(!t i. &0< t/\ t< e  /\ ~(i MOD k = l MOD k) ==> dist((&1-t) %(w l),w i)< scs_b_v39 s l i) `,

[REPEAT STRIP_TAC
THEN MP_TAC DEFORMATION_DIST_LE_BLL_PRIME_LE3
THEN RESA_TAC
THEN POP_ASSUM MP_TAC
THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[RIGHT_IMP_EXISTS_THM]
THEN REWRITE_TAC[SKOLEM_THM]
THEN STRIP_TAC
THEN ABBREV_TAC`e1= inf {(e:num->real) i|  i < k/\  ~(i= l MOD k)}`
THEN EXISTS_TAC`e1:real`
THEN SUBGOAL_THEN`FINITE {(e:num->real) i | i < k /\ ~(i = l MOD k)}`ASSUME_TAC;


MATCH_MP_TAC FINITE_SUBSET
THEN EXISTS_TAC`IMAGE (e:num->real) (0..k)`
THEN STRIP_TAC;

MATCH_MP_TAC FINITE_IMAGE
THEN REWRITE_TAC[FINITE_NUMSEG];

REWRITE_TAC[SUBSET;IMAGE;IN_ELIM_THM;IN_NUMSEG]
THEN REPEAT RESA_TAC
THEN EXISTS_TAC`i:num`
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN POP_ASSUM MP_TAC
THEN ARITH_TAC;

SUBGOAL_THEN`~({(e:num->real) i | i < k /\ ~(i = l MOD k)} = {})`ASSUME_TAC;

REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;IN_ELIM_THM]
THEN MP_TAC(SET_RULE`l MOD k=0\/ ~(0=l MOD k )`)
THEN RESA_TAC;


EXISTS_TAC`(e:num->real)1`
THEN EXISTS_TAC`1`
THEN ASM_REWRITE_TAC[ARITH_RULE`~(1=0)`]
THEN MP_TAC(ARITH_RULE`3<=k==> 1<k `)
THEN RESA_TAC;


EXISTS_TAC`(e:num->real)0`
THEN EXISTS_TAC`0`
THEN ASM_REWRITE_TAC[ARITH_RULE`~(1=0)`]
THEN MP_TAC(ARITH_RULE`3<=k==> 0<k `)
THEN RESA_TAC;


STRIP_TAC;

MRESA_TAC REAL_LT_INF_FINITE[`{(e:num->real) i|  i < k/\  ~(i= l MOD k)}`;`&0`]
THEN REWRITE_TAC[IN_ELIM_THM]
THEN REPEAT RESA_TAC
THEN MRESA_TAC MOD_LT[`i:num`;`k:num`]
THEN REPLICATE_TAC (13-5) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i:num`]);

REPEAT STRIP_TAC
THEN MRESA_TAC REAL_LT_INF_FINITE[`{(e:num->real) i|  i < k/\  ~(i= l MOD k)}`;`t:real`]
THEN POP_ASSUM MP_TAC
THEN SUBGOAL_THEN`e (i MOD k) IN {(e:num->real) i | i < k /\ ~(i = l MOD k)}`ASSUME_TAC;

REWRITE_TAC[IN_ELIM_THM]
THEN EXISTS_TAC`i MOD k`
THEN ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC DIVISION[`i:num`;`k:num`];

STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA1_TAC th`(e:num->real) (i MOD k)`)
THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`)
THEN RESA_TAC
THEN MRESA_TAC MOD_REFL[`i:num`;`k:num`]
THEN REPLICATE_TAC (15-5) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i:num MOD k`])
THEN POP_ASSUM(fun th-> MRESA1_TAC th`t:real`)
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s l`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])]);;

let DIHV_SPECIAL_SCALE1 = 
prove
 (`!a v w1 w2:real^N.
        (&0< a )
        ==> dihV (vec 0) w1 (a % v)  w2 = dihV (vec 0) w1 v  w2`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[DIHV; VECTOR_SUB_RZERO] THEN
  CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
  REWRITE_TAC[DOT_LMUL; DOT_RMUL; GSYM VECTOR_MUL_ASSOC] THEN
  REWRITE_TAC[VECTOR_ARITH `c % a % x - a % b  % y:real^N =
                            (a ) % (c% x - b % y)`] THEN
  REWRITE_TAC[angle; VECTOR_SUB_RZERO] THEN
  REWRITE_TAC[VECTOR_ANGLE_LMUL; VECTOR_ANGLE_RMUL] THEN
  ASM_REWRITE_TAC[REAL_LE_SQUARE; REAL_ENTIRE]
  THEN MP_TAC(REAL_ARITH`&0< a==> ~(a= &0) /\ &0<= a`)
  THEN RESA_TAC);;


let DIHV_SPECIAL_SCALE2 = 
prove (`!a v w1 w2:real^N.
        (&0< a )
        ==> dihV (vec 0) w1 w2 (a % v)  = dihV (vec 0) w1  w2 v `,

  REPEAT STRIP_TAC THEN REWRITE_TAC[DIHV; VECTOR_SUB_RZERO] THEN
  CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
  REWRITE_TAC[DOT_LMUL; DOT_RMUL; GSYM VECTOR_MUL_ASSOC] THEN
  REWRITE_TAC[VECTOR_ARITH `c % a % x - a % b  % y:real^N =
                            (a ) % (c% x - b % y)`] THEN
  REWRITE_TAC[angle; VECTOR_SUB_RZERO] THEN
  REWRITE_TAC[VECTOR_ANGLE_LMUL; VECTOR_ANGLE_RMUL] THEN
  ASM_REWRITE_TAC[REAL_LE_SQUARE; REAL_ENTIRE]
  THEN MP_TAC(REAL_ARITH`&0< a==> ~(a= &0) /\ &0<= a`)
  THEN RESA_TAC);;


let DEFORMATION_BB_WW_DEFOR_LE3=
prove_by_refinement(
`!s k w l.
  is_scs_v39 s /\
  MMs_v39 s w /\
  scs_k_v39 s =k/\
 3=k/\ 
  (!i. scs_diag k l i ==> &4 * h0 < scs_b_v39 s l i) /\
  ~(&2 = norm (w l)) /\
  (!i. ~(i MOD k = l MOD k) ==> scs_a_v39 s l i < dist(w l,w i)) /\
  (!i. ~(scs_J_v39 s l i)) /\
  (!V E v.
     V = IMAGE w (:num) /\
      E = IMAGE (\i. {w i, w (SUC i)}) (:num) ==>
      ~(lunar (v,(w l)) V E )) ==> 
(?e1. &0< e1/\(!t. &0 < t /\ t < e1
==> BBs_v39 s (\i. ww_defor ((w:num->real^3) l) ((w:num->real^3) i) t)) )`,

[
REPEAT STRIP_TAC
THEN REPLICATE_TAC (9-2)(POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN POP_ASSUM MP_TAC
THEN MP_TAC th
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
THEN ASSUME_TAC th
THEN STRIP_TAC)
THEN ABBREV_TAC`V= IMAGE (w:num->real^3) (:num)`
THEN ABBREV_TAC`E = IMAGE (\i. {(w:num->real^3) i, w (SUC i)}) (:num)`
THEN ABBREV_TAC`FF = IMAGE (\i. ((w:num->real^3) i, w (SUC i))) (:num)`
THEN MRESAL_TAC JKQEWGV2[`s:scs_v39`;`w:num->real^3`][LET_DEF;LET_END_DEF;]
THEN MRESAL_TAC (GEN_ALL WW_DEFOR_DEFORMATION)[`(w:num->real^3) l`;`V:real^3->bool`;`&1`][REAL_ARITH`&0< &1`]
THEN SUBGOAL_THEN`(w:num->real^3) l IN ball_annulus` ASSUME_TAC;

ASM_TAC
THEN REPLICATE_TAC 5 (STRIP_TAC)
THEN MP_TAC(ARITH_RULE`3= k==> (k<=3)`)
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;IMAGE;IN_ELIM_THM;SUBSET]
THEN REPEAT RESA_TAC
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) l= w x)`ASSUME_TAC;

EXISTS_TAC`l:num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];

REPLICATE_TAC (25-9) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`(w:num->real^3) l`);

MP_TAC(ARITH_RULE`3=k==> 3<=k`)
THEN RESA_TAC
THEN MRESA_TAC (GEN_ALL DEFORMATION_IN_BALL_ANNULUS)[`(w:num->real^3) l`]
THEN MP_TAC DEFORMATION_DIST_LE_ALL_COM_LE3
THEN RESA_TAC
THEN MP_TAC DEFORMATION_DIST_LE_BLL_COM_LE3
THEN RESA_TAC
THEN ABBREV_TAC`e1=(min (min (min e e') e'')(&1))/ &2`
THEN MP_TAC(REAL_ARITH`e1=(min (min (min e e') e'') (&1))/ &2 /\ &0< e /\ &0< e'/\ &0< e''==>  &0<e1 /\ e1< e/\ e1< e'/\ e1< e''/\ e1< &1`)
THEN RESA_TAC
THEN SUBGOAL_THEN`!t. &0 < t /\ t < e1
==> BBs_v39 s (\i. ww_defor ((w:num->real^3) l) ((w:num->real^3) i) t)` ASSUME_TAC;


REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39]
THEN REPEAT STRIP_TAC;


ASM_REWRITE_TAC[SUBSET;IMAGE;IN_ELIM_THM;ww_defor]
THEN REPEAT RESA_TAC
THEN MP_TAC(SET_RULE`((w:num->real^3) x' = w l)\/ ~(w x' = w l)`)
THEN RESA_TAC;


REPLICATE_TAC (40-25) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MATCH_MP_TAC th)
THEN ASM_REWRITE_TAC[]
THEN REPLICATE_TAC (44-27) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;


ASM_TAC
THEN REPLICATE_TAC 5 (STRIP_TAC)
THEN MP_TAC(ARITH_RULE`3= k==> (k<=3)`)
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;IMAGE;IN_ELIM_THM;SUBSET]
THEN REPEAT RESA_TAC
THEN SUBGOAL_THEN`(?x. x IN (:num) /\ (w:num->real^3) x'= w x)`ASSUME_TAC;

EXISTS_TAC`x':num`
THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`];


REPLICATE_TAC (43-9) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
THEN MRESA1_TAC th`(w:num->real^3) x'`);

ASM_TAC
THEN REPLICATE_TAC 5 (STRIP_TAC)
THEN MP_TAC(ARITH_RULE`3< k==> ~(k<=3)`)
THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;periodic;ww_defor]
THEN REPEAT RESA_TAC;


ASM_REWRITE_TAC[ww_defor]
THEN MP_TAC(ARITH_RULE`3= k==> ~(k=0)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`(w:num->real^3) i =w l \/ ~(w i = w l)`)
THEN RESA_TAC;


MP_TAC(SET_RULE`(w:num->real^3) j =w l \/ ~(w j = w l)`)
THEN RESA_TAC;



MRESA_TAC (GEN_ALL Qknvmlb.VV_INJ)[`s:scs_v39`;`k:num`;`w:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i MOD k`;`j MOD k`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s j`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;DIST_POS_LE]);


MRESA_TAC (GEN_ALL Qknvmlb.VV_INJ)[`s:scs_v39`;`k:num`;`w:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
THEN MRESA_TAC DIVISION[`l:num`;`k:num`]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i MOD k`;`l MOD k`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s j`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;DIST_POS_LE])
THEN MP_TAC(SET_RULE`j MOD k = l MOD k==> (w:num->real^3)(j MOD k)=(w:num->real^3)(l MOD k)`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`t< e1/\ e1< e'==> t< e'`)
THEN RESA_TAC
THEN REPLICATE_TAC (72-47) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`t:real`;`j:num`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s j`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC ;


MP_TAC(SET_RULE`(w:num->real^3) j =w l \/ ~(w j = w l)`)
THEN RESA_TAC;

MRESA_TAC (GEN_ALL Qknvmlb.VV_INJ)[`s:scs_v39`;`k:num`;`w:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
THEN MRESA_TAC DIVISION[`l:num`;`k:num`]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC th[`j MOD k`;`l MOD k`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;DIST_POS_LE])
THEN MP_TAC(SET_RULE`i MOD k = l MOD k==> (w:num->real^3)(i MOD k)=(w:num->real^3)(l MOD k)`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`t< e1/\ e1< e'==> t< e'`)
THEN RESA_TAC
THEN REPLICATE_TAC (72-47) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`t:real`;`i:num`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN REMOVE_ASSUM_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC ;

ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC;

ASM_REWRITE_TAC[ww_defor]
THEN MP_TAC(ARITH_RULE`3= k==> ~(k=0)`)
THEN RESA_TAC
THEN MP_TAC(SET_RULE`(w:num->real^3) i =w l \/ ~(w i = w l)`)
THEN RESA_TAC;

MP_TAC(SET_RULE`(w:num->real^3) j =w l \/ ~(w j = w l)`)
THEN RESA_TAC;

MRESA_TAC (GEN_ALL Qknvmlb.VV_INJ)[`s:scs_v39`;`k:num`;`w:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i MOD k`;`j MOD k`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s j`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD k)`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`;DIST_REFL]);

REPLICATE_TAC (69-12) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i:num`;`j:num`])
THEN REPLICATE_TAC (3) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;

REPLICATE_TAC (70-12) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`i:num`;`j:num`])
THEN REPLICATE_TAC (3) (POP_ASSUM MP_TAC)
THEN REAL_ARITH_TAC;

MRESA_TAC (GEN_ALL Qknvmlb.VV_INJ)[`s:scs_v39`;`k:num`;`w:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
THEN MRESA_TAC DIVISION[`l:num`;`k:num`]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC th[`i MOD k`;`l MOD k`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s j`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;DIST_POS_LE])
THEN MP_TAC(SET_RULE`j MOD k = l MOD k==> (w:num->real^3)(j MOD k)=(w:num->real^3)(l MOD k)`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`t< e1/\ e1< e''==> t< e''`)
THEN RESA_TAC
THEN REPLICATE_TAC (72-49) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`t:real`;`j:num`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s j`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN REMOVE_ASSUM_TAC
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC ;

MP_TAC(SET_RULE`(w:num->real^3) j =w l \/ ~(w j = w l)`)
THEN RESA_TAC;

MRESA_TAC (GEN_ALL Qknvmlb.VV_INJ)[`s:scs_v39`;`k:num`;`w:num->real^3`]
THEN ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC
THEN POP_ASSUM MP_TAC
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`w:num->real^3`][ARITH_RULE`~(4=0)`;]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`]
THEN MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
THEN MRESA_TAC DIVISION[`l:num`;`k:num`]
THEN STRIP_TAC
THEN POP_ASSUM (fun th-> MRESA_TAC th[`j MOD k`;`l MOD k`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`j:num`[ARITH_RULE`4 MOD 4=0`])
THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;DIST_POS_LE])
THEN MP_TAC(SET_RULE`i MOD k = l MOD k==> (w:num->real^3)(i MOD k)=(w:num->real^3)(l MOD k)`)
THEN RESA_TAC
THEN MP_TAC(REAL_ARITH`t< e1/\ e1< e''==> t< e''`)
THEN RESA_TAC
THEN REPLICATE_TAC (72-49) (POP_ASSUM MP_TAC)
THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
THEN MRESA_TAC th[`t:real`;`i:num`])
THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][ARITH_RULE`~(4=0)`;periodic]
THEN POP_ASSUM (fun th-> MRESAL1_TAC th`l:num`[ARITH_RULE`4 MOD 4=0`])
THEN REMOVE_ASSUM_TAC
THEN ONCE_REWRITE_TAC[DIST_SYM]
THEN POP_ASSUM MP_TAC
THEN REAL_ARITH_TAC ;

ASM_TAC
THEN REWRITE_TAC[MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBprime_v39;BBs_v39;is_scs_v39;periodic2]
THEN REPEAT RESA_TAC;

ASM_REWRITE_TAC[]
THEN MP_TAC(ARITH_RULE`3=k==> (k<=3)`)
THEN RESA_TAC;


STRIP_TAC
THEN REMOVE_ASSUM_TAC
THEN EXISTS_TAC`e1:real`
THEN ASM_REWRITE_TAC[]]);;


 end;;


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