SetByBSTMapEnv

Mappings of sets with an accumulating environment.

Signature of SetByBSTMapEnv

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

SIGNATURE SetByBSTMapEnv[env, from, < :from ** from -> bool,

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

                              to, < :to ** to -> bool]

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 env from to

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

Mapping with an Environment

f * (e,<>) == (e,<>)
f * (e,ft::rt) == (e2,ft1::rt1)
WHERE (e1,ft1) == f(e,ft) (e2,rt1) == f * (e1,rt). The order of elements should not be relevant.

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

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