1	import Base
2	import lawful-bytes@0.1.1.0/defs.bend as D
3	import ./defs.bend as F
4	import lawful-words@0.1.0.0/proof_nat.bend as N
5	import lawful-words@0.1.0.0/proof_u32.bend as U
6	import lawful-arrays@0.1.0.0/proof_base.bend as AB
7	
8	# The laws about lists, text and decb, restated with every variable reusable
9	# (same names and statements as in LAWS.bend).
10	
11	# Lists
12	# =====
13	
14	law append_nil:
15	  for +xs: List<&2, U32>
16	  {List.append(&2, U32, xs, Nil{}) == xs : List<&2, U32>}
17	
18	def append_nil(xs):
19	  match xs:
20	    case Nil{}:
21	      {==}
22	    case Con{+x, t}:
23	      %append_nil(t) : {x <> List.append(&2, U32, t, Nil{}) == x <> _ : List<&2, U32>}
24	      {==}
25	
26	law append_assoc:
27	  for +xs: List<&2, U32>
28	  for +ys: List<&2, U32>
29	  for +zs: List<&2, U32>
30	  {List.append(&2, U32, List.append(&2, U32, xs, ys), zs) == List.append(&2, U32, xs, List.append(&2, U32, ys, zs)) : List<&2, U32>}
31	
32	def append_assoc(xs, ys, zs):
33	  match xs:
34	    case Nil{}:
35	      {==}
36	    case Con{+x, t}:
37	      %append_assoc(t, ys, zs) :
38	        {x <> List.append(&2, U32, List.append(&2, U32, t, ys), zs) == x <> _ : List<&2, U32>}
39	      {==}
40	
41	law take_zero2:
42	  for +ps: List<&2, List<&2, U32>>
43	  {List.take(&2, List<&2, U32>, ps, 0n) == Nil{} : List<&2, List<&2, U32>>}
44	
45	def take_zero2(ps):
46	  match ps:
47	    case Nil{}:
48	      {==}
49	    case Con{p, t}:
50	      {==}
51	
52	# split
53	# =====
54	
55	law sl_fin:
56	  for +x: U32
57	  for +r: List<&2, List<&2, U32>>
58	  for +b: Bool
59	  for +c: Nat
60	  for +hr: {List.length(&2, List<&2, U32>, r) == Nat.add(c, 1n) : Nat}
61	  {List.length(&2, List<&2, U32>, F.split.fin(x, r, b)) == Nat.add(F.count.if(b, c), 1n) : Nat}
62	
63	def sl_fin(x, r, b, c, hr):
64	  match r b:
65	    case Nil{} True{}:
66	      %hr : {1n+0n == 1n+_ : Nat}
67	      {==}
68	    case Nil{} False{}:
69	      Empty.absurd({1n == Nat.add(c, 1n) : Nat},
70	        AB.succ_ne_zero(c, Equal.sym(Nat, 0n, 1n+c, Equal.trans(Nat, 0n, Nat.add(c, 1n), 1n+c, hr, N.add_one(c)))))
71	    case Con{h, t} True{}:
72	      %hr : {1n+List.length(&2, List<&2, U32>, h <> t) == 1n+_ : Nat}
73	      {==}
74	    case Con{h, t} False{}:
75	      hr
76	
77	law split_length:
78	  for +xs: List<&2, U32>
79	  for +sep: U32
80	  {List.length(&2, List<&2, U32>, F.split(xs, sep)) == Nat.add(F.count(xs, sep), 1n) : Nat}
81	
82	def split_length(xs, sep):
83	  match xs:
84	    case Nil{}:
85	      {==}
86	    case Con{+x, t}:
87	      sl_fin(x, F.split(t, sep), U32.is_eq(x, sep), F.count(t, sep), split_length(t, sep))
88	
89	# join.go of the pieces of split is the separator, then their join.
90	law jg_fin:
91	  for +y: U32
92	  for +r: List<&2, List<&2, U32>>
93	  for +b: Bool
94	  for +sep: U32
95	  {F.join.go(F.split.fin(y, r, b), sep) == sep <> F.join(F.split.fin(y, r, b), sep) : List<&2, U32>}
96	
97	def jg_fin(y, r, b, sep):
98	  match r b:
99	    case Nil{} True{}:
100	      {==}
101	    case Nil{} False{}:
102	      {==}
103	    case Con{h, t} True{}:
104	      {==}
105	    case Con{h, t} False{}:
106	      {==}
107	
108	law jg:
109	  for +t: List<&2, U32>
110	  for +sep: U32
111	  {F.join.go(F.split(t, sep), sep) == sep <> F.join(F.split(t, sep), sep) : List<&2, U32>}
112	
113	def jg(t, sep):
114	  match t:
115	    case Nil{}:
116	      {==}
117	    case Con{+y, t2}:
118	      jg_fin(y, F.split(t2, sep), U32.is_eq(y, sep), sep)
119	
120	law join_push:
121	  for +x: U32
122	  for +r: List<&2, List<&2, U32>>
123	  for +sep: U32
124	  {F.join(F.split.push(x, r), sep) == x <> F.join(r, sep) : List<&2, U32>}
125	
126	def join_push(x, r, sep):
127	  match r:
128	    case Nil{}:
129	      {==}
130	    case Con{h, t}:
131	      {==}
132	
133	law sj_fin:
134	  for +x: U32
135	  for +t: List<&2, U32>
136	  for +sep: U32
137	  for +b: Bool
138	  for +hb: {U32.is_eq(x, sep) == b : Bool}
139	  for +ih: {F.join(F.split(t, sep), sep) == t : List<&2, U32>}
140	  for +hg: {F.join.go(F.split(t, sep), sep) == sep <> F.join(F.split(t, sep), sep) : List<&2, U32>}
141	  {F.join(F.split.fin(x, F.split(t, sep), b), sep) == x <> t : List<&2, U32>}
142	
143	def sj_fin(x, t, sep, b, hb, ih, hg):
144	  match b:
145	    case True{}:
146	      %Equal.sym(List<&2, U32>, F.join.go(F.split(t, sep), sep), sep <> F.join(F.split(t, sep), sep), hg) :
147	        {_ == x <> t : List<&2, U32>}
148	      %Equal.sym(List<&2, U32>, F.join(F.split(t, sep), sep), t, ih) : {sep <> _ == x <> t : List<&2, U32>}
149	      %Equal.sym(U32, x, sep, U.is_eq_true(x, sep, hb)) : {sep <> t == _ <> t : List<&2, U32>}
150	      {==}
151	    case False{}:
152	      %Equal.sym(List<&2, U32>, F.join(F.split.push(x, F.split(t, sep)), sep), x <> F.join(F.split(t, sep), sep),
153	        join_push(x, F.split(t, sep), sep)) :
154	        {_ == x <> t : List<&2, U32>}
155	      %Equal.sym(List<&2, U32>, F.join(F.split(t, sep), sep), t, ih) : {x <> _ == x <> t : List<&2, U32>}
156	      {==}
157	
158	law split_join:
159	  for +xs: List<&2, U32>
160	  for +sep: U32
161	  {F.join(F.split(xs, sep), sep) == xs : List<&2, U32>}
162	
163	def split_join(xs, sep):
164	  match xs:
165	    case Nil{}:
166	      {==}
167	    case Con{+x, t}:
168	      sj_fin(x, t, sep, U32.is_eq(x, sep), {==}, split_join(t, sep), jg(t, sep))
169	
170	# Text
171	# ====
172	
173	law text_codes:
174	  for +s: String
175	  {F.text(F.codes(s)) == s : String}
176	
177	def text_codes(s):
178	  match s:
179	    case SNil{}:
180	      {==}
181	    case SCon{Chr{x}, t}:
182	      %text_codes(t) : {SCon{Chr{x}, F.text(F.codes(t))} == SCon{Chr{x}, _} : String}
183	      {==}
184	
185	law st_fin:
186	  for +x: U32
187	  for +r: List<&2, List<&2, U32>>
188	  for +b: Bool
189	  {String.split.fin(Chr{x}, F.texts(r), b) == F.texts(F.split.fin(x, r, b)) : List<&2, String>}
190	
191	def st_fin(x, r, b):
192	  match r b:
193	    case Nil{} True{}:
194	      {==}
195	    case Nil{} False{}:
196	      {==}
197	    case Con{h, t} True{}:
198	      {==}
199	    case Con{h, t} False{}:
200	      {==}
201	
202	law split_text:
203	  for +xs: List<&2, U32>
204	  for +sep: U32
205	  {String.split(F.text(xs), Chr{sep}) == F.texts(F.split(xs, sep)) : List<&2, String>}
206	
207	def split_text(xs, sep):
208	  match xs:
209	    case Nil{}:
210	      {==}
211	    case Con{+x, t}:
212	      %Equal.sym(List<&2, String>, String.split(F.text(t), Chr{sep}), F.texts(F.split(t, sep)), split_text(t, sep)) :
213	        {String.split.fin(Chr{x}, _, U32.is_eq(x, sep)) == F.texts(F.split.fin(x, F.split(t, sep), U32.is_eq(x, sep))) : List<&2, String>}
214	      st_fin(x, F.split(t, sep), U32.is_eq(x, sep))
215	
216	law text_app:
217	  for +a: List<&2, U32>
218	  for +b: List<&2, U32>
219	  {F.text(List.append(&2, U32, a, b)) == String.append(F.text(a), F.text(b)) : String}
220	
221	def text_app(a, b):
222	  match a:
223	    case Nil{}:
224	      {==}
225	    case Con{+x, t}:
226	      %text_app(t, b) : {SCon{Chr{x}, F.text(List.append(&2, U32, t, b))} == SCon{Chr{x}, _} : String}
227	      {==}
228	
229	law jt:
230	  for +t: List<&2, List<&2, U32>>
231	  for +p: List<&2, U32>
232	  for +sep: U32
233	  {F.text(List.append(&2, U32, p, F.join.go(t, sep))) == String.join.go(F.texts(t), F.text(p), F.text([sep])) : String}
234	
235	def jt(t, p, sep):
236	  match t:
237	    case Nil{}:
238	      %Equal.sym(List<&2, U32>, List.append(&2, U32, p, Nil{}), p, append_nil(p)) : {F.text(_) == F.text(p) : String}
239	      {==}
240	    case Con{+h2, t2}:
241	      +X = {sep <> List.append(&2, U32, h2, F.join.go(t2, sep)) : List<&2, U32>}
242	      %Equal.sym(String, F.text(List.append(&2, U32, p, X)), String.append(F.text(p), F.text(X)), text_app(p, X)) :
243	        {_ == String.join.go(F.texts(h2 <> t2), F.text(p), F.text([sep])) : String}
244	      %jt(t2, h2, sep) :
245	        {String.append(F.text(p), SCon{Chr{sep}, F.text(List.append(&2, U32, h2, F.join.go(t2, sep)))}) == String.append(F.text(p), SCon{Chr{sep}, _}) : String}
246	      {==}
247	
248	law join_text:
249	  for +ps: List<&2, List<&2, U32>>
250	  for +sep: U32
251	  {F.text(F.join(ps, sep)) == String.join(F.texts(ps), F.text([sep])) : String}
252	
253	def join_text(ps, sep):
254	  match ps:
255	    case Nil{}:
256	      {==}
257	    case Con{p, t}:
258	      jt(t, p, sep)
259	
260	# Joining at piece k
261	# ==================
262	
263	law ja0:
264	  for +q: List<&2, U32>
265	  for +t2: List<&2, List<&2, U32>>
266	  for +sep: U32
267	  for +h: {Nat.is_lt(1n, List.length(&2, List<&2, U32>, q <> t2)) == True{} : Bool}
268	  {F.join.go(q <> t2, sep) == List.append(&2, U32, F.join.go(List.take(&2, List<&2, U32>, q <> t2, 1n), sep), sep <> F.join(List.drop(&2, List<&2, U32>, q <> t2, 1n), sep)) : List<&2, U32>}
269	
270	def ja0(q, t2, sep, h):
271	  match t2:
272	    case Nil{}:
273	      Empty.absurd({F.join.go([q], sep) == List.append(&2, U32, F.join.go([q], sep), [sep]) : List<&2, U32>}, AB.false_ne_true(h))
274	    case Con{+r, t3}:
275	      +Z = {sep <> List.append(&2, U32, r, F.join.go(t3, sep)) : List<&2, U32>}
276	      %Equal.sym(List<&2, U32>, List.append(&2, U32, q, Nil{}), q, append_nil(q)) :
277	        {sep <> List.append(&2, U32, q, Z) == sep <> List.append(&2, U32, _, Z) : List<&2, U32>}
278	      {==}
279	
280	law ja_go:
281	  for +t: List<&2, List<&2, U32>>
282	  for +sep: U32
283	  for +k: Nat
284	  for +h: {Nat.is_lt(Nat.add(k, 1n), List.length(&2, List<&2, U32>, t)) == True{} : Bool}
285	  {F.join.go(t, sep) == List.append(&2, U32, F.join.go(List.take(&2, List<&2, U32>, t, Nat.add(k, 1n)), sep), sep <> F.join(List.drop(&2, List<&2, U32>, t, Nat.add(k, 1n)), sep)) : List<&2, U32>}
286	
287	def ja_go(t, sep, k, h):
288	  match t k:
289	    case Nil{} _:
290	      Empty.absurd({F.join.go(Nil{}, sep) == List.append(&2, U32, F.join.go(List.take(&2, List<&2, U32>, Nil{}, Nat.add(k, 1n)), sep), sep <> F.join(List.drop(&2, List<&2, U32>, Nil{}, Nat.add(k, 1n)), sep)) : List<&2, U32>},
291	        AB.lt_zero_absurd(Nat.add(k, 1n), h))
292	    case Con{+q, t2} 0n:
293	      ja0(q, t2, sep, h)
294	    case Con{+q, t2} 1n+k2:
295	      +JT = F.join.go(List.take(&2, List<&2, U32>, t2, Nat.add(k2, 1n)), sep)
296	      +Z = {sep <> F.join(List.drop(&2, List<&2, U32>, t2, Nat.add(k2, 1n)), sep) : List<&2, U32>}
297	      %Equal.sym(List<&2, U32>, F.join.go(t2, sep), List.append(&2, U32, JT, Z), ja_go(t2, sep, k2, h)) :
298	        {sep <> List.append(&2, U32, q, _) == sep <> List.append(&2, U32, List.append(&2, U32, q, JT), Z) : List<&2, U32>}
299	      %Equal.sym(List<&2, U32>, List.append(&2, U32, List.append(&2, U32, q, JT), Z), List.append(&2, U32, q, List.append(&2, U32, JT, Z)), append_assoc(q, JT, Z)) :
300	        {sep <> List.append(&2, U32, q, List.append(&2, U32, JT, Z)) == sep <> _ : List<&2, U32>}
301	      {==}
302	
303	law jat0:
304	  for +p: List<&2, U32>
305	  for +t: List<&2, List<&2, U32>>
306	  for +sep: U32
307	  for +h: {Nat.is_lt(1n, List.length(&2, List<&2, U32>, p <> t)) == True{} : Bool}
308	  {F.join(p <> t, sep) == List.append(&2, U32, F.join(List.take(&2, List<&2, U32>, p <> t, 1n), sep), sep <> F.join(List.drop(&2, List<&2, U32>, p <> t, 1n), sep)) : List<&2, U32>}
309	
310	def jat0(p, t, sep, h):
311	  match t:
312	    case Nil{}:
313	      Empty.absurd({F.join([p], sep) == List.append(&2, U32, F.join([p], sep), [sep]) : List<&2, U32>}, AB.false_ne_true(h))
314	    case Con{+r, t3}:
315	      +Z = {sep <> List.append(&2, U32, r, F.join.go(t3, sep)) : List<&2, U32>}
316	      %Equal.sym(List<&2, U32>, List.append(&2, U32, p, Nil{}), p, append_nil(p)) :
317	        {List.append(&2, U32, p, Z) == List.append(&2, U32, _, Z) : List<&2, U32>}
318	      {==}
319	
320	law join_at:
321	  for +ps: List<&2, List<&2, U32>>
322	  for +sep: U32
323	  for +k: Nat
324	  for +h: {Nat.is_lt(Nat.add(k, 1n), List.length(&2, List<&2, U32>, ps)) == True{} : Bool}
325	  {F.join(ps, sep) == List.append(&2, U32, F.join(List.take(&2, List<&2, U32>, ps, Nat.add(k, 1n)), sep), Con{sep, F.join(List.drop(&2, List<&2, U32>, ps, Nat.add(k, 1n)), sep)}) : List<&2, U32>}
326	
327	def join_at(ps, sep, k, h):
328	  match ps k:
329	    case Nil{} _:
330	      Empty.absurd({F.join(Nil{}, sep) == List.append(&2, U32, F.join(List.take(&2, List<&2, U32>, Nil{}, Nat.add(k, 1n)), sep), sep <> F.join(List.drop(&2, List<&2, U32>, Nil{}, Nat.add(k, 1n)), sep)) : List<&2, U32>},
331	        AB.lt_zero_absurd(Nat.add(k, 1n), h))
332	    case Con{+p, t} 0n:
333	      jat0(p, t, sep, h)
334	    case Con{+p, t} 1n+k2:
335	      +JT = F.join.go(List.take(&2, List<&2, U32>, t, Nat.add(k2, 1n)), sep)
336	      +Z = {sep <> F.join(List.drop(&2, List<&2, U32>, t, Nat.add(k2, 1n)), sep) : List<&2, U32>}
337	      %Equal.sym(List<&2, U32>, F.join.go(t, sep), List.append(&2, U32, JT, Z), ja_go(t, sep, k2, h)) :
338	        {List.append(&2, U32, p, _) == List.append(&2, U32, List.append(&2, U32, p, JT), Z) : List<&2, U32>}
339	      %Equal.sym(List<&2, U32>, List.append(&2, U32, List.append(&2, U32, p, JT), Z), List.append(&2, U32, p, List.append(&2, U32, JT, Z)), append_assoc(p, JT, Z)) :
340	        {List.append(&2, U32, p, List.append(&2, U32, JT, Z)) == _ : List<&2, U32>}
341	      {==}
342	
343	# Ends
344	# ====
345	
346	law ends_arith:
347	  for +from: Nat
348	  for +lp: Nat
349	  for +lj: Nat
350	  {Nat.add(Nat.add(Nat.add(from, lp), 1n), lj) == Nat.add(from, Nat.add(lp, 1n+lj)) : Nat}
351	
352	def ends_arith(from, lp, lj):
353	  %Equal.sym(Nat, Nat.add(Nat.add(from, lp), 1n), 1n+Nat.add(from, lp), N.add_one(Nat.add(from, lp))) :
354	    {Nat.add(_, lj) == Nat.add(from, Nat.add(lp, 1n+lj)) : Nat}
355	  %Equal.sym(Nat, Nat.add(lp, 1n+lj), 1n+Nat.add(lp, lj), N.add_succ(lp, lj)) :
356	    {Nat.add(1n+Nat.add(from, lp), lj) == Nat.add(from, _) : Nat}
357	  %Equal.sym(Nat, Nat.add(from, 1n+Nat.add(lp, lj)), 1n+Nat.add(from, Nat.add(lp, lj)), N.add_succ(from, Nat.add(lp, lj))) :
358	    {Nat.add(1n+Nat.add(from, lp), lj) == _ : Nat}
359	  %N.add_assoc(from, lp, lj) : {1n+Nat.add(Nat.add(from, lp), lj) == 1n+_ : Nat}
360	  {==}
361	
362	# One step of ej, with the induction hypothesis for the rest (t is not empty).
363	law ej_step:
364	  for +p: List<&2, U32>
365	  for +t: List<&2, List<&2, U32>>
366	  for +sep: U32
367	  for +from: Nat
368	  for +k2: Nat
369	  for +h: {Nat.is_lt(1n+k2, List.length(&2, List<&2, U32>, p <> t)) == True{} : Bool}
370	  for +ih: {List.get(&2, Nat, F.ends(t, Nat.add(Nat.add(from, List.length(&2, U32, p)), 1n)), k2) == Some{Nat.add(Nat.add(Nat.add(from, List.length(&2, U32, p)), 1n), List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, t, 1n+k2), sep)))} : Maybe<&2, Nat>}
371	  {List.get(&2, Nat, F.ends(p <> t, from), 1n+k2) == Some{Nat.add(from, List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, p <> t, 1n+1n+k2), sep)))} : Maybe<&2, Nat>}
372	
373	def ej_step(p, t, sep, from, k2, h, ih):
374	  match t:
375	    case Nil{}:
376	      Empty.absurd({List.get(&2, Nat, F.ends([p], from), 1n+k2) == Some{Nat.add(from, List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, [p], 1n+1n+k2), sep)))} : Maybe<&2, Nat>}, AB.lt_zero_absurd(k2, h))
377	    case Con{+q, t2}:
378	      +lp = List.length(&2, U32, p)
379	      +f1 = Nat.add(Nat.add(from, lp), 1n)
380	      +J = F.join(List.take(&2, List<&2, U32>, q <> t2, 1n+k2), sep)
381	      +RHS = {Some{Nat.add(from, List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, p <> q <> t2, 1n+1n+k2), sep)))} : Maybe<&2, Nat>}
382	      %Equal.sym(Maybe<&2, Nat>, List.get(&2, Nat, F.ends(q <> t2, f1), k2), Some{Nat.add(f1, List.length(&2, U32, J))}, ih) :
383	        {_ == RHS : Maybe<&2, Nat>}
384	      %Equal.sym(Nat, List.length(&2, U32, List.append(&2, U32, p, sep <> J)), Nat.add(lp, List.length(&2, U32, sep <> J)),
385	        AB.length_append(U32, p, sep <> J)) :
386	        {Some{Nat.add(f1, List.length(&2, U32, J))} == Some{Nat.add(from, _)} : Maybe<&2, Nat>}
387	      %ends_arith(from, lp, List.length(&2, U32, J)) :
388	        {Some{Nat.add(f1, List.length(&2, U32, J))} == Some{_} : Maybe<&2, Nat>}
389	      {==}
390	
391	law ej:
392	  for +ps: List<&2, List<&2, U32>>
393	  for +sep: U32
394	  for +from: Nat
395	  for +k: Nat
396	  for +h: {Nat.is_lt(k, List.length(&2, List<&2, U32>, ps)) == True{} : Bool}
397	  {List.get(&2, Nat, F.ends(ps, from), k) == Some{Nat.add(from, List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, ps, 1n+k), sep)))} : Maybe<&2, Nat>}
398	
399	def ej(ps, sep, from, k, h):
400	  match ps k:
401	    case Nil{} _:
402	      Empty.absurd({List.get(&2, Nat, F.ends(Nil{}, from), k) == Some{Nat.add(from, 0n)} : Maybe<&2, Nat>}, AB.lt_zero_absurd(k, h))
403	    case Con{+p, t} 0n:
404	      %Equal.sym(List<&2, List<&2, U32>>, List.take(&2, List<&2, U32>, t, 0n), Nil{}, take_zero2(t)) :
405	        {Some{Nat.add(from, List.length(&2, U32, p))} == Some{Nat.add(from, List.length(&2, U32, F.join(p <> _, sep)))} : Maybe<&2, Nat>}
406	      %Equal.sym(List<&2, U32>, List.append(&2, U32, p, Nil{}), p, append_nil(p)) :
407	        {Some{Nat.add(from, List.length(&2, U32, p))} == Some{Nat.add(from, List.length(&2, U32, _))} : Maybe<&2, Nat>}
408	      {==}
409	    case Con{+p, t} 1n+k2:
410	      ej_step(p, t, sep, from, k2, h, ej(t, sep, Nat.add(Nat.add(from, List.length(&2, U32, p)), 1n), k2, h))
411	
412	law ends_join:
413	  for +ps: List<&2, List<&2, U32>>
414	  for +sep: U32
415	  for +from: Nat
416	  for +k: Nat
417	  for +h: {Nat.is_lt(k, List.length(&2, List<&2, U32>, ps)) == True{} : Bool}
418	  {List.get(&2, Nat, F.ends(ps, from), k) == Some{Nat.add(from, List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, ps, Nat.add(k, 1n)), sep)))} : Maybe<&2, Nat>}
419	
420	def ends_join(ps, sep, from, k, h):
421	  %Equal.sym(Nat, Nat.add(k, 1n), 1n+k, N.add_one(k)) :
422	    {List.get(&2, Nat, F.ends(ps, from), k) == Some{Nat.add(from, List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, ps, _), sep)))} : Maybe<&2, Nat>}
423	  ej(ps, sep, from, k, h)
424	
425	law pieces_length:
426	  for +es: List<&2, U32>
427	  for +xs: List<&2, U32>
428	  for +from: Nat
429	  {List.length(&2, List<&2, U32>, F.pieces(es, xs, from)) == List.length(&2, U32, es) : Nat}
430	
431	def pieces_length(es, xs, from):
432	  match es:
433	    case Nil{}:
434	      {==}
435	    case Con{+e, t}:
436	      %pieces_length(t, xs, Nat.add(U32.to_nat(e), 1n)) :
437	        {1n+List.length(&2, List<&2, U32>, F.pieces(t, xs, Nat.add(U32.to_nat(e), 1n))) == 1n+_ : Nat}
438	      {==}
439	
440	# decb
441	# ====
442	
443	# 2^32 must never take part in a conversion (the checker would expand it), so
444	# the bound stays a variable M and the law instantiates it.
445	def decb_if(+n: Nat, b: Bool, hb: {b == True{} : Bool}) -> {F.decb.if(n, b) == Some{n} : Maybe<&2, Nat>}:
446	  match b:
447	    case True{}:
448	      {==}
449	    case False{}:
450	      Empty.absurd({F.decb.if(n, False{}) == Some{n} : Maybe<&2, Nat>}, AB.false_ne_true(hb))
451	
452	law decb_fits_m:
453	  for +xs: List<&2, U32>
454	  for +n: Nat
455	  for +m: Nat
456	  for +h: {F.dec(xs) == Some{n} : Maybe<&2, Nat>}
457	  for +hn: {Nat.is_lt(n, m) == True{} : Bool}
458	  {F.decb(xs, m) == Some{n} : Maybe<&2, Nat>}
459	
460	def decb_fits_m(xs, n, m, h, hn):
461	  %Equal.sym(Maybe<&2, Nat>, F.dec(xs), Some{n}, h) : {F.decb.of(_, m) == Some{n} : Maybe<&2, Nat>}
462	  decb_if(n, Nat.is_lt(n, m), hn)
463	
464	law decb_fits:
465	  for +xs: List<&2, U32>
466	  for +n: Nat
467	  for +h: {F.dec(xs) == Some{n} : Maybe<&2, Nat>}
468	  for +hn: {Nat.is_lt(n, Nat.pow(2n, 32n)) == True{} : Bool}
469	  {F.decb(xs, Nat.pow(2n, 32n)) == Some{n} : Maybe<&2, Nat>}
470	
471	def decb_fits(xs, n, h, hn):
472	  decb_fits_m(xs, n, Nat.pow(2n, 32n), h, hn)