1	import Base
2	import ./proof_nat.bend as N
3	
4	# Facts about Word(n), n bits lowest first, as numbers: W(n, w) is
5	# Word.to_nat(n, w) and P(n) is 2^n. Proven once for every width by
6	# induction on n; proof_u32.bend specializes them to 32.
7	
8	# Numbers
9	# =======
10	
11	# The value of a word with head bit b and tail t.
12	law wcon:
13	  for +p: Nat
14	  for +b: Bool
15	  for +t: Word(p)
16	  {Word.to_nat(1n+p, WCon{b, t}) == Nat.add(N.bn(b), Nat.double(Word.to_nat(p, t))) : Nat}
17	
18	def wcon(p, b, t):
19	  match b:
20	    case False{}:
21	      {==}
22	    case True{}:
23	      {==}
24	
25	law bn_lt2:
26	  for +b: Bool
27	  {Nat.is_lt(N.bn(b), 2n) == True{} : Bool}
28	
29	def bn_lt2(b):
30	  match b:
31	    case False{}:
32	      {==}
33	    case True{}:
34	      {==}
35	
36	# The same value as t * 2 + b.
37	law wcon2:
38	  for +p: Nat
39	  for +b: Bool
40	  for +t: Word(p)
41	  {Word.to_nat(1n+p, WCon{b, t}) == Nat.add(Nat.mul(Word.to_nat(p, t), 2n), N.bn(b)) : Nat}
42	
43	def wcon2(p, b, t):
44	  +x = Word.to_nat(p, t)
45	  %Equal.sym(Nat, Nat.mul(x, 2n), Nat.double(x), N.mul2_r(x)) : {Word.to_nat(1n+p, WCon{b, t}) == Nat.add(_, N.bn(b)) : Nat}
46	  %N.add_comm(N.bn(b), Nat.double(x)) : {Word.to_nat(1n+p, WCon{b, t}) == _ : Nat}
47	  wcon(p, b, t)
48	
49	# b + 2x < 2y when x < y.
50	law lt_dbl_bit:
51	  for +x: Nat
52	  for +y: Nat
53	  for +b: Bool
54	  for +h: {Nat.is_lt(x, y) == True{} : Bool}
55	  {Nat.is_lt(Nat.add(N.bn(b), Nat.double(x)), Nat.double(y)) == True{} : Bool}
56	
57	def lt_dbl_bit(x, y, b, h):
58	  match x y:
59	    case _ 0n:
60	      Empty.absurd({Nat.is_lt(Nat.add(N.bn(b), Nat.double(x)), 0n) == True{} : Bool},
61	        N.false_ne_true(Equal.trans(Bool, False{}, Nat.is_lt(x, 0n), True{}, Equal.sym(Bool, Nat.is_lt(x, 0n), False{}, N.lt_zero(x)), h)))
62	    case 0n 1n+q:
63	      match b:
64	        case False{}:
65	          {==}
66	        case True{}:
67	          {==}
68	    case 1n+p 1n+q:
69	      match b:
70	        case False{}:
71	          lt_dbl_bit(p, q, False{}, h)
72	        case True{}:
73	          lt_dbl_bit(p, q, True{}, h)
74	
75	# b + 2x < 2y gives x < y.
76	law lt_dbl_inv:
77	  for +x: Nat
78	  for +y: Nat
79	  for +b: Bool
80	  for +h: {Nat.is_lt(Nat.add(N.bn(b), Nat.double(x)), Nat.double(y)) == True{} : Bool}
81	  {Nat.is_lt(x, y) == True{} : Bool}
82	
83	def lt_dbl_inv(x, y, b, h):
84	  match x y:
85	    case 0n 0n:
86	      match b:
87	        case False{}:
88	          Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, N.false_ne_true(h))
89	        case True{}:
90	          Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, N.false_ne_true(h))
91	    case 0n 1n+q:
92	      {==}
93	    case 1n+p 0n:
94	      match b:
95	        case False{}:
96	          Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, N.false_ne_true(h))
97	        case True{}:
98	          Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, N.false_ne_true(h))
99	    case 1n+p 1n+q:
100	      match b:
101	        case False{}:
102	          lt_dbl_inv(p, q, False{}, h)
103	        case True{}:
104	          lt_dbl_inv(p, q, True{}, h)
105	
106	# (b + 2x) % 2q = b + 2 (x % q).
107	law moddbl:
108	  for +b: Bool
109	  for +x: Nat
110	  for +q: Nat
111	  for +hq: {Nat.is_lt(0n, q) == True{} : Bool}
112	  {Nat.mod(Nat.add(N.bn(b), Nat.double(x)), Nat.double(q)) == Nat.add(N.bn(b), Nat.double(Nat.mod(x, q))) : Nat}
113	
114	def moddbl(b, x, q, hq):
115	  +d = Nat.div(x, q)
116	  +r = Nat.mod(x, q)
117	  +dq = Nat.double(q)
118	  %N.div_mod(x, q) : {Nat.mod(Nat.add(N.bn(b), Nat.double(_)), dq) == Nat.add(N.bn(b), Nat.double(r)) : Nat}
119	  %Equal.sym(Nat, Nat.double(Nat.add(Nat.mul(d, q), r)), Nat.add(Nat.double(Nat.mul(d, q)), Nat.double(r)), N.dbl_dist(Nat.mul(d, q), r)) :
120	    {Nat.mod(Nat.add(N.bn(b), _), dq) == Nat.add(N.bn(b), Nat.double(r)) : Nat}
121	  %N.mul_dbl_r(d, q) : {Nat.mod(Nat.add(N.bn(b), Nat.add(_, Nat.double(r))), dq) == Nat.add(N.bn(b), Nat.double(r)) : Nat}
122	  %N.add_left_comm(Nat.mul(d, dq), N.bn(b), Nat.double(r)) : {Nat.mod(_, dq) == Nat.add(N.bn(b), Nat.double(r)) : Nat}
123	  N.mod_mul_add(d, dq, Nat.add(N.bn(b), Nat.double(r)), lt_dbl_bit(r, q, b, N.mod_lt(x, q, hq)))
124	
125	# Every word stands for a number below 2^n.
126	law wlt:
127	  for +n: Nat
128	  for +w: Word(n)
129	  {Nat.is_lt(Word.to_nat(n, w), Nat.pow(2n, n)) == True{} : Bool}
130	
131	def wlt(n, w):
132	  match n:
133	    case 0n:
134	      match w:
135	        case WNil{}:
136	          {==}
137	    case 1n+p:
138	      match w:
139	        case WCon{+b, +t}:
140	          %Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.double(Nat.pow(2n, p)), N.pow2s(p)) :
141	            {Nat.is_lt(Word.to_nat(1n+p, WCon{b, t}), _) == True{} : Bool}
142	          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{b, t}), Nat.add(N.bn(b), Nat.double(Word.to_nat(p, t))), wcon(p, b, t)) :
143	            {Nat.is_lt(_, Nat.double(Nat.pow(2n, p))) == True{} : Bool}
144	          lt_dbl_bit(Word.to_nat(p, t), Nat.pow(2n, p), b, wlt(p, t))
145	
146	# r + c * m = x with r < m gives x % m = r.
147	law carry_mod:
148	  for +r: Nat
149	  for +c: Nat
150	  for +m: Nat
151	  for +x: Nat
152	  for +e: {Nat.add(r, Nat.mul(c, m)) == x : Nat}
153	  for +h: {Nat.is_lt(r, m) == True{} : Bool}
154	  {Nat.mod(x, m) == r : Nat}
155	
156	def carry_mod(r, c, m, x, e, h):
157	  %Equal.trans(Nat, Nat.add(Nat.mul(c, m), r), Nat.add(r, Nat.mul(c, m)), x, N.add_comm(Nat.mul(c, m), r), e) :
158	    {Nat.mod(_, m) == r : Nat}
159	  N.mod_mul_add(c, m, r, h)
160	
161	# Comparison
162	# ==========
163	
164	law cmp_dbl:
165	  for +x: Nat
166	  for +y: Nat
167	  for +a: Bool
168	  for +b: Bool
169	  {Word.cmp.fin(a, b, Nat.cmp(x, y)) == Nat.cmp(Nat.add(N.bn(a), Nat.double(x)), Nat.add(N.bn(b), Nat.double(y))) : Cmp}
170	
171	def cmp_dbl(x, y, a, b):
172	  match x y:
173	    case 0n 0n:
174	      match a b:
175	        case False{} False{}:
176	          {==}
177	        case False{} True{}:
178	          {==}
179	        case True{} False{}:
180	          {==}
181	        case True{} True{}:
182	          {==}
183	    case 0n 1n+q:
184	      match a b:
185	        case False{} False{}:
186	          {==}
187	        case False{} True{}:
188	          {==}
189	        case True{} False{}:
190	          {==}
191	        case True{} True{}:
192	          {==}
193	    case 1n+p 0n:
194	      match a b:
195	        case False{} False{}:
196	          {==}
197	        case False{} True{}:
198	          {==}
199	        case True{} False{}:
200	          {==}
201	        case True{} True{}:
202	          {==}
203	    case 1n+p 1n+q:
204	      match a b:
205	        case False{} False{}:
206	          cmp_dbl(p, q, False{}, False{})
207	        case False{} True{}:
208	          cmp_dbl(p, q, False{}, True{})
209	        case True{} False{}:
210	          cmp_dbl(p, q, True{}, False{})
211	        case True{} True{}:
212	          cmp_dbl(p, q, True{}, True{})
213	
214	# Words compare as their numbers.
215	law wcmp:
216	  for +n: Nat
217	  for +a: Word(n)
218	  for +b: Word(n)
219	  {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}
220	
221	def wcmp(n, a, b):
222	  match n:
223	    case 0n:
224	      match a b:
225	        case WNil{} WNil{}:
226	          {==}
227	    case 1n+p:
228	      match a b:
229	        case WCon{+x, +at} WCon{+y, +bt}:
230	          %Equal.sym(Cmp, Word.cmp(p, at, bt), Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt)), wcmp(p, at, bt)) :
231	            {Word.cmp.fin(x, y, _) == Nat.cmp(Word.to_nat(1n+p, WCon{x, at}), Word.to_nat(1n+p, WCon{y, bt})) : Cmp}
232	          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{x, at}), Nat.add(N.bn(x), Nat.double(Word.to_nat(p, at))), wcon(p, x, at)) :
233	            {Word.cmp.fin(x, y, Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt))) == Nat.cmp(_, Word.to_nat(1n+p, WCon{y, bt})) : Cmp}
234	          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{y, bt}), Nat.add(N.bn(y), Nat.double(Word.to_nat(p, bt))), wcon(p, y, bt)) :
235	            {Word.cmp.fin(x, y, Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt))) == Nat.cmp(Nat.add(N.bn(x), Nat.double(Word.to_nat(p, at))), _) : Cmp}
236	          cmp_dbl(Word.to_nat(p, at), Word.to_nat(p, bt), x, y)
237	
238	def Cmp.disc_eq(c: Cmp) -> Type:
239	  match c:
240	    case EQ{}:
241	      Empty
242	    case o:
243	      Unit
244	
245	def lt_ne_eq(e: {LT{} == EQ{} : Cmp}) -> Empty:
246	  %e : Cmp.disc_eq(_)
247	  Unit{}
248	
249	def gt_ne_eq(e: {GT{} == EQ{} : Cmp}) -> Empty:
250	  %e : Cmp.disc_eq(_)
251	  Unit{}
252	
253	def bool_cmp_eq(+a: Bool, +b: Bool, e: {Bool.cmp(a, b) == EQ{} : Cmp}) -> {a == b : Bool}:
254	  match a b:
255	    case False{} False{}:
256	      {==}
257	    case False{} True{}:
258	      Empty.absurd({False{} == True{} : Bool}, lt_ne_eq(e))
259	    case True{} False{}:
260	      Empty.absurd({True{} == False{} : Bool}, gt_ne_eq(e))
261	    case True{} True{}:
262	      {==}
263	
264	def word_fin_t(+ab: Bool, +bb: Bool, +t: Cmp, e: {Word.cmp.fin(ab, bb, t) == EQ{} : Cmp}) -> {t == EQ{} : Cmp}:
265	  match t:
266	    case LT{}:
267	      Empty.absurd({LT{} == EQ{} : Cmp}, lt_ne_eq(e))
268	    case EQ{}:
269	      {==}
270	    case GT{}:
271	      Empty.absurd({GT{} == EQ{} : Cmp}, gt_ne_eq(e))
272	
273	def word_fin_b(+ab: Bool, +bb: Bool, +t: Cmp, e: {Word.cmp.fin(ab, bb, t) == EQ{} : Cmp}) -> {Bool.cmp(ab, bb) == EQ{} : Cmp}:
274	  match t:
275	    case LT{}:
276	      Empty.absurd({Bool.cmp(ab, bb) == EQ{} : Cmp}, lt_ne_eq(e))
277	    case EQ{}:
278	      e
279	    case GT{}:
280	      Empty.absurd({Bool.cmp(ab, bb) == EQ{} : Cmp}, gt_ne_eq(e))
281	
282	def word_cmp_eq(+n: Nat, +a: Word(n), +b: Word(n), +e: {Word.cmp(n, a, b) == EQ{} : Cmp}) -> {a == b : Word(n)}:
283	  match n:
284	    case 0n:
285	      match a b:
286	        case WNil{} WNil{}:
287	          {==}
288	    case 1n+p:
289	      match a b:
290	        case WCon{+ab, +at} WCon{+bb, +bt}:
291	          %bool_cmp_eq(ab, bb, word_fin_b(ab, bb, Word.cmp(p, at, bt), e)) : {WCon{ab, at} == WCon{_, bt} : Word(1n+p)}
292	          %word_cmp_eq(p, at, bt, word_fin_t(ab, bb, Word.cmp(p, at, bt), e)) : {WCon{ab, at} == WCon{ab, _} : Word(1n+p)}
293	          {==}
294	
295	# Two words that stand for the same number are the same word.
296	law winj:
297	  for +n: Nat
298	  for +a: Word(n)
299	  for +b: Word(n)
300	  for +e: {Word.to_nat(n, a) == Word.to_nat(n, b) : Nat}
301	  {a == b : Word(n)}
302	
303	def winj(n, a, b, e):
304	  word_cmp_eq(n, a, b,
305	    %Equal.sym(Cmp, Word.cmp(n, a, b), Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)), wcmp(n, a, b)) : {_ == EQ{} : Cmp}
306	    %e : {Nat.cmp(Word.to_nat(n, a), _) == EQ{} : Cmp}
307	    N.cmp_refl(Word.to_nat(n, a)))
308	
309	# Increment, addition, subtraction
310	# ================================
311	
312	# The carry out of Word.inc: set when every bit is set.
313	def incc(n: Nat, w: Word(n)) -> Bool:
314	  match n:
315	    case 0n:
316	      True{}
317	    case 1n+p:
318	      match w:
319	        case WCon{False{}, t}:
320	          False{}
321	        case WCon{True{}, t}:
322	          incc(p, t)
323	
324	law winc:
325	  for +n: Nat
326	  for +w: Word(n)
327	  {Nat.add(Word.to_nat(n, Word.inc(n, w)), Nat.mul(N.bn(incc(n, w)), Nat.pow(2n, n))) == 1n+Word.to_nat(n, w) : Nat}
328	
329	def winc(n, w):
330	  match n:
331	    case 0n:
332	      match w:
333	        case WNil{}:
334	          {==}
335	    case 1n+p:
336	      match w:
337	        case WCon{False{}, +t}:
338	          %Equal.sym(Nat, Nat.add(Nat.double(Word.to_nat(p, t)), 0n), Nat.double(Word.to_nat(p, t)), N.add_zero(Nat.double(Word.to_nat(p, t)))) :
339	            {1n+_ == 1n+Nat.double(Word.to_nat(p, t)) : Nat}
340	          {==}
341	        case WCon{True{}, +t}:
342	          +i = Word.to_nat(p, Word.inc(p, t))
343	          +c = N.bn(incc(p, t))
344	          +pp = Nat.pow(2n, p)
345	          %Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.double(pp), N.pow2s(p)) :
346	            {Nat.add(Nat.double(i), Nat.mul(c, _)) == 2n+Nat.double(Word.to_nat(p, t)) : Nat}
347	          %Equal.sym(Nat, Nat.mul(c, Nat.double(pp)), Nat.double(Nat.mul(c, pp)), N.mul_dbl_r(c, pp)) :
348	            {Nat.add(Nat.double(i), _) == 2n+Nat.double(Word.to_nat(p, t)) : Nat}
349	          %N.dbl_dist(i, Nat.mul(c, pp)) : {_ == 2n+Nat.double(Word.to_nat(p, t)) : Nat}
350	          %Equal.sym(Nat, Nat.add(i, Nat.mul(c, pp)), 1n+Word.to_nat(p, t), winc(p, t)) : {Nat.double(_) == 2n+Nat.double(Word.to_nat(p, t)) : Nat}
351	          {==}
352	
353	# The carry out of Word.adc without inversion (f = False).
354	def cout(n: Nat, a: Word(n), b: Word(n), c: Bool) -> Bool:
355	  match n:
356	    case 0n:
357	      c
358	    case 1n+p:
359	      match a b:
360	        case WCon{False{}, at} WCon{bb, bt}:
361	          cout(p, at, bt, Bool.and(bb, c))
362	        case WCon{True{}, at} WCon{bb, bt}:
363	          cout(p, at, bt, Bool.or(bb, c))
364	
365	# One bit of the sum, as numbers.
366	law adc_step:
367	  for +p: Nat
368	  for +x: Nat
369	  for +y: Nat
370	  for +c: Nat
371	  for +s: Nat
372	  for +k: Nat
373	  for +a: Nat
374	  for +b: Nat
375	  for +r: Nat
376	  for +co: Nat
377	  for +ih: {Nat.add(r, Nat.mul(co, Nat.pow(2n, p))) == Nat.add(k, Nat.add(a, b)) : Nat}
378	  for +bit: {Nat.add(s, Nat.double(k)) == Nat.add(c, Nat.add(x, y)) : Nat}
379	  {Nat.add(Nat.add(s, Nat.double(r)), Nat.mul(co, Nat.pow(2n, 1n+p)))
380	    == Nat.add(c, Nat.add(Nat.add(x, Nat.double(a)), Nat.add(y, Nat.double(b)))) : Nat}
381	
382	def adc_step(p, x, y, c, s, k, a, b, r, co, ih, bit):
383	  +pp = Nat.pow(2n, p)
384	  +dr = Nat.double(r)
385	  +da = Nat.double(a)
386	  +db = Nat.double(b)
387	  +dk = Nat.double(k)
388	  +rhs = Nat.add(c, Nat.add(Nat.add(x, da), Nat.add(y, db)))
389	  %Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.double(pp), N.pow2s(p)) :
390	    {Nat.add(Nat.add(s, dr), Nat.mul(co, _)) == rhs : Nat}
391	  %Equal.sym(Nat, Nat.mul(co, Nat.double(pp)), Nat.double(Nat.mul(co, pp)), N.mul_dbl_r(co, pp)) :
392	    {Nat.add(Nat.add(s, dr), _) == rhs : Nat}
393	  %Equal.sym(Nat, Nat.add(Nat.add(s, dr), Nat.double(Nat.mul(co, pp))), Nat.add(s, Nat.add(dr, Nat.double(Nat.mul(co, pp)))),
394	      N.add_assoc(s, dr, Nat.double(Nat.mul(co, pp)))) :
395	    {_ == rhs : Nat}
396	  %N.dbl_dist(r, Nat.mul(co, pp)) : {Nat.add(s, _) == rhs : Nat}
397	  %Equal.sym(Nat, Nat.add(r, Nat.mul(co, pp)), Nat.add(k, Nat.add(a, b)), ih) : {Nat.add(s, Nat.double(_)) == rhs : Nat}
398	  %Equal.sym(Nat, Nat.double(Nat.add(k, Nat.add(a, b))), Nat.add(dk, Nat.double(Nat.add(a, b))), N.dbl_dist(k, Nat.add(a, b))) :
399	    {Nat.add(s, _) == rhs : Nat}
400	  %Equal.sym(Nat, Nat.double(Nat.add(a, b)), Nat.add(da, db), N.dbl_dist(a, b)) :
401	    {Nat.add(s, Nat.add(dk, _)) == rhs : Nat}
402	  %N.add_assoc(s, dk, Nat.add(da, db)) : {_ == rhs : Nat}
403	  %Equal.sym(Nat, Nat.add(s, dk), Nat.add(c, Nat.add(x, y)), bit) : {Nat.add(_, Nat.add(da, db)) == rhs : Nat}
404	  %Equal.sym(Nat, Nat.add(Nat.add(c, Nat.add(x, y)), Nat.add(da, db)), Nat.add(c, Nat.add(Nat.add(x, y), Nat.add(da, db))),
405	      N.add_assoc(c, Nat.add(x, y), Nat.add(da, db))) :
406	    {_ == rhs : Nat}
407	  %Equal.sym(Nat, Nat.add(Nat.add(x, y), Nat.add(da, db)), Nat.add(Nat.add(x, da), Nat.add(y, db)), N.add_swap(x, y, da, db)) :
408	    {Nat.add(c, _) == rhs : Nat}
409	  {==}
410	
411	# The sum with its carry out: r + co * 2^n = c + a + b.
412	law wadc:
413	  for +n: Nat
414	  for +a: Word(n)
415	  for +b: Word(n)
416	  for +c: Bool
417	  {Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.mul(N.bn(cout(n, a, b, c)), Nat.pow(2n, n)))
418	    == Nat.add(N.bn(c), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : Nat}
419	
420	def wadc(n, a, b, c):
421	  match n:
422	    case 0n:
423	      match a b c:
424	        case WNil{} WNil{} False{}:
425	          {==}
426	        case WNil{} WNil{} True{}:
427	          {==}
428	    case 1n+p:
429	      match a b c:
430	        case WCon{False{}, +at} WCon{False{}, +bt} False{}:
431	          adc_step(p, 0n, 0n, 0n, 0n, 0n, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})),
432	            N.bn(cout(p, at, bt, False{})), wadc(p, at, bt, False{}), {==})
433	        case WCon{False{}, +at} WCon{False{}, +bt} True{}:
434	          adc_step(p, 0n, 0n, 1n, 1n, 0n, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})),
435	            N.bn(cout(p, at, bt, False{})), wadc(p, at, bt, False{}), {==})
436	        case WCon{False{}, +at} WCon{True{}, +bt} False{}:
437	          adc_step(p, 0n, 1n, 0n, 1n, 0n, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})),
438	            N.bn(cout(p, at, bt, False{})), wadc(p, at, bt, False{}), {==})
439	        case WCon{False{}, +at} WCon{True{}, +bt} True{}:
440	          adc_step(p, 0n, 1n, 1n, 0n, 1n, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})),
441	            N.bn(cout(p, at, bt, True{})), wadc(p, at, bt, True{}), {==})
442	        case WCon{True{}, +at} WCon{False{}, +bt} False{}:
443	          adc_step(p, 1n, 0n, 0n, 1n, 0n, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.adc(p, at, bt, False{}, False{})),
444	            N.bn(cout(p, at, bt, False{})), wadc(p, at, bt, False{}), {==})
445	        case WCon{True{}, +at} WCon{False{}, +bt} True{}:
446	          adc_step(p, 1n, 0n, 1n, 0n, 1n, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})),
447	            N.bn(cout(p, at, bt, True{})), wadc(p, at, bt, True{}), {==})
448	        case WCon{True{}, +at} WCon{True{}, +bt} False{}:
449	          adc_step(p, 1n, 1n, 0n, 0n, 1n, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})),
450	            N.bn(cout(p, at, bt, True{})), wadc(p, at, bt, True{}), {==})
451	        case WCon{True{}, +at} WCon{True{}, +bt} True{}:
452	          adc_step(p, 1n, 1n, 1n, 1n, 1n, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.adc(p, at, bt, False{}, True{})),
453	            N.bn(cout(p, at, bt, True{})), wadc(p, at, bt, True{}), {==})
454	
455	# Subtraction is addition of the complement with carry in.
456	def adc_t.con(-p: Nat, at: Word(p), bt: Word(p), sk: Bool & Bool,
457	  ih: @k: Bool -> {Word.adc(p, at, bt, True{}, k) == Word.adc(p, at, Word.not(p, bt), False{}, k) : Word(p)}) ->
458	  {Word.adc.con(p, at, bt, True{}, sk) == Word.adc.con(p, at, Word.not(p, bt), False{}, sk) : Word(1n+p)}:
459	  match sk:
460	    case (s, k):
461	      %ih(k) : {WCon{s, Word.adc(p, at, bt, True{}, k)} == WCon{s, _} : Word(1n+p)}
462	      {==}
463	
464	law adc_t:
465	  for +n: Nat
466	  for +a: Word(n)
467	  for +b: Word(n)
468	  for +c: Bool
469	  {Word.adc(n, a, b, True{}, c) == Word.adc(n, a, Word.not(n, b), False{}, c) : Word(n)}
470	
471	def adc_t(n, a, b, c):
472	  match n:
473	    case 0n:
474	      match a b:
475	        case WNil{} WNil{}:
476	          {==}
477	    case 1n+p:
478	      match a b:
479	        case WCon{+ab, +at} WCon{+bb, +bt}:
480	          adc_t.con(p, at, bt, Bool.full_add(ab, Bool.not(bb), c), k => adc_t(p, at, bt, k))
481	
482	# not w and w add up to 2^n - 1.
483	law wnot:
484	  for +n: Nat
485	  for +w: Word(n)
486	  {1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) == Nat.pow(2n, n) : Nat}
487	
488	def wnot(n, w):
489	  match n:
490	    case 0n:
491	      match w:
492	        case WNil{}:
493	          {==}
494	    case 1n+p:
495	      match w:
496	        case WCon{False{}, +t}:
497	          +x = Word.to_nat(p, Word.not(p, t))
498	          +y = Word.to_nat(p, t)
499	          %Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.double(Nat.pow(2n, p)), N.pow2s(p)) : {2n+Nat.add(Nat.double(x), Nat.double(y)) == _ : Nat}
500	          %wnot(p, t) : {2n+Nat.add(Nat.double(x), Nat.double(y)) == Nat.double(_) : Nat}
501	          %Equal.sym(Nat, Nat.double(Nat.add(x, y)), Nat.add(Nat.double(x), Nat.double(y)), N.dbl_dist(x, y)) :
502	            {2n+Nat.add(Nat.double(x), Nat.double(y)) == 2n+_ : Nat}
503	          {==}
504	        case WCon{True{}, +t}:
505	          +x = Word.to_nat(p, Word.not(p, t))
506	          +y = Word.to_nat(p, t)
507	          %Equal.sym(Nat, Nat.add(Nat.double(x), 1n+Nat.double(y)), 1n+Nat.add(Nat.double(x), Nat.double(y)), N.add_succ(Nat.double(x), Nat.double(y))) :
508	            {1n+_ == Nat.pow(2n, 1n+p) : Nat}
509	          %Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.double(Nat.pow(2n, p)), N.pow2s(p)) : {2n+Nat.add(Nat.double(x), Nat.double(y)) == _ : Nat}
510	          %wnot(p, t) : {2n+Nat.add(Nat.double(x), Nat.double(y)) == Nat.double(_) : Nat}
511	          %Equal.sym(Nat, Nat.double(Nat.add(x, y)), Nat.add(Nat.double(x), Nat.double(y)), N.dbl_dist(x, y)) :
512	            {2n+Nat.add(Nat.double(x), Nat.double(y)) == 2n+_ : Nat}
513	          {==}
514	
515	# (a + 2^n) - b = 1 + a + not b.
516	law wsub_val:
517	  for +n: Nat
518	  for +a: Word(n)
519	  for +b: Word(n)
520	  {Nat.sub(Nat.add(Word.to_nat(n, a), Nat.pow(2n, n)), Word.to_nat(n, b))
521	    == 1n+Nat.add(Word.to_nat(n, a), Word.to_nat(n, Word.not(n, b))) : Nat}
522	
523	def wsub_val(n, a, b):
524	  +x = Word.to_nat(n, a)
525	  +y = Word.to_nat(n, b)
526	  +z = Word.to_nat(n, Word.not(n, b))
527	  %wnot(n, b) : {Nat.sub(Nat.add(x, _), y) == 1n+Nat.add(x, z) : Nat}
528	  %Equal.sym(Nat, Nat.add(x, 1n+Nat.add(z, y)), 1n+Nat.add(x, Nat.add(z, y)), N.add_succ(x, Nat.add(z, y))) :
529	    {Nat.sub(_, y) == 1n+Nat.add(x, z) : Nat}
530	  %N.add_assoc(x, z, y) : {Nat.sub(1n+_, y) == 1n+Nat.add(x, z) : Nat}
531	  N.sub_add(1n+Nat.add(x, z), y)
532	
533	# Shifts
534	# ======
535	
536	# The bit shifted out of the top by Word.shl.put.
537	def stop(n: Nat, c: Bool, w: Word(n)) -> Bool:
538	  match n:
539	    case 0n:
540	      c
541	    case 1n+p:
542	      match w:
543	        case WCon{b, t}:
544	          stop(p, b, t)
545	
546	law wput:
547	  for +n: Nat
548	  for +c: Bool
549	  for +w: Word(n)
550	  {Nat.add(Word.to_nat(n, Word.shl.put(n, c, w)), Nat.mul(N.bn(stop(n, c, w)), Nat.pow(2n, n)))
551	    == Nat.add(N.bn(c), Nat.double(Word.to_nat(n, w))) : Nat}
552	
553	def wput(n, c, w):
554	  match n:
555	    case 0n:
556	      match c w:
557	        case False{} WNil{}:
558	          {==}
559	        case True{} WNil{}:
560	          {==}
561	    case 1n+p:
562	      match w:
563	        case WCon{+b, +t}:
564	          +s = Word.to_nat(p, Word.shl.put(p, b, t))
565	          +o = N.bn(stop(p, b, t))
566	          +pp = Nat.pow(2n, p)
567	          +rhs = Nat.add(N.bn(c), Nat.double(Word.to_nat(1n+p, WCon{b, t})))
568	          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{c, Word.shl.put(p, b, t)}), Nat.add(N.bn(c), Nat.double(s)), wcon(p, c, Word.shl.put(p, b, t))) :
569	            {Nat.add(_, Nat.mul(o, Nat.pow(2n, 1n+p))) == rhs : Nat}
570	          %Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.double(pp), N.pow2s(p)) :
571	            {Nat.add(Nat.add(N.bn(c), Nat.double(s)), Nat.mul(o, _)) == rhs : Nat}
572	          %Equal.sym(Nat, Nat.mul(o, Nat.double(pp)), Nat.double(Nat.mul(o, pp)), N.mul_dbl_r(o, pp)) :
573	            {Nat.add(Nat.add(N.bn(c), Nat.double(s)), _) == rhs : Nat}
574	          %Equal.sym(Nat, Nat.add(Nat.add(N.bn(c), Nat.double(s)), Nat.double(Nat.mul(o, pp))), Nat.add(N.bn(c), Nat.add(Nat.double(s), Nat.double(Nat.mul(o, pp)))),
575	              N.add_assoc(N.bn(c), Nat.double(s), Nat.double(Nat.mul(o, pp)))) :
576	            {_ == rhs : Nat}
577	          %N.dbl_dist(s, Nat.mul(o, pp)) : {Nat.add(N.bn(c), _) == rhs : Nat}
578	          %Equal.sym(Nat, Nat.add(s, Nat.mul(o, pp)), Nat.add(N.bn(b), Nat.double(Word.to_nat(p, t))), wput(p, b, t)) :
579	            {Nat.add(N.bn(c), Nat.double(_)) == rhs : Nat}
580	          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{b, t}), Nat.add(N.bn(b), Nat.double(Word.to_nat(p, t))), wcon(p, b, t)) :
581	            {Nat.add(N.bn(c), Nat.double(Nat.add(N.bn(b), Nat.double(Word.to_nat(p, t))))) == Nat.add(N.bn(c), Nat.double(_)) : Nat}
582	          {==}
583	
584	# The bit shifted out of the top by Word.shl.
585	def shtop(n: Nat, w: Word(n)) -> Bool:
586	  match n:
587	    case 0n:
588	      False{}
589	    case 1n+p:
590	      match w:
591	        case WCon{b, t}:
592	          stop(p, b, t)
593	
594	law wshl:
595	  for +n: Nat
596	  for +w: Word(n)
597	  {Nat.add(Word.to_nat(n, Word.shl(n, w)), Nat.mul(N.bn(shtop(n, w)), Nat.pow(2n, n))) == Nat.double(Word.to_nat(n, w)) : Nat}
598	
599	def wshl(n, w):
600	  match n:
601	    case 0n:
602	      match w:
603	        case WNil{}:
604	          {==}
605	    case 1n+p:
606	      match w:
607	        case WCon{+b, +t}:
608	          +s = Word.to_nat(p, Word.shl.put(p, b, t))
609	          +o = N.bn(stop(p, b, t))
610	          +pp = Nat.pow(2n, p)
611	          +rhs = Nat.double(Word.to_nat(1n+p, WCon{b, t}))
612	          %Equal.sym(Nat, Nat.pow(2n, 1n+p), Nat.double(pp), N.pow2s(p)) :
613	            {Nat.add(Nat.double(s), Nat.mul(o, _)) == rhs : Nat}
614	          %Equal.sym(Nat, Nat.mul(o, Nat.double(pp)), Nat.double(Nat.mul(o, pp)), N.mul_dbl_r(o, pp)) :
615	            {Nat.add(Nat.double(s), _) == rhs : Nat}
616	          %N.dbl_dist(s, Nat.mul(o, pp)) : {_ == rhs : Nat}
617	          %Equal.sym(Nat, Nat.add(s, Nat.mul(o, pp)), Nat.add(N.bn(b), Nat.double(Word.to_nat(p, t))), wput(p, b, t)) :
618	            {Nat.double(_) == rhs : Nat}
619	          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{b, t}), Nat.add(N.bn(b), Nat.double(Word.to_nat(p, t))), wcon(p, b, t)) :
620	            {Nat.double(Nat.add(N.bn(b), Nat.double(Word.to_nat(p, t)))) == Nat.double(_) : Nat}
621	          {==}
622	
623	law wshl_mod:
624	  for +n: Nat
625	  for +w: Word(n)
626	  {Word.to_nat(n, Word.shl(n, w)) == Nat.mod(Nat.double(Word.to_nat(n, w)), Nat.pow(2n, n)) : Nat}
627	
628	def wshl_mod(n, w):
629	  Equal.sym(Nat, Nat.mod(Nat.double(Word.to_nat(n, w)), Nat.pow(2n, n)), Word.to_nat(n, Word.shl(n, w)),
630	    carry_mod(Word.to_nat(n, Word.shl(n, w)), N.bn(shtop(n, w)), Nat.pow(2n, n), Nat.double(Word.to_nat(n, w)),
631	      wshl(n, w), wlt(n, Word.shl(n, w))))
632	
633	law wpad:
634	  for +p: Nat
635	  for +t: Word(p)
636	  {Word.to_nat(1n+p, Word.shr.pad(p, t)) == Word.to_nat(p, t) : Nat}
637	
638	def wpad(p, t):
639	  match p:
640	    case 0n:
641	      match t:
642	        case WNil{}:
643	          {==}
644	    case 1n+q:
645	      match t:
646	        case WCon{False{}, +u}:
647	          Equal.cong(Nat, Nat, x => Nat.double(x), Word.to_nat(1n+q, Word.shr.pad(q, u)), Word.to_nat(q, u), wpad(q, u))
648	        case WCon{True{}, +u}:
649	          Equal.cong(Nat, Nat, x => 1n+Nat.double(x), Word.to_nat(1n+q, Word.shr.pad(q, u)), Word.to_nat(q, u), wpad(q, u))
650	
651	law wdiv2:
652	  for +p: Nat
653	  for +b: Bool
654	  for +t: Word(p)
655	  {Nat.div(Word.to_nat(1n+p, WCon{b, t}), 2n) == Word.to_nat(p, t) : Nat}
656	
657	def wdiv2(p, b, t):
658	  %Equal.sym(Nat, Word.to_nat(1n+p, WCon{b, t}), Nat.add(Nat.mul(Word.to_nat(p, t), 2n), N.bn(b)), wcon2(p, b, t)) :
659	    {Nat.div(_, 2n) == Word.to_nat(p, t) : Nat}
660	  N.div_mul_add(Word.to_nat(p, t), 2n, N.bn(b), bn_lt2(b))
661	
662	law wshr:
663	  for +n: Nat
664	  for +w: Word(n)
665	  {Word.to_nat(n, Word.shr(n, w)) == Nat.div(Word.to_nat(n, w), 2n) : Nat}
666	
667	def wshr(n, w):
668	  match n:
669	    case 0n:
670	      match w:
671	        case WNil{}:
672	          {==}
673	    case 1n+p:
674	      match w:
675	        case WCon{+b, +t}:
676	          Equal.trans(Nat, Word.to_nat(1n+p, Word.shr.pad(p, t)), Word.to_nat(p, t), Nat.div(Word.to_nat(1n+p, WCon{b, t}), 2n),
677	            wpad(p, t), Equal.sym(Nat, Nat.div(Word.to_nat(1n+p, WCon{b, t}), 2n), Word.to_nat(p, t), wdiv2(p, b, t)))
678	
679	# Addition and multiplication modulo 2^n
680	# ======================================
681	
682	law wadd_mod:
683	  for +n: Nat
684	  for +a: Word(n)
685	  for +b: Word(n)
686	  {Word.to_nat(n, Word.add(n, a, b)) == Nat.mod(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n)) : Nat}
687	
688	def wadd_mod(n, a, b):
689	  +r = Word.to_nat(n, Word.adc(n, a, b, False{}, False{}))
690	  Equal.sym(Nat, Nat.mod(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n)), r,
691	    carry_mod(r, N.bn(cout(n, a, b, False{})), Nat.pow(2n, n), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)),
692	      wadc(n, a, b, False{}), wlt(n, Word.adc(n, a, b, False{}, False{}))))
693	
694	law modmulin:
695	  for +x: Nat
696	  for +y: Nat
697	  for +z: Nat
698	  for +m: Nat
699	  {Nat.mod(Nat.add(x, Nat.mul(y, Nat.mod(z, m))), m) == Nat.mod(Nat.add(x, Nat.mul(y, z)), m) : Nat}
700	
701	def modmulin(x, y, z, m):
702	  %N.mod_add_mod_r(x, Nat.mul(y, Nat.mod(z, m)), m) : {_ == Nat.mod(Nat.add(x, Nat.mul(y, z)), m) : Nat}
703	  %Equal.sym(Nat, Nat.mod(Nat.mul(y, Nat.mod(z, m)), m), Nat.mod(Nat.mul(y, z), m), N.mod_mul_mod_r(y, z, m)) :
704	    {Nat.mod(Nat.add(x, _), m) == Nat.mod(Nat.add(x, Nat.mul(y, z)), m) : Nat}
705	  N.mod_add_mod_r(x, Nat.mul(y, z), m)
706	
707	law wmul_go:
708	  for +n: Nat
709	  for +m: Nat
710	  for +a: Word(m)
711	  for +b: Word(n)
712	  for +acc: Word(n)
713	  {Word.to_nat(n, Word.mul.go(n, m, a, b, acc))
714	    == Nat.mod(Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(m, a), Word.to_nat(n, b))), Nat.pow(2n, n)) : Nat}
715	
716	def wmul_go(n, m, a, b, acc):
717	  match m:
718	    case 0n:
719	      match a:
720	        case WNil{}:
721	          +c = Word.to_nat(n, acc)
722	          %Equal.sym(Nat, Nat.add(c, 0n), c, N.add_zero(c)) : {c == Nat.mod(_, Nat.pow(2n, n)) : Nat}
723	          Equal.sym(Nat, Nat.mod(c, Nat.pow(2n, n)), c, N.mod_small(c, Nat.pow(2n, n), wlt(n, acc)))
724	    case 1n+mp:
725	      match a:
726	        case WCon{False{}, +at}:
727	          +c = Word.to_nat(n, acc)
728	          +x = Word.to_nat(mp, at)
729	          +y = Word.to_nat(n, b)
730	          +pn = Nat.pow(2n, n)
731	          +rhs = Nat.mod(Nat.add(c, Nat.mul(Nat.double(x), y)), pn)
732	          Equal.trans(Nat, Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)),
733	            Nat.mod(Nat.add(c, Nat.mul(x, Word.to_nat(n, Word.shl(n, b)))), pn), rhs,
734	            wmul_go(n, mp, at, Word.shl(n, b), acc),
735	            %Equal.sym(Nat, Word.to_nat(n, Word.shl(n, b)), Nat.mod(Nat.double(y), pn), wshl_mod(n, b)) :
736	              {Nat.mod(Nat.add(c, Nat.mul(x, _)), pn) == rhs : Nat}
737	            %Equal.sym(Nat, Nat.mod(Nat.add(c, Nat.mul(x, Nat.mod(Nat.double(y), pn))), pn), Nat.mod(Nat.add(c, Nat.mul(x, Nat.double(y))), pn),
738	                modmulin(c, x, Nat.double(y), pn)) :
739	              {_ == rhs : Nat}
740	            %Equal.sym(Nat, Nat.mul(x, Nat.double(y)), Nat.double(Nat.mul(x, y)), N.mul_dbl_r(x, y)) :
741	              {Nat.mod(Nat.add(c, _), pn) == rhs : Nat}
742	            %Equal.sym(Nat, Nat.mul(Nat.double(x), y), Nat.double(Nat.mul(x, y)), N.mul_dbl_l(x, y)) :
743	              {Nat.mod(Nat.add(c, Nat.double(Nat.mul(x, y))), pn) == Nat.mod(Nat.add(c, _), pn) : Nat}
744	            {==})
745	        case WCon{True{}, +at}:
746	          +c = Word.to_nat(n, acc)
747	          +x = Word.to_nat(mp, at)
748	          +y = Word.to_nat(n, b)
749	          +pn = Nat.pow(2n, n)
750	          +rhs = Nat.mod(Nat.add(c, Nat.add(y, Nat.mul(Nat.double(x), y))), pn)
751	          Equal.trans(Nat, Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))),
752	            Nat.mod(Nat.add(Word.to_nat(n, Word.add(n, acc, b)), Nat.mul(x, Word.to_nat(n, Word.shl(n, b)))), pn), rhs,
753	            wmul_go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)),
754	            %Equal.sym(Nat, Word.to_nat(n, Word.add(n, acc, b)), Nat.mod(Nat.add(c, y), pn), wadd_mod(n, acc, b)) :
755	              {Nat.mod(Nat.add(_, Nat.mul(x, Word.to_nat(n, Word.shl(n, b)))), pn) == rhs : Nat}
756	            %Equal.sym(Nat, Word.to_nat(n, Word.shl(n, b)), Nat.mod(Nat.double(y), pn), wshl_mod(n, b)) :
757	              {Nat.mod(Nat.add(Nat.mod(Nat.add(c, y), pn), Nat.mul(x, _)), pn) == rhs : Nat}
758	            %Equal.sym(Nat, Nat.mod(Nat.add(Nat.mod(Nat.add(c, y), pn), Nat.mul(x, Nat.mod(Nat.double(y), pn))), pn),
759	                Nat.mod(Nat.add(Nat.add(c, y), Nat.mul(x, Nat.mod(Nat.double(y), pn))), pn),
760	                N.mod_add_mod_l(Nat.add(c, y), Nat.mul(x, Nat.mod(Nat.double(y), pn)), pn)) :
761	              {_ == rhs : Nat}
762	            %Equal.sym(Nat, Nat.mod(Nat.add(Nat.add(c, y), Nat.mul(x, Nat.mod(Nat.double(y), pn))), pn), Nat.mod(Nat.add(Nat.add(c, y), Nat.mul(x, Nat.double(y))), pn),
763	                modmulin(Nat.add(c, y), x, Nat.double(y), pn)) :
764	              {_ == rhs : Nat}
765	            %Equal.sym(Nat, Nat.mul(x, Nat.double(y)), Nat.double(Nat.mul(x, y)), N.mul_dbl_r(x, y)) :
766	              {Nat.mod(Nat.add(Nat.add(c, y), _), pn) == rhs : Nat}
767	            %Equal.sym(Nat, Nat.mul(Nat.double(x), y), Nat.double(Nat.mul(x, y)), N.mul_dbl_l(x, y)) :
768	              {Nat.mod(Nat.add(Nat.add(c, y), Nat.double(Nat.mul(x, y))), pn) == Nat.mod(Nat.add(c, Nat.add(y, _)), pn) : Nat}
769	            %Equal.sym(Nat, Nat.add(Nat.add(c, y), Nat.double(Nat.mul(x, y))), Nat.add(c, Nat.add(y, Nat.double(Nat.mul(x, y)))),
770	                N.add_assoc(c, y, Nat.double(Nat.mul(x, y)))) :
771	              {Nat.mod(_, pn) == Nat.mod(Nat.add(c, Nat.add(y, Nat.double(Nat.mul(x, y)))), pn) : Nat}
772	            {==})
773	
774	# Bits
775	# ====
776	
777	# Bit k of a word (False from n up).
778	def wbit(n: Nat, w: Word(n), k: Nat) -> Bool:
779	  match n:
780	    case 0n:
781	      False{}
782	    case 1n+p:
783	      match w:
784	        case WCon{b, t}:
785	          match k:
786	            case 0n:
787	              b
788	            case 1n+j:
789	              wbit(p, t, j)
790	
791	law is_eq_bn:
792	  for +b: Bool
793	  {Nat.is_eq(N.bn(b), 1n) == b : Bool}
794	
795	def is_eq_bn(b):
796	  match b:
797	    case False{}:
798	      {==}
799	    case True{}:
800	      {==}
801	
802	# The numeric bit (as in D.bit) is the word's bit.
803	law wbit_num:
804	  for +n: Nat
805	  for +w: Word(n)
806	  for +k: Nat
807	  {Nat.is_eq(Nat.mod(Nat.div(Word.to_nat(n, w), Nat.pow(2n, k)), 2n), 1n) == wbit(n, w, k) : Bool}
808	
809	def wbit_num(n, w, k):
810	  match n:
811	    case 0n:
812	      match w:
813	        case WNil{}:
814	          %Equal.sym(Nat, Nat.div(0n, Nat.pow(2n, k)), 0n, N.div_zero_l(Nat.pow(2n, k))) :
815	            {Nat.is_eq(Nat.mod(_, 2n), 1n) == False{} : Bool}
816	          {==}
817	    case 1n+p:
818	      match w:
819	        case WCon{+b, +t}:
820	          match k:
821	            case 0n:
822	              +x = Word.to_nat(1n+p, WCon{b, t})
823	              %Equal.sym(Nat, Nat.div(x, 1n), x, N.div_one(x)) : {Nat.is_eq(Nat.mod(_, 2n), 1n) == b : Bool}
824	              %Equal.sym(Nat, x, Nat.add(Nat.mul(Word.to_nat(p, t), 2n), N.bn(b)), wcon2(p, b, t)) : {Nat.is_eq(Nat.mod(_, 2n), 1n) == b : Bool}
825	              %Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(Word.to_nat(p, t), 2n), N.bn(b)), 2n), N.bn(b), N.mod_mul_add(Word.to_nat(p, t), 2n, N.bn(b), bn_lt2(b))) :
826	                {Nat.is_eq(_, 1n) == b : Bool}
827	              is_eq_bn(b)
828	            case 1n+j:
829	              +x = Word.to_nat(1n+p, WCon{b, t})
830	              %N.div_div(x, 2n, Nat.pow(2n, j)) : {Nat.is_eq(Nat.mod(_, 2n), 1n) == wbit(p, t, j) : Bool}
831	              %Equal.sym(Nat, Nat.div(x, 2n), Word.to_nat(p, t), wdiv2(p, b, t)) :
832	                {Nat.is_eq(Nat.mod(Nat.div(_, Nat.pow(2n, j)), 2n), 1n) == wbit(p, t, j) : Bool}
833	              wbit_num(p, t, j)
834	
835	law wbit_and:
836	  for +n: Nat
837	  for +a: Word(n)
838	  for +b: Word(n)
839	  for +k: Nat
840	  {wbit(n, Word.and(n, a, b), k) == Bool.and(wbit(n, a, k), wbit(n, b, k)) : Bool}
841	
842	def wbit_and(n, a, b, k):
843	  match n:
844	    case 0n:
845	      {==}
846	    case 1n+p:
847	      match a b:
848	        case WCon{+x, +at} WCon{+y, +bt}:
849	          match k:
850	            case 0n:
851	              {==}
852	            case 1n+j:
853	              wbit_and(p, at, bt, j)
854	
855	law wbit_or:
856	  for +n: Nat
857	  for +a: Word(n)
858	  for +b: Word(n)
859	  for +k: Nat
860	  {wbit(n, Word.or(n, a, b), k) == Bool.or(wbit(n, a, k), wbit(n, b, k)) : Bool}
861	
862	def wbit_or(n, a, b, k):
863	  match n:
864	    case 0n:
865	      {==}
866	    case 1n+p:
867	      match a b:
868	        case WCon{+x, +at} WCon{+y, +bt}:
869	          match k:
870	            case 0n:
871	              {==}
872	            case 1n+j:
873	              wbit_or(p, at, bt, j)
874	
875	law wbit_xor:
876	  for +n: Nat
877	  for +a: Word(n)
878	  for +b: Word(n)
879	  for +k: Nat
880	  {wbit(n, Word.xor(n, a, b), k) == Bool.xor(wbit(n, a, k), wbit(n, b, k)) : Bool}
881	
882	def wbit_xor(n, a, b, k):
883	  match n:
884	    case 0n:
885	      {==}
886	    case 1n+p:
887	      match a b:
888	        case WCon{+x, +at} WCon{+y, +bt}:
889	          match k:
890	            case 0n:
891	              {==}
892	            case 1n+j:
893	              wbit_xor(p, at, bt, j)
894	
895	law wbit_not:
896	  for +n: Nat
897	  for +a: Word(n)
898	  for +k: Nat
899	  {wbit(n, Word.not(n, a), k) == Bool.and(Nat.is_lt(k, n), Bool.not(wbit(n, a, k))) : Bool}
900	
901	def wbit_not(n, a, k):
902	  match n:
903	    case 0n:
904	      match k:
905	        case 0n:
906	          {==}
907	        case 1n+j:
908	          {==}
909	    case 1n+p:
910	      match a:
911	        case WCon{+x, +at}:
912	          match k:
913	            case 0n:
914	              {==}
915	            case 1n+j:
916	              wbit_not(p, at, j)
917	
918	# The lowest bit where two words differ (0 if they are equal).
919	def wdiff(n: Nat, a: Word(n), b: Word(n)) -> Nat:
920	  match n:
921	    case 0n:
922	      0n
923	    case 1n+p:
924	      match a b:
925	        case WCon{False{}, at} WCon{False{}, bt}:
926	          1n+wdiff(p, at, bt)
927	        case WCon{False{}, at} WCon{True{}, bt}:
928	          0n
929	        case WCon{True{}, at} WCon{False{}, bt}:
930	          0n
931	        case WCon{True{}, at} WCon{True{}, bt}:
932	          1n+wdiff(p, at, bt)
933	
934	# Two words with the same bit where they would first differ are equal.
935	law wext:
936	  for +n: Nat
937	  for +a: Word(n)
938	  for +b: Word(n)
939	  for +e: {wbit(n, a, wdiff(n, a, b)) == wbit(n, b, wdiff(n, a, b)) : Bool}
940	  {a == b : Word(n)}
941	
942	def wext(n, a, b, e):
943	  match n:
944	    case 0n:
945	      match a b:
946	        case WNil{} WNil{}:
947	          {==}
948	    case 1n+p:
949	      match a b:
950	        case WCon{False{}, +at} WCon{False{}, +bt}:
951	          %wext(p, at, bt, e) : {WCon{False{}, at} == WCon{False{}, _} : Word(1n+p)}
952	          {==}
953	        case WCon{False{}, +at} WCon{True{}, +bt}:
954	          Empty.absurd({WCon{False{}, at} == WCon{True{}, bt} : Word(1n+p)}, N.false_ne_true(e))
955	        case WCon{True{}, +at} WCon{False{}, +bt}:
956	          Empty.absurd({WCon{True{}, at} == WCon{False{}, bt} : Word(1n+p)}, N.true_ne_false(e))
957	        case WCon{True{}, +at} WCon{True{}, +bt}:
958	          %wext(p, at, bt, e) : {WCon{True{}, at} == WCon{True{}, _} : Word(1n+p)}
959	          {==}
960	
961	# Masks and disjoint words
962	# ========================
963	
964	law moddbl_w:
965	  for +p: Nat
966	  for +x: Bool
967	  for +t: Word(p)
968	  for +j: Nat
969	  {Nat.mod(Word.to_nat(1n+p, WCon{x, t}), Nat.pow(2n, 1n+j)) == Nat.add(N.bn(x), Nat.double(Nat.mod(Word.to_nat(p, t), Nat.pow(2n, j)))) : Nat}
970	
971	def moddbl_w(p, x, t, j):
972	  %Equal.sym(Nat, Word.to_nat(1n+p, WCon{x, t}), Nat.add(N.bn(x), Nat.double(Word.to_nat(p, t))), wcon(p, x, t)) :
973	    {Nat.mod(_, Nat.pow(2n, 1n+j)) == Nat.add(N.bn(x), Nat.double(Nat.mod(Word.to_nat(p, t), Nat.pow(2n, j)))) : Nat}
974	  %Equal.sym(Nat, Nat.pow(2n, 1n+j), Nat.double(Nat.pow(2n, j)), N.pow2s(j)) :
975	    {Nat.mod(Nat.add(N.bn(x), Nat.double(Word.to_nat(p, t))), _) == Nat.add(N.bn(x), Nat.double(Nat.mod(Word.to_nat(p, t), Nat.pow(2n, j)))) : Nat}
976	  moddbl(x, Word.to_nat(p, t), Nat.pow(2n, j), N.pow_pos(j))
977	
978	law lt_w:
979	  for +p: Nat
980	  for +y: Bool
981	  for +t: Word(p)
982	  for +j: Nat
983	  for +h: {Nat.is_lt(Word.to_nat(1n+p, WCon{y, t}), Nat.pow(2n, 1n+j)) == True{} : Bool}
984	  {Nat.is_lt(Word.to_nat(p, t), Nat.pow(2n, j)) == True{} : Bool}
985	
986	def lt_w(p, y, t, j, h):
987	  lt_dbl_inv(Word.to_nat(p, t), Nat.pow(2n, j), y,
988	    %wcon(p, y, t) : {Nat.is_lt(_, Nat.double(Nat.pow(2n, j))) == True{} : Bool}
989	    %N.pow2s(j) : {Nat.is_lt(Word.to_nat(1n+p, WCon{y, t}), _) == True{} : Bool}
990	    h)
991	
992	law mask_step:
993	  for +p: Nat
994	  for +x: Bool
995	  for +t: Word(p)
996	  for +j: Nat
997	  for +r: Nat
998	  for +ih: {r == Nat.mod(Word.to_nat(p, t), Nat.pow(2n, j)) : Nat}
999	  {Nat.add(N.bn(x), Nat.double(r)) == Nat.mod(Word.to_nat(1n+p, WCon{x, t}), Nat.pow(2n, 1n+j)) : Nat}
1000	
1001	def mask_step(p, x, t, j, r, ih):
1002	  %Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{x, t}), Nat.pow(2n, 1n+j)), Nat.add(N.bn(x), Nat.double(Nat.mod(Word.to_nat(p, t), Nat.pow(2n, j)))), moddbl_w(p, x, t, j)) :
1003	    {Nat.add(N.bn(x), Nat.double(r)) == _ : Nat}
1004	  %ih : {Nat.add(N.bn(x), Nat.double(r)) == Nat.add(N.bn(x), Nat.double(_)) : Nat}
1005	  {==}
1006	
1007	# And with a word standing for 2^k - 1 keeps the low k bits.
1008	law and_mask:
1009	  for +n: Nat
1010	  for +a: Word(n)
1011	  for +m: Word(n)
1012	  for +k: Nat
1013	  for +h: {Word.to_nat(n, m) == Nat.sub(Nat.pow(2n, k), 1n) : Nat}
1014	  {Word.to_nat(n, Word.and(n, a, m)) == Nat.mod(Word.to_nat(n, a), Nat.pow(2n, k)) : Nat}
1015	
1016	def and_mask(n, a, m, k, h):
1017	  match n:
1018	    case 0n:
1019	      match a m:
1020	        case WNil{} WNil{}:
1021	          Equal.sym(Nat, Nat.mod(0n, Nat.pow(2n, k)), 0n, N.mod_zero_l(Nat.pow(2n, k)))
1022	    case 1n+p:
1023	      match a m k:
1024	        case WCon{+x, +at} WCon{False{}, +mt} 0n:
1025	          +ih = and_mask(p, at, mt, 0n, N.dbl_zero(Word.to_nat(p, mt), h))
1026	          +r = Word.to_nat(p, Word.and(p, at, mt))
1027	          %Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{x, at}), 1n), 0n, N.mod_one(Word.to_nat(1n+p, WCon{x, at}))) :
1028	            {Word.to_nat(1n+p, WCon{Bool.and(x, False{}), Word.and(p, at, mt)}) == _ : Nat}
1029	          %Equal.sym(Bool, Bool.and(x, False{}), False{}, N.and_false_r(x)) :
1030	            {Word.to_nat(1n+p, WCon{_, Word.and(p, at, mt)}) == 0n : Nat}
1031	          %Equal.sym(Nat, r, Nat.mod(Word.to_nat(p, at), 1n), ih) : {Nat.double(_) == 0n : Nat}
1032	          %Equal.sym(Nat, Nat.mod(Word.to_nat(p, at), 1n), 0n, N.mod_one(Word.to_nat(p, at))) : {Nat.double(_) == 0n : Nat}
1033	          {==}
1034	        case WCon{+x, +at} WCon{True{}, +mt} 0n:
1035	          Empty.absurd({Word.to_nat(1n+p, WCon{Bool.and(x, True{}), Word.and(p, at, mt)}) == Nat.mod(Word.to_nat(1n+p, WCon{x, at}), 1n) : Nat},
1036	            N.succ_ne_zero(Nat.double(Word.to_nat(p, mt)), h))
1037	        case WCon{+x, +at} WCon{False{}, +mt} 1n+j:
1038	          Empty.absurd({Word.to_nat(1n+p, WCon{Bool.and(x, False{}), Word.and(p, at, mt)}) == Nat.mod(Word.to_nat(1n+p, WCon{x, at}), Nat.pow(2n, 1n+j)) : Nat},
1039	            N.dbl_ne_odd(Word.to_nat(p, mt), Nat.sub(Nat.pow(2n, j), 1n),
1040	              Equal.trans(Nat, Nat.double(Word.to_nat(p, mt)), Nat.sub(Nat.pow(2n, 1n+j), 1n), 1n+Nat.double(Nat.sub(Nat.pow(2n, j), 1n)), h, N.pow_sub1(j))))
1041	        case WCon{+x, +at} WCon{True{}, +mt} 1n+j:
1042	          +hm = N.dbl_inj(Word.to_nat(p, mt), Nat.sub(Nat.pow(2n, j), 1n),
1043	            N.succ_inj(Nat.double(Word.to_nat(p, mt)), Nat.double(Nat.sub(Nat.pow(2n, j), 1n)),
1044	              Equal.trans(Nat, 1n+Nat.double(Word.to_nat(p, mt)), Nat.sub(Nat.pow(2n, 1n+j), 1n), 1n+Nat.double(Nat.sub(Nat.pow(2n, j), 1n)), h, N.pow_sub1(j))))
1045	          %Equal.sym(Bool, Bool.and(x, True{}), x, N.and_true_r_id(x)) :
1046	            {Word.to_nat(1n+p, WCon{_, Word.and(p, at, mt)}) == Nat.mod(Word.to_nat(1n+p, WCon{x, at}), Nat.pow(2n, 1n+j)) : Nat}
1047	          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{x, Word.and(p, at, mt)}), Nat.add(N.bn(x), Nat.double(Word.to_nat(p, Word.and(p, at, mt)))), wcon(p, x, Word.and(p, at, mt))) :
1048	            {_ == Nat.mod(Word.to_nat(1n+p, WCon{x, at}), Nat.pow(2n, 1n+j)) : Nat}
1049	          mask_step(p, x, at, j, Word.to_nat(p, Word.and(p, at, mt)), and_mask(p, at, mt, j, hm))
1050	
1051	# x < 1 gives x = 0.
1052	law lt_one:
1053	  for +x: Nat
1054	  for +h: {Nat.is_lt(x, 1n) == True{} : Bool}
1055	  {x == 0n : Nat}
1056	
1057	def lt_one(x, h):
1058	  match x:
1059	    case 0n:
1060	      {==}
1061	    case 1n+p:
1062	      Empty.absurd({1n+p == 0n : Nat}, N.false_ne_true(Equal.trans(Bool, False{}, Nat.is_lt(p, 0n), True{}, Equal.sym(Bool, Nat.is_lt(p, 0n), False{}, N.lt_zero(p)), h)))
1063	
1064	law or_zero:
1065	  for +n: Nat
1066	  for +a: Word(n)
1067	  for +b: Word(n)
1068	  for +h: {Word.to_nat(n, b) == 0n : Nat}
1069	  {Word.to_nat(n, Word.or(n, a, b)) == Word.to_nat(n, a) : Nat}
1070	
1071	def or_zero(n, a, b, h):
1072	  match n:
1073	    case 0n:
1074	      match a b:
1075	        case WNil{} WNil{}:
1076	          {==}
1077	    case 1n+p:
1078	      match a b:
1079	        case WCon{False{}, +at} WCon{False{}, +bt}:
1080	          Equal.cong(Nat, Nat, z => Nat.double(z), Word.to_nat(p, Word.or(p, at, bt)), Word.to_nat(p, at), or_zero(p, at, bt, N.dbl_zero(Word.to_nat(p, bt), h)))
1081	        case WCon{True{}, +at} WCon{False{}, +bt}:
1082	          Equal.cong(Nat, Nat, z => 1n+Nat.double(z), Word.to_nat(p, Word.or(p, at, bt)), Word.to_nat(p, at), or_zero(p, at, bt, N.dbl_zero(Word.to_nat(p, bt), h)))
1083	        case WCon{+x, +at} WCon{True{}, +bt}:
1084	          Empty.absurd({Word.to_nat(1n+p, Word.or(1n+p, WCon{x, at}, WCon{True{}, bt})) == Word.to_nat(1n+p, WCon{x, at}) : Nat},
1085	            N.succ_ne_zero(Nat.double(Word.to_nat(p, bt)), h))
1086	
1087	law xor_zero:
1088	  for +n: Nat
1089	  for +a: Word(n)
1090	  for +b: Word(n)
1091	  for +h: {Word.to_nat(n, b) == 0n : Nat}
1092	  {Word.to_nat(n, Word.xor(n, a, b)) == Word.to_nat(n, a) : Nat}
1093	
1094	def xor_zero(n, a, b, h):
1095	  match n:
1096	    case 0n:
1097	      match a b:
1098	        case WNil{} WNil{}:
1099	          {==}
1100	    case 1n+p:
1101	      match a b:
1102	        case WCon{False{}, +at} WCon{False{}, +bt}:
1103	          Equal.cong(Nat, Nat, z => Nat.double(z), Word.to_nat(p, Word.xor(p, at, bt)), Word.to_nat(p, at), xor_zero(p, at, bt, N.dbl_zero(Word.to_nat(p, bt), h)))
1104	        case WCon{True{}, +at} WCon{False{}, +bt}:
1105	          Equal.cong(Nat, Nat, z => 1n+Nat.double(z), Word.to_nat(p, Word.xor(p, at, bt)), Word.to_nat(p, at), xor_zero(p, at, bt, N.dbl_zero(Word.to_nat(p, bt), h)))
1106	        case WCon{+x, +at} WCon{True{}, +bt}:
1107	          Empty.absurd({Word.to_nat(1n+p, Word.xor(1n+p, WCon{x, at}, WCon{True{}, bt})) == Word.to_nat(1n+p, WCon{x, at}) : Nat},
1108	            N.succ_ne_zero(Nat.double(Word.to_nat(p, bt)), h))
1109	
1110	# y + 2r = 2a + (y + 2b) when r = a + b.
1111	law split_step:
1112	  for +y: Bool
1113	  for +a: Nat
1114	  for +b: Nat
1115	  for +r: Nat
1116	  for +ih: {r == Nat.add(a, b) : Nat}
1117	  {Nat.add(N.bn(y), Nat.double(r)) == Nat.add(Nat.double(a), Nat.add(N.bn(y), Nat.double(b))) : Nat}
1118	
1119	def split_step(y, a, b, r, ih):
1120	  %Equal.sym(Nat, r, Nat.add(a, b), ih) : {Nat.add(N.bn(y), Nat.double(_)) == Nat.add(Nat.double(a), Nat.add(N.bn(y), Nat.double(b))) : Nat}
1121	  %Equal.sym(Nat, Nat.double(Nat.add(a, b)), Nat.add(Nat.double(a), Nat.double(b)), N.dbl_dist(a, b)) :
1122	    {Nat.add(N.bn(y), _) == Nat.add(Nat.double(a), Nat.add(N.bn(y), Nat.double(b))) : Nat}
1123	  N.add_left_comm(N.bn(y), Nat.double(a), Nat.double(b))
1124	
1125	def or_split.s(+p: Nat, +x: Bool, +y: Bool, +at: Word(p), +bt: Word(p), +j: Nat,
1126	  ha: {Nat.mod(Word.to_nat(1n+p, WCon{x, at}), Nat.pow(2n, 1n+j)) == 0n : Nat},
1127	  hb: {Nat.is_lt(Word.to_nat(1n+p, WCon{y, bt}), Nat.pow(2n, 1n+j)) == True{} : Bool},
1128	  ih: {Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)) == 0n : Nat} -> {Nat.is_lt(Word.to_nat(p, bt), Nat.pow(2n, j)) == True{} : Bool} ->
1129	    {Word.to_nat(p, Word.or(p, at, bt)) == Nat.add(Word.to_nat(p, at), Word.to_nat(p, bt)) : Nat}) ->
1130	  {Word.to_nat(1n+p, Word.or(1n+p, WCon{x, at}, WCon{y, bt})) == Nat.add(Word.to_nat(1n+p, WCon{x, at}), Word.to_nat(1n+p, WCon{y, bt})) : Nat}:
1131	  match x y:
1132	    case True{} _:
1133	      Empty.absurd({Word.to_nat(1n+p, Word.or(1n+p, WCon{True{}, at}, WCon{y, bt})) == Nat.add(Word.to_nat(1n+p, WCon{True{}, at}), Word.to_nat(1n+p, WCon{y, bt})) : Nat},
1134	        N.succ_ne_zero(Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))),
1135	          Equal.trans(Nat, 1n+Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), Nat.mod(Word.to_nat(1n+p, WCon{True{}, at}), Nat.pow(2n, 1n+j)), 0n,
1136	            Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{True{}, at}), Nat.pow(2n, 1n+j)), 1n+Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), moddbl_w(p, True{}, at, j)),
1137	            ha)))
1138	    case False{} False{}:
1139	      split_step(False{}, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.or(p, at, bt)),
1140	        ih(N.dbl_zero(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)),
1141	          Equal.trans(Nat, Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), 0n,
1142	            Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), moddbl_w(p, False{}, at, j)),
1143	            ha)))(lt_w(p, False{}, bt, j, hb)))
1144	    case False{} True{}:
1145	      split_step(True{}, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.or(p, at, bt)),
1146	        ih(N.dbl_zero(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)),
1147	          Equal.trans(Nat, Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), 0n,
1148	            Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), moddbl_w(p, False{}, at, j)),
1149	            ha)))(lt_w(p, True{}, bt, j, hb)))
1150	
1151	# Or of a word with only bits from k up and a word below 2^k is their sum.
1152	law or_split:
1153	  for +n: Nat
1154	  for +a: Word(n)
1155	  for +b: Word(n)
1156	  for +k: Nat
1157	  for +ha: {Nat.mod(Word.to_nat(n, a), Nat.pow(2n, k)) == 0n : Nat}
1158	  for +hb: {Nat.is_lt(Word.to_nat(n, b), Nat.pow(2n, k)) == True{} : Bool}
1159	  {Word.to_nat(n, Word.or(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
1160	
1161	def or_split(n, a, b, k, ha, hb):
1162	  match n:
1163	    case 0n:
1164	      match a b:
1165	        case WNil{} WNil{}:
1166	          {==}
1167	    case 1n+p:
1168	      match a b k:
1169	        case WCon{+x, +at} WCon{+y, +bt} 0n:
1170	          +ea = Word.to_nat(1n+p, WCon{x, at})
1171	          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{y, bt}), 0n, lt_one(Word.to_nat(1n+p, WCon{y, bt}), hb)) : {Word.to_nat(1n+p, Word.or(1n+p, WCon{x, at}, WCon{y, bt})) == Nat.add(ea, _) : Nat}
1172	          %Equal.sym(Nat, Nat.add(ea, 0n), ea, N.add_zero(ea)) : {Word.to_nat(1n+p, Word.or(1n+p, WCon{x, at}, WCon{y, bt})) == _ : Nat}
1173	          or_zero(1n+p, WCon{x, at}, WCon{y, bt}, lt_one(Word.to_nat(1n+p, WCon{y, bt}), hb))
1174	        case WCon{+x, +at} WCon{+y, +bt} 1n+j:
1175	          or_split.s(p, x, y, at, bt, j, ha, hb, ha2 => hb2 => or_split(p, at, bt, j, ha2, hb2))
1176	
1177	def xor_split.s(+p: Nat, +x: Bool, +y: Bool, +at: Word(p), +bt: Word(p), +j: Nat,
1178	  ha: {Nat.mod(Word.to_nat(1n+p, WCon{x, at}), Nat.pow(2n, 1n+j)) == 0n : Nat},
1179	  hb: {Nat.is_lt(Word.to_nat(1n+p, WCon{y, bt}), Nat.pow(2n, 1n+j)) == True{} : Bool},
1180	  ih: {Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)) == 0n : Nat} -> {Nat.is_lt(Word.to_nat(p, bt), Nat.pow(2n, j)) == True{} : Bool} ->
1181	    {Word.to_nat(p, Word.xor(p, at, bt)) == Nat.add(Word.to_nat(p, at), Word.to_nat(p, bt)) : Nat}) ->
1182	  {Word.to_nat(1n+p, Word.xor(1n+p, WCon{x, at}, WCon{y, bt})) == Nat.add(Word.to_nat(1n+p, WCon{x, at}), Word.to_nat(1n+p, WCon{y, bt})) : Nat}:
1183	  match x y:
1184	    case True{} _:
1185	      Empty.absurd({Word.to_nat(1n+p, Word.xor(1n+p, WCon{True{}, at}, WCon{y, bt})) == Nat.add(Word.to_nat(1n+p, WCon{True{}, at}), Word.to_nat(1n+p, WCon{y, bt})) : Nat},
1186	        N.succ_ne_zero(Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))),
1187	          Equal.trans(Nat, 1n+Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), Nat.mod(Word.to_nat(1n+p, WCon{True{}, at}), Nat.pow(2n, 1n+j)), 0n,
1188	            Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{True{}, at}), Nat.pow(2n, 1n+j)), 1n+Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), moddbl_w(p, True{}, at, j)),
1189	            ha)))
1190	    case False{} False{}:
1191	      split_step(False{}, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.xor(p, at, bt)),
1192	        ih(N.dbl_zero(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)),
1193	          Equal.trans(Nat, Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), 0n,
1194	            Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), moddbl_w(p, False{}, at, j)),
1195	            ha)))(lt_w(p, False{}, bt, j, hb)))
1196	    case False{} True{}:
1197	      split_step(True{}, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.xor(p, at, bt)),
1198	        ih(N.dbl_zero(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)),
1199	          Equal.trans(Nat, Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), 0n,
1200	            Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), moddbl_w(p, False{}, at, j)),
1201	            ha)))(lt_w(p, True{}, bt, j, hb)))
1202	
1203	# Xor likewise.
1204	law xor_split:
1205	  for +n: Nat
1206	  for +a: Word(n)
1207	  for +b: Word(n)
1208	  for +k: Nat
1209	  for +ha: {Nat.mod(Word.to_nat(n, a), Nat.pow(2n, k)) == 0n : Nat}
1210	  for +hb: {Nat.is_lt(Word.to_nat(n, b), Nat.pow(2n, k)) == True{} : Bool}
1211	  {Word.to_nat(n, Word.xor(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
1212	
1213	def xor_split(n, a, b, k, ha, hb):
1214	  match n:
1215	    case 0n:
1216	      match a b:
1217	        case WNil{} WNil{}:
1218	          {==}
1219	    case 1n+p:
1220	      match a b k:
1221	        case WCon{+x, +at} WCon{+y, +bt} 0n:
1222	          +ea = Word.to_nat(1n+p, WCon{x, at})
1223	          %Equal.sym(Nat, Word.to_nat(1n+p, WCon{y, bt}), 0n, lt_one(Word.to_nat(1n+p, WCon{y, bt}), hb)) : {Word.to_nat(1n+p, Word.xor(1n+p, WCon{x, at}, WCon{y, bt})) == Nat.add(ea, _) : Nat}
1224	          %Equal.sym(Nat, Nat.add(ea, 0n), ea, N.add_zero(ea)) : {Word.to_nat(1n+p, Word.xor(1n+p, WCon{x, at}, WCon{y, bt})) == _ : Nat}
1225	          xor_zero(1n+p, WCon{x, at}, WCon{y, bt}, lt_one(Word.to_nat(1n+p, WCon{y, bt}), hb))
1226	        case WCon{+x, +at} WCon{+y, +bt} 1n+j:
1227	          xor_split.s(p, x, y, at, bt, j, ha, hb, ha2 => hb2 => xor_split(p, at, bt, j, ha2, hb2))