text_formalization/local/AURSIPD.hl

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