YES TRS: filter(cons(X,Y),0(),M) -> cons(0(),n__filter(activate(Y),M,M)) filter(cons(X,Y),s(N),M) -> cons(X,n__filter(activate(Y),N,M)) sieve(cons(0(),Y)) -> cons(0(),n__sieve(activate(Y))) sieve(cons(s(N),Y)) -> cons(s(N),n__sieve(filter(activate(Y),N,N))) nats(N) -> cons(N,n__nats(s(N))) zprimes() -> sieve(nats(s(s(0())))) filter(X1,X2,X3) -> n__filter(X1,X2,X3) sieve(X) -> n__sieve(X) nats(X) -> n__nats(X) activate(n__filter(X1,X2,X3)) -> filter(X1,X2,X3) activate(n__sieve(X)) -> sieve(X) activate(n__nats(X)) -> nats(X) activate(X) -> X max/plus interpretations on N: filter_A(x1,x2,x3) = max{31, x1, 6, 8} filter#_A(x1,x2,x3) = max{34, 4 + x1, 6, -1} cons_A(x1,x2) = max{28, -1 + x1, 7 + x2} cons#_A(x1,x2) = max{8, 1 + x1, 23} 0_A = 32 0#_A = 21 n__filter_A(x1,x2,x3) = max{22, -7 + x1, 6, 23} n__filter#_A(x1,x2,x3) = max{33, 5, 5, 5} activate_A(x1) = max{31, 7 + x1} activate#_A(x1) = max{0, 11 + x1} s_A(x1) = max{49, 6} s#_A(x1) = max{0, -1} sieve_A(x1) = max{27, 19 + x1} sieve#_A(x1) = max{22, 13 + x1} n__sieve_A(x1) = max{1, 12 + x1} n__sieve#_A(x1) = max{21, 17} nats_A(x1) = max{50, 1 + x1} nats#_A(x1) = max{24, 1 + x1} n__nats_A(x1) = max{43, -6 + x1} n__nats#_A(x1) = max{0, -49 + x1} zprimes_A = 69 zprimes#_A = 64 precedence: zprimes > sieve > filter = activate > n__filter = nats > s = n__nats > cons > 0 = n__sieve