YES O(n) 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())))) } DUP: We consider a non-duplicating system. 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())))) } BOUND: Automaton: { zprimes_0() -> 7, nats_1(7) -> 8, nats_0(7) -> 7, sieve_1(8) -> 7, sieve_0(7) -> 7, s_2(7) -> 9, s_1(7) -> 7, s_0(7) -> 7, filter_0(7, 7, 7) -> 7, 0_2() -> 9, 0_1() -> 7, 0_0() -> 7, cons_2(9) -> 7, cons_2(7) -> 8, cons_1(9) -> 7, cons_1(7) -> 7, cons_0(7) -> 7 } Strict: {} Qed