MapByBSTCompose

Composing Maps

Signature of MapByBSTCompose

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 MapByBSTCompose[dom, < : dom ** dom -> bool, 

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

                     interdom, < : interdom ** interdom -> bool, 
                     codom]

IMPORT MapByBST[dom, <, interdom] ONLY map
       MapByBST[interdom, <, codom] ONLY map
       MapByBST[dom, <, codom] ONLY map

Parameter

The first map maps elements from dom to interdom, the second maps from interdom to codom. The resulting map finally maps elements from dom to codom.

The < are total strict orders: the formula ALL x y. ~(x < y) AND ~(y < x) => x === y must hold.

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

Composing Maps

M1 o M2 = {(d -> r) | EX m. M1!d = m and M2!m = r}

FUN o : map[dom, <, interdom] ** map[interdom, <, codom] -> 
                    map[dom, <, codom]

next node: MapByBSTInvert,
prev node: MapByBSTReduce,
up to node: Subsystem Maps By Binary Search Trees