proof_fast_w2.bend
lawful-bytes@0.1.0.0 · 1,431 lines · 0 definitions
1import Base
2import lawful-words@0.1.0.0/defs.bend as W
3import lawful-words@0.1.0.0/proof_nat.bend as N
4import lawful-words@0.1.0.0/proof_u32.bend as U
5import lawful-words@0.1.0.0/proof_bytes.bend as Y
6import lawful-words@0.1.0.0/proof_zb.bend as Z
7import lawful-arrays@0.1.0.0/proof_base.bend as AB
8import lawful-bytes@0.1.0.0/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
17law 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
24def 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
47law 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
53def 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
66law iz:
67 for +w: Word(32n)
68 {U32.is_zero(U32{w}) == Z.allz(32n, w) : Bool}
69
70def iz(w):
71 Z.allz_cmp(32n, w)
72
73law 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
79def 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
90law 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
95def 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
105def 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
112law wor0:
113 for +n: Nat
114 for +x: Word(n)
115 {Word.or(n, x, Word.zero(n)) == x : Word(n)}
116
117def 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
129law or0r:
130 for +y: U32
131 {U32.or(y, 0) == y : U32}
132
133def 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
139law or255:
140 for +y: U32
141 {U32.is_eq(U32.or(y, 255), 0) == False{} : Bool}
142
143def 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
149law nth4_same:
150 for +j: Nat
151 for +c: U32
152 {W.nth4(j, c, c, c, c) == c : U32}
153
154def 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
169law 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
176def 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.
191law 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
203def 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
214law 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
219def 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
224law 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
231def 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
238law 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
246def 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.
254law 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
264def 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.
273law 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
281def 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.
291def 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
294law 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
301def 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
336law 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
344def 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
379law 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
390def 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
905law 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
917def 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