2 (* tchales, This does not run in Multivariate *)
5 let TRIANGLE_IN_BARRIER = prove(` ! s v0 v1 v2 . {v0, v1, v2} IN barrier s
7 ~(xx = yy) /\ {xx, yy} SUBSET {v1, v2, v0}
8 ==> &2 <= dist (xx,yy) /\ dist (xx,yy) <= sqrt (&8)) /\
10 aa IN {v1, v2, v0} /\ bb IN {v1, v2, v0} ==> dist (aa,bb) <= #2.51) \/
12 {aa, bb} SUBSET {v1, v2, v0} /\
13 #2.51 < dist (aa,bb) /\
15 ~({x, y} = {aa, bb}) /\ {x, y} SUBSET {v1, v2, v0}
16 ==> dist (x,y) <= #2.51)))`,
17 REWRITE_TAC[ barrier; IN_ELIM_THM] THEN
18 REWRITE_TAC[ GSYM (MESON[]` P {x, y, z} <=>
19 (?a b c. P {a, b, c} /\ {x, y, z} = {a, b, c})`)] THEN
21 REWRITE_TAC[ MESON[]` (! a b c d. P a b c d ==> las a b c d ) ==> (! a b c d .
22 P a b c d \/ Q a b c d ==> las a b c d) <=>
23 (! a b c d. P a b c d ==> las a b c d ) ==> (! a b c d .
24 Q a b c d ==> las a b c d)`] THEN DISCH_TAC THEN
25 NHANH (CUTHE2 CASES_OF_Q_SYS) THEN
27 MATCH_MP_TAC (MESON[]` ((? a. Q a) ==> l) /\ ((?a. R a ) ==> l) ==>
28 (? a. P a /\ ( Q a \/ R a )) ==> l `) THEN
29 REWRITE_TAC[ NOV1] THEN
30 NHANH (CUTHE4 TRIANGLE_IN_STRICT_QUA) THEN
31 MATCH_MP_TAC (MESON[]` (b ==> l) /\ ( a /\ c ==> l) ==> a /\ ( b \/ c ) ==> l`) THEN
32 ASM_REWRITE_TAC[] THEN
33 REWRITE_TAC[ strict_qua; quarter; SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`; def_simplex] THEN
35 REWRITE_TAC[ MESON[]` a /\ a /\ l <=> a /\ l `; packing ] THEN
36 MATCH_MP_TAC (MESON[] `(a ==> aa) /\ (b ==> bb) ==> a /\ b ==> aa /\ (cc \/ bb)`) THEN
37 SIMP_TAC[ SET_RULE `{a,b,c} = {c,a,b} `] THEN
38 NHANH (SET_RULE ` {v0, v1, v2, v4} SUBSET s ==> {v0,v1,v2} SUBSET s `) THEN
39 NHANH ( MESON[SET_RULE ` x IN a /\ a SUBSET s ==> s x `]`(!u v. s u /\ s v /\ ~(u = v) ==> &2 <= dist (u,v)) /\
40 ({v0, v1, v2, v4} SUBSET s /\ {v0, v1, v2} SUBSET s) /\ l ==>
41 (!u v. u IN {v0,v1,v2} /\ v IN {v0,v1,v2} /\ ~(u = v) ==> &2 <= dist (u,v))`) THEN
43 NHANH ( MESON[PAIR_D3] ` d3 v w <= sqrt (&8) ==> (! x y. x IN {v0, v1, v2, v4} /\
44 y IN {v0, v1, v2, v4} /\ {x,y} = {v,w} ==> d3 x y <= sqrt (&8) )`) THEN
45 REWRITE_TAC[ SET_RULE ` {a,b} SUBSET s <=> a IN s /\ b IN s `] THEN
46 SIMP_TAC[ SET_RULE ` {a,b,c} = {c,a,b} `] THEN
47 REWRITE_TAC[ GSYM d3 ] THEN
48 MESON_TAC[ MATCH_MP REAL_LE_RSQRT (REAL_ARITH ` (&2 * #1.255 ) pow 2 <= &8 `);
49 SET_RULE ` x IN {a,b,c} ==> x IN {a,b,c,d} `; REAL_ARITH ` a <= b /\ b <= c ==> a <= c `]);;
61 let le1_82 = prove (`!s v0 Y.
66 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s}
67 ==> UNIONS {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2} IN barrier s} SUBSET
68 Y`, SIMP_TAC[] THEN SET_TAC[]);;
72 let rhand_subset_lhand = prove (` ! (s:real^3 -> bool) (v0:real^3) Z Y.
76 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
77 Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s}
79 normball v0 t0 INTER voronoi v0 s DIFF (Y UNION Z) SUBSET
80 normball v0 t0 INTER VC v0 s DIFF (Y UNION Z)`, REWRITE_TAC[ SET_RULE ` a INTER b DIFF c SUBSET a INTER d DIFF c <=>
81 (!x. x IN a INTER b DIFF c ==> x IN d) ` ] THEN
82 REWRITE_TAC[ GSYM ( MESON[centered_pac; le1_82; prove (` ! x s. centered_pac s x ==> x IN near2t0 x s `, REWRITE_TAC[
83 centered_pac; near2t0] THEN REWRITE_TAC[ MESON [DIST_REFL; t0; REAL_ARITH ` &0 < &2 * #1.255 `] `
84 packing s /\ v0 IN s <=> packing s /\ v0 IN s /\ dist (v0,v0) < &2 * t0`] THEN
85 SET_TAC[] ) ] ` !s v0 Z Y.
89 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
90 Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\
91 UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
97 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
98 Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s}
100 REWRITE_TAC[SET_RULE ` x IN a INTER b DIFF c <=> x IN a /\ x IN b /\ ~( x IN c )`] THEN
101 REWRITE_TAC[ MESON[] ` centered_pac s v0 /\
104 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
105 Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\
106 UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
108 ==> (!x. x IN normball v0 t0 /\ x IN voronoi v0 s /\ ~(x IN Y UNION Z)
109 ==> x IN VC v0 s) <=>
113 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
114 Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\
115 UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
117 ==> (!x. x IN normball v0 t0 /\
121 {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
123 ==> x IN VC v0 s) `] THEN
124 ONCE_REWRITE_TAC[ SET_RULE ` ~(x IN Y UNION Z) /\
125 UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
128 UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s}) /\
130 UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
131 Y `] THEN REWRITE_TAC[ centered_pac ] THEN
132 REWRITE_TAC[ MESON[] ` (packing s /\ v0 IN s) /\
135 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
136 Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\
137 UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
139 ==> (!x. x IN normball v0 t0 /\
143 {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s}) /\
146 {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
148 ==> x IN VC v0 s) <=>
149 (packing s /\ v0 IN s) /\
152 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
153 Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s} /\
154 UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
157 x IN normball v0 t0 /\
161 {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s}) /\
164 {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
166 ==> x IN VC v0 s) `] THEN
167 REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[normball] THEN
168 REWRITE_TAC[ SET_RULE ` z IN { x | P x } <=> P z `] THEN
169 REWRITE_TAC[ voronoi; VC; lambda_x; d3 ] THEN
170 REWRITE_TAC[ SET_RULE ` x IN { x | P x } <=> P x `] THEN
171 REWRITE_TAC[MESON[DIST_SYM ; import_le ] ` v0 IN s /\
173 (!w. s w /\ ~(w = v0) ==> dist (x,v0) < dist (x,w)) /\
175 UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s}) /\
177 UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
181 (!w. s w /\ ~(w = v0) ==> dist (x,v0) < dist (x,w)) /\
183 UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s}) /\
185 UNIONS {aff_ge {v0} {w1, w2} | w1,w2 | {v0, w1, w2} IN barrier s} SUBSET
187 ~obstructed v0 x s `] THEN
188 ONCE_REWRITE_TAC[MESON[t0; REAL_ARITH ` #1.255 < &2 /\ (! a b (c:real). a < b
189 /\ b < c ==> a < c ) `; DIST_SYM ]` dist ( x, v0 ) < t0 <=> dist ( x, v0 ) < t0 /\
190 dist ( v0, x) < &2 `] THEN
191 SIMP_TAC[ DIST_SYM ] THEN
192 MESON_TAC[ SET_RULE ` ! s x. s x <=> x IN s `]);;
196 (* ++++++++++++++++++++++++++++ *)
201 let lhand_subset_rhand = prove(` ! (s:real^3 -> bool) (v0:real^3) Z Y.
205 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
206 Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s}
207 ==> normball v0 t0 INTER VC v0 s DIFF (Y UNION Z) SUBSET
208 normball v0 t0 INTER voronoi v0 s DIFF (Y UNION Z)`,
209 REWRITE_TAC[ SET_RULE ` a INTER b DIFF c SUBSET a INTER d DIFF c <=>
210 a INTER b DIFF c DIFF d = {} `] THEN
211 REWRITE_TAC[ SET_RULE ` a = {} <=> (! x. ~ (x IN a))`] THEN
212 REWRITE_TAC[ SET_RULE` x IN a DIFF b <=> x IN a /\ ~( x IN b ) `] THEN
213 REWRITE_TAC[ SET_RULE ` x IN a INTER b <=> x IN a /\ x IN b `] THEN PHA THEN
214 REWRITE_TAC[ SET_RULE ` x IN normball v0 t0 /\ x IN VC v0 s /\ ~(x IN Y UNION Z) /\ P x <=>
215 x IN normball v0 t0 DIFF Z /\ x IN VC v0 s /\ ~(x IN Y UNION Z) /\ P x `] THEN
216 REWRITE_TAC[MESON[lemma_of_lemma82]`
220 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
221 Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s}
222 ==> (!x. ~(x IN normball v0 t0 DIFF Z /\
225 ~(x IN voronoi v0 s))) <=>
229 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
230 Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s}
231 ==> (!x. ~(x IN normball v0 t0 DIFF Z /\
232 (?w. w IN near2t0 v0 s /\ x IN voronoi w s) /\
235 ~(x IN voronoi v0 s))) `] THEN
236 REWRITE_TAC[ MESON[] `
237 (?w. w IN near2t0 v0 s /\ x IN voronoi w s) /\
240 ~(x IN voronoi v0 s) <=>
241 (?w. w IN near2t0 v0 s /\ x IN voronoi w s /\ ~(w = v0)) /\
244 ~(x IN voronoi v0 s) `] THEN
245 REWRITE_TAC[ MESON[near2t0] `
246 (?w. w IN near2t0 v0 s /\ x IN voronoi w s /\ ~(w = v0)) <=>
247 (?w. w IN {x | x IN s /\ dist (v0,x) < &2 * t0} /\
250 REWRITE_TAC[ SET_RULE` a IN { a | p a } <=> p a `] THEN
251 REWRITE_TAC[ voronoi; lambda_x] THEN
252 REWRITE_TAC[ SET_RULE ` x IN { v | P v } <=> P x `] THEN PHA THEN
253 REWRITE_TAC[ MESON[] ` a /\ b /\ d ==> c <=> b /\ d ==> a ==> c `] THEN
254 REPEAT GEN_TAC THEN DISCH_TAC THEN
255 REWRITE_TAC[centered_pac] THEN
256 MATCH_MP_TAC (MESON[]` (a /\ b ==> (!x. ~b \/ P x)) ==> a /\ b ==> (!x. P x)`) THEN
257 REWRITE_TAC[ MESON[] ` ~(v0 IN s) \/ ~(x IN normball v0 t0 DIFF Z /\ last) <=>
258 ~(v0 IN s /\ x IN normball v0 t0 DIFF Z /\ last)`] THEN
259 REWRITE_TAC[ MESON[]`
261 x IN normball v0 t0 DIFF Z /\
263 dist (v0,w) < &2 * t0 /\
264 (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
267 x IN normball v0 t0 DIFF Z /\
270 dist (v0,w) < &2 * t0 /\
271 (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
274 REWRITE_TAC[ MESON[ SET_RULE` x IN s <=> s x `] `
277 dist (v0,w) < &2 * t0 /\
278 (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
282 dist (x,w) < dist (x,v0) /\
283 dist (v0,w) < &2 * t0 /\
284 (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
286 REWRITE_TAC[ SET_RULE ` x IN a DIFF b <=> x IN a /\ ~ ( x IN b ) `] THEN
287 REWRITE_TAC[ MESON[normball ; SET_RULE `x IN { x | p x } <=> p x `] ` x IN normball v0 t0
288 <=> dist (x,v0) < t0 `] THEN
289 REWRITE_TAC[ MESON[REAL_ARITH ` a < b /\ b < c ==> a < c `]`
290 (dist (x,v0) < t0 /\ ~(x IN Z)) /\
293 dist (x,w) < dist (x,v0) /\
294 dist (v0,w) < &2 * t0 /\
295 (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
297 <=> (dist (x,v0) < t0 /\ ~(x IN Z)) /\
299 v0 IN s /\ dist(x,w) < t0 /\
300 dist (x,w) < dist (x,v0) /\
301 dist (v0,w) < &2 * t0 /\
302 (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
303 ~(w = v0)) /\ las `] THEN
304 ASM_SIMP_TAC[] THEN PHA THEN
305 REWRITE_TAC[ MESON[] ` a /\ b /\ c /\ d /\ las <=> (a /\ d ) /\ b /\ c /\ las `] THEN
306 ONCE_REWRITE_TAC[ MESON[near2t0; SET_RULE ` x IN { x | p x } <=> p x ` ]` (w IN s /\ dist (v0,w) < &2 * t0) <=>
307 w IN near2t0 v0 s /\ (w IN s /\ dist (v0,w) < &2 * t0) `] THEN
308 REWRITE_TAC[ SET_RULE ` ~ ( x IN a UNION b) <=> ~( x IN a ) /\ ~ (x IN b)`] THEN PHA THEN
309 SIMP_TAC[MESON[] ` a /\ a /\ b <=> a /\ b `] THEN
310 REWRITE_TAC[ MESON[] ` a/\ b /\ ( ? w. P w ) /\ la <=> b /\ ( ? w. a /\ P w ) /\ la `] THEN
311 ONCE_REWRITE_TAC[ MESON[ SET_RULE ` w IN near2t0 v0 s
312 ==> UNIONS {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2} IN barrier s} SUBSET
314 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} `]
315 ` w IN near2t0 v0 s /\
317 <=> UNIONS {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2} IN barrier s} SUBSET
319 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
321 w IN s /\ last `] THEN
322 REWRITE_TAC[ MESON[] ` a /\ b /\ c /\ d /\ last <=> a /\ b /\ ( c/\ d ) /\ last `] THEN
323 REWRITE_TAC[ SET_RULE ` ~ ( x IN a ) /\ b SUBSET a <=> ~ ( x IN a )/\ ~( x IN b ) /\ b SUBSET a`] THEN PHA THEN
324 REWRITE_TAC[ MESON[DIST_SYM; import_le ] ` dist (x,v0) < t0 /\
328 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\
329 {w, w1, w2} IN barrier s}) /\
332 {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2} IN barrier s}) /\
334 {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2} IN barrier s} SUBSET
336 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\
337 {w, w1, w2} IN barrier s} /\
340 dist (v0,w) < &2 * t0 /\
341 (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
343 dist (x,w) < dist (x,v0) /\
345 <=> dist (x,v0) < t0 /\
349 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\
350 {w, w1, w2} IN barrier s}) /\
353 {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2} IN barrier s}) /\
355 {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2} IN barrier s} SUBSET
357 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\
358 {w, w1, w2} IN barrier s} /\
361 dist (v0,w) < &2 * t0 /\
362 (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
364 dist (x,w) < dist (x,v0) /\
365 ~(w = v0) /\ ~obstructed w x s `] THEN
366 ONCE_REWRITE_TAC[ MESON[t0; REAL_ARITH ` #1.255 < &2 /\ (! a b c. a < b /\ b < c ==> a < c )` ] `
367 dist (x,w) < t0 /\ dist (x,w) < dist (x,v0) /\ last <=>
368 dist (x,w) < &2 /\ dist (x,w) < t0 /\ dist (x,w) < dist (x,v0) /\ last`] THEN
369 REWRITE_TAC[ MESON[ in_VC; DIST_SYM ] `w IN s /\
370 dist (v0,w) < &2 * t0 /\
371 (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
374 dist (x,w) < dist (x,v0) /\
376 ~obstructed w x s <=>
377 dist (v0,w) < &2 * t0 /\
380 dist (x,w) < dist (x,v0) /\
382 (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
384 ~obstructed w x s` ] THEN
385 REWRITE_TAC[ MESON[DIST_SYM] ` dist(x,w) < &2 <=> dist (w,x) < &2 `] THEN
386 REWRITE_TAC[MESON[in_VC]` w IN s /\
387 (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
391 (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
393 ~obstructed w x s /\ x IN VC w s ` ] THEN
394 REWRITE_TAC[ MESON[]` ~(w = v0) /\
395 dist (x,w) < dist (x,v0) /\
397 (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
402 dist (x,w) < dist (x,v0) /\
404 (!w'. s w' /\ ~(w' = w) ==> dist (x,w) < dist (x,w')) /\
407 ~(w = v0) /\ x IN VC w s `] THEN
408 ONCE_REWRITE_TAC[ MESON[]` dist (x,v0) < t0 /\
409 x IN VC v0 s /\ last <=> dist (x,v0) < t0 /\ last /\ x IN VC v0 s `]
411 ONCE_REWRITE_TAC[SET_RULE ` x IN a /\ x IN b <=> ~ ( a INTER b = {} ) /\ x IN a /\ x IN b `] THEN
412 SIMP_TAC[ MESON[VC_DISJOINT ] ` ~(w = v0) /\
413 ~(VC w s INTER VC v0 s = {}) /\
415 x IN VC v0 s <=> F `]);;
418 (* +++++++++++++++++++++++++ *)
420 let lemma82_FOCUDTG = prove (`! (s:real^3 -> bool) (v0:real^3) Z Y.
424 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} /\
425 Z = UNIONS {e_plane u v | u IN near2t0 v0 s /\ v IN near2t0 v0 s}
426 ==> normball v0 t0 INTER VC v0 s DIFF (Y UNION Z) =
427 normball v0 t0 INTER voronoi v0 s DIFF (Y UNION Z)`,
428 REWRITE_TAC[ SET_RULE ` a ==> (b = c) <=> a ==>( b SUBSET c /\ c SUBSET b ) `]
429 THEN MESON_TAC[ lhand_subset_rhand; rhand_subset_lhand] );;
431 (* ========= END LEMMA 8.2 ======== *)
433 let a_le_sub = SET_RULE ` w IN near2t0 v0 s
434 ==> UNIONS {aff_ge {w} {w1, w2} | w1,w2 | {w, w1, w2} IN barrier s} SUBSET
436 {aff_ge {w} {w1, w2} | w IN near2t0 v0 s /\ {w, w1, w2} IN barrier s} `;;
459 (* ============= BEGIN LEMMA 8.3 =========== *)
462 let barrier' = new_definition ` barrier' v0 s =
463 {{a, b, c} | {a, b, c} IN barrier s /\ v0 IN {a, b, c} \/
464 (?q. diagonal a b q s /\ q IN Q_SYS s /\ c IN anchor_points a b s)} `;;
467 let lemma7_7_CXRHOVG = new_axiom `!s q1 q2 v w.
468 {v, w} SUBSET q1 INTER q2 /\ quarter q2 s /\ diagonal v w q1 s /\ q1 IN Q_SYS s
469 ==> q2 IN Q_SYS s `;;
472 let tarski_UMMNOJN = new_axiom` !x w v0 v1 v2.
473 ~(conv {x, w} INTER cone v0 {v1, v2} = {}) /\
474 dist (x,v0) < dist (x,v1) /\
475 dist (x,v0) < dist (x,v2) /\
476 dist (x,w) < dist (x,v0) /\
478 ~(xx = yy) /\ {xx, yy} SUBSET {v1, v2, v0}
479 ==> &2 <= dist (xx,yy) /\ dist (xx,yy) <= sqrt (&8)) /\
481 aa IN {v1, v2, v0} /\ bb IN {v1, v2, v0}
482 ==> dist (aa,bb) <= #2.51) \/
484 {aa, bb} SUBSET {v1, v2, v0} /\
485 #2.51 < dist (aa,bb) /\
487 ~({x, y} = {aa, bb}) /\ {x, y} SUBSET {v1, v2, v0}
488 ==> dist (x,y) <= #2.51)))
489 ==> (!a. a IN {v1, v2, v0} ==> dist (w,a) <= #2.51) /\
490 ~(conv {v0, v1, v2} INTER conv0 {x, w} = {}) `;;
492 (* ================ *)
494 let TRIANGLE_IN_BARRIER' = prove(
496 {v0, v1, v2} IN barrier' v0 s
498 ~(xx = yy) /\ {xx, yy} SUBSET {v1, v2, v0}
499 ==> &2 <= dist (xx,yy) /\ dist (xx,yy) <= sqrt (&8)) /\
501 aa IN {v1, v2, v0} /\ bb IN {v1, v2, v0}
502 ==> dist (aa,bb) <= #2.51) \/
504 {aa, bb} SUBSET {v1, v2, v0} /\
505 #2.51 < dist (aa,bb) /\
507 ~({x, y} = {aa, bb}) /\ {x, y} SUBSET {v1, v2, v0}
508 ==> dist (x,y) <= #2.51))) `,
509 REWRITE_TAC[ barrier'; IN_ELIM_THM] THEN MATCH_MP_TAC (MESON[] ` (!s v0 v1 v2.
511 ({a, b, c} IN barrier s /\ v0 IN {a, b, c} \/
512 (?q. diagonal a b q s /\ c IN anchor_points a b s)) /\
513 {v0, v1, v2} = {a, b, c})
517 ({a, b, c} IN barrier s /\ v0 IN {a, b, c} \/
518 (?q. diagonal a b q s /\
520 c IN anchor_points a b s)) /\
521 {v0, v1, v2} = {a, b, c})
522 ==> las s v0 v1 v2 )`) THEN
523 REWRITE_TAC[ MESON[]` ( ? a b c. ( P {a,b,c} \/ Q a b c ) /\ {v0, v1, v2} = {a, b, c} ) <=>
524 P {v0, v1, v2} \/ ( ? a b c. Q a b c /\ {v0, v1, v2} = {a, b, c} ) `] THEN
526 MATCH_MP_TAC (MESON[]` (a ==> l) /\ (c ==> l) ==> a /\ b \/ c ==> l`) THEN
527 REWRITE_TAC[ TRIANGLE_IN_BARRIER] THEN
528 NHANH (CUTHE4 DIA_OF_QUARTER) THEN
529 REWRITE_TAC[ anchor_points; IN_ELIM_THM; anchor] THEN
530 NHANH (MESON[diagonal; quarter] ` diagonal a b q s ==> packing s `) THEN PHA THEN
531 REWRITE_TAC[ MESON[] ` packing s /\ aa /\ bb /\ cc /\ {c, a, b} SUBSET s /\ l
532 <=> ( packing s /\ {c, a, b} SUBSET s ) /\ aa /\ bb /\ cc /\ l `] THEN
533 NHANH (CUTHE2 SUB_PACKING ) THEN
534 REWRITE_TAC[GSYM d3] THEN
535 REWRITE_TAC[ REAL_ARITH ` &2 * t0 <= d3 a b <=> d3 a b <= &2 * t0 /\ &2 * t0 = d3 a b \/ &2 * t0
536 < d3 a b `; t0; REAL_ARITH ` &2 * #1.255 = #2.51 ` ] THEN
537 REWRITE_TAC[ SET_RULE ` {x,y} SUBSET s <=> x IN s /\ y IN s`] THEN
538 SIMP_TAC[ SET_RULE `!a b c. {c, a, b} = {a, b, c}`] THEN PHA THEN
539 REWRITE_TAC[ MESON[]` a /\ b /\ a /\ l <=> a /\ b /\ l `] THEN
541 REWRITE_TAC[ MESON[]` (?q. P q /\ l1 \/ P q /\ l2) <=> (?q. P q) /\ (l1 \/ l2)`] THEN
543 MATCH_MP_TAC (MESON[] ` ((? a b c. Q a b c) ==> l) ==> (? a b c. P a b c /\ Q a b c ) ==> l `) THEN
544 REWRITE_TAC[ MESON[]` ( a \/ b ) /\ c <=> a /\ c \/ b /\ c `] THEN
545 ONCE_REWRITE_TAC[ MESON[]` (d3 a b <= #2.51 /\ l <=> l /\ d3 a b <= #2.51) /\
546 (#2.51 < d3 a b /\ l <=> l /\ #2.51 < d3 a b) `] THEN PHA THEN
547 REWRITE_TAC[ MESON[]` d3 c a <= #2.51 /\
549 d3 a b <= #2.51 /\ l <=> ( d3 a b <= #2.51 /\
551 d3 c b <= #2.51 ) /\ l `] THEN
553 prove(`! a b c. d3 a b <= #2.51 /\ d3 c a <= #2.51 /\
554 d3 c b <= #2.51 ==> (!aa bb. aa IN {a,b,c} /\ bb IN {a,b,c} ==> d3 aa bb <= #2.51)`,
555 REWRITE_TAC[ SET_RULE ` x IN {a,b,c} <=> x = a \/ x= b \/ x= c `] THEN
556 MESON_TAC[ D3_REFL; trg_d3_sym; REAL_ARITH ` &0 <= #2.51 `]))) THEN
557 REWRITE_TAC[ MESON[] ` d3 a b <= sqrt (&8) /\
566 d3 a b <= sqrt (&8) /\
568 d3 c b <= #2.51 `] THEN
572 d3 a b <= sqrt (&8) /\
580 ~({x, y} = {aa, bb}) /\ x IN {a, b, c} /\ y IN {a, b, c}
581 ==> d3 x y <= #2.51)) /\
583 ~(xx = yy) /\ xx IN {a,b,c} /\ yy IN {a,b,c}
584 ==> d3 xx yy <= sqrt (&8))`,
585 REWRITE_TAC[ MESON[]` (? a b. P a b ) /\ l <=> (? a b. P a b /\ l ) `] THEN
586 REWRITE_TAC[ SET_RULE ` x IN {a,b,c} <=> x = a \/ x = b \/ x = c `] THEN
587 REPEAT GEN_TAC THEN DISCH_TAC THEN EXISTS_TAC `a:real^3` THEN EXISTS_TAC `b:real^3`
588 THEN FIRST_X_ASSUM MP_TAC THEN
589 REWRITE_TAC[ SET_RULE `{a,b} ={x,y} <=> a = x /\ b = y \/ a = y /\ b = x `] THEN
590 MESON_TAC[trg_d3_sym; db_t0_sq8; D3_REFL; REAL_ARITH ` &0 <= #2.51 /\ (! a b c. a <= b /\ b < c ==> a <= c )`]))) THEN
592 ONCE_REWRITE_TAC[ MESON[] `(! x y. P x y ) /\ l <=> l /\ (! x y. P x y) `] THEN
594 ONCE_REWRITE_TAC[ SET_RULE ` {v0, v1, v2} = {a, b, c} <=> {v1, v2, v0} = {a, b, c}`] THEN
595 NHANH ( MESON[db_t0_sq8 ; REAL_ARITH ` a <= b /\ b < c ==> a <= c `]` (!aa bb. aa IN {a, b, c} /\ bb IN {a, b, c} ==> d3 aa bb <= #2.51) /\
596 {v1, v2, v0} = {a, b, c} /\
597 (!x y. x IN {a, b, c} /\ y IN {a, b, c} /\ ~(x = y) ==> &2 <= d3 x y)
598 ==> (! x y. ~(x=y) /\ x IN {v1,v2,v0} /\ y IN {v1,v2,v0}==> &2 <= d3 x y /\
599 d3 x y <= sqrt (&8)) `) THEN
600 PHA THEN REWRITE_TAC[ MESON[]` {v1, v2, v0} = {a, b, c} /\ l <=> l /\ {v1, v2, v0} = {a, b, c}`] THEN PHA THEN
601 PURE_ONCE_REWRITE_TAC[ MESON[]` P {a,b,c} /\ Q {a,b,c} /\ R {a,b,c} /\ {v1,v2,v0} = {a,b,c} <=> P {v1,v2,v0} /\
602 Q {v1,v2,v0} /\ R {v1,v2,v0} /\ {v1,v2,v0} = {a,b,c} ` ] THEN
610 let NOV6 = prove(` ! s v0 v1 v2 w. packing s /\
611 CARD {v0, v1, v2, w} = 4 /\
612 (!a. a IN {v1, v2, v0} ==> dist (w,a) <= #2.51) /\
613 {v0, v1, v2, w} SUBSET s /\
615 {a, b, c} = {v0, v1, v2} /\
617 d3 a b <= sqrt (&8) /\
618 c IN anchor_points a b s)
619 ==> quarter {v0, v1, v2, w} s`,
620 REWRITE_TAC[ quarter; def_simplex] THEN
621 REWRITE_TAC[ prove(`! v0 v1 v2 w. CARD {v0, v1, v2, w} = 4 <=> ~(v0 = v1 \/ v0 = v2 \/ v0 = w \/ v1 = v2 \/ v1 = w \/ v2 = w)`,
622 REWRITE_TAC[ CARD4] THEN SET_TAC[])] THEN
624 NHANH ( SET_RULE ` {a, b, c} = {v0, v1, v2} ==> a IN {v0,v1,v2,w} /\
625 b IN {v0,v1,v2,w} `) THEN
626 REWRITE_TAC[ MESON[]` (!a . P a ) /\ a /\ (? a b c. Q a b c) <=>
627 a /\ (?a b c. Q a b c /\ (!a . P a ))`] THEN
628 REWRITE_TAC[ anchor_points; anchor; IN_ELIM_THM] THEN PHA THEN
629 SIMP_TAC[ SET_RULE ` {v1, v2, v0} = {v0, v1, v2}`] THEN
630 PURE_ONCE_REWRITE_TAC[ MESON []` {a, b, c} = {v0, v1, v2} /\ P {v0, v1, v2}
631 <=> {a, b, c} = {v0, v1, v2} /\ P {a, b, c}`] THEN
632 ONCE_REWRITE_TAC[ DIST_SYM] THEN
633 REWRITE_TAC[ GSYM d3 ] THEN
634 REWRITE_TAC[ MESON[t0; REAL_ARITH ` #2.51 = &2 * #1.255 `] ` #2.51 = &2 * t0 `] THEN
635 NHANH (CUTHE4 SHORT_EDGES) THEN
636 PURE_ONCE_REWRITE_TAC[ SET_RULE ` {a, b, c, w} = w INSERT {a,b,c} `] THEN
637 PURE_ONCE_REWRITE_TAC[ GSYM (MESON []` {a, b, c} = {v0, v1, v2} /\ P {v0, v1, v2}
638 <=> {a, b, c} = {v0, v1, v2} /\ P {a, b, c}`)] THEN MESON_TAC[]);;
642 let NOV7 = prove(`!s v0 v1 v2 w x . CARD {v0, v1, v2, w, x} = 5 /\
643 (!a. a IN {v1, v2, v0} ==> dist (w,a) <= #2.51) /\
644 {v0, v1, v2, w} SUBSET s /\
646 (?q. diagonal a b q s /\ q IN Q_SYS s /\ c IN anchor_points a b s) /\
647 {v0, v1, v2} = {a, b, c})
648 ==> {v0, v1, v2, w} IN Q_SYS s`,
649 ONCE_REWRITE_TAC[ SET_RULE ` {v0, v1, v2, w, x} = {x,v0, v1, v2, w}`] THEN
650 REWRITE_TAC[CARD5; GSYM CARD4] THEN
651 NHANH (CUTHE4 DIA_OF_QUARTER) THEN
652 NHANH (MESON[diagonal; quarter] `diagonal a b q s ==> packing s `) THEN
653 PHA THEN REWRITE_TAC[ MESON[]` (?q. diagonal a b q s /\ a1 /\ a2 /\ a3 /\ q IN Q_SYS s /\ a4) <=>
654 a1 /\ a2 /\ a3 /\ a4 /\ (?q. diagonal a b q s /\ q IN Q_SYS s) `] THEN
655 NHANH ( MESON[NOV6]` CARD {v0, v1, v2, w} = 4 /\
656 (!a. a IN {v1, v2, v0} ==> dist (w,a) <= #2.51) /\
657 {v0, v1, v2, w} SUBSET s /\
661 d3 a b <= sqrt (&8) /\
662 c IN anchor_points a b s /\
663 (?q. diagonal a b q s /\ q IN Q_SYS s)) /\
664 {v0, v1, v2} = {a, b, c})
665 ==> quarter {v0, v1, v2, w} s`) THEN
666 PHA THEN REWRITE_TAC[ MESON[]` (? a. P a) /\ aa <=> (? a . P a /\ aa )`] THEN
667 NHANH (MESON[diagonal] ` diagonal a b q s ==> {a,b} SUBSET q `) THEN
668 PHA THEN REWRITE_TAC[ MESON[]` (? a. P a) /\ aa <=> (? a . P a /\ aa )`] THEN
669 NHANH (SET_RULE ` {v0, v1, v2} = {a, b, c} ==> {a,b} SUBSET {v0,v1,v2,w} `) THEN
670 REWRITE_TAC[ SET_RULE ` {a, b} SUBSET q /\ aa /\ bb /\ {a, b} SUBSET {v0, v1, v2, w} <=>
671 {a, b} SUBSET q INTER {v0, v1, v2, w} /\ aa /\ bb`] THEN
672 MESON_TAC[lemma7_7_CXRHOVG]);;
675 let lemma8_3_OVOAHCG =prove(`!s v0 v1 v2 w x. {v0, v1, v2, w} SUBSET s /\ CARD {v0,v1,v2,w,x} = 5 /\
677 ~(conv {x, w} INTER aff_ge {v0} {v1, v2} = {}) /\
678 {v0, v1, v2} IN barrier' v0 s /\
679 unobstructed v0 x s /\
680 dist (x,v0) < dist (x,v1) /\
681 dist (x,v0) < dist (x,v2)
683 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[ MESON[] ` a ==> ~b <=> a /\ b ==> ~b`] THEN
684 REWRITE_TAC[IN_ELIM_THM] THEN
685 NHANH (MESON[CARD5] ` CARD {x, w, v0, v1, v2} = 5 ==> ~(x IN {w,v0,v1,v2})`) THEN
686 NHANH ( SET_RULE ` ~(x IN {w,v0,v1,v2}) ==> ~( x = w ) `) THEN
687 PHA THEN REWRITE_TAC[ MESON[]` unobstructed v0 x s /\ a <=> a /\
688 unobstructed v0 x s `] THEN REWRITE_TAC[ MESON[]` ~(x = w) /\ a <=> a /\ ~(x = w) `]
690 NHANH (SET_RULE ` ~(v0 IN {v1, v2, w, x}) ==> ~( v0 = w )`) THEN
691 NGOAC THEN MATCH_MP_TAC (MESON[] ` (a ==> c) ==> ( a /\ b ==> c ) `) THEN PHA THEN
692 REWRITE_TAC[ unobstructed] THEN
693 REWRITE_TAC[ MESON[] ` ~(v0 = w) /\ centered_pac s v0 /\ aa /\ bb /\ cc /\
694 x IN VC w s /\ ~obstructed v0 x s /\ las <=>
695 aa /\ bb /\ cc /\ las /\ ( centered_pac s v0 /\ ~(v0 = w) /\
696 ~obstructed v0 x s /\ x IN VC w s )`] THEN
697 NHANH (CUTHE4 (prove(` ! s v0 w x . centered_pac s v0 /\ ~(v0 = w) /\ ~obstructed v0 x s /\ x IN VC w s
698 ==> d3 w x < d3 v0 x`, REWRITE_TAC[ VC; lambda_x; IN_ELIM_THM] THEN PURE_ONCE_REWRITE_TAC
699 [ MESON[] `( !s v0 w x. a v0 x s w ==> b v0 x w ) <=> ( ! s v0 w x. ( d3 v0 x < &2 \/
700 ~(d3 v0 x < &2)) /\ a v0 x s w ==> b v0 x w) `] THEN MESON_TAC[centered_pac; trg_d3_sym;
701 REAL_ARITH` ~(d3 v0 x < &2) /\ d3 w x < &2 ==> d3 w x < d3 v0 x`]))) THEN
702 NHANH (CUTHE4 TRIANGLE_IN_BARRIER') THEN
704 ONCE_REWRITE_TAC[MESON[] ` a1 /\ a2 /\ a3 /\ a4 /\
705 ~(conv {x, w} INTER aff_ge {v0} {v1, v2} = {}) /\ aa /\ bb /\ cc /\ dd /\ a5 <=> aa /\
706 bb /\ cc /\ dd /\ ~(conv {x, w} INTER aff_ge {v0} {v1, v2} = {}) /\ a3 /\ a4 /\
707 a5 /\ a1 /\ a2`] THEN ONCE_REWRITE_TAC[ trg_d3_sym] THEN REWRITE_TAC[d3] THEN
708 REWRITE_TAC[MESON[aff_ge_def; cone]` aff_ge {v0} {v1, v2} = cone v0 {v1,v2}`] THEN
709 ONCE_REWRITE_TAC[ MESON[] ` CARD {v0, v1, v2, w, x} = 5 /\ a1 /\ a2 /\ a3 /\ a4 /\ a5 /\ a6 /\ l <=>
710 a1 /\ a2 /\ a3 /\ a4 /\ a5 /\ a6 /\ CARD {v0, v1, v2, w, x} = 5 /\ l`] THEN
711 NHANH (CUTHE5 tarski_UMMNOJN) THEN
712 PHA THEN REWRITE_TAC[ MESON[] ` ( a \/ b ) /\ c <=> c /\ ( a \/ b ) `] THEN
713 REWRITE_TAC[ MESON[] `{v0, v1, v2} IN barrier' v0 s /\ a <=>
714 a /\ {v0, v1, v2} IN barrier' v0 s`] THEN
715 REWRITE_TAC[ barrier'; IN_ELIM_THM] THEN
716 PURE_ONCE_REWRITE_TAC[ MESON[]` (?a b c.
719 {v0, v1, v2} = {a, b, c})
720 <=> P {v0, v1, v2} \/ (? a b c. Q a b c /\ {v0, v1, v2} = {a, b, c})`] THEN PHA THEN
721 ONCE_REWRITE_TAC[ MESON[] ` ~(conv {v0, v1, v2} INTER conv0 {x, w} = {}) /\ aa /\ (b \/ bb) <=>
722 ~(conv {v0, v1, v2} INTER conv0 {x, w} = {}) /\
724 (~(conv {v0, v1, v2} INTER conv0 {x, w} = {}) /\ b \/ bb)`] THEN
725 REWRITE_TAC[ SET_RULE ` conv {v0, v1, v2} INTER conv0 {x, w} =
726 conv0 {x, w} INTER conv {v0, v1, v2}`] THEN
727 NHANH (MESON[ def_obstructed] ` ~(conv0 {x, w} INTER conv {v0, v1, v2} = {}) /\
728 {v0, v1, v2} IN barrier s /\ l ==> obstructed x w s `) THEN
729 PHA THEN REWRITE_TAC[ MESON[] ` {v0, v1, v2, w} SUBSET s /\ a <=> a /\ {v0, v1, v2, w}
731 REWRITE_TAC[ MESON[] ` (!a. a IN {v1, v2, v0} ==> dist (w,a) <= #2.51) /\ a <=>
732 a /\ (!a. a IN {v1, v2, v0} ==> dist (w,a) <= #2.51)`] THEN
733 REWRITE_TAC[ MESON[]` CARD {v0, v1, v2, w, x} = 5 /\ a <=>
734 a /\ CARD {v0, v1, v2, w, x} = 5 `] THEN
736 ONCE_REWRITE_TAC[ MESON[] ` ( a \/ b) /\ a1 /\ a2 /\ {v0, v1, v2, w} SUBSET s <=> ( a \/
737 a2 /\ a1 /\ {v0, v1, v2, w} SUBSET s /\ b) /\ a1 /\ a2 /\ {v0, v1, v2, w} SUBSET s`] THEN
738 NHANH (CUTHE6 NOV7) THEN
739 NHANH (prove(` {v0, v1, v2, w} IN Q_SYS s ==> {v0,v1,v2} IN barrier s `,
740 REWRITE_TAC[ barrier; SET_RULE` {a,b,c} UNION {d} = {a,b,c,d} `; IN_ELIM_THM]
741 THEN MESON_TAC[])) THEN
742 ONCE_REWRITE_TAC[ MESON[] ` ~(conv0 {x, w} INTER conv {v0, v1, v2} = {}) /\ a1
743 /\ ( a \/ b ) /\ l <=> ~(conv0 {x, w} INTER conv {v0, v1, v2} = {}) /\ a1
744 /\ ( a \/ b /\ ~(conv0 {x, w} INTER conv {v0, v1, v2} = {}) ) /\ l`] THEN
745 PHA THEN NHANH (MESON[def_obstructed] ` {v0, v1, v2} IN barrier s /\
746 ~(conv0 {x, w} INTER conv {v0, v1, v2} = {}) ==> obstructed x w s`) THEN
747 REWRITE_TAC[ MESON[]` (a /\ b \/ a /\ c ) <=> a /\ ( b \/ c ) `] THEN
749 REWRITE_TAC[ MESON[] `( obstructed x w s /\ b \/ obstructed x w s
750 /\ c ) <=> obstructed x w s /\ ( b \/ c ) `] THEN PHA THEN
751 REWRITE_TAC[MESON[ OBS_IMP_NOT_IN_VC] ` a1/\a2/\a3 /\ obstructed x w s /\ l
752 ==> ~(x IN VC w s)`]);;
754 let lambda_x = prove(` ! x s. lambda_x x s ={w | w IN s /\ d3 w x < &2 /\ ~obstruct w x s}`,
755 REWRITE_TAC[lambda_x; OBSTRUCT_EQ]);;
757 (* ==== end repare VC === *)
764 let TCQPONA = new_axiom ` ! s v v1 v2 v3.
766 CARD {v, v1, v2, v3} = 4 /\
767 {v, v1, v2, v3} SUBSET s /\
768 d3 v1 v2 <= &2 * t0 /\
769 d3 v2 v3 <= &2 * t0 /\
770 d3 v3 v1 <= &2 * t0 /\
771 ~(conv {v1, v2, v3} INTER voronoi v s = {})
772 ==> (!x. x IN {v1, v2, v3} ==> &2 <= d3 x v /\ d3 x v <= &2 * t0)`;;
776 let CEWWWDQ = new_axiom ` !s v v1 v2 v3.
778 CARD {v, v1, v2, v3} = 4 /\
779 {v, v1, v2, v3} SUBSET s /\
780 d3 v1 v2 <= &2 * t0 /\
781 d3 v2 v3 <= &2 * t0 /\
782 d3 v1 v3 <= sqrt (&8) /\
783 ~(conv {v1, v2, v3} INTER voronoi v s = {})
784 ==> (!x. x IN {v1, v2, v3} ==> &2 <= d3 x v /\ d3 x v <= &2 * t0)`;;
789 let QHSEWMI = new_axiom ` !v1 v2 v3 w1 w2.
790 ~(conv {w1, w2} INTER conv {v1, v2, v3} = {}) /\
791 ~(w1 IN conv {v1,v2,v3})
792 ==> w2 IN cone w1 {v1, v2, v3}`;;
797 (* =================== *)
799 let BAR_TRI = prove(` ! b s. b IN barrier s <=> (? x y z . b = {x,y,z} /\ {x,y,z} IN barrier s)`,
800 REWRITE_TAC[ barrier ; IN_ELIM_THM] THEN MESON_TAC[]);;
806 let NOV20 = prove(` ! v0 x' y z. v0 IN {x', y, z} <=> (?yy zz. {v0, yy, zz} = {x', y, z})`,
808 REWRITE_TAC[EQ_EXPAND] THEN
809 REWRITE_TAC[SET_RULE `((?yy zz. {v0, yy, zz} = {x', y, z})
810 ==> v0 IN {x', y, z})`] THEN
811 REWRITE_TAC[IN_SET3] THEN
812 MESON_TAC[SET_RULE ` x = a
813 ==> {x, b, c} = {a, b, c} /\
814 {x, b, c} = {b, a, c} /\
815 {x, b, c} = {b, c, a}`]);;
819 let X_IN_VOR_X = prove(` ! x:real^A s. x IN voronoi x s `,
820 REWRITE_TAC[voronoi; IN_ELIM_THM; DIST_REFL; DIST_POS_LT] THEN
821 MESON_TAC[DIST_POS_LT]);;
823 let IN_VO2_EQ = prove(` ! s v0 x . x IN voro2 v0 s <=>
824 (!w. s w /\ ~(w = v0) ==> d3 x v0 < d3 x w) /\ d3 x v0 < &2`,
825 REWRITE_TAC[voro2; voronoi; IN_ELIM_THM; d3]);;
827 let IN_VO_EQ = prove(`! x s v0 . x IN voronoi v0 s <=> (!w. s w /\
828 ~(w = v0) ==> dist(x,v0) < dist(x,w))`, REWRITE_TAC[voronoi; IN_ELIM_THM]);;
831 let IN_BAR_DISTINCT = prove(` ! a b c s. {a,b,c} IN barrier s ==>
832 ~( a = b\/ b= c \/ c = a)`,
833 REWRITE_TAC[barrier; IN_ELIM_THM; quasi_tri;set_3elements] THEN
834 KHANANG THEN REWRITE_TAC[EXISTS_OR_THM] THEN NHANH ( MESON[]` (?v1 v2 v3.
835 (a1 /\ a2 v1 v2 v3 /\
836 ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
838 {a, b, c} = {v1, v2, v3}) ==> (?v1 v2 v3.
839 ~(v1 = v2 \/ v2 = v3 \/ v3 = v1) /\
840 {a, b, c} = {v1, v2, v3})`) THEN
841 ONCE_REWRITE_TAC[MESON[EQ_SYM_EQ]` {a,b,c} = {x,y,z} <=> {x,y,z} = {a,b,c}` ] THEN
842 REWRITE_TAC[ set_3elements] THEN MESON_TAC[OCT23]);;
845 let FOUR_POINTS = prove(`!a b c d s.
846 {a, b, c} IN barrier s /\ ~(d IN {a, b, c}) ==> CARD {a, b, c, d} = 4`,
847 NHANH (CUTHE4 IN_BAR_DISTINCT) THEN ONCE_REWRITE_TAC[
848 SET_RULE ` {a,b,c,d} = {d,a,b,c} `] THEN MESON_TAC[CARD4]);;
854 let IN_Q_SYS_IMP4 = prove(`!q s. q IN Q_SYS s ==>
855 (?a b c d. {a, b, c} UNION {d} = q)`,
856 NHANH (SPEC_ALL CASES_OF_Q_SYS) THEN
857 REWRITE_TAC[quasi_reg_tet; strict_qua; quarter; simplex] THEN
858 REWRITE_TAC[SET_RULE` {a,b,c,d} = {a,b,c} UNION {d} `] THEN
862 let SET2_SU_EX = SET_RULE` {(a:A),b} SUBSET s <=> a IN s /\ b IN s `;;
863 let D3_SYM = MESON[trg_d3_sym]` ! x y. d3 x y = d3 y x `;;
866 let EXISTS_DIA = prove(`! q s. quarter q s ==> (? a b. diagonal a b q s)`,
867 REWRITE_TAC[quarter; diagonal] THEN
868 REWRITE_TAC[SET2_SU_EX] THEN
870 NHANH (MESON[REAL_LE_TRANS]`&2 * t0 <= d3 v w /\ a1 /\ (!x y. P x y ==> d3 x y <= &2 * t0)
871 ==> (!x y. P x y ==> d3 x y <= d3 v w)`) THEN
873 REWRITE_TAC[MESON[REAL_ARITH ` a = b ==> a <= b `] ` a ==> b = c:real <=>
874 a ==> ( b = c /\ b <= c )`] THEN
878 let QUARTER_EQ_EX_DIA = prove(`! q s. quarter q s <=> (? a b. diagonal a b q s)`,
879 REWRITE_TAC[EQ_EXPAND; EXISTS_DIA; diagonal] THEN MESON_TAC[]);;
882 let IN_Q_IMP = prove(`!q s.
886 {a, b} SUBSET q INTER q1 /\ quarter q s /\ diagonal a b q1 s /\ q1 IN Q_SYS s)`,
887 REWRITE_TAC[MESON[CASES_OF_Q_SYS]` (q IN Q_SYS s ==> a ) <=> q IN Q_SYS s
888 /\ (quasi_reg_tet q s \/ strict_qua q s) ==> a `] THEN
890 REWRITE_TAC[MESON[]` a \/ b ==> c <=> (a ==> c) /\ ( b==> c) `] THEN
892 REWRITE_TAC[strict_qua] THEN
893 NHANH (SPEC_ALL EXISTS_DIA) THEN
894 NHANH (MESON[diagonal]` diagonal d1 d2 q s ==> {d1, d2} SUBSET q `) THEN
895 REWRITE_TAC[SUBSET_INTER] THEN
898 let NOV21 = prove(` ! q s. quasi_reg_tet q s ==> q IN Q_SYS s`,
899 REWRITE_TAC[Q_SYS; IN_ELIM_THM] THEN REWRITE_TAC[ MESON[]` a ==> a \/ b `]);;
902 let NOVE21 = prove(` ! q s. quasi_reg_tet q s \/
904 {a, b} SUBSET q1 INTER q /\ quarter q s /\ diagonal a b q1 s /\ q1 IN Q_SYS s)
906 MP_TAC NOV21 THEN REWRITE_TAC[OR_IMP_EX] THEN SIMP_TAC[] THEN
907 MP_TAC lemma7_7_CXRHOVG THEN MESON_TAC[]);;
910 let COND_Q_SYS =prove(`!q s.
911 q IN Q_SYS s <=> quasi_reg_tet q s \/
912 (?a b q1. {a, b} SUBSET q INTER q1 /\ quarter q s /\
913 diagonal a b q1 s /\ q1 IN Q_SYS s)`, REWRITE_TAC[EQ_EXPAND] THEN
914 REWRITE_TAC[IN_Q_IMP] THEN MESON_TAC[INTER_COMM; NOVE21]);;
918 let SET4_SUB_EX = SET_RULE ` {a,b,c,d} SUBSET s <=>
919 a IN s /\ b IN s /\ c IN s /\ (d:A) IN s `;;
923 let IMP_QUA_RE_TE = prove(`!s v0 x y z. v0 IN s /\ packing s /\
924 {x, y, z} SUBSET s /\
925 (!aa bb. aa IN {y, z, x} /\ bb IN {y, z, x} ==> dist (aa,bb) <= #2.51) /\
926 ~(voronoi v0 s INTER conv {x, y, z} = {}) /\
927 CARD {x, y, z, v0} = 4 ==> quasi_reg_tet {v0,x,y,z} s `,
928 NHANH (SET_RULE ` (! aa bb. aa IN {y, z, x} /\ bb IN {y, z, x} ==> P aa bb )
929 ==> P x y /\ P y z /\ P z x `) THEN
930 ONCE_REWRITE_TAC[ SET_RULE `{a,b,c,d} = {d,a,b,c}`] THEN
931 REWRITE_TAC[ SET_RULE ` v0 IN s /\ packing s /\
932 {x, y, z} SUBSET s /\ l <=> packing s /\ {v0,x,y,z} SUBSET s /\ l `] THEN
933 REWRITE_TAC[ MESON[]` a /\ b/\ ( c1 /\ c2 ) /\ d /\ e <=> c1 /\ a /\ e
934 /\ b /\ c2 /\d `] THEN
935 ONCE_REWRITE_TAC[INTER_COMM] THEN
936 REWRITE_TAC[ GSYM db_t0; GSYM d3] THEN PHA THEN
937 NHANH (SPEC_ALL TCQPONA) THEN
938 REWRITE_TAC[quasi_reg_tet; def_simplex; CARD4;IN_SET3; IN_SET4;
939 DE_MORGAN_THM; SET4_SUB_EX; db_t0] THEN
940 SIMP_TAC[] THEN PHA THEN DAO THEN
941 REWRITE_TAC[ MESON[D3_SYM]` (!x'. x' = x \/ x' = y \/ x' = z ==>
942 d3 x' v0 <= #2.51 /\ &2 <= d3 x' v0) /\ a1 /\
946 l ==> (!v w. ~(v = w) /\
947 (v = z \/ v = v0 \/ v = x \/ v = y) /\
948 (w = z \/ w = v0 \/ w = x \/ w = y)
949 ==> d3 v w <= #2.51)`]);;
953 let SET3_U_SET1 = SET_RULE ` {a,b,c} UNION {d} = {a,b,c,d} `;;
956 let IN_BA_IM_PA_SU = prove(`! s x y z. {x, y, z} IN barrier s ==>
957 packing s /\ {x, y, z} SUBSET s`,
958 REWRITE_TAC[barrier; IN_ELIM_THM] THEN
959 NHANH (SPEC_ALL CASES_OF_Q_SYS) THEN REPEAT GEN_TAC THEN
960 REWRITE_TAC[quasi_tri] THEN KHANANG THEN
961 REWRITE_TAC[MESON[]` (?a b c. P a b c \/ Q a b c) ==> l <=>
962 ((?a b c . P a b c ) ==> l) /\ ((?a b c. Q a b c) ==> l)`] THEN
963 REWRITE_TAC[MESON[]` (?v1 v2 v3. (packing s /\
964 {v1, v2, v3} SUBSET s /\P v1 v2 v3 ) /\
965 {x, y, z} = {v1, v2, v3}) ==> packing s /\ {x, y, z} SUBSET s`] THEN
966 REWRITE_TAC[quasi_reg_tet; strict_qua; quarter; SET3_U_SET1; def_simplex] THEN
967 REWRITE_TAC[SET_RULE ` {a,b,c,d} SUBSET s <=> {a,b,c} SUBSET s /\ d IN s `] THEN
971 let FIRST_NOV22 = prove(` ! s v0 x y z. {x, y, z} IN barrier s /\
973 ~(xx = yy) /\ {xx, yy} SUBSET {y, z, x}
974 ==> &2 <= dist (xx,yy) /\ dist (xx,yy) <= sqrt (&8)) /\
975 (!aa bb. aa IN {y, z, x} /\ bb IN {y, z, x} ==> dist (aa,bb) <= #2.51) /\
977 ~(voronoi v0 s INTER conv {x, y, z} = {}) /\
978 CARD {x, y, z, v0} = 4
979 ==> {v0, x, y, z} IN Q_SYS s`,
980 NHANH (SPEC_ALL IN_BA_IM_PA_SU ) THEN
982 ONCE_REWRITE_TAC[MESON[]` a1 /\ a2 /\ a3 /\ a4 /\ a5 /\ a6 /\ a7 /\ a8 <=>
983 a1 /\ a4 /\ a6 /\ a2 /\ a3 /\ a5 /\ a7 /\ a8 `] THEN
984 NHANH (SPEC_ALL IMP_QUA_RE_TE) THEN
985 MESON_TAC[COND_Q_SYS]);;
989 let QUA_TRI_EDGE = prove(` ! q s. quasi_tri q s ==>
990 (! a b. a IN q /\ b IN q ==> d3 a b <= &2 * t0 )`,REWRITE_TAC[quasi_tri; db_t0]
991 THEN MP_TAC D3_REFL THEN MP_TAC (REAL_ARITH ` &0 <= #2.51 `) THEN MESON_TAC[]);;
994 let BAR_WI_LONG_ED = prove(`!bar s.
995 bar IN barrier s /\ (?a b. #2.51 < d3 a b /\ a IN bar /\ b IN bar)
996 ==> (?w. w INSERT bar IN Q_SYS s /\ strict_qua (w INSERT bar) s)`,
997 REWRITE_TAC[barrier; IN_ELIM_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THENL
998 [REPEAT (FIRST_X_ASSUM MP_TAC);REPEAT (FIRST_X_ASSUM MP_TAC)]
999 THENL [NHANH (SPEC_ALL QUA_TRI_EDGE);
1000 ABBREV_TAC ` an w s = (w:real^3 INSERT (bar:real^3 -> bool) IN Q_SYS s)`] THENL
1001 [REWRITE_TAC[ GSYM db_t0]; NHANH (SPEC_ALL CASES_OF_Q_SYS)] THENL
1002 [MESON_TAC[REAL_ARITH ` a <= b <=> ~( b < a )`];
1003 NHANH (MESON[QUA_TET_IMPLY_QUA_TRI]`quasi_reg_tet ({v0, v1, v2} UNION {v4}) s ==>
1004 quasi_tri {v0, v1, v2} s`)] THEN NHANH (SPEC_ALL QUA_TRI_EDGE) THEN
1005 STRIP_TAC THENL [ASM_MESON_TAC[db_t0; REAL_ARITH` a <= b <=> ~( b < a ) `];
1006 ASM_MESON_TAC[SET_RULE ` s UNION {a} = a INSERT s `]]);;
1010 let PER_SET3 = SET_RULE ` {a,b,c} = {a,c,b} /\ {a,b,c} = {b,a,c} /\
1011 {a,b,c} = {c,a,b} /\ {a,b,c} = {b,c,a} /\ {a,b,c} = {c,b,a} `;;
1013 let EXI_THIRD_PO =prove( ` ! a b c x y: A. {x,y} SUBSET {a,b,c} /\ ~(x=y)
1014 ==> (? z. {x,y,z} = {a,b,c} ) `, REPEAT GEN_TAC THEN
1015 REWRITE_TAC[SET2_SU_EX] THEN REWRITE_TAC[SET2_SU_EX; IN_SET3] THEN
1016 KHANANG THEN REWRITE_TAC[MESON[]`x = a /\ y = a /\ ~(x = y) <=> F`] THEN
1017 MESON_TAC[ PER_SET3]);;
1022 let IMP_QUA = prove(` ! a b c s v0. packing s /\
1023 CARD {v0, a, b, c} = 4 /\
1024 {v0, a, b, c} SUBSET s /\
1025 d3 a b <= &2 * t0 /\
1026 d3 b c <= &2 * t0 /\ &2 * t0 <= d3 a c /\
1027 d3 a c <= sqrt (&8) /\
1028 (!x. x IN {a, b, c} ==> &2 <= d3 x v0 /\ d3 x v0 <= &2 * t0)
1029 ==> quarter {v0, a, b, c} s `,
1030 REWRITE_TAC[quarter; def_simplex; CARD4; IN_SET3; DE_MORGAN_THM] THEN
1031 SIMP_TAC[] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
1032 EXISTS_TAC `a:real^3` THEN EXISTS_TAC `c:real^3` THEN
1033 ASM_SIMP_TAC[FOUR_IN] THEN REWRITE_TAC[IN_SET4; PAIR_EQ_EXPAND] THEN
1034 MP_TAC (MESON[REAL_ARITH ` &0 <= #2.51`; db_t0]` &0 <= &2*t0 `) THEN
1035 ASM_MESON_TAC[D3_SYM; D3_REFL]);;
1038 let QUA_RE_TE_EDGE = prove(`! a b q s. quasi_reg_tet q s /\ a IN q /\ b IN q
1039 ==> d3 a b <= &2 * t0 `, REWRITE_TAC[quasi_reg_tet] THEN MP_TAC D3_REFL THEN
1040 REWRITE_TAC[db_t0] THEN MESON_TAC[REAL_ARITH `&0 <= #2.51 `]);;
1045 let CONSI_OF_LE77 = prove(`!s v0 v4 w x y z.
1046 quarter ({x, y, z} UNION {v0}) s /\
1049 {x, y, z} UNION {v4} IN Q_SYS s /\
1050 diagonal aa bb ({x, y, z} UNION {v4}) s
1051 ==> {x, y, z} UNION {v0} IN Q_SYS s`,
1052 REWRITE_TAC[MESON[]` quarter q s /\ a <=>a/\quarter q s `] THEN
1053 PHA THEN NHANH (SET_RULE ` aa IN {x, y, z} /\ bb IN {x, y, z} /\ l
1056 ({x, y, z} UNION {v4}) INTER ({x, y, z} UNION {v0}))`) THEN
1057 PHA THEN NHANH (MESON[]` diagonal aa bb ({x, y, z} UNION {v4}) s /\
1058 quarter ({x, y, z} UNION {v0}) s /\
1059 (!v0 v4. P v0 v4) ==> P v0 v4 `) THEN MESON_TAC[lemma7_7_CXRHOVG]);;
1069 let IMP_IN_Q_SYS = prove( ` ! s v0 x y z . {x, y, z} IN barrier s /\ v0 IN s /\
1070 ~(voronoi v0 s INTER conv {x, y, z} = {}) /\
1071 CARD {x, y, z, v0} = 4
1072 ==> {v0, x, y, z} IN Q_SYS s`,
1073 NHANH (CUTHE4 TRIANGLE_IN_BARRIER) THEN
1075 REWRITE_TAC[OR_IMP_EX] THEN
1076 REWRITE_TAC[FIRST_NOV22] THEN
1078 MATCH_MP_TAC (MESON[]`(a /\ c ==> d ) ==> a /\ b /\ c ==> d `) THEN
1079 NHANH (SPEC_ALL IN_BA_IM_PA_SU) THEN
1080 REWRITE_TAC[MESON[]` a /\ b /\ c ==> d <=> b ==> a /\ c ==> d`] THEN
1081 NHANH (MESON[DIST_NZ; REAL_ARITH ` &0 < #2.51 /\ ( a < b /\ b < c ==> a < c )`]`
1082 #2.51 < dist (aa,bb) ==> ~( aa = bb ) `) THEN
1083 REWRITE_TAC[ MESON[]` a /\ ( b /\ c ) /\ l <=> (a /\ c ) /\ b /\ l`] THEN
1084 NHANH (SPEC_ALL EXI_THIRD_PO) THEN
1085 REWRITE_TAC[MESON[]` a/\ b/\ c/\ d <=> c /\ a/\b/\d`] THEN
1086 STRIP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN
1087 ONCE_REWRITE_TAC[ EQ_SYM_EQ] THEN
1088 REWRITE_TAC[MESON[]` a = b ==> P a <=> a = b ==> P b `] THEN
1089 ONCE_REWRITE_TAC[ EQ_SYM_EQ] THEN
1090 ONCE_REWRITE_TAC[ SET_RULE ` {x, y, z, v0} = {v0,y,z,x} `] THEN
1091 REWRITE_TAC[CARD4; GSYM CARD3] THEN
1092 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
1093 REWRITE_TAC[MESON[]` a = b ==> P a <=> a = b ==> P b `] THEN
1094 REWRITE_TAC[IMP_IMP] THEN PHA THEN
1095 REWRITE_TAC[MESON[]` (! a b. P a b ) /\l <=> l/\(!a b. P a b)`] THEN
1097 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
1098 REWRITE_TAC[CARD3] THEN
1099 NHANH (SET_RULE ` ~(aa = bb \/ bb = z' \/ z' = aa) /\
1101 ~({x', y'} = {aa, bb}) /\ {x', y'} SUBSET {aa, bb, z'}
1103 P bb z' /\ P z' aa `) THEN
1105 REWRITE_TAC[MESON[CARD4]` ~(v0 IN {aa, bb, z'}) /\
1106 ~(aa = bb \/ bb = z' \/ z' = aa) /\ l <=> CARD {v0,aa,bb,z'} = 4 /\ l `] THEN
1107 ONCE_REWRITE_TAC[ SET_RULE ` {v0, aa, bb, z'} = {v0,bb,z',aa}`] THEN
1108 SIMP_TAC[SET_RULE ` {y,z,x} = {x,y,z} `] THEN
1109 REWRITE_TAC[ GSYM d3; GSYM db_t0] THEN
1110 REWRITE_TAC[ GSYM d3; GSYM db_t0; SET2_SU_EX] THEN
1111 REWRITE_TAC[MESON[]` (aa IN {x, y, z} /\ bb IN {x, y, z}) /\a1 /\a2 /\
1112 &2 * t0 < d3 aa bb /\a3 /\ a4 /\ a5 /\ l <=> (aa IN {x, y, z} /\ bb IN {x, y, z}
1113 /\ a5 /\ &2 * t0 < d3 aa bb) /\ a1 /\ a2 /\ a3 /\ a4 /\ l `] THEN
1114 NHANH (SPEC_ALL DIAGONAL_BARRIER) THEN
1115 NHANH (SPEC_ALL DIA_OF_QUARTER) THEN
1116 REWRITE_TAC[ GSYM LEFT_AND_EXISTS_THM] THEN
1118 REWRITE_TAC[MESON[]` d3 aa bb <= sqrt (&8) /\ l <=>l/\d3 aa bb <= sqrt (&8)`] THEN
1119 REWRITE_TAC[MESON[]` a = b /\ P b <=> a = b /\ P a`] THEN
1120 PHA THEN REWRITE_TAC[MESON[]` ~ ( a INTER b = {}) /\ l <=> l/\ ~ ( a INTER b = {})`]
1122 REWRITE_TAC[SET_RULE` v0 IN s /\
1124 {aa, bb, z'} SUBSET s /\
1125 CARD {v0, aa, bb, z'} = 4 /\
1128 l /\ a1 /\ CARD {v0, aa, bb, z'} = 4 /\ {v0, bb, z', aa} SUBSET s /\ las`] THEN
1129 ONCE_REWRITE_TAC[MESON[SET_RULE ` {v0, aa, bb, z'} = {v0,bb,z',aa}`]` CARD {v0, aa, bb, z'} =4
1130 <=> CARD {v0,bb,z',aa} = 4 `] THEN
1131 ONCE_REWRITE_TAC[INTER_COMM] THEN
1132 ONCE_REWRITE_TAC[MESON[SET_RULE ` {a,b,c} = {b,c,a}`]`
1133 conv {a,b,c} = conv {b,c,a} `] THEN
1134 ONCE_REWRITE_TAC[MESON[D3_SYM]` d3 aa bb <= sqrt (&8) <=> d3 bb aa <= sqrt (&8)`] THEN
1135 NHANH (SPEC_ALL CEWWWDQ) THEN
1136 NHANH (REAL_ARITH ` a < b ==> a <= b `) THEN
1137 ONCE_REWRITE_TAC[MESON[]` ( a/\ b ) /\ c <=> c /\ b /\ a `] THEN
1139 NHANH (MESON[IMP_QUA; D3_SYM]` packing s /\
1140 CARD {v0, bb, z', aa} = 4 /\
1141 {v0, bb, z', aa} SUBSET s /\
1142 d3 bb z' <= &2 * t0 /\
1143 d3 z' aa <= &2 * t0 /\
1144 d3 bb aa <= sqrt (&8) /\ a2 /\
1145 (!x. x IN {bb, z', aa} ==> &2 <= d3 x v0 /\ d3 x v0 <= &2 * t0) /\
1146 &2 * t0 <= d3 aa bb /\ a1 ==> quarter {v0, bb, z', aa} s`) THEN
1147 REWRITE_TAC[MESON[]`( ? a. P a ) /\ l <=> l /\ (?a. P a) `] THEN
1148 REWRITE_TAC[barrier; IN_ELIM_THM] THEN
1149 REWRITE_TAC[MESON[]` P b /\ a = b <=> a = b /\ P a `] THEN
1150 REWRITE_TAC[GSYM LEFT_AND_EXISTS_THM] THEN
1152 REWRITE_TAC[MESON[]`( a < b /\ l <=> l /\ a < b ) /\
1153 ( ( x \/ y ) /\ z <=> z /\ ( x \/ y ))`] THEN
1154 REWRITE_TAC[ MESON[]` a IN s /\ b /\ c <=> c /\ a IN s /\ b `] THEN
1155 NHANH (SPEC_ALL QUA_TRI_EDGE) THEN
1157 REWRITE_TAC[MESON[real_lt]`&2 * t0 < d3 aa bb /\
1158 (a1 /\ (!a b. a IN s /\ b IN s ==> d3 a b <= &2 * t0) \/ a2) /\
1161 &2 * t0 < d3 aa bb /\ a2 /\ aa IN s /\ bb IN s`] THEN
1162 NHANH (SPEC_ALL CASES_OF_Q_SYS) THEN
1163 REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
1165 NHANH (MESON[SET_RULE ` a IN s ==> a IN ( s UNION t )`; QUA_RE_TE_EDGE]`
1166 quasi_reg_tet ({x, y, z} UNION {v4}) s /\
1168 bb IN {x, y, z} ==> d3 aa bb <= &2 * t0 `) THEN
1170 REWRITE_TAC [REAL_ARITH ` a <= b <=> ~( b < a ) `] THEN
1171 REWRITE_TAC[MESON[]`(?v4. ~(&2 * t0 < d3 aa bb) /\ P v4 \/ Q v4) /\ a1 /\ &2 * t0 < d3 aa bb <=>
1172 (?v4. Q v4) /\ a1 /\ &2 * t0 < d3 aa bb`] THEN
1173 REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
1175 NHANH (MESON[SET_RULE` a IN s ==> a IN ( s UNION t ) `; DIAGONAL_STRICT_QUA]`
1177 aa IN {x, y, z} /\ a1 /\
1178 strict_qua ({x, y, z} UNION {v4}) s /\
1180 &2 * t0 < d3 aa bb /\ l ==> diagonal aa bb ({x, y, z} UNION {v4}) s `) THEN
1181 NHANH (MESON[strict_qua]` strict_qua q s /\ l ==> quarter q s `) THEN
1183 REWRITE_TAC[SET_RULE ` {v0, bb, z', aa} = {aa,bb,z'} UNION {v0}`] THEN
1185 REWRITE_TAC[MESON[]` a = b /\ l <=> l/\ a= b `] THEN
1186 REWRITE_TAC[MESON[]` quarter q s /\
1187 &2 * t0 < d3 aa bb /\l <=> &2 * t0 < d3 aa bb /\l /\ quarter q s`] THEN
1189 REWRITE_TAC[MESON[]` quarter ({aa, bb, z'} UNION {v0}) s /\
1191 {aa, bb, z'} = {x, y, z} /\ l <=> l /\ a1 /\ {aa, bb, z'} = {x, y, z}
1192 /\ quarter ({x, y, z} UNION {v0}) s`] THEN
1193 REWRITE_TAC[MESON[]` a IN Q_SYS s /\ l <=> l /\ a IN Q_SYS s`] THEN
1194 REWRITE_TAC[MESON[]` a IN s /\ b /\ l <=>l /\ a IN s /\b `] THEN
1195 REWRITE_TAC[ MESON[]` diagonal aa bb ({x, y, z} UNION {v4}) s /\ l <=>
1196 l /\ diagonal aa bb ({x, y, z} UNION {v4}) s`] THEN
1198 NHANH (MESON[CONSI_OF_LE77]` quarter ({x, y, z} UNION {v0}) s /\
1201 {x, y, z} UNION {v4} IN Q_SYS s /\a1/\
1202 diagonal aa bb ({x, y, z} UNION {v4}) s
1203 ==> {x, y, z} UNION {v0} IN Q_SYS s`) THEN
1205 REWRITE_TAC[GSYM RIGHT_AND_EXISTS_THM] THEN
1206 REWRITE_TAC[MESON[SET_RULE ` {x, y, z} UNION {v0} = {y, v0, x} UNION {z} `;CASES_OF_Q_SYS]`
1207 {x, y, z} UNION {v0} IN Q_SYS s /\ last
1208 ==> {y, v0, x} UNION {z} IN Q_SYS s /\
1209 quasi_reg_tet ({y, v0, x} UNION {z}) s \/
1210 {y, v0, x} UNION {z} IN Q_SYS s /\
1211 strict_qua ({y, v0, x} UNION {z}) s`]);;
1216 let POS_EQ_INV_POS = prove(`!x. &0 < x <=> &0 < &1 / x`, GEN_TAC THEN EQ_TAC
1217 THENL [REWRITE_TAC[MESON[REAL_LT_RDIV_0; REAL_ARITH ` &0 < &1 `]`! b. &0 < b
1218 ==> &0 < &1 / b `];REWRITE_TAC[] THEN
1219 MESON_TAC[MESON[REAL_LT_RDIV_0; REAL_ARITH ` &0 < &1 `]` &0 < b
1220 ==> &0 < &1 / b `; REAL_FIELD ` &1 / ( &1 / x ) = x ` ]]);;
1223 let STRIP_TR = REPEAT STRIP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC)
1224 THEN REWRITE_TAC[IMP_IMP] THEN PHA;;
1226 let INTER_DIF_EM_EX = SET_RULE `! a b. ~(a INTER b = {}) <=> (? x. x IN a /\ x IN b ) `;;
1231 let AFF_LE_CONE =prove(` ! a b x y z. ~( conv0 {a,b} INTER conv {x,y,z} = {})
1232 ==> ( b IN aff_le {x,y,z} {a}) /\ ( b IN cone a {x,y,z}) `,
1233 REWRITE_TAC[CONV_SET3; CONV0_SET2; INTER_DIF_EM_EX; IN_ELIM_THM] THEN
1234 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT (FIRST_X_ASSUM MP_TAC) THEN
1235 REWRITE_TAC[IMP_IMP] THEN PHA THEN REWRITE_TAC[MESON[]` x' = aa /\a1
1236 /\a2 /\a3/\a4 /\ x' = bb <=> x' = aa /\a1 /\a2 /\a3/\a4 /\ aa = bb `]
1237 THEN REWRITE_TAC[ VECTOR_ARITH ` a + b:real^N = c <=> b = c - a`] THEN
1238 NHANH (MESON[VECTOR_MUL_LCANCEL]` b' % b = a ==> (&1 / b') % (b' % b)
1239 = (&1 / b') % a `) THEN REWRITE_TAC[VECTOR_MUL_ASSOC;
1240 VECTOR_SUB_LDISTRIB; VECTOR_ADD_LDISTRIB; simp_def] THEN
1241 NHANH (MESON[POS_EQ_INV_POS]` &0 < a ==> &0 < &1 / a `) THEN
1242 REWRITE_TAC[VECTOR_ARITH ` a - b % x = a + ( -- b ) % x `] THEN
1243 MP_TAC (REAL_FIELD `! b. &0 < b ==> &1 / b * b = &1 `) THEN
1244 REWRITE_TAC[IMP_IMP] THEN PHA THEN REWRITE_TAC[REAL_ARITH ` a / b * c
1245 = (a * c) / b`; REAL_MUL_LID; VECTOR_ARITH ` a - b % x = a + (--b) % x `] THEN
1246 REWRITE_TAC[REAL_ARITH ` -- ( a / b ) = ( -- a ) / b `] THEN
1247 NHANH (MESON[REAL_ARITH ` a / m + b / m + c / m + d / m = ( a + b + c + d ) / m `]`
1248 b' / b' % b = (a'' / b' % x + b'' / b' % y + c / b' % z) + --a' / b' % a
1249 ==> a'' / b' + b'' / b' + c / b' + -- a' / b' = ( a'' + b'' + c + -- a' ) / b' `)
1250 THEN NHANH (MESON[REAL_ARITH ` a' + b' = &1 /\ a'' + b'' + c = &1
1251 ==> a'' + b'' + c + --a' = b' `]` a' + b' = &1 /\a1 /\a2 /\a3 /\a4 /\
1252 a'' + b'' + c = &1 /\ l ==> a'' + b'' + c + --a' = b'`) THEN
1253 MP_TAC (REAL_ARITH ` ! a. a < &0 ==> a <= &0 `) THEN REWRITE_TAC[ IN_ELIM_THM]
1254 THEN NHANH (MESON[]`(!b. &0 < b ==> b / b = &1) /\ --a' / b' < &0 /\
1255 &0 < a' /\ &0 < &1 / a' /\ &0 < b' /\ l ==> b' / b' = &1 `) THEN
1256 REWRITE_TAC[MESON[] ` a /\ b' / b' = &1 ==> l <=> b' / b' = &1 ==> a ==> l`] THEN
1257 SIMP_TAC[VECTOR_MUL_LID] THEN PHA THEN NHANH (MESON[REAL_LT_DIV]
1258 ` &0 < a' /\ &0 < &1 / a' /\ &0 < b' /\ l ==> &0 < a' / b' `) THEN
1259 REWRITE_TAC[REAL_ARITH ` &0 < a' / b' <=> --a' / b' < &0 `] THEN
1260 REWRITE_TAC[ MESON[]` a = x / y /\ x = y <=> a = y/ y /\ x = y `] THEN
1261 REWRITE_TAC[ VECTOR_ARITH ` ((a:real^N) + b ) + c = a + b + c `] THEN
1262 STRIP_TR THENL [MESON_TAC[VECTOR_MUL_LID];
1263 REWRITE_TAC[cone; GSYM aff_ge_def; simp_def; IN_ELIM_THM]] THEN
1264 MP_TAC VECTOR_MUL_LID THEN SIMP_TAC[VECTOR_ARITH ` a + b + c + (d:real^N)
1265 = b + c + d + a `] THEN REWRITE_TAC[MESON[]` &0 <= a /\ l <=> l /\ &0 <= a `]
1266 THEN SIMP_TAC[ REAL_ARITH ` a + b + c + d = b + c + d + a `] THEN
1267 REWRITE_TAC[ MESON[]` &0 < a /\ l <=> l /\ &0 < a `] THEN PHA THEN
1268 NHANH (MESON[REAL_ARITH ` &0 < b ==> &0 <= b `; REAL_LE_DIV]` &0 <= c /\
1269 &0 <= b'' /\ &0 <= a'' /\ &0 < b' /\ &0 < a' ==>
1270 &0 <= a'' / b' /\ &0 <= b''/ b' /\ &0 <= c/ b' `) THEN
1271 NHANH (MESON[REAL_FIELD ` &0 < b' ==> b' / b' = &1 `]`(&0 <= c /\ &0
1272 <= b'' /\ &0 <= a'' /\ &0 < b' /\ &0 < a') ==> b' / b' = &1 `) THEN
1273 REWRITE_TAC[ MESON[]` a / a = &1 /\ l <=> l /\ a / a = &1 `] THEN DAO THEN
1274 REWRITE_TAC[IMP_IMP] THEN REWRITE_TAC[ MESON[]`b' / b' = &1 /\ &0 < a' /\
1275 &0 < b' /\ l <=> &0 < a' /\ l /\ &0 < b' /\ b' / b' = &1 `] THEN
1276 REWRITE_TAC[ MESON[]` a = (b:real^N) /\ l <=> l /\ b = a `] THEN
1277 PHA THEN REWRITE_TAC[ MESON[]` aaa = b' / b' % b /\ &0 < b' /\
1278 b' / b' = &1 <=> &0 < b' /\ b' / b' = &1 /\ aaa = &1 % b `]
1279 THEN REWRITE_TAC[ VECTOR_MUL_LID] THEN MESON_TAC[]);;
1282 let NOVE30 = prove(`! P l. ( ! x y z i j k s. ( P x y z i j k s <=> P y x z j i k s)
1283 /\ ( l x y z <=> l y x z ) ) /\ (! x y z i j k s. i <= j /\ P x y z i j k s ==>
1284 l x y z ) ==> (! x y z i j k s. P x y z i j k s ==> l x y z ) `,
1285 ONCE_REWRITE_TAC[ MESON[]` a ==> (!x y z i j k s. P x y z i j k s ==> l x y z) <=>
1286 (a ==> (!x y z i j k s. i <= j /\ P x y z i j k s ==> l x y z)) /\(a ==>
1287 (!x y z i j k s. ~(i <= j) /\ P x y z i j k s ==> l x y z)) `] THEN REPEAT
1289 CONJ_TAC THENL [MESON_TAC[]; MESON_TAC[REAL_ARITH ` ~( a <= b ) ==> b <= a `]]);;
1293 let NOVE31 = prove(`! P l. ( ! x y z i j k s. ( P x y z i j k s <=> P z y x k j i s )
1294 /\ ( l x y z <=> l z y x ) ) /\ (! x y z i j k s. i <= j /\ i <= k /\ P x y z i j k s
1295 ==> l x y z ) ==> (! x y z i j k s. i <= j /\ P x y z i j k s ==> l x y z ) `,
1296 ONCE_REWRITE_TAC[ MESON[]` a ==> (!x y z i j k s. P x y z i j k s ==> l x y z) <=>
1297 (a ==> (!x y z i j k s. i <= k /\ P x y z i j k s ==> l x y z)) /\(a ==>
1298 (!x y z i j k s. ~(i <= k) /\ P x y z i j k s ==> l x y z)) `] THEN REPEAT
1299 GEN_TAC THEN CONJ_TAC THENL [MESON_TAC[]; MESON_TAC[REAL_LE_TRANS;
1300 REAL_ARITH ` ~( a <= b ) ==> b <= a `]]);;
1305 let IMP_IN_BA = prove(`! x y z a s. {x,y,z} UNION {a} IN Q_SYS s ==> {x,y,z} IN barrier s `,
1306 REWRITE_TAC[barrier; IN_ELIM_THM] THEN MESON_TAC[]);;
1310 let IMP_IN_AFF4 = prove(` ! s v0 xx x y z. xx IN cone v0 {x, y, z} /\
1311 ~(xx IN UNIONS {aff_ge {v0} {v1, v2} | v1,v2 | barrier s {v0, v1, v2}}) /\
1312 {v0, x, y, z} IN Q_SYS s ==> xx IN aff_gt {v0} {x, y, z}`,
1313 REWRITE_TAC[cone; GSYM aff_ge_def; simp_def; IN_ELIM_THM] THEN
1314 REPLICATE_TAC 3 GEN_TAC THEN REWRITE_TAC[MESON[]` ( ! x y z. (? s i j k.
1315 P s i j k x y z ) /\ Q x y z ==> l x y z) <=> ( ! x y z i j k s.
1316 P s i j k x y z /\ Q x y z ==> l x y z ) `] THEN MATCH_MP_TAC NOVE30 THEN
1317 CONJ_TAC THENL [MESON_TAC[PER_SET3; REAL_ARITH ` a + b + c = b + a + c ` ;
1318 VECTOR_ARITH `(a:real^N ) + b + c = b + a + c `]; MATCH_MP_TAC NOVE31 THEN
1319 CONJ_TAC]THENL [MESON_TAC[PER_SET3; REAL_ARITH ` a + b + c = c + b + a ` ;
1320 VECTOR_ARITH `(a:real^N ) + b + c = c + b + a `]; PHA] THEN
1321 REWRITE_TAC[MESON[REAL_ARITH ` &0 <= i <=> i = &0 \/ &0 < i `]`
1322 &0 <= i /\ &0 <= j /\ &0 <= k /\ l <=> ( i = &0 \/ &0 < i ) /\ &0 <= j /\
1323 &0 <= k /\ l `] THEN KHANANG THEN REPEAT GEN_TAC THEN
1324 STRIP_TAC THENL [REPEAT (FIRST_X_ASSUM MP_TAC) THEN REPLICATE_TAC 3 DISCH_TAC
1325 THEN REWRITE_TAC[IMP_IMP] THEN ASM_SIMP_TAC[] THEN REWRITE_TAC[VECTOR_MUL_LZERO;
1326 VECTOR_ADD_LID; REAL_ADD_LID] THEN REWRITE_TAC[SET_RULE ` {v0, x, y, z} = {v0,y,z}
1327 UNION {x} `] THEN NHANH (SPEC_ALL IMP_IN_BA) THEN REWRITE_TAC[IN_UNIONS;
1328 IN_ELIM_THM] THEN REWRITE_TAC[MESON[IN]` barrier s a /\ l <=> a IN barrier s /\
1329 l`] THEN PHA THEN REWRITE_TAC[MESON[]` (? t. (? v1 v2 . P v1 v2 /\ t = Q v1 v2 )
1330 /\ xx IN t ) <=> (? v1 v2. P v1 v2 /\ xx IN Q v1 v2 ) `] THEN REWRITE_TAC[IN_ELIM_THM]
1331 THEN MESON_TAC[]; STRIP_TR THEN REWRITE_TAC[MESON[REAL_ARITH ` i <= j /\ &0 < i
1332 ==> &0 < j `]` i <= j /\ i <= k /\ &0 < i /\l <=> i <= j /\ i <= k /\ &0 < j /\
1333 &0 < k /\ &0 < i /\ l`] THEN MESON_TAC[]]);;
1339 let VORO2_EX =prove(`! v0 s. voro2 v0 s = {x | (!w. s w /\ ~(w = v0) ==>
1340 d3 x v0 < d3 x w) /\ d3 x v0 < &2} `, REWRITE_TAC[voro2; voronoi; d3 ]
1345 let LEMMA81 = prove(`!(X:real^3 -> bool) Z s v0:real^3 .
1346 centered_pac s v0 /\
1347 Z = UNIONS {aff_ge {v0} {v1, v2} | v1,v2 | {v0, v1, v2} IN barrier s} /\
1349 {aff_gt {v0} {v1, v2, v3} INTER
1350 aff_le {v1, v2, v3} {v0} INTER
1351 voro2 v0 s | v1,v2,v3 | {v0, v1, v2, v3} IN Q_SYS s}
1352 ==> voro2 v0 s SUBSET X UNION Z UNION VC v0 s`,
1353 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[SET_RULE ` as SUBSET a UNION b UNION c <=>
1354 ( as DIFF (b UNION c)) SUBSET a`] THEN REWRITE_TAC[SUBSET; IN_DIFF; IN_UNION;
1355 VC; lambda_x; IN_ELIM_THM; voro2;voronoi; GSYM d3; DE_MORGAN_THM; centered_pac]
1356 THEN ABBREV_TAC ` ketluan x = ((x:real^3) IN (X:real^3 -> bool))` THEN SIMP_TAC[]
1357 THEN PHA THEN REWRITE_TAC[MESON[]` a /\b/\e/\c==>d <=> c ==> a/\b/\e==>d`] THEN
1358 DISCH_TAC THEN REWRITE_TAC[GSYM (MESON[]` a /\b/\e/\c==>d <=> c ==> a/\b/\e==>d`)]
1359 THEN REWRITE_TAC[MESON[trg_d3_sym]` d3 x v0 < &2 /\ aa/\
1360 ((~(d3 v0 x < &2) \/ l) \/ l') <=> d3 x v0 < &2 /\ aa/\ (l\/ l')`; IN] THEN
1361 PHA THEN REWRITE_TAC[MESON[]` (!w. s w /\ ~(w = v0) ==> d3 x v0 < d3 x w) /\
1362 aa /\ bb /\ (cc \/ ~(!w. s w /\ dd w /\ ee w /\ ~(w = v0) ==> d3 x v0 < d3 x w)) <=>
1363 (!w. s w /\ ~(w = v0) ==> d3 x v0 < d3 x w) /\ aa /\ bb /\ cc`] THEN
1364 REWRITE_TAC[obstruct] THEN ONCE_REWRITE_TAC[BAR_TRI] THEN
1365 REWRITE_TAC[ MESON[]`(?bar. (?x y z. bar = {x, y, z} /\ P {x, y, z}) /\ Q bar) <=>
1366 (?x y z. P {x, y, z} /\ Q {x, y, z})`] THEN NHANH (MESON[]` ~(conv0 {v0, x} INTER
1367 conv {x', y, z} = {}) ==> v0 IN {x' ,y,z} \/ ~( v0 IN {x', y,z})`) THEN KHANANG THEN
1368 NHANH (MESON[IN_SET3; SET_RULE` x = a ==> {x,b,c} = {a,b,c} /\ {x,b,c} = {b,c,a} /\
1369 {x,b,c} = {b,a,c} `]` x IN {a,b,c} ==> (? yy zz. {x,yy,zz} = {a,b,c})`) THEN
1370 REWRITE_TAC[EXISTS_OR_THM] THEN NGOAC THEN REWRITE_TAC[MESON[]`(?x' y z. P {x', y, z}
1371 /\ (?yy zz. {x, yy, zz} = {x', y, z})) <=> (?y z. P {x, y, z})`] THEN
1372 NHANH (CUTHE4 IN_AFF_GE_CON) THEN PHA THEN
1373 REWRITE_TAC[SET_RULE` ~UNIONS {aff_ge {v0} {v1, v2} | v1,v2 | barrier s {v0, v1, v2}} x /\
1374 ((?y z. {v0, y, z} IN barrier s /\ aaa y z /\ x IN aff_ge {v0} {y, z} /\
1375 bbb y z) \/ last) <=> ~UNIONS {aff_ge {v0} {v1, v2} | v1,v2 | barrier s {v0, v1, v2}} x /\
1376 last`] THEN REWRITE_TAC[DE_MORGAN_THM] THEN SIMP_TAC[GSYM NOV20] THEN
1377 REWRITE_TAC[d3; GSYM IN_VO_EQ] THEN NHANH (MESON[X_IN_VOR_X; VORONOI_CONV]` x IN voronoi v0 s
1378 ==> v0 IN voronoi v0 s /\ convex (voronoi v0 s )`) THEN
1379 NHANH (MESON[CONVEX_IM_CONV02_SU ]` x IN voronoi v0 s /\ v0 IN voronoi v0 s /\
1380 convex (voronoi v0 s) ==> conv0 {v0,x} SUBSET voronoi v0 s `) THEN PHA THEN
1381 DISCH_TAC THEN GEN_TAC THEN STRIP_TAC THENL [REPEAT (FIRST_X_ASSUM MP_TAC) THEN
1382 REWRITE_TAC[ IMP_IMP] THEN PHA THEN NHANH (SET_RULE` conv0 {v0, x} SUBSET voronoi v0 s
1383 /\a1 /\a2 /\a3 /\ ~(conv0 {v0, x} INTER conv {x', y, z} = {}) /\ l ==>
1384 ~( voronoi v0 s INTER conv {x', y, z} = {})`) THEN NHANH (MESON[FOUR_POINTS]
1385 ` {x', y, z} IN barrier s /\ a1 /\ ~(v0 IN {x', y, z}) ==> CARD {x',y,z, v0} = 4 `)
1386 THEN PHA THEN NHANH (SET_RULE ` conv0 {v0, x} SUBSET s /\ a1 /\a2 /\a3 /\
1387 ~(conv0 {v0, x} INTER s1 = {}) /\ l ==> ~( s INTER s1 = {}) `) THEN PHA THEN
1388 REWRITE_TAC[MESON[]`( s x /\ l <=>l/\ s x)/\ (a IN barrier s /\ l <=>
1389 l /\ a IN barrier s) `] THEN NHANH (SPEC_ALL (REWRITE_RULE[CONV3_EQ] IN_AFF_GE_CON))
1390 THEN PHA THEN REWRITE_TAC[SET_RULE ` ~UNIONS {aff_ge {v0} {v1, v2} | v1,v2 |
1391 barrier s {v0, v1, v2}} x /\ a1 /\ x IN aff_ge {v0} {y, z} /\
1392 a2 /\ a3/\ {v0, y, z} IN barrier s /\ a4 <=> F `] ; REPEAT (FIRST_X_ASSUM MP_TAC)]
1393 THEN REWRITE_TAC[ IMP_IMP] THEN PHA THEN
1394 NHANH (SET_RULE` conv0 {v0, x} SUBSET voronoi v0 s /\a1 /\a2 /\a3 /\
1395 ~(conv0 {v0, x} INTER conv {x', y, z} = {}) /\ l ==>
1396 ~( voronoi v0 s INTER conv {x', y, z} = {})`) THEN
1397 NHANH (MESON[FOUR_POINTS]` {x', y, z} IN barrier s /\ a1 /\
1398 ~(v0 IN {x', y, z}) ==> CARD {x',y,z, v0} = 4 `) THEN PHA THEN NHANH (SET_RULE `
1399 conv0 {v0, x} SUBSET s /\ a1 /\a2 /\a3 /\ ~(conv0 {v0, x} INTER s1 = {}) /\ l
1400 ==> ~( s INTER s1 = {}) `) THEN PHA THEN REWRITE_TAC[MESON[]`( s x /\ l <=>l/\
1401 s x)/\ (a IN barrier s /\ l <=> l /\ a IN barrier s) `] THEN PHA THEN
1402 NHANH (MESON[IMP_IN_Q_SYS; IN]` CARD {x', y, z, v0} = 4 /\
1403 ~(voronoi v0 s INTER conv {x', y, z} = {}) /\ {x', y, z} IN barrier s /\
1404 s v0 ==> {v0,x',y,z} IN Q_SYS s `) THEN NHANH (SPEC_ALL AFF_LE_CONE) THEN PHA THEN
1405 ONCE_REWRITE_TAC[MESON[IN] ` ~ UNIONS s x <=> ~ ( x IN UNIONS s ) `] THEN
1406 ONCE_REWRITE_TAC[MESON[]` a1 /\a /\ b /\ x IN cone v0 {x', y, z} /\ l <=>a /\ b /\ l /\
1407 x IN cone v0 {x', y, z} /\ a1 `] THEN PHA THEN REWRITE_TAC[MESON[]` a IN Q_SYS s /\
1408 b /\ c <=> b /\ c /\ a IN Q_SYS s`] THEN NHANH (SPEC_ALL IMP_IN_AFF4) THEN
1409 NGOAC THEN REWRITE_TAC[MESON[]` (a /\ b ) /\ x IN aff_gt {v0} {x', y, z} <=>
1410 x IN aff_gt {v0} {x', y, z}/\ b/\ a `] THEN PHA THEN DAO THEN
1411 REWRITE_TAC[GSYM VORO2_EX] THEN REWRITE_TAC[prove(`dist (x,v0) < &2 /\a1/\a2/\a3 /\
1412 x IN voronoi v0 s /\ l <=> a1/\a2/\a3 /\ l /\ x IN voro2 v0 s`, REWRITE_TAC[GSYM d3;
1413 voro2; IN_ELIM_THM] THEN MESON_TAC[])] THEN REWRITE_TAC[MESON[]`x IN aff_le a s /\
1414 l <=> l /\ x IN aff_le a s `] THEN DAO THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
1415 SIMP_TAC[] THEN ONCE_REWRITE_TAC[MESON[]` (! x. P x ) /\ a = b /\ l <=> b = a /\ l /\
1416 (! x . P x )`] THEN SIMP_TAC[] THEN MATCH_MP_TAC (MESON[]` ( a1 /\a2/\a3/\a4 ==> l )
1417 ==> ( a1/\a2/\a3/\a4/\a5 ==> l ) `) THEN REWRITE_TAC[IN_UNIONS; IN_ELIM_THM] THEN
1418 REWRITE_TAC[ MESON[]` (?t. (? a b c. P a b c /\ t = Q a b c ) /\ x IN t )
1419 <=> (? a b c. P a b c /\ x IN Q a b c ) `] THEN REWRITE_TAC[IN_INTER] THEN