-- import the calculus rules and transformations
-- import LR-StandardReductions.inp
-- import LR-Answers.inp
-- import LR-Transformations.inp
-- import LR-Unions.inp
-- overlap all left hand sides of each transformation with all left hand sides of each normal
-- order reduction
-- union (abscpcx,0) = {(abs,0),(cpcx,0)}


        
overlap (gc,1).r    
    all 
        except {(SR,lll,+,1),(SR,lll,+,2),(SR,lll,+,3)}
        ignore {(SR,lll,+,1),(SR,lll,+,2),(SR,lll,+,3),
                (casebool-c,0)
               ,(cpT,0),(cpd,0),(ucp,0)
               ,(casepair-c,1)
               ,(caselist-c,0)
               ,(lbeta,1)
               ,(seq-c,0)
               ,(lll,0)               
               ,(ucp,0)
               ,(cpcx,0)
               ,(cpx,0)
               ,(xch,1)
               ,(abs,0)
               }
overlap (gc,2).r      
    all 
        except {(SR,lll,+,1),(SR,lll,+,2),(SR,lll,+,3)}
        ignore {
                (casebool-c,0)
               ,(casepair-c,1)
               ,(caselist-c,0)
               ,(cpT,0),(cpd,0),(ucp,0)
               ,(lbeta,1)
               ,(lll,0)               
               ,(seq-c,0)
               ,(cpcx,0)
               ,(cpx,0)
               ,(xch,1)
               ,(abs,0)
               }
        
-- add an option to allow not too much abs-steps for closing, e.g. 1, since
-- the transformation is non-terminating and blows up the expressions

overlap (abs,1).r  
    all 
        except {(SR,lll,+,1),(SR,lll,+,2),(SR,lll,+,3)}
        ignore {(SR,lll,+,0),(cpcx,0),(lbeta,1)
               ,(cpT,0),(cpd,0),(ucp,0),(gc,2)
               ,(lll,0)
               ,(caselist-c,0)
               ,(casebool-c,0)
               ,(casepair-c,1)
               ,(seq-c,0)
               }
        restrict {(abs,1):1,(abs,2):1,(cpx-e,1):2,(cpx-e,2):2,(cpx-in,1):2}               


overlap (abs,2).r  
    all 
        except {(SR,lll,+,1),(SR,lll,+,2),(SR,lll,+,3)}
        ignore {(SR,lll,+,0),(cpcx,0),(lbeta,1)
               ,(cpT,0),(cpd,0),(ucp,0),(gc,2)
               ,(lll,0)
               ,(caselist-c,0)
               ,(casebool-c,0)
               ,(casepair-c,1)
               ,(seq-c,0)
               }
        restrict {(abs,1):1,(abs,2):1,(cpx-e,1):2,(cpx-e,2):2,(cpx-in,1):2}               


        


overlap (ucp,1).r
    all 
        except {(SR,lll,+,1),(SR,lll,+,2),(SR,lll,+,3)}
        ignore {(cpcx,0),(caselist-c,0),(casebool-c,0),(casepair-c,1),(cpx,0),(xch,1),(abs,0),(lbeta,1)
                ,(seq-c,0),(cpT,0), (cpd,0),(lll,0)
               }
overlap (ucp,2).r
    all 
        except {(SR,lll,+,1),(SR,lll,+,2),(SR,lll,+,3)}
        ignore {(cpcx,0),(caselist-c,0),(casebool-c,0),(casepair-c,1),(cpx,0),(xch,1),(abs,0),(lbeta,1)
                ,(seq-c,0),(cpT,0), (cpd,0),(lll,0)
               }
               
overlap (ucp,3).r
    all 
        except {(SR,lll,+,1),(SR,lll,+,2),(SR,lll,+,3)}
        ignore {(cpcx,0),(caselist-c,0),(casebool-c,0),(casepair-c,1),(cpx,0),(xch,1),(abs,0),(lbeta,1)
                ,(seq-c,0),(cpT,0), (cpd,0),(lll,0)
               }