NatMapFilter

Filtering of NatMaps

Signature of NatMapFilter

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

SIGNATURE NatMapFilter[codom]

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

IMPORT NatMap[codom] ONLY natMap
       Nat ONLY nat

Parameter

codom the type of the codomain.

SORT codom

Filtering

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

FUN | : (nat ** codom -> bool) ** natMap -> natMap

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

FUN partition : (nat ** codom -> bool) ** natMap -> natMap ** natMap

next node: NatMapMap,
prev node: NatMapConv,
up to node: Subsystem Mapping Natural Numbers