legacy/oldfan/RWXUYZZ.hl

   1
   2 (* ========================================================================== *)
   3 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   4 (*                                                                            *)
   5 (* Chapter: Fan                                              *)
   6 (* Author: Hoang Le Truong                                        *)
   7 (* Date: 2010-02-09                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11
  12
  13 module  Dartset_leads_into = struct
  14
  15
  16
  17 open Sphere;;
  18 open Fan_defs;;
  19 open Hypermap_of_fan;;
  20 open Tactic_fan;;
  21 open Lemma_fan;;
  22 open Fan;;
  23 open Hypermap_of_fan;;
  24 open Node_fan;;
  25 open Azim_node;;
  26 open Sum_azim_node;;
  27 open Disjoint_fan;;
  28 open Lead_fan;;
  29 open Fan_misc;;
  30 open Leads_into_fan;;
  31 open Fully_surrounded;;
  32 open Sin_azim_cross_dot;;
  33 open Leads_intos;;
  34 open Hypermap;;
  35
  36
  37 (* ========================================================================== *)
  38 (*   FAN  AND CONVEX              *)
  39 (* ========================================================================== *)
  40
  41
  42 let angle_is_small_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3.
  43 FAN(x,V,E)/\ {v,u} IN E /\ {u,w} IN E
  44 /\ sigma_fan x V E u w = v
  45 /\ fan80(x,V,E)
  46 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
  47 ==>
  48  azim x v u w <= azim x v u (sigma_fan x V E v u) `,
  49
  50
  51 REPEAT STRIP_TAC
  52 THEN POP_ASSUM MP_TAC
  53 THEN POP_ASSUM MP_TAC
  54 THEN DISCH_THEN(LABEL_TAC "BE")
  55 THEN DISCH_THEN(LABEL_TAC"EM")
  56 THEN USE_THEN "BE" MP_TAC
  57 THEN REWRITE_TAC[fan80]
  58 THEN DISCH_TAC
  59 THEN POP_ASSUM (fun th->   MRESA_TAC th [`u:real^3`;`w:real^3`]
  60 THEN MRESA_TAC th [`v:real^3`;`u:real^3`])
  61 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
  62 ` (v:real^3)`]
  63 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
  64 ` (u:real^3)`]
  65 THEN REMOVE_THEN "EM" (fun th-> MRESA1_TAC th `v:real^3` THEN MP_TAC (th) THEN DISCH_THEN(LABEL_TAC"EM"))
  66 THEN DISJ_CASES_TAC(SET_RULE`set_of_edge v V E = {u} \/ ~(set_of_edge v V E = {u:real^3})`)
  67 THENL(*1*)[
  68 MRESA_TAC CARD_SING[`u:real^3`; `(set_of_edge v V E):real^3->bool`]
  69 THEN POP_ASSUM MP_TAC
  70 THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(th)])
  71 THEN ASM_TAC THEN ARITH_TAC;(*1*)
  72 MRESA_TAC SIGMA_FAN[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]
  73 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` sigma_fan x V E v (u:real^3)`;` (v:real^3)`]
  74 THEN POP_ASSUM MP_TAC THEN RESA_TAC
  75 THEN MRESA_TAC properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
  76 THEN MRESA_TAC notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
  77 THEN MRESA_TAC th3[`x:real^3`;`v:real^3`;`w:real^3`]
  78 THEN  ABBREV_TAC`w1=(sigma_fan x V E v u) :real^3`
  79 THEN MRESA_TAC properties_of_fully_surrounded1_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`w1:real^3`]
  80 THEN DISJ_CASES_TAC(REAL_ARITH`  azim x v u w1 < azim x v u w\/ azim x v u w <= azim x v u w1 `)
  81 THENL(*2*)[
  82 MP_TAC(REAL_ARITH`azim x v u w1 < azim x v u w ==> azim x v u w1 <= azim x v u w`)
  83 THEN RESA_TAC
  84 THEN MRESA_TAC sum4_azim_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w1:real^3`;`w:real^3`]
  85 THEN MP_TAC(REAL_ARITH` &0< azim x v u w1 /\ azim x v u w1 < azim x v u w /\ azim x v u w = azim x v u w1 + azim x v w1 w
  86 ==> &0< azim x v w1 w /\ azim x v w1 w <= azim x v u w`)
  87 THEN RESA_TAC
  88 THEN MP_TAC(REAL_ARITH`azim x v w1 w <= azim x v u w /\ azim x v u w < pi
  89 ==> azim x v w1 w < pi`)
  90 THEN RESA_TAC
  91 THEN MRESA_TAC exists_cut_in_edge_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`w1:real^3`]
  92 THEN POP_ASSUM MP_TAC
  93 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[SET_RULE`~(A={})<=> ?x. x IN A`;INTER]
  94 THEN REWRITE_TAC[IN_ELIM_THM]
  95 THEN STRIP_TAC
  96 THEN ABBREV_TAC`va=(&1-a)%u + a%w:real^3`
  97 THEN MRESA_TAC not_collinear_is_properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`;`a:real`]
  98 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`va:real^3`] decomposition_planar_by_angle_fan)
  99 THEN ASM_REWRITE_TAC[]
 100 THEN STRIP_TAC
 101 THENL(*3*)[
 102 MRESA_TAC point_in_aff_ge[`(x:real^3)`;`(v:real^3)`;`(w1:real^3)`]
 103 THEN MRESA_TAC not_cut_in_edges_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`;`a:real`]
 104 THEN MP_TAC(SET_RULE`w1 IN aff_gt {x} {v, va}
 105  /\ w1 IN aff_ge {x} {v, w1}==> ~(aff_gt {x} {v, va} INTER aff_ge {x:real^3} {v, w1}={})`)
 106 THEN RESA_TAC
 107 THEN POP_ASSUM MP_TAC
 108 THEN POP_ASSUM MP_TAC
 109 THEN FIND_ASSUM MP_TAC`{v,w1:real^3} IN E`
 110 THEN SET_TAC[];(*3*)
 111 MRESA_TAC pos_in_aff_ge_fan [`x:real^3`;`u:real^3`;`w:real^3`;`a:real`]
 112 THEN MP_TAC(SET_RULE`va IN aff_ge {x} {v, w1:real^3} /\ va IN aff_ge {x} {u, w}
 113 ==>va IN  aff_ge {x} {u, w} INTER aff_ge {x} {v, w1:real^3} `)
 114 THEN RESA_TAC
 115 THEN POP_ASSUM MP_TAC
 116 THEN FIND_ASSUM MP_TAC `FAN(x:real^3,V,E)`
 117 THEN REWRITE_TAC[FAN;fan7]
 118 THEN STRIP_TAC
 119 THEN POP_ASSUM  (fun th-> MP_TAC(ISPECL[`{(u:real^3),(w:real^3)}`;`{(v:real^3),(w1:real^3)}`]th))
 120   THEN ASM_REWRITE_TAC[UNION;IN_ELIM_THM;]
 121 THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
 122 THEN MP_TAC(SET_RULE`~(v=u) /\ DISJOINT{x,v} {w} ==> ~(v IN {u,w:real^3}) `)
 123 THEN RESA_TAC
 124 THEN MP_TAC(SET_RULE`~(v IN {u,w:real^3})/\ ~(u=w)==> ~({u, w} INTER {v, w1} = {u, w:real^3})`)
 125 THEN RESA_TAC
 126 THEN MP_TAC(SET_RULE`~({u, w} INTER {v, w1} = {u, w:real^3}) ==> {u, w} INTER {v, w1} PSUBSET {u, w} `)
 127 THEN RESA_TAC
 128 THEN MP_TAC(SET_RULE`{u, w} INTER {v, w1} PSUBSET {u, w:real^3} ==> {u, w} INTER {v, w1} SUBSET {u}\/  {u, w} INTER {v, w1} SUBSET {w} `)
 129 THEN ASM_REWRITE_TAC[]
 130 THEN STRIP_TAC
 131 THENL(*4*)[
 132 MRESAL_TAC AFF_GE_MONO_RIGHT [`{x:real^3}`;`{u, w} INTER {v, w1:real^3}`; `{u:real^3}`][DISJOINT;SET_RULE`{x} INTER {u} = {}<=> ~(x=u:real^3)`]
 133 THEN STRIP_TAC
 134 THEN MRESAL_TAC AFF_GE_SUBSET_AFFINE_HULL[`{x:real^3}`;`{u:real^3}`][SET_RULE`{x} UNION {u}={x,u}`;GSYM aff]
 135 THEN MP_TAC(SET_RULE`aff_ge {x:real^3} ({u, w} INTER {v, w1}) SUBSET aff_ge {x} {u}/\ aff_ge {x} {u} SUBSET aff {x, u}/\ va IN aff_ge {x} ({u, w} INTER {v, w1})==> va IN aff {x,u}`)
 136 THEN RESA_TAC
 137 THEN POP_ASSUM MP_TAC
 138 THEN REWRITE_TAC[aff;AFFINE_HULL_2;IN_ELIM_THM]
 139 THEN STRIP_TAC
 140 THEN POP_ASSUM MP_TAC
 141 THEN EXPAND_TAC"va"
 142 THEN REWRITE_TAC[VECTOR_ARITH`(&1 - a) % u + a % w = u' % x + v'' % u
 143 <=> a % w = u' % x + (v''+a- &1) % u`]
 144 THEN MP_TAC(REAL_ARITH`&0< a==> ~(a = &0)`) THEN RESA_TAC
 145 THEN MRESA1_TAC REAL_MUL_LINV`a:real`
 146 THEN STRIP_TAC
 147 THEN MP_TAC(SET_RULE`a % w = u' % x + (v' + a - &1) % u:real^3 ==> (inv (a))%(a % w ) = (inv (a))%( u' % x + (v' + a - &1) % u)`)
 148 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
 149 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`; VECTOR_ARITH`A%(B+C)=A%B+A%C`]
 150 THEN REDUCE_VECTOR_TAC
 151 THEN STRIP_TAC
 152 THEN SUBGOAL_THEN `w IN aff {x,u:real^3}` ASSUME_TAC
 153 THENL(*5*)[
 154 REWRITE_TAC[aff;AFFINE_HULL_2;IN_ELIM_THM]
 155 THEN EXISTS_TAC`(inv a * u'):real`
 156 THEN EXISTS_TAC`(inv a * (v' + a - &1)):real`
 157 THEN ASM_REWRITE_TAC[REAL_ARITH`inv a * u' + inv a * (v' + a - &1) =inv a * ( a+ (u' + v') - &1)`;REAL_ARITH`A+ &1- &1=A`];(*5*)
 158 POP_ASSUM MP_TAC
 159 THEN FIND_ASSUM MP_TAC `~(w IN aff {x, u:real^3})`
 160 THEN SET_TAC[]](*5*);(*4*)
 161
 162 FIND_ASSUM MP_TAC`{u,w:real^3} IN E`
 163 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 164 THEN STRIP_TAC
 165 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u:real^3`;`w:real^3`]
 166 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 167 THEN MRESAL_TAC AFF_GE_MONO_RIGHT [`{x:real^3}`;`{u, w} INTER {v, w1:real^3}`; `{w:real^3}`][DISJOINT;SET_RULE`{x} INTER {w} = {}<=> ~(x=w:real^3)`]
 168 THEN STRIP_TAC
 169 THEN MRESAL_TAC AFF_GE_SUBSET_AFFINE_HULL[`{x:real^3}`;`{w:real^3}`][SET_RULE`{x} UNION {w}={x,w}`;GSYM aff]
 170 THEN MP_TAC(SET_RULE`aff_ge {x:real^3} ({u, w} INTER {v, w1}) SUBSET aff_ge {x} {w}/\ aff_ge {x} {w} SUBSET aff {x, w}/\ va IN aff_ge {x} ({u, w} INTER {v, w1})==> va IN aff {x,w}`)
 171 THEN RESA_TAC
 172 THEN POP_ASSUM MP_TAC
 173 THEN REWRITE_TAC[aff;AFFINE_HULL_2;IN_ELIM_THM]
 174 THEN STRIP_TAC
 175 THEN POP_ASSUM MP_TAC
 176 THEN EXPAND_TAC"va"
 177 THEN REWRITE_TAC[VECTOR_ARITH`(&1 - a) % u + a % w = u' % x + v'' % w
 178 <=> (&1-a) % u = u' % x + (v''-a) % w`]
 179 THEN MP_TAC(REAL_ARITH`a < &1==> ~(&1- a= &0)`) THEN RESA_TAC
 180 THEN MRESA1_TAC REAL_MUL_LINV`&1-a:real`
 181 THEN STRIP_TAC
 182 THEN MP_TAC(SET_RULE`(&1-a) % u = u' % x + (v' - a) % w:real^3 ==> (inv (&1-a))%((&1-a) % u ) = (inv (&1-a))%( u' % x + (v' - a) % w)`)
 183 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
 184 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`; VECTOR_ARITH`A%(B+C)=A%B+A%C`]
 185 THEN REDUCE_VECTOR_TAC
 186 THEN STRIP_TAC
 187 THEN SUBGOAL_THEN `u IN aff {x,w:real^3}` ASSUME_TAC
 188 THENL(*5*)[
 189 REWRITE_TAC[aff;AFFINE_HULL_2;IN_ELIM_THM]
 190 THEN EXISTS_TAC`(inv (&1-a) * u'):real`
 191 THEN EXISTS_TAC`(inv (&1-a) * (v' - a)):real`
 192 THEN ASM_REWRITE_TAC[REAL_ARITH`inv (&1-a') * u' + inv (&1-a') * (v' - a') =inv (&1-a') * ( (u' + v') - a')`;];(*5*)
 193
 194 POP_ASSUM MP_TAC
 195 THEN FIND_ASSUM MP_TAC `~(u IN aff {x, w:real^3})`
 196 THEN SET_TAC[]](*5*)](*4*)](*3*);(*2*)
 197
 198 ASM_REWRITE_TAC[]]]);;
 199
 200
 201
 202 let angle_is_smallpi_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3.
 203 FAN(x,V,E)/\ {v,u} IN E /\ {u,w} IN E
 204 /\ sigma_fan x V E u w = v
 205 /\ fan80(x,V,E)
 206 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 207 ==>
 208 &0< azim x v u w /\ azim x v u w <pi`,
 209 REPEAT STRIP_TAC
 210 THENL[
 211 POP_ASSUM MP_TAC
 212 THEN POP_ASSUM MP_TAC
 213 THEN DISCH_THEN(LABEL_TAC "BE")
 214 THEN DISCH_THEN(LABEL_TAC"EM")
 215 THEN USE_THEN "BE" MP_TAC
 216 THEN REWRITE_TAC[fan80]
 217 THEN DISCH_TAC
 218 THEN POP_ASSUM (fun th->   MRESA_TAC th [`u:real^3`;`w:real^3`]
 219 THEN MRESA_TAC th [`v:real^3`;`u:real^3`])
 220 THEN MRESA_TAC properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
 221 THEN MRESA_TAC notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 222 THEN SUBGOAL_THEN`~(azim x v u (w:real^3)= &0)`ASSUME_TAC
 223 THENL[STRIP_TAC
 224 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`];
 225 MATCH_MP_TAC(REAL_ARITH`~(azim x v u (w:real^3)= &0)/\ &0<= azim x v u w ==> &0 < azim x v u w`)
 226 THEN ASM_REWRITE_TAC[azim]];
 227
 228 POP_ASSUM MP_TAC
 229 THEN POP_ASSUM MP_TAC
 230 THEN DISCH_THEN(LABEL_TAC "BE")
 231 THEN DISCH_THEN(LABEL_TAC"EM")
 232 THEN USE_THEN "BE" MP_TAC
 233 THEN REWRITE_TAC[fan80]
 234 THEN DISCH_TAC
 235 THEN POP_ASSUM (fun th->   MRESA_TAC th [`u:real^3`;`w:real^3`]
 236 THEN MRESA_TAC th [`v:real^3`;`u:real^3`])
 237 THEN MRESA_TAC angle_is_small_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` u:real^3`;`w:real^3`]
 238 THEN ASM_TAC THEN REAL_ARITH_TAC]);;
 239
 240
 241
 242
 243 let exists_rw_dart_inter_aff_gt_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3 .
 244 FAN(x,V,E)/\ {v,u} IN E /\ {u,w} IN E
 245 /\ sigma_fan x V E u w = v
 246 /\ fan80(x,V,E)
 247 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 248 ==>
 249 (?h:real. &0< h /\
 250 (!t:real. &0< t /\ t< h==>
 251 (!s:real. &0<s /\ s< pi/ &2
 252 ==>
 253 ~(rw_dart_fan x V E ((x:real^3),(v:real^3),(u:real^3),(sigma_fan x V E v (u:real^3))) (cos(s)) INTER aff_gt {x} {v, (&1-t)%u+t%w}={})
 254 )))`,
 255
 256
 257 REPEAT STRIP_TAC
 258 THEN POP_ASSUM MP_TAC
 259 THEN POP_ASSUM MP_TAC
 260 THEN DISCH_THEN(LABEL_TAC "BE")
 261 THEN DISCH_THEN(LABEL_TAC"EM")
 262 THEN USE_THEN "BE" MP_TAC
 263 THEN REWRITE_TAC[fan80]
 264 THEN DISCH_TAC
 265 THEN POP_ASSUM (fun th->   MRESA_TAC th [`u:real^3`;`w:real^3`]
 266 THEN MRESA_TAC th [`v:real^3`;`u:real^3`])
 267 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
 268 ` (v:real^3)`]
 269 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
 270 ` (u:real^3)`]
 271 THEN REMOVE_THEN "EM" (fun th-> MRESA1_TAC th `v:real^3` THEN MP_TAC (th) THEN DISCH_THEN(LABEL_TAC"EM"))
 272 THEN DISJ_CASES_TAC(SET_RULE`set_of_edge v V E = {u} \/ ~(set_of_edge v V E = {u:real^3})`)
 273 THENL(*1*)[
 274 MRESA_TAC CARD_SING[`u:real^3`; `(set_of_edge v V E):real^3->bool`]
 275 THEN POP_ASSUM MP_TAC
 276 THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(th)])
 277 THEN ASM_TAC THEN ARITH_TAC;(*1*)
 278
 279 MRESA_TAC SIGMA_FAN[`(x:real^3)`;` (V:real^3->bool)`;` (E:(real^3->bool)->bool)`;` (v:real^3)`;` (u:real^3)`]
 280 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` sigma_fan x V E v (u:real^3)`;` (v:real^3)`]
 281 THEN POP_ASSUM MP_TAC THEN RESA_TAC
 282 THEN MRESA_TAC properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
 283 THEN MRESA_TAC notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 284 THEN MRESA_TAC th3[`x:real^3`;`v:real^3`;`w:real^3`]
 285 THEN  ABBREV_TAC`w1=(sigma_fan x V E v u) :real^3`
 286 THEN MRESA_TAC properties_of_fully_surrounded1_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`w1:real^3`]
 287 THEN DISJ_CASES_TAC(REAL_ARITH`  azim x v u w1 < azim x v u w\/ azim x v u w <= azim x v u w1 `)
 288 THENL(*2*)[
 289 MP_TAC(REAL_ARITH`azim x v u w1 < azim x v u w ==> azim x v u w1 <= azim x v u w`)
 290 THEN RESA_TAC
 291 THEN MRESA_TAC sum4_azim_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w1:real^3`;`w:real^3`]
 292 THEN MP_TAC(REAL_ARITH` &0< azim x v u w1 /\ azim x v u w1 < azim x v u w /\ azim x v u w = azim x v u w1 + azim x v w1 w
 293 ==> &0< azim x v w1 w /\ azim x v w1 w <= azim x v u w`)
 294 THEN RESA_TAC
 295 THEN MP_TAC(REAL_ARITH`azim x v w1 w <= azim x v u w /\ azim x v u w < pi
 296 ==> azim x v w1 w < pi`)
 297 THEN RESA_TAC
 298 THEN MRESA_TAC exists_cut_in_edge_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`w1:real^3`]
 299 THEN POP_ASSUM MP_TAC
 300 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[SET_RULE`~(A={})<=> ?x. x IN A`;INTER]
 301 THEN REWRITE_TAC[IN_ELIM_THM]
 302 THEN STRIP_TAC
 303 THEN ABBREV_TAC`va=(&1-a)%u + a%w:real^3`
 304 THEN MRESA_TAC not_collinear_is_properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`;`a:real`]
 305 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`w1:real^3`;`va:real^3`] decomposition_planar_by_angle_fan)
 306 THEN ASM_REWRITE_TAC[]
 307 THEN STRIP_TAC
 308 THENL(*3*)[
 309 MRESA_TAC point_in_aff_ge[`(x:real^3)`;`(v:real^3)`;`(w1:real^3)`]
 310 THEN MRESA_TAC not_cut_in_edges_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`;`a:real`]
 311 THEN MP_TAC(SET_RULE`w1 IN aff_gt {x} {v, va}
 312  /\ w1 IN aff_ge {x} {v, w1}==> ~(aff_gt {x} {v, va} INTER aff_ge {x:real^3} {v, w1}={})`)
 313 THEN RESA_TAC
 314 THEN POP_ASSUM MP_TAC
 315 THEN POP_ASSUM MP_TAC
 316 THEN FIND_ASSUM MP_TAC`{v,w1:real^3} IN E`
 317 THEN SET_TAC[];(*3*)
 318
 319 MRESA_TAC pos_in_aff_ge_fan [`x:real^3`;`u:real^3`;`w:real^3`;`a:real`]
 320 THEN MP_TAC(SET_RULE`va IN aff_ge {x} {v, w1:real^3} /\ va IN aff_ge {x} {u, w}
 321 ==>va IN  aff_ge {x} {u, w} INTER aff_ge {x} {v, w1:real^3} `)
 322 THEN RESA_TAC
 323 THEN POP_ASSUM MP_TAC
 324 THEN FIND_ASSUM MP_TAC `FAN(x:real^3,V,E)`
 325 THEN REWRITE_TAC[FAN;fan7]
 326 THEN STRIP_TAC
 327 THEN POP_ASSUM  (fun th-> MP_TAC(ISPECL[`{(u:real^3),(w:real^3)}`;`{(v:real^3),(w1:real^3)}`]th))
 328   THEN ASM_REWRITE_TAC[UNION;IN_ELIM_THM;]
 329 THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
 330 THEN MP_TAC(SET_RULE`~(v=u) /\ DISJOINT{x,v} {w} ==> ~(v IN {u,w:real^3}) `)
 331 THEN RESA_TAC
 332 THEN MP_TAC(SET_RULE`~(v IN {u,w:real^3})/\ ~(u=w)==> ~({u, w} INTER {v, w1} = {u, w:real^3})`)
 333 THEN RESA_TAC
 334 THEN MP_TAC(SET_RULE`~({u, w} INTER {v, w1} = {u, w:real^3}) ==> {u, w} INTER {v, w1} PSUBSET {u, w} `)
 335 THEN RESA_TAC
 336 THEN MP_TAC(SET_RULE`{u, w} INTER {v, w1} PSUBSET {u, w:real^3} ==> {u, w} INTER {v, w1} SUBSET {u}\/  {u, w} INTER {v, w1} SUBSET {w} `)
 337 THEN ASM_REWRITE_TAC[]
 338 THEN STRIP_TAC
 339 THENL(*4*)[
 340 MRESAL_TAC AFF_GE_MONO_RIGHT [`{x:real^3}`;`{u, w} INTER {v, w1:real^3}`; `{u:real^3}`][DISJOINT;SET_RULE`{x} INTER {u} = {}<=> ~(x=u:real^3)`]
 341 THEN STRIP_TAC
 342 THEN MRESAL_TAC AFF_GE_SUBSET_AFFINE_HULL[`{x:real^3}`;`{u:real^3}`][SET_RULE`{x} UNION {u}={x,u}`;GSYM aff]
 343 THEN MP_TAC(SET_RULE`aff_ge {x:real^3} ({u, w} INTER {v, w1}) SUBSET aff_ge {x} {u}/\ aff_ge {x} {u} SUBSET aff {x, u}/\ va IN aff_ge {x} ({u, w} INTER {v, w1})==> va IN aff {x,u}`)
 344 THEN RESA_TAC
 345 THEN POP_ASSUM MP_TAC
 346 THEN REWRITE_TAC[aff;AFFINE_HULL_2;IN_ELIM_THM]
 347 THEN STRIP_TAC
 348 THEN POP_ASSUM MP_TAC
 349 THEN EXPAND_TAC"va"
 350 THEN REWRITE_TAC[VECTOR_ARITH`(&1 - a) % u + a % w = u' % x + v'' % u
 351 <=> a % w = u' % x + (v''+a- &1) % u`]
 352 THEN MP_TAC(REAL_ARITH`&0< a==> ~(a = &0)`) THEN RESA_TAC
 353 THEN MRESA1_TAC REAL_MUL_LINV`a:real`
 354 THEN STRIP_TAC
 355 THEN MP_TAC(SET_RULE`a % w = u' % x + (v' + a - &1) % u:real^3 ==> (inv (a))%(a % w ) = (inv (a))%( u' % x + (v' + a - &1) % u)`)
 356 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
 357 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`; VECTOR_ARITH`A%(B+C)=A%B+A%C`]
 358 THEN REDUCE_VECTOR_TAC
 359 THEN STRIP_TAC
 360 THEN SUBGOAL_THEN `w IN aff {x,u:real^3}` ASSUME_TAC
 361 THENL(*5*)[
 362 REWRITE_TAC[aff;AFFINE_HULL_2;IN_ELIM_THM]
 363 THEN EXISTS_TAC`(inv a * u'):real`
 364 THEN EXISTS_TAC`(inv a * (v' + a - &1)):real`
 365 THEN ASM_REWRITE_TAC[REAL_ARITH`inv a * u' + inv a * (v' + a - &1) =inv a * ( a+ (u' + v') - &1)`;REAL_ARITH`A+ &1- &1=A`];(*5*)
 366 POP_ASSUM MP_TAC
 367 THEN FIND_ASSUM MP_TAC `~(w IN aff {x, u:real^3})`
 368 THEN SET_TAC[]](*5*);(*4*)
 369
 370 FIND_ASSUM MP_TAC`{u,w:real^3} IN E`
 371 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 372 THEN STRIP_TAC
 373 THEN MRESA_TAC remark1_fan[`x:real^3 `;`(V:real^3->bool) `;`(E:(real^3->bool)->bool)`;` u:real^3`;`w:real^3`]
 374 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 375 THEN MRESAL_TAC AFF_GE_MONO_RIGHT [`{x:real^3}`;`{u, w} INTER {v, w1:real^3}`; `{w:real^3}`][DISJOINT;SET_RULE`{x} INTER {w} = {}<=> ~(x=w:real^3)`]
 376 THEN STRIP_TAC
 377 THEN MRESAL_TAC AFF_GE_SUBSET_AFFINE_HULL[`{x:real^3}`;`{w:real^3}`][SET_RULE`{x} UNION {w}={x,w}`;GSYM aff]
 378 THEN MP_TAC(SET_RULE`aff_ge {x:real^3} ({u, w} INTER {v, w1}) SUBSET aff_ge {x} {w}/\ aff_ge {x} {w} SUBSET aff {x, w}/\ va IN aff_ge {x} ({u, w} INTER {v, w1})==> va IN aff {x,w}`)
 379 THEN RESA_TAC
 380 THEN POP_ASSUM MP_TAC
 381 THEN REWRITE_TAC[aff;AFFINE_HULL_2;IN_ELIM_THM]
 382 THEN STRIP_TAC
 383 THEN POP_ASSUM MP_TAC
 384 THEN EXPAND_TAC"va"
 385 THEN REWRITE_TAC[VECTOR_ARITH`(&1 - a) % u + a % w = u' % x + v'' % w
 386 <=> (&1-a) % u = u' % x + (v''-a) % w`]
 387 THEN MP_TAC(REAL_ARITH`a < &1==> ~(&1- a= &0)`) THEN RESA_TAC
 388 THEN MRESA1_TAC REAL_MUL_LINV`&1-a:real`
 389 THEN STRIP_TAC
 390 THEN MP_TAC(SET_RULE`(&1-a) % u = u' % x + (v' - a) % w:real^3 ==> (inv (&1-a))%((&1-a) % u ) = (inv (&1-a))%( u' % x + (v' - a) % w)`)
 391 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
 392 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A%B%C=(A*B)%C`; VECTOR_ARITH`A%(B+C)=A%B+A%C`]
 393 THEN REDUCE_VECTOR_TAC
 394 THEN STRIP_TAC
 395 THEN SUBGOAL_THEN `u IN aff {x,w:real^3}` ASSUME_TAC
 396 THENL(*5*)[REWRITE_TAC[aff;AFFINE_HULL_2;IN_ELIM_THM]
 397 THEN EXISTS_TAC`(inv (&1-a) * u'):real`
 398 THEN EXISTS_TAC`(inv (&1-a) * (v' - a)):real`
 399 THEN ASM_REWRITE_TAC[REAL_ARITH`inv (&1-a') * u' + inv (&1-a') * (v' - a') =inv (&1-a') * ( (u' + v') - a')`;];(*5*)
 400
 401 POP_ASSUM MP_TAC
 402 THEN FIND_ASSUM MP_TAC `~(u IN aff {x, w:real^3})`
 403 THEN SET_TAC[]](*5*)](*4*)](*3*);(*2*)
 404
 405 EXISTS_TAC`&1`
 406 THEN REWRITE_TAC[REAL_ARITH`&0< &1`]
 407 THEN REPEAT STRIP_TAC
 408 THEN POP_ASSUM MP_TAC
 409 THEN ABBREV_TAC`va=(&1-t)%u + t%w:real^3`
 410 THEN MRESA_TAC not_collinear_is_properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`;`t:real`]
 411 THEN MRESA_TAC inequality4_aim_in_convex_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`t:real`]
 412 THEN ASM_REWRITE_TAC[rw_dart_fan;w_dart_fan]
 413 THEN SUBGOAL_THEN`aff_gt {x} {v,va:real^3} SUBSET wedge x v u w1` ASSUME_TAC
 414 THENL(*3*)[
 415 REWRITE_TAC[SUBSET; IN_ELIM_THM; wedge]
 416 THEN GEN_TAC
 417 THEN MRESAL_TAC aff_gt_inter_aff_gt [`(x:real^3)`;`(v:real^3)`;`(va:real^3)`][INTER;IN_ELIM_THM]
 418 THEN STRIP_TAC
 419 THEN MRESAL_TAC properties_of_collinear4_points_fan[`x:real^3`;`v:real^3`;`va:real^3`;`x':real^3`][IN_ELIM_THM]
 420 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 421 THEN ASM_REWRITE_TAC[]
 422 THEN MRESA_TAC AZIM_EQ_ALT[`x:real^3`;`v:real^3`;`u:real^3`; `x':real^3`;`va:real^3`]
 423 THEN POP_ASSUM MP_TAC
 424 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 425 THEN RESA_TAC
 426 THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
 427 THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC
 428 THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
 429 THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC
 430 THEN REAL_ARITH_TAC;(*3*)
 431
 432 MP_TAC(SET_RULE`aff_gt {x} {v, va:real^3} SUBSET wedge x v u w1 ==> (wedge x v u w1 INTER rcone_fan x v (cos s)) INTER aff_gt {x} {v, va}=(rcone_fan x v (cos s)) INTER aff_gt {x} {v, va}`)
 433 THEN RESA_TAC
 434 THEN REWRITE_TAC[rcone_fan;INTER;IN_ELIM_THM]
 435 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`;IN_ELIM_THM]
 436 THEN DISJ_CASES_TAC(REAL_ARITH`(v - x) dot (va - x:real^3) <= &0 \/ &0< (v - x) dot (va - x)`)
 437 THENL(*4*)[
 438 ABBREV_TAC`s1= s/ &2:real`
 439 THEN MP_TAC(REAL_ARITH`&0< s /\ s< pi/ &2/\ s1= s/ &2 /\ &0< pi ==> &0<= s1 /\ s1< s /\  s <= pi/\ &0<s1 /\ s1<pi/ &2`)
 440 THEN REWRITE_TAC[PI_WORKS]
 441 THEN RESA_TAC
 442 THEN EXISTS_TAC`sin (s1) % (e1_fan x v va) + (cos s1) %(e3_fan x v va)+x :real^3 `
 443 THEN REWRITE_TAC[dist;vector_norm;VECTOR_ARITH`(B+C+A)-A=(B+C:real^3)`; DOT_LADD;DOT_RADD;DOT_RMUL;DOT_LMUL;]
 444 THEN MRESAL_TAC properties_coordinate[`x:real^3`;`v:real^3`;`va:real^3`][orthonormal]
 445 THEN ONCE_REWRITE_TAC[DOT_SYM]
 446 THEN ASSUME_TAC(ISPEC`s1:real`SIN_CIRCLE)
 447 THEN ASM_REWRITE_TAC[]
 448 THEN REDUCE_ARITH_TAC
 449 THEN ASM_REWRITE_TAC[REAL_ARITH`sin s * sin s + cos s * cos s =(sin s) pow 2 + (cos s) pow 2`;e3_fan;DOT_RMUL; ]
 450 THEN ONCE_REWRITE_TAC[GSYM vector_norm;]
 451 THEN REWRITE_TAC[DOT_SQUARE_NORM;]
 452 THEN MRESAL1_TAC  SQRT_POW_2`&1`[REAL_ARITH`a pow 2 = a * a`;REAL_ARITH`&0<= &1`;]
 453 THEN POP_ASSUM MP_TAC
 454 THEN MRESAL_TAC SQRT_MUL[`&1`;`&1`][REAL_ARITH`&0<= &1`;]
 455 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th); REAL_ARITH`&1* &1= &1`])
 456 THEN RESA_TAC
 457 THEN REDUCE_ARITH_TAC
 458 THEN SUBGOAL_THEN`~(norm((v:real^3)-(x:real^3))= &0)` ASSUME_TAC
 459 THENL(*5*)[ ASM_REWRITE_TAC[NORM_EQ_0;VECTOR_ARITH`v-x=vec 0<=> x=v`];(*5*)
 460
 461 MP_TAC(ISPEC`norm((v:real^3)-(x:real^3))`REAL_MUL_LINV)
 462 THEN REWRITE_TAC[REAL_ARITH`A*B*D *D=(B*D) *D *A`;REAL_ARITH`A>B<=> B<A`]
 463 THEN RESA_TAC
 464 THEN REDUCE_ARITH_TAC
 465 THEN ASSUME_TAC(ISPEC`v-x:real^3`NORM_POS_LE)
 466 THEN STRIP_TAC
 467 THENL(*6*)[
 468 MATCH_MP_TAC REAL_LT_LMUL
 469 THEN MP_TAC(REAL_ARITH`~(norm (v - x:real^3) = &0)/\ &0 <= norm (v - x)==> &0< norm (v - x) `)
 470 THEN RESA_TAC
 471 THEN MATCH_MP_TAC COS_MONO_LT
 472 THEN ASM_REWRITE_TAC[];(*6*)
 473
 474 MRESA_TAC condition1_to_in_aff_gt_by_angle[`x:real^3`;`v:real^3`;`va:real^3`;`s1:real`]
 475 THEN POP_ASSUM MP_TAC
 476 THEN REWRITE_TAC[e3_fan]](*6*)](*5*);(*4*)
 477 SUBGOAL_THEN`&0<(atn ((norm ((v - x) cross (va - x))) * inv((v - x) dot (va - x))))` ASSUME_TAC
 478 THENL(*5*)[
 479 MP_TAC(ISPEC`(v - x) dot (va - x:real^3)`REAL_LT_INV)
 480 THEN RESA_TAC
 481 THEN ASSUME_TAC(PI_WORKS)
 482 THEN MP_TAC(REAL_ARITH`&0< pi ==> --(pi / &2) < &0`)
 483 THEN RESA_TAC
 484 THEN MRESAL_TAC  ATN_MONO_LT[`&0:real`;` (norm ((v - x) cross (va - x)) * inv ((v - x) dot (va - x))):real`][ ATN_0]
 485 THEN POP_ASSUM MATCH_MP_TAC
 486 THEN MATCH_MP_TAC REAL_LT_MUL
 487 THEN ASM_REWRITE_TAC[]
 488 THEN SUBGOAL_THEN`~(norm((v - x) cross (va - x:real^3))= &0)` ASSUME_TAC
 489 THENL(*6*)[ASM_REWRITE_TAC[NORM_EQ_0]
 490 THEN MP_TAC(ISPECL[`v-x:real^3`;`va-x:real^3`]CROSS_EQ_0)
 491 THEN ONCE_REWRITE_TAC[GSYM COLLINEAR_3;]
 492 THEN RESA_TAC
 493 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,A,C}`]
 494 THEN ASM_REWRITE_TAC[];
 495 POP_ASSUM MP_TAC
 496 THEN MP_TAC(ISPEC`(v - x) cross (va - x:real^3)`NORM_POS_LE)
 497 THEN REAL_ARITH_TAC];(*5*)
 498
 499 ABBREV_TAC`s1= min (s:real) (atn ((norm ((v - x) cross (va - x))) * inv((v - x) dot (va - x)))) / &2`
 500 THEN ASSUME_TAC(ISPEC`(norm ((v - x) cross (u - x)) * inv ((v - x) dot (u - x))):real`ATN_BOUNDS)
 501 THEN MP_TAC(REAL_ARITH`&0< s /\ s< pi/ &2/\ s1= min (s:real) (atn ((norm ((v - x) cross (va - x))) * inv((v - x) dot (va - x)))) / &2
 502  /\ &0< pi /\  &0< (atn ((norm ((v - x) cross (va - x))) * inv((v - x) dot (va - x))))
 503 /\ (atn ((norm ((v - x) cross (va - x))) * inv((v - x) dot (va - x)))) < pi/ &2
 504 ==> &0<= s1 /\ s1< s /\  s <= pi/\ &0<s1 /\ s1<pi/ &2
 505 /\  s1< (atn ((norm ((v - x) cross (va - x))) * inv((v - x) dot (va - x))))
 506 `)
 507 THEN REWRITE_TAC[PI_WORKS]
 508 THEN RESA_TAC
 509 THEN EXISTS_TAC`sin (s1) % (e1_fan x v va) + (cos s1) %(e3_fan x v va)+x :real^3 `
 510 THEN REWRITE_TAC[dist;vector_norm;VECTOR_ARITH`(B+C+A)-A=(B+C:real^3)`; DOT_LADD;DOT_RADD;DOT_RMUL;DOT_LMUL;]
 511 THEN MRESAL_TAC properties_coordinate[`x:real^3`;`v:real^3`;`va:real^3`][orthonormal]
 512 THEN ONCE_REWRITE_TAC[DOT_SYM]
 513 THEN ASSUME_TAC(ISPEC`s1:real`SIN_CIRCLE)
 514 THEN ASM_REWRITE_TAC[]
 515 THEN REDUCE_ARITH_TAC
 516 THEN ASM_REWRITE_TAC[REAL_ARITH`sin s * sin s + cos s * cos s =(sin s) pow 2 + (cos s) pow 2`;e3_fan;DOT_RMUL; ]
 517 THEN ONCE_REWRITE_TAC[GSYM vector_norm;]
 518 THEN REWRITE_TAC[DOT_SQUARE_NORM;]
 519 THEN MRESAL1_TAC  SQRT_POW_2`&1`[REAL_ARITH`a pow 2 = a * a`;REAL_ARITH`&0<= &1`;]
 520 THEN POP_ASSUM MP_TAC
 521 THEN MRESAL_TAC SQRT_MUL[`&1`;`&1`][REAL_ARITH`&0<= &1`;]
 522 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th); REAL_ARITH`&1* &1= &1`])
 523 THEN RESA_TAC
 524 THEN REDUCE_ARITH_TAC
 525 THEN SUBGOAL_THEN`~(norm((v:real^3)-(x:real^3))= &0)` ASSUME_TAC
 526 THENL(*6*)[ASM_REWRITE_TAC[NORM_EQ_0;VECTOR_ARITH`v-x=vec 0<=> x=v`];(*6*)
 527 MP_TAC(ISPEC`norm((v:real^3)-(x:real^3))`REAL_MUL_LINV)
 528 THEN REWRITE_TAC[REAL_ARITH`A*B*D *D=(B*D) *D *A`;REAL_ARITH`A>B<=> B<A`]
 529 THEN RESA_TAC
 530 THEN REDUCE_ARITH_TAC
 531 THEN ASSUME_TAC(ISPEC`v-x:real^3`NORM_POS_LE)
 532 THEN STRIP_TAC
 533 THENL(*7*)[
 534 MATCH_MP_TAC REAL_LT_LMUL
 535 THEN MP_TAC(REAL_ARITH`~(norm (v - x:real^3) = &0)/\ &0 <= norm (v - x)==> &0< norm (v - x) `)
 536 THEN RESA_TAC
 537 THEN MATCH_MP_TAC COS_MONO_LT
 538 THEN ASM_REWRITE_TAC[];
 539 MRESA_TAC condition_to_in_aff_gt_by_angle[`x:real^3`;`v:real^3`;`va:real^3`;`s1:real`]
 540 THEN POP_ASSUM MP_TAC
 541 THEN REWRITE_TAC[e3_fan]]]]]]]]);;
 542
 543
 544
 545
 546
 547
 548
 549 let exists_point_inside_domain_cone_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3 s:real.
 550 FAN(x,V,E)/\ {v,u} IN E /\ {u,w} IN E
 551 /\ sigma_fan x V E u w = v
 552 /\ &0<s /\ s<pi/ &2
 553 /\ fan80(x,V,E)
 554 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 555 ==>
 556 (?y:real^3. y IN rw_dart_fan x V E ((x:real^3),(u:real^3),(w:real^3),(w2:real^3)) (cos(s)) /\
 557 azim x v u y< azim x v u w)`,
 558 REPEAT STRIP_TAC
 559 THEN POP_ASSUM MP_TAC
 560 THEN POP_ASSUM MP_TAC
 561 THEN DISCH_THEN(LABEL_TAC "BE")
 562 THEN DISCH_THEN(LABEL_TAC"EM")
 563 THEN USE_THEN "BE" MP_TAC
 564 THEN REWRITE_TAC[fan80]
 565 THEN DISCH_TAC
 566 THEN POP_ASSUM (fun th->   MRESA_TAC th [`u:real^3`;`w:real^3`]
 567 THEN MRESA_TAC th [`v:real^3`;`u:real^3`])
 568 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
 569 ` (v:real^3)`]
 570 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
 571 ` (u:real^3)`]
 572 THEN REMOVE_THEN "EM" (fun th-> MRESA1_TAC th `u:real^3` THEN MP_TAC (th) THEN DISCH_THEN(LABEL_TAC"EM"))
 573 THEN DISJ_CASES_TAC(SET_RULE`set_of_edge u V E = {w} \/ ~(set_of_edge u V E = {w:real^3})`)
 574 THENL(*1*)[
 575 MRESA_TAC CARD_SING[`w:real^3`; `(set_of_edge u V E):real^3->bool`]
 576 THEN POP_ASSUM MP_TAC
 577 THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(th)])
 578 THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;(*1*)
 579
 580 MRESA_TAC not_empty_rw_dart_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`u:real^3`; `w:real^3`]
 581 THEN POP_ASSUM(fun th-> MRESA1_TAC th `s:real`)
 582 THEN POP_ASSUM MP_TAC
 583 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`;rw_dart_fan;INTER; w_dart_fan;wedge;IN_ELIM_THM;]
 584 THEN STRIP_TAC
 585 THEN MP_TAC(REAL_ARITH`azim x u w y< azim x u w v==> azim x u w y<= azim x u w (v:real^3)`)
 586 THEN RESA_TAC
 587 THEN MRESA_TAC sum4_azim_fan[`x:real^3`;`u:real^3`;`w:real^3`;`y:real^3`;`v:real^3`]
 588 THEN POP_ASSUM MP_TAC
 589 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 590 THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC"YEU EM")
 591 THEN MP_TAC(REAL_ARITH`azim x u w y< azim x u w v/\ &0< azim x u w y/\ azim x u w v < pi /\ azim x u w v = azim x u w y + azim x u y v==>  ~(azim x u y (v:real^3)= &0)/\ &0< azim x u y v/\ azim x u y v < pi/\ ~(azim x u y (v:real^3)= pi)`)
 592 THEN RESA_TAC
 593 THEN POP_ASSUM MP_TAC
 594 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`y:real^3`;`v:real^3`]
 595 THEN POP_ASSUM MP_TAC
 596 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 597 THEN RESA_TAC
 598 THEN POP_ASSUM MP_TAC
 599 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
 600 THEN REPEAT DISCH_TAC
 601 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR[`x:real^3`;`v:real^3`;`y:real^3`;`u:real^3`]
 602 THEN SUBGOAL_THEN`~(azim x v u (y:real^3)= &0)`ASSUME_TAC
 603 THENL(*2*)[
 604 STRIP_TAC
 605 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
 606 THEN POP_ASSUM MP_TAC
 607 THEN REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
 608 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`y:real^3`;`v:real^3`]
 609 THEN POP_ASSUM MATCH_MP_TAC
 610 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 611 THEN ASM_REWRITE_TAC[];(*2*)
 612
 613 SUBGOAL_THEN`~(azim x v u (y:real^3)= pi)`ASSUME_TAC
 614 THENL(*3*)[
 615
 616 STRIP_TAC
 617 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
 618 THEN POP_ASSUM MP_TAC
 619 THEN REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
 620 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`y:real^3`;`v:real^3`]
 621 THEN POP_ASSUM MATCH_MP_TAC
 622 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 623 THEN ASM_REWRITE_TAC[];(*3*)
 624
 625 MP_TAC(REAL_ARITH`~(azim x v u y=pi)==>pi< azim x v u y  \/ azim x v u (y:real^3) < pi`)
 626 THEN RESA_TAC
 627 THENL(*4*)[
 628
 629 MRESA_TAC AZIM_COMPL[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
 630 THEN MRESA_TAC azim[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
 631 THEN MP_TAC(REAL_ARITH`pi< azim x v u y /\ azim x v u y < &2 * pi /\ azim x v y u = &2 * pi - azim x v u y
 632 ==> azim x v y u< pi/\ &0<azim x v y u  `)
 633 THEN RESA_TAC
 634 THEN POP_ASSUM MP_TAC
 635 THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC
 636 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)])
 637 THEN REPEAT STRIP_TAC
 638 THEN MRESA_TAC cross_dot_fully_surrounded_fan[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
 639 THEN MRESA_TAC cross_dot_fully_surrounded_fan[`x:real^3`;`u:real^3`;`v:real^3`;`y:real^3`]
 640 THEN POP_ASSUM MP_TAC
 641 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;CROSS_TRIPLE;]
 642 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
 643 THEN ASM_REWRITE_TAC[DOT_LNEG]
 644 THEN POP_ASSUM MP_TAC
 645 THEN REAL_ARITH_TAC;(*4*)
 646
 647 DISJ_CASES_TAC(REAL_ARITH`azim x v u w <= azim x v u (y:real^3) \/ azim x v u y < azim x v u w`)
 648 THENL(*5*)[
 649 ABBREV_TAC`a1=(v-x):real^3`
 650 THEN ABBREV_TAC`a2=(y-x):real^3`
 651 THEN ABBREV_TAC`a3=(u-x) :real^3`
 652 THEN ABBREV_TAC`a4=w-x:real^3`
 653 THEN ABBREV_TAC`va=a1 cross a4:real^3`
 654 THEN ABBREV_TAC`vb=a2 cross a3:real^3`
 655 THEN ABBREV_TAC`v3= (vb:real^3) cross (va:real^3)+(x:real^3)`
 656 THEN ABBREV_TAC`v4= &1/ &2 % v3+ &1/ &2 % u:real^3`
 657 THEN MRESA_TAC cross_dot_fully_surrounded_fan[`x:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
 658 THEN POP_ASSUM MP_TAC
 659 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;CROSS_TRIPLE;]
 660 THEN ONCE_REWRITE_TAC[CROSS_SKEW; ]
 661 THEN ASM_REWRITE_TAC[DOT_LNEG]
 662 THEN STRIP_TAC
 663 THEN SUBGOAL_THEN `v3 IN aff_gt {x,u} {y:real^3}` ASSUME_TAC
 664 THENL(*6*)[
 665 MRESA_TAC th3[`(x:real^3)` ;` (u:real^3)`;`(y:real^3) `;]
 666 THEN MRESAL_TAC  AFF_GT_2_1[`x:real^3`;`u:real^3`;`y:real^3`][IN_ELIM_THM]
 667 THEN EXISTS_TAC`&1-(va:real^3) dot (a2:real^3)+va dot (a3:real^3)`
 668 THEN EXISTS_TAC`((va:real^3) dot (a2:real^3))`
 669 THEN EXISTS_TAC`(--((va:real^3) dot (a3:real^3)))`
 670 THEN ASM_REWRITE_TAC[REAL_ARITH`(&1 - va dot a3 + va dot a2) + (va dot a3) + --(va dot a2) = &1`;VECTOR_ARITH`(&1-A+B)%X+ (A)%U+ (--B) %V=A%(U-X)- B%(V-X)+X`]
 671 THEN EXPAND_TAC"v3"
 672 THEN EXPAND_TAC"vb"
 673 THEN ONCE_REWRITE_TAC[CROSS_SKEW; ]
 674 THEN REWRITE_TAC[CROSS_LAGRANGE;VECTOR_ARITH`--(A-B)+C=B-A+C:real^3`];(*6*)
 675 SUBGOAL_THEN `(v4:real^3) IN aff_gt {x,u} {y:real^3}` ASSUME_TAC
 676 THENL(*7*)[
 677 POP_ASSUM MP_TAC
 678 THEN MRESA_TAC th3[`(x:real^3)` ;` (u:real^3)`;`(y:real^3) `;]
 679 THEN MRESAL_TAC  AFF_GT_2_1[`x:real^3`;`u:real^3`;`y:real^3`][IN_ELIM_THM]
 680 THEN STRIP_TAC
 681 THEN EXISTS_TAC`&1/ &2 * t1:real`
 682 THEN EXISTS_TAC`&1/ &2 * t2+ &1/ &2:real`
 683 THEN EXISTS_TAC`&1/ &2*t3:real`
 684 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 / &2 * t1 + (&1 / &2 * t2 + &1 / &2) + &1 / &2 * t3 = &1/ &2*(t1+t2+t3)+ &1/ &2`; REAL_ARITH`&1/ &2 * &1 + &1/ &2= &1`;VECTOR_ARITH`(&1 / &2 * t1) % x + (&1 / &2 * t2 + &1 / &2) % u + (&1 / &2 * t3) % y= &1/ &2 %(t1 % x + t2 % u + t3 % y)+ &1/ &2 % u`]
 685 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)])
 686 THEN ASM_REWRITE_TAC[]
 687 THEN MATCH_MP_TAC REAL_LT_MUL
 688 THEN ASM_REWRITE_TAC[]
 689 THEN REAL_ARITH_TAC;(*7*)
 690 MRESA_TAC aff_gt_imp_not_collinear[`x:real^3`;`y:real^3`;`u:real^3`; `v4:real^3`]
 691 THEN MRESA_TAC AZIM_EQ_ALT[`x:real^3`;`u:real^3`;`w:real^3`; `v4:real^3`;`y:real^3`]
 692 THEN EXISTS_TAC`v4:real^3`
 693 THEN ASM_REWRITE_TAC[]
 694 THEN SUBGOAL_THEN `v3 IN aff_gt {x,v} {w:real^3}` ASSUME_TAC
 695 THENL(*8*)[
 696
 697 MRESA_TAC properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
 698 THEN MRESA_TAC notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 699 THEN MRESA_TAC th3[`(x:real^3)` ;` (v:real^3)`;`(w:real^3) `;]
 700 THEN MRESAL_TAC  AFF_GT_2_1[`x:real^3`;`v:real^3`;`w:real^3`][IN_ELIM_THM]
 701 THEN EXISTS_TAC`&1-(vb:real^3) dot (a4:real^3)+vb dot (a1:real^3)`
 702 THEN EXISTS_TAC`((vb:real^3) dot (a4:real^3))`
 703 THEN EXISTS_TAC`(--((vb:real^3) dot (a1:real^3)))`
 704 THEN ASM_REWRITE_TAC[REAL_ARITH`(&1 - vb dot a4 + vb dot a1) + (vb dot a4) + --(vb dot a1) = &1`;VECTOR_ARITH`(&1-A+B)%X+ (A)%U+ (--B) %V=A%(U-X)- B%(V-X)+X`]
 705 THEN EXPAND_TAC"v3"
 706 THEN EXPAND_TAC"va"
 707 THEN REWRITE_TAC[CROSS_LAGRANGE;VECTOR_ARITH`--(A-B)+C=B-A+C:real^3`]
 708 THEN MRESA_TAC cross_dot_fully_surrounded_fan[`x:real^3`;`v:real^3`;`y:real^3`;`u:real^3`]
 709 THEN POP_ASSUM MP_TAC
 710 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;CROSS_TRIPLE;]
 711 THEN ONCE_REWRITE_TAC[CROSS_SKEW; ]
 712 THEN ASM_REWRITE_TAC[DOT_LNEG]
 713 THEN DISCH_TAC
 714 THEN POP_ASSUM MATCH_MP_TAC
 715 THEN MRESA_TAC azim[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
 716 THEN FIND_ASSUM(MP_TAC)`~(azim x v u (y:real^3)= &0)`
 717 THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC
 718 THEN REAL_ARITH_TAC;(*8*)
 719
 720 REMOVE_THEN "YEU EM"(fun th-> ASM_REWRITE_TAC[SYM(th)])
 721 THEN MRESA_TAC properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
 722 THEN MRESA_TAC notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 723 THEN MRESA_TAC aff_gt_imp_not_collinear[`x:real^3`;`w:real^3`;`v:real^3`; `v3:real^3`]
 724 THEN MRESA_TAC AZIM_EQ_ALT[`x:real^3`;`v:real^3`;`u:real^3`; `v3:real^3`;`w:real^3`]
 725 THEN SUBGOAL_THEN`~(coplanar{x,v,u,v3:real^3})`ASSUME_TAC
 726 THENL(*9*)[
 727 STRIP_TAC
 728 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`v3:real^3`]
 729 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`];(*9*)
 730
 731 SUBGOAL_THEN`~(azim x u v3 (v:real^3)= &0)`ASSUME_TAC
 732 THENL(*10*)[
 733 POP_ASSUM MP_TAC
 734 THEN MATCH_MP_TAC MONO_NOT
 735 THEN ASM_REWRITE_TAC[]
 736 THEN STRIP_TAC
 737 THEN MRESA_TAC AZIM_EQ_0_PI_IMP_COPLANAR[`x:real^3`;`u:real^3`;`v3:real^3`;`v:real^3`]
 738 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
 739 THEN ASM_REWRITE_TAC[];(*10*)
 740 MRESA_TAC notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`v3:real^3`]
 741 THEN MRESA_TAC AZIM_EQ_ALT[`x:real^3`;`u:real^3`;`v:real^3`; `v3:real^3`;`y:real^3`]
 742 THEN POP_ASSUM MP_TAC
 743 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;]
 744 THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC"YEU EM")
 745 THEN MRESA_TAC AZIM_COMPL[`x:real^3`;`u:real^3`;`y:real^3`;`v:real^3`]
 746 THEN POP_ASSUM MP_TAC
 747 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;]
 748 THEN RESA_TAC
 749 THEN MRESA_TAC AZIM_COMPL[`x:real^3`;`u:real^3`;`v3:real^3`;`v:real^3`]
 750 THEN POP_ASSUM MP_TAC
 751 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;]
 752 THEN RESA_TAC
 753 THEN MP_TAC(REAL_ARITH`&2 * pi - azim x u y v = &2 * pi - azim x u v3 v==> azim x u v3 v= azim x u y v  `)
 754 THEN RESA_TAC
 755 THEN MRESAL_TAC inequality4_aim_in_convex_fan[`x:real^3`;`v:real^3`;`u:real^3`;`v3:real^3`;`&1/ &2`][REAL_ARITH`&1- &1/ &2= &1/ &2/\ &0< &1/ &2 /\ &1/ &2< &1`;VECTOR_ARITH`A+B=B+A:real^3`]
 756 THEN MATCH_MP_TAC  conditions_in_rcone_fan
 757 THEN EXISTS_TAC `y:real^3`
 758 THEN ASM_REWRITE_TAC[]
 759 THEN MRESA_TAC th3[`(x:real^3)` ;` (u:real^3)`;`(y:real^3) `;]
 760 THEN MRESAL_TAC  AFF_GT_1_2[`x:real^3`;`u:real^3`;`y:real^3`][IN_ELIM_THM]
 761 THEN EXISTS_TAC`&1/ &2 *(&1-(va:real^3) dot (a2:real^3)+va dot (a3:real^3))`
 762 THEN EXISTS_TAC`&1/ &2 *((va:real^3) dot (a2:real^3))+ &1/ &2`
 763 THEN EXISTS_TAC`&1/ &2 *(--((va:real^3) dot (a3:real^3)))`
 764 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 / &2 * t1 + (&1 / &2 * t2 + &1 / &2) + &1 / &2 * t3 = &1/ &2*(t1+t2+t3)+ &1/ &2`; REAL_ARITH`&1/ &2 * &1 + &1/ &2= &1`;VECTOR_ARITH`(&1 / &2 * t1) % x + (&1 / &2 * t2 + &1 / &2) % u + (&1 / &2 * t3) % y= &1/ &2 %(t1 % x + t2 % u + t3 % y)+ &1/ &2 % u`;REAL_ARITH`(&1 - va dot a3 + va dot a2) + (va dot a3) + --(va dot a2) = &1`;VECTOR_ARITH`(&1-A+B)%X+ (A)%U+ (--B) %V=A%(U-X)- B%(V-X)+X`]
 765 THEN EXPAND_TAC"v4"
 766 THEN EXPAND_TAC"v3"
 767 THEN EXPAND_TAC"vb"
 768 THEN ONCE_REWRITE_TAC[CROSS_SKEW; ]
 769 THEN REWRITE_TAC[CROSS_LAGRANGE;VECTOR_ARITH`--(A-B)+C=B-A+C:real^3`]
 770 THEN MP_TAC(REAL_ARITH`&0< --(va dot (a3:real^3))==> &0 < &1 / &2 * --(va dot a3)`)
 771 THEN RESA_TAC
 772 THEN MATCH_MP_TAC(REAL_ARITH`&0<= (va dot (a2:real^3))==> &0 < &1 / &2 * (va dot a2)+ &1/ &2`)
 773 THEN MRESA_TAC cross_dot_fully_surrounded_ge_fan[`x:real^3`;`v:real^3`;`y:real^3`;`w:real^3`]
 774 THEN POP_ASSUM MATCH_MP_TAC
 775 THEN MRESA_TAC sum4_azim_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`y:real^3`]
 776 THEN REWRITE_TAC[azim]
 777 THEN MATCH_MP_TAC(REAL_ARITH`azim x v u y = azim x v u w + azim x v w y/\ &0<= azim x v u w /\ azim x v u y < pi ==>azim x v w y <= pi`)
 778 THEN ASM_REWRITE_TAC[azim]](*10*)](*9*)](*8*)](*7*)](*6*);(*5*)
 779 EXISTS_TAC`y:real^3`
 780 THEN REMOVE_THEN "YEU EM" (fun th-> REWRITE_TAC[SYM(th)])
 781 THEN ASM_REWRITE_TAC[]]]]]]);;
 782
 783
 784
 785
 786 let exists_cut_rcone_fan_with_edge_run_fan=prove(
 787 `!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3 s:real.
 788 FAN(x,V,E)/\ {v,u} IN E /\ {u,w} IN E
 789 /\ sigma_fan x V E u w = v
 790 /\ &0<s /\ s<pi/ &2
 791 /\ fan80(x,V,E)
 792 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 793 ==>
 794 (?t:real. &0< t /\ t< &1 /\
 795 ~(rw_dart_fan x V E ((x:real^3),(u:real^3),(w:real^3),(sigma_fan x V E u w:real^3)) (cos(s)) INTER aff_gt {x} {v, (&1-t)%u+t%w}={}))`,
 796 REPEAT STRIP_TAC
 797 THEN POP_ASSUM MP_TAC
 798 THEN POP_ASSUM MP_TAC
 799 THEN DISCH_THEN(LABEL_TAC "BE")
 800 THEN DISCH_THEN(LABEL_TAC"EM")
 801 THEN USE_THEN "BE" MP_TAC
 802 THEN REWRITE_TAC[fan80]
 803 THEN DISCH_TAC
 804 THEN POP_ASSUM (fun th->   MRESA_TAC th [`u:real^3`;`w:real^3`]
 805 THEN MRESA_TAC th [`v:real^3`;`u:real^3`])
 806 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
 807 ` (v:real^3)`]
 808 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
 809 ` (u:real^3)`]
 810 THEN REMOVE_THEN "EM" (fun th-> MRESA1_TAC th `u:real^3` THEN MP_TAC (th) THEN DISCH_THEN(LABEL_TAC"EM"))
 811 THEN DISJ_CASES_TAC(SET_RULE`set_of_edge u V E = {w} \/ ~(set_of_edge u V E = {w:real^3})`)
 812 THENL[
 813 MRESA_TAC CARD_SING[`w:real^3`; `(set_of_edge u V E):real^3->bool`]
 814 THEN POP_ASSUM MP_TAC
 815 THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(th)])
 816 THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
 817 MRESA_TAC properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
 818 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`;rw_dart_fan;INTER; w_dart_fan;wedge;IN_ELIM_THM;]
 819 THEN MRESA_TAC inequality3_aim_in_convex_fan
 820 [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;` w:real^3`]
 821 THEN POP_ASSUM MP_TAC
 822 THEN DISCH_THEN(LABEL_TAC"NHO EM")
 823 THEN MRESA_TAC exists_point_inside_domain_cone_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `w:real^3`;`s:real`]
 824 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
 825 THEN ASM_REWRITE_TAC[rw_dart_fan;INTER; w_dart_fan;wedge;IN_ELIM_THM;]
 826 THEN REPEAT STRIP_TAC
 827 THEN MP_TAC(REAL_ARITH`azim x u w y< azim x u w v==> azim x u w y<= azim x u w (v:real^3)`)
 828 THEN RESA_TAC
 829 THEN MRESA_TAC sum4_azim_fan[`x:real^3`;`u:real^3`;`w:real^3`;`y:real^3`;`v:real^3`]
 830 THEN POP_ASSUM MP_TAC
 831 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 832 THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC"YEU EM")
 833 THEN MP_TAC(REAL_ARITH`azim x u w y< azim x u w v/\ &0< azim x u w y/\ azim x u w v < pi /\ azim x u w v = azim x u w y + azim x u y v==>  ~(azim x u y (v:real^3)= &0)/\ &0< azim x u y v/\ azim x u y v < pi/\ ~(azim x u y (v:real^3)= pi)`)
 834 THEN RESA_TAC
 835 THEN POP_ASSUM MP_TAC
 836 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`y:real^3`;`v:real^3`]
 837 THEN POP_ASSUM MP_TAC
 838 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 839 THEN RESA_TAC
 840 THEN POP_ASSUM MP_TAC
 841 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
 842 THEN REPEAT DISCH_TAC
 843 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR[`x:real^3`;`v:real^3`;`y:real^3`;`u:real^3`]
 844 THEN SUBGOAL_THEN`~(azim x v u (y:real^3)= &0)`ASSUME_TAC
 845 THENL[STRIP_TAC
 846 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
 847 THEN POP_ASSUM MP_TAC
 848 THEN REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
 849 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`y:real^3`;`v:real^3`]
 850 THEN POP_ASSUM MATCH_MP_TAC
 851 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 852 THEN ASM_REWRITE_TAC[];
 853 MP_TAC(REAL_ARITH`&0<= azim x v u (y:real^3) /\ ~(azim x v u y= &0)==> &0< azim x v u y`)
 854 THEN ASM_REWRITE_TAC[azim] THEN STRIP_TAC
 855 THEN MRESA_TAC angle_is_smallpi_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
 856 THEN ABBREV_TAC`a1=(v-x):real^3`
 857 THEN ABBREV_TAC`a2=(y-x):real^3`
 858 THEN ABBREV_TAC`a3=(u-x) :real^3`
 859 THEN ABBREV_TAC`a4=w-x:real^3`
 860 THEN ABBREV_TAC`va=a2 cross a1:real^3`
 861 THEN ABBREV_TAC`vb=a4 cross a3:real^3`
 862 THEN ABBREV_TAC`v3=(va:real^3) cross (vb:real^3)+(x:real^3)`
 863 THEN MRESA_TAC cut_in_angle_fan[`x:real^3`;`w:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
 864 THEN POP_ASSUM MP_TAC
 865 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
 866 THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
 867 THEN RESA_TAC
 868 THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN DISCH_TAC
 869 THEN MRESA_TAC scale_in_edges_fan[`(x:real^3)`;`(u:real^3)`;`(w:real^3)`;`(v3:real^3)`]
 870 THEN EXISTS_TAC`t:real`
 871 THEN ASM_REWRITE_TAC[]
 872 THEN EXISTS_TAC`y:real^3`
 873 THEN REMOVE_THEN "YEU EM" (fun th-> REWRITE_TAC[SYM(th)])
 874 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 875 THEN ASM_REWRITE_TAC[]
 876 THEN MP_TAC(REAL_ARITH`&0<t:real==> ~(t= &0)`) THEN RESA_TAC
 877 THEN MP_TAC(REAL_ARITH`&0<a:real==> ~(a= &0)`) THEN RESA_TAC
 878 THEN MRESA_TAC continuous_coplanar_fan [`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 879 THEN POP_ASSUM (fun th-> MRESA1_TAC th `t:real`)
 880 THEN MRESA_TAC notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`(&1 - t) % u + t % w:real^3`]
 881 THEN MRESAL_TAC aff_gt_1_2_scale_fan[`x:real^3`;`v:real^3`;`v3:real^3`;`(&1 - t) % u + t % w:real^3`;`a:real`][VECTOR_ARITH`(&1 - t) % u + t % w - x = ((&1 - t) % u + t % w) - x`]
 882 THEN POP_ASSUM MP_TAC
 883 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 884 THEN RESA_TAC
 885 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)])
 886 THEN MRESAL_TAC COLLINEAR_SPECIAL_SCALE[`a:real`;`(v3 - x):real^3`;`v-x:real^3`][VECTOR_ARITH`(&1 - t) % u + t % w - x = ((&1 - t) % u + t % w) - x`]
 887 THEN POP_ASSUM MP_TAC
 888 THEN EXPAND_TAC"a1"
 889 THEN ONCE_REWRITE_TAC[GSYM COLLINEAR_3]
 890 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,C,A}`]
 891 THEN ASM_REWRITE_TAC[]
 892 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 893 THEN STRIP_TAC
 894 THEN MRESA_TAC th3[`(x:real^3)` ;` (v3:real^3)`;`(v:real^3) `;]
 895 THEN MRESAL_TAC  AFF_GT_1_2[`x:real^3`;`v3:real^3`;`v:real^3`][IN_ELIM_THM;]
 896 THEN EXPAND_TAC"v3"
 897 THEN EXPAND_TAC"va"
 898 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
 899 THEN REWRITE_TAC[CROSS_LAGRANGE;]
 900 THEN MP_TAC(REAL_ARITH`azim x u w y < azim x u w v /\ azim x u w v< pi==> azim x u w y< pi`)
 901 THEN RESA_TAC
 902 THEN MRESA_TAC cross_dot_fully_surrounded_fan[`x:real^3`;`u:real^3`;`y:real^3`;`w:real^3`]
 903 THEN POP_ASSUM MP_TAC
 904 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
 905 THEN ASM_REWRITE_TAC[DOT_LNEG]
 906 THEN STRIP_TAC
 907 THEN MRESA_TAC cross_dot_fully_surrounded_fan[`x:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
 908 THEN POP_ASSUM MP_TAC
 909 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 910 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
 911 THEN ASM_REWRITE_TAC[DOT_LNEG]
 912 THEN STRIP_TAC
 913 THEN MP_TAC(REAL_ARITH`&0< --(vb dot (a1:real^3))==> ~(--(vb dot (a1:real^3))= &0)`) THEN RESA_TAC
 914 THEN MRESA1_TAC REAL_MUL_LINV `(--(vb dot (a1:real^3)):real)`
 915 THEN MRESA1_TAC REAL_LT_INV `(--(vb dot (a1:real^3)):real)`
 916 THEN MRESA_TAC REAL_LT_MUL [`inv(--(vb dot (a1:real^3)):real)`;`--(vb dot (a2:real^3)):real`]
 917 THEN EXISTS_TAC`&1- inv (--(vb dot (a1:real^3)))- inv (--(vb dot a1)) * --(vb dot a2)`
 918 THEN EXISTS_TAC`inv (--(vb dot (a1:real^3)))`
 919 THEN EXISTS_TAC`inv (--(vb dot a1)) * --(vb dot (a2:real^3))`
 920 THEN ASM_REWRITE_TAC[REAL_ARITH`&1- T1 -T2 +T1 +T2 = &1`;VECTOR_ARITH`A%(--(B%X-C%Y)+Z)=(A*(--B))%X-(A*(--C))%Y+A%Z:real^3`]
 921 THEN EXPAND_TAC"a1"
 922 THEN EXPAND_TAC"a2"
 923 THEN VECTOR_ARITH_TAC]]);;
 924
 925
 926
 927
 928
 929
 930
 931
 932
 933 let aff_gt_in_rw_dart_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3 y:real^3 s:real.
 934 FAN(x,V,E)/\ {v,u} IN E /\ {u,w} IN E
 935 /\ sigma_fan x V E u w = v
 936 /\ &0<s /\ s<pi/ &2
 937 /\ y IN rw_dart_fan x V E ((x:real^3),(u:real^3),(w:real^3),(v:real^3)) (cos(s))
 938 /\ fan80(x,V,E)
 939 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 940 ==> aff_gt {x} {u,y} SUBSET rw_dart_fan x V E ((x:real^3),(u:real^3),(w:real^3),(sigma_fan x V E u w:real^3)) (cos(s)) `,
 941 REPEAT STRIP_TAC
 942 THEN POP_ASSUM MP_TAC
 943 THEN POP_ASSUM MP_TAC
 944 THEN POP_ASSUM MP_TAC
 945 THEN DISCH_THEN(LABEL_TAC "CON")
 946 THEN DISCH_THEN(LABEL_TAC "BE")
 947 THEN DISCH_THEN(LABEL_TAC"EM")
 948 THEN USE_THEN "BE" MP_TAC
 949 THEN REWRITE_TAC[fan80]
 950 THEN DISCH_TAC
 951 THEN POP_ASSUM (fun th->   MRESA_TAC th [`u:real^3`;`w:real^3`]
 952 THEN MRESA_TAC th [`v:real^3`;`u:real^3`])
 953 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
 954 ` (v:real^3)`]
 955 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
 956 ` (u:real^3)`]
 957 THEN REMOVE_THEN "EM" (fun th-> MRESA1_TAC th `u:real^3` THEN MP_TAC (th) THEN DISCH_THEN(LABEL_TAC"EM"))
 958 THEN DISJ_CASES_TAC(SET_RULE`set_of_edge u V E = {w} \/ ~(set_of_edge u V E = {w:real^3})`)
 959 THENL[MRESA_TAC CARD_SING[`w:real^3`; `(set_of_edge u V E):real^3->bool`]
 960 THEN POP_ASSUM MP_TAC
 961 THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(th)])
 962 THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
 963 REMOVE_THEN "CON" MP_TAC
 964 THEN ASM_REWRITE_TAC[rw_dart_fan;INTER; SUBSET; w_dart_fan;wedge;IN_ELIM_THM;]
 965 THEN STRIP_TAC THEN GEN_TAC THEN STRIP_TAC
 966 THEN MRESA_TAC aff_gt_inter_aff_gt [`(x:real^3)`;`(u:real^3)`;`(y:real^3)`]
 967 THEN MP_TAC(SET_RULE`aff_gt {x} {u, y} = aff_gt {x, u} {y} INTER aff_gt {x, y} {u}
 968 /\ x' IN aff_gt {x} {u, y:real^3} ==> x' IN aff_gt {x,u} {y}`) THEN RESA_TAC
 969 THEN MRESA_TAC aff_gt_imp_not_collinear[`x:real^3`;`y:real^3`;`u:real^3`; `x':real^3`]
 970 THEN MRESA_TAC AZIM_EQ_ALT[`x:real^3`;`u:real^3`;`w:real^3`;`x':real^3`;`y:real^3`;]
 971 THEN MATCH_MP_TAC  conditions_in_rcone_fan
 972 THEN EXISTS_TAC`y:real^3`
 973 THEN ASM_REWRITE_TAC[]]);;
 974
 975
 976
 977
 978 let exists_rw_dart_inter_aff_gt1_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3 s:real.
 979 FAN(x,V,E)/\ {v,u} IN E /\ {u,w} IN E
 980 /\ sigma_fan x V E u w = v
 981 /\ &0<s /\ s<pi/ &2
 982 /\ fan80(x,V,E)
 983 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
 984 ==>
 985 (?h:real. &0< h /\
 986 (!t:real. &0< t /\ t< h==>
 987 ~(rw_dart_fan x V E ((x:real^3),(u:real^3),(w:real^3),(sigma_fan x V E u w:real^3)) (cos(s)) INTER aff_gt {x} {v, (&1-t)%u+t%w}={})
 988 ))`,
 989
 990 REPEAT STRIP_TAC
 991 THEN POP_ASSUM MP_TAC
 992 THEN POP_ASSUM MP_TAC
 993 THEN DISCH_THEN(LABEL_TAC "BE")
 994 THEN DISCH_THEN(LABEL_TAC"EM")
 995 THEN USE_THEN "BE" MP_TAC
 996 THEN REWRITE_TAC[fan80]
 997 THEN DISCH_TAC
 998 THEN POP_ASSUM (fun th->   MRESA_TAC th [`u:real^3`;`w:real^3`]
 999 THEN MRESA_TAC th [`v:real^3`;`u:real^3`])
1000 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
1001 ` (v:real^3)`]
1002 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
1003 ` (u:real^3)`]
1004 THEN REMOVE_THEN "EM" (fun th-> MRESA1_TAC th `u:real^3` THEN MP_TAC (th) THEN DISCH_THEN(LABEL_TAC"EM"))
1005 THEN DISJ_CASES_TAC(SET_RULE`set_of_edge u V E = {w} \/ ~(set_of_edge u V E = {w:real^3})`)
1006 THENL[ MRESA_TAC CARD_SING[`w:real^3`; `(set_of_edge u V E):real^3->bool`]
1007 THEN POP_ASSUM MP_TAC
1008 THEN POP_ASSUM(fun th->REWRITE_TAC[SYM(th)])
1009 THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
1010 MRESA_TAC exists_cut_rcone_fan_with_edge_run_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` v:real^3`;`u:real^3`;`w:real^3`;`s:real`]
1011 THEN POP_ASSUM MP_TAC
1012 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`;INTER;IN_ELIM_THM;]
1013 THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
1014 THEN DISCH_THEN(LABEL_TAC"OK") THEN DISCH_TAC
1015 THEN USE_THEN "OK" MP_TAC
1016 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[rw_dart_fan;]
1017 THEN ASM_REWRITE_TAC[INTER; w_dart_fan;wedge;IN_ELIM_THM;]
1018 THEN STRIP_TAC
1019 THEN EXISTS_TAC`t:real`
1020 THEN ASM_REWRITE_TAC[]
1021 THEN REPEAT STRIP_TAC
1022 THEN ABBREV_TAC`vt= (&1 - t':real) % u + t' % w :real^3`
1023 THEN ABBREV_TAC`a1=(v-x):real^3`
1024 THEN ABBREV_TAC`a2=vt-x:real^3`
1025 THEN ABBREV_TAC`a3=(y-x):real^3`
1026 THEN ABBREV_TAC`a4=(u-x) :real^3`
1027 THEN ABBREV_TAC`va=a1 cross a2:real^3`
1028 THEN ABBREV_TAC`vb=a3 cross a4:real^3`
1029 THEN ABBREV_TAC`v3=(vb:real^3) cross (va:real^3)+(x:real^3)`
1030 THEN MP_TAC(REAL_ARITH`&0< t'/\ t'< t /\ t< &1==> ~(t'= &0) /\ t'< &1`) THEN RESA_TAC
1031 THEN MRESA_TAC in_aff_gt_1_2[`x:real^3`;`u:real^3`;`w:real^3 `;`t':real`]
1032 THEN MRESA_TAC aff_gt_inter_aff_gt [`(x:real^3)`;`(u:real^3)`;`(w:real^3)`]
1033 THEN MP_TAC(SET_RULE`aff_gt {x} {u, w} = aff_gt {x, u} {w} INTER aff_gt {x, w} {u}
1034 /\ vt IN aff_gt {x} {u, w:real^3} ==> vt IN aff_gt {x,u} {w}`) THEN RESA_TAC
1035 THEN MRESA_TAC aff_gt_imp_not_collinear[`x:real^3`;`w:real^3`;`u:real^3`; `vt:real^3`]
1036 THEN MRESA_TAC properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
1037 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
1038 THEN POP_ASSUM MP_TAC
1039 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1040 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
1041 THEN ASM_REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC
1042 THEN MRESA_TAC AZIM_EQ_ALT[`x:real^3`;`u:real^3`;`v:real^3`;`vt:real^3`;`w:real^3`;]
1043 THEN POP_ASSUM MP_TAC
1044 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1045 THEN ASM_REWRITE_TAC[]
1046 THEN STRIP_TAC
1047 THEN MRESA_TAC AZIM_COMPL[`x:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
1048 THEN POP_ASSUM MP_TAC
1049 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;]
1050 THEN RESA_TAC
1051 THEN MRESA_TAC AZIM_COMPL[`x:real^3`;`u:real^3`;`v:real^3`;`vt:real^3`]
1052 THEN POP_ASSUM MP_TAC
1053 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`;]
1054 THEN RESA_TAC
1055 THEN POP_ASSUM MP_TAC
1056 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)])
1057 THEN STRIP_TAC
1058 THEN MRESA_TAC AZIM_EQ_ALT[`x:real^3`;`u:real^3`;`y:real^3`;`vt:real^3`;`w:real^3`;]
1059 THEN MP_TAC(REAL_ARITH`&0< azim x u w y /\ azim x u w y< azim x u w v /\ azim x u w v< pi==>
1060 azim x u w y<= azim x u w v/\ ~(azim x u w y = &0 \/ azim x u w y= pi)`) THEN RESA_TAC
1061 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`w:real^3`;`y:real^3`]
1062 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`y:real^3`;`w:real^3`]
1063 THEN POP_ASSUM MP_TAC
1064 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,B,D,C}`]
1065 THEN ASM_REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC
1066 THEN MRESA_TAC AZIM_COMPL[`x:real^3`;`u:real^3`;`y:real^3`;`w:real^3`]
1067 THEN MRESA_TAC AZIM_COMPL[`x:real^3`;`u:real^3`;`y:real^3`;`vt:real^3`]
1068 THEN POP_ASSUM MP_TAC
1069 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM(th)])
1070 THEN STRIP_TAC
1071 THEN MRESA_TAC continuous_coplanar_fan [`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
1072 THEN POP_ASSUM (fun th-> MRESA1_TAC th `t':real`)
1073 THEN MRESA_TAC cut_in_angle_fan[`x:real^3`;`v:real^3`;`u:real^3`;`vt:real^3`;`y:real^3`]
1074 THEN POP_ASSUM MP_TAC
1075 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
1076 THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
1077 THEN RESA_TAC
1078 THEN MRESA_TAC aff_gt_in_rw_dart_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`;`y:real^3`;`s:real`]
1079 THEN EXISTS_TAC`v3:real^3`
1080 THEN ASM_REWRITE_TAC[]
1081 THEN MATCH_MP_TAC(SET_RULE`aff_gt {x} {u, y} SUBSET rw_dart_fan x V E (x,u,w,v) (cos s)
1082 /\ v3 IN aff_gt {x} {u, y} ==> v3 IN rw_dart_fan x V E (x,u,w,v) (cos s)`)
1083 THEN ASM_REWRITE_TAC[]
1084 THEN MRESA_TAC cut_in_angle_fan[`x:real^3`;`y:real^3`;`v:real^3`;`u:real^3`;`vt:real^3`]
1085 THEN POP_ASSUM MP_TAC
1086 THEN CONV_TAC(TOP_DEPTH_CONV let_CONV)
1087 THEN ASM_REWRITE_TAC[]
1088 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
1089 THEN ASM_REWRITE_TAC[CROSS_LNEG;CROSS_RNEG]
1090 THEN ONCE_REWRITE_TAC[GSYM CROSS_RNEG]
1091 THEN ONCE_REWRITE_TAC[GSYM CROSS_SKEW]
1092 THEN RESA_TAC
1093 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1094 THEN POP_ASSUM  MATCH_MP_TAC
1095 THEN MRESA_TAC sum4_azim_fan[`x:real^3`;`u:real^3`;`w:real^3`;`y:real^3`;`v:real^3`]
1096 THEN POP_ASSUM MP_TAC
1097 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1098 THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(LABEL_TAC"NHO EM")
1099 THEN MP_TAC(REAL_ARITH`azim x u w y< azim x u w v/\ &0< azim x u w y/\ azim x u w v < pi /\ azim x u w v = azim x u w y + azim x u y v==>  ~(azim x u y (v:real^3)= &0 \/ azim x u y (v:real^3)= pi)`)
1100 THEN RESA_TAC
1101 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`u:real^3`;`y:real^3`;`v:real^3`]
1102 THEN POP_ASSUM MP_TAC
1103 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1104 THEN RESA_TAC
1105 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,C,B}`]
1106 THEN ASM_REWRITE_TAC[]
1107 THEN MRESA_TAC notcoplanar_imp_notcollinear_fan[`x:real^3`;`u:real^3`;`v:real^3`;`y:real^3`]
1108 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`]
1109 THEN POP_ASSUM MP_TAC
1110 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
1111 THEN ASM_REWRITE_TAC[DE_MORGAN_THM] THEN STRIP_TAC
1112 THEN MP_TAC(REAL_ARITH`&0<=azim x v u y /\ ~(azim x v u y= &0)==> &0< azim x v u y`)
1113 THEN ASM_REWRITE_TAC[azim] THEN RESA_TAC
1114 THEN MRESA_TAC notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`vt:real^3`]
1115 THEN MRESAL_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`x:real^3`;`v:real^3`;`u:real^3`;`vt:real^3`][DE_MORGAN_THM]
1116 THEN MP_TAC(REAL_ARITH`&0<=azim x v u vt /\ ~(azim x v u vt= &0)==> &0< azim x v u vt`)
1117 THEN ASM_REWRITE_TAC[azim] THEN RESA_TAC
1118 THEN MP_TAC(REAL_ARITH`&0<t==> ~(t= &0)`) THEN RESA_TAC
1119 THEN MRESA_TAC continuous_coplanar_fan [`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
1120 THEN POP_ASSUM (fun th-> MRESA1_TAC th `t:real`)
1121 THEN MRESA_TAC notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`(&1-t) %u+ t%w:real^3`]
1122 THEN MRESA_TAC aff_gt_inter_aff_gt [`(x:real^3)`;`(v:real^3)`;`((&1-t) %u+ t%w:real^3)`]
1123 THEN MP_TAC(SET_RULE`aff_gt {x} {v, (&1-t) %u+ t%w} = aff_gt {x, v} {(&1-t) %u+ t%w} INTER aff_gt {x, (&1-t) %u+ t%w} {v}
1124 /\ y IN aff_gt {x} {v, (&1-t) %u+ t%w:real^3} ==> y IN aff_gt {x,v} {(&1-t) %u+ t%w}`) THEN RESA_TAC
1125 THEN MRESA_TAC AZIM_EQ_ALT[`x:real^3`;`v:real^3`;`u:real^3`;`y:real^3`;`(&1-t) %u+ t%w:real^3`;]
1126 THEN MRESA_TAC inequality4_aim_in_convex_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`;`t:real`]
1127 THEN MRESA_TAC angle_is_smallpi_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
1128 THEN MP_TAC(REAL_ARITH`azim x v u w< pi /\ azim x v u ((&1 - t) % u + t % w) < azim x v u w
1129 ==> azim x v u ((&1 - t) % u + t % w) < pi`) THEN RESA_TAC
1130 THEN ABBREV_TAC`vs= (&1 - t:real) % u + t % w :real^3`
1131 THEN MRESA_TAC in_aff_gt_1_2[`x:real^3`;`u:real^3`;`w:real^3 `;`t:real`]
1132 THEN MP_TAC(SET_RULE`aff_gt {x} {u, w} = aff_gt {x, u} {w} INTER aff_gt {x, w} {u}
1133 /\ vs IN aff_gt {x} {u, w:real^3} ==> vs IN aff_gt {x,u} {w}`) THEN RESA_TAC
1134 THEN MRESA1_TAC REAL_MUL_LINV`t:real`
1135 THEN MRESA1_TAC REAL_LT_INV`t:real`
1136 THEN MRESA_TAC REAL_LT_MUL[`inv t:real`;`t':real`]
1137 THEN MRESA_TAC REAL_LT_LMUL[`inv t:real`;`t':real`;`t:real`]
1138
1139 THEN MRESA_TAC AZIM_EQ_ALT[`x:real^3`;`u:real^3`;`v:real^3`;`vs:real^3`;`w:real^3`;]
1140 THEN REMOVE_THEN"NHO EM" MP_TAC
1141 THEN DISCH_TAC THEN REMOVE_ASSUM_TAC
1142 THEN MRESA_TAC AZIM_COMPL[`x:real^3`;`u:real^3`;`v:real^3`;`vs:real^3`]
1143 THEN MRESA_TAC AZIM_COMPL[`x:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
1144 THEN MRESA_TAC inequality4_aim_in_convex_fan[`x:real^3`;`v:real^3`;`u:real^3`;`vs:real^3`;`inv (t) * t':real`]
1145 THEN POP_ASSUM MP_TAC
1146 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM(th)])
1147 THEN STRIP_TAC
1148 THEN MATCH_MP_TAC(SET_RULE`azim x v u ((&1 - inv t * t') % u + (inv t * t') % vs) < azim x v u vs /\
1149 (&1 - inv t * t') % u + (inv t * t') % vs = vt ==> azim x v u vt < azim x v u vs`)
1150 THEN ASM_REWRITE_TAC[]
1151 THEN EXPAND_TAC"vs"
1152 THEN ASM_REWRITE_TAC[VECTOR_ARITH`(&1 - inv t * t') % u + (inv t * t') % ((&1 - t) % u + t % w)
1153 = (&1 - (inv t * t) * t') % u + ((inv t * t) *t') % w`;REAL_ARITH`&1* A=A`]]);;
1154
1155
1156
1157
1158
1159 let there_exists_component_contain_aff_gt_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3.
1160 FAN(x,V,E)/\ {v,u} IN E /\ {u,w} IN E
1161 /\ sigma_fan x V E u w = v
1162 /\ fan80(x,V,E)
1163 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1164 ==>
1165  (?h:real. &0< h /\ (?y:real^3.
1166  aff_gt {x} {v, (&1-h)%u+h%w} SUBSET connected_component (yfan(x,V,E)) y ))`,
1167
1168 REPEAT STRIP_TAC
1169 THEN POP_ASSUM MP_TAC
1170 THEN POP_ASSUM MP_TAC
1171 THEN DISCH_THEN(LABEL_TAC "BE")
1172 THEN DISCH_THEN(LABEL_TAC"EM")
1173 THEN USE_THEN "BE" MP_TAC
1174 THEN REWRITE_TAC[fan80]
1175 THEN DISCH_TAC
1176 THEN POP_ASSUM (fun th->   MRESA_TAC th [`u:real^3`;`w:real^3`]
1177 THEN MRESA_TAC th [`v:real^3`;`u:real^3`])
1178 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (u:real^3)`;
1179 ` (v:real^3)`]
1180 THEN MRESA_TAC remark1_fan[`(x:real^3) `;`(V:real^3->bool)`;` (E:(real^3->bool)->bool) `;` (w:real^3)`;
1181 ` (u:real^3)`]
1182 THEN REMOVE_THEN "EM" (fun th-> MRESA1_TAC th `u:real^3` THEN MP_TAC (th) THEN DISCH_THEN(LABEL_TAC"EM"))
1183 THEN MRESA_TAC fan_run_in_small_is_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
1184 THEN POP_ASSUM(fun th-> MRESA1_TAC th `h/ &2`)
1185 THEN POP_ASSUM MP_TAC
1186 THEN MP_TAC(REAL_ARITH`&0< h==> ~(h/ &2 = &0)/\ &0< h/ &2 /\ h/ &2 < h`) THEN RESA_TAC
1187 THEN DISCH_TAC
1188 THEN EXISTS_TAC`h/ &2 :real`
1189 THEN ASM_REWRITE_TAC[]
1190 THEN EXISTS_TAC`&1/ &2 % v + &1/ &2 %((&1 - h / &2) % u + h / &2 % w:real^3)`
1191 THEN MATCH_MP_TAC CONNECTED_COMPONENT_MAXIMAL
1192 THEN ASM_REWRITE_TAC[]
1193 THEN MRESA_TAC CONVEX_AFF_GT[`{x:real^3}`;`{v, (&1 - h / &2) % u + h / &2 % w:real^3}`]
1194 THEN MRESA_TAC properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
1195 THEN MRESA_TAC continuous_coplanar_fan [`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
1196 THEN POP_ASSUM (fun th-> MRESA1_TAC th `h/ &2:real`)
1197 THEN MRESA_TAC notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`(&1-h/ &2) %u+  h / &2 %w:real^3`]
1198 THEN MRESA_TAC th3[`(x:real^3)` ;` (v:real^3)`;`(&1 - h/ &2) % (u:real^3) + h / &2 % (w:real^3)`;]
1199 THEN MRESAL_TAC in_aff_gt_1_2[`x:real^3`;`v:real^3`;`(&1 - h / &2) % u + h / &2 % w:real^3 `;`&1/ &2:real`]
1200 [REAL_ARITH`&1/ &2 < &1 /\ &0< &1/ &2 `; REAL_ARITH`&1 - &1/ &2 = &1/ &2` ]
1201 THEN MATCH_MP_TAC CONVEX_CONNECTED
1202 THEN ASM_REWRITE_TAC[]);;
1203
1204
1205
1206 let CONNECTED_COMPONENT_OF_SUBSET = prove
1207  (`!s t x y. s SUBSET t /\ connected_component s x y
1208            ==> connected_component t x y`,
1209   REWRITE_TAC[connected_component] THEN SET_TAC[]);;
1210
1211 let connected_component_of_faces_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) v:real^3 u:real^3 w:real^3.
1212 FAN(x,V,E)/\ {v,u} IN E /\ {u,w} IN E
1213 /\ sigma_fan x V E u w = v
1214 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1215 /\ fan80(x,V,E)
1216 ==>
1217 dart_leads_into x V E v u = dart_leads_into x V E u w`,
1218 REPEAT STRIP_TAC
1219 THEN POP_ASSUM MP_TAC
1220 THEN POP_ASSUM MP_TAC
1221 THEN DISCH_THEN(LABEL_TAC "BE")
1222 THEN DISCH_THEN(LABEL_TAC"con")
1223 THEN USE_THEN "con" MP_TAC
1224 THEN REWRITE_TAC[fan80]
1225 THEN DISCH_TAC
1226 THEN POP_ASSUM (fun th->   MRESA_TAC th [`u:real^3`;`w:real^3`]
1227 THEN MRESA_TAC th [`v:real^3`;`u:real^3`])
1228 THEN MRESA_TAC exists_leads_into_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;` u:real^3`]
1229 THEN POP_ASSUM MP_TAC
1230 THEN DISCH_THEN (LABEL_TAC"ANH")
1231 THEN MRESA_TAC exists_leads_into_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`u:real^3`;` w:real^3`]
1232 THEN POP_ASSUM MP_TAC
1233 THEN DISCH_THEN (LABEL_TAC"YEU")
1234 THEN ABBREV_TAC`h00= min h' (pi/ &2) / &2 :real`
1235 THEN MP_TAC(REAL_ARITH`&0< h' /\ &0< pi /\ h00= min h' (pi/ &2) / &2 :real==> &0< h00 /\ h00 < pi / &2`)
1236 THEN REWRITE_TAC[PI_WORKS]
1237 THEN RESA_TAC
1238 THEN MRESA_TAC exists_rw_dart_inter_aff_gt1_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` v:real^3`;` u:real^3`;` w:real^3`;`h00:real`]
1239 THEN POP_ASSUM MP_TAC
1240 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`]
1241 THEN DISCH_THEN (LABEL_TAC"EM")
1242 THEN MRESA_TAC exists_rw_dart_inter_aff_gt_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;` v:real^3`;` u:real^3`;` w:real^3`]
1243 THEN POP_ASSUM MP_TAC
1244 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`]
1245 THEN DISCH_THEN (LABEL_TAC"NHIEU")
1246 THEN MRESA_TAC fan_run_in_small_is_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`;`w:real^3`]
1247 THEN POP_ASSUM MP_TAC
1248 THEN DISCH_THEN (LABEL_TAC"HA")
1249 THEN ABBREV_TAC`h1' = min h'' h''' / &2 :real`
1250 THEN ABBREV_TAC`h1= min h1' h'''' / &2 :real`
1251 THEN MP_TAC(REAL_ARITH`&0< h'' /\ &0 < h''' /\ h1'= min h'' h''' / &2 ==> &0< h1' /\ h1'< h'' /\ h1' < h'''`)
1252 THEN RESA_TAC
1253 THEN MP_TAC(REAL_ARITH`&0< h1'/\ h1'< h'' /\ h1' < h''' /\ &0 < h'''' /\ h1= min h1' h'''' / &2 ==> &0< h1 /\ h1< h'' /\ h1 < h''' /\ h1< h''''`)
1254 THEN RESA_TAC
1255 THEN ABBREV_TAC`h2= min h (pi/ &2) / &2 :real`
1256 THEN MP_TAC(REAL_ARITH`&0< h /\ &0< pi /\ h2= min h (pi/ &2) / &2 :real==> &0< h2 /\ h2 < pi / &2`)
1257 THEN REWRITE_TAC[PI_WORKS]
1258 THEN RESA_TAC
1259 THEN REMOVE_THEN "NHIEU" (fun th-> MRESAL1_TAC th `h1:real`[INTER;IN_ELIM_THM])
1260 THEN POP_ASSUM (fun th-> MRESA1_TAC th `h2:real`)
1261 THEN MP_TAC(REAL_ARITH`&0< h2 /\ h2= min h (pi/ &2) / &2 :real==>  h2 < h`)
1262 THEN RESA_TAC
1263 THEN USE_THEN "ANH" (fun th -> MP_TAC(ISPECL[`h2:real`;`y:real^3`]th))
1264 THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1265 THEN RESA_TAC
1266 THEN POP_ASSUM MP_TAC
1267 THEN DISCH_THEN (LABEL_TAC"LAM")
1268 THEN REMOVE_THEN "EM" (fun th-> MRESAL1_TAC th `h1:real`[INTER;IN_ELIM_THM])
1269 THEN MP_TAC(REAL_ARITH`&0< h00 /\ h00= min h' (pi/ &2) / &2 :real==>  h00 < h'`)
1270 THEN RESA_TAC
1271 THEN USE_THEN "YEU" (fun th -> MP_TAC(ISPECL[`h00:real`;`y':real^3`]th))
1272 THEN POP_ASSUM (fun th-> REWRITE_TAC[th])
1273 THEN RESA_TAC
1274 THEN SUBGOAL_THEN `U=U':real^3->bool` ASSUME_TAC
1275 THENL[
1276 REMOVE_THEN "LAM" (fun th-> REWRITE_TAC[SYM(th)])
1277 THEN POP_ASSUM  (fun th-> REWRITE_TAC[SYM(th)])
1278 THEN REWRITE_TAC[CONNECTED_COMPONENT_EQ_EQ]
1279 THEN MRESA_TAC CONVEX_AFF_GT[`{x:real^3}`;`{v, (&1 - h1) % u + h1  % w:real^3}`]
1280 THEN MRESA_TAC CONVEX_CONNECTED[`aff_gt {x} {v, (&1 - h1) % u + h1 % w}:real^3->bool`]
1281 THEN POP_ASSUM MP_TAC
1282 THEN REWRITE_TAC[CONNECTED_IFF_CONNECTED_COMPONENT]
1283 THEN DISCH_TAC
1284 THEN POP_ASSUM (fun th-> MRESA_TAC th [`y:real^3`;`y':real^3`])
1285 THEN REMOVE_THEN "HA" (fun th-> MRESA1_TAC th `h1:real`)
1286 THEN MRESA_TAC CONNECTED_COMPONENT_OF_SUBSET[`aff_gt {x} {v, (&1 - h1) % u + h1 % w:real^3}:real^3-> bool`;`yfan (x:real^3,(V:real^3->bool),(E:(real^3->bool)->bool)):real^3->bool`;`y:real^3`;`y':real^3`]
1287 THEN ASM_TAC THEN SET_TAC[];
1288 SUBGOAL_THEN`dart_leads_into x V E v u= U:real^3->bool` ASSUME_TAC
1289 THENL[
1290 REMOVE_ASSUM_TAC
1291 THEN MATCH_MP_TAC unique_dart_leads_into
1292 THEN ASM_REWRITE_TAC[]
1293 THEN EXISTS_TAC`h:real`
1294 THEN ASM_REWRITE_TAC[];
1295
1296 SUBGOAL_THEN`dart_leads_into x V E u w= U':real^3->bool` ASSUME_TAC
1297 THENL[ MATCH_MP_TAC unique_dart_leads_into
1298 THEN ASM_REWRITE_TAC[]
1299 THEN EXISTS_TAC`h':real`
1300 THEN ASM_REWRITE_TAC[];
1301 ASM_REWRITE_TAC[]]]]);;
1302
1303
1304
1305
1306 (************************)
1307
1308 let dart_leads_into1 = new_definition
1309     `dart_leads_into1 (x,V,E) (v,u) = @s.  s IN topological_component_yfan (x,V,E) /\
1310         (?eps. (eps < &1) /\
1311            rw_dart_fan x V E (x,v,u,sigma_fan x V E v u) eps  SUBSET s)`;;
1312
1313
1314 let dartset_leads_into = new_definition
1315   `dartset_leads_into (x,V,E) ds =
1316     @s. (!y. (y IN ds) ==> (s = dart_leads_into1 (x,V,E) y))`;;
1317
1318
1319
1320 let exists_dartset_leads_into_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds.
1321 FAN(x,V,E)
1322 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1323 /\ fan80(x,V,E)
1324 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
1325 ==>
1326 ?s:real^3->bool. !y. y IN ds==> s= dart_leads_into x V E (pr2 y) (pr3 y)`,
1327
1328 REPEAT STRIP_TAC
1329 THEN POP_ASSUM MP_TAC
1330 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)))`]
1331 THEN ASM_REWRITE_TAC[face_set;set_of_orbits;IN_ELIM_THM]
1332 THEN STRIP_TAC
1333 THEN EXISTS_TAC`dart_leads_into x V E (pr2 x') (pr3 x'):real^3->bool`
1334 THEN ASM_REWRITE_TAC[orbit_map;IN_ELIM_THM]
1335 THEN REPEAT STRIP_TAC
1336 THEN POP_ASSUM MP_TAC
1337 THEN POP_ASSUM MP_TAC
1338 THEN DISJ_CASES_TAC(SET_RULE`~(x' IN d1_fan (x,V,E) )\/ (x' IN d1_fan (x:real^3,V,E))`)
1339 THENL[MRESA_TAC id_power_enf_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool) `;`x':real^3#real^3#real^3#real^3` ;`n:num`;`(\t. res (t x V E) (d1_fan (x,V,E)))`]
1340 THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
1341 SPEC_TAC (`y:real^3#real^3#real^3#real^3`,`y:real^3#real^3#real^3#real^3`)
1342 THEN SPEC_TAC (`n:num`,`n:num`)
1343 THEN INDUCT_TAC
1344 THENL[
1345 REWRITE_TAC[POWER_0;I_THM]
1346 THEN SET_TAC[];
1347
1348 POP_ASSUM MP_TAC
1349 THEN MRESA_TAC into_domain_power_efn_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool) `;`n:num`;`(\t. res (t x V E) (d1_fan (x,V,E)))`]
1350 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':real^3#real^3#real^3#real^3` )
1351 THEN MRESA_TAC into_domain_power_efn_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool) `;`SUC n:num`;`(\t. res (t x V E) (d1_fan (x,V,E)))`]
1352 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':real^3#real^3#real^3#real^3` )
1353 THEN ABBREV_TAC`y1=(f1_fan x V E POWER n) (x':real^3#real^3#real^3#real^3)`
1354 THEN DISCH_THEN(LABEL_TAC "EM")
1355 THEN ASM_REWRITE_TAC[COM_POWER;o_DEF]
1356 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`y1:real^3#real^3#real^3#real^3`[ARITH_RULE`(n:num)>= 0`])
1357 THEN REPEAT STRIP_TAC
1358 THEN MRESA_TAC into_domain1_power_efn_fan[`x:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`n:num`]
1359 THEN POP_ASSUM(fun th-> MRESA1_TAC th`x':real^3#real^3#real^3#real^3`)
1360 THEN MRESA_TAC properties_of_f1_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`y:real^3#real^3#real^3#real^3`; `y1:real^3#real^3#real^3#real^3`]
1361 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"EM") THEN REPEAT STRIP_TAC
1362 THEN ABBREV_TAC`u=pr2 (f1_fan x V E y1):real^3`
1363 THEN ABBREV_TAC`w=pr3 (f1_fan x V E y1):real^3`
1364 THEN ABBREV_TAC`v=sigma_fan x V E u w:real^3`
1365 THEN REMOVE_THEN "EM" MP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC
1366 THEN MRESA_TAC connected_component_of_faces_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`v:real^3`;`u:real^3`; `w:real^3`]]]);;
1367
1368
1369
1370
1371 let dartset_leads_into_fan = new_definition
1372   `dartset_leads_into_fan x V E ds =
1373     @s. (!y. (y IN ds) ==> (s = dart_leads_into x V E (pr2 y) (pr3 y)))`;;
1374
1375
1376
1377 let DARTSET_LEADS_INTO_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds.
1378 FAN(x,V,E)
1379 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1380 /\ fan80(x,V,E)
1381 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
1382 ==>
1383 (!y. y IN ds==> dartset_leads_into_fan x V E ds= dart_leads_into x V E (pr2 y) (pr3 y))`,
1384 REPEAT GEN_TAC THEN STRIP_TAC
1385 THEN ONCE_REWRITE_TAC[dartset_leads_into_fan]
1386 THEN MRESA_TAC exists_dartset_leads_into_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;
1387 `ds:real^3#real^3#real^3#real^3->bool`]
1388 THEN SELECT_ELIM_TAC
1389 THEN EXISTS_TAC`s:real^3->bool`
1390  THEN ASM_REWRITE_TAC[]);;
1391
1392
1393
1394
1395
1396
1397
1398
1399 let UNIQUE_DARTSET_LEADS_INTO_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds s.
1400 FAN(x,V,E)
1401 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1402 /\ fan80(x,V,E)
1403 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
1404 /\ (!y. y IN ds==> s= dart_leads_into x V E (pr2 y) (pr3 y))
1405 ==> dartset_leads_into_fan x V E ds= s`,
1406 REPEAT STRIP_TAC
1407 THEN POP_ASSUM MP_TAC
1408 THEN MRESA_TAC FACE_FAN_NOT_EMPTY[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;
1409 `ds:real^3#real^3#real^3#real^3->bool`]
1410 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`]
1411 THEN STRIP_TAC
1412 THEN MRESA_TAC DARTSET_LEADS_INTO_FAN[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;
1413 `ds:real^3#real^3#real^3#real^3->bool`]
1414 THEN POP_ASSUM (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`)
1415 THEN DISCH_TAC
1416 THEN POP_ASSUM (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3`));;
1417
1418
1419
1420
1421 let equality_dart_leads_into=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds y y1.
1422 FAN(x,V,E)
1423 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1424 /\ fan80(x,V,E)
1425 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
1426 /\ y IN ds /\ y1 IN ds
1427
1428 ==>dart_leads_into x V E (pr2 y) (pr3 y)= dart_leads_into x V E (pr2 y1) (pr3 y1)`,
1429 REPEAT STRIP_TAC
1430 THEN MRESA_TAC exists_dartset_leads_into_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;
1431 `ds:real^3#real^3#real^3#real^3->bool`]
1432 THEN POP_ASSUM (fun th-> MRESA1_TAC th `y:real^3#real^3#real^3#real^3` THEN ASSUME_TAC(th))
1433 THEN POP_ASSUM (fun th-> MRESA1_TAC th `y1:real^3#real^3#real^3#real^3`));;
1434
1435
1436 let UNIQUE_DARTSET_LEADS_INTO1_FAN=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds s.
1437 FAN(x,V,E)
1438 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1439 /\ fan80(x,V,E)
1440 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
1441 /\ y IN ds /\ s= dart_leads_into x V E (pr2 y) (pr3 y)
1442 ==> dartset_leads_into_fan x V E ds= s`,
1443 REPEAT STRIP_TAC
1444 THEN SUBGOAL_THEN`(!y. y IN ds==> s= dart_leads_into (x:real^3) V E (pr2 y) (pr3 y))` ASSUME_TAC
1445 THENL[REPEAT STRIP_TAC
1446 THEN MRESA_TAC equality_dart_leads_into[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;
1447 `ds:real^3#real^3#real^3#real^3->bool`;`y:real^3#real^3#real^3#real^3`;`y':real^3#real^3#real^3#real^3`];
1448 MRESA_TAC UNIQUE_DARTSET_LEADS_INTO_FAN[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;
1449 `ds:real^3#real^3#real^3#real^3->bool`;`s:real^3->bool`]]);;
1450
1451
1452 let exists_point_dart_leads_into_fan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds.
1453 FAN(x,V,E)
1454 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1455 /\ fan80(x,V,E)
1456 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
1457 ==> ?y. y IN ds /\ dartset_leads_into_fan x V E ds =dart_leads_into x V E (pr2 y) (pr3 y)`,
1458
1459 REPEAT STRIP_TAC
1460 THEN MRESA_TAC FACE_FAN_NOT_EMPTY[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;
1461 `ds:real^3#real^3#real^3#real^3->bool`]
1462 THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?y. y IN A`]
1463 THEN STRIP_TAC
1464 THEN EXISTS_TAC`y:real^3#real^3#real^3#real^3`
1465 THEN ASM_REWRITE_TAC[]
1466 THEN MRESA_TAC UNIQUE_DARTSET_LEADS_INTO1_FAN [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;
1467 `ds:real^3#real^3#real^3#real^3->bool`;`(dart_leads_into x V E (pr2 y) (pr3 y)):real^3->bool`]);;
1468
1469
1470
1471
1472
1473
1474 let dartset_leads_into_is_topological_component_yfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds.
1475 FAN(x,V,E)
1476 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1477 /\ fan80(x,V,E)
1478 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
1479 ==> dartset_leads_into_fan x V E ds IN topological_component_yfan (x,V,E)`,
1480 REPEAT STRIP_TAC
1481 THEN MRESA_TAC exists_point_dart_leads_into_fan [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;
1482 `ds:real^3#real^3#real^3#real^3->bool`;]
1483 THEN MRESA_TAC properties_of_elements_in_face_fully_surroundedfan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`ds:real^3#real^3#real^3#real^3->bool`; `y:real^3#real^3#real^3#real^3`]
1484 THEN MRESA_TAC dart_leads_into_fan_in_topological_component_yfan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`pr2(y):real^3`; `pr3(y):real^3`]);;
1485
1486
1487 let dartset_leads_into_subset_yfan=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds:real^3#real^3#real^3#real^3->bool.
1488 FAN(x,V,E)
1489 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1490 /\ fan80(x,V,E)
1491 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
1492 ==>
1493 dartset_leads_into_fan x V E ds SUBSET yfan (x,V,E)`,
1494 REPEAT STRIP_TAC
1495 THEN MRESA_TAC dartset_leads_into_is_topological_component_yfan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`ds:real^3#real^3#real^3#real^3->bool`]
1496 THEN POP_ASSUM MP_TAC
1497 THEN REWRITE_TAC[topological_component_yfan;IN_ELIM_THM;]
1498 THEN STRIP_TAC
1499 THEN ASM_REWRITE_TAC[CONNECTED_COMPONENT_SUBSET]);;
1500
1501
1502
1503
1504 let RWXUYZZ=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds:real^3#real^3#real^3#real^3->bool.
1505 FAN(x,V,E)
1506 /\ (!v. v IN V==>CARD (set_of_edge v V E) >1)
1507 /\ fan80(x,V,E)
1508 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
1509 ==>
1510 (?s:real^3->bool. !y. y IN ds==> s= dart_leads_into x V E (pr2 y) (pr3 y))
1511 /\ dartset_leads_into_fan x V E ds IN topological_component_yfan (x,V,E)`,
1512 MESON_TAC[dartset_leads_into_is_topological_component_yfan;exists_dartset_leads_into_fan]);;
1513
1514
1515
1516
1517 end;;
1518
1519