text_formalization/local/CNICGSF.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 Cnicgsf = 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 open Nuxcoea;;
  87 open Aursipd;;
  88 open Cuxvzoz;;
  89 open Rrcwnsj;;
  90 open Tfitskc;;
  91 open Hexagons;;
  92 open Otmtotj;;
  93 open Hijqaha;;
  94
  95
  96
  97
  98 (*******************)
  99
 100 let SCS_DIAG_SCS_5I1_02=prove(`scs_diag (scs_k_v39 scs_5I1) 0 2`,
 101 REWRITE_TAC[K_SCS_5I1;scs_diag]
 102 THEN ARITH_TAC);;
 103
 104
 105
 106
 107
 108 let SCS_5I1_SLICE_02=prove_by_refinement(
 109 `scs_arrow_v39
 110 { scs_stab_diag_v39 scs_5I1 0 2}
 111 {scs_prop_equ_v39 scs_3M1 1,scs_prop_equ_v39 scs_4M2 1}`,
 112
 113 [MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
 114 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5I1_02;STAB_5I1_SCS;SCS_K_D_A_STAB_EQ;]
 115 THEN EXISTS_TAC`0`
 116 THEN EXISTS_TAC`2`
 117 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5I1_02]
 118 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
 119 THEN REPEAT RESA_TAC;
 120
 121 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
 122 THEN STRIP_TAC
 123 THEN MATCH_MP_TAC scs_inj
 124 THEN ASM_SIMP_TAC[SCS_5I1_BASIC;SCS_3M1_BASIC;J_SCS_4M2;BASIC_HALF_SLICE_STAB;J_SCS_3M1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4M2_BASIC]
 125 THEN STRIP_TAC;
 126
 127 ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5I1]
 128 THEN ARITH_TAC;
 129
 130 STRIP_TAC
 131 THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_5I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1;scs_3M1;scs_5M3;
 132 ARITH_RULE`(2 + 1 + 5 - 0) MOD 5= 3/\ 0 MOD 5=0/\ a+0=a`;scs_prop_equ_v39]
 133 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 134 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 135 THEN SCS_TAC
 136 THEN REPEAT GEN_TAC
 137 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
 138 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
 139 THEN RESA_TAC
 140 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
 141 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
 142 THEN RESA_TAC
 143 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 144 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
 145 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
 146 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
 147 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
 148 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
 149 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
 150 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
 151 THEN ASM_TAC
 152 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
 153 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
 154 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 155 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
 156 THEN REPEAT RESA_TAC
 157 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
 158 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
 159 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
 160 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
 161 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
 162 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
 163 THEN SYM_ASSUM_TAC
 164 THEN SCS_TAC;
 165
 166 ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_4M2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5I1]
 167 THEN ARITH_TAC;
 168
 169 STRIP_TAC
 170 THEN
 171 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_5I1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2;scs_3T4_prime;scs_5M3;
 172 ARITH_RULE`(0+1 + 5 - 2) MOD 5= 4/\ 2 MOD 5=2/\ a+0=a`;scs_prop_equ_v39]
 173 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 174 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 175 THEN SCS_TAC
 176 THEN REPEAT GEN_TAC
 177 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`)
 178 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION]
 179 THEN RESA_TAC
 180 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`)
 181 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
 182 THEN RESA_TAC
 183 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 184 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
 185 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
 186 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
 187 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
 188 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
 189 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
 190 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
 191 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
 192 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
 193 THEN ASM_TAC
 194 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
 195 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
 196 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 197 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
 198 THEN REPEAT RESA_TAC
 199 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
 200 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
 201 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
 202 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
 203 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
 204 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+x:num`;`1+x':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
 205 THEN SYM_ASSUM_TAC
 206 THEN SCS_TAC;
 207
 208 SCS_TAC
 209 THEN REAL_ARITH_TAC;
 210
 211 SCS_TAC
 212 THEN REAL_ARITH_TAC;
 213
 214 SCS_TAC
 215 THEN REAL_ARITH_TAC;
 216
 217 SCS_TAC
 218 THEN REWRITE_TAC[cstab]
 219 THEN REAL_ARITH_TAC;
 220
 221 SCS_TAC
 222 THEN REWRITE_TAC[cstab]
 223 THEN REAL_ARITH_TAC;
 224
 225 POP_ASSUM MP_TAC
 226 THEN REWRITE_TAC[J_SCS_3M1]]);;
 227
 228
 229 let CNICGSF1=prove(`scs_arrow_v39
 230 { scs_stab_diag_v39 scs_5I1 0 2}
 231 {scs_3M1, scs_4M2 }`,
 232 MATCH_MP_TAC FZIOTEF_TRANS
 233 THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_3M1 1, scs_prop_equ_v39 scs_4M2 1}`
 234 THEN ASM_REWRITE_TAC[SCS_5I1_SLICE_02;SET_RULE`{A,B}={A}UNION {B}`]
 235 THEN MATCH_MP_TAC FZIOTEF_UNION
 236 THEN STRIP_TAC
 237 THENL[
 238 MRESAS_TAC PRO_EQU_ID1[`scs_3M1`;`1`;`3`][SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`(3 - 1 MOD 3)=2`]
 239 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1 1`;`2`][PROP_EQU_IS_SCS;SCS_3M1_IS_SCS]
 240 THEN DICH_TAC 0
 241 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
 242 THEN REWRITE_TAC[];
 243
 244 MRESAS_TAC PRO_EQU_ID1[`scs_4M2`;`1`;`4`][SCS_4M2_IS_SCS;K_SCS_4M2;ARITH_RULE`(4 - 1 MOD 4)=3`]
 245 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M2 1`;`3`][PROP_EQU_IS_SCS;SCS_4M2_IS_SCS]
 246 THEN DICH_TAC 0
 247 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
 248 THEN REWRITE_TAC[]]);;
 249
 250
 251 (**************)
 252
 253 let SCS_DIAG_SCS_5I2_02=prove(`scs_diag (scs_k_v39 scs_5I2) 0 2`,
 254 REWRITE_TAC[K_SCS_5I2;scs_diag]
 255 THEN ARITH_TAC);;
 256
 257
 258
 259 let SCS_5I2_SLICE_02=prove_by_refinement(`scs_arrow_v39
 260 { scs_stab_diag_v39 scs_5I2 0 2}
 261 {scs_prop_equ_v39 scs_3T1 1,scs_prop_equ_v39 scs_4M3' 1}`,
 262 [
 263
 264 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
 265 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5I2_02;STAB_5I2_SCS;SCS_K_D_A_STAB_EQ;]
 266 THEN EXISTS_TAC`0`
 267 THEN EXISTS_TAC`2`
 268 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5I2_02]
 269 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
 270 THEN REPEAT RESA_TAC;
 271 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
 272 THEN STRIP_TAC
 273 THEN MATCH_MP_TAC scs_inj
 274 THEN ASM_SIMP_TAC[SCS_5I2_BASIC;SCS_3T1_BASIC;J_SCS_4M3;BASIC_HALF_SLICE_STAB;J_SCS_3T1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4M3_BASIC]
 275 THEN STRIP_TAC;
 276
 277
 278 ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5I2]
 279 THEN ARITH_TAC;
 280 STRIP_TAC
 281 THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_5I2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1;scs_3M1;scs_5M3;
 282 ARITH_RULE`(2 + 1 + 5 - 0) MOD 5= 3/\ 0 MOD 5=0/\ a+0=a`;scs_prop_equ_v39]
 283 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 284 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 285 THEN SCS_TAC
 286 THEN REPEAT GEN_TAC
 287 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
 288 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
 289 THEN RESA_TAC
 290 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
 291 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
 292 THEN RESA_TAC
 293 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 294 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
 295 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
 296 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
 297 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
 298 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
 299 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
 300 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
 301 THEN ASM_TAC
 302 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
 303 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
 304 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 305 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
 306 THEN REPEAT RESA_TAC
 307 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
 308 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
 309 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
 310 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
 311 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
 312 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
 313 THEN SYM_ASSUM_TAC
 314 THEN SCS_TAC;
 315
 316 ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_4M3;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5I2]
 317 THEN ARITH_TAC;
 318
 319
 320 STRIP_TAC
 321 THEN
 322 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_5I2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M3;
 323 ARITH_RULE`(0+1 + 5 - 2) MOD 5= 4/\ 2 MOD 5=2/\ a+0=a`;scs_prop_equ_v39]
 324 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 325 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 326 THEN SCS_TAC
 327 THEN REPEAT GEN_TAC
 328 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`)
 329 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION]
 330 THEN RESA_TAC
 331 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`)
 332 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
 333 THEN RESA_TAC
 334 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 335 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
 336 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
 337 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
 338 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
 339 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
 340 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
 341 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
 342 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
 343 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
 344 THEN ASM_TAC
 345 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
 346 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
 347 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 348 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
 349 THEN REPEAT RESA_TAC
 350 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
 351 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
 352 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
 353 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
 354 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
 355 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+x:num`;`1+x':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
 356 THEN SYM_ASSUM_TAC
 357 THEN SCS_TAC;
 358
 359 SCS_TAC
 360 THEN REAL_ARITH_TAC;
 361
 362 SCS_TAC
 363 THEN REAL_ARITH_TAC;
 364
 365 SCS_TAC
 366 THEN REAL_ARITH_TAC;
 367
 368 SCS_TAC
 369 THEN REWRITE_TAC[cstab]
 370 THEN REAL_ARITH_TAC;
 371
 372 SCS_TAC
 373 THEN REWRITE_TAC[cstab]
 374 THEN REAL_ARITH_TAC;
 375
 376 POP_ASSUM MP_TAC
 377 THEN REWRITE_TAC[J_SCS_3T1];
 378
 379 ]);;
 380
 381
 382
 383 let CNICGSF2=prove(`scs_arrow_v39
 384 { scs_stab_diag_v39 scs_5I2 0 2}
 385 {scs_3T1, scs_4M3' }`,
 386 MATCH_MP_TAC FZIOTEF_TRANS
 387 THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_3T1 1, scs_prop_equ_v39 scs_4M3' 1}`
 388 THEN ASM_REWRITE_TAC[SCS_5I2_SLICE_02;SET_RULE`{A,B}={A}UNION {B}`]
 389 THEN MATCH_MP_TAC FZIOTEF_UNION
 390 THEN STRIP_TAC
 391 THENL[
 392
 393 MRESAS_TAC PRO_EQU_ID1[`scs_3T1`;`1`;`3`][SCS_3T1_IS_SCS;K_SCS_3T1;ARITH_RULE`(3 - 1 MOD 3)=2`]
 394 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T1 1`;`2`][PROP_EQU_IS_SCS;SCS_3T1_IS_SCS]
 395 THEN DICH_TAC 0
 396 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
 397 THEN REWRITE_TAC[];
 398
 399 MRESAS_TAC PRO_EQU_ID1[`scs_4M3'`;`1`;`4`][SCS_4M3_IS_SCS;K_SCS_4M3;ARITH_RULE`(4 - 1 MOD 4)=3`]
 400 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M3' 1`;`3`][PROP_EQU_IS_SCS;SCS_4M3_IS_SCS]
 401 THEN DICH_TAC 0
 402 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
 403 THEN REWRITE_TAC[]]);;
 404
 405
 406
 407 (*****************************)
 408
 409 let SCS_DIAG_SCS_5M1_02=prove(`scs_diag (scs_k_v39 scs_5M1) 0 2`,
 410 REWRITE_TAC[K_SCS_5M1;scs_diag]
 411 THEN ARITH_TAC);;
 412
 413 let SCS_DIAG_SCS_5M1_03=prove(`scs_diag (scs_k_v39 scs_5M1) 0 3`,
 414 REWRITE_TAC[K_SCS_5M1;scs_diag]
 415 THEN ARITH_TAC);;
 416
 417 let SCS_DIAG_SCS_5M1_24=prove(`scs_diag (scs_k_v39 scs_5M1) 2 4`,
 418 REWRITE_TAC[K_SCS_5M1;scs_diag]
 419 THEN ARITH_TAC);;
 420
 421
 422 let SCS_5M1_SLICE_02=prove_by_refinement(
 423 `scs_arrow_v39
 424 { scs_stab_diag_v39 scs_5M1 0 2}
 425 {scs_prop_equ_v39 scs_3T4 2,scs_prop_equ_v39 scs_4M2 1}`,
 426
 427 [
 428
 429
 430 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
 431 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M1_02;STAB_5M1_SCS;SCS_K_D_A_STAB_EQ;]
 432 THEN EXISTS_TAC`0`
 433 THEN EXISTS_TAC`2`
 434 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M1_02]
 435 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
 436 THEN REPEAT RESA_TAC;
 437 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
 438 THEN STRIP_TAC
 439 THEN MATCH_MP_TAC scs_inj
 440 THEN ASM_SIMP_TAC[SCS_5M1_BASIC;SCS_3T4_BASIC;J_SCS_4M2;BASIC_HALF_SLICE_STAB;J_SCS_3T4;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4M2_BASIC]
 441 THEN STRIP_TAC;
 442
 443
 444 ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3T4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M1]
 445 THEN ARITH_TAC;
 446 STRIP_TAC
 447 THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_5M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3T4;scs_3M1;scs_5M3;
 448 ARITH_RULE`(2 + 1 + 5 - 0) MOD 5= 3/\ 0 MOD 5=0/\ a+0=a`;scs_prop_equ_v39]
 449 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 450 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 451 THEN SCS_TAC
 452 THEN REPEAT GEN_TAC
 453 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
 454 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
 455 THEN RESA_TAC
 456 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
 457 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
 458 THEN RESA_TAC
 459 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 460 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
 461 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`2`][ARITH_RULE`~(3=0)`]
 462 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`2`][ARITH_RULE`~(3=0)`]
 463 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`2`][ARITH_RULE`~(3=0)`]
 464 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`2`][ARITH_RULE`~(3=0)`]
 465 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`2`][ARITH_RULE`~(3=0)`]
 466 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`2`][ARITH_RULE`~(3=0)`]
 467 THEN ASM_TAC
 468 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
 469 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
 470 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 471 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
 472 THEN REPEAT RESA_TAC
 473 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
 474 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
 475 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
 476 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
 477 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
 478 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`2+x:num`;`2+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
 479 THEN SYM_ASSUM_TAC
 480 THEN SCS_TAC;
 481
 482 ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_4M2;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M1]
 483 THEN ARITH_TAC;
 484
 485
 486 STRIP_TAC
 487 THEN
 488 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_5M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M2;
 489 ARITH_RULE`(0+1 + 5 - 2) MOD 5= 4/\ 2 MOD 5=2/\ a+0=a`;scs_prop_equ_v39]
 490 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 491 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 492 THEN SCS_TAC
 493 THEN REPEAT GEN_TAC
 494 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`)
 495 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION]
 496 THEN RESA_TAC
 497 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`)
 498 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
 499 THEN RESA_TAC
 500 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 501 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
 502 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
 503 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
 504 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
 505 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
 506 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
 507 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
 508 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
 509 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
 510 THEN ASM_TAC
 511 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
 512 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
 513 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 514 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
 515 THEN REPEAT RESA_TAC
 516 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
 517 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
 518 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
 519 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
 520 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
 521 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+x:num`;`1+x':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1`]
 522 THEN SYM_ASSUM_TAC
 523 THEN SCS_TAC;
 524
 525 SCS_TAC
 526 THEN REAL_ARITH_TAC;
 527
 528 SCS_TAC
 529 THEN REAL_ARITH_TAC;
 530
 531 SCS_TAC
 532 THEN REAL_ARITH_TAC;
 533
 534 SCS_TAC
 535 THEN REWRITE_TAC[cstab]
 536 THEN REAL_ARITH_TAC;
 537
 538 SCS_TAC
 539 THEN REWRITE_TAC[cstab]
 540 THEN REAL_ARITH_TAC;
 541
 542 POP_ASSUM MP_TAC
 543 THEN REWRITE_TAC[J_SCS_3T4];
 544 ]);;
 545
 546
 547
 548
 549 let CNICGSF3=prove(`scs_arrow_v39
 550 { scs_stab_diag_v39 scs_5M1 0 2}
 551 {scs_3T4, scs_4M2 }`,
 552 MATCH_MP_TAC FZIOTEF_TRANS
 553 THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_3T4 2, scs_prop_equ_v39 scs_4M2 1}`
 554 THEN ASM_REWRITE_TAC[SCS_5M1_SLICE_02;SET_RULE`{A,B}={A}UNION {B}`]
 555 THEN MATCH_MP_TAC FZIOTEF_UNION
 556 THEN STRIP_TAC
 557 THENL[
 558
 559 MRESAS_TAC PRO_EQU_ID1[`scs_3T4`;`2`;`3`][SCS_3T4_IS_SCS;K_SCS_3T4;ARITH_RULE`(3 - 2 MOD 3)=1`]
 560 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3T4 2`;`1`][PROP_EQU_IS_SCS;SCS_3T4_IS_SCS]
 561 THEN DICH_TAC 0
 562 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
 563 THEN REWRITE_TAC[];
 564
 565 MRESAS_TAC PRO_EQU_ID1[`scs_4M2`;`1`;`4`][SCS_4M2_IS_SCS;K_SCS_4M2;ARITH_RULE`(4 - 1 MOD 4)=3`]
 566 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M2 1`;`3`][PROP_EQU_IS_SCS;SCS_4M2_IS_SCS]
 567 THEN DICH_TAC 0
 568 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
 569 THEN REWRITE_TAC[]]);;
 570
 571
 572 (********************)
 573
 574 let SCS_5M1_SLICE_03=prove_by_refinement(`scs_arrow_v39
 575 { scs_stab_diag_v39 scs_5M1 0 3}
 576 {scs_prop_equ_v39 scs_4M4' 1,scs_prop_equ_v39 scs_3M1 1}`,
 577 [
 578
 579 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
 580 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M1_03;STAB_5M1_SCS;SCS_K_D_A_STAB_EQ;]
 581 THEN EXISTS_TAC`0`
 582 THEN EXISTS_TAC`3`
 583 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M1_03]
 584 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
 585 THEN REPEAT RESA_TAC;
 586
 587
 588 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
 589 THEN STRIP_TAC
 590 THEN MATCH_MP_TAC scs_inj
 591 THEN ASM_SIMP_TAC[SCS_5M1_BASIC;SCS_3M1_BASIC;J_SCS_4M4;BASIC_HALF_SLICE_STAB;J_SCS_3M1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4M4_BASIC]
 592 THEN STRIP_TAC;
 593
 594
 595
 596 ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_4M4;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M1]
 597 THEN ARITH_TAC;
 598
 599
 600
 601
 602 STRIP_TAC
 603 THEN
 604 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_5M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4;
 605 ARITH_RULE`(3+1 + 5 - 0) MOD 5= 4/\ 0 MOD 5=0/\ a+0=a`;scs_prop_equ_v39]
 606 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 607 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 608 THEN SCS_TAC
 609 THEN REPEAT GEN_TAC
 610 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`)
 611 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION]
 612 THEN RESA_TAC
 613 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`)
 614 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
 615 THEN RESA_TAC
 616 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 617 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
 618 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
 619 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
 620 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
 621 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
 622 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
 623 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
 624 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
 625 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
 626 THEN ASM_TAC
 627 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
 628 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
 629 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 630 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
 631 THEN REPEAT RESA_TAC
 632 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
 633 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
 634 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
 635 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
 636 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
 637 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+x:num`;`1+x':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1/\ 3+1=4`]
 638 THEN SYM_ASSUM_TAC
 639 THEN SCS_TAC;
 640
 641
 642
 643 ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M1]
 644 THEN ARITH_TAC;
 645
 646
 647
 648
 649
 650 STRIP_TAC
 651 THEN ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_5M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1;scs_3M1;scs_5M3;
 652 ARITH_RULE`(0 + 1 + 5 - 3) MOD 5= 3/\ 3 MOD 5=3/\ a+0=a`;scs_prop_equ_v39]
 653 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 654 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 655 THEN SCS_TAC
 656 THEN REPEAT GEN_TAC
 657 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
 658 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
 659 THEN RESA_TAC
 660 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
 661 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
 662 THEN RESA_TAC
 663 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 664 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
 665 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
 666 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
 667 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
 668 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
 669 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
 670 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
 671 THEN ASM_TAC
 672 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
 673 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
 674 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 675 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
 676 THEN REPEAT RESA_TAC
 677 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
 678 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
 679 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
 680 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
 681 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
 682 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
 683 THEN SYM_ASSUM_TAC
 684 THEN SCS_TAC;
 685
 686
 687
 688
 689
 690 SCS_TAC
 691 THEN REAL_ARITH_TAC;
 692
 693
 694 SCS_TAC
 695 THEN REAL_ARITH_TAC;
 696
 697
 698 SCS_TAC
 699 THEN REAL_ARITH_TAC;
 700
 701 SCS_TAC
 702 THEN REWRITE_TAC[cstab]
 703 THEN REAL_ARITH_TAC;
 704
 705 SCS_TAC
 706 THEN REWRITE_TAC[cstab]
 707 THEN REAL_ARITH_TAC;
 708
 709 POP_ASSUM MP_TAC
 710 THEN REWRITE_TAC[J_SCS_4M4];
 711
 712 ]);;
 713
 714
 715
 716
 717
 718 let CNICGSF4=prove(`scs_arrow_v39
 719 { scs_stab_diag_v39 scs_5M1 0 3}
 720 {scs_4M4', scs_3M1 }`,
 721 MATCH_MP_TAC FZIOTEF_TRANS
 722 THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_4M4' 1, scs_prop_equ_v39 scs_3M1 1}`
 723 THEN ASM_REWRITE_TAC[SCS_5M1_SLICE_03;SET_RULE`{A,B}={A}UNION {B}`]
 724 THEN MATCH_MP_TAC FZIOTEF_UNION
 725 THEN STRIP_TAC
 726 THENL[
 727 MRESAS_TAC PRO_EQU_ID1[`scs_4M4'`;`1`;`4`][SCS_4M4_IS_SCS;K_SCS_4M4;ARITH_RULE`(4 - 1 MOD 4)=3`]
 728 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M4' 1`;`3`][PROP_EQU_IS_SCS;SCS_4M4_IS_SCS]
 729 THEN DICH_TAC 0
 730 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
 731 THEN REWRITE_TAC[];
 732
 733 MRESAS_TAC PRO_EQU_ID1[`scs_3M1`;`1`;`3`][SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`(3 - 1 MOD 3)=2`]
 734 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1 1`;`2`][PROP_EQU_IS_SCS;SCS_3M1_IS_SCS]
 735 THEN DICH_TAC 0
 736 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
 737 THEN REWRITE_TAC[];
 738 ]);;
 739
 740
 741
 742 (*****************************)
 743
 744
 745
 746
 747
 748
 749
 750
 751 let SCS_5M1_SLICE_24=prove_by_refinement(`scs_arrow_v39
 752 { scs_stab_diag_v39 scs_5M1 2 4}
 753 {scs_prop_equ_v39 scs_3M1 1,scs_prop_equ_v39 scs_4M5' 1}`,
 754 [
 755
 756 MATCH_MP_TAC (GEN_ALL Lkgrqui.LKGRQUI)
 757 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M1_24;STAB_5M1_SCS;SCS_K_D_A_STAB_EQ;]
 758 THEN EXISTS_TAC`2`
 759 THEN EXISTS_TAC`4`
 760 THEN ASM_SIMP_TAC[SCS_DIAG_SCS_5M1_24]
 761 THEN REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ]
 762 THEN REPEAT RESA_TAC;
 763
 764
 765
 766 REWRITE_TAC[is_scs_slice_v39;LET_DEF;LET_END_DEF;PAIR_EQ;scs_slice_v39;]
 767 THEN STRIP_TAC
 768 THEN MATCH_MP_TAC scs_inj
 769 THEN ASM_SIMP_TAC[SCS_5M1_BASIC;SCS_3M1_BASIC;J_SCS_4M5;BASIC_HALF_SLICE_STAB;J_SCS_3M1;D_HALF_SLICE;BAISC_PROP_EQU;K_SCS_PROP_EUQ;SCS_4M5_BASIC]
 770 THEN STRIP_TAC;
 771
 772
 773
 774
 775 ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_3M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M1]
 776 THEN ARITH_TAC;
 777
 778
 779
 780 STRIP_TAC
 781 THEN
 782 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_5M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_3M1;scs_3M1;scs_5M3;
 783 ARITH_RULE`(4 + 1 + 5 - 2) MOD 5= 3/\ 2 MOD 5=2/\ a+0=a`;scs_prop_equ_v39]
 784 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 785 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 786 THEN SCS_TAC
 787 THEN REPEAT GEN_TAC
 788 THEN MP_TAC(ARITH_RULE`x MOD 3<3==> x MOD 3=0\/ x MOD 3=1\/ x MOD 3=2`)
 789 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_3_TAC;DIVISION]
 790 THEN RESA_TAC
 791 THEN MP_TAC(ARITH_RULE`x' MOD 3<3==> x' MOD 3=0\/ x' MOD 3=1\/ x' MOD 3=2`)
 792 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
 793 THEN RESA_TAC
 794 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 795 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
 796 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`0`;`1`][ARITH_RULE`~(3=0)`]
 797 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`1`;`1`][ARITH_RULE`~(3=0)`]
 798 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x`;`2`;`1`][ARITH_RULE`~(3=0)`]
 799 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`0`;`1`][ARITH_RULE`~(3=0)`]
 800 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`1`;`1`][ARITH_RULE`~(3=0)`]
 801 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`3`;`x'`;`2`;`1`][ARITH_RULE`~(3=0)`]
 802 THEN ASM_TAC
 803 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
 804 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
 805 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 806 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
 807 THEN REPEAT RESA_TAC
 808 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
 809 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
 810 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
 811 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
 812 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC]
 813 THEN MRESAL_TAC Hexagons.PSORT_MOD[`3`;`1+x:num`;`1+x':num`][ARITH_RULE`~(3=0)/\ 2+1=3/\ 4 MOD 3=1`]
 814 THEN SYM_ASSUM_TAC
 815 THEN SCS_TAC;
 816
 817
 818 ASM_SIMP_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_4M5;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_5M1]
 819 THEN ARITH_TAC;
 820
 821
 822
 823
 824 STRIP_TAC
 825 THEN
 826 ASM_REWRITE_TAC[scs_half_slice_v39;mk_unadorned_v39;scs_v39_explicit;LET_DEF;LET_END_DEF;SCS_K_D_A_STAB_EQ;K_SCS_5M1;scs_basic;unadorned_v39;scs_stab_diag_v39;scs_stab_diag_v39;K_SCS_4M4;
 827 ARITH_RULE`(2+1 + 5 - 4) MOD 5= 4/\ 4 MOD 5=4/\ a+0=a`;scs_prop_equ_v39]
 828 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 829 THEN ONCE_REWRITE_TAC[FUN_EQ_THM]
 830 THEN SCS_TAC
 831 THEN REPEAT GEN_TAC
 832 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`)
 833 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION]
 834 THEN RESA_TAC
 835 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`)
 836 THEN ASM_SIMP_TAC[Uxckfpe.ARITH_4_TAC;DIVISION;ARITH_RULE`4-1=3`]
 837 THEN RESA_TAC
 838 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 839 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_3_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT;PSORT_5_EXPLICIT;Terminal.FUNLIST_EXPLICIT]
 840 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`0`;`1`][ARITH_RULE`~(4=0)`]
 841 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`1`;`1`][ARITH_RULE`~(4=0)`]
 842 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`2`;`1`][ARITH_RULE`~(4=0)`]
 843 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x`;`3`;`1`][ARITH_RULE`~(4=0)`]
 844 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`0`;`1`][ARITH_RULE`~(4=0)`]
 845 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`1`;`1`][ARITH_RULE`~(4=0)`]
 846 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`2`;`1`][ARITH_RULE`~(4=0)`]
 847 THEN MRESAL_TAC Ocbicby.MOD_EQ_MOD_SHIFT[`4`;`x'`;`3`;`1`][ARITH_RULE`~(4=0)`]
 848 THEN ASM_TAC
 849 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\1+4=5/\ 1<=5/\
 850 2<=3/\ 0+a=a`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
 851 THEN ASM_REWRITE_TAC[SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\
 852 b=c)`;ASSOCD_v39;MAP;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC;PAIR_EQ;Ocbicby.MOD_EQ_MOD_SHIFT]
 853 THEN REPEAT RESA_TAC
 854 THEN ASM_REWRITE_TAC[ARITH_RULE`1+1=2/\ 1+2=3/\ ~(1<=0)/\ ~(2<=1)/\ ~(2<=0) /\ 0<=1/\ 0<=2/\ 2<=2/\ 0<=3/\2+2=4/\ 3+2=5/\4+2=6/\ 5+2=7/\ 1<=2/\2<=3/\ ~(3<=1)
 855 /\ ~(4<=0)/\ ~(4<=3)/\ ~(4<=2)/\ ~(4<=1)/\ ~(3<=0) /\ ~(3<=2)/\0+a=a/\a<=a
 856 /\ ~(5<=0)/\ ~(5<=1)/\ ~(5<=4)/\ ~(5<=3)/\ ~(5<=2) /\ 2+1=3
 857 /\ 0<=5/\ 1<=5/\ 2<=5/\ 3<=5/\ 4<=5/\ ~(0=2)/\
 858 3+3=6/\ 2+3=5 /\ 0<=4`;PAIR_EQ;Uxckfpe.ARITH_4_TAC;Uxckfpe.ARITH_6_TAC]
 859 THEN MRESAL_TAC Hexagons.PSORT_MOD[`4`;`1+x:num`;`1+x':num`][ARITH_RULE`~(4=0)/\ 2+1=3/\ 4 MOD 3=1/\ 2+4=6/\ 3+4=7/\ 7 MOD 5=2`]
 860 THEN SYM_ASSUM_TAC
 861 THEN SCS_TAC;
 862
 863
 864
 865 SCS_TAC
 866 THEN REAL_ARITH_TAC;
 867
 868
 869
 870 SCS_TAC
 871 THEN REAL_ARITH_TAC;
 872
 873
 874
 875 SCS_TAC
 876 THEN REAL_ARITH_TAC;
 877
 878
 879 SCS_TAC
 880 THEN REWRITE_TAC[cstab]
 881 THEN REAL_ARITH_TAC;
 882
 883
 884 SCS_TAC
 885 THEN REWRITE_TAC[cstab]
 886 THEN REAL_ARITH_TAC;
 887
 888
 889 POP_ASSUM MP_TAC
 890 THEN REWRITE_TAC[J_SCS_3M1];
 891
 892 ]);;
 893
 894
 895
 896
 897
 898 let CNICGSF5=prove(`scs_arrow_v39
 899 { scs_stab_diag_v39 scs_5M1 2 4}
 900 { scs_3M1, scs_4M5' }`,
 901 MATCH_MP_TAC FZIOTEF_TRANS
 902 THEN EXISTS_TAC`{ scs_prop_equ_v39 scs_3M1 1,scs_prop_equ_v39 scs_4M5' 1}`
 903 THEN ASM_REWRITE_TAC[SCS_5M1_SLICE_24;SET_RULE`{A,B}={A}UNION {B}`]
 904 THEN MATCH_MP_TAC FZIOTEF_UNION
 905 THEN STRIP_TAC
 906 THENL[
 907 MRESAS_TAC PRO_EQU_ID1[`scs_3M1`;`1`;`3`][SCS_3M1_IS_SCS;K_SCS_3M1;ARITH_RULE`(3 - 1 MOD 3)=2`]
 908 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_3M1 1`;`2`][PROP_EQU_IS_SCS;SCS_3M1_IS_SCS]
 909 THEN DICH_TAC 0
 910 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
 911 THEN REWRITE_TAC[];
 912
 913 MRESAS_TAC PRO_EQU_ID1[`scs_4M5'`;`1`;`4`][SCS_4M5_IS_SCS;K_SCS_4M5;ARITH_RULE`(4 - 1 MOD 4)=3`]
 914 THEN MRESAS_TAC YXIONXL3[`scs_prop_equ_v39 scs_4M5' 1`;`3`][PROP_EQU_IS_SCS;SCS_4M5_IS_SCS]
 915 THEN DICH_TAC 0
 916 THEN POP_ASSUM (fun th-> ONCE_REWRITE_TAC[SYM th])
 917 THEN REWRITE_TAC[];]);;
 918
 919
 920  end;;
 921
 922
 923 (*
 924 let check_completeness_claimA_concl =
 925   Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)
 926 *)
 927
 928
 929
 930