def ba.answer

bend-osdev-algo@0.1.0.0 · PROOF.bend:1376

import Base
import bend-osdev-algo@0.1.0.0/bsearch.bend as S
import bend-osdev-array@0.1.0.0/array.bend as AR
import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as Q

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))