PROOF.ba.kc: def of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF
Lines 1270-1276 of bend-osdev-algo@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&start_line=1270&end_line=1276

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

# the element read at m is below the key exactly when m is below LB
def 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}:
  match b:
    case True{}:
      bs.below(Q.bq.pre(l, n), key, m, AR.Arrays.nth(U32, l, m, 0), eg, eb)
    case False{}:
      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))

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bs.above
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=bs.below
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/bsearch.bend&name=bsearch.sorted
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.lb
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.not_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.pre
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.nth