text_formalization/local/RRCWNSJ.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 Rrcwnsj = 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 let BB_VV_FUN_EQ=prove(`is_scs_v39 s /\ BBs_v39 s vv
  93    ==> (!i j. vv i = vv j <=> i MOD (scs_k_v39 s) = j MOD (scs_k_v39 s))`,
  94 REPEAT RESA_TAC
  95 THEN EQ_TAC
  96 THENL[
  97 MRESA_TAC W_IN_BB_FUN_EQ[`vv`;`i`;`j`;`s`];
  98 MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`vv`;`j`]]);;
  99
 100 let WL_IN_E=prove(`{(w:num->real^3) l,w (SUC l)} IN IMAGE (\i. {w i,w (SUC i)}) (:num)`,
 101 REWRITE_TAC[IMAGE;IN_ELIM_THM]
 102 THEN EXISTS_TAC`l:num`
 103 THEN ASM_REWRITE_TAC[]
 104 THEN SET_TAC[]);;
 105
 106
 107
 108 let LUNAR_IN_V=prove(`lunar (v,w) V E==> v IN V/\ w IN V`,
 109 REWRITE_TAC[lunar]
 110 THEN SET_TAC[]);;
 111
 112
 113
 114 let B_LE_2h0_A_EQ2_IN_CASES_6=prove(
 115 `scs_k_v39 s=6  /\ is_scs_v39 s
 116 ==> !i. scs_b_v39 s i (SUC i)<= &2 *h0/\ scs_a_v39 s i (SUC i)= &2 `,
 117 STRIP_TAC
 118 THEN POP_ASSUM (fun th-> MP_TAC th
 119 THEN ASSUME_TAC th)
 120 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;]
 121 THEN RESA_TAC
 122 THEN GEN_TAC
 123 THEN DICH_TAC (0)
 124 THEN REWRITE_TAC[ARITH_RULE`a+b<=b <=> a= 0`]
 125 THEN SUBGOAL_THEN`FINITE
 126       {i | i < 6 /\
 127            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}` ASSUME_TAC
 128 THENL[
 129
 130 MATCH_MP_TAC FINITE_SUBSET
 131 THEN EXISTS_TAC`0..6`
 132 THEN ASM_REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_ELIM_THM;IN_NUMSEG]
 133 THEN ARITH_TAC;
 134
 135 MRESA_TAC CARD_EQ_0[`{i | i < 6 /\
 136         (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`]
 137 THEN REWRITE_TAC[SET_RULE`A={}<=> !x. ~(x IN A)`;IN_ELIM_THM]
 138 THEN MRESAL_TAC DIVISION[`i`;`6`][ARITH_RULE`~(6=0)`]
 139 THEN STRIP_TAC
 140 THEN THAYTHEL_TAC 0[`i MOD 6`][DE_MORGAN_THM;REAL_ARITH`~(a<b)<=> b<=a`]
 141 THEN POP_ASSUM MP_TAC
 142 THEN POP_ASSUM MP_TAC
 143 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i:num`;`SUC(i MOD 6)  MOD 6:num`;`s:scs_v39`;`i MOD 6:num`;`SUC(i MOD 6):num`][MOD_REFL;ARITH_RULE`~(6=0)`]
 144 THEN SYM_ASSUM_TAC
 145 THEN ASM_SIMP_TAC[Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)`]
 146 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i:num`;`SUC i MOD 6:num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`]
 147 THEN THAYTHES_TAC (26-17)[`i MOD 6`;`SUC i MOD 6`][DIVISION;Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)/\ 1<6`;Qknvmlb.SUC_MOD_NOT_EQ]
 148 THEN DICH_TAC 0
 149 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i:num`;`SUC(i MOD 6)  MOD 6:num`;`s:scs_v39`;`i MOD 6:num`;`SUC(i MOD 6):num`][MOD_REFL;ARITH_RULE`~(6=0)`]
 150 THEN SYM_ASSUM_TAC
 151 THEN ASM_SIMP_TAC[Hypermap.lemma_suc_mod;ARITH_RULE`~(6=0)`]
 152 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i:num`;`SUC i MOD 6:num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)/\ 1<6`;Qknvmlb.SUC_MOD_NOT_EQ]
 153 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`i MOD 6:num`;`SUC i MOD 6:num`;`s:scs_v39`;`i:num`;`SUC i:num`][MOD_REFL;ARITH_RULE`~(6=0)`]
 154 THEN REAL_ARITH_TAC]);;
 155
 156
 157
 158 let J_EMPY_CASES_6=prove(`scs_k_v39 s=6  /\ is_scs_v39 s
 159 ==>  scs_J_v39 s i= {}`,
 160 STRIP_TAC
 161 THEN MP_TAC(SET_RULE`(?x. scs_J_v39 s i x) \/ (scs_J_v39 s i= {})`)
 162 THEN RESA_TAC
 163 THEN MP_TAC B_LE_2h0_A_EQ2_IN_CASES_6
 164 THEN RESA_TAC
 165 THEN ASM_TAC
 166 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 167 THEN REPEAT RESA_TAC
 168 THEN THAYTHEL_ASM_TAC(22-19)[`i`;`x`][]
 169 THEN THAYTHEL_ASM_TAC (24-18)[`i`;`x`][]
 170 THENL[
 171
 172 DICH_TAC (25-18)
 173 THEN RESA_TAC
 174 THEN DICH_TAC 4
 175 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i`;`x`;`s`;`i`;`SUC i`][is_scs_v39]
 176 THEN THAYTHE_TAC (25-19)[`i`]
 177 THEN REMOVE_ASSUM_TAC
 178 THEN POP_ASSUM MP_TAC
 179 THEN SYM_ASSUM_TAC
 180 THEN REWRITE_TAC[h0;cstab]
 181 THEN REAL_ARITH_TAC;
 182
 183 DICH_TAC (25-18)
 184 THEN RESA_TAC
 185 THEN DICH_TAC 4
 186 THEN MRESAS_TAC(GEN_ALL CHANGE_B_SCS_MOD)[`i`;`x`;`s`;`SUC x`;`x`][is_scs_v39]
 187 THEN THAYTHE_TAC (25-19)[`x`]
 188 THEN REMOVE_ASSUM_TAC
 189 THEN POP_ASSUM MP_TAC
 190 THEN SYM_ASSUM_TAC
 191 THEN REWRITE_TAC[h0;cstab]
 192 THEN REAL_ARITH_TAC]);;
 193
 194
 195 let BB_RHO_NODE_IVS=prove(`scs_k_v39 s = k /\
 196        vv p1 = u /\
 197        IMAGE vv (:num) = V /\
 198        IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\
 199        IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\
 200        is_scs_v39 s /\
 201        3<k /\
 202        BBs_v39 s vv
 203        ==> rho_node1 FF u = vv (p1+1) /\ ivs_rho_node1 FF u = vv (p1+k-1)`,
 204 STRIP_TAC
 205 THEN MP_TAC(ARITH_RULE`3<k==> ~(k<=3)`)
 206 THEN RESA_TAC
 207 THEN MP_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME
 208 THEN RESA_TAC
 209 THEN THAYTHEL_ASM_TAC 0[`SUC 0`][ITER;I_DEF;ARITH_RULE`SUC 0+a= a+1`]
 210 THEN THAYTHEL_ASM_TAC 0[`k-1`][ITER;I_DEF;ARITH_RULE`SUC 0+a= a+1`]
 211 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`vv`]
 212 THEN MP_TAC Local_lemmas.CVLF_LF_F
 213 THEN RESA_TAC
 214 THEN MRESA_TAC WL_IN_V[`p1`;`vv`]
 215 THEN MP_TAC Odxlstcv2.CARD_V_EQ_SCS_K1
 216 THEN RESA_TAC
 217 THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1
 218 THEN RESA_TAC
 219 THEN THAYTHES_TAC 0[`vv p1`][WL_IN_V;ARITH_RULE`k-1+a=a+k-1`]);;
 220
 221
 222
 223 let BB_F_SUC_PRE=prove(`is_scs_v39 s /\ BBs_v39 s f ==> f (SUC (i + (scs_k_v39 s) - 1)) = f i`,
 224 STRIP_TAC
 225 THEN MATCH_MP_TAC Oxlzlez.F_SUC_PRE
 226 THEN POP_ASSUM MP_TAC
 227 THEN POP_ASSUM MP_TAC
 228 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39;is_scs_v39]
 229 THEN REPEAT RESA_TAC
 230 THEN POP_ASSUM MP_TAC
 231 THEN DICH_TAC (23-1)
 232 THEN ARITH_TAC);;
 233
 234
 235 let RRCWNSJ_concl = `
 236 main_nonlinear_terminal_v11
 237 ==>(!s (v:num->real^3).
 238   is_scs_v39 s /\ scs_basic_v39 s /\ MMs_v39 s v/\
 239   3< scs_k_v39 s /\
 240   (!i j. scs_diag (scs_k_v39 s) i j ==> &4 * h0 < scs_b_v39 s i j) /\
 241   (!i j. scs_diag (scs_k_v39 s) i j ==> (scs_a_v39 s i j <= cstab /\ cstab <     dist(v i, v j))) /\
 242   (!i. scs_b_v39 s i (SUC i) <= cstab) ==>
 243   scs_generic v)`;;
 244
 245
 246
 247
 248 let RRCWNSJ = prove_by_refinement(
 249  RRCWNSJ_concl,
 250 [
 251 STRIP_TAC
 252 THEN REPEAT GEN_TAC
 253 THEN ABBREV_TAC`k= scs_k_v39 s`
 254 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
 255 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
 256 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
 257 THEN REPEAT RESA_TAC
 258 THEN MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
 259 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
 260 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
 261 THEN MP_TAC Local_lemmas.CVLF_LF_F
 262 THEN RESA_TAC
 263 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
 264 THEN RESA_TAC
 265 THEN MRESA_TAC LUNAR_IN_V[`E`;`v'`;`w`;`V`]
 266 THEN POP_ASSUM MP_TAC
 267 THEN POP_ASSUM MP_TAC
 268 THEN EXPAND_TAC "V"
 269 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM]
 270 THEN REPEAT RESA_TAC
 271 THEN DICH_TAC 5
 272 THEN RESA_TAC
 273 THEN MRESA_TAC Axjrpnc.AXJRPNC[`s`;`v`;`x`;`x'`]
 274 THEN DICH_TAC 1
 275 THEN STRIP_TAC
 276 THEN POP_ASSUM(fun  th->ASSUME_TAC (SYM th))
 277 THEN MP_TAC B_LE_2h0_A_EQ2_IN_CASES_6
 278 THEN RESA_TAC
 279 THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`]
 280 THEN THAYTHEL_ASM_TAC 0[`x`][]
 281 THEN THAYTHE_TAC 0[`SUC x`]
 282 THEN SUBGOAL_THEN`norm((v:num->real^3) (SUC x))= &2 \/ norm (v x- v (SUC x))= &2` ASSUME_TAC;
 283
 284 MP_TAC(REAL_ARITH`&2 <= norm (v x - v (SUC x))
 285 /\ &2 <= norm (v (SUC x) - v (SUC (SUC x)))
 286 ==> (&2 < norm (v x - v (SUC x))
 287 /\ &2 < norm (v (SUC x) - v (SUC (SUC x))))\/  norm (v x - v (SUC x))= &2
 288 \/  (norm ((v:num->real^3) (SUC x) - v (SUC (SUC x)))= &2) `)
 289 THEN RESA_TAC;
 290
 291 SUBGOAL_THEN`!i. ~(i MOD k = (SUC x) MOD k) ==> scs_a_v39 s (SUC x) i < dist (v (SUC x),(v:num->real^3) i)`ASSUME_TAC
 292 ;
 293
 294
 295 REPEAT RESA_TAC
 296 THEN MP_TAC(SET_RULE`i MOD k= x MOD k\/ ~(i MOD k= x MOD k)`)
 297 THEN RESA_TAC;
 298
 299
 300 MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v:num->real^3`;`x:num`]
 301 THEN ONCE_REWRITE_TAC[DIST_SYM]
 302 THEN ASM_REWRITE_TAC[dist]
 303 THEN THAYTHE_TAC (33-26)[`x`]
 304 THEN DICH_TAC (34-28)
 305 THEN SYM_ASSUM_TAC
 306 THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC x`;`i `;`s:scs_v39`;`SUC x`;`x`][is_scs_v39]
 307 THEN ASM_TAC
 308 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
 309 THEN REPEAT RESA_TAC;
 310
 311
 312
 313 MP_TAC(SET_RULE`i MOD k= SUC (SUC x) MOD k\/ ~(i MOD k= SUC (SUC x) MOD k)`)
 314 THEN RESA_TAC;
 315
 316
 317
 318 MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v:num->real^3`;`SUC(SUC x):num`]
 319 THEN THAYTHEL_TAC (34-26)[`SUC(x)`][dist]
 320 THEN DICH_TAC (35-29)
 321 THEN SYM_ASSUM_TAC
 322 THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC x`;`i`;`s:scs_v39`;`SUC x`;`SUC(SUC x)`][is_scs_v39]
 323 THEN ASM_TAC
 324 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
 325 THEN REPEAT RESA_TAC;
 326
 327
 328
 329 MP_TAC(ARITH_RULE`~(6=0)`)
 330 THEN RESA_TAC
 331 THEN THAYTHES_TAC (34-9)[`i`;`SUC x`][scs_diag;ADD1;ARITH_RULE`~(6=0)/\ i+1=1+i`;Ocbicby.MOD_EQ_MOD_SHIFT]
 332 THEN ONCE_REWRITE_TAC[DIST_SYM]
 333 THEN ASM_TAC
 334 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
 335 THEN REPEAT RESA_TAC
 336 THEN POP_ASSUM MP_TAC
 337 THEN DICH_TAC 0
 338 THEN REAL_ARITH_TAC;
 339
 340
 341 MRESA_TAC J_EMPY_CASES_6[`s`;`SUC x`]
 342 THEN DICH_TAC 0
 343 THEN REWRITE_TAC[SET_RULE`(a = {})<=> !i. ~ (a i)`]
 344 THEN STRIP_TAC
 345 THEN MRESAL_TAC ODXLSTCv2[`s`;`k`;`v`;`SUC x`][DE_MORGAN_THM;]
 346 THEN POP_ASSUM MP_TAC
 347 THEN SUBGOAL_THEN`!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (SUC x)) V' E'`
 348 ASSUME_TAC
 349 ;
 350
 351
 352 REPEAT RESA_TAC
 353 THEN DICH_TAC (35-23)
 354 THEN RESA_TAC
 355 THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
 356 THEN REPLICATE_TAC (49-36) (REMOVE_ASSUM_TAC)
 357 THEN MRESA_TAC WL_IN_V[`SUC x`;`v:num->real^3`]
 358 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~(1 MOD 6= 3 MOD 6)`)
 359 THEN RESA_TAC
 360 THEN THAYTHES_TAC 5[`(v:num->real^3) (SUC x)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
 361 THEN POP_ASSUM MP_TAC
 362 THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT]
 363 THEN MRESAS_TAC Jkqewgv.JKQEWGV3[`s`;`v`;`v (SUC x)`;`v1`][LET_DEF;LET_END_DEF;]
 364 THEN DICH_TAC 0
 365 THEN ONCE_REWRITE_TAC[Local_lemmas.LUNAR_COMM]
 366 THEN ASM_REWRITE_TAC[ADD1]
 367 THEN MP_TAC PI_WORKS
 368 THEN REAL_ARITH_TAC;
 369
 370 ASM_REWRITE_TAC[]
 371 ;
 372
 373
 374 MP_TAC(REAL_ARITH`norm (v (SUC x)) = &2 \/ ~(norm ((v:num->real^3) (SUC x)) = &2)`)
 375 THEN RESA_TAC
 376 THEN MRESA_TAC J_EMPY_CASES_6[`s`;`SUC x`]
 377 THEN DICH_TAC 0
 378 THEN REWRITE_TAC[SET_RULE`(a = {})<=> !i. ~ (a i)`]
 379 THEN STRIP_TAC
 380 THEN SUBGOAL_THEN`!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (SUC x)) V' E'`
 381 ASSUME_TAC
 382 ;
 383
 384
 385 REPEAT RESA_TAC
 386 THEN DICH_TAC (34-23)
 387 THEN RESA_TAC
 388 THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
 389 THEN REPLICATE_TAC (48-35) (REMOVE_ASSUM_TAC)
 390 THEN MRESA_TAC WL_IN_V[`SUC x`;`v:num->real^3`]
 391 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~(1 MOD 6= 3 MOD 6)`)
 392 THEN RESA_TAC
 393 THEN THAYTHES_TAC 5[`(v:num->real^3) (SUC x)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
 394 THEN POP_ASSUM MP_TAC
 395 THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT]
 396 THEN MRESAS_TAC Jkqewgv.JKQEWGV3[`s`;`v`;`v (SUC x)`;`v1`][LET_DEF;LET_END_DEF;]
 397 THEN DICH_TAC 0
 398 THEN ONCE_REWRITE_TAC[Local_lemmas.LUNAR_COMM]
 399 THEN ASM_REWRITE_TAC[ADD1]
 400 THEN MP_TAC PI_WORKS
 401 THEN REAL_ARITH_TAC;
 402
 403
 404 SUBGOAL_THEN`(!i. scs_diag k (SUC x) i
 405            ==> scs_a_v39 s (SUC x) i < dist (v (SUC x),(v:num->real^3) i))`ASSUME_TAC
 406 ;
 407
 408 GEN_TAC
 409 THEN STRIP_TAC
 410 THEN THAYTHE_TAC (33-9)[`SUC x`;`i`]
 411 THEN POP_ASSUM MP_TAC
 412 THEN POP_ASSUM MP_TAC
 413 THEN REAL_ARITH_TAC
 414 ;
 415
 416
 417
 418
 419 SUBGOAL_THEN`azim (vec 0) (v (SUC x)) (v (SUC (SUC x))) ((v:num->real^3) (SUC x + k - 1)) = pi`ASSUME_TAC
 420 ;
 421
 422
 423 DICH_TAC (33-23)
 424 THEN RESA_TAC
 425 THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
 426 THEN REPLICATE_TAC (48-35) (REMOVE_ASSUM_TAC)
 427 THEN MRESA_TAC WL_IN_V[`SUC x`;`v:num->real^3`]
 428 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~(1 MOD 6= 3 MOD 6)`)
 429 THEN RESA_TAC
 430 THEN THAYTHES_TAC 5[`(v:num->real^3) (SUC x)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
 431 THEN POP_ASSUM MP_TAC
 432 THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT;interior_angle1;GSYM ivs_rho_node1]
 433 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (x+1)`;`v`;`x+1`;`k`];
 434
 435
 436 SUBGOAL_THEN`~collinear {vec 0, (v:num->real^3) (SUC (SUC x)), v (SUC x + k - 1)}`
 437 ASSUME_TAC
 438 ;
 439
 440
 441 DICH_TAC (34-23)
 442 THEN RESA_TAC
 443 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~(2 MOD 6= 3 MOD 6)/\ ~(2 MOD 6= 0 MOD 6)`)
 444 THEN RESA_TAC
 445 THEN MRESA_TAC Lunar_deform.LOCAL_CONVEX_NOT_COLLINEAR[`FF`;`E`;`V`;`w`;`v'`]
 446 THEN MRESA_TAC BB_F_SUC_PRE[`s`;`v`;`x`]
 447 THEN ASM_SIMP_TAC[BB_F_SUC_PRE;ARITH_RULE`SUC i+k-1=SUC(i+k-1)`]
 448 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 449 THEN MATCH_DICH_TAC 1
 450 THEN MRESAS_TAC WL_IN_V[`SUC (SUC x)`;`v:num->real^3`][BB_VV_FUN_EQ;ARITH_RULE`SUC (SUC x)=x+2`;Ocbicby.MOD_EQ_MOD_SHIFT]
 451 THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
 452 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
 453 THEN RESA_TAC
 454 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT];
 455
 456
 457
 458
 459
 460 SUBGOAL_THEN`(v:num->real^3) (SUC x) IN aff_gt {vec 0} {v (SUC (SUC x)), v (SUC x + k - 1)}`
 461 ASSUME_TAC;
 462
 463
 464 DICH_TAC (35-23)
 465 THEN RESA_TAC
 466 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~(2 MOD 6= 1 MOD 6)/\ ~(2 MOD 6= 0 MOD 6)/\ ~(6<=3)/\ 3 MOD 6=3`)
 467 THEN RESA_TAC
 468 THEN MRESA_TAC Odxlstcv2.CARD_V_EQ_SCS_K1[`s`;`v`;`V`;`k`]
 469 THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v x`;`v`;`x`]
 470 THEN MRESAS_TAC Local_lemmas.LUNAR_IMP_HALF_CIRCLE_SUBSET_AFF_GT[`E`;`V`;`w`;`FF`;`v'`][BB_VV_FUN_EQ]
 471 THEN DICH_TAC 1
 472 THEN ASM_SIMP_TAC[BB_VV_FUN_EQ;]
 473 THEN ONCE_REWRITE_TAC[ARITH_RULE`i+x=x+i:num`]
 474 THEN REWRITE_TAC[ARITH_RULE`3+x=x+3`]
 475 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
 476 THEN STRIP_TAC
 477 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
 478 THEN DICH_TAC 1
 479 THEN MRESAL_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;` FF`;`v x`;`v`;`x`;`k`][ARITH_RULE`0< l/\ l<3<=> l=1\/ l=2`;SET_RULE`{v (l + x) | l = 1 \/ l = 2} = {v (1+x), v(2+x)}`;SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`;ARITH_RULE`2+x=x+2`]
 480 THEN STRIP_TAC
 481 THEN MP_TAC(SET_RULE`v (x + 2) IN aff_gt {vec 0, v x} {v (x + 1)}
 482 /\  aff_gt {vec 0, v x} {v (x + 1)} SUBSET aff_ge {vec 0, v x} {v (x + 1)}
 483 ==> v (x + 2) IN aff_ge {vec 0, (v:num->real^3) x} {v (x + 1)}`)
 484 THEN ASM_REWRITE_TAC[AFF_GT_SUBSET_AFF_GE]
 485 THEN STRIP_TAC
 486 THEN MRESA_TAC BB_F_SUC_PRE[`s`;`v`;`x`]
 487 THEN ASM_SIMP_TAC[BB_F_SUC_PRE;ARITH_RULE`k-1+ SUC i=SUC(i+k-1)`]
 488 THEN DICH_TAC(52-34)
 489 THEN ASM_SIMP_TAC[BB_F_SUC_PRE;ARITH_RULE`SUC i+k-1=SUC(i+k-1)/\ SUC (SUC x)= x+2`]
 490 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 491 THEN RESA_TAC
 492 THEN MRESA_TAC WL_IN_V[`x`;`v:num->real^3`]
 493 THEN MRESA_TAC WL_IN_V[`x+2`;`v:num->real^3`]
 494 THEN MRESAL_TAC WL_IN_E[`x`;`v:num->real^3`][ADD1]
 495 THEN MRESA_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2[`E`;`V`;`FF`;`v x`]
 496 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
 497 THEN MRESAL_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`v x`;`v (x+1)`;`v (x+2)`][ADD1]
 498 THEN MRESA_TAC th3[`vec 0:real^3`;`v x`;`v (x+2)`]
 499 THEN MRESAS_TAC Planarity.POINT_IN_AFF_GE_IMP_IN_EDGE[`vec 0:real^3`;`V`;`E`;`v(x)`;`v (x+1)`;`v (x+2)`][SET_RULE`a IN{b,c}<=> a=b\/ a=c`;Ocbicby.MOD_EQ_MOD_SHIFT;BB_VV_FUN_EQ]
 500 ;
 501
 502
 503 MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
 504 THEN GEN_REWRITE_TAC( LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x:num`]
 505 THEN RESA_TAC
 506 THEN DICH_TAC 1
 507 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
 508 ;
 509
 510
 511 MRESAL_TAC IMJXPHRv2[`s`;`k`;`v`;`SUC x`][dist]
 512 THEN POP_ASSUM MP_TAC
 513 THEN MRESA_TAC BB_F_SUC_PRE[`s`;`v`;`x`]
 514 THEN ASM_SIMP_TAC[BB_F_SUC_PRE;ARITH_RULE` SUC i+k-1=SUC(i+k-1)`]
 515 THEN MP_TAC(ARITH_RULE`SUC (x + 6 - 1)= 1*6+x/\ ~(6=0)`)
 516 THEN RESA_TAC
 517 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC x:num`;`1*k+x `;`s:scs_v39`;`SUC x:num`;`(1*k+x) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
 518 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`SUC x:num`;`x MOD k `;`s:scs_v39`;`SUC x:num`;`x:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
 519 THEN STRIP_TAC
 520 THEN REWRITE_TAC[GSYM dist]
 521 THEN ONCE_REWRITE_TAC[DIST_SYM]
 522 THEN REWRITE_TAC[dist]
 523 THEN SYM_ASSUM_TAC
 524 THEN ASM_TAC
 525 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 526 THEN REPEAT RESA_TAC
 527 ;
 528
 529
 530 (********CASES 2*****)
 531
 532
 533
 534 SUBGOAL_THEN`norm((v:num->real^3) (x+k-1))= &2 \/ norm (v (x+k-1)- v (x))= &2` ASSUME_TAC;
 535
 536 REPLICATE_TAC 3 REMOVE_ASSUM_TAC
 537 THEN ASSUME_TAC(ARITH_RULE`(x + k - 1) + k - 1=x + k - 1 + k - 1`)
 538 THEN MRESA_TAC BB_F_SUC_PRE[`s`;`v`;`x`]
 539 THEN MRESAL_TAC BB_F_SUC_PRE[`s`;`v`;`x+k-1`][]
 540 THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`]
 541 THEN THAYTHEL_ASM_TAC 0[`x+k-1`][]
 542 THEN THAYTHE_TAC 0[`x+ k-1+k-1`]
 543 THEN MP_TAC(REAL_ARITH`&2 <= norm (v (x+k-1) - v (x))
 544 /\ &2 <= norm (v (x+k-1+k-1) - v (x+k-1))
 545 ==> (&2 < norm (v (x+k-1) - v (x))
 546 /\ &2 < norm (v (x+k-1+k-1) - v (x+k-1)))\/  norm (v (x+k-1) - v (x))= &2
 547 \/  (norm ((v:num->real^3) (x+k-1+k-1) - v (x+k-1))= &2) `)
 548 THEN RESA_TAC;
 549
 550 SUBGOAL_THEN`!i. ~(i MOD k = (x+k-1) MOD k) ==> scs_a_v39 s (x+k-1) i < dist (v (x+k-1),(v:num->real^3) i)`ASSUME_TAC
 551 ;
 552
 553
 554 REPEAT RESA_TAC
 555 THEN MP_TAC(SET_RULE`i MOD k= x MOD k\/ ~(i MOD k= x MOD k)`)
 556 THEN RESA_TAC;
 557
 558
 559 MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v:num->real^3`;`x:num`]
 560 THEN THAYTHE_TAC (36-26)[`x+k-1`]
 561 THEN POP_ASSUM MP_TAC
 562 THEN MP_TAC(ARITH_RULE`SUC (x + 6 - 1)= 1*6+x/\ ~(6=0)`)
 563 THEN RESA_TAC
 564 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1:num`;`1*k+x `;`s:scs_v39`;` x+k-1:num`;`(1*k+x) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
 565 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1:num`;`x MOD k `;`s:scs_v39`;` x+k-1:num`;`x:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
 566 THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1`;`i `;`s:scs_v39`;` x+k-1`;`x`][is_scs_v39;dist]
 567 THEN RESA_TAC
 568 THEN DICH_TAC (42-31)
 569 ;
 570
 571 MP_TAC(SET_RULE`i MOD k= (x+k-1+k-1) MOD k\/ ~(i MOD k= (x+k-1+k-1) MOD k)`)
 572 THEN RESA_TAC;
 573
 574
 575
 576 MRESA_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`i`;`v:num->real^3`;`(x+k-1+k-1):num`]
 577 THEN ONCE_REWRITE_TAC[DIST_SYM]
 578 THEN THAYTHEL_TAC (37-26)[`x+k-1+k-1`][dist]
 579 THEN DICH_TAC 0
 580 THEN MP_TAC(ARITH_RULE`SUC (x + 6 - 1+ 6 - 1)= 1*6+(x+ 6 - 1)/\ ~(6=0)`)
 581 THEN RESA_TAC
 582 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1+k-1:num`;`1*k+(x+k-1) `;`s:scs_v39`;` x+k-1+k-1:num`;`(1*k+(x+k-1)) MOD k:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
 583 THEN MRESAS_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1+k-1:num`;`(x+k-1) MOD k `;`s:scs_v39`;` x+k-1+k-1:num`;`x+k-1:num`][MOD_REFL;ARITH_RULE`~(6=0)`;MOD_MULT_ADD]
 584 THEN MRESAL_TAC(GEN_ALL CHANGE_A_SCS_MOD)[`x+k-1`;`i `;`s:scs_v39`;` x+k-1`;`x+k-1+k-1`][is_scs_v39;dist]
 585 THEN ASM_TAC
 586 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
 587 THEN REPEAT RESA_TAC;
 588
 589
 590
 591 MP_TAC(ARITH_RULE`~(6=0)/\  1+(x + 6- 1)= 1*6+x`)
 592 THEN RESA_TAC
 593 THEN THAYTHES_TAC (38-9)[`i`;`x+k-1`][scs_diag;ADD1;ARITH_RULE`~(6=0)/\ i+1=1+i`;Ocbicby.MOD_EQ_MOD_SHIFT;MOD_MULT_ADD]
 594 THEN ONCE_REWRITE_TAC[DIST_SYM]
 595 THEN DICH_TAC 0
 596 THEN MP_TAC(ARITH_RULE`x+6-1=1+(x+6-2)`)
 597 THEN RESA_TAC
 598 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
 599 THEN DICH_TAC 3
 600 THEN MP_TAC(ARITH_RULE`x+6-1+6-1=1*6+(x+6-2)`)
 601 THEN RESA_TAC
 602 THEN ASM_SIMP_TAC[MOD_MULT_ADD]
 603 THEN ASM_TAC
 604 THEN REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF]
 605 THEN REPEAT RESA_TAC
 606 THEN POP_ASSUM MP_TAC
 607 THEN DICH_TAC 0
 608 THEN REAL_ARITH_TAC;
 609
 610
 611 MRESA_TAC J_EMPY_CASES_6[`s`;`x+k-1`]
 612 THEN DICH_TAC 0
 613 THEN REWRITE_TAC[SET_RULE`(a = {})<=> !i. ~ (a i)`]
 614 THEN STRIP_TAC
 615 THEN MRESAL_TAC ODXLSTCv2[`s`;`k`;`v`;`x+k-1`][DE_MORGAN_THM;]
 616 THEN POP_ASSUM MP_TAC
 617 THEN SUBGOAL_THEN`!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (x+k-1)) V' E'`
 618 ASSUME_TAC
 619 ;
 620
 621
 622 REPEAT RESA_TAC
 623 THEN DICH_TAC (38-23)
 624 THEN RESA_TAC
 625 THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
 626 THEN REPLICATE_TAC (52-39) (REMOVE_ASSUM_TAC)
 627 THEN MRESA_TAC WL_IN_V[`x+k-1`;`v:num->real^3`]
 628 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~((6-1) MOD 6= 3 MOD 6) /\ ~((6-1) MOD 6= 0 MOD 6)`)
 629 THEN RESA_TAC
 630 THEN THAYTHES_TAC 6[`(v:num->real^3) (x+k-1)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
 631 THEN POP_ASSUM MP_TAC
 632 THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT]
 633 THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
 634 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
 635 THEN RESA_TAC
 636 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
 637 THEN MRESAS_TAC Jkqewgv.JKQEWGV3[`s`;`v`;`v (x+k-1)`;`v1`][LET_DEF;LET_END_DEF;]
 638 THEN DICH_TAC 0
 639 THEN ONCE_REWRITE_TAC[Local_lemmas.LUNAR_COMM]
 640 THEN ASM_REWRITE_TAC[ADD1]
 641 THEN MP_TAC PI_WORKS
 642 THEN REAL_ARITH_TAC;
 643
 644 ASM_REWRITE_TAC[]
 645 ;
 646
 647
 648 MP_TAC(REAL_ARITH`norm (v (x+k-1)) = &2 \/ ~(norm ((v:num->real^3) (x+k-1)) = &2)`)
 649 THEN RESA_TAC
 650 THEN MRESA_TAC J_EMPY_CASES_6[`s`;`x+k-1`]
 651 THEN DICH_TAC 0
 652 THEN REWRITE_TAC[SET_RULE`(a = {})<=> !i. ~ (a i)`]
 653 THEN STRIP_TAC
 654 THEN SUBGOAL_THEN`!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (x+k-1)) V' E'`
 655 ASSUME_TAC
 656 ;
 657
 658
 659 REPEAT RESA_TAC
 660 THEN DICH_TAC (37-23)
 661 THEN RESA_TAC
 662 THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
 663 THEN REPLICATE_TAC (48-35) (REMOVE_ASSUM_TAC)
 664 THEN MRESA_TAC WL_IN_V[`x+k-1`;`v:num->real^3`]
 665 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~((6-1) MOD 6= 3 MOD 6) /\ ~((6-1) MOD 6= 0 MOD 6)`)
 666 THEN RESA_TAC
 667 THEN THAYTHES_TAC 6[`(v:num->real^3) (x+k-1)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
 668 THEN POP_ASSUM MP_TAC
 669 THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT]
 670 THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
 671 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
 672 THEN RESA_TAC
 673 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
 674 THEN MRESAS_TAC Jkqewgv.JKQEWGV3[`s`;`v`;`v (x+k-1)`;`v1`][LET_DEF;LET_END_DEF;]
 675 THEN DICH_TAC 0
 676 THEN ONCE_REWRITE_TAC[Local_lemmas.LUNAR_COMM]
 677 THEN ASM_REWRITE_TAC[ADD1]
 678 THEN MP_TAC PI_WORKS
 679 THEN REAL_ARITH_TAC;
 680
 681
 682 SUBGOAL_THEN`(!i. scs_diag k (x+k-1) i
 683            ==> scs_a_v39 s (x+k-1) i < dist (v (x+k-1),(v:num->real^3) i))`ASSUME_TAC
 684 ;
 685
 686 GEN_TAC
 687 THEN STRIP_TAC
 688 THEN THAYTHE_TAC (36-9)[`x+k-1`;`i`]
 689 THEN POP_ASSUM MP_TAC
 690 THEN POP_ASSUM MP_TAC
 691 THEN REAL_ARITH_TAC
 692 ;
 693
 694
 695
 696
 697 SUBGOAL_THEN`azim (vec 0) ((v:num->real^3) (x + k - 1)) (v x) (v (x + k - 1+k-1)) = pi`ASSUME_TAC
 698 ;
 699
 700
 701 REMOVE_ASSUM_TAC
 702 THEN REMOVE_ASSUM_TAC
 703 THEN REMOVE_ASSUM_TAC
 704 THEN MRESA_TAC Local_lemmas.HKIRPEP[`E`;`w`;`FF`;`v'`;`V`]
 705 THEN DICH_TAC 0
 706 THEN DICH_TAC(33-23)
 707 THEN ASM_REWRITE_TAC[]
 708 THEN STRIP_TAC
 709 THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]
 710 THEN ASSUME_TAC th)
 711 THEN REWRITE_TAC[]
 712 THEN STRIP_TAC
 713 THEN REPLICATE_TAC (47-34) (REMOVE_ASSUM_TAC)
 714 THEN MRESA_TAC WL_IN_V[`x+k-1`;`v:num->real^3`]
 715 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~((6-1) MOD 6= 3 MOD 6) /\ ~((6-1) MOD 6= 0 MOD 6)`)
 716 THEN RESA_TAC
 717 THEN THAYTHES_TAC 6[`(v:num->real^3) (x+k-1)`][DIFF;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a= b\/ a=c`;BB_VV_FUN_EQ;DE_MORGAN_THM;Qknvmlb.SUC_MOD_NOT_EQ;]
 718 THEN POP_ASSUM MP_TAC
 719 THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT]
 720 THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
 721 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
 722 THEN RESA_TAC
 723 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
 724 THEN ASM_SIMP_TAC[ADD1;Ocbicby.MOD_EQ_MOD_SHIFT;interior_angle1;GSYM ivs_rho_node1]
 725 THEN MRESAL_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (x+k-1)`;`v`;`x+k-1`;`k`][ARITH_RULE`(x + k - 1) + 1= SUC (x + k - 1)`];
 726
 727
 728
 729 SUBGOAL_THEN`~collinear {vec 0, (v:num->real^3) x, v (x + k - 1 + k - 1)}`
 730 ASSUME_TAC
 731 ;
 732
 733
 734 DICH_TAC (37-23)
 735 THEN RESA_TAC
 736 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ ~((6-1+6-1) MOD 6= 3 MOD 6)/\ ~((6-1+6-1) MOD 6= 0 MOD 6)`)
 737 THEN RESA_TAC
 738 THEN MRESA_TAC Lunar_deform.LOCAL_CONVEX_NOT_COLLINEAR[`FF`;`E`;`V`;`w`;`v'`]
 739 THEN MATCH_DICH_TAC 0
 740 THEN MRESAS_TAC WL_IN_V[`x+k-1+k-1`;`v:num->real^3`][BB_VV_FUN_EQ;ARITH_RULE`SUC (SUC x)=x+2`;Ocbicby.MOD_EQ_MOD_SHIFT]
 741 THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
 742 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
 743 THEN RESA_TAC
 744 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT];
 745
 746
 747
 748
 749 SUBGOAL_THEN`(v:num->real^3) (x + k - 1) IN aff_gt {vec 0} {v x, v (x + k - 1 + k - 1)}`
 750 ASSUME_TAC;
 751
 752
 753 DICH_TAC (38-23)
 754 THEN RESA_TAC
 755 THEN MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(6=0)/\ (0 MOD 6= (3+3) MOD 6)/\ ~(1 MOD 6= 3 MOD 6)/\ ~(6<=3)/\ ~((3+1) MOD 6= (6-1) MOD 6)`)
 756 THEN RESA_TAC
 757 THEN MRESA_TAC Odxlstcv2.CARD_V_EQ_SCS_K1[`s`;`v`;`V`;`k`]
 758 THEN MRESA_TAC Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME[`V`;`E`;`k`;`s`;`FF`;`v (x+3)`;`v`;`x+3`]
 759 THEN MRESA_TAC Local_lemmas.AFF_IVS_RHO_NODE_EQQ[`V`;`E`;`w`;`FF`;`v'`]
 760 THEN MRESAS_TAC Local_lemmas.LUNAR_IMP_HALF_CIRCLE_SUBSET_AFF_GT[`E`;`V`;`v'`;`FF`;`w`][BB_VV_FUN_EQ;Local_lemmas.LUNAR_COMM;]
 761 THEN POP_ASSUM MP_TAC
 762 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th] THEN ASSUME_TAC(SYM th))
 763 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v x`;`v`;`x`;`k`]
 764 THEN DICH_TAC 2
 765 THEN ASM_SIMP_TAC[BB_VV_FUN_EQ;]
 766 THEN ONCE_REWRITE_TAC[ARITH_RULE`i+x+3=x+i+3:num`]
 767 THEN MP_TAC(SET_RULE`x= x+0==> x MOD k= (x+0) MOD k`)
 768 THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o DEPTH_CONV)[ARITH_RULE`x+0=x`]
 769 THEN RESA_TAC
 770 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT]
 771 THEN ONCE_REWRITE_TAC[ARITH_RULE`i+3=3+i:num`]
 772 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;MOD_LT]
 773 THEN STRIP_TAC
 774 THEN ASM_REWRITE_TAC[ARITH_RULE`0< l/\ l<3<=> l=1\/ l=2`;SET_RULE`{v (x + 3 + l) | l = 1 \/ l = 2} = {v (x+3+1), v(x+3+2)}`;SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`;ARITH_RULE` 3+2=6-1`]
 775 THEN MP_TAC(ARITH_RULE`x+6-1+6-1= 1*6+(x+3+1)`)
 776 THEN RESA_TAC
 777 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`1 * k + x + 3 + 1`;`v:num->real^3`;`(1 * k + x + 3 + 1) MOD k:num`][MOD_REFL;MOD_MULT_ADD]
 778 THEN MRESAS_TAC CHANGE_W_IN_BBS_MOD_IS_SCS[`s`;`(x + 3 + 1) MOD k`;`v:num->real^3`;`(x + 3 + 1):num`][MOD_REFL;MOD_MULT_ADD]
 779 THEN STRIP_TAC
 780 THEN MP_TAC(SET_RULE`v (x + 3+1) IN aff_gt {vec 0, v x} {v (x +k- 1)}
 781 /\  aff_gt {vec 0, v x} {v (x +k- 1)} SUBSET aff_ge {vec 0, v x} {v (x + k-1)}
 782 ==> v (x + 3+1) IN aff_ge {vec 0, (v:num->real^3) x} {v (x + k-1)}`)
 783 THEN ASM_REWRITE_TAC[AFF_GT_SUBSET_AFF_GE]
 784 THEN STRIP_TAC
 785 THEN DICH_TAC (59-37)
 786 THEN RESA_TAC
 787 THEN MRESA_TAC WL_IN_V[`x+k-1`;`v:num->real^3`]
 788 THEN MRESA_TAC WL_IN_V[`x+3+1`;`v:num->real^3`]
 789 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (x+k-1)`;`v`;`x+k-1`;`k`]
 790 THEN MRESAL_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2[`E`;`V`;`FF`;`v (x+k-1)`][GSYM ADD1]
 791 THEN DICH_TAC 0
 792 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
 793 THEN RESA_TAC
 794 THEN MRESAL_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`v x`;`v (x+k-1)`;`v (x+3+1)`][ADD1]
 795 THEN MRESAL_TAC WL_IN_E[`x+k-1`;`v:num->real^3`][]
 796 THEN DICH_TAC 0
 797 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
 798 THEN RESA_TAC
 799 THEN MRESA_TAC th3[`vec 0:real^3`;`v x`;`v (x+3+1)`]
 800 THEN MRESAS_TAC Planarity.POINT_IN_AFF_GE_IMP_IN_EDGE[`vec 0:real^3`;`V`;`E`;`v(x)`;`v (x+k-1)`;`v (x+3+1)`][SET_RULE`a IN{b,c}<=> a=b\/ a=c`;Ocbicby.MOD_EQ_MOD_SHIFT;BB_VV_FUN_EQ];
 801
 802 MRESAL_TAC IMJXPHRv2[`s`;`k`;`v`;`x+k-1`][dist]
 803 ;
 804
 805
 806 POP_ASSUM MP_TAC
 807 THEN POP_ASSUM MP_TAC
 808 THEN REWRITE_TAC[GSYM dist]
 809 THEN DISCH_TAC
 810 THEN ONCE_REWRITE_TAC[DIST_SYM]
 811 THEN DISCH_TAC
 812 ;
 813
 814
 815
 816 MRESA_TAC BB_F_SUC_PRE[`s`;`v:num->real^3`;`x`]
 817 THEN MP_TAC Axjrpnc.DIST_LE_2h0_IN_CASES_6
 818 THEN RESA_TAC
 819 THEN THAYTHEL_ASM_TAC 0[`x`][GSYM dist]
 820 THEN THAYTHEL_TAC 0[`x+k-1`][GSYM dist]
 821 THEN POP_ASSUM MP_TAC
 822 THEN REWRITE_TAC[]
 823 THEN ONCE_REWRITE_TAC[DIST_SYM]
 824 THEN STRIP_TAC;
 825
 826 SUBGOAL_THEN`      cstab <= dist (v (SUC x),(v:num->real^3) (x + k - 1))`ASSUME_TAC
 827 ;
 828
 829 MP_TAC(ARITH_RULE`1<6/\ 2<6/\ ~(1 MOD 6=6 MOD 6)/\ (x+6-1)+1=x+6/\ ~(1 MOD 6= (6-1) MOD 6)/\ ~(6=0)/\ ~((2) MOD 6= (6-1) MOD 6)`)
 830 THEN RESA_TAC
 831 THEN THAYTHES_TAC (41-10)[`SUC x`;`x+k-1`][scs_diag;ADD1;ARITH_RULE`(i+1)+1= i+2`;Ocbicby.MOD_EQ_MOD_SHIFT]
 832 THEN POP_ASSUM MP_TAC
 833 THEN REAL_ARITH_TAC;
 834
 835
 836 DICH_TAC (35-24)
 837 THEN RESA_TAC
 838 THEN MRESAL_TAC JKQEWGV3[`s`;`v`;`v'`;`w`][LET_DEF;LET_END_DEF;];
 839
 840
 841 DICH_TAC 1
 842 THEN STRIP_TAC
 843 THEN REMOVE_ASSUM_TAC
 844 THEN MP_TAC SYNQIWN
 845 THEN RESA_TAC
 846 THEN THAYTHE_TAC 0[`s`;`v`;`x`;`k`]
 847 THEN DICH_TAC 0
 848 THEN DICH_TAC (35-30)
 849 THEN DICH_TAC (34-29)
 850 THEN RESA_TAC
 851 THEN RESA_TAC
 852 THEN DICH_TAC 2
 853 THEN REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;ADD1]
 854 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (x)`;`v`;`x`;`k`]
 855 THEN REAL_ARITH_TAC;
 856
 857
 858
 859
 860
 861 ]);;
 862
 863
 864
 865
 866
 867
 868  end;;
 869
 870
 871 (*
 872 let check_completeness_claimA_concl =
 873   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
 874 *)
 875
 876
 877
 878