PROOF.ba.key_cmp: def of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF
Lines 1278-1284 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=1278&end_line=1284

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-array@0.1.0.0/LAWS.bend as AL
import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as Q

def 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}:
  +hmS = Q.bq.lt_le_trans(m, U32.to_nat(n), AR.Arrays.slots(d), hmN, hN)
  +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)
  +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)
  +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))
  %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}
  ba.kc(Nat.is_lt(m, Q.bq.lb(l, n, key)), l, key, n, hs, m, eg, {==})

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=List.length
  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_le
  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=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/PROOF.bend&name=ba.kc
  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.get_nth
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.get_take
  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.lt_le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.lt_rw
  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/LAWS.bend&name=index_of_u32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.index
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.nth
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.slots