next node: MapByOSMap,
prev node: MapByOSConv,
up to node: Subsystem Maps By Ordered Sequences


MapByOSFilter

Signature of MapByOSFilter

List of Import References :
See BOOL
See DENOTATION
See MapByOS
See Nat
See Option
See Pair
See Seq
See Set

SIGNATURE MapByOSFilter[dom, <, codom]

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

--

-- Parameter
SORT dom codom
FUN < : dom ** dom -> bool
        -- total strict-order; in 
        --   ~(x < y) AND ~(y < x) => x = y
        -- should = represent semantic equality

IMPORT MapByOS[dom, <, codom] ONLY map

FUN | : (dom ** codom -> bool) ** map -> map
--  (d -> r) in P|M <=> d->r in M and (P,d,r)

FUN partition : (dom ** codom -> bool) ** map -> map ** map
--  informally: partition(P, M) = (P |M, ~P |M)


next node: MapByOSMap,
prev node: MapByOSConv,
up to node: Subsystem Maps By Ordered Sequences