module Hypermap_of_fan  = struct

open Sphere;;
open Fan_defs;;
open Tactic_fan;;
open Lemma_fan;;		
open Hypermap;;
open Fan;;

(* ========================================================================== *)
(*                   DEFINITION OF HYPERMAP OF 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)}`;;

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 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) )`;;
(* 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) )`;;


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))}`;;






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))`;;




(*
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 {}))`;;
 


(* ========================================================================== *)
(*                   ORBITS NODE FAN                    *)
(* ========================================================================== *)






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`,

MESON_TAC[image_power_map_points;properties_of_set_of_edge_fan]);;
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`,

MESON_TAC[image_power_map_points;properties_of_set_of_edge_fan]);;

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)} `,

MESON_TAC[IN2_ORBITS_FAN;remark1_fan;image_power_map_points;properties_of_set_of_edge_fan]);;






(* ========================================================================== *)
(*                  PERMUTES OF E_FAN N_FAN F1_FAN         (^_^)            *)
(* ========================================================================== *)



(* 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))
`,
MESON_TAC[MONO_N_FAN;SUR_N_FAN;MONO_F1_FAN;SUR_F1_FAN;MONO_E_FAN;SUR_E_FAN]);;






(* ========================================================================== *)
(*                  PROPERTIES OF E_FAN N_FAN F1_FAN         (^_^)            *)
(* ========================================================================== *)


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[]);;



(* ========================================================================== *)
(*             REPRESENTATION OF HYPERMAP OF 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[]);;


(* ========================================================================== *)
(*                 PROPERTIES OF HYPERMAP OF FAN          (^_^)            *)
(* ========================================================================== *)



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 AAUHTVE=
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)) ) ==> 
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))`,


MESON_TAC[lemma_hypermap1_of_fanx;e_fan_permutes;n_fan_permutes;finite_d_fan;f1_fan_permutes;plain_hypermap_fan;e_fan_no_fix_point;f_fan_no_fix_point;distinct_nodes;edge_lie_different_nodes]);;
(********************************)




end;;