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