*** 1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        *(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))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {*/2,-/2,exp/2} / {+/2,0/0,s/1}
      Obligation:
        Innermost
        basic terms: {*,-,exp}/{+,0,s}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      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:
          {}
        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.
*** 1.1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        *(s(x),y) -> +(y,*(x,y))
        exp(x,0()) -> s(0())
      Weak DP Rules:
        
      Weak TRS Rules:
        *(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
        basic terms: {*,-,exp}/{+,0,s}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      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:
          {}
        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.
*** 1.1.1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        *(s(x),y) -> +(y,*(x,y))
      Weak DP Rules:
        
      Weak TRS Rules:
        *(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
        basic terms: {*,-,exp}/{+,0,s}
    Applied Processor:
      NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      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(*) = x1 + x2       
          p(+) = x2            
          p(-) = 4*x1 + 2*x1^2 
          p(0) = 1             
        p(exp) = 2*x1*x2 + 2*x2
          p(s) = 1 + x1        
      
      Following rules are strictly oriented:
      *(s(x),y) = 1 + x + y  
                > x + y      
                = +(y,*(x,y))
      
      
      Following rules are (at-least) weakly oriented:
          *(0(),y) =  1 + y                
                   >= 1                    
                   =  0()                  
      
          -(x,0()) =  4*x + 2*x^2          
                   >= x                    
                   =  x                    
      
          -(0(),y) =  6                    
                   >= 1                    
                   =  0()                  
      
      -(s(x),s(y)) =  6 + 8*x + 2*x^2      
                   >= 4*x + 2*x^2          
                   =  -(x,y)               
      
        exp(x,0()) =  2 + 2*x              
                   >= 2                    
                   =  s(0())               
      
       exp(x,s(y)) =  2 + 2*x + 2*x*y + 2*y
                   >= x + 2*x*y + 2*y      
                   =  *(x,exp(x,y))        
      
*** 1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        *(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
        basic terms: {*,-,exp}/{+,0,s}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).