def bs.some.h

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

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

1170def bs.some.h(c: Bool, x: U32, key: U32, ec: {U32.is_eq(x, key) == c : Bool}, +xs: List<&2, U32>, +lb: Nat, +i: Nat, e: {S.bsearch.find.hit(c, lb) == Some{i} : Maybe<&2, Nat>}, g: {List.get(&2, U32, xs, lb) == Some{x} : Maybe<&2, U32>}) -> {List.get(&2, U32, xs, i) == Some{key} : Maybe<&2, U32>}:
1171  match c:
1172    case True{}:
1173      %some_inj(lb, i, e) : {List.get(&2, U32, xs, _) == Some{key} : Maybe<&2, U32>}
1174      %u32.eq(x, key, ec) : {List.get(&2, U32, xs, lb) == Some{_} : Maybe<&2, U32>}
1175      g
1176    case False{}:
1177      Empty.absurd({List.get(&2, U32, xs, i) == Some{key} : Maybe<&2, U32>}, absurd.ns(i, e))