def bn.b
bend-kit-collections@0.1.4.1 · PROOF.bend:272
import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
import Base
import bend-kit-collections@0.1.4.1/LAWS.bend as Laws
import bend-kit-collections@0.1.4.1/omap.bend as O
272def bn.b(
273 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>,
274 +k: K, -v: V, +lo: O.OMap<K, V>, +hi: O.OMap<K, V>,
275 e: {Laws.bounded(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, lb, ub) == True{} : Bool}
276) -> {Laws.below(~K, ~cmp, ub, k) == True{} : Bool}:
277 c4.b(Laws.above(~K, ~cmp, lb, k), Laws.below(~K, ~cmp, ub, k),
278 Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}),
279 Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub), e)