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 + [0]          
              p(+) = [1] x2 + [12]         
              p(-) = [4] x1 + [1] x2 + [13]
              p(0) = [2]                   
            p(exp) = [5] x2 + [0]          
              p(s) = [1] x1 + [2]          
          
          Following rules are strictly oriented:
              -(x,0()) = [4] x + [15]        
                       > [1] x + [0]         
                       = x                   
          
              -(0(),y) = [1] y + [21]        
                       > [2]                 
                       = 0()                 
          
          -(s(x),s(y)) = [4] x + [1] y + [23]
                       > [4] x + [1] y + [13]
                       = -(x,y)              
          
            exp(x,0()) = [10]                
                       > [4]                 
                       = s(0())              
          
           exp(x,s(y)) = [5] y + [10]        
                       > [5] y + [0]         
                       = *(x,exp(x,y))       
          
          
          Following rules are (at-least) weakly oriented:
           *(0(),y) =  [1] y + [0] 
                    >= [2]         
                    =  0()         
          
          *(s(x),y) =  [1] y + [0] 
                    >= [1] y + [12]
                    =  +(y,*(x,y)) 
          
        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:
            *(0(),y) -> 0()
            *(s(x),y) -> +(y,*(x,y))
        - Weak TRS:
            -(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 + [10]        
              p(+) = [1] x2 + [0]         
              p(-) = [2] x1 + [2] x2 + [6]
              p(0) = [0]                  
            p(exp) = [8] x2 + [14]        
              p(s) = [1] x1 + [2]         
          
          Following rules are strictly oriented:
          *(0(),y) = [1] y + [10]
                   > [0]         
                   = 0()         
          
          
          Following rules are (at-least) weakly oriented:
             *(s(x),y) =  [1] y + [10]        
                       >= [1] y + [10]        
                       =  +(y,*(x,y))         
          
              -(x,0()) =  [2] x + [6]         
                       >= [1] x + [0]         
                       =  x                   
          
              -(0(),y) =  [2] y + [6]         
                       >= [0]                 
                       =  0()                 
          
          -(s(x),s(y)) =  [2] x + [2] y + [14]
                       >= [2] x + [2] y + [6] 
                       =  -(x,y)              
          
            exp(x,0()) =  [14]                
                       >= [2]                 
                       =  s(0())              
          
           exp(x,s(y)) =  [8] y + [30]        
                       >= [8] y + [24]        
                       =  *(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(*) = 2 + x1 + x2        
            p(+) = x2                 
            p(-) = x1*x2 + 2*x1^2 + x2
            p(0) = 2                  
          p(exp) = x1*x2 + 2*x2       
            p(s) = 1 + x1             
        
        Following rules are strictly oriented:
        *(s(x),y) = 3 + x + y  
                  > 2 + x + y  
                  = +(y,*(x,y))
        
        
        Following rules are (at-least) weakly oriented:
            *(0(),y) =  4 + y                      
                     >= 2                          
                     =  0()                        
        
            -(x,0()) =  2 + 2*x + 2*x^2            
                     >= x                          
                     =  x                          
        
            -(0(),y) =  8 + 3*y                    
                     >= 2                          
                     =  0()                        
        
        -(s(x),s(y)) =  4 + 5*x + x*y + 2*x^2 + 2*y
                     >= x*y + 2*x^2 + y            
                     =  -(x,y)                     
        
          exp(x,0()) =  4 + 2*x                    
                     >= 3                          
                     =  s(0())                     
        
         exp(x,s(y)) =  2 + x + x*y + 2*y          
                     >= 2 + x + x*y + 2*y          
                     =  *(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))