PROOF.bend

bend-osdev-algo@0.1.0.0 · 1,493 lines · 141 definitions

1import Base
2import bend-osdev-word64@0.1.0.0/word64.bend as W
3import bend-osdev-word64@0.1.0.0/LAWS.bend as WL
4import bend-osdev-word64@0.1.0.0/PROOF.bend as WP
5import bend-osdev-algo@0.1.0.0/algo.bend as A
6import bend-osdev-algo@0.1.0.0/bitmap.bend as M
7import bend-osdev-algo@0.1.0.0/bsearch.bend as S
8import bend-osdev-array@0.1.0.0/array.bend as AR
9import bend-osdev-array@0.1.0.0/LAWS.bend as AL
10import bend-osdev-array@0.1.0.0/PROOF.bend as APF
11import bend-osdev-algo@0.1.0.0/proof_u32.bend as U
12import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as Q
13import bend-osdev-algo@0.1.0.0/LAWS.bend as Laws
14
15# Contradictions
16
17def absurd.bool(b: Bool) -> Type:
18  match b:
19    case True{}:
20      Unit
21    case False{}:
22      Empty
23
24def absurd.tf(e: {True{} == False{} : Bool}) -> Empty:
25  %e : absurd.bool(_)
26  Unit{}
27
28def absurd.ft(e: {False{} == True{} : Bool}) -> Empty:
29  %Equal.sym(Bool, False{}, True{}, e) : absurd.bool(_)
30  Unit{}
31
32def absurd.nat(n: Nat) -> Type:
33  match n:
34    case 0n:
35      Empty
36    case 1n+p:
37      Unit
38
39def absurd.sz(-k: Nat, e: {1n+k == 0n : Nat}) -> Empty:
40  %e : absurd.nat(_)
41  Unit{}
42
43def absurd.maybe(m: Maybe<&2, Nat>) -> Type:
44  match m:
45    case None{}:
46      Empty
47    case Some{k}:
48      Unit
49
50def absurd.sn(-k: Nat, e: {Some{k} == None{} : Maybe<&2, Nat>}) -> Empty:
51  %e : absurd.maybe(_)
52  Unit{}
53
54def absurd.ns(-k: Nat, e: {None{} == Some{k} : Maybe<&2, Nat>}) -> Empty:
55  %Equal.sym(Maybe<&2, Nat>, None{}, Some{k}, e) : absurd.maybe(_)
56  Unit{}
57
58def maybe.get(m: Maybe<&2, Nat>) -> Nat:
59  match m:
60    case None{}:
61      0n
62    case Some{k}:
63      k
64
65def some_inj(-a: Nat, -b: Nat, e: {Some{a} == Some{b} : Maybe<&2, Nat>}) -> {a == b : Nat}:
66  Equal.cong(Maybe<&2, Nat>, Nat, m => maybe.get(m), Some{a}, Some{b}, e)
67
68# Nat
69
70def nat.le_zero(x: Nat) -> {Nat.is_le(0n, x) == True{} : Bool}:
71  match x:
72    case 0n:
73      {==}
74    case 1n+p:
75      {==}
76
77def nat.lt_zero(x: Nat) -> {Nat.is_lt(x, 0n) == False{} : Bool}:
78  match x:
79    case 0n:
80      {==}
81    case 1n+p:
82      {==}
83
84def nat.lt_irrefl(x: Nat) -> {Nat.is_lt(x, x) == False{} : Bool}:
85  match x:
86    case 0n:
87      {==}
88    case 1n+p:
89      nat.lt_irrefl(p)
90
91def nat.le_refl(x: Nat) -> {Nat.is_le(x, x) == True{} : Bool}:
92  match x:
93    case 0n:
94      {==}
95    case 1n+p:
96      nat.le_refl(p)
97
98def nat.le_succ(a: Nat, b: Nat, e: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(a, 1n+b) == True{} : Bool}:
99  match a b:
100    case 0n _:
101      {==}
102    case 1n+ap 0n:
103      Empty.absurd({Nat.is_le(1n+ap, 1n) == True{} : Bool}, absurd.ft(e))
104    case 1n+ap 1n+bp:
105      nat.le_succ(ap, bp, e)
106
107def nat.add_zero(a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
108  match a:
109    case 0n:
110      {==}
111    case 1n+p:
112      %nat.add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
113      {==}
114
115def nat.add_succ(a: Nat, -b: Nat) -> {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}:
116  match a:
117    case 0n:
118      {==}
119    case 1n+p:
120      %Equal.sym(Nat, Nat.add(p, 1n+b), 1n+Nat.add(p, b), nat.add_succ(p, b)) : {1n+_ == 2n+Nat.add(p, b) : Nat}
121      {==}
122
123# n - k + k = n, for k <= n
124def nat.sub_add(n: Nat, k: Nat, e: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.add(Nat.sub(n, k), k) == n : Nat}:
125  match n k:
126    case 0n 0n:
127      {==}
128    case 0n 1n+kp:
129      Empty.absurd({Nat.add(0n, 1n+kp) == 0n : Nat}, absurd.ft(e))
130    case 1n+np 0n:
131      nat.add_zero(1n+np)
132    case 1n+ +np 1n+ +kp:
133      %Equal.sym(Nat, Nat.add(Nat.sub(np, kp), 1n+kp), 1n+Nat.add(Nat.sub(np, kp), kp), nat.add_succ(Nat.sub(np, kp), kp)) : {_ == 1n+np : Nat}
134      %nat.sub_add(np, kp, e) : {1n+Nat.add(Nat.sub(np, kp), kp) == 1n+_ : Nat}
135      {==}
136
137def nat.sub_le(n: Nat, k: Nat) -> {Nat.is_le(Nat.sub(n, k), n) == True{} : Bool}:
138  match n k:
139    case 0n _:
140      {==}
141    case 1n+np 0n:
142      nat.le_refl(np)
143    case 1n+ +np 1n+ +kp:
144      nat.le_succ(Nat.sub(np, kp), np, nat.sub_le(np, kp))
145
146# k <= l <= n gives k + (n - l) <= n
147def nat.add_sub_le(k: Nat, l: Nat, n: Nat, e: {Nat.is_le(k, l) == True{} : Bool}, f: {Nat.is_le(l, n) == True{} : Bool}) -> {Nat.is_le(Nat.add(k, Nat.sub(n, l)), n) == True{} : Bool}:
148  match k l n:
149    case 0n _ _:
150      nat.sub_le(n, l)
151    case 1n+kp 0n _:
152      Empty.absurd({Nat.is_le(Nat.add(1n+kp, Nat.sub(n, 0n)), n) == True{} : Bool}, absurd.ft(e))
153    case 1n+kp 1n+lp 0n:
154      Empty.absurd({Nat.is_le(Nat.add(1n+kp, 0n), 0n) == True{} : Bool}, absurd.ft(f))
155    case 1n+kp 1n+lp 1n+np:
156      nat.add_sub_le(kp, lp, np, e, f)
157
158# Words: popcount
159
160def bitw.popcount_le(n: Nat, w: Word(n)) -> {Nat.is_le(A.bitw.popcount(n, w), n) == True{} : Bool}:
161  match n:
162    case 0n:
163      {==}
164    case 1n+ +p:
165      match w:
166        case WCon{True{}, t}:
167          bitw.popcount_le(p, t)
168        case WCon{False{}, +t}:
169          nat.le_succ(A.bitw.popcount(p, t), p, bitw.popcount_le(p, t))
170
171def bitw.popcount_not(n: Nat, w: Word(n)) -> {Nat.add(A.bitw.popcount(n, w), A.bitw.popcount(n, Word.not(n, w))) == n : Nat}:
172  match n:
173    case 0n:
174      {==}
175    case 1n+ +p:
176      match w:
177        case WCon{True{}, +t}:
178          %bitw.popcount_not(p, t) : {1n+Nat.add(A.bitw.popcount(p, t), A.bitw.popcount(p, Word.not(p, t))) == 1n+_ : Nat}
179          {==}
180        case WCon{False{}, +t}:
181          %Equal.sym(Nat, Nat.add(A.bitw.popcount(p, t), 1n+A.bitw.popcount(p, Word.not(p, t))), 1n+Nat.add(A.bitw.popcount(p, t), A.bitw.popcount(p, Word.not(p, t))), nat.add_succ(A.bitw.popcount(p, t), A.bitw.popcount(p, Word.not(p, t)))) : {_ == 1n+p : Nat}
182          %bitw.popcount_not(p, t) : {1n+Nat.add(A.bitw.popcount(p, t), A.bitw.popcount(p, Word.not(p, t))) == 1n+_ : Nat}
183          {==}
184
185# Words: the bit a 1-based position names, and the positions below and above
186
187def bitw.at1(n: Nat, w: Word(n), m: Nat) -> Bool:
188  match m:
189    case 0n:
190      False{}
191    case 1n+k:
192      A.bitw.test(n, w, k)
193
194def nat.pos(m: Nat) -> Bool:
195  match m:
196    case 0n:
197      False{}
198    case 1n+k:
199      True{}
200
201# j lies below the lowest set bit (every j does when there is none)
202def bitw.below(j: Nat, m: Nat) -> Bool:
203  match m:
204    case 0n:
205      True{}
206    case 1n+k:
207      Nat.is_lt(j, k)
208
209# j lies above the highest set bit (every j does when there is none)
210def bitw.above(j: Nat, m: Nat) -> Bool:
211  match m:
212    case 0n:
213      True{}
214    case 1n+k:
215      Nat.is_lt(k, j)
216
217# Words: ffs
218
219def bitw.ffs_set.h(p: Nat, -t: Word(p), m: Nat, ih: {bitw.at1(p, t, m) == nat.pos(m) : Bool}) -> {bitw.at1(1n+p, WCon{False{}, t}, A.bitw.ffs.step(False{}, m)) == nat.pos(A.bitw.ffs.step(False{}, m)) : Bool}:
220  match m:
221    case 0n:
222      {==}
223    case 1n+k:
224      ih
225
226def bitw.ffs_set(n: Nat, w: Word(n)) -> {bitw.at1(n, w, A.bitw.ffs(n, w)) == nat.pos(A.bitw.ffs(n, w)) : Bool}:
227  match n:
228    case 0n:
229      {==}
230    case 1n+ +p:
231      match w:
232        case WCon{True{}, t}:
233          {==}
234        case WCon{False{}, +t}:
235          bitw.ffs_set.h(p, t, A.bitw.ffs(p, t), bitw.ffs_set(p, t))
236
237def bitw.ffs_low.z(m: Nat) -> {Bool.and(bitw.below(0n, A.bitw.ffs.step(False{}, m)), False{}) == False{} : Bool}:
238  match m:
239    case 0n:
240      {==}
241    case 1n+k:
242      {==}
243
244def bitw.ffs_low.s(-p: Nat, -t: Word(p), m: Nat, -j: Nat, ih: {Bool.and(bitw.below(j, m), A.bitw.test(p, t, j)) == False{} : Bool}) -> {Bool.and(bitw.below(1n+j, A.bitw.ffs.step(False{}, m)), A.bitw.test(1n+p, WCon{False{}, t}, 1n+j)) == False{} : Bool}:
245  match m:
246    case 0n:
247      ih
248    case 1n+k:
249      ih
250
251def bitw.ffs_low(n: Nat, w: Word(n), j: Nat) -> {Bool.and(bitw.below(j, A.bitw.ffs(n, w)), A.bitw.test(n, w, j)) == False{} : Bool}:
252  match n:
253    case 0n:
254      {==}
255    case 1n+ +p:
256      match w j:
257        case WCon{True{}, t} 0n:
258          {==}
259        case WCon{True{}, t} 1n+q:
260          {==}
261        case WCon{False{}, t} 0n:
262          bitw.ffs_low.z(A.bitw.ffs(p, t))
263        case WCon{False{}, +t} 1n+ +q:
264          bitw.ffs_low.s(p, t, A.bitw.ffs(p, t), q, bitw.ffs_low(p, t, q))
265
266def bitw.ffs_zero.h(m: Nat, e: {A.bitw.ffs.step(False{}, m) == 0n : Nat}) -> {m == 0n : Nat}:
267  match m:
268    case 0n:
269      {==}
270    case 1n+k:
271      Empty.absurd({1n+k == 0n : Nat}, absurd.sz(1n+k, e))
272
273def bitw.ffs_zero(n: Nat, w: Word(n), e: {A.bitw.ffs(n, w) == 0n : Nat}) -> {w == Word.zero(n) : Word(n)}:
274  match n:
275    case 0n:
276      match w:
277        case WNil{}:
278          {==}
279    case 1n+ +p:
280      match w:
281        case WCon{True{}, t}:
282          Empty.absurd({WCon{True{}, t} == Word.zero(1n+p) : Word(1n+p)}, absurd.sz(0n, e))
283        case WCon{False{}, +t}:
284          %bitw.ffs_zero(p, t, bitw.ffs_zero.h(A.bitw.ffs(p, t), e)) : {WCon{False{}, t} == WCon{False{}, _} : Word(1n+p)}
285          {==}
286
287# Words: fls
288
289def bitw.fls_set.h(p: Nat, -t: Word(p), m: Nat, b: Bool, ih: {bitw.at1(p, t, m) == nat.pos(m) : Bool}) -> {bitw.at1(1n+p, WCon{b, t}, A.bitw.fls.step(m, b)) == nat.pos(A.bitw.fls.step(m, b)) : Bool}:
290  match m:
291    case 0n:
292      match b:
293        case True{}:
294          {==}
295        case False{}:
296          {==}
297    case 1n+k:
298      ih
299
300def bitw.fls_set(n: Nat, w: Word(n)) -> {bitw.at1(n, w, A.bitw.fls(n, w)) == nat.pos(A.bitw.fls(n, w)) : Bool}:
301  match n:
302    case 0n:
303      {==}
304    case 1n+ +p:
305      match w:
306        case WCon{b, +t}:
307          bitw.fls_set.h(p, t, A.bitw.fls(p, t), b, bitw.fls_set(p, t))
308
309def bitw.fls_high.z(m: Nat, b: Bool) -> {Bool.and(bitw.above(0n, A.bitw.fls.step(m, b)), b) == False{} : Bool}:
310  match m:
311    case 0n:
312      match b:
313        case True{}:
314          {==}
315        case False{}:
316          {==}
317    case 1n+k:
318      {==}
319
320def bitw.fls_high.s(-p: Nat, -t: Word(p), m: Nat, b: Bool, -j: Nat, ih: {Bool.and(bitw.above(j, m), A.bitw.test(p, t, j)) == False{} : Bool}) -> {Bool.and(bitw.above(1n+j, A.bitw.fls.step(m, b)), A.bitw.test(1n+p, WCon{b, t}, 1n+j)) == False{} : Bool}:
321  match m:
322    case 0n:
323      match b:
324        case True{}:
325          ih
326        case False{}:
327          ih
328    case 1n+k:
329      ih
330
331def bitw.fls_high(n: Nat, w: Word(n), j: Nat) -> {Bool.and(bitw.above(j, A.bitw.fls(n, w)), A.bitw.test(n, w, j)) == False{} : Bool}:
332  match n:
333    case 0n:
334      {==}
335    case 1n+ +p:
336      match w j:
337        case WCon{+b, t} 0n:
338          bitw.fls_high.z(A.bitw.fls(p, t), b)
339        case WCon{+b, +t} 1n+ +q:
340          bitw.fls_high.s(p, t, A.bitw.fls(p, t), b, q, bitw.fls_high(p, t, q))
341
342def bitw.fls_zero.m(m: Nat, b: Bool, e: {A.bitw.fls.step(m, b) == 0n : Nat}) -> {m == 0n : Nat}:
343  match m:
344    case 0n:
345      {==}
346    case 1n+k:
347      Empty.absurd({1n+k == 0n : Nat}, absurd.sz(1n+k, e))
348
349def bitw.fls_zero.b(m: Nat, b: Bool, e: {A.bitw.fls.step(m, b) == 0n : Nat}) -> {b == False{} : Bool}:
350  match m:
351    case 0n:
352      match b:
353        case True{}:
354          Empty.absurd({True{} == False{} : Bool}, absurd.sz(0n, e))
355        case False{}:
356          {==}
357    case 1n+k:
358      Empty.absurd({b == False{} : Bool}, absurd.sz(1n+k, e))
359
360def bitw.fls_zero(n: Nat, w: Word(n), e: {A.bitw.fls(n, w) == 0n : Nat}) -> {w == Word.zero(n) : Word(n)}:
361  match n:
362    case 0n:
363      match w:
364        case WNil{}:
365          {==}
366    case 1n+ +p:
367      match w:
368        case WCon{+b, +t}:
369          +e2 = e
370          %bitw.fls_zero(p, t, bitw.fls_zero.m(A.bitw.fls(p, t), b, e2)) : {WCon{b, t} == WCon{False{}, _} : Word(1n+p)}
371          %bitw.fls_zero.b(A.bitw.fls(p, t), b, e2) : {WCon{b, t} == WCon{_, t} : Word(1n+p)}
372          {==}
373
374def bitw.fls_le.h(m: Nat, b: Bool, +p: Nat, ih: {Nat.is_le(m, p) == True{} : Bool}) -> {Nat.is_le(A.bitw.fls.step(m, b), 1n+p) == True{} : Bool}:
375  match m:
376    case 0n:
377      match b:
378        case True{}:
379          nat.le_zero(p)
380        case False{}:
381          {==}
382    case 1n+k:
383      ih
384
385def bitw.fls_le(n: Nat, w: Word(n)) -> {Nat.is_le(A.bitw.fls(n, w), n) == True{} : Bool}:
386  match n:
387    case 0n:
388      {==}
389    case 1n+ +p:
390      match w:
391        case WCon{b, +t}:
392          bitw.fls_le.h(A.bitw.fls(p, t), b, p, bitw.fls_le(p, t))
393
394# ffs <= fls
395def bitw.ffs_le_fls.f(a: Nat, m: Nat, ih: {Nat.is_le(a, m) == True{} : Bool}) -> {Nat.is_le(A.bitw.ffs.step(False{}, a), A.bitw.fls.step(m, False{})) == True{} : Bool}:
396  match a m:
397    case 0n _:
398      nat.le_zero(A.bitw.fls.step(m, False{}))
399    case 1n+i 0n:
400      Empty.absurd({Nat.is_le(2n+i, 0n) == True{} : Bool}, absurd.ft(ih))
401    case 1n+i 1n+k:
402      ih
403
404def bitw.ffs_le_fls.t(m: Nat) -> {Nat.is_le(1n, A.bitw.fls.step(m, True{})) == True{} : Bool}:
405  match m:
406    case 0n:
407      {==}
408    case 1n+k:
409      {==}
410
411def bitw.ffs_le_fls(n: Nat, w: Word(n)) -> {Nat.is_le(A.bitw.ffs(n, w), A.bitw.fls(n, w)) == True{} : Bool}:
412  match n:
413    case 0n:
414      {==}
415    case 1n+ +p:
416      match w:
417        case WCon{True{}, t}:
418          bitw.ffs_le_fls.t(A.bitw.fls(p, t))
419        case WCon{False{}, +t}:
420          bitw.ffs_le_fls.f(A.bitw.ffs(p, t), A.bitw.fls(p, t), bitw.ffs_le_fls(p, t))
421
422# Words: ctz
423
424def bitw.ctz_spec(+n: Nat, m: Nat) -> Nat:
425  match m:
426    case 0n:
427      n
428    case 1n+k:
429      k
430
431def bitw.ctz_ffs.h(+p: Nat, c: Nat, m: Nat, ih: {c == bitw.ctz_spec(p, m) : Nat}) -> {1n+c == bitw.ctz_spec(1n+p, A.bitw.ffs.step(False{}, m)) : Nat}:
432  match m:
433    case 0n:
434      %ih : {1n+c == 1n+_ : Nat}
435      {==}
436    case 1n+k:
437      %ih : {1n+c == 1n+_ : Nat}
438      {==}
439
440def bitw.ctz_ffs(n: Nat, w: Word(n)) -> {A.bitw.ctz(n, w) == bitw.ctz_spec(n, A.bitw.ffs(n, w)) : Nat}:
441  match n:
442    case 0n:
443      {==}
444    case 1n+ +p:
445      match w:
446        case WCon{True{}, t}:
447          {==}
448        case WCon{False{}, +t}:
449          bitw.ctz_ffs.h(p, A.bitw.ctz(p, t), A.bitw.ffs(p, t), bitw.ctz_ffs(p, t))
450
451# Words: from a 0-based index back to the 1-based position
452
453def bitw.index_some(m: Nat, -k: Nat, e: {A.bitw.index(m) == Some{k} : Maybe<&2, Nat>}) -> {m == 1n+k : Nat}:
454  match m:
455    case 0n:
456      Empty.absurd({0n == 1n+k : Nat}, absurd.ns(k, e))
457    case 1n+i:
458      %some_inj(i, k, e) : {1n+i == 1n+_ : Nat}
459      {==}
460
461def bitw.index_none(m: Nat, e: {A.bitw.index(m) == None{} : Maybe<&2, Nat>}) -> {m == 0n : Nat}:
462  match m:
463    case 0n:
464      {==}
465    case 1n+i:
466      Empty.absurd({1n+i == 0n : Nat}, absurd.sn(i, e))
467
468# Words: the laws, at any width
469
470def bitw.first_set_is_set(+n: Nat, +w: Word(n), +k: Nat, e: {A.bitw.index(A.bitw.ffs(n, w)) == Some{k} : Maybe<&2, Nat>}) -> {A.bitw.test(n, w, k) == True{} : Bool}:
471  %bitw.index_some(A.bitw.ffs(n, w), k, e) : {bitw.at1(n, w, _) == nat.pos(_) : Bool}
472  bitw.ffs_set(n, w)
473
474def bitw.first_set_lowest(+n: Nat, +w: Word(n), +k: Nat, +j: Nat, e: {A.bitw.index(A.bitw.ffs(n, w)) == Some{k} : Maybe<&2, Nat>}, l: {Nat.is_lt(j, k) == True{} : Bool}) -> {A.bitw.test(n, w, j) == False{} : Bool}:
475  %l : {Bool.and(_, A.bitw.test(n, w, j)) == False{} : Bool}
476  %bitw.index_some(A.bitw.ffs(n, w), k, e) : {Bool.and(bitw.below(j, _), A.bitw.test(n, w, j)) == False{} : Bool}
477  bitw.ffs_low(n, w, j)
478
479def bitw.first_set_none(+n: Nat, +w: Word(n), e: {A.bitw.index(A.bitw.ffs(n, w)) == None{} : Maybe<&2, Nat>}) -> {w == Word.zero(n) : Word(n)}:
480  bitw.ffs_zero(n, w, bitw.index_none(A.bitw.ffs(n, w), e))
481
482def bitw.last_set_is_set(+n: Nat, +w: Word(n), +k: Nat, e: {A.bitw.index(A.bitw.fls(n, w)) == Some{k} : Maybe<&2, Nat>}) -> {A.bitw.test(n, w, k) == True{} : Bool}:
483  %bitw.index_some(A.bitw.fls(n, w), k, e) : {bitw.at1(n, w, _) == nat.pos(_) : Bool}
484  bitw.fls_set(n, w)
485
486def bitw.last_set_highest(+n: Nat, +w: Word(n), +k: Nat, +j: Nat, e: {A.bitw.index(A.bitw.fls(n, w)) == Some{k} : Maybe<&2, Nat>}, l: {Nat.is_lt(k, j) == True{} : Bool}) -> {A.bitw.test(n, w, j) == False{} : Bool}:
487  %l : {Bool.and(_, A.bitw.test(n, w, j)) == False{} : Bool}
488  %bitw.index_some(A.bitw.fls(n, w), k, e) : {Bool.and(bitw.above(j, _), A.bitw.test(n, w, j)) == False{} : Bool}
489  bitw.fls_high(n, w, j)
490
491def bitw.last_set_none(+n: Nat, +w: Word(n), e: {A.bitw.index(A.bitw.fls(n, w)) == None{} : Maybe<&2, Nat>}) -> {w == Word.zero(n) : Word(n)}:
492  bitw.fls_zero(n, w, bitw.index_none(A.bitw.fls(n, w), e))
493
494def bitw.ctz_first_set(+n: Nat, +w: Word(n), +k: Nat, e: {A.bitw.index(A.bitw.ffs(n, w)) == Some{k} : Maybe<&2, Nat>}) -> {A.bitw.ctz(n, w) == k : Nat}:
495  %bitw.index_some(A.bitw.ffs(n, w), k, e) : {A.bitw.ctz(n, w) == bitw.ctz_spec(n, _) : Nat}
496  bitw.ctz_ffs(n, w)
497
498# with the highest set bit at k, k <= m in a word of width 1 + m
499def bitw.last_le(+m: Nat, +w: Word(1n+m), +k: Nat, e: {A.bitw.index(A.bitw.fls(1n+m, w)) == Some{k} : Maybe<&2, Nat>}) -> {Nat.is_le(k, m) == True{} : Bool}:
500  %bitw.index_some(A.bitw.fls(1n+m, w), k, e) : {Nat.is_le(_, 1n+m) == True{} : Bool}
501  bitw.fls_le(1n+m, w)
502
503def bitw.clz_last_set(+m: Nat, +w: Word(1n+m), +k: Nat, +e: {A.bitw.index(A.bitw.fls(1n+m, w)) == Some{k} : Maybe<&2, Nat>}) -> {Nat.add(A.bitw.clz(1n+m, w), k) == m : Nat}:
504  %Equal.sym(Nat, A.bitw.fls(1n+m, w), 1n+k, bitw.index_some(A.bitw.fls(1n+m, w), k, e)) : {Nat.add(Nat.sub(1n+m, _), k) == m : Nat}
505  nat.sub_add(m, k, bitw.last_le(m, w, k, e))
506
507def bitw.first_le_last(+n: Nat, +w: Word(n), +i: Nat, +k: Nat, e: {A.bitw.index(A.bitw.ffs(n, w)) == Some{i} : Maybe<&2, Nat>}, f: {A.bitw.index(A.bitw.fls(n, w)) == Some{k} : Maybe<&2, Nat>}) -> {Nat.is_le(i, k) == True{} : Bool}:
508  %bitw.index_some(A.bitw.ffs(n, w), i, e) : {Nat.is_le(_, 1n+k) == True{} : Bool}
509  %bitw.index_some(A.bitw.fls(n, w), k, f) : {Nat.is_le(A.bitw.ffs(n, w), _) == True{} : Bool}
510  bitw.ffs_le_fls(n, w)
511
512def bitw.ctz_clz.h(+k: Nat, +m: Nat, l: Nat, e: {Nat.is_le(1n+k, l) == True{} : Bool}, f: {Nat.is_le(l, 1n+m) == True{} : Bool}) -> {Nat.is_le(Nat.add(k, Nat.sub(1n+m, l)), m) == True{} : Bool}:
513  match l:
514    case 0n:
515      Empty.absurd({Nat.is_le(Nat.add(k, 1n+m), m) == True{} : Bool}, absurd.ft(e))
516    case 1n+i:
517      nat.add_sub_le(k, i, m, e, f)
518
519def bitw.ffs_fls_k(+n: Nat, +w: Word(n), +k: Nat, e: {A.bitw.index(A.bitw.ffs(n, w)) == Some{k} : Maybe<&2, Nat>}) -> {Nat.is_le(1n+k, A.bitw.fls(n, w)) == True{} : Bool}:
520  %bitw.index_some(A.bitw.ffs(n, w), k, e) : {Nat.is_le(_, A.bitw.fls(n, w)) == True{} : Bool}
521  bitw.ffs_le_fls(n, w)
522
523def bitw.ctz_clz(+m: Nat, +w: Word(1n+m), +k: Nat, +e: {A.bitw.index(A.bitw.ffs(1n+m, w)) == Some{k} : Maybe<&2, Nat>}) -> {Nat.is_le(Nat.add(A.bitw.ctz(1n+m, w), A.bitw.clz(1n+m, w)), m) == True{} : Bool}:
524  %Equal.sym(Nat, A.bitw.ctz(1n+m, w), k, bitw.ctz_first_set(1n+m, w, k, e)) : {Nat.is_le(Nat.add(_, A.bitw.clz(1n+m, w)), m) == True{} : Bool}
525  bitw.ctz_clz.h(k, m, A.bitw.fls(1n+m, w), bitw.ffs_fls_k(1n+m, w, k, e), bitw.fls_le(1n+m, w))
526
527# U32: a word whose bits are all clear is 0
528
529def u32.zero(+x: U32, e: {A.bits32.word(x) == Word.zero(32n) : Word(32n)}) -> {x == 0 : U32}:
530  match x:
531    case U32{w}:
532      %e : {U32{w} == U32{_} : U32}
533      {==}
534
535# W64: the halves of a joined word (word64's bits.lo, bits.hi and bits.cat)
536
537def w64.lo_cat(m: Nat, +n: Nat, l: Word(m), +h: Word(n)) -> {W.W64.bits.lo(m, n, W.W64.bits.cat(m, n, l, h)) == l : Word(m)}:
538  match m:
539    case 0n:
540      match l:
541        case WNil{}:
542          {==}
543    case 1n+ +p:
544      match l:
545        case WCon{+b, +t}:
546          %w64.lo_cat(p, n, t, h) : {WCon{b, W.W64.bits.lo(p, n, W.W64.bits.cat(p, n, t, h))} == WCon{b, _} : Word(1n+p)}
547          {==}
548
549def w64.hi_cat(m: Nat, +n: Nat, l: Word(m), +h: Word(n)) -> {W.W64.bits.hi(m, n, W.W64.bits.cat(m, n, l, h)) == h : Word(n)}:
550  match m:
551    case 0n:
552      match l:
553        case WNil{}:
554          {==}
555    case 1n+ +p:
556      match l:
557        case WCon{b, +t}:
558          w64.hi_cat(p, n, t, h)
559
560def w64.zero(+a: W.W64, +e: {A.bits64.word(a) == Word.zero(64n) : Word(64n)}) -> {a == W.W64.zero() : W.W64}:
561  +l = A.bits32.word(W.W64.lo(a))
562  +h = A.bits32.word(W.W64.hi(a))
563  +c = W.W64.bits.cat(32n, 32n, l, h)
564  +el = Equal.trans(Word(32n), l, W.W64.bits.lo(32n, 32n, c), Word.zero(32n), Equal.sym(Word(32n), W.W64.bits.lo(32n, 32n, c), l, w64.lo_cat(32n, 32n, l, h)), Equal.cong(Word(64n), Word(32n), v => W.W64.bits.lo(32n, 32n, v), c, Word.zero(64n), e))
565  +eh = Equal.trans(Word(32n), h, W.W64.bits.hi(32n, 32n, c), Word.zero(32n), Equal.sym(Word(32n), W.W64.bits.hi(32n, 32n, c), h, w64.hi_cat(32n, 32n, l, h)), Equal.cong(Word(64n), Word(32n), v => W.W64.bits.hi(32n, 32n, v), c, Word.zero(64n), e))
566  %WL.parts_of(a) : {_ == W.W64.zero() : W.W64}
567  %Equal.sym(U32, W.W64.hi(a), 0, u32.zero(W.W64.hi(a), eh)) : {W.W64.from_parts(_, W.W64.lo(a)) == W.W64.zero() : W.W64}
568  %Equal.sym(U32, W.W64.lo(a), 0, u32.zero(W.W64.lo(a), el)) : {W.W64.from_parts(0, _) == W.W64.zero() : W.W64}
569  {==}
570
571# Bit sequences: next
572
573def bitseq.next_le(size: Nat, start: Nat, want: Bool, bs: List<&2, Bool>) -> {Nat.is_le(M.bitseq.next(size, start, want, bs), size) == True{} : Bool}:
574  match size:
575    case 0n:
576      {==}
577    case 1n+ +s:
578      match start want bs:
579        case 1n+st w Nil{}:
580          bitseq.next_le(s, st, w, Nil{})
581        case 1n+st w Con{h, t}:
582          bitseq.next_le(s, st, w, t)
583        case 0n False{} Nil{}:
584          {==}
585        case 0n True{} Nil{}:
586          nat.le_refl(s)
587        case 0n True{} Con{True{}, t}:
588          {==}
589        case 0n False{} Con{False{}, t}:
590          {==}
591        case 0n True{} Con{False{}, t}:
592          bitseq.next_le(s, 0n, True{}, t)
593        case 0n False{} Con{True{}, t}:
594          bitseq.next_le(s, 0n, False{}, t)
595
596def bitseq.next_hit(size: Nat, start: Nat, want: Bool, bs: List<&2, Bool>, l: {Nat.is_lt(M.bitseq.next(size, start, want, bs), size) == True{} : Bool}) -> {M.bitseq.at(bs, M.bitseq.next(size, start, want, bs)) == want : Bool}:
597  match size:
598    case 0n:
599      Empty.absurd({M.bitseq.at(bs, 0n) == want : Bool}, absurd.ft(l))
600    case 1n+ +s:
601      match start want bs:
602        case 1n+st w Nil{}:
603          bitseq.next_hit(s, st, w, Nil{}, l)
604        case 1n+st w Con{h, t}:
605          bitseq.next_hit(s, st, w, t, l)
606        case 0n False{} Nil{}:
607          {==}
608        case 0n True{} Nil{}:
609          Empty.absurd({False{} == True{} : Bool}, absurd.ft(Equal.trans(Bool, False{}, Nat.is_lt(s, s), True{}, Equal.sym(Bool, Nat.is_lt(s, s), False{}, nat.lt_irrefl(s)), l)))
610        case 0n True{} Con{True{}, t}:
611          {==}
612        case 0n False{} Con{False{}, t}:
613          {==}
614        case 0n True{} Con{False{}, t}:
615          bitseq.next_hit(s, 0n, True{}, t, l)
616        case 0n False{} Con{True{}, t}:
617          bitseq.next_hit(s, 0n, False{}, t, l)
618
619def bitseq.next_ge(size: Nat, start: Nat, want: Bool, bs: List<&2, Bool>, l: {Nat.is_lt(M.bitseq.next(size, start, want, bs), size) == True{} : Bool}) -> {Nat.is_le(start, M.bitseq.next(size, start, want, bs)) == True{} : Bool}:
620  match size:
621    case 0n:
622      Empty.absurd({Nat.is_le(start, 0n) == True{} : Bool}, absurd.ft(l))
623    case 1n+ +s:
624      match start want bs:
625        case 1n+st w Nil{}:
626          bitseq.next_ge(s, st, w, Nil{}, l)
627        case 1n+st w Con{h, t}:
628          bitseq.next_ge(s, st, w, t, l)
629        case 0n False{} Nil{}:
630          {==}
631        case 0n True{} Nil{}:
632          {==}
633        case 0n True{} Con{True{}, t}:
634          {==}
635        case 0n False{} Con{False{}, t}:
636          {==}
637        case 0n True{} Con{False{}, t}:
638          {==}
639        case 0n False{} Con{True{}, t}:
640          {==}
641
642def bitseq.lt0(+j: Nat, -T: Type, l: {Nat.is_lt(j, 0n) == True{} : Bool}) -> T:
643  Empty.absurd(T, absurd.ft(Equal.trans(Bool, False{}, Nat.is_lt(j, 0n), True{}, Equal.sym(Bool, Nat.is_lt(j, 0n), False{}, nat.lt_zero(j)), l)))
644
645def bitseq.next_miss(size: Nat, start: Nat, want: Bool, bs: List<&2, Bool>, j: Nat, l: {Nat.is_le(start, j) == True{} : Bool}, m: {Nat.is_lt(j, M.bitseq.next(size, start, want, bs)) == True{} : Bool}) -> {M.bitseq.at(bs, j) == Bool.not(want) : Bool}:
646  match size:
647    case 0n:
648      bitseq.lt0(j, {M.bitseq.at(bs, j) == Bool.not(want) : Bool}, m)
649    case 1n+ +s:
650      match start want bs j:
651        case 1n+st w Nil{} 0n:
652          Empty.absurd({False{} == Bool.not(w) : Bool}, absurd.ft(l))
653        case 1n+st w Nil{} 1n+jp:
654          bitseq.next_miss(s, st, w, Nil{}, jp, l, m)
655        case 1n+st w Con{h, t} 0n:
656          Empty.absurd({h == Bool.not(w) : Bool}, absurd.ft(l))
657        case 1n+st w Con{h, t} 1n+jp:
658          bitseq.next_miss(s, st, w, t, jp, l, m)
659        case 0n False{} Nil{} +jj:
660          bitseq.lt0(jj, {M.bitseq.at(Nil{}, jj) == True{} : Bool}, m)
661        case 0n True{} Nil{} jj:
662          {==}
663        case 0n True{} Con{True{}, t} +jj:
664          bitseq.lt0(jj, {M.bitseq.at(Con{True{}, t}, jj) == False{} : Bool}, m)
665        case 0n False{} Con{False{}, t} +jj:
666          bitseq.lt0(jj, {M.bitseq.at(Con{False{}, t}, jj) == True{} : Bool}, m)
667        case 0n True{} Con{False{}, t} 0n:
668          {==}
669        case 0n True{} Con{False{}, t} 1n+ +jp:
670          bitseq.next_miss(s, 0n, True{}, t, jp, nat.le_zero(jp), m)
671        case 0n False{} Con{True{}, t} 0n:
672          {==}
673        case 0n False{} Con{True{}, t} 1n+ +jp:
674          bitseq.next_miss(s, 0n, False{}, t, jp, nat.le_zero(jp), m)
675
676# The laws: U32
677
678def Laws.popcount_le(x):
679  bitw.popcount_le(32n, A.bits32.word(x))
680
681def Laws.popcount_not(x):
682  match x:
683    case U32{w}:
684      bitw.popcount_not(32n, w)
685
686def Laws.first_set_is_set(x, k, e):
687  bitw.first_set_is_set(32n, A.bits32.word(x), k, e)
688
689def Laws.first_set_lowest(x, k, j, e, l):
690  bitw.first_set_lowest(32n, A.bits32.word(x), k, j, e, l)
691
692def Laws.first_set_none(x, e):
693  match x:
694    case U32{+w}:
695      %bitw.first_set_none(32n, w, e) : {U32{w} == U32{_} : U32}
696      {==}
697
698def Laws.last_set_is_set(x, k, e):
699  bitw.last_set_is_set(32n, A.bits32.word(x), k, e)
700
701def Laws.last_set_highest(x, k, j, e, l):
702  bitw.last_set_highest(32n, A.bits32.word(x), k, j, e, l)
703
704def Laws.last_set_none(x, e):
705  match x:
706    case U32{+w}:
707      %bitw.last_set_none(32n, w, e) : {U32{w} == U32{_} : U32}
708      {==}
709
710def Laws.ctz_first_set(x, k, e):
711  bitw.ctz_first_set(32n, A.bits32.word(x), k, e)
712
713def Laws.clz_last_set(x, k, e):
714  bitw.clz_last_set(31n, A.bits32.word(x), k, e)
715
716def Laws.first_le_last(x, i, k, e, f):
717  bitw.first_le_last(32n, A.bits32.word(x), i, k, e, f)
718
719def Laws.ctz_clz(x, k, e):
720  bitw.ctz_clz(31n, A.bits32.word(x), k, e)
721
722# The laws: W64
723
724def Laws.popcount64_le(a):
725  bitw.popcount_le(64n, A.bits64.word(a))
726
727def Laws.first_set64_is_set(a, k, e):
728  bitw.first_set_is_set(64n, A.bits64.word(a), k, e)
729
730def Laws.first_set64_lowest(a, k, j, e, l):
731  bitw.first_set_lowest(64n, A.bits64.word(a), k, j, e, l)
732
733def w64.first_set_none(+a: W.W64, e: {A.bits64.first_set(a) == None{} : Maybe<&2, Nat>}) -> {a == W.W64.zero() : W.W64}:
734  w64.zero(a, bitw.first_set_none(64n, A.bits64.word(a), e))
735
736def Laws.first_set64_none(a, e):
737  w64.first_set_none(a, e)
738
739def Laws.last_set64_is_set(a, k, e):
740  bitw.last_set_is_set(64n, A.bits64.word(a), k, e)
741
742def Laws.last_set64_highest(a, k, j, e, l):
743  bitw.last_set_highest(64n, A.bits64.word(a), k, j, e, l)
744
745def Laws.ctz64_first_set(a, k, e):
746  bitw.ctz_first_set(64n, A.bits64.word(a), k, e)
747
748def Laws.clz64_last_set(a, k, e):
749  bitw.clz_last_set(63n, A.bits64.word(a), k, e)
750
751def Laws.ctz_clz64(a, k, e):
752  bitw.ctz_clz(63n, A.bits64.word(a), k, e)
753
754# The laws: bitmaps
755
756def Laws.next_set_le_size(words, size, start):
757  bitseq.next_le(size, start, True{}, M.bitmap.bits(words))
758
759def Laws.next_set_is_set(words, size, start, l):
760  bitseq.next_hit(size, start, True{}, M.bitmap.bits(words), l)
761
762def Laws.next_set_at_least(words, size, start, l):
763  bitseq.next_ge(size, start, True{}, M.bitmap.bits(words), l)
764
765def Laws.next_set_none_before(words, size, start, j, l, m):
766  bitseq.next_miss(size, start, True{}, M.bitmap.bits(words), j, l, m)
767
768def Laws.next_clear_le_size(words, size, start):
769  bitseq.next_le(size, start, False{}, M.bitmap.bits(words))
770
771def Laws.next_clear_is_clear(words, size, start, l):
772  bitseq.next_hit(size, start, False{}, M.bitmap.bits(words), l)
773
774def Laws.next_clear_at_least(words, size, start, l):
775  bitseq.next_ge(size, start, False{}, M.bitmap.bits(words), l)
776
777def Laws.next_clear_none_before(words, size, start, j, l, m):
778  bitseq.next_miss(size, start, False{}, M.bitmap.bits(words), j, l, m)
779
780# Vectors
781
782def Laws.vec_popcount():
783  {==}
784
785def Laws.vec_zero():
786  {==}
787
788def Laws.vec_forty():
789  {==}
790
791def Laws.vec_top():
792  {==}
793
794def Laws.vec64_halves():
795  {==}
796
797def Laws.vec64_zero():
798  {==}
799
800def Laws.vec_next_set():
801  {==}
802
803def Laws.vec_next_set_none():
804  {==}
805
806def Laws.vec_next_clear():
807  {==}
808
809def Laws.vec_next_past_size():
810  {==}
811
812# Binary search: Maybe<&2, U32>
813
814def absurd.maybe32(m: Maybe<&2, U32>) -> Type:
815  match m:
816    case None{}:
817      Empty
818    case Some{k}:
819      Unit
820
821def absurd.ns32(-k: U32, e: {None{} == Some{k} : Maybe<&2, U32>}) -> Empty:
822  %Equal.sym(Maybe<&2, U32>, None{}, Some{k}, e) : absurd.maybe32(_)
823  Unit{}
824
825def maybe32.get(m: Maybe<&2, U32>) -> U32:
826  match m:
827    case None{}:
828      0
829    case Some{k}:
830      k
831
832def some_inj32(-a: U32, -b: U32, e: {Some{a} == Some{b} : Maybe<&2, U32>}) -> {a == b : U32}:
833  Equal.cong(Maybe<&2, U32>, U32, m => maybe32.get(m), Some{a}, Some{b}, e)
834
835def absurd.sn_nat(-k: Nat, e: {Some{k} == None{} : Maybe<&2, Nat>}) -> Empty:
836  absurd.sn(k, e)
837
838# Binary search: Bool
839
840def bool.and_l(a: Bool, -b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
841  match a:
842    case True{}:
843      {==}
844    case False{}:
845      Empty.absurd({False{} == True{} : Bool}, absurd.ft(e))
846
847def bool.and_r(a: Bool, -b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
848  match a:
849    case True{}:
850      e
851    case False{}:
852      Empty.absurd({b == True{} : Bool}, absurd.ft(e))
853
854# Binary search: the order of U32 is the order of its value as a Nat
855
856def nat.dbit(b: Bool, a: Nat) -> Nat:
857  match b:
858    case False{}:
859      Nat.double(a)
860    case True{}:
861      1n+Nat.double(a)
862
863def word.cmp_nat.d(a: Nat, b: Nat, x: Bool, y: Bool) -> {Word.cmp.fin(x, y, Nat.cmp(a, b)) == Nat.cmp(nat.dbit(x, a), nat.dbit(y, b)) : Cmp}:
864  match a b:
865    case 0n 0n:
866      match x y:
867        case True{} True{}:
868          {==}
869        case True{} False{}:
870          {==}
871        case False{} True{}:
872          {==}
873        case False{} False{}:
874          {==}
875    case 0n 1n+bp:
876      match x y:
877        case True{} True{}:
878          {==}
879        case True{} False{}:
880          {==}
881        case False{} True{}:
882          {==}
883        case False{} False{}:
884          {==}
885    case 1n+ap 0n:
886      match x y:
887        case True{} True{}:
888          {==}
889        case True{} False{}:
890          {==}
891        case False{} True{}:
892          {==}
893        case False{} False{}:
894          {==}
895    case 1n+ +ap 1n+ +bp:
896      match x y:
897        case True{} True{}:
898          word.cmp_nat.d(ap, bp, True{}, True{})
899        case True{} False{}:
900          word.cmp_nat.d(ap, bp, True{}, False{})
901        case False{} True{}:
902          word.cmp_nat.d(ap, bp, False{}, True{})
903        case False{} False{}:
904          word.cmp_nat.d(ap, bp, False{}, False{})
905
906def word.cmp_nat.h(+p: Nat, +x: Bool, +y: Bool, +at: Word(p), +bt: Word(p), ih: {Word.cmp(p, at, bt) == Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt)) : Cmp}) -> {Word.cmp.fin(x, y, Word.cmp(p, at, bt)) == Nat.cmp(nat.dbit(x, Word.to_nat(p, at)), nat.dbit(y, Word.to_nat(p, bt))) : Cmp}:
907  %Equal.sym(Cmp, Word.cmp(p, at, bt), Nat.cmp(Word.to_nat(p, at), Word.to_nat(p, bt)), ih) : {Word.cmp.fin(x, y, _) == Nat.cmp(nat.dbit(x, Word.to_nat(p, at)), nat.dbit(y, Word.to_nat(p, bt))) : Cmp}
908  word.cmp_nat.d(Word.to_nat(p, at), Word.to_nat(p, bt), x, y)
909
910def word.cmp_nat(n: Nat, a: Word(n), b: Word(n)) -> {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}:
911  match n:
912    case 0n:
913      match a b:
914        case WNil{} WNil{}:
915          {==}
916    case 1n+ +p:
917      match a b:
918        case WCon{True{}, +at} WCon{True{}, +bt}:
919          word.cmp_nat.h(p, True{}, True{}, at, bt, word.cmp_nat(p, at, bt))
920        case WCon{True{}, +at} WCon{False{}, +bt}:
921          word.cmp_nat.h(p, True{}, False{}, at, bt, word.cmp_nat(p, at, bt))
922        case WCon{False{}, +at} WCon{True{}, +bt}:
923          word.cmp_nat.h(p, False{}, True{}, at, bt, word.cmp_nat(p, at, bt))
924        case WCon{False{}, +at} WCon{False{}, +bt}:
925          word.cmp_nat.h(p, False{}, False{}, at, bt, word.cmp_nat(p, at, bt))
926
927def u32.cmp_nat(a: U32, b: U32) -> {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}:
928  match a b:
929    case U32{wa} U32{wb}:
930      word.cmp_nat(32n, wa, wb)
931
932# a hypothesis about U32's order, as one about Nat's
933def u32.mv_le(+a: U32, +b: U32, -v: Bool, h: {U32.is_le(a, b) == v : Bool}) -> {Nat.is_le(U32.to_nat(a), U32.to_nat(b)) == v : Bool}:
934  %u32.cmp_nat(a, b) : {Cmp.is_le(_) == v : Bool}
935  h
936
937def u32.mv_lt(+a: U32, +b: U32, -v: Bool, h: {U32.is_lt(a, b) == v : Bool}) -> {Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == v : Bool}:
938  %u32.cmp_nat(a, b) : {Cmp.is_lt(_) == v : Bool}
939  h
940
941def u32.mv_eq(+a: U32, +b: U32, -v: Bool, h: {U32.is_eq(a, b) == v : Bool}) -> {Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) == v : Bool}:
942  %u32.cmp_nat(a, b) : {Cmp.is_eq(_) == v : Bool}
943  h
944
945# Nat order facts
946
947def nat.le_trans(a: Nat, b: Nat, c: Nat, e: {Nat.is_le(a, b) == True{} : Bool}, f: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_le(a, c) == True{} : Bool}:
948  match a b c:
949    case 0n _ _:
950      nat.le_zero(c)
951    case 1n+ap 0n _:
952      Empty.absurd({Nat.is_le(1n+ap, c) == True{} : Bool}, absurd.ft(e))
953    case 1n+ap 1n+bp 0n:
954      Empty.absurd({Nat.is_le(1n+ap, 0n) == True{} : Bool}, absurd.ft(f))
955    case 1n+ap 1n+bp 1n+cp:
956      nat.le_trans(ap, bp, cp, e, f)
957
958# not a < c, a <= b: not b < c
959def nat.nlt_le(a: Nat, b: Nat, c: Nat, e: {Nat.is_lt(a, c) == False{} : Bool}, f: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_lt(b, c) == False{} : Bool}:
960  match a b c:
961    case 0n _ 0n:
962      nat.lt_zero(b)
963    case 0n _ 1n+cp:
964      Empty.absurd({Nat.is_lt(b, 1n+cp) == False{} : Bool}, absurd.tf(e))
965    case 1n+ap 0n _:
966      Empty.absurd({Nat.is_lt(0n, c) == False{} : Bool}, absurd.ft(f))
967    case 1n+ap 1n+bp 0n:
968      {==}
969    case 1n+ap 1n+bp 1n+cp:
970      nat.nlt_le(ap, bp, cp, e, f)
971
972# k < a (not a < k, a != k), a <= b: b != k
973def nat.gt_le_ne(a: Nat, b: Nat, k: Nat, e: {Nat.is_lt(a, k) == False{} : Bool}, f: {Nat.is_eq(a, k) == False{} : Bool}, g: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_eq(b, k) == False{} : Bool}:
974  match a b k:
975    case 0n _ 0n:
976      Empty.absurd({Nat.is_eq(b, 0n) == False{} : Bool}, absurd.tf(f))
977    case 0n _ 1n+kp:
978      Empty.absurd({Nat.is_eq(b, 1n+kp) == False{} : Bool}, absurd.tf(e))
979    case 1n+ap 0n _:
980      Empty.absurd({Nat.is_eq(0n, k) == False{} : Bool}, absurd.ft(g))
981    case 1n+ap 1n+bp 0n:
982      {==}
983    case 1n+ap 1n+bp 1n+kp:
984      nat.gt_le_ne(ap, bp, kp, e, f, g)
985
986# U32 order facts
987
988def u32.le_trans(+a: U32, +b: U32, +c: U32, e: {U32.is_le(a, b) == True{} : Bool}, f: {U32.is_le(b, c) == True{} : Bool}) -> {U32.is_le(a, c) == True{} : Bool}:
989  %Equal.sym(Cmp, U32.cmp(a, c), Nat.cmp(U32.to_nat(a), U32.to_nat(c)), u32.cmp_nat(a, c)) : {Cmp.is_le(_) == True{} : Bool}
990  nat.le_trans(U32.to_nat(a), U32.to_nat(b), U32.to_nat(c), u32.mv_le(a, b, True{}, e), u32.mv_le(b, c, True{}, f))
991
992def u32.nlt_le(+a: U32, +b: U32, +c: U32, e: {U32.is_lt(a, c) == False{} : Bool}, f: {U32.is_le(a, b) == True{} : Bool}) -> {U32.is_lt(b, c) == False{} : Bool}:
993  %Equal.sym(Cmp, U32.cmp(b, c), Nat.cmp(U32.to_nat(b), U32.to_nat(c)), u32.cmp_nat(b, c)) : {Cmp.is_lt(_) == False{} : Bool}
994  nat.nlt_le(U32.to_nat(a), U32.to_nat(b), U32.to_nat(c), u32.mv_lt(a, c, False{}, e), u32.mv_le(a, b, True{}, f))
995
996def u32.gt_le_ne(+a: U32, +b: U32, +k: U32, e: {U32.is_lt(a, k) == False{} : Bool}, f: {U32.is_eq(a, k) == False{} : Bool}, g: {U32.is_le(a, b) == True{} : Bool}) -> {U32.is_eq(b, k) == False{} : Bool}:
997  %Equal.sym(Cmp, U32.cmp(b, k), Nat.cmp(U32.to_nat(b), U32.to_nat(k)), u32.cmp_nat(b, k)) : {Cmp.is_eq(_) == False{} : Bool}
998  nat.gt_le_ne(U32.to_nat(a), U32.to_nat(b), U32.to_nat(k), u32.mv_lt(a, k, False{}, e), u32.mv_eq(a, k, False{}, f), u32.mv_le(a, b, True{}, g))
999
1000def cmp.lt_ne(c: Cmp, e: {Cmp.is_lt(c) == True{} : Bool}) -> {Cmp.is_eq(c) == False{} : Bool}:
1001  match c:
1002    case LT{}:
1003      {==}
1004    case EQ{}:
1005      Empty.absurd({True{} == False{} : Bool}, absurd.ft(e))
1006    case GT{}:
1007      Empty.absurd({False{} == False{} : Bool}, absurd.ft(e))
1008
1009def u32.lt_ne(+a: U32, +b: U32, e: {U32.is_lt(a, b) == True{} : Bool}) -> {U32.is_eq(a, b) == False{} : Bool}:
1010  cmp.lt_ne(U32.cmp(a, b), e)
1011
1012# is_eq gives equality
1013
1014def word.eq_tail(c: Cmp, x: Bool, y: Bool, e: {Cmp.is_eq(Word.cmp.fin(x, y, c)) == True{} : Bool}) -> {Cmp.is_eq(c) == True{} : Bool}:
1015  match c:
1016    case LT{}:
1017      Empty.absurd({False{} == True{} : Bool}, absurd.ft(e))
1018    case EQ{}:
1019      {==}
1020    case GT{}:
1021      Empty.absurd({False{} == True{} : Bool}, absurd.ft(e))
1022
1023def word.eq_head(c: Cmp, x: Bool, y: Bool, e: {Cmp.is_eq(Word.cmp.fin(x, y, c)) == True{} : Bool}) -> {x == y : Bool}:
1024  match c:
1025    case LT{}:
1026      Empty.absurd({x == y : Bool}, absurd.ft(e))
1027    case EQ{}:
1028      match x y:
1029        case True{} True{}:
1030          {==}
1031        case False{} False{}:
1032          {==}
1033        case True{} False{}:
1034          Empty.absurd({True{} == False{} : Bool}, absurd.ft(e))
1035        case False{} True{}:
1036          Empty.absurd({False{} == True{} : Bool}, absurd.ft(e))
1037    case GT{}:
1038      Empty.absurd({x == y : Bool}, absurd.ft(e))
1039
1040def word.eq(n: Nat, a: Word(n), b: Word(n), e: {Cmp.is_eq(Word.cmp(n, a, b)) == True{} : Bool}) -> {a == b : Word(n)}:
1041  match n:
1042    case 0n:
1043      match a b:
1044        case WNil{} WNil{}:
1045          {==}
1046    case 1n+ +p:
1047      match a b:
1048        case WCon{+x, +at} WCon{+y, +bt}:
1049          +e2 = e
1050          %word.eq(p, at, bt, word.eq_tail(Word.cmp(p, at, bt), x, y, e2)) : {WCon{x, at} == WCon{y, _} : Word(1n+p)}
1051          %word.eq_head(Word.cmp(p, at, bt), x, y, e2) : {WCon{x, at} == WCon{_, at} : Word(1n+p)}
1052          {==}
1053
1054def u32.eq(a: U32, b: U32, e: {U32.is_eq(a, b) == True{} : Bool}) -> {a == b : U32}:
1055  match a b:
1056    case U32{+wa} U32{+wb}:
1057      %word.eq(32n, wa, wb, e) : {U32{wa} == U32{_} : U32}
1058      {==}
1059
1060# Binary search: sorted lists
1061
1062def bs.sorted_tail(t: List<&2, U32>, x0: U32, s: {S.bsearch.sorted.pair(t, x0) == True{} : Bool}) -> {S.bsearch.sorted(t) == True{} : Bool}:
1063  match t:
1064    case Nil{}:
1065      {==}
1066    case Con{y, tt}:
1067      bool.and_r(U32.is_le(x0, y), S.bsearch.sorted.pair(tt, y), s)
1068
1069# the head of a sorted list is at most each of its elements
1070def bs.head_le(t: List<&2, U32>, +x0: U32, s: {S.bsearch.sorted.pair(t, x0) == True{} : Bool}, i: Nat, +x: U32, e: {List.get(&2, U32, t, i) == Some{x} : Maybe<&2, U32>}) -> {U32.is_le(x0, x) == True{} : Bool}:
1071  match t i:
1072    case Nil{} _:
1073      Empty.absurd({U32.is_le(x0, x) == True{} : Bool}, absurd.ns32(x, e))
1074    case Con{+y, tt} 0n:
1075      %some_inj32(y, x, e) : {U32.is_le(x0, _) == True{} : Bool}
1076      bool.and_l(U32.is_le(x0, y), S.bsearch.sorted.pair(tt, y), s)
1077    case Con{+y, +tt} 1n+ip:
1078      +s2 = s
1079      u32.le_trans(x0, y, x, bool.and_l(U32.is_le(x0, y), S.bsearch.sorted.pair(tt, y), s2), bs.head_le(tt, y, bool.and_r(U32.is_le(x0, y), S.bsearch.sorted.pair(tt, y), s2), ip, x, e))
1080
1081# Binary search: lower_bound
1082
1083def bs.le_len.h(c: Bool, r: Nat, +n: Nat, ih: {Nat.is_le(r, n) == True{} : Bool}) -> {Nat.is_le(S.bsearch.below.step(c, r), 1n+n) == True{} : Bool}:
1084  match c:
1085    case True{}:
1086      ih
1087    case False{}:
1088      {==}
1089
1090def bs.le_len(xs: List<&2, U32>, +key: U32) -> {Nat.is_le(S.bsearch.lower_bound(xs, key), List.length(&2, U32, xs)) == True{} : Bool}:
1091  match xs:
1092    case Nil{}:
1093      {==}
1094    case Con{x, +t}:
1095      bs.le_len.h(U32.is_lt(x, key), S.bsearch.lower_bound(t, key), List.length(&2, U32, t), bs.le_len(t, key))
1096
1097def bs.step0(c: Bool, +r: Nat, l: {Nat.is_lt(0n, S.bsearch.below.step(c, r)) == True{} : Bool}) -> {c == True{} : Bool}:
1098  match c:
1099    case True{}:
1100      {==}
1101    case False{}:
1102      Empty.absurd({False{} == True{} : Bool}, absurd.ft(l))
1103
1104def bs.step1(c: Bool, +r: Nat, +i: Nat, l: {Nat.is_lt(1n+i, S.bsearch.below.step(c, r)) == True{} : Bool}) -> {Nat.is_lt(i, r) == True{} : Bool}:
1105  match c:
1106    case True{}:
1107      l
1108    case False{}:
1109      Empty.absurd({Nat.is_lt(i, r) == True{} : Bool}, absurd.ft(l))
1110
1111def bs.below(xs: List<&2, U32>, +key: U32, i: Nat, +x: U32, e: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}, l: {Nat.is_lt(i, S.bsearch.lower_bound(xs, key)) == True{} : Bool}) -> {U32.is_lt(x, key) == True{} : Bool}:
1112  match xs i:
1113    case Nil{} _:
1114      Empty.absurd({U32.is_lt(x, key) == True{} : Bool}, absurd.ns32(x, e))
1115    case Con{+x0, t} 0n:
1116      %some_inj32(x0, x, e) : {U32.is_lt(_, key) == True{} : Bool}
1117      bs.step0(U32.is_lt(x0, key), S.bsearch.lower_bound(t, key), l)
1118    case Con{+x0, +t} 1n+ +ip:
1119      bs.below(t, key, ip, x, e, bs.step1(U32.is_lt(x0, key), S.bsearch.lower_bound(t, key), ip, l))
1120
1121def bs.above0(c: Bool, +r: Nat, l: {Nat.is_le(S.bsearch.below.step(c, r), 0n) == True{} : Bool}) -> {c == False{} : Bool}:
1122  match c:
1123    case True{}:
1124      Empty.absurd({True{} == False{} : Bool}, absurd.ft(l))
1125    case False{}:
1126      {==}
1127
1128def bs.above1(c: Bool, +x0: U32, +x: U32, +key: U32, ec: {U32.is_lt(x0, key) == c : Bool}, +r: Nat, +i: Nat, l: {Nat.is_le(S.bsearch.below.step(c, r), 1n+i) == True{} : Bool}, ih: {Nat.is_le(r, i) == True{} : Bool} -> {U32.is_lt(x, key) == False{} : Bool}, h: {U32.is_le(x0, x) == True{} : Bool}) -> {U32.is_lt(x, key) == False{} : Bool}:
1129  match c:
1130    case True{}:
1131      ih(l)
1132    case False{}:
1133      u32.nlt_le(x0, x, key, ec, h)
1134
1135def bs.above(xs: List<&2, U32>, +key: U32, i: Nat, +x: U32, s: {S.bsearch.sorted(xs) == True{} : Bool}, e: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}, l: {Nat.is_le(S.bsearch.lower_bound(xs, key), i) == True{} : Bool}) -> {U32.is_lt(x, key) == False{} : Bool}:
1136  match xs i:
1137    case Nil{} _:
1138      Empty.absurd({U32.is_lt(x, key) == False{} : Bool}, absurd.ns32(x, e))
1139    case Con{+x0, t} 0n:
1140      %some_inj32(x0, x, e) : {U32.is_lt(_, key) == False{} : Bool}
1141      bs.above0(U32.is_lt(x0, key), S.bsearch.lower_bound(t, key), l)
1142    case Con{+x0, +t} 1n+ +ip:
1143      +s2 = s
1144      +e2 = e
1145      bs.above1(U32.is_lt(x0, key), x0, x, key, {==}, S.bsearch.lower_bound(t, key), ip, l, h => bs.above(t, key, ip, x, bs.sorted_tail(t, x0, s2), e2, h), bs.head_le(t, x0, s2, ip, x, e2))
1146
1147# Binary search: find
1148
1149def bs.hit_none(c: Bool, +i: Nat, e: {S.bsearch.find.hit(c, i) == None{} : Maybe<&2, Nat>}) -> {c == False{} : Bool}:
1150  match c:
1151    case True{}:
1152      Empty.absurd({True{} == False{} : Bool}, absurd.sn(i, e))
1153    case False{}:
1154      {==}
1155
1156def bs.hit_shift(c: Bool, +i: Nat, e: {S.bsearch.find.hit(c, 1n+i) == None{} : Maybe<&2, Nat>}) -> {S.bsearch.find.hit(c, i) == None{} : Maybe<&2, Nat>}:
1157  match c:
1158    case True{}:
1159      Empty.absurd({Some{i} == None{} : Maybe<&2, Nat>}, absurd.sn(1n+i, e))
1160    case False{}:
1161      {==}
1162
1163def bs.check_shift(m: Maybe<&2, U32>, +i: Nat, +key: U32, e: {S.bsearch.find.check(1n+i, m, key) == None{} : Maybe<&2, Nat>}) -> {S.bsearch.find.check(i, m, key) == None{} : Maybe<&2, Nat>}:
1164  match m:
1165    case None{}:
1166      {==}
1167    case Some{y}:
1168      bs.hit_shift(U32.is_eq(y, key), i, e)
1169
1170def bs.some.h(c: Bool, x: U32, key: U32, ec: {U32.is_eq(x, key) == c : Bool}, +xs: List<&2, U32>, +lb: Nat, +i: Nat, e: {S.bsearch.find.hit(c, lb) == Some{i} : Maybe<&2, Nat>}, g: {List.get(&2, U32, xs, lb) == Some{x} : Maybe<&2, U32>}) -> {List.get(&2, U32, xs, i) == Some{key} : Maybe<&2, U32>}:
1171  match c:
1172    case True{}:
1173      %some_inj(lb, i, e) : {List.get(&2, U32, xs, _) == Some{key} : Maybe<&2, U32>}
1174      %u32.eq(x, key, ec) : {List.get(&2, U32, xs, lb) == Some{_} : Maybe<&2, U32>}
1175      g
1176    case False{}:
1177      Empty.absurd({List.get(&2, U32, xs, i) == Some{key} : Maybe<&2, U32>}, absurd.ns(i, e))
1178
1179def bs.some(m: Maybe<&2, U32>, +key: U32, +xs: List<&2, U32>, +lb: Nat, +i: Nat, g: {List.get(&2, U32, xs, lb) == m : Maybe<&2, U32>}, e: {S.bsearch.find.check(lb, m, key) == Some{i} : Maybe<&2, Nat>}) -> {List.get(&2, U32, xs, i) == Some{key} : Maybe<&2, U32>}:
1180  match m:
1181    case None{}:
1182      Empty.absurd({List.get(&2, U32, xs, i) == Some{key} : Maybe<&2, U32>}, absurd.ns(i, e))
1183    case Some{+x}:
1184      bs.some.h(U32.is_eq(x, key), x, key, {==}, xs, lb, i, e, g)
1185
1186def bs.none0(c: Bool, +x0: U32, +key: U32, ec: {U32.is_lt(x0, key) == c : Bool}, +t: List<&2, U32>, +r: Nat, e: {S.bsearch.find.check(S.bsearch.below.step(c, r), List.get(&2, U32, Con{x0, t}, S.bsearch.below.step(c, r)), key) == None{} : Maybe<&2, Nat>}) -> {U32.is_eq(x0, key) == False{} : Bool}:
1187  match c:
1188    case True{}:
1189      u32.lt_ne(x0, key, ec)
1190    case False{}:
1191      bs.hit_none(U32.is_eq(x0, key), 0n, e)
1192
1193def bs.none1(c: Bool, +x0: U32, +x: U32, +key: U32, ec: {U32.is_lt(x0, key) == c : Bool}, +t: List<&2, U32>, +r: Nat, e: {S.bsearch.find.check(S.bsearch.below.step(c, r), List.get(&2, U32, Con{x0, t}, S.bsearch.below.step(c, r)), key) == None{} : Maybe<&2, Nat>}, ih: {S.bsearch.find.check(r, List.get(&2, U32, t, r), key) == None{} : Maybe<&2, Nat>} -> {U32.is_eq(x, key) == False{} : Bool}, h: {U32.is_le(x0, x) == True{} : Bool}) -> {U32.is_eq(x, key) == False{} : Bool}:
1194  match c:
1195    case True{}:
1196      ih(bs.check_shift(List.get(&2, U32, t, r), r, key, e))
1197    case False{}:
1198      u32.gt_le_ne(x0, x, key, ec, bs.hit_none(U32.is_eq(x0, key), 0n, e), h)
1199
1200def bs.none(xs: List<&2, U32>, +key: U32, i: Nat, +x: U32, s: {S.bsearch.sorted(xs) == True{} : Bool}, e: {S.bsearch.find(xs, key) == None{} : Maybe<&2, Nat>}, g: {List.get(&2, U32, xs, i) == Some{x} : Maybe<&2, U32>}) -> {U32.is_eq(x, key) == False{} : Bool}:
1201  match xs i:
1202    case Nil{} _:
1203      Empty.absurd({U32.is_eq(x, key) == False{} : Bool}, absurd.ns32(x, g))
1204    case Con{+x0, +t} 0n:
1205      %some_inj32(x0, x, g) : {U32.is_eq(_, key) == False{} : Bool}
1206      bs.none0(U32.is_lt(x0, key), x0, key, {==}, t, S.bsearch.lower_bound(t, key), e)
1207    case Con{+x0, +t} 1n+ +ip:
1208      +s2 = s
1209      +g2 = g
1210      bs.none1(U32.is_lt(x0, key), x0, x, key, {==}, t, S.bsearch.lower_bound(t, key), e, h => bs.none(t, key, ip, x, bs.sorted_tail(t, x0, s2), h, g2), bs.head_le(t, x0, s2, ip, x, g2))
1211
1212def bs.find_some(+xs: List<&2, U32>, +key: U32, +i: Nat, e: {S.bsearch.find(xs, key) == Some{i} : Maybe<&2, Nat>}) -> {List.get(&2, U32, xs, i) == Some{key} : Maybe<&2, U32>}:
1213  bs.some(List.get(&2, U32, xs, S.bsearch.lower_bound(xs, key)), key, xs, S.bsearch.lower_bound(xs, key), i, {==}, e)
1214
1215# The laws: binary search
1216
1217def Laws.lower_bound_le_length(xs, key):
1218  bs.le_len(xs, key)
1219
1220def Laws.lower_bound_below(xs, key, i, x, e, l):
1221  bs.below(xs, key, i, x, e, l)
1222
1223def Laws.lower_bound_above(xs, key, i, x, s, e, l):
1224  bs.above(xs, key, i, x, s, e, l)
1225
1226def Laws.find_some(xs, key, i, e):
1227  bs.find_some(xs, key, i, e)
1228
1229def Laws.find_none(xs, key, i, x, s, e, g):
1230  bs.none(xs, key, i, x, s, e, g)
1231
1232def Laws.vec_lower_bound():
1233  {==}
1234
1235def Laws.vec_array_lower_bound():
1236  {==}
1237
1238def Laws.vec_array_lower_bound_end():
1239  {==}
1240
1241def Laws.vec_array_find():
1242  {==}
1243
1244def Laws.vec_array_find_none():
1245  {==}
1246
1247def Laws.wit_first_last():
1248  {==}
1249
1250def Laws.wit_first_last64():
1251  {==}
1252
1253def Laws.wit_next():
1254  {==}
1255
1256def Laws.wit_bsearch():
1257  {==}
1258
1259# Binary search on an Array<U32>
1260# ===============================
1261#
1262# The array is reflected once into Arrays.of_list(d, l, 0) (array's
1263# `reflect`); proof_bsearch.bend shows that the search on it is Q.bq.run on
1264# Data and hands the array back (Q.bq.go). Below, Q.bq.run is followed on
1265# the values of lo and hi: lo <= lower_bound <= hi <= n throughout, and
1266# hi - lo < 2^f with f halvings left, so after the 33 halvings lo is the
1267# lower bound. LB below is Q.bq.lb(l, n, key), the lower bound of the
1268# searched prefix Q.bq.pre(l, n) of l.
1269
1270# the element read at m is below the key exactly when m is below LB
1271def ba.kc(b: Bool, +l: List<&2, U32>, +key: U32, +n: U32, +hs: {S.bsearch.sorted(Q.bq.pre(l, n)) == True{} : Bool}, +m: Nat, +eg: {List.get(&2, U32, Q.bq.pre(l, n), m) == Some{AR.Arrays.nth(U32, l, m, 0)} : Maybe<&2, U32>}, +eb: {Nat.is_lt(m, Q.bq.lb(l, n, key)) == b : Bool}) -> {U32.is_lt(AR.Arrays.nth(U32, l, m, 0), key) == b : Bool}:
1272  match b:
1273    case True{}:
1274      bs.below(Q.bq.pre(l, n), key, m, AR.Arrays.nth(U32, l, m, 0), eg, eb)
1275    case False{}:
1276      bs.above(Q.bq.pre(l, n), key, m, AR.Arrays.nth(U32, l, m, 0), hs, eg, Q.bq.not_lt(m, Q.bq.lb(l, n, key), eb))
1277
1278def ba.key_cmp(+d: Nat, +l: List<&2, U32>, +hl: {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}, +key: U32, +n: U32, +hN: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}, +hs: {S.bsearch.sorted(Q.bq.pre(l, n)) == True{} : Bool}, +mid: U32, +m: Nat, +eM: {U32.to_nat(mid) == m : Nat}, +hmN: {Nat.is_lt(m, U32.to_nat(n)) == True{} : Bool}) -> {U32.is_lt(AR.Arrays.nth(U32, l, AR.Arrays.index(d, mid), 0), key) == Nat.is_lt(m, Q.bq.lb(l, n, key)) : Bool}:
1279  +hmS = Q.bq.lt_le_trans(m, U32.to_nat(n), AR.Arrays.slots(d), hmN, hN)
1280  +eI = Equal.trans(Nat, AR.Arrays.index(d, mid), U32.to_nat(mid), m, AL.index_of_u32(d, mid, Q.bq.lt_rw(m, AR.Arrays.slots(d), U32.to_nat(mid), AR.Arrays.slots(d), Equal.sym(Nat, U32.to_nat(mid), m, eM), {==}, hmS)), eM)
1281  +hml = Q.bq.lt_rw(m, AR.Arrays.slots(d), m, List.length(&2, U32, l), {==}, Equal.sym(Nat, List.length(&2, U32, l), AR.Arrays.slots(d), hl), hmS)
1282  +eg = Equal.trans(Maybe<&2, U32>, List.get(&2, U32, Q.bq.pre(l, n), m), List.get(&2, U32, l, m), Some{AR.Arrays.nth(U32, l, m, 0)}, Q.bq.get_take(l, U32.to_nat(n), m, hmN), Q.bq.get_nth(l, m, hml))
1283  %Equal.sym(Nat, AR.Arrays.index(d, mid), m, eI) : {U32.is_lt(AR.Arrays.nth(U32, l, _, 0), key) == Nat.is_lt(m, Q.bq.lb(l, n, key)) : Bool}
1284  ba.kc(Nat.is_lt(m, Q.bq.lb(l, n, key)), l, key, n, hs, m, eg, {==})
1285
1286# after a halving that keeps the upper half: hi - (mid + 1) is
1287# (hi - lo) - (1 + (hi - lo) / 2)
1288def ba.jz_eq(+lo: U32, +hi: U32, eI: {U32.to_nat(U32.inc(Q.bq.mid(lo, hi))) == 1n+Q.bq.m(lo, hi) : Nat}, ehs: {Nat.add(U32.to_nat(lo), Q.bq.s(lo, hi)) == U32.to_nat(hi) : Nat}) -> {Nat.sub(Q.bq.s(lo, hi), 1n+U.uq.half(Q.bq.s(lo, hi))) == Q.bq.s(U32.inc(Q.bq.mid(lo, hi)), hi) : Nat}:
1289  +l0 = U32.to_nat(lo)
1290  +s = Q.bq.s(lo, hi)
1291  +hs = U.uq.half(s)
1292  +m = Q.bq.m(lo, hi)
1293  %Equal.sym(Nat, U32.to_nat(U32.inc(Q.bq.mid(lo, hi))), 1n+m, eI) : {Nat.sub(s, 1n+hs) == Nat.sub(U32.to_nat(hi), _) : Nat}
1294  %ehs : {Nat.sub(s, 1n+hs) == Nat.sub(_, 1n+m) : Nat}
1295  %U.uq.add_succ(l0, hs) : {Nat.sub(s, 1n+hs) == Nat.sub(Nat.add(l0, s), _) : Nat}
1296  Equal.sym(Nat, Nat.sub(Nat.add(l0, s), Nat.add(l0, 1n+hs)), Nat.sub(s, 1n+hs), Q.bq.sub_cancel(l0, s, 1n+hs))
1297
1298# one halving, with the element at mid below the key (b) or not
1299def ba.adv2(b: Bool, +g: Nat, +d: Nat, +l: List<&2, U32>, +key: U32, +n: U32, +lo: U32, +hi: U32, +eb: {Nat.is_lt(Q.bq.m(lo, hi), Q.bq.lb(l, n, key)) == b : Bool}, +i1: {Nat.is_le(U32.to_nat(lo), Q.bq.lb(l, n, key)) == True{} : Bool}, +i2: {Nat.is_le(Q.bq.lb(l, n, key), U32.to_nat(hi)) == True{} : Bool}, +i3: {Nat.is_le(U32.to_nat(hi), U32.to_nat(n)) == True{} : Bool}, +hz: {Nat.is_lt(Q.bq.s(lo, hi), U.uq.pw(1n+g)) == True{} : Bool}, +eM: {U32.to_nat(Q.bq.mid(lo, hi)) == Q.bq.m(lo, hi) : Nat}, +ehs: {Nat.add(U32.to_nat(lo), Q.bq.s(lo, hi)) == U32.to_nat(hi) : Nat}, +hmh: {Nat.is_lt(Q.bq.m(lo, hi), U32.to_nat(hi)) == True{} : Bool}, ih: @lo2: U32 -> @hi2: U32 -> @j1: {Nat.is_le(U32.to_nat(lo2), Q.bq.lb(l, n, key)) == True{} : Bool} -> @j2: {Nat.is_le(Q.bq.lb(l, n, key), U32.to_nat(hi2)) == True{} : Bool} -> @j3: {Nat.is_le(U32.to_nat(hi2), U32.to_nat(n)) == True{} : Bool} -> @jz: {Nat.is_lt(Q.bq.s(lo2, hi2), U.uq.pw(g)) == True{} : Bool} -> {U32.to_nat(Q.bq.run(g, d, l, lo2, hi2, key)) == Q.bq.lb(l, n, key) : Nat}) -> {U32.to_nat(Q.bq.run(g, d, l, Q.bq.lo_b(b, lo, Q.bq.mid(lo, hi)), Q.bq.hi_b(b, hi, Q.bq.mid(lo, hi)), key)) == Q.bq.lb(l, n, key) : Nat}:
1300  match b:
1301    case True{}:
1302      +h0 = U32.to_nat(hi)
1303      +l0 = U32.to_nat(lo)
1304      +s = Q.bq.s(lo, hi)
1305      +m = Q.bq.m(lo, hi)
1306      +mid = Q.bq.mid(lo, hi)
1307      +lb = Q.bq.lb(l, n, key)
1308      +hinc = Q.bq.le_rw(1n+m, h0, 1n+U32.to_nat(mid), h0, U.uq.succ_cong(m, U32.to_nat(mid), Equal.sym(Nat, U32.to_nat(mid), m, eM)), {==}, Equal.trans(Bool, Nat.is_le(1n+m, h0), Nat.is_lt(m, h0), True{}, U.uq.le_succ(m, h0), hmh))
1309      +eI = Equal.trans(Nat, U32.to_nat(U32.inc(mid)), 1n+U32.to_nat(mid), 1n+m, U.uq.u32_inc(mid, hi, hinc), U.uq.succ_cong(U32.to_nat(mid), m, eM))
1310      +j1 = Q.bq.le_rw(1n+m, lb, U32.to_nat(U32.inc(mid)), lb, Equal.sym(Nat, U32.to_nat(U32.inc(mid)), 1n+m, eI), {==}, Equal.trans(Bool, Nat.is_le(1n+m, lb), Nat.is_lt(m, lb), True{}, U.uq.le_succ(m, lb), eb))
1311      +jz = Q.bq.lt_rw(Nat.sub(s, 1n+U.uq.half(s)), U.uq.pw(g), Q.bq.s(U32.inc(mid), hi), U.uq.pw(g), ba.jz_eq(lo, hi, eI, ehs), {==}, Q.bq.hr_lt_pw(s, U.uq.pw(g), hz))
1312      ih(U32.inc(mid), hi, j1, i2, i3, jz)
1313    case False{}:
1314      +h0 = U32.to_nat(hi)
1315      +l0 = U32.to_nat(lo)
1316      +s = Q.bq.s(lo, hi)
1317      +m = Q.bq.m(lo, hi)
1318      +mid = Q.bq.mid(lo, hi)
1319      +lb = Q.bq.lb(l, n, key)
1320      +j2 = Q.bq.le_rw(lb, m, lb, U32.to_nat(mid), {==}, Equal.sym(Nat, U32.to_nat(mid), m, eM), Q.bq.not_lt(m, lb, eb))
1321      +j3 = Q.bq.le_rw(m, U32.to_nat(n), U32.to_nat(mid), U32.to_nat(n), Equal.sym(Nat, U32.to_nat(mid), m, eM), {==}, Q.bq.le_trans(m, h0, U32.to_nat(n), Q.bq.lt_le(m, h0, hmh), i3))
1322      +e2 = Equal.trans(Nat, U.uq.half(s), Nat.sub(Nat.add(l0, U.uq.half(s)), l0), Nat.sub(U32.to_nat(mid), l0), Equal.sym(Nat, Nat.sub(Nat.add(l0, U.uq.half(s)), l0), U.uq.half(s), U.uq.sub_add_l(l0, U.uq.half(s))), Equal.cong(Nat, Nat, z => Nat.sub(z, l0), m, U32.to_nat(mid), Equal.sym(Nat, U32.to_nat(mid), m, eM)))
1323      +jz = Q.bq.lt_rw(U.uq.half(s), U.uq.pw(g), Q.bq.s(lo, mid), U.uq.pw(g), e2, {==}, Q.bq.half_lt_pw(s, U.uq.pw(g), hz))
1324      ih(lo, mid, i1, j2, j3, jz)
1325
1326# one halving of [lo, hi): active when lo < hi (c)
1327def ba.adv(c: Bool, +g: Nat, +d: Nat, +l: List<&2, U32>, +hl: {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}, +key: U32, +n: U32, +hN: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}, +hs: {S.bsearch.sorted(Q.bq.pre(l, n)) == True{} : Bool}, +lo: U32, +hi: U32, +ec: {U32.is_lt(lo, hi) == c : Bool}, +i1: {Nat.is_le(U32.to_nat(lo), Q.bq.lb(l, n, key)) == True{} : Bool}, +i2: {Nat.is_le(Q.bq.lb(l, n, key), U32.to_nat(hi)) == True{} : Bool}, +i3: {Nat.is_le(U32.to_nat(hi), U32.to_nat(n)) == True{} : Bool}, +hz: {Nat.is_lt(Q.bq.s(lo, hi), U.uq.pw(1n+g)) == True{} : Bool}, ih: @lo2: U32 -> @hi2: U32 -> @j1: {Nat.is_le(U32.to_nat(lo2), Q.bq.lb(l, n, key)) == True{} : Bool} -> @j2: {Nat.is_le(Q.bq.lb(l, n, key), U32.to_nat(hi2)) == True{} : Bool} -> @j3: {Nat.is_le(U32.to_nat(hi2), U32.to_nat(n)) == True{} : Bool} -> @jz: {Nat.is_lt(Q.bq.s(lo2, hi2), U.uq.pw(g)) == True{} : Bool} -> {U32.to_nat(Q.bq.run(g, d, l, lo2, hi2, key)) == Q.bq.lb(l, n, key) : Nat}) -> {U32.to_nat(Q.bq.run(g, d, l, Q.bq.nlo.a(c, U32.is_lt(Q.bq.x(d, l, lo, hi), key), lo, Q.bq.mid(lo, hi)), Q.bq.nhi.a(c, U32.is_lt(Q.bq.x(d, l, lo, hi), key), hi, Q.bq.mid(lo, hi)), key)) == Q.bq.lb(l, n, key) : Nat}:
1328  match c:
1329    case False{}:
1330      +h0 = U32.to_nat(hi)
1331      +l0 = U32.to_nat(lo)
1332      +e0 = Q.bq.sub_le0(h0, l0, Q.bq.not_lt(l0, h0, u32.mv_lt(lo, hi, False{}, ec)))
1333      ih(lo, hi, i1, i2, i3, Q.bq.lt_rw(0n, U.uq.pw(g), Q.bq.s(lo, hi), U.uq.pw(g), Equal.sym(Nat, Q.bq.s(lo, hi), 0n, e0), {==}, Q.bq.pw_pos(g)))
1334    case True{}:
1335      +h0 = U32.to_nat(hi)
1336      +l0 = U32.to_nat(lo)
1337      +s = Q.bq.s(lo, hi)
1338      +m = Q.bq.m(lo, hi)
1339      +mid = Q.bq.mid(lo, hi)
1340      +lb = Q.bq.lb(l, n, key)
1341      +sh = U32.to_nat(U32.shr(U32.sub(hi, lo)))
1342      +hlt = u32.mv_lt(lo, hi, True{}, ec)
1343      +hle = Q.bq.lt_le(l0, h0, hlt)
1344      +eD = U.uq.u32_sub(hi, lo, hle)
1345      +eE = Equal.trans(Nat, sh, U.uq.half(U32.to_nat(U32.sub(hi, lo))), U.uq.half(s), U.uq.u32_shr(U32.sub(hi, lo)), Equal.cong(Nat, Nat, z => U.uq.half(z), U32.to_nat(U32.sub(hi, lo)), s, eD))
1346      +ehs = Q.bq.add_sub(l0, h0, hle)
1347      +hmh = Q.bq.lt_rw(Nat.add(l0, U.uq.half(s)), Nat.add(l0, s), m, h0, {==}, ehs, Equal.trans(Bool, Nat.is_lt(Nat.add(l0, U.uq.half(s)), Nat.add(l0, s)), Nat.is_lt(U.uq.half(s), s), True{}, Q.bq.lt_cancel(l0, U.uq.half(s), s), Q.bq.half_lt(s, Q.bq.sub_pos(l0, h0, hlt))))
1348      +hadd = Q.bq.le_rw(m, h0, Nat.add(l0, sh), h0, Equal.cong(Nat, Nat, z => Nat.add(l0, z), U.uq.half(s), sh, Equal.sym(Nat, sh, U.uq.half(s), eE)), {==}, Q.bq.lt_le(m, h0, hmh))
1349      +eM = Equal.trans(Nat, U32.to_nat(mid), Nat.add(l0, sh), m, U.uq.u32_add(lo, U32.shr(U32.sub(hi, lo)), hi, hadd), Equal.cong(Nat, Nat, z => Nat.add(l0, z), sh, U.uq.half(s), eE))
1350      +hmN = Q.bq.lt_le_trans(m, h0, U32.to_nat(n), hmh, i3)
1351      %Equal.sym(Bool, U32.is_lt(Q.bq.x(d, l, lo, hi), key), Nat.is_lt(m, lb), ba.key_cmp(d, l, hl, key, n, hN, hs, mid, m, eM, hmN)) : {U32.to_nat(Q.bq.run(g, d, l, Q.bq.lo_b(_, lo, mid), Q.bq.hi_b(_, hi, mid), key)) == lb : Nat}
1352      ba.adv2(Nat.is_lt(m, lb), g, d, l, key, n, lo, hi, {==}, i1, i2, i3, hz, eM, ehs, hmh, ih)
1353
1354# f halvings from lo <= LB <= hi <= n with hi - lo < 2^f end at LB
1355def ba.run(f: Nat, +d: Nat, +l: List<&2, U32>, +hl: {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}, +key: U32, +n: U32, +hN: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}, +hs: {S.bsearch.sorted(Q.bq.pre(l, n)) == True{} : Bool}, +lo: U32, +hi: U32, +i1: {Nat.is_le(U32.to_nat(lo), Q.bq.lb(l, n, key)) == True{} : Bool}, +i2: {Nat.is_le(Q.bq.lb(l, n, key), U32.to_nat(hi)) == True{} : Bool}, +i3: {Nat.is_le(U32.to_nat(hi), U32.to_nat(n)) == True{} : Bool}, +hz: {Nat.is_lt(Q.bq.s(lo, hi), U.uq.pw(f)) == True{} : Bool}) -> {U32.to_nat(Q.bq.run(f, d, l, lo, hi, key)) == Q.bq.lb(l, n, key) : Nat}:
1356  match f:
1357    case 0n:
1358      +l0 = U32.to_nat(lo)
1359      +h0 = U32.to_nat(hi)
1360      +lb = Q.bq.lb(l, n, key)
1361      Q.bq.le_antisym(l0, lb, i1, Q.bq.le_trans(lb, h0, l0, i2, Q.bq.sub0_le(h0, l0, Q.bq.lt_one(Q.bq.s(lo, hi), hz))))
1362    case 1n+ +g:
1363      ba.adv(U32.is_lt(lo, hi), g, d, l, hl, key, n, hN, hs, lo, hi, {==}, i1, i2, i3, hz, lo2 => hi2 => j1 => j2 => j3 => jz => ba.run(g, d, l, hl, key, n, hN, hs, lo2, hi2, j1, j2, j3, jz))
1364
1365# n < 2^32 < 2^33: the 33 halvings suffice (stated so that 2^33 is never
1366# expanded)
1367def ba.hz33(n: U32) -> {Nat.is_lt(Q.bq.s(0, n), U.uq.pw(33n)) == True{} : Bool}:
1368  match n:
1369    case U32{+w}:
1370      U.uq.lt_succ_pw(32n, 33n, {==}, Word.to_nat(32n, w), Q.bq.s(0, U32{w}), Equal.sym(Nat, Nat.sub(Word.to_nat(32n, w), 0n), Word.to_nat(32n, w), Q.bq.sub_zero(Word.to_nat(32n, w))), U.uq.val_lt(32n, w))
1371
1372# the lower bound is at most n
1373def ba.lb_le(-d: Nat, +l: List<&2, U32>, +n: U32, +key: U32, +hl: {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}, +hn: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}) -> {Nat.is_le(Q.bq.lb(l, n, key), U32.to_nat(n)) == True{} : Bool}:
1374  Q.bq.le_rw(Q.bq.lb(l, n, key), List.length(&2, U32, Q.bq.pre(l, n)), Q.bq.lb(l, n, key), U32.to_nat(n), {==}, Q.bq.len_take(l, U32.to_nat(n), Q.bq.le_rw(U32.to_nat(n), AR.Arrays.slots(d), U32.to_nat(n), List.length(&2, U32, l), {==}, Equal.sym(Nat, List.length(&2, U32, l), AR.Arrays.slots(d), hl), hn)), Laws.lower_bound_le_length(Q.bq.pre(l, n), key))
1375
1376# the search's answer is the lower bound
1377def ba.answer(+d: Nat, +l: List<&2, U32>, +hl: {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}, +key: U32, +n: U32, +hn: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}, +hs: {S.bsearch.sorted(Q.bq.pre(l, n)) == True{} : Bool}) -> {U32.to_nat(Q.bq.run(33n, d, l, 0, n, key)) == Q.bq.lb(l, n, key) : Nat}:
1378  ba.run(33n, d, l, hl, key, n, hn, hs, 0, n, Q.bq.le_zero(Q.bq.lb(l, n, key)), ba.lb_le(d, l, n, key, hl, hn), Q.bq.le_refl(U32.to_nat(n)), ba.hz33(n))
1379
1380# a sorted prefix of the reflected array is a sorted prefix of l
1381def ba.hs(+d: Nat, -a: Array<U32>, +l: List<&2, U32>, +n: U32, e1: {AR.Arrays.of_list(U32, d, l, 0) == a : Array<U32>}, +hl: {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}, hs: {S.bsearch.sorted(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n))) == True{} : Bool}) -> {S.bsearch.sorted(Q.bq.pre(l, n)) == True{} : Bool}:
1382  %AL.of_list_leaves(U32, d, l, 0, hl) : {S.bsearch.sorted(List.take(&2, U32, _, U32.to_nat(n))) == True{} : Bool}
1383  %Equal.sym(Array<U32>, AR.Arrays.of_list(U32, d, l, 0), a, e1) : {S.bsearch.sorted(List.take(&2, U32, AR.Arrays.leaves(U32, _), U32.to_nat(n))) == True{} : Bool}
1384  hs
1385
1386# The find: the element at the lower bound, if it is inside the first n
1387
1388def ba.hit(b: Bool, +r: U32, +lb: Nat, +er: {U32.to_nat(r) == lb : Nat}) -> {Laws.algo_index_nat(Bool.pick(Maybe<&2, U32>, b, Some{r}, None{})) == S.bsearch.find.hit(b, lb) : Maybe<&2, Nat>}:
1389  match b:
1390    case True{}:
1391      Equal.cong(Nat, Maybe<&2, Nat>, z => Some{z}, U32.to_nat(r), lb, er)
1392    case False{}:
1393      {==}
1394
1395def ba.fd(c: Bool, +d: Nat, +l: List<&2, U32>, +hl: {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}, +key: U32, +n: U32, +hn: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}, +r: U32, +ec: {U32.is_lt(r, n) == c : Bool}, +er: {U32.to_nat(r) == Q.bq.lb(l, n, key) : Nat}) -> {Laws.algo_index_nat(Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array.found(c, (AR.Arrays.of_list(U32, d, l, 0), AR.Arrays.nth(U32, l, AR.Arrays.index(d, r), 0)), r, key))) == S.bsearch.find(Q.bq.pre(l, n), key) : Maybe<&2, Nat>}:
1396  match c:
1397    case True{}:
1398      +lb = Q.bq.lb(l, n, key)
1399      +nn = U32.to_nat(n)
1400      +pre = Q.bq.pre(l, n)
1401      +hnl = Q.bq.le_rw(nn, AR.Arrays.slots(d), nn, List.length(&2, U32, l), {==}, Equal.sym(Nat, List.length(&2, U32, l), AR.Arrays.slots(d), hl), hn)
1402      +hc = Equal.trans(Bool, Nat.is_lt(lb, nn), Nat.is_lt(U32.to_nat(r), nn), True{}, Equal.cong(Nat, Bool, z => Nat.is_lt(z, nn), lb, U32.to_nat(r), Equal.sym(Nat, U32.to_nat(r), lb, er)), u32.mv_lt(r, n, True{}, ec))
1403      +hls = Q.bq.lt_le_trans(lb, nn, AR.Arrays.slots(d), hc, hn)
1404      +ei = Equal.trans(Nat, AR.Arrays.index(d, r), U32.to_nat(r), lb, AL.index_of_u32(d, r, Q.bq.lt_rw(lb, AR.Arrays.slots(d), U32.to_nat(r), AR.Arrays.slots(d), Equal.sym(Nat, U32.to_nat(r), lb, er), {==}, hls)), er)
1405      +hll = Q.bq.lt_rw(lb, AR.Arrays.slots(d), lb, List.length(&2, U32, l), {==}, Equal.sym(Nat, List.length(&2, U32, l), AR.Arrays.slots(d), hl), hls)
1406      +eg = Equal.trans(Maybe<&2, U32>, List.get(&2, U32, pre, lb), List.get(&2, U32, l, lb), Some{AR.Arrays.nth(U32, l, lb, 0)}, Q.bq.get_take(l, nn, lb, hc), Q.bq.get_nth(l, lb, hll))
1407      %Equal.sym(Nat, AR.Arrays.index(d, r), lb, ei) : {Laws.algo_index_nat(Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array.found(True{}, (AR.Arrays.of_list(U32, d, l, 0), AR.Arrays.nth(U32, l, _, 0)), r, key))) == S.bsearch.find(pre, key) : Maybe<&2, Nat>}
1408      %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, pre, lb), Some{AR.Arrays.nth(U32, l, lb, 0)}, eg) : {Laws.algo_index_nat(Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array.found(True{}, (AR.Arrays.of_list(U32, d, l, 0), AR.Arrays.nth(U32, l, lb, 0)), r, key))) == S.bsearch.find.check(lb, _, key) : Maybe<&2, Nat>}
1409      ba.hit(U32.is_eq(AR.Arrays.nth(U32, l, lb, 0), key), r, lb, er)
1410    case False{}:
1411      +lb = Q.bq.lb(l, n, key)
1412      +nn = U32.to_nat(n)
1413      +pre = Q.bq.pre(l, n)
1414      +hnl = Q.bq.le_rw(nn, AR.Arrays.slots(d), nn, List.length(&2, U32, l), {==}, Equal.sym(Nat, List.length(&2, U32, l), AR.Arrays.slots(d), hl), hn)
1415      +hc = Equal.trans(Bool, Nat.is_lt(lb, nn), Nat.is_lt(U32.to_nat(r), nn), False{}, Equal.cong(Nat, Bool, z => Nat.is_lt(z, nn), lb, U32.to_nat(r), Equal.sym(Nat, U32.to_nat(r), lb, er)), u32.mv_lt(r, n, False{}, ec))
1416      +eln = Q.bq.le_antisym(lb, nn, ba.lb_le(d, l, n, key, hl, hn), Q.bq.not_lt(lb, nn, hc))
1417      +eg = Equal.trans(Maybe<&2, U32>, List.get(&2, U32, pre, lb), List.get(&2, U32, pre, List.length(&2, U32, pre)), None{}, Equal.cong(Nat, Maybe<&2, U32>, z => List.get(&2, U32, pre, z), lb, List.length(&2, U32, pre), Equal.trans(Nat, lb, nn, List.length(&2, U32, pre), eln, Equal.sym(Nat, List.length(&2, U32, pre), nn, Q.bq.len_take(l, nn, hnl)))), Q.bq.get_len(pre))
1418      %Equal.sym(Maybe<&2, U32>, List.get(&2, U32, pre, lb), None{}, eg) : {Laws.algo_index_nat(Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array.found(False{}, (AR.Arrays.of_list(U32, d, l, 0), AR.Arrays.nth(U32, l, AR.Arrays.index(d, r), 0)), r, key))) == S.bsearch.find.check(lb, _, key) : Maybe<&2, Nat>}
1419      {==}
1420
1421def ba.fs(c: Bool, -a0: Array<U32>, -x: U32, +r: U32, +key: U32) -> {Pair.fst(Array<U32>, Maybe<&2, U32>, S.bsearch.array.found(c, (a0, x), r, key)) == a0 : Array<U32>}:
1422  match c:
1423    case True{}:
1424      {==}
1425    case False{}:
1426      {==}
1427
1428# The laws, each on its array reflected
1429
1430def ba.lb.body(+d: Nat, -a: Array<U32>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +n: U32, +hn: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}, +key: U32, hs: {S.bsearch.sorted(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n))) == True{} : Bool}, +l: List<&2, U32>, +e1: {AR.Arrays.of_list(U32, d, l, 0) == a : Array<U32>}, +hl: {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}) -> {U32.to_nat(Pair.snd(Array<U32>, U32, S.bsearch.array_lower_bound(a, n, key))) == S.bsearch.lower_bound(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n)), key) : Nat}:
1431  -ol = AR.Arrays.of_list(U32, d, l, 0)
1432  %e1 : {U32.to_nat(Pair.snd(Array<U32>, U32, S.bsearch.array_lower_bound(_, n, key))) == S.bsearch.lower_bound(List.take(&2, U32, AR.Arrays.leaves(U32, _), U32.to_nat(n)), key) : Nat}
1433  %Equal.sym(List<&2, U32>, AR.Arrays.leaves(U32, ol), l, AL.of_list_leaves(U32, d, l, 0, hl)) : {U32.to_nat(Pair.snd(Array<U32>, U32, S.bsearch.array_lower_bound(ol, n, key))) == S.bsearch.lower_bound(List.take(&2, U32, _, U32.to_nat(n)), key) : Nat}
1434  %Equal.sym(Array<U32> & U32, S.bsearch.array.go(33n, S.BsearchState{ol, 0, n}, key), (ol, Q.bq.run(33n, d, l, 0, n, key)), Q.bq.go(33n, d, l, hl, hd, 0, n, key)) : {U32.to_nat(Pair.snd(Array<U32>, U32, _)) == Q.bq.lb(l, n, key) : Nat}
1435  ba.answer(d, l, hl, key, n, hn, ba.hs(d, a, l, n, e1, hl, hs))
1436
1437def ba.lb.ref(+d: Nat, -a: Array<U32>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +n: U32, +hn: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}, +key: U32, hs: {S.bsearch.sorted(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n))) == True{} : Bool}, r: &l: List<&2, U32> -> {AR.Arrays.of_list(U32, d, l, 0) == a : Array<U32>} & {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}) -> {U32.to_nat(Pair.snd(Array<U32>, U32, S.bsearch.array_lower_bound(a, n, key))) == S.bsearch.lower_bound(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n)), key) : Nat}:
1438  (l, e) = r
1439  (e1, hl) = e
1440  ba.lb.body(d, a, hd, n, hn, key, hs, l, e1, hl)
1441
1442def ba.lbs.body(+d: Nat, -a: Array<U32>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +n: U32, +key: U32, +l: List<&2, U32>, +e1: {AR.Arrays.of_list(U32, d, l, 0) == a : Array<U32>}, +hl: {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}) -> {Pair.fst(Array<U32>, U32, S.bsearch.array_lower_bound(a, n, key)) == a : Array<U32>}:
1443  -ol = AR.Arrays.of_list(U32, d, l, 0)
1444  %e1 : {Pair.fst(Array<U32>, U32, S.bsearch.array_lower_bound(_, n, key)) == _ : Array<U32>}
1445  %Equal.sym(Array<U32> & U32, S.bsearch.array.go(33n, S.BsearchState{ol, 0, n}, key), (ol, Q.bq.run(33n, d, l, 0, n, key)), Q.bq.go(33n, d, l, hl, hd, 0, n, key)) : {Pair.fst(Array<U32>, U32, _) == ol : Array<U32>}
1446  {==}
1447
1448def ba.lbs.ref(+d: Nat, -a: Array<U32>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +n: U32, +key: U32, r: &l: List<&2, U32> -> {AR.Arrays.of_list(U32, d, l, 0) == a : Array<U32>} & {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}) -> {Pair.fst(Array<U32>, U32, S.bsearch.array_lower_bound(a, n, key)) == a : Array<U32>}:
1449  (l, e) = r
1450  (e1, hl) = e
1451  ba.lbs.body(d, a, hd, n, key, l, e1, hl)
1452
1453def ba.fl.body(+d: Nat, -a: Array<U32>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +n: U32, +hn: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}, +key: U32, hs: {S.bsearch.sorted(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n))) == True{} : Bool}, +l: List<&2, U32>, +e1: {AR.Arrays.of_list(U32, d, l, 0) == a : Array<U32>}, +hl: {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}) -> {Laws.algo_index_nat(Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array_find(a, n, key))) == S.bsearch.find(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n)), key) : Maybe<&2, Nat>}:
1454  -ol = AR.Arrays.of_list(U32, d, l, 0)
1455  +r = Q.bq.run(33n, d, l, 0, n, key)
1456  %e1 : {Laws.algo_index_nat(Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array_find(_, n, key))) == S.bsearch.find(List.take(&2, U32, AR.Arrays.leaves(U32, _), U32.to_nat(n)), key) : Maybe<&2, Nat>}
1457  %Equal.sym(List<&2, U32>, AR.Arrays.leaves(U32, ol), l, AL.of_list_leaves(U32, d, l, 0, hl)) : {Laws.algo_index_nat(Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array_find(ol, n, key))) == S.bsearch.find(List.take(&2, U32, _, U32.to_nat(n)), key) : Maybe<&2, Nat>}
1458  %Equal.sym(Array<U32> & U32, S.bsearch.array.go(33n, S.BsearchState{ol, 0, n}, key), (ol, r), Q.bq.go(33n, d, l, hl, hd, 0, n, key)) : {Laws.algo_index_nat(Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array.find(_, n, key))) == S.bsearch.find(Q.bq.pre(l, n), key) : Maybe<&2, Nat>}
1459  %Equal.sym(Array<U32> & U32, Array.get(U32, ol, r), (ol, AR.Arrays.nth(U32, l, AR.Arrays.index(d, r), 0)), AL.of_list_get(U32, d, l, 0, hl, hd, r)) : {Laws.algo_index_nat(Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array.found(U32.is_lt(r, n), _, r, key))) == S.bsearch.find(Q.bq.pre(l, n), key) : Maybe<&2, Nat>}
1460  ba.fd(U32.is_lt(r, n), d, l, hl, key, n, hn, r, {==}, ba.answer(d, l, hl, key, n, hn, ba.hs(d, a, l, n, e1, hl, hs)))
1461
1462def ba.fl.ref(+d: Nat, -a: Array<U32>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +n: U32, +hn: {Nat.is_le(U32.to_nat(n), AR.Arrays.slots(d)) == True{} : Bool}, +key: U32, hs: {S.bsearch.sorted(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n))) == True{} : Bool}, r: &l: List<&2, U32> -> {AR.Arrays.of_list(U32, d, l, 0) == a : Array<U32>} & {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}) -> {Laws.algo_index_nat(Pair.snd(Array<U32>, Maybe<&2, U32>, S.bsearch.array_find(a, n, key))) == S.bsearch.find(List.take(&2, U32, AR.Arrays.leaves(U32, a), U32.to_nat(n)), key) : Maybe<&2, Nat>}:
1463  (l, e) = r
1464  (e1, hl) = e
1465  ba.fl.body(d, a, hd, n, hn, key, hs, l, e1, hl)
1466
1467def ba.fls.body(+d: Nat, -a: Array<U32>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +n: U32, +key: U32, +l: List<&2, U32>, +e1: {AR.Arrays.of_list(U32, d, l, 0) == a : Array<U32>}, +hl: {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}) -> {Pair.fst(Array<U32>, Maybe<&2, U32>, S.bsearch.array_find(a, n, key)) == a : Array<U32>}:
1468  -ol = AR.Arrays.of_list(U32, d, l, 0)
1469  +r = Q.bq.run(33n, d, l, 0, n, key)
1470  %e1 : {Pair.fst(Array<U32>, Maybe<&2, U32>, S.bsearch.array_find(_, n, key)) == _ : Array<U32>}
1471  %Equal.sym(Array<U32> & U32, S.bsearch.array.go(33n, S.BsearchState{ol, 0, n}, key), (ol, r), Q.bq.go(33n, d, l, hl, hd, 0, n, key)) : {Pair.fst(Array<U32>, Maybe<&2, U32>, S.bsearch.array.find(_, n, key)) == ol : Array<U32>}
1472  %Equal.sym(Array<U32> & U32, Array.get(U32, ol, r), (ol, AR.Arrays.nth(U32, l, AR.Arrays.index(d, r), 0)), AL.of_list_get(U32, d, l, 0, hl, hd, r)) : {Pair.fst(Array<U32>, Maybe<&2, U32>, S.bsearch.array.found(U32.is_lt(r, n), _, r, key)) == ol : Array<U32>}
1473  ba.fs(U32.is_lt(r, n), ol, AR.Arrays.nth(U32, l, AR.Arrays.index(d, r), 0), r, key)
1474
1475def ba.fls.ref(+d: Nat, -a: Array<U32>, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +n: U32, +key: U32, r: &l: List<&2, U32> -> {AR.Arrays.of_list(U32, d, l, 0) == a : Array<U32>} & {List.length(&2, U32, l) == AR.Arrays.slots(d) : Nat}) -> {Pair.fst(Array<U32>, Maybe<&2, U32>, S.bsearch.array_find(a, n, key)) == a : Array<U32>}:
1476  (l, e) = r
1477  (e1, hl) = e
1478  ba.fls.body(d, a, hd, n, key, l, e1, hl)
1479
1480def Laws.array_lower_bound_list(d, a, hp, hd, n, hn, key, hs):
1481  ba.lb.ref(d, a, hd, n, hn, key, hs, AL.reflect(U32, d, a, hp, 0))
1482
1483def Laws.array_lower_bound_same(d, a, hp, hd, n, key):
1484  ba.lbs.ref(d, a, hd, n, key, AL.reflect(U32, d, a, hp, 0))
1485
1486def Laws.array_find_list(d, a, hp, hd, n, hn, key, hs):
1487  ba.fl.ref(d, a, hd, n, hn, key, hs, AL.reflect(U32, d, a, hp, 0))
1488
1489def Laws.array_find_same(d, a, hp, hd, n, key):
1490  ba.fls.ref(d, a, hd, n, key, AL.reflect(U32, d, a, hp, 0))
1491
1492def Laws.wit_array_bsearch():
1493  {==}