next node: MapByOS,
prev node: MapByOSCompose,
up to node: Subsystem Maps By Ordered Sequences


MapByOSInvert

Signature of MapByOSInvert

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

SIGNATURE MapByOSInvert[dom,   < : dom ** dom -> bool, 

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

                    codom, < : codom ** codom -> bool]
-- inverting maps

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

IMPORT MapByOS[dom, <, codom] ONLY map
       MapByOS[codom, <, dom] ONLY map

FUN invert: map[dom, <, codom] -> map[codom, <, dom]
-- invert(m)
-- informally invert{(d1->c1), (d2->c2), ... }
--	      = {(c1->d1), (c2->d2), ...}
-- invert is undefined, if m is not injective


next node: MapByOS,
prev node: MapByOSCompose,
up to node: Subsystem Maps By Ordered Sequences