MAYBE

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

Strict Trs:
  { filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M))
  , filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M))
  , sieve(cons(0(), Y)) -> cons(0(), sieve(Y))
  , sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N)))
  , nats(N) -> cons(N, nats(s(N)))
  , zprimes() -> sieve(nats(s(s(0())))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { filter^#(cons(X, Y), 0(), M) -> c_1(filter^#(Y, M, M))
  , filter^#(cons(X, Y), s(N), M) -> c_2(filter^#(Y, N, M))
  , sieve^#(cons(0(), Y)) -> c_3(sieve^#(Y))
  , sieve^#(cons(s(N), Y)) ->
    c_4(sieve^#(filter(Y, N, N)), filter^#(Y, N, N))
  , nats^#(N) -> c_5(nats^#(s(N)))
  , zprimes^#() -> c_6(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^#(cons(X, Y), 0(), M) -> c_1(filter^#(Y, M, M))
  , filter^#(cons(X, Y), s(N), M) -> c_2(filter^#(Y, N, M))
  , sieve^#(cons(0(), Y)) -> c_3(sieve^#(Y))
  , sieve^#(cons(s(N), Y)) ->
    c_4(sieve^#(filter(Y, N, N)), filter^#(Y, N, N))
  , nats^#(N) -> c_5(nats^#(s(N)))
  , zprimes^#() -> c_6(sieve^#(nats(s(s(0())))), nats^#(s(s(0())))) }
Weak Trs:
  { filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M))
  , filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M))
  , sieve(cons(0(), Y)) -> cons(0(), sieve(Y))
  , sieve(cons(s(N), Y)) -> cons(s(N), sieve(filter(Y, N, N)))
  , nats(N) -> cons(N, nats(s(N)))
  , zprimes() -> sieve(nats(s(s(0())))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { filter(cons(X, Y), 0(), M) -> cons(0(), filter(Y, M, M))
    , filter(cons(X, Y), s(N), M) -> cons(X, filter(Y, N, M))
    , nats(N) -> cons(N, nats(s(N))) }

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

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

The input cannot be shown compatible

Arrrr..