TRS: { filter(cons(X), 0(), M) -> cons(0()), filter(cons(X), s(N), M) -> cons(X), sieve(cons(0())) -> cons(0()), sieve(cons(s(N))) -> cons(s(N)), nats(N) -> cons(N), zprimes() -> sieve(nats(s(s(0()))))} POP*: Quasi-Precedence: nats > cons, filter > cons, zprimes > nats, zprimes > sieve, zprimes > s, zprimes > 0 empty Normal: pi(nats) = [1], pi(sieve) = [1], pi(filter) = [1,2,3] Safe: pi(s) = [1], pi(cons) = [1] Predicative System: { filter(cons(;X),0(),M;) -> cons(;0()), filter(cons(;X),s(;N),M;) -> cons(;X), sieve(cons(;0());) -> cons(;0()), sieve(cons(;s(;N));) -> cons(;s(;N)), nats(N;) -> cons(;N), zprimes() -> sieve(nats(s(;s(;0())););)} Qed