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, 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	# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
776	
777	# The zero word is the natural zero: to_nat (zero n) = 0, reversed to rewrite toward the simple side.
778	law word_to_nat_zero_sym:
779	  for n: Nat
780	  {0n == Word.to_nat(n, Word.zero(n)) : Nat}
781	
782	def word_to_nat_zero_sym(n):
783	  Equal.sym(Nat, Word.to_nat(n, Word.zero(n)), 0n, word_to_nat_zero(n))
784	
785	# Comparing words compares their values: cmp a b = cmp (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
786	law word_cmp_to_nat_sym:
787	  for n: Nat
788	  for a: Word(n)
789	  for b: Word(n)
790	  {Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.cmp(n, a, b) : Cmp}
791	
792	def word_cmp_to_nat_sym(n, a, b):
793	  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))
794	
795	# 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.
796	law word_not_add_sym:
797	  for n: Nat
798	  for w: Word(n)
799	  {Nat.pow(2n, n) == 1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) : Nat}
800	
801	def word_not_add_sym(n, w):
802	  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))
803	
804	# 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.
805	law word_adc_exact_sym:
806	  for n: Nat
807	  for a: Word(n)
808	  for b: Word(n)
809	  for c: Bool
810	  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))
811	  {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}
812	
813	def word_adc_exact_sym(n, a, b, c, h):
814	  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))
815	
816	# 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.
817	law word_adc_overflow_sym:
818	  for n: Nat
819	  for a: Word(n)
820	  for b: Word(n)
821	  for c: Bool
822	  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)))
823	  {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}
824	
825	def word_adc_overflow_sym(n, a, b, c, h):
826	  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))
827	
828	# 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.
829	law word_adc_wrap_sym:
830	  for n: Nat
831	  for a: Word(n)
832	  for b: Word(n)
833	  for c: Bool
834	  {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}
835	
836	def word_adc_wrap_sym(n, a, b, c):
837	  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))
838	
839	# 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.
840	law word_add_exact_sym:
841	  for n: Nat
842	  for a: Word(n)
843	  for b: Word(n)
844	  for h: MNat.lt(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n))
845	  {Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.to_nat(n, Word.add(n, a, b)) : Nat}
846	
847	def word_add_exact_sym(n, a, b, h):
848	  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))
849	
850	# Word addition wraps modulo 2^n: to_nat (add a b) = (a + b) % 2^n, reversed to rewrite toward the simple side.
851	law word_add_wrap_sym:
852	  for n: Nat
853	  for a: Word(n)
854	  for b: Word(n)
855	  {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}
856	
857	def word_add_wrap_sym(n, a, b):
858	  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))
859	
860	# Increment is exact without overflow: 1 + w < 2^n implies to_nat (inc w) = 1 + w, reversed to rewrite toward the simple side.
861	law word_inc_exact_sym:
862	  for n: Nat
863	  for w: Word(n)
864	  for h: MNat.lt(1n+Word.to_nat(n, w), Nat.pow(2n, n))
865	  {1n+Word.to_nat(n, w) == Word.to_nat(n, Word.inc(n, w)) : Nat}
866	
867	def word_inc_exact_sym(n, w, h):
868	  Equal.sym(Nat, Word.to_nat(n, Word.inc(n, w)), 1n+Word.to_nat(n, w), word_inc_exact(n, w, h))
869	
870	# Increment wraps modulo 2^n: to_nat (inc w) = (1 + w) % 2^n, reversed to rewrite toward the simple side.
871	law word_inc_wrap_sym:
872	  for n: Nat
873	  for w: Word(n)
874	  {Nat.mod(1n+Word.to_nat(n, w), Nat.pow(2n, n)) == Word.to_nat(n, Word.inc(n, w)) : Nat}
875	
876	def word_inc_wrap_sym(n, w):
877	  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))
878	
879	# Word subtraction is exact without underflow: b <= a implies to_nat (sub a b) = a - b, reversed to rewrite toward the simple side.
880	law word_sub_exact_sym:
881	  for n: Nat
882	  for a: Word(n)
883	  for b: Word(n)
884	  for h: MNat.le(Word.to_nat(n, b), Word.to_nat(n, a))
885	  {Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.to_nat(n, Word.sub(n, a, b)) : Nat}
886	
887	def word_sub_exact_sym(n, a, b, h):
888	  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))
889	
890	# Word subtraction wraps modulo 2^n: to_nat (sub a b) = (a + (2^n - b)) % 2^n, reversed to rewrite toward the simple side.
891	law word_sub_wrap_sym:
892	  for n: Nat
893	  for a: Word(n)
894	  for b: Word(n)
895	  {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}
896	
897	def word_sub_wrap_sym(n, a, b):
898	  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))
899	
900	# Comparing U32s compares their values: cmp a b = cmp (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
901	law u32_cmp_to_nat_sym:
902	  for a: U32
903	  for b: U32
904	  {Nat.cmp(U32.to_nat(a), U32.to_nat(b)) == U32.cmp(a, b) : Cmp}
905	
906	def u32_cmp_to_nat_sym(a, b):
907	  Equal.sym(Cmp, U32.cmp(a, b), Nat.cmp(U32.to_nat(a), U32.to_nat(b)), u32_cmp_to_nat(a, b))
908	
909	# U32 equality tests the values: is_eq a b = is_eq (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
910	law u32_is_eq_to_nat_sym:
911	  for a: U32
912	  for b: U32
913	  {Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) == U32.is_eq(a, b) : Bool}
914	
915	def u32_is_eq_to_nat_sym(a, b):
916	  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))
917	
918	# U32 disequality tests the values: is_ne a b = is_ne (to_nat a) (to_nat b), reversed to rewrite toward the simple side.
919	law u32_is_ne_to_nat_sym:
920	  for a: U32
921	  for b: U32
922	  {Nat.is_ne(U32.to_nat(a), U32.to_nat(b)) == U32.is_ne(a, b) : Bool}
923	
924	def u32_is_ne_to_nat_sym(a, b):
925	  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))
926	
927	# 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.
928	law u32_is_lt_to_nat_sym:
929	  for a: U32
930	  for b: U32
931	  {Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == U32.is_lt(a, b) : Bool}
932	
933	def u32_is_lt_to_nat_sym(a, b):
934	  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))
935	
936	# 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.
937	law u32_is_le_to_nat_sym:
938	  for a: U32
939	  for b: U32
940	  {Nat.is_le(U32.to_nat(a), U32.to_nat(b)) == U32.is_le(a, b) : Bool}
941	
942	def u32_is_le_to_nat_sym(a, b):
943	  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))
944	
945	# 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.
946	law u32_is_gt_to_nat_sym:
947	  for a: U32
948	  for b: U32
949	  {Nat.is_gt(U32.to_nat(a), U32.to_nat(b)) == U32.is_gt(a, b) : Bool}
950	
951	def u32_is_gt_to_nat_sym(a, b):
952	  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))
953	
954	# 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.
955	law u32_is_ge_to_nat_sym:
956	  for a: U32
957	  for b: U32
958	  {Nat.is_ge(U32.to_nat(a), U32.to_nat(b)) == U32.is_ge(a, b) : Bool}
959	
960	def u32_is_ge_to_nat_sym(a, b):
961	  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))
962	
963	# U32 addition is exact without overflow: a + b < 2^32 implies to_nat (a + b) = a + b, reversed to rewrite toward the simple side.
964	law u32_add_exact_sym:
965	  for a: U32
966	  for b: U32
967	  for h: MNat.lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n))
968	  {Nat.add(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.add(a, b)) : Nat}
969	
970	def u32_add_exact_sym(a, b, h):
971	  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))
972	
973	# U32 addition wraps modulo 2^32: to_nat (a + b) = (a + b) % 2^32, reversed to rewrite toward the simple side.
974	law u32_add_wrap_sym:
975	  for a: U32
976	  for b: U32
977	  {Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.pow(2n, 32n)) == U32.to_nat(U32.add(a, b)) : Nat}
978	
979	def u32_add_wrap_sym(a, b):
980	  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))
981	
982	# U32 subtraction is exact without underflow: b <= a implies to_nat (a - b) = a - b, reversed to rewrite toward the simple side.
983	law u32_sub_exact_sym:
984	  for a: U32
985	  for b: U32
986	  for h: MNat.le(U32.to_nat(b), U32.to_nat(a))
987	  {Nat.sub(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.sub(a, b)) : Nat}
988	
989	def u32_sub_exact_sym(a, b, h):
990	  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))
991	
992	# U32 subtraction wraps modulo 2^32: to_nat (a - b) = (a + (2^32 - b)) % 2^32, reversed to rewrite toward the simple side.
993	law u32_sub_wrap_sym:
994	  for a: U32
995	  for b: U32
996	  {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}
997	
998	def u32_sub_wrap_sym(a, b):
999	  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))
1000	
1001	# U32 increment is exact without overflow: 1 + a < 2^32 implies to_nat (inc a) = 1 + a, reversed to rewrite toward the simple side.
1002	law u32_inc_exact_sym:
1003	  for a: U32
1004	  for h: MNat.lt(1n+U32.to_nat(a), Nat.pow(2n, 32n))
1005	  {1n+U32.to_nat(a) == U32.to_nat(U32.inc(a)) : Nat}
1006	
1007	def u32_inc_exact_sym(a, h):
1008	  Equal.sym(Nat, U32.to_nat(U32.inc(a)), 1n+U32.to_nat(a), u32_inc_exact(a, h))
1009	
1010	# U32 increment wraps modulo 2^32: to_nat (inc a) = (1 + a) % 2^32, reversed to rewrite toward the simple side.
1011	law u32_inc_wrap_sym:
1012	  for a: U32
1013	  {Nat.mod(1n+U32.to_nat(a), Nat.pow(2n, 32n)) == U32.to_nat(U32.inc(a)) : Nat}
1014	
1015	def u32_inc_wrap_sym(a):
1016	  Equal.sym(Nat, U32.to_nat(U32.inc(a)), Nat.mod(1n+U32.to_nat(a), Nat.pow(2n, 32n)), u32_inc_wrap(a))
1017	
1018	# 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.
1019	law u32_to_nat_from_nat_sym:
1020	  for k: Nat
1021	  for h: MNat.lt(k, Nat.pow(2n, 32n))
1022	  {k == U32.to_nat(U32.from_nat(k)) : Nat}
1023	
1024	def u32_to_nat_from_nat_sym(k, h):
1025	  Equal.sym(Nat, U32.to_nat(U32.from_nat(k)), k, u32_to_nat_from_nat(k, h))
1026	
1027	# Converting a U32 to a natural and back is the identity: from_nat (to_nat a) = a, reversed to rewrite toward the simple side.
1028	law u32_from_nat_to_nat_sym:
1029	  for a: U32
1030	  {a == U32.from_nat(U32.to_nat(a)) : U32}
1031	
1032	def u32_from_nat_to_nat_sym(a):
1033	  Equal.sym(U32, U32.from_nat(U32.to_nat(a)), a, u32_from_nat_to_nat(a))
1034	
1035	# 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.
1036	law u32_to_nat_from_nat_mod_sym:
1037	  for k: Nat
1038	  {Nat.mod(k, Nat.pow(2n, 32n)) == U32.to_nat(U32.from_nat(k)) : Nat}
1039	
1040	def u32_to_nat_from_nat_mod_sym(k):
1041	  Equal.sym(Nat, U32.to_nat(U32.from_nat(k)), Nat.mod(k, Nat.pow(2n, 32n)), u32_to_nat_from_nat_mod(k))
1042	
1043	# 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.
1044	law u32_min_to_nat_sym:
1045	  for a: U32
1046	  for b: U32
1047	  {Nat.min(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.min(a, b)) : Nat}
1048	
1049	def u32_min_to_nat_sym(a, b):
1050	  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))
1051	
1052	# 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.
1053	law u32_max_to_nat_sym:
1054	  for a: U32
1055	  for b: U32
1056	  {Nat.max(U32.to_nat(a), U32.to_nat(b)) == U32.to_nat(U32.max(a, b)) : Nat}
1057	
1058	def u32_max_to_nat_sym(a, b):
1059	  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))