WORST_CASE(?,O(n^2))
* Step 1: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            *(0(),y) -> 0()
            *(s(x),y) -> +(y,*(x,y))
            -(x,0()) -> x
            -(0(),y) -> 0()
            -(s(x),s(y)) -> -(x,y)
            exp(x,0()) -> s(0())
            exp(x,s(y)) -> *(x,exp(x,y))
        - Signature:
            {*/2,-/2,exp/2} / {+/2,0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*,-,exp} and constructors {+,0,s}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(*) = {2},
            uargs(+) = {2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
              p(*) = [1] x2 + [2]         
              p(+) = [1] x2 + [0]         
              p(-) = [4] x1 + [1] x2 + [6]
              p(0) = [0]                  
            p(exp) = [10] x2 + [1]        
              p(s) = [1] x1 + [1]         
          
          Following rules are strictly oriented:
              *(0(),y) = [1] y + [2]         
                       > [0]                 
                       = 0()                 
          
              -(x,0()) = [4] x + [6]         
                       > [1] x + [0]         
                       = x                   
          
              -(0(),y) = [1] y + [6]         
                       > [0]                 
                       = 0()                 
          
          -(s(x),s(y)) = [4] x + [1] y + [11]
                       > [4] x + [1] y + [6] 
                       = -(x,y)              
          
           exp(x,s(y)) = [10] y + [11]       
                       > [10] y + [3]        
                       = *(x,exp(x,y))       
          
          
          Following rules are (at-least) weakly oriented:
           *(s(x),y) =  [1] y + [2]
                     >= [1] y + [2]
                     =  +(y,*(x,y))
          
          exp(x,0()) =  [1]        
                     >= [1]        
                     =  s(0())     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            *(s(x),y) -> +(y,*(x,y))
            exp(x,0()) -> s(0())
        - Weak TRS:
            *(0(),y) -> 0()
            -(x,0()) -> x
            -(0(),y) -> 0()
            -(s(x),s(y)) -> -(x,y)
            exp(x,s(y)) -> *(x,exp(x,y))
        - Signature:
            {*/2,-/2,exp/2} / {+/2,0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*,-,exp} and constructors {+,0,s}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(*) = {2},
            uargs(+) = {2}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
              p(*) = [1] x2 + [0]
              p(+) = [1] x2 + [0]
              p(-) = [2] x1 + [0]
              p(0) = [0]         
            p(exp) = [7]         
              p(s) = [1] x1 + [0]
          
          Following rules are strictly oriented:
          exp(x,0()) = [7]   
                     > [0]   
                     = s(0())
          
          
          Following rules are (at-least) weakly oriented:
              *(0(),y) =  [1] y + [0]  
                       >= [0]          
                       =  0()          
          
             *(s(x),y) =  [1] y + [0]  
                       >= [1] y + [0]  
                       =  +(y,*(x,y))  
          
              -(x,0()) =  [2] x + [0]  
                       >= [1] x + [0]  
                       =  x            
          
              -(0(),y) =  [0]          
                       >= [0]          
                       =  0()          
          
          -(s(x),s(y)) =  [2] x + [0]  
                       >= [2] x + [0]  
                       =  -(x,y)       
          
           exp(x,s(y)) =  [7]          
                       >= [7]          
                       =  *(x,exp(x,y))
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: NaturalPI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            *(s(x),y) -> +(y,*(x,y))
        - Weak TRS:
            *(0(),y) -> 0()
            -(x,0()) -> x
            -(0(),y) -> 0()
            -(s(x),s(y)) -> -(x,y)
            exp(x,0()) -> s(0())
            exp(x,s(y)) -> *(x,exp(x,y))
        - Signature:
            {*/2,-/2,exp/2} / {+/2,0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*,-,exp} and constructors {+,0,s}
    + Applied Processor:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(*) = {2},
          uargs(+) = {2}
        
        Following symbols are considered usable:
          {*,-,exp}
        TcT has computed the following interpretation:
            p(*) = 1 + 2*x1 + x2               
            p(+) = x2                          
            p(-) = 1 + 2*x1*x2 + x1^2          
            p(0) = 2                           
          p(exp) = 2*x1 + 2*x1*x2 + x1^2 + x2^2
            p(s) = 1 + x1                      
        
        Following rules are strictly oriented:
        *(s(x),y) = 3 + 2*x + y
                  > 1 + 2*x + y
                  = +(y,*(x,y))
        
        
        Following rules are (at-least) weakly oriented:
            *(0(),y) =  5 + y                            
                     >= 2                                
                     =  0()                              
        
            -(x,0()) =  1 + 4*x + x^2                    
                     >= x                                
                     =  x                                
        
            -(0(),y) =  5 + 4*y                          
                     >= 2                                
                     =  0()                              
        
        -(s(x),s(y)) =  4 + 4*x + 2*x*y + x^2 + 2*y      
                     >= 1 + 2*x*y + x^2                  
                     =  -(x,y)                           
        
          exp(x,0()) =  4 + 6*x + x^2                    
                     >= 3                                
                     =  s(0())                           
        
         exp(x,s(y)) =  1 + 4*x + 2*x*y + x^2 + 2*y + y^2
                     >= 1 + 4*x + 2*x*y + x^2 + y^2      
                     =  *(x,exp(x,y))                    
        
* Step 4: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            *(0(),y) -> 0()
            *(s(x),y) -> +(y,*(x,y))
            -(x,0()) -> x
            -(0(),y) -> 0()
            -(s(x),s(y)) -> -(x,y)
            exp(x,0()) -> s(0())
            exp(x,s(y)) -> *(x,exp(x,y))
        - Signature:
            {*/2,-/2,exp/2} / {+/2,0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {*,-,exp} and constructors {+,0,s}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))