1	# bend-mathlib/u32.bend: machine words as naturals; Word(n) and U32 operations agree with Nat arithmetic
2	# (compare, add, sub, inc, not, min, max, div, from_nat).
3	import Base
4	import ./nat.bend as MNat
5	
6	def internal_succ_double_lt(a: Nat, b: Nat, h: MNat.lt(a, b)) -> MNat.lt(1n+Nat.double(a), Nat.double(b)):
7	  match a b:
8	    case 0n 0n:
9	      Empty.absurd(MNat.lt(1n, 0n), MNat.internal_false_ne_true(h))
10	    case 0n 1n+q:
11	      {==}
12	    case 1n+p 0n:
13	      Empty.absurd(MNat.lt(3n+Nat.double(p), 0n), MNat.internal_false_ne_true(h))
14	    case 1n+p 1n+q:
15	      internal_succ_double_lt(p, q, h)
16	
17	# A word's value is below two to the width: to_nat w < 2^n.
18	law word_to_nat_lt:
19	  for n: Nat
20	  for w: Word(n)
21	  MNat.lt(Word.to_nat(n, w), Nat.pow(2n, n))
22	
23	def word_to_nat_lt(n, w):
24	  match n:
25	    case 0n:
26	      {==}
27	    case 1n++p:
28	      match w:
29	        case WCon{False{}, t}:
30	          +t = t
31	          %MNat.two_pow_succ_sym(p) : MNat.lt(Nat.double(Word.to_nat(p, t)), _)
32	          MNat.double_lt_double(Word.to_nat(p, t), Nat.pow(2n, p), word_to_nat_lt(p, t))
33	        case WCon{True{}, t}:
34	          +t = t
35	          %MNat.two_pow_succ_sym(p) : MNat.lt(1n+Nat.double(Word.to_nat(p, t)), _)
36	          internal_succ_double_lt(Word.to_nat(p, t), Nat.pow(2n, p), word_to_nat_lt(p, t))
37	
38	# The zero word is the natural zero: to_nat (zero n) = 0.
39	law word_to_nat_zero:
40	  for n: Nat
41	  {Word.to_nat(n, Word.zero(n)) == 0n : Nat}
42	
43	def word_to_nat_zero(n):
44	  match n:
45	    case 0n:
46	      {==}
47	    case 1n++p:
48	      Equal.cong(Nat, Nat, x => Nat.double(x), Word.to_nat(p, Word.zero(p)), 0n, word_to_nat_zero(p))
49	
50	# Distinct words have distinct values: to_nat a = to_nat b implies a = b.
51	law word_to_nat_inj:
52	  for n: Nat
53	  for a: Word(n)
54	  for b: Word(n)
55	  for e: {Word.to_nat(n, a) == Word.to_nat(n, b) : Nat}
56	  {a == b : Word(n)}
57	
58	def word_to_nat_inj(n, a, b, e):
59	  match n:
60	    case 0n:
61	      match a b:
62	        case WNil{} WNil{}:
63	          {==}
64	    case 1n++p:
65	      match a b:
66	        case WCon{False{}, +at} WCon{False{}, +bt}:
67	          Equal.cong(Word(p), Word(1n+p), w => WCon{False{}, w}, at, bt, word_to_nat_inj(p, at, bt, MNat.double_inj(Word.to_nat(p, at), Word.to_nat(p, bt), e)))
68	        case WCon{True{}, +at} WCon{True{}, +bt}:
69	          Equal.cong(Word(p), Word(1n+p), w => WCon{True{}, w}, at, bt, word_to_nat_inj(p, at, bt, MNat.double_inj(Word.to_nat(p, at), Word.to_nat(p, bt), MNat.succ_inj(Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt)), e))))
70	        case WCon{False{}, +at} WCon{True{}, +bt}:
71	          Empty.absurd({WCon{False{}, at} == WCon{True{}, bt} : Word(1n+p)}, MNat.double_ne_succ_double(Word.to_nat(p, at), Word.to_nat(p, bt))(e))
72	        case WCon{True{}, +at} WCon{False{}, +bt}:
73	          Empty.absurd({WCon{True{}, at} == WCon{False{}, bt} : Word(1n+p)}, MNat.double_ne_succ_double(Word.to_nat(p, bt), Word.to_nat(p, at))(Equal.sym(Nat, 1n+Nat.double(Word.to_nat(p, at)), Nat.double(Word.to_nat(p, bt)), e)))
74	
75	def internal_bv(b: Bool) -> Nat:
76	  Bool.pick(Nat, b, 1n, 0n)
77	
78	def internal_to_nat_con(-p: Nat, b: Bool, -t: Word(p)) -> {Nat.add(internal_bv(b), Nat.double(Word.to_nat(p, t))) == Word.to_nat(1n+p, WCon{b, t}) : Nat}:
79	  match b:
80	    case False{}:
81	      {==}
82	    case True{}:
83	      {==}
84	
85	def internal_cmp_bits(x: Nat, y: Nat, ab: Bool, bb: Bool) -> {Word.cmp.fin(ab, bb, Nat.cmp(x, y)) == Nat.cmp(Nat.add(internal_bv(ab), Nat.double(x)), Nat.add(internal_bv(bb), Nat.double(y))) : Cmp}:
86	  match x y:
87	    case 0n 0n:
88	      match ab bb:
89	        case False{} False{}:
90	          {==}
91	        case False{} True{}:
92	          {==}
93	        case True{} False{}:
94	          {==}
95	        case True{} True{}:
96	          {==}
97	    case 0n 1n+q:
98	      match ab bb:
99	        case False{} False{}:
100	          {==}
101	        case False{} True{}:
102	          {==}
103	        case True{} False{}:
104	          {==}
105	        case True{} True{}:
106	          {==}
107	    case 1n+p 0n:
108	      match ab bb:
109	        case False{} False{}:
110	          {==}
111	        case False{} True{}:
112	          {==}
113	        case True{} False{}:
114	          {==}
115	        case True{} True{}:
116	          {==}
117	    case 1n+p 1n+q:
118	      match ab bb:
119	        case False{} False{}:
120	          internal_cmp_bits(p, q, False{}, False{})
121	        case False{} True{}:
122	          internal_cmp_bits(p, q, False{}, True{})
123	        case True{} False{}:
124	          internal_cmp_bits(p, q, True{}, False{})
125	        case True{} True{}:
126	          internal_cmp_bits(p, q, True{}, True{})
127	
128	# Comparing words compares their values: cmp a b = cmp (to_nat a) (to_nat b).
129	law word_cmp_to_nat:
130	  for n: Nat
131	  for a: Word(n)
132	  for b: Word(n)
133	  {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}
134	
135	def word_cmp_to_nat(n, a, b):
136	  match n:
137	    case 0n:
138	      {==}
139	    case 1n++p:
140	      match a b:
141	        case WCon{+ab, +at} WCon{+bb, +bt}:
142	          %internal_to_nat_con(p, ab, at) : {Word.cmp.fin(ab, bb, Word.cmp(p, at, bt)) == Nat.cmp(_, Word.to_nat(1n+p, WCon{bb, bt})) : Cmp}
143	          %internal_to_nat_con(p, bb, bt) : {Word.cmp.fin(ab, bb, Word.cmp(p, at, bt)) == Nat.cmp(Nat.add(internal_bv(ab), Nat.double(Word.to_nat(p, at))), _) : Cmp}
144	          %Equal.sym(Cmp, Word.cmp(p, at, bt), Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt)), word_cmp_to_nat(p, at, bt)) : {Word.cmp.fin(ab, bb, _) == Nat.cmp(Nat.add(internal_bv(ab), Nat.double(Word.to_nat(p, at))), Nat.add(internal_bv(bb), Nat.double(Word.to_nat(p, bt)))) : Cmp}
145	          internal_cmp_bits(Word.to_nat(p, at), Word.to_nat(p, bt), ab, bb)
146	
147	# One plus a word plus its complement is two to the width: 1 + to_nat (not w) + to_nat w = 2^n.
148	law word_not_add:
149	  for n: Nat
150	  for w: Word(n)
151	  {1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) == Nat.pow(2n, n) : Nat}
152	
153	def word_not_add(n, w):
154	  match n:
155	    case 0n:
156	      {==}
157	    case 1n++p:
158	      match w:
159	        case WCon{False{}, +t}:
160	          -u = Word.to_nat(p, Word.not(p, t))
161	          -x = Word.to_nat(p, t)
162	          %MNat.two_pow_succ_sym(p) : {2n+Nat.add(Nat.double(u), Nat.double(x)) == _ : Nat}
163	          %word_not_add(p, t) : {2n+Nat.add(Nat.double(u), Nat.double(x)) == Nat.double(_) : Nat}
164	          %MNat.double_add(Word.to_nat(p, Word.not(p, t)), Word.to_nat(p, t)) : {2n+_ == 2n+Nat.double(Nat.add(u, x)) : Nat}
165	          {==}
166	        case WCon{True{}, +t}:
167	          -u = Word.to_nat(p, Word.not(p, t))
168	          -x = Word.to_nat(p, t)
169	          %MNat.add_succ_sym(Nat.double(Word.to_nat(p, Word.not(p, t))), Nat.double(Word.to_nat(p, t))) : {1n+_ == Nat.pow(2n, 1n+p) : Nat}
170	          %MNat.two_pow_succ_sym(p) : {2n+Nat.add(Nat.double(u), Nat.double(x)) == _ : Nat}
171	          %word_not_add(p, t) : {2n+Nat.add(Nat.double(u), Nat.double(x)) == Nat.double(_) : Nat}
172	          %MNat.double_add(Word.to_nat(p, Word.not(p, t)), Word.to_nat(p, t)) : {2n+_ == 2n+Nat.double(Nat.add(u, x)) : Nat}
173	          {==}
174	
175	def internal_pick_pow(o: Bool, p: Nat) -> {Nat.double(Bool.pick(Nat, o, Nat.pow(2n, p), 0n)) == Bool.pick(Nat, o, Nat.pow(2n, 1n+p), 0n) : Nat}:
176	  match o:
177	    case False{}:
178	      {==}
179	    case True{}:
180	      MNat.two_pow_succ_sym(p)
181	
182	def internal_carry(n: Nat, a: Word(n), b: Word(n), c: Bool) -> Bool:
183	  match n:
184	    case 0n:
185	      c
186	    case 1n+p:
187	      match a b:
188	        case WCon{False{}, at} WCon{+bb, bt}:
189	          internal_carry(p, at, bt, Bool.and(bb, c))
190	        case WCon{True{}, at} WCon{+bb, bt}:
191	          internal_carry(p, at, bt, Bool.or(bb, c))
192	
193	def internal_full_add(a: Bool, b: Bool, c: Bool) -> {Nat.add(Nat.add(internal_bv(a), internal_bv(b)), internal_bv(c)) == Nat.add(internal_bv(Pair.fst(Bool, Bool, Bool.full_add(a, b, c))), Nat.double(internal_bv(Pair.snd(Bool, Bool, Bool.full_add(a, b, c))))) : Nat}:
194	  match a b c:
195	    case False{} False{} False{}:
196	      {==}
197	    case False{} False{} True{}:
198	      {==}
199	    case False{} True{} False{}:
200	      {==}
201	    case False{} True{} True{}:
202	      {==}
203	    case True{} False{} False{}:
204	      {==}
205	    case True{} False{} True{}:
206	      {==}
207	    case True{} True{} False{}:
208	      {==}
209	    case True{} True{} True{}:
210	      {==}
211	
212	def internal_adc_nat(+s: Nat, +k: Nat, +a: Nat, +b: Nat, +c: Nat, +e: Nat, +q: Nat, +x: Nat, +y: Nat,
213	  ih: {Nat.add(e, q) == Nat.add(Nat.add(x, y), k) : Nat},
214	  fa: {Nat.add(Nat.add(a, b), c) == Nat.add(s, Nat.double(k)) : Nat})
215	  -> {Nat.add(Nat.add(s, Nat.double(e)), Nat.double(q)) == Nat.add(Nat.add(Nat.add(a, Nat.double(x)), Nat.add(b, Nat.double(y))), c) : Nat}:
216	  -d = Nat.double(Nat.add(x, y))
217	  -r = Nat.add(Nat.add(Nat.add(a, Nat.double(x)), Nat.add(b, Nat.double(y))), c)
218	  %MNat.add_assoc_sym(s, Nat.double(e), Nat.double(q)) : {_ == r : Nat}
219	  %MNat.double_add(e, q) : {Nat.add(s, _) == r : Nat}
220	  %Equal.sym(Nat, Nat.add(e, q), Nat.add(Nat.add(x, y), k), ih) : {Nat.add(s, Nat.double(_)) == r : Nat}
221	  %MNat.double_add_sym(Nat.add(x, y), k) : {Nat.add(s, _) == r : Nat}
222	  -l = Nat.add(s, Nat.add(d, Nat.double(k)))
223	  %MNat.add_add_add_comm(a, b, Nat.double(x), Nat.double(y)) : {l == Nat.add(_, c) : Nat}
224	  %MNat.double_add(x, y) : {l == Nat.add(Nat.add(Nat.add(a, b), _), c) : Nat}
225	  %MNat.add_right_comm_sym(Nat.add(a, b), Nat.double(Nat.add(x, y)), c) : {l == _ : Nat}
226	  %Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(s, Nat.double(k)), fa) : {l == Nat.add(_, d) : Nat}
227	  %MNat.add_assoc_sym(s, Nat.double(k), Nat.double(Nat.add(x, y))) : {l == _ : Nat}
228	  %MNat.add_comm(Nat.double(Nat.add(x, y)), Nat.double(k)) : {l == Nat.add(s, _) : Nat}
229	  {==}
230	
231	def internal_adc_core(n: Nat, a: Word(n), b: Word(n), c: Bool) -> {Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Bool.pick(Nat, internal_carry(n, a, b, c), Nat.pow(2n, n), 0n)) == Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), internal_bv(c)) : Nat}:
232	  match n:
233	    case 0n:
234	      match c:
235	        case False{}:
236	          {==}
237	        case True{}:
238	          {==}
239	    case 1n++p:
240	      match a b:
241	        case WCon{False{}, +at} WCon{+bb, +bt}:
242	          +c = c
243	          -e = Word.adc(p, at, bt, False{}, Bool.and(bb, c))
244	          -o = internal_carry(p, at, bt, Bool.and(bb, c))
245	          -r = Nat.add(Nat.add(Word.to_nat(1n+p, WCon{False{}, at}), Word.to_nat(1n+p, WCon{bb, bt})), internal_bv(c))
246	          %internal_to_nat_con(p, Bool.xor(bb, c), Word.adc(p, at, bt, False{}, Bool.and(bb, c))) : {Nat.add(_, Bool.pick(Nat, o, Nat.pow(2n, 1n+p), 0n)) == r : Nat}
247	          %internal_pick_pow(internal_carry(p, at, bt, Bool.and(bb, c)), p) : {Nat.add(Nat.add(internal_bv(Bool.xor(bb, c)), Nat.double(Word.to_nat(p, e))), _) == r : Nat}
248	          -l = Nat.add(Nat.add(internal_bv(Bool.xor(bb, c)), Nat.double(Word.to_nat(p, e))), Nat.double(Bool.pick(Nat, o, Nat.pow(2n, p), 0n)))
249	          %internal_to_nat_con(p, False{}, at) : {l == Nat.add(Nat.add(_, Word.to_nat(1n+p, WCon{bb, bt})), internal_bv(c)) : Nat}
250	          %internal_to_nat_con(p, bb, bt) : {l == Nat.add(Nat.add(Nat.add(internal_bv(False{}), Nat.double(Word.to_nat(p, at))), _), internal_bv(c)) : Nat}
251	          internal_adc_nat(internal_bv(Bool.xor(bb, c)), internal_bv(Bool.and(bb, c)), internal_bv(False{}), internal_bv(bb), internal_bv(c), Word.to_nat(p, Word.adc(p, at, bt, False{}, Bool.and(bb, c))), Bool.pick(Nat, internal_carry(p, at, bt, Bool.and(bb, c)), Nat.pow(2n, p), 0n), Word.to_nat(p, at), Word.to_nat(p, bt), internal_adc_core(p, at, bt, Bool.and(bb, c)), internal_full_add(False{}, bb, c))
252	        case WCon{True{}, +at} WCon{+bb, +bt}:
253	          +c = c
254	          -e = Word.adc(p, at, bt, False{}, Bool.or(bb, c))
255	          -o = internal_carry(p, at, bt, Bool.or(bb, c))
256	          -r = Nat.add(Nat.add(Word.to_nat(1n+p, WCon{True{}, at}), Word.to_nat(1n+p, WCon{bb, bt})), internal_bv(c))
257	          %internal_to_nat_con(p, Bool.not(Bool.xor(bb, c)), Word.adc(p, at, bt, False{}, Bool.or(bb, c))) : {Nat.add(_, Bool.pick(Nat, o, Nat.pow(2n, 1n+p), 0n)) == r : Nat}
258	          %internal_pick_pow(internal_carry(p, at, bt, Bool.or(bb, c)), p) : {Nat.add(Nat.add(internal_bv(Bool.not(Bool.xor(bb, c))), Nat.double(Word.to_nat(p, e))), _) == r : Nat}
259	          -l = Nat.add(Nat.add(internal_bv(Bool.not(Bool.xor(bb, c))), Nat.double(Word.to_nat(p, e))), Nat.double(Bool.pick(Nat, o, Nat.pow(2n, p), 0n)))
260	          %internal_to_nat_con(p, True{}, at) : {l == Nat.add(Nat.add(_, Word.to_nat(1n+p, WCon{bb, bt})), internal_bv(c)) : Nat}
261	          %internal_to_nat_con(p, bb, bt) : {l == Nat.add(Nat.add(Nat.add(internal_bv(True{}), Nat.double(Word.to_nat(p, at))), _), internal_bv(c)) : Nat}
262	          internal_adc_nat(internal_bv(Bool.not(Bool.xor(bb, c))), internal_bv(Bool.or(bb, c)), internal_bv(True{}), internal_bv(bb), internal_bv(c), Word.to_nat(p, Word.adc(p, at, bt, False{}, Bool.or(bb, c))), Bool.pick(Nat, internal_carry(p, at, bt, Bool.or(bb, c)), Nat.pow(2n, p), 0n), Word.to_nat(p, at), Word.to_nat(p, bt), internal_adc_core(p, at, bt, Bool.or(bb, c)), internal_full_add(True{}, bb, c))
263	
264	def internal_lt_congl(-x: Nat, -y: Nat, -m: Nat, e: {x == y : Nat}, h: MNat.lt(x, m)) -> MNat.lt(y, m):
265	  %e : MNat.lt(_, m)
266	  h
267	
268	def internal_le_congr(-m: Nat, -x: Nat, -y: Nat, e: {y == x : Nat}, h: MNat.le(m, y)) -> MNat.le(m, x):
269	  %e : MNat.le(m, _)
270	  h
271	
272	def internal_fin_exact(+e: Nat, +s: Nat, +m: Nat, o: Bool, eq: {Nat.add(e, Bool.pick(Nat, o, m, 0n)) == s : Nat}, h: MNat.lt(s, m)) -> {e == s : Nat}:
273	  match o:
274	    case False{}:
275	      Equal.trans(Nat, e, Nat.add(e, 0n), s, MNat.add_zero_sym(e), eq)
276	    case True{}:
277	      +le = MNat.le_of_add_eq(m, e, s, Equal.trans(Nat, Nat.add(m, e), Nat.add(e, m), s, MNat.add_comm(m, e), eq))
278	      Empty.absurd({e == s : Nat}, MNat.lt_irrefl(s)(MNat.lt_of_lt_of_le(s, m, s, h, le)))
279	
280	def internal_fin_wrap(+e: Nat, -s: Nat, +m: Nat, o: Bool, eq: {Nat.add(e, Bool.pick(Nat, o, m, 0n)) == s : Nat}, h: MNat.lt(e, m)) -> {e == Nat.mod(s, m) : Nat}:
281	  match o:
282	    case False{}:
283	      %eq : {e == Nat.mod(_, m) : Nat}
284	      %MNat.add_zero_sym(e) : {e == Nat.mod(_, m) : Nat}
285	      Equal.sym(Nat, Nat.mod(e, m), e, MNat.mod_eq_of_lt(e, m, h))
286	    case True{}:
287	      %eq : {e == Nat.mod(_, m) : Nat}
288	      %MNat.add_comm(m, e) : {e == Nat.mod(_, m) : Nat}
289	      %MNat.add_mod_left_sym(e, m) : {e == _ : Nat}
290	      Equal.sym(Nat, Nat.mod(e, m), e, MNat.mod_eq_of_lt(e, m, h))
291	
292	def internal_fin_over(+e: Nat, +s: Nat, +m: Nat, o: Bool, eq: {Nat.add(e, Bool.pick(Nat, o, m, 0n)) == s : Nat}, h: MNat.lt(e, m), le: MNat.le(m, s)) -> {Nat.add(e, m) == s : Nat}:
293	  match o:
294	    case False{}:
295	      +es = Equal.trans(Nat, e, Nat.add(e, 0n), s, MNat.add_zero_sym(e), eq)
296	      Empty.absurd({Nat.add(e, m) == s : Nat}, MNat.lt_irrefl(m)(MNat.lt_of_le_of_lt(m, s, m, le, internal_lt_congl(e, s, m, es, h))))
297	    case True{}:
298	      eq
299	
300	# The adder is exact below the overflow: a + b + carry-in < 2^n implies to_nat (adc a b False c) = a + b + carry-in.
301	law word_adc_exact:
302	  for n: Nat
303	  for a: Word(n)
304	  for b: Word(n)
305	  for c: Bool
306	  for h: MNat.lt(Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n))
307	  {Word.to_nat(n, Word.adc(n, a, b, False{}, c)) == Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)) : Nat}
308	
309	def word_adc_exact(n, a, b, c, h):
310	  +n = n
311	  +a = a
312	  +b = b
313	  +c = c
314	  internal_fin_exact(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n), internal_carry(n, a, b, c), internal_adc_core(n, a, b, c), h)
315	
316	# The adder drops exactly one 2^n on overflow: 2^n <= a + b + carry-in implies to_nat (adc a b False c) + 2^n = a + b + carry-in.
317	law word_adc_overflow:
318	  for n: Nat
319	  for a: Word(n)
320	  for b: Word(n)
321	  for c: Bool
322	  for h: MNat.le(Nat.pow(2n, n), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)))
323	  {Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.pow(2n, n)) == Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)) : Nat}
324	
325	def word_adc_overflow(n, a, b, c, h):
326	  +n = n
327	  +a = a
328	  +b = b
329	  +c = c
330	  internal_fin_over(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n), internal_carry(n, a, b, c), internal_adc_core(n, a, b, c), word_to_nat_lt(n, Word.adc(n, a, b, False{}, c)), h)
331	
332	# The adder wraps modulo 2^n: to_nat (adc a b False c) = (a + b + carry-in) % 2^n.
333	law word_adc_wrap:
334	  for n: Nat
335	  for a: Word(n)
336	  for b: Word(n)
337	  for c: Bool
338	  {Word.to_nat(n, Word.adc(n, a, b, False{}, c)) == Nat.mod(Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n)) : Nat}
339	
340	def word_adc_wrap(n, a, b, c):
341	  +n = n
342	  +a = a
343	  +b = b
344	  +c = c
345	  internal_fin_wrap(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n), internal_carry(n, a, b, c), internal_adc_core(n, a, b, c), word_to_nat_lt(n, Word.adc(n, a, b, False{}, c)))
346	
347	# Word addition is exact without overflow: a + b < 2^n implies to_nat (add a b) = a + b.
348	law word_add_exact:
349	  for n: Nat
350	  for a: Word(n)
351	  for b: Word(n)
352	  for h: MNat.lt(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n))
353	  {Word.to_nat(n, Word.add(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
354	
355	def word_add_exact(n, a, b, h):
356	  +n = n
357	  +a = a
358	  +b = b
359	  %MNat.add_zero(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : {Word.to_nat(n, Word.add(n, a, b)) == _ : Nat}
360	  word_adc_exact(n, a, b, False{}, internal_lt_congl(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), 0n), Nat.pow(2n, n), MNat.add_zero_sym(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))), h))
361	
362	# Word addition wraps modulo 2^n: to_nat (add a b) = (a + b) % 2^n.
363	law word_add_wrap:
364	  for n: Nat
365	  for a: Word(n)
366	  for b: Word(n)
367	  {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}
368	
369	def word_add_wrap(n, a, b):
370	  +n = n
371	  +a = a
372	  +b = b
373	  %MNat.add_zero(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b))) : {Word.to_nat(n, Word.add(n, a, b)) == Nat.mod(_, Nat.pow(2n, n)) : Nat}
374	  word_adc_wrap(n, a, b, False{})
375	
376	def internal_inc_carry(n: Nat, w: Word(n)) -> Bool:
377	  match n:
378	    case 0n:
379	      True{}
380	    case 1n+p:
381	      match w:
382	        case WCon{False{}, t}:
383	          False{}
384	        case WCon{True{}, t}:
385	          internal_inc_carry(p, t)
386	
387	def internal_inc_core(n: Nat, w: Word(n)) -> {Nat.add(Word.to_nat(n, Word.inc(n, w)), Bool.pick(Nat, internal_inc_carry(n, w), Nat.pow(2n, n), 0n)) == 1n+Word.to_nat(n, w) : Nat}:
388	  match n:
389	    case 0n:
390	      {==}
391	    case 1n++p:
392	      match w:
393	        case WCon{False{}, t}:
394	          MNat.add_zero(1n+Nat.double(Word.to_nat(p, t)))
395	        case WCon{True{}, +t}:
396	          -x = Word.to_nat(p, t)
397	          %internal_pick_pow(internal_inc_carry(p, t), p) : {Nat.add(Nat.double(Word.to_nat(p, Word.inc(p, t))), _) == 2n+Nat.double(x) : Nat}
398	          %MNat.double_add(Word.to_nat(p, Word.inc(p, t)), Bool.pick(Nat, internal_inc_carry(p, t), Nat.pow(2n, p), 0n)) : {_ == 2n+Nat.double(x) : Nat}
399	          Equal.cong(Nat, Nat, z => Nat.double(z), Nat.add(Word.to_nat(p, Word.inc(p, t)), Bool.pick(Nat, internal_inc_carry(p, t), Nat.pow(2n, p), 0n)), 1n+Word.to_nat(p, t), internal_inc_core(p, t))
400	
401	# Increment is exact without overflow: 1 + w < 2^n implies to_nat (inc w) = 1 + w.
402	law word_inc_exact:
403	  for n: Nat
404	  for w: Word(n)
405	  for h: MNat.lt(1n+Word.to_nat(n, w), Nat.pow(2n, n))
406	  {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}
407	
408	def word_inc_exact(n, w, h):
409	  +n = n
410	  +w = w
411	  internal_fin_exact(Word.to_nat(n, Word.inc(n, w)), 1n+Word.to_nat(n, w), Nat.pow(2n, n), internal_inc_carry(n, w), internal_inc_core(n, w), h)
412	
413	# Increment wraps modulo 2^n: to_nat (inc w) = (1 + w) % 2^n.
414	law word_inc_wrap:
415	  for n: Nat
416	  for w: Word(n)
417	  {Word.to_nat(n, Word.inc(n, w)) == Nat.mod(1n+Word.to_nat(n, w), Nat.pow(2n, n)) : Nat}
418	
419	def word_inc_wrap(n, w):
420	  +n = n
421	  +w = w
422	  internal_fin_wrap(Word.to_nat(n, Word.inc(n, w)), 1n+Word.to_nat(n, w), Nat.pow(2n, n), internal_inc_carry(n, w), internal_inc_core(n, w), word_to_nat_lt(n, Word.inc(n, w)))
423	
424	def internal_adc_not(n: Nat, a: Word(n), b: Word(n), c: Bool) -> {Word.adc(n, a, b, True{}, c) == Word.adc(n, a, Word.not(n, b), False{}, c) : Word(n)}:
425	  match n:
426	    case 0n:
427	      {==}
428	    case 1n++p:
429	      match a b:
430	        case WCon{False{}, +at} WCon{+bb, +bt}:
431	          +c = c
432	          Equal.cong(Word(p), Word(1n+p), w => WCon{Bool.xor(Bool.not(bb), c), w}, Word.adc(p, at, bt, True{}, Bool.and(Bool.not(bb), c)), Word.adc(p, at, Word.not(p, bt), False{}, Bool.and(Bool.not(bb), c)), internal_adc_not(p, at, bt, Bool.and(Bool.not(bb), c)))
433	        case WCon{True{}, +at} WCon{+bb, +bt}:
434	          +c = c
435	          Equal.cong(Word(p), Word(1n+p), w => WCon{Bool.not(Bool.xor(Bool.not(bb), c)), w}, Word.adc(p, at, bt, True{}, Bool.or(Bool.not(bb), c)), Word.adc(p, at, Word.not(p, bt), False{}, Bool.or(Bool.not(bb), c)), internal_adc_not(p, at, bt, Bool.or(Bool.not(bb), c)))
436	
437	def internal_sub_arith(+x: Nat, +y: Nat, +u: Nat, -m: Nat, h: MNat.le(y, x), c: {1n+Nat.add(u, y) == m : Nat}) -> {Nat.add(Nat.add(x, u), 1n) == Nat.add(Nat.sub(x, y), m) : Nat}:
438	  -d = Nat.sub(x, y)
439	  %c : {Nat.add(Nat.add(x, u), 1n) == Nat.add(d, _) : Nat}
440	  %MNat.add_sub_of_le(y, x, h) : {Nat.add(Nat.add(_, u), 1n) == Nat.add(d, 1n+Nat.add(u, y)) : Nat}
441	  -l = Nat.add(Nat.add(Nat.add(y, d), u), 1n)
442	  %MNat.add_succ_sym(Nat.sub(x, y), Nat.add(u, y)) : {l == _ : Nat}
443	  %MNat.add_comm(1n, Nat.add(Nat.add(y, Nat.sub(x, y)), u)) : {_ == 1n+Nat.add(d, Nat.add(u, y)) : Nat}
444	  -l2 = Nat.add(1n, Nat.add(Nat.add(y, d), u))
445	  %MNat.add_comm(y, u) : {l2 == 1n+Nat.add(d, _) : Nat}
446	  %MNat.add_left_comm(y, Nat.sub(x, y), u) : {l2 == 1n+_ : Nat}
447	  %MNat.add_assoc(y, Nat.sub(x, y), u) : {l2 == 1n+_ : Nat}
448	  {==}
449	
450	# Word subtraction is exact without underflow: b <= a implies to_nat (sub a b) = a - b.
451	law word_sub_exact:
452	  for n: Nat
453	  for a: Word(n)
454	  for b: Word(n)
455	  for h: MNat.le(Word.to_nat(n, b), Word.to_nat(n, a))
456	  {Word.to_nat(n, Word.sub(n, a, b)) == Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
457	
458	def word_sub_exact(n, a, b, h):
459	  +n = n
460	  +a = a
461	  +b = b
462	  -x = Word.to_nat(n, a)
463	  -y = Word.to_nat(n, b)
464	  -nb = Word.not(n, b)
465	  -e = Word.to_nat(n, Word.adc(n, a, nb, False{}, True{}))
466	  -s = Nat.add(Nat.add(x, Word.to_nat(n, nb)), 1n)
467	  -m = Nat.pow(2n, n)
468	  %Equal.sym(Word(n), Word.adc(n, a, b, True{}, True{}), Word.adc(n, a, Word.not(n, b), False{}, True{}), internal_adc_not(n, a, b, True{})) : {Word.to_nat(n, _) == Nat.sub(x, y) : Nat}
469	  +ar = internal_sub_arith(Word.to_nat(n, a), Word.to_nat(n, b), Word.to_nat(n, Word.not(n, b)), Nat.pow(2n, n), h, word_not_add(n, b))
470	  +le = internal_le_congr(Nat.pow(2n, n), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, Word.not(n, b))), 1n), Nat.add(Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n)), Equal.sym(Nat, s, Nat.add(Nat.sub(x, y), m), ar), MNat.le_add_left(Nat.pow(2n, n), Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b))))
471	  +ov = internal_fin_over(Word.to_nat(n, Word.adc(n, a, Word.not(n, b), False{}, True{})), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, Word.not(n, b))), 1n), Nat.pow(2n, n), internal_carry(n, a, Word.not(n, b), True{}), internal_adc_core(n, a, Word.not(n, b), True{}), word_to_nat_lt(n, Word.adc(n, a, Word.not(n, b), False{}, True{})), le)
472	  MNat.add_right_cancel(Word.to_nat(n, Word.adc(n, a, Word.not(n, b), False{}, True{})), Nat.pow(2n, n), Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)), Equal.trans(Nat, Nat.add(e, m), s, Nat.add(Nat.sub(x, y), m), ov, ar))
473	
474	def internal_sub_wrap_arith(+x: Nat, +y: Nat, +u: Nat, -m: Nat, c: {1n+Nat.add(u, y) == m : Nat}) -> {Nat.add(Nat.add(x, u), 1n) == Nat.add(x, Nat.sub(m, y)) : Nat}:
475	  %c : {Nat.add(Nat.add(x, u), 1n) == Nat.add(x, Nat.sub(_, y)) : Nat}
476	  %MNat.add_sub_cancel_sym(1n+u, y) : {Nat.add(Nat.add(x, u), 1n) == Nat.add(x, _) : Nat}
477	  %MNat.add_succ_sym(x, u) : {Nat.add(Nat.add(x, u), 1n) == _ : Nat}
478	  MNat.add_comm(Nat.add(x, u), 1n)
479	
480	# Word subtraction wraps modulo 2^n: to_nat (sub a b) = (a + (2^n - b)) % 2^n.
481	law word_sub_wrap:
482	  for n: Nat
483	  for a: Word(n)
484	  for b: Word(n)
485	  {Word.to_nat(n, Word.sub(n, a, b)) == Nat.mod(Nat.add(Word.to_nat(n, a), Nat.sub(Nat.pow(2n, n), Word.to_nat(n, b))), Nat.pow(2n, n)) : Nat}
486	
487	def word_sub_wrap(n, a, b):
488	  +n = n
489	  +a = a
490	  +b = b
491	  -x = Word.to_nat(n, a)
492	  -y = Word.to_nat(n, b)
493	  -u = Word.to_nat(n, Word.not(n, b))
494	  -m = Nat.pow(2n, n)
495	  %Equal.sym(Word(n), Word.adc(n, a, b, True{}, True{}), Word.adc(n, a, Word.not(n, b), False{}, True{}), internal_adc_not(n, a, b, True{})) : {Word.to_nat(n, _) == Nat.mod(Nat.add(x, Nat.sub(m, y)), m) : Nat}
496	  %internal_sub_wrap_arith(Word.to_nat(n, a), Word.to_nat(n, b), Word.to_nat(n, Word.not(n, b)), Nat.pow(2n, n), word_not_add(n, b)) : {Word.to_nat(n, Word.adc(n, a, Word.not(n, b), False{}, True{})) == Nat.mod(_, m) : Nat}
497	  word_adc_wrap(n, a, Word.not(n, b), True{})
498	
499	def internal_bound(-s: Nat, -m: Nat, e: {Nat.pow(2n, 32n) == m : Nat}, h: MNat.lt(s, m)) -> MNat.lt(s, Nat.pow(2n, 32n)):
500	  %Equal.sym(Nat, Nat.pow(2n, 32n), m, e) : MNat.lt(s, _)
501	  h
502	
503	def internal_u32_to_nat_lt(-m: Nat, a: U32, e: {Nat.pow(2n, 32n) == m : Nat}) -> MNat.lt(U32.to_nat(a), m):
504	  match a:
505	    case U32{w}:
506	      %e : MNat.lt(Word.to_nat(32n, w), _)
507	      word_to_nat_lt(32n, w)
508	
509	# A U32's value is below 2^32.
510	law u32_to_nat_lt:
511	  for a: U32
512	  MNat.lt(U32.to_nat(a), Nat.pow(2n, 32n))
513	
514	def u32_to_nat_lt(a):
515	  internal_u32_to_nat_lt(Nat.pow(2n, 32n), a, {==})
516	
517	# Distinct U32s have distinct values: to_nat a = to_nat b implies a = b.
518	law u32_to_nat_inj:
519	  for a: U32
520	  for b: U32
521	  for e: {U32.to_nat(a) == U32.to_nat(b) : Nat}
522	  {a == b : U32}
523	
524	def u32_to_nat_inj(a, b, e):
525	  match a b:
526	    case U32{+x} U32{+y}:
527	      Equal.cong(Word(32n), U32, w => U32{w}, x, y, word_to_nat_inj(32n, x, y, e))
528	
529	# Comparing U32s compares their values: cmp a b = cmp (to_nat a) (to_nat b).
530	law u32_cmp_to_nat:
531	  for a: U32
532	  for b: U32
533	  {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}
534	
535	def u32_cmp_to_nat(a, b):
536	  match a b:
537	    case U32{x} U32{y}:
538	      word_cmp_to_nat(32n, x, y)
539	
540	# U32 equality tests the values: is_eq a b = is_eq (to_nat a) (to_nat b).
541	law u32_is_eq_to_nat:
542	  for a: U32
543	  for b: U32
544	  {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}
545	
546	def u32_is_eq_to_nat(a, b):
547	  +a = a
548	  +b = b
549	  Equal.cong(Cmp, Bool, k => Cmp.is_eq(k), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
550	
551	# U32 disequality tests the values: is_ne a b = is_ne (to_nat a) (to_nat b).
552	law u32_is_ne_to_nat:
553	  for a: U32
554	  for b: U32
555	  {U32.is_ne(a, b) == Nat.is_ne(U32.to_nat(a), U32.to_nat(b)) : Bool}
556	
557	def u32_is_ne_to_nat(a, b):
558	  +a = a
559	  +b = b
560	  Equal.cong(Cmp, Bool, k => Bool.not(Cmp.is_eq(k)), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
561	
562	# The U32 strict order is the order of the values: is_lt a b = is_lt (to_nat a) (to_nat b).
563	law u32_is_lt_to_nat:
564	  for a: U32
565	  for b: U32
566	  {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}
567	
568	def u32_is_lt_to_nat(a, b):
569	  +a = a
570	  +b = b
571	  Equal.cong(Cmp, Bool, k => Cmp.is_lt(k), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
572	
573	# The U32 order is the order of the values: is_le a b = is_le (to_nat a) (to_nat b).
574	law u32_is_le_to_nat:
575	  for a: U32
576	  for b: U32
577	  {U32.is_le(a, b) == Nat.is_le(U32.to_nat(a), U32.to_nat(b)) : Bool}
578	
579	def u32_is_le_to_nat(a, b):
580	  +a = a
581	  +b = b
582	  Equal.cong(Cmp, Bool, k => Cmp.is_le(k), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
583	
584	# The reverse U32 strict order is that of the values: is_gt a b = is_gt (to_nat a) (to_nat b).
585	law u32_is_gt_to_nat:
586	  for a: U32
587	  for b: U32
588	  {U32.is_gt(a, b) == Nat.is_gt(U32.to_nat(a), U32.to_nat(b)) : Bool}
589	
590	def u32_is_gt_to_nat(a, b):
591	  +a = a
592	  +b = b
593	  Equal.cong(Cmp, Bool, k => Cmp.is_gt(k), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
594	
595	# The reverse U32 order is that of the values: is_ge a b = is_ge (to_nat a) (to_nat b).
596	law u32_is_ge_to_nat:
597	  for a: U32
598	  for b: U32
599	  {U32.is_ge(a, b) == Nat.is_ge(U32.to_nat(a), U32.to_nat(b)) : Bool}
600	
601	def u32_is_ge_to_nat(a, b):
602	  +a = a
603	  +b = b
604	  Equal.cong(Cmp, Bool, k => Cmp.is_ge(k), U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
605	
606	def internal_u32_add_exact(-m: Nat, a: U32, b: U32, e: {Nat.pow(2n, 32n) == m : Nat}, h: MNat.lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), m)) -> {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}:
607	  match a b:
608	    case U32{+x} U32{+y}:
609	      word_add_exact(32n, x, y, internal_bound(Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, y)), m, e, h))
610	
611	# U32 addition is exact without overflow: a + b < 2^32 implies to_nat (a + b) = a + b.
612	law u32_add_exact:
613	  for a: U32
614	  for b: U32
615	  for h: MNat.lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n))
616	  {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
617	
618	def u32_add_exact(a, b, h):
619	  internal_u32_add_exact(Nat.pow(2n, 32n), a, b, {==}, h)
620	
621	def internal_u32_add_wrap(-m: Nat, a: U32, b: U32, e: {Nat.pow(2n, 32n) == m : Nat}) -> {U32.to_nat(U32.add(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), m) : Nat}:
622	  match a b:
623	    case U32{+x} U32{+y}:
624	      %e : {Word.to_nat(32n, Word.add(32n, x, y)) == Nat.mod(Nat.add(Word.to_nat(32n, x), Word.to_nat(32n, y)), _) : Nat}
625	      word_add_wrap(32n, x, y)
626	
627	# U32 addition wraps modulo 2^32: to_nat (a + b) = (a + b) % 2^32.
628	law u32_add_wrap:
629	  for a: U32
630	  for b: U32
631	  {U32.to_nat(U32.add(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)) : Nat}
632	
633	def u32_add_wrap(a, b):
634	  internal_u32_add_wrap(Nat.pow(2n, 32n), a, b, {==})
635	
636	# U32 subtraction is exact without underflow: b <= a implies to_nat (a - b) = a - b.
637	law u32_sub_exact:
638	  for a: U32
639	  for b: U32
640	  for h: MNat.le(U32.to_nat(b), U32.to_nat(a))
641	  {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}
642	
643	def u32_sub_exact(a, b, h):
644	  match a b:
645	    case U32{x} U32{y}:
646	      word_sub_exact(32n, x, y, h)
647	
648	def internal_u32_sub_wrap(-m: Nat, a: U32, b: U32, e: {Nat.pow(2n, 32n) == m : Nat}) -> {U32.to_nat(U32.sub(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), Nat.sub(m, U32.to_nat(b))), m) : Nat}:
649	  match a b:
650	    case U32{+x} U32{+y}:
651	      %e : {Word.to_nat(32n, Word.sub(32n, x, y)) == Nat.mod(Nat.add(Word.to_nat(32n, x), Nat.sub(_, Word.to_nat(32n, y))), _) : Nat}
652	      word_sub_wrap(32n, x, y)
653	
654	# U32 subtraction wraps modulo 2^32: to_nat (a - b) = (a + (2^32 - b)) % 2^32.
655	law u32_sub_wrap:
656	  for a: U32
657	  for b: U32
658	  {U32.to_nat(U32.sub(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), Nat.sub(Nat.pow(2n, 32n), U32.to_nat(b))), Nat.pow(2n, 32n)) : Nat}
659	
660	def u32_sub_wrap(a, b):
661	  internal_u32_sub_wrap(Nat.pow(2n, 32n), a, b, {==})
662	
663	def internal_u32_inc_exact(-m: Nat, a: U32, e: {Nat.pow(2n, 32n) == m : Nat}, h: MNat.lt(1n+U32.to_nat(a), m)) -> {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}:
664	  match a:
665	    case U32{+w}:
666	      word_inc_exact(32n, w, internal_bound(1n+Word.to_nat(32n, w), m, e, h))
667	
668	# U32 increment is exact without overflow: 1 + a < 2^32 implies to_nat (inc a) = 1 + a.
669	law u32_inc_exact:
670	  for a: U32
671	  for h: MNat.lt(1n+U32.to_nat(a), Nat.pow(2n, 32n))
672	  {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}
673	
674	def u32_inc_exact(a, h):
675	  internal_u32_inc_exact(Nat.pow(2n, 32n), a, {==}, h)
676	
677	def internal_u32_inc_wrap(-m: Nat, a: U32, e: {Nat.pow(2n, 32n) == m : Nat}) -> {U32.to_nat(U32.inc(a)) == Nat.mod(1n+U32.to_nat(a), m) : Nat}:
678	  match a:
679	    case U32{+w}:
680	      %e : {Word.to_nat(32n, Word.inc(32n, w)) == Nat.mod(1n+Word.to_nat(32n, w), _) : Nat}
681	      word_inc_wrap(32n, w)
682	
683	# U32 increment wraps modulo 2^32: to_nat (inc a) = (1 + a) % 2^32.
684	law u32_inc_wrap:
685	  for a: U32
686	  {U32.to_nat(U32.inc(a)) == Nat.mod(1n+U32.to_nat(a), Nat.pow(2n, 32n)) : Nat}
687	
688	def u32_inc_wrap(a):
689	  internal_u32_inc_wrap(Nat.pow(2n, 32n), a, {==})
690	
691	def internal_u32_to_nat_from_nat(+m: Nat, +e: {Nat.pow(2n, 32n) == m : Nat}, k: Nat, h: MNat.lt(k, m)) -> {U32.to_nat(U32.from_nat(k)) == k : Nat}:
692	  match k:
693	    case 0n:
694	      {==}
695	    case 1n++p:
696	      +h = h
697	      +ih = internal_u32_to_nat_from_nat(m, e, p, MNat.lt_trans(p, 1n+p, m, MNat.lt_succ_self(p), h))
698	      +hu = internal_lt_congl(1n+p, 1n+U32.to_nat(U32.from_nat(p)), m, Equal.cong(Nat, Nat, z => 1n+z, p, U32.to_nat(U32.from_nat(p)), Equal.sym(Nat, U32.to_nat(U32.from_nat(p)), p, ih)), h)
699	      Equal.trans(Nat, U32.to_nat(U32.inc(U32.from_nat(p))), 1n+U32.to_nat(U32.from_nat(p)), 1n+p, internal_u32_inc_exact(m, U32.from_nat(p), e, hu), Equal.cong(Nat, Nat, z => 1n+z, U32.to_nat(U32.from_nat(p)), p, ih))
700	
701	# Converting a natural below 2^32 to U32 and back is the identity: k < 2^32 implies to_nat (from_nat k) = k.
702	law u32_to_nat_from_nat:
703	  for k: Nat
704	  for h: MNat.lt(k, Nat.pow(2n, 32n))
705	  {U32.to_nat(U32.from_nat(k)) == k : Nat}
706	
707	def u32_to_nat_from_nat(k, h):
708	  internal_u32_to_nat_from_nat(Nat.pow(2n, 32n), {==}, k, h)
709	
710	# Converting a U32 to a natural and back is the identity: from_nat (to_nat a) = a.
711	law u32_from_nat_to_nat:
712	  for a: U32
713	  {U32.from_nat(U32.to_nat(a)) == a : U32}
714	
715	def u32_from_nat_to_nat(a):
716	  +a = a
717	  u32_to_nat_inj(U32.from_nat(U32.to_nat(a)), a, u32_to_nat_from_nat(U32.to_nat(a), u32_to_nat_lt(a)))
718	
719	def internal_mod_succ_mod(+p: Nat, +m: Nat) -> {Nat.mod(1n+Nat.mod(p, m), m) == Nat.mod(1n+p, m) : Nat}:
720	  %MNat.mod_add_div(p, m) : {Nat.mod(1n+Nat.mod(p, m), m) == Nat.mod(1n+_, m) : Nat}
721	  Equal.sym(Nat, Nat.mod(Nat.add(1n+Nat.mod(p, m), Nat.mul(m, Nat.div(p, m))), m), Nat.mod(1n+Nat.mod(p, m), m), MNat.add_mul_mod_self_left(1n+Nat.mod(p, m), m, Nat.div(p, m)))
722	
723	def internal_u32_to_nat_from_nat_mod(+m: Nat, +e: {Nat.pow(2n, 32n) == m : Nat}, k: Nat) -> {U32.to_nat(U32.from_nat(k)) == Nat.mod(k, m) : Nat}:
724	  match k:
725	    case 0n:
726	      Equal.sym(Nat, Nat.mod(0n, m), 0n, MNat.zero_mod(m))
727	    case 1n++p:
728	      -u = U32.from_nat(p)
729	      Equal.trans(Nat, U32.to_nat(U32.inc(u)), Nat.mod(1n+U32.to_nat(u), m), Nat.mod(1n+p, m), internal_u32_inc_wrap(m, U32.from_nat(p), e), Equal.trans(Nat, Nat.mod(1n+U32.to_nat(u), m), Nat.mod(1n+Nat.mod(p, m), m), Nat.mod(1n+p, m), Equal.cong(Nat, Nat, z => Nat.mod(1n+z, m), U32.to_nat(u), Nat.mod(p, m), internal_u32_to_nat_from_nat_mod(m, e, p)), internal_mod_succ_mod(p, m)))
730	
731	# Converting any natural to U32 and back reduces it modulo 2^32: to_nat (from_nat k) = k % 2^32.
732	law u32_to_nat_from_nat_mod:
733	  for k: Nat
734	  {U32.to_nat(U32.from_nat(k)) == Nat.mod(k, Nat.pow(2n, 32n)) : Nat}
735	
736	def u32_to_nat_from_nat_mod(k):
737	  internal_u32_to_nat_from_nat_mod(Nat.pow(2n, 32n), {==}, k)
738	
739	def internal_min_fin(+u: U32, +v: U32, c: Bool, e: {Nat.is_lt(U32.to_nat(u), U32.to_nat(v)) == c : Bool}) -> {U32.to_nat(Bool.pick(U32, c, u, v)) == Nat.min(U32.to_nat(u), U32.to_nat(v)) : Nat}:
740	  match c:
741	    case True{}:
742	      Equal.sym(Nat, Nat.min(U32.to_nat(u), U32.to_nat(v)), U32.to_nat(u), MNat.min_eq_left(U32.to_nat(u), U32.to_nat(v), MNat.le_of_lt(U32.to_nat(u), U32.to_nat(v), e)))
743	    case False{}:
744	      Equal.sym(Nat, Nat.min(U32.to_nat(u), U32.to_nat(v)), U32.to_nat(v), MNat.min_eq_right(U32.to_nat(u), U32.to_nat(v), MNat.le_of_not_lt(U32.to_nat(u), U32.to_nat(v), e)))
745	
746	# The U32 minimum is the minimum of the values: to_nat (min a b) = min (to_nat a) (to_nat b).
747	law u32_min_to_nat:
748	  for a: U32
749	  for b: U32
750	  {U32.to_nat(U32.min(a, b)) == Nat.min(U32.to_nat(a), U32.to_nat(b)) : Nat}
751	
752	def u32_min_to_nat(a, b):
753	  match a b:
754	    case U32{+x} U32{+y}:
755	      internal_min_fin(U32{x}, U32{y}, U32.is_lt(U32{x}, U32{y}), Equal.sym(Bool, U32.is_lt(U32{x}, U32{y}), Nat.is_lt(U32.to_nat(U32{x}), U32.to_nat(U32{y})), u32_is_lt_to_nat(U32{x}, U32{y})))
756	
757	def internal_max_fin(+u: U32, +v: U32, c: Bool, e: {Nat.is_lt(U32.to_nat(u), U32.to_nat(v)) == c : Bool}) -> {U32.to_nat(Bool.pick(U32, c, v, u)) == Nat.max(U32.to_nat(u), U32.to_nat(v)) : Nat}:
758	  match c:
759	    case True{}:
760	      Equal.sym(Nat, Nat.max(U32.to_nat(u), U32.to_nat(v)), U32.to_nat(v), MNat.max_eq_right(U32.to_nat(u), U32.to_nat(v), MNat.le_of_lt(U32.to_nat(u), U32.to_nat(v), e)))
761	    case False{}:
762	      Equal.sym(Nat, Nat.max(U32.to_nat(u), U32.to_nat(v)), U32.to_nat(u), MNat.max_eq_left(U32.to_nat(u), U32.to_nat(v), MNat.le_of_not_lt(U32.to_nat(u), U32.to_nat(v), e)))
763	
764	# The U32 maximum is the maximum of the values: to_nat (max a b) = max (to_nat a) (to_nat b).
765	law u32_max_to_nat:
766	  for a: U32
767	  for b: U32
768	  {U32.to_nat(U32.max(a, b)) == Nat.max(U32.to_nat(a), U32.to_nat(b)) : Nat}
769	
770	def u32_max_to_nat(a, b):
771	  match a b:
772	    case U32{+x} U32{+y}:
773	      internal_max_fin(U32{x}, U32{y}, U32.is_lt(U32{x}, U32{y}), Equal.sym(Bool, U32.is_lt(U32{x}, U32{y}), Nat.is_lt(U32.to_nat(U32{x}), U32.to_nat(U32{y})), u32_is_lt_to_nat(U32{x}, U32{y})))
774	
775	def internal_shl_val(n: Nat, md: Nat, ts: Bool & Word(n)) -> Nat:
776	  match ts:
777	    case (t, s):
778	      Nat.add(Word.to_nat(n, s), Bool.pick(Nat, t, md, 0n))
779	
780	def internal_shl_con(+p: Nat, +c: Bool, r: Bool & Word(p), -x: Nat, ih: {internal_shl_val(p, Nat.pow(2n, p), r) == x : Nat}) -> {internal_shl_val(1n+p, Nat.pow(2n, 1n+p), Word.shl.out.con(p, c, r)) == Nat.add(internal_bv(c), Nat.double(x)) : Nat}:
781	  match r:
782	    case (+hi, +t2):
783	      +u = Word.to_nat(p, t2)
784	      +v = Bool.pick(Nat, hi, Nat.pow(2n, p), 0n)
785	      %ih : {Nat.add(Word.to_nat(1n+p, WCon{c, t2}), Bool.pick(Nat, hi, Nat.pow(2n, 1n+p), 0n)) == Nat.add(internal_bv(c), Nat.double(_)) : Nat}
786	      %MNat.double_add_sym(u, v) : {Nat.add(Word.to_nat(1n+p, WCon{c, t2}), Bool.pick(Nat, hi, Nat.pow(2n, 1n+p), 0n)) == Nat.add(internal_bv(c), _) : Nat}
787	      %internal_pick_pow(hi, p) : {Nat.add(Word.to_nat(1n+p, WCon{c, t2}), _) == Nat.add(internal_bv(c), Nat.add(Nat.double(u), Nat.double(v))) : Nat}
788	      %internal_to_nat_con(p, c, t2) : {Nat.add(_, Nat.double(v)) == Nat.add(internal_bv(c), Nat.add(Nat.double(u), Nat.double(v))) : Nat}
789	      MNat.add_assoc(internal_bv(c), Nat.double(u), Nat.double(v))
790	
791	def internal_shl_out(n: Nat, c: Bool, w: Word(n)) -> {internal_shl_val(n, Nat.pow(2n, n), Word.shl.out(n, c, w)) == Nat.add(internal_bv(c), Nat.double(Word.to_nat(n, w))) : Nat}:
792	  match n:
793	    case 0n:
794	      match c:
795	        case False{}:
796	          match w:
797	            case WNil{}:
798	              {==}
799	        case True{}:
800	          match w:
801	            case WNil{}:
802	              {==}
803	    case 1n++p:
804	      match w:
805	        case WCon{+b, +t}:
806	          %internal_to_nat_con(p, b, t) : {internal_shl_val(1n+p, Nat.pow(2n, 1n+p), Word.shl.out(1n+p, c, WCon{b, t})) == Nat.add(internal_bv(c), Nat.double(_)) : Nat}
807	          internal_shl_con(p, c, Word.shl.out(p, b, t), Nat.add(internal_bv(b), Nat.double(Word.to_nat(p, t))), internal_shl_out(p, b, t))
808	
809	def internal_shl_out32(-md: Nat, em: {Nat.pow(2n, 32n) == md : Nat}, x: Bool, rw: Word(32n)) -> {internal_shl_val(32n, md, Word.shl.out(32n, x, rw)) == Nat.add(internal_bv(x), Nat.double(Word.to_nat(32n, rw))) : Nat}:
810	  %em : {internal_shl_val(32n, _, Word.shl.out(32n, x, rw)) == Nat.add(internal_bv(x), Nat.double(Word.to_nat(32n, rw))) : Nat}
811	  internal_shl_out(32n, x, rw)
812	
813	def internal_div_step(+k: Nat, +q: Nat, +b: Nat, +r2: Nat, +x: Nat, +r: Nat, -a: Nat, ek: {Nat.add(Nat.mul(k, b), r2) == Nat.add(x, Nat.double(r)) : Nat}, ea: {Nat.add(Nat.mul(q, b), r) == a : Nat}) -> {Nat.add(Nat.mul(Nat.add(k, Nat.double(q)), b), r2) == Nat.add(x, Nat.double(a)) : Nat}:
814	  -l = Nat.add(Nat.mul(Nat.add(k, Nat.double(q)), b), r2)
815	  %ea : {l == Nat.add(x, Nat.double(_)) : Nat}
816	  %MNat.double_add_sym(Nat.mul(q, b), r) : {l == Nat.add(x, _) : Nat}
817	  %MNat.double_mul_sym(q, b) : {l == Nat.add(x, Nat.add(_, Nat.double(r))) : Nat}
818	  %MNat.add_mul_sym(k, Nat.double(q), b) : {Nat.add(_, r2) == Nat.add(x, Nat.add(Nat.mul(Nat.double(q), b), Nat.double(r))) : Nat}
819	  %MNat.add_left_comm(Nat.mul(Nat.double(q), b), x, Nat.double(r)) : {Nat.add(Nat.add(Nat.mul(k, b), Nat.mul(Nat.double(q), b)), r2) == _ : Nat}
820	  %ek : {Nat.add(Nat.add(Nat.mul(k, b), Nat.mul(Nat.double(q), b)), r2) == Nat.add(Nat.mul(Nat.double(q), b), _) : Nat}
821	  %MNat.add_left_comm(Nat.mul(k, b), Nat.mul(Nat.double(q), b), r2) : {Nat.add(Nat.add(Nat.mul(k, b), Nat.mul(Nat.double(q), b)), r2) == _ : Nat}
822	  MNat.add_assoc(Nat.mul(k, b), Nat.mul(Nat.double(q), b), r2)
823	
824	def internal_bit_double_lt(x: Bool, +r: Nat, +b: Nat, h: MNat.lt(r, b)) -> MNat.lt(Nat.add(internal_bv(x), Nat.double(r)), Nat.double(b)):
825	  match x:
826	    case False{}:
827	      MNat.double_lt_double(r, b, h)
828	    case True{}:
829	      %Equal.sym(Bool, Nat.is_lt(1n+Nat.double(r), Nat.double(b)), Nat.is_le(2n+Nat.double(r), Nat.double(b)), MNat.is_lt_eq_succ_le(1n+Nat.double(r), Nat.double(b))) : {_ == True{} : Bool}
830	      MNat.double_le_double(1n+r, b, MNat.succ_le_of_lt(r, b, h))
831	
832	def internal_rem_lt_add(+b: Nat, +r2: Nat, -v: Nat, e: {Nat.add(b, r2) == v : Nat}, h: MNat.lt(v, Nat.double(b))) -> MNat.lt(Nat.add(b, r2), Nat.add(b, b)):
833	  %Equal.sym(Nat, Nat.add(b, r2), v, e) : MNat.lt(_, Nat.add(b, b))
834	  %MNat.double_eq_add(b) : MNat.lt(v, _)
835	  h
836	
837	def internal_rem_lt(+b: Nat, +r2: Nat, -v: Nat, e: {Nat.add(b, r2) == v : Nat}, h: MNat.lt(v, Nat.double(b))) -> MNat.lt(r2, b):
838	  MNat.lt_of_add_lt_add_left(b, r2, b, internal_rem_lt_add(b, r2, v, e, h))
839	
840	def internal_wrap_sum(+b: Nat, +s: Nat, +m: Nat, -v: Nat, hb: MNat.lt(b, m), es: {Nat.add(s, m) == v : Nat}) -> {Nat.add(b, Nat.add(s, Nat.sub(m, b))) == v : Nat}:
841	  %MNat.add_left_comm(s, b, Nat.sub(m, b)) : {_ == v : Nat}
842	  %Equal.sym(Nat, Nat.add(b, Nat.sub(m, b)), m, MNat.add_sub_of_le(b, m, MNat.le_of_lt(b, m, hb))) : {Nat.add(s, _) == v : Nat}
843	  es
844	
845	def internal_wrap_rem(+b: Nat, +s: Nat, +m: Nat, +v: Nat, +hb: MNat.lt(b, m), es: {Nat.add(s, m) == v : Nat}, hv: MNat.lt(v, Nat.double(b))) -> {Nat.add(b, Nat.mod(Nat.add(s, Nat.sub(m, b)), m)) == v : Nat}:
846	  +y = Nat.add(s, Nat.sub(m, b))
847	  +ey = internal_wrap_sum(b, s, m, v, hb, es)
848	  +hy = internal_rem_lt(b, y, v, ey, hv)
849	  %Equal.sym(Nat, Nat.mod(y, m), y, MNat.mod_eq_of_lt(y, m, MNat.lt_trans(y, b, m, hy, hb))) : {Nat.add(b, _) == v : Nat}
850	  ey
851	
852	def internal_dm_inv(m: Nat, b: Nat, a: Nat, qr: Word(m) & U32) -> Type:
853	  match qr:
854	    case (q, r):
855	      {Nat.add(Nat.mul(Word.to_nat(m, q), b), U32.to_nat(r)) == a : Nat} & MNat.lt(U32.to_nat(r), b)
856	
857	def internal_dm_take(+p: Nat, +q: Word(p), +b: Nat, +r2: Nat, +x: Bool, +r: Nat, -a: Nat, ea: {Nat.add(Nat.mul(Word.to_nat(p, q), b), r) == a : Nat}, hr: MNat.lt(r, b), +e2: {Nat.add(b, r2) == Nat.add(internal_bv(x), Nat.double(r)) : Nat}) -> {Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), b), r2) == Nat.add(internal_bv(x), Nat.double(a)) : Nat} & MNat.lt(r2, b):
858	  +ek = Equal.trans(Nat, Nat.add(Nat.mul(1n, b), r2), Nat.add(b, r2), Nat.add(internal_bv(x), Nat.double(r)), Equal.cong(Nat, Nat, z => Nat.add(z, r2), Nat.mul(1n, b), b, MNat.one_mul(b)), e2)
859	  (internal_div_step(1n, Word.to_nat(p, q), b, r2, internal_bv(x), r, a, ek, ea), internal_rem_lt(b, r2, Nat.add(internal_bv(x), Nat.double(r)), e2, internal_bit_double_lt(x, r, b, hr)))
860	
861	def internal_dm_wrap(+b: U32, +s: Word(32n), +x: Bool, +r: Nat, +m: Nat, +em: {Nat.pow(2n, 32n) == m : Nat}, hr: MNat.lt(r, U32.to_nat(b)), es: {Nat.add(Word.to_nat(32n, s), m) == Nat.add(internal_bv(x), Nat.double(r)) : Nat}) -> {Nat.add(U32.to_nat(b), U32.to_nat(U32.sub(U32{s}, b))) == Nat.add(internal_bv(x), Nat.double(r)) : Nat}:
862	  +bn = U32.to_nat(b)
863	  +sn = Word.to_nat(32n, s)
864	  +v = Nat.add(internal_bv(x), Nat.double(r))
865	  %Equal.sym(Nat, U32.to_nat(U32.sub(U32{s}, b)), Nat.mod(Nat.add(sn, Nat.sub(m, bn)), m), internal_u32_sub_wrap(m, U32{s}, b, em)) : {Nat.add(bn, _) == v : Nat}
866	  internal_wrap_rem(bn, sn, m, v, internal_u32_to_nat_lt(m, b, em), es, internal_bit_double_lt(x, r, bn, hr))
867	
868	def internal_dm_fin(+p: Nat, +q: Word(p), +s: Word(32n), +b: U32, +x: Bool, +r: Nat, -a: Nat, +m: Nat, +em: {Nat.pow(2n, 32n) == m : Nat}, t: Bool, g: Bool, ea: {Nat.add(Nat.mul(Word.to_nat(p, q), U32.to_nat(b)), r) == a : Nat}, +hr: MNat.lt(r, U32.to_nat(b)), es: {Nat.add(Word.to_nat(32n, s), Bool.pick(Nat, t, m, 0n)) == Nat.add(internal_bv(x), Nat.double(r)) : Nat}, eg: {Bool.or(t, U32.is_ge(U32{s}, b)) == g : Bool}) -> internal_dm_inv(1n+p, U32.to_nat(b), Nat.add(internal_bv(x), Nat.double(a)), U32.divmod.go.fin(p, q, U32{s}, b, g)):
869	  match t g:
870	    case True{} True{}:
871	      internal_dm_take(p, q, U32.to_nat(b), U32.to_nat(U32.sub(U32{s}, b)), x, r, a, ea, hr, internal_dm_wrap(b, s, x, r, m, em, hr, es))
872	    case True{} False{}:
873	      Empty.absurd(internal_dm_inv(1n+p, U32.to_nat(b), Nat.add(internal_bv(x), Nat.double(a)), U32.divmod.go.fin(p, q, U32{s}, b, False{})), MNat.internal_div_true_ne_false(eg))
874	    case False{} True{}:
875	      +bn = U32.to_nat(b)
876	      +sn = Word.to_nat(32n, s)
877	      +hle = Equal.trans(Bool, Nat.is_le(bn, sn), U32.is_ge(U32{s}, b), True{}, Equal.trans(Bool, Nat.is_le(bn, sn), Nat.is_ge(sn, bn), U32.is_ge(U32{s}, b), MNat.is_ge_eq_is_le_sym(sn, bn), Equal.sym(Bool, U32.is_ge(U32{s}, b), Nat.is_ge(sn, bn), u32_is_ge_to_nat(U32{s}, b))), eg)
878	      +e2 = Equal.trans(Nat, Nat.add(bn, U32.to_nat(U32.sub(U32{s}, b))), Nat.add(bn, Nat.sub(sn, bn)), Nat.add(internal_bv(x), Nat.double(r)), Equal.cong(Nat, Nat, z => Nat.add(bn, z), U32.to_nat(U32.sub(U32{s}, b)), Nat.sub(sn, bn), u32_sub_exact(U32{s}, b, hle)), Equal.trans(Nat, Nat.add(bn, Nat.sub(sn, bn)), sn, Nat.add(internal_bv(x), Nat.double(r)), MNat.add_sub_of_le(bn, sn, hle), Equal.trans(Nat, sn, Nat.add(sn, 0n), Nat.add(internal_bv(x), Nat.double(r)), MNat.add_zero_sym(sn), es)))
879	      internal_dm_take(p, q, bn, U32.to_nat(U32.sub(U32{s}, b)), x, r, a, ea, hr, e2)
880	    case False{} False{}:
881	      +bn = U32.to_nat(b)
882	      +sn = Word.to_nat(32n, s)
883	      +hnle = Equal.trans(Bool, Nat.is_le(bn, sn), U32.is_ge(U32{s}, b), False{}, Equal.trans(Bool, Nat.is_le(bn, sn), Nat.is_ge(sn, bn), U32.is_ge(U32{s}, b), MNat.is_ge_eq_is_le_sym(sn, bn), Equal.sym(Bool, U32.is_ge(U32{s}, b), Nat.is_ge(sn, bn), u32_is_ge_to_nat(U32{s}, b))), eg)
884	      +ek = Equal.trans(Nat, sn, Nat.add(sn, 0n), Nat.add(internal_bv(x), Nat.double(r)), MNat.add_zero_sym(sn), es)
885	      (internal_div_step(0n, Word.to_nat(p, q), bn, sn, internal_bv(x), r, a, ek, ea), MNat.lt_of_not_le(bn, sn, hnle))
886	
887	def internal_dm_shl(+p: Nat, +q: Word(p), +b: U32, +x: Bool, +r: Nat, -a: Nat, ea: {Nat.add(Nat.mul(Word.to_nat(p, q), U32.to_nat(b)), r) == a : Nat}, +hr: MNat.lt(r, U32.to_nat(b)), +md: Nat, +em: {Nat.pow(2n, 32n) == md : Nat}, ts: Bool & Word(32n), es: {internal_shl_val(32n, md, ts) == Nat.add(internal_bv(x), Nat.double(r)) : Nat}) -> internal_dm_inv(1n+p, U32.to_nat(b), Nat.add(internal_bv(x), Nat.double(a)), U32.divmod.go.shl(p, q, b, ts)):
888	  match ts:
889	    case (+t, +s):
890	      internal_dm_fin(p, q, s, b, x, r, a, md, em, t, Bool.or(t, U32.is_ge(U32{s}, b)), ea, hr, es, {==})
891	
892	def internal_dm_rec(+p: Nat, +x: Bool, +b: U32, +md: Nat, +em: {Nat.pow(2n, 32n) == md : Nat}, -a: Nat, qr: Word(p) & U32, ih: internal_dm_inv(p, U32.to_nat(b), a, qr)) -> internal_dm_inv(1n+p, U32.to_nat(b), Nat.add(internal_bv(x), Nat.double(a)), U32.divmod.go.rec(p, x, b, qr)):
893	  match qr:
894	    case (+q, r):
895	      match r:
896	        case U32{+rw}:
897	          match ih:
898	            case (ea, +hr):
899	              internal_dm_shl(p, q, b, x, Word.to_nat(32n, rw), a, ea, hr, md, em, Word.shl.out(32n, x, rw), internal_shl_out32(md, em, x, rw))
900	
901	def internal_dm_go(m: Nat, w: Word(m), +b: U32, +hb: MNat.lt(0n, U32.to_nat(b)), +md: Nat, +em: {Nat.pow(2n, 32n) == md : Nat}) -> internal_dm_inv(m, U32.to_nat(b), Word.to_nat(m, w), U32.divmod.go(m, w, b)):
902	  match m:
903	    case 0n:
904	      match w:
905	        case WNil{}:
906	          ({==}, hb)
907	    case 1n++p:
908	      match w:
909	        case WCon{+x, +hi}:
910	          %internal_to_nat_con(p, x, hi) : internal_dm_inv(1n+p, U32.to_nat(b), _, U32.divmod.go(1n+p, WCon{x, hi}, b))
911	          internal_dm_rec(p, x, b, md, em, Word.to_nat(p, hi), U32.divmod.go(p, hi, b), internal_dm_go(p, hi, b, hb, md, em))
912	
913	def internal_div_unique(+q: Nat, b: Nat, +r: Nat, -a: Nat, hb: MNat.lt(0n, b), e: {Nat.add(Nat.mul(q, b), r) == a : Nat}, h: MNat.lt(r, b)) -> {q == Nat.div(a, b) : Nat}:
914	  match b:
915	    case 0n:
916	      Empty.absurd({q == Nat.div(a, 0n) : Nat}, MNat.internal_false_ne_true(hb))
917	    case 1n++bp:
918	      %e : {q == Nat.div(_, 1n+bp) : Nat}
919	      %MNat.add_comm(r, Nat.mul(q, 1n+bp)) : {q == Nat.div(_, 1n+bp) : Nat}
920	      %MNat.add_mul_div_right_sym(r, q, bp) : {q == _ : Nat}
921	      %Equal.sym(Nat, Nat.div(r, 1n+bp), 0n, MNat.div_eq_zero_of_le(r, bp, MNat.le_of_lt_succ(r, bp, h))) : {q == Nat.add(_, q) : Nat}
922	      {==}
923	
924	def internal_div_fin(+b: U32, -a: Nat, hb: MNat.lt(0n, U32.to_nat(b)), qr: Word(32n) & U32, inv: internal_dm_inv(32n, U32.to_nat(b), a, qr)) -> {U32.to_nat(U32.div.fin(qr)) == Nat.div(a, U32.to_nat(b)) : Nat}:
925	  match qr:
926	    case (q, r):
927	      match inv:
928	        case (e, h):
929	          internal_div_unique(Word.to_nat(32n, q), U32.to_nat(b), U32.to_nat(r), a, hb, e, h)
930	
931	def internal_div_if(+md: Nat, +em: {Nat.pow(2n, 32n) == md : Nat}, +aw: Word(32n), +bw: Word(32n), z: Bool, ez: {U32.is_zero(U32{bw}) == z : Bool}) -> {U32.to_nat(U32.div.if(aw, U32{bw}, z)) == Nat.div(Word.to_nat(32n, aw), Word.to_nat(32n, bw)) : Nat}:
932	  match z:
933	    case True{}:
934	      +bn = Word.to_nat(32n, bw)
935	      +ee = Equal.trans(Bool, Nat.is_eq(bn, 0n), U32.is_zero(U32{bw}), True{}, Equal.sym(Bool, U32.is_zero(U32{bw}), Nat.is_eq(bn, 0n), u32_is_eq_to_nat(U32{bw}, 0)), ez)
936	      %Equal.sym(Nat, bn, 0n, MNat.eq_of_is_eq(bn, 0n, ee)) : {0n == Nat.div(Word.to_nat(32n, aw), _) : Nat}
937	      {==}
938	    case False{}:
939	      +bn = Word.to_nat(32n, bw)
940	      +ee = Equal.trans(Bool, Nat.is_eq(bn, 0n), U32.is_zero(U32{bw}), False{}, Equal.sym(Bool, U32.is_zero(U32{bw}), Nat.is_eq(bn, 0n), u32_is_eq_to_nat(U32{bw}, 0)), ez)
941	      +hb = MNat.pos_of_ne_zero(bn, ee)
942	      internal_div_fin(U32{bw}, Word.to_nat(32n, aw), hb, U32.divmod.go(32n, aw, U32{bw}), internal_dm_go(32n, aw, U32{bw}, hb, md, em))
943	
944	# U32 division is the division of the values, also for a zero divisor: to_nat (a / b) = to_nat a / to_nat b.
945	law u32_div_to_nat:
946	  for a: U32
947	  for b: U32
948	  {U32.to_nat(U32.div(a, b)) == Nat.div(U32.to_nat(a), U32.to_nat(b)) : Nat}
949	
950	def u32_div_to_nat(a, b):
951	  match a b:
952	    case U32{aw} U32{+bw}:
953	      internal_div_if(Nat.pow(2n, 32n), {==}, aw, bw, U32.is_zero(U32{bw}), {==})
954	
955	# U32 division is antitone in a positive divisor: 0 < s and s <= t imply a / t <= a / s.
956	law u32_div_le_div_left:
957	  for a: U32
958	  for s: U32
959	  for t: U32
960	  for hs: {U32.is_lt(0, s) == True{} : Bool}
961	  for h: {U32.is_le(s, t) == True{} : Bool}
962	  {U32.is_le(U32.div(a, t), U32.div(a, s)) == True{} : Bool}
963	
964	def u32_div_le_div_left(a, s, t, hs, h):
965	  +a = a
966	  +s = s
967	  +t = t
968	  %Equal.sym(Bool, U32.is_le(U32.div(a, t), U32.div(a, s)), Nat.is_le(U32.to_nat(U32.div(a, t)), U32.to_nat(U32.div(a, s))), u32_is_le_to_nat(U32.div(a, t), U32.div(a, s))) : {_ == True{} : Bool}
969	  %Equal.sym(Nat, U32.to_nat(U32.div(a, t)), Nat.div(U32.to_nat(a), U32.to_nat(t)), u32_div_to_nat(a, t)) : {Nat.is_le(_, U32.to_nat(U32.div(a, s))) == True{} : Bool}
970	  %Equal.sym(Nat, U32.to_nat(U32.div(a, s)), Nat.div(U32.to_nat(a), U32.to_nat(s)), u32_div_to_nat(a, s)) : {Nat.is_le(Nat.div(U32.to_nat(a), U32.to_nat(t)), _) == True{} : Bool}
971	  +hs2 = Equal.trans(Bool, Nat.is_lt(U32.to_nat(0), U32.to_nat(s)), U32.is_lt(0, s), True{}, Equal.sym(Bool, U32.is_lt(0, s), Nat.is_lt(U32.to_nat(0), U32.to_nat(s)), u32_is_lt_to_nat(0, s)), hs)
972	  +h2 = Equal.trans(Bool, Nat.is_le(U32.to_nat(s), U32.to_nat(t)), U32.is_le(s, t), True{}, Equal.sym(Bool, U32.is_le(s, t), Nat.is_le(U32.to_nat(s), U32.to_nat(t)), u32_is_le_to_nat(s, t)), h)
973	  MNat.div_le_div_left(U32.to_nat(a), U32.to_nat(s), U32.to_nat(t), hs2, h2)
974	
975	# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
976	
977	# The zero word is the natural zero: to_nat (zero n) = 0, reversed to rewrite toward the simple side.
978	law word_to_nat_zero_sym:
979	  for n: Nat
980	  {0n == Word.to_nat(n, Word.zero(n)) : Nat}
981	
982	def word_to_nat_zero_sym(n):
983	  Equal.sym(Nat, Word.to_nat(n, Word.zero(n)), 0n, word_to_nat_zero(n))
984	
985	# Comparing words compares their values: cmp a b = cmp (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
986	law word_cmp_to_nat_sym:
987	  for n: Nat
988	  for a: Word(n)
989	  for b: Word(n)
990	  {Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.cmp(n, a, b) : Cmp}
991	
992	def word_cmp_to_nat_sym(n, a, b):
993	  Equal.sym(Cmp, Word.cmp(n, a, b), Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)), word_cmp_to_nat(n, a, b))
994	
995	# One plus a word plus its complement is two to the width: 1 + to_nat (not w) + to_nat w = 2^n, reversed to rewrite toward the simple side.
996	law word_not_add_sym:
997	  for n: Nat
998	  for w: Word(n)
999	  {Nat.pow(2n, n) == 1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) : Nat}
1000	
1001	def word_not_add_sym(n, w):
1002	  Equal.sym(Nat, 1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)), Nat.pow(2n, n), word_not_add(n, w))
1003	
1004	# The adder is exact below the overflow: a + b + carry-in < 2^n implies to_nat (adc a b False c) = a + b + carry-in, reversed to rewrite toward the simple side.
1005	law word_adc_exact_sym:
1006	  for n: Nat
1007	  for a: Word(n)
1008	  for b: Word(n)
1009	  for c: Bool
1010	  for h: MNat.lt(Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n))
1011	  {Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)) == Word.to_nat(n, Word.adc(n, a, b, False{}, c)) : Nat}
1012	
1013	def word_adc_exact_sym(n, a, b, c, h):
1014	  Equal.sym(Nat, Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), word_adc_exact(n, a, b, c, h))
1015	
1016	# The adder drops exactly one 2^n on overflow: 2^n <= a + b + carry-in implies to_nat (adc a b False c) + 2^n = a + b + carry-in, reversed to rewrite toward the simple side.
1017	law word_adc_overflow_sym:
1018	  for n: Nat
1019	  for a: Word(n)
1020	  for b: Word(n)
1021	  for c: Bool
1022	  for h: MNat.le(Nat.pow(2n, n), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)))
1023	  {Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)) == Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.pow(2n, n)) : Nat}
1024	
1025	def word_adc_overflow_sym(n, a, b, c, h):
1026	  Equal.sym(Nat, Nat.add(Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.pow(2n, n)), Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), word_adc_overflow(n, a, b, c, h))
1027	
1028	# The adder wraps modulo 2^n: to_nat (adc a b False c) = (a + b + carry-in) % 2^n, reversed to rewrite toward the simple side.
1029	law word_adc_wrap_sym:
1030	  for n: Nat
1031	  for a: Word(n)
1032	  for b: Word(n)
1033	  for c: Bool
1034	  {Nat.mod(Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n)) == Word.to_nat(n, Word.adc(n, a, b, False{}, c)) : Nat}
1035	
1036	def word_adc_wrap_sym(n, a, b, c):
1037	  Equal.sym(Nat, Word.to_nat(n, Word.adc(n, a, b, False{}, c)), Nat.mod(Nat.add(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Bool.pick(Nat, c, 1n, 0n)), Nat.pow(2n, n)), word_adc_wrap(n, a, b, c))
1038	
1039	# Word addition is exact without overflow: a + b < 2^n implies to_nat (add a b) = a + b, reversed to rewrite toward the simple side.
1040	law word_add_exact_sym:
1041	  for n: Nat
1042	  for a: Word(n)
1043	  for b: Word(n)
1044	  for h: MNat.lt(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n))
1045	  {Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.to_nat(n, Word.add(n, a, b)) : Nat}
1046	
1047	def word_add_exact_sym(n, a, b, h):
1048	  Equal.sym(Nat, Word.to_nat(n, Word.add(n, a, b)), Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), word_add_exact(n, a, b, h))
1049	
1050	# Word addition wraps modulo 2^n: to_nat (add a b) = (a + b) % 2^n, reversed to rewrite toward the simple side.
1051	law word_add_wrap_sym:
1052	  for n: Nat
1053	  for a: Word(n)
1054	  for b: Word(n)
1055	  {Nat.mod(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n)) == Word.to_nat(n, Word.add(n, a, b)) : Nat}
1056	
1057	def word_add_wrap_sym(n, a, b):
1058	  Equal.sym(Nat, 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)), word_add_wrap(n, a, b))
1059	
1060	# Increment is exact without overflow: 1 + w < 2^n implies to_nat (inc w) = 1 + w, reversed to rewrite toward the simple side.
1061	law word_inc_exact_sym:
1062	  for n: Nat
1063	  for w: Word(n)
1064	  for h: MNat.lt(1n+Word.to_nat(n, w), Nat.pow(2n, n))
1065	  {1n+Word.to_nat(n, w) == Word.to_nat(n, Word.inc(n, w)) : Nat}
1066	
1067	def word_inc_exact_sym(n, w, h):
1068	  Equal.sym(Nat, Word.to_nat(n, Word.inc(n, w)), 1n+Word.to_nat(n, w), word_inc_exact(n, w, h))
1069	
1070	# Increment wraps modulo 2^n: to_nat (inc w) = (1 + w) % 2^n, reversed to rewrite toward the simple side.
1071	law word_inc_wrap_sym:
1072	  for n: Nat
1073	  for w: Word(n)
1074	  {Nat.mod(1n+Word.to_nat(n, w), Nat.pow(2n, n)) == Word.to_nat(n, Word.inc(n, w)) : Nat}
1075	
1076	def word_inc_wrap_sym(n, w):
1077	  Equal.sym(Nat, Word.to_nat(n, Word.inc(n, w)), Nat.mod(1n+Word.to_nat(n, w), Nat.pow(2n, n)), word_inc_wrap(n, w))
1078	
1079	# Word subtraction is exact without underflow: b <= a implies to_nat (sub a b) = a - b, reversed to rewrite toward the simple side.
1080	law word_sub_exact_sym:
1081	  for n: Nat
1082	  for a: Word(n)
1083	  for b: Word(n)
1084	  for h: MNat.le(Word.to_nat(n, b), Word.to_nat(n, a))
1085	  {Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.to_nat(n, Word.sub(n, a, b)) : Nat}
1086	
1087	def word_sub_exact_sym(n, a, b, h):
1088	  Equal.sym(Nat, Word.to_nat(n, Word.sub(n, a, b)), Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)), word_sub_exact(n, a, b, h))
1089	
1090	# Word subtraction wraps modulo 2^n: to_nat (sub a b) = (a + (2^n - b)) % 2^n, reversed to rewrite toward the simple side.
1091	law word_sub_wrap_sym:
1092	  for n: Nat
1093	  for a: Word(n)
1094	  for b: Word(n)
1095	  {Nat.mod(Nat.add(Word.to_nat(n, a), Nat.sub(Nat.pow(2n, n), Word.to_nat(n, b))), Nat.pow(2n, n)) == Word.to_nat(n, Word.sub(n, a, b)) : Nat}
1096	
1097	def word_sub_wrap_sym(n, a, b):
1098	  Equal.sym(Nat, Word.to_nat(n, Word.sub(n, a, b)), Nat.mod(Nat.add(Word.to_nat(n, a), Nat.sub(Nat.pow(2n, n), Word.to_nat(n, b))), Nat.pow(2n, n)), word_sub_wrap(n, a, b))
1099	
1100	# Comparing U32s compares their values: cmp a b = cmp (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1101	law u32_cmp_to_nat_sym:
1102	  for a: U32
1103	  for b: U32
1104	  {Nat.cmp(U32.to_nat(a), U32.to_nat(b)) == U32.cmp(a, b) : Cmp}
1105	
1106	def u32_cmp_to_nat_sym(a, b):
1107	  Equal.sym(Cmp, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
1108	
1109	# U32 equality tests the values: is_eq a b = is_eq (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1110	law u32_is_eq_to_nat_sym:
1111	  for a: U32
1112	  for b: U32
1113	  {Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) == U32.is_eq(a, b) : Bool}
1114	
1115	def u32_is_eq_to_nat_sym(a, b):
1116	  Equal.sym(Bool, U32.is_eq(a, b), Nat.is_eq(U32.to_nat(a), U32.to_nat(b)), u32_is_eq_to_nat(a, b))
1117	
1118	# U32 disequality tests the values: is_ne a b = is_ne (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1119	law u32_is_ne_to_nat_sym:
1120	  for a: U32
1121	  for b: U32
1122	  {Nat.is_ne(U32.to_nat(a), U32.to_nat(b)) == U32.is_ne(a, b) : Bool}
1123	
1124	def u32_is_ne_to_nat_sym(a, b):
1125	  Equal.sym(Bool, U32.is_ne(a, b), Nat.is_ne(U32.to_nat(a), U32.to_nat(b)), u32_is_ne_to_nat(a, b))
1126	
1127	# The U32 strict order is the order of the values: is_lt a b = is_lt (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1128	law u32_is_lt_to_nat_sym:
1129	  for a: U32
1130	  for b: U32
1131	  {Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == U32.is_lt(a, b) : Bool}
1132	
1133	def u32_is_lt_to_nat_sym(a, b):
1134	  Equal.sym(Bool, U32.is_lt(a, b), Nat.is_lt(U32.to_nat(a), U32.to_nat(b)), u32_is_lt_to_nat(a, b))
1135	
1136	# The U32 order is the order of the values: is_le a b = is_le (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1137	law u32_is_le_to_nat_sym:
1138	  for a: U32
1139	  for b: U32
1140	  {Nat.is_le(U32.to_nat(a), U32.to_nat(b)) == U32.is_le(a, b) : Bool}
1141	
1142	def u32_is_le_to_nat_sym(a, b):
1143	  Equal.sym(Bool, U32.is_le(a, b), Nat.is_le(U32.to_nat(a), U32.to_nat(b)), u32_is_le_to_nat(a, b))
1144	
1145	# The reverse U32 strict order is that of the values: is_gt a b = is_gt (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1146	law u32_is_gt_to_nat_sym:
1147	  for a: U32
1148	  for b: U32
1149	  {Nat.is_gt(U32.to_nat(a), U32.to_nat(b)) == U32.is_gt(a, b) : Bool}
1150	
1151	def u32_is_gt_to_nat_sym(a, b):
1152	  Equal.sym(Bool, U32.is_gt(a, b), Nat.is_gt(U32.to_nat(a), U32.to_nat(b)), u32_is_gt_to_nat(a, b))
1153	
1154	# The reverse U32 order is that of the values: is_ge a b = is_ge (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1155	law u32_is_ge_to_nat_sym:
1156	  for a: U32
1157	  for b: U32
1158	  {Nat.is_ge(U32.to_nat(a), U32.to_nat(b)) == U32.is_ge(a, b) : Bool}
1159	
1160	def u32_is_ge_to_nat_sym(a, b):
1161	  Equal.sym(Bool, U32.is_ge(a, b), Nat.is_ge(U32.to_nat(a), U32.to_nat(b)), u32_is_ge_to_nat(a, b))
1162	
1163	# U32 addition is exact without overflow: a + b < 2^32 implies to_nat (a + b) = a + b, reversed to rewrite toward the simple side.
1164	law u32_add_exact_sym:
1165	  for a: U32
1166	  for b: U32
1167	  for h: MNat.lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n))
1168	  {Nat.add(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.add(a, b)) : Nat}
1169	
1170	def u32_add_exact_sym(a, b, h):
1171	  Equal.sym(Nat, U32.to_nat(U32.add(a, b)), Nat.add(U32.to_nat(a), U32.to_nat(b)), u32_add_exact(a, b, h))
1172	
1173	# U32 addition wraps modulo 2^32: to_nat (a + b) = (a + b) % 2^32, reversed to rewrite toward the simple side.
1174	law u32_add_wrap_sym:
1175	  for a: U32
1176	  for b: U32
1177	  {Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)) == U32.to_nat(U32.add(a, b)) : Nat}
1178	
1179	def u32_add_wrap_sym(a, b):
1180	  Equal.sym(Nat, U32.to_nat(U32.add(a, b)), Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)), u32_add_wrap(a, b))
1181	
1182	# U32 subtraction is exact without underflow: b <= a implies to_nat (a - b) = a - b, reversed to rewrite toward the simple side.
1183	law u32_sub_exact_sym:
1184	  for a: U32
1185	  for b: U32
1186	  for h: MNat.le(U32.to_nat(b), U32.to_nat(a))
1187	  {Nat.sub(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.sub(a, b)) : Nat}
1188	
1189	def u32_sub_exact_sym(a, b, h):
1190	  Equal.sym(Nat, U32.to_nat(U32.sub(a, b)), Nat.sub(U32.to_nat(a), U32.to_nat(b)), u32_sub_exact(a, b, h))
1191	
1192	# U32 subtraction wraps modulo 2^32: to_nat (a - b) = (a + (2^32 - b)) % 2^32, reversed to rewrite toward the simple side.
1193	law u32_sub_wrap_sym:
1194	  for a: U32
1195	  for b: U32
1196	  {Nat.mod(Nat.add(U32.to_nat(a), Nat.sub(Nat.pow(2n, 32n), U32.to_nat(b))), Nat.pow(2n, 32n)) == U32.to_nat(U32.sub(a, b)) : Nat}
1197	
1198	def u32_sub_wrap_sym(a, b):
1199	  Equal.sym(Nat, U32.to_nat(U32.sub(a, b)), Nat.mod(Nat.add(U32.to_nat(a), Nat.sub(Nat.pow(2n, 32n), U32.to_nat(b))), Nat.pow(2n, 32n)), u32_sub_wrap(a, b))
1200	
1201	# U32 increment is exact without overflow: 1 + a < 2^32 implies to_nat (inc a) = 1 + a, reversed to rewrite toward the simple side.
1202	law u32_inc_exact_sym:
1203	  for a: U32
1204	  for h: MNat.lt(1n+U32.to_nat(a), Nat.pow(2n, 32n))
1205	  {1n+U32.to_nat(a) == U32.to_nat(U32.inc(a)) : Nat}
1206	
1207	def u32_inc_exact_sym(a, h):
1208	  Equal.sym(Nat, U32.to_nat(U32.inc(a)), 1n+U32.to_nat(a), u32_inc_exact(a, h))
1209	
1210	# U32 increment wraps modulo 2^32: to_nat (inc a) = (1 + a) % 2^32, reversed to rewrite toward the simple side.
1211	law u32_inc_wrap_sym:
1212	  for a: U32
1213	  {Nat.mod(1n+U32.to_nat(a), Nat.pow(2n, 32n)) == U32.to_nat(U32.inc(a)) : Nat}
1214	
1215	def u32_inc_wrap_sym(a):
1216	  Equal.sym(Nat, U32.to_nat(U32.inc(a)), Nat.mod(1n+U32.to_nat(a), Nat.pow(2n, 32n)), u32_inc_wrap(a))
1217	
1218	# Converting a natural below 2^32 to U32 and back is the identity: k < 2^32 implies to_nat (from_nat k) = k, reversed to rewrite toward the simple side.
1219	law u32_to_nat_from_nat_sym:
1220	  for k: Nat
1221	  for h: MNat.lt(k, Nat.pow(2n, 32n))
1222	  {k == U32.to_nat(U32.from_nat(k)) : Nat}
1223	
1224	def u32_to_nat_from_nat_sym(k, h):
1225	  Equal.sym(Nat, U32.to_nat(U32.from_nat(k)), k, u32_to_nat_from_nat(k, h))
1226	
1227	# Converting a U32 to a natural and back is the identity: from_nat (to_nat a) = a, reversed to rewrite toward the simple side.
1228	law u32_from_nat_to_nat_sym:
1229	  for a: U32
1230	  {a == U32.from_nat(U32.to_nat(a)) : U32}
1231	
1232	def u32_from_nat_to_nat_sym(a):
1233	  Equal.sym(U32, U32.from_nat(U32.to_nat(a)), a, u32_from_nat_to_nat(a))
1234	
1235	# Converting any natural to U32 and back reduces it modulo 2^32: to_nat (from_nat k) = k % 2^32, reversed to rewrite toward the simple side.
1236	law u32_to_nat_from_nat_mod_sym:
1237	  for k: Nat
1238	  {Nat.mod(k, Nat.pow(2n, 32n)) == U32.to_nat(U32.from_nat(k)) : Nat}
1239	
1240	def u32_to_nat_from_nat_mod_sym(k):
1241	  Equal.sym(Nat, U32.to_nat(U32.from_nat(k)), Nat.mod(k, Nat.pow(2n, 32n)), u32_to_nat_from_nat_mod(k))
1242	
1243	# The U32 minimum is the minimum of the values: to_nat (min a b) = min (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1244	law u32_min_to_nat_sym:
1245	  for a: U32
1246	  for b: U32
1247	  {Nat.min(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.min(a, b)) : Nat}
1248	
1249	def u32_min_to_nat_sym(a, b):
1250	  Equal.sym(Nat, U32.to_nat(U32.min(a, b)), Nat.min(U32.to_nat(a), U32.to_nat(b)), u32_min_to_nat(a, b))
1251	
1252	# The U32 maximum is the maximum of the values: to_nat (max a b) = max (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
1253	law u32_max_to_nat_sym:
1254	  for a: U32
1255	  for b: U32
1256	  {Nat.max(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.max(a, b)) : Nat}
1257	
1258	def u32_max_to_nat_sym(a, b):
1259	  Equal.sym(Nat, U32.to_nat(U32.max(a, b)), Nat.max(U32.to_nat(a), U32.to_nat(b)), u32_max_to_nat(a, b))
1260	
1261	# U32 division is the division of the values, also for a zero divisor: to_nat (a / b) = to_nat a / to_nat b, reversed to rewrite toward the simple side.
1262	law u32_div_to_nat_sym:
1263	  for a: U32
1264	  for b: U32
1265	  {Nat.div(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.div(a, b)) : Nat}
1266	
1267	def u32_div_to_nat_sym(a, b):
1268	  Equal.sym(Nat, U32.to_nat(U32.div(a, b)), Nat.div(U32.to_nat(a), U32.to_nat(b)), u32_div_to_nat(a, b))