proof_cut.bend

lawful-fields@0.1.1.0 · 1,001 lines · 49 definitions

1import Base
2import lawful-bytes@0.1.1.0/defs.bend as D
3import lawful-bytes@0.1.1.0/bytes.bend as B
4import lawful-fields@0.1.1.0/defs.bend as F
5import lawful-fields@0.1.1.0/fields.bend as K
6import lawful-bytes@0.1.1.0/proof_seq.bend as S
7import lawful-bytes@0.1.1.0/proof_core.bend as C
8import lawful-bytes@0.1.1.0/proof_ops.bend as O
9import lawful-bytes@0.1.1.0/proof_list.bend as Q
10import lawful-bytes@0.1.1.0/proof_append.bend as X
11import lawful-bytes@0.1.1.0/proof_shift.bend as H
12import lawful-bytes@0.1.1.0/proof_find.bend as FI
13import lawful-words@0.1.0.0/proof_nat.bend as N
14import lawful-words@0.1.0.0/proof_u32.bend as U
15import lawful-arrays@0.1.0.0/proof_base.bend as AB
16import 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
26law tz:
27  for -A: Data
28  for +xs: List<&2, A>
29  {List.take(&2, A, xs, 0n) == Nil{} : List<&2, A>}
30
31def tz(A, xs):
32  match xs:
33    case Nil{}:
34      {==}
35    case Con{x, t}:
36      {==}
37
38def is_nil_t(xs: List<&2, U32>) -> Type:
39  match xs:
40    case Nil{}:
41      Unit
42    case Con{x, t}:
43      Empty
44
45law nil_cons:
46  for -x: U32
47  for -t: List<&2, U32>
48  for e: {Nil{} == x <> t : List<&2, U32>}
49  Empty
50
51def nil_cons(x, t, e):
52  %e : is_nil_t(_)
53  Unit{}
54
55law 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
62def 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.
75law 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
82def 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.
92law 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
99def 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
107law 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
114def 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
125law 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
131def 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
140law 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
146def 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
155law 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
161def 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.
175law 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
182def 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
195def nn(ps: List<&2, List<&2, U32>>) -> Bool:
196  match ps:
197    case Nil{}:
198      False{}
199    case Con{p, t}:
200      True{}
201
202law nn_push:
203  for +c: U32
204  for +ps: List<&2, List<&2, U32>>
205  {nn(F.split.push(c, ps)) == True{} : Bool}
206
207def nn_push(c, ps):
208  match ps:
209    case Nil{}:
210      {==}
211    case Con{p, t}:
212      {==}
213
214law 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
220def nn_fin(c, ps, b):
221  match b:
222    case False{}:
223      nn_push(c, ps)
224    case True{}:
225      {==}
226
227law split_nn:
228  for +xs: List<&2, U32>
229  for +sep: U32
230  {nn(F.split(xs, sep)) == True{} : Bool}
231
232def 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
239law 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
249def 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.
268law 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
274def 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
281law 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
291def 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.
305law 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
311def 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.
322def 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
329def 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
336law 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
342def 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
352law 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
358def 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
367law 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
374def 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
386law 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
394def 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.
407law 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
416def 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
431law 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
439def 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
449law 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
457def 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.
469law 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
476def 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
486law sa:
487  for +s: Nat
488  for +l: Nat
489  {Nat.sub(Nat.add(Nat.add(s, 1n), l), s) == 1n+l : Nat}
490
491def 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
495law 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
505def 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
526law 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
538def 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.
558law 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
566def 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
577law 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
587def 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).
610law 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
616def 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
634def 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
637def 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
644def 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
654law 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
663def 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
670law 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
680def 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
698law 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
707def 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
713law 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
722def 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.
732law 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
742def 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.
753law 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
768def 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
787law 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
805def 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
888law 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
902def 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
921law 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
935def 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
938law 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
952def 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
972law 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
986def 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)