*** 1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        activate(X) -> X
        and(tt(),X) -> activate(X)
        plus(N,0()) -> N
        plus(N,s(M)) -> s(plus(N,M))
        x(N,0()) -> 0()
        x(N,s(M)) -> plus(x(N,M),N)
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {activate/1,and/2,plus/2,x/2} / {0/0,s/1,tt/0}
      Obligation:
        Full
        basic terms: {activate,and,plus,x}/{0,s,tt}
    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) = [3]                  
          p(activate) = [2] x1 + [4]         
               p(and) = [7] x1 + [4] x2 + [0]
              p(plus) = [1] x1 + [1]         
                 p(s) = [1] x1 + [7]         
                p(tt) = [1]                  
                 p(x) = [1] x1 + [3] x2 + [0]
        
        Following rules are strictly oriented:
        activate(X) = [2] X + [4]         
                    > [1] X + [0]         
                    = X                   
        
        and(tt(),X) = [4] X + [7]         
                    > [2] X + [4]         
                    = activate(X)         
        
        plus(N,0()) = [1] N + [1]         
                    > [1] N + [0]         
                    = N                   
        
           x(N,0()) = [1] N + [9]         
                    > [3]                 
                    = 0()                 
        
          x(N,s(M)) = [3] M + [1] N + [21]
                    > [3] M + [1] N + [1] 
                    = plus(x(N,M),N)      
        
        
        Following rules are (at-least) weakly oriented:
        plus(N,s(M)) =  [1] N + [1] 
                     >= [1] N + [8] 
                     =  s(plus(N,M))
        
      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:
        plus(N,s(M)) -> s(plus(N,M))
      Weak DP Rules:
        
      Weak TRS Rules:
        activate(X) -> X
        and(tt(),X) -> activate(X)
        plus(N,0()) -> N
        x(N,0()) -> 0()
        x(N,s(M)) -> plus(x(N,M),N)
      Signature:
        {activate/1,and/2,plus/2,x/2} / {0/0,s/1,tt/0}
      Obligation:
        Full
        basic terms: {activate,and,plus,x}/{0,s,tt}
    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:
        {}
      TcT has computed the following interpretation:
               p(0) = 0                               
        p(activate) = 4*x1                            
             p(and) = 1 + 4*x1*x2 + x1^2 + 5*x2 + x2^2
            p(plus) = x1 + 2*x2                       
               p(s) = 1 + x1                          
              p(tt) = 1                               
               p(x) = 2*x1 + 2*x1*x2                  
      
      Following rules are strictly oriented:
      plus(N,s(M)) = 2 + 2*M + N 
                   > 1 + 2*M + N 
                   = s(plus(N,M))
      
      
      Following rules are (at-least) weakly oriented:
      activate(X) =  4*X           
                  >= X             
                  =  X             
      
      and(tt(),X) =  2 + 9*X + X^2 
                  >= 4*X           
                  =  activate(X)   
      
      plus(N,0()) =  N             
                  >= N             
                  =  N             
      
         x(N,0()) =  2*N           
                  >= 0             
                  =  0()           
      
        x(N,s(M)) =  2*M*N + 4*N   
                  >= 2*M*N + 4*N   
                  =  plus(x(N,M),N)
      
*** 1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        activate(X) -> X
        and(tt(),X) -> activate(X)
        plus(N,0()) -> N
        plus(N,s(M)) -> s(plus(N,M))
        x(N,0()) -> 0()
        x(N,s(M)) -> plus(x(N,M),N)
      Signature:
        {activate/1,and/2,plus/2,x/2} / {0/0,s/1,tt/0}
      Obligation:
        Full
        basic terms: {activate,and,plus,x}/{0,s,tt}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).