YES

The TRS could be proven terminating. The proof took 21 ms.

The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (3ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

zprimes^#

→

nats^#(s(s(0)))

zprimes^#

→

sieve^#(nats(s(s(0))))

Rewrite Rules

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

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, sieve, zprimes, filter, cons

Strategy

There are no SCCs!