-- ===============
-- Calculus LR
-- ===============

-- the syntax comprises letrec, variables, abstractions, and applications,
-- case-expressions, data constructors, seq-expressions.
-- For data constructors we only built in 
-- Booleans, Lists, Pairs
-- The LRSX-unification tool automatically detects the abstractions,applications app
-- with the right arity, strictness, and operator arity,
-- for constructors it suffices to provide the strictness 
-- only once, e.g. in cons[] (which means no strict positions).
-- We also use some dummy-constructor for expression non-capture constraints
-- A and T contexts are "built-in" and EE^A[] are chain-variables of A-contexts, and
-- |VV| are chain-variables of the trivial context

-- Thus it suffices to provide the normal order reduction rules and the 
-- the transformation rules.
-- Computing overlaps will import the file as a calculus description

-- =======================
-- normal order reduction
-- =======================

-- ***********************
-- **
-- three cases for (no,lbeta)-redution, corresponding to the reduction contexts 
{SR,lbeta,1}        A[app (\X.S) R]
                    ==> A[letrec X=R in S]
    -- constraints:
    where (R,\X.HOLE)
         ,(R,letrec X=HOLE in S)

{SR,lbeta,2}        letrec E in A[app (\X.S) R]
                    ==> letrec E in A[letrec X=R in S]
    -- constraints:
    where E /= {}
        ,(R,\X.HOLE)
        ,(R,letrec X=HOLE in S)


{SR,lbeta,3}        letrec E; EE^A[X1,app (\X.S) R] in A1[var X1]
                    ==> letrec E; EE^A[X1,letrec X=R in S] in A1[var X1]
    -- constraints:
    where (R,\X.HOLE)
         ,(R,letrec X=HOLE in S)


-- ***********************
-- **   
-- two cases for (no,cp-in)-reduction (without/with variable-to-variable chain)
         
                        
{SR,cp-in,1}        letrec VV|Xn,\X.S|; E in A[var Xn] 
                    ==> letrec  VV|Xn,\X.S|; E in A[\X.S] 


-- **
-- ***********************                    
     
-- ***********************     
-- **                    
-- two cases for (no,cp-e)-reduction (without/with variable-to-variable chain)
                    

                         
{SR,cp-e,1}         letrec VV|Xn,\X.S|; EE^A[Y,A1[var Xn]]; E in A[var Y]
                    ==> letrec  VV|Xn,\X.S|; EE^A[Y,A1[\X.S]]; E in A[var Y] 
    -- constraints:
    where A1 /= []

-- **
-- ***********************                    
     
-- ***********************     
-- **                    
-- (no,llet-in)
    
{SR,llet-in}       letrec E1 in letrec E2 in R
                    ==> letrec E1;E2 in R 
    -- constraints:
    where E1 /= {}
         ,E2 /= {}
         ,[E1,letrec E2 in HOLE]
         
-- **
-- ***********************                    
     
-- ***********************     
-- **                    
-- two cases for (no,llet-e), without/with EE-chain
                        
{SR,llet-e,1}       letrec E1;X=letrec E2 in R in A[var X] 
                    ==> letrec E1;E2;X=R in A[var X] 
    -- constraints:
    where E2 /= {}
        ,[E1,letrec E2 in HOLE]
        ,(A[var X],letrec E2 in HOLE)
        
                          
{SR,llet-e,2}       letrec E1;X=letrec E2 in R;EE^A[Y,var X] in A[var Y] 
                    ==> letrec E1;E2;X=R;EE^A[Y,var X] in A[var Y]     
    -- constraint:
    where E2 /= {}
        ,[E1;EE^A[Y,var X],letrec E2 in HOLE]
        ,(var X,letrec E1;E2;EE^A[Y,var X] in HOLE)
        ,(A[var Y],letrec E2 in HOLE)
         
-- **
-- ***********************                    
     
-- ***********************     
-- **                    
-- three cases for (no,lapp) corresponding to reduction contexts

{SR,lapp,1}         A[app (letrec E in R) S] 
                    ==> A[letrec E in (app R S)] 
    -- constraints:
    where  E /={}
          ,(S,letrec E in HOLE)
                    
{SR,lapp,2}         letrec E1 in A[app (letrec E in R) S] 
                    ==> letrec E1 in A[letrec E in (app R S)]
    -- constraints:                    
    where E1 /= {}
         ,E /={} 
         ,(S,letrec E in HOLE)

{SR,lapp,3}         letrec E1;EE^A[X,app (letrec E in R) S] in A1[var X] 
                    ==> letrec E1;EE^A[X,letrec E in app R S] in A1[var X] 
    -- constraints:
    where E/={}
         ,(S,letrec E in HOLE)


-- **
-- ***********************                    
                   

-- ***********************     
-- **                    
-- three cases for (no,lcase) corresponding to reduction contexts,
-- for each type of case

{SR,lcaselist,1}        A[caselist (letrec E in R) S1 X.XS.S2] 
                        ==> A[letrec E in (caselist R S1 X.XS.S2)] 
    -- constraints:
    where  E /={}
         ,(S1,letrec E in HOLE)
         ,(dummyww[] X.XS.S2 ,letrec E in HOLE)
         ,(var X,dummylist3[] XS.HOLE)
         ,(var XS,dummylist3[] X.HOLE)
                    
{SR,lcaselist,2}        letrec E1 in A[caselist (letrec E in R) S1 X.XS.S2] 
                        ==> letrec E1 in A[letrec E in (caselist R S1 X.XS.S2)] 
    -- constraints:
    where E1 /= {}
        , E /={} 
        ,(S1,letrec E in HOLE)
        ,(dummyww[] X.XS.S2,letrec E in HOLE)
         ,(var X,dummylist3[] XS.HOLE)
         ,(var XS,dummylist3[] X.HOLE)

{SR,lcaselist,3}        letrec E1;EE^A[X,caselist (letrec E in R) S1 Y.YS.S2] in A1[var X] 
                        ==> letrec E1;EE^A[X,letrec E in caselist R S1 Y.YS.S2] in A1[var X] 
    -- constraints:
    where E/={}
        ,(S1,letrec E in HOLE)
        ,(dummyww[] Y.YS.S2,letrec E in HOLE)
        ,(var Y,dummylist3[] YS.HOLE)
        ,(var YS,dummylist3[] Y.HOLE)

{SR,lcasebool,1}        A[casebool (letrec E in R) S1 S2] 
                        ==> A[letrec E in (casebool R S1 S2)] 
    -- constraints:
    where  E /={}
         ,(S1,letrec E in HOLE)
         ,(S2,letrec E in HOLE)
                    
{SR,lcasebool,2}        letrec E1 in A[casebool (letrec E in R) S1 S2] 
                        ==> letrec E1 in A[letrec E in (casebool R S1 S2)]
    -- constraints:
    where E1 /= {}
        , E /={} 
        ,(S1,letrec E in HOLE)
        ,(S2,letrec E in HOLE)

{SR,lcasebool,3}        letrec E1;EE^A[X,casebool (letrec E in R) S1 S2] in A1[var X] 
                        ==> letrec E1;EE^A[X,letrec E in casebool R S1 S2] in A1[var X] 
    -- constraints:
    where E/={}
        ,(S1,letrec E in HOLE)
        ,(S2,letrec E in HOLE)

{SR,lcasepair,1}        A[casepair (letrec E in R) X1.X2.S1] 
                        ==> A[letrec E in (casepair R X1.X2.S1)] 
    -- constraints:
    where  E /={}
         ,(dummypair[] X1.X2.S1,letrec E in HOLE)
         ,(var X1,dummylist3[] X2.HOLE)
         ,(var X2,dummylist3[] X1.HOLE)
                    
{SR,lcasepair,2}        letrec E1 in A[casepair (letrec E in R) X1.X2.S1] 
                        ==> letrec E1 in A[letrec E in (casepair R X1.X2.S1)]
    -- constraints:
    where E1 /= {}
        , E /={} 
        ,(dummypair[] X1.X2.S1,letrec E in HOLE)
         ,(var X1,dummylist3[] X2.HOLE)
         ,(var X2,dummylist3[] X1.HOLE)

{SR,lcasepair,3}        letrec E1;EE^A[X,casepair (letrec E in R) X1.X2.S1] in A1[var X] 
                        ==> letrec E1;EE^A[X,letrec E in casepair R X1.X2.S1] in A1[var X] 
    -- constraints:
    where E/={}
        ,(dummypair[] X1.X2.S1,letrec E in HOLE)
         ,(var X1,dummylist3[] X2.HOLE)
         ,(var X2,dummylist3[] X1.HOLE)

-- **
-- ***********************                    


-- ***********************     
-- **                    
-- three cases for (no,lseq) corresponding to reduction contexts,

{SR,lseq,1}         A[seq (letrec E in R) S] 
                    ==> A[letrec E in (seq R S)] 
    -- constraints:
    where  E /={}
          ,(S,letrec E in HOLE)
                    
{SR,lseq,2}         letrec E1 in A[seq (letrec E in R) S] 
                    ==> letrec E1 in A[letrec E in (seq R S)]
    -- constraints:                    
    where E1 /= {}
         ,E /={} 
         ,(S,letrec E in HOLE)

{SR,lseq,3}         letrec E1;EE^A[X,seq (letrec E in R) S] in A1[var X] 
                    ==> letrec E1;EE^A[X,letrec E in seq R S] in A1[var X] 
    -- constraints:
    where E/={}
         ,(S,letrec E in HOLE)

-- **
-- ***********************                    



-- ***********************     
-- **                    
-- (case-c)-reduction, three cases corresponding to reduction contexts,
-- for each alternative of a case and for each type of case
        
{SR,caselist-c,1}       A[caselist[1] (nil[]) SNIL X.XS.SCONS]                
                        ==> A[SNIL]
  where
          (var X,dummylist3[] XS.HOLE)
         ,(var XS,dummylist3[] X.HOLE)

                        
{SR,caselist-c,2}       A[caselist (cons[] R RS) SNIL X.XS.SCONS]
                        ==> A[letrec X=R; XS=RS in SCONS]
    -- constraints:
    where (R, (dummylist1[] X.XS.HOLE))
         ,(RS, (dummylist2[] X.XS.HOLE))
         ,(var X,dummylist3[] XS.HOLE)
         ,(var XS,dummylist3[] X.HOLE)
                             
{SR,caselist-c,3}       letrec E in A[caselist[1] (nil) SNIL X.XS.SCONS] 
                        ==> letrec E in A[SNIL]
    -- constraints:
    where  E /= {}
         ,(var X,dummylist3[] XS.HOLE)
         ,(var XS,dummylist3[] X.HOLE)
              
{SR,caselist-c,4}       letrec E in A[caselist (cons[] R RS) SNIL X.XS.SCONS]  
                        ==> letrec E in A[letrec X=R; XS=RS in SCONS]
    -- constraints:
    where E /= {}
        ,(R, (dummylist1[] X.XS.HOLE))
        ,(RS, (dummylist2[] X.XS.HOLE))
        ,(var X,dummylist3[] XS.HOLE)
        ,(var XS,dummylist3[] X.HOLE)

{SR,caselist-c,5}       letrec E;EE^A[X1,caselist (nil) SNIL X.XS.SCONS] in A1[var X1]     
                        ==> letrec E;EE^A[X1,SNIL] in A1[var X1]
 where
          (var X,dummylist3[] XS.HOLE)
         ,(var XS,dummylist3[] X.HOLE)
                        
{SR,caselist-c,6}       letrec E;EE^A[X1,caselist (cons[] R RS) SNIL X.XS.SCONS] in A1[var X1] 
                        ==> letrec E; EE^A[X1,letrec X=R;XS=RS in SCONS] in A1[var X1]
    -- constraints:
    where (R, (dummylist1[] X.XS.HOLE))
         ,(RS, (dummylist2[] X.XS.HOLE))
         ,(var X,dummylist3[] XS.HOLE)
         ,(var XS,dummylist3[] X.HOLE)

{SR,casebool-c,1}       A[casebool[1] (false[]) SFALSE STRUE]
                        ==> A[SFALSE]
                        
{SR,casebool-c,2}       A[casebool[1] (true[]) SFALSE STRUE]
                        ==> A[STRUE]
                        
{SR,casebool-c,3}       letrec E in A[casebool[1] (false[]) SFALSE STRUE]
                        ==> letrec E in A[SFALSE]
    -- constraints:
    where  E /= {}
                        
{SR,casebool-c,4}       letrec E in A[casebool[1] (true[]) SFALSE STRUE]
                        ==> letrec E in A[STRUE]
    -- constraints:
    where  E /= {}
                    
{SR,casebool-c,5}       letrec E;EE^A[X1,casebool[1] (false[]) SFALSE STRUE] in A1[var X1]
                        ==> letrec E;EE^A[X1,SFALSE] in A1[var X1]
                        
{SR,casebool-c,6}       letrec E;EE^A[X1,casebool[1] (true[]) SFALSE STRUE] in A1[var X1]
                        ==> letrec E;EE^A[X1,STRUE] in A1[var X1]

{SR,casepair-c,1}       A[casepair[1] (pair[] S1 S2) X1.X2.SPAIR]
                        ==> A[letrec X1=S1; X2=S2 in SPAIR]
    -- constraints:
    where (S1, (dummypair1[] X1.X2.HOLE))
         ,(S2, (dummypair1[] X1.X2.HOLE))
         ,(var X1,dummylist3[] X2.HOLE)
         ,(var X2,dummylist3[] X1.HOLE)
                  
{SR,casepair-c,2}       letrec E in A[casepair[1] (pair[] S1 S2) X1.X2.SPAIR]                
                        ==> letrec E in A[letrec X1=S1; X2=S2 in SPAIR]
    -- constraints:
    where E /= {}
         ,(S1, (dummypair1[] X1.X2.HOLE))
         ,(S2, (dummypair1[] X1.X2.HOLE))
         ,(var X1,dummylist3[] X2.HOLE)
         ,(var X2,dummylist3[] X1.HOLE)
                 
{SR,casepair-c,3}       letrec E;EE^A[X1,casepair[1] (pair[] S1 S2) Y1.Y2.SPAIR] in A1[var X1]                
                        ==> letrec E;EE^A[X1,letrec Y1=S1; Y2=S2 in SPAIR] in A1[var X1]
    -- constraints:
      where
          (S1, (dummypair1[] Y1.Y2.HOLE))
         ,(S2, (dummypair1[] Y1.Y2.HOLE))
         ,(var Y1,dummylist3[] Y2.HOLE)
         ,(var Y2,dummylist3[] Y1.HOLE)

-- **                    
-- ***********************     


-- ***********************     
-- **                    
-- (case-in)-reduction
-- for each alternative of a case and for each type of case
         
                        
{SR,caselist-in,1}      letrec VV|Xn,nil|; E in A[caselist (var Xn) SNIL X.XS.SCONS]
                         ==> letrec VV|Xn,nil|; E in A[SNIL]
                        
         where 
          (var X,dummylist3[] XS.HOLE)
         ,(var XS,dummylist3[] X.HOLE)

{SR,caselist-in,2}      letrec  VV|Xn,(cons[] R RS)|; E in A[caselist (var Xn) SNIL X.XS.SCONS]
                        ==> letrec  Z = R; ZS = RS; VV|Xn,(cons (var Z) (var ZS))|; E in A[letrec X=var Z;XS=var ZS in SCONS]
    -- constraints
    where (var ZS,(letrec X=dummy0[];XS=dummy3; VV|Xn,dummy0[]|; E;  Z = dummy3 in A[HOLE]))
         ,(var Z,letrec X=dummy0[];XS=dummy3; VV|Xn,dummy0[]|; E;  ZS = dummy3 in A[HOLE])
         ,(letrec  VV|Xn,(cons R RS)|; E in A[caselist (var Xn) SNIL X.XS.SCONS], letrec Z=dummy0[];ZS=dummy0[] in HOLE)
         ,(cons R RS, letrec Z=dummy0[];ZS=dummy0[] in HOLE)
         ,(R, (dummylist1[] X.XS.HOLE))
         ,(RS, (dummylist2[] X.XS.HOLE))
         ,(var X,dummylist3[] XS.HOLE)
         ,(var XS,dummylist3[] X.HOLE)
               

                        
                        
{SR,casebool-in,1}      letrec VV|Xn,false|; E in A[casebool (var Xn) SFALSE STRUE]
                        ==> letrec VV|Xn,false|; E in A[SFALSE]
                        
                        
{SR,casebool-in,2}      letrec VV|Xn,true|; E in A[casebool (var Xn) SFALSE STRUE]
                        ==> letrec VV|Xn,true|; E in A[STRUE]

         
{SR,casepair-in,1}      letrec  VV|Xn,(pair[] S1 S2)|;E in A[casepair (var Xn) Y1.Y2.SPAIR]
                        ==> letrec  Z1 = S1; Z2 = S2;  VV|Xn,(pair[] (var Z1) (var Z2))|;E in A[letrec Y1=var Z1;Y2=var Z2 in SPAIR]
    -- constraints
    where (var Z1,(letrec Y1=dummy0[];Y2=dummy0; VV|Xn,dummy0[]|; E;  Z2 = dummy0 in A[HOLE]))
         ,(var Z2,letrec Y1=dummy0[];Y2=dummy0; VV|Xn,dummy0[]|; E;  Z1 = dummy0 in A[HOLE])
         ,(letrec VV|Xn,(pair[] S1 S2)|;E in A[casepair (var Xn) Y1.Y2.SPAIR], letrec Z1=dummy0[];Z2=dummy0[] in HOLE)
         ,(S1, (dummypair[] Y1.Y2.HOLE))
         ,(S2, (dummypair[] Y1.Y2.HOLE))
         ,(pair[] S1 S2, letrec Z1=dummy0[];Z2=dummy0[] in HOLE)
         ,(var Y1,dummylist[] Y2.HOLE)
         ,(var Y2,dummylist[] Y1.HOLE)



-- **                    
-- ***********************     


-- ***********************     
-- **                    
-- (case-e)-reduction, two cases (without/with VV-Chain)
-- for each alternative of a case and for each type of case
         
{SR,caselist-e,1}       letrec VV|Xn,nil|; E; EE^A[Ym,caselist (var Xn) SNIL X.XS.SCONS] in A[var Ym]
                        ==> letrec VV|Xn,nil|; E; EE^A[Ym,SNIL] in A[var Ym]
                    
  where
         (var X,dummylist[] XS.HOLE)
         ,(var XS,dummylist[] X.HOLE)
                        
{SR,caselist-e,2}       letrec VV|Xn,(cons R RS)|; E; EE^A[Ym,caselist (var Xn) SNIL X.XS.SCONS] in A[var Ym]
                        ==> letrec Z = R; ZS = RS; VV|Xn,(cons (var Z) (var ZS))|; E; EE^A[Ym,letrec X=var Z;XS=var ZS in SCONS] in A[var Ym]
    where
      (var ZS,letrec X=dummy0[];XS=dummy3; VV|Xn,dummy0[]|; E; EE^A[Ym,caselist (var Xn) SNIL X.XS.SCONS]; Z = dummy0[] in A[HOLE])
     ,(var Z,letrec X=dummy0[];XS=dummy3; VV|Xn,dummy0[]|; E; EE^A[Ym,caselist (var Xn) SNIL X.XS.SCONS]; ZS = dummy0[] in A[HOLE])
     ,(letrec  VV|Xn,(cons R RS)|; E; EE^A[Ym,caselist (var Xn) SNIL X.XS.SCONS] in A[var Ym],letrec Z=dummy0[];ZS=dummy0[] in HOLE)
     ,(R, (dummylist1[] X.XS.HOLE))
     ,(RS, (dummylist2[] X.XS.HOLE))
     ,(cons R RS, letrec Z=dummy0[];ZS=dummy0[] in HOLE)
     ,(var X,dummylist3[] XS.HOLE)
     ,(var XS,dummylist3[] X.HOLE)

     
{SR,casebool-e,1}       letrec VV|Xn,false|; E; EE^A[Ym,casebool (var Xn) SFALSE STRUE] in A[var Ym]
                        ==> letrec VV|Xn,false|; E; EE^A[Ym,SFALSE] in A[var Ym]

                        

{SR,casebool-e,2}       letrec VV|Xn,true|; E; EE^A[Ym,casebool (var Xn) SFALSE STRUE] in A[var Ym]
                        ==> letrec VV|Xn,true|; E; EE^A[Ym,STRUE] in A[var Ym]
                    
                        
{SR,casepair-e,1}       letrec  VV|Xn,(pair[] R1 R2)|; E; EE^A[Ym,casepair (var Xn) Y1.Y2.SPAIR] in A[var Ym]
                        ==> letrec Z1 = R1; Z2 = R2; VV|Xn,(pair[] (var Z1) (var Z2))|; E; EE^A[Ym,letrec Y1 =var Z1;Y2=var Z2 in SPAIR] in A[var Ym]
    where
      (var Z1,letrec X=dummy0[];XS=dummy3; VV|Xn,dummy0[]|; E; EE^A[Ym,casepair (var Xn) Y1.Y2.SPAIR]; Z2 = dummy0[] in A[HOLE])
     ,(var Z2,letrec X=dummy0[];XS=dummy3; VV|Xn,dummy0[]|; E; EE^A[Ym,casepair (var Xn) Y1.Y2.SPAIR]; Z1 = dummy0[] in A[HOLE])
     ,(letrec VV|Xn,(pair[] R1 R2)|; E; EE^A[Ym,casepair (var Xn) Y1.Y2.SPAIR] in A[var Ym],letrec Z1=dummy0[];Z2=dummy0[] in HOLE)
     ,(R1, (dummypair1[] Y1.Y2.HOLE))
     ,(R2, (dummypair2[] Y1.Y2.HOLE))
     ,(var Y1,dummylist3[] Y2.HOLE)
     ,(var Y2,dummylist3[] Y1.HOLE)
     
-- **                    
-- ***********************     


-- ***********************     
-- **                    
-- (seq-c)-reduction, three cases corresponding to reduction contexts,
-- for abstractions, and each data constructor
        
{SR,seq-c,1}            A[seq (nil[]) S]                
                        ==> A[S]

{SR,seq-c,2}            A[seq (cons R1 R2) S]                
                        ==> A[S]
                        
{SR,seq-c,3}            A[seq (pair[] R1 R2) S]                
                        ==> A[S]
                        
{SR,seq-c,4}            A[seq (true) S]                
                        ==> A[S]
                        
{SR,seq-c,5}            A[seq (false) S]                
                        ==> A[S]
                        
{SR,seq-c,6}            A[seq (\X.R) S]                
                        ==> A[S]
                        
{SR,seq-c,7}            letrec E in A[seq (nil[]) S]                
                        ==> letrec E in A[S]
    -- constraints:
    where E /= {}

{SR,seq-c,8}            letrec E in A[seq (cons R1 R2) S]                
                        ==> letrec E in A[S]
    -- constraints:
    where E /= {}
                        
{SR,seq-c,9}            letrec E in A[seq (pair[] R1 R2) S]                
                        ==> letrec E in A[S]
    -- constraints:
    where E /= {}
                        
{SR,seq-c,10}            letrec E in A[seq (true) S]                
                        ==> letrec E in A[S]
    -- constraints:
    where E /= {}
                                                
{SR,seq-c,11}            letrec E in A[seq (false) S]                
                        ==> letrec E in A[S]
    -- constraints:
    where E /= {}

{SR,seq-c,12}           letrec E in A[seq (\X.R) S]                
                        ==> letrec E in A[S]
    -- constraints:
    where E /= {}
                
{SR,seq-c,13}            letrec E;EE^A[X1,seq (nil[]) S] in A1[var X1]
                        ==> letrec E;EE^A[X1,S] in A1[var X1]

{SR,seq-c,14}            letrec E;EE^A[X1,seq (cons R1 R2) S] in A1[var X1]                
                        ==> letrec E;EE^A[X1,S] in A1[var X1]
                        
{SR,seq-c,15}            letrec E;EE^A[X1,seq (pair[] R1 R2) S] in A1[var X1]                
                        ==> letrec E;EE^A[X1,S] in A1[var X1]
                        
{SR,seq-c,16}            letrec E;EE^A[X1,seq (true) S] in A1[var X1]              
                        ==> letrec E;EE^A[X1,S] in A1[var X1]
                                                
{SR,seq-c,17}            letrec E;EE^A[X1,seq (false) S] in A1[var X1]               
                        ==> letrec E;EE^A[X1,S] in A1[var X1]

{SR,seq-c,18}            letrec E;EE^A[X1,seq (\X.R) S] in A1[var X1]                
                        ==> letrec E;EE^A[X1,S] in A1[var X1]
                             
-- **                    
-- ***********************     


-- ***********************     
-- **                    
-- (seq-in)-reduction, two cases (with/without VV-Chain)
-- for each data constructor
     
                       
{SR,seq-in,1}           letrec VV|Xn,false|; E in A[seq (var Xn) S]
                        ==> letrec VV|Xn,false|; E in A[S]
                        
{SR,seq-in,2}           letrec VV|Xn,true|; E in A[seq (var Xn) S]
                        ==> letrec  VV|Xn,true|; E in A[S]
                        
{SR,seq-in,3}           letrec VV|Xn,nil|; E in A[seq (var Xn) S]
                        ==> letrec VV|Xn,nil|; E in A[S]

                        
{SR,seq-in,4}           letrec VV|Xn,(cons R1 R2)|; E in A[seq (var Xn) S]
                        ==> letrec VV|Xn,(cons R1 R2)|; E in A[S]
                        
                        
{SR,seq-in,5}          letrec VV|Xn,(pair[] R1 R2)|; E in A[seq (var Xn) S]
                        ==> letrec  VV|Xn,(pair[] R1 R2)|; E in A[S]
     
-- **                    
-- ***********************     


-- ***********************     
-- **                    
-- (seq-e)-reduction, two cases (with/without VV-Chain)
-- for each data constructor
     
     
{SR,seq-e,1}            letrec VV|Xn,false|; E; EE^A[Ym,seq (var Xn) S] in A[var Ym]
                        ==> letrec VV|Xn,false|; E; EE^A[Ym,S] in A[var Ym]

{SR,seq-e,2}            letrec VV|Xn,true|; E; EE^A[Ym,seq (var Xn) S] in A[var Ym]
                        ==> letrec VV|Xn,true|; E; EE^A[Ym,S] in A[var Ym]
                        
{SR,seq-e,3}            letrec VV|Xn,nil|; E; EE^A[Ym,seq (var Xn) S] in A[var Ym]
                        ==> letrec VV|Xn,nil|; E; EE^A[Ym,S] in A[var Ym]
                        
{SR,seq-e,4}            letrec VV|Xn,(cons R1 R2)|; E; EE^A[Ym,seq (var Xn) S] in A[var Ym]
                        ==> letrec VV|Xn,(cons R1 R2)|; E; EE^A[Ym,S] in A[var Ym]

{SR,seq-e,5}            letrec VV|Xn,(pair[] R1 R2)|; E; EE^A[Ym,seq (var Xn) S] in A[var Ym]
                        ==> letrec VV|Xn,(pair[] R1 R2)|; E; EE^A[Ym,S] in A[var Ym]
-- **                    
-- ***********************     


--
-- transitive closure rules of let shifting

{SR,lll,+,1}         A[letrec E in R]
                    ==> letrec E in A[R]
    -- constraints:
    where  A/=[], E /={}
          ,(A[dummy0[]],letrec E in HOLE)

          
          
{SR,lll,+,2}    letrec E1 in A[letrec E in R]
                    ==> letrec E1;E in A[R]
    -- constraints:
    where E1 /= {}
         ,E /={}
         ,A/= []
         ,(A[dummy0[]],letrec E in HOLE)
         ,[E1,letrec E in HOLE]

{SR,lll,+,3}    letrec E1;EE^A[X,A[letrec E in R]] in A1[var X]
                    ==> letrec E1;E;EE^A[X,A[R]] in A1[var X]
    -- constraints:
    where E/={}, A/=[]
         ,(A[dummy0[]],letrec E in HOLE)
         ,[E1,letrec E in HOLE]
         ,(var X,letrec E in HOLE)