text_formalization/local/JKQEWGV.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 Jkqewgv = struct
  16
  17 open Polyhedron;;
  18 open Sphere;;
  19 open Topology;;
  20 open Fan_misc;;
  21 open Planarity;;
  22 open Conforming;;
  23 open Hypermap;;
  24 open Fan;;
  25 open Topology;;
  26 open Wrgcvdr_cizmrrh;;
  27 open Local_lemmas;;
  28 open Collect_geom;;
  29 open Dih2k_hypermap;;
  30 open Wjscpro;;
  31 open Tecoxbm;;
  32 open Hdplygy;;
  33 open Nkezbfc_local;;
  34 open Flyspeck_constants;;
  35 open Gbycpxs;;
  36 open Pcrttid;;
  37 open Local_lemmas;;
  38 open Pack_defs;;
  39
  40 open Hales_tactic;;
  41
  42 open Appendix;;
  43
  44
  45 open Hypermap;;
  46 open Fan;;
  47 open Wrgcvdr_cizmrrh;;
  48 open Local_lemmas;;
  49 open Flyspeck_constants;;
  50 open Pack_defs;;
  51
  52 open Hales_tactic;;
  53
  54 open Appendix;;
  55
  56
  57 open Zithlqn;;
  58
  59
  60 open Xwitccn;;
  61
  62 open Ayqjtmd;;
  63
  64
  65 let IS_SCS_STABLE_SYSTEM=prove_by_refinement(
  66 `is_scs_v39 s /\ 3< scs_k_v39 s
  67 ==>
  68 stable_system (scs_k_v39 s) (scs_d_v39 s)  (0..(scs_k_v39 s)-1)
  69 (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s))
  70 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)) (\i. ((1+i):num MOD (scs_k_v39 s)))
  71 `,
  72   (* {{{ proof *)
  73 [
  74 REWRITE_TAC[is_scs_v39;stable_system;constraint_system;torsor;change_type_v2;change_type_v3]
  75 THEN RESA_TAC
  76 THEN RESA_TAC
  77 THEN MP_TAC (ARITH_RULE`3<= scs_k_v39 s==> (scs_k_v39 s - 1 +1)-0= scs_k_v39 s
  78 /\ (scs_k_v39 s - 1 +1)= scs_k_v39 s/\ 1< scs_k_v39 s /\ 1<= scs_k_v39 s /\ 1<= scs_k_v39 s -1/\ ~(scs_k_v39 s=0)`)
  79 THEN RESA_TAC
  80 THEN MRESA_TAC HAS_SIZE_NUMSEG[`0`;`scs_k_v39 s -1`]
  81 THEN REPLICATE_TAC 23 (POP_ASSUM MP_TAC)
  82 THEN REMOVE_ASSUM_TAC
  83 THEN REPEAT DISCH_TAC
  84 THEN STRIP_TAC;
  85
  86 STRIP_TAC;
  87
  88 STRIP_TAC;
  89
  90 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
  91 THEN MRESAL1_TAC Hypermap.LE_MOD_SUC`scs_k_v39 s -1`[ADD1];
  92
  93 STRIP_TAC;
  94
  95 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
  96 THEN REPEAT STRIP_TAC
  97 THEN MP_TAC(ARITH_RULE`x1 <= scs_k_v39 s - 1 /\
  98 x2 <= scs_k_v39 s - 1
  99 ==> 1+ x1 <= scs_k_v39 s -1 +1 /\ 1+ x2 <= scs_k_v39 s - 1+1`)
 100 THEN RESA_TAC
 101 THEN MRESAL_TAC (GEN_ALL MOD_IMP_EQ)[`scs_k_v39 s`;`1+x1`;`1+x2`][ARITH_RULE`1<= 1+A /\ (1+A<=4<=> A<=3)`]
 102 THEN POP_ASSUM MP_TAC
 103 THEN ARITH_TAC;
 104
 105 STRIP_TAC;
 106
 107 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
 108 THEN REPEAT STRIP_TAC
 109 THEN POP_ASSUM MP_TAC
 110 THEN MP_TAC(ARITH_RULE`0<i==> 1<= i`)
 111 THEN RESA_TAC
 112 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s:num`;`x:num`;`i:num`]
 113 THEN MP_TAC(ARITH_RULE`3<= scs_k_v39 s/\ scs_k_v39 s<=6
 114 ==> scs_k_v39 s=3 \/ scs_k_v39 s=4 \/ scs_k_v39 s=5 \/ scs_k_v39 s= 6`)
 115 THEN RESA_TAC
 116 THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT DISCH_TAC
 117 THEN POP_ASSUM MP_TAC);
 118
 119 MP_TAC(ARITH_RULE`0<i /\ i< 3==> i=1 \/ i=2 `)
 120 THEN RESA_TAC
 121 THEN MP_TAC(ARITH_RULE`x<= 3-1==> x=0 \/ x=1 \/ x=2 `)
 122 THEN ASM_REWRITE_TAC[]
 123 THEN RESA_TAC
 124 THEN ARITH_TAC;
 125
 126 MP_TAC(ARITH_RULE`0<i /\ i< 4==> i=1 \/ i=2 \/ i=3`)
 127 THEN RESA_TAC
 128 THEN MP_TAC(ARITH_RULE`x<= 4-1==> x=0 \/ x=1 \/ x=2 \/ x=3`)
 129 THEN ASM_REWRITE_TAC[]
 130 THEN RESA_TAC
 131 THEN ARITH_TAC;
 132
 133 MP_TAC(ARITH_RULE`0<i /\ i< 5==> i=1 \/ i=2 \/ i=3\/ i=4`)
 134 THEN RESA_TAC
 135 THEN MP_TAC(ARITH_RULE`x<= 5-1==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4`)
 136 THEN ASM_REWRITE_TAC[]
 137 THEN RESA_TAC
 138 THEN ARITH_TAC;
 139
 140 MP_TAC(ARITH_RULE`0<i /\ i< 6==> i=1 \/ i=2 \/ i=3\/ i=4\/ i=5`)
 141 THEN RESA_TAC
 142 THEN MP_TAC(ARITH_RULE`x<= 6-1==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4\/ x=5`)
 143 THEN ASM_REWRITE_TAC[]
 144 THEN RESA_TAC
 145 THEN ARITH_TAC;
 146
 147 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
 148 THEN REPEAT STRIP_TAC
 149 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s:num`;`x:num`;`scs_k_v39 s:num`]
 150 THEN MRESAL_TAC MOD_MULT_ADD[`1`;`scs_k_v39 s`;`x:num`][ARITH_RULE`1*A=A`]
 151 THEN MP_TAC(ARITH_RULE`x<=scs_k_v39 s -1 /\ 3<= scs_k_v39 s ==> x< scs_k_v39 s`)
 152 THEN RESA_TAC
 153 THEN MRESA_TAC MOD_LT[`x:num`;`scs_k_v39 s`];
 154
 155 STRIP_TAC;
 156
 157 REPLICATE_TAC 15 (REMOVE_ASSUM_TAC)
 158 THEN REPEAT STRIP_TAC
 159 THEN POP_ASSUM(fun th-> MRESA_TAC th[`i:num`;`j:num`])
 160 THEN REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
 161 THEN REAL_ARITH_TAC;
 162
 163 STRIP_TAC;
 164
 165 REPEAT GEN_TAC
 166 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s`;`j:num`;`scs_k_v39 s`]
 167 THEN MRESAL_TAC MOD_MULT_ADD[`1`;`scs_k_v39 s`;`j:num`][ARITH_RULE`1*A=A`]
 168 THEN MRESAL_TAC MOD_MOD_REFL[`j:num`;`scs_k_v39 s`][ARITH_RULE`~(5=0)`]
 169 THEN ASM_TAC
 170 THEN REWRITE_TAC[periodic2]
 171 THEN REPEAT DISCH_TAC
 172 THEN ONCE_REWRITE_TAC[SET_RULE`A=B <=> B=A`]
 173 THEN STRIP_TAC;
 174
 175 MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s i`][periodic];
 176
 177 MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s i`][periodic];
 178
 179 STRIP_TAC;
 180
 181 ASM_TAC
 182 THEN REWRITE_TAC[periodic2;SUBSET;IN_ELIM_THM]
 183 THEN REPEAT DISCH_TAC
 184 THEN REPEAT STRIP_TAC
 185 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
 186 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 187 THEN MRESAL_TAC th[`i:num`;`j:num`][ADD1;ARITH_RULE`1+i=i+1`]);
 188
 189 EXISTS_TAC`i MOD scs_k_v39 s`
 190 THEN REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
 191 THEN MRESA_TAC DIVISION[`i:num`;`scs_k_v39 s`]
 192 THEN MP_TAC(ARITH_RULE`i MOD scs_k_v39 s < scs_k_v39 s
 193 /\ 3<= scs_k_v39 s
 194 ==> i MOD scs_k_v39 s <= scs_k_v39 s-1`)
 195 THEN RESA_TAC
 196 THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
 197 THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1];
 198
 199 EXISTS_TAC`j MOD scs_k_v39 s`
 200 THEN REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
 201 THEN MRESA_TAC DIVISION[`j:num`;`scs_k_v39 s`]
 202 THEN MP_TAC(ARITH_RULE`j MOD scs_k_v39 s < scs_k_v39 s
 203 /\ 3<= scs_k_v39 s
 204 ==> j MOD scs_k_v39 s <= scs_k_v39 s-1`)
 205 THEN RESA_TAC
 206 THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
 207 THEN MRESAL_TAC MOD_ADD_MOD[`j:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
 208 THEN SET_TAC[];
 209
 210 SUBGOAL_THEN`{{i MOD scs_k_v39 s, j MOD scs_k_v39 s} | i,j | scs_J_v39 s i j}
 211 SUBSET {{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
 212            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
 213 ASSUME_TAC;
 214
 215 REWRITE_TAC[SUBSET;IN_ELIM_THM]
 216 THEN GEN_TAC
 217 THEN RESA_TAC
 218 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
 219 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 220 THEN MRESAL_TAC th[`i:num`;`j:num`][ADD1;ARITH_RULE`1+i=i+1`]);
 221
 222 EXISTS_TAC`i:num MOD scs_k_v39 s`
 223 THEN ASM_REWRITE_TAC[]
 224 THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
 225 THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
 226 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0)`]
 227 THEN MRESA_TAC DIVISION[`i:num`;`scs_k_v39 s`]
 228 THEN ASM_TAC
 229 THEN REWRITE_TAC[periodic;periodic2]
 230 THEN REPEAT DISCH_TAC
 231 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][periodic]
 232 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j:num`)
 233 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][periodic]
 234 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(i MOD scs_k_v39 s) +1:num`)
 235 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 236 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][periodic]
 237 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(i MOD scs_k_v39 s) +1:num`)
 238 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 239 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + 1) MOD scs_k_v39 s)`][periodic]
 240 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
 241 THEN REPLICATE_TAC 19 (POP_ASSUM MP_TAC)
 242 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 243 THEN MRESA_TAC th[`(i MOD scs_k_v39 s)`; `((i + 1) MOD scs_k_v39 s)`])
 244 THEN REWRITE_TAC[h0;cstab;sqrt8]
 245 THEN REAL_ARITH_TAC;
 246
 247 EXISTS_TAC`j:num MOD scs_k_v39 s`
 248 THEN ASM_REWRITE_TAC[]
 249 THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
 250 THEN MRESAL_TAC MOD_ADD_MOD[`j:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
 251 THEN MRESAL_TAC MOD_MOD_REFL[`j:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0)`]
 252 THEN MRESA_TAC DIVISION[`j:num`;`scs_k_v39 s`]
 253 THEN ASM_TAC
 254 THEN REWRITE_TAC[periodic;periodic2;SET_RULE`{A,B}={B,A}`]
 255 THEN REPEAT DISCH_TAC
 256 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s j`][periodic]
 257 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
 258 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][periodic]
 259 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(j MOD scs_k_v39 s) +1:num`)
 260 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 261 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][periodic]
 262 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(j MOD scs_k_v39 s) +1:num`)
 263 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 264 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((j + 1) MOD scs_k_v39 s)`][periodic]
 265 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j:num`)
 266 THEN REPLICATE_TAC 19 (POP_ASSUM MP_TAC)
 267 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 268 THEN MRESA_TAC th[`(j MOD scs_k_v39 s)`; `((j + 1) MOD scs_k_v39 s)`])
 269 THEN REWRITE_TAC[h0;cstab;sqrt8]
 270 THEN REAL_ARITH_TAC;
 271
 272 SUBGOAL_THEN`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
 273                                                     (&2 * h0 <
 274                                                      scs_b_v39 s i (SUC i) \/
 275                                                      &2 <
 276                                                      scs_a_v39 s i (SUC i))}
 277 SUBSET IMAGE (\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s}) {i | i < scs_k_v39 s /\
 278            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
 279  ASSUME_TAC;
 280
 281  REWRITE_TAC[IN_ELIM_THM;IMAGE;SUBSET];
 282
 283 SUBGOAL_THEN` {i | i < scs_k_v39 s /\
 284            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}
 285 SUBSET 0.. scs_k_v39 s`
 286  ASSUME_TAC;
 287
 288 REWRITE_TAC[IN_ELIM_THM;SUBSET;IN_NUMSEG]
 289 THEN ARITH_TAC;
 290
 291 MRESAL_TAC CARD_SUBSET[`{i | i < scs_k_v39 s /\
 292            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
 293 `0.. scs_k_v39 s`][FINITE_NUMSEG]
 294 THEN MRESAL_TAC FINITE_SUBSET[`{i | i < scs_k_v39 s /\
 295            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
 296 `0.. scs_k_v39 s`][FINITE_NUMSEG]
 297 THEN MRESAL_TAC CARD_SUBSET_IMAGE
 298 [`(\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s})`;`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
 299                                                     (&2 * h0 <
 300                                                      scs_b_v39 s i (SUC i) \/
 301                                                      &2 <
 302                                                      scs_a_v39 s i (SUC i))}`;`{i | i < scs_k_v39 s /\
 303            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
 304 ][FINITE_NUMSEG]
 305 THEN MRESAL_TAC FINITE_IMAGE
 306 [`(\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s})`;`{i | i < scs_k_v39 s /\
 307            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
 308 ][FINITE_NUMSEG]
 309 THEN MRESAL_TAC FINITE_SUBSET[`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
 310                                                     (&2 * h0 <
 311                                                      scs_b_v39 s i (SUC i) \/
 312                                                      &2 <
 313                                                      scs_a_v39 s i (SUC i))}`;
 314 `IMAGE (\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s}) {i | i < scs_k_v39 s /\
 315            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`][FINITE_NUMSEG]
 316 THEN MRESAL_TAC CARD_SUBSET[`{{i MOD scs_k_v39 s, j MOD scs_k_v39 s} | i,j | scs_J_v39 s i j}`;
 317 `{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
 318                                                     (&2 * h0 <
 319                                                      scs_b_v39 s i (SUC i) \/
 320                                                      &2 <
 321                                                      scs_a_v39 s i (SUC i))}`][FINITE_NUMSEG]
 322 THEN POP_ASSUM MP_TAC
 323 THEN REPLICATE_TAC 2 (REMOVE_ASSUM_TAC)
 324 THEN POP_ASSUM MP_TAC
 325 THEN REPLICATE_TAC 13(REMOVE_ASSUM_TAC)
 326 THEN POP_ASSUM MP_TAC
 327 THEN ARITH_TAC;
 328
 329 STRIP_TAC;
 330
 331 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
 332 THEN REPEAT STRIP_TAC
 333 THEN REPLICATE_TAC 16 (POP_ASSUM MP_TAC)
 334 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 335 THEN MATCH_MP_TAC th)
 336 THEN ASM_REWRITE_TAC[]
 337 THEN REMOVE_ASSUM_TAC
 338 THEN POP_ASSUM MP_TAC
 339 THEN POP_ASSUM MP_TAC
 340 THEN REPLICATE_TAC 24 (REMOVE_ASSUM_TAC)
 341 THEN POP_ASSUM MP_TAC
 342 THEN ARITH_TAC;
 343
 344 STRIP_TAC;
 345
 346 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`;]
 347 THEN REPEAT STRIP_TAC
 348 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
 349 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 350 THEN MRESAL1_TAC th`i:num`[ADD1])
 351 THEN ASM_TAC
 352 THEN REWRITE_TAC[periodic2]
 353 THEN REPEAT STRIP_TAC
 354 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][periodic]
 355 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
 356 THEN ASM_REWRITE_TAC[ARITH_RULE`1+i=i+1`]
 357 THEN REMOVE_ASSUM_TAC
 358 THEN POP_ASSUM MP_TAC
 359 THEN REAL_ARITH_TAC;
 360
 361 REWRITE_TAC[IN_ELIM_THM]
 362 THEN REPEAT STRIP_TAC
 363 THEN ASM_REWRITE_TAC[]
 364 THEN MP_TAC(SET_RULE`{i, j} = {i' MOD scs_k_v39 s, j' MOD scs_k_v39 s}
 365 ==> (i = i' MOD scs_k_v39 s /\ j= j' MOD scs_k_v39 s)\/
 366 (j = i' MOD scs_k_v39 s /\ i= j' MOD scs_k_v39 s)`)
 367 THEN ASM_REWRITE_TAC[]
 368 THEN STRIP_TAC
 369 THEN ASM_REWRITE_TAC[]
 370 THEN ASM_TAC
 371 THEN REWRITE_TAC[periodic2]
 372 THEN REPEAT STRIP_TAC
 373 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][periodic]
 374 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j':num`)
 375 THEN REPLICATE_TAC 21 (POP_ASSUM MP_TAC)
 376 THEN POP_ASSUM(fun th-> MRESA_TAC th[`i':num`;`(j' MOD scs_k_v39 s)`]
 377 THEN MRESA_TAC th[`i' MOD scs_k_v39 s:num`;`(j' MOD scs_k_v39 s)`])
 378 THEN REPEAT STRIP_TAC
 379 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD scs_k_v39 s)`][periodic;]
 380 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i':num`)
 381 THEN REPLICATE_TAC 15 (POP_ASSUM MP_TAC)
 382 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 383 THEN MRESA_TAC th[`(i' MOD scs_k_v39 s)`;`(j' MOD scs_k_v39 s)`])
 384 THEN REWRITE_TAC[sqrt8]
 385 ]);;
 386
 387
 388
 389
 390
 391
 392
 393
 394
 395
 396
 397
 398
 399
 400
 401
 402
 403
 404
 405
 406
 407
 408
 409 let IS_SCS_TRI_STABLE_SYSTEM=prove_by_refinement(
 410 `is_scs_v39 s /\ scs_k_v39 s=3
 411 ==>
 412 tri_stable (scs_k_v39 s) (scs_d_v39 s)  (0..(scs_k_v39 s)-1)
 413 (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s))
 414 (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)) (\i. ((1+i):num MOD (scs_k_v39 s)))
 415 `,
 416 [
 417 REWRITE_TAC[is_scs_v39;tri_stable;constraint_system;torsor;change_type_v2;change_type_v3]
 418 THEN RESA_TAC
 419 THEN RESA_TAC
 420 THEN MP_TAC (ARITH_RULE`3<= scs_k_v39 s==> (scs_k_v39 s - 1 +1)-0= scs_k_v39 s
 421 /\ (scs_k_v39 s - 1 +1)= scs_k_v39 s/\ 1< scs_k_v39 s /\ 1<= scs_k_v39 s /\ 1<= scs_k_v39 s -1/\ ~(scs_k_v39 s=0)/\ 3-0=3`)
 422 THEN RESA_TAC
 423 THEN MRESA_TAC HAS_SIZE_NUMSEG[`0`;`scs_k_v39 s -1`]
 424 THEN REPLICATE_TAC 23 (POP_ASSUM MP_TAC)
 425 THEN REMOVE_ASSUM_TAC
 426 THEN REPEAT DISCH_TAC
 427 THEN STRIP_TAC;
 428
 429 STRIP_TAC;
 430
 431 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
 432 THEN MRESAL1_TAC Hypermap.LE_MOD_SUC`scs_k_v39 s -1`[ADD1];
 433
 434 STRIP_TAC;
 435
 436 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
 437 THEN REPEAT STRIP_TAC
 438 THEN MP_TAC(ARITH_RULE`x1 <= scs_k_v39 s - 1 /\
 439 x2 <= scs_k_v39 s - 1
 440 ==> 1+ x1 <= scs_k_v39 s -1 +1 /\ 1+ x2 <= scs_k_v39 s - 1+1`)
 441 THEN RESA_TAC
 442 THEN MRESAL_TAC (GEN_ALL MOD_IMP_EQ)[`scs_k_v39 s`;`1+x1`;`1+x2`][ARITH_RULE`1<= 1+A /\ (1+A<=4<=> A<=3)`]
 443 THEN POP_ASSUM MP_TAC
 444 THEN ARITH_TAC;
 445
 446 STRIP_TAC;
 447
 448 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
 449 THEN REPEAT STRIP_TAC
 450 THEN POP_ASSUM MP_TAC
 451 THEN MP_TAC(ARITH_RULE`0<i==> 1<= i`)
 452 THEN RESA_TAC
 453 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s:num`;`x:num`;`i:num`]
 454 THEN MP_TAC(ARITH_RULE`0<i /\ i< 3==> i=1 \/ i=2 `)
 455 THEN RESA_TAC
 456 THEN MP_TAC(ARITH_RULE`x<= 3-1==> x=0 \/ x=1 \/ x=2 `)
 457 THEN ASM_REWRITE_TAC[]
 458 THEN RESA_TAC
 459 THEN ARITH_TAC;
 460
 461 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
 462 THEN REPEAT STRIP_TAC
 463 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s:num`;`x:num`;`scs_k_v39 s:num`]
 464 THEN MRESAL_TAC MOD_MULT_ADD[`1`;`scs_k_v39 s`;`x:num`][ARITH_RULE`1*A=A`]
 465 THEN MP_TAC(ARITH_RULE`x<=scs_k_v39 s -1 /\ 3<= scs_k_v39 s ==> x< scs_k_v39 s`)
 466 THEN RESA_TAC
 467 THEN MRESA_TAC MOD_LT[`x:num`;`scs_k_v39 s`];
 468
 469 STRIP_TAC;
 470
 471 REPLICATE_TAC 16 (REMOVE_ASSUM_TAC)
 472 THEN REPEAT STRIP_TAC
 473 THEN POP_ASSUM(fun th-> MRESA_TAC th[`i:num`;`j:num`])
 474 THEN REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
 475 THEN REAL_ARITH_TAC;
 476
 477 STRIP_TAC;
 478
 479 REPEAT GEN_TAC
 480 THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`scs_k_v39 s`;`j:num`;`scs_k_v39 s`]
 481 THEN MRESAL_TAC MOD_MULT_ADD[`1`;`scs_k_v39 s`;`j:num`][ARITH_RULE`1*A=A`]
 482 THEN MRESAL_TAC MOD_MOD_REFL[`j:num`;`scs_k_v39 s`][ARITH_RULE`~(5=0)`]
 483 THEN ASM_TAC
 484 THEN REWRITE_TAC[periodic2]
 485 THEN REPEAT DISCH_TAC
 486 THEN ONCE_REWRITE_TAC[SET_RULE`A=B <=> B=A`]
 487 THEN STRIP_TAC;
 488
 489 MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s i`][periodic];
 490
 491 MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s i`][periodic];
 492
 493 STRIP_TAC;
 494
 495 ASM_TAC
 496 THEN REWRITE_TAC[periodic2;SUBSET;IN_ELIM_THM]
 497 THEN REPEAT DISCH_TAC
 498 THEN REPEAT STRIP_TAC
 499 THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
 500 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 501 THEN MRESAL_TAC th[`i:num`;`j:num`][ADD1;ARITH_RULE`1+i=i+1`]);
 502
 503 EXISTS_TAC`i MOD scs_k_v39 s`
 504 THEN REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
 505 THEN MRESA_TAC DIVISION[`i:num`;`scs_k_v39 s`]
 506 THEN MP_TAC(ARITH_RULE`i MOD scs_k_v39 s < scs_k_v39 s
 507 /\ 3<= scs_k_v39 s
 508 ==> i MOD scs_k_v39 s <= scs_k_v39 s-1`)
 509 THEN RESA_TAC
 510 THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
 511 THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1];
 512
 513 EXISTS_TAC`j MOD scs_k_v39 s`
 514 THEN REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
 515 THEN MRESA_TAC DIVISION[`j:num`;`scs_k_v39 s`]
 516 THEN MP_TAC(ARITH_RULE`j MOD scs_k_v39 s < scs_k_v39 s
 517 /\ 3<= scs_k_v39 s
 518 ==> j MOD scs_k_v39 s <= scs_k_v39 s-1`)
 519 THEN RESA_TAC
 520 THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
 521 THEN MRESAL_TAC MOD_ADD_MOD[`j:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
 522 THEN SET_TAC[];
 523
 524 SUBGOAL_THEN`{{i MOD scs_k_v39 s, j MOD scs_k_v39 s} | i,j | scs_J_v39 s i j}
 525 SUBSET {{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
 526            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
 527 ASSUME_TAC;
 528
 529 REWRITE_TAC[SUBSET;IN_ELIM_THM]
 530 THEN GEN_TAC
 531 THEN RESA_TAC
 532 THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
 533 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 534 THEN MRESAL_TAC th[`i:num`;`j:num`][ADD1;ARITH_RULE`1+i=i+1`]);
 535
 536 EXISTS_TAC`i:num MOD scs_k_v39 s`
 537 THEN ASM_REWRITE_TAC[]
 538 THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
 539 THEN MRESAL_TAC MOD_ADD_MOD[`i:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
 540 THEN MRESAL_TAC MOD_MOD_REFL[`i:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0)`]
 541 THEN MRESA_TAC DIVISION[`i:num`;`scs_k_v39 s`]
 542 THEN ASM_TAC
 543 THEN REWRITE_TAC[periodic;periodic2]
 544 THEN REPEAT DISCH_TAC
 545 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i`][periodic]
 546 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j:num`)
 547 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (i MOD scs_k_v39 s)`][periodic]
 548 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(i MOD scs_k_v39 s) +1:num`)
 549 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 550 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (i MOD scs_k_v39 s)`][periodic]
 551 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(i MOD scs_k_v39 s) +1:num`)
 552 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 553 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((i + 1) MOD scs_k_v39 s)`][periodic]
 554 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
 555 THEN REPLICATE_TAC 20 (POP_ASSUM MP_TAC)
 556 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 557 THEN MRESA_TAC th[`(i MOD scs_k_v39 s)`; `((i + 1) MOD scs_k_v39 s)`])
 558 THEN REWRITE_TAC[h0;cstab;sqrt8]
 559 THEN REAL_ARITH_TAC;
 560
 561 EXISTS_TAC`j:num MOD scs_k_v39 s`
 562 THEN ASM_REWRITE_TAC[]
 563 THEN MRESA_TAC MOD_LT[`1:num`;`scs_k_v39 s`]
 564 THEN MRESAL_TAC MOD_ADD_MOD[`j:num`;`1:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0) /\ 1 MOD 4=1`;ADD1]
 565 THEN MRESAL_TAC MOD_MOD_REFL[`j:num`;`scs_k_v39 s`][ARITH_RULE`~(4=0)`]
 566 THEN MRESA_TAC DIVISION[`j:num`;`scs_k_v39 s`]
 567 THEN ASM_TAC
 568 THEN REWRITE_TAC[periodic;periodic2;SET_RULE`{A,B}={B,A}`]
 569 THEN REPEAT DISCH_TAC
 570 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s j`][periodic]
 571 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
 572 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (j MOD scs_k_v39 s)`][periodic]
 573 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(j MOD scs_k_v39 s) +1:num`)
 574 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 575 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (j MOD scs_k_v39 s)`][periodic]
 576 THEN POP_ASSUM(fun th-> MRESA1_TAC th`(j MOD scs_k_v39 s) +1:num`)
 577 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
 578 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s ((j + 1) MOD scs_k_v39 s)`][periodic]
 579 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j:num`)
 580 THEN REPLICATE_TAC 20 (POP_ASSUM MP_TAC)
 581 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
 582 THEN MRESA_TAC th[`(j MOD scs_k_v39 s)`; `((j + 1) MOD scs_k_v39 s)`])
 583 THEN REWRITE_TAC[h0;cstab;sqrt8]
 584 THEN REAL_ARITH_TAC;
 585
 586 SUBGOAL_THEN`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
 587                                                     (&2 * h0 <
 588                                                      scs_b_v39 s i (SUC i) \/
 589                                                      &2 <
 590                                                      scs_a_v39 s i (SUC i))}
 591 SUBSET IMAGE (\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s}) {i | i < scs_k_v39 s /\
 592            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`
 593  ASSUME_TAC;
 594
 595  REWRITE_TAC[IN_ELIM_THM;IMAGE;SUBSET];
 596
 597 SUBGOAL_THEN` {i | i < scs_k_v39 s /\
 598            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}
 599 SUBSET 0.. scs_k_v39 s`
 600  ASSUME_TAC;
 601
 602 REWRITE_TAC[IN_ELIM_THM;SUBSET;IN_NUMSEG]
 603 THEN ARITH_TAC;
 604
 605
 606
 607 MRESAL_TAC CARD_SUBSET[`{i | i < scs_k_v39 s /\
 608            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
 609 `0.. scs_k_v39 s`][FINITE_NUMSEG]
 610 THEN MRESAL_TAC FINITE_SUBSET[`{i | i < scs_k_v39 s /\
 611            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
 612 `0.. scs_k_v39 s`][FINITE_NUMSEG]
 613 THEN MRESAL_TAC CARD_SUBSET_IMAGE
 614 [`(\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s})`;`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
 615                                                     (&2 * h0 <
 616                                                      scs_b_v39 s i (SUC i) \/
 617                                                      &2 <
 618                                                      scs_a_v39 s i (SUC i))}`;`{i | i < scs_k_v39 s /\
 619            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
 620 ][FINITE_NUMSEG]
 621 THEN MRESAL_TAC FINITE_IMAGE
 622 [`(\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s})`;`{i | i < scs_k_v39 s /\
 623            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`;
 624 ][FINITE_NUMSEG]
 625 THEN MRESAL_TAC FINITE_SUBSET[`{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
 626                                                     (&2 * h0 <
 627                                                      scs_b_v39 s i (SUC i) \/
 628                                                      &2 <
 629                                                      scs_a_v39 s i (SUC i))}`;
 630 `IMAGE (\i. {i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s}) {i | i < scs_k_v39 s /\
 631            (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))}`][FINITE_NUMSEG]
 632 THEN MRESAL_TAC CARD_SUBSET[`{{i MOD scs_k_v39 s, j MOD scs_k_v39 s} | i,j | scs_J_v39 s i j}`;
 633 `{{i MOD scs_k_v39 s, SUC i MOD scs_k_v39 s} |i| i < scs_k_v39 s /\
 634                                                     (&2 * h0 <
 635                                                      scs_b_v39 s i (SUC i) \/
 636                                                      &2 <
 637                                                      scs_a_v39 s i (SUC i))}`][FINITE_NUMSEG]
 638 THEN POP_ASSUM MP_TAC
 639 THEN REPLICATE_TAC 2 (REMOVE_ASSUM_TAC)
 640 THEN POP_ASSUM MP_TAC
 641 THEN REPLICATE_TAC 13(REMOVE_ASSUM_TAC)
 642 THEN POP_ASSUM (fun th->
 643 POP_ASSUM MP_TAC
 644 THEN ASM_REWRITE_TAC[th])
 645 THEN ARITH_TAC;
 646
 647
 648 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`]
 649 THEN REPEAT STRIP_TAC
 650 THEN REPLICATE_TAC 17 (POP_ASSUM MP_TAC)
 651 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 652 THEN MATCH_MP_TAC th)
 653 THEN ASM_REWRITE_TAC[]
 654 THEN REMOVE_ASSUM_TAC
 655 THEN POP_ASSUM MP_TAC
 656 THEN POP_ASSUM MP_TAC
 657 THEN REPLICATE_TAC 25 (REMOVE_ASSUM_TAC)
 658 THEN POP_ASSUM MP_TAC
 659 THEN ARITH_TAC;
 660
 661
 662 STRIP_TAC;
 663
 664 REWRITE_TAC[ARITH_RULE`4-1=3`;IN_NUMSEG;ARITH_RULE`0<= A`;]
 665 THEN REPEAT STRIP_TAC
 666 THEN REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
 667 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 668 THEN MRESAL1_TAC th`i:num`[ADD1])
 669 THEN ASM_TAC
 670 THEN REWRITE_TAC[periodic2]
 671 THEN REPEAT STRIP_TAC
 672 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s i`][periodic]
 673 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i:num`)
 674 THEN ASM_REWRITE_TAC[ARITH_RULE`1+i=i+1`]
 675 THEN POP_ASSUM MP_TAC;
 676
 677 REWRITE_TAC[IN_ELIM_THM]
 678 THEN REPEAT STRIP_TAC
 679 THEN ASM_REWRITE_TAC[]
 680 THEN MP_TAC(SET_RULE`{i, j} = {i' MOD scs_k_v39 s, j' MOD scs_k_v39 s}
 681 ==> (i = i' MOD scs_k_v39 s /\ j= j' MOD scs_k_v39 s)\/
 682 (j = i' MOD scs_k_v39 s /\ i= j' MOD scs_k_v39 s)`)
 683 THEN ASM_REWRITE_TAC[]
 684 THEN STRIP_TAC
 685 THEN ASM_REWRITE_TAC[]
 686 THEN ASM_TAC
 687 THEN REWRITE_TAC[periodic2]
 688 THEN REPEAT STRIP_TAC
 689 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][periodic]
 690 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j':num`)
 691 THEN REPLICATE_TAC 22 (POP_ASSUM MP_TAC)
 692 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 693 THEN MRESA_TAC th[`i':num`;`(j' MOD scs_k_v39 s)`]
 694 THEN MRESA_TAC th[`i' MOD scs_k_v39 s:num`;`(j' MOD scs_k_v39 s)`])
 695 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j' MOD scs_k_v39 s)`][periodic;]
 696 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i':num`)
 697 THEN REPLICATE_TAC (42 -16) (POP_ASSUM MP_TAC)
 698 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 699 THEN MRESA_TAC th[`(i' MOD scs_k_v39 s)`;`(j' MOD scs_k_v39 s)`])
 700 THEN REWRITE_TAC[sqrt8];
 701 ]);;
 702
 703
 704
 705
 706
 707 let IS_SCS_IN_BALL_ANNULUS_4=
 708 fun (so:term)->
 709 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
 710 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 711 THEN MP_TAC th THEN REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM])
 712 THEN STRIP_TAC
 713 THEN POP_ASSUM MATCH_MP_TAC
 714 THEN EXISTS_TAC so
 715 THEN MRESAL_TAC VECTOR_3_4[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=4/\ 2<=4/\ 3<=4/\ 4<=4/\ 4 MOD 4= 0 /\ 1 MOD 4= 1 /\ 2 MOD 4= 2/\ 3 MOD 4= 3/\ ~(2=1)
 716 /\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)`;SET_RULE`(a:num) IN (:num)`]
 717 ;;
 718
 719
 720
 721 let IS_SCS_IN_V_SY_4=
 722 fun (so:term)->
 723  EXISTS_TAC so
 724 THEN MRESAL_TAC VECTOR_3_4[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=4/\ 2<=4/\ 3<=4/\ 4<=4/\ 4 MOD 4= 0 /\ 1 MOD 4= 1 /\ 2 MOD 4= 2/\ 3 MOD 4= 3/\ ~(2=1)
 725 /\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)/\ 1<=1/\ 1<=2 /\ 1<=3/\ SUC 1=2/\ SUC 2=3 /\ SUC 3=4/\ SUC 0=1`;SET_RULE`(a:num) IN (:num)`]
 726 ;;
 727
 728
 729 let PROVE_E_SY_INV_TAC_4=
 730 fun (th:term)->
 731 MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x':num`;th;`4`][ARITH_RULE`~(4=0)/\ 4 MOD 4=0/\ SUC 0  MOD 4=1/\ 1 MOD 4=1 /\ 2 MOD 4=2 /\ 3 MOD 4=3`]
 732 THEN EXISTS_TAC th
 733 THEN MRESAL_TAC VECTOR_3_4[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=4/\ 2<=4/\ 3<=4/\ 4<=4/\ 4 MOD 4= 0 /\ 1 MOD 4= 1 /\ 2 MOD 4= 2/\ 3 MOD 4= 3/\ ~(2=1)
 734 /\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)/\ SUC 1=2/\ SUC 0=1 /\ SUC 2= 3/\ SUC 3=4/\ 1<=1 /\ 1<=2 /\ 1<=3`];;
 735
 736
 737
 738
 739 let V_E_FF_IS_SCS_CASES_4=prove_by_refinement(
 740 ` is_scs_v39 s /\ scs_k_v39 s=4 /\ vv IN BBs_v39 s
 741 /\  dimindex(:M)=scs_k_v39 s
 742 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 0]:real^3^M= v
 743 /\ matvec (v:real^3^M) =a
 744 ==>
 745 V_SY (v:real^3^M)=IMAGE vv (:num)/\
 746   E_SY (v:real^3^M)=IMAGE (\i. {vv i, vv (SUC i)}) (:num)/\
 747 F_SY (v:real^3^M)=IMAGE (\i. vv i,vv (SUC i)) (:num)`
 748 ,
 749   (* {{{ proof *)
 750 [
 751 STRIP_TAC
 752 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
 753 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;IN;mk_unadorned_v39]
 754 THEN REPEAT STRIP_TAC;
 755
 756 REWRITE_TAC[V_SY;rows]
 757 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`]
 758 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
 759 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`]
 760 THEN GEN_TAC
 761 THEN EQ_TAC;
 762
 763 REPEAT STRIP_TAC
 764 THENL[
 765 IS_SCS_IN_V_SY_4`1`;
 766 IS_SCS_IN_V_SY_4`2`;
 767 IS_SCS_IN_V_SY_4`3`;
 768 IS_SCS_IN_V_SY_4`0`];
 769
 770 REPEAT STRIP_TAC
 771 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4)<=> (1<= i /\ i<= 4)`]
 772 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`4`;`vv:num-> real^3`][ARITH_RULE`~(4=0)`]
 773 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`)
 774 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
 775 THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
 776 THEN MP_TAC(ARITH_RULE`x' MOD 4 < 4==>  x' MOD 4 =0 \/ x' MOD 4 = 1\/ x' MOD 4 = 2 \/ x' MOD 4 =3`)
 777 THEN RESA_TAC
 778 THENL[
 779 IS_SCS_IN_V_SY_4`4`;
 780 IS_SCS_IN_V_SY_4`1`;
 781 IS_SCS_IN_V_SY_4`2`;
 782 IS_SCS_IN_V_SY_4`3`];
 783
 784 REWRITE_TAC[E_SY;rows]
 785 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
 786 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`]
 787 THEN GEN_TAC
 788 THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
 789 THEN EQ_TAC;
 790
 791 RESA_TAC
 792 THENL[
 793 IS_SCS_IN_V_SY_4`1`;
 794 IS_SCS_IN_V_SY_4`2`;
 795 IS_SCS_IN_V_SY_4`3`
 796 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`4`;`vv:num-> real^3`][ARITH_RULE`~(4=0)`]
 797 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 3`[ARITH_RULE`SUC 3 MOD 4=0/\ SUC 3=4`])
 798 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
 799 IS_SCS_IN_V_SY_4`0`];
 800
 801 STRIP_TAC
 802 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4)<=> (1<= i /\ i<= 4)`]
 803 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`4`;`vv:num-> real^3`][ARITH_RULE`~(4=0)`]
 804 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
 805 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
 806 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
 807 THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
 808 THEN MP_TAC(ARITH_RULE`x' MOD 4 < 4==>  x' MOD 4 =0 \/ x' MOD 4 = 1\/ x' MOD 4 = 2 \/ x' MOD 4 =3`)
 809 THEN RESA_TAC
 810 THENL[
 811 PROVE_E_SY_INV_TAC_4 `4`;
 812 PROVE_E_SY_INV_TAC_4 `1`;
 813 PROVE_E_SY_INV_TAC_4 `2`;
 814 PROVE_E_SY_INV_TAC_4 `3`];
 815
 816 REWRITE_TAC[F_SY;rows]
 817 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
 818 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`]
 819 THEN GEN_TAC
 820 THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
 821 THEN EQ_TAC;
 822
 823 RESA_TAC
 824 THENL[
 825 IS_SCS_IN_V_SY_4`1`;
 826 IS_SCS_IN_V_SY_4`2`;
 827 IS_SCS_IN_V_SY_4`3`
 828 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`4`;`vv:num-> real^3`][ARITH_RULE`~(4=0)`]
 829 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 3`[ARITH_RULE`SUC 3 MOD 4=0/\ SUC 3=4`])
 830 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
 831 IS_SCS_IN_V_SY_4`0`];
 832
 833 STRIP_TAC
 834 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4)<=> (1<= i /\ i<= 4)`]
 835 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`4`;`vv:num-> real^3`][ARITH_RULE`~(4=0)`]
 836 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
 837 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
 838 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
 839 THEN MRESAL_TAC DIVISION[`x':num`;`4`][ARITH_RULE`~(4=0)`]
 840 THEN MP_TAC(ARITH_RULE`x' MOD 4 < 4==>  x' MOD 4 =0 \/ x' MOD 4 = 1\/ x' MOD 4 = 2 \/ x' MOD 4 =3`)
 841 THEN RESA_TAC
 842 THENL[
 843 PROVE_E_SY_INV_TAC_4 `4`;
 844 PROVE_E_SY_INV_TAC_4 `1`;
 845 PROVE_E_SY_INV_TAC_4 `2`;
 846 PROVE_E_SY_INV_TAC_4 `3`]]);;
 847
 848
 849
 850
 851 let IN_IS_SCS_CASE_4=prove_by_refinement(
 852 ` is_scs_v39 s /\ scs_k_v39 s=4 /\ BBs_v39 s vv
 853 /\  dimindex(:M)= scs_k_v39 s
 854 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 0]:real^3^M= v
 855 /\ matvec (v:real^3^M) =a
 856 ==>
 857 a IN {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v }`
 858 ,
 859   (* {{{ proof *)
 860 [
 861 REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;IN_ELIM_THM;CONDITION1_SY;CONDITION2_SY;BBs_v39;LET_DEF;LET_END_DEF;change_type_v3;dist]
 862 THEN STRIP_TAC;
 863
 864 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
 865 THEN ASM_REWRITE_TAC[]
 866 THEN ARITH_TAC;
 867
 868 EXISTS_TAC`v:real^3^M`
 869 THEN ASM_REWRITE_TAC[]
 870 THEN STRIP_TAC;
 871
 872 REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`]
 873 THEN REPEAT STRIP_TAC
 874 THENL[
 875 IS_SCS_IN_BALL_ANNULUS_4 `1`;
 876 IS_SCS_IN_BALL_ANNULUS_4 `2`;
 877 IS_SCS_IN_BALL_ANNULUS_4 `3`;
 878 IS_SCS_IN_BALL_ANNULUS_4 `0`];
 879
 880 STRIP_TAC;
 881
 882 REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 4)<=> (i=1\/ i=2\/ i=3 \/ i=4)`]
 883 THEN REPEAT GEN_TAC
 884 THEN STRIP_TAC
 885 THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 4==> (i=1\/ i=2\/ i=3 \/ i=4)`)
 886 THEN RESA_TAC
 887 THEN MRESAL_TAC VECTOR_3_4[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=4/\ 2<=4/\ 3<=4/\ 4<=4/\ 4 MOD 4= 0 /\ 1 MOD 4= 1 /\ 2 MOD 4= 2/\ 3 MOD 4= 3/\ ~(2=1)
 888 /\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)`;SET_RULE`(a:num) IN (:num)`]
 889 THEN ASM_TAC
 890 THEN REWRITE_TAC[is_scs_v39;periodic2]
 891 THEN STRIP_TAC
 892 THEN REPEAT DISCH_TAC
 893 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 1`][periodic;ARITH_RULE`~(4=0)`]
 894 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
 895 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
 896 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 1`][periodic;ARITH_RULE`~(4=0)`]
 897 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
 898 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
 899 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 2`][periodic;ARITH_RULE`~(4=0)`]
 900 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
 901 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
 902 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 2`][periodic;ARITH_RULE`~(4=0)`]
 903 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
 904 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
 905 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 3`][periodic;ARITH_RULE`~(4=0)`]
 906 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
 907 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
 908 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 3`][periodic;ARITH_RULE`~(4=0)`]
 909 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
 910 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
 911 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 4`][periodic;ARITH_RULE`~(4=0)`]
 912 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
 913 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
 914 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 4`][periodic;ARITH_RULE`~(4=0)`]
 915 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
 916 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
 917 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 0`][periodic;ARITH_RULE`~(4=0)`]
 918 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
 919 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
 920 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(4=0)`]
 921 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])
 922 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
 923 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
 924 THEN POP_ASSUM(fun th-> MRESA_TAC th[`0`;`0`]);
 925
 926 MP_TAC V_E_FF_IS_SCS_CASES_4
 927 THEN ASM_REWRITE_TAC[]
 928 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;IN_ELIM_THM;CONDITION1_SY;CONDITION2_SY;BBs_v39;LET_DEF;LET_END_DEF;change_type_v3;dist;IN]
 929 THEN RESA_TAC]);;
 930
 931
 932
 933
 934
 935 let  IS_EAR_V25_EQ_EAR_SY=prove(`is_scs_v39 s /\ 3< scs_k_v39 s
 936 /\ stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
 937          (change_type_v3 (scs_a_v39 s)),
 938          (change_type_v3 (scs_b_v39 s)),
 939          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
 940          (\i. (1 + i) MOD scs_k_v39 s))=s1
 941 ==>
 942 (is_ear_v39 s <=> ear_sy s1)`,
 943 REPEAT STRIP_TAC
 944 THEN MP_TAC IS_SCS_STABLE_SYSTEM
 945 THEN ASM_REWRITE_TAC[]
 946 THEN STRIP_TAC
 947 THEN REWRITE_TAC[is_ear_v39;ear_sy]
 948 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
 949          (change_type_v3 (scs_a_v39 s))`;`
 950          (change_type_v3 (scs_b_v39 s))`;`
 951          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
 952          (\i. (1 + i) MOD scs_k_v39 s)`]
 953 THEN MP_TAC (ARITH_RULE`3< scs_k_v39 s==> (scs_k_v39 s - 1 +1)-0= scs_k_v39 s
 954 /\ ~(scs_k_v39 s=3)`)
 955 THEN RESA_TAC
 956 THEN MRESAL_TAC HAS_SIZE_NUMSEG[`0`;`scs_k_v39 s -1`][HAS_SIZE]);;
 957
 958
 959
 960
 961
 962
 963 let INJ_H_FUN_TAC=
 964 fun (so:term)->
 965 STRIP_TAC
 966 THENL[
 967 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`1 MOD 4=1 /\ SUC 1=2/\ 1+1=2 /\ 2 MOD 4=2/\ 1+2=3 /\ 3 MOD 4=3/\ 1+3=4 /\ 4 MOD 4=0/\ 1+0=1`]
 968 THEN REPEAT STRIP_TAC)
 969 THEN EXISTS_TAC so
 970 THEN EXPAND_TAC"h"
 971 THEN REWRITE_TAC[ARITH_RULE`1 MOD 4=1 /\ SUC 1=2/\ 1<4/\ ~(1=0)/\ 2<4 /\ 2 MOD 4=2 /\ ~(2=0)/\ SUC 2=3/\ 3<4/\ 3 MOD 4=3 /\ ~(3=0)/\ SUC 3=4/\ 0 MOD 4=0/\ 0<4/\ SUC 0=1`]
 972 THEN ASM_TAC
 973 THEN REWRITE_TAC[periodic;periodic2;is_scs_v39]
 974 THEN REPEAT STRIP_TAC
 975 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][periodic;ARITH_RULE`1 MOD 4=1 /\ SUC 1=2/\ 1<4/\ ~(4=0)`]
 976 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j:num`)
 977 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD 4)`][periodic;ARITH_RULE`1 MOD 4=1 /\ SUC 1=2/\ 1<4/\ ~(4=0)`]
 978 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i':num`)
 979 THEN POP_ASSUM MP_TAC
 980 THEN MP_TAC(SET_RULE`{1, 2} = {i' MOD 4, j MOD 4}
 981 ==> (1 =i' MOD 4 /\ 2= j MOD 4)\/ (2 =i' MOD 4 /\ 1= j MOD 4)`)
 982 THEN RESA_TAC
 983 THEN MP_TAC(SET_RULE`{2, 3} = {i' MOD 4, j MOD 4}
 984 ==> (2 =i' MOD 4 /\ 3= j MOD 4)\/ (3 =i' MOD 4 /\ 2= j MOD 4)`)
 985 THEN RESA_TAC
 986 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 3`][periodic;ARITH_RULE`1 MOD 4=1 /\ SUC 1=2/\ 1<4/\ ~(4=0)`]
 987 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4:num`[ARITH_RULE`4 MOD 4=0`])
 988 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
 989 THEN ASM_REWRITE_TAC[]
 990 THEN MP_TAC(SET_RULE`{3,0} = {i' MOD 4, j MOD 4}
 991 ==> (3 =i' MOD 4 /\ 0= j MOD 4)\/ (0 =i' MOD 4 /\ 3= j MOD 4)`)
 992 THEN RESA_TAC
 993 THEN MP_TAC(SET_RULE`{0,1} = {i' MOD 4, j MOD 4}
 994 ==> (i' MOD 4=1 /\ j MOD 4=0)\/ (i' MOD 4=0 /\ j MOD 4=1)`)
 995 THEN RESA_TAC;
 996 REPEAT STRIP_TAC
 997 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
 998 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
 999 THEN MATCH_MP_TAC th)
1000 THEN ASM_REWRITE_TAC[]];;
1001
1002
1003 let EXISTS_SCS_J_TAC=
1004 fun (so:term) (so1:term) (so2:term)->
1005 EXPAND_TAC "h"
1006 THEN REWRITE_TAC[ARITH_RULE`0 MOD 4=0/\SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4`]
1007 THEN STRIP_TAC
1008 THEN EXISTS_TAC so
1009 THEN ASM_REWRITE_TAC[ARITH_RULE`4 MOD 4=0/\ SUC 0=1/\ 1<=4/\ 4<=4/\ 1+0=1/\ 1 MOD 4=1/\ 1<=1/\ 1<=4/\ 1 MOD 4=1/\ 1+1=2/\ ~(1=0)/\ 2 MOD 4=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=4/\ 1+2=3/\ 3 MOD 4=3/\ 1<=3/\ 3<=4/\ 1+3=4/\ SUC 3=4/\ ~(3=0)`]
1010 THEN EXISTS_TAC so1
1011 THEN EXISTS_TAC so2
1012 THEN ASM_REWRITE_TAC[ARITH_RULE`0 MOD 4=0/\ 1 MOD 4=1/\ 2 MOD 4=2/\ 3 MOD 4=3/\ 4 MOD 4=0`]
1013 ;;
1014
1015
1016
1017
1018 let TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4=prove_by_refinement(
1019 `is_scs_v39 s /\ scs_k_v39 s=4
1020 /\ vv IN BBs_v39 s
1021 /\  dimindex(:M)=scs_k_v39 s
1022 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 0]:real^3^M= v
1023 /\ matvec (v:real^3^M) =a
1024 /\ stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
1025          (change_type_v3 (scs_a_v39 s)),
1026          (change_type_v3 (scs_b_v39 s)),
1027          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
1028          (\i. (1 + i) MOD scs_k_v39 s))=s1
1029 ==>  taustar_v39 s vv = tau_star s1 a`
1030 ,
1031   (* {{{ proof *)
1032 [
1033 REPEAT STRIP_TAC
1034 THEN POP_ASSUM MP_TAC
1035 THEN MP_TAC V_E_FF_IS_SCS_CASES_4
1036 THEN ASM_REWRITE_TAC[IN]
1037 THEN STRIP_TAC
1038 THEN STRIP_TAC
1039 THEN MP_TAC IS_SCS_STABLE_SYSTEM
1040 THEN ASM_REWRITE_TAC[ARITH_RULE`3<4`]
1041 THEN STRIP_TAC
1042 THEN ASM_REWRITE_TAC[taustar_v39;tau_star]
1043 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;IN;mk_unadorned_v39;]
1044 THEN ASM_SIMP_TAC[dsv_J_empty]
1045 THEN EXPAND_TAC"a"
1046 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
1047 THEN ASM_REWRITE_TAC[REAL_ARITH`A-B=A-C<=>B=C`;dsv_v39;d_fun]
1048 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
1049          (change_type_v3 (scs_a_v39 s))`;`
1050          (change_type_v3 (scs_b_v39 s))`;`
1051          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
1052          (\i. (1 + i) MOD scs_k_v39 s)`]
1053 THEN ASM_REWRITE_TAC[REAL_ARITH`A+B=A+C<=>B=C`;sigma_sy]
1054 THEN MP_TAC IS_EAR_V25_EQ_EAR_SY
1055 THEN ASM_REWRITE_TAC[ARITH_RULE`3<4`]
1056 THEN STRIP_TAC
1057 THEN ASM_REWRITE_TAC[REAL_EQ_MUL_LCANCEL;REAL_ARITH`~(#0.1 = &0)`]
1058 THEN SUBGOAL_THEN`~((if ear_sy s1 then &1 else -- &1) = &0)` ASSUME_TAC;
1059
1060 MP_TAC(SET_RULE`(ear_sy s1)\/ ~(ear_sy s1)`)
1061 THEN RESA_TAC
1062 THEN REAL_ARITH_TAC;
1063
1064 ASM_REWRITE_TAC[J1_SY ]
1065 THEN MATCH_MP_TAC SUM_EQ_GENERAL
1066 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1067 THEN ABBREV_TAC`h =(\i. if (i MOD 4 = 0) then (4,1)
1068 else (i MOD 4, SUC(i MOD 4)))`
1069 THEN SUBGOAL_THEN`(!x x'.
1070       (x < 4 /\ scs_J_v39 s x (SUC x))  /\
1071       (x' < 4 /\ scs_J_v39 s x' (SUC x')) /\
1072       h x' = (h:num->num #num) x
1073       ==> x = x')` ASSUME_TAC;
1074
1075 REPEAT STRIP_TAC
1076 THEN POP_ASSUM MP_TAC
1077 THEN MP_TAC(ARITH_RULE` x< 4 ==> x=0\/ x=1\/ x=2 \/ x=3 `)
1078 THEN RESA_TAC
1079 THEN MP_TAC(ARITH_RULE` x'< 4 ==> x'=0\/ x'=1\/ x'=2 \/ x'=3 `)
1080 THEN RESA_TAC
1081 THEN EXPAND_TAC"h"
1082 THEN REWRITE_TAC[ARITH_RULE`1 MOD 4=1 /\ 0 MOD 4=0/\ 2 MOD 4=2/\ 3 MOD 4=3 /\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ SUC 1=2/\ ~(1=4)/\ ~(2=4)/\ ~(3=4)`;ARITH_RULE`A=B <=> B=A:num`;PAIR_EQ;DE_MORGAN_THM]
1083 THEN RESA_TAC;
1084
1085 EXISTS_TAC`h:num->(num#num)`
1086 THEN ASM_REWRITE_TAC[change_type_v2;IN_ELIM_THM;IN_NUMSEG]
1087 THEN STRIP_TAC
1088 THEN REPEAT STRIP_TAC;
1089
1090 ASM_REWRITE_TAC[EXISTS_UNIQUE_THM]
1091 THEN MP_TAC(ARITH_RULE`1<= i/\ i<=4 ==> i=1\/ i=2 \/ i=3 \/ i=4`)
1092 THEN RESA_TAC
1093 THENL[
1094 INJ_H_FUN_TAC `1`;
1095 INJ_H_FUN_TAC `2`;
1096 INJ_H_FUN_TAC `3`;
1097 INJ_H_FUN_TAC `0`];
1098
1099 POP_ASSUM MP_TAC
1100 THEN MP_TAC(ARITH_RULE`x<4 ==> x=0 \/ x=1 \/ x=2 \/ x=3`)
1101 THEN RESA_TAC
1102 THENL[
1103 EXISTS_SCS_J_TAC `4` `0` `1`;
1104 EXISTS_SCS_J_TAC `1` `1` `2`;
1105 EXISTS_SCS_J_TAC `2` `2` `3`;
1106 EXISTS_SCS_J_TAC `3` `3` `4`];
1107
1108 POP_ASSUM MP_TAC
1109 THEN MP_TAC(ARITH_RULE`x<4 ==> x=0 \/ x=1 \/ x=2 \/ x=3`)
1110 THEN RESA_TAC
1111 THEN EXPAND_TAC"h"
1112 THEN REWRITE_TAC[ARITH_RULE`0 MOD 4=0/\ SUC 0=1`]
1113 THEN EXPAND_TAC"a"
1114 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
1115 THEN MRESAL_TAC VECTOR_3_4[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 0`][ARITH_RULE`1<=4/\ 2<=4/\ 3<=4/\ 4<=4/\ 4 MOD 4= 0 /\ 1 MOD 4= 1 /\ 2 MOD 4= 2/\ 3 MOD 4= 3/\ ~(2=1)/\ ~(2=0)
1116 /\ ~(3=0)/\ SUC 4 MOD 4= 1 /\ SUC 1 MOD 4= 2 /\ SUC 2 MOD 4= 3/\ SUC 3 MOD 4= 0/\ ~(3=1)/\ ~(1=0)/\ SUC 1=2/\ SUC 0=1 /\ SUC 2= 3/\ SUC 3=4 /\ SUC 4=5`;SET_RULE`(a:num)IN (:num)`;dist]
1117 THEN REPLICATE_TAC 25 (POP_ASSUM MP_TAC)
1118 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1119 THEN MP_TAC th)
1120 THEN ASM_REWRITE_TAC[IN;BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`]
1121 THEN REPEAT STRIP_TAC
1122 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(4=0)`]
1123 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`4`[ARITH_RULE`4 MOD 4=0`])]);;
1124
1125
1126
1127
1128 let JKQEWGV1_CASE_4=prove(
1129 `!s vv. is_scs_v39 s /\ scs_k_v39 s=4 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
1130 /\ dimindex(:M)=scs_k_v39 s
1131  ==>
1132   (sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
1133    (IMAGE (\i. (vv i,vv (SUC i))) (:num))  < pi)`,
1134 REPEAT GEN_TAC
1135 THEN STRIP_TAC
1136 THEN MP_TAC IS_SCS_STABLE_SYSTEM
1137 THEN RESA_TAC
1138 THEN POP_ASSUM MP_TAC
1139 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<4`]
1140 THEN STRIP_TAC
1141 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
1142          (change_type_v3 (scs_a_v39 s)),
1143          (change_type_v3 (scs_b_v39 s)),
1144          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
1145          (\i. (1 + i) MOD scs_k_v39 s))`
1146 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
1147          (change_type_v3 (scs_a_v39 s))`;`
1148          (change_type_v3 (scs_b_v39 s))`;`
1149          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
1150          (\i. (1 + i) MOD scs_k_v39 s)`]
1151 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 0]:real^3^M`
1152 THEN ABBREV_TAC`a=matvec (v:real^3^M)`
1153 THEN MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4
1154 THEN RESA_TAC
1155 THEN POP_ASSUM MP_TAC
1156 THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
1157 THEN STRIP_TAC
1158 THEN MP_TAC IN_IS_SCS_CASE_4
1159 THEN RESA_TAC
1160 THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<4`;]
1161 THEN REMOVE_ASSUM_TAC
1162 THEN POP_ASSUM MP_TAC
1163 THEN EXPAND_TAC"a"
1164 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
1165 THEN MP_TAC V_E_FF_IS_SCS_CASES_4
1166 THEN ASM_REWRITE_TAC[IN]
1167 THEN RESA_TAC
1168 THEN ASM_TAC
1169 THEN ASM_REWRITE_TAC[is_scs_v39;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;IN;mk_unadorned_v39]
1170 THEN REPEAT RESA_TAC
1171 THEN POP_ASSUM MP_TAC
1172 THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
1173 THEN RESA_TAC
1174 THEN MP_TAC(REAL_ARITH`pi <=
1175   sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
1176   (IMAGE (\i. vv i,vv (SUC i)) (:num)) \/
1177   sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
1178   (IMAGE (\i. vv i,vv (SUC i)) (:num))< pi`)
1179 THEN RESA_TAC
1180 THEN REPLICATE_TAC 19 REMOVE_ASSUM_TAC
1181 THEN POP_ASSUM MP_TAC
1182 THEN REAL_ARITH_TAC);;
1183
1184
1185
1186 let IS_SCS_IN_V_SY_5=
1187 fun (so:term)->
1188  EXISTS_TAC so
1189 THEN MRESAL_TAC VECTOR_3_5[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 4 MOD 5= 4/\ 5 MOD 5=0 /\ 1 MOD 5= 1 /\ 2 MOD 5= 2/\ 3 MOD 5= 3 /\ ~(2=1)/\ SUC 5 MOD 5=1
1190 /\ SUC 4 MOD 5= 0 /\ SUC 1 MOD 5= 2 /\ SUC 2 MOD 5= 3/\ SUC 3 MOD 5= 4/\ ~(3=1)/\ ~(1=0)/\ 5<=5/\ 1<=1 /\ 1<=2 /\ 1<= 3 /\ 1<=4 /\ 1<=5
1191 /\ SUC 1=2 /\ SUC 0 =1/\ SUC 2=3/\  SUC 3=4/\ SUC 4=5  `; SET_RULE`(a:num) IN (:num)`]
1192 ;;
1193
1194
1195 let PROVE_E_SY_INV_TAC_5=
1196 fun (th:term)->
1197 MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x':num`;th;`5`][ARITH_RULE`~(5=0)/\ 4 MOD 5=4/\ SUC 0  MOD 5=1/\ 1 MOD 5=1 /\ 2 MOD 5=2 /\ 3 MOD 5=3/\ 5 MOD 5=0`]
1198 THEN EXISTS_TAC th
1199 THEN MRESAL_TAC VECTOR_3_5[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 4 MOD 5= 4/\ 5 MOD 5=0 /\ 1 MOD 5= 1 /\ 2 MOD 5= 2/\ 3 MOD 5= 3 /\ ~(2=1)/\ SUC 5 MOD 5=1
1200 /\ SUC 4 MOD 5= 0 /\ SUC 1 MOD 5= 2 /\ SUC 2 MOD 5= 3/\ SUC 3 MOD 5= 4/\ ~(3=1)/\ ~(1=0)/\ 5<=5/\ 1<=1 /\ 1<=2 /\ 1<= 3 /\ 1<=4 /\ 1<=5
1201 /\ SUC 1=2 /\ SUC 0 =1/\ SUC 2=3/\  SUC 3=4/\ SUC 4=5  `; SET_RULE`(a:num) IN (:num)`]
1202 ;;
1203
1204
1205
1206
1207
1208
1209
1210
1211 let V_E_FF_IS_SCS_CASES_5=prove_by_refinement(
1212 ` is_scs_v39 s /\ scs_k_v39 s=5 /\ vv IN BBs_v39 s
1213 /\  dimindex(:M)=scs_k_v39 s
1214 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 0]:real^3^M= v
1215 /\ matvec (v:real^3^M) =a
1216 ==>
1217 V_SY (v:real^3^M)=IMAGE vv (:num)/\
1218   E_SY (v:real^3^M)=IMAGE (\i. {vv i, vv (SUC i)}) (:num)/\
1219 F_SY (v:real^3^M)=IMAGE (\i. vv i,vv (SUC i)) (:num)`,
1220   (* {{{ proof *)
1221 [
1222
1223 STRIP_TAC
1224 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1225 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(5<=3)`;IN;mk_unadorned_v39]
1226 THEN REPEAT STRIP_TAC;
1227
1228 REWRITE_TAC[V_SY;rows]
1229 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5)`]
1230 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
1231 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5)`]
1232 THEN GEN_TAC
1233 THEN EQ_TAC;
1234
1235 REPEAT STRIP_TAC
1236 THENL[
1237 IS_SCS_IN_V_SY_5`1`;
1238 IS_SCS_IN_V_SY_5`2`;
1239 IS_SCS_IN_V_SY_5`3`;
1240 IS_SCS_IN_V_SY_5`4`;
1241 IS_SCS_IN_V_SY_5`0`];
1242
1243 REPEAT STRIP_TAC
1244 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)<=> (1<= i /\ i<= 5)`]
1245 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`5`;`vv:num-> real^3`][ARITH_RULE`~(5=0)`]
1246 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`)
1247 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1248 THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
1249 THEN MP_TAC(ARITH_RULE`x' MOD 5 < 5==>  x' MOD 5 =0 \/ x' MOD 5 = 1\/ x' MOD 5 = 2 \/ x' MOD 5 =3\/ x' MOD 5 =4`)
1250 THEN RESA_TAC
1251 THENL[
1252 IS_SCS_IN_V_SY_5`5`;
1253 IS_SCS_IN_V_SY_5`1`;
1254 IS_SCS_IN_V_SY_5`2`;
1255 IS_SCS_IN_V_SY_5`3`;
1256 IS_SCS_IN_V_SY_5`4`];
1257
1258 REWRITE_TAC[E_SY;rows]
1259 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
1260 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)`]
1261 THEN GEN_TAC
1262 THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
1263 THEN EQ_TAC;
1264
1265 RESA_TAC
1266 THENL[
1267 IS_SCS_IN_V_SY_5`1`;
1268 IS_SCS_IN_V_SY_5`2`;
1269 IS_SCS_IN_V_SY_5`3`;
1270 IS_SCS_IN_V_SY_5`4`
1271 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`5`;`vv:num-> real^3`][ARITH_RULE`~(5=0)`]
1272 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 4`[ARITH_RULE`SUC 4 MOD 5=0/\ SUC 4=5`])
1273 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
1274 IS_SCS_IN_V_SY_5`0`];
1275
1276 STRIP_TAC
1277 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5)<=> (1<= i /\ i<= 5)`]
1278 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`5`;`vv:num-> real^3`][ARITH_RULE`~(5=0)`]
1279 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
1280 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1281 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1282 THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
1283 THEN MP_TAC(ARITH_RULE`x' MOD 5 < 5==>  x' MOD 5 =0 \/ x' MOD 5 = 1\/ x' MOD 5 = 2 \/ x' MOD 5 =3 \/ x' MOD 5 =4`)
1284 THEN RESA_TAC
1285 THENL[
1286 PROVE_E_SY_INV_TAC_5 `5`;
1287 PROVE_E_SY_INV_TAC_5 `1`;
1288 PROVE_E_SY_INV_TAC_5 `2`;
1289 PROVE_E_SY_INV_TAC_5 `3`;
1290 PROVE_E_SY_INV_TAC_5 `4`];
1291
1292 REWRITE_TAC[F_SY;rows]
1293 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
1294 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)`]
1295 THEN GEN_TAC
1296 THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
1297 THEN EQ_TAC;
1298
1299 RESA_TAC
1300 THENL[
1301 IS_SCS_IN_V_SY_5`1`;
1302 IS_SCS_IN_V_SY_5`2`;
1303 IS_SCS_IN_V_SY_5`3`;
1304 IS_SCS_IN_V_SY_5`4`
1305 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`5`;`vv:num-> real^3`][ARITH_RULE`~(5=0)`]
1306 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 4`[ARITH_RULE`SUC 4 MOD 5=0/\ SUC 4=5`])
1307 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
1308 IS_SCS_IN_V_SY_5`0`];
1309
1310 STRIP_TAC
1311 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5)<=> (1<= i /\ i<= 5)`]
1312 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`5`;`vv:num-> real^3`][ARITH_RULE`~(5=0)`]
1313 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
1314 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1315 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1316 THEN MRESAL_TAC DIVISION[`x':num`;`5`][ARITH_RULE`~(5=0)`]
1317 THEN MP_TAC(ARITH_RULE`x' MOD 5 < 5==>  x' MOD 5 =0 \/ x' MOD 5 = 1\/ x' MOD 5 = 2 \/ x' MOD 5 =3 \/ x' MOD 5 =4`)
1318 THEN RESA_TAC
1319 THENL[
1320 PROVE_E_SY_INV_TAC_5 `5`;
1321 PROVE_E_SY_INV_TAC_5 `1`;
1322 PROVE_E_SY_INV_TAC_5 `2`;
1323 PROVE_E_SY_INV_TAC_5 `3`;
1324 PROVE_E_SY_INV_TAC_5 `4`];
1325 ]);;
1326
1327
1328
1329 let IS_SCS_IN_BALL_ANNULUS_5=
1330 fun (so:term)->
1331 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1332 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1333 THEN MP_TAC th THEN REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM])
1334 THEN STRIP_TAC
1335 THEN POP_ASSUM MATCH_MP_TAC
1336 THEN EXISTS_TAC so
1337 THEN MRESAL_TAC VECTOR_3_5[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 4 MOD 5= 4/\ 5 MOD 5=0 /\ 1 MOD 5= 1 /\ 2 MOD 5= 2/\ 3 MOD 5= 3 /\ ~(2=1)/\ SUC 5 MOD 5=1
1338 /\ SUC 4 MOD 5= 0 /\ SUC 1 MOD 5= 2 /\ SUC 2 MOD 5= 3/\ SUC 3 MOD 5= 4/\ ~(3=1)/\ ~(1=0)/\ 5<=5/\ 1<=1 /\ 1<=2 /\ 1<= 3 /\ 1<=4 /\ 1<=5
1339 /\ SUC 1=2 /\ SUC 0 =1/\ SUC 2=3/\  SUC 3=4/\ SUC 4=5  `; SET_RULE`(a:num) IN (:num)`]
1340 ;;
1341
1342
1343
1344
1345 let IN_IS_SCS_CASE_5=prove_by_refinement(
1346 ` is_scs_v39 s /\ scs_k_v39 s=5 /\ BBs_v39 s vv
1347 /\  dimindex(:M)= scs_k_v39 s
1348 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 0]:real^3^M= v
1349 /\ matvec (v:real^3^M) =a
1350 ==>
1351 a IN {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v }`,
1352   (* {{{ proof *)
1353 [
1354
1355 REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;IN_ELIM_THM;CONDITION1_SY;CONDITION2_SY;BBs_v39;LET_DEF;LET_END_DEF;change_type_v3;dist]
1356 THEN STRIP_TAC;
1357
1358 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1359 THEN ASM_REWRITE_TAC[]
1360 THEN ARITH_TAC;
1361
1362 EXISTS_TAC`v:real^3^M`
1363 THEN ASM_REWRITE_TAC[]
1364 THEN STRIP_TAC;
1365
1366 REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)`]
1367 THEN REPEAT STRIP_TAC
1368 THENL[
1369 IS_SCS_IN_BALL_ANNULUS_5 `1`;
1370 IS_SCS_IN_BALL_ANNULUS_5 `2`;
1371 IS_SCS_IN_BALL_ANNULUS_5 `3`;
1372 IS_SCS_IN_BALL_ANNULUS_5 `4`;
1373 IS_SCS_IN_BALL_ANNULUS_5 `0`];
1374
1375 STRIP_TAC;
1376
1377 REWRITE_TAC[ARITH_RULE`(1<=i /\ i<= 5)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)`]
1378 THEN REPEAT GEN_TAC
1379 THEN STRIP_TAC
1380 THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 5==> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5)`)
1381 THEN RESA_TAC
1382 THEN MRESAL_TAC VECTOR_3_5[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 4 MOD 5= 4/\ 5 MOD 5=0 /\ 1 MOD 5= 1 /\ 2 MOD 5= 2/\ 3 MOD 5= 3 /\ ~(2=1)/\ SUC 5 MOD 5=1
1383 /\ SUC 4 MOD 5= 0 /\ SUC 1 MOD 5= 2 /\ SUC 2 MOD 5= 3/\ SUC 3 MOD 5= 4/\ ~(3=1)/\ ~(1=0)/\ 5<=5/\ 1<=1 /\ 1<=2 /\ 1<= 3 /\ 1<=4 /\ 1<=5
1384 /\ SUC 1=2 /\ SUC 0 =1/\ SUC 2=3/\  SUC 3=4/\ SUC 4=5  `; SET_RULE`(a:num) IN (:num)`]
1385 THEN ASM_TAC
1386 THEN REWRITE_TAC[is_scs_v39;periodic2]
1387 THEN STRIP_TAC
1388 THEN REPEAT DISCH_TAC
1389 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 1`][periodic;ARITH_RULE`~(5=0)`]
1390 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1391 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1392 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 1`][periodic;ARITH_RULE`~(5=0)`]
1393 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1394 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1395 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 2`][periodic;ARITH_RULE`~(5=0)`]
1396 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1397 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1398 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 2`][periodic;ARITH_RULE`~(5=0)`]
1399 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1400 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1401 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 3`][periodic;ARITH_RULE`~(5=0)`]
1402 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1403 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1404 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 3`][periodic;ARITH_RULE`~(5=0)`]
1405 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1406 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1407 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 4`][periodic;ARITH_RULE`~(5=0)`]
1408 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1409 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1410 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 4`][periodic;ARITH_RULE`~(5=0)`]
1411 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1412 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1413 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 5`][periodic;ARITH_RULE`~(5=0)`]
1414 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1415 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1416 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 5`][periodic;ARITH_RULE`~(5=0)`]
1417 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1418 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1419 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 0`][periodic;ARITH_RULE`~(5=0)`]
1420 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1421 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
1422 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(5=0)`]
1423 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`])
1424 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
1425 THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
1426 THEN POP_ASSUM(fun th-> MRESA_TAC th[`0`;`0`]);
1427
1428 MP_TAC V_E_FF_IS_SCS_CASES_5
1429 THEN ASM_REWRITE_TAC[]
1430 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;IN_ELIM_THM;CONDITION1_SY;CONDITION2_SY;BBs_v39;LET_DEF;LET_END_DEF;change_type_v3;dist;IN]
1431 THEN RESA_TAC]);;
1432
1433
1434
1435
1436 let INJ_H_FUN_TAC=
1437 fun (so:term)->
1438 STRIP_TAC
1439 THENL[
1440 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`1 MOD 5=1 /\ SUC 1=2/\ 1+1=2 /\ 2 MOD 5=2/\ 1+2=3 /\ 3 MOD 5=3/\ 1+3=4 /\ 5 MOD 5=0/\ 1+0=1/\ 1+4=5 /\ 4 MOD 5=4`]
1441 THEN REPEAT STRIP_TAC)
1442 THEN EXISTS_TAC so
1443 THEN EXPAND_TAC"h"
1444 THEN REWRITE_TAC[ARITH_RULE`1 MOD 5=1 /\ SUC 1=2/\ 1<5/\ ~(1=0)/\ 2<5 /\ 2 MOD 5=2 /\ ~(2=0)/\ SUC 2=3/\ 3<5/\ 3 MOD 5=3 /\ ~(3=0)/\ SUC 3=4/\ 0 MOD 5=0/\ 0<5/\ SUC 0=1/\4<5 /\ SUC 4=5/\ ~(4=0)/\ 4 MOD 5=4`]
1445 THEN ASM_TAC
1446 THEN REWRITE_TAC[periodic;periodic2;is_scs_v39]
1447 THEN REPEAT STRIP_TAC
1448 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][periodic;ARITH_RULE`1 MOD 5=1 /\ SUC 1=2/\ 1<5/\ ~(5=0)`]
1449 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j:num`)
1450 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD 5)`][periodic;ARITH_RULE`1 MOD 5=1 /\ SUC 1=2/\ 1<5/\ ~(5=0)`]
1451 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i':num`)
1452 THEN POP_ASSUM MP_TAC
1453 THEN MP_TAC(SET_RULE`{1, 2} = {i' MOD 5, j MOD 5}
1454 ==> (1 =i' MOD 5 /\ 2= j MOD 5)\/ (2 =i' MOD 5 /\ 1= j MOD 5)`)
1455 THEN RESA_TAC
1456 THEN MP_TAC(SET_RULE`{2, 3} = {i' MOD 5, j MOD 5}
1457 ==> (2 =i' MOD 5 /\ 3= j MOD 5)\/ (3 =i' MOD 5 /\ 2= j MOD 5)`)
1458 THEN RESA_TAC
1459 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 4`][periodic;ARITH_RULE`1 MOD 5=1 /\ SUC 1=2/\ 1<5/\ ~(5=0)`]
1460 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5:num`[ARITH_RULE`5 MOD 5=0`])
1461 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
1462 THEN ASM_REWRITE_TAC[]
1463 THEN MP_TAC(SET_RULE`{3,4} = {i' MOD 5, j MOD 5}
1464 ==> (3 =i' MOD 5 /\ 4= j MOD 5)\/ (4 =i' MOD 5 /\ 3= j MOD 5)`)
1465 THEN RESA_TAC
1466 THEN MP_TAC(SET_RULE`{4,0} = {i' MOD 5, j MOD 5}
1467 ==> (4=i' MOD 5 /\ 0=j MOD 5)\/ (0=i' MOD 5 /\  4=j MOD 5)`)
1468 THEN RESA_TAC
1469 THEN MP_TAC(SET_RULE`{0,1} = {i' MOD 5, j MOD 5}
1470 ==> (i' MOD 5=1 /\ j MOD 5=0)\/ (i' MOD 5=0 /\ j MOD 5=1)`)
1471 THEN RESA_TAC;
1472 REPEAT STRIP_TAC
1473 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
1474 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1475 THEN MATCH_MP_TAC th)
1476 THEN ASM_REWRITE_TAC[]];;
1477
1478
1479
1480
1481
1482 let EXISTS_SCS_J_TAC=
1483 fun (so:term) (so1:term) (so2:term)->
1484 EXPAND_TAC "h"
1485 THEN REWRITE_TAC[ARITH_RULE`0 MOD 5=0/\SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5`]
1486 THEN STRIP_TAC
1487 THEN EXISTS_TAC so
1488 THEN ASM_REWRITE_TAC[ARITH_RULE`5 MOD 5=0/\ SUC 0=1/\ 1<=5/\ 5<=5/\ 1+0=1/\ 1 MOD 5=1/\ 1<=1/\ 1<=5/\ 1 MOD 5=1/\ 1+1=2/\ ~(1=0)/\ 2 MOD 5=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=5/\ 1+2=3/\ 3 MOD 5=3/\ 1<=3/\ 3<=5/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ ~(4=0)/\ 1<=4/\ 4<=5/\ SUC 4=5/\ 4 MOD 5=4/\ 1+4=5`]
1489 THEN EXISTS_TAC so1
1490 THEN EXISTS_TAC so2
1491 THEN ASM_REWRITE_TAC[ARITH_RULE`0 MOD 5=0/\ 1 MOD 5=1/\ 2 MOD 5=2/\ 3 MOD 5=3/\ 5 MOD 5=0/\ 4 MOD 5=4`]
1492 ;;
1493
1494
1495
1496
1497
1498 let TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5=prove_by_refinement(
1499 `is_scs_v39 s /\ scs_k_v39 s=5
1500 /\ vv IN BBs_v39 s
1501 /\  dimindex(:M)=scs_k_v39 s
1502 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 0]:real^3^M= v
1503 /\ matvec (v:real^3^M) =a
1504 /\ stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
1505          (change_type_v3 (scs_a_v39 s)),
1506          (change_type_v3 (scs_b_v39 s)),
1507          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
1508          (\i. (1 + i) MOD scs_k_v39 s))=s1
1509 ==>  taustar_v39 s vv = tau_star s1 a`,
1510   (* {{{ proof *)
1511 [
1512 REPEAT STRIP_TAC
1513 THEN POP_ASSUM MP_TAC
1514 THEN MP_TAC V_E_FF_IS_SCS_CASES_5
1515 THEN ASM_REWRITE_TAC[IN]
1516 THEN STRIP_TAC
1517 THEN STRIP_TAC
1518 THEN MP_TAC IS_SCS_STABLE_SYSTEM
1519 THEN ASM_REWRITE_TAC[ARITH_RULE`3<5`]
1520 THEN STRIP_TAC
1521 THEN ASM_REWRITE_TAC[taustar_v39;tau_star]
1522 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(5<=3)`;IN;mk_unadorned_v39;]
1523 THEN ASM_SIMP_TAC[dsv_J_empty]
1524 THEN EXPAND_TAC"a"
1525 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
1526 THEN ASM_REWRITE_TAC[REAL_ARITH`A-B=A-C<=>B=C`;dsv_v39;d_fun]
1527 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
1528          (change_type_v3 (scs_a_v39 s))`;`
1529          (change_type_v3 (scs_b_v39 s))`;`
1530          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
1531          (\i. (1 + i) MOD scs_k_v39 s)`]
1532 THEN ASM_REWRITE_TAC[REAL_ARITH`A+B=A+C<=>B=C`;sigma_sy]
1533 THEN MP_TAC IS_EAR_V25_EQ_EAR_SY
1534 THEN ASM_REWRITE_TAC[ARITH_RULE`3<5`]
1535 THEN STRIP_TAC
1536 THEN ASM_REWRITE_TAC[REAL_EQ_MUL_LCANCEL;REAL_ARITH`~(#0.1 = &0)`]
1537 THEN SUBGOAL_THEN`~((if ear_sy s1 then &1 else -- &1) = &0)` ASSUME_TAC;
1538
1539 MP_TAC(SET_RULE`(ear_sy s1)\/ ~(ear_sy s1)`)
1540 THEN RESA_TAC
1541 THEN REAL_ARITH_TAC;
1542
1543 ASM_REWRITE_TAC[J1_SY ]
1544 THEN MATCH_MP_TAC SUM_EQ_GENERAL
1545 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
1546 THEN ABBREV_TAC`h =(\i. if (i MOD 5 = 0) then (5,1)
1547 else (i MOD 5, SUC(i MOD 5)))`
1548 THEN SUBGOAL_THEN`(!x x'.
1549       (x < 5 /\ scs_J_v39 s x (SUC x))  /\
1550       (x' < 5 /\ scs_J_v39 s x' (SUC x')) /\
1551       h x' = (h:num->num #num) x
1552       ==> x = x')` ASSUME_TAC;
1553
1554 REPEAT STRIP_TAC
1555 THEN POP_ASSUM MP_TAC
1556 THEN MP_TAC(ARITH_RULE` x< 5 ==> x=0\/ x=1\/ x=2 \/ x=3\/ x=4 `)
1557 THEN RESA_TAC
1558 THEN MP_TAC(ARITH_RULE` x'< 5 ==> x'=0\/ x'=1\/ x'=2 \/ x'=3  \/ x'=4`)
1559 THEN RESA_TAC
1560 THEN EXPAND_TAC"h"
1561 THEN REWRITE_TAC[ARITH_RULE`1 MOD 5=1 /\ 0 MOD 5=0/\ 2 MOD 5=2/\ 3 MOD 5=3 /\ 4 MOD 5=4/\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(4=0)/\ SUC 1=2/\ ~(1=5)/\ ~(2=5)/\ ~(3=5)/\ ~(4=5)`;ARITH_RULE`A=B <=> B=A:num`;PAIR_EQ;DE_MORGAN_THM]
1562 THEN RESA_TAC;
1563
1564 EXISTS_TAC`h:num->(num#num)`
1565 THEN ASM_REWRITE_TAC[change_type_v2;IN_ELIM_THM;IN_NUMSEG]
1566 THEN STRIP_TAC
1567 THEN REPEAT STRIP_TAC;
1568
1569 ASM_REWRITE_TAC[EXISTS_UNIQUE_THM]
1570 THEN MP_TAC(ARITH_RULE`1<= i/\ i<=5 ==> i=1\/ i=2 \/ i=3 \/ i=4 \/i=5 `)
1571 THEN RESA_TAC
1572 THENL[
1573 INJ_H_FUN_TAC `1`;
1574 INJ_H_FUN_TAC `2`;
1575 INJ_H_FUN_TAC `3`;
1576 INJ_H_FUN_TAC `4`;
1577 INJ_H_FUN_TAC `0`];
1578
1579 POP_ASSUM MP_TAC
1580 THEN MP_TAC(ARITH_RULE`x<5 ==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4`)
1581 THEN RESA_TAC
1582 THENL[
1583 EXISTS_SCS_J_TAC `5` `0` `1`;
1584 EXISTS_SCS_J_TAC `1` `1` `2`;
1585 EXISTS_SCS_J_TAC `2` `2` `3`;
1586 EXISTS_SCS_J_TAC `3` `3` `4`;
1587 EXISTS_SCS_J_TAC `4` `4` `5`];
1588
1589 POP_ASSUM MP_TAC
1590 THEN MP_TAC(ARITH_RULE`x<5 ==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4`)
1591 THEN RESA_TAC
1592 THEN EXPAND_TAC"h"
1593 THEN REWRITE_TAC[ARITH_RULE`0 MOD 5=0/\ SUC 0=1`]
1594 THEN EXPAND_TAC"a"
1595 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
1596 THEN MRESAL_TAC VECTOR_3_5[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 0`;][ARITH_RULE`1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ 4 MOD 5= 4/\ 5 MOD 5=0 /\ 1 MOD 5= 1 /\ 2 MOD 5= 2/\ 3 MOD 5= 3 /\ ~(2=1)/\ SUC 5 MOD 5=1/\ ~(2=0) /\ ~(3=0)/\ ~(4=0)
1597 /\ SUC 4 MOD 5= 0 /\ SUC 1 MOD 5= 2 /\ SUC 2 MOD 5= 3/\ SUC 3 MOD 5= 4/\ ~(3=1)/\ ~(1=0)/\ 5<=5/\ 1<=1 /\ 1<=2 /\ 1<= 3 /\ 1<=4 /\ 1<=5
1598 /\ SUC 1=2 /\ SUC 0 =1/\ SUC 2=3/\  SUC 3=4/\ SUC 4=5  `; SET_RULE`(a:num) IN (:num)`;dist]
1599 THEN REPLICATE_TAC 26 (POP_ASSUM MP_TAC)
1600 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1601 THEN MP_TAC th)
1602 THEN ASM_REWRITE_TAC[IN;BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`]
1603 THEN REPEAT STRIP_TAC
1604 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(5=0)`]
1605 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`5`[ARITH_RULE`5 MOD 5=0`]);]);;
1606
1607
1608
1609
1610 let JKQEWGV1_CASE_5=prove(`!s vv. is_scs_v39 s /\ scs_k_v39 s=5 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
1611 /\ dimindex(:M)=scs_k_v39 s
1612  ==>
1613   (sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
1614    (IMAGE (\i. (vv i,vv (SUC i))) (:num))  < pi)`,
1615 REPEAT GEN_TAC
1616 THEN STRIP_TAC
1617 THEN MP_TAC IS_SCS_STABLE_SYSTEM
1618 THEN RESA_TAC
1619 THEN POP_ASSUM MP_TAC
1620 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<5`]
1621 THEN STRIP_TAC
1622 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
1623          (change_type_v3 (scs_a_v39 s)),
1624          (change_type_v3 (scs_b_v39 s)),
1625          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
1626          (\i. (1 + i) MOD scs_k_v39 s))`
1627 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
1628          (change_type_v3 (scs_a_v39 s))`;`
1629          (change_type_v3 (scs_b_v39 s))`;`
1630          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
1631          (\i. (1 + i) MOD scs_k_v39 s)`]
1632 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 0]:real^3^M`
1633 THEN ABBREV_TAC`a=matvec (v:real^3^M)`
1634 THEN MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5
1635 THEN RESA_TAC
1636 THEN POP_ASSUM MP_TAC
1637 THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
1638 THEN STRIP_TAC
1639 THEN MP_TAC IN_IS_SCS_CASE_5
1640 THEN RESA_TAC
1641 THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<5`;]
1642 THEN REMOVE_ASSUM_TAC
1643 THEN POP_ASSUM MP_TAC
1644 THEN EXPAND_TAC"a"
1645 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
1646 THEN MP_TAC V_E_FF_IS_SCS_CASES_5
1647 THEN ASM_REWRITE_TAC[IN]
1648 THEN RESA_TAC
1649 THEN ASM_TAC
1650 THEN ASM_REWRITE_TAC[is_scs_v39;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(5<=3)`;IN;mk_unadorned_v39]
1651 THEN REPEAT RESA_TAC
1652 THEN POP_ASSUM MP_TAC
1653 THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
1654 THEN RESA_TAC
1655 THEN MP_TAC(REAL_ARITH`pi <=
1656   sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
1657   (IMAGE (\i. vv i,vv (SUC i)) (:num)) \/
1658   sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
1659   (IMAGE (\i. vv i,vv (SUC i)) (:num))< pi`)
1660 THEN RESA_TAC
1661 THEN REPLICATE_TAC 19 REMOVE_ASSUM_TAC
1662 THEN POP_ASSUM MP_TAC
1663 THEN REAL_ARITH_TAC);;
1664
1665
1666
1667
1668 let IS_SCS_IN_V_SY_6=
1669 fun (so:term)->
1670  EXISTS_TAC so
1671 THEN MRESAL_TAC VECTOR_3_6[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 5`;`(vv:num->real^3) 0`][ARITH_RULE`1<=6/\ 2<=6/\ 3<=6/\ 4<=6/\ 5<=6 /\ 6<=6 /\ 0 MOD 6= 0 /\ 1 MOD 6= 1 /\ 2 MOD 6= 2/\ 3 MOD 6= 3 /\ 4 MOD 6= 4 /\ 5 MOD 6=5 /\ 6 MOD 6=0 /\ ~(2=1)
1672 /\ SUC 0 MOD 6= 1 /\ SUC 1 MOD 6= 2 /\ SUC 2 MOD 6= 3/\ SUC 3 MOD 6= 4
1673 /\ SUC 4 MOD 6= 5 /\ SUC 5 MOD 6 = 0 /\ SUC 6 MOD 6 =1 /\ ~(3=1)/\ ~(1=0)
1674 /\ 1<=1 /\1<=2/\ 1<=3/\ 1<=4/\1<=5
1675 /\ SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`; SET_RULE`(a:num) IN (:num)`]
1676 ;;
1677
1678
1679 let PROVE_E_SY_INV_TAC_6=
1680 fun (th:term)->
1681 MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x':num`;th;`6`][ARITH_RULE`~(6=0)/\ 4 MOD 6=4/\ SUC 0  MOD 6=1/\ 1 MOD 6=1 /\ 2 MOD 6=2 /\ 3 MOD 6=3/\ 6 MOD 6=0/\ 5 MOD 6=5`]
1682 THEN EXISTS_TAC th
1683 THEN MRESAL_TAC VECTOR_3_6[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 5`;`(vv:num->real^3) 0`][ARITH_RULE`1<=6/\ 2<=6/\ 3<=6/\ 4<=6/\ 5<=6 /\ 6<=6 /\ 0 MOD 6= 0 /\ 1 MOD 6= 1 /\ 2 MOD 6= 2/\ 3 MOD 6= 3 /\ 4 MOD 6= 4 /\ 5 MOD 6=5 /\ 6 MOD 6=0 /\ ~(2=1)
1684 /\ SUC 0 MOD 6= 1 /\ SUC 1 MOD 6= 2 /\ SUC 2 MOD 6= 3/\ SUC 3 MOD 6= 4
1685 /\ SUC 4 MOD 6= 5 /\ SUC 5 MOD 6 = 0 /\ SUC 6 MOD 6 =1 /\ ~(3=1)/\ ~(1=0)
1686 /\ 1<=1 /\1<=2/\ 1<=3/\ 1<=4/\1<=5
1687 /\ SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`; SET_RULE`(a:num) IN (:num)`]
1688 ;;
1689
1690
1691
1692
1693
1694
1695
1696
1697 let V_E_FF_IS_SCS_CASES_6=prove_by_refinement(
1698 ` is_scs_v39 s /\ scs_k_v39 s=6 /\ vv IN BBs_v39 s
1699 /\  dimindex(:M)=scs_k_v39 s
1700 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 5;(vv:num->real^3) 0]:real^3^M= v
1701 /\ matvec (v:real^3^M) =a
1702 ==>
1703 V_SY (v:real^3^M)=IMAGE vv (:num)/\
1704   E_SY (v:real^3^M)=IMAGE (\i. {vv i, vv (SUC i)}) (:num)/\
1705 F_SY (v:real^3^M)=IMAGE (\i. vv i,vv (SUC i)) (:num)`,
1706   (* {{{ proof *)
1707 [
1708 STRIP_TAC
1709 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1710 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`;IN;mk_unadorned_v39]
1711 THEN REPEAT STRIP_TAC;
1712
1713 REWRITE_TAC[V_SY;rows]
1714 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5\/ i=6)`]
1715 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
1716 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5\/ i=6)`]
1717 THEN GEN_TAC
1718 THEN EQ_TAC;
1719
1720 REPEAT STRIP_TAC
1721 THENL[
1722 IS_SCS_IN_V_SY_6`1`;
1723 IS_SCS_IN_V_SY_6`2`;
1724 IS_SCS_IN_V_SY_6`3`;
1725 IS_SCS_IN_V_SY_6`4`;
1726 IS_SCS_IN_V_SY_6`5`;
1727 IS_SCS_IN_V_SY_6`0`];
1728
1729 REPEAT STRIP_TAC
1730 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)<=> (1<= i /\ i<= 6)`]
1731 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`6`;`vv:num-> real^3`][ARITH_RULE`~(6=0)`]
1732 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num`)
1733 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1734 THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
1735 THEN MP_TAC(ARITH_RULE`x' MOD 6 < 6==>  x' MOD 6 =0 \/ x' MOD 6 = 1\/ x' MOD 6 = 2 \/ x' MOD 6 =3\/ x' MOD 6 =4\/ x' MOD 6=5`)
1736 THEN RESA_TAC
1737 THENL[
1738 IS_SCS_IN_V_SY_6`6`;
1739 IS_SCS_IN_V_SY_6`1`;
1740 IS_SCS_IN_V_SY_6`2`;
1741 IS_SCS_IN_V_SY_6`3`;
1742 IS_SCS_IN_V_SY_6`4`;
1743 IS_SCS_IN_V_SY_6`5`];
1744
1745 REWRITE_TAC[E_SY;rows]
1746 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
1747 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)`]
1748 THEN GEN_TAC
1749 THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
1750 THEN EQ_TAC;
1751
1752 RESA_TAC
1753 THENL[
1754 IS_SCS_IN_V_SY_6`1`;
1755 IS_SCS_IN_V_SY_6`2`;
1756 IS_SCS_IN_V_SY_6`3`;
1757 IS_SCS_IN_V_SY_6`4`;
1758 IS_SCS_IN_V_SY_6`5`
1759 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`6`;`vv:num-> real^3`][ARITH_RULE`~(6=0)`]
1760 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 5`[ARITH_RULE`SUC 5 MOD 6=0/\ SUC 5=6`])
1761 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
1762 IS_SCS_IN_V_SY_6`0`];
1763
1764 STRIP_TAC
1765 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5\/ i=6)<=> (1<= i /\ i<= 6)`]
1766 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`6`;`vv:num-> real^3`][ARITH_RULE`~(6=0)`]
1767 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
1768 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1769 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1770 THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
1771 THEN MP_TAC(ARITH_RULE`x' MOD 6 < 6==>  x' MOD 6 =0 \/ x' MOD 6 = 1\/ x' MOD 6 = 2 \/ x' MOD 6 =3 \/ x' MOD 6 =4\/ x' MOD 6=5`)
1772 THEN RESA_TAC
1773 THENL[
1774 PROVE_E_SY_INV_TAC_6 `6`;
1775 PROVE_E_SY_INV_TAC_6 `1`;
1776 PROVE_E_SY_INV_TAC_6 `2`;
1777 PROVE_E_SY_INV_TAC_6 `3`;
1778 PROVE_E_SY_INV_TAC_6 `4`;
1779 PROVE_E_SY_INV_TAC_6 `5`;];
1780
1781 REWRITE_TAC[F_SY;rows]
1782 THEN ASM_REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM]
1783 THEN REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)`]
1784 THEN GEN_TAC
1785 THEN ONCE_REWRITE_TAC[GSYM EXTENSION]
1786 THEN EQ_TAC;
1787
1788 RESA_TAC
1789 THENL[
1790 IS_SCS_IN_V_SY_6`1`;
1791 IS_SCS_IN_V_SY_6`2`;
1792 IS_SCS_IN_V_SY_6`3`;
1793 IS_SCS_IN_V_SY_6`4`;
1794 IS_SCS_IN_V_SY_6`5`
1795 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`6`;`vv:num-> real^3`][ARITH_RULE`~(6=0)`]
1796 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`SUC 5`[ARITH_RULE`SUC 5 MOD 6=0/\ SUC 5=6`])
1797 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
1798 IS_SCS_IN_V_SY_6`0`];
1799
1800 STRIP_TAC
1801 THEN REWRITE_TAC[ARITH_RULE` (i=1\/ i=2\/ i=3 \/ i=4 \/ i=5\/ i=6)<=> (1<= i /\ i<= 6)`]
1802 THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`6`;`vv:num-> real^3`][ARITH_RULE`~(6=0)`]
1803 THEN POP_ASSUM (fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x':num`)
1804 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1805 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
1806 THEN MRESAL_TAC DIVISION[`x':num`;`6`][ARITH_RULE`~(6=0)`]
1807 THEN MP_TAC(ARITH_RULE`x' MOD 6 < 6==>  x' MOD 6 =0 \/ x' MOD 6 = 1\/ x' MOD 6 = 2 \/ x' MOD 6 =3 \/ x' MOD 6 =4\/ x' MOD 6=5`)
1808 THEN RESA_TAC
1809 THENL[
1810 PROVE_E_SY_INV_TAC_6 `6`;
1811 PROVE_E_SY_INV_TAC_6 `1`;
1812 PROVE_E_SY_INV_TAC_6 `2`;
1813 PROVE_E_SY_INV_TAC_6 `3`;
1814 PROVE_E_SY_INV_TAC_6 `4`;
1815 PROVE_E_SY_INV_TAC_6 `5`;]]);;
1816
1817
1818
1819
1820
1821
1822 let IS_SCS_IN_BALL_ANNULUS_6=
1823 fun (so:term)->
1824 REPLICATE_TAC 7 (POP_ASSUM MP_TAC)
1825 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1826 THEN MP_TAC th THEN REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM])
1827 THEN STRIP_TAC
1828 THEN POP_ASSUM MATCH_MP_TAC
1829 THEN EXISTS_TAC so
1830 THEN MRESAL_TAC VECTOR_3_6[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 5`;`(vv:num->real^3) 0`][ARITH_RULE`1<=6/\ 2<=6/\ 3<=6/\ 4<=6/\ 5<=6 /\ 6<=6 /\ 0 MOD 6= 0 /\ 1 MOD 6= 1 /\ 2 MOD 6= 2/\ 3 MOD 6= 3 /\ 4 MOD 6= 4 /\ 5 MOD 6=5 /\ 6 MOD 6=0 /\ ~(2=1)
1831 /\ SUC 0 MOD 6= 1 /\ SUC 1 MOD 6= 2 /\ SUC 2 MOD 6= 3/\ SUC 3 MOD 6= 4
1832 /\ SUC 4 MOD 6= 5 /\ SUC 5 MOD 6 = 0 /\ SUC 6 MOD 6 =1 /\ ~(3=1)/\ ~(1=0)
1833 /\ 1<=1 /\1<=2/\ 1<=3/\ 1<=4/\1<=5
1834 /\ SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`; SET_RULE`(a:num) IN (:num)`]
1835 ;;
1836
1837
1838
1839
1840 let IN_IS_SCS_CASE_6=prove_by_refinement(
1841 ` is_scs_v39 s /\ scs_k_v39 s=6 /\ BBs_v39 s vv
1842 /\  dimindex(:M)= scs_k_v39 s
1843 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 5;(vv:num->real^3) 0]:real^3^M= v
1844 /\ matvec (v:real^3^M) =a
1845 ==>
1846 a IN {matvec(v:real^3^M) | (!i. 1<=i /\  i <= dimindex(:M)==> row i v IN ball_annulus) /\  CONDITION1_SY (change_type_v3 (scs_a_v39 s)) (change_type_v3 (scs_b_v39 s)) v /\ CONDITION2_SY v }`,
1847   (* {{{ proof *)
1848 [
1849 REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;IN_ELIM_THM;CONDITION1_SY;CONDITION2_SY;BBs_v39;LET_DEF;LET_END_DEF;change_type_v3;dist]
1850 THEN STRIP_TAC;
1851
1852 REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
1853 THEN ASM_REWRITE_TAC[]
1854 THEN ARITH_TAC;
1855
1856 EXISTS_TAC`v:real^3^M`
1857 THEN ASM_REWRITE_TAC[]
1858 THEN STRIP_TAC;
1859
1860 REWRITE_TAC[ARITH_RULE`(1<= i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)`]
1861 THEN REPEAT STRIP_TAC
1862 THENL[
1863 IS_SCS_IN_BALL_ANNULUS_6 `1`;
1864 IS_SCS_IN_BALL_ANNULUS_6 `2`;
1865 IS_SCS_IN_BALL_ANNULUS_6 `3`;
1866 IS_SCS_IN_BALL_ANNULUS_6 `4`;
1867 IS_SCS_IN_BALL_ANNULUS_6 `5`;
1868 IS_SCS_IN_BALL_ANNULUS_6 `0`];
1869
1870 STRIP_TAC;
1871
1872 REWRITE_TAC[ARITH_RULE`(1<=i /\ i<= 6)<=> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)`]
1873 THEN REPEAT GEN_TAC
1874 THEN STRIP_TAC
1875 THEN MP_TAC(ARITH_RULE`1<=i /\ i<= 6==> (i=1\/ i=2\/ i=3 \/ i=4\/ i=5\/ i=6)`)
1876 THEN RESA_TAC
1877 THEN MRESAL_TAC VECTOR_3_6[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 5`;`(vv:num->real^3) 0`][ARITH_RULE`1<=6/\ 2<=6/\ 3<=6/\ 4<=6/\ 5<=6 /\ 6<=6 /\ 0 MOD 6= 0 /\ 1 MOD 6= 1 /\ 2 MOD 6= 2/\ 3 MOD 6= 3 /\ 4 MOD 6= 4 /\ 5 MOD 6=5 /\ 6 MOD 6=0 /\ ~(2=1)
1878 /\ SUC 0 MOD 6= 1 /\ SUC 1 MOD 6= 2 /\ SUC 2 MOD 6= 3/\ SUC 3 MOD 6= 4
1879 /\ SUC 4 MOD 6= 5 /\ SUC 5 MOD 6 = 0 /\ SUC 6 MOD 6 =1 /\ ~(3=1)/\ ~(1=0)
1880 /\ 1<=1 /\1<=2/\ 1<=3/\ 1<=4/\1<=5
1881 /\ SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`; SET_RULE`(a:num) IN (:num)`]
1882 THEN ASM_TAC
1883 THEN REWRITE_TAC[is_scs_v39;periodic2]
1884 THEN STRIP_TAC
1885 THEN REPEAT DISCH_TAC
1886 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 1`][periodic;ARITH_RULE`~(6=0)`]
1887 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1888 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1889 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 1`][periodic;ARITH_RULE`~(6=0)`]
1890 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1891 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1892 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 2`][periodic;ARITH_RULE`~(6=0)`]
1893 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1894 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1895 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 2`][periodic;ARITH_RULE`~(6=0)`]
1896 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1897 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1898 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 3`][periodic;ARITH_RULE`~(6=0)`]
1899 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1900 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1901 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 3`][periodic;ARITH_RULE`~(6=0)`]
1902 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1903 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1904 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 4`][periodic;ARITH_RULE`~(6=0)`]
1905 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1906 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1907 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 4`][periodic;ARITH_RULE`~(6=0)`]
1908 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1909 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1910 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 5`][periodic;ARITH_RULE`~(6=0)`]
1911 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1912 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1913 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 5`][periodic;ARITH_RULE`~(6=0)`]
1914 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1915 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1916 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 6`][periodic;ARITH_RULE`~(6=0)`]
1917 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1918 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1919 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 6`][periodic;ARITH_RULE`~(6=0)`]
1920 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1921 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;NORM_SUB])
1922 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_a_v39 s 0`][periodic;ARITH_RULE`~(6=0)`]
1923 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1924 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
1925 THEN MRESAL_TAC  (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s:num`;`scs_b_v39 s 0`][periodic;ARITH_RULE`~(6=0)`]
1926 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])
1927 THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th;])
1928 THEN REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
1929 THEN POP_ASSUM(fun th-> MRESA_TAC th[`0`;`0`]);
1930
1931 MP_TAC V_E_FF_IS_SCS_CASES_6
1932 THEN ASM_REWRITE_TAC[]
1933 THEN ASM_REWRITE_TAC[SET_RULE`~(A={})<=> (?a. a IN A)`;IN_ELIM_THM;CONDITION1_SY;CONDITION2_SY;BBs_v39;LET_DEF;LET_END_DEF;change_type_v3;dist;IN]
1934 THEN RESA_TAC]);;
1935
1936
1937
1938
1939 let INJ_H_FUN_TAC=
1940 fun (so:term)->
1941 STRIP_TAC
1942 THENL[
1943 POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th;ARITH_RULE`1 MOD 6=1 /\ SUC 1=2/\ 1+1=2 /\ 2 MOD 6=2/\ 1+2=3 /\ 3 MOD 6=3/\ 1+3=4 /\ 6 MOD 6=0/\ 1+0=1/\ 1+4=5 /\ 4 MOD 6=4/\ 1+5=6/\ 5 MOD 6=5`]
1944 THEN REPEAT STRIP_TAC)
1945 THEN EXISTS_TAC so
1946 THEN EXPAND_TAC"h"
1947 THEN REWRITE_TAC[ARITH_RULE`1 MOD 6=1 /\ SUC 1=2/\ 1<6/\ ~(1=0)/\ 2<6 /\ 2 MOD 6=2 /\ ~(2=0)/\ SUC 2=3/\ 3<6/\ 3 MOD 6=3 /\ ~(3=0)/\ SUC 3=4/\ 0 MOD 6=0/\ 0<6/\ SUC 0=1/\4<6 /\ SUC 4=5/\ ~(4=0)/\ 4 MOD 6=4/\ SUC 5=6/\ ~(5=0)/\ 5 MOD 6=5/\ 5<6`]
1948 THEN ASM_TAC
1949 THEN REWRITE_TAC[periodic;periodic2;is_scs_v39]
1950 THEN REPEAT STRIP_TAC
1951 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s i'`][periodic;ARITH_RULE`1 MOD 6=1 /\ SUC 1=2/\ 1<6/\ ~(6=0)`]
1952 THEN POP_ASSUM(fun th-> MRESA1_TAC th`j:num`)
1953 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s (j MOD 6)`][periodic;ARITH_RULE`1 MOD 6=1 /\ SUC 1=2/\ 1<6/\ ~(6=0)`]
1954 THEN POP_ASSUM(fun th-> MRESA1_TAC th`i':num`)
1955 THEN POP_ASSUM MP_TAC
1956 THEN MP_TAC(SET_RULE`{1, 2} = {i' MOD 6, j MOD 6}
1957 ==> (1 =i' MOD 6 /\ 2= j MOD 6)\/ (2 =i' MOD 6 /\ 1= j MOD 6)`)
1958 THEN RESA_TAC
1959 THEN MP_TAC(SET_RULE`{2, 3} = {i' MOD 6, j MOD 6}
1960 ==> (2 =i' MOD 6 /\ 3= j MOD 6)\/ (3 =i' MOD 6 /\ 2= j MOD 6)`)
1961 THEN RESA_TAC
1962 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_J_v39 s 5`][periodic;ARITH_RULE`1 MOD 6=1 /\ SUC 1=2/\ 1<6/\ ~(6=0)`]
1963 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6:num`[ARITH_RULE`6 MOD 6=0`])
1964 THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th))
1965 THEN ASM_REWRITE_TAC[]
1966 THEN MP_TAC(SET_RULE`{3,4} = {i' MOD 6, j MOD 6}
1967 ==> (3 =i' MOD 6 /\ 4= j MOD 6)\/ (4 =i' MOD 6 /\ 3= j MOD 6)`)
1968 THEN RESA_TAC
1969 THEN MP_TAC(SET_RULE`{4,5} = {i' MOD 6, j MOD 6}
1970 ==> (4=i' MOD 6 /\ 5=j MOD 6)\/ (5=i' MOD 6 /\  4=j MOD 6)`)
1971 THEN RESA_TAC
1972 THEN MP_TAC(SET_RULE`{5,0} = {i' MOD 6, j MOD 6}
1973 ==> (5=i' MOD 6 /\ 0=j MOD 6)\/ (0=i' MOD 6 /\  5=j MOD 6)`)
1974 THEN RESA_TAC
1975 THEN MP_TAC(SET_RULE`{0,1} = {i' MOD 6, j MOD 6}
1976 ==> (i' MOD 6=1 /\ j MOD 6=0)\/ (i' MOD 6=0 /\ j MOD 6=1)`)
1977 THEN RESA_TAC;
1978 REPEAT STRIP_TAC
1979 THEN REPLICATE_TAC 12 (POP_ASSUM MP_TAC)
1980 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
1981 THEN MATCH_MP_TAC th)
1982 THEN ASM_REWRITE_TAC[]];;
1983
1984
1985
1986
1987
1988
1989
1990
1991
1992
1993 let EXISTS_SCS_J_TAC=
1994 fun (so:term) (so1:term) (so2:term)->
1995 EXPAND_TAC "h"
1996 THEN REWRITE_TAC[ARITH_RULE`0 MOD 6=0/\SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`]
1997 THEN STRIP_TAC
1998 THEN EXISTS_TAC so
1999 THEN ASM_REWRITE_TAC[ARITH_RULE`6 MOD 6=0/\ SUC 0=1/\ 1<=6/\ 6<=6/\ 1+0=1/\ 1 MOD 6=1/\ 1<=1/\ 1<=6/\ 1 MOD 6=1/\ 1+1=2/\ ~(1=0)/\ 2 MOD 6=2/\ SUC 2=3/\ ~(2=0)/\ 1<=2/\ 2<=6/\ 1+2=3/\ 3 MOD 6=3/\ 1<=3/\ 3<=6/\ 1+3=4/\ SUC 3=4/\ ~(3=0)/\ ~(4=0)/\ 1<=4/\ 4<=6/\ SUC 4=5/\ 4 MOD 6=4/\ 1+4=5
2000 /\ ~(5=0)/\ 1<=5/\ 5<=6/\ SUC 5=6/\ 5 MOD 6=5/\ 1+5=6`]
2001 THEN EXISTS_TAC so1
2002 THEN EXISTS_TAC so2
2003 THEN ASM_REWRITE_TAC[ARITH_RULE`0 MOD 6=0/\ 1 MOD 6=1/\ 2 MOD 6=2/\ 3 MOD 6=3/\ 6 MOD 6=0/\ 4 MOD 6=4/\ 5 MOD 6=5`]
2004 ;;
2005
2006
2007
2008
2009
2010
2011
2012
2013
2014
2015
2016 let TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6=prove_by_refinement(
2017 `is_scs_v39 s /\ scs_k_v39 s=6
2018 /\ vv IN BBs_v39 s
2019 /\  dimindex(:M)=scs_k_v39 s
2020 /\ vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 5;(vv:num->real^3) 0]:real^3^M= v
2021 /\ matvec (v:real^3^M) =a
2022 /\ stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
2023          (change_type_v3 (scs_a_v39 s)),
2024          (change_type_v3 (scs_b_v39 s)),
2025          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
2026          (\i. (1 + i) MOD scs_k_v39 s))=s1
2027 ==>  taustar_v39 s vv = tau_star s1 a`,
2028   (* {{{ proof *)
2029 [
2030 REPEAT STRIP_TAC
2031 THEN POP_ASSUM MP_TAC
2032 THEN MP_TAC V_E_FF_IS_SCS_CASES_6
2033 THEN ASM_REWRITE_TAC[IN]
2034 THEN STRIP_TAC
2035 THEN STRIP_TAC
2036 THEN MP_TAC IS_SCS_STABLE_SYSTEM
2037 THEN ASM_REWRITE_TAC[ARITH_RULE`3<6`]
2038 THEN STRIP_TAC
2039 THEN ASM_REWRITE_TAC[taustar_v39;tau_star]
2040 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`;IN;mk_unadorned_v39;]
2041 THEN ASM_SIMP_TAC[dsv_J_empty]
2042 THEN EXPAND_TAC"a"
2043 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
2044 THEN ASM_REWRITE_TAC[REAL_ARITH`A-B=A-C<=>B=C`;dsv_v39;d_fun]
2045 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
2046          (change_type_v3 (scs_a_v39 s))`;`
2047          (change_type_v3 (scs_b_v39 s))`;`
2048          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
2049          (\i. (1 + i) MOD scs_k_v39 s)`]
2050 THEN ASM_REWRITE_TAC[REAL_ARITH`A+B=A+C<=>B=C`;sigma_sy]
2051 THEN MP_TAC IS_EAR_V25_EQ_EAR_SY
2052 THEN ASM_REWRITE_TAC[ARITH_RULE`3<6`]
2053 THEN STRIP_TAC
2054 THEN ASM_REWRITE_TAC[REAL_EQ_MUL_LCANCEL;REAL_ARITH`~(#0.1 = &0)`]
2055 THEN SUBGOAL_THEN`~((if ear_sy s1 then &1 else -- &1) = &0)` ASSUME_TAC;
2056
2057 MP_TAC(SET_RULE`(ear_sy s1)\/ ~(ear_sy s1)`)
2058 THEN RESA_TAC
2059 THEN REAL_ARITH_TAC;
2060
2061 ASM_REWRITE_TAC[J1_SY ]
2062 THEN MATCH_MP_TAC SUM_EQ_GENERAL
2063 THEN ASM_REWRITE_TAC[IN_ELIM_THM]
2064 THEN ABBREV_TAC`h =(\i. if (i MOD 6 = 0) then (6,1)
2065 else (i MOD 6, SUC(i MOD 6)))`
2066 THEN SUBGOAL_THEN`(!x x'.
2067       (x < 6 /\ scs_J_v39 s x (SUC x))  /\
2068       (x' < 6 /\ scs_J_v39 s x' (SUC x')) /\
2069       h x' = (h:num->num #num) x
2070       ==> x = x')` ASSUME_TAC;
2071
2072 REPEAT STRIP_TAC
2073 THEN POP_ASSUM MP_TAC
2074 THEN MP_TAC(ARITH_RULE` x< 6 ==> x=0\/ x=1\/ x=2 \/ x=3\/ x=4\/ x=5 `)
2075 THEN RESA_TAC
2076 THEN MP_TAC(ARITH_RULE` x'< 6 ==> x'=0\/ x'=1\/ x'=2 \/ x'=3  \/ x'=4\/ x'=5`)
2077 THEN RESA_TAC
2078 THEN EXPAND_TAC"h"
2079 THEN REWRITE_TAC[ARITH_RULE`1 MOD 6=1 /\ 0 MOD 6=0/\ 2 MOD 6=2/\ 3 MOD 6=3 /\ 4 MOD 6=4/\ ~(1=0)/\ ~(2=0)/\ ~(3=0)/\ ~(4=0)/\ SUC 1=2/\ ~(1=6)/\ ~(2=6)/\ ~(3=6)/\ ~(4=6)/\ ~(5=0)/\ 5 MOD 6=5 /\ SUC 5=6`;ARITH_RULE`A=B <=> B=A:num`;PAIR_EQ;DE_MORGAN_THM]
2080 THEN RESA_TAC;
2081
2082 EXISTS_TAC`h:num->(num#num)`
2083 THEN ASM_REWRITE_TAC[change_type_v2;IN_ELIM_THM;IN_NUMSEG]
2084 THEN STRIP_TAC
2085 THEN REPEAT STRIP_TAC;
2086
2087 ASM_REWRITE_TAC[EXISTS_UNIQUE_THM]
2088 THEN MP_TAC(ARITH_RULE`1<= i/\ i<=6 ==> i=1\/ i=2 \/ i=3 \/ i=4 \/i=5 \/ i=6`)
2089 THEN RESA_TAC
2090 THENL[
2091 INJ_H_FUN_TAC `1`;
2092 INJ_H_FUN_TAC `2`;
2093 INJ_H_FUN_TAC `3`;
2094 INJ_H_FUN_TAC `4`;
2095 INJ_H_FUN_TAC `5`;
2096 INJ_H_FUN_TAC `0`];
2097
2098 POP_ASSUM MP_TAC
2099 THEN MP_TAC(ARITH_RULE`x<6 ==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4\/ x=5`)
2100 THEN RESA_TAC
2101 THENL[
2102 EXISTS_SCS_J_TAC `6` `0` `1`;
2103 EXISTS_SCS_J_TAC `1` `1` `2`;
2104 EXISTS_SCS_J_TAC `2` `2` `3`;
2105 EXISTS_SCS_J_TAC `3` `3` `4`;
2106 EXISTS_SCS_J_TAC `4` `4` `5`;
2107 EXISTS_SCS_J_TAC `5` `5` `6`];
2108
2109 POP_ASSUM MP_TAC
2110 THEN MP_TAC(ARITH_RULE`x<6 ==> x=0 \/ x=1 \/ x=2 \/ x=3\/ x=4\/ x=5`)
2111 THEN RESA_TAC
2112 THEN EXPAND_TAC"h"
2113 THEN REWRITE_TAC[ARITH_RULE`0 MOD 6=0/\ SUC 0=1`]
2114 THEN EXPAND_TAC"a"
2115 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
2116 THEN MRESAL_TAC VECTOR_3_6[`(vv:num->real^3) 1`;`(vv:num->real^3) 2`;`(vv:num->real^3) 3`;`(vv:num->real^3) 4`;`(vv:num->real^3) 5`;`(vv:num->real^3) 0`][ARITH_RULE`1<=6/\ 2<=6/\ 3<=6/\ 4<=6/\ 5<=6 /\ 6<=6 /\ 0 MOD 6= 0 /\ 1 MOD 6= 1 /\ 2 MOD 6= 2/\ 3 MOD 6= 3 /\ 4 MOD 6= 4 /\ 5 MOD 6=5 /\ 6 MOD 6=0 /\ ~(2=1)/\ ~(2=0)/\ ~(3=0)/\ ~(4=0)/\ ~(5=0)
2117 /\ SUC 0 MOD 6= 1 /\ SUC 1 MOD 6= 2 /\ SUC 2 MOD 6= 3/\ SUC 3 MOD 6= 4
2118 /\ SUC 4 MOD 6= 5 /\ SUC 5 MOD 6 = 0 /\ SUC 6 MOD 6 =1 /\ ~(3=1)/\ ~(1=0)
2119 /\ 1<=1 /\1<=2/\ 1<=3/\ 1<=4/\1<=5
2120 /\ SUC 0=1/\ SUC 1=2/\ SUC 2=3/\ SUC 3=4/\ SUC 4=5/\ SUC 5=6`; SET_RULE`(a:num) IN (:num)`;dist]
2121 THEN REPLICATE_TAC 27 (POP_ASSUM MP_TAC)
2122 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2123 THEN MP_TAC th)
2124 THEN ASM_REWRITE_TAC[IN;BBs_v39;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`]
2125 THEN REPEAT STRIP_TAC
2126 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(6=0)`]
2127 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`6`[ARITH_RULE`6 MOD 6=0`])]);;
2128
2129
2130
2131
2132 let JKQEWGV1_CASE_6=prove(
2133 `!s vv. is_scs_v39 s /\ scs_k_v39 s=6 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
2134 /\ dimindex(:M)=scs_k_v39 s
2135  ==>
2136   (sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
2137    (IMAGE (\i. (vv i,vv (SUC i))) (:num))  < pi)`,
2138 REPEAT GEN_TAC
2139 THEN STRIP_TAC
2140 THEN MP_TAC IS_SCS_STABLE_SYSTEM
2141 THEN RESA_TAC
2142 THEN POP_ASSUM MP_TAC
2143 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<6`]
2144 THEN STRIP_TAC
2145 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
2146          (change_type_v3 (scs_a_v39 s)),
2147          (change_type_v3 (scs_b_v39 s)),
2148          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
2149          (\i. (1 + i) MOD scs_k_v39 s))`
2150 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
2151          (change_type_v3 (scs_a_v39 s))`;`
2152          (change_type_v3 (scs_b_v39 s))`;`
2153          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
2154          (\i. (1 + i) MOD scs_k_v39 s)`]
2155 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 5;(vv:num->real^3) 0]:real^3^M`
2156 THEN ABBREV_TAC`a=matvec (v:real^3^M)`
2157 THEN MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6
2158 THEN RESA_TAC
2159 THEN POP_ASSUM MP_TAC
2160 THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
2161 THEN STRIP_TAC
2162 THEN MP_TAC IN_IS_SCS_CASE_6
2163 THEN RESA_TAC
2164 THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<6`;]
2165 THEN REMOVE_ASSUM_TAC
2166 THEN POP_ASSUM MP_TAC
2167 THEN EXPAND_TAC"a"
2168 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
2169 THEN MP_TAC V_E_FF_IS_SCS_CASES_6
2170 THEN ASM_REWRITE_TAC[IN]
2171 THEN RESA_TAC
2172 THEN ASM_TAC
2173 THEN ASM_REWRITE_TAC[is_scs_v39;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`;IN;mk_unadorned_v39]
2174 THEN REPEAT RESA_TAC
2175 THEN POP_ASSUM MP_TAC
2176 THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
2177 THEN RESA_TAC
2178 THEN MP_TAC(REAL_ARITH`pi <=
2179   sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
2180   (IMAGE (\i. vv i,vv (SUC i)) (:num)) \/
2181   sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
2182   (IMAGE (\i. vv i,vv (SUC i)) (:num))< pi`)
2183 THEN RESA_TAC
2184 THEN REPLICATE_TAC 19 REMOVE_ASSUM_TAC
2185 THEN POP_ASSUM MP_TAC
2186 THEN REAL_ARITH_TAC);;
2187
2188
2189
2190
2191 let IN_IMAGE_VV_EQ_3 =
2192 fun (th:term)->
2193  MRESAL_TAC(GEN_ALL IMP_SUC_MOD_EQ)[`x':num`;th;`3`][ARITH_RULE`~(3=0)/\ 0 MOD 3=0/\ SUC 0  MOD 3=1/\ 1 MOD 3=1/\ SUC 1=2 /\ 2 MOD 3=2 /\ 3 MOD 3=0/\ SUC 2=3`]
2194 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`]
2195 THEN POP_ASSUM(fun th-> MRESA1_TAC th`x':num` THEN MRESA1_TAC th`SUC x'`)
2196 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
2197 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;SET_RULE`A IN {A,B,C} /\ B IN {A,B,C}/\ C IN {A,B,C}  `])
2198 ;;
2199
2200
2201
2202
2203 let V_E_FF_IS_SCS_CASES_3=prove_by_refinement(
2204 ` scs_k_v39 s=3/\ is_scs_v39 s  /\ BBs_v39 s vv
2205 /\ dimindex(:M)=scs_k_v39 s
2206  ==>
2207   ((IMAGE (\i. {vv i, vv (SUC i)}) (:num) ={{vv 0,vv 1},{vv 1, vv 2},{vv 2, vv 0}})
2208 /\   (IMAGE (\i. (vv i,vv (SUC i))) (:num)= {(vv 0,vv 1),(vv 1, vv 2),(vv 2, vv 0)})  )`,
2209   (* {{{ proof *)
2210 [
2211 STRIP_TAC
2212 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
2213 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;IN;mk_unadorned_v39]
2214 THEN RESA_TAC
2215 THEN REWRITE_TAC[ARITH_RULE`3<=3`]
2216 THEN REPEAT STRIP_TAC;
2217
2218
2219
2220
2221 ONCE_REWRITE_TAC[EXTENSION]
2222 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;]
2223 THEN GEN_TAC
2224 THEN EQ_TAC;
2225
2226 RESA_TAC
2227 THEN MRESAL_TAC DIVISION[`x':num`;`3`][ARITH_RULE`~(3=0)`]
2228 THEN MP_TAC(ARITH_RULE`x' MOD 3 < 3==> x' MOD 3 =0 \/ x' MOD 3 =1\/ x' MOD 3 =2`)
2229 THEN RESA_TAC
2230 THENL[
2231 IN_IMAGE_VV_EQ_3 `0`;
2232 IN_IMAGE_VV_EQ_3 `1`;
2233 IN_IMAGE_VV_EQ_3 `2`];
2234
2235
2236 REWRITE_TAC[SET_RULE`X IN {A,B,C}<=> X=A \/ X=B\/ X=C`]
2237 THEN RESA_TAC;
2238
2239 EXISTS_TAC`0`
2240 THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 0=1`];
2241
2242 EXISTS_TAC`1`
2243 THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 1=2`];
2244
2245 EXISTS_TAC`2`
2246 THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 2=3`]
2247 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`]
2248 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`])
2249 ;
2250
2251
2252 ONCE_REWRITE_TAC[EXTENSION]
2253 THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;]
2254 THEN GEN_TAC
2255 THEN EQ_TAC;
2256
2257 RESA_TAC
2258 THEN MRESAL_TAC DIVISION[`x':num`;`3`][ARITH_RULE`~(3=0)`]
2259 THEN MP_TAC(ARITH_RULE`x' MOD 3 < 3==> x' MOD 3 =0 \/ x' MOD 3 =1\/ x' MOD 3 =2`)
2260 THEN RESA_TAC
2261 THENL[
2262 IN_IMAGE_VV_EQ_3 `0`;
2263 IN_IMAGE_VV_EQ_3 `1`;
2264 IN_IMAGE_VV_EQ_3 `2`];
2265
2266
2267 REWRITE_TAC[SET_RULE`X IN {A,B,C}<=> X=A \/ X=B\/ X=C`]
2268 THEN RESA_TAC
2269 ;
2270
2271 EXISTS_TAC`0`
2272 THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 0=1`];
2273
2274 EXISTS_TAC`1`
2275 THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 1=2`];
2276
2277 EXISTS_TAC`2`
2278 THEN REWRITE_TAC[SET_RULE`(a:num)IN (:num)`;ARITH_RULE`SUC 2=3`]
2279 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_RULE`~(3=0)`]
2280 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`]);
2281 ]);;
2282
2283
2284
2285 let IS_SCS_POINT_IN_BBS_IS_NOT_0_3=prove_by_refinement(
2286 `scs_k_v39 s=3/\ is_scs_v39 s
2287 /\ vv IN BBs_v39 s
2288 ==> ~(vv 1= vec 0)/\  ~(vv 2= vec 0) /\ ~(vv 0= vec 0)`,
2289   (* {{{ proof *)
2290 [
2291 REWRITE_TAC[IN]
2292 THEN STRIP_TAC
2293 THEN POP_ASSUM MP_TAC
2294 THEN POP_ASSUM MP_TAC
2295 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;IMAGE;SUBSET;IN_ELIM_THM;is_scs_v39]
2296 THEN STRIP_TAC
2297 THEN STRIP_TAC
2298 THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv 0 = (vv:num->real^3) x)`ASSUME_TAC;
2299 EXISTS_TAC`0`
2300 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2301 SUBGOAL_THEN`(?x. x IN (:num) /\ vv 1 = (vv:num->real^3) x)`ASSUME_TAC;
2302 EXISTS_TAC`1`
2303 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2304 SUBGOAL_THEN`(?x. x IN (:num) /\ vv 2 = (vv:num->real^3) x)`ASSUME_TAC;
2305 EXISTS_TAC`2`
2306 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2307 REPLICATE_TAC 5(POP_ASSUM MP_TAC)
2308 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2309 THEN MRESAL1_TAC th`(vv:num->real^3) 0`[ball_annulus;IN_ELIM_THM;DIFF;ball]
2310 THEN MRESAL1_TAC th`(vv:num->real^3) 1`[ball_annulus;IN_ELIM_THM;DIFF;ball]
2311 THEN MRESAL1_TAC th`(vv:num->real^3) 2`[ball_annulus;IN_ELIM_THM;DIFF;ball;])
2312 THEN STRIP_TAC;
2313 STRIP_TAC
2314 THEN POP_ASSUM(fun th-> ASM_TAC
2315 THEN REWRITE_TAC[th;DIST_REFL;REAL_ARITH`(&0< &2)`]);
2316 STRIP_TAC;
2317 STRIP_TAC
2318 THEN POP_ASSUM(fun th-> ASM_TAC
2319 THEN REWRITE_TAC[th;DIST_REFL;REAL_ARITH`(&0< &2)`]);
2320 STRIP_TAC
2321 THEN POP_ASSUM(fun th-> ASM_TAC
2322 THEN REWRITE_TAC[th;DIST_REFL;REAL_ARITH`(&0< &2)`])
2323 ]);;
2324   (* }}} *)
2325
2326
2327
2328 let IS_SCS_NOT_COLLINEAR_BBs_CASE_3=prove_by_refinement(
2329 `scs_k_v39 s=3/\ is_scs_v39 s
2330 /\ vv IN BBs_v39 s
2331 ==> ~collinear{vec 0, vv 1 ,vv 2}/\
2332  ~collinear{vec 0, vv 1 ,vv 0}/\
2333  ~collinear{vec 0, vv 2 ,vv 0}`,
2334   (* {{{ proof *)
2335 [
2336
2337
2338 REWRITE_TAC[Local_lemmas.collinear_fan22;aff;AFFINE_HULL_2;IN_ELIM_THM;VECTOR_ARITH`A % vec 0+B=B`]
2339 THEN STRIP_TAC
2340 THEN MP_TAC IS_SCS_POINT_IN_BBS_IS_NOT_0_3
2341 THEN RESA_TAC
2342 THEN ASM_TAC
2343 THEN REWRITE_TAC[IN]
2344 THEN STRIP_TAC
2345 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;is_scs_v39]
2346 THEN POP_ASSUM(fun th->
2347 STRIP_TAC
2348 THEN ASSUME_TAC th)
2349 THEN REPEAT STRIP_TAC;
2350
2351 REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
2352 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2353 THEN MRESAL_TAC th[`1`;`2`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
2354 ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0/\ 1<3/\ 2<3`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
2355 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
2356 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2357 THEN MRESAL_TAC th[`1`;`2`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
2358 ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
2359 THEN REPLICATE_TAC 9(POP_ASSUM MP_TAC)
2360 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2361 THEN MP_TAC th)
2362 THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv 1 = (vv:num->real^3) x)`ASSUME_TAC;
2363
2364
2365 EXISTS_TAC`1`
2366 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2367
2368 SUBGOAL_THEN`(?x. x IN (:num) /\ vv 2 = (vv:num->real^3) x)`ASSUME_TAC;
2369
2370
2371 EXISTS_TAC`2`
2372 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2373
2374
2375 REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
2376 THEN STRIP_TAC
2377 THEN POP_ASSUM(fun th->  MRESAL1_TAC th`(vv:num->real^3) 2`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`]
2378 THEN MRESAL1_TAC th`(vv:num->real^3) 1`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`])
2379 THEN MP_TAC(REAL_ARITH`&0<= &1-v\/ &0<= --( &1-v)`)
2380 THEN STRIP_TAC
2381 ;
2382
2383
2384  MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
2385 THEN STRIP_TAC
2386 ;
2387
2388
2389 MRESA1_TAC Trigonometry2.ABS_REFL `v:real`
2390 THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
2391 THEN POP_ASSUM(fun th-> ASM_TAC
2392 THEN REWRITE_TAC[th]
2393 THEN REPEAT STRIP_TAC)
2394 THEN POP_ASSUM(fun th-> ASM_TAC
2395 THEN REWRITE_TAC[th]
2396 THEN REPEAT STRIP_TAC)
2397 THEN MP_TAC(REAL_ARITH`&2 <=scs_a_v39 s 2 1/\ scs_a_v39 s 2 1<= (&1 - v) * norm (vv 1)
2398 /\ &2 <= v * norm (vv 1) ==> &4<= norm ((vv:num->real^3) 1)`)
2399 THEN REPLICATE_TAC 4(POP_ASSUM MP_TAC)
2400 THEN ASM_REWRITE_TAC[h0]
2401 THEN REAL_ARITH_TAC
2402 ;
2403
2404
2405
2406
2407 MRESAL1_TAC Trigonometry2.ABS_REFL `-- v:real`[REAL_ABS_NEG]
2408 THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
2409 THEN POP_ASSUM(fun th-> ASM_TAC
2410 THEN REWRITE_TAC[th]
2411 THEN REPEAT STRIP_TAC)
2412 THEN POP_ASSUM(fun th-> ASM_TAC
2413 THEN REWRITE_TAC[th; ]
2414 THEN REPEAT STRIP_TAC)
2415 THEN MP_TAC(REAL_ARITH`&2 <= --v * norm (vv 1)
2416 /\ &2 <= norm (vv 1) ==> &4<=(&1- v) *norm ((vv:num->real^3) 1)`)
2417 THEN ASM_REWRITE_TAC[]
2418 THEN REPLICATE_TAC 8(POP_ASSUM MP_TAC)
2419 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2420 THEN POP_ASSUM MP_TAC
2421 THEN REWRITE_TAC[SYM th])
2422 THEN REPLICATE_TAC 23(POP_ASSUM MP_TAC)
2423 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2424 THEN MRESAL1_TAC th`1`[ARITH_RULE`SUC 1=2`])
2425 THEN POP_ASSUM MP_TAC
2426 THEN POP_ASSUM MP_TAC
2427 THEN REPLICATE_TAC 9(REMOVE_ASSUM_TAC)
2428 THEN POP_ASSUM MP_TAC
2429 THEN REAL_ARITH_TAC;
2430
2431
2432
2433
2434  MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
2435 THEN STRIP_TAC
2436 ;
2437
2438
2439
2440
2441
2442
2443
2444 MRESAL1_TAC Trigonometry2.ABS_REFL ` v:real`[REAL_ABS_NEG]
2445 THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
2446 THEN POP_ASSUM(fun th-> ASM_TAC
2447 THEN REWRITE_TAC[th]
2448 THEN REPEAT STRIP_TAC)
2449 THEN POP_ASSUM(fun th-> ASM_TAC
2450 THEN REWRITE_TAC[th; ]
2451 THEN REPEAT STRIP_TAC)
2452 THEN MP_TAC(REAL_ARITH`&2 <=   norm (vv 1)
2453 /\ &2 <= scs_a_v39 s 2 1/\ scs_a_v39 s 2 1<= --(&1 - v) * norm (vv 1) ==> &4<= v *norm ((vv:num->real^3) 1)`)
2454 THEN ASM_REWRITE_TAC[]
2455 THEN REPLICATE_TAC 5(POP_ASSUM MP_TAC)
2456 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2457 THEN MP_TAC th)
2458 THEN POP_ASSUM MP_TAC
2459 THEN ASM_REWRITE_TAC[h0]
2460 THEN REAL_ARITH_TAC
2461 ;
2462
2463
2464 MRESAL1_TAC Trigonometry2.ABS_REFL ` --v:real`[REAL_ABS_NEG]
2465 THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
2466 THEN POP_ASSUM(fun th-> ASM_TAC
2467 THEN REWRITE_TAC[th]
2468 THEN REPEAT STRIP_TAC)
2469 THEN POP_ASSUM(fun th-> ASM_TAC
2470 THEN REWRITE_TAC[th; ]
2471 THEN REPEAT STRIP_TAC)
2472 THEN MP_TAC(REAL_ARITH`&2 <=   norm (vv 1)
2473 /\ &2 <= --v * norm (vv 1) ==> &4<= (&1-v) *norm ((vv:num->real^3) 1)`)
2474 THEN ASM_REWRITE_TAC[REAL_ARITH`~(a<= b) <=> b<a`]
2475 THEN REPLICATE_TAC 12(POP_ASSUM MP_TAC)
2476 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2477 THEN MP_TAC th)
2478 THEN REPLICATE_TAC 11(POP_ASSUM MP_TAC)
2479 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2480 THEN MP_TAC th)
2481 THEN POP_ASSUM MP_TAC
2482 THEN ASM_REWRITE_TAC[]
2483 THEN REAL_ARITH_TAC;
2484
2485
2486
2487
2488
2489 REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
2490 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2491 THEN MRESAL_TAC th[`0`;`1`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
2492 ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0/\ 1<3/\ 2<3/\ 0<3 /\ ~(0=1)`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
2493 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
2494 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2495 THEN MRESAL_TAC th[`0`;`1`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
2496 ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0`;dist;VECTOR_ARITH`B%A - A= --((&1-B)%A)`;NORM_MUL;NORM_NEG])
2497 THEN REPLICATE_TAC 9(POP_ASSUM MP_TAC)
2498 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2499 THEN MP_TAC th)
2500 THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv 1 = (vv:num->real^3) x)`ASSUME_TAC;
2501
2502
2503 EXISTS_TAC`1`
2504 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2505
2506 SUBGOAL_THEN`(?x. x IN (:num) /\ vv 0 = (vv:num->real^3) x)`ASSUME_TAC;
2507
2508
2509 EXISTS_TAC`0`
2510 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2511
2512
2513 REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
2514 THEN STRIP_TAC
2515 THEN POP_ASSUM(fun th->  MRESAL1_TAC th`(vv:num->real^3) 0`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`]
2516 THEN MRESAL1_TAC th`(vv:num->real^3) 1`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`])
2517 THEN MP_TAC(REAL_ARITH`&0<= &1-v\/ &0<= --( &1-v)`)
2518 THEN STRIP_TAC
2519 ;
2520
2521
2522  MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
2523 THEN STRIP_TAC
2524 ;
2525
2526
2527 MRESA1_TAC Trigonometry2.ABS_REFL `v:real`
2528 THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
2529 THEN POP_ASSUM(fun th-> ASM_TAC
2530 THEN REWRITE_TAC[th]
2531 THEN REPEAT STRIP_TAC)
2532 THEN POP_ASSUM(fun th-> ASM_TAC
2533 THEN REWRITE_TAC[th]
2534 THEN REPEAT STRIP_TAC)
2535 THEN MP_TAC(REAL_ARITH`&2 <=scs_a_v39 s 1 0/\ scs_a_v39 s 1 0<= (&1 - v) * norm (vv 1)
2536 /\ &2 <= v * norm (vv 1) ==> &4<= norm ((vv:num->real^3) 1)`)
2537 THEN REPLICATE_TAC 4(POP_ASSUM MP_TAC)
2538 THEN ASM_REWRITE_TAC[h0]
2539 THEN REAL_ARITH_TAC;
2540
2541 MRESAL1_TAC Trigonometry2.ABS_REFL `-- v:real`[REAL_ABS_NEG]
2542 THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
2543 THEN POP_ASSUM(fun th-> ASM_TAC
2544 THEN REWRITE_TAC[th]
2545 THEN REPEAT STRIP_TAC)
2546 THEN POP_ASSUM(fun th-> ASM_TAC
2547 THEN REWRITE_TAC[th; ]
2548 THEN REPEAT STRIP_TAC)
2549 THEN MP_TAC(REAL_ARITH`&2 <= --v * norm (vv 1)
2550 /\ &2 <= norm (vv 1) ==> &4<=(&1- v) *norm ((vv:num->real^3) 1)`)
2551 THEN ASM_REWRITE_TAC[]
2552 THEN REPLICATE_TAC 8(POP_ASSUM MP_TAC)
2553 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2554 THEN POP_ASSUM MP_TAC
2555 THEN REWRITE_TAC[SYM th])
2556 THEN REPLICATE_TAC 23(POP_ASSUM MP_TAC)
2557 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2558 THEN MRESAL1_TAC th`0`[ARITH_RULE`SUC 0=1`])
2559 THEN POP_ASSUM MP_TAC
2560 THEN POP_ASSUM MP_TAC
2561 THEN REPLICATE_TAC 9(REMOVE_ASSUM_TAC)
2562 THEN POP_ASSUM MP_TAC
2563 THEN REAL_ARITH_TAC;
2564
2565  MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
2566 THEN STRIP_TAC;
2567
2568
2569 MRESAL1_TAC Trigonometry2.ABS_REFL ` v:real`[REAL_ABS_NEG]
2570 THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
2571 THEN POP_ASSUM(fun th-> ASM_TAC
2572 THEN REWRITE_TAC[th]
2573 THEN REPEAT STRIP_TAC)
2574 THEN POP_ASSUM(fun th-> ASM_TAC
2575 THEN REWRITE_TAC[th; ]
2576 THEN REPEAT STRIP_TAC)
2577 THEN MP_TAC(REAL_ARITH`&2 <=   norm (vv 1)
2578 /\ &2 <= scs_a_v39 s 1 0/\ scs_a_v39 s 1 0<= --(&1 - v) * norm (vv 1) ==> &4<= v *norm ((vv:num->real^3) 1)`)
2579 THEN ASM_REWRITE_TAC[]
2580 THEN REPLICATE_TAC 5(POP_ASSUM MP_TAC)
2581 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2582 THEN MP_TAC th)
2583 THEN POP_ASSUM MP_TAC
2584 THEN ASM_REWRITE_TAC[h0]
2585 THEN REAL_ARITH_TAC
2586 ;
2587
2588
2589 MRESAL1_TAC Trigonometry2.ABS_REFL ` --v:real`[REAL_ABS_NEG]
2590 THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
2591 THEN POP_ASSUM(fun th-> ASM_TAC
2592 THEN REWRITE_TAC[th]
2593 THEN REPEAT STRIP_TAC)
2594 THEN POP_ASSUM(fun th-> ASM_TAC
2595 THEN REWRITE_TAC[th; ]
2596 THEN REPEAT STRIP_TAC)
2597 THEN MP_TAC(REAL_ARITH`&2 <=   norm (vv 1)
2598 /\ &2 <= --v * norm (vv 1) ==> &4<= (&1-v) *norm ((vv:num->real^3) 1)`)
2599 THEN ASM_REWRITE_TAC[REAL_ARITH`~(a<= b) <=> b<a`]
2600 THEN REPLICATE_TAC 12(POP_ASSUM MP_TAC)
2601 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2602 THEN MP_TAC th)
2603 THEN REPLICATE_TAC 11(POP_ASSUM MP_TAC)
2604 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2605 THEN MP_TAC th)
2606 THEN POP_ASSUM MP_TAC
2607 THEN ASM_REWRITE_TAC[]
2608 THEN REAL_ARITH_TAC;
2609
2610
2611
2612 REPLICATE_TAC 14 (POP_ASSUM MP_TAC)
2613 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2614 THEN MRESAL_TAC th[`0`;`2`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
2615 ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0/\ 1<3/\ 2<3/\ 0<3 /\ ~(0=1)/\ ~(0=2)`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
2616 THEN REPLICATE_TAC 6 (POP_ASSUM MP_TAC)
2617 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2618 THEN MRESAL_TAC th[`0`;`2`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
2619 ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0`;dist;VECTOR_ARITH`B%A - A= --((&1-B)%A)`;NORM_MUL;NORM_NEG])
2620 THEN REPLICATE_TAC 9(POP_ASSUM MP_TAC)
2621 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2622 THEN MP_TAC th)
2623 THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv 2 = (vv:num->real^3) x)`ASSUME_TAC;
2624
2625
2626 EXISTS_TAC`2`
2627 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2628
2629 SUBGOAL_THEN`(?x. x IN (:num) /\ vv 0 = (vv:num->real^3) x)`ASSUME_TAC;
2630
2631
2632 EXISTS_TAC`0`
2633 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2634
2635
2636 REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
2637 THEN STRIP_TAC
2638 THEN POP_ASSUM(fun th->  MRESAL1_TAC th`(vv:num->real^3) 0`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`]
2639 THEN MRESAL1_TAC th`(vv:num->real^3) 2`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`])
2640 THEN MP_TAC(REAL_ARITH`&0<= &1-v\/ &0<= --( &1-v)`)
2641 THEN STRIP_TAC
2642 ;
2643
2644
2645  MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
2646 THEN STRIP_TAC
2647 ;
2648
2649
2650 MRESA1_TAC Trigonometry2.ABS_REFL `v:real`
2651 THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
2652 THEN POP_ASSUM(fun th-> ASM_TAC
2653 THEN REWRITE_TAC[th]
2654 THEN REPEAT STRIP_TAC)
2655 THEN POP_ASSUM(fun th-> ASM_TAC
2656 THEN REWRITE_TAC[th]
2657 THEN REPEAT STRIP_TAC)
2658 THEN MP_TAC(REAL_ARITH`&2 <=scs_a_v39 s 2 0/\ scs_a_v39 s 2 0<= (&1 - v) * norm (vv 2)
2659 /\ &2 <= v * norm (vv 2) ==> &4<= norm ((vv:num->real^3) 2)`)
2660 THEN REPLICATE_TAC 4(POP_ASSUM MP_TAC)
2661 THEN ASM_REWRITE_TAC[h0]
2662 THEN REAL_ARITH_TAC
2663 ;
2664
2665
2666
2667
2668 MRESAL1_TAC Trigonometry2.ABS_REFL `-- v:real`[REAL_ABS_NEG]
2669 THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
2670 THEN POP_ASSUM(fun th-> ASM_TAC
2671 THEN REWRITE_TAC[th]
2672 THEN REPEAT STRIP_TAC)
2673 THEN POP_ASSUM(fun th-> ASM_TAC
2674 THEN REWRITE_TAC[th; ]
2675 THEN REPEAT STRIP_TAC)
2676 THEN MP_TAC(REAL_ARITH`&2 <= --v * norm (vv 2)
2677 /\ &2 <= norm (vv 2) ==> &4<=(&1- v) *norm ((vv:num->real^3) 2)`)
2678 THEN ASM_REWRITE_TAC[]
2679 THEN REPLICATE_TAC 8(POP_ASSUM MP_TAC)
2680 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2681 THEN POP_ASSUM MP_TAC
2682 THEN REWRITE_TAC[SYM th])
2683 THEN REPLICATE_TAC 23(POP_ASSUM MP_TAC)
2684 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2685 THEN MRESAL1_TAC th`2`[ARITH_RULE`SUC 2=3`])
2686 THEN POP_ASSUM MP_TAC
2687 THEN POP_ASSUM MP_TAC
2688 THEN REPLICATE_TAC 9(REMOVE_ASSUM_TAC)
2689 THEN ASM_TAC
2690 THEN REWRITE_TAC[periodic2]
2691 THEN REPEAT STRIP_TAC
2692 THEN POP_ASSUM MP_TAC
2693 THEN POP_ASSUM MP_TAC
2694 THEN POP_ASSUM MP_TAC
2695 THEN MRESAL_TAC (GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s 2`][ARITH_RULE`~(3=0)`;periodic]
2696 THEN POP_ASSUM(fun th-> MRESAL1_TAC th`3:num`[ARITH_RULE`3 MOD 3=0`])
2697 THEN REAL_ARITH_TAC;
2698
2699
2700
2701
2702  MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
2703 THEN STRIP_TAC
2704 ;
2705
2706
2707
2708
2709
2710
2711
2712 MRESAL1_TAC Trigonometry2.ABS_REFL ` v:real`[REAL_ABS_NEG]
2713 THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
2714 THEN POP_ASSUM(fun th-> ASM_TAC
2715 THEN REWRITE_TAC[th]
2716 THEN REPEAT STRIP_TAC)
2717 THEN POP_ASSUM(fun th-> ASM_TAC
2718 THEN REWRITE_TAC[th; ]
2719 THEN REPEAT STRIP_TAC)
2720 THEN MP_TAC(REAL_ARITH`&2 <=   norm (vv 2)
2721 /\ &2 <= scs_a_v39 s 2 0/\ scs_a_v39 s 2 0<= --(&1 - v) * norm (vv 2) ==> &4<= v *norm ((vv:num->real^3) 2)`)
2722 THEN ASM_REWRITE_TAC[]
2723 THEN REPLICATE_TAC 5(POP_ASSUM MP_TAC)
2724 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2725 THEN MP_TAC th)
2726 THEN POP_ASSUM MP_TAC
2727 THEN ASM_REWRITE_TAC[h0]
2728 THEN REAL_ARITH_TAC
2729 ;
2730
2731
2732 MRESAL1_TAC Trigonometry2.ABS_REFL ` --v:real`[REAL_ABS_NEG]
2733 THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
2734 THEN POP_ASSUM(fun th-> ASM_TAC
2735 THEN REWRITE_TAC[th]
2736 THEN REPEAT STRIP_TAC)
2737 THEN POP_ASSUM(fun th-> ASM_TAC
2738 THEN REWRITE_TAC[th; ]
2739 THEN REPEAT STRIP_TAC)
2740 THEN MP_TAC(REAL_ARITH`&2 <=   norm (vv 2)
2741 /\ &2 <= --v * norm (vv 2) ==> &4<= (&1-v) *norm ((vv:num->real^3) 2)`)
2742 THEN ASM_REWRITE_TAC[REAL_ARITH`~(a<= b) <=> b<a`]
2743 THEN REPLICATE_TAC 12(POP_ASSUM MP_TAC)
2744 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2745 THEN MP_TAC th)
2746 THEN REPLICATE_TAC 11(POP_ASSUM MP_TAC)
2747 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2748 THEN MP_TAC th)
2749 THEN POP_ASSUM MP_TAC
2750 THEN ASM_REWRITE_TAC[]
2751 THEN REAL_ARITH_TAC;
2752 ]);;
2753   (* }}} *)
2754
2755
2756
2757
2758 let IS_SCS_POINT_IN_BBS_IS_NOT_0_LE_3=prove_by_refinement(
2759 `3<scs_k_v39 s/\ is_scs_v39 s
2760 /\ vv IN BBs_v39 s
2761 ==> ~(vv i= vec 0)`,
2762 [REWRITE_TAC[IN]
2763 THEN STRIP_TAC
2764 THEN POP_ASSUM MP_TAC
2765 THEN POP_ASSUM MP_TAC
2766 THEN MP_TAC(ARITH_RULE`3<scs_k_v39 s==> ~(scs_k_v39 s<=3)`)
2767 THEN RESA_TAC
2768 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`~(4<=3)`;mk_unadorned_v39;CS_ADJ;IMAGE;SUBSET;IN_ELIM_THM;is_scs_v39]
2769 THEN STRIP_TAC
2770 THEN STRIP_TAC
2771 THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv i= (vv:num->real^3) x)`ASSUME_TAC;
2772 EXISTS_TAC`i:num`
2773 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2774 REPLICATE_TAC 4(POP_ASSUM MP_TAC)
2775 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
2776 THEN MRESAL1_TAC th`(vv:num->real^3) i`[ball_annulus;IN_ELIM_THM;DIFF;ball])
2777 THEN POP_ASSUM MP_TAC
2778 THEN REWRITE_TAC[DIST_REFL;REAL_ARITH`(&0< &2)`]
2779 ]);;
2780   (* }}} *)
2781
2782
2783
2784
2785 let IS_SCS_NOT_COLLINEAR_BBs_CASE_LE_3=prove_by_refinement(
2786 `3< scs_k_v39 s/\ is_scs_v39 s
2787 /\ vv IN BBs_v39 s
2788 /\ ~(i MOD (scs_k_v39 s)=j MOD (scs_k_v39 s))
2789 /\ dist(vv (i MOD (scs_k_v39 s)) ,vv (j MOD (scs_k_v39 s))) <= cstab
2790 ==> ~collinear{vec 0, vv (i MOD (scs_k_v39 s)) ,vv (j MOD (scs_k_v39 s))}`,
2791 [
2792 REWRITE_TAC[Local_lemmas.collinear_fan22;aff;AFFINE_HULL_2;IN_ELIM_THM;VECTOR_ARITH`A % vec 0+B=B`;cstab]
2793 THEN STRIP_TAC
2794 THEN MRESA_TAC( GEN_ALL IS_SCS_POINT_IN_BBS_IS_NOT_0_LE_3)[`s:scs_v39`;`vv:num->real^3`;`i MOD scs_k_v39 s`]
2795 THEN RESA_TAC
2796 THEN ASM_TAC
2797 THEN REWRITE_TAC[IN]
2798 THEN STRIP_TAC
2799 THEN ASM_REWRITE_TAC[scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;is_scs_v39]
2800 THEN POP_ASSUM(fun th->
2801 STRIP_TAC
2802 THEN ASSUME_TAC th)
2803 THEN REPEAT STRIP_TAC;
2804
2805 MP_TAC(ARITH_RULE`3 < scs_k_v39 s==> ~(scs_k_v39 s <= 3)`)
2806 THEN RESA_TAC;
2807
2808
2809 ABBREV_TAC`k=scs_k_v39 s`
2810 THEN POP_ASSUM MP_TAC
2811 THEN MP_TAC(ARITH_RULE`3<=k ==> ~(k=0)`)
2812 THEN RESA_TAC
2813 THEN STRIP_TAC
2814 THEN MRESA_TAC DIVISION[`i:num`;`k:num`]
2815 THEN MRESA_TAC DIVISION[`j:num`;`k:num`]
2816 THEN REPLICATE_TAC (35-14) (POP_ASSUM MP_TAC)
2817 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2818 THEN MRESAL_TAC th[`i MOD k`;`j MOD k`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
2819 ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0/\ 1<3/\ 2<3`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
2820 THEN REPLICATE_TAC (35-25)(POP_ASSUM MP_TAC)
2821 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2822 THEN MP_TAC th)
2823 THEN REPLICATE_TAC (34-22) (POP_ASSUM MP_TAC)
2824 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2825 THEN POP_ASSUM MP_TAC
2826 THEN MRESAL_TAC th[`i MOD k`;`j MOD k`][scs_k_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;LET_DEF;LET_END_DEF;BBs_v39;ARITH_RULE`3<=3`;mk_unadorned_v39;CS_ADJ;
2827 ARITH_RULE`1 MOD 3 =1 /\ 2 MOD 3=2/\ ~(1=2) /\ SUC 1=2 /\ SUC 2=3/\ 3 MOD 3=0`;dist;VECTOR_ARITH`A- B%A=(&1-B)%A`;NORM_MUL])
2828 THEN REPLICATE_TAC (35-20)(POP_ASSUM MP_TAC)
2829 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2830 THEN MP_TAC th)
2831 THEN SUBGOAL_THEN`(?x. x IN (:num) /\ vv (i MOD k) = (vv:num->real^3) x)`ASSUME_TAC;
2832
2833 EXISTS_TAC`i MOD k`
2834 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2835
2836 SUBGOAL_THEN`(?x. x IN (:num) /\ vv (j MOD k) = (vv:num->real^3) x)`ASSUME_TAC;
2837
2838 EXISTS_TAC`j MOD k`
2839 THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN (:num)`];
2840
2841 REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM]
2842 THEN STRIP_TAC
2843 THEN POP_ASSUM(fun th->  MRESAL1_TAC th`(vv:num->real^3) (i MOD k)`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`]
2844 THEN MRESAL1_TAC th`(vv:num->real^3) (j MOD k)`[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- B= --B`;NORM_NEG;NORM_MUL;REAL_ARITH`~(a<b) <=> b<=a`])
2845 THEN MP_TAC(REAL_ARITH`&0<= &1-v\/ &0<= --( &1-v)`)
2846 THEN STRIP_TAC;
2847
2848  MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
2849 THEN STRIP_TAC;
2850
2851 MRESA1_TAC Trigonometry2.ABS_REFL `v:real`
2852 THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
2853 THEN POP_ASSUM(fun th-> ASM_TAC
2854 THEN REWRITE_TAC[th]
2855 THEN REPEAT STRIP_TAC)
2856 THEN POP_ASSUM(fun th-> ASM_TAC
2857 THEN REWRITE_TAC[th]
2858 THEN REPEAT STRIP_TAC)
2859 THEN MP_TAC(REAL_ARITH`&2 <=scs_a_v39 s (i MOD k) (j MOD k)/\ scs_a_v39 s (i MOD k) (j MOD k)<= (&1 - v) * norm (vv (i MOD k))
2860 /\ &2 <= v * norm (vv (i MOD k)) ==> &4<= norm ((vv:num->real^3) (i MOD k))`)
2861 THEN REPLICATE_TAC 6(POP_ASSUM MP_TAC)
2862 THEN ASM_REWRITE_TAC[h0]
2863 THEN REAL_ARITH_TAC;
2864
2865
2866 MRESAL1_TAC Trigonometry2.ABS_REFL `-- v:real`[REAL_ABS_NEG]
2867 THEN MRESA1_TAC Trigonometry2.ABS_REFL `&1- v:real`
2868 THEN POP_ASSUM(fun th-> ASM_TAC
2869 THEN REWRITE_TAC[th]
2870 THEN REPEAT STRIP_TAC)
2871 THEN POP_ASSUM(fun th-> ASM_TAC
2872 THEN REWRITE_TAC[th; ]
2873 THEN REPEAT STRIP_TAC)
2874 THEN MP_TAC(REAL_ARITH`&2 <= --v * norm (vv (i MOD k))
2875 /\ &2 <= norm (vv (i MOD k)) ==> &4<=(&1- v) *norm ((vv:num->real^3) (i MOD k) )`)
2876 THEN ASM_REWRITE_TAC[]
2877 THEN REPLICATE_TAC (45-35)(POP_ASSUM MP_TAC)
2878 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2879 THEN POP_ASSUM MP_TAC
2880 THEN MP_TAC th
2881 THEN ASM_REWRITE_TAC[])
2882 THEN REAL_ARITH_TAC;
2883
2884 MP_TAC(REAL_ARITH`&0<= v\/ &0<= --( v)`)
2885 THEN STRIP_TAC;
2886
2887
2888 MRESAL1_TAC Trigonometry2.ABS_REFL ` v:real`[REAL_ABS_NEG]
2889 THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
2890 THEN POP_ASSUM(fun th-> ASM_TAC
2891 THEN REWRITE_TAC[th]
2892 THEN REPEAT STRIP_TAC)
2893 THEN POP_ASSUM(fun th-> ASM_TAC
2894 THEN REWRITE_TAC[th; ]
2895 THEN REPEAT STRIP_TAC)
2896 THEN MP_TAC(REAL_ARITH`&2 <=   norm (vv (i MOD k))
2897 /\ &2 <= scs_a_v39 s (i MOD k) (j MOD k)/\ scs_a_v39 s (i MOD k) (j MOD k)<= --(&1 - v) * norm (vv (i MOD k)) ==> &4<= v *norm ((vv:num->real^3) (i MOD k))`)
2898 THEN ASM_REWRITE_TAC[]
2899 THEN REPLICATE_TAC 3(POP_ASSUM MP_TAC)
2900 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2901 THEN MP_TAC th)
2902 THEN POP_ASSUM MP_TAC
2903 THEN ASM_REWRITE_TAC[h0]
2904 THEN REAL_ARITH_TAC;
2905
2906 MRESAL1_TAC Trigonometry2.ABS_REFL ` --v:real`[REAL_ABS_NEG]
2907 THEN MRESAL1_TAC Trigonometry2.ABS_REFL `--(&1- v):real` [REAL_ABS_NEG]
2908 THEN POP_ASSUM(fun th-> ASM_TAC
2909 THEN REWRITE_TAC[th]
2910 THEN REPEAT STRIP_TAC)
2911 THEN POP_ASSUM(fun th-> ASM_TAC
2912 THEN REWRITE_TAC[th; ]
2913 THEN REPEAT STRIP_TAC)
2914 THEN MP_TAC(REAL_ARITH`&2 <=   norm (vv (i MOD k))
2915 /\ &2 <= --v * norm (vv (i MOD k)) ==> &4<= (&1-v) *norm ((vv:num->real^3) (i MOD k))`)
2916 THEN ASM_REWRITE_TAC[REAL_ARITH`~(a<= b) <=> b<a`]
2917 THEN REPLICATE_TAC (45-32)(POP_ASSUM MP_TAC)
2918 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2919 THEN MP_TAC th)
2920 THEN REPLICATE_TAC (44-32)(POP_ASSUM MP_TAC)
2921 THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC
2922 THEN MP_TAC th)
2923 THEN POP_ASSUM MP_TAC
2924 THEN ASM_REWRITE_TAC[]
2925 THEN REAL_ARITH_TAC;
2926 ]);;
2927   (* }}} *)
2928
2929
2930
2931
2932
2933
2934
2935
2936
2937
2938
2939
2940 let JKQEWGV1=prove(
2941 `!s vv. is_scs_v39 s /\ 3< scs_k_v39 s /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
2942  ==>
2943   (sol_local (IMAGE (\i. {vv i, vv (SUC i)}) (:num))
2944    (IMAGE (\i. (vv i,vv (SUC i))) (:num))  < pi)`,
2945 REPEAT STRIP_TAC
2946 THEN ASM_TAC
2947 THEN STRIP_TAC
2948 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
2949 THEN MP_TAC th
2950 THEN REWRITE_TAC[is_scs_v39]
2951 THEN ASSUME_TAC th
2952 THEN STRIP_TAC)
2953 THEN MP_TAC(ARITH_RULE`3< scs_k_v39 s /\  scs_k_v39 s<=6 ==> scs_k_v39 s = 4\/ scs_k_v39 s = 5 \/ scs_k_v39 s =6`)
2954 THEN RESA_TAC
2955 THENL[
2956 MP_TAC(INST_TYPE [`:2+2`,`:M`]JKQEWGV1_CASE_4)
2957 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_4]
2958 THEN STRIP_TAC
2959 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]);
2960
2961 MP_TAC(INST_TYPE [`:2+3`,`:M`]JKQEWGV1_CASE_5)
2962 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_5]
2963 THEN STRIP_TAC
2964 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]);
2965
2966 MP_TAC(INST_TYPE [`:3+3`,`:M`]JKQEWGV1_CASE_6)
2967 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_6]
2968 THEN STRIP_TAC
2969 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])]);;
2970
2971
2972
2973
2974 let JKQEWGV2_CASE_4=prove(`!s vv. is_scs_v39 s /\ scs_k_v39 s=4 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
2975 /\ dimindex(:M)=scs_k_v39 s
2976 ==>
2977   (
2978     let V = IMAGE vv (:num) in
2979   let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
2980   ~circular V E)`,
2981 REPEAT GEN_TAC
2982 THEN STRIP_TAC
2983 THEN MP_TAC IS_SCS_STABLE_SYSTEM
2984 THEN RESA_TAC
2985 THEN POP_ASSUM MP_TAC
2986 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<4`]
2987 THEN STRIP_TAC
2988 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
2989          (change_type_v3 (scs_a_v39 s)),
2990          (change_type_v3 (scs_b_v39 s)),
2991          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
2992          (\i. (1 + i) MOD scs_k_v39 s))`
2993 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
2994          (change_type_v3 (scs_a_v39 s))`;`
2995          (change_type_v3 (scs_b_v39 s))`;`
2996          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
2997          (\i. (1 + i) MOD scs_k_v39 s)`]
2998 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 0]:real^3^M`
2999 THEN ABBREV_TAC`a=matvec (v:real^3^M)`
3000 THEN MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4
3001 THEN RESA_TAC
3002 THEN POP_ASSUM MP_TAC
3003 THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
3004 THEN STRIP_TAC
3005 THEN MP_TAC IN_IS_SCS_CASE_4
3006 THEN RESA_TAC
3007 THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<4`;]
3008 THEN POP_ASSUM MP_TAC
3009 THEN EXPAND_TAC"a"
3010 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
3011 THEN MP_TAC V_E_FF_IS_SCS_CASES_4
3012 THEN ASM_REWRITE_TAC[IN]
3013 THEN RESA_TAC
3014 THEN ASM_TAC
3015 THEN ASM_REWRITE_TAC[is_scs_v39;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(4<=3)`;IN;mk_unadorned_v39]
3016 THEN REPEAT RESA_TAC
3017 THEN POP_ASSUM MP_TAC
3018 THEN REWRITE_TAC[]
3019 THEN POP_ASSUM MATCH_MP_TAC
3020 THEN MP_TAC(REAL_ARITH`taustar_v39 s vv < &0 ==> taustar_v39 s vv <= &0`)
3021 THEN RESA_TAC
3022 THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
3023 THEN RESA_TAC);;
3024
3025
3026
3027 let JKQEWGV2_CASE_5=prove(`!s vv. is_scs_v39 s /\ scs_k_v39 s=5 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
3028 /\ dimindex(:M)=scs_k_v39 s
3029 ==>
3030   (
3031     let V = IMAGE vv (:num) in
3032   let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
3033   ~circular V E)`,
3034 REPEAT GEN_TAC
3035 THEN STRIP_TAC
3036 THEN MP_TAC IS_SCS_STABLE_SYSTEM
3037 THEN RESA_TAC
3038 THEN POP_ASSUM MP_TAC
3039 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<5`]
3040 THEN STRIP_TAC
3041 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
3042          (change_type_v3 (scs_a_v39 s)),
3043          (change_type_v3 (scs_b_v39 s)),
3044          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
3045          (\i. (1 + i) MOD scs_k_v39 s))`
3046 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
3047          (change_type_v3 (scs_a_v39 s))`;`
3048          (change_type_v3 (scs_b_v39 s))`;`
3049          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
3050          (\i. (1 + i) MOD scs_k_v39 s)`]
3051 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 0]:real^3^M`
3052 THEN ABBREV_TAC`a=matvec (v:real^3^M)`
3053 THEN MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5
3054 THEN RESA_TAC
3055 THEN POP_ASSUM MP_TAC
3056 THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
3057 THEN STRIP_TAC
3058 THEN MP_TAC IN_IS_SCS_CASE_5
3059 THEN RESA_TAC
3060 THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<5`;]
3061 THEN POP_ASSUM MP_TAC
3062 THEN EXPAND_TAC"a"
3063 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
3064 THEN MP_TAC V_E_FF_IS_SCS_CASES_5
3065 THEN ASM_REWRITE_TAC[IN]
3066 THEN RESA_TAC
3067 THEN ASM_TAC
3068 THEN ASM_REWRITE_TAC[is_scs_v39;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(5<=3)`;IN;mk_unadorned_v39]
3069 THEN REPEAT RESA_TAC
3070 THEN POP_ASSUM MP_TAC
3071 THEN REWRITE_TAC[]
3072 THEN POP_ASSUM MATCH_MP_TAC
3073 THEN MP_TAC(REAL_ARITH`taustar_v39 s vv < &0 ==> taustar_v39 s vv <= &0`)
3074 THEN RESA_TAC
3075 THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
3076 THEN RESA_TAC);;
3077
3078
3079
3080
3081
3082 let JKQEWGV2_CASE_6=prove(`!s vv. is_scs_v39 s /\ scs_k_v39 s=6 /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
3083 /\ dimindex(:M)=scs_k_v39 s
3084 ==>
3085   (
3086     let V = IMAGE vv (:num) in
3087   let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
3088   ~circular V E)`,
3089 REPEAT GEN_TAC
3090 THEN STRIP_TAC
3091 THEN MP_TAC IS_SCS_STABLE_SYSTEM
3092 THEN RESA_TAC
3093 THEN POP_ASSUM MP_TAC
3094 THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?a. a IN A`;ARITH_RULE`3<6`]
3095 THEN STRIP_TAC
3096 THEN ABBREV_TAC`s1 =stable_sy((scs_k_v39 s),(scs_d_v39 s),(0..scs_k_v39 s - 1),
3097          (change_type_v3 (scs_a_v39 s)),
3098          (change_type_v3 (scs_b_v39 s)),
3099          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s)),
3100          (\i. (1 + i) MOD scs_k_v39 s))`
3101 THEN MRESA_TAC stable_sy_explicit[`(scs_k_v39 s)`;`(scs_d_v39 s)`;`(0..scs_k_v39 s - 1)`;`
3102          (change_type_v3 (scs_a_v39 s))`;`
3103          (change_type_v3 (scs_b_v39 s))`;`
3104          (change_type_v2 (scs_J_v39 s) (scs_k_v39 s))`;`
3105          (\i. (1 + i) MOD scs_k_v39 s)`]
3106 THEN ABBREV_TAC`v=vector[(vv:num->real^3) 1;(vv:num->real^3) 2;(vv:num->real^3) 3;(vv:num->real^3) 4;(vv:num->real^3) 5;(vv:num->real^3) 0]:real^3^M`
3107 THEN ABBREV_TAC`a=matvec (v:real^3^M)`
3108 THEN MP_TAC TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6
3109 THEN RESA_TAC
3110 THEN POP_ASSUM MP_TAC
3111 THEN ASM_REWRITE_TAC[IN;REAL_ARITH`(a=b)<=> (b=a:real)`]
3112 THEN STRIP_TAC
3113 THEN MP_TAC IN_IS_SCS_CASE_6
3114 THEN RESA_TAC
3115 THEN MRESAL_TAC (GEN_ALL GBYCPXS)[`(scs_k_v39 s)`;`s1:stable_sy`;`a:real^(M,3)finite_product`][k_sy;B_SY1;ARITH_RULE`2<6`;]
3116 THEN POP_ASSUM MP_TAC
3117 THEN EXPAND_TAC"a"
3118 THEN REWRITE_TAC[Dih2k_hypermap.VECMATS_MATVEC_ID]
3119 THEN MP_TAC V_E_FF_IS_SCS_CASES_6
3120 THEN ASM_REWRITE_TAC[IN]
3121 THEN RESA_TAC
3122 THEN ASM_TAC
3123 THEN ASM_REWRITE_TAC[is_scs_v39;scs_d_v39_explicit;scs_a_v39_explicit;scs_b_v39_explicit;BBs_v39;ARITH_RULE`3<=3`;LET_DEF;LET_END_DEF;ARITH_RULE`~(6<=3)`;IN;mk_unadorned_v39]
3124 THEN REPEAT RESA_TAC
3125 THEN POP_ASSUM MP_TAC
3126 THEN REWRITE_TAC[]
3127 THEN POP_ASSUM MATCH_MP_TAC
3128 THEN MP_TAC(REAL_ARITH`taustar_v39 s vv < &0 ==> taustar_v39 s vv <= &0`)
3129 THEN RESA_TAC
3130 THEN MP_TAC(REAL_ARITH`scs_d_v39 s < #0.9==> scs_d_v39 s <= #0.9`)
3131 THEN RESA_TAC);;
3132
3133
3134
3135
3136 let JKQEWGV2=prove(
3137 `!s vv. is_scs_v39 s /\ 3< scs_k_v39 s /\ BBs_v39 s vv /\ taustar_v39 s vv < &0
3138  ==>
3139   (
3140     let V = IMAGE vv (:num) in
3141   let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
3142   ~circular V E)`,
3143 REPEAT STRIP_TAC
3144 THEN ASM_TAC
3145 THEN STRIP_TAC
3146 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
3147 THEN MP_TAC th
3148 THEN REWRITE_TAC[is_scs_v39]
3149 THEN ASSUME_TAC th
3150 THEN STRIP_TAC)
3151 THEN MP_TAC(ARITH_RULE`3< scs_k_v39 s /\  scs_k_v39 s<=6 ==> scs_k_v39 s = 4\/ scs_k_v39 s = 5 \/ scs_k_v39 s =6`)
3152 THEN RESA_TAC
3153 THENL[
3154 MP_TAC(INST_TYPE [`:2+2`,`:M`]JKQEWGV2_CASE_4)
3155 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_4]
3156 THEN STRIP_TAC
3157 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]);
3158
3159 MP_TAC(INST_TYPE [`:2+3`,`:M`]JKQEWGV2_CASE_5)
3160 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_5]
3161 THEN STRIP_TAC
3162 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`]);
3163
3164 MP_TAC(INST_TYPE [`:3+3`,`:M`]JKQEWGV2_CASE_6)
3165 THEN ASM_REWRITE_TAC[Basics.DIMINDEX_6]
3166 THEN STRIP_TAC
3167 THEN POP_ASSUM(fun th-> MRESA_TAC th[`s:scs_v39`;`vv:num->real^3`])]);;
3168
3169
3170
3171
3172
3173 let JKQEWGV3 = prove_by_refinement(
3174 `!s vv v w.
3175   (let V = IMAGE vv (:num) in
3176    let E = IMAGE (\i. {vv i, vv (SUC i)}) (:num) in
3177    let FF = IMAGE (\i. (vv i,vv (SUC i))) (:num) in
3178      (is_scs_v39 s /\ BBs_v39 s vv /\ 3< scs_k_v39 s /\ taustar_v39 s vv < &0 /\ lunar (v,w) V E ==>
3179         (interior_angle1 (vec 0) FF v  < pi / &2 )))`,
3180   (* {{{ proof *)
3181 [
3182 REWRITE_TAC[LET_DEF;LET_END_DEF;]
3183 THEN REPEAT STRIP_TAC
3184 THEN POP_ASSUM(fun th-> MP_TAC th
3185 THEN REWRITE_TAC[lunar]
3186 THEN ASSUME_TAC th)
3187 THEN ABBREV_TAC`V= IMAGE (vv:num->real^3) (:num)`
3188 THEN ABBREV_TAC`E= IMAGE (\i. {vv i,(vv:num->real^3) (SUC i)}) (:num)`
3189 THEN ABBREV_TAC`FF= IMAGE (\i. (vv i,(vv:num->real^3) (SUC i))) (:num)`
3190 THEN MRESA_TAC (GEN_ALL HKIRPEP)[`E:(real^3->bool)->bool`;`w:real^3`;`FF:real^3#real^3->bool`;`v:real^3`;`V:real^3->bool`]
3191 THEN ASM_TAC
3192 THEN STRIP_TAC
3193 THEN STRIP_TAC
3194 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th
3195 THEN MP_TAC(ARITH_RULE`3< scs_k_v39 s==> ~( scs_k_v39 s<= 3)`)
3196 THEN RESA_TAC
3197 THEN ASM_REWRITE_TAC[BBs_v39;LET_DEF;LET_END_DEF;]
3198 THEN STRIP_TAC
3199 THEN ASSUME_TAC th)
3200 THEN MP_TAC(SET_RULE`{v, w:real^3} SUBSET V ==> v IN V /\ w IN V`)
3201 THEN RESA_TAC
3202 THEN MRESA_TAC(GEN_ALL Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS)
3203 [`IMAGE (\i. {vv i, (vv:num->real^3) (SUC i)}) (:num)`;`IMAGE ((vv:num->real^3)) (:num)`;`IMAGE (\i. ((vv:num->real^3) i,vv (SUC i))) (:num)`]
3204 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`)
3205 THEN MRESA_TAC JKQEWGV1[`s:scs_v39`;`vv:num->real^3`]
3206 THEN POP_ASSUM MP_TAC
3207 THEN REWRITE_TAC[sol_local]
3208 THEN REPLICATE_TAC 8 (POP_ASSUM MP_TAC)
3209 THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC
3210 THEN POP_ASSUM MP_TAC
3211 THEN MP_TAC th)
3212 THEN REPLICATE_TAC 4 (POP_ASSUM MP_TAC)
3213 THEN POP_ASSUM(fun th->   REPLICATE_TAC 3 STRIP_TAC
3214 THEN MP_TAC Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM
3215 THEN REWRITE_TAC[th]
3216 THEN ASSUME_TAC th
3217 THEN MP_TAC th
3218 THEN REWRITE_TAC[convex_local_fan]
3219 THEN REPEAT STRIP_TAC)
3220 THEN POP_ASSUM MP_TAC
3221 THEN MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF
3222 THEN RESA_TAC
3223 THEN MP_TAC Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2
3224 THEN RESA_TAC
3225 THEN POP_ASSUM(fun th-> MRESA1_TAC th`v:real^3`
3226 THEN MRESA1_TAC th`w:real^3`)
3227 THEN MP_TAC(SET_RULE`v,rho_node1 FF v IN FF/\
3228 w,rho_node1 FF w IN FF ==>
3229 {(v,rho_node1 FF v ),(w,rho_node1 FF w)} SUBSET FF`)
3230 THEN RESA_TAC
3231 THEN MRESA_TAC SUM_DIFF[`(\e:real^3#real^3. azim_in_fan e E - pi)`;`FF:real^3#real^3->bool`;`{(v,rho_node1 FF v),(w,rho_node1 FF w)}`]
3232 THEN POP_ASSUM MP_TAC
3233 THEN REWRITE_TAC[REAL_ARITH`A=B-C<=> B=A+C`]
3234 THEN RESA_TAC
3235 THEN MRESAL_TAC Geomdetail.SUM_DIS2[`(v,rho_node1 FF v)`;`(w,rho_node1 FF w)`;`(\e:real^3#real^3. azim_in_fan e E - pi)`][PAIR_EQ]
3236 THEN SUBGOAL_THEN`sum (FF DIFF {(v,rho_node1 FF v), (w,rho_node1 FF w)})
3237  (\e. azim_in_fan e E - pi)= &0` ASSUME_TAC;
3238
3239 MATCH_MP_TAC SUM_EQ_0
3240 THEN REWRITE_TAC[DIFF;IN_ELIM_THM;SET_RULE`~(a IN {b,c}) <=> ~(a=b) /\ ~(a=c)`]
3241 THEN REPEAT STRIP_TAC
3242 THEN REPLICATE_TAC 8 (POP_ASSUM MP_TAC)
3243 THEN POP_ASSUM(fun th->   REPLICATE_TAC 8 STRIP_TAC
3244 THEN MRESA1_TAC th`x:real^3#real^3`)
3245 THEN POP_ASSUM(fun th->   REPLICATE_TAC 3 (POP_ASSUM MP_TAC)
3246 THEN ONCE_REWRITE_TAC[th]
3247 THEN REWRITE_TAC[PAIR_EQ])
3248 THEN REPEAT STRIP_TAC
3249 THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V)
3250 [`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`FST (x:real^3#real^3)`;`rho_node1 FF (FST (x:real^3#real^3))`;`V:real^3->bool`]
3251 THEN REPLICATE_TAC 13 (POP_ASSUM MP_TAC)
3252 THEN POP_ASSUM(fun th->   REPLICATE_TAC 13 STRIP_TAC
3253 THEN MRESA1_TAC th`FST (x:real^3#real^3)`)
3254 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3255 THEN SUBGOAL_THEN`FST (x:real^3#real^3) IN V DIFF {v,w}`ASSUME_TAC;
3256
3257 ASM_REWRITE_TAC[DIFF;IN_ELIM_THM;SET_RULE`~(a IN {b,c}) <=> ~(a=b) /\ ~(a=c)`]
3258 THEN REMOVE_ASSUM_TAC
3259 THEN REMOVE_ASSUM_TAC
3260 THEN POP_ASSUM MP_TAC
3261 THEN POP_ASSUM MP_TAC
3262 THEN SET_TAC[];
3263
3264 REPLICATE_TAC (34-7) (POP_ASSUM MP_TAC)
3265 THEN POP_ASSUM(fun th->   REPLICATE_TAC (34-7) STRIP_TAC
3266 THEN MP_TAC th
3267 THEN RESA_TAC)
3268 THEN REPLICATE_TAC (47-34) (REMOVE_ASSUM_TAC)
3269 THEN POP_ASSUM (fun th-> MRESA1_TAC th`FST (x:real^3#real^3)`)
3270 THEN REAL_ARITH_TAC;
3271
3272 ASM_REWRITE_TAC[]
3273 THEN REPLICATE_TAC 10 (POP_ASSUM MP_TAC)
3274 THEN POP_ASSUM(fun th->   REPLICATE_TAC 10 STRIP_TAC
3275 THEN MRESA1_TAC th`v:real^3`
3276 THEN MRESA1_TAC th`w:real^3`)
3277 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3278 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3279 THEN REPLICATE_TAC (30-7) (POP_ASSUM MP_TAC)
3280 THEN POP_ASSUM(fun th->   REPLICATE_TAC (30-7) STRIP_TAC
3281 THEN MP_TAC th)
3282 THEN REPLICATE_TAC (12) (POP_ASSUM MP_TAC)
3283 THEN POP_ASSUM(fun th->   REPLICATE_TAC (12) STRIP_TAC
3284 THEN REWRITE_TAC[th])
3285 THEN STRIP_TAC
3286 THEN REPLICATE_TAC (10) (REMOVE_ASSUM_TAC)
3287 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])
3288 THEN ASM_REWRITE_TAC[]
3289 THEN REAL_ARITH_TAC]);;
3290
3291
3292
3293
3294
3295
3296
3297  end;;
3298
3299
3300 (*
3301 let check_completeness_claimA_concl =
3302   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
3303 *)
3304
3305
3306
3307