MapByBSTFilter

Filtering of Maps

Signature of MapByBSTFilter

List of Import References :
See BOOL
See BSTree
See DENOTATION
See MapByBST
See Nat
See Option
See Pair
See Seq
See SetByBST
See Tree

SIGNATURE MapByBSTFilter[dom, <, codom]

$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)

IMPORT MapByBST[dom, <, codom] ONLY map

Parameter

dom is the type of the domain, dodom the type of the codomain. < is a total strict order: the formula ALL x y. ~(x < y) AND ~(y < x) => x === y must hold.

SORT dom codom
FUN < : dom ** dom -> bool

Filtering

(d -> r) in P|M <=> d->r in M and (P,d,r)

FUN | : (dom ** codom -> bool) ** map -> map

Informally: partition(P, M) = (P |M, ~P |M)

FUN partition : (dom ** codom -> bool) ** map -> map ** map

next node: MapByBSTMap,
prev node: MapByBSTConv,
up to node: Subsystem Maps By Binary Search Trees