ProofBsearch.bq.step_eq: def of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as ProofBsearch
Lines 98-103 of bend-osdev-algo@0.1.0.0/proof_bsearch.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&start_line=98&end_line=103

import Base
import bend-osdev-algo@0.1.0.0/bsearch.bend as S

def bq.step_eq(c: Bool, -a: Array<U32>, +x: U32, +key: U32, +lo: U32, +hi: U32, +mid: U32) -> {S.bsearch.array.step(c, (a, x), key, lo, hi, mid) == S.BsearchState{a, bq.nlo.a(c, U32.is_lt(x, key), lo, mid), bq.nhi.a(c, U32.is_lt(x, key), hi, mid)} : S.BsearchState}:
  match c:
    case True{}:
      bq.pick_eq(U32.is_lt(x, key), a, lo, hi, mid)
    case False{}:
      {==}

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  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/bsearch.bend&name=BsearchState
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/bsearch.bend&name=bsearch.array.step
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.nhi.a
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.nlo.a
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_bsearch.bend&name=bq.pick_eq