YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (100ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (124ms).
 |    | – Problem 3 was processed with processor PolynomialLinearRange4 (106ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4 (57ms).
 |    |    |    | – Problem 5 was processed with processor PolynomialLinearRange4 (137ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

T(nats(x_1)) → T(x_1)T(sieve(Y)) → sieve#(Y)
T(filter(x_1, x_2, x_3)) → T(x_3)T(filter(x_1, x_2, x_3)) → T(x_2)
zprimes# → nats#(s(s(0)))zprimes# → sieve#(nats(s(s(0))))
T(filter(x_1, x_2, x_3)) → T(x_1)T(nats(s(N))) → nats#(s(N))
T(s(x_1)) → T(x_1)T(filter(Y, M, M)) → filter#(Y, M, M)
T(filter(Y, N, M)) → filter#(Y, N, M)T(sieve(x_1)) → T(x_1)
T(filter(Y, N, N)) → filter#(Y, N, N)T(sieve(filter(Y, N, N))) → sieve#(filter(Y, N, N))

Rewrite Rules

filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(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

Context-sensitive strategy:
μ(T) = μ(0) = μ(zprimes#) = μ(zprimes) = ∅
μ(nats) = μ(sieve) = μ(s) = μ(sieve#) = μ(nats#) = μ(cons) = {1}
μ(filter#) = μ(filter) = {1, 2, 3}

The following SCCs where found

T(nats(x_1)) → T(x_1)T(filter(x_1, x_2, x_3)) → T(x_1)
T(filter(x_1, x_2, x_3)) → T(x_3)T(s(x_1)) → T(x_1)
T(sieve(x_1)) → T(x_1)T(filter(x_1, x_2, x_3)) → T(x_2)

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(nats(x_1)) → T(x_1)T(filter(x_1, x_2, x_3)) → T(x_1)
T(filter(x_1, x_2, x_3)) → T(x_3)T(s(x_1)) → T(x_1)
T(sieve(x_1)) → T(x_1)T(filter(x_1, x_2, x_3)) → T(x_2)

Rewrite Rules

filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(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

Context-sensitive strategy:
μ(T) = μ(0) = μ(zprimes#) = μ(zprimes) = ∅
μ(nats) = μ(s) = μ(sieve) = μ(sieve#) = μ(nats#) = μ(cons) = {1}
μ(filter#) = μ(filter) = {1, 2, 3}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

T(nats(x_1)) → T(x_1)

Problem 3: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(filter(x_1, x_2, x_3)) → T(x_3)T(filter(x_1, x_2, x_3)) → T(x_1)
T(s(x_1)) → T(x_1)T(sieve(x_1)) → T(x_1)
T(filter(x_1, x_2, x_3)) → T(x_2)

Rewrite Rules

filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))zprimes → sieve(nats(s(s(0))))

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(zprimes#) = μ(zprimes) = ∅
μ(nats) = μ(sieve) = μ(s) = μ(sieve#) = μ(nats#) = μ(cons) = {1}
μ(filter#) = μ(filter) = {1, 2, 3}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

T(s(x_1)) → T(x_1)

Problem 4: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(filter(x_1, x_2, x_3)) → T(x_1)T(filter(x_1, x_2, x_3)) → T(x_3)
T(sieve(x_1)) → T(x_1)T(filter(x_1, x_2, x_3)) → T(x_2)

Rewrite Rules

filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(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

Context-sensitive strategy:
μ(T) = μ(0) = μ(zprimes#) = μ(zprimes) = ∅
μ(nats) = μ(s) = μ(sieve) = μ(sieve#) = μ(nats#) = μ(cons) = {1}
μ(filter#) = μ(filter) = {1, 2, 3}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

T(filter(x_1, x_2, x_3)) → T(x_3)T(filter(x_1, x_2, x_3)) → T(x_1)
T(filter(x_1, x_2, x_3)) → T(x_2)

Problem 5: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(sieve(x_1)) → T(x_1)

Rewrite Rules

filter(cons(X, Y), 0, M) → cons(0, filter(Y, M, M))filter(cons(X, Y), s(N), M) → cons(X, filter(Y, N, M))
sieve(cons(0, Y)) → cons(0, sieve(Y))sieve(cons(s(N), Y)) → cons(s(N), sieve(filter(Y, N, N)))
nats(N) → cons(N, nats(s(N)))zprimes → sieve(nats(s(s(0))))

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(zprimes#) = μ(zprimes) = ∅
μ(nats) = μ(sieve) = μ(s) = μ(sieve#) = μ(nats#) = μ(cons) = {1}
μ(filter#) = μ(filter) = {1, 2, 3}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

T(sieve(x_1)) → T(x_1)