-- =================================================================================================
-- unions for standard reductions
-- =================================================================================================

-- =====================================================
-- lbeta-reductions

union (SR,lbeta,0)          = { (SR,lbeta,1), (SR,lbeta,2), (SR,lbeta,3) }

-- =====================================================
-- cp-reductions
--
union (SR,cp-in,0)          = { (SR,cp-in,1)}
union (SR,cp-e,0)           = { (SR,cp-e,1)}
union (SR,cp,0)             = { (SR,cp-in,0), (SR,cp-e,0) }
-- =====================================================


-- =====================================================
-- lll-reductions
--

union (SR,llet-e,0)         = { (SR,llet-e,1),(SR,llet-e,2) }
union (SR,llet,0)           = { (SR,llet-in,1), (SR,llet-e,0) }
union (SR,lapp,0)           = { (SR,lapp,1), (SR,lapp,2), (SR,lapp,3) }
union (SR,lcaselist,0)      = { (SR,lcaselist,1), (SR,lcaselist,2), (SR,lcaselist,3) }
union (SR,lcasebool,0)      = { (SR,lcasebool,1), (SR,lcasebool,2), (SR,lcasebool,3) }
union (SR,lcasepair,0)      = { (SR,lcasepair,1), (SR,lcasepair,2), (SR,lcasepair,3) }
union (SR,lcase,0)          = { (SR,lcaselist,0), (SR,lcasebool,0), (SR,lcasepair,0) }
union (SR,lseq,0)           = { (SR,lseq,1), (SR,lseq,2), (SR,lseq,3) }
union (SR,lll,+,0)          = { (SR,lll,+,1),(SR,lll,+,2),(SR,lll,+,3) }



-- =====================================================
-- case-reductions
--
union (SR,caselist-c,0)     = {(SR,caselist-c,1),(SR,caselist-c,2),(SR,caselist-c,3),(SR,caselist-c,4),(SR,caselist-c,5),(SR,caselist-c,6)}
union (SR,casebool-c,0)     = {(SR,casebool-c,1),(SR,casebool-c,2),(SR,casebool-c,3),(SR,casebool-c,4),(SR,casebool-c,5),(SR,casebool-c,6)}
union (SR,casepair-c,0)     = {(SR,casepair-c,1),(SR,casepair-c,2),(SR,casepair-c,3)}
union (SR,case-c,0)         = {(SR,caselist-c,0),(SR,casebool-c,0),(SR,casepair-c,0)}

union (SR,caselist-in,0)    = {(SR,caselist-in,1),(SR,caselist-in,2)}
union (SR,casebool-in,0)    = {(SR,casebool-in,1),(SR,casebool-in,2)}
union (SR,casepair-in,0)    = {(SR,casepair-in,1)}
union (SR,case-in,0)        = {(SR,caselist-in,0),(SR,casebool-in,0),(SR,casepair-in,0)}

union (SR,caselist-e,0)     = {(SR,caselist-e,1),(SR,caselist-e,2)}
union (SR,casebool-e,0)     = {(SR,casebool-e,1),(SR,casebool-e,2)}
union (SR,casepair-e,0)     = {(SR,casepair-e,1)}
union (SR,case-e,0)         = {(SR,caselist-e,0),(SR,casebool-e,0),(SR,casepair-e,0)}

union (SR,case,0)           = {(SR,case-c,0), (SR,case-in,0), (SR,case-e,0)}
--
-- =====================================================
-- seq-reductions
--

union (SR,seq-c,0)          = {(SR,seq-c,1),(SR,seq-c,2),(SR,seq-c,3),(SR,seq-c,4),(SR,seq-c,5),(SR,seq-c,6),(SR,seq-c,7),(SR,seq-c,8),(SR,seq-c,9),(SR,seq-c,10),
                               (SR,seq-c,11),(SR,seq-c,12),(SR,seq-c,13),(SR,seq-c,14),(SR,seq-c,15),(SR,seq-c,16),(SR,seq-c,17),(SR,seq-c,18)}
union (SR,seq-in,0)         = {(SR,seq-in,1),(SR,seq-in,2),(SR,seq-in,3),(SR,seq-in,4),(SR,seq-in,5)}
union (SR,seq-e,0)          = {(SR,seq-e,1),(SR,seq-e,2),(SR,seq-e,3),(SR,seq-e,4),(SR,seq-e,5)}
union (SR,seq,0)            = {(SR,seq-c,0),(SR,seq-in,0),(SR,seq-e,0)}


-- =================================================================================================
-- unions for transformations
-- =================================================================================================

-- =====================================================
-- cpcx 

union (cpcx-in,0)           = {(cpcx-in,1),(cpcx-in,2),(cpcx-in,3),(cpcx-in,4),(cpcx-in,5)}
union (cpcx-e,0)            = {(cpcx-e,1),(cpcx-e,2),(cpcx-e,3),(cpcx-e,4),(cpcx-e,5)
                               ,(cpcx-e,6),(cpcx-e,7),(cpcx-e,8),(cpcx-e,9),(cpcx-e,10)}
union (cpcx,0)              = {(cpcx-in,0),(cpcx-e,0)}

-- =====================================================
-- case
union (caselist-c,0)        = {(caselist-c,1),(caselist-c,2)}                    
union (casebool-c,0)        = {(casebool-c,1),(casebool-c,2)}
union (case-c,0)            = {(caselist-c,0),(casebool-c,0),(casepair-c,1)}

-- =====================================================
-- seq
union (seq-c,0)             = {(seq-c,1),(seq-c,2),(seq-c,3),(seq-c,4),(seq-c,5),(seq-c,6)}


-- =====================================================
-- abs

union (abs,0)               = {(abs,1),(abs,2)}

-- =====================================================
-- cpd

union (cpd,0)               = {(cpd-in,1), (cpd-e,1), (cpd-e,2) }

-- =====================================================
-- cpT
union (cpT,0)               = {(cpT-in,1), (cpT-e,1), (cpT-e,2) }


-- =====================================================
-- lll
union (llet,0)              = { (llet-in,1), (llet-e,1) } 

-- =====================================================
-- ucp 
union (ucp,0)               = { (ucp,1), (ucp,2), (ucp,3)}

-- =====================================================
-- gc 

union (gc,0)                = { (gc,1), (gc,2) }

-- =====================================================
-- cpx
union (cpx-e,0)             = { (cpx-e,1), (cpx-e,2) }
union (cpx,0)               = { (cpx-e,0), (cpx-in,1) }


union (lcase,0) = {(lcasepair,1),(lcaselist,1),(lcasebool,1)}


-- to ensure termination of the (lll)-diagrams we cannot use the union
-- of (lll), thus we expand (SR,lll)-steps to all possibilites.
-- The following rules will add special diagrams for this:
-- --SR,lll--> ~~~> SR,lapp
-- --SR,lll--> ~~~> SR,lcase
-- --SR,lll--> ~~~> SR,lseq
-- --SR,lll--> ~~~> SR,llet
-- This is necessary since we cannot omit the special (SR,lll,+) reductions
-- and they cannot easily represented by (SR,lapp),... reductions

expand (SR,lll,0) = {(SR,lseq,0),(SR,lapp,0),(SR,llet,0),(SR,lcase,0)}