YES
The TRS could be proven terminating. The proof took 952 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (50ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (683ms).
| | – Problem 3 was processed with processor PolynomialLinearRange4iUR (81ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| filter#(cons(X, Y), s(N), M) | → | activate#(Y) | | activate#(n__nats(X)) | → | nats#(X) |
| sieve#(cons(s(N), Y)) | → | activate#(Y) | | activate#(n__filter(X1, X2, X3)) | → | filter#(X1, X2, X3) |
| filter#(cons(X, Y), 0, M) | → | activate#(Y) | | sieve#(cons(0, Y)) | → | activate#(Y) |
| zprimes# | → | nats#(s(s(0))) | | activate#(n__sieve(X)) | → | sieve#(X) |
| zprimes# | → | sieve#(nats(s(s(0)))) | | sieve#(cons(s(N), Y)) | → | filter#(activate(Y), N, N) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: activate, n__nats, nats, 0, s, sieve, n__filter, zprimes, filter, n__sieve, cons
Strategy
The following SCCs where found
| filter#(cons(X, Y), s(N), M) → activate#(Y) | sieve#(cons(s(N), Y)) → activate#(Y) |
| activate#(n__filter(X1, X2, X3)) → filter#(X1, X2, X3) | filter#(cons(X, Y), 0, M) → activate#(Y) |
| sieve#(cons(0, Y)) → activate#(Y) | activate#(n__sieve(X)) → sieve#(X) |
| sieve#(cons(s(N), Y)) → filter#(activate(Y), N, N) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| filter#(cons(X, Y), s(N), M) | → | activate#(Y) | | sieve#(cons(s(N), Y)) | → | activate#(Y) |
| activate#(n__filter(X1, X2, X3)) | → | filter#(X1, X2, X3) | | filter#(cons(X, Y), 0, M) | → | activate#(Y) |
| sieve#(cons(0, Y)) | → | activate#(Y) | | activate#(n__sieve(X)) | → | sieve#(X) |
| sieve#(cons(s(N), Y)) | → | filter#(activate(Y), N, N) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: activate, n__nats, nats, 0, s, sieve, n__filter, zprimes, filter, n__sieve, cons
Strategy
Polynomial Interpretation
- 0: 2
- activate(x): x
- activate#(x): x
- cons(x,y): y
- filter(x,y,z): x
- filter#(x,y,z): x
- n__filter(x,y,z): x
- n__nats(x): 0
- n__sieve(x): x + 2
- nats(x): 0
- s(x): 0
- sieve(x): x + 2
- sieve#(x): x + 1
- zprimes: 0
Improved Usable rules
| activate(n__filter(X1, X2, X3)) | → | filter(X1, X2, X3) | | filter(X1, X2, X3) | → | n__filter(X1, X2, X3) |
| activate(n__sieve(X)) | → | sieve(X) | | activate(X) | → | X |
| filter(cons(X, Y), s(N), M) | → | cons(X, n__filter(activate(Y), N, M)) | | nats(N) | → | cons(N, n__nats(s(N))) |
| sieve(cons(s(N), Y)) | → | cons(s(N), n__sieve(filter(activate(Y), N, N))) | | nats(X) | → | n__nats(X) |
| sieve(X) | → | n__sieve(X) | | activate(n__nats(X)) | → | nats(X) |
| sieve(cons(0, Y)) | → | cons(0, n__sieve(activate(Y))) | | filter(cons(X, Y), 0, M) | → | cons(0, n__filter(activate(Y), M, M)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| sieve#(cons(s(N), Y)) | → | activate#(Y) | | sieve#(cons(0, Y)) | → | activate#(Y) |
| activate#(n__sieve(X)) | → | sieve#(X) | | sieve#(cons(s(N), Y)) | → | filter#(activate(Y), N, N) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| filter#(cons(X, Y), s(N), M) | → | activate#(Y) | | activate#(n__filter(X1, X2, X3)) | → | filter#(X1, X2, X3) |
| filter#(cons(X, Y), 0, M) | → | activate#(Y) |
Rewrite 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 |
Original Signature
Termination of terms over the following signature is verified: n__nats, activate, nats, 0, sieve, s, n__filter, zprimes, n__sieve, filter, cons
Strategy
Polynomial Interpretation
- 0: 1
- activate(x): 0
- activate#(x): 2x + 1
- cons(x,y): 2y + 1
- filter(x,y,z): 0
- filter#(x,y,z): z + y + x
- n__filter(x,y,z): 3z + y + 3x
- n__nats(x): 0
- n__sieve(x): 0
- nats(x): 0
- s(x): 2x + 1
- sieve(x): 0
- zprimes: 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| filter#(cons(X, Y), s(N), M) | → | activate#(Y) | | activate#(n__filter(X1, X2, X3)) | → | filter#(X1, X2, X3) |
| filter#(cons(X, Y), 0, M) | → | activate#(Y) |