def bn.h
bend-kit-collections@0.1.4.1 · PROOF.bend:290
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
290def bn.h(
291 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>,
292 +k: K, -v: V, +lo: O.OMap<K, V>, +hi: O.OMap<K, V>,
293 e: {Laws.bounded(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, lb, ub) == True{} : Bool}
294) -> {Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub) == True{} : Bool}:
295 c4.d(Laws.above(~K, ~cmp, lb, k), Laws.below(~K, ~cmp, ub, k),
296 Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}),
297 Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub), e)