proof_fast_w1.bend

lawful-bytes@0.1.1.0 · 708 lines · 10 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.1.0/fast.bend as FA
9
10# Word facts for fast.bend's zero-byte search, at the level of bits (the
11# style of lawful-words' proof_zb.bend: a word is four bytes, app8, and a
12# per-byte lemma checked on all 256 bytes).
13
14# And is associative
15# ==================
16
17law wand_assoc:
18  for +n: Nat
19  for +x: Word(n)
20  for +y: Word(n)
21  for +z: Word(n)
22  {Word.and(n, x, Word.and(n, y, z)) == Word.and(n, Word.and(n, x, y), z) : Word(n)}
23
24def wand_assoc(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{+b, +yt} WCon{+c, +zt}:
31          %wand_assoc(p, xt, yt, zt) :
32            {WCon{False{}, Word.and(p, xt, Word.and(p, yt, zt))} == WCon{False{}, _} : Word(1n+p)}
33          {==}
34        case WCon{True{}, +xt} WCon{+b, +yt} WCon{+c, +zt}:
35          %wand_assoc(p, xt, yt, zt) :
36            {WCon{Bool.and(b, c), Word.and(p, xt, Word.and(p, yt, zt))} == WCon{Bool.and(b, c), _} : Word(1n+p)}
37          {==}
38
39law uand_assoc:
40  for +a: U32
41  for +b: U32
42  for +c: U32
43  {U32.and(a, U32.and(b, c)) == U32.and(U32.and(a, b), c) : U32}
44
45def uand_assoc(a, b, c):
46  match a b c:
47    case U32{+x} U32{+y} U32{+z}:
48      %wand_assoc(32n, x, y, z) : {U32{Word.and(32n, x, Word.and(32n, y, z))} == U32{_} : U32}
49      {==}
50
51# fast.bend's zb is lawful-words' zb.
52law zb_eq:
53  for +v: U32
54  {FA.zb(v) == W.zb(v) : U32}
55
56def zb_eq(v):
57  uand_assoc(U32.sub(v, 16843009), U32.not(v), 2155905152)
58
59# One byte of the masked zero-byte test
60# =====================================
61
62# With no borrow in and the byte's flag kept by the mask, the masked flags are
63# all clear exactly when the byte is not zero and the rest are clear.
64law zbk_byte:
65  for +n: Nat
66  for +x: Word(8n)
67  for +r: Word(n)
68  for +kr: Word(n)
69  for +hr: Word(n)
70  for +mr: Word(n)
71  {Z.allz(Nat.add(8n, n), Word.and(Nat.add(8n, n), Z.zf(Nat.add(8n, n), Z.app8(n, x, r), Z.app8(n, Z.one8(), kr), Z.app8(n, Z.h8(), hr), True{}), Z.app8(n, Z.h8(), mr)))
72    == Bool.and(Bool.not(Z.allz(8n, x)), Z.allz(n, Word.and(n, Z.zf(n, r, kr, hr, True{}), mr))) : Bool}
73
74def zbk_byte(n, x, r, kr, hr, mr):
75  match x:
76    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
77      {==}
78    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
79      {==}
80    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
81      {==}
82    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
83      {==}
84    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
85      {==}
86    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
87      {==}
88    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
89      {==}
90    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
91      {==}
92    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
93      {==}
94    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
95      {==}
96    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
97      {==}
98    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
99      {==}
100    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
101      {==}
102    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
103      {==}
104    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
105      {==}
106    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
107      {==}
108    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
109      {==}
110    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
111      {==}
112    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
113      {==}
114    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
115      {==}
116    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
117      {==}
118    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
119      {==}
120    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
121      {==}
122    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
123      {==}
124    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
125      {==}
126    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
127      {==}
128    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
129      {==}
130    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
131      {==}
132    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
133      {==}
134    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
135      {==}
136    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
137      {==}
138    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
139      {==}
140    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
141      {==}
142    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
143      {==}
144    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
145      {==}
146    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
147      {==}
148    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
149      {==}
150    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
151      {==}
152    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
153      {==}
154    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
155      {==}
156    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
157      {==}
158    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
159      {==}
160    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
161      {==}
162    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
163      {==}
164    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
165      {==}
166    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
167      {==}
168    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
169      {==}
170    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
171      {==}
172    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
173      {==}
174    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
175      {==}
176    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
177      {==}
178    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
179      {==}
180    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
181      {==}
182    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
183      {==}
184    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
185      {==}
186    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
187      {==}
188    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
189      {==}
190    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
191      {==}
192    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
193      {==}
194    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
195      {==}
196    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
197      {==}
198    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
199      {==}
200    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
201      {==}
202    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}:
203      {==}
204    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
205      {==}
206    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
207      {==}
208    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
209      {==}
210    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
211      {==}
212    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
213      {==}
214    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
215      {==}
216    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
217      {==}
218    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
219      {==}
220    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
221      {==}
222    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
223      {==}
224    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
225      {==}
226    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
227      {==}
228    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
229      {==}
230    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
231      {==}
232    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
233      {==}
234    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
235      {==}
236    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
237      {==}
238    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
239      {==}
240    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
241      {==}
242    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
243      {==}
244    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
245      {==}
246    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
247      {==}
248    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
249      {==}
250    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
251      {==}
252    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
253      {==}
254    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
255      {==}
256    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
257      {==}
258    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
259      {==}
260    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
261      {==}
262    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
263      {==}
264    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
265      {==}
266    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
267      {==}
268    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
269      {==}
270    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
271      {==}
272    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
273      {==}
274    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
275      {==}
276    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
277      {==}
278    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
279      {==}
280    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
281      {==}
282    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
283      {==}
284    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
285      {==}
286    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
287      {==}
288    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
289      {==}
290    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
291      {==}
292    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
293      {==}
294    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
295      {==}
296    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
297      {==}
298    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
299      {==}
300    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
301      {==}
302    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
303      {==}
304    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
305      {==}
306    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
307      {==}
308    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
309      {==}
310    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
311      {==}
312    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
313      {==}
314    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
315      {==}
316    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
317      {==}
318    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
319      {==}
320    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
321      {==}
322    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
323      {==}
324    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
325      {==}
326    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
327      {==}
328    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
329      {==}
330    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WNil{}}}}}}}}}:
331      {==}
332    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
333      {==}
334    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
335      {==}
336    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
337      {==}
338    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
339      {==}
340    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
341      {==}
342    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
343      {==}
344    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
345      {==}
346    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
347      {==}
348    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
349      {==}
350    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
351      {==}
352    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
353      {==}
354    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
355      {==}
356    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
357      {==}
358    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
359      {==}
360    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
361      {==}
362    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
363      {==}
364    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
365      {==}
366    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
367      {==}
368    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
369      {==}
370    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
371      {==}
372    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
373      {==}
374    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
375      {==}
376    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
377      {==}
378    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
379      {==}
380    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
381      {==}
382    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
383      {==}
384    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
385      {==}
386    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
387      {==}
388    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
389      {==}
390    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
391      {==}
392    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
393      {==}
394    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
395      {==}
396    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
397      {==}
398    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
399      {==}
400    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
401      {==}
402    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
403      {==}
404    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
405      {==}
406    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
407      {==}
408    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
409      {==}
410    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
411      {==}
412    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
413      {==}
414    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
415      {==}
416    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
417      {==}
418    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
419      {==}
420    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
421      {==}
422    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
423      {==}
424    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
425      {==}
426    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
427      {==}
428    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
429      {==}
430    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
431      {==}
432    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
433      {==}
434    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
435      {==}
436    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
437      {==}
438    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
439      {==}
440    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
441      {==}
442    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
443      {==}
444    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
445      {==}
446    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
447      {==}
448    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
449      {==}
450    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
451      {==}
452    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
453      {==}
454    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
455      {==}
456    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
457      {==}
458    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WNil{}}}}}}}}}:
459      {==}
460    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
461      {==}
462    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
463      {==}
464    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
465      {==}
466    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
467      {==}
468    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
469      {==}
470    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
471      {==}
472    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
473      {==}
474    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
475      {==}
476    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
477      {==}
478    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
479      {==}
480    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
481      {==}
482    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
483      {==}
484    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
485      {==}
486    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
487      {==}
488    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
489      {==}
490    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
491      {==}
492    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
493      {==}
494    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
495      {==}
496    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
497      {==}
498    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
499      {==}
500    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
501      {==}
502    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
503      {==}
504    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
505      {==}
506    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
507      {==}
508    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
509      {==}
510    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
511      {==}
512    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
513      {==}
514    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
515      {==}
516    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
517      {==}
518    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
519      {==}
520    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
521      {==}
522    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
523      {==}
524    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
525      {==}
526    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
527      {==}
528    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
529      {==}
530    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
531      {==}
532    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
533      {==}
534    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
535      {==}
536    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
537      {==}
538    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
539      {==}
540    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
541      {==}
542    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
543      {==}
544    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
545      {==}
546    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
547      {==}
548    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
549      {==}
550    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
551      {==}
552    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
553      {==}
554    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
555      {==}
556    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
557      {==}
558    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
559      {==}
560    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
561      {==}
562    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
563      {==}
564    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
565      {==}
566    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
567      {==}
568    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
569      {==}
570    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
571      {==}
572    case WCon{False{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
573      {==}
574    case WCon{True{}, WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
575      {==}
576    case WCon{False{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
577      {==}
578    case WCon{True{}, WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
579      {==}
580    case WCon{False{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
581      {==}
582    case WCon{True{}, WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
583      {==}
584    case WCon{False{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
585      {==}
586    case WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WCon{True{}, WNil{}}}}}}}}}:
587      {==}
588
589# The flags of the low 1 byte(s), as words of four bytes.
590law tkw1:
591  for +X0: Word(8n)
592  for +X1: Word(8n)
593  for +X2: Word(8n)
594  for +X3: Word(8n)
595  {Z.allz(32n, Word.and(32n, Z.zf(32n, Z.app8(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})))), Z.app8(24n, Z.one8(), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})))), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})))), True{}), Z.app8(24n, Z.h8(), Word.zero(24n)))) == Bool.and(Bool.not(Z.allz(8n, X0)), True{}) : Bool}
596
597def tkw1(X0, X1, X2, X3):
598  %Equal.sym(Bool, Z.allz(Nat.add(8n, 24n), Word.and(Nat.add(8n, 24n), Z.zf(Nat.add(8n, 24n), Z.app8(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})))), Z.app8(24n, Z.one8(), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})))), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})))), True{}), Z.app8(24n, Z.h8(), Word.zero(24n)))),
599    Bool.and(Bool.not(Z.allz(8n, X0)), Z.allz(24n, Word.and(24n, Z.zf(24n, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{}))), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{}))), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{}))), True{}), Word.zero(24n)))),
600    zbk_byte(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{}))), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{}))), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{}))), Word.zero(24n))) :
601    {_ == Bool.and(Bool.not(Z.allz(8n, X0)), True{}) : Bool}
602  %Equal.sym(Bool, Z.allz(24n, Word.and(24n, Z.zf(24n, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{}))), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{}))), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{}))), True{}), Word.zero(24n))), True{},
603    Z.allz_andz(24n, Z.zf(24n, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{}))), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{}))), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{}))), True{}))) :
604    {Bool.and(Bool.not(Z.allz(8n, X0)), _) == Bool.and(Bool.not(Z.allz(8n, X0)), True{}) : Bool}
605  {==}
606
607# The flags of the low 2 byte(s), as words of four bytes.
608law tkw2:
609  for +X0: Word(8n)
610  for +X1: Word(8n)
611  for +X2: Word(8n)
612  for +X3: Word(8n)
613  {Z.allz(32n, Word.and(32n, Z.zf(32n, Z.app8(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})))), Z.app8(24n, Z.one8(), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})))), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})))), True{}), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Word.zero(16n))))) == Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), True{})) : Bool}
614
615def tkw2(X0, X1, X2, X3):
616  %Equal.sym(Bool, Z.allz(Nat.add(8n, 24n), Word.and(Nat.add(8n, 24n), Z.zf(Nat.add(8n, 24n), Z.app8(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})))), Z.app8(24n, Z.one8(), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})))), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})))), True{}), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Word.zero(16n))))),
617    Bool.and(Bool.not(Z.allz(8n, X0)), Z.allz(24n, Word.and(24n, Z.zf(24n, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{}))), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{}))), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{}))), True{}), Z.app8(16n, Z.h8(), Word.zero(16n))))),
618    zbk_byte(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{}))), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{}))), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{}))), Z.app8(16n, Z.h8(), Word.zero(16n)))) :
619    {_ == Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), True{})) : Bool}
620  %Equal.sym(Bool, Z.allz(Nat.add(8n, 16n), Word.and(Nat.add(8n, 16n), Z.zf(Nat.add(8n, 16n), Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{}))), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{}))), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{}))), True{}), Z.app8(16n, Z.h8(), Word.zero(16n)))),
621    Bool.and(Bool.not(Z.allz(8n, X1)), Z.allz(16n, Word.and(16n, Z.zf(16n, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})), True{}), Word.zero(16n)))),
622    zbk_byte(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})), Word.zero(16n))) :
623    {Bool.and(Bool.not(Z.allz(8n, X0)), _) == Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), True{})) : Bool}
624  %Equal.sym(Bool, Z.allz(16n, Word.and(16n, Z.zf(16n, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})), True{}), Word.zero(16n))), True{},
625    Z.allz_andz(16n, Z.zf(16n, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})), True{}))) :
626    {Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), _)) == Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), True{})) : Bool}
627  {==}
628
629# The flags of the low 3 byte(s), as words of four bytes.
630law tkw3:
631  for +X0: Word(8n)
632  for +X1: Word(8n)
633  for +X2: Word(8n)
634  for +X3: Word(8n)
635  {Z.allz(32n, Word.and(32n, Z.zf(32n, Z.app8(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})))), Z.app8(24n, Z.one8(), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})))), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})))), True{}), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Word.zero(8n)))))) == Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), Bool.and(Bool.not(Z.allz(8n, X2)), True{}))) : Bool}
636
637def tkw3(X0, X1, X2, X3):
638  %Equal.sym(Bool, Z.allz(Nat.add(8n, 24n), Word.and(Nat.add(8n, 24n), Z.zf(Nat.add(8n, 24n), Z.app8(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})))), Z.app8(24n, Z.one8(), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})))), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})))), True{}), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Word.zero(8n)))))),
639    Bool.and(Bool.not(Z.allz(8n, X0)), Z.allz(24n, Word.and(24n, Z.zf(24n, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{}))), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{}))), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{}))), True{}), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Word.zero(8n)))))),
640    zbk_byte(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{}))), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{}))), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{}))), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Word.zero(8n))))) :
641    {_ == Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), Bool.and(Bool.not(Z.allz(8n, X2)), True{}))) : Bool}
642  %Equal.sym(Bool, Z.allz(Nat.add(8n, 16n), Word.and(Nat.add(8n, 16n), Z.zf(Nat.add(8n, 16n), Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{}))), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{}))), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{}))), True{}), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Word.zero(8n))))),
643    Bool.and(Bool.not(Z.allz(8n, X1)), Z.allz(16n, Word.and(16n, Z.zf(16n, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})), True{}), Z.app8(8n, Z.h8(), Word.zero(8n))))),
644    zbk_byte(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})), Z.app8(8n, Z.h8(), Word.zero(8n)))) :
645    {Bool.and(Bool.not(Z.allz(8n, X0)), _) == Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), Bool.and(Bool.not(Z.allz(8n, X2)), True{}))) : Bool}
646  %Equal.sym(Bool, Z.allz(Nat.add(8n, 8n), Word.and(Nat.add(8n, 8n), Z.zf(Nat.add(8n, 8n), Z.app8(8n, X2, Z.app8(0n, X3, WNil{})), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})), True{}), Z.app8(8n, Z.h8(), Word.zero(8n)))),
647    Bool.and(Bool.not(Z.allz(8n, X2)), Z.allz(8n, Word.and(8n, Z.zf(8n, Z.app8(0n, X3, WNil{}), Z.app8(0n, Z.one8(), WNil{}), Z.app8(0n, Z.h8(), WNil{}), True{}), Word.zero(8n)))),
648    zbk_byte(8n, X2, Z.app8(0n, X3, WNil{}), Z.app8(0n, Z.one8(), WNil{}), Z.app8(0n, Z.h8(), WNil{}), Word.zero(8n))) :
649    {Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), _)) == Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), Bool.and(Bool.not(Z.allz(8n, X2)), True{}))) : Bool}
650  %Equal.sym(Bool, Z.allz(8n, Word.and(8n, Z.zf(8n, Z.app8(0n, X3, WNil{}), Z.app8(0n, Z.one8(), WNil{}), Z.app8(0n, Z.h8(), WNil{}), True{}), Word.zero(8n))), True{},
651    Z.allz_andz(8n, Z.zf(8n, Z.app8(0n, X3, WNil{}), Z.app8(0n, Z.one8(), WNil{}), Z.app8(0n, Z.h8(), WNil{}), True{}))) :
652    {Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), Bool.and(Bool.not(Z.allz(8n, X2)), _))) == Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), Bool.and(Bool.not(Z.allz(8n, X2)), True{}))) : Bool}
653  {==}
654
655law tk1:
656  for +v: U32
657  {U32.is_zero(U32.and(W.zb(v), 128)) == Bool.and(U32.is_ne(W.byte(v, 0n), 0), True{}) : Bool}
658
659def tk1(v):
660  match v:
661    case U32{WCon{+c0, WCon{+c1, WCon{+c2, WCon{+c3, WCon{+c4, WCon{+c5, WCon{+c6, WCon{+c7, WCon{+c8, WCon{+c9, WCon{+c10, WCon{+c11, WCon{+c12, WCon{+c13, WCon{+c14, WCon{+c15, WCon{+c16, WCon{+c17, WCon{+c18, WCon{+c19, WCon{+c20, WCon{+c21, WCon{+c22, WCon{+c23, WCon{+c24, WCon{+c25, WCon{+c26, WCon{+c27, WCon{+c28, WCon{+c29, WCon{+c30, WCon{+c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
662      +X0 = {WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}} : Word(8n)}
663      +X1 = {WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WNil{}}}}}}}}} : Word(8n)}
664      +X2 = {WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WNil{}}}}}}}}} : Word(8n)}
665      +X3 = {WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}} : Word(8n)}
666      %Equal.sym(Bool, U32.is_ne(W.byte(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, 0n), 0), Bool.not(Z.allz(8n, X0)), Z.zb_ne0(c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31)) :
667        {U32.is_zero(U32.and(W.zb(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), 128)) == Bool.and(_, True{}) : Bool}
668      Equal.trans(Bool, Cmp.is_eq(Word.cmp(32n, Word.and(32n, Z.zf(32n, Z.app8(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})))), Z.app8(24n, Z.one8(), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})))), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})))), True{}), Z.app8(24n, Z.h8(), Word.zero(24n))), Word.zero(32n))), Z.allz(32n, Word.and(32n, Z.zf(32n, Z.app8(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})))), Z.app8(24n, Z.one8(), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})))), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})))), True{}), Z.app8(24n, Z.h8(), Word.zero(24n)))), Bool.and(Bool.not(Z.allz(8n, X0)), True{}),
669        Z.allz_cmp(32n, Word.and(32n, Z.zf(32n, Z.app8(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})))), Z.app8(24n, Z.one8(), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})))), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})))), True{}), Z.app8(24n, Z.h8(), Word.zero(24n)))), tkw1(X0, X1, X2, X3))
670
671law tk2:
672  for +v: U32
673  {U32.is_zero(U32.and(W.zb(v), 32896)) == Bool.and(U32.is_ne(W.byte(v, 0n), 0), Bool.and(U32.is_ne(W.byte(v, 1n), 0), True{})) : Bool}
674
675def tk2(v):
676  match v:
677    case U32{WCon{+c0, WCon{+c1, WCon{+c2, WCon{+c3, WCon{+c4, WCon{+c5, WCon{+c6, WCon{+c7, WCon{+c8, WCon{+c9, WCon{+c10, WCon{+c11, WCon{+c12, WCon{+c13, WCon{+c14, WCon{+c15, WCon{+c16, WCon{+c17, WCon{+c18, WCon{+c19, WCon{+c20, WCon{+c21, WCon{+c22, WCon{+c23, WCon{+c24, WCon{+c25, WCon{+c26, WCon{+c27, WCon{+c28, WCon{+c29, WCon{+c30, WCon{+c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
678      +X0 = {WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}} : Word(8n)}
679      +X1 = {WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WNil{}}}}}}}}} : Word(8n)}
680      +X2 = {WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WNil{}}}}}}}}} : Word(8n)}
681      +X3 = {WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}} : Word(8n)}
682      %Equal.sym(Bool, U32.is_ne(W.byte(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, 0n), 0), Bool.not(Z.allz(8n, X0)), Z.zb_ne0(c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31)) :
683        {U32.is_zero(U32.and(W.zb(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), 32896)) == Bool.and(_, Bool.and(U32.is_ne(W.byte(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, 1n), 0), True{})) : Bool}
684      %Equal.sym(Bool, U32.is_ne(W.byte(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, 1n), 0), Bool.not(Z.allz(8n, X1)), Z.zb_ne1(c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31)) :
685        {U32.is_zero(U32.and(W.zb(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), 32896)) == Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(_, True{})) : Bool}
686      Equal.trans(Bool, Cmp.is_eq(Word.cmp(32n, Word.and(32n, Z.zf(32n, Z.app8(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})))), Z.app8(24n, Z.one8(), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})))), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})))), True{}), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Word.zero(16n)))), Word.zero(32n))), Z.allz(32n, Word.and(32n, Z.zf(32n, Z.app8(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})))), Z.app8(24n, Z.one8(), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})))), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})))), True{}), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Word.zero(16n))))), Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), True{})),
687        Z.allz_cmp(32n, Word.and(32n, Z.zf(32n, Z.app8(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})))), Z.app8(24n, Z.one8(), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})))), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})))), True{}), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Word.zero(16n))))), tkw2(X0, X1, X2, X3))
688
689law tk3:
690  for +v: U32
691  {U32.is_zero(U32.and(W.zb(v), 8421504)) == Bool.and(U32.is_ne(W.byte(v, 0n), 0), Bool.and(U32.is_ne(W.byte(v, 1n), 0), Bool.and(U32.is_ne(W.byte(v, 2n), 0), True{}))) : Bool}
692
693def tk3(v):
694  match v:
695    case U32{WCon{+c0, WCon{+c1, WCon{+c2, WCon{+c3, WCon{+c4, WCon{+c5, WCon{+c6, WCon{+c7, WCon{+c8, WCon{+c9, WCon{+c10, WCon{+c11, WCon{+c12, WCon{+c13, WCon{+c14, WCon{+c15, WCon{+c16, WCon{+c17, WCon{+c18, WCon{+c19, WCon{+c20, WCon{+c21, WCon{+c22, WCon{+c23, WCon{+c24, WCon{+c25, WCon{+c26, WCon{+c27, WCon{+c28, WCon{+c29, WCon{+c30, WCon{+c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
696      +X0 = {WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}} : Word(8n)}
697      +X1 = {WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WNil{}}}}}}}}} : Word(8n)}
698      +X2 = {WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WNil{}}}}}}}}} : Word(8n)}
699      +X3 = {WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}} : Word(8n)}
700      %Equal.sym(Bool, U32.is_ne(W.byte(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, 0n), 0), Bool.not(Z.allz(8n, X0)), Z.zb_ne0(c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31)) :
701        {U32.is_zero(U32.and(W.zb(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), 8421504)) == Bool.and(_, Bool.and(U32.is_ne(W.byte(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, 1n), 0), Bool.and(U32.is_ne(W.byte(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, 2n), 0), True{}))) : Bool}
702      %Equal.sym(Bool, U32.is_ne(W.byte(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, 1n), 0), Bool.not(Z.allz(8n, X1)), Z.zb_ne1(c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31)) :
703        {U32.is_zero(U32.and(W.zb(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), 8421504)) == Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(_, Bool.and(U32.is_ne(W.byte(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, 2n), 0), True{}))) : Bool}
704      %Equal.sym(Bool, U32.is_ne(W.byte(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, 2n), 0), Bool.not(Z.allz(8n, X2)), Z.zb_ne2(c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31)) :
705        {U32.is_zero(U32.and(W.zb(U32{WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WCon{c8, WCon{c9, WCon{c10, WCon{c11, WCon{c12, WCon{c13, WCon{c14, WCon{c15, WCon{c16, WCon{c17, WCon{c18, WCon{c19, WCon{c20, WCon{c21, WCon{c22, WCon{c23, WCon{c24, WCon{c25, WCon{c26, WCon{c27, WCon{c28, WCon{c29, WCon{c30, WCon{c31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), 8421504)) == Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), Bool.and(_, True{}))) : Bool}
706      Equal.trans(Bool, Cmp.is_eq(Word.cmp(32n, Word.and(32n, Z.zf(32n, Z.app8(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})))), Z.app8(24n, Z.one8(), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})))), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})))), True{}), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Word.zero(8n))))), Word.zero(32n))), Z.allz(32n, Word.and(32n, Z.zf(32n, Z.app8(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})))), Z.app8(24n, Z.one8(), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})))), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})))), True{}), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Word.zero(8n)))))), Bool.and(Bool.not(Z.allz(8n, X0)), Bool.and(Bool.not(Z.allz(8n, X1)), Bool.and(Bool.not(Z.allz(8n, X2)), True{}))),
707        Z.allz_cmp(32n, Word.and(32n, Z.zf(32n, Z.app8(24n, X0, Z.app8(16n, X1, Z.app8(8n, X2, Z.app8(0n, X3, WNil{})))), Z.app8(24n, Z.one8(), Z.app8(16n, Z.one8(), Z.app8(8n, Z.one8(), Z.app8(0n, Z.one8(), WNil{})))), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Z.app8(0n, Z.h8(), WNil{})))), True{}), Z.app8(24n, Z.h8(), Z.app8(16n, Z.h8(), Z.app8(8n, Z.h8(), Word.zero(8n)))))), tkw3(X0, X1, X2, X3))
708