text_formalization/local/WKEIDFT.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 Wkeidft = struct
  16
  17
  18 open Polyhedron;;
  19 open Sphere;;
  20 open Topology;;
  21 open Fan_misc;;
  22 open Planarity;;
  23 open Conforming;;
  24 open Hypermap;;
  25 open Fan;;
  26 open Topology;;
  27 open Wrgcvdr_cizmrrh;;
  28 open Local_lemmas;;
  29 open Collect_geom;;
  30 open Dih2k_hypermap;;
  31 open Wjscpro;;
  32 open Tecoxbm;;
  33 open Hdplygy;;
  34 open Nkezbfc_local;;
  35 open Flyspeck_constants;;
  36 open Gbycpxs;;
  37 open Pcrttid;;
  38 open Local_lemmas1;;
  39 open Pack_defs;;
  40
  41 open Hales_tactic;;
  42
  43 open Appendix;;
  44
  45
  46
  47
  48
  49 open Hypermap;;
  50 open Fan;;
  51 open Wrgcvdr_cizmrrh;;
  52 open Local_lemmas;;
  53 open Flyspeck_constants;;
  54 open Pack_defs;;
  55
  56 open Hales_tactic;;
  57
  58 open Appendix;;
  59
  60
  61 open Zithlqn;;
  62
  63
  64 open Xwitccn;;
  65
  66 open Ayqjtmd;;
  67
  68 open Jkqewgv;;
  69
  70
  71 open Mtuwlun;;
  72
  73
  74 open Uxckfpe;;
  75 open Sgtrnaf;;
  76
  77 open Yxionxl;;
  78
  79 open Qknvmlb;;
  80 open Odxlstcv2;;
  81
  82 open Yxionxl2;;
  83 open Eyypqdw;;
  84 open Ocbicby;;
  85 open Imjxphr;;
  86
  87 open Nuxcoea;;
  88 open Fektyiy;;
  89
  90
  91
  92 let SUR_MOD_FUN=prove(`~(k=0)==> ?i. (i+p) MOD k = p' MOD k`,
  93 STRIP_TAC
  94 THEN MP_TAC(ARITH_RULE`p MOD k<= p' MOD k\/ p' MOD k< p MOD k`)
  95 THEN RESA_TAC
  96 THENL[
  97 EXISTS_TAC`p' MOD k- p MOD k`
  98 THEN MRESA_TAC DIVISION[`p'`;`k`]
  99 THEN MP_TAC(ARITH_RULE`p' MOD k< k /\ p MOD k<= p' MOD k ==> p' MOD k - p MOD k < k /\ p' MOD k - p MOD k + p MOD k= p' MOD k`)
 100 THEN RESA_TAC
 101 THEN MRESAS_TAC MOD_LT[`p' MOD k- p MOD k`;`k`][DIVISION]
 102 THEN MRESAS_TAC MOD_ADD_MOD[`p' MOD k- p MOD k`;`p`;`k`][DIVISION;MOD_REFL]
 103 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]);
 104
 105 EXISTS_TAC`p' MOD k +k - p MOD k`
 106 THEN MRESA_TAC DIVISION[`p`;`k`]
 107 THEN MP_TAC(ARITH_RULE`p MOD k< k /\ p' MOD k< p MOD k ==> p' MOD k +k - p MOD k < k /\ (p' MOD k + k - p MOD k) + p MOD k=1*k+ p' MOD k`)
 108 THEN RESA_TAC
 109 THEN MRESAS_TAC MOD_LT[`p' MOD k+k- p MOD k`;`k`][DIVISION]
 110 THEN MRESAS_TAC MOD_ADD_MOD[`p' MOD k+k- p MOD k`;`p`;`k`][DIVISION;MOD_REFL;MOD_MULT_ADD]
 111 THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th])]);;
 112
 113 let TRANS_DIAG=prove(`~(k=0)/\ (i+p) MOD k = p' MOD k /\ p' + q = p + q'
 114 ==> (i+q) MOD k= q' MOD k `,
 115 STRIP_TAC
 116 THEN MATCH_MP_TAC Hdplygy.MOD_EQ_MOD
 117 THEN EXISTS_TAC`p:num`
 118 THEN ASM_REWRITE_TAC[]
 119 THEN ONCE_REWRITE_TAC[ARITH_RULE`p + i + q= (i +p)+ q:num`]
 120 THEN MRESA_TAC MOD_ADD_MOD[`i+p:num`;`q`;`k`]
 121 THEN POP_ASSUM(fun th-> ASM_SIMP_TAC[SYM th;MOD_ADD_MOD]));;
 122
 123
 124 (*************)
 125
 126
 127 (*******************)
 128
 129
 130 let scs_components = prove_by_refinement(
 131   `!s. dest_scs_v39 s = (scs_k_v39 s,scs_d_v39 s,scs_a_v39
 132 s,scs_am_v39 s ,scs_bm_v39 s,scs_b_v39 s,scs_J_v39 s,
 133                          scs_lo_v39 s,scs_hi_v39 s,scs_str_v39 s)`,
 134   (* {{{ proof *)
 135   [
 136   REWRITE_TAC[Wrgcvdr_cizmrrh.PAIR_EQ2;scs_k_v39;scs_d_v39;scs_a_v39;];
 137   REWRITE_TAC[scs_am_v39;scs_bm_v39;scs_b_v39;];
 138   REWRITE_TAC[scs_J_v39;scs_hi_v39;scs_lo_v39;];
 139   REWRITE_TAC[scs_str_v39];
 140
 141 BY(REWRITE_TAC[Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.part2;Misc_defs_and_lemmas.part3;Misc_defs_and_lemmas.part4;
 142 Misc_defs_and_lemmas.part5;Misc_defs_and_lemmas.part6;Misc_defs_and_lemmas.part7;Misc_defs_and_lemmas.drop0;Misc_defs_and_lemmas.drop3;Misc_defs_and_lemmas.drop1;Misc_defs_and_lemmas.part0;Misc_defs_and_lemmas.part8;Misc_defs_and_lemmas.drop2])
 143   ]);;
 144   (* }}} *)
 145
 146 let scs_inj = prove_by_refinement(
 147   `!s s'. scs_basic_v39 s /\  scs_basic_v39 s' /\
 148     scs_d_v39 s = scs_d_v39 s' /\
 149     scs_k_v39 s = scs_k_v39 s' /\
 150     (scs_a_v39 s = scs_a_v39 s') /\
 151     (scs_b_v39 s = scs_b_v39 s')
 152   ==> (s = s')`,
 153
 154   (* {{{ proof *)
 155   [
 156   REPEAT WEAKER_STRIP_TAC;
 157   REPEAT (FIRST_X_ASSUM_ST `scs_basic_v39` MP_TAC);
 158   REWRITE_TAC[scs_basic;unadorned_v39];
 159   ONCE_REWRITE_TAC[EQ_SYM_EQ];
 160   REWRITE_TAC[SET_RULE `{} = a <=> a = {}`];
 161   REPEAT WEAKER_STRIP_TAC;
 162   ONCE_REWRITE_TAC[GSYM scs_v39];
 163   AP_TERM_TAC;
 164   ASM_REWRITE_TAC[scs_components];
 165   TYPIFY `scs_J_v39 s = scs_J_v39 s'` (C SUBGOAL_THEN SUBST1_TAC);
 166     BY(ASM_REWRITE_TAC[FUN_EQ_THM]);
 167   BY(REWRITE_TAC[])
 168   ]);;
 169   (* }}} *)
 170
 171
 172
 173 let DIAG_PSORT1=prove_by_refinement(` ~(k=0) /\ (i+p) MOD k = p' MOD k /\
 174 p' + q = p + q' /\ ~(k=0) /\ (psort k (i',j) = psort k (p,q))
 175 ==>  (psort k (i+i',i+j) = psort k (p',q'))`,
 176
 177 [
 178 REWRITE_TAC[psort;LET_DEF;LET_END_DEF;COND_EXPAND
 179 ]
 180 THEN RESA_TAC
 181 THEN POP_ASSUM MP_TAC
 182 THEN MP_TAC TRANS_DIAG
 183 THEN RESA_TAC
 184 THEN MP_TAC(SET_RULE`i' MOD k <= j MOD k \/ ~(i' MOD k <= j MOD k)`)
 185 THEN RESA_TAC;
 186
 187 MP_TAC(SET_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
 188 THEN RESA_TAC;
 189
 190 REWRITE_TAC[PAIR_EQ]
 191 THEN RESA_TAC
 192 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
 193 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`];
 194
 195 REWRITE_TAC[PAIR_EQ]
 196 THEN RESA_TAC
 197 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
 198 THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][]
 199 THEN MP_TAC(ARITH_RULE`(~(p' MOD k<= q' MOD k))\/ (p' MOD k < q' MOD k ) \/ (p' MOD k = q' MOD k )`)
 200 THEN RESA_TAC;
 201
 202 MP_TAC(ARITH_RULE` ~(p' MOD k<= q' MOD k)==> q' MOD k <= p' MOD k`)
 203 THEN RESA_TAC;
 204
 205 MP_TAC(ARITH_RULE` (p' MOD k< q' MOD k)==> ~(q' MOD k <= p' MOD k)/\ (p' MOD k<= q' MOD k)`)
 206 THEN RESA_TAC;
 207
 208 MP_TAC(SET_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
 209 THEN RESA_TAC;
 210
 211 REWRITE_TAC[PAIR_EQ]
 212 THEN RESA_TAC
 213 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
 214 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`];
 215
 216
 217 MP_TAC(ARITH_RULE`(~(p' MOD k<= q' MOD k))\/ (p' MOD k < q' MOD k ) \/ (p' MOD k = q' MOD k )`)
 218 THEN RESA_TAC;
 219
 220 MP_TAC(ARITH_RULE` ~(p' MOD k<= q' MOD k)==> q' MOD k <= p' MOD k`)
 221 THEN RESA_TAC;
 222
 223 MP_TAC(ARITH_RULE` (p' MOD k< q' MOD k)==> ~(q' MOD k <= p' MOD k)/\ (p' MOD k<= q' MOD k)`)
 224 THEN RESA_TAC;
 225
 226 REWRITE_TAC[PAIR_EQ]
 227 THEN RESA_TAC
 228 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
 229 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`]]);;
 230
 231
 232
 233
 234
 235 let DIAG_PSORT2=prove_by_refinement(` ~(k=0) /\ (i+p) MOD k = p' MOD k /\
 236 p' + q = p + q' /\ ~(k=0) /\ (psort k (i+i',i+j) = psort k (p',q'))
 237 ==>
 238 (psort k (i',j) = psort k (p,q))`,
 239 [
 240 REWRITE_TAC[psort;LET_DEF;LET_END_DEF;COND_EXPAND
 241 ]
 242 THEN RESA_TAC
 243 THEN POP_ASSUM MP_TAC
 244 THEN MP_TAC TRANS_DIAG
 245 THEN RESA_TAC
 246 THEN MP_TAC(SET_RULE`(i+i') MOD k <= (i+j) MOD k \/ ~((i+i') MOD k <= (i+j) MOD k)`)
 247 THEN RESA_TAC;
 248
 249 MP_TAC(SET_RULE`p' MOD k <= q' MOD k \/ ~(p' MOD k <= q' MOD k)`)
 250 THEN RESA_TAC;
 251
 252 REWRITE_TAC[PAIR_EQ]
 253 THEN RESA_TAC
 254 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
 255 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`];
 256
 257 REWRITE_TAC[PAIR_EQ]
 258 THEN RESA_TAC
 259 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
 260 THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][];
 261
 262 MP_TAC(ARITH_RULE`(~(p MOD k<= q MOD k))\/ (p MOD k < q MOD k ) \/ (p MOD k = q MOD k )`)
 263 THEN RESA_TAC;
 264
 265
 266 MP_TAC(ARITH_RULE` ~(p MOD k<= q MOD k)==> q MOD k <= p MOD k`)
 267 THEN RESA_TAC;
 268
 269 MP_TAC(ARITH_RULE` (p MOD k< q MOD k)==> ~(q MOD k <= p MOD k)/\ (p MOD k<= q MOD k)`)
 270 THEN RESA_TAC;
 271
 272 MP_TAC(SET_RULE`p' MOD k <= q' MOD k \/ ~(p' MOD k <= q' MOD k)`)
 273 THEN RESA_TAC;
 274
 275 REWRITE_TAC[PAIR_EQ]
 276 THEN RESA_TAC
 277 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`q`;`i`]
 278 THEN MRESAS_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`p`;`i`][];
 279
 280 MP_TAC(ARITH_RULE`(~(p MOD k<= q MOD k))\/ (p MOD k < q MOD k ) \/ (p MOD k = q MOD k )`)
 281 THEN RESA_TAC;
 282
 283 MP_TAC(ARITH_RULE` ~(p MOD k<= q MOD k)==> q MOD k <= p MOD k`)
 284 THEN RESA_TAC;
 285
 286 MP_TAC(ARITH_RULE` (p MOD k< q MOD k)==> ~(q MOD k <= p MOD k)/\ (p MOD k<= q MOD k)`)
 287 THEN RESA_TAC;
 288
 289 REWRITE_TAC[PAIR_EQ]
 290 THEN RESA_TAC
 291 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`i'`;`p`;`i`]
 292 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`j`;`q`;`i`]]);;
 293
 294
 295
 296
 297 let DIAG_PSORT=prove(
 298  ` ~(k=0) /\ (i+p) MOD k = p' MOD k /\
 299 p' + q = p + q' /\ ~(k=0)
 300 ==>
 301 ((psort k (i+i',i+j) = psort k (p',q'))
 302 <=>
 303 (psort k (i',j) = psort k (p,q)))`,
 304 STRIP_TAC
 305 THEN EQ_TAC
 306 THEN STRIP_TAC
 307 THENL[
 308 MATCH_MP_TAC DIAG_PSORT2
 309 THEN RESA_TAC;
 310 MATCH_MP_TAC DIAG_PSORT1
 311 THEN RESA_TAC]);;
 312
 313 let TRANS_DIAG=prove(`
 314 ~(k=0)
 315 ==> (scs_diag k i' j<=> scs_diag k (i+i') (i+j)) `,
 316 SIMP_TAC[scs_diag;ARITH_RULE`SUC (i + i') = i + (i' + 1)/\ SUC i= i+1`;Ocbicby.MOD_EQ_MOD_SHIFT]);;
 317
 318
 319 let A_EQ_PSORT=prove(` is_scs_v39 s  /\ psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (p,q)
 320 ==> scs_a_v39 s i j= scs_a_v39 s p q`,
 321 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF; BBs_v39; FUN_EQ_THM;psort]
 322 THEN REPEAT RESA_TAC
 323 THEN POP_ASSUM MP_TAC
 324 THEN ABBREV_TAC`k=scs_k_v39 s`
 325 THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k \/ ~(i MOD k <= j MOD k)`)
 326 THEN RESA_TAC
 327 THEN MP_TAC(ARITH_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
 328 THEN RESA_TAC
 329 THEN
 330 REWRITE_TAC[PAIR_EQ]
 331 THEN STRIP_TAC
 332 THEN MRESA_TAC CHANGE_A_SCS_MOD[`i`;`j`;`s`;`p`;`q`]
 333 THEN MRESA_TAC CHANGE_A_SCS_MOD[`j`;`i`;`s`;`p`;`q`]
 334 THEN ASM_TAC
 335 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 336 THEN REPEAT RESA_TAC);;
 337
 338
 339 let B_EQ_PSORT=prove(` is_scs_v39 s  /\ psort (scs_k_v39 s) (i,j) = psort (scs_k_v39 s) (p,q)
 340 ==> scs_b_v39 s i j= scs_b_v39 s p q`,
 341 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF; BBs_v39; FUN_EQ_THM;psort]
 342 THEN REPEAT RESA_TAC
 343 THEN POP_ASSUM MP_TAC
 344 THEN ABBREV_TAC`k=scs_k_v39 s`
 345 THEN MP_TAC(ARITH_RULE`i MOD k <= j MOD k \/ ~(i MOD k <= j MOD k)`)
 346 THEN RESA_TAC
 347 THEN MP_TAC(ARITH_RULE`p MOD k <= q MOD k \/ ~(p MOD k <= q MOD k)`)
 348 THEN RESA_TAC
 349 THEN
 350 REWRITE_TAC[PAIR_EQ]
 351 THEN STRIP_TAC
 352 THEN MRESA_TAC CHANGE_B_SCS_MOD[`i`;`j`;`s`;`p`;`q`]
 353 THEN MRESA_TAC CHANGE_B_SCS_MOD[`j`;`i`;`s`;`p`;`q`]
 354 THEN ASM_TAC
 355 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 356 THEN REPEAT RESA_TAC);;
 357
 358 let PROPERTY_OF_K_SCS=prove(`is_scs_v39 s==> ~(scs_k_v39 s= 0)/\ 0< scs_k_v39 s/\ 1< scs_k_v39 s/\ 2< scs_k_v39 s`,
 359 STRIP_TAC
 360 THEN MP_TAC Axjrpnc.is_scs_k_le_3
 361 THEN RESA_TAC
 362 THEN DICH_TAC 0
 363 THEN ARITH_TAC);;
 364
 365 let WKEIDFT_A_concl = `!s s' a b a' b' p q p' q' i.
 366   (let k = scs_k_v39 s in
 367      (is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
 368        (!i. scs_a_v39 s i (i + 1) = a) /\
 369        (!i. scs_b_v39 s i (i + 1) = b) /\
 370        (!i. scs_a_v39 s' i (i + 1) = a) /\
 371        (!i. scs_b_v39 s' i (i + 1) = b) /\
 372        scs_k_v39 s' = k /\
 373        p' + q = p + q' /\
 374        scs_d_v39 s = scs_d_v39 s' /\
 375        (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_a_v39 s i j = a') /\
 376        (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_b_v39 s i j = b') /\
 377        (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_a_v39 s' i j = a') /\
 378        (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_b_v39 s' i j = b') /\
 379          scs_a_v39 s p q = scs_a_v39 s' p' q' /\ scs_b_v39 s p q = scs_b_v39 s' p' q' /\ (i+p) MOD k = p' MOD k ==>
 380 (\j j'. scs_a_v39 s' (i + j) (i + j')) = scs_a_v39 s))`;;
 381
 382
 383
 384 let WKEIDFT_A=prove_by_refinement( WKEIDFT_A_concl,
 385 [
 386 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39; FUN_EQ_THM]
 387 THEN REPEAT RESA_TAC
 388 THEN ABBREV_TAC`k= scs_k_v39 s`
 389 THEN MP_TAC(SET_RULE`scs_diag k x x'\/ ~(scs_diag k x x')`)
 390 THEN RESA_TAC;
 391
 392 MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
 393 THEN RESA_TAC;
 394
 395 MP_TAC PROPERTY_OF_K_SCS
 396 THEN RESA_TAC
 397 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
 398 THEN MRESA_TAC A_EQ_PSORT[`x`;`x'`;`s`;`p`;`q`]
 399 THEN MRESA_TAC A_EQ_PSORT[`i+x:num`;`i+x':num`;`s'`;`p'`;`q'`];
 400
 401 MP_TAC PROPERTY_OF_K_SCS
 402 THEN RESA_TAC
 403 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
 404 THEN MRESA_TAC TRANS_DIAG[`k`;`x`;`i`;`x'`]
 405 THEN MATCH_DICH_TAC (26-13)
 406 THEN ASM_REWRITE_TAC[];
 407
 408
 409 POP_ASSUM MP_TAC
 410 THEN REWRITE_TAC[scs_diag;DE_MORGAN_THM]
 411 THEN STRIP_TAC;
 412
 413 MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`x`;`x`]
 414 THEN MP_TAC PROPERTY_OF_K_SCS
 415 THEN RESA_TAC
 416 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`x'`;`i`]
 417 THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+x:num`;`i+x:num`]
 418 THEN ASM_TAC
 419 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 420 THEN REPEAT RESA_TAC;
 421
 422 MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`x`;`SUC x`]
 423 THEN MP_TAC PROPERTY_OF_K_SCS
 424 THEN RESA_TAC
 425 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`SUC x`;`x'`;`i`]
 426 THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+x:num`;`i+SUC x:num`]
 427 THEN REWRITE_TAC[ADD1]
 428 THEN THAYTHEL_TAC(26-6)[`i+x:num`][ARITH_RULE`(i + x) + 1= i + x + 1`]
 429 THEN THAYTHE_TAC(26-4)[`x`];
 430
 431
 432 MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`SUC x'`;`x'`]
 433 THEN MP_TAC PROPERTY_OF_K_SCS
 434 THEN RESA_TAC
 435 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`SUC x'`;`i`]
 436 THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+SUC x':num`;`i+x':num`]
 437 THEN REWRITE_TAC[ADD1]
 438 THEN THAYTHEL_TAC(26-6)[`i+x':num`][ARITH_RULE`(i + x) + 1= i + x + 1`]
 439 THEN THAYTHE_TAC(26-4)[`x'`]
 440 THEN ASM_TAC
 441 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 442 THEN REPEAT RESA_TAC]);;
 443
 444
 445
 446
 447
 448 let WKEIDFT_B_concl = `!s s' a b a' b' p q p' q' a1 i.
 449   (let k = scs_k_v39 s in
 450      (is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
 451        (!i. scs_b_v39 s i i = a1) /\
 452        (!i. scs_b_v39 s' i i = a1) /\
 453        (!i. scs_a_v39 s i (i + 1) = a) /\
 454        (!i. scs_b_v39 s i (i + 1) = b) /\
 455        (!i. scs_a_v39 s' i (i + 1) = a) /\
 456        (!i. scs_b_v39 s' i (i + 1) = b) /\
 457        scs_k_v39 s' = k /\
 458        p' + q = p + q' /\
 459        scs_d_v39 s = scs_d_v39 s' /\
 460        (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_a_v39 s i j = a') /\
 461        (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_b_v39 s i j = b') /\
 462        (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_a_v39 s' i j = a') /\
 463        (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_b_v39 s' i j = b') /\
 464          scs_a_v39 s p q = scs_a_v39 s' p' q' /\ scs_b_v39 s p q = scs_b_v39 s' p' q' /\ (i+p) MOD k = p' MOD k ==>
 465 (\j j'. scs_b_v39 s' (i + j) (i + j')) = scs_b_v39 s))`;;
 466
 467
 468
 469 let WKEIDFT_B=prove_by_refinement( WKEIDFT_B_concl,
 470 [
 471 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39; FUN_EQ_THM]
 472 THEN REPEAT RESA_TAC
 473 THEN ABBREV_TAC`k= scs_k_v39 s`
 474 THEN MP_TAC(SET_RULE`scs_diag k x x'\/ ~(scs_diag k x x')`)
 475 THEN RESA_TAC;
 476
 477 MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
 478 THEN RESA_TAC;
 479
 480 MP_TAC PROPERTY_OF_K_SCS
 481 THEN RESA_TAC
 482 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
 483 THEN MRESA_TAC B_EQ_PSORT[`x`;`x'`;`s`;`p`;`q`]
 484 THEN MRESA_TAC B_EQ_PSORT[`i+x:num`;`i+x':num`;`s'`;`p'`;`q'`];
 485
 486 MP_TAC PROPERTY_OF_K_SCS
 487 THEN RESA_TAC
 488 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
 489 THEN MRESA_TAC TRANS_DIAG[`k`;`x`;`i`;`x'`]
 490 THEN MATCH_DICH_TAC (26-14)
 491 THEN ASM_REWRITE_TAC[];
 492
 493 POP_ASSUM MP_TAC
 494 THEN REWRITE_TAC[scs_diag;DE_MORGAN_THM]
 495 THEN STRIP_TAC;
 496
 497 MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`x`;`x`]
 498 THEN MP_TAC PROPERTY_OF_K_SCS
 499 THEN RESA_TAC
 500 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`x'`;`i`]
 501 THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+x:num`;`i+x:num`]
 502 THEN ASM_TAC
 503 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 504 THEN REPEAT RESA_TAC;
 505
 506 MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`x`;`SUC x`]
 507 THEN MP_TAC PROPERTY_OF_K_SCS
 508 THEN RESA_TAC
 509 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`SUC x`;`x'`;`i`]
 510 THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+x:num`;`i+SUC x:num`]
 511 THEN REWRITE_TAC[ADD1]
 512 THEN THAYTHEL_TAC(26-7)[`i+x:num`][ARITH_RULE`(i + x) + 1= i + x + 1`]
 513 THEN THAYTHE_TAC(26-5)[`x`];
 514
 515 MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`SUC x'`;`x'`]
 516 THEN MP_TAC PROPERTY_OF_K_SCS
 517 THEN RESA_TAC
 518 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`SUC x'`;`i`]
 519 THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s'`;`i+SUC x':num`;`i+x':num`]
 520 THEN REWRITE_TAC[ADD1]
 521 THEN THAYTHEL_TAC(26-7)[`i+x':num`][ARITH_RULE`(i + x) + 1= i + x + 1`]
 522 THEN THAYTHE_TAC(26-5)[`x'`]
 523 THEN ASM_TAC
 524 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 525 THEN REPEAT RESA_TAC]);;
 526
 527
 528
 529
 530
 531 let WKEIDFT_EQU_concl = `
 532   (let k = scs_k_v39 s in
 533      (is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
 534        (!i. scs_b_v39 s i i = a1) /\
 535        (!i. scs_b_v39 s' i i = a1) /\
 536        (!i. scs_a_v39 s i (i + 1) = a) /\
 537        (!i. scs_b_v39 s i (i + 1) = b) /\
 538        (!i. scs_a_v39 s' i (i + 1) = a) /\
 539        (!i. scs_b_v39 s' i (i + 1) = b) /\
 540        scs_k_v39 s' = k /\
 541        p' + q = p + q' /\
 542        scs_d_v39 s = scs_d_v39 s' /\
 543        (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_a_v39 s i j = a') /\
 544        (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_b_v39 s i j = b') /\
 545        (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_a_v39 s' i j = a') /\
 546        (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_b_v39 s' i j = b') /\
 547          scs_a_v39 s p q = scs_a_v39 s' p' q' /\ scs_b_v39 s p q = scs_b_v39 s' p' q'  ==>
 548    ?i.  s'= scs_prop_equ_v39 s i))`;;
 549
 550
 551
 552
 553
 554 let WKEIDFT_EQU=prove( WKEIDFT_EQU_concl,
 555 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; scs_basic]
 556 THEN REPEAT RESA_TAC
 557 THEN ABBREV_TAC`k= scs_k_v39 s`
 558 THEN MP_TAC PROPERTY_OF_K_SCS
 559 THEN RESA_TAC
 560 THEN MRESA_TAC SUR_MOD_FUN[`p':num`;`p:num`;`k:num`]
 561 THEN ASM_TAC
 562 THEN REPEAT RESA_TAC
 563 THEN EXISTS_TAC`i:num`
 564 THEN MRESAL_TAC WKEIDFT_B[`s':scs_v39`;`s:scs_v39`;`a:real`;`b:real`;`a':real`;`b':real`;`p':num`;`q':num`;`p:num`;`q:num`;`a1:real`;`i`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
 565 THEN MRESAL_TAC WKEIDFT_A[`s':scs_v39`;`s:scs_v39`;`a:real`;`b:real`;`a':real`;`b':real`;`p':num`;`q':num`;`p:num`;`q:num`;`i`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
 566 THEN MATCH_MP_TAC scs_inj
 567 THEN ASM_REWRITE_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
 568 THEN SET_TAC[]);;
 569
 570 let WKEIDFT_concl = `!s s' a b a' b' p q p' q'.
 571   (let k = scs_k_v39 s in
 572      (is_scs_v39 s /\ is_scs_v39 s' /\ scs_basic_v39 s /\ scs_basic_v39 s' /\
 573        (!i. scs_b_v39 s i i = a1) /\
 574        (!i. scs_b_v39 s' i i = a1) /\
 575        (!i. scs_a_v39 s i (i + 1) = a) /\
 576        (!i. scs_b_v39 s i (i + 1) = b) /\
 577        (!i. scs_a_v39 s' i (i + 1) = a) /\
 578        (!i. scs_b_v39 s' i (i + 1) = b) /\
 579        scs_k_v39 s' = k /\
 580        p' + q = p + q' /\
 581        scs_d_v39 s = scs_d_v39 s' /\
 582        (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_a_v39 s i j = a') /\
 583        (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p,q)) ==> scs_b_v39 s i j = b') /\
 584        (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_a_v39 s' i j = a') /\
 585        (!i j. scs_diag k i j /\ ~(psort k (i,j) = psort k (p',q')) ==> scs_b_v39 s' i j = b') /\
 586          scs_a_v39 s p q = scs_a_v39 s' p' q' /\ scs_b_v39 s p q = scs_b_v39 s' p' q' ==>
 587      scs_arrow_v39 {s} {s'}))`;;
 588
 589
 590
 591 let WKEIDFT_PRIME= prove(WKEIDFT_concl,
 592 REWRITE_TAC[LET_DEF;LET_END_DEF]
 593 THEN REPEAT RESA_TAC
 594 THEN MP_TAC WKEIDFT_EQU
 595 THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
 596 THEN RESA_TAC
 597 THEN MATCH_MP_TAC YXIONXL3
 598 THEN ASM_REWRITE_TAC[]);;
 599
 600
 601
 602 (********************************)
 603
 604 let WKEIDFT_B_v2_concl = `!s a b a' b' p q p' q'.
 605     (let k = scs_k_v39 s in
 606        (is_scs_v39 s /\ scs_basic_v39 s /\
 607           (!i. scs_a_v39 s i (i + 1) = a) /\
 608           (!i. scs_b_v39 s i (i + 1) = b) /\
 609            p' + q = p + q' /\
 610          scs_diag k p q/\
 611          scs_diag k p' q'/\
 612            (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\
 613            (!i j. scs_diag k i j  ==> scs_a_v39 s i j = a') /\
 614            (!i j. scs_diag k i j  ==> scs_b_v39 s i j = b')/\
 615           (!i. scs_b_v39 s i i = b1) /\
 616  (i+p) MOD k = p' MOD k ==>
 617 (\j j'. scs_b_v39 (scs_stab_diag_v39 s p' q') (i + j) (i + j')) = scs_b_v39 (scs_stab_diag_v39 s p q)))`;;
 618
 619
 620 let WKEIDFT_B_V2=prove_by_refinement( WKEIDFT_B_v2_concl,
 621 [
 622 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39; FUN_EQ_THM;scs_stab_diag_v39;mk_unadorned_v39;scs_v39_explicit]
 623 THEN REPEAT RESA_TAC
 624 THEN ABBREV_TAC`k= scs_k_v39 s`;
 625
 626 MP_TAC(SET_RULE`scs_diag k x x'\/ ~(scs_diag k x x')`)
 627 THEN RESA_TAC;
 628
 629 MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
 630 THEN RESA_TAC;
 631
 632 MP_TAC PROPERTY_OF_K_SCS
 633 THEN RESA_TAC
 634 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
 635 THEN MRESA_TAC B_EQ_PSORT[`x`;`x'`;`s`;`p`;`q`]
 636 THEN MRESA_TAC B_EQ_PSORT[`i+x:num`;`i+x':num`;`s'`;`p'`;`q'`];
 637
 638 MP_TAC PROPERTY_OF_K_SCS
 639 THEN RESA_TAC
 640 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
 641 THEN MRESA_TAC TRANS_DIAG[`k`;`x`;`i`;`x'`] ;
 642
 643 POP_ASSUM MP_TAC
 644 THEN REWRITE_TAC[scs_diag;DE_MORGAN_THM]
 645 THEN STRIP_TAC;
 646
 647 MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
 648 THEN RESA_TAC
 649 THEN MP_TAC PROPERTY_OF_K_SCS
 650 THEN RESA_TAC
 651 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
 652 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`x'`;`i`]
 653 THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+x:num`;`i+x:num`]
 654 THEN MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`x`;`x`];
 655
 656 MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
 657 THEN RESA_TAC
 658 THEN MP_TAC PROPERTY_OF_K_SCS
 659 THEN RESA_TAC
 660 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
 661 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`SUC x`;`x'`;`i`]
 662 THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+x:num`;`i+SUC x:num`]
 663 THEN MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`x`;`SUC x`]
 664 THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+a+1=(i+a)+1`];
 665
 666
 667 MP_TAC(SET_RULE`(psort k (x,x') = psort k (p,q))\/ ~(psort k (x,x') = psort k (p,q))`)
 668 THEN RESA_TAC
 669 THEN MP_TAC PROPERTY_OF_K_SCS
 670 THEN RESA_TAC
 671 THEN MRESAS_TAC DIAG_PSORT[`i`;`p'`;`q'`;`x`;`x'`;`k`;`p`;`q`][PROPERTY_OF_K_SCS]
 672 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`SUC x'`;`i`]
 673 THEN MRESA_TAC CHANGE_B_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+SUC x':num`;`i+x':num`]
 674 THEN MRESA_TAC CHANGE_B_SCS_MOD[`x`;`x'`;`s`;`SUC x'`;`x'`]
 675 THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+a+1=(i+a)+1`]
 676 THEN ASM_TAC
 677 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 678 THEN REPEAT RESA_TAC]);;
 679
 680
 681
 682
 683
 684
 685 let WKEIDFT_A_v2_concl = `!s a b a' b' p q p' q'.
 686     (let k = scs_k_v39 s in
 687        (is_scs_v39 s /\ scs_basic_v39 s /\
 688           (!i. scs_a_v39 s i (i + 1) = a) /\
 689           (!i. scs_b_v39 s i (i + 1) = b) /\
 690            p' + q = p + q' /\
 691          scs_diag k p q/\
 692          scs_diag k p' q'/\
 693            (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\
 694            (!i j. scs_diag k i j  ==> scs_a_v39 s i j = a') /\
 695            (!i j. scs_diag k i j  ==> scs_b_v39 s i j = b')/\
 696           (!i. scs_b_v39 s i i = b1) /\
 697  (i+p) MOD k = p' MOD k ==>
 698 (\j j'. scs_a_v39 (scs_stab_diag_v39 s p' q') (i + j) (i + j')) = scs_a_v39 (scs_stab_diag_v39 s p q)))`;;
 699
 700
 701 let WKEIDFT_A_V2=prove_by_refinement( WKEIDFT_A_v2_concl,
 702 [
 703 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; BBs_v39; FUN_EQ_THM;scs_stab_diag_v39;mk_unadorned_v39;scs_v39_explicit]
 704 THEN REPEAT RESA_TAC
 705 THEN ABBREV_TAC`k= scs_k_v39 s`;
 706
 707 MP_TAC(SET_RULE`scs_diag k x x'\/ ~(scs_diag k x x')`)
 708 THEN RESA_TAC;
 709
 710 MP_TAC PROPERTY_OF_K_SCS
 711 THEN RESA_TAC
 712 THEN MRESAS_TAC TRANS_DIAG[`k`;`x`;`i`;`x'`][];
 713
 714 POP_ASSUM MP_TAC
 715 THEN REWRITE_TAC[scs_diag;DE_MORGAN_THM]
 716 THEN STRIP_TAC;
 717
 718 MP_TAC PROPERTY_OF_K_SCS
 719 THEN RESA_TAC
 720 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`x'`;`i`]
 721 THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+x:num`;`i+x:num`]
 722 THEN MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`x`;`x`]
 723 THEN ASM_TAC
 724 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 725 THEN REPEAT RESA_TAC;
 726
 727 MP_TAC PROPERTY_OF_K_SCS
 728 THEN RESA_TAC
 729 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`SUC x`;`x'`;`i`]
 730 THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+x:num`;`i+SUC x:num`]
 731 THEN MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`x`;`SUC x`]
 732 THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+a+1=(i+a)+1`];
 733
 734 MP_TAC PROPERTY_OF_K_SCS
 735 THEN RESA_TAC
 736 THEN MRESA_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`k`;`x`;`SUC x'`;`i`]
 737 THEN MRESA_TAC CHANGE_A_SCS_MOD[`i+x:num`;`i+x':num`;`s`;`i+SUC x':num`;`i+x':num`]
 738 THEN MRESA_TAC CHANGE_A_SCS_MOD[`x`;`x'`;`s`;`SUC x'`;`x'`]
 739 THEN ASM_SIMP_TAC[ADD1;ARITH_RULE`i+a+1=(i+a)+1`]
 740 THEN ASM_TAC
 741 THEN REWRITE_TAC[LET_DEF;LET_END_DEF;is_scs_v39]
 742 THEN REPEAT RESA_TAC]);;
 743
 744
 745 let SCS_K_D_A_STAB_EQ=prove(`scs_d_v39 (scs_stab_diag_v39 s i j) =scs_d_v39 s
 746 /\ scs_k_v39 (scs_stab_diag_v39 s i j) =scs_k_v39 s
 747 /\(!i' j'. scs_a_v39 (scs_stab_diag_v39 s i j) i' j'= scs_a_v39 s i' j')`,
 748 SIMP_TAC[scs_basic;LET_DEF;LET_END_DEF;BBs_v39;scs_stab_diag_v39;scs_v39_explicit;mk_unadorned_v39]);;
 749
 750
 751
 752
 753 let WKEIDFT_EQU_v2_concl = `
 754     (let k = scs_k_v39 s in
 755        (is_scs_v39 s /\ scs_basic_v39 s /\
 756           (!i. scs_a_v39 s i (i + 1) = a) /\
 757           (!i. scs_b_v39 s i (i + 1) = b) /\
 758            p' + q = p + q' /\
 759          scs_diag k p q/\
 760          scs_diag k p' q'/\
 761     3 < k /\
 762            (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\
 763            (!i j. scs_diag k i j  ==> scs_a_v39 s i j = a') /\
 764            (!i j. scs_diag k i j  ==> scs_b_v39 s i j = b')/\
 765           (!i. scs_b_v39 s i i = b1) ==>
 766 ?i.  scs_stab_diag_v39 s p' q'= scs_prop_equ_v39 (scs_stab_diag_v39 s p q) i))`;;
 767
 768
 769 let WKEIDFT_EQU_V2= prove(WKEIDFT_EQU_v2_concl,
 770 REWRITE_TAC[scs_prop_equ_v39;scs_arrow_v39;IN_SING;LET_DEF;LET_END_DEF;unadorned_v39; scs_basic]
 771 THEN REPEAT RESA_TAC
 772 THEN ABBREV_TAC`k= scs_k_v39 s`
 773 THEN MP_TAC PROPERTY_OF_K_SCS
 774 THEN RESA_TAC
 775 THEN MRESA_TAC SUR_MOD_FUN[`p':num`;`p:num`;`k:num`]
 776 THEN ASM_TAC
 777 THEN REPEAT RESA_TAC
 778 THEN EXISTS_TAC`i:num`
 779 THEN MRESAL_TAC WKEIDFT_B_V2[`b1`;`i`;`s`;`a`;`b`;`a'`;`b'`;`p'`;`q'`;`p`;`q`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
 780 THEN MRESAL_TAC WKEIDFT_A_V2[`b1`;`i`;`s`;`a`;`b`;`a'`;`b'`;`p'`;`q'`;`p`;`q`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
 781 THEN MRESAS_TAC Yrtafyh.YRTAFYH[`s`;`p`;`q`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;SCS_K_D_A_STAB_EQ]
 782 THEN DICH_TAC 1
 783 THEN STRIP_TAC
 784 THEN SYM_ASSUM_TAC
 785 THEN DICH_TAC 1
 786 THEN STRIP_TAC
 787 THEN SYM_ASSUM_TAC
 788 THEN MATCH_MP_TAC scs_inj
 789 THEN MRESAS_TAC Yrtafyh.YRTAFYH[`s`;`p'`;`q'`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;SCS_K_D_A_STAB_EQ]
 790 THEN ASM_SIMP_TAC[scs_v39_explicit;LET_DEF;LET_END_DEF;scs_basic;unadorned_v39]
 791 THEN SET_TAC[]);;
 792
 793 let WKEIDFT_concl = `!s a b a' b' p q p' q'.
 794     (let k = scs_k_v39 s in
 795        (is_scs_v39 s /\ scs_basic_v39 s /\
 796           (!i. scs_a_v39 s i (i + 1) = a) /\
 797           (!i. scs_b_v39 s i (i + 1) = b) /\
 798            p' + q = p + q' /\
 799          scs_diag k p q/\
 800          scs_diag k p' q'/\
 801     3 < k /\
 802            (!i j. scs_diag k i j ==> scs_a_v39 s i j <= cstab) /\
 803            (!i j. scs_diag k i j  ==> scs_a_v39 s i j = a') /\
 804            (!i j. scs_diag k i j  ==> scs_b_v39 s i j = b')/\
 805           (!i. scs_b_v39 s i i = b1) ==>
 806 scs_arrow_v39 {scs_stab_diag_v39 s p q} {scs_stab_diag_v39 s p' q'}))`;;
 807
 808
 809 let WKEIDFT=prove(WKEIDFT_concl,
 810 REWRITE_TAC[LET_DEF;LET_END_DEF]
 811 THEN REPEAT RESA_TAC
 812 THEN MP_TAC WKEIDFT_EQU_V2
 813 THEN REWRITE_TAC[LET_DEF;LET_END_DEF]
 814 THEN RESA_TAC
 815 THEN MATCH_MP_TAC YXIONXL3
 816 THEN ASM_REWRITE_TAC[]
 817 THEN MRESAS_TAC Yrtafyh.YRTAFYH[`s`;`p`;`q`][LET_DEF;LET_END_DEF;scs_basic;unadorned_v39;SCS_K_D_A_STAB_EQ]);;
 818
 819
 820
 821
 822
 823
 824  end;;
 825
 826
 827 (*
 828 let check_completeness_claimA_concl =
 829   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
 830 *)
 831
 832
 833
 834