*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
        times(X,s(Y)) -> plus(X,times(Y,X))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {plus/2,times/2} / {s/1}
      Obligation:
        Innermost
        basic terms: {plus,times}/{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) = {2}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
           p(plus) = [1] x2 + [0]         
              p(s) = [1] x1 + [1]         
          p(times) = [1] x1 + [1] x2 + [8]
        
        Following rules are strictly oriented:
        times(X,s(Y)) = [1] X + [1] Y + [9]
                      > [1] X + [1] Y + [8]
                      = plus(X,times(Y,X)) 
        
        
        Following rules are (at-least) weakly oriented:
        plus(plus(X,Y),Z) =  [1] Z + [0]      
                          >= [1] Z + [0]      
                          =  plus(X,plus(Y,Z))
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
      Weak DP Rules:
        
      Weak TRS Rules:
        times(X,s(Y)) -> plus(X,times(Y,X))
      Signature:
        {plus/2,times/2} / {s/1}
      Obligation:
        Innermost
        basic terms: {plus,times}/{s}
    Applied Processor:
      NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 1 non-zero interpretation-entries in the diagonal of the component-wise maxima):
      The following argument positions are considered usable:
        uargs(plus) = {2}
      
      Following symbols are considered usable:
        {plus,times}
      TcT has computed the following interpretation:
         p(plus) = [0 4] x1 + [1 0] x2 + [1]
                   [0 1]      [0 1]      [2]
            p(s) = [1 7] x1 + [4]           
                   [0 0]      [0]           
        p(times) = [1 4] x1 + [1 0] x2 + [4]
                   [2 4]      [2 2]      [6]
      
      Following rules are strictly oriented:
      plus(plus(X,Y),Z) = [0 4] X + [0 4] Y + [1
                          0] Z + [9]            
                          [0 1]     [0 1]     [0
                          1]     [4]            
                        > [0 4] X + [0 4] Y + [1
                          0] Z + [2]            
                          [0 1]     [0 1]     [0
                          1]     [4]            
                        = plus(X,plus(Y,Z))     
      
      
      Following rules are (at-least) weakly oriented:
      times(X,s(Y)) =  [1 4] X + [1  7] Y + [8] 
                       [2 4]     [2 14]     [14]
                    >= [1 4] X + [1 4] Y + [5]  
                       [2 3]     [2 4]     [8]  
                    =  plus(X,times(Y,X))       
      
*** 1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
        times(X,s(Y)) -> plus(X,times(Y,X))
      Signature:
        {plus/2,times/2} / {s/1}
      Obligation:
        Innermost
        basic terms: {plus,times}/{s}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).