1	import Base
2	import lawful-bytes@0.1.1.0/defs.bend as D
3	import lawful-bytes@0.1.1.0/bytes.bend as B
4	import ./defs.bend as F
5	import ./fields.bend as K
6	import lawful-bytes@0.1.1.0/proof_seq.bend as S
7	import lawful-bytes@0.1.1.0/proof_core.bend as C
8	import lawful-bytes@0.1.1.0/proof_ops.bend as O
9	import lawful-bytes@0.1.1.0/proof_list.bend as Q
10	import lawful-bytes@0.1.1.0/proof_append.bend as X
11	import lawful-bytes@0.1.1.0/proof_shift.bend as H
12	import lawful-bytes@0.1.1.0/proof_find.bend as FI
13	import lawful-words@0.1.0.0/proof_nat.bend as N
14	import lawful-words@0.1.0.0/proof_u32.bend as U
15	import lawful-arrays@0.1.0.0/proof_base.bend as AB
16	import lawful-arrays@0.1.0.0/proof_tree.bend as P
17	
18	# cut on the mirror C.BT(len, t) (lawful-bytes). CG mirrors cut.go as a Data
19	# function (cg_eq), so the laws are about CG. split is described by run_len
20	# (sp1, sp2): the first piece ends at the first separator. The ends of
21	# split(ys) from s determine its pieces (pb) and lie in s .. s + length(ys) (wl).
22	
23	# Nat and list facts
24	# ==================
25	
26	law tz:
27	  for -A: Data
28	  for +xs: List<&2, A>
29	  {List.take(&2, A, xs, 0n) == Nil{} : List<&2, A>}
30	
31	def tz(A, xs):
32	  match xs:
33	    case Nil{}:
34	      {==}
35	    case Con{x, t}:
36	      {==}
37	
38	def is_nil_t(xs: List<&2, U32>) -> Type:
39	  match xs:
40	    case Nil{}:
41	      Unit
42	    case Con{x, t}:
43	      Empty
44	
45	law nil_cons:
46	  for -x: U32
47	  for -t: List<&2, U32>
48	  for e: {Nil{} == x <> t : List<&2, U32>}
49	  Empty
50	
51	def nil_cons(x, t, e):
52	  %e : is_nil_t(_)
53	  Unit{}
54	
55	law le_antisym:
56	  for +a: Nat
57	  for +b: Nat
58	  for +h1: {Nat.is_le(a, b) == True{} : Bool}
59	  for +h2: {Nat.is_le(b, a) == True{} : Bool}
60	  {a == b : Nat}
61	
62	def le_antisym(a, b, h1, h2):
63	  match a b:
64	    case 0n 0n:
65	      {==}
66	    case 0n 1n+q:
67	      Empty.absurd({0n == 1n+q : Nat}, AB.false_ne_true(h2))
68	    case 1n+p 0n:
69	      Empty.absurd({1n+p == 0n : Nat}, AB.false_ne_true(h1))
70	    case 1n+p 1n+q:
71	      %le_antisym(p, q, h1, h2) : {1n+p == 1n+_ : Nat}
72	      {==}
73	
74	# T <= s + r gives T - s <= r.
75	law sub_le_of:
76	  for +tt: Nat
77	  for +s: Nat
78	  for +r: Nat
79	  for +h: {Nat.is_le(tt, Nat.add(s, r)) == True{} : Bool}
80	  {Nat.is_le(Nat.sub(tt, s), r) == True{} : Bool}
81	
82	def sub_le_of(tt, s, r, h):
83	  match tt s:
84	    case 0n _:
85	      N.le_zero_l(r)
86	    case 1n+p 0n:
87	      h
88	    case 1n+p 1n+q:
89	      sub_le_of(p, q, r, h)
90	
91	# s + r < T gives r < T - s.
92	law lt_sub_of:
93	  for +s: Nat
94	  for +r: Nat
95	  for +tt: Nat
96	  for +h: {Nat.is_lt(Nat.add(s, r), tt) == True{} : Bool}
97	  {Nat.is_lt(r, Nat.sub(tt, s)) == True{} : Bool}
98	
99	def lt_sub_of(s, r, tt, h):
100	  +h1 = Equal.trans(Bool, Nat.is_le(1n+Nat.add(s, r), tt), Nat.is_lt(Nat.add(s, r), tt), True{}, N.le_succ_lt(Nat.add(s, r), tt), h)
101	  +h2 = AB.subst(Nat, y => {Nat.is_le(y, tt) == True{} : Bool}, 1n+Nat.add(s, r), Nat.add(s, 1n+r),
102	    Equal.sym(Nat, Nat.add(s, 1n+r), 1n+Nat.add(s, r), N.add_succ(s, r)), h1)
103	  Equal.trans(Bool, Nat.is_lt(r, Nat.sub(tt, s)), Nat.is_le(1n+r, Nat.sub(tt, s)), True{},
104	    Equal.sym(Bool, Nat.is_le(1n+r, Nat.sub(tt, s)), Nat.is_lt(r, Nat.sub(tt, s)), N.le_succ_lt(r, Nat.sub(tt, s))),
105	    N.le_sub_r(s, 1n+r, tt, h2))
106	
107	law sub_mono:
108	  for +a: Nat
109	  for +b: Nat
110	  for +c: Nat
111	  for +h: {Nat.is_le(a, b) == True{} : Bool}
112	  {Nat.is_le(Nat.sub(a, c), Nat.sub(b, c)) == True{} : Bool}
113	
114	def sub_mono(a, b, c, h):
115	  match a b c:
116	    case 0n _ _:
117	      N.le_zero_l(Nat.sub(b, c))
118	    case 1n+p 0n _:
119	      Empty.absurd({Nat.is_le(Nat.sub(1n+p, c), 0n) == True{} : Bool}, AB.false_ne_true(h))
120	    case 1n+p 1n+q 0n:
121	      h
122	    case 1n+p 1n+q 1n+r:
123	      sub_mono(p, q, r, h)
124	
125	law sub_sub:
126	  for +tt: Nat
127	  for +s: Nat
128	  for +k: Nat
129	  {Nat.sub(Nat.sub(tt, s), k) == Nat.sub(tt, Nat.add(s, k)) : Nat}
130	
131	def sub_sub(tt, s, k):
132	  match tt s:
133	    case 0n _:
134	      {==}
135	    case 1n+p 0n:
136	      {==}
137	    case 1n+p 1n+q:
138	      sub_sub(p, q, k)
139	
140	law drop_drop:
141	  for +xs: List<&2, U32>
142	  for +a: Nat
143	  for +b: Nat
144	  {List.drop(&2, U32, List.drop(&2, U32, xs, a), b) == List.drop(&2, U32, xs, Nat.add(a, b)) : List<&2, U32>}
145	
146	def drop_drop(xs, a, b):
147	  match xs a:
148	    case Nil{} _:
149	      {==}
150	    case Con{x, t} 0n:
151	      {==}
152	    case Con{x, t} 1n+p:
153	      drop_drop(t, p, b)
154	
155	law drop_take:
156	  for +zs: List<&2, U32>
157	  for +n: Nat
158	  for +k: Nat
159	  {List.drop(&2, U32, List.take(&2, U32, zs, n), k) == List.take(&2, U32, List.drop(&2, U32, zs, k), Nat.sub(n, k)) : List<&2, U32>}
160	
161	def drop_take(zs, n, k):
162	  match zs n k:
163	    case Nil{} _ _:
164	      {==}
165	    case Con{x, t} 0n 0n:
166	      {==}
167	    case Con{x, t} 0n 1n+j:
168	      Equal.sym(List<&2, U32>, List.take(&2, U32, List.drop(&2, U32, t, j), 0n), Nil{}, tz(U32, List.drop(&2, U32, t, j)))
169	    case Con{x, t} 1n+p 0n:
170	      {==}
171	    case Con{x, t} 1n+p 1n+j:
172	      drop_take(t, p, j)
173	
174	# A slice dropped by k is the slice from s + k.
175	law slice_drop:
176	  for +xs: List<&2, U32>
177	  for +s: Nat
178	  for +tt: Nat
179	  for +k: Nat
180	  {List.drop(&2, U32, D.slice(xs, s, Nat.sub(tt, s)), k) == D.slice(xs, Nat.add(s, k), Nat.sub(tt, Nat.add(s, k))) : List<&2, U32>}
181	
182	def slice_drop(xs, s, tt, k):
183	  %Equal.sym(List<&2, U32>, List.drop(&2, U32, List.take(&2, U32, List.drop(&2, U32, xs, s), Nat.sub(tt, s)), k),
184	    List.take(&2, U32, List.drop(&2, U32, List.drop(&2, U32, xs, s), k), Nat.sub(Nat.sub(tt, s), k)), drop_take(List.drop(&2, U32, xs, s), Nat.sub(tt, s), k)) :
185	    {_ == D.slice(xs, Nat.add(s, k), Nat.sub(tt, Nat.add(s, k))) : List<&2, U32>}
186	  %Equal.sym(List<&2, U32>, List.drop(&2, U32, List.drop(&2, U32, xs, s), k), List.drop(&2, U32, xs, Nat.add(s, k)), drop_drop(xs, s, k)) :
187	    {List.take(&2, U32, _, Nat.sub(Nat.sub(tt, s), k)) == D.slice(xs, Nat.add(s, k), Nat.sub(tt, Nat.add(s, k))) : List<&2, U32>}
188	  %Equal.sym(Nat, Nat.sub(Nat.sub(tt, s), k), Nat.sub(tt, Nat.add(s, k)), sub_sub(tt, s, k)) :
189	    {List.take(&2, U32, List.drop(&2, U32, xs, Nat.add(s, k)), _) == D.slice(xs, Nat.add(s, k), Nat.sub(tt, Nat.add(s, k))) : List<&2, U32>}
190	  {==}
191	
192	# split by run_len
193	# ================
194	
195	def nn(ps: List<&2, List<&2, U32>>) -> Bool:
196	  match ps:
197	    case Nil{}:
198	      False{}
199	    case Con{p, t}:
200	      True{}
201	
202	law nn_push:
203	  for +c: U32
204	  for +ps: List<&2, List<&2, U32>>
205	  {nn(F.split.push(c, ps)) == True{} : Bool}
206	
207	def nn_push(c, ps):
208	  match ps:
209	    case Nil{}:
210	      {==}
211	    case Con{p, t}:
212	      {==}
213	
214	law nn_fin:
215	  for +c: U32
216	  for +ps: List<&2, List<&2, U32>>
217	  for +b: Bool
218	  {nn(F.split.fin(c, ps, b)) == True{} : Bool}
219	
220	def nn_fin(c, ps, b):
221	  match b:
222	    case False{}:
223	      nn_push(c, ps)
224	    case True{}:
225	      {==}
226	
227	law split_nn:
228	  for +xs: List<&2, U32>
229	  for +sep: U32
230	  {nn(F.split(xs, sep)) == True{} : Bool}
231	
232	def split_nn(xs, sep):
233	  match xs:
234	    case Nil{}:
235	      {==}
236	    case Con{+x, t}:
237	      nn_fin(x, F.split(t, sep), U32.is_eq(x, sep))
238	
239	law sp1c:
240	  for +x: U32
241	  for +t: List<&2, U32>
242	  for +sep: U32
243	  for +b: Bool
244	  for +hb: {U32.is_eq(x, sep) == b : Bool}
245	  for +h: {Nat.is_lt(D.run_len(x <> t, sep), List.length(&2, U32, x <> t)) == True{} : Bool}
246	  for ih: {Nat.is_lt(D.run_len(t, sep), List.length(&2, U32, t)) == True{} : Bool} -> {F.split(t, sep) == List.take(&2, U32, t, D.run_len(t, sep)) <> F.split(List.drop(&2, U32, t, Nat.add(D.run_len(t, sep), 1n)), sep) : List<&2, List<&2, U32>>}
247	  {F.split(x <> t, sep) == List.take(&2, U32, x <> t, D.run_len(x <> t, sep)) <> F.split(List.drop(&2, U32, x <> t, Nat.add(D.run_len(x <> t, sep), 1n)), sep) : List<&2, List<&2, U32>>}
248	
249	def sp1c(x, t, sep, b, hb, h, ih):
250	  match b:
251	    case True{}:
252	      +R = Nat.add(1n, D.run_len(t, sep))
253	      %Equal.sym(Bool, U32.is_eq(x, sep), True{}, hb) :
254	        {F.split.fin(x, F.split(t, sep), _) == List.take(&2, U32, x <> t, Bool.pick(Nat, _, 0n, R)) <> F.split(List.drop(&2, U32, x <> t, Nat.add(Bool.pick(Nat, _, 0n, R), 1n)), sep) : List<&2, List<&2, U32>>}
255	      %Equal.sym(List<&2, U32>, List.drop(&2, U32, t, 0n), t, X.drop_zero(t)) : {Nil{} <> F.split(t, sep) == Nil{} <> F.split(_, sep) : List<&2, List<&2, U32>>}
256	      {==}
257	    case False{}:
258	      +r = D.run_len(t, sep)
259	      +R = Nat.add(1n, r)
260	      %Equal.sym(Bool, U32.is_eq(x, sep), False{}, hb) :
261	        {F.split.fin(x, F.split(t, sep), _) == List.take(&2, U32, x <> t, Bool.pick(Nat, _, 0n, R)) <> F.split(List.drop(&2, U32, x <> t, Nat.add(Bool.pick(Nat, _, 0n, R), 1n)), sep) : List<&2, List<&2, U32>>}
262	      +h2 = AB.subst(Bool, y => {Nat.is_lt(Bool.pick(Nat, y, 0n, R), 1n+List.length(&2, U32, t)) == True{} : Bool}, U32.is_eq(x, sep), False{}, hb, h)
263	      %Equal.sym(List<&2, List<&2, U32>>, F.split(t, sep), List.take(&2, U32, t, r) <> F.split(List.drop(&2, U32, t, Nat.add(r, 1n)), sep), ih(h2)) :
264	        {F.split.push(x, _) == (x <> List.take(&2, U32, t, r)) <> F.split(List.drop(&2, U32, t, Nat.add(r, 1n)), sep) : List<&2, List<&2, U32>>}
265	      {==}
266	
267	# With a separator in ys, the first piece ends at it.
268	law sp1:
269	  for +ys: List<&2, U32>
270	  for +sep: U32
271	  for +h: {Nat.is_lt(D.run_len(ys, sep), List.length(&2, U32, ys)) == True{} : Bool}
272	  {F.split(ys, sep) == List.take(&2, U32, ys, D.run_len(ys, sep)) <> F.split(List.drop(&2, U32, ys, Nat.add(D.run_len(ys, sep), 1n)), sep) : List<&2, List<&2, U32>>}
273	
274	def sp1(ys, sep, h):
275	  match ys:
276	    case Nil{}:
277	      Empty.absurd({F.split(Nil{}, sep) == Nil{} <> F.split(Nil{}, sep) : List<&2, List<&2, U32>>}, AB.false_ne_true(h))
278	    case Con{+x, t}:
279	      sp1c(x, t, sep, U32.is_eq(x, sep), {==}, h, hh => sp1(t, sep, hh))
280	
281	law sp2c:
282	  for +x: U32
283	  for +t: List<&2, U32>
284	  for +sep: U32
285	  for +b: Bool
286	  for +hb: {U32.is_eq(x, sep) == b : Bool}
287	  for +h: {Nat.is_le(List.length(&2, U32, x <> t), D.run_len(x <> t, sep)) == True{} : Bool}
288	  for ih: {Nat.is_le(List.length(&2, U32, t), D.run_len(t, sep)) == True{} : Bool} -> {F.split(t, sep) == [t] : List<&2, List<&2, U32>>}
289	  {F.split(x <> t, sep) == [x <> t] : List<&2, List<&2, U32>>}
290	
291	def sp2c(x, t, sep, b, hb, h, ih):
292	  match b:
293	    case True{}:
294	      +R = Nat.add(1n, D.run_len(t, sep))
295	      +h2 = AB.subst(Bool, y => {Nat.is_le(1n+List.length(&2, U32, t), Bool.pick(Nat, y, 0n, R)) == True{} : Bool}, U32.is_eq(x, sep), True{}, hb, h)
296	      Empty.absurd({F.split(x <> t, sep) == [x <> t] : List<&2, List<&2, U32>>}, AB.false_ne_true(h2))
297	    case False{}:
298	      +R = Nat.add(1n, D.run_len(t, sep))
299	      +h2 = AB.subst(Bool, y => {Nat.is_le(1n+List.length(&2, U32, t), Bool.pick(Nat, y, 0n, R)) == True{} : Bool}, U32.is_eq(x, sep), False{}, hb, h)
300	      %Equal.sym(Bool, U32.is_eq(x, sep), False{}, hb) : {F.split.fin(x, F.split(t, sep), _) == [x <> t] : List<&2, List<&2, U32>>}
301	      %Equal.sym(List<&2, List<&2, U32>>, F.split(t, sep), [t], ih(h2)) : {F.split.push(x, _) == [x <> t] : List<&2, List<&2, U32>>}
302	      {==}
303	
304	# Without one, split gives ys itself.
305	law sp2:
306	  for +ys: List<&2, U32>
307	  for +sep: U32
308	  for +h: {Nat.is_le(List.length(&2, U32, ys), D.run_len(ys, sep)) == True{} : Bool}
309	  {F.split(ys, sep) == [ys] : List<&2, List<&2, U32>>}
310	
311	def sp2(ys, sep, h):
312	  match ys:
313	    case Nil{}:
314	      {==}
315	    case Con{+x, t}:
316	      sp2c(x, t, sep, U32.is_eq(x, sep), {==}, h, hh => sp2(t, sep, hh))
317	
318	# Pieces and bounds from ends
319	# ===========================
320	
321	# pieces and within read only the numbers of their offsets.
322	def PN(ns: List<&2, Nat>, +xs: List<&2, U32>, +from: Nat) -> List<&2, List<&2, U32>>:
323	  match ns:
324	    case Nil{}:
325	      Nil{}
326	    case Con{+e, t}:
327	      Con{D.slice(xs, from, Nat.sub(e, from)), PN(t, xs, Nat.add(e, 1n))}
328	
329	def WN(ns: List<&2, Nat>, +from: Nat, +to: Nat) -> Bool:
330	  match ns:
331	    case Nil{}:
332	      True{}
333	    case Con{+e, t}:
334	      (Nat.is_le(from, e) && Nat.is_le(e, to)) && WN(t, from, to)
335	
336	law pn:
337	  for +es: List<&2, U32>
338	  for +xs: List<&2, U32>
339	  for +from: Nat
340	  {F.pieces(es, xs, from) == PN(F.nats(es), xs, from) : List<&2, List<&2, U32>>}
341	
342	def pn(es, xs, from):
343	  match es:
344	    case Nil{}:
345	      {==}
346	    case Con{+e, t}:
347	      +a = Nat.add(U32.to_nat(e), 1n)
348	      +S0 = D.slice(xs, from, Nat.sub(U32.to_nat(e), from))
349	      %pn(t, xs, a) : {Con{S0, F.pieces(t, xs, a)} == Con{S0, _} : List<&2, List<&2, U32>>}
350	      {==}
351	
352	law wn:
353	  for +es: List<&2, U32>
354	  for +a: Nat
355	  for +b: Nat
356	  {F.within(es, a, b) == WN(F.nats(es), a, b) : Bool}
357	
358	def wn(es, a, b):
359	  match es:
360	    case Nil{}:
361	      {==}
362	    case Con{+e, t}:
363	      +X0 = Nat.is_le(a, U32.to_nat(e)) && Nat.is_le(U32.to_nat(e), b)
364	      %wn(t, a, b) : {Bool.and(X0, F.within(t, a, b)) == Bool.and(X0, _) : Bool}
365	      {==}
366	
367	law pntake:
368	  for +ns: List<&2, Nat>
369	  for +n: Nat
370	  for +xs: List<&2, U32>
371	  for +s: Nat
372	  {PN(List.take(&2, Nat, ns, n), xs, s) == List.take(&2, List<&2, U32>, PN(ns, xs, s), n) : List<&2, List<&2, U32>>}
373	
374	def pntake(ns, n, xs, s):
375	  match ns n:
376	    case Nil{} _:
377	      {==}
378	    case Con{e, t} 0n:
379	      {==}
380	    case Con{+e, t} 1n+m:
381	      +S0 = D.slice(xs, s, Nat.sub(e, s))
382	      %pntake(t, m, xs, Nat.add(e, 1n)) :
383	        {Con{S0, PN(List.take(&2, Nat, t, m), xs, Nat.add(e, 1n))} == Con{S0, _} : List<&2, List<&2, U32>>}
384	      {==}
385	
386	law wtake:
387	  for +ns: List<&2, Nat>
388	  for +n: Nat
389	  for +a: Nat
390	  for +b: Nat
391	  for +hw: {WN(ns, a, b) == True{} : Bool}
392	  {WN(List.take(&2, Nat, ns, n), a, b) == True{} : Bool}
393	
394	def wtake(ns, n, a, b, hw):
395	  match ns n:
396	    case Nil{} _:
397	      {==}
398	    case Con{e, t} 0n:
399	      {==}
400	    case Con{+e, t} 1n+m:
401	      +X0 = Nat.is_le(a, e) && Nat.is_le(e, b)
402	      %Equal.sym(Bool, X0, True{}, AB.and_true_l(X0, WN(t, a, b), hw)) :
403	        {Bool.and(_, WN(List.take(&2, Nat, t, m), a, b)) == True{} : Bool}
404	      wtake(t, m, a, b, AB.and_true_r(X0, WN(t, a, b), hw))
405	
406	# A lower bound may be lowered.
407	law wk:
408	  for +ns: List<&2, Nat>
409	  for +a: Nat
410	  for +a2: Nat
411	  for +b: Nat
412	  for +h: {Nat.is_le(a, a2) == True{} : Bool}
413	  for +hw: {WN(ns, a2, b) == True{} : Bool}
414	  {WN(ns, a, b) == True{} : Bool}
415	
416	def wk(ns, a, a2, b, h, hw):
417	  match ns:
418	    case Nil{}:
419	      {==}
420	    case Con{+e, t}:
421	      +X2 = Nat.is_le(a2, e) && Nat.is_le(e, b)
422	      +hx = AB.and_true_l(X2, WN(t, a2, b), hw)
423	      %Equal.sym(Bool, Nat.is_le(a, e), True{}, N.le_trans(a, a2, e, h, AB.and_true_l(Nat.is_le(a2, e), Nat.is_le(e, b), hx))) :
424	        {Bool.and(Bool.and(_, Nat.is_le(e, b)), WN(t, a, b)) == True{} : Bool}
425	      %Equal.sym(Bool, Nat.is_le(e, b), True{}, AB.and_true_r(Nat.is_le(a2, e), Nat.is_le(e, b), hx)) :
426	        {Bool.and(Bool.and(True{}, _), WN(t, a, b)) == True{} : Bool}
427	      %Equal.sym(Bool, WN(t, a, b), True{}, wk(t, a, a2, b, h, AB.and_true_r(X2, WN(t, a2, b), hw))) :
428	        {Bool.and(Bool.and(True{}, True{}), _) == True{} : Bool}
429	      {==}
430	
431	law pre_get:
432	  for +xs: List<&2, U32>
433	  for +s: Nat
434	  for +x: U32
435	  for +t: List<&2, U32>
436	  for +hp: {List.take(&2, U32, List.drop(&2, U32, xs, s), 1n+List.length(&2, U32, t)) == x <> t : List<&2, U32>}
437	  {List.get(&2, U32, xs, s) == Some{x} : Maybe<&2, U32>}
438	
439	def pre_get(xs, s, x, t, hp):
440	  match xs s:
441	    case Nil{} _:
442	      Empty.absurd({List.get(&2, U32, Nil{}, s) == Some{x} : Maybe<&2, U32>}, nil_cons(x, t, hp))
443	    case Con{+y, r} 0n:
444	      Equal.cong(U32, Maybe<&2, U32>, z => Some{z}, y, x,
445	        AB.cons_inj_h(U32, y, x, List.take(&2, U32, r, List.length(&2, U32, t)), t, hp))
446	    case Con{y, r} 1n+p:
447	      pre_get(r, p, x, t, hp)
448	
449	law pre_tail:
450	  for +xs: List<&2, U32>
451	  for +s: Nat
452	  for +x: U32
453	  for +t: List<&2, U32>
454	  for +hp: {List.take(&2, U32, List.drop(&2, U32, xs, s), 1n+List.length(&2, U32, t)) == x <> t : List<&2, U32>}
455	  {List.take(&2, U32, List.drop(&2, U32, xs, Nat.add(s, 1n)), List.length(&2, U32, t)) == t : List<&2, U32>}
456	
457	def pre_tail(xs, s, x, t, hp):
458	  match xs s:
459	    case Nil{} _:
460	      Empty.absurd({List.take(&2, U32, Nil{}, List.length(&2, U32, t)) == t : List<&2, U32>}, nil_cons(x, t, hp))
461	    case Con{+y, r} 0n:
462	      %Equal.sym(List<&2, U32>, List.drop(&2, U32, r, 0n), r, X.drop_zero(r)) :
463	        {List.take(&2, U32, _, List.length(&2, U32, t)) == t : List<&2, U32>}
464	      AB.cons_inj_t(U32, y, x, List.take(&2, U32, r, List.length(&2, U32, t)), t, hp)
465	    case Con{y, r} 1n+p:
466	      pre_tail(r, p, x, t, hp)
467	
468	# Pushing a byte onto the first piece shifts every end by one.
469	law ends_push:
470	  for +x: U32
471	  for +ps: List<&2, List<&2, U32>>
472	  for +s: Nat
473	  for +hnn: {nn(ps) == True{} : Bool}
474	  {F.ends(F.split.push(x, ps), s) == F.ends(ps, Nat.add(s, 1n)) : List<&2, Nat>}
475	
476	def ends_push(x, ps, s, hnn):
477	  match ps:
478	    case Nil{}:
479	      Empty.absurd({F.ends(F.split.push(x, Nil{}), s) == F.ends(Nil{}, Nat.add(s, 1n)) : List<&2, Nat>}, AB.false_ne_true(hnn))
480	    case Con{+p, r}:
481	      +L = List.length(&2, U32, p)
482	      %Equal.sym(Nat, Nat.add(Nat.add(s, 1n), L), Nat.add(s, Nat.add(1n, L)), N.add_assoc(s, 1n, L)) :
483	        {F.ends(F.split.push(x, p <> r), s) == Con{_, F.ends(r, Nat.add(_, 1n))} : List<&2, Nat>}
484	      {==}
485	
486	law sa:
487	  for +s: Nat
488	  for +l: Nat
489	  {Nat.sub(Nat.add(Nat.add(s, 1n), l), s) == 1n+l : Nat}
490	
491	def sa(s, l):
492	  %Equal.sym(Nat, Nat.add(Nat.add(s, 1n), l), Nat.add(s, Nat.add(1n, l)), N.add_assoc(s, 1n, l)) : {Nat.sub(_, s) == 1n+l : Nat}
493	  N.sub_add_l(s, 1n+l)
494	
495	law pb_push:
496	  for +x: U32
497	  for +ps: List<&2, List<&2, U32>>
498	  for +xs: List<&2, U32>
499	  for +s: Nat
500	  for +hnn: {nn(ps) == True{} : Bool}
501	  for +hg: {List.get(&2, U32, xs, s) == Some{x} : Maybe<&2, U32>}
502	  for +ih: {PN(F.ends(ps, Nat.add(s, 1n)), xs, Nat.add(s, 1n)) == ps : List<&2, List<&2, U32>>}
503	  {PN(F.ends(F.split.push(x, ps), s), xs, s) == F.split.push(x, ps) : List<&2, List<&2, U32>>}
504	
505	def pb_push(x, ps, xs, s, hnn, hg, ih):
506	  match ps:
507	    case Nil{}:
508	      Empty.absurd({PN(F.ends(F.split.push(x, Nil{}), s), xs, s) == F.split.push(x, Nil{}) : List<&2, List<&2, U32>>}, AB.false_ne_true(hnn))
509	    case Con{+p, r}:
510	      +L = List.length(&2, U32, p)
511	      +s1 = Nat.add(s, 1n)
512	      +A2 = Nat.add(s1, L)
513	      +TL = PN(F.ends(r, Nat.add(A2, 1n)), xs, Nat.add(A2, 1n))
514	      +hh = AB.cons_inj_h(List<&2, U32>, D.slice(xs, s1, Nat.sub(A2, s1)), p, TL, r, ih)
515	      +ht = AB.cons_inj_t(List<&2, U32>, D.slice(xs, s1, Nat.sub(A2, s1)), p, TL, r, ih)
516	      %Equal.sym(List<&2, Nat>, F.ends(F.split.push(x, p <> r), s), F.ends(p <> r, s1), ends_push(x, p <> r, s, {==})) :
517	        {PN(_, xs, s) == F.split.push(x, p <> r) : List<&2, List<&2, U32>>}
518	      %Equal.sym(List<&2, List<&2, U32>>, TL, r, ht) : {Con{D.slice(xs, s, Nat.sub(A2, s)), _} == Con{x <> p, r} : List<&2, List<&2, U32>>}
519	      %Equal.sym(Nat, Nat.sub(A2, s), 1n+L, sa(s, L)) : {Con{D.slice(xs, s, _), r} == Con{x <> p, r} : List<&2, List<&2, U32>>}
520	      %Equal.sym(List<&2, U32>, D.slice(xs, s, 1n+L), x <> D.slice(xs, s1, L), X.slice_cons(xs, s, L, x, hg)) :
521	        {Con{_, r} == Con{x <> p, r} : List<&2, List<&2, U32>>}
522	      +hh2 = AB.subst(Nat, y => {D.slice(xs, s1, y) == p : List<&2, U32>}, Nat.sub(A2, s1), L, N.sub_add_l(s1, L), hh)
523	      %Equal.sym(List<&2, U32>, D.slice(xs, s1, L), p, hh2) : {Con{x <> _, r} == Con{x <> p, r} : List<&2, List<&2, U32>>}
524	      {==}
525	
526	law pbc:
527	  for +x: U32
528	  for +t: List<&2, U32>
529	  for +xs: List<&2, U32>
530	  for +s: Nat
531	  for +sep: U32
532	  for +b: Bool
533	  for +hb: {U32.is_eq(x, sep) == b : Bool}
534	  for +hg: {List.get(&2, U32, xs, s) == Some{x} : Maybe<&2, U32>}
535	  for +ih: {PN(F.ends(F.split(t, sep), Nat.add(s, 1n)), xs, Nat.add(s, 1n)) == F.split(t, sep) : List<&2, List<&2, U32>>}
536	  {PN(F.ends(F.split(x <> t, sep), s), xs, s) == F.split(x <> t, sep) : List<&2, List<&2, U32>>}
537	
538	def pbc(x, t, xs, s, sep, b, hb, hg, ih):
539	  match b:
540	    case True{}:
541	      %Equal.sym(Bool, U32.is_eq(x, sep), True{}, hb) :
542	        {PN(F.ends(F.split.fin(x, F.split(t, sep), _), s), xs, s) == F.split.fin(x, F.split(t, sep), _) : List<&2, List<&2, U32>>}
543	      %Equal.sym(Nat, Nat.add(s, 0n), s, N.add_zero(s)) :
544	        {Con{D.slice(xs, s, Nat.sub(_, s)), PN(F.ends(F.split(t, sep), Nat.add(_, 1n)), xs, Nat.add(_, 1n))} == Nil{} <> F.split(t, sep) : List<&2, List<&2, U32>>}
545	      %Equal.sym(Nat, Nat.sub(s, s), 0n, H.sub_self(s)) :
546	        {Con{D.slice(xs, s, _), PN(F.ends(F.split(t, sep), Nat.add(s, 1n)), xs, Nat.add(s, 1n))} == Nil{} <> F.split(t, sep) : List<&2, List<&2, U32>>}
547	      %Equal.sym(List<&2, U32>, D.slice(xs, s, 0n), Nil{}, X.slice_zero(xs, s)) :
548	        {Con{_, PN(F.ends(F.split(t, sep), Nat.add(s, 1n)), xs, Nat.add(s, 1n))} == Nil{} <> F.split(t, sep) : List<&2, List<&2, U32>>}
549	      %Equal.sym(List<&2, List<&2, U32>>, PN(F.ends(F.split(t, sep), Nat.add(s, 1n)), xs, Nat.add(s, 1n)), F.split(t, sep), ih) :
550	        {Con{Nil{}, _} == Nil{} <> F.split(t, sep) : List<&2, List<&2, U32>>}
551	      {==}
552	    case False{}:
553	      %Equal.sym(Bool, U32.is_eq(x, sep), False{}, hb) :
554	        {PN(F.ends(F.split.fin(x, F.split(t, sep), _), s), xs, s) == F.split.fin(x, F.split(t, sep), _) : List<&2, List<&2, U32>>}
555	      pb_push(x, F.split(t, sep), xs, s, split_nn(t, sep), hg, ih)
556	
557	# The ends of split(ys) from s give back its pieces when ys starts xs at s.
558	law pb:
559	  for +ys: List<&2, U32>
560	  for +xs: List<&2, U32>
561	  for +s: Nat
562	  for +sep: U32
563	  for +hp: {List.take(&2, U32, List.drop(&2, U32, xs, s), List.length(&2, U32, ys)) == ys : List<&2, U32>}
564	  {PN(F.ends(F.split(ys, sep), s), xs, s) == F.split(ys, sep) : List<&2, List<&2, U32>>}
565	
566	def pb(ys, xs, s, sep, hp):
567	  match ys:
568	    case Nil{}:
569	      %Equal.sym(Nat, Nat.add(s, 0n), s, N.add_zero(s)) : {Con{D.slice(xs, s, Nat.sub(_, s)), Nil{}} == [Nil{}] : List<&2, List<&2, U32>>}
570	      %Equal.sym(Nat, Nat.sub(s, s), 0n, H.sub_self(s)) : {Con{D.slice(xs, s, _), Nil{}} == [Nil{}] : List<&2, List<&2, U32>>}
571	      %Equal.sym(List<&2, U32>, D.slice(xs, s, 0n), Nil{}, X.slice_zero(xs, s)) : {Con{_, Nil{}} == [Nil{}] : List<&2, List<&2, U32>>}
572	      {==}
573	    case Con{+x, t}:
574	      pbc(x, t, xs, s, sep, U32.is_eq(x, sep), {==}, pre_get(xs, s, x, t, hp),
575	        pb(t, xs, Nat.add(s, 1n), sep, pre_tail(xs, s, x, t, hp)))
576	
577	law wc:
578	  for +x: U32
579	  for +t: List<&2, U32>
580	  for +s: Nat
581	  for +sep: U32
582	  for +b: Bool
583	  for +hb: {U32.is_eq(x, sep) == b : Bool}
584	  for +ih: {WN(F.ends(F.split(t, sep), Nat.add(s, 1n)), s, Nat.add(s, 1n+List.length(&2, U32, t))) == True{} : Bool}
585	  {WN(F.ends(F.split(x <> t, sep), s), s, Nat.add(s, List.length(&2, U32, x <> t))) == True{} : Bool}
586	
587	def wc(x, t, s, sep, b, hb, ih):
588	  match b:
589	    case True{}:
590	      +U = Nat.add(s, 1n+List.length(&2, U32, t))
591	      %Equal.sym(Bool, U32.is_eq(x, sep), True{}, hb) : {WN(F.ends(F.split.fin(x, F.split(t, sep), _), s), s, U) == True{} : Bool}
592	      %Equal.sym(Nat, Nat.add(s, 0n), s, N.add_zero(s)) :
593	        {Bool.and(Bool.and(Nat.is_le(s, _), Nat.is_le(_, U)), WN(F.ends(F.split(t, sep), Nat.add(_, 1n)), s, U)) == True{} : Bool}
594	      %Equal.sym(Bool, Nat.is_le(s, s), True{}, N.le_refl(s)) :
595	        {Bool.and(Bool.and(_, Nat.is_le(s, U)), WN(F.ends(F.split(t, sep), Nat.add(s, 1n)), s, U)) == True{} : Bool}
596	      %Equal.sym(Bool, Nat.is_le(s, U), True{}, N.le_add_r(s, 1n+List.length(&2, U32, t))) :
597	        {Bool.and(Bool.and(True{}, _), WN(F.ends(F.split(t, sep), Nat.add(s, 1n)), s, U)) == True{} : Bool}
598	      %Equal.sym(Bool, WN(F.ends(F.split(t, sep), Nat.add(s, 1n)), s, U), True{}, ih) :
599	        {Bool.and(Bool.and(True{}, True{}), _) == True{} : Bool}
600	      {==}
601	    case False{}:
602	      +U = Nat.add(s, 1n+List.length(&2, U32, t))
603	      %Equal.sym(Bool, U32.is_eq(x, sep), False{}, hb) : {WN(F.ends(F.split.fin(x, F.split(t, sep), _), s), s, U) == True{} : Bool}
604	      %Equal.sym(List<&2, Nat>, F.ends(F.split.push(x, F.split(t, sep)), s), F.ends(F.split(t, sep), Nat.add(s, 1n)),
605	        ends_push(x, F.split(t, sep), s, split_nn(t, sep))) :
606	        {WN(_, s, U) == True{} : Bool}
607	      ih
608	
609	# The ends of split(ys) from s lie in s .. s + length(ys).
610	law wl:
611	  for +ys: List<&2, U32>
612	  for +s: Nat
613	  for +sep: U32
614	  {WN(F.ends(F.split(ys, sep), s), s, Nat.add(s, List.length(&2, U32, ys))) == True{} : Bool}
615	
616	def wl(ys, s, sep):
617	  match ys:
618	    case Nil{}:
619	      %Equal.sym(Nat, Nat.add(s, 0n), s, N.add_zero(s)) : {Bool.and(Bool.and(Nat.is_le(s, _), Nat.is_le(_, _)), True{}) == True{} : Bool}
620	      %Equal.sym(Bool, Nat.is_le(s, s), True{}, N.le_refl(s)) : {Bool.and(Bool.and(_, _), True{}) == True{} : Bool}
621	      {==}
622	    case Con{+x, t}:
623	      +L = List.length(&2, U32, t)
624	      +s1 = Nat.add(s, 1n)
625	      +ih = wl(t, s1, sep)
626	      wc(x, t, s, sep, U32.is_eq(x, sep), {==},
627	        wk(F.ends(F.split(t, sep), s1), s, s1, Nat.add(s, 1n+L), N.le_add_r(s, 1n),
628	          AB.subst(Nat, y => {WN(F.ends(F.split(t, sep), s1), s1, y) == True{} : Bool}, Nat.add(s1, L), Nat.add(s, Nat.add(1n, L)),
629	            N.add_assoc(s, 1n, L), ih)))
630	
631	# The loop as a Data function
632	# ===========================
633	
634	def FV(+len: U32, +t: P.Tree<U32>, +s: U32, +to: U32, +sep: U32) -> U32:
635	  Pair.snd(D.Bytes, U32, B.find(C.BT(len, t), s, to, sep))
636	
637	def NX(want: Bool, +len: U32, +t: P.Tree<U32>, +s: U32, +to: U32, +sep: U32) -> U32:
638	  match want:
639	    case True{}:
640	      FV(len, t, s, to, sep)
641	    case False{}:
642	      to
643	
644	def CG(+n: Nat, more: Bool, +e: U32, +len: U32, +t: P.Tree<U32>, +to: U32, +sep: U32) -> List<&2, U32>:
645	  match n more:
646	    case 0n _:
647	      Nil{}
648	    case 1n+m False{}:
649	      Nil{}
650	    case 1n+m True{}:
651	      +go = U32.is_lt(e, to)
652	      Con{e, CG(m, go, NX(go && Bool.not(Nat.is_eq(m, 0n)), len, t, (e + 1 : U32), to, sep), len, t, to, sep)}
653	
654	law nx_eq:
655	  for +want: Bool
656	  for +len: U32
657	  for +t: P.Tree<U32>
658	  for +s: U32
659	  for +to: U32
660	  for +sep: U32
661	  {K.cut.next(want, C.BT(len, t), s, to, sep) == (C.BT(len, t), NX(want, len, t, s, to, sep)) : D.Bytes & U32}
662	
663	def nx_eq(want, len, t, s, to, sep):
664	  match want:
665	    case True{}:
666	      FI.find_pair_t(len, t, s, to, sep)
667	    case False{}:
668	      {==}
669	
670	law cg_eq:
671	  for +n: Nat
672	  for +more: Bool
673	  for +e: U32
674	  for +len: U32
675	  for +t: P.Tree<U32>
676	  for +to: U32
677	  for +sep: U32
678	  {K.cut.go(n, more, (C.BT(len, t), e), to, sep) == (C.BT(len, t), CG(n, more, e, len, t, to, sep)) : D.Bytes & List<&2, U32>}
679	
680	def cg_eq(n, more, e, len, t, to, sep):
681	  match n more:
682	    case 0n _:
683	      {==}
684	    case 1n+m False{}:
685	      {==}
686	    case 1n+m True{}:
687	      +go = U32.is_lt(e, to)
688	      +W = go && Bool.not(Nat.is_eq(m, 0n))
689	      +e1 = (e + 1 : U32)
690	      +nx = NX(W, len, t, e1, to, sep)
691	      %Equal.sym(D.Bytes & U32, K.cut.next(W, C.BT(len, t), e1, to, sep), (C.BT(len, t), nx), nx_eq(W, len, t, e1, to, sep)) :
692	        {K.cut.cons(e, K.cut.go(m, go, _, to, sep)) == (C.BT(len, t), CG(1n+m, True{}, e, len, t, to, sep)) : D.Bytes & List<&2, U32>}
693	      %Equal.sym(D.Bytes & List<&2, U32>, K.cut.go(m, go, (C.BT(len, t), nx), to, sep), (C.BT(len, t), CG(m, go, nx, len, t, to, sep)),
694	        cg_eq(m, go, nx, len, t, to, sep)) :
695	        {K.cut.cons(e, _) == (C.BT(len, t), CG(1n+m, True{}, e, len, t, to, sep)) : D.Bytes & List<&2, U32>}
696	      {==}
697	
698	law cut_eq:
699	  for +len: U32
700	  for +t: P.Tree<U32>
701	  for +from: U32
702	  for +to: U32
703	  for +sep: U32
704	  for +n: Nat
705	  {K.cut(C.BT(len, t), from, to, sep, n) == (C.BT(len, t), CG(n, True{}, NX(Bool.not(Nat.is_eq(n, 0n)), len, t, from, to, sep), len, t, to, sep)) : D.Bytes & List<&2, U32>}
706	
707	def cut_eq(len, t, from, to, sep, n):
708	  +W0 = Bool.not(Nat.is_eq(n, 0n))
709	  %Equal.sym(D.Bytes & U32, K.cut.next(W0, C.BT(len, t), from, to, sep), (C.BT(len, t), NX(W0, len, t, from, to, sep)), nx_eq(W0, len, t, from, to, sep)) :
710	    {K.cut.go(n, True{}, _, to, sep) == (C.BT(len, t), CG(n, True{}, NX(W0, len, t, from, to, sep), len, t, to, sep)) : D.Bytes & List<&2, U32>}
711	  cg_eq(n, True{}, NX(W0, len, t, from, to, sep), len, t, to, sep)
712	
713	law cut_pair_t:
714	  for +len: U32
715	  for +t: P.Tree<U32>
716	  for +from: U32
717	  for +to: U32
718	  for +sep: U32
719	  for +n: Nat
720	  {K.cut(C.BT(len, t), from, to, sep, n) == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, K.cut(C.BT(len, t), from, to, sep, n))) : D.Bytes & List<&2, U32>}
721	
722	def cut_pair_t(len, t, from, to, sep, n):
723	  %Equal.sym(D.Bytes & List<&2, U32>, K.cut(C.BT(len, t), from, to, sep, n),
724	    (C.BT(len, t), CG(n, True{}, NX(Bool.not(Nat.is_eq(n, 0n)), len, t, from, to, sep), len, t, to, sep)), cut_eq(len, t, from, to, sep, n)) :
725	    {_ == (C.BT(len, t), Pair.snd(D.Bytes, List<&2, U32>, _)) : D.Bytes & List<&2, U32>}
726	  {==}
727	
728	# The loop invariant
729	# ==================
730	
731	# The slice from s to T has T - s bytes.
732	law ylen:
733	  for +len: U32
734	  for +t: P.Tree<U32>
735	  for +d: Nat
736	  for +s: Nat
737	  for +tt: Nat
738	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
739	  for +hT: {Nat.is_le(tt, U32.to_nat(len)) == True{} : Bool}
740	  {List.length(&2, U32, D.slice(D.view(C.BT(len, t)), s, Nat.sub(tt, s))) == Nat.sub(tt, s) : Nat}
741	
742	def ylen(len, t, d, s, tt, h, hT):
743	  +xs = D.view(C.BT(len, t))
744	  +e1 = Equal.trans(Nat, List.length(&2, U32, List.drop(&2, U32, xs, s)), Nat.sub(List.length(&2, U32, xs), s), Nat.sub(U32.to_nat(len), s),
745	    H.drop_length(xs, s),
746	    Equal.cong(Nat, Nat, y => Nat.sub(y, s), List.length(&2, U32, xs), U32.to_nat(len), O.view_size_t(len, t, d, h)))
747	  S.take_length(List.drop(&2, U32, xs, s), Nat.sub(tt, s),
748	    AB.subst(Nat, y => {Nat.is_le(Nat.sub(tt, s), y) == True{} : Bool}, Nat.sub(U32.to_nat(len), s), List.length(&2, U32, List.drop(&2, U32, xs, s)),
749	      Equal.sym(Nat, List.length(&2, U32, List.drop(&2, U32, xs, s)), Nat.sub(U32.to_nat(len), s), e1),
750	      sub_mono(tt, U32.to_nat(len), s, hT)))
751	
752	# After the last piece (the end reached to): one more end, at to.
753	law cgf:
754	  for +s: Nat
755	  for +e: U32
756	  for +len: U32
757	  for +t: P.Tree<U32>
758	  for +d: Nat
759	  for +to: U32
760	  for +sep: U32
761	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
762	  for +hT: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
763	  for +he: {U32.to_nat(e) == D.first(D.view(C.BT(len, t)), s, U32.to_nat(to), sep) : Nat}
764	  for +hg: {U32.is_lt(e, to) == False{} : Bool}
765	  for +kk: Nat
766	  {Con{U32.to_nat(e), Nil{}} == List.take(&2, Nat, F.ends(F.split(D.slice(D.view(C.BT(len, t)), s, Nat.sub(U32.to_nat(to), s)), sep), s), 1n+kk) : List<&2, Nat>}
767	
768	def cgf(s, e, len, t, d, to, sep, h, hT, he, hg, kk):
769	  +xs = D.view(C.BT(len, t))
770	  +TT = U32.to_nat(to)
771	  +ys = D.slice(xs, s, Nat.sub(TT, s))
772	  +r = D.run_len(ys, sep)
773	  +hyl = ylen(len, t, d, s, TT, h, hT)
774	  +hn = Equal.trans(Bool, Nat.is_lt(U32.to_nat(e), TT), U32.is_lt(e, to), False{}, Equal.sym(Bool, U32.is_lt(e, to), Nat.is_lt(U32.to_nat(e), TT), U.is_lt_to_nat(e, to)), hg)
775	  +hle = AB.subst(Nat, y => {Nat.is_le(TT, y) == True{} : Bool}, U32.to_nat(e), Nat.add(s, r), he, N.not_lt_le(U32.to_nat(e), TT, hn))
776	  +h1 = AB.subst(Nat, y => {Nat.is_le(y, r) == True{} : Bool}, Nat.sub(TT, s), List.length(&2, U32, ys), Equal.sym(Nat, List.length(&2, U32, ys), Nat.sub(TT, s), hyl),
777	    sub_le_of(TT, s, r, hle))
778	  +h2 = AB.subst(Nat, y => {Nat.is_le(r, y) == True{} : Bool}, Nat.sub(TT, s), List.length(&2, U32, ys), Equal.sym(Nat, List.length(&2, U32, ys), Nat.sub(TT, s), hyl),
779	    Q.pl_r_le(List.drop(&2, U32, xs, s), Nat.sub(TT, s), sep))
780	  %Equal.sym(List<&2, List<&2, U32>>, F.split(ys, sep), [ys], sp2(ys, sep, h1)) :
781	    {Con{U32.to_nat(e), Nil{}} == List.take(&2, Nat, F.ends(_, s), 1n+kk) : List<&2, Nat>}
782	  %Equal.sym(Nat, U32.to_nat(e), D.first(D.view(C.BT(len, t)), s, U32.to_nat(to), sep), he) :
783	    {Con{_, Nil{}} == Con{Nat.add(s, List.length(&2, U32, ys)), Nil{}} : List<&2, Nat>}
784	  %le_antisym(r, List.length(&2, U32, ys), h2, h1) : {Con{Nat.add(s, r), Nil{}} == Con{Nat.add(s, _), Nil{}} : List<&2, Nat>}
785	  {==}
786	
787	law cgv:
788	  for +k: Nat
789	  for +g: Bool
790	  for +s: Nat
791	  for +e: U32
792	  for +len: U32
793	  for +t: P.Tree<U32>
794	  for +d: Nat
795	  for +to: U32
796	  for +sep: U32
797	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
798	  for +hT: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
799	  for +hs: {Nat.is_le(s, U32.to_nat(to)) == True{} : Bool}
800	  for +hsep: {U32.is_lt(sep, 256) == True{} : Bool}
801	  for +he: {U32.to_nat(e) == D.first(D.view(C.BT(len, t)), s, U32.to_nat(to), sep) : Nat}
802	  for +hg: {U32.is_lt(e, to) == g : Bool}
803	  {F.nats(CG(1n+k, True{}, e, len, t, to, sep)) == List.take(&2, Nat, F.ends(F.split(D.slice(D.view(C.BT(len, t)), s, Nat.sub(U32.to_nat(to), s)), sep), s), 1n+k) : List<&2, Nat>}
804	
805	def cgv(k, g, s, e, len, t, d, to, sep, h, hT, hs, hsep, he, hg):
806	  match k g:
807	    case 0n False{}:
808	      +RHS = List.take(&2, Nat, F.ends(F.split(D.slice(D.view(C.BT(len, t)), s, Nat.sub(U32.to_nat(to), s)), sep), s), 1n)
809	      %Equal.sym(Bool, U32.is_lt(e, to), False{}, hg) :
810	        {Con{U32.to_nat(e), F.nats(CG(0n, _, NX(Bool.and(_, Bool.not(Nat.is_eq(0n, 0n))), len, t, (e + 1 : U32), to, sep), len, t, to, sep))} == RHS : List<&2, Nat>}
811	      cgf(s, e, len, t, d, to, sep, h, hT, he, hg, 0n)
812	    case 1n+k2 False{}:
813	      +RHS = List.take(&2, Nat, F.ends(F.split(D.slice(D.view(C.BT(len, t)), s, Nat.sub(U32.to_nat(to), s)), sep), s), 1n+1n+k2)
814	      %Equal.sym(Bool, U32.is_lt(e, to), False{}, hg) :
815	        {Con{U32.to_nat(e), F.nats(CG(1n+k2, _, NX(Bool.and(_, Bool.not(Nat.is_eq(1n+k2, 0n))), len, t, (e + 1 : U32), to, sep), len, t, to, sep))} == RHS : List<&2, Nat>}
816	      cgf(s, e, len, t, d, to, sep, h, hT, he, hg, 1n+k2)
817	    case 0n True{}:
818	      +xs = D.view(C.BT(len, t))
819	      +TT = U32.to_nat(to)
820	      +ys = D.slice(xs, s, Nat.sub(TT, s))
821	      +r = D.run_len(ys, sep)
822	      +hyl = ylen(len, t, d, s, TT, h, hT)
823	      +hlt = AB.subst(Nat, y => {Nat.is_lt(y, TT) == True{} : Bool}, U32.to_nat(e), Nat.add(s, r), he,
824	        Equal.trans(Bool, Nat.is_lt(U32.to_nat(e), TT), U32.is_lt(e, to), True{}, Equal.sym(Bool, U32.is_lt(e, to), Nat.is_lt(U32.to_nat(e), TT), U.is_lt_to_nat(e, to)), hg))
825	      +hr = AB.subst(Nat, y => {Nat.is_lt(r, y) == True{} : Bool}, Nat.sub(TT, s), List.length(&2, U32, ys), Equal.sym(Nat, List.length(&2, U32, ys), Nat.sub(TT, s), hyl),
826	        lt_sub_of(s, r, TT, hlt))
827	      +REST = F.split(List.drop(&2, U32, ys, Nat.add(r, 1n)), sep)
828	      +RHS = List.take(&2, Nat, F.ends(F.split(ys, sep), s), 1n)
829	      %Equal.sym(Bool, U32.is_lt(e, to), True{}, hg) :
830	        {Con{U32.to_nat(e), F.nats(CG(0n, _, NX(Bool.and(_, Bool.not(Nat.is_eq(0n, 0n))), len, t, (e + 1 : U32), to, sep), len, t, to, sep))} == RHS : List<&2, Nat>}
831	      %Equal.sym(List<&2, List<&2, U32>>, F.split(ys, sep), List.take(&2, U32, ys, r) <> REST, sp1(ys, sep, hr)) :
832	        {Con{U32.to_nat(e), Nil{}} == List.take(&2, Nat, F.ends(_, s), 1n) : List<&2, Nat>}
833	      +L1 = List.length(&2, U32, List.take(&2, U32, ys, r))
834	      %Equal.sym(List<&2, Nat>, List.take(&2, Nat, F.ends(REST, Nat.add(Nat.add(s, L1), 1n)), 0n), Nil{}, tz(Nat, F.ends(REST, Nat.add(Nat.add(s, L1), 1n)))) :
835	        {Con{U32.to_nat(e), Nil{}} == Con{Nat.add(s, L1), _} : List<&2, Nat>}
836	      %Equal.sym(Nat, List.length(&2, U32, List.take(&2, U32, ys, r)), r, S.take_length(ys, r, N.lt_to_le(r, List.length(&2, U32, ys), hr))) : {Con{U32.to_nat(e), Nil{}} == Con{Nat.add(s, _), Nil{}} : List<&2, Nat>}
837	      %Equal.sym(Nat, U32.to_nat(e), D.first(D.view(C.BT(len, t)), s, U32.to_nat(to), sep), he) :
838	        {Con{_, Nil{}} == Con{Nat.add(s, r), Nil{}} : List<&2, Nat>}
839	      {==}
840	    case 1n+k2 True{}:
841	      +xs = D.view(C.BT(len, t))
842	      +TT = U32.to_nat(to)
843	      +ys = D.slice(xs, s, Nat.sub(TT, s))
844	      +r = D.run_len(ys, sep)
845	      +e1 = (e + 1 : U32)
846	      +e2 = FV(len, t, e1, to, sep)
847	      +s2 = U32.to_nat(e1)
848	      +hyl = ylen(len, t, d, s, TT, h, hT)
849	      +htl = Equal.trans(Bool, Nat.is_lt(U32.to_nat(e), TT), U32.is_lt(e, to), True{}, Equal.sym(Bool, U32.is_lt(e, to), Nat.is_lt(U32.to_nat(e), TT), U.is_lt_to_nat(e, to)), hg)
850	      +hlt = AB.subst(Nat, y => {Nat.is_lt(y, TT) == True{} : Bool}, U32.to_nat(e), Nat.add(s, r), he, htl)
851	      +hr = AB.subst(Nat, y => {Nat.is_lt(r, y) == True{} : Bool}, Nat.sub(TT, s), List.length(&2, U32, ys), Equal.sym(Nat, List.length(&2, U32, ys), Nat.sub(TT, s), hyl),
852	        lt_sub_of(s, r, TT, hlt))
853	      +M = Nat.mul(4n, Nat.pow(2n, d))
854	      +ei = C.inc_fits(e, d, C.ok_d(len, t, d, h),
855	        N.lt_le_trans(U32.to_nat(e), U32.to_nat(len), M, N.lt_le_trans(U32.to_nat(e), TT, U32.to_nat(len), htl, hT), C.ok_len(len, t, d, h)))
856	      +es2 = Equal.trans(Nat, s2, Nat.add(U32.to_nat(e), 1n), Nat.add(Nat.add(s, r), 1n), ei,
857	        Equal.cong(Nat, Nat, y => Nat.add(y, 1n), U32.to_nat(e), Nat.add(s, r), he))
858	      +hs2 = AB.subst(Nat, y => {Nat.is_le(y, TT) == True{} : Bool}, Nat.add(Nat.add(s, r), 1n), s2, Equal.sym(Nat, s2, Nat.add(Nat.add(s, r), 1n), es2),
859	        C.succ_le(Nat.add(s, r), TT, hlt))
860	      +hft2 = Equal.trans(Bool, U32.is_le(e1, to), Nat.is_le(s2, TT), True{}, U.is_le_to_nat(e1, to), hs2)
861	      +he2 = FI.find_view_t(len, t, d, e1, to, sep, h, hft2, hT, hsep)
862	      +ih = cgv(k2, U32.is_lt(e2, to), s2, e2, len, t, d, to, sep, h, hT, hs2, hsep, he2, {==})
863	      +RHS = List.take(&2, Nat, F.ends(F.split(ys, sep), s), 1n+1n+k2)
864	      +REST = F.split(List.drop(&2, U32, ys, Nat.add(r, 1n)), sep)
865	      +L1 = List.length(&2, U32, List.take(&2, U32, ys, r))
866	      %Equal.sym(Bool, U32.is_lt(e, to), True{}, hg) :
867	        {Con{U32.to_nat(e), F.nats(CG(1n+k2, _, NX(Bool.and(_, Bool.not(Nat.is_eq(1n+k2, 0n))), len, t, e1, to, sep), len, t, to, sep))} == RHS : List<&2, Nat>}
868	      %Equal.sym(List<&2, List<&2, U32>>, F.split(ys, sep), List.take(&2, U32, ys, r) <> REST, sp1(ys, sep, hr)) :
869	        {Con{U32.to_nat(e), F.nats(CG(1n+k2, True{}, e2, len, t, to, sep))} == List.take(&2, Nat, F.ends(_, s), 1n+1n+k2) : List<&2, Nat>}
870	      %Equal.sym(Nat, List.length(&2, U32, List.take(&2, U32, ys, r)), r, S.take_length(ys, r, N.lt_to_le(r, List.length(&2, U32, ys), hr))) :
871	        {Con{U32.to_nat(e), F.nats(CG(1n+k2, True{}, e2, len, t, to, sep))} == Con{Nat.add(s, _), List.take(&2, Nat, F.ends(REST, Nat.add(Nat.add(s, _), 1n)), 1n+k2)} : List<&2, Nat>}
872	      %Equal.sym(Nat, U32.to_nat(e), D.first(D.view(C.BT(len, t)), s, U32.to_nat(to), sep), he) :
873	        {Con{_, F.nats(CG(1n+k2, True{}, e2, len, t, to, sep))} == Con{Nat.add(s, r), List.take(&2, Nat, F.ends(REST, Nat.add(Nat.add(s, r), 1n)), 1n+k2)} : List<&2, Nat>}
874	      %Equal.sym(List<&2, U32>, List.drop(&2, U32, ys, Nat.add(r, 1n)), D.slice(xs, Nat.add(s, Nat.add(r, 1n)), Nat.sub(TT, Nat.add(s, Nat.add(r, 1n)))),
875	        slice_drop(xs, s, TT, Nat.add(r, 1n))) :
876	        {Con{Nat.add(s, r), F.nats(CG(1n+k2, True{}, e2, len, t, to, sep))} == Con{Nat.add(s, r), List.take(&2, Nat, F.ends(F.split(_, sep), Nat.add(Nat.add(s, r), 1n)), 1n+k2)} : List<&2, Nat>}
877	      %N.add_assoc(s, r, 1n) :
878	        {Con{Nat.add(s, r), F.nats(CG(1n+k2, True{}, e2, len, t, to, sep))} == Con{Nat.add(s, r), List.take(&2, Nat, F.ends(F.split(D.slice(xs, _, Nat.sub(TT, _)), sep), Nat.add(Nat.add(s, r), 1n)), 1n+k2)} : List<&2, Nat>}
879	      %es2 :
880	        {Con{Nat.add(s, r), F.nats(CG(1n+k2, True{}, e2, len, t, to, sep))} == Con{Nat.add(s, r), List.take(&2, Nat, F.ends(F.split(D.slice(xs, _, Nat.sub(TT, _)), sep), _), 1n+k2)} : List<&2, Nat>}
881	      %Equal.sym(List<&2, Nat>, F.nats(CG(1n+k2, True{}, e2, len, t, to, sep)), List.take(&2, Nat, F.ends(F.split(D.slice(xs, s2, Nat.sub(TT, s2)), sep), s2), 1n+k2), ih) :
882	        {Con{Nat.add(s, r), _} == Con{Nat.add(s, r), List.take(&2, Nat, F.ends(F.split(D.slice(xs, s2, Nat.sub(TT, s2)), sep), s2), 1n+k2)} : List<&2, Nat>}
883	      {==}
884	
885	# The laws
886	# ========
887	
888	law ce:
889	  for +n: Nat
890	  for +len: U32
891	  for +t: P.Tree<U32>
892	  for +d: Nat
893	  for +from: U32
894	  for +to: U32
895	  for +sep: U32
896	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
897	  for +hft: {U32.is_le(from, to) == True{} : Bool}
898	  for +ht: {Nat.is_le(U32.to_nat(to), D.size(C.BT(len, t))) == True{} : Bool}
899	  for +hs: {U32.is_lt(sep, 256) == True{} : Bool}
900	  {F.nats(Pair.snd(D.Bytes, List<&2, U32>, K.cut(C.BT(len, t), from, to, sep, n))) == List.take(&2, Nat, F.ends(F.split(D.slice(D.view(C.BT(len, t)), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), sep), U32.to_nat(from)), n) : List<&2, Nat>}
901	
902	def ce(n, len, t, d, from, to, sep, h, hft, ht, hs):
903	  match n:
904	    case 0n:
905	      +E0 = F.ends(F.split(D.slice(D.view(C.BT(len, t)), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), sep), U32.to_nat(from))
906	      %Equal.sym(D.Bytes & List<&2, U32>, K.cut(C.BT(len, t), from, to, sep, 0n),
907	        (C.BT(len, t), CG(0n, True{}, NX(Bool.not(Nat.is_eq(0n, 0n)), len, t, from, to, sep), len, t, to, sep)), cut_eq(len, t, from, to, sep, 0n)) :
908	        {F.nats(Pair.snd(D.Bytes, List<&2, U32>, _)) == List.take(&2, Nat, E0, 0n) : List<&2, Nat>}
909	      Equal.sym(List<&2, Nat>, List.take(&2, Nat, E0, 0n), Nil{}, tz(Nat, E0))
910	    case 1n+k:
911	      +E0 = F.ends(F.split(D.slice(D.view(C.BT(len, t)), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), sep), U32.to_nat(from))
912	      +e0 = FV(len, t, from, to, sep)
913	      %Equal.sym(D.Bytes & List<&2, U32>, K.cut(C.BT(len, t), from, to, sep, 1n+k),
914	        (C.BT(len, t), CG(1n+k, True{}, NX(Bool.not(Nat.is_eq(1n+k, 0n)), len, t, from, to, sep), len, t, to, sep)), cut_eq(len, t, from, to, sep, 1n+k)) :
915	        {F.nats(Pair.snd(D.Bytes, List<&2, U32>, _)) == List.take(&2, Nat, E0, 1n+k) : List<&2, Nat>}
916	      cgv(k, U32.is_lt(e0, to), U32.to_nat(from), e0, len, t, d, to, sep, h, ht,
917	        Equal.trans(Bool, Nat.is_le(U32.to_nat(from), U32.to_nat(to)), U32.is_le(from, to), True{},
918	          Equal.sym(Bool, U32.is_le(from, to), Nat.is_le(U32.to_nat(from), U32.to_nat(to)), U.is_le_to_nat(from, to)), hft),
919	        hs, FI.find_view_t(len, t, d, from, to, sep, h, hft, ht, hs), {==})
920	
921	law cut_ends_t:
922	  for +len: U32
923	  for +t: P.Tree<U32>
924	  for +d: Nat
925	  for +from: U32
926	  for +to: U32
927	  for +sep: U32
928	  for +n: Nat
929	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
930	  for +hft: {U32.is_le(from, to) == True{} : Bool}
931	  for +ht: {Nat.is_le(U32.to_nat(to), D.size(C.BT(len, t))) == True{} : Bool}
932	  for +hs: {U32.is_lt(sep, 256) == True{} : Bool}
933	  {F.nats(Pair.snd(D.Bytes, List<&2, U32>, K.cut(C.BT(len, t), from, to, sep, n))) == List.take(&2, Nat, F.ends(F.split(D.slice(D.view(C.BT(len, t)), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), sep), U32.to_nat(from)), n) : List<&2, Nat>}
934	
935	def cut_ends_t(len, t, d, from, to, sep, n, h, hft, ht, hs):
936	  ce(n, len, t, d, from, to, sep, h, hft, ht, hs)
937	
938	law cut_view_t:
939	  for +len: U32
940	  for +t: P.Tree<U32>
941	  for +d: Nat
942	  for +from: U32
943	  for +to: U32
944	  for +sep: U32
945	  for +n: Nat
946	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
947	  for +hft: {U32.is_le(from, to) == True{} : Bool}
948	  for +ht: {Nat.is_le(U32.to_nat(to), D.size(C.BT(len, t))) == True{} : Bool}
949	  for +hs: {U32.is_lt(sep, 256) == True{} : Bool}
950	  {F.pieces(Pair.snd(D.Bytes, List<&2, U32>, K.cut(C.BT(len, t), from, to, sep, n)), D.view(C.BT(len, t)), U32.to_nat(from)) == List.take(&2, List<&2, U32>, F.split(D.slice(D.view(C.BT(len, t)), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), sep), n) : List<&2, List<&2, U32>>}
951	
952	def cut_view_t(len, t, d, from, to, sep, n, h, hft, ht, hs):
953	  +xs = D.view(C.BT(len, t))
954	  +F0 = U32.to_nat(from)
955	  +TT = U32.to_nat(to)
956	  +ys = D.slice(xs, F0, Nat.sub(TT, F0))
957	  +ES = Pair.snd(D.Bytes, List<&2, U32>, K.cut(C.BT(len, t), from, to, sep, n))
958	  +E0 = F.ends(F.split(ys, sep), F0)
959	  +RHS = List.take(&2, List<&2, U32>, F.split(ys, sep), n)
960	  +hyl = ylen(len, t, d, F0, TT, h, ht)
961	  +hp = AB.subst(Nat, y => {List.take(&2, U32, List.drop(&2, U32, xs, F0), y) == ys : List<&2, U32>}, Nat.sub(TT, F0), List.length(&2, U32, ys),
962	    Equal.sym(Nat, List.length(&2, U32, ys), Nat.sub(TT, F0), hyl), {==})
963	  %Equal.sym(List<&2, List<&2, U32>>, F.pieces(ES, xs, F0), PN(F.nats(ES), xs, F0), pn(ES, xs, F0)) : {_ == RHS : List<&2, List<&2, U32>>}
964	  %Equal.sym(List<&2, Nat>, F.nats(ES), List.take(&2, Nat, E0, n), cut_ends_t(len, t, d, from, to, sep, n, h, hft, ht, hs)) :
965	    {PN(_, xs, F0) == RHS : List<&2, List<&2, U32>>}
966	  %Equal.sym(List<&2, List<&2, U32>>, PN(List.take(&2, Nat, E0, n), xs, F0), List.take(&2, List<&2, U32>, PN(E0, xs, F0), n), pntake(E0, n, xs, F0)) :
967	    {_ == RHS : List<&2, List<&2, U32>>}
968	  %Equal.sym(List<&2, List<&2, U32>>, PN(E0, xs, F0), F.split(ys, sep), pb(ys, xs, F0, sep, hp)) :
969	    {List.take(&2, List<&2, U32>, _, n) == RHS : List<&2, List<&2, U32>>}
970	  {==}
971	
972	law cut_bounds_t:
973	  for +len: U32
974	  for +t: P.Tree<U32>
975	  for +d: Nat
976	  for +from: U32
977	  for +to: U32
978	  for +sep: U32
979	  for +n: Nat
980	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
981	  for +hft: {U32.is_le(from, to) == True{} : Bool}
982	  for +ht: {Nat.is_le(U32.to_nat(to), D.size(C.BT(len, t))) == True{} : Bool}
983	  for +hs: {U32.is_lt(sep, 256) == True{} : Bool}
984	  {F.within(Pair.snd(D.Bytes, List<&2, U32>, K.cut(C.BT(len, t), from, to, sep, n)), U32.to_nat(from), U32.to_nat(to)) == True{} : Bool}
985	
986	def cut_bounds_t(len, t, d, from, to, sep, n, h, hft, ht, hs):
987	  +xs = D.view(C.BT(len, t))
988	  +F0 = U32.to_nat(from)
989	  +TT = U32.to_nat(to)
990	  +ys = D.slice(xs, F0, Nat.sub(TT, F0))
991	  +ES = Pair.snd(D.Bytes, List<&2, U32>, K.cut(C.BT(len, t), from, to, sep, n))
992	  +E0 = F.ends(F.split(ys, sep), F0)
993	  +hft2 = Equal.trans(Bool, Nat.is_le(F0, TT), U32.is_le(from, to), True{}, Equal.sym(Bool, U32.is_le(from, to), Nat.is_le(F0, TT), U.is_le_to_nat(from, to)), hft)
994	  +eT = Equal.trans(Nat, Nat.add(F0, List.length(&2, U32, ys)), Nat.add(F0, Nat.sub(TT, F0)), TT,
995	    Equal.cong(Nat, Nat, y => Nat.add(F0, y), List.length(&2, U32, ys), Nat.sub(TT, F0), ylen(len, t, d, F0, TT, h, ht)),
996	    N.le_sub_add(F0, TT, hft2))
997	  +hw = AB.subst(Nat, y => {WN(E0, F0, y) == True{} : Bool}, Nat.add(F0, List.length(&2, U32, ys)), TT, eT, wl(ys, F0, sep))
998	  %Equal.sym(Bool, F.within(ES, F0, TT), WN(F.nats(ES), F0, TT), wn(ES, F0, TT)) : {_ == True{} : Bool}
999	  %Equal.sym(List<&2, Nat>, F.nats(ES), List.take(&2, Nat, E0, n), cut_ends_t(len, t, d, from, to, sep, n, h, hft, ht, hs)) :
1000	    {WN(_, F0, TT) == True{} : Bool}
1001	  wtake(E0, n, F0, TT, hw)