text_formalization/fan/CFYXFTY.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  Cfyxfty = struct
  14
  15
  16
  17
  18
  19
  20
  21
  22
  23 open Sphere;;
  24 open Fan_defs;;
  25 open Hypermap;;
  26 open Vol1;;
  27 open Fan;;
  28 open Topology;;
  29 open Fan_misc;;
  30 open Planarity;;
  31 open Conforming;;
  32 open Sphere;;
  33 open Hypermap;;
  34 open Fan;;
  35 open Topology;;
  36 open Polyhedron;;
  37 open Prove_by_refinement;;
  38 open Nkezbfc_local;;
  39
  40
  41
  42 let EDGES0_FAN=new_definition`EDGES0_FAN (p:real^3->bool) f1={e | e IN (edges p) /\ ~(aff_gt {vec 0} e INTER closure(fchanged f1)={})}`;;
  43
  44
  45
  46
  47 let CONVEX_CLOSURE_DARTSET_LEADS_INTO_FAN=prove(`
  48 !p:real^3->bool f1:real^3#real^3#real^3#real^3->bool U:real^3->bool.
  49  bounded p /\ polyhedron p /\ vec 0 IN interior p
  50 /\ f1 IN face_set (hypermap1_of_fanx  (vec 0,vertices p,edges p))
  51 /\
  52 dartset_leads_into_fan (vec 0) (vertices p) (edges p) f1 =U
  53 ==> convex(closure U)`,
  54
  55 REPEAT STRIP_TAC
  56 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
  57 THEN MRESA1_TAC CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON`p:real^3->bool`
  58 THEN POP_ASSUM MP_TAC
  59 THEN DISCH_THEN(LABEL_TAC"LINH")
  60 THEN MRESA1_TAC POLYTOPE_FAN80`p:real^3->bool`
  61 THEN MRESAL_TAC PIIJBJK[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;][conforming_fan;conforming_half_space_fan]
  62 THEN REMOVE_ASSUM_TAC
  63 THEN REMOVE_ASSUM_TAC
  64 THEN POP_ASSUM (fun th-> MRESA1_TAC th`f1:real^3#real^3#real^3#real^3->bool`)
  65 THEN MATCH_MP_TAC CONVEX_CLOSURE
  66 THEN MATCH_MP_TAC CONVEX_INTERS
  67 THEN REWRITE_TAC[IN_ELIM_THM]
  68 THEN REPEAT RESA_TAC
  69 THEN MESON_TAC[CONVEX_AFF_GT]);;
  70
  71
  72 let WBLARHH_BIJ = prove_by_refinement(
  73   `!p:real^3->bool. bounded p /\ polyhedron p /\ vec 0 IN interior p ==>
  74  (BIJ
  75    (dartset_leads_into_fan (vec 0) (vertices p) (edges p))
  76    (face_set (hypermap1_of_fanx(vec 0,vertices p,edges p)))
  77    (topological_component_yfan (vec 0,vertices p, edges p)))`,
  78   (* {{{ proof *)
  79   [
  80 REWRITE_TAC [BIJ;INJ;SURJ;IN;IN_ELIM_THM];
  81 GEN_TAC ;
  82 STRIP_TAC ;
  83 MRESA_TAC (REWRITE_RULE[IN] POLYHEDRON_FAN) [`p:real^3->bool`;`vec 0:real^3`];
  84 MRESA1_TAC (REWRITE_RULE[IN] CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON)`p:real^3->bool`;
  85  MRESA1_TAC (REWRITE_RULE[IN] POLYTOPE_FAN80) `p:real^3->bool`;
  86 MRESA_TAC (REWRITE_RULE[IN] dartset_leads_into_is_topological_component_yfan) [`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`];
  87  MRESAL_TAC (REWRITE_RULE[IN] Conforming.PIIJBJK)[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;][REWRITE_RULE[IN] Conforming.conforming_fan;REWRITE_RULE[IN] Conforming.conforming_bijection_fan];
  88 ASM_MESON_TAC []
  89   ]);;
  90   (* }}} *)
  91
  92
  93
  94
  95
  96
  97 let CONVEX_CLOSURE_FCHANGED=prove(`!p:real^3->bool f U.
  98  bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p
  99 /\ f facet_of p /\
 100  fchanged f= U
 101 ==> convex(closure U)`,
 102 REPEAT STRIP_TAC
 103 THEN MRESA_TAC Polyhedron.FCHANGED_IN_COMPONENT[`f:real^3->bool`;`p:real^3->bool`]
 104 THEN MRESAL1_TAC WBLARHH_BIJ`p:real^3->bool`[BIJ;SURJ]
 105 THEN POP_ASSUM(fun th-> MRESA1_TAC th`U:real^3->bool`)
 106 THEN MRESAL1_TAC WBLARHH`p:real^3->bool`[]
 107 THEN POP_ASSUM(fun th-> MRESA1_TAC th`y:real^3#real^3#real^3#real^3->bool`)
 108 THEN MRESA_TAC CONVEX_CLOSURE_DARTSET_LEADS_INTO_FAN[`p:real^3->bool`; `y:real^3#real^3#real^3#real^3->bool`;` U:real^3->bool`] );;
 109
 110
 111 let GINGUAP=prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds.
 112 FAN(x,V,E)
 113 /\ conforming_fan (x,V,E)
 114 /\ ds IN face_set(hypermap1_of_fanx (x,V,E))
 115 ==>   convex(dartset_leads_into_fan x V E ds)`,
 116
 117 REWRITE_TAC[conforming_fan;conforming_half_space_fan]
 118 THEN REPEAT STRIP_TAC
 119 THEN POP_ASSUM MP_TAC
 120 THEN POP_ASSUM MP_TAC
 121 THEN POP_ASSUM MP_TAC
 122 THEN POP_ASSUM MP_TAC
 123 THEN DISCH_THEN(LABEL_TAC"EM")
 124 THEN REPEAT STRIP_TAC
 125 THEN REMOVE_THEN "EM"(fun th-> MRESA1_TAC th`ds:real^3#real^3#real^3#real^3->bool`)
 126 THEN MATCH_MP_TAC CONVEX_INTERS
 127 THEN REWRITE_TAC[IN_ELIM_THM]
 128 THEN REPEAT STRIP_TAC
 129 THEN ASM_REWRITE_TAC[CONVEX_AFF_GT]);;
 130
 131
 132
 133
 134
 135
 136 let AFF_GT_SUBSET_DARTSET_LEADS_INTO= prove(`!x:real^3 (V:real^3->bool) (E:(real^3->bool)->bool) ds y z.
 137 FAN(x,V,E)
 138 /\ conforming_fan (x,V,E)
 139  /\ (!v. v IN V==>CARD (set_of_edge v V E) > 1)
 140 /\ fan80(x,V,E)
 141 /\ ds IN face_set (hypermap1_of_fanx (x,V,E))
 142 /\ y IN dartset_leads_into_fan x V E ds
 143 /\ z IN dartset_leads_into_fan x V E ds
 144 ==> aff_gt {x} {y,z}  SUBSET dartset_leads_into_fan x V E ds`,
 145 REPEAT STRIP_TAC
 146 THEN MRESA_TAC Planarity.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)`]
 147 THEN MRESA_TAC nonsetedge_fully_surround_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
 148 THEN MRESA_TAC point_in_yfan_not_x_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`dartset_leads_into_fan x V E ds`;` z:real^3`]
 149 THEN MRESA_TAC point_in_yfan_not_x_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`dartset_leads_into_fan x V E ds`;` y:real^3`]
 150 THEN MRESAL_TAC GINGUAP[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`ds:(real^3#real^3#real^3#real^3->bool)`][CONVEX_CONTAINS_SEGMENT]
 151 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`y:real^3`;`z:real^3`][segment;SUBSET;IN_ELIM_THM])
 152 THEN SUBGOAL_THEN`(!t. &0 < t /\ t < &1 ==> (&1 - t) % y + t % z IN yfan (x:real^3,V:real^3->bool,E))` ASSUME_TAC
 153 THENL[
 154 POP_ASSUM MP_TAC
 155 THEN DISCH_THEN(LABEL_TAC"LINH")
 156 THEN REPEAT STRIP_TAC
 157 THEN REMOVE_THEN "LINH" (fun th-> MRESA1_TAC th`(&1 - t) % y + t % z:real^3`)
 158 THEN POP_ASSUM MP_TAC
 159 THEN SUBGOAL_THEN`(?u. (&0 <= u /\ u <= &1) /\
 160            (&1 - t) % y + t % z = (&1 - u) % y + u % z:real^3)` ASSUME_TAC
 161 THENL[
 162 EXISTS_TAC`t:real`
 163 THEN REWRITE_TAC[]
 164 THEN POP_ASSUM MP_TAC
 165 THEN POP_ASSUM MP_TAC
 166 THEN REAL_ARITH_TAC;
 167 RESA_TAC
 168 THEN POP_ASSUM MP_TAC
 169 THEN MRESA_TAC Planarity.dartset_leads_into_subset_yfan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`ds:(real^3#real^3#real^3#real^3->bool)`]
 170 THEN POP_ASSUM MP_TAC
 171 THEN SET_TAC[]];
 172 MRESAL_TAC Planarity.aff_gt_subset_component_y_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`dartset_leads_into_fan x V E ds`;`y:real^3`;`z:real^3`][SET_RULE`DISJOINT {x} {y, z}<=> ~(x=y) /\ ~(x=z)`;SUBSET]]);;
 173
 174
 175 let FACET_SUBSET_CLOSURE_FCHANGED=prove(`!p:real^3->bool f.
 176  bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p
 177 /\ f facet_of p
 178 ==> f SUBSET closure(fchanged f)`,
 179
 180 REPEAT STRIP_TAC
 181 THEN MRESA_TAC Polyhedron.RELATIVE_SUBSET_FCHANGE[`p:real^3->bool`;`vec 0:real^3`;`f:real^3->bool`]
 182 THEN MRESA_TAC FACET_OF_IMP_FACE_OF[`f:real^3->bool`;`p:real^3->bool`]
 183 THEN MRESA_TAC FACE_OF_POLYHEDRON_POLYHEDRON[`p:real^3->bool`;`f:real^3->bool`]
 184 THEN POP_ASSUM MP_TAC
 185 THEN REWRITE_TAC[POLYHEDRON_EQ_FINITE_FACES]
 186 THEN STRIP_TAC
 187 THEN MRESA1_TAC CONVEX_CLOSURE_RELATIVE_INTERIOR`f:real^3->bool`
 188 THEN MRESA_TAC SUBSET_CLOSURE[`relative_interior f:real^3->bool`;`fchanged f:real^3->bool`]
 189 THEN MRESA1_TAC CLOSURE_SUBSET`f:real^3->bool`
 190 THEN POP_ASSUM MP_TAC
 191 THEN POP_ASSUM MP_TAC
 192 THEN SET_TAC[]);;
 193
 194
 195
 196
 197
 198 let MAP_EDGES_FACET_INTO_E1_FAN=prove_by_refinement(`!p:real^3->bool f e.
 199  bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p
 200 /\ f facet_of p
 201 /\ e IN edges f
 202 ==> e IN EDGES0_FAN p f `,
 203
 204 [ REWRITE_TAC[EDGES0_FAN;IN_ELIM_THM;edges]
 205 THEN REPEAT STRIP_TAC;
 206 ASM_TAC
 207 THEN REWRITE_TAC[edge_of;facet_of]
 208 THEN REPEAT STRIP_TAC
 209 THEN EXISTS_TAC`v:real^3`
 210 THEN EXISTS_TAC`w:real^3`
 211 THEN ASM_REWRITE_TAC[]
 212 THEN ASM_MESON_TAC[FACE_OF_TRANS];
 213 POP_ASSUM MP_TAC
 214 THEN MRESA_TAC FACET_SUBSET_CLOSURE_FCHANGED[`p:real^3->bool`;`f:real^3->bool`]
 215 THEN MRESA_TAC EDGE_OF_IMP_SUBSET[`segment [v,w:real^3]`;`f:real^3->bool`]
 216 THEN MRESA_TAC SEGMENT_OPEN_SUBSET_CLOSED[`v:real^3`;`w:real^3`]
 217 THEN MRESA_TAC SEGMENT_EDGE_OF[`f:real^3->bool`;`v:real^3`;`w:real^3`]
 218 THEN ABBREV_TAC`t= &1/ &2 % v+ &1/ &2 % w:real^3`
 219 THEN SUBGOAL_THEN`?u1. &0 < u1 /\ u1 < &1 /\ t = (&1 - u1) % v + u1 % w:real^3`
 220 ASSUME_TAC;
 221 EXISTS_TAC`&1/ &2`
 222 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - &1/ &2= &1/ &2`]
 223 THEN REAL_ARITH_TAC;
 224 MRESA_TAC IN_SEGMENT[`v:real^3`;`w:real^3`;`t:real^3`]
 225 THEN SUBGOAL_THEN`t IN closure(fchanged f:real^3->bool)`ASSUME_TAC;
 226 ASM_TAC
 227 THEN SET_TAC[];
 228 REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;INTER;IN_ELIM_THM]
 229 THEN EXISTS_TAC`t:real^3`
 230 THEN ASM_REWRITE_TAC[]
 231 THEN MRESA_TAC facet_of[`f:real^3->bool`;`p:real^3->bool`]
 232 THEN MRESA_TAC EXTREME_POINT_OF_FACE[`f:real^3->bool`;`p:real^3->bool`;`v:real^3`]
 233 THEN MRESA_TAC EXTREME_POINT_OF_FACE[`f:real^3->bool`;`p:real^3->bool`;`w:real^3`]
 234 THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`v:real^3`]
 235 THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`w:real^3`]
 236 THEN MP_TAC(SET_RULE`~(v IN interior p) /\ ~(w IN interior p) /\ (vec 0 IN interior p)==> DISJOINT{vec 0} {v,w:real^3}`)
 237 THEN RESA_TAC
 238 THEN MRESAL_TAC AFF_GT_1_2[`vec 0:real^3`;`v:real^3`;`w:real^3`][IN_ELIM_THM]
 239 THEN EXISTS_TAC`&0`
 240 THEN EXISTS_TAC`&1/ &2`
 241 THEN EXISTS_TAC`&1/ &2`
 242 THEN ASM_REWRITE_TAC[VECTOR_ARITH`a % vec 0+ A+B=A+B`]
 243 THEN REAL_ARITH_TAC]);;
 244
 245 let LIM_NULL_CMUL_BOUNDED_FAN = prove
 246  (`!f g:A->real^N B net.
 247         eventually (\a. abs(f a) < B) net /\
 248         (g --> vec 0) net
 249         ==> ((\n. f n % g n) --> vec 0) net`,
 250   REPEAT GEN_TAC THEN REWRITE_TAC[tendsto] THEN STRIP_TAC THEN
 251   X_GEN_TAC `e:real` THEN DISCH_TAC THEN
 252   FIRST_X_ASSUM(MP_TAC o SPEC `e / (abs B + &1)`) THEN
 253   ASM_SIMP_TAC[REAL_LT_DIV; REAL_ARITH `&0 < abs x + &1`] THEN
 254   UNDISCH_TAC `eventually (\a. abs(f a) < B) (net:(A net))` THEN
 255   REWRITE_TAC[IMP_IMP; GSYM EVENTUALLY_AND] THEN
 256   MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MP) THEN
 257   REWRITE_TAC[dist; VECTOR_SUB_RZERO; o_THM; NORM_LIFT; NORM_MUL] THEN
 258   MATCH_MP_TAC ALWAYS_EVENTUALLY THEN X_GEN_TAC `x:A` THEN REWRITE_TAC[] THEN
 259   STRIP_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
 260   EXISTS_TAC `B * e / (abs B + &1)` THEN
 261   ASM_SIMP_TAC[REAL_LE_MUL2; REAL_ABS_POS; NORM_POS_LE; REAL_LT_IMP_LE] THEN
 262   REWRITE_TAC[REAL_ARITH `c * (a / b) = (c * a) / b`] THEN
 263   SIMP_TAC[REAL_LT_LDIV_EQ; REAL_ARITH `&0 < abs x + &1`] THEN
 264   MATCH_MP_TAC(REAL_ARITH
 265    `e * B <= e * abs B /\ &0 < e ==> B * e < e * (abs B + &1)`) THEN
 266   ASM_SIMP_TAC[REAL_LE_LMUL_EQ] THEN REAL_ARITH_TAC);;
 267
 268
 269
 270
 271
 272 let MAP_EDGES_FACET_INTO_E1_FAN_INJ=prove_by_refinement(`!p:real^3->bool f e.
 273  bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p
 274 /\ f facet_of p
 275 /\ e IN EDGES0_FAN p f
 276 ==> e IN edges f`,
 277 [REWRITE_TAC[EDGES0_FAN;IN_ELIM_THM;SET_RULE`~(A={})<=> ?a. a IN A`;INTER]
 278 THEN REPEAT STRIP_TAC
 279 THEN POP_ASSUM MP_TAC
 280 THEN FIND_ASSUM MP_TAC`e IN edges (p:real^3->bool)`
 281 THEN REWRITE_TAC[edges;IN_ELIM_THM;edge_of]
 282 THEN REPEAT STRIP_TAC
 283 THEN EXISTS_TAC`v:real^3`
 284 THEN EXISTS_TAC`w:real^3`
 285 THEN ASM_REWRITE_TAC[]
 286 THEN POP_ASSUM MP_TAC
 287 THEN REWRITE_TAC[CLOSURE_SEQUENTIAL;fchanged;IN_ELIM_THM]
 288 THEN STRIP_TAC
 289 THEN POP_ASSUM MP_TAC
 290 THEN POP_ASSUM MP_TAC
 291 THEN REWRITE_TAC[SKOLEM_THM;]
 292 THEN REPEAT STRIP_TAC
 293 THEN MRESAL_TAC CONVERGENT_IMP_CAUCHY[`x:num->real^3`;`a:real^3`][cauchy]
 294 THEN POP_ASSUM MP_TAC
 295 THEN MRESA_TAC FACET_OF_POLYHEDRON[`p:real^3->bool`;`f:real^3->bool`]
 296 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN ASSUME_TAC(SYM th))
 297 THEN SUBGOAL_THEN`!n. a' dot (v1:num->real^3) n=b:real ` ASSUME_TAC;
 298 MRESA1_TAC RELATIVE_INTERIOR`f:real^3->bool`
 299 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;IN_ELIM_THM] THEN REPEAT STRIP_TAC)
 300 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[SYM th;IN_ELIM_THM;INTER] THEN REPEAT STRIP_TAC)
 301 THEN ASM_TAC
 302 THEN SET_TAC[];
 303 FIND_ASSUM(fun th -> MP_TAC th THEN REWRITE_TAC[facet_of] THEN STRIP_TAC)`f facet_of (p:real^3->bool)`
 304 THEN POP_ASSUM MP_TAC
 305 THEN DISJ_CASES_TAC(SET_RULE`f=p \/ ~(f=p:real^3->bool)`);
 306 ASM_REWRITE_TAC[]
 307 THEN REAL_ARITH_TAC;
 308 MRESA_TAC FACE_OF_DISJOINT_INTERIOR[`f:real^3->bool`;`p:real^3->bool`]
 309 THEN STRIP_TAC
 310 THEN REMOVE_ASSUM_TAC
 311 THEN DISJ_CASES_TAC(REAL_ARITH`(b= &0) \/ ~(b= &0)`);
 312 SUBGOAL_THEN`vec 0 IN (f:real^3->bool)`ASSUME_TAC;
 313 POP_ASSUM MP_TAC
 314 THEN POP_ASSUM MP_TAC
 315 THEN POP_ASSUM MP_TAC
 316 THEN POP_ASSUM MP_TAC
 317 THEN POP_ASSUM MP_TAC
 318 THEN POP_ASSUM MP_TAC
 319 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;INTER;IN_ELIM_THM;DOT_RZERO])
 320 THEN STRIP_TAC
 321 THEN RESA_TAC
 322 THEN MRESA1_TAC INTERIOR_SUBSET`p:real^3->bool`
 323 THEN REPEAT RESA_TAC
 324 THEN ASM_TAC
 325 THEN SET_TAC[];
 326  ASM_TAC
 327 THEN SET_TAC[];
 328 SUBGOAL_THEN`(lift o (t:num->real) --> lift(inv b *(a' dot a:real^3))) sequentially`ASSUME_TAC;
 329 MRESAL_TAC CONTINUOUS_ON_LIFT_DOT[`(:real^3)`;`a':real^3`;][GSYM CONVERGENT_EQ_CAUCHY]
 330 THEN MRESA_TAC CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN[`lift o (\y. (a':real^3) dot y)`;`(:real^3)`]
 331 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`a:real^3`[SET_RULE`(a:real^3) IN (:real^3)`])
 332 THEN MRESA_TAC (GEN_ALL CONTINUOUS_WITHIN_SEQUENTIALLY)[`(:real^3)`;`lift o (\y. (a':real^3) dot y)`;`(a:real^3)`]
 333 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num->real^3`[SET_RULE`(a:real^3) IN (:real^3)`;o_DEF;DOT_RMUL])
 334 THEN POP_ASSUM MP_TAC
 335 THEN REWRITE_TAC[LIM_SEQUENTIALLY;dist;GSYM LIFT_SUB;NORM_LIFT]
 336 THEN DISCH_THEN(LABEL_TAC"HA")
 337 THEN REPEAT STRIP_TAC
 338 THEN MRESA1_TAC REAL_ABS_CASES`b:real`
 339 THEN MRESA1_TAC REAL_LT_INV`abs (b:real)`
 340 THEN MRESA_TAC REAL_LT_MUL[`(abs b)`;`e':real`]
 341 THEN REMOVE_THEN "HA" (fun th-> MRESA1_TAC th`abs b * e'`)
 342 THEN EXISTS_TAC`N:num`
 343 THEN POP_ASSUM MP_TAC
 344 THEN DISCH_THEN(LABEL_TAC"THY")
 345 THEN REPEAT STRIP_TAC
 346 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th `n:num`)
 347 THEN MP_TAC(REAL_ARITH`&0< abs b==> ~(abs b= &0)`)
 348 THEN RESA_TAC
 349 THEN MRESA1_TAC REAL_MUL_LINV`abs b`
 350 THEN MRESA1_TAC REAL_MUL_LINV`b:real`
 351 THEN MRESAL_TAC REAL_LT_LMUL[`inv(abs b)`;`abs (((t:num->real) n) * b - a' dot (a:real^3))`;`(abs b) * e'`][REAL_ARITH`A*B*C=(A*B)*C/\ &1 *A=A`;]
 352 THEN POP_ASSUM MP_TAC
 353 THEN ASM_REWRITE_TAC[GSYM REAL_ABS_INV;GSYM REAL_ABS_MUL;REAL_ARITH`A*(b*c- D)= (A*c)* b- A*D/\ &1 * A=A`];
 354 SUBGOAL_THEN`!n:num. (v1 n) IN (f:real^3->bool)`ASSUME_TAC;
 355 MRESA1_TAC RELATIVE_INTERIOR`f:real^3->bool`
 356 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;IN_ELIM_THM] THEN REPEAT STRIP_TAC)
 357 THEN REMOVE_ASSUM_TAC
 358 THEN REMOVE_ASSUM_TAC
 359 THEN REMOVE_ASSUM_TAC
 360 THEN REMOVE_ASSUM_TAC
 361 THEN REMOVE_ASSUM_TAC
 362 THEN REMOVE_ASSUM_TAC
 363 THEN REMOVE_ASSUM_TAC
 364 THEN REMOVE_ASSUM_TAC
 365 THEN REMOVE_ASSUM_TAC
 366 THEN REMOVE_ASSUM_TAC
 367 THEN REMOVE_ASSUM_TAC
 368 THEN POP_ASSUM(fun th-> MRESA1_TAC th`n:num`)
 369 THEN ASM_REWRITE_TAC[];
 370 MRESA_TAC FACET_OF_IMP_SUBSET[`f:real^3->bool`;`p:real^3->bool`]
 371 THEN SUBGOAL_THEN `!n. norm ((v1:num->real^3) n) <= diameter (p:real^3->bool)` ASSUME_TAC;
 372 STRIP_TAC
 373 THEN POP_ASSUM MP_TAC
 374 THEN POP_ASSUM(fun th-> MRESA1_TAC th`n:num`)
 375 THEN STRIP_TAC
 376 THEN MRESA1_TAC INTERIOR_SUBSET`p:real^3->bool`
 377 THEN MP_TAC(SET_RULE`vec 0 IN interior p /\ interior p  SUBSET p==> vec 0 IN p:real^3->bool`)
 378 THEN RESA_TAC
 379 THEN MP_TAC(SET_RULE`(v1:num->real^3) n IN f /\ f SUBSET p:real^3->bool==> v1 n IN p`)
 380 THEN RESA_TAC
 381 THEN MRESA1_TAC DIAMETER_BOUNDED`p:real^3->bool`
 382 THEN REMOVE_ASSUM_TAC
 383 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(v1:num->real^3) n`;`(vec 0):real^3`][VECTOR_ARITH`A- vec 0=A`]);
 384 DISJ_CASES_TAC(SET_RULE`a' dot (a:real^3)= &0 \/ ~(a' dot (a:real^3)= &0)`);
 385  SUBGOAL_THEN(`(x --> (vec 0:real^3)) sequentially`) ASSUME_TAC;
 386 ASM_REWRITE_TAC[LIM_SEQUENTIALLY;dist;NORM_LIFT;VECTOR_ARITH`A- vec 0=A`;NORM_MUL]
 387 THEN REPEAT STRIP_TAC
 388 THEN FIND_ASSUM(MP_TAC)`(lift o t --> lift (inv b * (a' dot (a:real^3)))) sequentially`
 389 THEN REWRITE_TAC[LIM_SEQUENTIALLY;dist;GSYM LIFT_SUB;o_DEF;NORM_LIFT]
 390 THEN ASM_REWRITE_TAC[REAL_ARITH`A- B * &0=A`]
 391 THEN SUBGOAL_THEN`&0< diameter (p:real^3->bool)` ASSUME_TAC;
 392 REMOVE_ASSUM_TAC
 393 THEN REMOVE_ASSUM_TAC
 394 THEN POP_ASSUM(fun th-> MRESA1_TAC th`a1:num`)
 395 THEN POP_ASSUM MP_TAC
 396 THEN REMOVE_ASSUM_TAC
 397 THEN POP_ASSUM(fun th-> MRESA1_TAC th`a1:num`)
 398 THEN MP_TAC(SET_RULE`(v1:num->real^3) a1 IN f /\ f INTER interior p = {} /\ vec 0 IN interior p==> ~(v1 a1 = vec 0)`)
 399 THEN RESA_TAC
 400 THEN MRESA1_TAC NORM_POS_LT`(v1:num->real^3) a1`
 401 THEN POP_ASSUM MP_TAC
 402 THEN REAL_ARITH_TAC;
 403 MRESA1_TAC REAL_LT_INV`diameter (p:real^3->bool)`
 404 THEN MRESA_TAC REAL_LT_MUL[`inv (diameter (p:real^3->bool))`;`e':real`]
 405 THEN STRIP_TAC
 406 THEN POP_ASSUM(fun th-> MRESA1_TAC th`inv (diameter (p:real^3->bool)) * e'`)
 407 THEN POP_ASSUM MP_TAC
 408 THEN DISCH_THEN(LABEL_TAC"HA")
 409 THEN EXISTS_TAC`N:num`
 410 THEN REPEAT STRIP_TAC
 411 THEN REMOVE_THEN"HA"(fun th-> MRESA1_TAC th`n:num`)
 412 THEN MP_TAC(REAL_ARITH`&0 < diameter (p:real^3->bool)==> ~(diameter p= &0)`)
 413 THEN RESA_TAC
 414 THEN MRESA1_TAC REAL_MUL_LINV`(diameter (p:real^3->bool))`
 415 THEN MRESAL_TAC REAL_LT_LMUL[`(diameter (p:real^3->bool))`;`abs ((t:num->real) n)`;`inv (diameter (p:real^3->bool)) * e'`][REAL_ARITH`A*B*C=(B*A)*C/\ &1 *A=A`]
 416 THEN MRESAL_TAC REAL_LE_LMUL[`abs ((t:num->real) n)`;`norm ((v1:num->real^3) n)`;`(diameter (p:real^3->bool))`][REAL_ARITH`A*B*C=(B*A)*C/\ &1 *A=A`;REAL_ABS_POS]
 417 THEN POP_ASSUM MP_TAC
 418 THEN POP_ASSUM MP_TAC
 419 THEN REAL_ARITH_TAC;
 420 MRESAL_TAC LIM_UNIQUE[`sequentially`;`x:num-> real^3`;`a:real^3`;`vec 0:real^3`][TRIVIAL_LIMIT_SEQUENTIALLY]
 421 THEN MRESA_TAC SEGMENT_FACE_OF[`p:real^3->bool`;`v:real^3`;`w:real^3`]
 422 THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`v:real^3`]
 423 THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`w:real^3`]
 424 THEN MP_TAC(SET_RULE`~(v IN interior p) /\ ~(w IN interior p) /\ (vec 0 IN interior p)==> DISJOINT{vec 0} {v,w:real^3}`)
 425 THEN RESA_TAC
 426 THEN DISJ_CASES_TAC(SET_RULE`(vec 0 IN aff_gt {vec 0} {v, w:real^3}) \/ ~(vec 0 IN aff_gt {vec 0} {v, w})`);
 427 POP_ASSUM MP_TAC
 428  THEN MRESAL_TAC AFF_GT_1_2[`vec 0:real^3`;`v:real^3`;`w:real^3`][IN_ELIM_THM;VECTOR_ARITH`vec 0= t % vec 0 +A+B<=>  A+B=vec 0`]
 429 THEN REPEAT STRIP_TAC;
 430 SUBGOAL_THEN`vec 0 IN segment[v,w:real^3]`ASSUME_TAC;
 431 REMOVE_ASSUM_TAC
 432 THEN ASM_REWRITE_TAC[IN_SEGMENT]
 433 THEN EXISTS_TAC`inv (&1- t1) * t3`
 434 THEN POP_ASSUM MP_TAC
 435 THEN POP_ASSUM MP_TAC
 436 THEN REWRITE_TAC[REAL_ARITH`A+B+C= &1<=> B+C= &1- A`]
 437 THEN STRIP_TAC
 438 THEN MP_TAC(REAL_ARITH`&0< t2 /\ &0< t3 ==> ~(t2+ t3= &0)`)
 439 THEN RESA_TAC
 440 THEN MRESA1_TAC REAL_MUL_LINV`&1 - t1`
 441 THEN STRIP_TAC
 442 THEN MP_TAC(SET_RULE`t2 % v + t3 % w = vec 0:real^3 ==> (inv (t2+t3))%(t2 % v+ t3 % w) = (inv (t2+t3))%(vec 0)`)
 443 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
 444 THEN ASM_REWRITE_TAC[VECTOR_ARITH`a % vec 0= vec 0/\ A %(B+C)=A % B+A %C/\ A % D %C=(A*D)%C`]
 445 THEN STRIP_TAC
 446 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 447 THEN POP_ASSUM MP_TAC
 448 THEN POP_ASSUM MP_TAC
 449 THEN MP_TAC(SET_RULE`t2+ t3= &1- t1 ==> (inv (&1 - t1))*(t2 +t3) = (inv (&1-t1))*( &1- t1)`)
 450 THEN POP_ASSUM (fun th-> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th]
 451 THEN REWRITE_TAC[]
 452 THEN DISCH_THEN(LABEL_TAC"HA")
 453 THEN STRIP_TAC
 454 THEN STRIP_TAC
 455 THEN REMOVE_THEN "HA" MP_TAC
 456 THEN ASM_REWRITE_TAC[REAL_ARITH`A*(B+C)= &1 <=> A*B= &1 - A*C`]
 457 THEN RESA_TAC
 458 THEN ASSUME_TAC th)
 459 THEN MP_TAC(REAL_ARITH`&0< t2 /\ &0< t3 ==> &0 < t2+ t3`)
 460 THEN RESA_TAC
 461 THEN MRESA1_TAC REAL_LT_INV`&1 - t1`
 462 THEN MRESA_TAC REAL_LT_MUL[`inv(&1 -t1)`;`t3:real`]
 463 THEN MRESA_TAC REAL_LT_MUL[`inv(&1 -t1)`;`t2:real`]
 464 THEN MP_TAC(REAL_ARITH`&0 < inv (&1 - t1) * t3==> &0 <= inv (&1 - t1) * t3`)
 465 THEN RESA_TAC
 466 THEN POP_ASSUM MP_TAC
 467 THEN POP_ASSUM MP_TAC
 468 THEN REAL_ARITH_TAC;
 469 DISJ_CASES_TAC(SET_RULE`(segment [v,w] = p) \/ ~(segment [v,w:real^3] = p)`);
 470 POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
 471 THEN MRESA_TAC Polyhedron.AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`]
 472 THEN POP_ASSUM MP_TAC
 473 THEN ARITH_TAC;
 474 MRESA_TAC FACE_OF_DISJOINT_INTERIOR[`segment[v,w:real^3]`;`p:real^3->bool`]
 475 THEN ASM_TAC
 476 THEN SET_TAC[];
 477 POP_ASSUM MP_TAC
 478 THEN REMOVE_ASSUM_TAC
 479 THEN REMOVE_ASSUM_TAC
 480 THEN REMOVE_ASSUM_TAC
 481 THEN REMOVE_ASSUM_TAC
 482 THEN REMOVE_ASSUM_TAC
 483 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
 484 THEN FIND_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)`e={v,w:real^3}`
 485 THEN ASM_TAC
 486 THEN SET_TAC[];
 487 MRESA1_TAC REAL_INV_EQ_0`b:real`
 488 THEN MRESA_TAC Trigonometry2.NOT_MUL_EQ0_EQ[`inv b`;`a' dot (a:real^3)`]
 489 THEN MRESA_TAC LIM_INV[`sequentially`;`t:num->real`;`inv b * (a' dot a:real^3)`]
 490 THEN MRESA_TAC CONVERGENT_IMP_BOUNDED[`lift o inv o (t:num->real)`; `lift (inv(inv b * (a' dot (a:real^3))))`]
 491 THEN MRESAL_TAC tendsto[`lift o inv o (t:num->real)`; `lift (inv(inv b * (a' dot (a:real^3))))`;`sequentially`][o_DEF;dist;GSYM LIFT_SUB;NORM_LIFT]
 492 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`&1`[REAL_ARITH`&0< &1`])
 493 THEN MRESAL_TAC LIM_NULL_CMUL_BOUNDED_FAN[`(\n. inv ((t:num->real) n) - inv (inv b * (a' dot a:real^3)))`;`(\n. (x:num->real^3) n -a)`;`&1`;`sequentially`][GSYM LIM_NULL;VECTOR_ARITH`A%(B-C)=A%B-A%C /\ A% D%B=(A*D)%B`]
 494 THEN MRESA_TAC (GEN_ALL LIM_CMUL)[`sequentially`;`x:num->real^3`;`a:real^3`;`inv (inv b * (a' dot (a:real^3)))`]
 495 THEN MRESA_TAC LIM_NULL[`sequentially`;`(\x. inv (inv b * (a' dot a:real^3)) % t x % (v1:num->real^3) x)`;`inv (inv b * (a' dot a)) % a:real^3`]
 496 THEN MRESAL_TAC LIM_ADD[`sequentially`;`(\x. inv (inv b * (a' dot a:real^3)) % t x % (v1:num->real^3) x -inv (inv b * (a' dot a)) % a:real^3)`;`(\n:num. ((inv (t n) - inv (inv b * (a' dot a))) * t n) % v1 n -
 497             (inv (t n) - inv (inv b * (a' dot a))) % a:real^3)`;`vec 0:real^3`;`vec 0:real^3`][VECTOR_ARITH`inv (inv b * (a' dot a)) % t x % v1 x -
 498             inv (inv b * (a' dot a)) % a +
 499             ((inv (t x) - inv (inv b * (a' dot a))) * t x) % v1 x -
 500             (inv (t x) - inv (inv b * (a' dot a))) % a
 501 =(inv (t x)  * t x) % v1 x -
 502             (inv (t x) ) % a/\ vec 0+ vec 0= vec 0`]
 503 THEN SUBGOAL_THEN`((\n:num. inv (t n) % a:real^3) --> inv (inv b * (a' dot a)) % a:real^3) sequentially` ASSUME_TAC;
 504 REWRITE_TAC[LIM_SEQUENTIALLY;dist;GSYM VECTOR_SUB_RDISTRIB;NORM_MUL]
 505 THEN DISJ_CASES_TAC(SET_RULE`norm (a:real^3)= &0 \/ ~(norm a= &0)`);
 506 ASM_REWRITE_TAC[REAL_ARITH`A * &0= &0`]
 507 THEN REAL_ARITH_TAC;
 508 REPEAT STRIP_TAC
 509 THEN FIND_ASSUM MP_TAC`(lift o inv o t --> lift (inv (inv b * (a' dot a:real^3)))) sequentially`
 510 THEN REWRITE_TAC[LIM_SEQUENTIALLY;NORM_LIFT;dist;o_DEF;GSYM LIFT_SUB]
 511 THEN MP_TAC(REAL_ARITH`&0<= norm a /\ ~(norm a= &0)==> &0< norm (a:real^3) `)
 512 THEN ASM_REWRITE_TAC[NORM_POS_LE]
 513 THEN STRIP_TAC
 514 THEN MRESA1_TAC REAL_LT_INV`norm (a:real^3)`
 515 THEN MRESA1_TAC REAL_MUL_LINV`norm (a:real^3)`
 516 THEN MRESA_TAC REAL_LT_MUL[`e':real`;`inv(norm (a:real^3))`]
 517 THEN STRIP_TAC
 518 THEN POP_ASSUM(fun th-> MRESA1_TAC th` e' * inv(norm (a:real^3)) :real`)
 519 THEN POP_ASSUM MP_TAC
 520 THEN DISCH_THEN(LABEL_TAC"THY")
 521 THEN EXISTS_TAC`N:num`
 522 THEN REPEAT STRIP_TAC
 523 THEN REMOVE_THEN "THY"(fun th-> MRESA1_TAC th`n:num`)
 524 THEN MRESAL_TAC REAL_LT_RMUL[`abs (inv (t (n:num)) - inv (inv b * (a' dot (a:real^3))))`;`e' * inv (norm (a:real^3))`;`norm (a:real^3)`][REAL_ARITH`(a*b)*c=a*(b*c)/\ a * &1=a`];
 525 MRESA_TAC LIM_NULL[`sequentially`;`(\n:num. inv (t n) % (a:real^3))`;`inv (inv b * (a' dot a)) % (a:real^3)`]
 526 THEN MRESAL_TAC LIM_ADD[`sequentially`;`(\x:num. (inv (t x) * t x) % v1 x - inv (t x) % a:real^3)`;`(\x:num. inv (t x) % a - inv (inv b * (a' dot a)) % a:real^3)`;`vec 0:real^3`;`vec 0:real^3`][VECTOR_ARITH` A-B+B-C=A-C:real^3 /\ vec 0+ vec 0= vec 0`]
 527 THEN MRESA_TAC LIM_NULL[`sequentially`;`(\x:num. (inv (t x) * t x) % (v1:num->real^3) x)`;`inv (inv b * (a' dot a)) % (a:real^3)`]
 528 THEN POP_ASSUM MP_TAC
 529 THEN SUBGOAL_THEN`!n:num. inv( t n) * t n= &1 ` ASSUME_TAC;
 530 REPEAT STRIP_TAC
 531 THEN MATCH_MP_TAC REAL_MUL_LINV
 532 THEN MATCH_MP_TAC(REAL_ARITH`A > &0==> ~(A= &0)`)
 533 THEN ASM_REWRITE_TAC[];
 534 ASM_REWRITE_TAC[VECTOR_ARITH`&1 % A=A`]
 535 THEN STRIP_TAC
 536 THEN MP_TAC(SET_RULE`(!n:num. v1 n IN f:real^3->bool) /\ ((\n. v1 n) --> inv (inv b * (a' dot (a:real^3))) % (a:real^3)) sequentially ==> (?v1:num->real^3. (!n:num. v1 n IN f:real^3->bool) /\ (v1 --> inv (inv b * (a' dot (a:real^3))) % (a:real^3)) sequentially)`)
 537 THEN ASM_REWRITE_TAC[]
 538 THEN DISCH_TAC
 539 THEN MRESA_TAC CLOSURE_SEQUENTIAL[`f:real^3->bool`;`inv (inv b * (a' dot (a:real^3))) % (a:real^3)`]
 540 THEN POP_ASSUM MP_TAC
 541 THEN MRESA1_TAC POLYTOPE_EQ_BOUNDED_POLYHEDRON`p:real^3->bool`
 542 THEN MRESA_TAC FACE_OF_POLYTOPE_POLYTOPE[`f:real^3->bool`;`p:real^3->bool`]
 543 THEN MRESA1_TAC POLYTOPE_IMP_CLOSED`f:real^3->bool`
 544 THEN MRESA1_TAC CLOSURE_CLOSED`f:real^3->bool`
 545 THEN REPEAT STRIP_TAC
 546 THEN REMOVE_ASSUM_TAC
 547 THEN MP_TAC(SET_RULE`vec 0 IN interior p /\ interior p SUBSET (p:real^3->bool)
 548 /\ p SUBSET {x | a' dot x <= b} ==> a' dot vec 0<= b`)
 549 THEN ASM_REWRITE_TAC[INTERIOR_SUBSET;DOT_RZERO]
 550 THEN STRIP_TAC
 551 THEN MP_TAC(REAL_ARITH`&0<= b /\ ~(b= &0) ==> &0< b`)
 552 THEN RESA_TAC
 553 THEN DISJ_CASES_TAC(REAL_ARITH`&0< -- (a' dot (a:real^3)) \/ &0<= a' dot (a:real^3)`);
 554 MRESAL_TAC CONTINUOUS_ON_LIFT_DOT[`(:real^3)`;`a':real^3`;][GSYM CONVERGENT_EQ_CAUCHY]
 555 THEN MRESA_TAC CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN[`lift o (\y. (a':real^3) dot y)`;`(:real^3)`]
 556 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`a:real^3`[SET_RULE`(a:real^3) IN (:real^3)`])
 557 THEN MRESA_TAC (GEN_ALL CONTINUOUS_WITHIN_SEQUENTIALLY)[`(:real^3)`;`lift o (\y. (a':real^3) dot y)`;`(a:real^3)`]
 558 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`x:num->real^3`[SET_RULE`(a:real^3) IN (:real^3)`;o_DEF;DOT_RMUL])
 559 THEN POP_ASSUM MP_TAC
 560 THEN REWRITE_TAC[LIM_SEQUENTIALLY;dist;GSYM LIFT_SUB;NORM_LIFT]
 561 THEN MP_TAC(REAL_ARITH`&0< --(a' dot (a:real^3))==> &0< --(a' dot (a:real^3))/ &2`)
 562 THEN RESA_TAC
 563 THEN STRIP_TAC
 564 THEN POP_ASSUM(fun th-> MRESA1_TAC th`--(a' dot (a:real^3))/ &2`)
 565 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`N:num`[ARITH_RULE`N<=N:num`])
 566 THEN POP_ASSUM MP_TAC
 567 THEN MP_TAC(REAL_ARITH`(t:num->real) N > &0 ==> &0< t N`)
 568 THEN RESA_TAC
 569 THEN MRESA_TAC REAL_LT_MUL[`(t:num->real) N`;`b:real`]
 570 THEN MP_TAC(REAL_ARITH`&0< (t:num->real) N * b /\ &0< --(a' dot (a:real^3))  ==> &0< t N * b- a' dot a`)
 571 THEN RESA_TAC
 572 THEN MRESAL1_TAC (GEN_ALL Trigonometry2.LT_IMP_ABS_REFL)`(t:num->real) N * b- a' dot (a:real^3)`[REAL_ARITH`A - B < -- B/ &2<=> A< B/ &2`]
 573 THEN STRIP_TAC
 574 THEN MP_TAC(REAL_ARITH`(t:num->real) N * b < (a' dot (a:real^3))/ &2 /\ &0< --(a' dot (a:real^3))  ==> ~(&0< t N * b)`)
 575 THEN RESA_TAC;
 576 MP_TAC(REAL_ARITH`&0 <= (a' dot (a:real^3)) /\ ~(a' dot (a:real^3)= &0)  ==> &0< a' dot a`)
 577 THEN RESA_TAC
 578 THEN MRESA1_TAC REAL_LT_INV`b:real`
 579 THEN MRESA_TAC REAL_LT_MUL[`inv b:real`;`(a' dot (a:real^3)):real`]
 580 THEN MRESA1_TAC REAL_LT_INV`inv b *(a' dot (a:real^3)):real`
 581 THEN MRESA_TAC SEGMENT_FACE_OF[`p:real^3->bool`;`v:real^3`;`w:real^3`]
 582 THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`v:real^3`]
 583 THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`w:real^3`]
 584 THEN MP_TAC(SET_RULE`~(v IN interior p) /\ ~(w IN interior p) /\ (vec 0 IN interior p)==> DISJOINT{vec 0} {v,w:real^3}`)
 585 THEN RESA_TAC
 586 THEN SUBGOAL_THEN`a IN aff_gt {vec 0} {v,w:real^3}` ASSUME_TAC;
 587 ASM_MESON_TAC[];
 588 MRESA_TAC Planarity.scale_aff_gt_fan[`vec 0:real^3`;`v:real^3`;`w:real^3`]
 589 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`a:real^3`;`inv (inv b * (a' dot (a:real^3)))`][VECTOR_ARITH`a- vec 0= a /\ a+ vec 0=a`])
 590 THEN DISJ_CASES_TAC(SET_RULE`inv (inv b * (a' dot a)) % a IN relative_interior f \/ ~(inv (inv b * (a' dot a)) % a IN relative_interior (f:real^3->bool) )`);
 591 SUBGOAL_THEN `inv (inv b * (a' dot a)) % a IN fchanged (f:real^3->bool)`ASSUME_TAC;
 592 REWRITE_TAC[fchanged;IN_ELIM_THM]
 593 THEN EXISTS_TAC`inv (inv b * (a' dot a)) % a:real^3`
 594 THEN EXISTS_TAC `&1`
 595 THEN ASM_REWRITE_TAC[REAL_ARITH`&1> &0`;]
 596 THEN VECTOR_ARITH_TAC;
 597 MRESA1_TAC Polyhedron.FCHANGED_EQ_YFAN`p:real^3->bool`
 598 THEN SUBGOAL_THEN` fchanged f SUBSET yfan (vec 0,vertices p,edges (p:real^3->bool))`ASSUME_TAC;
 599 POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;UNIONS;IN_ELIM_THM;SUBSET])
 600 THEN REPEAT STRIP_TAC
 601 THEN EXISTS_TAC`fchanged f:real^3->bool`
 602 THEN ASM_REWRITE_TAC[]
 603 THEN EXISTS_TAC`f:real^3->bool`
 604 THEN ASM_REWRITE_TAC[];
 605 SUBGOAL_THEN `{v, w:real^3} IN edges p` ASSUME_TAC;
 606 ASM_REWRITE_TAC[IN_ELIM_THM;edges]
 607 THEN EXISTS_TAC`v:real^3`
 608 THEN EXISTS_TAC`w:real^3`
 609 THEN ASM_REWRITE_TAC[edge_of];
 610 MRESA_TAC Planarity.AFF_GE_SUBSET_XFAN[`vec 0:real^3`;`vertices p:real^3->bool`;`edges (p:real^3->bool)`;`v:real^3`;`w:real^3`]
 611 THEN MRESA_TAC AFF_GT_SUBSET_AFF_GE[`{vec 0:real^3}`;`{v,w:real^3}`]
 612 THEN MP_TAC(SET_RULE`aff_ge {vec 0} {v, w} SUBSET xfan (vec 0,vertices p,edges p)/\ aff_gt {vec 0} {v, w} SUBSET aff_ge {vec 0} {v, w}
 613 /\ inv (inv b * (a' dot a)) % a IN aff_gt {vec 0} {v, w}
 614 ==> inv (inv b * (a' dot a)) % a IN xfan (vec 0,vertices p,edges (p:real^3->bool))`)
 615 THEN RESA_TAC
 616 THEN MP_TAC(SET_RULE`inv (inv b * (a' dot a)) % a IN fchanged f
 617 /\ fchanged f SUBSET yfan (vec 0,vertices p,edges p)
 618 ==> inv (inv b * (a' dot a)) % a IN  yfan (vec 0,vertices p,edges (p:real^3->bool))`)
 619 THEN RESA_TAC
 620 THEN POP_ASSUM MP_TAC
 621 THEN ASM_REWRITE_TAC[yfan;IN_ELIM_THM; DIFF];
 622 POP_ASSUM MP_TAC
 623 THEN MRESA_TAC FACE_OF_POLYHEDRON_POLYHEDRON[`p:real^3->bool`;`f:real^3->bool`]
 624 THEN MRESA1_TAC RELATIVE_INTERIOR_OF_POLYHEDRON`f:real^3->bool`
 625 THEN ASM_REWRITE_TAC[DIFF;IN_ELIM_THM;DE_MORGAN_THM;UNIONS;]
 626 THEN STRIP_TAC
 627 THEN POP_ASSUM MP_TAC
 628 THEN SUBGOAL_THEN`?v w. {v,w} IN edges (p:real^3->bool) /\ u = segment[v,w]`ASSUME_TAC;
 629  FIND_ASSUM MP_TAC`u facet_of (f:real^3->bool)`
 630 THEN FIND_ASSUM MP_TAC`f facet_of (p:real^3->bool)`
 631 THEN REWRITE_TAC[facet_of]
 632 THEN ASM_REWRITE_TAC[edges;IN_ELIM_THM;edge_of]
 633 THEN MRESA_TAC Polyhedron.AFF_DIM_INTERIOR_EQ_3[`vec 0:real^3`;`p:real^3->bool`]
 634 THEN RESA_TAC
 635 THEN REWRITE_TAC[ARITH_RULE`&3 - &1- &1= &1:int`]
 636 THEN RESA_TAC
 637 THEN MRESA_TAC FACE_OF_TRANS[`u:real^3->bool`;`f:real^3->bool`;`p:real^3->bool`]
 638 THEN MRESA_TAC Polyhedron.EXPAND_EDGE_POLYTOPE[`u:real^3->bool`;`p:real^3->bool`]
 639 THEN ASM_REWRITE_TAC[]
 640 THEN EXISTS_TAC`a'':real^3`
 641 THEN EXISTS_TAC`b':real^3`
 642 THEN REWRITE_TAC[]
 643 THEN EXISTS_TAC`a'':real^3`
 644 THEN EXISTS_TAC`b':real^3`
 645 THEN ASM_REWRITE_TAC[]
 646 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);
 647 POP_ASSUM MP_TAC
 648 THEN STRIP_TAC
 649 THEN ASM_REWRITE_TAC[]
 650 THEN MRESA_TAC FACET_OF_IMP_FACE_OF[`u:real^3->bool`;`f:real^3->bool`]
 651 THEN MRESA_TAC FACE_OF_TRANS[`u:real^3->bool`;`f:real^3->bool`;`p:real^3->bool`]
 652 THEN SUBGOAL_THEN`segment [v',w'] SUBSET aff_ge {vec 0} {v',w':real^3}` ASSUME_TAC;
 653 MRESA_TAC SEGMENT_FACE_OF[`p:real^3->bool`;`v':real^3`;`w':real^3`]
 654 THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`v':real^3`]
 655 THEN MRESA_TAC EXTREME_POINT_NOT_IN_INTERIOR[`p:real^3->bool`;`w':real^3`]
 656 THEN MP_TAC(SET_RULE`~(v' IN interior p) /\ ~(w' IN interior p) /\ (vec 0 IN interior p)==> DISJOINT{vec 0} {v',w':real^3}`)
 657 THEN RESA_TAC
 658 THEN MRESAL_TAC Polyhedron.in_aff_ge_fan[`vec 0:real^3`;`v':real^3`;`w':real^3`]
 659 [segment;SUBSET;IN_ELIM_THM]
 660 THEN POP_ASSUM MP_TAC
 661 THEN DISCH_THEN(LABEL_TAC"THY")
 662 THEN REPEAT STRIP_TAC
 663 THEN REMOVE_THEN "THY"(fun th-> MRESA1_TAC th `u':real`);
 664  MRESA_TAC AFF_GT_SUBSET_AFF_GE[`{vec 0:real^3}`;`{v,w:real^3}`]
 665 THEN MP_TAC(SET_RULE` aff_gt {vec 0} {v, w} SUBSET aff_ge {vec 0} {v, w}
 666 /\ inv (inv b * (a' dot a)) % a IN aff_gt {vec 0} {v, w}
 667 ==> inv (inv b * (a' dot a)) % a IN aff_ge {vec 0} {v, w:real^3}`)
 668 THEN RESA_TAC
 669 THEN STRIP_TAC
 670 THEN MP_TAC(SET_RULE`  inv (inv b * (a' dot a)) % a IN segment[v',w']
 671 /\ segment[v',w'] SUBSET aff_ge {vec 0} {v', w'}
 672 /\ inv (inv b * (a' dot a)) % a IN aff_ge {vec 0} {v, w:real^3}
 673 ==> inv (inv b * (a' dot a)) % a IN aff_ge {vec 0} {v', w':real^3} INTER aff_ge {vec 0} {v,w}`)
 674 THEN RESA_TAC
 675 THEN POP_ASSUM MP_TAC
 676 THEN MRESAL_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`][FAN;fan7;UNION;IN_ELIM_THM]
 677 THEN POP_ASSUM(fun th-> MRESA_TAC th [`{v',w':real^3}`;`e:(real^3->bool)`])
 678 THEN MRESA1_TAC Polyhedron.POLYTOPE_FAN80`p:real^3->bool`
 679 THEN MRESA1_TAC Polyhedron.CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON`p:real^3->bool`
 680 THEN DISJ_CASES_TAC(SET_RULE`{v', w'} INTER {v, w:real^3} = {} \/ ~({v', w'} INTER {v, w} = {})`);
 681 MP_TAC(REAL_ARITH`&0 < inv (inv b * (a' dot (a:real^3)))==> ~(inv (inv b * (a' dot a))= &0)`)
 682 THEN RESA_TAC
 683 THEN ASM_REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING;VECTOR_MUL_EQ_0]
 684 THEN STRIP_TAC
 685 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;DOT_RZERO]);
 686 POP_ASSUM MP_TAC
 687 THEN REWRITE_TAC[SET_RULE`~(A={}) <=> ?v1. v1 IN A`]
 688 THEN STRIP_TAC
 689 THEN POP_ASSUM MP_TAC
 690 THEN REWRITE_TAC[ INTER;IN_ELIM_THM]
 691 THEN STRIP_TAC
 692 THEN POP_ASSUM MP_TAC
 693 THEN MP_TAC(SET_RULE`v1' IN {v',w':real^3} ==> v1'= v' \/ v1'= w'`)
 694 THEN RESA_TAC;
 695 STRIP_TAC
 696 THEN MP_TAC(SET_RULE`v' IN {v,w:real^3} ==> v'= v \/ v'= w`)
 697 THEN RESA_TAC;
 698 DISJ_CASES_TAC(SET_RULE`~(w'=w) \/ w'=w:real^3`);
 699 MP_TAC(SET_RULE`~(w'=w:real^3) ==>{x | x IN {v, w'} /\ x IN {v, w}}= {v}`)
 700 THEN RESA_TAC
 701 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
 702 THEN MRESA_TAC Conforming.properties12_fan7[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`]
 703 THEN MRESA_TAC properties_of_graph[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`w':real^3`;`v':real^3`]
 704 THEN MP_TAC(SET_RULE` e IN edges p /\ v IN vertices p
 705 /\ UNIONS {aff_gt {vec 0:real^3} e' | e' IN edges (p:real^3->bool)} INTER UNIONS {aff_ge {vec 0} {v} | v IN vertices p}= {} ==> aff_gt {vec 0:real^3} e INTER aff_ge {vec 0:real^3} {v}= {}`)
 706 THEN RESA_TAC
 707 THEN STRIP_TAC
 708 THEN MP_TAC(SET_RULE`inv (inv b * (a' dot a)) % a IN aff_gt {vec 0} {v, w}
 709 /\ inv (inv b * (a' dot a)) % a IN aff_ge {vec 0} {v}
 710 ==> ~(aff_gt {vec 0:real^3} {v,w} INTER aff_ge {vec 0:real^3} {v}= {})`)
 711 THEN RESA_TAC;
 712 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
 713 THEN POP_ASSUM MP_TAC
 714 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
 715 THEN ASM_REWRITE_TAC[];
 716 DISJ_CASES_TAC(SET_RULE`~(w'=v) \/ w'=v:real^3`);
 717 MP_TAC(SET_RULE`~(w'=v:real^3) ==>{x | x IN {w, w'} /\ x IN {v, w}}= {w}`)
 718 THEN RESA_TAC
 719 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
 720 THEN MRESA_TAC Conforming.properties12_fan7[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`]
 721 THEN MRESA_TAC properties_of_graph[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`w':real^3`;`v':real^3`]
 722 THEN POP_ASSUM MP_TAC
 723 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 724 THEN RESA_TAC
 725 THEN MP_TAC(SET_RULE` e IN edges p /\ w IN vertices p
 726 /\ UNIONS {aff_gt {vec 0:real^3} e' | e' IN edges (p:real^3->bool)} INTER UNIONS {aff_ge {vec 0} {v} | v IN vertices p}= {} ==> aff_gt {vec 0:real^3} e INTER aff_ge {vec 0:real^3} {w}= {}`)
 727 THEN RESA_TAC
 728 THEN STRIP_TAC
 729 THEN MP_TAC(SET_RULE`inv (inv b * (a' dot a)) % a IN aff_gt {vec 0} {v, w}
 730 /\ inv (inv b * (a' dot a)) % a IN aff_ge {vec 0} {w}
 731 ==> ~(aff_gt {vec 0:real^3} {v,w} INTER aff_ge {vec 0:real^3} {w}= {})`)
 732 THEN RESA_TAC;
 733 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
 734 THEN POP_ASSUM MP_TAC
 735 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
 736 THEN ONCE_REWRITE_TAC[SEGMENT_SYM]
 737 THEN ASM_REWRITE_TAC[];
 738 STRIP_TAC
 739 THEN MP_TAC(SET_RULE`w' IN {v,w:real^3} ==> w'= v \/ w'= w`)
 740 THEN RESA_TAC;
 741 DISJ_CASES_TAC(SET_RULE`~(v'=w) \/ v'=w:real^3`);
 742 MP_TAC(SET_RULE`~(v'=w:real^3) ==>{x | x IN {v', v} /\ x IN {v, w}}= {v}`)
 743 THEN RESA_TAC
 744 THEN MRESA_TAC Conforming.properties12_fan7[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`]
 745 THEN POP_ASSUM MP_TAC
 746 THEN POP_ASSUM MP_TAC
 747 THEN POP_ASSUM MP_TAC
 748 THEN POP_ASSUM MP_TAC
 749 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
 750 THEN MRESA_TAC properties_of_graph[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`v':real^3`;`w':real^3`]
 751 THEN POP_ASSUM MP_TAC
 752 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 753 THEN RESA_TAC
 754 THEN POP_ASSUM MP_TAC
 755 THEN DISCH_THEN(LABEL_TAC"THY")
 756 THEN REPEAT STRIP_TAC
 757 THEN REMOVE_THEN "THY" MP_TAC
 758 THEN RESA_TAC
 759 THEN MP_TAC(SET_RULE` e IN edges p /\ v IN vertices p
 760 /\ UNIONS {aff_gt {vec 0:real^3} e' | e' IN edges (p:real^3->bool)} INTER UNIONS {aff_ge {vec 0} {v} | v IN vertices p}= {} ==> aff_gt {vec 0:real^3} e INTER aff_ge {vec 0:real^3} {v}= {}`)
 761 THEN RESA_TAC
 762 THEN MP_TAC(SET_RULE`inv (inv b * (a' dot a)) % a IN aff_gt {vec 0} {v, w}
 763 /\ inv (inv b * (a' dot a)) % a IN aff_ge {vec 0} {v}
 764 ==> ~(aff_gt {vec 0:real^3} {v,w} INTER aff_ge {vec 0:real^3} {v}= {})`)
 765 THEN RESA_TAC;
 766 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
 767 THEN POP_ASSUM MP_TAC
 768 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
 769 THEN ONCE_REWRITE_TAC[SEGMENT_SYM]
 770 THEN ASM_REWRITE_TAC[];
 771 DISJ_CASES_TAC(SET_RULE`~(v'=v) \/ v'=v:real^3`);
 772 MP_TAC(SET_RULE`~(v'=v:real^3) ==>{x | x IN {v', w} /\ x IN {v, w}}= {w}`)
 773 THEN RESA_TAC
 774 THEN MRESA_TAC Conforming.properties12_fan7[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`]
 775 THEN POP_ASSUM MP_TAC
 776 THEN POP_ASSUM MP_TAC
 777 THEN POP_ASSUM MP_TAC
 778 THEN POP_ASSUM MP_TAC
 779 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
 780 THEN MRESA_TAC properties_of_graph[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`v':real^3`;`w':real^3`]
 781 THEN POP_ASSUM MP_TAC
 782 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 783 THEN RESA_TAC
 784 THEN POP_ASSUM MP_TAC
 785 THEN DISCH_THEN(LABEL_TAC"THY")
 786 THEN REPEAT STRIP_TAC
 787 THEN REMOVE_THEN "THY" MP_TAC
 788 THEN RESA_TAC
 789 THEN MP_TAC(SET_RULE` e IN edges p /\ w IN vertices p
 790 /\ UNIONS {aff_gt {vec 0:real^3} e' | e' IN edges (p:real^3->bool)} INTER UNIONS {aff_ge {vec 0} {v} | v IN vertices p}= {} ==> aff_gt {vec 0:real^3} e INTER aff_ge {vec 0:real^3} {w}= {}`)
 791 THEN RESA_TAC
 792 THEN MP_TAC(SET_RULE`inv (inv b * (a' dot a)) % a IN aff_gt {vec 0} {v, w}
 793 /\ inv (inv b * (a' dot a)) % a IN aff_ge {vec 0} {w}
 794 ==> ~(aff_gt {vec 0:real^3} {v,w} INTER aff_ge {vec 0:real^3} {w}= {})`)
 795 THEN RESA_TAC;
 796 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
 797 THEN POP_ASSUM MP_TAC
 798 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
 799 THEN ASM_REWRITE_TAC[]]);;
 800
 801
 802
 803
 804
 805
 806 let CONVEX_OPEN_AFF_GT_FACE=prove(`FAN(x,V,E)
 807 /\ (!v. v IN V ==> CARD (set_of_edge v V E) > 1)
 808 /\ fan80(x,V,E)
 809 /\ f IN face_set (hypermap1_of_fanx (x,V,E))
 810 ==> (!s. s IN {aff_gt {x, pr2 y, pr3 y} {pr3 (f1_fan x V E y)} | y IN (f:real^3#real^3#real^3#real^3->bool)} ==> convex s /\ open s)`,
 811
 812 REWRITE_TAC[IN_ELIM_THM]
 813 THEN REPEAT STRIP_TAC
 814 THENL[
 815 ASM_REWRITE_TAC[CONVEX_AFF_GT];
 816 MRESA_TAC fully_surrounded_imp_aff_gt_3_1_of_dart_eq_fan[`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`f:real^3#real^3#real^3#real^3->bool`;`y:real^3#real^3#real^3#real^3`]
 817 THEN MATCH_MP_TAC OPEN_AFF_GT_3_1
 818 THEN MRESA_TAC properties_of_elements_in_face_fully_surroundedfan[`x:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`f:real^3#real^3#real^3#real^3->bool`; `y:real^3#real^3#real^3#real^3`]
 819 THEN FIND_ASSUM MP_TAC `fan80(x:real^3,V,E)`
 820 THEN REWRITE_TAC[fan80]
 821 THEN DISCH_TAC
 822 THEN POP_ASSUM (fun th -> MRESA_TAC th [`(pr2 y):real^3`;`(pr3 y):real^3`] )
 823 THEN MRESA_TAC sigma_fan_in_set_of_edge[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`(pr2 y):real^3`;`(pr3 y):real^3`]
 824 THEN POP_ASSUM MP_TAC
 825 THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`(pr2 y):real^3`;`(pr3 y):real^3`]
 826 THEN DISCH_TAC
 827 THEN MRESA_TAC properties_of_set_of_edge_fan [`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`(pr2 y):real^3`;`(sigma_fan x V E (pr2 y) (pr3 y)):real^3`]
 828 THEN MRESA_TAC properties_fully_surrounded [`x:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`(sigma_fan x V E (pr2 y) (pr3 y)):real^3`;`(pr2 y):real^3`;`(pr3 y):real^3`;]
 829 THEN POP_ASSUM MP_TAC
 830 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
 831 THEN RESA_TAC
 832 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
 833 THEN ASM_REWRITE_TAC[]]);;
 834
 835
 836 let AFF_GE_3_1 = prove
 837  (`!x v u w.
 838         DISJOINT {x,v,u} {w}
 839         ==> aff_ge {x,v,u} {w} =
 840              {y | ?t1 t2 t3 t4.
 841                      &0 <= t4 /\
 842                      t1 + t2 +t3 +t4 = &1 /\
 843                      y = t1 % x + t2 % v + t3 % u +t4 % w }`,
 844   AFF_TAC);;
 845
 846
 847 let inter_aff_ge_3_1_is_aff_ge_1_3=prove(`!x v u w:real^3.
 848 ~coplanar {x,v,u,w}
 849 ==>
 850 aff_ge {x,v,u} {w} INTER aff_ge {x,u,w} {v} INTER aff_ge {x,w,v} {u}=aff_ge {x} {v,u,w}`,
 851 GEOM_ORIGIN_TAC `x:real^3`
 852 THEN REPEAT STRIP_TAC
 853 THEN MRESA_TAC notcoplanar_disjoints[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 854 THEN MRESA_TAC notcoplanar_disjoint[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 855 THEN MRESA_TAC AFF_GE_3_1[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 856 THEN MRESA_TAC AFF_GE_3_1[`(vec 0):real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
 857 THEN MRESA_TAC AFF_GE_3_1[`(vec 0):real^3`;`w:real^3`;`v:real^3`;`u:real^3`]
 858 THEN MRESA_TAC AFF_GE_1_3[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 859 THEN MRESA_TAC NOT_COPLANAR_0_4_IMP_INDEPENDENT[`v:real^3`;`u:real^3`;`w:real^3`]
 860 THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;INTER]
 861 THEN REDUCE_VECTOR_TAC
 862 THEN GEN_TAC
 863 THEN EQ_TAC
 864 THENL[
 865 STRIP_TAC
 866 THEN POP_ASSUM MP_TAC
 867 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t2 % v + t3 % u + t4 % w = t2'' % w + t3'' % v + t4'' % u <=> (t2-t3'') % v + (t3-t4'') % u + (t4-t2'') % w= vec 0`]
 868 THEN STRIP_TAC
 869 THEN MRESAL_TAC INDEPENDENT_3[`v:real^3`;`u:real^3`;`w:real^3`;`t2-t3'':real`; `t3-t4'':real`; `t4 -t2'':real`][REAL_ARITH`A-B= &0<=> A=B`]
 870 THEN POP_ASSUM MP_TAC
 871 THEN POP_ASSUM MP_TAC
 872 THEN POP_ASSUM MP_TAC
 873 THEN REMOVE_ASSUM_TAC
 874 THEN POP_ASSUM MP_TAC
 875 THEN POP_ASSUM MP_TAC
 876 THEN POP_ASSUM MP_TAC
 877 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t2 % v + t3 % u + t4 % w = t2' % u + t3' % w + t4' % v <=> (t2-t4') % v + (t3-t2') % u + (t4-t3') % w= vec 0`]
 878 THEN STRIP_TAC
 879 THEN MRESAL_TAC INDEPENDENT_3[`v:real^3`;`u:real^3`;`w:real^3`;`t2-t4':real`; `t3-t2':real`; `t4 -t3':real`][REAL_ARITH`A-B= &0<=> A=B`]
 880 THEN REPEAT STRIP_TAC
 881 THEN EXISTS_TAC`t1'':real`
 882 THEN EXISTS_TAC`t3'':real`
 883 THEN EXISTS_TAC`t4'':real`
 884 THEN EXISTS_TAC`t2'':real`
 885 THEN ASM_REWRITE_TAC[REAL_ARITH`t1+t2+t3+t4=t1+t4+t2+t3:real`]
 886 THEN ASM_TAC
 887 THEN REAL_ARITH_TAC;
 888
 889 STRIP_TAC
 890 THEN STRIP_TAC
 891 THENL[EXISTS_TAC`t1:real`
 892 THEN EXISTS_TAC`t2:real`
 893 THEN EXISTS_TAC`t3:real`
 894 THEN EXISTS_TAC`t4:real`
 895 THEN ASM_REWRITE_TAC[];
 896
 897 STRIP_TAC
 898 THENL[
 899 EXISTS_TAC`t1:real`
 900 THEN EXISTS_TAC`t3:real`
 901 THEN EXISTS_TAC`t4:real`
 902 THEN EXISTS_TAC`t2:real`
 903 THEN ASM_REWRITE_TAC[REAL_ARITH`t1  + t3 + t4+ t2:real=t1 + t2 + t3 + t4`]
 904 THEN VECTOR_ARITH_TAC;
 905 EXISTS_TAC`t1:real`
 906 THEN EXISTS_TAC`t4:real`
 907 THEN EXISTS_TAC`t2:real`
 908 THEN EXISTS_TAC`t3:real`
 909 THEN ASM_REWRITE_TAC[REAL_ARITH`t1  + t4+ t2+ t3:real=t1 + t2 + t3 + t4`]
 910 THEN VECTOR_ARITH_TAC]]]);;
 911
 912
 913 let CLOSURE_AFF_GT_3_1_EQ_AFF_GE_3_1=prove_by_refinement(`!x v u w:real^3. ~coplanar {x, v, u, w} ==>
 914 closure (aff_gt {x,v, u}  {w}) = aff_ge {x, v, u} {w}`,
 915 [GEOM_ORIGIN_TAC `x:real^3`
 916 THEN REPEAT STRIP_TAC
 917 THEN MRESA_TAC notcoplanar_disjoints[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 918 THEN MRESAL_TAC Planarity.coplanar_cross_dot[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`][VECTOR_ARITH`A- vec 0=A`]
 919 THEN MP_TAC(REAL_ARITH`~((v cross u) dot w = &0) ==> &0 < (v cross u) dot w \/ &0 < --((v cross u) dot (w:real^3))`)
 920 THEN RESA_TAC;
 921 MRESAL_TAC Planarity.aff_gt_3_1_rep_cross_dot[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`][VECTOR_ARITH`A- vec 0=A`]
 922 THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`][VECTOR_ARITH`A- vec 0=A`]
 923 THEN DISJ_CASES_TAC (SET_RULE` v cross u = vec 0 \/ ~(v cross (u:real^3) = vec 0)`);
 924 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th; DOT_LZERO]);
 925 REWRITE_TAC[REAL_ARITH`&0 < A <=> (-- A) < &0`;REAL_ARITH`&0 <= A <=> (-- A) <= &0`;GSYM DOT_LNEG]
 926 THEN MATCH_MP_TAC CLOSURE_HALFSPACE_LT
 927 THEN ASM_REWRITE_TAC[VECTOR_ARITH`-- A=  vec 0<=> A= vec 0:real^3`];
 928 POP_ASSUM MP_TAC
 929 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
 930 THEN REWRITE_TAC[DOT_LNEG; REAL_ARITH`-- (-- A)=A`]
 931 THEN STRIP_TAC
 932 THEN MRESAL_TAC Planarity.aff_gt_3_1_rep_cross_dot[`(vec 0):real^3`;`u:real^3`;`v:real^3`;`w:real^3`][VECTOR_ARITH`A- vec 0=A`]
 933 THEN POP_ASSUM MP_TAC
 934 THEN ONCE_REWRITE_TAC[SET_RULE`{X, u, v, w}= {X, v, u, w}`]
 935 THEN RESA_TAC
 936 THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot[`(vec 0):real^3`;`u:real^3`;`v:real^3`;`w:real^3`][VECTOR_ARITH`A- vec 0=A`]
 937 THEN POP_ASSUM MP_TAC
 938 THEN ONCE_REWRITE_TAC[SET_RULE`{X, u, v, w}= {X, v, u, w}`]
 939 THEN RESA_TAC
 940 THEN DISJ_CASES_TAC (SET_RULE` u cross v = vec 0 \/ ~(u cross (v:real^3) = vec 0)`);
 941 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th; DOT_LZERO])
 942 THEN REAL_ARITH_TAC;
 943 ONCE_REWRITE_TAC[SET_RULE`{X, u, v}= {X, v, u}`]
 944 THEN ASM_REWRITE_TAC[]
 945 THEN REWRITE_TAC[REAL_ARITH`&0 < A <=> (-- A) < &0`;REAL_ARITH`&0 <= A <=> (-- A) <= &0`;GSYM DOT_LNEG]
 946 THEN MATCH_MP_TAC CLOSURE_HALFSPACE_LT
 947 THEN ASM_REWRITE_TAC[VECTOR_ARITH`-- A=  vec 0<=> A= vec 0:real^3`]]);;
 948
 949 let CLOSURE_AFF_GT_1_3_EQ_AFF_GE_1_3= prove(`!x v u w:real^3. ~coplanar {x, v, u, w} ==>
 950 closure (aff_gt {x} {v, u, w}) = aff_ge {x} {v, u, w}`,
 951 REPEAT STRIP_TAC
 952 THEN MRESA_TAC inter_aff_ge_3_1_is_aff_ge_1_3[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 953 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 954 THEN MRESA_TAC OPEN_AFF_GT_3_1[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 955 THEN MRESA_TAC OPEN_AFF_GT_3_1[`x:real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
 956 THEN POP_ASSUM MP_TAC
 957 THEN ONCE_REWRITE_TAC[SET_RULE`{x, u, w, v}={x, v,u, w}`]
 958 THEN RESA_TAC
 959 THEN MRESA_TAC OPEN_AFF_GT_3_1[`x:real^3`;`w:real^3`;`v:real^3`;`u:real^3`]
 960 THEN POP_ASSUM MP_TAC
 961 THEN ONCE_REWRITE_TAC[SET_RULE`{x, w, v, u}={x, v,u, w}`]
 962 THEN RESA_TAC
 963 THEN MRESA_TAC CONVEX_AFF_GT[`{x,v,u:real^3}`;`{w:real^3}`]
 964 THEN MRESA_TAC CONVEX_AFF_GT[`{x,u:real^3,w}`;`{v:real^3}`]
 965 THEN MRESA_TAC CONVEX_AFF_GT[`{x,w,v:real^3}`;`{u:real^3}`]
 966 THEN MRESA_TAC Planarity.notcoplanar_4point_aff_gt_1_3_not_empty[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 967 THEN POP_ASSUM MP_TAC
 968 THEN MRESA_TAC Planarity.inter_aff_gt_3_1_is_aff_gt_1_3[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 969 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 970 THEN STRIP_TAC
 971 THEN MP_TAC(SET_RULE`~(aff_gt {x, v, u} {w} INTER aff_gt {x, u, w} {v} INTER aff_gt {x, w, v} {u} =
 972    {})
 973 ==> ~(aff_gt {x, v, u} {w} INTER aff_gt {x, u, w} {v:real^3} =
 974    {})`)
 975 THEN RESA_TAC
 976 THEN MRESA_TAC CLOSURE_INTER_CONVEX_OPEN[`aff_gt {x, v, u} {w:real^3}`;`aff_gt {x, u, w} {v:real^3}`]
 977 THEN MRESA_TAC OPEN_INTER[`aff_gt {x, v, u} {w:real^3}`;`aff_gt {x, u, w} {v:real^3}`]
 978 THEN MRESA_TAC CONVEX_INTER[`aff_gt {x, v, u} {w:real^3}`;`aff_gt {x, u, w} {v:real^3}`]
 979 THEN MRESAL_TAC CLOSURE_INTER_CONVEX_OPEN[`aff_gt {x, v, u} {w:real^3} INTER aff_gt {x, u, w} {v:real^3}`;`aff_gt {x, w, v} {u:real^3}`][SET_RULE`(A INTER B) INTER C= A INTER B INTER C`]
 980 THEN MRESA_TAC CLOSURE_AFF_GT_3_1_EQ_AFF_GE_3_1[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 981 THEN MRESA_TAC CLOSURE_AFF_GT_3_1_EQ_AFF_GE_3_1[`x:real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
 982 THEN POP_ASSUM MP_TAC
 983 THEN ONCE_REWRITE_TAC[SET_RULE`{x, u, w, v}={x, v,u, w}`]
 984 THEN RESA_TAC
 985 THEN MRESA_TAC CLOSURE_AFF_GT_3_1_EQ_AFF_GE_3_1[`x:real^3`;`w:real^3`;`v:real^3`;`u:real^3`]
 986 THEN POP_ASSUM MP_TAC
 987 THEN ONCE_REWRITE_TAC[SET_RULE`{x, w, v,u}={x, v,u, w}`]
 988 THEN RESA_TAC);;
 989
 990
 991 let AFF_GT_SUBSET_CLOSURE_DARTSET_LEADS_INTO_FAN=prove(`FAN(x,V,E)
 992 /\ (!v. v IN V ==> CARD (set_of_edge v V E) > 1)
 993 /\ fan80(x,V,E)
 994 /\ f IN face_set (hypermap1_of_fanx (x,V,E))
 995 /\ e IN f
 996 ==>  aff_gt {x} {(pr2 e), pr3 e } SUBSET closure(dartset_leads_into_fan x V E f)`,
 997
 998 REPEAT STRIP_TAC
 999 THEN MRESAL_TAC properties_of_elements_in_face_fully_surroundedfan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`f:real^3#real^3#real^3#real^3->bool`;`e:real^3#real^3#real^3#real^3`][edges;IN_ELIM_THM]
1000 THEN ABBREV_TAC`v=pr2 (e:real^3#real^3#real^3#real^3)`
1001 THEN ABBREV_TAC`w=pr3 (e:real^3#real^3#real^3#real^3)`
1002 THEN ABBREV_TAC`u=sigma_fan x V E v (w:real^3)`
1003 THEN MRESA_TAC remark1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`w:real^3`;`v:real^3`]
1004 THEN MRESA_TAC Fan.sigma_fan_in_set_of_edge[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`]
1005 THEN MRESA_TAC remark1_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`u:real^3`;`v:real^3`]
1006 THEN REMOVE_ASSUM_TAC
1007 THEN POP_ASSUM MP_TAC
1008 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1009 THEN STRIP_TAC
1010 THEN MRESA_TAC aff_gt_1_3_subset_dart_leads_into_fan[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`u:real^3`;`v:real^3`;`w:real^3`]
1011 THEN MRESA_TAC SUBSET_CLOSURE[`aff_gt {x} {u, v, w:real^3}`;`dart_leads_into x V E v (w:real^3)`]
1012 THEN MRESA_TAC Planarity.DARTSET_LEADS_INTO_FAN[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`f:real^3#real^3#real^3#real^3->bool`]
1013 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(e:real^3#real^3#real^3#real^3)`)
1014 THEN REMOVE_ASSUM_TAC
1015 THEN POP_ASSUM MP_TAC
1016 THEN FIND_ASSUM MP_TAC`fan80(x:real^3,V,E)`
1017 THEN REWRITE_TAC[fan80]
1018 THEN STRIP_TAC
1019 THEN POP_ASSUM(fun th-> MRESA_TAC th[`v:real^3`;`w:real^3`])
1020 THEN MRESA_TAC Planarity.properties_fully_surrounded[`x:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`u:real^3`;`v:real^3`;`w:real^3`]
1021 THEN MRESA_TAC CLOSURE_AFF_GT_1_3_EQ_AFF_GE_1_3[`x:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
1022 THEN MRESA_TAC Planarity.aff_ge_1_3_eq_unions_aff_ge_1_2_and_aff_gt_1_3[`x:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
1023 THEN STRIP_TAC
1024 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1025 THEN MRESA_TAC AFF_GT_SUBSET_AFF_GE[`{x:real^3}`;`{v,w:real^3}`]
1026 THEN POP_ASSUM MP_TAC
1027 THEN POP_ASSUM MP_TAC
1028 THEN SET_TAC[]);;
1029
1030
1031
1032
1033 let IN_EDGES0_FAN=prove(`!p:real^3->bool f f1.
1034  bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p
1035 /\ f IN face_set (hypermap1_of_fanx  (vec 0,vertices p,edges p))
1036 /\ f1 facet_of p /\                                                      dartset_leads_into_fan (vec 0) (vertices p) (edges p) f = fchanged f1
1037 /\ e IN f
1038 ==> {pr2 e, pr3 e} IN EDGES0_FAN p f1`,
1039 REPEAT STRIP_TAC
1040 THEN REWRITE_TAC[EDGES0_FAN;IN_ELIM_THM;edges]
1041 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
1042 THEN MRESA1_TAC Polyhedron.POLYTOPE_FAN80`p:real^3->bool`
1043 THEN MRESA1_TAC Polyhedron.CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON`p:real^3->bool`
1044 THEN MRESA_TAC properties_of_elements_in_face_fully_surroundedfan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`f:real^3#real^3#real^3#real^3->bool`;`e:real^3#real^3#real^3#real^3`]
1045 THEN POP_ASSUM(fun th-> MP_TAC th THEN REWRITE_TAC[edges;IN_ELIM_THM]
1046 THEN STRIP_TAC THEN MP_TAC th THEN ASM_REWRITE_TAC[] THEN STRIP_TAC)
1047 THEN STRIP_TAC
1048 THENL[
1049 EXISTS_TAC`v:real^3`
1050 THEN EXISTS_TAC`w:real^3`
1051 THEN ASM_REWRITE_TAC[];
1052 MRESA_TAC (GEN_ALL AFF_GT_SUBSET_CLOSURE_DARTSET_LEADS_INTO_FAN)[`e:real^3#real^3#real^3#real^3`;`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`f:real^3#real^3#real^3#real^3->bool`]
1053 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`w:real^3`;`v:real^3`]
1054 THEN MRESA_TAC Planarity.exists_in_aff_gt_disjoint[`vec 0:real^3`;`v:real^3`;`w:real^3`]
1055 THEN REWRITE_TAC[SET_RULE`~(A= {})<=> ?a. a IN A`]
1056 THEN EXISTS_TAC`y:real^3`
1057 THEN ASM_TAC
1058 THEN SET_TAC[]]);;
1059
1060
1061 let SUBSET_EDGES0_FAN=prove(`!p:real^3->bool f f1.
1062  bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p
1063 /\ f IN face_set (hypermap1_of_fanx  (vec 0,vertices p,edges p))
1064 /\ f1 facet_of p /\                                                      dartset_leads_into_fan (vec 0) (vertices p) (edges p) f = fchanged f1
1065 ==> {{pr2 e, pr3 e}|  e IN f} SUBSET  EDGES0_FAN p f1`,
1066  REWRITE_TAC[SUBSET;IN_ELIM_THM]
1067 THEN REPEAT STRIP_TAC
1068 THEN ASM_REWRITE_TAC[]
1069 THEN ASM_MESON_TAC[IN_EDGES0_FAN]);;
1070
1071
1072
1073
1074 let EDGES0_SUBSET_FAN=prove_by_refinement(`!p:real^3->bool f f1.
1075  bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p
1076 /\ f IN face_set (hypermap1_of_fanx  (vec 0,vertices p,edges p))
1077 /\ f1 facet_of p /\
1078  fchanged f1 =dartset_leads_into_fan (vec 0) (vertices p) (edges p) f
1079 ==>   EDGES0_FAN p f1 SUBSET {{pr2 e, pr3 e}|  e IN f} `,
1080 [REPEAT STRIP_TAC
1081 THEN  REWRITE_TAC[SUBSET;EDGES0_FAN;IN_ELIM_THM]
1082 THEN REPEAT STRIP_TAC
1083 THEN POP_ASSUM MP_TAC
1084 THEN POP_ASSUM (fun th-> MP_TAC th THEN REWRITE_TAC[edges;IN_ELIM_THM] THEN STRIP_TAC THEN MP_TAC th THEN RESA_TAC)
1085 THEN ASM_REWRITE_TAC[SET_RULE`~(A={}) <=> ?a. a IN A`;INTER;IN_ELIM_THM]
1086 THEN RESA_TAC
1087 THEN POP_ASSUM MP_TAC
1088 THEN DISCH_THEN(LABEL_TAC "THYGIANG1")
1089 THEN ABBREV_TAC`x1= (vec 0:real^3)`
1090 THEN ABBREV_TAC`V=(vertices (p:real^3->bool)) `
1091 THEN ABBREV_TAC`E=(edges (p:real^3->bool))`
1092 THEN ABBREV_TAC`u=inverse1_sigma_fan (x1:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (v:real^3) (w:real^3)`
1093 THEN ABBREV_TAC`U= dartset_leads_into_fan x1 V E f`
1094 THEN MRESA_TAC POLYHEDRON_FAN[`p:real^3->bool`;`vec 0:real^3`]
1095 THEN MRESA1_TAC Polyhedron.POLYTOPE_FAN80`p:real^3->bool`
1096 THEN MRESA1_TAC Polyhedron.CARD_SET_OF_EDGE_INEQ_1_POLYHEDRON`p:real^3->bool`
1097 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`w:real^3`;`v:real^3`]
1098 THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x1:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`]
1099 THEN REMOVE_ASSUM_TAC
1100 THEN POP_ASSUM (fun th-> POP_ASSUM (fun th-> MRESA1_TAC th `w:real^3`) THEN MRESA1_TAC th `w:real^3`)
1101 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`u:real^3`;`v:real^3`]
1102 THEN REMOVE_ASSUM_TAC
1103 THEN POP_ASSUM MP_TAC
1104 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1105 THEN STRIP_TAC
1106 THEN MRESA_TAC dartset_leads_into_is_topological_component_yfan[`x1:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`f:real^3#real^3#real^3#real^3->bool`]
1107 THEN MRESA_TAC exists_point_in_component_yfan[`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)` ;`U:real^3->bool`]
1108 THEN POP_ASSUM MP_TAC
1109 THEN DISCH_THEN(LABEL_TAC "THYGIANG")
1110 THEN SUBGOAL_THEN`a IN xfan (x1:real^3,(V:real^3->bool),E)`ASSUME_TAC;
1111 REWRITE_TAC[xfan;IN_ELIM_THM]
1112 THEN EXISTS_TAC`{v,w:real^3}`
1113 THEN MRESA_TAC AFF_GT_SUBSET_AFF_GE[`{x1:real^3}`;`{v,w:real^3}`]
1114 THEN ASM_TAC
1115 THEN SET_TAC[IN];
1116 MRESA_TAC Planarity.origin_is_not_aff_gt_fan[`x1:real^3`;`v:real^3`;`w:real^3`]
1117 THEN MP_TAC(SET_RULE`~(x1 IN aff_gt {x1} {v, w}) /\ (a IN aff_gt {x1} {v, w}) ==> ~(a= x1:real^3)`)
1118 THEN RESA_TAC
1119 THEN MRESA_TAC Planarity.topological_component_subset_yfan[`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:(real^3->bool)`]
1120 THEN SUBGOAL_THEN`~(a IN U:real^3->bool)` ASSUME_TAC;
1121 POP_ASSUM MP_TAC
1122 THEN REWRITE_TAC[yfan]
1123 THEN ASM_TAC
1124 THEN SET_TAC[];
1125 DISJ_CASES_TAC(SET_RULE`~(!t. &0 < t /\ t < &1 ==> (&1 - t) % a + t % z IN (U:real^3->bool)) \/ (!t. &0 < t /\ t < &1 ==> (&1 - t) % a + t % z IN (U:real^3->bool))`);
1126 POP_ASSUM MP_TAC
1127 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP]
1128 THEN STRIP_TAC
1129 THEN POP_ASSUM MP_TAC
1130 THEN DISCH_THEN(LABEL_TAC"THY")
1131 THEN MRESA_TAC PIIJBJK[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;]
1132 THEN MRESA_TAC GINGUAP[`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`f:(real^3#real^3#real^3#real^3->bool)`]
1133 THEN MRESA1_TAC CLOSURE_SUBSET`U:real^3->bool`
1134 THEN MP_TAC(SET_RULE`z IN U/\ U SUBSET closure U ==> z IN closure (U:real^3->bool)`)
1135 THEN RESA_TAC
1136 THEN MRESAL1_TAC CONVEX_CLOSURE`U:real^3->bool`[CONVEX_CONTAINS_SEGMENT]
1137 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`a:real^3`;`z:real^3`][segment;SUBSET;IN_ELIM_THM])
1138 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(&1 - t) % a + t % z:real^3`)
1139 THEN POP_ASSUM MP_TAC
1140 THEN SUBGOAL_THEN`(?u. (&0 <= u /\ u <= &1) /\
1141            (&1 - t) % a + t % z = (&1 - u) % a + u % z:real^3)` ASSUME_TAC;
1142 EXISTS_TAC`t:real`
1143 THEN ASM_REWRITE_TAC[]
1144 THEN ASM_TAC
1145 THEN REAL_ARITH_TAC;
1146 ASM_REWRITE_TAC[]
1147 THEN DISCH_THEN(LABEL_TAC"THY1")
1148 THEN FIND_ASSUM MP_TAC`conforming_fan (x1:real^3,V,E)`
1149 THEN REWRITE_TAC[conforming_fan;conforming_half_space_fan]
1150 THEN STRIP_TAC
1151 THEN REMOVE_ASSUM_TAC
1152 THEN REMOVE_ASSUM_TAC
1153 THEN POP_ASSUM(fun th-> MRESA1_TAC th`f:(real^3#real^3#real^3#real^3->bool)`)
1154 THEN MP_TAC( ISPECL [`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`f:(real^3#real^3#real^3#real^3->bool)`]
1155 Conforming.exists_point_in_dartset_leads_into_fan)
1156 THEN ONCE_REWRITE_TAC[SET_RULE`(?a. a IN A) <=> ~(A={})`]
1157 THEN ASM_REWRITE_TAC[]
1158 THEN STRIP_TAC
1159 THEN MRESA_TAC (GEN_ALL CONVEX_OPEN_AFF_GT_FACE)[`f:(real^3#real^3#real^3#real^3->bool)`;`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`]
1160 THEN MRESA1_TAC CLOSURE_INTERS_CONVEX_OPEN`{aff_gt {x1, pr2 y, pr3 y} {pr3 (f1_fan x1 V E y)} | y IN (f:(real^3#real^3#real^3#real^3->bool))}`
1161 THEN REMOVE_THEN "THY" MP_TAC
1162 THEN ASM_REWRITE_TAC[INTERS;IN_ELIM_THM;NOT_FORALL_THM;NOT_IMP]
1163 THEN STRIP_TAC
1164 THEN POP_ASSUM MP_TAC
1165 THEN ASM_REWRITE_TAC[]
1166 THEN REMOVE_ASSUM_TAC
1167 THEN REMOVE_THEN "THY1" MP_TAC
1168 THEN ASM_REWRITE_TAC[]
1169 THEN REWRITE_TAC[INTERS;IN_ELIM_THM;NOT_FORALL_THM;NOT_IMP;]
1170 THEN SUBGOAL_THEN`closure (aff_gt {x1, pr2 y, pr3 y} {pr3 (f1_fan x1 V E y)}) IN
1171       IMAGE closure
1172       {aff_gt {x1, pr2 y, pr3 y} {pr3 (f1_fan x1 V E y)} | y IN (f:(real^3#real^3#real^3#real^3->bool))}`ASSUME_TAC;
1173 REWRITE_TAC[IMAGE;IN_ELIM_THM]
1174 THEN EXISTS_TAC`aff_gt {x1:real^3, pr2 y, pr3 y} {pr3 (f1_fan x1 V E y)}`
1175 THEN ASM_REWRITE_TAC[]
1176 THEN EXISTS_TAC`y:real^3#real^3#real^3#real^3`
1177 THEN ASM_REWRITE_TAC[];
1178 STRIP_TAC
1179 THEN POP_ASSUM(fun th-> MRESA1_TAC th`closure (aff_gt {x1, pr2 y, pr3 y} {pr3 (f1_fan x1 V E y)})`)
1180 THEN POP_ASSUM MP_TAC
1181 THEN MRESA_TAC Conforming.fully_surrounded_imp_aff_gt_3_1_of_dart_eq_fan
1182 [`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`f:(real^3#real^3#real^3#real^3->bool)`;`y:real^3#real^3#real^3#real^3`]
1183 THEN MRESA_TAC properties_of_elements_in_face_fully_surroundedfan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`f:real^3#real^3#real^3#real^3->bool`;`y:real^3#real^3#real^3#real^3`]
1184 THEN REMOVE_THEN"THYGIANG" MP_TAC
1185 THEN ASM_REWRITE_TAC[INTERS;IN_ELIM_THM]
1186 THEN SUBGOAL_THEN`(?y'. y' IN f /\
1187             aff_gt {x1:real^3, pr2 y, pr3 y} {sigma_fan x1 V E (pr2 y) (pr3 y)} =
1188             aff_gt {x1, pr2 y', pr3 y'} {pr3 (f1_fan x1 V E y')})
1189 ` ASSUME_TAC;
1190 EXISTS_TAC`y:real^3#real^3#real^3#real^3`
1191 THEN ASM_REWRITE_TAC[];
1192 STRIP_TAC
1193 THEN POP_ASSUM(fun th-> MRESA1_TAC th `aff_gt {x1:real^3, pr2 y, pr3 y} {pr3 (f1_fan x1 V E y)}`)
1194 THEN POP_ASSUM MP_TAC
1195 THEN REMOVE_THEN"THYGIANG1" MP_TAC
1196 THEN ASM_REWRITE_TAC[]
1197 THEN REWRITE_TAC[INTERS;IN_ELIM_THM;NOT_FORALL_THM;NOT_IMP;]
1198 THEN STRIP_TAC
1199 THEN POP_ASSUM(fun th-> MRESA1_TAC th`closure (aff_gt {x1, pr2 y, pr3 y} {pr3 (f1_fan x1 V E y)})`)
1200 THEN POP_ASSUM MP_TAC
1201 THEN ABBREV_TAC`v1=pr2 (y:real^3#real^3#real^3#real^3)`
1202 THEN ABBREV_TAC`w1=pr3 (y:real^3#real^3#real^3#real^3)`
1203 THEN ABBREV_TAC`u1=sigma_fan x1 V E v1 (w1:real^3)`
1204 THEN MRESA_TAC remark1_fan[`x1:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`w1:real^3`;`v1:real^3`]
1205 THEN MRESA_TAC Fan.sigma_fan_in_set_of_edge[`x1:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`v1:real^3`;`w1:real^3`]
1206 THEN MRESA_TAC remark1_fan[`x1:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`u1:real^3`;`v1:real^3`]
1207 THEN REMOVE_ASSUM_TAC
1208 THEN POP_ASSUM MP_TAC
1209 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1210 THEN STRIP_TAC
1211 THEN FIND_ASSUM MP_TAC`fan80(x1:real^3,V,E)`
1212 THEN REWRITE_TAC[fan80]
1213 THEN STRIP_TAC
1214 THEN POP_ASSUM(fun th-> MRESA_TAC th[`v1:real^3`;`w1:real^3`])
1215 THEN MRESA_TAC Planarity.properties_fully_surrounded[`x1:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`u1:real^3`;`v1:real^3`;`w1:real^3`]
1216 THEN POP_ASSUM MP_TAC
1217 THEN ONCE_REWRITE_TAC[SET_RULE`{x1, u1, v1, w1}={x1, w1, v1, u1}`]
1218 THEN STRIP_TAC
1219 THEN MRESA_TAC CLOSURE_AFF_GT_3_1_EQ_AFF_GE_3_1[`x1:real^3`;`w1:real^3`;`v1:real^3`;`u1:real^3`]
1220 THEN MRESA_TAC Planarity.coplanar_cross_dot[`x1:real^3`;`w1:real^3`;`v1:real^3`;`u1:real^3`]
1221 THEN MP_TAC(REAL_ARITH`~(((w1 - x1) cross (v1 - x1)) dot (u1 - x1) = &0)
1222 ==> &0 < ((w1 - x1) cross (v1 - x1)) dot (u1 - x1)
1223 \/ &0 < --( ((w1 - x1) cross (v1 - x1)) dot (u1 - x1:real^3) )`)
1224 THEN RESA_TAC;
1225 MRESA_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot[`x1:real^3`;`w1:real^3`;`v1:real^3`;`u1:real^3`]
1226 THEN MRESA_TAC aff_gt_3_1_rep_cross_dot[`x1:real^3`;`w1:real^3`;`v1:real^3`;`u1:real^3`]
1227 THEN EXPAND_TAC"x1"
1228 THEN REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`;DOT_RADD;DOT_RMUL]
1229 THEN REPEAT STRIP_TAC
1230 THEN MRESA_TAC REAL_LT_MUL[`t:real`;`(w1 cross v1) dot (z:real^3)`]
1231 THEN MP_TAC(REAL_ARITH`t< &1==> &0<= &1- t`)
1232 THEN RESA_TAC
1233 THEN MRESA_TAC REAL_LE_MUL[`&1-t:real`;`(w1 cross v1) dot (a:real^3)`]
1234 THEN POP_ASSUM MP_TAC
1235 THEN REMOVE_ASSUM_TAC
1236 THEN POP_ASSUM MP_TAC
1237 THEN POP_ASSUM MP_TAC
1238 THEN REAL_ARITH_TAC;
1239 POP_ASSUM MP_TAC
1240 THEN REWRITE_TAC[VECTOR_ARITH`A - vec 0=A`;GSYM DOT_LNEG]
1241 THEN ONCE_REWRITE_TAC[GSYM CROSS_SKEW]
1242 THEN STRIP_TAC
1243 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1244 THEN MRESA_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot[`x1:real^3`;`v1:real^3`;`w1:real^3`;`u1:real^3`]
1245 THEN POP_ASSUM MP_TAC
1246 THEN ONCE_REWRITE_TAC[SET_RULE`{x1, v1, w1, u1}={x1, w1, v1, u1}`]
1247 THEN RESA_TAC
1248 THEN MRESA_TAC aff_gt_3_1_rep_cross_dot[`x1:real^3`;`v1:real^3`;`w1:real^3`;`u1:real^3`]
1249 THEN POP_ASSUM MP_TAC
1250 THEN ONCE_REWRITE_TAC[SET_RULE`{x1, v1, w1, u1}={x1, w1, v1, u1}`]
1251 THEN RESA_TAC
1252 THEN EXPAND_TAC"x1"
1253 THEN REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`;DOT_RADD;DOT_RMUL]
1254 THEN REPEAT STRIP_TAC
1255 THEN MRESA_TAC REAL_LT_MUL[`t:real`;`(v1 cross w1) dot (z:real^3)`]
1256 THEN MP_TAC(REAL_ARITH`t< &1==> &0<= &1- t`)
1257 THEN RESA_TAC
1258 THEN MRESA_TAC REAL_LE_MUL[`&1-t:real`;`(v1 cross w1) dot (a:real^3)`]
1259 THEN POP_ASSUM MP_TAC
1260 THEN REMOVE_ASSUM_TAC
1261 THEN POP_ASSUM MP_TAC
1262 THEN POP_ASSUM MP_TAC
1263 THEN REAL_ARITH_TAC;
1264 SUBGOAL_THEN `(!t. &0 < t /\ t < &1 ==> (&1 - t) % a + t % z IN yfan (x1,V:real^3->bool,E))` ASSUME_TAC;
1265 ASM_TAC
1266 THEN SET_TAC[];
1267 MRESA_TAC not_azim_points1_in_yfan[`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`a:real^3`;`z:real^3`;`v:real^3`;`w:real^3`]
1268 THEN MRESA_TAC not_azim_points1_in_yfan[`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`a:real^3`;`z:real^3`;`w:real^3`;`v:real^3`]
1269 THEN POP_ASSUM MP_TAC
1270 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1271 THEN ASM_REWRITE_TAC[]
1272 THEN STRIP_TAC
1273 THEN MP_TAC(REAL_ARITH`~(azim x1 a z v = &0) /\ &0<= azim x1 a z v==> &0< azim x1 a z (v:real^3) `)
1274 THEN ASM_REWRITE_TAC[azim]
1275 THEN STRIP_TAC
1276 THEN MRESA_TAC properties_of_collinear4_points_fan[`x1:real^3`;`v:real^3`;`w:real^3`;`a:real^3`]
1277 THEN MRESA_TAC properties_of_collinear4_points_fan[`x1:real^3`;`w:real^3`;`v:real^3`;`a:real^3`]
1278 THEN POP_ASSUM MP_TAC
1279 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1280 THEN ASM_REWRITE_TAC[]
1281 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1282 THEN STRIP_TAC
1283 THEN MRESA_TAC point_in_yfan_and_point_in_xfan_indepent_fan[`x1:real^3`;`(V:real^3->bool)`;` (E:(real^3->bool)->bool)`;`U:real^3->bool`;`a:real^3`;` z:real^3`]
1284 THEN DISJ_CASES_TAC(REAL_ARITH`azim x1 a z (v:real^3)< pi \/ pi<= azim x1 a z (v:real^3)`);
1285 MRESA_TAC cross_dot_fully_surrounded_fan[`x1:real^3`;`a:real^3`; `v:real^3`;`z:real^3`]
1286 THEN POP_ASSUM MP_TAC
1287 THEN EXPAND_TAC"x1"
1288 THEN REWRITE_TAC[VECTOR_ARITH`A- vec 0 =A`]
1289 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1290 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1291 THEN STRIP_TAC
1292 THEN ABBREV_TAC`u1=inverse1_sigma_fan (x1:real^3) (V:real^3->bool) (E:(real^3->bool)->bool) (w:real^3) (v:real^3)`
1293 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`v:real^3`;`w:real^3`]
1294 THEN REMOVE_ASSUM_TAC
1295 THEN POP_ASSUM MP_TAC
1296 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1297 THEN RESA_TAC
1298 THEN MRESA_TAC INVERSE1_SIGMA_FAN[`x1:real^3`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`w:real^3`]
1299 THEN REMOVE_ASSUM_TAC
1300 THEN POP_ASSUM (fun th-> POP_ASSUM (fun th-> MRESA1_TAC th `v:real^3`
1301 THEN POP_ASSUM MP_TAC
1302 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1303 THEN RESA_TAC
1304 ) THEN MRESA1_TAC th `v:real^3`THEN POP_ASSUM MP_TAC
1305 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1306 THEN RESA_TAC
1307 )
1308 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;`u1:real^3`;`w:real^3`]
1309 THEN REMOVE_ASSUM_TAC
1310 THEN POP_ASSUM MP_TAC
1311 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1312 THEN STRIP_TAC
1313 THEN MRESA_TAC exists_dart_leads_into_edge_eq_topological1_component_fan[`x1:real^3`;`(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`a:real^3`;`z:real^3`;`v:real^3`;`w:real^3`;` (u1:real^3)`]
1314 THEN POP_ASSUM MP_TAC
1315 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1316 THEN ASM_REWRITE_TAC[]
1317 THEN EXPAND_TAC"x1"
1318 THEN REWRITE_TAC[VECTOR_ARITH`A- vec 0 =A`]
1319 THEN ASM_REWRITE_TAC[]
1320 THEN STRIP_TAC
1321 THEN EXISTS_TAC`(x1,v,w,sigma_fan x1 V E v w):real^3#real^3#real^3#real^3`
1322 THEN ASM_REWRITE_TAC[pr2;pr3]
1323 THEN ABBREV_TAC`ds2= face (hypermap1_of_fanx (x1,V,E)) ((x1,v,w,sigma_fan x1 V E v w):real^3#real^3#real^3#real^3)`
1324 THEN MRESA_TAC hypermap_of_fan_rep[`x1:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`(\t. res (t x1 V E) (d1_fan (x1,V,E)))`]
1325 THEN REMOVE_ASSUM_TAC
1326 THEN REMOVE_ASSUM_TAC
1327 THEN REMOVE_ASSUM_TAC
1328 THEN SUBGOAL_THEN`ds2 IN face_set(hypermap1_of_fanx (x1:real^3,V,E))` ASSUME_TAC;
1329 ASM_REWRITE_TAC[face_set;set_of_orbits;IN_ELIM_THM]
1330 THEN EXISTS_TAC`(x1,v,w,sigma_fan x1 V E v w):real^3#real^3#real^3#real^3`
1331 THEN EXPAND_TAC"ds2"
1332 THEN REWRITE_TAC[face]
1333 THEN MRESA_TAC dartset_fully_surrounded_is_non_isolated_fan[`x1:real^3`;`(V:real^3->bool)`; `(E:(real^3->bool)->bool)`]
1334 THEN REWRITE_TAC[d1_fan;IN_ELIM_THM]
1335 THEN EXISTS_TAC`x1:real^3`
1336 THEN EXISTS_TAC`v:real^3`
1337 THEN EXISTS_TAC`w:real^3`
1338 THEN EXISTS_TAC`sigma_fan x1 V E v w:real^3`
1339 THEN ASM_REWRITE_TAC[];
1340 SUBGOAL_THEN` (x1,v,w,sigma_fan x1 V E v w):real^3#real^3#real^3#real^3 IN ds2` ASSUME_TAC;
1341 EXPAND_TAC"ds2"
1342 THEN REWRITE_TAC[face;IN_ELIM_THM;orbit_map]
1343 THEN EXISTS_TAC`0:num`
1344 THEN REWRITE_TAC[ARITH_RULE`0>= 0`;POWER;I_DEF];
1345 MRESA_TAC DARTSET_LEADS_INTO_FAN[`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`ds2:real^3#real^3#real^3#real^3->bool`]
1346 THEN POP_ASSUM (fun th-> MRESAL1_TAC th `(x1,v,w,sigma_fan x1 V E v w):real^3#real^3#real^3#real^3`[pr2;pr3])
1347 THEN MRESA_TAC PIIJBJK[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;]
1348 THEN POP_ASSUM MP_TAC
1349 THEN ASM_REWRITE_TAC[conforming_fan;conforming_bijection_fan;EXISTS_UNIQUE]
1350 THEN STRIP_TAC
1351 THEN REMOVE_ASSUM_TAC
1352 THEN REMOVE_ASSUM_TAC
1353 THEN REMOVE_ASSUM_TAC
1354 THEN POP_ASSUM(fun th-> MRESA1_TAC th`U:real^3->bool`)
1355 THEN POP_ASSUM(fun th-> MRESA1_TAC th`ds2:real^3#real^3#real^3#real^3->bool`
1356 THEN MRESA1_TAC th`f:real^3#real^3#real^3#real^3->bool`)
1357 THEN POP_ASSUM MP_TAC
1358 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);
1359 MRESA_TAC aff_gt2_subset_aff_ge[`x1:real^3`;`w:real^3`; `v:real^3`;`a:real^3`]
1360 THEN POP_ASSUM MP_TAC
1361 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1362 THEN RESA_TAC
1363 THEN MRESA_TAC sum5_azim_fan[`x1:real^3`;`a:real^3`;`z:real^3`;`w:real^3`;`v:real^3`]
1364 THEN MP_TAC(REAL_ARITH`azim x1 a z v = azim x1 a z w + pi/\
1365 azim x1 a z v < &2 * pi/\ ~(azim x1 a z w = &0) /\ &0 <= azim x1 a z w
1366 ==>  &0< azim x1 a z w /\ azim x1 a z w < pi
1367 `)
1368 THEN ASM_REWRITE_TAC[azim]
1369 THEN STRIP_TAC;
1370 MRESA_TAC cross_dot_fully_surrounded_fan[`x1:real^3`;`a:real^3`; `w:real^3`;`z:real^3`]
1371 THEN POP_ASSUM MP_TAC
1372 THEN EXPAND_TAC"x1"
1373 THEN REWRITE_TAC[VECTOR_ARITH`A- vec 0 =A`]
1374 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1375 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1376 THEN STRIP_TAC
1377 THEN MRESA_TAC exists_dart_leads_into_edge_eq_topological1_component_fan[`x1:real^3`;`(V:real^3->bool)` ;`(E:(real^3->bool)->bool)`;`U:real^3->bool`;`a:real^3`;`z:real^3`;`w:real^3`;`v:real^3`;` (u:real^3)`]
1378 THEN POP_ASSUM MP_TAC
1379 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1380 THEN ASM_REWRITE_TAC[]
1381 THEN EXPAND_TAC"x1"
1382 THEN REWRITE_TAC[VECTOR_ARITH`A- vec 0 =A`]
1383 THEN ASM_REWRITE_TAC[]
1384 THEN STRIP_TAC
1385 THEN EXISTS_TAC`(x1,w,v,sigma_fan x1 V E w v):real^3#real^3#real^3#real^3`
1386 THEN ASM_REWRITE_TAC[pr2;pr3]
1387 THEN ABBREV_TAC`ds2= face (hypermap1_of_fanx (x1,V,E)) ((x1,w,v,sigma_fan x1 V E  w v):real^3#real^3#real^3#real^3)`
1388 THEN MRESA_TAC hypermap_of_fan_rep[`x1:real^3`;`V:real^3->bool`;`(E:(real^3->bool)->bool)`;`(\t. res (t x1 V E) (d1_fan (x1,V,E)))`]
1389 THEN REMOVE_ASSUM_TAC
1390 THEN REMOVE_ASSUM_TAC
1391 THEN REMOVE_ASSUM_TAC
1392 THEN SUBGOAL_THEN`ds2 IN face_set(hypermap1_of_fanx (x1:real^3,V,E))` ASSUME_TAC;
1393 ASM_REWRITE_TAC[face_set;set_of_orbits;IN_ELIM_THM]
1394 THEN EXISTS_TAC`(x1,w,v,sigma_fan x1 V E w v):real^3#real^3#real^3#real^3`
1395 THEN EXPAND_TAC"ds2"
1396 THEN REWRITE_TAC[face]
1397 THEN MRESA_TAC dartset_fully_surrounded_is_non_isolated_fan[`x1:real^3`;`(V:real^3->bool)`; `(E:(real^3->bool)->bool)`]
1398 THEN REWRITE_TAC[d1_fan;IN_ELIM_THM]
1399 THEN EXISTS_TAC`x1:real^3`
1400 THEN EXISTS_TAC`w:real^3`
1401 THEN EXISTS_TAC`v:real^3`
1402 THEN EXISTS_TAC`sigma_fan x1 V E w v:real^3`
1403 THEN ASM_REWRITE_TAC[]
1404 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1405 THEN ASM_REWRITE_TAC[];
1406 ASM_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1407 THEN SUBGOAL_THEN` (x1,w,v,sigma_fan x1 V E w v):real^3#real^3#real^3#real^3 IN ds2` ASSUME_TAC;
1408 EXPAND_TAC"ds2"
1409 THEN REWRITE_TAC[face;IN_ELIM_THM;orbit_map]
1410 THEN EXISTS_TAC`0:num`
1411 THEN REWRITE_TAC[ARITH_RULE`0>= 0`;POWER;I_DEF];
1412 MRESA_TAC DARTSET_LEADS_INTO_FAN[`x1:real^3`;`(V:real^3->bool)`;`(E:(real^3->bool)->bool)`;`ds2:real^3#real^3#real^3#real^3->bool`]
1413 THEN POP_ASSUM (fun th-> MRESAL1_TAC th `(x1,w,v,sigma_fan x1 V E w v):real^3#real^3#real^3#real^3`[pr2;pr3])
1414 THEN MRESA_TAC PIIJBJK[`vec 0:real^3`;`vertices (p:real^3->bool)`;`edges (p:real^3->bool)`;]
1415 THEN POP_ASSUM MP_TAC
1416 THEN ASM_REWRITE_TAC[conforming_fan;conforming_bijection_fan;EXISTS_UNIQUE]
1417 THEN STRIP_TAC
1418 THEN REMOVE_ASSUM_TAC
1419 THEN REMOVE_ASSUM_TAC
1420 THEN REMOVE_ASSUM_TAC
1421 THEN POP_ASSUM(fun th-> MRESA1_TAC th`U:real^3->bool`)
1422 THEN POP_ASSUM(fun th-> MRESA1_TAC th`ds2:real^3#real^3#real^3#real^3->bool`
1423 THEN MRESA1_TAC th`f:real^3#real^3#real^3#real^3->bool`)
1424 THEN POP_ASSUM MP_TAC
1425 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
1426 ]);;
1427
1428 let CFYXFTY0=prove(`!p:real^3->bool f.
1429  bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p
1430 /\ f facet_of p
1431 ==>  EDGES0_FAN p f = edges f`,
1432 SET_TAC[MAP_EDGES_FACET_INTO_E1_FAN; MAP_EDGES_FACET_INTO_E1_FAN_INJ]);;
1433
1434
1435 let CFYXFTY1=prove(`!p:real^3->bool f f1.
1436  bounded (p:real^3->bool) /\ polyhedron p /\ vec 0 IN interior p
1437 /\ f IN face_set (hypermap1_of_fanx  (vec 0,vertices p,edges p))
1438 /\ f1 facet_of p /\
1439  fchanged f1 =dartset_leads_into_fan (vec 0) (vertices p) (edges p) f
1440 ==>   EDGES0_FAN p f1 = {{pr2 e, pr3 e}|  e IN f} `,
1441 REPEAT STRIP_TAC
1442 THEN REWRITE_TAC[EXTENSION]
1443 THEN GEN_TAC
1444 THEN EQ_TAC
1445 THENL[  MRESA_TAC EDGES0_SUBSET_FAN[`p:real^3->bool`;`f:real^3#real^3#real^3#real^3->bool`;`f1:real^3->bool`]
1446 THEN POP_ASSUM MP_TAC
1447 THEN SET_TAC[];
1448  MRESA_TAC SUBSET_EDGES0_FAN [`p:real^3->bool`;`f:real^3#real^3#real^3#real^3->bool`;`f1:real^3->bool`]
1449 THEN POP_ASSUM MP_TAC
1450 THEN SET_TAC[]]);;
1451
1452
1453 end;;
1454
1455