YES(O(1),O(n^2))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { and(tt(), X) -> activate(X)
  , activate(X) -> 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) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^2))

The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(plus) = {1}, Uargs(s) = {1}

TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).

   [and](x1, x2) = [1] x1 + [1] x2 + [7]
                                        
            [tt] = [7]                  
                                        
  [activate](x1) = [1] x1 + [5]         
                                        
  [plus](x1, x2) = [1] x1 + [7]         
                                        
             [0] = [7]                  
                                        
         [s](x1) = [1] x1 + [7]         
                                        
     [x](x1, x2) = [1] x2 + [7]         

The following symbols are considered usable

  {and, activate, plus, x}

The order satisfies the following ordering constraints:

   [and(tt(), X)] =  [1] X + [14]      
                  >  [1] X + [5]       
                  =  [activate(X)]     
                                       
    [activate(X)] =  [1] X + [5]       
                  >  [1] X + [0]       
                  =  [X]               
                                       
   [plus(N, 0())] =  [1] N + [7]       
                  >  [1] N + [0]       
                  =  [N]               
                                       
  [plus(N, s(M))] =  [1] N + [7]       
                  ?  [1] N + [14]      
                  =  [s(plus(N, M))]   
                                       
      [x(N, 0())] =  [14]              
                  >  [7]               
                  =  [0()]             
                                       
     [x(N, s(M))] =  [1] M + [14]      
                  >= [1] M + [14]      
                  =  [plus(x(N, M), N)]
                                       

Further, it can be verified that all rules not oriented are covered by the weightgap condition.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs:
  { plus(N, s(M)) -> s(plus(N, M))
  , x(N, s(M)) -> plus(x(N, M), N) }
Weak Trs:
  { and(tt(), X) -> activate(X)
  , activate(X) -> X
  , plus(N, 0()) -> N
  , x(N, 0()) -> 0() }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^2))

The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(plus) = {1}, Uargs(s) = {1}

TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).

   [and](x1, x2) = [1] x1 + [1] x2 + [7]
                                        
            [tt] = [7]                  
                                        
  [activate](x1) = [1] x1 + [5]         
                                        
  [plus](x1, x2) = [1] x1 + [0]         
                                        
             [0] = [7]                  
                                        
         [s](x1) = [1] x1 + [4]         
                                        
     [x](x1, x2) = [1] x1 + [1] x2 + [4]

The following symbols are considered usable

  {and, activate, plus, x}

The order satisfies the following ordering constraints:

   [and(tt(), X)] =  [1] X + [14]       
                  >  [1] X + [5]        
                  =  [activate(X)]      
                                        
    [activate(X)] =  [1] X + [5]        
                  >  [1] X + [0]        
                  =  [X]                
                                        
   [plus(N, 0())] =  [1] N + [0]        
                  >= [1] N + [0]        
                  =  [N]                
                                        
  [plus(N, s(M))] =  [1] N + [0]        
                  ?  [1] N + [4]        
                  =  [s(plus(N, M))]    
                                        
      [x(N, 0())] =  [1] N + [11]       
                  >  [7]                
                  =  [0()]              
                                        
     [x(N, s(M))] =  [1] N + [1] M + [8]
                  >  [1] N + [1] M + [4]
                  =  [plus(x(N, M), N)] 
                                        

Further, it can be verified that all rules not oriented are covered by the weightgap condition.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).

Strict Trs: { plus(N, s(M)) -> s(plus(N, M)) }
Weak Trs:
  { and(tt(), X) -> activate(X)
  , activate(X) -> X
  , plus(N, 0()) -> N
  , x(N, 0()) -> 0()
  , x(N, s(M)) -> plus(x(N, M), N) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^2))

We use the processor 'polynomial interpretation' to orient
following rules strictly.

Trs: { plus(N, s(M)) -> s(plus(N, M)) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^2)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  The following argument positions are considered usable:
  
    Uargs(plus) = {1}, Uargs(s) = {1}
  
  TcT has computed the following constructor-restricted polynomial
  interpretation.
  
   [and](x1, x2) = 1 + 3*x1 + 3*x1*x2 + 3*x1^2 + 3*x2 + 3*x2^2
                                                              
          [tt]() = 1                                          
                                                              
  [activate](x1) = 3 + x1 + 3*x1^2                            
                                                              
  [plus](x1, x2) = 3 + x1 + 2*x2                              
                                                              
           [0]() = 0                                          
                                                              
         [s](x1) = 1 + x1                                     
                                                              
     [x](x1, x2) = 2 + 2*x1 + 2*x1*x2 + 2*x2 + 2*x2^2         
                                                              
  
  The following symbols are considered usable
  
    {and, activate, plus, x}
  
  This order satisfies the following ordering constraints.
  
     [and(tt(), X)] = 7 + 6*X + 3*X^2              
                    > 3 + X + 3*X^2                
                    = [activate(X)]                
                                                   
      [activate(X)] = 3 + X + 3*X^2                
                    > X                            
                    = [X]                          
                                                   
     [plus(N, 0())] = 3 + N                        
                    > N                            
                    = [N]                          
                                                   
    [plus(N, s(M))] = 5 + N + 2*M                  
                    > 4 + N + 2*M                  
                    = [s(plus(N, M))]              
                                                   
        [x(N, 0())] = 2 + 2*N                      
                    >                              
                    = [0()]                        
                                                   
       [x(N, s(M))] = 6 + 4*N + 2*N*M + 6*M + 2*M^2
                    > 5 + 4*N + 2*N*M + 2*M + 2*M^2
                    = [plus(x(N, M), N)]           
                                                   

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
  { and(tt(), X) -> activate(X)
  , activate(X) -> 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) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^2))