SetByBSTMap

Signature of SetByBSTMap

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

/*  %The mapping functions on sets. */
SIGNATURE SetByBSTMap[from ,< :from ** from -> bool, to, < :to ** to -> bool]

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

IMPORT SetByBST[from, <] ONLY set
       SetByBST[to, <]   ONLY set

Parameter

from is the element type of the source set, to that of the target set. < is a total strict order on the respective type: the formula ALL x y. ~(x < y) AND ~(y < x) => x === y must hold.

SORT from to

FUN < : from ** from -> bool
FUN < : to ** to -> bool

-- $Mapping$

Apply a function to all elements of a set. Note that the set size may decrease, if the function is not injective on the set elements.

FUN * : (from -> to)** set[from, <] -> set[to, <]

next node: SetByBSTConstr,
prev node: SetByBSTReduce,
up to node: Subsystem Sets By Binary Search Trees