1	import Base
2	import ./defs.bend as D
3	import ./bytes.bend as B
4	import ./fast.bend as FA
5	import ./proof_seq.bend as Q
6	import ./proof_core.bend as C
7	import ./proof_ops.bend as O
8	import ./proof_append.bend as X
9	import ./proof_shift.bend as H
10	import lawful-words@0.1.0.0/defs.bend as W
11	import lawful-words@0.1.0.0/proof_nat.bend as N
12	import lawful-words@0.1.0.0/proof_u32.bend as U
13	import lawful-words@0.1.0.0/proof_bytes.bend as Y
14	import lawful-arrays@0.1.0.0/defs.bend as A
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	import lawful-arrays@0.1.0.0/proof_index.bend as I
18	
19	# fast.bend's append on the mirror. The first bytes go through bytes.bend's
20	# append (X.append_*_t), up to dst's next word boundary; then append.words
21	# writes whole words, each the merge of two src words. AWT computes the tree
22	# append.words leaves (aw_eq), and the view invariant (av) says that after the
23	# words written so far the bytes in use are the target's. Up to 3 bytes past
24	# the new length come from src bytes past s + n: they are outside the view.
25	
26	# Lists
27	# =====
28	
29	law drop_drop:
30	  for +xs: List<&2, U32>
31	  for +a: Nat
32	  for +b: Nat
33	  {List.drop(&2, U32, List.drop(&2, U32, xs, a), b) == List.drop(&2, U32, xs, Nat.add(a, b)) : List<&2, U32>}
34	
35	def drop_drop(xs, a, b):
36	  match xs a:
37	    case Nil{} _:
38	      {==}
39	    case Con{x, t} 0n:
40	      {==}
41	    case Con{x, t} 1n+p:
42	      drop_drop(t, p, b)
43	
44	# A list whose first element is b.
45	law tcons:
46	  for +ys: List<&2, U32>
47	  for +b: U32
48	  for +m: Nat
49	  for +rest: List<&2, U32>
50	  for +h: {List.get(&2, U32, ys, 0n) == Some{b} : Maybe<&2, U32>}
51	  for +ht: {List.take(&2, U32, List.drop(&2, U32, ys, 1n), m) == rest : List<&2, U32>}
52	  {List.take(&2, U32, ys, 1n+m) == b <> rest : List<&2, U32>}
53	
54	def tcons(ys, b, m, rest, h, ht):
55	  match ys:
56	    case Nil{}:
57	      Empty.absurd({List.take(&2, U32, Nil{}, 1n+m) == b <> rest : List<&2, U32>}, X.none_some(b, h))
58	    case Con{+y, t}:
59	      %Equal.sym(U32, y, b, X.some_inj(y, b, h)) : {_ <> List.take(&2, U32, t, m) == b <> rest : List<&2, U32>}
60	      %Equal.sym(List<&2, U32>, List.take(&2, U32, t, m), rest,
61	        AB.subst(List<&2, U32>, z => {List.take(&2, U32, z, m) == rest : List<&2, U32>}, List.drop(&2, U32, t, 0n), t, X.drop_zero(t), ht)) :
62	        {b <> _ == b <> rest : List<&2, U32>}
63	      {==}
64	
65	# The first m (<= 4) elements of ys are b0 .. b3, given each one asked for.
66	law tg1:
67	  for +ys: List<&2, U32>
68	  for +m: Nat
69	  for +b0: U32
70	  for +hm: {Nat.is_le(m, 1n) == True{} : Bool}
71	  for g0: {Nat.is_lt(0n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 0n) == Some{b0} : Maybe<&2, U32>}
72	  {List.take(&2, U32, ys, m) == List.take(&2, U32, [b0], m) : List<&2, U32>}
73	
74	def tg1(ys, m, b0, hm, g0):
75	  match m:
76	    case 0n:
77	      Q.take_zero(ys)
78	    case 1n+m1:
79	      match m1:
80	        case 0n:
81	          tcons(ys, b0, 0n, Nil{}, g0({==}), Q.take_zero(List.drop(&2, U32, ys, 1n)))
82	        case 1n+m2:
83	          Empty.absurd({List.take(&2, U32, ys, 2n+m2) == List.take(&2, U32, [b0], 2n+m2) : List<&2, U32>}, AB.false_ne_true(hm))
84	
85	law tg2:
86	  for +ys: List<&2, U32>
87	  for +m: Nat
88	  for +b0: U32
89	  for +b1: U32
90	  for +hm: {Nat.is_le(m, 2n) == True{} : Bool}
91	  for g0: {Nat.is_lt(0n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 0n) == Some{b0} : Maybe<&2, U32>}
92	  for g1: {Nat.is_lt(1n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 1n) == Some{b1} : Maybe<&2, U32>}
93	  {List.take(&2, U32, ys, m) == List.take(&2, U32, [b0, b1], m) : List<&2, U32>}
94	
95	def tg2(ys, m, b0, b1, hm, g0, g1):
96	  match m:
97	    case 0n:
98	      Q.take_zero(ys)
99	    case 1n+m1:
100	      tcons(ys, b0, m1, List.take(&2, U32, [b1], m1), g0({==}),
101	        tg1(List.drop(&2, U32, ys, 1n), m1, b1, hm,
102	          h => Equal.trans(Maybe<&2, U32>, List.get(&2, U32, List.drop(&2, U32, ys, 1n), 0n), List.get(&2, U32, ys, 1n), Some{b1},
103	            H.get_drop(ys, 1n, 0n), g1(h))))
104	
105	law tg3:
106	  for +ys: List<&2, U32>
107	  for +m: Nat
108	  for +b0: U32
109	  for +b1: U32
110	  for +b2: U32
111	  for +hm: {Nat.is_le(m, 3n) == True{} : Bool}
112	  for g0: {Nat.is_lt(0n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 0n) == Some{b0} : Maybe<&2, U32>}
113	  for g1: {Nat.is_lt(1n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 1n) == Some{b1} : Maybe<&2, U32>}
114	  for g2: {Nat.is_lt(2n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 2n) == Some{b2} : Maybe<&2, U32>}
115	  {List.take(&2, U32, ys, m) == List.take(&2, U32, [b0, b1, b2], m) : List<&2, U32>}
116	
117	def tg3(ys, m, b0, b1, b2, hm, g0, g1, g2):
118	  match m:
119	    case 0n:
120	      Q.take_zero(ys)
121	    case 1n+m1:
122	      tcons(ys, b0, m1, List.take(&2, U32, [b1, b2], m1), g0({==}),
123	        tg2(List.drop(&2, U32, ys, 1n), m1, b1, b2, hm,
124	          h => Equal.trans(Maybe<&2, U32>, List.get(&2, U32, List.drop(&2, U32, ys, 1n), 0n), List.get(&2, U32, ys, 1n), Some{b1},
125	            H.get_drop(ys, 1n, 0n), g1(h)),
126	          h => Equal.trans(Maybe<&2, U32>, List.get(&2, U32, List.drop(&2, U32, ys, 1n), 1n), List.get(&2, U32, ys, 2n), Some{b2},
127	            H.get_drop(ys, 1n, 1n), g2(h))))
128	
129	law tg4:
130	  for +ys: List<&2, U32>
131	  for +m: Nat
132	  for +b0: U32
133	  for +b1: U32
134	  for +b2: U32
135	  for +b3: U32
136	  for +hm: {Nat.is_le(m, 4n) == True{} : Bool}
137	  for g0: {Nat.is_lt(0n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 0n) == Some{b0} : Maybe<&2, U32>}
138	  for g1: {Nat.is_lt(1n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 1n) == Some{b1} : Maybe<&2, U32>}
139	  for g2: {Nat.is_lt(2n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 2n) == Some{b2} : Maybe<&2, U32>}
140	  for g3: {Nat.is_lt(3n, m) == True{} : Bool} -> {List.get(&2, U32, ys, 3n) == Some{b3} : Maybe<&2, U32>}
141	  {List.take(&2, U32, ys, m) == List.take(&2, U32, [b0, b1, b2, b3], m) : List<&2, U32>}
142	
143	def tg4(ys, m, b0, b1, b2, b3, hm, g0, g1, g2, g3):
144	  match m:
145	    case 0n:
146	      Q.take_zero(ys)
147	    case 1n+m1:
148	      tcons(ys, b0, m1, List.take(&2, U32, [b1, b2, b3], m1), g0({==}),
149	        tg3(List.drop(&2, U32, ys, 1n), m1, b1, b2, b3, hm,
150	          h => Equal.trans(Maybe<&2, U32>, List.get(&2, U32, List.drop(&2, U32, ys, 1n), 0n), List.get(&2, U32, ys, 1n), Some{b1},
151	            H.get_drop(ys, 1n, 0n), g1(h)),
152	          h => Equal.trans(Maybe<&2, U32>, List.get(&2, U32, List.drop(&2, U32, ys, 1n), 1n), List.get(&2, U32, ys, 2n), Some{b2},
153	            H.get_drop(ys, 1n, 1n), g2(h)),
154	          h => Equal.trans(Maybe<&2, U32>, List.get(&2, U32, List.drop(&2, U32, ys, 1n), 2n), List.get(&2, U32, ys, 3n), Some{b3},
155	            H.get_drop(ys, 1n, 2n), g3(h))))
156	
157	# Writing word q replaces bytes 4q .. 4q+3 of the unpacked list.
158	law us1:
159	  for +ws: List<&2, U32>
160	  for +q: Nat
161	  for +x: U32
162	  for +m: Nat
163	  for +hq: {Nat.is_lt(q, List.length(&2, U32, ws)) == True{} : Bool}
164	  for +hm: {Nat.is_le(m, 4n) == True{} : Bool}
165	  {List.take(&2, U32, D.unpack(List.set(&2, U32, ws, q, x)), Nat.add(Nat.mul(q, 4n), m)) == List.append(&2, U32, List.take(&2, U32, D.unpack(ws), Nat.mul(q, 4n)), List.take(&2, U32, C.L4(x), m)) : List<&2, U32>}
166	
167	def us1(ws, q, x, m, hq, hm):
168	  match ws q:
169	    case Nil{} _:
170	      Empty.absurd({List.take(&2, U32, Nil{}, Nat.add(Nat.mul(q, 4n), m)) == List.append(&2, U32, List.take(&2, U32, Nil{}, Nat.mul(q, 4n)), List.take(&2, U32, C.L4(x), m)) : List<&2, U32>},
171	        AB.lt_zero_absurd(q, hq))
172	    case Con{w0, t} 0n:
173	      Q.take_append_l(C.L4(x), D.unpack(t), m, hm)
174	    case Con{+w0, t} 1n+p:
175	      %us1(t, p, x, m, hq, hm) :
176	        {W.byte(w0, 0n) <> W.byte(w0, 1n) <> W.byte(w0, 2n) <> W.byte(w0, 3n) <> List.take(&2, U32, D.unpack(List.set(&2, U32, t, p, x)), Nat.add(Nat.mul(p, 4n), m))
177	          == W.byte(w0, 0n) <> W.byte(w0, 1n) <> W.byte(w0, 2n) <> W.byte(w0, 3n) <> _ : List<&2, U32>}
178	      {==}
179	
180	law take_split:
181	  for +ys: List<&2, U32>
182	  for +a: Nat
183	  for +m: Nat
184	  {List.append(&2, U32, List.take(&2, U32, ys, a), List.take(&2, U32, List.drop(&2, U32, ys, a), m)) == List.take(&2, U32, ys, Nat.add(a, m)) : List<&2, U32>}
185	
186	def take_split(ys, a, m):
187	  match ys a:
188	    case Nil{} _:
189	      {==}
190	    case Con{y, t} 0n:
191	      {==}
192	    case Con{+y, t} 1n+p:
193	      %take_split(t, p, m) :
194	        {y <> List.append(&2, U32, List.take(&2, U32, t, p), List.take(&2, U32, List.drop(&2, U32, t, p), m)) == y <> _ : List<&2, U32>}
195	      {==}
196	
197	law slice_split:
198	  for +xs: List<&2, U32>
199	  for +s: Nat
200	  for +a: Nat
201	  for +b: Nat
202	  {List.append(&2, U32, D.slice(xs, s, a), D.slice(xs, Nat.add(s, a), b)) == D.slice(xs, s, Nat.add(a, b)) : List<&2, U32>}
203	
204	def slice_split(xs, s, a, b):
205	  %drop_drop(xs, s, a) :
206	    {List.append(&2, U32, D.slice(xs, s, a), List.take(&2, U32, _, b)) == D.slice(xs, s, Nat.add(a, b)) : List<&2, U32>}
207	  take_split(List.drop(&2, U32, xs, s), a, b)
208	
209	# A slice of the first l elements, inside them.
210	law slice_take:
211	  for +xs: List<&2, U32>
212	  for +l: Nat
213	  for +q: Nat
214	  for +n: Nat
215	  for +h: {Nat.is_le(Nat.add(q, n), l) == True{} : Bool}
216	  {D.slice(List.take(&2, U32, xs, l), q, n) == List.take(&2, U32, List.drop(&2, U32, xs, q), n) : List<&2, U32>}
217	
218	def slice_take(xs, l, q, n, h):
219	  match xs l q n:
220	    case Nil{} _ _ _:
221	      {==}
222	    case Con{x, t} 0n 0n 0n:
223	      {==}
224	    case Con{x, t} 0n 0n 1n+n1:
225	      Empty.absurd({List.take(&2, U32, Nil{}, 1n+n1) == x <> List.take(&2, U32, t, n1) : List<&2, U32>}, AB.false_ne_true(h))
226	    case Con{x, t} 0n 1n+q1 _:
227	      Empty.absurd({List.take(&2, U32, List.drop(&2, U32, Nil{}, 1n+q1), n) == List.take(&2, U32, List.drop(&2, U32, t, q1), n) : List<&2, U32>},
228	        AB.false_ne_true(h))
229	    case Con{x, t} 1n+l1 0n _:
230	      Q.take_take(x <> t, 1n+l1, n, h)
231	    case Con{x, t} 1n+l1 1n+q1 _:
232	      slice_take(t, l1, q1, n, h)
233	
234	law slice_length:
235	  for +xs: List<&2, U32>
236	  for +s: Nat
237	  for +a: Nat
238	  for +h: {Nat.is_le(Nat.add(s, a), List.length(&2, U32, xs)) == True{} : Bool}
239	  {List.length(&2, U32, D.slice(xs, s, a)) == a : Nat}
240	
241	def slice_length(xs, s, a, h):
242	  Q.take_length(List.drop(&2, U32, xs, s), a,
243	    AB.subst(Nat, y => {Nat.is_le(a, y) == True{} : Bool}, Nat.sub(List.length(&2, U32, xs), s), List.length(&2, U32, List.drop(&2, U32, xs, s)),
244	      Equal.sym(Nat, List.length(&2, U32, List.drop(&2, U32, xs, s)), Nat.sub(List.length(&2, U32, xs), s), H.drop_length(xs, s)),
245	      N.le_sub_r(s, a, List.length(&2, U32, xs), h)))
246	
247	# Nat
248	# ===
249	
250	law le_antisym:
251	  for +a: Nat
252	  for +b: Nat
253	  for +h1: {Nat.is_le(a, b) == True{} : Bool}
254	  for +h2: {Nat.is_le(b, a) == True{} : Bool}
255	  {a == b : Nat}
256	
257	def le_antisym(a, b, h1, h2):
258	  match a b:
259	    case 0n 0n:
260	      {==}
261	    case 0n 1n+q:
262	      Empty.absurd({0n == 1n+q : Nat}, AB.false_ne_true(h2))
263	    case 1n+p 0n:
264	      Empty.absurd({1n+p == 0n : Nat}, AB.false_ne_true(h1))
265	    case 1n+p 1n+q:
266	      %le_antisym(p, q, h1, h2) : {1n+p == 1n+_ : Nat}
267	      {==}
268	
269	law min_l:
270	  for +a: Nat
271	  for +b: Nat
272	  for +h: {Nat.is_lt(a, b) == True{} : Bool}
273	  {Nat.min(a, b) == a : Nat}
274	
275	def min_l(a, b, h):
276	  match a b:
277	    case 0n _:
278	      {==}
279	    case 1n+p 0n:
280	      Empty.absurd({0n == 1n+p : Nat}, AB.false_ne_true(h))
281	    case 1n+p 1n+q:
282	      %min_l(p, q, h) : {1n+Nat.min(p, q) == 1n+_ : Nat}
283	      {==}
284	
285	law min_r:
286	  for +a: Nat
287	  for +b: Nat
288	  for +h: {Nat.is_lt(a, b) == False{} : Bool}
289	  {Nat.min(a, b) == b : Nat}
290	
291	def min_r(a, b, h):
292	  match a b:
293	    case 0n 0n:
294	      {==}
295	    case 0n 1n+q:
296	      Empty.absurd({0n == 1n+q : Nat}, AB.true_ne_false(h))
297	    case 1n+p 0n:
298	      {==}
299	    case 1n+p 1n+q:
300	      %min_r(p, q, h) : {1n+Nat.min(p, q) == 1n+_ : Nat}
301	      {==}
302	
303	law min_le:
304	  for +a: Nat
305	  for +b: Nat
306	  {Nat.is_le(Nat.min(a, b), b) == True{} : Bool}
307	
308	def min_le(a, b):
309	  match a b:
310	    case 0n _:
311	      N.le_zero_l(b)
312	    case 1n+p 0n:
313	      {==}
314	    case 1n+p 1n+q:
315	      min_le(p, q)
316	
317	law lt_w:
318	  for +w: Nat
319	  for +x: Nat
320	  for +pp: Nat
321	  for +h: {Nat.is_lt(Nat.add(Nat.mul(w, 4n), x), Nat.mul(4n, pp)) == True{} : Bool}
322	  {Nat.is_lt(w, pp) == True{} : Bool}
323	
324	def lt_w(w, x, pp, h):
325	  N.lt_mul_cancel(4n, w, pp,
326	    AB.subst(Nat, y => {Nat.is_lt(y, Nat.mul(4n, pp)) == True{} : Bool}, Nat.mul(w, 4n), Nat.mul(4n, w), N.mul_comm(w, 4n),
327	      N.le_lt_trans(Nat.mul(w, 4n), Nat.add(Nat.mul(w, 4n), x), Nat.mul(4n, pp), N.le_add_r(Nat.mul(w, 4n), x), h)))
328	
329	law lt8:
330	  for +r: Nat
331	  for +j: Nat
332	  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
333	  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
334	  {Nat.is_lt(Nat.add(r, j), 8n) == True{} : Bool}
335	
336	def lt8(r, j, hr, hj):
337	  match r:
338	    case 0n:
339	      N.lt_trans(j, 4n, 8n, hj, {==})
340	    case 1n+r1:
341	      match r1:
342	        case 0n:
343	          N.lt_trans(j, 4n, 7n, hj, {==})
344	        case 1n+r2:
345	          match r2:
346	            case 0n:
347	              N.lt_trans(j, 4n, 6n, hj, {==})
348	            case 1n+r3:
349	              match r3:
350	                case 0n:
351	                  N.lt_trans(j, 4n, 5n, hj, {==})
352	                case 1n+r4:
353	                  Empty.absurd({Nat.is_lt(Nat.add(4n+r4, j), 8n) == True{} : Bool}, AB.lt_zero_absurd(r4, hr))
354	
355	law sub4_lt:
356	  for +x: Nat
357	  for +h: {Nat.is_lt(x, 8n) == True{} : Bool}
358	  {Nat.is_lt(Nat.sub(x, 4n), 4n) == True{} : Bool}
359	
360	def sub4_lt(x, h):
361	  match x:
362	    case 0n:
363	      {==}
364	    case 1n+x1:
365	      match x1:
366	        case 0n:
367	          {==}
368	        case 1n+x2:
369	          match x2:
370	            case 0n:
371	              {==}
372	            case 1n+x3:
373	              match x3:
374	                case 0n:
375	                  {==}
376	                case 1n+x4:
377	                  %Equal.sym(Nat, Nat.sub(x4, 0n), x4, N.sub_zero(x4)) : {Nat.is_lt(_, 4n) == True{} : Bool}
378	                  h
379	
380	# Index 4w + x for x >= 4 is index 4(w + 1) + (x - 4).
381	law idx_up:
382	  for +w: Nat
383	  for +x: Nat
384	  for +h: {Nat.is_le(4n, x) == True{} : Bool}
385	  {Nat.add(Nat.mul(w, 4n), x) == Nat.add(Nat.mul(1n+w, 4n), Nat.sub(x, 4n)) : Nat}
386	
387	def idx_up(w, x, h):
388	  %Equal.sym(Nat, x, Nat.add(4n, Nat.sub(x, 4n)), Equal.sym(Nat, Nat.add(4n, Nat.sub(x, 4n)), x, N.le_sub_add(4n, x, h))) :
389	    {Nat.add(Nat.mul(w, 4n), _) == Nat.add(Nat.mul(1n+w, 4n), Nat.sub(x, 4n)) : Nat}
390	  N.add_left_comm(Nat.mul(w, 4n), 4n, Nat.sub(x, 4n))
391	
392	# Words and shifts
393	# ================
394	
395	# The tree append.words leaves: p is the word read next (hi), lo the word
396	# before it, td the dst block, di the dst word written, sh the shift in bits.
397	def AWT(n: Nat, +ts: P.Tree<U32>, +p: U32, +lo: U32, +td: P.Tree<U32>, +si: U32, +di: U32, +sh: Nat) -> P.Tree<U32>:
398	  match n:
399	    case 0n:
400	      td
401	    case 1n+k:
402	      +hi = C.WD(ts, p)
403	      AWT(k, ts, (si + 2 : U32), hi, I.set_tree(U32, td, di, U32.or(U32.shrn(lo, sh), U32.shln(hi, Nat.sub(32n, sh)))), (si + 1 : U32), (di + 1 : U32), sh)
404	
405	law aw_eq:
406	  for +n: Nat
407	  for +ts: P.Tree<U32>
408	  for +p: U32
409	  for +lo: U32
410	  for +td: P.Tree<U32>
411	  for +si: U32
412	  for +di: U32
413	  for +sh: Nat
414	  {FA.append.words(n, Array.get(U32, P.fromT(U32, ts), p), lo, P.fromT(U32, td), si, di, sh) == (P.fromT(U32, AWT(n, ts, p, lo, td, si, di, sh)), P.fromT(U32, ts)) : Array<U32> & Array<U32>}
415	
416	def aw_eq(n, ts, p, lo, td, si, di, sh):
417	  match n:
418	    case 0n:
419	      %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, ts), p), (P.fromT(U32, ts), C.WD(ts, p)), P.get_pair_t(U32, ts, p)) :
420	        {FA.append.words(0n, _, lo, P.fromT(U32, td), si, di, sh) == (P.fromT(U32, td), P.fromT(U32, ts)) : Array<U32> & Array<U32>}
421	      {==}
422	    case 1n+k:
423	      +hi = C.WD(ts, p)
424	      +mw = U32.or(U32.shrn(lo, sh), U32.shln(hi, Nat.sub(32n, sh)))
425	      %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, ts), p), (P.fromT(U32, ts), hi), P.get_pair_t(U32, ts, p)) :
426	        {FA.append.words(1n+k, _, lo, P.fromT(U32, td), si, di, sh) == (P.fromT(U32, AWT(1n+k, ts, p, lo, td, si, di, sh)), P.fromT(U32, ts)) : Array<U32> & Array<U32>}
427	      %Equal.sym(Array<U32>, Array.set(U32, P.fromT(U32, td), di, mw), P.fromT(U32, I.set_tree(U32, td, di, mw)), I.set_tree_eq(U32, td, di, mw)) :
428	        {FA.append.words(k, Array.get(U32, P.fromT(U32, ts), (si + 2 : U32)), hi, _, (si + 1 : U32), (di + 1 : U32), sh) == (P.fromT(U32, AWT(k, ts, (si + 2 : U32), hi, I.set_tree(U32, td, di, mw), (si + 1 : U32), (di + 1 : U32), sh)), P.fromT(U32, ts)) : Array<U32> & Array<U32>}
429	      aw_eq(k, ts, (si + 2 : U32), hi, I.set_tree(U32, td, di, mw), (si + 1 : U32), (di + 1 : U32), sh)
430	
431	# The code's shifted pair is lawful-words' merge.
432	law mrg2:
433	  for +lo: U32
434	  for +hi: U32
435	  for +r: Nat
436	  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
437	  {U32.or(U32.shrn(lo, Nat.mul(8n, r)), U32.shln(hi, Nat.sub(32n, Nat.mul(8n, r)))) == W.merge(lo, hi, r) : U32}
438	
439	def mrg2(lo, hi, r, hr):
440	  match r:
441	    case 0n:
442	      {==}
443	    case 1n+r1:
444	      match r1:
445	        case 0n:
446	          {==}
447	        case 1n+r2:
448	          match r2:
449	            case 0n:
450	              {==}
451	            case 1n+r3:
452	              match r3:
453	                case 0n:
454	                  {==}
455	                case 1n+r4:
456	                  Empty.absurd({U32.or(U32.shrn(lo, Nat.mul(8n, 4n+r4)), U32.shln(hi, Nat.sub(32n, Nat.mul(8n, 4n+r4)))) == W.merge(lo, hi, 4n+r4) : U32},
457	                    AB.lt_zero_absurd(r4, hr))
458	
459	law mrg:
460	  for +lo: U32
461	  for +hi: U32
462	  for +sh: Nat
463	  for +r: Nat
464	  for +hsh: {sh == Nat.mul(8n, r) : Nat}
465	  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
466	  {U32.or(U32.shrn(lo, sh), U32.shln(hi, Nat.sub(32n, sh))) == W.merge(lo, hi, r) : U32}
467	
468	def mrg(lo, hi, sh, r, hsh, hr):
469	  %Equal.sym(Nat, sh, Nat.mul(8n, r), hsh) : {U32.or(U32.shrn(lo, _), U32.shln(hi, Nat.sub(32n, _))) == W.merge(lo, hi, r) : U32}
470	  mrg2(lo, hi, r, hr)
471	
472	law and3_lt:
473	  for +q: U32
474	  {Nat.is_lt(U32.to_nat((q .&. 3 : U32)), 4n) == True{} : Bool}
475	
476	def and3_lt(q):
477	  AB.subst(Nat, y => {Nat.is_lt(y, 4n) == True{} : Bool}, Nat.mod(U32.to_nat(q), 4n), U32.to_nat((q .&. 3 : U32)),
478	    Equal.sym(Nat, U32.to_nat((q .&. 3 : U32)), Nat.mod(U32.to_nat(q), 4n), U.to_nat_and_mask(q, 3, 2n, {==})),
479	    N.mod_lt(U32.to_nat(q), 4n, {==}))
480	
481	law shq2:
482	  for +x: U32
483	  for +r: Nat
484	  for +e: {U32.to_nat(x) == r : Nat}
485	  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
486	  {U32.to_nat((x << 3n : U32)) == Nat.mul(8n, U32.to_nat(x)) : Nat}
487	
488	def shq2(x, r, e, hr):
489	  match r:
490	    case 0n:
491	      %Equal.sym(U32, x, 0, U.to_nat_inj(x, 0, e)) : {U32.to_nat((_ << 3n : U32)) == Nat.mul(8n, U32.to_nat(_)) : Nat}
492	      {==}
493	    case 1n+r1:
494	      match r1:
495	        case 0n:
496	          %Equal.sym(U32, x, 1, U.to_nat_inj(x, 1, e)) : {U32.to_nat((_ << 3n : U32)) == Nat.mul(8n, U32.to_nat(_)) : Nat}
497	          {==}
498	        case 1n+r2:
499	          match r2:
500	            case 0n:
501	              %Equal.sym(U32, x, 2, U.to_nat_inj(x, 2, e)) : {U32.to_nat((_ << 3n : U32)) == Nat.mul(8n, U32.to_nat(_)) : Nat}
502	              {==}
503	            case 1n+r3:
504	              match r3:
505	                case 0n:
506	                  %Equal.sym(U32, x, 3, U.to_nat_inj(x, 3, e)) : {U32.to_nat((_ << 3n : U32)) == Nat.mul(8n, U32.to_nat(_)) : Nat}
507	                  {==}
508	                case 1n+r4:
509	                  Empty.absurd({U32.to_nat((x << 3n : U32)) == Nat.mul(8n, U32.to_nat(x)) : Nat}, AB.lt_zero_absurd(r4, hr))
510	
511	# The shift of append.w is 8 * (q & 3).
512	law shq:
513	  for +q: U32
514	  {U32.to_nat(((q .&. 3 : U32) << 3n : U32)) == Nat.mul(8n, U32.to_nat((q .&. 3 : U32))) : Nat}
515	
516	def shq(q):
517	  shq2((q .&. 3 : U32), U32.to_nat((q .&. 3 : U32)), {==}, and3_lt(q))
518	
519	# Bytes of a merged word
520	# ======================
521	
522	def US(+ts: P.Tree<U32>) -> List<&2, U32>:
523	  D.unpack(C.WL(ts))
524	
525	law mb_lo:
526	  for +ts: P.Tree<U32>
527	  for +e: Nat
528	  for +si: U32
529	  for +p: U32
530	  for +lo: U32
531	  for +r: Nat
532	  for +j: Nat
533	  for +hf: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
534	  for +he: {Nat.is_le(e, 29n) == True{} : Bool}
535	  for +hlo: {lo == C.WD(ts, si) : U32}
536	  for +hb: {Nat.is_lt(Nat.add(Nat.mul(U32.to_nat(si), 4n), Nat.add(r, j)), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
537	  for +hq: {Nat.is_lt(Nat.add(r, j), 4n) == True{} : Bool}
538	  {List.get(&2, U32, US(ts), Nat.add(Nat.mul(U32.to_nat(si), 4n), Nat.add(r, j))) == Some{W.byte(W.merge(lo, C.WD(ts, p), r), j)} : Maybe<&2, U32>}
539	
540	def mb_lo(ts, e, si, p, lo, r, j, hf, he, hlo, hb, hq):
541	  +w = U32.to_nat(si)
542	  +hi = C.WD(ts, p)
543	  +RHS = {Some{W.byte(W.merge(lo, hi, r), j)} : Maybe<&2, U32>}
544	  %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, US(ts), Nat.add(Nat.mul(w, 4n), Nat.add(r, j))), C.mb(List.get(&2, U32, C.WL(ts), w), Nat.add(r, j)),
545	    C.unpack_get(C.WL(ts), w, Nat.add(r, j), hq)) :
546	    {_ == RHS : Maybe<&2, U32>}
547	  %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, C.WL(ts), w), Some{C.WD(ts, si)}, C.wd_get(ts, e, si, hf, he, lt_w(w, Nat.add(r, j), Nat.pow(2n, e), hb))) :
548	    {C.mb(_, Nat.add(r, j)) == RHS : Maybe<&2, U32>}
549	  %Equal.sym(U32, W.byte(W.merge(lo, hi, r), j), W.byte(lo, Nat.add(j, r)),
550	    Y.byte_merge_lo(lo, hi, r, j, AB.subst(Nat, y => {Nat.is_lt(y, 4n) == True{} : Bool}, Nat.add(r, j), Nat.add(j, r), N.add_comm(r, j), hq))) :
551	    {Some{W.byte(C.WD(ts, si), Nat.add(r, j))} == Some{_} : Maybe<&2, U32>}
552	  %Equal.sym(U32, lo, C.WD(ts, si), hlo) : {Some{W.byte(C.WD(ts, si), Nat.add(r, j))} == Some{W.byte(_, Nat.add(j, r))} : Maybe<&2, U32>}
553	  %N.add_comm(r, j) : {Some{W.byte(C.WD(ts, si), Nat.add(r, j))} == Some{W.byte(C.WD(ts, si), _)} : Maybe<&2, U32>}
554	  {==}
555	
556	law mb_hi:
557	  for +ts: P.Tree<U32>
558	  for +e: Nat
559	  for +si: U32
560	  for +p: U32
561	  for +lo: U32
562	  for +r: Nat
563	  for +j: Nat
564	  for +hf: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
565	  for +he: {Nat.is_le(e, 29n) == True{} : Bool}
566	  for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat}
567	  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
568	  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
569	  for +hb: {Nat.is_lt(Nat.add(Nat.mul(U32.to_nat(si), 4n), Nat.add(r, j)), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
570	  for +hq: {Nat.is_lt(Nat.add(r, j), 4n) == False{} : Bool}
571	  {List.get(&2, U32, US(ts), Nat.add(Nat.mul(U32.to_nat(si), 4n), Nat.add(r, j))) == Some{W.byte(W.merge(lo, C.WD(ts, p), r), j)} : Maybe<&2, U32>}
572	
573	def mb_hi(ts, e, si, p, lo, r, j, hf, he, hp, hr, hj, hb, hq):
574	  +w = U32.to_nat(si)
575	  +hi = C.WD(ts, p)
576	  +x = Nat.add(r, j)
577	  +z = Nat.sub(x, 4n)
578	  +RHS = {Some{W.byte(W.merge(lo, hi, r), j)} : Maybe<&2, U32>}
579	  +h4 = N.not_lt_le(x, 4n, hq)
580	  +eu = idx_up(w, x, h4)
581	  +hz = sub4_lt(x, lt8(r, j, hr, hj))
582	  +ep = Equal.trans(Nat, U32.to_nat(p), Nat.add(w, 1n), 1n+w, hp, N.add_one(w))
583	  +hb2 = AB.subst(Nat, y => {Nat.is_lt(y, Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}, Nat.add(Nat.mul(w, 4n), x), Nat.add(Nat.mul(1n+w, 4n), z), eu, hb)
584	  +hpl = AB.subst(Nat, y => {Nat.is_lt(y, Nat.pow(2n, e)) == True{} : Bool}, 1n+w, U32.to_nat(p), Equal.sym(Nat, U32.to_nat(p), 1n+w, ep),
585	    lt_w(1n+w, z, Nat.pow(2n, e), hb2))
586	  +gp = AB.subst(Nat, y => {List.get(&2, U32, C.WL(ts), y) == Some{hi} : Maybe<&2, U32>}, U32.to_nat(p), 1n+w, ep, C.wd_get(ts, e, p, hf, he, hpl))
587	  %Equal.sym(Nat, Nat.add(Nat.mul(w, 4n), x), Nat.add(Nat.mul(1n+w, 4n), z), eu) : {List.get(&2, U32, US(ts), _) == RHS : Maybe<&2, U32>}
588	  %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, US(ts), Nat.add(Nat.mul(1n+w, 4n), z)), C.mb(List.get(&2, U32, C.WL(ts), 1n+w), z),
589	    C.unpack_get(C.WL(ts), 1n+w, z, hz)) :
590	    {_ == RHS : Maybe<&2, U32>}
591	  %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, C.WL(ts), 1n+w), Some{hi}, gp) : {C.mb(_, z) == RHS : Maybe<&2, U32>}
592	  %Equal.sym(U32, W.byte(W.merge(lo, hi, r), j), W.byte(hi, Nat.sub(Nat.add(j, r), 4n)),
593	    Y.byte_merge_hi(lo, hi, r, j, N.lt_to_le(r, 4n, hr), hj,
594	      AB.subst(Nat, y => {Nat.is_le(4n, y) == True{} : Bool}, x, Nat.add(j, r), N.add_comm(r, j), h4))) :
595	    {Some{W.byte(hi, z)} == Some{_} : Maybe<&2, U32>}
596	  %N.add_comm(r, j) : {Some{W.byte(hi, z)} == Some{W.byte(hi, Nat.sub(_, 4n))} : Maybe<&2, U32>}
597	  {==}
598	
599	law gsel:
600	  for +ts: P.Tree<U32>
601	  for +e: Nat
602	  for +si: U32
603	  for +p: U32
604	  for +lo: U32
605	  for +r: Nat
606	  for +j: Nat
607	  for +b: Bool
608	  for +hf: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
609	  for +he: {Nat.is_le(e, 29n) == True{} : Bool}
610	  for +hlo: {lo == C.WD(ts, si) : U32}
611	  for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat}
612	  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
613	  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
614	  for +hb: {Nat.is_lt(Nat.add(Nat.mul(U32.to_nat(si), 4n), Nat.add(r, j)), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
615	  for +hq: {Nat.is_lt(Nat.add(r, j), 4n) == b : Bool}
616	  {List.get(&2, U32, US(ts), Nat.add(Nat.mul(U32.to_nat(si), 4n), Nat.add(r, j))) == Some{W.byte(W.merge(lo, C.WD(ts, p), r), j)} : Maybe<&2, U32>}
617	
618	def gsel(ts, e, si, p, lo, r, j, b, hf, he, hlo, hp, hr, hj, hb, hq):
619	  match b:
620	    case True{}:
621	      mb_lo(ts, e, si, p, lo, r, j, hf, he, hlo, hb, hq)
622	    case False{}:
623	      mb_hi(ts, e, si, p, lo, r, j, hf, he, hp, hr, hj, hb, hq)
624	
625	# Byte j of the window at 4 si + r, for j below m.
626	law gj:
627	  for +ts: P.Tree<U32>
628	  for +e: Nat
629	  for +si: U32
630	  for +p: U32
631	  for +lo: U32
632	  for +r: Nat
633	  for +m: Nat
634	  for +j: Nat
635	  for +hf: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
636	  for +he: {Nat.is_le(e, 29n) == True{} : Bool}
637	  for +hlo: {lo == C.WD(ts, si) : U32}
638	  for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat}
639	  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
640	  for +hm: {Nat.is_le(m, 4n) == True{} : Bool}
641	  for +hb: {Nat.is_le(Nat.add(Nat.add(Nat.mul(U32.to_nat(si), 4n), r), m), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
642	  for +hjm: {Nat.is_lt(j, m) == True{} : Bool}
643	  {List.get(&2, U32, List.drop(&2, U32, US(ts), Nat.add(Nat.mul(U32.to_nat(si), 4n), r)), j) == Some{W.byte(W.merge(lo, C.WD(ts, p), r), j)} : Maybe<&2, U32>}
644	
645	def gj(ts, e, si, p, lo, r, m, j, hf, he, hlo, hp, hr, hm, hb, hjm):
646	  +X = Nat.mul(U32.to_nat(si), 4n)
647	  +ea = N.add_assoc(X, r, j)
648	  +hbj = AB.subst(Nat, y => {Nat.is_lt(y, Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}, Nat.add(Nat.add(X, r), j), Nat.add(X, Nat.add(r, j)), ea,
649	    N.lt_le_trans(Nat.add(Nat.add(X, r), j), Nat.add(Nat.add(X, r), m), Nat.mul(4n, Nat.pow(2n, e)), N.lt_add_l(Nat.add(X, r), j, m, hjm), hb))
650	  %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, List.drop(&2, U32, US(ts), Nat.add(X, r)), j), List.get(&2, U32, US(ts), Nat.add(Nat.add(X, r), j)), H.get_drop(US(ts), Nat.add(X, r), j)) :
651	    {_ == Some{W.byte(W.merge(lo, C.WD(ts, p), r), j)} : Maybe<&2, U32>}
652	  %Equal.sym(Nat, Nat.add(Nat.add(X, r), j), Nat.add(X, Nat.add(r, j)), ea) : {List.get(&2, U32, US(ts), _) == Some{W.byte(W.merge(lo, C.WD(ts, p), r), j)} : Maybe<&2, U32>}
653	  gsel(ts, e, si, p, lo, r, j, Nat.is_lt(Nat.add(r, j), 4n), hf, he, hlo, hp, hr, N.lt_le_trans(j, m, 4n, hjm, hm), hbj, {==})
654	
655	# The first m bytes of a merged word are the m src bytes from 4 si + r.
656	law win:
657	  for +ts: P.Tree<U32>
658	  for +e: Nat
659	  for +si: U32
660	  for +p: U32
661	  for +lo: U32
662	  for +r: Nat
663	  for +m: Nat
664	  for +hf: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
665	  for +he: {Nat.is_le(e, 29n) == True{} : Bool}
666	  for +hlo: {lo == C.WD(ts, si) : U32}
667	  for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat}
668	  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
669	  for +hm: {Nat.is_le(m, 4n) == True{} : Bool}
670	  for +hb: {Nat.is_le(Nat.add(Nat.add(Nat.mul(U32.to_nat(si), 4n), r), m), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
671	  {List.take(&2, U32, C.L4(W.merge(lo, C.WD(ts, p), r)), m) == List.take(&2, U32, List.drop(&2, U32, US(ts), Nat.add(Nat.mul(U32.to_nat(si), 4n), r)), m) : List<&2, U32>}
672	
673	def win(ts, e, si, p, lo, r, m, hf, he, hlo, hp, hr, hm, hb):
674	  +mw = W.merge(lo, C.WD(ts, p), r)
675	  +ys = List.drop(&2, U32, US(ts), Nat.add(Nat.mul(U32.to_nat(si), 4n), r))
676	  Equal.sym(List<&2, U32>, List.take(&2, U32, ys, m), List.take(&2, U32, C.L4(mw), m),
677	    tg4(ys, m, W.byte(mw, 0n), W.byte(mw, 1n), W.byte(mw, 2n), W.byte(mw, 3n), hm,
678	      h => gj(ts, e, si, p, lo, r, m, 0n, hf, he, hlo, hp, hr, hm, hb, h),
679	      h => gj(ts, e, si, p, lo, r, m, 1n, hf, he, hlo, hp, hr, hm, hb, h),
680	      h => gj(ts, e, si, p, lo, r, m, 2n, hf, he, hlo, hp, hr, hm, hb, h),
681	      h => gj(ts, e, si, p, lo, r, m, 3n, hf, he, hlo, hp, hr, hm, hb, h)))
682	
683	# Nat facts for the word loop
684	# ===========================
685	
686	law lt_w0:
687	  for +w: Nat
688	  for +pp: Nat
689	  for +h: {Nat.is_lt(Nat.mul(w, 4n), Nat.mul(4n, pp)) == True{} : Bool}
690	  {Nat.is_lt(w, pp) == True{} : Bool}
691	
692	def lt_w0(w, pp, h):
693	  N.lt_mul_cancel(4n, w, pp, AB.subst(Nat, y => {Nat.is_lt(y, Nat.mul(4n, pp)) == True{} : Bool}, Nat.mul(w, 4n), Nat.mul(4n, w), N.mul_comm(w, 4n), h))
694	
695	law le_x4:
696	  for +w: Nat
697	  {Nat.is_le(w, Nat.mul(w, 4n)) == True{} : Bool}
698	
699	def le_x4(w):
700	  AB.subst(Nat, y => {Nat.is_le(w, y) == True{} : Bool}, Nat.mul(4n, w), Nat.mul(w, 4n), N.mul_comm(4n, w), N.le_add_r(w, Nat.mul(3n, w)))
701	
702	law four_alg:
703	  for +a: Nat
704	  for +b: Nat
705	  {Nat.add(4n, Nat.add(a, b)) == Nat.add(a, Nat.add(b, 4n)) : Nat}
706	
707	def four_alg(a, b):
708	  %N.add_comm(4n, b) : {Nat.add(4n, Nat.add(a, b)) == Nat.add(a, _) : Nat}
709	  Equal.sym(Nat, Nat.add(a, Nat.add(4n, b)), Nat.add(4n, Nat.add(a, b)), N.add_left_comm(a, 4n, b))
710	
711	law c4:
712	  for +o: Nat
713	  for +y: Nat
714	  for +np: Nat
715	  for +h: {Nat.is_lt(Nat.add(o, Nat.add(4n, y)), Nat.add(np, 4n)) == True{} : Bool}
716	  {Nat.is_lt(Nat.add(o, y), np) == True{} : Bool}
717	
718	def c4(o, y, np, h):
719	  +h2 = AB.subst(Nat, z => {Nat.is_lt(z, Nat.add(np, 4n)) == True{} : Bool}, Nat.add(o, Nat.add(4n, y)), Nat.add(4n, Nat.add(o, y)), N.add_left_comm(o, 4n, y), h)
720	  AB.subst(Nat, z => {Nat.is_lt(Nat.add(4n, Nat.add(o, y)), z) == True{} : Bool}, Nat.add(np, 4n), Nat.add(4n, np), N.add_comm(np, 4n), h2)
721	
722	law w2_bound:
723	  for +w: Nat
724	  for +pp: Nat
725	  for +hp: {Nat.is_lt(0n, pp) == True{} : Bool}
726	  for +h: {Nat.is_lt(w, pp) == True{} : Bool}
727	  {Nat.is_le(Nat.add(w, 2n), Nat.mul(4n, pp)) == True{} : Bool}
728	
729	def w2_bound(w, pp, hp, h):
730	  +R = Nat.add(pp, Nat.add(pp, Nat.add(pp, 0n)))
731	  +h1 = AB.subst(Nat, y => {Nat.is_le(y, Nat.add(pp, 1n)) == True{} : Bool}, Nat.add(Nat.add(w, 1n), 1n), Nat.add(w, 2n), N.add_assoc(w, 1n, 1n),
732	    N.le_add_mono_r(1n, Nat.add(w, 1n), pp, C.succ_le(w, pp, h)))
733	  N.le_trans(Nat.add(w, 2n), Nat.add(pp, 1n), Nat.mul(4n, pp), h1,
734	    N.le_add_mono_l(pp, 1n, R, Equal.trans(Bool, Nat.is_le(1n, R), Nat.is_lt(0n, R), True{}, N.le_succ_lt(0n, R), N.pos_add_l(pp, Nat.add(pp, Nat.add(pp, 0n)), hp))))
735	
736	law sub_le_of:
737	  for +a: Nat
738	  for +b: Nat
739	  for +c: Nat
740	  for +h: {Nat.is_le(a, Nat.add(b, c)) == True{} : Bool}
741	  {Nat.is_le(Nat.sub(a, b), c) == True{} : Bool}
742	
743	def sub_le_of(a, b, c, h):
744	  match a b:
745	    case 0n _:
746	      N.le_zero_l(c)
747	    case 1n+p 0n:
748	      h
749	    case 1n+p 1n+q:
750	      sub_le_of(p, q, c, h)
751	
752	# One word written
753	# ================
754	
755	law step:
756	  for +ts: P.Tree<U32>
757	  for +e: Nat
758	  for +td: P.Tree<U32>
759	  for +d: Nat
760	  for +p: U32
761	  for +lo: U32
762	  for +si: U32
763	  for +di: U32
764	  for +sh: Nat
765	  for +l1: Nat
766	  for +qn: Nat
767	  for +r: Nat
768	  for +o: Nat
769	  for +np: Nat
770	  for +v1: List<&2, U32>
771	  for +m: Nat
772	  for +hfs: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
773	  for +hes: {Nat.is_le(e, 29n) == True{} : Bool}
774	  for +hfd: {A.full(U32, P.fromT(U32, td), d) == True{} : Bool}
775	  for +hdd: {Nat.is_le(d, 29n) == True{} : Bool}
776	  for +hdi: {Nat.mul(U32.to_nat(di), 4n) == Nat.add(l1, o) : Nat}
777	  for +hsi: {Nat.add(Nat.mul(U32.to_nat(si), 4n), r) == Nat.add(qn, o) : Nat}
778	  for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat}
779	  for +hlo: {lo == C.WD(ts, si) : U32}
780	  for +hsh: {sh == Nat.mul(8n, r) : Nat}
781	  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
782	  for +hq: {Nat.is_le(Nat.add(qn, np), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
783	  for +hl: {Nat.is_le(Nat.add(l1, np), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
784	  for +ho: {Nat.is_lt(o, np) == True{} : Bool}
785	  for +hm: {Nat.is_le(m, 4n) == True{} : Bool}
786	  for +hmv: {Nat.is_le(Nat.add(o, m), np) == True{} : Bool}
787	  for +hinv: {List.take(&2, U32, US(td), Nat.add(l1, o)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), o)) : List<&2, U32>}
788	  {List.take(&2, U32, US(I.set_tree(U32, td, di, U32.or(U32.shrn(lo, sh), U32.shln(C.WD(ts, p), Nat.sub(32n, sh))))), Nat.add(l1, Nat.add(o, m))) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), Nat.add(o, m))) : List<&2, U32>}
789	
790	def step(ts, e, td, d, p, lo, si, di, sh, l1, qn, r, o, np, v1, m, hfs, hes, hfd, hdd, hdi, hsi, hp, hlo, hsh, hr, hq, hl, ho, hm, hmv, hinv):
791	  +hi = C.WD(ts, p)
792	  +mw = U32.or(U32.shrn(lo, sh), U32.shln(hi, Nat.sub(32n, sh)))
793	  +dd = U32.to_nat(di)
794	  +w = U32.to_nat(si)
795	  +ys = List.drop(&2, U32, US(ts), qn)
796	  +RHS = List.append(&2, U32, v1, List.take(&2, U32, ys, Nat.add(o, m)))
797	  +hdl = AB.subst(Nat, y => {Nat.is_lt(y, Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}, Nat.add(l1, o), Nat.mul(dd, 4n), Equal.sym(Nat, Nat.mul(dd, 4n), Nat.add(l1, o), hdi),
798	    N.lt_le_trans(Nat.add(l1, o), Nat.add(l1, np), Nat.mul(4n, Nat.pow(2n, d)), N.lt_add_l(l1, o, np, ho), hl))
799	  +hD = lt_w0(dd, Nat.pow(2n, d), hdl)
800	  +hDl = AB.subst(Nat, y => {Nat.is_lt(dd, y) == True{} : Bool}, Nat.pow(2n, d), List.length(&2, U32, C.WL(td)),
801	    Equal.sym(Nat, List.length(&2, U32, C.WL(td)), Nat.pow(2n, d), P.view_length(U32, d, td, hfd)), hD)
802	  +eidx = Equal.trans(Nat, Nat.add(Nat.mul(dd, 4n), m), Nat.add(Nat.add(l1, o), m), Nat.add(l1, Nat.add(o, m)),
803	    Equal.cong(Nat, Nat, z => Nat.add(z, m), Nat.mul(dd, 4n), Nat.add(l1, o), hdi), N.add_assoc(l1, o, m))
804	  +hb = AB.subst(Nat, y => {Nat.is_le(Nat.add(y, m), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}, Nat.add(qn, o), Nat.add(Nat.mul(w, 4n), r),
805	    Equal.sym(Nat, Nat.add(Nat.mul(w, 4n), r), Nat.add(qn, o), hsi),
806	    AB.subst(Nat, y => {Nat.is_le(y, Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}, Nat.add(qn, Nat.add(o, m)), Nat.add(Nat.add(qn, o), m),
807	      Equal.sym(Nat, Nat.add(Nat.add(qn, o), m), Nat.add(qn, Nat.add(o, m)), N.add_assoc(qn, o, m)),
808	      N.le_trans(Nat.add(qn, Nat.add(o, m)), Nat.add(qn, np), Nat.mul(4n, Nat.pow(2n, e)), N.le_add_mono_l(qn, Nat.add(o, m), np, hmv), hq)))
809	  +ew = Equal.trans(List<&2, U32>, List.take(&2, U32, C.L4(mw), m), List.take(&2, U32, C.L4(W.merge(lo, hi, r)), m), List.take(&2, U32, List.drop(&2, U32, US(ts), Nat.add(qn, o)), m),
810	    Equal.cong(U32, List<&2, U32>, z => List.take(&2, U32, C.L4(z), m), mw, W.merge(lo, hi, r), mrg(lo, hi, sh, r, hsh, hr)),
811	    Equal.trans(List<&2, U32>, List.take(&2, U32, C.L4(W.merge(lo, hi, r)), m), List.take(&2, U32, List.drop(&2, U32, US(ts), Nat.add(Nat.mul(w, 4n), r)), m),
812	      List.take(&2, U32, List.drop(&2, U32, US(ts), Nat.add(qn, o)), m),
813	      win(ts, e, si, p, lo, r, m, hfs, hes, hlo, hp, hr, hm, hb),
814	      Equal.cong(Nat, List<&2, U32>, z => List.take(&2, U32, List.drop(&2, U32, US(ts), z), m), Nat.add(Nat.mul(w, 4n), r), Nat.add(qn, o), hsi)))
815	  +ew2 = AB.subst(List<&2, U32>, z => {List.take(&2, U32, C.L4(mw), m) == List.take(&2, U32, z, m) : List<&2, U32>},
816	    List.drop(&2, U32, US(ts), Nat.add(qn, o)), List.drop(&2, U32, ys, o),
817	    Equal.sym(List<&2, U32>, List.drop(&2, U32, ys, o), List.drop(&2, U32, US(ts), Nat.add(qn, o)), drop_drop(US(ts), qn, o)), ew)
818	  %Equal.sym(List<&2, U32>, C.WL(I.set_tree(U32, td, di, mw)), List.set(&2, U32, C.WL(td), dd, mw), C.wl_set(td, d, di, mw, hfd, hdd, hD)) :
819	    {List.take(&2, U32, D.unpack(_), Nat.add(l1, Nat.add(o, m))) == RHS : List<&2, U32>}
820	  %eidx : {List.take(&2, U32, D.unpack(List.set(&2, U32, C.WL(td), dd, mw)), _) == RHS : List<&2, U32>}
821	  %Equal.sym(List<&2, U32>, List.take(&2, U32, D.unpack(List.set(&2, U32, C.WL(td), dd, mw)), Nat.add(Nat.mul(dd, 4n), m)),
822	    List.append(&2, U32, List.take(&2, U32, D.unpack(C.WL(td)), Nat.mul(dd, 4n)), List.take(&2, U32, C.L4(mw), m)),
823	    us1(C.WL(td), dd, mw, m, hDl, hm)) :
824	    {_ == RHS : List<&2, U32>}
825	  %Equal.sym(Nat, Nat.mul(dd, 4n), Nat.add(l1, o), hdi) :
826	    {List.append(&2, U32, List.take(&2, U32, D.unpack(C.WL(td)), _), List.take(&2, U32, C.L4(mw), m)) == RHS : List<&2, U32>}
827	  %Equal.sym(List<&2, U32>, List.take(&2, U32, US(td), Nat.add(l1, o)), List.append(&2, U32, v1, List.take(&2, U32, ys, o)), hinv) :
828	    {List.append(&2, U32, _, List.take(&2, U32, C.L4(mw), m)) == RHS : List<&2, U32>}
829	  %Equal.sym(List<&2, U32>, List.take(&2, U32, C.L4(mw), m), List.take(&2, U32, List.drop(&2, U32, ys, o), m), ew2) :
830	    {List.append(&2, U32, List.append(&2, U32, v1, List.take(&2, U32, ys, o)), _) == RHS : List<&2, U32>}
831	  Equal.trans(List<&2, U32>, List.append(&2, U32, List.append(&2, U32, v1, List.take(&2, U32, ys, o)), List.take(&2, U32, List.drop(&2, U32, ys, o), m)),
832	    List.append(&2, U32, v1, List.append(&2, U32, List.take(&2, U32, ys, o), List.take(&2, U32, List.drop(&2, U32, ys, o), m))), RHS,
833	    X.append_assoc(v1, List.take(&2, U32, ys, o), List.take(&2, U32, List.drop(&2, U32, ys, o), m)),
834	    Equal.cong(List<&2, U32>, List<&2, U32>, z => List.append(&2, U32, v1, z),
835	      List.append(&2, U32, List.take(&2, U32, ys, o), List.take(&2, U32, List.drop(&2, U32, ys, o), m)), List.take(&2, U32, ys, Nat.add(o, m)), take_split(ys, o, m)))
836	
837	# The last word, when fewer than 4 bytes are left.
838	law avf:
839	  for +k1: Nat
840	  for +ts: P.Tree<U32>
841	  for +e: Nat
842	  for +td: P.Tree<U32>
843	  for +d: Nat
844	  for +p: U32
845	  for +lo: U32
846	  for +si: U32
847	  for +di: U32
848	  for +sh: Nat
849	  for +l1: Nat
850	  for +qn: Nat
851	  for +r: Nat
852	  for +o: Nat
853	  for +np: Nat
854	  for +v1: List<&2, U32>
855	  for +hbq: {Nat.is_le(Nat.add(o, 4n), np) == False{} : Bool}
856	  for +hfs: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
857	  for +hes: {Nat.is_le(e, 29n) == True{} : Bool}
858	  for +hfd: {A.full(U32, P.fromT(U32, td), d) == True{} : Bool}
859	  for +hdd: {Nat.is_le(d, 29n) == True{} : Bool}
860	  for +hdi: {Nat.mul(U32.to_nat(di), 4n) == Nat.add(l1, o) : Nat}
861	  for +hsi: {Nat.add(Nat.mul(U32.to_nat(si), 4n), r) == Nat.add(qn, o) : Nat}
862	  for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat}
863	  for +hlo: {lo == C.WD(ts, si) : U32}
864	  for +hsh: {sh == Nat.mul(8n, r) : Nat}
865	  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
866	  for +hq: {Nat.is_le(Nat.add(qn, np), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
867	  for +hl: {Nat.is_le(Nat.add(l1, np), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
868	  for +hon: {Nat.is_le(o, np) == True{} : Bool}
869	  for +hc1: {Nat.is_le(np, Nat.add(o, Nat.mul(1n+k1, 4n))) == True{} : Bool}
870	  for +hc2: {Nat.is_lt(Nat.add(o, Nat.mul(1n+k1, 4n)), Nat.add(np, 4n)) == True{} : Bool}
871	  for +hinv: {List.take(&2, U32, US(td), Nat.add(l1, o)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), o)) : List<&2, U32>}
872	  {List.take(&2, U32, US(AWT(1n+k1, ts, p, lo, td, si, di, sh)), Nat.add(l1, np)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), np)) : List<&2, U32>}
873	
874	def avf(k1, ts, e, td, d, p, lo, si, di, sh, l1, qn, r, o, np, v1, hbq, hfs, hes, hfd, hdd, hdi, hsi, hp, hlo, hsh, hr, hq, hl, hon, hc1, hc2, hinv):
875	  match k1:
876	    case 0n:
877	      +hi = C.WD(ts, p)
878	      +mw = U32.or(U32.shrn(lo, sh), U32.shln(hi, Nat.sub(32n, sh)))
879	      +ho = N.le_lt_trans(o, Nat.add(o, 0n), np, N.le_add_r(o, 0n), c4(o, 0n, np, hc2))
880	      +eo = N.le_sub_add(o, np, N.lt_to_le(o, np, ho))
881	      +hm = sub_le_of(np, o, 4n, N.lt_to_le(np, Nat.add(o, 4n), N.not_le_lt(Nat.add(o, 4n), np, hbq)))
882	      +hmv = AB.subst(Nat, y => {Nat.is_le(y, np) == True{} : Bool}, np, Nat.add(o, Nat.sub(np, o)), Equal.sym(Nat, Nat.add(o, Nat.sub(np, o)), np, eo), N.le_refl(np))
883	      AB.subst(Nat, y => {List.take(&2, U32, US(I.set_tree(U32, td, di, mw)), Nat.add(l1, y)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), y)) : List<&2, U32>},
884	        Nat.add(o, Nat.sub(np, o)), np, eo,
885	        step(ts, e, td, d, p, lo, si, di, sh, l1, qn, r, o, np, v1, Nat.sub(np, o), hfs, hes, hfd, hdd, hdi, hsi, hp, hlo, hsh, hr, hq, hl, ho, hm, hmv, hinv))
886	    case 1n+k2:
887	      +X2 = Nat.mul(k2, 4n)
888	      +h1 = c4(o, Nat.add(4n, X2), np, hc2)
889	      +h2 = N.le_lt_trans(Nat.add(o, 4n), Nat.add(o, Nat.add(4n, X2)), np, N.le_add_mono_l(o, 4n, Nat.add(4n, X2), N.le_add_r(4n, X2)), h1)
890	      Empty.absurd({List.take(&2, U32, US(AWT(2n+k2, ts, p, lo, td, si, di, sh)), Nat.add(l1, np)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), np)) : List<&2, U32>},
891	        AB.false_ne_true(Equal.trans(Bool, False{}, Nat.is_le(Nat.add(o, 4n), np), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(o, 4n), np), False{}, hbq),
892	          N.lt_to_le(Nat.add(o, 4n), np, h2))))
893	
894	# The word loop
895	# =============
896	
897	# After the words written so far (o bytes, o <= np), the bytes in use agree
898	# with v1 then src from qn; the k words left finish the np bytes.
899	law av:
900	  for +k: Nat
901	  for +b: Bool
902	  for +ts: P.Tree<U32>
903	  for +e: Nat
904	  for +td: P.Tree<U32>
905	  for +d: Nat
906	  for +p: U32
907	  for +lo: U32
908	  for +si: U32
909	  for +di: U32
910	  for +sh: Nat
911	  for +l1: Nat
912	  for +qn: Nat
913	  for +r: Nat
914	  for +o: Nat
915	  for +np: Nat
916	  for +v1: List<&2, U32>
917	  for +hbq: {Nat.is_le(Nat.add(o, 4n), np) == b : Bool}
918	  for +hfs: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
919	  for +hes: {Nat.is_le(e, 29n) == True{} : Bool}
920	  for +hfd: {A.full(U32, P.fromT(U32, td), d) == True{} : Bool}
921	  for +hdd: {Nat.is_le(d, 29n) == True{} : Bool}
922	  for +hdi: {Nat.mul(U32.to_nat(di), 4n) == Nat.add(l1, o) : Nat}
923	  for +hsi: {Nat.add(Nat.mul(U32.to_nat(si), 4n), r) == Nat.add(qn, o) : Nat}
924	  for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat}
925	  for +hlo: {lo == C.WD(ts, si) : U32}
926	  for +hsh: {sh == Nat.mul(8n, r) : Nat}
927	  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
928	  for +hq: {Nat.is_le(Nat.add(qn, np), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
929	  for +hl: {Nat.is_le(Nat.add(l1, np), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
930	  for +hon: {Nat.is_le(o, np) == True{} : Bool}
931	  for +hc1: {Nat.is_le(np, Nat.add(o, Nat.mul(k, 4n))) == True{} : Bool}
932	  for +hc2: {Nat.is_lt(Nat.add(o, Nat.mul(k, 4n)), Nat.add(np, 4n)) == True{} : Bool}
933	  for +hinv: {List.take(&2, U32, US(td), Nat.add(l1, o)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), o)) : List<&2, U32>}
934	  {List.take(&2, U32, US(AWT(k, ts, p, lo, td, si, di, sh)), Nat.add(l1, np)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), np)) : List<&2, U32>}
935	
936	def av(k, b, ts, e, td, d, p, lo, si, di, sh, l1, qn, r, o, np, v1, hbq, hfs, hes, hfd, hdd, hdi, hsi, hp, hlo, hsh, hr, hq, hl, hon, hc1, hc2, hinv):
937	  match k b:
938	    case 0n _:
939	      +eo = le_antisym(o, np, hon, AB.subst(Nat, y => {Nat.is_le(np, y) == True{} : Bool}, Nat.add(o, 0n), o, N.add_zero(o), hc1))
940	      %eo : {List.take(&2, U32, US(td), Nat.add(l1, _)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), _)) : List<&2, U32>}
941	      hinv
942	    case 1n+k1 True{}:
943	      +w = U32.to_nat(si)
944	      +dd = U32.to_nat(di)
945	      +hi = C.WD(ts, p)
946	      +mw = U32.or(U32.shrn(lo, sh), U32.shln(hi, Nat.sub(32n, sh)))
947	      +MD = Nat.mul(4n, Nat.pow(2n, d))
948	      +ME = Nat.mul(4n, Nat.pow(2n, e))
949	      +X = Nat.mul(k1, 4n)
950	      +ho = N.le_lt_trans(o, Nat.add(o, X), np, N.le_add_r(o, X), c4(o, X, np, hc2))
951	      +hinv2 = step(ts, e, td, d, p, lo, si, di, sh, l1, qn, r, o, np, v1, 4n, hfs, hes, hfd, hdd, hdi, hsi, hp, hlo, hsh, hr, hq, hl, ho, {==}, hbq, hinv)
952	      +hdl = AB.subst(Nat, y => {Nat.is_lt(y, MD) == True{} : Bool}, Nat.add(l1, o), Nat.mul(dd, 4n), Equal.sym(Nat, Nat.mul(dd, 4n), Nat.add(l1, o), hdi),
953	        N.lt_le_trans(Nat.add(l1, o), Nat.add(l1, np), MD, N.lt_add_l(l1, o, np, ho), hl))
954	      +e1 = C.inc_fits(di, d, hdd, N.le_lt_trans(dd, Nat.mul(dd, 4n), MD, le_x4(dd), hdl))
955	      +hwl = AB.subst(Nat, y => {Nat.is_lt(y, ME) == True{} : Bool}, Nat.add(qn, o), Nat.add(Nat.mul(w, 4n), r), Equal.sym(Nat, Nat.add(Nat.mul(w, 4n), r), Nat.add(qn, o), hsi),
956	        N.lt_le_trans(Nat.add(qn, o), Nat.add(qn, np), ME, N.lt_add_l(qn, o, np, ho), hq))
957	      +hw4 = N.le_lt_trans(Nat.mul(w, 4n), Nat.add(Nat.mul(w, 4n), r), ME, N.le_add_r(Nat.mul(w, 4n), r), hwl)
958	      +e2 = C.inc_fits(si, e, hes, N.le_lt_trans(w, Nat.mul(w, 4n), ME, le_x4(w), hw4))
959	      +e3 = C.add_fits(si, 2, e, hes, w2_bound(w, Nat.pow(2n, e), AB.pow_pos(e), lt_w0(w, Nat.pow(2n, e), hw4)))
960	      +hdi2 = Equal.trans(Nat, Nat.mul(U32.to_nat((di + 1 : U32)), 4n), Nat.mul(1n+dd, 4n), Nat.add(l1, Nat.add(o, 4n)),
961	        Equal.cong(Nat, Nat, z => Nat.mul(z, 4n), U32.to_nat((di + 1 : U32)), 1n+dd, Equal.trans(Nat, U32.to_nat((di + 1 : U32)), Nat.add(dd, 1n), 1n+dd, e1, N.add_one(dd))),
962	        Equal.trans(Nat, Nat.add(4n, Nat.mul(dd, 4n)), Nat.add(4n, Nat.add(l1, o)), Nat.add(l1, Nat.add(o, 4n)),
963	          Equal.cong(Nat, Nat, z => Nat.add(4n, z), Nat.mul(dd, 4n), Nat.add(l1, o), hdi), four_alg(l1, o)))
964	      +hsi2 = Equal.trans(Nat, Nat.add(Nat.mul(U32.to_nat((si + 1 : U32)), 4n), r), Nat.add(Nat.mul(1n+w, 4n), r), Nat.add(qn, Nat.add(o, 4n)),
965	        Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, 4n), r), U32.to_nat((si + 1 : U32)), 1n+w, Equal.trans(Nat, U32.to_nat((si + 1 : U32)), Nat.add(w, 1n), 1n+w, e2, N.add_one(w))),
966	        Equal.trans(Nat, Nat.add(4n, Nat.add(Nat.mul(w, 4n), r)), Nat.add(4n, Nat.add(qn, o)), Nat.add(qn, Nat.add(o, 4n)),
967	          Equal.cong(Nat, Nat, z => Nat.add(4n, z), Nat.add(Nat.mul(w, 4n), r), Nat.add(qn, o), hsi), four_alg(qn, o)))
968	      +hp2 = Equal.trans(Nat, U32.to_nat((si + 2 : U32)), Nat.add(w, 2n), Nat.add(U32.to_nat((si + 1 : U32)), 1n), e3,
969	        Equal.sym(Nat, Nat.add(U32.to_nat((si + 1 : U32)), 1n), Nat.add(w, 2n),
970	          Equal.trans(Nat, Nat.add(U32.to_nat((si + 1 : U32)), 1n), Nat.add(Nat.add(w, 1n), 1n), Nat.add(w, 2n),
971	            Equal.cong(Nat, Nat, z => Nat.add(z, 1n), U32.to_nat((si + 1 : U32)), Nat.add(w, 1n), e2), N.add_assoc(w, 1n, 1n))))
972	      +hlo2 = Equal.cong(U32, U32, z => C.WD(ts, z), p, (si + 1 : U32),
973	        U.to_nat_inj(p, (si + 1 : U32), Equal.trans(Nat, U32.to_nat(p), Nat.add(w, 1n), U32.to_nat((si + 1 : U32)), hp, Equal.sym(Nat, U32.to_nat((si + 1 : U32)), Nat.add(w, 1n), e2))))
974	      +ea = Equal.sym(Nat, Nat.add(Nat.add(o, 4n), X), Nat.add(o, Nat.add(4n, X)), N.add_assoc(o, 4n, X))
975	      +hc12 = AB.subst(Nat, y => {Nat.is_le(np, y) == True{} : Bool}, Nat.add(o, Nat.add(4n, X)), Nat.add(Nat.add(o, 4n), X), ea, hc1)
976	      +hc22 = AB.subst(Nat, y => {Nat.is_lt(y, Nat.add(np, 4n)) == True{} : Bool}, Nat.add(o, Nat.add(4n, X)), Nat.add(Nat.add(o, 4n), X), ea, hc2)
977	      av(k1, Nat.is_le(Nat.add(Nat.add(o, 4n), 4n), np), ts, e, I.set_tree(U32, td, di, mw), d, (si + 2 : U32), hi, (si + 1 : U32), (di + 1 : U32), sh, l1, qn, r, Nat.add(o, 4n), np, v1,
978	        {==}, hfs, hes, C.full_set(td, d, di, mw, hfd), hdd, hdi2, hsi2, hp2, hlo2, hsh, hr, hq, hl, hbq, hc12, hc22, hinv2)
979	    case 1n+k1 False{}:
980	      avf(k1, ts, e, td, d, p, lo, si, di, sh, l1, qn, r, o, np, v1, hbq, hfs, hes, hfd, hdd, hdi, hsi, hp, hlo, hsh, hr, hq, hl, hon, hc1, hc2, hinv)
981	
982	# Facts for the top level
983	# =======================
984	
985	# The length after the reference append's pushes.
986	law ag_size:
987	  for +n: Nat
988	  for +ld: U32
989	  for +td: P.Tree<U32>
990	  for +ls: U32
991	  for +ts: P.Tree<U32>
992	  for +d: Nat
993	  for +s: U32
994	  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
995	  for +hc: {Nat.is_le(Nat.add(U32.to_nat(ld), n), D.cap(C.BT(ld, td))) == True{} : Bool}
996	  {D.size(Pair.fst(D.Bytes, D.Bytes, B.append.go(n, C.BT(ld, td), B.at(C.BT(ls, ts), s), s))) == Nat.add(U32.to_nat(ld), n) : Nat}
997	
998	def ag_size(n, ld, td, ls, ts, d, s, hd, hc):
999	  match n:
1000	    case 0n:
1001	      %Equal.sym(D.Bytes & U32, B.at(C.BT(ls, ts), s), (C.BT(ls, ts), C.AT(ls, ts, s)), C.at_pair_t(ls, ts, s)) :
1002	        {D.size(Pair.fst(D.Bytes, D.Bytes, B.append.go(0n, C.BT(ld, td), _, s))) == Nat.add(U32.to_nat(ld), 0n) : Nat}
1003	      Equal.sym(Nat, Nat.add(U32.to_nat(ld), 0n), U32.to_nat(ld), N.add_zero(U32.to_nat(ld)))
1004	    case 1n+k:
1005	      +x = C.AT(ls, ts, s)
1006	      %Equal.sym(D.Bytes & U32, B.at(C.BT(ls, ts), s), (C.BT(ls, ts), x), C.at_pair_t(ls, ts, s)) :
1007	        {D.size(Pair.fst(D.Bytes, D.Bytes, B.append.go(1n+k, C.BT(ld, td), _, s))) == Nat.add(U32.to_nat(ld), 1n+k) : Nat}
1008	      %Equal.sym(D.Bytes, B.push(C.BT(ld, td), x), C.BT((ld + 1 : U32), X.PT(ld, td, x)), O.push_eq_t(ld, td, x)) :
1009	        {D.size(Pair.fst(D.Bytes, D.Bytes, B.append.go(k, _, B.at(C.BT(ls, ts), (s + 1 : U32)), (s + 1 : U32)))) == Nat.add(U32.to_nat(ld), 1n+k) : Nat}
1010	      Equal.trans(Nat, D.size(Pair.fst(D.Bytes, D.Bytes, B.append.go(k, C.BT((ld + 1 : U32), X.PT(ld, td, x)), B.at(C.BT(ls, ts), (s + 1 : U32)), (s + 1 : U32)))),
1011	        Nat.add(U32.to_nat((ld + 1 : U32)), k), Nat.add(U32.to_nat(ld), 1n+k),
1012	        ag_size(k, (ld + 1 : U32), X.PT(ld, td, x), ls, ts, d, (s + 1 : U32), X.step_ok(ld, td, d, x, k, hd, hc), X.step_cap(ld, td, d, x, k, hd, hc)),
1013	        Equal.trans(Nat, Nat.add(U32.to_nat((ld + 1 : U32)), k), Nat.add(Nat.add(U32.to_nat(ld), 1n), k), Nat.add(U32.to_nat(ld), 1n+k),
1014	          Equal.cong(Nat, Nat, z => Nat.add(z, k), U32.to_nat((ld + 1 : U32)), Nat.add(U32.to_nat(ld), 1n),
1015	            C.inc_fits(ld, d, C.ok_d(ld, td, d, hd), X.step_room(ld, td, d, k, hd, hc))),
1016	          N.add_assoc(U32.to_nat(ld), 1n, k)))
1017	
1018	law aw_full:
1019	  for +n: Nat
1020	  for +ts: P.Tree<U32>
1021	  for +p: U32
1022	  for +lo: U32
1023	  for +td: P.Tree<U32>
1024	  for +si: U32
1025	  for +di: U32
1026	  for +sh: Nat
1027	  for +d: Nat
1028	  for +hfd: {A.full(U32, P.fromT(U32, td), d) == True{} : Bool}
1029	  {A.full(U32, P.fromT(U32, AWT(n, ts, p, lo, td, si, di, sh)), d) == True{} : Bool}
1030	
1031	def aw_full(n, ts, p, lo, td, si, di, sh, d, hfd):
1032	  match n:
1033	    case 0n:
1034	      hfd
1035	    case 1n+k:
1036	      +mw = U32.or(U32.shrn(lo, sh), U32.shln(C.WD(ts, p), Nat.sub(32n, sh)))
1037	      aw_full(k, ts, (si + 2 : U32), C.WD(ts, p), I.set_tree(U32, td, di, mw), (si + 1 : U32), (di + 1 : U32), sh, d, C.full_set(td, d, di, mw, hfd))
1038	
1039	law mul4div:
1040	  for +z: Nat
1041	  for +y: Nat
1042	  for +e: {z == Nat.mul(y, 4n) : Nat}
1043	  {Nat.mul(Nat.div(z, 4n), 4n) == z : Nat}
1044	
1045	def mul4div(z, y, e):
1046	  %Equal.sym(Nat, z, Nat.mul(y, 4n), e) : {Nat.mul(Nat.div(_, 4n), 4n) == _ : Nat}
1047	  Equal.cong(Nat, Nat, w => Nat.mul(w, 4n), Nat.div(Nat.mul(y, 4n), 4n), y,
1048	    AB.subst(Nat, w => {Nat.div(w, 4n) == y : Nat}, Nat.add(Nat.mul(y, 4n), 0n), Nat.mul(y, 4n), N.add_zero(Nat.mul(y, 4n)), N.div_mul_add(y, 4n, 0n, {==})))
1049	
1050	# x = 4a + k with k + h = 4 gives x + h = 4(a + 1).
1051	law al_k:
1052	  for +x: Nat
1053	  for +a: Nat
1054	  for +k: Nat
1055	  for +h: Nat
1056	  for +ex: {x == Nat.add(Nat.mul(a, 4n), k) : Nat}
1057	  for +ek: {Nat.add(k, h) == 4n : Nat}
1058	  {Nat.add(x, h) == Nat.mul(1n+a, 4n) : Nat}
1059	
1060	def al_k(x, a, k, h, ex, ek):
1061	  %Equal.sym(Nat, x, Nat.add(Nat.mul(a, 4n), k), ex) : {Nat.add(_, h) == Nat.mul(1n+a, 4n) : Nat}
1062	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(a, 4n), k), h), Nat.add(Nat.mul(a, 4n), Nat.add(k, h)), N.add_assoc(Nat.mul(a, 4n), k, h)) : {_ == Nat.mul(1n+a, 4n) : Nat}
1063	  %Equal.sym(Nat, Nat.add(k, h), 4n, ek) : {Nat.add(Nat.mul(a, 4n), _) == Nat.mul(1n+a, 4n) : Nat}
1064	  N.add_comm(Nat.mul(a, 4n), 4n)
1065	
1066	def H0(+ld: U32) -> U32:
1067	  U32.and(U32.sub(4, U32.and(ld, 3)), 3)
1068	
1069	law exk:
1070	  for +ld: U32
1071	  for +k: Nat
1072	  for +ek: {U32.to_nat((ld .&. 3 : U32)) == k : Nat}
1073	  {U32.to_nat(ld) == Nat.add(Nat.mul(Nat.div(U32.to_nat(ld), 4n), 4n), k) : Nat}
1074	
1075	def exk(ld, k, ek):
1076	  +x = U32.to_nat(ld)
1077	  +a = Nat.div(x, 4n)
1078	  +ex0 = Equal.sym(Nat, Nat.add(Nat.mul(a, 4n), U32.to_nat((ld .&. 3 : U32))), x,
1079	    AB.subst(Nat, z => {Nat.add(Nat.mul(a, 4n), z) == x : Nat}, Nat.mod(x, 4n), U32.to_nat((ld .&. 3 : U32)),
1080	      Equal.sym(Nat, U32.to_nat((ld .&. 3 : U32)), Nat.mod(x, 4n), U.to_nat_and_mask(ld, 3, 2n, {==})), N.div_mod(x, 4n)))
1081	  AB.subst(Nat, z => {x == Nat.add(Nat.mul(a, 4n), z) : Nat}, U32.to_nat((ld .&. 3 : U32)), k, ek, ex0)
1082	
1083	law align2:
1084	  for +ld: U32
1085	  for +k: Nat
1086	  for +ek: {U32.to_nat((ld .&. 3 : U32)) == k : Nat}
1087	  for +hk: {Nat.is_lt(k, 4n) == True{} : Bool}
1088	  {Nat.mul(Nat.div(Nat.add(U32.to_nat(ld), U32.to_nat(H0(ld))), 4n), 4n) == Nat.add(U32.to_nat(ld), U32.to_nat(H0(ld))) : Nat}
1089	
1090	def align2(ld, k, ek, hk):
1091	  match k:
1092	    case 0n:
1093	      +x = U32.to_nat(ld)
1094	      +a = Nat.div(x, 4n)
1095	      +ex = exk(ld, 0n, ek)
1096	      +eh = Equal.cong(U32, Nat, z => U32.to_nat(U32.and(U32.sub(4, z), 3)), (ld .&. 3 : U32), 0, U.to_nat_inj((ld .&. 3 : U32), 0, ek))
1097	      mul4div(Nat.add(x, U32.to_nat(H0(ld))), a,
1098	        Equal.trans(Nat, Nat.add(x, U32.to_nat(H0(ld))), Nat.add(x, 0n), Nat.mul(a, 4n), Equal.cong(Nat, Nat, z => Nat.add(x, z), U32.to_nat(H0(ld)), 0n, eh),
1099	          Equal.trans(Nat, Nat.add(x, 0n), x, Nat.mul(a, 4n), N.add_zero(x),
1100	            Equal.trans(Nat, x, Nat.add(Nat.mul(a, 4n), 0n), Nat.mul(a, 4n), ex, N.add_zero(Nat.mul(a, 4n))))))
1101	    case 1n+k1:
1102	      match k1:
1103	        case 0n:
1104	          +x = U32.to_nat(ld)
1105	          +a = Nat.div(x, 4n)
1106	          +ex = exk(ld, 1n, ek)
1107	          +eh = Equal.cong(U32, Nat, z => U32.to_nat(U32.and(U32.sub(4, z), 3)), (ld .&. 3 : U32), 1, U.to_nat_inj((ld .&. 3 : U32), 1, ek))
1108	          mul4div(Nat.add(x, U32.to_nat(H0(ld))), 1n+a,
1109	            Equal.trans(Nat, Nat.add(x, U32.to_nat(H0(ld))), Nat.add(x, 3n), Nat.mul(1n+a, 4n), Equal.cong(Nat, Nat, z => Nat.add(x, z), U32.to_nat(H0(ld)), 3n, eh),
1110	              al_k(x, a, 1n, 3n, ex, {==})))
1111	        case 1n+k2:
1112	          match k2:
1113	            case 0n:
1114	              +x = U32.to_nat(ld)
1115	              +a = Nat.div(x, 4n)
1116	              +ex = exk(ld, 2n, ek)
1117	              +eh = Equal.cong(U32, Nat, z => U32.to_nat(U32.and(U32.sub(4, z), 3)), (ld .&. 3 : U32), 2, U.to_nat_inj((ld .&. 3 : U32), 2, ek))
1118	              mul4div(Nat.add(x, U32.to_nat(H0(ld))), 1n+a,
1119	                Equal.trans(Nat, Nat.add(x, U32.to_nat(H0(ld))), Nat.add(x, 2n), Nat.mul(1n+a, 4n), Equal.cong(Nat, Nat, z => Nat.add(x, z), U32.to_nat(H0(ld)), 2n, eh),
1120	                  al_k(x, a, 2n, 2n, ex, {==})))
1121	            case 1n+k3:
1122	              match k3:
1123	                case 0n:
1124	                  +x = U32.to_nat(ld)
1125	                  +a = Nat.div(x, 4n)
1126	                  +ex = exk(ld, 3n, ek)
1127	                  +eh = Equal.cong(U32, Nat, z => U32.to_nat(U32.and(U32.sub(4, z), 3)), (ld .&. 3 : U32), 3, U.to_nat_inj((ld .&. 3 : U32), 3, ek))
1128	                  mul4div(Nat.add(x, U32.to_nat(H0(ld))), 1n+a,
1129	                    Equal.trans(Nat, Nat.add(x, U32.to_nat(H0(ld))), Nat.add(x, 1n), Nat.mul(1n+a, 4n), Equal.cong(Nat, Nat, z => Nat.add(x, z), U32.to_nat(H0(ld)), 1n, eh),
1130	                      al_k(x, a, 3n, 1n, ex, {==})))
1131	                case 1n+k4:
1132	                  Empty.absurd({Nat.mul(Nat.div(Nat.add(U32.to_nat(ld), U32.to_nat(H0(ld))), 4n), 4n) == Nat.add(U32.to_nat(ld), U32.to_nat(H0(ld))) : Nat}, AB.lt_zero_absurd(k4, hk))
1133	
1134	# dst's length after the first h0 bytes is a multiple of 4.
1135	law align:
1136	  for +ld: U32
1137	  {Nat.mul(Nat.div(Nat.add(U32.to_nat(ld), U32.to_nat(H0(ld))), 4n), 4n) == Nat.add(U32.to_nat(ld), U32.to_nat(H0(ld))) : Nat}
1138	
1139	def align(ld):
1140	  align2(ld, U32.to_nat((ld .&. 3 : U32)), {==}, and3_lt(ld))
1141	
1142	# x + y < 2^e for x <= 4 * 2^d and y <= 3, when d + 2 < e (e a variable:
1143	# the callers put 32n only in the final type).
1144	law x3_lt_e:
1145	  for +x: Nat
1146	  for +y: Nat
1147	  for +d: Nat
1148	  for +e: Nat
1149	  for +hy: {Nat.is_le(y, 3n) == True{} : Bool}
1150	  for +hx: {Nat.is_le(x, Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
1151	  for +he: {Nat.is_lt(Nat.add(2n, d), e) == True{} : Bool}
1152	  {Nat.is_lt(Nat.add(x, y), Nat.pow(2n, e)) == True{} : Bool}
1153	
1154	def x3_lt_e(x, y, d, e, hy, hx, he):
1155	  +pp = Nat.pow(2n, d)
1156	  +q = Nat.pow(2n, Nat.add(2n, d))
1157	  +eq = N.mul_assoc(2n, 2n, pp)
1158	  +hxq = AB.subst(Nat, z => {Nat.is_le(x, z) == True{} : Bool}, Nat.mul(Nat.mul(2n, 2n), pp), Nat.mul(2n, Nat.mul(2n, pp)), eq, hx)
1159	  +h1 = N.le_trans(Nat.add(x, y), Nat.add(q, y), Nat.add(q, 3n), N.le_add_mono_r(y, x, q, hxq), N.le_add_mono_l(q, y, 3n, hy))
1160	  +h41 = N.le_mul_l(4n, 1n, pp, Equal.trans(Bool, Nat.is_le(1n, pp), Nat.is_lt(0n, pp), True{}, N.le_succ_lt(0n, pp), AB.pow_pos(d)))
1161	  +h4q = AB.subst(Nat, z => {Nat.is_le(4n, z) == True{} : Bool}, Nat.mul(Nat.mul(2n, 2n), pp), Nat.mul(2n, Nat.mul(2n, pp)), eq, h41)
1162	  +h4 = Equal.trans(Bool, Nat.is_lt(3n, q), Nat.is_le(4n, q), True{}, Equal.sym(Bool, Nat.is_le(4n, q), Nat.is_lt(3n, q), N.le_succ_lt(3n, q)), h4q)
1163	  +h2 = AB.subst(Nat, z => {Nat.is_lt(Nat.add(q, 3n), z) == True{} : Bool}, Nat.add(q, q), Nat.add(q, Nat.add(q, 0n)),
1164	    Equal.cong(Nat, Nat, z => Nat.add(q, z), q, Nat.add(q, 0n), Equal.sym(Nat, Nat.add(q, 0n), q, N.add_zero(q))), N.lt_add_l(q, 3n, q, h4))
1165	  +h3 = N.pow_le(Nat.add(3n, d), e, Equal.trans(Bool, Nat.is_le(Nat.add(3n, d), e), Nat.is_lt(Nat.add(2n, d), e), True{}, N.le_succ_lt(Nat.add(2n, d), e), he))
1166	  N.le_lt_trans(Nat.add(x, y), Nat.add(q, 3n), Nat.pow(2n, e), h1, N.lt_le_trans(Nat.add(q, 3n), Nat.pow(2n, Nat.add(3n, d)), Nat.pow(2n, e), h2, h3))
1167	
1168	# The word count (np + 3) >> 2 covers np bytes with less than one word left.
1169	law cnt1:
1170	  for +np: Nat
1171	  {Nat.is_le(np, Nat.mul(Nat.div(Nat.add(np, 3n), 4n), 4n)) == True{} : Bool}
1172	
1173	def cnt1(np):
1174	  +xx = Nat.add(np, 3n)
1175	  +q = Nat.div(xx, 4n)
1176	  +rm = Nat.mod(xx, 4n)
1177	  +h1 = AB.subst(Nat, z => {Nat.is_le(z, Nat.add(Nat.mul(q, 4n), 3n)) == True{} : Bool}, Nat.add(Nat.mul(q, 4n), rm), xx, N.div_mod(xx, 4n),
1178	    N.le_add_mono_l(Nat.mul(q, 4n), rm, 3n, Equal.trans(Bool, Nat.is_le(rm, 3n), Nat.is_lt(rm, 4n), True{}, Equal.sym(Bool, Nat.is_lt(rm, 4n), Nat.is_le(rm, 3n), N.lt_succ_iff(rm, 3n)), N.mod_lt(xx, 4n, {==}))))
1179	  +h2 = AB.subst(Nat, z => {Nat.is_le(z, Nat.add(Nat.mul(q, 4n), 3n)) == True{} : Bool}, xx, Nat.add(3n, np), N.add_comm(np, 3n), h1)
1180	  AB.subst(Nat, z => {Nat.is_le(Nat.add(3n, np), z) == True{} : Bool}, Nat.add(Nat.mul(q, 4n), 3n), Nat.add(3n, Nat.mul(q, 4n)), N.add_comm(Nat.mul(q, 4n), 3n), h2)
1181	
1182	law cnt2:
1183	  for +np: Nat
1184	  {Nat.is_lt(Nat.mul(Nat.div(Nat.add(np, 3n), 4n), 4n), Nat.add(np, 4n)) == True{} : Bool}
1185	
1186	def cnt2(np):
1187	  +xx = Nat.add(np, 3n)
1188	  +q = Nat.div(xx, 4n)
1189	  +rm = Nat.mod(xx, 4n)
1190	  N.le_lt_trans(Nat.mul(q, 4n), xx, Nat.add(np, 4n),
1191	    AB.subst(Nat, z => {Nat.is_le(Nat.mul(q, 4n), z) == True{} : Bool}, Nat.add(Nat.mul(q, 4n), rm), xx, N.div_mod(xx, 4n), N.le_add_r(Nat.mul(q, 4n), rm)),
1192	    N.lt_add_l(np, 3n, 4n, {==}))
1193	
1194	# The fast append on mirrors
1195	# ==========================
1196	
1197	# The bytes done one at a time, the bytes left, and where they start.
1198	def HH(+ld: U32, +n: U32) -> U32:
1199	  U32.min(H0(ld), n)
1200	
1201	def NPw(+ld: U32, +n: U32) -> U32:
1202	  U32.sub(n, HH(ld, n))
1203	
1204	def QQ(+ld: U32, +s: U32, +n: U32) -> U32:
1205	  U32.add(s, HH(ld, n))
1206	
1207	def NW(+ld: U32, +n: U32) -> Nat:
1208	  U32.to_nat(U32.shrn(U32.add(NPw(ld, n), 3), 2n))
1209	
1210	def SH(+q: U32) -> Nat:
1211	  U32.to_nat(U32.shln(U32.and(q, 3), 3n))
1212	
1213	def TF(+ld: U32, +ts: P.Tree<U32>, +s: U32, +n: U32, +l1: U32, +t1: P.Tree<U32>) -> P.Tree<U32>:
1214	  AWT(NW(ld, n), ts, U32.add(U32.shrn(QQ(ld, s, n), 2n), 1), C.WD(ts, U32.shrn(QQ(ld, s, n), 2n)), t1, U32.shrn(QQ(ld, s, n), 2n), U32.shrn(l1, 2n), SH(QQ(ld, s, n)))
1215	
1216	# With BT(l1, t1) the result of the first bytes, fast append is these mirrors.
1217	law fa_eq:
1218	  for +ld: U32
1219	  for +td: P.Tree<U32>
1220	  for +ls: U32
1221	  for +ts: P.Tree<U32>
1222	  for +s: U32
1223	  for +n: U32
1224	  for +l1: U32
1225	  for +t1: P.Tree<U32>
1226	  for +e1: {C.BT(l1, t1) == Pair.fst(D.Bytes, D.Bytes, B.append(C.BT(ld, td), C.BT(ls, ts), s, HH(ld, n))) : D.Bytes}
1227	  {FA.append(C.BT(ld, td), C.BT(ls, ts), s, n) == (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
1228	
1229	def fa_eq(ld, td, ls, ts, s, n, l1, t1, e1):
1230	  +h = HH(ld, n)
1231	  +q = QQ(ld, s, n)
1232	  +qw = U32.shrn(q, 2n)
1233	  %Equal.sym(D.Bytes & D.Bytes, B.append(C.BT(ld, td), C.BT(ls, ts), s, h), (Pair.fst(D.Bytes, D.Bytes, B.append(C.BT(ld, td), C.BT(ls, ts), s, h)), C.BT(ls, ts)),
1234	    X.append_pair_t(ld, td, ls, ts, s, h)) :
1235	    {FA.append.k(NPw(ld, n), q, _) == (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
1236	  %e1 : {FA.append.k(NPw(ld, n), q, (_, C.BT(ls, ts))) == (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
1237	  %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, ts), qw), (P.fromT(U32, ts), C.WD(ts, qw)), P.get_pair_t(U32, ts, qw)) :
1238	    {FA.append.w(l1, NPw(ld, n), q, P.fromT(U32, t1), ls, _) == (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
1239	  %Equal.sym(Array<U32> & Array<U32>,
1240	    FA.append.words(NW(ld, n), Array.get(U32, P.fromT(U32, ts), U32.add(qw, 1)), C.WD(ts, qw), P.fromT(U32, t1), qw, U32.shrn(l1, 2n), SH(q)),
1241	    (P.fromT(U32, TF(ld, ts, s, n, l1, t1)), P.fromT(U32, ts)),
1242	    aw_eq(NW(ld, n), ts, U32.add(qw, 1), C.WD(ts, qw), t1, qw, U32.shrn(l1, 2n), SH(q))) :
1243	    {FA.append.fin(U32.add(l1, NPw(ld, n)), ls, _) == (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
1244	  {==}
1245	
1246	# The last list step: the bytes of the prefix and of the words make the slice.
1247	law fin_eq:
1248	  for +v1: List<&2, U32>
1249	  for +vd: List<&2, U32>
1250	  for +us: List<&2, U32>
1251	  for +ls: Nat
1252	  for +s: Nat
1253	  for +hh: Nat
1254	  for +qn: Nat
1255	  for +np: Nat
1256	  for +nn: Nat
1257	  for +hv: {v1 == List.append(&2, U32, vd, D.slice(List.take(&2, U32, us, ls), s, hh)) : List<&2, U32>}
1258	  for +hq: {qn == Nat.add(s, hh) : Nat}
1259	  for +hnp: {np == Nat.sub(nn, hh) : Nat}
1260	  for +hhn: {Nat.is_le(hh, nn) == True{} : Bool}
1261	  for +hb: {Nat.is_le(Nat.add(s, nn), ls) == True{} : Bool}
1262	  {List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, us, qn), np)) == List.append(&2, U32, vd, D.slice(List.take(&2, U32, us, ls), s, nn)) : List<&2, U32>}
1263	
1264	def fin_eq(v1, vd, us, ls, s, hh, qn, np, nn, hv, hq, hnp, hhn, hb):
1265	  +xs = List.take(&2, U32, us, ls)
1266	  +rest = Nat.sub(nn, hh)
1267	  +RHS = List.append(&2, U32, vd, D.slice(xs, s, nn))
1268	  +esum = Equal.trans(Nat, Nat.add(Nat.add(s, hh), rest), Nat.add(s, Nat.add(hh, rest)), Nat.add(s, nn), N.add_assoc(s, hh, rest),
1269	    Equal.cong(Nat, Nat, z => Nat.add(s, z), Nat.add(hh, rest), nn, N.le_sub_add(hh, nn, hhn)))
1270	  %Equal.sym(Nat, np, rest, hnp) : {List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, us, qn), _)) == RHS : List<&2, U32>}
1271	  %Equal.sym(Nat, qn, Nat.add(s, hh), hq) : {List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, us, _), rest)) == RHS : List<&2, U32>}
1272	  %Equal.sym(List<&2, U32>, v1, List.append(&2, U32, vd, D.slice(xs, s, hh)), hv) :
1273	    {List.append(&2, U32, _, List.take(&2, U32, List.drop(&2, U32, us, Nat.add(s, hh)), rest)) == RHS : List<&2, U32>}
1274	  %slice_take(us, ls, Nat.add(s, hh), rest,
1275	    AB.subst(Nat, z => {Nat.is_le(z, ls) == True{} : Bool}, Nat.add(s, nn), Nat.add(Nat.add(s, hh), rest), Equal.sym(Nat, Nat.add(Nat.add(s, hh), rest), Nat.add(s, nn), esum), hb)) :
1276	    {List.append(&2, U32, List.append(&2, U32, vd, D.slice(xs, s, hh)), _) == RHS : List<&2, U32>}
1277	  Equal.trans(List<&2, U32>, List.append(&2, U32, List.append(&2, U32, vd, D.slice(xs, s, hh)), D.slice(xs, Nat.add(s, hh), rest)),
1278	    List.append(&2, U32, vd, List.append(&2, U32, D.slice(xs, s, hh), D.slice(xs, Nat.add(s, hh), rest))), RHS,
1279	    X.append_assoc(vd, D.slice(xs, s, hh), D.slice(xs, Nat.add(s, hh), rest)),
1280	    Equal.cong(List<&2, U32>, List<&2, U32>, z => List.append(&2, U32, vd, z),
1281	      List.append(&2, U32, D.slice(xs, s, hh), D.slice(xs, Nat.add(s, hh), rest)), D.slice(xs, s, nn),
1282	      Equal.trans(List<&2, U32>, List.append(&2, U32, D.slice(xs, s, hh), D.slice(xs, Nat.add(s, hh), rest)), D.slice(xs, s, Nat.add(hh, rest)), D.slice(xs, s, nn),
1283	        slice_split(xs, s, hh, rest), Equal.cong(Nat, List<&2, U32>, z => D.slice(xs, s, z), Nat.add(hh, rest), nn, N.le_sub_add(hh, nn, hhn)))))
1284	
1285	# Facts shared by the three laws
1286	# ==============================
1287	
1288	def D1(+ld: U32, +td: P.Tree<U32>, +ls: U32, +ts: P.Tree<U32>, +s: U32, +n: U32) -> D.Bytes:
1289	  Pair.fst(D.Bytes, D.Bytes, B.append(C.BT(ld, td), C.BT(ls, ts), s, HH(ld, n)))
1290	
1291	law hh_le:
1292	  for +ld: U32
1293	  for +n: U32
1294	  {Nat.is_le(U32.to_nat(HH(ld, n)), U32.to_nat(n)) == True{} : Bool}
1295	
1296	def hh_le(ld, n):
1297	  AB.subst(Nat, y => {Nat.is_le(y, U32.to_nat(n)) == True{} : Bool}, Nat.min(U32.to_nat(H0(ld)), U32.to_nat(n)), U32.to_nat(HH(ld, n)),
1298	    Equal.sym(Nat, U32.to_nat(HH(ld, n)), Nat.min(U32.to_nat(H0(ld)), U32.to_nat(n)), U.to_nat_min(H0(ld), n)),
1299	    min_le(U32.to_nat(H0(ld)), U32.to_nat(n)))
1300	
1301	law hc_h:
1302	  for +ld: U32
1303	  for +td: P.Tree<U32>
1304	  for +n: U32
1305	  for +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool}
1306	  {Nat.is_le(Nat.add(U32.to_nat(ld), U32.to_nat(HH(ld, n))), D.cap(C.BT(ld, td))) == True{} : Bool}
1307	
1308	def hc_h(ld, td, n, hc):
1309	  N.le_trans(Nat.add(U32.to_nat(ld), U32.to_nat(HH(ld, n))), Nat.add(U32.to_nat(ld), U32.to_nat(n)), D.cap(C.BT(ld, td)),
1310	    N.le_add_mono_l(U32.to_nat(ld), U32.to_nat(HH(ld, n)), U32.to_nat(n), hh_le(ld, n)), hc)
1311	
1312	law ok1:
1313	  for +ld: U32
1314	  for +td: P.Tree<U32>
1315	  for +ls: U32
1316	  for +ts: P.Tree<U32>
1317	  for +d: Nat
1318	  for +s: U32
1319	  for +n: U32
1320	  for +l1: U32
1321	  for +t1: P.Tree<U32>
1322	  for +e1: {C.BT(l1, t1) == D1(ld, td, ls, ts, s, n) : D.Bytes}
1323	  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
1324	  for +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool}
1325	  {D.ok(C.BT(l1, t1), d) == True{} : Bool}
1326	
1327	def ok1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc):
1328	  AB.subst(D.Bytes, y => {D.ok(y, d) == True{} : Bool}, D1(ld, td, ls, ts, s, n), C.BT(l1, t1), Equal.sym(D.Bytes, C.BT(l1, t1), D1(ld, td, ls, ts, s, n), e1),
1329	    X.append_ok_t(ld, td, ls, ts, d, s, HH(ld, n), hd, hc_h(ld, td, n, hc)))
1330	
1331	law el1:
1332	  for +ld: U32
1333	  for +td: P.Tree<U32>
1334	  for +ls: U32
1335	  for +ts: P.Tree<U32>
1336	  for +d: Nat
1337	  for +s: U32
1338	  for +n: U32
1339	  for +l1: U32
1340	  for +t1: P.Tree<U32>
1341	  for +e1: {C.BT(l1, t1) == D1(ld, td, ls, ts, s, n) : D.Bytes}
1342	  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
1343	  for +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool}
1344	  {U32.to_nat(l1) == Nat.add(U32.to_nat(ld), U32.to_nat(HH(ld, n))) : Nat}
1345	
1346	def el1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc):
1347	  Equal.trans(Nat, U32.to_nat(l1), D.size(D1(ld, td, ls, ts, s, n)), Nat.add(U32.to_nat(ld), U32.to_nat(HH(ld, n))),
1348	    Equal.cong(D.Bytes, Nat, b => D.size(b), C.BT(l1, t1), D1(ld, td, ls, ts, s, n), e1),
1349	    ag_size(U32.to_nat(HH(ld, n)), ld, td, ls, ts, d, s, hd, hc_h(ld, td, n, hc)))
1350	
1351	law enp:
1352	  for +ld: U32
1353	  for +n: U32
1354	  {U32.to_nat(NPw(ld, n)) == Nat.sub(U32.to_nat(n), U32.to_nat(HH(ld, n))) : Nat}
1355	
1356	def enp(ld, n):
1357	  U.to_nat_sub_le(n, HH(ld, n), Equal.trans(Bool, U32.is_le(HH(ld, n), n), Nat.is_le(U32.to_nat(HH(ld, n)), U32.to_nat(n)), True{}, U.is_le_to_nat(HH(ld, n), n), hh_le(ld, n)))
1358	
1359	# l1 + (n - h) = ld + n.
1360	law esum:
1361	  for +ld: U32
1362	  for +l1: U32
1363	  for +n: U32
1364	  for +el: {U32.to_nat(l1) == Nat.add(U32.to_nat(ld), U32.to_nat(HH(ld, n))) : Nat}
1365	  {Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))) == Nat.add(U32.to_nat(ld), U32.to_nat(n)) : Nat}
1366	
1367	def esum(ld, l1, n, el):
1368	  +a = U32.to_nat(ld)
1369	  +h = U32.to_nat(HH(ld, n))
1370	  +nn = U32.to_nat(n)
1371	  %Equal.sym(Nat, U32.to_nat(l1), Nat.add(a, h), el) : {Nat.add(_, U32.to_nat(NPw(ld, n))) == Nat.add(a, nn) : Nat}
1372	  %Equal.sym(Nat, U32.to_nat(NPw(ld, n)), Nat.sub(nn, h), enp(ld, n)) : {Nat.add(Nat.add(a, h), _) == Nat.add(a, nn) : Nat}
1373	  Equal.trans(Nat, Nat.add(Nat.add(a, h), Nat.sub(nn, h)), Nat.add(a, Nat.add(h, Nat.sub(nn, h))), Nat.add(a, nn), N.add_assoc(a, h, Nat.sub(nn, h)),
1374	    Equal.cong(Nat, Nat, z => Nat.add(a, z), Nat.add(h, Nat.sub(nn, h)), nn, N.le_sub_add(h, nn, hh_le(ld, n))))
1375	
1376	law hlen0:
1377	  for +ld: U32
1378	  for +td: P.Tree<U32>
1379	  for +l1: U32
1380	  for +d: Nat
1381	  for +n: U32
1382	  for +el: {U32.to_nat(l1) == Nat.add(U32.to_nat(ld), U32.to_nat(HH(ld, n))) : Nat}
1383	  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
1384	  for +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool}
1385	  {Nat.is_le(Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
1386	
1387	def hlen0(ld, td, l1, d, n, el, hd, hc):
1388	  AB.subst(Nat, y => {Nat.is_le(y, Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}, Nat.add(U32.to_nat(ld), U32.to_nat(n)), Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))),
1389	    Equal.sym(Nat, Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))), Nat.add(U32.to_nat(ld), U32.to_nat(n)), esum(ld, l1, n, el)),
1390	    AB.subst(Nat, y => {Nat.is_le(Nat.add(U32.to_nat(ld), U32.to_nat(n)), y) == True{} : Bool}, D.cap(C.BT(ld, td)), Nat.mul(4n, Nat.pow(2n, d)), O.cap_ok_t(ld, td, d, hd), hc))
1391	
1392	# The pair law
1393	# ============
1394	
1395	def fap.go(+ld: U32, +td: P.Tree<U32>, +ls: U32, +ts: P.Tree<U32>, +s: U32, +n: U32, m: C.BMirror(D1(ld, td, ls, ts, s, n))) ->
1396	  {FA.append(C.BT(ld, td), C.BT(ls, ts), s, n) == (Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n)), C.BT(ls, ts)) : D.Bytes & D.Bytes}:
1397	  (+l1, m2) = m
1398	  (+t1, +e1) = m2
1399	  %Equal.sym(D.Bytes & D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n), (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)),
1400	    fa_eq(ld, td, ls, ts, s, n, l1, t1, e1)) :
1401	    {_ == (Pair.fst(D.Bytes, D.Bytes, _), C.BT(ls, ts)) : D.Bytes & D.Bytes}
1402	  {==}
1403	
1404	law fast_append_pair_t:
1405	  for +ld: U32
1406	  for +td: P.Tree<U32>
1407	  for +ls: U32
1408	  for +ts: P.Tree<U32>
1409	  for +s: U32
1410	  for +n: U32
1411	  {FA.append(C.BT(ld, td), C.BT(ls, ts), s, n) == (Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
1412	
1413	def fast_append_pair_t(ld, td, ls, ts, s, n):
1414	  fap.go(ld, td, ls, ts, s, n, C.bmirror(D1(ld, td, ls, ts, s, n)))
1415	
1416	# The ok law
1417	# ==========
1418	
1419	def fao.go(+ld: U32, +td: P.Tree<U32>, +ls: U32, +ts: P.Tree<U32>, +d: Nat, +s: U32, +n: U32,
1420	  +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool},
1421	  +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool},
1422	  m: C.BMirror(D1(ld, td, ls, ts, s, n))) ->
1423	  {D.ok(Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n)), d) == True{} : Bool}:
1424	  (+l1, m2) = m
1425	  (+t1, +e1) = m2
1426	  +q = QQ(ld, s, n)
1427	  +hk1 = ok1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc)
1428	  +el = el1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc)
1429	  +hdd = C.ok_d(ld, td, d, hd)
1430	  +hl0 = hlen0(ld, td, l1, d, n, el, hd, hc)
1431	  %Equal.sym(D.Bytes & D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n), (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)),
1432	    fa_eq(ld, td, ls, ts, s, n, l1, t1, e1)) :
1433	    {D.ok(Pair.fst(D.Bytes, D.Bytes, _), d) == True{} : Bool}
1434	  C.ok_mk(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1), d,
1435	    aw_full(NW(ld, n), ts, U32.add(U32.shrn(q, 2n), 1), C.WD(ts, U32.shrn(q, 2n)), t1, U32.shrn(q, 2n), U32.shrn(l1, 2n), SH(q), d, C.ok_full(l1, t1, d, hk1)),
1436	    hdd,
1437	    AB.subst(Nat, y => {Nat.is_le(y, Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}, Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))), U32.to_nat(U32.add(l1, NPw(ld, n))),
1438	      Equal.sym(Nat, U32.to_nat(U32.add(l1, NPw(ld, n))), Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n))), C.add_fits(l1, NPw(ld, n), d, hdd, hl0)), hl0))
1439	
1440	law fast_append_ok_t:
1441	  for +ld: U32
1442	  for +td: P.Tree<U32>
1443	  for +ls: U32
1444	  for +ts: P.Tree<U32>
1445	  for +d: Nat
1446	  for +s: U32
1447	  for +n: U32
1448	  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
1449	  for +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool}
1450	  {D.ok(Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n)), d) == True{} : Bool}
1451	
1452	def fast_append_ok_t(ld, td, ls, ts, d, s, n, hd, hc):
1453	  fao.go(ld, td, ls, ts, d, s, n, hd, hc, C.bmirror(D1(ld, td, ls, ts, s, n)))
1454	
1455	# The view law
1456	# ============
1457	
1458	law esum_n:
1459	  for +a: Nat
1460	  for +h: Nat
1461	  for +nn: Nat
1462	  for +hle: {Nat.is_le(h, nn) == True{} : Bool}
1463	  {Nat.add(Nat.add(a, h), Nat.sub(nn, h)) == Nat.add(a, nn) : Nat}
1464	
1465	def esum_n(a, h, nn, hle):
1466	  Equal.trans(Nat, Nat.add(Nat.add(a, h), Nat.sub(nn, h)), Nat.add(a, Nat.add(h, Nat.sub(nn, h))), Nat.add(a, nn), N.add_assoc(a, h, Nat.sub(nn, h)),
1467	    Equal.cong(Nat, Nat, z => Nat.add(a, z), Nat.add(h, Nat.sub(nn, h)), nn, N.le_sub_add(h, nn, hle)))
1468	
1469	# What the word loop leaves: the bytes in use after the prefix, then src from q.
1470	law avc:
1471	  for +b0: Bool
1472	  for +ld: U32
1473	  for +td: P.Tree<U32>
1474	  for +ls: U32
1475	  for +ts: P.Tree<U32>
1476	  for +d: Nat
1477	  for +e: Nat
1478	  for +s: U32
1479	  for +n: U32
1480	  for +l1: U32
1481	  for +t1: P.Tree<U32>
1482	  for +hb0: {Nat.is_lt(U32.to_nat(H0(ld)), U32.to_nat(n)) == b0 : Bool}
1483	  for +e1: {C.BT(l1, t1) == D1(ld, td, ls, ts, s, n) : D.Bytes}
1484	  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
1485	  for +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool}
1486	  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(C.BT(ls, ts))) == True{} : Bool}
1487	  for +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool}
1488	  {List.take(&2, U32, US(TF(ld, ts, s, n, l1, t1)), Nat.add(U32.to_nat(l1), U32.to_nat(NPw(ld, n)))) == List.append(&2, U32, D.view(C.BT(l1, t1)), List.take(&2, U32, List.drop(&2, U32, US(ts), U32.to_nat(QQ(ld, s, n))), U32.to_nat(NPw(ld, n)))) : List<&2, U32>}
1489	
1490	def avc(b0, ld, td, ls, ts, d, e, s, n, l1, t1, hb0, e1, hd, he, hs, hc):
1491	  match b0:
1492	    case True{}:
1493	      +q = QQ(ld, s, n)
1494	      +qw = U32.shrn(q, 2n)
1495	      +L1 = U32.to_nat(l1)
1496	      +NP = U32.to_nat(NPw(ld, n))
1497	      +qn = U32.to_nat(q)
1498	      +sn = U32.to_nat(s)
1499	      +nn = U32.to_nat(n)
1500	      +hhn = U32.to_nat(HH(ld, n))
1501	      +h0n = U32.to_nat(H0(ld))
1502	      +r0 = U32.to_nat((q .&. 3 : U32))
1503	      +ME = Nat.mul(4n, Nat.pow(2n, e))
1504	      +MD = Nat.mul(4n, Nat.pow(2n, d))
1505	      +v1 = D.view(C.BT(l1, t1))
1506	      +hfs = C.ok_full(ls, ts, e, he)
1507	      +hes = C.ok_d(ls, ts, e, he)
1508	      +hdd = C.ok_d(ld, td, d, hd)
1509	      +hk1 = ok1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc)
1510	      +el = el1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc)
1511	      +hl0 = hlen0(ld, td, l1, d, n, el, hd, hc)
1512	      +hsl = N.le_trans(Nat.add(sn, nn), U32.to_nat(ls), ME, hs, C.ok_len(ls, ts, e, he))
1513	      +ehh = Equal.trans(Nat, hhn, Nat.min(h0n, nn), h0n, U.to_nat_min(H0(ld), n), min_l(h0n, nn, hb0))
1514	      +eL = Equal.trans(Nat, L1, Nat.add(U32.to_nat(ld), hhn), Nat.add(U32.to_nat(ld), h0n), el, Equal.cong(Nat, Nat, z => Nat.add(U32.to_nat(ld), z), hhn, h0n, ehh))
1515	      +hdi0 = Equal.trans(Nat, Nat.mul(U32.to_nat(U32.shrn(l1, 2n)), 4n), Nat.mul(Nat.div(L1, 4n), 4n), Nat.add(L1, 0n),
1516	        Equal.cong(Nat, Nat, z => Nat.mul(z, 4n), U32.to_nat(U32.shrn(l1, 2n)), Nat.div(L1, 4n), U.to_nat_shrn(l1, 2n)),
1517	        Equal.trans(Nat, Nat.mul(Nat.div(L1, 4n), 4n), Nat.mul(Nat.div(Nat.add(U32.to_nat(ld), h0n), 4n), 4n), Nat.add(L1, 0n),
1518	          Equal.cong(Nat, Nat, z => Nat.mul(Nat.div(z, 4n), 4n), L1, Nat.add(U32.to_nat(ld), h0n), eL),
1519	          Equal.trans(Nat, Nat.mul(Nat.div(Nat.add(U32.to_nat(ld), h0n), 4n), 4n), Nat.add(U32.to_nat(ld), h0n), Nat.add(L1, 0n), align(ld),
1520	            Equal.trans(Nat, Nat.add(U32.to_nat(ld), h0n), L1, Nat.add(L1, 0n), Equal.sym(Nat, L1, Nat.add(U32.to_nat(ld), h0n), eL),
1521	              Equal.sym(Nat, Nat.add(L1, 0n), L1, N.add_zero(L1))))))
1522	      +hsi0 = Equal.trans(Nat, Nat.add(Nat.mul(U32.to_nat(qw), 4n), r0), Nat.add(Nat.mul(Nat.div(qn, 4n), 4n), r0), Nat.add(qn, 0n),
1523	        Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, 4n), r0), U32.to_nat(qw), Nat.div(qn, 4n), U.to_nat_shrn(q, 2n)),
1524	        Equal.trans(Nat, Nat.add(Nat.mul(Nat.div(qn, 4n), 4n), r0), qn, Nat.add(qn, 0n), Equal.sym(Nat, qn, Nat.add(Nat.mul(Nat.div(qn, 4n), 4n), r0), exk(q, r0, {==})),
1525	          Equal.sym(Nat, Nat.add(qn, 0n), qn, N.add_zero(qn))))
1526	      +hbq = N.le_trans(Nat.add(sn, hhn), Nat.add(sn, nn), ME, N.le_add_mono_l(sn, hhn, nn, hh_le(ld, n)), hsl)
1527	      +eq = C.add_fits(s, HH(ld, n), e, hes, hbq)
1528	      +hhl = AB.subst(Nat, z => {Nat.is_lt(z, nn) == True{} : Bool}, h0n, hhn, Equal.sym(Nat, hhn, h0n, ehh), hb0)
1529	      +hq4 = AB.subst(Nat, z => {Nat.is_lt(z, ME) == True{} : Bool}, Nat.add(sn, hhn), qn, Equal.sym(Nat, qn, Nat.add(sn, hhn), eq),
1530	        N.lt_le_trans(Nat.add(sn, hhn), Nat.add(sn, nn), ME, N.lt_add_l(sn, hhn, nn, hhl), hsl))
1531	      +hdq = AB.subst(Nat, z => {Nat.is_lt(z, Nat.pow(2n, e)) == True{} : Bool}, Nat.div(qn, 4n), U32.to_nat(qw), Equal.sym(Nat, U32.to_nat(qw), Nat.div(qn, 4n), U.to_nat_shrn(q, 2n)),
1532	        N.div_lt(qn, 4n, Nat.pow(2n, e), {==}, hq4))
1533	      +hp0 = C.inc_fits(qw, e, hes, N.lt_le_trans(U32.to_nat(qw), Nat.pow(2n, e), ME, hdq, N.le_add_r(Nat.pow(2n, e), Nat.add(Nat.pow(2n, e), Nat.add(Nat.pow(2n, e), Nat.add(Nat.pow(2n, e), 0n))))))
1534	      +eqs = Equal.trans(Nat, Nat.add(qn, NP), Nat.add(Nat.add(sn, hhn), NP), Nat.add(sn, nn), Equal.cong(Nat, Nat, z => Nat.add(z, NP), qn, Nat.add(sn, hhn), eq),
1535	        Equal.trans(Nat, Nat.add(Nat.add(sn, hhn), NP), Nat.add(Nat.add(sn, hhn), Nat.sub(nn, hhn)), Nat.add(sn, nn), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sn, hhn), z), NP, Nat.sub(nn, hhn), enp(ld, n)),
1536	          esum_n(sn, hhn, nn, hh_le(ld, n))))
1537	      +hq0 = AB.subst(Nat, z => {Nat.is_le(z, ME) == True{} : Bool}, Nat.add(sn, nn), Nat.add(qn, NP), Equal.sym(Nat, Nat.add(qn, NP), Nat.add(sn, nn), eqs), hsl)
1538	      +hnp = N.le_trans(NP, Nat.add(L1, NP), MD, N.le_add_l(NP, L1), hl0)
1539	      +efit = U.to_nat_add_fits_p(NPw(ld, n), 3, x3_lt_e(NP, U32.to_nat(3), d, 32n, {==}, hnp, C.he32(d, hdd)))
1540	      +enw = Equal.trans(Nat, NW(ld, n), Nat.div(U32.to_nat(U32.add(NPw(ld, n), 3)), 4n), Nat.div(Nat.add(NP, 3n), 4n), U.to_nat_shrn(U32.add(NPw(ld, n), 3), 2n),
1541	        Equal.cong(Nat, Nat, z => Nat.div(z, 4n), U32.to_nat(U32.add(NPw(ld, n), 3)), Nat.add(NP, 3n), efit))
1542	      +hc10 = AB.subst(Nat, z => {Nat.is_le(NP, Nat.mul(z, 4n)) == True{} : Bool}, Nat.div(Nat.add(NP, 3n), 4n), NW(ld, n), Equal.sym(Nat, NW(ld, n), Nat.div(Nat.add(NP, 3n), 4n), enw), cnt1(NP))
1543	      +hc20 = AB.subst(Nat, z => {Nat.is_lt(Nat.mul(z, 4n), Nat.add(NP, 4n)) == True{} : Bool}, Nat.div(Nat.add(NP, 3n), 4n), NW(ld, n), Equal.sym(Nat, NW(ld, n), Nat.div(Nat.add(NP, 3n), 4n), enw), cnt2(NP))
1544	      +hinv0 = Equal.trans(List<&2, U32>, List.take(&2, U32, US(t1), Nat.add(L1, 0n)), List.take(&2, U32, US(t1), L1), List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), 0n)),
1545	        Equal.cong(Nat, List<&2, U32>, z => List.take(&2, U32, US(t1), z), Nat.add(L1, 0n), L1, N.add_zero(L1)),
1546	        Equal.sym(List<&2, U32>, List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), 0n)), v1,
1547	          Equal.trans(List<&2, U32>, List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), 0n)), List.append(&2, U32, v1, Nil{}), v1,
1548	            Equal.cong(List<&2, U32>, List<&2, U32>, z => List.append(&2, U32, v1, z), List.take(&2, U32, List.drop(&2, U32, US(ts), qn), 0n), Nil{}, Q.take_zero(List.drop(&2, U32, US(ts), qn))),
1549	            X.append_nil(v1))))
1550	      av(NW(ld, n), Nat.is_le(Nat.add(0n, 4n), NP), ts, e, t1, d, U32.add(qw, 1), C.WD(ts, qw), qw, U32.shrn(l1, 2n), SH(q), L1, qn, r0, 0n, NP, v1,
1551	        {==}, hfs, hes, C.ok_full(l1, t1, d, hk1), hdd, hdi0, hsi0, hp0, {==}, shq(q), and3_lt(q), hq0, hl0, N.le_zero_l(NP), hc10, hc20, hinv0)
1552	    case False{}:
1553	      +q = QQ(ld, s, n)
1554	      +qw = U32.shrn(q, 2n)
1555	      +L1 = U32.to_nat(l1)
1556	      +NP = U32.to_nat(NPw(ld, n))
1557	      +qn = U32.to_nat(q)
1558	      +nn = U32.to_nat(n)
1559	      +hhn = U32.to_nat(HH(ld, n))
1560	      +v1 = D.view(C.BT(l1, t1))
1561	      +ehh = Equal.trans(Nat, hhn, Nat.min(U32.to_nat(H0(ld)), nn), nn, U.to_nat_min(H0(ld), n), min_r(U32.to_nat(H0(ld)), nn, hb0))
1562	      +enp0 = Equal.trans(Nat, NP, Nat.sub(nn, hhn), 0n, enp(ld, n),
1563	        Equal.trans(Nat, Nat.sub(nn, hhn), Nat.sub(nn, nn), 0n, Equal.cong(Nat, Nat, z => Nat.sub(nn, z), hhn, nn, ehh), H.sub_self(nn)))
1564	      +enw0 = Equal.cong(U32, Nat, z => U32.to_nat(U32.shrn(U32.add(z, 3), 2n)), NPw(ld, n), 0, U.to_nat_inj(NPw(ld, n), 0, enp0))
1565	      %Equal.sym(Nat, NW(ld, n), U32.to_nat(U32.shrn(U32.add(0, 3), 2n)), enw0) :
1566	        {List.take(&2, U32, US(AWT(_, ts, U32.add(qw, 1), C.WD(ts, qw), t1, qw, U32.shrn(l1, 2n), SH(q))), Nat.add(L1, NP)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), NP)) : List<&2, U32>}
1567	      %Equal.sym(Nat, NP, 0n, enp0) :
1568	        {List.take(&2, U32, US(t1), Nat.add(L1, _)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), _)) : List<&2, U32>}
1569	      Equal.trans(List<&2, U32>, List.take(&2, U32, US(t1), Nat.add(L1, 0n)), List.take(&2, U32, US(t1), L1), List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), 0n)),
1570	        Equal.cong(Nat, List<&2, U32>, z => List.take(&2, U32, US(t1), z), Nat.add(L1, 0n), L1, N.add_zero(L1)),
1571	        Equal.sym(List<&2, U32>, List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), 0n)), v1,
1572	          Equal.trans(List<&2, U32>, List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), 0n)), List.append(&2, U32, v1, Nil{}), v1,
1573	            Equal.cong(List<&2, U32>, List<&2, U32>, z => List.append(&2, U32, v1, z), List.take(&2, U32, List.drop(&2, U32, US(ts), qn), 0n), Nil{}, Q.take_zero(List.drop(&2, U32, US(ts), qn))),
1574	            X.append_nil(v1))))
1575	
1576	def fav.go(+ld: U32, +td: P.Tree<U32>, +ls: U32, +ts: P.Tree<U32>, +d: Nat, +e: Nat, +s: U32, +n: U32,
1577	  +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool},
1578	  +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool},
1579	  +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(C.BT(ls, ts))) == True{} : Bool},
1580	  +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool},
1581	  m: C.BMirror(D1(ld, td, ls, ts, s, n))) ->
1582	  {D.view(Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n))) == List.append(&2, U32, D.view(C.BT(ld, td)), D.slice(D.view(C.BT(ls, ts)), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}:
1583	  (+l1, m2) = m
1584	  (+t1, +e1) = m2
1585	  +sn = U32.to_nat(s)
1586	  +nn = U32.to_nat(n)
1587	  +hhn = U32.to_nat(HH(ld, n))
1588	  +L1 = U32.to_nat(l1)
1589	  +NP = U32.to_nat(NPw(ld, n))
1590	  +RHS = List.append(&2, U32, D.view(C.BT(ld, td)), D.slice(D.view(C.BT(ls, ts)), sn, nn))
1591	  +el = el1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc)
1592	  +hl0 = hlen0(ld, td, l1, d, n, el, hd, hc)
1593	  +hss = N.le_trans(Nat.add(sn, hhn), Nat.add(sn, nn), U32.to_nat(ls), N.le_add_mono_l(sn, hhn, nn, hh_le(ld, n)), hs)
1594	  +vd1 = AB.subst(D.Bytes, y => {D.view(y) == List.append(&2, U32, D.view(C.BT(ld, td)), D.slice(D.view(C.BT(ls, ts)), sn, hhn)) : List<&2, U32>},
1595	    D1(ld, td, ls, ts, s, n), C.BT(l1, t1), Equal.sym(D.Bytes, C.BT(l1, t1), D1(ld, td, ls, ts, s, n), e1),
1596	    X.append_view_t(ld, td, ls, ts, d, e, s, HH(ld, n), hd, he, hss, hc_h(ld, td, n, hc)))
1597	  +eq = C.add_fits(s, HH(ld, n), e, C.ok_d(ls, ts, e, he),
1598	    N.le_trans(Nat.add(sn, hhn), U32.to_nat(ls), Nat.mul(4n, Nat.pow(2n, e)), hss, C.ok_len(ls, ts, e, he)))
1599	  %Equal.sym(D.Bytes & D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n), (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)),
1600	    fa_eq(ld, td, ls, ts, s, n, l1, t1, e1)) :
1601	    {D.view(Pair.fst(D.Bytes, D.Bytes, _)) == RHS : List<&2, U32>}
1602	  %Equal.sym(Nat, U32.to_nat(U32.add(l1, NPw(ld, n))), Nat.add(L1, NP), C.add_fits(l1, NPw(ld, n), d, C.ok_d(ld, td, d, hd), hl0)) :
1603	    {List.take(&2, U32, US(TF(ld, ts, s, n, l1, t1)), _) == RHS : List<&2, U32>}
1604	  Equal.trans(List<&2, U32>, List.take(&2, U32, US(TF(ld, ts, s, n, l1, t1)), Nat.add(L1, NP)),
1605	    List.append(&2, U32, D.view(C.BT(l1, t1)), List.take(&2, U32, List.drop(&2, U32, US(ts), U32.to_nat(QQ(ld, s, n))), NP)), RHS,
1606	    avc(Nat.is_lt(U32.to_nat(H0(ld)), nn), ld, td, ls, ts, d, e, s, n, l1, t1, {==}, e1, hd, he, hs, hc),
1607	    fin_eq(D.view(C.BT(l1, t1)), D.view(C.BT(ld, td)), US(ts), U32.to_nat(ls), sn, hhn, U32.to_nat(QQ(ld, s, n)), NP, nn, vd1, eq, enp(ld, n), hh_le(ld, n), hs))
1608	
1609	law fast_append_view_t:
1610	  for +ld: U32
1611	  for +td: P.Tree<U32>
1612	  for +ls: U32
1613	  for +ts: P.Tree<U32>
1614	  for +d: Nat
1615	  for +e: Nat
1616	  for +s: U32
1617	  for +n: U32
1618	  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
1619	  for +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool}
1620	  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(C.BT(ls, ts))) == True{} : Bool}
1621	  for +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool}
1622	  {D.view(Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n))) == List.append(&2, U32, D.view(C.BT(ld, td)), D.slice(D.view(C.BT(ls, ts)), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}
1623	
1624	def fast_append_view_t(ld, td, ls, ts, d, e, s, n, hd, he, hs, hc):
1625	  fav.go(ld, td, ls, ts, d, e, s, n, hd, he, hs, hc, C.bmirror(D1(ld, td, ls, ts, s, n)))