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 lawful-words@0.1.0.0/defs.bend as W
7	import lawful-words@0.1.0.0/proof_nat.bend as N
8	import lawful-words@0.1.0.0/proof_u32.bend as U
9	import lawful-arrays@0.1.0.0/defs.bend as A
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	# find and find2 on the mirror C.BT(len, t). The loops read one byte ahead:
15	# r holds byte j + 1 while hit says whether byte j matched. Each lemma takes r
16	# as a literal pair (C.BT(len, t), byte) so the loop's destructuring computes;
17	# the next read is rewritten into that form with C.at_pair_t.
18	
19	# Small facts
20	# ===========
21	
22	def is_some_t(m: Maybe<&2, U32>) -> Type:
23	  match m:
24	    case None{}:
25	      Unit
26	    case Some{x}:
27	      Empty
28	
29	law none_ne_some:
30	  for -x: U32
31	  for e: {None{} == Some{x} : Maybe<&2, U32>}
32	  Empty
33	
34	def none_ne_some(x, e):
35	  AB.subst(Maybe<&2, U32>, m => is_some_t(m), None{}, Some{x}, e, Unit{})
36	
37	law drop_zero:
38	  for +xs: List<&2, U32>
39	  {List.drop(&2, U32, xs, 0n) == xs : List<&2, U32>}
40	
41	def drop_zero(xs):
42	  match xs:
43	    case Nil{}:
44	      {==}
45	    case Con{x, t}:
46	      {==}
47	
48	# Dropping j elements from a list with x at j leaves x in front.
49	law drop_cons:
50	  for +xs: List<&2, U32>
51	  for +j: Nat
52	  for +x: U32
53	  for +hx: {List.get(&2, U32, xs, j) == Some{x} : Maybe<&2, U32>}
54	  {List.drop(&2, U32, xs, j) == x <> List.drop(&2, U32, xs, Nat.add(j, 1n)) : List<&2, U32>}
55	
56	def drop_cons(xs, j, x, hx):
57	  match xs j:
58	    case Nil{} _:
59	      Empty.absurd({Nil{} == x <> Nil{} : List<&2, U32>}, none_ne_some(x, hx))
60	    case Con{+y, t} 0n:
61	      +yx = Equal.cong(Maybe<&2, U32>, U32, m => I.unsome(U32, y, m), Some{y}, Some{x}, hx)
62	      %Equal.sym(List<&2, U32>, List.drop(&2, U32, t, 0n), t, drop_zero(t)) : {y <> t == x <> _ : List<&2, U32>}
63	      %yx : {y <> t == _ <> t : List<&2, U32>}
64	      {==}
65	    case Con{y, t} 1n+p:
66	      drop_cons(t, p, x, hx)
67	
68	law slice_cons:
69	  for +xs: List<&2, U32>
70	  for +j: Nat
71	  for +k: Nat
72	  for +x: U32
73	  for +hx: {List.get(&2, U32, xs, j) == Some{x} : Maybe<&2, U32>}
74	  {D.slice(xs, j, 1n+k) == x <> D.slice(xs, Nat.add(j, 1n), k) : List<&2, U32>}
75	
76	def slice_cons(xs, j, k, x, hx):
77	  %Equal.sym(List<&2, U32>, List.drop(&2, U32, xs, j), x <> List.drop(&2, U32, xs, Nat.add(j, 1n)), drop_cons(xs, j, x, hx)) :
78	    {List.take(&2, U32, _, 1n+k) == x <> D.slice(xs, Nat.add(j, 1n), k) : List<&2, U32>}
79	  {==}
80	
81	law lt_add_succ:
82	  for +a: Nat
83	  for +k: Nat
84	  {Nat.is_lt(a, Nat.add(a, 1n+k)) == True{} : Bool}
85	
86	def lt_add_succ(a, k):
87	  match a:
88	    case 0n:
89	      {==}
90	    case 1n+p:
91	      lt_add_succ(p, k)
92	
93	# (j + 1) + 1 is j + 2, for every word j (no range needed: through from_nat).
94	law add11:
95	  for +j: U32
96	  {U32.add(U32.add(j, 1), 1) == U32.add(j, 2) : U32}
97	
98	def add11(j):
99	  +tj = U32.to_nat(j)
100	  %U.from_nat_to_nat(j) : {U32.add(U32.add(_, 1), 1) == U32.add(j, 2) : U32}
101	  %U.from_nat_add(tj, 1n) : {U32.add(_, 1) == U32.add(j, 2) : U32}
102	  %U.from_nat_add(Nat.add(tj, 1n), 1n) : {_ == U32.add(j, 2) : U32}
103	  %Equal.sym(Nat, Nat.add(Nat.add(tj, 1n), 1n), Nat.add(tj, Nat.add(1n, 1n)), N.add_assoc(tj, 1n, 1n)) :
104	    {U32.from_nat(_) == U32.add(j, 2) : U32}
105	  %U.from_nat_to_nat(j) : {U32.from_nat(Nat.add(tj, 2n)) == U32.add(_, 2) : U32}
106	  U.from_nat_add(tj, 2n)
107	
108	# The loops hand the buffer back
109	# ==============================
110	
111	law fgo_pair:
112	  for n: Nat
113	  for +hit: Bool
114	  for +len: U32
115	  for +t: P.Tree<U32>
116	  for +x: U32
117	  for +j: U32
118	  for +to: U32
119	  for +c: U32
120	  {B.find.go(n, hit, (C.BT(len, t), x), j, to, c) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find.go(n, hit, (C.BT(len, t), x), j, to, c))) : D.Bytes & U32}
121	
122	def fgo_pair(n, hit, len, t, x, j, to, c):
123	  match n hit:
124	    case 0n _:
125	      {==}
126	    case 1n+k True{}:
127	      {==}
128	    case 1n+k False{}:
129	      +H = U32.is_eq(x, c)
130	      +j2 = (j + 2 : U32)
131	      %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j2), (C.BT(len, t), C.AT(len, t, j2)), C.at_pair_t(len, t, j2)) :
132	        {B.find.go(k, H, _, (j + 1 : U32), to, c) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find.go(k, H, _, (j + 1 : U32), to, c))) : D.Bytes & U32}
133	      fgo_pair(k, H, len, t, C.AT(len, t, j2), (j + 1 : U32), to, c)
134	
135	law find_pair_t:
136	  for +len: U32
137	  for +t: P.Tree<U32>
138	  for +from: U32
139	  for +to: U32
140	  for +c: U32
141	  {B.find(C.BT(len, t), from, to, c) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find(C.BT(len, t), from, to, c))) : D.Bytes & U32}
142	
143	def find_pair_t(len, t, from, to, c):
144	  +n = Nat.sub(U32.to_nat(to), U32.to_nat(from))
145	  +f1 = (from + 1 : U32)
146	  +H = U32.is_eq(C.AT(len, t, from), c)
147	  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), from), (C.BT(len, t), C.AT(len, t, from)), C.at_pair_t(len, t, from)) :
148	    {B.find.start(n, _, from, to, c) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find.start(n, _, from, to, c))) : D.Bytes & U32}
149	  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), f1), (C.BT(len, t), C.AT(len, t, f1)), C.at_pair_t(len, t, f1)) :
150	    {B.find.go(n, H, _, from, to, c) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find.go(n, H, _, from, to, c))) : D.Bytes & U32}
151	  fgo_pair(n, H, len, t, C.AT(len, t, f1), from, to, c)
152	
153	law fgo2_pair:
154	  for n: Nat
155	  for +hit: Bool
156	  for +len: U32
157	  for +t: P.Tree<U32>
158	  for +x: U32
159	  for +j: U32
160	  for +to: U32
161	  for +c1: U32
162	  for +c2: U32
163	  {B.find2.go(n, hit, (C.BT(len, t), x), j, to, c1, c2) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find2.go(n, hit, (C.BT(len, t), x), j, to, c1, c2))) : D.Bytes & U32}
164	
165	def fgo2_pair(n, hit, len, t, x, j, to, c1, c2):
166	  match n hit:
167	    case 0n _:
168	      {==}
169	    case 1n+k True{}:
170	      {==}
171	    case 1n+k False{}:
172	      +H = U32.is_eq(x, c1) || U32.is_eq(x, c2)
173	      +j2 = (j + 2 : U32)
174	      %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j2), (C.BT(len, t), C.AT(len, t, j2)), C.at_pair_t(len, t, j2)) :
175	        {B.find2.go(k, H, _, (j + 1 : U32), to, c1, c2) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find2.go(k, H, _, (j + 1 : U32), to, c1, c2))) : D.Bytes & U32}
176	      fgo2_pair(k, H, len, t, C.AT(len, t, j2), (j + 1 : U32), to, c1, c2)
177	
178	law find2_pair_t:
179	  for +len: U32
180	  for +t: P.Tree<U32>
181	  for +from: U32
182	  for +to: U32
183	  for +c1: U32
184	  for +c2: U32
185	  {B.find2(C.BT(len, t), from, to, c1, c2) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find2(C.BT(len, t), from, to, c1, c2))) : D.Bytes & U32}
186	
187	def find2_pair_t(len, t, from, to, c1, c2):
188	  +n = Nat.sub(U32.to_nat(to), U32.to_nat(from))
189	  +f1 = (from + 1 : U32)
190	  +x0 = C.AT(len, t, from)
191	  +H = U32.is_eq(x0, c1) || U32.is_eq(x0, c2)
192	  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), from), (C.BT(len, t), x0), C.at_pair_t(len, t, from)) :
193	    {B.find2.start(n, _, from, to, c1, c2) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find2.start(n, _, from, to, c1, c2))) : D.Bytes & U32}
194	  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), f1), (C.BT(len, t), C.AT(len, t, f1)), C.at_pair_t(len, t, f1)) :
195	    {B.find2.go(n, H, _, from, to, c1, c2) == (C.BT(len, t), Pair.snd(D.Bytes, U32, B.find2.go(n, H, _, from, to, c1, c2))) : D.Bytes & U32}
196	  fgo2_pair(n, H, len, t, C.AT(len, t, f1), from, to, c1, c2)
197	
198	# Index steps
199	# ===========
200	
201	# With j + 1 + k = to <= len, byte j is in range.
202	law step_lt:
203	  for +len: U32
204	  for +j: U32
205	  for +to: U32
206	  for +k: Nat
207	  for +hn: {Nat.add(U32.to_nat(j), 1n+k) == U32.to_nat(to) : Nat}
208	  for +hto: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
209	  {Nat.is_lt(U32.to_nat(j), U32.to_nat(len)) == True{} : Bool}
210	
211	def step_lt(len, j, to, k, hn, hto):
212	  +tj = U32.to_nat(j)
213	  N.lt_le_trans(tj, U32.to_nat(to), U32.to_nat(len),
214	    AB.subst(Nat, x => {Nat.is_lt(tj, x) == True{} : Bool}, Nat.add(tj, 1n+k), U32.to_nat(to), hn, lt_add_succ(tj, k)),
215	    hto)
216	
217	law step_lt4:
218	  for +len: U32
219	  for +t: P.Tree<U32>
220	  for +d: Nat
221	  for +j: U32
222	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
223	  for +hj: {Nat.is_lt(U32.to_nat(j), U32.to_nat(len)) == True{} : Bool}
224	  {Nat.is_lt(U32.to_nat(j), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
225	
226	def step_lt4(len, t, d, j, h, hj):
227	  N.lt_le_trans(U32.to_nat(j), U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), hj, C.ok_len(len, t, d, h))
228	
229	law step_get:
230	  for +len: U32
231	  for +t: P.Tree<U32>
232	  for +d: Nat
233	  for +j: U32
234	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
235	  for +hj: {Nat.is_lt(U32.to_nat(j), U32.to_nat(len)) == True{} : Bool}
236	  {List.get(&2, U32, D.view(C.BT(len, t)), U32.to_nat(j)) == Some{C.AT(len, t, j)} : Maybe<&2, U32>}
237	
238	def step_get(len, t, d, j, h, hj):
239	  Equal.sym(Maybe<&2, U32>, Some{C.AT(len, t, j)}, List.get(&2, U32, D.view(C.BT(len, t)), U32.to_nat(j)),
240	    C.at_view_t(len, t, d, j, C.ok_full(len, t, d, h), C.ok_d(len, t, d, h), C.ok_len(len, t, d, h), hj))
241	
242	law step_n:
243	  for +j: U32
244	  for +k: Nat
245	  for +to: U32
246	  for +d: Nat
247	  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
248	  for +hj4: {Nat.is_lt(U32.to_nat(j), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
249	  for +hn: {Nat.add(U32.to_nat(j), 1n+k) == U32.to_nat(to) : Nat}
250	  {Nat.add(U32.to_nat((j + 1 : U32)), k) == U32.to_nat(to) : Nat}
251	
252	def step_n(j, k, to, d, hd, hj4, hn):
253	  +tj = U32.to_nat(j)
254	  %Equal.sym(Nat, U32.to_nat((j + 1 : U32)), Nat.add(tj, 1n), C.inc_fits(j, d, hd, hj4)) :
255	    {Nat.add(_, k) == U32.to_nat(to) : Nat}
256	  %Equal.sym(Nat, Nat.add(Nat.add(tj, 1n), k), Nat.add(tj, Nat.add(1n, k)), N.add_assoc(tj, 1n, k)) :
257	    {_ == U32.to_nat(to) : Nat}
258	  hn
259	
260	# find
261	# ====
262	
263	# hit says byte j is c, r holds byte j + 1, j + n = to.
264	law fgo_view:
265	  for +n: Nat
266	  for +hit: Bool
267	  for +len: U32
268	  for +t: P.Tree<U32>
269	  for +d: Nat
270	  for +j: U32
271	  for +to: U32
272	  for +c: U32
273	  for +hh: {U32.is_eq(C.AT(len, t, j), c) == hit : Bool}
274	  for +hn: {Nat.add(U32.to_nat(j), n) == U32.to_nat(to) : Nat}
275	  for +hto: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
276	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
277	  {U32.to_nat(Pair.snd(D.Bytes, U32, B.find.go(n, hit, (C.BT(len, t), C.AT(len, t, (j + 1 : U32))), j, to, c))) == Nat.add(U32.to_nat(j), D.run_len(D.slice(D.view(C.BT(len, t)), U32.to_nat(j), n), c)) : Nat}
278	
279	def fgo_view(n, hit, len, t, d, j, to, c, hh, hn, hto, h):
280	  match n hit:
281	    case 0n _:
282	      +tj = U32.to_nat(j)
283	      %Equal.sym(List<&2, U32>, List.take(&2, U32, List.drop(&2, U32, D.view(C.BT(len, t)), tj), 0n), Nil{},
284	        Q.take_zero(List.drop(&2, U32, D.view(C.BT(len, t)), tj))) :
285	        {U32.to_nat(to) == Nat.add(tj, D.run_len(_, c)) : Nat}
286	      Equal.sym(Nat, Nat.add(tj, 0n), U32.to_nat(to), hn)
287	    case 1n+k True{}:
288	      +tj = U32.to_nat(j)
289	      +VW = D.view(C.BT(len, t))
290	      +x = C.AT(len, t, j)
291	      +S = D.slice(VW, Nat.add(tj, 1n), k)
292	      +hj = step_lt(len, j, to, k, hn, hto)
293	      %Equal.sym(List<&2, U32>, D.slice(VW, tj, 1n+k), x <> S, slice_cons(VW, tj, k, x, step_get(len, t, d, j, h, hj))) :
294	        {tj == Nat.add(tj, D.run_len(_, c)) : Nat}
295	      %Equal.sym(Bool, U32.is_eq(x, c), True{}, hh) :
296	        {tj == Nat.add(tj, Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(S, c)))) : Nat}
297	      Equal.sym(Nat, Nat.add(tj, 0n), tj, AB.add_zero(tj))
298	    case 1n+k False{}:
299	      +tj = U32.to_nat(j)
300	      +VW = D.view(C.BT(len, t))
301	      +x = C.AT(len, t, j)
302	      +S = D.slice(VW, Nat.add(tj, 1n), k)
303	      +j1 = (j + 1 : U32)
304	      +j11 = (j1 + 1 : U32)
305	      +H1 = U32.is_eq(C.AT(len, t, j1), c)
306	      +RHS = Nat.add(tj, D.run_len(D.slice(VW, tj, 1n+k), c))
307	      +hd = C.ok_d(len, t, d, h)
308	      +hj = step_lt(len, j, to, k, hn, hto)
309	      +hj4 = step_lt4(len, t, d, j, h, hj)
310	      %add11(j) : {U32.to_nat(Pair.snd(D.Bytes, U32, B.find.go(k, H1, B.at(C.BT(len, t), _), j1, to, c))) == RHS : Nat}
311	      %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j11), (C.BT(len, t), C.AT(len, t, j11)), C.at_pair_t(len, t, j11)) :
312	        {U32.to_nat(Pair.snd(D.Bytes, U32, B.find.go(k, H1, _, j1, to, c))) == RHS : Nat}
313	      +G = U32.to_nat(Pair.snd(D.Bytes, U32, B.find.go(k, H1, (C.BT(len, t), C.AT(len, t, j11)), j1, to, c)))
314	      %Equal.sym(List<&2, U32>, D.slice(VW, tj, 1n+k), x <> S, slice_cons(VW, tj, k, x, step_get(len, t, d, j, h, hj))) :
315	        {G == Nat.add(tj, D.run_len(_, c)) : Nat}
316	      %Equal.sym(Bool, U32.is_eq(x, c), False{}, hh) :
317	        {G == Nat.add(tj, Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(S, c)))) : Nat}
318	      %N.add_assoc(tj, 1n, D.run_len(S, c)) : {G == _ : Nat}
319	      %C.inc_fits(j, d, hd, hj4) : {G == Nat.add(_, D.run_len(D.slice(VW, _, k), c)) : Nat}
320	      fgo_view(k, H1, len, t, d, j1, to, c, {==}, step_n(j, k, to, d, hd, hj4, hn), hto, h)
321	
322	# from <= to as numbers.
323	law le_ft:
324	  for +from: U32
325	  for +to: U32
326	  for +hft: {U32.is_le(from, to) == True{} : Bool}
327	  {Nat.is_le(U32.to_nat(from), U32.to_nat(to)) == True{} : Bool}
328	
329	def le_ft(from, to, hft):
330	  Equal.trans(Bool, Nat.is_le(U32.to_nat(from), U32.to_nat(to)), U32.is_le(from, to), True{},
331	    Equal.sym(Bool, U32.is_le(from, to), Nat.is_le(U32.to_nat(from), U32.to_nat(to)), U.is_le_to_nat(from, to)), hft)
332	
333	law find_view_t:
334	  for +len: U32
335	  for +t: P.Tree<U32>
336	  for +d: Nat
337	  for +from: U32
338	  for +to: U32
339	  for +c: U32
340	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
341	  for +hft: {U32.is_le(from, to) == True{} : Bool}
342	  for +ht: {Nat.is_le(U32.to_nat(to), D.size(C.BT(len, t))) == True{} : Bool}
343	  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
344	  {U32.to_nat(Pair.snd(D.Bytes, U32, B.find(C.BT(len, t), from, to, c))) == D.first(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c) : Nat}
345	
346	def find_view_t(len, t, d, from, to, c, h, hft, ht, hc):
347	  +tf = U32.to_nat(from)
348	  +tt = U32.to_nat(to)
349	  +n = Nat.sub(tt, tf)
350	  +f1 = (from + 1 : U32)
351	  +H = U32.is_eq(C.AT(len, t, from), c)
352	  +RHS = D.first(D.view(C.BT(len, t)), tf, tt, c)
353	  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), from), (C.BT(len, t), C.AT(len, t, from)), C.at_pair_t(len, t, from)) :
354	    {U32.to_nat(Pair.snd(D.Bytes, U32, B.find.start(n, _, from, to, c))) == RHS : Nat}
355	  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), f1), (C.BT(len, t), C.AT(len, t, f1)), C.at_pair_t(len, t, f1)) :
356	    {U32.to_nat(Pair.snd(D.Bytes, U32, B.find.go(n, H, _, from, to, c))) == RHS : Nat}
357	  fgo_view(n, H, len, t, d, from, to, c, {==}, N.le_sub_add(tf, tt, le_ft(from, to, hft)), ht, h)
358	
359	# find2
360	# =====
361	
362	# hit says byte j is c1 or c2, r holds byte j + 1, j + n = to.
363	law fgo2_view:
364	  for +n: Nat
365	  for +hit: Bool
366	  for +len: U32
367	  for +t: P.Tree<U32>
368	  for +d: Nat
369	  for +j: U32
370	  for +to: U32
371	  for +c1: U32
372	  for +c2: U32
373	  for +hh: {(U32.is_eq(C.AT(len, t, j), c1) || U32.is_eq(C.AT(len, t, j), c2)) == hit : Bool}
374	  for +hn: {Nat.add(U32.to_nat(j), n) == U32.to_nat(to) : Nat}
375	  for +hto: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
376	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
377	  {U32.to_nat(Pair.snd(D.Bytes, U32, B.find2.go(n, hit, (C.BT(len, t), C.AT(len, t, (j + 1 : U32))), j, to, c1, c2))) == Nat.add(U32.to_nat(j), D.run_len2(D.slice(D.view(C.BT(len, t)), U32.to_nat(j), n), c1, c2)) : Nat}
378	
379	def fgo2_view(n, hit, len, t, d, j, to, c1, c2, hh, hn, hto, h):
380	  match n hit:
381	    case 0n _:
382	      +tj = U32.to_nat(j)
383	      %Equal.sym(List<&2, U32>, List.take(&2, U32, List.drop(&2, U32, D.view(C.BT(len, t)), tj), 0n), Nil{},
384	        Q.take_zero(List.drop(&2, U32, D.view(C.BT(len, t)), tj))) :
385	        {U32.to_nat(to) == Nat.add(tj, D.run_len2(_, c1, c2)) : Nat}
386	      Equal.sym(Nat, Nat.add(tj, 0n), U32.to_nat(to), hn)
387	    case 1n+k True{}:
388	      +tj = U32.to_nat(j)
389	      +VW = D.view(C.BT(len, t))
390	      +x = C.AT(len, t, j)
391	      +S = D.slice(VW, Nat.add(tj, 1n), k)
392	      +hj = step_lt(len, j, to, k, hn, hto)
393	      %Equal.sym(List<&2, U32>, D.slice(VW, tj, 1n+k), x <> S, slice_cons(VW, tj, k, x, step_get(len, t, d, j, h, hj))) :
394	        {tj == Nat.add(tj, D.run_len2(_, c1, c2)) : Nat}
395	      %Equal.sym(Bool, U32.is_eq(x, c1) || U32.is_eq(x, c2), True{}, hh) :
396	        {tj == Nat.add(tj, Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(S, c1, c2)))) : Nat}
397	      Equal.sym(Nat, Nat.add(tj, 0n), tj, AB.add_zero(tj))
398	    case 1n+k False{}:
399	      +tj = U32.to_nat(j)
400	      +VW = D.view(C.BT(len, t))
401	      +x = C.AT(len, t, j)
402	      +S = D.slice(VW, Nat.add(tj, 1n), k)
403	      +j1 = (j + 1 : U32)
404	      +j11 = (j1 + 1 : U32)
405	      +H1 = U32.is_eq(C.AT(len, t, j1), c1) || U32.is_eq(C.AT(len, t, j1), c2)
406	      +RHS = Nat.add(tj, D.run_len2(D.slice(VW, tj, 1n+k), c1, c2))
407	      +hd = C.ok_d(len, t, d, h)
408	      +hj = step_lt(len, j, to, k, hn, hto)
409	      +hj4 = step_lt4(len, t, d, j, h, hj)
410	      %add11(j) : {U32.to_nat(Pair.snd(D.Bytes, U32, B.find2.go(k, H1, B.at(C.BT(len, t), _), j1, to, c1, c2))) == RHS : Nat}
411	      %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j11), (C.BT(len, t), C.AT(len, t, j11)), C.at_pair_t(len, t, j11)) :
412	        {U32.to_nat(Pair.snd(D.Bytes, U32, B.find2.go(k, H1, _, j1, to, c1, c2))) == RHS : Nat}
413	      +G = U32.to_nat(Pair.snd(D.Bytes, U32, B.find2.go(k, H1, (C.BT(len, t), C.AT(len, t, j11)), j1, to, c1, c2)))
414	      %Equal.sym(List<&2, U32>, D.slice(VW, tj, 1n+k), x <> S, slice_cons(VW, tj, k, x, step_get(len, t, d, j, h, hj))) :
415	        {G == Nat.add(tj, D.run_len2(_, c1, c2)) : Nat}
416	      %Equal.sym(Bool, U32.is_eq(x, c1) || U32.is_eq(x, c2), False{}, hh) :
417	        {G == Nat.add(tj, Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(S, c1, c2)))) : Nat}
418	      %N.add_assoc(tj, 1n, D.run_len2(S, c1, c2)) : {G == _ : Nat}
419	      %C.inc_fits(j, d, hd, hj4) : {G == Nat.add(_, D.run_len2(D.slice(VW, _, k), c1, c2)) : Nat}
420	      fgo2_view(k, H1, len, t, d, j1, to, c1, c2, {==}, step_n(j, k, to, d, hd, hj4, hn), hto, h)
421	
422	law find2_view_t:
423	  for +len: U32
424	  for +t: P.Tree<U32>
425	  for +d: Nat
426	  for +from: U32
427	  for +to: U32
428	  for +c1: U32
429	  for +c2: U32
430	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
431	  for +hft: {U32.is_le(from, to) == True{} : Bool}
432	  for +ht: {Nat.is_le(U32.to_nat(to), D.size(C.BT(len, t))) == True{} : Bool}
433	  for +hc1: {U32.is_lt(c1, 256) == True{} : Bool}
434	  for +hc2: {U32.is_lt(c2, 256) == True{} : Bool}
435	  {U32.to_nat(Pair.snd(D.Bytes, U32, B.find2(C.BT(len, t), from, to, c1, c2))) == D.first2(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c1, c2) : Nat}
436	
437	def find2_view_t(len, t, d, from, to, c1, c2, h, hft, ht, hc1, hc2):
438	  +tf = U32.to_nat(from)
439	  +tt = U32.to_nat(to)
440	  +n = Nat.sub(tt, tf)
441	  +f1 = (from + 1 : U32)
442	  +H = U32.is_eq(C.AT(len, t, from), c1) || U32.is_eq(C.AT(len, t, from), c2)
443	  +RHS = D.first2(D.view(C.BT(len, t)), tf, tt, c1, c2)
444	  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), from), (C.BT(len, t), C.AT(len, t, from)), C.at_pair_t(len, t, from)) :
445	    {U32.to_nat(Pair.snd(D.Bytes, U32, B.find2.start(n, _, from, to, c1, c2))) == RHS : Nat}
446	  %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), f1), (C.BT(len, t), C.AT(len, t, f1)), C.at_pair_t(len, t, f1)) :
447	    {U32.to_nat(Pair.snd(D.Bytes, U32, B.find2.go(n, H, _, from, to, c1, c2))) == RHS : Nat}
448	  fgo2_view(n, H, len, t, d, from, to, c1, c2, {==}, N.le_sub_add(tf, tt, le_ft(from, to, hft)), ht, h)