1	import Base
2	import ./defs.bend as D
3	import lawful-words@0.1.0.0/proof_nat.bend as WN
4	import lawful-words@0.1.0.0/proof_u32.bend as WU
5	
6	# The pure list laws: first/first2 (search answers) and list_eq. Every
7	# variable is reusable, so PROOF.bend can forward the laws here.
8	#
9	# first(xs, from, to, c) is from + run_len(take(drop(xs, from), to - from)).
10	# For xs = x <> rest, from = 1+f and to = 1+t it computes to
11	# 1 + first(rest, f, t, c) (and to 1 + first(rest, f, 0n, c) for to = 0n), so
12	# every law goes by induction on xs and from down to from = 0n, where it is a
13	# fact about run_len(take(xs, to)) (the pl_r* and pl_r2* lemmas).
14	
15	# Bool and Nat
16	# ============
17	
18	law pl_ft:
19	  for e: {False{} == True{} : Bool}
20	  Empty
21	
22	def pl_ft(e):
23	  %e : Bool.pick(Type, _, Empty, Unit)
24	  Unit{}
25	
26	law pl_tf:
27	  for e: {True{} == False{} : Bool}
28	  Empty
29	
30	def pl_tf(e):
31	  %e : Bool.pick(Type, _, Unit, Empty)
32	  Unit{}
33	
34	# k < 0 is impossible.
35	law pl_lt0:
36	  for +k: Nat
37	  for +e: {Nat.is_lt(k, 0n) == True{} : Bool}
38	  Empty
39	
40	def pl_lt0(k, e):
41	  match k:
42	    case 0n:
43	      pl_ft(e)
44	    case 1n+p:
45	      pl_ft(e)
46	
47	law pl_and_l:
48	  for +a: Bool
49	  for +b: Bool
50	  for +e: {Bool.and(a, b) == True{} : Bool}
51	  {a == True{} : Bool}
52	
53	def pl_and_l(a, b, e):
54	  match a:
55	    case True{}:
56	      {==}
57	    case False{}:
58	      Empty.absurd({False{} == True{} : Bool}, pl_ft(e))
59	
60	law pl_and_r:
61	  for +a: Bool
62	  for +b: Bool
63	  for +e: {Bool.and(a, b) == True{} : Bool}
64	  {b == True{} : Bool}
65	
66	def pl_and_r(a, b, e):
67	  match a:
68	    case True{}:
69	      e
70	    case False{}:
71	      Empty.absurd({b == True{} : Bool}, pl_ft(e))
72	
73	# 0 <= n, inside a conjunction.
74	law pl_le0_and:
75	  for +n: Nat
76	  for +b: Bool
77	  for +e: {b == True{} : Bool}
78	  {(Nat.is_le(0n, n) && b) == True{} : Bool}
79	
80	def pl_le0_and(n, b, e):
81	  match n:
82	    case 0n:
83	      e
84	    case 1n+p:
85	      e
86	
87	law pl_u32_eq_refl:
88	  for +a: U32
89	  {U32.is_eq(a, a) == True{} : Bool}
90	
91	def pl_u32_eq_refl(a):
92	  Equal.trans(Bool, U32.is_eq(a, a), Nat.is_eq(U32.to_nat(a), U32.to_nat(a)), True{},
93	    WU.is_eq_to_nat(a, a), WN.eq_refl(U32.to_nat(a)))
94	
95	# run_len over a prefix (from = 0n)
96	# ================================
97	
98	law pl_r_step_le:
99	  for +z: Bool
100	  for +r: Nat
101	  for +p: Nat
102	  for +h: {Nat.is_le(r, p) == True{} : Bool}
103	  {Nat.is_le(Bool.pick(Nat, z, 0n, 1n+r), 1n+p) == True{} : Bool}
104	
105	def pl_r_step_le(z, r, p, h):
106	  match z:
107	    case True{}:
108	      {==}
109	    case False{}:
110	      h
111	
112	# The run is no longer than the prefix.
113	law pl_r_le:
114	  for +zs: List<&2, U32>
115	  for +n: Nat
116	  for +c: U32
117	  {Nat.is_le(D.run_len(List.take(&2, U32, zs, n), c), n) == True{} : Bool}
118	
119	def pl_r_le(zs, n, c):
120	  match zs n:
121	    case Nil{} 0n:
122	      {==}
123	    case Nil{} 1n+p:
124	      {==}
125	    case Con{x, t} 0n:
126	      {==}
127	    case Con{x, t} 1n+p:
128	      pl_r_step_le(U32.is_eq(x, c), D.run_len(List.take(&2, U32, t, p), c), p, pl_r_le(t, p, c))
129	
130	law pl_r_hit_step:
131	  for +x: U32
132	  for +t: List<&2, U32>
133	  for +c: U32
134	  for +r: Nat
135	  for +p: Nat
136	  for +z: Bool
137	  for +hz: {U32.is_eq(x, c) == z : Bool}
138	  for +hlt: {Nat.is_lt(Bool.pick(Nat, z, 0n, 1n+r), 1n+p) == True{} : Bool}
139	  for ih: {Nat.is_lt(r, p) == True{} : Bool} -> {D.has(t, r, c) == True{} : Bool}
140	  {D.has(Con{x, t}, Bool.pick(Nat, z, 0n, 1n+r), c) == True{} : Bool}
141	
142	def pl_r_hit_step(x, t, c, r, p, z, hz, hlt, ih):
143	  match z:
144	    case True{}:
145	      hz
146	    case False{}:
147	      ih(hlt)
148	
149	# Short of the end, the run stops at a c.
150	law pl_r_hit:
151	  for +zs: List<&2, U32>
152	  for +n: Nat
153	  for +c: U32
154	  for +ht: {Nat.is_le(n, List.length(&2, U32, zs)) == True{} : Bool}
155	  for +hlt: {Nat.is_lt(D.run_len(List.take(&2, U32, zs, n), c), n) == True{} : Bool}
156	  {D.has(zs, D.run_len(List.take(&2, U32, zs, n), c), c) == True{} : Bool}
157	
158	def pl_r_hit(zs, n, c, ht, hlt):
159	  match zs n:
160	    case Nil{} 0n:
161	      Empty.absurd({D.has(Nil{}, 0n, c) == True{} : Bool}, pl_ft(hlt))
162	    case Nil{} 1n+p:
163	      Empty.absurd({D.has(Nil{}, 0n, c) == True{} : Bool}, pl_ft(ht))
164	    case Con{x, t} 0n:
165	      Empty.absurd({D.has(Con{x, t}, 0n, c) == True{} : Bool}, pl_ft(hlt))
166	    case Con{x, t} 1n+p:
167	      pl_r_hit_step(x, t, c, D.run_len(List.take(&2, U32, t, p), c), p, U32.is_eq(x, c), {==}, hlt,
168	        h => pl_r_hit(t, p, c, ht, h))
169	
170	law pl_r_miss_step:
171	  for +x: U32
172	  for +t: List<&2, U32>
173	  for +c: U32
174	  for +r: Nat
175	  for +z: Bool
176	  for +k: Nat
177	  for +hz: {U32.is_eq(x, c) == z : Bool}
178	  for +hk: {Nat.is_lt(k, Bool.pick(Nat, z, 0n, 1n+r)) == True{} : Bool}
179	  for ih: @k2: Nat -> {Nat.is_lt(k2, r) == True{} : Bool} -> {D.has(t, k2, c) == False{} : Bool}
180	  {D.has(Con{x, t}, k, c) == False{} : Bool}
181	
182	def pl_r_miss_step(x, t, c, r, z, k, hz, hk, ih):
183	  match z k:
184	    case True{} k:
185	      Empty.absurd({D.has(Con{x, t}, k, c) == False{} : Bool}, pl_lt0(k, hk))
186	    case False{} 0n:
187	      hz
188	    case False{} 1n+k2:
189	      ih(k2, hk)
190	
191	# Before the end of the run, no c.
192	law pl_r_miss:
193	  for +zs: List<&2, U32>
194	  for +n: Nat
195	  for +c: U32
196	  for +k: Nat
197	  for +hk: {Nat.is_lt(k, D.run_len(List.take(&2, U32, zs, n), c)) == True{} : Bool}
198	  {D.has(zs, k, c) == False{} : Bool}
199	
200	def pl_r_miss(zs, n, c, k, hk):
201	  match zs n:
202	    case Nil{} n:
203	      {==}
204	    case Con{x, t} 0n:
205	      Empty.absurd({D.has(Con{x, t}, k, c) == False{} : Bool}, pl_lt0(k, hk))
206	    case Con{x, t} 1n+p:
207	      pl_r_miss_step(x, t, c, D.run_len(List.take(&2, U32, t, p), c), U32.is_eq(x, c), k, {==}, hk,
208	        k2 => h => pl_r_miss(t, p, c, k2, h))
209	
210	# The search laws
211	# ===============
212	
213	law first_range:
214	  for +xs: List<&2, U32>
215	  for +from: Nat
216	  for +to: Nat
217	  for +c: U32
218	  for +hft: {Nat.is_le(from, to) == True{} : Bool}
219	  for +ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
220	  {(Nat.is_le(from, D.first(xs, from, to, c)) && Nat.is_le(D.first(xs, from, to, c), to)) == True{} : Bool}
221	
222	def first_range(xs, from, to, c, hft, ht):
223	  match xs from to:
224	    case Nil{} 0n 0n:
225	      {==}
226	    case Nil{} 0n 1n+t:
227	      Empty.absurd({(Nat.is_le(0n, D.first(Nil{}, 0n, 1n+t, c)) && Nat.is_le(D.first(Nil{}, 0n, 1n+t, c), 1n+t)) == True{} : Bool}, pl_ft(ht))
228	    case Nil{} 1n+f 0n:
229	      Empty.absurd({(Nat.is_le(1n+f, D.first(Nil{}, 1n+f, 0n, c)) && Nat.is_le(D.first(Nil{}, 1n+f, 0n, c), 0n)) == True{} : Bool}, pl_ft(hft))
230	    case Nil{} 1n+f 1n+t:
231	      Empty.absurd({(Nat.is_le(1n+f, D.first(Nil{}, 1n+f, 1n+t, c)) && Nat.is_le(D.first(Nil{}, 1n+f, 1n+t, c), 1n+t)) == True{} : Bool}, pl_ft(ht))
232	    case Con{x, rest} 0n 0n:
233	      {==}
234	    case Con{x, rest} 0n 1n+t:
235	      pl_le0_and(D.first(Con{x, rest}, 0n, 1n+t, c), Nat.is_le(D.first(Con{x, rest}, 0n, 1n+t, c), 1n+t),
236	        pl_r_le(Con{x, rest}, 1n+t, c))
237	    case Con{x, rest} 1n+f 0n:
238	      Empty.absurd({(Nat.is_le(1n+f, D.first(Con{x, rest}, 1n+f, 0n, c)) && Nat.is_le(D.first(Con{x, rest}, 1n+f, 0n, c), 0n)) == True{} : Bool}, pl_ft(hft))
239	    case Con{x, rest} 1n+f 1n+t:
240	      first_range(rest, f, t, c, hft, ht)
241	
242	# Below to, the answer holds c.
243	law first_hit:
244	  for +xs: List<&2, U32>
245	  for +from: Nat
246	  for +to: Nat
247	  for +c: U32
248	  for +hft: {Nat.is_le(from, to) == True{} : Bool}
249	  for +ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
250	  for +hlt: {Nat.is_lt(D.first(xs, from, to, c), to) == True{} : Bool}
251	  {D.has(xs, D.first(xs, from, to, c), c) == True{} : Bool}
252	
253	def first_hit(xs, from, to, c, hft, ht, hlt):
254	  match xs from to:
255	    case Nil{} 0n 0n:
256	      Empty.absurd({D.has(Nil{}, D.first(Nil{}, 0n, 0n, c), c) == True{} : Bool}, pl_ft(hlt))
257	    case Nil{} 0n 1n+t:
258	      Empty.absurd({D.has(Nil{}, D.first(Nil{}, 0n, 1n+t, c), c) == True{} : Bool}, pl_ft(ht))
259	    case Nil{} 1n+f 0n:
260	      Empty.absurd({D.has(Nil{}, D.first(Nil{}, 1n+f, 0n, c), c) == True{} : Bool}, pl_ft(hft))
261	    case Nil{} 1n+f 1n+t:
262	      Empty.absurd({D.has(Nil{}, D.first(Nil{}, 1n+f, 1n+t, c), c) == True{} : Bool}, pl_ft(ht))
263	    case Con{x, rest} 0n 0n:
264	      Empty.absurd({D.has(Con{x, rest}, D.first(Con{x, rest}, 0n, 0n, c), c) == True{} : Bool}, pl_ft(hlt))
265	    case Con{x, rest} 0n 1n+t:
266	      pl_r_hit(Con{x, rest}, 1n+t, c, ht, hlt)
267	    case Con{x, rest} 1n+f 0n:
268	      Empty.absurd({D.has(Con{x, rest}, D.first(Con{x, rest}, 1n+f, 0n, c), c) == True{} : Bool}, pl_ft(hft))
269	    case Con{x, rest} 1n+f 1n+t:
270	      first_hit(rest, f, t, c, hft, ht, hlt)
271	
272	# No index from from up to the answer holds c.
273	law first_miss:
274	  for +xs: List<&2, U32>
275	  for +from: Nat
276	  for +to: Nat
277	  for +c: U32
278	  for +k: Nat
279	  for +hk1: {Nat.is_le(from, k) == True{} : Bool}
280	  for +hk2: {Nat.is_lt(k, D.first(xs, from, to, c)) == True{} : Bool}
281	  {D.has(xs, k, c) == False{} : Bool}
282	
283	def first_miss(xs, from, to, c, k, hk1, hk2):
284	  match xs from to k:
285	    case Nil{} from to k:
286	      {==}
287	    case Con{x, rest} 0n 0n k:
288	      pl_r_miss(Con{x, rest}, 0n, c, k, hk2)
289	    case Con{x, rest} 0n 1n+t k:
290	      pl_r_miss(Con{x, rest}, 1n+t, c, k, hk2)
291	    case Con{x, rest} 1n+f to 0n:
292	      Empty.absurd({D.has(Con{x, rest}, 0n, c) == False{} : Bool}, pl_ft(hk1))
293	    case Con{x, rest} 1n+f 0n 1n+k2:
294	      first_miss(rest, f, 0n, c, k2, hk1, hk2)
295	    case Con{x, rest} 1n+f 1n+t 1n+k2:
296	      first_miss(rest, f, t, c, k2, hk1, hk2)
297	
298	# Lists compared element by element
299	# =================================
300	
301	law list_eq_true:
302	  for +xs: List<&2, U32>
303	  for +ys: List<&2, U32>
304	  for +h: {D.list_eq(xs, ys) == True{} : Bool}
305	  {xs == ys : List<&2, U32>}
306	
307	def list_eq_true(xs, ys, h):
308	  match xs ys:
309	    case Nil{} Nil{}:
310	      {==}
311	    case Con{x, xt} Con{y, yt}:
312	      +ex = WU.is_eq_true(x, y, pl_and_l(U32.is_eq(x, y), D.list_eq(xt, yt), h))
313	      +et = list_eq_true(xt, yt, pl_and_r(U32.is_eq(x, y), D.list_eq(xt, yt), h))
314	      %ex : {Con{x, xt} == Con{_, yt} : List<&2, U32>}
315	      %et : {Con{x, xt} == Con{x, _} : List<&2, U32>}
316	      {==}
317	    case Nil{} Con{y, yt}:
318	      Empty.absurd({Nil{} == Con{y, yt} : List<&2, U32>}, pl_ft(h))
319	    case Con{x, xt} Nil{}:
320	      Empty.absurd({Con{x, xt} == Nil{} : List<&2, U32>}, pl_ft(h))
321	
322	law list_eq_refl:
323	  for +xs: List<&2, U32>
324	  {D.list_eq(xs, xs) == True{} : Bool}
325	
326	def list_eq_refl(xs):
327	  match xs:
328	    case Nil{}:
329	      {==}
330	    case Con{x, t}:
331	      %Equal.sym(Bool, U32.is_eq(x, x), True{}, pl_u32_eq_refl(x)) :
332	        {Bool.and(_, D.list_eq(t, t)) == True{} : Bool}
333	      list_eq_refl(t)
334	
335	# run_len2 over a prefix (from = 0n), as for run_len
336	# ==================================================
337	
338	law pl_r2_le:
339	  for +zs: List<&2, U32>
340	  for +n: Nat
341	  for +c1: U32
342	  for +c2: U32
343	  {Nat.is_le(D.run_len2(List.take(&2, U32, zs, n), c1, c2), n) == True{} : Bool}
344	
345	def pl_r2_le(zs, n, c1, c2):
346	  match zs n:
347	    case Nil{} 0n:
348	      {==}
349	    case Nil{} 1n+p:
350	      {==}
351	    case Con{x, t} 0n:
352	      {==}
353	    case Con{x, t} 1n+p:
354	      pl_r_step_le(U32.is_eq(x, c1) || U32.is_eq(x, c2), D.run_len2(List.take(&2, U32, t, p), c1, c2), p,
355	        pl_r2_le(t, p, c1, c2))
356	
357	law pl_r2_hit_step:
358	  for +x: U32
359	  for +t: List<&2, U32>
360	  for +c1: U32
361	  for +c2: U32
362	  for +r: Nat
363	  for +p: Nat
364	  for +z: Bool
365	  for +hz: {(U32.is_eq(x, c1) || U32.is_eq(x, c2)) == z : Bool}
366	  for +hlt: {Nat.is_lt(Bool.pick(Nat, z, 0n, 1n+r), 1n+p) == True{} : Bool}
367	  for ih: {Nat.is_lt(r, p) == True{} : Bool} -> {D.has2(t, r, c1, c2) == True{} : Bool}
368	  {D.has2(Con{x, t}, Bool.pick(Nat, z, 0n, 1n+r), c1, c2) == True{} : Bool}
369	
370	def pl_r2_hit_step(x, t, c1, c2, r, p, z, hz, hlt, ih):
371	  match z:
372	    case True{}:
373	      hz
374	    case False{}:
375	      ih(hlt)
376	
377	law pl_r2_hit:
378	  for +zs: List<&2, U32>
379	  for +n: Nat
380	  for +c1: U32
381	  for +c2: U32
382	  for +ht: {Nat.is_le(n, List.length(&2, U32, zs)) == True{} : Bool}
383	  for +hlt: {Nat.is_lt(D.run_len2(List.take(&2, U32, zs, n), c1, c2), n) == True{} : Bool}
384	  {D.has2(zs, D.run_len2(List.take(&2, U32, zs, n), c1, c2), c1, c2) == True{} : Bool}
385	
386	def pl_r2_hit(zs, n, c1, c2, ht, hlt):
387	  match zs n:
388	    case Nil{} 0n:
389	      Empty.absurd({D.has2(Nil{}, 0n, c1, c2) == True{} : Bool}, pl_ft(hlt))
390	    case Nil{} 1n+p:
391	      Empty.absurd({D.has2(Nil{}, 0n, c1, c2) == True{} : Bool}, pl_ft(ht))
392	    case Con{x, t} 0n:
393	      Empty.absurd({D.has2(Con{x, t}, 0n, c1, c2) == True{} : Bool}, pl_ft(hlt))
394	    case Con{x, t} 1n+p:
395	      pl_r2_hit_step(x, t, c1, c2, D.run_len2(List.take(&2, U32, t, p), c1, c2), p,
396	        U32.is_eq(x, c1) || U32.is_eq(x, c2), {==}, hlt, h => pl_r2_hit(t, p, c1, c2, ht, h))
397	
398	law pl_r2_miss_step:
399	  for +x: U32
400	  for +t: List<&2, U32>
401	  for +c1: U32
402	  for +c2: U32
403	  for +r: Nat
404	  for +z: Bool
405	  for +k: Nat
406	  for +hz: {(U32.is_eq(x, c1) || U32.is_eq(x, c2)) == z : Bool}
407	  for +hk: {Nat.is_lt(k, Bool.pick(Nat, z, 0n, 1n+r)) == True{} : Bool}
408	  for ih: @k2: Nat -> {Nat.is_lt(k2, r) == True{} : Bool} -> {D.has2(t, k2, c1, c2) == False{} : Bool}
409	  {D.has2(Con{x, t}, k, c1, c2) == False{} : Bool}
410	
411	def pl_r2_miss_step(x, t, c1, c2, r, z, k, hz, hk, ih):
412	  match z k:
413	    case True{} k:
414	      Empty.absurd({D.has2(Con{x, t}, k, c1, c2) == False{} : Bool}, pl_lt0(k, hk))
415	    case False{} 0n:
416	      hz
417	    case False{} 1n+k2:
418	      ih(k2, hk)
419	
420	law pl_r2_miss:
421	  for +zs: List<&2, U32>
422	  for +n: Nat
423	  for +c1: U32
424	  for +c2: U32
425	  for +k: Nat
426	  for +hk: {Nat.is_lt(k, D.run_len2(List.take(&2, U32, zs, n), c1, c2)) == True{} : Bool}
427	  {D.has2(zs, k, c1, c2) == False{} : Bool}
428	
429	def pl_r2_miss(zs, n, c1, c2, k, hk):
430	  match zs n:
431	    case Nil{} n:
432	      {==}
433	    case Con{x, t} 0n:
434	      Empty.absurd({D.has2(Con{x, t}, k, c1, c2) == False{} : Bool}, pl_lt0(k, hk))
435	    case Con{x, t} 1n+p:
436	      pl_r2_miss_step(x, t, c1, c2, D.run_len2(List.take(&2, U32, t, p), c1, c2),
437	        U32.is_eq(x, c1) || U32.is_eq(x, c2), k, {==}, hk, k2 => h => pl_r2_miss(t, p, c1, c2, k2, h))
438	
439	# The two-value search laws
440	# =========================
441	
442	law first2_range:
443	  for +xs: List<&2, U32>
444	  for +from: Nat
445	  for +to: Nat
446	  for +c1: U32
447	  for +c2: U32
448	  for +hft: {Nat.is_le(from, to) == True{} : Bool}
449	  for +ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
450	  {(Nat.is_le(from, D.first2(xs, from, to, c1, c2)) && Nat.is_le(D.first2(xs, from, to, c1, c2), to)) == True{} : Bool}
451	
452	def first2_range(xs, from, to, c1, c2, hft, ht):
453	  match xs from to:
454	    case Nil{} 0n 0n:
455	      {==}
456	    case Nil{} 0n 1n+t:
457	      Empty.absurd({(Nat.is_le(0n, D.first2(Nil{}, 0n, 1n+t, c1, c2)) && Nat.is_le(D.first2(Nil{}, 0n, 1n+t, c1, c2), 1n+t)) == True{} : Bool}, pl_ft(ht))
458	    case Nil{} 1n+f 0n:
459	      Empty.absurd({(Nat.is_le(1n+f, D.first2(Nil{}, 1n+f, 0n, c1, c2)) && Nat.is_le(D.first2(Nil{}, 1n+f, 0n, c1, c2), 0n)) == True{} : Bool}, pl_ft(hft))
460	    case Nil{} 1n+f 1n+t:
461	      Empty.absurd({(Nat.is_le(1n+f, D.first2(Nil{}, 1n+f, 1n+t, c1, c2)) && Nat.is_le(D.first2(Nil{}, 1n+f, 1n+t, c1, c2), 1n+t)) == True{} : Bool}, pl_ft(ht))
462	    case Con{x, rest} 0n 0n:
463	      {==}
464	    case Con{x, rest} 0n 1n+t:
465	      pl_le0_and(D.first2(Con{x, rest}, 0n, 1n+t, c1, c2), Nat.is_le(D.first2(Con{x, rest}, 0n, 1n+t, c1, c2), 1n+t),
466	        pl_r2_le(Con{x, rest}, 1n+t, c1, c2))
467	    case Con{x, rest} 1n+f 0n:
468	      Empty.absurd({(Nat.is_le(1n+f, D.first2(Con{x, rest}, 1n+f, 0n, c1, c2)) && Nat.is_le(D.first2(Con{x, rest}, 1n+f, 0n, c1, c2), 0n)) == True{} : Bool}, pl_ft(hft))
469	    case Con{x, rest} 1n+f 1n+t:
470	      first2_range(rest, f, t, c1, c2, hft, ht)
471	
472	law first2_hit:
473	  for +xs: List<&2, U32>
474	  for +from: Nat
475	  for +to: Nat
476	  for +c1: U32
477	  for +c2: U32
478	  for +hft: {Nat.is_le(from, to) == True{} : Bool}
479	  for +ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
480	  for +hlt: {Nat.is_lt(D.first2(xs, from, to, c1, c2), to) == True{} : Bool}
481	  {D.has2(xs, D.first2(xs, from, to, c1, c2), c1, c2) == True{} : Bool}
482	
483	def first2_hit(xs, from, to, c1, c2, hft, ht, hlt):
484	  match xs from to:
485	    case Nil{} 0n 0n:
486	      Empty.absurd({D.has2(Nil{}, D.first2(Nil{}, 0n, 0n, c1, c2), c1, c2) == True{} : Bool}, pl_ft(hlt))
487	    case Nil{} 0n 1n+t:
488	      Empty.absurd({D.has2(Nil{}, D.first2(Nil{}, 0n, 1n+t, c1, c2), c1, c2) == True{} : Bool}, pl_ft(ht))
489	    case Nil{} 1n+f 0n:
490	      Empty.absurd({D.has2(Nil{}, D.first2(Nil{}, 1n+f, 0n, c1, c2), c1, c2) == True{} : Bool}, pl_ft(hft))
491	    case Nil{} 1n+f 1n+t:
492	      Empty.absurd({D.has2(Nil{}, D.first2(Nil{}, 1n+f, 1n+t, c1, c2), c1, c2) == True{} : Bool}, pl_ft(ht))
493	    case Con{x, rest} 0n 0n:
494	      Empty.absurd({D.has2(Con{x, rest}, D.first2(Con{x, rest}, 0n, 0n, c1, c2), c1, c2) == True{} : Bool}, pl_ft(hlt))
495	    case Con{x, rest} 0n 1n+t:
496	      pl_r2_hit(Con{x, rest}, 1n+t, c1, c2, ht, hlt)
497	    case Con{x, rest} 1n+f 0n:
498	      Empty.absurd({D.has2(Con{x, rest}, D.first2(Con{x, rest}, 1n+f, 0n, c1, c2), c1, c2) == True{} : Bool}, pl_ft(hft))
499	    case Con{x, rest} 1n+f 1n+t:
500	      first2_hit(rest, f, t, c1, c2, hft, ht, hlt)
501	
502	law first2_miss:
503	  for +xs: List<&2, U32>
504	  for +from: Nat
505	  for +to: Nat
506	  for +c1: U32
507	  for +c2: U32
508	  for +k: Nat
509	  for +hk1: {Nat.is_le(from, k) == True{} : Bool}
510	  for +hk2: {Nat.is_lt(k, D.first2(xs, from, to, c1, c2)) == True{} : Bool}
511	  {D.has2(xs, k, c1, c2) == False{} : Bool}
512	
513	def first2_miss(xs, from, to, c1, c2, k, hk1, hk2):
514	  match xs from to k:
515	    case Nil{} from to k:
516	      {==}
517	    case Con{x, rest} 0n 0n k:
518	      pl_r2_miss(Con{x, rest}, 0n, c1, c2, k, hk2)
519	    case Con{x, rest} 0n 1n+t k:
520	      pl_r2_miss(Con{x, rest}, 1n+t, c1, c2, k, hk2)
521	    case Con{x, rest} 1n+f to 0n:
522	      Empty.absurd({D.has2(Con{x, rest}, 0n, c1, c2) == False{} : Bool}, pl_ft(hk1))
523	    case Con{x, rest} 1n+f 0n 1n+k2:
524	      first2_miss(rest, f, 0n, c1, c2, k2, hk1, hk2)
525	    case Con{x, rest} 1n+f 1n+t 1n+k2:
526	      first2_miss(rest, f, t, c1, c2, k2, hk1, hk2)