TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60002 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (2075ms).
| – Problem 2 was processed with processor SubtermCriterion (2ms).
| | – Problem 8 remains open; application of the following processors failed [DependencyGraph (12ms), PolynomialLinearRange4iUR (24ms), DependencyGraph (8ms), PolynomialLinearRange8NegiUR (5ms), DependencyGraph (7ms)].
| – Problem 3 was processed with processor SubtermCriterion (4ms).
| – Problem 4 was processed with processor SubtermCriterion (2ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| – Problem 6 was processed with processor SubtermCriterion (1ms).
| | – Problem 9 remains open; application of the following processors failed [DependencyGraph (3ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (21ms), DependencyGraph (3ms)].
| – Problem 7 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (277ms), PolynomialLinearRange4iUR (3333ms), DependencyGraph (216ms), PolynomialLinearRange8NegiUR (10000ms), DependencyGraph (202ms), ReductionPairSAT (timeout)].
The following open problems remain:
Open Dependency Pair Problem 7
Dependency Pairs
| mark#(filter(X1, X2, X3)) | → | mark#(X3) | | mark#(0) | → | active#(0) |
| mark#(cons(X1, X2)) | → | active#(cons(mark(X1), X2)) | | mark#(s(X)) | → | active#(s(mark(X))) |
| active#(filter(cons(X, Y), 0, M)) | → | mark#(cons(0, filter(Y, M, M))) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| active#(sieve(cons(0, Y))) | → | mark#(cons(0, sieve(Y))) | | active#(filter(cons(X, Y), s(N), M)) | → | mark#(cons(X, filter(Y, N, M))) |
| active#(sieve(cons(s(N), Y))) | → | mark#(cons(s(N), sieve(filter(Y, N, N)))) | | mark#(nats(X)) | → | active#(nats(mark(X))) |
| active#(nats(N)) | → | mark#(cons(N, nats(s(N)))) | | mark#(zprimes) | → | active#(zprimes) |
| mark#(filter(X1, X2, X3)) | → | active#(filter(mark(X1), mark(X2), mark(X3))) | | mark#(filter(X1, X2, X3)) | → | mark#(X2) |
| mark#(filter(X1, X2, X3)) | → | mark#(X1) | | mark#(nats(X)) | → | mark#(X) |
| mark#(s(X)) | → | mark#(X) | | mark#(sieve(X)) | → | active#(sieve(mark(X))) |
| active#(zprimes) | → | mark#(sieve(nats(s(s(0))))) | | mark#(sieve(X)) | → | mark#(X) |
Rewrite Rules
| active(filter(cons(X, Y), 0, M)) | → | mark(cons(0, filter(Y, M, M))) | | active(filter(cons(X, Y), s(N), M)) | → | mark(cons(X, filter(Y, N, M))) |
| active(sieve(cons(0, Y))) | → | mark(cons(0, sieve(Y))) | | active(sieve(cons(s(N), Y))) | → | mark(cons(s(N), sieve(filter(Y, N, N)))) |
| active(nats(N)) | → | mark(cons(N, nats(s(N)))) | | active(zprimes) | → | mark(sieve(nats(s(s(0))))) |
| mark(filter(X1, X2, X3)) | → | active(filter(mark(X1), mark(X2), mark(X3))) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(sieve(X)) | → | active(sieve(mark(X))) | | mark(nats(X)) | → | active(nats(mark(X))) |
| mark(zprimes) | → | active(zprimes) | | filter(mark(X1), X2, X3) | → | filter(X1, X2, X3) |
| filter(X1, mark(X2), X3) | → | filter(X1, X2, X3) | | filter(X1, X2, mark(X3)) | → | filter(X1, X2, X3) |
| filter(active(X1), X2, X3) | → | filter(X1, X2, X3) | | filter(X1, active(X2), X3) | → | filter(X1, X2, X3) |
| filter(X1, X2, active(X3)) | → | filter(X1, X2, X3) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | nats(mark(X)) | → | nats(X) |
| nats(active(X)) | → | nats(X) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, sieve, s, active, mark, zprimes, filter, cons
Open Dependency Pair Problem 8
Dependency Pairs
| filter#(X1, X2, active(X3)) | → | filter#(X1, X2, X3) | | filter#(X1, X2, mark(X3)) | → | filter#(X1, X2, X3) |
| filter#(X1, mark(X2), X3) | → | filter#(X1, X2, X3) | | filter#(X1, active(X2), X3) | → | filter#(X1, X2, X3) |
Rewrite Rules
| active(filter(cons(X, Y), 0, M)) | → | mark(cons(0, filter(Y, M, M))) | | active(filter(cons(X, Y), s(N), M)) | → | mark(cons(X, filter(Y, N, M))) |
| active(sieve(cons(0, Y))) | → | mark(cons(0, sieve(Y))) | | active(sieve(cons(s(N), Y))) | → | mark(cons(s(N), sieve(filter(Y, N, N)))) |
| active(nats(N)) | → | mark(cons(N, nats(s(N)))) | | active(zprimes) | → | mark(sieve(nats(s(s(0))))) |
| mark(filter(X1, X2, X3)) | → | active(filter(mark(X1), mark(X2), mark(X3))) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(sieve(X)) | → | active(sieve(mark(X))) | | mark(nats(X)) | → | active(nats(mark(X))) |
| mark(zprimes) | → | active(zprimes) | | filter(mark(X1), X2, X3) | → | filter(X1, X2, X3) |
| filter(X1, mark(X2), X3) | → | filter(X1, X2, X3) | | filter(X1, X2, mark(X3)) | → | filter(X1, X2, X3) |
| filter(active(X1), X2, X3) | → | filter(X1, X2, X3) | | filter(X1, active(X2), X3) | → | filter(X1, X2, X3) |
| filter(X1, X2, active(X3)) | → | filter(X1, X2, X3) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | nats(mark(X)) | → | nats(X) |
| nats(active(X)) | → | nats(X) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, zprimes, filter, cons
Open Dependency Pair Problem 9
Dependency Pairs
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(X1, mark(X2)) | → | cons#(X1, X2) |
Rewrite Rules
| active(filter(cons(X, Y), 0, M)) | → | mark(cons(0, filter(Y, M, M))) | | active(filter(cons(X, Y), s(N), M)) | → | mark(cons(X, filter(Y, N, M))) |
| active(sieve(cons(0, Y))) | → | mark(cons(0, sieve(Y))) | | active(sieve(cons(s(N), Y))) | → | mark(cons(s(N), sieve(filter(Y, N, N)))) |
| active(nats(N)) | → | mark(cons(N, nats(s(N)))) | | active(zprimes) | → | mark(sieve(nats(s(s(0))))) |
| mark(filter(X1, X2, X3)) | → | active(filter(mark(X1), mark(X2), mark(X3))) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(sieve(X)) | → | active(sieve(mark(X))) | | mark(nats(X)) | → | active(nats(mark(X))) |
| mark(zprimes) | → | active(zprimes) | | filter(mark(X1), X2, X3) | → | filter(X1, X2, X3) |
| filter(X1, mark(X2), X3) | → | filter(X1, X2, X3) | | filter(X1, X2, mark(X3)) | → | filter(X1, X2, X3) |
| filter(active(X1), X2, X3) | → | filter(X1, X2, X3) | | filter(X1, active(X2), X3) | → | filter(X1, X2, X3) |
| filter(X1, X2, active(X3)) | → | filter(X1, X2, X3) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | nats(mark(X)) | → | nats(X) |
| nats(active(X)) | → | nats(X) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, zprimes, filter, cons
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(cons(X1, X2)) | → | active#(cons(mark(X1), X2)) | | active#(sieve(cons(s(N), Y))) | → | sieve#(filter(Y, N, N)) |
| active#(filter(cons(X, Y), s(N), M)) | → | filter#(Y, N, M) | | filter#(X1, active(X2), X3) | → | filter#(X1, X2, X3) |
| active#(zprimes) | → | nats#(s(s(0))) | | sieve#(mark(X)) | → | sieve#(X) |
| active#(sieve(cons(s(N), Y))) | → | mark#(cons(s(N), sieve(filter(Y, N, N)))) | | mark#(s(X)) | → | s#(mark(X)) |
| active#(sieve(cons(s(N), Y))) | → | cons#(s(N), sieve(filter(Y, N, N))) | | active#(nats(N)) | → | mark#(cons(N, nats(s(N)))) |
| active#(zprimes) | → | s#(s(0)) | | mark#(s(X)) | → | mark#(X) |
| mark#(sieve(X)) | → | active#(sieve(mark(X))) | | active#(zprimes) | → | mark#(sieve(nats(s(s(0))))) |
| mark#(filter(X1, X2, X3)) | → | mark#(X3) | | filter#(active(X1), X2, X3) | → | filter#(X1, X2, X3) |
| active#(zprimes) | → | s#(0) | | mark#(cons(X1, X2)) | → | mark#(X1) |
| mark#(nats(X)) | → | nats#(mark(X)) | | nats#(mark(X)) | → | nats#(X) |
| active#(sieve(cons(0, Y))) | → | cons#(0, sieve(Y)) | | active#(sieve(cons(s(N), Y))) | → | filter#(Y, N, N) |
| active#(nats(N)) | → | nats#(s(N)) | | cons#(X1, active(X2)) | → | cons#(X1, X2) |
| sieve#(active(X)) | → | sieve#(X) | | filter#(X1, X2, mark(X3)) | → | filter#(X1, X2, X3) |
| active#(nats(N)) | → | s#(N) | | mark#(filter(X1, X2, X3)) | → | mark#(X1) |
| mark#(filter(X1, X2, X3)) | → | mark#(X2) | | mark#(nats(X)) | → | mark#(X) |
| mark#(sieve(X)) | → | mark#(X) | | active#(filter(cons(X, Y), 0, M)) | → | filter#(Y, M, M) |
| active#(filter(cons(X, Y), 0, M)) | → | mark#(cons(0, filter(Y, M, M))) | | cons#(mark(X1), X2) | → | cons#(X1, X2) |
| filter#(mark(X1), X2, X3) | → | filter#(X1, X2, X3) | | active#(filter(cons(X, Y), s(N), M)) | → | mark#(cons(X, filter(Y, N, M))) |
| nats#(active(X)) | → | nats#(X) | | filter#(X1, mark(X2), X3) | → | filter#(X1, X2, X3) |
| mark#(sieve(X)) | → | sieve#(mark(X)) | | cons#(X1, mark(X2)) | → | cons#(X1, X2) |
| mark#(cons(X1, X2)) | → | cons#(mark(X1), X2) | | active#(sieve(cons(s(N), Y))) | → | s#(N) |
| mark#(0) | → | active#(0) | | filter#(X1, X2, active(X3)) | → | filter#(X1, X2, X3) |
| mark#(s(X)) | → | active#(s(mark(X))) | | active#(filter(cons(X, Y), s(N), M)) | → | cons#(X, filter(Y, N, M)) |
| active#(nats(N)) | → | cons#(N, nats(s(N))) | | active#(sieve(cons(0, Y))) | → | sieve#(Y) |
| cons#(active(X1), X2) | → | cons#(X1, X2) | | active#(sieve(cons(0, Y))) | → | mark#(cons(0, sieve(Y))) |
| active#(zprimes) | → | sieve#(nats(s(s(0)))) | | s#(mark(X)) | → | s#(X) |
| mark#(nats(X)) | → | active#(nats(mark(X))) | | active#(filter(cons(X, Y), 0, M)) | → | cons#(0, filter(Y, M, M)) |
| mark#(zprimes) | → | active#(zprimes) | | mark#(filter(X1, X2, X3)) | → | active#(filter(mark(X1), mark(X2), mark(X3))) |
| s#(active(X)) | → | s#(X) | | mark#(filter(X1, X2, X3)) | → | filter#(mark(X1), mark(X2), mark(X3)) |
Rewrite Rules
| active(filter(cons(X, Y), 0, M)) | → | mark(cons(0, filter(Y, M, M))) | | active(filter(cons(X, Y), s(N), M)) | → | mark(cons(X, filter(Y, N, M))) |
| active(sieve(cons(0, Y))) | → | mark(cons(0, sieve(Y))) | | active(sieve(cons(s(N), Y))) | → | mark(cons(s(N), sieve(filter(Y, N, N)))) |
| active(nats(N)) | → | mark(cons(N, nats(s(N)))) | | active(zprimes) | → | mark(sieve(nats(s(s(0))))) |
| mark(filter(X1, X2, X3)) | → | active(filter(mark(X1), mark(X2), mark(X3))) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(sieve(X)) | → | active(sieve(mark(X))) | | mark(nats(X)) | → | active(nats(mark(X))) |
| mark(zprimes) | → | active(zprimes) | | filter(mark(X1), X2, X3) | → | filter(X1, X2, X3) |
| filter(X1, mark(X2), X3) | → | filter(X1, X2, X3) | | filter(X1, X2, mark(X3)) | → | filter(X1, X2, X3) |
| filter(active(X1), X2, X3) | → | filter(X1, X2, X3) | | filter(X1, active(X2), X3) | → | filter(X1, X2, X3) |
| filter(X1, X2, active(X3)) | → | filter(X1, X2, X3) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | nats(mark(X)) | → | nats(X) |
| nats(active(X)) | → | nats(X) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, zprimes, filter, cons
Strategy
The following SCCs where found
| sieve#(active(X)) → sieve#(X) | sieve#(mark(X)) → sieve#(X) |
| mark#(filter(X1, X2, X3)) → mark#(X3) | mark#(cons(X1, X2)) → active#(cons(mark(X1), X2)) |
| mark#(0) → active#(0) | mark#(s(X)) → active#(s(mark(X))) |
| active#(filter(cons(X, Y), 0, M)) → mark#(cons(0, filter(Y, M, M))) | mark#(cons(X1, X2)) → mark#(X1) |
| active#(filter(cons(X, Y), s(N), M)) → mark#(cons(X, filter(Y, N, M))) | active#(sieve(cons(0, Y))) → mark#(cons(0, sieve(Y))) |
| active#(sieve(cons(s(N), Y))) → mark#(cons(s(N), sieve(filter(Y, N, N)))) | mark#(nats(X)) → active#(nats(mark(X))) |
| mark#(zprimes) → active#(zprimes) | active#(nats(N)) → mark#(cons(N, nats(s(N)))) |
| mark#(filter(X1, X2, X3)) → active#(filter(mark(X1), mark(X2), mark(X3))) | mark#(nats(X)) → mark#(X) |
| mark#(filter(X1, X2, X3)) → mark#(X1) | mark#(filter(X1, X2, X3)) → mark#(X2) |
| mark#(s(X)) → mark#(X) | mark#(sieve(X)) → active#(sieve(mark(X))) |
| mark#(sieve(X)) → mark#(X) | active#(zprimes) → mark#(sieve(nats(s(s(0))))) |
| s#(mark(X)) → s#(X) | s#(active(X)) → s#(X) |
| cons#(X1, active(X2)) → cons#(X1, X2) | cons#(mark(X1), X2) → cons#(X1, X2) |
| cons#(X1, mark(X2)) → cons#(X1, X2) | cons#(active(X1), X2) → cons#(X1, X2) |
| filter#(active(X1), X2, X3) → filter#(X1, X2, X3) | filter#(X1, X2, active(X3)) → filter#(X1, X2, X3) |
| filter#(X1, X2, mark(X3)) → filter#(X1, X2, X3) | filter#(X1, mark(X2), X3) → filter#(X1, X2, X3) |
| filter#(X1, active(X2), X3) → filter#(X1, X2, X3) | filter#(mark(X1), X2, X3) → filter#(X1, X2, X3) |
| nats#(mark(X)) → nats#(X) | nats#(active(X)) → nats#(X) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| filter#(active(X1), X2, X3) | → | filter#(X1, X2, X3) | | filter#(X1, X2, active(X3)) | → | filter#(X1, X2, X3) |
| filter#(X1, X2, mark(X3)) | → | filter#(X1, X2, X3) | | filter#(X1, mark(X2), X3) | → | filter#(X1, X2, X3) |
| filter#(X1, active(X2), X3) | → | filter#(X1, X2, X3) | | filter#(mark(X1), X2, X3) | → | filter#(X1, X2, X3) |
Rewrite Rules
| active(filter(cons(X, Y), 0, M)) | → | mark(cons(0, filter(Y, M, M))) | | active(filter(cons(X, Y), s(N), M)) | → | mark(cons(X, filter(Y, N, M))) |
| active(sieve(cons(0, Y))) | → | mark(cons(0, sieve(Y))) | | active(sieve(cons(s(N), Y))) | → | mark(cons(s(N), sieve(filter(Y, N, N)))) |
| active(nats(N)) | → | mark(cons(N, nats(s(N)))) | | active(zprimes) | → | mark(sieve(nats(s(s(0))))) |
| mark(filter(X1, X2, X3)) | → | active(filter(mark(X1), mark(X2), mark(X3))) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(sieve(X)) | → | active(sieve(mark(X))) | | mark(nats(X)) | → | active(nats(mark(X))) |
| mark(zprimes) | → | active(zprimes) | | filter(mark(X1), X2, X3) | → | filter(X1, X2, X3) |
| filter(X1, mark(X2), X3) | → | filter(X1, X2, X3) | | filter(X1, X2, mark(X3)) | → | filter(X1, X2, X3) |
| filter(active(X1), X2, X3) | → | filter(X1, X2, X3) | | filter(X1, active(X2), X3) | → | filter(X1, X2, X3) |
| filter(X1, X2, active(X3)) | → | filter(X1, X2, X3) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | nats(mark(X)) | → | nats(X) |
| nats(active(X)) | → | nats(X) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, zprimes, filter, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| filter#(active(X1), X2, X3) | → | filter#(X1, X2, X3) | | filter#(mark(X1), X2, X3) | → | filter#(X1, X2, X3) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| sieve#(active(X)) | → | sieve#(X) | | sieve#(mark(X)) | → | sieve#(X) |
Rewrite Rules
| active(filter(cons(X, Y), 0, M)) | → | mark(cons(0, filter(Y, M, M))) | | active(filter(cons(X, Y), s(N), M)) | → | mark(cons(X, filter(Y, N, M))) |
| active(sieve(cons(0, Y))) | → | mark(cons(0, sieve(Y))) | | active(sieve(cons(s(N), Y))) | → | mark(cons(s(N), sieve(filter(Y, N, N)))) |
| active(nats(N)) | → | mark(cons(N, nats(s(N)))) | | active(zprimes) | → | mark(sieve(nats(s(s(0))))) |
| mark(filter(X1, X2, X3)) | → | active(filter(mark(X1), mark(X2), mark(X3))) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(sieve(X)) | → | active(sieve(mark(X))) | | mark(nats(X)) | → | active(nats(mark(X))) |
| mark(zprimes) | → | active(zprimes) | | filter(mark(X1), X2, X3) | → | filter(X1, X2, X3) |
| filter(X1, mark(X2), X3) | → | filter(X1, X2, X3) | | filter(X1, X2, mark(X3)) | → | filter(X1, X2, X3) |
| filter(active(X1), X2, X3) | → | filter(X1, X2, X3) | | filter(X1, active(X2), X3) | → | filter(X1, X2, X3) |
| filter(X1, X2, active(X3)) | → | filter(X1, X2, X3) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | nats(mark(X)) | → | nats(X) |
| nats(active(X)) | → | nats(X) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, zprimes, filter, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| sieve#(active(X)) | → | sieve#(X) | | sieve#(mark(X)) | → | sieve#(X) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s#(mark(X)) | → | s#(X) | | s#(active(X)) | → | s#(X) |
Rewrite Rules
| active(filter(cons(X, Y), 0, M)) | → | mark(cons(0, filter(Y, M, M))) | | active(filter(cons(X, Y), s(N), M)) | → | mark(cons(X, filter(Y, N, M))) |
| active(sieve(cons(0, Y))) | → | mark(cons(0, sieve(Y))) | | active(sieve(cons(s(N), Y))) | → | mark(cons(s(N), sieve(filter(Y, N, N)))) |
| active(nats(N)) | → | mark(cons(N, nats(s(N)))) | | active(zprimes) | → | mark(sieve(nats(s(s(0))))) |
| mark(filter(X1, X2, X3)) | → | active(filter(mark(X1), mark(X2), mark(X3))) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(sieve(X)) | → | active(sieve(mark(X))) | | mark(nats(X)) | → | active(nats(mark(X))) |
| mark(zprimes) | → | active(zprimes) | | filter(mark(X1), X2, X3) | → | filter(X1, X2, X3) |
| filter(X1, mark(X2), X3) | → | filter(X1, X2, X3) | | filter(X1, X2, mark(X3)) | → | filter(X1, X2, X3) |
| filter(active(X1), X2, X3) | → | filter(X1, X2, X3) | | filter(X1, active(X2), X3) | → | filter(X1, X2, X3) |
| filter(X1, X2, active(X3)) | → | filter(X1, X2, X3) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | nats(mark(X)) | → | nats(X) |
| nats(active(X)) | → | nats(X) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, zprimes, filter, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| s#(mark(X)) | → | s#(X) | | s#(active(X)) | → | s#(X) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| nats#(mark(X)) | → | nats#(X) | | nats#(active(X)) | → | nats#(X) |
Rewrite Rules
| active(filter(cons(X, Y), 0, M)) | → | mark(cons(0, filter(Y, M, M))) | | active(filter(cons(X, Y), s(N), M)) | → | mark(cons(X, filter(Y, N, M))) |
| active(sieve(cons(0, Y))) | → | mark(cons(0, sieve(Y))) | | active(sieve(cons(s(N), Y))) | → | mark(cons(s(N), sieve(filter(Y, N, N)))) |
| active(nats(N)) | → | mark(cons(N, nats(s(N)))) | | active(zprimes) | → | mark(sieve(nats(s(s(0))))) |
| mark(filter(X1, X2, X3)) | → | active(filter(mark(X1), mark(X2), mark(X3))) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(sieve(X)) | → | active(sieve(mark(X))) | | mark(nats(X)) | → | active(nats(mark(X))) |
| mark(zprimes) | → | active(zprimes) | | filter(mark(X1), X2, X3) | → | filter(X1, X2, X3) |
| filter(X1, mark(X2), X3) | → | filter(X1, X2, X3) | | filter(X1, X2, mark(X3)) | → | filter(X1, X2, X3) |
| filter(active(X1), X2, X3) | → | filter(X1, X2, X3) | | filter(X1, active(X2), X3) | → | filter(X1, X2, X3) |
| filter(X1, X2, active(X3)) | → | filter(X1, X2, X3) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | nats(mark(X)) | → | nats(X) |
| nats(active(X)) | → | nats(X) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, zprimes, filter, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| nats#(mark(X)) | → | nats#(X) | | nats#(active(X)) | → | nats#(X) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(mark(X1), X2) | → | cons#(X1, X2) |
| cons#(X1, mark(X2)) | → | cons#(X1, X2) | | cons#(active(X1), X2) | → | cons#(X1, X2) |
Rewrite Rules
| active(filter(cons(X, Y), 0, M)) | → | mark(cons(0, filter(Y, M, M))) | | active(filter(cons(X, Y), s(N), M)) | → | mark(cons(X, filter(Y, N, M))) |
| active(sieve(cons(0, Y))) | → | mark(cons(0, sieve(Y))) | | active(sieve(cons(s(N), Y))) | → | mark(cons(s(N), sieve(filter(Y, N, N)))) |
| active(nats(N)) | → | mark(cons(N, nats(s(N)))) | | active(zprimes) | → | mark(sieve(nats(s(s(0))))) |
| mark(filter(X1, X2, X3)) | → | active(filter(mark(X1), mark(X2), mark(X3))) | | mark(cons(X1, X2)) | → | active(cons(mark(X1), X2)) |
| mark(0) | → | active(0) | | mark(s(X)) | → | active(s(mark(X))) |
| mark(sieve(X)) | → | active(sieve(mark(X))) | | mark(nats(X)) | → | active(nats(mark(X))) |
| mark(zprimes) | → | active(zprimes) | | filter(mark(X1), X2, X3) | → | filter(X1, X2, X3) |
| filter(X1, mark(X2), X3) | → | filter(X1, X2, X3) | | filter(X1, X2, mark(X3)) | → | filter(X1, X2, X3) |
| filter(active(X1), X2, X3) | → | filter(X1, X2, X3) | | filter(X1, active(X2), X3) | → | filter(X1, X2, X3) |
| filter(X1, X2, active(X3)) | → | filter(X1, X2, X3) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| cons(X1, mark(X2)) | → | cons(X1, X2) | | cons(active(X1), X2) | → | cons(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | s(mark(X)) | → | s(X) |
| s(active(X)) | → | s(X) | | sieve(mark(X)) | → | sieve(X) |
| sieve(active(X)) | → | sieve(X) | | nats(mark(X)) | → | nats(X) |
| nats(active(X)) | → | nats(X) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, zprimes, filter, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(active(X1), X2) | → | cons#(X1, X2) |