1	import Base
2	import ../../lib/nat.bend as N
3	import ../../lib/logic.bend as L
4	import ../../lib/u32.bend as U
5	import ./words.bend as LW
6	import ../../math/hash/hash.bend as HH
7	import ../../math/natural/arith.bend as NR
8	import ../../../src/crypto/argon2/phc.bend as PH
9	# Generated by tools/generators/argon2_phc_gen.py; do not edit by hand.
10	
11	# The PHC string of an Argon2id hash parses back to its fields: base64 and
12	# decimal round trips, and the '$'-separated fields. Every finite fact
13	# (a crumb, a base64 digit, a decimal digit) is checked value by value.
14	
15	# Every byte is below 256.
16	def ok(bs: List<&2, U32>) -> Bool:
17	  match bs:
18	    case Nil{}:
19	      True{}
20	    case x <> r:
21	      Bool.and(Nat.is_lt(U32.to_nat(x), 256n), ok(r))
22	
23	def ok_head(+x: U32, +r: List<&2, U32>, +h: {ok(x <> r) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}:
24	  L.and_left(Nat.is_lt(U32.to_nat(x), 256n), ok(r), h)
25	
26	def ok_tail(+x: U32, +r: List<&2, U32>, +h: {ok(x <> r) == True{} : Bool}) -> {ok(r) == True{} : Bool}:
27	  L.and_right(Nat.is_lt(U32.to_nat(x), 256n), ok(r), h)
28	
29	def u(+n: Nat) -> U32:
30	  U32.from_nat(n)
31	
32	# ---------------------------------------------------------------- base64 digits
33	
34	def dv_n(+n: Nat, +h: {Nat.is_lt(n, 64n) == True{} : Bool}) -> {PH.value(PH.digit(u(n))) == Some{u(n)} : Maybe<&2, U32>}:
35	  match n:
36	    case 0n:
37	      {==}
38	    case 1n:
39	      {==}
40	    case 2n:
41	      {==}
42	    case 3n:
43	      {==}
44	    case 4n:
45	      {==}
46	    case 5n:
47	      {==}
48	    case 6n:
49	      {==}
50	    case 7n:
51	      {==}
52	    case 8n:
53	      {==}
54	    case 9n:
55	      {==}
56	    case 10n:
57	      {==}
58	    case 11n:
59	      {==}
60	    case 12n:
61	      {==}
62	    case 13n:
63	      {==}
64	    case 14n:
65	      {==}
66	    case 15n:
67	      {==}
68	    case 16n:
69	      {==}
70	    case 17n:
71	      {==}
72	    case 18n:
73	      {==}
74	    case 19n:
75	      {==}
76	    case 20n:
77	      {==}
78	    case 21n:
79	      {==}
80	    case 22n:
81	      {==}
82	    case 23n:
83	      {==}
84	    case 24n:
85	      {==}
86	    case 25n:
87	      {==}
88	    case 26n:
89	      {==}
90	    case 27n:
91	      {==}
92	    case 28n:
93	      {==}
94	    case 29n:
95	      {==}
96	    case 30n:
97	      {==}
98	    case 31n:
99	      {==}
100	    case 32n:
101	      {==}
102	    case 33n:
103	      {==}
104	    case 34n:
105	      {==}
106	    case 35n:
107	      {==}
108	    case 36n:
109	      {==}
110	    case 37n:
111	      {==}
112	    case 38n:
113	      {==}
114	    case 39n:
115	      {==}
116	    case 40n:
117	      {==}
118	    case 41n:
119	      {==}
120	    case 42n:
121	      {==}
122	    case 43n:
123	      {==}
124	    case 44n:
125	      {==}
126	    case 45n:
127	      {==}
128	    case 46n:
129	      {==}
130	    case 47n:
131	      {==}
132	    case 48n:
133	      {==}
134	    case 49n:
135	      {==}
136	    case 50n:
137	      {==}
138	    case 51n:
139	      {==}
140	    case 52n:
141	      {==}
142	    case 53n:
143	      {==}
144	    case 54n:
145	      {==}
146	    case 55n:
147	      {==}
148	    case 56n:
149	      {==}
150	    case 57n:
151	      {==}
152	    case 58n:
153	      {==}
154	    case 59n:
155	      {==}
156	    case 60n:
157	      {==}
158	    case 61n:
159	      {==}
160	    case 62n:
161	      {==}
162	    case 63n:
163	      {==}
164	    case 64n+r:
165	      Empty.absurd({PH.value(PH.digit(u(64n+r))) == Some{u(64n+r)} : Maybe<&2, U32>}, N.lt_zero_absurd(r, h))
166	
167	def digit_value(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 64n) == True{} : Bool}) -> {PH.value(PH.digit(x)) == Some{x} : Maybe<&2, U32>}:
168	  %LW.rt(x) : {PH.value(PH.digit(_)) == Some{_} : Maybe<&2, U32>}
169	  dv_n(U32.to_nat(x), h)
170	
171	def nd_n(+n: Nat, +h: {Nat.is_lt(n, 64n) == True{} : Bool}) -> {PH.dollar(SCon{PH.digit(u(n)), SNil{}}) == False{} : Bool}:
172	  match n:
173	    case 0n:
174	      {==}
175	    case 1n:
176	      {==}
177	    case 2n:
178	      {==}
179	    case 3n:
180	      {==}
181	    case 4n:
182	      {==}
183	    case 5n:
184	      {==}
185	    case 6n:
186	      {==}
187	    case 7n:
188	      {==}
189	    case 8n:
190	      {==}
191	    case 9n:
192	      {==}
193	    case 10n:
194	      {==}
195	    case 11n:
196	      {==}
197	    case 12n:
198	      {==}
199	    case 13n:
200	      {==}
201	    case 14n:
202	      {==}
203	    case 15n:
204	      {==}
205	    case 16n:
206	      {==}
207	    case 17n:
208	      {==}
209	    case 18n:
210	      {==}
211	    case 19n:
212	      {==}
213	    case 20n:
214	      {==}
215	    case 21n:
216	      {==}
217	    case 22n:
218	      {==}
219	    case 23n:
220	      {==}
221	    case 24n:
222	      {==}
223	    case 25n:
224	      {==}
225	    case 26n:
226	      {==}
227	    case 27n:
228	      {==}
229	    case 28n:
230	      {==}
231	    case 29n:
232	      {==}
233	    case 30n:
234	      {==}
235	    case 31n:
236	      {==}
237	    case 32n:
238	      {==}
239	    case 33n:
240	      {==}
241	    case 34n:
242	      {==}
243	    case 35n:
244	      {==}
245	    case 36n:
246	      {==}
247	    case 37n:
248	      {==}
249	    case 38n:
250	      {==}
251	    case 39n:
252	      {==}
253	    case 40n:
254	      {==}
255	    case 41n:
256	      {==}
257	    case 42n:
258	      {==}
259	    case 43n:
260	      {==}
261	    case 44n:
262	      {==}
263	    case 45n:
264	      {==}
265	    case 46n:
266	      {==}
267	    case 47n:
268	      {==}
269	    case 48n:
270	      {==}
271	    case 49n:
272	      {==}
273	    case 50n:
274	      {==}
275	    case 51n:
276	      {==}
277	    case 52n:
278	      {==}
279	    case 53n:
280	      {==}
281	    case 54n:
282	      {==}
283	    case 55n:
284	      {==}
285	    case 56n:
286	      {==}
287	    case 57n:
288	      {==}
289	    case 58n:
290	      {==}
291	    case 59n:
292	      {==}
293	    case 60n:
294	      {==}
295	    case 61n:
296	      {==}
297	    case 62n:
298	      {==}
299	    case 63n:
300	      {==}
301	    case 64n+r:
302	      Empty.absurd({PH.dollar(SCon{PH.digit(u(64n+r)), SNil{}}) == False{} : Bool}, N.lt_zero_absurd(r, h))
303	
304	def no_dollar(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 64n) == True{} : Bool}) -> {PH.dollar(SCon{PH.digit(x), SNil{}}) == False{} : Bool}:
305	  %LW.rt(x) : {PH.dollar(SCon{PH.digit(_), SNil{}}) == False{} : Bool}
306	  nd_n(U32.to_nat(x), h)
307	
308	# ---------------------------------------------------------------- crumbs
309	
310	# A value below 4 round-trips through U32.
311	def tn(+i: Nat, +h: {Nat.is_lt(i, 4n) == True{} : Bool}) -> {U32.to_nat(U32.from_nat(i)) == i : Nat}:
312	  U.to_nat_from_nat(i, 2n, {==}, h)
313	
314	# m < K * 4 gives m / 4 < K.
315	def div4_lt(+m: Nat, +k: Nat, +h: {Nat.is_lt(m, Nat.mul(k, 4n)) == True{} : Bool}) -> {Nat.is_lt(Nat.div(m, 4n), k) == True{} : Bool}:
316	  N.not_le_lt(k, Nat.div(m, 4n), Equal.trans(Bool, Nat.is_le(k, Nat.div(m, 4n)), Nat.is_le(Nat.mul(k, 4n), m), False{}, NR.le_div(3n, k, m), N.lt_not_le(m, Nat.mul(k, 4n), h)))
317	
318	def c0_lt(+x: U32) -> {Nat.is_lt(U32.to_nat(PH.c0(x)), 4n) == True{} : Bool}:
319	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(U32.to_nat(x), 4n))), Nat.mod(U32.to_nat(x), 4n), tn(Nat.mod(U32.to_nat(x), 4n), NR.dm_lt(3n, U32.to_nat(x)))) : {Nat.is_lt(_, 4n) == True{} : Bool}
320	  NR.dm_lt(3n, U32.to_nat(x))
321	
322	def c1_lt(+x: U32) -> {Nat.is_lt(U32.to_nat(PH.c1(x)), 4n) == True{} : Bool}:
323	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n))), Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n), tn(Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n), NR.dm_lt(3n, Nat.div(U32.to_nat(x), 4n)))) : {Nat.is_lt(_, 4n) == True{} : Bool}
324	  NR.dm_lt(3n, Nat.div(U32.to_nat(x), 4n))
325	
326	def c2_lt(+x: U32) -> {Nat.is_lt(U32.to_nat(PH.c2(x)), 4n) == True{} : Bool}:
327	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), NR.dm_lt(3n, Nat.div(Nat.div(U32.to_nat(x), 4n), 4n)))) : {Nat.is_lt(_, 4n) == True{} : Bool}
328	  NR.dm_lt(3n, Nat.div(Nat.div(U32.to_nat(x), 4n), 4n))
329	
330	def t3_lt(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}) -> {Nat.is_lt(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), 4n) == True{} : Bool}:
331	  div4_lt(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n, div4_lt(Nat.div(U32.to_nat(x), 4n), 16n, div4_lt(U32.to_nat(x), 64n, h)))
332	
333	def c3_lt(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(PH.c3(x)), 4n) == True{} : Bool}:
334	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), t3_lt(x, h))) : {Nat.is_lt(_, 4n) == True{} : Bool}
335	  t3_lt(x, h)
336	
337	# A byte is the byte of its crumbs.
338	def byte_rt(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}) -> {PH.byte_of(PH.c3(x), PH.c2(x), PH.c1(x), PH.c0(x)) == x : U32}:
339	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), t3_lt(x, h))) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(_, 4n), U32.to_nat(PH.c2(x))), 4n), U32.to_nat(PH.c1(x))), 4n), U32.to_nat(PH.c0(x)))) == x : U32}
340	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), NR.dm_lt(3n, Nat.div(Nat.div(U32.to_nat(x), 4n), 4n)))) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), 4n), _), 4n), U32.to_nat(PH.c1(x))), 4n), U32.to_nat(PH.c0(x)))) == x : U32}
341	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n))), Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n), tn(Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n), NR.dm_lt(3n, Nat.div(U32.to_nat(x), 4n)))) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), 4n), Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n)), 4n), _), 4n), U32.to_nat(PH.c0(x)))) == x : U32}
342	  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(U32.to_nat(x), 4n))), Nat.mod(U32.to_nat(x), 4n), tn(Nat.mod(U32.to_nat(x), 4n), NR.dm_lt(3n, U32.to_nat(x)))) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), 4n), Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n)), 4n), Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n)), 4n), _)) == x : U32}
343	  %NR.dm_eq(3n, Nat.div(Nat.div(U32.to_nat(x), 4n), 4n)) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(_, 4n), Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n)), 4n), Nat.mod(U32.to_nat(x), 4n))) == x : U32}
344	  %NR.dm_eq(3n, Nat.div(U32.to_nat(x), 4n)) : {U32.from_nat(Nat.add(Nat.mul(_, 4n), Nat.mod(U32.to_nat(x), 4n))) == x : U32}
345	  %NR.dm_eq(3n, U32.to_nat(x)) : {U32.from_nat(_) == x : U32}
346	  LW.rt(x)
347	
348	# ---------------------------------------------------------------- digit values of crumbs
349	
350	def su_eq_n(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_lt(a, 4n) == True{} : Bool}, +hb: {Nat.is_lt(b, 4n) == True{} : Bool}, +hc: {Nat.is_lt(c, 4n) == True{} : Bool}) -> {PH.su(PH.sext(u(a), u(b), u(c))) == u(a) : U32}:
351	  match a b c:
352	    case 0n 0n 0n:
353	      {==}
354	    case 0n 0n 1n:
355	      {==}
356	    case 0n 0n 2n:
357	      {==}
358	    case 0n 0n 3n:
359	      {==}
360	    case 0n 1n 0n:
361	      {==}
362	    case 0n 1n 1n:
363	      {==}
364	    case 0n 1n 2n:
365	      {==}
366	    case 0n 1n 3n:
367	      {==}
368	    case 0n 2n 0n:
369	      {==}
370	    case 0n 2n 1n:
371	      {==}
372	    case 0n 2n 2n:
373	      {==}
374	    case 0n 2n 3n:
375	      {==}
376	    case 0n 3n 0n:
377	      {==}
378	    case 0n 3n 1n:
379	      {==}
380	    case 0n 3n 2n:
381	      {==}
382	    case 0n 3n 3n:
383	      {==}
384	    case 1n 0n 0n:
385	      {==}
386	    case 1n 0n 1n:
387	      {==}
388	    case 1n 0n 2n:
389	      {==}
390	    case 1n 0n 3n:
391	      {==}
392	    case 1n 1n 0n:
393	      {==}
394	    case 1n 1n 1n:
395	      {==}
396	    case 1n 1n 2n:
397	      {==}
398	    case 1n 1n 3n:
399	      {==}
400	    case 1n 2n 0n:
401	      {==}
402	    case 1n 2n 1n:
403	      {==}
404	    case 1n 2n 2n:
405	      {==}
406	    case 1n 2n 3n:
407	      {==}
408	    case 1n 3n 0n:
409	      {==}
410	    case 1n 3n 1n:
411	      {==}
412	    case 1n 3n 2n:
413	      {==}
414	    case 1n 3n 3n:
415	      {==}
416	    case 2n 0n 0n:
417	      {==}
418	    case 2n 0n 1n:
419	      {==}
420	    case 2n 0n 2n:
421	      {==}
422	    case 2n 0n 3n:
423	      {==}
424	    case 2n 1n 0n:
425	      {==}
426	    case 2n 1n 1n:
427	      {==}
428	    case 2n 1n 2n:
429	      {==}
430	    case 2n 1n 3n:
431	      {==}
432	    case 2n 2n 0n:
433	      {==}
434	    case 2n 2n 1n:
435	      {==}
436	    case 2n 2n 2n:
437	      {==}
438	    case 2n 2n 3n:
439	      {==}
440	    case 2n 3n 0n:
441	      {==}
442	    case 2n 3n 1n:
443	      {==}
444	    case 2n 3n 2n:
445	      {==}
446	    case 2n 3n 3n:
447	      {==}
448	    case 3n 0n 0n:
449	      {==}
450	    case 3n 0n 1n:
451	      {==}
452	    case 3n 0n 2n:
453	      {==}
454	    case 3n 0n 3n:
455	      {==}
456	    case 3n 1n 0n:
457	      {==}
458	    case 3n 1n 1n:
459	      {==}
460	    case 3n 1n 2n:
461	      {==}
462	    case 3n 1n 3n:
463	      {==}
464	    case 3n 2n 0n:
465	      {==}
466	    case 3n 2n 1n:
467	      {==}
468	    case 3n 2n 2n:
469	      {==}
470	    case 3n 2n 3n:
471	      {==}
472	    case 3n 3n 0n:
473	      {==}
474	    case 3n 3n 1n:
475	      {==}
476	    case 3n 3n 2n:
477	      {==}
478	    case 3n 3n 3n:
479	      {==}
480	    case 4n+r _ _:
481	      Empty.absurd({PH.su(PH.sext(u(4n+r), u(b), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, ha))
482	    case 0n 4n+r _:
483	      Empty.absurd({PH.su(PH.sext(u(0n), u(4n+r), u(c))) == u(0n) : U32}, N.lt_zero_absurd(r, hb))
484	    case 0n 0n 4n+r:
485	      Empty.absurd({PH.su(PH.sext(u(0n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
486	    case 0n 1n 4n+r:
487	      Empty.absurd({PH.su(PH.sext(u(0n), u(1n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
488	    case 0n 2n 4n+r:
489	      Empty.absurd({PH.su(PH.sext(u(0n), u(2n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
490	    case 0n 3n 4n+r:
491	      Empty.absurd({PH.su(PH.sext(u(0n), u(3n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
492	    case 1n 4n+r _:
493	      Empty.absurd({PH.su(PH.sext(u(1n), u(4n+r), u(c))) == u(1n) : U32}, N.lt_zero_absurd(r, hb))
494	    case 1n 0n 4n+r:
495	      Empty.absurd({PH.su(PH.sext(u(1n), u(0n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
496	    case 1n 1n 4n+r:
497	      Empty.absurd({PH.su(PH.sext(u(1n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
498	    case 1n 2n 4n+r:
499	      Empty.absurd({PH.su(PH.sext(u(1n), u(2n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
500	    case 1n 3n 4n+r:
501	      Empty.absurd({PH.su(PH.sext(u(1n), u(3n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
502	    case 2n 4n+r _:
503	      Empty.absurd({PH.su(PH.sext(u(2n), u(4n+r), u(c))) == u(2n) : U32}, N.lt_zero_absurd(r, hb))
504	    case 2n 0n 4n+r:
505	      Empty.absurd({PH.su(PH.sext(u(2n), u(0n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
506	    case 2n 1n 4n+r:
507	      Empty.absurd({PH.su(PH.sext(u(2n), u(1n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
508	    case 2n 2n 4n+r:
509	      Empty.absurd({PH.su(PH.sext(u(2n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
510	    case 2n 3n 4n+r:
511	      Empty.absurd({PH.su(PH.sext(u(2n), u(3n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
512	    case 3n 4n+r _:
513	      Empty.absurd({PH.su(PH.sext(u(3n), u(4n+r), u(c))) == u(3n) : U32}, N.lt_zero_absurd(r, hb))
514	    case 3n 0n 4n+r:
515	      Empty.absurd({PH.su(PH.sext(u(3n), u(0n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
516	    case 3n 1n 4n+r:
517	      Empty.absurd({PH.su(PH.sext(u(3n), u(1n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
518	    case 3n 2n 4n+r:
519	      Empty.absurd({PH.su(PH.sext(u(3n), u(2n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
520	    case 3n 3n 4n+r:
521	      Empty.absurd({PH.su(PH.sext(u(3n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
522	
523	def su_eq(+x: U32, +y: U32, +z: U32, +hx: {Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool}, +hy: {Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool}, +hz: {Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool}) -> {PH.su(PH.sext(x, y, z)) == x : U32}:
524	  %LW.rt(x) : {PH.su(PH.sext(_, y, z)) == _ : U32}
525	  %LW.rt(y) : {PH.su(PH.sext(u(U32.to_nat(x)), _, z)) == u(U32.to_nat(x)) : U32}
526	  %LW.rt(z) : {PH.su(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)) == u(U32.to_nat(x)) : U32}
527	  su_eq_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)
528	
529	def sv_eq_n(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_lt(a, 4n) == True{} : Bool}, +hb: {Nat.is_lt(b, 4n) == True{} : Bool}, +hc: {Nat.is_lt(c, 4n) == True{} : Bool}) -> {PH.sv(PH.sext(u(a), u(b), u(c))) == u(b) : U32}:
530	  match a b c:
531	    case 0n 0n 0n:
532	      {==}
533	    case 0n 0n 1n:
534	      {==}
535	    case 0n 0n 2n:
536	      {==}
537	    case 0n 0n 3n:
538	      {==}
539	    case 0n 1n 0n:
540	      {==}
541	    case 0n 1n 1n:
542	      {==}
543	    case 0n 1n 2n:
544	      {==}
545	    case 0n 1n 3n:
546	      {==}
547	    case 0n 2n 0n:
548	      {==}
549	    case 0n 2n 1n:
550	      {==}
551	    case 0n 2n 2n:
552	      {==}
553	    case 0n 2n 3n:
554	      {==}
555	    case 0n 3n 0n:
556	      {==}
557	    case 0n 3n 1n:
558	      {==}
559	    case 0n 3n 2n:
560	      {==}
561	    case 0n 3n 3n:
562	      {==}
563	    case 1n 0n 0n:
564	      {==}
565	    case 1n 0n 1n:
566	      {==}
567	    case 1n 0n 2n:
568	      {==}
569	    case 1n 0n 3n:
570	      {==}
571	    case 1n 1n 0n:
572	      {==}
573	    case 1n 1n 1n:
574	      {==}
575	    case 1n 1n 2n:
576	      {==}
577	    case 1n 1n 3n:
578	      {==}
579	    case 1n 2n 0n:
580	      {==}
581	    case 1n 2n 1n:
582	      {==}
583	    case 1n 2n 2n:
584	      {==}
585	    case 1n 2n 3n:
586	      {==}
587	    case 1n 3n 0n:
588	      {==}
589	    case 1n 3n 1n:
590	      {==}
591	    case 1n 3n 2n:
592	      {==}
593	    case 1n 3n 3n:
594	      {==}
595	    case 2n 0n 0n:
596	      {==}
597	    case 2n 0n 1n:
598	      {==}
599	    case 2n 0n 2n:
600	      {==}
601	    case 2n 0n 3n:
602	      {==}
603	    case 2n 1n 0n:
604	      {==}
605	    case 2n 1n 1n:
606	      {==}
607	    case 2n 1n 2n:
608	      {==}
609	    case 2n 1n 3n:
610	      {==}
611	    case 2n 2n 0n:
612	      {==}
613	    case 2n 2n 1n:
614	      {==}
615	    case 2n 2n 2n:
616	      {==}
617	    case 2n 2n 3n:
618	      {==}
619	    case 2n 3n 0n:
620	      {==}
621	    case 2n 3n 1n:
622	      {==}
623	    case 2n 3n 2n:
624	      {==}
625	    case 2n 3n 3n:
626	      {==}
627	    case 3n 0n 0n:
628	      {==}
629	    case 3n 0n 1n:
630	      {==}
631	    case 3n 0n 2n:
632	      {==}
633	    case 3n 0n 3n:
634	      {==}
635	    case 3n 1n 0n:
636	      {==}
637	    case 3n 1n 1n:
638	      {==}
639	    case 3n 1n 2n:
640	      {==}
641	    case 3n 1n 3n:
642	      {==}
643	    case 3n 2n 0n:
644	      {==}
645	    case 3n 2n 1n:
646	      {==}
647	    case 3n 2n 2n:
648	      {==}
649	    case 3n 2n 3n:
650	      {==}
651	    case 3n 3n 0n:
652	      {==}
653	    case 3n 3n 1n:
654	      {==}
655	    case 3n 3n 2n:
656	      {==}
657	    case 3n 3n 3n:
658	      {==}
659	    case 4n+r _ _:
660	      Empty.absurd({PH.sv(PH.sext(u(4n+r), u(b), u(c))) == u(b) : U32}, N.lt_zero_absurd(r, ha))
661	    case 0n 4n+r _:
662	      Empty.absurd({PH.sv(PH.sext(u(0n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb))
663	    case 0n 0n 4n+r:
664	      Empty.absurd({PH.sv(PH.sext(u(0n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
665	    case 0n 1n 4n+r:
666	      Empty.absurd({PH.sv(PH.sext(u(0n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
667	    case 0n 2n 4n+r:
668	      Empty.absurd({PH.sv(PH.sext(u(0n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
669	    case 0n 3n 4n+r:
670	      Empty.absurd({PH.sv(PH.sext(u(0n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
671	    case 1n 4n+r _:
672	      Empty.absurd({PH.sv(PH.sext(u(1n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb))
673	    case 1n 0n 4n+r:
674	      Empty.absurd({PH.sv(PH.sext(u(1n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
675	    case 1n 1n 4n+r:
676	      Empty.absurd({PH.sv(PH.sext(u(1n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
677	    case 1n 2n 4n+r:
678	      Empty.absurd({PH.sv(PH.sext(u(1n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
679	    case 1n 3n 4n+r:
680	      Empty.absurd({PH.sv(PH.sext(u(1n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
681	    case 2n 4n+r _:
682	      Empty.absurd({PH.sv(PH.sext(u(2n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb))
683	    case 2n 0n 4n+r:
684	      Empty.absurd({PH.sv(PH.sext(u(2n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
685	    case 2n 1n 4n+r:
686	      Empty.absurd({PH.sv(PH.sext(u(2n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
687	    case 2n 2n 4n+r:
688	      Empty.absurd({PH.sv(PH.sext(u(2n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
689	    case 2n 3n 4n+r:
690	      Empty.absurd({PH.sv(PH.sext(u(2n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
691	    case 3n 4n+r _:
692	      Empty.absurd({PH.sv(PH.sext(u(3n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb))
693	    case 3n 0n 4n+r:
694	      Empty.absurd({PH.sv(PH.sext(u(3n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
695	    case 3n 1n 4n+r:
696	      Empty.absurd({PH.sv(PH.sext(u(3n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
697	    case 3n 2n 4n+r:
698	      Empty.absurd({PH.sv(PH.sext(u(3n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
699	    case 3n 3n 4n+r:
700	      Empty.absurd({PH.sv(PH.sext(u(3n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
701	
702	def sv_eq(+x: U32, +y: U32, +z: U32, +hx: {Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool}, +hy: {Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool}, +hz: {Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool}) -> {PH.sv(PH.sext(x, y, z)) == y : U32}:
703	  %LW.rt(x) : {PH.sv(PH.sext(_, y, z)) == y : U32}
704	  %LW.rt(y) : {PH.sv(PH.sext(u(U32.to_nat(x)), _, z)) == _ : U32}
705	  %LW.rt(z) : {PH.sv(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)) == u(U32.to_nat(y)) : U32}
706	  sv_eq_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)
707	
708	def sw_eq_n(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_lt(a, 4n) == True{} : Bool}, +hb: {Nat.is_lt(b, 4n) == True{} : Bool}, +hc: {Nat.is_lt(c, 4n) == True{} : Bool}) -> {PH.sw(PH.sext(u(a), u(b), u(c))) == u(c) : U32}:
709	  match a b c:
710	    case 0n 0n 0n:
711	      {==}
712	    case 0n 0n 1n:
713	      {==}
714	    case 0n 0n 2n:
715	      {==}
716	    case 0n 0n 3n:
717	      {==}
718	    case 0n 1n 0n:
719	      {==}
720	    case 0n 1n 1n:
721	      {==}
722	    case 0n 1n 2n:
723	      {==}
724	    case 0n 1n 3n:
725	      {==}
726	    case 0n 2n 0n:
727	      {==}
728	    case 0n 2n 1n:
729	      {==}
730	    case 0n 2n 2n:
731	      {==}
732	    case 0n 2n 3n:
733	      {==}
734	    case 0n 3n 0n:
735	      {==}
736	    case 0n 3n 1n:
737	      {==}
738	    case 0n 3n 2n:
739	      {==}
740	    case 0n 3n 3n:
741	      {==}
742	    case 1n 0n 0n:
743	      {==}
744	    case 1n 0n 1n:
745	      {==}
746	    case 1n 0n 2n:
747	      {==}
748	    case 1n 0n 3n:
749	      {==}
750	    case 1n 1n 0n:
751	      {==}
752	    case 1n 1n 1n:
753	      {==}
754	    case 1n 1n 2n:
755	      {==}
756	    case 1n 1n 3n:
757	      {==}
758	    case 1n 2n 0n:
759	      {==}
760	    case 1n 2n 1n:
761	      {==}
762	    case 1n 2n 2n:
763	      {==}
764	    case 1n 2n 3n:
765	      {==}
766	    case 1n 3n 0n:
767	      {==}
768	    case 1n 3n 1n:
769	      {==}
770	    case 1n 3n 2n:
771	      {==}
772	    case 1n 3n 3n:
773	      {==}
774	    case 2n 0n 0n:
775	      {==}
776	    case 2n 0n 1n:
777	      {==}
778	    case 2n 0n 2n:
779	      {==}
780	    case 2n 0n 3n:
781	      {==}
782	    case 2n 1n 0n:
783	      {==}
784	    case 2n 1n 1n:
785	      {==}
786	    case 2n 1n 2n:
787	      {==}
788	    case 2n 1n 3n:
789	      {==}
790	    case 2n 2n 0n:
791	      {==}
792	    case 2n 2n 1n:
793	      {==}
794	    case 2n 2n 2n:
795	      {==}
796	    case 2n 2n 3n:
797	      {==}
798	    case 2n 3n 0n:
799	      {==}
800	    case 2n 3n 1n:
801	      {==}
802	    case 2n 3n 2n:
803	      {==}
804	    case 2n 3n 3n:
805	      {==}
806	    case 3n 0n 0n:
807	      {==}
808	    case 3n 0n 1n:
809	      {==}
810	    case 3n 0n 2n:
811	      {==}
812	    case 3n 0n 3n:
813	      {==}
814	    case 3n 1n 0n:
815	      {==}
816	    case 3n 1n 1n:
817	      {==}
818	    case 3n 1n 2n:
819	      {==}
820	    case 3n 1n 3n:
821	      {==}
822	    case 3n 2n 0n:
823	      {==}
824	    case 3n 2n 1n:
825	      {==}
826	    case 3n 2n 2n:
827	      {==}
828	    case 3n 2n 3n:
829	      {==}
830	    case 3n 3n 0n:
831	      {==}
832	    case 3n 3n 1n:
833	      {==}
834	    case 3n 3n 2n:
835	      {==}
836	    case 3n 3n 3n:
837	      {==}
838	    case 4n+r _ _:
839	      Empty.absurd({PH.sw(PH.sext(u(4n+r), u(b), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, ha))
840	    case 0n 4n+r _:
841	      Empty.absurd({PH.sw(PH.sext(u(0n), u(4n+r), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, hb))
842	    case 0n 0n 4n+r:
843	      Empty.absurd({PH.sw(PH.sext(u(0n), u(0n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
844	    case 0n 1n 4n+r:
845	      Empty.absurd({PH.sw(PH.sext(u(0n), u(1n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
846	    case 0n 2n 4n+r:
847	      Empty.absurd({PH.sw(PH.sext(u(0n), u(2n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
848	    case 0n 3n 4n+r:
849	      Empty.absurd({PH.sw(PH.sext(u(0n), u(3n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
850	    case 1n 4n+r _:
851	      Empty.absurd({PH.sw(PH.sext(u(1n), u(4n+r), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, hb))
852	    case 1n 0n 4n+r:
853	      Empty.absurd({PH.sw(PH.sext(u(1n), u(0n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
854	    case 1n 1n 4n+r:
855	      Empty.absurd({PH.sw(PH.sext(u(1n), u(1n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
856	    case 1n 2n 4n+r:
857	      Empty.absurd({PH.sw(PH.sext(u(1n), u(2n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
858	    case 1n 3n 4n+r:
859	      Empty.absurd({PH.sw(PH.sext(u(1n), u(3n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
860	    case 2n 4n+r _:
861	      Empty.absurd({PH.sw(PH.sext(u(2n), u(4n+r), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, hb))
862	    case 2n 0n 4n+r:
863	      Empty.absurd({PH.sw(PH.sext(u(2n), u(0n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
864	    case 2n 1n 4n+r:
865	      Empty.absurd({PH.sw(PH.sext(u(2n), u(1n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
866	    case 2n 2n 4n+r:
867	      Empty.absurd({PH.sw(PH.sext(u(2n), u(2n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
868	    case 2n 3n 4n+r:
869	      Empty.absurd({PH.sw(PH.sext(u(2n), u(3n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
870	    case 3n 4n+r _:
871	      Empty.absurd({PH.sw(PH.sext(u(3n), u(4n+r), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, hb))
872	    case 3n 0n 4n+r:
873	      Empty.absurd({PH.sw(PH.sext(u(3n), u(0n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
874	    case 3n 1n 4n+r:
875	      Empty.absurd({PH.sw(PH.sext(u(3n), u(1n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
876	    case 3n 2n 4n+r:
877	      Empty.absurd({PH.sw(PH.sext(u(3n), u(2n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
878	    case 3n 3n 4n+r:
879	      Empty.absurd({PH.sw(PH.sext(u(3n), u(3n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
880	
881	def sw_eq(+x: U32, +y: U32, +z: U32, +hx: {Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool}, +hy: {Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool}, +hz: {Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool}) -> {PH.sw(PH.sext(x, y, z)) == z : U32}:
882	  %LW.rt(x) : {PH.sw(PH.sext(_, y, z)) == z : U32}
883	  %LW.rt(y) : {PH.sw(PH.sext(u(U32.to_nat(x)), _, z)) == z : U32}
884	  %LW.rt(z) : {PH.sw(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)) == _ : U32}
885	  sw_eq_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)
886	
887	def sx_lt_n(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_lt(a, 4n) == True{} : Bool}, +hb: {Nat.is_lt(b, 4n) == True{} : Bool}, +hc: {Nat.is_lt(c, 4n) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(PH.sext(u(a), u(b), u(c))), 64n) == True{} : Bool}:
888	  match a b c:
889	    case 0n 0n 0n:
890	      {==}
891	    case 0n 0n 1n:
892	      {==}
893	    case 0n 0n 2n:
894	      {==}
895	    case 0n 0n 3n:
896	      {==}
897	    case 0n 1n 0n:
898	      {==}
899	    case 0n 1n 1n:
900	      {==}
901	    case 0n 1n 2n:
902	      {==}
903	    case 0n 1n 3n:
904	      {==}
905	    case 0n 2n 0n:
906	      {==}
907	    case 0n 2n 1n:
908	      {==}
909	    case 0n 2n 2n:
910	      {==}
911	    case 0n 2n 3n:
912	      {==}
913	    case 0n 3n 0n:
914	      {==}
915	    case 0n 3n 1n:
916	      {==}
917	    case 0n 3n 2n:
918	      {==}
919	    case 0n 3n 3n:
920	      {==}
921	    case 1n 0n 0n:
922	      {==}
923	    case 1n 0n 1n:
924	      {==}
925	    case 1n 0n 2n:
926	      {==}
927	    case 1n 0n 3n:
928	      {==}
929	    case 1n 1n 0n:
930	      {==}
931	    case 1n 1n 1n:
932	      {==}
933	    case 1n 1n 2n:
934	      {==}
935	    case 1n 1n 3n:
936	      {==}
937	    case 1n 2n 0n:
938	      {==}
939	    case 1n 2n 1n:
940	      {==}
941	    case 1n 2n 2n:
942	      {==}
943	    case 1n 2n 3n:
944	      {==}
945	    case 1n 3n 0n:
946	      {==}
947	    case 1n 3n 1n:
948	      {==}
949	    case 1n 3n 2n:
950	      {==}
951	    case 1n 3n 3n:
952	      {==}
953	    case 2n 0n 0n:
954	      {==}
955	    case 2n 0n 1n:
956	      {==}
957	    case 2n 0n 2n:
958	      {==}
959	    case 2n 0n 3n:
960	      {==}
961	    case 2n 1n 0n:
962	      {==}
963	    case 2n 1n 1n:
964	      {==}
965	    case 2n 1n 2n:
966	      {==}
967	    case 2n 1n 3n:
968	      {==}
969	    case 2n 2n 0n:
970	      {==}
971	    case 2n 2n 1n:
972	      {==}
973	    case 2n 2n 2n:
974	      {==}
975	    case 2n 2n 3n:
976	      {==}
977	    case 2n 3n 0n:
978	      {==}
979	    case 2n 3n 1n:
980	      {==}
981	    case 2n 3n 2n:
982	      {==}
983	    case 2n 3n 3n:
984	      {==}
985	    case 3n 0n 0n:
986	      {==}
987	    case 3n 0n 1n:
988	      {==}
989	    case 3n 0n 2n:
990	      {==}
991	    case 3n 0n 3n:
992	      {==}
993	    case 3n 1n 0n:
994	      {==}
995	    case 3n 1n 1n:
996	      {==}
997	    case 3n 1n 2n:
998	      {==}
999	    case 3n 1n 3n:
1000	      {==}
1001	    case 3n 2n 0n:
1002	      {==}
1003	    case 3n 2n 1n:
1004	      {==}
1005	    case 3n 2n 2n:
1006	      {==}
1007	    case 3n 2n 3n:
1008	      {==}
1009	    case 3n 3n 0n:
1010	      {==}
1011	    case 3n 3n 1n:
1012	      {==}
1013	    case 3n 3n 2n:
1014	      {==}
1015	    case 3n 3n 3n:
1016	      {==}
1017	    case 4n+r _ _:
1018	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(4n+r), u(b), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, ha))
1019	    case 0n 4n+r _:
1020	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(4n+r), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hb))
1021	    case 0n 0n 4n+r:
1022	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(0n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1023	    case 0n 1n 4n+r:
1024	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(1n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1025	    case 0n 2n 4n+r:
1026	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(2n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1027	    case 0n 3n 4n+r:
1028	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(3n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1029	    case 1n 4n+r _:
1030	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(4n+r), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hb))
1031	    case 1n 0n 4n+r:
1032	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(0n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1033	    case 1n 1n 4n+r:
1034	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(1n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1035	    case 1n 2n 4n+r:
1036	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(2n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1037	    case 1n 3n 4n+r:
1038	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(3n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1039	    case 2n 4n+r _:
1040	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(4n+r), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hb))
1041	    case 2n 0n 4n+r:
1042	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(0n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1043	    case 2n 1n 4n+r:
1044	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(1n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1045	    case 2n 2n 4n+r:
1046	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(2n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1047	    case 2n 3n 4n+r:
1048	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(3n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1049	    case 3n 4n+r _:
1050	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(4n+r), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hb))
1051	    case 3n 0n 4n+r:
1052	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(0n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1053	    case 3n 1n 4n+r:
1054	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(1n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1055	    case 3n 2n 4n+r:
1056	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(2n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1057	    case 3n 3n 4n+r:
1058	      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(3n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
1059	
1060	def sx_lt(+x: U32, +y: U32, +z: U32, +hx: {Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool}, +hy: {Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool}, +hz: {Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(PH.sext(x, y, z)), 64n) == True{} : Bool}:
1061	  %LW.rt(x) : {Nat.is_lt(U32.to_nat(PH.sext(_, y, z)), 64n) == True{} : Bool}
1062	  %LW.rt(y) : {Nat.is_lt(U32.to_nat(PH.sext(u(U32.to_nat(x)), _, z)), 64n) == True{} : Bool}
1063	  %LW.rt(z) : {Nat.is_lt(U32.to_nat(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)), 64n) == True{} : Bool}
1064	  sx_lt_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)
1065	
1066	# ---------------------------------------------------------------- base64
1067	
1068	def b64_rt(+bs: List<&2, U32>, +h: {ok(bs) == True{} : Bool}) -> {PH.unb64(PH.b64(bs)) == Some{bs} : Maybe<&2, List<&2, U32>>}:
1069	  match bs:
1070	    case Nil{}:
1071	      {==}
1072	    case +a <> Nil{}:
1073	      +ha = ok_head(a, Nil{}, h)
1074	      +ta = ok_tail(a, Nil{}, h)
1075	      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)))), Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, digit_value(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {PH.dec2(_, PH.value(PH.digit(PH.sext(PH.c0(a), 0, 0)))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1076	      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c0(a), 0, 0))), Some{PH.sext(PH.c0(a), 0, 0)}, digit_value(PH.sext(PH.c0(a), 0, 0), sx_lt(PH.c0(a), 0, 0, c0_lt(a), {==}, {==}))) : {PH.dec2(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, _) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1077	      %Equal.sym(U32, PH.su(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c3(a), su_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec2_fin(PH.byte_of(_, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), 0, 0))), Bool.and(U32.is_eq(PH.sv(PH.sext(PH.c0(a), 0, 0)), 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1078	      %Equal.sym(U32, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c2(a), sv_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec2_fin(PH.byte_of(PH.c3(a), _, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), 0, 0))), Bool.and(U32.is_eq(PH.sv(PH.sext(PH.c0(a), 0, 0)), 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1079	      %Equal.sym(U32, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c1(a), sw_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec2_fin(PH.byte_of(PH.c3(a), PH.c2(a), _, PH.su(PH.sext(PH.c0(a), 0, 0))), Bool.and(U32.is_eq(PH.sv(PH.sext(PH.c0(a), 0, 0)), 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1080	      %Equal.sym(U32, PH.su(PH.sext(PH.c0(a), 0, 0)), PH.c0(a), su_eq(PH.c0(a), 0, 0, c0_lt(a), {==}, {==})) : {PH.dec2_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), _), Bool.and(U32.is_eq(PH.sv(PH.sext(PH.c0(a), 0, 0)), 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1081	      %Equal.sym(U32, PH.sv(PH.sext(PH.c0(a), 0, 0)), 0, sv_eq(PH.c0(a), 0, 0, c0_lt(a), {==}, {==})) : {PH.dec2_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), Bool.and(U32.is_eq(_, 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1082	      %Equal.sym(U32, PH.sw(PH.sext(PH.c0(a), 0, 0)), 0, sw_eq(PH.c0(a), 0, 0, c0_lt(a), {==}, {==})) : {PH.dec2_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), Bool.and(U32.is_eq(0, 0), U32.is_eq(_, 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1083	      %Equal.sym(U32, PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), a, byte_rt(a, ha)) : {PH.dec2_fin(_, Bool.and(U32.is_eq(0, 0), U32.is_eq(0, 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
1084	      {==}
1085	    case +a <> +b <> Nil{}:
1086	      +ha = ok_head(a, b <> Nil{}, h)
1087	      +ta = ok_tail(a, b <> Nil{}, h)
1088	      +hb = ok_head(b, Nil{}, ta)
1089	      +tb = ok_tail(b, Nil{}, ta)
1090	      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)))), Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, digit_value(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {PH.dec3(_, PH.value(PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)))) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1091	      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, digit_value(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)), sx_lt(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b)))) : {PH.dec3(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, _, PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)))) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1092	      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0))), Some{PH.sext(PH.c1(b), PH.c0(b), 0)}, digit_value(PH.sext(PH.c1(b), PH.c0(b), 0), sx_lt(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==}))) : {PH.dec3(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, _) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1093	      %Equal.sym(U32, PH.su(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c3(a), su_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec3_fin(PH.byte_of(_, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1094	      %Equal.sym(U32, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c2(a), sv_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), _, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1095	      %Equal.sym(U32, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c1(a), sw_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), _, PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1096	      %Equal.sym(U32, PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c0(a), su_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), _), PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1097	      %Equal.sym(U32, PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c3(b), sv_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(_, PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1098	      %Equal.sym(U32, PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c2(b), sw_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(PH.c3(b), _, PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1099	      %Equal.sym(U32, PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.c1(b), su_eq(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==})) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(PH.c3(b), PH.c2(b), _, PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1100	      %Equal.sym(U32, PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.c0(b), sv_eq(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==})) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), _), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1101	      %Equal.sym(U32, PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0, sw_eq(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==})) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)), U32.is_eq(_, 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1102	      %Equal.sym(U32, PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), a, byte_rt(a, ha)) : {PH.dec3_fin(_, PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)), U32.is_eq(0, 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1103	      %Equal.sym(U32, PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)), b, byte_rt(b, hb)) : {PH.dec3_fin(a, _, U32.is_eq(0, 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
1104	      {==}
1105	    case +a <> +b <> +c <> +rest:
1106	      +ha = ok_head(a, b <> c <> rest, h)
1107	      +ta = ok_tail(a, b <> c <> rest, h)
1108	      +hb = ok_head(b, c <> rest, ta)
1109	      +tb = ok_tail(b, c <> rest, ta)
1110	      +hc = ok_head(c, rest, tb)
1111	      +tc = ok_tail(c, rest, tb)
1112	      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)))), Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, digit_value(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {PH.dec4(_, PH.value(PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))), PH.value(PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))), PH.unb64(PH.b64(rest))) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1113	      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, digit_value(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)), sx_lt(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b)))) : {PH.dec4(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, _, PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))), PH.value(PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))), PH.unb64(PH.b64(rest))) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1114	      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))), Some{PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))}, digit_value(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)), sx_lt(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc)))) : {PH.dec4(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, _, PH.value(PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))), PH.unb64(PH.b64(rest))) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1115	      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))), Some{PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))}, digit_value(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)), sx_lt(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c)))) : {PH.dec4(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, Some{PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))}, _, PH.unb64(PH.b64(rest))) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1116	      %Equal.sym(Maybe<&2, List<&2, U32>>, PH.unb64(PH.b64(rest)), Some{rest}, b64_rt(rest, tc)) : {PH.dec4(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, Some{PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))}, Some{PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))}, _) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1117	      %Equal.sym(U32, PH.su(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c3(a), su_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {Some{PH.byte_of(_, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))) <> PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1118	      %Equal.sym(U32, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c2(a), sv_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {Some{PH.byte_of(PH.c3(a), _, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))) <> PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1119	      %Equal.sym(U32, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c1(a), sw_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), _, PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))) <> PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1120	      %Equal.sym(U32, PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c0(a), su_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), _) <> PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1121	      %Equal.sym(U32, PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c3(b), sv_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(_, PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1122	      %Equal.sym(U32, PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c2(b), sw_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), _, PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1123	      %Equal.sym(U32, PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.c1(b), su_eq(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), _, PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1124	      %Equal.sym(U32, PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.c0(b), sv_eq(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), _) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1125	      %Equal.sym(U32, PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.c3(c), sw_eq(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(_, PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1126	      %Equal.sym(U32, PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.c2(c), su_eq(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(PH.c3(c), _, PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1127	      %Equal.sym(U32, PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.c1(c), sv_eq(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(PH.c3(c), PH.c2(c), _, PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1128	      %Equal.sym(U32, PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.c0(c), sw_eq(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(PH.c3(c), PH.c2(c), PH.c1(c), _) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1129	      %Equal.sym(U32, PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), a, byte_rt(a, ha)) : {Some{_ <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(PH.c3(c), PH.c2(c), PH.c1(c), PH.c0(c)) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1130	      %Equal.sym(U32, PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)), b, byte_rt(b, hb)) : {Some{a <> _ <> PH.byte_of(PH.c3(c), PH.c2(c), PH.c1(c), PH.c0(c)) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1131	      %Equal.sym(U32, PH.byte_of(PH.c3(c), PH.c2(c), PH.c1(c), PH.c0(c)), c, byte_rt(c, hc)) : {Some{a <> b <> _ <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
1132	      {==}
1133	
1134	# ---------------------------------------------------------------- the '$' separator
1135	
1136	# No character is '$'.
1137	def nd(s: String) -> Bool:
1138	  match s:
1139	    case SNil{}:
1140	      True{}
1141	    case SCon{c, r}:
1142	      Bool.and(Bool.not(PH.dollar(SCon{c, SNil{}})), nd(r))
1143	
1144	def dollar_cons(+c: Char, +r: String, +r2: String) -> {PH.dollar(SCon{c, r}) == PH.dollar(SCon{c, r2}) : Bool}:
1145	  match c:
1146	    case Chr{x}:
1147	      {==}
1148	
1149	def nd_head(+c: Char, +r: String, +h: {nd(SCon{c, r}) == True{} : Bool}) -> {PH.dollar(SCon{c, SNil{}}) == False{} : Bool}:
1150	  +e = L.and_left(Bool.not(PH.dollar(SCon{c, SNil{}})), nd(r), h)
1151	  L.not_true(PH.dollar(SCon{c, SNil{}}), e)
1152	
1153	def nd_tail(+c: Char, +r: String, +h: {nd(SCon{c, r}) == True{} : Bool}) -> {nd(r) == True{} : Bool}:
1154	  L.and_right(Bool.not(PH.dollar(SCon{c, SNil{}})), nd(r), h)
1155	
1156	# A string without '$', then '$': the field before it and the rest.
1157	def field_nd(+cs: String, +r: String, +h: {nd(cs) == True{} : Bool}) -> {PH.field_go(String.append(cs, SCon{Chr{36}, r}), PH.dollar(String.append(cs, SCon{Chr{36}, r}))) == Some{PH.Cut{cs, r}} : Maybe<&2, PH.Cut>}:
1158	  match cs:
1159	    case SNil{}:
1160	      {==}
1161	    case SCon{Chr{+x}, +t}:
1162	      +hd = Equal.trans(Bool, PH.dollar(SCon{Chr{x}, String.append(t, SCon{Chr{36}, r})}), PH.dollar(SCon{Chr{x}, SNil{}}), False{}, dollar_cons(Chr{x}, String.append(t, SCon{Chr{36}, r}), SNil{}), nd_head(Chr{x}, t, h))
1163	      %Equal.sym(Bool, PH.dollar(SCon{Chr{x}, String.append(t, SCon{Chr{36}, r})}), False{}, hd) : {PH.field_go(SCon{Chr{x}, String.append(t, SCon{Chr{36}, r})}, _) == Some{PH.Cut{SCon{Chr{x}, t}, r}} : Maybe<&2, PH.Cut>}
1164	      %Equal.sym(Maybe<&2, PH.Cut>, PH.field_go(String.append(t, SCon{Chr{36}, r}), PH.dollar(String.append(t, SCon{Chr{36}, r}))), Some{PH.Cut{t, r}}, field_nd(t, r, nd_tail(Chr{x}, t, h))) : {PH.field_cons(x, _) == Some{PH.Cut{SCon{Chr{x}, t}, r}} : Maybe<&2, PH.Cut>}
1165	      {==}
1166	
1167	def b64_nd(+bs: List<&2, U32>, +h: {ok(bs) == True{} : Bool}) -> {nd(PH.b64(bs)) == True{} : Bool}:
1168	  match bs:
1169	    case Nil{}:
1170	      {==}
1171	    case +a <> Nil{}:
1172	      +ha = ok_head(a, Nil{}, h)
1173	      +ta = ok_tail(a, Nil{}, h)
1174	      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), SNil{}}), False{}, no_dollar(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), 0, 0)), SNil{}})), True{})) == True{} : Bool}
1175	      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), 0, 0)), SNil{}}), False{}, no_dollar(PH.sext(PH.c0(a), 0, 0), sx_lt(PH.c0(a), 0, 0, c0_lt(a), {==}, {==}))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), True{})) == True{} : Bool}
1176	      {==}
1177	    case +a <> +b <> Nil{}:
1178	      +ha = ok_head(a, b <> Nil{}, h)
1179	      +ta = ok_tail(a, b <> Nil{}, h)
1180	      +hb = ok_head(b, Nil{}, ta)
1181	      +tb = ok_tail(b, Nil{}, ta)
1182	      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), SNil{}}), False{}, no_dollar(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), SNil{}})), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)), SNil{}})), True{}))) == True{} : Bool}
1183	      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), SNil{}}), False{}, no_dollar(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)), sx_lt(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b)))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)), SNil{}})), True{}))) == True{} : Bool}
1184	      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)), SNil{}}), False{}, no_dollar(PH.sext(PH.c1(b), PH.c0(b), 0), sx_lt(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==}))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), True{}))) == True{} : Bool}
1185	      {==}
1186	    case +a <> +b <> +c <> +rest:
1187	      +ha = ok_head(a, b <> c <> rest, h)
1188	      +ta = ok_tail(a, b <> c <> rest, h)
1189	      +hb = ok_head(b, c <> rest, ta)
1190	      +tb = ok_tail(b, c <> rest, ta)
1191	      +hc = ok_head(c, rest, tb)
1192	      +tc = ok_tail(c, rest, tb)
1193	      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), SNil{}}), False{}, no_dollar(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), SNil{}})), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), SNil{}})), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), SNil{}})), nd(PH.b64(rest)))))) == True{} : Bool}
1194	      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), SNil{}}), False{}, no_dollar(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)), sx_lt(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b)))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), SNil{}})), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), SNil{}})), nd(PH.b64(rest)))))) == True{} : Bool}
1195	      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), SNil{}}), False{}, no_dollar(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)), sx_lt(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc)))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), SNil{}})), nd(PH.b64(rest)))))) == True{} : Bool}
1196	      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), SNil{}}), False{}, no_dollar(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)), sx_lt(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c)))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), nd(PH.b64(rest)))))) == True{} : Bool}
1197	      %Equal.sym(Bool, nd(PH.b64(rest)), True{}, b64_nd(rest, tc)) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), _)))) == True{} : Bool}
1198	      {==}
1199	
1200	def field_b64(+bs: List<&2, U32>, +r: String, +h: {ok(bs) == True{} : Bool}) -> {PH.field(String.append(PH.b64(bs), SCon{Chr{36}, r})) == Some{PH.Cut{PH.b64(bs), r}} : Maybe<&2, PH.Cut>}:
1201	  field_nd(PH.b64(bs), r, b64_nd(bs, h))
1202	
1203	# ---------------------------------------------------------------- decimal
1204	
1205	def dd_n(+n: Nat, +h: {Nat.is_lt(n, 10n) == True{} : Bool}) -> {U32.to_nat(U32.sub(U32.add(48, U32.from_nat(n)), 48)) == n : Nat}:
1206	  match n:
1207	    case 0n:
1208	      {==}
1209	    case 1n:
1210	      {==}
1211	    case 2n:
1212	      {==}
1213	    case 3n:
1214	      {==}
1215	    case 4n:
1216	      {==}
1217	    case 5n:
1218	      {==}
1219	    case 6n:
1220	      {==}
1221	    case 7n:
1222	      {==}
1223	    case 8n:
1224	      {==}
1225	    case 9n:
1226	      {==}
1227	    case 10n+r:
1228	      Empty.absurd({U32.to_nat(U32.sub(U32.add(48, U32.from_nat(10n+r)), 48)) == 10n+r : Nat}, N.lt_zero_absurd(r, h))
1229	
1230	def di_n(+n: Nat, +h: {Nat.is_lt(n, 10n) == True{} : Bool}) -> {PH.is_digit(U32.add(48, U32.from_nat(n))) == True{} : Bool}:
1231	  match n:
1232	    case 0n:
1233	      {==}
1234	    case 1n:
1235	      {==}
1236	    case 2n:
1237	      {==}
1238	    case 3n:
1239	      {==}
1240	    case 4n:
1241	      {==}
1242	    case 5n:
1243	      {==}
1244	    case 6n:
1245	      {==}
1246	    case 7n:
1247	      {==}
1248	    case 8n:
1249	      {==}
1250	    case 9n:
1251	      {==}
1252	    case 10n+r:
1253	      Empty.absurd({PH.is_digit(U32.add(48, U32.from_nat(10n+r))) == True{} : Bool}, N.lt_zero_absurd(r, h))
1254	
1255	def mul10_ge(+k: Nat) -> {Nat.is_le(k, Nat.mul(k, 10n)) == True{} : Bool}:
1256	  match k:
1257	    case 0n:
1258	      {==}
1259	    case 1n+ +j:
1260	      +x = Nat.mul(j, 10n)
1261	      +h1 = N.le_trans(j, x, Nat.add(x, 9n), mul10_ge(j), N.le_add_right(x, 9n))
1262	      L.subst(Nat, z => {Nat.is_le(j, z) == True{} : Bool}, Nat.add(x, 9n), Nat.add(9n, x), N.add_comm(x, 9n), h1)
1263	
1264	# m < 9 + 10 m
1265	def lt9(+m: Nat) -> {Nat.is_lt(m, Nat.add(9n, Nat.mul(m, 10n))) == True{} : Bool}:
1266	  +x = Nat.mul(m, 10n)
1267	  +h0 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(x, 9n)) == True{} : Bool}, Nat.add(x, 0n), x, N.add_zero(x), N.lt_add_left(0n, 9n, x, {==}))
1268	  +h1 = N.le_lt_trans(m, x, Nat.add(x, 9n), mul10_ge(m), h0)
1269	  L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, Nat.add(x, 9n), Nat.add(9n, x), N.add_comm(x, 9n), h1)
1270	
1271	# n / 10 < n for n >= 1.
1272	def div10_lt(+n: Nat, +h: {Nat.is_le(1n, n) == True{} : Bool}) -> {Nat.is_lt(Nat.div(n, 10n), n) == True{} : Bool}:
1273	  match n:
1274	    case 0n:
1275	      Empty.absurd({Nat.is_lt(Nat.div(0n, 10n), 0n) == True{} : Bool}, L.false_true(h))
1276	    case 1n+ +m:
1277	      +e = NR.le_div(9n, 1n+m, 1n+m)
1278	      +f = N.lt_not_le(m, Nat.add(9n, Nat.mul(m, 10n)), lt9(m))
1279	      N.not_le_lt(1n+m, Nat.div(1n+m, 10n), Equal.trans(Bool, Nat.is_le(1n+m, Nat.div(1n+m, 10n)), Nat.is_le(Nat.mul(1n+m, 10n), 1n+m), False{}, e, f))
1280	
1281	def ge10_pos(+n: Nat, +h: {Nat.is_lt(n, 10n) == False{} : Bool}) -> {Nat.is_le(1n, n) == True{} : Bool}:
1282	  match n:
1283	    case 0n:
1284	      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, L.true_false(h))
1285	    case 1n+ +m:
1286	      N.zero_le(m)
1287	
1288	def sd_dec(+f: Nat, +n: Nat, +acc: String, +Y: String, +last: Bool, +el: {Nat.is_lt(n, 10n) == last : Bool}, +hf: {Nat.is_lt(n, f) == True{} : Bool}) -> {PH.starts_digit(String.append(PH.dec_go(f, n, acc, last), Y)) == True{} : Bool}:
1289	  match f last:
1290	    case 0n _:
1291	      Empty.absurd({PH.starts_digit(String.append(acc, Y)) == True{} : Bool}, N.lt_zero_absurd(n, hf))
1292	    case 1n+ +g True{}:
1293	      di_n(n, el)
1294	    case 1n+ +g False{}:
1295	      +q = Nat.div(n, 10n)
1296	      sd_dec(g, q, SCon{PH.dchar(Nat.mod(n, 10n)), acc}, Y, Nat.is_lt(q, 10n), {==}, N.lt_le_trans(q, n, g, div10_lt(n, ge10_pos(n, el)), N.lt_succ_le(n, g, hf)))
1297	
1298	def dec_step(+n: Nat, +ay: String, +hr: {Nat.is_lt(Nat.mod(n, 10n), 10n) == True{} : Bool}) -> {PH.read_go(SCon{PH.dchar(Nat.mod(n, 10n)), ay}, Nat.div(n, 10n), PH.starts_digit(SCon{PH.dchar(Nat.mod(n, 10n)), ay})) == PH.read_go(ay, n, PH.starts_digit(ay)) : PH.Got}:
1299	  +q = Nat.div(n, 10n)
1300	  +r = Nat.mod(n, 10n)
1301	  -rhs = PH.read_go(ay, n, PH.starts_digit(ay))
1302	  %Equal.sym(Bool, PH.is_digit(U32.add(48, U32.from_nat(r))), True{}, di_n(r, hr)) : {PH.read_go(SCon{PH.dchar(r), ay}, q, _) == rhs : PH.Got}
1303	  %Equal.sym(Nat, U32.to_nat(U32.sub(U32.add(48, U32.from_nat(r)), 48)), r, dd_n(r, hr)) : {PH.read_go(ay, Nat.add(Nat.mul(q, 10n), _), PH.starts_digit(ay)) == rhs : PH.Got}
1304	  %NR.dm_eq(9n, n) : {PH.read_go(ay, _, PH.starts_digit(ay)) == rhs : PH.Got}
1305	  {==}
1306	
1307	# Reading the decimal digits of n before acc gives n and acc.
1308	def dec_go_rt(+f: Nat, +n: Nat, +acc: String, +Y: String, +last: Bool, +el: {Nat.is_lt(n, 10n) == last : Bool}, +hf: {Nat.is_lt(n, f) == True{} : Bool}) -> {PH.read_go(String.append(PH.dec_go(f, n, acc, last), Y), 0n, True{}) == PH.read_go(String.append(acc, Y), n, PH.starts_digit(String.append(acc, Y))) : PH.Got}:
1309	  match f last:
1310	    case 0n _:
1311	      Empty.absurd({PH.read_go(String.append(acc, Y), 0n, True{}) == PH.read_go(String.append(acc, Y), n, PH.starts_digit(String.append(acc, Y))) : PH.Got}, N.lt_zero_absurd(n, hf))
1312	    case 1n+ +g True{}:
1313	      %Equal.sym(Nat, U32.to_nat(U32.sub(U32.add(48, U32.from_nat(n)), 48)), n, dd_n(n, el)) : {PH.read_go(String.append(acc, Y), _, PH.starts_digit(String.append(acc, Y))) == PH.read_go(String.append(acc, Y), n, PH.starts_digit(String.append(acc, Y))) : PH.Got}
1314	      {==}
1315	    case 1n+ +g False{}:
1316	      +q = Nat.div(n, 10n)
1317	      +r = Nat.mod(n, 10n)
1318	      +ay = String.append(acc, Y)
1319	      +hr = NR.dm_lt(9n, n)
1320	      +hq = N.lt_le_trans(q, n, g, div10_lt(n, ge10_pos(n, el)), N.lt_succ_le(n, g, hf))
1321	      -rhs = PH.read_go(ay, n, PH.starts_digit(ay))
1322	      Equal.trans(PH.Got, PH.read_go(String.append(PH.dec_go(g, q, SCon{PH.dchar(r), acc}, Nat.is_lt(q, 10n)), Y), 0n, True{}), PH.read_go(SCon{PH.dchar(r), ay}, q, PH.starts_digit(SCon{PH.dchar(r), ay})), rhs,
1323	        dec_go_rt(g, q, SCon{PH.dchar(r), acc}, Y, Nat.is_lt(q, 10n), {==}, hq),
1324	        dec_step(n, ay, hr))
1325	
1326	def got_nd(+n: Nat, +c: Char, +Y: String) -> {Some{PH.read_go(SCon{c, Y}, n, False{})} == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}:
1327	  match c:
1328	    case Chr{x}:
1329	      {==}
1330	
1331	# A decimal number followed by a non-digit is read back.
1332	def dec_rt(+n: Nat, +c: Char, +Y: String, +hc: {PH.starts_digit(SCon{c, Y}) == False{} : Bool}) -> {PH.read(String.append(PH.decimal(n), SCon{c, Y})) == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}:
1333	  +s = String.append(PH.dec_go(1n+n, n, SNil{}, Nat.is_lt(n, 10n)), SCon{c, Y})
1334	  %Equal.sym(Bool, PH.starts_digit(s), True{}, sd_dec(1n+n, n, SNil{}, SCon{c, Y}, Nat.is_lt(n, 10n), {==}, N.lt_succ(n))) : {PH.read_check(s, _) == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}
1335	  %Equal.sym(PH.Got, PH.read_go(s, 0n, True{}), PH.read_go(SCon{c, Y}, n, PH.starts_digit(SCon{c, Y})), dec_go_rt(1n+n, n, SNil{}, SCon{c, Y}, Nat.is_lt(n, 10n), {==}, N.lt_succ(n))) : {Some{_} == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}
1336	  %Equal.sym(Bool, PH.starts_digit(SCon{c, Y}), False{}, hc) : {Some{PH.read_go(SCon{c, Y}, n, _)} == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}
1337	  got_nd(n, c, Y)
1338	
1339	
1340	# ---------------------------------------------------------------- the PHC string
1341	
1342	def append_nil(+x: String) -> {String.append(x, SNil{}) == x : String}:
1343	  match x:
1344	    case SNil{}:
1345	      {==}
1346	    case SCon{+h, +t}:
1347	      Equal.cong(String, String, z => SCon{h, z}, String.append(t, SNil{}), t, append_nil(t))
1348	
1349	# parse(format(x)) == Some{x}, for byte lists of bytes below 256.
1350	def parse_format(+m: Nat, +t: Nat, +p: Nat, +salt: List<&2, U32>, +hash: List<&2, U32>, +hs: {ok(salt) == True{} : Bool}, +hh: {ok(hash) == True{} : Bool}) -> {PH.parse(PH.format(PH.Phc{m, t, p, salt, hash})) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}:
1351	  %Equal.sym(Maybe<&2, PH.Got>, PH.read(String.append(PH.decimal(m), SCon{Chr{44}, String.append("t=", String.concat([PH.decimal(t), ",p=", PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))})), Some{PH.Got{m, SCon{Chr{44}, String.append("t=", String.concat([PH.decimal(t), ",p=", PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))}}}, dec_rt(m, Chr{44}, String.append("t=", String.concat([PH.decimal(t), ",p=", PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)])), {==})) : {PH.parse_m(_) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1352	  %Equal.sym(Maybe<&2, PH.Got>, PH.read(String.append(PH.decimal(t), SCon{Chr{44}, String.append("p=", String.concat([PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))})), Some{PH.Got{t, SCon{Chr{44}, String.append("p=", String.concat([PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))}}}, dec_rt(t, Chr{44}, String.append("p=", String.concat([PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)])), {==})) : {PH.parse_t(m, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1353	  %Equal.sym(Maybe<&2, PH.Got>, PH.read(String.append(PH.decimal(p), SCon{Chr{36}, String.concat([PH.b64(salt), "$", PH.b64(hash)])})), Some{PH.Got{p, SCon{Chr{36}, String.concat([PH.b64(salt), "$", PH.b64(hash)])}}}, dec_rt(p, Chr{36}, String.concat([PH.b64(salt), "$", PH.b64(hash)]), {==})) : {PH.parse_p(m, t, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1354	  %Equal.sym(Maybe<&2, PH.Cut>, PH.field(String.append(PH.b64(salt), SCon{Chr{36}, String.concat([PH.b64(hash)])})), Some{PH.Cut{PH.b64(salt), String.concat([PH.b64(hash)])}}, field_b64(salt, String.concat([PH.b64(hash)]), hs)) : {PH.parse_salt(m, t, p, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1355	  %Equal.sym(String, String.append(PH.b64(hash), SNil{}), PH.b64(hash), append_nil(PH.b64(hash))) : {PH.parse_hash(m, t, p, PH.unb64(PH.b64(salt)), PH.unb64(_)) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1356	  %Equal.sym(Maybe<&2, List<&2, U32>>, PH.unb64(PH.b64(salt)), Some{salt}, b64_rt(salt, hs)) : {PH.parse_hash(m, t, p, _, PH.unb64(PH.b64(hash))) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1357	  %Equal.sym(Maybe<&2, List<&2, U32>>, PH.unb64(PH.b64(hash)), Some{hash}, b64_rt(hash, hh)) : {PH.parse_hash(m, t, p, Some{salt}, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
1358	  {==}