YES TRS: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} DP: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), mark#(0()) -> active#(0()), mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3)), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(s(X)) -> s#(mark(X)), mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(sieve(X)) -> sieve#(mark(X)), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), mark#(nats(X)) -> nats#(mark(X)), mark#(zprimes()) -> active#(zprimes()), cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2), filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3), active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), active#(filter(cons(X, Y), 0(), M)) -> cons#(0(), filter(Y, M, M)), active#(filter(cons(X, Y), 0(), M)) -> filter#(Y, M, M), active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), active#(filter(cons(X, Y), s(N), M)) -> cons#(X, filter(Y, N, M)), active#(filter(cons(X, Y), s(N), M)) -> filter#(Y, N, M), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), active#(sieve(cons(0(), Y))) -> cons#(0(), sieve(Y)), active#(sieve(cons(0(), Y))) -> sieve#(Y), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), active#(sieve(cons(s(N), Y))) -> cons#(s(N), sieve(filter(Y, N, N))), active#(sieve(cons(s(N), Y))) -> filter#(Y, N, N), active#(sieve(cons(s(N), Y))) -> sieve#(filter(Y, N, N)), active#(nats(N)) -> mark#(cons(N, nats(s(N)))), active#(nats(N)) -> cons#(N, nats(s(N))), active#(nats(N)) -> s#(N), active#(nats(N)) -> nats#(s(N)), active#(zprimes()) -> mark#(sieve(nats(s(s(0()))))), active#(zprimes()) -> s#(0()), active#(zprimes()) -> s#(s(0())), active#(zprimes()) -> sieve#(nats(s(s(0())))), active#(zprimes()) -> nats#(s(s(0()))), s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X), sieve#(mark(X)) -> sieve#(X), sieve#(active(X)) -> sieve#(X), nats#(mark(X)) -> nats#(X), nats#(active(X)) -> nats#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} EDG: { (active#(filter(cons(X, Y), s(N), M)) -> filter#(Y, N, M), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)) (active#(filter(cons(X, Y), s(N), M)) -> filter#(Y, N, M), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (active#(filter(cons(X, Y), s(N), M)) -> filter#(Y, N, M), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (active#(filter(cons(X, Y), s(N), M)) -> filter#(Y, N, M), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (active#(filter(cons(X, Y), s(N), M)) -> filter#(Y, N, M), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (active#(filter(cons(X, Y), s(N), M)) -> filter#(Y, N, M), filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3)) (filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3), filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3)) (active#(zprimes()) -> mark#(sieve(nats(s(s(0()))))), mark#(sieve(X)) -> sieve#(mark(X))) (active#(zprimes()) -> mark#(sieve(nats(s(s(0()))))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(zprimes()) -> mark#(sieve(nats(s(s(0()))))), mark#(sieve(X)) -> mark#(X)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(nats(N)) -> nats#(s(N))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(nats(N)) -> s#(N)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(nats(N)) -> cons#(N, nats(s(N)))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(s(N), Y))) -> sieve#(filter(Y, N, N))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(s(N), Y))) -> filter#(Y, N, N)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(s(N), Y))) -> cons#(s(N), sieve(filter(Y, N, N)))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N))))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(0(), Y))) -> sieve#(Y)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(0(), Y))) -> cons#(0(), sieve(Y))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y)))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(filter(cons(X, Y), s(N), M)) -> filter#(Y, N, M)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(filter(cons(X, Y), s(N), M)) -> cons#(X, filter(Y, N, M))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M)))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(filter(cons(X, Y), 0(), M)) -> filter#(Y, M, M)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(filter(cons(X, Y), 0(), M)) -> cons#(0(), filter(Y, M, M))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M)))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(nats(X)) -> nats#(mark(X))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(nats(X)) -> active#(nats(mark(X)))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(nats(X)) -> mark#(X)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(sieve(X)) -> sieve#(mark(X))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(sieve(X)) -> mark#(X)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(s(X)) -> s#(mark(X))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(s(X)) -> active#(s(mark(X)))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(s(X)) -> mark#(X)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(filter(X1, X2, X3)) -> mark#(X3)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(filter(X1, X2, X3)) -> mark#(X2)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(filter(X1, X2, X3)) -> mark#(X1)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(nats(X)) -> nats#(mark(X))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(nats(X)) -> active#(nats(mark(X)))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(nats(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(sieve(X)) -> sieve#(mark(X))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(sieve(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(s(X)) -> s#(mark(X))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(s(X)) -> active#(s(mark(X)))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(s(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(filter(X1, X2, X3)) -> mark#(X3)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(filter(X1, X2, X3)) -> mark#(X2)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(filter(X1, X2, X3)) -> mark#(X1)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sieve(cons(0(), Y))) -> sieve#(Y), sieve#(active(X)) -> sieve#(X)) (active#(sieve(cons(0(), Y))) -> sieve#(Y), sieve#(mark(X)) -> sieve#(X)) (mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3)), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)) (mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3)), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3)), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3)), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3)), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3)), filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(zprimes()) -> active#(zprimes())) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(nats(X)) -> nats#(mark(X))) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(nats(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(sieve(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(s(X)) -> s#(mark(X))) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(s(X)) -> active#(s(mark(X)))) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3))) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(filter(X1, X2, X3)) -> mark#(X3)) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(filter(X1, X2, X3)) -> mark#(X2)) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(filter(X1, X2, X3)) -> mark#(X1)) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(0()) -> active#(0())) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(zprimes()) -> active#(zprimes())) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(nats(X)) -> nats#(mark(X))) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(nats(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(sieve(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3))) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X3)) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X2)) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X1)) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(nats(X)) -> nats#(mark(X))) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(nats(X)) -> active#(nats(mark(X)))) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(nats(X)) -> mark#(X)) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(sieve(X)) -> sieve#(mark(X))) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(sieve(X)) -> mark#(X)) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(s(X)) -> s#(mark(X))) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(s(X)) -> active#(s(mark(X)))) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(s(X)) -> mark#(X)) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3))) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(filter(X1, X2, X3)) -> mark#(X3)) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(filter(X1, X2, X3)) -> mark#(X2)) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(filter(X1, X2, X3)) -> mark#(X1)) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sieve(cons(s(N), Y))) -> cons#(s(N), sieve(filter(Y, N, N))), cons#(active(X1), X2) -> cons#(X1, X2)) (active#(sieve(cons(s(N), Y))) -> cons#(s(N), sieve(filter(Y, N, N))), cons#(mark(X1), X2) -> cons#(X1, X2)) (active#(sieve(cons(s(N), Y))) -> cons#(s(N), sieve(filter(Y, N, N))), cons#(X1, active(X2)) -> cons#(X1, X2)) (active#(sieve(cons(s(N), Y))) -> cons#(s(N), sieve(filter(Y, N, N))), cons#(X1, mark(X2)) -> cons#(X1, X2)) (active#(sieve(cons(s(N), Y))) -> sieve#(filter(Y, N, N)), sieve#(active(X)) -> sieve#(X)) (active#(sieve(cons(s(N), Y))) -> sieve#(filter(Y, N, N)), sieve#(mark(X)) -> sieve#(X)) (active#(nats(N)) -> nats#(s(N)), nats#(active(X)) -> nats#(X)) (active#(nats(N)) -> nats#(s(N)), nats#(mark(X)) -> nats#(X)) (mark#(sieve(X)) -> sieve#(mark(X)), sieve#(active(X)) -> sieve#(X)) (mark#(sieve(X)) -> sieve#(mark(X)), sieve#(mark(X)) -> sieve#(X)) (active#(filter(cons(X, Y), 0(), M)) -> cons#(0(), filter(Y, M, M)), cons#(X1, active(X2)) -> cons#(X1, X2)) (active#(filter(cons(X, Y), 0(), M)) -> cons#(0(), filter(Y, M, M)), cons#(X1, mark(X2)) -> cons#(X1, X2)) (active#(nats(N)) -> cons#(N, nats(s(N))), cons#(active(X1), X2) -> cons#(X1, X2)) (active#(nats(N)) -> cons#(N, nats(s(N))), cons#(mark(X1), X2) -> cons#(X1, X2)) (active#(nats(N)) -> cons#(N, nats(s(N))), cons#(X1, active(X2)) -> cons#(X1, X2)) (active#(nats(N)) -> cons#(N, nats(s(N))), cons#(X1, mark(X2)) -> cons#(X1, X2)) (mark#(sieve(X)) -> mark#(X), mark#(zprimes()) -> active#(zprimes())) (mark#(sieve(X)) -> mark#(X), mark#(nats(X)) -> nats#(mark(X))) (mark#(sieve(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(nats(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(sieve(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3))) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X3)) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X2)) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X1)) (mark#(sieve(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(sieve(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(sieve(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(sieve(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)) (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X)) (sieve#(mark(X)) -> sieve#(X), sieve#(active(X)) -> sieve#(X)) (sieve#(mark(X)) -> sieve#(X), sieve#(mark(X)) -> sieve#(X)) (nats#(mark(X)) -> nats#(X), nats#(active(X)) -> nats#(X)) (nats#(mark(X)) -> nats#(X), nats#(mark(X)) -> nats#(X)) (nats#(active(X)) -> nats#(X), nats#(mark(X)) -> nats#(X)) (nats#(active(X)) -> nats#(X), nats#(active(X)) -> nats#(X)) (sieve#(active(X)) -> sieve#(X), sieve#(mark(X)) -> sieve#(X)) (sieve#(active(X)) -> sieve#(X), sieve#(active(X)) -> sieve#(X)) (s#(active(X)) -> s#(X), s#(mark(X)) -> s#(X)) (s#(active(X)) -> s#(X), s#(active(X)) -> s#(X)) (mark#(nats(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(nats(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(nats(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(nats(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(nats(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X1)) (mark#(nats(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X2)) (mark#(nats(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X3)) (mark#(nats(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3))) (mark#(nats(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(nats(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(nats(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(nats(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(nats(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(nats(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(nats(X)) -> mark#(X), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> mark#(X)) (mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> nats#(mark(X))) (mark#(nats(X)) -> mark#(X), mark#(zprimes()) -> active#(zprimes())) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(s(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X3)) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3))) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(nats(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(nats(X)) -> nats#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(zprimes()) -> active#(zprimes())) (active#(filter(cons(X, Y), s(N), M)) -> cons#(X, filter(Y, N, M)), cons#(X1, mark(X2)) -> cons#(X1, X2)) (active#(filter(cons(X, Y), s(N), M)) -> cons#(X, filter(Y, N, M)), cons#(X1, active(X2)) -> cons#(X1, X2)) (active#(filter(cons(X, Y), s(N), M)) -> cons#(X, filter(Y, N, M)), cons#(mark(X1), X2) -> cons#(X1, X2)) (active#(filter(cons(X, Y), s(N), M)) -> cons#(X, filter(Y, N, M)), cons#(active(X1), X2) -> cons#(X1, X2)) (mark#(nats(X)) -> nats#(mark(X)), nats#(mark(X)) -> nats#(X)) (mark#(nats(X)) -> nats#(mark(X)), nats#(active(X)) -> nats#(X)) (mark#(s(X)) -> s#(mark(X)), s#(mark(X)) -> s#(X)) (mark#(s(X)) -> s#(mark(X)), s#(active(X)) -> s#(X)) (active#(nats(N)) -> s#(N), s#(mark(X)) -> s#(X)) (active#(nats(N)) -> s#(N), s#(active(X)) -> s#(X)) (active#(sieve(cons(s(N), Y))) -> filter#(Y, N, N), filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3)) (active#(sieve(cons(s(N), Y))) -> filter#(Y, N, N), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (active#(sieve(cons(s(N), Y))) -> filter#(Y, N, N), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (active#(sieve(cons(s(N), Y))) -> filter#(Y, N, N), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (active#(sieve(cons(s(N), Y))) -> filter#(Y, N, N), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (active#(sieve(cons(s(N), Y))) -> filter#(Y, N, N), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(filter(X1, X2, X3)) -> mark#(X1)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(filter(X1, X2, X3)) -> mark#(X2)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(filter(X1, X2, X3)) -> mark#(X3)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3))) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(s(X)) -> mark#(X)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(s(X)) -> active#(s(mark(X)))) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(s(X)) -> s#(mark(X))) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(sieve(X)) -> mark#(X)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(sieve(X)) -> sieve#(mark(X))) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(nats(X)) -> mark#(X)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(nats(X)) -> active#(nats(mark(X)))) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(nats(X)) -> nats#(mark(X))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M)))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(filter(cons(X, Y), 0(), M)) -> cons#(0(), filter(Y, M, M))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(filter(cons(X, Y), 0(), M)) -> filter#(Y, M, M)) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M)))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(filter(cons(X, Y), s(N), M)) -> cons#(X, filter(Y, N, M))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(filter(cons(X, Y), s(N), M)) -> filter#(Y, N, M)) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y)))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(sieve(cons(0(), Y))) -> cons#(0(), sieve(Y))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(sieve(cons(0(), Y))) -> sieve#(Y)) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N))))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(sieve(cons(s(N), Y))) -> cons#(s(N), sieve(filter(Y, N, N)))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(sieve(cons(s(N), Y))) -> filter#(Y, N, N)) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(sieve(cons(s(N), Y))) -> sieve#(filter(Y, N, N))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(nats(N)) -> cons#(N, nats(s(N)))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(nats(N)) -> s#(N)) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(nats(N)) -> nats#(s(N))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X3)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats(X)) -> nats#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(zprimes()) -> active#(zprimes())) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M)))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(filter(cons(X, Y), 0(), M)) -> cons#(0(), filter(Y, M, M))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(filter(cons(X, Y), 0(), M)) -> filter#(Y, M, M)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M)))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(filter(cons(X, Y), s(N), M)) -> cons#(X, filter(Y, N, M))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(filter(cons(X, Y), s(N), M)) -> filter#(Y, N, M)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y)))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sieve(cons(0(), Y))) -> cons#(0(), sieve(Y))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sieve(cons(0(), Y))) -> sieve#(Y)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N))))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sieve(cons(s(N), Y))) -> cons#(s(N), sieve(filter(Y, N, N)))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sieve(cons(s(N), Y))) -> filter#(Y, N, N)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sieve(cons(s(N), Y))) -> sieve#(filter(Y, N, N))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(nats(N)) -> mark#(cons(N, nats(s(N))))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(nats(N)) -> cons#(N, nats(s(N)))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(nats(N)) -> s#(N)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(nats(N)) -> nats#(s(N))) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(0()) -> active#(0())) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(filter(X1, X2, X3)) -> mark#(X1)) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(filter(X1, X2, X3)) -> mark#(X2)) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(filter(X1, X2, X3)) -> mark#(X3)) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3))) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(s(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(s(X)) -> active#(s(mark(X)))) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(s(X)) -> s#(mark(X))) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(sieve(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(nats(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(nats(X)) -> nats#(mark(X))) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(zprimes()) -> active#(zprimes())) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(filter(X1, X2, X3)) -> mark#(X1)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(filter(X1, X2, X3)) -> mark#(X2)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(filter(X1, X2, X3)) -> mark#(X3)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(filter(X1, X2, X3)) -> filter#(mark(X1), mark(X2), mark(X3))) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(s(X)) -> mark#(X)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(s(X)) -> active#(s(mark(X)))) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(s(X)) -> s#(mark(X))) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(sieve(X)) -> mark#(X)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(sieve(X)) -> sieve#(mark(X))) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(nats(X)) -> mark#(X)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(nats(X)) -> active#(nats(mark(X)))) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(nats(X)) -> nats#(mark(X))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M)))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(filter(cons(X, Y), 0(), M)) -> cons#(0(), filter(Y, M, M))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(filter(cons(X, Y), 0(), M)) -> filter#(Y, M, M)) (mark#(nats(X)) -> active#(nats(mark(X))), active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M)))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(filter(cons(X, Y), s(N), M)) -> cons#(X, filter(Y, N, M))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(filter(cons(X, Y), s(N), M)) -> filter#(Y, N, M)) (mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y)))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(0(), Y))) -> cons#(0(), sieve(Y))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(0(), Y))) -> sieve#(Y)) (mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N))))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(s(N), Y))) -> cons#(s(N), sieve(filter(Y, N, N)))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(s(N), Y))) -> filter#(Y, N, N)) (mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(s(N), Y))) -> sieve#(filter(Y, N, N))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(nats(N)) -> cons#(N, nats(s(N)))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(nats(N)) -> s#(N)) (mark#(nats(X)) -> active#(nats(mark(X))), active#(nats(N)) -> nats#(s(N))) (mark#(s(X)) -> active#(s(mark(X))), active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M)))) (mark#(s(X)) -> active#(s(mark(X))), active#(filter(cons(X, Y), 0(), M)) -> cons#(0(), filter(Y, M, M))) (mark#(s(X)) -> active#(s(mark(X))), active#(filter(cons(X, Y), 0(), M)) -> filter#(Y, M, M)) (mark#(s(X)) -> active#(s(mark(X))), active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M)))) (mark#(s(X)) -> active#(s(mark(X))), active#(filter(cons(X, Y), s(N), M)) -> cons#(X, filter(Y, N, M))) (mark#(s(X)) -> active#(s(mark(X))), active#(filter(cons(X, Y), s(N), M)) -> filter#(Y, N, M)) (mark#(s(X)) -> active#(s(mark(X))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y)))) (mark#(s(X)) -> active#(s(mark(X))), active#(sieve(cons(0(), Y))) -> cons#(0(), sieve(Y))) (mark#(s(X)) -> active#(s(mark(X))), active#(sieve(cons(0(), Y))) -> sieve#(Y)) (mark#(s(X)) -> active#(s(mark(X))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N))))) (mark#(s(X)) -> active#(s(mark(X))), active#(sieve(cons(s(N), Y))) -> cons#(s(N), sieve(filter(Y, N, N)))) (mark#(s(X)) -> active#(s(mark(X))), active#(sieve(cons(s(N), Y))) -> filter#(Y, N, N)) (mark#(s(X)) -> active#(s(mark(X))), active#(sieve(cons(s(N), Y))) -> sieve#(filter(Y, N, N))) (mark#(s(X)) -> active#(s(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))) (mark#(s(X)) -> active#(s(mark(X))), active#(nats(N)) -> cons#(N, nats(s(N)))) (mark#(s(X)) -> active#(s(mark(X))), active#(nats(N)) -> s#(N)) (mark#(s(X)) -> active#(s(mark(X))), active#(nats(N)) -> nats#(s(N))) (filter#(active(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3)) (filter#(active(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (filter#(active(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(active(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(active(X1), X2, X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(active(X1), X2, X3) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3)) (filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)) (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(active(X1), X2) -> cons#(X1, X2)) (mark#(zprimes()) -> active#(zprimes()), active#(zprimes()) -> mark#(sieve(nats(s(s(0())))))) (mark#(zprimes()) -> active#(zprimes()), active#(zprimes()) -> s#(0())) (mark#(zprimes()) -> active#(zprimes()), active#(zprimes()) -> s#(s(0()))) (mark#(zprimes()) -> active#(zprimes()), active#(zprimes()) -> sieve#(nats(s(s(0()))))) (mark#(zprimes()) -> active#(zprimes()), active#(zprimes()) -> nats#(s(s(0())))) (active#(sieve(cons(0(), Y))) -> cons#(0(), sieve(Y)), cons#(X1, mark(X2)) -> cons#(X1, X2)) (active#(sieve(cons(0(), Y))) -> cons#(0(), sieve(Y)), cons#(X1, active(X2)) -> cons#(X1, X2)) (active#(filter(cons(X, Y), 0(), M)) -> filter#(Y, M, M), filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3)) (active#(filter(cons(X, Y), 0(), M)) -> filter#(Y, M, M), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (active#(filter(cons(X, Y), 0(), M)) -> filter#(Y, M, M), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (active#(filter(cons(X, Y), 0(), M)) -> filter#(Y, M, M), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (active#(filter(cons(X, Y), 0(), M)) -> filter#(Y, M, M), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (active#(filter(cons(X, Y), 0(), M)) -> filter#(Y, M, M), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)) } SCCS: Scc: { nats#(mark(X)) -> nats#(X), nats#(active(X)) -> nats#(X)} Scc: { sieve#(mark(X)) -> sieve#(X), sieve#(active(X)) -> sieve#(X)} Scc: { s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)} Scc: { filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)} Scc: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)} Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), mark#(zprimes()) -> active#(zprimes()), active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), active#(nats(N)) -> mark#(cons(N, nats(s(N)))), active#(zprimes()) -> mark#(sieve(nats(s(s(0())))))} SCC: Strict: { nats#(mark(X)) -> nats#(X), nats#(active(X)) -> nats#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(nats#) = 0 Strict: {nats#(active(X)) -> nats#(X)} EDG: {(nats#(active(X)) -> nats#(X), nats#(active(X)) -> nats#(X))} SCCS: Scc: {nats#(active(X)) -> nats#(X)} SCC: Strict: {nats#(active(X)) -> nats#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(nats#) = 0 Strict: {} Qed SCC: Strict: { sieve#(mark(X)) -> sieve#(X), sieve#(active(X)) -> sieve#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(sieve#) = 0 Strict: {sieve#(active(X)) -> sieve#(X)} EDG: {(sieve#(active(X)) -> sieve#(X), sieve#(active(X)) -> sieve#(X))} SCCS: Scc: {sieve#(active(X)) -> sieve#(X)} SCC: Strict: {sieve#(active(X)) -> sieve#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(sieve#) = 0 Strict: {} Qed SCC: Strict: { s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(s#) = 0 Strict: {s#(active(X)) -> s#(X)} EDG: {(s#(active(X)) -> s#(X), s#(active(X)) -> s#(X))} SCCS: Scc: {s#(active(X)) -> s#(X)} SCC: Strict: {s#(active(X)) -> s#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(s#) = 0 Strict: {} Qed SCC: Strict: { filter#(X1, X2, mark(X3)) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(filter#) = 2 Strict: {filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)} EDG: {(filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (filter#(active(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (filter#(active(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(active(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(active(X1), X2, X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(active(X1), X2, X3) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3))} SCCS: Scc: {filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)} SCC: Strict: {filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(active(X1), X2, X3) -> filter#(X1, X2, X3)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(filter#) = 0 Strict: {filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)} EDG: {(filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3)) (filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3))} SCCS: Scc: {filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)} SCC: Strict: {filter#(X1, X2, active(X3)) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(filter#) = 2 Strict: { filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)} EDG: {(filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3))} SCCS: Scc: { filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)} SCC: Strict: { filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(mark(X1), X2, X3) -> filter#(X1, X2, X3)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(filter#) = 0 Strict: { filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)} EDG: {(filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3)) (filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3))} SCCS: Scc: { filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)} SCC: Strict: { filter#(X1, mark(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(filter#) = 1 Strict: {filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)} EDG: {(filter#(X1, active(X2), X3) -> filter#(X1, X2, X3), filter#(X1, active(X2), X3) -> filter#(X1, X2, X3))} SCCS: Scc: {filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)} SCC: Strict: {filter#(X1, active(X2), X3) -> filter#(X1, X2, X3)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(filter#) = 1 Strict: {} Qed SCC: Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(cons#) = 0 Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)} EDG: {(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))} SCCS: Scc: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)} SCC: Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(cons#) = 0 Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)} EDG: {(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))} SCCS: Scc: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)} SCC: Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(cons#) = 1 Strict: {cons#(X1, active(X2)) -> cons#(X1, X2)} EDG: {(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))} SCCS: Scc: {cons#(X1, active(X2)) -> cons#(X1, X2)} SCC: Strict: {cons#(X1, active(X2)) -> cons#(X1, X2)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(cons#) = 1 Strict: {} Qed SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), mark#(zprimes()) -> active#(zprimes()), active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), active#(nats(N)) -> mark#(cons(N, nats(s(N)))), active#(zprimes()) -> mark#(sieve(nats(s(s(0())))))} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} POLY: Argument Filtering: pi(zprimes) = [], pi(nats) = [], pi(sieve) = [], pi(s) = [], pi(active#) = 0, pi(active) = [], pi(filter) = [], pi(0) = [], pi(cons) = [], pi(mark#) = [], pi(mark) = [] Usable Rules: {} Interpretation: [mark#] = 1, [filter] = 1, [cons] = 0, [nats] = 1, [sieve] = 1, [s] = 0, [zprimes] = 1 Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), mark#(zprimes()) -> active#(zprimes()), active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), active#(nats(N)) -> mark#(cons(N, nats(s(N)))), active#(zprimes()) -> mark#(sieve(nats(s(s(0())))))} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} EDG: { (mark#(zprimes()) -> active#(zprimes()), active#(zprimes()) -> mark#(sieve(nats(s(s(0())))))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(nats(X)) -> active#(nats(mark(X)))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(nats(X)) -> mark#(X)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(sieve(X)) -> mark#(X)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(s(X)) -> mark#(X)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(filter(X1, X2, X3)) -> mark#(X3)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(filter(X1, X2, X3)) -> mark#(X2)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(filter(X1, X2, X3)) -> mark#(X1)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(nats(X)) -> active#(nats(mark(X)))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(nats(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(sieve(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(s(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(filter(X1, X2, X3)) -> mark#(X3)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(filter(X1, X2, X3)) -> mark#(X2)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(filter(X1, X2, X3)) -> mark#(X1)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(zprimes()) -> active#(zprimes())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X3)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(zprimes()) -> active#(zprimes())) (mark#(s(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(nats(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X3)) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(nats(X)) -> mark#(X), mark#(zprimes()) -> active#(zprimes())) (mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> mark#(X)) (mark#(nats(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(nats(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(nats(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(nats(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(nats(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X3)) (mark#(nats(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X2)) (mark#(nats(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X1)) (mark#(nats(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N))))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y)))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M)))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M)))) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(nats(X)) -> active#(nats(mark(X)))) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(nats(X)) -> mark#(X)) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(sieve(X)) -> mark#(X)) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(s(X)) -> mark#(X)) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(filter(X1, X2, X3)) -> mark#(X3)) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(filter(X1, X2, X3)) -> mark#(X2)) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(filter(X1, X2, X3)) -> mark#(X1)) (active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(filter(X1, X2, X3)) -> mark#(X1)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(filter(X1, X2, X3)) -> mark#(X2)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(filter(X1, X2, X3)) -> mark#(X3)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(s(X)) -> mark#(X)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(sieve(X)) -> mark#(X)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(nats(X)) -> mark#(X)) (active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M)))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M)))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y)))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N))))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))) (active#(zprimes()) -> mark#(sieve(nats(s(s(0()))))), mark#(sieve(X)) -> mark#(X)) (active#(zprimes()) -> mark#(sieve(nats(s(s(0()))))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X1)) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X2)) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> mark#(X3)) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(sieve(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(nats(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(zprimes()) -> active#(zprimes())) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X1)) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X2)) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X3)) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(sieve(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(nats(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(zprimes()) -> active#(zprimes())) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(filter(X1, X2, X3)) -> mark#(X1)) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(filter(X1, X2, X3)) -> mark#(X2)) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(filter(X1, X2, X3)) -> mark#(X3)) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(sieve(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(nats(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(zprimes()) -> active#(zprimes())) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(filter(X1, X2, X3)) -> mark#(X1)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(filter(X1, X2, X3)) -> mark#(X2)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(filter(X1, X2, X3)) -> mark#(X3)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(s(X)) -> mark#(X)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(sieve(X)) -> mark#(X)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(nats(X)) -> mark#(X)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(filter(X1, X2, X3)) -> mark#(X1)) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(filter(X1, X2, X3)) -> mark#(X2)) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(filter(X1, X2, X3)) -> mark#(X3)) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(s(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(sieve(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(nats(X)) -> mark#(X)) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(zprimes()) -> active#(zprimes())) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M)))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M)))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y)))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N))))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))) } SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), mark#(zprimes()) -> active#(zprimes()), active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), active#(nats(N)) -> mark#(cons(N, nats(s(N)))), active#(zprimes()) -> mark#(sieve(nats(s(s(0())))))} SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> mark#(X2), mark#(filter(X1, X2, X3)) -> mark#(X3), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), mark#(zprimes()) -> active#(zprimes()), active#(filter(cons(X, Y), 0(), M)) -> mark#(cons(0(), filter(Y, M, M))), active#(filter(cons(X, Y), s(N), M)) -> mark#(cons(X, filter(Y, N, M))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), active#(nats(N)) -> mark#(cons(N, nats(s(N)))), active#(zprimes()) -> mark#(sieve(nats(s(s(0())))))} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} POLY: Argument Filtering: pi(zprimes) = [], pi(nats) = 0, pi(sieve) = 0, pi(s) = 0, pi(active#) = [0], pi(active) = 0, pi(filter) = [0,1,2], pi(0) = [], pi(cons) = 0, pi(mark#) = [0], pi(mark) = 0 Usable Rules: {} Interpretation: [active#](x0) = x0 + 1, [mark#](x0) = x0 + 1, [filter](x0, x1, x2) = x0 + x1 + x2 + 1, [zprimes] = 1, [0] = 0 Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), mark#(zprimes()) -> active#(zprimes()), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} EDG: {(mark#(s(X)) -> mark#(X), mark#(zprimes()) -> active#(zprimes())) (mark#(s(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(nats(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N))))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y)))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N))))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y)))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(nats(X)) -> active#(nats(mark(X)))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(nats(X)) -> mark#(X)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(sieve(X)) -> mark#(X)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(s(X)) -> mark#(X)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(nats(X)) -> active#(nats(mark(X)))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(nats(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(sieve(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(s(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(s(X)) -> mark#(X)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(sieve(X)) -> mark#(X)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(nats(X)) -> mark#(X)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(zprimes()) -> active#(zprimes())) (mark#(nats(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(nats(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(nats(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(nats(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(nats(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> mark#(X)) (mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(nats(X)) -> mark#(X), mark#(zprimes()) -> active#(zprimes())) (mark#(sieve(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3)))) (mark#(sieve(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(nats(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(zprimes()) -> active#(zprimes())) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y)))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N))))) (mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), active#(nats(N)) -> mark#(cons(N, nats(s(N)))))} SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))} SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2, X3)) -> active#(filter(mark(X1), mark(X2), mark(X3))), mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} POLY: Argument Filtering: pi(zprimes) = [], pi(nats) = [], pi(sieve) = [], pi(s) = [], pi(active#) = 0, pi(active) = [], pi(filter) = [], pi(0) = [], pi(cons) = [], pi(mark#) = [], pi(mark) = [] Usable Rules: {} Interpretation: [mark#] = 1, [filter] = 0, [nats] = 1, [sieve] = 1 Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} EDG: {(mark#(sieve(X)) -> active#(sieve(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N))))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y)))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(nats(X)) -> active#(nats(mark(X)))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(nats(X)) -> mark#(X)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(sieve(X)) -> mark#(X)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(s(X)) -> mark#(X)) (active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(nats(X)) -> active#(nats(mark(X)))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(nats(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(sieve(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(s(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sieve(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(nats(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(nats(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(nats(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(nats(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(nats(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> mark#(X)) (mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(nats(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X)))) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(s(X)) -> mark#(X)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(sieve(X)) -> mark#(X)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(nats(X)) -> mark#(X)) (active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y)))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N))))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats(X)) -> active#(nats(mark(X))))} SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))} SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), active#(sieve(cons(0(), Y))) -> mark#(cons(0(), sieve(Y))), active#(sieve(cons(s(N), Y))) -> mark#(cons(s(N), sieve(filter(Y, N, N)))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} POLY: Argument Filtering: pi(zprimes) = [], pi(nats) = 0, pi(sieve) = [0], pi(s) = 0, pi(active#) = 0, pi(active) = 0, pi(filter) = 0, pi(0) = [], pi(cons) = 0, pi(mark#) = 0, pi(mark) = 0 Usable Rules: {} Interpretation: [sieve](x0) = x0 + 1, [0] = 0 Strict: {mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} EDG: {(mark#(sieve(X)) -> active#(sieve(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))) (mark#(s(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(nats(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(nats(X)) -> active#(nats(mark(X)))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(nats(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(s(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(nats(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(nats(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(nats(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> mark#(X)) (mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(nats(X)) -> active#(nats(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats(X)) -> active#(nats(mark(X))))} SCCS: Scc: {mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))} SCC: Strict: {mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} POLY: Argument Filtering: pi(zprimes) = [], pi(nats) = [], pi(sieve) = [], pi(s) = [], pi(active#) = 0, pi(active) = [], pi(filter) = [], pi(0) = [], pi(cons) = [], pi(mark#) = [], pi(mark) = [] Usable Rules: {} Interpretation: [mark#] = 1, [nats] = 1, [sieve] = 0 Strict: {mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} EDG: {(mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> mark#(X)) (mark#(nats(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(nats(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(nats(X)) -> active#(nats(mark(X)))) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(nats(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(s(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(nats(X)) -> active#(nats(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(nats(X)) -> active#(nats(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(nats(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))))} SCCS: Scc: {mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))} SCC: Strict: {mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(nats(X)) -> mark#(X), mark#(nats(X)) -> active#(nats(mark(X))), active#(nats(N)) -> mark#(cons(N, nats(s(N))))} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} POLY: Argument Filtering: pi(zprimes) = [], pi(nats) = [0], pi(sieve) = 0, pi(s) = 0, pi(active#) = 0, pi(active) = 0, pi(filter) = [0,2], pi(0) = [], pi(cons) = 0, pi(mark#) = [0], pi(mark) = 0 Usable Rules: {} Interpretation: [mark#](x0) = x0 + 1, [nats](x0) = x0 + 1 Strict: {mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), active#(nats(N)) -> mark#(cons(N, nats(s(N))))} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} EDG: {(active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(s(X)) -> mark#(X)) (active#(nats(N)) -> mark#(cons(N, nats(s(N)))), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))} SCCS: Scc: {mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)} SCC: Strict: {mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(mark#) = 0 Strict: {mark#(s(X)) -> mark#(X)} EDG: {(mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))} SCCS: Scc: {mark#(s(X)) -> mark#(X)} SCC: Strict: {mark#(s(X)) -> mark#(X)} Weak: { mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(0()) -> active(0()), mark(filter(X1, X2, X3)) -> active(filter(mark(X1), mark(X2), mark(X3))), mark(s(X)) -> active(s(mark(X))), mark(sieve(X)) -> active(sieve(mark(X))), mark(nats(X)) -> active(nats(mark(X))), mark(zprimes()) -> active(zprimes()), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), filter(X1, X2, mark(X3)) -> filter(X1, X2, X3), filter(X1, X2, active(X3)) -> filter(X1, X2, X3), filter(X1, mark(X2), X3) -> filter(X1, X2, X3), filter(X1, active(X2), X3) -> filter(X1, X2, X3), filter(mark(X1), X2, X3) -> filter(X1, X2, X3), filter(active(X1), X2, X3) -> filter(X1, X2, X3), active(filter(cons(X, Y), 0(), M)) -> mark(cons(0(), filter(Y, M, M))), active(filter(cons(X, Y), s(N), M)) -> mark(cons(X, filter(Y, N, M))), active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y))), active(sieve(cons(s(N), Y))) -> mark(cons(s(N), sieve(filter(Y, N, N)))), active(nats(N)) -> mark(cons(N, nats(s(N)))), active(zprimes()) -> mark(sieve(nats(s(s(0()))))), s(mark(X)) -> s(X), s(active(X)) -> s(X), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), nats(mark(X)) -> nats(X), nats(active(X)) -> nats(X)} SPSC: Simple Projection: pi(mark#) = 0 Strict: {} Qed