~/jendhub

def bn.a

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

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

262# Projections and introduction for bounded on one node.
263def bn.a(
264  ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>,
265  +k: K, -v: V, +lo: O.OMap<K, V>, +hi: O.OMap<K, V>,
266  e: {Laws.bounded(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, lb, ub) == True{} : Bool}
267) -> {Laws.above(~K, ~cmp, lb, k) == True{} : Bool}:
268  c4.a(Laws.above(~K, ~cmp, lb, k), Laws.below(~K, ~cmp, ub, k),
269    Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}),
270    Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub), e)

Uses (8)

Used by (11)