1 import Base 2 import lawful-words@0.1.0.0/defs.bend as W 3 import lawful-words@0.1.0.0/proof_nat.bend as N 4 import lawful-words@0.1.0.0/proof_u32.bend as U 5 import lawful-words@0.1.0.0/proof_bytes.bend as Y 6 import lawful-words@0.1.0.0/proof_zb.bend as Z 7 import lawful-arrays@0.1.0.0/proof_base.bend as AB 8 import ./fast.bend as FA 9 10 # Or, the broadcast byte, the bytes of the masked first word, and the tables 11 # that turn the per-byte tests into places (4 Bools per word, checked case by 12 # case). 13 14 # Or and the zero test 15 # ==================== 16 17 law allz_orm: 18 for +n: Nat 19 for +x: Word(n) 20 for +y: Word(n) 21 for +z: Word(n) 22 {Z.allz(n, Word.and(n, Word.or(n, x, y), z)) == Bool.and(Z.allz(n, Word.and(n, x, z)), Z.allz(n, Word.and(n, y, z))) : Bool} 23 24 def allz_orm(n, x, y, z): 25 match n: 26 case 0n: 27 {==} 28 case 1n+p: 29 match x y z: 30 case WCon{False{}, +xt} WCon{False{}, +yt} WCon{False{}, +zt}: 31 allz_orm(p, xt, yt, zt) 32 case WCon{False{}, +xt} WCon{False{}, +yt} WCon{True{}, +zt}: 33 allz_orm(p, xt, yt, zt) 34 case WCon{False{}, +xt} WCon{True{}, +yt} WCon{False{}, +zt}: 35 allz_orm(p, xt, yt, zt) 36 case WCon{False{}, +xt} WCon{True{}, +yt} WCon{True{}, +zt}: 37 Equal.sym(Bool, Bool.and(Z.allz(p, Word.and(p, xt, zt)), False{}), False{}, N.and_false_r(Z.allz(p, Word.and(p, xt, zt)))) 38 case WCon{True{}, +xt} WCon{False{}, +yt} WCon{False{}, +zt}: 39 allz_orm(p, xt, yt, zt) 40 case WCon{True{}, +xt} WCon{False{}, +yt} WCon{True{}, +zt}: 41 {==} 42 case WCon{True{}, +xt} WCon{True{}, +yt} WCon{False{}, +zt}: 43 allz_orm(p, xt, yt, zt) 44 case WCon{True{}, +xt} WCon{True{}, +yt} WCon{True{}, +zt}: 45 {==} 46 47 law allz_or: 48 for +n: Nat 49 for +x: Word(n) 50 for +y: Word(n) 51 {Z.allz(n, Word.or(n, x, y)) == Bool.and(Z.allz(n, x), Z.allz(n, y)) : Bool} 52 53 def allz_or(n, x, y): 54 match n: 55 case 0n: 56 {==} 57 case 1n+p: 58 match x y: 59 case WCon{False{}, +xt} WCon{False{}, +yt}: 60 allz_or(p, xt, yt) 61 case WCon{False{}, +xt} WCon{True{}, +yt}: 62 Equal.sym(Bool, Bool.and(Z.allz(p, xt), False{}), False{}, N.and_false_r(Z.allz(p, xt))) 63 case WCon{True{}, +xt} WCon{+b, +yt}: 64 {==} 65 66 law iz: 67 for +w: Word(32n) 68 {U32.is_zero(U32{w}) == Z.allz(32n, w) : Bool} 69 70 def iz(w): 71 Z.allz_cmp(32n, w) 72 73 law uorm: 74 for +a: U32 75 for +b: U32 76 for +h: U32 77 {U32.is_zero(U32.and(U32.or(a, b), h)) == Bool.and(U32.is_zero(U32.and(a, h)), U32.is_zero(U32.and(b, h))) : Bool} 78 79 def uorm(a, b, h): 80 match a b h: 81 case U32{+x} U32{+y} U32{+z}: 82 %Equal.sym(Bool, U32.is_zero(U32{Word.and(32n, x, z)}), Z.allz(32n, Word.and(32n, x, z)), iz(Word.and(32n, x, z))) : 83 {U32.is_zero(U32{Word.and(32n, Word.or(32n, x, y), z)}) == Bool.and(_, U32.is_zero(U32{Word.and(32n, y, z)})) : Bool} 84 %Equal.sym(Bool, U32.is_zero(U32{Word.and(32n, y, z)}), Z.allz(32n, Word.and(32n, y, z)), iz(Word.and(32n, y, z))) : 85 {U32.is_zero(U32{Word.and(32n, Word.or(32n, x, y), z)}) == Bool.and(Z.allz(32n, Word.and(32n, x, z)), _) : Bool} 86 Equal.trans(Bool, U32.is_zero(U32{Word.and(32n, Word.or(32n, x, y), z)}), Z.allz(32n, Word.and(32n, Word.or(32n, x, y), z)), 87 Bool.and(Z.allz(32n, Word.and(32n, x, z)), Z.allz(32n, Word.and(32n, y, z))), 88 iz(Word.and(32n, Word.or(32n, x, y), z)), allz_orm(32n, x, y, z)) 89 90 law uor0: 91 for +a: U32 92 for +b: U32 93 {U32.is_zero(U32.or(a, b)) == Bool.and(U32.is_zero(a), U32.is_zero(b)) : Bool} 94 95 def uor0(a, b): 96 match a b: 97 case U32{+x} U32{+y}: 98 %Equal.sym(Bool, U32.is_zero(U32{x}), Z.allz(32n, x), iz(x)) : 99 {U32.is_zero(U32{Word.or(32n, x, y)}) == Bool.and(_, U32.is_zero(U32{y})) : Bool} 100 %Equal.sym(Bool, U32.is_zero(U32{y}), Z.allz(32n, y), iz(y)) : 101 {U32.is_zero(U32{Word.or(32n, x, y)}) == Bool.and(Z.allz(32n, x), _) : Bool} 102 Equal.trans(Bool, U32.is_zero(U32{Word.or(32n, x, y)}), Z.allz(32n, Word.or(32n, x, y)), Bool.and(Z.allz(32n, x), Z.allz(32n, y)), 103 iz(Word.or(32n, x, y)), allz_or(32n, x, y)) 104 105 def or_false(-p: Nat, +b: Bool, +t: Word(p)) -> {WCon{Bool.or(b, False{}), t} == WCon{b, t} : Word(1n+p)}: 106 match b: 107 case False{}: 108 {==} 109 case True{}: 110 {==} 111 112 law wor0: 113 for +n: Nat 114 for +x: Word(n) 115 {Word.or(n, x, Word.zero(n)) == x : Word(n)} 116 117 def wor0(n, x): 118 match n: 119 case 0n: 120 match x: 121 case WNil{}: 122 {==} 123 case 1n+p: 124 match x: 125 case WCon{+b, +t}: 126 %Equal.sym(Word(p), Word.or(p, t, Word.zero(p)), t, wor0(p, t)) : {WCon{Bool.or(b, False{}), _} == WCon{b, t} : Word(1n+p)} 127 or_false(p, b, t) 128 129 law or0r: 130 for +y: U32 131 {U32.or(y, 0) == y : U32} 132 133 def or0r(y): 134 match y: 135 case U32{+x}: 136 %Equal.sym(Word(32n), Word.or(32n, x, Word.zero(32n)), x, wor0(32n, x)) : {U32{_} == U32{x} : U32} 137 {==} 138 139 law or255: 140 for +y: U32 141 {U32.is_eq(U32.or(y, 255), 0) == False{} : Bool} 142 143 def or255(y): 144 Equal.trans(Bool, U32.is_zero(U32.or(y, 255)), Bool.and(U32.is_zero(y), False{}), False{}, uor0(y, 255), N.and_false_r(U32.is_zero(y))) 145 146 # The broadcast byte 147 # ================== 148 149 law nth4_same: 150 for +j: Nat 151 for +c: U32 152 {W.nth4(j, c, c, c, c) == c : U32} 153 154 def nth4_same(j, c): 155 match j: 156 case 0n: 157 {==} 158 case 1n+p: 159 match p: 160 case 0n: 161 {==} 162 case 1n+q: 163 match q: 164 case 0n: 165 {==} 166 case 1n+r: 167 {==} 168 169 law nk: 170 for +x: Nat 171 for +A: Nat 172 for +B: Nat 173 for +E: Nat 174 {Nat.mul(x, Nat.add(1n, Nat.add(Nat.mul(1n, A), Nat.add(Nat.mul(1n, B), Nat.mul(1n, E))))) == Nat.add(x, Nat.add(Nat.mul(x, A), Nat.add(Nat.mul(x, B), Nat.mul(x, E)))) : Nat} 175 176 def nk(x, A, B, E): 177 +RHS = Nat.add(x, Nat.add(Nat.mul(x, A), Nat.add(Nat.mul(x, B), Nat.mul(x, E)))) 178 %Equal.sym(Nat, Nat.add(A, 0n), A, N.add_zero(A)) : 179 {Nat.mul(x, Nat.add(1n, Nat.add(_, Nat.add(Nat.mul(1n, B), Nat.mul(1n, E))))) == RHS : Nat} 180 %Equal.sym(Nat, Nat.add(B, 0n), B, N.add_zero(B)) : 181 {Nat.mul(x, Nat.add(1n, Nat.add(A, Nat.add(_, Nat.mul(1n, E))))) == RHS : Nat} 182 %Equal.sym(Nat, Nat.add(E, 0n), E, N.add_zero(E)) : 183 {Nat.mul(x, Nat.add(1n, Nat.add(A, Nat.add(B, _)))) == RHS : Nat} 184 %Equal.sym(Nat, Nat.mul(x, Nat.add(1n, Nat.add(A, Nat.add(B, E)))), Nat.add(Nat.mul(x, 1n), Nat.mul(x, Nat.add(A, Nat.add(B, E)))), N.mul_add(x, 1n, Nat.add(A, Nat.add(B, E)))) : {_ == RHS : Nat} 185 %Equal.sym(Nat, Nat.mul(x, 1n), x, N.mul_one(x)) : {Nat.add(_, Nat.mul(x, Nat.add(A, Nat.add(B, E)))) == RHS : Nat} 186 %Equal.sym(Nat, Nat.mul(x, Nat.add(A, Nat.add(B, E))), Nat.add(Nat.mul(x, A), Nat.mul(x, Nat.add(B, E))), N.mul_add(x, A, Nat.add(B, E))) : {Nat.add(x, _) == RHS : Nat} 187 %Equal.sym(Nat, Nat.mul(x, Nat.add(B, E)), Nat.add(Nat.mul(x, B), Nat.mul(x, E)), N.mul_add(x, B, E)) : {Nat.add(x, Nat.add(Nat.mul(x, A), _)) == RHS : Nat} 188 {==} 189 190 # rep(c) == pack4(c, c, c, c), as numbers with 2^32, 2^8, 2^16, 2^24 abstract. 191 law rg: 192 for +c: U32 193 for +M: Nat 194 for +A: Nat 195 for +B: Nat 196 for +E: Nat 197 for +h1: {U32.to_nat(U32.mul(c, W.pack4(1, 1, 1, 1))) == Nat.mod(Nat.mul(U32.to_nat(c), U32.to_nat(W.pack4(1, 1, 1, 1))), M) : Nat} 198 for +h2: {U32.to_nat(W.pack4(1, 1, 1, 1)) == Nat.add(U32.to_nat(1), Nat.add(Nat.mul(U32.to_nat(1), A), Nat.add(Nat.mul(U32.to_nat(1), B), Nat.mul(U32.to_nat(1), E)))) : Nat} 199 for +h3: {U32.to_nat(W.pack4(c, c, c, c)) == Nat.add(U32.to_nat(c), Nat.add(Nat.mul(U32.to_nat(c), A), Nat.add(Nat.mul(U32.to_nat(c), B), Nat.mul(U32.to_nat(c), E)))) : Nat} 200 for +h4: {Nat.is_lt(U32.to_nat(W.pack4(c, c, c, c)), M) == True{} : Bool} 201 {U32.to_nat(U32.mul(c, W.pack4(1, 1, 1, 1))) == U32.to_nat(W.pack4(c, c, c, c)) : Nat} 202 203 def rg(c, M, A, B, E, h1, h2, h3, h4): 204 +x = U32.to_nat(c) 205 +P = U32.to_nat(W.pack4(c, c, c, c)) 206 +KX = Nat.add(U32.to_nat(1), Nat.add(Nat.mul(U32.to_nat(1), A), Nat.add(Nat.mul(U32.to_nat(1), B), Nat.mul(U32.to_nat(1), E)))) 207 +PX = Nat.add(x, Nat.add(Nat.mul(x, A), Nat.add(Nat.mul(x, B), Nat.mul(x, E)))) 208 %Equal.sym(Nat, U32.to_nat(U32.mul(c, W.pack4(1, 1, 1, 1))), Nat.mod(Nat.mul(x, U32.to_nat(W.pack4(1, 1, 1, 1))), M), h1) : {_ == P : Nat} 209 %Equal.sym(Nat, U32.to_nat(W.pack4(1, 1, 1, 1)), KX, h2) : {Nat.mod(Nat.mul(x, _), M) == P : Nat} 210 %Equal.sym(Nat, Nat.mul(x, KX), PX, nk(x, A, B, E)) : {Nat.mod(_, M) == P : Nat} 211 %h3 : {Nat.mod(_, M) == P : Nat} 212 N.mod_small(P, M, h4) 213 214 law rep_pack: 215 for +c: U32 216 for +hc: {U32.is_lt(c, 256) == True{} : Bool} 217 {FA.rep(c) == W.pack4(c, c, c, c) : U32} 218 219 def rep_pack(c, hc): 220 U.to_nat_inj(FA.rep(c), W.pack4(c, c, c, c), 221 rg(c, Nat.pow(2n, 32n), Nat.pow(2n, 8n), Nat.pow(2n, 16n), Nat.pow(2n, 24n), U.to_nat_mul_p(c, W.pack4(1, 1, 1, 1)), 222 Y.to_nat_pack4(1, 1, 1, 1, {==}, {==}, {==}, {==}), Y.to_nat_pack4(c, c, c, c, hc, hc, hc, hc), U.to_nat_lt_p(W.pack4(c, c, c, c)))) 223 224 law rep_byte: 225 for +c: U32 226 for +j: Nat 227 for +hc: {U32.is_lt(c, 256) == True{} : Bool} 228 for +hj: {Nat.is_lt(j, 4n) == True{} : Bool} 229 {W.byte(FA.rep(c), j) == c : U32} 230 231 def rep_byte(c, j, hc, hj): 232 %Equal.sym(U32, FA.rep(c), W.pack4(c, c, c, c), rep_pack(c, hc)) : {W.byte(_, j) == c : U32} 233 Equal.trans(U32, W.byte(W.pack4(c, c, c, c), j), W.nth4(j, c, c, c, c), c, Y.byte_pack4(c, c, c, c, j, hc, hc, hc, hc, hj), nth4_same(j, c)) 234 235 # The byte tests of the searched words 236 # ==================================== 237 238 law ej_xor: 239 for +w: U32 240 for +c: U32 241 for +j: Nat 242 for +hc: {U32.is_lt(c, 256) == True{} : Bool} 243 for +hj: {Nat.is_lt(j, 4n) == True{} : Bool} 244 {U32.is_eq(W.byte(U32.xor(w, FA.rep(c)), j), 0) == U32.is_eq(W.byte(w, j), c) : Bool} 245 246 def ej_xor(w, c, j, hc, hj): 247 +RHS = U32.is_eq(W.byte(w, j), c) 248 %Equal.sym(U32, W.byte(U32.xor(w, FA.rep(c)), j), U32.xor(W.byte(w, j), W.byte(FA.rep(c), j)), Y.byte_xor(w, FA.rep(c), j)) : 249 {U32.is_eq(_, 0) == RHS : Bool} 250 %Equal.sym(U32, W.byte(FA.rep(c), j), c, rep_byte(c, j, hc, hj)) : {U32.is_eq(U32.xor(W.byte(w, j), _), 0) == RHS : Bool} 251 U.is_zero_xor(W.byte(w, j), c) 252 253 # A byte of the first word at or above the start: the test of c. 254 law e_hi: 255 for +w: U32 256 for +c: U32 257 for +m: U32 258 for +j: Nat 259 for +hc: {U32.is_lt(c, 256) == True{} : Bool} 260 for +hj: {Nat.is_lt(j, 4n) == True{} : Bool} 261 for +hm: {W.byte(m, j) == 0 : U32} 262 {U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), m), j), 0) == U32.is_eq(W.byte(w, j), c) : Bool} 263 264 def e_hi(w, c, m, j, hc, hj, hm): 265 +X = U32.xor(w, FA.rep(c)) 266 +RHS = U32.is_eq(W.byte(w, j), c) 267 %Equal.sym(U32, W.byte(U32.or(X, m), j), U32.or(W.byte(X, j), W.byte(m, j)), Y.byte_or(X, m, j)) : {U32.is_eq(_, 0) == RHS : Bool} 268 %Equal.sym(U32, W.byte(m, j), 0, hm) : {U32.is_eq(U32.or(W.byte(X, j), _), 0) == RHS : Bool} 269 %Equal.sym(U32, U32.or(W.byte(X, j), 0), W.byte(X, j), or0r(W.byte(X, j))) : {U32.is_eq(_, 0) == RHS : Bool} 270 ej_xor(w, c, j, hc, hj) 271 272 # A byte below the start: set to 0xFF, never zero. 273 law e_lo: 274 for +w: U32 275 for +c: U32 276 for +m: U32 277 for +j: Nat 278 for +hm: {W.byte(m, j) == 255 : U32} 279 {U32.is_eq(W.byte(U32.or(U32.xor(w, FA.rep(c)), m), j), 0) == False{} : Bool} 280 281 def e_lo(w, c, m, j, hm): 282 +X = U32.xor(w, FA.rep(c)) 283 %Equal.sym(U32, W.byte(U32.or(X, m), j), U32.or(W.byte(X, j), W.byte(m, j)), Y.byte_or(X, m, j)) : {U32.is_eq(_, 0) == False{} : Bool} 284 %Equal.sym(U32, W.byte(m, j), 255, hm) : {U32.is_eq(U32.or(W.byte(X, j), _), 0) == False{} : Bool} 285 or255(W.byte(X, j)) 286 287 # Tables 288 # ====== 289 290 # run_len over the four byte tests of a word. 291 def R4(e0: Bool, e1: Bool, e2: Bool, e3: Bool) -> Nat: 292 Bool.pick(Nat, e0, 0n, Nat.add(1n, Bool.pick(Nat, e1, 0n, Nat.add(1n, Bool.pick(Nat, e2, 0n, Nat.add(1n, Bool.pick(Nat, e3, 0n, Nat.add(1n, 0n)))))))) 293 294 law bt_none: 295 for +e0: Bool 296 for +e1: Bool 297 for +e2: Bool 298 for +e3: Bool 299 {Bool.and(Bool.not(e0), Bool.and(Bool.not(e1), Bool.and(Bool.not(e2), Bool.not(e3)))) == Nat.is_eq(R4(e0, e1, e2, e3), 4n) : Bool} 300 301 def bt_none(e0, e1, e2, e3): 302 match e0 e1 e2 e3: 303 case False{} False{} False{} False{}: 304 {==} 305 case False{} False{} False{} True{}: 306 {==} 307 case False{} False{} True{} False{}: 308 {==} 309 case False{} False{} True{} True{}: 310 {==} 311 case False{} True{} False{} False{}: 312 {==} 313 case False{} True{} False{} True{}: 314 {==} 315 case False{} True{} True{} False{}: 316 {==} 317 case False{} True{} True{} True{}: 318 {==} 319 case True{} False{} False{} False{}: 320 {==} 321 case True{} False{} False{} True{}: 322 {==} 323 case True{} False{} True{} False{}: 324 {==} 325 case True{} False{} True{} True{}: 326 {==} 327 case True{} True{} False{} False{}: 328 {==} 329 case True{} True{} False{} True{}: 330 {==} 331 case True{} True{} True{} False{}: 332 {==} 333 case True{} True{} True{} True{}: 334 {==} 335 336 law bt_bidx: 337 for +e0: Bool 338 for +e1: Bool 339 for +e2: Bool 340 for +e3: Bool 341 for +h: {Nat.is_lt(R4(e0, e1, e2, e3), 4n) == True{} : Bool} 342 {U32.to_nat(U32.add(U32.add(FA.b2u(Bool.and(Bool.not(e0), True{})), FA.b2u(Bool.and(Bool.not(e0), Bool.and(Bool.not(e1), True{})))), FA.b2u(Bool.and(Bool.not(e0), Bool.and(Bool.not(e1), Bool.and(Bool.not(e2), True{})))))) == R4(e0, e1, e2, e3) : Nat} 343 344 def bt_bidx(e0, e1, e2, e3, h): 345 match e0 e1 e2 e3: 346 case False{} False{} False{} False{}: 347 Empty.absurd({U32.to_nat(U32.add(U32.add(FA.b2u(Bool.and(Bool.not(False{}), True{})), FA.b2u(Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), True{})))), FA.b2u(Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), True{})))))) == R4(False{}, False{}, False{}, False{}) : Nat}, AB.false_ne_true(h)) 348 case False{} False{} False{} True{}: 349 {==} 350 case False{} False{} True{} False{}: 351 {==} 352 case False{} False{} True{} True{}: 353 {==} 354 case False{} True{} False{} False{}: 355 {==} 356 case False{} True{} False{} True{}: 357 {==} 358 case False{} True{} True{} False{}: 359 {==} 360 case False{} True{} True{} True{}: 361 {==} 362 case True{} False{} False{} False{}: 363 {==} 364 case True{} False{} False{} True{}: 365 {==} 366 case True{} False{} True{} False{}: 367 {==} 368 case True{} False{} True{} True{}: 369 {==} 370 case True{} True{} False{} False{}: 371 {==} 372 case True{} True{} False{} True{}: 373 {==} 374 case True{} True{} True{} False{}: 375 {==} 376 case True{} True{} True{} True{}: 377 {==} 378 379 law bt2_none: 380 for +e0: Bool 381 for +e1: Bool 382 for +e2: Bool 383 for +e3: Bool 384 for +f0: Bool 385 for +f1: Bool 386 for +f2: Bool 387 for +f3: Bool 388 {Bool.and(Bool.and(Bool.not(e0), Bool.and(Bool.not(e1), Bool.and(Bool.not(e2), Bool.not(e3)))), Bool.and(Bool.not(f0), Bool.and(Bool.not(f1), Bool.and(Bool.not(f2), Bool.not(f3))))) == Nat.is_eq(Nat.min(R4(e0, e1, e2, e3), R4(f0, f1, f2, f3)), 4n) : Bool} 389 390 def bt2_none(e0, e1, e2, e3, f0, f1, f2, f3): 391 match e0 e1 e2 e3 f0 f1 f2 f3: 392 case False{} False{} False{} False{} False{} False{} False{} False{}: 393 {==} 394 case False{} False{} False{} False{} False{} False{} False{} True{}: 395 {==} 396 case False{} False{} False{} False{} False{} False{} True{} False{}: 397 {==} 398 case False{} False{} False{} False{} False{} False{} True{} True{}: 399 {==} 400 case False{} False{} False{} False{} False{} True{} False{} False{}: 401 {==} 402 case False{} False{} False{} False{} False{} True{} False{} True{}: 403 {==} 404 case False{} False{} False{} False{} False{} True{} True{} False{}: 405 {==} 406 case False{} False{} False{} False{} False{} True{} True{} True{}: 407 {==} 408 case False{} False{} False{} False{} True{} False{} False{} False{}: 409 {==} 410 case False{} False{} False{} False{} True{} False{} False{} True{}: 411 {==} 412 case False{} False{} False{} False{} True{} False{} True{} False{}: 413 {==} 414 case False{} False{} False{} False{} True{} False{} True{} True{}: 415 {==} 416 case False{} False{} False{} False{} True{} True{} False{} False{}: 417 {==} 418 case False{} False{} False{} False{} True{} True{} False{} True{}: 419 {==} 420 case False{} False{} False{} False{} True{} True{} True{} False{}: 421 {==} 422 case False{} False{} False{} False{} True{} True{} True{} True{}: 423 {==} 424 case False{} False{} False{} True{} False{} False{} False{} False{}: 425 {==} 426 case False{} False{} False{} True{} False{} False{} False{} True{}: 427 {==} 428 case False{} False{} False{} True{} False{} False{} True{} False{}: 429 {==} 430 case False{} False{} False{} True{} False{} False{} True{} True{}: 431 {==} 432 case False{} False{} False{} True{} False{} True{} False{} False{}: 433 {==} 434 case False{} False{} False{} True{} False{} True{} False{} True{}: 435 {==} 436 case False{} False{} False{} True{} False{} True{} True{} False{}: 437 {==} 438 case False{} False{} False{} True{} False{} True{} True{} True{}: 439 {==} 440 case False{} False{} False{} True{} True{} False{} False{} False{}: 441 {==} 442 case False{} False{} False{} True{} True{} False{} False{} True{}: 443 {==} 444 case False{} False{} False{} True{} True{} False{} True{} False{}: 445 {==} 446 case False{} False{} False{} True{} True{} False{} True{} True{}: 447 {==} 448 case False{} False{} False{} True{} True{} True{} False{} False{}: 449 {==} 450 case False{} False{} False{} True{} True{} True{} False{} True{}: 451 {==} 452 case False{} False{} False{} True{} True{} True{} True{} False{}: 453 {==} 454 case False{} False{} False{} True{} True{} True{} True{} True{}: 455 {==} 456 case False{} False{} True{} False{} False{} False{} False{} False{}: 457 {==} 458 case False{} False{} True{} False{} False{} False{} False{} True{}: 459 {==} 460 case False{} False{} True{} False{} False{} False{} True{} False{}: 461 {==} 462 case False{} False{} True{} False{} False{} False{} True{} True{}: 463 {==} 464 case False{} False{} True{} False{} False{} True{} False{} False{}: 465 {==} 466 case False{} False{} True{} False{} False{} True{} False{} True{}: 467 {==} 468 case False{} False{} True{} False{} False{} True{} True{} False{}: 469 {==} 470 case False{} False{} True{} False{} False{} True{} True{} True{}: 471 {==} 472 case False{} False{} True{} False{} True{} False{} False{} False{}: 473 {==} 474 case False{} False{} True{} False{} True{} False{} False{} True{}: 475 {==} 476 case False{} False{} True{} False{} True{} False{} True{} False{}: 477 {==} 478 case False{} False{} True{} False{} True{} False{} True{} True{}: 479 {==} 480 case False{} False{} True{} False{} True{} True{} False{} False{}: 481 {==} 482 case False{} False{} True{} False{} True{} True{} False{} True{}: 483 {==} 484 case False{} False{} True{} False{} True{} True{} True{} False{}: 485 {==} 486 case False{} False{} True{} False{} True{} True{} True{} True{}: 487 {==} 488 case False{} False{} True{} True{} False{} False{} False{} False{}: 489 {==} 490 case False{} False{} True{} True{} False{} False{} False{} True{}: 491 {==} 492 case False{} False{} True{} True{} False{} False{} True{} False{}: 493 {==} 494 case False{} False{} True{} True{} False{} False{} True{} True{}: 495 {==} 496 case False{} False{} True{} True{} False{} True{} False{} False{}: 497 {==} 498 case False{} False{} True{} True{} False{} True{} False{} True{}: 499 {==} 500 case False{} False{} True{} True{} False{} True{} True{} False{}: 501 {==} 502 case False{} False{} True{} True{} False{} True{} True{} True{}: 503 {==} 504 case False{} False{} True{} True{} True{} False{} False{} False{}: 505 {==} 506 case False{} False{} True{} True{} True{} False{} False{} True{}: 507 {==} 508 case False{} False{} True{} True{} True{} False{} True{} False{}: 509 {==} 510 case False{} False{} True{} True{} True{} False{} True{} True{}: 511 {==} 512 case False{} False{} True{} True{} True{} True{} False{} False{}: 513 {==} 514 case False{} False{} True{} True{} True{} True{} False{} True{}: 515 {==} 516 case False{} False{} True{} True{} True{} True{} True{} False{}: 517 {==} 518 case False{} False{} True{} True{} True{} True{} True{} True{}: 519 {==} 520 case False{} True{} False{} False{} False{} False{} False{} False{}: 521 {==} 522 case False{} True{} False{} False{} False{} False{} False{} True{}: 523 {==} 524 case False{} True{} False{} False{} False{} False{} True{} False{}: 525 {==} 526 case False{} True{} False{} False{} False{} False{} True{} True{}: 527 {==} 528 case False{} True{} False{} False{} False{} True{} False{} False{}: 529 {==} 530 case False{} True{} False{} False{} False{} True{} False{} True{}: 531 {==} 532 case False{} True{} False{} False{} False{} True{} True{} False{}: 533 {==} 534 case False{} True{} False{} False{} False{} True{} True{} True{}: 535 {==} 536 case False{} True{} False{} False{} True{} False{} False{} False{}: 537 {==} 538 case False{} True{} False{} False{} True{} False{} False{} True{}: 539 {==} 540 case False{} True{} False{} False{} True{} False{} True{} False{}: 541 {==} 542 case False{} True{} False{} False{} True{} False{} True{} True{}: 543 {==} 544 case False{} True{} False{} False{} True{} True{} False{} False{}: 545 {==} 546 case False{} True{} False{} False{} True{} True{} False{} True{}: 547 {==} 548 case False{} True{} False{} False{} True{} True{} True{} False{}: 549 {==} 550 case False{} True{} False{} False{} True{} True{} True{} True{}: 551 {==} 552 case False{} True{} False{} True{} False{} False{} False{} False{}: 553 {==} 554 case False{} True{} False{} True{} False{} False{} False{} True{}: 555 {==} 556 case False{} True{} False{} True{} False{} False{} True{} False{}: 557 {==} 558 case False{} True{} False{} True{} False{} False{} True{} True{}: 559 {==} 560 case False{} True{} False{} True{} False{} True{} False{} False{}: 561 {==} 562 case False{} True{} False{} True{} False{} True{} False{} True{}: 563 {==} 564 case False{} True{} False{} True{} False{} True{} True{} False{}: 565 {==} 566 case False{} True{} False{} True{} False{} True{} True{} True{}: 567 {==} 568 case False{} True{} False{} True{} True{} False{} False{} False{}: 569 {==} 570 case False{} True{} False{} True{} True{} False{} False{} True{}: 571 {==} 572 case False{} True{} False{} True{} True{} False{} True{} False{}: 573 {==} 574 case False{} True{} False{} True{} True{} False{} True{} True{}: 575 {==} 576 case False{} True{} False{} True{} True{} True{} False{} False{}: 577 {==} 578 case False{} True{} False{} True{} True{} True{} False{} True{}: 579 {==} 580 case False{} True{} False{} True{} True{} True{} True{} False{}: 581 {==} 582 case False{} True{} False{} True{} True{} True{} True{} True{}: 583 {==} 584 case False{} True{} True{} False{} False{} False{} False{} False{}: 585 {==} 586 case False{} True{} True{} False{} False{} False{} False{} True{}: 587 {==} 588 case False{} True{} True{} False{} False{} False{} True{} False{}: 589 {==} 590 case False{} True{} True{} False{} False{} False{} True{} True{}: 591 {==} 592 case False{} True{} True{} False{} False{} True{} False{} False{}: 593 {==} 594 case False{} True{} True{} False{} False{} True{} False{} True{}: 595 {==} 596 case False{} True{} True{} False{} False{} True{} True{} False{}: 597 {==} 598 case False{} True{} True{} False{} False{} True{} True{} True{}: 599 {==} 600 case False{} True{} True{} False{} True{} False{} False{} False{}: 601 {==} 602 case False{} True{} True{} False{} True{} False{} False{} True{}: 603 {==} 604 case False{} True{} True{} False{} True{} False{} True{} False{}: 605 {==} 606 case False{} True{} True{} False{} True{} False{} True{} True{}: 607 {==} 608 case False{} True{} True{} False{} True{} True{} False{} False{}: 609 {==} 610 case False{} True{} True{} False{} True{} True{} False{} True{}: 611 {==} 612 case False{} True{} True{} False{} True{} True{} True{} False{}: 613 {==} 614 case False{} True{} True{} False{} True{} True{} True{} True{}: 615 {==} 616 case False{} True{} True{} True{} False{} False{} False{} False{}: 617 {==} 618 case False{} True{} True{} True{} False{} False{} False{} True{}: 619 {==} 620 case False{} True{} True{} True{} False{} False{} True{} False{}: 621 {==} 622 case False{} True{} True{} True{} False{} False{} True{} True{}: 623 {==} 624 case False{} True{} True{} True{} False{} True{} False{} False{}: 625 {==} 626 case False{} True{} True{} True{} False{} True{} False{} True{}: 627 {==} 628 case False{} True{} True{} True{} False{} True{} True{} False{}: 629 {==} 630 case False{} True{} True{} True{} False{} True{} True{} True{}: 631 {==} 632 case False{} True{} True{} True{} True{} False{} False{} False{}: 633 {==} 634 case False{} True{} True{} True{} True{} False{} False{} True{}: 635 {==} 636 case False{} True{} True{} True{} True{} False{} True{} False{}: 637 {==} 638 case False{} True{} True{} True{} True{} False{} True{} True{}: 639 {==} 640 case False{} True{} True{} True{} True{} True{} False{} False{}: 641 {==} 642 case False{} True{} True{} True{} True{} True{} False{} True{}: 643 {==} 644 case False{} True{} True{} True{} True{} True{} True{} False{}: 645 {==} 646 case False{} True{} True{} True{} True{} True{} True{} True{}: 647 {==} 648 case True{} False{} False{} False{} False{} False{} False{} False{}: 649 {==} 650 case True{} False{} False{} False{} False{} False{} False{} True{}: 651 {==} 652 case True{} False{} False{} False{} False{} False{} True{} False{}: 653 {==} 654 case True{} False{} False{} False{} False{} False{} True{} True{}: 655 {==} 656 case True{} False{} False{} False{} False{} True{} False{} False{}: 657 {==} 658 case True{} False{} False{} False{} False{} True{} False{} True{}: 659 {==} 660 case True{} False{} False{} False{} False{} True{} True{} False{}: 661 {==} 662 case True{} False{} False{} False{} False{} True{} True{} True{}: 663 {==} 664 case True{} False{} False{} False{} True{} False{} False{} False{}: 665 {==} 666 case True{} False{} False{} False{} True{} False{} False{} True{}: 667 {==} 668 case True{} False{} False{} False{} True{} False{} True{} False{}: 669 {==} 670 case True{} False{} False{} False{} True{} False{} True{} True{}: 671 {==} 672 case True{} False{} False{} False{} True{} True{} False{} False{}: 673 {==} 674 case True{} False{} False{} False{} True{} True{} False{} True{}: 675 {==} 676 case True{} False{} False{} False{} True{} True{} True{} False{}: 677 {==} 678 case True{} False{} False{} False{} True{} True{} True{} True{}: 679 {==} 680 case True{} False{} False{} True{} False{} False{} False{} False{}: 681 {==} 682 case True{} False{} False{} True{} False{} False{} False{} True{}: 683 {==} 684 case True{} False{} False{} True{} False{} False{} True{} False{}: 685 {==} 686 case True{} False{} False{} True{} False{} False{} True{} True{}: 687 {==} 688 case True{} False{} False{} True{} False{} True{} False{} False{}: 689 {==} 690 case True{} False{} False{} True{} False{} True{} False{} True{}: 691 {==} 692 case True{} False{} False{} True{} False{} True{} True{} False{}: 693 {==} 694 case True{} False{} False{} True{} False{} True{} True{} True{}: 695 {==} 696 case True{} False{} False{} True{} True{} False{} False{} False{}: 697 {==} 698 case True{} False{} False{} True{} True{} False{} False{} True{}: 699 {==} 700 case True{} False{} False{} True{} True{} False{} True{} False{}: 701 {==} 702 case True{} False{} False{} True{} True{} False{} True{} True{}: 703 {==} 704 case True{} False{} False{} True{} True{} True{} False{} False{}: 705 {==} 706 case True{} False{} False{} True{} True{} True{} False{} True{}: 707 {==} 708 case True{} False{} False{} True{} True{} True{} True{} False{}: 709 {==} 710 case True{} False{} False{} True{} True{} True{} True{} True{}: 711 {==} 712 case True{} False{} True{} False{} False{} False{} False{} False{}: 713 {==} 714 case True{} False{} True{} False{} False{} False{} False{} True{}: 715 {==} 716 case True{} False{} True{} False{} False{} False{} True{} False{}: 717 {==} 718 case True{} False{} True{} False{} False{} False{} True{} True{}: 719 {==} 720 case True{} False{} True{} False{} False{} True{} False{} False{}: 721 {==} 722 case True{} False{} True{} False{} False{} True{} False{} True{}: 723 {==} 724 case True{} False{} True{} False{} False{} True{} True{} False{}: 725 {==} 726 case True{} False{} True{} False{} False{} True{} True{} True{}: 727 {==} 728 case True{} False{} True{} False{} True{} False{} False{} False{}: 729 {==} 730 case True{} False{} True{} False{} True{} False{} False{} True{}: 731 {==} 732 case True{} False{} True{} False{} True{} False{} True{} False{}: 733 {==} 734 case True{} False{} True{} False{} True{} False{} True{} True{}: 735 {==} 736 case True{} False{} True{} False{} True{} True{} False{} False{}: 737 {==} 738 case True{} False{} True{} False{} True{} True{} False{} True{}: 739 {==} 740 case True{} False{} True{} False{} True{} True{} True{} False{}: 741 {==} 742 case True{} False{} True{} False{} True{} True{} True{} True{}: 743 {==} 744 case True{} False{} True{} True{} False{} False{} False{} False{}: 745 {==} 746 case True{} False{} True{} True{} False{} False{} False{} True{}: 747 {==} 748 case True{} False{} True{} True{} False{} False{} True{} False{}: 749 {==} 750 case True{} False{} True{} True{} False{} False{} True{} True{}: 751 {==} 752 case True{} False{} True{} True{} False{} True{} False{} False{}: 753 {==} 754 case True{} False{} True{} True{} False{} True{} False{} True{}: 755 {==} 756 case True{} False{} True{} True{} False{} True{} True{} False{}: 757 {==} 758 case True{} False{} True{} True{} False{} True{} True{} True{}: 759 {==} 760 case True{} False{} True{} True{} True{} False{} False{} False{}: 761 {==} 762 case True{} False{} True{} True{} True{} False{} False{} True{}: 763 {==} 764 case True{} False{} True{} True{} True{} False{} True{} False{}: 765 {==} 766 case True{} False{} True{} True{} True{} False{} True{} True{}: 767 {==} 768 case True{} False{} True{} True{} True{} True{} False{} False{}: 769 {==} 770 case True{} False{} True{} True{} True{} True{} False{} True{}: 771 {==} 772 case True{} False{} True{} True{} True{} True{} True{} False{}: 773 {==} 774 case True{} False{} True{} True{} True{} True{} True{} True{}: 775 {==} 776 case True{} True{} False{} False{} False{} False{} False{} False{}: 777 {==} 778 case True{} True{} False{} False{} False{} False{} False{} True{}: 779 {==} 780 case True{} True{} False{} False{} False{} False{} True{} False{}: 781 {==} 782 case True{} True{} False{} False{} False{} False{} True{} True{}: 783 {==} 784 case True{} True{} False{} False{} False{} True{} False{} False{}: 785 {==} 786 case True{} True{} False{} False{} False{} True{} False{} True{}: 787 {==} 788 case True{} True{} False{} False{} False{} True{} True{} False{}: 789 {==} 790 case True{} True{} False{} False{} False{} True{} True{} True{}: 791 {==} 792 case True{} True{} False{} False{} True{} False{} False{} False{}: 793 {==} 794 case True{} True{} False{} False{} True{} False{} False{} True{}: 795 {==} 796 case True{} True{} False{} False{} True{} False{} True{} False{}: 797 {==} 798 case True{} True{} False{} False{} True{} False{} True{} True{}: 799 {==} 800 case True{} True{} False{} False{} True{} True{} False{} False{}: 801 {==} 802 case True{} True{} False{} False{} True{} True{} False{} True{}: 803 {==} 804 case True{} True{} False{} False{} True{} True{} True{} False{}: 805 {==} 806 case True{} True{} False{} False{} True{} True{} True{} True{}: 807 {==} 808 case True{} True{} False{} True{} False{} False{} False{} False{}: 809 {==} 810 case True{} True{} False{} True{} False{} False{} False{} True{}: 811 {==} 812 case True{} True{} False{} True{} False{} False{} True{} False{}: 813 {==} 814 case True{} True{} False{} True{} False{} False{} True{} True{}: 815 {==} 816 case True{} True{} False{} True{} False{} True{} False{} False{}: 817 {==} 818 case True{} True{} False{} True{} False{} True{} False{} True{}: 819 {==} 820 case True{} True{} False{} True{} False{} True{} True{} False{}: 821 {==} 822 case True{} True{} False{} True{} False{} True{} True{} True{}: 823 {==} 824 case True{} True{} False{} True{} True{} False{} False{} False{}: 825 {==} 826 case True{} True{} False{} True{} True{} False{} False{} True{}: 827 {==} 828 case True{} True{} False{} True{} True{} False{} True{} False{}: 829 {==} 830 case True{} True{} False{} True{} True{} False{} True{} True{}: 831 {==} 832 case True{} True{} False{} True{} True{} True{} False{} False{}: 833 {==} 834 case True{} True{} False{} True{} True{} True{} False{} True{}: 835 {==} 836 case True{} True{} False{} True{} True{} True{} True{} False{}: 837 {==} 838 case True{} True{} False{} True{} True{} True{} True{} True{}: 839 {==} 840 case True{} True{} True{} False{} False{} False{} False{} False{}: 841 {==} 842 case True{} True{} True{} False{} False{} False{} False{} True{}: 843 {==} 844 case True{} True{} True{} False{} False{} False{} True{} False{}: 845 {==} 846 case True{} True{} True{} False{} False{} False{} True{} True{}: 847 {==} 848 case True{} True{} True{} False{} False{} True{} False{} False{}: 849 {==} 850 case True{} True{} True{} False{} False{} True{} False{} True{}: 851 {==} 852 case True{} True{} True{} False{} False{} True{} True{} False{}: 853 {==} 854 case True{} True{} True{} False{} False{} True{} True{} True{}: 855 {==} 856 case True{} True{} True{} False{} True{} False{} False{} False{}: 857 {==} 858 case True{} True{} True{} False{} True{} False{} False{} True{}: 859 {==} 860 case True{} True{} True{} False{} True{} False{} True{} False{}: 861 {==} 862 case True{} True{} True{} False{} True{} False{} True{} True{}: 863 {==} 864 case True{} True{} True{} False{} True{} True{} False{} False{}: 865 {==} 866 case True{} True{} True{} False{} True{} True{} False{} True{}: 867 {==} 868 case True{} True{} True{} False{} True{} True{} True{} False{}: 869 {==} 870 case True{} True{} True{} False{} True{} True{} True{} True{}: 871 {==} 872 case True{} True{} True{} True{} False{} False{} False{} False{}: 873 {==} 874 case True{} True{} True{} True{} False{} False{} False{} True{}: 875 {==} 876 case True{} True{} True{} True{} False{} False{} True{} False{}: 877 {==} 878 case True{} True{} True{} True{} False{} False{} True{} True{}: 879 {==} 880 case True{} True{} True{} True{} False{} True{} False{} False{}: 881 {==} 882 case True{} True{} True{} True{} False{} True{} False{} True{}: 883 {==} 884 case True{} True{} True{} True{} False{} True{} True{} False{}: 885 {==} 886 case True{} True{} True{} True{} False{} True{} True{} True{}: 887 {==} 888 case True{} True{} True{} True{} True{} False{} False{} False{}: 889 {==} 890 case True{} True{} True{} True{} True{} False{} False{} True{}: 891 {==} 892 case True{} True{} True{} True{} True{} False{} True{} False{}: 893 {==} 894 case True{} True{} True{} True{} True{} False{} True{} True{}: 895 {==} 896 case True{} True{} True{} True{} True{} True{} False{} False{}: 897 {==} 898 case True{} True{} True{} True{} True{} True{} False{} True{}: 899 {==} 900 case True{} True{} True{} True{} True{} True{} True{} False{}: 901 {==} 902 case True{} True{} True{} True{} True{} True{} True{} True{}: 903 {==} 904 905 law bt2_bidx: 906 for +e0: Bool 907 for +e1: Bool 908 for +e2: Bool 909 for +e3: Bool 910 for +f0: Bool 911 for +f1: Bool 912 for +f2: Bool 913 for +f3: Bool 914 for +h: {Nat.is_lt(Nat.min(R4(e0, e1, e2, e3), R4(f0, f1, f2, f3)), 4n) == True{} : Bool} 915 {U32.to_nat(U32.add(U32.add(FA.b2u(Bool.and(Bool.and(Bool.not(e0), True{}), Bool.and(Bool.not(f0), True{}))), FA.b2u(Bool.and(Bool.and(Bool.not(e0), Bool.and(Bool.not(e1), True{})), Bool.and(Bool.not(f0), Bool.and(Bool.not(f1), True{}))))), FA.b2u(Bool.and(Bool.and(Bool.not(e0), Bool.and(Bool.not(e1), Bool.and(Bool.not(e2), True{}))), Bool.and(Bool.not(f0), Bool.and(Bool.not(f1), Bool.and(Bool.not(f2), True{}))))))) == Nat.min(R4(e0, e1, e2, e3), R4(f0, f1, f2, f3)) : Nat} 916 917 def bt2_bidx(e0, e1, e2, e3, f0, f1, f2, f3, h): 918 match e0 e1 e2 e3 f0 f1 f2 f3: 919 case False{} False{} False{} False{} False{} False{} False{} False{}: 920 Empty.absurd({U32.to_nat(U32.add(U32.add(FA.b2u(Bool.and(Bool.and(Bool.not(False{}), True{}), Bool.and(Bool.not(False{}), True{}))), FA.b2u(Bool.and(Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), True{})), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), True{}))))), FA.b2u(Bool.and(Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), True{}))), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), True{}))))))) == Nat.min(R4(False{}, False{}, False{}, False{}), R4(False{}, False{}, False{}, False{})) : Nat}, AB.false_ne_true(h)) 921 case False{} False{} False{} False{} False{} False{} False{} True{}: 922 {==} 923 case False{} False{} False{} False{} False{} False{} True{} False{}: 924 {==} 925 case False{} False{} False{} False{} False{} False{} True{} True{}: 926 {==} 927 case False{} False{} False{} False{} False{} True{} False{} False{}: 928 {==} 929 case False{} False{} False{} False{} False{} True{} False{} True{}: 930 {==} 931 case False{} False{} False{} False{} False{} True{} True{} False{}: 932 {==} 933 case False{} False{} False{} False{} False{} True{} True{} True{}: 934 {==} 935 case False{} False{} False{} False{} True{} False{} False{} False{}: 936 {==} 937 case False{} False{} False{} False{} True{} False{} False{} True{}: 938 {==} 939 case False{} False{} False{} False{} True{} False{} True{} False{}: 940 {==} 941 case False{} False{} False{} False{} True{} False{} True{} True{}: 942 {==} 943 case False{} False{} False{} False{} True{} True{} False{} False{}: 944 {==} 945 case False{} False{} False{} False{} True{} True{} False{} True{}: 946 {==} 947 case False{} False{} False{} False{} True{} True{} True{} False{}: 948 {==} 949 case False{} False{} False{} False{} True{} True{} True{} True{}: 950 {==} 951 case False{} False{} False{} True{} False{} False{} False{} False{}: 952 {==} 953 case False{} False{} False{} True{} False{} False{} False{} True{}: 954 {==} 955 case False{} False{} False{} True{} False{} False{} True{} False{}: 956 {==} 957 case False{} False{} False{} True{} False{} False{} True{} True{}: 958 {==} 959 case False{} False{} False{} True{} False{} True{} False{} False{}: 960 {==} 961 case False{} False{} False{} True{} False{} True{} False{} True{}: 962 {==} 963 case False{} False{} False{} True{} False{} True{} True{} False{}: 964 {==} 965 case False{} False{} False{} True{} False{} True{} True{} True{}: 966 {==} 967 case False{} False{} False{} True{} True{} False{} False{} False{}: 968 {==} 969 case False{} False{} False{} True{} True{} False{} False{} True{}: 970 {==} 971 case False{} False{} False{} True{} True{} False{} True{} False{}: 972 {==} 973 case False{} False{} False{} True{} True{} False{} True{} True{}: 974 {==} 975 case False{} False{} False{} True{} True{} True{} False{} False{}: 976 {==} 977 case False{} False{} False{} True{} True{} True{} False{} True{}: 978 {==} 979 case False{} False{} False{} True{} True{} True{} True{} False{}: 980 {==} 981 case False{} False{} False{} True{} True{} True{} True{} True{}: 982 {==} 983 case False{} False{} True{} False{} False{} False{} False{} False{}: 984 {==} 985 case False{} False{} True{} False{} False{} False{} False{} True{}: 986 {==} 987 case False{} False{} True{} False{} False{} False{} True{} False{}: 988 {==} 989 case False{} False{} True{} False{} False{} False{} True{} True{}: 990 {==} 991 case False{} False{} True{} False{} False{} True{} False{} False{}: 992 {==} 993 case False{} False{} True{} False{} False{} True{} False{} True{}: 994 {==} 995 case False{} False{} True{} False{} False{} True{} True{} False{}: 996 {==} 997 case False{} False{} True{} False{} False{} True{} True{} True{}: 998 {==} 999 case False{} False{} True{} False{} True{} False{} False{} False{}: 1000 {==} 1001 case False{} False{} True{} False{} True{} False{} False{} True{}: 1002 {==} 1003 case False{} False{} True{} False{} True{} False{} True{} False{}: 1004 {==} 1005 case False{} False{} True{} False{} True{} False{} True{} True{}: 1006 {==} 1007 case False{} False{} True{} False{} True{} True{} False{} False{}: 1008 {==} 1009 case False{} False{} True{} False{} True{} True{} False{} True{}: 1010 {==} 1011 case False{} False{} True{} False{} True{} True{} True{} False{}: 1012 {==} 1013 case False{} False{} True{} False{} True{} True{} True{} True{}: 1014 {==} 1015 case False{} False{} True{} True{} False{} False{} False{} False{}: 1016 {==} 1017 case False{} False{} True{} True{} False{} False{} False{} True{}: 1018 {==} 1019 case False{} False{} True{} True{} False{} False{} True{} False{}: 1020 {==} 1021 case False{} False{} True{} True{} False{} False{} True{} True{}: 1022 {==} 1023 case False{} False{} True{} True{} False{} True{} False{} False{}: 1024 {==} 1025 case False{} False{} True{} True{} False{} True{} False{} True{}: 1026 {==} 1027 case False{} False{} True{} True{} False{} True{} True{} False{}: 1028 {==} 1029 case False{} False{} True{} True{} False{} True{} True{} True{}: 1030 {==} 1031 case False{} False{} True{} True{} True{} False{} False{} False{}: 1032 {==} 1033 case False{} False{} True{} True{} True{} False{} False{} True{}: 1034 {==} 1035 case False{} False{} True{} True{} True{} False{} True{} False{}: 1036 {==} 1037 case False{} False{} True{} True{} True{} False{} True{} True{}: 1038 {==} 1039 case False{} False{} True{} True{} True{} True{} False{} False{}: 1040 {==} 1041 case False{} False{} True{} True{} True{} True{} False{} True{}: 1042 {==} 1043 case False{} False{} True{} True{} True{} True{} True{} False{}: 1044 {==} 1045 case False{} False{} True{} True{} True{} True{} True{} True{}: 1046 {==} 1047 case False{} True{} False{} False{} False{} False{} False{} False{}: 1048 {==} 1049 case False{} True{} False{} False{} False{} False{} False{} True{}: 1050 {==} 1051 case False{} True{} False{} False{} False{} False{} True{} False{}: 1052 {==} 1053 case False{} True{} False{} False{} False{} False{} True{} True{}: 1054 {==} 1055 case False{} True{} False{} False{} False{} True{} False{} False{}: 1056 {==} 1057 case False{} True{} False{} False{} False{} True{} False{} True{}: 1058 {==} 1059 case False{} True{} False{} False{} False{} True{} True{} False{}: 1060 {==} 1061 case False{} True{} False{} False{} False{} True{} True{} True{}: 1062 {==} 1063 case False{} True{} False{} False{} True{} False{} False{} False{}: 1064 {==} 1065 case False{} True{} False{} False{} True{} False{} False{} True{}: 1066 {==} 1067 case False{} True{} False{} False{} True{} False{} True{} False{}: 1068 {==} 1069 case False{} True{} False{} False{} True{} False{} True{} True{}: 1070 {==} 1071 case False{} True{} False{} False{} True{} True{} False{} False{}: 1072 {==} 1073 case False{} True{} False{} False{} True{} True{} False{} True{}: 1074 {==} 1075 case False{} True{} False{} False{} True{} True{} True{} False{}: 1076 {==} 1077 case False{} True{} False{} False{} True{} True{} True{} True{}: 1078 {==} 1079 case False{} True{} False{} True{} False{} False{} False{} False{}: 1080 {==} 1081 case False{} True{} False{} True{} False{} False{} False{} True{}: 1082 {==} 1083 case False{} True{} False{} True{} False{} False{} True{} False{}: 1084 {==} 1085 case False{} True{} False{} True{} False{} False{} True{} True{}: 1086 {==} 1087 case False{} True{} False{} True{} False{} True{} False{} False{}: 1088 {==} 1089 case False{} True{} False{} True{} False{} True{} False{} True{}: 1090 {==} 1091 case False{} True{} False{} True{} False{} True{} True{} False{}: 1092 {==} 1093 case False{} True{} False{} True{} False{} True{} True{} True{}: 1094 {==} 1095 case False{} True{} False{} True{} True{} False{} False{} False{}: 1096 {==} 1097 case False{} True{} False{} True{} True{} False{} False{} True{}: 1098 {==} 1099 case False{} True{} False{} True{} True{} False{} True{} False{}: 1100 {==} 1101 case False{} True{} False{} True{} True{} False{} True{} True{}: 1102 {==} 1103 case False{} True{} False{} True{} True{} True{} False{} False{}: 1104 {==} 1105 case False{} True{} False{} True{} True{} True{} False{} True{}: 1106 {==} 1107 case False{} True{} False{} True{} True{} True{} True{} False{}: 1108 {==} 1109 case False{} True{} False{} True{} True{} True{} True{} True{}: 1110 {==} 1111 case False{} True{} True{} False{} False{} False{} False{} False{}: 1112 {==} 1113 case False{} True{} True{} False{} False{} False{} False{} True{}: 1114 {==} 1115 case False{} True{} True{} False{} False{} False{} True{} False{}: 1116 {==} 1117 case False{} True{} True{} False{} False{} False{} True{} True{}: 1118 {==} 1119 case False{} True{} True{} False{} False{} True{} False{} False{}: 1120 {==} 1121 case False{} True{} True{} False{} False{} True{} False{} True{}: 1122 {==} 1123 case False{} True{} True{} False{} False{} True{} True{} False{}: 1124 {==} 1125 case False{} True{} True{} False{} False{} True{} True{} True{}: 1126 {==} 1127 case False{} True{} True{} False{} True{} False{} False{} False{}: 1128 {==} 1129 case False{} True{} True{} False{} True{} False{} False{} True{}: 1130 {==} 1131 case False{} True{} True{} False{} True{} False{} True{} False{}: 1132 {==} 1133 case False{} True{} True{} False{} True{} False{} True{} True{}: 1134 {==} 1135 case False{} True{} True{} False{} True{} True{} False{} False{}: 1136 {==} 1137 case False{} True{} True{} False{} True{} True{} False{} True{}: 1138 {==} 1139 case False{} True{} True{} False{} True{} True{} True{} False{}: 1140 {==} 1141 case False{} True{} True{} False{} True{} True{} True{} True{}: 1142 {==} 1143 case False{} True{} True{} True{} False{} False{} False{} False{}: 1144 {==} 1145 case False{} True{} True{} True{} False{} False{} False{} True{}: 1146 {==} 1147 case False{} True{} True{} True{} False{} False{} True{} False{}: 1148 {==} 1149 case False{} True{} True{} True{} False{} False{} True{} True{}: 1150 {==} 1151 case False{} True{} True{} True{} False{} True{} False{} False{}: 1152 {==} 1153 case False{} True{} True{} True{} False{} True{} False{} True{}: 1154 {==} 1155 case False{} True{} True{} True{} False{} True{} True{} False{}: 1156 {==} 1157 case False{} True{} True{} True{} False{} True{} True{} True{}: 1158 {==} 1159 case False{} True{} True{} True{} True{} False{} False{} False{}: 1160 {==} 1161 case False{} True{} True{} True{} True{} False{} False{} True{}: 1162 {==} 1163 case False{} True{} True{} True{} True{} False{} True{} False{}: 1164 {==} 1165 case False{} True{} True{} True{} True{} False{} True{} True{}: 1166 {==} 1167 case False{} True{} True{} True{} True{} True{} False{} False{}: 1168 {==} 1169 case False{} True{} True{} True{} True{} True{} False{} True{}: 1170 {==} 1171 case False{} True{} True{} True{} True{} True{} True{} False{}: 1172 {==} 1173 case False{} True{} True{} True{} True{} True{} True{} True{}: 1174 {==} 1175 case True{} False{} False{} False{} False{} False{} False{} False{}: 1176 {==} 1177 case True{} False{} False{} False{} False{} False{} False{} True{}: 1178 {==} 1179 case True{} False{} False{} False{} False{} False{} True{} False{}: 1180 {==} 1181 case True{} False{} False{} False{} False{} False{} True{} True{}: 1182 {==} 1183 case True{} False{} False{} False{} False{} True{} False{} False{}: 1184 {==} 1185 case True{} False{} False{} False{} False{} True{} False{} True{}: 1186 {==} 1187 case True{} False{} False{} False{} False{} True{} True{} False{}: 1188 {==} 1189 case True{} False{} False{} False{} False{} True{} True{} True{}: 1190 {==} 1191 case True{} False{} False{} False{} True{} False{} False{} False{}: 1192 {==} 1193 case True{} False{} False{} False{} True{} False{} False{} True{}: 1194 {==} 1195 case True{} False{} False{} False{} True{} False{} True{} False{}: 1196 {==} 1197 case True{} False{} False{} False{} True{} False{} True{} True{}: 1198 {==} 1199 case True{} False{} False{} False{} True{} True{} False{} False{}: 1200 {==} 1201 case True{} False{} False{} False{} True{} True{} False{} True{}: 1202 {==} 1203 case True{} False{} False{} False{} True{} True{} True{} False{}: 1204 {==} 1205 case True{} False{} False{} False{} True{} True{} True{} True{}: 1206 {==} 1207 case True{} False{} False{} True{} False{} False{} False{} False{}: 1208 {==} 1209 case True{} False{} False{} True{} False{} False{} False{} True{}: 1210 {==} 1211 case True{} False{} False{} True{} False{} False{} True{} False{}: 1212 {==} 1213 case True{} False{} False{} True{} False{} False{} True{} True{}: 1214 {==} 1215 case True{} False{} False{} True{} False{} True{} False{} False{}: 1216 {==} 1217 case True{} False{} False{} True{} False{} True{} False{} True{}: 1218 {==} 1219 case True{} False{} False{} True{} False{} True{} True{} False{}: 1220 {==} 1221 case True{} False{} False{} True{} False{} True{} True{} True{}: 1222 {==} 1223 case True{} False{} False{} True{} True{} False{} False{} False{}: 1224 {==} 1225 case True{} False{} False{} True{} True{} False{} False{} True{}: 1226 {==} 1227 case True{} False{} False{} True{} True{} False{} True{} False{}: 1228 {==} 1229 case True{} False{} False{} True{} True{} False{} True{} True{}: 1230 {==} 1231 case True{} False{} False{} True{} True{} True{} False{} False{}: 1232 {==} 1233 case True{} False{} False{} True{} True{} True{} False{} True{}: 1234 {==} 1235 case True{} False{} False{} True{} True{} True{} True{} False{}: 1236 {==} 1237 case True{} False{} False{} True{} True{} True{} True{} True{}: 1238 {==} 1239 case True{} False{} True{} False{} False{} False{} False{} False{}: 1240 {==} 1241 case True{} False{} True{} False{} False{} False{} False{} True{}: 1242 {==} 1243 case True{} False{} True{} False{} False{} False{} True{} False{}: 1244 {==} 1245 case True{} False{} True{} False{} False{} False{} True{} True{}: 1246 {==} 1247 case True{} False{} True{} False{} False{} True{} False{} False{}: 1248 {==} 1249 case True{} False{} True{} False{} False{} True{} False{} True{}: 1250 {==} 1251 case True{} False{} True{} False{} False{} True{} True{} False{}: 1252 {==} 1253 case True{} False{} True{} False{} False{} True{} True{} True{}: 1254 {==} 1255 case True{} False{} True{} False{} True{} False{} False{} False{}: 1256 {==} 1257 case True{} False{} True{} False{} True{} False{} False{} True{}: 1258 {==} 1259 case True{} False{} True{} False{} True{} False{} True{} False{}: 1260 {==} 1261 case True{} False{} True{} False{} True{} False{} True{} True{}: 1262 {==} 1263 case True{} False{} True{} False{} True{} True{} False{} False{}: 1264 {==} 1265 case True{} False{} True{} False{} True{} True{} False{} True{}: 1266 {==} 1267 case True{} False{} True{} False{} True{} True{} True{} False{}: 1268 {==} 1269 case True{} False{} True{} False{} True{} True{} True{} True{}: 1270 {==} 1271 case True{} False{} True{} True{} False{} False{} False{} False{}: 1272 {==} 1273 case True{} False{} True{} True{} False{} False{} False{} True{}: 1274 {==} 1275 case True{} False{} True{} True{} False{} False{} True{} False{}: 1276 {==} 1277 case True{} False{} True{} True{} False{} False{} True{} True{}: 1278 {==} 1279 case True{} False{} True{} True{} False{} True{} False{} False{}: 1280 {==} 1281 case True{} False{} True{} True{} False{} True{} False{} True{}: 1282 {==} 1283 case True{} False{} True{} True{} False{} True{} True{} False{}: 1284 {==} 1285 case True{} False{} True{} True{} False{} True{} True{} True{}: 1286 {==} 1287 case True{} False{} True{} True{} True{} False{} False{} False{}: 1288 {==} 1289 case True{} False{} True{} True{} True{} False{} False{} True{}: 1290 {==} 1291 case True{} False{} True{} True{} True{} False{} True{} False{}: 1292 {==} 1293 case True{} False{} True{} True{} True{} False{} True{} True{}: 1294 {==} 1295 case True{} False{} True{} True{} True{} True{} False{} False{}: 1296 {==} 1297 case True{} False{} True{} True{} True{} True{} False{} True{}: 1298 {==} 1299 case True{} False{} True{} True{} True{} True{} True{} False{}: 1300 {==} 1301 case True{} False{} True{} True{} True{} True{} True{} True{}: 1302 {==} 1303 case True{} True{} False{} False{} False{} False{} False{} False{}: 1304 {==} 1305 case True{} True{} False{} False{} False{} False{} False{} True{}: 1306 {==} 1307 case True{} True{} False{} False{} False{} False{} True{} False{}: 1308 {==} 1309 case True{} True{} False{} False{} False{} False{} True{} True{}: 1310 {==} 1311 case True{} True{} False{} False{} False{} True{} False{} False{}: 1312 {==} 1313 case True{} True{} False{} False{} False{} True{} False{} True{}: 1314 {==} 1315 case True{} True{} False{} False{} False{} True{} True{} False{}: 1316 {==} 1317 case True{} True{} False{} False{} False{} True{} True{} True{}: 1318 {==} 1319 case True{} True{} False{} False{} True{} False{} False{} False{}: 1320 {==} 1321 case True{} True{} False{} False{} True{} False{} False{} True{}: 1322 {==} 1323 case True{} True{} False{} False{} True{} False{} True{} False{}: 1324 {==} 1325 case True{} True{} False{} False{} True{} False{} True{} True{}: 1326 {==} 1327 case True{} True{} False{} False{} True{} True{} False{} False{}: 1328 {==} 1329 case True{} True{} False{} False{} True{} True{} False{} True{}: 1330 {==} 1331 case True{} True{} False{} False{} True{} True{} True{} False{}: 1332 {==} 1333 case True{} True{} False{} False{} True{} True{} True{} True{}: 1334 {==} 1335 case True{} True{} False{} True{} False{} False{} False{} False{}: 1336 {==} 1337 case True{} True{} False{} True{} False{} False{} False{} True{}: 1338 {==} 1339 case True{} True{} False{} True{} False{} False{} True{} False{}: 1340 {==} 1341 case True{} True{} False{} True{} False{} False{} True{} True{}: 1342 {==} 1343 case True{} True{} False{} True{} False{} True{} False{} False{}: 1344 {==} 1345 case True{} True{} False{} True{} False{} True{} False{} True{}: 1346 {==} 1347 case True{} True{} False{} True{} False{} True{} True{} False{}: 1348 {==} 1349 case True{} True{} False{} True{} False{} True{} True{} True{}: 1350 {==} 1351 case True{} True{} False{} True{} True{} False{} False{} False{}: 1352 {==} 1353 case True{} True{} False{} True{} True{} False{} False{} True{}: 1354 {==} 1355 case True{} True{} False{} True{} True{} False{} True{} False{}: 1356 {==} 1357 case True{} True{} False{} True{} True{} False{} True{} True{}: 1358 {==} 1359 case True{} True{} False{} True{} True{} True{} False{} False{}: 1360 {==} 1361 case True{} True{} False{} True{} True{} True{} False{} True{}: 1362 {==} 1363 case True{} True{} False{} True{} True{} True{} True{} False{}: 1364 {==} 1365 case True{} True{} False{} True{} True{} True{} True{} True{}: 1366 {==} 1367 case True{} True{} True{} False{} False{} False{} False{} False{}: 1368 {==} 1369 case True{} True{} True{} False{} False{} False{} False{} True{}: 1370 {==} 1371 case True{} True{} True{} False{} False{} False{} True{} False{}: 1372 {==} 1373 case True{} True{} True{} False{} False{} False{} True{} True{}: 1374 {==} 1375 case True{} True{} True{} False{} False{} True{} False{} False{}: 1376 {==} 1377 case True{} True{} True{} False{} False{} True{} False{} True{}: 1378 {==} 1379 case True{} True{} True{} False{} False{} True{} True{} False{}: 1380 {==} 1381 case True{} True{} True{} False{} False{} True{} True{} True{}: 1382 {==} 1383 case True{} True{} True{} False{} True{} False{} False{} False{}: 1384 {==} 1385 case True{} True{} True{} False{} True{} False{} False{} True{}: 1386 {==} 1387 case True{} True{} True{} False{} True{} False{} True{} False{}: 1388 {==} 1389 case True{} True{} True{} False{} True{} False{} True{} True{}: 1390 {==} 1391 case True{} True{} True{} False{} True{} True{} False{} False{}: 1392 {==} 1393 case True{} True{} True{} False{} True{} True{} False{} True{}: 1394 {==} 1395 case True{} True{} True{} False{} True{} True{} True{} False{}: 1396 {==} 1397 case True{} True{} True{} False{} True{} True{} True{} True{}: 1398 {==} 1399 case True{} True{} True{} True{} False{} False{} False{} False{}: 1400 {==} 1401 case True{} True{} True{} True{} False{} False{} False{} True{}: 1402 {==} 1403 case True{} True{} True{} True{} False{} False{} True{} False{}: 1404 {==} 1405 case True{} True{} True{} True{} False{} False{} True{} True{}: 1406 {==} 1407 case True{} True{} True{} True{} False{} True{} False{} False{}: 1408 {==} 1409 case True{} True{} True{} True{} False{} True{} False{} True{}: 1410 {==} 1411 case True{} True{} True{} True{} False{} True{} True{} False{}: 1412 {==} 1413 case True{} True{} True{} True{} False{} True{} True{} True{}: 1414 {==} 1415 case True{} True{} True{} True{} True{} False{} False{} False{}: 1416 {==} 1417 case True{} True{} True{} True{} True{} False{} False{} True{}: 1418 {==} 1419 case True{} True{} True{} True{} True{} False{} True{} False{}: 1420 {==} 1421 case True{} True{} True{} True{} True{} False{} True{} True{}: 1422 {==} 1423 case True{} True{} True{} True{} True{} True{} False{} False{}: 1424 {==} 1425 case True{} True{} True{} True{} True{} True{} False{} True{}: 1426 {==} 1427 case True{} True{} True{} True{} True{} True{} True{} False{}: 1428 {==} 1429 case True{} True{} True{} True{} True{} True{} True{} True{}: 1430 {==} 1431