1	import Base
2	import ./defs.bend as D
3	import ./bytes.bend as B
4	import ./proof_seq.bend as Q
5	import ./proof_core.bend as C
6	import ./proof_ops.bend as O
7	import lawful-words@0.1.0.0/defs.bend as W
8	import lawful-words@0.1.0.0/proof_nat.bend as N
9	import lawful-words@0.1.0.0/proof_bytes.bend as Y
10	import lawful-arrays@0.1.0.0/proof_base.bend as AB
11	import lawful-arrays@0.1.0.0/proof_tree.bend as P
12	import lawful-arrays@0.1.0.0/proof_index.bend as I
13	
14	# append: n pushes onto dst of bytes s.. of src, and shift, laws on the mirror
15	# (named as in proof_ops.bend). The loop lemmas take dst as a mirror that changes
16	# at every push (O.push_eq_t names the new one) and src as a fixed mirror.
17	
18	# Lists
19	# =====
20	
21	law append_nil:
22	  for +xs: List<&2, U32>
23	  {List.append(&2, U32, xs, Nil{}) == xs : List<&2, U32>}
24	
25	def append_nil(xs):
26	  match xs:
27	    case Nil{}:
28	      {==}
29	    case Con{+x, t}:
30	      %append_nil(t) : {x <> List.append(&2, U32, t, Nil{}) == x <> _ : List<&2, U32>}
31	      {==}
32	
33	law append_assoc:
34	  for +xs: List<&2, U32>
35	  for +ys: List<&2, U32>
36	  for +zs: List<&2, U32>
37	  {List.append(&2, U32, List.append(&2, U32, xs, ys), zs) == List.append(&2, U32, xs, List.append(&2, U32, ys, zs)) : List<&2, U32>}
38	
39	def append_assoc(xs, ys, zs):
40	  match xs:
41	    case Nil{}:
42	      {==}
43	    case Con{+x, t}:
44	      %append_assoc(t, ys, zs) :
45	        {x <> List.append(&2, U32, List.append(&2, U32, t, ys), zs) == x <> _ : List<&2, U32>}
46	      {==}
47	
48	law drop_zero:
49	  for +xs: List<&2, U32>
50	  {List.drop(&2, U32, xs, 0n) == xs : List<&2, U32>}
51	
52	def drop_zero(xs):
53	  match xs:
54	    case Nil{}:
55	      {==}
56	    case Con{x, t}:
57	      {==}
58	
59	def is_some_t(m: Maybe<&2, U32>) -> Type:
60	  match m:
61	    case None{}:
62	      Unit
63	    case Some{x}:
64	      Empty
65	
66	law none_some:
67	  for -x: U32
68	  for e: {None{} == Some{x} : Maybe<&2, U32>}
69	  Empty
70	
71	def none_some(x, e):
72	  %e : is_some_t(_)
73	  Unit{}
74	
75	law some_inj:
76	  for +x: U32
77	  for +y: U32
78	  for +e: {Some{x} == Some{y} : Maybe<&2, U32>}
79	  {x == y : U32}
80	
81	def some_inj(x, y, e):
82	  Equal.cong(Maybe<&2, U32>, U32, m => I.unsome(U32, x, m), Some{x}, Some{y}, e)
83	
84	law slice_zero:
85	  for +xs: List<&2, U32>
86	  for +i: Nat
87	  {D.slice(xs, i, 0n) == Nil{} : List<&2, U32>}
88	
89	def slice_zero(xs, i):
90	  Q.take_zero(List.drop(&2, U32, xs, i))
91	
92	# A slice of 1 + k from i starts with element i.
93	law slice_cons:
94	  for +xs: List<&2, U32>
95	  for +i: Nat
96	  for +k: Nat
97	  for +x: U32
98	  for +h: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}
99	  {D.slice(xs, i, 1n+k) == x <> D.slice(xs, Nat.add(i, 1n), k) : List<&2, U32>}
100	
101	def slice_cons(xs, i, k, x, h):
102	  match xs i:
103	    case Nil{} _:
104	      Empty.absurd({D.slice(Nil{}, i, 1n+k) == x <> D.slice(Nil{}, Nat.add(i, 1n), k) : List<&2, U32>}, none_some(x, h))
105	    case Con{+y, t} 0n:
106	      %some_inj(y, x, h) : {y <> List.take(&2, U32, t, k) == _ <> List.take(&2, U32, List.drop(&2, U32, t, 0n), k) : List<&2, U32>}
107	      %Equal.sym(List<&2, U32>, List.drop(&2, U32, t, 0n), t, drop_zero(t)) :
108	        {y <> List.take(&2, U32, t, k) == y <> List.take(&2, U32, _, k) : List<&2, U32>}
109	      {==}
110	    case Con{y, t} 1n+p:
111	      slice_cons(t, p, k, x, h)
112	
113	# Nat order
114	# =========
115	
116	law le_split:
117	  for +a: Nat
118	  for +k: Nat
119	  for +m: Nat
120	  for +h: {Nat.is_le(Nat.add(a, 1n+k), m) == True{} : Bool}
121	  {Nat.is_lt(a, m) == True{} : Bool}
122	
123	def le_split(a, k, m, h):
124	  +h2 = AB.subst(Nat, y => {Nat.is_le(y, m) == True{} : Bool}, Nat.add(a, 1n+k), 1n+Nat.add(a, k), N.add_succ(a, k), h)
125	  N.le_lt_trans(a, Nat.add(a, k), m, N.le_add_r(a, k),
126	    Equal.trans(Bool, Nat.is_lt(Nat.add(a, k), m), Nat.is_le(1n+Nat.add(a, k), m), True{},
127	      Equal.sym(Bool, Nat.is_le(1n+Nat.add(a, k), m), Nat.is_lt(Nat.add(a, k), m), N.le_succ_lt(Nat.add(a, k), m)), h2))
128	
129	law le_shift:
130	  for +a: Nat
131	  for +k: Nat
132	  for +m: Nat
133	  for +h: {Nat.is_le(Nat.add(a, 1n+k), m) == True{} : Bool}
134	  {Nat.is_le(Nat.add(Nat.add(a, 1n), k), m) == True{} : Bool}
135	
136	def le_shift(a, k, m, h):
137	  %Equal.sym(Nat, Nat.add(Nat.add(a, 1n), k), Nat.add(a, Nat.add(1n, k)), N.add_assoc(a, 1n, k)) : {Nat.is_le(_, m) == True{} : Bool}
138	  h
139	
140	# One push
141	# ========
142	
143	# The tree after pushing x onto BT(ld, td).
144	def PT(+ld: U32, +td: P.Tree<U32>, +x: U32) -> P.Tree<U32>:
145	  I.set_tree(U32, td, (ld >> 2n : U32), W.put_byte(C.WD(td, (ld >> 2n : U32)), U32.to_nat((ld .&. 3 : U32)), x))
146	
147	law step_room:
148	  for +ld: U32
149	  for +td: P.Tree<U32>
150	  for +d: Nat
151	  for +k: Nat
152	  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
153	  for +hc: {Nat.is_le(Nat.add(U32.to_nat(ld), 1n+k), D.cap(C.BT(ld, td))) == True{} : Bool}
154	  {Nat.is_lt(U32.to_nat(ld), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
155	
156	def step_room(ld, td, d, k, hd, hc):
157	  +M = Nat.mul(4n, Nat.pow(2n, d))
158	  le_split(U32.to_nat(ld), k, M,
159	    AB.subst(Nat, y => {Nat.is_le(Nat.add(U32.to_nat(ld), 1n+k), y) == True{} : Bool}, D.cap(C.BT(ld, td)), M, O.cap_ok_t(ld, td, d, hd), hc))
160	
161	law step_lt:
162	  for +ld: U32
163	  for +td: P.Tree<U32>
164	  for +d: Nat
165	  for +k: Nat
166	  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
167	  for +hc: {Nat.is_le(Nat.add(U32.to_nat(ld), 1n+k), D.cap(C.BT(ld, td))) == True{} : Bool}
168	  {Nat.is_lt(D.size(C.BT(ld, td)), D.cap(C.BT(ld, td))) == True{} : Bool}
169	
170	def step_lt(ld, td, d, k, hd, hc):
171	  le_split(U32.to_nat(ld), k, D.cap(C.BT(ld, td)), hc)
172	
173	law step_ok:
174	  for +ld: U32
175	  for +td: P.Tree<U32>
176	  for +d: Nat
177	  for +x: U32
178	  for +k: Nat
179	  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
180	  for +hc: {Nat.is_le(Nat.add(U32.to_nat(ld), 1n+k), D.cap(C.BT(ld, td))) == True{} : Bool}
181	  {D.ok(C.BT((ld + 1 : U32), PT(ld, td, x)), d) == True{} : Bool}
182	
183	def step_ok(ld, td, d, x, k, hd, hc):
184	  AB.subst(D.Bytes, y => {D.ok(y, d) == True{} : Bool}, B.push(C.BT(ld, td), x), C.BT((ld + 1 : U32), PT(ld, td, x)),
185	    O.push_eq_t(ld, td, x), O.push_ok_t(ld, td, d, x, hd, step_lt(ld, td, d, k, hd, hc)))
186	
187	law step_cap:
188	  for +ld: U32
189	  for +td: P.Tree<U32>
190	  for +d: Nat
191	  for +x: U32
192	  for +k: Nat
193	  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
194	  for +hc: {Nat.is_le(Nat.add(U32.to_nat(ld), 1n+k), D.cap(C.BT(ld, td))) == True{} : Bool}
195	  {Nat.is_le(Nat.add(U32.to_nat((ld + 1 : U32)), k), D.cap(C.BT((ld + 1 : U32), PT(ld, td, x)))) == True{} : Bool}
196	
197	def step_cap(ld, td, d, x, k, hd, hc):
198	  +M = Nat.mul(4n, Nat.pow(2n, d))
199	  +hr = step_room(ld, td, d, k, hd, hc)
200	  %Equal.sym(Nat, D.cap(C.BT((ld + 1 : U32), PT(ld, td, x))), M, O.cap_ok_t((ld + 1 : U32), PT(ld, td, x), d, step_ok(ld, td, d, x, k, hd, hc))) :
201	    {Nat.is_le(Nat.add(U32.to_nat((ld + 1 : U32)), k), _) == True{} : Bool}
202	  %Equal.sym(Nat, U32.to_nat((ld + 1 : U32)), Nat.add(U32.to_nat(ld), 1n), C.inc_fits(ld, d, C.ok_d(ld, td, d, hd), hr)) :
203	    {Nat.is_le(Nat.add(_, k), M) == True{} : Bool}
204	  le_shift(U32.to_nat(ld), k, M,
205	    AB.subst(Nat, y => {Nat.is_le(Nat.add(U32.to_nat(ld), 1n+k), y) == True{} : Bool}, D.cap(C.BT(ld, td)), M, O.cap_ok_t(ld, td, d, hd), hc))
206	
207	# One read of src
208	# ===============
209	
210	law read_lt:
211	  for +ls: U32
212	  for +s: U32
213	  for +k: Nat
214	  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+k), U32.to_nat(ls)) == True{} : Bool}
215	  {Nat.is_lt(U32.to_nat(s), U32.to_nat(ls)) == True{} : Bool}
216	
217	def read_lt(ls, s, k, hs):
218	  le_split(U32.to_nat(s), k, U32.to_nat(ls), hs)
219	
220	law read_inc:
221	  for +ls: U32
222	  for +ts: P.Tree<U32>
223	  for +e: Nat
224	  for +s: U32
225	  for +k: Nat
226	  for +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool}
227	  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+k), U32.to_nat(ls)) == True{} : Bool}
228	  {U32.to_nat((s + 1 : U32)) == Nat.add(U32.to_nat(s), 1n) : Nat}
229	
230	def read_inc(ls, ts, e, s, k, he, hs):
231	  C.inc_fits(s, e, C.ok_d(ls, ts, e, he),
232	    N.lt_le_trans(U32.to_nat(s), U32.to_nat(ls), Nat.mul(4n, Nat.pow(2n, e)), read_lt(ls, s, k, hs), C.ok_len(ls, ts, e, he)))
233	
234	law read_next:
235	  for +ls: U32
236	  for +ts: P.Tree<U32>
237	  for +e: Nat
238	  for +s: U32
239	  for +k: Nat
240	  for +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool}
241	  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+k), U32.to_nat(ls)) == True{} : Bool}
242	  {Nat.is_le(Nat.add(U32.to_nat((s + 1 : U32)), k), U32.to_nat(ls)) == True{} : Bool}
243	
244	def read_next(ls, ts, e, s, k, he, hs):
245	  %Equal.sym(Nat, U32.to_nat((s + 1 : U32)), Nat.add(U32.to_nat(s), 1n), read_inc(ls, ts, e, s, k, he, hs)) :
246	    {Nat.is_le(Nat.add(_, k), U32.to_nat(ls)) == True{} : Bool}
247	  le_shift(U32.to_nat(s), k, U32.to_nat(ls), hs)
248	
249	# append
250	# ======
251	
252	law append_go_pair:
253	  for +n: Nat
254	  for -dst: D.Bytes
255	  for +ls: U32
256	  for +ts: P.Tree<U32>
257	  for +s: U32
258	  {B.append.go(n, dst, B.at(C.BT(ls, ts), s), s) == (Pair.fst(D.Bytes, D.Bytes, B.append.go(n, dst, B.at(C.BT(ls, ts), s), s)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
259	
260	def append_go_pair(n, dst, ls, ts, s):
261	  match n:
262	    case 0n:
263	      %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)) :
264	        {B.append.go(0n, dst, _, s) == (Pair.fst(D.Bytes, D.Bytes, B.append.go(0n, dst, _, s)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
265	      {==}
266	    case 1n+k:
267	      %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)) :
268	        {B.append.go(1n+k, dst, _, s) == (Pair.fst(D.Bytes, D.Bytes, B.append.go(1n+k, dst, _, s)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
269	      append_go_pair(k, B.push(dst, C.AT(ls, ts, s)), ls, ts, (s + 1 : U32))
270	
271	law append_pair_t:
272	  for +ld: U32
273	  for +td: P.Tree<U32>
274	  for +ls: U32
275	  for +ts: P.Tree<U32>
276	  for +s: U32
277	  for +n: U32
278	  {B.append(C.BT(ld, td), C.BT(ls, ts), s, n) == (Pair.fst(D.Bytes, D.Bytes, B.append(C.BT(ld, td), C.BT(ls, ts), s, n)), C.BT(ls, ts)) : D.Bytes & D.Bytes}
279	
280	def append_pair_t(ld, td, ls, ts, s, n):
281	  append_go_pair(U32.to_nat(n), C.BT(ld, td), ls, ts, s)
282	
283	law append_go_ok:
284	  for +n: Nat
285	  for +ld: U32
286	  for +td: P.Tree<U32>
287	  for +ls: U32
288	  for +ts: P.Tree<U32>
289	  for +d: Nat
290	  for +s: U32
291	  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
292	  for +hc: {Nat.is_le(Nat.add(U32.to_nat(ld), n), D.cap(C.BT(ld, td))) == True{} : Bool}
293	  {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append.go(n, C.BT(ld, td), B.at(C.BT(ls, ts), s), s)), d) == True{} : Bool}
294	
295	def append_go_ok(n, ld, td, ls, ts, d, s, hd, hc):
296	  match n:
297	    case 0n:
298	      %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)) :
299	        {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append.go(0n, C.BT(ld, td), _, s)), d) == True{} : Bool}
300	      hd
301	    case 1n+k:
302	      +x = C.AT(ls, ts, s)
303	      %Equal.sym(D.Bytes & U32, B.at(C.BT(ls, ts), s), (C.BT(ls, ts), x), C.at_pair_t(ls, ts, s)) :
304	        {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append.go(1n+k, C.BT(ld, td), _, s)), d) == True{} : Bool}
305	      %Equal.sym(D.Bytes, B.push(C.BT(ld, td), x), C.BT((ld + 1 : U32), PT(ld, td, x)), O.push_eq_t(ld, td, x)) :
306	        {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append.go(k, _, B.at(C.BT(ls, ts), (s + 1 : U32)), (s + 1 : U32))), d) == True{} : Bool}
307	      append_go_ok(k, (ld + 1 : U32), PT(ld, td, x), ls, ts, d, (s + 1 : U32), step_ok(ld, td, d, x, k, hd, hc), step_cap(ld, td, d, x, k, hd, hc))
308	
309	law append_ok_t:
310	  for +ld: U32
311	  for +td: P.Tree<U32>
312	  for +ls: U32
313	  for +ts: P.Tree<U32>
314	  for +d: Nat
315	  for +s: U32
316	  for +n: U32
317	  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
318	  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}
319	  {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append(C.BT(ld, td), C.BT(ls, ts), s, n)), d) == True{} : Bool}
320	
321	def append_ok_t(ld, td, ls, ts, d, s, n, hd, hc):
322	  append_go_ok(U32.to_nat(n), ld, td, ls, ts, d, s, hd, hc)
323	
324	law append_go_view:
325	  for +n: Nat
326	  for +ld: U32
327	  for +td: P.Tree<U32>
328	  for +ls: U32
329	  for +ts: P.Tree<U32>
330	  for +d: Nat
331	  for +e: Nat
332	  for +s: U32
333	  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
334	  for +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool}
335	  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), n), U32.to_nat(ls)) == True{} : Bool}
336	  for +hc: {Nat.is_le(Nat.add(U32.to_nat(ld), n), D.cap(C.BT(ld, td))) == True{} : Bool}
337	  {D.view(Pair.fst(D.Bytes, D.Bytes, B.append.go(n, C.BT(ld, td), B.at(C.BT(ls, ts), s), s))) == List.append(&2, U32, D.view(C.BT(ld, td)), D.slice(D.view(C.BT(ls, ts)), U32.to_nat(s), n)) : List<&2, U32>}
338	
339	def append_go_view(n, ld, td, ls, ts, d, e, s, hd, he, hs, hc):
340	  match n:
341	    case 0n:
342	      +V = D.view(C.BT(ld, td))
343	      +xs = D.view(C.BT(ls, ts))
344	      %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)) :
345	        {D.view(Pair.fst(D.Bytes, D.Bytes, B.append.go(0n, C.BT(ld, td), _, s))) == List.append(&2, U32, V, D.slice(xs, U32.to_nat(s), 0n)) : List<&2, U32>}
346	      %Equal.sym(List<&2, U32>, D.slice(xs, U32.to_nat(s), 0n), Nil{}, slice_zero(xs, U32.to_nat(s))) :
347	        {V == List.append(&2, U32, V, _) : List<&2, U32>}
348	      Equal.sym(List<&2, U32>, List.append(&2, U32, V, Nil{}), V, append_nil(V))
349	    case 1n+k:
350	      +x = C.AT(ls, ts, s)
351	      +s1 = (s + 1 : U32)
352	      +ld1 = (ld + 1 : U32)
353	      +td1 = PT(ld, td, x)
354	      +V = D.view(C.BT(ld, td))
355	      +xs = D.view(C.BT(ls, ts))
356	      +RHS = List.append(&2, U32, V, D.slice(xs, U32.to_nat(s), 1n+k))
357	      %Equal.sym(D.Bytes & U32, B.at(C.BT(ls, ts), s), (C.BT(ls, ts), x), C.at_pair_t(ls, ts, s)) :
358	        {D.view(Pair.fst(D.Bytes, D.Bytes, B.append.go(1n+k, C.BT(ld, td), _, s))) == RHS : List<&2, U32>}
359	      %Equal.sym(D.Bytes, B.push(C.BT(ld, td), x), C.BT(ld1, td1), O.push_eq_t(ld, td, x)) :
360	        {D.view(Pair.fst(D.Bytes, D.Bytes, B.append.go(k, _, B.at(C.BT(ls, ts), s1), s1))) == RHS : List<&2, U32>}
361	      +hd1 = step_ok(ld, td, d, x, k, hd, hc)
362	      %Equal.sym(List<&2, U32>, D.view(Pair.fst(D.Bytes, D.Bytes, B.append.go(k, C.BT(ld1, td1), B.at(C.BT(ls, ts), s1), s1))),
363	        List.append(&2, U32, D.view(C.BT(ld1, td1)), D.slice(xs, U32.to_nat(s1), k)),
364	        append_go_view(k, ld1, td1, ls, ts, d, e, s1, hd1, he, read_next(ls, ts, e, s, k, he, hs), step_cap(ld, td, d, x, k, hd, hc))) :
365	        {_ == RHS : List<&2, U32>}
366	      +hv = AB.subst(U32, y => {U32.is_lt(y, 256) == True{} : Bool}, W.byte(C.WD(ts, (s >> 2n : U32)), U32.to_nat((s .&. 3 : U32))), x,
367	        Equal.sym(U32, x, W.byte(C.WD(ts, (s >> 2n : U32)), U32.to_nat((s .&. 3 : U32))), C.at_val(ls, ts, s)),
368	        Y.byte_lt(C.WD(ts, (s >> 2n : U32)), U32.to_nat((s .&. 3 : U32))))
369	      +pv = AB.subst(D.Bytes, y => {D.view(y) == List.append(&2, U32, V, [x]) : List<&2, U32>}, B.push(C.BT(ld, td), x), C.BT(ld1, td1),
370	        O.push_eq_t(ld, td, x), O.push_view_t(ld, td, d, x, hd, step_lt(ld, td, d, k, hd, hc), hv))
371	      %Equal.sym(List<&2, U32>, D.view(C.BT(ld1, td1)), List.append(&2, U32, V, [x]), pv) :
372	        {List.append(&2, U32, _, D.slice(xs, U32.to_nat(s1), k)) == RHS : List<&2, U32>}
373	      %Equal.sym(Nat, U32.to_nat(s1), Nat.add(U32.to_nat(s), 1n), read_inc(ls, ts, e, s, k, he, hs)) :
374	        {List.append(&2, U32, List.append(&2, U32, V, [x]), D.slice(xs, _, k)) == RHS : List<&2, U32>}
375	      +hx = Equal.sym(Maybe<&2, U32>, Some{x}, List.get(&2, U32, xs, U32.to_nat(s)),
376	        C.at_view_t(ls, ts, e, s, C.ok_full(ls, ts, e, he), C.ok_d(ls, ts, e, he), C.ok_len(ls, ts, e, he), read_lt(ls, s, k, hs)))
377	      %Equal.sym(List<&2, U32>, D.slice(xs, U32.to_nat(s), 1n+k), x <> D.slice(xs, Nat.add(U32.to_nat(s), 1n), k),
378	        slice_cons(xs, U32.to_nat(s), k, x, hx)) :
379	        {List.append(&2, U32, List.append(&2, U32, V, [x]), D.slice(xs, Nat.add(U32.to_nat(s), 1n), k)) == List.append(&2, U32, V, _) : List<&2, U32>}
380	      append_assoc(V, [x], D.slice(xs, Nat.add(U32.to_nat(s), 1n), k))
381	
382	law append_view_t:
383	  for +ld: U32
384	  for +td: P.Tree<U32>
385	  for +ls: U32
386	  for +ts: P.Tree<U32>
387	  for +d: Nat
388	  for +e: Nat
389	  for +s: U32
390	  for +n: U32
391	  for +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool}
392	  for +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool}
393	  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(C.BT(ls, ts))) == True{} : Bool}
394	  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}
395	  {D.view(Pair.fst(D.Bytes, D.Bytes, B.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>}
396	
397	def append_view_t(ld, td, ls, ts, d, e, s, n, hd, he, hs, hc):
398	  append_go_view(U32.to_nat(n), ld, td, ls, ts, d, e, s, hd, he, hs, hc)