MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { filter(X1, X2, X3) -> n__filter(X1, X2, X3)
  , filter(cons(X, Y), 0(), M) ->
    cons(0(), n__filter(activate(Y), M, M))
  , filter(cons(X, Y), s(N), M) ->
    cons(X, n__filter(activate(Y), N, M))
  , activate(X) -> X
  , activate(n__filter(X1, X2, X3)) -> filter(X1, X2, X3)
  , activate(n__sieve(X)) -> sieve(X)
  , activate(n__nats(X)) -> nats(X)
  , sieve(X) -> n__sieve(X)
  , sieve(cons(0(), Y)) -> cons(0(), n__sieve(activate(Y)))
  , sieve(cons(s(N), Y)) ->
    cons(s(N), n__sieve(filter(activate(Y), N, N)))
  , nats(N) -> cons(N, n__nats(s(N)))
  , nats(X) -> n__nats(X)
  , zprimes() -> sieve(nats(s(s(0())))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { filter^#(X1, X2, X3) -> c_1()
  , filter^#(cons(X, Y), 0(), M) -> c_2(activate^#(Y))
  , filter^#(cons(X, Y), s(N), M) -> c_3(activate^#(Y))
  , activate^#(X) -> c_4()
  , activate^#(n__filter(X1, X2, X3)) -> c_5(filter^#(X1, X2, X3))
  , activate^#(n__sieve(X)) -> c_6(sieve^#(X))
  , activate^#(n__nats(X)) -> c_7(nats^#(X))
  , sieve^#(X) -> c_8()
  , sieve^#(cons(0(), Y)) -> c_9(activate^#(Y))
  , sieve^#(cons(s(N), Y)) ->
    c_10(filter^#(activate(Y), N, N), activate^#(Y))
  , nats^#(N) -> c_11()
  , nats^#(X) -> c_12()
  , zprimes^#() ->
    c_13(sieve^#(nats(s(s(0())))), nats^#(s(s(0())))) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { filter^#(X1, X2, X3) -> c_1()
  , filter^#(cons(X, Y), 0(), M) -> c_2(activate^#(Y))
  , filter^#(cons(X, Y), s(N), M) -> c_3(activate^#(Y))
  , activate^#(X) -> c_4()
  , activate^#(n__filter(X1, X2, X3)) -> c_5(filter^#(X1, X2, X3))
  , activate^#(n__sieve(X)) -> c_6(sieve^#(X))
  , activate^#(n__nats(X)) -> c_7(nats^#(X))
  , sieve^#(X) -> c_8()
  , sieve^#(cons(0(), Y)) -> c_9(activate^#(Y))
  , sieve^#(cons(s(N), Y)) ->
    c_10(filter^#(activate(Y), N, N), activate^#(Y))
  , nats^#(N) -> c_11()
  , nats^#(X) -> c_12()
  , zprimes^#() ->
    c_13(sieve^#(nats(s(s(0())))), nats^#(s(s(0())))) }
Weak Trs:
  { filter(X1, X2, X3) -> n__filter(X1, X2, X3)
  , filter(cons(X, Y), 0(), M) ->
    cons(0(), n__filter(activate(Y), M, M))
  , filter(cons(X, Y), s(N), M) ->
    cons(X, n__filter(activate(Y), N, M))
  , activate(X) -> X
  , activate(n__filter(X1, X2, X3)) -> filter(X1, X2, X3)
  , activate(n__sieve(X)) -> sieve(X)
  , activate(n__nats(X)) -> nats(X)
  , sieve(X) -> n__sieve(X)
  , sieve(cons(0(), Y)) -> cons(0(), n__sieve(activate(Y)))
  , sieve(cons(s(N), Y)) ->
    cons(s(N), n__sieve(filter(activate(Y), N, N)))
  , nats(N) -> cons(N, n__nats(s(N)))
  , nats(X) -> n__nats(X)
  , zprimes() -> sieve(nats(s(s(0())))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: filter^#(X1, X2, X3) -> c_1()
    , 2: filter^#(cons(X, Y), 0(), M) -> c_2(activate^#(Y))
    , 3: filter^#(cons(X, Y), s(N), M) -> c_3(activate^#(Y))
    , 4: activate^#(X) -> c_4()
    , 5: activate^#(n__filter(X1, X2, X3)) -> c_5(filter^#(X1, X2, X3))
    , 6: activate^#(n__sieve(X)) -> c_6(sieve^#(X))
    , 7: activate^#(n__nats(X)) -> c_7(nats^#(X))
    , 8: sieve^#(X) -> c_8()
    , 9: sieve^#(cons(0(), Y)) -> c_9(activate^#(Y))
    , 10: sieve^#(cons(s(N), Y)) ->
          c_10(filter^#(activate(Y), N, N), activate^#(Y))
    , 11: nats^#(N) -> c_11()
    , 12: nats^#(X) -> c_12()
    , 13: zprimes^#() ->
          c_13(sieve^#(nats(s(s(0())))), nats^#(s(s(0())))) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { filter^#(cons(X, Y), 0(), M) -> c_2(activate^#(Y))
  , filter^#(cons(X, Y), s(N), M) -> c_3(activate^#(Y))
  , activate^#(n__filter(X1, X2, X3)) -> c_5(filter^#(X1, X2, X3))
  , activate^#(n__sieve(X)) -> c_6(sieve^#(X))
  , activate^#(n__nats(X)) -> c_7(nats^#(X))
  , sieve^#(cons(0(), Y)) -> c_9(activate^#(Y))
  , sieve^#(cons(s(N), Y)) ->
    c_10(filter^#(activate(Y), N, N), activate^#(Y))
  , zprimes^#() ->
    c_13(sieve^#(nats(s(s(0())))), nats^#(s(s(0())))) }
Weak DPs:
  { filter^#(X1, X2, X3) -> c_1()
  , activate^#(X) -> c_4()
  , sieve^#(X) -> c_8()
  , nats^#(N) -> c_11()
  , nats^#(X) -> c_12() }
Weak Trs:
  { filter(X1, X2, X3) -> n__filter(X1, X2, X3)
  , filter(cons(X, Y), 0(), M) ->
    cons(0(), n__filter(activate(Y), M, M))
  , filter(cons(X, Y), s(N), M) ->
    cons(X, n__filter(activate(Y), N, M))
  , activate(X) -> X
  , activate(n__filter(X1, X2, X3)) -> filter(X1, X2, X3)
  , activate(n__sieve(X)) -> sieve(X)
  , activate(n__nats(X)) -> nats(X)
  , sieve(X) -> n__sieve(X)
  , sieve(cons(0(), Y)) -> cons(0(), n__sieve(activate(Y)))
  , sieve(cons(s(N), Y)) ->
    cons(s(N), n__sieve(filter(activate(Y), N, N)))
  , nats(N) -> cons(N, n__nats(s(N)))
  , nats(X) -> n__nats(X)
  , zprimes() -> sieve(nats(s(s(0())))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: filter^#(cons(X, Y), 0(), M) -> c_2(activate^#(Y))
    , 2: filter^#(cons(X, Y), s(N), M) -> c_3(activate^#(Y))
    , 3: activate^#(n__filter(X1, X2, X3)) -> c_5(filter^#(X1, X2, X3))
    , 4: activate^#(n__sieve(X)) -> c_6(sieve^#(X))
    , 5: activate^#(n__nats(X)) -> c_7(nats^#(X))
    , 6: sieve^#(cons(0(), Y)) -> c_9(activate^#(Y))
    , 7: sieve^#(cons(s(N), Y)) ->
         c_10(filter^#(activate(Y), N, N), activate^#(Y))
    , 8: zprimes^#() ->
         c_13(sieve^#(nats(s(s(0())))), nats^#(s(s(0()))))
    , 9: filter^#(X1, X2, X3) -> c_1()
    , 10: activate^#(X) -> c_4()
    , 11: sieve^#(X) -> c_8()
    , 12: nats^#(N) -> c_11()
    , 13: nats^#(X) -> c_12() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { filter^#(cons(X, Y), 0(), M) -> c_2(activate^#(Y))
  , filter^#(cons(X, Y), s(N), M) -> c_3(activate^#(Y))
  , activate^#(n__filter(X1, X2, X3)) -> c_5(filter^#(X1, X2, X3))
  , activate^#(n__sieve(X)) -> c_6(sieve^#(X))
  , sieve^#(cons(0(), Y)) -> c_9(activate^#(Y))
  , sieve^#(cons(s(N), Y)) ->
    c_10(filter^#(activate(Y), N, N), activate^#(Y))
  , zprimes^#() ->
    c_13(sieve^#(nats(s(s(0())))), nats^#(s(s(0())))) }
Weak DPs:
  { filter^#(X1, X2, X3) -> c_1()
  , activate^#(X) -> c_4()
  , activate^#(n__nats(X)) -> c_7(nats^#(X))
  , sieve^#(X) -> c_8()
  , nats^#(N) -> c_11()
  , nats^#(X) -> c_12() }
Weak Trs:
  { filter(X1, X2, X3) -> n__filter(X1, X2, X3)
  , filter(cons(X, Y), 0(), M) ->
    cons(0(), n__filter(activate(Y), M, M))
  , filter(cons(X, Y), s(N), M) ->
    cons(X, n__filter(activate(Y), N, M))
  , activate(X) -> X
  , activate(n__filter(X1, X2, X3)) -> filter(X1, X2, X3)
  , activate(n__sieve(X)) -> sieve(X)
  , activate(n__nats(X)) -> nats(X)
  , sieve(X) -> n__sieve(X)
  , sieve(cons(0(), Y)) -> cons(0(), n__sieve(activate(Y)))
  , sieve(cons(s(N), Y)) ->
    cons(s(N), n__sieve(filter(activate(Y), N, N)))
  , nats(N) -> cons(N, n__nats(s(N)))
  , nats(X) -> n__nats(X)
  , zprimes() -> sieve(nats(s(s(0())))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

{ filter^#(X1, X2, X3) -> c_1()
, activate^#(X) -> c_4()
, activate^#(n__nats(X)) -> c_7(nats^#(X))
, sieve^#(X) -> c_8()
, nats^#(N) -> c_11()
, nats^#(X) -> c_12() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { filter^#(cons(X, Y), 0(), M) -> c_2(activate^#(Y))
  , filter^#(cons(X, Y), s(N), M) -> c_3(activate^#(Y))
  , activate^#(n__filter(X1, X2, X3)) -> c_5(filter^#(X1, X2, X3))
  , activate^#(n__sieve(X)) -> c_6(sieve^#(X))
  , sieve^#(cons(0(), Y)) -> c_9(activate^#(Y))
  , sieve^#(cons(s(N), Y)) ->
    c_10(filter^#(activate(Y), N, N), activate^#(Y))
  , zprimes^#() ->
    c_13(sieve^#(nats(s(s(0())))), nats^#(s(s(0())))) }
Weak Trs:
  { filter(X1, X2, X3) -> n__filter(X1, X2, X3)
  , filter(cons(X, Y), 0(), M) ->
    cons(0(), n__filter(activate(Y), M, M))
  , filter(cons(X, Y), s(N), M) ->
    cons(X, n__filter(activate(Y), N, M))
  , activate(X) -> X
  , activate(n__filter(X1, X2, X3)) -> filter(X1, X2, X3)
  , activate(n__sieve(X)) -> sieve(X)
  , activate(n__nats(X)) -> nats(X)
  , sieve(X) -> n__sieve(X)
  , sieve(cons(0(), Y)) -> cons(0(), n__sieve(activate(Y)))
  , sieve(cons(s(N), Y)) ->
    cons(s(N), n__sieve(filter(activate(Y), N, N)))
  , nats(N) -> cons(N, n__nats(s(N)))
  , nats(X) -> n__nats(X)
  , zprimes() -> sieve(nats(s(s(0())))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  { zprimes^#() ->
    c_13(sieve^#(nats(s(s(0())))), nats^#(s(s(0())))) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { filter^#(cons(X, Y), 0(), M) -> c_1(activate^#(Y))
  , filter^#(cons(X, Y), s(N), M) -> c_2(activate^#(Y))
  , activate^#(n__filter(X1, X2, X3)) -> c_3(filter^#(X1, X2, X3))
  , activate^#(n__sieve(X)) -> c_4(sieve^#(X))
  , sieve^#(cons(0(), Y)) -> c_5(activate^#(Y))
  , sieve^#(cons(s(N), Y)) ->
    c_6(filter^#(activate(Y), N, N), activate^#(Y))
  , zprimes^#() -> c_7(sieve^#(nats(s(s(0()))))) }
Weak Trs:
  { filter(X1, X2, X3) -> n__filter(X1, X2, X3)
  , filter(cons(X, Y), 0(), M) ->
    cons(0(), n__filter(activate(Y), M, M))
  , filter(cons(X, Y), s(N), M) ->
    cons(X, n__filter(activate(Y), N, M))
  , activate(X) -> X
  , activate(n__filter(X1, X2, X3)) -> filter(X1, X2, X3)
  , activate(n__sieve(X)) -> sieve(X)
  , activate(n__nats(X)) -> nats(X)
  , sieve(X) -> n__sieve(X)
  , sieve(cons(0(), Y)) -> cons(0(), n__sieve(activate(Y)))
  , sieve(cons(s(N), Y)) ->
    cons(s(N), n__sieve(filter(activate(Y), N, N)))
  , nats(N) -> cons(N, n__nats(s(N)))
  , nats(X) -> n__nats(X)
  , zprimes() -> sieve(nats(s(s(0())))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { filter(X1, X2, X3) -> n__filter(X1, X2, X3)
    , filter(cons(X, Y), 0(), M) ->
      cons(0(), n__filter(activate(Y), M, M))
    , filter(cons(X, Y), s(N), M) ->
      cons(X, n__filter(activate(Y), N, M))
    , activate(X) -> X
    , activate(n__filter(X1, X2, X3)) -> filter(X1, X2, X3)
    , activate(n__sieve(X)) -> sieve(X)
    , activate(n__nats(X)) -> nats(X)
    , sieve(X) -> n__sieve(X)
    , sieve(cons(0(), Y)) -> cons(0(), n__sieve(activate(Y)))
    , sieve(cons(s(N), Y)) ->
      cons(s(N), n__sieve(filter(activate(Y), N, N)))
    , nats(N) -> cons(N, n__nats(s(N)))
    , nats(X) -> n__nats(X) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { filter^#(cons(X, Y), 0(), M) -> c_1(activate^#(Y))
  , filter^#(cons(X, Y), s(N), M) -> c_2(activate^#(Y))
  , activate^#(n__filter(X1, X2, X3)) -> c_3(filter^#(X1, X2, X3))
  , activate^#(n__sieve(X)) -> c_4(sieve^#(X))
  , sieve^#(cons(0(), Y)) -> c_5(activate^#(Y))
  , sieve^#(cons(s(N), Y)) ->
    c_6(filter^#(activate(Y), N, N), activate^#(Y))
  , zprimes^#() -> c_7(sieve^#(nats(s(s(0()))))) }
Weak Trs:
  { filter(X1, X2, X3) -> n__filter(X1, X2, X3)
  , filter(cons(X, Y), 0(), M) ->
    cons(0(), n__filter(activate(Y), M, M))
  , filter(cons(X, Y), s(N), M) ->
    cons(X, n__filter(activate(Y), N, M))
  , activate(X) -> X
  , activate(n__filter(X1, X2, X3)) -> filter(X1, X2, X3)
  , activate(n__sieve(X)) -> sieve(X)
  , activate(n__nats(X)) -> nats(X)
  , sieve(X) -> n__sieve(X)
  , sieve(cons(0(), Y)) -> cons(0(), n__sieve(activate(Y)))
  , sieve(cons(s(N), Y)) ->
    cons(s(N), n__sieve(filter(activate(Y), N, N)))
  , nats(N) -> cons(N, n__nats(s(N)))
  , nats(X) -> n__nats(X) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..