(* ========================================================================== *)
(* 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) *)