def ba.kc

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

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

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