YES
The TRS could be proven terminating. The proof took 5260 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (688ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (2800ms).
| | – Problem 12 was processed with processor PolynomialLinearRange4iUR (1676ms).
| – Problem 3 was processed with processor SubtermCriterion (2ms).
| – Problem 4 was processed with processor SubtermCriterion (2ms).
| – Problem 5 was processed with processor SubtermCriterion (2ms).
| – Problem 6 was processed with processor SubtermCriterion (2ms).
| – Problem 7 was processed with processor SubtermCriterion (1ms).
| – Problem 8 was processed with processor SubtermCriterion (4ms).
| – Problem 9 was processed with processor SubtermCriterion (8ms).
| | – Problem 10 was processed with processor SubtermCriterion (0ms).
| | | – Problem 11 was processed with processor PolynomialLinearRange4iUR (9ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| proper#(cons(X1, X2)) | → | proper#(X1) | | top#(ok(X)) | → | top#(active(X)) |
| active#(sieve(cons(s(N), Y))) | → | sieve#(filter(Y, N, N)) | | active#(nats(X)) | → | active#(X) |
| active#(filter(cons(X, Y), s(N), M)) | → | filter#(Y, N, M) | | active#(zprimes) | → | nats#(s(s(0))) |
| active#(sieve(X)) | → | active#(X) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
| sieve#(mark(X)) | → | sieve#(X) | | active#(nats(X)) | → | nats#(active(X)) |
| proper#(sieve(X)) | → | sieve#(proper(X)) | | active#(cons(X1, X2)) | → | cons#(active(X1), X2) |
| active#(filter(X1, X2, X3)) | → | active#(X1) | | active#(sieve(cons(s(N), Y))) | → | cons#(s(N), sieve(filter(Y, N, N))) |
| active#(zprimes) | → | s#(s(0)) | | proper#(filter(X1, X2, X3)) | → | proper#(X1) |
| top#(mark(X)) | → | proper#(X) | | nats#(ok(X)) | → | nats#(X) |
| active#(zprimes) | → | s#(0) | | top#(mark(X)) | → | top#(proper(X)) |
| proper#(cons(X1, X2)) | → | proper#(X2) | | filter#(ok(X1), ok(X2), ok(X3)) | → | filter#(X1, X2, X3) |
| 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)) |
| proper#(s(X)) | → | proper#(X) | | active#(filter(X1, X2, X3)) | → | filter#(X1, active(X2), X3) |
| filter#(X1, X2, mark(X3)) | → | filter#(X1, X2, X3) | | proper#(filter(X1, X2, X3)) | → | proper#(X3) |
| active#(nats(N)) | → | s#(N) | | proper#(filter(X1, X2, X3)) | → | proper#(X2) |
| proper#(filter(X1, X2, X3)) | → | filter#(proper(X1), proper(X2), proper(X3)) | | proper#(nats(X)) | → | nats#(proper(X)) |
| active#(cons(X1, X2)) | → | active#(X1) | | active#(filter(cons(X, Y), 0, M)) | → | filter#(Y, M, M) |
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | filter#(mark(X1), X2, X3) | → | filter#(X1, X2, X3) |
| top#(ok(X)) | → | active#(X) | | active#(filter(X1, X2, X3)) | → | filter#(active(X1), X2, X3) |
| filter#(X1, mark(X2), X3) | → | filter#(X1, X2, X3) | | active#(filter(X1, X2, X3)) | → | active#(X2) |
| active#(sieve(X)) | → | sieve#(active(X)) | | active#(filter(X1, X2, X3)) | → | active#(X3) |
| active#(sieve(cons(s(N), Y))) | → | s#(N) | | sieve#(ok(X)) | → | sieve#(X) |
| active#(filter(X1, X2, X3)) | → | filter#(X1, X2, active(X3)) | | 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) |
| active#(s(X)) | → | s#(active(X)) | | active#(zprimes) | → | sieve#(nats(s(s(0)))) |
| s#(ok(X)) | → | s#(X) | | s#(mark(X)) | → | s#(X) |
| active#(filter(cons(X, Y), 0, M)) | → | cons#(0, filter(Y, M, M)) | | proper#(cons(X1, X2)) | → | cons#(proper(X1), proper(X2)) |
| active#(s(X)) | → | active#(X) | | proper#(s(X)) | → | s#(proper(X)) |
| proper#(nats(X)) | → | proper#(X) | | proper#(sieve(X)) | → | proper#(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))))) |
| active(filter(X1, X2, X3)) | → | filter(active(X1), X2, X3) | | active(filter(X1, X2, X3)) | → | filter(X1, active(X2), X3) |
| active(filter(X1, X2, X3)) | → | filter(X1, X2, active(X3)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(sieve(X)) | → | sieve(active(X)) |
| active(nats(X)) | → | nats(active(X)) | | filter(mark(X1), X2, X3) | → | mark(filter(X1, X2, X3)) |
| filter(X1, mark(X2), X3) | → | mark(filter(X1, X2, X3)) | | filter(X1, X2, mark(X3)) | → | mark(filter(X1, X2, X3)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| sieve(mark(X)) | → | mark(sieve(X)) | | nats(mark(X)) | → | mark(nats(X)) |
| proper(filter(X1, X2, X3)) | → | filter(proper(X1), proper(X2), proper(X3)) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(sieve(X)) | → | sieve(proper(X)) | | proper(nats(X)) | → | nats(proper(X)) |
| proper(zprimes) | → | ok(zprimes) | | filter(ok(X1), ok(X2), ok(X3)) | → | ok(filter(X1, X2, X3)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| sieve(ok(X)) | → | ok(sieve(X)) | | nats(ok(X)) | → | ok(nats(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top
Strategy
The following SCCs where found
| active#(nats(X)) → active#(X) | active#(s(X)) → active#(X) |
| active#(sieve(X)) → active#(X) | active#(filter(X1, X2, X3)) → active#(X2) |
| active#(filter(X1, X2, X3)) → active#(X1) | active#(cons(X1, X2)) → active#(X1) |
| active#(filter(X1, X2, X3)) → active#(X3) |
| sieve#(ok(X)) → sieve#(X) | sieve#(mark(X)) → sieve#(X) |
| cons#(mark(X1), X2) → cons#(X1, X2) | cons#(ok(X1), ok(X2)) → cons#(X1, X2) |
| proper#(s(X)) → proper#(X) | proper#(cons(X1, X2)) → proper#(X1) |
| proper#(filter(X1, X2, X3)) → proper#(X3) | proper#(cons(X1, X2)) → proper#(X2) |
| proper#(filter(X1, X2, X3)) → proper#(X1) | proper#(filter(X1, X2, X3)) → proper#(X2) |
| proper#(nats(X)) → proper#(X) | proper#(sieve(X)) → proper#(X) |
| filter#(X1, X2, mark(X3)) → filter#(X1, X2, X3) | filter#(ok(X1), ok(X2), ok(X3)) → filter#(X1, X2, X3) |
| filter#(X1, mark(X2), X3) → filter#(X1, X2, X3) | filter#(mark(X1), X2, X3) → filter#(X1, X2, X3) |
| nats#(ok(X)) → nats#(X) | nats#(mark(X)) → nats#(X) |
| top#(mark(X)) → top#(proper(X)) | top#(ok(X)) → top#(active(X)) |
| s#(mark(X)) → s#(X) | s#(ok(X)) → s#(X) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| top#(mark(X)) | → | top#(proper(X)) | | top#(ok(X)) | → | top#(active(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))))) |
| active(filter(X1, X2, X3)) | → | filter(active(X1), X2, X3) | | active(filter(X1, X2, X3)) | → | filter(X1, active(X2), X3) |
| active(filter(X1, X2, X3)) | → | filter(X1, X2, active(X3)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(sieve(X)) | → | sieve(active(X)) |
| active(nats(X)) | → | nats(active(X)) | | filter(mark(X1), X2, X3) | → | mark(filter(X1, X2, X3)) |
| filter(X1, mark(X2), X3) | → | mark(filter(X1, X2, X3)) | | filter(X1, X2, mark(X3)) | → | mark(filter(X1, X2, X3)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| sieve(mark(X)) | → | mark(sieve(X)) | | nats(mark(X)) | → | mark(nats(X)) |
| proper(filter(X1, X2, X3)) | → | filter(proper(X1), proper(X2), proper(X3)) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(sieve(X)) | → | sieve(proper(X)) | | proper(nats(X)) | → | nats(proper(X)) |
| proper(zprimes) | → | ok(zprimes) | | filter(ok(X1), ok(X2), ok(X3)) | → | ok(filter(X1, X2, X3)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| sieve(ok(X)) | → | ok(sieve(X)) | | nats(ok(X)) | → | ok(nats(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top
Strategy
Polynomial Interpretation
- 0: 0
- active(x): x
- cons(x,y): 2x
- filter(x,y,z): z + 2y + x + 1
- mark(x): x + 1
- nats(x): 2x + 1
- ok(x): x
- proper(x): x
- s(x): 2x
- sieve(x): x + 1
- top(x): 0
- top#(x): 2x
- zprimes: 3
Improved Usable rules
| sieve(mark(X)) | → | mark(sieve(X)) | | nats(ok(X)) | → | ok(nats(X)) |
| active(s(X)) | → | s(active(X)) | | active(sieve(cons(0, Y))) | → | mark(cons(0, sieve(Y))) |
| filter(X1, X2, mark(X3)) | → | mark(filter(X1, X2, X3)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| proper(filter(X1, X2, X3)) | → | filter(proper(X1), proper(X2), proper(X3)) | | filter(X1, mark(X2), X3) | → | mark(filter(X1, X2, X3)) |
| s(mark(X)) | → | mark(s(X)) | | proper(s(X)) | → | s(proper(X)) |
| active(nats(X)) | → | nats(active(X)) | | nats(mark(X)) | → | mark(nats(X)) |
| proper(sieve(X)) | → | sieve(proper(X)) | | active(filter(cons(X, Y), s(N), M)) | → | mark(cons(X, filter(Y, N, M))) |
| sieve(ok(X)) | → | ok(sieve(X)) | | active(sieve(X)) | → | sieve(active(X)) |
| filter(mark(X1), X2, X3) | → | mark(filter(X1, X2, X3)) | | active(sieve(cons(s(N), Y))) | → | mark(cons(s(N), sieve(filter(Y, N, N)))) |
| active(filter(X1, X2, X3)) | → | filter(X1, X2, active(X3)) | | s(ok(X)) | → | ok(s(X)) |
| filter(ok(X1), ok(X2), ok(X3)) | → | ok(filter(X1, X2, X3)) | | active(filter(cons(X, Y), 0, M)) | → | mark(cons(0, filter(Y, M, M))) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | active(nats(N)) | → | mark(cons(N, nats(s(N)))) |
| active(zprimes) | → | mark(sieve(nats(s(s(0))))) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) | | proper(nats(X)) | → | nats(proper(X)) |
| active(filter(X1, X2, X3)) | → | filter(X1, active(X2), X3) | | proper(zprimes) | → | ok(zprimes) |
| active(filter(X1, X2, X3)) | → | filter(active(X1), X2, X3) | | proper(0) | → | ok(0) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| top#(mark(X)) | → | top#(proper(X)) |
Problem 12: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| top#(ok(X)) | → | top#(active(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))))) |
| active(filter(X1, X2, X3)) | → | filter(active(X1), X2, X3) | | active(filter(X1, X2, X3)) | → | filter(X1, active(X2), X3) |
| active(filter(X1, X2, X3)) | → | filter(X1, X2, active(X3)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(sieve(X)) | → | sieve(active(X)) |
| active(nats(X)) | → | nats(active(X)) | | filter(mark(X1), X2, X3) | → | mark(filter(X1, X2, X3)) |
| filter(X1, mark(X2), X3) | → | mark(filter(X1, X2, X3)) | | filter(X1, X2, mark(X3)) | → | mark(filter(X1, X2, X3)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| sieve(mark(X)) | → | mark(sieve(X)) | | nats(mark(X)) | → | mark(nats(X)) |
| proper(filter(X1, X2, X3)) | → | filter(proper(X1), proper(X2), proper(X3)) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(sieve(X)) | → | sieve(proper(X)) | | proper(nats(X)) | → | nats(proper(X)) |
| proper(zprimes) | → | ok(zprimes) | | filter(ok(X1), ok(X2), ok(X3)) | → | ok(filter(X1, X2, X3)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| sieve(ok(X)) | → | ok(sieve(X)) | | nats(ok(X)) | → | ok(nats(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, sieve, s, active, ok, mark, proper, zprimes, filter, top, cons
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 2x
- cons(x,y): x
- filter(x,y,z): 2x + 1
- mark(x): 0
- nats(x): 2x
- ok(x): 2x + 1
- proper(x): 0
- s(x): x
- sieve(x): 2x
- top(x): 0
- top#(x): x
- zprimes: 0
Improved Usable rules
| nats(ok(X)) | → | ok(nats(X)) | | sieve(mark(X)) | → | mark(sieve(X)) |
| active(s(X)) | → | s(active(X)) | | active(sieve(cons(0, Y))) | → | mark(cons(0, sieve(Y))) |
| filter(X1, X2, mark(X3)) | → | mark(filter(X1, X2, X3)) | | cons(mark(X1), X2) | → | mark(cons(X1, X2)) |
| filter(X1, mark(X2), X3) | → | mark(filter(X1, X2, X3)) | | s(mark(X)) | → | mark(s(X)) |
| nats(mark(X)) | → | mark(nats(X)) | | active(nats(X)) | → | nats(active(X)) |
| active(filter(cons(X, Y), s(N), M)) | → | mark(cons(X, filter(Y, N, M))) | | sieve(ok(X)) | → | ok(sieve(X)) |
| active(sieve(X)) | → | sieve(active(X)) | | active(sieve(cons(s(N), Y))) | → | mark(cons(s(N), sieve(filter(Y, N, N)))) |
| filter(mark(X1), X2, X3) | → | mark(filter(X1, X2, X3)) | | active(filter(X1, X2, X3)) | → | filter(X1, X2, active(X3)) |
| s(ok(X)) | → | ok(s(X)) | | filter(ok(X1), ok(X2), ok(X3)) | → | ok(filter(X1, X2, X3)) |
| active(filter(cons(X, Y), 0, M)) | → | mark(cons(0, filter(Y, M, M))) | | cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) |
| active(nats(N)) | → | mark(cons(N, nats(s(N)))) | | active(zprimes) | → | mark(sieve(nats(s(s(0))))) |
| active(cons(X1, X2)) | → | cons(active(X1), X2) | | active(filter(X1, X2, X3)) | → | filter(X1, active(X2), X3) |
| active(filter(X1, X2, X3)) | → | filter(active(X1), X2, X3) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| top#(ok(X)) | → | top#(active(X)) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| proper#(s(X)) | → | proper#(X) | | proper#(cons(X1, X2)) | → | proper#(X1) |
| proper#(filter(X1, X2, X3)) | → | proper#(X3) | | proper#(cons(X1, X2)) | → | proper#(X2) |
| proper#(filter(X1, X2, X3)) | → | proper#(X1) | | proper#(filter(X1, X2, X3)) | → | proper#(X2) |
| proper#(nats(X)) | → | proper#(X) | | proper#(sieve(X)) | → | proper#(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))))) |
| active(filter(X1, X2, X3)) | → | filter(active(X1), X2, X3) | | active(filter(X1, X2, X3)) | → | filter(X1, active(X2), X3) |
| active(filter(X1, X2, X3)) | → | filter(X1, X2, active(X3)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(sieve(X)) | → | sieve(active(X)) |
| active(nats(X)) | → | nats(active(X)) | | filter(mark(X1), X2, X3) | → | mark(filter(X1, X2, X3)) |
| filter(X1, mark(X2), X3) | → | mark(filter(X1, X2, X3)) | | filter(X1, X2, mark(X3)) | → | mark(filter(X1, X2, X3)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| sieve(mark(X)) | → | mark(sieve(X)) | | nats(mark(X)) | → | mark(nats(X)) |
| proper(filter(X1, X2, X3)) | → | filter(proper(X1), proper(X2), proper(X3)) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(sieve(X)) | → | sieve(proper(X)) | | proper(nats(X)) | → | nats(proper(X)) |
| proper(zprimes) | → | ok(zprimes) | | filter(ok(X1), ok(X2), ok(X3)) | → | ok(filter(X1, X2, X3)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| sieve(ok(X)) | → | ok(sieve(X)) | | nats(ok(X)) | → | ok(nats(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| proper#(s(X)) | → | proper#(X) | | proper#(cons(X1, X2)) | → | proper#(X1) |
| proper#(cons(X1, X2)) | → | proper#(X2) | | proper#(filter(X1, X2, X3)) | → | proper#(X3) |
| proper#(filter(X1, X2, X3)) | → | proper#(X2) | | proper#(filter(X1, X2, X3)) | → | proper#(X1) |
| proper#(nats(X)) | → | proper#(X) | | proper#(sieve(X)) | → | proper#(X) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(ok(X1), ok(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))))) |
| active(filter(X1, X2, X3)) | → | filter(active(X1), X2, X3) | | active(filter(X1, X2, X3)) | → | filter(X1, active(X2), X3) |
| active(filter(X1, X2, X3)) | → | filter(X1, X2, active(X3)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(sieve(X)) | → | sieve(active(X)) |
| active(nats(X)) | → | nats(active(X)) | | filter(mark(X1), X2, X3) | → | mark(filter(X1, X2, X3)) |
| filter(X1, mark(X2), X3) | → | mark(filter(X1, X2, X3)) | | filter(X1, X2, mark(X3)) | → | mark(filter(X1, X2, X3)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| sieve(mark(X)) | → | mark(sieve(X)) | | nats(mark(X)) | → | mark(nats(X)) |
| proper(filter(X1, X2, X3)) | → | filter(proper(X1), proper(X2), proper(X3)) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(sieve(X)) | → | sieve(proper(X)) | | proper(nats(X)) | → | nats(proper(X)) |
| proper(zprimes) | → | ok(zprimes) | | filter(ok(X1), ok(X2), ok(X3)) | → | ok(filter(X1, X2, X3)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| sieve(ok(X)) | → | ok(sieve(X)) | | nats(ok(X)) | → | ok(nats(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | cons#(ok(X1), ok(X2)) | → | cons#(X1, X2) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| nats#(ok(X)) | → | nats#(X) | | nats#(mark(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))))) |
| active(filter(X1, X2, X3)) | → | filter(active(X1), X2, X3) | | active(filter(X1, X2, X3)) | → | filter(X1, active(X2), X3) |
| active(filter(X1, X2, X3)) | → | filter(X1, X2, active(X3)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(sieve(X)) | → | sieve(active(X)) |
| active(nats(X)) | → | nats(active(X)) | | filter(mark(X1), X2, X3) | → | mark(filter(X1, X2, X3)) |
| filter(X1, mark(X2), X3) | → | mark(filter(X1, X2, X3)) | | filter(X1, X2, mark(X3)) | → | mark(filter(X1, X2, X3)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| sieve(mark(X)) | → | mark(sieve(X)) | | nats(mark(X)) | → | mark(nats(X)) |
| proper(filter(X1, X2, X3)) | → | filter(proper(X1), proper(X2), proper(X3)) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(sieve(X)) | → | sieve(proper(X)) | | proper(nats(X)) | → | nats(proper(X)) |
| proper(zprimes) | → | ok(zprimes) | | filter(ok(X1), ok(X2), ok(X3)) | → | ok(filter(X1, X2, X3)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| sieve(ok(X)) | → | ok(sieve(X)) | | nats(ok(X)) | → | ok(nats(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| nats#(ok(X)) | → | nats#(X) | | nats#(mark(X)) | → | nats#(X) |
Problem 6: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| active#(nats(X)) | → | active#(X) | | active#(s(X)) | → | active#(X) |
| active#(sieve(X)) | → | active#(X) | | active#(filter(X1, X2, X3)) | → | active#(X2) |
| active#(filter(X1, X2, X3)) | → | active#(X1) | | active#(cons(X1, X2)) | → | active#(X1) |
| active#(filter(X1, X2, X3)) | → | active#(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))))) |
| active(filter(X1, X2, X3)) | → | filter(active(X1), X2, X3) | | active(filter(X1, X2, X3)) | → | filter(X1, active(X2), X3) |
| active(filter(X1, X2, X3)) | → | filter(X1, X2, active(X3)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(sieve(X)) | → | sieve(active(X)) |
| active(nats(X)) | → | nats(active(X)) | | filter(mark(X1), X2, X3) | → | mark(filter(X1, X2, X3)) |
| filter(X1, mark(X2), X3) | → | mark(filter(X1, X2, X3)) | | filter(X1, X2, mark(X3)) | → | mark(filter(X1, X2, X3)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| sieve(mark(X)) | → | mark(sieve(X)) | | nats(mark(X)) | → | mark(nats(X)) |
| proper(filter(X1, X2, X3)) | → | filter(proper(X1), proper(X2), proper(X3)) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(sieve(X)) | → | sieve(proper(X)) | | proper(nats(X)) | → | nats(proper(X)) |
| proper(zprimes) | → | ok(zprimes) | | filter(ok(X1), ok(X2), ok(X3)) | → | ok(filter(X1, X2, X3)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| sieve(ok(X)) | → | ok(sieve(X)) | | nats(ok(X)) | → | ok(nats(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| active#(nats(X)) | → | active#(X) | | active#(s(X)) | → | active#(X) |
| active#(sieve(X)) | → | active#(X) | | active#(filter(X1, X2, X3)) | → | active#(X2) |
| active#(filter(X1, X2, X3)) | → | active#(X3) | | active#(filter(X1, X2, X3)) | → | active#(X1) |
| active#(cons(X1, X2)) | → | active#(X1) |
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s#(mark(X)) | → | s#(X) | | s#(ok(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))))) |
| active(filter(X1, X2, X3)) | → | filter(active(X1), X2, X3) | | active(filter(X1, X2, X3)) | → | filter(X1, active(X2), X3) |
| active(filter(X1, X2, X3)) | → | filter(X1, X2, active(X3)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(sieve(X)) | → | sieve(active(X)) |
| active(nats(X)) | → | nats(active(X)) | | filter(mark(X1), X2, X3) | → | mark(filter(X1, X2, X3)) |
| filter(X1, mark(X2), X3) | → | mark(filter(X1, X2, X3)) | | filter(X1, X2, mark(X3)) | → | mark(filter(X1, X2, X3)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| sieve(mark(X)) | → | mark(sieve(X)) | | nats(mark(X)) | → | mark(nats(X)) |
| proper(filter(X1, X2, X3)) | → | filter(proper(X1), proper(X2), proper(X3)) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(sieve(X)) | → | sieve(proper(X)) | | proper(nats(X)) | → | nats(proper(X)) |
| proper(zprimes) | → | ok(zprimes) | | filter(ok(X1), ok(X2), ok(X3)) | → | ok(filter(X1, X2, X3)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| sieve(ok(X)) | → | ok(sieve(X)) | | nats(ok(X)) | → | ok(nats(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| s#(mark(X)) | → | s#(X) | | s#(ok(X)) | → | s#(X) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| sieve#(ok(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))))) |
| active(filter(X1, X2, X3)) | → | filter(active(X1), X2, X3) | | active(filter(X1, X2, X3)) | → | filter(X1, active(X2), X3) |
| active(filter(X1, X2, X3)) | → | filter(X1, X2, active(X3)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(sieve(X)) | → | sieve(active(X)) |
| active(nats(X)) | → | nats(active(X)) | | filter(mark(X1), X2, X3) | → | mark(filter(X1, X2, X3)) |
| filter(X1, mark(X2), X3) | → | mark(filter(X1, X2, X3)) | | filter(X1, X2, mark(X3)) | → | mark(filter(X1, X2, X3)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| sieve(mark(X)) | → | mark(sieve(X)) | | nats(mark(X)) | → | mark(nats(X)) |
| proper(filter(X1, X2, X3)) | → | filter(proper(X1), proper(X2), proper(X3)) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(sieve(X)) | → | sieve(proper(X)) | | proper(nats(X)) | → | nats(proper(X)) |
| proper(zprimes) | → | ok(zprimes) | | filter(ok(X1), ok(X2), ok(X3)) | → | ok(filter(X1, X2, X3)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| sieve(ok(X)) | → | ok(sieve(X)) | | nats(ok(X)) | → | ok(nats(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| sieve#(ok(X)) | → | sieve#(X) | | sieve#(mark(X)) | → | sieve#(X) |
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| filter#(X1, X2, mark(X3)) | → | filter#(X1, X2, X3) | | filter#(ok(X1), ok(X2), ok(X3)) | → | filter#(X1, X2, X3) |
| filter#(X1, mark(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))))) |
| active(filter(X1, X2, X3)) | → | filter(active(X1), X2, X3) | | active(filter(X1, X2, X3)) | → | filter(X1, active(X2), X3) |
| active(filter(X1, X2, X3)) | → | filter(X1, X2, active(X3)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(sieve(X)) | → | sieve(active(X)) |
| active(nats(X)) | → | nats(active(X)) | | filter(mark(X1), X2, X3) | → | mark(filter(X1, X2, X3)) |
| filter(X1, mark(X2), X3) | → | mark(filter(X1, X2, X3)) | | filter(X1, X2, mark(X3)) | → | mark(filter(X1, X2, X3)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| sieve(mark(X)) | → | mark(sieve(X)) | | nats(mark(X)) | → | mark(nats(X)) |
| proper(filter(X1, X2, X3)) | → | filter(proper(X1), proper(X2), proper(X3)) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(sieve(X)) | → | sieve(proper(X)) | | proper(nats(X)) | → | nats(proper(X)) |
| proper(zprimes) | → | ok(zprimes) | | filter(ok(X1), ok(X2), ok(X3)) | → | ok(filter(X1, X2, X3)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| sieve(ok(X)) | → | ok(sieve(X)) | | nats(ok(X)) | → | ok(nats(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| filter#(ok(X1), ok(X2), ok(X3)) | → | filter#(X1, X2, X3) | | filter#(mark(X1), X2, X3) | → | filter#(X1, X2, X3) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| filter#(X1, X2, mark(X3)) | → | filter#(X1, X2, X3) | | filter#(X1, mark(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))))) |
| active(filter(X1, X2, X3)) | → | filter(active(X1), X2, X3) | | active(filter(X1, X2, X3)) | → | filter(X1, active(X2), X3) |
| active(filter(X1, X2, X3)) | → | filter(X1, X2, active(X3)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(sieve(X)) | → | sieve(active(X)) |
| active(nats(X)) | → | nats(active(X)) | | filter(mark(X1), X2, X3) | → | mark(filter(X1, X2, X3)) |
| filter(X1, mark(X2), X3) | → | mark(filter(X1, X2, X3)) | | filter(X1, X2, mark(X3)) | → | mark(filter(X1, X2, X3)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| sieve(mark(X)) | → | mark(sieve(X)) | | nats(mark(X)) | → | mark(nats(X)) |
| proper(filter(X1, X2, X3)) | → | filter(proper(X1), proper(X2), proper(X3)) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(sieve(X)) | → | sieve(proper(X)) | | proper(nats(X)) | → | nats(proper(X)) |
| proper(zprimes) | → | ok(zprimes) | | filter(ok(X1), ok(X2), ok(X3)) | → | ok(filter(X1, X2, X3)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| sieve(ok(X)) | → | ok(sieve(X)) | | nats(ok(X)) | → | ok(nats(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, sieve, s, active, ok, mark, proper, zprimes, filter, top, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| filter#(X1, mark(X2), X3) | → | filter#(X1, X2, X3) |
Problem 11: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| filter#(X1, X2, mark(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))))) |
| active(filter(X1, X2, X3)) | → | filter(active(X1), X2, X3) | | active(filter(X1, X2, X3)) | → | filter(X1, active(X2), X3) |
| active(filter(X1, X2, X3)) | → | filter(X1, X2, active(X3)) | | active(cons(X1, X2)) | → | cons(active(X1), X2) |
| active(s(X)) | → | s(active(X)) | | active(sieve(X)) | → | sieve(active(X)) |
| active(nats(X)) | → | nats(active(X)) | | filter(mark(X1), X2, X3) | → | mark(filter(X1, X2, X3)) |
| filter(X1, mark(X2), X3) | → | mark(filter(X1, X2, X3)) | | filter(X1, X2, mark(X3)) | → | mark(filter(X1, X2, X3)) |
| cons(mark(X1), X2) | → | mark(cons(X1, X2)) | | s(mark(X)) | → | mark(s(X)) |
| sieve(mark(X)) | → | mark(sieve(X)) | | nats(mark(X)) | → | mark(nats(X)) |
| proper(filter(X1, X2, X3)) | → | filter(proper(X1), proper(X2), proper(X3)) | | proper(cons(X1, X2)) | → | cons(proper(X1), proper(X2)) |
| proper(0) | → | ok(0) | | proper(s(X)) | → | s(proper(X)) |
| proper(sieve(X)) | → | sieve(proper(X)) | | proper(nats(X)) | → | nats(proper(X)) |
| proper(zprimes) | → | ok(zprimes) | | filter(ok(X1), ok(X2), ok(X3)) | → | ok(filter(X1, X2, X3)) |
| cons(ok(X1), ok(X2)) | → | ok(cons(X1, X2)) | | s(ok(X)) | → | ok(s(X)) |
| sieve(ok(X)) | → | ok(sieve(X)) | | nats(ok(X)) | → | ok(nats(X)) |
| top(mark(X)) | → | top(proper(X)) | | top(ok(X)) | → | top(active(X)) |
Original Signature
Termination of terms over the following signature is verified: nats, 0, s, sieve, active, mark, ok, proper, zprimes, filter, cons, top
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 0
- cons(x,y): 0
- filter(x,y,z): 0
- filter#(x,y,z): 2z + y + x
- mark(x): 2x + 1
- nats(x): 0
- ok(x): 0
- proper(x): 0
- s(x): 0
- sieve(x): 0
- top(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#(X1, X2, mark(X3)) | → | filter#(X1, X2, X3) |