text_formalization/local/NKEZBFC.hl

   1 module Nkezbfc_local = struct
   2
   3
   4 open Sphere;;
   5 open Fan_defs;;
   6 open Hypermap;;
   7 open Vol1;;
   8 open Fan;;
   9 open Topology;;
  10 open Fan_misc;;
  11 open Planarity;;
  12 open Conforming;;
  13 open Sphere;;
  14 open Trigonometry1;;
  15 open Trigonometry2;;
  16 open Hypermap;;
  17 open Fan;;
  18 open Topology;;
  19 open Prove_by_refinement;;
  20 open Wrgcvdr_cizmrrh;;
  21 open Local_lemmas;;
  22
  23
  24
  25 open Ldurdpn;;
  26 open Lvducxu;;
  27 open Aff_sgn_tac;;
  28 open Local_lemmas1;;
  29
  30
  31
  32 (* deprecated 2013-02-22
  33 let sol_local_fan = new_definition ` sol_local_fan V E f= &2 * pi+ sum f (\e. azim_in_fan e E- pi)`;;
  34 *)
  35
  36 let sol_local = new_definition ` sol_local E f= &2 * pi+ sum f (\e. azim_in_fan e E- pi)`;;
  37
  38
  39 let CONVEX_LOFA_IMP_INANGLE_EQ_AZIM = prove_by_refinement
  40 (`convex_local_fan (V,E,FF) ==>(!v. v IN V ==> interior_angle1 (vec 0) FF v = azim_in_fan (v, rho_node1 FF v) E) `,
  41 [REWRITE_TAC[convex_local_fan; azim_in_fan2];
  42 REPEAT STRIP_TAC;
  43 ASSUME_TAC2 EXISTS_INVERSE_OF_V;
  44 DOWN THEN STRIP_TAC;
  45 ASSUME_TAC2 LOFA_IMP_EE_TWO_ELMS;
  46 ASSUME_TAC2 LOFA_CARD_EE_V_1;
  47 ASSUME_TAC2 LOCAL_FAN_RHO_NODE_PROS2;
  48 DOWN THEN STRIP_TAC;
  49 UNDISCH_TAC` v:real^3 IN V `;
  50 FIRST_ASSUM NHANH;
  51 UNDISCH_TAC` !x. x IN FF
  52 ==> (let d = azim_cycle (EE (FST x) E) (vec 0) (FST x) (SND x) in
  53 if CARD (EE (FST x) E) > 1
  54 then azim (vec 0) (FST x) (SND x) d
  55 else &2 * pi) <=
  56 pi /\
  57 V SUBSET wedge_in_fan_ge x E`;
  58 DISCH_THEN NHANH;
  59 LET_TAC;
  60 SWITCH_TAC` EE v E = {rho_node1 FF v, vv} `;
  61 ASM_SIMP_TAC[ARITH_RULE` a = 2 ==> a > 1 `];
  62 STRIP_TAC;
  63 DOWN THEN DOWN THEN PHA;
  64 ASSUME_TAC2 (SPEC `vv:real^3 ` (GEN` v:real^3 ` IVS_RHO_IDD));
  65 EXPAND_TAC "d";
  66 SIMP_TAC[];
  67 UNDISCH_TAC` {rho_node1 FF v, vv} = EE v E `;
  68 DISCH_THEN (SUBST1_TAC o SYM);
  69 EXPAND_TAC "v";
  70 DOWN;
  71 SIMP_TAC[interior_angle1; GSYM ivs_rho_node1; AZIM_CYCLE_TWO_POINT_SET]]);;
  72
  73
  74
  75 let SOL_LOFA_EQ_SUM_INANGLE=prove_by_refinement(` convex_local_fan(V,E,FF)
  76 ==> sol_local E FF= &2 * pi + sum V (\v. interior_angle1 (vec 0) FF v -pi)`,
  77 [REWRITE_TAC[sol_local;]
  78 THEN REPEAT STRIP_TAC
  79 THEN POP_ASSUM(fun th-> MP_TAC th THEN
  80 REWRITE_TAC[convex_local_fan] THEN STRIP_TAC
  81 THEN ASSUME_TAC th)
  82 THEN MRESAL_TAC (GEN_ALL WRGCVDR)[`E:(real^3->bool)->bool`;`(\x:real^3#real^3. FST x)`;`FF:(real^3#real^3)->bool`;`V:real^3->bool`;`hro:real^3->real^3`][REAL_ARITH`&2 * pi + A= &2 * pi + B<=> A=B`;BIJ;INJ;SURJ]
  83 THEN MATCH_MP_TAC SUM_EQ_GENERAL
  84 THEN EXISTS_TAC`(\x:real^3#real^3. FST x)`
  85 THEN ASM_REWRITE_TAC[]
  86 THEN STRIP_TAC;
  87 ASM_TAC
  88 THEN MESON_TAC[];
  89 REPEAT STRIP_TAC;
  90 ASM_TAC
  91 THEN MESON_TAC[];
  92 ASSUME_TAC2 LOCAL_FAN_RHO_NODE_PROS
  93 THEN POP_ASSUM MP_TAC
  94 THEN STRIP_TAC
  95 THEN POP_ASSUM(fun th-> MRESA1_TAC th `x:real^3#real^3`)
  96 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th;])
  97 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_IMP_IN_V2
  98 THEN ASSUME_TAC2 CONVEX_LOFA_IMP_INANGLE_EQ_AZIM
  99 THEN POP_ASSUM(fun th-> MRESA1_TAC th `FST (x:real^3#real^3)`)]);;
 100
 101
 102
 103 let CARD_VERTEX_GE_3_LOCAL_FAN=prove_by_refinement(`!V E FF. convex_local_fan(V,E,FF)
 104 ==> 3 <= CARD V`,
 105
 106 [REPEAT STRIP_TAC
 107 THEN POP_ASSUM(fun th-> MP_TAC th THEN
 108 REWRITE_TAC[convex_local_fan] THEN STRIP_TAC
 109 THEN ASSUME_TAC th)
 110 THEN SUBGOAL_THEN`?v:real^3. v IN V`ASSUME_TAC;
 111 ASM_TAC
 112 THEN SIMP_TAC[convex_local_fan;local_fan;FAN;fan1;SET_RULE`~(V SUBSET {}) <=> ~(V= {})`;SET_RULE`~(V={}) <=> ?v. v IN V`]
 113 THEN LET_TAC
 114 THEN SET_TAC[];
 115
 116 POP_ASSUM MP_TAC
 117 THEN STRIP_TAC
 118 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`]
 119 THEN REMOVE_ASSUM_TAC
 120 THEN POP_ASSUM(fun th-> MRESA1_TAC th `v:real^3`)
 121 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)
 122 [`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`rho_node1 FF v` ;`V:real^3->bool`]
 123 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`]
 124 THEN REMOVE_ASSUM_TAC
 125 THEN POP_ASSUM(fun th-> MRESA1_TAC th `rho_node1 FF v:real^3`)
 126 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)
 127 [`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`rho_node1 FF v:real^3`;`rho_node1 FF (rho_node1 FF v)` ;`V:real^3->bool`]
 128 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)
 129 [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` v:real^3`;]
 130 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)
 131 [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` rho_node1 FF v:real^3`;]
 132 THEN MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`rho_node1 FF v:real^3`]
 133 THEN MP_TAC(SET_RULE`DISJOINT {vec 0, v:real^3} {rho_node1 FF v}==> ~(v=rho_node1 FF v)`)
 134 THEN RESA_TAC
 135 THEN MRESA_TAC th3[`vec 0:real^3`;`rho_node1 FF v:real^3`;`rho_node1 FF (rho_node1 FF v):real^3`]
 136 THEN MP_TAC(SET_RULE`DISJOINT {vec 0, rho_node1 FF v:real^3} {rho_node1 FF (rho_node1 FF v)}==> ~(rho_node1 FF v=rho_node1 FF(rho_node1 FF v))`)
 137 THEN RESA_TAC
 138 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE
 139 THEN POP_ASSUM(fun th-> MRESA1_TAC th `v:real^3`)
 140 THEN SUBGOAL_THEN(`CARD {v,rho_node1 FF v,rho_node1 FF (rho_node1 FF v):real^3}=3`)ASSUME_TAC;
 141
 142 SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
 143 IN_INSERT; NOT_IN_EMPTY]
 144 THEN ASM_REWRITE_TAC[]
 145 THEN ARITH_TAC;
 146 MP_TAC(SET_RULE`rho_node1 FF v IN V /\ v IN V /\ rho_node1 FF (rho_node1 FF v) IN V==> {v,rho_node1 FF v,rho_node1 FF (rho_node1 FF v):real^3} SUBSET V`)
 147 THEN RESA_TAC
 148 THEN ASM_TAC
 149 THEN REWRITE_TAC[local_fan;FAN;fan1]
 150 THEN LET_TAC
 151 THEN REPEAT STRIP_TAC
 152 THEN MRESA_TAC CARD_SUBSET[`{v,rho_node1 FF v,rho_node1 FF (rho_node1 FF v):real^3}`;`V:real^3->bool`]]);;
 153
 154
 155
 156
 157 let REP_VERTEX_3_LOCAL_FAN=prove_by_refinement(` CARD V=3 /\ convex_local_fan(V,E,FF)
 158 ==> ?v. V= {v,rho_node1 FF v,rho_node1 FF (rho_node1 FF v)}
 159 /\ ~(v=rho_node1 FF v) /\ ~(rho_node1 FF v=rho_node1 FF (rho_node1 FF v))/\
 160 ~(rho_node1 FF (rho_node1 FF v)=v)`,
 161 [
 162 REPEAT STRIP_TAC
 163 THEN POP_ASSUM(fun th-> MP_TAC th THEN
 164 REWRITE_TAC[convex_local_fan] THEN STRIP_TAC
 165 THEN ASSUME_TAC th)
 166 THEN SUBGOAL_THEN`?v:real^3. v IN V`ASSUME_TAC;
 167 ASM_TAC
 168 THEN SIMP_TAC[convex_local_fan;local_fan;FAN;fan1;SET_RULE`~(V SUBSET {}) <=> ~(V= {})`;SET_RULE`~(V={}) <=> ?v. v IN V`]
 169 THEN LET_TAC
 170 THEN SET_TAC[];
 171 POP_ASSUM MP_TAC
 172 THEN STRIP_TAC
 173 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`]
 174 THEN REMOVE_ASSUM_TAC
 175 THEN POP_ASSUM(fun th-> MRESA1_TAC th `v:real^3`)
 176 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)
 177 [`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`rho_node1 FF v` ;`V:real^3->bool`]
 178 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`]
 179 THEN REMOVE_ASSUM_TAC
 180 THEN POP_ASSUM(fun th-> MRESA1_TAC th `rho_node1 FF v:real^3`)
 181 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)
 182 [`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`rho_node1 FF v:real^3`;`rho_node1 FF (rho_node1 FF v)` ;`V:real^3->bool`]
 183 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)
 184 [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` v:real^3`;]
 185 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)
 186 [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` rho_node1 FF v:real^3`;]
 187 THEN MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`rho_node1 FF v:real^3`]
 188 THEN MP_TAC(SET_RULE`DISJOINT {vec 0, v:real^3} {rho_node1 FF v}==> ~(v=rho_node1 FF v)`)
 189 THEN RESA_TAC
 190 THEN MRESA_TAC th3[`vec 0:real^3`;`rho_node1 FF v:real^3`;`rho_node1 FF (rho_node1 FF v):real^3`]
 191 THEN MP_TAC(SET_RULE`DISJOINT {vec 0, rho_node1 FF v:real^3} {rho_node1 FF (rho_node1 FF v)}==> ~(rho_node1 FF v=rho_node1 FF(rho_node1 FF v))`)
 192 THEN RESA_TAC
 193 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE
 194 THEN POP_ASSUM(fun th-> MRESA1_TAC th `v:real^3`)
 195 THEN SUBGOAL_THEN(`CARD {v,rho_node1 FF v,rho_node1 FF (rho_node1 FF v):real^3}=3`)ASSUME_TAC;
 196 SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
 197 IN_INSERT; NOT_IN_EMPTY]
 198 THEN ASM_REWRITE_TAC[]
 199 THEN ARITH_TAC;
 200
 201 MP_TAC(SET_RULE`rho_node1 FF v IN V /\ v IN V /\ rho_node1 FF (rho_node1 FF v) IN V==> {v,rho_node1 FF v,rho_node1 FF (rho_node1 FF v):real^3} SUBSET V`)
 202 THEN RESA_TAC
 203 THEN ASM_TAC
 204 THEN REWRITE_TAC[local_fan;FAN;fan1]
 205 THEN LET_TAC
 206 THEN REPEAT STRIP_TAC
 207 THEN MRESA_TAC CARD_SUBSET_EQ[`{v,rho_node1 FF v,rho_node1 FF (rho_node1 FF v):real^3}`;`V:real^3->bool`]
 208 THEN EXISTS_TAC`v:real^3`
 209 THEN ASM_REWRITE_TAC[]
 210 THEN ASM_TAC
 211 THEN REPEAT RESA_TAC]);;
 212
 213
 214 let CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS = prove(`convex_local_fan (V,E,FF) ==>(!v. v IN V ==> interior_angle1 (vec 0) FF v = azim (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v)) `,
 215
 216 REWRITE_TAC[convex_local_fan; azim_in_fan2]
 217 THEN REPEAT STRIP_TAC
 218 THEN ASSUME_TAC2 EXISTS_INVERSE_OF_V
 219 THEN DOWN THEN STRIP_TAC
 220 THEN ASSUME_TAC2 LOFA_IMP_EE_TWO_ELMS
 221 THEN ASSUME_TAC2 LOFA_CARD_EE_V_1
 222 THEN ASSUME_TAC2 LOCAL_FAN_RHO_NODE_PROS2
 223 THEN DOWN THEN STRIP_TAC
 224 THEN UNDISCH_TAC` v:real^3 IN V `
 225 THEN FIRST_ASSUM NHANH
 226 THEN UNDISCH_TAC` !x. x IN FF
 227 ==> (let d = azim_cycle (EE (FST x) E) (vec 0) (FST x) (SND x) in
 228 if CARD (EE (FST x) E) > 1
 229 then azim (vec 0) (FST x) (SND x) d
 230 else &2 * pi) <=
 231 pi /\
 232 V SUBSET wedge_in_fan_ge x E`
 233 THEN DISCH_THEN NHANH
 234 THEN LET_TAC
 235 THEN SWITCH_TAC` EE v E = {rho_node1 FF v, vv} `
 236 THEN ASM_SIMP_TAC[ARITH_RULE` a = 2 ==> a > 1 `]
 237 THEN STRIP_TAC
 238 THEN DOWN THEN DOWN THEN PHA
 239 THEN ASSUME_TAC2 (SPEC `vv:real^3 ` (GEN` v:real^3 ` IVS_RHO_IDD))
 240 THEN EXPAND_TAC "d"
 241 THEN SIMP_TAC[]
 242 THEN UNDISCH_TAC` {rho_node1 FF v, vv} = EE v E `
 243 THEN DISCH_THEN (SUBST1_TAC o SYM)
 244 THEN EXPAND_TAC "v"
 245 THEN DOWN
 246 THEN SIMP_TAC[interior_angle1; GSYM ivs_rho_node1; AZIM_CYCLE_TWO_POINT_SET]);;
 247
 248 let SOL_LOCAL_FAN_POS_CASE3=prove(`!V E FF. convex_local_fan(V,E,FF)
 249 /\ CARD V=3
 250 ==> &0 <= sol_local E FF`,
 251 REPEAT STRIP_TAC
 252 THEN ASSUME_TAC2 SOL_LOFA_EQ_SUM_INANGLE
 253 THEN ASM_REWRITE_TAC[]
 254 THEN ASSUME_TAC2 REP_VERTEX_3_LOCAL_FAN
 255 THEN POP_ASSUM MP_TAC
 256 THEN RESA_TAC
 257 THEN SIMP_TAC[HAS_SIZE; SUM_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
 258 IN_INSERT; NOT_IN_EMPTY]
 259 THEN ASM_REWRITE_TAC[]
 260 THEN UNDISCH_TAC`convex_local_fan (V:real^3->bool,E,FF)`
 261 THEN STRIP_TAC
 262 THEN POP_ASSUM( fun th-> MP_TAC th
 263 THEN REWRITE_TAC[convex_local_fan ] THEN ASSUME_TAC th)
 264 THEN STRIP_TAC
 265 THEN MRESAL_TAC(GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`v:real^3`;][SET_RULE`A IN {A,B,C}`]
 266 THEN MRESAL_TAC(GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` rho_node1 FF v:real^3`;][SET_RULE`B IN {A,B,C}`]
 267 THEN MRESAL_TAC(GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` rho_node1 FF (rho_node1 FF v):real^3`;][SET_RULE`C IN {A,B,C}`]
 268 THEN DISJ_CASES_TAC(SET_RULE`(?v. v IN V /\ pi <= interior_angle1 (vec 0) FF v)\/ ~(?v. v IN V /\ pi <= interior_angle1 (vec 0) FF v)`)
 269 THENL[
 270
 271 POP_ASSUM MP_TAC
 272 THEN ASM_REWRITE_TAC[SET_RULE`A IN {B,C,D}<=> A=B \/ A=C\/ A=D`]
 273 THEN STRIP_TAC
 274 THEN POP_ASSUM MP_TAC
 275 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
 276 THEN POP_ASSUM MP_TAC
 277 THEN POP_ASSUM MP_TAC
 278 THEN POP_ASSUM MP_TAC
 279 THEN REAL_ARITH_TAC;
 280 POP_ASSUM MP_TAC
 281 THEN POP_ASSUM MP_TAC
 282 THEN POP_ASSUM MP_TAC
 283 THEN POP_ASSUM MP_TAC
 284 THEN ASM_REWRITE_TAC[NOT_EXISTS_THM;DE_MORGAN_THM; REAL_ARITH`~(a<= b) <=> b<a`]
 285 THEN ASSUME_TAC2 CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS
 286 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`v:real^3`[SET_RULE`A IN {A,B,C}`]
 287 THEN MRESAL1_TAC th`rho_node1 FF v:real^3`[SET_RULE`B IN {A,B,C}`]
 288 THEN MRESAL1_TAC th`rho_node1 FF (rho_node1 FF v:real^3)`[SET_RULE`C IN {A,B,C}`])
 289 THEN MRESAL_TAC( GEN_ALL Local_lemmas.IVS_RHO_IDD)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`v:real^3`;][SET_RULE`A IN {A,B,C}`]
 290 THEN MRESAL_TAC( GEN_ALL Local_lemmas.IVS_RHO_IDD)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`rho_node1 FF v:real^3`;][SET_RULE`B IN {A,B,C}`]
 291 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`]
 292 THEN REMOVE_ASSUM_TAC
 293 THEN POP_ASSUM(fun th-> MRESAL1_TAC th `rho_node1 FF (rho_node1 FF v):real^3`[SET_RULE`C IN {A,B,C}`])
 294 THEN MRESAL_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)
 295 [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` rho_node1 FF (rho_node1 FF v):real^3`;][SET_RULE`C IN {A,B,C}`]
 296 THEN MRESA_TAC th3[`vec 0:real^3`;`rho_node1 FF (rho_node1 FF v):real^3`;`rho_node1 FF (rho_node1 FF (rho_node1 FF v)):real^3`]
 297 THEN MP_TAC(SET_RULE`DISJOINT {vec 0, rho_node1 FF (rho_node1 FF v):real^3} {rho_node1 FF (rho_node1 FF (rho_node1 FF v))}==> ~(rho_node1 FF (rho_node1 FF v)=rho_node1 FF (rho_node1 FF (rho_node1 FF v)))`)
 298 THEN RESA_TAC
 299 THEN MRESAL_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)
 300 [`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`rho_node1 FF (rho_node1 FF v):real^3`;`rho_node1 FF (rho_node1 FF (rho_node1 FF v))` ;`V:real^3->bool`][SET_RULE`C IN {A,B,C}`]
 301 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`]
 302 THEN POP_ASSUM(fun th-> MRESAL1_TAC th `rho_node1 FF v:real^3`[SET_RULE`B IN {A,B,C}`])
 303 THEN MP_TAC(SET_RULE`~(rho_node1 FF (rho_node1 FF v) =
 304 rho_node1 FF (rho_node1 FF (rho_node1 FF v:real^3)))
 305 /\ rho_node1 FF (rho_node1 FF (rho_node1 FF v)) IN
 306 {v, rho_node1 FF v, rho_node1 FF (rho_node1 FF v)}
 307 /\ ~(rho_node1 FF (rho_node1 FF (rho_node1 FF v)) = rho_node1 FF v)
 308 ==> rho_node1 FF (rho_node1 FF (rho_node1 FF v))=v
 309 `)
 310 THEN RESA_TAC
 311 THEN MRESAL_TAC( GEN_ALL Local_lemmas.IVS_RHO_IDD)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`rho_node1 FF (rho_node1 FF v):real^3`;][SET_RULE`C IN {A,B,C}`]
 312 THEN ABBREV_TAC`u=rho_node1 FF v`
 313 THEN ABBREV_TAC`w=rho_node1 FF u`
 314 THEN REPEAT STRIP_TAC
 315 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`v:real^3`[SET_RULE`A IN {A,B,C}`]
 316 THEN MRESAL1_TAC th`u:real^3`[SET_RULE`B IN {A,B,C}`]
 317 THEN MRESAL1_TAC th`w:real^3`[SET_RULE`C IN {A,B,C}`;])
 318 THEN REWRITE_TAC[REAL_ARITH`&0 <=
 319 &2 * pi + A - pi + B - pi + C - pi + &0 <=> &0 <= A+B+C - pi `]
 320 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`]
 321 THEN REMOVE_ASSUM_TAC
 322 THEN POP_ASSUM(fun th-> MRESAL1_TAC th `v:real^3`[SET_RULE`A IN {A,B,C}`]
 323 THEN MRESAL1_TAC th `u:real^3`[SET_RULE`B IN {A,B,C}`])
 324 THEN MRESAL_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)
 325 [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` v:real^3`;][SET_RULE`A IN {A,B,C}`]
 326 THEN UNDISCH_TAC`~collinear {vec 0, w:real^3, rho_node1 FF w}`
 327 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 328 THEN RESA_TAC
 329 THEN MP_TAC(REAL_ARITH`&0< azim (vec 0) v u w /\ azim (vec 0) v u w < pi ==> ~(azim (vec 0) v u w = &0 \/ azim (vec 0) v u (w:real^3) = pi)`)
 330 THEN RESA_TAC
 331 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 332 THEN POP_ASSUM (fun th->
 333 MP_TAC th THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
 334 THEN STRIP_TAC
 335 THEN MP_TAC th THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
 336 THEN STRIP_TAC
 337 THEN MP_TAC th THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
 338 THEN STRIP_TAC
 339 THEN MP_TAC th THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,C,B}`]
 340 THEN STRIP_TAC
 341 THEN ASSUME_TAC th)
 342 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR [`vec 0:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
 343 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR [`vec 0:real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
 344 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR [`vec 0:real^3`;`w:real^3`;`v:real^3`;`u:real^3`]
 345 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR [`vec 0:real^3`;`w:real^3`;`u:real^3`;`v:real^3`]
 346 THEN MRESA_TAC AZIM_DIVH [`vec 0:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 347 THEN MRESA_TAC AZIM_DIVH [`vec 0:real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
 348 THEN MRESA_TAC AZIM_DIVH [`vec 0:real^3`;`w:real^3`;`v:real^3`;`u:real^3`]
 349 THEN MRESAL_TAC VOLUME_SOLID_TRIANGLE[`&1:real`;`vec 0:real^3`;`v:real^3`;`u:real^3`;`w:real^3`][REAL_ARITH`&0< &1`]
 350 THEN POP_ASSUM MP_TAC
 351 THEN REPEAT LET_TAC
 352 THEN MRESA_TAC MEASURABLE_BALL_AFF_GT[`vec 0:real^3`;`&1`;`{vec 0:real^3}`;`{v,u,w:real^3}`]
 353 THEN STRIP_TAC
 354 THEN MP_TAC(MESON[volume_props]`measurable (ball (vec 0,&1) INTER aff_gt {vec 0} {v, u, w})==> vol (ball (vec 0,&1) INTER aff_gt {vec 0} {v, u, w}) >= &0`)
 355 THEN RESA_TAC
 356 THEN POP_ASSUM MP_TAC
 357 THEN REAL_ARITH_TAC]);;
 358
 359
 360 let AFF_LT_1_1 = prove
 361 (`!x w.
 362 ~(x=w)
 363 ==> aff_lt {x} {w} =
 364 {y | ?t1 t2.
 365 t2 < &0 /\
 366 t1 + t2 = &1 /\
 367 y = t1 % x + t2 % w}`,
 368 REWRITE_TAC[SET_RULE`~(x=w) <=> DISJOINT {x} {w}`] THEN AFF_TAC);;
 369
 370 let PROPERTIES_GENERIC_LOCAL_FAN=prove_by_refinement(`!V E FF v0. local_fan(V,E,FF) /\ v0 IN V /\ generic V E
 371 ==> (!v. v IN V /\ ~(v = v0) ==> ~collinear {vec 0, v0, v})`,
 372 [REPEAT GEN_TAC
 373 THEN REWRITE_TAC[generic;]
 374 THEN STRIP_TAC
 375 THEN POP_ASSUM MP_TAC
 376 THEN DISCH_THEN(LABEL_TAC"LINH")
 377 THEN REPEAT STRIP_TAC
 378 THEN MRESA_TAC(GEN_ALL LOCAL_FAN_RHO_NODE_PROS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;]
 379 THEN REMOVE_ASSUM_TAC
 380 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v0:real^3`)
 381 THEN MRESAL_TAC(GEN_ALL LOCAL_FAN_IN_FF_IN_ORD_PAIRS)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`v0,rho_node1 FF v0`;`E:(real^3->bool)->bool`;][GSYM IN_E_IFF_IN_ORD_E]
 382 THEN REMOVE_THEN "LINH"(fun th-> MRESA_TAC th[`v0:real^3`;`rho_node1 FF v0`;`v:real^3`])
 383 THEN POP_ASSUM MP_TAC
 384 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?w. w IN A`]
 385 THEN POP_ASSUM MP_TAC
 386 THEN POP_ASSUM MP_TAC
 387 THEN POP_ASSUM MP_TAC
 388 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 389 THEN REWRITE_TAC[COLLINEAR_3_EXPAND;VECTOR_ARITH`u % vec 0+ a=a`]
 390 THEN REPEAT STRIP_TAC;
 391 ASM_TAC
 392 THEN REWRITE_TAC[local_fan;FAN;fan2]
 393 THEN LET_TAC
 394 THEN SET_TAC[];
 395 ASM_REWRITE_TAC[]
 396 THEN DISJ_CASES_TAC(REAL_ARITH`&0<= &1-u \/ &1 -u< &0`);
 397 SUBGOAL_THEN`~(vec 0= v0:real^3)`ASSUME_TAC;
 398 ASM_TAC
 399 THEN REWRITE_TAC[local_fan;FAN;fan2]
 400 THEN LET_TAC
 401 THEN SET_TAC[];
 402 SUBGOAL_THEN`~(vec 0= v:real^3)`ASSUME_TAC;
 403 ASM_TAC
 404 THEN REWRITE_TAC[local_fan;FAN;fan2]
 405 THEN LET_TAC
 406 THEN SET_TAC[];
 407 SUBGOAL_THEN`v IN aff_ge {vec 0} {v0:real^3}` ASSUME_TAC;
 408 MRESAL_TAC AFF_GE_1_1[`vec 0:real^3`;`v0:real^3`][IN_ELIM_THM]
 409 THEN EXISTS_TAC `u:real`
 410 THEN EXISTS_TAC `&1-u:real`
 411 THEN ASM_REWRITE_TAC[REAL_ARITH`u+ &1- u= &1`]
 412 THEN VECTOR_ARITH_TAC;
 413 SUBGOAL_THEN`v IN aff_ge {vec 0} {v:real^3}` ASSUME_TAC;
 414 MRESAL_TAC AFF_GE_1_1[`vec 0:real^3`;`v:real^3`][IN_ELIM_THM]
 415 THEN EXISTS_TAC `&0:real`
 416 THEN EXISTS_TAC `&1:real`
 417 THEN ASM_REWRITE_TAC[REAL_ARITH`&0 + &1= &1 /\ &0<= &1`]
 418 THEN VECTOR_ARITH_TAC;
 419 UNDISCH_TAC`local_fan (V:real^3->bool,E,FF)`
 420 THEN REWRITE_TAC[local_fan;FAN;fan7]
 421 THEN LET_TAC
 422 THEN STRIP_TAC
 423 THEN REMOVE_ASSUM_TAC
 424 THEN REMOVE_ASSUM_TAC
 425 THEN REMOVE_ASSUM_TAC
 426 THEN UNDISCH_TAC `v=(&1 - u) % v0:real^3`
 427 THEN MP_TAC(SET_RULE`~(v = (v0:real^3))==> {v} INTER {v0}= {}`)
 428 THEN ASM_REWRITE_TAC[]
 429 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`{v:real^3}`;`{v0:real^3}`][UNION;IN_ELIM_THM;SET_RULE`(?v. v IN V /\ {v0} = {v})<=> v0 IN V`])
 430 THEN STRIP_TAC
 431 THEN UNDISCH_TAC`aff_ge {vec 0} {v} INTER aff_ge {vec 0} {v0} =
 432 aff_ge {vec 0} ({v} INTER {v0:real^3})`
 433 THEN ASM_REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING]
 434 THEN STRIP_TAC
 435 THEN MP_TAC(SET_RULE`v IN aff_ge {vec 0} {v0}/\ v IN aff_ge {vec 0} {v:real^3}
 436 /\ aff_ge {vec 0} {v} INTER aff_ge {vec 0} {v0} = {vec 0} ==> vec 0= v`)
 437 THEN ASM_REWRITE_TAC[];
 438 MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` v0:real^3`;]
 439 THEN MRESA_TAC Planarity.point_in_aff_ge[`vec 0:real^3`;`v0:real^3`;`rho_node1 FF v0`]
 440 THEN EXISTS_TAC`v0:real^3`
 441 THEN ASM_REWRITE_TAC[INTER;IN_ELIM_THM]
 442 THEN SUBGOAL_THEN`~(vec 0= v:real^3)`ASSUME_TAC;
 443 ASM_TAC
 444 THEN REWRITE_TAC[local_fan;FAN;fan2]
 445 THEN LET_TAC
 446 THEN SET_TAC[];
 447 POP_ASSUM MP_TAC
 448 THEN RESA_TAC
 449 THEN MRESAL_TAC AFF_LT_1_1[`vec 0:real^3`;`(&1 - u) % v0:real^3`][IN_ELIM_THM]
 450 THEN EXISTS_TAC `&1- inv(&1-u):real`
 451 THEN EXISTS_TAC `inv(&1-u):real`
 452 THEN ASM_REWRITE_TAC[REAL_ARITH`&1-a+a= &1`; VECTOR_ARITH`a %b%v=(a*b)%v`]
 453 THEN MP_TAC(REAL_ARITH`&1- u< &0 ==> ~(&1- u = &0)`)
 454 THEN RESA_TAC
 455 THEN MRESA1_TAC REAL_MUL_LINV`&1- u:real`
 456 THEN REWRITE_TAC[VECTOR_ARITH`v0 = (&1 - inv (&1 - u)) % vec 0 + &1 % v0`;REAL_ARITH`a< &0<=> &0< -- a`;GSYM REAL_INV_NEG;REAL_LT_INV_EQ]
 457 THEN ASM_TAC
 458 THEN REAL_ARITH_TAC]);;
 459
 460 let PROPERTIES_GENERIC= prove(` local_fan(V,E,FF) /\ generic V E /\ v IN V /\ w IN V
 461 ==> (!u u1. u IN {v,w} /\ u1 IN V /\ ~(u=u1) ==> ~(collinear {vec 0, u, u1}))`,
 462 REWRITE_TAC[SET_RULE`u IN {v,w} <=> u=v \/ u=w`]
 463 THEN REPEAT STRIP_TAC
 464 THEN ASM_MESON_TAC[PROPERTIES_GENERIC_LOCAL_FAN]);;
 465
 466 let PROPERTIES_GENERIC1= prove(` convex_local_fan(V,E,FF) /\ generic V E /\ v IN V /\ w IN V
 467 ==> (!u u1. u IN {v,w} /\ u1 IN V /\ ~(u=u1) ==> ~(collinear {vec 0, u, u1}))`,
 468 REWRITE_TAC[SET_RULE`u IN {v,w} <=> u=v \/ u=w`;convex_local_fan]
 469 THEN REPEAT STRIP_TAC
 470 THEN ASM_MESON_TAC[PROPERTIES_GENERIC_LOCAL_FAN;]);;
 471
 472
 473 let AZIM_PI_WEDGE_SIN = prove_by_refinement(` azim u v w ww = pi ==>
 474 wedge u v w ww = {x| &0 < sin (azim u v w x ) } `,
 475 [REWRITE_TAC[wedge; EXTENSION; IN_ELIM_THM]
 476 THEN ONCE_REWRITE_TAC[GSYM (SPEC ` -- (u:real^3) ` AZIM_TRANSLATION)]
 477 THEN REWRITE_TAC[VECTOR_ARITH` -- a + (a:real^N) = vec 0`;VECTOR_ARITH` -- a + b = b - a:real^N `; re_eqvl]
 478 THEN REPEAT STRIP_TAC
 479 THEN ASM_REWRITE_TAC[]
 480 THEN EQ_TAC;
 481 SIMP_TAC[SIN_POS_PI];
 482 MP_TAC (SPECL [`u - u:real^3 `;` v - u:real^3 `;` w - u:real^3 `;
 483 ` x - u:real^3 `] AZIM_RANGE)
 484 THEN STRIP_TAC
 485 THEN ABBREV_TAC ` goc = azim (u - u) (v - u) (w - u) (x - u) `
 486 THEN MP_TAC(REAL_ARITH`&0 <= goc==> goc= &0 \/ &0< goc `)
 487 THEN RESA_TAC;
 488 ASM_REWRITE_TAC[SIN_0]
 489 THEN REAL_ARITH_TAC;
 490 ASM_REWRITE_TAC[]
 491 THEN ASM_CASES_TAC `collinear {u, v, x:real^3}`;
 492 MRESA_TAC azim_def[`w:real^3`;`x:real^3`;`v:real^3`;`u:real^3`]
 493 THEN POP_ASSUM MP_TAC
 494 THEN ONCE_REWRITE_TAC[GSYM (SPEC ` -- (u:real^3) ` AZIM_TRANSLATION)]
 495 THEN REWRITE_TAC[VECTOR_ARITH` -- a + (a:real^N) = vec 0`;VECTOR_ARITH` -- a + b = b - a:real^N `; re_eqvl]
 496 THEN RESA_TAC
 497 THEN ASM_REWRITE_TAC[SIN_0]
 498 THEN REAL_ARITH_TAC;
 499 ASM_REWRITE_TAC[]
 500 THEN STRIP_TAC
 501 THEN ASM_CASES_TAC ` goc < pi `
 502 THEN ASM_REWRITE_TAC[]
 503 THEN SUBGOAL_THEN` sin goc < &0 ` MP_TAC;
 504 ONCE_REWRITE_TAC[SIN_SUB_PERIODIC]
 505 THEN REWRITE_TAC[REAL_ARITH` -- a < &0 <=> &0 < a `]
 506 THEN MATCH_MP_TAC SIN_POS_PI
 507 THEN
 508 ASM_REWRITE_TAC[REAL_ARITH` a - b < b <=> a < &2 * b `;REAL_ARITH` &0 < a - pi <=> ~( a < pi ) /\ ~(a= pi) `]
 509 THEN STRIP_TAC
 510 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th; SIN_PI])
 511 THEN REAL_ARITH_TAC;
 512 ASM_TAC THEN REAL_ARITH_TAC]);;
 513
 514
 515
 516
 517 let AZIM_PI_WEDGE_CROSS_DOT = prove_by_refinement(` azim u v w ww = pi ==>
 518 wedge u v w ww = {x | &0 < ((v - u) cross ( w - u )) dot ( x - u )}`,
 519 [SIMP_TAC[AZIM_PI_WEDGE_SIN; EXTENSION; IN_ELIM_THM];
 520 REPEAT STRIP_TAC;
 521 ONCE_REWRITE_TAC[GSYM (SPEC ` -- (u:real^3) ` AZIM_TRANSLATION)];
 522 REWRITE_TAC[VECTOR_ARITH` -- a + a:real^N = vec 0 `; VECTOR_ARITH` -- a + x = x - a:real^N `];
 523 MP_TAC (SPECL [` v - u:real^3 `;` w - u:real^3 `;` x - u:real^3 `] Trigonometry2.JBDNJJB);
 524 REWRITE_TAC[re_eqvl];
 525 STRIP_TAC;
 526 ASM_REWRITE_TAC[VECTOR_SUB_REFL];
 527 ASM_SIMP_TAC[REAL_LT_MUL_EQ]]);;
 528
 529
 530 let AFF_GT_SUBSET_WEDGE_IMP_VERTEX=prove(`!x v w y z. ~collinear{x,v,w}
 531 /\ ~collinear{x,v,y}
 532 /\ ~collinear{x,v,z}
 533 /\ aff_gt {x} {v,w} SUBSET wedge x v y z
 534 ==> w IN wedge x v y z`,
 535 REPEAT STRIP_TAC
 536 THEN MRESA_TAC Planarity.exists_in_aff_gt[`x:real^3`;`v:real^3`;`w:real^3`]
 537 THEN MP_TAC(SET_RULE`y' IN aff_gt {x} {v, w} /\ aff_gt {x:real^3} {v, w} SUBSET wedge x v y z ==> y' IN wedge x v y z`)
 538 THEN MRESA_TAC th3[`x:real^3`;`v:real^3`;`w:real^3`]
 539 THEN REWRITE_TAC[wedge;IN_ELIM_THM]
 540 THEN MRESA_TAC Planarity.aff_gt_inter_aff_gt[`x:real^3`;`v:real^3`;`w:real^3`]
 541 THEN UNDISCH_TAC`y' IN aff_gt {x} {v, w:real^3}`
 542 THEN ASM_REWRITE_TAC[INTER;IN_ELIM_THM]
 543 THEN STRIP_TAC
 544 THEN MRESA_TAC Planarity.aff_gt_imp_not_collinear[`x:real^3`;`w:real^3`;`v:real^3`;`y':real^3`]
 545 THEN MRESA_TAC AZIM_EQ[`x:real^3`;`v:real^3`;`y:real^3`;`w:real^3`;`y':real^3`]
 546 THEN RESA_TAC);;
 547
 548 let CONDITION_INANGLE_CROSS_DOT=prove(` aff_gt {x} {v,w} SUBSET wedge x v y z
 549 /\ ~collinear{x,v,w}
 550 /\ ~collinear{x,v,y}
 551 /\ ~collinear{x,v,z}
 552 /\ u= (v-x) cross (w-x)
 553 /\ azim x v y z<pi
 554 ==> &0 < ((v - x) cross (y - x)) dot (w - x)/\
 555 &0 < ((v - x) cross (w - x)) dot (z - x)`,
 556 REPEAT STRIP_TAC
 557 THEN MRESA_TAC (AFF_GT_SUBSET_WEDGE_IMP_VERTEX)[`x:real^3`;`v:real^3`;`w:real^3`;`y:real^3`;`z:real^3`]
 558 THEN POP_ASSUM MP_TAC
 559 THEN REWRITE_TAC[wedge;IN_ELIM_THM]
 560 THEN STRIP_TAC
 561 THEN MP_TAC(REAL_ARITH`azim x v y w < azim x v y z /\ azim x v y z < pi
 562 ==> azim x v y w < pi /\ azim x v y w <= azim x v y z`)
 563 THEN RESA_TAC
 564 THEN MRESA1_TAC SIN_POS_PI`azim x v y w`
 565 THEN POP_ASSUM MP_TAC
 566 THEN MRESA_TAC Fan.sum4_azim_fan[`x:real^3`;`v:real^3`;`y:real^3`;`w:real^3`;`z:real^3`]
 567 THEN MP_TAC(REAL_ARITH`azim x v y w < azim x v y z /\ &0< azim x v y w
 568 /\ azim x v y z < pi /\ azim x v y z = azim x v y w + azim x v w z
 569 ==> &0< azim x v w z /\ azim x v w z< pi`)
 570 THEN RESA_TAC
 571 THEN MRESA1_TAC SIN_POS_PI`azim x v w z`
 572 THEN POP_ASSUM MP_TAC
 573 THEN ONCE_REWRITE_TAC[GSYM (SPEC ` -- (x:real^3) ` AZIM_TRANSLATION)]
 574 THEN REWRITE_TAC[VECTOR_ARITH` -- a + (a:real^N) = vec 0`;VECTOR_ARITH` -- a + b = b - a:real^N `; re_eqvl]
 575 THEN MP_TAC (SPECL [` v - x:real^3 `;` w - x:real^3 `;` z - x:real^3 `] Trigonometry2.JBDNJJB)
 576 THEN REWRITE_TAC[re_eqvl;VECTOR_ARITH`a-a= vec 0`]
 577 THEN MP_TAC (SPECL [` v - x:real^3 `;` y - x:real^3 `;` w - x:real^3 `] Trigonometry2.JBDNJJB)
 578 THEN REWRITE_TAC[re_eqvl;]
 579 THEN RESA_TAC
 580 THEN RESA_TAC
 581 THEN REPEAT STRIP_TAC
 582 THEN MP_TAC REAL_LT_MUL_EQ
 583 THEN STRIP_TAC
 584 THEN REMOVE_ASSUM_TAC
 585 THEN POP_ASSUM(fun th-> MRESA_TAC th[`t:real`;`((v - x) cross (y - x)) dot (w - x:real^3)`] THEN MRESA_TAC th[`t':real`;`(((v - x) cross (w - x)) dot (z - x:real^3))`]));;
 586
 587 let AFF_GE_3_1 = prove
 588 (`!x v u w.
 589 DISJOINT {x,v,u} {w}
 590 ==> aff_ge {x,v,u} {w} =
 591 {y | ?t1 t2 t3 t4.
 592 &0 <= t4 /\
 593 t1 + t2 +t3 +t4 = &1 /\
 594 y = t1 % x + t2 % v + t3 % u +t4 % w }`,
 595 AFF_TAC);;
 596
 597
 598 let AFF_GE_2_2=prove(`!x u v w.
 599 DISJOINT {x, u} {v, w}
 600 ==> aff_ge {x, u} {v, w} =
 601 {y | ?t1 t2 t3 t4.
 602 &0 <= t3 /\
 603 &0 <= t4 /\
 604 t1 + t2 + t3 +t4= &1 /\
 605 y = t1 % x + t2 %u + t3 % v + t4 % w}`,
 606 AFF_TAC);;
 607
 608
 609
 610 let inter_aff_ge_3_1_is_aff_ge_2_2=prove(`!x v u w:real^3.
 611 ~coplanar {x,v,u,w}
 612 ==>
 613 aff_ge {x,v,u} {w} INTER aff_ge {x,u,w} {v} =aff_ge {x,u} {v,w}`,
 614 GEOM_ORIGIN_TAC `x:real^3`
 615 THEN REPEAT STRIP_TAC
 616 THEN MRESA_TAC notcoplanar_disjoints[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 617 THEN MRESA_TAC notcoplanar_disjoint[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 618 THEN MRESA_TAC AFF_GE_3_1[`(vec 0):real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 619 THEN MRESA_TAC AFF_GE_3_1[`(vec 0):real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
 620 THEN MRESA_TAC AFF_GE_2_2[`(vec 0):real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
 621 THEN MRESA_TAC NOT_COPLANAR_0_4_IMP_INDEPENDENT[`v:real^3`;`u:real^3`;`w:real^3`]
 622 THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM;INTER]
 623 THEN REDUCE_VECTOR_TAC
 624 THEN GEN_TAC
 625 THEN EQ_TAC
 626 THENL[
 627 STRIP_TAC
 628 THEN POP_ASSUM MP_TAC
 629 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`]
 630 THEN STRIP_TAC
 631 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`]
 632 THEN REPEAT STRIP_TAC
 633 THEN EXISTS_TAC`t1':real`
 634 THEN EXISTS_TAC`t2':real`
 635 THEN EXISTS_TAC`t4':real`
 636 THEN EXISTS_TAC`t3':real`
 637 THEN ASM_REWRITE_TAC[REAL_ARITH`t1+t2+t3+t4=t1+t2+t4+t3:real`;VECTOR_ARITH`t4' % v + t2' % u + t3' % w = t2' % u + t4' % v + t3' % w:real^3`]
 638 THEN ASM_TAC
 639 THEN REAL_ARITH_TAC;
 640 STRIP_TAC
 641 THEN STRIP_TAC
 642 THENL[
 643 EXISTS_TAC`t1:real`
 644 THEN EXISTS_TAC`t3:real`
 645 THEN EXISTS_TAC`t2:real`
 646 THEN EXISTS_TAC`t4:real`
 647 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t2 % u + t3 % v + t4 % w = t3 % v + t2 % u + t4 % w:real^3`;REAL_ARITH`t1 + t3 + t2 + t4=t1 + t2 + t3 + t4`];
 648 EXISTS_TAC`t1:real`
 649 THEN EXISTS_TAC`t2:real`
 650 THEN EXISTS_TAC`t4:real`
 651 THEN EXISTS_TAC`t3:real`
 652 THEN ASM_REWRITE_TAC[REAL_ARITH`t1 + t2 + t4+ t3:real=t1 + t2 + t3 + t4`]
 653 THEN VECTOR_ARITH_TAC]]);;
 654
 655
 656 let aff_ge_3_1_rep_cross_dot=prove(
 657 `!x:real^3 v:real^3 u:real^3 w:real^3.
 658 ~coplanar {x,v,u,w}
 659 /\ &0< ((v-x) cross (u-x)) dot (w-x)
 660 ==> aff_ge {x,v,u} {w} ={y:real^3| &0<= (((v-x) cross (u-x)) dot (y-x)) }`,
 661
 662 REPEAT STRIP_TAC
 663 THEN POP_ASSUM MP_TAC
 664 THEN MRESA_TAC notcoplanar_imp_notcollinear_fan[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 665 THEN MRESA_TAC notcoplanar_disjoints[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 666 THEN DISCH_THEN(LABEL_TAC"YEU")
 667 THEN MRESA_TAC AFF_GE_3_1[`x:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
 668 THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM]
 669 THEN GEN_TAC
 670 THEN EQ_TAC
 671 THENL[STRIP_TAC
 672 THEN ASM_REWRITE_TAC[VECTOR_ARITH`((t1 % x + t2 % v + t3 % u + t4 % w) - x)=((t1+t2+t3+t4) - &1) % x + t2 % (v-x) + t3 % (u-x) + t4 % (w - x)`; REAL_ARITH`&1- &1= &0`]
 673 THEN REDUCE_VECTOR_TAC
 674 THEN REWRITE_TAC[CROSS_LNEG;CROSS_LMUL;CROSS_LADD;CROSS_REFL;DOT_RMUL;DOT_RADD;DOT_CROSS_SELF;]
 675 THEN REDUCE_ARITH_TAC
 676 THEN MATCH_MP_TAC REAL_LE_MUL
 677 THEN ASM_REWRITE_TAC[]
 678 THEN ASM_TAC THEN REAL_ARITH_TAC;
 679 DISCH_THEN(LABEL_TAC"ME")
 680 THEN MP_TAC(ISPECL[`x:real^3`;`v:real^3`;`u:real^3`]properties_coordinate) THEN RESA_TAC
 681 THEN MRESA_TAC ORTHONORMAL_IMP_SPANNING[`e1_fan (x:real^3) (v:real^3) (u:real^3)`;`e2_fan (x:real^3)( v:real^3) (u:real^3)`;`e3_fan (x:real^3) (v:real^3) (u:real^3)`;]
 682 THEN POP_ASSUM MP_TAC
 683 THEN ASM_REWRITE_TAC[SPAN_3;EXTENSION]
 684 THEN DISCH_TAC THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(x':real^3)-(x:real^3)`th) THEN ASSUME_TAC(th))
 685 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(w:real^3)-(x:real^3)`th)THEN ASSUME_TAC(th))
 686 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(u:real^3)-(x:real^3)`th)THEN ASSUME_TAC(th))
 687 THEN POP_ASSUM(fun th-> MP_TAC(ISPEC`(v:real^3)-(x:real^3)`th))
 688 THEN REWRITE_TAC[SET_RULE`(a:real^3) IN (:real^3)`;IN_ELIM_THM;VECTOR_ARITH`A-B=C<=>A=C+B:real^3`]
 689 THEN REPEAT STRIP_TAC
 690 THEN ABBREV_TAC`e1=e1_fan x v u:real^3`
 691 THEN ABBREV_TAC`e2=e2_fan x v u:real^3`
 692 THEN ABBREV_TAC`e3=e3_fan x v u:real^3`
 693 THEN REMOVE_THEN"YEU" MP_TAC
 694 THEN MRESA_TAC ORTHONORMAL_CROSS[`e1:real^3`;`e2:real^3`;`e3:real^3`;]
 695 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1 % x +
 696 t2 % ((u' % e1 + v' % e2 + w' % e3) + x) +
 697 t3 % ((u'' % e1 + v'' % e2 + w'' % e3) + x) +
 698 t4 % ((u''' % e1 + v''' % e2 + w''' % e3) + x)
 699 = (t2 * u' + t3 * u'' +t4 * u''') % e1 + (t2 * v'+t3*v''+ t4 * v''') % e2 + (t2 * w'+ t3 * w''+ t4 * w''') % e3 +(t1+t2+t3+t4) % x :real^3`;VECTOR_ARITH`((u' % e1 + v' % e2 + w' % e3) + x) - x=u' % e1 + v' % e2 + w' % e3`;CROSS_LMUL;CROSS_RMUL;CROSS_LADD;CROSS_RADD;CROSS_REFL;]
 700 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
 701 THEN ASM_REWRITE_TAC[]
 702 THEN REDUCE_VECTOR_TAC
 703 THEN FIND_ASSUM MP_TAC`orthonormal e1 e2 (e3:real^3)`
 704 THEN REWRITE_TAC[orthonormal]
 705 THEN STRIP_TAC
 706 THEN ASM_REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL;DOT_RMUL;DOT_LNEG]
 707 THEN ONCE_REWRITE_TAC[DOT_SYM]
 708 THEN ASM_REWRITE_TAC[]
 709 THEN REDUCE_ARITH_TAC
 710 THEN ABBREV_TAC`a1=vector[u':real;u'':real;u''':real]:real^3`
 711 THEN ABBREV_TAC`a2=vector[v':real;v'':real;v''':real]:real^3`
 712 THEN ABBREV_TAC`a3=vector[w':real;w'':real;w''':real]:real^3`
 713 THEN ABBREV_TAC`A=vector[a1;a2;a3:real^3]:real^3^3`
 714 THEN ABBREV_TAC`b=vector[u'''':real;v'''':real;w'''':real]:real^3`
 715 THEN STRIP_TAC
 716 THEN SUBGOAL_THEN`&0< det(A:real^3^3)`ASSUME_TAC
 717 THENL[
 718 EXPAND_TAC"A"
 719 THEN EXPAND_TAC "a1"
 720 THEN EXPAND_TAC "a2"
 721 THEN EXPAND_TAC "a3"
 722 THEN REWRITE_TAC[DET_3;VECTOR_3]
 723 THEN POP_ASSUM MP_TAC
 724 THEN REAL_ARITH_TAC;
 725 MP_TAC(REAL_ARITH`&0< det (A:real^3^3)==> ~(det A= &0) /\ &0<= det (A:real^3^3)`) THEN RESA_TAC
 726 THEN MRESA_TAC CRAMER[`A:real^3^3`;]
 727 THEN POP_ASSUM MP_TAC
 728 THEN REWRITE_TAC[SWAP_FORALL_THM]
 729 THEN STRIP_TAC
 730 THEN POP_ASSUM(fun th-> MRESA_TAC th[`b:real^3`])
 731 THEN POP_ASSUM MP_TAC
 732 THEN REWRITE_TAC[MESON[]
 733 ` (!x. p(x) <=> x = a) <=> (?x. p(x)) /\ (!x. p(x) ==> x = a)`]
 734 THEN STRIP_TAC
 735 THEN POP_ASSUM MP_TAC
 736 THEN POP_ASSUM MP_TAC
 737 THEN DISCH_THEN(LABEL_TAC "LINH1")
 738 THEN DISCH_THEN(LABEL_TAC "LINH2")
 739 THEN REMOVE_THEN "LINH1" MP_TAC
 740 THEN MRESAL_TAC MATRIX_VECTOR_MUL_COMPONENT[`A:real^3^3`;`x'':real^3`][DIMINDEX_3]
 741 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1:num`[ARITH_RULE`1<=1/\ 1<=3`;LAMBDA_BETA;VECTOR_3] THEN ASSUME_TAC th)
 742 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`2:num`[ARITH_RULE`1<=2/\ 2<=3`;VECTOR_3] THEN ASSUME_TAC th)
 743 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`1<=3/\ 3<=3`;VECTOR_3;])
 744 THEN DISCH_TAC
 745 THEN POP_ASSUM(fun th -> MP_TAC th THEN ASSUME_TAC th)
 746 THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[VECTOR_3;CART_EQ;]
 747 THEN REWRITE_TAC[DIMINDEX_3]
 748 THEN STRIP_TAC
 749 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1:num`[ARITH_RULE`1<=1/\ 1<=3`;DOT_SYM;] THEN ASSUME_TAC th)
 750 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`2:num`[ARITH_RULE`1<=2/\ 2<=3`;DOT_SYM;] THEN ASSUME_TAC th)
 751 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`1<=3/\ 3<=3`;DOT_SYM;])
 752 THEN POP_ASSUM MP_TAC
 753 THEN POP_ASSUM MP_TAC
 754 THEN POP_ASSUM MP_TAC
 755 THEN POP_ASSUM MP_TAC
 756 THEN EXPAND_TAC"A"
 757 THEN EXPAND_TAC "a1"
 758 THEN EXPAND_TAC "a2"
 759 THEN EXPAND_TAC "a3"
 760 THEN EXPAND_TAC "b"
 761 THEN REWRITE_TAC[VECTOR_3;DOT_3]
 762 THEN DISCH_THEN(LABEL_TAC"MA")
 763 THEN REPEAT STRIP_TAC
 764 THEN EXISTS_TAC`&1- (x'':real^3)$1 - x''$2 -x''$3`
 765 THEN EXISTS_TAC`(x'':real^3)$1`
 766 THEN EXISTS_TAC`(x'':real^3)$2`
 767 THEN EXISTS_TAC`(x'':real^3)$3`
 768 THEN ASM_REWRITE_TAC[REAL_ARITH` &1 - x''$1 - x''$2 - x''$3 + x''$1 + x''$2 + x''$3= &1`;VECTOR_ARITH`(u'''' % e1 + v'''' % e2 + w'''' % e3) + x =
 769 u'''' % e1 + v'''' % e2 + w'''' % e3 + &1 % x`]
 770 THEN REMOVE_THEN "MA" MP_TAC
 771 THEN RESA_TAC
 772 THEN MRESAL_TAC CRAMER_LEMMA1[`A:real^3^3`;`x'':real^3`;`3`][ARITH_RULE`1<=3/\ 3<=3`;DIMINDEX_3;]
 773 THEN POP_ASSUM MP_TAC
 774 THEN REMOVE_ASSUM_TAC
 775 THEN DISCH_THEN(LABEL_TAC"LINH3")
 776 THEN ABBREV_TAC`b1=vector[u':real;u'':real;u'''':real]:real^3`
 777 THEN ABBREV_TAC`b2=vector[v':real;v'':real;v'''':real]:real^3`
 778 THEN ABBREV_TAC`b3=vector[w':real;w'':real;w'''':real]:real^3`
 779 THEN ABBREV_TAC`B=vector[b1;b2;b3:real^3]:real^3^3`
 780 THEN SUBGOAL_THEN`(lambda i j. if j = 3 then (b:real^3)$i else (A:real^3^3)$i$j):real^3^3=B` ASSUME_TAC
 781
 782 THENL[
 783 ONCE_ASM_SIMP_TAC[CART_EQ;]
 784 THEN ONCE_ASM_SIMP_TAC[CART_EQ;]
 785 THEN ASM_SIMP_TAC[LAMBDA_BETA;DIMINDEX_3]
 786 THEN REPEAT STRIP_TAC
 787 THEN COND_CASES_TAC
 788 THEN ASM_REWRITE_TAC[]
 789 THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 3==> i=1 \/ i=2 \/ i=3`)
 790 THEN RESA_TAC
 791 THEN EXPAND_TAC"B"
 792 THEN EXPAND_TAC "b1"
 793 THEN EXPAND_TAC "b2"
 794 THEN EXPAND_TAC "b3"
 795 THEN EXPAND_TAC "b"
 796 THEN MP_TAC(ARITH_RULE`1<=i' /\ i'<= 3/\ ~(i'=3)==> i'=1 \/ i'=2`)
 797 THEN EXPAND_TAC "A"
 798 THEN REWRITE_TAC[VECTOR_3]
 799 THEN RESA_TAC
 800 THEN EXPAND_TAC "b1"
 801 THEN EXPAND_TAC "b2"
 802 THEN EXPAND_TAC "b3"
 803 THEN EXPAND_TAC "a3"
 804 THEN EXPAND_TAC "a1"
 805 THEN EXPAND_TAC "a2"
 806 THEN REWRITE_TAC[VECTOR_3];
 807 REMOVE_THEN"LINH3" MP_TAC
 808 THEN ASM_REWRITE_TAC[]
 809 THEN REMOVE_ASSUM_TAC
 810 THEN STRIP_TAC
 811 THEN SUBGOAL_THEN`&0<= det(B:real^3^3)`ASSUME_TAC
 812 THENL[REMOVE_ASSUM_TAC
 813 THEN EXPAND_TAC"B"
 814 THEN EXPAND_TAC "b1"
 815 THEN EXPAND_TAC "b2"
 816 THEN EXPAND_TAC "b3"
 817 THEN REWRITE_TAC[DET_3;VECTOR_3]
 818 THEN REMOVE_THEN "ME" MP_TAC
 819 THEN ASM_REWRITE_TAC[VECTOR_ARITH`((u' % e1 + v' % e2 + w' % e3) + x) - x=u' % e1 + v' % e2 + w' % e3`;CROSS_LMUL;CROSS_RMUL;CROSS_LADD;CROSS_RADD;CROSS_REFL;]
 820 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
 821 THEN ASM_REWRITE_TAC[]
 822 THEN REDUCE_VECTOR_TAC
 823 THEN ASM_REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL;DOT_RMUL;DOT_LNEG]
 824 THEN ONCE_REWRITE_TAC[DOT_SYM]
 825 THEN ASM_REWRITE_TAC[]
 826 THEN REDUCE_ARITH_TAC
 827 THEN REAL_ARITH_TAC;
 828 POP_ASSUM MP_TAC
 829 THEN RESA_TAC
 830 THEN MRESA1_TAC REAL_LE_INV`det (A:real^3^3)`
 831 THEN MRESA1_TAC REAL_MUL_LINV`det (A:real^3^3)`
 832 THEN MRESAL_TAC REAL_LE_MUL[`inv(det(A:real^3^3))`;`(x'':real^3)$3 * det(A:real^3^3)`][REAL_ARITH`A*(B*C)=(A*C)*B`;REAL_ARITH`&1*A=A`]]]]]);;
 833
 834
 835
 836 let PROPERTIES_AFF_GT_SUBSET_WEDGE=prove_by_refinement(`convex_local_fan (V,E,FF) /\ v IN V /\ w IN V /\ ~(v=w)/\ generic V E
 837 /\ azim_in_fan (v, rho_node1 FF v) E < pi
 838 /\ aff_gt {vec 0} {v,w} SUBSET wedge_in_fan_gt (v, rho_node1 FF v) E
 839 ==>
 840 (!x. x IN FF ==>
 841 aff_gt {vec 0} {v,w} SUBSET wedge_in_fan_gt x E)`,
 842 let lemma=prove(`!A. A \/ ~A`, SET_TAC[])
 843 in
 844 [
 845 REWRITE_TAC[convex_local_fan;wedge_in_fan_gt]
 846 THEN STRIP_TAC
 847 THEN POP_ASSUM MP_TAC
 848 THEN NHANH (ARITH_RULE` a = 2 ==> a > 1 `)
 849 THEN MRESAL_TAC (GEN_ALL LOFA_CARD_EE_V_1)[`FF:real^3#real^3->bool`;`V:real^3->bool`;`v:real^3`;`E:(real^3->bool)->bool`;][ARITH_RULE`2>1`]
 850 THEN REPEAT STRIP_TAC
 851 THEN SUBGOAL_THEN ` FST (x:real^3 # real^3) IN V /\ SND x IN V ` MP_TAC;
 852 MATCH_MP_TAC LOCAL_FAN_IMP_IN_V
 853 THEN ASM_REWRITE_TAC[];
 854 STRIP_TAC
 855 THEN ONCE_REWRITE_TAC[GSYM PAIR]
 856 THEN REWRITE_TAC[wedge_in_fan_gt;]
 857 THEN MRESAL_TAC (GEN_ALL LOFA_CARD_EE_V_1)[`FF:real^3#real^3->bool`;`V:real^3->bool`;`FST (x:real^3#real^3)`;`E:(real^3->bool)->bool`;][ARITH_RULE`2>1`]
 858 THEN MRESAL_TAC (GEN_ALL PGSQVBL)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`w:real^3`;`x:real^3#real^3`;`E:(real^3->bool)->bool`][convex_local_fan;SET_RULE`{a,b} SUBSET V<=> a IN V /\ b IN V`]
 859 THEN POP_ASSUM MP_TAC
 860 THEN UNDISCH_TAC`!x:real^3#real^3. x IN FF ==> azim_in_fan x E <= pi /\ V SUBSET wedge_in_fan_ge x E`
 861 THEN STRIP_TAC
 862 THEN POP_ASSUM(fun th-> MRESA1_TAC th `x:real^3#real^3` THEN POP_ASSUM MP_TAC
 863 THEN POP_ASSUM MP_TAC THEN ASSUME_TAC th)
 864 THEN ONCE_REWRITE_TAC[GSYM PAIR]
 865 THEN REWRITE_TAC[wedge_in_fan_ge;azim_in_fan]
 866 THEN ASM_REWRITE_TAC[ARITH_RULE`2>1`]
 867 THEN LET_TAC
 868 THEN STRIP_TAC
 869 THEN MRESA_TAC PROPERTIES_GENERIC_LOCAL_FAN[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`]
 870 THEN POP_ASSUM (fun th-> MRESA1_TAC th`w:real^3`)
 871 THEN MP_TAC(REAL_ARITH`azim (vec 0) (FST x) (SND x) d <= pi==> azim (vec 0) (FST x) (SND x) d = pi \/ azim (vec 0) (FST x) (SND x) d < pi`)
 872 THEN RESA_TAC;
 873 MRESA_TAC (GEN_ALL AZIM_PI_WEDGE_GE_CROSS_DOT)[`d:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`;`vec 0:real^3`]
 874 THEN MRESA_TAC (GEN_ALL AZIM_PI_WEDGE_CROSS_DOT)[`d:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`;`vec 0:real^3`]
 875 THEN REWRITE_TAC[VECTOR_ARITH`a- vec 0=a`]
 876 THEN REPEAT STRIP_TAC
 877 THEN MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`w:real^3`]
 878 THEN MRESAL_TAC AFF_GT_1_2[`vec 0:real^3`;`v:real^3`;`w:real^3`][IN_ELIM_THM;SUBSET]
 879 THEN REPEAT STRIP_TAC
 880 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t % vec 0 +a=a`;DOT_RADD;DOT_RMUL]
 881 THEN MATCH_MP_TAC(REAL_ARITH`!A B. (&0< A /\ &0<= B)\/(&0<= A/\ &0< B)==> &0< A+B`)
 882 THEN MP_TAC REAL_LT_MUL_EQ
 883 THEN STRIP_TAC
 884 THEN REMOVE_ASSUM_TAC
 885 THEN POP_ASSUM(fun th-> MRESA_TAC th[`t2:real`;`((FST x cross SND x) dot v:real^3)`] THEN MRESA_TAC th[`t3:real`;`((FST x cross SND x) dot w:real^3)`])
 886 THEN MP_TAC REAL_LE_MUL_EQ
 887 THEN STRIP_TAC
 888 THEN REMOVE_ASSUM_TAC
 889 THEN POP_ASSUM(fun th-> MRESA_TAC th[`t2:real`;`((FST x cross SND x) dot v:real^3)`] THEN MRESA_TAC th[`t3:real`;`((FST x cross SND x) dot w:real^3)`])
 890 THEN MP_TAC(SET_RULE`V SUBSET {x' | &0 <= (FST x cross SND x) dot (x':real^3)} /\ v IN V
 891 /\ w IN V
 892 ==> &0<= (FST x cross SND x) dot w /\ &0<= (FST x cross SND x) dot v`)
 893 THEN RESA_TAC
 894 THEN ONCE_REWRITE_TAC[SET_RULE`A\/ B<=> ~(~A /\ ~ B)`]
 895 THEN STRIP_TAC
 896 THEN MP_TAC(REAL_ARITH`&0 <= (FST x cross SND x) dot w /\ &0 <= (FST x cross SND x) dot v /\ ~(&0 < (FST x cross SND x) dot v) /\ ~(&0 < (FST x cross SND x) dot w)
 897 ==> (FST x cross SND x) dot v= &0 /\
 898 (FST x cross SND x) dot w = &0`)
 899 THEN RESA_TAC
 900 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2
 901 THEN ASSUME_TAC2 EXISTS_INVERSE_OF_V
 902 THEN DOWN THEN STRIP_TAC
 903 THEN ASSUME_TAC2 LOFA_IMP_EE_TWO_ELMS
 904 THEN ASSUME_TAC2 LOFA_CARD_EE_V_1
 905 THEN UNDISCH_TAC ` azim_in_fan (v:real^3, rho_node1 FF v) E < pi`
 906 THEN UNDISCH_TAC`aff_gt {vec 0} {v, w:real^3} SUBSET
 907 wedge (vec 0) v (rho_node1 FF v)
 908 (azim_cycle (EE v E) (vec 0) v (rho_node1 FF v))`
 909 THEN ASM_REWRITE_TAC[azim_in_fan;ARITH_RULE`2>1`;Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]
 910 THEN LET_TAC
 911 THEN STRIP_TAC
 912 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`d':real^3`]
 913 THEN POP_ASSUM MP_TAC
 914 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 915 THEN STRIP_TAC THEN STRIP_TAC
 916 THEN MRESAL_TAC (GEN_ALL CONDITION_INANGLE_CROSS_DOT)[`v cross w:real^3`;`(rho_node1 FF v:real^3)`;`v:real^3`;`w:real^3`;`d':real^3`;`vec 0:real^3`][VECTOR_ARITH`a- vec 0=a`]
 917 THEN UNDISCH_TAC`&0 < (v cross rho_node1 FF v) dot w`
 918 THEN REWRITE_TAC[]
 919 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
 920 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
 921 THEN REPEAT STRIP_TAC
 922 THEN ASSUME_TAC2 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V
 923 THEN MP_TAC(SET_RULE`V SUBSET {x':real^3 | &0 <= (FST x cross SND x) dot x'}
 924 /\ d' IN V /\ rho_node1 FF v IN V==> &0 <= (FST x cross SND x) dot d'
 925 /\ &0 <= (FST x cross SND x) dot (rho_node1 FF v)`)
 926 THEN RESA_TAC
 927 THEN MRESAL_TAC DOT_CROSS[`(FST x cross (SND x):real^3)`;`v cross w:real^3`;`(rho_node1 FF v)`;`d':real^3`][CROSS_LAGRANGE;
 928 VECTOR_ARITH`&0 % v - &0 % w= vec 0`;DOT_LZERO; REAL_ARITH`&0=A-B<=> A=B`]
 929 THEN MP_TAC(REAL_ARITH`&0 < (v cross w) dot (d':real^3)==> &0 <= (v cross w) dot d'`)
 930 THEN RESA_TAC
 931 THEN MRESAL_TAC CROSS_CROSS_DET[`FST (x:real^3#real^3)`;`(SND (x:real^3#real^3)):real^3`;`v:real^3`;`w:real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
 932 THEN MP_TAC(REAL_ARITH`&0 <= (FST x cross SND x) dot rho_node1 FF v
 933 ==> (FST x cross SND x) dot rho_node1 FF v= &0 \/ &0 < (FST x cross SND x) dot rho_node1 FF v`)
 934 THEN RESA_TAC;
 935 MRESAL_TAC CROSS_CROSS_DET[`FST (x:real^3#real^3)`;`(SND (x:real^3#real^3)):real^3`;`v:real^3`;`rho_node1 FF v:real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
 936 THEN MRESAL_TAC DOT_CROSS[`(FST x cross (SND x):real^3)`;`v cross (rho_node1 FF v)`;`(FST x cross SND x):real^3`;`w:real^3`][CROSS_LAGRANGE;DOT_LZERO; REAL_ARITH`&0=B- &0*A<=> B= &0`; REAL_ENTIRE;DOT_EQ_0];
 937 POP_ASSUM MP_TAC
 938 THEN REWRITE_TAC[CROSS_EQ_0]
 939 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;` (x:real^3#real^3)`];
 940 POP_ASSUM MP_TAC
 941 THEN REWRITE_TAC[]
 942 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
 943 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
 944 THEN ASM_TAC
 945 THEN REAL_ARITH_TAC;
 946 MP_TAC(REAL_ARITH`&0 <= (FST x cross SND x) dot (d':real^3)
 947 ==> (FST x cross SND x) dot (d':real^3)= &0 \/ &0 < (FST x cross SND x) dot (d':real^3)`)
 948 THEN RESA_TAC;
 949 MRESAL_TAC CROSS_CROSS_DET[`FST (x:real^3#real^3)`;`(SND (x:real^3#real^3)):real^3`;`v:real^3`;`d':real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
 950 THEN MRESAL_TAC DOT_CROSS[`(FST x cross (SND x):real^3)`;`v cross (d':real^3)`;`(FST x cross SND x):real^3`;`w:real^3`][CROSS_LAGRANGE;DOT_LZERO; REAL_ARITH`&0=B- &0*A<=> B= &0`; REAL_ENTIRE;DOT_EQ_0];
 951 POP_ASSUM MP_TAC
 952 THEN REWRITE_TAC[CROSS_EQ_0]
 953 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;` (x:real^3#real^3)`];
 954 POP_ASSUM MP_TAC
 955 THEN REWRITE_TAC[]
 956 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
 957 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
 958 THEN ONCE_REWRITE_TAC[CROSS_SKEW;]
 959 THEN REWRITE_TAC[ DOT_LNEG]
 960 THEN ASM_TAC
 961 THEN REAL_ARITH_TAC;
 962 MRESA_TAC REAL_LT_MUL[`(FST x cross SND x) dot rho_node1 FF v`;`((v cross w) dot (d':real^3))`]
 963 THEN MP_TAC REAL_LT_MUL_EQ
 964 THEN STRIP_TAC
 965 THEN REMOVE_ASSUM_TAC
 966 THEN POP_ASSUM(fun th-> MRESA_TAC th[`(FST x cross SND x) dot (d':real^3)`;`(v cross w) dot (rho_node1 FF v:real^3)`] )
 967 THEN POP_ASSUM MP_TAC
 968 THEN REWRITE_TAC[]
 969 THEN ONCE_REWRITE_TAC[CROSS_SKEW;]
 970 THEN REWRITE_TAC[ DOT_LNEG]
 971 THEN ASM_TAC
 972 THEN REAL_ARITH_TAC;
 973 MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;` (x:real^3#real^3)`]
 974 THEN MRESA_TAC(GEN_ALL EXISTS_INVERSE_OF_V)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`FST (x:real^3#real^3)`]
 975 THEN MRESA_TAC (GEN_ALL LOFA_IMP_EE_TWO_ELMS)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;` FST(x:real^3#real^3)`;`vv:real^3`]
 976 THEN UNDISCH_TAC`azim_cycle (EE (FST x) E) (vec 0) (FST x) (SND x) = d:real^3`
 977 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_RHO_NODE_PROS
 978 THEN POP_ASSUM MP_TAC THEN RESA_TAC
 979 THEN POP_ASSUM(fun th-> MRESA1_TAC th`x:real^3#real^3`)
 980 THEN SUBGOAL_THEN`rho_node1 FF (FST x)= SND x` ASSUME_TAC;
 981 POP_ASSUM (fun th-> ONCE_REWRITE_TAC[th])
 982 THEN SET_TAC[];
 983 ASM_REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]
 984 THEN STRIP_TAC
 985 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`vv:real^3`]
 986 THEN POP_ASSUM MP_TAC
 987 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 988 THEN STRIP_TAC
 989 THEN MRESA_TAC (GEN_ALL Local_lemmas.WEDGE_GE_EQ_AFF_GE)[`vec 0:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`;`d:real^3`]
 990 THEN MRESA_TAC (GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`FST (x:real^3#real^3)`]
 991 THEN POP_ASSUM MP_TAC
 992 THEN MRESAL_TAC( GEN_ALL CONVEX_LOFA_IMP_INANGLE_EQ_AZIM) [`V:real^3->bool`;`FF:real^3#real^3->bool`;`E:(real^3->bool)->bool`][convex_local_fan]
 993 THEN POP_ASSUM(fun th-> MRESAL1_TAC th `FST (x:real^3#real^3)`[azim_in_fan;Local_lemmas.AZIM_CYCLE_TWO_POINT_SET; ARITH_RULE`2>1`])
 994 THEN LET_TAC
 995 THEN STRIP_TAC
 996 THEN MP_TAC(REAL_ARITH`&0 < azim (vec 0) (FST x) (SND x) d /\ azim (vec 0) (FST x) (SND x) d< pi ==> ~( azim (vec 0) (FST x) (SND x) d= &0 \/ azim (vec 0) (FST x) (SND x) d= pi)`)
 997 THEN RESA_TAC
 998 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`;`d:real^3`]
 999 THEN MRESA_TAC WEDGE_LUNE[`vec 0:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`;`d:real^3`]
1000 THEN MRESA_TAC inter_aff_gt_3_1_is_aff_gt_2_2[`vec 0:real^3`;`SND (x:real^3#real^3)`; `FST (x:real^3#real^3)`;`d:real^3`]
1001 THEN POP_ASSUM MP_TAC
1002 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
1003 THEN RESA_TAC
1004 THEN MRESA_TAC inter_aff_ge_3_1_is_aff_ge_2_2[`vec 0:real^3`;`SND (x:real^3#real^3)`; `FST (x:real^3#real^3)`;`d:real^3`]
1005 THEN POP_ASSUM MP_TAC
1006 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
1007 THEN RESA_TAC
1008 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1009 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;SET_RULE`A SUBSET B INTER C<=> A SUBSET B /\ A SUBSET C`])
1010 THEN MRESA1_TAC SIN_POS_PI`azim (vec 0) (FST x) (SND x) d`
1011 THEN POP_ASSUM MP_TAC
1012 THEN MP_TAC (SPECL [` FST(x:real^3#real^3) `;` SND (x:real^3#real^3) `;` d:real^3 `] Trigonometry2.JBDNJJB)
1013 THEN REWRITE_TAC[re_eqvl;]
1014 THEN RESA_TAC
1015 THEN MP_TAC REAL_LT_MUL_EQ
1016 THEN STRIP_TAC
1017 THEN REMOVE_ASSUM_TAC
1018 THEN POP_ASSUM(fun th-> MRESA_TAC th[`t:real`;`((FST x cross SND (x:real^3#real^3)) dot d)`] )
1019 THEN REMOVE_ASSUM_TAC
1020 THEN REMOVE_ASSUM_TAC
1021 THEN REMOVE_ASSUM_TAC
1022 THEN STRIP_TAC
1023 THEN MRESAL_TAC aff_ge_3_1_rep_cross_dot[`vec 0:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`;`d:real^3`][VECTOR_ARITH`a- vec 0=a`]
1024 THEN MRESAL_TAC aff_gt_3_1_rep_cross_dot[`vec 0:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`;`d:real^3`][VECTOR_ARITH`a- vec 0=a`]
1025 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1026 THEN ASM_REWRITE_TAC[]
1027 THEN MRESAL_TAC aff_ge_3_1_rep_cross_dot[`vec 0:real^3`;`d:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`][VECTOR_ARITH`a- vec 0=a`]
1028 THEN MRESAL_TAC aff_gt_3_1_rep_cross_dot[`vec 0:real^3`;`d:real^3`;`FST (x:real^3#real^3)`;`SND (x:real^3#real^3)`][VECTOR_ARITH`a- vec 0=a`]
1029 THEN POP_ASSUM MP_TAC
1030 THEN POP_ASSUM MP_TAC
1031 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
1032 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1033 THEN RESA_TAC
1034 THEN RESA_TAC
1035 THEN ONCE_REWRITE_TAC[GSYM CROSS_TRIPLE]
1036 THEN REPEAT STRIP_TAC;
1037 MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`w:real^3`]
1038 THEN MRESAL_TAC AFF_GT_1_2[`vec 0:real^3`;`v:real^3`;`w:real^3`][IN_ELIM_THM;SUBSET]
1039 THEN REPEAT STRIP_TAC
1040 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t % vec 0 +a=a`;DOT_RADD;DOT_RMUL]
1041 THEN MATCH_MP_TAC(REAL_ARITH`!A B. (&0< A /\ &0<= B)\/(&0<= A/\ &0< B)==> &0< A+B`)
1042 THEN MP_TAC REAL_LT_MUL_EQ
1043 THEN STRIP_TAC
1044 THEN REMOVE_ASSUM_TAC
1045 THEN POP_ASSUM(fun th-> MRESA_TAC th[`t2:real`;`((FST x cross SND x) dot v:real^3)`] THEN MRESA_TAC th[`t3:real`;`((FST x cross SND x) dot w:real^3)`])
1046 THEN MP_TAC REAL_LE_MUL_EQ
1047 THEN STRIP_TAC
1048 THEN REMOVE_ASSUM_TAC
1049 THEN POP_ASSUM(fun th-> MRESA_TAC th[`t2:real`;`((FST x cross SND x) dot v:real^3)`] THEN MRESA_TAC th[`t3:real`;`((FST x cross SND x) dot w:real^3)`])
1050 THEN MP_TAC(SET_RULE`V SUBSET {x' | &0 <= (FST x cross SND x) dot (x':real^3)} /\ v IN V
1051 /\ w IN V
1052 ==> &0<= (FST x cross SND x) dot w /\ &0<= (FST x cross SND x) dot v`)
1053 THEN RESA_TAC
1054 THEN ONCE_REWRITE_TAC[SET_RULE`A\/ B<=> ~(~A /\ ~ B)`]
1055 THEN STRIP_TAC
1056 THEN MP_TAC(REAL_ARITH`&0 <= (FST x cross SND x) dot w /\ &0 <= (FST x cross SND x) dot v /\ ~(&0 < (FST x cross SND x) dot v) /\ ~(&0 < (FST x cross SND x) dot w)
1057 ==> (FST x cross SND x) dot v= &0 /\
1058 (FST x cross SND x) dot w = &0`)
1059 THEN RESA_TAC
1060 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2
1061 THEN ASSUME_TAC2 EXISTS_INVERSE_OF_V
1062 THEN DOWN THEN STRIP_TAC
1063 THEN MRESA_TAC (GEN_ALL LOFA_IMP_EE_TWO_ELMS)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`vv':real^3`]
1064 THEN ASSUME_TAC2 LOFA_CARD_EE_V_1
1065 THEN UNDISCH_TAC ` azim_in_fan (v:real^3, rho_node1 FF v) E < pi`
1066 THEN UNDISCH_TAC`aff_gt {vec 0} {v, w:real^3} SUBSET
1067 wedge (vec 0) v (rho_node1 FF v)
1068 (azim_cycle (EE v E) (vec 0) v (rho_node1 FF v))`
1069 THEN ASM_REWRITE_TAC[azim_in_fan;ARITH_RULE`2>1`;Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]
1070 THEN LET_TAC
1071 THEN STRIP_TAC
1072 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`d':real^3`]
1073 THEN POP_ASSUM MP_TAC
1074 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1075 THEN STRIP_TAC THEN STRIP_TAC
1076 THEN MRESAL_TAC (GEN_ALL CONDITION_INANGLE_CROSS_DOT)[`v cross w:real^3`;`(rho_node1 FF v:real^3)`;`v:real^3`;`w:real^3`;`d':real^3`;`vec 0:real^3`][VECTOR_ARITH`a- vec 0=a`]
1077 THEN UNDISCH_TAC`&0 < (v cross rho_node1 FF v) dot w`
1078 THEN REWRITE_TAC[]
1079 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1080 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1081 THEN REPEAT STRIP_TAC
1082 THEN ASSUME_TAC2 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V
1083 THEN MP_TAC(SET_RULE`V SUBSET {x':real^3 | &0 <= (FST x cross SND x) dot x'}
1084 /\ d' IN V /\ rho_node1 FF v IN V==> &0 <= (FST x cross SND x) dot d'
1085 /\ &0 <= (FST x cross SND x) dot (rho_node1 FF v)`)
1086 THEN RESA_TAC
1087 THEN MRESAL_TAC DOT_CROSS[`(FST x cross (SND x):real^3)`;`v cross w:real^3`;`(rho_node1 FF v)`;`d':real^3`][CROSS_LAGRANGE;
1088 VECTOR_ARITH`&0 % v - &0 % w= vec 0`;DOT_LZERO; REAL_ARITH`&0=A-B<=> A=B`]
1089 THEN MP_TAC(REAL_ARITH`&0 < (v cross w) dot (d':real^3)==> &0 <= (v cross w) dot d'`)
1090 THEN RESA_TAC
1091 THEN MRESAL_TAC CROSS_CROSS_DET[`FST (x:real^3#real^3)`;`(SND (x:real^3#real^3)):real^3`;`v:real^3`;`w:real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
1092 THEN MP_TAC(REAL_ARITH`&0 <= (FST x cross SND x) dot rho_node1 FF v
1093 ==> (FST x cross SND x) dot rho_node1 FF v= &0 \/ &0 < (FST x cross SND x) dot rho_node1 FF v`)
1094 THEN RESA_TAC;
1095 MRESAL_TAC CROSS_CROSS_DET[`FST (x:real^3#real^3)`;`(SND (x:real^3#real^3)):real^3`;`v:real^3`;`rho_node1 FF v:real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
1096 THEN MRESAL_TAC DOT_CROSS[`(FST x cross (SND x):real^3)`;`v cross (rho_node1 FF v)`;`(FST x cross SND x):real^3`;`w:real^3`][CROSS_LAGRANGE;DOT_LZERO; REAL_ARITH`&0=B- &0*A<=> B= &0`; REAL_ENTIRE;DOT_EQ_0];
1097 POP_ASSUM MP_TAC
1098 THEN REWRITE_TAC[CROSS_EQ_0]
1099 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;` (x:real^3#real^3)`];
1100 POP_ASSUM MP_TAC
1101 THEN REWRITE_TAC[]
1102 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1103 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1104 THEN ASM_TAC
1105 THEN REAL_ARITH_TAC;
1106 MP_TAC(REAL_ARITH`&0 <= (FST x cross SND x) dot (d':real^3)
1107 ==> (FST x cross SND x) dot (d':real^3)= &0 \/ &0 < (FST x cross SND x) dot (d':real^3)`)
1108 THEN RESA_TAC;
1109 MRESAL_TAC CROSS_CROSS_DET[`FST (x:real^3#real^3)`;`(SND (x:real^3#real^3)):real^3`;`v:real^3`;`d':real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
1110 THEN MRESAL_TAC DOT_CROSS[`(FST x cross (SND x):real^3)`;`v cross (d':real^3)`;`(FST x cross SND x):real^3`;`w:real^3`][CROSS_LAGRANGE;DOT_LZERO; REAL_ARITH`&0=B- &0*A<=> B= &0`; REAL_ENTIRE;DOT_EQ_0];
1111 POP_ASSUM MP_TAC
1112 THEN REWRITE_TAC[CROSS_EQ_0]
1113 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;` (x:real^3#real^3)`];
1114 POP_ASSUM MP_TAC
1115 THEN REWRITE_TAC[]
1116 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1117 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1118 THEN ONCE_REWRITE_TAC[CROSS_SKEW;]
1119 THEN REWRITE_TAC[ DOT_LNEG]
1120 THEN ASM_TAC
1121 THEN REAL_ARITH_TAC;
1122 MRESA_TAC REAL_LT_MUL[`(FST x cross SND x) dot rho_node1 FF v`;`((v cross w) dot (d':real^3))`]
1123 THEN MP_TAC REAL_LT_MUL_EQ
1124 THEN STRIP_TAC
1125 THEN REMOVE_ASSUM_TAC
1126 THEN POP_ASSUM(fun th-> MRESA_TAC th[`(FST x cross SND x) dot (d':real^3)`;`(v cross w) dot (rho_node1 FF v:real^3)`] )
1127 THEN POP_ASSUM MP_TAC
1128 THEN REWRITE_TAC[]
1129 THEN ONCE_REWRITE_TAC[CROSS_SKEW;]
1130 THEN REWRITE_TAC[ DOT_LNEG]
1131 THEN ASM_TAC
1132 THEN REAL_ARITH_TAC;
1133 MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`w:real^3`]
1134 THEN MRESAL_TAC AFF_GT_1_2[`vec 0:real^3`;`v:real^3`;`w:real^3`][IN_ELIM_THM;SUBSET]
1135 THEN REPEAT STRIP_TAC
1136 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t % vec 0 +a=a`;DOT_RADD;DOT_RMUL]
1137 THEN MATCH_MP_TAC(REAL_ARITH`!A B. (&0< A /\ &0<= B)\/(&0<= A/\ &0< B)==> &0< A+B`)
1138 THEN MP_TAC REAL_LT_MUL_EQ
1139 THEN STRIP_TAC
1140 THEN REMOVE_ASSUM_TAC
1141 THEN POP_ASSUM(fun th-> MRESA_TAC th[`t2:real`;`((d cross FST (x:real^3#real^3)) dot v:real^3)`] THEN MRESA_TAC th[`t3:real`;`((d cross FST (x:real^3#real^3)) dot w:real^3)`])
1142 THEN MP_TAC REAL_LE_MUL_EQ
1143 THEN STRIP_TAC
1144 THEN REMOVE_ASSUM_TAC
1145 THEN POP_ASSUM(fun th-> MRESA_TAC th[`t2:real`;`((d cross FST (x:real^3#real^3)) dot v:real^3)`] THEN MRESA_TAC th[`t3:real`;`((d cross FST (x:real^3#real^3)) dot w:real^3)`])
1146 THEN MP_TAC(SET_RULE`V SUBSET {y | &0 <= (d cross FST (x:real^3#real^3)) dot (y:real^3)} /\ v IN V
1147 /\ w IN V
1148 ==> &0<= (d cross FST x) dot w /\ &0<= (d cross FST x) dot v`)
1149 THEN RESA_TAC
1150 THEN ONCE_REWRITE_TAC[SET_RULE`A\/ B<=> ~(~A /\ ~ B)`]
1151 THEN STRIP_TAC
1152 THEN MP_TAC(REAL_ARITH`&0 <= (d cross FST x) dot w /\ &0 <= (d cross FST x) dot v /\ ~(&0 < (d cross FST x) dot v) /\ ~(&0 < (d cross FST x) dot w)
1153 ==> (d cross FST (x:real^3#real^3)) dot v= &0 /\
1154 (d cross FST x) dot w = &0`)
1155 THEN RESA_TAC
1156 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2
1157 THEN ASSUME_TAC2 EXISTS_INVERSE_OF_V
1158 THEN DOWN THEN STRIP_TAC
1159 THEN MRESA_TAC (GEN_ALL LOFA_IMP_EE_TWO_ELMS)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`vv':real^3`]
1160 THEN ASSUME_TAC2 LOFA_CARD_EE_V_1
1161 THEN UNDISCH_TAC ` azim_in_fan (v:real^3, rho_node1 FF v) E < pi`
1162 THEN UNDISCH_TAC`aff_gt {vec 0} {v, w:real^3} SUBSET
1163 wedge (vec 0) v (rho_node1 FF v)
1164 (azim_cycle (EE v E) (vec 0) v (rho_node1 FF v))`
1165 THEN ASM_REWRITE_TAC[azim_in_fan;ARITH_RULE`2>1`;Local_lemmas.AZIM_CYCLE_TWO_POINT_SET]
1166 THEN LET_TAC
1167 THEN STRIP_TAC
1168 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`d':real^3`]
1169 THEN POP_ASSUM MP_TAC
1170 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1171 THEN STRIP_TAC THEN STRIP_TAC
1172 THEN MRESAL_TAC (GEN_ALL CONDITION_INANGLE_CROSS_DOT)[`v cross w:real^3`;`(rho_node1 FF v:real^3)`;`v:real^3`;`w:real^3`;`d':real^3`;`vec 0:real^3`][VECTOR_ARITH`a- vec 0=a`]
1173 THEN UNDISCH_TAC`&0 < (v cross rho_node1 FF v) dot w`
1174 THEN REWRITE_TAC[]
1175 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1176 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1177 THEN REPEAT STRIP_TAC
1178 THEN ASSUME_TAC2 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V
1179 THEN MP_TAC(SET_RULE`V SUBSET {x':real^3 | &0 <= (d cross FST (x:real^3#real^3)) dot x'}
1180 /\ d' IN V /\ rho_node1 FF v IN V==> &0 <= (d cross FST (x:real^3#real^3)) dot d'
1181 /\ &0 <= (d cross FST (x:real^3#real^3)) dot (rho_node1 FF v)`)
1182 THEN RESA_TAC
1183 THEN MRESAL_TAC DOT_CROSS[`(d cross FST (x:real^3#real^3):real^3)`;`v cross w:real^3`;`(rho_node1 FF v)`;`d':real^3`][CROSS_LAGRANGE;
1184 VECTOR_ARITH`&0 % v - &0 % w= vec 0`;DOT_LZERO; REAL_ARITH`&0=A-B<=> A=B`]
1185 THEN MP_TAC(REAL_ARITH`&0 < (v cross w) dot (d':real^3)==> &0 <= (v cross w) dot d'`)
1186 THEN RESA_TAC
1187 THEN MRESAL_TAC CROSS_CROSS_DET[`d:real^3`;`FST (x:real^3#real^3)`;`v:real^3`;`w:real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
1188 THEN MP_TAC(REAL_ARITH`&0 <= (d cross FST (x:real^3#real^3)) dot rho_node1 FF v
1189 ==> (d cross FST (x:real^3#real^3)) dot rho_node1 FF v= &0 \/ &0 < (d cross FST (x:real^3#real^3)) dot rho_node1 FF v`)
1190 THEN RESA_TAC;
1191 MRESAL_TAC CROSS_CROSS_DET[`d:real^3`;`FST (x:real^3#real^3)`;`v:real^3`;`rho_node1 FF v:real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
1192 THEN MRESAL_TAC DOT_CROSS[`(d cross FST (x:real^3#real^3))`;`v cross (rho_node1 FF v)`;`d cross FST (x:real^3#real^3):real^3`;`w:real^3`][CROSS_LAGRANGE;DOT_LZERO; REAL_ARITH`&0=B- &0*A<=> B= &0`; REAL_ENTIRE;DOT_EQ_0];
1193 POP_ASSUM MP_TAC
1194 THEN REWRITE_TAC[CROSS_EQ_0]
1195 THEN UNDISCH_TAC `!x:real^3. x IN V ==> x,rho_node1 FF x IN FF`
1196 THEN STRIP_TAC
1197 THEN POP_ASSUM(fun th-> MRESA1_TAC th`vv:real^3`)
1198 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;` (d:real^3,FST (x:real^3#real^3))`];
1199 POP_ASSUM MP_TAC
1200 THEN REWRITE_TAC[]
1201 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1202 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1203 THEN ASM_TAC
1204 THEN REAL_ARITH_TAC;
1205 MP_TAC(REAL_ARITH`&0 <= ((d cross FST (x:real^3#real^3))) dot (d':real^3)
1206 ==> ((d cross FST (x:real^3#real^3))) dot (d':real^3)= &0 \/ &0 < ((d cross FST (x:real^3#real^3))) dot (d':real^3)`)
1207 THEN RESA_TAC;
1208 MRESAL_TAC CROSS_CROSS_DET[`d:real^3`;`FST (x:real^3#real^3)`;`v:real^3`;`d':real^3`][DET_CROSS;VECTOR_ARITH`&0 % v - &0 % w= vec 0`]
1209 THEN MRESAL_TAC DOT_CROSS[`(d cross FST (x:real^3#real^3))`;`v cross (d':real^3)`;`(d cross FST (x:real^3#real^3)):real^3`;`w:real^3`][CROSS_LAGRANGE;DOT_LZERO; REAL_ARITH`&0=B- &0*A<=> B= &0`; REAL_ENTIRE;DOT_EQ_0];
1210 POP_ASSUM MP_TAC
1211 THEN REWRITE_TAC[CROSS_EQ_0]
1212 THEN UNDISCH_TAC `!x:real^3. x IN V ==> x,rho_node1 FF x IN FF`
1213 THEN STRIP_TAC
1214 THEN POP_ASSUM(fun th-> MRESA1_TAC th`vv:real^3`)
1215 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;` (d:real^3,FST (x:real^3#real^3))`];
1216 POP_ASSUM MP_TAC
1217 THEN REWRITE_TAC[]
1218 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1219 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1220 THEN ONCE_REWRITE_TAC[CROSS_SKEW;]
1221 THEN REWRITE_TAC[ DOT_LNEG]
1222 THEN ASM_TAC
1223 THEN REAL_ARITH_TAC;
1224 MRESA_TAC REAL_LT_MUL[`(d cross FST (x:real^3#real^3)) dot rho_node1 FF v`;`((v cross w) dot (d':real^3))`]
1225 THEN MP_TAC REAL_LT_MUL_EQ
1226 THEN STRIP_TAC
1227 THEN REMOVE_ASSUM_TAC
1228 THEN POP_ASSUM(fun th-> MRESA_TAC th[`(d cross FST (x:real^3#real^3)) dot (d':real^3)`;`(v cross w) dot (rho_node1 FF v:real^3)`] )
1229 THEN POP_ASSUM MP_TAC
1230 THEN REWRITE_TAC[]
1231 THEN ONCE_REWRITE_TAC[CROSS_SKEW;]
1232 THEN REWRITE_TAC[ DOT_LNEG]
1233 THEN ASM_TAC
1234 THEN REAL_ARITH_TAC]);;
1235
1236 let AFF_GE_SUBSET_AFF_GE_UNION=prove(`!x v u v1:real^3.
1237 DISJOINT {x} {v, u} /\
1238 DISJOINT {x} {v, v1} /\
1239 DISJOINT {x} {v1, u} /\
1240 v1 IN aff_gt {x} {v, u}
1241 ==> aff_ge {x} {v, u} SUBSET aff_ge {x} {v, v1} UNION aff_ge {x} {v1,u}`,
1242 REPEAT STRIP_TAC
1243 THEN POP_ASSUM MP_TAC
1244 THEN MRESA_TAC AFF_GE_1_2[`x:real^3`;`v:real^3`;`u:real^3`]
1245 THEN MRESA_TAC AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`]
1246 THEN MRESA_TAC AFF_GE_1_2[`x:real^3`;`v:real^3`;`v1:real^3`]
1247 THEN MRESAL_TAC AFF_GE_1_2[`x:real^3`;`v1:real^3`;`u:real^3`][SUBSET;IN_ELIM_THM;UNION]
1248 THEN REPEAT STRIP_TAC
1249 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1'' % x + t2'' % v + t3'' % (t1 % x + t2 % v + t3 % u)= (t1''+t3'' *t1) % x + (t2''+ t3''* t2) % v + (t3''*t3) % u`
1250 ;VECTOR_ARITH`t1'' % x + t2'' % (t1 % x + t2 % v + t3 % u) + t3'' % u=
1251 (t1''+ t2''* t1) % x + (t2'' * t2) % v + (t3'' + t2''*t3) % u`]
1252 THEN DISJ_CASES_TAC(REAL_ARITH`inv t3 * t3' <= inv t2 * t2' \/ inv t2 * t2' <= inv t3 * t3'`)
1253 THENL[
1254 MATCH_MP_TAC(SET_RULE`A==> A\/B`)
1255 THEN MP_TAC(REAL_ARITH`&0< t3==> ~(t3= &0) /\ &0<= t3`)
1256 THEN RESA_TAC
1257 THEN MRESA1_TAC REAL_MUL_LINV`t3:real`
1258 THEN MP_TAC(REAL_ARITH`&0< t2==> ~(t2= &0)/\ &0<= t2`)
1259 THEN RESA_TAC
1260 THEN MRESA1_TAC REAL_MUL_LINV`t2:real`
1261 THEN EXISTS_TAC`&1-(t2'- inv t3 * t3' * t2)- inv t3 * t3'`
1262 THEN EXISTS_TAC`(t2'- inv t3 * t3' * t2)`
1263 THEN EXISTS_TAC`inv t3 * t3'`
1264 THEN ASM_REWRITE_TAC[REAL_ARITH`&1- A-B+A+B= &1`;REAL_ARITH`&0<= a-b<=>b<=a`; REAL_ARITH`t2' - inv t3 * t3' * t2 + (inv t3 * t3') * t2= t2'`; REAL_ARITH`(A*B)*C=B*(A*C)`; REAL_ARITH`&1 - (t2' - inv t3 * t3' * t2) - inv t3 * t3' + t3' * inv t3 * t1=
1265 &1 - t2' -inv t3 * t3' *(t3-(t1+t2+t3)+ &1)`; REAL_ARITH`a- &1+ &1=a`; REAL_ARITH`a* &1=a`]
1266 THEN ASM_REWRITE_TAC[REAL_ARITH`a*b*c= (a*c) *b`; REAL_ARITH`(&1 - t2' - &1 * t3')= t1' + &1- (t1'+t2'+t3')`; REAL_ARITH`a+ &1- &1=a`;]
1267 THEN MRESA_TAC REAL_LE_LMUL[`t2:real`;`inv t3 * t3'`;`inv t2 * t2'`]
1268 THEN POP_ASSUM MP_TAC
1269 THEN ASM_REWRITE_TAC[REAL_ARITH`A*B*C=(B*A)*C/\ &1* a=a`]
1270 THEN RESA_TAC
1271 THEN MATCH_MP_TAC REAL_LE_MUL
1272 THEN ASM_REWRITE_TAC[]
1273 THEN MATCH_MP_TAC REAL_LE_INV
1274 THEN ASM_REWRITE_TAC[];
1275 MATCH_MP_TAC(SET_RULE`B==> A\/B`)
1276 THEN MP_TAC(REAL_ARITH`&0< t3==> ~(t3= &0) /\ &0<= t3`)
1277 THEN RESA_TAC
1278 THEN MRESA1_TAC REAL_MUL_LINV`t3:real`
1279 THEN MP_TAC(REAL_ARITH`&0< t2==> ~(t2= &0)/\ &0<= t2`)
1280 THEN RESA_TAC
1281 THEN MRESA1_TAC REAL_MUL_LINV`t2:real`
1282 THEN EXISTS_TAC`&1- inv t2 * t2' -( t3'- inv t2 * t2'* t3)`
1283 THEN EXISTS_TAC`inv t2 * t2'`
1284 THEN EXISTS_TAC`( t3'- inv t2 * t2'* t3)`
1285 THEN ASM_REWRITE_TAC[REAL_ARITH`&1- A-B+A+B= &1`;REAL_ARITH`&0<= a-b<=>b<=a`; REAL_ARITH`t2' - inv t3 * t3' * t2 + (inv t3 * t3') * t2= t2'`; REAL_ARITH`(A*B)*C=B*(A*C)`;]
1286 THEN ASM_REWRITE_TAC[ REAL_ARITH`(&1 - inv t2 * t2' - (t3' - (inv t2 * t3) * t2') + (t2' * t1) * inv t2)
1287 = &1 - t3' - inv t2 * t2'* ( t2 -(t1+t2+t3)+ &1)`; REAL_ARITH`a- &1+ &1=a`; REAL_ARITH`a* &1=a`;REAL_ARITH`a*b*c= (a*c) *b`; REAL_ARITH`(&1 - t2' - &1 * t3')= t1' + &1- (t1'+t3'+t2')`; REAL_ARITH`a+ &1- &1=a`;]
1288 THEN MRESA_TAC REAL_LE_LMUL[`t3:real`;`inv t2 * t2'`;`inv t3 * t3'`]
1289 THEN POP_ASSUM MP_TAC
1290 THEN ASM_REWRITE_TAC[REAL_ARITH`A*B*C=(B*A)*C/\ &1* a=a`]
1291 THEN RESA_TAC
1292 THEN MATCH_MP_TAC REAL_LE_MUL
1293 THEN ASM_REWRITE_TAC[]
1294 THEN MATCH_MP_TAC REAL_LE_INV
1295 THEN ASM_REWRITE_TAC[]]);;
1296
1297
1298 let aff_ge_subset3_aff_ge=prove(`!x:real^3 v:real^3 u:real^3 v1:real^3.
1299 DISJOINT {x} {v,u} /\ DISJOINT {x} {v,v1}
1300 /\ v1 IN aff_gt {x} {v,u}
1301 ==>
1302 aff_ge {x} {v,v1} SUBSET aff_ge {x} {v,u}`,
1303 REPEAT STRIP_TAC
1304 THEN POP_ASSUM MP_TAC
1305 THEN MRESAL_TAC AFF_GE_1_2[`x:real^3`;`v:real^3`;`u:real^3`][IN_ELIM_THM]
1306 THEN MRESAL_TAC AFF_GT_1_2[`x:real^3`;`v:real^3`;`u:real^3`][IN_ELIM_THM]
1307 THEN MRESAL_TAC AFF_GE_1_2[`x:real^3`;`v:real^3`;`v1:real^3`][IN_ELIM_THM;SUBSET]
1308 THEN REPEAT STRIP_TAC
1309 THEN POP_ASSUM MP_TAC
1310 THEN ASM_REWRITE_TAC[VECTOR_ARITH`t1' % x + t2' % v + t3' % (t1 % x + t2 % v + t3 % u)
1311 =(t1'+ t3'*t1) % x + (t2'+ t3' * t2) % v + (t3' * t3) % u:real^3`]
1312 THEN STRIP_TAC
1313 THEN EXISTS_TAC`t1' + t3' * t1:real`
1314 THEN EXISTS_TAC`t2' + t3' * t2:real`
1315 THEN EXISTS_TAC`t3' * t3:real`
1316 THEN MP_TAC(REAL_ARITH`&0< t2 /\ &0< t3==> &0<= t2 /\ &0<= t3`)
1317 THEN RESA_TAC
1318 THEN MRESA_TAC REAL_LE_MUL[`t3':real`;`t2:real`]
1319 THEN MRESA_TAC REAL_LE_MUL[`t3':real`;`t3:real`]
1320 THEN ASM_REWRITE_TAC[REAL_ARITH`(t1' + t3' * t1) + (t2' + t3' * t2) + t3' * t3=
1321 t1'+ t2' + t3'*(t1+t2+t3)`; REAL_ARITH`A* &1=A`]
1322 THEN ASM_TAC
1323 THEN REAL_ARITH_TAC);;
1324
1325
1326 let AFF_GE_EQ_AFF_GE_UNION=prove(`!x v u v1:real^3.
1327 DISJOINT {x} {v, u} /\
1328 DISJOINT {x} {v, v1} /\
1329 DISJOINT {x} {v1, u} /\
1330 v1 IN aff_gt {x} {v, u}
1331 ==> aff_ge {x} {v, u} = aff_ge {x} {v, v1} UNION aff_ge {x} {v1,u}`,
1332 REPEAT STRIP_TAC
1333 THEN ASSUME_TAC2 AFF_GE_SUBSET_AFF_GE_UNION
1334 THEN MRESA_TAC aff_ge_subset3_aff_ge[`x:real^3`;`v:real^3`;`u:real^3`;`v1:real^3`]
1335 THEN MRESA_TAC aff_ge_subset3_aff_ge[`x:real^3`;`u:real^3`;`v:real^3`;`v1:real^3`]
1336 THEN POP_ASSUM MP_TAC
1337 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1338 THEN ASM_REWRITE_TAC[]
1339 THEN STRIP_TAC
1340 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
1341 THEN POP_ASSUM MP_TAC
1342 THEN POP_ASSUM MP_TAC
1343 THEN POP_ASSUM MP_TAC
1344 THEN SET_TAC[]);;
1345
1346
1347
1348 let order = new_definition ` order f x y = (@n. ITER n f x =y /\ (!i. 0< i /\ i< n ==> ~(ITER i f x= y)))`;;
1349 let slicev = new_definition ` slicev E FF v w = {u| ?n. 0<= n /\ n<= order (rho_node1 FF) v w /\ u= ITER n (rho_node1 FF) v}`;;
1350
1351 let slicee = new_definition ` slicee E FF v w = {e| ?u. u IN (slicev E FF v w) DELETE w /\ e={u,rho_node1 FF u} } UNION {{w,v}}`;;
1352
1353 let slicef = new_definition ` slicef E FF v w = {f| ?u. u IN (slicev E FF v w) DELETE w /\ f=(u,rho_node1 FF u) } UNION {(w,v)}`;;
1354
1355
1356 let rho_fun = new_definition `rho_fun y = &1 + (inv (&2 * h0 - &2)) * (inv pi) * sol0 * (y - &2)`;;
1357
1358
1359 let tau_fun = new_definition `tau_fun V E f = sum (f) (\e. rho_fun(norm(FST e)) * (azim_in_fan e E)) - (pi + sol0) * &(CARD f -2)`;;
1360
1361
1362
1363 let ORDER=prove(`(ITER n f x = y /\ (!i. 0 < i /\ i < n ==> ~(ITER i f x = y)))
1364 ==>
1365 ITER (order f x y) f x= y /\ (!i. 0 < i /\ i < order f x y ==> ~(ITER i f x = y))`,
1366 STRIP_TAC
1367 THEN ONCE_REWRITE_TAC[order]
1368 THEN SELECT_ELIM_TAC
1369 THEN ASM_REWRITE_TAC[]
1370 THEN POP_ASSUM MP_TAC
1371 THEN POP_ASSUM MP_TAC
1372 THEN SET_TAC[]);;
1373
1374 let UNIQUE_ORDER=prove_by_refinement(`!f:A->A. ITER n f x = y /\ (!i. 0 < i /\ i < n ==> ~(ITER i f x = y)) /\ ~(x=y)
1375 ==>
1376 order f x y= n`,
1377 [REPEAT STRIP_TAC
1378 THEN MRESA_TAC (GEN_ALL ORDER)[`n:num`;`f:A->A`;`x:A`;`y:A`]
1379 THEN MP_TAC(ARITH_RULE`order (f:A->A) x y =0 \/ 0< order (f:A->A) x y `)
1380 THEN RESA_TAC;
1381 POP_ASSUM(fun th -> ASM_TAC THEN REWRITE_TAC[th;ITER])
1382 THEN SET_TAC[];
1383 MP_TAC(ARITH_RULE`order (f:A->A) x y <n \/ n<= order (f:A->A) x y `)
1384 THEN RESA_TAC;
1385 ASM_TAC
1386 THEN STRIP_TAC
1387 THEN STRIP_TAC
1388 THEN POP_ASSUM(fun th-> MRESA1_TAC th `order (f:A->A) x y`)
1389 THEN POP_ASSUM MP_TAC
1390 THEN DISCH_THEN(LABEL_TAC "THY")
1391 THEN REPEAT STRIP_TAC
1392 THEN REMOVE_THEN "THY" MP_TAC
1393 THEN RESA_TAC;
1394 MP_TAC(ARITH_RULE`n<= order (f:A->A) x y ==> n< order (f:A->A) x y \/ order (f:A->A) x y =n`)
1395 THEN RESA_TAC;
1396 MP_TAC(ARITH_RULE`n =0 \/ 0< n`)
1397 THEN RESA_TAC;
1398 POP_ASSUM(fun th -> ASM_TAC THEN REWRITE_TAC[th;ITER])
1399 THEN SET_TAC[];
1400 POP_ASSUM MP_TAC
1401 THEN POP_ASSUM MP_TAC
1402 THEN POP_ASSUM MP_TAC
1403 THEN POP_ASSUM MP_TAC
1404 THEN POP_ASSUM MP_TAC
1405 THEN DISCH_THEN(LABEL_TAC "THY")
1406 THEN REPEAT STRIP_TAC
1407 THEN REMOVE_THEN "THY" (fun th-> MRESA1_TAC th`n:num`)]);;
1408
1409
1410
1411
1412
1413 let COMPATIBLE_BW_TWO_LEMMAS = prove_by_refinement
1414 (`convex_local_fan (V,E,FF) /\
1415         v IN V /\
1416         w IN V /\
1417         ~(v = w) /\
1418        (!x. x IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt x E) /\
1419        HS = hypermap (HYP (vec 0,V,E UNION {{v, w}})) /\
1420        fv = face HS (v,rho_node1 FF v)
1421 ==>  (v_prime V fv  =  slicev E FF v w ) /\
1422  e_prime  (E UNION {{v, w}}) fv = slicee E FF v w /\
1423 fv = slicef E FF v w `,
1424 [STRIP_TAC;
1425 ASSUME_TAC2 PROVE_THE_SLICE_ASSUMPTION;
1426 MP_TAC POINTS_IN_HAFL_CIRCLE;
1427 ANTS_TAC;
1428 DOWN_TAC;
1429 SIMP_TAC[convex_local_fan];
1430
1431 ASSUME_TAC2 Local_lemmas.CVX_LO_IMP_LO;
1432 ASSUME_TAC2 POINT_PRESENTED_IN_RHOND1;
1433 DOWN THEN STRIP_TAC;
1434 DISCH_TAC;
1435 MP_TAC DETERMINE_FV2;
1436 PHA;
1437 ANTS_TAC;
1438 ASM_REWRITE_TAC[TAUT` a /\ b ==> c <=> a ==> b ==> c `];
1439
1440
1441 DISCH_TAC;
1442 SUBGOAL_THEN` v_prime   (V:real^3 -> bool) (fv:real^3#real^3 -> bool) =
1443 slicev (E:(real^3 -> bool) -> bool) FF v w ` MP_TAC;
1444 ASM_REWRITE_TAC[slicev; EXTENSION; IN_ELIM_THM];
1445 GEN_TAC;
1446 EQ_TAC;
1447 STRIP_TAC;
1448 EXISTS_TAC` n':num`;
1449 ASM_REWRITE_TAC[LE_0];
1450 MP_TAC (ISPECL [` v:real^3 `;` w:real^3 `;` n:num `; ` rho_node1 FF `] (GEN_ALL UNIQUE_ORDER));
1451 ANTS_TAC;
1452 ASM_REWRITE_TAC[];
1453 GEN_TAC;
1454 ASM_CASES_TAC` i = 0`;
1455 ASM_REWRITE_TAC[ITER];
1456 ASSUME_TAC2 (ARITH_RULE` ~( i =0) ==> 0 < i `);
1457 ASM_REWRITE_TAC[];
1458 SIMP_TAC[];
1459
1460 STRIP_TAC;
1461
1462 ASM_CASES_TAC` n < (n': num) `;
1463 DOWN;
1464 FIRST_X_ASSUM NHANH;
1465 ASM_REWRITE_TAC[];
1466 DOWN;
1467 ARITH_TAC;
1468
1469
1470
1471 STRIP_TAC;
1472 EXISTS_TAC `n':num `;
1473 ASM_REWRITE_TAC[];
1474 MP_TAC (ISPECL [` v:real^3 `;` w:real^3 `;` n:num `; ` rho_node1 FF `] (GEN_ALL UNIQUE_ORDER));
1475 ANTS_TAC;
1476 ASM_REWRITE_TAC[];
1477 GEN_TAC;
1478 ASM_CASES_TAC` i = 0 `;
1479 ASM_REWRITE_TAC[ITER];
1480 ASSUME_TAC2 (ARITH_RULE` ~( i = 0) ==> 0 < i `);
1481 ASM_REWRITE_TAC[];
1482 DISCH_THEN SUBST_ALL_TAC;
1483 GEN_TAC THEN DISCH_TAC;
1484 ASSUME_TAC2 (ARITH_RULE` m < n' /\ n' <= n ==> m < n:num `);
1485 DOWN;
1486 ASM_REWRITE_TAC[];
1487
1488
1489 SIMP_TAC[];
1490 REWRITE_TAC[slicee; slicef];
1491 DISCH_THEN (SUBST_ALL_TAC o SYM);
1492 REWRITE_TAC[e_prime];
1493
1494
1495 CONJ_TAC;
1496 REWRITE_TAC[EXTENSION; IN_UNION];
1497 GEN_TAC;
1498 EQ_TAC;
1499 ONCE_REWRITE_TAC[IN_ELIM_THM];
1500 REWRITE_TAC[];
1501 FIRST_ASSUM SUBST1_TAC;
1502 REWRITE_TAC[IN_INSERT];
1503 FIRST_ASSUM (SUBST1_TAC o SYM);
1504 STRIP_TAC;
1505
1506 DOWN THEN DOWN;
1507 SIMP_TAC[PAIR_EQ];
1508
1509
1510 DISJ1_TAC;
1511 DOWN THEN DOWN;
1512 REWRITE_TAC[IN_ELIM_THM; PAIR_EQ];
1513 STRIP_TAC;
1514 STRIP_TAC;
1515 EXISTS_TAC` ITER m (rho_node1 FF) v `;
1516 REWRITE_TAC[GSYM IN_INSERT; GSYM EXTENSION];
1517 DOWN;
1518 ASM_REWRITE_TAC[];
1519 SIMP_TAC[GSYM ITER; ADD1];
1520 STRIP_TAC;
1521 REWRITE_TAC[IN_DELETE; IN_ELIM_THM];
1522 CONJ_TAC;
1523 EXISTS_TAC `m:num `;
1524 REWRITE_TAC[];
1525 ASM_REWRITE_TAC[];
1526 GEN_TAC THEN STRIP_TAC;
1527 ASSUME_TAC2 (ARITH_RULE` m' < m /\ m < (n:num) ==> m' < n`);
1528 DOWN;
1529 ASM_REWRITE_TAC[];
1530
1531 UNDISCH_TAC` m < (n:num) `;
1532 ASM_REWRITE_TAC[];
1533
1534 DISJ2_TAC THEN DISJ1_TAC;
1535 DOWN THEN DOWN;
1536 SIMP_TAC[PAIR_EQ];
1537
1538
1539 ASM_REWRITE_TAC[];
1540
1541
1542 REWRITE_TAC[INSERT_COMM];
1543 REPLICATE_TAC 3 DOWN;
1544 REWRITE_TAC[NOT_IN_EMPTY];
1545
1546 REPLICATE_TAC 3 DOWN;
1547 REWRITE_TAC[NOT_IN_EMPTY];
1548
1549 (* ==================== *)
1550
1551 REWRITE_TAC[GSYM EXTENSION; GSYM IN_INSERT];
1552 DOWN;
1553 FIRST_ASSUM SUBST1_TAC;
1554 SIMP_TAC[];
1555 STRIP_TAC;
1556 REWRITE_TAC[IN_ELIM_THM; IN_DELETE];
1557 STRIP_TAC;
1558 EXISTS_TAC` u: real^3`;
1559 EXISTS_TAC` rho_node1 FF u `;
1560 REWRITE_TAC[IN_INSERT; IN_ELIM_THM];
1561 ASM_REWRITE_TAC[];
1562
1563
1564 CONJ_TAC;
1565 DISJ1_TAC;
1566 MATCH_MP_TAC LOCAL_RHO_NODE_PAIR_E;
1567 ASM_REWRITE_TAC[];
1568 UNDISCH_TAC` (v:real^3) IN V `;
1569 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER;
1570 DOWN THEN SIMP_TAC[];
1571 DISJ2_TAC;
1572 EXISTS_TAC` n': num `;
1573 REWRITE_TAC[GSYM ITER; ADD1];
1574 ASM_CASES_TAC` (n:num) < n' `;
1575 DOWN;
1576 FIRST_X_ASSUM NHANH;
1577 ASM_REWRITE_TAC[];
1578
1579 DOWN;
1580 ASM_CASES_TAC` n = (n': num) `;
1581 UNDISCH_TAC` ~(u = (w:real^3)) `;
1582 FIRST_X_ASSUM SUBST_ALL_TAC;
1583 ASM_REWRITE_TAC[];
1584 DOWN THEN ARITH_TAC;
1585
1586
1587
1588
1589
1590 DOWN;
1591 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; IN_ELIM_THM];
1592 STRIP_TAC;
1593 EXISTS_TAC` w:real^3 `;
1594 EXISTS_TAC` v:real^3 `;
1595 DOWN THEN SIMP_TAC[];
1596
1597
1598 SIMP_TAC[INSERT_COMM];
1599 DOWN;
1600 FIRST_ASSUM SUBST1_TAC;
1601 SIMP_TAC[];
1602 STRIP_TAC;
1603
1604
1605
1606 FIRST_X_ASSUM (SUBST1_TAC o SYM);
1607 ASSUME_TAC2 DETERMINE_FV;
1608 FIRST_X_ASSUM SUBST1_TAC;
1609 REWRITE_TAC[EXTENSION; IN_INSERT; IN_UNION; IN_ELIM_THM];
1610 GEN_TAC;
1611 EQ_TAC;
1612 STRIP_TAC;
1613 FIRST_X_ASSUM (fun x -> REWRITE_TAC[x]);
1614 DISJ1_TAC;
1615 EXISTS_TAC` ITER n' (rho_node1 FF) v `;
1616 ASM_REWRITE_TAC[IN_DELETE; IN_ELIM_THM;GSYM ITER; ADD1];
1617 CONJ_TAC;
1618 EXISTS_TAC `n': num `;
1619 REWRITE_TAC[];
1620 GEN_TAC;
1621 NHANH (ARITH_RULE` a < (b:num) ==> a < b + 1 `);
1622 FIRST_X_ASSUM NHANH;
1623 SIMP_TAC[];
1624 MP_TAC (ARITH_RULE` n' < n' + 1 `);
1625 ASM_REWRITE_TAC[];
1626
1627
1628 REWRITE_TAC[NOT_IN_EMPTY];
1629 STRIP_TAC;
1630 DISJ2_TAC;
1631 DOWN THEN DOWN;
1632 REWRITE_TAC[IN_ELIM_THM; IN_DELETE];
1633 STRIP_TAC;
1634 STRIP_TAC;
1635 EXISTS_TAC` n':num `;
1636 ASM_REWRITE_TAC[ADD1;GSYM ITER];
1637 GEN_TAC;
1638 ASM_CASES_TAC` m = (n': num) `;
1639 STRIP_TAC;
1640 UNDISCH_TAC` ~( u = (w:real^3)) `;
1641 ASM_REWRITE_TAC[];
1642 DOWN THEN PHA;
1643 REWRITE_TAC[ARITH_RULE` ~(m = n') /\ m < n' + 1 <=> m < (n':num) `];
1644 ASM_REWRITE_TAC[];
1645 DOWN THEN SIMP_TAC[]]);;
1646
1647
1648
1649
1650
1651 let COMPATIBLE_BW_TWO_LEMMAS2 = prove_by_refinement
1652 (`(convex_local_fan (V,E,FF) /\
1653         v IN V /\
1654         w IN V /\
1655         ~(v = w) /\
1656        (!x. x IN FF ==> aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt x E) /\
1657        HS = hypermap (HYP (vec 0,V,E UNION {{v, w}})) /\
1658        fv = face HS (v,rho_node1 FF v))/\
1659 fw = face HS (w, rho_node1 FF w)
1660 ==> ( (v_prime V fv  =  slicev E FF v w ) /\
1661  e_prime  (E UNION {{v, w}}) fv = slicee E FF v w /\
1662 fv = slicef E FF v w ) /\
1663 ( (v_prime V fw  =  slicev E FF w v ) /\
1664  e_prime  (E UNION {{w, v}}) fw = slicee E FF w v /\
1665 fw = slicef E FF w v )`,
1666 [NHANH COMPATIBLE_BW_TWO_LEMMAS;
1667 STRIP_TAC;
1668 CONJ_TAC;
1669 CONJ_TAC;
1670 FIRST_X_ASSUM ACCEPT_TAC;
1671 CONJ_TAC;
1672 FIRST_X_ASSUM ACCEPT_TAC;
1673 FIRST_X_ASSUM ACCEPT_TAC;
1674
1675
1676 MATCH_MP_TAC COMPATIBLE_BW_TWO_LEMMAS;
1677 ASM_REWRITE_TAC[];
1678 REWRITE_TAC[INSERT_COMM];
1679 ASM_REWRITE_TAC[]]);;
1680
1681
1682
1683
1684
1685 let EJRCFJD_concl=`!V E FF v w. convex_local_fan(V,E,FF)
1686 /\
1687 v IN V /\ w IN V
1688 /\ (!u u1. u IN {v,w} /\ u1 IN V /\ ~(u=u1) ==> ~(collinear {vec 0, u, u1}))
1689 /\ (!e. e IN FF ==> aff_gt {vec 0} {v,w} SUBSET wedge_in_fan_gt e E)
1690 ==> convex_local_fan(slicev E FF v w, slicee E FF v w, slicef E FF v w)
1691 /\ convex_local_fan(slicev E FF w v, slicee E FF w v, slicef E FF w v)
1692 /\ tau_fun V E FF >= tau_fun (slicev E FF v w) (slicee E FF v w) (slicef E FF v w) + tau_fun (slicev E FF w v) (slicee E FF w v) (slicef E FF w v)
1693 /\ sol_local E FF= sol_local (slicee E FF v w) (slicef E FF v w) + sol_local (slicee E FF w v) (slicef E FF w v)
1694 /\ CARD (slicev E FF v w) < CARD V
1695 /\ CARD (slicev E FF w v) < CARD V
1696 /\(generic V E ==> generic (slicev E FF v w) (slicee E FF v w)
1697 /\ generic (slicev E FF w v) (slicee E FF w v))`
1698 ;;
1699
1700 let NKEZBFC_concl=`!V E FF. convex_local_fan(V,E,FF) /\ generic V E
1701 ==> &0 <= sol_local E FF`
1702 ;;
1703
1704 let NKEZBFC_concl2 = mk_imp (EJRCFJD_concl, NKEZBFC_concl);;
1705
1706
1707 let lemma=prove(`!A. A \/ ~A`, SET_TAC[]);;
1708 let lemma1=prove(`!A. ~A \/ A`, SET_TAC[]);;
1709
1710
1711
1712
1713
1714
1715
1716 g(NKEZBFC_concl2);;
1717
1718 let NKEZBFC_PREP =prove_by_refinement(NKEZBFC_concl2,
1719 [REPEAT STRIP_TAC
1720 THEN ABBREV_TAC`n= CARD (V:real^3->bool)-3`
1721 THEN ASM_TAC
1722 THEN DISCH_THEN(LABEL_TAC"LINH")
1723 THEN SPEC_TAC(`V:real^3->bool`,`V:real^3->bool`)
1724 THEN SPEC_TAC(`E:(real^3->bool)->bool`,`E:(real^3->bool)->bool`)
1725 THEN SPEC_TAC(`FF:real^3#real^3->bool`,`FF:real^3#real^3->bool`)
1726 THEN SPEC_TAC(`n:num`,`n:num`)
1727 THEN MATCH_MP_TAC num_WF
1728 THEN INDUCT_TAC;
1729 REPEAT STRIP_TAC
1730 THEN MRESA_TAC CARD_VERTEX_GE_3_LOCAL_FAN[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`]
1731 THEN MP_TAC(ARITH_RULE`3<= CARD (V:real^3->bool) /\ CARD V -3 =0 <=> CARD V=3`)
1732 THEN RESA_TAC
1733 THEN ASM_MESON_TAC[SOL_LOCAL_FAN_POS_CASE3];
1734 POP_ASSUM MP_TAC
1735 THEN DISCH_THEN(LABEL_TAC"LINH1")
1736 THEN DISCH_THEN(LABEL_TAC"LIN21")
1737 THEN REPEAT STRIP_TAC
1738 THEN MRESA_TAC CARD_VERTEX_GE_3_LOCAL_FAN[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`]
1739 THEN MRESA1_TAC lemma `(?v w:real^3. v IN V /\ w IN V
1740 /\ (!e. e IN FF ==> aff_gt {vec 0} {v,w} SUBSET wedge_in_fan_gt e E)
1741 ):bool`;
1742 MRESA_TAC (GEN_ALL PROPERTIES_GENERIC1)[`FF:real^3#real^3->bool`;`E:(real^3->bool)->bool`;`v:real^3`;`w:real^3`;`V:real^3->bool`;]
1743 THEN REMOVE_THEN "LINH"(fun th-> MRESA_TAC th[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`w:real^3`])
1744 THEN MRESA_TAC CARD_VERTEX_GE_3_LOCAL_FAN[`(slicev (E:(real^3->bool)->bool) FF v w):real^3->bool`;`(slicee (E:(real^3->bool)->bool) FF v w):(real^3->bool)->bool`;`(slicef (E:(real^3->bool)->bool) FF v w):real^3#real^3->bool`]
1745 THEN MRESA_TAC CARD_VERTEX_GE_3_LOCAL_FAN[`(slicev (E:(real^3->bool)->bool) FF w v):real^3->bool`;`(slicee (E:(real^3->bool)->bool) FF w v ):(real^3->bool)->bool`;`(slicef (E:(real^3->bool)->bool) FF w v ):real^3#real^3->bool`]
1746 THEN MP_TAC(ARITH_RULE`CARD (slicev E FF v w)< CARD V
1747 /\ CARD (slicev E FF w v)< CARD V
1748 /\ 3<= CARD V /\ 3<= CARD (slicev E FF v w)
1749 /\ 3<= CARD (slicev E FF w v)==> CARD (slicev (E:(real^3->bool)->bool) FF v w) -3 < CARD V -3
1750 /\ CARD (slicev E FF w v) -3 < CARD (V:real^3->bool) -3`)
1751 THEN RESA_TAC
1752 THEN REMOVE_THEN "LIN21"(fun th-> MRESA1_TAC th`CARD (slicev (E:(real^3->bool)->bool) FF v w) -3`
1753 THEN POP_ASSUM(fun th-> MRESA_TAC th[`(slicef (E:(real^3->bool)->bool) FF v w)`;`(slicee (E:(real^3->bool)->bool) FF v w)`;`(slicev (E:(real^3->bool)->bool) FF v w):real^3->bool`])
1754 THEN MRESA1_TAC th`CARD (slicev (E:(real^3->bool)->bool) FF w v) -3`
1755 THEN POP_ASSUM(fun th-> MRESA_TAC th[`(slicef (E:(real^3->bool)->bool) FF w v)`;`(slicee (E:(real^3->bool)->bool) FF w v)`;`(slicev (E:(real^3->bool)->bool) FF w v)`]))
1756 THEN POP_ASSUM MP_TAC
1757 THEN POP_ASSUM MP_TAC
1758 THEN REAL_ARITH_TAC;
1759 POP_ASSUM MP_TAC
1760 THEN REWRITE_TAC[NOT_EXISTS_THM;DE_MORGAN_THM]
1761 THEN DISCH_THEN(LABEL_TAC"LINH2")
1762 THEN ASSUME_TAC2 SOL_LOFA_EQ_SUM_INANGLE
1763 THEN MRESA1_TAC lemma`(!v. v IN V==> pi <= interior_angle1 (vec 0) FF v )`;
1764 MATCH_MP_TAC(REAL_ARITH`&0< pi /\ &0<= A==> &0<= &2 * pi+A`)
1765 THEN REWRITE_TAC[PI_WORKS]
1766 THEN MATCH_MP_TAC SUM_POS_LE
1767 THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= A-B<=> B<= A`]
1768 THEN ASM_TAC
1769 THEN REWRITE_TAC[convex_local_fan;local_fan;FAN;fan1]
1770 THEN LET_TAC
1771 THEN REPEAT STRIP_TAC
1772 THEN ASM_REWRITE_TAC[];
1773 POP_ASSUM MP_TAC
1774 THEN REWRITE_TAC[NOT_IMP;NOT_FORALL_THM;REAL_ARITH`~(a<=b) <=> b<a`]
1775 THEN STRIP_TAC
1776 THEN UNDISCH_TAC`convex_local_fan (V:real^3->bool,E,FF)`
1777 THEN STRIP_TAC
1778 THEN POP_ASSUM(fun th -> MP_TAC th THEN REWRITE_TAC[convex_local_fan] THEN ASSUME_TAC th THEN STRIP_TAC)
1779 THEN MRESA_TAC PROPERTIES_GENERIC_LOCAL_FAN[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`;]
1780 THEN ABBREV_TAC`vv=(\i. ITER i (rho_node1 FF) v)`
1781 THEN ABBREV_TAC`bta=(\i. azim (vec 0) v (vv 1) (vv i))`
1782 THEN ABBREV_TAC`k=CARD (V:real^3->bool)`
1783 THEN MRESA1_TAC lemma1`(!i. i<k ==> bta i= &0 \/ bta i= bta (k-1)):bool`;
1784 POP_ASSUM MP_TAC
1785 THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP;DE_MORGAN_THM]
1786 THEN STRIP_TAC
1787 THEN DISJ_CASES_TAC(ARITH_RULE` k-1<= i \/ (i< k-1)`);
1788 MP_TAC(ARITH_RULE`k-1<= i /\ i< k /\ 3<= k==> i= k-1`)
1789 THEN RESA_TAC
1790 THEN POP_ASSUM (fun th-> ASM_TAC THEN REWRITE_TAC[th])
1791 THEN SET_TAC[];
1792 MP_TAC(ARITH_RULE` 3<= k==> k-1<k`)
1793 THEN RESA_TAC
1794 THEN MRESA_TAC (GEN_ALL EGHNAVX)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`bta:num->real`;
1795 `FF:real^3#real^3->bool`; `i:num`;`v:real^3`;`vv:num->real^3`;`CARD (V:real^3->bool)`]
1796 THEN POP_ASSUM MP_TAC
1797 THEN EXPAND_TAC "bta"
1798 THEN REWRITE_TAC[]
1799 THEN EXPAND_TAC "vv"
1800 THEN REWRITE_TAC[]
1801 THEN STRIP_TAC
1802 THEN POP_ASSUM (fun th-> MRESA_TAC th[`i:num`;`k-1:num`])
1803 THEN MP_TAC(REAL_ARITH`~(bta i = &0) /\ ~(bta i = bta (k - 1))
1804 /\ &0<= bta i /\ bta i<= bta(k-1)==> &0< bta i /\ bta i< bta(k-1)`)
1805 THEN ASM_REWRITE_TAC[]
1806 THEN EXPAND_TAC "bta"
1807 THEN REWRITE_TAC[]
1808 THEN EXPAND_TAC "vv"
1809 THEN REWRITE_TAC[]
1810 THEN ASM_REWRITE_TAC[azim;ITER1]
1811 THEN ABBREV_TAC`w=(ITER i (rho_node1 FF) v)`
1812 THEN ASSUME_TAC2 Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
1813 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
1814 THEN STRIP_TAC
1815 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
1816 THEN POP_ASSUM (fun th-> MRESA1_TAC th `i:num`)
1817 THEN REMOVE_THEN "LINH2"(fun th-> MRESA_TAC th [`v:real^3`;`w:real^3`] )
1818 THEN SUBGOAL_THEN`0< i` ASSUME_TAC;
1819 ONCE_REWRITE_TAC[ARITH_RULE`0<i<=> ~(i=0)`]
1820 THEN STRIP_TAC
1821 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1822 THEN UNDISCH_TAC`~(bta 0 = &0)`
1823 THEN EXPAND_TAC"bta"
1824 THEN EXPAND_TAC"vv"
1825 THEN REWRITE_TAC[ITER;Local_lemmas.AZIM_SPEC_DEGENERATE];
1826 ASSUME_TAC2 Local_lemmas.LOFA_IMP_DIS_ELMS23
1827 THEN POP_ASSUM(fun th->MRESAL_TAC th[`0:num`;`i:num`][ITER])
1828 THEN SUBGOAL_THEN`azim_in_fan (v,rho_node1 FF v) E < pi`ASSUME_TAC;
1829 ASSUME_TAC2 CONVEX_LOFA_IMP_INANGLE_EQ_AZIM
1830 THEN POP_ASSUM (fun th-> MRESA1_TAC th`v:real^3`)
1831 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);
1832 SUBGOAL_THEN`aff_gt {vec 0} {v, w} SUBSET wedge_in_fan_gt (v,rho_node1 FF v) E`
1833 ASSUME_TAC;
1834 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2
1835 THEN ASSUME_TAC2 EXISTS_INVERSE_OF_V
1836 THEN DOWN THEN STRIP_TAC
1837 THEN MRESA_TAC (GEN_ALL LOFA_IMP_EE_TWO_ELMS)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`vv':real^3`]
1838 THEN ASSUME_TAC2 LOFA_CARD_EE_V_1
1839 THEN UNDISCH_TAC ` azim_in_fan (v:real^3, rho_node1 FF v) E < pi`
1840 THEN ASM_REWRITE_TAC[azim_in_fan;wedge_in_fan_gt;ARITH_RULE`2>1`;Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;]
1841 THEN LET_TAC
1842 THEN STRIP_TAC
1843 THEN UNDISCH_TAC `!v'. v' IN V /\ ~(v' = v) ==> ~collinear {vec 0, v, v':real^3}`
1844 THEN STRIP_TAC
1845 THEN POP_ASSUM (fun th-> MRESA1_TAC th`w:real^3`)
1846 THEN MRESA_TAC Planarity.aff_gt_inter_aff_gt[`vec 0:real^3`;`v:real^3`;`w:real^3`]
1847 THEN MATCH_MP_TAC(SET_RULE`A SUBSET B==> A INTER C SUBSET B`)
1848 THEN REWRITE_TAC[SUBSET]
1849 THEN REPEAT STRIP_TAC
1850 THEN MRESA_TAC Planarity.aff_gt_imp_not_collinear[`vec 0:real^3`;`w:real^3`;`v:real^3`;`x:real^3`]
1851 THEN MRESA_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`(rho_node1 FF v)`;`w:real^3`;`x:real^3`]
1852 THEN REWRITE_TAC[wedge;IN_ELIM_THM]
1853 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])
1854 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_RHO_NODE_PROS
1855 THEN POP_ASSUM MP_TAC
1856 THEN STRIP_TAC
1857 THEN REMOVE_ASSUM_TAC
1858 THEN POP_ASSUM (fun th-> MRESA1_TAC th`vv':real^3`)
1859 THEN MRESA_TAC (GEN_ALL Local_lemmas.IVS_RHO_NODE1_DETE)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`d:real^3`]
1860 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]);
1861 MRESA_TAC (GEN_ALL PROPERTIES_AFF_GT_SUBSET_WEDGE)
1862 [`V:real^3->bool`;`FF:real^3#real^3->bool`;`v:real^3`;`w:real^3`;`E:(real^3->bool)->bool`;];
1863 POP_ASSUM MP_TAC
1864 THEN SUBGOAL_THEN`interior_angle1 (vec 0) FF v= bta (k-1)` ASSUME_TAC;
1865 ASSUME_TAC2 Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
1866 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
1867 THEN EXPAND_TAC"bta"
1868 THEN EXPAND_TAC"vv"
1869 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
1870 THEN ASM_REWRITE_TAC[ITER1]
1871 THEN ASSUME_TAC2 CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS
1872 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`);
1873 ASSUME_TAC2 Local_lemmas.INTERIOR_ANGLE1_POS
1874 THEN POP_ASSUM MP_TAC
1875 THEN RESA_TAC
1876 THEN STRIP_TAC
1877 THEN SUBGOAL_THEN`?i. i< k-1/\ bta i= &0 /\ bta (i+1)= bta (k-1)` ASSUME_TAC;
1878 ONCE_REWRITE_TAC[SET_RULE`A= ~(~A)`]
1879 THEN STRIP_TAC
1880 THEN UNDISCH_TAC`CARD (V:real^3->bool) = k`
1881 THEN POP_ASSUM MP_TAC
1882 THEN REWRITE_TAC[NOT_EXISTS_THM;DE_MORGAN_THM]
1883 THEN STRIP_TAC
1884 THEN SUBGOAL_THEN`!i:num. i< k ==> bta i = &0` ASSUME_TAC;
1885 INDUCT_TAC;
1886 STRIP_TAC
1887 THEN EXPAND_TAC "bta"
1888 THEN EXPAND_TAC "vv"
1889 THEN REWRITE_TAC[ITER;Local_lemmas.AZIM_SPEC_DEGENERATE];
1890 REWRITE_TAC[ARITH_RULE`SUC i= i+1`]
1891 THEN POP_ASSUM MP_TAC
1892 THEN POP_ASSUM MP_TAC
1893 THEN POP_ASSUM MP_TAC
1894 THEN DISCH_THEN(LABEL_TAC"LINH1")
1895 THEN DISCH_THEN(LABEL_TAC"LINH2")
1896 THEN DISCH_THEN(LABEL_TAC"LINH3")
1897 THEN STRIP_TAC
1898 THEN MP_TAC(ARITH_RULE`i+1< k /\ 3<= k ==> i< k /\ (i< k-1)`)
1899 THEN RESA_TAC
1900 THEN REMOVE_THEN "LINH3" MP_TAC
1901 THEN RESA_TAC
1902 THEN REMOVE_THEN "LINH2"(fun th-> MRESA1_TAC th `i:num`)
1903 THEN REMOVE_THEN "LINH1"(fun th-> MRESA1_TAC th `i+1:num`);
1904 POP_ASSUM MP_TAC
1905 THEN DISCH_THEN(LABEL_TAC"LINH1")
1906 THEN STRIP_TAC
1907 THEN MP_TAC(ARITH_RULE`3<= k==> k-1< k/\ 0< k`)
1908 THEN RESA_TAC
1909 THEN REMOVE_THEN "LINH1"(fun th-> MRESA1_TAC th`k-1:num`)
1910 THEN MP_TAC(REAL_ARITH`&0< bta(k-1)==> ~(bta(k-1)= &0)`)
1911 THEN ASM_REWRITE_TAC[];
1912 POP_ASSUM MP_TAC
1913 THEN STRIP_TAC
1914 THEN MP_TAC(ARITH_RULE`i< k-1 ==> i< k`)
1915 THEN RESA_TAC
1916 THEN SUBGOAL_THEN`!j. 0 < j /\ j < k /\ ~(j=i) /\ ~(j=i+1)
1917 ==> interior_angle1 (vec 0) FF (ITER j (rho_node1 FF) v) = pi` ASSUME_TAC;
1918 REPEAT STRIP_TAC
1919 THEN POP_ASSUM MP_TAC
1920 THEN ONCE_REWRITE_TAC[ARITH_RULE`~(j=i+1)<=> (j< i+1\/ i+1< j)`]
1921 THEN MP_TAC(ARITH_RULE`~(j=i:num)<=> (j< i\/ i< j)`)
1922 THEN ASM_REWRITE_TAC[ARITH_RULE`((j < i \/ i < j)
1923 /\(j < i + 1 \/ i + 1 < j)) <=> (j < i \/ i + 1 < j:num)`; SET_RULE`A==>B==>C <=> A/\B ==>C`]
1924 THEN REMOVE_ASSUM_TAC
1925 THEN STRIP_TAC;
1926 MRESA_TAC (GEN_ALL EGHNAVX)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`bta:num->real`;
1927 `FF:real^3#real^3->bool`; `i:num`;`v:real^3`;`vv:num->real^3`;`CARD (V:real^3->bool)`]
1928 THEN POP_ASSUM MP_TAC
1929 THEN EXPAND_TAC "bta"
1930 THEN REWRITE_TAC[]
1931 THEN EXPAND_TAC "vv"
1932 THEN REWRITE_TAC[]
1933 THEN STRIP_TAC
1934 THEN REMOVE_ASSUM_TAC
1935 THEN REMOVE_ASSUM_TAC
1936 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`);
1937 MP_TAC(ARITH_RULE` i<k-1==> i+1=k-1\/ (i+1< k-1 /\ 0< i+1)`)
1938 THEN RESA_TAC;
1939 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
1940 THEN POP_ASSUM MP_TAC
1941 THEN POP_ASSUM MP_TAC
1942 THEN UNDISCH_TAC`3<= (k:num)`
1943 THEN ARITH_TAC;
1944 MRESA_TAC (GEN_ALL EGHNAVX)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`bta:num->real`;
1945 `FF:real^3#real^3->bool`; `i+1:num`;`v:real^3`;`vv:num->real^3`;`CARD (V:real^3->bool)`]
1946 THEN POP_ASSUM MP_TAC
1947 THEN EXPAND_TAC "bta"
1948 THEN REWRITE_TAC[]
1949 THEN EXPAND_TAC "vv"
1950 THEN REWRITE_TAC[]
1951 THEN STRIP_TAC
1952 THEN REMOVE_ASSUM_TAC
1953 THEN POP_ASSUM (fun th-> MRESA1_TAC th`j:num`);
1954 ASSUME_TAC2 Local_lemmas.LOFA_IMP_LT_CARD_SET_V
1955 THEN ABBREV_TAC`u=(ITER i (rho_node1 FF) v)`
1956 THEN ABBREV_TAC`w=(ITER (i+1) (rho_node1 FF) v)`
1957 THEN ABBREV_TAC`s={v,u,w:real^3}`
1958 THEN SUBGOAL_THEN`s SUBSET V:real^3->bool` ASSUME_TAC;
1959 EXPAND_TAC"s"
1960 THEN EXPAND_TAC"V"
1961 THEN REWRITE_TAC[SET_RULE`{A,B,C} SUBSET V<=> A IN V /\ B IN V /\ C IN V`;IN_ELIM_THM]
1962 THEN STRIP_TAC;
1963 EXISTS_TAC`0:num`
1964 THEN REWRITE_TAC[ITER;]
1965 THEN ASM_REWRITE_TAC[]
1966 THEN UNDISCH_TAC`3<=k`
1967 THEN ARITH_TAC;
1968 STRIP_TAC;
1969 EXISTS_TAC `i:num`
1970 THEN ASM_REWRITE_TAC[];
1971 EXISTS_TAC `i+1:num`
1972 THEN ASM_REWRITE_TAC[]
1973 THEN UNDISCH_TAC`i < k - 1:num`
1974 THEN ARITH_TAC;
1975 SUBGOAL_THEN`(!x. x IN V /\ ~(x IN s) ==> (\v. interior_angle1 (vec 0) FF v - pi) x = &0)` ASSUME_TAC;
1976 EXPAND_TAC"V"
1977 THEN REWRITE_TAC[IN_ELIM_THM]
1978 THEN ASM_REWRITE_TAC[]
1979 THEN REPEAT STRIP_TAC
1980 THEN POP_ASSUM MP_TAC
1981 THEN POP_ASSUM MP_TAC
1982 THEN DISJ_CASES_TAC(ARITH_RULE`n' = 0 \/ 0< (n':num)`);
1983 ASM_REWRITE_TAC[ITER]
1984 THEN RESA_TAC
1985 THEN EXPAND_TAC"s"
1986 THEN SET_TAC[];
1987 DISJ_CASES_TAC(ARITH_RULE`n' = i \/ ~(n':num=i)`);
1988 ASM_REWRITE_TAC[ITER]
1989 THEN RESA_TAC
1990 THEN EXPAND_TAC"s"
1991 THEN SET_TAC[];
1992 DISJ_CASES_TAC(ARITH_RULE`n' = i+1 \/ ~(n':num=i+1)`);
1993 ASM_REWRITE_TAC[ITER]
1994 THEN RESA_TAC
1995 THEN EXPAND_TAC"s"
1996 THEN SET_TAC[];
1997 REPEAT STRIP_TAC
1998 THEN UNDISCH_TAC`!j. 0 < j /\ j < k /\ ~(j = i) /\ ~(j = i + 1)
1999 ==> interior_angle1 (vec 0) FF (ITER j (rho_node1 FF) v) = pi`
2000 THEN STRIP_TAC
2001 THEN POP_ASSUM(fun th-> MRESA1_TAC th`n':num`)
2002 THEN REAL_ARITH_TAC;
2003 MRESA_TAC SUM_SUPERSET[`(\v:real^3. interior_angle1 (vec 0) FF v - pi)`;`s:real^3->bool`;`V:real^3->bool`]
2004 THEN REMOVE_ASSUM_TAC
2005 THEN REMOVE_ASSUM_TAC
2006 THEN POP_ASSUM MP_TAC
2007 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th; ])
2008 THEN REWRITE_TAC[SET_RULE`{A,B,C} SUBSET V <=> A IN V /\ B IN V /\ C IN V`]
2009 THEN STRIP_TAC
2010 THEN DISJ_CASES_TAC(ARITH_RULE`i = 0 \/ 0< (i:num)`);
2011 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th; ARITH_RULE`0+1=1`]
2012 THEN REPEAT STRIP_TAC)
2013 THEN UNDISCH_TAC`bta 1 = bta (k - 1):real`
2014 THEN UNDISCH_TAC `&0 < bta (k - 1):real`
2015 THEN MRESA_TAC( GEN_ALL Local_lemmas.FIRST_EQ0_LAST_LT_PI)
2016 [`E:(real^3->bool)->bool`;`V:real^3->bool`;
2017 `FF:real^3#real^3->bool`;`v:real^3`;`vv:num->real^3`; `bta:num->real`;`CARD (V:real^3->bool)`]
2018 THEN POP_ASSUM MP_TAC
2019 THEN EXPAND_TAC "bta"
2020 THEN REWRITE_TAC[]
2021 THEN EXPAND_TAC "vv"
2022 THEN REWRITE_TAC[]
2023 THEN STRIP_TAC
2024 THEN ASM_REWRITE_TAC[]
2025 THEN REAL_ARITH_TAC;
2026 MP_TAC(ARITH_RULE`i< k-1==> i+1< k`)
2027 THEN RESA_TAC
2028 THEN ASSUME_TAC2 Local_lemmas.LOFA_IMP_DIS_ELMS23
2029 THEN POP_ASSUM (fun th-> MRESAL_TAC th[`0`;`i:num`][ITER] THEN MRESAL_TAC th[`0`;`i+1:num`][ITER;ARITH_RULE`0< i+1`] THEN MRESAL_TAC th[`i:num`;`i+1:num`][ARITH_RULE`i<i+1`])
2030 THEN UNDISCH_TAC`interior_angle1 (vec 0) FF v = bta (k - 1):real`
2031 THEN STRIP_TAC
2032 THEN REMOVE_ASSUM_TAC
2033 THEN SIMP_TAC[HAS_SIZE; SUM_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
2034 IN_INSERT; NOT_IN_EMPTY]
2035 THEN ASM_REWRITE_TAC[]
2036 THEN MRESAL_TAC(GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`v:real^3`;][SET_RULE`A IN {A,B,C}`]
2037 THEN MRESAL_TAC(GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` u:real^3`;][SET_RULE`B IN {A,B,C}`]
2038 THEN MRESAL_TAC(GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` w:real^3`;][SET_RULE`C IN {A,B,C}`]
2039 THEN DISJ_CASES_TAC(SET_RULE`(?v1. v1 IN {v,u,w} /\ pi <= interior_angle1 (vec 0) FF v1)\/ ~(?v1. v1 IN {v,u,w} /\ pi <= interior_angle1 (vec 0) FF v1)`);
2040 POP_ASSUM MP_TAC
2041 THEN ASM_REWRITE_TAC[SET_RULE`A IN {B,C,D}<=> A=B \/ A=C\/ A=D`]
2042 THEN STRIP_TAC
2043 THEN POP_ASSUM MP_TAC
2044 THEN POP_ASSUM(fun th-> REWRITE_TAC[th])
2045 THEN POP_ASSUM MP_TAC
2046 THEN POP_ASSUM MP_TAC
2047 THEN POP_ASSUM MP_TAC
2048 THEN REAL_ARITH_TAC;
2049 POP_ASSUM MP_TAC
2050 THEN POP_ASSUM MP_TAC
2051 THEN POP_ASSUM MP_TAC
2052 THEN POP_ASSUM MP_TAC
2053 THEN ASM_REWRITE_TAC[NOT_EXISTS_THM;DE_MORGAN_THM; REAL_ARITH`~(a<= b) <=> b<a`]
2054 THEN ASSUME_TAC2 CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS
2055 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`v:real^3`[SET_RULE`A IN {A,B,C}`]
2056 THEN MRESAL1_TAC th`u:real^3`[SET_RULE`B IN {A,B,C}`]
2057 THEN MRESAL1_TAC th`w:real^3`[SET_RULE`C IN {A,B,C}`])
2058 THEN REPEAT STRIP_TAC
2059 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`u:real^3`[SET_RULE`B IN {A,B,C}`]
2060 THEN MRESAL1_TAC th`w:real^3`[SET_RULE`C IN {A,B,C}`])
2061 THEN UNDISCH_TAC`interior_angle1 (vec 0) FF v < pi`
2062 THEN RESA_TAC
2063 THEN SUBGOAL_THEN`u IN aff_gt {vec 0, v} {rho_node1 FF v}` ASSUME_TAC;
2064 MRESA_TAC (GEN_ALL EGHNAVX)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`bta:num->real`;
2065 `FF:real^3#real^3->bool`; `i:num`;`v:real^3`;`vv:num->real^3`;`CARD (V:real^3->bool)`]
2066 THEN POP_ASSUM MP_TAC
2067 THEN EXPAND_TAC "bta"
2068 THEN REWRITE_TAC[]
2069 THEN EXPAND_TAC "vv"
2070 THEN REWRITE_TAC[]
2071 THEN STRIP_TAC
2072 THEN REMOVE_ASSUM_TAC
2073 THEN SUBGOAL_THEN`u IN {ITER k (rho_node1 FF) v | 0 < k /\ k <= i}` ASSUME_TAC;
2074 REWRITE_TAC[IN_ELIM_THM]
2075 THEN EXISTS_TAC`i:num`
2076 THEN ASM_REWRITE_TAC[]
2077 THEN ARITH_TAC;
2078 MP_TAC(SET_RULE`{ITER k (rho_node1 FF) v | 0 < k /\ k <= i} SUBSET
2079 aff_gt {vec 0, v} {ITER 1 (rho_node1 FF) v} /\ u IN {ITER k (rho_node1 FF) v | 0 < k /\ k <= i} ==> u IN aff_gt {vec 0, v} {ITER 1 (rho_node1 FF) v}`)
2080 THEN ASM_REWRITE_TAC[ITER1];
2081 SUBGOAL_THEN`w IN aff_gt {vec 0, v} {ivs_rho_node1 FF v}` ASSUME_TAC;
2082 ASSUME_TAC2 Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
2083 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
2084 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2085 THEN MP_TAC(ARITH_RULE` i<k-1==> i+1=k-1\/ (i+1< k-1 /\ 0< i+1)`)
2086 THEN RESA_TAC;
2087 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2088 THEN ASM_REWRITE_TAC[]
2089 THEN MATCH_MP_TAC Local_lemmas.DISJOINT_IMP_Z_IN_AFF_GT
2090 THEN ASM_REWRITE_TAC[SET_RULE`DISJOINT {A,B}{C}<=> ~(A=C) /\ ~(B=C)`]
2091 THEN UNDISCH_TAC`!v':real^3. v' IN V /\ ~(v' = v) ==> ~collinear {vec 0, v, v'}`
2092 THEN STRIP_TAC
2093 THEN POP_ASSUM(fun th-> MRESA1_TAC th`w:real^3`)
2094 THEN MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`w:real^3`];
2095 MRESA_TAC (GEN_ALL EGHNAVX)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`bta:num->real`;
2096 `FF:real^3#real^3->bool`; `i+1:num`;`v:real^3`;`vv:num->real^3`;`CARD (V:real^3->bool)`]
2097 THEN POP_ASSUM MP_TAC
2098 THEN EXPAND_TAC "bta"
2099 THEN REWRITE_TAC[]
2100 THEN EXPAND_TAC "vv"
2101 THEN REWRITE_TAC[]
2102 THEN STRIP_TAC
2103 THEN SUBGOAL_THEN`w IN {ITER n (rho_node1 FF) v | i + 1 <= n /\ n < k}` ASSUME_TAC;
2104 REWRITE_TAC[IN_ELIM_THM]
2105 THEN EXISTS_TAC`i+1:num`
2106 THEN ASM_REWRITE_TAC[]
2107 THEN ARITH_TAC;
2108 POP_ASSUM MP_TAC
2109 THEN POP_ASSUM MP_TAC
2110 THEN SET_TAC[];
2111 UNDISCH_TAC`!v':real^3. v' IN V /\ ~(v' = v) ==> ~collinear {vec 0, v, v'}`
2112 THEN STRIP_TAC
2113 THEN POP_ASSUM(fun th-> MRESA1_TAC th`w:real^3` THEN MRESA1_TAC th`u:real^3` THEN ASSUME_TAC th)
2114 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2
2115 THEN ASSUME_TAC Local_lemmas.LOFA_IMP_NOT_COLL_IVS
2116 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
2117 THEN MRESA_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`rho_node1 FF v`;`ivs_rho_node1 FF v`;`w:real^3`]
2118 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2119 THEN MRESA_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`w:real^3`;`rho_node1 FF v`;`u:real^3`;]
2120 THEN MP_TAC(REAL_ARITH`&0 < azim (vec 0) v (rho_node1 FF v) w ==> ~(azim (vec 0) v (rho_node1 FF v) w= &0)`)
2121 THEN RESA_TAC
2122 THEN MRESA_TAC AZIM_COMPL[`vec 0:real^3`;`v:real^3`;`rho_node1 FF v`;`w:real^3`]
2123 THEN MP_TAC(REAL_ARITH` azim (vec 0) v (rho_node1 FF v) w < &2 * pi==> ~(&2 * pi - azim (vec 0) v (rho_node1 FF v) w = &0)`)
2124 THEN ASM_REWRITE_TAC[azim]
2125 THEN STRIP_TAC
2126 THEN MRESAL_TAC AZIM_COMPL[`vec 0:real^3`;`v:real^3`;`w:real^3`;`u:real^3`][REAL_ARITH`a-(a- B)=B`]
2127 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[SYM th] THEN REPEAT STRIP_TAC)
2128 THEN REMOVE_ASSUM_TAC
2129 THEN REMOVE_ASSUM_TAC
2130 THEN REMOVE_ASSUM_TAC
2131 THEN REMOVE_ASSUM_TAC
2132 THEN SUBGOAL_THEN`rho_node1 FF u= w` ASSUME_TAC;
2133 EXPAND_TAC"w"
2134 THEN REWRITE_TAC[ARITH_RULE`i+1= SUC i`;ITER]
2135 THEN ASM_REWRITE_TAC[];
2136 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2137 THEN SUBGOAL_THEN`ivs_rho_node1 FF w=u` ASSUME_TAC;
2138 EXPAND_TAC"w"
2139 THEN REWRITE_TAC[ARITH_RULE`i+1= SUC i`;ITER]
2140 THEN ASM_REWRITE_TAC[]
2141 THEN MRESA_TAC( GEN_ALL Local_lemmas.IVS_RHO_IDD)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` u:real^3`;];
2142 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2143 THEN SUBGOAL_THEN`!j. j< i==> aff_ge {vec 0:real^3} {v, vv (j+1)}= UNIONS {aff_ge {vec 0} {vv j1, vv (j1+1)}| j1 <= j}`ASSUME_TAC;
2144 INDUCT_TAC;
2145 STRIP_TAC
2146 THEN EXPAND_TAC"vv"
2147 THEN REWRITE_TAC[ARITH_RULE`j1<= 0<=> j1= 0`;ARITH_RULE`0+1=1`;ITER1;ITER;
2148 SET_RULE`UNIONS
2149 {aff_ge {vec 0} {ITER j1 (rho_node1 FF) v, ITER (j1 + 1) (rho_node1 FF) v} |
2150 j1 =
2151 0}= aff_ge {vec 0} {ITER 0 (rho_node1 FF) v, ITER (0 + 1) (rho_node1 FF) v}`];
2152 POP_ASSUM MP_TAC
2153 THEN DISCH_THEN(LABEL_TAC"LINH")
2154 THEN REPEAT STRIP_TAC
2155 THEN MP_TAC(ARITH_RULE`SUC j<i /\ i<k-1==> SUC j+1< k/\ j< i /\ j+1<k/\ SUC j <= i/\ SUC(SUC j)<= i /\ SUC j < k/\ SUC (SUC j)<k`)
2156 THEN RESA_TAC
2157 THEN REMOVE_THEN"LINH" MP_TAC
2158 THEN RESA_TAC
2159 THEN REWRITE_TAC[ARITH_RULE`j1<= SUC j <=> j1<= j \/ j1= SUC j`
2160 ;SET_RULE`UNIONS {aff_ge {vec 0} {vv j1, vv (j1 + 1)} | j1 <= j \/ j1 = SUC j}
2161 = UNIONS {aff_ge {vec 0} {vv j1, vv (j1 + 1)} | j1 <= j } UNION aff_ge {vec 0} {vv (SUC j), vv (SUC j + 1)}`]
2162 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;ARITH_RULE`SUC i= i+1`] THEN ASSUME_TAC (SYM th))
2163 THEN MATCH_MP_TAC AFF_GE_EQ_AFF_GE_UNION
2164 THEN ASSUME_TAC2 Local_lemmas.LOFA_IMP_CARD_FF_V_EQ
2165 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_DIS_ELMS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`SUC j+1:num`;`FF:real^3#real^3->bool`;` v:real^3`;]
2166 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`0:num`[ARITH_RULE`0< SUC j+1`;ITER])
2167 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_DIS_ELMS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`j+1:num`;`FF:real^3#real^3->bool`;` v:real^3`;]
2168 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`0:num`[ARITH_RULE`0< j+1`;ITER])
2169 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
2170 THEN EXPAND_TAC"vv"
2171 THEN UNDISCH_TAC`!v'. v' IN V /\ ~(v' = v) ==> ~collinear {vec 0, v, v':real^3}`
2172 THEN STRIP_TAC
2173 THEN POP_ASSUM(fun th-> MRESA1_TAC th`ITER (SUC j + 1) (rho_node1 FF) v` THEN ASSUME_TAC th)
2174 THEN POP_ASSUM(fun th-> MRESA1_TAC th`ITER (j + 1) (rho_node1 FF) v` THEN ASSUME_TAC th)
2175 THEN MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`ITER (j + 1) (rho_node1 FF) v`]
2176 THEN MRESAL_TAC th3[`vec 0:real^3`;`v:real^3`;`ITER (SUC j + 1) (rho_node1 FF) v`][ARITH_RULE`SUC i=i+1`]
2177 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2) [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` ITER (j + 1) (rho_node1 FF) v:real^3`;]
2178 THEN MRESA_TAC th3[`vec 0:real^3`;`ITER (j + 1) (rho_node1 FF) v:real^3`;`rho_node1 FF
2179 (ITER (j + 1) (rho_node1 FF) v)`]
2180 THEN REMOVE_ASSUM_TAC
2181 THEN POP_ASSUM MP_TAC
2182 THEN REWRITE_TAC[ARITH_RULE`j+1= SUC j`;ITER]
2183 THEN RESA_TAC
2184 THEN MRESA_TAC (GEN_ALL EGHNAVX)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`bta:num->real`;
2185 `FF:real^3#real^3->bool`; `i:num`;`v:real^3`;`vv:num->real^3`;`CARD (V:real^3->bool)`]
2186 THEN POP_ASSUM MP_TAC
2187 THEN EXPAND_TAC "bta"
2188 THEN REWRITE_TAC[]
2189 THEN EXPAND_TAC "vv"
2190 THEN REWRITE_TAC[]
2191 THEN STRIP_TAC
2192 THEN REMOVE_ASSUM_TAC
2193 THEN ABBREV_TAC`g=rho_node1 FF (ITER j (rho_node1 FF) v)`
2194 THEN SUBGOAL_THEN`g IN {ITER k (rho_node1 FF) v | 0 < k /\ k <= i}` ASSUME_TAC;
2195 REWRITE_TAC[IN_ELIM_THM]
2196 THEN EXISTS_TAC`SUC j`
2197 THEN ASM_REWRITE_TAC[ARITH_RULE`0< SUC j`;ITER];
2198 MP_TAC(SET_RULE` g IN {ITER k (rho_node1 FF) v | 0 < k /\ k <= i}
2199 /\ {ITER k (rho_node1 FF) v | 0 < k /\ k <= i} SUBSET
2200 aff_gt {vec 0, v} {ITER 1 (rho_node1 FF) v}
2201 ==> g IN
2202 aff_gt {vec 0, v} {ITER 1 (rho_node1 FF) v}`)
2203 THEN RESA_TAC
2204 THEN UNDISCH_TAC `~collinear {vec 0, v, ITER (j + 1) (rho_node1 FF) v}`
2205 THEN REWRITE_TAC[ARITH_RULE`j+1= SUC j`;ITER]
2206 THEN RESA_TAC
2207 THEN MRESAL_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`ivs_rho_node1 FF v`;`ITER 1 (rho_node1 FF) v`;`g:real^3`][ITER1]
2208 THEN SUBGOAL_THEN`rho_node1 FF g IN {ITER k (rho_node1 FF) v | 0 < k /\ k <= i}` ASSUME_TAC;
2209 REWRITE_TAC[IN_ELIM_THM]
2210 THEN EXISTS_TAC`SUC (SUC j)`
2211 THEN ASM_REWRITE_TAC[ARITH_RULE`0< SUC j`;ITER];
2212 MP_TAC(SET_RULE` rho_node1 FF g IN {ITER k (rho_node1 FF) v | 0 < k /\ k <= i}
2213 /\ {ITER k (rho_node1 FF) v | 0 < k /\ k <= i} SUBSET
2214 aff_gt {vec 0, v} {ITER 1 (rho_node1 FF) v}
2215 ==> rho_node1 FF g IN
2216 aff_gt {vec 0, v} {ITER 1 (rho_node1 FF) v}`)
2217 THEN RESA_TAC
2218 THEN UNDISCH_TAC `~collinear {vec 0, v, ITER (SUC j + 1) (rho_node1 FF) v}`
2219 THEN REWRITE_TAC[ARITH_RULE`j+1= SUC j`;ITER]
2220 THEN RESA_TAC
2221 THEN MRESAL_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`ivs_rho_node1 FF v`;`ITER 1 (rho_node1 FF) v`;`rho_node1 FF g:real^3`][ITER1]
2222 THEN MRESAL_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`ivs_rho_node1 FF v`;`g:real^3`;`rho_node1 FF g:real^3`][ITER1]
2223 THEN MRESA_TAC AFF_GT_SUBSET_AFF_GE[`{vec 0, v:real^3}`;`{g:real^3}`]
2224 THEN MP_TAC(SET_RULE`rho_node1 FF g IN aff_gt {vec 0, v} { g}
2225 /\ aff_gt {vec 0, v} {g} SUBSET
2226 aff_ge {vec 0, v} {g}
2227 ==> rho_node1 FF g IN
2228 aff_ge {vec 0, v} {g}`)
2229 THEN RESA_TAC
2230 THEN MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`v:real^3`;`g:real^3`;` rho_node1 FF g:real^3`]
2231 THEN POP_ASSUM MP_TAC
2232 THEN UNDISCH_TAC`UNIONS {aff_ge {vec 0} {vv j1, vv (j1 + 1)} | j1 <= j} =
2233 aff_ge {vec 0:real^3} {v, vv (j + 1)}`
2234 THEN EXPAND_TAC "vv"
2235 THEN REWRITE_TAC[ARITH_RULE`j+1= SUC j`;ITER]
2236 THEN ASM_REWRITE_TAC[]
2237 THEN STRIP_TAC
2238 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;UNIONS;IN_ELIM_THM])
2239 THEN STRIP_TAC
2240 THEN POP_ASSUM MP_TAC
2241 THEN RESA_TAC
2242 THEN UNDISCH_TAC`local_fan (V:real^3->bool,E,FF)`
2243 THEN STRIP_TAC
2244 THEN POP_ASSUM(fun th-> MP_TAC th
2245 THEN REWRITE_TAC[local_fan;]
2246 THEN LET_TAC
2247 THEN STRIP_TAC
2248 THEN REMOVE_ASSUM_TAC
2249 THEN REMOVE_ASSUM_TAC
2250 THEN REMOVE_ASSUM_TAC
2251 THEN ASSUME_TAC th)
2252 THEN UNDISCH_TAC`!i. ITER i (rho_node1 FF) v IN V`
2253 THEN STRIP_TAC
2254 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC(SUC j)`[ITER] THEN MRESA1_TAC th`j1:num` )
2255 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_EE_TWO_ELMS
2256 )[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`rho_node1 FF (ITER j1 (rho_node1 FF) v)`;`ITER j1 (rho_node1 FF) v`]
2257 THEN MP_TAC(SET_RULE`EE (rho_node1 FF (ITER j1 (rho_node1 FF) v)) E =
2258 {rho_node1 FF (rho_node1 FF (ITER j1 (rho_node1 FF) v)), ITER j1
2259 (rho_node1 FF)
2260 v}
2261 ==> ITER j1
2262 (rho_node1 FF)
2263 v IN EE (rho_node1 FF (ITER j1 (rho_node1 FF) v)) E `)
2264 THEN REWRITE_TAC[EE;IN_ELIM_THM]
2265 THEN REWRITE_TAC[GSYM EE]
2266 THEN RESA_TAC
2267 THEN POP_ASSUM MP_TAC
2268 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2269 THEN STRIP_TAC
2270 THEN MP_TAC(ARITH_RULE`j1<= j==> j1< SUC(SUC j) /\ SUC j1< SUC(SUC j)`)
2271 THEN RESA_TAC
2272 THEN ASSUME_TAC2 Local_lemmas.LOFA_IMP_DIS_ELMS23
2273 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j1:num`;`SUC(SUC j)`;][ITER]
2274 THEN MRESAL_TAC th[`SUC j1:num`;`SUC(SUC j)`;][ITER])
2275 THEN MRESA_TAC (GEN_ALL Local_lemmas.FAN_IN_AFF_GE_IMP_EQ)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`vec 0:real^3`;`ITER j1 (rho_node1 FF) v`;`rho_node1 FF g`;`rho_node1 FF (ITER j1 (rho_node1 FF) v)`];
2276 POP_ASSUM MP_TAC
2277 THEN MP_TAC(ARITH_RULE`0< i==> i-1< i/\ i-1+1=i`)
2278 THEN RESA_TAC
2279 THEN STRIP_TAC
2280 THEN POP_ASSUM (fun th-> MRESA1_TAC th`i-1`)
2281 THEN SUBGOAL_THEN`ivs_rho_node1 FF u IN aff_ge {vec 0} {v,u}` ASSUME_TAC;
2282 POP_ASSUM MP_TAC
2283 THEN EXPAND_TAC"vv"
2284 THEN ASM_REWRITE_TAC[]
2285 THEN RESA_TAC
2286 THEN REWRITE_TAC[IN_ELIM_THM;UNIONS]
2287 THEN EXISTS_TAC`aff_ge {vec 0}
2288 {ITER (i-1) (rho_node1 FF) v, ITER (i-1 + 1) (rho_node1 FF) v}`
2289 THEN STRIP_TAC;
2290 EXISTS_TAC`i-1:num`
2291 THEN ASM_REWRITE_TAC[ARITH_RULE`A-1<=A-1`];
2292 ASM_REWRITE_TAC[]
2293 THEN MRESA_TAC( GEN_ALL Local_lemmas.LOFA_IMP_NOT_COLL_IVS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`u:real^3`]
2294 THEN POP_ASSUM MP_TAC
2295 THEN ASSUME_TAC2 Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
2296 THEN POP_ASSUM(fun th-> MRESA1_TAC th`u:real^3`)
2297 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2298 THEN EXPAND_TAC"u"
2299 THEN REWRITE_TAC[ITER_ADD; ]
2300 THEN MP_TAC(ARITH_RULE`0<i /\ 3<= k ==>k -1 + i = k + (i-1)`)
2301 THEN RESA_TAC
2302 THEN ONCE_REWRITE_TAC[GSYM ITER_ADD; ]
2303 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
2304 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i-1:num`)
2305 THEN ASSUME_TAC2 Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID
2306 THEN POP_ASSUM(fun th-> MRESA1_TAC th`ITER (i - 1) (rho_node1 FF) v`)
2307 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2308 THEN STRIP_TAC
2309 THEN MRESA_TAC Planarity.point_in_aff_ge[`vec 0:real^3`;`ITER (i - 1) (rho_node1 FF) v`;`u:real^3`];
2310 ASSUME_TAC2 Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
2311 THEN POP_ASSUM (fun th-> MRESA1_TAC th`u:real^3`)
2312 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V)[`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`u:real^3`;`V:real^3->bool`]
2313 THEN POP_ASSUM(fun th-> MRESA1_TAC th`k-1:num`)
2314 THEN SUBGOAL_THEN`azim (vec 0) u w (ivs_rho_node1 FF u)= azim (vec 0) u w v` ASSUME_TAC;
2315 DISJ_CASES_TAC(SET_RULE`v= ivs_rho_node1 FF u \/ ~(ivs_rho_node1 FF u= v)`);
2316 ASM_REWRITE_TAC[];
2317 UNDISCH_TAC`!v':real^3. v' IN V /\ ~(v' = v) ==> ~collinear {vec 0, v, v'}`
2318 THEN STRIP_TAC
2319 THEN POP_ASSUM(fun th-> MRESA1_TAC th`ivs_rho_node1 FF u`)
2320 THEN MRESA_TAC Topology.aff_ge_inter_aff_ge[`vec 0:real^3`;`v:real^3`;`u:real^3`]
2321 THEN MP_TAC(SET_RULE`ivs_rho_node1 FF u IN aff_ge {vec 0} {v, u}
2322 /\ aff_ge {vec 0} {v, u} =
2323 aff_ge {vec 0, v} {u} INTER aff_ge {vec 0, u} {v}
2324 ==> ivs_rho_node1 FF u IN aff_ge {vec 0,u} { v}`)
2325 THEN RESA_TAC
2326 THEN MRESA_TAC( GEN_ALL Local_lemmas.LOFA_IMP_NOT_COLL_IVS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`u:real^3`]
2327 THEN MRESA_TAC AZIM_EQ_0_GE[`vec 0:real^3`;`u:real^3`;`ivs_rho_node1 FF u`;`v:real^3`]
2328 THEN POP_ASSUM MP_TAC
2329 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2330 THEN RESA_TAC
2331 THEN MRESAL_TAC Fan.sum5_azim_fan[`vec 0:real^3`;`u:real^3`;`w:real^3`;`(ivs_rho_node1 FF u)`;`v:real^3`][azim]
2332 THEN POP_ASSUM MP_TAC
2333 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2334 THEN ASM_REWRITE_TAC[]
2335 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2) [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` u:real^3`;]
2336 THEN POP_ASSUM MP_TAC
2337 THEN UNDISCH_TAC`ITER (i + 1) (rho_node1 FF) v = w`
2338 THEN REWRITE_TAC[ARITH_RULE`i+1=SUC i`;ITER]
2339 THEN RESA_TAC
2340 THEN RESA_TAC
2341 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2342 THEN RESA_TAC
2343 THEN REAL_ARITH_TAC;
2344 ASM_REWRITE_TAC[]
2345 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2346 THEN SUBGOAL_THEN`!j. j< k-i-1==> aff_ge {vec 0:real^3} {v, vv (k-j-1)}= UNIONS {aff_ge {vec 0} {vv (k-j1-1), vv (k-j1)}| j1 <= j}`ASSUME_TAC;
2347 INDUCT_TAC;
2348 STRIP_TAC
2349 THEN EXPAND_TAC"vv"
2350 THEN ASSUME_TAC2 Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID
2351 THEN REWRITE_TAC[ARITH_RULE`j1<= 0<=> j1= 0`;ARITH_RULE`k-0=k`;ITER1;ITER;
2352 SET_RULE`UNIONS
2353 {aff_ge {vec 0}
2354 {ITER (k - j1 - 1) (rho_node1 FF) v, ITER (k - j1) (rho_node1 FF) v} |
2355 j1 =
2356 0}= aff_ge {vec 0}
2357 {ITER (k - 0 - 1) (rho_node1 FF) v, ITER (k - 0) (rho_node1 FF) v}`]
2358 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
2359 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`]
2360 THEN REWRITE_TAC[];
2361 POP_ASSUM MP_TAC
2362 THEN DISCH_THEN(LABEL_TAC"LINH")
2363 THEN REPEAT STRIP_TAC
2364 THEN MP_TAC(ARITH_RULE`SUC j<k-i-1 /\ 0<i /\i<k-1==> i+1< k-SUC j/\ j< k-i-1/\ k-j-1-1<k /\ 0< k-j-1-1 /\ k-j-1< k /\ 0< k-j-1`)
2365 THEN RESA_TAC
2366 THEN REMOVE_THEN"LINH" MP_TAC
2367 THEN RESA_TAC
2368 THEN REWRITE_TAC[ARITH_RULE`j1<= SUC j <=> j1<= j \/ j1= SUC j`
2369 ;SET_RULE`UNIONS
2370 {aff_ge {vec 0} {vv (k - j1 - 1), vv (k - j1)} | j1 <= j \/ j1 = SUC j }
2371 = UNIONS
2372 {aff_ge {vec 0} {vv (k - j1 - 1), vv (k - j1)} | j1 <= j} UNION aff_ge {vec 0} {vv (k-SUC j-1), vv (k-SUC j)}`]
2373 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;ARITH_RULE`SUC i= i+1`] THEN ASSUME_TAC (SYM th))
2374 THEN GEN_REWRITE_TAC(RAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`]
2375 THEN REWRITE_TAC[ARITH_RULE`k-(j+1)=k-j-1`]
2376 THEN MATCH_MP_TAC AFF_GE_EQ_AFF_GE_UNION
2377 THEN ASSUME_TAC2 Local_lemmas.LOFA_IMP_CARD_FF_V_EQ
2378 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_DIS_ELMS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`k-j-1-1:num`;`FF:real^3#real^3->bool`;` v:real^3`;]
2379 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`0:num`[ITER])
2380 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_DIS_ELMS)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`k-j-1:num`;`FF:real^3#real^3->bool`;` v:real^3`;]
2381 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`0:num`[ARITH_RULE`0< j+1`;ITER])
2382 THEN ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V
2383 THEN EXPAND_TAC"vv"
2384 THEN UNDISCH_TAC`!v'. v' IN V /\ ~(v' = v) ==> ~collinear {vec 0, v, v':real^3}`
2385 THEN STRIP_TAC
2386 THEN POP_ASSUM(fun th-> MRESA1_TAC th`ITER (k-j - 1-1) (rho_node1 FF) v` THEN ASSUME_TAC th)
2387 THEN POP_ASSUM(fun th-> MRESA1_TAC th`ITER (k-j-1) (rho_node1 FF) v` THEN ASSUME_TAC th)
2388 THEN MRESA_TAC th3[`vec 0:real^3`;`v:real^3`;`ITER (k-j-1 - 1) (rho_node1 FF) v`]
2389 THEN MRESAL_TAC th3[`vec 0:real^3`;`v:real^3`;`ITER (k-j-1) (rho_node1 FF) v`][ARITH_RULE`SUC i=i+1`]
2390 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2) [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` ITER (k-j-1- 1) (rho_node1 FF) v:real^3`;]
2391 THEN MRESA_TAC th3[`vec 0:real^3`;`ITER (k-j -1- 1) (rho_node1 FF) v:real^3`;`rho_node1 FF
2392 (ITER (k-j - 1-1) (rho_node1 FF) v)`]
2393 THEN REMOVE_ASSUM_TAC
2394 THEN POP_ASSUM MP_TAC
2395 THEN MP_TAC(ARITH_RULE`0< k - j - 1 - 1 ==> SUC (k - j - 1 - 1)= k-j-1`)
2396 THEN RESA_TAC
2397 THEN REWRITE_TAC[GSYM ITER]
2398 THEN RESA_TAC
2399 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2400 THEN ASM_REWRITE_TAC[]
2401 THEN MP_TAC(ARITH_RULE` i<k-1==> i+1=k-1\/ (i+1< k-1 /\ 0< i+1)`)
2402 THEN RESA_TAC;
2403 UNDISCH_TAC`SUC j < k - i -1`
2404 THEN POP_ASSUM MP_TAC
2405 THEN ARITH_TAC;
2406 ASSUME_TAC2 Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
2407 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
2408 THEN MRESA_TAC (GEN_ALL EGHNAVX)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`bta:num->real`;
2409 `FF:real^3#real^3->bool`; `i+1:num`;`v:real^3`;`vv:num->real^3`;`CARD (V:real^3->bool)`]
2410 THEN POP_ASSUM MP_TAC
2411 THEN EXPAND_TAC "bta"
2412 THEN REWRITE_TAC[]
2413 THEN EXPAND_TAC "vv"
2414 THEN REWRITE_TAC[]
2415 THEN STRIP_TAC
2416 THEN ABBREV_TAC`g=ITER (k-j-1-1) (rho_node1 FF) v`
2417 THEN SUBGOAL_THEN`ITER (k - j - 1) (rho_node1 FF) v= rho_node1 FF g` ASSUME_TAC;
2418 EXPAND_TAC"g"
2419 THEN REWRITE_TAC[GSYM ITER]
2420 THEN ASM_REWRITE_TAC[];
2421 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC THEN ASSUME_TAC th)
2422 THEN SUBGOAL_THEN`g IN {ITER n (rho_node1 FF) v | i+1 <= n /\ n < k}` ASSUME_TAC;
2423 REWRITE_TAC[IN_ELIM_THM]
2424 THEN EXISTS_TAC`k-j-1-1`
2425 THEN ASM_REWRITE_TAC[ARITH_RULE`0< SUC j`;ITER]
2426 THEN MP_TAC(ARITH_RULE`SUC j < k - i - 1 /\ 0<i==> i+1<= k-j-1-1`)
2427 THEN RESA_TAC;
2428 MP_TAC(SET_RULE` g IN {ITER n (rho_node1 FF) v | i+1<=n /\ n < k}
2429 /\ {ITER n (rho_node1 FF) v | i+1<=n /\ n < k} SUBSET
2430 aff_gt {vec 0, v} {ITER (k-1) (rho_node1 FF) v}
2431 ==> g IN
2432 aff_gt {vec 0, v} {ITER (k-1) (rho_node1 FF) v}`)
2433 THEN RESA_TAC
2434 THEN MRESAL_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`rho_node1 FF v`;`ITER (k-1) (rho_node1 FF) v`;`g:real^3`][ITER1]
2435 THEN SUBGOAL_THEN`rho_node1 FF g IN {ITER n (rho_node1 FF) v | i+1 <= n /\ n < k}` ASSUME_TAC;
2436 REWRITE_TAC[IN_ELIM_THM]
2437 THEN EXISTS_TAC`k-j-1`
2438 THEN ASM_REWRITE_TAC[ARITH_RULE`0< SUC j`;ITER]
2439 THEN MP_TAC(ARITH_RULE`SUC j < k - i - 1 /\ 0<i==> i+1<= k-j-1`)
2440 THEN RESA_TAC;
2441 MP_TAC(SET_RULE` rho_node1 FF g IN {ITER n (rho_node1 FF) v | i+1 <= n /\ n < k}
2442 /\ {ITER n (rho_node1 FF) v | i+1 <= n /\ n < k} SUBSET
2443 aff_gt {vec 0, v} {ITER (k-1) (rho_node1 FF) v}
2444 ==> rho_node1 FF g IN
2445 aff_gt {vec 0, v} {ITER(k-1) (rho_node1 FF) v}`)
2446 THEN RESA_TAC
2447 THEN MRESAL_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`rho_node1 FF v`;`ITER (k-1) (rho_node1 FF) v`;`rho_node1 FF g:real^3`][ITER1]
2448 THEN MRESAL_TAC AZIM_EQ[`vec 0:real^3`;`v:real^3`;`rho_node1 FF v`;`rho_node1 FF g:real^3`;`g:real^3`][ITER1]
2449 THEN MRESA_TAC AFF_GT_SUBSET_AFF_GE[`{vec 0, v:real^3}`;`{rho_node1 FF g:real^3}`]
2450 THEN MP_TAC(SET_RULE`g IN aff_gt {vec 0, v} {rho_node1 FF g}
2451 /\ aff_gt {vec 0, v} {rho_node1 FF g} SUBSET
2452 aff_ge {vec 0, v} {rho_node1 FF g}
2453 ==> g IN
2454 aff_ge {vec 0, v} {rho_node1 FF g}`)
2455 THEN RESA_TAC
2456 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2457 THEN MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`v:real^3`;` rho_node1 FF g:real^3`;` g:real^3`]
2458 THEN POP_ASSUM MP_TAC
2459 THEN UNDISCH_TAC`UNIONS {aff_ge {vec 0} {vv (k - j1 - 1), vv (k - j1)} | j1 <= j} =
2460 aff_ge {vec 0:real^3} {v, vv (k - j - 1)}`
2461 THEN EXPAND_TAC "vv"
2462 THEN ASM_REWRITE_TAC[]
2463 THEN STRIP_TAC
2464 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;UNIONS;IN_ELIM_THM])
2465 THEN STRIP_TAC
2466 THEN POP_ASSUM MP_TAC
2467 THEN RESA_TAC
2468 THEN UNDISCH_TAC`local_fan (V:real^3->bool,E,FF)`
2469 THEN STRIP_TAC
2470 THEN POP_ASSUM(fun th-> MP_TAC th
2471 THEN REWRITE_TAC[local_fan;]
2472 THEN LET_TAC
2473 THEN STRIP_TAC
2474 THEN REMOVE_ASSUM_TAC
2475 THEN REMOVE_ASSUM_TAC
2476 THEN REMOVE_ASSUM_TAC
2477 THEN ASSUME_TAC th)
2478 THEN UNDISCH_TAC`!i. ITER i (rho_node1 FF) v IN V`
2479 THEN STRIP_TAC
2480 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`k-j-1-1`[ITER] THEN MRESA1_TAC th`k-j1-1:num` )
2481 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_EE_TWO_ELMS
2482 )[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`rho_node1 FF (ITER (k-j1-1) (rho_node1 FF) v)`;`ITER (k-j1-1) (rho_node1 FF) v`]
2483 THEN MP_TAC(SET_RULE`EE (rho_node1 FF (ITER (k-j1-1) (rho_node1 FF) v)) E =
2484 {rho_node1 FF (rho_node1 FF (ITER (k-j1-1) (rho_node1 FF) v)), ITER (k-j1-1)
2485 (rho_node1 FF)
2486 v}
2487 ==> ITER (k-j1-1)
2488 (rho_node1 FF)
2489 v IN EE (rho_node1 FF (ITER (k-j1-1) (rho_node1 FF) v)) E `)
2490 THEN REWRITE_TAC[EE;IN_ELIM_THM]
2491 THEN REWRITE_TAC[GSYM EE]
2492 THEN RESA_TAC
2493 THEN POP_ASSUM MP_TAC
2494 THEN ASM_REWRITE_TAC[GSYM ITER]
2495 THEN MP_TAC(ARITH_RULE`j1<=j /\ SUC j< k-i-1 /\ 0<i ==> SUC (k-j1-1)= k-j1 /\ k-j-1-1< k-j1 /\ k-j-1-1< k-j1-1 /\ k-j1-1<k`)
2496 THEN RESA_TAC
2497 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
2498 THEN STRIP_TAC
2499 THEN ASSUME_TAC2 Local_lemmas.LOFA_IMP_DIS_ELMS23
2500 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`k-j-1-1:num`;`k-j1-1`;][ITER] THEN ASSUME_TAC th)
2501 THEN SUBGOAL_THEN`~(ITER (k - j1) (rho_node1 FF) v = g)` ASSUME_TAC;
2502 MP_TAC(ARITH_RULE`j < k - i - 1 /\ j1<=j /\ 0< i==> k-j1=k \/ k- j1< k`)
2503 THEN RESA_TAC;
2504 ASSUME_TAC2 Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID
2505 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`);
2506 POP_ASSUM MP_TAC
2507 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`k-j-1-1:num`;`k-j1:num`;][ITER] THEN ASSUME_TAC th)
2508 THEN POP_ASSUM MP_TAC
2509 THEN DISCH_THEN(LABEL_TAC"linh")
2510 THEN STRIP_TAC
2511 THEN REMOVE_THEN"linh" MP_TAC
2512 THEN RESA_TAC;
2513 MRESA_TAC (GEN_ALL Local_lemmas.FAN_IN_AFF_GE_IMP_EQ)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`vec 0:real^3`;`ITER (k-j1-1) (rho_node1 FF) v`;`g:real^3`;`ITER (k-j1) (rho_node1 FF) v`];
2514 POP_ASSUM MP_TAC
2515 THEN MP_TAC(ARITH_RULE`i< k-1/\ 0< i ==> k-i-1-1< k-i-1 /\ k - (k - i - 1 - 1) - 1= SUC(i) /\ k - (k - i - 1 - 1) = SUC(SUC i)`)
2516 THEN RESA_TAC
2517 THEN STRIP_TAC
2518 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k-i-1-1`[ARITH_RULE`SUC i=i+1`])
2519 THEN SUBGOAL_THEN`rho_node1 FF w IN aff_ge {vec 0} {v,w}` ASSUME_TAC ;
2520 POP_ASSUM MP_TAC
2521 THEN EXPAND_TAC"vv"
2522 THEN ASM_REWRITE_TAC[]
2523 THEN RESA_TAC
2524 THEN REWRITE_TAC[IN_ELIM_THM;UNIONS]
2525 THEN EXISTS_TAC`aff_ge {vec 0}
2526 {ITER (k-(k - i - 1 - 1)-1) (rho_node1 FF) v, ITER (k-(k - i - 1 - 1)) (rho_node1 FF) v}`
2527 THEN STRIP_TAC;
2528 EXISTS_TAC`k - i - 1 - 1:num`
2529 THEN ASM_REWRITE_TAC[ARITH_RULE`A-1<=A-1`];
2530 ASM_REWRITE_TAC[ARITH_RULE`SUC i=i+1`]
2531 THEN ONCE_REWRITE_TAC[ARITH_RULE`i+1= SUC i`]
2532 THEN ASM_REWRITE_TAC[ITER]
2533 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`w:real^3`]
2534 THEN MRESA_TAC Planarity.point_in_aff_ge[`vec 0:real^3`;`w:real^3`;`rho_node1 FF w:real^3`];
2535 SUBGOAL_THEN`azim (vec 0) w (rho_node1 FF w) u= azim (vec 0) w v u` ASSUME_TAC;
2536 DISJ_CASES_TAC(SET_RULE`v= rho_node1 FF w \/ ~(rho_node1 FF w= v)`);
2537 ASM_REWRITE_TAC[];
2538 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER
2539 THEN POP_ASSUM(fun th-> MRESA1_TAC th`w:real^3`)
2540 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`1`[ITER1])
2541 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)[`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;`w:real^3`]
2542 THEN UNDISCH_TAC`!v':real^3. v' IN V /\ ~(v' = v) ==> ~collinear {vec 0, v, v'}`
2543 THEN STRIP_TAC
2544 THEN POP_ASSUM(fun th-> MRESA1_TAC th`rho_node1 FF w`)
2545 THEN MRESA_TAC Topology.aff_ge_inter_aff_ge[`vec 0:real^3`;`v:real^3`;`w:real^3`]
2546 THEN MP_TAC(SET_RULE`rho_node1 FF w IN aff_ge {vec 0} {v, w}
2547 /\ aff_ge {vec 0} {v, w} =
2548 aff_ge {vec 0, v} {w} INTER aff_ge {vec 0, w} {v}
2549 ==> rho_node1 FF w IN aff_ge {vec 0,w} { v}`)
2550 THEN RESA_TAC
2551 THEN MRESA_TAC AZIM_EQ_0_GE[`vec 0:real^3`;`w:real^3`;`rho_node1 FF w`;`v:real^3`]
2552 THEN POP_ASSUM MP_TAC
2553 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2554 THEN RESA_TAC
2555 THEN MRESAL_TAC Fan.sum5_azim_fan[`vec 0:real^3`;`w:real^3`;`u:real^3`;`(rho_node1 FF w)`;`v:real^3`][azim]
2556 THEN POP_ASSUM MP_TAC
2557 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2558 THEN ASM_REWRITE_TAC[]
2559 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2)
2560 [`E:(real^3->bool)->bool`;`V:real^3->bool`;`FF:real^3#real^3->bool`;` u:real^3`;]
2561 THEN POP_ASSUM MP_TAC
2562 THEN UNDISCH_TAC`ITER (i + 1) (rho_node1 FF) v = w`
2563 THEN REWRITE_TAC[ARITH_RULE`i+1=SUC i`;ITER]
2564 THEN RESA_TAC
2565 THEN RESA_TAC
2566 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2567 THEN RESA_TAC
2568 THEN POP_ASSUM MP_TAC
2569 THEN REWRITE_TAC[REAL_ARITH`a+ &0=a`]
2570 THEN STRIP_TAC
2571 THEN MP_TAC(REAL_ARITH`&0< azim (vec 0) w (rho_node1 FF w) u ==> ~(azim (vec 0) w (rho_node1 FF w) u = &0)`)
2572 THEN RESA_TAC
2573 THEN MRESAL_TAC AZIM_COMPL[`vec 0:real^3`;`w:real^3`;`rho_node1 FF w:real^3`;`u:real^3`][REAL_ARITH`a-(a- B)=B`]
2574 THEN POP_ASSUM MP_TAC
2575 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2576 THEN RESA_TAC
2577 THEN MP_TAC(REAL_ARITH` azim (vec 0) w (rho_node1 FF w) u < &2 * pi ==> ~(&2 * pi - azim (vec 0) w (rho_node1 FF w) u = &0)`)
2578 THEN ASM_REWRITE_TAC[azim]
2579 THEN STRIP_TAC
2580 THEN MRESAL_TAC AZIM_COMPL[`vec 0:real^3`;`w:real^3`;`u:real^3`;`v:real^3`][REAL_ARITH`a-(a- B)=B`]
2581 THEN POP_ASSUM MP_TAC
2582 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
2583 THEN RESA_TAC;
2584 ASM_REWRITE_TAC[]
2585 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC)
2586 THEN MP_TAC(REAL_ARITH`&0< azim (vec 0) v u w /\ azim (vec 0) v u w < pi ==> ~(azim (vec 0) v u w = &0 \/ azim (vec 0) v u (w:real^3) = pi)`)
2587 THEN RESA_TAC
2588 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
2589 THEN POP_ASSUM (fun th->
2590 MP_TAC th THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
2591 THEN STRIP_TAC
2592 THEN MP_TAC th THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
2593 THEN STRIP_TAC
2594 THEN MP_TAC th THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,D,B}`]
2595 THEN STRIP_TAC
2596 THEN MP_TAC th THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,C,B}`]
2597 THEN STRIP_TAC
2598 THEN ASSUME_TAC th)
2599 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR [`vec 0:real^3`;`u:real^3`;`v:real^3`;`w:real^3`]
2600 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR [`vec 0:real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
2601 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR [`vec 0:real^3`;`w:real^3`;`v:real^3`;`u:real^3`]
2602 THEN MRESA_TAC NOT_COPLANAR_NOT_COLLINEAR [`vec 0:real^3`;`w:real^3`;`u:real^3`;`v:real^3`]
2603 THEN MRESA_TAC AZIM_DIVH [`vec 0:real^3`;`v:real^3`;`u:real^3`;`w:real^3`]
2604 THEN MRESA_TAC AZIM_DIVH [`vec 0:real^3`;`u:real^3`;`w:real^3`;`v:real^3`]
2605 THEN MRESA_TAC AZIM_DIVH [`vec 0:real^3`;`w:real^3`;`v:real^3`;`u:real^3`]
2606 THEN MRESAL_TAC VOLUME_SOLID_TRIANGLE[`&1:real`;`vec 0:real^3`;`v:real^3`;`u:real^3`;`w:real^3`][REAL_ARITH`&0< &1`]
2607 THEN POP_ASSUM MP_TAC
2608 THEN REPEAT LET_TAC
2609 THEN MRESA_TAC MEASURABLE_BALL_AFF_GT[`vec 0:real^3`;`&1`;`{vec 0:real^3}`;`{v,u,w:real^3}`]
2610 THEN STRIP_TAC
2611 THEN MP_TAC(MESON[volume_props]`measurable (ball (vec 0,&1) INTER aff_gt {vec 0} {v, u, w})==> vol (ball (vec 0,&1) INTER aff_gt {vec 0} {v, u, w}) >= &0`)
2612 THEN RESA_TAC
2613 THEN POP_ASSUM MP_TAC
2614 THEN REAL_ARITH_TAC]);;
2615
2616
2617
2618 end;;