YES
(VAR X Y M N X1 X2 X3)
(RULES 
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
)

Proving termination of rewriting for Ex9_BLR02_Z:

-> Dependency pairs:
nF_filter(cons(X,Y),0,M) -> nF_activate(Y)
nF_filter(cons(X,Y),s(N),M) -> nF_activate(Y)
nF_sieve(cons(0,Y)) -> nF_activate(Y)
nF_sieve(cons(s(N),Y)) -> nF_filter(activate(Y),N,N)
nF_sieve(cons(s(N),Y)) -> nF_activate(Y)
nF_zprimes -> nF_sieve(nats(s(s(0))))
nF_zprimes -> nF_nats(s(s(0)))
nF_activate(n__filter(X1,X2,X3)) -> nF_filter(X1,X2,X3)
nF_activate(n__sieve(X)) -> nF_sieve(X)
nF_activate(n__nats(X)) -> nF_nats(X)

-> Proof of termination for Ex9_BLR02_Z_1:
-> -> Dependency pairs in cycle:
nF_filter(cons(X,Y),0,M) -> nF_activate(Y)
nF_activate(n__filter(X1,X2,X3)) -> nF_filter(X1,X2,X3)
nF_sieve(cons(s(N),Y)) -> nF_activate(Y)
nF_activate(n__sieve(X)) -> nF_sieve(X)
nF_sieve(cons(0,Y)) -> nF_activate(Y)
nF_filter(cons(X,Y),s(N),M) -> nF_activate(Y)
nF_sieve(cons(s(N),Y)) -> nF_filter(activate(Y),N,N)

UsableRules:
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)))
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

Polynomial Interpretation:

[filter](X1,X2,X3) = X1
[cons](X1,X2) = X2
[0] = 0
[n__filter](X1,X2,X3) = X1
[activate](X) = X
[s](X) = 0
[sieve](X) = X + 1
[n__sieve](X) = X + 1
[nats](X) = 0
[n__nats](X) = 0
[zprimes] = 0
[nF_filter](X1,X2,X3) = X1
[nF_activate](X) = X
[nF_sieve](X) = X + 1

TIME: 0.251749

-> -> Dependency pairs in cycle:
nF_filter(cons(X,Y),0,M) -> nF_activate(Y)
nF_activate(n__filter(X1,X2,X3)) -> nF_filter(X1,X2,X3)
nF_filter(cons(X,Y),s(N),M) -> nF_activate(Y)
nF_sieve(cons(0,Y)) -> nF_activate(Y)
nF_activate(n__sieve(X)) -> nF_sieve(X)
nF_sieve(cons(s(N),Y)) -> nF_activate(Y)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.