1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
3 (* Section: Appendix, Main Estimate, check_completeness *)
4 (* Chapter: Local Fan *)
6 (* Author: Thomas Hales *)
8 (* ========================================================================== *)
10 module Iunbuig = struct
16 let LET_THM = CONJ LET_DEF LET_END_DEF;;
19 let quadratic_at_most_2_roots = prove_by_refinement(
21 ~(a = &0) /\ a * x pow 2 + b * x + c = &0 ==> x = x1 \/ x = x2`,
25 ASM_CASES_TAC `~(?x1. a * x1 pow 2 + b * x1 + c = &0)`;
27 FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[] THEN REPEAT STRIP_TAC;
28 ASM_CASES_TAC `!x2. a * x2 pow 2 + b * x2 + c = &0 ==> x2 = x1`;
30 FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM] THEN REPEAT STRIP_TAC;
31 GEXISTL_TAC [`x1`;`x2`];
32 BY(GEN_TAC THEN ASM_TAC THEN CONV_TAC REAL_RING)
33 (* String.length above = 414. String.length below = 233. 56% the length. *)
36 asmcs `~(?x1. a * x1 pow 2 + b * x1 + c = &0)`
38 fx mp then rt[] then str/r
39 asmcs `!x2. a * x2 pow 2 + b * x2 + c = &0 ==> x2 = x1`
41 fx mp then rt[NOT_FORALL_THM] then str/r
43 g then asm then cvc REAL_RING
46 If there are no roots, it is obvious. Otherwise, let x1 be a root.
47 If every root is x1 it is obvious. Otherwise, let x2 be a second root.
48 Instantiate the existential quantifiers with these two roots, and solve the resulting
49 problem by Groebner basis algorithm.
54 let ARCV_ADD_AFF_GE = prove_by_refinement(
55 `!(u:real^N) v w x. ~(v = u) /\ ~(w = u) /\ ~(x = u) /\ x IN aff_ge {u} {v, w} ==>
56 arcV u v x + arcV u x w = arcV u v w`,
59 BY(REWRITE_TAC[ARCV_ANGLE;ANGLES_ADD_AFF_GE])
63 let SUM_NUMSEG4 = prove_by_refinement(
64 `!t. sum (0..4) t = t 0 + t 1 + t 2 + t 3 + t 4`,
67 REWRITE_TAC[arith `4 = SUC 3`;SUM_CLAUSES_NUMSEG;Qknvmlb.SUM_NUMSEG3;arith `0 <= SUC 3`];
72 let epsilon_pent = prove_by_refinement(
73 `!e e' e'' e''' e''''. &0 < e /\ &0 < e' /\ &0 < e'' /\ &0 < e''' /\ &0 < e'''' ==> (?e'''''. &0 < e''''' /\ (!t. abs t < e''''' ==> abs t < e) /\ (!t. abs t < e''''' ==> abs t < e') /\ (!t. abs t < e''''' ==> abs t < e'') /\ (!t. abs t < e''''' ==> abs t < e''') /\ (!t. abs t < e''''' ==> abs t < e''''))`,
76 REPEAT WEAKER_STRIP_TAC;
77 INTRO_TAC Cuxvzoz.epsilon_quad [`e`;`e'`;`e''`;`e'''`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
78 INTRO_TAC Cuxvzoz.epsilon_pair [`e''''`;`e'''''`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
79 TYPIFY `e''''''` EXISTS_TAC;
80 BY(ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN (REPEAT (FIRST_X_ASSUM MATCH_MP_TAC)) THEN ASM_REWRITE_TAC[])
84 let epsilon_hex = prove_by_refinement(
85 `!e e' e'' e''' e'''' e5. &0 < e /\ &0 < e' /\ &0 < e'' /\ &0 < e''' /\ &0 < e'''' /\ &0 < e5 ==> (?e6. &0 < e6 /\ (!t. abs t < e6 ==> abs t < e) /\ (!t. abs t < e6 ==> abs t < e') /\ (!t. abs t < e6 ==> abs t < e'') /\ (!t. abs t < e6 ==> abs t < e''') /\ (!t. abs t < e6 ==> abs t < e'''') /\ (!t. abs t < e6 ==> abs t < e5))`,
88 REPEAT WEAKER_STRIP_TAC;
89 INTRO_TAC epsilon_pent [`e`;`e'`;`e''`;`e'''`;`e''''`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
90 INTRO_TAC Cuxvzoz.epsilon_pair [`e'''''`;`e5`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
91 TYPIFY `e''''''` EXISTS_TAC;
92 BY(ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN (REPEAT (FIRST_X_ASSUM MATCH_MP_TAC)) THEN ASM_REWRITE_TAC[])
96 let epsilon_hept = prove_by_refinement(
97 `!e e' e'' e''' e'''' e5 e6. &0 < e /\ &0 < e' /\ &0 < e'' /\ &0 < e''' /\ &0 < e'''' /\ &0 < e5 /\ &0 < e6 ==> (?e7. &0 < e7 /\ (!t. abs t < e7 ==> abs t < e) /\ (!t. abs t < e7 ==> abs t < e') /\ (!t. abs t < e7 ==> abs t < e'') /\ (!t. abs t < e7 ==> abs t < e''') /\ (!t. abs t < e7 ==> abs t < e'''') /\ (!t. abs t < e7 ==> abs t < e5) /\ (!t. abs t < e7 ==> abs t < e6))`,
100 REPEAT WEAKER_STRIP_TAC;
101 INTRO_TAC epsilon_hex [`e`;`e'`;`e''`;`e'''`;`e''''`;`e5`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
102 INTRO_TAC Cuxvzoz.epsilon_pair [`e6`;`e6'`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
103 TYPIFY `e'''''` EXISTS_TAC;
104 BY(ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN (REPEAT (FIRST_X_ASSUM MATCH_MP_TAC)) THEN ASM_REWRITE_TAC[])
108 let re_eqvl_imp_le = prove_by_refinement(
109 `!a b. re_eqvl a b ==> (&0 <= a <=> &0 <= b)`,
112 TYPIFY `!a b. re_eqvl a b /\ &0 <= b ==> &0 <= a` ENOUGH_TO_SHOW_TAC;
113 BY(MESON_TAC[Leaf_cell.RE_EQVL_SYM]);
114 REWRITE_TAC[Trigonometry2.re_eqvl];
115 REPEAT WEAKER_STRIP_TAC;
117 GMATCH_SIMP_TAC REAL_LE_MUL;
118 BY(ASM_TAC THEN REAL_ARITH_TAC)
122 let re_eqvl_real_sgn = prove_by_refinement(
123 `!x y. re_eqvl x y <=> real_sgn x = real_sgn y`,
126 REPEAT WEAKER_STRIP_TAC;
127 MATCH_MP_TAC (TAUT `((a ==>b) /\ (b ==> a)) ==> (a = b)`);
128 REWRITE_TAC[Trigonometry2.re_eqvl];
129 CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[];
130 REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[REAL_SGN_MUL;GSYM REAL_SGN_EQ;arith `&0 < t <=> t > &0`];
131 BY(DISCH_THEN (unlist REWRITE_TAC) THEN REAL_ARITH_TAC);
132 FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[REAL_SGN];
133 TYPIFY `x = &0` ASM_CASES_TAC;
134 ASM_REWRITE_TAC[arith `abs(&0) = &0`;arith `&0 / &0 = &0`;arith `&0 = x <=> x = &0`;REAL_DIV_EQ_0;REAL_ENTIRE;arith `abs y = &0 <=> y = &0`];
135 BY(MESON_TAC[arith `&0 < &1`]);
137 TYPIFY `~(y = &0)` (C SUBGOAL_THEN ASSUME_TAC);
139 FIRST_X_ASSUM_ST `abs` MP_TAC;
140 BY(ASM_REWRITE_TAC[arith `&0 / t = &0`;REAL_DIV_EQ_0] THEN ASM_TAC THEN REAL_ARITH_TAC);
141 TYPIFY `x / y` EXISTS_TAC;
143 Calc_derivative.CALC_ID_TAC;
144 BY(ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
145 REWRITE_TAC[Calc_derivative.invert_den_lt];
146 REWRITE_TAC[REAL_MUL_POS_LT];
147 FIRST_X_ASSUM_ST `abs` MP_TAC THEN REWRITE_TAC[GSYM REAL_SGN;real_sgn];
148 RULE_ASSUM_TAC (REWRITE_RULE[arith `~(x = &0) <=> (&0 < x \/ x < &0) /\ ~(&0 < x /\ x < &0)`]);
149 ASSUME_TAC (arith ` ~(&1 = -- &1)`);
150 BY(REPEAT COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[])
154 let coplanar_delta_y_zero = prove_by_refinement(
155 `!(u0:real^3) u1 u2 u3. coplanar {u0, u1, u2, u3} <=>
156 delta_y (dist (u0,u1)) (dist (u0,u2)) (dist (u0,u3))
159 (dist (u1,u2)) = &0`,
162 REPEAT WEAKER_STRIP_TAC;
163 BY(ASM_MESON_TAC[Terminal.DELTA_Y_POS_4POINTS;Oxlzlez.coplanar_delta_y;arith `&0 <= x ==> (~(&0 < x) <=> (x = &0))`])
167 let real_continuous_finite_range_constant = prove_by_refinement(
168 `!f a b. f real_continuous_on (real_interval (a,b)) /\ FINITE (IMAGE f (real_interval (a,b))) ==>
169 (?c. !x. x IN real_interval (a,b) ==> f x = c)`,
172 REPEAT WEAKER_STRIP_TAC;
173 TYPIFY `(?c. !x. x IN IMAGE lift (real_interval(a,b)) ==> ((lift o f o drop) x = c))` ENOUGH_TO_SHOW_TAC;
174 REPEAT WEAKER_STRIP_TAC;
175 TYPIFY `drop c` EXISTS_TAC;
176 REPEAT WEAKER_STRIP_TAC;
177 FIRST_X_ASSUM_ST `IMAGE` (C INTRO_TAC [`lift x`]);
178 REWRITE_TAC[o_THM;LIFT_DROP];
180 MATCH_MP_TAC FUN_IN_IMAGE;
181 BY(ASM_REWRITE_TAC[]);
182 DISCH_THEN (SUBST1_TAC o GSYM);
183 BY(REWRITE_TAC[LIFT_DROP]);
184 MATCH_MP_TAC CONTINUOUS_FINITE_RANGE_CONSTANT;
186 ONCE_REWRITE_TAC[GSYM LIFT_DROP];
187 REWRITE_TAC[GSYM INTERVAL_REAL_INTERVAL];
188 BY(REWRITE_TAC[CONNECTED_INTERVAL]);
191 BY(ASM_REWRITE_TAC[GSYM REAL_CONTINUOUS_ON]);
192 REWRITE_TAC[GSYM IMAGE_o;ETA_AX;GSYM o_ASSOC];
193 TYPIFY_GOAL_THEN `!X. IMAGE (lift o f o drop o lift) X = IMAGE lift (IMAGE f (IMAGE (drop o lift) X))` (unlist REWRITE_TAC);
194 BY(REWRITE_TAC[GSYM IMAGE_o;GSYM o_ASSOC]);
195 REWRITE_TAC[IMAGE_LIFT_DROP];
196 MATCH_MP_TAC FINITE_IMAGE;
197 BY(ASM_REWRITE_TAC[])
201 let planar_deform_dist = prove_by_refinement(
202 `!(v0:real^3) v1 v2 f V e'.
203 v1 IN V /\ v2 IN V /\ ~(v0 = vec 0) /\
204 &0 < e' /\ deformation f V (--e',e') /\ (!v t. ~(v =v1) /\ ~(v = v2) ==> f v t = v) /\
206 ==> coplanar {vec 0, v0, f v1 t, f v2 t} /\
207 dist (v0,f v1 t) = dist (v0,v1) /\
208 norm (f v1 t) = norm v1 /\
209 dist (f v2 t,v0) = dist (v2,v0) /\
210 norm (f v2 t) = norm v2) ==>
211 (!t. abs t < e' ==> dist(f v1 t,f v2 t) = dist(v1,v2))
215 REPEAT WEAKER_STRIP_TAC;
216 TYPIFY `f v1 (&0) = v1 /\ f v2 (&0) = v2` (C SUBGOAL_THEN ASSUME_TAC);
217 FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation];
219 TYPED_ABBREV_TAC `b = ((norm v0 * norm v0) * norm v0 * norm v0 + (norm v2 * norm v2 - dist (v0,v2) * dist (v0,v2)) * (norm v1 * norm v1 - dist (v0,v1) * dist (v0,v1)) - (norm v0 * norm v0) * (norm v1 * norm v1 + norm v2 * norm v2 + dist (v0,v2) * dist (v0,v2) + dist (v0,v1) * dist (v0,v1)))`;
220 TYPED_ABBREV_TAC `c = (norm v0 * norm v0) * (norm v2 * norm v2) * dist (v0,v2) * dist (v0,v2) + (norm v0 * norm v0) * (norm v1 * norm v1) * dist (v0,v1) * dist (v0,v1) - (norm v2 * norm v2) * (norm v0 * norm v0 + norm v1 * norm v1 - norm v2 * norm v2 + dist (v0,v2) * dist (v0,v2) - dist (v0,v1) * dist (v0,v1)) * dist (v0,v1) * dist (v0,v1) - (norm v1 * norm v1) * (dist (v0,v2) * dist (v0,v2)) * (norm v0 * norm v0 - norm v1 * norm v1 + norm v2 * norm v2 - dist (v0,v2) * dist (v0,v2) + dist (v0,v1) * dist (v0,v1))`;
221 TYPED_ABBREV_TAC `a = (norm v0 * norm v0)`;
222 INTRO_TAC quadratic_at_most_2_roots [`a`;`b`;`c`];
223 REPEAT WEAKER_STRIP_TAC;
224 INTRO_TAC real_continuous_finite_range_constant [`(\t. dist(f v1 t, f v2 t))`;`-- e'`;`e'`];
227 GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
228 REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL];
229 REPEAT WEAKER_STRIP_TAC;
230 MATCH_MP_TAC Local_lemmas1.CON_ATREAL_REAL_CON2_REDO;
231 FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation;ETA_AX];
233 TYPIFY `IMAGE (\t. dist (f v1 t,f v2 t) pow 2) (real_interval (--e',e')) SUBSET {x1,x2}` ENOUGH_TO_SHOW_TAC;
234 TYPIFY `FINITE {x1,x2}` ENOUGH_TO_SHOW_TAC;
235 TYPIFY_GOAL_THEN `!X. IMAGE (\t. dist (f v1 t,f v2 t) pow 2) X = IMAGE (\t. t pow 2) (IMAGE (\t. dist (f v1 t,f v2 t)) X)` (unlist REWRITE_TAC);
236 REWRITE_TAC[GSYM IMAGE_o];
237 BY(GEN_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM;o_THM]);
238 TYPED_ABBREV_TAC `s = (IMAGE (\t. dist (f v1 t,f v2 t)) (real_interval (--e',e')))`;
239 INTRO_TAC HAS_SIZE_IMAGE_INJ_EQ [`(\t. t pow 2)`;`s`;`CARD (IMAGE (\t. t pow 2) s)`];
242 REWRITE_TAC[IN_IMAGE] THEN REPEAT WEAKER_STRIP_TAC;
243 FIRST_X_ASSUM MP_TAC;
245 REWRITE_TAC[GSYM REAL_EQ_SQUARE_ABS];
246 REPEAT (GMATCH_SIMP_TAC (arith `&0 <= x ==> abs x = x`));
247 BY(REWRITE_TAC[DIST_POS_LE]);
248 REWRITE_TAC[HAS_SIZE];
249 BY(MESON_TAC[FINITE_SUBSET;FINITE_IMAGE]);
250 BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]);
251 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_IMAGE];
252 REPEAT WEAKER_STRIP_TAC;
253 FIRST_X_ASSUM MATCH_MP_TAC;
256 REWRITE_TAC[REAL_ENTIRE];
257 REWRITE_TAC[NORM_EQ_0];
258 BY(ASM_REWRITE_TAC[]);
259 FIRST_X_ASSUM_ST `coplanar` (C INTRO_TAC [`x'`]);
261 BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[IN_REAL_INTERVAL;arith `-- e < t /\ t < e <=> abs t < e`]);
262 REPEAT WEAKER_STRIP_TAC;
263 FIRST_X_ASSUM_ST `coplanar` MP_TAC THEN REWRITE_TAC[coplanar_delta_y_zero];
264 REPEAT (FIRST_X_ASSUM_ST `dist` MP_TAC) THEN REWRITE_TAC[DIST_SYM;DIST_0] THEN REPEAT WEAKER_STRIP_TAC THEN (FIRST_X_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[];
265 ONCE_REWRITE_TAC[arith `x = &0 <=> -- x = &0`];
266 ASM_REWRITE_TAC[Sphere.delta_y;Nonlinear_lemma.delta_quadratic];
268 REPEAT WEAKER_STRIP_TAC;
269 FIRST_ASSUM (C INTRO_TAC [`&0`]);
270 FIRST_X_ASSUM (C INTRO_TAC [`t`]);
272 REPEAT (DISCH_THEN GMATCH_SIMP_TAC);
274 FIRST_X_ASSUM_ST `deformation` MP_TAC THEN ASM_REWRITE_TAC[Localization.deformation;IN_REAL_INTERVAL;arith `--e < t /\ t < e <=> abs t < e`;arith `abs(&0) = &0`];
280 let deform_pent_exists = prove_by_refinement(
281 `!V g23 v0 v1 v2 v3 e. ?f.
283 ( v1 IN V /\ v2 IN V /\
284 (coplanar {vec 0,v0,v1,v2} ==> (v1 cross v0) dot (v2 cross v0) > &0) /\
285 ~coplanar {vec 0,v0,v2,v3} /\ ~(collinear {vec 0,v1,v2}) /\
286 &0 < azim (vec 0) v1 v2 v0 /\ azim (vec 0) v1 v2 v0 <= pi /\
287 v2 dot (v3 cross v0) > &0 /\
289 g23 real_continuous_on (real_interval (--e,e)) /\
292 (?e'. &0 < e' /\ deformation f V (-- e', e') /\
293 (!v t. ~(v = v1) /\ ~(v = v2) ==> f v t = v) /\
295 dist(v0,f v1 t) = dist(v0,v1) /\
296 dist(f v2 t,f v1 t) = dist(v2,v1) /\
297 norm(f v1 t) = norm(v1) /\
298 dist (f v2 t,v0) = dist(v2,v0) /\
299 dist (f v2 t,v3) = dist(v2,v3)+ g23 t /\
300 norm(f v2 t) = norm (v2)
304 REPEAT WEAKER_STRIP_TAC;
305 REWRITE_TAC[MESON [] `(?f. a ==> P f) <=> (a ==> (?f. P f))`];
306 REPEAT WEAKER_STRIP_TAC;
307 TYPIFY `~coplanar {vec 0,v0,v1,v2}` ASM_CASES_TAC;
308 INTRO_TAC Cuxvzoz.deform_684_pent_exists [`V`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
309 REPEAT WEAKER_STRIP_TAC;
310 FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[];
311 REWRITE_TAC[arith `x > &0 <=> &0 <= x /\ ~(x = &0)`];
315 BY(REPEAT (FIRST_X_ASSUM_ST `coplanar` MP_TAC) THEN REWRITE_TAC[GSYM Local_lemmas.CROSS_DOT_COPLANAR] THEN VEC3_TAC);
316 INTRO_TAC Trigonometry2.JBDNJJB [`v1`;`v2`;`v0`];
317 TYPIFY `((v1 cross v2) dot v0) = v1 dot (v2 cross v0)` (C SUBGOAL_THEN SUBST1_TAC);
319 ONCE_REWRITE_TAC[Leaf_cell.RE_EQVL_SYM];
320 DISCH_THEN ((unlist REWRITE_TAC) o (MATCH_MP re_eqvl_imp_le));
321 BY(ASM_MESON_TAC[Local_lemmas.SIN_AZIM_POS_PI_LT]);
322 REPEAT WEAKER_STRIP_TAC;
323 BY(GEXISTL_TAC [`f`;`e'`] THEN ASM_MESON_TAC[]);
324 COMMENT "planar case";
325 INTRO_TAC Cuxvzoz.deform_planar_exists [`V`;`(\ (t:real). &0)`;`(\ (t:real). &0)`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
326 RULE_ASSUM_TAC(REWRITE_RULE[]);
327 REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[arith `x + &0 = x`];
328 GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT THEN REWRITE_TAC[REAL_CONTINUOUS_CONST;Ocbicby.REAL_OPEN_REAL_INTERVAL];
331 BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
332 BY(FIRST_X_ASSUM_ST `collinear` MP_TAC THEN MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b} = {a,b}`]);
333 REPEAT WEAKER_STRIP_TAC;
334 GEXISTL_TAC [`f`;`e'`] THEN ASM_REWRITE_TAC[];
335 REPEAT WEAKER_STRIP_TAC;
336 TYPIFY `~(v0 = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
337 BY(ASM_MESON_TAC[COPLANAR_3;SET_RULE `{a,a,b,c} = {a,b,c}`]);
338 INTRO_TAC planar_deform_dist [`v0`;`v1`;`v2`;`f`;`V`;`e'`];
343 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[DIST_SYM] THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[])
349 let deform_pent_exists = prove_by_refinement(
350 `!V g23 v0 v1 v2 v3 e. ?f.
352 ( v1 IN V /\ v2 IN V /\
353 (coplanar {vec 0,v0,v1,v2} ==> (v1 cross v0) dot (v2 cross v0) > &0) /\
354 ~coplanar {vec 0,v0,v2,v3} /\ ~(collinear {vec 0,v1,v2}) /\
355 azim (vec 0) v1 v2 v0 <= pi /\
356 v2 dot (v3 cross v0) > &0 /\
358 g23 real_continuous_on (real_interval (--e,e)) /\
361 (?e'. &0 < e' /\ deformation f V (-- e', e') /\
362 (!v t. ~(v = v1) /\ ~(v = v2) ==> f v t = v) /\
364 dist(v0,f v1 t) = dist(v0,v1) /\
365 dist(f v2 t,f v1 t) = dist(v2,v1) /\
366 norm(f v1 t) = norm(v1) /\
367 dist (f v2 t,v0) = dist(v2,v0) /\
368 dist (f v2 t,v3) = dist(v2,v3)+ g23 t /\
369 norm(f v2 t) = norm (v2)
373 REPEAT WEAKER_STRIP_TAC;
374 REWRITE_TAC[MESON [] `(?f. a ==> P f) <=> (a ==> (?f. P f))`];
375 REPEAT WEAKER_STRIP_TAC;
376 TYPIFY `~coplanar {vec 0,v0,v1,v2}` ASM_CASES_TAC;
377 INTRO_TAC Cuxvzoz.deform_684_pent_exists [`V`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
378 REPEAT WEAKER_STRIP_TAC;
379 FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[];
380 REWRITE_TAC[arith `x > &0 <=> &0 <= x /\ ~(x = &0)`];
384 BY(REPEAT (FIRST_X_ASSUM_ST `coplanar` MP_TAC) THEN REWRITE_TAC[GSYM Local_lemmas.CROSS_DOT_COPLANAR] THEN VEC3_TAC);
385 INTRO_TAC Trigonometry2.JBDNJJB [`v1`;`v2`;`v0`];
386 TYPIFY `((v1 cross v2) dot v0) = v1 dot (v2 cross v0)` (C SUBGOAL_THEN SUBST1_TAC);
388 ONCE_REWRITE_TAC[Leaf_cell.RE_EQVL_SYM];
389 DISCH_THEN ((unlist REWRITE_TAC) o (MATCH_MP re_eqvl_imp_le));
390 BY(ASM_MESON_TAC[Local_lemmas.SIN_AZIM_POS_PI_LT]);
391 REPEAT WEAKER_STRIP_TAC;
392 BY(GEXISTL_TAC [`f`;`e'`] THEN ASM_MESON_TAC[]);
393 COMMENT "planar case";
394 INTRO_TAC Cuxvzoz.deform_planar_exists [`V`;`(\ (t:real). &0)`;`(\ (t:real). &0)`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
395 RULE_ASSUM_TAC(REWRITE_RULE[]);
396 REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[arith `x + &0 = x`];
397 GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT THEN REWRITE_TAC[REAL_CONTINUOUS_CONST;Ocbicby.REAL_OPEN_REAL_INTERVAL];
400 BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
401 BY(FIRST_X_ASSUM_ST `collinear` MP_TAC THEN MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b} = {a,b}`]);
402 REPEAT WEAKER_STRIP_TAC;
403 GEXISTL_TAC [`f`;`e'`] THEN ASM_REWRITE_TAC[];
404 REPEAT WEAKER_STRIP_TAC;
405 TYPIFY `~(v0 = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
406 BY(ASM_MESON_TAC[COPLANAR_3;SET_RULE `{a,a,b,c} = {a,b,c}`]);
407 INTRO_TAC planar_deform_dist [`v0`;`v1`;`v2`;`f`;`V`;`e'`];
412 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[DIST_SYM] THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[])
417 let deform_pent_exists = prove_by_refinement(
418 `!V g23 v0 v1 v2 v3 e. ?f.
419 v1 IN V /\ v2 IN V /\
420 (coplanar {vec 0,v0,v1,v2} ==> (v1 cross v0) dot (v2 cross v0) > &0) /\
421 ~coplanar {vec 0,v0,v2,v3} /\ ~(collinear {vec 0,v1,v2}) /\
422 azim (vec 0) v1 v2 v0 <= pi /\
423 v2 dot (v3 cross v0) > &0 /\
425 g23 real_continuous_on (real_interval (--e,e)) /\
428 (?e'. &0 < e' /\ deformation f V (-- e', e') /\
429 (!v t. ~(v = v1) /\ ~(v = v2) ==> f v t = v) /\
431 dist(v0,f v1 t) = dist(v0,v1) /\
432 dist(f v2 t,f v1 t) = dist(v2,v1) /\
433 norm(f v1 t) = norm(v1) /\
434 dist (f v2 t,v0) = dist(v2,v0) /\
435 dist (f v2 t,v3) = dist(v2,v3)+ g23 t /\
436 norm(f v2 t) = norm (v2) /\
437 (coplanar {vec 0,v0,v1,v2} ==> coplanar {vec 0,v0,f v1 t,f v2 t})
441 REPEAT WEAKER_STRIP_TAC;
442 REWRITE_TAC[MESON [] `(?f. a ==> P f) <=> (a ==> (?f. P f))`];
443 REPEAT WEAKER_STRIP_TAC;
444 TYPIFY `~coplanar {vec 0,v0,v1,v2}` ASM_CASES_TAC;
445 INTRO_TAC Cuxvzoz.deform_684_pent_exists [`V`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
446 REPEAT WEAKER_STRIP_TAC;
447 FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[];
448 REWRITE_TAC[arith `x > &0 <=> &0 <= x /\ ~(x = &0)`];
452 BY(REPEAT (FIRST_X_ASSUM_ST `coplanar` MP_TAC) THEN REWRITE_TAC[GSYM Local_lemmas.CROSS_DOT_COPLANAR] THEN VEC3_TAC);
453 INTRO_TAC Trigonometry2.JBDNJJB [`v1`;`v2`;`v0`];
454 TYPIFY `((v1 cross v2) dot v0) = v1 dot (v2 cross v0)` (C SUBGOAL_THEN SUBST1_TAC);
456 ONCE_REWRITE_TAC[Leaf_cell.RE_EQVL_SYM];
457 DISCH_THEN ((unlist REWRITE_TAC) o (MATCH_MP re_eqvl_imp_le));
458 BY(ASM_MESON_TAC[Local_lemmas.SIN_AZIM_POS_PI_LT]);
459 REPEAT WEAKER_STRIP_TAC;
460 BY(GEXISTL_TAC [`f`;`e'`] THEN ASM_MESON_TAC[]);
461 COMMENT "planar case";
462 INTRO_TAC Cuxvzoz.deform_planar_exists [`V`;`(\ (t:real). &0)`;`(\ (t:real). &0)`;`g23`;`v0`;`v1`;`v2`;`v3`;`e`];
463 RULE_ASSUM_TAC(REWRITE_RULE[]);
464 REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ASM_REWRITE_TAC[arith `x + &0 = x`];
465 GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT THEN REWRITE_TAC[REAL_CONTINUOUS_CONST;Ocbicby.REAL_OPEN_REAL_INTERVAL];
468 BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
469 BY(FIRST_X_ASSUM_ST `collinear` MP_TAC THEN MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b} = {a,b}`]);
470 REPEAT WEAKER_STRIP_TAC;
471 GEXISTL_TAC [`f`;`e'`] THEN ASM_REWRITE_TAC[];
472 REPEAT WEAKER_STRIP_TAC;
473 TYPIFY `~(v0 = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
474 BY(ASM_MESON_TAC[COPLANAR_3;SET_RULE `{a,a,b,c} = {a,b,c}`]);
475 INTRO_TAC planar_deform_dist [`v0`;`v1`;`v2`;`f`;`V`;`e'`];
480 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[DIST_SYM] THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[])
485 let EGHNAVX_SCS = prove_by_refinement(
487 (let bta = (\j. azim (vec 0) (v p) (v (p+1)) (v (p+j))) in
488 ( is_scs_v39 s /\ scs_k_v39 s = k /\
495 (!i j. i < j /\ j < k ==> bta i <= bta j) /\
496 (!q j. bta q = &0 /\ 0 < j /\ j <= q /\ q < k
497 ==> (j<q ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v (p+j+k-1)) = pi) /\
498 v (p+j) IN aff_gt {vec 0,v p} {v (p+1)}) /\
499 (!q j. bta q = bta (k - 1) /\ 0 < q /\ q < k - 1 /\ q <= j /\ j < k
500 ==> (q < j ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v(p+j+k-1)) = pi) /\
501 v(p+j) IN aff_gt {vec 0, v p} {v (p + k - 1)})))`,
506 REPEAT WEAKER_STRIP_TAC;
507 TYPED_ABBREV_TAC `FF = IMAGE (\i. (v i,v (SUC i))) (:num)`;
508 TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
509 TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
510 INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`k`];
513 TYPIFY `periodic v k /\ convex_local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
514 BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN ASM_MESON_TAC[arith `3 < k ==> ~(k<= 3)`]);
515 INTRO_TAC Terminal.ITER_vv_rho_node1 [`v`;`k`];
516 ASM_REWRITE_TAC[LET_THM];
517 TYPIFY_GOAL_THEN `3 <= k` (unlist REWRITE_TAC);
518 BY(ASM_MESON_TAC[arith `3 < k ==> 3 <= k`]);
520 INTRO_TAC (GEN_ALL Odxlstcv2.CARD_V_EQ_SCS_K1) [`s`;`v`;`V`;`k`];
523 TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
524 MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
525 BY(ASM_REWRITE_TAC[]);
526 TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
529 MATCH_MP_TAC FUN_IN_IMAGE;
530 BY(REWRITE_TAC[IN_UNIV]);
531 TYPIFY `!i j. ~(v i = v j) ==> ~collinear {vec 0, v i, v j}` (C SUBGOAL_THEN ASSUME_TAC);
532 INTRO_TAC Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN [`V`;`E`;`FF`];
533 BY(ASM_MESON_TAC[Appendix.scs_generic]);
534 INTRO_TAC (GENL [`v0:real^3`;`vv:num->real^3`;`i:num`] Local_lemmas.EGHNAVX) [`v p`;`\ (i:num). v (p + i)`];
535 REWRITE_TAC[RIGHT_FORALL_IMP_THM;GSYM RIGHT_AND_FORALL_THM];
539 REPEAT WEAKER_STRIP_TAC;
540 TYPIFY `?i'. v' = v i'` (C SUBGOAL_THEN MP_TAC);
541 FIRST_X_ASSUM_ST `IN` MP_TAC;
543 BY(REWRITE_TAC[IN_IMAGE;IN_UNIV]);
544 REPEAT WEAKER_STRIP_TAC;
548 REPEAT WEAKER_STRIP_TAC;
550 INTRO_TAC (GSYM Ocbicby.INTERIOR_ANGLE1_AZIM) [`s`;`v`];
551 ASM_REWRITE_TAC[LET_THM];
552 TYPIFY_GOAL_THEN `v IN BBs_v39 s` (unlist REWRITE_TAC);
553 BY(ASM_REWRITE_TAC[IN]);
555 COMMENT "first conjunct";
557 REPEAT WEAKER_STRIP_TAC;
558 FIRST_X_ASSUM_ST `SUBSET` (C INTRO_TAC [`q`]);
560 REPEAT WEAKER_STRIP_TAC;
563 FIRST_X_ASSUM (C INTRO_TAC [`j`]);
565 BY(REWRITE_TAC[arith `SUC (p+j) = p+j+1 /\ ((p+j) + k - 1 = p+j+k-1)`]);
567 FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_ELIM_THM];
568 DISCH_THEN (C INTRO_TAC [`v (p+(j:num))`]);
569 DISCH_THEN MATCH_MP_TAC;
570 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
571 REPEAT WEAKER_STRIP_TAC;
572 FIRST_X_ASSUM_ST `SUBSET` (C INTRO_TAC [`q`]);
574 REPEAT WEAKER_STRIP_TAC;
577 FIRST_X_ASSUM (C INTRO_TAC [`j`]);
579 BY(REWRITE_TAC[arith `SUC (p+j) = p+j+1 /\ ((p+j) + k - 1 = p+j+k-1)`]);
580 FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_ELIM_THM];
581 DISCH_THEN (C INTRO_TAC [`v (p+(j:num))`]);
582 DISCH_THEN MATCH_MP_TAC;
583 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[])
588 let EGHNAVX_COLL_SCS = prove_by_refinement(
590 (let bta = (\j. azim (vec 0) (v p) (v (p+1)) (v (p+j))) in
591 ( is_scs_v39 s /\ scs_k_v39 s = k /\
595 (!i. ~(v i = v p) ==> ~collinear {vec 0,v p,v i})
599 (!i j. i < j /\ j < k ==> bta i <= bta j) /\
600 (!q j. bta q = &0 /\ 0 < j /\ j <= q /\ q < k
601 ==> (j<q ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v (p+j+k-1)) = pi) /\
602 v (p+j) IN aff_gt {vec 0,v p} {v (p+1)}) /\
603 (!q j. bta q = bta (k - 1) /\ 0 < q /\ q < k - 1 /\ q <= j /\ j < k
604 ==> (q < j ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v(p+j+k-1)) = pi) /\
605 v(p+j) IN aff_gt {vec 0, v p} {v (p + k - 1)})))`,
610 REPEAT WEAKER_STRIP_TAC;
611 TYPED_ABBREV_TAC `FF = IMAGE (\i. (v i,v (SUC i))) (:num)`;
612 TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
613 TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
614 INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`k`];
617 TYPIFY `periodic v k /\ convex_local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
618 BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN ASM_MESON_TAC[arith `3 < k ==> ~(k<= 3)`]);
619 INTRO_TAC Terminal.ITER_vv_rho_node1 [`v`;`k`];
620 ASM_REWRITE_TAC[LET_THM];
621 TYPIFY_GOAL_THEN `3 <= k` (unlist REWRITE_TAC);
622 BY(ASM_MESON_TAC[arith `3 < k ==> 3 <= k`]);
624 INTRO_TAC (GEN_ALL Odxlstcv2.CARD_V_EQ_SCS_K1) [`s`;`v`;`V`;`k`];
627 TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
628 MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
629 BY(ASM_REWRITE_TAC[]);
630 TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
633 MATCH_MP_TAC FUN_IN_IMAGE;
634 BY(REWRITE_TAC[IN_UNIV]);
635 INTRO_TAC (GENL [`v0:real^3`;`vv:num->real^3`;`i:num`] Local_lemmas.EGHNAVX) [`v p`;`\ (i:num). v (p + i)`];
636 REWRITE_TAC[RIGHT_FORALL_IMP_THM;GSYM RIGHT_AND_FORALL_THM];
641 (REWRITE_TAC[IN_IMAGE;IN_UNIV]);
645 REPEAT WEAKER_STRIP_TAC;
647 INTRO_TAC (GSYM Ocbicby.INTERIOR_ANGLE1_AZIM) [`s`;`v`];
648 ASM_REWRITE_TAC[LET_THM];
649 TYPIFY_GOAL_THEN `v IN BBs_v39 s` (unlist REWRITE_TAC);
650 BY(ASM_REWRITE_TAC[IN]);
652 COMMENT "first conjunct";
654 REPEAT WEAKER_STRIP_TAC;
655 FIRST_X_ASSUM_ST `SUBSET` (C INTRO_TAC [`q`]);
657 REPEAT WEAKER_STRIP_TAC;
660 FIRST_X_ASSUM (C INTRO_TAC [`j`]);
662 BY(REWRITE_TAC[arith `SUC (p+j) = p+j+1 /\ ((p+j) + k - 1 = p+j+k-1)`]);
664 FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_ELIM_THM];
665 DISCH_THEN (C INTRO_TAC [`v (p+(j:num))`]);
666 DISCH_THEN MATCH_MP_TAC;
667 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
668 REPEAT WEAKER_STRIP_TAC;
669 FIRST_X_ASSUM_ST `SUBSET` (C INTRO_TAC [`q`]);
671 REPEAT WEAKER_STRIP_TAC;
674 FIRST_X_ASSUM (C INTRO_TAC [`j`]);
676 BY(REWRITE_TAC[arith `SUC (p+j) = p+j+1 /\ ((p+j) + k - 1 = p+j+k-1)`]);
677 FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_ELIM_THM];
678 DISCH_THEN (C INTRO_TAC [`v (p+(j:num))`]);
679 DISCH_THEN MATCH_MP_TAC;
680 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[])
684 let EGHNAVX_SCS = prove_by_refinement(
686 (let bta = (\j. azim (vec 0) (v p) (v (p+1)) (v (p+j))) in
687 ( is_scs_v39 s /\ scs_k_v39 s = k /\
694 (!i j. i < j /\ j < k ==> bta i <= bta j) /\
695 (!q j. bta q = &0 /\ 0 < j /\ j <= q /\ q < k
696 ==> (j<q ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v (p+j+k-1)) = pi) /\
697 v (p+j) IN aff_gt {vec 0,v p} {v (p+1)}) /\
698 (!q j. bta q = bta (k - 1) /\ 0 < q /\ q < k - 1 /\ q <= j /\ j < k
699 ==> (q < j ==> azim (vec 0) (v (p+j)) (v (p+j+1)) (v(p+j+k-1)) = pi) /\
700 v(p+j) IN aff_gt {vec 0, v p} {v (p + k - 1)})))`,
703 REWRITE_TAC[LET_THM];
704 REPEAT WEAKER_STRIP_TAC;
705 MATCH_MP_TAC (REWRITE_RULE[LET_THM] EGHNAVX_COLL_SCS);
706 TYPIFY `s` EXISTS_TAC;
708 REPEAT WEAKER_STRIP_TAC;
709 FIRST_X_ASSUM_ST `scs_generic` MP_TAC;
710 REWRITE_TAC[Appendix.scs_generic];
712 TYPED_ABBREV_TAC `FF = IMAGE (\i. (v i,v (SUC i))) (:num)`;
713 TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
714 TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
715 TYPIFY `convex_local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
716 BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN ASM_MESON_TAC[arith `3 < k ==> ~(k<= 3)`]);
717 TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
718 MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
719 BY(ASM_REWRITE_TAC[]);
720 TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
723 MATCH_MP_TAC FUN_IN_IMAGE;
724 BY(REWRITE_TAC[IN_UNIV]);
725 BY(ASM_MESON_TAC[Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN])
729 let coplanar_cross_reduction = prove_by_refinement(
731 is_scs_v39 s /\ scs_k_v39 s = k /\
736 coplanar {vec 0,v i, v(i+1),v(i+2)} ==>
737 (v(i+1) cross v i) dot (v(i+2) cross v i) > &0`,
740 REPEAT WEAKER_STRIP_TAC;
741 TYPIFY `~(k=0)` (C SUBGOAL_THEN ASSUME_TAC);
742 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
743 TYPED_ABBREV_TAC `FF = IMAGE (\i. (v i,v (SUC i))) (:num)`;
744 TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
745 TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
746 FIRST_ASSUM_ST `coplanar` MP_TAC;
747 REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
749 TYPIFY `~coplanar ({vec 0} UNION V)` (C SUBGOAL_THEN ASSUME_TAC);
751 MATCH_MP_TAC Fektyiy.FEKTYIY;
752 TYPIFY `s` EXISTS_TAC;
753 BY(ASM_REWRITE_TAC[IN]);
754 TYPIFY `BBprime2_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
755 BY(ASM_MESON_TAC[Appendix.scs_basic;Ayqjtmd.unadorned_MMs]);
756 TYPIFY `BBprime_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
757 BY(ASM_MESON_TAC[Appendix.BBprime2_v39]);
758 TYPIFY `BBs_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
759 BY(ASM_MESON_TAC[Appendix.BBprime_v39]);
760 INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`k`];
763 TYPIFY `periodic v k /\ convex_local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
764 BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN ASM_MESON_TAC[arith `3 < k ==> ~(k<= 3)`]);
765 INTRO_TAC Terminal.ITER_vv_rho_node1 [`v`;`k`];
766 ASM_REWRITE_TAC[LET_THM];
767 ASM_SIMP_TAC[arith `3 < k ==> 3 <= k`];
769 INTRO_TAC (GEN_ALL Odxlstcv2.CARD_V_EQ_SCS_K1) [`s`;`v`;`V`;`k`];
772 TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
773 MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
774 BY(ASM_REWRITE_TAC[]);
775 TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
778 MATCH_MP_TAC FUN_IN_IMAGE;
779 BY(REWRITE_TAC[IN_UNIV]);
780 TYPIFY `!i j. ~(v i = v j) ==> ~collinear {vec 0, v i, v j}` (C SUBGOAL_THEN ASSUME_TAC);
781 INTRO_TAC Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN [`V`;`E`;`FF`];
782 BY(ASM_MESON_TAC[Appendix.scs_generic]);
783 INTRO_TAC EGHNAVX_SCS [`s`;`k`;`v`;`i`];
784 REWRITE_TAC[LET_THM];
786 REPEAT WEAKER_STRIP_TAC;
787 COMMENT "insert here";
788 TYPIFY `!a. 0 < a /\ (a:num) < k ==> ~(v i = v (i+a))` (C SUBGOAL_THEN ASSUME_TAC);
789 TYPIFY `!i. v (i MOD k) = v i` (C SUBGOAL_THEN ASSUME_TAC);
791 MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
792 BY(ASM_MESON_TAC[arith `3 < k ==> ~(0=k)`]);
793 FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
794 GEN_TAC THEN DISCH_TAC;
795 TYPIFY_GOAL_THEN `!i j. i < k /\ j < (k:num) /\ ~(i = j) ==> ~(v i = v j)` MATCH_MP_TAC;
797 REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC;
798 BY(ASM_MESON_TAC[DIVISION]);
799 TYPIFY `i MOD k = (i+0) MOD k` (C SUBGOAL_THEN SUBST1_TAC);
800 BY(REWRITE_TAC[arith `i + 0 = i`]);
801 GMATCH_SIMP_TAC Ocbicby.MOD_EQ_MOD_SHIFT;
802 REPEAT (GMATCH_SIMP_TAC MOD_LT);
803 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
804 FIRST_X_ASSUM DISJ_CASES_TAC;
805 FIRST_X_ASSUM_ST `&0` (C INTRO_TAC [`2`;`2`]);
806 ASM_REWRITE_TAC[arith `0 < 2 /\ 2 <= 2 /\ ~(2 < 2)`];
808 BY(MATCH_MP_TAC (arith `3 < k ==> 2 < k`) THEN ASM_REWRITE_TAC[]);
809 GMATCH_SIMP_TAC Local_lemmas1.COLL_AFF_GT_2_1;
811 FIRST_X_ASSUM MATCH_MP_TAC;
812 FIRST_X_ASSUM MATCH_MP_TAC;
813 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
815 REWRITE_TAC[IN_ELIM_THM];
816 REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[CROSS_LMUL;CROSS_LADD;DOT_RMUL;DOT_RADD;CROSS_LZERO;DOT_RZERO;CROSS_REFL];
817 REWRITE_TAC[arith `t1 * &0 + x = x`;arith `x > &0 <=> &0 < x`];
818 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
820 REWRITE_TAC[DOT_POS_LT];
821 REWRITE_TAC[CROSS_EQ_0];
822 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
823 BY(ASM_REWRITE_TAC[]);
824 COMMENT "second conj";
825 FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`2`]);
826 FIRST_X_ASSUM_ST `aff_gt` kill;
827 FIRST_X_ASSUM_ST `0 < a` MP_TAC THEN BURY_MP_TAC;
828 FIRST_X_ASSUM (C INTRO_TAC [`2`;`k-1`]);
830 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
832 TYPIFY_GOAL_THEN `azim (vec 0) (v i) (v (i + 1)) (v (i + 2)) = azim (vec 0) (v i) (v (i + 1)) (v (i + k - 1))` (unlist REWRITE_TAC);
833 BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
836 TYPIFY `V SUBSET affine hull {vec 0,v i,v (i+k-1)}` ENOUGH_TO_SHOW_TAC;
837 DISCH_TAC THEN FIRST_X_ASSUM_ST `coplanar` MP_TAC THEN REWRITE_TAC[coplanar];
838 GEXISTL_TAC [`(vec 0):real^3`;`v i`;`v (i+k-1)`];
839 FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_UNION;IN_SING];
840 TYPIFY `vec 0 IN affine hull {vec 0,v i ,v(i+k-1)}` ENOUGH_TO_SHOW_TAC;
842 MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
844 TYPIFY `!w. w IN IMAGE v (i..i + k - 1) ==> w IN affine hull {vec 0,v i , v(i+k-1)}` ENOUGH_TO_SHOW_TAC;
845 GMATCH_SIMP_TAC (GSYM Oxl_2012.PERIODIC_IMAGE_EQUAL);
848 INTRO_TAC Oxl_def.periodic_numseg [`(\j. v j IN affine hull {vec 0,v i,v (i+k-1)})`;`k`];
852 FIRST_X_ASSUM_ST `periodic` MP_TAC THEN REWRITE_TAC[Oxl_def.periodic];
854 REPEAT WEAKER_STRIP_TAC;
855 FIRST_X_ASSUM MATCH_MP_TAC;
856 MATCH_MP_TAC FUN_IN_IMAGE;
857 BY(ASM_REWRITE_TAC[]);
860 REWRITE_TAC[IMAGE;IN_UNIV;SUBSET;IN_ELIM_THM];
861 BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
862 REWRITE_TAC[IN_IMAGE;IN_NUMSEG];
863 REPEAT WEAKER_STRIP_TAC;
865 TYPIFY `?j. 0 <= j /\ j < k /\ x = i + j` (C SUBGOAL_THEN MP_TAC);
866 TYPIFY `x - (i:num)` EXISTS_TAC;
867 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
868 REPEAT WEAKER_STRIP_TAC;
870 TYPIFY `!j. 2 <= j /\ j < k==> v (i + j) IN affine hull {vec 0,v i, v(i+k-1)}` (C SUBGOAL_THEN ASSUME_TAC);
871 REPEAT WEAKER_STRIP_TAC;
872 FIRST_X_ASSUM (C INTRO_TAC [`j'`]);
874 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
875 TYPIFY `aff_gt {vec 0,v i} {v (i+k-1)} SUBSET affine hull {vec 0,v i,v (i+k-1)}` ENOUGH_TO_SHOW_TAC;
877 TYPIFY `{vec 0,v i,v (i+k-1)} = {vec 0,v i} UNION {v (i+k-1)}` (C SUBGOAL_THEN SUBST1_TAC);
879 BY(REWRITE_TAC[ AFF_GT_SUBSET_AFFINE_HULL]);
880 TYPIFY `{vec 0,v i, v (i+2)} SUBSET affine hull {vec 0, v i, v (i+k-1)}` (C SUBGOAL_THEN ASSUME_TAC);
881 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
882 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
883 MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
885 MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
887 FIRST_X_ASSUM MATCH_MP_TAC;
888 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
889 INTRO_TAC AFFINE_HULL_3_GENERATED [`{vec 0, v i, v (i + 2)}`;`(vec 0):real^3`;`v i`;`v (i+k-1)`];
892 FIRST_X_ASSUM MATCH_MP_TAC;
893 FIRST_X_ASSUM MATCH_MP_TAC;
894 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
896 ASSUME_TAC (arith ` 2 <= j \/ j = 0 \/ j = 1` );
897 REPEAT (POP_ASSUM DISJ_CASES_TAC);
899 ASM_REWRITE_TAC[arith `i + 0 = i`] THEN MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
902 (FIRST_X_ASSUM_ST `coplanar (a INSERT X)` MP_TAC);
903 REWRITE_TAC[coplanar] THEN REPEAT WEAKER_STRIP_TAC;
904 INTRO_TAC AFFINE_HULL_3_GENERATED [`{vec 0, v i, v (i + 2)}`;`u`;`v'`;`w'`];
907 BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
908 FIRST_X_ASSUM MATCH_MP_TAC;
909 FIRST_X_ASSUM MATCH_MP_TAC;
910 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
911 BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[])
915 let coplanar_aff_gt_simple = prove_by_refinement(
917 is_scs_v39 s /\ scs_k_v39 s = k /\
921 (!j. ~(v j = v i) ==> ~collinear {vec 0,v i,v j}) /\
922 coplanar {vec 0,v i, v(i+1),v(i+2)} ==>
923 v (i+1) IN aff_gt {vec 0} {v i, v(i+2)}`,
926 REPEAT WEAKER_STRIP_TAC;
927 TYPIFY `~(k=0)` (C SUBGOAL_THEN ASSUME_TAC);
928 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
929 TYPED_ABBREV_TAC `FF = IMAGE (\i. (v i,v (SUC i))) (:num)`;
930 TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
931 TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
932 FIRST_ASSUM_ST `coplanar` MP_TAC;
933 REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
935 TYPIFY `~coplanar ({vec 0} UNION V)` (C SUBGOAL_THEN ASSUME_TAC);
937 MATCH_MP_TAC Fektyiy.FEKTYIY;
938 TYPIFY `s` EXISTS_TAC;
939 BY(ASM_REWRITE_TAC[IN]);
940 TYPIFY `BBprime2_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
941 BY(ASM_MESON_TAC[Appendix.scs_basic;Ayqjtmd.unadorned_MMs]);
942 TYPIFY `BBprime_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
943 BY(ASM_MESON_TAC[Appendix.BBprime2_v39]);
944 TYPIFY `BBs_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
945 BY(ASM_MESON_TAC[Appendix.BBprime_v39]);
946 INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`k`];
949 TYPIFY `periodic v k /\ convex_local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
950 BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN ASM_MESON_TAC[arith `3 < k ==> ~(k<= 3)`]);
951 INTRO_TAC Terminal.ITER_vv_rho_node1 [`v`;`k`];
952 ASM_REWRITE_TAC[LET_THM];
953 ASM_SIMP_TAC[arith `3 < k ==> 3 <= k`];
955 INTRO_TAC (GEN_ALL Odxlstcv2.CARD_V_EQ_SCS_K1) [`s`;`v`;`V`;`k`];
958 TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
959 MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
960 BY(ASM_REWRITE_TAC[]);
961 TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
964 MATCH_MP_TAC FUN_IN_IMAGE;
965 BY(REWRITE_TAC[IN_UNIV]);
966 INTRO_TAC EGHNAVX_COLL_SCS [`s`;`k`;`v`;`i`];
967 REWRITE_TAC[LET_THM];
969 REPEAT WEAKER_STRIP_TAC;
970 TYPIFY `!a. 0 < a /\ (a:num) < k ==> ~(v i = v (i+a))` (C SUBGOAL_THEN ASSUME_TAC);
971 TYPIFY `!i. v (i MOD k) = v i` (C SUBGOAL_THEN ASSUME_TAC);
973 MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
974 BY(ASM_MESON_TAC[arith `3 < k ==> ~(0=k)`]);
975 FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
976 GEN_TAC THEN DISCH_TAC;
977 TYPIFY_GOAL_THEN `!i j. i < k /\ j < (k:num) /\ ~(i = j) ==> ~(v i = v j)` MATCH_MP_TAC;
979 REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC;
980 BY(ASM_MESON_TAC[DIVISION]);
981 TYPIFY `i MOD k = (i+0) MOD k` (C SUBGOAL_THEN SUBST1_TAC);
982 BY(REWRITE_TAC[arith `i + 0 = i`]);
983 GMATCH_SIMP_TAC Ocbicby.MOD_EQ_MOD_SHIFT;
984 REPEAT (GMATCH_SIMP_TAC MOD_LT);
985 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
986 FIRST_X_ASSUM DISJ_CASES_TAC;
987 FIRST_X_ASSUM_ST `&0` (C INTRO_TAC [`2`;`2`]);
991 BY(MATCH_MP_TAC (arith `3 < k ==> 2 < k`) THEN ASM_REWRITE_TAC[]);
992 GMATCH_SIMP_TAC Local_lemmas1.COLL_AFF_GT_2_1;
993 GMATCH_SIMP_TAC AFF_GT_1_2;
994 REWRITE_TAC[IN_ELIM_THM;arith `t % vec 0 + a = a`];
996 ONCE_REWRITE_TAC[DISJOINT_SYM];
997 MATCH_MP_TAC Fan.th3a;
998 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {c,a,b}`] THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC);
999 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN FIRST_X_ASSUM MATCH_MP_TAC;
1000 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1003 FIRST_X_ASSUM MATCH_MP_TAC;
1004 ONCE_REWRITE_TAC[EQ_SYM_EQ];
1005 FIRST_X_ASSUM MATCH_MP_TAC;
1006 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1007 REPEAT WEAKER_STRIP_TAC;
1008 GEXISTL_TAC [`&1 + t2 / t3 - &1 / t3`;`-- t2 / t3`;`&1 / t3`];
1010 GMATCH_SIMP_TAC REAL_LT_DIV;
1011 GMATCH_SIMP_TAC REAL_LT_DIV;
1012 ASM_REWRITE_TAC[arith `&0 < &1`];
1014 TYPIFY `--t2 / t3 % v i + &1 / t3 % (t2 % v i + t3 % v (i + 1)) = (-- t2 / t3 + (&1 / t3) * t2) % v i + ((&1 / t3)*t3) % v (i+1) ` (C SUBGOAL_THEN SUBST1_TAC);
1015 BY(VECTOR_ARITH_TAC);
1016 TYPIFY_GOAL_THEN `(--t2 / t3 + &1 / t3 * t2) = &0 /\ (&1 / t3 * t3 = &1)` (unlist REWRITE_TAC);
1017 BY(CONJ_TAC THEN Calc_derivative.CALC_ID_TAC THEN (REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC)) THEN REAL_ARITH_TAC);
1018 BY(VECTOR_ARITH_TAC);
1020 BY(Calc_derivative.CALC_ID_TAC THEN REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1021 TYPIFY `~(&0 <= t2)` ENOUGH_TO_SHOW_TAC;
1022 BY(REPLICATE_TAC 2 (POP_ASSUM MP_TAC) THEN MESON_TAC[arith `~(&0 <= t2) ==> &0 < -- t2`]);
1024 INTRO_TAC (GEN_ALL Local_lemmas.FAN_IN_AFF_GE_IMP_EQ) [`V`;`E`;`(vec 0):real^3`;`v i`;`v (i+2)`;`v (i+1)`];
1027 MATCH_MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
1028 BY(ASM_REWRITE_TAC[]);
1031 MATCH_MP_TAC FUN_IN_IMAGE;
1032 BY(REWRITE_TAC[IN_UNIV]);
1035 BY(REWRITE_TAC[arith `i+1 = SUC i`;IN_IMAGE;IN_UNIV] THEN MESON_TAC[]);
1036 GMATCH_SIMP_TAC AFF_GE_1_2;
1037 REWRITE_TAC[IN_ELIM_THM];
1039 ONCE_REWRITE_TAC[DISJOINT_SYM];
1040 MATCH_MP_TAC Fan.th3a;
1041 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {c,a,b}`] THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC);
1042 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN FIRST_X_ASSUM MATCH_MP_TAC;
1043 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1044 GEXISTL_TAC [`t1`;`t2`;`t3`];
1045 FIRST_X_ASSUM_ST `i+2` SUBST1_TAC;
1046 REWRITE_TAC[CONJ_ASSOC] THEN CONJ2_TAC;
1047 BY(VECTOR_ARITH_TAC);
1048 BY(REPLICATE_TAC 6 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1049 REWRITE_TAC[DE_MORGAN_THM];
1051 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN FIRST_X_ASSUM MATCH_MP_TAC;
1052 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1053 ONCE_REWRITE_TAC[EQ_SYM_EQ];
1054 MATCH_MP_TAC Hypermap_iso.fan_in_e_imp_neq;
1055 GEXISTL_TAC [`V`;`E`];
1057 MATCH_MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
1058 BY(ASM_REWRITE_TAC[]);
1060 BY(REWRITE_TAC[arith `i+2 = SUC (i+1)`;IN_IMAGE;IN_UNIV] THEN MESON_TAC[]);
1061 COMMENT "second disj";
1062 FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`2`]);
1063 FIRST_X_ASSUM_ST `aff_gt` kill;
1064 FIRST_X_ASSUM_ST `0 < a` MP_TAC THEN BURY_MP_TAC;
1065 FIRST_X_ASSUM (C INTRO_TAC [`2`;`k-1`]);
1067 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1069 TYPIFY_GOAL_THEN `azim (vec 0) (v i) (v (i + 1)) (v (i + 2)) = azim (vec 0) (v i) (v (i + 1)) (v (i + k - 1))` (unlist REWRITE_TAC);
1070 BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1073 TYPIFY `V SUBSET affine hull {vec 0,v i,v (i+k-1)}` ENOUGH_TO_SHOW_TAC;
1074 DISCH_TAC THEN FIRST_X_ASSUM_ST `coplanar` MP_TAC THEN REWRITE_TAC[coplanar];
1075 GEXISTL_TAC [`(vec 0):real^3`;`v i`;`v (i+k-1)`];
1076 FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET;IN_UNION;IN_SING];
1077 TYPIFY `vec 0 IN affine hull {vec 0,v i ,v(i+k-1)}` ENOUGH_TO_SHOW_TAC;
1079 MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
1081 TYPIFY `!w. w IN IMAGE v (i..i + k - 1) ==> w IN affine hull {vec 0,v i , v(i+k-1)}` ENOUGH_TO_SHOW_TAC;
1082 GMATCH_SIMP_TAC (GSYM Oxl_2012.PERIODIC_IMAGE_EQUAL);
1085 INTRO_TAC Oxl_def.periodic_numseg [`(\j. v j IN affine hull {vec 0,v i,v (i+k-1)})`;`k`];
1089 FIRST_X_ASSUM_ST `periodic` MP_TAC THEN REWRITE_TAC[Oxl_def.periodic];
1091 REPEAT WEAKER_STRIP_TAC;
1092 FIRST_X_ASSUM MATCH_MP_TAC;
1093 MATCH_MP_TAC FUN_IN_IMAGE;
1094 BY(ASM_REWRITE_TAC[]);
1097 REWRITE_TAC[IMAGE;IN_UNIV;SUBSET;IN_ELIM_THM];
1098 BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
1099 REWRITE_TAC[IN_IMAGE;IN_NUMSEG];
1100 REPEAT WEAKER_STRIP_TAC;
1102 TYPIFY `?j. 0 <= j /\ j < k /\ x = i + j` (C SUBGOAL_THEN MP_TAC);
1103 TYPIFY `x - (i:num)` EXISTS_TAC;
1104 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1105 REPEAT WEAKER_STRIP_TAC;
1107 TYPIFY `!j. 2 <= j /\ j < k==> v (i + j) IN affine hull {vec 0,v i, v(i+k-1)}` (C SUBGOAL_THEN ASSUME_TAC);
1108 REPEAT WEAKER_STRIP_TAC;
1109 FIRST_X_ASSUM (C INTRO_TAC [`j'`]);
1111 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
1112 TYPIFY `aff_gt {vec 0,v i} {v (i+k-1)} SUBSET affine hull {vec 0,v i,v (i+k-1)}` ENOUGH_TO_SHOW_TAC;
1114 TYPIFY `{vec 0,v i,v (i+k-1)} = {vec 0,v i} UNION {v (i+k-1)}` (C SUBGOAL_THEN SUBST1_TAC);
1116 BY(REWRITE_TAC[ AFF_GT_SUBSET_AFFINE_HULL]);
1117 TYPIFY `{vec 0,v i, v (i+2)} SUBSET affine hull {vec 0, v i, v (i+k-1)}` (C SUBGOAL_THEN ASSUME_TAC);
1118 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
1119 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
1120 MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
1122 MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
1124 FIRST_X_ASSUM MATCH_MP_TAC;
1125 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1126 INTRO_TAC AFFINE_HULL_3_GENERATED [`{vec 0, v i, v (i + 2)}`;`(vec 0):real^3`;`v i`;`v (i+k-1)`];
1129 FIRST_X_ASSUM MATCH_MP_TAC;
1130 ONCE_REWRITE_TAC[EQ_SYM_EQ];
1131 FIRST_X_ASSUM MATCH_MP_TAC;
1132 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1133 INTRO_TAC AFFINE_HULL_3_GENERATED [`{vec 0, v i, v (i + 2)}`;`(vec 0):real^3`;`v i`;`v (i+k-1)`];
1136 FIRST_X_ASSUM MATCH_MP_TAC;
1137 ONCE_REWRITE_TAC[EQ_SYM_EQ];
1138 FIRST_X_ASSUM MATCH_MP_TAC;
1139 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1141 ASSUME_TAC (arith ` 2 <= j \/ j = 0 \/ j = 1` );
1142 REPEAT (POP_ASSUM DISJ_CASES_TAC);
1143 BY(ASM_MESON_TAC[]);
1144 ASM_REWRITE_TAC[arith `i + 0 = i`] THEN MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
1147 (FIRST_X_ASSUM_ST `coplanar (a INSERT X)` MP_TAC);
1148 REWRITE_TAC[coplanar] THEN REPEAT WEAKER_STRIP_TAC;
1149 INTRO_TAC AFFINE_HULL_3_GENERATED [`{vec 0, v i, v (i + 2)}`;`u`;`v'`;`w'`];
1152 BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
1153 FIRST_X_ASSUM MATCH_MP_TAC;
1154 ONCE_REWRITE_TAC[EQ_SYM_EQ];
1155 FIRST_X_ASSUM MATCH_MP_TAC;
1156 BY(FIRST_X_ASSUM_ST `3 < k` MP_TAC THEN ARITH_TAC);
1157 BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[])
1162 let a5_assumption_reduction = prove_by_refinement(
1167 (!i j. scs_diag 5 i j ==> scs_a_v39 s i j < dist(v i,v j)) /\
1168 deformation f (IMAGE v (:num)) (--e,e) /\
1169 (!w t. ~(w = v 0) /\ ~(w = v 1) ==> (f w t = w)) /\
1170 (?e1. &0 < e1 /\ (!t. abs t < e1 ==> dist(f (v 1) t,v 2) = dist(v 1,v 2) /\ dist(f (v 0) t,v 4) = dist(v 0,v 4))) /\
1171 (?e1. &0 < e1 /\ (!t. abs t < e1 ==> scs_a_v39 s 0 1 <= dist(f (v 0) t,f (v 1) t)))
1173 (!i j. ?e1. &0 < e1 /\ (scs_a_v39 s i j = dist(v i,v j) ==>
1174 (!t. abs t < e1 ==> scs_a_v39 s i j <= dist(f (v i) t,f (v j) t))))
1178 REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC Cuxvzoz.I_IMP THEN ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
1179 TYPIFY `!i j.scs_a_v39 s (i MOD 5) (j MOD 5) = scs_a_v39 s i j /\ scs_b_v39 s (i MOD 5) (j MOD 5) = scs_b_v39 s i j ` (C SUBGOAL_THEN ASSUME_TAC);
1180 FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC;
1181 ASM_REWRITE_TAC[Appendix.is_scs_v39];
1182 REPEAT WEAKER_STRIP_TAC;
1183 BY(REPEAT (FIRST_X_ASSUM_ST `periodic2` MP_TAC) THEN MESON_TAC[Cuxvzoz.periodic2_MOD;arith `~(5 = 0)`]);
1184 TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
1185 BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
1186 TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
1188 MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
1189 BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
1190 INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
1193 TYPIFY `!j. j < 5 ==> (j MOD 5 = j)` (C SUBGOAL_THEN ASSUME_TAC);
1194 BY(REWRITE_TAC[MOD_LT]);
1195 COMMENT "scs_a_v39";
1197 MATCH_MP_TAC Terminal.periodic2_mod_reduce;
1198 TYPIFY `5` EXISTS_TAC;
1199 ASM_REWRITE_TAC[arith `~(5=0)`];
1201 MATCH_MP_TAC Cuxvzoz.MOD_periodic2;
1202 BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[] THEN MESON_TAC[arith `~(5=0)`]);
1203 TYPIFY_GOAL_THEN `!P. (!i j. P i j ==> P j i) /\ (!i j. (i <= (j:num)) ==> P i j) ==> (!i j. P i j)` MATCH_MP_TAC;
1204 BY(MESON_TAC[arith `i <= j \/ j <= (i:num)`]);
1206 REPEAT WEAKER_STRIP_TAC;
1207 ONCE_REWRITE_TAC[DIST_SYM];
1208 TYPIFY `scs_a_v39 s j i = scs_a_v39 s i j` (C SUBGOAL_THEN SUBST1_TAC);
1209 FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC THEN REWRITE_TAC[Appendix.is_scs_v39] THEN REPEAT WEAKER_STRIP_TAC;
1210 BY(ASM_MESON_TAC[]);
1211 FIRST_X_ASSUM MATCH_MP_TAC;
1212 BY(ASM_REWRITE_TAC[]);
1213 TYPIFY `!t. f (v 2) t = v 2 /\ f (v 3) t = v 3 /\ f (v 4) t = v 4` (C SUBGOAL_THEN ASSUME_TAC);
1214 BY(ASM_MESON_TAC[arith `0 < 5 /\ 1 < 5 /\ 2 < 5 /\ 3 < 5 /\ 4 < 5 /\ ~(2 = 0) /\ ~(2 = 1) /\ ~(3 = 0) /\ ~(3 = 1) /\ ~(4 =0) /\ ~(4=1)`]);
1215 REWRITE_TAC[arith `i < 5 <=> (i = 0) \/ (i = 1) \/ (i=2) \/ (i =3) \/ (i=4)`];
1216 TYPIFY `scs_diag 5 0 2 /\ scs_diag 5 0 3 /\ scs_diag 5 1 3 /\ scs_diag 5 1 4 /\ scs_diag 5 2 4` (C SUBGOAL_THEN ASSUME_TAC);
1217 BY(REWRITE_TAC[Appendix.scs_diag;Uxckfpe.ARITH_5_TAC]);
1218 ONCE_REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (b ==> a ==> c)`];
1219 TYPIFY `!i j. scs_diag 5 i j ==> (?e1. &0 < e1 /\ (scs_a_v39 s i j = dist (v i,v j) ==> (!t. abs t < e1 ==> scs_a_v39 s i j <= dist (f (v i) t,f (v j) t))))` (C SUBGOAL_THEN ASSUME_TAC);
1220 BY(ASM_MESON_TAC[arith `x < y ==> ~(x = y)`]);
1221 TYPIFY `!i. T ==> (?e1. &0 < e1 /\ (scs_a_v39 s i i = dist (v i,v i) ==> (!t. abs t < e1 ==> scs_a_v39 s i i <= dist (f (v i) t,f (v i) t))))` (C SUBGOAL_THEN ASSUME_TAC);
1222 REWRITE_TAC[DIST_REFL];
1223 BY(MESON_TAC[arith `x = &0 ==> x <= &0`;arith `&0 < &1`]);
1225 TYPIFY `(?e1. &0 < e1 /\ (scs_a_v39 s 0 1 = dist (v 0,v 1) ==> (!t. abs t < e1 ==> scs_a_v39 s 0 1 <= dist (f (v 0) t,f (v 1) t)))) /\ (?e1. &0 < e1 /\ (scs_a_v39 s 1 2 = dist (v 1,v 2) ==> (!t. abs t < e1 ==> scs_a_v39 s 1 2 <= dist (f (v 1) t,f (v 2) t)))) /\ (?e1. &0 < e1 /\ (scs_a_v39 s 2 3 = dist (v 2,v 3) ==> (!t. abs t < e1 ==> scs_a_v39 s 2 3 <= dist (f (v 2) t,f (v 3) t)))) /\ (?e1. &0 < e1 /\ (scs_a_v39 s 3 4 = dist (v 3,v 4) ==> (!t. abs t < e1 ==> scs_a_v39 s 3 4 <= dist (f (v 3) t,f (v 4) t)))) /\ (?e1. &0 < e1 /\ (scs_a_v39 s 0 4 = dist (v 0,v 4) ==> (!t. abs t < e1 ==> scs_a_v39 s 0 4 <= dist (f (v 0) t,f (v 4) t))))` (C SUBGOAL_THEN MP_TAC);
1227 TYPIFY_GOAL_THEN `!a b. (?e1. &0 < e1 /\ (a = b ==> (!t. abs t < e1 ==> a <= b)))` (unlist REWRITE_TAC);
1228 BY(MESON_TAC[arith `&0 < &1`;arith `(a = b) ==> (a <= b)`]);
1230 BY(ASM_MESON_TAC[]);
1231 BY(ASM_MESON_TAC[arith `x = y ==> x <= y`]);
1232 REWRITE_TAC[LEFT_OR_DISTRIB;RIGHT_OR_DISTRIB;GSYM DISJ_ASSOC];
1233 ONCE_REWRITE_TAC[TAUT `(a1 /\ a2 /\ a3 /\ a4 /\ a5) <=> ((T ==> a1) /\ (T ==> a2) /\ (T ==> a3) /\ (T ==> a4) /\ (T ==> a5))`];
1234 REPEAT WEAKER_STRIP_TAC;
1235 FIRST_X_ASSUM MP_TAC;
1236 BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN FIRST_X_ASSUM (unlist REWRITE_TAC) THEN NUM_REDUCE_TAC THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[])
1241 let a5_assumption_reduction = prove_by_refinement(
1246 (!i j. scs_diag 5 i j ==> scs_a_v39 s i j < dist(v i,v j)) /\
1247 deformation f (IMAGE v (:num)) (--e,e) /\
1248 (!w t. ~(w = v 4) /\ ~(w = v 0) ==> (f w t = w)) /\
1249 (?e1. &0 < e1 /\ (!t. abs t < e1 ==> dist(f (v 4) t,f (v 0) t) = dist(v 4,v 0) /\ dist(f (v 4) t,v 3) = dist(v 4,v 3))) /\
1250 (?e1. &0 < e1 /\ (!t. abs t < e1 ==> scs_a_v39 s 0 1 <= dist(f (v 0) t,v 1)))
1252 (!i j. ?e1. &0 < e1 /\ (scs_a_v39 s i j = dist(v i,v j) ==>
1253 (!t. abs t < e1 ==> scs_a_v39 s i j <= dist(f (v i) t,f (v j) t))))
1257 REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC Cuxvzoz.I_IMP THEN ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
1258 TYPIFY `!i j.scs_a_v39 s (i MOD 5) (j MOD 5) = scs_a_v39 s i j /\ scs_b_v39 s (i MOD 5) (j MOD 5) = scs_b_v39 s i j ` (C SUBGOAL_THEN ASSUME_TAC);
1259 FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC;
1260 ASM_REWRITE_TAC[Appendix.is_scs_v39];
1261 REPEAT WEAKER_STRIP_TAC;
1262 BY(REPEAT (FIRST_X_ASSUM_ST `periodic2` MP_TAC) THEN MESON_TAC[Cuxvzoz.periodic2_MOD;arith `~(5 = 0)`]);
1263 TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
1264 BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
1265 TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
1267 MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
1268 BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
1269 INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
1272 TYPIFY `!j. j < 5 ==> (j MOD 5 = j)` (C SUBGOAL_THEN ASSUME_TAC);
1273 BY(REWRITE_TAC[MOD_LT]);
1274 COMMENT "scs_a_v39";
1276 MATCH_MP_TAC Terminal.periodic2_mod_reduce;
1277 TYPIFY `5` EXISTS_TAC;
1278 ASM_REWRITE_TAC[arith `~(5=0)`];
1280 MATCH_MP_TAC Cuxvzoz.MOD_periodic2;
1281 BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[] THEN MESON_TAC[arith `~(5=0)`]);
1282 TYPIFY_GOAL_THEN `!P. (!i j. P i j ==> P j i) /\ (!i j. (i <= (j:num)) ==> P i j) ==> (!i j. P i j)` MATCH_MP_TAC;
1283 BY(MESON_TAC[arith `i <= j \/ j <= (i:num)`]);
1285 REPEAT WEAKER_STRIP_TAC;
1286 ONCE_REWRITE_TAC[DIST_SYM];
1287 TYPIFY `scs_a_v39 s j i = scs_a_v39 s i j` (C SUBGOAL_THEN SUBST1_TAC);
1288 FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC THEN REWRITE_TAC[Appendix.is_scs_v39] THEN REPEAT WEAKER_STRIP_TAC;
1289 BY(ASM_MESON_TAC[]);
1290 FIRST_X_ASSUM MATCH_MP_TAC;
1291 BY(ASM_REWRITE_TAC[]);
1292 TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(i=j) ==> ~(v i = v j)` (C SUBGOAL_THEN ASSUME_TAC);
1293 BY(ASM_MESON_TAC[]);
1294 TYPIFY `!t. f (v 2) t = v 2 /\ f (v 3) t = v 3 /\ f (v 1) t = v 1` (C SUBGOAL_THEN ASSUME_TAC);
1295 BY(GEN_TAC THEN REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC THEN REPEAT CONJ_TAC) THEN NUM_REDUCE_TAC);
1296 REWRITE_TAC[arith `i < 5 <=> (i = 0) \/ (i = 1) \/ (i=2) \/ (i =3) \/ (i=4)`];
1297 TYPIFY `scs_diag 5 0 2 /\ scs_diag 5 0 3 /\ scs_diag 5 1 3 /\ scs_diag 5 1 4 /\ scs_diag 5 2 4` (C SUBGOAL_THEN ASSUME_TAC);
1298 BY(REWRITE_TAC[Appendix.scs_diag;Uxckfpe.ARITH_5_TAC]);
1299 ONCE_REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (b ==> a ==> c)`];
1300 TYPIFY `!i j. scs_diag 5 i j ==> (?e1. &0 < e1 /\ (scs_a_v39 s i j = dist (v i,v j) ==> (!t. abs t < e1 ==> scs_a_v39 s i j <= dist (f (v i) t,f (v j) t))))` (C SUBGOAL_THEN ASSUME_TAC);
1301 BY(ASM_MESON_TAC[arith `x < y ==> ~(x = y)`]);
1302 TYPIFY `!i. T ==> (?e1. &0 < e1 /\ (scs_a_v39 s i i = dist (v i,v i) ==> (!t. abs t < e1 ==> scs_a_v39 s i i <= dist (f (v i) t,f (v i) t))))` (C SUBGOAL_THEN ASSUME_TAC);
1303 REWRITE_TAC[DIST_REFL];
1304 BY(MESON_TAC[arith `x = &0 ==> x <= &0`;arith `&0 < &1`]);
1306 TYPIFY `(?e1. &0 < e1 /\ (scs_a_v39 s 0 1 = dist (v 0,v 1) ==> (!t. abs t < e1 ==> scs_a_v39 s 0 1 <= dist (f (v 0) t,f (v 1) t)))) /\ (?e1. &0 < e1 /\ (scs_a_v39 s 1 2 = dist (v 1,v 2) ==> (!t. abs t < e1 ==> scs_a_v39 s 1 2 <= dist (f (v 1) t,f (v 2) t)))) /\ (?e1. &0 < e1 /\ (scs_a_v39 s 2 3 = dist (v 2,v 3) ==> (!t. abs t < e1 ==> scs_a_v39 s 2 3 <= dist (f (v 2) t,f (v 3) t)))) /\ (?e1. &0 < e1 /\ (scs_a_v39 s 3 4 = dist (v 3,v 4) ==> (!t. abs t < e1 ==> scs_a_v39 s 3 4 <= dist (f (v 3) t,f (v 4) t)))) /\ (?e1. &0 < e1 /\ (scs_a_v39 s 0 4 = dist (v 0,v 4) ==> (!t. abs t < e1 ==> scs_a_v39 s 0 4 <= dist (f (v 0) t,f (v 4) t))))` (C SUBGOAL_THEN MP_TAC);
1308 TYPIFY_GOAL_THEN `!a b. (?e1. &0 < e1 /\ (a = b ==> (!t. abs t < e1 ==> a <= b)))` (unlist REWRITE_TAC);
1309 BY(MESON_TAC[arith `&0 < &1`;arith `(a = b) ==> (a <= b)`]);
1311 BY(ASM_MESON_TAC[]);
1312 ONCE_REWRITE_TAC[DIST_SYM];
1313 BY(ASM_MESON_TAC[arith `x = y ==> x <= y`]);
1314 REWRITE_TAC[LEFT_OR_DISTRIB;RIGHT_OR_DISTRIB;GSYM DISJ_ASSOC];
1315 ONCE_REWRITE_TAC[TAUT `(a1 /\ a2 /\ a3 /\ a4 /\ a5) <=> ((T ==> a1) /\ (T ==> a2) /\ (T ==> a3) /\ (T ==> a4) /\ (T ==> a5))`];
1316 REPEAT WEAKER_STRIP_TAC;
1317 FIRST_X_ASSUM MP_TAC;
1318 BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN FIRST_X_ASSUM (unlist REWRITE_TAC) THEN NUM_REDUCE_TAC THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[])
1323 let b5_assumption_reduction = prove_by_refinement(
1328 (!i j. scs_diag 5 i j ==> &4 * h0 < scs_b_v39 s i j) /\
1329 deformation f (IMAGE v (:num)) (--e,e) /\
1330 (!w t. ~(w = v 0) /\ ~(w = v 1) ==> (f w t = w)) /\
1331 (?e1. &0 < e1 /\ (!t. abs t < e1 ==> dist(f (v 1) t,v 2) = dist(v 1,v 2) /\ dist(f (v 0) t,v 4) = dist(v 0,v 4))) /\
1332 (?e1. &0 < e1 /\ (!t. abs t < e1 ==> dist(f (v 0) t,f (v 1) t) <= dist(v 0, v 1)))
1334 (!i j. ?e1. &0 < e1 /\ (dist(v i,v j) = scs_b_v39 s i j ==>
1335 (!t. abs t < e1 ==> dist(f (v i) t,f (v j) t) <= scs_b_v39 s i j)))
1339 REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC Cuxvzoz.I_IMP THEN ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
1340 TYPIFY `!i j.scs_a_v39 s (i MOD 5) (j MOD 5) = scs_a_v39 s i j /\ scs_b_v39 s (i MOD 5) (j MOD 5) = scs_b_v39 s i j ` (C SUBGOAL_THEN ASSUME_TAC);
1341 FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC;
1342 ASM_REWRITE_TAC[Appendix.is_scs_v39];
1343 REPEAT WEAKER_STRIP_TAC;
1344 BY(REPEAT (FIRST_X_ASSUM_ST `periodic2` MP_TAC) THEN MESON_TAC[Cuxvzoz.periodic2_MOD;arith `~(5 = 0)`]);
1345 TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
1346 BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
1347 TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
1349 MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
1350 BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
1351 INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
1354 TYPIFY `!j. j < 5 ==> (j MOD 5 = j)` (C SUBGOAL_THEN ASSUME_TAC);
1355 BY(REWRITE_TAC[MOD_LT]);
1356 COMMENT "scs_b_v39";
1358 MATCH_MP_TAC Terminal.periodic2_mod_reduce;
1359 TYPIFY `5` EXISTS_TAC;
1360 ASM_REWRITE_TAC[arith `~(5=0)`];
1362 MATCH_MP_TAC Cuxvzoz.MOD_periodic2;
1363 BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[] THEN MESON_TAC[arith `~(5=0)`]);
1364 TYPIFY_GOAL_THEN `!P. (!i j. P i j ==> P j i) /\ (!i j. (i <= (j:num)) ==> P i j) ==> (!i j. P i j)` MATCH_MP_TAC;
1365 BY(MESON_TAC[arith `i <= j \/ j <= (i:num)`]);
1367 REPEAT WEAKER_STRIP_TAC;
1368 ONCE_REWRITE_TAC[DIST_SYM];
1369 TYPIFY `scs_b_v39 s j i = scs_b_v39 s i j` (C SUBGOAL_THEN SUBST1_TAC);
1370 FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC THEN REWRITE_TAC[Appendix.is_scs_v39] THEN REPEAT WEAKER_STRIP_TAC;
1371 BY(ASM_MESON_TAC[]);
1372 FIRST_X_ASSUM MATCH_MP_TAC;
1373 BY(ASM_REWRITE_TAC[]);
1374 TYPIFY `!t. f (v 2) t = v 2 /\ f (v 3) t = v 3 /\ f (v 4) t = v 4` (C SUBGOAL_THEN ASSUME_TAC);
1375 BY(ASM_MESON_TAC[arith `0 < 5 /\ 1 < 5 /\ 2 < 5 /\ 3 < 5 /\ 4 < 5 /\ ~(2 = 0) /\ ~(2 = 1) /\ ~(3 = 0) /\ ~(3 = 1) /\ ~(4 =0) /\ ~(4=1)`]);
1376 TYPIFY `scs_diag 5 0 2 /\ scs_diag 5 0 3 /\ scs_diag 5 1 3 /\ scs_diag 5 1 4 /\ scs_diag 5 2 4` (C SUBGOAL_THEN ASSUME_TAC);
1377 BY(REWRITE_TAC[Appendix.scs_diag;Uxckfpe.ARITH_5_TAC]);
1378 TYPIFY `!i j. scs_diag 5 i j ==> (?e1. &0 < e1 /\ (dist (v i,v j) = scs_b_v39 s i j ==> (!t. abs t < e1 ==> dist (f (v i) t,f (v j) t) <= scs_b_v39 s i j)))` (C SUBGOAL_THEN ASSUME_TAC);
1379 REPEAT WEAKER_STRIP_TAC;
1380 TYPIFY `&1` EXISTS_TAC;
1381 (REWRITE_TAC[arith `&0 < &1`]);
1382 TYPIFY `dist(v i,v j) <= &4 * h0` ENOUGH_TO_SHOW_TAC;
1383 FIRST_X_ASSUM_ST `&4 * h0` (C INTRO_TAC [`i`;`j`]);
1386 INTRO_TAC DIST_TRIANGLE [`v i`;`(vec 0):real^3`;`v j`];
1387 REWRITE_TAC[DIST_0];
1388 TYPIFY `!i. norm (v i) <= &2 * h0` ENOUGH_TO_SHOW_TAC;
1389 BY(DISCH_TAC THEN FIRST_ASSUM (C INTRO_TAC [`i`]) THEN FIRST_X_ASSUM (C INTRO_TAC [`j`]) THEN REAL_ARITH_TAC);
1390 FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN REPEAT WEAKER_STRIP_TAC;
1391 BY(FIRST_X_ASSUM_ST `ball_annulus` MP_TAC THEN REWRITE_TAC[Terminal.IMAGE_SUBSET_IN;IN_UNIV] THEN MESON_TAC[Fnjlbxs.in_ball_annulus]);
1392 TYPIFY `!i. T ==> (?e1. &0 < e1 /\ (dist (v i,v i) = scs_b_v39 s i i ==> (!t. abs t < e1 ==> dist (f (v i) t,f (v i) t) <= scs_b_v39 s i i)))` (C SUBGOAL_THEN ASSUME_TAC);
1393 REWRITE_TAC[DIST_REFL];
1394 BY(MESON_TAC[arith `x = &0 ==> x <= &0`;arith `&0 < &1`]);
1396 TYPIFY `(?e1. &0 < e1 /\ (dist (v 0,v 1) = scs_b_v39 s 0 1 ==> (!t. abs t < e1 ==> dist (f (v 0) t,f (v 1) t) <= scs_b_v39 s 0 1))) /\(?e1. &0 < e1 /\ (dist (v 1,v 2) = scs_b_v39 s 1 2 ==> (!t. abs t < e1 ==> dist (f (v 1) t,f (v 2) t) <= scs_b_v39 s 1 2))) /\(?e1. &0 < e1 /\ (dist (v 2,v 3) = scs_b_v39 s 2 3 ==> (!t. abs t < e1 ==> dist (f (v 2) t,f (v 3) t) <= scs_b_v39 s 2 3))) /\(?e1. &0 < e1 /\ (dist (v 3,v 4) = scs_b_v39 s 3 4 ==> (!t. abs t < e1 ==> dist (f (v 3) t,f (v 4) t) <= scs_b_v39 s 3 4))) /\(?e1. &0 < e1 /\ (dist (v 0,v 4) = scs_b_v39 s 0 4 ==> (!t. abs t < e1 ==> dist (f (v 0) t,f (v 4) t) <= scs_b_v39 s 0 4)))` (C SUBGOAL_THEN MP_TAC);
1398 TYPIFY_GOAL_THEN `!a b. (?e1. &0 < e1 /\ (a = b ==> (!t. abs t < e1 ==> a <= b)))` (unlist REWRITE_TAC);
1399 BY(MESON_TAC[arith `&0 < &1`;arith `(a = b) ==> (a <= b)`]);
1401 BY(ASM_MESON_TAC[]);
1402 BY(ASM_MESON_TAC[arith `x = y ==> x <= y`]);
1404 REWRITE_TAC[arith `i < 5 <=> (i = 0) \/ (i = 1) \/ (i=2) \/ (i =3) \/ (i=4)`];
1405 ONCE_REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (b ==> a ==> c)`];
1406 REWRITE_TAC[LEFT_OR_DISTRIB;RIGHT_OR_DISTRIB;GSYM DISJ_ASSOC];
1407 FIRST_X_ASSUM MP_TAC;
1408 ONCE_REWRITE_TAC[TAUT `(a1 /\ a2 /\ a3 /\ a4 /\ a5) <=> ((T ==> a1) /\ (T ==> a2) /\ (T ==> a3) /\ (T ==> a4) /\ (T ==> a5))`];
1409 REPEAT WEAKER_STRIP_TAC;
1410 FIRST_X_ASSUM MP_TAC;
1411 BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN FIRST_X_ASSUM (unlist REWRITE_TAC) THEN NUM_REDUCE_TAC THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[])
1416 let b5_assumption_reduction = prove_by_refinement(
1421 (!i j. scs_diag 5 i j ==> &4 * h0 < scs_b_v39 s i j) /\
1422 deformation f (IMAGE v (:num)) (--e,e) /\
1423 (!w t. ~(w = v 4) /\ ~(w = v 0) ==> (f w t = w)) /\
1424 (?e1. &0 < e1 /\ (!t. abs t < e1 ==> dist(f (v 4) t,f (v 0) t) = dist(v 4,v 0) /\ dist(f (v 4) t,v 3) = dist(v 4,v 3))) /\
1425 (?e1. &0 < e1 /\ (!t. abs t < e1 ==> dist(f (v 0) t, (v 1)) <= dist(v 0, v 1)))
1427 (!i j. ?e1. &0 < e1 /\ (dist(v i,v j) = scs_b_v39 s i j ==>
1428 (!t. abs t < e1 ==> dist(f (v i) t,f (v j) t) <= scs_b_v39 s i j)))
1432 REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC Cuxvzoz.I_IMP THEN ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
1433 TYPIFY `!i j.scs_a_v39 s (i MOD 5) (j MOD 5) = scs_a_v39 s i j /\ scs_b_v39 s (i MOD 5) (j MOD 5) = scs_b_v39 s i j ` (C SUBGOAL_THEN ASSUME_TAC);
1434 FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC;
1435 ASM_REWRITE_TAC[Appendix.is_scs_v39];
1436 REPEAT WEAKER_STRIP_TAC;
1437 BY(REPEAT (FIRST_X_ASSUM_ST `periodic2` MP_TAC) THEN MESON_TAC[Cuxvzoz.periodic2_MOD;arith `~(5 = 0)`]);
1438 TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
1439 BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
1440 TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
1442 MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
1443 BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
1444 INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
1447 TYPIFY `!j. j < 5 ==> (j MOD 5 = j)` (C SUBGOAL_THEN ASSUME_TAC);
1448 BY(REWRITE_TAC[MOD_LT]);
1449 COMMENT "scs_b_v39";
1451 MATCH_MP_TAC Terminal.periodic2_mod_reduce;
1452 TYPIFY `5` EXISTS_TAC;
1453 ASM_REWRITE_TAC[arith `~(5=0)`];
1455 MATCH_MP_TAC Cuxvzoz.MOD_periodic2;
1456 BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[] THEN MESON_TAC[arith `~(5=0)`]);
1457 TYPIFY_GOAL_THEN `!P. (!i j. P i j ==> P j i) /\ (!i j. (i <= (j:num)) ==> P i j) ==> (!i j. P i j)` MATCH_MP_TAC;
1458 BY(MESON_TAC[arith `i <= j \/ j <= (i:num)`]);
1460 REPEAT WEAKER_STRIP_TAC;
1461 ONCE_REWRITE_TAC[DIST_SYM];
1462 TYPIFY `scs_b_v39 s j i = scs_b_v39 s i j` (C SUBGOAL_THEN SUBST1_TAC);
1463 FIRST_X_ASSUM_ST `is_scs_v39` MP_TAC THEN REWRITE_TAC[Appendix.is_scs_v39] THEN REPEAT WEAKER_STRIP_TAC;
1464 BY(ASM_MESON_TAC[]);
1465 FIRST_X_ASSUM MATCH_MP_TAC;
1466 BY(ASM_REWRITE_TAC[]);
1467 TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(i=j) ==> ~(v i = v j)` (C SUBGOAL_THEN ASSUME_TAC);
1468 BY(ASM_MESON_TAC[]);
1469 TYPIFY `!t. f (v 2) t = v 2 /\ f (v 3) t = v 3 /\ f (v 1) t = v 1` (C SUBGOAL_THEN ASSUME_TAC);
1470 BY(GEN_TAC THEN REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC THEN REPEAT CONJ_TAC) THEN NUM_REDUCE_TAC);
1471 TYPIFY `scs_diag 5 0 2 /\ scs_diag 5 0 3 /\ scs_diag 5 1 3 /\ scs_diag 5 1 4 /\ scs_diag 5 2 4` (C SUBGOAL_THEN ASSUME_TAC);
1472 BY(REWRITE_TAC[Appendix.scs_diag;Uxckfpe.ARITH_5_TAC]);
1473 TYPIFY `!i j. scs_diag 5 i j ==> (?e1. &0 < e1 /\ (dist (v i,v j) = scs_b_v39 s i j ==> (!t. abs t < e1 ==> dist (f (v i) t,f (v j) t) <= scs_b_v39 s i j)))` (C SUBGOAL_THEN ASSUME_TAC);
1474 REPEAT WEAKER_STRIP_TAC;
1475 TYPIFY `&1` EXISTS_TAC;
1476 (REWRITE_TAC[arith `&0 < &1`]);
1477 TYPIFY `dist(v i,v j) <= &4 * h0` ENOUGH_TO_SHOW_TAC;
1478 FIRST_X_ASSUM_ST `&4 * h0` (C INTRO_TAC [`i`;`j`]);
1481 INTRO_TAC DIST_TRIANGLE [`v i`;`(vec 0):real^3`;`v j`];
1482 REWRITE_TAC[DIST_0];
1483 TYPIFY `!i. norm (v i) <= &2 * h0` ENOUGH_TO_SHOW_TAC;
1484 BY(DISCH_TAC THEN FIRST_ASSUM (C INTRO_TAC [`i`]) THEN FIRST_X_ASSUM (C INTRO_TAC [`j`]) THEN REAL_ARITH_TAC);
1485 FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN REPEAT WEAKER_STRIP_TAC;
1486 BY(FIRST_X_ASSUM_ST `ball_annulus` MP_TAC THEN REWRITE_TAC[Terminal.IMAGE_SUBSET_IN;IN_UNIV] THEN MESON_TAC[Fnjlbxs.in_ball_annulus]);
1487 TYPIFY `!i. T ==> (?e1. &0 < e1 /\ (dist (v i,v i) = scs_b_v39 s i i ==> (!t. abs t < e1 ==> dist (f (v i) t,f (v i) t) <= scs_b_v39 s i i)))` (C SUBGOAL_THEN ASSUME_TAC);
1488 REWRITE_TAC[DIST_REFL];
1489 BY(MESON_TAC[arith `x = &0 ==> x <= &0`;arith `&0 < &1`]);
1491 TYPIFY `(?e1. &0 < e1 /\ (dist (v 0,v 1) = scs_b_v39 s 0 1 ==> (!t. abs t < e1 ==> dist (f (v 0) t,f (v 1) t) <= scs_b_v39 s 0 1))) /\(?e1. &0 < e1 /\ (dist (v 1,v 2) = scs_b_v39 s 1 2 ==> (!t. abs t < e1 ==> dist (f (v 1) t,f (v 2) t) <= scs_b_v39 s 1 2))) /\(?e1. &0 < e1 /\ (dist (v 2,v 3) = scs_b_v39 s 2 3 ==> (!t. abs t < e1 ==> dist (f (v 2) t,f (v 3) t) <= scs_b_v39 s 2 3))) /\(?e1. &0 < e1 /\ (dist (v 3,v 4) = scs_b_v39 s 3 4 ==> (!t. abs t < e1 ==> dist (f (v 3) t,f (v 4) t) <= scs_b_v39 s 3 4))) /\(?e1. &0 < e1 /\ (dist (v 0,v 4) = scs_b_v39 s 0 4 ==> (!t. abs t < e1 ==> dist (f (v 0) t,f (v 4) t) <= scs_b_v39 s 0 4)))` (C SUBGOAL_THEN MP_TAC);
1493 TYPIFY_GOAL_THEN `!a b. (?e1. &0 < e1 /\ (a = b ==> (!t. abs t < e1 ==> a <= b)))` (unlist REWRITE_TAC);
1494 BY(MESON_TAC[arith `&0 < &1`;arith `(a = b) ==> (a <= b)`]);
1496 BY(ASM_MESON_TAC[]);
1497 REPEAT (FIRST_X_ASSUM_ST `dist(v 4,v 0)` MP_TAC);
1498 REWRITE_TAC[DIST_SYM];
1499 BY(ASM_MESON_TAC[arith `x = y ==> x <= y`]);
1501 REWRITE_TAC[arith `i < 5 <=> (i = 0) \/ (i = 1) \/ (i=2) \/ (i =3) \/ (i=4)`];
1502 ONCE_REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (b ==> a ==> c)`];
1503 REWRITE_TAC[LEFT_OR_DISTRIB;RIGHT_OR_DISTRIB;GSYM DISJ_ASSOC];
1504 FIRST_X_ASSUM MP_TAC;
1505 ONCE_REWRITE_TAC[TAUT `(a1 /\ a2 /\ a3 /\ a4 /\ a5) <=> ((T ==> a1) /\ (T ==> a2) /\ (T ==> a3) /\ (T ==> a4) /\ (T ==> a5))`];
1506 REPEAT WEAKER_STRIP_TAC;
1507 FIRST_X_ASSUM MP_TAC;
1508 BY(REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN FIRST_X_ASSUM (unlist REWRITE_TAC) THEN NUM_REDUCE_TAC THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[])
1512 (* was dihV_dih_y *)
1514 let azim_dih_y = prove_by_refinement(
1515 `!v0 v1 v2 v3. ~collinear {v0,v1,v2} /\ ~collinear{v0,v1,v3} /\ azim v0 v1 v2 v3 <= pi ==>
1516 azim v0 v1 v2 v3 = dih_y (dist(v0,v1)) (dist(v0,v2)) (dist(v0,v3))
1517 (dist(v2,v3)) (dist(v1,v3)) (dist(v1,v2))`,
1520 REPEAT WEAKER_STRIP_TAC;
1521 INTRO_TAC AZIM_DIHV_SAME_STRONG [`v0`;`v1`;`v2`;`v3`];
1523 DISCH_THEN SUBST1_TAC;
1524 GMATCH_SIMP_TAC (REWRITE_RULE[LET_THM] Merge_ineq.DIHV_DIH_X);
1525 REWRITE_TAC[Sphere.dih_y;LET_THM;arith `x*x = x pow 2`];
1526 BY(ASM_REWRITE_TAC[GSYM Collect_geom2.NOT_COL_EQ_UPS_X_POS])
1530 (* next azim reduction *)
1533 let azm5_reduction = prove_by_refinement(
1539 deformation f (IMAGE v (:num)) (--e,e) /\
1540 (!w t. ~(w = v 0) /\ ~(w = v 4) ==> f w t = w) /\
1541 azim (vec 0) (v 0) (v 1) (v 4) < pi /\
1542 azim (vec 0) (v 1) (v 2) (v 0) < pi /\
1543 &0 < azim (vec 0) (v 0) (v 1) (v 3) /\
1546 ==> azim (vec 0) (v 3) (f (v 0) t) (v 1) <=
1547 azim (vec 0) (v 3) (v 0) (v 1))) /\
1550 // make this a dih_y condition??
1551 ==> azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) =
1552 azim (vec 0) (v 3) (v 4) (v 0) /\
1553 azim (vec 0) (f (v 4) t) (f (v 0) t) (v 3) =
1554 azim (vec 0) (v 4) (v 0) (v 3) /\
1555 azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) =
1556 azim (vec 0) (v 0) (v 3) (v 4)))
1557 ==> azim (vec 0) (v 3) (v 4) (v 2) =
1558 azim (vec 0) (v 3) (v 4) (v 0) +
1559 azim (vec 0) (v 3) (v 0) (v 1) +
1560 azim (vec 0) (v 3) (v 1) (v 2) /\
1561 azim (vec 0) (v 0) (v 1) (v 4) =
1562 azim (vec 0) (v 0) (v 1) (v 3) + azim (vec 0) (v 0) (v 3) (v 4) /\
1563 azim (vec 0) (v 1) (v 2) (v 0) =
1564 azim (vec 0) (v 1) (v 2) (v 3) + azim (vec 0) (v 1) (v 3) (v 0) /\
1567 ==> azim (vec 0) (v 3) (f (v 4) t) (v 2) =
1568 azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) +
1569 azim (vec 0) (v 3) (f (v 0) t) (v 1) +
1570 azim (vec 0) (v 3) (v 1) (v 2) /\
1571 azim (vec 0) (f (v 0) t) (v 1) (f (v 4) t) =
1572 azim (vec 0) (f (v 0) t) (v 1) (v 3) +
1573 azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) /\
1574 azim (vec 0) (v 1) (v 2) (f (v 0) t) =
1575 azim (vec 0) (v 1) (v 2) (v 3) +
1576 azim (vec 0) (v 1) (v 3) (f (v 0) t) /\
1577 &0 < azim (vec 0) (f (v 0) t) (v 1) (v 3) /\
1578 azim (vec 0) (f (v 0) t) (v 1) (v 3) < pi)) /\
1579 (!i. ?e0. &0 < e0 /\
1580 (azim (vec 0) (v i) (v (i + 1)) (v (i + 4)) = pi
1582 ==> azim (vec 0) (f (v i) t) (f (v (i + 1)) t)
1583 (f (v (i + 4)) t) <=
1587 REPEAT WEAKER_STRIP_TAC;
1588 ASSUME_TAC (arith `~(0 = 5)`);
1589 TYPIFY `!i. i MOD 5 < 5` (C SUBGOAL_THEN ASSUME_TAC);
1590 BY((FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[DIVISION]);
1591 TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
1592 BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
1593 TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
1595 MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
1596 BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
1597 TYPIFY `v 5 = v 0 /\ v 6 = v 1 /\ v 7 = v 2 /\ v 8 = v 3 /\ v 9 = v 4` (C SUBGOAL_THEN ASSUME_TAC);
1598 FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
1599 BY(REWRITE_TAC[Ocbicby.MOD_5_EXPLICIT;arith `8 = 1*5 + 3`;arith `9 = 1*5 + 4`;MOD_MULT_ADD]);
1600 INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
1603 TYPIFY ` generic (IMAGE v (:num)) (IMAGE (\i. {v i, v (SUC i)}) (:num)) /\ convex_local_fan (IMAGE v (:num), IMAGE (\i. {v i, v (SUC i)}) (:num), IMAGE (\i. v i,v (SUC i)) (:num))` (C SUBGOAL_THEN ASSUME_TAC);
1605 FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[LET_THM;Appendix.BBs_v39];
1606 BY(MESON_TAC[arith `~(5 <= 3)`]);
1607 BY(FIRST_X_ASSUM_ST `scs_generic` MP_TAC THEN MESON_TAC[Appendix.scs_generic]);
1608 FIRST_X_ASSUM MP_TAC THEN BURY_MP_TAC;
1609 COMMENT "first addition";
1611 INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`3`;`4`];
1612 ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 4 = 7 /\ 3 + 3 = 6 /\ 3 <= 5 /\ 0 < 3 /\ 3 < 4 /\ 4 < 5`];
1613 DISCH_THEN SUBST1_TAC;
1614 INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`2`;`3`];
1615 ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 3 = 6 /\ 3 + 2 = 5 /\ 3 <= 5 /\ 0 < 2 /\ 2 < 3 /\ 3 < 5`];
1616 DISCH_THEN SUBST1_TAC;
1619 COMMENT "second addition";
1621 INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`0`;`3`;`4`];
1623 BY(ASM_REWRITE_TAC[LET_THM]);
1624 COMMENT "third addition";
1625 INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`0`;`3`;`4`];
1627 ASM_REWRITE_TAC[LET_THM];
1631 INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`1`;`2`;`4`];
1633 BY(ASM_REWRITE_TAC[LET_THM]);
1635 TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(i = j) ==> ~(v i = v j)` (C SUBGOAL_THEN ASSUME_TAC);
1636 BY(ASM_MESON_TAC[]);
1637 TYPIFY `!t. f (v 1) t = v 1 /\ f (v 2) t = v 2 /\ f (v 3) t = v 3` (C SUBGOAL_THEN ASSUME_TAC);
1639 BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN NUM_REDUCE_TAC);
1640 COMMENT "colinearity";
1641 TYPIFY `!i j. ~(v i = v j) ==> ~collinear {vec 0,v i, v j}` (C SUBGOAL_THEN ASSUME_TAC);
1642 REPEAT GEN_TAC THEN DISCH_TAC;
1643 MATCH_MP_TAC Zlzthic.PROPERTIES_GENERIC_LOCAL_FAN_ALT;
1644 GEXISTL_TAC [`IMAGE v (:num)`;`IMAGE (\i. {v i, v (SUC i)}) (:num)`;`IMAGE (\i. (v i, v (SUC i))) (:num)`];
1645 ASM_REWRITE_TAC[IN_IMAGE;IN_UNIV];
1647 MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
1648 BY(ASM_REWRITE_TAC[]);
1650 COMMENT "deform collinear";
1651 TYPIFY `!i j. ~collinear {vec 0,v i,v j} ==> (?e1. &0 < e1 /\ (!t. abs t < e1 ==> ~collinear {vec 0, f (v i) t, f (v j) t}))` (C SUBGOAL_THEN ASSUME_TAC);
1652 REPEAT WEAKER_STRIP_TAC;
1653 INTRO_TAC (GEN_ALL Local_lemmas1.CONTINUOUS_PRESERVE_COLLINEAR) [`&0`;`(vec 0):real^3`;`f (v i)`;`f (v j)`];
1655 FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation;arith `abs(&0 - x) = abs x`];
1656 REWRITE_TAC[IN_IMAGE;IN_UNIV];
1657 BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
1658 BY(REWRITE_TAC[arith `abs(&0 - r') = abs r'`]);
1659 TYPIFY `!i. azim (vec 0) (v i) (v (i+1)) (v(i+4)) <= pi` (C SUBGOAL_THEN ASSUME_TAC);
1660 REWRITE_TAC[arith `i+1 = SUC i`;arith `4 = 5 - 1`];
1662 MATCH_MP_TAC (REWRITE_RULE[LET_THM] Terminal.convex_local_fan_azim_le_pi);
1663 ASM_REWRITE_TAC[arith `3 <= 5`];
1664 FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM];
1665 BY(DISCH_THEN (unlist REWRITE_TAC));
1667 TYPIFY_GOAL_THEN `(?e1. &0 < e1 /\ (!t. abs t < e1 ==> azim (vec 0) (v 3) (f (v 4) t) (v 2) = azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) + azim (vec 0) (v 3) (f (v 0) t) (v 1) + azim (vec 0) (v 3) (v 1) (v 2) )) /\(?e1. &0 < e1 /\ (!t. abs t < e1 ==> azim (vec 0) (f (v 0) t) (v 1) (f (v 4) t) = azim (vec 0) (f (v 0) t) (v 1) (v 3) + azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) )) /\ (?e1. &0 < e1 /\ (!t. abs t < e1 ==> azim (vec 0) (v 1) (v 2) (f (v 0) t) = azim (vec 0) (v 1) (v 2) (v 3) + azim (vec 0) (v 1) (v 3) (f (v 0) t))) /\ (?e1. &0 < e1 /\ (!t. abs t < e1 ==> &0 < azim (vec 0) (f (v 0) t) (v 1) (v 3) /\ azim (vec 0) (f (v 0) t) (v 1) (v 3) < pi)) ==> (?e1. &0 < e1 /\ (!t. abs t < e1 ==> azim (vec 0) (v 3) (f (v 4) t) (v 2) = azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) + azim (vec 0) (v 3) (f (v 0) t) (v 1) + azim (vec 0) (v 3) (v 1) (v 2) /\ azim (vec 0) (f (v 0) t) (v 1) (f (v 4) t) = azim (vec 0) (f (v 0) t) (v 1) (v 3) + azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) /\ azim (vec 0) (v 1) (v 2) (f (v 0) t) = azim (vec 0) (v 1) (v 2) (v 3) + azim (vec 0) (v 1) (v 3) (f (v 0) t) /\ &0 < azim (vec 0) (f (v 0) t) (v 1) (v 3) /\ azim (vec 0) (f (v 0) t) (v 1) (v 3) < pi))` (GMATCH_SIMP_TAC);
1668 REPEAT WEAKER_STRIP_TAC;
1669 INTRO_TAC Cuxvzoz.epsilon_quad [`e1''`;`e1'''`;`e1''''`;`e1'''''`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1670 TYPIFY `e''''` EXISTS_TAC;
1671 ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC THEN REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[];
1672 BY(ASM_MESON_TAC[]);
1673 BY(ASM_MESON_TAC[]);
1674 REWRITE_TAC[GSYM CONJ_ASSOC];
1675 COMMENT "azim bounds";
1676 TYPIFY `azim (vec 0) (v 0) (v 1) (v 3) < pi` (C SUBGOAL_THEN ASSUME_TAC);
1677 FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 4) < pi` MP_TAC;
1679 MATCH_MP_TAC (arith `&0 <= y ==> (x + y < pi ==> x < pi)`);
1680 BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
1681 TYPIFY `~coplanar {vec 0,v 0,v 1,v 3}` (C SUBGOAL_THEN ASSUME_TAC);
1682 REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
1683 BY(REPEAT (FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 3)` MP_TAC) THEN REAL_ARITH_TAC);
1684 TYPIFY `&0 < azim (vec 0) (v 3) (v 0) (v 1) /\ &0 < azim (vec 0) (v 1) (v 3) (v 0)` (C SUBGOAL_THEN ASSUME_TAC);
1685 REWRITE_TAC[Zlzthic.azim_pos_iff_nz];
1686 FIRST_X_ASSUM_ST `coplanar` MP_TAC;
1687 BY(MESON_TAC[Local_lemmas1.AZIM_COND_FOR_COPLANAR;SET_RULE `{a,b,c,d} = {a,d,b,c}`;SET_RULE `{a,b,c,d}={a,c,d,b}`]);
1688 INTRO_TAC Cuxvzoz.WNWSHJT_ALT [`v 3`;`v 0`;`v 1`;`f`;`-- e`;`e`;`pi - azim (vec 0) (v 0) (v 3) (v 4)`];
1690 ASM_REWRITE_TAC[arith `a < pi - b <=> a + b < pi`];
1692 MATCH_MP_TAC Zlzthic.deformation_subset;
1693 TYPIFY `IMAGE v (:num)` EXISTS_TAC;
1694 ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_UNIV];
1695 BY(MESON_TAC[FUN_IN_IMAGE;IN_UNIV]);
1696 REWRITE_TAC[CONJ_ASSOC];
1698 FIRST_X_ASSUM_ST `coplanar` MP_TAC;
1699 BY(MESON_TAC[Planarity.notcoplanar_imp_notcollinear_fan;SET_RULE `{a,b,c} = {a,c,b}`]);
1700 BY(REPEAT (FIRST_X_ASSUM_ST `x < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
1701 REPEAT WEAKER_STRIP_TAC;
1702 INTRO_TAC Cuxvzoz.WNWSHJT_ALT [`v 0`;`v 1`;`v 3`;`f`;`-- e`;`e`;`pi - azim (vec 0) (v 1) (v 2) (v 3)`];
1704 ASM_REWRITE_TAC[arith `a < pi - b <=> a + b < pi`];
1706 MATCH_MP_TAC Zlzthic.deformation_subset;
1707 TYPIFY `IMAGE v (:num)` EXISTS_TAC;
1708 ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_UNIV];
1709 BY(MESON_TAC[FUN_IN_IMAGE;IN_UNIV]);
1710 REWRITE_TAC[CONJ_ASSOC];
1712 FIRST_X_ASSUM_ST `coplanar` MP_TAC;
1713 BY(MESON_TAC[Planarity.notcoplanar_imp_notcollinear_fan;SET_RULE `{a,b,c} = {a,c,b}`]);
1714 BY(REPEAT (FIRST_X_ASSUM_ST `x < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
1715 REPEAT WEAKER_STRIP_TAC;
1716 COMMENT "azim additivity";
1717 TYPIFY `?e3. &0 < e3 /\ (!t. abs t < e3 ==> ~collinear {vec 0,f (v 0) t,f (v 4) t} /\ ~collinear {vec 0,f (v 0) t,f (v 3) t} /\ ~collinear {vec 0,f (v 0) t,f (v 1) t} /\ ~collinear {vec 0,f (v 4) t,f (v 3) t})` (C SUBGOAL_THEN ASSUME_TAC);
1718 FIRST_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`4`]) THEN ANTS_TAC THENL [REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC;REPEAT WEAKER_STRIP_TAC];
1719 FIRST_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`3`]) THEN ANTS_TAC THENL [REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC;REPEAT WEAKER_STRIP_TAC];
1720 FIRST_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`1`]) THEN ANTS_TAC THENL [REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC;REPEAT WEAKER_STRIP_TAC];
1721 FIRST_X_ASSUM_ST `collinear` (C INTRO_TAC [`4`;`3`]) THEN ANTS_TAC THENL [REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC;REPEAT WEAKER_STRIP_TAC];
1722 INTRO_TAC Cuxvzoz.epsilon_quad [`e1''`;`e1'''`;`e1''''`;`e1'''''`] THEN ANTS_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
1723 TYPIFY `e''''` EXISTS_TAC THEN CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
1724 BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]);
1725 FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
1727 INTRO_TAC Cuxvzoz.epsilon_triple [`e1`;`e1'`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1728 TYPIFY `e'''` EXISTS_TAC;
1729 ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1730 REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1731 REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1732 INTRO_TAC Cuxvzoz.azim_dominated_split [`(vec 0):real^3`;`v 3`;`v 4`;`v 1`;`v 2`;`(vec 0):real^3`;`v 3`;`f (v 4) t`;`v 1`;`v 2`];
1733 INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`3`;`4`];
1734 ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 4 = 7 /\ 3 + 3 = 6 /\ 3 <= 5 /\ 0 < 3 /\ 3 < 4 /\ 4 < 5`];
1735 DISCH_THEN (SUBST1_TAC o GSYM) THEN ASM_REWRITE_TAC[arith `x <= x`];
1736 INTRO_TAC Cuxvzoz.azim_dominated_split [`(vec 0):real^3`;`v 3`;`v 4`;`v 0`;`v 1`;`(vec 0):real^3`;`v 3`;`f (v 4) t`;`f (v 0) t`;`v 1`];
1737 ASM_REWRITE_TAC[arith `x <= x`];
1738 INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`2`;`3`];
1739 NUM_REDUCE_TAC THEN ASM_REWRITE_TAC[LET_THM];
1741 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN ASM_REWRITE_TAC[];
1742 TYPIFY_GOAL_THEN `~collinear {vec 0, v 1, v 3} /\ ~collinear {vec 0, v 1, v 3} /\ ~collinear {vec 0, v 2, v 3}` (unlist REWRITE_TAC);
1743 BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
1744 BY(REPLICATE_TAC 15 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1746 COMMENT "azim 0 additive";
1747 FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
1749 INTRO_TAC Cuxvzoz.epsilon_triple [`e'`;`e1'`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1750 TYPIFY `e''''` EXISTS_TAC;
1751 ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1752 REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1753 REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1754 MATCH_MP_TAC Fan.sum3_azim_fan;
1756 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MP_TAC PI_POS THEN REAL_ARITH_TAC);
1757 REPEAT WEAKER_STRIP_TAC;
1758 COMMENT "azim 1 additive";
1760 INTRO_TAC Cuxvzoz.epsilon_pair [`e''`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1761 TYPIFY `e'''` EXISTS_TAC;
1762 ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1763 REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1764 REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1765 MATCH_MP_TAC Fan.sum3_azim_fan;
1768 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MP_TAC PI_POS THEN REAL_ARITH_TAC);
1769 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
1771 BY(CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
1772 REPEAT WEAKER_STRIP_TAC;
1773 COMMENT "pi bounds";
1775 TYPIFY `e'` EXISTS_TAC;
1776 CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
1777 TYPIFY ` &0 < azim (vec 0) (f (v 0) t) (f (v 1) t) (f (v 3) t) /\ azim (vec 0) (f (v 0) t) (f (v 1) t) (f (v 3) t) < pi - azim (vec 0) (v 0) (v 3) (v 4)` ENOUGH_TO_SHOW_TAC;
1779 MATCH_MP_TAC (arith `&0 <= b ==> (&0 < a /\ a < pi - b ==> &0 < a /\ a < pi)`);
1780 BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
1781 FIRST_X_ASSUM MATCH_MP_TAC;
1782 BY(ASM_REWRITE_TAC[]);
1783 MATCH_MP_TAC Oxl_def.periodic_numseg;
1784 TYPIFY `5` EXISTS_TAC;
1785 REWRITE_TAC[arith `~(5 = 0)`];
1787 FIRST_X_ASSUM_ST `periodic` MP_TAC;
1788 REWRITE_TAC[Oxl_def.periodic];
1789 REWRITE_TAC[arith `(i+5)+j = (i+j)+5`];
1790 BY(DISCH_THEN (unlist REWRITE_TAC));
1791 REWRITE_TAC[IN_NUMSEG;arith `(0 <= i /\ i <= 5-1) <=> (i = 0 \/ i = 1 \/ i = 2 \/ i = 3 \/ i = 4)`];
1792 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN NUM_REDUCE_TAC;
1793 EXISTS_TAC `&1` THEN REPEAT (FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 4) < pi` MP_TAC);
1794 BY(MESON_TAC[arith `&0 < &1`;arith `x < pi ==> ~(x=pi)`]);
1795 REPEAT (FIRST_X_ASSUM_ST `+` kill);
1796 ASM_REWRITE_TAC[] THEN EXISTS_TAC `&1` THEN REPEAT (FIRST_X_ASSUM_ST `azim (vec 0) (v 1) (v 2) (v 0) < pi` MP_TAC);
1797 BY(MESON_TAC[arith `&0 < &1`;arith `x < pi ==> ~(x=pi)`]);
1798 BY(ASM_REWRITE_TAC[] THEN EXISTS_TAC `&1` THEN MESON_TAC[arith `&0 < &1`;arith `x <= x`]);
1799 INTRO_TAC Cuxvzoz.epsilon_triple [`e1''`;`e1'`;`e1`] THEN ANTS_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
1800 TYPIFY `e'''` EXISTS_TAC THEN CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
1801 REPLICATE_TAC 3(FIRST_X_ASSUM (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC);
1802 REPEAT (FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1804 FIRST_X_ASSUM_ST `a = pi` (SUBST1_TAC o GSYM);
1806 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
1807 TYPIFY `e1'` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1808 REPEAT (FIRST_X_ASSUM_ST `4` (C INTRO_TAC [`t`]));
1809 ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1810 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC)
1815 let azim5_reduction = prove_by_refinement(
1821 deformation f (IMAGE v (:num)) (--e,e) /\
1822 (!w t. ~(w = v 4) /\ ~(w = v 0) ==> f w t = w) /\
1823 azim (vec 0) (v 0) (v 1) (v 4) < pi /\
1824 azim (vec 0) (v 1) (v 2) (v 0) < pi /\
1825 &0 < azim (vec 0) (v 0) (v 1) (v 3) /\
1828 ==> azim (vec 0) (v 3) (f (v 0) t) (v 1) <=
1829 azim (vec 0) (v 3) (v 0) (v 1))) /\
1832 ==> dist (v 3,f (v 4) t) = dist (v 3,v 4) /\
1833 dist (f (v 0) t,f (v 4) t) = dist (v 0,v 4) /\
1834 norm (f (v 4) t) = norm (v 4) /\
1835 dist (f (v 0) t,v 3) = dist (v 0,v 3) /\
1836 dist (f (v 0) t,v 1) = dist (v 0,v 1) - abs t /\
1837 norm (f (v 0) t) = norm (v 0) /\
1838 (coplanar {vec 0, v 3, v 4, v 0}
1839 ==> coplanar {vec 0, v 3, f (v 4) t, f (v 0) t})))
1840 ==> azim (vec 0) (v 3) (v 4) (v 2) =
1841 azim (vec 0) (v 3) (v 4) (v 0) +
1842 azim (vec 0) (v 3) (v 0) (v 1) +
1843 azim (vec 0) (v 3) (v 1) (v 2) /\
1844 azim (vec 0) (v 0) (v 1) (v 4) =
1845 azim (vec 0) (v 0) (v 1) (v 3) + azim (vec 0) (v 0) (v 3) (v 4) /\
1846 azim (vec 0) (v 1) (v 2) (v 0) =
1847 azim (vec 0) (v 1) (v 2) (v 3) + azim (vec 0) (v 1) (v 3) (v 0) /\
1850 ==> azim (vec 0) (v 3) (f (v 4) t) (v 2) =
1851 azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) +
1852 azim (vec 0) (v 3) (f (v 0) t) (v 1) +
1853 azim (vec 0) (v 3) (v 1) (v 2) /\
1854 azim (vec 0) (f (v 0) t) (v 1) (f (v 4) t) =
1855 azim (vec 0) (f (v 0) t) (v 1) (v 3) +
1856 azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) /\
1857 azim (vec 0) (v 1) (v 2) (f (v 0) t) =
1858 azim (vec 0) (v 1) (v 2) (v 3) +
1859 azim (vec 0) (v 1) (v 3) (f (v 0) t) /\
1860 &0 < azim (vec 0) (f (v 0) t) (v 1) (v 3) /\
1861 azim (vec 0) (f (v 0) t) (v 1) (v 3) < pi)) /\
1862 (!i. ?e0. &0 < e0 /\
1863 (azim (vec 0) (v i) (v (i + 1)) (v (i + 4)) = pi
1865 ==> azim (vec 0) (f (v i) t) (f (v (i + 1)) t)
1866 (f (v (i + 4)) t) <=
1870 ==> azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) =
1871 azim (vec 0) (v 3) (v 4) (v 0) /\
1872 azim (vec 0) (f (v 4) t) (f (v 0) t) (v 3) =
1873 azim (vec 0) (v 4) (v 0) (v 3) /\
1874 azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) =
1875 azim (vec 0) (v 0) (v 3) (v 4)))`,
1878 REPEAT WEAKER_STRIP_TAC;
1879 ASSUME_TAC (arith `~(0 = 5)`);
1880 TYPIFY `!i. i MOD 5 < 5` (C SUBGOAL_THEN ASSUME_TAC);
1881 BY((FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[DIVISION]);
1882 TYPIFY `periodic v 5` (C SUBGOAL_THEN ASSUME_TAC);
1883 BY(FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN MESON_TAC[]);
1884 TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
1886 MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
1887 BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
1888 TYPIFY `v 5 = v 0 /\ v 6 = v 1 /\ v 7 = v 2 /\ v 8 = v 3 /\ v 9 = v 4` (C SUBGOAL_THEN ASSUME_TAC);
1889 FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
1890 BY(REWRITE_TAC[Ocbicby.MOD_5_EXPLICIT;arith `8 = 1*5 + 3`;arith `9 = 1*5 + 4`;MOD_MULT_ADD]);
1891 INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
1894 TYPIFY ` generic (IMAGE v (:num)) (IMAGE (\i. {v i, v (SUC i)}) (:num)) /\ convex_local_fan (IMAGE v (:num), IMAGE (\i. {v i, v (SUC i)}) (:num), IMAGE (\i. v i,v (SUC i)) (:num))` (C SUBGOAL_THEN ASSUME_TAC);
1896 FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN ASM_REWRITE_TAC[LET_THM;Appendix.BBs_v39];
1897 BY(MESON_TAC[arith `~(5 <= 3)`]);
1898 BY(FIRST_X_ASSUM_ST `scs_generic` MP_TAC THEN MESON_TAC[Appendix.scs_generic]);
1899 FIRST_X_ASSUM MP_TAC THEN BURY_MP_TAC;
1900 COMMENT "first addition";
1902 INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`3`;`4`];
1903 ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 4 = 7 /\ 3 + 3 = 6 /\ 3 <= 5 /\ 0 < 3 /\ 3 < 4 /\ 4 < 5`];
1904 DISCH_THEN SUBST1_TAC;
1905 INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`2`;`3`];
1906 ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 3 = 6 /\ 3 + 2 = 5 /\ 3 <= 5 /\ 0 < 2 /\ 2 < 3 /\ 3 < 5`];
1907 DISCH_THEN SUBST1_TAC;
1910 COMMENT "second addition";
1912 INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`0`;`3`;`4`];
1914 BY(ASM_REWRITE_TAC[LET_THM]);
1915 COMMENT "third addition";
1916 INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`0`;`3`;`4`];
1918 ASM_REWRITE_TAC[LET_THM];
1922 INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`1`;`2`;`4`];
1924 BY(ASM_REWRITE_TAC[LET_THM]);
1926 TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(i = j) ==> ~(v i = v j)` (C SUBGOAL_THEN ASSUME_TAC);
1927 BY(ASM_MESON_TAC[]);
1928 TYPIFY `!t. f (v 1) t = v 1 /\ f (v 2) t = v 2 /\ f (v 3) t = v 3` (C SUBGOAL_THEN ASSUME_TAC);
1930 BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN NUM_REDUCE_TAC);
1931 COMMENT "colinearity";
1932 TYPIFY `!i j. ~(v i = v j) ==> ~collinear {vec 0,v i, v j}` (C SUBGOAL_THEN ASSUME_TAC);
1933 REPEAT GEN_TAC THEN DISCH_TAC;
1934 MATCH_MP_TAC Zlzthic.PROPERTIES_GENERIC_LOCAL_FAN_ALT;
1935 GEXISTL_TAC [`IMAGE v (:num)`;`IMAGE (\i. {v i, v (SUC i)}) (:num)`;`IMAGE (\i. (v i, v (SUC i))) (:num)`];
1936 ASM_REWRITE_TAC[IN_IMAGE;IN_UNIV];
1938 MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
1939 BY(ASM_REWRITE_TAC[]);
1941 COMMENT "deform collinear";
1942 TYPIFY `!i j. ~collinear {vec 0,v i,v j} ==> (?e1. &0 < e1 /\ (!t. abs t < e1 ==> ~collinear {vec 0, f (v i) t, f (v j) t}))` (C SUBGOAL_THEN ASSUME_TAC);
1943 REPEAT WEAKER_STRIP_TAC;
1944 INTRO_TAC (GEN_ALL Local_lemmas1.CONTINUOUS_PRESERVE_COLLINEAR) [`&0`;`(vec 0):real^3`;`f (v i)`;`f (v j)`];
1946 FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation;arith `abs(&0 - x) = abs x`];
1947 REWRITE_TAC[IN_IMAGE;IN_UNIV];
1948 BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
1949 BY(REWRITE_TAC[arith `abs(&0 - r') = abs r'`]);
1950 TYPIFY `!i. azim (vec 0) (v i) (v (i+1)) (v(i+4)) <= pi` (C SUBGOAL_THEN ASSUME_TAC);
1951 REWRITE_TAC[arith `i+1 = SUC i`;arith `4 = 5 - 1`];
1953 MATCH_MP_TAC (REWRITE_RULE[LET_THM] Terminal.convex_local_fan_azim_le_pi);
1954 ASM_REWRITE_TAC[arith `3 <= 5`];
1955 FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM];
1956 BY(DISCH_THEN (unlist REWRITE_TAC));
1958 TYPIFY_GOAL_THEN `(?e1. &0 < e1 /\ (!t. abs t < e1 ==> azim (vec 0) (v 3) (f (v 4) t) (v 2) = azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) + azim (vec 0) (v 3) (f (v 0) t) (v 1) + azim (vec 0) (v 3) (v 1) (v 2) )) /\(?e1. &0 < e1 /\ (!t. abs t < e1 ==> azim (vec 0) (f (v 0) t) (v 1) (f (v 4) t) = azim (vec 0) (f (v 0) t) (v 1) (v 3) + azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) )) /\ (?e1. &0 < e1 /\ (!t. abs t < e1 ==> azim (vec 0) (v 1) (v 2) (f (v 0) t) = azim (vec 0) (v 1) (v 2) (v 3) + azim (vec 0) (v 1) (v 3) (f (v 0) t))) /\ (?e1. &0 < e1 /\ (!t. abs t < e1 ==> &0 < azim (vec 0) (f (v 0) t) (v 1) (v 3) /\ azim (vec 0) (f (v 0) t) (v 1) (v 3) < pi)) ==> (?e1. &0 < e1 /\ (!t. abs t < e1 ==> azim (vec 0) (v 3) (f (v 4) t) (v 2) = azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) + azim (vec 0) (v 3) (f (v 0) t) (v 1) + azim (vec 0) (v 3) (v 1) (v 2) /\ azim (vec 0) (f (v 0) t) (v 1) (f (v 4) t) = azim (vec 0) (f (v 0) t) (v 1) (v 3) + azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) /\ azim (vec 0) (v 1) (v 2) (f (v 0) t) = azim (vec 0) (v 1) (v 2) (v 3) + azim (vec 0) (v 1) (v 3) (f (v 0) t) /\ &0 < azim (vec 0) (f (v 0) t) (v 1) (v 3) /\ azim (vec 0) (f (v 0) t) (v 1) (v 3) < pi))` (GMATCH_SIMP_TAC);
1959 REPEAT WEAKER_STRIP_TAC;
1960 INTRO_TAC Cuxvzoz.epsilon_quad [`e1''`;`e1'''`;`e1''''`;`e1'''''`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
1961 TYPIFY `e''''` EXISTS_TAC;
1962 ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC THEN REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[];
1963 BY(ASM_MESON_TAC[]);
1964 BY(ASM_MESON_TAC[]);
1965 REWRITE_TAC[GSYM CONJ_ASSOC];
1966 COMMENT "azim bounds";
1967 TYPIFY `azim (vec 0) (v 0) (v 1) (v 3) < pi` (C SUBGOAL_THEN ASSUME_TAC);
1968 FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 4) < pi` MP_TAC;
1970 MATCH_MP_TAC (arith `&0 <= y ==> (x + y < pi ==> x < pi)`);
1971 BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
1972 TYPIFY `~coplanar {vec 0,v 0,v 1,v 3}` (C SUBGOAL_THEN ASSUME_TAC);
1973 REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
1974 BY(REPEAT (FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 3)` MP_TAC) THEN REAL_ARITH_TAC);
1975 TYPIFY `&0 < azim (vec 0) (v 3) (v 0) (v 1) /\ &0 < azim (vec 0) (v 1) (v 3) (v 0)` (C SUBGOAL_THEN ASSUME_TAC);
1976 REWRITE_TAC[Zlzthic.azim_pos_iff_nz];
1977 FIRST_X_ASSUM_ST `coplanar` MP_TAC;
1978 BY(MESON_TAC[Local_lemmas1.AZIM_COND_FOR_COPLANAR;SET_RULE `{a,b,c,d} = {a,d,b,c}`;SET_RULE `{a,b,c,d}={a,c,d,b}`]);
1979 INTRO_TAC Cuxvzoz.WNWSHJT_ALT [`v 3`;`v 0`;`v 1`;`f`;`-- e`;`e`;`pi - azim (vec 0) (v 0) (v 3) (v 4)`];
1981 ASM_REWRITE_TAC[arith `a < pi - b <=> a + b < pi`];
1983 MATCH_MP_TAC Zlzthic.deformation_subset;
1984 TYPIFY `IMAGE v (:num)` EXISTS_TAC;
1985 ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_UNIV];
1986 BY(MESON_TAC[FUN_IN_IMAGE;IN_UNIV]);
1987 REWRITE_TAC[CONJ_ASSOC];
1989 FIRST_X_ASSUM_ST `coplanar` MP_TAC;
1990 BY(MESON_TAC[Planarity.notcoplanar_imp_notcollinear_fan;SET_RULE `{a,b,c} = {a,c,b}`]);
1991 BY(REPEAT (FIRST_X_ASSUM_ST `x < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
1992 REPEAT WEAKER_STRIP_TAC;
1993 INTRO_TAC Cuxvzoz.WNWSHJT_ALT [`v 0`;`v 1`;`v 3`;`f`;`-- e`;`e`;`pi - azim (vec 0) (v 1) (v 2) (v 3)`];
1995 ASM_REWRITE_TAC[arith `a < pi - b <=> a + b < pi`];
1997 MATCH_MP_TAC Zlzthic.deformation_subset;
1998 TYPIFY `IMAGE v (:num)` EXISTS_TAC;
1999 ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY;IN_UNIV];
2000 BY(MESON_TAC[FUN_IN_IMAGE;IN_UNIV]);
2001 REWRITE_TAC[CONJ_ASSOC];
2003 FIRST_X_ASSUM_ST `coplanar` MP_TAC;
2004 BY(MESON_TAC[Planarity.notcoplanar_imp_notcollinear_fan;SET_RULE `{a,b,c} = {a,c,b}`]);
2005 BY(REPEAT (FIRST_X_ASSUM_ST `x < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
2006 REPEAT WEAKER_STRIP_TAC;
2007 COMMENT "034 triangle";
2008 TYPIFY `?e3. &0 < e3 /\ (!t. abs t < e3 ==> ~collinear {vec 0,f (v 0) t,f (v 4) t} /\ ~collinear {vec 0,f (v 0) t,f (v 3) t} /\ ~collinear {vec 0,f (v 0) t,f (v 1) t} /\ ~collinear {vec 0,f (v 4) t,f (v 3) t})` (C SUBGOAL_THEN ASSUME_TAC);
2009 FIRST_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`4`]) THEN ANTS_TAC THENL [REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC;REPEAT WEAKER_STRIP_TAC];
2010 FIRST_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`3`]) THEN ANTS_TAC THENL [REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC;REPEAT WEAKER_STRIP_TAC];
2011 FIRST_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`1`]) THEN ANTS_TAC THENL [REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC;REPEAT WEAKER_STRIP_TAC];
2012 FIRST_X_ASSUM_ST `collinear` (C INTRO_TAC [`4`;`3`]) THEN ANTS_TAC THENL [REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC;REPEAT WEAKER_STRIP_TAC];
2013 INTRO_TAC Cuxvzoz.epsilon_quad [`e1''`;`e1'''`;`e1''''`;`e1'''''`] THEN ANTS_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
2014 TYPIFY `e''''` EXISTS_TAC THEN CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
2015 BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]);
2016 FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
2017 TYPIFY `!i. f (v i) (&0) = v i` (C SUBGOAL_THEN ASSUME_TAC);
2018 FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation];
2019 REPEAT WEAKER_STRIP_TAC;
2020 BY(FIRST_X_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC FUN_IN_IMAGE THEN REWRITE_TAC[IN_UNIV]);
2021 REWRITE_TAC[CONJ_ASSOC] THEN SUBCONJ2_TAC;
2022 TYPIFY `?e2. &0 < e2 /\ (!t. abs t < e2 ==> azim (vec 0) (f (v 4) t) (f (v 0) t) (v 3) <= pi)` ASM_CASES_TAC;
2023 FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
2024 INTRO_TAC Cuxvzoz.epsilon_triple [`e1'`;`e3`;`e2`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2025 TYPIFY `e'''` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2026 REPLICATE_TAC 3 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2027 REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2028 TYPIFY `azim (vec 0) (f (v 0) t) (v 3) (f (v 4) t) <= pi /\ azim (vec 0) (v 3) (f (v 4) t) (f (v 0) t) <= pi /\ azim (vec 0) (v 0) (v 3) (v 4) <= pi /\ azim (vec 0) (v 3) (v 4) (v 0) <= pi /\ azim (vec 0) (v 4) (v 0) (v 3) <= pi` (C SUBGOAL_THEN ASSUME_TAC);
2029 FIRST_X_ASSUM MP_TAC THEN (FIRST_X_ASSUM_ST `x <= pi` (C INTRO_TAC [`4`]));
2030 NUM_REDUCE_TAC THEN ASM_REWRITE_TAC[];
2031 BY(MESON_TAC[Xivphks.FSQKWKK]);
2032 FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
2033 REPEAT (FIRST_X_ASSUM_ST `a <= pi` (ASSUME_TAC o (MATCH_MP (REWRITE_RULE[TAUT `(a /\ b /\ c ==> d) <=> (c ==> (a /\ b ==> d))`] azim_dih_y))));
2034 REPLICATE_TAC 6 (POP_ASSUM GMATCH_SIMP_TAC);
2036 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN ASM_REWRITE_TAC[];
2037 TYPIFY_GOAL_THEN `(~collinear {vec 0, v 0, v 4} /\ ~collinear {vec 0, v 3, v 4}) /\ (~collinear {vec 0, v 4, v 3} /\ ~collinear {vec 0, v 0, v 3}) /\ (~collinear {vec 0, v 3, v 0} /\ ~collinear {vec 0, v 4, v 0})` (unlist REWRITE_TAC);
2038 BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
2039 ASM_REWRITE_TAC[DIST_SYM];
2040 BY(REPEAT (FIRST_X_ASSUM_ST `dist` MP_TAC) THEN REWRITE_TAC[DIST_SYM;DIST_0] THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[]);
2043 FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[];
2044 COMMENT "second half of assumption. All angles 034 <=pi";
2045 TYPIFY `coplanar {vec 0, v 3, v 4, v 0}` ASM_CASES_TAC;
2046 TYPIFY `e1'` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2047 FIRST_X_ASSUM_ST `coplanar` (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2048 FIRST_X_ASSUM MP_TAC;
2049 TYPIFY `{vec 0, v 3, f (v 4) t, f (v 0) t} = {vec 0, f (v 4) t, f (v 0) t, v 3}` (C SUBGOAL_THEN SUBST1_TAC);
2051 REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
2052 BY(MP_TAC PI_POS THEN REAL_ARITH_TAC);
2053 POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {a,c,d,b}`] THEN REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR;DE_MORGAN_THM] THEN REPEAT WEAKER_STRIP_TAC;
2054 TYPIFY `&0 < azim (vec 0) (v 4) (v 0) (v 3) /\ azim (vec 0) (v 4) (v 0) (v 3) < pi` (C SUBGOAL_THEN ASSUME_TAC);
2055 REWRITE_TAC[arith `&0 < x <=> &0 <= x /\ ~(x = &0) `;arith `x < pi <=> x <= pi /\ ~(x = pi)`];
2056 REWRITE_TAC[Counting_spheres.AZIM_NN];
2058 FIRST_X_ASSUM_ST `a <= pi` (C INTRO_TAC [`4`]) THEN NUM_REDUCE_TAC;
2059 BY(ASM_REWRITE_TAC[]);
2060 TYPIFY `&0 < e` (C SUBGOAL_THEN ASSUME_TAC);
2061 FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation;IN_REAL_INTERVAL];
2063 INTRO_TAC Cuxvzoz.epsilon_pair [`e3`;`e`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2064 INTRO_TAC Zlzthic.WNWSHJT [`v 3`;`v 4`;`v 0`;`f`;`-- e'''`;`e'''`] THEN ASM_REWRITE_TAC[];
2066 TYPIFY_GOAL_THEN `~collinear {vec 0, v 4, v 0} /\ ~collinear {vec 0, v 4, v 3}` (unlist REWRITE_TAC);
2067 BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
2068 MATCH_MP_TAC Cuxvzoz.deformation_restrict;
2069 TYPIFY `e` EXISTS_TAC THEN ASM_REWRITE_TAC[];
2070 MATCH_MP_TAC Zlzthic.deformation_subset;
2071 TYPIFY `(IMAGE v (:num))` EXISTS_TAC;
2072 ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
2073 BY(GEN_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC FUN_IN_IMAGE THEN REWRITE_TAC[IN_UNIV]);
2074 BY(MESON_TAC[arith `x < pi ==> x <= pi`]);
2075 (REPEAT WEAKER_STRIP_TAC THEN REWRITE_TAC[GSYM CONJ_ASSOC]);
2076 COMMENT "azim additivity";
2078 INTRO_TAC Cuxvzoz.epsilon_triple [`e1`;`e1''`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2079 TYPIFY `e'''` EXISTS_TAC;
2080 ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2081 REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2082 REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2083 INTRO_TAC Cuxvzoz.azim_dominated_split [`(vec 0):real^3`;`v 3`;`v 4`;`v 1`;`v 2`;`(vec 0):real^3`;`v 3`;`f (v 4) t`;`v 1`;`v 2`];
2084 INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`3`;`4`];
2085 ASM_REWRITE_TAC[LET_THM;arith `SUC 3 = 4 /\ 3 + 4 = 7 /\ 3 + 3 = 6 /\ 3 <= 5 /\ 0 < 3 /\ 3 < 4 /\ 4 < 5`];
2086 DISCH_THEN (SUBST1_TAC o GSYM) THEN ASM_REWRITE_TAC[arith `x <= x`];
2087 INTRO_TAC Cuxvzoz.azim_dominated_split [`(vec 0):real^3`;`v 3`;`v 4`;`v 0`;`v 1`;`(vec 0):real^3`;`v 3`;`f (v 4) t`;`f (v 0) t`;`v 1`];
2088 ASM_REWRITE_TAC[arith `x <= x`];
2089 INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`3`;`2`;`3`];
2090 NUM_REDUCE_TAC THEN ASM_REWRITE_TAC[LET_THM];
2092 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN ASM_REWRITE_TAC[];
2093 TYPIFY_GOAL_THEN `~collinear {vec 0, v 1, v 3} /\ ~collinear {vec 0, v 1, v 3} /\ ~collinear {vec 0, v 2, v 3}` (unlist REWRITE_TAC);
2094 BY(REPEAT CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
2095 BY(REPLICATE_TAC 15 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2096 COMMENT "azim 0 additive";
2097 REPEAT WEAKER_STRIP_TAC;
2099 INTRO_TAC Cuxvzoz.epsilon_triple [`e'`;`e1''`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2100 TYPIFY `e''''` EXISTS_TAC;
2101 ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2102 REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2103 REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2104 MATCH_MP_TAC Fan.sum3_azim_fan;
2106 BY(REPLICATE_TAC 15 (FIRST_X_ASSUM MP_TAC) THEN MP_TAC PI_POS THEN REAL_ARITH_TAC);
2107 REPEAT WEAKER_STRIP_TAC;
2108 COMMENT "azim 1 additive";
2110 INTRO_TAC Cuxvzoz.epsilon_pair [`e''`;`e3`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2111 TYPIFY `e'''` EXISTS_TAC;
2112 ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2113 REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2114 REPEAT (FIRST_X_ASSUM_ST `abs t < e` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2115 MATCH_MP_TAC Fan.sum3_azim_fan;
2118 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MP_TAC PI_POS THEN REAL_ARITH_TAC);
2119 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
2121 BY(CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
2122 REPEAT WEAKER_STRIP_TAC;
2123 COMMENT "pi bounds";
2125 TYPIFY `e'` EXISTS_TAC;
2126 CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
2127 TYPIFY ` &0 < azim (vec 0) (f (v 0) t) (f (v 1) t) (f (v 3) t) /\ azim (vec 0) (f (v 0) t) (f (v 1) t) (f (v 3) t) < pi - azim (vec 0) (v 0) (v 3) (v 4)` ENOUGH_TO_SHOW_TAC;
2129 MATCH_MP_TAC (arith `&0 <= b ==> (&0 < a /\ a < pi - b ==> &0 < a /\ a < pi)`);
2130 BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
2131 FIRST_X_ASSUM MATCH_MP_TAC;
2132 BY(ASM_REWRITE_TAC[]);
2133 MATCH_MP_TAC Oxl_def.periodic_numseg;
2134 TYPIFY `5` EXISTS_TAC;
2135 REWRITE_TAC[arith `~(5 = 0)`];
2137 FIRST_X_ASSUM_ST `periodic` MP_TAC;
2138 REWRITE_TAC[Oxl_def.periodic];
2139 REWRITE_TAC[arith `(i+5)+j = (i+j)+5`];
2140 BY(DISCH_THEN (unlist REWRITE_TAC));
2141 REWRITE_TAC[IN_NUMSEG;arith `(0 <= i /\ i <= 5-1) <=> (i = 0 \/ i = 1 \/ i = 2 \/ i = 3 \/ i = 4)`];
2142 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN NUM_REDUCE_TAC;
2143 EXISTS_TAC `&1` THEN REPEAT (FIRST_X_ASSUM_ST `azim (vec 0) (v 0) (v 1) (v 4) < pi` MP_TAC);
2144 BY(MESON_TAC[arith `&0 < &1`;arith `x < pi ==> ~(x=pi)`]);
2145 REPEAT (FIRST_X_ASSUM_ST `+` kill);
2146 ASM_REWRITE_TAC[] THEN EXISTS_TAC `&1` THEN REPEAT (FIRST_X_ASSUM_ST `azim (vec 0) (v 1) (v 2) (v 0) < pi` MP_TAC);
2147 BY(MESON_TAC[arith `&0 < &1`;arith `x < pi ==> ~(x=pi)`]);
2148 BY(ASM_REWRITE_TAC[] THEN EXISTS_TAC `&1` THEN MESON_TAC[arith `&0 < &1`;arith `x <= x`]);
2149 INTRO_TAC Cuxvzoz.epsilon_triple [`e1'''`;`e1''`;`e1`] THEN ANTS_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
2150 TYPIFY `e'''` EXISTS_TAC THEN CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
2151 REPLICATE_TAC 3(FIRST_X_ASSUM (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC);
2152 REPEAT (FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2154 FIRST_X_ASSUM_ST `a = pi` (SUBST1_TAC o GSYM);
2156 BY(REPLICATE_TAC 15 (FIRST_X_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
2157 TYPIFY `e1''` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2158 FIRST_X_ASSUM_ST `azim a b c d = azim a' b' c' d'` (C INTRO_TAC [`t`]);
2159 BY(ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[arith `x <= x`])
2163 let L13_LEMMA = prove_by_refinement(
2164 `main_nonlinear_terminal_v11
2166 (!V E FF s v. IMAGE (\i. v i,v (SUC i)) (:num) = FF
2172 /\ IMAGE v (:num) = V
2173 /\ IMAGE (\i. {v i, v (SUC i)}) (:num) = E
2174 /\ ~coplanar {vec 0, v 1, v 2, v 0}
2175 ==> &0 < azim (vec 0) (v 0) (v 1) (v 3) )`,
2178 REPEAT WEAKER_STRIP_TAC;
2179 REWRITE_TAC[arith `&0 < a <=> ~(a = &0) /\ (&0 <= a)`];
2180 REWRITE_TAC[Counting_spheres.AZIM_NN];
2182 FIRST_X_ASSUM_ST `coplanar {vec 0,v 1 ,v 2,v 0}` MP_TAC;
2184 INTRO_TAC EGHNAVX_SCS [`s`;`5`;`v`;`0`];
2185 ASM_REWRITE_TAC[LET_THM];
2187 REPEAT WEAKER_STRIP_TAC;
2189 FIRST_X_ASSUM (C INTRO_TAC [`3`;`2`]);
2192 REPEAT WEAKER_STRIP_TAC;
2193 REWRITE_TAC[coplanar];
2194 GEXISTL_TAC [`(vec 0):real^3`;`v 0`;`v 1`];
2195 TYPIFY `{vec 0, v 0, v 1} SUBSET affine hull {vec 0, v 0, v 1} /\ v 2 IN affine hull {vec 0, v 0, v 1}` ENOUGH_TO_SHOW_TAC;
2197 REWRITE_TAC[HULL_SUBSET];
2198 INTRO_TAC AFF_GT_SUBSET_AFFINE_HULL [`{vec 0,v 0}`;`{v 1}`];
2199 TYPIFY `{vec 0, v 0} UNION {v 1} = {vec 0, v 0, v 1}` (C SUBGOAL_THEN SUBST1_TAC);
2201 BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[])
2205 let IUNBUIG = prove_by_refinement(
2206 `main_nonlinear_terminal_v11 ==>
2208 IMAGE (\i. (v i,v (SUC i))) (:num) = FF /\
2214 (!i j. scs_diag 5 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4 * h0 < scs_b_v39 s i j) /\
2215 scs_a_v39 s 0 1 = &2 /\
2216 scs_b_v39 s 0 1 <= cstab /\
2217 interior_angle1 (vec 0) FF (v 0) < pi /\ interior_angle1 (vec 0) FF (v 1) < pi /\
2218 (!i. ~(i MOD 5 = 0) ==> dist(v i,v (i+1)) = &2) /\
2219 xrr (norm (v 0)) (norm (v 3)) (dist(v 0,v 3)) <= #15.53 /\
2220 xrr (norm (v 1)) (norm (v 3)) (dist(v 1,v 3)) <= #15.53 ==>
2221 dist(v 0,v 1) = &2)`,
2224 REPEAT WEAKER_STRIP_TAC;
2225 TYPIFY `BBprime2_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
2226 BY(ASM_MESON_TAC[Appendix.scs_basic;Ayqjtmd.unadorned_MMs]);
2227 TYPIFY `BBprime_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
2228 BY(ASM_MESON_TAC[Appendix.BBprime2_v39]);
2229 TYPIFY `BBs_v39 s v` (C SUBGOAL_THEN ASSUME_TAC);
2230 BY(ASM_MESON_TAC[Appendix.BBprime_v39]);
2231 INTRO_TAC Appendix.BBs_v39 [`s`;`v`];
2232 ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;Terminal.IMAGE_SUBSET_IN;IN_UNIV;arith `~(5 <= 3)`];
2233 REPEAT WEAKER_STRIP_TAC;
2234 TYPED_ABBREV_TAC `V = IMAGE v (:num)`;
2235 TYPED_ABBREV_TAC `E = IMAGE (\i. {v i, v (SUC i)}) (:num)`;
2236 TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
2237 MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
2238 BY(ASM_REWRITE_TAC[]);
2239 TYPIFY `!i. v i IN V` (C SUBGOAL_THEN ASSUME_TAC);
2240 REPEAT WEAKER_STRIP_TAC;
2242 REWRITE_TAC[IN_IMAGE;IN_UNIV];
2244 INTRO_TAC Cuxvzoz.BBs_inj [`s`;`v`;`5`];
2247 TYPIFY `!i. interior_angle1 (vec 0) FF (v i) = azim (vec 0) (v i) (v (i+1)) (v (i+4))` (C SUBGOAL_THEN ASSUME_TAC);
2250 GMATCH_SIMP_TAC (REWRITE_RULE[LET_THM] (GSYM Ocbicby.INTERIOR_ANGLE1_AZIM));
2251 TYPIFY `s` EXISTS_TAC;
2252 BY(ASM_REWRITE_TAC[IN;arith `5 - 1 = 4`;arith `3 < 5`;arith `SUC i = i+1`]);
2253 INTRO_TAC Ocbicby.LOCAL_FAN_AZIM_POS [`s`;`v`];
2254 ASM_REWRITE_TAC[LET_THM;IN;arith `5-1 = 4`;arith `SUC i = i+1`];
2256 TYPIFY `!i. v (i MOD 5) = v i` (C SUBGOAL_THEN ASSUME_TAC);
2258 MATCH_MP_TAC (GSYM Oxl_def.periodic_mod);
2259 BY(ASM_REWRITE_TAC[arith `~(0=5)`]);
2260 TYPIFY `v 5 = v 0 /\ v 6 = v 1 /\ v 7 = v 2 /\ v 8 = v 3 /\ v 9 = v 4` (C SUBGOAL_THEN ASSUME_TAC);
2261 FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
2262 BY(REWRITE_TAC[Ocbicby.MOD_5_EXPLICIT;arith `8 = 1*5 + 3`;arith `9 = 1*5 + 4`;MOD_MULT_ADD]);
2263 TYPIFY `~coplanar {vec 0, v 0,v 1,v 4} /\ ~coplanar {vec 0,v 1,v 2,v 0}` (C SUBGOAL_THEN ASSUME_TAC);
2264 ASM_REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
2265 BY(ASM_MESON_TAC[arith `x < pi ==> ~(x = pi)`;arith `&0 < a ==> ~(a = &0)`;arith `0+i=i`;arith `1+1=2 /\ 1+4=5`]);
2266 TYPIFY `generic V E` (C SUBGOAL_THEN ASSUME_TAC);
2267 BY(FIRST_X_ASSUM_ST `scs_generic` MP_TAC THEN ASM_REWRITE_TAC[Appendix.scs_generic]);
2268 INTRO_TAC Terminal.vv_split_azim_generic [`v`;`5`;`0`;`3`;`4`];
2270 ASM_REWRITE_TAC[LET_THM];
2272 COMMENT "collinearity";
2273 TYPIFY `!i j. ~(v i = v j) ==> ~collinear {vec 0,v i, v j}` (C SUBGOAL_THEN ASSUME_TAC);
2274 REPEAT GEN_TAC THEN DISCH_TAC;
2275 MATCH_MP_TAC Zlzthic.PROPERTIES_GENERIC_LOCAL_FAN_ALT;
2276 GEXISTL_TAC [`IMAGE v (:num)`;`IMAGE (\i. {v i, v (SUC i)}) (:num)`;`IMAGE (\i. (v i, v (SUC i))) (:num)`];
2277 ASM_REWRITE_TAC[IN_IMAGE;IN_UNIV];
2279 TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(i = j) ==> ~(v i = v j)` (C SUBGOAL_THEN ASSUME_TAC);
2280 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
2281 COMMENT "non coplanar 013 digression";
2282 INTRO_TAC (UNDISCH L13_LEMMA) [`V`;`E`;`FF`;`s`;`v`];
2285 REPEAT (FIRST_X_ASSUM_ST `interior_angle1 a b c < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN NUM_REDUCE_TAC;
2286 REPEAT WEAKER_STRIP_TAC;
2287 TYPIFY `azim (vec 0) (v 0) (v 1) (v 3) < pi` (C SUBGOAL_THEN ASSUME_TAC);
2288 FIRST_X_ASSUM_ST `+` MP_TAC;
2289 MATCH_MP_TAC (arith `&0 <= a2 /\ a < pi ==> (a = a1 + a2 ==> a1 < pi)`);
2290 REWRITE_TAC[Counting_spheres.AZIM_NN];
2291 BY(ASM_REWRITE_TAC[]);
2292 TYPIFY `~coplanar {vec 0,v 0, v 1,v 3}` (C SUBGOAL_THEN ASSUME_TAC);
2293 REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
2294 BY(REPLICATE_TAC 4 (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2295 COMMENT "introduce deformation";
2296 INTRO_TAC deform_pent_exists [`V`;`(\t. -- abs t)`;`v 3`;`v 4`;`v 0`;`v 1`;`&1`];
2298 REPEAT WEAKER_STRIP_TAC;
2299 FIRST_X_ASSUM MP_TAC;
2301 REWRITE_TAC[arith `&0 < &1`;arith `--abs (&0) = &0`];
2304 INTRO_TAC coplanar_cross_reduction [`s`;`5`;`v`;`3`];
2306 BY(ASM_REWRITE_TAC[]);
2308 FIRST_X_ASSUM MP_TAC;
2309 BY(MESON_TAC[SET_RULE `{a,b,c,d} = {a,d,b,c}`]);
2311 BY(REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
2313 INTRO_TAC (GEN_ALL Local_lemmas.CONVEX_LOFA_IMP_INANGLE_LE_PI) [`E`;`V`;`FF`;`v 4`];
2316 BY(ASM_REWRITE_TAC[]);
2318 INTRO_TAC Trigonometry.JBDNJJB [`v 0`;`v 1`;`v 3`];
2319 TYPIFY `v 0 dot (v 1 cross v 3) = ((v 0 cross v 1) dot v 3)` (C SUBGOAL_THEN SUBST1_TAC);
2321 REWRITE_TAC[arith `x > &0 <=> &0 < x`];
2322 ONCE_REWRITE_TAC[Leaf_cell.RE_EQVL_SYM];
2323 REWRITE_TAC[Trigonometry2.re_eqvl];
2324 REPEAT WEAKER_STRIP_TAC;
2326 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
2327 BY(ASM_REWRITE_TAC[Cuxvzoz.sin_azim_pos]);
2328 GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
2329 REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL];
2330 REPEAT WEAKER_STRIP_TAC;
2331 MATCH_MP_TAC REAL_CONTINUOUS_NEG;
2332 BY(REWRITE_TAC[Cuxvzoz.real_continuous_abs]);
2333 REPEAT WEAKER_STRIP_TAC;
2334 (COMMENT "reduction lemmas");
2336 TYPIFY `&2 < dist(v 0,v 1)` (C SUBGOAL_THEN ASSUME_TAC);
2337 FIRST_X_ASSUM_ST `scs_a_v39` (C INTRO_TAC [`0`;`1`]);
2338 BY(ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
2339 FIRST_X_ASSUM_ST `~` MP_TAC THEN REWRITE_TAC[];
2340 TYPIFY `!i. f (v i) (&0) = v i` (C SUBGOAL_THEN ASSUME_TAC);
2341 FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation];
2342 BY(ASM_MESON_TAC[]);
2343 INTRO_TAC a5_assumption_reduction [`s`;`f`;`v`;`e'`];
2347 REPEAT WEAKER_STRIP_TAC;
2348 FIRST_X_ASSUM_ST `scs_diag` (C INTRO_TAC [`i`;`j`]);
2349 BY(ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);
2351 TYPIFY `e'` EXISTS_TAC THEN CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
2352 FIRST_X_ASSUM (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[DIST_SYM];
2354 INTRO_TAC Cuxvzoz.continuous_nbd_pos [`\ t. dist(f (v 0) t,v 1) - &2`;`&0`];
2355 ASM_REWRITE_TAC[arith `abs (t' - &0) = abs t'`;arith `&0 < a - b <=> b < a`];
2357 FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation];
2358 REPEAT WEAKER_STRIP_TAC;
2359 FIRST_X_ASSUM_ST `atreal` (C INTRO_TAC [`v 0`;`&0`]);
2362 BY((REPEAT (REPEAT CONJ_TAC THEN (MATCH_MP_TAC REAL_CONTINUOUS_ADD ORELSE MATCH_MP_TAC Local_lemmas1.CON_ATREAL_REAL_CON ORELSE MATCH_MP_TAC Local_lemmas1.CON_ATREAL_REAL_CON2 ORELSE MATCH_MP_TAC REAL_CONTINUOUS_MUL ORELSE MATCH_MP_TAC REAL_CONTINUOUS_POW ORELSE MATCH_MP_TAC REAL_CONTINUOUS_SUB THEN ASM_REWRITE_TAC[REAL_CONTINUOUS_CONST;ETA_AX]))));
2363 BY(MESON_TAC[arith `x < y ==> x <= y`]);
2365 (COMMENT "b5 reduction");
2366 INTRO_TAC b5_assumption_reduction [`s`;`f`;`v`;`e'`];
2370 BY(ASM_MESON_TAC[]);
2372 TYPIFY `e'` EXISTS_TAC;
2373 FIRST_X_ASSUM_ST `norm` MP_TAC THEN ASM_REWRITE_TAC[DIST_SYM];
2375 TYPIFY `e'` EXISTS_TAC;
2376 CONJ_TAC THENL [ASM_REWRITE_TAC[];REPEAT WEAKER_STRIP_TAC];
2377 FIRST_X_ASSUM_ST `norm` (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[DIST_SYM];
2378 DISCH_THEN (unlist REWRITE_TAC);
2381 COMMENT "deform collinear";
2382 TYPIFY `!t. f (v 1) t = v 1 /\ f (v 2) t = v 2 /\ f (v 3) t = v 3` (C SUBGOAL_THEN ASSUME_TAC);
2383 BY(GEN_TAC THEN REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN NUM_REDUCE_TAC);
2384 TYPIFY `!i j. i < 5 /\ j < 5 /\ ~(v i = v j) ==> (?e. &0 < e /\ (!t. abs t < e==> ~collinear {vec 0, f (v i) t, f (v j) t}))` (C SUBGOAL_THEN ASSUME_TAC);
2385 REPEAT WEAKER_STRIP_TAC;
2386 INTRO_TAC (GEN_ALL Local_lemmas1.CONTINUOUS_PRESERVE_COLLINEAR) [`&0`;`(vec 0):real^3`;`f (v i)`;`f (v j)`];
2387 REWRITE_TAC[arith `abs(&0 - r') = abs r'`] THEN DISCH_THEN MATCH_MP_TAC;
2389 FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation];
2390 REPEAT WEAKER_STRIP_TAC;
2391 REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC;
2392 BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
2393 FIRST_X_ASSUM MATCH_MP_TAC;
2394 FIRST_X_ASSUM MATCH_MP_TAC;
2395 BY(ASM_MESON_TAC[]);
2396 TYPIFY `!i. azim (vec 0) (v i) (v (i+1)) (v(i+4)) <= pi` (C SUBGOAL_THEN ASSUME_TAC);
2397 REWRITE_TAC[arith `i+1 = SUC i`;arith `4 = 5 - 1`];
2399 MATCH_MP_TAC (REWRITE_RULE[LET_THM] Terminal.convex_local_fan_azim_le_pi);
2400 ASM_REWRITE_TAC[arith `3 <= 5`];
2401 FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM];
2402 BY(ASM_REWRITE_TAC[]);
2404 INTRO_TAC Zlzthic.NONPLANAR_OPEN [`(\ (t:real). (vec 0):real^3)`;`f (v 0)`;`\ (t:real). v 1`;`\ (t:real). v 3`;`&0`];
2405 ASM_REWRITE_TAC[CONTINUOUS_CONST];
2407 FIRST_X_ASSUM_ST `deformation` MP_TAC THEN REWRITE_TAC[Localization.deformation] THEN REPEAT WEAKER_STRIP_TAC;
2408 BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
2409 REWRITE_TAC[arith `abs (&0 - t') = abs t'`] THEN REPEAT WEAKER_STRIP_TAC;
2410 COMMENT "azim reduction";
2411 INTRO_TAC azim5_reduction [`s`;`f`;`v`;`e'`];
2415 BY(REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `a < pi` MP_TAC) THEN ASM_REWRITE_TAC[] THEN MESON_TAC[]);
2417 TYPIFY `e'` EXISTS_TAC;
2418 BY(ASM_REWRITE_TAC[arith `x - abs t = x + --abs t`]);
2419 INTRO_TAC Zlzthic.WNWSHJT [`v 1`;`v 3`;`v 0`;`f`;`-- e'`;`e'`];
2423 MATCH_MP_TAC Zlzthic.deformation_subset;
2424 TYPIFY `V` EXISTS_TAC;
2425 ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
2426 BY(EXPAND_TAC "V" THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC FUN_IN_IMAGE THEN REWRITE_TAC[IN_UNIV]);
2427 TYPIFY_GOAL_THEN `~collinear {vec 0, v 3, v 0} /\ ~collinear {vec 0, v 3, v 1}` (unlist REWRITE_TAC);
2428 BY(CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
2429 FIRST_X_ASSUM_ST `coplanar` kill;
2430 FIRST_X_ASSUM_ST `~coplanar s` MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {a,d,b,c}`] THEN REWRITE_TAC[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR];
2431 REWRITE_TAC[arith `&0 < a <=> &0 <= a /\ ~(a = &0)`];
2432 REWRITE_TAC[Counting_spheres.AZIM_NN];
2433 REWRITE_TAC[arith `a < pi <=> a <= pi /\ ~(a = pi)`;DE_MORGAN_THM];
2434 DISCH_THEN (unlist REWRITE_TAC);
2435 REPLICATE_TAC 2(MATCH_MP_TAC Xivphks.FSQKWKK);
2436 FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`0`]) THEN NUM_REDUCE_TAC THEN ASM_REWRITE_TAC[];
2437 MATCH_MP_TAC (arith `&0 <= a2 ==> (a1 + a2 <= pi ==> a1 <= pi)`);
2438 BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
2439 (REPEAT WEAKER_STRIP_TAC);
2440 INTRO_TAC Cuxvzoz.epsilon_triple [`e`;`e''`;`e'`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2441 TYPIFY `e''''` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2442 REPLICATE_TAC 3 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2443 INTRO_TAC azim_dih_y [`(vec 0):real^3`;`v 3`;`f (v 0) t`;`v 1`];
2444 INTRO_TAC azim_dih_y [`(vec 0):real^3`;`v 3`;`(v 0)`;`v 1`];
2445 DISCH_THEN GMATCH_SIMP_TAC;
2447 FIRST_X_ASSUM_ST `x < pi` (C INTRO_TAC [`&0`]) THEN ASM_REWRITE_TAC[arith `abs(&0) = &0`];
2448 SIMP_TAC[arith `x < pi ==> x <= pi`];
2450 BY(CONJ_TAC THEN REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
2451 DISCH_THEN GMATCH_SIMP_TAC;
2453 REWRITE_TAC[CONJ_ASSOC] THEN CONJ2_TAC;
2454 MATCH_MP_TAC (arith `x < pi ==> x <= pi`);
2455 BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
2457 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
2458 BY(FIRST_X_ASSUM_ST `coplanar` (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[] THEN MESON_TAC[Planarity.notcoplanar_imp_notcollinear_fan]);
2459 BY(REPEAT (FIRST_X_ASSUM MATCH_MP_TAC) THEN NUM_REDUCE_TAC);
2460 FIRST_X_ASSUM_ST `norm` (C INTRO_TAC [`t`]);
2461 ASM_REWRITE_TAC[DIST_SYM;DIST_0];
2462 REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[];
2463 MATCH_MP_TAC Ocbicby.dih_y_mono;
2464 FIRST_X_ASSUM_ST `~coplanar s` (C INTRO_TAC [`t`]) THEN ASM_REWRITE_TAC[];
2465 FIRST_X_ASSUM_ST `~coplanar s` MP_TAC;
2466 REPEAT WEAKER_STRIP_TAC;
2467 REWRITE_TAC[arith `d + -- abs t <= d`];
2469 REWRITE_TAC[NORM_POS_LT];
2470 POP_ASSUM (MP_TAC o (MATCH_MP Planarity.notcoplanar_disjoint));
2473 FIRST_X_ASSUM_ST `abs` (SUBST1_TAC o GSYM);
2474 REWRITE_TAC[GSYM DIST_NZ];
2475 POP_ASSUM (MP_TAC o (MATCH_MP Planarity.notcoplanar_disjoint));
2478 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[Oxlzlez.coplanar_delta_y;DIST_SYM;DIST_0];
2479 BY(MESON_TAC[Merge_ineq.delta_y_sym]);
2480 INTRO_TAC Terminal.DELTA_Y_POS_4POINTS [`(vec 0):real^3`;`v 3`;`v 0`;`v 1`];
2481 BY(REWRITE_TAC[DIST_0;DIST_SYM]);
2482 REPEAT WEAKER_STRIP_TAC;
2483 (COMMENT "end of azim reduction");
2484 COMMENT "deformation in BBs";
2485 INTRO_TAC Cuxvzoz.deformation_BBs_ALT [`s`;`5`;`f`;`v`;`e'`];
2489 MATCH_MP_TAC Terminal.periodic_mod_reduce;
2490 TYPIFY `5` EXISTS_TAC THEN REWRITE_TAC[arith `~(5 = 0)`];
2492 FIRST_X_ASSUM_ST `periodic` MP_TAC THEN REWRITE_TAC[Oxl_def.periodic];
2494 REWRITE_TAC[arith `i < 5 <=> i = 0 \/ i = 1 \/ i = 2 \/ i = 3 \/ i = 4`];
2495 REPEAT WEAKER_STRIP_TAC THEN (FIRST_X_ASSUM_ST `norm` (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2496 BY(FIRST_X_ASSUM_ST ` \/ ` MP_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);
2497 REPEAT WEAKER_STRIP_TAC;
2498 COMMENT "back to root, next tau";
2499 TYPIFY `!t. abs t < e'' ==> sum {i | i < 5} (\i. rho_fun (norm (v i)) * azim (vec 0) (v i) (v (i + 1)) (v (i + 5 - 1))) <= sum {i | i < 5} (\i. rho_fun (norm (f (v i) t)) * azim (vec 0) (f (v i) t) (f(v(i+1)) t) (f (v (i + 5 - 1)) t))` (C SUBGOAL_THEN ASSUME_TAC);
2500 REPEAT WEAKER_STRIP_TAC;
2501 MATCH_MP_TAC Cuxvzoz.MMs_minimize_tau_fun;
2502 TYPIFY `s` EXISTS_TAC;
2503 ASM_REWRITE_TAC[arith `3 < 5`];
2504 FIRST_X_ASSUM MATCH_MP_TAC;
2505 BY(FIRST_X_ASSUM (unlist REWRITE_TAC));
2507 TYPIFY `{i | i < 5} = 0..4` (C SUBGOAL_THEN SUBST1_TAC);
2508 BY(REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG] THEN ARITH_TAC);
2509 REWRITE_TAC[SUM_NUMSEG4];
2512 COMMENT "introduce nonlinear 684";
2513 TYPIFY `scs_diag 5 0 2 /\ scs_diag 5 0 3 /\ scs_diag 5 1 3 /\ scs_diag 5 1 4 /\ scs_diag 5 2 4` (C SUBGOAL_THEN ASSUME_TAC);
2514 BY(REWRITE_TAC[Appendix.scs_diag;Uxckfpe.ARITH_5_TAC]);
2515 INTRO_TAC (UNDISCH Ocbicby.LEMMA_6843920790) [`norm (v 3)`;`norm (v 0)`;`norm (v 1)`;`dist(v 0,v 1)`;`dist (v 1,v 3)`;`dist(v 0,v 3)`];
2518 ONCE_REWRITE_TAC[Ocbicby.xrr_sym];
2519 ASM_REWRITE_TAC[GSYM Sphere.cstab];
2520 TYPIFY_GOAL_THEN `(&2 <= norm (v 3) /\ norm (v 3) <= &2 * h0) /\ (&2 <= norm (v 0) /\ norm (v 0) <= &2 * h0) /\ (&2 <= norm (v 1) /\ norm (v 1) <= &2 * h0)` (unlist REWRITE_TAC);
2521 REWRITE_TAC[GSYM Fnjlbxs.in_ball_annulus];
2522 FIRST_X_ASSUM_ST `BBs_v39` kill THEN FIRST_X_ASSUM_ST `BBs_v39` MP_TAC THEN REWRITE_TAC[Appendix.BBs_v39;LET_THM] THEN EXPAND_TAC "V" THEN REPEAT WEAKER_STRIP_TAC;
2523 FIRST_X_ASSUM_ST `ball_annulus` MP_TAC;
2524 REWRITE_TAC[SUBSET;IN_IMAGE;IN_UNIV];
2526 REWRITE_TAC[ CONJ_ASSOC] THEN CONJ2_TAC;
2527 INTRO_TAC Oxlzlez.coplanar_delta_y [`(vec 0):real^3`;`v 3`;`v 0`;`v 1`];
2528 REWRITE_TAC[DIST_0;DIST_SYM] THEN DISCH_THEN (SUBST1_TAC o GSYM);
2529 BY(ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {a,c,d,b}`] THEN ASM_REWRITE_TAC[]);
2530 TYPIFY_GOAL_THEN `(&2 <= dist (v 0,v 1) /\ dist (v 0,v 1) <= cstab)` (unlist REWRITE_TAC);
2531 REPEAT (FIRST_X_ASSUM_ST `scs_a_v39` (C INTRO_TAC [`0`;`1`])) THEN FIRST_X_ASSUM_ST `scs_a_v39 s 0 1 = &2` MP_TAC THEN FIRST_X_ASSUM_ST `scs_b_v39 s 0 1 <= cstab` MP_TAC;
2534 REPEAT (FIRST_X_ASSUM_ST `scs_a_v39` (C INTRO_TAC [`1`;`3`]) );
2535 BY(ASM_REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC);
2536 REPEAT (FIRST_X_ASSUM_ST `scs_a_v39` (C INTRO_TAC [`0`;`3`]) );
2537 BY(ASM_REWRITE_TAC[Sphere.cstab] THEN REAL_ARITH_TAC);
2538 REPEAT WEAKER_STRIP_TAC;
2540 FIRST_X_ASSUM_ST `IN` MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM;TAUT `~(a ==> b) <=> (a /\ ~b)`;arith `~(a < b) <=> b <= a`];
2541 TYPIFY `?e2. &0 < e2 /\ (!t. abs t < e2 ==> dist(v 0,v 1) + t IN real_interval(a,b))` (C SUBGOAL_THEN MP_TAC);
2542 INTRO_TAC Zlzthic.real_interval_contains_0_ball [`a-dist(v 0,v 1)`;`b - dist(v 0,v 1)`;`&1`];
2543 REWRITE_TAC[arith `&0 < &1`;arith `a - d < &0 <=> a < d`;arith `&0 < b - d <=> d < b`];
2545 FIRST_X_ASSUM_ST `dist s IN real_interval (a,b)` MP_TAC;
2546 BY(REWRITE_TAC[IN_REAL_INTERVAL]);
2547 REPEAT WEAKER_STRIP_TAC;
2548 TYPIFY `e'''` EXISTS_TAC;
2549 (ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC THEN (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_REAL_INTERVAL]);
2551 REPEAT WEAKER_STRIP_TAC;
2552 TYPIFY `?t. (t < &0) /\ abs t < e2 /\ taum (norm (v 3)) (norm (v 0)) (norm (v 1)) (dist(v 0, v 1)) (dist (v 1,v 3)) (dist (v 0,v 3)) <= taum (norm (v 3)) (norm (v 0)) (norm (v 1)) (dist (v 0,v 1) + t) (dist (v 1,v 3)) (dist (v 0,v 3))` ENOUGH_TO_SHOW_TAC;
2553 REPEAT WEAKER_STRIP_TAC;
2554 GEXISTL_TAC [`dist(v 0,v 1) + t`;`dist(v 0,v 1)`];
2557 BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2558 FIRST_X_ASSUM MATCH_MP_TAC;
2559 BY(ASM_REWRITE_TAC[]);
2560 COMMENT "choose epsilon and t";
2561 INTRO_TAC epsilon_hex [`e`;`e'`;`e''`;`e1`;`e1'`;`e2`] THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2562 TYPIFY `?t. t < &0 /\ abs t < e6` (C SUBGOAL_THEN MP_TAC);
2563 TYPIFY `-- e6 / &2` EXISTS_TAC;
2564 BY(FIRST_X_ASSUM_ST `&0 < e6` MP_TAC THEN REAL_ARITH_TAC);
2565 REPEAT WEAKER_STRIP_TAC;
2566 REPLICATE_TAC 6 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2567 TYPIFY `t` EXISTS_TAC THEN ASM_REWRITE_TAC[];
2568 REPLICATE_TAC 8 (FIRST_X_ASSUM (C INTRO_TAC [`t`])) THEN ASM_REWRITE_TAC[] THEN REPEAT WEAKER_STRIP_TAC;
2569 FIRST_X_ASSUM_ST `rho_fun` MP_TAC THEN ASM_REWRITE_TAC[Appendix.rho_rho_fun];
2570 REWRITE_TAC[arith `r0 * (a013 + a034) + r1 * (a123 + a130) + r2 * a231 + r3 * (a340 + a301+a312) + r4 * a403 <= r0 * (f013 + a034) + r1 * (a123 + f130) + r2 * a231 + r3 *(a340+f301 +a312) + r4*a403 <=> r0 * a013 + r1*a130 + r3* a301 <= r0 * f013 + r1 * f130 + r3 * f301`];
2571 MATCH_MP_TAC (arith `a - (pi+sol0) = a' /\ b - (pi+sol0) = b' ==> (a <= b ==> a' <= b')`);
2572 REWRITE_TAC[arith `(a + b+c) - (pi + sol0) = a + b + c - (pi + sol0)`];
2574 GMATCH_SIMP_TAC (GSYM Cuxvzoz.tau3_azim);
2575 GMATCH_SIMP_TAC Cuxvzoz.tau3_taum_nonplanar;
2577 REWRITE_TAC[DIST_SYM];
2579 BY(MESON_TAC[Terminal.taum_sym]);
2580 BY(REPEAT (FIRST_X_ASSUM_ST `a < pi` MP_TAC) THEN REAL_ARITH_TAC);
2581 FIRST_X_ASSUM_ST `norm a = norm b` (SUBST1_TAC o GSYM);
2582 TYPIFY `dist(v 0,v 1) + t = dist(v 0,v 1) + -- abs t` (C SUBGOAL_THEN SUBST1_TAC);
2583 BY(FIRST_X_ASSUM_ST `t < &0` MP_TAC THEN REAL_ARITH_TAC);
2584 FIRST_X_ASSUM_ST `d = d' + -- abs t` (SUBST1_TAC o GSYM);
2585 GMATCH_SIMP_TAC (GSYM Cuxvzoz.tau3_azim);
2586 GMATCH_SIMP_TAC Cuxvzoz.tau3_taum_nonplanar;
2587 REWRITE_TAC[DIST_SYM];
2588 REWRITE_TAC[CONJ_ASSOC] THEN CONJ2_TAC;
2589 ASM_REWRITE_TAC[DIST_SYM];
2590 BY(MESON_TAC[Terminal.taum_sym]);
2592 FIRST_X_ASSUM_ST `a < pi` MP_TAC;