*** 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:
        Full
        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:
        Full
        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:
        {}
      TcT has computed the following interpretation:
         p(plus) = [0 2] x1 + [1 0] x2 + [0]
                   [0 1]      [0 1]      [2]
            p(s) = [1 2] x1 + [0]           
                   [0 0]      [6]           
        p(times) = [4 2] x1 + [4 0] x2 + [0]
                   [4 5]      [4 1]      [2]
      
      Following rules are strictly oriented:
      plus(plus(X,Y),Z) = [0 2] X + [0 2] Y + [1
                          0] Z + [4]            
                          [0 1]     [0 1]     [0
                          1]     [4]            
                        > [0 2] X + [0 2] Y + [1
                          0] Z + [0]            
                          [0 1]     [0 1]     [0
                          1]     [4]            
                        = plus(X,plus(Y,Z))     
      
      
      Following rules are (at-least) weakly oriented:
      times(X,s(Y)) =  [4 2] X + [4 8] Y + [0]
                       [4 5]     [4 8]     [8]
                    >= [4 2] X + [4 2] Y + [0]
                       [4 2]     [4 5]     [4]
                    =  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:
        Full
        basic terms: {plus,times}/{s}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).