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

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

Strict Trs:
  { 2nd(cons(X, n__cons(Y, Z))) -> activate(Y)
  , cons(X1, X2) -> n__cons(X1, X2)
  , activate(X) -> X
  , activate(n__cons(X1, X2)) -> cons(X1, X2)
  , activate(n__from(X)) -> from(X)
  , from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^1))

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

The following argument positions are usable:
  none

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

          [2nd](x1) = [1] x1 + [1]         
                                           
     [cons](x1, x2) = [1] x1 + [1] x2 + [7]
                                           
  [n__cons](x1, x2) = [1] x1 + [1] x2 + [7]
                                           
     [activate](x1) = [1] x1 + [7]         
                                           
         [from](x1) = [1] x1 + [3]         
                                           
      [n__from](x1) = [1] x1 + [7]         
                                           
            [s](x1) = [0]                  

The following symbols are considered usable

  {2nd, cons, activate, from}

The order satisfies the following ordering constraints:

  [2nd(cons(X, n__cons(Y, Z)))] =  [1] X + [1] Y + [1] Z + [15]
                                >  [1] Y + [7]                 
                                =  [activate(Y)]               
                                                               
                 [cons(X1, X2)] =  [1] X1 + [1] X2 + [7]       
                                >= [1] X1 + [1] X2 + [7]       
                                =  [n__cons(X1, X2)]           
                                                               
                  [activate(X)] =  [1] X + [7]                 
                                >  [1] X + [0]                 
                                =  [X]                         
                                                               
    [activate(n__cons(X1, X2))] =  [1] X1 + [1] X2 + [14]      
                                >  [1] X1 + [1] X2 + [7]       
                                =  [cons(X1, X2)]              
                                                               
         [activate(n__from(X))] =  [1] X + [14]                
                                >  [1] X + [3]                 
                                =  [from(X)]                   
                                                               
                      [from(X)] =  [1] X + [3]                 
                                ?  [1] X + [14]                
                                =  [cons(X, n__from(s(X)))]    
                                                               
                      [from(X)] =  [1] X + [3]                 
                                ?  [1] X + [7]                 
                                =  [n__from(X)]                
                                                               

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^1)).

Strict Trs:
  { cons(X1, X2) -> n__cons(X1, X2)
  , from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X) }
Weak Trs:
  { 2nd(cons(X, n__cons(Y, Z))) -> activate(Y)
  , activate(X) -> X
  , activate(n__cons(X1, X2)) -> cons(X1, X2)
  , activate(n__from(X)) -> from(X) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^1))

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

The following argument positions are usable:
  none

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

          [2nd](x1) = [1] x1 + [2]         
                                           
     [cons](x1, x2) = [1] x1 + [1] x2 + [7]
                                           
  [n__cons](x1, x2) = [1] x1 + [1] x2 + [6]
                                           
     [activate](x1) = [1] x1 + [7]         
                                           
         [from](x1) = [1] x1 + [7]         
                                           
      [n__from](x1) = [1] x1 + [6]         
                                           
            [s](x1) = [1]                  

The following symbols are considered usable

  {2nd, cons, activate, from}

The order satisfies the following ordering constraints:

  [2nd(cons(X, n__cons(Y, Z)))] = [1] X + [1] Y + [1] Z + [15]
                                > [1] Y + [7]                 
                                = [activate(Y)]               
                                                              
                 [cons(X1, X2)] = [1] X1 + [1] X2 + [7]       
                                > [1] X1 + [1] X2 + [6]       
                                = [n__cons(X1, X2)]           
                                                              
                  [activate(X)] = [1] X + [7]                 
                                > [1] X + [0]                 
                                = [X]                         
                                                              
    [activate(n__cons(X1, X2))] = [1] X1 + [1] X2 + [13]      
                                > [1] X1 + [1] X2 + [7]       
                                = [cons(X1, X2)]              
                                                              
         [activate(n__from(X))] = [1] X + [13]                
                                > [1] X + [7]                 
                                = [from(X)]                   
                                                              
                      [from(X)] = [1] X + [7]                 
                                ? [1] X + [14]                
                                = [cons(X, n__from(s(X)))]    
                                                              
                      [from(X)] = [1] X + [7]                 
                                > [1] X + [6]                 
                                = [n__from(X)]                
                                                              

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^1)).

Strict Trs: { from(X) -> cons(X, n__from(s(X))) }
Weak Trs:
  { 2nd(cons(X, n__cons(Y, Z))) -> activate(Y)
  , cons(X1, X2) -> n__cons(X1, X2)
  , activate(X) -> X
  , activate(n__cons(X1, X2)) -> cons(X1, X2)
  , activate(n__from(X)) -> from(X)
  , from(X) -> n__from(X) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(n^1))

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

The following argument positions are usable:
  none

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

          [2nd](x1) = [1] x1 + [7]         
                                           
     [cons](x1, x2) = [1] x1 + [1] x2 + [0]
                                           
  [n__cons](x1, x2) = [1] x1 + [1] x2 + [0]
                                           
     [activate](x1) = [1] x1 + [7]         
                                           
         [from](x1) = [1] x1 + [7]         
                                           
      [n__from](x1) = [1] x1 + [3]         
                                           
            [s](x1) = [3]                  

The following symbols are considered usable

  {2nd, cons, activate, from}

The order satisfies the following ordering constraints:

  [2nd(cons(X, n__cons(Y, Z)))] =  [1] X + [1] Y + [1] Z + [7]
                                >= [1] Y + [7]                
                                =  [activate(Y)]              
                                                              
                 [cons(X1, X2)] =  [1] X1 + [1] X2 + [0]      
                                >= [1] X1 + [1] X2 + [0]      
                                =  [n__cons(X1, X2)]          
                                                              
                  [activate(X)] =  [1] X + [7]                
                                >  [1] X + [0]                
                                =  [X]                        
                                                              
    [activate(n__cons(X1, X2))] =  [1] X1 + [1] X2 + [7]      
                                >  [1] X1 + [1] X2 + [0]      
                                =  [cons(X1, X2)]             
                                                              
         [activate(n__from(X))] =  [1] X + [10]               
                                >  [1] X + [7]                
                                =  [from(X)]                  
                                                              
                      [from(X)] =  [1] X + [7]                
                                >  [1] X + [6]                
                                =  [cons(X, n__from(s(X)))]   
                                                              
                      [from(X)] =  [1] X + [7]                
                                >  [1] X + [3]                
                                =  [n__from(X)]               
                                                              

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(1)).

Weak Trs:
  { 2nd(cons(X, n__cons(Y, Z))) -> activate(Y)
  , cons(X1, X2) -> n__cons(X1, X2)
  , activate(X) -> X
  , activate(n__cons(X1, X2)) -> cons(X1, X2)
  , activate(n__from(X)) -> from(X)
  , from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

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