text_formalization/local/VASYYAU.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 Vasyyau = struct
  16
  17
  18
  19 open Polyhedron;;
  20 open Sphere;;
  21 open Topology;;
  22 open Fan_misc;;
  23 open Planarity;;
  24 open Conforming;;
  25 open Hypermap;;
  26 open Fan;;
  27 open Topology;;
  28 open Wrgcvdr_cizmrrh;;
  29 open Local_lemmas;;
  30 open Collect_geom;;
  31 open Dih2k_hypermap;;
  32 open Wjscpro;;
  33 open Tecoxbm;;
  34 open Hdplygy;;
  35 open Nkezbfc_local;;
  36 open Flyspeck_constants;;
  37 open Gbycpxs;;
  38 open Pcrttid;;
  39 open Local_lemmas1;;
  40 open Pack_defs;;
  41
  42 open Hales_tactic;;
  43
  44 open Appendix;;
  45
  46
  47
  48
  49
  50 open Hypermap;;
  51 open Fan;;
  52 open Wrgcvdr_cizmrrh;;
  53 open Local_lemmas;;
  54 open Flyspeck_constants;;
  55 open Pack_defs;;
  56
  57 open Hales_tactic;;
  58
  59 open Appendix;;
  60
  61
  62 open Zithlqn;;
  63
  64
  65 open Xwitccn;;
  66
  67 open Ayqjtmd;;
  68
  69 open Jkqewgv;;
  70
  71
  72 open Mtuwlun;;
  73
  74
  75 open Uxckfpe;;
  76 open Sgtrnaf;;
  77
  78 open Yxionxl;;
  79
  80 open Qknvmlb;;
  81 open Odxlstcv2;;
  82
  83 open Yxionxl2;;
  84 open Eyypqdw;;
  85 open Ocbicby;;
  86 open Imjxphr;;
  87 open Nuxcoea;;
  88 open Aursipd;;
  89 open Cuxvzoz;;
  90 open Rrcwnsj;;
  91 open Tfitskc;;
  92 open Hexagons;;
  93 open Otmtotj;;
  94 open Hijqaha;;
  95 open Cnicgsf;;
  96 open Ardbzye;;
  97 open Aueaheh;;
  98
  99
 100 let WGDHPPI= prove(`!s v.
 101     is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s ==>
 102     CARD { i | i < scs_k_v39 s /\ scs_is_str s v i} <= 1`,
 103 REPEAT RESA_TAC
 104 THEN MRESA_TAC GSXRFWM[`s`;`v`]
 105 THEN MRESAL_TAC Aursipd.AURSIPD[`s`;`v`][ARITH_RULE`3<4`]
 106 THEN DICH_TAC 0
 107 THEN ARITH_TAC);;
 108
 109 (************************************)
 110
 111 let DIST_V_IN_BB_LE_C=prove(`   scs_b_v39 s i (SUC i) <= c/\
 112   BBs_v39 s v
 113 ==> dist (v i, v (SUC i))<= c`,
 114 REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;dist]
 115 THEN RESA_TAC
 116 THEN THAYTHE_TAC 1[`i`;`SUC i`]
 117 THEN ASM_TAC
 118 THEN REAL_ARITH_TAC);;
 119
 120
 121 let arclength_lt_1553 = prove_by_refinement(
 122   `&2 * arclength (&2) (&2) (&2 * h0) < arclength (&2) (&2)
 123 (sqrt(#15.53))`,
 124   (* {{{ proof *)
 125   [
 126   REPEAT (GMATCH_SIMP_TAC Compute_2158872499.ATN_UPS_X_BREAKDOWN1);
 127   GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
 128   REPEAT (GMATCH_SIMP_TAC REAL_LT_MUL_EQ);
 129   REWRITE_TAC[arith `x + &2 - &2 = x`];
 130   REWRITE_TAC[Sphere.h0];
 131   TYPIFY `#3.9 < sqrt (#15.53) /\ sqrt(#15.53) < #3.95` (C
 132 SUBGOAL_THEN ASSUME_TAC);
 133     GMATCH_SIMP_TAC REAL_LT_RSQRT;
 134     CONJ_TAC;
 135       BY(REAL_ARITH_TAC);
 136     MATCH_MP_TAC REAL_LT_LSQRT;
 137     BY(REAL_ARITH_TAC);
 138   TYPIFY_GOAL_THEN `&0 < &2 + &2 *  #1.26 - &2 /\  &0 < &2 + &2 - &2 *
 139  #1.26 /\ &0 < &2 + &2 + &2 *  #1.26 /\ &0 < &2 + sqrt  #15.53 - &2 /\
 140 &0 < &2 + &2 - sqrt  #15.53 /\ &0 < &2 + &2 + sqrt  #15.53 /\ &0 <
 141 sqrt  #15.53 /\ &0 < &2 *  #1.26` (unlist REWRITE_TAC);
 142     BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
 143   MP_TAC (Flyspeck_constants.calc `&2 * (pi / &2 +  atn  (((&2 *
 144 #1.26) * &2 *  #1.26 - &2 * &2 - &2 * &2) /   sqrt   ((&2 + &2 + &2 *
 145  #1.26) *    (&2 + &2 - &2 *  #1.26) *    (&2 + &2 *  #1.26 - &2) *
 146  &2 *     #1.26))) < pi / &2 + atn ((sqrt  #15.53 * sqrt  #15.53 - &2
 147 * &2 - &2 * &2) /  sqrt  ((&2 + &2 + sqrt  #15.53) *   (&2 + &2 - sqrt
 148  #15.53) *   (&2 + sqrt  #15.53 - &2) *   sqrt  #15.53))` );
 149   BY(REWRITE_TAC[])
 150   ]);;
 151   (* }}} *)
 152
 153
 154   let ASSWPOW= prove_by_refinement( `!s v i.
 155     is_scs_v39 s /\ v IN MMs_v39 s /\ scs_k_v39 s = 4 /\ scs_basic_v39 s /\
 156     scs_b_v39 s i (i+1) <= &2 * h0 /\  scs_b_v39 s (i+1) (i+2) <= &2 * h0
 157     ==>    xrr (norm (v i)) (norm(v(i+2))) (dist(v i,v(i+2))) <= #15.53 `,
 158 [
 159 REWRITE_TAC[IN;GSYM ADD1;ARITH_RULE`i+2=SUC(SUC i)`]
 160 THEN REPEAT GEN_TAC
 161 THEN ABBREV_TAC`k= scs_k_v39 s`
 162 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
 163 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
 164 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
 165 THEN REPEAT RESA_TAC
 166 THEN ASSUME_TAC(ARITH_RULE`3<4`)
 167 THEN MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
 168 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
 169 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`k:num`;`s`;`v`]
 170 THEN MP_TAC Local_lemmas.CVLF_LF_F
 171 THEN RESA_TAC;
 172
 173
 174
 175
 176
 177 MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`i`]
 178 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC i`]
 179 THEN MRESA_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`SUC(SUC i)`]
 180 THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`i`]
 181 THEN MRESA_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`SUC i`]
 182 THEN MRESAL_TAC DIST_V_IN_BB_LE_C[`s`;`v`;`i`;`&2*h0`][dist]
 183 THEN MRESAL_TAC DIST_V_IN_BB_LE_C[`s`;`v`;`SUC i`;`&2*h0`][dist]
 184 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v i`;`v (SUC i)`;`&2* h0`][dist;]
 185 THEN POP_ASSUM MP_TAC
 186 THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
 187 THEN REWRITE_TAC[GSYM h0]
 188 THEN STRIP_TAC
 189 THEN MRESAL_TAC Ppbtydq.OIQKKEP[`v (SUC i)`;`v (SUC(SUC i))`;`&2* h0`][dist;]
 190 THEN POP_ASSUM MP_TAC
 191 THEN REWRITE_TAC[h0;REAL_ARITH`&2 * #1.26 < &4`]
 192 THEN REWRITE_TAC[GSYM h0]
 193 THEN STRIP_TAC
 194 THEN DICH_TAC (26-18)
 195 THEN DICH_TAC (25-18)
 196 THEN DICH_TAC (24-18)
 197 THEN REWRITE_TAC[Ckqowsa_3_points.in_ball_annulus]
 198 THEN REPEAT STRIP_TAC
 199 THEN MRESA_TAC Trigonometry2.ARCV_INEQUALTY[`vec 0:real^3`;`v i`;`v (SUC (SUC i))`;`v(SUC i)`]
 200 THEN MP_TAC(REAL_ARITH`arcV (vec 0) (v (i)) (v (SUC (i))) <= arclength (&2) (&2) (&2 * h0)
 201 /\ arcV (vec 0) ((v:num->real^3) (SUC (i))) (v (SUC (SUC (i)))) <=
 202       arclength (&2) (&2) (&2 * h0)
 203 /\ &2 * arclength (&2) (&2) (&2 * h0) < arclength (&2) (&2)
 204 (sqrt(#15.53))
 205 /\ arcV (vec 0) (v i) (v (SUC (SUC i))) <=
 206       arcV (vec 0) (v i) (v (SUC i)) +
 207       arcV (vec 0) (v (SUC i)) (v (SUC (SUC i)))
 208 ==>arcV (vec 0) (v i) (v (SUC (SUC i)))
 209  < arclength (&2) (&2)
 210 (sqrt(#15.53))`)
 211 THEN ASM_SIMP_TAC[arclength_lt_1553]
 212 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 213 THEN MRESAS_TAC Planarity.IMP_NORM_FAN[`v (i+0)`;`v(i+2):real^3`][VECTOR_ARITH`A- vec 0=A:real^3`;ARITH_RULE`~(4=0)/\ ~(0 MOD 4 = 2 MOD 4)`;Ocbicby.MOD_EQ_MOD_SHIFT]
 214 THEN MRESA_TAC WL_IN_V[`i+0`;`v:num->real^3`]
 215 THEN MRESA_TAC WL_IN_V[`i+2`;`v:num->real^3`]
 216 THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN;scs_generic]
 217 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (i+0)`;`v (i+2)`;`V`]
 218 THEN THAYTHES_TAC 0[`v (i+0)`;`v (i+2)`][SET_RULE`a IN {a,b}`;ARITH_RULE`~(4=0)/\ ~(0 MOD 4 = 2 MOD 4)`;Ocbicby.MOD_EQ_MOD_SHIFT]
 219 THEN ASM_TAC
 220 THEN REWRITE_TAC[ARITH_RULE`i+0=i/\ i+2=SUC(SUC i)`]
 221 THEN REPEAT RESA_TAC
 222 THEN ABBREV_TAC`u=(v:num->real^3) i`
 223 THEN ABBREV_TAC`w=(v:num->real^3) (SUC (SUC i))`
 224 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`u`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A:real^3`]
 225 THEN MRESAL_TAC Planarity.IMP_NORM_FAN[`w`;`vec 0:real^3`][VECTOR_ARITH`A- vec 0=A:real^3`]
 226 THEN MRESAL_TAC Collect_geom2.NOT_COL_EQ_UPS_X_POS[`vec 0:real^3`;`u`;`w`][dist;VECTOR_ARITH`vec 0- a= --a:real^3`;NORM_NEG]
 227 THEN MRESAL_TAC arclength_xrr[`norm (u)`;`norm w`;`norm (u-w)`][REAL_ARITH`a*a= a pow 2`]
 228 THEN MRESA_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`u`;`w`]
 229 THEN DICH_TAC (62-45)
 230 THEN ASM_SIMP_TAC[dist;VECTOR_ARITH`vec 0- a= --a:real^3`;NORM_NEG]
 231 THEN MRESAL_TAC arclength_xrr[`&2`;`&2`;`sqrt #15.53`][REAL_ARITH`a*a= a pow 2/\ &0< &2`]
 232 THEN DICH_TAC 0;
 233
 234
 235
 236
 237
 238   TYPIFY `#3.9 < sqrt (#15.53) /\ sqrt(#15.53) < #3.95` (C
 239 SUBGOAL_THEN ASSUME_TAC);
 240
 241     GMATCH_SIMP_TAC REAL_LT_RSQRT;
 242     CONJ_TAC;
 243       BY(REAL_ARITH_TAC);
 244
 245     MATCH_MP_TAC REAL_LT_LSQRT;
 246
 247     BY(REAL_ARITH_TAC);
 248
 249   TYPIFY_GOAL_THEN `&0 < &2 + &2 *  #1.26 - &2 /\  &0 < &2 + &2 - &2 *
 250  #1.26 /\ &0 < &2 + &2 + &2 *  #1.26 /\ &0 < &2 + sqrt  #15.53 - &2 /\
 251 &0 < &2 + &2 - sqrt  #15.53 /\ &0 < &2 + &2 + sqrt  #15.53 /\ &0 <
 252 sqrt  #15.53 /\ &0 < &2 *  #1.26` (unlist REWRITE_TAC);
 253     BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
 254 MP_TAC(REAL_ARITH`#3.9 < sqrt #15.53==> &0 < sqrt #15.53`)
 255 THEN RESA_TAC
 256 THEN MRESAL_TAC SQRT_POW2[`#15.53`][REAL_ARITH`&0<= #15.53`]
 257 THEN REWRITE_TAC[ups_x;REAL_ARITH`&0 <
 258   --(&2 pow 2) * &2 pow 2 - &2 pow 2 * &2 pow 2 - #15.53 * #15.53 +
 259   &2 * &2 pow 2 * #15.53 +
 260   &2 * &2 pow 2 * &2 pow 2 +
 261   &2 * &2 pow 2 * #15.53`]
 262 THEN RESA_TAC
 263 THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`norm u`;`norm w`;`norm (u-w)`][REAL_ARITH`a*a= a pow 2`]
 264 THEN MP_TAC(REAL_ARITH`&0 < xrr (norm u) (norm w) (norm (u-w))/\
 265 xrr (norm u) (norm w) (norm (u-w)) < &16
 266 ==> abs (&1 - xrr (norm u) (norm w) (norm (u-w:real^3)) / &8) <= &1`)
 267 THEN RESA_TAC
 268 THEN SUBGOAL_THEN`abs (&1 - xrr (&2) (&2) (sqrt #15.53) / &8) <= &1`ASSUME_TAC
 269 ;
 270
 271
 272
 273 ASM_REWRITE_TAC[xrr;REAL_ARITH`a*a= a pow 2`]
 274 THEN REAL_ARITH_TAC;
 275
 276
 277 MRESAL_TAC ACS_MONO_LT_EQ[`&1 - xrr (norm u) (norm w) (norm (u-w)) / &8`;`&1 - xrr (&2) (&2) (sqrt #15.53) / &8`][REAL_ARITH`&1- a/ &8< &1- b/ &8<=> b<a`]
 278 THEN MATCH_MP_TAC(REAL_ARITH`a<=b==>(c<a==>c<=b)`)
 279 ;
 280
 281
 282
 283 ASM_REWRITE_TAC[xrr;REAL_ARITH`a*a= a pow 2`]
 284 THEN REAL_ARITH_TAC;
 285
 286 ]);;
 287
 288
 289
 290
 291
 292 let YEBWJNG=  prove_by_refinement(
 293  `main_nonlinear_terminal_v11 ==>
 294   (!s v p.
 295     is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\
 296     (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
 297     (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
 298        (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
 299     ~scs_is_str s v p /\ ~scs_is_str s v (p+1) /\ scs_a_v39 s p (p+1) = &2
 300     ==> dist(v p,v(p+1)) = &2)`,
 301 [
 302 REWRITE_TAC[IN;scs_is_str]
 303 THEN REPEAT RESA_TAC
 304 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
 305 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
 306 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
 307 THEN ASM_TAC
 308 THEN REPEAT RESA_TAC
 309 THEN MP_TAC Cuxvzoz.CUXVZOZ
 310 THEN RESA_TAC
 311 THEN MATCH_DICH_TAC 0
 312 THEN EXISTS_TAC`s:scs_v39`
 313 THEN EXISTS_TAC`FF:real^3#real^3->bool`
 314 THEN EXISTS_TAC`4`
 315 THEN ASSUME_TAC(ARITH_RULE`3<4/\ 1<4/\ ~(4=0)`)
 316 THEN ASM_SIMP_TAC[]
 317 THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN]
 318 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1]
 319 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 320 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`s`;`v`]
 321 THEN MP_TAC Local_lemmas.CVLF_LF_F
 322 THEN RESA_TAC
 323 THEN MP_TAC SCS_DIAG_A_LE_DIST
 324 THEN RESA_TAC
 325 THEN ASM_SIMP_TAC[]
 326 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
 327 THEN MRESA_TAC WL_IN_V[`SUC p`;`v:num->real^3`]
 328 THEN MRESA_TAC WL_IN_V[`p+4-1`;`v:num->real^3`]
 329 THEN MRESA_TAC WL_IN_V[`SUC p+4-1`;`v:num->real^3`]
 330 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
 331 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][GSYM ADD1]
 332 THEN THAYTHE_TAC 0[`v (p+4-1)`]
 333 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 334 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) <= pi
 335 /\ ~(azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) = pi)
 336 ==> azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) < pi`)
 337 THEN RESA_TAC
 338 THEN REWRITE_TAC[ADD1]
 339 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+1)`;`v`;`p+1`;`4`]
 340 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][GSYM ADD1]
 341 THEN THAYTHE_TAC 0[`v (SUC p+4-1)`]
 342 THEN DICH_TAC (31-8)
 343 THEN REWRITE_TAC[GSYM ADD1]
 344 THEN STRIP_TAC
 345 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) <= pi
 346 /\ ~(azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) = pi)
 347 ==> azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) < pi`)
 348 THEN RESA_TAC
 349 THEN THAYTHES_TAC(32-26)[`1 * 4 + p`;`p`][MOD_MULT_ADD]
 350 THEN MRESAL_TAC Axjrpnc.DIST_EDGE_IN_BB_LE_2[`s`;`v`;`p+3`][ARITH_RULE`SUC(i+3)=1*4+i/\ p+4-1=p+3`;GSYM dist]
 351 THEN SUBGOAL_THEN`!i. scs_b_v39 s i (SUC(i)) <= cstab`ASSUME_TAC;
 352
 353 GEN_TAC
 354 THEN THAYTHE_TAC (33-6)[`i`]
 355 THEN DICH_TAC 0
 356 THEN REWRITE_TAC[cstab;h0;ADD1]
 357 THEN REAL_ARITH_TAC;
 358
 359 MP_TAC Axjrpnc.NORM_V_IN_BB_LE_CSTAB
 360 THEN RESA_TAC
 361 THEN REWRITE_TAC[GSYM dist]
 362 THEN THAYTHES_TAC 0[`p+3`][ARITH_RULE`SUC(i+3)=1*4+i/\ p+4-1=p+3`;GSYM dist]
 363 THEN ONCE_REWRITE_TAC[SET_RULE`A/\B<=> B/\A`]
 364 THEN STRIP_TAC;
 365
 366 THAYTHE_TAC (35-6)[`p`];
 367
 368 DICH_TAC 0
 369 THEN REWRITE_TAC[ADD1]
 370 THEN REAL_ARITH_TAC;
 371
 372 DICH_TAC 1
 373 THEN REWRITE_TAC[h0]
 374 THEN REAL_ARITH_TAC;
 375
 376 MRESA_TAC Ardbzye.SCS_DIAG_4_ADD2[`p`]
 377 THEN THAYTHE_TAC (36-5)[`p+1`;`p+3`]
 378 THEN ONCE_REWRITE_TAC[DIST_SYM]
 379 THEN DICH_TAC 1
 380 THEN REWRITE_TAC[ADD1;cstab]
 381 THEN REAL_ARITH_TAC]);;
 382
 383 (************************************)
 384
 385
 386 let NOT_MOD_4_CASES=prove(`~(i MOD 4 = (p + 2) MOD 4)<=> i MOD 4 = p MOD 4\/  i MOD 4 = (p + 1) MOD 4
 387 \/ i MOD 4 = (p + 3) MOD 4`,
 388 MRESAL_TAC MOD_ADD_MOD[`p`;`1`;`4`][ARITH_RULE`~(4=0)`]
 389 THEN SYM_ASSUM_TAC
 390 THEN MRESAL_TAC MOD_ADD_MOD[`p`;`2`;`4`][ARITH_RULE`~(4=0)`]
 391 THEN SYM_ASSUM_TAC
 392 THEN MRESAL_TAC MOD_ADD_MOD[`p`;`3`;`4`][ARITH_RULE`~(4=0)`]
 393 THEN SYM_ASSUM_TAC
 394 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
 395 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
 396 THEN RESA_TAC
 397 THEN MP_TAC(ARITH_RULE`p MOD 4<4==> p MOD 4=0\/ p MOD 4=1\/ p MOD 4=2\/ p MOD 4=3`)
 398 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
 399 THEN RESA_TAC
 400 THEN ARITH_TAC);;
 401
 402
 403
 404
 405 let NOT_MOD_4_CASES_3=prove(`~(i MOD 4 = (p + 3) MOD 4)<=> i MOD 4 = p MOD 4\/  i MOD 4 = (p + 1) MOD 4
 406 \/ i MOD 4 = (p + 2) MOD 4`,
 407 MRESAL_TAC MOD_ADD_MOD[`p`;`1`;`4`][ARITH_RULE`~(4=0)`]
 408 THEN SYM_ASSUM_TAC
 409 THEN MRESAL_TAC MOD_ADD_MOD[`p`;`2`;`4`][ARITH_RULE`~(4=0)`]
 410 THEN SYM_ASSUM_TAC
 411 THEN MRESAL_TAC MOD_ADD_MOD[`p`;`3`;`4`][ARITH_RULE`~(4=0)`]
 412 THEN SYM_ASSUM_TAC
 413 THEN MP_TAC(ARITH_RULE`i MOD 4<4==> i MOD 4=0\/ i MOD 4=1\/ i MOD 4=2\/ i MOD 4=3`)
 414 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
 415 THEN RESA_TAC
 416 THEN MP_TAC(ARITH_RULE`p MOD 4<4==> p MOD 4=0\/ p MOD 4=1\/ p MOD 4=2\/ p MOD 4=3`)
 417 THEN ASM_SIMP_TAC[DIVISION;ARITH_RULE`~(4=0)`]
 418 THEN RESA_TAC
 419 THEN ARITH_TAC);;
 420
 421
 422
 423
 424 let SCS_STR_CASES_4= prove_by_refinement(`!s v.
 425     is_scs_v39 s /\ scs_k_v39 s = 4 /\ MMs_v39 s v /\
 426     ~scs_is_str s v p /\ ~scs_is_str s v (p+1)
 427 ==>  ~scs_is_str s v (p+3)\/  ~scs_is_str s v (p+2)`,
 428 [
 429 REPEAT RESA_TAC
 430 THEN REWRITE_TAC[GSYM DE_MORGAN_THM]
 431 THEN STRIP_TAC
 432 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ (4-1) MOD 4= 4-1/\ 1<4`)
 433 THEN MRESAL_TAC MMS_IMP_BBS[`s`;`v`][IN]
 434 THEN SUBGOAL_THEN`(p +3) MOD 4 IN { i | i < scs_k_v39 s /\ scs_is_str s (v:num->real^3) i}`
 435 ASSUME_TAC;
 436
 437 ASM_REWRITE_TAC[IN_ELIM_THM]
 438 THEN ASM_TAC
 439 THEN SIMP_TAC[scs_is_str;DIVISION;]
 440 THEN REPEAT RESA_TAC
 441 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 442 THEN THAYTHES_TAC 0[`(p+3) MOD 4`;`p+3:num`][MOD_REFL]
 443 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 444 THEN THAYTHES_TAC 0[`SUC((p+3) MOD 4)`;`SUC((p+3) MOD 4)MOD 4`][MOD_REFL;Hypermap.lemma_suc_mod]
 445 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 446 THEN THAYTHES_TAC 0[`SUC(p+3) MOD 4`;`SUC(p+3) `][MOD_REFL;Hypermap.lemma_suc_mod]
 447 THEN MRESA_TAC MOD_ADD_MOD[`p+3`;`4-1`;`4`]
 448 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 449 THEN THAYTHES_TAC 0[`(p + 3) MOD 4 + 4 - 1`;`((p + 3) MOD 4 + 4 - 1)MOD 4`][MOD_REFL;Hypermap.lemma_suc_mod]
 450 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 451 THEN THAYTHES_TAC 0[`((p + 3) + 4 - 1) MOD 4`;`(p + 3)  + 4 - 1`][MOD_REFL;Hypermap.lemma_suc_mod];
 452
 453
 454 SUBGOAL_THEN`(p +2) MOD 4 IN { i | i < scs_k_v39 s /\ scs_is_str s (v:num->real^3) i}`
 455 ASSUME_TAC;
 456
 457 ASM_REWRITE_TAC[IN_ELIM_THM]
 458 THEN ASM_TAC
 459 THEN SIMP_TAC[scs_is_str;DIVISION;]
 460 THEN REPEAT RESA_TAC
 461 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 462 THEN THAYTHES_TAC 0[`(p+2) MOD 4`;`p+2:num`][MOD_REFL]
 463 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 464 THEN THAYTHES_TAC 0[`SUC((p+2) MOD 4)`;`SUC((p+2) MOD 4)MOD 4`][MOD_REFL;Hypermap.lemma_suc_mod]
 465 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 466 THEN THAYTHES_TAC 0[`SUC(p+2) MOD 4`;`SUC(p+2) `][MOD_REFL;Hypermap.lemma_suc_mod]
 467 THEN MRESA_TAC MOD_ADD_MOD[`p+2`;`4-1`;`4`]
 468 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 469 THEN THAYTHES_TAC 0[`(p + 2) MOD 4 + 4 - 1`;`((p + 2) MOD 4 + 4 - 1)MOD 4`][MOD_REFL;Hypermap.lemma_suc_mod]
 470 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 471 THEN THAYTHES_TAC 0[`((p + 2) + 4 - 1) MOD 4`;`(p + 2)  + 4 - 1`][MOD_REFL;Hypermap.lemma_suc_mod];
 472
 473 MP_TAC(SET_RULE`(p + 3) MOD 4 IN {i | i < scs_k_v39 s /\ scs_is_str s v i}/\
 474 (p + 2) MOD 4 IN {i | i < scs_k_v39 s /\ scs_is_str s v i}
 475 ==> {(p + 3) MOD 4 ,(p + 2) MOD 4 } SUBSET {i | i < scs_k_v39 s /\ scs_is_str s v i}`)
 476 THEN RESA_TAC
 477 THEN MRESA_TAC Qknvmlb.SUC_MOD_NOT_EQ[`4`]
 478 THEN DICH_TAC 1
 479 THEN THAYTHEL_TAC 0[`p+2`][ARITH_RULE`SUC(p+2)=p+3`]
 480 THEN MRESA_TAC Planarity.CARD_2_FAN[`(p + 3) MOD 4`;`(p + 2) MOD 4`]
 481 THEN STRIP_TAC
 482 THEN SUBGOAL_THEN`FINITE {i | i < 4 /\ scs_is_str s v i}` ASSUME_TAC;
 483
 484 MATCH_MP_TAC FINITE_SUBSET
 485 THEN EXISTS_TAC`0..4`
 486 THEN ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_NUMSEG;FINITE_NUMSEG]
 487 THEN ARITH_TAC;
 488
 489 MRESA_TAC CARD_SUBSET[`{(p + 3) MOD 4, (p + 2) MOD 4}`;`{i | i < 4 /\ scs_is_str s v i}`]
 490 THEN POP_ASSUM MP_TAC
 491 THEN MRESAL_TAC WGDHPPI[`s`;`v`][IN]
 492 THEN DICH_TAC 0
 493 THEN ARITH_TAC]);;
 494
 495
 496
 497
 498 let NEHXMWH_concl=`main_nonlinear_terminal_v11 ==>
 499   (!s FF v p.
 500   IMAGE (\i. (v i,v (SUC i))) (:num) = FF /\
 501   is_scs_v39 s /\
 502   scs_k_v39 s = 4 /\
 503   MMs_v39 s v /\
 504   scs_basic_v39 s /\
 505   scs_generic v /\
 506   (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4 * h0 < scs_b_v39 s i j) /\
 507   (!i. ~(i MOD 4 = (p+2) MOD 4)  ==> interior_angle1 (vec 0) FF (v i) < pi)
 508   ==> (dist(v p,v(p+1)) = scs_a_v39 s p (p+1) \/ dist(v p,v(p+1)) = scs_b_v39 s p (p+1)))`;;
 509
 510 let NEHXMWH1_concl=`main_nonlinear_terminal_v11 ==>
 511   (!s FF v p.
 512   IMAGE (\i. (v i,v (SUC i))) (:num) = FF /\
 513   is_scs_v39 s /\
 514   scs_k_v39 s = 4 /\
 515   MMs_v39 s v /\
 516   scs_basic_v39 s /\
 517   scs_generic v /\
 518   (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4 * h0 < scs_b_v39 s i j) /\
 519   (!i. ~(i MOD 4 = (p+3) MOD 4)  ==> interior_angle1 (vec 0) FF (v i) < pi)
 520   ==> (dist(v p,v(p+1)) = scs_a_v39 s p (p+1) \/ dist(v p,v(p+1)) = scs_b_v39 s p (p+1)))`;;
 521
 522
 523
 524   let TUAPYYU_concl = `
 525 main_nonlinear_terminal_v11 ==>
 526 (!s v p.
 527     is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\
 528     (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
 529     (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
 530        (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
 531     ~scs_is_str s v p /\ ~scs_is_str s v (p+1)
 532     ==> dist(v p,v(p+1)) = scs_a_v39 s p (p+1) \/ dist(v p,v(p+1)) = scs_b_v39 s p (p+1))`;;
 533
 534
 535
 536 let TUAPYYU1= prove_by_refinement((mk_imp(NEHXMWH1_concl,mk_imp(NEHXMWH_concl, TUAPYYU_concl))),
 537 [
 538 REWRITE_TAC[IN;scs_is_str]
 539 THEN REPEAT RESA_TAC
 540 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
 541 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
 542 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
 543 THEN ASM_TAC
 544 THEN REPEAT RESA_TAC
 545 THEN ASSUME_TAC(ARITH_RULE`3<4/\ 1<4/\ ~(4=0)`)
 546 THEN ASM_SIMP_TAC[]
 547 THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN]
 548 THEN MRESAL_TAC SCS_STR_CASES_4[`p`;`s`;`v`][scs_is_str]
 549 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1]
 550 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 551 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`s`;`v`]
 552 THEN MP_TAC Local_lemmas.CVLF_LF_F
 553 THEN RESA_TAC
 554 THEN MP_TAC SCS_DIAG_A_LE_DIST
 555 THEN RESA_TAC
 556 THEN ASM_SIMP_TAC[]
 557 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
 558 THEN MRESA_TAC WL_IN_V[`SUC p`;`v:num->real^3`]
 559 THEN MRESA_TAC WL_IN_V[`p+4-1`;`v:num->real^3`]
 560 THEN MRESA_TAC WL_IN_V[`SUC p+4-1`;`v:num->real^3`]
 561 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
 562 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][GSYM ADD1]
 563 THEN THAYTHE_TAC 0[`v (p+4-1)`]
 564 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 565 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) <= pi
 566 /\ ~(azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) = pi)
 567 ==> azim (vec 0) (v p) (v (SUC p)) (v (p + 4 - 1)) < pi`)
 568 THEN RESA_TAC
 569 THEN REWRITE_TAC[ADD1]
 570 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+1)`;`v`;`p+1`;`4`]
 571 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][GSYM ADD1]
 572 THEN THAYTHE_TAC 0[`v (SUC p+4-1)`]
 573 THEN DICH_TAC (32-9)
 574 THEN REWRITE_TAC[GSYM ADD1]
 575 THEN STRIP_TAC
 576 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) <= pi
 577 /\ ~(azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) = pi)
 578 ==> azim (vec 0) (v (SUC p)) (v (SUC (SUC p))) (v (SUC p + 4 - 1)) < pi`)
 579 THEN RESA_TAC;
 580
 581 DICH_TAC (33)
 582 THEN RESA_TAC
 583 THEN REWRITE_TAC[ADD1]
 584 THEN MATCH_DICH_TAC 0
 585 THEN EXISTS_TAC`FF:real^3#real^3->bool`
 586 THEN ASM_SIMP_TAC[]
 587 THEN ASM_REWRITE_TAC[NOT_MOD_4_CASES]
 588 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1]
 589 THEN REPEAT RESA_TAC;
 590
 591 THAYTHEL_TAC(32-25)[`i`;`p`][GSYM ADD1];
 592
 593
 594 THAYTHEL_TAC(32-25)[`i`;`p+1`][ADD1]
 595 THEN ASM_REWRITE_TAC[GSYM ADD1];
 596
 597
 598 MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+3)`;`v`;`p+3`;`4`]
 599 THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
 600 THEN MRESA_TAC WL_IN_V[`(p+3)+4-1`;`v:num->real^3`]
 601 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+3)`][GSYM ADD1]
 602 THEN THAYTHE_TAC 0[`v ((p+3)+4-1)`]
 603 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p+3)) (v (SUC (p+3))) (v ((p+3) + 4 - 1)) <= pi
 604 /\ ~(azim (vec 0) (v (p+3)) (v (SUC (p+3))) (v ((p+3) + 4 - 1)) = pi)
 605 ==> azim (vec 0) (v (p+3)) (v (SUC ((p+3)))) (v ((p+3) + 4 - 1)) < pi`)
 606 THEN RESA_TAC;
 607
 608 THAYTHEL_TAC(38-25)[`i`;`p+3`][GSYM ADD1];
 609
 610 DICH_TAC (34)
 611 THEN RESA_TAC
 612 THEN REWRITE_TAC[ADD1]
 613 THEN MATCH_DICH_TAC 0
 614 THEN EXISTS_TAC`FF:real^3#real^3->bool`
 615 THEN ASM_SIMP_TAC[]
 616 THEN ASM_REWRITE_TAC[NOT_MOD_4_CASES_3]
 617 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1]
 618 THEN REPEAT RESA_TAC;
 619
 620 THAYTHEL_TAC(32-25)[`i`;`p`][GSYM ADD1];
 621
 622
 623 THAYTHEL_TAC(32-25)[`i`;`p+1`][ADD1]
 624 THEN ASM_REWRITE_TAC[GSYM ADD1];
 625
 626
 627 MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+2)`;`v`;`p+2`;`4`]
 628 THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
 629 THEN MRESA_TAC WL_IN_V[`(p+2)+4-1`;`v:num->real^3`]
 630 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+2)`][GSYM ADD1]
 631 THEN THAYTHE_TAC 0[`v ((p+2)+4-1)`]
 632 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p+2)) (v (SUC (p+2))) (v ((p+2) + 4 - 1)) <= pi
 633 /\ ~(azim (vec 0) (v (p+2)) (v (SUC (p+2))) (v ((p+2) + 4 - 1)) = pi)
 634 ==> azim (vec 0) (v (p+2)) (v (SUC ((p+2)))) (v ((p+2) + 4 - 1)) < pi`)
 635 THEN RESA_TAC;
 636
 637 THAYTHEL_TAC(38-25)[`i`;`p+2`][GSYM ADD1]]);;
 638
 639
 640 let TUAPYYU=prove( TUAPYYU_concl,
 641 STRIP_TAC
 642 THEN MP_TAC TUAPYYU1
 643 THEN RESA_TAC
 644 THEN MP_TAC Jotswix.NEHXMWH
 645 THEN MP_TAC Jotswix.BZQNDMN
 646 THEN ASM_REWRITE_TAC[]);;
 647
 648
 649 (**************************)
 650
 651
 652 let SCS_M_CASES_4_LE_2=prove(`scs_k_v39 s = 4/\ is_scs_v39 s
 653 ==> CARD (scs_M s)<=2`,
 654 REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;scs_M]
 655 THEN RESA_TAC
 656 THEN DICH_TAC 0
 657 THEN ASM_REWRITE_TAC[]
 658 THEN ARITH_TAC);;
 659
 660
 661
 662 let SCS_M_CASES_4_EQ=prove(`scs_k_v39 s = 4/\ is_scs_v39 s /\ {p MOD 4,(p+3)MOD 4} SUBSET scs_M s
 663 ==> scs_M s={p MOD 4,(p+3)MOD 4}`,
 664 REPEAT STRIP_TAC
 665 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ ~(0 MOD 4 = 3 MOD 4)`)
 666 THEN MRESAS_TAC Planarity.CARD_2_FAN[`(p+0) MOD 4`;`(p+3) MOD 4`][Ocbicby.MOD_EQ_MOD_SHIFT]
 667 THEN DICH_TAC 0
 668 THEN REWRITE_TAC[ARITH_RULE`p+0=p`]
 669 THEN STRIP_TAC
 670 THEN MP_TAC SCS_M_CASES_4_LE_2
 671 THEN RESA_TAC
 672 THEN MP_TAC Jlxfdmj.FINITE_SCS_M
 673 THEN RESA_TAC
 674 THEN MRESA_TAC CARD_SUBSET_LE[`{p MOD 4, (p + 3) MOD 4}`;`scs_M s`]);;
 675
 676 let B_LE_2h0_SCS_M_4=prove(`scs_k_v39 s = 4/\ is_scs_v39 s /\ {p MOD 4,(p+3)MOD 4} SUBSET scs_M s
 677 ==> scs_b_v39 s (p+1) (p+2)<= &2*h0`,
 678 REPEAT STRIP_TAC
 679 THEN MP_TAC SCS_M_CASES_4_EQ
 680 THEN RESA_TAC
 681 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ ~(1 MOD 4 = 3 MOD 4)/\ 1<4`)
 682 THEN SUBGOAL_THEN`~((p+1) MOD 4 IN scs_M s)`ASSUME_TAC
 683 THENL[
 684 ASM_SIMP_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`;Ocbicby.MOD_EQ_MOD_SHIFT]
 685 THEN MRESAL_TAC Qknvmlb.SUC_MOD_NOT_EQ[`4`][ADD1];
 686
 687 DICH_TAC 0
 688 THEN REWRITE_TAC[scs_M;IN_ELIM_THM]
 689 THEN ASM_SIMP_TAC[DIVISION]
 690 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1) MOD 4`;`SUC ((p + 1) MOD 4)`;`s`;`p+1`;`SUC ((p + 1) MOD 4) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD]
 691 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`SUC (p + 1) MOD 4`;`s`;`p+1`;`SUC (p + 1)`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`SUC(p+1)=p+2`]
 692 THEN REAL_ARITH_TAC]);;
 693
 694
 695 let B_LE_2h0_2_SCS_M_4=prove(`scs_k_v39 s = 4/\ is_scs_v39 s /\ {p MOD 4,(p+3)MOD 4} SUBSET scs_M s
 696 ==> scs_b_v39 s (p+2) (p+3)<= &2*h0`,
 697 REPEAT STRIP_TAC
 698 THEN MP_TAC SCS_M_CASES_4_EQ
 699 THEN RESA_TAC
 700 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ ~(2 MOD 4 = 3 MOD 4)/\ ~(2 MOD 4 = 0 MOD 4)/\ 1<4`)
 701 THEN SUBGOAL_THEN`~((p+2) MOD 4 IN scs_M s)`ASSUME_TAC
 702 THENL[
 703 ASM_SIMP_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`;Ocbicby.MOD_EQ_MOD_SHIFT]
 704 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`2`;`0`;`p`][ARITH_RULE`p+0=p`];
 705 DICH_TAC 0
 706 THEN REWRITE_TAC[scs_M;IN_ELIM_THM]
 707 THEN ASM_SIMP_TAC[DIVISION]
 708 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2) MOD 4`;`SUC ((p + 2) MOD 4)`;`s`;`p+2`;`SUC ((p + 2) MOD 4) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD]
 709 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2)`;`SUC (p + 2) MOD 4`;`s`;`p+2`;`SUC (p + 2)`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`SUC(p+2)=p+3`]
 710 THEN REAL_ARITH_TAC]);;
 711
 712
 713
 714 let B_LE_2h0_2_SCS_M_4=prove(`scs_k_v39 s = 4/\ is_scs_v39 s /\ {p MOD 4,(p+3)MOD 4} SUBSET scs_M s
 715 ==> scs_b_v39 s (p+1) (p+2)<= &2*h0 /\ scs_b_v39 s (p+2) (p+3)<= &2*h0`,
 716 SIMP_TAC[B_LE_2h0_2_SCS_M_4;B_LE_2h0_SCS_M_4]);;
 717
 718
 719
 720 let WKZZEEH = prove_by_refinement(`main_nonlinear_terminal_v11 ==>
 721   (!s v p.
 722     is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ MMs_v39 s v/\
 723     (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
 724     (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
 725        (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
 726     ~scs_is_str s v p /\ ~scs_is_str s v (p+1) /\ ~scs_is_str s v (p+3)
 727     ==> (~(dist(v p,v(p+3)) = cstab /\ dist(v(p),v(p+1)) = cstab)))`,
 728 [STRIP_TAC
 729 THEN REPEAT GEN_TAC
 730 THEN STRIP_TAC
 731 THEN REWRITE_TAC[DE_MORGAN_THM]
 732 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
 733 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
 734 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
 735 THEN ASM_TAC
 736 THEN REPEAT RESA_TAC
 737 THEN ASSUME_TAC(ARITH_RULE`3<4/\ 1<4/\ ~(4=0)`)
 738 THEN ASM_SIMP_TAC[]
 739 THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN]
 740 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 741 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`s`;`v`]
 742 THEN MP_TAC Local_lemmas.CVLF_LF_F
 743 THEN RESA_TAC
 744 THEN SUBGOAL_THEN`!i. dist((v:num->real^3) i, v(SUC i))<= cstab`ASSUME_TAC
 745 ;
 746
 747
 748 REWRITE_TAC[dist]
 749 THEN MATCH_MP_TAC (GEN_ALL Axjrpnc.NORM_V_IN_BB_LE_CSTAB)
 750 THEN EXISTS_TAC`s:scs_v39`
 751 THEN ASM_REWRITE_TAC[]
 752 THEN GEN_TAC
 753 THEN REWRITE_TAC[ADD1]
 754 THEN THAYTHE_TAC (18-6)[`i`]
 755 THEN REWRITE_TAC[cstab;h0]
 756 THEN REAL_ARITH_TAC;
 757
 758 THAYTHEL_ASM_TAC 0[`p`][ADD1]
 759 THEN THAYTHEL_TAC 0[`p+3`][ARITH_RULE`SUC(p+3)=1*4+p`]
 760 THEN DICH_TAC 0
 761 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 762 THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
 763 THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[DIST_SYM]
 764 THEN REMOVE_ASSUM_TAC
 765 THEN DICH_TAC 0
 766 THEN MP_TAC Jotswix.JOTSWIX
 767 THEN RESA_TAC
 768 THEN THAYTHE_TAC 0[`s`;`FF`;`v`;`p`]
 769 THEN DICH_TAC 0
 770 THEN SUBGOAL_THEN`scs_a_v39 s p (p + 1) < cstab`ASSUME_TAC;
 771
 772
 773 THAYTHE_TAC (18-6)[`p`]
 774 THEN REWRITE_TAC[cstab;h0]
 775 THEN REAL_ARITH_TAC;
 776
 777
 778 ASM_REWRITE_TAC[]
 779 THEN SUBGOAL_THEN`(!i. ~(i MOD 4 = (p + 2) MOD 4) ==> interior_angle1 (vec 0) FF ((v:num->real^3)i) < pi)`ASSUME_TAC;
 780
 781 REMOVE_ASSUM_TAC
 782 THEN ASM_REWRITE_TAC[NOT_MOD_4_CASES]
 783 THEN REPEAT STRIP_TAC;
 784
 785
 786 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 787 THEN THAYTHES_TAC 0[`i`;`p`][MOD_MULT_ADD]
 788 THEN DICH_TAC(20-7)
 789 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1;scs_is_str]
 790 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
 791 THEN MRESA_TAC WL_IN_V[`SUC p`;`v:num->real^3`]
 792 THEN MRESA_TAC WL_IN_V[`p+4-1`;`v:num->real^3`]
 793 THEN MRESA_TAC WL_IN_V[`SUC p+4-1`;`v:num->real^3`]
 794 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
 795 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][GSYM ADD1]
 796 THEN THAYTHE_TAC 0[`v (p+4-1)`]
 797 THEN DICH_TAC 0
 798 THEN REAL_ARITH_TAC;
 799
 800
 801
 802
 803 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 804 THEN THAYTHES_TAC 0[`i`;`p+1`][MOD_MULT_ADD]
 805 THEN DICH_TAC(20-8)
 806 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1;scs_is_str]
 807 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
 808 THEN MRESA_TAC WL_IN_V[`SUC p`;`v:num->real^3`]
 809 THEN MRESA_TAC WL_IN_V[`p+4-1`;`v:num->real^3`]
 810 THEN MRESA_TAC WL_IN_V[`SUC p+4-1`;`v:num->real^3`]
 811 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (SUC p)`;`v`;`(SUC p)`;`4`]
 812 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][GSYM ADD1]
 813 THEN THAYTHE_TAC 0[`v ((SUC p)+4-1)`]
 814 THEN DICH_TAC 0
 815 THEN REAL_ARITH_TAC;
 816
 817
 818
 819
 820 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 821 THEN THAYTHES_TAC 0[`i`;`p+3`][MOD_MULT_ADD]
 822 THEN DICH_TAC(20-9)
 823 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;GSYM ADD1;scs_is_str]
 824 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
 825 THEN MRESA_TAC WL_IN_V[`(p+3)`;`v:num->real^3`]
 826 THEN MRESA_TAC WL_IN_V[`p+4-1`;`v:num->real^3`]
 827 THEN MRESA_TAC WL_IN_V[`(p+3)+4-1`;`v:num->real^3`]
 828 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v ((p+3))`;`v`;`((p+3))`;`4`]
 829 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v ((p+3))`][GSYM ADD1]
 830 THEN THAYTHE_TAC 0[`v (((p+3))+4-1)`]
 831 THEN DICH_TAC 0
 832 THEN REAL_ARITH_TAC;
 833
 834
 835 REPEAT RESA_TAC
 836 THEN MP_TAC(REAL_ARITH`dist (v p,v (p + 1)) <= cstab/\
 837 dist (v p,v (p + 3)) <= cstab
 838 ==> (dist (v p,v (p + 1)) = cstab/\dist (v p,v (p + 3)) = cstab)
 839 \/ dist ((v:num->real^3) p,v (p + 1)) < cstab \/ dist (v p,v (p + 3)) < cstab`)
 840 THEN RESA_TAC;
 841
 842
 843 SUBGOAL_THEN`p MOD 4 IN scs_M s`ASSUME_TAC;
 844
 845
 846 ASM_SIMP_TAC[scs_M;IN_ELIM_THM;DIVISION]
 847 THEN MATCH_MP_TAC(SET_RULE`A==> A\/B`)
 848 THEN DICH_TAC(25-15)
 849 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;]
 850 THEN STRIP_TAC
 851 THEN THAYTHE_TAC 0[`p MOD 4`;`SUC(p MOD 4)`]
 852 THEN DICH_TAC 0
 853 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 854 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 855 THEN THAYTHES_TAC 0[`p MOD 4`;`p`][MOD_REFL]
 856 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 857 THEN THAYTHES_TAC 0[`SUC(p MOD 4)`;`SUC(p MOD 4) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD]
 858 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 859 THEN THAYTHES_TAC 0[`SUC p MOD 4`;`SUC p`][MOD_REFL;ADD1;cstab;h0]
 860 THEN REAL_ARITH_TAC
 861 ;
 862
 863
 864
 865 SUBGOAL_THEN`(p+3) MOD 4 IN scs_M s`ASSUME_TAC;
 866
 867 REMOVE_ASSUM_TAC
 868 THEN ASM_SIMP_TAC[scs_M;IN_ELIM_THM;DIVISION]
 869 THEN MATCH_MP_TAC(SET_RULE`A==> A\/B`)
 870 THEN DICH_TAC(25-15)
 871 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;]
 872 THEN STRIP_TAC
 873 THEN THAYTHE_TAC 0[`(p+3) MOD 4`;`SUC((p+3) MOD 4)`]
 874 THEN DICH_TAC 0
 875 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 876 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 877 THEN THAYTHES_TAC 0[`(p+3) MOD 4`;`(p+3)`][MOD_REFL]
 878 THEN ONCE_REWRITE_TAC[DIST_SYM]
 879 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 880 THEN THAYTHES_TAC 0[`SUC((p+3) MOD 4)`;`SUC((p+3) MOD 4) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`SUC(p+3)=(1*4+p)`;MOD_MULT_ADD]
 881 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 882 THEN THAYTHES_TAC 0[`p MOD 4`;`p`][MOD_REFL;ADD1;cstab;h0]
 883 THEN REAL_ARITH_TAC
 884 ;
 885
 886
 887 MP_TAC(SET_RULE`p MOD 4 IN scs_M s/\
 888 (p + 3) MOD 4 IN scs_M s==>{p MOD 4,(p+3)MOD 4} SUBSET scs_M s`)
 889 THEN RESA_TAC
 890 THEN MP_TAC B_LE_2h0_2_SCS_M_4
 891 THEN RESA_TAC
 892 THEN MRESAL_TAC ASSWPOW[`s`;`v`;`p+1`][IN;ARITH_RULE`(a+1)+1=a+2/\ (a+1)+2=a+3`]
 893 THEN POP_ASSUM MP_TAC
 894 THEN REWRITE_TAC[]
 895 THEN ONCE_REWRITE_TAC[DIST_SYM]
 896 THEN ONCE_REWRITE_TAC[Ocbicby.xrr_sym]
 897 THEN STRIP_TAC
 898 THEN DICH_TAC(31-21)
 899 THEN ASM_REWRITE_TAC[]
 900 THEN REAL_ARITH_TAC;
 901
 902
 903
 904 DICH_TAC 0
 905 THEN REAL_ARITH_TAC
 906 ;
 907
 908 DICH_TAC 0
 909 THEN REAL_ARITH_TAC
 910 ;
 911 ]);;
 912
 913
 914 (***************************)
 915 let BASIC_IMP_NOT_J=prove(`scs_basic_v39 s==> (!p i. ~scs_J_v39 s p i)`,
 916 REWRITE_TAC[scs_basic]
 917 THEN SET_TAC[]);;
 918
 919 let CONDTION_A_LT_B=prove(`(!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
 920        (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab))
 921 ==> (!i. scs_a_v39 s i (i+1)< scs_b_v39 s i (i+1))`,
 922 REWRITE_TAC[h0;cstab]
 923 THEN REPEAT STRIP_TAC
 924 THEN THAYTHE_TAC 0[`i`]
 925 THEN ASM_TAC
 926 THEN REAL_ARITH_TAC);;
 927
 928 let A_EQ2_IMP_B=prove(`(!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
 929        (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab))
 930 /\ scs_a_v39 s p (p+1) = &2
 931 ==>  scs_b_v39 s p (p+1)= &2 * h0`,
 932 REPEAT STRIP_TAC
 933 THEN THAYTHE_TAC 1[`p`]
 934 THEN DICH_TAC 1
 935 THEN ASM_REWRITE_TAC[cstab;h0]
 936 THEN REAL_ARITH_TAC);;
 937
 938 let A_EQ2h0_IMP_B=prove(`(!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
 939        (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab))
 940 /\ scs_a_v39 s p (p+1) = &2 * h0
 941 ==>  scs_b_v39 s p (p+1)= cstab`,
 942 REPEAT STRIP_TAC
 943 THEN THAYTHE_TAC 1[`p`]
 944 THEN DICH_TAC 1
 945 THEN ASM_REWRITE_TAC[cstab;h0]
 946 THEN REAL_ARITH_TAC);;
 947
 948
 949 let A_NOT_EQ2_IMP_B=prove(`(!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
 950        (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab))
 951 /\ ~(scs_a_v39 s p (p+1) = &2 )
 952 ==>  scs_a_v39 s p (p+1) = &2* h0 /\ scs_b_v39 s p (p+1)= cstab`,
 953 REPEAT STRIP_TAC
 954 THEN THAYTHE_TAC 1[`p`]);;
 955
 956
 957
 958 let B_LE_2h0_IMP_B=prove(`(!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
 959        (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab))
 960 /\ scs_b_v39 s p (p+1) <= &2 *h0
 961 ==>  scs_a_v39 s p (p+1) = &2 /\ scs_b_v39 s p (p+1)= &2*h0`,
 962 REPEAT STRIP_TAC
 963 THEN DICH_TAC 0
 964 THEN THAYTHE_TAC 0[`p`]
 965 THEN ASM_REWRITE_TAC[cstab;h0]
 966 THEN REAL_ARITH_TAC);;
 967
 968
 969 let STR_MOD_EQ=prove(`is_scs_v39 s /\ scs_k_v39 s = k /\ v IN MMs_v39 s
 970 ==>
 971 (scs_is_str s v (p MOD k)<=> scs_is_str s v p)`,
 972 REWRITE_TAC[IN;scs_is_str]
 973 THEN REPEAT STRIP_TAC
 974 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
 975 THEN MP_TAC Yrtafyh.PROPERTY_OF_K_SCS
 976 THEN RESA_TAC
 977 THEN MP_TAC(ARITH_RULE`1<k==> k-1<k`)
 978 THEN RESA_TAC
 979 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 980 THEN THAYTHES_TAC 0[`p MOD k`;`p`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;MOD_REFL]
 981 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 982 THEN THAYTHES_TAC 0[`SUC(p MOD k)`;`SUC p`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;MOD_REFL;Yxionxl2.MOD_SUC_MOD]
 983 THEN MRESAS_TAC MOD_ADD_MOD[`p`;`k-1`;`k`][MOD_LT]
 984 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
 985 THEN THAYTHES_TAC 0[`(p MOD k)+k-1`;` p+k-1`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;MOD_REFL;Yxionxl2.MOD_SUC_MOD]);;
 986
 987 let IN_SCS_STR_CASES_4=prove(`
 988     is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s  /\ scs_is_str s v p==>
 989 p MOD 4 IN {i | i < 4 /\ scs_is_str s v i}`,
 990 REWRITE_TAC[IN]
 991 THEN REPEAT STRIP_TAC
 992 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\1<4/\ 3<4`)
 993 THEN ASM_SIMP_TAC[IN_ELIM_THM;DIVISION]
 994 THEN DICH_TAC 1
 995 THEN MRESAL_TAC STR_MOD_EQ[`4`;`s`;`v`;`p`][IN]);;
 996
 997
 998 let FINITE_SET_STR=prove(`FINITE {i | i < k /\ scs_is_str s v i}`,
 999 MATCH_MP_TAC FINITE_SUBSET
1000 THEN EXISTS_TAC`0..k`
1001 THEN ASM_REWRITE_TAC[FINITE_NUMSEG;IN_ELIM_THM;IN_NUMSEG;SUBSET]
1002 THEN ARITH_TAC);;
1003
1004 let NOT_STR_IN_CASES_4=prove(`!s v.
1005     is_scs_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s  /\ scs_is_str s v p==>
1006     ~scs_is_str s v (p+1)/\ ~scs_is_str s v (p+2)/\ ~scs_is_str s v (p+3)`,
1007 REPEAT GEN_TAC
1008 THEN STRIP_TAC
1009 THEN ASSUME_TAC(ARITH_RULE`~(4=0)`)
1010 THEN MRESA_TAC WGDHPPI[`s`;`v`]
1011 THEN MP_TAC IN_SCS_STR_CASES_4
1012 THEN RESA_TAC
1013 THEN MRESA_TAC FINITE_SET_STR[`4`;`s`;`v`]
1014 THEN MRESAS_TAC CARD_SUBSET_LE[`{p MOD 4}`;`{i | i < 4 /\ scs_is_str s v i}`][Geomdetail.CARD_SING;SET_RULE`a IN A==> {a} SUBSET A`]
1015 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`2`;`0`;`p`][ARITH_RULE`p+0=p/\ ~(2 MOD 4= 0 MOD 4)`]
1016 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`1`;`0`;`p`][ARITH_RULE`p+0=p/\ ~(1 MOD 4= 0 MOD 4)`]
1017 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`3`;`0`;`p`][ARITH_RULE`p+0=p/\ ~(3 MOD 4= 0 MOD 4)`]
1018 THEN MP_TAC(SET_RULE`{p MOD 4} = {i | i < 4 /\ scs_is_str s v i}/\
1019 ~((p + 2) MOD 4 = p MOD 4)/\
1020 ~((p + 1) MOD 4 = p MOD 4)/\
1021 ~((p + 3) MOD 4 = p MOD 4)
1022 ==> ~((p + 1) MOD 4 IN {i | i < 4 /\ scs_is_str s v i})/\
1023  ~((p + 2) MOD 4 IN {i | i < 4 /\ scs_is_str s v i})/\
1024 ~((p + 3) MOD 4 IN {i | i < 4 /\ scs_is_str s v i})`)
1025 THEN RESA_TAC
1026 THEN DICH_TAC 0
1027 THEN DICH_TAC 0
1028 THEN DICH_TAC 0
1029 THEN ASM_SIMP_TAC[IN_ELIM_THM; DIVISION;STR_MOD_EQ]);;
1030
1031
1032 let NOT_STR_IN_CASES_4_1=prove(`!s v.
1033          is_scs_v39 s /\
1034          scs_k_v39 s = 4 /\
1035          v IN MMs_v39 s /\
1036          scs_is_str s v (p+1)
1037          ==> ~scs_is_str s v (p ) /\
1038              ~scs_is_str s v (p + 2) /\
1039              ~scs_is_str s v (p + 3)`,
1040 REPEAT GEN_TAC
1041 THEN STRIP_TAC
1042 THEN MRESAL_TAC NOT_STR_IN_CASES_4[`p+1`;`s`;`v`][ARITH_RULE`(p+1)+1=p+2/\ (p+1)+2=p+3/\ (p+1)+3=1*4+p`]
1043 THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`1*4+p`][MOD_MULT_ADD]
1044 THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`p`][MOD_MULT_ADD]);;
1045
1046
1047 let PRO_ADD_NOT_IN_SCS_M=prove(`is_scs_v39 s/\ scs_a_v39 s i (i+1) = &2 * h0/\ scs_k_v39 s=k
1048 ==> i MOD k IN scs_M s`,
1049 REWRITE_TAC[IN_ELIM_THM;scs_M]
1050 THEN RESA_TAC
1051 THEN MP_TAC Yrtafyh.PROPERTY_OF_K_SCS
1052 THEN RESA_TAC
1053 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`i MOD k`;`SUC(i MOD k)`;`s`;`i`;`SUC(i MOD k) MOD k`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;DIVISION]
1054 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`i`;`SUC i MOD k`;`s`;`i`;`SUC i`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1055 THEN ASM_REWRITE_TAC[ADD1;h0]
1056 THEN REAL_ARITH_TAC);;
1057
1058 let TUAPYYU_IMP_CASES=prove(`
1059 main_nonlinear_terminal_v11 ==>
1060 (!s v p.
1061     is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ v IN MMs_v39 s /\
1062     (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
1063     (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
1064        (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
1065     ~scs_is_str s v p /\ ~scs_is_str s v (p+1)
1066     ==> dist(v p,v(p+1)) = &2\/ dist(v p,v(p+1)) = &2 * h0 \/ dist(v p,v(p+1)) = cstab)`,
1067 REPEAT STRIP_TAC
1068 THEN MP_TAC TUAPYYU
1069 THEN RESA_TAC
1070 THEN THAYTHEL_TAC 0[`s`;`v`;`p`][]
1071 THEN THAYTHE_TAC 3[`p`]);;
1072
1073 let SCS_M_CASES_4_EQ1=prove(`scs_k_v39 s = 4/\ is_scs_v39 s /\ {(p+1) MOD 4,(p+3)MOD 4} SUBSET scs_M s
1074 ==> scs_M s={(p+1) MOD 4,(p+3)MOD 4}`,
1075 REPEAT STRIP_TAC
1076 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ ~(1 MOD 4 = 3 MOD 4)`)
1077 THEN MRESAS_TAC Planarity.CARD_2_FAN[`(p+1) MOD 4`;`(p+3) MOD 4`][Ocbicby.MOD_EQ_MOD_SHIFT]
1078 THEN DICH_TAC 0
1079 THEN REWRITE_TAC[ARITH_RULE`p+1=p+1`]
1080 THEN STRIP_TAC
1081 THEN MP_TAC SCS_M_CASES_4_LE_2
1082 THEN RESA_TAC
1083 THEN MP_TAC Jlxfdmj.FINITE_SCS_M
1084 THEN RESA_TAC
1085 THEN MRESA_TAC CARD_SUBSET_LE[`{(p+1) MOD 4, (p + 3) MOD 4}`;`scs_M s`]);;
1086
1087
1088
1089
1090 let B_LE_2h0_2_SCS_M_4_1=prove(
1091 `scs_k_v39 s = 4/\ is_scs_v39 s /\ {(p+1) MOD 4,(p+3)MOD 4} SUBSET scs_M s
1092 ==> scs_b_v39 s (p+2) (p+3)<= &2*h0`,
1093 REPEAT STRIP_TAC
1094 THEN MP_TAC SCS_M_CASES_4_EQ1
1095 THEN RESA_TAC
1096 THEN ASSUME_TAC(ARITH_RULE`~(4=0)/\ ~(2 MOD 4 = 3 MOD 4)/\ ~(2 MOD 4 = 1 MOD 4)/\ 1<4`)
1097 THEN SUBGOAL_THEN`~((p+2) MOD 4 IN scs_M s)`ASSUME_TAC
1098 THENL[
1099
1100 ASM_SIMP_TAC[SET_RULE`a IN {b,c}<=> a=b\/ a=c`;Ocbicby.MOD_EQ_MOD_SHIFT]
1101 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`2`;`1`;`p`][ARITH_RULE`p+0=p`];
1102
1103 DICH_TAC 0
1104 THEN REWRITE_TAC[scs_M;IN_ELIM_THM]
1105 THEN ASM_SIMP_TAC[DIVISION]
1106 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2) MOD 4`;`SUC ((p + 2) MOD 4)`;`s`;`p+2`;`SUC ((p + 2) MOD 4) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD]
1107 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2)`;`SUC (p + 2) MOD 4`;`s`;`p+2`;`SUC (p + 2)`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`SUC(p+2)=p+3`]
1108 THEN REAL_ARITH_TAC]);;
1109
1110
1111 let SCS_A_SYM=prove(`is_scs_v39 s
1112 ==> scs_a_v39 s i j= scs_a_v39 s j i`,
1113 REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;dist]
1114 THEN RESA_TAC);;
1115
1116 let SCS_B_SYM=prove(`is_scs_v39 s
1117 ==> scs_b_v39 s i j= scs_b_v39 s j i`,
1118 REWRITE_TAC[is_scs_v39;LET_DEF;LET_END_DEF;dist]
1119 THEN RESA_TAC);;
1120
1121
1122
1123
1124 (***************************)
1125
1126 let PWEIWBZ= prove_by_refinement(`
1127 main_nonlinear_terminal_v11 ==>
1128 (!s v p.
1129     is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ MMs_v39 s v/\
1130     (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
1131     (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
1132        (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
1133     scs_a_v39 s p (p+1) = &2
1134     ==> dist(v p,v(p+1)) = &2)`,
1135 [REPEAT RESA_TAC
1136 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
1137 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
1138 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
1139 THEN ASM_TAC
1140 THEN REPEAT RESA_TAC
1141 THEN ASSUME_TAC(ARITH_RULE`3<4/\ 1<4/\ ~(4=0)/\ 4-1=3/\ SUC (p + 3)= 1*4+p/\ SUC p= p+1`)
1142 THEN ASM_SIMP_TAC[]
1143 THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN;scs_generic]
1144 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
1145 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`s`;`v`]
1146 THEN MP_TAC Local_lemmas.CVLF_LF_F
1147 THEN RESA_TAC
1148 THEN MP_TAC Tfitskc.SCS_DIAG_A_LE_DIST
1149 THEN RESA_TAC
1150 THEN MP_TAC(SET_RULE`(~scs_is_str s v p /\ ~scs_is_str s v (p+1))\/ scs_is_str s v p \/ scs_is_str s v (p+1)`)
1151 THEN RESA_TAC;
1152
1153
1154 MP_TAC YEBWJNG
1155 THEN RESA_TAC
1156 THEN MATCH_DICH_TAC 0
1157 THEN EXISTS_TAC`s:scs_v39`
1158 THEN ASM_REWRITE_TAC[IN];
1159
1160
1161 MRESAL_TAC NOT_STR_IN_CASES_4[`p`;`s`;`v`][IN]
1162 THEN DICH_TAC 3
1163 THEN ASM_REWRITE_TAC[scs_is_str;]
1164 THEN STRIP_TAC
1165 THEN DICH_TAC(21-13)
1166 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;]
1167 THEN STRIP_TAC
1168 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
1169 THEN THAYTHE_TAC 1[`p+3`;`p`]
1170 ;
1171
1172
1173 MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
1174 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
1175 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
1176 THEN RESA_TAC
1177 THEN POP_ASSUM MP_TAC
1178 THEN REWRITE_TAC[NOT_EXISTS_THM]
1179 THEN STRIP_TAC
1180 THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (p)) V' E')` ASSUME_TAC;
1181
1182
1183
1184 REPEAT RESA_TAC
1185 ;
1186
1187
1188
1189 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1190 THEN THAYTHES_TAC 0[`(p+3)+1`;`p`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1191 THEN DICH_TAC 0
1192 THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p=(p+3)+1`]
1193 THEN STRIP_TAC
1194 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1195 THEN THAYTHES_TAC 0[`(p+3)+2`;`p+1`][ARITH_RULE`(p+3)+2=1*4+p+1`;MOD_MULT_ADD]
1196 THEN DICH_TAC 0
1197 THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p+1=(p+3)+2`]
1198 THEN STRIP_TAC
1199 THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v p`;`v (p+1)`;`(v:num->real^3) (p+3)`]
1200 THEN POP_ASSUM MP_TAC
1201 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
1202 THEN STRIP_TAC
1203 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
1204 THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
1205 THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
1206 THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
1207 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+3)`;`V`]
1208 THEN SUBGOAL_THEN`(!j. ~(v j = v (p + 3)) ==> ~collinear {vec 0, (v:num->real^3) (p + 3), v j})`ASSUME_TAC
1209 ;
1210
1211 REPEAT RESA_TAC
1212 THEN DICH_TAC 0
1213 THEN REWRITE_TAC[]
1214 THEN MATCH_DICH_TAC 1
1215 THEN ASM_SIMP_TAC[]
1216 THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
1217 THEN SET_TAC[];
1218
1219
1220 MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p+3`][ARITH_RULE`0+2=2`]
1221 THEN DICH_TAC 0
1222 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
1223 THEN STRIP_TAC
1224 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1225 THEN THAYTHES_TAC 3[`v (p+1)`;`v(p+3)`][SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 3 MOD 4)`]
1226 THEN MP_TAC CONDTION_A_LT_B
1227 THEN RESA_TAC
1228 THEN MP_TAC(REAL_ARITH`scs_a_v39 s (p + 3) p <= dist (v (p + 3),v p)
1229 ==> scs_a_v39 s (p + 3) p = dist (v (p + 3),v p)\/ scs_a_v39 s (p + 3) p < dist (v (p + 3),(v:num->real^3) p)`)
1230 THEN RESA_TAC
1231 ;
1232
1233
1234
1235
1236
1237 SUBGOAL_THEN`dist (v (p + 3),(v:num->real^3) p) < scs_b_v39 s (p + 3) p`
1238 ASSUME_TAC
1239 ;
1240
1241 THAYTHE_TAC 1[`p+3`]
1242 THEN DICH_TAC 0
1243 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`((p + 3) +1)`;`s`;`p+3`;`((p + 3)+1) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1244 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1245 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1246 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1247 ;
1248
1249
1250
1251 MRESAS_TAC NUXCOEAv2[`s`;`4`;`v`;`p`;`p+3`][MOD_MULT_ADD;BASIC_IMP_NOT_J]
1252 ;
1253
1254
1255 MP_TAC(SET_RULE`~(&2=norm ((v:num->real^3) p))\/ norm (v p)= &2`)
1256 THEN RESA_TAC
1257 ;
1258
1259 MRESAS_TAC IMJXPHRv2[`s`;`4`;`v`;`p`;][MOD_MULT_ADD;BASIC_IMP_NOT_J]
1260 ;
1261
1262 MP_TAC(SET_RULE`(scs_a_v39 s (p+1) (p+2) = &2 )\/ ~((scs_a_v39 s (p+1) (p+2) = &2 ))`)
1263 THEN RESA_TAC;
1264
1265
1266
1267 SUBGOAL_THEN`scs_a_v39 s (p + 3) p < scs_b_v39 s (p + 3) p`
1268 ASSUME_TAC
1269 ;
1270
1271 THAYTHE_TAC (45-42)[`p+3`]
1272 THEN DICH_TAC 0
1273 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`((p + 3) +1)`;`s`;`p+3`;`((p + 3)+1) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1274 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1275 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1276 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1277 ;
1278
1279
1280
1281 MP_TAC  YEBWJNG
1282 THEN RESA_TAC
1283 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][IN;ARITH_RULE`(p+1)+1=p+2`]
1284 THEN ASSUME_TAC(ARITH_RULE`(p+1)+1=p+2/\ (p+2)+1=p+3`)
1285 THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+1`]
1286 THEN THAYTHE_TAC (49-42)[`p+2`]
1287 THEN MP_TAC Cqaoqlr.CQAOQLR
1288 THEN RESA_TAC
1289 THEN THAYTHES_TAC 0[`s`;`v`;`p`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1290 THEN MATCH_DICH_TAC 0
1291 THEN REWRITE_TAC[h0]
1292 THEN REAL_ARITH_TAC;
1293
1294
1295
1296 ASSUME_TAC(ARITH_RULE`(p+1)+1=p+2/\ (p+2)+1=p+3/\ (p+2)+3=1*4+p+1/\ (p+1)+3=1*4+p/\ (p+3)+1=1*4+p/\ (p+3)+3=1*4+p+2/\ (p+3)+2=1*4+p+1`)
1297 THEN MRESA_TAC A_NOT_EQ2_IMP_B[`s`;`p+1`]
1298 THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`1*4+p+1`][IN;MOD_MULT_ADD]
1299 THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`p+1`][IN;MOD_MULT_ADD;MOD_REFL]
1300 THEN THAYTHES_TAC (50-40)[`1 * 4 + p + 1`;`p+1`][MOD_MULT_ADD]
1301 THEN MP_TAC WKZZEEH
1302 THEN RESA_TAC
1303 THEN THAYTHE_TAC 0[`s`;`v`;`p+2`]
1304 THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p+1`;`4`;`s`]
1305 THEN MP_TAC(SET_RULE`scs_a_v39 s (p + 3) p = &2 \/ ~(scs_a_v39 s (p + 3) p = &2 )`)
1306 THEN RESA_TAC;
1307
1308 (**********CASES a 3 0 =2********************)
1309
1310 MP_TAC TUAPYYU
1311 THEN RESA_TAC
1312 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][IN];
1313
1314
1315 MP_TAC Jotswix.LEMMA_PWE1
1316 THEN RESA_TAC
1317 THEN THAYTHEL_TAC 0[`s`;`v`;`p`][scs_generic;IN;REAL_ARITH`a<=a`;scs_is_str]
1318 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1319 THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
1320 THEN MP_TAC Cuxvzoz.CJBDXXN
1321 THEN RESA_TAC
1322 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+1`;`v`]
1323 THEN ONCE_REWRITE_TAC[DIST_SYM]
1324 THEN MATCH_DICH_TAC 0
1325 THEN ASM_SIMP_TAC[]
1326 THEN REWRITE_TAC[GSYM ADD1]
1327 THEN ASM_REWRITE_TAC[scs_generic]
1328 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1329 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
1330 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+1)`;`v`;`(p+1)`;`4`]
1331 THEN DICH_TAC(58-17)
1332 THEN ASM_REWRITE_TAC[scs_is_str]
1333 THEN RESA_TAC
1334 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][]
1335 THEN THAYTHE_TAC 0[`v (p)`]
1336 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) <= pi
1337 /\ ~(azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) = pi)
1338 ==> azim (vec 0) (v (p + 1)) (v (p + 2)) ((v:num->real^3) p) < pi`)
1339 THEN RESA_TAC
1340 THEN ONCE_REWRITE_TAC[DIST_SYM]
1341 THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
1342  &2 * #1.26 <= #3.01`]
1343 THEN REPEAT STRIP_TAC;
1344
1345
1346
1347 THAYTHES_TAC(60-5)[`p`;`p+2`][SCS_DIAG_4_ADD0]
1348 THEN DICH_TAC 1
1349 THEN REWRITE_TAC[cstab]
1350 THEN REAL_ARITH_TAC;
1351
1352 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1353 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
1354 THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+2)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 2 MOD 4)`]
1355 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
1356 THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+0)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
1357 THEN DICH_TAC 0
1358 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`]
1359 THEN RESA_TAC
1360 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+1)`;`v(p+2)`;`v p`]
1361 ;
1362
1363
1364
1365
1366 MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1367 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1368 THEN ASM_TAC
1369 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1370 THEN REPEAT RESA_TAC
1371 ;
1372
1373
1374
1375 MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1376 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1377 THEN ASM_TAC
1378 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1379 THEN REPEAT RESA_TAC
1380 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;h0]
1381 THEN REAL_ARITH_TAC;
1382
1383
1384 POP_ASSUM MP_TAC
1385 THEN ONCE_REWRITE_TAC[DIST_SYM]
1386 THEN STRIP_TAC
1387 THEN DICH_TAC 3
1388 THEN RESA_TAC
1389 THEN MP_TAC TUAPYYU_IMP_CASES
1390 THEN RESA_TAC
1391 THEN THAYTHEL_TAC 0[`s`;`v`;`p+2`][IN];
1392
1393
1394 (************CASES 2 3= 2**********)
1395
1396 MP_TAC Jotswix.LEMMA_PWE2
1397 THEN RESA_TAC
1398 THEN THAYTHEL_TAC 0[`s`;`v`;`p`][scs_generic;IN;REAL_ARITH`a<=a/\ &2 <= &2 * #1.26`;scs_is_str;h0]
1399 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1400 THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
1401 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1402 THEN THAYTHES_TAC 0[`1*4+p+2`;`p+2`][MOD_MULT_ADD]
1403 THEN MP_TAC Cuxvzoz.CUXVZOZ
1404 THEN RESA_TAC
1405 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+3`;`v`]
1406 THEN DICH_TAC 0
1407 THEN ASM_SIMP_TAC[]
1408 THEN REWRITE_TAC[GSYM ADD1]
1409 THEN ASM_REWRITE_TAC[scs_generic]
1410 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1411 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
1412 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+3)`;`v`;`(p+3)`;`4`]
1413 THEN DICH_TAC(60-19)
1414 THEN ASM_REWRITE_TAC[scs_is_str]
1415 THEN RESA_TAC
1416 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+3)`][]
1417 THEN THAYTHE_TAC 0[`v (p+2)`]
1418 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 3))  (v p) (v (p + 2)) <= pi
1419 /\ ~(azim (vec 0) (v (p + 3))  (v p) (v (p + 2)) = pi)
1420 ==> azim (vec 0) (v (p + 3))  ((v:num->real^3) p) (v (p + 2)) < pi`)
1421 THEN RESA_TAC
1422 THEN ONCE_REWRITE_TAC[DIST_SYM]
1423 THEN SUBGOAL_THEN`&3 <= dist ((v:num->real^3) p,v (p + 2))`ASSUME_TAC
1424 ;
1425
1426
1427
1428
1429 THAYTHES_TAC(62-5)[`p`;`p+2`][SCS_DIAG_4_ADD0]
1430 THEN DICH_TAC 1
1431 THEN REWRITE_TAC[cstab]
1432 THEN REAL_ARITH_TAC;
1433
1434 SUBGOAL_THEN`(pi / &2 < azim (vec 0) (v (p + 3)) (v p) (v (p + 2)) \/
1435    azim (vec 0) (v p) (rho_node1 FF (v p)) (ivs_rho_node1 FF ((v:num->real^3) p)) < pi)`ASSUME_TAC
1436 ;
1437
1438
1439
1440
1441
1442 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1443 THEN THAYTHEL_ASM_TAC(64-37)[`p+0`][]
1444 THEN THAYTHES_TAC(0)[`p+2`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 2 MOD 4)`]
1445 THEN DICH_TAC 1
1446 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 0 MOD 4)`]
1447 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`]
1448 THEN RESA_TAC
1449 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+3)`;`v(p)`;`v (p+2)`]
1450 ;
1451
1452
1453 SUBGOAL_THEN`scs_a_v39 s (p + 3) (1 * 4 + p) = &2`ASSUME_TAC
1454 ;
1455
1456
1457
1458 MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1459 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1460 THEN ASM_TAC
1461 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1462 THEN REPEAT RESA_TAC
1463 ;
1464
1465
1466 SUBGOAL_THEN`scs_b_v39 s (p + 3) (1 * 4 + p) <= &2 * h0`ASSUME_TAC
1467 ;
1468
1469
1470
1471 MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1472 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1473 THEN ASM_TAC
1474 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1475 THEN REPEAT RESA_TAC
1476 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;]
1477 THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+3`]
1478 THEN REAL_ARITH_TAC
1479 ;
1480
1481
1482 ASM_REWRITE_TAC[cstab;REAL_ARITH`&2 <= #3.01`]
1483 THEN ONCE_REWRITE_TAC[DIST_SYM]
1484 THEN STRIP_TAC
1485 THEN ONCE_REWRITE_TAC[DIST_SYM]
1486 THEN MP_TAC Cqaoqlr.CQAOQLR
1487 THEN RESA_TAC
1488 THEN THAYTHES_TAC 0[`s`;`v`;`p+3`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1489 THEN DICH_TAC 0
1490 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p)`;`(1 * 4 + p+1)`;`s`;`p`;`p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1491 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p)`;`(1 * 4 + p+1)`;`s`;`p`;`p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1492 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p+2)`;`(p+3)`;`s`;`p+2`;`p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1493 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p+2)`;`(p+3)`;`s`;`p+2`;`p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1494 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;`p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1495 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;`p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1496 THEN THAYTHEL_ASM_TAC(73-40)[`p+2`][]
1497 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`( p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1498 THEN THAYTHEL_ASM_TAC(1)[`p+3`][h0;cstab]
1499 THEN REAL_ARITH_TAC;
1500
1501 (************CASES 2 3= 2* H0**********)
1502
1503
1504 MP_TAC Jotswix.LEMMA_PWE2
1505 THEN RESA_TAC
1506 THEN THAYTHEL_TAC 0[`s`;`v`;`p`][scs_generic;IN;REAL_ARITH`a<=a/\ &2 <= &2 * #1.26`;scs_is_str;h0]
1507 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1508 THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
1509 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1510 THEN THAYTHES_TAC 0[`1*4+p+2`;`p+2`][MOD_MULT_ADD]
1511 THEN MP_TAC Cuxvzoz.CUXVZOZ
1512 THEN RESA_TAC
1513 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+3`;`v`]
1514 THEN DICH_TAC 0
1515 THEN ASM_SIMP_TAC[]
1516 THEN REWRITE_TAC[GSYM ADD1]
1517 THEN ASM_REWRITE_TAC[scs_generic]
1518 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1519 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
1520 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+3)`;`v`;`(p+3)`;`4`]
1521 THEN DICH_TAC(60-19)
1522 THEN ASM_REWRITE_TAC[scs_is_str]
1523 THEN RESA_TAC
1524 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+3)`][]
1525 THEN THAYTHE_TAC 0[`v (p+2)`]
1526 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 3))  (v p) (v (p + 2)) <= pi
1527 /\ ~(azim (vec 0) (v (p + 3))  (v p) (v (p + 2)) = pi)
1528 ==> azim (vec 0) (v (p + 3))  ((v:num->real^3) p) (v (p + 2)) < pi`)
1529 THEN RESA_TAC
1530 THEN ONCE_REWRITE_TAC[DIST_SYM]
1531 THEN SUBGOAL_THEN`&3 <= dist ((v:num->real^3) p,v (p + 2))`ASSUME_TAC
1532 ;
1533
1534
1535
1536
1537 THAYTHES_TAC(62-5)[`p`;`p+2`][SCS_DIAG_4_ADD0]
1538 THEN DICH_TAC 1
1539 THEN REWRITE_TAC[cstab]
1540 THEN REAL_ARITH_TAC;
1541
1542 SUBGOAL_THEN`(pi / &2 < azim (vec 0) (v (p + 3)) (v p) (v (p + 2)) \/
1543    azim (vec 0) (v p) (rho_node1 FF (v p)) (ivs_rho_node1 FF ((v:num->real^3) p)) < pi)`ASSUME_TAC
1544 ;
1545
1546
1547
1548
1549
1550 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1551 THEN THAYTHEL_ASM_TAC(64-37)[`p+0`][]
1552 THEN THAYTHES_TAC(0)[`p+2`][Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 2 MOD 4)`]
1553 THEN DICH_TAC 1
1554 THEN ASM_SIMP_TAC[Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 0 MOD 4)`]
1555 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`]
1556 THEN RESA_TAC
1557 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+3)`;`v(p)`;`v (p+2)`]
1558 ;
1559
1560
1561 SUBGOAL_THEN`scs_a_v39 s (p + 3) (1 * 4 + p) = &2`ASSUME_TAC
1562 ;
1563
1564
1565
1566 MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1567 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1568 THEN ASM_TAC
1569 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1570 THEN REPEAT RESA_TAC
1571 ;
1572
1573
1574 SUBGOAL_THEN`scs_b_v39 s (p + 3) (1 * 4 + p) <= &2 * h0`ASSUME_TAC
1575 ;
1576
1577
1578
1579 MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1580 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`p MOD 4`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1581 THEN ASM_TAC
1582 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1583 THEN REPEAT RESA_TAC
1584 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;]
1585 THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+3`]
1586 THEN REAL_ARITH_TAC
1587 ;
1588
1589
1590 ASM_REWRITE_TAC[cstab;REAL_ARITH`&2 <= &2 * #1.26 /\ &2 * #1.26 <= #3.01`;h0]
1591 THEN ONCE_REWRITE_TAC[DIST_SYM]
1592 THEN STRIP_TAC
1593 THEN ONCE_REWRITE_TAC[DIST_SYM]
1594 THEN MP_TAC Cqaoqlr.CQAOQLR
1595 THEN RESA_TAC
1596 THEN THAYTHES_TAC 0[`s`;`v`;`p+3`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1597 THEN DICH_TAC 0
1598 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p)`;`(1 * 4 + p+1)`;`s`;`p`;`p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1599 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p)`;`(1 * 4 + p+1)`;`s`;`p`;`p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1600 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p+2)`;`(p+3)`;`s`;`p+2`;`p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1601 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p+2)`;`(p+3)`;`s`;`p+2`;`p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1602 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1 * 4 + p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;`p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1603 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1 * 4 + p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;`p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1604 THEN THAYTHEL_ASM_TAC(73-40)[`p+2`][]
1605 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`( p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1606 THEN THAYTHEL_ASM_TAC(1)[`p+3`][h0;cstab]
1607 THEN REAL_ARITH_TAC;
1608
1609
1610
1611 (*************CASES a 3 0 NOT = 2************)
1612
1613
1614 MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1615 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1616 THEN MRESA_TAC A_NOT_EQ2_IMP_B [`s`;`p+3`]
1617 THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p+3`;`4`;`s`]
1618 THEN MRESAL_TAC B_LE_2h0_2_SCS_M_4_1[`s`;`p`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`]
1619 THEN MRESA_TAC B_LE_2h0_IMP_B[`s`;`p+2`]
1620 THEN MP_TAC YEBWJNG
1621 THEN RESA_TAC
1622 THEN THAYTHEL_TAC 0[`s`;`v`;`p+2`][IN];
1623
1624
1625
1626 MP_TAC TUAPYYU
1627 THEN RESA_TAC
1628 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][IN];
1629
1630
1631 MP_TAC Jotswix.LEMMA_PWE3
1632 THEN RESA_TAC
1633 THEN THAYTHEL_TAC 0[`s`;`v`;`p`][scs_generic;IN;REAL_ARITH`a<=a`;scs_is_str]
1634 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1635 THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
1636 THEN MP_TAC Cuxvzoz.CJBDXXN
1637 THEN RESA_TAC
1638 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+1`;`v`]
1639 THEN ONCE_REWRITE_TAC[DIST_SYM]
1640 THEN MATCH_DICH_TAC 0
1641 THEN ASM_SIMP_TAC[]
1642 THEN REWRITE_TAC[GSYM ADD1]
1643 THEN ASM_REWRITE_TAC[scs_generic]
1644 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1645 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
1646 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+1)`;`v`;`(p+1)`;`4`]
1647 ;
1648
1649 DICH_TAC(67-17)
1650 THEN ASM_REWRITE_TAC[scs_is_str]
1651 THEN RESA_TAC
1652 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][]
1653 THEN THAYTHE_TAC 0[`v (p)`]
1654 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) <= pi
1655 /\ ~(azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) = pi)
1656 ==> azim (vec 0) (v (p + 1)) (v (p + 2)) ((v:num->real^3) p) < pi`)
1657 THEN RESA_TAC
1658 THEN ONCE_REWRITE_TAC[DIST_SYM]
1659 THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
1660  &2 * #1.26 <= #3.01`]
1661 THEN REPEAT STRIP_TAC;
1662
1663
1664
1665 THAYTHES_TAC(69-5)[`p`;`p+2`][SCS_DIAG_4_ADD0]
1666 THEN DICH_TAC 1
1667 THEN REWRITE_TAC[cstab]
1668 THEN REAL_ARITH_TAC;
1669
1670 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1671 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
1672 THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+2)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 2 MOD 4)`]
1673 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
1674 THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+0)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
1675 THEN DICH_TAC 0
1676 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`]
1677 THEN RESA_TAC
1678 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+1)`;`v(p+2)`;`v p`]
1679 THEN ASM_REWRITE_TAC[DIHV_SYM];
1680
1681
1682
1683
1684 MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1685 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1686 THEN ASM_TAC
1687 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1688 THEN REPEAT RESA_TAC
1689 ;
1690
1691
1692
1693 MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1694 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1695 THEN ASM_TAC
1696 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1697 THEN REPEAT RESA_TAC
1698 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;h0]
1699 THEN REAL_ARITH_TAC;
1700
1701
1702
1703 (*************CASES 1 2= cstab **************)
1704
1705
1706 MP_TAC Jotswix.LEMMA_PWE3
1707 THEN RESA_TAC
1708 THEN THAYTHEL_TAC 0[`s`;`v`;`p`][scs_generic;IN;REAL_ARITH`a<=a/\ &2 * #1.26 <= #3.01`;scs_is_str;h0;cstab]
1709 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1710 THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
1711 THEN MP_TAC Cuxvzoz.CJBDXXN
1712 THEN RESA_TAC
1713 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+1`;`v`]
1714 THEN ONCE_REWRITE_TAC[DIST_SYM]
1715 THEN MATCH_DICH_TAC 0
1716 THEN ASM_SIMP_TAC[]
1717 THEN REWRITE_TAC[GSYM ADD1]
1718 THEN ASM_REWRITE_TAC[scs_generic]
1719 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1720 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
1721 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+1)`;`v`;`(p+1)`;`4`]
1722 ;
1723
1724 DICH_TAC(67-17)
1725 THEN ASM_REWRITE_TAC[scs_is_str]
1726 THEN RESA_TAC
1727 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+1)`][]
1728 THEN THAYTHE_TAC 0[`v (p)`]
1729 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) <= pi
1730 /\ ~(azim (vec 0) (v (p + 1)) (v (p + 2)) (v p) = pi)
1731 ==> azim (vec 0) (v (p + 1)) (v (p + 2)) ((v:num->real^3) p) < pi`)
1732 THEN RESA_TAC
1733 THEN ONCE_REWRITE_TAC[DIST_SYM]
1734 THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
1735  &2 * #1.26 <= #3.01`]
1736 THEN REPEAT STRIP_TAC;
1737
1738
1739
1740 THAYTHES_TAC(69-5)[`p`;`p+2`][SCS_DIAG_4_ADD0]
1741 THEN DICH_TAC 1
1742 THEN REWRITE_TAC[cstab]
1743 THEN REAL_ARITH_TAC;
1744
1745 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1746 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
1747 THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+2)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 2 MOD 4)`]
1748 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+2)`;`V`]
1749 THEN THAYTHES_TAC 0[`v (p+1)`;`v (p+0)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
1750 THEN DICH_TAC 0
1751 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`]
1752 THEN RESA_TAC
1753 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+1)`;`v(p+2)`;`v p`]
1754 THEN ASM_REWRITE_TAC[DIHV_SYM];
1755
1756
1757
1758
1759 MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1760 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1761 THEN ASM_TAC
1762 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1763 THEN REPEAT RESA_TAC
1764 ;
1765
1766
1767
1768 MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`(1 * 4 + p)`;`s`;`p+1`;`(1 * 4 + p) MOD 4`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1769 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+1)`;`p MOD 4`;`s`;`p+1`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1770 THEN ASM_TAC
1771 THEN REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;is_scs_v39]
1772 THEN REPEAT RESA_TAC
1773 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;h0]
1774 THEN REAL_ARITH_TAC;
1775
1776
1777 REAL_ARITH_TAC;
1778
1779
1780 REAL_ARITH_TAC;
1781
1782
1783
1784 (*********scs_is_str p+1***********)
1785
1786
1787
1788
1789 MRESAL_TAC NOT_STR_IN_CASES_4_1[`p`;`s`;`v`][IN]
1790 THEN DICH_TAC 3
1791 THEN ASM_REWRITE_TAC[scs_is_str;]
1792 THEN STRIP_TAC
1793 THEN DICH_TAC(21-13)
1794 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;]
1795 THEN STRIP_TAC
1796 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
1797 THEN THAYTHE_TAC 1[`p+1`;`(p+2)`]
1798 ;
1799
1800
1801 MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
1802 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
1803 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
1804 THEN RESA_TAC
1805 THEN POP_ASSUM MP_TAC
1806 THEN REWRITE_TAC[NOT_EXISTS_THM]
1807 THEN STRIP_TAC
1808 THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (p)) V' E')` ASSUME_TAC;
1809
1810
1811
1812 REPEAT RESA_TAC
1813 ;
1814
1815
1816 ASSUME_TAC(ARITH_RULE`(p+1)+1=p+2/\ (p+1)+3= 1*4+p/\ (p+3)+1= 1*4+p/\ (p+3)+2= 1*4+p+1/\ (p+3)+3= 1*4+p+2`)
1817 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1818 THEN THAYTHES_TAC 0[`1*4+p`;`p`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1819 THEN DICH_TAC(32-20)
1820 THEN RESA_TAC
1821 THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v (p+1)`;`v (p+2)`;`(v:num->real^3) (p)`]
1822 THEN POP_ASSUM MP_TAC
1823 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
1824 THEN STRIP_TAC
1825 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
1826 THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
1827 THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
1828 THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
1829 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+2)`;`V`]
1830 THEN SUBGOAL_THEN`(!j. ~(v j = v (p)) ==> ~collinear {vec 0, (v:num->real^3) (p ), v j})`ASSUME_TAC
1831 ;
1832
1833 REPEAT RESA_TAC
1834 THEN DICH_TAC 0
1835 THEN REWRITE_TAC[]
1836 THEN MATCH_DICH_TAC 1
1837 THEN ASM_SIMP_TAC[]
1838 THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
1839 THEN SET_TAC[];
1840
1841
1842 MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p`][ARITH_RULE`0+2=2`]
1843 THEN DICH_TAC 0
1844 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
1845 THEN STRIP_TAC
1846 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1847 THEN THAYTHES_TAC 3[`v (p+0)`;`v(p+2)`][SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(0 MOD 4 = 2 MOD 4)`]
1848 THEN DICH_TAC 0
1849 THEN REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
1850 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`]
1851 THEN STRIP_TAC
1852 THEN MP_TAC CONDTION_A_LT_B
1853 THEN RESA_TAC
1854 THEN MP_TAC(REAL_ARITH`scs_a_v39 s (p+1) (p+2) <= dist (v (p+1),v (p+2))
1855 ==> scs_a_v39 s (p+1) (p+2) = dist (v (p+1),v (p+2))\/ scs_a_v39 s  (p+1) (p+2) < dist (v (p+1),(v:num->real^3) (p+2))`)
1856 THEN RESA_TAC
1857 ;
1858
1859
1860
1861
1862
1863 SUBGOAL_THEN`dist (v (p + 1),(v:num->real^3) (p+2)) < scs_b_v39 s (p + 1) (p+2)`
1864 ASSUME_TAC
1865 ;
1866
1867 THAYTHE_TAC 1[`p+1`]
1868 THEN DICH_TAC 0
1869 ;
1870
1871 MRESAS_TAC NUXCOEAv2[`s`;`4`;`v`;`p+1`;`p+2`][MOD_MULT_ADD;BASIC_IMP_NOT_J]
1872 THEN DICH_TAC 0
1873 THEN ONCE_REWRITE_TAC[DIST_SYM]
1874 THEN MRESA_TAC SCS_A_SYM[`s`;`1*4+p`;`p+1`]
1875 THEN MRESA_TAC SCS_A_SYM[`s`;`p+1`;`p+2`]
1876 THEN MRESA_TAC SCS_B_SYM[`s`;`p+1`;`p+2`]
1877 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;`(p+1)`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1878 THEN ASM_SIMP_TAC[DIST_SYM];
1879
1880
1881 MP_TAC(SET_RULE`~(&2=norm ((v:num->real^3) (p+1)))\/ norm (v (p+1))= &2`)
1882 THEN RESA_TAC
1883 ;
1884
1885 MRESAS_TAC IMJXPHRv2[`s`;`4`;`v`;`p+1`;][MOD_MULT_ADD;BASIC_IMP_NOT_J]
1886 THEN DICH_TAC 0
1887 THEN MRESA_TAC SCS_A_SYM[`s`;`1*4+p`;`p+1`]
1888 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;`(p+1)`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1889 THEN ASM_SIMP_TAC[DIST_SYM];
1890
1891
1892
1893
1894
1895
1896
1897 MP_TAC(SET_RULE`(scs_a_v39 s (p+3) (p) = &2 )\/ ~((scs_a_v39 s (p+3) (p) = &2 ))`)
1898 THEN RESA_TAC;
1899
1900
1901
1902 MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;` p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1903 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;` p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1904 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p+2)`;`(p+3)`;`s`;`p+2`;` p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1905 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;` p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1906 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p+2)`;`(p+3)`;`s`;`p+2`;` p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1907 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;` p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1908 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p)`;`(1 * 4 + p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1909 THEN MRESAL_TAC STR_MOD_EQ[`4`;`s`;`v`;`1*4+p`][IN;MOD_MULT_ADD]
1910 THEN MRESAL_TAC STR_MOD_EQ[`4`;`s`;`v`;`p`][IN;MOD_MULT_ADD]
1911 THEN MP_TAC  YEBWJNG
1912 THEN RESA_TAC
1913 THEN THAYTHEL_TAC 0[`s`;`v`;`p+3`][IN;ARITH_RULE`(p+1)+1=p+2`]
1914 THEN THAYTHEL_ASM_TAC (55-42)[`p+1`][]
1915 THEN THAYTHEL_TAC 0[`p+2`][ARITH_RULE`(i+2)+1=i+3`]
1916 THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+3`]
1917 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(1 * 4 + p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1918 THEN THAYTHES_TAC (58-40)[`(1 * 4 + p+1)`;`p+1`][MOD_MULT_ADD]
1919 THEN MP_TAC Cqaoqlr.CQAOQLR
1920 THEN RESA_TAC
1921 THEN THAYTHES_TAC 0[`s`;`v`;`p+3`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1922 THEN MATCH_DICH_TAC 0
1923 THEN REWRITE_TAC[h0]
1924 THEN REAL_ARITH_TAC;
1925
1926
1927
1928 ASSUME_TAC(ARITH_RULE`(p+1)+1=p+2/\ (p+2)+1=p+3/\ (p+2)+3=1*4+p+1/\ (p+1)+3=1*4+p/\ (p+3)+1=1*4+p/\ (p+3)+3=1*4+p+2/\ (p+3)+2=1*4+p+1/\ (p+1)+2=p+3`)
1929 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;` p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1930 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;` p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1931 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p+2)`;`(p+3)`;`s`;`p+2`;` p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1932 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p+1)`;`(1 * 4 + p+2)`;`s`;`p+1`;` p+2`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1933 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p+2)`;`(p+3)`;`s`;`p+2`;` p+3`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1934 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;` p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1935 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(1*4+p)`;`(1 * 4 + p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1936 THEN MRESA_TAC A_NOT_EQ2_IMP_B[`s`;`p+3`]
1937 THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`1*4+p+2`][IN;MOD_MULT_ADD]
1938 THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`p+2`][IN;MOD_MULT_ADD;MOD_REFL]
1939 THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`1*4+p`][IN;MOD_MULT_ADD]
1940 THEN MRESAS_TAC STR_MOD_EQ[`4`;`s`;`v`;`p`][IN;MOD_MULT_ADD;MOD_REFL]
1941 ;
1942
1943 THAYTHES_TAC (59-40)[`1 * 4 + p + 2`;`p+2`][MOD_MULT_ADD]
1944 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1945 THEN THAYTHES_TAC 0[`1*4+p+1`;`p+1`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1946 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
1947 THEN THAYTHES_TAC 0[`1*4+p+3`;`p+3`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1948 THEN MP_TAC WKZZEEH
1949 THEN RESA_TAC
1950 THEN THAYTHE_TAC 0[`s`;`v`;`p+3`]
1951 THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p+3`;`4`;`s`]
1952 THEN MP_TAC(SET_RULE`scs_a_v39 s (p + 1) (p+2) = &2 \/ ~(scs_a_v39 s (p + 1) (p+2) = &2 )`)
1953 THEN RESA_TAC;
1954
1955 (**********CASES a 1 2 =2********************)
1956
1957
1958 MP_TAC TUAPYYU
1959 THEN RESA_TAC
1960 THEN THAYTHEL_TAC 0[`s`;`v`;`p+3`][IN];
1961
1962
1963
1964
1965
1966
1967 MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
1968 THEN MP_TAC Jotswix.LEMMA_PWE2
1969 THEN RESA_TAC
1970 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][scs_generic;IN;REAL_ARITH`a<=a`;]
1971 THEN DICH_TAC 0
1972 THEN ASM_REWRITE_TAC[scs_is_str]
1973 THEN STRIP_TAC
1974 THEN MP_TAC Cuxvzoz.CUXVZOZ
1975 THEN RESA_TAC
1976 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p`;`v`]
1977 THEN MATCH_DICH_TAC 0
1978 THEN ASM_SIMP_TAC[]
1979 THEN REWRITE_TAC[GSYM ADD1]
1980 THEN ASM_REWRITE_TAC[scs_generic]
1981 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
1982 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
1983 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
1984 ;
1985
1986 DICH_TAC(69-17)
1987 THEN ASM_REWRITE_TAC[scs_is_str]
1988 THEN RESA_TAC
1989 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][]
1990 THEN THAYTHE_TAC 0[`v (p+3)`]
1991 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) <= pi
1992 /\ ~(azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) = pi)
1993 ==> azim (vec 0) (v p) (v (p + 1)) ((v:num->real^3) (p + 3))  < pi`)
1994 THEN RESA_TAC
1995 THEN ONCE_REWRITE_TAC[DIST_SYM]
1996 THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
1997  &2 * #1.26 <= #3.01`]
1998 THEN REPEAT STRIP_TAC;
1999
2000
2001
2002 THAYTHES_TAC(71-5)[`p+1`;`p+3`][SCS_DIAG_4_ADD2]
2003 THEN DICH_TAC 1
2004 THEN REWRITE_TAC[cstab]
2005 THEN REAL_ARITH_TAC;
2006
2007
2008
2009 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2010 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+1)`;`V`]
2011 THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+1)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
2012 THEN DICH_TAC 0
2013 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
2014 THEN RESA_TAC
2015 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+3)`;`V`]
2016 THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+3)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 0 MOD 4)`]
2017 THEN DICH_TAC 0
2018 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
2019 THEN RESA_TAC
2020 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v p`;`v(p+1)`;`v (p+3)`]
2021 ;
2022
2023
2024
2025
2026
2027
2028
2029
2030 DICH_TAC 3
2031 THEN RESA_TAC
2032 THEN POP_ASSUM MP_TAC
2033 THEN ONCE_REWRITE_TAC[DIST_SYM]
2034 THEN STRIP_TAC
2035 THEN MP_TAC TUAPYYU_IMP_CASES
2036 THEN RESA_TAC
2037 THEN THAYTHEL_TAC 0[`s`;`v`;`p+2`][IN];
2038
2039
2040 (************CASES 2 3= 2**********)
2041
2042
2043 MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2044 THEN MP_TAC Jotswix.LEMMA_PWE1
2045 THEN RESA_TAC
2046 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][scs_generic;IN;REAL_ARITH`a<=a/\ &2 <= &2 * #1.26`;h0]
2047 THEN DICH_TAC 0
2048 THEN ASM_REWRITE_TAC[scs_is_str]
2049 THEN STRIP_TAC
2050 THEN MP_TAC Cuxvzoz.CJBDXXN
2051 THEN RESA_TAC
2052 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+2`;`v`]
2053 THEN DICH_TAC 0
2054 THEN ONCE_REWRITE_TAC[DIST_SYM]
2055 THEN ASM_SIMP_TAC[]
2056 THEN REWRITE_TAC[GSYM ADD1]
2057 THEN ASM_REWRITE_TAC[scs_generic]
2058 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
2059 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+2)`;`(1 * 4 + p+1)`;`s`;`p+2`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2060 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2)`;`(1 * 4 + p+1)`;`s`;`p+2`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2061 THEN MRESA_TAC SCS_A_SYM[`s`;`p+1`;`p+2`]
2062 THEN MRESA_TAC SCS_B_SYM[`s`;`p+1`;`p+2`]
2063 THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+1`]
2064 THEN ONCE_REWRITE_TAC[DIST_SYM]
2065 THEN ASM_SIMP_TAC[REAL_ARITH`a<=a`]
2066 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+2)`;`v`;`(p+2)`;`4`]
2067 ;
2068
2069 DICH_TAC(75-18)
2070 THEN ASM_REWRITE_TAC[scs_is_str]
2071 THEN RESA_TAC
2072 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+2)`][]
2073 THEN THAYTHE_TAC 0[`v (p+1)`]
2074 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) <= pi
2075 /\ ~(azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) = pi)
2076 ==> azim (vec 0) (v (p + 2)) (v (p + 3)) ((v:num->real^3) (p + 1)) < pi`)
2077 THEN RESA_TAC
2078 THEN ONCE_REWRITE_TAC[DIST_SYM]
2079 THEN SUBGOAL_THEN`&3 <= dist ((v:num->real^3) (p+1),v (p + 3))`ASSUME_TAC
2080 ;
2081
2082
2083
2084
2085 THAYTHES_TAC(77-5)[`p+1`;`p+3`][SCS_DIAG_4_ADD2]
2086 THEN DICH_TAC 1
2087 THEN REWRITE_TAC[cstab]
2088 THEN REAL_ARITH_TAC;
2089
2090 SUBGOAL_THEN`(pi / &2 < azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) \/
2091    azim (vec 0) ((v:num->real^3) (p + 1)) (rho_node1 FF (v (p + 1)))
2092    (ivs_rho_node1 FF (v (p + 1))) <
2093    pi)`ASSUME_TAC
2094 ;
2095
2096
2097
2098
2099
2100 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2101 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+2)`;`v (p+1)`;`V`]
2102 THEN THAYTHES_TAC 0[`v (p+2)`;`v (p+1)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 2 MOD 4)`]
2103 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+2)`;`v (p+3)`;`V`]
2104 THEN THAYTHES_TAC 0[`v (p+2)`;`v (p+3)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 2 MOD 4)`]
2105 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+2)`;`v(p+3)`;`v (p+1)`]
2106 ;
2107
2108
2109 ASM_REWRITE_TAC[cstab;REAL_ARITH`&2 <= #3.01`]
2110 THEN STRIP_TAC
2111 THEN MP_TAC Cqaoqlr.CQAOQLR
2112 THEN RESA_TAC
2113 THEN THAYTHES_TAC 0[`s`;`v`;`p`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
2114 THEN MATCH_DICH_TAC 0
2115 THEN THAYTHEL_ASM_TAC(80-40)[`p+2`][h0;cstab]
2116 THEN REAL_ARITH_TAC;
2117
2118 (************CASES 2 3= 2* H0**********)
2119
2120
2121
2122
2123 MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2124 THEN MP_TAC Jotswix.LEMMA_PWE1
2125 THEN RESA_TAC
2126 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][scs_generic;IN;REAL_ARITH`a<=a/\ &2 <= &2 * #1.26`;h0]
2127 THEN DICH_TAC 0
2128 THEN ASM_REWRITE_TAC[scs_is_str]
2129 THEN STRIP_TAC
2130 THEN MP_TAC Cuxvzoz.CJBDXXN
2131 THEN RESA_TAC
2132 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p+2`;`v`]
2133 THEN DICH_TAC 0
2134 THEN ONCE_REWRITE_TAC[DIST_SYM]
2135 THEN ASM_SIMP_TAC[]
2136 THEN REWRITE_TAC[GSYM ADD1]
2137 THEN ASM_REWRITE_TAC[scs_generic]
2138 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
2139 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+2)`;`(1 * 4 + p+1)`;`s`;`p+2`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2140 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+2)`;`(1 * 4 + p+1)`;`s`;`p+2`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2141 THEN MRESA_TAC SCS_A_SYM[`s`;`p+1`;`p+2`]
2142 THEN MRESA_TAC SCS_B_SYM[`s`;`p+1`;`p+2`]
2143 THEN MRESA_TAC A_EQ2_IMP_B[`s`;`p+1`]
2144 THEN ONCE_REWRITE_TAC[DIST_SYM]
2145 THEN ASM_SIMP_TAC[REAL_ARITH`a<=a`]
2146 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v (p+2)`;`v`;`(p+2)`;`4`]
2147 ;
2148
2149 DICH_TAC(75-18)
2150 THEN ASM_REWRITE_TAC[scs_is_str]
2151 THEN RESA_TAC
2152 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v (p+2)`][]
2153 THEN THAYTHE_TAC 0[`v (p+1)`]
2154 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) <= pi
2155 /\ ~(azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) = pi)
2156 ==> azim (vec 0) (v (p + 2)) (v (p + 3)) ((v:num->real^3) (p + 1)) < pi`)
2157 THEN RESA_TAC
2158 THEN ONCE_REWRITE_TAC[DIST_SYM]
2159 THEN SUBGOAL_THEN`&3 <= dist ((v:num->real^3) (p+1),v (p + 3))`ASSUME_TAC
2160 ;
2161
2162
2163
2164
2165 THAYTHES_TAC(77-5)[`p+1`;`p+3`][SCS_DIAG_4_ADD2]
2166 THEN DICH_TAC 1
2167 THEN REWRITE_TAC[cstab]
2168 THEN REAL_ARITH_TAC;
2169
2170 SUBGOAL_THEN`(pi / &2 < azim (vec 0) (v (p + 2)) (v (p + 3)) (v (p + 1)) \/
2171    azim (vec 0) ((v:num->real^3) (p + 1)) (rho_node1 FF (v (p + 1)))
2172    (ivs_rho_node1 FF (v (p + 1))) <
2173    pi)`ASSUME_TAC
2174 ;
2175
2176
2177
2178
2179
2180 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2181 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+2)`;`v (p+1)`;`V`]
2182 THEN THAYTHES_TAC 0[`v (p+2)`;`v (p+1)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 2 MOD 4)`]
2183 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+2)`;`v (p+3)`;`V`]
2184 THEN THAYTHES_TAC 0[`v (p+2)`;`v (p+3)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 2 MOD 4)`]
2185 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v (p+2)`;`v(p+3)`;`v (p+1)`]
2186 ;
2187
2188
2189 ASM_REWRITE_TAC[cstab;REAL_ARITH`&2 <= &2 * #1.26 /\ &2 * #1.26 <= #3.01`;h0]
2190 THEN STRIP_TAC
2191 THEN MP_TAC Cqaoqlr.CQAOQLR
2192 THEN RESA_TAC
2193 THEN THAYTHES_TAC 0[`s`;`v`;`p`][scs_generic;IN;A_EQ2_IMP_B;REAL_ARITH`a<=a`]
2194 THEN MATCH_DICH_TAC 0
2195 THEN THAYTHEL_ASM_TAC(80-40)[`p+2`][h0;cstab]
2196 THEN REAL_ARITH_TAC;
2197
2198
2199 (*************CASES a 1 2 NOT = 2************)
2200
2201
2202 MRESA_TAC A_NOT_EQ2_IMP_B [`s`;`p+1`]
2203 THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p+1`;`4`;`s`]
2204 THEN MRESAL_TAC B_LE_2h0_2_SCS_M_4_1[`s`;`p`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`]
2205 THEN MRESA_TAC B_LE_2h0_IMP_B[`s`;`p+2`]
2206 THEN MP_TAC YEBWJNG
2207 THEN RESA_TAC
2208 THEN THAYTHEL_TAC 0[`s`;`v`;`p+2`][IN];
2209
2210
2211
2212 MP_TAC TUAPYYU
2213 THEN RESA_TAC
2214 THEN THAYTHEL_TAC 0[`s`;`v`;`p+3`][IN];
2215
2216
2217 MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2218 THEN MP_TAC Jotswix.LEMMA_PWE4
2219 THEN RESA_TAC
2220 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][scs_generic;IN;REAL_ARITH`a<=a`;]
2221 THEN DICH_TAC 0
2222 THEN ONCE_REWRITE_TAC[DIST_SYM]
2223 THEN ASM_REWRITE_TAC[scs_is_str;REAL_ARITH`a<=a`]
2224 THEN STRIP_TAC
2225 THEN ONCE_REWRITE_TAC[DIST_SYM]
2226 ;
2227
2228
2229
2230
2231 MP_TAC Cuxvzoz.CUXVZOZ
2232 THEN RESA_TAC
2233 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p`;`v`]
2234 THEN MATCH_DICH_TAC 0
2235 THEN ASM_SIMP_TAC[]
2236 THEN REWRITE_TAC[GSYM ADD1]
2237 THEN ASM_REWRITE_TAC[scs_generic]
2238 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
2239 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
2240 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
2241 ;
2242
2243 DICH_TAC(76-17)
2244 THEN ASM_REWRITE_TAC[scs_is_str]
2245 THEN RESA_TAC
2246 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][]
2247 THEN THAYTHE_TAC 0[`v (p+3)`]
2248 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) <= pi
2249 /\ ~(azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) = pi)
2250 ==> azim (vec 0) (v p) (v (p + 1)) ((v:num->real^3) (p + 3))  < pi`)
2251 THEN RESA_TAC
2252 THEN ONCE_REWRITE_TAC[DIST_SYM]
2253 THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
2254  &2 * #1.26 <= #3.01`]
2255 THEN REPEAT STRIP_TAC;
2256
2257
2258
2259 THAYTHES_TAC(78-5)[`p+1`;`p+3`][SCS_DIAG_4_ADD2]
2260 THEN DICH_TAC 1
2261 THEN REWRITE_TAC[cstab]
2262 THEN REAL_ARITH_TAC;
2263
2264
2265
2266 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2267 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+1)`;`V`]
2268 THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+1)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
2269 THEN DICH_TAC 0
2270 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
2271 THEN RESA_TAC
2272 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+3)`;`V`]
2273 THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+3)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 0 MOD 4)`]
2274 THEN DICH_TAC 0
2275 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
2276 THEN RESA_TAC
2277 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v p`;`v(p+1)`;`v (p+3)`]
2278 ;
2279
2280
2281
2282 (*************CASES 0 3= cstab **************)
2283
2284
2285
2286 MRESAS_TAC CHANGE_A_SCS_MOD[`(1*4+p)`;`(p+1)`;`s`;`p`;` p+1`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2287 THEN MP_TAC Jotswix.LEMMA_PWE4
2288 THEN RESA_TAC
2289 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][scs_generic;IN;REAL_ARITH`a<=a`;]
2290 THEN DICH_TAC 0
2291 THEN ONCE_REWRITE_TAC[DIST_SYM]
2292 THEN ASM_REWRITE_TAC[scs_is_str;REAL_ARITH`&2 * #1.26 <= #3.01`;h0;cstab]
2293 THEN STRIP_TAC
2294 THEN ONCE_REWRITE_TAC[DIST_SYM]
2295 ;
2296
2297 MP_TAC Cuxvzoz.CUXVZOZ
2298 THEN RESA_TAC
2299 THEN THAYTHE_TAC 0[`s`;`FF`;`4`;`p`;`v`]
2300 THEN MATCH_DICH_TAC 0
2301 THEN ASM_SIMP_TAC[]
2302 THEN REWRITE_TAC[GSYM ADD1]
2303 THEN ASM_REWRITE_TAC[scs_generic]
2304 THEN ASM_SIMP_TAC[A_EQ2_IMP_B;REAL_ARITH`a<=a`]
2305 THEN ASM_REWRITE_TAC[interior_angle1;GSYM ivs_rho_node1;]
2306 THEN MRESA_TAC BB_RHO_NODE_IVS[`V`;`E`;`s`;`FF`;`v p`;`v`;`p`;`4`]
2307 ;
2308
2309 DICH_TAC(76-17)
2310 THEN ASM_REWRITE_TAC[scs_is_str]
2311 THEN RESA_TAC
2312 THEN MRESAL_TAC Local_lemmas.IN_V_IMP_AZIM_LESS_PI[`E`;`V`;`FF`;`v p`][]
2313 THEN THAYTHE_TAC 0[`v (p+3)`]
2314 THEN MP_TAC(REAL_ARITH`azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) <= pi
2315 /\ ~(azim (vec 0) (v p) (v (p + 1)) (v (p + 3)) = pi)
2316 ==> azim (vec 0) (v p) (v (p + 1)) ((v:num->real^3) (p + 3))  < pi`)
2317 THEN RESA_TAC
2318 THEN ONCE_REWRITE_TAC[DIST_SYM]
2319 THEN ASM_REWRITE_TAC[h0;cstab;REAL_ARITH`&2 <= &2 * #1.26 /\
2320  &2 * #1.26 <= #3.01`]
2321 THEN REPEAT STRIP_TAC;
2322
2323
2324
2325 THAYTHES_TAC(78-5)[`p+1`;`p+3`][SCS_DIAG_4_ADD2]
2326 THEN DICH_TAC 1
2327 THEN REWRITE_TAC[cstab]
2328 THEN REAL_ARITH_TAC;
2329
2330
2331
2332 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2333 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+1)`;`V`]
2334 THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+1)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 0 MOD 4)`]
2335 THEN DICH_TAC 0
2336 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
2337 THEN RESA_TAC
2338 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v p`;`v (p+3)`;`V`]
2339 THEN THAYTHES_TAC 0[`v (p+0)`;`v (p+3)`][SET_RULE`a IN {a,b}`;SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(3 MOD 4 = 0 MOD 4)`]
2340 THEN DICH_TAC 0
2341 THEN ASM_REWRITE_TAC[ARITH_RULE`a+0=a`;SET_RULE`a IN {a,b}`]
2342 THEN RESA_TAC
2343 THEN MRESA_TAC AZIM_DIHV_SAME_STRONG[`vec 0:real^3`;`v p`;`v(p+1)`;`v (p+3)`]
2344 ;
2345
2346
2347
2348
2349 REAL_ARITH_TAC;
2350
2351 ]);;
2352
2353
2354
2355 let h0_CSTAB_LT_4=prove(`&2< &2*h0 /\ cstab< &4/\ &2<= &2*h0 /\ cstab<= &4
2356 /\ &2*h0< &4/\ &2< &4`,
2357 REWRITE_TAC[cstab;h0]
2358 THEN REAL_ARITH_TAC);;
2359
2360
2361
2362
2363
2364
2365
2366 let VASYYAU= prove_by_refinement(`
2367 main_nonlinear_terminal_v11 ==>
2368 (!s v p.
2369     is_scs_v39 s /\ scs_basic_v39 s /\ scs_k_v39 s = 4 /\ MMs_v39 s v/\
2370     (!i j. scs_diag 4 i j ==> scs_a_v39 s i j <= cstab /\ cstab < dist(v i,v j) /\ &4*h0 < scs_b_v39 s i j) /\
2371     (!i. (scs_a_v39 s i (i+1) = &2 /\ scs_b_v39 s i (i+1)= &2*h0) \/
2372        (scs_a_v39 s i (i+1) = &2 * h0 /\ scs_b_v39 s i (i+1)= cstab)) /\
2373     scs_is_str s v p
2374     ==> (dist(v p,v (p+1)) = scs_a_v39 s p (p+1) /\ dist(v p,v (p+3)) = scs_a_v39 s p (p+3)))`,
2375 [STRIP_TAC
2376 THEN REPEAT GEN_TAC
2377 THEN STRIP_TAC
2378 THEN ABBREV_TAC`V= IMAGE (v:num->real^3) (:num)`
2379 THEN ABBREV_TAC`E = IMAGE (\i. {(v:num->real^3) i, v (SUC i)}) (:num)`
2380 THEN ABBREV_TAC`FF = IMAGE (\i. ((v:num->real^3) i, v (SUC i))) (:num)`
2381 THEN ASM_TAC
2382 THEN REPLICATE_TAC 11 (RESA_TAC)
2383 THEN ASSUME_TAC(ARITH_RULE`3<4/\ 1<4/\ ~(4=0)/\ 4-1=3/\ SUC (p + 3)= 1*4+p/\ SUC p= p+1`)
2384 THEN ASM_SIMP_TAC[]
2385 THEN MRESAL_TAC GSXRFWM[`s`;`v`][IN;scs_generic]
2386 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
2387 THEN MRESA_TAC Imjxphr.BBS_IMP_CONVEX_LOCAL_FAN[`4`;`s`;`v`]
2388 THEN MP_TAC Local_lemmas.CVLF_LF_F
2389 THEN RESA_TAC
2390 THEN MP_TAC Tfitskc.SCS_DIAG_A_LE_DIST
2391 THEN RESA_TAC
2392 THEN MP_TAC Jlxfdmj.SCS_A_2
2393 THEN RESA_TAC
2394 THEN THAYTHE_TAC 0[`p`]
2395 THEN MP_TAC(REAL_ARITH`&2 <= scs_a_v39 s p (p + 1)
2396 ==> scs_a_v39 s p (p+1) = &2\/ &2 < scs_a_v39 s p (p + 1)`)
2397 THEN RESA_TAC;
2398
2399
2400 MP_TAC PWEIWBZ
2401 THEN RESA_TAC
2402 THEN THAYTHE_TAC 0[`s`;`v`;`p`]
2403 THEN DICH_TAC(20-7)
2404 THEN ASM_REWRITE_TAC[scs_is_str]
2405 THEN STRIP_TAC;
2406
2407
2408 MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
2409 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
2410 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
2411 THEN RESA_TAC
2412 THEN POP_ASSUM MP_TAC
2413 THEN REWRITE_TAC[NOT_EXISTS_THM]
2414 THEN STRIP_TAC
2415 THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (p)) V' E')` ASSUME_TAC;
2416
2417
2418
2419
2420 REPEAT RESA_TAC
2421 ;
2422
2423
2424
2425 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2426 THEN THAYTHES_TAC 0[`(p+3)+1`;`p`][ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2427 THEN DICH_TAC 0
2428 THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p=(p+3)+1`]
2429 THEN STRIP_TAC
2430 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2431 THEN THAYTHES_TAC 0[`(p+3)+2`;`p+1`][ARITH_RULE`(p+3)+2=1*4+p+1`;MOD_MULT_ADD]
2432 THEN DICH_TAC 0
2433 THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p+1=(p+3)+2`]
2434 THEN STRIP_TAC
2435 THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v p`;`v (p+1)`;`(v:num->real^3) (p+3)`]
2436 THEN POP_ASSUM MP_TAC
2437 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
2438 THEN STRIP_TAC
2439 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
2440 THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
2441 THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
2442 THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
2443 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+3)`;`V`]
2444 THEN SUBGOAL_THEN`(!j. ~(v j = v (p + 3)) ==> ~collinear {vec 0, (v:num->real^3) (p + 3), v j})`ASSUME_TAC
2445 ;
2446
2447
2448 REPEAT RESA_TAC
2449 THEN DICH_TAC 0
2450 THEN REWRITE_TAC[]
2451 THEN MATCH_DICH_TAC 1
2452 THEN ASM_SIMP_TAC[]
2453 THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
2454 THEN SET_TAC[];
2455
2456
2457
2458 MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p+3`][ARITH_RULE`0+2=2`]
2459 THEN DICH_TAC 0
2460 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
2461 THEN STRIP_TAC
2462 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2463 THEN THAYTHES_TAC 3[`v (p+1)`;`v(p+3)`][SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 3 MOD 4)`]
2464 THEN MP_TAC CONDTION_A_LT_B
2465 THEN RESA_TAC;
2466
2467
2468
2469 MRESAS_TAC NUXCOEAv2[`s`;`4`;`v`;`p`;`p+1`][MOD_MULT_ADD;BASIC_IMP_NOT_J]
2470 THEN DICH_TAC 0
2471 THEN MRESA_TAC SCS_A_SYM[`s`;`p`;`p+1`]
2472 THEN MRESA_TAC SCS_B_SYM[`s`;`p`;`p+1`]
2473 THEN ONCE_REWRITE_TAC[DIST_SYM]
2474 THEN ASM_REWRITE_TAC[]
2475 THEN THAYTHE_TAC 2[`p`]
2476 THEN RESA_TAC;
2477
2478 ASSUME_TAC(ARITH_RULE`(p+3)+1=1*4+p/\ (p+1)+1=p+2/\ (p+2)+1=p+3`)
2479 THEN MRESAS_TAC CHANGE_A_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2480 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2481 THEN THAYTHES_TAC 0[`1*4+p`;`p`][MOD_MULT_ADD]
2482 THEN MP_TAC Jlxfdmj.SCS_A_2
2483 THEN RESA_TAC
2484 THEN THAYTHE_TAC 0[`p+3`]
2485 THEN MP_TAC(REAL_ARITH`&2 <= scs_a_v39 s (p + 3) p
2486 ==> scs_a_v39 s (p+3) p = &2\/ &2 < scs_a_v39 s (p + 3) p`)
2487 THEN RESA_TAC;
2488
2489
2490 MP_TAC PWEIWBZ
2491 THEN RESA_TAC
2492 THEN THAYTHE_TAC 0[`s`;`v`;`p+3`]
2493 THEN MRESA_TAC SCS_A_SYM[`s`;`p+3`;`p`]
2494 THEN ONCE_REWRITE_TAC[DIST_SYM]
2495 THEN ASM_REWRITE_TAC[]
2496 THEN ONCE_REWRITE_TAC[DIST_SYM]
2497 THEN DICH_TAC(26-7)
2498 THEN ASM_REWRITE_TAC[scs_is_str]
2499 THEN STRIP_TAC;
2500
2501
2502 MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
2503 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
2504 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
2505 THEN RESA_TAC
2506 THEN POP_ASSUM MP_TAC
2507 THEN REWRITE_TAC[NOT_EXISTS_THM]
2508 THEN STRIP_TAC
2509 THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (p)) V' E')` ASSUME_TAC;
2510
2511
2512
2513
2514 REPEAT RESA_TAC
2515 ;
2516
2517
2518
2519 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2520 THEN THAYTHES_TAC 0[`(p+3)+2`;`p+1`][ARITH_RULE`(p+3)+2=1*4+p+1`;MOD_MULT_ADD]
2521 THEN DICH_TAC 0
2522 THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p+1=(p+3)+2`]
2523 THEN STRIP_TAC
2524 THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v p`;`v (p+1)`;`(v:num->real^3) (p+3)`]
2525 THEN POP_ASSUM MP_TAC
2526 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
2527 THEN STRIP_TAC
2528 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
2529 THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
2530 THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
2531 THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
2532 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+3)`;`V`]
2533 THEN SUBGOAL_THEN`(!j. ~(v j = v (p + 3)) ==> ~collinear {vec 0, (v:num->real^3) (p + 3), v j})`ASSUME_TAC
2534 ;
2535
2536
2537 REPEAT RESA_TAC
2538 THEN DICH_TAC 0
2539 THEN REWRITE_TAC[]
2540 THEN MATCH_DICH_TAC 1
2541 THEN ASM_SIMP_TAC[]
2542 THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
2543 THEN SET_TAC[];
2544
2545
2546
2547 MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p+3`][ARITH_RULE`0+2=2`]
2548 THEN DICH_TAC 0
2549 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
2550 THEN STRIP_TAC
2551 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2552 THEN THAYTHES_TAC 3[`v (p+1)`;`v(p+3)`][SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 3 MOD 4)`]
2553 THEN MP_TAC CONDTION_A_LT_B
2554 THEN RESA_TAC;
2555
2556
2557
2558 MRESAS_TAC NUXCOEAv2[`s`;`4`;`v`;`p`;`p+3`][MOD_MULT_ADD;BASIC_IMP_NOT_J]
2559 THEN DICH_TAC 0
2560 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2561 THEN THAYTHE_TAC 1[`p+3`]
2562 THEN RESA_TAC;
2563
2564
2565 MP_TAC(REAL_ARITH`&2 < scs_a_v39 s p (p + 1)
2566 /\ &2 < scs_a_v39 s (p + 3) p
2567 ==> ~(scs_a_v39 s (p + 3) p = &2)/\ ~(scs_a_v39 s p (p + 1)= &2)`)
2568 THEN RESA_TAC
2569 THEN MP_TAC A_NOT_EQ2_IMP_B
2570 THEN RESA_TAC
2571 THEN MRESAS_TAC CHANGE_B_SCS_MOD[`(p+3)`;`(1 * 4 + p)`;`s`;`p+3`;`p`][MOD_REFL;Yxionxl2.MOD_SUC_MOD;ARITH_RULE`(p+3)+1=1*4+p`;MOD_MULT_ADD]
2572 THEN MRESA_TAC  A_NOT_EQ2_IMP_B[`s`;`p+3`]
2573 THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p`;`4`;`s`]
2574 THEN MRESA_TAC PRO_ADD_NOT_IN_SCS_M[`p+3`;`4`;`s`]
2575 THEN MRESAL_TAC B_LE_2h0_2_SCS_M_4[`s`;`p`][SET_RULE`{a,b} SUBSET A<=> a IN A/\ b IN A`]
2576 THEN MRESA_TAC B_LE_2h0_IMP_B[`s`;`p+1`]
2577 THEN MRESA_TAC B_LE_2h0_IMP_B[`s`;`p+2`]
2578 THEN MRESAL_TAC NOT_STR_IN_CASES_4[`p`;`s`;`v`][IN]
2579 THEN MP_TAC YEBWJNG
2580 THEN RESA_TAC
2581 THEN THAYTHEL_TAC 0[`s`;`v`;`p+1`][IN]
2582 THEN MP_TAC YEBWJNG
2583 THEN RESA_TAC
2584 THEN THAYTHEL_TAC 0[`s`;`v`;`p+2`][IN]
2585 THEN DICH_TAC (44-13)
2586 THEN ASM_REWRITE_TAC[LET_DEF;LET_END_DEF;BBs_v39]
2587 THEN RESA_TAC
2588 THEN MRESA_TAC MMS_IMP_BBS[`s`;`v`]
2589 THEN THAYTHEL_ASM_TAC 1[`p`;`p+1`][]
2590 THEN THAYTHE_TAC 0[`p+3`;`p`];
2591
2592
2593
2594 MP_TAC(SET_RULE`~(&2=norm ((v:num->real^3) p))\/ norm (v p)= &2`)
2595 THEN RESA_TAC
2596 ;
2597
2598
2599
2600
2601 DICH_TAC(51-7)
2602 THEN ASM_REWRITE_TAC[scs_is_str]
2603 THEN STRIP_TAC;
2604
2605
2606 MRESAL_TAC MMS_IMP_BBPRIME[`s`;`v`][LET_DEF;LET_END_DEF;BBprime_v39]
2607 THEN MRESAL_TAC JKQEWGV2[`s`;`v`][LET_DEF;LET_END_DEF;scs_generic]
2608 THEN MP_TAC Wrgcvdr_cizmrrh.CIZMRRH
2609 THEN RESA_TAC
2610 THEN POP_ASSUM MP_TAC
2611 THEN REWRITE_TAC[NOT_EXISTS_THM]
2612 THEN STRIP_TAC
2613 THEN SUBGOAL_THEN`(!V' E' v1. V' = V /\ E' = E ==> ~lunar (v1,(v:num->real^3) (p)) V' E')` ASSUME_TAC;
2614
2615
2616
2617
2618 REPEAT RESA_TAC
2619 ;
2620
2621
2622
2623 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2624 THEN THAYTHES_TAC 0[`(p+3)+2`;`p+1`][ARITH_RULE`(p+3)+2=1*4+p+1`;MOD_MULT_ADD]
2625 THEN DICH_TAC 0
2626 THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p+1=(p+3)+2`]
2627 THEN STRIP_TAC
2628 THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v p`;`v (p+1)`;`(v:num->real^3) (p+3)`]
2629 THEN POP_ASSUM MP_TAC
2630 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
2631 THEN STRIP_TAC
2632 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
2633 THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
2634 THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
2635 THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
2636 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+3)`;`V`]
2637 THEN SUBGOAL_THEN`(!j. ~(v j = v (p + 3)) ==> ~collinear {vec 0, (v:num->real^3) (p + 3), v j})`ASSUME_TAC
2638 ;
2639
2640
2641 REPEAT RESA_TAC
2642 THEN DICH_TAC 0
2643 THEN REWRITE_TAC[]
2644 THEN MATCH_DICH_TAC 1
2645 THEN ASM_SIMP_TAC[]
2646 THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
2647 THEN SET_TAC[];
2648
2649
2650
2651 MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p+3`][ARITH_RULE`0+2=2`]
2652 THEN DICH_TAC 0
2653 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
2654 THEN STRIP_TAC
2655 THEN MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2656 THEN THAYTHES_TAC 3[`v (p+1)`;`v(p+3)`][SET_RULE`a IN {a,b}`;Ocbicby.MOD_EQ_MOD_SHIFT;ARITH_RULE`~(1 MOD 4 = 3 MOD 4)`]
2657 THEN MP_TAC CONDTION_A_LT_B
2658 THEN RESA_TAC;
2659
2660
2661
2662 MRESAS_TAC IMJXPHRv2[`s`;`4`;`v`;`p`;][MOD_MULT_ADD;BASIC_IMP_NOT_J]
2663 ;
2664
2665
2666
2667 MRESAS_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`p`][Ckqowsa_3_points.in_ball_annulus;dist]
2668 THEN MRESAS_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`p+1`][Ckqowsa_3_points.in_ball_annulus;dist]
2669 THEN MRESAS_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`p+2`][Ckqowsa_3_points.in_ball_annulus;dist]
2670 THEN MRESAS_TAC WL_IN_BALL_ANNULUS[`s`;`v`;`p+3`][Ckqowsa_3_points.in_ball_annulus;dist]
2671 THEN MRESAL_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`v p`;`v (p+3)`][dist;VECTOR_ARITH`vec 0- A= --A`; NORM_NEG]
2672 THEN MRESAL_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`v (p+1)`;`v (p)`][dist;VECTOR_ARITH`vec 0- A= --A`; NORM_NEG]
2673 THEN MRESAL_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`v (p+1)`;`v (p+2)`][dist;VECTOR_ARITH`vec 0- A= --A`; NORM_NEG]
2674 THEN MRESAL_TAC Trigonometry1.arcVarc[`vec 0:real^3`;`v (p+2)`;`v (p+3)`][dist;VECTOR_ARITH`vec 0- A= --A`; NORM_NEG]
2675 THEN MRESA_TAC Trigonometry.KEITDWB[`vec 0:real^3`;`v (p+1)`;`v (p+3)`;`v (p+2)`];
2676
2677
2678
2679
2680 DICH_TAC(68-7)
2681 THEN ASM_REWRITE_TAC[scs_is_str]
2682 THEN STRIP_TAC;
2683
2684
2685
2686
2687 MRESA_TAC BB_VV_FUN_EQ[`v`;`s`]
2688 THEN THAYTHES_TAC 0[`(p+3)+2`;`p+1`][ARITH_RULE`(p+3)+2=1*4+p+1`;MOD_MULT_ADD]
2689 THEN DICH_TAC 0
2690 THEN REWRITE_TAC[ARITH_RULE`1 * 4 + p+1=(p+3)+2`]
2691 THEN STRIP_TAC
2692 THEN MRESA_TAC Local_lemmas1.AZIM_COND_FOR_COPLANAR[`vec 0:real^3`;`v p`;`v (p+1)`;`(v:num->real^3) (p+3)`]
2693 THEN POP_ASSUM MP_TAC
2694 THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,B,C}`]
2695 THEN STRIP_TAC
2696 THEN MRESA_TAC WL_IN_V[`p`;`v:num->real^3`]
2697 THEN MRESA_TAC WL_IN_V[`p+1`;`v:num->real^3`]
2698 THEN MRESA_TAC WL_IN_V[`p+2`;`v:num->real^3`]
2699 THEN MRESA_TAC WL_IN_V[`p+3`;`v:num->real^3`]
2700 THEN MRESA_TAC Nkezbfc_local.PROPERTIES_GENERIC[`FF`;`E`;`v (p+1)`;`v (p+3)`;`V`]
2701 THEN SUBGOAL_THEN`(!j. ~(v j = v (p + 3)) ==> ~collinear {vec 0, (v:num->real^3) (p + 3), v j})`ASSUME_TAC
2702 ;
2703
2704
2705 REPEAT RESA_TAC
2706 THEN DICH_TAC 0
2707 THEN REWRITE_TAC[]
2708 THEN MATCH_DICH_TAC 1
2709 THEN ASM_SIMP_TAC[]
2710 THEN MRESA_TAC WL_IN_V[`j`;`v:num->real^3`]
2711 THEN SET_TAC[];
2712
2713
2714
2715 MRESAL_TAC Iunbuig.coplanar_aff_gt_simple[`s`;`4`;`v`;`p+3`][ARITH_RULE`0+2=2`]
2716 THEN DICH_TAC 0
2717 THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`]
2718 THEN STRIP_TAC
2719 THEN MP_TAC(SET_RULE`v p IN aff_gt {vec 0} {v (p + 1), v (p + 3)}
2720 /\ aff_gt {vec 0} {v (p + 1), v (p + 3)} SUBSET aff_ge {vec 0} {v (p + 1), v (p + 3)}
2721 ==> (v:num->real^3) p IN aff_ge {vec 0} {v (p + 1), v (p + 3)}`)
2722 THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE]
2723 THEN RESA_TAC
2724 THEN MRESA_TAC Iunbuig.ARCV_ADD_AFF_GE[`vec 0:real^3`;`v (p+1)`;`v (p+3)`;`v (p)`]
2725 THEN DICH_TAC(79-67)
2726 THEN SYM_ASSUM_TAC
2727 THEN REWRITE_TAC[GSYM dist]
2728 THEN ONCE_REWRITE_TAC[DIST_SYM]
2729 THEN ASSUME_TAC(h0_CSTAB_LT_4)
2730 THEN MP_TAC(REAL_ARITH`  norm ((v:num->real^3) (p + 1)) <= &2 * h0 /\ &2<= norm (v (p + 1))/\
2731 norm ((v:num->real^3) (p + 3)) <= &2 * h0 /\ &2<= norm (v (p + 3))/\
2732 norm ((v:num->real^3) (p + 2)) <= &2 * h0 /\ &2<= norm (v (p + 2))/\
2733 cstab< &4/\ &2 * h0< &4 /\ &2< &2 *h0
2734 /\ dist (v p,v (p + 1)) <= cstab
2735 /\ &2* h0<= dist (v p,v (p + 1))
2736 /\ dist (v p,v (p + 3)) <= cstab
2737 /\ &2* h0<= dist (v p,v (p + 3))
2738 ==> norm (v (p + 1)) < &4 /\ &0< norm (v (p + 1))/\
2739 norm (v (p + 3)) < &4 /\ &0< norm (v (p + 3))/\
2740 norm (v (p + 2)) < &4 /\ &0< norm (v (p + 2))/\
2741  dist (v p,v (p + 1))< &4/\ &2<= dist (v p,v (p + 1))/\ &0<  dist (v p,v (p + 1))/\
2742  dist (v p,v (p + 3))< &4/\ &2<= dist (v p,v (p + 3))/\ &0<  dist (v p,v (p + 3))/\
2743  &2< dist (v p,v (p + 1))/\
2744  &2< dist (v p,v (p + 3))/\
2745  &0< &2
2746 `)
2747 THEN RESA_TAC
2748 THEN DICH_TAC 0
2749 THEN ONCE_REWRITE_TAC[DIST_SYM]
2750 THEN ASM_REWRITE_TAC[]
2751 THEN ONCE_REWRITE_TAC[DIST_SYM]
2752 THEN RESA_TAC
2753 THEN MRESAS_TAC Oxlzlez.DIST_IMP_UPS_X_POS[`vec 0:real^3`;`v (p)`;`v (p+1)`][]
2754 THEN DICH_TAC 0
2755 THEN ASM_SIMP_TAC[dist;VECTOR_ARITH`vec 0- A= -- A`; NORM_NEG;REAL_ARITH`a<=b/\ b<c==> a<c`]
2756 THEN REWRITE_TAC[GSYM dist]
2757 THEN STRIP_TAC
2758 THEN MRESAS_TAC Ocbicby.arclength_xrr[`(&2)`;`(norm (v (p + 1)))`;`(dist (v p,v (p + 1)))`][REAL_ARITH`a*a= a pow 2`]
2759 THEN ONCE_REWRITE_TAC[Arc_properties.arc_sym]
2760 THEN ASM_REWRITE_TAC[]
2761 THEN ONCE_REWRITE_TAC[Arc_properties.arc_sym]
2762 THEN MRESAS_TAC Oxlzlez.DIST_IMP_UPS_X_POS[`vec 0:real^3`;`v (p)`;`v (p+3)`][]
2763 THEN DICH_TAC 0
2764 THEN ASM_SIMP_TAC[dist;VECTOR_ARITH`vec 0- A= -- A`; NORM_NEG;REAL_ARITH`a<=b/\ b<c==> a<c`]
2765 THEN REWRITE_TAC[GSYM dist]
2766 THEN STRIP_TAC
2767 THEN MRESAS_TAC Ocbicby.arclength_xrr[`(&2)`;`(norm (v (p + 3)))`;`(dist (v p,v (p + 3)))`][REAL_ARITH`a*a= a pow 2`]
2768 THEN ONCE_REWRITE_TAC[DIST_SYM]
2769 THEN ASM_REWRITE_TAC[]
2770 THEN ONCE_REWRITE_TAC[DIST_SYM]
2771 THEN MRESAS_TAC Oxlzlez.DIST_IMP_UPS_X_POS[`vec 0:real^3`;`v (p+2)`;`v (p+3)`][]
2772 THEN DICH_TAC 0
2773 THEN ASM_SIMP_TAC[dist;VECTOR_ARITH`vec 0- A= -- A`; NORM_NEG;REAL_ARITH`a<=b/\ b<c==> a<c`]
2774 THEN REWRITE_TAC[GSYM dist]
2775 THEN STRIP_TAC
2776 THEN MRESAS_TAC Ocbicby.arclength_xrr[`(norm (v (p + 2)))`;`(norm (v (p + 3)))`;`(dist (v (p+2),v (p + 3)))`][REAL_ARITH`a*a= a pow 2`]
2777 THEN MRESAS_TAC Oxlzlez.DIST_IMP_UPS_X_POS[`vec 0:real^3`;`v (p+1)`;`v (p+2)`][]
2778 THEN DICH_TAC 0
2779 THEN ASM_SIMP_TAC[dist;VECTOR_ARITH`vec 0- A= -- A`; NORM_NEG;REAL_ARITH`a<=b/\ b<c==> a<c`]
2780 THEN REWRITE_TAC[GSYM dist]
2781 THEN STRIP_TAC
2782 THEN MRESAS_TAC Ocbicby.arclength_xrr[`(norm (v (p + 1)))`;`(norm (v (p + 2)))`;`(dist (v (p+1),v (p + 2)))`][REAL_ARITH`a*a= a pow 2`]
2783 THEN MRESAL_TAC Ocbicby.xrr_increasing[`&2`;`(norm (v (p + 1)))`;`&2`;`(dist (v p,v (p + 1)))`][REAL_ARITH`&0<= &2`]
2784 THEN MRESAL_TAC Ocbicby.xrr_increasing[`&2`;`(norm (v (p + 3)))`;`&2`;`(dist (v (p+3),v (p)))`][REAL_ARITH`&0<= &2`]
2785 THEN DICH_TAC 0
2786 THEN ONCE_REWRITE_TAC[DIST_SYM]
2787 THEN ASM_REWRITE_TAC[]
2788 THEN ONCE_REWRITE_TAC[DIST_SYM]
2789 THEN STRIP_TAC
2790 THEN MRESA_TAC Ocbicby.xrr_sym[`(norm (v (p + 2)))`;`(norm (v (p + 1)))`;`(dist (v (p+1),v (p+2)))`]
2791 THEN MRESAL_TAC Ocbicby.xrr_decreasing[`&2`;`(norm (v (p + 2)))`;`(norm (v (p + 1)))`;`(dist (v (p+2),v (p+3)))`][REAL_ARITH`&0<= &2`]
2792 THEN MRESAL_TAC Ocbicby.xrr_decreasing[`&2`;`(norm (v (p + 2)))`;`(norm (v (p + 3)))`;`(dist (v (p+1),v (p+2)))`][REAL_ARITH`&0<= &2`]
2793 THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`(&2)`;`(norm (v (p + 1)))`;` (dist (v p,v (p + 1)))`][REAL_ARITH`a*a= a pow 2`]
2794 THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`(&2)`;`(norm (v (p + 3)))`;` (dist (v (p+3),v (p)))`][REAL_ARITH`a*a= a pow 2`]
2795 THEN DICH_TAC 0
2796 THEN ONCE_REWRITE_TAC[DIST_SYM]
2797 THEN ASM_REWRITE_TAC[]
2798 THEN ONCE_REWRITE_TAC[DIST_SYM]
2799 THEN RESA_TAC
2800 THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`(norm (v (p + 1)))`;`(norm (v (p + 2)))`;` (dist (v (p+1),v (p + 2)))`][REAL_ARITH`a*a= a pow 2`]
2801 THEN MRESAL_TAC Ocbicby.xrr_bounds_2[`(norm (v (p + 2)))`;`(norm (v (p + 3)))`;` (dist (v (p+2),v (p + 3)))`][REAL_ARITH`a*a= a pow 2`]
2802 THEN MP_TAC(REAL_ARITH`xrr (&2) (norm ((v:num->real^3) (p + 1))) (&2) <
2803       xrr (&2) (norm (v (p + 1))) (dist (v p,v (p + 1)))/\
2804 xrr (&2) (norm (v (p + 3))) (&2) <
2805       xrr (&2) (norm (v (p + 3))) (dist (v (p + 3),v p))/\
2806 xrr (norm (v (p + 1))) (norm (v (p + 2))) (&2) <=
2807       xrr (&2) (norm (v (p + 1))) (&2)/\
2808 xrr (norm (v (p + 2))) (norm (v (p + 3))) (&2) <=
2809       xrr (&2) (norm (v (p + 3))) (&2)/\
2810 &0 < xrr (&2) (norm (v (p + 1))) (dist (v p,v (p + 1)))/\
2811 xrr (&2) (norm (v (p + 1))) (dist (v p,v (p + 1))) < &16/\
2812 &0 < xrr (&2) (norm (v (p + 3))) (dist (v (p + 3),v p))/\
2813 xrr (&2) (norm (v (p + 3))) (dist (v (p + 3),v p)) < &16/\
2814 &0 < xrr (norm (v (p + 1))) (norm (v (p + 2))) (&2)/\
2815 xrr (norm (v (p + 1))) (norm (v (p + 2))) (&2) < &16/\
2816 &0 < xrr (norm (v (p + 2))) (norm (v (p + 3))) (&2)/\
2817 xrr (norm (v (p + 2))) (norm (v (p + 3))) (&2) < &16
2818 ==> xrr (&2) (norm (v (p + 1))) (dist (v p,v (p + 1))) <= &16 /\
2819       &0 <= xrr (&2) (norm (v (p + 1))) (&2)/\
2820 xrr (&2) (norm (v (p + 3))) (dist (v (p + 3),v p)) <= &16 /\
2821       &0 <= xrr (&2) (norm (v (p + 3))) (&2)/\
2822 xrr (&2) (norm (v (p + 1))) (&2) <= &16 /\
2823       &0 <= xrr (norm (v (p + 1))) (norm (v (p + 2))) (&2)/\
2824 xrr (&2) (norm (v (p + 3))) (&2) <= &16 /\
2825       &0 <= xrr (norm (v (p + 2))) (norm (v (p + 3))) (&2)
2826 `)
2827 THEN RESA_TAC
2828 THEN MRESAL_TAC ACS_MONO_LT[`&1 - xrr (&2) (norm (v (p + 1))) (dist (v p,v (p + 1))) / &8`;`&1 - xrr (&2) (norm (v (p + 1))) (&2) / &8`]
2829 [REAL_ARITH`&1- a/ &8< &1- b/ &8 <=> b<a`;REAL_ARITH`&1- a/ &8<= &1<=> &0<=a`;
2830 REAL_ARITH`(-- &1) <= &1- a/ &8<=> a<= &16`]
2831 THEN MRESAL_TAC ACS_MONO_LT[`&1 - xrr (&2) (norm (v (p + 3))) (dist (v (p+3),v (p ))) / &8`;`&1 - xrr (&2) (norm (v (p + 3))) (&2) / &8`]
2832 [REAL_ARITH`&1- a/ &8< &1- b/ &8 <=> b<a`;REAL_ARITH`&1- a/ &8<= &1<=> &0<=a`;
2833 REAL_ARITH`(-- &1) <= &1- a/ &8<=> a<= &16`]
2834 THEN MRESAL_TAC ACS_MONO_LE[`&1 - xrr (&2) (norm (v (p + 1))) (&2) / &8`;`&1 - xrr (norm (v (p + 1))) (norm (v (p + 2))) (&2) / &8`]
2835 [REAL_ARITH`&1- a/ &8<= &1- b/ &8 <=> b<=a`;REAL_ARITH`&1- a/ &8<= &1<=> &0<=a`;
2836 REAL_ARITH`(-- &1) <= &1- a/ &8<=> a<= &16`]
2837 THEN MRESAL_TAC ACS_MONO_LE[`&1 - xrr (&2) (norm (v (p + 3))) (&2) / &8`;`&1 - xrr (norm (v (p + 2))) (norm (v (p + 3))) (&2) / &8`]
2838 [REAL_ARITH`&1- a/ &8<= &1- b/ &8 <=> b<=a`;REAL_ARITH`&1- a/ &8<= &1<=> &0<=a`;
2839 REAL_ARITH`(-- &1) <= &1- a/ &8<=> a<= &16`]
2840 THEN DICH_TAC 0
2841 THEN DICH_TAC 0
2842 THEN DICH_TAC 0
2843 THEN DICH_TAC 0
2844 THEN REAL_ARITH_TAC;
2845
2846 ]);;
2847
2848
2849
2850
2851  end;;
2852
2853
2854 (*
2855 let check_completeness_claimA_concl =
2856   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
2857 *)
2858
2859
2860
2861