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(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 innermost 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]      [0]
                                   
    [cons](x1, x2) = [1 0] x2 + [0]
                     [0 1]      [0]
                                   
    [activate](x1) = [1 2] x1 + [1]
                     [0 2]      [0]
                                   
        [from](x1) = [1 0] x1 + [1]
                     [0 1]      [2]
                                   
     [n__from](x1) = [1 0] x1 + [0]
                     [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] = [1]           
                     [1]           
                                   
         [c_2](x1) = [1 0] x1 + [1]
                     [0 1]      [2]
                                   
  [activate^#](x1) = [1 2] x1 + [2]
                     [1 2]      [2]
                                   
             [c_3] = [1]           
                     [1]           
                                   
         [c_4](x1) = [1 0] x1 + [2]
                     [0 1]      [2]
                                   
      [from^#](x1) = [1 0] x1 + [1]
                     [0 0]      [2]
                                   
         [c_5](x1) = [1 0] x1 + [2]
                     [0 1]      [2]
                                   
         [s^#](x1) = [1 0] x1 + [1]
                     [0 0]      [2]
                                   
             [c_6] = [1]           
                     [1]           
                                   
             [c_7] = [1]           
                     [1]           
                                   
             [c_8] = [1]           
                     [1]           

The following symbols are considered usable

  {activate, from, s, 2nd^#, activate^#, from^#, s^#}

The order satisfies the following ordering constraints:

                  [activate(X)] =  [1 2] X + [1]                       
                                   [0 2]     [0]                       
                                >  [1 0] X + [0]                       
                                   [0 1]     [0]                       
                                =  [X]                                 
                                                                       
         [activate(n__from(X))] =  [1 2] X + [3]                       
                                   [0 2]     [2]                       
                                >  [1 2] X + [2]                       
                                   [0 2]     [2]                       
                                =  [from(activate(X))]                 
                                                                       
            [activate(n__s(X))] =  [1 2] X + [3]                       
                                   [0 2]     [2]                       
                                >  [1 2] X + [2]                       
                                   [0 2]     [1]                       
                                =  [s(activate(X))]                    
                                                                       
                      [from(X)] =  [1 0] X + [1]                       
                                   [0 1]     [2]                       
                                >  [1 0] X + [0]                       
                                   [0 1]     [2]                       
                                =  [cons(X, n__from(n__s(X)))]         
                                                                       
                      [from(X)] =  [1 0] X + [1]                       
                                   [0 1]     [2]                       
                                >  [1 0] X + [0]                       
                                   [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 + [0]                       
                                   [0 0]     [0]                       
                                ?  [1]                                 
                                   [1]                                 
                                =  [c_1()]                             
                                                                       
           [2nd^#(cons(X, X1))] =  [1 2] X1 + [0]                      
                                   [0 0]      [0]                      
                                ?  [1 2] X1 + [2]                      
                                   [0 0]      [2]                      
                                =  [c_2(2nd^#(cons1(X, activate(X1))))]
                                                                       
                [activate^#(X)] =  [1 2] X + [2]                       
                                   [1 2]     [2]                       
                                >  [1]                                 
                                   [1]                                 
                                =  [c_3()]                             
                                                                       
       [activate^#(n__from(X))] =  [1 2] X + [4]                       
                                   [1 2]     [4]                       
                                >= [1 2] X + [4]                       
                                   [0 0]     [4]                       
                                =  [c_4(from^#(activate(X)))]          
                                                                       
          [activate^#(n__s(X))] =  [1 2] X + [4]                       
                                   [1 2]     [4]                       
                                >= [1 2] X + [4]                       
                                   [0 0]     [4]                       
                                =  [c_5(s^#(activate(X)))]             
                                                                       
                    [from^#(X)] =  [1 0] X + [1]                       
                                   [0 0]     [2]                       
                                >= [1]                                 
                                   [1]                                 
                                =  [c_6()]                             
                                                                       
                    [from^#(X)] =  [1 0] X + [1]                       
                                   [0 0]     [2]                       
                                >= [1]                                 
                                   [1]                                 
                                =  [c_7()]                             
                                                                       
                       [s^#(X)] =  [1 0] X + [1]                       
                                   [0 0]     [2]                       
                                >= [1]                                 
                                   [1]                                 
                                =  [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^#(cons1(X, cons(Y, Z))) -> c_1()
  , 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
  , 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() }
Weak DPs: { activate^#(X) -> c_3() }
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,5,6,7} by applications
of Pre({1,5,6,7}) = {2,3,4}. Here rules are labeled as follows:

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

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^#(n__from(X)) -> c_4(from^#(activate(X)))
  , activate^#(n__s(X)) -> c_5(s^#(activate(X))) }
Weak DPs:
  { 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
  , activate^#(X) -> c_3()
  , from^#(X) -> c_6()
  , from^#(X) -> c_7()
  , 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,2,3} by applications of
Pre({1,2,3}) = {}. Here rules are labeled as follows:

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

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

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)))
  , from^#(X) -> c_6()
  , from^#(X) -> c_7()
  , 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__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() }

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