text_formalization/local/HDPLYGY.hl

   1
   2 (* ========================================================================== *)
   3 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   4 (*                                                                            *)
   5 (* Chapter: Local Fan                                              *)
   6 (* Author: Hoang Le Truong                                        *)
   7 (* Date: 2012-04-01                                                           *)
   8 (* ========================================================================= *)
   9
  10
  11
  12
  13 module   Hdplygy = struct
  14
  15
  16
  17
  18 open Wjscpro;;
  19 open Polyhedron;;
  20 open Sphere;;
  21 open Fan_defs;;
  22 open Hypermap;;
  23 open Vol1;;
  24 open Fan;;
  25 open Topology;;
  26 open Fan_misc;;
  27 open Planarity;;
  28 open Conforming;;
  29 open Sphere;;
  30 open Hypermap;;
  31 open Fan;;
  32 open Topology;;
  33 open Prove_by_refinement;;
  34 open Pack_defs;;
  35 open Wrgcvdr_cizmrrh;;
  36 open Local_lemmas;;
  37 open Collect_geom;;
  38 open Dih2k_hypermap;;
  39 open Tecoxbm;;
  40
  41 let a_ear0=new_definition`a_ear0 J (i,j)=( if i  MOD 3=j MOD 3 then &0 else
  42  (if {i  MOD 3,j MOD 3} IN J then sqrt(&8) else &2)) `;;
  43
  44 let b_ear0=new_definition`b_ear0 J (i,j)=( if i  MOD 3=j MOD 3 then &0 else
  45  (if {i  MOD 3,j MOD 3} IN J then cstab else &2* h0)) `;;
  46
  47
  48 let MOD_EQ_MOD1=prove(`!x1 x2 y n. ~(n=0) /\ (y + x1) MOD n = (y + x2) MOD n /\ x2<= x1
  49  ==> x1 MOD n = x2 MOD n`,
  50 REPEAT STRIP_TAC
  51 THEN MRESA_TAC DIVISION[`y+x1:num`;`n:num`]
  52 THEN MRESA_TAC DIVISION[`y+x2:num`;`n:num`]
  53 THEN MP_TAC(ARITH_RULE`y + x2 = (y + x2) DIV n * n + (y + x2) MOD n
  54 /\ y + x1 = (y + x1) DIV n * n + (y + x2) MOD n
  55 ==> x1- x2= (y + x1) DIV n *n- (y + x2) DIV n * n `)
  56 THEN POP_ASSUM( fun th-> GEN_REWRITE_TAC(  LAND_CONV o LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
  57 THEN REWRITE_TAC[]
  58 THEN REMOVE_ASSUM_TAC
  59 THEN POP_ASSUM( fun th-> GEN_REWRITE_TAC( LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
  60 THEN REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB]
  61 THEN STRIP_TAC
  62 THEN MRESA_TAC MOD_MULT[`n:num`;`(y + x1) DIV n - (y + x2) DIV n`]
  63 THEN POP_ASSUM MP_TAC
  64 THEN ONCE_REWRITE_TAC[ARITH_RULE`n * ((y + x1) DIV n - (y + x2) DIV n) = ((y + x1) DIV n - (y + x2) DIV n) *n`]
  65 THEN STRIP_TAC
  66 THEN MP_TAC(ARITH_RULE`x2<= x1 ==> x1= x2 + (x1- x2):num`)
  67 THEN RESA_TAC
  68 THEN MRESAL_TAC MOD_ADD_MOD[`x2:num`;`x1-x2:num`;`n:num`][ARITH_RULE` A+0=A/\ (A+B)+C=A+B+C`]
  69 THEN POP_ASSUM MP_TAC
  70 THEN POP_ASSUM(fun th-> GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SYM th])
  71 THEN MRESAL_TAC MOD_MOD_REFL[`x2:num`;`n:num`][ARITH_RULE`3*1=3/\ ~(3=0)`]
  72 THEN RESA_TAC);;
  73
  74
  75
  76 let MOD_EQ_MOD=prove(`!x1 x2 y n. ~(n=0) /\ (y + x1) MOD n = (y + x2) MOD n
  77  ==> x1 MOD n = x2 MOD n`,
  78 REPEAT STRIP_TAC
  79 THEN DISJ_CASES_TAC(ARITH_RULE`x2<= x1 \/ x1<= x2:num`)
  80 THENL[MRESA_TAC MOD_EQ_MOD1[`x1:num`;`x2:num`;`y:num`;`n:num`];
  81 MRESA_TAC MOD_EQ_MOD1[`x2:num`;`x1:num`;`y:num`;`n:num`]]);;
  82
  83
  84 let EAR_STABLE_SYSTEM=prove_by_refinement(`stable_system 3 ((#0.11)) (0..2) (a_ear0 {{1,2}}) (b_ear0 {{1,2}})  ({{1,2}}) (\i. (1 + i) MOD 3)`,
  85 [
  86 MRESAL_TAC HAS_SIZE_NUMSEG[`0`;`2`][ARITH_RULE`(2+1)-0=3`]
  87 THEN ASM_SIMP_TAC[stable_system;constraint_system;torsor;ARITH_RULE`3<= 3 /\3<=6/\ 1+3<=6/\ (2+1)-0=3`;CARD_NUMSEG;Hypermap.CARD_SINGLETON;]
  88 THEN REMOVE_ASSUM_TAC
  89 THEN STRIP_TAC;
  90
  91 STRIP_TAC;
  92
  93 STRIP_TAC;
  94
  95 REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
  96 THEN MRESAL1_TAC Hypermap.LE_MOD_SUC`2`[ARITH_RULE`SUC 2=3`];
  97
  98 STRIP_TAC;
  99
 100 REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
 101 THEN REPEAT STRIP_TAC
 102 THEN MRESAL_TAC (GEN_ALL MOD_IMP_EQ)[`3`;`1+x1`;`1+x2`][ARITH_RULE`1<= 1+A /\ (1+A<=3<=> A<=2)`]
 103 THEN POP_ASSUM MP_TAC
 104 THEN ARITH_TAC;
 105
 106 STRIP_TAC;
 107
 108 REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
 109 THEN REPEAT STRIP_TAC
 110 THEN POP_ASSUM MP_TAC
 111 THEN MP_TAC(ARITH_RULE`0<i==> 1<= i /\ 1<3`)
 112 THEN RESA_TAC
 113 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`3:num`;`x:num`;`i:num`]
 114 THEN MP_TAC(ARITH_RULE`0<i /\ i< 3==> i=1 \/ i=2`)
 115 THEN RESA_TAC
 116 THEN MP_TAC(ARITH_RULE`x<= 2==> x=0 \/ x=1 \/ x=2`)
 117 THEN ASM_REWRITE_TAC[]
 118 THEN RESA_TAC
 119 THEN ARITH_TAC;
 120
 121 REWRITE_TAC[ARITH_RULE`3-1=2`;IN_NUMSEG;ARITH_RULE`0<= A`]
 122 THEN REPEAT STRIP_TAC
 123 THEN ASSUME_TAC(ARITH_RULE`1<=3 /\1<3/\ 1<=2`)
 124 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`3:num`;`x:num`;`3:num`]
 125 THEN MRESAL_TAC MOD_MULT_ADD[`1`;`3`;`x:num`][ARITH_RULE`1*3=3`]
 126 THEN MP_TAC(ARITH_RULE`x<= 2==> x=0 \/ x=1 \/ x=2`)
 127 THEN ASM_REWRITE_TAC[]
 128 THEN RESA_TAC
 129 THEN ARITH_TAC;
 130
 131 STRIP_TAC;
 132
 133 REWRITE_TAC[b_ear0;a_ear0]
 134 THEN REPEAT GEN_TAC
 135 THEN DISJ_CASES_TAC(SET_RULE`i MOD 3 =j MOD 3 \/ ~(i  MOD 3 =j MOD 3:num)`);
 136
 137 ASM_REWRITE_TAC[REAL_ARITH`&0<= &0`];
 138
 139 ASM_REWRITE_TAC[]
 140 THEN  DISJ_CASES_TAC(SET_RULE`{i MOD 3,j MOD 3} IN {{1,2}} \/ ~({i MOD 3,j MOD 3} IN {{1,2}})`);
 141
 142 ASM_REWRITE_TAC[IN_SING]
 143 THEN ONCE_REWRITE_TAC[SET_RULE`{i  MOD 3,j MOD 3} ={1,2} <=> {j MOD 3,i  MOD 3}= {1,2}`]
 144 THEN POP_ASSUM MP_TAC
 145 THEN ASM_REWRITE_TAC[IN_SING;cstab]
 146 THEN RESA_TAC
 147 THEN MATCH_MP_TAC REAL_LE_LSQRT
 148 THEN REAL_ARITH_TAC;
 149
 150 ASM_REWRITE_TAC[IN_SING]
 151 THEN ONCE_REWRITE_TAC[SET_RULE`{i MOD 3,j MOD 3} ={1,2} <=> {j MOD 3,i MOD 3}= {1,2}`]
 152 THEN POP_ASSUM MP_TAC
 153 THEN ASM_REWRITE_TAC[IN_SING;h0]
 154 THEN RESA_TAC
 155 THEN REAL_ARITH_TAC;
 156
 157 STRIP_TAC;
 158
 159 REPEAT GEN_TAC
 160 THEN MP_TAC(ARITH_RULE`1<= 3 /\ 1<3`)
 161 THEN RESA_TAC
 162 THEN MRESAL_TAC MOD_MULT_ADD[`1`;`3`;`j:num`][ARITH_RULE`1*3=3`]
 163 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`3:num`;`j:num`;`3:num`]
 164 THEN SIMP_TAC[b_ear0;a_ear0;ARITH_RULE`A+0=A`;MOD_MOD_REFL;ARITH_RULE`~(3=0)`];
 165
 166 REWRITE_TAC[SUBSET;IN_SING;IN_ELIM_THM;IN_NUMSEG]
 167 THEN REPEAT STRIP_TAC
 168 THEN EXISTS_TAC`1`
 169 THEN ASM_REWRITE_TAC[ARITH_RULE`0<=1 /\ 1<=2/\ (1 +1 ) MOD 3= 2`];
 170 STRIP_TAC;
 171 REWRITE_TAC[a_ear0;IN_NUMSEG]
 172 THEN REPEAT STRIP_TAC
 173 THEN MP_TAC(ARITH_RULE`i<= 2/\ j<= 2==> i< 3 /\ j< 3`)
 174 THEN RESA_TAC
 175 THEN MRESA_TAC MOD_LT[`i:num`;`3`]
 176 THEN MRESA_TAC MOD_LT[`j:num`;`3`]
 177 THEN  DISJ_CASES_TAC(SET_RULE`{i,j} IN {{1,2}} \/ ~({i,j} IN {{1,2}})`);
 178 ASM_REWRITE_TAC[]
 179 THEN MATCH_MP_TAC REAL_LE_RSQRT
 180 THEN REAL_ARITH_TAC;
 181 ASM_REWRITE_TAC[]
 182 THEN REAL_ARITH_TAC;
 183 STRIP_TAC;
 184 REWRITE_TAC[b_ear0;a_ear0;MOD_MOD_REFL]
 185 THEN REPEAT STRIP_TAC
 186 THEN DISJ_CASES_TAC(SET_RULE`i MOD 3 =(1+i) MOD 3 MOD 3\/ ~(i  MOD 3 =(1+i) MOD 3 MOD 3:num)`);
 187 ASM_REWRITE_TAC[REAL_ARITH`&0<= &0`;cstab]
 188 THEN REAL_ARITH_TAC;
 189 ASM_REWRITE_TAC[]
 190 THEN  DISJ_CASES_TAC(SET_RULE`{i MOD 3,(1+i) MOD 3 MOD 3} IN {{1,2}} \/ ~({i MOD 3,(1+i) MOD 3 MOD 3} IN {{1,2}})`);
 191 ASM_REWRITE_TAC[]
 192 THEN REAL_ARITH_TAC;
 193 ASM_REWRITE_TAC[h0;cstab]
 194 THEN REAL_ARITH_TAC;
 195 REWRITE_TAC[IN_SING;a_ear0;b_ear0]
 196 THEN REPEAT STRIP_TAC
 197 THEN MP_TAC(SET_RULE`{i,j}={1,2} /\ ~(1=2) ==> ~(i=j) /\ (i =1\/ i=2) /\ (j=1\/ j=2)`)
 198 THEN ASM_REWRITE_TAC[ARITH_RULE`~(1=2)`]
 199 THEN DISCH_TAC
 200 THEN MP_TAC(ARITH_RULE`(i =1\/ i=2) /\ (j=1\/ j=2)==> i< 3 /\ j< 3`)
 201 THEN RESA_TAC
 202 THEN MRESA_TAC MOD_LT[`i:num`;`3`]
 203 THEN MRESA_TAC MOD_LT[`j:num`;`3`]]);;
 204
 205
 206
 207
 208
 209
 210
 211
 212
 213
 214
 215 let exist_stable_system=prove_by_refinement(`?s:(num#real#(num->bool)#(num#num->real)#(num#num->real)#((num->bool)->bool)#(num->num)). stable_system (FST s) (FST (SND s)) (FST (SND (SND s))) (FST (SND (SND (SND s)))) (FST(SND (SND (SND (SND s))))) (FST (SND (SND (SND (SND (SND s))))))
 216 (SND(SND (SND (SND (SND (SND s))))))`,
 217 [EXISTS_TAC`3, (#0.11), (0..2), (a_ear0 {{1,2}}), (b_ear0 {{1,2}}), ({{1,2}}),(\i. (1 + i) MOD 3)`
 218 THEN REWRITE_TAC[EAR_STABLE_SYSTEM]]);;
 219
 220
 221 let stable_sy_tybij = (new_type_definition "stable_sy" ("stable_sy", "tuple_stable_sy")exist_stable_system);;
 222
 223
 224 let k_sy = new_definition `k_sy (s:stable_sy) = FST (tuple_stable_sy s)`;;
 225
 226 let d_sy = new_definition `d_sy (s:stable_sy) = (FST (SND (tuple_stable_sy s)))`;;
 227
 228 let I_SY = new_definition `I_SY (s:stable_sy) = (FST (SND (SND  (tuple_stable_sy s))))`;;
 229
 230 let a_sy = new_definition `a_sy (s:stable_sy) = (FST (SND (SND (SND (tuple_stable_sy s)))))`;;
 231
 232 let b_sy = new_definition `b_sy (s:stable_sy) = (FST(SND (SND (SND (SND (tuple_stable_sy s)))))) `;;
 233
 234
 235 let J_SY = new_definition `J_SY (s:stable_sy) = (FST (SND (SND (SND (SND (SND  (tuple_stable_sy s))))))) `;;
 236
 237 let f_sy = new_definition `f_sy (s:stable_sy) = (SND(SND (SND (SND (SND (SND  (tuple_stable_sy s)))))))`;;
 238
 239
 240
 241 let stable_sy_lemma=prove(`!s:stable_sy. stable_system (k_sy s) (d_sy s) (I_SY s) (a_sy s) (b_sy s) (J_SY s) (f_sy s)`,
 242    ASM_REWRITE_TAC[stable_sy_tybij;k_sy;d_sy;I_SY; a_sy; b_sy; J_SY; f_sy]);;
 243
 244
 245 let ear_sy=new_definition `ear_sy (s:stable_sy)<=> CARD(I_SY s)=3 /\ d_sy s= #0.11 /\ CARD (J_SY s)= 1 /\ a_sy (s)= a_ear0 (J_SY s)
 246 /\  b_sy (s)= b_ear0 (J_SY s) `;;
 247
 248
 249 let sigma_sy=new_definition `sigma_sy (s:stable_sy) = (if ear_sy s then &1 else -- &1) `;;
 250
 251 let J1_SY=new_definition `J1_SY (s:stable_sy)= {x| ?i. {i MOD (k_sy s),f_sy s (i MOD (k_sy s))} IN J_SY s /\ i IN 1..(k_sy s) /\ x=i,SUC(i MOD (k_sy s))}`;;
 252
 253 let d_fun=new_definition `d_fun (s:stable_sy,l:real^(M,3)finite_product) = (d_sy s) + #0.1 * sigma_sy s * sum (J1_SY s) (\x. cstab -norm (row (FST x) (vecmats l) - row (SND x) (vecmats l) ))`;;
 254
 255 let tau_star=new_definition `tau_star (s:stable_sy) (l:real^(M,3)finite_product)= tau_fun (V_SY (vecmats l)) (E_SY (vecmats l)) (F_SY (vecmats l)) - d_fun (s,l)`;;
 256
 257
 258 let FINITE_J_SY=prove(`!s:stable_sy .
 259 FINITE (J_SY s)`,
 260 GEN_TAC
 261 THEN MRESAL1_TAC stable_sy_lemma`s:stable_sy`[stable_system;IN_NUMSEG;ARITH_RULE`0<= i:num`;]
 262 THEN REMOVE_ASSUM_TAC
 263 THEN REMOVE_ASSUM_TAC
 264 THEN REMOVE_ASSUM_TAC
 265 THEN POP_ASSUM MP_TAC
 266 THEN REWRITE_TAC[constraint_system;torsor;HAS_SIZE]
 267 THEN STRIP_TAC
 268 THEN REMOVE_ASSUM_TAC
 269 THEN MRESA_TAC FINITE_SUBSET[`J_SY (s:stable_sy)`;`{{i, f_sy s i} | i | i IN I_SY (s:stable_sy)}`]
 270 THEN POP_ASSUM MATCH_MP_TAC
 271 THEN MRESAL_TAC FINITE_IMAGE[`(\i. {i, f_sy (s:stable_sy) i})`;`I_SY (s:stable_sy)`][FINITE_NUMSEG;IMAGE]
 272 THEN SUBGOAL_THEN`{y | ?x. x IN I_SY s /\ y = {x,f_sy s x}}={{i, f_sy s i} | i | i IN I_SY (s:stable_sy)}`ASSUME_TAC
 273 THENL[REWRITE_TAC[EXTENSION;IN_ELIM_THM];
 274 POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th])]);;
 275
 276
 277 let FINITE_J1_SY=prove(`!s:stable_sy .
 278 FINITE (J1_SY s)`,
 279 GEN_TAC
 280 THEN REWRITE_TAC[J1_SY]
 281 THEN MRESAL_TAC FINITE_IMAGE[`(\i. i, SUC(i MOD (k_sy s)))`;`1..k_sy (s:stable_sy)`][FINITE_NUMSEG;IMAGE]
 282 THEN MATCH_MP_TAC FINITE_SUBSET
 283 THEN EXISTS_TAC`{y | ?x. x IN 1..(k_sy (s:stable_sy)) /\ y = x,SUC(x MOD (k_sy s))}`
 284 THEN ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM]
 285 THEN REPEAT RESA_TAC
 286 THEN EXISTS_TAC`i:num`
 287 THEN ASM_REWRITE_TAC[]);;
 288
 289 let CONTINUOUS_ON_ROW=prove(`!i s:real^(M,N)finite_product->bool. 1<= i/\ i<= dimindex(:M) ==>  (\x. row i (vecmats x)) continuous_on s`,
 290 REWRITE_TAC[continuous_on;]
 291 THEN REPEAT STRIP_TAC
 292 THEN EXISTS_TAC`e:real`
 293 THEN REPEAT RESA_TAC
 294 THEN POP_ASSUM MP_TAC
 295 THEN MP_TAC(ARITH_RULE`1<= i/\ i<= dimindex(:M) ==> i-1< dimindex(:M)`)
 296 THEN RESA_TAC
 297 THEN MRESAL_TAC (GEN_ALL VECMAT_ROW)[`i-1:num`;`vecmats(x':real^(M,N)finite_product)`][MATVEC_VECMATS_ID]
 298 THEN MRESAL_TAC (GEN_ALL VECMAT_ROW)[`i-1:num`;`vecmats(x:real^(M,N)finite_product)`][MATVEC_VECMATS_ID]
 299 THEN MRESA_TAC (GEN_ALL DIST_VECMAT)[`i-1:num`;`x':real^(M,N)finite_product`;`x:real^(M,N)finite_product`]
 300 THEN MP_TAC(ARITH_RULE`1<= i/\ i<= dimindex(:M) ==> i= SUC(i-1)`)
 301 THEN ASM_REWRITE_TAC[]
 302 THEN STRIP_TAC
 303 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
 304 THEN POP_ASSUM MP_TAC
 305 THEN REAL_ARITH_TAC);;
 306
 307
 308 let INDEX_J1_SY=prove(`!s:stable_sy .
 309 x IN J1_SY s ==> 1 <= FST x /\ FST x <= k_sy s`,
 310 REWRITE_TAC[J1_SY;IN_ELIM_THM;IN_NUMSEG]
 311 THEN REPEAT STRIP_TAC
 312 THEN ASM_REWRITE_TAC[]);;
 313
 314
 315
 316 let CONTINUOUS_ON_D_FUN=prove(`!s:stable_sy .
 317 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k))
 318 ==> lift o(\l:real^(M,3)finite_product. d_fun(s,l)) continuous_on (B_SY1 (a_sy s) (b_sy s))`,
 319 REPEAT STRIP_TAC
 320 THEN REWRITE_TAC[d_fun;LIFT_ADD;o_DEF;]
 321 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
 322 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;]
 323 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
 324 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
 325 THEN ASSUME_TAC FINITE_J1_SY
 326 THEN POP_ASSUM(fun th -> MRESA1_TAC th`s:stable_sy`)
 327 THEN ASM_SIMP_TAC[LIFT_SUM;o_DEF]
 328 THEN MATCH_MP_TAC CONTINUOUS_ON_VSUM
 329 THEN ASM_REWRITE_TAC[]
 330 THEN REPEAT STRIP_TAC
 331 THEN REWRITE_TAC[LIFT_SUB]
 332 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
 333 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;]
 334 THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE
 335 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
 336 THEN STRIP_TAC
 337 THENL[
 338 MATCH_MP_TAC CONTINUOUS_ON_ROW
 339 THEN POP_ASSUM MP_TAC
 340 THEN REWRITE_TAC[J1_SY;IN_ELIM_THM;IN_NUMSEG]
 341 THEN REPEAT RESA_TAC;
 342 MATCH_MP_TAC CONTINUOUS_ON_ROW
 343 THEN POP_ASSUM MP_TAC
 344 THEN REWRITE_TAC[J1_SY;IN_ELIM_THM;IN_NUMSEG]
 345 THEN REPEAT RESA_TAC
 346 THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
 347 THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
 348 THEN POP_ASSUM MP_TAC
 349 THEN ARITH_TAC]);;
 350
 351 let INJ_B_SY=prove(`!s:stable_sy x:real^(M,3)finite_product. x IN (B_SY1 (a_sy s) (b_sy s)) /\ k_sy s =k /\ dimindex(:M) =k /\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
 352 ==>
 353 (!i j.
 354      i IN 1..k /\
 355      j IN 1..k /\
 356      row i (vecmats x),row (SUC (i MOD k)) (vecmats x) =
 357      row j (vecmats x),row (SUC (j MOD k)) (vecmats x)
 358      ==> i = j)`,
 359 REWRITE_TAC[PAIR_EQ;IN_NUMSEG]
 360 THEN REPEAT STRIP_TAC
 361 THEN MRESA1_TAC stable_sy_lemma`s:stable_sy`
 362 THEN MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d_sy (s:stable_sy)`;`J_SY (s:stable_sy)`;`k_sy (s:stable_sy)`;`i:num`;`j:num`;`a_sy (s:stable_sy)`;`b_sy (s:stable_sy)`;`row i (vecmats (x:real^(M,3)finite_product))`;`row j (vecmats (x:real^(M,3)finite_product))`;`x:real^(M,3)finite_product`]
 363 THEN POP_ASSUM MP_TAC
 364 THEN DISJ_CASES_TAC(SET_RULE`~(i=j) \/ i=j:num`)
 365 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0]
 366 THEN REAL_ARITH_TAC);;
 367
 368 let INJ_ROW_B_SY=prove(`!s:stable_sy x:real^(M,3)finite_product. x IN (B_SY1 (a_sy s) (b_sy s)) /\ k_sy s =k /\ dimindex(:M) =k /\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
 369 ==>
 370 (!i j.
 371      i IN 1..k /\
 372      j IN 1..k /\
 373      row i (vecmats x) =
 374      row j (vecmats x)
 375      ==> i = j)`,
 376 REWRITE_TAC[PAIR_EQ;IN_NUMSEG]
 377 THEN REPEAT STRIP_TAC
 378 THEN MRESA1_TAC stable_sy_lemma`s:stable_sy`
 379 THEN MRESA_TAC (GEN_ALL PROPERTIES_OF_FAN_IN_B_SY)[`d_sy (s:stable_sy)`;`J_SY (s:stable_sy)`;`k_sy (s:stable_sy)`;`i:num`;`j:num`;`a_sy (s:stable_sy)`;`b_sy (s:stable_sy)`;`row i (vecmats (x:real^(M,3)finite_product))`;`row j (vecmats (x:real^(M,3)finite_product))`;`x:real^(M,3)finite_product`]
 380 THEN POP_ASSUM MP_TAC
 381 THEN DISJ_CASES_TAC(SET_RULE`~(i=j) \/ i=j:num`)
 382 THEN ASM_REWRITE_TAC[VECTOR_ARITH`A-A= vec 0`;NORM_0]
 383 THEN REAL_ARITH_TAC);;
 384
 385
 386
 387 let CHANGE_SUM_TAU_FUN=prove(`!s:stable_sy x:real^(M,3)finite_product.  k_sy s =k /\ dimindex(:M) =k /\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
 388 /\
 389 x IN (B_SY1 (a_sy s) (b_sy s))
 390 ==>
 391 (\x.
 392       sum (F_SY (vecmats x))
 393       (\e. rho_fun (norm (FST e)) * azim_in_fan e (E_SY (vecmats x)))) x
 394 = (\x. sum (1..k_sy s)
 395       (\i. rho_fun (norm (row i (vecmats x))) * azim_in_fan (row i (vecmats x), row (SUC (i MOD (k_sy s))) (vecmats x)) (E_SY (vecmats x)))) x`,
 396  REPEAT STRIP_TAC
 397 THEN POP_ASSUM(fun th-> MP_TAC th THEN REWRITE_TAC[B_SY1;IN_ELIM_THM]
 398 THEN STRIP_TAC
 399 THEN MP_TAC th
 400 THEN RESA_TAC)
 401 THEN SUBGOAL_THEN`{y | ?x1. x1 IN 1..dimindex (:M) /\
 402                    y =
 403                    row x1 (vecmats x),
 404                    row (SUC (x1 MOD dimindex (:M))) (vecmats x)}
 405 ={row i (vecmats x),row (SUC (i MOD dimindex (:M))) (vecmats (x:real^(M,3)finite_product)) | 1 <= i /\
 406                                                                   i <=
 407                                                                   dimindex
 408                                                                   (:M)}`ASSUME_TAC
 409 THENL[
 410 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG];
 411 POP_ASSUM MP_TAC
 412 THEN ASM_REWRITE_TAC[GSYM F_SY]
 413 THEN STRIP_TAC
 414 THEN MRESAL_TAC SUM_IMAGE[`(\i. (row i (vecmats x), row (SUC (i MOD (k_sy s))) (vecmats (x:real^(M,3)finite_product))))`;`(\e. rho_fun (norm (FST e)) * azim_in_fan e (E_SY (vecmats (x:real^(M,3)finite_product))))`;`1..(k_sy (s:stable_sy))`][o_DEF;IMAGE]
 415 THEN POP_ASSUM MATCH_MP_TAC
 416 THEN MATCH_MP_TAC INJ_B_SY
 417 THEN EXISTS_TAC`s:stable_sy`
 418 THEN ASM_REWRITE_TAC[]]);;
 419
 420
 421
 422 let CONTINUOUS_ON_SAME_DOMAIN=prove(`!f g s:real^M->bool. (!x. x IN s==> f x= g x) /\ f continuous_on s ==> g  continuous_on s`,
 423 SIMP_TAC[continuous_on]
 424 THEN REPEAT STRIP_TAC
 425 THEN POP_ASSUM MP_TAC
 426 THEN POP_ASSUM MP_TAC
 427 THEN POP_ASSUM MP_TAC
 428 THEN POP_ASSUM MP_TAC
 429 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
 430 THEN DISCH_THEN(LABEL_TAC"THY")
 431 THEN REPEAT STRIP_TAC
 432 THEN REMOVE_THEN "THY"(fun th-> MRESA1_TAC th`x:real^M`)
 433 THEN POP_ASSUM(fun th-> MRESA1_TAC th`e:real`)
 434 THEN POP_ASSUM MP_TAC
 435 THEN DISCH_THEN(LABEL_TAC"THY")
 436 THEN EXISTS_TAC`d:real`
 437 THEN ASM_REWRITE_TAC[]
 438 THEN REPEAT STRIP_TAC
 439 THEN REMOVE_THEN"THYGIANG"(fun th-> MRESA1_TAC th`x':real^M` THEN MRESA1_TAC th`x:real^M`)
 440 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`x':real^M`));;
 441
 442
 443 let EDGE_IN_F_SY=prove(`!(l:real^(M,3)finite_product). 1<= i /\ i<= dimindex (:M)
 444 /\ u = row i (vecmats l)
 445 /\ v= row (SUC (i MOD dimindex (:M))) (vecmats l)
 446 ==> u,v IN F_SY (vecmats l)`,
 447 REPEAT STRIP_TAC
 448 THEN REWRITE_TAC[F_SY;IN_ELIM_THM]
 449 THEN EXISTS_TAC`i:num`
 450 THEN ASM_REWRITE_TAC[]);;
 451
 452
 453
 454 let JBDNJJB3=prove(`!u:real^3 v:real^3 w:real^3.
 455 ~collinear {vec 0, u, v} /\ ~collinear {vec 0, u, w}
 456 ==>
 457 sin(azim (vec 0) u v w)=inv (sqrt(norm w pow 2 - (inv (norm u) * (u dot w)) pow 2) * norm (u cross v)) *(u cross v) dot w`,
 458 REPEAT STRIP_TAC
 459 THEN MRESA_TAC th3[`((vec 0):real^3)`;` (u:real^3)`;` (v:real^3)`]
 460 THEN MRESA_TAC properties_coordinate[`((vec 0):real^3)`;` (u:real^3)`;` (v:real^3)`]
 461 THEN MRESA_TAC azim[`((vec 0):real^3)`;` (u:real^3)`;` (v:real^3)`;`(w:real^3)`]
 462 THEN POP_ASSUM (fun th->MRESA_TAC th [`e1_fan ((vec 0):real^3) (u:real^3) (v:real^3)`;`e2_fan ((vec 0):real^3) (u:real^3) (v:real^3)`;`e3_fan ((vec 0):real^3) (u:real^3) (v:real^3)`])
 463 THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC
 464 THEN DISCH_THEN (LABEL_TAC"YEU EM")
 465 THEN DISCH_TAC THEN DISCH_TAC
 466 THEN SUBGOAL_THEN`sqrt(norm w pow 2 - (inv (norm u) * (u dot (w:real^3))) pow 2) =r2`ASSUME_TAC
 467 THENL[
 468 MRESA1_TAC NORM_POW_2`w:real^3`
 469 THEN POP_ASSUM MP_TAC
 470 THEN GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[VECTOR_ARITH`a=a- vec 0`]
 471 THEN ASM_REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL;DOT_RMUL;REAL_ARITH`A* &0= &0 /\ &0+ A=A`]
 472 THEN ONCE_REWRITE_TAC[DOT_SYM]
 473 THEN ASM_REWRITE_TAC[REAL_ARITH`A* &0= &0 /\ &0+ A=A`]
 474 THEN FIND_ASSUM MP_TAC`orthonormal (e1_fan (vec 0) u v) (e2_fan (vec 0) u v)
 475       (e3_fan (vec 0) u (v:real^3))`
 476 THEN REWRITE_TAC[orthonormal;]
 477 THEN RESA_TAC
 478 THEN ONCE_REWRITE_TAC[DOT_SYM]
 479 THEN ASM_REWRITE_TAC[REAL_ARITH`A* &0= &0 /\ A+ &0=A/\ &0 +A=A
 480 /\ (r2 * cos (psi + azim (vec 0) u v w)) *
 481  (r2 * cos (psi + azim (vec 0) u v w)) *
 482  &1 +
 483  (r2 * sin (psi + azim (vec 0) u v w)) *
 484  (r2 * sin (psi + azim (vec 0) u v w)) *
 485  &1 +
 486  h2 * h2 * ((u - vec 0) dot (u - vec 0))
 487 = (r2 pow 2) * ( (sin (psi + azim (vec 0) u v w)) pow 2 +(cos (psi + azim (vec 0) u v w)) pow 2 ) +
 488  h2 * h2 * ((u - vec 0) dot (u - vec 0))`;Trigonometry.WPMXVYZ]
 489 THEN MP_TAC(VECTOR_ARITH`w dot u= (w- vec 0) dot (u- vec 0:real^3)`)
 490 THEN ASM_REWRITE_TAC[DOT_LADD;DOT_RADD;DOT_LMUL;DOT_RMUL;REAL_ARITH`A* &0= &0 /\ &0+ A=A`]
 491 THEN ONCE_REWRITE_TAC[DOT_SYM]
 492 THEN ASM_REWRITE_TAC[REAL_ARITH`A* &0= &0 /\ &0+ A=A`]
 493 THEN STRIP_TAC
 494 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN MP_TAC(SYM th) THEN REWRITE_TAC[VECTOR_ARITH`A- vec 0=A`;GSYM NORM_POW_2])
 495 THEN ONCE_REWRITE_TAC[REAL_ARITH`A *B= B*A`]
 496 THEN MP_TAC(ISPECL[`u:real^3`;`(vec 0) :real^3`]imp_norm_not_zero_fan)
 497 THEN REDUCE_VECTOR_TAC
 498 THEN RESA_TAC
 499 THEN MP_TAC(ISPEC`(norm(u:real^3))`REAL_MUL_LINV)
 500 THEN RESA_TAC
 501 THEN STRIP_TAC
 502 THEN MP_TAC(SET_RULE`norm u pow 2 * h2 = u dot w
 503 ==> inv (norm u) * inv (norm u) *(norm u pow 2 * h2) = inv (norm u) *inv (norm u) *(u dot (w:real^3))`)
 504 THEN POP_ASSUM( fun th -> GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
 505 THEN ASM_REWRITE_TAC[REAL_ARITH` inv (norm u) * inv (norm u) * norm u pow 2 * h2 =(inv (norm u) * norm u) pow 2 * h2/\ &1 pow 2 * h2= h2/\ &1 *A=A`]
 506 THEN RESA_TAC
 507 THEN REWRITE_TAC[REAL_ARITH`
 508 (u dot w) * inv (norm u) * inv (norm u) * (u dot w) = (inv (norm u) * (u dot w)) pow 2`]
 509 THEN ONCE_REWRITE_TAC[REAL_ARITH`
 510 norm w pow 2 = r2 pow 2 + (inv (norm u) * (u dot w)) pow 2
 511 <=>  norm w pow 2 - (inv (norm u) * (u dot w)) pow 2= r2 pow 2 `]
 512 THEN STRIP_TAC
 513 THEN ONCE_REWRITE_TAC[REAL_ARITH`A*B=B*A`]
 514 THEN ONCE_REWRITE_TAC[DOT_SYM]
 515 THEN ASM_REWRITE_TAC[]
 516 THEN MATCH_MP_TAC POW_2_SQRT
 517 THEN MATCH_MP_TAC(REAL_ARITH`&0< A==> &0<= A`)
 518 THEN ASM_REWRITE_TAC[];
 519 MRESA_TAC sincos1_of_u_fan[`((vec 0):real^3)`;` (u:real^3)`;` (v:real^3)`;`r1:real`; `psi:real`; `h1:real`]
 520 THEN REMOVE_THEN "YEU EM" MP_TAC
 521 THEN ASM_REWRITE_TAC[COS_ADD;SIN_ADD;]
 522 THEN REDUCE_ARITH_TAC
 523 THEN REDUCE_VECTOR_TAC
 524 THEN STRIP_TAC
 525 THEN MP_TAC(SET_RULE`w =
 526       (r2 * cos (azim (vec 0) u v w)) % e1_fan (vec 0) u v +
 527       (r2 * sin (azim (vec 0) u v w)) % e2_fan (vec 0) u v +
 528       h2 % u ==>
 529 (u cross v) dot w =
 530 (u cross v) dot ((r2 * cos (azim (vec 0) u v w)) % e1_fan (vec 0) u v +
 531       (r2 * sin (azim (vec 0) u v w)) % e2_fan (vec 0) u v +
 532       h2 % u)`)
 533 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
 534 THEN REWRITE_TAC[DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL;DOT_CROSS_SELF; e2_fan;e1_fan;e3_fan;
 535 VECTOR_ARITH`A- vec 0= A`;CROSS_LADD; CROSS_RADD; CROSS_LMUL; CROSS_RMUL;CROSS_REFL;CROSS_RNEG;CROSS_LNEG;]
 536 THEN REDUCE_ARITH_TAC
 537 THEN REWRITE_TAC[NORM_MUL;REAL_INV_MUL;REAL_ABS_INV;REAL_INV_INV;REAL_ABS_NORM;DOT_SQUARE_NORM
 538 ;REAL_ARITH`(r2 * sin (azim (vec 0) u v w)) *
 539  (norm u * inv (norm (u cross v))) *
 540  inv (norm u) *
 541  norm (u cross v) pow 2 =(r2* norm(u cross v)) * sin (azim (vec 0) u v w) *
 542  ( inv (norm u) * norm u)*
 543 ( inv (norm (u cross v))* norm (u cross (v:real^3)))`
 544 ]
 545 THEN MP_TAC(ISPECL[`u:real^3`;`(vec 0) :real^3`]imp_norm_not_zero_fan)
 546 THEN REDUCE_VECTOR_TAC
 547 THEN RESA_TAC
 548 THEN MP_TAC(ISPEC`(norm(u:real^3))`REAL_MUL_LINV)
 549 THEN RESA_TAC
 550 THEN ASSUME_TAC(ISPEC`u:real^3`NORM_POS_LE)
 551 THEN MP_TAC(REAL_ARITH`~(&0 =norm(u:real^3)) /\ &0 <= norm(u:real^3)==> &0 <norm(u:real^3)`)
 552 THEN RESA_TAC
 553 THEN SUBGOAL_THEN`~(u cross v = vec 0)` ASSUME_TAC
 554 THENL[ASM_REWRITE_TAC[CROSS_EQ_0];
 555 MP_TAC(ISPECL[`u cross v :real^3`;`(vec 0) :real^3`]imp_norm_not_zero_fan)
 556 THEN REDUCE_VECTOR_TAC
 557 THEN RESA_TAC
 558 THEN MP_TAC(ISPEC`(norm(u cross v:real^3))`REAL_MUL_LINV)
 559 THEN RESA_TAC
 560 THEN ASSUME_TAC(ISPEC`u cross v:real^3`NORM_POS_LE)
 561 THEN MP_TAC(REAL_ARITH`~(&0 =norm(u cross v:real^3)) /\ &0 <= norm(u cross v:real^3)==> &0 <norm(u cross v:real^3)`)
 562 THEN RESA_TAC
 563 THEN MRESA_TAC REAL_LT_MUL[`r2:real`;`norm(u cross v:real^3)`]
 564 THEN MP_TAC(REAL_ARITH`&0<(r2:real)*norm(u cross v:real^3)==> ~((r2:real)*norm(u cross v:real^3)= &0)`)
 565 THEN REDUCE_VECTOR_TAC
 566 THEN RESA_TAC
 567 THEN MP_TAC(ISPEC`(r2 * norm(u cross v:real^3))`REAL_MUL_LINV)
 568 THEN RESA_TAC
 569 THEN MP_TAC(ISPEC`(r2 * norm(u cross v:real^3))`REAL_LT_INV)
 570 THEN RESA_TAC
 571 THEN REDUCE_ARITH_TAC
 572 THEN STRIP_TAC
 573 THEN MP_TAC(SET_RULE`(u cross v) dot w = (r2 * norm (u cross v)) * sin (azim (vec 0) u v w) ==>
 574 inv (r2 * norm (u cross v))*(r2 * norm (u cross v)) * sin (azim (vec 0) u v w)= inv (r2 * norm (u cross v)) *((u cross v) dot w)`)
 575 THEN POP_ASSUM (fun th->GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[th])
 576 THEN ASM_REWRITE_TAC[REAL_ARITH`inv (r2 * norm (u cross v)) * (r2 * norm (u cross v)) *
 577  sin (azim (vec 0) u v w)=(inv (r2 * norm (u cross v)) * (r2 * norm (u cross v)))*
 578  sin (azim (vec 0) u v w)`]
 579 THEN REDUCE_ARITH_TAC
 580 THEN STRIP_TAC
 581 THEN ASM_REWRITE_TAC[GSYM REAL_INV_MUL]]]);;
 582
 583
 584
 585
 586 let CONTINUOUS_AT_SQRT = prove
 587  (`!a. &0 < drop a ==>  (lift o sqrt o drop) continuous (at a)`,
 588   REPEAT STRIP_TAC THEN REWRITE_TAC[continuous_at; o_THM; DIST_LIFT] THEN
 589   X_GEN_TAC `e:real` THEN DISCH_TAC THEN
 590   EXISTS_TAC `min (drop a) (e * sqrt(drop a))` THEN
 591   ASM_SIMP_TAC[REAL_LT_MIN; SQRT_POS_LT; REAL_LT_MUL; DIST_REAL] THEN
 592   X_GEN_TAC `b:real^1` THEN REWRITE_TAC[GSYM drop] THEN STRIP_TAC THEN
 593   FIRST_ASSUM(ASSUME_TAC o MATCH_MP (REAL_ARITH
 594    `abs(b - a) < a ==> &0 < b`)) THEN
 595   SUBGOAL_THEN
 596    `sqrt(drop b) - sqrt(drop a) =
 597     (drop b - drop a) / (sqrt(drop a) + sqrt(drop b))`
 598   SUBST1_TAC THENL
 599    [MATCH_MP_TAC(REAL_FIELD
 600      `sa pow 2 = a /\ sb pow 2 = b /\ &0 < sa /\ &0 < sb
 601       ==> sb - sa = (b - a) / (sa + sb)`) THEN
 602     ASM_SIMP_TAC[SQRT_POS_LT; SQRT_POW_2; REAL_LT_IMP_LE];
 603     ASM_SIMP_TAC[REAL_ABS_DIV; SQRT_POS_LT; REAL_LT_ADD; REAL_LT_LDIV_EQ;
 604                  REAL_ARITH `&0 < x ==> abs x = x`] THEN
 605     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
 606         REAL_LTE_TRANS)) THEN
 607     ASM_SIMP_TAC[REAL_LE_LMUL_EQ; REAL_LE_ADDR; SQRT_POS_LE;
 608                  REAL_LT_IMP_LE]]);;
 609
 610
 611 let SEQUENTIALLY_DIVH=prove_by_refinement(`!f:num->real^3 g:num->real^3 h:num->real^3.((\n:num. f n) --> a) sequentially /\ ((\n:num. g n) --> b) sequentially /\ ((\n:num. h n) --> c) sequentially /\ ~(collinear {vec 0, a,b:real^3}) /\ ~(collinear {vec 0, a,c}) /\ (!n. ~(collinear {vec 0, f n, g n}) /\ ~(collinear {vec 0, f n, h n}))
 612 ==> ((lift o (\n:num. dihV (vec 0) (f(n)) (g(n)) (h n)))--> lift ( dihV (vec 0) a b c)) sequentially`,
 613 [REPEAT STRIP_TAC
 614 THEN MRESA_TAC Trigonometry2.FOR_LEMMA19[`vec 0:real^3`;`a:real^3`; `b:real^3`;`c:real^3`]
 615 THEN POP_ASSUM MP_TAC
 616 THEN REPEAT LET_TAC
 617 THEN RESA_TAC
 618 THEN ABBREV_TAC`v01n= (\n:num. dist (vec 0:real^3, f n) pow 2)`
 619 THEN ABBREV_TAC`v02n= (\n:num. dist (vec 0:real^3, g n) pow 2)`
 620 THEN ABBREV_TAC`v03n= (\n:num. dist (vec 0:real^3, h n) pow 2)`
 621 THEN ABBREV_TAC`v12n= (\n:num. dist (f n, (g n):real^3) pow 2)`
 622 THEN ABBREV_TAC`v13n= (\n:num. dist (f n, (h n):real^3) pow 2)`
 623 THEN ABBREV_TAC`v23n= (\n:num. dist (g n, (h n):real^3) pow 2)`
 624 THEN SUBGOAL_THEN`(\n. dihV (vec 0) ((f:num->real^3) n) (g n) (h n))
 625 = (\n:num. acs
 626   (delta_x4 (v01n n) (v02n n) (v03n n) (v23n n) (v13n n) (v12n n) /
 627    sqrt (ups_x (v01n n) (v02n n) (v12n n) * ups_x (v01n n) (v03n n) (v13n n)
 628 )
 629 )
 630 )`ASSUME_TAC;
 631 REWRITE_TAC[FUN_EQ_THM]
 632 THEN STRIP_TAC
 633 THEN MRESA_TAC Trigonometry2.FOR_LEMMA19[`vec 0:real^3`;`(f (x:num)):real^3`; `(g (x:num)):real^3`;`(h (x:num)):real^3`]
 634 THEN POP_ASSUM MP_TAC
 635 THEN REPEAT LET_TAC
 636 THEN RESA_TAC
 637 THEN EXPAND_TAC"v01n"
 638 THEN EXPAND_TAC"v02n"
 639 THEN EXPAND_TAC"v03n"
 640 THEN EXPAND_TAC"v12n"
 641 THEN EXPAND_TAC"v23n"
 642 THEN EXPAND_TAC"v13n"
 643 THEN REWRITE_TAC[]
 644 THEN ASM_REWRITE_TAC[];
 645 ASM_REWRITE_TAC[]
 646 THEN MRESAL1_TAC REAL_CONTINUOUS_WITHIN_ACS_STRONG`delta_x4 v01 v02 v03 v23 v13 v12 /
 647    sqrt (ups_x v01 v02 v12 * ups_x v01 v03 v13)`[REAL_CONTINUOUS_CONTINUOUS_WITHINREAL;CONTINUOUS_WITHIN_SEQUENTIALLY]
 648 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`lift o(\n:num.
 649        (delta_x4 (v01n n) (v02n n) (v03n n) (v23n n) (v13n n) (v12n n) /
 650         sqrt
 651         (ups_x (v01n n) (v02n n) (v12n n) * ups_x (v01n n) (v03n n) (v13n n))))`[o_DEF;LIFT_DROP])
 652 THEN POP_ASSUM MATCH_MP_TAC
 653 THEN STRIP_TAC;
 654 REWRITE_TAC[ IN_ELIM_THM;IMAGE]
 655 THEN GEN_TAC
 656 THEN EXISTS_TAC`delta_x4 (v01n n) (v02n n) (v03n n) (v23n n) (v13n n) (v12n n) /
 657       sqrt
 658       (ups_x (v01n n) (v02n n) (v12n n) * ups_x (v01n n) (v03n n) (v13n (n:num)))`
 659 THEN ASM_REWRITE_TAC[]
 660 THEN MRESA_TAC (GEN_ALL Trigonometry2.PROVE_DELTA_OVER_SQRT_2UPS)[`(f (n:num)):real^3`;`(h (n:num)):real^3`;`(g (n:num)):real^3`;`vec 0:real^3`;`(v23n (n:num)):real`;`(v02n (n:num)):real` ;`(v12n (n:num)):real`;`(v01n (n:num)):real`;`(v03n (n:num)):real`;`(v13n (n:num)):real`]
 661 THEN POP_ASSUM MP_TAC
 662 THEN EXPAND_TAC"v01n"
 663 THEN EXPAND_TAC"v02n"
 664 THEN EXPAND_TAC"v03n"
 665 THEN EXPAND_TAC"v12n"
 666 THEN EXPAND_TAC"v23n"
 667 THEN EXPAND_TAC"v13n"
 668 THEN REWRITE_TAC[]
 669 THEN REPEAT LET_TAC
 670 THEN RESA_TAC
 671 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th; NORM_CAUCHY_SCHWARZ_DIV]);
 672 REWRITE_TAC[real_div;LIFT_CMUL]
 673 THEN MATCH_MP_TAC LIM_MUL
 674 THEN STRIP_TAC;
 675 REWRITE_TAC[o_DEF;delta_x4;LIFT_SUB;LIFT_ADD;LIFT_CMUL]
 676 THEN MATCH_MP_TAC LIM_ADD
 677 THEN STRIP_TAC;
 678 MATCH_MP_TAC LIM_SUB
 679 THEN STRIP_TAC;
 680 MATCH_MP_TAC LIM_MUL
 681 THEN REWRITE_TAC[o_DEF]
 682 THEN EXPAND_TAC"v01n"
 683 THEN EXPAND_TAC"v02n"
 684 THEN EXPAND_TAC"v03n"
 685 THEN EXPAND_TAC"v12n"
 686 THEN EXPAND_TAC"v23n"
 687 THEN EXPAND_TAC"v13n"
 688 THEN EXPAND_TAC"v01"
 689 THEN EXPAND_TAC"v02"
 690 THEN EXPAND_TAC"v03"
 691 THEN EXPAND_TAC"v12"
 692 THEN EXPAND_TAC"v23"
 693 THEN EXPAND_TAC"v13"
 694 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
 695 THEN STRIP_TAC;
 696 MATCH_MP_TAC LIM_NEG
 697 THEN MATCH_MP_TAC LIM_MUL
 698 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 699 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`b:real^3`
 700 THEN POP_ASSUM MP_TAC
 701 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 702 THEN STRIP_TAC
 703 THEN POP_ASSUM MATCH_MP_TAC
 704 THEN ASM_REWRITE_TAC[]
 705 THEN ASM_TAC
 706 THEN REWRITE_TAC[ETA_AX]
 707 THEN SET_TAC[];
 708 MATCH_MP_TAC LIM_MUL
 709 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 710 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`c:real^3`
 711 THEN POP_ASSUM MP_TAC
 712 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 713 THEN STRIP_TAC
 714 THEN POP_ASSUM MATCH_MP_TAC
 715 THEN ASM_REWRITE_TAC[]
 716 THEN ASM_TAC
 717 THEN REWRITE_TAC[ETA_AX]
 718 THEN SET_TAC[];
 719 MATCH_MP_TAC LIM_MUL
 720 THEN REWRITE_TAC[o_DEF]
 721 THEN EXPAND_TAC"v01n"
 722 THEN EXPAND_TAC"v02n"
 723 THEN EXPAND_TAC"v03n"
 724 THEN EXPAND_TAC"v12n"
 725 THEN EXPAND_TAC"v23n"
 726 THEN EXPAND_TAC"v13n"
 727 THEN EXPAND_TAC"v01"
 728 THEN EXPAND_TAC"v02"
 729 THEN EXPAND_TAC"v03"
 730 THEN EXPAND_TAC"v12"
 731 THEN EXPAND_TAC"v23"
 732 THEN EXPAND_TAC"v13"
 733 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
 734 THEN STRIP_TAC;
 735 MATCH_MP_TAC LIM_MUL
 736 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 737 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
 738 THEN POP_ASSUM MP_TAC
 739 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 740 THEN STRIP_TAC
 741 THEN POP_ASSUM MATCH_MP_TAC
 742 THEN ASM_REWRITE_TAC[]
 743 THEN ASM_TAC
 744 THEN REWRITE_TAC[ETA_AX]
 745 THEN SET_TAC[];
 746 MATCH_MP_TAC LIM_MUL
 747 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 748 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`b-c:real^3`
 749 THEN POP_ASSUM MP_TAC
 750 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 751 THEN STRIP_TAC
 752 THEN POP_ASSUM MATCH_MP_TAC
 753 THEN ASM_REWRITE_TAC[]
 754 THEN MATCH_MP_TAC LIM_SUB
 755 THEN ASM_TAC
 756 THEN REWRITE_TAC[ETA_AX]
 757 THEN SET_TAC[];
 758 MATCH_MP_TAC LIM_ADD
 759 THEN STRIP_TAC;
 760 MATCH_MP_TAC LIM_MUL
 761 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 762 THEN EXPAND_TAC"v01n"
 763 THEN EXPAND_TAC"v02n"
 764 THEN EXPAND_TAC"v03n"
 765 THEN EXPAND_TAC"v12n"
 766 THEN EXPAND_TAC"v23n"
 767 THEN EXPAND_TAC"v13n"
 768 THEN EXPAND_TAC"v01"
 769 THEN EXPAND_TAC"v02"
 770 THEN EXPAND_TAC"v03"
 771 THEN EXPAND_TAC"v12"
 772 THEN EXPAND_TAC"v23"
 773 THEN EXPAND_TAC"v13"
 774 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
 775 THEN STRIP_TAC;
 776 MATCH_MP_TAC LIM_MUL
 777 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 778 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`b:real^3`
 779 THEN POP_ASSUM MP_TAC
 780 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 781 THEN STRIP_TAC
 782 THEN POP_ASSUM MATCH_MP_TAC
 783 THEN ASM_REWRITE_TAC[]
 784 THEN ASM_TAC
 785 THEN REWRITE_TAC[ETA_AX]
 786 THEN SET_TAC[];
 787 MATCH_MP_TAC LIM_MUL
 788 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 789 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-c:real^3`
 790 THEN POP_ASSUM MP_TAC
 791 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 792 THEN STRIP_TAC
 793 THEN POP_ASSUM MATCH_MP_TAC
 794 THEN ASM_REWRITE_TAC[]
 795 THEN MATCH_MP_TAC LIM_SUB
 796 THEN ASM_TAC
 797 THEN REWRITE_TAC[ETA_AX]
 798 THEN SET_TAC[];
 799 MATCH_MP_TAC LIM_ADD
 800 THEN STRIP_TAC;
 801 MATCH_MP_TAC LIM_SUB
 802 THEN STRIP_TAC;
 803 MATCH_MP_TAC LIM_MUL
 804 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 805 THEN EXPAND_TAC"v01n"
 806 THEN EXPAND_TAC"v02n"
 807 THEN EXPAND_TAC"v03n"
 808 THEN EXPAND_TAC"v12n"
 809 THEN EXPAND_TAC"v23n"
 810 THEN EXPAND_TAC"v13n"
 811 THEN EXPAND_TAC"v01"
 812 THEN EXPAND_TAC"v02"
 813 THEN EXPAND_TAC"v03"
 814 THEN EXPAND_TAC"v12"
 815 THEN EXPAND_TAC"v23"
 816 THEN EXPAND_TAC"v13"
 817 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
 818 THEN STRIP_TAC;
 819 MATCH_MP_TAC LIM_MUL
 820 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 821 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`c:real^3`
 822 THEN POP_ASSUM MP_TAC
 823 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 824 THEN STRIP_TAC
 825 THEN POP_ASSUM MATCH_MP_TAC
 826 THEN ASM_REWRITE_TAC[]
 827 THEN ASM_TAC
 828 THEN REWRITE_TAC[ETA_AX]
 829 THEN SET_TAC[];
 830 MATCH_MP_TAC LIM_MUL
 831 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 832 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-b:real^3`
 833 THEN POP_ASSUM MP_TAC
 834 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 835 THEN STRIP_TAC
 836 THEN POP_ASSUM MATCH_MP_TAC
 837 THEN ASM_REWRITE_TAC[]
 838 THEN MATCH_MP_TAC LIM_SUB
 839 THEN ASM_TAC
 840 THEN REWRITE_TAC[ETA_AX]
 841 THEN SET_TAC[];
 842 MATCH_MP_TAC LIM_MUL
 843 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 844 THEN EXPAND_TAC"v01n"
 845 THEN EXPAND_TAC"v02n"
 846 THEN EXPAND_TAC"v03n"
 847 THEN EXPAND_TAC"v12n"
 848 THEN EXPAND_TAC"v23n"
 849 THEN EXPAND_TAC"v13n"
 850 THEN EXPAND_TAC"v01"
 851 THEN EXPAND_TAC"v02"
 852 THEN EXPAND_TAC"v03"
 853 THEN EXPAND_TAC"v12"
 854 THEN EXPAND_TAC"v23"
 855 THEN EXPAND_TAC"v13"
 856 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
 857 THEN STRIP_TAC;
 858 MATCH_MP_TAC LIM_MUL
 859 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 860 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-c:real^3`
 861 THEN POP_ASSUM MP_TAC
 862 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 863 THEN STRIP_TAC
 864 THEN POP_ASSUM MATCH_MP_TAC
 865 THEN ASM_REWRITE_TAC[]
 866 THEN MATCH_MP_TAC LIM_SUB
 867 THEN ASM_TAC
 868 THEN REWRITE_TAC[ETA_AX]
 869 THEN SET_TAC[];
 870 MATCH_MP_TAC LIM_MUL
 871 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 872 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-b:real^3`
 873 THEN POP_ASSUM MP_TAC
 874 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 875 THEN STRIP_TAC
 876 THEN POP_ASSUM MATCH_MP_TAC
 877 THEN ASM_REWRITE_TAC[]
 878 THEN MATCH_MP_TAC LIM_SUB
 879 THEN ASM_TAC
 880 THEN REWRITE_TAC[ETA_AX]
 881 THEN SET_TAC[];
 882 MATCH_MP_TAC LIM_MUL
 883 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 884 THEN EXPAND_TAC"v01n"
 885 THEN EXPAND_TAC"v02n"
 886 THEN EXPAND_TAC"v03n"
 887 THEN EXPAND_TAC"v12n"
 888 THEN EXPAND_TAC"v23n"
 889 THEN EXPAND_TAC"v13n"
 890 THEN EXPAND_TAC"v01"
 891 THEN EXPAND_TAC"v02"
 892 THEN EXPAND_TAC"v03"
 893 THEN EXPAND_TAC"v12"
 894 THEN EXPAND_TAC"v23"
 895 THEN EXPAND_TAC"v13"
 896 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
 897 THEN STRIP_TAC;
 898 MATCH_MP_TAC LIM_MUL
 899 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 900 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
 901 THEN POP_ASSUM MP_TAC
 902 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 903 THEN STRIP_TAC
 904 THEN POP_ASSUM MATCH_MP_TAC
 905 THEN ASM_REWRITE_TAC[]
 906 THEN ASM_TAC
 907 THEN REWRITE_TAC[ETA_AX]
 908 THEN SET_TAC[];
 909 MATCH_MP_TAC LIM_ADD
 910 THEN STRIP_TAC;
 911 MATCH_MP_TAC LIM_NEG
 912 THEN MATCH_MP_TAC LIM_MUL
 913 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 914 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
 915 THEN POP_ASSUM MP_TAC
 916 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 917 THEN STRIP_TAC
 918 THEN POP_ASSUM MATCH_MP_TAC
 919 THEN ASM_REWRITE_TAC[]
 920 THEN ASM_TAC
 921 THEN REWRITE_TAC[ETA_AX]
 922 THEN SET_TAC[];
 923 MATCH_MP_TAC LIM_ADD
 924 THEN STRIP_TAC;
 925 MATCH_MP_TAC LIM_MUL
 926 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 927 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`b:real^3`
 928 THEN POP_ASSUM MP_TAC
 929 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 930 THEN STRIP_TAC
 931 THEN POP_ASSUM MATCH_MP_TAC
 932 THEN ASM_REWRITE_TAC[]
 933 THEN ASM_TAC
 934 THEN REWRITE_TAC[ETA_AX]
 935 THEN SET_TAC[];
 936 MATCH_MP_TAC LIM_ADD
 937 THEN STRIP_TAC;
 938 MATCH_MP_TAC LIM_SUB
 939 THEN STRIP_TAC;
 940 MATCH_MP_TAC LIM_MUL
 941 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 942 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`c:real^3`
 943 THEN POP_ASSUM MP_TAC
 944 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 945 THEN STRIP_TAC
 946 THEN POP_ASSUM MATCH_MP_TAC
 947 THEN ASM_REWRITE_TAC[]
 948 THEN ASM_TAC
 949 THEN REWRITE_TAC[ETA_AX]
 950 THEN SET_TAC[];
 951 MATCH_MP_TAC LIM_MUL
 952 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 953 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`b-c:real^3`
 954 THEN POP_ASSUM MP_TAC
 955 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 956 THEN STRIP_TAC
 957 THEN POP_ASSUM MATCH_MP_TAC
 958 THEN ASM_REWRITE_TAC[]
 959 THEN MATCH_MP_TAC LIM_SUB
 960 THEN ASM_TAC
 961 THEN REWRITE_TAC[ETA_AX]
 962 THEN SET_TAC[];
 963 MATCH_MP_TAC LIM_ADD
 964 THEN STRIP_TAC;
 965 MATCH_MP_TAC LIM_MUL
 966 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 967 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-c:real^3`
 968 THEN POP_ASSUM MP_TAC
 969 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 970 THEN STRIP_TAC
 971 THEN POP_ASSUM MATCH_MP_TAC
 972 THEN ASM_REWRITE_TAC[]
 973 THEN MATCH_MP_TAC LIM_SUB
 974 THEN ASM_TAC
 975 THEN REWRITE_TAC[ETA_AX]
 976 THEN SET_TAC[];
 977 MATCH_MP_TAC LIM_MUL
 978 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
 979 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-b:real^3`
 980 THEN POP_ASSUM MP_TAC
 981 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
 982 THEN STRIP_TAC
 983 THEN POP_ASSUM MATCH_MP_TAC
 984 THEN ASM_REWRITE_TAC[]
 985 THEN MATCH_MP_TAC LIM_SUB
 986 THEN ASM_TAC
 987 THEN REWRITE_TAC[ETA_AX]
 988 THEN SET_TAC[];
 989 MRESAL_TAC LIM_INV [`sequentially`;`(\x:num.
 990        (sqrt
 991        (ups_x (v01n x) (v02n x) (v12n x) * ups_x (v01n x) (v03n x) (v13n x))))`;`sqrt (ups_x v01 v02 v12 * ups_x v01 v03 v13)`][o_DEF]
 992 THEN POP_ASSUM MATCH_MP_TAC
 993 THEN SUBGOAL_THEN `&0< ups_x v01 v02 v12 * ups_x v01 v03 v13` ASSUME_TAC;
 994 MATCH_MP_TAC REAL_LT_MUL
 995 THEN MRESA_TAC (GEN_ALL Trigonometry2.NOT_COLLINEAR_IMP_UPS_LT)[`b:real^3`;`vec 0 :real^3`;`a:real^3`]
 996 THEN POP_ASSUM MP_TAC
 997 THEN REPEAT LET_TAC
 998 THEN MRESA_TAC (GEN_ALL Trigonometry2.NOT_COLLINEAR_IMP_UPS_LT)[`c:real^3`;`vec 0 :real^3`;`a:real^3`]
 999 THEN POP_ASSUM MP_TAC
1000 THEN REPEAT LET_TAC
1001 THEN REAL_ARITH_TAC;
1002 MRESA1_TAC SQRT_POS_LT`ups_x v01 v02 v12 * ups_x v01 v03 v13`
1003 THEN MP_TAC(REAL_ARITH`
1004 &0< sqrt (ups_x v01 v02 v12 * ups_x v01 v03 v13)
1005 ==> ~(sqrt (ups_x v01 v02 v12 * ups_x v01 v03 v13) = &0)`)
1006 THEN RESA_TAC
1007 THEN MRESAL1_TAC CONTINUOUS_AT_SQRT`lift(ups_x v01 v02 v12 * ups_x v01 v03 (v13:real))`[CONTINUOUS_AT_SEQUENTIALLY;o_DEF;LIFT_DROP]
1008 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`(\x:num. lift
1009        (       (ups_x (v01n x) (v02n x) (v12n x) * ups_x (v01n x) (v03n x) (v13n x))))`[LIFT_DROP])
1010 THEN POP_ASSUM MATCH_MP_TAC
1011 THEN REWRITE_TAC[LIFT_CMUL]
1012 THEN MATCH_MP_TAC LIM_MUL
1013 THEN REWRITE_TAC[ups_x;o_DEF;LIFT_ADD;LIFT_SUB;LIFT_CMUL]
1014 THEN STRIP_TAC;
1015 MATCH_MP_TAC LIM_ADD
1016 THEN STRIP_TAC;
1017 MATCH_MP_TAC LIM_SUB
1018 THEN STRIP_TAC;
1019 MATCH_MP_TAC LIM_SUB
1020 THEN STRIP_TAC;
1021 MATCH_MP_TAC LIM_MUL
1022 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1023 THEN EXPAND_TAC"v01n"
1024 THEN EXPAND_TAC"v02n"
1025 THEN EXPAND_TAC"v03n"
1026 THEN EXPAND_TAC"v12n"
1027 THEN EXPAND_TAC"v23n"
1028 THEN EXPAND_TAC"v13n"
1029 THEN EXPAND_TAC"v01"
1030 THEN EXPAND_TAC"v02"
1031 THEN EXPAND_TAC"v03"
1032 THEN EXPAND_TAC"v12"
1033 THEN EXPAND_TAC"v23"
1034 THEN EXPAND_TAC"v13"
1035 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1036 THEN STRIP_TAC;
1037 MATCH_MP_TAC LIM_NEG
1038 THEN MATCH_MP_TAC LIM_MUL
1039 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1040 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
1041 THEN POP_ASSUM MP_TAC
1042 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1043 THEN STRIP_TAC
1044 THEN POP_ASSUM MATCH_MP_TAC
1045 THEN ASM_REWRITE_TAC[]
1046 THEN ASM_TAC
1047 THEN REWRITE_TAC[ETA_AX]
1048 THEN SET_TAC[];
1049 MATCH_MP_TAC LIM_MUL
1050 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1051 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
1052 THEN POP_ASSUM MP_TAC
1053 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1054 THEN STRIP_TAC
1055 THEN POP_ASSUM MATCH_MP_TAC
1056 THEN ASM_REWRITE_TAC[]
1057 THEN ASM_TAC
1058 THEN REWRITE_TAC[ETA_AX]
1059 THEN SET_TAC[];
1060 MATCH_MP_TAC LIM_MUL
1061 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1062 THEN EXPAND_TAC"v01n"
1063 THEN EXPAND_TAC"v02n"
1064 THEN EXPAND_TAC"v03n"
1065 THEN EXPAND_TAC"v12n"
1066 THEN EXPAND_TAC"v23n"
1067 THEN EXPAND_TAC"v13n"
1068 THEN EXPAND_TAC"v01"
1069 THEN EXPAND_TAC"v02"
1070 THEN EXPAND_TAC"v03"
1071 THEN EXPAND_TAC"v12"
1072 THEN EXPAND_TAC"v23"
1073 THEN EXPAND_TAC"v13"
1074 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1075 THEN MATCH_MP_TAC LIM_MUL
1076 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1077 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`b:real^3`
1078 THEN POP_ASSUM MP_TAC
1079 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1080 THEN STRIP_TAC
1081 THEN POP_ASSUM MATCH_MP_TAC
1082 THEN ASM_REWRITE_TAC[]
1083 THEN ASM_TAC
1084 THEN REWRITE_TAC[ETA_AX]
1085 THEN SET_TAC[];
1086 MATCH_MP_TAC LIM_MUL
1087 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1088 THEN EXPAND_TAC"v01n"
1089 THEN EXPAND_TAC"v02n"
1090 THEN EXPAND_TAC"v03n"
1091 THEN EXPAND_TAC"v12n"
1092 THEN EXPAND_TAC"v23n"
1093 THEN EXPAND_TAC"v13n"
1094 THEN EXPAND_TAC"v01"
1095 THEN EXPAND_TAC"v02"
1096 THEN EXPAND_TAC"v03"
1097 THEN EXPAND_TAC"v12"
1098 THEN EXPAND_TAC"v23"
1099 THEN EXPAND_TAC"v13"
1100 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1101 THEN MATCH_MP_TAC LIM_MUL
1102 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1103 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-b:real^3`
1104 THEN POP_ASSUM MP_TAC
1105 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1106 THEN STRIP_TAC
1107 THEN POP_ASSUM MATCH_MP_TAC
1108 THEN ASM_REWRITE_TAC[]
1109 THEN MATCH_MP_TAC LIM_SUB
1110 THEN ASM_TAC
1111 THEN REWRITE_TAC[ETA_AX]
1112 THEN SET_TAC[];
1113 MATCH_MP_TAC LIM_ADD
1114 THEN STRIP_TAC;
1115 MATCH_MP_TAC LIM_CMUL
1116 THEN MATCH_MP_TAC LIM_MUL
1117 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1118 THEN EXPAND_TAC"v01n"
1119 THEN EXPAND_TAC"v02n"
1120 THEN EXPAND_TAC"v03n"
1121 THEN EXPAND_TAC"v12n"
1122 THEN EXPAND_TAC"v23n"
1123 THEN EXPAND_TAC"v13n"
1124 THEN EXPAND_TAC"v01"
1125 THEN EXPAND_TAC"v02"
1126 THEN EXPAND_TAC"v03"
1127 THEN EXPAND_TAC"v12"
1128 THEN EXPAND_TAC"v23"
1129 THEN EXPAND_TAC"v13"
1130 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1131 THEN STRIP_TAC;
1132 MATCH_MP_TAC LIM_MUL
1133 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1134 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
1135 THEN POP_ASSUM MP_TAC
1136 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1137 THEN STRIP_TAC
1138 THEN POP_ASSUM MATCH_MP_TAC
1139 THEN ASM_REWRITE_TAC[]
1140 THEN ASM_TAC
1141 THEN REWRITE_TAC[ETA_AX]
1142 THEN SET_TAC[];
1143 MATCH_MP_TAC LIM_MUL
1144 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1145 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-b:real^3`
1146 THEN POP_ASSUM MP_TAC
1147 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1148 THEN STRIP_TAC
1149 THEN POP_ASSUM MATCH_MP_TAC
1150 THEN ASM_REWRITE_TAC[]
1151 THEN MATCH_MP_TAC LIM_SUB
1152 THEN ASM_TAC
1153 THEN REWRITE_TAC[ETA_AX]
1154 THEN SET_TAC[];
1155 MATCH_MP_TAC LIM_ADD
1156 THEN STRIP_TAC;
1157 MATCH_MP_TAC LIM_CMUL
1158 THEN MATCH_MP_TAC LIM_MUL
1159 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1160 THEN EXPAND_TAC"v01n"
1161 THEN EXPAND_TAC"v02n"
1162 THEN EXPAND_TAC"v03n"
1163 THEN EXPAND_TAC"v12n"
1164 THEN EXPAND_TAC"v23n"
1165 THEN EXPAND_TAC"v13n"
1166 THEN EXPAND_TAC"v01"
1167 THEN EXPAND_TAC"v02"
1168 THEN EXPAND_TAC"v03"
1169 THEN EXPAND_TAC"v12"
1170 THEN EXPAND_TAC"v23"
1171 THEN EXPAND_TAC"v13"
1172 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1173 THEN STRIP_TAC;
1174 MATCH_MP_TAC LIM_MUL
1175 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1176 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
1177 THEN POP_ASSUM MP_TAC
1178 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1179 THEN STRIP_TAC
1180 THEN POP_ASSUM MATCH_MP_TAC
1181 THEN ASM_REWRITE_TAC[]
1182 THEN ASM_TAC
1183 THEN REWRITE_TAC[ETA_AX]
1184 THEN SET_TAC[];
1185 MATCH_MP_TAC LIM_MUL
1186 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1187 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`b:real^3`
1188 THEN POP_ASSUM MP_TAC
1189 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1190 THEN STRIP_TAC
1191 THEN POP_ASSUM MATCH_MP_TAC
1192 THEN ASM_REWRITE_TAC[]
1193 THEN ASM_TAC
1194 THEN REWRITE_TAC[ETA_AX]
1195 THEN SET_TAC[];
1196 MATCH_MP_TAC LIM_CMUL
1197 THEN MATCH_MP_TAC LIM_MUL
1198 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1199 THEN EXPAND_TAC"v01n"
1200 THEN EXPAND_TAC"v02n"
1201 THEN EXPAND_TAC"v03n"
1202 THEN EXPAND_TAC"v12n"
1203 THEN EXPAND_TAC"v23n"
1204 THEN EXPAND_TAC"v13n"
1205 THEN EXPAND_TAC"v01"
1206 THEN EXPAND_TAC"v02"
1207 THEN EXPAND_TAC"v03"
1208 THEN EXPAND_TAC"v12"
1209 THEN EXPAND_TAC"v23"
1210 THEN EXPAND_TAC"v13"
1211 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1212 THEN STRIP_TAC;
1213 MATCH_MP_TAC LIM_MUL
1214 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1215 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`b:real^3`
1216 THEN POP_ASSUM MP_TAC
1217 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1218 THEN STRIP_TAC
1219 THEN POP_ASSUM MATCH_MP_TAC
1220 THEN ASM_REWRITE_TAC[]
1221 THEN ASM_TAC
1222 THEN REWRITE_TAC[ETA_AX]
1223 THEN SET_TAC[];
1224 MATCH_MP_TAC LIM_MUL
1225 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1226 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-b:real^3`
1227 THEN POP_ASSUM MP_TAC
1228 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1229 THEN STRIP_TAC
1230 THEN POP_ASSUM MATCH_MP_TAC
1231 THEN ASM_REWRITE_TAC[]
1232 THEN MATCH_MP_TAC LIM_SUB
1233 THEN ASM_TAC
1234 THEN REWRITE_TAC[ETA_AX]
1235 THEN SET_TAC[];
1236 MATCH_MP_TAC LIM_ADD
1237 THEN STRIP_TAC;
1238 MATCH_MP_TAC LIM_SUB
1239 THEN STRIP_TAC;
1240 MATCH_MP_TAC LIM_SUB
1241 THEN STRIP_TAC;
1242 MATCH_MP_TAC LIM_MUL
1243 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1244 THEN EXPAND_TAC"v01n"
1245 THEN EXPAND_TAC"v02n"
1246 THEN EXPAND_TAC"v03n"
1247 THEN EXPAND_TAC"v12n"
1248 THEN EXPAND_TAC"v23n"
1249 THEN EXPAND_TAC"v13n"
1250 THEN EXPAND_TAC"v01"
1251 THEN EXPAND_TAC"v02"
1252 THEN EXPAND_TAC"v03"
1253 THEN EXPAND_TAC"v12"
1254 THEN EXPAND_TAC"v23"
1255 THEN EXPAND_TAC"v13"
1256 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1257 THEN STRIP_TAC;
1258 MATCH_MP_TAC LIM_NEG
1259 THEN MATCH_MP_TAC LIM_MUL
1260 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1261 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
1262 THEN POP_ASSUM MP_TAC
1263 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1264 THEN STRIP_TAC
1265 THEN POP_ASSUM MATCH_MP_TAC
1266 THEN ASM_REWRITE_TAC[]
1267 THEN ASM_TAC
1268 THEN REWRITE_TAC[ETA_AX]
1269 THEN SET_TAC[];
1270 MATCH_MP_TAC LIM_MUL
1271 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1272 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
1273 THEN POP_ASSUM MP_TAC
1274 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1275 THEN STRIP_TAC
1276 THEN POP_ASSUM MATCH_MP_TAC
1277 THEN ASM_REWRITE_TAC[]
1278 THEN ASM_TAC
1279 THEN REWRITE_TAC[ETA_AX]
1280 THEN SET_TAC[];
1281 MATCH_MP_TAC LIM_MUL
1282 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1283 THEN EXPAND_TAC"v01n"
1284 THEN EXPAND_TAC"v02n"
1285 THEN EXPAND_TAC"v03n"
1286 THEN EXPAND_TAC"v12n"
1287 THEN EXPAND_TAC"v23n"
1288 THEN EXPAND_TAC"v13n"
1289 THEN EXPAND_TAC"v01"
1290 THEN EXPAND_TAC"v02"
1291 THEN EXPAND_TAC"v03"
1292 THEN EXPAND_TAC"v12"
1293 THEN EXPAND_TAC"v23"
1294 THEN EXPAND_TAC"v13"
1295 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1296 THEN MATCH_MP_TAC LIM_MUL
1297 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1298 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`c:real^3`
1299 THEN POP_ASSUM MP_TAC
1300 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1301 THEN STRIP_TAC
1302 THEN POP_ASSUM MATCH_MP_TAC
1303 THEN ASM_REWRITE_TAC[]
1304 THEN ASM_TAC
1305 THEN REWRITE_TAC[ETA_AX]
1306 THEN SET_TAC[];
1307 MATCH_MP_TAC LIM_MUL
1308 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1309 THEN EXPAND_TAC"v01n"
1310 THEN EXPAND_TAC"v02n"
1311 THEN EXPAND_TAC"v03n"
1312 THEN EXPAND_TAC"v12n"
1313 THEN EXPAND_TAC"v23n"
1314 THEN EXPAND_TAC"v13n"
1315 THEN EXPAND_TAC"v01"
1316 THEN EXPAND_TAC"v02"
1317 THEN EXPAND_TAC"v03"
1318 THEN EXPAND_TAC"v12"
1319 THEN EXPAND_TAC"v23"
1320 THEN EXPAND_TAC"v13"
1321 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1322 THEN MATCH_MP_TAC LIM_MUL
1323 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1324 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-c:real^3`
1325 THEN POP_ASSUM MP_TAC
1326 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1327 THEN STRIP_TAC
1328 THEN POP_ASSUM MATCH_MP_TAC
1329 THEN ASM_REWRITE_TAC[]
1330 THEN MATCH_MP_TAC LIM_SUB
1331 THEN ASM_TAC
1332 THEN REWRITE_TAC[ETA_AX]
1333 THEN SET_TAC[];
1334 MATCH_MP_TAC LIM_ADD
1335 THEN STRIP_TAC;
1336 MATCH_MP_TAC LIM_CMUL
1337 THEN MATCH_MP_TAC LIM_MUL
1338 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1339 THEN EXPAND_TAC"v01n"
1340 THEN EXPAND_TAC"v02n"
1341 THEN EXPAND_TAC"v03n"
1342 THEN EXPAND_TAC"v12n"
1343 THEN EXPAND_TAC"v23n"
1344 THEN EXPAND_TAC"v13n"
1345 THEN EXPAND_TAC"v01"
1346 THEN EXPAND_TAC"v02"
1347 THEN EXPAND_TAC"v03"
1348 THEN EXPAND_TAC"v12"
1349 THEN EXPAND_TAC"v23"
1350 THEN EXPAND_TAC"v13"
1351 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1352 THEN STRIP_TAC;
1353 MATCH_MP_TAC LIM_MUL
1354 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1355 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
1356 THEN POP_ASSUM MP_TAC
1357 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1358 THEN STRIP_TAC
1359 THEN POP_ASSUM MATCH_MP_TAC
1360 THEN ASM_REWRITE_TAC[]
1361 THEN ASM_TAC
1362 THEN REWRITE_TAC[ETA_AX]
1363 THEN SET_TAC[];
1364 MATCH_MP_TAC LIM_MUL
1365 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1366 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-c:real^3`
1367 THEN POP_ASSUM MP_TAC
1368 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1369 THEN STRIP_TAC
1370 THEN POP_ASSUM MATCH_MP_TAC
1371 THEN ASM_REWRITE_TAC[]
1372 THEN MATCH_MP_TAC LIM_SUB
1373 THEN ASM_TAC
1374 THEN REWRITE_TAC[ETA_AX]
1375 THEN SET_TAC[];
1376 MATCH_MP_TAC LIM_ADD
1377 THEN STRIP_TAC;
1378 MATCH_MP_TAC LIM_CMUL
1379 THEN MATCH_MP_TAC LIM_MUL
1380 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1381 THEN EXPAND_TAC"v01n"
1382 THEN EXPAND_TAC"v02n"
1383 THEN EXPAND_TAC"v03n"
1384 THEN EXPAND_TAC"v12n"
1385 THEN EXPAND_TAC"v23n"
1386 THEN EXPAND_TAC"v13n"
1387 THEN EXPAND_TAC"v01"
1388 THEN EXPAND_TAC"v02"
1389 THEN EXPAND_TAC"v03"
1390 THEN EXPAND_TAC"v12"
1391 THEN EXPAND_TAC"v23"
1392 THEN EXPAND_TAC"v13"
1393 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1394 THEN STRIP_TAC;
1395 MATCH_MP_TAC LIM_MUL
1396 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1397 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a:real^3`
1398 THEN POP_ASSUM MP_TAC
1399 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1400 THEN STRIP_TAC
1401 THEN POP_ASSUM MATCH_MP_TAC
1402 THEN ASM_REWRITE_TAC[]
1403 THEN ASM_TAC
1404 THEN REWRITE_TAC[ETA_AX]
1405 THEN SET_TAC[];
1406 MATCH_MP_TAC LIM_MUL
1407 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1408 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`c:real^3`
1409 THEN POP_ASSUM MP_TAC
1410 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1411 THEN STRIP_TAC
1412 THEN POP_ASSUM MATCH_MP_TAC
1413 THEN ASM_REWRITE_TAC[]
1414 THEN ASM_TAC
1415 THEN REWRITE_TAC[ETA_AX]
1416 THEN SET_TAC[];
1417 MATCH_MP_TAC LIM_CMUL
1418 THEN MATCH_MP_TAC LIM_MUL
1419 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1420 THEN EXPAND_TAC"v01n"
1421 THEN EXPAND_TAC"v02n"
1422 THEN EXPAND_TAC"v03n"
1423 THEN EXPAND_TAC"v12n"
1424 THEN EXPAND_TAC"v23n"
1425 THEN EXPAND_TAC"v13n"
1426 THEN EXPAND_TAC"v01"
1427 THEN EXPAND_TAC"v02"
1428 THEN EXPAND_TAC"v03"
1429 THEN EXPAND_TAC"v12"
1430 THEN EXPAND_TAC"v23"
1431 THEN EXPAND_TAC"v13"
1432 THEN REWRITE_TAC[dist;VECTOR_ARITH`vec 0- A= --A`;NORM_NEG;LIFT_NEG;REAL_ARITH`A pow 2= A * A`;LIFT_CMUL]
1433 THEN STRIP_TAC;
1434 MATCH_MP_TAC LIM_MUL
1435 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1436 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`c:real^3`
1437 THEN POP_ASSUM MP_TAC
1438 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1439 THEN STRIP_TAC
1440 THEN POP_ASSUM MATCH_MP_TAC
1441 THEN ASM_REWRITE_TAC[]
1442 THEN ASM_TAC
1443 THEN REWRITE_TAC[ETA_AX]
1444 THEN SET_TAC[];
1445 MATCH_MP_TAC LIM_MUL
1446 THEN REWRITE_TAC[LIM_NULL_NORM;o_DEF]
1447 THEN  MRESA1_TAC CONTINUOUS_AT_LIFT_NORM`a-c:real^3`
1448 THEN POP_ASSUM MP_TAC
1449 THEN REWRITE_TAC[CONTINUOUS_AT_SEQUENTIALLY;o_DEF]
1450 THEN STRIP_TAC
1451 THEN POP_ASSUM MATCH_MP_TAC
1452 THEN ASM_REWRITE_TAC[]
1453 THEN MATCH_MP_TAC LIM_SUB
1454 THEN ASM_TAC
1455 THEN REWRITE_TAC[ETA_AX]
1456 THEN SET_TAC[]]);;
1457
1458 let COLLINEAR_B_SY=prove(`!s:stable_sy l:real^(M,3)finite_product.
1459 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
1460 /\ l IN B_SY1 (a_sy s) (b_sy s)
1461 /\ 1<= i /\ i<= k
1462 ==> ~collinear{vec 0, row i (vecmats l),row (SUC (i MOD k_sy s)) (vecmats l)}`,
1463 REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY;convex_local_fan;local_fan]
1464 THEN LET_TAC
1465 THEN REPEAT STRIP_TAC
1466 THEN POP_ASSUM MP_TAC
1467 THEN MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD k_sy s)) (vecmats (l:real^(M,3)finite_product))`;`(l:real^(M,3)finite_product)`]
1468 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))`;`row (SUC (i MOD k_sy s)) (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`]
1469 THEN POP_ASSUM MP_TAC
1470 THEN ASM_REWRITE_TAC[VECMATS_MATVEC_ID]
1471 THEN RESA_TAC);;
1472
1473
1474
1475 let COLLINEAR_AZIM_CYCLE_B_SY=prove(`!s:stable_sy l:real^(M,3)finite_product.
1476 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
1477 /\ l IN B_SY1 (a_sy s) (b_sy s)
1478 /\ 1<= i /\ i<= k
1479 ==> ~collinear{vec 0, row i (vecmats l),
1480 azim_cycle (EE (row i (vecmats l)) (E_SY (vecmats l)))
1481          (vec 0)
1482          (row i (vecmats l))
1483         (row (SUC (i MOD k_sy s)) (vecmats l))}`,
1484 REWRITE_TAC[B_SY1;IN_ELIM_THM;CONDITION2_SY;convex_local_fan;local_fan]
1485 THEN LET_TAC
1486 THEN REPEAT STRIP_TAC
1487 THEN POP_ASSUM MP_TAC
1488 THEN MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD k_sy s)) (vecmats (l:real^(M,3)finite_product))`;`(l:real^(M,3)finite_product)`]
1489 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))`;`row (SUC (i MOD k_sy s)) (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`]
1490 THEN POP_ASSUM MP_TAC
1491 THEN ASM_REWRITE_TAC[VECMATS_MATVEC_ID]
1492 THEN RESA_TAC
1493 THEN MRESAL_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))`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD k_sy s)) (vecmats (l:real^(M,3)finite_product))`][VECMATS_MATVEC_ID]
1494 THEN MRESAL_TAC Fan.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 k_sy s)) (vecmats (l:real^(M,3)finite_product))`][VECMATS_MATVEC_ID]
1495 THEN MRESAL_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 v') (E_SY v') (row i v')
1496       (row (SUC (i MOD k)) (v':real^3^M))`;`row i (vecmats (l:real^(M,3)finite_product))`][VECMATS_MATVEC_ID]
1497 THEN POP_ASSUM MP_TAC
1498 THEN RESA_TAC);;
1499
1500
1501 let AZIM_EQ_DIHV_IN_B_SY=prove(`!s:stable_sy l:real^(M,3)finite_product i.
1502 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
1503 /\ 1<= i /\ i<= k
1504 /\ (row i (vecmats l))= u
1505 /\ row (SUC (i MOD k_sy s)) (vecmats l)=v
1506 /\ azim_cycle (EE u (E_SY (vecmats l))) (vec 0) u v=w
1507 /\ l IN B_SY1 (a_sy s) (b_sy s)
1508 ==> azim (vec 0) u v w= dihV (vec 0) u v w`,
1509 REPEAT STRIP_TAC
1510 THEN ASM_TAC
1511 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
1512 THEN REPEAT STRIP_TAC
1513 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)
1514 THEN MRESA1_TAC (GEN_ALL VECMATS_MATVEC_ID)`v':real^3^M`
1515 THEN POP_ASSUM MP_TAC
1516 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
1517 THEN POP_ASSUM MP_TAC
1518 THEN POP_ASSUM MP_TAC
1519 THEN POP_ASSUM MP_TAC
1520 THEN DISCH_THEN(LABEL_TAC"THY")
1521 THEN DISCH_THEN(LABEL_TAC"THY2")
1522 THEN STRIP_TAC
1523 THEN POP_ASSUM(fun th-> MP_TAC th
1524 THEN REWRITE_TAC[convex_local_fan]
1525 THEN STRIP_TAC
1526 THEN POP_ASSUM MP_TAC
1527 THEN POP_ASSUM(fun th1-> MP_TAC th1
1528 THEN REWRITE_TAC[local_fan]
1529 THEN LET_TAC
1530 THEN STRIP_TAC
1531 THEN POP_ASSUM MP_TAC
1532 THEN POP_ASSUM(fun th2-> ASSUME_TAC (SYM th2))
1533 THEN STRIP_TAC
1534 THEN ASSUME_TAC th1)
1535 THEN DISCH_THEN(LABEL_TAC"THY1")
1536 THEN ASSUME_TAC th)
1537 THEN STRIP_TAC
1538 THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(SYM th))
1539 THEN REMOVE_THEN"THYGIANG"(fun th-> SUBST_ALL_TAC(th) THEN ASSUME_TAC th)
1540 THEN MRESA_TAC (GEN_ALL EDGE_IN_F_SY)[`i:num`;`u:real^3`;`v:real^3`;`l:real^(M,3)finite_product`]
1541 THEN REMOVE_THEN"THY1"(fun th-> MRESA1_TAC th`u:real^3,v:real^3`)
1542 THEN REMOVE_ASSUM_TAC
1543 THEN POP_ASSUM MP_TAC
1544 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))`;`((u,v):real^3#real^3)`]
1545 THEN MRESA_TAC( GEN_ALL COLLINEAR_B_SY)[`k:num`;`i:num`;`s:stable_sy`;`l:real^(M,3)finite_product`]
1546 THEN MRESA_TAC( GEN_ALL COLLINEAR_AZIM_CYCLE_B_SY)[`k:num`;`i:num`;`s:stable_sy`;`l:real^(M,3)finite_product`]
1547 THEN MATCH_MP_TAC Local_lemmas.AZIM_LE_PI_EQ_DIHV
1548 THEN ASM_REWRITE_TAC[]);;
1549
1550
1551 let CONTINUOUS_ON_RHO_FUN_AND_AZIM=prove_by_refinement(`!s:stable_sy .
1552 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
1553 ==> lift o(\x:real^(M,3)finite_product.  sum (1..k_sy s)
1554       (\i. rho_fun (norm (row i (vecmats x))) * azim_in_fan (row i (vecmats x), row (SUC (i MOD (k_sy s))) (vecmats x)) (E_SY (vecmats x))))
1555 continuous_on
1556  B_SY1 (a_sy s) (b_sy s)`,
1557 [REPEAT STRIP_TAC
1558 THEN SIMP_TAC[o_DEF;LIFT_SUM;FINITE_NUMSEG]
1559 THEN MATCH_MP_TAC CONTINUOUS_ON_VSUM
1560 THEN SIMP_TAC[o_DEF;LIFT_CMUL;FINITE_NUMSEG]
1561 THEN REPEAT STRIP_TAC
1562 THEN MATCH_MP_TAC CONTINUOUS_ON_MUL
1563 THEN STRIP_TAC;
1564 REWRITE_TAC[rho_fun;o_DEF;LIFT_ADD]
1565 THEN MATCH_MP_TAC CONTINUOUS_ON_ADD
1566 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;LIFT_CMUL;LIFT_SUB]
1567 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
1568 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
1569 THEN MATCH_MP_TAC CONTINUOUS_ON_CMUL
1570 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
1571 THEN REWRITE_TAC[CONTINUOUS_ON_CONST;]
1572 THEN MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE
1573 THEN MATCH_MP_TAC CONTINUOUS_ON_ROW
1574 THEN POP_ASSUM MP_TAC
1575 THEN ASM_REWRITE_TAC[IN_NUMSEG];
1576 MATCH_MP_TAC CONTINUOUS_ON_SAME_DOMAIN
1577 THEN EXISTS_TAC`(\y:real^(M,3)finite_product. lift(azim (vec 0) (row x (vecmats y)) (row (SUC (x MOD k_sy s)) (vecmats y))
1578          (azim_cycle (EE (row x (vecmats y)) (E_SY(vecmats y))) (vec 0) (row x (vecmats y)) (row (SUC (x MOD k_sy s)) (vecmats y)))))`
1579 THEN STRIP_TAC;
1580 POP_ASSUM MP_TAC
1581 THEN ASM_REWRITE_TAC[IN_NUMSEG;IN_ELIM_THM;B_SY1;CONDITION2_SY;convex_local_fan]
1582 THEN REPEAT STRIP_TAC
1583 THEN MRESAL_TAC (GEN_ALL EDGE_IN_F_SY)[`x:num`;`row x (v:real^3^M)`;`row (SUC (x MOD k)) (v:real^3^M)`;`(matvec v):real^(M,3)finite_product`][VECMATS_MATVEC_ID]
1584 THEN MRESAL_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY ((v:real^3^M) )`;`F_SY ((v:real^3^M))`;`E_SY ( (v:real^3^M))`;`row x (v:real^3^M),
1585   row (SUC (x MOD dimindex (:M))) v`][VECMATS_MATVEC_ID;];
1586 REWRITE_TAC[CONTINUOUS_ON_SEQUENTIALLY;o_DEF]
1587 THEN REPEAT STRIP_TAC
1588 THEN POP_ASSUM MP_TAC
1589 THEN POP_ASSUM MP_TAC
1590 THEN POP_ASSUM MP_TAC
1591 THEN DISCH_THEN(LABEL_TAC"THYGIANG1")
1592 THEN DISCH_THEN(LABEL_TAC"THYGIANG")
1593 THEN STRIP_TAC
1594 THEN ABBREV_TAC`u=(azim_cycle (EE (row x (vecmats a)) (E_SY (vecmats a))) (vec 0)
1595    (row x (vecmats a))
1596   (row (SUC (x MOD k_sy s)) (vecmats (a:real^(M,3)finite_product))))`
1597 THEN ABBREV_TAC`v= row x (vecmats (a:real^(M,3)finite_product))`
1598 THEN ABBREV_TAC`w=row (SUC (x MOD k_sy s)) (vecmats (a:real^(M,3)finite_product))`
1599 THEN ABBREV_TAC`wn=(\n:num. row (SUC (x MOD k_sy s)) (vecmats ((x':num->real^(M,3)finite_product) n)))`
1600 THEN ABBREV_TAC`vn=(\n. row x (vecmats ((x':num->real^(M,3)finite_product)n)))`
1601 THEN ABBREV_TAC`un=(\n. azim_cycle (EE (row x (vecmats ((x':num->real^(M,3)finite_product)n)))(E_SY (vecmats ((x':num->real^(M,3)finite_product)n)))) (vec 0) (row x (vecmats ((x':num->real^(M,3)finite_product)n))) (row (SUC (x MOD k_sy s)) (vecmats ((x':num->real^(M,3)finite_product) n))))`
1602 THEN SUBGOAL_THEN`!n:num. ~collinear{vec 0:real^3, vn n, wn n} /\ ~collinear{vec 0, vn n, un n}` ASSUME_TAC;
1603 STRIP_TAC
1604 THEN EXPAND_TAC"wn"
1605 THEN EXPAND_TAC"vn"
1606 THEN EXPAND_TAC"un"
1607 THEN REWRITE_TAC[]
1608 THEN FIND_ASSUM MP_TAC`x IN 1..k_sy (s:stable_sy)`
1609 THEN REWRITE_TAC[IN_NUMSEG]
1610 THEN RESA_TAC
1611 THEN MRESA_TAC( GEN_ALL COLLINEAR_B_SY)[`k:num`;`x:num`;`s:stable_sy`;`(x':num->real^(M,3)finite_product) n`]
1612 THEN MRESA_TAC( GEN_ALL COLLINEAR_AZIM_CYCLE_B_SY)[`k:num`;`x:num`;`s:stable_sy`;`(x':num->real^(M,3)finite_product) n`];
1613 POP_ASSUM MP_TAC
1614 THEN EXPAND_TAC"vn"
1615 THEN EXPAND_TAC"wn"
1616 THEN EXPAND_TAC"un"
1617 THEN REWRITE_TAC[]
1618 THEN
1619 SUBGOAL_THEN`(\x1. lift
1620         (azim (vec 0) (row x (vecmats (x' x1)))
1621          (row (SUC (x MOD k_sy s)) (vecmats (x' x1)))
1622         (azim_cycle (EE (row x (vecmats (x' x1))) (E_SY (vecmats (x' x1))))
1623          (vec 0)
1624          (row x (vecmats (x' x1)))
1625         (row (SUC (x MOD k_sy s)) (vecmats (x' x1))))))
1626 = lift o(\x1.
1627         (dihV (vec 0) (row x (vecmats (x' x1)))
1628          (row (SUC (x MOD k_sy s)) (vecmats (x' x1)))
1629         (azim_cycle (EE (row x (vecmats (x' x1))) (E_SY (vecmats (x' x1))))
1630          (vec 0)
1631          (row x (vecmats (x' x1)))
1632         (row (SUC (x MOD k_sy s)) (vecmats ((x':num->real^(M,3)finite_product) x1))))))
1633 `ASSUME_TAC;
1634 REWRITE_TAC[FUN_EQ_THM;LIFT_EQ; o_DEF]
1635 THEN GEN_TAC
1636 THEN MATCH_MP_TAC AZIM_EQ_DIHV_IN_B_SY
1637 THEN EXISTS_TAC`s:stable_sy`
1638 THEN EXISTS_TAC`(x':num->real^(M,3)finite_product)x''`
1639 THEN EXISTS_TAC`x:num`
1640 THEN ASM_REWRITE_TAC[]
1641 THEN FIND_ASSUM MP_TAC`x IN 1..k_sy (s:stable_sy)`
1642 THEN REWRITE_TAC[IN_NUMSEG]
1643 THEN RESA_TAC;
1644 POP_ASSUM(fun th-> REWRITE_TAC[th])
1645 THEN FIND_ASSUM MP_TAC`x IN 1..k_sy (s:stable_sy)`
1646 THEN REWRITE_TAC[IN_NUMSEG]
1647 THEN RESA_TAC
1648 THEN MRESA_TAC (GEN_ALL AZIM_EQ_DIHV_IN_B_SY)[`k:num`;`v:real^3`;`w:real^3`;`u:real^3`;`s:stable_sy`;`a:real^(M,3)finite_product`;`x:num`]
1649 THEN RESA_TAC
1650 THEN MATCH_MP_TAC SEQUENTIALLY_DIVH
1651 THEN ASM_REWRITE_TAC[]
1652 THEN MRESA_TAC( GEN_ALL COLLINEAR_B_SY)[`k:num`;`x:num`;`s:stable_sy`;`a:real^(M,3)finite_product`]
1653 THEN MRESA_TAC( GEN_ALL COLLINEAR_AZIM_CYCLE_B_SY)[`k:num`;`x:num`;`s:stable_sy`;`a:real^(M,3)finite_product`]
1654 THEN SUBGOAL_THEN`1 <= SUC (x MOD dimindex (:M)) /\
1655       SUC (x MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC;
1656 ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`]
1657 THEN MRESAL_TAC DIVISION[`x:num`;`dimindex (:M):num`][DIMINDEX_NONZERO]
1658 THEN POP_ASSUM MP_TAC
1659 THEN ARITH_TAC;
1660 POP_ASSUM MP_TAC
1661 THEN RESA_TAC
1662 THEN MRESAL_TAC (GEN_ALL LIM_VECMAT)[`(\n:num. vecmats ((x':num->real^(M,3)finite_product) n))`;`vecmats(a:real^(M,3)finite_product)`][MATVEC_VECMATS_ID;ETA_AX]
1663 THEN POP_ASSUM(fun th-> MRESA1_TAC th`x:num` THEN MRESA1_TAC th`(SUC (x MOD k))` THEN MP_TAC th THEN DISCH_THEN(LABEL_TAC"THY"))
1664 THEN EXPAND_TAC"w"
1665 THEN FIND_ASSUM (fun th-> REWRITE_TAC[th])`k_sy (s:stable_sy)=k`
1666 THEN ASM_REWRITE_TAC[]
1667 THEN MP_TAC(ARITH_RULE`1<= x ==> x=1 \/ 1<x:num`)
1668 THEN RESA_TAC;
1669 SUBGOAL_THEN`(\x1. azim_cycle (EE (row 1 (vecmats (x' x1))) (E_SY (vecmats (x' x1))))
1670         (vec 0)
1671         (row 1 (vecmats (x' x1)))
1672         (row (SUC (1 MOD k)) (vecmats (x' x1))))
1673 = (\x1. row k (vecmats ((x':num->real^(M,3)finite_product) x1)))` ASSUME_TAC;
1674 REWRITE_TAC[FUN_EQ_THM]
1675 THEN GEN_TAC
1676 THEN MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
1677 THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`]
1678 THEN MP_TAC(ARITH_RULE`2<k==> 1< k /\ 1<=k`)
1679 THEN RESA_TAC
1680 THEN MRESAL_TAC (GEN_ALL AZIM_CYCLE_EQ1)[`k:num`;`(row 1 (vecmats ((x':num->real^(M,3)finite_product) x'')))`;`(row (SUC (1 MOD k)) (vecmats ((x':num->real^(M,3)finite_product) x'')))`;`row k (vecmats ((x':num->real^(M,3)finite_product) x''))`;`(x':num->real^(M,3)finite_product) x''`][ARITH_RULE`SUC 0=1`]
1681 THEN POP_ASSUM MATCH_MP_TAC
1682 THEN REMOVE_THEN "THYGIANG"(fun th-> MRESA1_TAC th`x'':num` )
1683 THEN POP_ASSUM (fun th-> MP_TAC th
1684 THEN REWRITE_TAC[IN_ELIM_THM;B_SY1;CONDITION2_SY;convex_local_fan;local_fan]
1685 THEN LET_TAC
1686 THEN RESA_TAC
1687 THEN ASM_REWRITE_TAC[VECMATS_MATVEC_ID]
1688 THEN ASSUME_TAC th)
1689 THEN STRIP_TAC;
1690 ARITH_TAC;
1691 MRESAL_TAC(GEN_ALL INJ_ROW_B_SY)[`k:num`;`s:stable_sy`;`(x':num->real^(M,3)finite_product) x''`][IN_NUMSEG;VECMATS_MATVEC_ID]
1692 THEN POP_ASSUM MP_TAC
1693 THEN SET_TAC[];
1694 POP_ASSUM(fun th-> REWRITE_TAC[th])
1695 THEN EXPAND_TAC"u"
1696 THEN EXPAND_TAC"v"
1697 THEN EXPAND_TAC"w"
1698 THEN POP_ASSUM(fun th-> REWRITE_TAC[th] THEN ASSUME_TAC th)
1699 THEN SUBGOAL_THEN`azim_cycle (EE (row 1 (vecmats a)) (E_SY (vecmats a)))
1700         (vec 0)
1701         (row 1 (vecmats a))
1702         (row (SUC (1 MOD k)) (vecmats a))
1703 =  row k (vecmats ((a:real^(M,3)finite_product) ))` ASSUME_TAC;
1704 MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO]
1705 THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`]
1706 THEN MP_TAC(ARITH_RULE`2<k==> 1< k /\ 1<=k`)
1707 THEN RESA_TAC
1708 THEN MRESAL_TAC (GEN_ALL AZIM_CYCLE_EQ1)[`k:num`;`(row 1 (vecmats ((a:real^(M,3)finite_product) )))`;`(row (SUC (1 MOD k)) (vecmats ((a:real^(M,3)finite_product))))`;`row k (vecmats ((a:real^(M,3)finite_product) ))`;`(a:real^(M,3)finite_product)`][ARITH_RULE`SUC 0=1`]
1709 THEN POP_ASSUM MATCH_MP_TAC
1710 THEN REMOVE_THEN "THYGIANG1"(fun th-> MP_TAC th
1711 THEN REWRITE_TAC[IN_ELIM_THM;B_SY1;CONDITION2_SY;convex_local_fan;local_fan]
1712 THEN LET_TAC
1713 THEN RESA_TAC
1714 THEN ASM_REWRITE_TAC[VECMATS_MATVEC_ID]
1715 THEN ASSUME_TAC th)
1716 THEN STRIP_TAC;
1717 ARITH_TAC;
1718 MRESAL_TAC(GEN_ALL INJ_ROW_B_SY)[`k:num`;`s:stable_sy`;`(a:real^(M,3)finite_product) `][IN_NUMSEG;VECMATS_MATVEC_ID]
1719 THEN POP_ASSUM MP_TAC
1720 THEN SET_TAC[];
1721 POP_ASSUM(fun th-> ASM_REWRITE_TAC[th])
1722 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`k:num`)
1723 THEN POP_ASSUM MATCH_MP_TAC
1724 THEN MP_TAC(ARITH_RULE`2<k==> 1< k /\ 1<=k`)
1725 THEN RESA_TAC
1726 THEN ARITH_TAC;
1727 SUBGOAL_THEN`(\x1. azim_cycle (EE (row x (vecmats (x' x1))) (E_SY (vecmats (x' x1))))
1728         (vec 0)
1729         (row x (vecmats (x' x1)))
1730         (row (SUC (x MOD k)) (vecmats (x' x1))))
1731 = (\x1. row (x-1) (vecmats ((x':num->real^(M,3)finite_product) x1)))` ASSUME_TAC;
1732 REWRITE_TAC[FUN_EQ_THM]
1733 THEN GEN_TAC
1734 THEN MRESAL_TAC (GEN_ALL AZIM_CYCLE_EQ1)[`x-1:num`;`(row x (vecmats ((x':num->real^(M,3)finite_product) x'')))`;`(row (SUC (x MOD k)) (vecmats ((x':num->real^(M,3)finite_product) x'')))`;`row (x-1) (vecmats ((x':num->real^(M,3)finite_product) x''))`;`(x':num->real^(M,3)finite_product) x''`][ARITH_RULE`SUC 0=1`]
1735 THEN POP_ASSUM MATCH_MP_TAC
1736 THEN MP_TAC(ARITH_RULE`2<k /\ 1< x/\ x<= k ==> 1< k /\ 1<=k /\ 1<= x-1 /\ x-1<= k/\ x-1< k`)
1737 THEN RESA_TAC
1738 THEN MRESAL_TAC MOD_LT[`x-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]
1739 THEN MP_TAC(ARITH_RULE`1<= x /\ x<= dimindex (:M) ==>   SUC (x-1)=x`)
1740 THEN RESA_TAC
1741 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
1742 THEN ASM_REWRITE_TAC[]
1743 THEN REMOVE_THEN "THYGIANG"(fun th-> MRESA1_TAC th`x'':num` )
1744 THEN POP_ASSUM (fun th-> MP_TAC th
1745 THEN REWRITE_TAC[IN_ELIM_THM;B_SY1;CONDITION2_SY;convex_local_fan;local_fan]
1746 THEN LET_TAC
1747 THEN RESA_TAC
1748 THEN ASM_REWRITE_TAC[VECMATS_MATVEC_ID]
1749 THEN ASSUME_TAC th)
1750 THEN MRESAL_TAC(GEN_ALL INJ_ROW_B_SY)[`k:num`;`s:stable_sy`;`(x':num->real^(M,3)finite_product) x''`][IN_NUMSEG;VECMATS_MATVEC_ID]
1751 THEN POP_ASSUM MP_TAC
1752 THEN SET_TAC[];
1753 POP_ASSUM(fun th-> REWRITE_TAC[th])
1754 THEN EXPAND_TAC"u"
1755 THEN EXPAND_TAC"v"
1756 THEN EXPAND_TAC"w"
1757 THEN POP_ASSUM(fun th-> REWRITE_TAC[th] THEN ASSUME_TAC th)
1758 THEN SUBGOAL_THEN`azim_cycle (EE (row x (vecmats a)) (E_SY (vecmats a)))
1759         (vec 0)
1760         (row x (vecmats a))
1761         (row (SUC (x MOD k)) (vecmats a))
1762 =  row (x-1) (vecmats ((a:real^(M,3)finite_product) ))` ASSUME_TAC;
1763 MRESAL_TAC (GEN_ALL AZIM_CYCLE_EQ1)[`x-1:num`;`(row x (vecmats ((a:real^(M,3)finite_product) )))`;`(row (SUC (x MOD k)) (vecmats ((a:real^(M,3)finite_product))))`;`row (x-1) (vecmats ((a:real^(M,3)finite_product) ))`;`(a:real^(M,3)finite_product)`][ARITH_RULE`SUC 0=1`]
1764 THEN POP_ASSUM MATCH_MP_TAC
1765 THEN MP_TAC(ARITH_RULE`2<k /\ 1< x/\ x<= k ==> 1< k /\ 1<=k /\ 1<= x-1 /\ x-1<= k/\ x-1< k`)
1766 THEN RESA_TAC
1767 THEN MRESAL_TAC MOD_LT[`x-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`]
1768 THEN MP_TAC(ARITH_RULE`1<= x /\ x<= dimindex (:M) ==>   SUC (x-1)=x`)
1769 THEN RESA_TAC
1770 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th])
1771 THEN ASM_REWRITE_TAC[]
1772 THEN REMOVE_THEN "THYGIANG1"(fun th-> MP_TAC th
1773 THEN REWRITE_TAC[IN_ELIM_THM;B_SY1;CONDITION2_SY;convex_local_fan;local_fan]
1774 THEN LET_TAC
1775 THEN RESA_TAC
1776 THEN ASM_REWRITE_TAC[VECMATS_MATVEC_ID]
1777 THEN ASSUME_TAC th)
1778 THEN MRESAL_TAC(GEN_ALL INJ_ROW_B_SY)[`k:num`;`s:stable_sy`;`(a:real^(M,3)finite_product) `][IN_NUMSEG;VECMATS_MATVEC_ID]
1779 THEN POP_ASSUM MP_TAC
1780 THEN SET_TAC[];
1781 FIND_ASSUM(fun th-> REWRITE_TAC[th])`k_sy (s:stable_sy)= k`
1782 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[th])
1783 THEN REMOVE_THEN"THY"(fun th-> MRESA1_TAC th`x-1:num`)
1784 THEN POP_ASSUM MATCH_MP_TAC
1785 THEN MP_TAC(ARITH_RULE`1< x /\ x<= dimindex (:M) ==> 1<= x-1 /\ x-1<=dimindex (:M)`)
1786 THEN RESA_TAC]);;
1787
1788 let CONTINUOUS_ON_TAU_FUN=prove(`!s:stable_sy .
1789 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
1790 ==> lift o(\l:real^(M,3)finite_product. tau_fun (V_SY (vecmats l)) (E_SY (vecmats l)) (F_SY (vecmats l))) continuous_on (B_SY1 (a_sy s) (b_sy s))`,
1791 REWRITE_TAC[tau_fun; o_DEF;LIFT_SUB]
1792 THEN REPEAT STRIP_TAC
1793 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
1794 THEN MRESAL_TAC (GEN_ALL CONTINUOUS_ON_RHO_FUN_AND_AZIM)[`k:num`;`s:stable_sy`][o_DEF]
1795 THEN STRIP_TAC
1796 THENL[
1797 MATCH_MP_TAC CONTINUOUS_ON_SAME_DOMAIN
1798 THEN EXISTS_TAC`(\x:real^(M,3)finite_product. lift
1799            (sum (1..k)
1800            (\i. rho_fun (norm (row i (vecmats x))) *
1801                 azim_in_fan
1802                 (row i (vecmats x),row (SUC (i MOD k)) (vecmats x))
1803                 (E_SY (vecmats x)))))`
1804 THEN ASM_REWRITE_TAC[]
1805 THEN REPEAT STRIP_TAC
1806 THEN MRESA_TAC (GEN_ALL CHANGE_SUM_TAU_FUN)[`k:num`;`s:stable_sy`;`x:real^(M,3)finite_product`];
1807 MATCH_MP_TAC CONTINUOUS_ON_SAME_DOMAIN
1808 THEN EXISTS_TAC`(\x:real^(M,3)finite_product. lift ((pi + sol0) * &(k-2 )))`
1809 THEN REWRITE_TAC[CONTINUOUS_ON_CONST]
1810 THEN REPEAT STRIP_TAC
1811 THEN MP_TAC(ARITH_RULE`2<k==> 1<k`)
1812 THEN RESA_TAC
1813 THEN MRESAL_TAC(GEN_ALL INJ_ROW_B_SY)[`k:num`;`s:stable_sy`;`x:real^(M,3)finite_product`][IN_NUMSEG;VECMATS_MATVEC_ID;SET_RULE`(1 <= i /\ i <= k) /\
1814           (1 <= j /\ j <= k) /\
1815           row i (vecmats x) = row j (vecmats x)
1816 <=> 1 <= i /\ i <= k /\
1817           1 <= j /\ j <= k /\
1818           row i (vecmats x) = row j (vecmats x)`]
1819 THEN MRESA1_TAC (GEN_ALL CARD_F_SY_EQ)`x:real^(M,3)finite_product`]);;
1820
1821
1822 let CONTINUOUS_ON_TAU_STAR=prove(`!s:stable_sy .
1823 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
1824 ==> lift o(\l:real^(M,3)finite_product. tau_star s l) continuous_on (B_SY1 (a_sy s) (b_sy s))`,
1825 REWRITE_TAC[tau_star;o_DEF;LIFT_SUB]
1826 THEN REPEAT STRIP_TAC
1827 THEN MATCH_MP_TAC CONTINUOUS_ON_SUB
1828 THEN MRESAL_TAC (GEN_ALL CONTINUOUS_ON_D_FUN)[`k:num`;`s:stable_sy`][o_DEF]
1829 THEN MRESAL_TAC (GEN_ALL CONTINUOUS_ON_TAU_FUN)[`k:num`;`s:stable_sy`][o_DEF]);;
1830
1831 let MINIMUM_IN_B_SY=prove(`!s:stable_sy .
1832 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
1833 /\ ~(B_SY1 (a_sy s) (b_sy s) = {}:real^(M,3)finite_product->bool)
1834 ==> ?x:real^(M,3)finite_product. x IN  (B_SY1 (a_sy s) (b_sy s))
1835 /\ (!y:real^(M,3)finite_product. y IN (B_SY1 (a_sy s) (b_sy s))
1836 ==> tau_star s x <= tau_star s y)`,
1837 REPEAT STRIP_TAC
1838 THEN MRESA_TAC CONTINUOUS_ATTAINS_INF[`(\l:real^(M,3)finite_product. tau_star (s:stable_sy) l)`;`(B_SY1 (a_sy s) (b_sy (s:stable_sy))):real^(M,3)finite_product->bool`]
1839 THEN POP_ASSUM MATCH_MP_TAC
1840 THEN STRIP_TAC
1841 THENL[
1842 REWRITE_TAC[B_SY1]
1843 THEN MRESA_TAC(GEN_ALL WJSCPRO) [`d_sy (s:stable_sy)`;`J_SY(s:stable_sy)`;`k:num`;`a_sy(s:stable_sy)`;`b_sy(s:stable_sy)`;]
1844 THEN MRESA1_TAC stable_sy_lemma`s:stable_sy`;
1845 MRESA_TAC (GEN_ALL CONTINUOUS_ON_TAU_STAR)[`k:num`;`s:stable_sy`]]);;
1846
1847
1848 let HDPLYGY=prove(`!s:stable_sy .
1849 k_sy s =k /\ dimindex(:M) =k/\ I_SY s= 0..k-1 /\ f_sy s=(\i. ((1+i):num MOD k)) /\ 2<k
1850 /\ ~(B_SY1 (a_sy s) (b_sy s) = {}:real^(M,3)finite_product->bool)
1851 ==>
1852 lift o(\l:real^(M,3)finite_product. tau_star s l) continuous_on (B_SY1 (a_sy s) (b_sy s))
1853 /\(?x:real^(M,3)finite_product. x IN  (B_SY1 (a_sy s) (b_sy s))
1854 /\ (!y:real^(M,3)finite_product. y IN (B_SY1 (a_sy s) (b_sy s))
1855 ==> tau_star s x <= tau_star s y))`,
1856 REPEAT STRIP_TAC
1857 THENL[
1858 MRESA_TAC(GEN_ALL CONTINUOUS_ON_TAU_STAR)[`k:num`;`s:stable_sy`];
1859 MRESA_TAC (GEN_ALL MINIMUM_IN_B_SY)[`k:num`;`s:stable_sy`]]);;
1860
1861
1862
1863
1864
1865
1866
1867
1868
1869 end;;
1870
1871