(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2010-02-09                                                           *)
(* ========================================================================== *)



flyspeck_needs "general/sphere.hl";;


module Fan  = struct


(*
# use "/home/truong/Desktop/googlecode/hol_light/hol.ml";;
needs "/home/truong/Desktop/googlecode/hol_light/Multivariate/flyspeck.ml";;
needs "/home/truong/Desktop/googlecode/flyspeck/text_formalization/general/sphere.hl";;
*)

		
		
open Sphere;;
open Fan_defs;;
open Hypermap;;


let ASM_TAC=REPEAT(POP_ASSUM MP_TAC);;
let RED_TAC=ASM_REWRITE_TAC[] THEN DISCH_TAC;;
let RES_TAC=ASM_REWRITE_TAC[] THEN STRIP_TAC;;
let REDA_TAC=ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[];;
let RESA_TAC=ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[];;
let REDAL_TAC (th: thm list) =ASM_REWRITE_TAC th THEN DISCH_TAC THEN ASM_REWRITE_TAC th;;
let RESAL_TAC (th: thm list) = ASM_REWRITE_TAC th THEN STRIP_TAC THEN ASM_REWRITE_TAC th;;
let REMOVE_ASSUM_TAC=POP_ASSUM(fun th-> REWRITE_TAC[]);;
let SYM_ASSUM_TAC=POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]);;
let SYM_ASSUM1_TAC=POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]THEN ASSUME_TAC(th));;
let RESP_TAC=ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th->REWRITE_TAC[th]);;
let RESPL_TAC (th: thm list) =ASM_REWRITE_TAC th THEN STRIP_TAC THEN POP_ASSUM(fun th->REWRITE_TAC [th]);;
let REDUCE_ARITH_TAC=REWRITE_TAC[REAL_ARITH`&0 * a= &0`; REAL_ARITH`a * &0 = &0`; REAL_ARITH`a + &0 = a`; 
REAL_ARITH`a- &0 =a`;REAL_ARITH`&0 +a =a`;REAL_ARITH`&1 * a =a`;REAL_ARITH`a * &1 =a`;REAL_ARITH`(A+B)-B=A`];;
let REDUCE_VECTOR_TAC=REWRITE_TAC[VECTOR_ARITH`&0 % a= vec 0`; VECTOR_ARITH`a % vec 0= vec 0`;VECTOR_ARITH`a + vec 0 = a`; 
VECTOR_ARITH`vec 0 +a =a`; VECTOR_ARITH`a- vec 0 =a`;VECTOR_ARITH`&1 % a =a`;VECTOR_ARITH`a- b =vec 0<=> a=b`];;

let MRESA_TAC th1 (th: term list) = MP_TAC(ISPECL th th1) THEN RESA_TAC;;
let MRESA1_TAC th1 th = MP_TAC(ISPEC th th1) THEN RESA_TAC;;

let MRESAL_TAC th1 (th: term list) (th2: thm list) =MP_TAC(ISPECL th th1) THEN ASM_REWRITE_TAC th2 THEN STRIP_TAC THEN ASM_REWRITE_TAC th2;;

let MRESAL1_TAC th1 th (th2: thm list) =MP_TAC(ISPEC th th1) THEN ASM_REWRITE_TAC th2 THEN STRIP_TAC THEN ASM_REWRITE_TAC th2;;

let ASM_SET_TAC l = 
    (TRY(POP_ASSUM_LIST(MP_TAC o end_itlist CONJ))) THEN SET_TAC l;;



let graph = new_definition `graph E <=> (!e. E e ==> (e HAS_SIZE 2))`;;
let fan1 = new_definition`fan1(x,V,E):bool <=>  FINITE V /\ ~(V SUBSET {}) `;;
let fan2 = new_definition`fan2(x,V,E):bool <=>   ~(x IN V)`;;
let fan3=new_definition`fan3(x,V,E):bool <=> (!v. (v IN V) ==> cyclic_set {w | {v,w} IN E } x v)`;;
let fan4 = new_definition`fan4(x,V,E):bool<=>  (!e. (e IN E) ==> (aff_gt {x} e  INTER V={}))`;;
let fan5 = new_definition`fan5(x,V,E):bool<=> (!e f. (e IN E)/\ (f IN E) /\ ~(e=f) ==> (aff_gt {x} e INTER aff_gt {x} f ={}))`;;
(* Deprecated, 2011-08-01, thales let fan = new_definition`fan(x,V,E)<=> ((UNIONS E) SUBSET V) /\ graph(E)/\ fan1(x,V,E)/\ fan2(x,V,E)/\ fan3(x,V,E)/\ fan4 (x,V,E) /\ fan5(x,V,E)`;; *)
let base_point_fan=new_definition`base_point_fan (x,V,E)=x`;;
let set_of_edge=new_definition`set_of_edge v V E={w|{v,w} IN E /\ w IN V}`;;
let fan6= new_definition`fan6(x,V,E):bool<=>(!e. (e IN E) ==> ~(collinear ({x} UNION e)))`;;
let fan7= new_definition`fan7(x,V,E):bool<=> (!e1 e2. (e1 IN E UNION {{v}| v IN V}) /\ (e2 IN E UNION {{v}| v IN V})
==> ((aff_ge {x} e1) INTER (aff_ge {x} e2) = aff_ge {x} (e1 INTER e2)))`;;
let FAN=new_definition`FAN(x,V,E) <=> ((UNIONS E) SUBSET V) /\ graph(E) /\ fan1(x,V,E) /\ fan2(x,V,E)/\
fan6(x,V,E)/\ fan7(x,V,E)`;;
(* ************************************************* *) (* Invariance theorems *)
let GRAPH = 
prove (`!E. graph E <=> !e. e IN E ==> e HAS_SIZE 2`,
REWRITE_TAC[graph; IN]);;
let CYCLIC_SET = 
prove (`cyclic_set W v w <=> ~(v = w) /\ FINITE W /\ (!p q h. p IN W /\ q IN W /\ p - q = h % (v - w) ==> p = q) /\ W INTER affine hull {v, w} = {}`,
REWRITE_TAC[cyclic_set; IN; VECTOR_ARITH `p - q:real^N = r <=> p = q + r`]);;
let CYCLIC_SET_TRANSLATION_EQ = 
prove (`!a:real^N s x y. cyclic_set (IMAGE (\x. a + x) s) (a + x) (a + y) <=> cyclic_set s x y`,
REWRITE_TAC[CYCLIC_SET] THEN GEOM_TRANSLATE_TAC[]);;
let CYCLIC_SET_LINEAR_IMAGE = 
prove (`!f:real^M->real^N s x y. linear f /\ (!x y. f x = f y ==> x = y) ==> (cyclic_set (IMAGE f s) (f x) (f y) <=> cyclic_set s x y)`,
GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV) [CYCLIC_SET; RIGHT_FORALL_IMP_THM; IMP_CONJ; FORALL_IN_IMAGE] THEN GEOM_TRANSFORM_TAC[]);;
add_translation_invariants [CYCLIC_SET_TRANSLATION_EQ];; add_linear_invariants [CYCLIC_SET_LINEAR_IMAGE];;
let GRAPH_TRANSLATION_EQ = 
prove (`!a:real^N E. graph (IMAGE (IMAGE (\x. a + x)) E) <=> graph E`,
REWRITE_TAC[GRAPH] THEN GEOM_TRANSLATE_TAC[]);;
let GRAPH_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N E. linear f /\ (!x y. f x = f y ==> x = y) ==> (graph(IMAGE (IMAGE f) E) <=> graph E)`,
REWRITE_TAC[GRAPH] THEN GEOM_TRANSFORM_TAC[]);;
let FAN1_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan1(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan1(x,V,E)`,
REWRITE_TAC[fan1] THEN GEOM_TRANSLATE_TAC[]);;
let FAN1_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan1(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan1(x,V,E))`,
REWRITE_TAC[fan1] THEN GEOM_TRANSFORM_TAC[]);;
let FAN2_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan2(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan2(x,V,E)`,
REWRITE_TAC[fan2] THEN GEOM_TRANSLATE_TAC[]);;
let FAN2_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan2(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan2(x,V,E))`,
REWRITE_TAC[fan2] THEN GEOM_TRANSFORM_TAC[]);;
let FAN3_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan3(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan3(x,V,E)`,
REWRITE_TAC[fan3] THEN GEOM_TRANSLATE_TAC[]);;
let FAN3_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan3(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan3(x,V,E))`,
let lemma = prove
   (`{w | {a,w} IN IMAGE (IMAGE f) s} =
     IMAGE f {w |w| {a,f w} IN IMAGE (IMAGE f) s}`,
    MATCH_MP_TAC(SET_RULE
     `(!y. P y ==> ?x. y = f x) ==> {w | P w} = IMAGE f {w | P(f w)}`) THEN
    REWRITE_TAC[IN_IMAGE; EXTENSION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN
    MESON_TAC[]) in
  REWRITE_TAC[fan3; FORALL_IN_IMAGE; lemma] THEN GEOM_TRANSFORM_TAC[]);;
let FAN4_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan4(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan4(x,V,E)`,
REWRITE_TAC[fan4] THEN GEOM_TRANSLATE_TAC[]);;
let FAN4_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan4(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan4(x,V,E))`,
REWRITE_TAC[fan4] THEN GEOM_TRANSFORM_TAC[]);;
let FAN5_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan5(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan5(x,V,E)`,
REWRITE_TAC[fan5] THEN GEOM_TRANSLATE_TAC[]);;
let FAN5_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan5(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan5(x,V,E))`,
GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV) [fan5; IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN GEOM_TRANSFORM_TAC[]);;
let FAN6_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan6(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan6(x,V,E)`,
REWRITE_TAC[fan6] THEN GEOM_TRANSLATE_TAC[]);;
let FAN6_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan6(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan6(x,V,E))`,
REWRITE_TAC[fan6] THEN GEOM_TRANSFORM_TAC[]);;
let FAN7_TRANSLATION_EQ = 
prove (`!a:real^N x V E. fan7(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> fan7(x,V,E)`,
REWRITE_TAC[fan7] THEN REWRITE_TAC[SET_RULE `e IN s UNION {f x | t x} <=> e IN s \/ ?x. t x /\ e = f x`] THEN GEOM_TRANSLATE_TAC[]);;
let FAN7_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (fan7(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> fan7(x,V,E))`,
REWRITE_TAC[fan7; IN_UNION] THEN REWRITE_TAC[LEFT_OR_DISTRIB; RIGHT_OR_DISTRIB; TAUT `a \/ b ==> c <=> (a ==> c) /\ (b ==> c)`] THEN GEN_REWRITE_TAC (funpow 4 BINDER_CONV o RAND_CONV o TOP_DEPTH_CONV) [FORALL_AND_THM; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN REWRITE_TAC[FORALL_IN_GSPEC] THEN REWRITE_TAC[IMP_IMP] THEN GEOM_TRANSFORM_TAC[]);;
add_translation_invariants [GRAPH_TRANSLATION_EQ; FAN1_TRANSLATION_EQ; FAN2_TRANSLATION_EQ; FAN3_TRANSLATION_EQ; FAN4_TRANSLATION_EQ; FAN5_TRANSLATION_EQ; FAN6_TRANSLATION_EQ; FAN7_TRANSLATION_EQ];; add_linear_invariants [GRAPH_LINEAR_IMAGE_EQ; FAN1_LINEAR_IMAGE_EQ; FAN2_LINEAR_IMAGE_EQ; FAN3_LINEAR_IMAGE_EQ; FAN4_LINEAR_IMAGE_EQ; FAN5_LINEAR_IMAGE_EQ; FAN6_LINEAR_IMAGE_EQ; FAN7_LINEAR_IMAGE_EQ];;
let FAN_TRANSLATION_EQ = 
prove (`!a:real^N x V E. FAN(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) <=> FAN(x,V,E)`,
REWRITE_TAC[FAN] THEN GEOM_TRANSLATE_TAC[]);;
let FAN_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> (FAN(f x,IMAGE f V,IMAGE (IMAGE f) E) <=> FAN(x,V,E))`,
REWRITE_TAC[FAN] THEN GEOM_TRANSFORM_TAC[]);;
add_translation_invariants [FAN_TRANSLATION_EQ];; add_linear_invariants [FAN_LINEAR_IMAGE_EQ];;
let BASE_POINT_FAN_TRANSLATION_EQ = 
prove (`!a x V E. base_point_fan(a + x,IMAGE (\x. a + x) V,IMAGE (IMAGE (\x. a + x)) E) = a + base_point_fan(x,V,E)`,
REWRITE_TAC[base_point_fan]);;
let BASE_POINT_FAN_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f ==> base_point_fan(f x,IMAGE f V,IMAGE (IMAGE f) E) = f(base_point_fan(x,V,E))`,
REWRITE_TAC[base_point_fan]);;
let SET_OF_EDGE_TRANSLATION_EQ = 
prove (`!a:real^N x V E. set_of_edge (a + x) (IMAGE (\x. a + x) V) (IMAGE (IMAGE (\x. a + x)) E) = IMAGE (\x. a + x) (set_of_edge x V E)`,
REWRITE_TAC[set_of_edge] THEN GEOM_TRANSLATE_TAC[]);;
let SET_OF_EDGE_LINEAR_IMAGE_EQ = 
prove (`!f:real^M->real^N x V E. linear f /\ (!x y. f x = f y ==> x = y) ==> set_of_edge (f x) (IMAGE f V) (IMAGE (IMAGE f) E) = IMAGE f (set_of_edge x V E)`,
let lemma = prove
   (`{w | {a,w} IN IMAGE (IMAGE f) s /\ P w} =
     {f w |w| {a,f w} IN IMAGE (IMAGE f) s /\ P(f w)}`,
    MATCH_MP_TAC(SET_RULE
     `(!y. P y ==> ?x. y = f x) ==> {w | P w} = {f w |w| P(f w)}`) THEN
    REWRITE_TAC[IN_IMAGE; EXTENSION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN
    MESON_TAC[]) in
  REWRITE_TAC[set_of_edge; lemma] THEN
  GEOM_TRANSFORM_TAC[] THEN SET_TAC[]);;
add_translation_invariants [BASE_POINT_FAN_TRANSLATION_EQ; SET_OF_EDGE_TRANSLATION_EQ];; add_linear_invariants [BASE_POINT_FAN_LINEAR_IMAGE_EQ; SET_OF_EDGE_LINEAR_IMAGE_EQ];; (*H2k hypermap*) (*let hk=new_definition`hk((D:A->bool),(f:A->A),(n:A->A),(e:A->A),(k:num)) <=> CARD D = 2 * k /\ (f permutes D) /\ (n permutes D) /\ (e permutes D ) /\ (e o n o f= I) /\ (?x:A y:A. (x IN D) /\ (y IN D) /\ (orbit_map (f:A->A) (x) INTER orbit_map (f) (y)={}) /\ (D = orbit_map (f:A->A) (x) UNION orbit_map (f) (y)) /\ (IMAGE n (orbit_map (f:A->A) (x)))= orbit_map (f) (y))`;; *) (* ************************************************* *) (* Proof remark rem:fan *)
let set_edges_is_finite_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool). FAN(x,V,E)==> FINITE E`,
REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan1;graph] THEN STRIP_TAC THEN MP_TAC(ISPEC `V:real^3->bool`FINITE_POWERSET) THEN RESA_TAC THEN MP_TAC(SET_RULE`UNIONS (E:(real^3->bool)->bool) SUBSET (V:real^3->bool)==> E SUBSET {t| t SUBSET V}`) THEN RESA_TAC THEN MP_TAC(ISPECL [`(E:(real^3->bool)->bool)`;`{t| t SUBSET (V:real^3->bool)}`] FINITE_SUBSET) THEN ASM_SET_TAC[]);;
let remark_fan1=
prove(`!v w V E. (v IN V) /\ (w IN V) ==>((w IN set_of_edge v V E)<=>(v IN set_of_edge w V E))`,
(
let lemma=prove(`{w,v}={v,w}`, SET_TAC[]) in
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[set_of_edge;IN_ELIM_THM]  THEN ASM_REWRITE_TAC[] THEN MESON_TAC[lemma]));;
let remark_finite_fan1=
prove(`!v:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FINITE V ==> FINITE (set_of_edge v V E)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN MP_TAC(ISPECL [`(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool))`; `V:real^3->bool`] FINITE_SUBSET) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[set_of_edge] THEN SET_TAC[] );;
let properties_of_set_of_edge=
prove(`!v:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) u:real^3. UNIONS E SUBSET V ==> ({v,u} IN E <=> u IN set_of_edge v V E)`,
REPEAT GEN_TAC THEN REWRITE_TAC[UNIONS; SUBSET; set_of_edge ; IN_ELIM_THM] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `u:real^3`th)) THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th)) THEN SET_TAC[]);;
let properties_of_set_of_edge_fan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3. FAN(x,V,E) ==> ({v,u} IN E <=> u IN set_of_edge v V E)`,
REWRITE_TAC[FAN] THEN REPEAT GEN_TAC THEN REWRITE_TAC[UNIONS; SUBSET; set_of_edge ; IN_ELIM_THM] THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"a") THEN STRIP_TAC THEN REMOVE_THEN "a"(fun th-> MP_TAC(ISPEC `u:real^3`th)) THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th)) THEN SET_TAC[]);;
let properties_of_graph=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3). FAN(x,V,E) /\{v,u} IN E==> v IN V`,
REPEAT GEN_TAC THEN REWRITE_TAC[FAN] THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC "a") THEN REPEAT STRIP_TAC THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS; SUBSET; IN_ELIM_THM] THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`v:real^3` th)) THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC THEN EXISTS_TAC `{(v:real^3),(u:real^3)}` THEN ASM_TAC THEN SET_TAC[]);;
let th3a12=
prove(`!x v u.(~ collinear {x,v,u} ==> DISJOINT {x,u} {v})`,
(
let th=prove(`{x,v,u}={x,v,u}`, SET_TAC[]) in
REPEAT GEN_TAC THEN REWRITE_TAC[th;IN_DISJOINT] THEN MATCH_MP_TAC MONO_NOT THEN 
REWRITE_TAC[COLLINEAR_3;COLLINEAR_LEMMA; VECTOR_ARITH` a-b= vec 0 <=> a = b`; IN_SING] THEN STRIP_TAC 
  THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC 
THEN ASM_REWRITE_TAC[] THEN SET_TAC[]));;
let th3a=
prove(`!x v u.(~ collinear {x,v,u} ==> DISJOINT {x,v} {u})`,
(
let th=prove(`{x,v,u}={x,u,v}`, SET_TAC[]) in
REPEAT GEN_TAC THEN REWRITE_TAC[th;IN_DISJOINT] THEN MATCH_MP_TAC MONO_NOT THEN 
REWRITE_TAC[COLLINEAR_3;COLLINEAR_LEMMA; VECTOR_ARITH` a-b= vec 0 <=> a = b`; IN_SING] THEN STRIP_TAC 
  THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC 
THEN ASM_REWRITE_TAC[] THEN SET_TAC[]));;
let th3b=
prove(`!x v u. ~ collinear {x,v,u} ==> ~(x=v) `,
REPEAT GEN_TAC THEN REWRITE_TAC[COLLINEAR_3;COLLINEAR_LEMMA; VECTOR_ARITH` a-b= vec 0 <=> a = b`; DE_MORGAN_THM] THEN SET_TAC[]);;
let th3b1=
prove(`!x v u. ~ collinear {x,v,u} ==> ~(x=u) `,
(
let th=prove(`{x,v,u}={x,u,v}`, SET_TAC[]) in
REWRITE_TAC[th;th3b]));;
let th3c= 
prove(`!x v u. ~ collinear {x,v,u} ==> ~(u IN aff {x,v})`,
REPEAT GEN_TAC THEN MATCH_MP_TAC MONO_NOT THEN REWRITE_TAC[aff; AFFINE_HULL_2; IN_ELIM_THM;COLLINEAR_3;COLLINEAR_LEMMA; VECTOR_ARITH` a-b= vec 0 <=> a = b`; DE_MORGAN_THM] THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[REAL_ARITH `u'+v'= &1 <=> v'= &1 -u'`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[VECTOR_ARITH`(u = u' % x + (&1 - u') % v) <=> (u - v = u' % (x-v))`] THEN SET_TAC[]);;
let th3d=
prove(`!x v u. ~(x=v)/\ ~(x=u) ==> DISJOINT {x} {v,u}`,
SET_TAC[]);;
let th3=
prove(`!x v u. ~ collinear {x,v,u} ==> ~ (x=v) /\ ~(x=u) /\ DISJOINT {x,v} {u}/\ DISJOINT {x,u} {v} /\DISJOINT {x} {v,u} /\ ~(u IN aff {x,v})`,
MESON_TAC[th3a;th3b;th3b1;th3c;th3d;th3a12]);;
let collinear1_fan=
prove(`!x v u. ~ collinear {x,u,v} <=> ~(u IN aff {x,v})/\ ~ (x=v)`,
(
let lem=prove(`!x v u. {x,v,u}= {x,u,v}`,SET_TAC[]) in
REPEAT GEN_TAC THEN EQ_TAC
THENL[
MESON_TAC[th3;lem];
REWRITE_TAC[SET_RULE`~(t1) /\ ~ t2<=> ~(t2\/ t1)`;COLLINEAR_3_EXPAND;aff; AFFINE_HULL_2;IN_ELIM_THM] 
THEN MATCH_MP_TAC MONO_NOT  THEN MATCH_MP_TAC MONO_OR THEN STRIP_TAC 
THENL[
REWRITE_TAC[];

STRIP_TAC THEN EXISTS_TAC`u':real` THEN EXISTS_TAC`&1- (u':real)` THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]]));;
let collinear_fan=
prove(`!x v u. ~ collinear {x,v,u} <=> ~(u IN aff {x,v})/\ ~ (x=v)`,
(
let lem=prove(`!x v u. {x,v,u}= {x,u,v}`,SET_TAC[]) in
MESON_TAC[collinear1_fan;lem]));;
let th4=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3). FAN(x,V,E) /\{v,u} IN E==> ~(x=v)`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`; `(v:real^3)`]properties_of_graph) THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[FAN;fan2] THEN SET_TAC[]);;
let remark4_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3). FAN(x,V,E) /\ {v,u} IN E==> ~ (x=v) /\ ~(x=u) /\ DISJOINT {x,v} {u}/\ DISJOINT {x,u} {v} /\ DISJOINT {x} {v,u} /\ ~(u IN aff {x,v})`,
REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan6] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN REPEAT DISCH_TAC THEN REMOVE_THEN"a"(fun th->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REWRITE_TAC[th3]);;
let collinears_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3). FAN(x,V,E) /\{v,u} IN E==>( ~ collinear {x,v,u} <=> ~(u IN aff {x,v}))`,
MESON_TAC[remark4_fan;collinear_fan]);;
let remark1_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (u:real^3) (v:real^3). FAN(x,V,E) ==> FINITE (set_of_edge v V E) /\({v,u} IN E <=> u IN set_of_edge v V E)/\ ({v,u} IN E==> ~ collinear {x,v,u}/\ ~ (x=v) /\ ~(x=u)/\ ~(v=u) /\ DISJOINT {x,v} {u}/\ DISJOINT {x,u} {v} /\DISJOINT {x} {v,u} /\ ~(u IN aff {x,v}) /\ v IN V/\ ( ~ collinear {x,v,u} <=> ~(u IN aff {x,v})))`,
(***************SIGMA_FAN*****************)
let sigma_fan=new_definition`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)=  
(if (set_of_edge v V E = {u} ) then u 
    else (@(w:real^3).  (w IN (set_of_edge v V E)) /\ ~(w=u) /\
(!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1)))`;;
(* This extends sigma to have a larger domain of R^3 rather than just V. It is the identity outside V (compare the definition of `permutes` ). *)
let extension_sigma_fan=new_definition`extension_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)=  
(if ~(u IN set_of_edge v V E ) then u 
    else (sigma_fan x V E v u))`;;
let exists_sigma_fan=
prove(` (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3). ~ (set_of_edge v V E= {u} ) /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E)) ==> (?(w:real^3). (w IN (set_of_edge v V E)) /\ ~(w=u) /\ (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1))) `,
(
let lemma = prove
   (`!X:real->bool. 
          FINITE X /\ ~(X = {}) 
          ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
    MESON_TAC[INF_FINITE]) in


MP_TAC(lemma) THEN DISCH_THEN(LABEL_TAC "a") THEN REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan1] THEN STRIP_TAC THEN MP_TAC (ISPECL[`(v:real^3)` ;`(V:real^3->bool)`; `(E:(real^3->bool)->bool)`]remark_finite_fan1) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
  
SUBGOAL_THEN `FINITE ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3))` ASSUME_TAC
THENL[(*2*)
ASM_MESON_TAC[FINITE_DELETE_IMP];(*2*)

DISJ_CASES_TAC(SET_RULE`((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})\/
 ~((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})`)
THENL[(*3*)
POP_ASSUM MP_TAC THEN REWRITE_TAC[DELETE;EXTENSION;IN_ELIM_THM] THEN DISCH_TAC
  THEN SUBGOAL_THEN `set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={u:real^3}` ASSUME_TAC
THENL[(*4*)
ASM_TAC THEN SET_TAC[];(*4*)
ASM_TAC THEN SET_TAC[]](*4*);(*3*)
SUBGOAL_THEN`~(IMAGE (azim x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3))={})` ASSUME_TAC
THENL[(*4*)
REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ASM_MESON_TAC[];(*4*)

SUBGOAL_THEN` FINITE (IMAGE (azim x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)))` ASSUME_TAC
THENL[(*5*)
ASM_MESON_TAC[FINITE_IMAGE];(*5*)
REMOVE_THEN "a" (fun th ->MP_TAC(ISPEC `(IMAGE (azim x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)))` th)) 
  THEN ASM_REWRITE_TAC[IMAGE;DELETE;IN_ELIM_THM] THEN STRIP_TAC THEN EXISTS_TAC`x':real^3`
  THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]
](*5*)](*4*)](*3*)](*2*)(*1*)));;
let azim1=new_definition`azim1 (x:real^3) (v:real^3) (u:real^3) (w:real^3)= &2 * pi- azim x v u w`;;
let exists_inverse_sigma_fan_alt=
prove(` (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3). ~ (set_of_edge v V E= {u} ) /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E)) ==> (?(w:real^3). (w IN (set_of_edge v V E)) /\ ~(w=u) /\ (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim1 x v u w <= azim1 x v u w1))) `,
(
let lemma = prove
   (`!X:real->bool. 
          FINITE X /\ ~(X = {}) 
          ==> ?a. a IN X /\ !x. x IN X ==> a <= x`,
    MESON_TAC[INF_FINITE]) in
MP_TAC(lemma) THEN DISCH_THEN(LABEL_TAC "a") THEN REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan1] THEN STRIP_TAC THEN MP_TAC (ISPECL[`(v:real^3)` ;`(V:real^3->bool)`; `(E:(real^3->bool)->bool)`]remark_finite_fan1) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
SUBGOAL_THEN `FINITE ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3))` ASSUME_TAC
THENL[(*2*)

ASM_MESON_TAC[FINITE_DELETE_IMP];(*2*)
DISJ_CASES_TAC(SET_RULE`((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})\/
 ~((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)={})`)
THENL[(*3*)
POP_ASSUM MP_TAC THEN REWRITE_TAC[DELETE;EXTENSION;IN_ELIM_THM] THEN DISCH_TAC
  THEN SUBGOAL_THEN `set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={u:real^3}` ASSUME_TAC
THENL[(*4*)
ASM_TAC THEN SET_TAC[];(*4*)
ASM_TAC THEN SET_TAC[](*4*)];

SUBGOAL_THEN`~(IMAGE ( azim1 x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3))={})` ASSUME_TAC
THENL[(*4*)
REWRITE_TAC[IMAGE_EQ_EMPTY] THEN ASM_MESON_TAC[];(*4*)
SUBGOAL_THEN` FINITE (IMAGE (azim1 x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)))` ASSUME_TAC
THENL[(*5*)
ASM_MESON_TAC[FINITE_IMAGE];(*5*)
REMOVE_THEN "a" (fun th ->MP_TAC(ISPEC `(IMAGE (azim1 x v u) ((set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)) DELETE  (u:real^3)))` th)) 
  THEN ASM_REWRITE_TAC[IMAGE;DELETE;IN_ELIM_THM]THEN STRIP_TAC
THEN EXISTS_TAC`x':real^3`
  THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]
](*5*)](*4*)](*3*)](*2*)(*1*)));;
let SIGMA_FAN=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3). ~ (set_of_edge v V E= {u} ) /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E)) ==> ((sigma_fan x V E v u) IN (set_of_edge v V E)) /\ ~((sigma_fan x V E v u)=u) /\ (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u (sigma_fan x V E v u) <= azim x v u w1)`,
REPEAT GEN_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC[sigma_fan] THEN MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)`; `(v:real^3)`; `(u:real^3)`]exists_sigma_fan) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN SELECT_ELIM_TAC THEN EXISTS_TAC`w:real^3` THEN ASM_REWRITE_TAC[]);;
let sigma_fan_in_set_of_edge=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3). FAN(x,V,E) /\ (u IN (set_of_edge v V E)) ==> ((sigma_fan x V E v u) IN (set_of_edge v V E))`,
REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SET_RULE`~ (set_of_edge v V E= {u:real^3} )\/ (set_of_edge v V E= {u} )`) THENL[ MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)`; `(v:real^3)`; `(u:real^3)`]SIGMA_FAN) THEN ASM_TAC THEN SET_TAC[]; ASM_REWRITE_TAC[sigma_fan;IN_SING]]);;
let AFF_GE_2_1 = 
prove (`!x v w. DISJOINT {x,v} {w} ==> aff_ge {x,v} {w} = {y | ?t1 t2 t3. &0 <= t3 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v + t3 % w}`,
AFF_TAC);;
let AFF_GE_1_2 = 
prove (`!x v w. DISJOINT {x} {v,w} ==> aff_ge {x} {v,w} = {y | ?t1 t2 t3. &0 <= t2 /\ &0 <= t3 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v + t3 % w}`,
AFF_TAC);;
let AFF_GE_1_1 = 
prove (`!x v w. DISJOINT {x} {v} ==> aff_ge {x} {v} = {y | ?t1 t2. &0 <= t2 /\ t1 + t2 = &1 /\ y = t1 % x + t2 % v }`,
AFF_TAC);;
let UNIQUE_FOINT_FAN=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3. FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)/\ ~(aff_ge {x} {v,u} INTER aff_ge {x} {v,w}=aff_ge {x} {v}) ==> u=w`,
REPEAT GEN_TAC THEN REWRITE_TAC[FAN;fan7;fan6] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT STRIP_TAC THEN REMOVE_THEN "a" (fun th-> MP_TAC(ISPECL[`{(v:real^3),(u:real^3)}`;`{(v:real^3),(w:real^3)}`]th)) THEN ASM_REWRITE_TAC[UNION;IN_ELIM_THM;] THEN DISJ_CASES_TAC(SET_RULE`~((u:real^3)=(w:real^3))\/ ((u:real^3)=(w:real^3))`) THENL [ MP_TAC(SET_RULE`~((u:real^3)=(w:real^3))==> {(v:real^3),(u:real^3)} INTER {(v:real^3),(w:real^3)}={v}`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]; ASM_TAC THEN SET_TAC[]]);;
let UNIQUE1_POINT_FAN=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3. FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)/\ w IN aff_gt {x,v} {u} ==> u=w`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC UNIQUE_FOINT_FAN THEN EXISTS_TAC `x:real^3` THEN EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `E:(real^3->bool)->bool` THEN EXISTS_TAC `v:real^3` THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN REWRITE_TAC[FAN;fan1;fan2;fan6;fan7] THEN REPEAT STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN DISCH_THEN (LABEL_TAC "b") THEN REPEAT DISCH_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th)) THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `{(v:real^3),(u:real^3)}`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "c") THEN DISCH_TAC THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]th3) THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]th3) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GT_2_1) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN REMOVE_THEN "c" MP_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN SUBGOAL_THEN` aff_ge {(x:real^3)} {(v:real^3)} SUBSET aff {x,v}` ASSUME_TAC THENL (*1*)[ MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_1) THEN MP_TAC(SET_RULE`~((x:real^3) = (v:real^3))==> DISJOINT {x} {v}`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[aff;AFFINE_HULL_2] THEN ASM_TAC THEN SET_TAC[];(*1*) SUBGOAL_THEN `~((w:real^3) IN aff_ge {x} {v})` ASSUME_TAC THENL (*2*)[ ASM_TAC THEN SET_TAC[];(*2*) POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "d") THEN DISJ_CASES_TAC(REAL_ARITH `(&0 <= (t2:real))\/ (&0 <= (-- (t2:real)))`) THENL (*3*)[ SUBGOAL_THEN `(w:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC THENL (*4*)[ MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN EXISTS_TAC `t3:real` THEN ASM_REWRITE_TAC[] THEN REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*4*) SUBGOAL_THEN `(w:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(w:real^3)}` ASSUME_TAC THENL (*5*)[ MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]AFF_GE_1_2) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `&0:real` THEN EXISTS_TAC `&0:real` THEN EXISTS_TAC `&1:real` THEN REWRITE_TAC[VECTOR_ARITH`w= &0 % x+ &0 % v + &1 % w `] THEN REAL_ARITH_TAC;(*5*) ASM_TAC THEN SET_TAC[]](*5*)](*4*);(*3*) SUBGOAL_THEN `(u:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(w:real^3)}` ASSUME_TAC THENL (*4*)[ MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`]AFF_GE_1_2) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `inv(t3:real) *(--(t1:real))` THEN EXISTS_TAC `inv(t3:real)*(--(t2:real))` THEN EXISTS_TAC `inv(t3:real)` THEN MP_TAC(ISPEC `t3:real` REAL_LT_INV) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(REAL_ARITH`&0< inv(t3:real)==> (&0 <= inv(t3:real))`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL [`inv (t3:real)`;`(--(t2:real))`] REAL_LE_MUL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`inv(t3:real) * -- (t1:real)+ inv(t3) * --(t2:real) +inv (t3)=inv (t3)*(&1-t1-t2)`] THEN MP_TAC(REAL_ARITH`(t1:real)+(t2:real)+(t3:real)= &1 ==> &1 - t1- t2=t3`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(REAL_ARITH`&0<(t3:real)==> ~(t3= &0)`) THEN ASM_REWRITE_TAC[VECTOR_ARITH` (inv t3 * --t1) % x + (inv t3 * --t2) % v + inv t3 % (t1 % x + t2 % v + t3 % u)= (inv t3 * t3) % u ` ] THEN DISCH_TAC THEN MP_TAC(ISPEC `t3:real` REAL_MUL_LINV) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[VECTOR_ARITH ` v= &1 % v`];(*4*) SUBGOAL_THEN `(u:real^3) IN aff_ge {(x:real^3)} {(v:real^3),(u:real^3)}` ASSUME_TAC THENL (*5*)[ MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`]AFF_GE_1_2) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `&0:real` THEN EXISTS_TAC `&0:real` THEN EXISTS_TAC `&1:real` THEN REWRITE_TAC[VECTOR_ARITH`u= &0 % x+ &0 % v + &1 % u `] THEN REAL_ARITH_TAC;(*5*) ASM_TAC THEN SET_TAC[]](*5*)](*4*)](*3*)](*2*)](*1*));;
let UNIQUE_AZIM_POINT_FAN=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3 w1:real^3. FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E) /\ { v, w1} IN E /\ (azim x v u w =azim x v u w1) ==> w=w1`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(th) THEN ASSUME_TAC(th)) THEN REWRITE_TAC[FAN;fan6] THEN REPEAT STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT DISCH_TAC THEN REMOVE_THEN "a"(fun th ->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th)) THEN POP_ASSUM(fun th ->MP_TAC(ISPEC `{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th)) THEN POP_ASSUM(fun th ->MP_TAC(ISPEC `{(v:real^3),(w1:real^3)}`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3) `;`(u:real^3) `;`w:real^3`;` w1:real^3`] AZIM_EQ) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;` w1:real^3`]UNIQUE1_POINT_FAN) THEN ASM_REWRITE_TAC[] );;
let UNIQUE_AZIM_0_POINT_FAN=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3. FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E) /\ (azim x v u w = &0) ==> u=w`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(th) THEN ASSUME_TAC(th)) THEN REWRITE_TAC[FAN;fan6] THEN REPEAT STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT DISCH_TAC THEN REMOVE_THEN "a"(fun th ->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th)) THEN POP_ASSUM(fun th ->MP_TAC(ISPEC `{(v:real^3),(w:real^3)}`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;`(v:real^3) `;`(u:real^3) `;`w:real^3`] AZIM_EQ_0_ALT) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;` w:real^3`]UNIQUE1_POINT_FAN) THEN ASM_REWRITE_TAC[] );;
let UNIQUE_SIGMA_FAN=
prove(` (!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (w:real^3). ~ (set_of_edge v V E= {u} ) /\ FAN(x,V,E) /\ (u IN (set_of_edge v V E)) /\ (w IN (set_of_edge v V E)) /\ ~(w=u) /\ (!(w1:real^3). (w1 IN (set_of_edge v V E))/\ ~(w1=u) ==> azim x v u w <= azim x v u w1) ==> sigma_fan x V E v u=w)`,
(
let th=prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) w:real^3.
FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)
==> (w IN aff_gt {x,v} {u} ==> u=w)`, MESON_TAC[UNIQUE1_POINT_FAN]
) in

ASSUME_TAC(th) THEN
REPEAT GEN_TAC  THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"123") THEN 
DISCH_TAC  THEN DISCH_THEN(LABEL_TAC "1") 
  THEN DISCH_THEN(LABEL_TAC "2") THEN DISCH_THEN(LABEL_TAC "3") THEN DISCH_THEN(LABEL_TAC "4") 
  THEN DISCH_THEN(LABEL_TAC"a") 
  THEN MP_TAC(ISPECL[`(x:real^3)`; `(V:real^3->bool)`; `(E:(real^3->bool)->bool)` ;`(v:real^3)`; `(u:real^3)`]SIGMA_FAN) 
  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
  THEN REMOVE_THEN "a" (fun th->MP_TAC(ISPEC `sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)` th)) 
  THEN ASM_REWRITE_TAC[]
  THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `w:real^3` th)) THEN ASM_REWRITE_TAC[] 
  THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"b")
  THEN REPEAT DISCH_TAC
  THEN SUBGOAL_THEN `azim x v u (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3)) = azim x v u (w:real^3)` ASSUME_TAC
THENL[
REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
REMOVE_THEN "123" (fun th->MP_TAC (ISPECL[`(x:real^3)`; `(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`; `(v:real^3)` ; `(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`;`(w:real^3)`]th)) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN
REMOVE_THEN"1" MP_TAC 
THEN  REWRITE_TAC[FAN;fan6;fan7] THEN STRIP_TAC THEN
POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "c") THEN DISCH_THEN (LABEL_TAC "d")
  THEN REMOVE_THEN"2" MP_TAC THEN REMOVE_THEN"3" MP_TAC THEN REMOVE_THEN"b" MP_TAC 
  THEN REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN REPEAT STRIP_TAC
  THEN REMOVE_THEN "c" MP_TAC THEN DISCH_TAC
  THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th))
  THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th))
  THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))}`th) THEN ASSUME_TAC(th))
  THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REPEAT STRIP_TAC  
  THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)` ;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))`; `(w:real^3)`]AZIM_EQ )
  THEN ASM_REWRITE_TAC[]
  THEN ASM_MESON_TAC[]]));;
let CYCLIC_SET_EDGE_FAN=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3). FAN(x,V,E) /\ v IN V ==> cyclic_set (set_of_edge v V E) x v`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(th) THEN ASSUME_TAC(th)) THEN REWRITE_TAC[FAN; cyclic_set;fan1;fan2;fan6;fan7] THEN STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC THENL(*1*)[ASM_TAC THEN SET_TAC[];(*1*) STRIP_TAC THENL (*2*)[ASM_TAC THEN SET_TAC[remark_finite_fan1];(*2*) STRIP_TAC THENL(*3*)[ ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN REPEAT GEN_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_THEN(LABEL_TAC "b") THEN STRIP_TAC THEN STRIP_TAC THEN REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3), (p:real^3)}` th) THEN ASSUME_TAC(th)) THEN POP_ASSUM (fun th-> MP_TAC(ISPEC `{(v:real^3), (q:real^3)}` th)) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (p:real^3)`]th3) THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (q:real^3)`]th3) THEN ASM_REWRITE_TAC[] THEN POP_ASSUM (fun th-> REWRITE_TAC[]) THEN POP_ASSUM (fun th-> REWRITE_TAC[]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th)) THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `(q:real^3) IN aff_gt {(x:real^3),(v:real^3)} {(p:real^3)}` ASSUME_TAC THENL (*4*)[ MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (p:real^3)`]AFF_GT_2_1) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `--(h:real)` THEN EXISTS_TAC `(h:real)` THEN EXISTS_TAC `&1` THEN REWRITE_TAC[VECTOR_ARITH`q= (-- (h:real)) % x + (h:real) % v + &1 % (q+ h% (x-v))`] THEN REAL_ARITH_TAC;(*4*) ASM_MESON_TAC[UNIQUE1_POINT_FAN]](*4*);(*3*) REWRITE_TAC[INTER;EXTENSION;IN_ELIM_THM] THEN GEN_TAC THEN SUBGOAL_THEN`(x':real^3) IN set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) ==> ~(x' IN aff {x,v})` ASSUME_TAC THENL(*4*)[ ASM_REWRITE_TAC[set_of_edge;IN_ELIM_THM] THEN REPEAT GEN_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_THEN(LABEL_TAC "b") THEN STRIP_TAC THEN STRIP_TAC THEN REMOVE_THEN "a" (fun th-> MP_TAC(ISPEC `{(v:real^3), (x':real^3)}` th) ) THEN ASM_REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (x':real^3)`]th3) THEN ASM_MESON_TAC[]; (*4*) EQ_TAC THENL(*5*)[ POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN STRIP_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[aff];(*5*) ASM_TAC THEN SET_TAC[]](*5*)](*4*)] (*3*)]]);;
let subset_cyclic_set_fan=
prove(`!x:real^3 v:real^3 V:real^3->bool W:real^3->bool. V SUBSET W /\ cyclic_set W x v ==> cyclic_set V x v`,
REPEAT GEN_TAC THEN REWRITE_TAC[cyclic_set] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`V:real^3->bool`;`W:real^3->bool`]FINITE_SUBSET) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN SET_TAC[]);;
let property_of_cyclic_set=
prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3. cyclic_set {u, w1, w2} x v ==> ~(v=x) /\ ~(u=x)/\ ~collinear {vec 0, v-x, u-x}`,
(
let th= prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
x IN {x,w1,w2}`, SET_TAC[]) in

(let th1=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
x IN  affine hull {x,v}
`,REPEAT GEN_TAC THEN REWRITE_TAC[AFFINE_HULL_2;INTER; IN_ELIM_THM] THEN EXISTS_TAC`&1` THEN EXISTS_TAC `&0` THEN
 MESON_TAC[REAL_ARITH`&1+ &0= &1`; VECTOR_ARITH`x= &1 % x + &0 % v`])
in

(let th2=prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3.
x IN {x,w1,w2} INTER affine hull {x,v}
`, REWRITE_TAC[INTER;IN_ELIM_THM] THEN REWRITE_TAC[th;th1]) in


REPEAT GEN_TAC THEN 
REWRITE_TAC[COLLINEAR_LEMMA;DE_MORGAN_THM;VECTOR_ARITH`a-b=vec 0 <=> a=b`;cyclic_set;] THEN STRIP_TAC 
  THEN ASM_REWRITE_TAC[VECTOR_ARITH`(v:real^3)=(x:real^3) <=> x=v`] THEN STRIP_TAC
THENL[ STRIP_TAC  THEN
  POP_ASSUM MP_TAC  THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a")  THEN DISCH_TAC 
THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `w2:real^3`] th2) THEN ASM_TAC THEN SET_TAC[];

STRIP_TAC THENL[

STRIP_TAC  THEN
  POP_ASSUM MP_TAC  THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a")  THEN DISCH_TAC 
THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `w2:real^3`] th2) THEN ASM_TAC THEN SET_TAC[];

STRIP_TAC 
THEN POP_ASSUM MP_TAC  
THEN POP_ASSUM MP_TAC 
THEN DISCH_THEN(LABEL_TAC"a")  
THEN DISCH_TAC 
THEN REMOVE_THEN "a" MP_TAC 
THEN POP_ASSUM MP_TAC 
THEN REWRITE_TAC[VECTOR_ARITH`(c:real) % ((v:real^3)-(x:real^3))=(u:real^3)-x <=> u =  (&1 - c) % x+c % v`] 
THEN DISCH_TAC 
THEN SUBGOAL_THEN `(u:real^3) IN affine hull {(x:real^3),(v:real^3)}` ASSUME_TAC
THENL[
REWRITE_TAC[AFFINE_HULL_2; IN_ELIM_THM] 
THEN EXISTS_TAC `&1 - (c:real)` 
THEN EXISTS_TAC`c:real`
THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - (c:real) +c= &1`;];

MP_TAC(ISPECL[`u:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `w2:real^3`]th) 
THEN DISCH_TAC 
THEN ASM_TAC 
THEN SET_TAC[INTER]
]]]))));;
let property_of_cyclic_set1=
prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3. cyclic_set {u, w1, w2} x v ==> ~collinear {x, v, w1}`,
(
let th=prove(`{u,w1,w2}={w1,u,w2}`,SET_TAC[]) in

REPEAT GEN_TAC THEN DISCH_TAC 
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w1:real^3`;`u:real^3`; `w2:real^3`] property_of_cyclic_set) THEN ASM_REWRITE_TAC[th] THEN STRIP_TAC THEN ASM_REWRITE_TAC[COLLINEAR_3]));;
let property_of_cyclic_set2=
prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3. cyclic_set {u, w1, w2} x v ==> ~collinear {x, v, w2}`,
(
let th=prove(`{u,w1,w2}={w2,w1,u}`,SET_TAC[]) in
( let th1=prove(`{u,w1,w2}={w1,w2,u}`,SET_TAC[]) in

REPEAT GEN_TAC THEN DISCH_TAC 
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w2:real^3`;`w1:real^3`; `u:real^3`] property_of_cyclic_set)
THEN ASM_REWRITE_TAC[th] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN MESON_TAC[th1;COLLINEAR_3])));;
let property_of_cyclic_set3=
prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3. cyclic_set {u, w1, w2} x v ==> ~ collinear {x, v, u}`,
(
let th=prove(`{u,w1,w2}={w1,u,w2}`,SET_TAC[]) in

REPEAT GEN_TAC THEN DISCH_TAC 
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set)
THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_MESON_TAC[COLLINEAR_3;th]));;
let properties_of_cyclic_set=
prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3. cyclic_set {u, w1, w2} x v ==> ~(v=x) /\ ~(u=x)/\ ~collinear {vec 0, v-x, u-x} /\ ~collinear {x, v, u} /\ ~collinear {x, v, w1} /\ ~collinear {x, v, w2}`,
let XOHLED=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3). FAN(x,V,E) /\ v IN V ==> cyclic_set (set_of_edge v V E) x v`,
MESON_TAC[CYCLIC_SET_EDGE_FAN]);;
let d1_fan =new_definition`
d1_fan (x,V,E) ={(x':real^3,v:real^3,w:real^3,w1:real^3)| (x'=x) /\ ({v,w} IN  E)/\ (w1 = sigma_fan x V E v w)}`;;
(* d2_fan not yet used *)
let d2_fan=new_definition`d2_fan (x,V,E)={ (x',v)| (x'=x) /\ (V v) /\ ((set_of_edge v V E) ={})}`;;
let inverse_sigma_fan_alt=new_definition`inverse_sigma_fan_alt x V E v w = @a. sigma_fan x V E v a=w`;;
let e_fan=new_definition` e_fan (x:real^3) V E = (\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,w,v,(sigma_fan x V E w v)))`;;
let f_fan=new_definition`f_fan (x:real^3) V E = (\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,w,(inverse_sigma_fan_alt x V E w v),v) )`;;
let n_fan=new_definition`n_fan (x:real^3) V E =(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,v,(sigma_fan x V E v w),(sigma_fan x V E v (sigma_fan x V E v w))))`;;
(* i_fan corrects the 4th coordinate to be the dart *)
let i_fan=new_definition`i_fan (x:real^3) V E=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,v,w,(sigma_fan x V E v w)))`;;
let pr1=new_definition`pr1=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). x)`;;
let pr2=new_definition`pr2=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). v)`;;
let pr3=new_definition`pr3=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). w)`;;
let pr4=new_definition`pr4=(\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). w1)`;;
(* if f = sigma, the power_map_points gives iterates of sigma (for fixed x v) *)
let power_map_points= new_recursive_definition num_RECURSION `(power_map_points f x V E v w 0 = w)/\(power_map_points f x V E v w  (SUC n)= f x V E v (power_map_points f x V E v w n))`;;
(* This is the composition operator (o), specialized to functions on 4-tuples *)
let o_funs=new_definition`!(f:real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3) (g:real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3). o_funs f g =(\(x:real^3,y:real^3,z:real^3,t:real^3).  f (pr1 (g(x,y,z,t)),pr2(g(x,y,z,t)),pr3(g(x,y,z,t)),pr4(g(x,y,z,t))))`;;
(* powers of permutations *)
let power_maps= new_recursive_definition num_RECURSION `(power_maps  (f:real^3->(real^3->bool)->((real^3->bool)->bool)->real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) 0 = i_fan (x:real^3) V E) /\ (power_maps f x V E (SUC n)= o_funs (f x V E)  (power_maps f x V E n))`;;
(* powers of node map *)
let power_n_fan= new_definition`power_n_fan x V E n=( \(x,v,w,w1). (x,v,(power_map_points sigma_fan x V E v w n),(power_map_points sigma_fan x V E v w (SUC n))))`;;
(* the node of a dart, in a special form for fans *)
let a_node_fan=new_definition`a_node_fan x V E (x,v,w,w1)={a | ?n. a=(power_maps  n_fan x V E n) (x,v,w,sigma_fan x V E v w)}`;;
(* The set X(V,E) *)
let xfan= new_definition`xfan (x,V,E)={v | ?e. (E e)/\(v IN aff_ge {x} e)}`;;
(* See comment by AS in fan_defs.hl. The correct definition is there. *)
let yfan_deprecated= new_definition`yfan_deprecated (x,V,E)={v:real^3 | ?e. ( E e )/\(~(v IN aff_ge {x} e))}`;;
(* W^0_{dart}(x,v,w...) *)
let w_dart_fan=new_definition`w_dart_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) ((y:real^3),(v:real^3),(w:real^3),(w1:real^3))=  
if (CARD (set_of_edge v V E) > 1) then wedge x v w (sigma_fan x V E v w)
else  
(if set_of_edge v  V E ={w} then (UNIV:real^3->bool) DIFF aff_ge {x,v} {w}
else (if set_of_edge v  V E ={} then (UNIV:real^3->bool) DIFF aff {x,v} else {}))`;;
let image_power_map_points=
prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) . FAN(x,V,E) /\ (u IN set_of_edge v V E) ==> power_map_points (sigma_fan) x V E v u i IN set_of_edge v V E`,
INDUCT_TAC THEN REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[power_map_points] THENL[ ASM_MESON_TAC[]; REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC "a") THEN REPEAT DISCH_TAC THEN REMOVE_THEN "a" (fun th -> MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` (v:real^3) `;`(u:real^3)`] th)) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISJ_CASES_TAC(SET_RULE `set_of_edge v V E ={power_map_points (sigma_fan) x V E v u i}\/ ~(set_of_edge v V E ={power_map_points (sigma_fan) x V E v u i})`) THENL[ASM_MESON_TAC[sigma_fan]; ASM_MESON_TAC[SIGMA_FAN]]]);;
let IN2_ORBITS_FAN=
prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) . FAN(x,V,E) /\ ({v,u} IN E) ==> {v,power_map_points (sigma_fan) x V E v u i} IN E`,
let IN1_ORBITS_FAN=
prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) . FAN(x,V,E) /\ (u IN set_of_edge v V E) ==> {v,power_map_points (sigma_fan) x V E v u i} IN E`,
let remark_power_map_points=
prove(`!(i:num) (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) . FAN(x,V,E) /\ ({v,u} IN E) ==> power_map_points (sigma_fan) x V E v u i IN set_of_edge v V E /\ {v,power_map_points sigma_fan x V E v u i} IN E /\ ~(collinear {x,v,power_map_points sigma_fan x V E v u i}) /\ ~(x = power_map_points (sigma_fan) x V E v u i) /\ ~(v = power_map_points (sigma_fan) x V E v u i) /\ DISJOINT {x, v} {power_map_points (sigma_fan) x V E v u i} /\ ~((power_map_points (sigma_fan) x V E v u i) IN aff {x, v}) /\ DISJOINT {x} {v, (power_map_points (sigma_fan) x V E v u i)} `,
(*-------------------------------------------------------------------------------------------*) (* the properties in normal vector *) (*-------------------------------------------------------------------------------------------*)
let imp_norm_not_zero_fan=
prove(`!v:real^3 x:real^3. ~(v = x) ==> ~(norm ( v - x) = &0)`,
REPEAT GEN_TAC THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `(v:real^3)-(x:real^3)= vec 0` ASSUME_TAC THENL [POP_ASSUM MP_TAC THEN MESON_TAC[NORM_EQ_0]; SUBGOAL_THEN `(v:real^3) = (x:real^3)` ASSUME_TAC THENL [POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC; ASM_TAC THEN SET_TAC[]]]);;
let imp_norm_gl_zero_fan=
prove(`!v:real^3 x:real^3. ~(v = x) ==> inv(norm ( v - x)) > &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~(norm ( (v:real^3) - (x:real^3)) = &0)` ASSUME_TAC THENL [ASM_MESON_TAC[imp_norm_not_zero_fan]; MP_TAC (ISPEC `(v:real^3)-(x:real^3)` NORM_POS_LE) THEN DISCH_TAC THEN SUBGOAL_THEN `norm((v:real^3)-(x:real^3))> &0` ASSUME_TAC THENL [POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; MP_TAC (ISPEC `norm((v:real^3)-(x:real^3))` REAL_LT_INV_EQ) THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC]]);;
let imp_inv_norm_not_zero_fan=
prove(`!v:real^3 x:real^3. ~(v = x) ==> ~(inv(norm ( v - x)) = &0)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN SUBGOAL_THEN `inv(norm ((v:real^3) - (x:real^3))) > &0` ASSUME_TAC THENL [ASM_MESON_TAC[imp_norm_gl_zero_fan]; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC]);;
let imp_norm_ge_zero_fan=
prove(`!v:real^3 x:real^3. ~(v = x) ==> inv(norm ( v - x)) >= &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~(norm ( (v:real^3) - (x:real^3)) = &0)` ASSUME_TAC THENL [ASM_MESON_TAC[imp_norm_not_zero_fan]; MP_TAC (ISPEC `(v:real^3)-(x:real^3)` NORM_POS_LE) THEN DISCH_TAC THEN SUBGOAL_THEN `norm((v:real^3)-(x:real^3))> &0` ASSUME_TAC THENL [POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; MP_TAC (ISPEC `norm((v:real^3)-(x:real^3))` REAL_LT_INV_EQ) THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC]]);;
let norm_of_normal_vector_is_unit_fan=
prove(`!v:real^3 x:real^3. ~(v = x) ==> norm(inv(norm ( v - x))% (v-x))= &1`,
REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[NORM_MUL] THEN SUBGOAL_THEN ` inv(norm ( (v:real^3) - (x:real^3))) >= &0` ASSUME_TAC THENL[ ASM_MESON_TAC[imp_norm_ge_zero_fan]; SUBGOAL_THEN ` ~(norm ( (v:real^3) - (x:real^3))= &0)` ASSUME_TAC THENL [ASM_MESON_TAC[imp_norm_not_zero_fan]; SUBGOAL_THEN ` abs(inv(norm ( (v:real^3) - (x:real^3))))= inv(norm ( (v:real^3) - (x:real^3)))` ASSUME_TAC THENL [ASM_MESON_TAC[REAL_ABS_REFL;REAL_ARITH `(a:real)>= &0 <=> &0 <= a`; ]; MP_TAC(ISPEC `norm ( (v:real^3) - (x:real^3))` REAL_MUL_LINV)THEN ASM_REWRITE_TAC[]]]]);;
(*---------------------------------------------------------------------------------------*) (* the normal coordinate is the definiton of frame in flyspeck(above JBDNJJB) *) (*---------------------------------------------------------------------------------------*)
let e3_fan=new_definition`e3_fan  (x:real^3) (v:real^3) (u:real^3) = inv(norm((v:real^3)-(x:real^3))) % ((v:real^3)-(x:real^3))`;;
let e2_fan=new_definition`e2_fan (x:real^3) (v:real^3) (u:real^3) = inv(norm((e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3)))) % ((e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))) `;;
let e1_fan=new_definition`e1_fan (x:real^3) (v:real^3) (u:real^3)=(e2_fan (x:real^3) (v:real^3) (u:real^3)) cross (e3_fan (x:real^3) (v:real^3) (u:real^3))`;;
let e3_mul_dist_fan=
prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) ==> dist (v,x) % e3_fan x v u = v - x`,
REPEAT GEN_TAC THEN REWRITE_TAC[e3_fan; dist; VECTOR_ARITH `(a:real) % (b:real)% (v:real^3)=(a*b)%v`] THEN MESON_TAC[imp_norm_not_zero_fan; REAL_MUL_RINV; VECTOR_ARITH `&1 %(v:real^3)=v`]);;
let norm_dot_fan=
prove(`!x:real^3. norm x = &1 ==> x dot x = &1`,
ASM_MESON_TAC[NORM_POW_2; REAL_ARITH `&1 pow 2= &1`]);;
let e3_is_normal_fan=
prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) ==> e3_fan x v u dot e3_fan x v u = &1`,
REPEAT GEN_TAC THEN REWRITE_TAC[e3_fan]THEN DISCH_TAC THEN SUBGOAL_THEN `norm(inv(norm((v:real^3)-(x:real^3))) %(v-x)) pow 2= &1 pow 2` ASSUME_TAC THENL [ASM_MESON_TAC[norm_of_normal_vector_is_unit_fan] ; ASM_MESON_TAC[NORM_POW_2; REAL_ARITH `&1 pow 2= &1`]]);;
let e2_is_normal_fan= 
prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> e2_fan x v u dot e2_fan x v u = &1`,
REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~((e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))= vec 0)` ASSUME_TAC THENL[ POP_ASSUM MP_TAC THEN MATCH_MP_TAC MONO_NOT THEN REWRITE_TAC[e3_fan;CROSS_LMUL] THEN DISCH_TAC THEN MP_TAC(ISPECL [`v:real^3`; `x:real^3`] imp_inv_norm_not_zero_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL [`inv(norm((v:real^3)-(x:real^3)))`; `((v:real^3) -(x:real^3)) cross ((u:real^3)-(x:real^3))`; `(vec 0):real^3`] VECTOR_MUL_LCANCEL_IMP) THEN ASM_REWRITE_TAC[VECTOR_MUL_RZERO;CROSS_EQ_0 ]; MP_TAC(ISPECL [`(e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))`; `((vec 0):real^3)`] norm_of_normal_vector_is_unit_fan) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[e2_fan; VECTOR_ARITH`(v:real^3)- vec 0 = v`] THEN MESON_TAC[norm_dot_fan]]);;
let e2_orthogonal_e3_fan=
prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> (e2_fan x v u) dot (e3_fan x v u)= &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e2_fan;e3_fan;CROSS_LMUL;DOT_RMUL;] THEN VEC3_TAC);;
let e1_is_normal_fan=
prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> e1_fan x v u dot e1_fan x v u = &1`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e1_fan;DOT_CROSS] THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ] e2_orthogonal_e3_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ] e2_is_normal_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ] e3_is_normal_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let e1_orthogonal_e3_fan=
prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> (e1_fan x v u) dot (e3_fan x v u)= &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e1_fan;DOT_CROSS_SELF] );;
let e1_orthogonal_e2_fan=
prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> (e1_fan x v u) dot (e2_fan x v u)= &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e1_fan;DOT_CROSS_SELF] );;
let e1_cross_e2_dot_e3_fan=
prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> &0 < (e1_fan x v u cross e2_fan x v u) dot e3_fan x v u`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e1_fan;CROSS_TRIPLE] THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ] e1_is_normal_fan) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[e1_fan] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let orthonormal_e1_e2_e3_fan=
prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> (orthonormal (e1_fan x v u) (e2_fan x v u) (e3_fan x v u))`,
let dot_e2_fan=
prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> (u-x) dot e2_fan x v u = &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e2_fan;DOT_RMUL;DOT_CROSS_SELF] THEN REAL_ARITH_TAC);;
let vdot_e2_fan=
prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> (v-x) dot e2_fan x v u = &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e2_fan;e3_fan;CROSS_LMUL;DOT_RMUL;DOT_CROSS_SELF] THEN REAL_ARITH_TAC);;
let vcross_e3_fan=
prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> (v - x) cross (e3_fan x v u) = vec 0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e3_fan;CROSS_RMUL;CROSS_REFL] THEN VECTOR_ARITH_TAC);;
let udot_e1_fan=
prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> &0 < (u - x) dot e1_fan x v u `,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[e1_fan; e2_fan;CROSS_LMUL;DOT_RMUL;DOT_SYM;DOT_LMUL;CROSS_TRIPLE] THEN SUBGOAL_THEN `~((e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))= vec 0)` ASSUME_TAC THENL[ POP_ASSUM MP_TAC THEN MATCH_MP_TAC MONO_NOT THEN REWRITE_TAC[e3_fan;CROSS_LMUL] THEN DISCH_TAC THEN MP_TAC(ISPECL [`v:real^3`; `x:real^3`] imp_inv_norm_not_zero_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL [`inv(norm((v:real^3)-(x:real^3)))`; `((v:real^3) -(x:real^3)) cross ((u:real^3)-(x:real^3))`; `(vec 0):real^3`] VECTOR_MUL_LCANCEL_IMP) THEN ASM_REWRITE_TAC[VECTOR_MUL_RZERO;CROSS_EQ_0 ]; MP_TAC(ISPECL [`(e3_fan (x:real^3) (v:real^3) (u:real^3)) cross ((u:real^3)-(x:real^3))`; `((vec 0):real^3)`]imp_norm_gl_zero_fan) THEN ASM_REWRITE_TAC[REAL_ARITH`(a:real)> &0 <=> &0 < (a:real)`;VECTOR_ARITH `(a:real^3)- vec 0=a`] THEN DISCH_TAC THEN MP_TAC(ISPEC `e3_fan (x:real^3) (v:real^3) (u:real^3) cross (u-x)`DOT_POS_LT) THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[REAL_LT_MUL]]);;
let udot_e1_fan1=
prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> &0 <= (u - x) dot e1_fan x v u `,
REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3` ;`v:real^3` ;`u:real^3`]udot_e1_fan) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let vdot_e1_fan=
prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) ==> (v - x) dot e1_fan x v u = &0`,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]e3_mul_dist_fan) THEN RES_TAC THEN SYM_ASSUM_TAC THEN REWRITE_TAC[DOT_SYM;DOT_LMUL] THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]e1_orthogonal_e3_fan) THEN RESA_TAC THEN REAL_ARITH_TAC);;
let properties_coordinate=
prove(`!x:real^3 v:real^3 u:real^3. ~(collinear {x, v, u}) ==> (orthonormal (e1_fan x v u) (e2_fan x v u) (e3_fan x v u)) /\ dist (v,x) % e3_fan x v u = v - x /\ ((v - x) cross (e3_fan x v u) = vec 0) /\ (v-x) dot e2_fan x v u = &0 /\ ((u-x) dot e2_fan x v u = &0) /\ &0 <= (u - x) dot e1_fan x v u /\ &0 < (u - x) dot e1_fan x v u /\ (v - x) dot e1_fan x v u = &0`,
(
let lem=prove(`!a b c. {a,b,c}={b,a,c}`,SET_TAC[]) in
REPEAT GEN_TAC THEN DISCH_THEN(LABEL_TAC "a") THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]th3)
  THEN RED_TAC THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[lem;] THEN GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[COLLINEAR_3]
THEN
ASM_MESON_TAC[orthonormal_e1_e2_e3_fan;e3_mul_dist_fan; dot_e2_fan;vdot_e2_fan;vcross_e3_fan;udot_e1_fan;udot_e1_fan1;vdot_e1_fan]));;
let module_of_vector =
prove(`!x:real^3 v:real^3 u:real^3 w:real^3 r:real psi:real h:real. ~(v=x) /\ ~(u=x) /\ ~(collinear {vec 0, v-x, u-x}) /\ (&0 < r) /\ (w=(r * cos psi) % e1_fan x v u + (r * sin psi) % e2_fan x v u + h % (v-x)) ==> sqrt(((w cross (e3_fan x v u)) dot e1_fan x v u) pow 2 + ((w cross (e3_fan x v u)) dot e2_fan x v u) pow 2) = r`,
REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;] THEN MP_TAC(ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ] orthonormal_e1_e2_e3_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (LABEL_TAC "a") THEN MP_TAC (ISPECL [`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`; `e3_fan (x:real^3) (v:real^3) (u:real^3)`]ORTHONORMAL_CROSS) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL [`x:real^3`; `v:real^3`; `u:real^3` ]vcross_e3_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]CROSS_SKEW) THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[DOT_LADD;DOT_LMUL;DOT_LZERO;DOT_LNEG] THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[orthonormal] THEN DISCH_TAC THEN ASM_REWRITE_TAC[DOT_SYM] THEN REWRITE_TAC[REAL_ARITH `-- &0 = &0`; REAL_ARITH`(a:real)* &0 = &0`; REAL_ARITH `(a:real) * &1 = a`; REAL_ARITH `(a:real) + &0 = a`;REAL_ARITH `&0 + (a:real) = a`;REAL_POW_MUL; REAL_ARITH `-- &1 pow 2 = &1`; REAL_ARITH `(d:real) * (b:real) + d * (c:real) = d * ( b + c)`;SIN_CIRCLE; sqrt] THEN MATCH_MP_TAC SELECT_UNIQUE THEN REWRITE_TAC[BETA_THM] THEN GEN_TAC THEN EQ_TAC THENL[ STRIP_TAC THEN SUBGOAL_THEN `((y:real) - (r:real))* (y + r) = &0` ASSUME_TAC THENL[ REWRITE_TAC[REAL_ADD_LDISTRIB; REAL_ARITH `((a:real)- (b:real)) * (c:real)= a *c - b * c`; REAL_ARITH`(y:real) * (r:real)= r * y`; REAL_ARITH `((a:real) +(b:real)) - ((b:real) + (c:real))= a - c`; REAL_ARITH `(a:real)- (c:real)= &0 <=> a = c`] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; MP_TAC (ISPECL [`(y:real)- (r:real)`; `(y:real)+(r:real)` ]REAL_ENTIRE) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL [POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]]; DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]);;
(****************************************************************************) (* some properties of azim in the orthonormal frame *) (****************************************************************************)
let collinear_imp_azim_is_rezo_fan=
prove( `!x:real^3 v:real^3 u:real^3 y:real h1:real h2:real. ~(v = x) /\ ~(u = x) /\ ~collinear {x, v, u} /\ &0 <= y /\ y < &2 * pi /\ ( !e1:real^3 e2:real^3 e3:real^3. orthonormal e1 e2 e3 /\ dist (v,x) % e3 = v - x ==> (?psi:real r1:real r2:real. u - x = (r1 * cos psi) % e1 + (r1 * sin psi) % e2 + h1 % (v - x) /\ u - x = (r2 * cos (psi + y)) % e1 + (r2 * sin (psi + y)) % e2 + h2 % (v - x) /\ &0 < r1 /\ &0 < r2)) ==> y = &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~collinear {vec 0, (v:real^3)-(x:real^3), (u:real^3)-x}` ASSUME_TAC THENL (*1*)[ POP_ASSUM MP_TAC THEN MATCH_MP_TAC MONO_NOT THEN MP_TAC(ISPECL [`v:real^3`; `x:real^3`; `u:real^3`] COLLINEAR_3) THEN SUBGOAL_THEN `{(v:real^3),(x:real^3),(u:real^3)}={x,v,u}` ASSUME_TAC THENL[SET_TAC[]; ASM_REWRITE_TAC[] THEN SET_TAC[]]; (*1*) REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "1") THEN DISCH_THEN (LABEL_TAC "2") THEN REWRITE_TAC[LEFT_IMP_FORALL_THM] THEN EXISTS_TAC `e1_fan (x:real^3) (v:real^3) (u:real^3)` THEN EXISTS_TAC `e2_fan (x:real^3) (v:real^3) (u:real^3)` THEN EXISTS_TAC `e3_fan (x:real^3) (v:real^3) (u:real^3)` THEN MP_TAC(ISPECL [`(x:real^3)` ;`(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL [`(x:real^3)` ;`(v:real^3)`;`u:real^3`] e3_mul_dist_fan)THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC "AB") THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `(u:real^3)- (x:real^3)`; `r1:real`; `psi:real`; `h1:real`] module_of_vector) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `(u:real^3)- (x:real^3)`; `r2:real`; `(psi:real)+(y:real)`; `h2:real`] module_of_vector) THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC th) THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `sin (psi:real)= &0` ASSUME_TAC THENL (*2*)[ MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] dot_e2_fan) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[DOT_LADD;DOT_LMUL] THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] vdot_e2_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e2_is_normal_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e1_orthogonal_e2_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ARITH`(a:real)* &0 = &0`; REAL_ARITH`(a:real)+ &0= a`; REAL_ARITH`&0 + (a:real)= a`; REAL_ARITH`(a:real) * &1= a`] THEN DISCH_TAC THEN MATCH_MP_TAC(ISPECL [`sin (psi:real)`;`&0`; `r1:real`] REAL_EQ_LCANCEL_IMP) THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC; (*2*) POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "a") THEN DISCH_THEN (LABEL_TAC "b") THEN REPEAT (DISCH_TAC) THEN REMOVE_THEN "a" MP_TAC THEN REMOVE_THEN "b" MP_TAC THEN REWRITE_TAC[COS_ADD;SIN_ADD] THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] dot_e2_fan) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[DOT_LADD;DOT_LMUL] THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] vdot_e2_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e2_is_normal_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e1_orthogonal_e2_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ARITH`(a:real)* &0 = &0`; REAL_ARITH`&0 * (a:real) = &0`; REAL_ARITH`(a:real)+ &0= a`; REAL_ARITH`&0 + (a:real)= a`; REAL_ARITH`(a:real) * &1= a`;REAL_ENTIRE] THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC THEN STRIP_TAC THENL(*3*)[ REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*3*) MP_TAC(ISPEC `psi:real` SIN_CIRCLE) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;(*3*) MP_TAC(ISPEC `y:real` SIN_EQ_0) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "3") THEN DISCH_TAC THEN REMOVE_THEN "1" MP_TAC THEN REMOVE_THEN "2" MP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(PI_WORKS) THEN REPEAT STRIP_TAC THEN MP_TAC(ISPECL [ `n:real`;`&2`;`pi:real`]REAL_LT_RCANCEL_IMP) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (LABEL_TAC "4") THEN MP_TAC(ISPECL [ `&0`;`n:real`;`pi:real`]REAL_LE_RCANCEL_IMP) THEN REWRITE_TAC[REAL_ARITH`&0 * (a:real) = &0`] THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC "5") THEN MP_TAC(ISPECL [`n:real`; `pi:real`]REAL_ENTIRE) THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REMOVE_THEN "3" MP_TAC THEN REWRITE_TAC[integer] THEN MP_TAC(ISPEC `n:real` REAL_ABS_REFL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN REMOVE_THEN "4" MP_TAC THEN REMOVE_THEN "5" MP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`0`; `n':num`]REAL_OF_NUM_LE) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL [`n':num`; `2`]REAL_OF_NUM_LT) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN SUBGOAL_THEN `(n':num)= 0 \/ n' = 1` ASSUME_TAC THENL (*4*)[ POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;(*4*) POP_ASSUM MP_TAC THEN STRIP_TAC THENL(*5*)[ ASM_MESON_TAC[REAL_OF_NUM_EQ];(*5*) POP_ASSUM MP_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN REPEAT DISCH_TAC THEN REMOVE_THEN "A" MP_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN REPEAT DISCH_TAC THEN REMOVE_THEN "A" MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN REPEAT DISCH_TAC THEN REMOVE_THEN "A" MP_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ARITH `&1 * (a:real)=a`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "A") THEN REPEAT DISCH_TAC THEN REMOVE_THEN "A" MP_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[SIN_PI;COS_PI; REAL_ARITH `(a:real)- &0 = a`; REAL_ARITH `(a:real) * &0= &0`; REAL_ARITH `(a:real) * -- &1= -- a`; VECTOR_ARITH `&0 % (v:real^3)= vec 0`; VECTOR_ARITH `(v:real^3)+ vec 0 + (w:real^3)= v+w`] THEN REMOVE_THEN "AB" MP_TAC THEN DISCH_TAC THEN POP_ASSUM (fun th -> REWRITE_TAC[SYM(th)]) THEN DISCH_TAC THEN SUBGOAL_THEN `(((r2:real) * --cos (psi:real)) % e1_fan (x:real^3) (v:real^3) (u:real^3) + (h2:real) % dist (v,x) % e3_fan x v u) dot e1_fan x v u =(((r2:real) * cos psi) % e1_fan x v u + (h1:real) % dist (v,x) % e3_fan x v u) dot e1_fan x v u` ASSUME_TAC THENL (*6*)[ ASM_REWRITE_TAC[]; (*6*) POP_ASSUM MP_TAC THEN REWRITE_TAC[DOT_LADD;DOT_LMUL;DOT_SYM;] THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e1_is_normal_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e1_orthogonal_e3_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ARITH `(a:real) * &0 = &0`; REAL_ARITH `(a:real)+ &0=a`; REAL_ARITH `(a:real) * &1 =a`; REAL_ARITH `(a:real) *(-- b)= a * b <=> &2 * a * b = &0`] THEN DISCH_TAC THEN MP_TAC(ISPECL [`&2 * (r2:real)`; `cos (psi:real)`]REAL_ENTIRE) THEN REWRITE_TAC[REAL_ARITH `((a:real)*(b:real))*(c:real)=a * b * c`] THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL(*7*)[ REPEAT(POP_ASSUM MP_TAC ) THEN REAL_ARITH_TAC;(*7*) MP_TAC( ISPEC `psi:real` SIN_CIRCLE) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ARITH `&0 pow 2= &0`; REAL_ARITH `&0 + &0 = &0`] THEN SET_TAC[](*7*)](*6*)](*5*)]]]]]);;
let azim_is_zero_fan=
prove(`!x:real^3 v:real^3 u:real^3. ~(v=x) /\ ~(u=x) /\ (~(collinear {x, v, u})) ==> azim (x:real^3) (v:real^3) (u:real^3) (u:real^3) = &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[azim_def] THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SELECT_UNIQUE THEN REWRITE_TAC[BETA_THM] THEN GEN_TAC THEN EQ_TAC THENL[ REPEAT STRIP_TAC THEN MP_TAC (ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `y:real`; `h1:real`; `h2:real`]collinear_imp_azim_is_rezo_fan) THEN ASM_REWRITE_TAC[]; DISCH_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL[ REAL_ARITH_TAC; STRIP_TAC THENL[ ASSUME_TAC(PI_WORKS) THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; MP_TAC(ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `u:real^3`] AZIM_EXISTS) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN EXISTS_TAC `h1:real` THEN EXISTS_TAC `h2:real` THEN MP_TAC (ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `theta:real`; `h1:real`; `h2:real`]collinear_imp_azim_is_rezo_fan) THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a") THEN DISCH_THEN (LABEL_TAC "b") THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[]]]]);;
let SINCOS_PRINCIPAL_VALUE_FAN = 
prove( `!x:real. ?y:real. (&0<= y /\ y < &2* pi) /\ (sin(y) = sin(x) /\ cos(y) = cos(x))`,
GEN_TAC THEN MP_TAC(SPECL [`x:real`] SINCOS_PRINCIPAL_VALUE) THEN STRIP_TAC THEN DISJ_CASES_TAC(REAL_ARITH`((y:real) < &0)\/ (&0 <= y)`) THENL [ EXISTS_TAC `(y:real)+ &2 * pi` THEN ASSUME_TAC(PI_POS) THEN ASM_REWRITE_TAC[SIN_PERIODIC;COS_PERIODIC] THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC; EXISTS_TAC `(y:real)` THEN ASSUME_TAC(PI_POS) THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]);;
let sin_of_u_fan=
prove(`!x:real^3 v:real^3 u:real^3 r1:real psi:real h1:real. ~collinear {u,x,v} /\ ~(v=x) /\ ~(u=x)/\ ~collinear {vec 0, v-x, u-x} /\ &0 < r1 /\ u - x = (r1 * cos psi) % (e1_fan x v u) + (r1 * sin psi) % (e2_fan x v u) + h1 % (v-x) ==> sin psi = &0`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] dot_e2_fan) THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[DOT_LADD;DOT_LMUL] THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] vdot_e2_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e2_is_normal_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] e1_orthogonal_e2_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ARITH`(a:real)* &0 = &0`; REAL_ARITH`(a:real)+ &0= a`; REAL_ARITH`&0 + (a:real)= a`; REAL_ARITH`(a:real) * &1= a`] THEN DISCH_TAC THEN MATCH_MP_TAC(ISPECL [`sin (psi:real)`;`&0`; `r1:real`] REAL_EQ_LCANCEL_IMP) THEN ASM_REWRITE_TAC[] THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);;
let cos_of_u_fan=
prove(`!x:real^3 v:real^3 u:real^3 r1:real psi:real h1:real. ~collinear {u,x,v} /\ ~(v=x) /\ ~(u=x)/\ ~collinear {vec 0, v-x, u-x} /\ &0 < r1 /\ u - x = (r1 * cos psi) % (e1_fan x v u) + (r1 * sin psi) % (e2_fan x v u) + h1 % (v-x) ==> cos psi = &1`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `(u:real^3)-(x:real^3)`; `r1:real`; `psi:real`; `h1:real`]module_of_vector) THEN ASM_REWRITE_TAC[] THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)] THEN ASSUME_TAC(th)) THEN POP_ASSUM MP_TAC THEN MP_TAC(ISPECL[`(u:real^3)-(x:real^3)`; `e3_fan (x:real^3) (v:real^3)(u:real^3)`;`e1_fan (x:real^3) (v:real^3)(u:real^3)`]CROSS_TRIPLE) THEN DISCH_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN MP_TAC(ISPECL[`(u:real^3)-(x:real^3)`; `e3_fan (x:real^3) (v:real^3)(u:real^3)`;`e2_fan (x:real^3) (v:real^3)(u:real^3)`]CROSS_TRIPLE) THEN DISCH_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] orthonormal_e1_e2_e3_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`e1_fan (x:real^3) (v:real^3)(u:real^3)`; `e2_fan (x:real^3) (v:real^3)(u:real^3)`;`e3_fan (x:real^3) (v:real^3)(u:real^3)`]ORTHONORMAL_CROSS )THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN STRIP_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[CROSS_SKEW;th]) THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`] dot_e2_fan)THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[ `e2_fan (x:real^3) (v:real^3)(u:real^3)`;`(u:real^3)-(x:real^3)`]DOT_SYM) THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`&0 pow 2 +(a:real)=a`] THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`] udot_e1_fan1) THEN ASM_REWRITE_TAC[DOT_LNEG;] THEN DISCH_TAC THEN MP_TAC(ISPECL[ `e1_fan (x:real^3) (v:real^3)(u:real^3)`;`(u:real^3)-(x:real^3)`]DOT_SYM) THEN DISCH_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN REWRITE_TAC[POW_2_SQRT_ABS;REAL_ABS_NEG] THEN MP_TAC(ISPECL[ `((u:real^3)-(x:real^3)) dot e1_fan (x:real^3) (v:real^3)(u:real^3)`] REAL_ABS_REFL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (LABEL_TAC "a") THEN DISCH_TAC THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3`; `r1:real`; `psi:real`; `h1:real`] sin_of_u_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[VECTOR_ARITH` (r1 * cos psi) % e1_fan x v u + (r1 * &0) % e2_fan x v u + h1 % (v - x)= (r1 * cos psi) % e1_fan x v u + h1 % (v - x)`] THEN DISCH_TAC THEN SUBGOAL_THEN`((u:real^3) - (x:real^3)) dot e1_fan x (v:real^3) u = (((r1:real) * cos (psi:real)) % e1_fan x v u + (h1:real) % (v - x)) dot e1_fan x v u` ASSUME_TAC THENL[ASM_MESON_TAC[]; POP_ASSUM MP_TAC THEN REWRITE_TAC[DOT_LADD;DOT_LMUL] THEN POP_ASSUM MP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)]) THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`] e1_orthogonal_e3_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[DOT_LMUL;DOT_SYM] THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`] e1_is_normal_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`(a:real)* &1+ (b:real)*(c:real)* &0= a`] THEN REPEAT DISCH_TAC THEN MP_TAC(ISPECL[`&1`;`cos (psi:real)`; `r1:real`]REAL_EQ_LCANCEL_IMP) THEN REWRITE_TAC[REAL_ARITH`(a:real)* &1=a`; REAL_ARITH`&1 = (a:real) <=> a= &1`] THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]);;
let sincos_of_u_fan=
prove(`!x:real^3 v:real^3 u:real^3 r1:real psi:real h1:real. ~collinear {u,x,v} /\ ~(v=x) /\ ~(u=x)/\ ~collinear {vec 0, v-x, u-x} /\ &0 < r1 /\ u - x = (r1 * cos psi) % (e1_fan x v u) + (r1 * sin psi) % (e2_fan x v u) + h1 % (v-x) ==> sin psi = &0 /\ cos psi = &1`,
MESON_TAC[cos_of_u_fan;sin_of_u_fan]);;
let sincos1_of_u_fan=
prove(`!x:real^3 v:real^3 u:real^3 r1:real psi:real h1:real. ~collinear {x,v,u} /\ &0 < r1 /\ u - x = (r1 * cos psi) % (e1_fan x v u) + (r1 * sin psi) % (e2_fan x v u) + h1 % (v-x) ==> sin psi = &0 /\ cos psi = &1`,
REPEAT STRIP_TAC THEN FIND_ASSUM MP_TAC`~collinear {x,v,u:real^3}` THEN ONCE_REWRITE_TAC[SET_RULE`{X,V,U}={U,X,V}`] THEN DISCH_TAC THEN FIND_ASSUM MP_TAC`~collinear {x,v,u:real^3}` THEN ONCE_REWRITE_TAC[SET_RULE`{X,V,U}={V,X,U}`] THEN ONCE_REWRITE_TAC[COLLINEAR_3] THEN DISCH_TAC THEN MRESA_TAC th3[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`] THEN MRESA_TAC sincos_of_u_fan[`(x:real^3)`;`(v:real^3)`;` (u:real^3)`;`r1:real`; `psi:real`; `h1:real`]) ;;
(****************************************************************************) (* the conditions to add azim *) (****************************************************************************)
let sum1_azim_fan=
prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3. cyclic_set {u, w1, w2} x v /\ (azim x v u w1 + azim x v w1 w2) < &2 * pi ==> azim x v u w2 = azim x v u w1+ azim x v w1 w2 `,
(
let th=prove(`!x v u. {v,x,u}={x,v,u}/\{v,x,u}={u,x,v}`,SET_TAC[]) in  


REPEAT GEN_TAC THEN STRIP_TAC 
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN
MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set1) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set2) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN MP_TAC(ISPECL[`v:real^3`; `x:real^3`; `u:real^3`]COLLINEAR_3) THEN ASM_REWRITE_TAC[] THEN
DISCH_TAC THEN  SUBGOAL_THEN `~collinear {(x:real^3),(v:real^3),(u:real^3)}/\ ~collinear {(u:real^3),(x:real^3),(v:real^3)}` ASSUME_TAC
THENL[ASM_MESON_TAC[th];

MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`] azim) 
  THEN STRIP_TAC 
THEN POP_ASSUM(MP_TAC o SPECL [`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]) 
  THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
  THEN MP_TAC(SPEC `psi:real` SINCOS_PRINCIPAL_VALUE_FAN ) THEN STRIP_TAC THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`u:real^3`]AZIM_EXISTS) THEN STRIP_TAC 
THEN
POP_ASSUM (fun th-> MP_TAC (ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]th)) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT DISCH_TAC
  THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1':real`; `psi':real`; `h1':real`]sincos_of_u_fan)
  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 

THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `h1':real`; `h1:real`; `r1':real`; `r1:real`;
`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`; `psi':real`; `y:real`  ] AZIM_UNIQUE)
  THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w2:real^3`; `h1':real`; `h2:real`; `r1':real`; `r2:real`;
`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`; `psi':real`; `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3) + azim x v w1 (w2:real^3)`  ] AZIM_UNIQUE) 
THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
THENL[ ASM_MESON_TAC[REAL_LE_ADD];


ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
     ]]));;
let sum3_azim_fan=
prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3. ((azim x v u w1 + azim x v w1 w2) < &2 * pi) /\ (~collinear {(x:real^3),(v:real^3),(w1:real^3)}) /\(~collinear {(x:real^3),(v:real^3),(w2:real^3)}) /\ (~collinear {(x:real^3),(v:real^3),(u:real^3)}) ==> azim x v u w2 = azim x v u w1+ azim x v w1 w2 `,
(
let th=prove(`!x v u. {x,v,u}={v,x,u}`,SET_TAC[]) in
 (let th1=prove(`!x v u. {x,v,u}={u,x,v}`,SET_TAC[]) in

REPEAT GEN_TAC THEN STRIP_TAC  THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a") 

THEN USE_THEN "a" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[th] THEN DISCH_THEN(LABEL_TAC "b")

THEN USE_THEN "a" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[th1] THEN DISCH_TAC

THEN USE_THEN "b" MP_TAC THEN
GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[COLLINEAR_3] THEN STRIP_TAC
THEN  
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]th3) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC (SPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`] azim) 
  THEN STRIP_TAC 
THEN POP_ASSUM(MP_TAC o SPECL [`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]) 
  THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
  THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
  THEN MP_TAC(SPEC `psi:real` SINCOS_PRINCIPAL_VALUE_FAN ) THEN STRIP_TAC THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`u:real^3`]AZIM_EXISTS) THEN STRIP_TAC 
THEN
POP_ASSUM (fun th-> MP_TAC (ISPECL[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]th)) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT DISCH_TAC
  THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1':real`; `psi':real`; `h1':real`]sincos_of_u_fan)
  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 

THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`; `h1':real`; `h1:real`; `r1':real`; `r1:real`;
`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`; `psi':real`; `y:real`  ] AZIM_UNIQUE)
  THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
THEN DISCH_TAC THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w2:real^3`; `h1':real`; `h2:real`; `r1':real`; `r2:real`;
`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`; `psi':real`; `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3) + azim x v w1 (w2:real^3)`  ] AZIM_UNIQUE) 
THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
THENL[
 ASM_MESON_TAC[REAL_LE_ADD];

ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]])));;
let sum2_azim_fan=
prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3. cyclic_set {u, w1, w2} x v /\ azim x v u w1 <= azim x v u w2 ==> azim x v u w2 = azim x v u w1 + azim x v w1 w2 `,
(
let th=prove(`!x v u. {v,x,u}={x,v,u}/\{v,x,u}={u,x,v}`,SET_TAC[]) in

REWRITE_TAC[REAL_ARITH`(a:real)=(b:real)+(c:real) <=> c=a-b`] THEN
REPEAT GEN_TAC THEN STRIP_TAC 
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN
MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set1) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`;`w1:real^3`; `w2:real^3`] property_of_cyclic_set2) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
  THEN MP_TAC(ISPECL[`v:real^3`; `x:real^3`; `u:real^3`]COLLINEAR_3) THEN ASM_REWRITE_TAC[] THEN
DISCH_TAC THEN  SUBGOAL_THEN `~collinear {(x:real^3),(v:real^3),(u:real^3)}/\ ~collinear {(u:real^3),(x:real^3),(v:real^3)}` ASSUME_TAC
THENL[ASM_MESON_TAC[th];
MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`] azim) 
  THEN STRIP_TAC 
THEN POP_ASSUM(MP_TAC o SPECL [`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]) 
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w2:real^3`] azim) THEN STRIP_TAC 
THEN POP_ASSUM(MP_TAC o SPECL [`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]) 
THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
  THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC 
  THEN DISCH_THEN (LABEL_TAC"a") THEN DISCH_THEN (LABEL_TAC"b")
THEN REPEAT STRIP_TAC
   THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
  THEN DISCH_THEN (LABEL_TAC"c") THEN REPEAT STRIP_TAC 
  THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1:real`; `psi:real`; `h1':real`]sincos_of_u_fan)
  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1':real`; `psi':real`; `h1:real`]sincos_of_u_fan)
  THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[] THEN  DISCH_TAC THEN DISCH_TAC
  THEN REMOVE_THEN "b" MP_TAC THEN REMOVE_THEN "c" MP_TAC
  THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
  THEN REPEAT STRIP_TAC 
  THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`; `h2:real`; `h2':real`; `r2':real`; `r2:real`;
`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`; `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)`; `azim (x:real^3) (v:real^3) (u:real^3) (w2:real^3) - azim x v u (w1:real^3)`  ] AZIM_UNIQUE) 
THEN DISCH_TAC THEN POP_ASSUM MATCH_MP_TAC 
THEN ASM_REWRITE_TAC[REAL_ARITH`(a:real)+(b:real)-a=b`; REAL_ARITH`(&0 <= (a:real)-(b:real))<=> b<= a`] THEN MP_TAC(ISPEC `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)` REAL_NEG_LE0) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
THEN MP_TAC(ISPECL[`azim (x:real^3) (v:real^3) (u:real^3) (w2:real^3)`;`&2 * pi`;`--azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)`;`&0`]REAL_LTE_ADD2 ) 
THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]));;
let sum4_azim_fan=
prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3. azim x v u w1 <= azim x v u w2 /\ (~collinear {(x:real^3),(v:real^3),(w1:real^3)}) /\(~collinear {(x:real^3),(v:real^3),(w2:real^3)}) /\ (~collinear {(x:real^3),(v:real^3),(u:real^3)}) ==> azim x v u w2 = azim x v u w1 + azim x v w1 w2 `,
(
let th=prove(`!x v u. {x,v,u}={v,x,u}`,SET_TAC[]) in
(let th1=prove(`!x v u. {x,v,u}={u,x,v}`,SET_TAC[]) in

REWRITE_TAC[REAL_ARITH`(a:real)=(b:real)+(c:real) <=> c=a-b`] THEN

REPEAT GEN_TAC THEN STRIP_TAC  THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "a1") 

THEN USE_THEN "a1" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[th] THEN DISCH_THEN(LABEL_TAC "b1")

THEN USE_THEN "a1" MP_TAC THEN GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[th1] THEN DISCH_TAC

THEN USE_THEN "b1" MP_TAC THEN
GEN_REWRITE_TAC ( LAND_CONV  o ONCE_DEPTH_CONV)[COLLINEAR_3] THEN STRIP_TAC
THEN
MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]th3) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w1:real^3`] azim) 
  THEN STRIP_TAC 
THEN POP_ASSUM(MP_TAC o SPECL [`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]) 
THEN MP_TAC (SPECL [`x:real^3`; `v:real^3`; `u:real^3`; `w2:real^3`] azim) THEN STRIP_TAC 
THEN POP_ASSUM(MP_TAC o SPECL [`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`]) 
THEN MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] orthonormal_e1_e2_e3_fan) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
MP_TAC(ISPECL[`(x:real^3)`; `(v:real^3)`; `(u:real^3)`] e3_mul_dist_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
  THEN ASM_REWRITE_TAC[]
THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC 
  THEN DISCH_THEN (LABEL_TAC"a") THEN DISCH_THEN (LABEL_TAC"b")
THEN REPEAT STRIP_TAC
   THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
  THEN DISCH_THEN (LABEL_TAC"c") THEN REPEAT STRIP_TAC 
  THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1:real`; `psi:real`; `h1':real`]sincos_of_u_fan)
  THEN ASM_REWRITE_TAC[] THEN DISCH_TAC
THEN MP_TAC(ISPECL[`x:real^3`; `v:real^3`; `u:real^3` ;`r1':real`; `psi':real`; `h1:real`]sincos_of_u_fan)
  THEN REMOVE_THEN "a" MP_TAC THEN ASM_REWRITE_TAC[] THEN  DISCH_TAC THEN DISCH_TAC
  THEN REMOVE_THEN "b" MP_TAC THEN REMOVE_THEN "c" MP_TAC
  THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;REAL_ARITH` &1 * (a:real) - &0 * (b:real)=a`;REAL_ARITH`&0 * (a:real) + &1 * (b:real)=b`]
  THEN REPEAT STRIP_TAC
  THEN MP_TAC (ISPECL [`x:real^3`; `v:real^3`; `w1:real^3`; `w2:real^3`; `h2:real`; `h2':real`; `r2':real`; `r2:real`;
`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3) (v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`; `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)`; `azim (x:real^3) (v:real^3) (u:real^3) (w2:real^3) - azim x v u (w1:real^3)`  ] AZIM_UNIQUE) 
THEN DISCH_TAC
THEN POP_ASSUM MATCH_MP_TAC
THEN ASM_REWRITE_TAC[REAL_ARITH`(a:real)+(b:real)-a=b`; REAL_ARITH`(&0 <= (a:real)-(b:real))<=> b<= a`] THEN MP_TAC(ISPEC `azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)` REAL_NEG_LE0) 
THEN ASM_REWRITE_TAC[] THEN DISCH_TAC 
THEN MP_TAC(ISPECL[`azim (x:real^3) (v:real^3) (u:real^3) (w2:real^3)`;`&2 * pi`;`--azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)`;`&0`]REAL_LTE_ADD2 ) 
THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC
)));;
let sum5_azim_fan=
prove(`!x:real^3 v:real^3 u:real^3 w1:real^3 w2:real^3. azim x v w1 w2 <= azim x v u w2 /\ (~collinear {(x:real^3),(v:real^3),(w1:real^3)}) /\(~collinear {(x:real^3),(v:real^3),(w2:real^3)}) /\ (~collinear {(x:real^3),(v:real^3),(u:real^3)}) ==> azim x v u w2 = azim x v u w1 + azim x v w1 w2 `,
REPEAT STRIP_TAC THEN REPEAT (POP_ASSUM MP_TAC) THEN DISCH_THEN(LABEL_TAC"1") THEN REPEAT STRIP_TAC THEN DISJ_CASES_TAC(REAL_ARITH`(azim x v u w2)= &0 \/ ~(azim x v u w2 = &0)`) THENL(*1*)[ SUBGOAL_THEN`azim x v w1 w2 = &0` ASSUME_TAC THENL(*2*)[ REPEAT(POP_ASSUM MP_TAC) THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`w2:real^3`]azim) THEN REAL_ARITH_TAC; (*2*) MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`w2:real^3`]AZIM_EQ_0_SYM) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`w2:real^3`]AZIM_EQ_0_SYM) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN SUBGOAL_THEN`azim x v w2 w1 = azim x v w2 u` ASSUME_TAC THENL(*3*)[ASM_MESON_TAC[];(*3*) REWRITE_TAC[REAL_ARITH`&0 = a + &0 <=> a= &0`] THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w2:real^3`;`u:real^3`;`w1:real^3`]AZIM_EQ_ALT) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`w1:real^3`]AZIM_EQ_0) THEN ASM_REWRITE_TAC[]]]; DISJ_CASES_TAC(REAL_ARITH`(azim x v w1 w2)= &0 \/ ~(azim x v w1 w2 = &0)`) THENL(*4*)[ ASM_REWRITE_TAC[REAL_ARITH`b = a + &0 <=> b= a`] THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`w2:real^3`]AZIM_EQ_0_ALT) THEN ASM_REWRITE_TAC[]THEN ASM_MESON_TAC[AZIM_EQ_ALT] ;(*4*) REMOVE_THEN"1" MP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`w2:real^3`]AZIM_COMPL ) THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`;`w2:real^3`]AZIM_COMPL ) THEN ASM_REWRITE_TAC[REAL_ARITH`a=b-c <=> c= b-a`] THEN DISCH_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_ARITH`a-b=c+a-d<=> d=b+c`;REAL_ARITH`a-b<=a-d<=> d<=b`] THEN ASM_MESON_TAC[sum4_azim_fan]] ]);;
(****************************************************************************) (* sigma_fan is permutes *) (****************************************************************************)
let  SUR_SIGMA_FAN=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3). FAN(x,V,E) /\ ({v,u} IN E) ==> ?w. {v,w} IN E /\sigma_fan x V E v w= u `,
REPEAT GEN_TAC THEN STRIP_TAC THEN DISJ_CASES_TAC(SET_RULE `(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(u:real^3)})\/ ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(u:real^3)})`) THENL(*1*)[ EXISTS_TAC`u:real^3` THEN ASM_REWRITE_TAC[sigma_fan];(*1*) MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]properties_of_set_of_edge_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]exists_inverse_sigma_fan_alt) THEN ASM_REWRITE_TAC[azim1;] THEN STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`]properties_of_set_of_edge_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN EXISTS_TAC `w:real^3` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;` (u:real^3)`] UNIQUE_SIGMA_FAN) THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC "be") THEN DISCH_TAC THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={w} \/ ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={w})`) THENL(*2*)[ FIND_ASSUM(MP_TAC)`u:real^3 IN set_of_edge v V E` THEN POP_ASSUM(fun th->REWRITE_TAC[th;IN_SING]) THEN ASM_TAC THEN SET_TAC[] ;(*2*) ASM_REWRITE_TAC[] THEN GEN_TAC THEN STRIP_TAC THEN DISJ_CASES_TAC(SET_RULE`~(azim (x:real^3) v w u <= azim x v w w1)\/ (azim (x:real^3) v w u <= azim x v w w1)`) THENL(*3*)[ ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`azim (x:real^3) v w w1 <= azim x v w u` ASSUME_TAC THENL(*4*)[ POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;(*4*) SUBGOAL_THEN `{(w:real^3),(w1:real^3),(u:real^3)} SUBSET set_of_edge v V E` ASSUME_TAC THENL(*5*)[ ASM_TAC THEN SET_TAC[];(*5*) FIND_ASSUM(MP_TAC)`FAN((x:real^3),V,E)` THEN REWRITE_TAC[FAN;fan6] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC "b") THEN STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`;` (v:real^3)`]properties_of_graph) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`]CYCLIC_SET_EDGE_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`{(w:real^3), (w1:real^3),(u:real^3)}`;`set_of_edge(v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)` ]subset_cyclic_set_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`;`w1:real^3`;`u:real^3`]sum2_azim_fan) THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w:real^3`;`w1:real^3`]azim) THEN STRIP_TAC THEN STRIP_TAC THEN SUBGOAL_THEN`azim (x:real^3) v w1 u <= azim x v w u` ASSUME_TAC THENL(*6*)[ REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;(*6*) POP_ASSUM MP_TAC THEN POP_ASSUM(fun th->REWRITE_TAC[]) THEN ASM_REWRITE_TAC[] THEN MP_TAC (ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(w1:real^3)`]properties_of_set_of_edge) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN REMOVE_THEN "b" (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th)) THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th)) THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),w1}`th) THEN ASSUME_TAC(th)) THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3)= &0) \/ ~(azim (x:real^3) (v:real^3) (u:real^3) (w1:real^3) = &0)`) THENL(*7*)[ MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;`w1:real^3`]UNIQUE_AZIM_0_POINT_FAN) THEN ASM_TAC THEN SET_TAC[];(*7*) DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3) (v:real^3) (u:real^3) (w:real^3)= &0) \/ ~(azim (x:real^3) (v:real^3) (u:real^3) (w:real^3) = &0)`) THENL(*8*)[ MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;`w:real^3`]UNIQUE_AZIM_0_POINT_FAN) THEN ASM_TAC THEN SET_TAC[];(*8*) MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;` (w1:real^3)`]AZIM_COMPL) THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (u:real^3)`;` (w:real^3)`]AZIM_COMPL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN FIND_ASSUM(MP_TAC o (SPEC`w1:real^3`))`!w1:real^3. w1 IN set_of_edge v V E /\ ~(w1 = u) ==> &2 * pi - azim x v u w <= &2 * pi - azim x v u w1` THEN REMOVE_THEN "be" MP_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC(SET_RULE`~(w1:real^3=u)\/ (w1=u)`) THENL(*9*)[ ASM_REWRITE_TAC[REAL_ARITH`&2 * pi -(a:real)<= &2 *pi - b <=> b <= a`] THEN DISJ_CASES_TAC(SET_RULE `(azim(x:real^3) v u w =azim x v u w1)\/ ~(azim(x:real^3) v u w =azim x v u w1)`) THENL(*10*)[ MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`;` (w:real^3)`;`(w1:real^3)`]UNIQUE_AZIM_POINT_FAN) THEN ASM_REWRITE_TAC[];(*10*) POP_ASSUM MP_TAC THEN REAL_ARITH_TAC](*10*);(*9*) SUBGOAL_THEN `azim (x:real^3) v w u= azim x v w w1` ASSUME_TAC THENL(*10*)[POP_ASSUM(fun th->REWRITE_TAC[th]);(*10*) REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC](*10*)(*9*)](*8*)](*7*)](*6*)](*5*)](*4*)](*3*); ASM_TAC THEN SET_TAC[]]]]);;
let MONO_SIGMA_FAN=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3) (w:real^3). FAN(x,V,E) /\ ({v,u} IN E) /\ ({v,w} IN E)/\ (sigma_fan x V E v u= sigma_fan x V E v w) ==> u=w `,
REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"1") THEN USE_THEN "1" MP_TAC THEN REWRITE_TAC[FAN;fan6] THEN REPEAT STRIP_TAC THEN REPEAT(POP_ASSUM MP_TAC) THEN DISCH_THEN (LABEL_TAC"1") THEN DISCH_THEN (LABEL_TAC"a") THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_THEN(LABEL_TAC "b") THEN REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`;` (v:real^3)`]properties_of_graph) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISJ_CASES_TAC(SET_RULE`(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(u:real^3)})\/ ~((set_of_edge v V E={u}))`) THENL(*1*)[ POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[set_of_edge; EXTENSION;IN_ELIM_THM] THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`w:real^3`th)) THEN ASM_REWRITE_TAC[] THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS;SUBSET; IN_ELIM_THM] THEN DISCH_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`w:real^3`th)) THEN ASM_REWRITE_TAC[IN_SING;LEFT_IMP_EXISTS_THM] THEN STRIP_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`{(v:real^3),(w:real^3)}`th)) THEN ASM_TAC THEN SET_TAC[];(*1*) DISJ_CASES_TAC(SET_RULE`(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(w:real^3)})\/ ~((set_of_edge v V E={w}))`) THENL(*2*)[ POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[set_of_edge; EXTENSION;IN_ELIM_THM] THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`u:real^3`th)) THEN ASM_REWRITE_TAC[] THEN REMOVE_THEN "a" MP_TAC THEN REWRITE_TAC[UNIONS;SUBSET; IN_ELIM_THM] THEN DISCH_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`u:real^3`th)) THEN ASM_REWRITE_TAC[IN_SING;LEFT_IMP_EXISTS_THM] THEN STRIP_TAC THEN POP_ASSUM (fun th->MP_TAC(ISPEC`{(v:real^3),(u:real^3)}`th)) THEN ASM_TAC THEN SET_TAC[];(*2*) MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (u:real^3)`]properties_of_set_of_edge) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (w:real^3)`]properties_of_set_of_edge) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]SIGMA_FAN) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(w:real^3)`th)) THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`]SIGMA_FAN) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(u:real^3)`th)) THEN ASM_REWRITE_TAC[] THEN MP_TAC (ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]properties_of_set_of_edge) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN REMOVE_THEN "b" (fun th->MP_TAC (ISPEC`{(v:real^3),(w:real^3)}`th) THEN ASSUME_TAC(th)) THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(u:real^3)}`th) THEN ASSUME_TAC(th)) THEN POP_ASSUM (fun th->MP_TAC (ISPEC`{(v:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3))}`th) THEN ASSUME_TAC(th)) THEN REWRITE_TAC[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISJ_CASES_TAC(SET_RULE`~((u:real^3)=(w:real^3))\/ u=w`) THENL(*3*)[ ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `{(w:real^3),(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)),(u:real^3)}SUBSET set_of_edge v V E` ASSUME_TAC THENL(*4*)[ ASM_TAC THEN SET_TAC[];(*4*) MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`]CYCLIC_SET_EDGE_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`{(w:real^3), (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)),(u:real^3)}`;`set_of_edge(v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)` ]subset_cyclic_set_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`;` (u:real^3)`]sum2_azim_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (LABEL_TAC "c") THEN DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3) (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))= &0) \/ ~(azim (x:real^3) (v:real^3) (w:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) = &0)`) THENL(*5*)[ MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`]UNIQUE_AZIM_0_POINT_FAN) THEN ASM_TAC THEN SET_TAC[];(*5*) DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3) (v:real^3) (w:real^3) (u:real^3)= &0) \/ ~(azim (x:real^3) (v:real^3) (w:real^3) (u:real^3) = &0)`) THENL(*6*)[ MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (w:real^3)`;`(u:real^3)`]UNIQUE_AZIM_0_POINT_FAN) THEN ASM_TAC THEN SET_TAC[];(*6*) DISJ_CASES_TAC(REAL_ARITH `(azim (x:real^3) (v:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) (u:real^3)= &0) \/ ~(azim (x:real^3) (v:real^3) (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)) (u:real^3) = &0)`) THENL(*7*)[ MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`;` (u:real^3)`]UNIQUE_AZIM_0_POINT_FAN) THEN ASM_TAC THEN SET_TAC[];(*7*) MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`;` (u:real^3)`]AZIM_COMPL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;` (w:real^3)`;` (u:real^3)`]AZIM_COMPL) THEN ASM_REWRITE_TAC[REAL_ARITH`&2 * pi - ((a:real)+(b:real))= --(a:real)+ (&2 * pi - b)`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_ARITH`b <= (a:real)+(b:real)<=> &0 <= a`] THEN MP_TAC(ISPECL[`(x:real^3)`;` (v:real^3)`;`(w:real^3)`;`(sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3))`] azim)THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC (*7*)](*6*)](*5*)](*4*)];(*3*) ASM_REWRITE_TAC[](*3*)]]]);;
let permutes_sigma_fan=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (u:real^3). FAN(x,V,E) /\ ({v,u} IN E) ==> (extension_sigma_fan x V E v) permutes (set_of_edge v V E)`,
REPEAT GEN_TAC THEN STRIP_TAC THEN FIND_ASSUM(MP_TAC)`FAN((x:real^3), V, E)` THEN REWRITE_TAC[FAN;fan1] THEN STRIP_TAC THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`]remark_finite_fan1) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`;`extension_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)`]PERMUTES_FINITE_INJECTIVE) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL[ GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan]; STRIP_TAC THENL[ GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan] THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(x':real^3)}\/ ~(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)={(x':real^3)})`) THENL[ASM_REWRITE_TAC[sigma_fan;IN_SING]; ASM_MESON_TAC[SIGMA_FAN]]; REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[extension_sigma_fan] THEN DISCH_TAC THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (x':real^3)`]properties_of_set_of_edge) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN MP_TAC(ISPECL[`(v:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (y:real^3)`]properties_of_set_of_edge) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_MESON_TAC[MONO_SIGMA_FAN]]]);;
(****************************************************************************) (* inverse of sigma_fan *) (****************************************************************************)
let exists_function_inverse_sigma_fan_alt=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3). FAN(x,V,E) ==> (?g. (!w:real^3. {v,w} IN E==> {v, g w} IN E) /\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( g w) =w) /\ (!w:real^3. {v,w} IN E==> g (sigma_fan x V E v w) =w)) `,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] sigma_fan_in_set_of_edge) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)`;`set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`; `set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool)`]BIJECTIVE_ON_LEFT_RIGHT_INVERSE) THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] properties_of_set_of_edge_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] MONO_SIGMA_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`] SUR_SIGMA_FAN) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]);;
(* This is the same as inverse_sigma_fan_alt, but easier to use. *)
let inverse1_sigma_fan=new_definition`inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3)= @g. (!w:real^3. {v,w} IN E==> {v, g w} IN E)
/\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( g w) =w)
/\ (!w:real^3. {v,w} IN E==> g (sigma_fan x V E v w) =w)`;;
let INVERSE1_SIGMA_FAN=
prove(`!(x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3). FAN(x,V,E) ==> ( (!w:real^3. {v,w} IN E==> {v, inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) w} IN E) /\ (!w:real^3. {v,w} IN E==> (sigma_fan x V E v)( inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) w) =w) /\ (!w:real^3. {v,w} IN E==> inverse1_sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (sigma_fan x V E v w) =w))`,
REPEAT GEN_TAC THEN STRIP_TAC THEN ONCE_REWRITE_TAC[inverse1_sigma_fan] THEN MP_TAC(ISPECL[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3) `]exists_function_inverse_sigma_fan_alt) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN SELECT_ELIM_TAC THEN EXISTS_TAC`g:real^3->real^3` THEN ASM_REWRITE_TAC[]);;
(* This is the same as f_fan, but easier to use *)
let f1_fan=new_definition`f1_fan (x:real^3) V E = (\((x:real^3),(v:real^3),(w:real^3),(w1:real^3)). (x,w,(inverse1_sigma_fan x V E w v),v) )`;;
(* Proof Lemma 6.1 [AAUHTVE] *)
let node_fan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) n:num. power_maps n_fan x V E n=power_n_fan x V E n`,
GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[power_maps; n_fan; power_n_fan; power_map_points] THEN INDUCT_TAC THEN REWRITE_TAC[power_maps; power_map_points;i_fan;] THEN REWRITE_TAC[power_map_points; power_maps] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[n_fan;o_funs; pr1; pr2; pr3; pr4]);;
let EQ_PAIR_4=
prove(`!a:real^3 b:real^3 c:real^3 d:real^3 a1:real^3 b1:real^3 c1:real^3 d:real^3. (a,b,c,d)=(a1,b1,c1,d1) <=> a=a1 /\ b=b1 /\ c=c1 /\ d=d1`,
REPEAT GEN_TAC THEN EQ_TAC THENL[ DISCH_TAC THEN MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr1(a,b,c,d)=pr1(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr1] THEN MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr2(a,b,c,d)=pr2(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr2] THEN MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr3(a,b,c,d)=pr3(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr3] THEN MP_TAC(SET_RULE`(a,b,c,d)=(a1,b1,c1,d1)==>pr4(a,b,c,d)=pr4(a1,b1,c1,d1)`) THEN REWRITE_TAC[pr4] THEN ASM_REWRITE_TAC[] THEN SET_TAC[]; SET_TAC[]]);;
let MONO_N_FAN=
prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FAN(x,V,E) ==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ n_fan x V E a =n_fan x V E b ==> a=b)`,
REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[n_fan;EQ_PAIR_4] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM (fun th -> REWRITE_TAC[]) THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`x:real^3`; `(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`;`w:real^3`;`v:real^3` ]remark1_fan) THEN ASM_REWRITE_TAC[] THEN MP_TAC(ISPECL[`x:real^3`; `(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`;`w':real^3`;`v:real^3` ]remark1_fan) THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[MONO_SIGMA_FAN;]);;
let SUR_N_FAN=
prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FAN(x,V,E) ==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ n_fan x V E b = a))`,
REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`v:real^3`;`w:real^3`] SUR_SIGMA_FAN) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN EXISTS_TAC`(x:real^3,v:real^3,w':real^3,w:real^3)` THEN ASM_REWRITE_TAC[n_fan] THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`w':real^3` THEN EXISTS_TAC`w:real^3` THEN ASM_REWRITE_TAC[]);;
let simp_inverse_sigma_fan_alt=
prove(`!x V E v w. inverse_sigma_fan_alt x V E v w= inverse (sigma_fan x V E v) w`,
REWRITE_TAC[inverse] THEN MESON_TAC[inverse_sigma_fan_alt]);;
let SUR_F1_FAN=
prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FAN(x,V,E) ==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ f1_fan x V E b = a))`,
REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN EXISTS_TAC`(x:real^3,sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) v w, v:real^3,sigma_fan x V E (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) v w) v)` THEN ASM_REWRITE_TAC[f_fan;EQ_PAIR_4;] THEN STRIP_TAC THENL[ EXISTS_TAC`x:real^3` THEN EXISTS_TAC`sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) v w` THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`sigma_fan x V E (sigma_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) v w) v` THEN ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC(SET_RULE`(set_of_edge (v:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) ={w:real^3}) \/ ~(set_of_edge v V E ={w})`) THENL[ REWRITE_TAC[sigma_fan;SET_RULE`{a,b}={b,a}`] THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[]) THEN POP_ASSUM (fun th-> REWRITE_TAC[]) THEN POP_ASSUM (fun th-> REWRITE_TAC[th]); MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`w:real^3`;`v:real^3`]remark1_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`v:real^3`;`w:real^3`]SIGMA_FAN) THEN ASM_REWRITE_TAC[remark1_fan] THEN STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`sigma_fan x V E v w:real^3`;`v:real^3`]remark1_fan) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[]) THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`]]; REWRITE_TAC[f1_fan] THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`v:real^3`]INVERSE1_SIGMA_FAN) THEN ASM_REWRITE_TAC[EQ_PAIR_4] THEN STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`w:real^3`th)) THEN ASM_REWRITE_TAC[]]);;
let MONO_F1_FAN=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FAN(x,V,E) ==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ f1_fan x V E a =f1_fan x V E b ==> a=b)`,
REWRITE_TAC[d1_fan;IN_ELIM_THM]THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[f1_fan;EQ_PAIR_4] THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;
let MONO_E_FAN=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FAN(x,V,E) ==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ e_fan x V E a =e_fan x V E b ==> a=b)`,
REWRITE_TAC[d1_fan;IN_ELIM_THM]THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[e_fan;EQ_PAIR_4] THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;
let SUR_E_FAN=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FAN(x,V,E) ==> (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ e_fan x V E b = a))`,
REWRITE_TAC[d1_fan; IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN EXISTS_TAC`(x:real^3,w:real^3,v:real^3, sigma_fan x (V:real^3->bool) (E:(real^3->bool)->bool) w v)` THEN ASM_REWRITE_TAC[e_fan] THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`w:real^3` THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`sigma_fan x (V:real^3->bool) (E:(real^3->bool)->bool) w v` THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`]);;
let permuters_of_enf_fan=
prove(` !x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FAN(x,V,E) ==> (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ n_fan x V E a =n_fan x V E b ==> a=b) /\ (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ n_fan x V E b = a)) /\ (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ f1_fan x V E a =f1_fan x V E b ==> a=b) /\ (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ f1_fan x V E b = a)) /\ (!a b. a IN d1_fan(x,V,E) /\ b IN d1_fan (x,V,E)/\ e_fan x V E a =e_fan x V E b ==> a=b) /\ (!a. a IN d1_fan(x,V,E) ==>(?b. b IN d1_fan(x,V,E) /\ e_fan x V E b = a)) `,
let condition_hypermap_fan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E)==> e_fan x V E((n_fan x V E) (f1_fan x V E a))=a)`,
REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[f1_fan;n_fan; e_fan; EQ_PAIR_4] THEN MP_TAC(ISPECL[`x:real^3`;` (V:real^3->bool)`; `(E:(real^3->bool)->bool)`;`w:real^3`]INVERSE1_SIGMA_FAN) THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN POP_ASSUM (fun th->REWRITE_TAC[]) THEN POP_ASSUM (fun th-> MP_TAC(ISPEC`v:real^3`th)) THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[]);;
let plain_hypermap_fan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E)==> (e_fan x V E) (e_fan x V E a) =a)`,
REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[e_fan; EQ_PAIR_4]);;
let e_fan_no_fix_point=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a=a ))`,
REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[e_fan; EQ_PAIR_4] THEN STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]remark1_fan) THEN ASM_MESON_TAC[]);;
let f_fan_no_fix_point=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FAN(x,V,E)==> (!a. a IN d1_fan(x,V,E) ==> ~(f1_fan x V E a=a ))`,
REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[f1_fan; EQ_PAIR_4] THEN STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]remark1_fan) THEN ASM_MESON_TAC[]);;
(* from hypermap.hl *) (******************************) parse_as_infix("POWER",(24,"right"));;
let POWER = new_recursive_definition num_RECURSION 
 `(!(f:A->A). f POWER 0  = I) /\  
  (!(f:A->A) (n:num). f POWER (SUC n) = (f POWER n) o f)`;;
let POWER_0 = 
prove(`!f:A->A. f POWER 0 = I`,
REWRITE_TAC[POWER]);;
let POWER_1 = 
prove(`!f:A->A. f POWER 1 = f`,
REWRITE_TAC[POWER; ONE; I_O_ID]);;
let POWER_2 = 
prove(`!f:A->A. f POWER 2 = f o f`,
REWRITE_TAC[POWER; TWO; POWER_1]);;
let orbit_map = new_definition `orbit_map (f:A->A)  (x:A) = {(f POWER n) x | n >= 0}`;;
(**************************************************)
let POWER_RIGHT=
prove(`!k:num f:A->A. f POWER SUC(k) = f o (f POWER k)`,
INDUCT_TAC THENL[REWRITE_TAC[POWER;o_DEF; I_DEF]; REWRITE_TAC[POWER;o_ASSOC] THEN GEN_TAC THEN POP_ASSUM(fun th -> MP_TAC(SPEC`f:A->A`th)) THEN DISCH_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th);POWER])]) ;;
let power_n_fan=
prove(`!l:num x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 w:real^3. FAN(x,V,E)/\ ({v,w} IN E)==> (n_fan (x:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) POWER l) (x,v,w,sigma_fan x V E v w)= (x,v, power_map_points sigma_fan x V E v w l, power_map_points sigma_fan x V E v w (SUC l) )`,
INDUCT_TAC THENL[REWRITE_TAC[POWER; power_map_points;I_DEF]; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"a") THEN REPEAT STRIP_TAC THEN REMOVE_THEN "a" (fun th -> MP_TAC(ISPECL[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`(v:real^3)`;`(w:real^3)`]th)) THEN ASM_REWRITE_TAC[POWER_RIGHT; o_DEF;] THEN DISCH_TAC THEN ASM_REWRITE_TAC[n_fan;power_map_points] ]);;
let distinct_nodes=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) . FAN(x,V,E)==> (!k:num l:num a. a IN d1_fan(x,V,E) ==> (((n_fan x V E) POWER k) o (e_fan x V E)) a= ((e_fan x V E)o((n_fan x V E) POWER l)) a==> (n_fan x V E POWER l) a=a)`,
REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[o_DEF;e_fan] THEN MP_TAC(ISPECL[`l:num`;` x:real^3 `;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` v:real^3`;` w:real^3`]power_n_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC(ISPECL[`k:num`;` x:real^3 `;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` w:real^3`;` v:real^3`]power_n_fan) THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={b,a}`] THEN DISCH_TAC THEN ASM_REWRITE_TAC[EQ_PAIR_4] THEN STRIP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[]) THEN POP_ASSUM(fun th-> REWRITE_TAC[]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]THEN ASSUME_TAC(th)) THEN ASM_REWRITE_TAC[power_map_points] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]));;
let edge_lie_different_nodes=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FAN(x,V,E)==> (!n:num a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a =(n_fan x V E POWER n) a)) `,
REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[e_fan] THEN MP_TAC(ISPECL[`n:num`;` x:real^3 `;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` v:real^3`;` w:real^3`]power_n_fan) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN ASM_REWRITE_TAC[EQ_PAIR_4] THEN STRIP_TAC THEN MP_TAC(ISPECL[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]remark1_fan) THEN ASM_MESON_TAC[]);;
(**********************)
let d20_fan=new_definition`d20_fan (x,V,E)={ (x',v,v,v)| (x'=x) /\ (V v) /\ ((set_of_edge v V E) ={})}`;;
let d_fan=new_definition`d_fan (x,V,E)= d1_fan (x,V,E) UNION d20_fan (x,V,E)`;;
let hypermap_of_fanx = new_definition
  `hypermap_of_fanx (x:real^3,V:real^3->bool,E:(real^3->bool)->bool) = 
    (let p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) in 
          hypermap( d_fan (x,V,E) , p e_fan, p n_fan, p f_fan))`;;
let hypermap1_of_fanx = new_definition
  `hypermap1_of_fanx (x:real^3,V:real^3->bool,E:(real^3->bool)->bool) = 
    (let p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) in 
          hypermap( d_fan (x,V,E) , p e_fan, p n_fan, p f1_fan))`;;
let finite_d1_fan=
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool). FAN(x,V,E) ==> FINITE (d1_fan (x,V,E))`,
REPEAT GEN_TAC THEN DISCH_THEN(LABEL_TAC"EM") THEN USE_THEN "EM" MP_TAC THEN REWRITE_TAC[FAN;fan1] THEN STRIP_TAC THEN MRESA_TAC set_edges_is_finite_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN MRESA_TAC FINITE_PRODUCT[`V:real^3->bool`;`V:real^3->bool`] THEN MRESA_TAC FINITE_IMAGE[`(\(a,b:real^3). (x,a,b,sigma_fan x V E a b))`;`{x,y | x IN (V:real^3->bool) /\ y IN V}`] THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC`(IMAGE (\(a,b). x,a,b,sigma_fan x V E a b) {x,y | x IN V /\ y IN (V:real^3->bool)})` THEN ASM_REWRITE_TAC[IMAGE;IN_ELIM_THM;d1_fan;SUBSET] THEN REPEAT STRIP_TAC THEN EXISTS_TAC`(v:real^3,w:real^3)` THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`w:real^3` THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` w:real^3`;`v:real^3`] THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` v:real^3`;`w:real^3`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;
let finite_d20_fan=
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool). FAN(x,V,E) ==> FINITE (d20_fan (x,V,E))`,
REPEAT GEN_TAC THEN DISCH_THEN(LABEL_TAC"EM") THEN USE_THEN "EM" MP_TAC THEN REWRITE_TAC[FAN;fan1] THEN STRIP_TAC THEN MRESA_TAC FINITE_IMAGE[`(\b:real^3. (x:real^3,b,b,b))`;`V:real^3->bool`] THEN MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC`(IMAGE (\b:real^3. (x:real^3,b,b,b)) (V:real^3->bool))` THEN ASM_REWRITE_TAC[d20_fan;SUBSET;IMAGE;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN EXISTS_TAC`v:real^3` THEN ASM_REWRITE_TAC[IN]);;
let finite_d_fan=
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool). FAN(x,V,E) ==> FINITE (d_fan (x,V,E))`,
REPEAT STRIP_TAC THEN REWRITE_TAC[d_fan;FINITE_UNION] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[finite_d1_fan;finite_d20_fan]);;
let subset_d_fan=
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool). d1_fan (x,V,E) SUBSET d_fan (x,V,E) /\ d20_fan (x,V,E) SUBSET d_fan(x,V,E)`,
REWRITE_TAC[d_fan] THEN SET_TAC[]);;
let FACE_FAN_NOT_EMPTY=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds s. FAN(x,V,E) /\ ds IN face_set(hypermap1_of_fanx (x,V,E)) ==> ~(ds={})`,
REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC lemma_face_representation[`hypermap1_of_fanx(x:real^3,V,E)`;`ds:real^3#real^3#real^3#real^3->bool`] THEN MRESA_TAC FACE_FINITE[`hypermap1_of_fanx(x:real^3,V,E)`;`x':real^3#real^3#real^3#real^3`] THEN STRIP_TAC THEN MRESA1_TAC CARD_EQ_0`face (hypermap1_of_fanx (x:real^3,V,E)) x'` THEN MRESA_TAC FACE_NOT_EMPTY[`hypermap1_of_fanx(x:real^3,V,E)`;`x':real^3#real^3#real^3#real^3`] THEN POP_ASSUM MP_TAC THEN ARITH_TAC);;
let into_domain_e_fan=
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool). FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) ==> (!y. y IN d_fan (x,V,E)==> ((p e_fan ) y) IN (d_fan (x,V,E)))`,
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[res;] THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`) THENL[ ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[e_fan;d1_fan;IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN MATCH_MP_TAC(SET_RULE`x,w,v,sigma_fan x V E w v IN d1_fan (x,V,E) /\ d1_fan (x,V,E) SUBSET d_fan (x,V,E) ==>x,w,v,sigma_fan x V E w v IN d_fan (x:real^3,V,E)`) THEN ASM_REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`w:real^3` THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`sigma_fan x V E w (v:real^3)` THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_REWRITE_TAC[]]);;
let into_domain1_e_fan=
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool). FAN(x,V,E) ==> (!y. y IN d1_fan (x,V,E)==> (e_fan x V E y IN d1_fan (x,V,E)))`,
REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[e_fan;d1_fan;IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`w:real^3` THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`sigma_fan x V E w (v:real^3)` THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_REWRITE_TAC[]);;
let e_fan_permutes=
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool). FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) ==> (p e_fan) permutes (d_fan (x,V,E))`,
REPEAT STRIP_TAC THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN MRESA_TAC PERMUTES_FINITE_SURJECTIVE[`d_fan (x:real^3,V,E)`;`res (e_fan x V E) (d1_fan (x:real^3,V,E))`] THEN STRIP_TAC THENL[ REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]; MRESA_TAC into_domain_e_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`) THENL[EXISTS_TAC`y:real^3#real^3#real^3#real^3` THEN ASM_REWRITE_TAC[res]; MRESA_TAC permuters_of_enf_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN POP_ASSUM (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`) THEN REWRITE_TAC[res] THEN EXISTS_TAC`b:real^3#real^3#real^3#real^3` THEN ASM_REWRITE_TAC[] THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN ASM_TAC THEN SET_TAC[]]]);;
let into_domain_f1_fan= 
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool). FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) ==> (!y. y IN d_fan (x,V,E)==> ((p f1_fan ) y) IN (d_fan (x,V,E)))`,
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[res;] THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`) THENL[ ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[f1_fan;d1_fan;IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN MATCH_MP_TAC(SET_RULE`x,w,inverse1_sigma_fan x V E w v,v IN d1_fan (x,V,E) /\ d1_fan (x,V,E) SUBSET d_fan (x,V,E) ==>x,w,inverse1_sigma_fan x V E w v,v IN d_fan (x:real^3,V,E)`) THEN ASM_REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`w:real^3` THEN EXISTS_TAC`inverse1_sigma_fan x V E w v:real^3` THEN EXISTS_TAC`(v:real^3)` THEN ASM_REWRITE_TAC[] THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`w:real^3`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`) THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN RESA_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]) THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`) THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_REWRITE_TAC[]]);;
let into_domain1_f1_fan= 
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool). FAN(x,V,E)==> (!y. y IN d1_fan (x,V,E)==> (f1_fan x V E y IN d1_fan (x,V,E)))`,
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[f1_fan;d1_fan;IN_ELIM_THM] THEN STRIP_TAC THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`w:real^3` THEN EXISTS_TAC`inverse1_sigma_fan x V E w v:real^3` THEN EXISTS_TAC`(v:real^3)` THEN ASM_REWRITE_TAC[] THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`w:real^3`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`) THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN RESA_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM(th)]) THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`) THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_REWRITE_TAC[]);;
let f1_fan_permutes=
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool). FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) ==> (p f1_fan) permutes (d_fan (x,V,E))`,
REPEAT STRIP_TAC THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN MRESA_TAC PERMUTES_FINITE_SURJECTIVE[`d_fan (x:real^3,V,E)`;`res (f1_fan x V E) (d1_fan (x:real^3,V,E))`] THEN STRIP_TAC THENL[ REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]; MRESA_TAC into_domain_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`) THENL[ EXISTS_TAC`y:real^3#real^3#real^3#real^3` THEN ASM_REWRITE_TAC[res]; MRESA_TAC permuters_of_enf_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`) THEN REWRITE_TAC[res] THEN EXISTS_TAC`b:real^3#real^3#real^3#real^3` THEN ASM_REWRITE_TAC[] THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN ASM_TAC THEN SET_TAC[]]]);;
let into_domain_n_fan= 
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool). FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) ==> (!y. y IN d_fan (x,V,E)==> ((p n_fan ) y) IN (d_fan (x,V,E)))`,
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[res;] THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`) THENL[ ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[n_fan;d1_fan;IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN MATCH_MP_TAC(SET_RULE`x,v,sigma_fan x V E v w,sigma_fan x V E v (sigma_fan x V E v w) IN d1_fan (x,V,E) /\ d1_fan (x,V,E) SUBSET d_fan (x,V,E) ==>x,v,sigma_fan x V E v w,sigma_fan x V E v (sigma_fan x V E v w) IN d_fan (x:real^3,V,E)`) THEN ASM_REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`sigma_fan x V E v w:real^3` THEN EXISTS_TAC`sigma_fan x V E v (sigma_fan x V E v (w:real^3))` THEN ASM_REWRITE_TAC[] THEN MRESA_TAC sigma_fan_in_set_of_edge[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`] THEN POP_ASSUM MP_TAC THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`] THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`(sigma_fan x V E v (w:real^3)):real^3`]]);;
let into_domain1_n_fan= 
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool). FAN(x,V,E) ==> (!y. y IN d1_fan (x,V,E)==> (n_fan x V E y IN d1_fan (x,V,E)))`,
REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[n_fan;d1_fan;IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`x:real^3` THEN EXISTS_TAC`v:real^3` THEN EXISTS_TAC`sigma_fan x V E v w:real^3` THEN EXISTS_TAC`sigma_fan x V E v (sigma_fan x V E v (w:real^3))` THEN ASM_REWRITE_TAC[] THEN MRESA_TAC sigma_fan_in_set_of_edge[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`] THEN POP_ASSUM MP_TAC THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`] THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`(sigma_fan x V E v (w:real^3)):real^3`]);;
let n_fan_permutes=
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool). FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) ==> (p n_fan) permutes (d_fan (x,V,E))`,
REPEAT STRIP_TAC THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN MRESA_TAC PERMUTES_FINITE_SURJECTIVE[`d_fan (x:real^3,V,E)`;`res (n_fan x V E) (d1_fan (x:real^3,V,E))`] THEN STRIP_TAC THENL[ REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]; MRESA_TAC into_domain_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SET_RULE`~(y IN d1_fan (x,V,E) )\/ (y IN d1_fan (x:real^3,V,E))`) THENL[ EXISTS_TAC`y:real^3#real^3#real^3#real^3` THEN ASM_REWRITE_TAC[res]; MRESA_TAC permuters_of_enf_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`) THEN REWRITE_TAC[res] THEN EXISTS_TAC`b:real^3#real^3#real^3#real^3` THEN ASM_REWRITE_TAC[] THEN MRESA_TAC subset_d_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN ASM_TAC THEN SET_TAC[]]]);;
let id_enf_fan=
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) y:real^3#real^3#real^3#real^3. FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) /\ ~(y IN d1_fan (x,V,E)) ==> (p e_fan) y=y /\ (p n_fan) y=y/\ (p f1_fan) y=y`,
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[res;d_fan;UNION;IN_ELIM_THM;DE_MORGAN_THM]);;
let id_power_enf_fan=
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) y:real^3#real^3#real^3#real^3 n:num p. FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) /\ ~(y IN d1_fan (x,V,E)) ==> ((p e_fan) POWER n) y=y /\ ((p n_fan) POWER n)y=y/\ ((p f1_fan) POWER n) y=y`,
(
let lem=prove(`!f:A->A x:A. f x = x ==> !m. (f POWER m) x = x`,
MRESA_TAC power_map_fix_point[`1:num`]
THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[POWER_1;ARITH_RULE`m*1=m:num`]) in
REPEAT STRIP_TAC
THEN MRESA_TAC id_enf_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`y:real^3#real^3#real^3#real^3`]
THEN MRESA_TAC lem[`(p e_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`y:real^3#real^3#real^3#real^3`]
THEN MRESA_TAC lem[`(p n_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`y:real^3#real^3#real^3#real^3`]
THEN MRESA_TAC lem[`(p f1_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`y:real^3#real^3#real^3#real^3`]));;
let into_domain_efn_fan=
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool). FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) ==> (!y. y IN d1_fan (x,V,E)==> (p e_fan ) y = e_fan x V E y) /\ (!y. y IN d1_fan (x,V,E)==> (p n_fan ) y = n_fan x V E y) /\(!y. y IN d1_fan (x,V,E)==> (p f1_fan ) y = f1_fan x V E y) `,
REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[res;]);;
let power_map_fix_set = 
prove(`!n f:A->A g:A->A s:A->bool. (!x:A. x IN s ==> f x= g x) /\ (!x:A. x IN s ==> g x IN s) ==> (!x. x IN s==>(f POWER n) x = (g POWER n) x)`,
INDUCT_TAC THENL[REWRITE_TAC[MULT; POWER; I_THM]; REWRITE_TAC[POWER; o_DEF] THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU") THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"EM") THEN DISCH_THEN(LABEL_TAC"NHO") THEN DISCH_TAC THEN REMOVE_THEN "YEU" (fun th -> MRESA_TAC th[`f:A->A`;`g:A->A`;`s:A->bool`]) THEN POP_ASSUM (fun th-> MRESA1_TAC th `g (x:A):A`) THEN POP_ASSUM MP_TAC THEN REMOVE_THEN "EM" (fun th -> MRESA1_TAC th `x:A`) THEN REMOVE_THEN "NHO" (fun th -> MRESA1_TAC th `x:A`)]);;
let into_domain_power_efn_fan=
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) n:num p. FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E))) ==> (!y. y IN d1_fan (x,V,E)==> ((p e_fan ) POWER n)y = ((e_fan x V E) POWER n) y) /\ (!y. y IN d1_fan (x,V,E)==> ((p n_fan ) POWER n) y = ((n_fan x V E) POWER n) y) /\(!y. y IN d1_fan (x,V,E)==> ((p f1_fan ) POWER n) y = ((f1_fan x V E) POWER n) y)`,
REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN MRESA_TAC into_domain_efn_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN MRESA_TAC into_domain1_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN MRESA_TAC into_domain1_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN MRESA_TAC into_domain1_e_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN MRESA_TAC power_map_fix_set[`n:num`; `(p e_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`; `(e_fan x V E):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`d1_fan (x:real^3,V,E)`;] THEN MRESA_TAC power_map_fix_set[`n:num`; `(p n_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`; `(n_fan x V E):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`d1_fan (x:real^3,V,E)`;] THEN MRESA_TAC power_map_fix_set[`n:num`; `(p f1_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`; `(f1_fan x V E):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`;`d1_fan (x:real^3,V,E)`;]);;
let power_fun_in_domain=
prove(`!n f:A->A s:A->bool.(!y. y IN s==> f y IN s)==> (!y. y IN s==> (f POWER n) y IN s)`,
INDUCT_TAC THENL[REWRITE_TAC[POWER_0; I_THM]; POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"YEU") THEN REPEAT STRIP_TAC THEN REMOVE_THEN "YEU" (fun th-> MRESA_TAC th[`f:A->A`;`s:A->bool`]) THEN REWRITE_TAC[COM_POWER;o_DEF] THEN POP_ASSUM (fun th-> MRESA1_TAC th`y:A`)]);;
let into_domain1_power_efn_fan= 
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) n:num. FAN(x,V,E) ==> (!y. y IN d1_fan (x,V,E)==> (((e_fan x V E) POWER n) y IN d1_fan (x,V,E))) /\ (!y. y IN d1_fan (x,V,E)==> (((n_fan x V E) POWER n) y IN d1_fan (x,V,E))) /\(!y. y IN d1_fan (x,V,E)==> (((f1_fan x V E) POWER n) y IN d1_fan (x,V,E)))`,
REPEAT GEN_TAC THEN DISCH_TAC THEN MRESA_TAC into_domain1_e_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;] THEN MRESA_TAC into_domain1_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;] THEN MRESA_TAC into_domain1_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;] THEN MRESA_TAC power_fun_in_domain[`n:num`;`e_fan x V (E:(real^3->bool)->bool)`;`d1_fan (x:real^3,V,E)`;] THEN MRESA_TAC power_fun_in_domain[`n:num`;`f1_fan x V (E:(real^3->bool)->bool)`;`d1_fan (x:real^3,V,E)`;] THEN MRESA_TAC power_fun_in_domain[`n:num`;`n_fan x V (E:(real^3->bool)->bool)`;`d1_fan (x:real^3,V,E)`;]);;
let lemma_hypermap1_of_fanx=
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool). FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) ==> (p e_fan) o (p n_fan) o (p f1_fan)= I`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_EXT THEN ASM_REWRITE_TAC[I_THM;o_DEF] THEN GEN_TAC THEN DISJ_CASES_TAC(SET_RULE`~(x' IN d1_fan (x,V,E) )\/ (x' IN d1_fan (x:real^3,V,E))`) THENL[ MRESA_TAC id_enf_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`x':real^3#real^3#real^3#real^3`]; MRESA_TAC into_domain_efn_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN POP_ASSUM (fun th-> MRESA1_TAC th `x':real^3#real^3#real^3#real^3` ) THEN REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th-> MRESA1_TAC th `f1_fan x V E x':real^3#real^3#real^3#real^3` ) THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN (LABEL_TAC"YEU") THEN MRESA_TAC into_domain1_f1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN POP_ASSUM (fun th-> MRESA1_TAC th `x':real^3#real^3#real^3#real^3` ) THEN RESA_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_THEN "YEU" (fun th-> MRESA1_TAC th `(n_fan x V E (f1_fan x V E x')):real^3#real^3#real^3#real^3` ) THEN POP_ASSUM MP_TAC THEN MRESA_TAC into_domain1_n_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN POP_ASSUM (fun th-> MRESA1_TAC th `f1_fan x V E x':real^3#real^3#real^3#real^3` ) THEN RESA_TAC THEN MRESA_TAC condition_hypermap_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`] THEN POP_ASSUM (fun th-> MRESA1_TAC th `x':real^3#real^3#real^3#real^3` )]);;
let hypermap_of_fan_rep=
prove(`!x:real^3 V:real^3->bool (E:(real^3->bool)->bool) p. FAN(x,V,E) /\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) ==> dart ( hypermap1_of_fanx (x,V,E)) =d_fan (x,V,E) /\ edge_map (hypermap1_of_fanx (x,V,E)) = p e_fan /\ node_map (hypermap1_of_fanx (x,V,E)) = p n_fan /\ face_map (hypermap1_of_fanx (x,V,E)) = p f1_fan `,
REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[hypermap1_of_fanx] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN ASM_REWRITE_TAC[] THEN MRESA_TAC finite_d_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`] THEN MRESA_TAC e_fan_permutes[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`] THEN MRESA_TAC n_fan_permutes[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`] THEN MRESA_TAC f1_fan_permutes[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`] THEN MRESA_TAC lemma_hypermap1_of_fanx[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`] THEN MRESA_TAC lemma_hypermap_rep[`d_fan (x:real^3,V,E):real^3#real^3#real^3#real^3->bool`; `(p e_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`; `(p n_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`; `(p f1_fan):real^3#real^3#real^3#real^3->real^3#real^3#real^3#real^3`]);;
let properties_of_f1_fan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) y y1. FAN(x,V,E) /\ y = f1_fan x V E y1 /\ y1 IN d1_fan (x,V,E) ==> pr3 y1 =pr2 y /\ {pr2 y1, pr3 y1} IN E /\ {pr2 y, pr3 y} IN E /\ pr2 y1= sigma_fan x V E (pr2 y) (pr3 y)`,
REPEAT GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[d1_fan; IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[pr2;pr3;f1_fan] THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`w:real^3`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`) THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN RESA_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`) THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_REWRITE_TAC[]);;
let face_subset_dart_fan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds. FAN(x,V,E) /\ ds IN face_set(hypermap1_of_fanx (x,V,E)) ==> ds SUBSET d_fan (x,V,E)`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MRESA_TAC lemma_face_representation[`hypermap1_of_fanx(x:real^3,V,E)`;`ds:real^3#real^3#real^3#real^3->bool`] THEN MRESA_TAC hypermap_of_fan_rep[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`(\t. res (t x V E) (d1_fan (x,V,E)))`] THEN MRESA_TAC lemma_face_subset[`hypermap1_of_fanx(x:real^3,V,E)`;`x':real^3#real^3#real^3#real^3`]);;
let properties_of_elements_in_face_fan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds y. FAN(x,V,E) /\ ds IN face_set(hypermap1_of_fanx (x,V,E)) /\ y IN ds ==> {pr2 y, pr3 y} IN E\/ pr2 y= pr3 y`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MRESA_TAC face_subset_dart_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`ds:real^3#real^3#real^3#real^3->bool`] THEN MP_TAC(SET_RULE`y IN ds /\ ds SUBSET d_fan (x,V,E)==> y IN d_fan (x,V,E)`) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[d_fan;d1_fan;d20_fan;UNION;IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[pr2;pr3]);;
let fully_surrounded_is_non_isolated_fan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FAN(x,V,E) /\ (!v. v IN V==>CARD (set_of_edge v V E) >1) ==> d20_fan(x,V,E)={}`,
REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU") THEN REWRITE_TAC[SET_RULE`A={}<=> ~(?y. y IN A)`] THEN REWRITE_TAC[d20_fan;IN_ELIM_THM] THEN STRIP_TAC THEN REMOVE_THEN "YEU"(fun th-> MRESAL1_TAC th`v:real^3`[IN;CARD_CLAUSES]) THEN POP_ASSUM MP_TAC THEN ARITH_TAC);;
let dartset_fully_surrounded_is_non_isolated_fan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool). FAN(x,V,E) /\ (!v. v IN V==>CARD (set_of_edge v V E) >1) ==> d_fan(x,V,E)=d1_fan(x,V,E)`,
REPEAT STRIP_TAC THEN MRESA_TAC fully_surrounded_is_non_isolated_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`] THEN ASM_REWRITE_TAC[d_fan;] THEN SET_TAC[]);;
let properties_of_elements_in_face_fully_surroundedfan=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds y. FAN(x,V,E) /\ (!v. v IN V==>CARD (set_of_edge v V E) >1) /\ ds IN face_set(hypermap1_of_fanx (x,V,E)) /\ y IN ds ==> {pr2 y, pr3 y} IN E`,
REPEAT GEN_TAC THEN STRIP_TAC THEN MRESA_TAC face_subset_dart_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`ds:real^3#real^3#real^3#real^3->bool`] THEN MP_TAC(SET_RULE`y IN ds /\ ds SUBSET d_fan (x,V,E)==> y IN d_fan (x,V,E)`) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC dartset_fully_surrounded_is_non_isolated_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`] THEN REWRITE_TAC[d1_fan;IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[pr2;pr3]);;
let AAUHTVE=
prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) p. FAN(x,V,E)/\ p = ( \ t. res (t x V E ) (d1_fan (x,V,E)) ) ==> FINITE (d_fan (x,V,E)) /\ (p e_fan) permutes (d_fan (x,V,E)) /\ (p n_fan) permutes (d_fan (x,V,E)) /\ (p f1_fan) permutes (d_fan (x,V,E)) /\(p e_fan) o (p n_fan) o (p f1_fan)= I /\ (!a. a IN d1_fan(x,V,E)==> (e_fan x V E) (e_fan x V E a) =a) /\ (!a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a=a )) /\ (!a. a IN d1_fan(x,V,E) ==> ~(f1_fan x V E a=a )) /\ (!k:num l:num a. a IN d1_fan(x,V,E) ==> (((n_fan x V E) POWER k) o (e_fan x V E)) a= ((e_fan x V E)o((n_fan x V E) POWER l)) a==> (n_fan x V E POWER l) a=a) /\ (!n:num a. a IN d1_fan(x,V,E) ==> ~(e_fan x V E a =(n_fan x V E POWER n) a))`,
(********************************) end;;