legacy/oldtame/UBHDEUU.hl

   1 (* ========================================================================== *)\r
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)\r
   3 (*                                                                            *)\r
   4 (* Lemma: UBHDEUU                                                        *)\r
   5 (* Chapter: Tame Hypermap                                                  *)\r
   6 (* Author: DANG TAT DAT                                                    *)\r
   7 (* Date: 2010-02-26                                                           *)\r
   8 (* ========================================================================== *)\r
   9 \r
  10 (*\r
  11 \r
  12 (V,E_{std}) is a fan\r
  13 \r
  14 *)\r
  15 \r
  16 (* \r
  17 This file is in desperate need of revision.\r
  18 \r
  19 Uses CHEAT_TAC  throughout the file.\r
  20     Doesn't load with the current build.\r
  21     V is used first as a variable (as in the definition of fan11), then as a defined constant \r
  22       let V = new_definition `V = ....`.  \r
  23     This prevents it from being loaded again after the first attempt, and makes it incompatible\r
  24         with most other files.\r
  25     It defines other single character constants r,p,q,... that are liable to cause problems.\r
  26     Incompatible with flyspeck-svn-1581 hol_light-svn-14 as of Feb 26, 2010.\r
  27 \r
  28 The definitions do not appear to be the standard ones.\r
  29 \r
  30 -THales\r
  31 \r
  32 *)\r
  33 \r
  34 \r
  35 module  Ubhdeuu = struct\r
  36 \r
  37 \r
  38 \r
  39 (* # use "hol.ml";;  *)\r
  40 (* needs "Multivariate/flyspeck.ml";; *)\r
  41 (* needs "update_database_310.ml";; *)\r
  42 (*  needs "hypermap.ml";; *)\r
  43 \r
  44 flyspeck_needs "general/sphere.hl";;\r
  45 flyspeck_needs "fan/fan_defs.hl";;\r
  46 \r
  47 prioritize_real();;\r
  48 \r
  49 (* Fan definition*)\r
  50 let graph = Fan.graph;;\r
  51 \r
  52 \r
  53 (* new_definition `graph (E:(real^3 ->bool)->bool)  <=>  (!e. E e ==> (e HAS_SIZE 2))`;; *)\r
  54 \r
  55 let fan11 = new_definition `fan11 (V:real^3 -> bool)  <=>  FINITE V`;;\r
  56 \r
  57 let fan21 = new_definition `fan21 (x:real^3,V:real^3 -> bool)  <=>   ~(x IN V)`;;\r
  58 \r
  59 let fan31 = new_definition `fan31 (V:real^3 -> bool,E:(real^3 ->bool)->bool) = E UNION {{v}| v IN V}`;;\r
  60 \r
  61 let fan41 = new_definition `fan41 (x:real^3,E:(real^3 ->bool)->bool) <=>(!e. (e IN E) ==> ~(collinear({x} UNION e)))`;;\r
  62  \r
  63 let fan51 = new_definition `fan51 (x:real^3,V:real^3 -> bool,E:(real^3 ->bool)->bool) <=> (!e1 e2. (e1 IN fan31(V,E)) /\(e2 IN fan31(V,E))==> ((aff_ge {x} e1) INTER (aff_ge {x} e2) = aff_ge {x} (e1 INTER e2)))`;;\r
  64 \r
  65 let new_fan = new_definition `new_fan(x:real^3,V,E) <=> ((UNIONS E) SUBSET V) /\ graph(E) /\ fan11(V) /\ fan21(x,V) /\ fan41(x,E) /\ fan51(x,V,E)`;;\r
  66 \r
  67 \r
  68 (*Contravening Hypermap*)\r
  69 \r
  70 (* Changed packing to a thm rather than a definition to make it compatible \r
  71    with definition in Sphere.packing -Feb 2010, thales *)\r
  72 \r
  73 let packing = prove( `packing (S:real^3 -> bool) = (!u v. (u IN S) /\ (v IN S) /\ ~(u = v) ==> (&2 <= dist( u, v)))`,REWRITE_TAC[IN;Sphere.packing]);;\r
  74 \r
  75 \r
  76 let h0 = new_definition `h0 = #1.26`;;  (*Definition Const real number*)\r
  77 \r
  78 let V = new_definition `V (x:real^3) (S:real^3 -> bool) = {v:real^3|(v IN S) /\ (x IN S) /\ ~(v = x) /\ (dist(v,x) <= (&2)*h0)}`;;\r
  79 \r
  80 let ESTD = new_definition `ESTD (V (x:real^3) (S:real^3 -> bool)) = {{v,w}|(v IN (V x S)) /\ (w IN (V x S))/\ ~(v = w) /\ dist(v,w) <= (&2)*h0}`;;\r
  81 \r
  82 let ECNT = new_definition `ECNT (V (x:real^3) (S:real^3 -> bool)) = {{v,w}|(v IN (V x S)) /\ (w IN (V x S))/\ ~(v = w) /\ dist(v,w) = &2}`;;\r
  83 \r
  84 (* UBHDEUU*)\r
  85 \r
  86 (* Let Proof (x,V,ESTD) is a fan*)\r
  87 let them1 = prove(`!x (y:real^3)(S:real^3 -> bool).(packing S) /\ (x IN S) /\ (y IN S)/\ ~(x = y) ==> (&2 <= dist(x,y))`,REWRITE_TAC [packing] THEN REPEAT STRIP_TAC THEN ASM_MESON_TAC [packing]);;\r
  88 \r
  89 let cautruc1 = prove (`!(x:real^3)(S:real^3->bool).(packing S) /\ (x IN S) ==> (V x S) SUBSET (S INTER (ball(x,(&2*h0 + &1))))`,REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC [ball;V;SUBSET;INTER] THEN STRIP_TAC THEN REWRITE_TAC [IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN SUBGOAL_THEN `&2 * h0 < &2 * h0 + &1` ASSUME_TAC THENL [ARITH_TAC;SUBGOAL_THEN `dist(x':real^3,x:real^3) < &2 * h0 + &1` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `dist(x':real^3,x:real^3) = dist(x,x')` ASSUME_TAC THENL [MESON_TAC [DIST_SYM];ASM_ARITH_TAC]]]);;\r
  90 \r
  91 (* USE the lemma5.1( KIUMVTC) *)\r
  92 let KIUMVTC = prove (`!(x:real^3) (b:real) (S:real^3 -> bool). &0 <= b /\ packing S ==> FINITE (S INTER ball (x,b))`, CHEAT_TAC);;\r
  93 \r
  94 let cautruc2 = prove(`!(x:real^3)(S:real^3 -> bool).  (x IN S)/\ (packing S) ==> FINITE (S INTER (ball(x,(&2*h0 + &1))))`,REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `&0 <= &2*h0 + &1` ASSUME_TAC THENL [REWRITE_TAC [h0] THEN ARITH_TAC;ASM_MESON_TAC [KIUMVTC]]);;\r
  95 \r
  96 let them2 = prove(`!(x:real^3) (y:real^3)(S:real^3 -> bool). (x IN S)/\(packing S) ==> (FINITE(V x S))`,REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `!x b S. &0 <= b /\ packing S ==> FINITE (S INTER ball (x,b))` ASSUME_TAC THENL [MESON_TAC [KIUMVTC];SUBGOAL_THEN `FINITE ((S:real^3->bool) INTER (ball(x:real^3,(&2*h0 + &1))))` ASSUME_TAC THENL [ASM_MESON_TAC [cautruc2];SUBGOAL_THEN `(V (x:real^3) (S:real^3->bool)) SUBSET (S INTER (ball(x,(&2*h0 + &1))))` ASSUME_TAC THENL [ASM_MESON_TAC [cautruc1];ASM_MESON_TAC [FINITE_SUBSET]]]]);;\r
  97 \r
  98 let them3 = prove(`!(x:real^3)(S:real^3 -> bool). (packing S) /\ (x IN S) ==> ~(x IN (V x S))`,REWRITE_TAC [packing] THEN REWRITE_TAC [V] THEN REWRITE_TAC [IN_ELIM_THM]);;\r
  99 \r
 100 let cautruc3 = prove(`!(a:real^3)(b:real^3)(c:real^3).(~(a = b))/\ (~(b = c)) /\ (~(c = a))/\ (dist(a,b) <= &2*h0) /\ (&2 <= dist(a,b))/\ (dist(b,c) <= &2*h0) /\ (&2 <= dist(b,c))/\ (dist(c,a) <= &2*h0) /\ (&2 <= dist(c,a))==> (~(angle(a,b,c)= &0))`,REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC [ANGLE_EQ_0_DIST_ABS] THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN SUBGOAL_THEN `dist(c:real^3,b:real^3) = dist(b,c)` ASSUME_TAC THENL [ASM_MESON_TAC [DIST_SYM];SUBGOAL_THEN `&2 <= dist(c:real^3,b:real^3)` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `  --dist (c:real^3,b:real^3) <= -- &2` ASSUME_TAC THENL [ASM_MESON_TAC [REAL_LE_NEG];SUBGOAL_THEN `dist (a:real^3,b:real^3) - dist (c:real^3,b) <= &2*h0 - &2` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `dist (c:real^3,b:real^3) <= &2 * h0` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `-- (&2*h0) <= --dist (c:real^3,b:real^3)` ASSUME_TAC THENL [ASM_MESON_TAC [REAL_LE_NEG];SUBGOAL_THEN `&2 - &2*h0 <= dist (a:real^3,b:real^3) - dist (c:real^3,b)` ASSUME_TAC THENL[ASM_ARITH_TAC;SUBGOAL_THEN `-- (&2*h0 - &2) = -- &2*h0 + -- (-- &2) ` ASSUME_TAC THENL [REAL_ARITH_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NEG_NEG] THEN STRIP_TAC;SUBGOAL_THEN `-- (&2*h0 - &2) <= dist (a:real^3,b:real^3) - dist (c:real^3,b)` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `abs (dist (a:real^3,b:real^3) - dist (c:real^3,b)) <= &2*h0 - &2` ASSUME_TAC THENL [ASM_MESON_TAC [REAL_BOUNDS_LE];SUBGOAL_THEN `dist(a:real^3,c:real^3) = dist (c:real^3,a:real^3)` ASSUME_TAC THENL [MESON_TAC [DIST_SYM];SUBGOAL_THEN `&2 <= dist(a:real^3,c:real^3)` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `&2*h0 - &2 < &2` ASSUME_TAC THENL[REWRITE_TAC [h0] THEN ARITH_TAC;SUBGOAL_THEN ` &2*h0 - &2 < dist (a:real^3,c:real^3)` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `abs (dist (a:real^3,b:real^3) - dist (c:real^3,b)) < dist(a,c)` ASSUME_TAC THENL [ASM_ARITH_TAC;ASM_ARITH_TAC]]]]]]]]]]]]]]]);;\r
 101 (*Proff~(angle (a,b,c) = pi)*)\r
 102 let cautruc4 = prove(`!(a:real^3)(b:real^3)(c:real^3).(~(a = b))/\ (~(b = c)) /\ (~(c = a))/\ (dist(a,b) <= &2*h0) /\ (&2 <= dist(a,b))/\ (dist(b,c) <= &2*h0) /\ (&2 <= dist(b,c))/\ (dist(c,a) <= &2*h0) /\ (&2 <= dist(c,a))==> (~(angle(a,b,c)= pi))`,REPEAT GEN_TAC THEN STRIP_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `between (b:real^3) (a:real^3,c:real^3)` ASSUME_TAC THENL [ASM_MESON_TAC [BETWEEN_ANGLE];SUBGOAL_THEN `dist (a:real^3,c:real^3) = dist (a,b) + dist (b,c:real^3)` ASSUME_TAC THENL [ASM_MESON_TAC [between];SUBGOAL_THEN `&2 + &2 <= dist (a:real^3,b:real^3) + dist (b,c:real^3)` ASSUME_TAC THENL[ASM_ARITH_TAC;SUBGOAL_THEN `&2 + &2 <= dist(a:real^ 3,c:real^3)` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `dist(c:real^3,a:real^3) = dist(a:real^3,c)` ASSUME_TAC THENL[MESON_TAC [DIST_SYM];SUBGOAL_THEN `&2 + &2 <= dist(c:real^3,a:real^3)` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `&2*h0 < &2 + &2` ASSUME_TAC THENL [REWRITE_TAC [h0] THEN ARITH_TAC;SUBGOAL_THEN `&2*h0 < dist(c:real^3,a:real^3)` ASSUME_TAC THENL [ASM_ARITH_TAC;ASM_ARITH_TAC]]]]]]]]);;\r
 103 \r
 104 let cautruc5 = prove(`!(a:real^3)(b:real^3)(c:real^3).(~(a = b))/\ (~(b = c)) /\ (~(c = a))/\ (dist(a,b) <= &2*h0) /\ (&2 <= dist(a,b))/\ (dist(b,c) <= &2*h0) /\ (&2 <= dist(b,c))/\ (dist(c,a) <= &2*h0) /\ (&2 <= dist(c,a))==>(~(angle(a,b,c)= &0))/\ (~(angle(a,b,c)= pi))`,REPEAT GEN_TAC THEN STRIP_TAC THEN STRIP_TAC THENL [ASM_MESON_TAC [cautruc3];ASM_MESON_TAC [cautruc4]]);;\r
 105 \r
 106 \r
 107 let cautruc6 = prove(`!(a:real^3)(b:real^3)(c:real^3).(~(a=b)) /\ (~(b=c)) /\ (~(angle (a,b,c) = &0))/\ (~(angle (a,b,c) = pi)) ==> ~(collinear{a,b,c})`,REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~(a:real^3 = b:real^3) /\ ~(b = c:real^3)==> (collinear {a, b, c} <=> angle (a,b,c) = &0 \/ angle (a,b,c) = pi)` ASSUME_TAC THENL [STRIP_TAC THEN ASM_MESON_TAC[COLLINEAR_ANGLE];POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]]);;\r
 108 \r
 109 let cautruc7 = prove(`!(a:real^3)(b:real^3)(c:real^3).(~(a = b))/\ (~(b = c)) /\ (~(c = a))/\ (dist(a,b) <= &2*h0 /\ (&2 <= dist(a,b)) /\ (&2 <= dist(b,c)))/\ (dist(c,a) <= &2*h0) /\ (&2 <= dist(c,a))==> (~(angle(a,b,c)= pi))`,REPEAT GEN_TAC THEN STRIP_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `between (b:real^3) (a:real^3,c:real^3)` ASSUME_TAC THENL [ASM_MESON_TAC [BETWEEN_ANGLE];SUBGOAL_THEN `dist (a:real^3,c:real^3) = dist (a,b) + dist (b,c:real^3)` ASSUME_TAC THENL [ASM_MESON_TAC [between];SUBGOAL_THEN `&2 + &2 <= dist (a:real^3,b:real^3) + dist (b,c:real^3)` ASSUME_TAC THENL[ASM_ARITH_TAC;SUBGOAL_THEN `&2 + &2 <= dist(a:real^ 3,c:real^3)` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `dist(c:real^3,a:real^3) = dist(a:real^3,c)` ASSUME_TAC THENL[MESON_TAC [DIST_SYM];SUBGOAL_THEN `&2 + &2 <= dist(c:real^3,a:real^3)` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `&2*h0 < &2 + &2` ASSUME_TAC THENL [REWRITE_TAC [h0] THEN ARITH_TAC;SUBGOAL_THEN `&2*h0 < dist(c:real^3,a:real^3)` ASSUME_TAC THENL [ASM_ARITH_TAC;ASM_ARITH_TAC]]]]]]]]);;\r
 110 \r
 111 let IN1 = prove(`!(x:A)(a:A)(b:A). x IN {a,b}  <=> (x = a) \/ (x = b) `,REPEAT GEN_TAC THEN REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY]);;\r
 112 \r
 113 let IN2 = prove(`!(x:A)(a:A)(b:A)(c:A). x IN {a,b,c}  <=> (x = a) \/ (x = b) \/ (x = c) `,REPEAT GEN_TAC THEN REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY]);;\r
 114 \r
 115 let SUBSET1 = prove(`!(a:real^3)(b:real^3)(x:real^3).{a,b,x} SUBSET ({x} UNION {a,b})`,REPEAT GEN_TAC THEN REWRITE_TAC [SUBSET;UNION] THEN GEN_TAC THEN REWRITE_TAC [IN2;IN1;IN_ELIM_THM] THEN STRIP_TAC THENL [ASM_MESON_TAC[];ASM_MESON_TAC[];REWRITE_TAC [IN_SING] THEN ASM_MESON_TAC []]);;\r
 116 \r
 117 let them4 = prove( `!(a:real^3)(b:real^3)(x:real^3)(S:real^3 -> bool). (packing S) /\ (x IN S) /\ ({a,b} IN (ESTD(V x S))) ==> ~(collinear ({x} UNION {a,b}))`,REWRITE_TAC [ESTD;V;IN_ELIM_PAIR_THM;IN_ELIM_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN STRIP_TAC  THEN SUBGOAL_THEN `&2 <= dist(v:real^3,x:real^3)` ASSUME_TAC THENL [ASM_MESON_TAC [them1];SUBGOAL_THEN `&2 <= dist(w:real^3,x:real^3)` ASSUME_TAC THENL [ASM_MESON_TAC [them1];SUBGOAL_THEN `&2 <= dist(v:real^3,w:real^3)` ASSUME_TAC THENL [ASM_MESON_TAC [them1];SUBGOAL_THEN `dist(v:real^3,x:real^3) = dist(x,v)` ASSUME_TAC THENL [MESON_TAC [DIST_SYM];SUBGOAL_THEN `dist(x:real^3,v:real^3) <= &2*h0` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `&2 <= dist(x:real^3,v:real^3)` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `v:real^3 = x:real^3 <=> x = v` ASSUME_TAC THENL [MESON_TAC [EQ_SYM_EQ];SUBGOAL_THEN `(~(x:real^3 = v:real^3))` ASSUME_TAC THENL [ASM_MESON_TAC[];SUBGOAL_THEN `(~(angle(v:real^3,w:real^3,x:real^3) = &0)) /\ (~(angle(v,w,x) = pi))` ASSUME_TAC THENL [ASM_MESON_TAC [cautruc5];SUBGOAL_THEN `{v:real^3,w:real^3,x:real^3} SUBSET ({x} UNION {v,w})` ASSUME_TAC THENL [MESON_TAC [SUBSET1];\r
 118 SUBGOAL_THEN `collinear ({v:real^3,w:real^3,x:real^3})` ASSUME_TAC THENL [ASM_MESON_TAC [COLLINEAR_SUBSET];SUBGOAL_THEN `~collinear ({v:real^3,w:real^3,x:real^3})` ASSUME_TAC THENL [ASM_MESON_TAC [cautruc6];ASM_ARITH_TAC]]]]]]]]]]]]);;\r
 119 \r
 120 let eunion = new_definition `Eunion (x:real^3) (S:real^3->bool) = UNIONS ( ESTD (V x S))`;;\r
 121 \r
 122 let them5 = prove(`!(x:real^3)(S:real^3 -> bool).(Eunion x S) SUBSET (V x S)`,REPEAT GEN_TAC THEN REWRITE_TAC [eunion;ESTD;UNIONS;SUBSET;IN_ELIM_THM] THEN GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC [IN1] THEN STRIP_TAC THENL [ASM_REWRITE_TAC[];ASM_REWRITE_TAC[]]);;\r
 123 \r
 124 let them6 = prove(`!(x:real^3)(S:real^3 -> bool) e. e IN (ESTD(V x S)) ==> (e HAS_SIZE 2)`,REPEAT GEN_TAC THEN REWRITE_TAC [HAS_SIZE_2_EXISTS;ESTD;IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC `v:real^3` THEN EXISTS_TAC `w:real^3` THEN STRIP_TAC THENL [ASM_MESON_TAC[];STRIP_TAC THEN REWRITE_TAC [IN1]]);;\r
 125 \r
 126 let them7 = prove(`!(x:real^3) (S:real^3 -> bool). (packing S) /\ (x IN S) ==> !e. e IN ESTD (V x S) ==>  ~collinear ({x} UNION e)`,REPEAT GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN REWRITE_TAC [ESTD;V;IN_ELIM_THM] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `{v:real^3,w:real^3} IN  (ESTD (V x S))` ASSUME_TAC THENL [REWRITE_TAC [ESTD;V;IN_ELIM_THM] THEN EXISTS_TAC `v:real^3` THEN EXISTS_TAC `w:real^3` THEN REPEAT STRIP_TAC THENL [ASM_REWRITE_TAC[];ASM_REWRITE_TAC[];POP_ASSUM MP_TAC THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[];ASM_REWRITE_TAC[];ASM_REWRITE_TAC[];ASM_REWRITE_TAC[];POP_ASSUM MP_TAC THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[];ASM_REWRITE_TAC[];POP_ASSUM MP_TAC THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[];ASM_ARITH_TAC;ARITH_TAC];ASM_MESON_TAC [them4]]);;\r
 127 \r
 128 (*My definition--------------------------------------- To proof this lemma! i'll proof it later *)\r
 129 \r
 130 \r
 131 let sigma_set1 = new_definition `sigma_set1 (x:real^3) (S:real^3->bool) = (ESTD(V x S)) UNION {{v}|v IN (V x S)}`;; \r
 132 \r
 133 let dn1 = prove(`!(v:real^3)(v':real^3). (~(v = v')) ==> {v} INTER {v'} = {}`,CHEAT_TAC);;\r
 134 let dn111 = prove(`!(v:real^3)(v':real^3) (w:real^3). (~(v = v')) /\ (~(v = w)) ==> {v} INTER {v',w} = {}`,CHEAT_TAC);;\r
 135 let dn112 = prove(`!(v:real^3)(v':real^3)(w:real^3) (w':real^3).(~({v, w} = {v', w'}))/\ (~(v = v')) /\ (~(v = w')) /\ (~(w = v')) /\ (~(w = w')) ==> {v,w} INTER {v',w'} = {}`,CHEAT_TAC);; \r
 136 \r
 137 let dn2 = prove (`!x:real^3. aff_ge {x} {}={x}`, CHEAT_TAC );; \r
 138 \r
 139 let dn3 = prove (`!x:real^3 v:real^3. aff_ge {x} {v}={y:real^3 |  ?t1:real t2:real. (t2 >= &0)/\ (t1 + t2= &1) /\ (y = t1 % x + t2 % v)}`,CHEAT_TAC);; \r
 140 \r
 141 let dn4 = prove (`!x:real^3 v:real^3 w:real^3. aff_ge {x} {v,w} = {y:real^3 |  ?t1:real (t2:real) t3:real. (t2 >= &0) /\ (t3 >= &0)  /\ (t1 + t2 + t3 = &1) /\ (y = t1 % x + t2 % v + t3 % w)}`, CHEAT_TAC);; \r
 142 \r
 143 let dn5 = prove (`!(v:real^3)(v':real^3)(w:real^3).(~(v=v')) /\ (~(v=w)) ==> {v} INTER {v',w} = {}`,CHEAT_TAC);; \r
 144 let dn51 =prove (`!(v:real^3)(v':real^3)(w:real^3).(~(v' = v)) /\ (~(v' = w)) ==> {v,w} INTER {v'} = {}`,CHEAT_TAC);;\r
 145 \r
 146 let dn6 = prove (`!(v':real^3)(w:real^3). {v'} INTER {v',w} = {v'}`,CHEAT_TAC);;\r
 147 let dn61 = prove (`!(v':real^3)(w:real^3). {w} INTER {v',w} = {w}`,CHEAT_TAC);;\r
 148 let dn62 =  prove (`!(v':real^3)(w:real^3). {v,w} INTER {v} = {v}`,CHEAT_TAC);;\r
 149 let dn63 =  prove (`!(v':real^3)(w:real^3). {v,w} INTER {w} = {w}`,CHEAT_TAC);;\r
 150 \r
 151 let dn7 =  prove (`!(v:real^3)(v':real^3)(w:real^3).(v = w) ==> {v} INTER {v',w} = {v}`,CHEAT_TAC);;\r
 152 \r
 153 let dn8 =  prove (`!(v:real^3)(v':real^3)(w:real^3)(w':real^3).{v',w'} INTER {v',w'} = {v',w'}`,CHEAT_TAC);;\r
 154 \r
 155 let dn9 =  prove (`!(v:real^3)(v':real^3)(w:real^3)(w':real^3). ~({v,w} = {v',w'}) ==> {v',w} INTER {v',w'} = {v'}`,CHEAT_TAC);;\r
 156 let dn91 =  prove (`!(v:real^3)(v':real^3)(w:real^3)(w':real^3). ~({v,w} = {v',w'}) ==> {w',w} INTER {v',w'} = {w'}`,CHEAT_TAC);;\r
 157 let dn92 =  prove (`!(v:real^3)(v':real^3)(w':real^3). ~({v,w} = {v',w'}) ==> ({v, v'} INTER {v', w'}) = {v'}`,CHEAT_TAC);;\r
 158 let dn93 =  prove (`!(v:real^3)(v':real^3)(w':real^3). ~({v,w} = {v',w'}) ==> ({v, w'} INTER {v', w'}) = {w'}`,CHEAT_TAC);;\r
 159 \r
 160 let dn10 = prove (`!(v:real^3)(v':real^3)(x:real^3).( (a:real) % v + (b:real) % v' + (c:real) % x = vec 0) ==> a = &0 /\ b = &0 /\ c = &0`,CHEAT_TAC);;\r
 161 \r
 162 let dn11 = prove (`!(v:real^3)(v':real^3)(x:real^3)(w:real^3).( (a:real) % v + (b:real) % v' + (c:real) % x + (d:real) % w = vec 0) ==> a = &0 /\ b = &0 /\ c = &0 /\ d = &0`,CHEAT_TAC);;\r
 163 \r
 164 let dn12 =  prove (`!(v:real^3)(v':real^3)(x:real^3)(w:real^3)(w':real^3).( (a:real) % v + (b:real) % v' + (c:real) % x + (d:real) % w + (e:real)%w' = vec 0) ==> a = &0 /\ b = &0 /\ c = &0 /\ d = &0 /\ e = &0`,CHEAT_TAC);;\r
 165 \r
 166 let logic1 = prove(`!p q r. p /\ (p \/ r) = p`,CHEAT_TAC);;\r
 167 (*-------------------------------------------------------------------------*)\r
 168 \r
 169 (*4 SUBGOAL*)\r
 170 (*SUB1*)\r
 171 (*Case v = v' *)\r
 172 let SUBCASE1 = prove (`!(v:real^3) (v':real^3) (x:real^3)(S:real^3->bool).(v IN S) /\ (x IN S ) /\ (v' IN S) /\ (~(v = x)) /\ (~(v' = x)) /\ (dist (v,x) <= &2 * h0) /\ (dist (v',x) <= &2 * h0) /\ (e1 = {v}) /\ (e2 = {v'}) /\ (v = v') ==> (!x'.x' IN  {y | ?t1 t2. t2 >= &0 /\ t1 + t2 = &1 /\ y = t1 % x + t2 % v} INTER {y | ?t1 t2. t2 >= &0 /\ t1 + t2 = &1 /\ y = t1 % x + t2 % v'} ==> x' IN aff_ge {x} ({v} INTER {v'}))`, REPEAT GEN_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC  THEN REWRITE_TAC [IN_SING;SING_GSPEC;INTER;IN_ELIM_THM] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC [IN_SING;SING_GSPEC;dn3;IN_ELIM_THM]);;\r
 173 \r
 174 let SUBCASE2 = prove(`!(v:real^3) (v':real^3) (x:real^3)(S:real^3->bool).(v IN S) /\ (x IN S ) /\ (v' IN S) /\ (~(v = x)) /\ (~(v' = x)) /\ (dist (v,x) <= &2 * h0) /\ (dist (v',x) <= &2 * h0) /\ (e1 = {v}) /\ (e2 = {v'}) /\ (~(v = v')) ==> (!x'.x' IN  {y | ?t1 t2. t2 >= &0 /\ t1 + t2 = &1 /\ y = t1 % x + t2 % v} INTER {y | ?t1 t2. t2 >= &0 /\ t1 + t2 = &1 /\ y = t1 % x + t2 % v'} ==> x' IN aff_ge {x} ({v} INTER {v'}))`,REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `{v:real^3} INTER {v':real^3} = {}` ASSUME_TAC THENL [ASM_MESON_TAC[dn1];ASM_REWRITE_TAC[]] THEN REWRITE_TAC [INTER;dn2;IN_SING;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN SUBGOAL_THEN `(x':real^3) - ((t1':real) % (x:real^3) + (t2':real) % (v':real^3)) = vec 0` ASSUME_TAC THENL [POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC;POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]] THEN REWRITE_TAC[VECTOR_ARITH `(t1 % x + t2 % v) - (t1' % x + t2' % v')= ((t1:real)- (t1':real)) % (x:real^3) + (t2:real) % (v:real^3) + (--(t2':real) % (v':real^3))`] THEN STRIP_TAC THEN SUBGOAL_THEN `(t1:real - t1':real) = &0 /\ t2:real = &0 /\ --t2':real = &0` ASSUME_TAC THENL [ASM_MESON_TAC [dn10];SUBGOAL_THEN `((t1:real) = (t1':real))` ASSUME_TAC THENL [ASM_MESON_TAC[REAL_SUB_0];SUBGOAL_THEN `(t1':real) + &0 = &1` ASSUME_TAC THENL [ASM_MESON_TAC[];SUBGOAL_THEN `(t1':real) = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC]]]]);;\r
 175 \r
 176 let cautruc8 = prove(`!(v:real^3) (v':real^3) (x:real^3)(S:real^3->bool).(v IN S) /\ (x IN S) /\ (v' IN S) /\ (~(v=x)) /\ (~(v'=x)) /\ (dist (v,x) <= &2 * h0) /\ (dist (v',x) <= &2 * h0) /\ e1 = {v} /\ e2 = {v'} ==> aff_ge {x} e1 INTER aff_ge {x} e2 = aff_ge {x} (e1 INTER e2)`,REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC [EXTENSION;GSYM SUBSET_ANTISYM_EQ;SUBSET] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC [IN_ELIM_THM] THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL [REWRITE_TAC [dn3] THEN GEN_TAC THEN REWRITE_TAC [IN_ELIM_THM] THEN ASM_CASES_TAC `v:real^3 = v':real^3` THENL[ASM_MESON_TAC [SUBCASE1];ASM_MESON_TAC [SUBCASE2]];ASM_CASES_TAC `v:real^3 = v':real^3` THENL [ASM_REWRITE_TAC[] THEN REWRITE_TAC [IN_SING;SING_GSPEC;INTER;IN_ELIM_THM];GEN_TAC THEN SUBGOAL_THEN `{v:real^3} INTER {v':real^3} = {}` ASSUME_TAC] THENL [ASM_MESON_TAC[dn1];ASM_REWRITE_TAC[]] THEN REWRITE_TAC [dn2;IN_SING;dn3;INTER;IN_ELIM_THM] THEN REPEAT STRIP_TAC THENL [EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL [ARITH_TAC;STRIP_TAC THENL [ARITH_TAC;VECTOR_ARITH_TAC]];EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN STRIP_TAC THENL [ARITH_TAC;STRIP_TAC THENL [ARITH_TAC;ASM_REWRITE_TAC[]THEN VECTOR_ARITH_TAC]]]]);;\r
 177 \r
 178 (*--------------------------------------------------------------------------------------*)\r
 179 (*SUB2*)\r
 180 let SUBCASE3 = prove(`!(v:real^3) (v':real^3) (x:real^3)(S:real^3->bool). (v IN S) /\ (x IN S) /\ (~(v = x)) /\ (dist (v,x) <= &2 * h0) /\ ( e1 = {v})/\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w IN S) /\ ( ~(w = x)) /\ (dist (w,x) <= &2 * h0) /\ (~(v' = w)) /\ (dist (v',w) <= &2 * h0) /\ (e2 = {v', w}) /\ (v = v') ==>(?t1 t2. t2 >= &0 /\ t1 + t2 = &1 /\ x' = t1 % x + t2 % v) /\(?t1 t2 t3. t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ x' = t1 % x + t2 % v' + t3 % w) ==> x' IN aff_ge {x} {x | x IN {v} /\ x IN {v', w}}`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN STRIP_TAC THEN REWRITE_TAC [GSYM INTER;dn6;dn3;IN_ELIM_THM] THEN EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN STRIP_TAC THENL [ASM_MESON_TAC[];STRIP_TAC THENL [ASM_MESON_TAC[];ASM_MESON_TAC[]]]);;\r
 181 \r
 182 let SUBCASE4 = prove(`!(v:real^3) (v':real^3) (x:real^3)(w:real^3)(S:real^3->bool). (v IN S) /\ (x IN S) /\ (~(v = x)) /\ (dist (v,x) <= &2 * h0) /\ ( e1 = {v})/\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w IN S) /\ ( ~(w = x)) /\ (dist (w,x) <= &2 * h0) /\ (~(v' = w)) /\ (dist (v',w) <= &2 * h0) /\ (e2 = {v', w}) /\ ~(v = v') /\ (v = w) ==>(?t1 t2. t2 >= &0 /\ t1 + t2 = &1 /\ x' = t1 % x + t2 % v) /\(?t1 t2 t3. t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ x' = t1 % x + t2 % v' + t3 % w) ==> x' IN aff_ge {x} {x | x IN {v} /\ x IN {v', w}}`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN STRIP_TAC THEN REWRITE_TAC [GSYM INTER;dn61;dn3;IN_ELIM_THM] THEN EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN STRIP_TAC THENL [ASM_MESON_TAC[];STRIP_TAC THENL [ASM_MESON_TAC[];ASM_MESON_TAC[]]]);;\r
 183 \r
 184 let SUBCASE5 = prove( `!(v:real^3) (v':real^3) (x:real^3)(w:real^3)(S:real^3->bool). (v IN S) /\ (x IN S) /\ (~(v = x)) /\ (dist (v,x) <= &2 * h0) /\ ( e1 = {v})/\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w IN S) /\ ( ~(w = x)) /\ (dist (w,x) <= &2 * h0) /\ (~(v' = w)) /\ (dist (v',w) <= &2 * h0) /\ (e2 = {v', w}) /\ ~(v = v') /\ ~(v = w) ==>(?t1 t2. t2 >= &0 /\ t1 + t2 = &1 /\ x' = t1 % x + t2 % v) /\(?t1 t2 t3. t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ x' = t1 % x + t2 % v' + t3 % w) ==> x' IN aff_ge {x} {x | x IN {v} /\ x IN {v', w}}`,REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC [GSYM INTER] THEN SUBGOAL_THEN `({v:real^3} INTER {v':real^3, w:real^3}) = {}` ASSUME_TAC THENL [ASM_MESON_TAC [dn111];ASM_REWRITE_TAC[]] THEN STRIP_TAC THEN REWRITE_TAC [dn2;IN_SING] THEN SUBGOAL_THEN `(x':real^3) - ((t1':real) % (x:real^3) + (t2':real) % (v':real^3) + (t3:real) % (w:real^3)) = vec 0` ASSUME_TAC THENL [POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC;POP_ASSUM MP_TAC THEN  ASM_REWRITE_TAC[] THEN REWRITE_TAC[VECTOR_ARITH `(t1 % x + t2 % v) - (t1' % x + t2' % v' + t3 % w) = ((t1:real)- (t1':real)) % (x:real^3) +((t2:real)%(v:real^3)) + (--(t2':real)%(v':real^3)) + (--(t3:real)%(w:real^3))`] THEN STRIP_TAC THEN SUBGOAL_THEN `((t1:real)- (t1':real)) = &0 /\ (t2:real) = &0 /\  (--(t2':real)) = &0 /\ (--(t3:real)) = &0` ASSUME_TAC THENL [ASM_MESON_TAC [dn11];SUBGOAL_THEN `t1:real = t1':real` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `(t1:real) + &0 = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `t1:real = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `t1':real = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC]]]]]]);;\r
 185 \r
 186 let SUBCASE6 = prove( `!(v:real^3) (v':real^3) (x:real^3)(w:real^3)(S:real^3->bool).  (v IN S) /\ (x IN S) /\ (~(v = x)) /\ (dist (v,x) <= &2 * h0) /\ ( e1 = {v})/\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w IN S) /\ ( ~(w = x)) /\ (dist (w,x) <= &2 * h0) /\ (~(v' = w)) /\ (dist (v',w) <= &2 * h0) /\ (e2 = {v', w})/\ (v = v')==> !x'. x' IN aff_ge {x} {x | x IN {v} /\ x IN {v', w}} ==> x' IN aff_ge {x} {v} /\ x' IN aff_ge {x} {v', w}`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN STRIP_TAC THEN REWRITE_TAC [GSYM INTER;dn6;dn3;dn4;IN_ELIM_THM] THEN REPEAT STRIP_TAC THENL [EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]];EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN EXISTS_TAC `&0` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]]]);;\r
 187 \r
 188 let SUBCASE7 = prove(`!(v:real^3) (v':real^3) (x:real^3)(w:real^3)(S:real^3->bool).  (v IN S) /\ (x IN S) /\ (~(v = x)) /\ (dist (v,x) <= &2 * h0) /\ ( e1 = {v})/\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w IN S) /\ ( ~(w = x)) /\ (dist (w,x) <= &2 * h0) /\ (~(v' = w)) /\ (dist (v',w) <= &2 * h0) /\ (e2 = {v', w})/\ ~(v = v') /\ (v = w)==> !x'. x' IN aff_ge {x} {x | x IN {v} /\ x IN {v', w}} ==> x' IN aff_ge {x} {v} /\ x' IN aff_ge {x} {v', w}`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN STRIP_TAC THEN REWRITE_TAC [GSYM INTER;dn61;dn3;dn4;IN_ELIM_THM] THEN REPEAT STRIP_TAC THENL [EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN STRIP_TAC THENL[ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]];EXISTS_TAC `t1:real` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `t2:real`THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]]]);;\r
 189 \r
 190 let SUBCASE8 = prove(`!(v:real^3) (v':real^3) (x:real^3)(w:real^3)(S:real^3->bool).  (v IN S) /\ (x IN S) /\ (~(v = x)) /\ (dist (v,x) <= &2 * h0) /\ ( e1 = {v})/\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w IN S) /\ ( ~(w = x)) /\ (dist (w,x) <= &2 * h0) /\ (~(v' = w)) /\ (dist (v',w) <= &2 * h0) /\ (e2 = {v', w})/\ ~(v = v') /\ ~(v = w)==> !x'. x' IN aff_ge {x} {x | x IN {v} /\ x IN {v', w}} ==> x' IN aff_ge {x} {v} /\ x' IN aff_ge {x} {v', w}`,REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC [GSYM INTER] THEN SUBGOAL_THEN `({v:real^3} INTER {v':real^3, w:real^3}) = {}` ASSUME_TAC THENL [ASM_MESON_TAC [dn111];ASM_REWRITE_TAC[]] THEN STRIP_TAC THEN REWRITE_TAC [dn2;IN_SING;dn3;dn4;IN_ELIM_THM] THEN REPEAT STRIP_TAC THENL [EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN STRIP_TAC THENL[ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]];EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL[ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]]]);;\r
 191 \r
 192 let cautruc9 = prove(`!(v:real^3) (v':real^3)(w:real^3) (x:real^3)(S:real^3->bool).(v IN S) /\ (x IN S) /\ (~(v = x)) /\ (dist (v,x) <= &2 * h0) /\ (e1 = {v}) /\ (v' IN S)/\ (~(v' = x)) /\ (dist (v',x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ (dist (w,x) <= &2 * h0) /\ (~(v' = w)) /\ (dist (v',w) <= &2 * h0) /\  (e2 = {v', w}) ==> {x' | x' IN aff_ge {x} e1 /\ x' IN aff_ge {x} e2} = aff_ge {x} {x | x IN e1 /\ x IN e2}`,REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC [EXTENSION;GSYM SUBSET_ANTISYM_EQ] THEN REWRITE_TAC [SUBSET] THEN REWRITE_TAC [IN_ELIM_THM] THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL (*----*) [REWRITE_TAC [dn3;dn4] THEN GEN_TAC THEN REWRITE_TAC [IN_ELIM_THM] (*v = v'*) THEN ASM_CASES_TAC `(v:real^3 = v':real^3)` THENL [ASM_MESON_TAC [SUBCASE3];(*v = w*) ASM_CASES_TAC `(v:real^3 = w:real^3)` THENL[ASM_MESON_TAC [SUBCASE4]; (* ~(v = v') /\ ~(v = w) *) ASM_MESON_TAC [SUBCASE5]]];(*Small Cases*)(*v = v'*) ASM_CASES_TAC `(v:real^3 = v':real^3)` THENL[ASM_MESON_TAC [SUBCASE6]; (*v = w*) ASM_CASES_TAC `(v:real^3 = w:real^3)` THENL[ASM_MESON_TAC [SUBCASE7];(* ~(v = v') /\ ~(v = w) *) ASM_MESON_TAC [SUBCASE8]]]]);;\r
 193 \r
 194 (*SUB3 like SUB2*)\r
 195 \r
 196 let SUBCASE31 = prove( `!(v:real^3) (v':real^3)(w:real^3) (x:real^3)(S:real^3->bool).( v IN S) /\ (x IN S) /\ (~(v = x)) /\ (dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ (dist (w,x) <= &2 * h0) /\ (~(v = w)) /\ (dist (v,w) <= &2 * h0) /\ (e1 = {v, w}) /\ (v' IN S) /\ (~(v' = x)) /\ (dist (v',x) <= &2 * h0) /\ (e2 = {v'})/\ (v' = v)==>  x' IN {y | ?t1 t2 t3. t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v + t3 % w} INTER{y | ?t1 t2. t2 >= &0 /\ t1 + t2 = &1 /\ y = t1 % x + t2 % v'} ==> x' IN aff_ge {x} ({v, w} INTER {v'})`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN REWRITE_TAC [dn62;dn3;INTER;IN_ELIM_THM] THEN STRIP_TAC THEN EXISTS_TAC `t1':real` THEN EXISTS_TAC `t2':real` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]);;\r
 197 \r
 198 let SUBCASE32 = prove(`!(v:real^3) (v':real^3)(w:real^3) (x:real^3)(S:real^3->bool).( v IN S) /\ (x IN S) /\ (~(v = x)) /\ (dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ (dist (w,x) <= &2 * h0) /\ (~(v = w)) /\ (dist (v,w) <= &2 * h0) /\ (e1 = {v, w}) /\ (v' IN S) /\ (~(v' = x)) /\ (dist (v',x) <= &2 * h0) /\ (e2 = {v'})/\ (~(v' = v)) /\ (v' = w)==>  x' IN {y | ?t1 t2 t3. t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v + t3 % w} INTER{y | ?t1 t2. t2 >= &0 /\ t1 + t2 = &1 /\ y = t1 % x + t2 % v'} ==> x' IN aff_ge {x} ({v, w} INTER {v'})`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN REWRITE_TAC [dn63;dn3;INTER;IN_ELIM_THM] THEN STRIP_TAC THEN EXISTS_TAC `t1':real` THEN EXISTS_TAC `t2':real` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]);;\r
 199 \r
 200 let SUBCASE33 = prove(`!(v:real^3) (v':real^3)(w:real^3) (x:real^3)(S:real^3->bool).( v IN S) /\ (x IN S) /\ (~(v = x)) /\ (dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ (dist (w,x) <= &2 * h0) /\ (~(v = w)) /\ (dist (v,w) <= &2 * h0) /\ (e1 = {v, w}) /\ (v' IN S) /\ (~(v' = x)) /\ (dist (v',x) <= &2 * h0) /\ (e2 = {v'})/\ (~(v' = v)) /\ (~(v' = w)) ==>  x' IN {y | ?t1 t2 t3. t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v + t3 % w} INTER{y | ?t1 t2. t2 >= &0 /\ t1 + t2 = &1 /\ y = t1 % x + t2 % v'} ==> x' IN aff_ge {x} ({v, w} INTER {v'})`,REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC [GSYM INTER] THEN SUBGOAL_THEN `({v:real^3,w:real^3} INTER {v':real^3}) = {}` ASSUME_TAC THENL [ASM_MESON_TAC [dn51];ASM_REWRITE_TAC[]] THEN REWRITE_TAC [dn2;IN_SING;INTER;IN_ELIM_THM] THEN STRIP_TAC THEN SUBGOAL_THEN `(x':real^3) - ((t1':real) % (x:real^3) + (t2':real) % (v':real^3)) = vec 0` ASSUME_TAC THENL [POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC;POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]] THEN REWRITE_TAC[VECTOR_ARITH `(t1 % x + t2 % v + t3 % w) - (t1' % x + t2' % v') = ((t1:real)- (t1':real)) % (x:real^3) +((t2:real)%(v:real^3)) + (--(t2':real)%(v':real^3)) + (t3:real)%(w:real^3)`] THEN STRIP_TAC THEN SUBGOAL_THEN `((t1:real)- (t1':real)) = &0 /\ (t2:real) = &0 /\  (--(t2':real)) = &0 /\ ((t3:real)) = &0` ASSUME_TAC THENL [ASM_MESON_TAC [dn11];SUBGOAL_THEN `t1:real = t1':real` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `(t1:real) + &0 + &0 = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `t1:real = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `t1':real = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC]]]]]);;\r
 201 \r
 202 let SUBCASE34 = prove( `!(v:real^3) (v':real^3)(w:real^3) (x:real^3)(S:real^3->bool).( v IN S) /\ (x IN S) /\ (~(v = x)) /\ (dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ (dist (w,x) <= &2 * h0) /\ (~(v = w)) /\ (dist (v,w) <= &2 * h0) /\ (e1 = {v, w}) /\ (v' IN S) /\ (~(v' = x)) /\ (dist (v',x) <= &2 * h0) /\ (e2 = {v'})/\ ((v' = v))==> !x'. x' IN aff_ge {x} ({v, w} INTER {v'}) ==> x' IN aff_ge {x} {v, w} INTER aff_ge {x} {v'}`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN STRIP_TAC THEN REWRITE_TAC [dn62;dn3;dn4;INTER;IN_ELIM_THM] THEN REPEAT STRIP_TAC THENL [EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN EXISTS_TAC `&0` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]];EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]]);;\r
 203 \r
 204 let SUBCASE35 = prove(`!(v:real^3) (v':real^3)(w:real^3) (x:real^3)(S:real^3->bool).( v IN S) /\ (x IN S) /\ (~(v = x)) /\ (dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ (dist (w,x) <= &2 * h0) /\ (~(v = w)) /\ (dist (v,w) <= &2 * h0) /\ (e1 = {v, w}) /\ (v' IN S) /\ (~(v' = x)) /\ (dist (v',x) <= &2 * h0) /\ (e2 = {v'})/\ (~(v' = v)) /\ (v' = w) ==> !x'. x' IN aff_ge {x} ({v, w} INTER {v'}) ==> x' IN aff_ge {x} {v, w} INTER aff_ge {x} {v'}`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN STRIP_TAC THEN REWRITE_TAC [dn63;dn3;dn4;INTER;IN_ELIM_THM] THEN REPEAT STRIP_TAC THENL [EXISTS_TAC `t1:real` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `t2:real` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]];EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]]);;\r
 205 \r
 206 let SUBCASE36 = prove( `!(v:real^3) (v':real^3)(w:real^3) (x:real^3)(S:real^3->bool).( v IN S) /\ (x IN S) /\ (~(v = x)) /\ (dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ (dist (w,x) <= &2 * h0) /\ (~(v = w)) /\ (dist (v,w) <= &2 * h0) /\ (e1 = {v, w}) /\ (v' IN S) /\ (~(v' = x)) /\ (dist (v',x) <= &2 * h0) /\ (e2 = {v'})/\ (~(v' = v)) /\ (~(v' = w)) ==> !x'. x' IN aff_ge {x} ({v, w} INTER {v'}) ==> x' IN aff_ge {x} {v, w} INTER aff_ge {x} {v'}`,REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `({v:real^3,w:real^3} INTER {v':real^3}) = {}` ASSUME_TAC THENL [ASM_MESON_TAC [dn51];ASM_REWRITE_TAC[]] THEN STRIP_TAC THEN REWRITE_TAC [dn2;IN_SING] THEN STRIP_TAC THEN REWRITE_TAC [dn3;dn4;INTER;IN_ELIM_THM] THEN STRIP_TAC THENL [EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]];EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]]);;\r
 207 \r
 208 \r
 209 \r
 210 let cautruc10 = prove(`!(v:real^3) (v':real^3)(w:real^3) (x:real^3)(S:real^3->bool).( v IN S) /\ (x IN S) /\ (~(v = x)) /\ (dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ (dist (w,x) <= &2 * h0) /\ (~(v = w)) /\ (dist (v,w) <= &2 * h0) /\ (e1 = {v, w}) /\ (v' IN S) /\ (~(v' = x)) /\ (dist (v',x) <= &2 * h0) /\ (e2 = {v'}) ==> aff_ge {x} e1 INTER aff_ge {x} e2 = aff_ge {x} (e1 INTER e2)`,REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC [EXTENSION;GSYM SUBSET_ANTISYM_EQ;SUBSET;IN_ELIM_THM] THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL(*----*)[REWRITE_TAC [dn3;dn4] THEN GEN_TAC THEN REWRITE_TAC [IN_ELIM_THM] THEN (*v' = v*)ASM_CASES_TAC `(v':real^3 = v:real^3)` THENL [ASM_MESON_TAC [SUBCASE31];(*v' = w*)ASM_CASES_TAC `(v':real^3 = w:real^3)` THENL [ASM_MESON_TAC [SUBCASE32];(*~(v' = v) /\ ~(v' = w)*)ASM_MESON_TAC [SUBCASE33]]];(*Small Case*)(*v = v'*)ASM_CASES_TAC `(v':real^3 = v:real^3)` THENL [ASM_MESON_TAC [SUBCASE34];(*v' = w*)ASM_CASES_TAC `(v':real^3 = w:real^3)` THENL [ASM_MESON_TAC [SUBCASE35];(* ~(v = v') /\ ~(v = w) *)ASM_MESON_TAC [SUBCASE36]]]]);;\r
 211 \r
 212 \r
 213 (*SUB4*)\r
 214 let SUBCASE41 = prove( `!(v:real^3)(v':real^3)(w:real^3)(w':real^3)(x:real^3)(S:real^3->bool).( v IN S) /\ ( x IN S) /\ ( ~(v = x)) /\ ( dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ ( dist (w,x) <= &2 * h0) /\ ( ~(v = w)) /\ ( dist (v,w) <= &2 * h0) /\ ( e1 = {v, w}) /\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w' IN S) /\ ( ~(w' = x)) /\ ( dist (w',x) <= &2 * h0) /\ ( ~(v' = w')) /\(dist(v',w') <= &2 * h0) /\ (e2 = {v', w'}) /\({v, w} = {v', w'})  ==> x' IN {y | ?t1 t2 t3.t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v + t3 % w} INTER {y | ?t1 t2 t3. t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v' + t3 % w'}  ==> x' IN aff_ge {x} ({v, w} INTER {v', w'})`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC [dn8;INTER;IN_ELIM_THM;dn4] THEN STRIP_TAC THEN REWRITE_TAC [IN_ELIM_THM] THEN EXISTS_TAC `t1':real` THEN EXISTS_TAC `t2':real` THEN EXISTS_TAC `t3':real` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]]);;\r
 215 \r
 216 let SUBCASE42 = prove(`!(v:real^3)(v':real^3)(w:real^3)(w':real^3)(x:real^3)(S:real^3->bool).( v IN S) /\ ( x IN S) /\ ( ~(v = x)) /\ ( dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ ( dist (w,x) <= &2 * h0) /\ ( ~(v = w)) /\ ( dist (v,w) <= &2 * h0) /\ ( e1 = {v, w}) /\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w' IN S) /\ ( ~(w' = x)) /\ ( dist (w',x) <= &2 * h0) /\ ( ~(v' = w')) /\(dist(v',w') <= &2 * h0) /\ (e2 = {v', w'}) /\(~({v, w} = {v', w'})) /\ (v = v') ==> x' IN {y | ?t1 t2 t3.t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v + t3 % w} INTER {y | ?t1 t2 t3. t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v' + t3 % w'}  ==> x' IN aff_ge {x} ({v, w} INTER {v', w'})`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN SUBGOAL_THEN `({v':real^3,w:real^3} INTER {v':real^3, w':real^3}) = {v'}` ASSUME_TAC THENL [ASM_MESON_TAC [dn9];ASM_REWRITE_TAC[]] THEN REWRITE_TAC [INTER;dn3;IN_ELIM_THM] THEN STRIP_TAC THEN SUBGOAL_THEN `(x':real^3) - ((t1':real) % (x:real^3) + (t2':real) % (v':real^3) + (t3':real) % (w':real^3)) = vec 0` ASSUME_TAC THENL [POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC;POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]] THEN REWRITE_TAC[VECTOR_ARITH `(t1 % x + t2 % v' + t3 % w) - (t1' % x + t2' % v' + t3' % w') = ((t1:real)- (t1':real)) % (x:real^3) + ((t2:real) - (t2':real)) % (v':real^3) + ((t3:real) % (w:real^3)) + (--(t3':real) % (w':real^3))`] THEN STRIP_TAC THEN SUBGOAL_THEN `((t1:real)- (t1':real)) = &0 /\  ((t2:real) - (t2':real)) = &0 /\ (t3:real) = &0 /\  (--(t3':real)) = &0` ASSUME_TAC THENL [ASM_MESON_TAC [dn11];SUBGOAL_THEN `(t1:real) + (t2:real) + &0 = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `(t1:real) + (t2:real) = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `(x':real^3) = (t1:real) % (x:real^3) + (t2:real) % (v':real^3) + &0 % (w:real^3)` ASSUME_TAC THENL [ASM_MESON_TAC[];EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC]]]]]]);;\r
 217 \r
 218 let SUBCASE43 = prove(`!(v:real^3)(v':real^3)(w:real^3)(w':real^3)(x:real^3)(S:real^3->bool).( v IN S) /\ ( x IN S) /\ ( ~(v = x)) /\ ( dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ ( dist (w,x) <= &2 * h0) /\ ( ~(v = w)) /\ ( dist (v,w) <= &2 * h0) /\ ( e1 = {v, w}) /\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w' IN S) /\ ( ~(w' = x)) /\ ( dist (w',x) <= &2 * h0) /\ ( ~(v' = w')) /\(dist(v',w') <= &2 * h0) /\ (e2 = {v', w'}) /\(~({v, w} = {v', w'})) /\ (~(v = v')) /\ (v = w') ==> x' IN {y | ?t1 t2 t3.t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v + t3 % w} INTER {y | ?t1 t2 t3. t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v' + t3 % w'}  ==> x' IN aff_ge {x} ({v, w} INTER {v', w'})`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN SUBGOAL_THEN `({w':real^3,w:real^3} INTER {v':real^3, w':real^3}) = {w'}` ASSUME_TAC THENL [ASM_MESON_TAC [dn91];ASM_REWRITE_TAC[]] THEN REWRITE_TAC [INTER;dn3;IN_ELIM_THM] THEN STRIP_TAC THEN SUBGOAL_THEN `(x':real^3) - ((t1':real) % (x:real^3) + (t2':real) % (v':real^3) + (t3':real) % (w':real^3)) = vec 0` ASSUME_TAC THENL [POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC;POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]] THEN REWRITE_TAC[VECTOR_ARITH `(t1 % x + t2 % w' + t3 % w) - (t1' % x + t2' % v' + t3' % w') = ((t1:real)- (t1':real)) % (x:real^3) + ((t2:real) - (t3':real)) % (w':real^3) + ((t3:real) % (w:real^3)) + (--(t2':real) % (v':real^3))`] THEN STRIP_TAC THEN SUBGOAL_THEN `((t1:real)- (t1':real)) = &0 /\  ((t2:real) - (t3':real)) = &0 /\ (t3:real) = &0 /\  (--(t2':real)) = &0` ASSUME_TAC THENL [ASM_MESON_TAC [dn11];SUBGOAL_THEN `(t1:real) + (t2:real) + &0 = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `(t1:real) + (t2:real) = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC]]]]]);;\r
 219 \r
 220 let SUBCASE44 = prove(`!(v:real^3)(v':real^3)(w:real^3)(w':real^3)(x:real^3)(S:real^3->bool).( v IN S) /\ ( x IN S) /\ ( ~(v = x)) /\ ( dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ ( dist (w,x) <= &2 * h0) /\ ( ~(v = w)) /\ ( dist (v,w) <= &2 * h0) /\ ( e1 = {v, w}) /\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w' IN S) /\ ( ~(w' = x)) /\ ( dist (w',x) <= &2 * h0) /\ ( ~(v' = w')) /\(dist(v',w') <= &2 * h0) /\ (e2 = {v', w'}) /\(~({v, w} = {v', w'})) /\ (~(v = v')) /\ (~(v = w')) /\ (w = v') ==> x' IN {y | ?t1 t2 t3.t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v + t3 % w} INTER {y | ?t1 t2 t3. t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v' + t3 % w'}  ==> x' IN aff_ge {x} ({v, w} INTER {v', w'})`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN SUBGOAL_THEN `({v:real^3,v':real^3} INTER {v':real^3, w':real^3}) = {v'}` ASSUME_TAC THENL [ASM_MESON_TAC [dn92];ASM_REWRITE_TAC[]] THEN REWRITE_TAC [INTER;dn3;IN_ELIM_THM] THEN STRIP_TAC THEN SUBGOAL_THEN `(x':real^3) - ((t1':real) % (x:real^3) + (t2':real) % (v':real^3) + (t3':real) % (w':real^3)) = vec 0` ASSUME_TAC THENL [POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC;POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]] THEN REWRITE_TAC[VECTOR_ARITH `(t1 % x + t2 % v + t3 % v') - (t1' % x + t2' % v' + t3' % w') = ((t1:real)- (t1':real)) % (x:real^3) + ((t2:real)) % (v:real^3) + ((t3:real)- (t2':real)) % (v':real^3) + (--(t3':real) % (w':real^3))`] THEN STRIP_TAC THEN SUBGOAL_THEN `((t1:real)- (t1':real)) = &0 /\  ((t2:real)) = &0 /\ ((t3:real)- (t2':real)) = &0 /\  (--(t3':real)) = &0` ASSUME_TAC THENL [ASM_MESON_TAC [dn11];SUBGOAL_THEN `(t1:real) + (t3:real) + &0 = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `(t1:real) + (t3:real) = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;EXISTS_TAC `t1:real` THEN EXISTS_TAC `t3:real` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC]]]]]);;\r
 221 \r
 222 let SUBCASE45 = prove(`!(v:real^3)(v':real^3)(w:real^3)(w':real^3)(x:real^3)(S:real^3->bool).( v IN S) /\ ( x IN S) /\ ( ~(v = x)) /\ ( dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ ( dist (w,x) <= &2 * h0) /\ ( ~(v = w)) /\ ( dist (v,w) <= &2 * h0) /\ ( e1 = {v, w}) /\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w' IN S) /\ ( ~(w' = x)) /\ ( dist (w',x) <= &2 * h0) /\ ( ~(v' = w')) /\(dist(v',w') <= &2 * h0) /\ (e2 = {v', w'}) /\(~({v, w} = {v', w'})) /\ (~(v = v')) /\ (~(v = w')) /\ (~(w = v')) /\ (w = w') ==> x' IN {y | ?t1 t2 t3.t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v + t3 % w} INTER {y | ?t1 t2 t3. t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v' + t3 % w'}  ==> x' IN aff_ge {x} ({v, w} INTER {v', w'})`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN SUBGOAL_THEN `({v:real^3,w':real^3} INTER {v':real^3, w':real^3}) = {w'}` ASSUME_TAC THENL [ASM_MESON_TAC [dn93];ASM_REWRITE_TAC[]] THEN REWRITE_TAC [INTER;dn3;IN_ELIM_THM] THEN STRIP_TAC THEN SUBGOAL_THEN `(x':real^3) - ((t1':real) % (x:real^3) + (t2':real) % (v':real^3) + (t3':real) % (w':real^3)) = vec 0` ASSUME_TAC THENL [POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC;POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]] THEN REWRITE_TAC[VECTOR_ARITH `(t1 % x + t2 % v + t3 % w') - (t1' % x + t2' % v' + t3' % w') = ((t1:real)- (t1':real)) % (x:real^3) + ((t2:real)) % (v:real^3) + ((t3:real)- (t3':real)) % (w':real^3) + (--(t2':real) % (v':real^3))`] THEN STRIP_TAC THEN SUBGOAL_THEN `((t1:real)- (t1':real)) = &0 /\  ((t2:real)) = &0 /\ ((t3:real)- (t3':real)) = &0 /\  (--(t2':real)) = &0` ASSUME_TAC THENL [ASM_MESON_TAC [dn11];SUBGOAL_THEN `(t1:real) + (t3:real) + &0 = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `(t1:real) + (t3:real) = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;EXISTS_TAC `t1:real` THEN EXISTS_TAC `t3:real` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC]]]]]);;\r
 223 \r
 224 let SUBCASE46 = prove(`!(v:real^3)(v':real^3)(w:real^3)(w':real^3)(x:real^3)(S:real^3->bool).( v IN S) /\ ( x IN S) /\ ( ~(v = x)) /\ ( dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ ( dist (w,x) <= &2 * h0) /\ ( ~(v = w)) /\ ( dist (v,w) <= &2 * h0) /\ ( e1 = {v, w}) /\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w' IN S) /\ ( ~(w' = x)) /\ ( dist (w',x) <= &2 * h0) /\ ( ~(v' = w')) /\(dist(v',w') <= &2 * h0) /\ (e2 = {v', w'}) /\(~({v, w} = {v', w'})) /\ (~(v = v')) /\ (~(v = w')) /\ (~(w = v')) /\ (~(w = w')) ==> x' IN {y | ?t1 t2 t3.t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v + t3 % w} INTER {y | ?t1 t2 t3. t2 >= &0 /\ t3 >= &0 /\ t1 + t2 + t3 = &1 /\ y = t1 % x + t2 % v' + t3 % w'}  ==> x' IN aff_ge {x} ({v, w} INTER {v', w'})`,REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC [GSYM INTER] THEN SUBGOAL_THEN `({v:real^3,w:real^3} INTER {v':real^3, w':real^3}) = {}` ASSUME_TAC THENL [ASM_MESON_TAC [dn112];ASM_REWRITE_TAC[]] THEN REWRITE_TAC [dn2;IN_SING;INTER;IN_ELIM_THM] THEN STRIP_TAC THEN SUBGOAL_THEN `(x':real^3) - ((t1':real) % (x:real^3) + (t2':real) % (v':real^3) + (t3':real) % (w':real^3)) = vec 0` ASSUME_TAC THENL [POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC;POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[]] THEN REWRITE_TAC[VECTOR_ARITH `(t1 % x + t2 % v + t3 % w) - (t1' % x + t2' % v' + t3' % w') = ((t1:real)- (t1':real)) % (x:real^3) + (t2:real) % (v:real^3) + (t3:real) % (w:real^3) + (--(t2':real) % (v':real^3)) + (--(t3':real) % (w':real^3))`] THEN STRIP_TAC THEN SUBGOAL_THEN `((t1:real)- (t1':real)) = &0 /\  ((t2:real)) = &0 /\ ((t3:real)) = &0 /\ (--(t2':real)) = &0 /\  (--(t3':real)) = &0` ASSUME_TAC THENL [ASM_MESON_TAC [dn12];SUBGOAL_THEN `(t1:real) + &0 + &0 = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;SUBGOAL_THEN `(t1:real) = &1` ASSUME_TAC THENL [ASM_ARITH_TAC;ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC]]]);;\r
 225 \r
 226 let SUBCASE47 = prove( `!(v:real^3)(v':real^3)(w:real^3)(w':real^3)(x:real^3)(S:real^3->bool).( v IN S) /\ ( x IN S) /\ ( ~(v = x)) /\ ( dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ ( dist (w,x) <= &2 * h0) /\ ( ~(v = w)) /\ ( dist (v,w) <= &2 * h0) /\ ( e1 = {v, w}) /\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w' IN S) /\ ( ~(w' = x)) /\ ( dist (w',x) <= &2 * h0) /\ ( ~(v' = w')) /\(dist(v',w') <= &2 * h0) /\ (e2 = {v', w'}) /\ ({v, w} = {v', w'}) ==> !x'. x' IN aff_ge {x} ({v, w} INTER {v', w'}) ==> x' IN aff_ge {x} {v, w} INTER aff_ge {x} {v', w'}`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC [dn8;INTER;IN_ELIM_THM]);;\r
 227 \r
 228 let SUBCASE48 = prove( `!(v:real^3)(v':real^3)(w:real^3)(w':real^3)(x:real^3)(S:real^3->bool).( v IN S) /\ ( x IN S) /\ ( ~(v = x)) /\ ( dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ ( dist (w,x) <= &2 * h0) /\ ( ~(v = w)) /\ ( dist (v,w) <= &2 * h0) /\ ( e1 = {v, w}) /\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w' IN S) /\ ( ~(w' = x)) /\ ( dist (w',x) <= &2 * h0) /\ ( ~(v' = w')) /\(dist(v',w') <= &2 * h0) /\ (e2 = {v', w'}) /\ (~({v, w} = {v', w'})) /\ (v = v') ==> !x'. x' IN aff_ge {x} ({v, w} INTER {v', w'}) ==> x' IN aff_ge {x} {v, w} INTER aff_ge {x} {v', w'}`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN SUBGOAL_THEN `({v':real^3,w:real^3} INTER {v':real^3, w':real^3}) = {v'}` ASSUME_TAC THENL [ASM_MESON_TAC [dn9];ASM_REWRITE_TAC[]] THEN REWRITE_TAC [INTER;dn3;IN_ELIM_THM] THEN STRIP_TAC THEN REWRITE_TAC [dn4] THEN STRIP_TAC THEN REWRITE_TAC [IN_ELIM_THM] THEN STRIP_TAC THENL [EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN EXISTS_TAC `&0` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]];EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN EXISTS_TAC `&0` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]]]);;\r
 229 \r
 230 let SUBCASE49 = prove(`!(v:real^3)(v':real^3)(w:real^3)(w':real^3)(x:real^3)(S:real^3->bool).( v IN S) /\ ( x IN S) /\ ( ~(v = x)) /\ ( dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ ( dist (w,x) <= &2 * h0) /\ ( ~(v = w)) /\ ( dist (v,w) <= &2 * h0) /\ ( e1 = {v, w}) /\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w' IN S) /\ ( ~(w' = x)) /\ ( dist (w',x) <= &2 * h0) /\ ( ~(v' = w')) /\(dist(v',w') <= &2 * h0) /\ (e2 = {v', w'}) /\ (~({v, w} = {v', w'})) /\ (~(v = v')) /\ (v = w') ==> !x'. x' IN aff_ge {x} ({v, w} INTER {v', w'}) ==> x' IN aff_ge {x} {v, w} INTER aff_ge {x} {v', w'}`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN SUBGOAL_THEN `({w':real^3,w:real^3} INTER {v':real^3, w':real^3}) = {w'}` ASSUME_TAC THENL [ASM_MESON_TAC [dn91];ASM_REWRITE_TAC[]] THEN REWRITE_TAC [INTER;dn3;IN_ELIM_THM] THEN STRIP_TAC THEN REWRITE_TAC [dn4] THEN STRIP_TAC THEN REWRITE_TAC [IN_ELIM_THM] THEN STRIP_TAC THENL [EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN EXISTS_TAC `&0` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]];EXISTS_TAC `t1:real` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `t2:real` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]]]);;\r
 231 \r
 232 let SUBCASE50 = prove(`!(v:real^3)(v':real^3)(w:real^3)(w':real^3)(x:real^3)(S:real^3->bool).( v IN S) /\ ( x IN S) /\ ( ~(v = x)) /\ ( dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ ( dist (w,x) <= &2 * h0) /\ ( ~(v = w)) /\ ( dist (v,w) <= &2 * h0) /\ ( e1 = {v, w}) /\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w' IN S) /\ ( ~(w' = x)) /\ ( dist (w',x) <= &2 * h0) /\ ( ~(v' = w')) /\(dist(v',w') <= &2 * h0) /\ (e2 = {v', w'}) /\ (~({v, w} = {v', w'})) /\ (~(v = v')) /\ (~(v = w')) /\ (w = v') ==> !x'. x' IN aff_ge {x} ({v, w} INTER {v', w'}) ==> x' IN aff_ge {x} {v, w} INTER aff_ge {x} {v', w'}`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN SUBGOAL_THEN `({v:real^3,v':real^3} INTER {v':real^3, w':real^3}) = {v'}` ASSUME_TAC THENL [ASM_MESON_TAC [dn92];ASM_REWRITE_TAC[]] THEN REWRITE_TAC [INTER] THEN STRIP_TAC THEN REWRITE_TAC [dn4;dn3;IN_ELIM_THM] THEN  REPEAT STRIP_TAC THENL [EXISTS_TAC `t1:real` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `t2:real` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]];EXISTS_TAC `t1:real` THEN EXISTS_TAC `t2:real` THEN EXISTS_TAC `&0` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]]]);;\r
 233 \r
 234 let SUBCASE51 = prove(`!(v:real^3)(v':real^3)(w:real^3)(w':real^3)(x:real^3)(S:real^3->bool).( v IN S) /\ ( x IN S) /\ ( ~(v = x)) /\ ( dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ ( dist (w,x) <= &2 * h0) /\ ( ~(v = w)) /\ ( dist (v,w) <= &2 * h0) /\ ( e1 = {v, w}) /\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w' IN S) /\ ( ~(w' = x)) /\ ( dist (w',x) <= &2 * h0) /\ ( ~(v' = w')) /\(dist(v',w') <= &2 * h0) /\ (e2 = {v', w'}) /\ (~({v, w} = {v', w'})) /\ (~(v = v')) /\ (~(v = w')) /\ (~(w = v')) /\ (w = w') ==> !x'. x' IN aff_ge {x} ({v, w} INTER {v', w'}) ==> x' IN aff_ge {x} {v, w} INTER aff_ge {x} {v', w'}`,REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN SUBGOAL_THEN `({v:real^3,w':real^3} INTER {v':real^3, w':real^3}) = {w'}` ASSUME_TAC THENL [ASM_MESON_TAC [dn93];ASM_REWRITE_TAC[]] THEN REWRITE_TAC [INTER;dn3;IN_ELIM_THM] THEN STRIP_TAC THEN REWRITE_TAC [dn4;IN_ELIM_THM] THEN REPEAT STRIP_TAC THENL [EXISTS_TAC `t1:real` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `t2:real` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]];EXISTS_TAC `t1:real` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `t2:real` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]]]);;\r
 235 \r
 236 let SUBCASE52 = prove( `!(v:real^3)(v':real^3)(w:real^3)(w':real^3)(x:real^3)(S:real^3->bool).( v IN S) /\ ( x IN S) /\ ( ~(v = x)) /\ ( dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ ( dist (w,x) <= &2 * h0) /\ ( ~(v = w)) /\ ( dist (v,w) <= &2 * h0) /\ ( e1 = {v, w}) /\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w' IN S) /\ ( ~(w' = x)) /\ ( dist (w',x) <= &2 * h0) /\ ( ~(v' = w')) /\(dist(v',w') <= &2 * h0) /\ (e2 = {v', w'}) /\ (~({v, w} = {v', w'})) /\ (~(v = v')) /\ (~(v = w')) /\ (~(w = v')) /\ (~(w = w')) ==> !x'. x' IN aff_ge {x} ({v, w} INTER {v', w'}) ==> x' IN aff_ge {x} {v, w} INTER aff_ge {x} {v', w'}`,REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC [GSYM INTER] THEN SUBGOAL_THEN `({v:real^3,w:real^3} INTER {v':real^3, w':real^3}) = {}` ASSUME_TAC THENL [ASM_MESON_TAC [dn112];ASM_REWRITE_TAC[]] THEN REWRITE_TAC [dn2;IN_SING;INTER;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN REWRITE_TAC [dn4;IN_ELIM_THM] THENL [EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]];EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0` THEN STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;STRIP_TAC THENL [ASM_ARITH_TAC;POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC]]]]);;\r
 237 \r
 238 let cautruc11 = prove(`!(v:real^3)(v':real^3)(w:real^3)(w':real^3)(x:real^3)(S:real^3->bool).( v IN S) /\ ( x IN S) /\ ( ~(v = x)) /\ ( dist (v,x) <= &2 * h0) /\ (w IN S) /\ (~(w = x)) /\ ( dist (w,x) <= &2 * h0) /\ ( ~(v = w)) /\ ( dist (v,w) <= &2 * h0) /\ ( e1 = {v, w}) /\ ( v' IN S) /\ ( ~(v' = x)) /\ ( dist (v',x) <= &2 * h0) /\ ( w' IN S) /\ ( ~(w' = x)) /\ ( dist (w',x) <= &2 * h0) /\ ( ~(v' = w')) /\(dist(v',w') <= &2 * h0) /\ (e2 = {v', w'}) ==> aff_ge {x} e1 INTER aff_ge {x} e2 = aff_ge {x} (e1 INTER e2)`,REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC [EXTENSION;GSYM SUBSET_ANTISYM_EQ;SUBSET;IN_ELIM_THM] THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL(*-------*)[REWRITE_TAC [dn4] THEN GEN_TAC THEN REWRITE_TAC [IN_ELIM_THM] THEN (*{v,w} = {v',w'}*)ASM_CASES_TAC `{v:real^3,w:real^3} = {v':real^3,w':real^3}` THENL [ASM_MESON_TAC [SUBCASE41];(*v = v'*)ASM_CASES_TAC `(v:real^3 = v':real^3)` THENL [ASM_MESON_TAC [SUBCASE42];(*v = w*)ASM_CASES_TAC `(v:real^3 = w':real^3)` THENL [ASM_MESON_TAC [SUBCASE43];(* w = v'*)ASM_CASES_TAC `(w:real^3 = v':real^3)` THENL [ASM_MESON_TAC [SUBCASE44];(*(w = w')*)ASM_CASES_TAC `(w:real^3 = w':real^3)` THENL [ASM_MESON_TAC [SUBCASE45];(*(~({v, w} = {v', w'}))/\ (~(v = v')) /\ (~(v = w')) /\ (~(w = v')) /\ (~(w = w')) *)ASM_MESON_TAC [SUBCASE46]]]]]];(*Small Cases*)(*{v,w} = {v',w'}*)ASM_CASES_TAC `{v:real^3,w:real^3} = {v':real^3,w':real^3}` THENL [ASM_MESON_TAC [SUBCASE47];(*v = v'*)ASM_CASES_TAC `(v:real^3 = v':real^3)` THENL [ASM_MESON_TAC [SUBCASE48];(*v = w*)ASM_CASES_TAC `(v:real^3 = w':real^3)` THENL [ASM_MESON_TAC [SUBCASE49];(* w = v'*)ASM_CASES_TAC `(w:real^3 = v':real^3)` THENL [ASM_MESON_TAC [SUBCASE50];(*(w = w')*)ASM_CASES_TAC `(w:real^3 = w':real^3)` THENL [ASM_MESON_TAC [SUBCASE51];(*(~({v, w} = {v', w'}))/\ (~(v = v')) /\ (~(v = w')) /\ (~(w = v')) /\ (~(w = w')) *)ASM_MESON_TAC [SUBCASE52]]]]]]]);;\r
 239 \r
 240 \r
 241 let them8 = prove(`!(x:real^3)(S:real^3 -> bool) e1 e2.(e1 IN (sigma_set1 x S)) /\ (e2 IN (sigma_set1 x S)) ==> ((aff_ge {x} e1) INTER (aff_ge {x} e2)) = aff_ge {x} (e1 INTER e2)`,REPEAT GEN_TAC THEN REWRITE_TAC [sigma_set1;ESTD;V;UNION;IN_ELIM_THM] THEN STRIP_TAC THENL [ASM_MESON_TAC [cautruc11];ASM_MESON_TAC [cautruc10];REWRITE_TAC [INTER] THEN ASM_MESON_TAC [cautruc9];ASM_MESON_TAC [cautruc8]]);;\r
 242 \r
 243 (*-------------------------------------------------*)\r
 244 (*Cause ECNT SUBSET ESTD then ESTD is general*)\r
 245 let  UBHDEUU  =prove(`!(x:real^3) (S:real^3 -> bool).(packing S) /\ (x IN S) ==>  new_fan (x, V x S, ESTD(V x S))`,REPEAT GEN_TAC THEN REWRITE_TAC [new_fan;fan11;fan21;fan41;fan51] THEN REPEAT STRIP_TAC THENL [REWRITE_TAC [GSYM eunion] THEN ASM_MESON_TAC [them5];REWRITE_TAC [graph] THEN GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `e IN ESTD (V x S)` ASSUME_TAC THENL[ ASM_MESON_TAC [IN];POP_ASSUM MP_TAC THEN ASM_MESON_TAC[them6]];ASM_MESON_TAC [them2];POP_ASSUM MP_TAC THEN REWRITE_TAC[] THEN ASM_MESON_TAC [them3];POP_ASSUM MP_TAC THEN REWRITE_TAC[] THEN ASM_MESON_TAC [them7];POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC [fan31] THEN REWRITE_TAC [GSYM sigma_set1] THEN ASM_MESON_TAC [them8]]);;\r
 246 \r
 247 (*=-=================================================================================================*)\r
 248 \r
 249 \r
 250 (* triangle, quadrilateral, exceptional *)\r
 251 let triangles = new_definition `triangles (H:(A)hypermap) (x:A)  \r
 252  <=> (CARD (face H x)) = 3`;;\r
 253 \r
 254 let quadilaterals = new_definition `quadilaterals (H:(A)hypermap) (x:A)\r
 255  <=> (CARD (face H x)) = 4`;;\r
 256 \r
 257 let exceptional_faces = new_definition `exceptional_faces (H:(A)hypermap)(x:A)\r
 258  <=> (CARD (face H x)) = 5`;;\r
 259 \r
 260 (*Type of a node*)\r
 261 \r
 262 let triangles_set = new_definition `triangles_set (H:(A)hypermap) (x:A) = \r
 263 {triangles H y  | y IN node H x}`;;\r
 264 \r
 265 let quadilaterals_set = new_definition ` quadilaterals_set (H:(A)hypermap) (x:A) = \r
 266 {quadilaterals H y  | y IN node H x}`;;\r
 267 \r
 268 let  exceptional_faces_set = new_definition `exceptional_faces_set (H:(A)hypermap) (x:A) = \r
 269 {exceptional_faces H y  | y IN node H x}`;;\r
 270 \r
 271 let set_of_triangles_meeting_node = new_definition `set_of_triangles_meeting_node (H:(A)hypermap) (x:A) = {face H (y:A) | y IN dart H /\ CARD (face H y) = 3 /\ y IN node H x}`;;\r
 272 \r
 273 let set_of_quadrilaterals_meeting_node = new_definition `set_of_quadrilaterals_meeting_node (H:(A)hypermap) (x:A) = {face H (y:A) | y IN dart H /\ CARD (face H y) = 4 /\ y IN node H x}`;;\r
 274 \r
 275 let set_of_exceptional_meeting_node = new_definition `set_of_exceptional_meeting_node (H:(A)hypermap) (x:A) = {face H (y:A) | y IN dart H /\ CARD (face H y) >= 5 /\ y IN node H x}`;;\r
 276 \r
 277 let p = new_definition `p (H:(A)hypermap) (x:A)\r
 278  = CARD (set_of_triangles_meeting_node H x)`;;\r
 279 \r
 280 \r
 281 let q = new_definition `q (H:(A)hypermap)(x:A)\r
 282  = CARD (set_of_quadrilaterals_meeting_node H x)`;;\r
 283 \r
 284 let r = new_definition `r (H:(A)hypermap) (x:A)\r
 285  = CARD (set_of_exceptional_meeting_node H x )`;;\r
 286 \r
 287 let type_of_node = new_definition `type_of_node (H:(A)hypermap) (x:A) =  (p H x,q H x,r H x )`;;\r
 288 (*let type_of_node = new_definition `type_of_node (H:(A)hypermap) (x:A) =  (CARD (set_of_triangles_meeting_node H x), CARD (set_of_quadrilaterals_meeting_node H x), CARD (set_of_exceptional_meeting_node H x ))`;;*)\r
 289 \r
 290 let tgt = new_definition `tgt = #1.541`;;\r
 291 \r
 292 (* Definition L --> the linear interpolation*)\r
 293 \r
 294 let atn2 = new_definition `atn2(x,y) =\r
 295     if ( abs y < x ) then atn(y / x) else\r
 296     (if (&0 < y) then ((pi / &2) - atn(x / y)) else\r
 297     (if (y < &0) then (-- (pi/ &2) - atn (x / y)) else (  pi )))`;;\r
 298 \r
 299 let ups_x = new_definition `ups_x x1 x2 x6 = \r
 300     --x1*x1 - x2*x2 - x6*x6 \r
 301     + &2 *x1*x6 + &2 *x1*x2 + &2 *x2*x6`;;\r
 302 \r
 303 let arclength = new_definition `arclength a b c  =\r
 304 pi/(&2) + (atn2( (sqrt (ups_x (a*a) (b*b) (c*c))),(c*c - a*a  -b*b)))`;;\r
 305 \r
 306 (*Definition faces of hypermap of cardinality at least 7*)  \r
 307 \r
 308 let FF = new_definition `FF (H:(A)hypermap) (x:A)  \r
 309  <=> (CARD (face H x))>= 7`;;\r
 310 \r
 311  \r
 312 let h1 = new_definition `h1 = {x|(&1 <= x) /\ (x <= h0)}`;;\r
 313 \r
 314 let L = new_definition `L x = \r
 315     if x = &1 then &1 else \r
 316     (if x = h0 then &0 else\r
 317     (if (x < h0) then ((h0 - x)/ (h0 - (&1)))\r
 318   else \r
 319      &0))`;;\r
 320 \r
 321 let thm_arc = `!u w. (u IN (V x S)) /\ (w IN (edge H u))  ==>  \r
 322  let dux = dist (u,x) in\r
 323  let dwx = dist (w,x) in\r
 324  let duw = dist (u,w) in\r
 325   arclength dux dwx duw >= arclength dux dwx (&2)`;;\r
 326 \r
 327 let thm_arc1 = `!u w.(u IN (V x S)) /\ (w IN (edge H u)) ==>\r
 328   let dux = dist (u,x) in\r
 329   let dwx = dist (w,x) in\r
 330   arclength dux dwx (&2) >= (&1) - ((#0.6076)*((dux/(&2)) - (&1))) - ((#0.6076)*((dwx/(&2)) - (&1)))`;;\r
 331 \r
 332 \r
 333 \r
 334 \r
 335 \r
 336 end;;\r