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

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

We add the following weak dependency pairs:

Strict DPs:
  { 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
  , 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
  , activate^#(X) -> c_3()
  , activate^#(n__from(X)) -> c_4(from^#(activate(X)))
  , activate^#(n__s(X)) -> c_5(s^#(activate(X)))
  , from^#(X) -> c_6()
  , from^#(X) -> c_7()
  , s^#(X) -> c_8() }

and mark the set of starting terms.

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

Strict DPs:
  { 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
  , 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
  , activate^#(X) -> c_3()
  , activate^#(n__from(X)) -> c_4(from^#(activate(X)))
  , activate^#(n__s(X)) -> c_5(s^#(activate(X)))
  , from^#(X) -> c_6()
  , from^#(X) -> c_7()
  , s^#(X) -> c_8() }
Strict Trs:
  { 2nd(cons1(X, cons(Y, Z))) -> Y
  , 2nd(cons(X, X1)) -> 2nd(cons1(X, activate(X1)))
  , activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , s(X) -> n__s(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We replace rewrite rules by usable rules:

  Strict Usable Rules:
    { activate(X) -> X
    , activate(n__from(X)) -> from(activate(X))
    , activate(n__s(X)) -> s(activate(X))
    , from(X) -> cons(X, n__from(n__s(X)))
    , from(X) -> n__from(X)
    , s(X) -> n__s(X) }

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

Strict DPs:
  { 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
  , 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
  , activate^#(X) -> c_3()
  , activate^#(n__from(X)) -> c_4(from^#(activate(X)))
  , activate^#(n__s(X)) -> c_5(s^#(activate(X)))
  , from^#(X) -> c_6()
  , from^#(X) -> c_7()
  , s^#(X) -> c_8() }
Strict Trs:
  { activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , s(X) -> n__s(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

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

The following argument positions are usable:
  Uargs(cons1) = {2}, Uargs(from) = {1}, Uargs(s) = {1},
  Uargs(2nd^#) = {1}, Uargs(c_2) = {1}, Uargs(c_4) = {1},
  Uargs(from^#) = {1}, Uargs(c_5) = {1}, Uargs(s^#) = {1}

TcT has computed the following constructor-restricted matrix
interpretation.

   [cons1](x1, x2) = [1 0] x2 + [0]
                     [0 0]      [1]
                                   
    [cons](x1, x2) = [1 0] x2 + [0]
                     [0 1]      [0]
                                   
    [activate](x1) = [1 2] x1 + [2]
                     [1 1]      [0]
                                   
        [from](x1) = [1 0] x1 + [2]
                     [0 1]      [2]
                                   
     [n__from](x1) = [1 0] x1 + [1]
                     [0 1]      [1]
                                   
        [n__s](x1) = [1 0] x1 + [0]
                     [0 1]      [1]
                                   
           [s](x1) = [1 0] x1 + [1]
                     [0 1]      [1]
                                   
       [2nd^#](x1) = [1 2] x1 + [0]
                     [0 0]      [0]
                                   
             [c_1] = [0]           
                     [0]           
                                   
         [c_2](x1) = [1 0] x1 + [0]
                     [0 1]      [0]
                                   
  [activate^#](x1) = [2 2] x1 + [0]
                     [0 0]      [0]
                                   
             [c_3] = [0]           
                     [0]           
                                   
         [c_4](x1) = [1 0] x1 + [0]
                     [0 1]      [0]
                                   
      [from^#](x1) = [1 0] x1 + [0]
                     [0 0]      [0]
                                   
         [c_5](x1) = [1 0] x1 + [0]
                     [0 1]      [0]
                                   
         [s^#](x1) = [1 0] x1 + [0]
                     [0 0]      [0]
                                   
             [c_6] = [0]           
                     [0]           
                                   
             [c_7] = [0]           
                     [0]           
                                   
             [c_8] = [0]           
                     [0]           

The order satisfies the following ordering constraints:

                  [activate(X)] =  [1 2] X + [2]                       
                                   [1 1]     [0]                       
                                >  [1 0] X + [0]                       
                                   [0 1]     [0]                       
                                =  [X]                                 
                                                                       
         [activate(n__from(X))] =  [1 2] X + [5]                       
                                   [1 1]     [2]                       
                                >  [1 2] X + [4]                       
                                   [1 1]     [2]                       
                                =  [from(activate(X))]                 
                                                                       
            [activate(n__s(X))] =  [1 2] X + [4]                       
                                   [1 1]     [1]                       
                                >  [1 2] X + [3]                       
                                   [1 1]     [1]                       
                                =  [s(activate(X))]                    
                                                                       
                      [from(X)] =  [1 0] X + [2]                       
                                   [0 1]     [2]                       
                                >  [1 0] X + [1]                       
                                   [0 1]     [2]                       
                                =  [cons(X, n__from(n__s(X)))]         
                                                                       
                      [from(X)] =  [1 0] X + [2]                       
                                   [0 1]     [2]                       
                                >  [1 0] X + [1]                       
                                   [0 1]     [1]                       
                                =  [n__from(X)]                        
                                                                       
                         [s(X)] =  [1 0] X + [1]                       
                                   [0 1]     [1]                       
                                >  [1 0] X + [0]                       
                                   [0 1]     [1]                       
                                =  [n__s(X)]                           
                                                                       
  [2nd^#(cons1(X, cons(Y, Z)))] =  [1 0] Z + [2]                       
                                   [0 0]     [0]                       
                                >  [0]                                 
                                   [0]                                 
                                =  [c_1()]                             
                                                                       
           [2nd^#(cons(X, X1))] =  [1 2] X1 + [0]                      
                                   [0 0]      [0]                      
                                ?  [1 2] X1 + [4]                      
                                   [0 0]      [0]                      
                                =  [c_2(2nd^#(cons1(X, activate(X1))))]
                                                                       
                [activate^#(X)] =  [2 2] X + [0]                       
                                   [0 0]     [0]                       
                                >= [0]                                 
                                   [0]                                 
                                =  [c_3()]                             
                                                                       
       [activate^#(n__from(X))] =  [2 2] X + [4]                       
                                   [0 0]     [0]                       
                                >  [1 2] X + [2]                       
                                   [0 0]     [0]                       
                                =  [c_4(from^#(activate(X)))]          
                                                                       
          [activate^#(n__s(X))] =  [2 2] X + [2]                       
                                   [0 0]     [0]                       
                                >= [1 2] X + [2]                       
                                   [0 0]     [0]                       
                                =  [c_5(s^#(activate(X)))]             
                                                                       
                    [from^#(X)] =  [1 0] X + [0]                       
                                   [0 0]     [0]                       
                                >= [0]                                 
                                   [0]                                 
                                =  [c_6()]                             
                                                                       
                    [from^#(X)] =  [1 0] X + [0]                       
                                   [0 0]     [0]                       
                                >= [0]                                 
                                   [0]                                 
                                =  [c_7()]                             
                                                                       
                       [s^#(X)] =  [1 0] X + [0]                       
                                   [0 0]     [0]                       
                                >= [0]                                 
                                   [0]                                 
                                =  [c_8()]                             
                                                                       

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

Strict DPs:
  { 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
  , activate^#(X) -> c_3()
  , activate^#(n__s(X)) -> c_5(s^#(activate(X)))
  , from^#(X) -> c_6()
  , from^#(X) -> c_7()
  , s^#(X) -> c_8() }
Weak DPs:
  { 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
  , activate^#(n__from(X)) -> c_4(from^#(activate(X))) }
Weak Trs:
  { activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , s(X) -> n__s(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

We estimate the number of application of {1,2,6} by applications of
Pre({1,2,6}) = {3}. Here rules are labeled as follows:

  DPs:
    { 1: 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
    , 2: activate^#(X) -> c_3()
    , 3: activate^#(n__s(X)) -> c_5(s^#(activate(X)))
    , 4: from^#(X) -> c_6()
    , 5: from^#(X) -> c_7()
    , 6: s^#(X) -> c_8()
    , 7: 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
    , 8: activate^#(n__from(X)) -> c_4(from^#(activate(X))) }

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

Strict DPs:
  { activate^#(n__s(X)) -> c_5(s^#(activate(X)))
  , from^#(X) -> c_6()
  , from^#(X) -> c_7() }
Weak DPs:
  { 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
  , 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
  , activate^#(X) -> c_3()
  , activate^#(n__from(X)) -> c_4(from^#(activate(X)))
  , s^#(X) -> c_8() }
Weak Trs:
  { activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , s(X) -> n__s(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

We estimate the number of application of {1} by applications of
Pre({1}) = {}. Here rules are labeled as follows:

  DPs:
    { 1: activate^#(n__s(X)) -> c_5(s^#(activate(X)))
    , 2: from^#(X) -> c_6()
    , 3: from^#(X) -> c_7()
    , 4: 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
    , 5: 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
    , 6: activate^#(X) -> c_3()
    , 7: activate^#(n__from(X)) -> c_4(from^#(activate(X)))
    , 8: s^#(X) -> c_8() }

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

Strict DPs:
  { from^#(X) -> c_6()
  , from^#(X) -> c_7() }
Weak DPs:
  { 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
  , 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
  , activate^#(X) -> c_3()
  , activate^#(n__from(X)) -> c_4(from^#(activate(X)))
  , activate^#(n__s(X)) -> c_5(s^#(activate(X)))
  , s^#(X) -> c_8() }
Weak Trs:
  { activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , s(X) -> n__s(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
, 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
, activate^#(X) -> c_3()
, activate^#(n__s(X)) -> c_5(s^#(activate(X)))
, s^#(X) -> c_8() }

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

Strict DPs:
  { from^#(X) -> c_6()
  , from^#(X) -> c_7() }
Weak DPs: { activate^#(n__from(X)) -> c_4(from^#(activate(X))) }
Weak Trs:
  { activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , s(X) -> n__s(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict
rules from (R) into the weak component:

Problem (R):
------------
  Strict DPs: { from^#(X) -> c_7() }
  Weak DPs:
    { activate^#(n__from(X)) -> c_4(from^#(activate(X)))
    , from^#(X) -> c_6() }
  Weak Trs:
    { activate(X) -> X
    , activate(n__from(X)) -> from(activate(X))
    , activate(n__s(X)) -> s(activate(X))
    , from(X) -> cons(X, n__from(n__s(X)))
    , from(X) -> n__from(X)
    , s(X) -> n__s(X) }
  StartTerms: basic terms
  Strategy: innermost

Problem (S):
------------
  Strict DPs: { from^#(X) -> c_6() }
  Weak DPs:
    { activate^#(n__from(X)) -> c_4(from^#(activate(X)))
    , from^#(X) -> c_7() }
  Weak Trs:
    { activate(X) -> X
    , activate(n__from(X)) -> from(activate(X))
    , activate(n__s(X)) -> s(activate(X))
    , from(X) -> cons(X, n__from(n__s(X)))
    , from(X) -> n__from(X)
    , s(X) -> n__s(X) }
  StartTerms: basic terms
  Strategy: innermost

Overall, the transformation results in the following sub-problem(s):

Generated new problems:
-----------------------
R) Strict DPs: { from^#(X) -> c_7() }
   Weak DPs:
     { activate^#(n__from(X)) -> c_4(from^#(activate(X)))
     , from^#(X) -> c_6() }
   Weak Trs:
     { activate(X) -> X
     , activate(n__from(X)) -> from(activate(X))
     , activate(n__s(X)) -> s(activate(X))
     , from(X) -> cons(X, n__from(n__s(X)))
     , from(X) -> n__from(X)
     , s(X) -> n__s(X) }
   StartTerms: basic terms
   Strategy: innermost
   
   This problem was proven YES(O(1),O(1)).

S) Strict DPs: { from^#(X) -> c_6() }
   Weak DPs:
     { activate^#(n__from(X)) -> c_4(from^#(activate(X)))
     , from^#(X) -> c_7() }
   Weak Trs:
     { activate(X) -> X
     , activate(n__from(X)) -> from(activate(X))
     , activate(n__s(X)) -> s(activate(X))
     , from(X) -> cons(X, n__from(n__s(X)))
     , from(X) -> n__from(X)
     , s(X) -> n__s(X) }
   StartTerms: basic terms
   Strategy: innermost
   
   This problem was proven YES(O(1),O(1)).


Proofs for generated problems:
------------------------------
R) We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(1)).
   
   Strict DPs: { from^#(X) -> c_7() }
   Weak DPs:
     { activate^#(n__from(X)) -> c_4(from^#(activate(X)))
     , from^#(X) -> c_6() }
   Weak Trs:
     { activate(X) -> X
     , activate(n__from(X)) -> from(activate(X))
     , activate(n__s(X)) -> s(activate(X))
     , from(X) -> cons(X, n__from(n__s(X)))
     , from(X) -> n__from(X)
     , s(X) -> n__s(X) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(1))
   
   The following weak DPs constitute a sub-graph of the DG that is
   closed under successors. The DPs are removed.
   
   { from^#(X) -> c_6() }
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(1)).
   
   Strict DPs: { from^#(X) -> c_7() }
   Weak DPs: { activate^#(n__from(X)) -> c_4(from^#(activate(X))) }
   Weak Trs:
     { activate(X) -> X
     , activate(n__from(X)) -> from(activate(X))
     , activate(n__s(X)) -> s(activate(X))
     , from(X) -> cons(X, n__from(n__s(X)))
     , from(X) -> n__from(X)
     , s(X) -> n__s(X) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(1))
   
   The dependency graph contains no loops, we remove all dependency
   pairs.
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(1)).
   
   Weak Trs:
     { activate(X) -> X
     , activate(n__from(X)) -> from(activate(X))
     , activate(n__s(X)) -> s(activate(X))
     , from(X) -> cons(X, n__from(n__s(X)))
     , from(X) -> n__from(X)
     , s(X) -> n__s(X) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(1))
   
   No rule is usable, rules are removed from the input problem.
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(1)).
   
   Rules: Empty
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(1))
   
   Empty rules are trivially bounded

S) We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(1)).
   
   Strict DPs: { from^#(X) -> c_6() }
   Weak DPs:
     { activate^#(n__from(X)) -> c_4(from^#(activate(X)))
     , from^#(X) -> c_7() }
   Weak Trs:
     { activate(X) -> X
     , activate(n__from(X)) -> from(activate(X))
     , activate(n__s(X)) -> s(activate(X))
     , from(X) -> cons(X, n__from(n__s(X)))
     , from(X) -> n__from(X)
     , s(X) -> n__s(X) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(1))
   
   The following weak DPs constitute a sub-graph of the DG that is
   closed under successors. The DPs are removed.
   
   { from^#(X) -> c_7() }
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(1)).
   
   Strict DPs: { from^#(X) -> c_6() }
   Weak DPs: { activate^#(n__from(X)) -> c_4(from^#(activate(X))) }
   Weak Trs:
     { activate(X) -> X
     , activate(n__from(X)) -> from(activate(X))
     , activate(n__s(X)) -> s(activate(X))
     , from(X) -> cons(X, n__from(n__s(X)))
     , from(X) -> n__from(X)
     , s(X) -> n__s(X) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(1))
   
   The dependency graph contains no loops, we remove all dependency
   pairs.
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(1)).
   
   Weak Trs:
     { activate(X) -> X
     , activate(n__from(X)) -> from(activate(X))
     , activate(n__s(X)) -> s(activate(X))
     , from(X) -> cons(X, n__from(n__s(X)))
     , from(X) -> n__from(X)
     , s(X) -> n__s(X) }
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(1))
   
   No rule is usable, rules are removed from the input problem.
   
   We are left with following problem, upon which TcT provides the
   certificate YES(O(1),O(1)).
   
   Rules: Empty
   Obligation:
     innermost runtime complexity
   Answer:
     YES(O(1),O(1))
   
   Empty rules are trivially bounded


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