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:
  { fst(X1, X2) -> n__fst(X1, X2)
  , fst(0(), Z) -> nil()
  , fst(s(X), cons(Y, Z)) ->
    cons(Y, n__fst(activate(X), activate(Z)))
  , activate(X) -> X
  , activate(n__fst(X1, X2)) -> fst(X1, X2)
  , activate(n__from(X)) -> from(X)
  , activate(n__add(X1, X2)) -> add(X1, X2)
  , activate(n__len(X)) -> len(X)
  , from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , add(X1, X2) -> n__add(X1, X2)
  , add(0(), X) -> X
  , add(s(X), Y) -> s(n__add(activate(X), Y))
  , len(X) -> n__len(X)
  , len(nil()) -> 0()
  , len(cons(X, Z)) -> s(n__len(activate(Z))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We add following weak dependency pairs:

Strict DPs:
  { fst^#(X1, X2) -> c_1()
  , fst^#(0(), Z) -> c_2()
  , fst^#(s(X), cons(Y, Z)) -> c_3(activate^#(X), activate^#(Z))
  , activate^#(X) -> c_4()
  , activate^#(n__fst(X1, X2)) -> c_5(fst^#(X1, X2))
  , activate^#(n__from(X)) -> c_6(from^#(X))
  , activate^#(n__add(X1, X2)) -> c_7(add^#(X1, X2))
  , activate^#(n__len(X)) -> c_8(len^#(X))
  , from^#(X) -> c_9()
  , from^#(X) -> c_10()
  , add^#(X1, X2) -> c_11()
  , add^#(0(), X) -> c_12()
  , add^#(s(X), Y) -> c_13(activate^#(X))
  , len^#(X) -> c_14()
  , len^#(nil()) -> c_15()
  , len^#(cons(X, Z)) -> c_16(activate^#(Z)) }

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:
  { fst^#(X1, X2) -> c_1()
  , fst^#(0(), Z) -> c_2()
  , fst^#(s(X), cons(Y, Z)) -> c_3(activate^#(X), activate^#(Z))
  , activate^#(X) -> c_4()
  , activate^#(n__fst(X1, X2)) -> c_5(fst^#(X1, X2))
  , activate^#(n__from(X)) -> c_6(from^#(X))
  , activate^#(n__add(X1, X2)) -> c_7(add^#(X1, X2))
  , activate^#(n__len(X)) -> c_8(len^#(X))
  , from^#(X) -> c_9()
  , from^#(X) -> c_10()
  , add^#(X1, X2) -> c_11()
  , add^#(0(), X) -> c_12()
  , add^#(s(X), Y) -> c_13(activate^#(X))
  , len^#(X) -> c_14()
  , len^#(nil()) -> c_15()
  , len^#(cons(X, Z)) -> c_16(activate^#(Z)) }
Strict Trs:
  { fst(X1, X2) -> n__fst(X1, X2)
  , fst(0(), Z) -> nil()
  , fst(s(X), cons(Y, Z)) ->
    cons(Y, n__fst(activate(X), activate(Z)))
  , activate(X) -> X
  , activate(n__fst(X1, X2)) -> fst(X1, X2)
  , activate(n__from(X)) -> from(X)
  , activate(n__add(X1, X2)) -> add(X1, X2)
  , activate(n__len(X)) -> len(X)
  , from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , add(X1, X2) -> n__add(X1, X2)
  , add(0(), X) -> X
  , add(s(X), Y) -> s(n__add(activate(X), Y))
  , len(X) -> n__len(X)
  , len(nil()) -> 0()
  , len(cons(X, Z)) -> s(n__len(activate(Z))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^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(n^1)).

Strict DPs:
  { fst^#(X1, X2) -> c_1()
  , fst^#(0(), Z) -> c_2()
  , fst^#(s(X), cons(Y, Z)) -> c_3(activate^#(X), activate^#(Z))
  , activate^#(X) -> c_4()
  , activate^#(n__fst(X1, X2)) -> c_5(fst^#(X1, X2))
  , activate^#(n__from(X)) -> c_6(from^#(X))
  , activate^#(n__add(X1, X2)) -> c_7(add^#(X1, X2))
  , activate^#(n__len(X)) -> c_8(len^#(X))
  , from^#(X) -> c_9()
  , from^#(X) -> c_10()
  , add^#(X1, X2) -> c_11()
  , add^#(0(), X) -> c_12()
  , add^#(s(X), Y) -> c_13(activate^#(X))
  , len^#(X) -> c_14()
  , len^#(nil()) -> c_15()
  , len^#(cons(X, Z)) -> c_16(activate^#(Z)) }
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(c_3) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1},
  Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_13) = {1},
  Uargs(c_16) = {1}

TcT has computed following constructor-restricted matrix
interpretation.

               [0] = [2]                  
                                          
             [nil] = [2]                  
                                          
           [s](x1) = [1] x1 + [1]         
                                          
    [cons](x1, x2) = [1] x2 + [2]         
                                          
  [n__fst](x1, x2) = [1] x1 + [1] x2 + [1]
                                          
     [n__from](x1) = [1] x1 + [2]         
                                          
  [n__add](x1, x2) = [1] x1 + [1] x2 + [1]
                                          
      [n__len](x1) = [1] x1 + [1]         
                                          
   [fst^#](x1, x2) = [2] x1 + [2] x2 + [1]
                                          
             [c_1] = [0]                  
                                          
             [c_2] = [0]                  
                                          
     [c_3](x1, x2) = [1] x1 + [1] x2 + [2]
                                          
  [activate^#](x1) = [2] x1 + [2]         
                                          
             [c_4] = [1]                  
                                          
         [c_5](x1) = [1] x1 + [1]         
                                          
         [c_6](x1) = [1] x1 + [0]         
                                          
      [from^#](x1) = [2] x1 + [1]         
                                          
         [c_7](x1) = [1] x1 + [1]         
                                          
   [add^#](x1, x2) = [2] x1 + [2] x2 + [2]
                                          
         [c_8](x1) = [1] x1 + [1]         
                                          
       [len^#](x1) = [2] x1 + [2]         
                                          
             [c_9] = [0]                  
                                          
            [c_10] = [0]                  
                                          
            [c_11] = [1]                  
                                          
            [c_12] = [1]                  
                                          
        [c_13](x1) = [1] x1 + [1]         
                                          
            [c_14] = [1]                  
                                          
            [c_15] = [1]                  
                                          
        [c_16](x1) = [1] x1 + [1]         

This order satisfies following ordering constraints:


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 DPs:
  { fst^#(X1, X2) -> c_1()
  , fst^#(0(), Z) -> c_2()
  , fst^#(s(X), cons(Y, Z)) -> c_3(activate^#(X), activate^#(Z))
  , activate^#(X) -> c_4()
  , activate^#(n__fst(X1, X2)) -> c_5(fst^#(X1, X2))
  , activate^#(n__from(X)) -> c_6(from^#(X))
  , activate^#(n__add(X1, X2)) -> c_7(add^#(X1, X2))
  , activate^#(n__len(X)) -> c_8(len^#(X))
  , from^#(X) -> c_9()
  , from^#(X) -> c_10()
  , add^#(X1, X2) -> c_11()
  , add^#(0(), X) -> c_12()
  , add^#(s(X), Y) -> c_13(activate^#(X))
  , len^#(X) -> c_14()
  , len^#(nil()) -> c_15()
  , len^#(cons(X, Z)) -> c_16(activate^#(Z)) }
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.

{ fst^#(X1, X2) -> c_1()
, fst^#(0(), Z) -> c_2()
, fst^#(s(X), cons(Y, Z)) -> c_3(activate^#(X), activate^#(Z))
, activate^#(X) -> c_4()
, activate^#(n__fst(X1, X2)) -> c_5(fst^#(X1, X2))
, activate^#(n__from(X)) -> c_6(from^#(X))
, activate^#(n__add(X1, X2)) -> c_7(add^#(X1, X2))
, activate^#(n__len(X)) -> c_8(len^#(X))
, from^#(X) -> c_9()
, from^#(X) -> c_10()
, add^#(X1, X2) -> c_11()
, add^#(0(), X) -> c_12()
, add^#(s(X), Y) -> c_13(activate^#(X))
, len^#(X) -> c_14()
, len^#(nil()) -> c_15()
, len^#(cons(X, Z)) -> c_16(activate^#(Z)) }

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