*** 1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        plus(x,0()) -> x
        plus(x,s(y)) -> s(plus(x,y))
        times(x,0()) -> 0()
        times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z)))
        times(x,s(y)) -> plus(times(x,y),x)
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {plus/2,times/2} / {0/0,s/1}
      Obligation:
        Innermost
        basic terms: {plus,times}/{0,s}
    Applied Processor:
      InnermostRuleRemoval
    Proof:
      Arguments of following rules are not normal-forms.
        times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z)))
      All above mentioned rules can be savely removed.
*** 1.1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        plus(x,0()) -> x
        plus(x,s(y)) -> s(plus(x,y))
        times(x,0()) -> 0()
        times(x,s(y)) -> plus(times(x,y),x)
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {plus/2,times/2} / {0/0,s/1}
      Obligation:
        Innermost
        basic terms: {plus,times}/{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(plus) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
              p(0) = [0]                   
           p(plus) = [1] x1 + [0]          
              p(s) = [1] x1 + [1]          
          p(times) = [12] x1 + [8] x2 + [3]
        
        Following rules are strictly oriented:
         times(x,0()) = [12] x + [3]         
                      > [0]                  
                      = 0()                  
        
        times(x,s(y)) = [12] x + [8] y + [11]
                      > [12] x + [8] y + [3] 
                      = plus(times(x,y),x)   
        
        
        Following rules are (at-least) weakly oriented:
         plus(x,0()) =  [1] x + [0] 
                     >= [1] x + [0] 
                     =  x           
        
        plus(x,s(y)) =  [1] x + [0] 
                     >= [1] x + [1] 
                     =  s(plus(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:
        plus(x,0()) -> x
        plus(x,s(y)) -> s(plus(x,y))
      Weak DP Rules:
        
      Weak TRS Rules:
        times(x,0()) -> 0()
        times(x,s(y)) -> plus(times(x,y),x)
      Signature:
        {plus/2,times/2} / {0/0,s/1}
      Obligation:
        Innermost
        basic terms: {plus,times}/{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(plus) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
              p(0) = [2]                  
           p(plus) = [1] x1 + [2]         
              p(s) = [1] x1 + [1]         
          p(times) = [1] x1 + [4] x2 + [8]
        
        Following rules are strictly oriented:
        plus(x,0()) = [1] x + [2]
                    > [1] x + [0]
                    = x          
        
        
        Following rules are (at-least) weakly oriented:
         plus(x,s(y)) =  [1] x + [2]         
                      >= [1] x + [3]         
                      =  s(plus(x,y))        
        
         times(x,0()) =  [1] x + [16]        
                      >= [2]                 
                      =  0()                 
        
        times(x,s(y)) =  [1] x + [4] y + [12]
                      >= [1] x + [4] y + [10]
                      =  plus(times(x,y),x)  
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        plus(x,s(y)) -> s(plus(x,y))
      Weak DP Rules:
        
      Weak TRS Rules:
        plus(x,0()) -> x
        times(x,0()) -> 0()
        times(x,s(y)) -> plus(times(x,y),x)
      Signature:
        {plus/2,times/2} / {0/0,s/1}
      Obligation:
        Innermost
        basic terms: {plus,times}/{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(plus) = {1},
        uargs(s) = {1}
      
      Following symbols are considered usable:
        {plus,times}
      TcT has computed the following interpretation:
            p(0) = 0                    
         p(plus) = 3 + x1 + 2*x2        
            p(s) = 1 + x1               
        p(times) = 2*x1*x2 + x2 + 2*x2^2
      
      Following rules are strictly oriented:
      plus(x,s(y)) = 5 + x + 2*y 
                   > 4 + x + 2*y 
                   = s(plus(x,y))
      
      
      Following rules are (at-least) weakly oriented:
        plus(x,0()) =  3 + x                        
                    >= x                            
                    =  x                            
      
       times(x,0()) =  0                            
                    >= 0                            
                    =  0()                          
      
      times(x,s(y)) =  3 + 2*x + 2*x*y + 5*y + 2*y^2
                    >= 3 + 2*x + 2*x*y + y + 2*y^2  
                    =  plus(times(x,y),x)           
      
*** 1.1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        plus(x,0()) -> x
        plus(x,s(y)) -> s(plus(x,y))
        times(x,0()) -> 0()
        times(x,s(y)) -> plus(times(x,y),x)
      Signature:
        {plus/2,times/2} / {0/0,s/1}
      Obligation:
        Innermost
        basic terms: {plus,times}/{0,s}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).