def bs.above1

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

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

1128def bs.above1(c: Bool, +x0: U32, +x: U32, +key: U32, ec: {U32.is_lt(x0, key) == c : Bool}, +r: Nat, +i: Nat, l: {Nat.is_le(S.bsearch.below.step(c, r), 1n+i) == True{} : Bool}, ih: {Nat.is_le(r, i) == True{} : Bool} -> {U32.is_lt(x, key) == False{} : Bool}, h: {U32.is_le(x0, x) == True{} : Bool}) -> {U32.is_lt(x, key) == False{} : Bool}:
1129  match c:
1130    case True{}:
1131      ih(l)
1132    case False{}:
1133      u32.nlt_le(x0, x, key, ec, h)