Update from HH
[Flyspeck/.git] / text_formalization / local / TECOXBM.hl
1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
3 (*                                                                            *)
4 (* Chapter: Fan                                              *)
5 (* Author: Hoang Le Truong                                        *)
6 (* Date: 2010-02-09                                                           *)
7 (* ========================================================================= *)
8
9
10
11
12 module   Tecoxbm = struct
13
14
15
16 open Wjscpro;;
17 open Polyhedron;;
18 open Sphere;;
19 open Fan_defs;;
20 open Hypermap;;
21 open Vol1;;
22 open Fan;;
23 open Topology;;         
24 open Fan_misc;;
25 open Planarity;; 
26 open Conforming;;
27 open Sphere;;
28 open Hypermap;;
29 open Fan;;
30 open Topology;;
31 open Prove_by_refinement;;
32 open Pack_defs;;
33 open Wrgcvdr_cizmrrh;;
34 open Local_lemmas;;
35 open Collect_geom;;
36 open Dih2k_hypermap;;
37
38
39 let CROSS_DOT_POS_SY=prove_by_refinement(`!l:real^(M,3)finite_product. stable_system k d (0..k-1) a b J (\i. ((1+i):num MOD k)) /\ k= dimindex(:M)/\ 2<k/\
40 u IN V_SY(vecmats(l))
41 /\ 1<= i /\ i<= dimindex (:M)
42 /\ row i (vecmats l)=y
43 /\  row (SUC (i MOD dimindex (:M))) (vecmats l)=z
44 /\l IN B_SY1 a b
45 ==> &0<= (y cross z) dot u `,
46 [REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY]
47 THEN REPEAT STRIP_TAC
48 THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
49 THEN POP_ASSUM MP_TAC 
50 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
51 THEN POP_ASSUM MP_TAC
52 THEN POP_ASSUM MP_TAC
53 THEN POP_ASSUM MP_TAC
54 THEN DISCH_THEN(LABEL_TAC"THY")
55 THEN STRIP_TAC
56 THEN STRIP_TAC
57 THEN POP_ASSUM(fun th-> MP_TAC th
58 THEN REWRITE_TAC[convex_local_fan]
59 THEN STRIP_TAC
60 THEN POP_ASSUM MP_TAC
61 THEN POP_ASSUM(fun th1-> MP_TAC th1
62 THEN REWRITE_TAC[local_fan]
63 THEN LET_TAC
64 THEN STRIP_TAC
65 THEN POP_ASSUM MP_TAC
66 THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
67 THEN STRIP_TAC
68 THEN ASSUME_TAC th1)
69 THEN DISCH_THEN(LABEL_TAC"THY1")
70 THEN ASSUME_TAC th)
71 THEN STRIP_TAC
72 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
73 THEN SUBGOAL_THEN `(y,z)IN F_SY(vecmats(l:real^(M,3)finite_product))`ASSUME_TAC;
74 REWRITE_TAC[F_SY;rows;IN_ELIM_THM]
75 THEN EXISTS_TAC`i:num`
76 THEN ASM_REWRITE_TAC[];
77 MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`y:real^3`;`z:real^3`;`(l:real^(M,3)finite_product)`]
78 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`z:real^3`;`y:real^3`]
79 THEN MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`y:real^3`;`z:real^3`]
80 THEN REMOVE_THEN"THY1"(fun th-> MRESA1_TAC th`(y,z):real^3#real^3`)
81 THEN POP_ASSUM MP_TAC
82 THEN POP_ASSUM MP_TAC
83 THEN MRESA_TAC (GEN_ALL Local_lemmas.DETERMINE_WEDGE_IN_FAN)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`((y,z):real^3#real^3)`]
84 THEN MRESA_TAC (GEN_ALL Local_lemmas.PGSQVBL)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`;`w:real^3`;`(y,z):real^3#real^3`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
85 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`((y,z):real^3#real^3)`]
86 THEN REWRITE_TAC[REAL_ARITH`A<=B<=> A=B\/ A<B`]
87 THEN RESA_TAC;
88 MRESAL_TAC (GEN_ALL Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT)[`(azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z)`;`y:real^3`;`z:real^3`;`vec 0:real^3`][VECTOR_ARITH`A -vec 0= A`]
89 THEN STRIP_TAC
90 THEN MP_TAC(SET_RULE`u IN V_SY (vecmats (l:real^(M,3)finite_product))
91 /\ V_SY (vecmats l) SUBSET {x | &0 <= (y cross z) dot x}
92 ==> &0<= (y cross z) dot u`)
93 THEN RESA_TAC
94 THEN POP_ASSUM MP_TAC
95 THEN POP_ASSUM MP_TAC
96 THEN REAL_ARITH_TAC;
97 POP_ASSUM MP_TAC
98 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y:real^3`;`z:real^3`]
99 THEN MRESA_TAC(sigma_fan_in_set_of_edge)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;]
100 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats (l:real^(M,3)finite_product))) (E_SY (vecmats (l:real^(M,3)finite_product))) (row i (vecmats (l:real^(M,3)finite_product)))
101       (row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`]
102 THEN POP_ASSUM MP_TAC
103 THEN RESA_TAC
104 THEN STRIP_TAC
105 THEN MRESA_TAC(GEN_ALL Local_lemmas.WEDGE_GE_EQ_AFF_GE)[`vec 0:real^3`;`y:real^3`;`z:real^3`;`(azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z)`]
106 THEN MP_TAC(REAL_ARITH`&0<= azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
107       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
108       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))
109 ==> azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
110       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
111       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) = &0 \/
112 &0< azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
113       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
114       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))`)
115 THEN ASM_REWRITE_TAC[azim]
116 THEN STRIP_TAC;
117 MRESA_TAC Fan.UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
118       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
119 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.FAN_IMP_EE_EQ_SET_OF_EDGE)[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]
120 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1)[`F_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]
121 THEN POP_ASSUM MP_TAC
122 THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={row (SUC (i MOD dimindex (:M))) (vecmats l)}
123 \/ ~(set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))})`);
124 POP_ASSUM MP_TAC
125 THEN RESA_TAC
126 THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
127                  IN_INSERT; NOT_IN_EMPTY]
128 THEN ARITH_TAC;
129 MRESA_TAC SIGMA_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`]
130 THEN REMOVE_ASSUM_TAC
131 THEN POP_ASSUM MP_TAC
132 THEN ONCE_REWRITE_TAC[SET_RULE`A=B<=>B=A`]
133 THEN REMOVE_ASSUM_TAC
134 THEN REMOVE_ASSUM_TAC
135 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]);
136 MP_TAC(REAL_ARITH`
137 &0<azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
138       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
139       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) /\
140       azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
141       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
142       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) <
143       pi
144 ==> ~(azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
145       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
146       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
147       &0 \/
148       azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
149       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
150       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
151       pi)`)
152 THEN RESA_TAC
153 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
154       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
155 THEN POP_ASSUM MP_TAC
156 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
157 THEN STRIP_TAC
158 THEN MRESA_TAC( GEN_ALL Nkezbfc_local.inter_aff_ge_3_1_is_aff_ge_2_2)[`vec 0:real^3`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
159       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
160 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
161 THEN MRESAL_TAC Planarity.cross_dot_fully_surrounded_fan[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
162       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`][VECTOR_ARITH`A- vec 0=A`]
163 THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot [`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
164       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`]
165 THEN POP_ASSUM MP_TAC
166 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
167 THEN RESA_TAC
168 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
169 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
170 THEN STRIP_TAC
171 THEN MP_TAC(SET_RULE`u IN V_SY (vecmats (l:real^(M,3)finite_product))
172 /\ V_SY (vecmats l) SUBSET {y' | &0 <= (y cross z) dot y'} INTER
173  aff_ge
174  {vec 0, sigma_fan (vec 0) (V_SY (vecmats l)) (E_SY (vecmats l)) y z, y}
175  {z}
176 ==> &0<= (y cross z) dot u`)
177 THEN RESA_TAC
178 THEN POP_ASSUM MP_TAC
179 THEN POP_ASSUM MP_TAC
180 THEN REAL_ARITH_TAC]);;
181
182
183 let IVS_RHO_NODE_IN_EDGE = prove(`!v. local_fan (V,E,FF) /\ v IN V ==> {v,ivs_rho_node1 FF v} IN E`,
184 NHANH EXISTS_INVERSE_OF_V THEN REPEAT STRIP_TAC 
185 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
186 THEN MRESA_TAC(GEN_ALL Local_lemmas.IVS_RHO_IDD)[`E:(real^3->bool)->bool`;`V:real^3->bool`;
187 `FF:real^3#real^3->bool`;`vv:real^3`]
188 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_IMP_EE_TWO_ELMS)[`V:real^3->bool`;`E:(real^3->bool)->bool`;
189 `FF:real^3#real^3->bool`;`rho_node1 (FF:real^3#real^3->bool) vv`;`vv:real^3`]
190 THEN MP_TAC(SET_RULE`EE (rho_node1 FF vv) E = {rho_node1 FF (rho_node1 FF vv), vv} ==> vv IN EE (rho_node1 FF vv) (E:(real^3->bool)->bool) `)
191 THEN RESA_TAC
192 THEN POP_ASSUM MP_TAC
193 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
194 THEN REWRITE_TAC[EE;IN_ELIM_THM]);;
195
196
197 let RHO_IVS_IDD = prove(` local_fan (V,E,FF) /\ v IN V
198 ==> rho_node1 FF ( ivs_rho_node1 FF v ) = v `,
199 NHANH EXISTS_INVERSE_OF_V 
200 THEN REPEAT STRIP_TAC
201 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th])
202 THEN MRESA_TAC (GEN_ALL Local_lemmas.IVS_RHO_IDD)[`E:(real^3->bool)->bool`;`V:real^3->bool`;
203 `FF:real^3#real^3->bool`;`vv:real^3`]);;
204
205
206
207 let PROPERTIES_OF_FAN_IN_B_SY=prove_by_refinement(`!l:real^(M,3)finite_product. stable_system k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\ dimindex(:M)= k/\ 2<k
208 /\ 1<= i /\ i<= dimindex (:M)
209 /\ 1<= j /\ j<= dimindex (:M)
210 /\ ~(i=j)
211 /\ row i (vecmats l)=y
212 /\  row j (vecmats l)=z
213 /\l IN B_SY1 a b
214 ==> &2<= norm (y-z)  `,
215 [REPEAT STRIP_TAC
216 THEN ASM_TAC
217 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
218 THEN REPEAT STRIP_TAC
219 THEN POP_ASSUM( fun th-> ASSUME_TAC th THEN MP_TAC th THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY;CONDITION1_SY] THEN STRIP_TAC)
220 THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
221 THEN POP_ASSUM MP_TAC 
222 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
223 THEN POP_ASSUM MP_TAC
224 THEN POP_ASSUM MP_TAC
225 THEN POP_ASSUM MP_TAC
226 THEN DISCH_THEN(LABEL_TAC"THY")
227 THEN DISCH_THEN(LABEL_TAC"THY2")
228 THEN STRIP_TAC
229 THEN POP_ASSUM(fun th-> MP_TAC th
230 THEN REWRITE_TAC[convex_local_fan]
231 THEN STRIP_TAC
232 THEN POP_ASSUM MP_TAC
233 THEN POP_ASSUM(fun th1-> MP_TAC th1
234 THEN REWRITE_TAC[local_fan]
235 THEN LET_TAC
236 THEN STRIP_TAC
237 THEN POP_ASSUM MP_TAC
238 THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
239 THEN STRIP_TAC
240 THEN ASSUME_TAC th1)
241 THEN DISCH_THEN(LABEL_TAC"THY1")
242 THEN ASSUME_TAC th)
243 THEN STRIP_TAC
244 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
245 THEN REMOVE_THEN"THY2"(fun th-> MRESA_TAC th[`i:num`;`j:num`])
246 THEN REMOVE_ASSUM_TAC
247 THEN POP_ASSUM MP_TAC
248 THEN REMOVE_THEN "THYGIANG" MP_TAC
249 THEN REWRITE_TAC[stable_system]
250 THEN STRIP_TAC
251 THEN REMOVE_ASSUM_TAC
252 THEN REMOVE_ASSUM_TAC
253 THEN POP_ASSUM MP_TAC
254 THEN POP_ASSUM MP_TAC
255 THEN DISCH_THEN(LABEL_TAC"THYGIANG2")
256 THEN MP_TAC(ARITH_RULE`i<= dimindex (:M)==> i <= dimindex (:M)-1 \/ i = dimindex (:M)`)
257 THEN RESA_TAC;
258
259 MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`)
260 THEN RESA_TAC;
261
262 STRIP_TAC
263 THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`i:num`;`j:num`][ARITH_RULE`0<= i:num`;IN_NUMSEG])
264 THEN POP_ASSUM MP_TAC
265 THEN REAL_ARITH_TAC;
266
267 MP_TAC(ARITH_RULE`1<= i /\ 2< k==> ~(i = 0) /\ ~(k=0)/\ 1<k /\ 1<=k`)
268 THEN RESA_TAC
269 THEN STRIP_TAC
270 THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`i:num`;`0:num`][ARITH_RULE`0<= i:num`;IN_NUMSEG])
271 THEN POP_ASSUM MP_TAC
272 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]
273 THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]
274 THEN REMOVE_THEN "THYGIANG2" MP_TAC
275 THEN REWRITE_TAC[constraint_system]
276 THEN STRIP_TAC
277 THEN REMOVE_ASSUM_TAC
278 THEN REMOVE_ASSUM_TAC
279 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A /\ k+k=k *2`])
280 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`]
281 THEN REAL_ARITH_TAC;
282
283 MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`)
284 THEN RESA_TAC;
285
286 MP_TAC(ARITH_RULE`2< k==> ~(k = 0)/\ 1<=k /\ 1<k`)
287 THEN RESA_TAC
288 THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`]
289 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`]
290 THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]
291 THEN REMOVE_THEN "THYGIANG2" MP_TAC
292 THEN REWRITE_TAC[constraint_system]
293 THEN STRIP_TAC
294 THEN REMOVE_ASSUM_TAC
295 THEN REMOVE_ASSUM_TAC
296 THEN POP_ASSUM MP_TAC
297 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `])
298 THEN STRIP_TAC
299 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A /\ k+k= k*2`])
300 THEN MP_TAC(ARITH_RULE`1<= j==> ~(j = 0)`)
301 THEN RESA_TAC
302 THEN STRIP_TAC
303 THEN POP_ASSUM  (fun th-> MRESAL_TAC th[`j:num`;`0:num`][ARITH_RULE`0<= i:num`;IN_NUMSEG])
304 THEN POP_ASSUM MP_TAC
305 THEN REAL_ARITH_TAC;
306
307 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th])
308 THEN SET_TAC[]]);;
309
310
311 let AFF_GT_INTER_AFF_SY=prove_by_refinement(`!l:real^(M,3)finite_product. stable_system k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\ dimindex(:M)= k/\ 2<k/\
312 {u,w} SUBSET V_SY(vecmats(l))
313 /\ norm(u-w)<= cstab
314 /\ &2<= norm(u-w)
315 /\ ~({u,w} IN E_SY(vecmats l))
316 /\ 1<= i /\ i<= dimindex (:M)
317 /\ row i (vecmats l)=y
318 /\  row (SUC (i MOD dimindex (:M))) (vecmats l)=z
319 /\l IN B_SY1 a b
320 ==> aff_gt {vec 0}{u,w} INTER aff {vec 0,y,z}={} `,
321 [REPEAT STRIP_TAC
322 THEN POP_ASSUM( fun th-> ASSUME_TAC th THEN MP_TAC th THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY] THEN STRIP_TAC)
323 THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
324 THEN POP_ASSUM MP_TAC 
325 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
326 THEN POP_ASSUM MP_TAC
327 THEN POP_ASSUM MP_TAC
328 THEN POP_ASSUM MP_TAC
329 THEN DISCH_THEN(LABEL_TAC"THY")
330 THEN STRIP_TAC
331 THEN STRIP_TAC
332 THEN POP_ASSUM(fun th-> MP_TAC th
333 THEN REWRITE_TAC[convex_local_fan]
334 THEN STRIP_TAC
335 THEN POP_ASSUM MP_TAC
336 THEN POP_ASSUM(fun th1-> MP_TAC th1
337 THEN REWRITE_TAC[local_fan]
338 THEN LET_TAC
339 THEN STRIP_TAC
340 THEN POP_ASSUM MP_TAC
341 THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
342 THEN STRIP_TAC
343 THEN ASSUME_TAC th1)
344 THEN DISCH_THEN(LABEL_TAC"THY1")
345 THEN ASSUME_TAC th)
346 THEN STRIP_TAC
347 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
348 THEN SUBGOAL_THEN `(y,z)IN F_SY(vecmats(l:real^(M,3)finite_product))`ASSUME_TAC;
349 REWRITE_TAC[F_SY;rows;IN_ELIM_THM]
350 THEN EXISTS_TAC`i:num`
351 THEN ASM_REWRITE_TAC[];
352 MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`y:real^3`;`z:real^3`;`(l:real^(M,3)finite_product)`]
353 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`z:real^3`;`y:real^3`]
354 THEN MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`y:real^3`;`z:real^3`]
355 THEN SUBGOAL_THEN `u IN ball_annulus` ASSUME_TAC;
356 MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats l) ==> u IN V_SY (vecmats (l:real^(M,3)finite_product))`)
357 THEN ASM_REWRITE_TAC[V_SY;IN_ELIM_THM;rows]
358 THEN STRIP_TAC
359 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i':num`);
360 SUBGOAL_THEN `w IN ball_annulus` ASSUME_TAC;
361 MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats l) ==> w IN V_SY (vecmats (l:real^(M,3)finite_product))`)
362 THEN ASM_REWRITE_TAC[V_SY;IN_ELIM_THM;rows]
363 THEN STRIP_TAC
364 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i':num`);
365 MRESAL_TAC (GEN_ALL NONPARALLEL_BALL_ANNULUS)[`u:real^3`;`w:real^3`][SET_RULE`{A} UNION {B,C}={A,B,C}`]
366 THEN MRESA_TAC th3[`vec 0:real^3`;`u:real^3`;`w:real^3`]
367 THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`u:real^3`;`w:real^3`]
368 THEN REWRITE_TAC[SET_RULE`A= {}<=> ~(?x1.  x1 IN A)`;INTER;IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
369 THEN STRIP_TAC
370 THEN POP_ASSUM MP_TAC
371 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A % vec 0+C=C`;DOT_RADD;DOT_RMUL];
372 SUBGOAL_THEN`&0<=(y cross z) dot u/\ &0<=(y cross z) dot w` ASSUME_TAC;
373 REMOVE_THEN"THY1"(fun th-> MRESA1_TAC th`(y,z):real^3#real^3`)
374 THEN POP_ASSUM MP_TAC
375 THEN POP_ASSUM MP_TAC
376 THEN MRESA_TAC (GEN_ALL Local_lemmas.DETERMINE_WEDGE_IN_FAN)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`((y,z):real^3#real^3)`]
377 THEN MRESA_TAC (GEN_ALL Local_lemmas.PGSQVBL)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`;`w:real^3`;`(y,z):real^3#real^3`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
378 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`((y,z):real^3#real^3)`]
379 THEN REWRITE_TAC[REAL_ARITH`A<=B<=> A=B\/ A<B`]
380 THEN RESA_TAC;
381 MRESAL_TAC (GEN_ALL Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT)[`(azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z)`;`y:real^3`;`z:real^3`;`vec 0:real^3`][VECTOR_ARITH`A -vec 0= A`]
382 THEN STRIP_TAC
383 THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
384 /\ V_SY (vecmats l) SUBSET {x | &0 <= (y cross z) dot x}
385 ==> &0<= (y cross z) dot u /\ &0<= (y cross z) dot w`)
386 THEN RESA_TAC
387 THEN POP_ASSUM MP_TAC
388 THEN POP_ASSUM MP_TAC
389 THEN REAL_ARITH_TAC;
390 POP_ASSUM MP_TAC
391 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y:real^3`;`z:real^3`]
392 THEN MRESA_TAC(sigma_fan_in_set_of_edge)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;]
393 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats (l:real^(M,3)finite_product))) (E_SY (vecmats (l:real^(M,3)finite_product))) (row i (vecmats (l:real^(M,3)finite_product)))
394       (row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`]
395 THEN POP_ASSUM MP_TAC
396 THEN RESA_TAC
397 THEN STRIP_TAC
398 THEN MRESA_TAC(GEN_ALL Local_lemmas.WEDGE_GE_EQ_AFF_GE)[`vec 0:real^3`;`y:real^3`;`z:real^3`;`(azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z)`]
399 THEN MP_TAC(REAL_ARITH`&0<= azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
400       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
401       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))
402 ==> azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
403       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
404       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) = &0 \/
405 &0< azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
406       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
407       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))`)
408 THEN ASM_REWRITE_TAC[azim]
409 THEN STRIP_TAC;
410 MRESA_TAC Fan.UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
411       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
412 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.FAN_IMP_EE_EQ_SET_OF_EDGE)[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]
413 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1)[`F_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]
414 THEN POP_ASSUM MP_TAC
415 THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={row (SUC (i MOD dimindex (:M))) (vecmats l)}
416 \/ ~(set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))})`);
417 POP_ASSUM MP_TAC
418 THEN RESA_TAC
419 THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
420                  IN_INSERT; NOT_IN_EMPTY]
421 THEN ARITH_TAC;
422 MRESA_TAC SIGMA_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`]
423 THEN REMOVE_ASSUM_TAC
424 THEN POP_ASSUM MP_TAC
425 THEN ONCE_REWRITE_TAC[SET_RULE`A=B<=>B=A`]
426 THEN REMOVE_ASSUM_TAC
427 THEN REMOVE_ASSUM_TAC
428 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]);
429 MP_TAC(REAL_ARITH`
430 &0<azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
431       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
432       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) /\
433       azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
434       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
435       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) <
436       pi
437 ==> ~(azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
438       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
439       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
440       &0 \/
441       azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
442       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
443       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
444       pi)`)
445 THEN RESA_TAC
446 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
447       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
448 THEN POP_ASSUM MP_TAC
449 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
450 THEN STRIP_TAC
451 THEN MRESA_TAC( GEN_ALL Nkezbfc_local.inter_aff_ge_3_1_is_aff_ge_2_2)[`vec 0:real^3`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
452       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
453 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
454 THEN MRESAL_TAC Planarity.cross_dot_fully_surrounded_fan[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
455       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`][VECTOR_ARITH`A- vec 0=A`]
456 THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot [`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
457       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`]
458 THEN POP_ASSUM MP_TAC
459 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
460 THEN RESA_TAC
461 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
462 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
463 THEN STRIP_TAC
464 THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
465 /\ V_SY (vecmats l) SUBSET {y' | &0 <= (y cross z) dot y'} INTER
466  aff_ge
467  {vec 0, sigma_fan (vec 0) (V_SY (vecmats l)) (E_SY (vecmats l)) y z, y}
468  {z}
469 ==> &0<= (y cross z) dot u /\ &0<= (y cross z) dot w`)
470 THEN RESA_TAC
471 THEN POP_ASSUM MP_TAC
472 THEN POP_ASSUM MP_TAC
473 THEN REAL_ARITH_TAC;
474 POP_ASSUM MP_TAC
475 THEN STRIP_TAC
476 THEN POP_ASSUM MP_TAC
477 THEN POP_ASSUM MP_TAC
478 THEN REWRITE_TAC[REAL_ARITH`&0<=A <=> &0< A \/ A= &0`]
479 THEN RESA_TAC;
480 REWRITE_TAC[REAL_ARITH`&0< A \/ A= &0<=> &0<=A `]
481 THEN STRIP_TAC;
482 MP_TAC(REAL_ARITH`&0< t3==> &0<= t3`)
483 THEN RESA_TAC
484 THEN MRESA_TAC REAL_LT_MUL[`t2:real`;`(y cross z) dot u`]
485 THEN MRESA_TAC REAL_LE_MUL[`t3:real`;`(y cross z) dot w`]
486 THEN POP_ASSUM MP_TAC
487 THEN POP_ASSUM MP_TAC
488 THEN REAL_ARITH_TAC;
489 STRIP_TAC;
490 MRESA_TAC REAL_LT_MUL[`t3:real`;`(y cross z) dot w`]
491 THEN POP_ASSUM MP_TAC
492 THEN REAL_ARITH_TAC;
493 STRIP_TAC
494 THEN REMOVE_ASSUM_TAC
495 THEN ABBREV_TAC`y1= rho_node1 (F_SY(vecmats (l:real^(M,3)finite_product))) u`
496 THEN ABBREV_TAC`z1= ivs_rho_node1 (F_SY(vecmats (l:real^(M,3)finite_product))) u`
497 THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
498 ==> u IN V_SY (vecmats (l:real^(M,3)finite_product))`)
499 THEN RESA_TAC
500 THEN SUBGOAL_THEN`y1 IN V_SY(vecmats(l:real^(M,3)finite_product))`ASSUME_TAC;
501 MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;]
502 THEN POP_ASSUM (fun th-> MRESAL1_TAC th `SUC 0`[ITER;I_DEF;o_DEF]);
503 SUBGOAL_THEN`z1 IN V_SY(vecmats(l:real^(M,3)finite_product))`ASSUME_TAC;
504 MRESA_TAC (GEN_ALL Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;]
505 THEN POP_ASSUM(fun th-> MRESA1_TAC th`u:real^3`)
506 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;]
507 THEN POP_ASSUM (fun th-> MRESAL1_TAC th `CARD (V_SY (vecmats (l:real^(M,3)finite_product))) - 1`[]);
508 SUBGOAL_THEN`&0<= (y cross z) dot y1/\ &0<= (y cross z) dot z1`ASSUME_TAC;
509 REMOVE_THEN"THY1"(fun th-> MRESA1_TAC th`(y,z):real^3#real^3`)
510 THEN POP_ASSUM MP_TAC
511 THEN POP_ASSUM MP_TAC
512 THEN MRESA_TAC (GEN_ALL Local_lemmas.DETERMINE_WEDGE_IN_FAN)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`((y,z):real^3#real^3)`]
513 THEN MRESA_TAC (GEN_ALL Local_lemmas.PGSQVBL)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`;`w:real^3`;`(y,z):real^3#real^3`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
514 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`((y,z):real^3#real^3)`]
515 THEN REWRITE_TAC[REAL_ARITH`A<=B<=> A=B\/ A<B`]
516 THEN RESA_TAC;
517 MRESAL_TAC (GEN_ALL Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT)[`(azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z)`;`y:real^3`;`z:real^3`;`vec 0:real^3`][VECTOR_ARITH`A -vec 0= A`]
518 THEN STRIP_TAC
519 THEN MP_TAC(SET_RULE`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))
520 /\ z1 IN V_SY (vecmats (l:real^(M,3)finite_product))
521 /\ V_SY (vecmats l) SUBSET {x | &0 <= (y cross z) dot x}
522 ==> &0<= (y cross z) dot y1 /\ &0<= (y cross z) dot z1`)
523 THEN RESA_TAC
524 THEN POP_ASSUM MP_TAC
525 THEN POP_ASSUM MP_TAC
526 THEN REAL_ARITH_TAC;
527 POP_ASSUM MP_TAC
528 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y:real^3`;`z:real^3`]
529 THEN MRESA_TAC(sigma_fan_in_set_of_edge)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;]
530 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats (l:real^(M,3)finite_product))) (E_SY (vecmats (l:real^(M,3)finite_product))) (row i (vecmats (l:real^(M,3)finite_product)))
531       (row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`]
532 THEN POP_ASSUM MP_TAC
533 THEN RESA_TAC
534 THEN STRIP_TAC
535 THEN MRESA_TAC(GEN_ALL Local_lemmas.WEDGE_GE_EQ_AFF_GE)[`vec 0:real^3`;`y:real^3`;`z:real^3`;`(azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z)`]
536 THEN MP_TAC(REAL_ARITH`&0<= azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
537       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
538       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))
539 ==> azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
540       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
541       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) = &0 \/
542 &0< azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
543       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
544       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))`)
545 THEN ASM_REWRITE_TAC[azim]
546 THEN STRIP_TAC;
547 MRESA_TAC Fan.UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
548       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
549 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.FAN_IMP_EE_EQ_SET_OF_EDGE)[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]
550 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1)[`F_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]
551 THEN POP_ASSUM MP_TAC
552 THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={row (SUC (i MOD dimindex (:M))) (vecmats l)}
553 \/ ~(set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))})`);
554 POP_ASSUM MP_TAC
555 THEN RESA_TAC
556 THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
557                  IN_INSERT; NOT_IN_EMPTY]
558 THEN ARITH_TAC;
559 MRESA_TAC SIGMA_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`]
560 THEN REMOVE_ASSUM_TAC
561 THEN POP_ASSUM MP_TAC
562 THEN ONCE_REWRITE_TAC[SET_RULE`A=B<=>B=A`]
563 THEN REMOVE_ASSUM_TAC
564 THEN REMOVE_ASSUM_TAC
565 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]);
566 MP_TAC(REAL_ARITH`
567 &0<azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
568       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
569       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) /\
570       azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
571       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
572       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) <
573       pi
574 ==> ~(azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
575       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
576       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
577       &0 \/
578       azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
579       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
580       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
581       pi)`)
582 THEN RESA_TAC
583 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
584       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
585 THEN POP_ASSUM MP_TAC
586 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
587 THEN STRIP_TAC
588 THEN MRESA_TAC( GEN_ALL Nkezbfc_local.inter_aff_ge_3_1_is_aff_ge_2_2)[`vec 0:real^3`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
589       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
590 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
591 THEN MRESAL_TAC Planarity.cross_dot_fully_surrounded_fan[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
592       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`][VECTOR_ARITH`A- vec 0=A`]
593 THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot [`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
594       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`]
595 THEN POP_ASSUM MP_TAC
596 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
597 THEN RESA_TAC
598 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
599 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
600 THEN STRIP_TAC
601 THEN MP_TAC(SET_RULE`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))
602 /\ z1 IN V_SY (vecmats (l:real^(M,3)finite_product))
603 /\ V_SY (vecmats l) SUBSET {y' | &0 <= (y cross z) dot y'} INTER
604  aff_ge
605  {vec 0, sigma_fan (vec 0) (V_SY (vecmats l)) (E_SY (vecmats l)) y z, y}
606  {z}
607 ==> &0<= (y cross z) dot y1 /\ &0<= (y cross z) dot z1 `)
608 THEN RESA_TAC
609 THEN POP_ASSUM MP_TAC
610 THEN POP_ASSUM MP_TAC
611 THEN REAL_ARITH_TAC;
612 POP_ASSUM MP_TAC
613 THEN POP_ASSUM MP_TAC
614 THEN POP_ASSUM MP_TAC
615 THEN POP_ASSUM MP_TAC
616 THEN DISCH_THEN(LABEL_TAC"CHANGE")
617 THEN STRIP_TAC
618 THEN STRIP_TAC
619 THEN DISCH_THEN(LABEL_TAC"THY4")
620 THEN REMOVE_THEN"CHANGE" (fun th-> ASSUME_TAC th THEN
621 MP_TAC th THEN REWRITE_TAC[V_SY;IN_ELIM_THM;rows]
622 THEN STRIP_TAC)
623 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
624 THEN SUBGOAL_THEN`u,row (SUC (i' MOD k)) (vecmats l) IN F_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
625 REWRITE_TAC[F_SY;rows;IN_ELIM_THM]
626 THEN EXISTS_TAC`i':num`
627 THEN ASM_REWRITE_TAC[];
628 MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;]
629 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`u:real^3,row (SUC (i' MOD k)) (vecmats (l:real^(M,3)finite_product))`[PAIR_EQ])
630 THEN MRESA_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`y1:real^3`;`y:real^3`;`l:real^(M,3)finite_product`]
631 THEN POP_ASSUM MP_TAC
632 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y:real^3`;`z:real^3`]
633 THEN POP_ASSUM MP_TAC
634 THEN POP_ASSUM MP_TAC
635 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
636 THEN RESA_TAC
637 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`]
638 THEN RESA_TAC
639 THEN MRESA_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`y1:real^3`;`z:real^3`;`l:real^(M,3)finite_product`]
640 THEN POP_ASSUM MP_TAC
641 THEN MRESA_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`y1:real^3`;`z1:real^3`;`l:real^(M,3)finite_product`]
642 THEN SUBGOAL_THEN(` &0 <= (z1 cross u) dot w /\ &0 <= (z1 cross u) dot y /\ &0 <= (z1 cross u) dot z  `)ASSUME_TAC;
643 MP_TAC(ARITH_RULE`1<=i'==> i'=1 \/ 1<= i'-1`)
644 THEN RESA_TAC;
645 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
646 THEN MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
647 THEN MP_TAC(ARITH_RULE`2<k==> 1<= k/\ k<=k`)
648 THEN RESA_TAC
649 THEN SUBGOAL_THEN`row k (vecmats l), u IN F_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
650 REWRITE_TAC[F_SY;rows;IN_ELIM_THM]
651 THEN EXISTS_TAC`k:num`
652 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC 0=1`];
653 MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;]
654 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`row k (vecmats (l:real^(M,3)finite_product)):real^3,u:real^3`[PAIR_EQ])
655 THEN FIND_ASSUM MP_TAC`ivs_rho_node1 (F_SY (vecmats (l:real^(M,3)finite_product))) u=z1`
656 THEN POP_ASSUM(fun th-> REWRITE_TAC[th] THEN ASSUME_TAC th)
657 THEN SUBGOAL_THEN`row k (vecmats l) IN V_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
658 REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
659 THEN EXISTS_TAC`k:num`
660 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC 0=1`];
661 MRESA_TAC(GEN_ALL Local_lemmas.IVS_RHO_IDD) [`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`(row k (vecmats (l:real^(M,3)finite_product)))`]
662 THEN STRIP_TAC
663 THEN MRESAL_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`k:num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`y:real^3`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]
664 THEN MRESAL_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`k:num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`z:real^3`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]
665 THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
666 ==> w IN V_SY (vecmats l) `)
667 THEN RESA_TAC
668 THEN MRESAL_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`k:num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`w:real^3`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`];
669 MP_TAC(ARITH_RULE`1<= i' /\ i'<= dimindex (:M) ==> i'-1 < dimindex (:M)/\ i'-1 <= dimindex (:M)`)
670 THEN RESA_TAC 
671 THEN MRESAL_TAC MOD_LT[`i'-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]
672 THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
673 ==> w IN V_SY (vecmats l) `)
674 THEN RESA_TAC
675 THEN MRESAL_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'-1:num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`y:real^3`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]
676 THEN MRESAL_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'-1:num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`z:real^3`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]
677 THEN MRESAL_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'-1:num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`w:real^3`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]
678 THEN POP_ASSUM MP_TAC
679 THEN POP_ASSUM MP_TAC
680 THEN POP_ASSUM MP_TAC
681 THEN MP_TAC(ARITH_RULE`1<= i' /\ i'<= dimindex (:M) ==>  SUC (i'-1)=i'`)
682 THEN RESA_TAC 
683 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
684 THEN SUBGOAL_THEN`row (i'-1) (vecmats l), u IN F_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
685 REWRITE_TAC[F_SY;rows;IN_ELIM_THM]
686 THEN EXISTS_TAC`i'-1:num`
687 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC 0=1`]
688 THEN MP_TAC(ARITH_RULE`1<= i' /\ i'<= dimindex (:M) ==>  SUC (i'-1)=i'`)
689 THEN RESA_TAC 
690 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]);
691 MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_RHO_NODE_PROS)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;]
692 THEN POP_ASSUM (fun th-> MRESAL1_TAC th`row (i'-1) (vecmats (l:real^(M,3)finite_product)):real^3,u:real^3`[PAIR_EQ])
693 THEN FIND_ASSUM MP_TAC`ivs_rho_node1 (F_SY (vecmats (l:real^(M,3)finite_product))) u=z1`
694 THEN POP_ASSUM(fun th-> REWRITE_TAC[th] THEN ASSUME_TAC th)
695 THEN SUBGOAL_THEN`row (i'-1) (vecmats l) IN V_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
696 REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
697 THEN EXISTS_TAC`i'-1:num`
698 THEN ASM_REWRITE_TAC[ARITH_RULE`SUC 0=1`];
699 MRESA_TAC(GEN_ALL Local_lemmas.IVS_RHO_IDD) [`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`(row (i'-1) (vecmats (l:real^(M,3)finite_product)))`]
700 THEN RESA_TAC
701 THEN REAL_ARITH_TAC;
702 POP_ASSUM MP_TAC
703 THEN STRIP_TAC
704 THEN POP_ASSUM MP_TAC
705 THEN POP_ASSUM MP_TAC
706 THEN SUBGOAL_THEN`u IN aff{vec 0, y,z:real^3}` ASSUME_TAC;
707 ASM_REWRITE_TAC[VECTOR_ARITH`A- vec 0=A`;IN_ELIM_THM];
708 POP_ASSUM MP_TAC
709 THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
710 THEN STRIP_TAC 
711 THEN POP_ASSUM (fun th-> REWRITE_TAC[th] THEN ASSUME_TAC (SYM th))
712 THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;DOT_LADD;DOT_LMUL;DOT_CROSS_SELF;REAL_ARITH`A* &0= &0/\ A+ &0=A /\ &0+ A=A`;CROSS_RADD;CROSS_RMUL;]
713 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
714 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
715 THEN MP_TAC(REAL_ARITH`&0 <= (y cross z) dot y1 ==> ~((y cross z) dot y1< &0)`)
716 THEN RESA_TAC
717 THEN SUBGOAL_THEN`(y cross z1) dot z<= &0` ASSUME_TAC;
718 ONCE_REWRITE_TAC[CROSS_TRIPLE]
719 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
720 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
721 THEN ASM_REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- A<= &0<=> &0<= A`];
722 MP_TAC(REAL_ARITH` (y cross z1) dot z<= &0 ==> ~(&0< (y cross z1) dot z)`)
723 THEN RESA_TAC
724 THEN REPEAT STRIP_TAC
725 THEN SUBGOAL_THEN`(y cross z1) dot z= &0 \/ (y cross z) dot y1= &0` ASSUME_TAC;
726 POP_ASSUM MP_TAC
727 THEN POP_ASSUM MP_TAC
728 THEN POP_ASSUM MP_TAC
729 THEN POP_ASSUM MP_TAC
730 THEN ASM_REWRITE_TAC[REAL_MUL_POS_LE]
731 THEN SUBGOAL_THEN`~(w' = &0 /\ v'= &0)` ASSUME_TAC;
732 STRIP_TAC
733 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
734 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
735 THEN ASM_TAC
736 THEN REWRITE_TAC[VECTOR_ARITH`&0 % A= vec 0/\ vec 0+ vec 0= vec 0`]
737 THEN REPEAT STRIP_TAC
738 THEN REMOVE_ASSUM_TAC
739 THEN REMOVE_ASSUM_TAC
740 THEN POP_ASSUM MP_TAC
741 THEN ASM_REWRITE_TAC[];
742 POP_ASSUM MP_TAC
743 THEN ASM_REWRITE_TAC[SET_RULE`~(A /\ B)<=> ~A \/ ~B`]
744 THEN RESA_TAC;
745 RESA_TAC;
746 MP_TAC(REAL_ARITH`w'< &0==> ~(&0 < w')`)
747 THEN RESA_TAC
748 THEN SET_TAC[];
749 DISCH_TAC
750 THEN REMOVE_ASSUM_TAC
751 THEN RESA_TAC;
752 POP_ASSUM MP_TAC
753 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
754 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
755 THEN STRIP_TAC
756 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
757 THEN ASM_REWRITE_TAC[DOT_LNEG;]
758 THEN REAL_ARITH_TAC;
759 MP_TAC(REAL_ARITH`v'< &0==> ~(&0 < v')`)
760 THEN RESA_TAC
761 THEN STRIP_TAC;
762 ONCE_REWRITE_TAC[CROSS_SKEW]
763 THEN ASM_REWRITE_TAC[DOT_LNEG;]
764 THEN REAL_ARITH_TAC;
765 POP_ASSUM MP_TAC
766 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
767 THEN ASM_REWRITE_TAC[DOT_LNEG; REAL_ARITH`&0< -- A<=> ~(&0 <= A)`];
768 POP_ASSUM MP_TAC
769 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
770 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
771 THEN ASM_REWRITE_TAC[DOT_LNEG; REAL_ARITH` A< &0 <=> ~(&0 <= A)`];
772 POP_ASSUM MP_TAC
773 THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats (l:real^(M,3)finite_product))
774 ==> w IN V_SY (vecmats l) `)
775 THEN RESA_TAC
776 THEN MRESA_TAC (GEN_ALL CROSS_DOT_POS_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`y1:real^3`;`w:real^3`;`l:real^(M,3)finite_product`]
777 THEN SUBGOAL_THEN`w IN aff{vec 0, y,z:real^3}` ASSUME_TAC;
778 ASM_REWRITE_TAC[VECTOR_ARITH`A- vec 0=A`;IN_ELIM_THM];
779 STRIP_TAC;
780 POP_ASSUM MP_TAC
781 THEN POP_ASSUM MP_TAC
782 THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
783 THEN STRIP_TAC 
784 THEN STRIP_TAC 
785 THEN SUBGOAL_THEN`z1 IN aff{vec 0,u,w:real^3}` ASSUME_TAC;
786 MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`u:real^3`;`w:real^3`]
787 THEN REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
788 THEN EXPAND_TAC"u"
789 THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;DOT_LADD;DOT_LMUL;CROSS_RADD;CROSS_RMUL;DOT_CROSS_SELF;CROSS_REFL;DOT_LZERO]
790 THEN ASM_REWRITE_TAC[]
791 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
792 THEN ASM_REWRITE_TAC[]
793 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
794 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
795 THEN ASM_REWRITE_TAC[CROSS_LNEG;DOT_LNEG]
796 THEN REAL_ARITH_TAC;
797 POP_ASSUM MP_TAC
798 THEN POP_ASSUM MP_TAC
799 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
800 THEN STRIP_TAC
801 THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
802 THEN STRIP_TAC
803 THEN FIND_ASSUM MP_TAC `&0 <= (u cross y1) dot z1`
804 THEN POP_ASSUM(fun th-> REWRITE_TAC[th;DOT_RADD;DOT_RMUL;DOT_CROSS_SELF;REAL_ARITH`A * &0+B=B`] THEN ASSUME_TAC (SYM th))
805 THEN MP_TAC(REAL_ARITH`&0 <= (u cross y1) dot w==> (u cross y1) dot w = &0 \/ &0 < (u cross y1) dot w`)
806 THEN RESA_TAC;
807 SUBGOAL_THEN`{u,row (SUC (i' MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
808 REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
809 THEN EXISTS_TAC`i':num`
810 THEN ASM_REWRITE_TAC[];
811 POP_ASSUM MP_TAC
812 THEN RESA_TAC
813 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y1:real^3`;`u:real^3`]
814 THEN SUBGOAL_THEN`w IN aff{vec 0,u,y1:real^3}` ASSUME_TAC;
815 MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`u:real^3`;`y1:real^3`]
816 THEN ASM_REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`];
817 POP_ASSUM MP_TAC
818 THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
819 THEN STRIP_TAC 
820 THEN POP_ASSUM (fun th-> ASSUME_TAC (SYM th))
821 THEN DISJ_CASES_TAC(REAL_ARITH`w''''< &0 \/ &0<= w''''`);
822 SUBGOAL_THEN`w IN aff_lt{vec 0,u} {y1:real^3}` ASSUME_TAC;
823 ASM_SIMP_TAC[AFF_LT_2_1;IN_ELIM_THM]
824 THEN EXISTS_TAC`u'''':real`
825 THEN EXISTS_TAC`v'''':real`
826 THEN EXISTS_TAC`w'''':real`
827 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A % vec 0+C=C`];
828 MRESA_TAC(GEN_ALL IVS_RHO_NODE_IN_EDGE)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`]
829 THEN MRESA_TAC AZIM_EQ_PI_ALT[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`w:real^3`]
830 THEN SUBGOAL_THEN`coplanar{vec 0, u, y1, z1:real^3} `ASSUME_TAC;
831 ASM_SIMP_TAC[Local_lemmas.COPLANAR_IFF_CROSS_DOT;VECTOR_ARITH`A- vec 0=A`]
832 THEN EXPAND_TAC"z1"
833 THEN REWRITE_TAC[DOT_RADD;DOT_RMUL]
834 THEN ASM_REWRITE_TAC[DOT_CROSS_SELF]
835 THEN REAL_ARITH_TAC;
836 MRESA_TAC(GEN_ALL Local_lemmas.LOFA_IMP_NOT_COLL_IVS)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`]
837 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`z1:real^3`];
838 MRESA_TAC Fan.UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`;`y1:real^3`;`z1:real^3`]
839 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`]
840 THEN POP_ASSUM (fun th-> MRESA1_TAC th`u:real^3`)
841 THEN MRESA_TAC(GEN_ALL RHO_IVS_IDD)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`];
842 POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
843 THEN MRESA_TAC AZIM_EQ[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`z1:real^3`;`w:real^3`]
844 THEN MP_TAC(SET_RULE`w IN aff_gt {vec 0, u} {z1}
845 /\  aff_gt {vec 0, u} {z1} SUBSET aff_ge {vec 0, u} {z1}
846 ==> w IN aff_ge {vec 0, u} {z1:real^3}`)
847 THEN ASM_REWRITE_TAC[AFF_GT_SUBSET_AFF_GE]
848 THEN STRIP_TAC
849 THEN MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`w:real^3`];
850 MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`z1:real^3`;`u:real^3`;`w:real^3`]
851 THEN POP_ASSUM MP_TAC
852 THEN SUBGOAL_THEN`z1 IN ball_annulus` ASSUME_TAC;
853 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
854 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
855 THEN STRIP_TAC
856 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
857 SUBGOAL_THEN `&2<= norm (z1- u:real^3)` ASSUME_TAC;
858 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
859 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
860 THEN STRIP_TAC
861 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
862 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
863 THEN POP_ASSUM MP_TAC
864 THEN RESA_TAC
865 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`z1:real^3`;`u:real^3`];
866 MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`l:real^(M,3)finite_product`];
867 SUBGOAL_THEN `&2<= norm (z1- w:real^3)` ASSUME_TAC;
868 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
869 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
870 THEN STRIP_TAC
871 THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
872 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
873 THEN STRIP_TAC
874 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
875 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
876 THEN POP_ASSUM MP_TAC
877 THEN RESA_TAC
878 THEN POP_ASSUM(fun th-> MP_TAC(SYM th))
879 THEN REMOVE_ASSUM_TAC
880 THEN REMOVE_ASSUM_TAC
881 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
882 THEN STRIP_TAC
883 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
884 THEN ASM_TAC
885 THEN SET_TAC[];
886 MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i''':num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`w:real^3`;`l:real^(M,3)finite_product`];
887 ASM_REWRITE_TAC[]
888 THEN STRIP_TAC
889 THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`z1:real^3`]
890 THEN POP_ASSUM MP_TAC
891 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
892 THEN ASM_REWRITE_TAC[]
893 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
894 THEN ASM_REWRITE_TAC[];
895 DISJ_CASES_TAC(SET_RULE`z1=w \/ ~(z1= w:real^3)`);
896 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
897 THEN ASM_TAC
898 THEN SET_TAC[];
899 MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
900 THEN POP_ASSUM MP_TAC
901 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
902 THEN RESA_TAC
903 THEN MP_TAC(SET_RULE`~(z1=w) /\ ~(u=w)==> {u,z1} INTER {w:real^3}={}`)
904 THEN RESA_TAC
905 THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
906 EXISTS_TAC`w:real^3`
907 THEN ASM_REWRITE_TAC[];
908 FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
909 THEN REWRITE_TAC[FAN;fan7]
910 THEN STRIP_TAC
911 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`{u,z1:real^3}`;`{w:real^3}`][UNION;IN_ELIM_THM;AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])
912 THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
913 THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
914 /\ aff_ge {vec 0} {u, z1} INTER aff_ge {vec 0} {w} = {vec 0}
915 /\ w IN aff_ge {vec 0} {u, z1}
916 ==> vec 0= w:real^3`)
917 THEN RESA_TAC;
918 SUBGOAL_THEN`w IN aff_ge{vec 0:real^3,u} {y1}` ASSUME_TAC;
919 ASM_SIMP_TAC[AFF_GE_2_1;IN_ELIM_THM]
920 THEN EXISTS_TAC`u'''':real`
921 THEN EXISTS_TAC`v'''':real`
922 THEN EXISTS_TAC`w'''':real`
923 THEN ASM_REWRITE_TAC[]
924 THEN VECTOR_ARITH_TAC;
925 MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`w:real^3`];
926 MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`y1:real^3`;`u:real^3`;`w:real^3`]
927 THEN POP_ASSUM MP_TAC
928 THEN SUBGOAL_THEN`y1 IN ball_annulus` ASSUME_TAC;
929 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
930 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
931 THEN STRIP_TAC
932 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
933 SUBGOAL_THEN `&2<= norm (y1- u:real^3)` ASSUME_TAC;
934 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
935 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
936 THEN STRIP_TAC
937 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
938 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
939 THEN POP_ASSUM MP_TAC
940 THEN RESA_TAC
941 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y1:real^3`;`u:real^3`];
942 MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`y1:real^3`;`u:real^3`;`l:real^(M,3)finite_product`];
943 SUBGOAL_THEN `&2<= norm (y1- w:real^3)` ASSUME_TAC;
944 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
945 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
946 THEN STRIP_TAC
947 THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
948 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
949 THEN STRIP_TAC
950 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
951 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
952 THEN POP_ASSUM MP_TAC
953 THEN RESA_TAC
954 THEN POP_ASSUM(fun th-> MP_TAC(SYM th))
955 THEN REMOVE_ASSUM_TAC
956 THEN REMOVE_ASSUM_TAC
957 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
958 THEN STRIP_TAC
959 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
960 THEN ASM_TAC
961 THEN SET_TAC[];
962 MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i''':num`;`a:num#num->real`;`b:num#num->real`;`y1:real^3`;`w:real^3`;`l:real^(M,3)finite_product`];
963 ASM_REWRITE_TAC[]
964 THEN STRIP_TAC
965 THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`y1:real^3`]
966 THEN POP_ASSUM MP_TAC
967 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
968 THEN ASM_REWRITE_TAC[]
969 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
970 THEN ASM_REWRITE_TAC[];
971 DISJ_CASES_TAC(SET_RULE`y1=w \/ ~(y1= w:real^3)`);
972 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
973 THEN ASM_TAC
974 THEN SET_TAC[];
975 MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
976 THEN POP_ASSUM MP_TAC
977 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
978 THEN RESA_TAC
979 THEN MP_TAC(SET_RULE`~(y1=w) /\ ~(u=w)==> {u,y1} INTER {w:real^3}={}`)
980 THEN RESA_TAC
981 THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
982 EXISTS_TAC`w:real^3`
983 THEN ASM_REWRITE_TAC[];
984 FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
985 THEN REWRITE_TAC[FAN;fan7]
986 THEN STRIP_TAC
987 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`{u,y1:real^3}`;`{w:real^3}`][UNION;IN_ELIM_THM;AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])
988 THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
989 THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
990 /\ aff_ge {vec 0} {u, y1} INTER aff_ge {vec 0} {w} = {vec 0}
991 /\ w IN aff_ge {vec 0} {u, y1}
992 ==> vec 0= w:real^3`)
993 THEN RESA_TAC;
994 MP_TAC(REAL_ARITH`&0 < (u cross y1:real^3) dot w ==> ~((u cross y1) dot w = &0) /\ ~((u cross y1) dot w < &0)`)
995 THEN RESA_TAC
996 THEN ASM_REWRITE_TAC[REAL_MUL_POS_LE]
997 THEN STRIP_TAC;
998 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
999 THEN ASM_TAC
1000 THEN REWRITE_TAC[VECTOR_ARITH`&0 %A= vec 0/\ A + vec 0=A`]
1001 THEN REPEAT STRIP_TAC
1002 THEN SUBGOAL_THEN`z1 IN aff{vec 0, u:real^3}`ASSUME_TAC;
1003 REWRITE_TAC[aff;AFFINE_HULL_2;IN_ELIM_THM]
1004 THEN EXISTS_TAC`&1- v''':real`
1005 THEN EXISTS_TAC`v''':real`
1006 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - v''' + v''' = &1`]
1007 THEN VECTOR_ARITH_TAC;
1008 MRESA_TAC(GEN_ALL Local_lemmas.LOFA_IMP_NOT_COLL_IVS)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`]
1009 THEN MRESA_TAC th3[`vec 0:real^3`;`u:real^3`;`z1:real^3`];
1010 POP_ASSUM MP_TAC
1011 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOFA_IMP_NOT_COLL_IVS)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`]
1012 THEN MRESA_TAC th3[`vec 0:real^3`;`u:real^3`;`z1:real^3`]
1013 THEN STRIP_TAC
1014 THEN SUBGOAL_THEN`w IN aff_ge{vec 0:real^3,u} {z1}` ASSUME_TAC;
1015 ASM_SIMP_TAC[AFF_GE_2_1;IN_ELIM_THM]
1016 THEN EXISTS_TAC`&1 + (inv w''') *v''' - inv w''':real`
1017 THEN EXISTS_TAC`-- (inv w''') *v''':real`
1018 THEN EXISTS_TAC`inv w''':real`
1019 THEN ASM_REWRITE_TAC[REAL_ARITH`(&1 + inv w''' * v''' - inv w''') + --inv w''' * v''' + inv w''' = &1`]
1020 THEN EXPAND_TAC"z1"
1021 THEN REWRITE_TAC[VECTOR_ARITH`(&1 + inv w''' * v''' - inv w''') % vec 0 +
1022  (--inv w''' * v''') % u +
1023  inv w''' % (v''' % u + w''' % w)
1024 = (inv w''' *w''') % w`]
1025 THEN MP_TAC(REAL_ARITH`&0< w'''==> ~(w'''= &0)`)
1026 THEN RESA_TAC
1027 THEN MRESAL1_TAC REAL_MUL_LINV`w''':real`[VECTOR_ARITH`A= &1 %A`]
1028 THEN MATCH_MP_TAC REAL_LE_INV
1029 THEN REMOVE_ASSUM_TAC
1030 THEN REMOVE_ASSUM_TAC
1031 THEN POP_ASSUM MP_TAC
1032 THEN REAL_ARITH_TAC;
1033 POP_ASSUM MP_TAC
1034 THEN POP_ASSUM MP_TAC
1035 THEN DISCH_THEN(LABEL_TAC"A")
1036 THEN STRIP_TAC
1037 THEN REMOVE_THEN"A" MP_TAC
1038 THEN MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`w:real^3`];
1039 MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`z1:real^3`;`u:real^3`;`w:real^3`]
1040 THEN POP_ASSUM MP_TAC
1041 THEN SUBGOAL_THEN`z1 IN ball_annulus` ASSUME_TAC;
1042 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1043 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1044 THEN STRIP_TAC
1045 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
1046 SUBGOAL_THEN `&2<= norm (z1- u:real^3)` ASSUME_TAC;
1047 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1048 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1049 THEN STRIP_TAC
1050 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
1051 POP_ASSUM MP_TAC
1052 THEN POP_ASSUM MP_TAC
1053 THEN MRESA_TAC th3[`u:real^3`;`z1:real^3`;`vec 0:real^3`]
1054 THEN POP_ASSUM MP_TAC
1055 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
1056 THEN RESA_TAC
1057 THEN STRIP_TAC
1058 THEN STRIP_TAC
1059 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1060 THEN POP_ASSUM MP_TAC
1061 THEN RESA_TAC;
1062 MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`l:real^(M,3)finite_product`];
1063 SUBGOAL_THEN `&2<= norm (z1- w:real^3)` ASSUME_TAC;
1064 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1065 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1066 THEN STRIP_TAC
1067 THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
1068 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1069 THEN STRIP_TAC
1070 THEN MRESA_TAC(GEN_ALL IVS_RHO_NODE_IN_EDGE)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`]
1071 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
1072 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1073 THEN POP_ASSUM MP_TAC
1074 THEN RESA_TAC
1075 THEN POP_ASSUM MP_TAC
1076 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1077 THEN ASM_REWRITE_TAC[];
1078 MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i''':num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`w:real^3`;`l:real^(M,3)finite_product`];
1079 ASM_REWRITE_TAC[]
1080 THEN STRIP_TAC
1081 THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`z1:real^3`]
1082 THEN POP_ASSUM MP_TAC
1083 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1084 THEN ASM_REWRITE_TAC[]
1085 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
1086 THEN ASM_REWRITE_TAC[];
1087 DISJ_CASES_TAC(SET_RULE`z1=w \/ ~(z1= w:real^3)`);
1088 MRESA_TAC(GEN_ALL IVS_RHO_NODE_IN_EDGE)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`];
1089 MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
1090 THEN POP_ASSUM MP_TAC
1091 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
1092 THEN RESA_TAC
1093 THEN MP_TAC(SET_RULE`~(z1=w) /\ ~(u=w)==> {u,z1} INTER {w:real^3}={}`)
1094 THEN RESA_TAC
1095 THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
1096 EXISTS_TAC`w:real^3`
1097 THEN ASM_REWRITE_TAC[];
1098 MRESA_TAC(GEN_ALL IVS_RHO_NODE_IN_EDGE)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`]
1099 THEN FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
1100 THEN REWRITE_TAC[FAN;fan7]
1101 THEN STRIP_TAC
1102 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`{u,z1:real^3}`;`{w:real^3}`][UNION;IN_ELIM_THM;AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])
1103 THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
1104 THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
1105 /\ aff_ge {vec 0} {u, z1} INTER aff_ge {vec 0} {w} = {vec 0}
1106 /\ w IN aff_ge {vec 0} {u, z1}
1107 ==> vec 0= w:real^3`)
1108 THEN RESA_TAC;
1109 POP_ASSUM MP_TAC
1110 THEN POP_ASSUM MP_TAC
1111 THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
1112 THEN STRIP_TAC 
1113 THEN STRIP_TAC 
1114 THEN SUBGOAL_THEN`y1 IN aff{vec 0,u,w:real^3}` ASSUME_TAC;
1115 MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`u:real^3`;`w:real^3`]
1116 THEN REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
1117 THEN EXPAND_TAC"u"
1118 THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;DOT_LADD;DOT_LMUL;CROSS_RADD;CROSS_RMUL;DOT_CROSS_SELF;CROSS_REFL;DOT_LZERO]
1119 THEN ASM_REWRITE_TAC[]
1120 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
1121 THEN ASM_REWRITE_TAC[CROSS_LNEG;DOT_LNEG]
1122 THEN REAL_ARITH_TAC;
1123 POP_ASSUM MP_TAC
1124 THEN POP_ASSUM MP_TAC
1125 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
1126 THEN STRIP_TAC
1127 THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
1128 THEN STRIP_TAC
1129 THEN FIND_ASSUM MP_TAC `&0 <= (u cross y1) dot z1`
1130 THEN POP_ASSUM(fun th-> REWRITE_TAC[th;CROSS_RADD;CROSS_RMUL;DOT_LADD;DOT_LMUL;DOT_CROSS_SELF;] THEN ASSUME_TAC (SYM th))
1131 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1132 THEN REWRITE_TAC[DOT_CROSS_SELF;REAL_ARITH`A * &0+B=B`]
1133 THEN MP_TAC(REAL_ARITH`&0 <= (z1 cross u) dot w==> (z1 cross u) dot w = &0 \/ &0 < (z1 cross u) dot w`)
1134 THEN RESA_TAC;
1135 SUBGOAL_THEN`{u,row (SUC (i' MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
1136 REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
1137 THEN EXISTS_TAC`i':num`
1138 THEN ASM_REWRITE_TAC[];
1139 POP_ASSUM MP_TAC
1140 THEN RESA_TAC
1141 THEN MRESA_TAC(GEN_ALL IVS_RHO_NODE_IN_EDGE)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`]
1142 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`z1:real^3`;`u:real^3`]
1143 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y1:real^3`;`u:real^3`]
1144 THEN SUBGOAL_THEN`w IN aff{vec 0,u,z1:real^3}` ASSUME_TAC;
1145 MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`u:real^3`;`z1:real^3`]
1146 THEN ASM_REWRITE_TAC[IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
1147 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
1148 THEN ASM_REWRITE_TAC[CROSS_LNEG;DOT_LNEG]
1149 THEN REAL_ARITH_TAC;
1150 POP_ASSUM MP_TAC
1151 THEN REWRITE_TAC[AFFINE_HULL_3;aff;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 +C=C`]
1152 THEN STRIP_TAC 
1153 THEN POP_ASSUM (fun th-> ASSUME_TAC (SYM th))
1154 THEN DISJ_CASES_TAC(REAL_ARITH`w''''< &0 \/ &0<= w''''`);
1155 SUBGOAL_THEN`w IN aff_lt{vec 0,u} {z1:real^3}` ASSUME_TAC;
1156 ASM_SIMP_TAC[AFF_LT_2_1;IN_ELIM_THM]
1157 THEN EXISTS_TAC`u'''':real`
1158 THEN EXISTS_TAC`v'''':real`
1159 THEN EXISTS_TAC`w'''':real`
1160 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A % vec 0+C=C`];
1161 MRESA_TAC AZIM_EQ_PI_ALT[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`w:real^3`]
1162 THEN SUBGOAL_THEN`coplanar{vec 0, u, z1, y1:real^3} `ASSUME_TAC;
1163 ASM_SIMP_TAC[Local_lemmas.COPLANAR_IFF_CROSS_DOT;VECTOR_ARITH`A- vec 0=A`]
1164 THEN EXPAND_TAC"y1"
1165 THEN REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_LADD;CROSS_LADD;DOT_RADD;DOT_RMUL;CROSS_REFL]
1166 THEN ASM_REWRITE_TAC[DOT_CROSS_SELF;]
1167 THEN ONCE_REWRITE_TAC[CROSS_SKEW]
1168 THEN ASM_REWRITE_TAC[CROSS_LNEG;DOT_LNEG]
1169 THEN REAL_ARITH_TAC;
1170 MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`y1:real^3`];
1171 MRESA_TAC Fan.UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`;`z1:real^3`;`y1:real^3`]
1172 THEN POP_ASSUM MP_TAC
1173 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`]
1174 THEN POP_ASSUM (fun th-> MRESA1_TAC th`u:real^3`)
1175 THEN STRIP_TAC
1176 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
1177 THEN MRESA_TAC(GEN_ALL RHO_IVS_IDD)[`E_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`u:real^3`];
1178 POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
1179 THEN MRESA_TAC AZIM_EQ[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`y1:real^3`;`w:real^3`]
1180 THEN MP_TAC(SET_RULE`w IN aff_gt {vec 0, u} {y1}
1181 /\  aff_gt {vec 0, u} {y1} SUBSET aff_ge {vec 0, u} {y1}
1182 ==> w IN aff_ge {vec 0, u} {y1:real^3}`)
1183 THEN ASM_REWRITE_TAC[AFF_GT_SUBSET_AFF_GE]
1184 THEN STRIP_TAC
1185 THEN MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`w:real^3`];
1186 MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`y1:real^3`;`u:real^3`;`w:real^3`]
1187 THEN POP_ASSUM MP_TAC
1188 THEN SUBGOAL_THEN`y1 IN ball_annulus` ASSUME_TAC;
1189 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1190 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1191 THEN STRIP_TAC
1192 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
1193 SUBGOAL_THEN `&2<= norm (y1- u:real^3)` ASSUME_TAC;
1194 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1195 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1196 THEN STRIP_TAC
1197 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
1198 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1199 THEN POP_ASSUM MP_TAC
1200 THEN RESA_TAC
1201 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y1:real^3`;`u:real^3`];
1202 MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`y1:real^3`;`u:real^3`;`l:real^(M,3)finite_product`];
1203 SUBGOAL_THEN `&2<= norm (y1- w:real^3)` ASSUME_TAC;
1204 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1205 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1206 THEN STRIP_TAC
1207 THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
1208 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1209 THEN STRIP_TAC
1210 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
1211 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1212 THEN POP_ASSUM MP_TAC
1213 THEN RESA_TAC
1214 THEN POP_ASSUM(fun th-> MP_TAC(SYM th))
1215 THEN REMOVE_ASSUM_TAC
1216 THEN REMOVE_ASSUM_TAC
1217 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1218 THEN STRIP_TAC
1219 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1220 THEN ASM_TAC
1221 THEN SET_TAC[];
1222 MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i''':num`;`a:num#num->real`;`b:num#num->real`;`y1:real^3`;`w:real^3`;`l:real^(M,3)finite_product`];
1223 ASM_REWRITE_TAC[]
1224 THEN STRIP_TAC
1225 THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`y1:real^3`]
1226 THEN POP_ASSUM MP_TAC
1227 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1228 THEN ASM_REWRITE_TAC[]
1229 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
1230 THEN ASM_REWRITE_TAC[]
1231 THEN STRIP_TAC
1232 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1233 THEN ASM_REWRITE_TAC[];
1234 DISJ_CASES_TAC(SET_RULE`y1=w \/ ~(y1= w:real^3)`);
1235 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1236 THEN ASM_TAC
1237 THEN SET_TAC[];
1238 MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
1239 THEN POP_ASSUM MP_TAC
1240 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
1241 THEN RESA_TAC
1242 THEN MP_TAC(SET_RULE`~(y1=w) /\ ~(u=w)==> {u,y1} INTER {w:real^3}={}`)
1243 THEN RESA_TAC
1244 THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
1245 EXISTS_TAC`w:real^3`
1246 THEN ASM_REWRITE_TAC[];
1247 FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
1248 THEN REWRITE_TAC[FAN;fan7]
1249 THEN STRIP_TAC
1250 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`{u,y1:real^3}`;`{w:real^3}`][UNION;IN_ELIM_THM;AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])
1251 THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
1252 THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
1253 /\ aff_ge {vec 0} {u, y1} INTER aff_ge {vec 0} {w} = {vec 0}
1254 /\ w IN aff_ge {vec 0} {u, y1}
1255 ==> vec 0= w:real^3`)
1256 THEN RESA_TAC;
1257 SUBGOAL_THEN`w IN aff_ge{vec 0:real^3,u} {z1}` ASSUME_TAC;
1258 ASM_SIMP_TAC[AFF_GE_2_1;IN_ELIM_THM]
1259 THEN EXISTS_TAC`u'''':real`
1260 THEN EXISTS_TAC`v'''':real`
1261 THEN EXISTS_TAC`w'''':real`
1262 THEN ASM_REWRITE_TAC[]
1263 THEN VECTOR_ARITH_TAC;
1264 MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`z1:real^3`;`w:real^3`];
1265 MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`z1:real^3`;`u:real^3`;`w:real^3`]
1266 THEN POP_ASSUM MP_TAC
1267 THEN SUBGOAL_THEN`z1 IN ball_annulus` ASSUME_TAC;
1268 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1269 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1270 THEN STRIP_TAC
1271 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
1272 SUBGOAL_THEN `&2<= norm (z1- u:real^3)` ASSUME_TAC;
1273 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1274 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1275 THEN STRIP_TAC
1276 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
1277 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1278 THEN POP_ASSUM MP_TAC
1279 THEN RESA_TAC
1280 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`z1:real^3`;`u:real^3`];
1281 MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`u:real^3`;`l:real^(M,3)finite_product`];
1282 SUBGOAL_THEN `&2<= norm (z1- w:real^3)` ASSUME_TAC;
1283 FIND_ASSUM MP_TAC`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1284 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1285 THEN STRIP_TAC
1286 THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
1287 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1288 THEN STRIP_TAC
1289 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
1290 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1291 THEN POP_ASSUM MP_TAC
1292 THEN RESA_TAC
1293 THEN POP_ASSUM(fun th-> MP_TAC(SYM th))
1294 THEN REMOVE_ASSUM_TAC
1295 THEN REMOVE_ASSUM_TAC
1296 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1297 THEN STRIP_TAC
1298 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1299 THEN ASM_TAC
1300 THEN SET_TAC[];
1301 MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i''':num`;`a:num#num->real`;`b:num#num->real`;`z1:real^3`;`w:real^3`;`l:real^(M,3)finite_product`];
1302 ASM_REWRITE_TAC[]
1303 THEN STRIP_TAC
1304 THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`z1:real^3`]
1305 THEN POP_ASSUM MP_TAC
1306 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1307 THEN ASM_REWRITE_TAC[]
1308 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
1309 THEN ASM_REWRITE_TAC[];
1310 DISJ_CASES_TAC(SET_RULE`z1=w \/ ~(z1= w:real^3)`);
1311 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1312 THEN ASM_TAC
1313 THEN SET_TAC[];
1314 MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
1315 THEN POP_ASSUM MP_TAC
1316 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
1317 THEN RESA_TAC
1318 THEN MP_TAC(SET_RULE`~(z1=w) /\ ~(u=w)==> {u,z1} INTER {w:real^3}={}`)
1319 THEN RESA_TAC
1320 THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
1321 EXISTS_TAC`w:real^3`
1322 THEN ASM_REWRITE_TAC[];
1323 FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
1324 THEN REWRITE_TAC[FAN;fan7]
1325 THEN STRIP_TAC
1326 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`{u,z1:real^3}`;`{w:real^3}`][UNION;IN_ELIM_THM;AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])
1327 THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
1328 THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
1329 /\ aff_ge {vec 0} {u, z1} INTER aff_ge {vec 0} {w} = {vec 0}
1330 /\ w IN aff_ge {vec 0} {u, z1}
1331 ==> vec 0= w:real^3`)
1332 THEN RESA_TAC;
1333 ONCE_REWRITE_TAC[CROSS_TRIPLE]
1334 THEN MP_TAC(REAL_ARITH`&0 < (z1 cross u:real^3) dot w ==> ~((z1 cross u) dot w = &0) /\ ~((z1 cross u) dot w < &0)`)
1335 THEN RESA_TAC
1336 THEN ASM_REWRITE_TAC[REAL_MUL_POS_LE]
1337 THEN STRIP_TAC;
1338 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1339 THEN ASM_TAC
1340 THEN REWRITE_TAC[VECTOR_ARITH`&0 %A= vec 0/\ A + vec 0=A`]
1341 THEN REPEAT STRIP_TAC
1342 THEN SUBGOAL_THEN`y1 IN aff{vec 0, u:real^3}`ASSUME_TAC;
1343 REWRITE_TAC[aff;AFFINE_HULL_2;IN_ELIM_THM]
1344 THEN EXISTS_TAC`&1- v''':real`
1345 THEN EXISTS_TAC`v''':real`
1346 THEN ASM_REWRITE_TAC[REAL_ARITH`&1 - v''' + v''' = &1`]
1347 THEN VECTOR_ARITH_TAC;
1348 SUBGOAL_THEN`{u,row (SUC (i' MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
1349 REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
1350 THEN EXISTS_TAC`i':num`
1351 THEN ASM_REWRITE_TAC[];
1352 POP_ASSUM MP_TAC
1353 THEN RESA_TAC
1354 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y1:real^3`;`u:real^3`];
1355 SUBGOAL_THEN`{u,row (SUC (i' MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
1356 REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
1357 THEN EXISTS_TAC`i':num`
1358 THEN ASM_REWRITE_TAC[];
1359 POP_ASSUM MP_TAC
1360 THEN RESA_TAC
1361 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y1:real^3`;`u:real^3`]
1362 THEN SUBGOAL_THEN`w IN aff_ge{vec 0:real^3,u} {y1}` ASSUME_TAC;
1363 ASM_SIMP_TAC[AFF_GE_2_1;IN_ELIM_THM]
1364 THEN EXISTS_TAC`&1 + (inv w''') *v''' - inv w''':real`
1365 THEN EXISTS_TAC`-- (inv w''') *v''':real`
1366 THEN EXISTS_TAC`inv w''':real`
1367 THEN ASM_REWRITE_TAC[REAL_ARITH`(&1 + inv w''' * v''' - inv w''') + --inv w''' * v''' + inv w''' = &1`]
1368 THEN EXPAND_TAC"y1"
1369 THEN REWRITE_TAC[VECTOR_ARITH`(&1 + inv w''' * v''' - inv w''') % vec 0 +
1370  (--inv w''' * v''') % u +
1371  inv w''' % (v''' % u + w''' % w)
1372 = (inv w''' *w''') % w`]
1373 THEN MP_TAC(REAL_ARITH`&0< w'''==> ~(w'''= &0)`)
1374 THEN RESA_TAC
1375 THEN MRESAL1_TAC REAL_MUL_LINV`w''':real`[VECTOR_ARITH`A= &1 %A`]
1376 THEN MATCH_MP_TAC REAL_LE_INV
1377 THEN ASM_TAC 
1378 THEN REAL_ARITH_TAC;
1379 REMOVE_THEN "THY4" MP_TAC
1380 THEN MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`u:real^3`;`y1:real^3`;`w:real^3`];
1381 MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`y1:real^3`;`u:real^3`;`w:real^3`]
1382 THEN POP_ASSUM MP_TAC
1383 THEN SUBGOAL_THEN`y1 IN ball_annulus` ASSUME_TAC;
1384 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1385 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1386 THEN STRIP_TAC
1387 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`i'':num`);
1388 SUBGOAL_THEN `&2<= norm (y1- u:real^3)` ASSUME_TAC;
1389 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1390 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1391 THEN STRIP_TAC
1392 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i' \/ ~(i''=i':num)`);
1393 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1394 THEN POP_ASSUM MP_TAC
1395 THEN RESA_TAC
1396 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y1:real^3`;`u:real^3`];
1397 MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`y1:real^3`;`u:real^3`;`l:real^(M,3)finite_product`];
1398 SUBGOAL_THEN `&2<= norm (y1- w:real^3)` ASSUME_TAC;
1399 FIND_ASSUM MP_TAC`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))`
1400 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1401 THEN STRIP_TAC
1402 THEN FIND_ASSUM MP_TAC`w IN V_SY (vecmats (l:real^(M,3)finite_product))`
1403 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1404 THEN STRIP_TAC
1405 THEN DISJ_CASES_TAC(ARITH_RULE`i''= i''' \/ ~(i''=i''':num)`);
1406 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1407 THEN POP_ASSUM MP_TAC
1408 THEN RESA_TAC
1409 THEN POP_ASSUM(fun th-> MP_TAC(SYM th))
1410 THEN REMOVE_ASSUM_TAC
1411 THEN REMOVE_ASSUM_TAC
1412 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1413 THEN STRIP_TAC
1414 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1415 THEN ASM_TAC
1416 THEN SET_TAC[];
1417 MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i'':num`;`i''':num`;`a:num#num->real`;`b:num#num->real`;`y1:real^3`;`w:real^3`;`l:real^(M,3)finite_product`];
1418 ASM_REWRITE_TAC[]
1419 THEN STRIP_TAC
1420 THEN MRESA_TAC (Planarity.properties_of_collinear4_points_fan)[`vec 0:real^3`;`w:real^3`;`u:real^3`;`y1:real^3`]
1421 THEN POP_ASSUM MP_TAC
1422 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1423 THEN ASM_REWRITE_TAC[]
1424 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
1425 THEN ASM_REWRITE_TAC[]
1426 THEN STRIP_TAC
1427 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1428 THEN ASM_REWRITE_TAC[];
1429 DISJ_CASES_TAC(SET_RULE`y1=w \/ ~(y1= w:real^3)`);
1430 POP_ASSUM (fun th-> SUBST_ALL_TAC(th))
1431 THEN ASM_TAC
1432 THEN SET_TAC[];
1433 MRESA_TAC th3[`u:real^3`;`w:real^3`;`vec 0:real^3`]
1434 THEN POP_ASSUM MP_TAC
1435 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`]
1436 THEN RESA_TAC
1437 THEN MP_TAC(SET_RULE`~(y1=w) /\ ~(u=w)==> {u,y1} INTER {w:real^3}={}`)
1438 THEN RESA_TAC
1439 THEN SUBGOAL_THEN`(?v. v IN V_SY (vecmats (l:real^(M,3)finite_product)) /\ {w} = {v:real^3})` ASSUME_TAC;
1440 EXISTS_TAC`w:real^3`
1441 THEN ASM_REWRITE_TAC[];
1442 FIND_ASSUM MP_TAC`FAN (vec 0,V_SY (vecmats l),E_SY (vecmats (l:real^(M,3)finite_product)))`
1443 THEN REWRITE_TAC[FAN;fan7]
1444 THEN STRIP_TAC
1445 THEN POP_ASSUM(fun th-> MRESAL_TAC th[`{u,y1:real^3}`;`{w:real^3}`][UNION;IN_ELIM_THM;AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING])
1446 THEN MRESA_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`w:real^3`]
1447 THEN MP_TAC(SET_RULE`w IN aff_ge {vec 0} {w}
1448 /\ aff_ge {vec 0} {u, y1} INTER aff_ge {vec 0} {w} = {vec 0}
1449 /\ w IN aff_ge {vec 0} {u, y1}
1450 ==> vec 0= w:real^3`)
1451 THEN RESA_TAC]);;
1452
1453
1454
1455
1456 let TECOXBM1=prove_by_refinement(`!l:real^(M,3)finite_product. stable_system k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\ k= dimindex(:M)/\ 2<k/\
1457 {u,w} SUBSET V_SY(vecmats(l))
1458 /\ norm(u-w)<= cstab
1459 /\ &2<= norm(u-w)
1460 /\ ~({u,w} IN E_SY(vecmats l))
1461 /\l IN B_SY1 a b
1462 ==> (!x. x IN F_SY(vecmats l)==> aff_gt {vec 0}{u,w} SUBSET wedge_in_fan_gt x (E_SY (vecmats l))) `,
1463 [GEN_TAC THEN STRIP_TAC
1464 THEN POP_ASSUM(fun th-> ASSUME_TAC th THEN MP_TAC th THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY]
1465 THEN REPEAT STRIP_TAC)
1466 THEN POP_ASSUM MP_TAC
1467 THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
1468 THEN POP_ASSUM MP_TAC 
1469 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1470 THEN POP_ASSUM(fun th-> MP_TAC th
1471 THEN REWRITE_TAC[convex_local_fan]
1472 THEN STRIP_TAC
1473 THEN POP_ASSUM MP_TAC
1474 THEN POP_ASSUM (fun th2-> ASSUME_TAC th2 THEN MP_TAC th2
1475 THEN REWRITE_TAC[local_fan]
1476 THEN LET_TAC
1477 THEN STRIP_TAC
1478 THEN POP_ASSUM MP_TAC
1479 THEN POP_ASSUM(fun th3-> ASSUME_TAC(SYM th3))
1480 THEN STRIP_TAC)
1481 THEN DISCH_THEN(LABEL_TAC"YEU")
1482 THEN ASSUME_TAC th)
1483 THEN STRIP_TAC
1484 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
1485 THEN MP_TAC(SET_RULE`{u,w} SUBSET V_SY(vecmats(l)) ==>  w IN V_SY(vecmats(l:real^(M,3)finite_product)) /\ u IN V_SY(vecmats(l))`)
1486 THEN RESA_TAC
1487 THEN STRIP_TAC
1488 THEN POP_ASSUM(fun th-> MP_TAC th
1489 THEN REWRITE_TAC[F_SY;IN_ELIM_THM;]
1490 THEN STRIP_TAC
1491 THEN ASSUME_TAC th)
1492 THEN ABBREV_TAC`y=row i (vecmats (l:real^(M,3)finite_product))`
1493 THEN ABBREV_TAC`z=row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`
1494 THEN SUBGOAL_THEN `y IN V_SY (vecmats (l:real^(M,3)finite_product))`ASSUME_TAC;
1495 REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1496 THEN EXISTS_TAC`i:num`
1497 THEN ASM_REWRITE_TAC[];
1498 MRESA_TAC (GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1)[`F_SY (vecmats (l:real^(M,3)finite_product))`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`y:real^3`;`E_SY (vecmats (l:real^(M,3)finite_product))`;]
1499 THEN ASM_REWRITE_TAC[wedge_in_fan_gt;ARITH_RULE`2>1`]
1500 THEN MRESA_TAC (GEN_ALL Local_lemmas.DETERMINE_WEDGE_IN_FAN)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`(x:real^3#real^3)`]
1501 THEN MRESA_TAC (GEN_ALL Local_lemmas.PGSQVBL)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`u:real^3`;`w:real^3`;`x:real^3#real^3`;`E_SY (vecmats (l:real^(M,3)finite_product))`]
1502 THEN MRESA_TAC AFF_GT_SUBSET_AFF_GE[`{vec 0:real^3}`;`{u,w:real^3}`]
1503 THEN MP_TAC(SET_RULE`aff_gt {vec 0} {u, w} SUBSET aff_ge {vec 0} {u, w}
1504 /\ aff_ge {vec 0} {u, w} SUBSET wedge_ge (vec 0) y z (azim_cycle (EE y (E_SY (vecmats l))) (vec 0) y z)
1505 ==> aff_gt {vec 0} {u, w} SUBSET wedge_ge (vec 0) y z (azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z)`)
1506 THEN RESA_TAC
1507 THEN POP_ASSUM MP_TAC
1508 THEN REMOVE_THEN "YEU"(fun th-> MRESA1_TAC th`x:real^3#real^3`)
1509 THEN REMOVE_ASSUM_TAC
1510 THEN POP_ASSUM MP_TAC
1511 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`(x:real^3#real^3)`]
1512 THEN ABBREV_TAC`y1=azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z`
1513 THEN REWRITE_TAC[REAL_ARITH`a<= b<=> a=b\/ a< b`]
1514 THEN STRIP_TAC;
1515 MRESA_TAC(GEN_ALL Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT)[`y1:real^3`;`y:real^3`;`z:real^3`;`vec 0:real^3`]
1516 THEN SUBGOAL_THEN`{y,row (SUC (i MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
1517 REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
1518 THEN EXISTS_TAC`i:num`
1519 THEN ASM_REWRITE_TAC[];
1520 POP_ASSUM MP_TAC
1521 THEN RESA_TAC
1522 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`z:real^3`;`y:real^3`]
1523 THEN MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`y:real^3`;`z:real^3`]
1524 THEN MRESA_TAC (GEN_ALL Nkezbfc_local.AZIM_PI_WEDGE_CROSS_DOT)[`y1:real^3`;`y:real^3`;`z:real^3`;`vec 0:real^3`]
1525 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;REAL_ARITH`&0<= A<=> A= &0 \/ &0< A`]
1526 THEN DISCH_THEN(LABEL_TAC"THY4")
1527 THEN REPEAT STRIP_TAC
1528 THEN REMOVE_THEN"THY4"(fun th-> MRESA1_TAC th`x'':real^3`)
1529 THEN SUBGOAL_THEN`x'' IN aff_gt {vec 0} {u, w} INTER aff {vec 0, y, z:real^3}` ASSUME_TAC;
1530 ASM_REWRITE_TAC[INTER;IN_ELIM_THM];
1531 MRESAL_TAC(GEN_ALL AFF_GT_INTER_AFF_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i:num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`w:real^3`;`y:real^3`;`z:real^3`;`l:real^(M,3)finite_product`][B_SY1;IN_ELIM_THM;CONDITION2_SY]
1532 THEN POP_ASSUM MP_TAC
1533 THEN POP_ASSUM MP_TAC
1534 THEN ASM_REWRITE_TAC[]
1535 THEN SET_TAC[];
1536 POP_ASSUM MP_TAC
1537 THEN SUBGOAL_THEN`{y,row (SUC (i MOD k)) (vecmats l)} IN E_SY(vecmats(l:real^(M,3)finite_product))` ASSUME_TAC;
1538 REWRITE_TAC[E_SY;rows;IN_ELIM_THM]
1539 THEN EXISTS_TAC`i:num`
1540 THEN ASM_REWRITE_TAC[];
1541 POP_ASSUM MP_TAC
1542 THEN RESA_TAC
1543 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`z:real^3`;`y:real^3`]
1544 THEN MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`y:real^3`;`z:real^3`]
1545 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`y:real^3`;`z:real^3`]
1546 THEN MRESA_TAC(sigma_fan_in_set_of_edge)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;]
1547 THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats (l:real^(M,3)finite_product))) (E_SY (vecmats (l:real^(M,3)finite_product))) (row i (vecmats (l:real^(M,3)finite_product)))
1548       (row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`]
1549 THEN POP_ASSUM MP_TAC
1550 THEN RESA_TAC
1551 THEN STRIP_TAC
1552 THEN MRESA_TAC(GEN_ALL Local_lemmas.WEDGE_GE_EQ_AFF_GE)[`vec 0:real^3`;`y:real^3`;`z:real^3`;`(azim_cycle (EE y (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) y z)`]
1553 THEN MP_TAC(REAL_ARITH`&0<= azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
1554       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
1555       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))
1556 ==> azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
1557       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
1558       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) = &0 \/
1559 &0< azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
1560       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
1561       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))`)
1562 THEN ASM_REWRITE_TAC[azim]
1563 THEN STRIP_TAC;
1564 MRESA_TAC Fan.UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
1565       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
1566 THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.FAN_IMP_EE_EQ_SET_OF_EDGE)[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]
1567 THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1)[`F_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`]
1568 THEN POP_ASSUM MP_TAC
1569 THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={row (SUC (i MOD dimindex (:M))) (vecmats l)}
1570 \/ ~(set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))})`);
1571 POP_ASSUM MP_TAC
1572 THEN RESA_TAC
1573 THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY;
1574                  IN_INSERT; NOT_IN_EMPTY]
1575 THEN ARITH_TAC;
1576 MRESA_TAC SIGMA_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`]
1577 THEN REMOVE_ASSUM_TAC
1578 THEN POP_ASSUM MP_TAC
1579 THEN ONCE_REWRITE_TAC[SET_RULE`A=B<=>B=A`]
1580 THEN REMOVE_ASSUM_TAC
1581 THEN REMOVE_ASSUM_TAC
1582 THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]);
1583 MP_TAC(REAL_ARITH`
1584 &0<azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
1585       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
1586       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) /\
1587       azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
1588       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
1589       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) <
1590       pi
1591 ==> ~(azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
1592       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
1593       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
1594       &0 \/
1595       azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))
1596       (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
1597       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) =
1598       pi)`)
1599 THEN RESA_TAC
1600 THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
1601       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
1602 THEN POP_ASSUM MP_TAC
1603 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
1604 THEN STRIP_TAC
1605 THEN MRESA_TAC( GEN_ALL Nkezbfc_local.inter_aff_ge_3_1_is_aff_ge_2_2)[`vec 0:real^3`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
1606       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
1607 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1608 THEN MRESAL_TAC Planarity.cross_dot_fully_surrounded_fan[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
1609       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`][VECTOR_ARITH`A- vec 0=A`]
1610 THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot [`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
1611       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`]
1612 THEN POP_ASSUM MP_TAC
1613 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
1614 THEN RESA_TAC
1615 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1616 THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot [`vec 0:real^3`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
1617       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`][VECTOR_ARITH`A- vec 0=A`]
1618 THEN POP_ASSUM MP_TAC
1619 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,C,B}`]
1620 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1621 THEN RESA_TAC
1622 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1623 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1624 THEN MRESA_TAC WEDGE_LUNE[`vec 0:real^3`;`y:real^3`;`z:real^3`;`y1:real^3`]
1625 THEN POP_ASSUM MP_TAC
1626 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
1627 THEN RESA_TAC
1628 THEN MRESA_TAC(inter_aff_gt_3_1_is_aff_gt_2_2)[`vec 0:real^3`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
1629       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`]
1630 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1631 THEN MRESAL_TAC aff_gt_3_1_rep_cross_dot [`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
1632       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`]
1633 THEN POP_ASSUM MP_TAC
1634 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`]
1635 THEN RESA_TAC
1636 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1637 THEN MRESAL_TAC aff_gt_3_1_rep_cross_dot [`vec 0:real^3`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product)))
1638       (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`][VECTOR_ARITH`A- vec 0=A`]
1639 THEN POP_ASSUM MP_TAC
1640 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,C,B}`]
1641 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1642 THEN RESA_TAC
1643 THEN REWRITE_TAC[SUBSET;IN_ELIM_THM;INTER]
1644 THEN DISCH_THEN(LABEL_TAC"YEU1")
1645 THEN REPEAT STRIP_TAC;
1646 REMOVE_THEN "YEU1"(fun th-> MRESA1_TAC th`x'':real^3`)
1647 THEN REMOVE_ASSUM_TAC
1648 THEN POP_ASSUM MP_TAC
1649 THEN REWRITE_TAC[REAL_ARITH`&0<= A<=> A= &0 \/ &0< A`]
1650 THEN STRIP_TAC;
1651 SUBGOAL_THEN`x'' IN aff_gt {vec 0} {u, w} INTER aff {vec 0, y, z:real^3}` ASSUME_TAC;
1652 ASM_REWRITE_TAC[INTER;IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
1653 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1654 THEN ASM_REWRITE_TAC[];
1655 MRESAL_TAC(GEN_ALL AFF_GT_INTER_AFF_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i:num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`w:real^3`;`y:real^3`;`z:real^3`;`l:real^(M,3)finite_product`][B_SY1;IN_ELIM_THM;CONDITION2_SY]
1656 THEN POP_ASSUM MP_TAC
1657 THEN POP_ASSUM MP_TAC
1658 THEN ASM_REWRITE_TAC[]
1659 THEN SET_TAC[];
1660 REMOVE_THEN "YEU1"(fun th-> MRESA1_TAC th`x'':real^3`)
1661 THEN POP_ASSUM MP_TAC
1662 THEN REWRITE_TAC[REAL_ARITH`&0<= A<=> A= &0 \/ &0< A`]
1663 THEN STRIP_TAC;
1664 SUBGOAL_THEN`x'' IN aff_gt {vec 0} {u, w} INTER aff {vec 0, y1, y:real^3}` ASSUME_TAC;
1665 MRESA_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`y1:real^3`;`y:real^3`]
1666 THEN POP_ASSUM MP_TAC
1667 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1668 THEN RESA_TAC
1669 THEN ASM_REWRITE_TAC[INTER;IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]
1670 THEN ONCE_REWRITE_TAC[CROSS_TRIPLE]
1671 THEN ASM_REWRITE_TAC[];
1672 POP_ASSUM MP_TAC
1673 THEN MRESA_TAC(GEN_ALL Lvducxu.AZIM_CY_FST_Y_IN_FF)[`x':real^3#real^3`;`F_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`vec 0:real^3`;`x:real^3#real^3`]
1674 THEN REMOVE_ASSUM_TAC
1675 THEN POP_ASSUM MP_TAC
1676 THEN REWRITE_TAC[F_SY;IN_ELIM_THM;PAIR_EQ]
1677 THEN STRIP_TAC
1678 THEN MRESAL_TAC(GEN_ALL AFF_GT_INTER_AFF_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`i':num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`w:real^3`;`y1:real^3`;`y:real^3`;`l:real^(M,3)finite_product`][B_SY1;IN_ELIM_THM;CONDITION2_SY]
1679 THEN SET_TAC[]]);;
1680
1681
1682 let TECOXBM2= prove(`!l:real^(M,3)finite_product. stable_system k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\ k= dimindex(:M)/\ 2<k/\
1683 {u,w} SUBSET V_SY(vecmats(l))
1684 /\ norm(u-w)<= cstab
1685 /\ &2<= norm(u-w)
1686 /\ ~({u,w} IN E_SY(vecmats l))
1687 /\l IN B_SY1 a b
1688 ==> ~(collinear ({vec 0} UNION {u,w}))`,
1689 REPEAT STRIP_TAC
1690 THEN POP_ASSUM MP_TAC
1691 THEN POP_ASSUM( fun th-> ASSUME_TAC th THEN MP_TAC th THEN REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY] THEN STRIP_TAC)
1692 THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v:real^3^M`
1693 THEN POP_ASSUM MP_TAC 
1694 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1695 THEN POP_ASSUM MP_TAC
1696 THEN POP_ASSUM MP_TAC
1697 THEN POP_ASSUM MP_TAC
1698 THEN DISCH_THEN(LABEL_TAC"THY")
1699 THEN STRIP_TAC
1700 THEN STRIP_TAC
1701 THEN POP_ASSUM(fun th-> MP_TAC th
1702 THEN REWRITE_TAC[convex_local_fan]
1703 THEN STRIP_TAC
1704 THEN POP_ASSUM MP_TAC
1705 THEN POP_ASSUM(fun th1-> MP_TAC th1
1706 THEN REWRITE_TAC[local_fan]
1707 THEN LET_TAC
1708 THEN STRIP_TAC
1709 THEN POP_ASSUM MP_TAC
1710 THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
1711 THEN STRIP_TAC
1712 THEN ASSUME_TAC th1)
1713 THEN DISCH_THEN(LABEL_TAC"THY1")
1714 THEN ASSUME_TAC th)
1715 THEN STRIP_TAC
1716 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
1717 THEN MATCH_MP_TAC NONPARALLEL_BALL_ANNULUS
1718 THEN ASM_REWRITE_TAC[]
1719 THEN MP_TAC(SET_RULE`{u, w} SUBSET V_SY (vecmats l)
1720 ==> u IN V_SY(vecmats l) /\ w IN V_SY(vecmats (l:real^(M,3)finite_product))`)
1721 THEN ASM_REWRITE_TAC[]
1722 THEN REWRITE_TAC[V_SY;rows;IN_ELIM_THM]
1723 THEN STRIP_TAC
1724 THEN REMOVE_THEN"THY" (fun th-> MRESA1_TAC th`i:num` THEN  MRESA1_TAC th`i':num` ));;
1725
1726 let TECOXBM=prove(`!l:real^(M,3)finite_product. stable_system k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\ k= dimindex(:M)/\ 2<k/\
1727 {u,w} SUBSET V_SY(vecmats(l))
1728 /\ norm(u-w)<= cstab
1729 /\ &2<= norm(u-w)
1730 /\ ~({u,w} IN E_SY(vecmats l))
1731 /\l IN B_SY1 a b
1732 ==> ~(collinear ({vec 0} UNION {u,w}))
1733 /\ (!x. x IN F_SY(vecmats l)==> aff_gt {vec 0}{u,w} SUBSET wedge_in_fan_gt x (E_SY (vecmats l)))`,
1734 GEN_TAC
1735 THEN STRIP_TAC
1736 THEN STRIP_TAC
1737 THENL[MRESA_TAC (GEN_ALL TECOXBM2)[`d:real`;`J:(num->bool)->bool`;`k:num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`w:real^3`;`l:real^(M,3)finite_product`];
1738 MRESA_TAC (GEN_ALL TECOXBM1)[`d:real`;`J:(num->bool)->bool`;`k:num`;`a:num#num->real`;`b:num#num->real`;`u:real^3`;`w:real^3`;`l:real^(M,3)finite_product`]]);;
1739
1740
1741 end;;
1742