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

Strict Trs:
  { primes() -> sieve(from(s(s(0()))))
  , sieve(X) -> n__sieve(X)
  , sieve(cons(X, Y)) -> cons(X, n__filter(X, n__sieve(activate(Y))))
  , from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , s(X) -> n__s(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , head(cons(X, Y)) -> X
  , tail(cons(X, Y)) -> activate(Y)
  , activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2))
  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  , activate(n__sieve(X)) -> sieve(activate(X))
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , filter(X1, X2) -> n__filter(X1, X2)
  , filter(s(s(X)), cons(Y, Z)) ->
    if(divides(s(s(X)), Y),
       n__filter(n__s(n__s(X)), activate(Z)),
       n__cons(Y, n__filter(X, n__sieve(Y)))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

Arguments of following rules are not normal-forms:

{ sieve(cons(X, Y)) -> cons(X, n__filter(X, n__sieve(activate(Y))))
, head(cons(X, Y)) -> X
, tail(cons(X, Y)) -> activate(Y)
, filter(s(s(X)), cons(Y, Z)) ->
  if(divides(s(s(X)), Y),
     n__filter(n__s(n__s(X)), activate(Z)),
     n__cons(Y, n__filter(X, n__sieve(Y)))) }

All above mentioned rules can be savely removed.

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

Strict Trs:
  { primes() -> sieve(from(s(s(0()))))
  , sieve(X) -> n__sieve(X)
  , from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , s(X) -> n__s(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2))
  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  , activate(n__sieve(X)) -> sieve(activate(X))
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , filter(X1, X2) -> n__filter(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We add the following dependency tuples:

Strict DPs:
  { primes^#() ->
    c_1(sieve^#(from(s(s(0())))),
        from^#(s(s(0()))),
        s^#(s(0())),
        s^#(0()))
  , sieve^#(X) -> c_2()
  , from^#(X) -> c_3(cons^#(X, n__from(n__s(X))))
  , from^#(X) -> c_4()
  , s^#(X) -> c_5()
  , cons^#(X1, X2) -> c_6()
  , activate^#(X) -> c_7()
  , activate^#(n__from(X)) -> c_8(from^#(activate(X)), activate^#(X))
  , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
  , activate^#(n__filter(X1, X2)) ->
    c_10(filter^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__cons(X1, X2)) ->
    c_11(cons^#(activate(X1), X2), activate^#(X1))
  , activate^#(n__sieve(X)) ->
    c_12(sieve^#(activate(X)), activate^#(X))
  , filter^#(X1, X2) -> c_15()
  , if^#(true(), X, Y) -> c_13(activate^#(X))
  , if^#(false(), X, Y) -> c_14(activate^#(Y)) }

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:
  { primes^#() ->
    c_1(sieve^#(from(s(s(0())))),
        from^#(s(s(0()))),
        s^#(s(0())),
        s^#(0()))
  , sieve^#(X) -> c_2()
  , from^#(X) -> c_3(cons^#(X, n__from(n__s(X))))
  , from^#(X) -> c_4()
  , s^#(X) -> c_5()
  , cons^#(X1, X2) -> c_6()
  , activate^#(X) -> c_7()
  , activate^#(n__from(X)) -> c_8(from^#(activate(X)), activate^#(X))
  , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
  , activate^#(n__filter(X1, X2)) ->
    c_10(filter^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__cons(X1, X2)) ->
    c_11(cons^#(activate(X1), X2), activate^#(X1))
  , activate^#(n__sieve(X)) ->
    c_12(sieve^#(activate(X)), activate^#(X))
  , filter^#(X1, X2) -> c_15()
  , if^#(true(), X, Y) -> c_13(activate^#(X))
  , if^#(false(), X, Y) -> c_14(activate^#(Y)) }
Weak Trs:
  { primes() -> sieve(from(s(s(0()))))
  , sieve(X) -> n__sieve(X)
  , from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , s(X) -> n__s(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2))
  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  , activate(n__sieve(X)) -> sieve(activate(X))
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , filter(X1, X2) -> n__filter(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We estimate the number of application of {2,4,5,6,7,13} by
applications of Pre({2,4,5,6,7,13}) = {1,3,8,9,10,11,12,14,15}.
Here rules are labeled as follows:

  DPs:
    { 1: primes^#() ->
         c_1(sieve^#(from(s(s(0())))),
             from^#(s(s(0()))),
             s^#(s(0())),
             s^#(0()))
    , 2: sieve^#(X) -> c_2()
    , 3: from^#(X) -> c_3(cons^#(X, n__from(n__s(X))))
    , 4: from^#(X) -> c_4()
    , 5: s^#(X) -> c_5()
    , 6: cons^#(X1, X2) -> c_6()
    , 7: activate^#(X) -> c_7()
    , 8: activate^#(n__from(X)) ->
         c_8(from^#(activate(X)), activate^#(X))
    , 9: activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
    , 10: activate^#(n__filter(X1, X2)) ->
          c_10(filter^#(activate(X1), activate(X2)),
               activate^#(X1),
               activate^#(X2))
    , 11: activate^#(n__cons(X1, X2)) ->
          c_11(cons^#(activate(X1), X2), activate^#(X1))
    , 12: activate^#(n__sieve(X)) ->
          c_12(sieve^#(activate(X)), activate^#(X))
    , 13: filter^#(X1, X2) -> c_15()
    , 14: if^#(true(), X, Y) -> c_13(activate^#(X))
    , 15: if^#(false(), X, Y) -> c_14(activate^#(Y)) }

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

Strict DPs:
  { primes^#() ->
    c_1(sieve^#(from(s(s(0())))),
        from^#(s(s(0()))),
        s^#(s(0())),
        s^#(0()))
  , from^#(X) -> c_3(cons^#(X, n__from(n__s(X))))
  , activate^#(n__from(X)) -> c_8(from^#(activate(X)), activate^#(X))
  , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
  , activate^#(n__filter(X1, X2)) ->
    c_10(filter^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__cons(X1, X2)) ->
    c_11(cons^#(activate(X1), X2), activate^#(X1))
  , activate^#(n__sieve(X)) ->
    c_12(sieve^#(activate(X)), activate^#(X))
  , if^#(true(), X, Y) -> c_13(activate^#(X))
  , if^#(false(), X, Y) -> c_14(activate^#(Y)) }
Weak DPs:
  { sieve^#(X) -> c_2()
  , from^#(X) -> c_4()
  , s^#(X) -> c_5()
  , cons^#(X1, X2) -> c_6()
  , activate^#(X) -> c_7()
  , filter^#(X1, X2) -> c_15() }
Weak Trs:
  { primes() -> sieve(from(s(s(0()))))
  , sieve(X) -> n__sieve(X)
  , from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , s(X) -> n__s(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2))
  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  , activate(n__sieve(X)) -> sieve(activate(X))
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , filter(X1, X2) -> n__filter(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

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

  DPs:
    { 1: primes^#() ->
         c_1(sieve^#(from(s(s(0())))),
             from^#(s(s(0()))),
             s^#(s(0())),
             s^#(0()))
    , 2: from^#(X) -> c_3(cons^#(X, n__from(n__s(X))))
    , 3: activate^#(n__from(X)) ->
         c_8(from^#(activate(X)), activate^#(X))
    , 4: activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
    , 5: activate^#(n__filter(X1, X2)) ->
         c_10(filter^#(activate(X1), activate(X2)),
              activate^#(X1),
              activate^#(X2))
    , 6: activate^#(n__cons(X1, X2)) ->
         c_11(cons^#(activate(X1), X2), activate^#(X1))
    , 7: activate^#(n__sieve(X)) ->
         c_12(sieve^#(activate(X)), activate^#(X))
    , 8: if^#(true(), X, Y) -> c_13(activate^#(X))
    , 9: if^#(false(), X, Y) -> c_14(activate^#(Y))
    , 10: sieve^#(X) -> c_2()
    , 11: from^#(X) -> c_4()
    , 12: s^#(X) -> c_5()
    , 13: cons^#(X1, X2) -> c_6()
    , 14: activate^#(X) -> c_7()
    , 15: filter^#(X1, X2) -> c_15() }

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

Strict DPs:
  { primes^#() ->
    c_1(sieve^#(from(s(s(0())))),
        from^#(s(s(0()))),
        s^#(s(0())),
        s^#(0()))
  , activate^#(n__from(X)) -> c_8(from^#(activate(X)), activate^#(X))
  , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
  , activate^#(n__filter(X1, X2)) ->
    c_10(filter^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__cons(X1, X2)) ->
    c_11(cons^#(activate(X1), X2), activate^#(X1))
  , activate^#(n__sieve(X)) ->
    c_12(sieve^#(activate(X)), activate^#(X))
  , if^#(true(), X, Y) -> c_13(activate^#(X))
  , if^#(false(), X, Y) -> c_14(activate^#(Y)) }
Weak DPs:
  { sieve^#(X) -> c_2()
  , from^#(X) -> c_3(cons^#(X, n__from(n__s(X))))
  , from^#(X) -> c_4()
  , s^#(X) -> c_5()
  , cons^#(X1, X2) -> c_6()
  , activate^#(X) -> c_7()
  , filter^#(X1, X2) -> c_15() }
Weak Trs:
  { primes() -> sieve(from(s(s(0()))))
  , sieve(X) -> n__sieve(X)
  , from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , s(X) -> n__s(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2))
  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  , activate(n__sieve(X)) -> sieve(activate(X))
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , filter(X1, X2) -> n__filter(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

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

  DPs:
    { 1: primes^#() ->
         c_1(sieve^#(from(s(s(0())))),
             from^#(s(s(0()))),
             s^#(s(0())),
             s^#(0()))
    , 2: activate^#(n__from(X)) ->
         c_8(from^#(activate(X)), activate^#(X))
    , 3: activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
    , 4: activate^#(n__filter(X1, X2)) ->
         c_10(filter^#(activate(X1), activate(X2)),
              activate^#(X1),
              activate^#(X2))
    , 5: activate^#(n__cons(X1, X2)) ->
         c_11(cons^#(activate(X1), X2), activate^#(X1))
    , 6: activate^#(n__sieve(X)) ->
         c_12(sieve^#(activate(X)), activate^#(X))
    , 7: if^#(true(), X, Y) -> c_13(activate^#(X))
    , 8: if^#(false(), X, Y) -> c_14(activate^#(Y))
    , 9: sieve^#(X) -> c_2()
    , 10: from^#(X) -> c_3(cons^#(X, n__from(n__s(X))))
    , 11: from^#(X) -> c_4()
    , 12: s^#(X) -> c_5()
    , 13: cons^#(X1, X2) -> c_6()
    , 14: activate^#(X) -> c_7()
    , 15: filter^#(X1, X2) -> c_15() }

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

Strict DPs:
  { activate^#(n__from(X)) -> c_8(from^#(activate(X)), activate^#(X))
  , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
  , activate^#(n__filter(X1, X2)) ->
    c_10(filter^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__cons(X1, X2)) ->
    c_11(cons^#(activate(X1), X2), activate^#(X1))
  , activate^#(n__sieve(X)) ->
    c_12(sieve^#(activate(X)), activate^#(X))
  , if^#(true(), X, Y) -> c_13(activate^#(X))
  , if^#(false(), X, Y) -> c_14(activate^#(Y)) }
Weak DPs:
  { primes^#() ->
    c_1(sieve^#(from(s(s(0())))),
        from^#(s(s(0()))),
        s^#(s(0())),
        s^#(0()))
  , sieve^#(X) -> c_2()
  , from^#(X) -> c_3(cons^#(X, n__from(n__s(X))))
  , from^#(X) -> c_4()
  , s^#(X) -> c_5()
  , cons^#(X1, X2) -> c_6()
  , activate^#(X) -> c_7()
  , filter^#(X1, X2) -> c_15() }
Weak Trs:
  { primes() -> sieve(from(s(s(0()))))
  , sieve(X) -> n__sieve(X)
  , from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , s(X) -> n__s(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2))
  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  , activate(n__sieve(X)) -> sieve(activate(X))
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , filter(X1, X2) -> n__filter(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

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

{ primes^#() ->
  c_1(sieve^#(from(s(s(0())))),
      from^#(s(s(0()))),
      s^#(s(0())),
      s^#(0()))
, sieve^#(X) -> c_2()
, from^#(X) -> c_3(cons^#(X, n__from(n__s(X))))
, from^#(X) -> c_4()
, s^#(X) -> c_5()
, cons^#(X1, X2) -> c_6()
, activate^#(X) -> c_7()
, filter^#(X1, X2) -> c_15() }

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

Strict DPs:
  { activate^#(n__from(X)) -> c_8(from^#(activate(X)), activate^#(X))
  , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
  , activate^#(n__filter(X1, X2)) ->
    c_10(filter^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__cons(X1, X2)) ->
    c_11(cons^#(activate(X1), X2), activate^#(X1))
  , activate^#(n__sieve(X)) ->
    c_12(sieve^#(activate(X)), activate^#(X))
  , if^#(true(), X, Y) -> c_13(activate^#(X))
  , if^#(false(), X, Y) -> c_14(activate^#(Y)) }
Weak Trs:
  { primes() -> sieve(from(s(s(0()))))
  , sieve(X) -> n__sieve(X)
  , from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , s(X) -> n__s(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2))
  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  , activate(n__sieve(X)) -> sieve(activate(X))
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , filter(X1, X2) -> n__filter(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { activate^#(n__from(X)) -> c_8(from^#(activate(X)), activate^#(X))
  , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
  , activate^#(n__filter(X1, X2)) ->
    c_10(filter^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__cons(X1, X2)) ->
    c_11(cons^#(activate(X1), X2), activate^#(X1))
  , activate^#(n__sieve(X)) ->
    c_12(sieve^#(activate(X)), activate^#(X)) }

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

Strict DPs:
  { activate^#(n__from(X)) -> c_1(activate^#(X))
  , activate^#(n__s(X)) -> c_2(activate^#(X))
  , activate^#(n__filter(X1, X2)) ->
    c_3(activate^#(X1), activate^#(X2))
  , activate^#(n__cons(X1, X2)) -> c_4(activate^#(X1))
  , activate^#(n__sieve(X)) -> c_5(activate^#(X))
  , if^#(true(), X, Y) -> c_6(activate^#(X))
  , if^#(false(), X, Y) -> c_7(activate^#(Y)) }
Weak Trs:
  { primes() -> sieve(from(s(s(0()))))
  , sieve(X) -> n__sieve(X)
  , from(X) -> cons(X, n__from(n__s(X)))
  , from(X) -> n__from(X)
  , s(X) -> n__s(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , activate(X) -> X
  , activate(n__from(X)) -> from(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2))
  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  , activate(n__sieve(X)) -> sieve(activate(X))
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , filter(X1, X2) -> n__filter(X1, X2) }
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:
  { activate^#(n__from(X)) -> c_1(activate^#(X))
  , activate^#(n__s(X)) -> c_2(activate^#(X))
  , activate^#(n__filter(X1, X2)) ->
    c_3(activate^#(X1), activate^#(X2))
  , activate^#(n__cons(X1, X2)) -> c_4(activate^#(X1))
  , activate^#(n__sieve(X)) -> c_5(activate^#(X))
  , if^#(true(), X, Y) -> c_6(activate^#(X))
  , if^#(false(), X, Y) -> c_7(activate^#(Y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

Consider the dependency graph

  1: activate^#(n__from(X)) -> c_1(activate^#(X))
     -->_1 activate^#(n__sieve(X)) -> c_5(activate^#(X)) :5
     -->_1 activate^#(n__cons(X1, X2)) -> c_4(activate^#(X1)) :4
     -->_1 activate^#(n__filter(X1, X2)) ->
           c_3(activate^#(X1), activate^#(X2)) :3
     -->_1 activate^#(n__s(X)) -> c_2(activate^#(X)) :2
     -->_1 activate^#(n__from(X)) -> c_1(activate^#(X)) :1
  
  2: activate^#(n__s(X)) -> c_2(activate^#(X))
     -->_1 activate^#(n__sieve(X)) -> c_5(activate^#(X)) :5
     -->_1 activate^#(n__cons(X1, X2)) -> c_4(activate^#(X1)) :4
     -->_1 activate^#(n__filter(X1, X2)) ->
           c_3(activate^#(X1), activate^#(X2)) :3
     -->_1 activate^#(n__s(X)) -> c_2(activate^#(X)) :2
     -->_1 activate^#(n__from(X)) -> c_1(activate^#(X)) :1
  
  3: activate^#(n__filter(X1, X2)) ->
     c_3(activate^#(X1), activate^#(X2))
     -->_2 activate^#(n__sieve(X)) -> c_5(activate^#(X)) :5
     -->_1 activate^#(n__sieve(X)) -> c_5(activate^#(X)) :5
     -->_2 activate^#(n__cons(X1, X2)) -> c_4(activate^#(X1)) :4
     -->_1 activate^#(n__cons(X1, X2)) -> c_4(activate^#(X1)) :4
     -->_2 activate^#(n__filter(X1, X2)) ->
           c_3(activate^#(X1), activate^#(X2)) :3
     -->_1 activate^#(n__filter(X1, X2)) ->
           c_3(activate^#(X1), activate^#(X2)) :3
     -->_2 activate^#(n__s(X)) -> c_2(activate^#(X)) :2
     -->_1 activate^#(n__s(X)) -> c_2(activate^#(X)) :2
     -->_2 activate^#(n__from(X)) -> c_1(activate^#(X)) :1
     -->_1 activate^#(n__from(X)) -> c_1(activate^#(X)) :1
  
  4: activate^#(n__cons(X1, X2)) -> c_4(activate^#(X1))
     -->_1 activate^#(n__sieve(X)) -> c_5(activate^#(X)) :5
     -->_1 activate^#(n__cons(X1, X2)) -> c_4(activate^#(X1)) :4
     -->_1 activate^#(n__filter(X1, X2)) ->
           c_3(activate^#(X1), activate^#(X2)) :3
     -->_1 activate^#(n__s(X)) -> c_2(activate^#(X)) :2
     -->_1 activate^#(n__from(X)) -> c_1(activate^#(X)) :1
  
  5: activate^#(n__sieve(X)) -> c_5(activate^#(X))
     -->_1 activate^#(n__sieve(X)) -> c_5(activate^#(X)) :5
     -->_1 activate^#(n__cons(X1, X2)) -> c_4(activate^#(X1)) :4
     -->_1 activate^#(n__filter(X1, X2)) ->
           c_3(activate^#(X1), activate^#(X2)) :3
     -->_1 activate^#(n__s(X)) -> c_2(activate^#(X)) :2
     -->_1 activate^#(n__from(X)) -> c_1(activate^#(X)) :1
  
  6: if^#(true(), X, Y) -> c_6(activate^#(X))
     -->_1 activate^#(n__sieve(X)) -> c_5(activate^#(X)) :5
     -->_1 activate^#(n__cons(X1, X2)) -> c_4(activate^#(X1)) :4
     -->_1 activate^#(n__filter(X1, X2)) ->
           c_3(activate^#(X1), activate^#(X2)) :3
     -->_1 activate^#(n__s(X)) -> c_2(activate^#(X)) :2
     -->_1 activate^#(n__from(X)) -> c_1(activate^#(X)) :1
  
  7: if^#(false(), X, Y) -> c_7(activate^#(Y))
     -->_1 activate^#(n__sieve(X)) -> c_5(activate^#(X)) :5
     -->_1 activate^#(n__cons(X1, X2)) -> c_4(activate^#(X1)) :4
     -->_1 activate^#(n__filter(X1, X2)) ->
           c_3(activate^#(X1), activate^#(X2)) :3
     -->_1 activate^#(n__s(X)) -> c_2(activate^#(X)) :2
     -->_1 activate^#(n__from(X)) -> c_1(activate^#(X)) :1
  

Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).

  { if^#(true(), X, Y) -> c_6(activate^#(X))
  , if^#(false(), X, Y) -> c_7(activate^#(Y)) }


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

Strict DPs:
  { activate^#(n__from(X)) -> c_1(activate^#(X))
  , activate^#(n__s(X)) -> c_2(activate^#(X))
  , activate^#(n__filter(X1, X2)) ->
    c_3(activate^#(X1), activate^#(X2))
  , activate^#(n__cons(X1, X2)) -> c_4(activate^#(X1))
  , activate^#(n__sieve(X)) -> c_5(activate^#(X)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
  { 1: activate^#(n__from(X)) -> c_1(activate^#(X))
  , 2: activate^#(n__s(X)) -> c_2(activate^#(X))
  , 3: activate^#(n__filter(X1, X2)) ->
       c_3(activate^#(X1), activate^#(X2))
  , 4: activate^#(n__cons(X1, X2)) -> c_4(activate^#(X1))
  , 5: activate^#(n__sieve(X)) -> c_5(activate^#(X)) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2},
    Uargs(c_4) = {1}, Uargs(c_5) = {1}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
          [n__from](x1) = [1] x1 + [4]         
                                               
             [n__s](x1) = [1] x1 + [4]         
                                               
    [n__filter](x1, x2) = [1] x1 + [1] x2 + [4]
                                               
      [n__cons](x1, x2) = [1] x1 + [4]         
                                               
         [n__sieve](x1) = [1] x1 + [4]         
                                               
       [activate^#](x1) = [2] x1 + [0]         
                                               
              [c_1](x1) = [1] x1 + [1]         
                                               
              [c_2](x1) = [1] x1 + [0]         
                                               
          [c_3](x1, x2) = [1] x1 + [1] x2 + [0]
                                               
              [c_4](x1) = [1] x1 + [0]         
                                               
              [c_5](x1) = [1] x1 + [0]         
  
  The order satisfies the following ordering constraints:
  
           [activate^#(n__from(X))] = [2] X + [8]                          
                                    > [2] X + [1]                          
                                    = [c_1(activate^#(X))]                 
                                                                           
              [activate^#(n__s(X))] = [2] X + [8]                          
                                    > [2] X + [0]                          
                                    = [c_2(activate^#(X))]                 
                                                                           
    [activate^#(n__filter(X1, X2))] = [2] X1 + [2] X2 + [8]                
                                    > [2] X1 + [2] X2 + [0]                
                                    = [c_3(activate^#(X1), activate^#(X2))]
                                                                           
      [activate^#(n__cons(X1, X2))] = [2] X1 + [8]                         
                                    > [2] X1 + [0]                         
                                    = [c_4(activate^#(X1))]                
                                                                           
          [activate^#(n__sieve(X))] = [2] X + [8]                          
                                    > [2] X + [0]                          
                                    = [c_5(activate^#(X))]                 
                                                                           

The strictly oriented rules are moved into the weak component.

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

Weak DPs:
  { activate^#(n__from(X)) -> c_1(activate^#(X))
  , activate^#(n__s(X)) -> c_2(activate^#(X))
  , activate^#(n__filter(X1, X2)) ->
    c_3(activate^#(X1), activate^#(X2))
  , activate^#(n__cons(X1, X2)) -> c_4(activate^#(X1))
  , activate^#(n__sieve(X)) -> c_5(activate^#(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.

{ activate^#(n__from(X)) -> c_1(activate^#(X))
, activate^#(n__s(X)) -> c_2(activate^#(X))
, activate^#(n__filter(X1, X2)) ->
  c_3(activate^#(X1), activate^#(X2))
, activate^#(n__cons(X1, X2)) -> c_4(activate^#(X1))
, activate^#(n__sieve(X)) -> c_5(activate^#(X)) }

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