proof_list.bend

lawful-bytes@0.1.1.0 · 526 lines · 26 definitions

1import Base
2import lawful-bytes@0.1.1.0/defs.bend as D
3import lawful-words@0.1.0.0/proof_nat.bend as WN
4import 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
18law pl_ft:
19  for e: {False{} == True{} : Bool}
20  Empty
21
22def pl_ft(e):
23  %e : Bool.pick(Type, _, Empty, Unit)
24  Unit{}
25
26law pl_tf:
27  for e: {True{} == False{} : Bool}
28  Empty
29
30def pl_tf(e):
31  %e : Bool.pick(Type, _, Unit, Empty)
32  Unit{}
33
34# k < 0 is impossible.
35law pl_lt0:
36  for +k: Nat
37  for +e: {Nat.is_lt(k, 0n) == True{} : Bool}
38  Empty
39
40def pl_lt0(k, e):
41  match k:
42    case 0n:
43      pl_ft(e)
44    case 1n+p:
45      pl_ft(e)
46
47law 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
53def 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
60law 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
66def 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.
74law 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
80def pl_le0_and(n, b, e):
81  match n:
82    case 0n:
83      e
84    case 1n+p:
85      e
86
87law pl_u32_eq_refl:
88  for +a: U32
89  {U32.is_eq(a, a) == True{} : Bool}
90
91def 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
98law 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
105def 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.
113law 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
119def 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
130law 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
142def 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.
150law 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
158def 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
170law 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
182def 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.
192law 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
200def 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
213law 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
222def 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.
243law 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
253def 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.
273law 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
283def 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
301law 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
307def 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
322law list_eq_refl:
323  for +xs: List<&2, U32>
324  {D.list_eq(xs, xs) == True{} : Bool}
325
326def 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
338law 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
345def 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
357law 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
370def 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
377law 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
386def 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
398law 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
411def 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
420law 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
429def 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
442law 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
452def 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
472law 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
483def 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
502law 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
513def 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)