1	import Base
2	import ./defs.bend as D
3	import ./proof_nat.bend as N
4	import ./proof_word.bend as W
5	import ./proof_u32.bend as U
6	
7	# Bytes in a word. Most laws compare two words bit by bit (U.bit_ext), with
8	# the bits of D.byte, shifts and 255 below.
9	
10	# Bool facts
11	# ==========
12	
13	law and_comm:
14	  for +a: Bool
15	  for +b: Bool
16	  {Bool.and(a, b) == Bool.and(b, a) : Bool}
17	
18	def and_comm(a, b):
19	  match a b:
20	    case False{} False{}:
21	      {==}
22	    case False{} True{}:
23	      {==}
24	    case True{} False{}:
25	      {==}
26	    case True{} True{}:
27	      {==}
28	
29	# and(a, and(b, and(c, d))) = and(b, and(a, d)) when a implies c.
30	law band_perm:
31	  for +a: Bool
32	  for +b: Bool
33	  for +c: Bool
34	  for +d: Bool
35	  for imp: {a == True{} : Bool} -> {c == True{} : Bool}
36	  {Bool.and(a, Bool.and(b, Bool.and(c, d))) == Bool.and(b, Bool.and(a, d)) : Bool}
37	
38	def band_perm(a, b, c, d, imp):
39	  match a:
40	    case False{}:
41	      Equal.sym(Bool, Bool.and(b, False{}), False{}, N.and_false_r(b))
42	    case True{}:
43	      %Equal.sym(Bool, c, True{}, imp({==})) : {Bool.and(b, Bool.and(_, d)) == Bool.and(b, d) : Bool}
44	      {==}
45	
46	# and(l, and(i, x)) = and(l, x) when l implies i.
47	law bimp:
48	  for +l: Bool
49	  for +i: Bool
50	  for +x: Bool
51	  for imp: {l == True{} : Bool} -> {i == True{} : Bool}
52	  {Bool.and(l, Bool.and(i, x)) == Bool.and(l, x) : Bool}
53	
54	def bimp(l, i, x, imp):
55	  match l:
56	    case False{}:
57	      {==}
58	    case True{}:
59	      %Equal.sym(Bool, i, True{}, imp({==})) : {Bool.and(_, x) == x : Bool}
60	      {==}
61	
62	# Bits of numbers
63	# ===============
64	
65	law lt_succ_self:
66	  for +j: Nat
67	  {Nat.is_lt(j, 1n+j) == True{} : Bool}
68	
69	def lt_succ_self(j):
70	  %Equal.sym(Bool, Nat.is_lt(j, 1n+j), Nat.is_le(j, j), N.lt_succ_iff(j, j)) : {_ == True{} : Bool}
71	  N.le_refl(j)
72	
73	# A word below 2^k has bit k clear.
74	law bit_zero_div:
75	  for +b: U32
76	  for +k: Nat
77	  for +h: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, k)) == True{} : Bool}
78	  {D.bit(b, k) == False{} : Bool}
79	
80	def bit_zero_div(b, k, h):
81	  %Equal.sym(Nat, Nat.div(U32.to_nat(b), Nat.pow(2n, k)), 0n, N.div_small(U32.to_nat(b), Nat.pow(2n, k), h)) :
82	    {Nat.is_eq(Nat.mod(_, 2n), 1n) == False{} : Bool}
83	  {==}
84	
85	law bit_lt_pow:
86	  for +b: U32
87	  for +n: Nat
88	  for +k: Nat
89	  for +hb: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, n)) == True{} : Bool}
90	  for +hk: {Nat.is_le(n, k) == True{} : Bool}
91	  {D.bit(b, k) == False{} : Bool}
92	
93	def bit_lt_pow(b, n, k, hb, hk):
94	  bit_zero_div(b, k, N.lt_le_trans(U32.to_nat(b), Nat.pow(2n, n), Nat.pow(2n, k), hb, N.pow_le(n, k, hk)))
95	
96	law bit_ge32:
97	  for +a: U32
98	  for +k: Nat
99	  for +hk: {Nat.is_le(32n, k) == True{} : Bool}
100	  {D.bit(a, k) == False{} : Bool}
101	
102	def bit_ge32(a, k, hk):
103	  bit_lt_pow(a, 32n, k, U.to_nat_lt_p(a), hk)
104	
105	def bit_lt32.go(+a: U32, +k: Nat, z: Bool, +ez: {Nat.is_lt(k, 32n) == z : Bool}) -> {D.bit(a, k) == Bool.and(z, D.bit(a, k)) : Bool}:
106	  match z:
107	    case True{}:
108	      {==}
109	    case False{}:
110	      bit_ge32(a, k, N.not_lt_le(k, 32n, ez))
111	
112	# Bits from 32 up are clear.
113	law bit_lt32:
114	  for +a: U32
115	  for +k: Nat
116	  {D.bit(a, k) == Bool.and(Nat.is_lt(k, 32n), D.bit(a, k)) : Bool}
117	
118	def bit_lt32(a, k):
119	  bit_lt32.go(a, k, Nat.is_lt(k, 32n), {==})
120	
121	law bit_zero:
122	  for +k: Nat
123	  {D.bit(0, k) == False{} : Bool}
124	
125	def bit_zero(k):
126	  bit_zero_div(0, k, N.pow_pos(k))
127	
128	law bit_shrn:
129	  for +a: U32
130	  for +s: Nat
131	  for +k: Nat
132	  {D.bit(U32.shrn(a, s), k) == D.bit(a, Nat.add(k, s)) : Bool}
133	
134	def bit_shrn(a, s, k):
135	  +x = U32.to_nat(a)
136	  +ps = Nat.pow(2n, s)
137	  +pk = Nat.pow(2n, k)
138	  %Equal.sym(Nat, U32.to_nat(U32.shrn(a, s)), Nat.div(x, ps), U.to_nat_shrn(a, s)) :
139	    {Nat.is_eq(Nat.mod(Nat.div(_, pk), 2n), 1n) == D.bit(a, Nat.add(k, s)) : Bool}
140	  %Equal.sym(Nat, Nat.div(Nat.div(x, ps), pk), Nat.div(x, Nat.mul(ps, pk)), N.div_div(x, ps, pk)) :
141	    {Nat.is_eq(Nat.mod(_, 2n), 1n) == D.bit(a, Nat.add(k, s)) : Bool}
142	  %N.mul_comm(pk, ps) : {Nat.is_eq(Nat.mod(Nat.div(x, _), 2n), 1n) == D.bit(a, Nat.add(k, s)) : Bool}
143	  %N.pow_add(2n, k, s) : {Nat.is_eq(Nat.mod(Nat.div(x, _), 2n), 1n) == D.bit(a, Nat.add(k, s)) : Bool}
144	  {==}
145	
146	# Bits of a left shift
147	# ====================
148	
149	law wbit_put:
150	  for +p: Nat
151	  for +c: Bool
152	  for +t: Word(p)
153	  for +j: Nat
154	  {W.wbit(p, Word.shl.put(p, c, t), j) == Bool.and(Nat.is_lt(j, p), W.wbit(1n+p, WCon{c, t}, j)) : Bool}
155	
156	def wbit_put(p, c, t, j):
157	  match p:
158	    case 0n:
159	      match t j:
160	        case WNil{} 0n:
161	          {==}
162	        case WNil{} 1n+i:
163	          {==}
164	    case 1n+q:
165	      match t j:
166	        case WCon{+b, +u} 0n:
167	          {==}
168	        case WCon{+b, +u} 1n+i:
169	          wbit_put(q, b, u, i)
170	
171	law bit_shl0:
172	  for +a: U32
173	  {D.bit(U32.shl(a), 0n) == False{} : Bool}
174	
175	def bit_shl0(a):
176	  match a:
177	    case U32{+x}:
178	      match x:
179	        case WCon{+b, +t}:
180	          U.bitw(Word.shl(32n, WCon{b, t}), 0n)
181	
182	law bit_shl1:
183	  for +a: U32
184	  for +j: Nat
185	  {D.bit(U32.shl(a), 1n+j) == Bool.and(Nat.is_lt(1n+j, 32n), D.bit(a, j)) : Bool}
186	
187	def bit_shl1(a, j):
188	  match a:
189	    case U32{+x}:
190	      match x:
191	        case WCon{+b, +t}:
192	          %Equal.sym(Bool, D.bit(U32{Word.shl(32n, WCon{b, t})}, 1n+j), W.wbit(32n, Word.shl(32n, WCon{b, t}), 1n+j), U.bitw(Word.shl(32n, WCon{b, t}), 1n+j)) :
193	            {_ == Bool.and(Nat.is_lt(1n+j, 32n), D.bit(U32{WCon{b, t}}, j)) : Bool}
194	          %Equal.sym(Bool, D.bit(U32{WCon{b, t}}, j), W.wbit(32n, WCon{b, t}, j), U.bitw(WCon{b, t}, j)) :
195	            {W.wbit(32n, Word.shl(32n, WCon{b, t}), 1n+j) == Bool.and(Nat.is_lt(1n+j, 32n), _) : Bool}
196	          wbit_put(31n, b, t, j)
197	
198	law bit_shln:
199	  for +a: U32
200	  for +s: Nat
201	  for +k: Nat
202	  {D.bit(U32.shln(a, s), k) == Bool.and(Nat.is_le(s, k), Bool.and(Nat.is_lt(k, 32n), D.bit(a, Nat.sub(k, s)))) : Bool}
203	
204	def bit_shln(a, s, k):
205	  match s:
206	    case 0n:
207	      %Equal.sym(Bool, Nat.is_le(0n, k), True{}, N.le_zero_l(k)) :
208	        {D.bit(a, k) == Bool.and(_, Bool.and(Nat.is_lt(k, 32n), D.bit(a, Nat.sub(k, 0n)))) : Bool}
209	      %Equal.sym(Nat, Nat.sub(k, 0n), k, N.sub_zero(k)) :
210	        {D.bit(a, k) == Bool.and(True{}, Bool.and(Nat.is_lt(k, 32n), D.bit(a, _))) : Bool}
211	      bit_lt32(a, k)
212	    case 1n+t:
213	      match k:
214	        case 0n:
215	          bit_shl0(U32.shln(a, t))
216	        case 1n+j:
217	          %Equal.sym(Bool, D.bit(U32.shl(U32.shln(a, t)), 1n+j), Bool.and(Nat.is_lt(1n+j, 32n), D.bit(U32.shln(a, t), j)), bit_shl1(U32.shln(a, t), j)) :
218	            {_ == Bool.and(Nat.is_le(t, j), Bool.and(Nat.is_lt(1n+j, 32n), D.bit(a, Nat.sub(j, t)))) : Bool}
219	          %Equal.sym(Bool, D.bit(U32.shln(a, t), j), Bool.and(Nat.is_le(t, j), Bool.and(Nat.is_lt(j, 32n), D.bit(a, Nat.sub(j, t)))), bit_shln(a, t, j)) :
220	            {Bool.and(Nat.is_lt(1n+j, 32n), _) == Bool.and(Nat.is_le(t, j), Bool.and(Nat.is_lt(1n+j, 32n), D.bit(a, Nat.sub(j, t)))) : Bool}
221	          band_perm(Nat.is_lt(1n+j, 32n), Nat.is_le(t, j), Nat.is_lt(j, 32n), D.bit(a, Nat.sub(j, t)),
222	            h => N.lt_trans(j, 1n+j, 32n, lt_succ_self(j), h))
223	
224	# 255 and bytes
225	# =============
226	
227	law bit_255:
228	  for +k: Nat
229	  {D.bit(255, k) == Nat.is_lt(k, 8n) : Bool}
230	
231	def bit_255(k):
232	  match k:
233	    case 0n:
234	      {==}
235	    case 1n+k1:
236	      match k1:
237	        case 0n:
238	          {==}
239	        case 1n+k2:
240	          match k2:
241	            case 0n:
242	              {==}
243	            case 1n+k3:
244	              match k3:
245	                case 0n:
246	                  {==}
247	                case 1n+k4:
248	                  match k4:
249	                    case 0n:
250	                      {==}
251	                    case 1n+k5:
252	                      match k5:
253	                        case 0n:
254	                          {==}
255	                        case 1n+k6:
256	                          match k6:
257	                            case 0n:
258	                              {==}
259	                            case 1n+k7:
260	                              match k7:
261	                                case 0n:
262	                                  {==}
263	                                case 1n+k8:
264	                                  Equal.trans(Bool, D.bit(255, 8n+k8), False{}, Nat.is_lt(8n+k8, 8n),
265	                                    bit_lt_pow(255, 8n, 8n+k8, {==}, N.le_zero_l(k8)),
266	                                    Equal.sym(Bool, Nat.is_lt(k8, 0n), False{}, N.lt_zero(k8)))
267	
268	# Bit k of byte j of w is bit 8j + k of w (and 0 from k = 8 up).
269	law bit_byte:
270	  for +w: U32
271	  for +j: Nat
272	  for +k: Nat
273	  {D.bit(D.byte(w, j), k) == Bool.and(Nat.is_lt(k, 8n), D.bit(w, Nat.add(Nat.mul(8n, j), k))) : Bool}
274	
275	def bit_byte(w, j, k):
276	  +s = Nat.mul(8n, j)
277	  %Equal.sym(Bool, D.bit(U32.and(U32.shrn(w, s), 255), k), Bool.and(D.bit(U32.shrn(w, s), k), D.bit(255, k)), U.bit_and(U32.shrn(w, s), 255, k)) :
278	    {_ == Bool.and(Nat.is_lt(k, 8n), D.bit(w, Nat.add(s, k))) : Bool}
279	  %Equal.sym(Bool, D.bit(U32.shrn(w, s), k), D.bit(w, Nat.add(k, s)), bit_shrn(w, s, k)) :
280	    {Bool.and(_, D.bit(255, k)) == Bool.and(Nat.is_lt(k, 8n), D.bit(w, Nat.add(s, k))) : Bool}
281	  %Equal.sym(Bool, D.bit(255, k), Nat.is_lt(k, 8n), bit_255(k)) :
282	    {Bool.and(D.bit(w, Nat.add(k, s)), _) == Bool.and(Nat.is_lt(k, 8n), D.bit(w, Nat.add(s, k))) : Bool}
283	  %N.add_comm(s, k) : {Bool.and(D.bit(w, _), Nat.is_lt(k, 8n)) == Bool.and(Nat.is_lt(k, 8n), D.bit(w, Nat.add(s, k))) : Bool}
284	  and_comm(D.bit(w, Nat.add(s, k)), Nat.is_lt(k, 8n))
285	
286	# More Bool facts
287	# ===============
288	
289	law band_dist:
290	  for +l: Bool
291	  for +x: Bool
292	  for +y: Bool
293	  {Bool.and(l, Bool.and(x, y)) == Bool.and(Bool.and(l, x), Bool.and(l, y)) : Bool}
294	
295	def band_dist(l, x, y):
296	  match l:
297	    case False{}:
298	      {==}
299	    case True{}:
300	      {==}
301	
302	law bor_dist:
303	  for +l: Bool
304	  for +x: Bool
305	  for +y: Bool
306	  {Bool.and(l, Bool.or(x, y)) == Bool.or(Bool.and(l, x), Bool.and(l, y)) : Bool}
307	
308	def bor_dist(l, x, y):
309	  match l:
310	    case False{}:
311	      {==}
312	    case True{}:
313	      {==}
314	
315	law bxor_dist:
316	  for +l: Bool
317	  for +x: Bool
318	  for +y: Bool
319	  {Bool.and(l, Bool.xor(x, y)) == Bool.xor(Bool.and(l, x), Bool.and(l, y)) : Bool}
320	
321	def bxor_dist(l, x, y):
322	  match l:
323	    case False{}:
324	      {==}
325	    case True{}:
326	      {==}
327	
328	law bnot_byte:
329	  for +l: Bool
330	  for +i: Bool
331	  for +x: Bool
332	  for imp: {l == True{} : Bool} -> {i == True{} : Bool}
333	  {Bool.and(l, Bool.and(i, Bool.not(x))) == Bool.xor(Bool.and(l, x), l) : Bool}
334	
335	def bnot_byte(l, i, x, imp):
336	  match l x:
337	    case False{} _:
338	      {==}
339	    case True{} False{}:
340	      %Equal.sym(Bool, i, True{}, imp({==})) : {Bool.and(_, True{}) == True{} : Bool}
341	      {==}
342	    case True{} True{}:
343	      %Equal.sym(Bool, i, True{}, imp({==})) : {Bool.and(_, False{}) == False{} : Bool}
344	      {==}
345	
346	law blow:
347	  for +l: Bool
348	  for +g: Bool
349	  for +y: Bool
350	  for imp: {l == True{} : Bool} -> {g == False{} : Bool}
351	  {Bool.and(l, Bool.and(g, y)) == False{} : Bool}
352	
353	def blow(l, g, y, imp):
354	  match l:
355	    case False{}:
356	      {==}
357	    case True{}:
358	      %Equal.sym(Bool, g, False{}, imp({==})) : {Bool.and(_, y) == False{} : Bool}
359	      {==}
360	
361	law bor_low:
362	  for +l: Bool
363	  for +x: Bool
364	  for +g: Bool
365	  for +y: Bool
366	  for imp: {l == True{} : Bool} -> {g == False{} : Bool}
367	  {Bool.and(l, Bool.or(x, Bool.and(g, y))) == Bool.and(l, x) : Bool}
368	
369	def bor_low(l, x, g, y, imp):
370	  match l:
371	    case False{}:
372	      {==}
373	    case True{}:
374	      %Equal.sym(Bool, g, False{}, imp({==})) : {Bool.or(x, Bool.and(_, y)) == x : Bool}
375	      N.or_false_r(x)
376	
377	law put_bits:
378	  for +l: Bool
379	  for +i: Bool
380	  for +x: Bool
381	  for +y: Bool
382	  for imp1: {l == True{} : Bool} -> {i == True{} : Bool}
383	  for imp2: {l == False{} : Bool} -> {y == False{} : Bool}
384	  {Bool.and(l, Bool.or(Bool.and(x, Bool.and(i, Bool.not(Bool.and(i, l)))), Bool.and(i, y))) == y : Bool}
385	
386	def put_bits(l, i, x, y, imp1, imp2):
387	  match l:
388	    case False{}:
389	      Equal.sym(Bool, y, False{}, imp2({==}))
390	    case True{}:
391	      %Equal.sym(Bool, i, True{}, imp1({==})) : {Bool.or(Bool.and(x, Bool.and(_, Bool.not(Bool.and(_, True{})))), Bool.and(_, y)) == y : Bool}
392	      %Equal.sym(Bool, Bool.and(x, False{}), False{}, N.and_false_r(x)) : {Bool.or(_, y) == y : Bool}
393	      {==}
394	
395	# Index arithmetic: byte j, bit k is bit 8j + k
396	# =============================================
397	
398	law lt_not_le:
399	  for +x: Nat
400	  for +y: Nat
401	  for +h: {Nat.is_lt(x, y) == True{} : Bool}
402	  {Nat.is_le(y, x) == False{} : Bool}
403	
404	def lt_not_le(x, y, h):
405	  match x y:
406	    case _ 0n:
407	      Empty.absurd({Nat.is_le(0n, x) == False{} : Bool}, N.false_ne_true(
408	        Equal.trans(Bool, False{}, Nat.is_lt(x, 0n), True{}, Equal.sym(Bool, Nat.is_lt(x, 0n), False{}, N.lt_zero(x)), h)))
409	    case 0n 1n+q:
410	      {==}
411	    case 1n+p 1n+q:
412	      lt_not_le(p, q, h)
413	
414	law idx32:
415	  for +j: Nat
416	  for +k: Nat
417	  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
418	  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
419	  {Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n) == True{} : Bool}
420	
421	def idx32(j, k, hj, hk):
422	  match j:
423	    case 0n:
424	      N.lt_trans(k, 8n, 32n, hk, {==})
425	    case 1n+j1:
426	      match j1:
427	        case 0n:
428	          N.lt_trans(k, 8n, 24n, hk, {==})
429	        case 1n+j2:
430	          match j2:
431	            case 0n:
432	              N.lt_trans(k, 8n, 16n, hk, {==})
433	            case 1n+j3:
434	              match j3:
435	                case 0n:
436	                  hk
437	                case 1n+j4:
438	                  Empty.absurd({Nat.is_lt(Nat.add(Nat.mul(8n, 4n+j4), k), 32n) == True{} : Bool}, N.false_ne_true(
439	                    Equal.trans(Bool, False{}, Nat.is_lt(j4, 0n), True{}, Equal.sym(Bool, Nat.is_lt(j4, 0n), False{}, N.lt_zero(j4)), hj)))
440	
441	# 8j + k < 8 (j + 1) for k < 8.
442	law lt_mul8:
443	  for +j: Nat
444	  for +k: Nat
445	  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
446	  {Nat.is_lt(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, 1n+j)) == True{} : Bool}
447	
448	def lt_mul8(j, k, hk):
449	  %Equal.sym(Nat, Nat.mul(8n, 1n+j), Nat.add(8n, Nat.mul(8n, j)), N.mul_succ_r(8n, j)) :
450	    {Nat.is_lt(Nat.add(Nat.mul(8n, j), k), _) == True{} : Bool}
451	  %N.add_comm(Nat.mul(8n, j), 8n) : {Nat.is_lt(Nat.add(Nat.mul(8n, j), k), _) == True{} : Bool}
452	  N.lt_add_l(Nat.mul(8n, j), k, 8n, hk)
453	
454	law idx_add:
455	  for +j: Nat
456	  for +s: Nat
457	  for +k: Nat
458	  {Nat.add(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, s)) == Nat.add(Nat.mul(8n, Nat.add(j, s)), k) : Nat}
459	
460	def idx_add(j, s, k):
461	  +a = Nat.mul(8n, j)
462	  +b = Nat.mul(8n, s)
463	  %Equal.sym(Nat, Nat.mul(8n, Nat.add(j, s)), Nat.add(a, b), N.mul_add(8n, j, s)) : {Nat.add(Nat.add(a, k), b) == Nat.add(_, k) : Nat}
464	  %Equal.sym(Nat, Nat.add(Nat.add(a, k), b), Nat.add(a, Nat.add(k, b)), N.add_assoc(a, k, b)) : {_ == Nat.add(Nat.add(a, b), k) : Nat}
465	  %Equal.sym(Nat, Nat.add(Nat.add(a, b), k), Nat.add(a, Nat.add(b, k)), N.add_assoc(a, b, k)) : {Nat.add(a, Nat.add(k, b)) == _ : Nat}
466	  %N.add_comm(k, b) : {Nat.add(a, Nat.add(k, b)) == Nat.add(a, _) : Nat}
467	  {==}
468	
469	law idx_sub:
470	  for +s: Nat
471	  for +j: Nat
472	  for +k: Nat
473	  for +hs: {Nat.is_le(s, j) == True{} : Bool}
474	  {Nat.sub(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, s)) == Nat.add(Nat.mul(8n, Nat.sub(j, s)), k) : Nat}
475	
476	def idx_sub(s, j, k, hs):
477	  +t = Nat.sub(j, s)
478	  %N.le_sub_add(s, j, hs) : {Nat.sub(Nat.add(Nat.mul(8n, _), k), Nat.mul(8n, s)) == Nat.add(Nat.mul(8n, t), k) : Nat}
479	  %Equal.sym(Nat, Nat.mul(8n, Nat.add(s, t)), Nat.add(Nat.mul(8n, s), Nat.mul(8n, t)), N.mul_add(8n, s, t)) :
480	    {Nat.sub(Nat.add(_, k), Nat.mul(8n, s)) == Nat.add(Nat.mul(8n, t), k) : Nat}
481	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(8n, s), Nat.mul(8n, t)), k), Nat.add(Nat.mul(8n, s), Nat.add(Nat.mul(8n, t), k)),
482	      N.add_assoc(Nat.mul(8n, s), Nat.mul(8n, t), k)) :
483	    {Nat.sub(_, Nat.mul(8n, s)) == Nat.add(Nat.mul(8n, t), k) : Nat}
484	  N.sub_add_l(Nat.mul(8n, s), Nat.add(Nat.mul(8n, t), k))
485	
486	law lt_sub:
487	  for +j: Nat
488	  for +r: Nat
489	  for +n: Nat
490	  for +h: {Nat.is_lt(Nat.add(j, r), n) == True{} : Bool}
491	  {Nat.is_lt(j, Nat.sub(n, r)) == True{} : Bool}
492	
493	def lt_sub(j, r, n, h):
494	  match r n:
495	    case 0n _:
496	      %Equal.sym(Nat, Nat.sub(n, 0n), n, N.sub_zero(n)) : {Nat.is_lt(j, _) == True{} : Bool}
497	      %N.add_zero(j) : {Nat.is_lt(_, n) == True{} : Bool}
498	      h
499	    case 1n+q 0n:
500	      Empty.absurd({Nat.is_lt(j, Nat.sub(0n, 1n+q)) == True{} : Bool}, N.false_ne_true(
501	        Equal.trans(Bool, False{}, Nat.is_lt(Nat.add(j, 1n+q), 0n), True{}, Equal.sym(Bool, Nat.is_lt(Nat.add(j, 1n+q), 0n), False{}, N.lt_zero(Nat.add(j, 1n+q))), h)))
502	    case 1n+q 1n+m:
503	      lt_sub(j, q, m, %N.add_succ(j, q) : {Nat.is_lt(_, 1n+m) == True{} : Bool}; h)
504	
505	law le_sub_l:
506	  for +n: Nat
507	  for +r: Nat
508	  for +j: Nat
509	  for +h: {Nat.is_le(n, Nat.add(j, r)) == True{} : Bool}
510	  {Nat.is_le(Nat.sub(n, r), j) == True{} : Bool}
511	
512	def le_sub_l(n, r, j, h):
513	  match n r:
514	    case _ 0n:
515	      %Equal.sym(Nat, Nat.sub(n, 0n), n, N.sub_zero(n)) : {Nat.is_le(_, j) == True{} : Bool}
516	      %N.add_zero(j) : {Nat.is_le(n, _) == True{} : Bool}
517	      h
518	    case 0n 1n+q:
519	      N.le_zero_l(j)
520	    case 1n+m 1n+q:
521	      le_sub_l(m, q, j, %N.add_succ(j, q) : {Nat.is_le(1n+m, _) == True{} : Bool}; h)
522	
523	law sub_sub_eq:
524	  for +j: Nat
525	  for +r: Nat
526	  for +n: Nat
527	  for +hr: {Nat.is_le(r, n) == True{} : Bool}
528	  {Nat.sub(j, Nat.sub(n, r)) == Nat.sub(Nat.add(j, r), n) : Nat}
529	
530	def sub_sub_eq(j, r, n, hr):
531	  match r n:
532	    case 0n _:
533	      %Equal.sym(Nat, Nat.sub(n, 0n), n, N.sub_zero(n)) : {Nat.sub(j, _) == Nat.sub(Nat.add(j, 0n), n) : Nat}
534	      %Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)) : {Nat.sub(j, n) == Nat.sub(_, n) : Nat}
535	      {==}
536	    case 1n+q 0n:
537	      Empty.absurd({Nat.sub(j, Nat.sub(0n, 1n+q)) == Nat.sub(Nat.add(j, 1n+q), 0n) : Nat}, N.false_ne_true(hr))
538	    case 1n+q 1n+m:
539	      %Equal.sym(Nat, Nat.add(j, 1n+q), 1n+Nat.add(j, q), N.add_succ(j, q)) : {Nat.sub(j, Nat.sub(m, q)) == Nat.sub(_, 1n+m) : Nat}
540	      sub_sub_eq(j, q, m, hr)
541	
542	# The byte laws
543	# =============
544	
545	law to_nat_byte:
546	  for +w: U32
547	  for +j: Nat
548	  {U32.to_nat(D.byte(w, j)) == Nat.mod(Nat.div(U32.to_nat(w), Nat.pow(2n, Nat.mul(8n, j))), Nat.pow(2n, 8n)) : Nat}
549	
550	def to_nat_byte(w, j):
551	  +s = Nat.mul(8n, j)
552	  %Equal.sym(Nat, U32.to_nat(U32.and(U32.shrn(w, s), 255)), Nat.mod(U32.to_nat(U32.shrn(w, s)), Nat.pow(2n, 8n)),
553	      U.to_nat_and_mask(U32.shrn(w, s), 255, 8n, {==})) :
554	    {_ == Nat.mod(Nat.div(U32.to_nat(w), Nat.pow(2n, s)), Nat.pow(2n, 8n)) : Nat}
555	  %Equal.sym(Nat, U32.to_nat(U32.shrn(w, s)), Nat.div(U32.to_nat(w), Nat.pow(2n, s)), U.to_nat_shrn(w, s)) :
556	    {Nat.mod(_, Nat.pow(2n, 8n)) == Nat.mod(Nat.div(U32.to_nat(w), Nat.pow(2n, s)), Nat.pow(2n, 8n)) : Nat}
557	  {==}
558	
559	law byte_lt:
560	  for +w: U32
561	  for +j: Nat
562	  {U32.is_lt(D.byte(w, j), 256) == True{} : Bool}
563	
564	def byte_lt(w, j):
565	  +x = Nat.div(U32.to_nat(w), Nat.pow(2n, Nat.mul(8n, j)))
566	  %Equal.sym(Bool, U32.is_lt(D.byte(w, j), 256), Nat.is_lt(U32.to_nat(D.byte(w, j)), U32.to_nat(256)), U.is_lt_to_nat(D.byte(w, j), 256)) :
567	    {_ == True{} : Bool}
568	  %Equal.sym(Nat, U32.to_nat(D.byte(w, j)), Nat.mod(x, Nat.pow(2n, 8n)), to_nat_byte(w, j)) :
569	    {Nat.is_lt(_, Nat.pow(2n, 8n)) == True{} : Bool}
570	  N.mod_lt(x, Nat.pow(2n, 8n), N.pow_pos(8n))
571	
572	def byte_and.k(+a: U32, +b: U32, +j: Nat, +k: Nat) -> {D.bit(D.byte(U32.and(a, b), j), k) == D.bit(U32.and(D.byte(a, j), D.byte(b, j)), k) : Bool}:
573	  +l = Nat.is_lt(k, 8n)
574	  +i = Nat.add(Nat.mul(8n, j), k)
575	  %Equal.sym(Bool, D.bit(D.byte(U32.and(a, b), j), k), Bool.and(l, D.bit(U32.and(a, b), i)), bit_byte(U32.and(a, b), j, k)) :
576	    {_ == D.bit(U32.and(D.byte(a, j), D.byte(b, j)), k) : Bool}
577	  %Equal.sym(Bool, D.bit(U32.and(a, b), i), Bool.and(D.bit(a, i), D.bit(b, i)), U.bit_and(a, b, i)) :
578	    {Bool.and(l, _) == D.bit(U32.and(D.byte(a, j), D.byte(b, j)), k) : Bool}
579	  %Equal.sym(Bool, D.bit(U32.and(D.byte(a, j), D.byte(b, j)), k), Bool.and(D.bit(D.byte(a, j), k), D.bit(D.byte(b, j), k)), U.bit_and(D.byte(a, j), D.byte(b, j), k)) :
580	    {Bool.and(l, Bool.and(D.bit(a, i), D.bit(b, i))) == _ : Bool}
581	  %Equal.sym(Bool, D.bit(D.byte(a, j), k), Bool.and(l, D.bit(a, i)), bit_byte(a, j, k)) :
582	    {Bool.and(l, Bool.and(D.bit(a, i), D.bit(b, i))) == Bool.and(_, D.bit(D.byte(b, j), k)) : Bool}
583	  %Equal.sym(Bool, D.bit(D.byte(b, j), k), Bool.and(l, D.bit(b, i)), bit_byte(b, j, k)) :
584	    {Bool.and(l, Bool.and(D.bit(a, i), D.bit(b, i))) == Bool.and(Bool.and(l, D.bit(a, i)), _) : Bool}
585	  band_dist(l, D.bit(a, i), D.bit(b, i))
586	
587	law byte_and:
588	  for +a: U32
589	  for +b: U32
590	  for +j: Nat
591	  {D.byte(U32.and(a, b), j) == U32.and(D.byte(a, j), D.byte(b, j)) : U32}
592	
593	def byte_and(a, b, j):
594	  U.bit_ext(D.byte(U32.and(a, b), j), U32.and(D.byte(a, j), D.byte(b, j)), k => byte_and.k(a, b, j, k))
595	
596	def byte_or.k(+a: U32, +b: U32, +j: Nat, +k: Nat) -> {D.bit(D.byte(U32.or(a, b), j), k) == D.bit(U32.or(D.byte(a, j), D.byte(b, j)), k) : Bool}:
597	  +l = Nat.is_lt(k, 8n)
598	  +i = Nat.add(Nat.mul(8n, j), k)
599	  %Equal.sym(Bool, D.bit(D.byte(U32.or(a, b), j), k), Bool.and(l, D.bit(U32.or(a, b), i)), bit_byte(U32.or(a, b), j, k)) :
600	    {_ == D.bit(U32.or(D.byte(a, j), D.byte(b, j)), k) : Bool}
601	  %Equal.sym(Bool, D.bit(U32.or(a, b), i), Bool.or(D.bit(a, i), D.bit(b, i)), U.bit_or(a, b, i)) :
602	    {Bool.and(l, _) == D.bit(U32.or(D.byte(a, j), D.byte(b, j)), k) : Bool}
603	  %Equal.sym(Bool, D.bit(U32.or(D.byte(a, j), D.byte(b, j)), k), Bool.or(D.bit(D.byte(a, j), k), D.bit(D.byte(b, j), k)), U.bit_or(D.byte(a, j), D.byte(b, j), k)) :
604	    {Bool.and(l, Bool.or(D.bit(a, i), D.bit(b, i))) == _ : Bool}
605	  %Equal.sym(Bool, D.bit(D.byte(a, j), k), Bool.and(l, D.bit(a, i)), bit_byte(a, j, k)) :
606	    {Bool.and(l, Bool.or(D.bit(a, i), D.bit(b, i))) == Bool.or(_, D.bit(D.byte(b, j), k)) : Bool}
607	  %Equal.sym(Bool, D.bit(D.byte(b, j), k), Bool.and(l, D.bit(b, i)), bit_byte(b, j, k)) :
608	    {Bool.and(l, Bool.or(D.bit(a, i), D.bit(b, i))) == Bool.or(Bool.and(l, D.bit(a, i)), _) : Bool}
609	  bor_dist(l, D.bit(a, i), D.bit(b, i))
610	
611	law byte_or:
612	  for +a: U32
613	  for +b: U32
614	  for +j: Nat
615	  {D.byte(U32.or(a, b), j) == U32.or(D.byte(a, j), D.byte(b, j)) : U32}
616	
617	def byte_or(a, b, j):
618	  U.bit_ext(D.byte(U32.or(a, b), j), U32.or(D.byte(a, j), D.byte(b, j)), k => byte_or.k(a, b, j, k))
619	
620	def byte_xor.k(+a: U32, +b: U32, +j: Nat, +k: Nat) -> {D.bit(D.byte(U32.xor(a, b), j), k) == D.bit(U32.xor(D.byte(a, j), D.byte(b, j)), k) : Bool}:
621	  +l = Nat.is_lt(k, 8n)
622	  +i = Nat.add(Nat.mul(8n, j), k)
623	  %Equal.sym(Bool, D.bit(D.byte(U32.xor(a, b), j), k), Bool.and(l, D.bit(U32.xor(a, b), i)), bit_byte(U32.xor(a, b), j, k)) :
624	    {_ == D.bit(U32.xor(D.byte(a, j), D.byte(b, j)), k) : Bool}
625	  %Equal.sym(Bool, D.bit(U32.xor(a, b), i), Bool.xor(D.bit(a, i), D.bit(b, i)), U.bit_xor(a, b, i)) :
626	    {Bool.and(l, _) == D.bit(U32.xor(D.byte(a, j), D.byte(b, j)), k) : Bool}
627	  %Equal.sym(Bool, D.bit(U32.xor(D.byte(a, j), D.byte(b, j)), k), Bool.xor(D.bit(D.byte(a, j), k), D.bit(D.byte(b, j), k)), U.bit_xor(D.byte(a, j), D.byte(b, j), k)) :
628	    {Bool.and(l, Bool.xor(D.bit(a, i), D.bit(b, i))) == _ : Bool}
629	  %Equal.sym(Bool, D.bit(D.byte(a, j), k), Bool.and(l, D.bit(a, i)), bit_byte(a, j, k)) :
630	    {Bool.and(l, Bool.xor(D.bit(a, i), D.bit(b, i))) == Bool.xor(_, D.bit(D.byte(b, j), k)) : Bool}
631	  %Equal.sym(Bool, D.bit(D.byte(b, j), k), Bool.and(l, D.bit(b, i)), bit_byte(b, j, k)) :
632	    {Bool.and(l, Bool.xor(D.bit(a, i), D.bit(b, i))) == Bool.xor(Bool.and(l, D.bit(a, i)), _) : Bool}
633	  bxor_dist(l, D.bit(a, i), D.bit(b, i))
634	
635	law byte_xor:
636	  for +a: U32
637	  for +b: U32
638	  for +j: Nat
639	  {D.byte(U32.xor(a, b), j) == U32.xor(D.byte(a, j), D.byte(b, j)) : U32}
640	
641	def byte_xor(a, b, j):
642	  U.bit_ext(D.byte(U32.xor(a, b), j), U32.xor(D.byte(a, j), D.byte(b, j)), k => byte_xor.k(a, b, j, k))
643	
644	def byte_not.k(+a: U32, +j: Nat, +hj: {Nat.is_lt(j, 4n) == True{} : Bool}, +k: Nat) ->
645	  {D.bit(D.byte(U32.not(a), j), k) == D.bit(U32.xor(D.byte(a, j), 255), k) : Bool}:
646	  +l = Nat.is_lt(k, 8n)
647	  +i = Nat.add(Nat.mul(8n, j), k)
648	  %Equal.sym(Bool, D.bit(D.byte(U32.not(a), j), k), Bool.and(l, D.bit(U32.not(a), i)), bit_byte(U32.not(a), j, k)) :
649	    {_ == D.bit(U32.xor(D.byte(a, j), 255), k) : Bool}
650	  %Equal.sym(Bool, D.bit(U32.not(a), i), Bool.and(Nat.is_lt(i, 32n), Bool.not(D.bit(a, i))), U.bit_not(a, i)) :
651	    {Bool.and(l, _) == D.bit(U32.xor(D.byte(a, j), 255), k) : Bool}
652	  %Equal.sym(Bool, D.bit(U32.xor(D.byte(a, j), 255), k), Bool.xor(D.bit(D.byte(a, j), k), D.bit(255, k)), U.bit_xor(D.byte(a, j), 255, k)) :
653	    {Bool.and(l, Bool.and(Nat.is_lt(i, 32n), Bool.not(D.bit(a, i)))) == _ : Bool}
654	  %Equal.sym(Bool, D.bit(D.byte(a, j), k), Bool.and(l, D.bit(a, i)), bit_byte(a, j, k)) :
655	    {Bool.and(l, Bool.and(Nat.is_lt(i, 32n), Bool.not(D.bit(a, i)))) == Bool.xor(_, D.bit(255, k)) : Bool}
656	  %Equal.sym(Bool, D.bit(255, k), l, bit_255(k)) :
657	    {Bool.and(l, Bool.and(Nat.is_lt(i, 32n), Bool.not(D.bit(a, i)))) == Bool.xor(Bool.and(l, D.bit(a, i)), _) : Bool}
658	  bnot_byte(l, Nat.is_lt(i, 32n), D.bit(a, i), hk => idx32(j, k, hj, hk))
659	
660	law byte_not:
661	  for +a: U32
662	  for +j: Nat
663	  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
664	  {D.byte(U32.not(a), j) == U32.xor(D.byte(a, j), 255) : U32}
665	
666	def byte_not(a, j, hj):
667	  U.bit_ext(D.byte(U32.not(a), j), U32.xor(D.byte(a, j), 255), k => byte_not.k(a, j, hj, k))
668	
669	def byte_shrn.k(+w: U32, +s: Nat, +j: Nat, +k: Nat) ->
670	  {D.bit(D.byte(U32.shrn(w, Nat.mul(8n, s)), j), k) == D.bit(D.byte(w, Nat.add(j, s)), k) : Bool}:
671	  +l = Nat.is_lt(k, 8n)
672	  +i = Nat.add(Nat.mul(8n, j), k)
673	  %Equal.sym(Bool, D.bit(D.byte(U32.shrn(w, Nat.mul(8n, s)), j), k), Bool.and(l, D.bit(U32.shrn(w, Nat.mul(8n, s)), i)), bit_byte(U32.shrn(w, Nat.mul(8n, s)), j, k)) :
674	    {_ == D.bit(D.byte(w, Nat.add(j, s)), k) : Bool}
675	  %Equal.sym(Bool, D.bit(U32.shrn(w, Nat.mul(8n, s)), i), D.bit(w, Nat.add(i, Nat.mul(8n, s))), bit_shrn(w, Nat.mul(8n, s), i)) :
676	    {Bool.and(l, _) == D.bit(D.byte(w, Nat.add(j, s)), k) : Bool}
677	  %Equal.sym(Bool, D.bit(D.byte(w, Nat.add(j, s)), k), Bool.and(l, D.bit(w, Nat.add(Nat.mul(8n, Nat.add(j, s)), k))), bit_byte(w, Nat.add(j, s), k)) :
678	    {Bool.and(l, D.bit(w, Nat.add(i, Nat.mul(8n, s)))) == _ : Bool}
679	  %idx_add(j, s, k) : {Bool.and(l, D.bit(w, Nat.add(i, Nat.mul(8n, s)))) == Bool.and(l, D.bit(w, _)) : Bool}
680	  {==}
681	
682	law byte_shrn:
683	  for +w: U32
684	  for +s: Nat
685	  for +j: Nat
686	  {D.byte(U32.shrn(w, Nat.mul(8n, s)), j) == D.byte(w, Nat.add(j, s)) : U32}
687	
688	def byte_shrn(w, s, j):
689	  U.bit_ext(D.byte(U32.shrn(w, Nat.mul(8n, s)), j), D.byte(w, Nat.add(j, s)), k => byte_shrn.k(w, s, j, k))
690	
691	def byte_shln_low.k(+w: U32, +s: Nat, +j: Nat, +hj: {Nat.is_lt(j, s) == True{} : Bool}, +k: Nat) ->
692	  {D.bit(D.byte(U32.shln(w, Nat.mul(8n, s)), j), k) == D.bit(0, k) : Bool}:
693	  +l = Nat.is_lt(k, 8n)
694	  +i = Nat.add(Nat.mul(8n, j), k)
695	  +s8 = Nat.mul(8n, s)
696	  %Equal.sym(Bool, D.bit(D.byte(U32.shln(w, s8), j), k), Bool.and(l, D.bit(U32.shln(w, s8), i)), bit_byte(U32.shln(w, s8), j, k)) :
697	    {_ == D.bit(0, k) : Bool}
698	  %Equal.sym(Bool, D.bit(U32.shln(w, s8), i), Bool.and(Nat.is_le(s8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(w, Nat.sub(i, s8)))), bit_shln(w, s8, i)) :
699	    {Bool.and(l, _) == D.bit(0, k) : Bool}
700	  %Equal.sym(Bool, D.bit(0, k), False{}, bit_zero(k)) :
701	    {Bool.and(l, Bool.and(Nat.is_le(s8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(w, Nat.sub(i, s8))))) == _ : Bool}
702	  blow(l, Nat.is_le(s8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(w, Nat.sub(i, s8))),
703	    hk => lt_not_le(i, s8, N.lt_le_trans(i, Nat.mul(8n, 1n+j), s8, lt_mul8(j, k, hk),
704	      N.le_mul_l(8n, 1n+j, s, %Equal.sym(Bool, Nat.is_le(1n+j, s), Nat.is_lt(j, s), N.le_succ_lt(j, s)) : {_ == True{} : Bool}; hj))))
705	
706	law byte_shln_low:
707	  for +w: U32
708	  for +s: Nat
709	  for +j: Nat
710	  for +hj: {Nat.is_lt(j, s) == True{} : Bool}
711	  {D.byte(U32.shln(w, Nat.mul(8n, s)), j) == 0 : U32}
712	
713	def byte_shln_low(w, s, j, hj):
714	  U.bit_ext(D.byte(U32.shln(w, Nat.mul(8n, s)), j), 0, k => byte_shln_low.k(w, s, j, hj, k))
715	
716	def byte_shln_high.k(+w: U32, +s: Nat, +j: Nat, +hs: {Nat.is_le(s, j) == True{} : Bool}, +hj: {Nat.is_lt(j, 4n) == True{} : Bool}, +k: Nat) ->
717	  {D.bit(D.byte(U32.shln(w, Nat.mul(8n, s)), j), k) == D.bit(D.byte(w, Nat.sub(j, s)), k) : Bool}:
718	  +l = Nat.is_lt(k, 8n)
719	  +i = Nat.add(Nat.mul(8n, j), k)
720	  +s8 = Nat.mul(8n, s)
721	  +x = D.bit(w, Nat.add(Nat.mul(8n, Nat.sub(j, s)), k))
722	  %Equal.sym(Bool, D.bit(D.byte(U32.shln(w, s8), j), k), Bool.and(l, D.bit(U32.shln(w, s8), i)), bit_byte(U32.shln(w, s8), j, k)) :
723	    {_ == D.bit(D.byte(w, Nat.sub(j, s)), k) : Bool}
724	  %Equal.sym(Bool, D.bit(U32.shln(w, s8), i), Bool.and(Nat.is_le(s8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(w, Nat.sub(i, s8)))), bit_shln(w, s8, i)) :
725	    {Bool.and(l, _) == D.bit(D.byte(w, Nat.sub(j, s)), k) : Bool}
726	  %Equal.sym(Bool, D.bit(D.byte(w, Nat.sub(j, s)), k), Bool.and(l, x), bit_byte(w, Nat.sub(j, s), k)) :
727	    {Bool.and(l, Bool.and(Nat.is_le(s8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(w, Nat.sub(i, s8))))) == _ : Bool}
728	  %Equal.sym(Bool, Nat.is_le(s8, i), True{}, N.le_trans(s8, Nat.mul(8n, j), i, N.le_mul_l(8n, s, j, hs), N.le_add_r(Nat.mul(8n, j), k))) :
729	    {Bool.and(l, Bool.and(_, Bool.and(Nat.is_lt(i, 32n), D.bit(w, Nat.sub(i, s8))))) == Bool.and(l, x) : Bool}
730	  %Equal.sym(Nat, Nat.sub(i, s8), Nat.add(Nat.mul(8n, Nat.sub(j, s)), k), idx_sub(s, j, k, hs)) :
731	    {Bool.and(l, Bool.and(True{}, Bool.and(Nat.is_lt(i, 32n), D.bit(w, _)))) == Bool.and(l, x) : Bool}
732	  bimp(l, Nat.is_lt(i, 32n), x, hk => idx32(j, k, hj, hk))
733	
734	law byte_shln_high:
735	  for +w: U32
736	  for +s: Nat
737	  for +j: Nat
738	  for +hs: {Nat.is_le(s, j) == True{} : Bool}
739	  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
740	  {D.byte(U32.shln(w, Nat.mul(8n, s)), j) == D.byte(w, Nat.sub(j, s)) : U32}
741	
742	def byte_shln_high(w, s, j, hs, hj):
743	  U.bit_ext(D.byte(U32.shln(w, Nat.mul(8n, s)), j), D.byte(w, Nat.sub(j, s)), k => byte_shln_high.k(w, s, j, hs, hj, k))
744	
745	# The bits of a merged word, at byte j, bit k.
746	law bit_merge:
747	  for +lo: U32
748	  for +hi: U32
749	  for +r: Nat
750	  for +j: Nat
751	  for +k: Nat
752	  {D.bit(D.byte(D.merge(lo, hi, r), j), k) == Bool.and(Nat.is_lt(k, 8n), Bool.or(D.bit(lo, Nat.add(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, r))),
753	    Bool.and(Nat.is_le(Nat.mul(8n, Nat.sub(4n, r)), Nat.add(Nat.mul(8n, j), k)), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n),
754	      D.bit(hi, Nat.sub(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, Nat.sub(4n, r)))))))) : Bool}
755	
756	def bit_merge(lo, hi, r, j, k):
757	  +l = Nat.is_lt(k, 8n)
758	  +i = Nat.add(Nat.mul(8n, j), k)
759	  +r8 = Nat.mul(8n, r)
760	  +u8 = Nat.mul(8n, Nat.sub(4n, r))
761	  %Equal.sym(Bool, D.bit(D.byte(D.merge(lo, hi, r), j), k), Bool.and(l, D.bit(D.merge(lo, hi, r), i)), bit_byte(D.merge(lo, hi, r), j, k)) :
762	    {_ == Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) : Bool}
763	  %Equal.sym(Bool, D.bit(U32.or(U32.shrn(lo, r8), U32.shln(hi, u8)), i), Bool.or(D.bit(U32.shrn(lo, r8), i), D.bit(U32.shln(hi, u8), i)), U.bit_or(U32.shrn(lo, r8), U32.shln(hi, u8), i)) :
764	    {Bool.and(l, _) == Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) : Bool}
765	  %Equal.sym(Bool, D.bit(U32.shrn(lo, r8), i), D.bit(lo, Nat.add(i, r8)), bit_shrn(lo, r8, i)) :
766	    {Bool.and(l, Bool.or(_, D.bit(U32.shln(hi, u8), i))) == Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) : Bool}
767	  %Equal.sym(Bool, D.bit(U32.shln(hi, u8), i), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))), bit_shln(hi, u8, i)) :
768	    {Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), _)) == Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) : Bool}
769	  {==}
770	
771	def byte_merge_lo.k(+lo: U32, +hi: U32, +r: Nat, +j: Nat, +h: {Nat.is_lt(Nat.add(j, r), 4n) == True{} : Bool}, +k: Nat) ->
772	  {D.bit(D.byte(D.merge(lo, hi, r), j), k) == D.bit(D.byte(lo, Nat.add(j, r)), k) : Bool}:
773	  +l = Nat.is_lt(k, 8n)
774	  +i = Nat.add(Nat.mul(8n, j), k)
775	  +r8 = Nat.mul(8n, r)
776	  +u8 = Nat.mul(8n, Nat.sub(4n, r))
777	  +y = Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))
778	  %Equal.sym(Bool, D.bit(D.byte(D.merge(lo, hi, r), j), k), Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), y))), bit_merge(lo, hi, r, j, k)) :
779	    {_ == D.bit(D.byte(lo, Nat.add(j, r)), k) : Bool}
780	  %Equal.sym(Bool, D.bit(D.byte(lo, Nat.add(j, r)), k), Bool.and(l, D.bit(lo, Nat.add(Nat.mul(8n, Nat.add(j, r)), k))), bit_byte(lo, Nat.add(j, r), k)) :
781	    {Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), y))) == _ : Bool}
782	  %idx_add(j, r, k) : {Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), y))) == Bool.and(l, D.bit(lo, _)) : Bool}
783	  bor_low(l, D.bit(lo, Nat.add(i, r8)), Nat.is_le(u8, i), y,
784	    hk => lt_not_le(i, u8, N.lt_le_trans(i, Nat.mul(8n, 1n+j), u8, lt_mul8(j, k, hk),
785	      N.le_mul_l(8n, 1n+j, Nat.sub(4n, r), %Equal.sym(Bool, Nat.is_le(1n+j, Nat.sub(4n, r)), Nat.is_lt(j, Nat.sub(4n, r)), N.le_succ_lt(j, Nat.sub(4n, r))) : {_ == True{} : Bool};
786	        lt_sub(j, r, 4n, h)))))
787	
788	law byte_merge_lo:
789	  for +lo: U32
790	  for +hi: U32
791	  for +r: Nat
792	  for +j: Nat
793	  for +h: {Nat.is_lt(Nat.add(j, r), 4n) == True{} : Bool}
794	  {D.byte(D.merge(lo, hi, r), j) == D.byte(lo, Nat.add(j, r)) : U32}
795	
796	def byte_merge_lo(lo, hi, r, j, h):
797	  U.bit_ext(D.byte(D.merge(lo, hi, r), j), D.byte(lo, Nat.add(j, r)), k => byte_merge_lo.k(lo, hi, r, j, h, k))
798	
799	def byte_merge_hi.k(+lo: U32, +hi: U32, +r: Nat, +j: Nat, +hr: {Nat.is_le(r, 4n) == True{} : Bool}, +hj: {Nat.is_lt(j, 4n) == True{} : Bool},
800	  +h: {Nat.is_le(4n, Nat.add(j, r)) == True{} : Bool}, +k: Nat) ->
801	  {D.bit(D.byte(D.merge(lo, hi, r), j), k) == D.bit(D.byte(hi, Nat.sub(Nat.add(j, r), 4n)), k) : Bool}:
802	  +l = Nat.is_lt(k, 8n)
803	  +i = Nat.add(Nat.mul(8n, j), k)
804	  +r8 = Nat.mul(8n, r)
805	  +u = Nat.sub(4n, r)
806	  +u8 = Nat.mul(8n, u)
807	  +hu = le_sub_l(4n, r, j, h)
808	  +x = D.bit(hi, Nat.add(Nat.mul(8n, Nat.sub(Nat.add(j, r), 4n)), k))
809	  %Equal.sym(Bool, D.bit(D.byte(D.merge(lo, hi, r), j), k),
810	      Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))), bit_merge(lo, hi, r, j, k)) :
811	    {_ == D.bit(D.byte(hi, Nat.sub(Nat.add(j, r), 4n)), k) : Bool}
812	  %Equal.sym(Bool, D.bit(D.byte(hi, Nat.sub(Nat.add(j, r), 4n)), k), Bool.and(l, x), bit_byte(hi, Nat.sub(Nat.add(j, r), 4n), k)) :
813	    {Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) == _ : Bool}
814	  %Equal.sym(Bool, D.bit(lo, Nat.add(i, r8)), False{}, bit_ge32(lo, Nat.add(i, r8),
815	      %Equal.sym(Nat, Nat.add(i, r8), Nat.add(Nat.mul(8n, Nat.add(j, r)), k), idx_add(j, r, k)) : {Nat.is_le(32n, _) == True{} : Bool}
816	      N.le_trans(32n, Nat.mul(8n, Nat.add(j, r)), Nat.add(Nat.mul(8n, Nat.add(j, r)), k), N.le_mul_l(8n, 4n, Nat.add(j, r), h), N.le_add_r(Nat.mul(8n, Nat.add(j, r)), k)))) :
817	    {Bool.and(l, Bool.or(_, Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) == Bool.and(l, x) : Bool}
818	  %Equal.sym(Bool, Nat.is_le(u8, i), True{}, N.le_trans(u8, Nat.mul(8n, j), i, N.le_mul_l(8n, u, j, hu), N.le_add_r(Nat.mul(8n, j), k))) :
819	    {Bool.and(l, Bool.or(False{}, Bool.and(_, Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) == Bool.and(l, x) : Bool}
820	  %Equal.sym(Nat, Nat.sub(i, u8), Nat.add(Nat.mul(8n, Nat.sub(j, u)), k), idx_sub(u, j, k, hu)) :
821	    {Bool.and(l, Bool.or(False{}, Bool.and(True{}, Bool.and(Nat.is_lt(i, 32n), D.bit(hi, _))))) == Bool.and(l, x) : Bool}
822	  %Equal.sym(Nat, Nat.sub(j, u), Nat.sub(Nat.add(j, r), 4n), sub_sub_eq(j, r, 4n, hr)) :
823	    {Bool.and(l, Bool.or(False{}, Bool.and(True{}, Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.add(Nat.mul(8n, _), k)))))) == Bool.and(l, x) : Bool}
824	  bimp(l, Nat.is_lt(i, 32n), x, hk => idx32(j, k, hj, hk))
825	
826	law byte_merge_hi:
827	  for +lo: U32
828	  for +hi: U32
829	  for +r: Nat
830	  for +j: Nat
831	  for +hr: {Nat.is_le(r, 4n) == True{} : Bool}
832	  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
833	  for +h: {Nat.is_le(4n, Nat.add(j, r)) == True{} : Bool}
834	  {D.byte(D.merge(lo, hi, r), j) == D.byte(hi, Nat.sub(Nat.add(j, r), 4n)) : U32}
835	
836	def byte_merge_hi(lo, hi, r, j, hr, hj, h):
837	  U.bit_ext(D.byte(D.merge(lo, hi, r), j), D.byte(hi, Nat.sub(Nat.add(j, r), 4n)), k => byte_merge_hi.k(lo, hi, r, j, hr, hj, h, k))
838	
839	# The bits of put_byte(w, j, b) at byte j, bit k.
840	def byte_put_same.k(+w: U32, +j: Nat, +b: U32, +hj: {Nat.is_lt(j, 4n) == True{} : Bool}, +hb: {U32.is_lt(b, 256) == True{} : Bool}, +k: Nat) ->
841	  {D.bit(D.byte(D.put_byte(w, j, b), j), k) == D.bit(b, k) : Bool}:
842	  +l = Nat.is_lt(k, 8n)
843	  +s = Nat.mul(8n, j)
844	  +i = Nat.add(s, k)
845	  +m = U32.shln(255, s)
846	  +ii = Nat.is_lt(i, 32n)
847	  %Equal.sym(Bool, D.bit(D.byte(D.put_byte(w, j, b), j), k), Bool.and(l, D.bit(D.put_byte(w, j, b), i)), bit_byte(D.put_byte(w, j, b), j, k)) :
848	    {_ == D.bit(b, k) : Bool}
849	  %Equal.sym(Bool, D.bit(U32.or(U32.and(w, U32.not(m)), U32.shln(b, s)), i), Bool.or(D.bit(U32.and(w, U32.not(m)), i), D.bit(U32.shln(b, s), i)),
850	      U.bit_or(U32.and(w, U32.not(m)), U32.shln(b, s), i)) :
851	    {Bool.and(l, _) == D.bit(b, k) : Bool}
852	  %Equal.sym(Bool, D.bit(U32.and(w, U32.not(m)), i), Bool.and(D.bit(w, i), D.bit(U32.not(m), i)), U.bit_and(w, U32.not(m), i)) :
853	    {Bool.and(l, Bool.or(_, D.bit(U32.shln(b, s), i))) == D.bit(b, k) : Bool}
854	  %Equal.sym(Bool, D.bit(U32.not(m), i), Bool.and(ii, Bool.not(D.bit(m, i))), U.bit_not(m, i)) :
855	    {Bool.and(l, Bool.or(Bool.and(D.bit(w, i), _), D.bit(U32.shln(b, s), i))) == D.bit(b, k) : Bool}
856	  %Equal.sym(Bool, D.bit(m, i), Bool.and(Nat.is_le(s, i), Bool.and(ii, D.bit(255, Nat.sub(i, s)))), bit_shln(255, s, i)) :
857	    {Bool.and(l, Bool.or(Bool.and(D.bit(w, i), Bool.and(ii, Bool.not(_))), D.bit(U32.shln(b, s), i))) == D.bit(b, k) : Bool}
858	  %Equal.sym(Bool, D.bit(U32.shln(b, s), i), Bool.and(Nat.is_le(s, i), Bool.and(ii, D.bit(b, Nat.sub(i, s)))), bit_shln(b, s, i)) :
859	    {Bool.and(l, Bool.or(Bool.and(D.bit(w, i), Bool.and(ii, Bool.not(Bool.and(Nat.is_le(s, i), Bool.and(ii, D.bit(255, Nat.sub(i, s))))))), _)) == D.bit(b, k) : Bool}
860	  %Equal.sym(Bool, Nat.is_le(s, i), True{}, N.le_add_r(s, k)) :
861	    {Bool.and(l, Bool.or(Bool.and(D.bit(w, i), Bool.and(ii, Bool.not(Bool.and(_, Bool.and(ii, D.bit(255, Nat.sub(i, s))))))),
862	      Bool.and(_, Bool.and(ii, D.bit(b, Nat.sub(i, s)))))) == D.bit(b, k) : Bool}
863	  %Equal.sym(Nat, Nat.sub(i, s), k, N.sub_add_l(s, k)) :
864	    {Bool.and(l, Bool.or(Bool.and(D.bit(w, i), Bool.and(ii, Bool.not(Bool.and(True{}, Bool.and(ii, D.bit(255, _)))))),
865	      Bool.and(True{}, Bool.and(ii, D.bit(b, _))))) == D.bit(b, k) : Bool}
866	  %Equal.sym(Bool, D.bit(255, k), l, bit_255(k)) :
867	    {Bool.and(l, Bool.or(Bool.and(D.bit(w, i), Bool.and(ii, Bool.not(Bool.and(True{}, Bool.and(ii, _))))),
868	      Bool.and(True{}, Bool.and(ii, D.bit(b, k))))) == D.bit(b, k) : Bool}
869	  put_bits(l, ii, D.bit(w, i), D.bit(b, k), hk => idx32(j, k, hj, hk),
870	    e => bit_lt_pow(b, 8n, k, %U.is_lt_to_nat(b, 256) : {_ == True{} : Bool}; hb, N.not_lt_le(k, 8n, e)))
871	
872	law byte_put_same:
873	  for +w: U32
874	  for +j: Nat
875	  for +b: U32
876	  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
877	  for +hb: {U32.is_lt(b, 256) == True{} : Bool}
878	  {D.byte(D.put_byte(w, j, b), j) == b : U32}
879	
880	def byte_put_same(w, j, b, hj, hb):
881	  U.bit_ext(D.byte(D.put_byte(w, j, b), j), b, k => byte_put_same.k(w, j, b, hj, hb, k))
882	
883	law other_bits:
884	  for +l: Bool
885	  for +g: Bool
886	  for +ii: Bool
887	  for +w: Bool
888	  for +z1: Bool
889	  for +z2: Bool
890	  for imp1: {l == True{} : Bool} -> {g == True{} : Bool} -> {z1 == False{} : Bool}
891	  for imp2: {l == True{} : Bool} -> {g == True{} : Bool} -> {z2 == False{} : Bool}
892	  {Bool.and(l, Bool.or(Bool.and(w, Bool.and(ii, Bool.not(Bool.and(g, Bool.and(ii, z1))))), Bool.and(g, Bool.and(ii, z2)))) == Bool.and(l, Bool.and(ii, w)) : Bool}
893	
894	def other_bits(l, g, ii, w, z1, z2, imp1, imp2):
895	  match l g ii w:
896	    case False{} _ _ _:
897	      {==}
898	    case True{} False{} True{} True{}:
899	      {==}
900	    case True{} False{} True{} False{}:
901	      {==}
902	    case True{} False{} False{} True{}:
903	      {==}
904	    case True{} False{} False{} False{}:
905	      {==}
906	    case True{} True{} True{} True{}:
907	      %Equal.sym(Bool, z1, False{}, imp1({==})({==})) :
908	        {Bool.and(True{}, Bool.or(Bool.and(True{}, Bool.and(True{}, Bool.not(Bool.and(True{}, Bool.and(True{}, _))))), Bool.and(True{}, Bool.and(True{}, z2)))) == Bool.and(True{}, Bool.and(True{}, True{})) : Bool}
909	      %Equal.sym(Bool, z2, False{}, imp2({==})({==})) :
910	        {Bool.and(True{}, Bool.or(Bool.and(True{}, Bool.and(True{}, Bool.not(Bool.and(True{}, Bool.and(True{}, False{}))))), Bool.and(True{}, Bool.and(True{}, _)))) == Bool.and(True{}, Bool.and(True{}, True{})) : Bool}
911	      {==}
912	    case True{} True{} True{} False{}:
913	      %Equal.sym(Bool, z1, False{}, imp1({==})({==})) :
914	        {Bool.and(True{}, Bool.or(Bool.and(False{}, Bool.and(True{}, Bool.not(Bool.and(True{}, Bool.and(True{}, _))))), Bool.and(True{}, Bool.and(True{}, z2)))) == Bool.and(True{}, Bool.and(True{}, False{})) : Bool}
915	      %Equal.sym(Bool, z2, False{}, imp2({==})({==})) :
916	        {Bool.and(True{}, Bool.or(Bool.and(False{}, Bool.and(True{}, Bool.not(Bool.and(True{}, Bool.and(True{}, False{}))))), Bool.and(True{}, Bool.and(True{}, _)))) == Bool.and(True{}, Bool.and(True{}, False{})) : Bool}
917	      {==}
918	    case True{} True{} False{} True{}:
919	      %Equal.sym(Bool, z1, False{}, imp1({==})({==})) :
920	        {Bool.and(True{}, Bool.or(Bool.and(True{}, Bool.and(False{}, Bool.not(Bool.and(True{}, Bool.and(False{}, _))))), Bool.and(True{}, Bool.and(False{}, z2)))) == Bool.and(True{}, Bool.and(False{}, True{})) : Bool}
921	      %Equal.sym(Bool, z2, False{}, imp2({==})({==})) :
922	        {Bool.and(True{}, Bool.or(Bool.and(True{}, Bool.and(False{}, Bool.not(Bool.and(True{}, Bool.and(False{}, False{}))))), Bool.and(True{}, Bool.and(False{}, _)))) == Bool.and(True{}, Bool.and(False{}, True{})) : Bool}
923	      {==}
924	    case True{} True{} False{} False{}:
925	      %Equal.sym(Bool, z1, False{}, imp1({==})({==})) :
926	        {Bool.and(True{}, Bool.or(Bool.and(False{}, Bool.and(False{}, Bool.not(Bool.and(True{}, Bool.and(False{}, _))))), Bool.and(True{}, Bool.and(False{}, z2)))) == Bool.and(True{}, Bool.and(False{}, False{})) : Bool}
927	      %Equal.sym(Bool, z2, False{}, imp2({==})({==})) :
928	        {Bool.and(True{}, Bool.or(Bool.and(False{}, Bool.and(False{}, Bool.not(Bool.and(True{}, Bool.and(False{}, False{}))))), Bool.and(True{}, Bool.and(False{}, _)))) == Bool.and(True{}, Bool.and(False{}, False{})) : Bool}
929	      {==}
930	
931	# Byte i of a word whose byte j (j != i) was set: bit k < 8 is beyond byte j.
932	law other_idx:
933	  for +i: Nat
934	  for +j: Nat
935	  for +k: Nat
936	  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
937	  for +hg: {Nat.is_le(Nat.mul(8n, j), Nat.add(Nat.mul(8n, i), k)) == True{} : Bool}
938	  for +hne: {Nat.is_eq(i, j) == False{} : Bool}
939	  {Nat.is_le(8n, Nat.sub(Nat.add(Nat.mul(8n, i), k), Nat.mul(8n, j))) == True{} : Bool}
940	
941	def other_idx(i, j, k, hk, hg, hne):
942	  +p = Nat.add(Nat.mul(8n, i), k)
943	  +hb = N.lt_mul_cancel(8n, j, 1n+i, N.le_lt_trans(Nat.mul(8n, j), p, Nat.mul(8n, 1n+i), hg, lt_mul8(i, k, hk)))
944	  +hc = {%N.lt_succ_iff(j, i) : {_ == True{} : Bool}; hb : {Nat.is_le(j, i) == True{} : Bool}}
945	  +hd = N.le_ne(j, i, hc, %N.eq_comm(i, j) : {_ == False{} : Bool}; hne)
946	  N.le_sub_r(Nat.mul(8n, j), 8n, p,
947	    %Equal.trans(Nat, Nat.mul(8n, 1n+j), Nat.add(8n, Nat.mul(8n, j)), Nat.add(Nat.mul(8n, j), 8n), N.mul_succ_r(8n, j), N.add_comm(8n, Nat.mul(8n, j))) :
948	      {Nat.is_le(_, p) == True{} : Bool}
949	    N.le_trans(Nat.mul(8n, 1n+j), Nat.mul(8n, i), p, N.le_mul_l(8n, 1n+j, i, hd), N.le_add_r(Nat.mul(8n, i), k)))
950	
951	def byte_put_other.k(+w: U32, +i: Nat, +j: Nat, +b: U32, +hb: {U32.is_lt(b, 256) == True{} : Bool}, +hij: {Nat.is_eq(i, j) == False{} : Bool}, +k: Nat) ->
952	  {D.bit(D.byte(D.put_byte(w, j, b), i), k) == D.bit(D.byte(w, i), k) : Bool}:
953	  +l = Nat.is_lt(k, 8n)
954	  +s = Nat.mul(8n, j)
955	  +p = Nat.add(Nat.mul(8n, i), k)
956	  +m = U32.shln(255, s)
957	  +ii = Nat.is_lt(p, 32n)
958	  +g = Nat.is_le(s, p)
959	  %Equal.sym(Bool, D.bit(D.byte(D.put_byte(w, j, b), i), k), Bool.and(l, D.bit(D.put_byte(w, j, b), p)), bit_byte(D.put_byte(w, j, b), i, k)) :
960	    {_ == D.bit(D.byte(w, i), k) : Bool}
961	  %Equal.sym(Bool, D.bit(U32.or(U32.and(w, U32.not(m)), U32.shln(b, s)), p), Bool.or(D.bit(U32.and(w, U32.not(m)), p), D.bit(U32.shln(b, s), p)),
962	      U.bit_or(U32.and(w, U32.not(m)), U32.shln(b, s), p)) :
963	    {Bool.and(l, _) == D.bit(D.byte(w, i), k) : Bool}
964	  %Equal.sym(Bool, D.bit(U32.and(w, U32.not(m)), p), Bool.and(D.bit(w, p), D.bit(U32.not(m), p)), U.bit_and(w, U32.not(m), p)) :
965	    {Bool.and(l, Bool.or(_, D.bit(U32.shln(b, s), p))) == D.bit(D.byte(w, i), k) : Bool}
966	  %Equal.sym(Bool, D.bit(U32.not(m), p), Bool.and(ii, Bool.not(D.bit(m, p))), U.bit_not(m, p)) :
967	    {Bool.and(l, Bool.or(Bool.and(D.bit(w, p), _), D.bit(U32.shln(b, s), p))) == D.bit(D.byte(w, i), k) : Bool}
968	  %Equal.sym(Bool, D.bit(m, p), Bool.and(g, Bool.and(ii, D.bit(255, Nat.sub(p, s)))), bit_shln(255, s, p)) :
969	    {Bool.and(l, Bool.or(Bool.and(D.bit(w, p), Bool.and(ii, Bool.not(_))), D.bit(U32.shln(b, s), p))) == D.bit(D.byte(w, i), k) : Bool}
970	  %Equal.sym(Bool, D.bit(U32.shln(b, s), p), Bool.and(g, Bool.and(ii, D.bit(b, Nat.sub(p, s)))), bit_shln(b, s, p)) :
971	    {Bool.and(l, Bool.or(Bool.and(D.bit(w, p), Bool.and(ii, Bool.not(Bool.and(g, Bool.and(ii, D.bit(255, Nat.sub(p, s))))))), _)) == D.bit(D.byte(w, i), k) : Bool}
972	  %Equal.sym(Bool, D.bit(255, Nat.sub(p, s)), Nat.is_lt(Nat.sub(p, s), 8n), bit_255(Nat.sub(p, s))) :
973	    {Bool.and(l, Bool.or(Bool.and(D.bit(w, p), Bool.and(ii, Bool.not(Bool.and(g, Bool.and(ii, _))))), Bool.and(g, Bool.and(ii, D.bit(b, Nat.sub(p, s)))))) == D.bit(D.byte(w, i), k) : Bool}
974	  %Equal.sym(Bool, D.bit(D.byte(w, i), k), Bool.and(l, D.bit(w, p)), bit_byte(w, i, k)) :
975	    {Bool.and(l, Bool.or(Bool.and(D.bit(w, p), Bool.and(ii, Bool.not(Bool.and(g, Bool.and(ii, Nat.is_lt(Nat.sub(p, s), 8n)))))), Bool.and(g, Bool.and(ii, D.bit(b, Nat.sub(p, s)))))) == _ : Bool}
976	  %Equal.sym(Bool, D.bit(w, p), Bool.and(ii, D.bit(w, p)), bit_lt32(w, p)) :
977	    {Bool.and(l, Bool.or(Bool.and(D.bit(w, p), Bool.and(ii, Bool.not(Bool.and(g, Bool.and(ii, Nat.is_lt(Nat.sub(p, s), 8n)))))), Bool.and(g, Bool.and(ii, D.bit(b, Nat.sub(p, s)))))) == Bool.and(l, _) : Bool}
978	  other_bits(l, g, ii, D.bit(w, p), Nat.is_lt(Nat.sub(p, s), 8n), D.bit(b, Nat.sub(p, s)),
979	    hl => hg => N.le_not_lt(8n, Nat.sub(p, s), other_idx(i, j, k, hl, hg, hij)),
980	    hl => hg => bit_lt_pow(b, 8n, Nat.sub(p, s), %U.is_lt_to_nat(b, 256) : {_ == True{} : Bool}; hb, other_idx(i, j, k, hl, hg, hij)))
981	
982	law byte_put_other:
983	  for +w: U32
984	  for +i: Nat
985	  for +j: Nat
986	  for +b: U32
987	  for +hb: {U32.is_lt(b, 256) == True{} : Bool}
988	  for +hij: {Nat.is_eq(i, j) == False{} : Bool}
989	  {D.byte(D.put_byte(w, j, b), i) == D.byte(w, i) : U32}
990	
991	def byte_put_other(w, i, j, b, hb, hij):
992	  U.bit_ext(D.byte(D.put_byte(w, j, b), i), D.byte(w, i), k => byte_put_other.k(w, i, j, b, hb, hij, k))
993	
994	# Packing
995	# =======
996	
997	def Cmp.disc_gt(c: Cmp) -> Type:
998	  match c:
999	    case GT{}:
1000	      Empty
1001	    case o:
1002	      Unit
1003	
1004	def lt_ne_gt(e: {LT{} == GT{} : Cmp}) -> Empty:
1005	  %e : Cmp.disc_gt(_)
1006	  Unit{}
1007	
1008	law gt_flip:
1009	  for +a: Nat
1010	  for +b: Nat
1011	  for +h: {Nat.cmp(a, b) == GT{} : Cmp}
1012	  {Nat.is_lt(b, a) == True{} : Bool}
1013	
1014	def gt_flip(a, b, h):
1015	  match a b:
1016	    case 0n 0n:
1017	      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, W.gt_ne_eq(Equal.sym(Cmp, EQ{}, GT{}, h)))
1018	    case 0n 1n+q:
1019	      Empty.absurd({Nat.is_lt(1n+q, 0n) == True{} : Bool}, lt_ne_gt(h))
1020	    case 1n+p 0n:
1021	      {==}
1022	    case 1n+p 1n+q:
1023	      gt_flip(p, q, h)
1024	
1025	# Bit k of byte J of b << 8X, for b < 256 and k < 8: bit k of b when J = X.
1026	def bsel.go(+b: U32, +x: Nat, +j: Nat, +k: Nat, +hb: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, 8n)) == True{} : Bool},
1027	  +hk: {Nat.is_lt(k, 8n) == True{} : Bool}, c: Cmp, +ec: {Nat.cmp(j, x) == c : Cmp}) ->
1028	  {Bool.and(Nat.is_le(Nat.mul(8n, x), Nat.add(Nat.mul(8n, j), k)), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n),
1029	     D.bit(b, Nat.sub(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, x)))))
1030	   == Bool.and(Nat.is_eq(j, x), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b, k))) : Bool}:
1031	  match c:
1032	    case LT{}:
1033	      +p = Nat.add(Nat.mul(8n, j), k)
1034	      +ii = Nat.is_lt(p, 32n)
1035	      +hlt = {%Equal.sym(Cmp, Nat.cmp(j, x), LT{}, ec) : {Cmp.is_lt(_) == True{} : Bool}; {==} : {Nat.is_lt(j, x) == True{} : Bool}}
1036	      %Equal.sym(Bool, Nat.is_le(Nat.mul(8n, x), p), False{}, lt_not_le(p, Nat.mul(8n, x), N.lt_le_trans(p, Nat.mul(8n, 1n+j), Nat.mul(8n, x), lt_mul8(j, k, hk),
1037	          N.le_mul_l(8n, 1n+j, x, %Equal.sym(Bool, Nat.is_le(1n+j, x), Nat.is_lt(j, x), N.le_succ_lt(j, x)) : {_ == True{} : Bool}; hlt)))) :
1038	        {Bool.and(_, Bool.and(ii, D.bit(b, Nat.sub(p, Nat.mul(8n, x))))) == Bool.and(Nat.is_eq(j, x), Bool.and(ii, D.bit(b, k))) : Bool}
1039	      %Equal.sym(Cmp, Nat.cmp(j, x), LT{}, ec) : {False{} == Bool.and(Cmp.is_eq(_), Bool.and(ii, D.bit(b, k))) : Bool}
1040	      {==}
1041	    case EQ{}:
1042	      +hjx = N.eq_sound(j, x, %Equal.sym(Cmp, Nat.cmp(j, x), EQ{}, ec) : {Cmp.is_eq(_) == True{} : Bool}; {==})
1043	      +p = Nat.add(Nat.mul(8n, j), k)
1044	      +ii = Nat.is_lt(p, 32n)
1045	      %hjx : {Bool.and(Nat.is_le(Nat.mul(8n, _), p), Bool.and(ii, D.bit(b, Nat.sub(p, Nat.mul(8n, _))))) == Bool.and(Nat.is_eq(j, _), Bool.and(ii, D.bit(b, k))) : Bool}
1046	      %Equal.sym(Bool, Nat.is_le(Nat.mul(8n, j), p), True{}, N.le_add_r(Nat.mul(8n, j), k)) :
1047	        {Bool.and(_, Bool.and(ii, D.bit(b, Nat.sub(p, Nat.mul(8n, j))))) == Bool.and(Nat.is_eq(j, j), Bool.and(ii, D.bit(b, k))) : Bool}
1048	      %Equal.sym(Nat, Nat.sub(p, Nat.mul(8n, j)), k, N.sub_add_l(Nat.mul(8n, j), k)) :
1049	        {Bool.and(True{}, Bool.and(ii, D.bit(b, _))) == Bool.and(Nat.is_eq(j, j), Bool.and(ii, D.bit(b, k))) : Bool}
1050	      %Equal.sym(Bool, Nat.is_eq(j, j), True{}, N.eq_refl(j)) :
1051	        {Bool.and(True{}, Bool.and(ii, D.bit(b, k))) == Bool.and(_, Bool.and(ii, D.bit(b, k))) : Bool}
1052	      {==}
1053	    case GT{}:
1054	      +p = Nat.add(Nat.mul(8n, j), k)
1055	      +ii = Nat.is_lt(p, 32n)
1056	      +hxj = gt_flip(j, x, ec)
1057	      +hle = N.lt_to_le(x, j, hxj)
1058	      +q = Nat.add(Nat.mul(8n, Nat.sub(j, x)), k)
1059	      %Equal.sym(Bool, Nat.is_le(Nat.mul(8n, x), p), True{}, N.le_trans(Nat.mul(8n, x), Nat.mul(8n, j), p, N.le_mul_l(8n, x, j, hle), N.le_add_r(Nat.mul(8n, j), k))) :
1060	        {Bool.and(_, Bool.and(ii, D.bit(b, Nat.sub(p, Nat.mul(8n, x))))) == Bool.and(Nat.is_eq(j, x), Bool.and(ii, D.bit(b, k))) : Bool}
1061	      %Equal.sym(Nat, Nat.sub(p, Nat.mul(8n, x)), q, idx_sub(x, j, k, hle)) :
1062	        {Bool.and(True{}, Bool.and(ii, D.bit(b, _))) == Bool.and(Nat.is_eq(j, x), Bool.and(ii, D.bit(b, k))) : Bool}
1063	      %Equal.sym(Bool, D.bit(b, q), False{}, bit_lt_pow(b, 8n, q, hb,
1064	          N.le_trans(8n, Nat.mul(8n, Nat.sub(j, x)), q,
1065	            N.le_mul_l(8n, 1n, Nat.sub(j, x), %Equal.sym(Bool, Nat.is_le(1n, Nat.sub(j, x)), Nat.is_lt(0n, Nat.sub(j, x)), N.le_succ_lt(0n, Nat.sub(j, x))) : {_ == True{} : Bool};
1066	              lt_sub(0n, x, j, hxj)),
1067	            N.le_add_r(Nat.mul(8n, Nat.sub(j, x)), k)))) :
1068	        {Bool.and(True{}, Bool.and(ii, _)) == Bool.and(Nat.is_eq(j, x), Bool.and(ii, D.bit(b, k))) : Bool}
1069	      %Equal.sym(Cmp, Nat.cmp(j, x), GT{}, ec) : {Bool.and(ii, False{}) == Bool.and(Cmp.is_eq(_), Bool.and(ii, D.bit(b, k))) : Bool}
1070	      N.and_false_r(ii)
1071	
1072	law bsel:
1073	  for +b: U32
1074	  for +x: Nat
1075	  for +j: Nat
1076	  for +k: Nat
1077	  for +hb: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, 8n)) == True{} : Bool}
1078	  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
1079	  {D.bit(U32.shln(b, Nat.mul(8n, x)), Nat.add(Nat.mul(8n, j), k))
1080	    == Bool.and(Nat.is_eq(j, x), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b, k))) : Bool}
1081	
1082	def bsel(b, x, j, k, hb, hk):
1083	  +p = Nat.add(Nat.mul(8n, j), k)
1084	  %Equal.sym(Bool, D.bit(U32.shln(b, Nat.mul(8n, x)), p), Bool.and(Nat.is_le(Nat.mul(8n, x), p), Bool.and(Nat.is_lt(p, 32n), D.bit(b, Nat.sub(p, Nat.mul(8n, x))))),
1085	      bit_shln(b, Nat.mul(8n, x), p)) :
1086	    {_ == Bool.and(Nat.is_eq(j, x), Bool.and(Nat.is_lt(p, 32n), D.bit(b, k))) : Bool}
1087	  bsel.go(b, x, j, k, hb, hk, Nat.cmp(j, x), {==})
1088	
1089	# A U32 test b < 256 as numbers.
1090	law lt256:
1091	  for +b: U32
1092	  for +h: {U32.is_lt(b, 256) == True{} : Bool}
1093	  {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, 8n)) == True{} : Bool}
1094	
1095	def lt256(b, h):
1096	  %U.is_lt_to_nat(b, 256) : {_ == True{} : Bool}
1097	  h
1098	
1099	# Bit k (k < 8) of byte j of pack4(b0, b1, b2, b3).
1100	law pack_bits:
1101	  for +b0: U32
1102	  for +b1: U32
1103	  for +b2: U32
1104	  for +b3: U32
1105	  for +j: Nat
1106	  for +k: Nat
1107	  for +h0: {Nat.is_lt(U32.to_nat(b0), Nat.pow(2n, 8n)) == True{} : Bool}
1108	  for +h1: {Nat.is_lt(U32.to_nat(b1), Nat.pow(2n, 8n)) == True{} : Bool}
1109	  for +h2: {Nat.is_lt(U32.to_nat(b2), Nat.pow(2n, 8n)) == True{} : Bool}
1110	  for +h3: {Nat.is_lt(U32.to_nat(b3), Nat.pow(2n, 8n)) == True{} : Bool}
1111	  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
1112	  {D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, j), k)) ==
1113	    Bool.or(Bool.and(Nat.is_eq(j, 0n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b0, k))),
1114	    Bool.or(Bool.and(Nat.is_eq(j, 1n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b1, k))),
1115	    Bool.or(Bool.and(Nat.is_eq(j, 2n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b2, k))),
1116	            Bool.and(Nat.is_eq(j, 3n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b3, k)))))) : Bool}
1117	
1118	def pack_bits(b0, b1, b2, b3, j, k, h0, h1, h2, h3, hk):
1119	  +p = Nat.add(Nat.mul(8n, j), k)
1120	  +ii = Nat.is_lt(p, 32n)
1121	  +a0 = Bool.and(Nat.is_eq(j, 0n), Bool.and(ii, D.bit(b0, k)))
1122	  +a1 = Bool.and(Nat.is_eq(j, 1n), Bool.and(ii, D.bit(b1, k)))
1123	  +a2 = Bool.and(Nat.is_eq(j, 2n), Bool.and(ii, D.bit(b2, k)))
1124	  +a3 = Bool.and(Nat.is_eq(j, 3n), Bool.and(ii, D.bit(b3, k)))
1125	  +r2 = U32.or(U32.shln(b2, 16n), U32.shln(b3, 24n))
1126	  +r1 = U32.or(U32.shln(b1, 8n), r2)
1127	  %Equal.sym(Bool, D.bit(U32.or(b0, r1), p), Bool.or(D.bit(b0, p), D.bit(r1, p)), U.bit_or(b0, r1, p)) :
1128	    {_ == Bool.or(a0, Bool.or(a1, Bool.or(a2, a3))) : Bool}
1129	  %Equal.sym(Bool, D.bit(r1, p), Bool.or(D.bit(U32.shln(b1, 8n), p), D.bit(r2, p)), U.bit_or(U32.shln(b1, 8n), r2, p)) :
1130	    {Bool.or(D.bit(b0, p), _) == Bool.or(a0, Bool.or(a1, Bool.or(a2, a3))) : Bool}
1131	  %Equal.sym(Bool, D.bit(r2, p), Bool.or(D.bit(U32.shln(b2, 16n), p), D.bit(U32.shln(b3, 24n), p)), U.bit_or(U32.shln(b2, 16n), U32.shln(b3, 24n), p)) :
1132	    {Bool.or(D.bit(b0, p), Bool.or(D.bit(U32.shln(b1, 8n), p), _)) == Bool.or(a0, Bool.or(a1, Bool.or(a2, a3))) : Bool}
1133	  %Equal.sym(Bool, D.bit(U32.shln(b0, Nat.mul(8n, 0n)), p), a0, bsel(b0, 0n, j, k, h0, hk)) :
1134	    {Bool.or(_, Bool.or(D.bit(U32.shln(b1, 8n), p), Bool.or(D.bit(U32.shln(b2, 16n), p), D.bit(U32.shln(b3, 24n), p)))) == Bool.or(a0, Bool.or(a1, Bool.or(a2, a3))) : Bool}
1135	  %Equal.sym(Bool, D.bit(U32.shln(b1, Nat.mul(8n, 1n)), p), a1, bsel(b1, 1n, j, k, h1, hk)) :
1136	    {Bool.or(a0, Bool.or(_, Bool.or(D.bit(U32.shln(b2, 16n), p), D.bit(U32.shln(b3, 24n), p)))) == Bool.or(a0, Bool.or(a1, Bool.or(a2, a3))) : Bool}
1137	  %Equal.sym(Bool, D.bit(U32.shln(b2, Nat.mul(8n, 2n)), p), a2, bsel(b2, 2n, j, k, h2, hk)) :
1138	    {Bool.or(a0, Bool.or(a1, Bool.or(_, D.bit(U32.shln(b3, 24n), p)))) == Bool.or(a0, Bool.or(a1, Bool.or(a2, a3))) : Bool}
1139	  %Equal.sym(Bool, D.bit(U32.shln(b3, Nat.mul(8n, 3n)), p), a3, bsel(b3, 3n, j, k, h3, hk)) :
1140	    {Bool.or(a0, Bool.or(a1, Bool.or(a2, _))) == Bool.or(a0, Bool.or(a1, Bool.or(a2, a3))) : Bool}
1141	  {==}
1142	
1143	law nth4_lt:
1144	  for +j: Nat
1145	  for +b0: U32
1146	  for +b1: U32
1147	  for +b2: U32
1148	  for +b3: U32
1149	  for +h0: {Nat.is_lt(U32.to_nat(b0), Nat.pow(2n, 8n)) == True{} : Bool}
1150	  for +h1: {Nat.is_lt(U32.to_nat(b1), Nat.pow(2n, 8n)) == True{} : Bool}
1151	  for +h2: {Nat.is_lt(U32.to_nat(b2), Nat.pow(2n, 8n)) == True{} : Bool}
1152	  for +h3: {Nat.is_lt(U32.to_nat(b3), Nat.pow(2n, 8n)) == True{} : Bool}
1153	  {Nat.is_lt(U32.to_nat(D.nth4(j, b0, b1, b2, b3)), Nat.pow(2n, 8n)) == True{} : Bool}
1154	
1155	def nth4_lt(j, b0, b1, b2, b3, h0, h1, h2, h3):
1156	  match j:
1157	    case 0n:
1158	      h0
1159	    case 1n+p:
1160	      match p:
1161	        case 0n:
1162	          h1
1163	        case 1n+q:
1164	          match q:
1165	            case 0n:
1166	              h2
1167	            case 1n+t:
1168	              h3
1169	
1170	# Bit k (k < 8) of byte j (j < 4) of a packed word is bit k of the j-th value.
1171	law pack_byte:
1172	  for +b0: U32
1173	  for +b1: U32
1174	  for +b2: U32
1175	  for +b3: U32
1176	  for +j: Nat
1177	  for +k: Nat
1178	  for +h0: {Nat.is_lt(U32.to_nat(b0), Nat.pow(2n, 8n)) == True{} : Bool}
1179	  for +h1: {Nat.is_lt(U32.to_nat(b1), Nat.pow(2n, 8n)) == True{} : Bool}
1180	  for +h2: {Nat.is_lt(U32.to_nat(b2), Nat.pow(2n, 8n)) == True{} : Bool}
1181	  for +h3: {Nat.is_lt(U32.to_nat(b3), Nat.pow(2n, 8n)) == True{} : Bool}
1182	  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
1183	  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
1184	  {D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, j), k)) == D.bit(D.nth4(j, b0, b1, b2, b3), k) : Bool}
1185	
1186	def pack_byte(b0, b1, b2, b3, j, k, h0, h1, h2, h3, hj, hk):
1187	  match j:
1188	    case 0n:
1189	      %Equal.sym(Bool, D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, 0n), k)), Bool.or(Bool.and(Nat.is_eq(0n, 0n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 0n), k), 32n), D.bit(b0, k))),
1190	          Bool.or(Bool.and(Nat.is_eq(0n, 1n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 0n), k), 32n), D.bit(b1, k))),
1191	          Bool.or(Bool.and(Nat.is_eq(0n, 2n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 0n), k), 32n), D.bit(b2, k))),
1192	                  Bool.and(Nat.is_eq(0n, 3n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 0n), k), 32n), D.bit(b3, k)))))),
1193	          pack_bits(b0, b1, b2, b3, 0n, k, h0, h1, h2, h3, hk)) :
1194	        {_ == D.bit(b0, k) : Bool}
1195	      %Equal.sym(Bool, Bool.or(Bool.and(Nat.is_lt(k, 32n), D.bit(b0, k)), False{}), Bool.and(Nat.is_lt(k, 32n), D.bit(b0, k)), N.or_false_r(Bool.and(Nat.is_lt(k, 32n), D.bit(b0, k)))) :
1196	        {_ == D.bit(b0, k) : Bool}
1197	      %Equal.sym(Bool, Nat.is_lt(k, 32n), True{}, idx32(0n, k, {==}, hk)) : {Bool.and(_, D.bit(b0, k)) == D.bit(b0, k) : Bool}
1198	      {==}
1199	    case 1n+j1:
1200	      match j1:
1201	        case 0n:
1202	          %Equal.sym(Bool, D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, 1n), k)), Bool.or(Bool.and(Nat.is_eq(1n, 0n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 1n), k), 32n), D.bit(b0, k))),
1203	              Bool.or(Bool.and(Nat.is_eq(1n, 1n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 1n), k), 32n), D.bit(b1, k))),
1204	              Bool.or(Bool.and(Nat.is_eq(1n, 2n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 1n), k), 32n), D.bit(b2, k))),
1205	                      Bool.and(Nat.is_eq(1n, 3n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 1n), k), 32n), D.bit(b3, k)))))),
1206	              pack_bits(b0, b1, b2, b3, 1n, k, h0, h1, h2, h3, hk)) :
1207	            {_ == D.bit(b1, k) : Bool}
1208	          %Equal.sym(Bool, Bool.or(Bool.and(Nat.is_lt(8n+k, 32n), D.bit(b1, k)), False{}), Bool.and(Nat.is_lt(8n+k, 32n), D.bit(b1, k)), N.or_false_r(Bool.and(Nat.is_lt(8n+k, 32n), D.bit(b1, k)))) :
1209	            {_ == D.bit(b1, k) : Bool}
1210	          %Equal.sym(Bool, Nat.is_lt(8n+k, 32n), True{}, idx32(1n, k, {==}, hk)) : {Bool.and(_, D.bit(b1, k)) == D.bit(b1, k) : Bool}
1211	          {==}
1212	        case 1n+j2:
1213	          match j2:
1214	            case 0n:
1215	              %Equal.sym(Bool, D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, 2n), k)), Bool.or(Bool.and(Nat.is_eq(2n, 0n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 2n), k), 32n), D.bit(b0, k))),
1216	                  Bool.or(Bool.and(Nat.is_eq(2n, 1n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 2n), k), 32n), D.bit(b1, k))),
1217	                  Bool.or(Bool.and(Nat.is_eq(2n, 2n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 2n), k), 32n), D.bit(b2, k))),
1218	                          Bool.and(Nat.is_eq(2n, 3n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 2n), k), 32n), D.bit(b3, k)))))),
1219	                  pack_bits(b0, b1, b2, b3, 2n, k, h0, h1, h2, h3, hk)) :
1220	                {_ == D.bit(b2, k) : Bool}
1221	              %Equal.sym(Bool, Bool.or(Bool.and(Nat.is_lt(16n+k, 32n), D.bit(b2, k)), False{}), Bool.and(Nat.is_lt(16n+k, 32n), D.bit(b2, k)), N.or_false_r(Bool.and(Nat.is_lt(16n+k, 32n), D.bit(b2, k)))) :
1222	                {_ == D.bit(b2, k) : Bool}
1223	              %Equal.sym(Bool, Nat.is_lt(16n+k, 32n), True{}, idx32(2n, k, {==}, hk)) : {Bool.and(_, D.bit(b2, k)) == D.bit(b2, k) : Bool}
1224	              {==}
1225	            case 1n+j3:
1226	              match j3:
1227	                case 0n:
1228	                  %Equal.sym(Bool, D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, 3n), k)), Bool.or(Bool.and(Nat.is_eq(3n, 0n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 3n), k), 32n), D.bit(b0, k))),
1229	                      Bool.or(Bool.and(Nat.is_eq(3n, 1n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 3n), k), 32n), D.bit(b1, k))),
1230	                      Bool.or(Bool.and(Nat.is_eq(3n, 2n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 3n), k), 32n), D.bit(b2, k))),
1231	                              Bool.and(Nat.is_eq(3n, 3n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, 3n), k), 32n), D.bit(b3, k)))))),
1232	                      pack_bits(b0, b1, b2, b3, 3n, k, h0, h1, h2, h3, hk)) :
1233	                    {_ == D.bit(b3, k) : Bool}
1234	                  %Equal.sym(Bool, Nat.is_lt(24n+k, 32n), True{}, idx32(3n, k, {==}, hk)) : {Bool.and(_, D.bit(b3, k)) == D.bit(b3, k) : Bool}
1235	                  {==}
1236	                case 1n+j4:
1237	                  Empty.absurd({D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, 4n+j4), k)) == D.bit(D.nth4(4n+j4, b0, b1, b2, b3), k) : Bool}, N.false_ne_true(
1238	                    Equal.trans(Bool, False{}, Nat.is_lt(j4, 0n), True{}, Equal.sym(Bool, Nat.is_lt(j4, 0n), False{}, N.lt_zero(j4)), hj)))
1239	
1240	def byte_pack4.l(+b0: U32, +b1: U32, +b2: U32, +b3: U32, +j: Nat, +k: Nat,
1241	  +h0: {Nat.is_lt(U32.to_nat(b0), Nat.pow(2n, 8n)) == True{} : Bool},
1242	  +h1: {Nat.is_lt(U32.to_nat(b1), Nat.pow(2n, 8n)) == True{} : Bool},
1243	  +h2: {Nat.is_lt(U32.to_nat(b2), Nat.pow(2n, 8n)) == True{} : Bool},
1244	  +h3: {Nat.is_lt(U32.to_nat(b3), Nat.pow(2n, 8n)) == True{} : Bool},
1245	  +hj: {Nat.is_lt(j, 4n) == True{} : Bool}, z: Bool, +ez: {Nat.is_lt(k, 8n) == z : Bool}) ->
1246	  {Bool.and(z, D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, j), k))) == D.bit(D.nth4(j, b0, b1, b2, b3), k) : Bool}:
1247	  match z:
1248	    case True{}:
1249	      pack_byte(b0, b1, b2, b3, j, k, h0, h1, h2, h3, hj, ez)
1250	    case False{}:
1251	      Equal.sym(Bool, D.bit(D.nth4(j, b0, b1, b2, b3), k), False{},
1252	        bit_lt_pow(D.nth4(j, b0, b1, b2, b3), 8n, k, nth4_lt(j, b0, b1, b2, b3, h0, h1, h2, h3), N.not_lt_le(k, 8n, ez)))
1253	
1254	def byte_pack4.k(+b0: U32, +b1: U32, +b2: U32, +b3: U32, +j: Nat,
1255	  +h0: {Nat.is_lt(U32.to_nat(b0), Nat.pow(2n, 8n)) == True{} : Bool},
1256	  +h1: {Nat.is_lt(U32.to_nat(b1), Nat.pow(2n, 8n)) == True{} : Bool},
1257	  +h2: {Nat.is_lt(U32.to_nat(b2), Nat.pow(2n, 8n)) == True{} : Bool},
1258	  +h3: {Nat.is_lt(U32.to_nat(b3), Nat.pow(2n, 8n)) == True{} : Bool},
1259	  +hj: {Nat.is_lt(j, 4n) == True{} : Bool}, +k: Nat) ->
1260	  {D.bit(D.byte(D.pack4(b0, b1, b2, b3), j), k) == D.bit(D.nth4(j, b0, b1, b2, b3), k) : Bool}:
1261	  %Equal.sym(Bool, D.bit(D.byte(D.pack4(b0, b1, b2, b3), j), k), Bool.and(Nat.is_lt(k, 8n), D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, j), k))),
1262	      bit_byte(D.pack4(b0, b1, b2, b3), j, k)) :
1263	    {_ == D.bit(D.nth4(j, b0, b1, b2, b3), k) : Bool}
1264	  byte_pack4.l(b0, b1, b2, b3, j, k, h0, h1, h2, h3, hj, Nat.is_lt(k, 8n), {==})
1265	
1266	law byte_pack4:
1267	  for +b0: U32
1268	  for +b1: U32
1269	  for +b2: U32
1270	  for +b3: U32
1271	  for +j: Nat
1272	  for +h0: {U32.is_lt(b0, 256) == True{} : Bool}
1273	  for +h1: {U32.is_lt(b1, 256) == True{} : Bool}
1274	  for +h2: {U32.is_lt(b2, 256) == True{} : Bool}
1275	  for +h3: {U32.is_lt(b3, 256) == True{} : Bool}
1276	  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
1277	  {D.byte(D.pack4(b0, b1, b2, b3), j) == D.nth4(j, b0, b1, b2, b3) : U32}
1278	
1279	def byte_pack4(b0, b1, b2, b3, j, h0, h1, h2, h3, hj):
1280	  U.bit_ext(D.byte(D.pack4(b0, b1, b2, b3), j), D.nth4(j, b0, b1, b2, b3),
1281	    k => byte_pack4.k(b0, b1, b2, b3, j, lt256(b0, h0), lt256(b1, h1), lt256(b2, h2), lt256(b3, h3), hj, k))
1282	
1283	law nth4_byte:
1284	  for +w: U32
1285	  for +j: Nat
1286	  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
1287	  {D.nth4(j, D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)) == D.byte(w, j) : U32}
1288	
1289	def nth4_byte(w, j, hj):
1290	  match j:
1291	    case 0n:
1292	      {==}
1293	    case 1n+p:
1294	      match p:
1295	        case 0n:
1296	          {==}
1297	        case 1n+q:
1298	          match q:
1299	            case 0n:
1300	              {==}
1301	            case 1n+t:
1302	              match t:
1303	                case 0n:
1304	                  {==}
1305	                case 1n+u:
1306	                  Empty.absurd({D.nth4(4n+u, D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)) == D.byte(w, 4n+u) : U32}, N.false_ne_true(
1307	                    Equal.trans(Bool, False{}, Nat.is_lt(u, 0n), True{}, Equal.sym(Bool, Nat.is_lt(u, 0n), False{}, N.lt_zero(u)), hj)))
1308	
1309	def pack4_bytes.go(+w: U32, +j: Nat, +k: Nat, +hk: {Nat.is_lt(k, 8n) == True{} : Bool}, z: Bool, +ez: {Nat.is_lt(j, 4n) == z : Bool}) ->
1310	  {D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), Nat.add(Nat.mul(8n, j), k)) == D.bit(w, Nat.add(Nat.mul(8n, j), k)) : Bool}:
1311	  match z:
1312	    case True{}:
1313	      +p = Nat.add(Nat.mul(8n, j), k)
1314	      %Equal.sym(Bool, D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), p),
1315	          D.bit(D.nth4(j, D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), k),
1316	          pack_byte(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n), j, k,
1317	            lt256(D.byte(w, 0n), byte_lt(w, 0n)), lt256(D.byte(w, 1n), byte_lt(w, 1n)), lt256(D.byte(w, 2n), byte_lt(w, 2n)), lt256(D.byte(w, 3n), byte_lt(w, 3n)), ez, hk)) :
1318	        {_ == D.bit(w, p) : Bool}
1319	      %Equal.sym(U32, D.nth4(j, D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), D.byte(w, j), nth4_byte(w, j, ez)) : {D.bit(_, k) == D.bit(w, p) : Bool}
1320	      %Equal.sym(Bool, D.bit(D.byte(w, j), k), Bool.and(Nat.is_lt(k, 8n), D.bit(w, p)), bit_byte(w, j, k)) : {_ == D.bit(w, p) : Bool}
1321	      %Equal.sym(Bool, Nat.is_lt(k, 8n), True{}, hk) : {Bool.and(_, D.bit(w, p)) == D.bit(w, p) : Bool}
1322	      {==}
1323	    case False{}:
1324	      +p = Nat.add(Nat.mul(8n, j), k)
1325	      +h32 = N.le_trans(32n, Nat.mul(8n, j), p, N.le_mul_l(8n, 4n, j, N.not_lt_le(j, 4n, ez)), N.le_add_r(Nat.mul(8n, j), k))
1326	      Equal.trans(Bool, D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), p), False{}, D.bit(w, p),
1327	        bit_ge32(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), p, h32),
1328	        Equal.sym(Bool, D.bit(w, p), False{}, bit_ge32(w, p, h32)))
1329	
1330	def pack4_bytes.k(+w: U32, +k: Nat) -> {D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), k) == D.bit(w, k) : Bool}:
1331	  +j = Nat.div(k, 8n)
1332	  +r = Nat.mod(k, 8n)
1333	  %Equal.trans(Nat, Nat.add(Nat.mul(8n, j), r), Nat.add(Nat.mul(j, 8n), r), k,
1334	      Equal.cong(Nat, Nat, t => Nat.add(t, r), Nat.mul(8n, j), Nat.mul(j, 8n), N.mul_comm(8n, j)), N.div_mod(k, 8n)) :
1335	    {D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), _) == D.bit(w, _) : Bool}
1336	  pack4_bytes.go(w, j, r, N.mod_lt(k, 8n, {==}), Nat.is_lt(j, 4n), {==})
1337	
1338	law pack4_bytes:
1339	  for +w: U32
1340	  {D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)) == w : U32}
1341	
1342	def pack4_bytes(w):
1343	  U.bit_ext(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), w, k => pack4_bytes.k(w, k))
1344	
1345	law byte_ext:
1346	  for +a: U32
1347	  for +b: U32
1348	  for +h0: {D.byte(a, 0n) == D.byte(b, 0n) : U32}
1349	  for +h1: {D.byte(a, 1n) == D.byte(b, 1n) : U32}
1350	  for +h2: {D.byte(a, 2n) == D.byte(b, 2n) : U32}
1351	  for +h3: {D.byte(a, 3n) == D.byte(b, 3n) : U32}
1352	  {a == b : U32}
1353	
1354	def byte_ext(a, b, h0, h1, h2, h3):
1355	  Equal.trans(U32, a, D.pack4(D.byte(a, 0n), D.byte(a, 1n), D.byte(a, 2n), D.byte(a, 3n)), b,
1356	    Equal.sym(U32, D.pack4(D.byte(a, 0n), D.byte(a, 1n), D.byte(a, 2n), D.byte(a, 3n)), a, pack4_bytes(a)),
1357	    %Equal.sym(U32, D.byte(a, 0n), D.byte(b, 0n), h0) : {D.pack4(_, D.byte(a, 1n), D.byte(a, 2n), D.byte(a, 3n)) == b : U32}
1358	    %Equal.sym(U32, D.byte(a, 1n), D.byte(b, 1n), h1) : {D.pack4(D.byte(b, 0n), _, D.byte(a, 2n), D.byte(a, 3n)) == b : U32}
1359	    %Equal.sym(U32, D.byte(a, 2n), D.byte(b, 2n), h2) : {D.pack4(D.byte(b, 0n), D.byte(b, 1n), _, D.byte(a, 3n)) == b : U32}
1360	    %Equal.sym(U32, D.byte(a, 3n), D.byte(b, 3n), h3) : {D.pack4(D.byte(b, 0n), D.byte(b, 1n), D.byte(b, 2n), _) == b : U32}
1361	    pack4_bytes(b))
1362	
1363	# The number a packed word stands for
1364	# ===================================
1365	
1366	law bor_comm:
1367	  for +x: Bool
1368	  for +y: Bool
1369	  {Bool.or(x, y) == Bool.or(y, x) : Bool}
1370	
1371	def bor_comm(x, y):
1372	  match x y:
1373	    case False{} False{}:
1374	      {==}
1375	    case False{} True{}:
1376	      {==}
1377	    case True{} False{}:
1378	      {==}
1379	    case True{} True{}:
1380	      {==}
1381	
1382	law wor_comm:
1383	  for +n: Nat
1384	  for +a: Word(n)
1385	  for +b: Word(n)
1386	  {Word.or(n, a, b) == Word.or(n, b, a) : Word(n)}
1387	
1388	def wor_comm(n, a, b):
1389	  match n:
1390	    case 0n:
1391	      match a b:
1392	        case WNil{} WNil{}:
1393	          {==}
1394	    case 1n+p:
1395	      match a b:
1396	        case WCon{+x, +at} WCon{+y, +bt}:
1397	          %bor_comm(x, y) : {WCon{Bool.or(x, y), Word.or(p, at, bt)} == WCon{_, Word.or(p, bt, at)} : Word(1n+p)}
1398	          %wor_comm(p, at, bt) : {WCon{Bool.or(x, y), Word.or(p, at, bt)} == WCon{Bool.or(x, y), _} : Word(1n+p)}
1399	          {==}
1400	
1401	law or_comm:
1402	  for +a: U32
1403	  for +b: U32
1404	  {U32.or(a, b) == U32.or(b, a) : U32}
1405	
1406	def or_comm(a, b):
1407	  match a b:
1408	    case U32{+x} U32{+y}:
1409	      %wor_comm(32n, x, y) : {U32{Word.or(32n, x, y)} == U32{_} : U32}
1410	      {==}
1411	
1412	law lt_mul_r:
1413	  for +a: Nat
1414	  for +b: Nat
1415	  for +c: Nat
1416	  for +h: {Nat.is_lt(a, b) == True{} : Bool}
1417	  for +hc: {Nat.is_lt(0n, c) == True{} : Bool}
1418	  {Nat.is_lt(Nat.mul(a, c), Nat.mul(b, c)) == True{} : Bool}
1419	
1420	def lt_mul_r(a, b, c, h, hc):
1421	  match a b:
1422	    case _ 0n:
1423	      Empty.absurd({Nat.is_lt(Nat.mul(a, c), 0n) == True{} : Bool}, N.false_ne_true(
1424	        Equal.trans(Bool, False{}, Nat.is_lt(a, 0n), True{}, Equal.sym(Bool, Nat.is_lt(a, 0n), False{}, N.lt_zero(a)), h)))
1425	    case 0n 1n+q:
1426	      N.pos_add_l(c, Nat.mul(q, c), hc)
1427	    case 1n+p 1n+q:
1428	      N.lt_add_l(c, Nat.mul(p, c), Nat.mul(q, c), lt_mul_r(p, q, c, h, hc))
1429	
1430	# 2^16, 2^24 and 2^32 in terms of a = 2^8.
1431	law p16:
1432	  for +a: Nat
1433	  for +ha: {Nat.pow(2n, 8n) == a : Nat}
1434	  {Nat.pow(2n, 16n) == Nat.mul(a, a) : Nat}
1435	
1436	def p16(a, ha):
1437	  %ha : {Nat.pow(2n, 16n) == Nat.mul(_, _) : Nat}
1438	  %{{==} : {Nat.add(8n, 8n) == 16n : Nat}} : {Nat.pow(2n, _) == Nat.mul(Nat.pow(2n, 8n), Nat.pow(2n, 8n)) : Nat}
1439	  N.pow_add(2n, 8n, 8n)
1440	
1441	law p24:
1442	  for +a: Nat
1443	  for +ha: {Nat.pow(2n, 8n) == a : Nat}
1444	  {Nat.pow(2n, 24n) == Nat.mul(Nat.mul(a, a), a) : Nat}
1445	
1446	def p24(a, ha):
1447	  %p16(a, ha) : {Nat.pow(2n, 24n) == Nat.mul(_, a) : Nat}
1448	  %ha : {Nat.pow(2n, 24n) == Nat.mul(Nat.pow(2n, 16n), _) : Nat}
1449	  %{{==} : {Nat.add(16n, 8n) == 24n : Nat}} : {Nat.pow(2n, _) == Nat.mul(Nat.pow(2n, 16n), Nat.pow(2n, 8n)) : Nat}
1450	  N.pow_add(2n, 16n, 8n)
1451	
1452	law p32:
1453	  for +a: Nat
1454	  for +m: Nat
1455	  for +ha: {Nat.pow(2n, 8n) == a : Nat}
1456	  for +hm: {Nat.pow(2n, 32n) == m : Nat}
1457	  {m == Nat.mul(Nat.mul(Nat.mul(a, a), a), a) : Nat}
1458	
1459	def p32(a, m, ha, hm):
1460	  %hm : {_ == Nat.mul(Nat.mul(Nat.mul(a, a), a), a) : Nat}
1461	  %p24(a, ha) : {Nat.pow(2n, 32n) == Nat.mul(_, a) : Nat}
1462	  %ha : {Nat.pow(2n, 32n) == Nat.mul(Nat.pow(2n, 24n), _) : Nat}
1463	  %{{==} : {Nat.add(24n, 8n) == 32n : Nat}} : {Nat.pow(2n, _) == Nat.mul(Nat.pow(2n, 24n), Nat.pow(2n, 8n)) : Nat}
1464	  N.pow_add(2n, 24n, 8n)
1465	
1466	law le_mul_pos:
1467	  for +x: Nat
1468	  for +c: Nat
1469	  for +hc: {Nat.is_lt(0n, c) == True{} : Bool}
1470	  {Nat.is_le(x, Nat.mul(x, c)) == True{} : Bool}
1471	
1472	def le_mul_pos(x, c, hc):
1473	  %N.mul_one(x) : {Nat.is_le(_, Nat.mul(x, c)) == True{} : Bool}
1474	  N.le_mul_l(x, 1n, c, %Equal.sym(Bool, Nat.is_le(1n, c), Nat.is_lt(0n, c), N.le_succ_lt(0n, c)) : {_ == True{} : Bool}; hc)
1475	
1476	# The value of b << 8s, 16 or 24, with a = 2^8 and m = 2^32 abstract.
1477	law shv:
1478	  for +b: U32
1479	  for +s: Nat
1480	  for +p: Nat
1481	  for +a: Nat
1482	  for +m: Nat
1483	  for +hm: {Nat.pow(2n, 32n) == m : Nat}
1484	  for +hp: {Nat.pow(2n, s) == p : Nat}
1485	  for +hb: {Nat.is_lt(U32.to_nat(b), a) == True{} : Bool}
1486	  for +hpm: {Nat.is_le(Nat.mul(a, p), m) == True{} : Bool}
1487	  for +hp0: {Nat.is_lt(0n, p) == True{} : Bool}
1488	  {U32.to_nat(U32.shln(b, s)) == Nat.mul(U32.to_nat(b), p) : Nat}
1489	
1490	def shv(b, s, p, a, m, hm, hp, hb, hpm, hp0):
1491	  Equal.trans(Nat, U32.to_nat(U32.shln(b, s)), Nat.mod(Nat.mul(U32.to_nat(b), Nat.pow(2n, s)), m), Nat.mul(U32.to_nat(b), p),
1492	    U.to_nat_shln.m(b, s, m, hm),
1493	    %Equal.sym(Nat, Nat.pow(2n, s), p, hp) : {Nat.mod(Nat.mul(U32.to_nat(b), _), m) == Nat.mul(U32.to_nat(b), p) : Nat}
1494	    N.mod_small(Nat.mul(U32.to_nat(b), p), m, N.lt_le_trans(Nat.mul(U32.to_nat(b), p), Nat.mul(a, p), m, lt_mul_r(U32.to_nat(b), a, p, hb, hp0), hpm)))
1495	
1496	law pk.m:
1497	  for +b0: U32
1498	  for +b1: U32
1499	  for +b2: U32
1500	  for +b3: U32
1501	  for +a: Nat
1502	  for +m: Nat
1503	  for +ha: {Nat.pow(2n, 8n) == a : Nat}
1504	  for +hm: {Nat.pow(2n, 32n) == m : Nat}
1505	  for +h0: {Nat.is_lt(U32.to_nat(b0), a) == True{} : Bool}
1506	  for +h1: {Nat.is_lt(U32.to_nat(b1), a) == True{} : Bool}
1507	  for +h2: {Nat.is_lt(U32.to_nat(b2), a) == True{} : Bool}
1508	  for +h3: {Nat.is_lt(U32.to_nat(b3), a) == True{} : Bool}
1509	  {U32.to_nat(D.pack4(b0, b1, b2, b3)) == Nat.add(U32.to_nat(b0), Nat.add(Nat.mul(U32.to_nat(b1), a),
1510	    Nat.add(Nat.mul(U32.to_nat(b2), Nat.mul(a, a)), Nat.mul(U32.to_nat(b3), Nat.mul(Nat.mul(a, a), a))))) : Nat}
1511	
1512	def pk.m(b0, b1, b2, b3, a, m, ha, hm, h0, h1, h2, h3):
1513	  +x0 = U32.to_nat(b0)
1514	  +x1 = U32.to_nat(b1)
1515	  +x2 = U32.to_nat(b2)
1516	  +x3 = U32.to_nat(b3)
1517	  +a2 = Nat.mul(a, a)
1518	  +a3 = Nat.mul(a2, a)
1519	  +ap = {%ha : {Nat.is_lt(0n, _) == True{} : Bool}; N.pow_pos(8n) : {Nat.is_lt(0n, a) == True{} : Bool}}
1520	  +a2p = lt_mul_r(0n, a, a, ap, ap)
1521	  +a3p = lt_mul_r(0n, a2, a, a2p, ap)
1522	  +em = {%Equal.sym(Nat, m, Nat.mul(a3, a), p32(a, m, ha, hm)) : {Nat.is_le(Nat.mul(a, a3), _) == True{} : Bool}; %N.mul_comm(a3, a) : {Nat.is_le(_, Nat.mul(a3, a)) == True{} : Bool}; N.le_refl(Nat.mul(a3, a)) :
1523	    {Nat.is_le(Nat.mul(a, a3), m) == True{} : Bool}}
1524	  +la3 = {%Equal.sym(Nat, m, Nat.mul(a3, a), p32(a, m, ha, hm)) : {Nat.is_le(a3, _) == True{} : Bool}; le_mul_pos(a3, a, ap) : {Nat.is_le(a3, m) == True{} : Bool}}
1525	  +la2 = N.le_trans(a2, a3, m, le_mul_pos(a2, a, ap), la3)
1526	  +s1 = U32.shln(b1, 8n)
1527	  +s2 = U32.shln(b2, 16n)
1528	  +s3 = U32.shln(b3, 24n)
1529	  +v1 = shv(b1, 8n, a, a, m, hm, ha, h1, N.le_trans(Nat.mul(a, a), a3, m, le_mul_pos(a2, a, ap), la3), ap)
1530	  +v2 = shv(b2, 16n, a2, a, m, hm, p16(a, ha), h2,
1531	    %N.mul_comm(a2, a) : {Nat.is_le(_, m) == True{} : Bool}; la3, a2p)
1532	  +v3 = shv(b3, 24n, a3, a, m, hm, p24(a, ha), h3, em, a3p)
1533	  # y = s2 | s3 = x3 a3 + x2 a2
1534	  +yv = Nat.add(Nat.mul(x3, a3), Nat.mul(x2, a2))
1535	  +ey = Equal.trans(Nat, U32.to_nat(U32.or(s2, s3)), U32.to_nat(U32.or(s3, s2)), yv,
1536	    %or_comm(s2, s3) : {U32.to_nat(U32.or(s2, s3)) == U32.to_nat(_) : Nat}; {==},
1537	    %Equal.sym(Nat, U32.to_nat(U32.or(s3, s2)), Nat.add(U32.to_nat(s3), U32.to_nat(s2)),
1538	        U.to_nat_or_split(s3, s2, 24n,
1539	          %Equal.sym(Nat, Nat.pow(2n, 24n), Nat.mul(Nat.mul(a, a), a), p24(a, ha)) : {Nat.mod(U32.to_nat(s3), _) == 0n : Nat}
1540	          %Equal.sym(Nat, U32.to_nat(s3), Nat.mul(x3, a3), v3) : {Nat.mod(_, a3) == 0n : Nat}
1541	          N.mul_mod(x3, a3),
1542	          %Equal.sym(Nat, Nat.pow(2n, 24n), Nat.mul(Nat.mul(a, a), a), p24(a, ha)) : {Nat.is_lt(U32.to_nat(s2), _) == True{} : Bool}
1543	          %Equal.sym(Nat, U32.to_nat(s2), Nat.mul(x2, a2), v2) : {Nat.is_lt(_, a3) == True{} : Bool}
1544	          %N.mul_comm(a, a2) : {Nat.is_lt(Nat.mul(x2, a2), _) == True{} : Bool}
1545	          lt_mul_r(x2, a, a2, h2, a2p))) :
1546	      {_ == yv : Nat}
1547	    %Equal.sym(Nat, U32.to_nat(s3), Nat.mul(x3, a3), v3) : {Nat.add(_, U32.to_nat(s2)) == yv : Nat}
1548	    %Equal.sym(Nat, U32.to_nat(s2), Nat.mul(x2, a2), v2) : {Nat.add(Nat.mul(x3, a3), _) == yv : Nat}
1549	    {==})
1550	  # x = s1 | y = y + x1 a
1551	  +yw = U32.or(s2, s3)
1552	  +xv = Nat.add(yv, Nat.mul(x1, a))
1553	  +eq2 = Equal.trans(Nat, Nat.mul(Nat.add(Nat.mul(x3, a), x2), a2), Nat.add(Nat.mul(Nat.mul(x3, a), a2), Nat.mul(x2, a2)), yv,
1554	      N.mul_add_r(Nat.mul(x3, a), x2, a2),
1555	      Equal.cong(Nat, Nat, t => Nat.add(t, Nat.mul(x2, a2)), Nat.mul(Nat.mul(x3, a), a2), Nat.mul(x3, a3),
1556	        %N.mul_comm(a, a2) : {Nat.mul(Nat.mul(x3, a), a2) == Nat.mul(x3, _) : Nat}; N.mul_assoc(x3, a, a2)))
1557	  +ymul = {%eq2 : {Nat.mod(_, a2) == 0n : Nat}; N.mul_mod(Nat.add(Nat.mul(x3, a), x2), a2) : {Nat.mod(yv, a2) == 0n : Nat}}
1558	  +ex = Equal.trans(Nat, U32.to_nat(U32.or(s1, yw)), U32.to_nat(U32.or(yw, s1)), xv,
1559	    %or_comm(s1, yw) : {U32.to_nat(U32.or(s1, yw)) == U32.to_nat(_) : Nat}; {==},
1560	    %Equal.sym(Nat, U32.to_nat(U32.or(yw, s1)), Nat.add(U32.to_nat(yw), U32.to_nat(s1)),
1561	        U.to_nat_or_split(yw, s1, 16n,
1562	          %Equal.sym(Nat, Nat.pow(2n, 16n), Nat.mul(a, a), p16(a, ha)) : {Nat.mod(U32.to_nat(yw), _) == 0n : Nat}
1563	          %Equal.sym(Nat, U32.to_nat(yw), yv, ey) : {Nat.mod(_, a2) == 0n : Nat}
1564	          ymul,
1565	          %Equal.sym(Nat, Nat.pow(2n, 16n), Nat.mul(a, a), p16(a, ha)) : {Nat.is_lt(U32.to_nat(s1), _) == True{} : Bool}
1566	          %Equal.sym(Nat, U32.to_nat(s1), Nat.mul(x1, a), v1) : {Nat.is_lt(_, a2) == True{} : Bool}
1567	          lt_mul_r(x1, a, a, h1, ap))) :
1568	      {_ == xv : Nat}
1569	    %Equal.sym(Nat, U32.to_nat(yw), yv, ey) : {Nat.add(_, U32.to_nat(s1)) == xv : Nat}
1570	    %Equal.sym(Nat, U32.to_nat(s1), Nat.mul(x1, a), v1) : {Nat.add(yv, _) == xv : Nat}
1571	    {==})
1572	  # pack = b0 | x = x + x0
1573	  +xw = U32.or(s1, yw)
1574	  +q = Nat.add(Nat.mul(Nat.add(Nat.mul(x3, a), x2), a), x1)
1575	  +xmul = {%Equal.trans(Nat, Nat.mul(q, a), Nat.add(Nat.mul(Nat.mul(Nat.add(Nat.mul(x3, a), x2), a), a), Nat.mul(x1, a)), xv,
1576	      N.mul_add_r(Nat.mul(Nat.add(Nat.mul(x3, a), x2), a), x1, a),
1577	      Equal.cong(Nat, Nat, t => Nat.add(t, Nat.mul(x1, a)), Nat.mul(Nat.mul(Nat.add(Nat.mul(x3, a), x2), a), a), yv,
1578	        Equal.trans(Nat, Nat.mul(Nat.mul(Nat.add(Nat.mul(x3, a), x2), a), a), Nat.mul(Nat.add(Nat.mul(x3, a), x2), a2), yv,
1579	          N.mul_assoc(Nat.add(Nat.mul(x3, a), x2), a, a), eq2))) :
1580	      {Nat.mod(_, a) == 0n : Nat}; N.mul_mod(q, a) : {Nat.mod(xv, a) == 0n : Nat}}
1581	  %or_comm(xw, b0) : {U32.to_nat(_) == Nat.add(x0, Nat.add(Nat.mul(x1, a), Nat.add(Nat.mul(x2, a2), Nat.mul(x3, a3)))) : Nat}
1582	  %Equal.sym(Nat, U32.to_nat(U32.or(xw, b0)), Nat.add(U32.to_nat(xw), x0),
1583	      U.to_nat_or_split(xw, b0, 8n,
1584	        %Equal.sym(Nat, Nat.pow(2n, 8n), a, ha) : {Nat.mod(U32.to_nat(xw), _) == 0n : Nat}
1585	        %Equal.sym(Nat, U32.to_nat(xw), xv, ex) : {Nat.mod(_, a) == 0n : Nat}
1586	        xmul,
1587	        %Equal.sym(Nat, Nat.pow(2n, 8n), a, ha) : {Nat.is_lt(x0, _) == True{} : Bool}; h0)) :
1588	    {_ == Nat.add(x0, Nat.add(Nat.mul(x1, a), Nat.add(Nat.mul(x2, a2), Nat.mul(x3, a3)))) : Nat}
1589	  %Equal.sym(Nat, U32.to_nat(xw), xv, ex) : {Nat.add(_, x0) == Nat.add(x0, Nat.add(Nat.mul(x1, a), Nat.add(Nat.mul(x2, a2), Nat.mul(x3, a3)))) : Nat}
1590	  %N.add_comm(x0, xv) : {_ == Nat.add(x0, Nat.add(Nat.mul(x1, a), Nat.add(Nat.mul(x2, a2), Nat.mul(x3, a3)))) : Nat}
1591	  %N.add_comm(Nat.mul(x1, a), yv) : {Nat.add(x0, _) == Nat.add(x0, Nat.add(Nat.mul(x1, a), Nat.add(Nat.mul(x2, a2), Nat.mul(x3, a3)))) : Nat}
1592	  %N.add_comm(Nat.mul(x2, a2), Nat.mul(x3, a3)) : {Nat.add(x0, Nat.add(Nat.mul(x1, a), _)) == Nat.add(x0, Nat.add(Nat.mul(x1, a), Nat.add(Nat.mul(x2, a2), Nat.mul(x3, a3)))) : Nat}
1593	  {==}
1594	
1595	law to_nat_pack4:
1596	  for +b0: U32
1597	  for +b1: U32
1598	  for +b2: U32
1599	  for +b3: U32
1600	  for +h0: {U32.is_lt(b0, 256) == True{} : Bool}
1601	  for +h1: {U32.is_lt(b1, 256) == True{} : Bool}
1602	  for +h2: {U32.is_lt(b2, 256) == True{} : Bool}
1603	  for +h3: {U32.is_lt(b3, 256) == True{} : Bool}
1604	  {U32.to_nat(D.pack4(b0, b1, b2, b3)) == Nat.add(U32.to_nat(b0), Nat.add(Nat.mul(U32.to_nat(b1), Nat.pow(2n, 8n)), Nat.add(Nat.mul(U32.to_nat(b2), Nat.pow(2n, 16n)), Nat.mul(U32.to_nat(b3), Nat.pow(2n, 24n))))) : Nat}
1605	
1606	def to_nat_pack4(b0, b1, b2, b3, h0, h1, h2, h3):
1607	  %Equal.sym(Nat, Nat.pow(2n, 24n), Nat.mul(Nat.mul(Nat.pow(2n, 8n), Nat.pow(2n, 8n)), Nat.pow(2n, 8n)), p24(Nat.pow(2n, 8n), {==})) :
1608	    {U32.to_nat(D.pack4(b0, b1, b2, b3)) == Nat.add(U32.to_nat(b0), Nat.add(Nat.mul(U32.to_nat(b1), Nat.pow(2n, 8n)), Nat.add(Nat.mul(U32.to_nat(b2), Nat.pow(2n, 16n)), Nat.mul(U32.to_nat(b3), _)))) : Nat}
1609	  %Equal.sym(Nat, Nat.pow(2n, 16n), Nat.mul(Nat.pow(2n, 8n), Nat.pow(2n, 8n)), p16(Nat.pow(2n, 8n), {==})) :
1610	    {U32.to_nat(D.pack4(b0, b1, b2, b3)) == Nat.add(U32.to_nat(b0), Nat.add(Nat.mul(U32.to_nat(b1), Nat.pow(2n, 8n)), Nat.add(Nat.mul(U32.to_nat(b2), _),
1611	      Nat.mul(U32.to_nat(b3), Nat.mul(Nat.mul(Nat.pow(2n, 8n), Nat.pow(2n, 8n)), Nat.pow(2n, 8n)))))) : Nat}
1612	  pk.m(b0, b1, b2, b3, Nat.pow(2n, 8n), Nat.pow(2n, 32n), {==}, {==}, lt256(b0, h0), lt256(b1, h1), lt256(b2, h2), lt256(b3, h3))