def bn.l

bend-kit-collections@0.1.4.1 · PROOF.bend:281

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

281def bn.l(
282  ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>,
283  +k: K, -v: V, +lo: O.OMap<K, V>, +hi: O.OMap<K, V>,
284  e: {Laws.bounded(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, lb, ub) == True{} : Bool}
285) -> {Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}) == True{} : Bool}:
286  c4.c(Laws.above(~K, ~cmp, lb, k), Laws.below(~K, ~cmp, ub, k),
287    Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}),
288    Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub), e)