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_find.bend as F
8	import ./proof_append.bend as X
9	import ./proof_shift.bend as H
10	import ./proof_fast_word.bend as FW
11	import lawful-words@0.1.0.0/defs.bend as W
12	import lawful-words@0.1.0.0/proof_nat.bend as N
13	import lawful-words@0.1.0.0/proof_u32.bend as U
14	import lawful-arrays@0.1.0.0/proof_base.bend as AB
15	import lawful-arrays@0.1.0.0/proof_tree.bend as P
16	import lawful-arrays@0.1.0.0/defs.bend as A
17	
18	# fast.bend's find on the mirror C.BT(len, t). FG is find.go as a function of
19	# the tree (fg_eq): the word loop answers the offset of the first flagged byte,
20	# or 4294967295; find.fin takes the min with to. The word facts (what the
21	# flags and bidx say) are in proof_fast_word.bend.
22	
23	def FG(n: Nat, z: Bool, +wi: U32, +m: U32, +rc: U32, +t: P.Tree<U32>) -> U32:
24	  match n z:
25	    case 0n _:
26	      4294967295
27	    case 1n+k True{}:
28	      +m2 = FA.zb((C.WD(t, (wi + 1 : U32)) .^. rc : U32))
29	      FG(k, U32.is_zero(m2), (wi + 1 : U32), m2, rc, t)
30	    case 1n+k False{}:
31	      ((wi << 2n : U32) + FA.bidx(m) : U32)
32	
33	law fg_eq:
34	  for +n: Nat
35	  for +z: Bool
36	  for +wi: U32
37	  for +m: U32
38	  for +rc: U32
39	  for +t: P.Tree<U32>
40	  {FA.find.go(n, z, Array.get(U32, P.fromT(U32, t), (wi + 1 : U32)), wi, m, rc) == (P.fromT(U32, t), FG(n, z, wi, m, rc, t)) : Array<U32> & U32}
41	
42	def fg_eq(n, z, wi, m, rc, t):
43	  match n z:
44	    case 0n _:
45	      %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), (wi + 1 : U32)), (P.fromT(U32, t), C.WD(t, (wi + 1 : U32))), P.get_pair_t(U32, t, (wi + 1 : U32))) :
46	        {FA.find.go(0n, z, _, wi, m, rc) == (P.fromT(U32, t), FG(0n, z, wi, m, rc, t)) : Array<U32> & U32}
47	      {==}
48	    case 1n+k True{}:
49	      +m2 = FA.zb((C.WD(t, (wi + 1 : U32)) .^. rc : U32))
50	      %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), (wi + 1 : U32)), (P.fromT(U32, t), C.WD(t, (wi + 1 : U32))), P.get_pair_t(U32, t, (wi + 1 : U32))) :
51	        {FA.find.go(1n+k, True{}, _, wi, m, rc) == (P.fromT(U32, t), FG(1n+k, True{}, wi, m, rc, t)) : Array<U32> & U32}
52	      %F.add11(wi) :
53	        {FA.find.go(k, U32.is_zero(m2), Array.get(U32, P.fromT(U32, t), _), (wi + 1 : U32), m2, rc) == (P.fromT(U32, t), FG(k, U32.is_zero(m2), (wi + 1 : U32), m2, rc, t)) : Array<U32> & U32}
54	      fg_eq(k, U32.is_zero(m2), (wi + 1 : U32), m2, rc, t)
55	    case 1n+k False{}:
56	      %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), (wi + 1 : U32)), (P.fromT(U32, t), C.WD(t, (wi + 1 : U32))), P.get_pair_t(U32, t, (wi + 1 : U32))) :
57	        {FA.find.go(1n+k, False{}, _, wi, m, rc) == (P.fromT(U32, t), FG(1n+k, False{}, wi, m, rc, t)) : Array<U32> & U32}
58	      {==}
59	
60	# The mask of the first word.
61	def M0(+t: P.Tree<U32>, +from: U32, +rc: U32) -> U32:
62	  FA.zb(((C.WD(t, (from >> 2n : U32)) .^. rc : U32) .|. U32.not(FA.low(from)) : U32))
63	
64	# fast find on the mirror: the same Bytes, and the min of the loop's answer with to.
65	law fast_eq:
66	  for +len: U32
67	  for +t: P.Tree<U32>
68	  for +from: U32
69	  for +to: U32
70	  for +c: U32
71	  {FA.find(C.BT(len, t), from, to, c) == (C.BT(len, t), U32.min(FG(FA.words(from, to), U32.is_zero(M0(t, from, FA.rep(c))), (from >> 2n : U32), M0(t, from, FA.rep(c)), FA.rep(c), t), to)) : D.Bytes & U32}
72	
73	def fast_eq(len, t, from, to, c):
74	  +k = (from >> 2n : U32)
75	  +rc = FA.rep(c)
76	  +n = FA.words(from, to)
77	  %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), k), (P.fromT(U32, t), C.WD(t, k)), P.get_pair_t(U32, t, k)) :
78	    {FA.find.k(len, FA.find.fin(to, FA.find.start(n, _, from, rc))) == (C.BT(len, t), U32.min(FG(n, U32.is_zero(M0(t, from, rc)), k, M0(t, from, rc), rc, t), to)) : D.Bytes & U32}
79	  %Equal.sym(Array<U32> & U32, FA.find.go(n, U32.is_zero(M0(t, from, rc)), Array.get(U32, P.fromT(U32, t), (k + 1 : U32)), k, M0(t, from, rc), rc),
80	    (P.fromT(U32, t), FG(n, U32.is_zero(M0(t, from, rc)), k, M0(t, from, rc), rc, t)), fg_eq(n, U32.is_zero(M0(t, from, rc)), k, M0(t, from, rc), rc, t)) :
81	    {FA.find.k(len, FA.find.fin(to, _)) == (C.BT(len, t), U32.min(FG(n, U32.is_zero(M0(t, from, rc)), k, M0(t, from, rc), rc, t), to)) : D.Bytes & U32}
82	  {==}
83	
84	# Lists
85	# =====
86	
87	law drop_append_l:
88	  for +xs: List<&2, U32>
89	  for +ys: List<&2, U32>
90	  for +o: Nat
91	  for +h: {Nat.is_le(o, List.length(&2, U32, xs)) == True{} : Bool}
92	  {List.drop(&2, U32, List.append(&2, U32, xs, ys), o) == List.append(&2, U32, List.drop(&2, U32, xs, o), ys) : List<&2, U32>}
93	
94	def drop_append_l(xs, ys, o, h):
95	  match xs o:
96	    case Nil{} 0n:
97	      X.drop_zero(ys)
98	    case Nil{} 1n+p:
99	      Empty.absurd({List.drop(&2, U32, ys, 1n+p) == ys : List<&2, U32>}, AB.false_ne_true(h))
100	    case Con{x, t} 0n:
101	      {==}
102	    case Con{x, t} 1n+p:
103	      drop_append_l(t, ys, p, h)
104	
105	law drop_unpack:
106	  for +ws: List<&2, U32>
107	  for +q: Nat
108	  {List.drop(&2, U32, D.unpack(ws), Nat.mul(q, 4n)) == D.unpack(List.drop(&2, U32, ws, q)) : List<&2, U32>}
109	
110	def drop_unpack(ws, q):
111	  match ws q:
112	    case Nil{} _:
113	      {==}
114	    case Con{x, t} 0n:
115	      X.drop_zero(D.unpack(Con{x, t}))
116	    case Con{x, t} 1n+p:
117	      drop_unpack(t, p)
118	
119	# Byte 4q + o onwards: the rest of word q, then the words after it.
120	law drop_word:
121	  for +ws: List<&2, U32>
122	  for +q: Nat
123	  for +o: Nat
124	  for +w: U32
125	  for +hw: {List.get(&2, U32, ws, q) == Some{w} : Maybe<&2, U32>}
126	  for +ho: {Nat.is_le(o, 4n) == True{} : Bool}
127	  {List.drop(&2, U32, D.unpack(ws), Nat.add(Nat.mul(q, 4n), o)) == List.append(&2, U32, List.drop(&2, U32, C.L4(w), o), D.unpack(List.drop(&2, U32, ws, Nat.add(q, 1n)))) : List<&2, U32>}
128	
129	def drop_word(ws, q, o, w, hw, ho):
130	  match ws q:
131	    case Nil{} _:
132	      Empty.absurd({List.drop(&2, U32, D.unpack(Nil{}), Nat.add(Nat.mul(q, 4n), o)) == List.append(&2, U32, List.drop(&2, U32, C.L4(w), o), D.unpack(List.drop(&2, U32, Nil{}, Nat.add(q, 1n)))) : List<&2, U32>},
133	        X.none_some(w, hw))
134	    case Con{+x, t} 0n:
135	      %X.some_inj(x, w, hw) :
136	        {List.drop(&2, U32, List.append(&2, U32, C.L4(x), D.unpack(t)), o) == List.append(&2, U32, List.drop(&2, U32, C.L4(_), o), D.unpack(List.drop(&2, U32, t, 0n))) : List<&2, U32>}
137	      %Equal.sym(List<&2, U32>, List.drop(&2, U32, t, 0n), t, X.drop_zero(t)) :
138	        {List.drop(&2, U32, List.append(&2, U32, C.L4(x), D.unpack(t)), o) == List.append(&2, U32, List.drop(&2, U32, C.L4(x), o), D.unpack(_)) : List<&2, U32>}
139	      drop_append_l(C.L4(x), D.unpack(t), o, ho)
140	    case Con{x, t} 1n+p:
141	      drop_word(t, p, o, w, hw, ho)
142	
143	# Whether the head of a list is c.
144	def hd_eq(xs: List<&2, U32>, +c: U32) -> Bool:
145	  match xs:
146	    case Nil{}:
147	      False{}
148	    case Con{x, t}:
149	      U32.is_eq(x, c)
150	
151	# A hit inside xs: the first c of take(xs ++ ys, n) is at min(run, n).
152	law run_hit:
153	  for +xs: List<&2, U32>
154	  for +ys: List<&2, U32>
155	  for +n: Nat
156	  for +c: U32
157	  for +b: Bool
158	  for +hb: {hd_eq(xs, c) == b : Bool}
159	  for +h: {Nat.is_lt(D.run_len(xs, c), List.length(&2, U32, xs)) == True{} : Bool}
160	  {D.run_len(List.take(&2, U32, List.append(&2, U32, xs, ys), n), c) == Nat.min(D.run_len(xs, c), n) : Nat}
161	
162	def run_hit(xs, ys, n, c, b, hb, h):
163	  match xs n b:
164	    case Nil{} _ _:
165	      Empty.absurd({D.run_len(List.take(&2, U32, ys, n), c) == Nat.min(0n, n) : Nat}, AB.lt_zero_absurd(0n, h))
166	    case Con{x, t} 0n True{}:
167	      %Equal.sym(Bool, hd_eq(x <> t, c), True{}, hb) : {0n == Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c))), 0n) : Nat}
168	      {==}
169	    case Con{x, t} 0n False{}:
170	      %Equal.sym(Bool, hd_eq(x <> t, c), False{}, hb) : {0n == Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c))), 0n) : Nat}
171	      {==}
172	    case Con{x, t} 1n+p True{}:
173	      %Equal.sym(Bool, hd_eq(x <> t, c), True{}, hb) :
174	        {Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(List.take(&2, U32, List.append(&2, U32, t, ys), p), c))) == Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c))), 1n+p) : Nat}
175	      {==}
176	    case Con{x, t} 1n+p False{}:
177	      %Equal.sym(Bool, hd_eq(x <> t, c), False{}, hb) :
178	        {Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(List.take(&2, U32, List.append(&2, U32, t, ys), p), c))) == Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c))), 1n+p) : Nat}
179	      +h2 = AB.subst(Bool, y => {Nat.is_lt(Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len(t, c))), 1n+List.length(&2, U32, t)) == True{} : Bool},
180	        hd_eq(x <> t, c), False{}, hb, h)
181	      %run_hit(t, ys, p, c, hd_eq(t, c), {==}, h2) :
182	        {1n+D.run_len(List.take(&2, U32, List.append(&2, U32, t, ys), p), c) == 1n+_ : Nat}
183	      {==}
184	
185	# No c in xs, and n reaches past it: the search goes on in ys.
186	law run_skip:
187	  for +xs: List<&2, U32>
188	  for +ys: List<&2, U32>
189	  for +n: Nat
190	  for +c: U32
191	  for +b: Bool
192	  for +hb: {hd_eq(xs, c) == b : Bool}
193	  for +h: {D.run_len(xs, c) == List.length(&2, U32, xs) : Nat}
194	  for +hn: {Nat.is_le(List.length(&2, U32, xs), n) == True{} : Bool}
195	  {D.run_len(List.take(&2, U32, List.append(&2, U32, xs, ys), n), c) == Nat.add(List.length(&2, U32, xs), D.run_len(List.take(&2, U32, ys, Nat.sub(n, List.length(&2, U32, xs))), c)) : Nat}
196	
197	def run_skip(xs, ys, n, c, b, hb, h, hn):
198	  match xs n b:
199	    case Nil{} _ _:
200	      %Equal.sym(Nat, Nat.sub(n, 0n), n, N.sub_zero(n)) :
201	        {D.run_len(List.take(&2, U32, ys, n), c) == D.run_len(List.take(&2, U32, ys, _), c) : Nat}
202	      {==}
203	    case Con{x, t} _ True{}:
204	      Empty.absurd({D.run_len(List.take(&2, U32, List.append(&2, U32, x <> t, ys), n), c) == Nat.add(1n+List.length(&2, U32, t), D.run_len(List.take(&2, U32, ys, Nat.sub(n, 1n+List.length(&2, U32, t))), c)) : Nat},
205	        N.zero_ne_succ(List.length(&2, U32, t), AB.subst(Bool, y => {Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len(t, c))) == 1n+List.length(&2, U32, t) : Nat},
206	          hd_eq(x <> t, c), True{}, hb, h)))
207	    case Con{x, t} 0n False{}:
208	      Empty.absurd({0n == Nat.add(1n+List.length(&2, U32, t), D.run_len(List.take(&2, U32, ys, Nat.sub(0n, 1n+List.length(&2, U32, t))), c)) : Nat},
209	        AB.false_ne_true(hn))
210	    case Con{x, t} 1n+p False{}:
211	      %Equal.sym(Bool, hd_eq(x <> t, c), False{}, hb) :
212	        {Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(List.take(&2, U32, List.append(&2, U32, t, ys), p), c))) == 1n+Nat.add(List.length(&2, U32, t), D.run_len(List.take(&2, U32, ys, Nat.sub(p, List.length(&2, U32, t))), c)) : Nat}
213	      +h2 = N.succ_inj(D.run_len(t, c), List.length(&2, U32, t),
214	        AB.subst(Bool, y => {Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len(t, c))) == 1n+List.length(&2, U32, t) : Nat}, hd_eq(x <> t, c), False{}, hb, h))
215	      %run_skip(t, ys, p, c, hd_eq(t, c), {==}, h2, hn) :
216	        {1n+D.run_len(List.take(&2, U32, List.append(&2, U32, t, ys), p), c) == 1n+_ : Nat}
217	      {==}
218	
219	# No c in xs, and n stays within it.
220	law run_none:
221	  for +xs: List<&2, U32>
222	  for +ys: List<&2, U32>
223	  for +n: Nat
224	  for +c: U32
225	  for +b: Bool
226	  for +hb: {hd_eq(xs, c) == b : Bool}
227	  for +h: {D.run_len(xs, c) == List.length(&2, U32, xs) : Nat}
228	  for +hn: {Nat.is_le(n, List.length(&2, U32, xs)) == True{} : Bool}
229	  {D.run_len(List.take(&2, U32, List.append(&2, U32, xs, ys), n), c) == n : Nat}
230	
231	def run_none(xs, ys, n, c, b, hb, h, hn):
232	  match xs n b:
233	    case Nil{} 0n _:
234	      %Equal.sym(List<&2, U32>, List.take(&2, U32, ys, 0n), Nil{}, Q.take_zero(ys)) : {D.run_len(_, c) == 0n : Nat}
235	      {==}
236	    case Nil{} 1n+p _:
237	      Empty.absurd({D.run_len(List.take(&2, U32, ys, 1n+p), c) == 1n+p : Nat}, AB.false_ne_true(hn))
238	    case Con{x, t} 0n _:
239	      {==}
240	    case Con{x, t} 1n+p True{}:
241	      Empty.absurd({D.run_len(List.take(&2, U32, List.append(&2, U32, x <> t, ys), 1n+p), c) == 1n+p : Nat},
242	        N.zero_ne_succ(List.length(&2, U32, t), AB.subst(Bool, y => {Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len(t, c))) == 1n+List.length(&2, U32, t) : Nat},
243	          hd_eq(x <> t, c), True{}, hb, h)))
244	    case Con{x, t} 1n+p False{}:
245	      %Equal.sym(Bool, hd_eq(x <> t, c), False{}, hb) :
246	        {Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(List.take(&2, U32, List.append(&2, U32, t, ys), p), c))) == 1n+p : Nat}
247	      +h2 = N.succ_inj(D.run_len(t, c), List.length(&2, U32, t),
248	        AB.subst(Bool, y => {Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len(t, c))) == 1n+List.length(&2, U32, t) : Nat}, hd_eq(x <> t, c), False{}, hb, h))
249	      %run_none(t, ys, p, c, hd_eq(t, c), {==}, h2, hn) : {1n+D.run_len(List.take(&2, U32, List.append(&2, U32, t, ys), p), c) == 1n+_ : Nat}
250	      {==}
251	
252	law run_le:
253	  for +xs: List<&2, U32>
254	  for +c: U32
255	  for +b: Bool
256	  for +hb: {hd_eq(xs, c) == b : Bool}
257	  {Nat.is_le(D.run_len(xs, c), List.length(&2, U32, xs)) == True{} : Bool}
258	
259	def run_le(xs, c, b, hb):
260	  match xs b:
261	    case Nil{} _:
262	      {==}
263	    case Con{x, t} True{}:
264	      %Equal.sym(Bool, hd_eq(x <> t, c), True{}, hb) :
265	        {Nat.is_le(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c))), 1n+List.length(&2, U32, t)) == True{} : Bool}
266	      {==}
267	    case Con{x, t} False{}:
268	      %Equal.sym(Bool, hd_eq(x <> t, c), False{}, hb) :
269	        {Nat.is_le(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c))), 1n+List.length(&2, U32, t)) == True{} : Bool}
270	      run_le(t, c, hd_eq(t, c), {==})
271	
272	# Nat
273	# ===
274	
275	law min_shift:
276	  for +s: Nat
277	  for +r: Nat
278	  for +tt: Nat
279	  for +h: {Nat.is_le(s, tt) == True{} : Bool}
280	  {Nat.min(Nat.add(s, r), tt) == Nat.add(s, Nat.min(r, Nat.sub(tt, s))) : Nat}
281	
282	def min_shift(s, r, tt, h):
283	  match s tt:
284	    case 0n 0n:
285	      {==}
286	    case 0n 1n+q:
287	      {==}
288	    case 1n+p 0n:
289	      Empty.absurd({Nat.min(1n+Nat.add(p, r), 0n) == 1n+Nat.add(p, Nat.min(r, 0n)) : Nat}, AB.false_ne_true(h))
290	    case 1n+p 1n+q:
291	      %min_shift(p, r, q, h) : {1n+Nat.min(Nat.add(p, r), q) == 1n+_ : Nat}
292	      {==}
293	
294	law le_cancel:
295	  for +a: Nat
296	  for +x: Nat
297	  for +y: Nat
298	  for +h: {Nat.is_le(Nat.add(a, x), Nat.add(a, y)) == True{} : Bool}
299	  {Nat.is_le(x, y) == True{} : Bool}
300	
301	def le_cancel(a, x, y, h):
302	  match a:
303	    case 0n:
304	      h
305	    case 1n+p:
306	      le_cancel(p, x, y, h)
307	
308	law lt_cancel:
309	  for +a: Nat
310	  for +x: Nat
311	  for +y: Nat
312	  for +h: {Nat.is_lt(Nat.add(a, x), Nat.add(a, y)) == True{} : Bool}
313	  {Nat.is_lt(x, y) == True{} : Bool}
314	
315	def lt_cancel(a, x, y, h):
316	  match a:
317	    case 0n:
318	      h
319	    case 1n+p:
320	      lt_cancel(p, x, y, h)
321	
322	law sub_sub:
323	  for +tt: Nat
324	  for +s: Nat
325	  for +l: Nat
326	  {Nat.sub(Nat.sub(tt, s), l) == Nat.sub(tt, Nat.add(s, l)) : Nat}
327	
328	def sub_sub(tt, s, l):
329	  match tt s:
330	    case 0n _:
331	      match l:
332	        case 0n:
333	          {==}
334	        case 1n+q:
335	          {==}
336	    case 1n+p 0n:
337	      {==}
338	    case 1n+p 1n+q:
339	      sub_sub(p, q, l)
340	
341	law mul4s:
342	  for +w: Nat
343	  {Nat.mul(Nat.add(w, 1n), 4n) == Nat.add(Nat.mul(w, 4n), 4n) : Nat}
344	
345	def mul4s(w):
346	  match w:
347	    case 0n:
348	      {==}
349	    case 1n+p:
350	      %mul4s(p) : {Nat.add(4n, Nat.mul(Nat.add(p, 1n), 4n)) == Nat.add(4n, _) : Nat}
351	      {==}
352	
353	# Word index bounds: the words searched lie inside the block.
354	law wlt:
355	  for +w: Nat
356	  for +k: Nat
357	  for +tt: Nat
358	  for +ll: Nat
359	  for +pp: Nat
360	  for +h1: {Nat.is_lt(Nat.mul(Nat.add(w, k), 4n), tt) == True{} : Bool}
361	  for +h2: {Nat.is_le(tt, ll) == True{} : Bool}
362	  for +h3: {Nat.is_le(ll, Nat.mul(4n, pp)) == True{} : Bool}
363	  {Nat.is_lt(w, pp) == True{} : Bool}
364	
365	def wlt(w, k, tt, ll, pp, h1, h2, h3):
366	  +a = N.le_lt_trans(Nat.mul(w, 4n), Nat.mul(Nat.add(w, k), 4n), Nat.mul(4n, pp), N.le_mul_r(w, Nat.add(w, k), 4n, N.le_add_r(w, k)),
367	    N.lt_le_trans(Nat.mul(Nat.add(w, k), 4n), tt, Nat.mul(4n, pp), h1, N.le_trans(tt, ll, Nat.mul(4n, pp), h2, h3)))
368	  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), a))
369	
370	law wb4:
371	  for +w: Nat
372	  for +pp: Nat
373	  for +h: {Nat.is_lt(w, pp) == True{} : Bool}
374	  {Nat.is_le(Nat.add(Nat.mul(w, 4n), 4n), Nat.mul(4n, pp)) == True{} : Bool}
375	
376	def wb4(w, pp, h):
377	  +a = N.le_mul_r(1n+w, pp, 4n, Equal.trans(Bool, Nat.is_le(1n+w, pp), Nat.is_lt(w, pp), True{}, N.le_succ_lt(w, pp), h))
378	  %Equal.sym(Nat, Nat.add(Nat.mul(w, 4n), 4n), Nat.add(4n, Nat.mul(w, 4n)), N.add_comm(Nat.mul(w, 4n), 4n)) : {Nat.is_le(_, Nat.mul(4n, pp)) == True{} : Bool}
379	  %Equal.sym(Nat, Nat.mul(4n, pp), Nat.mul(pp, 4n), N.mul_comm(4n, pp)) : {Nat.is_le(Nat.add(4n, Nat.mul(w, 4n)), _) == True{} : Bool}
380	  a
381	
382	# The loop's "no hit" answer 4294967295 is above every length.
383	law not0:
384	  {U32.not(0) == 4294967295 : U32}
385	
386	def not0():
387	  {==}
388	
389	law min_r:
390	  for +a: U32
391	  for +b: U32
392	  for +h: {U32.is_lt(a, b) == False{} : Bool}
393	  {U32.min(a, b) == b : U32}
394	
395	def min_r(a, b, h):
396	  match a b:
397	    case U32{x} U32{y}:
398	      %Equal.sym(Bool, U32.is_lt(U32{x}, U32{y}), False{}, h) : {Bool.pick(U32, _, U32{x}, U32{y}) == U32{y} : U32}
399	      {==}
400	
401	def gtop.go(+tt: Nat, +m: Nat, +ht: {Nat.is_lt(tt, m) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(Nat.sub(m, 1n), 0n), tt) == False{} : Bool}:
402	  match m:
403	    case 0n:
404	      Empty.absurd({Nat.is_lt(0n, tt) == False{} : Bool}, AB.lt_zero_absurd(tt, ht))
405	    case 1n+p:
406	      %Equal.sym(Nat, Nat.sub(Nat.sub(p, 0n), 0n), Nat.sub(p, 0n), N.sub_zero(Nat.sub(p, 0n))) : {Nat.is_lt(_, tt) == False{} : Bool}
407	      %Equal.sym(Nat, Nat.sub(p, 0n), p, N.sub_zero(p)) : {Nat.is_lt(_, tt) == False{} : Bool}
408	      N.le_not_lt(tt, p, Equal.trans(Bool, Nat.is_le(tt, p), Nat.is_lt(tt, 1n+p), True{}, Equal.sym(Bool, Nat.is_lt(tt, 1n+p), Nat.is_le(tt, p), N.lt_succ_iff(tt, p)), ht))
409	
410	# With the bound m abstract (m stands for 2^32).
411	law gtop:
412	  for +x: Nat
413	  for +tt: Nat
414	  for +m: Nat
415	  for +hx: {x == Nat.sub(Nat.sub(m, 1n), U32.to_nat(0)) : Nat}
416	  for +ht: {Nat.is_lt(tt, m) == True{} : Bool}
417	  {Nat.is_lt(x, tt) == False{} : Bool}
418	
419	def gtop(x, tt, m, hx, ht):
420	  %Equal.sym(Nat, x, Nat.sub(Nat.sub(m, 1n), U32.to_nat(0)), hx) : {Nat.is_lt(_, tt) == False{} : Bool}
421	  gtop.go(tt, m, ht)
422	
423	
424	law top_nat:
425	  {U32.to_nat(4294967295) == Nat.sub(Nat.sub(Nat.pow(2n, 32n), 1n), U32.to_nat(0)) : Nat}
426	
427	def top_nat():
428	  %not0() : {U32.to_nat(_) == Nat.sub(Nat.sub(Nat.pow(2n, 32n), 1n), U32.to_nat(0)) : Nat}
429	  U.to_nat_not_p(0)
430	
431	law is_lt_top:
432	  for +to: U32
433	  for +d: Nat
434	  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
435	  for +ht: {Nat.is_le(U32.to_nat(to), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
436	  {U32.is_lt(4294967295, to) == False{} : Bool}
437	
438	def is_lt_top(to, d, hd, ht):
439	  %Equal.sym(Bool, U32.is_lt(4294967295, to), Nat.is_lt(U32.to_nat(4294967295), U32.to_nat(to)), U.is_lt_to_nat(4294967295, to)) :
440	    {_ == False{} : Bool}
441	  gtop(U32.to_nat(4294967295), U32.to_nat(to), Nat.pow(2n, 32n), top_nat(), C.fits_e(U32.to_nat(to), d, 32n, C.he32(d, hd), ht))
442	
443	law min_top:
444	  for +to: U32
445	  for +d: Nat
446	  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
447	  for +ht: {Nat.is_le(U32.to_nat(to), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
448	  {U32.min(4294967295, to) == to : U32}
449	
450	def min_top(to, d, hd, ht):
451	  min_r(4294967295, to, is_lt_top(to, d, hd, ht))
452	
453	# The word loop
454	# =============
455	
456	# All the block's bytes, the start of a search inside word wi (o bytes in),
457	# the rest of that word, and the bytes from the next word on.
458	def UB(+t: P.Tree<U32>) -> List<&2, U32>:
459	  D.unpack(C.WL(t))
460	
461	def SS(+wi: U32, +o: Nat) -> Nat:
462	  Nat.add(Nat.mul(U32.to_nat(wi), 4n), o)
463	
464	def AW(+t: P.Tree<U32>, +wi: U32, +o: Nat) -> List<&2, U32>:
465	  List.drop(&2, U32, C.L4(C.WD(t, wi)), o)
466	
467	def BW(+t: P.Tree<U32>, +wi: U32) -> List<&2, U32>:
468	  List.drop(&2, U32, UB(t), Nat.mul(Nat.add(U32.to_nat(wi), 1n), 4n))
469	
470	law shl2:
471	  for +wi: U32
472	  for +d: Nat
473	  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
474	  for +hx: {Nat.is_le(Nat.mul(U32.to_nat(wi), 4n), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
475	  {U32.to_nat((wi << 2n : U32)) == Nat.mul(U32.to_nat(wi), 4n) : Nat}
476	
477	def shl2(wi, d, hd, hx):
478	  U.to_nat_shln_fits_p(wi, 2n, C.fits_e(Nat.mul(U32.to_nat(wi), Nat.pow(2n, 2n)), d, 32n, C.he32(d, hd), hx))
479	
480	law dw:
481	  for +t: P.Tree<U32>
482	  for +d: Nat
483	  for +wi: U32
484	  for +o: Nat
485	  for +hf: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool}
486	  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
487	  for +hk: {Nat.is_lt(U32.to_nat(wi), Nat.pow(2n, d)) == True{} : Bool}
488	  for +ho: {Nat.is_le(o, 4n) == True{} : Bool}
489	  {List.drop(&2, U32, UB(t), SS(wi, o)) == List.append(&2, U32, AW(t, wi, o), BW(t, wi)) : List<&2, U32>}
490	
491	def dw(t, d, wi, o, hf, hd, hk, ho):
492	  %Equal.sym(List<&2, U32>, List.drop(&2, U32, UB(t), Nat.mul(Nat.add(U32.to_nat(wi), 1n), 4n)), D.unpack(List.drop(&2, U32, C.WL(t), Nat.add(U32.to_nat(wi), 1n))),
493	    drop_unpack(C.WL(t), Nat.add(U32.to_nat(wi), 1n))) :
494	    {List.drop(&2, U32, UB(t), SS(wi, o)) == List.append(&2, U32, AW(t, wi, o), _) : List<&2, U32>}
495	  drop_word(C.WL(t), U32.to_nat(wi), o, C.WD(t, wi), C.wd_get(t, d, wi, hf, hd, hk), ho)
496	
497	law awl:
498	  for +t: P.Tree<U32>
499	  for +wi: U32
500	  for +o: Nat
501	  {List.length(&2, U32, AW(t, wi, o)) == Nat.sub(4n, o) : Nat}
502	
503	def awl(t, wi, o):
504	  H.drop_length(C.L4(C.WD(t, wi)), o)
505	
506	# The flagged word: the answer is the first c from the start, or to.
507	law fhit:
508	  for +len: U32
509	  for +t: P.Tree<U32>
510	  for +d: Nat
511	  for +to: U32
512	  for +c: U32
513	  for +wi: U32
514	  for +o: Nat
515	  for +v: U32
516	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
517	  for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
518	  for +ho: {Nat.is_lt(o, 4n) == True{} : Bool}
519	  for +hs: {Nat.is_le(SS(wi, o), U32.to_nat(to)) == True{} : Bool}
520	  for +hk: {Nat.is_lt(U32.to_nat(wi), Nat.pow(2n, d)) == True{} : Bool}
521	  for +hv: {FW.P0(v) == Nat.add(o, D.run_len(AW(t, wi, o), c)) : Nat}
522	  for +hz: {U32.is_zero(FA.zb(v)) == False{} : Bool}
523	  {U32.to_nat(U32.min(((wi << 2n : U32) + FA.bidx(FA.zb(v)) : U32), to)) == D.first(UB(t), SS(wi, o), U32.to_nat(to), c) : Nat}
524	
525	def fhit(len, t, d, to, c, wi, o, v, h, ht, ho, hs, hk, hv, hz):
526	  +W = U32.to_nat(wi)
527	  +T = U32.to_nat(to)
528	  +r = D.run_len(AW(t, wi, o), c)
529	  +M4 = Nat.mul(4n, Nat.pow(2n, d))
530	  +hd = C.ok_d(len, t, d, h)
531	  +hf = C.ok_full(len, t, d, h)
532	  +hp4 = run_le(C.L4(v), 0, hd_eq(C.L4(v), 0), {==})
533	  +hne = Equal.trans(Bool, Nat.is_eq(FW.P0(v), 4n), U32.is_zero(FA.zb(v)), False{}, Equal.sym(Bool, U32.is_zero(FA.zb(v)), Nat.is_eq(FW.P0(v), 4n), FW.zb_none(v)), hz)
534	  +hlt = Equal.trans(Bool, Nat.is_lt(FW.P0(v), 4n), Nat.is_le(1n+FW.P0(v), 4n), True{}, Equal.sym(Bool, Nat.is_le(1n+FW.P0(v), 4n), Nat.is_lt(FW.P0(v), 4n), N.le_succ_lt(FW.P0(v), 4n)),
535	    N.le_ne(FW.P0(v), 4n, hp4, hne))
536	  +hlt2 = AB.subst(Nat, y => {Nat.is_lt(y, 4n) == True{} : Bool}, FW.P0(v), Nat.add(o, r), hv, hlt)
537	  +eo = N.le_sub_add(o, 4n, N.lt_to_le(o, 4n, ho))
538	  +hrl0 = lt_cancel(o, r, Nat.sub(4n, o), AB.subst(Nat, y => {Nat.is_lt(Nat.add(o, r), y) == True{} : Bool}, 4n, Nat.add(o, Nat.sub(4n, o)), Equal.sym(Nat, Nat.add(o, Nat.sub(4n, o)), 4n, eo), hlt2))
539	  +hrl = AB.subst(Nat, y => {Nat.is_lt(r, y) == True{} : Bool}, Nat.sub(4n, o), List.length(&2, U32, AW(t, wi, o)), Equal.sym(Nat, List.length(&2, U32, AW(t, wi, o)), Nat.sub(4n, o), awl(t, wi, o)), hrl0)
540	  +eb = Equal.trans(Nat, U32.to_nat(FA.bidx(FA.zb(v))), FW.P0(v), Nat.add(o, r), FW.zb_bidx(v, hlt), hv)
541	  +hw4 = wb4(W, Nat.pow(2n, d), hk)
542	  +esh = shl2(wi, d, hd, N.le_trans(Nat.mul(W, 4n), Nat.add(Nat.mul(W, 4n), 4n), M4, N.le_add_r(Nat.mul(W, 4n), 4n), hw4))
543	  +b1 = N.le_trans(Nat.add(Nat.mul(W, 4n), Nat.add(o, r)), Nat.add(Nat.mul(W, 4n), 4n), M4,
544	    N.le_add_mono_l(Nat.mul(W, 4n), Nat.add(o, r), 4n, N.lt_to_le(Nat.add(o, r), 4n, hlt2)), hw4)
545	  +b2 = AB.subst(Nat, y => {Nat.is_le(Nat.add(y, Nat.add(o, r)), M4) == True{} : Bool}, Nat.mul(W, 4n), U32.to_nat((wi << 2n : U32)), Equal.sym(Nat, U32.to_nat((wi << 2n : U32)), Nat.mul(W, 4n), esh), b1)
546	  +b3 = AB.subst(Nat, y => {Nat.is_le(Nat.add(U32.to_nat((wi << 2n : U32)), y), M4) == True{} : Bool}, Nat.add(o, r), U32.to_nat(FA.bidx(FA.zb(v))),
547	    Equal.sym(Nat, U32.to_nat(FA.bidx(FA.zb(v))), Nat.add(o, r), eb), b2)
548	  +ej = C.add_fits((wi << 2n : U32), FA.bidx(FA.zb(v)), d, hd, b3)
549	  +RHS = D.first(UB(t), SS(wi, o), T, c)
550	  %Equal.sym(Nat, U32.to_nat(U32.min(((wi << 2n : U32) + FA.bidx(FA.zb(v)) : U32), to)), Nat.min(U32.to_nat(((wi << 2n : U32) + FA.bidx(FA.zb(v)) : U32)), T),
551	    U.to_nat_min(((wi << 2n : U32) + FA.bidx(FA.zb(v)) : U32), to)) :
552	    {_ == RHS : Nat}
553	  %Equal.sym(Nat, U32.to_nat(((wi << 2n : U32) + FA.bidx(FA.zb(v)) : U32)), Nat.add(U32.to_nat((wi << 2n : U32)), U32.to_nat(FA.bidx(FA.zb(v)))), ej) :
554	    {Nat.min(_, T) == RHS : Nat}
555	  %Equal.sym(Nat, U32.to_nat(FA.bidx(FA.zb(v))), Nat.add(o, r), eb) :
556	    {Nat.min(Nat.add(U32.to_nat((wi << 2n : U32)), _), T) == RHS : Nat}
557	  %Equal.sym(Nat, U32.to_nat((wi << 2n : U32)), Nat.mul(W, 4n), esh) :
558	    {Nat.min(Nat.add(_, Nat.add(o, r)), T) == RHS : Nat}
559	  %N.add_assoc(Nat.mul(W, 4n), o, r) :
560	    {Nat.min(_, T) == RHS : Nat}
561	  %Equal.sym(Nat, Nat.min(Nat.add(SS(wi, o), r), T), Nat.add(SS(wi, o), Nat.min(r, Nat.sub(T, SS(wi, o)))), min_shift(SS(wi, o), r, T, hs)) :
562	    {_ == RHS : Nat}
563	  %Equal.sym(List<&2, U32>, List.drop(&2, U32, UB(t), SS(wi, o)), List.append(&2, U32, AW(t, wi, o), BW(t, wi)), dw(t, d, wi, o, hf, hd, hk, N.lt_to_le(o, 4n, ho))) :
564	    {Nat.add(SS(wi, o), Nat.min(r, Nat.sub(T, SS(wi, o)))) == Nat.add(SS(wi, o), D.run_len(List.take(&2, U32, _, Nat.sub(T, SS(wi, o))), c)) : Nat}
565	  %Equal.sym(Nat, D.run_len(List.take(&2, U32, List.append(&2, U32, AW(t, wi, o), BW(t, wi)), Nat.sub(T, SS(wi, o))), c), Nat.min(r, Nat.sub(T, SS(wi, o))),
566	    run_hit(AW(t, wi, o), BW(t, wi), Nat.sub(T, SS(wi, o)), c, hd_eq(AW(t, wi, o), c), {==}, hrl)) :
567	    {Nat.add(SS(wi, o), Nat.min(r, Nat.sub(T, SS(wi, o)))) == Nat.add(SS(wi, o), _) : Nat}
568	  {==}
569	
570	# An unflagged word has no c from the start on.
571	law nohit_run:
572	  for +t: P.Tree<U32>
573	  for +wi: U32
574	  for +o: Nat
575	  for +v: U32
576	  for +c: U32
577	  for +hv: {FW.P0(v) == Nat.add(o, D.run_len(AW(t, wi, o), c)) : Nat}
578	  for +hz: {U32.is_zero(FA.zb(v)) == True{} : Bool}
579	  {D.run_len(AW(t, wi, o), c) == List.length(&2, U32, AW(t, wi, o)) : Nat}
580	
581	def nohit_run(t, wi, o, v, c, hv, hz):
582	  +r = D.run_len(AW(t, wi, o), c)
583	  +e4 = N.eq_sound(FW.P0(v), 4n, Equal.trans(Bool, Nat.is_eq(FW.P0(v), 4n), U32.is_zero(FA.zb(v)), True{},
584	    Equal.sym(Bool, U32.is_zero(FA.zb(v)), Nat.is_eq(FW.P0(v), 4n), FW.zb_none(v)), hz))
585	  +e5 = Equal.trans(Nat, Nat.add(o, r), FW.P0(v), 4n, Equal.sym(Nat, FW.P0(v), Nat.add(o, r), hv), e4)
586	  %Equal.sym(Nat, List.length(&2, U32, AW(t, wi, o)), Nat.sub(4n, o), awl(t, wi, o)) : {r == _ : Nat}
587	  %e5 : {r == Nat.sub(_, o) : Nat}
588	  Equal.sym(Nat, Nat.sub(Nat.add(o, r), o), r, N.sub_add_l(o, r))
589	
590	law pow_le4:
591	  for +p: Nat
592	  {Nat.is_le(p, Nat.mul(4n, p)) == True{} : Bool}
593	
594	def pow_le4(p):
595	  N.le_add_r(p, Nat.mul(3n, p))
596	
597	# The last word, unflagged: the answer is to.
598	law fnone0:
599	  for +len: U32
600	  for +t: P.Tree<U32>
601	  for +d: Nat
602	  for +to: U32
603	  for +c: U32
604	  for +wi: U32
605	  for +o: Nat
606	  for +v: U32
607	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
608	  for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
609	  for +ho: {Nat.is_lt(o, 4n) == True{} : Bool}
610	  for +hs: {Nat.is_le(SS(wi, o), U32.to_nat(to)) == True{} : Bool}
611	  for +hk: {Nat.is_lt(U32.to_nat(wi), Nat.pow(2n, d)) == True{} : Bool}
612	  for +hv: {FW.P0(v) == Nat.add(o, D.run_len(AW(t, wi, o), c)) : Nat}
613	  for +hz: {U32.is_zero(FA.zb(v)) == True{} : Bool}
614	  for +he: {Nat.is_le(U32.to_nat(to), Nat.mul(Nat.add(U32.to_nat(wi), 1n), 4n)) == True{} : Bool}
615	  {U32.to_nat(U32.min(4294967295, to)) == D.first(UB(t), SS(wi, o), U32.to_nat(to), c) : Nat}
616	
617	def fnone0(len, t, d, to, c, wi, o, v, h, ht, ho, hs, hk, hv, hz, he):
618	  +W = U32.to_nat(wi)
619	  +T = U32.to_nat(to)
620	  +X = Nat.sub(T, SS(wi, o))
621	  +hd = C.ok_d(len, t, d, h)
622	  +hf = C.ok_full(len, t, d, h)
623	  +a1 = AB.subst(Nat, y => {Nat.is_le(T, y) == True{} : Bool}, Nat.mul(Nat.add(W, 1n), 4n), Nat.add(Nat.mul(W, 4n), 4n), mul4s(W), he)
624	  +a2 = AB.subst(Nat, y => {Nat.is_le(y, Nat.add(Nat.mul(W, 4n), 4n)) == True{} : Bool}, T, Nat.add(SS(wi, o), X),
625	    Equal.sym(Nat, Nat.add(SS(wi, o), X), T, N.le_sub_add(SS(wi, o), T, hs)), a1)
626	  +a3 = AB.subst(Nat, y => {Nat.is_le(y, Nat.add(Nat.mul(W, 4n), 4n)) == True{} : Bool}, Nat.add(Nat.add(Nat.mul(W, 4n), o), X), Nat.add(Nat.mul(W, 4n), Nat.add(o, X)),
627	    N.add_assoc(Nat.mul(W, 4n), o, X), a2)
628	  +a4 = N.le_sub_r(o, X, 4n, le_cancel(Nat.mul(W, 4n), Nat.add(o, X), 4n, a3))
629	  +hn = AB.subst(Nat, y => {Nat.is_le(X, y) == True{} : Bool}, Nat.sub(4n, o), List.length(&2, U32, AW(t, wi, o)),
630	    Equal.sym(Nat, List.length(&2, U32, AW(t, wi, o)), Nat.sub(4n, o), awl(t, wi, o)), a4)
631	  +RHS = D.first(UB(t), SS(wi, o), T, c)
632	  %Equal.sym(U32, U32.min(4294967295, to), to, min_top(to, d, hd, N.le_trans(T, U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), ht, C.ok_len(len, t, d, h)))) :
633	    {U32.to_nat(_) == RHS : Nat}
634	  %Equal.sym(List<&2, U32>, List.drop(&2, U32, UB(t), SS(wi, o)), List.append(&2, U32, AW(t, wi, o), BW(t, wi)), dw(t, d, wi, o, hf, hd, hk, N.lt_to_le(o, 4n, ho))) :
635	    {T == Nat.add(SS(wi, o), D.run_len(List.take(&2, U32, _, X), c)) : Nat}
636	  %Equal.sym(Nat, D.run_len(List.take(&2, U32, List.append(&2, U32, AW(t, wi, o), BW(t, wi)), X), c), X,
637	    run_none(AW(t, wi, o), BW(t, wi), X, c, hd_eq(AW(t, wi, o), c), {==}, nohit_run(t, wi, o, v, c, hv, hz), hn)) :
638	    {T == Nat.add(SS(wi, o), _) : Nat}
639	  Equal.sym(Nat, Nat.add(SS(wi, o), X), T, N.le_sub_add(SS(wi, o), T, hs))
640	
641	# An unflagged word that is not the last: the search goes on at the next word.
642	law fskip:
643	  for +len: U32
644	  for +t: P.Tree<U32>
645	  for +d: Nat
646	  for +to: U32
647	  for +c: U32
648	  for +wi: U32
649	  for +o: Nat
650	  for +v: U32
651	  for +k: Nat
652	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
653	  for +ho: {Nat.is_lt(o, 4n) == True{} : Bool}
654	  for +hs: {Nat.is_le(SS(wi, o), U32.to_nat(to)) == True{} : Bool}
655	  for +hk: {Nat.is_lt(U32.to_nat(wi), Nat.pow(2n, d)) == True{} : Bool}
656	  for +hv: {FW.P0(v) == Nat.add(o, D.run_len(AW(t, wi, o), c)) : Nat}
657	  for +hz: {U32.is_zero(FA.zb(v)) == True{} : Bool}
658	  for +hs1: {Nat.is_le(Nat.mul(Nat.add(U32.to_nat(wi), 1n), 4n), U32.to_nat(to)) == True{} : Bool}
659	  {D.first(UB(t), SS(wi, o), U32.to_nat(to), c) == D.first(UB(t), Nat.mul(Nat.add(U32.to_nat(wi), 1n), 4n), U32.to_nat(to), c) : Nat}
660	
661	def fskip(len, t, d, to, c, wi, o, v, k, h, ho, hs, hk, hv, hz, hs1):
662	  +W = U32.to_nat(wi)
663	  +T = U32.to_nat(to)
664	  +S = SS(wi, o)
665	  +S1 = Nat.mul(Nat.add(W, 1n), 4n)
666	  +L = Nat.sub(4n, o)
667	  +hd = C.ok_d(len, t, d, h)
668	  +hf = C.ok_full(len, t, d, h)
669	  +eS = Equal.trans(Nat, Nat.add(S, L), Nat.add(Nat.mul(W, 4n), Nat.add(o, L)), S1, N.add_assoc(Nat.mul(W, 4n), o, L),
670	    Equal.trans(Nat, Nat.add(Nat.mul(W, 4n), Nat.add(o, L)), Nat.add(Nat.mul(W, 4n), 4n), S1,
671	      Equal.cong(Nat, Nat, y => Nat.add(Nat.mul(W, 4n), y), Nat.add(o, L), 4n, N.le_sub_add(o, 4n, N.lt_to_le(o, 4n, ho))),
672	      Equal.sym(Nat, S1, Nat.add(Nat.mul(W, 4n), 4n), mul4s(W))))
673	  +hl0 = N.le_sub_r(S, L, T, AB.subst(Nat, y => {Nat.is_le(y, T) == True{} : Bool}, S1, Nat.add(S, L), Equal.sym(Nat, Nat.add(S, L), S1, eS), hs1))
674	  +hn = AB.subst(Nat, y => {Nat.is_le(y, Nat.sub(T, S)) == True{} : Bool}, L, List.length(&2, U32, AW(t, wi, o)),
675	    Equal.sym(Nat, List.length(&2, U32, AW(t, wi, o)), L, awl(t, wi, o)), hl0)
676	  +RHS = D.first(UB(t), S1, T, c)
677	  %Equal.sym(List<&2, U32>, List.drop(&2, U32, UB(t), S), List.append(&2, U32, AW(t, wi, o), BW(t, wi)), dw(t, d, wi, o, hf, hd, hk, N.lt_to_le(o, 4n, ho))) :
678	    {Nat.add(S, D.run_len(List.take(&2, U32, _, Nat.sub(T, S)), c)) == RHS : Nat}
679	  %Equal.sym(Nat, D.run_len(List.take(&2, U32, List.append(&2, U32, AW(t, wi, o), BW(t, wi)), Nat.sub(T, S)), c),
680	    Nat.add(List.length(&2, U32, AW(t, wi, o)), D.run_len(List.take(&2, U32, BW(t, wi), Nat.sub(Nat.sub(T, S), List.length(&2, U32, AW(t, wi, o)))), c)),
681	    run_skip(AW(t, wi, o), BW(t, wi), Nat.sub(T, S), c, hd_eq(AW(t, wi, o), c), {==}, nohit_run(t, wi, o, v, c, hv, hz), hn)) :
682	    {Nat.add(S, _) == RHS : Nat}
683	  %Equal.sym(Nat, List.length(&2, U32, AW(t, wi, o)), L, awl(t, wi, o)) :
684	    {Nat.add(S, Nat.add(_, D.run_len(List.take(&2, U32, BW(t, wi), Nat.sub(Nat.sub(T, S), _)), c))) == RHS : Nat}
685	  %Equal.sym(Nat, Nat.sub(Nat.sub(T, S), L), Nat.sub(T, Nat.add(S, L)), sub_sub(T, S, L)) :
686	    {Nat.add(S, Nat.add(L, D.run_len(List.take(&2, U32, BW(t, wi), _), c))) == RHS : Nat}
687	  %N.add_assoc(S, L, D.run_len(List.take(&2, U32, BW(t, wi), Nat.sub(T, Nat.add(S, L))), c)) :
688	    {_ == RHS : Nat}
689	  %Equal.sym(Nat, Nat.add(S, L), S1, eS) :
690	    {Nat.add(_, D.run_len(List.take(&2, U32, BW(t, wi), Nat.sub(T, _)), c)) == RHS : Nat}
691	  {==}
692	
693	# The first byte of the next word starts a fresh search.
694	law hv0:
695	  for +t: P.Tree<U32>
696	  for +wi: U32
697	  for +c: U32
698	  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
699	  {FW.P0(U32.xor(C.WD(t, wi), FA.rep(c))) == Nat.add(0n, D.run_len(AW(t, wi, 0n), c)) : Nat}
700	
701	def hv0(t, wi, c, hc):
702	  %Equal.sym(List<&2, U32>, List.drop(&2, U32, C.L4(C.WD(t, wi)), 0n), C.L4(C.WD(t, wi)), X.drop_zero(C.L4(C.WD(t, wi)))) :
703	    {FW.P0(U32.xor(C.WD(t, wi), FA.rep(c))) == Nat.add(0n, D.run_len(_, c)) : Nat}
704	  FW.p0_xor(C.WD(t, wi), c, hc)
705	
706	# The loop invariant, for 1 + k words left (wi's included): the answer, capped
707	# at to, is the first c from the start o bytes into word wi.
708	law fi:
709	  for +k: Nat
710	  for +z: Bool
711	  for +len: U32
712	  for +t: P.Tree<U32>
713	  for +d: Nat
714	  for +to: U32
715	  for +c: U32
716	  for +wi: U32
717	  for +o: Nat
718	  for +v: U32
719	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
720	  for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
721	  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
722	  for +ho: {Nat.is_lt(o, 4n) == True{} : Bool}
723	  for +hs: {Nat.is_le(SS(wi, o), U32.to_nat(to)) == True{} : Bool}
724	  for +he1: {Nat.is_le(U32.to_nat(to), Nat.mul(Nat.add(U32.to_nat(wi), 1n+k), 4n)) == True{} : Bool}
725	  for +he2: {Nat.is_lt(Nat.mul(Nat.add(U32.to_nat(wi), k), 4n), U32.to_nat(to)) == True{} : Bool}
726	  for +hv: {FW.P0(v) == Nat.add(o, D.run_len(AW(t, wi, o), c)) : Nat}
727	  for +hz: {U32.is_zero(FA.zb(v)) == z : Bool}
728	  {U32.to_nat(U32.min(FG(1n+k, z, wi, FA.zb(v), FA.rep(c), t), to)) == D.first(UB(t), SS(wi, o), U32.to_nat(to), c) : Nat}
729	
730	def fi(k, z, len, t, d, to, c, wi, o, v, h, ht, hc, ho, hs, he1, he2, hv, hz):
731	  match k z:
732	    case 0n False{}:
733	      fhit(len, t, d, to, c, wi, o, v, h, ht, ho, hs,
734	        wlt(U32.to_nat(wi), 0n, U32.to_nat(to), U32.to_nat(len), Nat.pow(2n, d), he2, ht, C.ok_len(len, t, d, h)), hv, hz)
735	    case 1n+q False{}:
736	      fhit(len, t, d, to, c, wi, o, v, h, ht, ho, hs,
737	        wlt(U32.to_nat(wi), 1n+q, U32.to_nat(to), U32.to_nat(len), Nat.pow(2n, d), he2, ht, C.ok_len(len, t, d, h)), hv, hz)
738	    case 0n True{}:
739	      fnone0(len, t, d, to, c, wi, o, v, h, ht, ho, hs,
740	        wlt(U32.to_nat(wi), 0n, U32.to_nat(to), U32.to_nat(len), Nat.pow(2n, d), he2, ht, C.ok_len(len, t, d, h)), hv, hz, he1)
741	    case 1n+q True{}:
742	      +W = U32.to_nat(wi)
743	      +T = U32.to_nat(to)
744	      +j1 = (wi + 1 : U32)
745	      +v1 = U32.xor(C.WD(t, j1), FA.rep(c))
746	      +S1 = Nat.mul(Nat.add(W, 1n), 4n)
747	      +hk = wlt(W, 1n+q, T, U32.to_nat(len), Nat.pow(2n, d), he2, ht, C.ok_len(len, t, d, h))
748	      +ej1 = C.inc_fits(wi, d, C.ok_d(len, t, d, h), N.lt_le_trans(W, Nat.pow(2n, d), Nat.mul(4n, Nat.pow(2n, d)), hk, pow_le4(Nat.pow(2n, d))))
749	      +hs1 = N.lt_to_le(S1, T, N.le_lt_trans(S1, Nat.mul(Nat.add(W, 1n+q), 4n), T,
750	        N.le_mul_r(Nat.add(W, 1n), Nat.add(W, 1n+q), 4n, N.le_add_mono_l(W, 1n, 1n+q, N.le_zero_l(q))), he2))
751	      +ea = Equal.trans(Nat, Nat.add(Nat.mul(U32.to_nat(j1), 4n), 0n), Nat.mul(U32.to_nat(j1), 4n), S1, N.add_zero(Nat.mul(U32.to_nat(j1), 4n)),
752	        Equal.cong(Nat, Nat, y => Nat.mul(y, 4n), U32.to_nat(j1), Nat.add(W, 1n), ej1))
753	      +hsi = AB.subst(Nat, y => {Nat.is_le(y, T) == True{} : Bool}, S1, SS(j1, 0n), Equal.sym(Nat, SS(j1, 0n), S1, ea), hs1)
754	      +e1 = Equal.trans(Nat, Nat.add(U32.to_nat(j1), 1n+q), Nat.add(Nat.add(W, 1n), 1n+q), Nat.add(W, 1n+(1n+q)),
755	        Equal.cong(Nat, Nat, y => Nat.add(y, 1n+q), U32.to_nat(j1), Nat.add(W, 1n), ej1), N.add_assoc(W, 1n, 1n+q))
756	      +he1i = AB.subst(Nat, y => {Nat.is_le(T, Nat.mul(y, 4n)) == True{} : Bool}, Nat.add(W, 1n+(1n+q)), Nat.add(U32.to_nat(j1), 1n+q),
757	        Equal.sym(Nat, Nat.add(U32.to_nat(j1), 1n+q), Nat.add(W, 1n+(1n+q)), e1), he1)
758	      +e2 = Equal.trans(Nat, Nat.add(U32.to_nat(j1), q), Nat.add(Nat.add(W, 1n), q), Nat.add(W, 1n+q),
759	        Equal.cong(Nat, Nat, y => Nat.add(y, q), U32.to_nat(j1), Nat.add(W, 1n), ej1), N.add_assoc(W, 1n, q))
760	      +he2i = AB.subst(Nat, y => {Nat.is_lt(Nat.mul(y, 4n), T) == True{} : Bool}, Nat.add(W, 1n+q), Nat.add(U32.to_nat(j1), q),
761	        Equal.sym(Nat, Nat.add(U32.to_nat(j1), q), Nat.add(W, 1n+q), e2), he2)
762	      +ih = fi(q, U32.is_zero(FA.zb(v1)), len, t, d, to, c, j1, 0n, v1, h, ht, hc, {==}, hsi, he1i, he2i, hv0(t, j1, c, hc), {==})
763	      +sk = fskip(len, t, d, to, c, wi, o, v, q, h, ho, hs, hk, hv, hz, hs1)
764	      Equal.trans(Nat, U32.to_nat(U32.min(FG(1n+q, U32.is_zero(FA.zb(v1)), j1, FA.zb(v1), FA.rep(c), t), to)), D.first(UB(t), SS(j1, 0n), T, c), D.first(UB(t), SS(wi, o), T, c),
765	        ih, Equal.sym(Nat, D.first(UB(t), SS(wi, o), T, c), D.first(UB(t), SS(j1, 0n), T, c),
766	          Equal.trans(Nat, D.first(UB(t), SS(wi, o), T, c), D.first(UB(t), S1, T, c), D.first(UB(t), SS(j1, 0n), T, c), sk,
767	            Equal.cong(Nat, Nat, y => D.first(UB(t), y, T, c), S1, SS(j1, 0n), Equal.sym(Nat, SS(j1, 0n), S1, ea)))))
768	
769	# The top level
770	# =============
771	
772	law slice_take:
773	  for +xs: List<&2, U32>
774	  for +l: Nat
775	  for +f: Nat
776	  for +n: Nat
777	  for +h: {Nat.is_le(Nat.add(f, n), l) == True{} : Bool}
778	  {D.slice(List.take(&2, U32, xs, l), f, n) == D.slice(xs, f, n) : List<&2, U32>}
779	
780	def slice_take(xs, l, f, n, h):
781	  match xs l f:
782	    case Nil{} _ _:
783	      {==}
784	    case Con{x, t} 0n 0n:
785	      match n:
786	        case 0n:
787	          {==}
788	        case 1n+q:
789	          Empty.absurd({D.slice(Nil{}, 0n, 1n+q) == D.slice(x <> t, 0n, 1n+q) : List<&2, U32>}, AB.false_ne_true(h))
790	    case Con{x, t} 0n 1n+g:
791	      Empty.absurd({D.slice(Nil{}, 1n+g, n) == D.slice(x <> t, 1n+g, n) : List<&2, U32>}, AB.false_ne_true(h))
792	    case Con{+x, t} 1n+p 0n:
793	      match n:
794	        case 0n:
795	          {==}
796	        case 1n+q:
797	          Equal.cong(List<&2, U32>, List<&2, U32>, y => x <> y, List.take(&2, U32, List.take(&2, U32, t, p), q), List.take(&2, U32, t, q), Q.take_take(t, p, q, h))
798	    case Con{x, t} 1n+p 1n+g:
799	      slice_take(t, p, g, n, h)
800	
801	law le_antisym:
802	  for +a: Nat
803	  for +b: Nat
804	  for +h1: {Nat.is_le(a, b) == True{} : Bool}
805	  for +h2: {Nat.is_le(b, a) == True{} : Bool}
806	  {a == b : Nat}
807	
808	def le_antisym(a, b, h1, h2):
809	  match a b:
810	    case 0n 0n:
811	      {==}
812	    case 0n 1n+q:
813	      Empty.absurd({0n == 1n+q : Nat}, AB.false_ne_true(h2))
814	    case 1n+p 0n:
815	      Empty.absurd({1n+p == 0n : Nat}, AB.false_ne_true(h1))
816	    case 1n+p 1n+q:
817	      %le_antisym(p, q, h1, h2) : {1n+p == 1n+_ : Nat}
818	      {==}
819	
820	law lt_add_l:
821	  for +c: Nat
822	  for +a: Nat
823	  for +b: Nat
824	  for +h: {Nat.is_lt(a, b) == True{} : Bool}
825	  {Nat.is_lt(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}
826	
827	def lt_add_l(c, a, b, h):
828	  match c:
829	    case 0n:
830	      h
831	    case 1n+p:
832	      lt_add_l(p, a, b, h)
833	
834	law div_le4:
835	  for +a: Nat
836	  for +b: Nat
837	  for +h: {Nat.is_le(a, b) == True{} : Bool}
838	  {Nat.is_le(Nat.div(a, 4n), Nat.div(b, 4n)) == True{} : Bool}
839	
840	def div_le4(a, b, h):
841	  +qb = Nat.div(b, 4n)
842	  +rb = Nat.mod(b, 4n)
843	  +hb = AB.subst(Nat, y => {Nat.is_le(a, y) == True{} : Bool}, b, Nat.add(Nat.mul(qb, 4n), rb), Equal.sym(Nat, Nat.add(Nat.mul(qb, 4n), rb), b, N.div_mod(b, 4n)), h)
844	  +h1 = N.le_lt_trans(a, Nat.add(Nat.mul(qb, 4n), rb), Nat.add(Nat.mul(qb, 4n), 4n), hb, lt_add_l(Nat.mul(qb, 4n), rb, 4n, N.mod_lt(b, 4n, {==})))
845	  +h2 = AB.subst(Nat, y => {Nat.is_lt(a, y) == True{} : Bool}, Nat.add(Nat.mul(qb, 4n), 4n), Nat.mul(4n, 1n+qb),
846	    Equal.trans(Nat, Nat.add(Nat.mul(qb, 4n), 4n), Nat.mul(1n+qb, 4n), Nat.mul(4n, 1n+qb),
847	      Equal.trans(Nat, Nat.add(Nat.mul(qb, 4n), 4n), Nat.add(4n, Nat.mul(qb, 4n)), Nat.mul(1n+qb, 4n), N.add_comm(Nat.mul(qb, 4n), 4n), {==}),
848	      N.mul_comm(1n+qb, 4n)), h1)
849	  Equal.trans(Bool, Nat.is_le(Nat.div(a, 4n), qb), Nat.is_lt(Nat.div(a, 4n), 1n+qb), True{},
850	    Equal.sym(Bool, Nat.is_lt(Nat.div(a, 4n), 1n+qb), Nat.is_le(Nat.div(a, 4n), qb), N.lt_succ_iff(Nat.div(a, 4n), qb)),
851	    N.div_lt(a, 4n, 1n+qb, {==}, h2))
852	
853	# The last word holds byte to - 1: 4E < to <= 4E + 4 for E = (to - 1) / 4.
854	law last_lt:
855	  for +tt: Nat
856	  for +h: {Nat.is_lt(0n, tt) == True{} : Bool}
857	  {Nat.is_lt(Nat.mul(Nat.div(Nat.sub(tt, 1n), 4n), 4n), tt) == True{} : Bool}
858	
859	def last_lt(tt, h):
860	  match tt:
861	    case 0n:
862	      Empty.absurd({Nat.is_lt(Nat.mul(Nat.div(Nat.sub(0n, 1n), 4n), 4n), 0n) == True{} : Bool}, AB.false_ne_true(h))
863	    case 1n+p:
864	      %Equal.sym(Nat, Nat.sub(p, 0n), p, N.sub_zero(p)) : {Nat.is_lt(Nat.mul(Nat.div(_, 4n), 4n), 1n+p) == True{} : Bool}
865	      Equal.trans(Bool, Nat.is_lt(Nat.mul(Nat.div(p, 4n), 4n), 1n+p), Nat.is_le(Nat.mul(Nat.div(p, 4n), 4n), p), True{},
866	        N.lt_succ_iff(Nat.mul(Nat.div(p, 4n), 4n), p),
867	        AB.subst(Nat, y => {Nat.is_le(Nat.mul(Nat.div(p, 4n), 4n), y) == True{} : Bool}, Nat.add(Nat.mul(Nat.div(p, 4n), 4n), Nat.mod(p, 4n)), p, N.div_mod(p, 4n),
868	          N.le_add_r(Nat.mul(Nat.div(p, 4n), 4n), Nat.mod(p, 4n))))
869	
870	law last_le:
871	  for +tt: Nat
872	  for +h: {Nat.is_lt(0n, tt) == True{} : Bool}
873	  {Nat.is_le(tt, Nat.mul(Nat.add(Nat.div(Nat.sub(tt, 1n), 4n), 1n), 4n)) == True{} : Bool}
874	
875	def last_le(tt, h):
876	  match tt:
877	    case 0n:
878	      Empty.absurd({Nat.is_le(0n, Nat.mul(Nat.add(Nat.div(Nat.sub(0n, 1n), 4n), 1n), 4n)) == True{} : Bool}, AB.false_ne_true(h))
879	    case 1n+p:
880	      +q = Nat.div(p, 4n)
881	      %Equal.sym(Nat, Nat.sub(p, 0n), p, N.sub_zero(p)) : {Nat.is_le(1n+p, Nat.mul(Nat.add(Nat.div(_, 4n), 1n), 4n)) == True{} : Bool}
882	      %Equal.sym(Nat, Nat.mul(Nat.add(q, 1n), 4n), Nat.add(Nat.mul(q, 4n), 4n), mul4s(q)) : {Nat.is_le(1n+p, _) == True{} : Bool}
883	      %N.div_mod(p, 4n) : {Nat.is_le(1n+_, Nat.add(Nat.mul(q, 4n), 4n)) == True{} : Bool}
884	      %N.add_succ(Nat.mul(q, 4n), Nat.mod(p, 4n)) : {Nat.is_le(_, Nat.add(Nat.mul(q, 4n), 4n)) == True{} : Bool}
885	      N.le_add_mono_l(Nat.mul(q, 4n), 1n+Nat.mod(p, 4n), 4n,
886	        Equal.trans(Bool, Nat.is_le(1n+Nat.mod(p, 4n), 4n), Nat.is_lt(Nat.mod(p, 4n), 4n), True{}, N.le_succ_lt(Nat.mod(p, 4n), 4n), N.mod_lt(p, 4n, {==})))
887	
888	law lt_sub1:
889	  for +f: Nat
890	  for +tt: Nat
891	  for +h: {Nat.is_lt(f, tt) == True{} : Bool}
892	  {Nat.is_le(f, Nat.sub(tt, 1n)) == True{} : Bool}
893	
894	def lt_sub1(f, tt, h):
895	  match tt:
896	    case 0n:
897	      Empty.absurd({Nat.is_le(f, 0n) == True{} : Bool}, AB.lt_zero_absurd(f, h))
898	    case 1n+p:
899	      %Equal.sym(Nat, Nat.sub(p, 0n), p, N.sub_zero(p)) : {Nat.is_le(f, _) == True{} : Bool}
900	      Equal.trans(Bool, Nat.is_le(f, p), Nat.is_lt(f, 1n+p), True{}, Equal.sym(Bool, Nat.is_lt(f, 1n+p), Nat.is_le(f, p), N.lt_succ_iff(f, p)), h)
901	
902	law div_self_le:
903	  for +a: Nat
904	  {Nat.is_le(Nat.div(a, 4n), a) == True{} : Bool}
905	
906	def div_self_le(a):
907	  +h = Equal.trans(Bool, Nat.is_lt(a, 1n+Nat.add(a, Nat.mul(3n, 1n+a))), Nat.is_le(a, Nat.add(a, Nat.mul(3n, 1n+a))), True{},
908	    N.lt_succ_iff(a, Nat.add(a, Nat.mul(3n, 1n+a))), N.le_add_r(a, Nat.mul(3n, 1n+a)))
909	  Equal.trans(Bool, Nat.is_le(Nat.div(a, 4n), a), Nat.is_lt(Nat.div(a, 4n), 1n+a), True{},
910	    Equal.sym(Bool, Nat.is_lt(Nat.div(a, 4n), 1n+a), Nat.is_le(Nat.div(a, 4n), a), N.lt_succ_iff(Nat.div(a, 4n), a)),
911	    N.div_lt(a, 4n, 1n+a, {==}, h))
912	
913	law sub1_lt:
914	  for +tt: Nat
915	  for +h: {Nat.is_lt(0n, tt) == True{} : Bool}
916	  {Nat.is_lt(Nat.sub(tt, 1n), tt) == True{} : Bool}
917	
918	def sub1_lt(tt, h):
919	  match tt:
920	    case 0n:
921	      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, AB.false_ne_true(h))
922	    case 1n+p:
923	      %Equal.sym(Nat, Nat.sub(p, 0n), p, N.sub_zero(p)) : {Nat.is_lt(_, 1n+p) == True{} : Bool}
924	      Equal.trans(Bool, Nat.is_lt(p, 1n+p), Nat.is_le(p, p), True{}, N.lt_succ_iff(p, p), N.le_refl(p))
925	
926	# from < to: the loop runs 1 + k0 words, from word from >> 2 to word (to - 1) >> 2.
927	law fview_lt:
928	  for +len: U32
929	  for +t: P.Tree<U32>
930	  for +d: Nat
931	  for +from: U32
932	  for +to: U32
933	  for +c: U32
934	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
935	  for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
936	  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
937	  for +hlt: {Nat.is_lt(U32.to_nat(from), U32.to_nat(to)) == True{} : Bool}
938	  {U32.to_nat(U32.min(FG(U32.to_nat(((((to - 1 : U32) >> 2n : U32) - (from >> 2n : U32) : U32) + 1 : U32)), U32.is_zero(M0(t, from, FA.rep(c))), (from >> 2n : U32), M0(t, from, FA.rep(c)), FA.rep(c), t), to)) == D.first(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c) : Nat}
939	
940	def fview_lt(len, t, d, from, to, c, h, ht, hc, hlt):
941	  +F = U32.to_nat(from)
942	  +T = U32.to_nat(to)
943	  +wi0 = (from >> 2n : U32)
944	  +W0 = U32.to_nat(wi0)
945	  +o0 = U32.to_nat((from .&. 3 : U32))
946	  +ee = ((to - 1 : U32) >> 2n : U32)
947	  +E = U32.to_nat(ee)
948	  +rc = FA.rep(c)
949	  +hd = C.ok_d(len, t, d, h)
950	  +M4 = Nat.mul(4n, Nat.pow(2n, d))
951	  +hTM = N.le_trans(T, U32.to_nat(len), M4, ht, C.ok_len(len, t, d, h))
952	  +h0T = N.le_lt_trans(0n, F, T, N.le_zero_l(F), hlt)
953	  +eW0 = U.to_nat_shrn(from, 2n)
954	  +eo = U.to_nat_and_mask(from, 3, 2n, {==})
955	  +et1 = U.to_nat_sub_le(to, 1, Equal.trans(Bool, U32.is_le(1, to), Nat.is_le(U32.to_nat(1), T), True{}, U.is_le_to_nat(1, to),
956	    Equal.trans(Bool, Nat.is_le(1n, T), Nat.is_lt(0n, T), True{}, N.le_succ_lt(0n, T), h0T)))
957	  +eE = Equal.trans(Nat, E, Nat.div(U32.to_nat((to - 1 : U32)), 4n), Nat.div(Nat.sub(T, 1n), 4n), U.to_nat_shrn((to - 1 : U32), 2n),
958	    Equal.cong(Nat, Nat, y => Nat.div(y, 4n), U32.to_nat((to - 1 : U32)), Nat.sub(T, 1n), et1))
959	  +hWE = AB.subst(Nat, y => {Nat.is_le(W0, y) == True{} : Bool}, Nat.div(Nat.sub(T, 1n), 4n), E, Equal.sym(Nat, E, Nat.div(Nat.sub(T, 1n), 4n), eE),
960	    AB.subst(Nat, y => {Nat.is_le(y, Nat.div(Nat.sub(T, 1n), 4n)) == True{} : Bool}, Nat.div(F, 4n), W0, Equal.sym(Nat, W0, Nat.div(F, 4n), eW0),
961	      div_le4(F, Nat.sub(T, 1n), lt_sub1(F, T, hlt))))
962	  +k0 = Nat.sub(E, W0)
963	  +esub = U.to_nat_sub_le(ee, wi0, Equal.trans(Bool, U32.is_le(wi0, ee), Nat.is_le(W0, E), True{}, U.is_le_to_nat(wi0, ee), hWE))
964	  +hET = N.le_lt_trans(E, Nat.sub(T, 1n), T,
965	    AB.subst(Nat, y => {Nat.is_le(y, Nat.sub(T, 1n)) == True{} : Bool}, Nat.div(Nat.sub(T, 1n), 4n), E, Equal.sym(Nat, E, Nat.div(Nat.sub(T, 1n), 4n), eE), div_self_le(Nat.sub(T, 1n))),
966	    sub1_lt(T, h0T))
967	  +ek = C.inc_fits((ee - wi0 : U32), d, hd,
968	    AB.subst(Nat, y => {Nat.is_lt(y, M4) == True{} : Bool}, k0, U32.to_nat((ee - wi0 : U32)), Equal.sym(Nat, U32.to_nat((ee - wi0 : U32)), k0, esub),
969	      N.le_lt_trans(k0, E, M4, H.sub_le(E, W0), N.lt_le_trans(E, T, M4, hET, hTM))))
970	  +en = Equal.trans(Nat, U32.to_nat(((ee - wi0 : U32) + 1 : U32)), Nat.add(U32.to_nat((ee - wi0 : U32)), 1n), 1n+k0, ek,
971	    Equal.trans(Nat, Nat.add(U32.to_nat((ee - wi0 : U32)), 1n), Nat.add(k0, 1n), 1n+k0, Equal.cong(Nat, Nat, y => Nat.add(y, 1n), U32.to_nat((ee - wi0 : U32)), k0, esub), N.add_one(k0)))
972	  +eSF = Equal.trans(Nat, SS(wi0, o0), Nat.add(Nat.mul(Nat.div(F, 4n), 4n), Nat.mod(F, 4n)), F,
973	    Equal.trans(Nat, Nat.add(Nat.mul(W0, 4n), o0), Nat.add(Nat.mul(Nat.div(F, 4n), 4n), o0), Nat.add(Nat.mul(Nat.div(F, 4n), 4n), Nat.mod(F, 4n)),
974	      Equal.cong(Nat, Nat, y => Nat.add(Nat.mul(y, 4n), o0), W0, Nat.div(F, 4n), eW0),
975	      Equal.cong(Nat, Nat, y => Nat.add(Nat.mul(Nat.div(F, 4n), 4n), y), o0, Nat.mod(F, 4n), eo)),
976	    N.div_mod(F, 4n))
977	  +ho0 = AB.subst(Nat, y => {Nat.is_lt(y, 4n) == True{} : Bool}, Nat.mod(F, 4n), o0, Equal.sym(Nat, o0, Nat.mod(F, 4n), eo), N.mod_lt(F, 4n, {==}))
978	  +hs0 = AB.subst(Nat, y => {Nat.is_le(y, T) == True{} : Bool}, F, SS(wi0, o0), Equal.sym(Nat, SS(wi0, o0), F, eSF), N.lt_to_le(F, T, hlt))
979	  +eWk = N.le_sub_add(W0, E, hWE)
980	  +eA = Equal.trans(Nat, Nat.add(W0, 1n+k0), 1n+Nat.add(W0, k0), Nat.add(Nat.div(Nat.sub(T, 1n), 4n), 1n), N.add_succ(W0, k0),
981	    Equal.trans(Nat, 1n+Nat.add(W0, k0), 1n+E, Nat.add(Nat.div(Nat.sub(T, 1n), 4n), 1n), Equal.cong(Nat, Nat, y => 1n+y, Nat.add(W0, k0), E, eWk),
982	      Equal.trans(Nat, 1n+E, Nat.add(E, 1n), Nat.add(Nat.div(Nat.sub(T, 1n), 4n), 1n), Equal.sym(Nat, Nat.add(E, 1n), 1n+E, N.add_one(E)),
983	        Equal.cong(Nat, Nat, y => Nat.add(y, 1n), E, Nat.div(Nat.sub(T, 1n), 4n), eE))))
984	  +he1 = AB.subst(Nat, y => {Nat.is_le(T, Nat.mul(y, 4n)) == True{} : Bool}, Nat.add(Nat.div(Nat.sub(T, 1n), 4n), 1n), Nat.add(W0, 1n+k0),
985	    Equal.sym(Nat, Nat.add(W0, 1n+k0), Nat.add(Nat.div(Nat.sub(T, 1n), 4n), 1n), eA), last_le(T, h0T))
986	  +eB = Equal.trans(Nat, Nat.add(W0, k0), E, Nat.div(Nat.sub(T, 1n), 4n), eWk, eE)
987	  +he2 = AB.subst(Nat, y => {Nat.is_lt(Nat.mul(y, 4n), T) == True{} : Bool}, Nat.div(Nat.sub(T, 1n), 4n), Nat.add(W0, k0),
988	    Equal.sym(Nat, Nat.add(W0, k0), Nat.div(Nat.sub(T, 1n), 4n), eB), last_lt(T, h0T))
989	  +fiv = fi(k0, U32.is_zero(M0(t, from, rc)), len, t, d, to, c, wi0, o0, U32.or(U32.xor(C.WD(t, wi0), rc), U32.not(FA.low(from))),
990	    h, ht, hc, ho0, hs0, he1, he2, FW.p0_low(C.WD(t, wi0), c, from, hc), {==})
991	  +hh = AB.subst(Nat, y => {Nat.is_le(y, U32.to_nat(len)) == True{} : Bool}, T, Nat.add(F, Nat.sub(T, F)),
992	    Equal.sym(Nat, Nat.add(F, Nat.sub(T, F)), T, N.le_sub_add(F, T, N.lt_to_le(F, T, hlt))), ht)
993	  +E2 = Equal.trans(Nat, D.first(UB(t), SS(wi0, o0), T, c), D.first(UB(t), F, T, c), D.first(D.view(C.BT(len, t)), F, T, c),
994	    Equal.cong(Nat, Nat, y => D.first(UB(t), y, T, c), SS(wi0, o0), F, eSF),
995	    Equal.sym(Nat, D.first(D.view(C.BT(len, t)), F, T, c), D.first(UB(t), F, T, c),
996	      Equal.cong(List<&2, U32>, Nat, y => Nat.add(F, D.run_len(y, c)), D.slice(List.take(&2, U32, UB(t), U32.to_nat(len)), F, Nat.sub(T, F)), D.slice(UB(t), F, Nat.sub(T, F)),
997	        slice_take(UB(t), U32.to_nat(len), F, Nat.sub(T, F), hh))))
998	  %Equal.sym(Nat, U32.to_nat(((ee - wi0 : U32) + 1 : U32)), 1n+k0, en) :
999	    {U32.to_nat(U32.min(FG(_, U32.is_zero(M0(t, from, rc)), wi0, M0(t, from, rc), rc, t), to)) == D.first(D.view(C.BT(len, t)), F, T, c) : Nat}
1000	  Equal.trans(Nat, U32.to_nat(U32.min(FG(1n+k0, U32.is_zero(M0(t, from, rc)), wi0, M0(t, from, rc), rc, t), to)), D.first(UB(t), SS(wi0, o0), T, c),
1001	    D.first(D.view(C.BT(len, t)), F, T, c), fiv, E2)
1002	
1003	# The answer as a number, split on to <= from (no words: the answer is to = from).
1004	law fview_go:
1005	  for +b: Bool
1006	  for +len: U32
1007	  for +t: P.Tree<U32>
1008	  for +d: Nat
1009	  for +from: U32
1010	  for +to: U32
1011	  for +c: U32
1012	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
1013	  for +hft: {U32.is_le(from, to) == True{} : Bool}
1014	  for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
1015	  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
1016	  for +hb: {U32.is_le(to, from) == b : Bool}
1017	  {U32.to_nat(U32.min(FG(Bool.pick(Nat, b, 0n, U32.to_nat(((((to - 1 : U32) >> 2n : U32) - (from >> 2n : U32) : U32) + 1 : U32))), U32.is_zero(M0(t, from, FA.rep(c))), (from >> 2n : U32), M0(t, from, FA.rep(c)), FA.rep(c), t), to)) == D.first(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c) : Nat}
1018	
1019	def fview_go(b, len, t, d, from, to, c, h, hft, ht, hc, hb):
1020	  match b:
1021	    case True{}:
1022	      +F = U32.to_nat(from)
1023	      +T = U32.to_nat(to)
1024	      +xs = D.view(C.BT(len, t))
1025	      +hd = C.ok_d(len, t, d, h)
1026	      +eTF = le_antisym(T, F, Equal.trans(Bool, Nat.is_le(T, F), U32.is_le(to, from), True{}, Equal.sym(Bool, U32.is_le(to, from), Nat.is_le(T, F), U.is_le_to_nat(to, from)), hb),
1027	        Equal.trans(Bool, Nat.is_le(F, T), U32.is_le(from, to), True{}, Equal.sym(Bool, U32.is_le(from, to), Nat.is_le(F, T), U.is_le_to_nat(from, to)), hft))
1028	      %Equal.sym(U32, U32.min(4294967295, to), to, min_top(to, d, hd, N.le_trans(T, U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), ht, C.ok_len(len, t, d, h)))) :
1029	        {U32.to_nat(_) == D.first(xs, F, T, c) : Nat}
1030	      %Equal.sym(Nat, T, F, eTF) : {_ == D.first(xs, F, _, c) : Nat}
1031	      %Equal.sym(Nat, Nat.sub(F, F), 0n, H.sub_self(F)) : {F == Nat.add(F, D.run_len(D.slice(xs, F, _), c)) : Nat}
1032	      %Equal.sym(List<&2, U32>, D.slice(xs, F, 0n), Nil{}, X.slice_zero(xs, F)) : {F == Nat.add(F, D.run_len(_, c)) : Nat}
1033	      Equal.sym(Nat, Nat.add(F, 0n), F, N.add_zero(F))
1034	    case False{}:
1035	      fview_lt(len, t, d, from, to, c, h, ht, hc,
1036	        N.not_le_lt(U32.to_nat(to), U32.to_nat(from), Equal.trans(Bool, Nat.is_le(U32.to_nat(to), U32.to_nat(from)), U32.is_le(to, from), False{},
1037	          Equal.sym(Bool, U32.is_le(to, from), Nat.is_le(U32.to_nat(to), U32.to_nat(from)), U.is_le_to_nat(to, from)), hb)))
1038	
1039	# fast find equals the reference find, Bytes included.
1040	law fast_find_t:
1041	  for +len: U32
1042	  for +t: P.Tree<U32>
1043	  for +d: Nat
1044	  for +from: U32
1045	  for +to: U32
1046	  for +c: U32
1047	  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
1048	  for +hft: {U32.is_le(from, to) == True{} : Bool}
1049	  for +ht: {Nat.is_le(U32.to_nat(to), D.size(C.BT(len, t))) == True{} : Bool}
1050	  for +hc: {U32.is_lt(c, 256) == True{} : Bool}
1051	  {FA.find(C.BT(len, t), from, to, c) == B.find(C.BT(len, t), from, to, c) : D.Bytes & U32}
1052	
1053	def fast_find_t(len, t, d, from, to, c, h, hft, ht, hc):
1054	  +rc = FA.rep(c)
1055	  +MN = U32.min(FG(FA.words(from, to), U32.is_zero(M0(t, from, rc)), (from >> 2n : U32), M0(t, from, rc), rc, t), to)
1056	  +SN = Pair.snd(D.Bytes, U32, B.find(C.BT(len, t), from, to, c))
1057	  %Equal.sym(D.Bytes & U32, FA.find(C.BT(len, t), from, to, c), (C.BT(len, t), MN), fast_eq(len, t, from, to, c)) :
1058	    {_ == B.find(C.BT(len, t), from, to, c) : D.Bytes & U32}
1059	  %Equal.sym(D.Bytes & U32, B.find(C.BT(len, t), from, to, c), (C.BT(len, t), SN), F.find_pair_t(len, t, from, to, c)) :
1060	    {(C.BT(len, t), MN) == _ : D.Bytes & U32}
1061	  Equal.cong(U32, D.Bytes & U32, y => (C.BT(len, t), y), MN, SN,
1062	    U.to_nat_inj(MN, SN, Equal.trans(Nat, U32.to_nat(MN), D.first(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c), U32.to_nat(SN),
1063	      fview_go(U32.is_le(to, from), len, t, d, from, to, c, h, hft, ht, hc, {==}),
1064	      Equal.sym(Nat, U32.to_nat(SN), D.first(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c), F.find_view_t(len, t, d, from, to, c, h, hft, ht, hc)))))