YES 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())))) max/plus interpretations on N: filter_A(x1,x2,x3) = max{5, 4 + x1, 5 + x2, 5 + x3} filter#_A(x1,x2,x3) = max{5, 4 + x1, 5 + x2, 5 + x3} cons_A(x1) = max{4, 1 + x1} cons#_A(x1) = max{4, 1 + x1} 0_A = 2 0#_A = 2 s_A(x1) = max{0, x1} s#_A(x1) = max{0, x1} sieve_A(x1) = max{1, x1} sieve#_A(x1) = max{1, x1} nats_A(x1) = max{5, 5 + x1} nats#_A(x1) = max{5, 5 + x1} zprimes_A = 8 zprimes#_A = 8 precedence: filter > cons = zprimes > sieve = nats > 0 = s