YES
The TRS could be proven terminating. The proof took 42420 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (673ms).
| – Problem 2 was processed with processor SubtermCriterion (8ms).
| – Problem 3 was processed with processor SubtermCriterion (0ms).
| – Problem 4 was processed with processor SubtermCriterion (0ms).
| | – Problem 9 was processed with processor SubtermCriterion (1ms).
| – Problem 5 was processed with processor SubtermCriterion (1ms).
| – Problem 6 was processed with processor PolynomialLinearRange4 (236ms).
| | – Problem 12 was processed with processor PolynomialLinearRange4 (362ms).
| | | – Problem 13 was processed with processor PolynomialLinearRange4 (199ms).
| | | | – Problem 14 was processed with processor PolynomialLinearRange4 (161ms).
| | | | | – Problem 15 was processed with processor PolynomialLinearRange4 (161ms).
| | | | | | – Problem 16 was processed with processor PolynomialLinearRange4 (126ms).
| | | | | | | – Problem 17 was processed with processor PolynomialLinearRange4 (52ms).
| | | | | | | | – Problem 18 was processed with processor DependencyGraph (1ms).
| – Problem 7 was processed with processor SubtermCriterion (0ms).
| | – Problem 10 was processed with processor SubtermCriterion (0ms).
| – Problem 8 was processed with processor SubtermCriterion (1ms).
| | – Problem 11 was processed with processor SubtermCriterion (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(inf(X)) | → | mark#(X) | | mark#(take(X1, X2)) | → | mark#(X1) |
| mark#(eq(X1, X2)) | → | active#(eq(X1, X2)) | | active#(length(nil)) | → | mark#(0) |
| mark#(take(X1, X2)) | → | active#(take(mark(X1), mark(X2))) | | active#(eq(s(X), s(Y))) | → | eq#(X, Y) |
| active#(take(s(X), cons(Y, L))) | → | mark#(cons(Y, take(X, L))) | | length#(active(X)) | → | length#(X) |
| mark#(eq(X1, X2)) | → | eq#(X1, X2) | | active#(take(s(X), cons(Y, L))) | → | take#(X, L) |
| inf#(active(X)) | → | inf#(X) | | length#(mark(X)) | → | length#(X) |
| mark#(true) | → | active#(true) | | active#(length(cons(X, L))) | → | length#(L) |
| take#(X1, mark(X2)) | → | take#(X1, X2) | | mark#(inf(X)) | → | inf#(mark(X)) |
| mark#(s(X)) | → | active#(s(X)) | | active#(take(s(X), cons(Y, L))) | → | cons#(Y, take(X, L)) |
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | eq#(mark(X1), X2) | → | eq#(X1, X2) |
| active#(inf(X)) | → | cons#(X, inf(s(X))) | | mark#(false) | → | active#(false) |
| take#(mark(X1), X2) | → | take#(X1, X2) | | active#(length(cons(X, L))) | → | mark#(s(length(L))) |
| cons#(mark(X1), X2) | → | cons#(X1, X2) | | mark#(cons(X1, X2)) | → | cons#(X1, X2) |
| eq#(X1, mark(X2)) | → | eq#(X1, X2) | | active#(take(0, X)) | → | mark#(nil) |
| eq#(active(X1), X2) | → | eq#(X1, X2) | | eq#(X1, active(X2)) | → | eq#(X1, X2) |
| active#(eq(s(X), s(Y))) | → | mark#(eq(X, Y)) | | active#(eq(X, Y)) | → | mark#(false) |
| active#(inf(X)) | → | s#(X) | | mark#(nil) | → | active#(nil) |
| take#(X1, active(X2)) | → | take#(X1, X2) | | mark#(length(X)) | → | mark#(X) |
| mark#(inf(X)) | → | active#(inf(mark(X))) | | cons#(X1, mark(X2)) | → | cons#(X1, X2) |
| mark#(0) | → | active#(0) | | active#(inf(X)) | → | mark#(cons(X, inf(s(X)))) |
| mark#(length(X)) | → | length#(mark(X)) | | active#(inf(X)) | → | inf#(s(X)) |
| active#(length(cons(X, L))) | → | s#(length(L)) | | cons#(active(X1), X2) | → | cons#(X1, X2) |
| mark#(cons(X1, X2)) | → | active#(cons(X1, X2)) | | mark#(take(X1, X2)) | → | take#(mark(X1), mark(X2)) |
| mark#(s(X)) | → | s#(X) | | s#(mark(X)) | → | s#(X) |
| mark#(take(X1, X2)) | → | mark#(X2) | | s#(active(X)) | → | s#(X) |
| inf#(mark(X)) | → | inf#(X) | | mark#(length(X)) | → | active#(length(mark(X))) |
| active#(eq(0, 0)) | → | mark#(true) | | take#(active(X1), X2) | → | take#(X1, X2) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, inf, length, true, active, false, mark, eq, cons, nil
Strategy
The following SCCs where found
| length#(mark(X)) → length#(X) | length#(active(X)) → length#(X) |
| inf#(mark(X)) → inf#(X) | inf#(active(X)) → inf#(X) |
| mark#(inf(X)) → mark#(X) | active#(inf(X)) → mark#(cons(X, inf(s(X)))) |
| mark#(take(X1, X2)) → mark#(X1) | active#(length(cons(X, L))) → mark#(s(length(L))) |
| mark#(eq(X1, X2)) → active#(eq(X1, X2)) | mark#(take(X1, X2)) → active#(take(mark(X1), mark(X2))) |
| mark#(s(X)) → active#(s(X)) | mark#(cons(X1, X2)) → active#(cons(X1, X2)) |
| active#(take(s(X), cons(Y, L))) → mark#(cons(Y, take(X, L))) | active#(eq(s(X), s(Y))) → mark#(eq(X, Y)) |
| mark#(length(X)) → mark#(X) | mark#(take(X1, X2)) → mark#(X2) |
| mark#(inf(X)) → active#(inf(mark(X))) | mark#(length(X)) → active#(length(mark(X))) |
| cons#(X1, active(X2)) → cons#(X1, X2) | cons#(mark(X1), X2) → cons#(X1, X2) |
| cons#(active(X1), X2) → cons#(X1, X2) | cons#(X1, mark(X2)) → cons#(X1, X2) |
| s#(mark(X)) → s#(X) | s#(active(X)) → s#(X) |
| take#(mark(X1), X2) → take#(X1, X2) | take#(X1, active(X2)) → take#(X1, X2) |
| take#(X1, mark(X2)) → take#(X1, X2) | take#(active(X1), X2) → take#(X1, X2) |
| eq#(X1, active(X2)) → eq#(X1, X2) | eq#(active(X1), X2) → eq#(X1, X2) |
| eq#(mark(X1), X2) → eq#(X1, X2) | eq#(X1, mark(X2)) → eq#(X1, X2) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| s#(mark(X)) | → | s#(X) | | s#(active(X)) | → | s#(X) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, inf, length, true, active, false, mark, eq, cons, nil
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 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| inf#(mark(X)) | → | inf#(X) | | inf#(active(X)) | → | inf#(X) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, inf, length, true, active, false, mark, eq, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| inf#(mark(X)) | → | inf#(X) | | inf#(active(X)) | → | inf#(X) |
Problem 4: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| take#(mark(X1), X2) | → | take#(X1, X2) | | take#(X1, active(X2)) | → | take#(X1, X2) |
| take#(X1, mark(X2)) | → | take#(X1, X2) | | take#(active(X1), X2) | → | take#(X1, X2) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, inf, length, true, active, false, mark, eq, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| take#(mark(X1), X2) | → | take#(X1, X2) | | take#(active(X1), X2) | → | take#(X1, X2) |
Problem 9: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| take#(X1, active(X2)) | → | take#(X1, X2) | | take#(X1, mark(X2)) | → | take#(X1, X2) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, length, inf, false, active, true, mark, nil, cons, eq
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| take#(X1, active(X2)) | → | take#(X1, X2) | | take#(X1, mark(X2)) | → | take#(X1, X2) |
Problem 5: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| length#(mark(X)) | → | length#(X) | | length#(active(X)) | → | length#(X) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, inf, length, true, active, false, mark, eq, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| length#(mark(X)) | → | length#(X) | | length#(active(X)) | → | length#(X) |
Problem 6: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(inf(X)) | → | mark#(X) | | active#(inf(X)) | → | mark#(cons(X, inf(s(X)))) |
| active#(length(cons(X, L))) | → | mark#(s(length(L))) | | mark#(take(X1, X2)) | → | mark#(X1) |
| mark#(eq(X1, X2)) | → | active#(eq(X1, X2)) | | mark#(take(X1, X2)) | → | active#(take(mark(X1), mark(X2))) |
| mark#(s(X)) | → | active#(s(X)) | | mark#(cons(X1, X2)) | → | active#(cons(X1, X2)) |
| active#(take(s(X), cons(Y, L))) | → | mark#(cons(Y, take(X, L))) | | active#(eq(s(X), s(Y))) | → | mark#(eq(X, Y)) |
| mark#(take(X1, X2)) | → | mark#(X2) | | mark#(length(X)) | → | mark#(X) |
| mark#(inf(X)) | → | active#(inf(mark(X))) | | mark#(length(X)) | → | active#(length(mark(X))) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, inf, length, true, active, false, mark, eq, cons, nil
Strategy
Polynomial Interpretation
- 0: 1
- active(x): 2x + 1
- active#(x): 2x
- cons(x,y): 1
- eq(x,y): 1
- false: 1
- inf(x): 1
- length(x): 1
- mark(x): 3
- mark#(x): 2
- nil: 1
- s(x): 0
- take(x,y): 1
- true: 1
Standard Usable rules
| active(take(0, X)) | → | mark(nil) | | cons(active(X1), X2) | → | cons(X1, X2) |
| active(length(cons(X, L))) | → | mark(s(length(L))) | | inf(active(X)) | → | inf(X) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | length(mark(X)) | → | length(X) |
| mark(s(X)) | → | active(s(X)) | | inf(mark(X)) | → | inf(X) |
| active(length(nil)) | → | mark(0) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| mark(true) | → | active(true) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| mark(nil) | → | active(nil) | | mark(0) | → | active(0) |
| s(active(X)) | → | s(X) | | take(X1, active(X2)) | → | take(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | active(eq(X, Y)) | → | mark(false) |
| active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) | | mark(eq(X1, X2)) | → | active(eq(X1, X2)) |
| mark(length(X)) | → | active(length(mark(X))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(inf(X)) | → | active(inf(mark(X))) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| take(mark(X1), X2) | → | take(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| take(X1, mark(X2)) | → | take(X1, X2) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| mark(false) | → | active(false) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | length(active(X)) | → | length(X) |
| s(mark(X)) | → | s(X) | | eq(mark(X1), X2) | → | eq(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | active(eq(0, 0)) | → | mark(true) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(s(X)) | → | active#(s(X)) |
Problem 12: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(inf(X)) | → | mark#(X) | | active#(inf(X)) | → | mark#(cons(X, inf(s(X)))) |
| active#(length(cons(X, L))) | → | mark#(s(length(L))) | | mark#(take(X1, X2)) | → | mark#(X1) |
| mark#(eq(X1, X2)) | → | active#(eq(X1, X2)) | | mark#(take(X1, X2)) | → | active#(take(mark(X1), mark(X2))) |
| mark#(cons(X1, X2)) | → | active#(cons(X1, X2)) | | active#(take(s(X), cons(Y, L))) | → | mark#(cons(Y, take(X, L))) |
| active#(eq(s(X), s(Y))) | → | mark#(eq(X, Y)) | | mark#(take(X1, X2)) | → | mark#(X2) |
| mark#(length(X)) | → | mark#(X) | | mark#(inf(X)) | → | active#(inf(mark(X))) |
| mark#(length(X)) | → | active#(length(mark(X))) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, length, inf, false, active, true, mark, nil, cons, eq
Strategy
Polynomial Interpretation
- 0: 0
- active(x): x
- active#(x): 0
- cons(x,y): 0
- eq(x,y): 0
- false: 0
- inf(x): x
- length(x): 3x
- mark(x): x
- mark#(x): 3x
- nil: 1
- s(x): 0
- take(x,y): y + 2x + 1
- true: 0
Standard Usable rules
| active(take(0, X)) | → | mark(nil) | | cons(active(X1), X2) | → | cons(X1, X2) |
| active(length(cons(X, L))) | → | mark(s(length(L))) | | inf(active(X)) | → | inf(X) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | length(mark(X)) | → | length(X) |
| mark(s(X)) | → | active(s(X)) | | inf(mark(X)) | → | inf(X) |
| active(length(nil)) | → | mark(0) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| mark(true) | → | active(true) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| mark(nil) | → | active(nil) | | mark(0) | → | active(0) |
| s(active(X)) | → | s(X) | | take(X1, active(X2)) | → | take(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | active(eq(X, Y)) | → | mark(false) |
| active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) | | mark(eq(X1, X2)) | → | active(eq(X1, X2)) |
| mark(length(X)) | → | active(length(mark(X))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(inf(X)) | → | active(inf(mark(X))) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| take(mark(X1), X2) | → | take(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| take(X1, mark(X2)) | → | take(X1, X2) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| mark(false) | → | active(false) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | length(active(X)) | → | length(X) |
| s(mark(X)) | → | s(X) | | eq(mark(X1), X2) | → | eq(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | active(eq(0, 0)) | → | mark(true) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(take(X1, X2)) | → | mark#(X1) | | mark#(take(X1, X2)) | → | active#(take(mark(X1), mark(X2))) |
| mark#(take(X1, X2)) | → | mark#(X2) |
Problem 13: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(inf(X)) | → | mark#(X) | | active#(take(s(X), cons(Y, L))) | → | mark#(cons(Y, take(X, L))) |
| active#(inf(X)) | → | mark#(cons(X, inf(s(X)))) | | active#(eq(s(X), s(Y))) | → | mark#(eq(X, Y)) |
| active#(length(cons(X, L))) | → | mark#(s(length(L))) | | mark#(length(X)) | → | mark#(X) |
| mark#(eq(X1, X2)) | → | active#(eq(X1, X2)) | | mark#(inf(X)) | → | active#(inf(mark(X))) |
| mark#(length(X)) | → | active#(length(mark(X))) | | mark#(cons(X1, X2)) | → | active#(cons(X1, X2)) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, inf, length, true, active, false, mark, eq, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 0
- active#(x): 2x
- cons(x,y): 0
- eq(x,y): 0
- false: 0
- inf(x): 0
- length(x): 0
- mark(x): 2x
- mark#(x): 0
- nil: 0
- s(x): 0
- take(x,y): 1
- true: 0
Standard Usable rules
| active(take(0, X)) | → | mark(nil) | | cons(active(X1), X2) | → | cons(X1, X2) |
| active(length(cons(X, L))) | → | mark(s(length(L))) | | inf(active(X)) | → | inf(X) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | length(mark(X)) | → | length(X) |
| mark(s(X)) | → | active(s(X)) | | inf(mark(X)) | → | inf(X) |
| active(length(nil)) | → | mark(0) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| mark(true) | → | active(true) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| mark(nil) | → | active(nil) | | mark(0) | → | active(0) |
| s(active(X)) | → | s(X) | | take(X1, active(X2)) | → | take(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | active(eq(X, Y)) | → | mark(false) |
| active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) | | mark(eq(X1, X2)) | → | active(eq(X1, X2)) |
| mark(length(X)) | → | active(length(mark(X))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(inf(X)) | → | active(inf(mark(X))) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| take(mark(X1), X2) | → | take(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| take(X1, mark(X2)) | → | take(X1, X2) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| mark(false) | → | active(false) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | length(active(X)) | → | length(X) |
| s(mark(X)) | → | s(X) | | eq(mark(X1), X2) | → | eq(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | active(eq(0, 0)) | → | mark(true) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| active#(take(s(X), cons(Y, L))) | → | mark#(cons(Y, take(X, L))) |
Problem 14: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(inf(X)) | → | mark#(X) | | active#(inf(X)) | → | mark#(cons(X, inf(s(X)))) |
| active#(length(cons(X, L))) | → | mark#(s(length(L))) | | active#(eq(s(X), s(Y))) | → | mark#(eq(X, Y)) |
| mark#(length(X)) | → | mark#(X) | | mark#(eq(X1, X2)) | → | active#(eq(X1, X2)) |
| mark#(inf(X)) | → | active#(inf(mark(X))) | | mark#(length(X)) | → | active#(length(mark(X))) |
| mark#(cons(X1, X2)) | → | active#(cons(X1, X2)) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, length, inf, false, active, true, mark, nil, cons, eq
Strategy
Polynomial Interpretation
- 0: 3
- active(x): 0
- active#(x): 2x
- cons(x,y): 0
- eq(x,y): 1
- false: 1
- inf(x): 1
- length(x): 1
- mark(x): 0
- mark#(x): 2
- nil: 3
- s(x): 3
- take(x,y): 3
- true: 3
Standard Usable rules
| active(take(0, X)) | → | mark(nil) | | cons(active(X1), X2) | → | cons(X1, X2) |
| active(length(cons(X, L))) | → | mark(s(length(L))) | | inf(active(X)) | → | inf(X) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(s(X)) | → | active(s(X)) |
| inf(mark(X)) | → | inf(X) | | length(mark(X)) | → | length(X) |
| active(length(nil)) | → | mark(0) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| mark(true) | → | active(true) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| mark(nil) | → | active(nil) | | mark(0) | → | active(0) |
| s(active(X)) | → | s(X) | | take(X1, active(X2)) | → | take(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | active(eq(X, Y)) | → | mark(false) |
| active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) | | mark(eq(X1, X2)) | → | active(eq(X1, X2)) |
| mark(length(X)) | → | active(length(mark(X))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(inf(X)) | → | active(inf(mark(X))) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| take(mark(X1), X2) | → | take(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| take(X1, mark(X2)) | → | take(X1, X2) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| mark(false) | → | active(false) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | s(mark(X)) | → | s(X) |
| length(active(X)) | → | length(X) | | take(active(X1), X2) | → | take(X1, X2) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | active(eq(0, 0)) | → | mark(true) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(cons(X1, X2)) | → | active#(cons(X1, X2)) |
Problem 15: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| mark#(inf(X)) | → | mark#(X) | | active#(inf(X)) | → | mark#(cons(X, inf(s(X)))) |
| active#(eq(s(X), s(Y))) | → | mark#(eq(X, Y)) | | active#(length(cons(X, L))) | → | mark#(s(length(L))) |
| mark#(length(X)) | → | mark#(X) | | mark#(eq(X1, X2)) | → | active#(eq(X1, X2)) |
| mark#(inf(X)) | → | active#(inf(mark(X))) | | mark#(length(X)) | → | active#(length(mark(X))) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, inf, length, true, active, false, mark, eq, cons, nil
Strategy
Polynomial Interpretation
- 0: 1
- active(x): x
- active#(x): 2
- cons(x,y): y
- eq(x,y): 2
- false: 0
- inf(x): 2x + 2
- length(x): 2x + 2
- mark(x): x
- mark#(x): x
- nil: 0
- s(x): 0
- take(x,y): y
- true: 1
Standard Usable rules
| active(take(0, X)) | → | mark(nil) | | cons(active(X1), X2) | → | cons(X1, X2) |
| active(length(cons(X, L))) | → | mark(s(length(L))) | | inf(active(X)) | → | inf(X) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(s(X)) | → | active(s(X)) |
| inf(mark(X)) | → | inf(X) | | length(mark(X)) | → | length(X) |
| active(length(nil)) | → | mark(0) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| mark(true) | → | active(true) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| mark(nil) | → | active(nil) | | mark(0) | → | active(0) |
| s(active(X)) | → | s(X) | | take(X1, active(X2)) | → | take(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | active(eq(X, Y)) | → | mark(false) |
| active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) | | mark(eq(X1, X2)) | → | active(eq(X1, X2)) |
| mark(length(X)) | → | active(length(mark(X))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(inf(X)) | → | active(inf(mark(X))) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| take(mark(X1), X2) | → | take(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| take(X1, mark(X2)) | → | take(X1, X2) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| mark(false) | → | active(false) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | s(mark(X)) | → | s(X) |
| length(active(X)) | → | length(X) | | take(active(X1), X2) | → | take(X1, X2) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | active(eq(0, 0)) | → | mark(true) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(inf(X)) | → | mark#(X) | | active#(length(cons(X, L))) | → | mark#(s(length(L))) |
| mark#(length(X)) | → | mark#(X) |
Problem 16: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| active#(inf(X)) | → | mark#(cons(X, inf(s(X)))) | | active#(eq(s(X), s(Y))) | → | mark#(eq(X, Y)) |
| mark#(eq(X1, X2)) | → | active#(eq(X1, X2)) | | mark#(inf(X)) | → | active#(inf(mark(X))) |
| mark#(length(X)) | → | active#(length(mark(X))) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, length, inf, false, active, true, mark, nil, cons, eq
Strategy
Polynomial Interpretation
- 0: 1
- active(x): x
- active#(x): x
- cons(x,y): 0
- eq(x,y): 0
- false: 0
- inf(x): 1
- length(x): x + 1
- mark(x): x
- mark#(x): 2x
- nil: 0
- s(x): 1
- take(x,y): 0
- true: 0
Standard Usable rules
| active(take(0, X)) | → | mark(nil) | | cons(active(X1), X2) | → | cons(X1, X2) |
| active(length(cons(X, L))) | → | mark(s(length(L))) | | inf(active(X)) | → | inf(X) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(s(X)) | → | active(s(X)) |
| inf(mark(X)) | → | inf(X) | | length(mark(X)) | → | length(X) |
| active(length(nil)) | → | mark(0) | | cons(X1, mark(X2)) | → | cons(X1, X2) |
| mark(true) | → | active(true) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| mark(nil) | → | active(nil) | | mark(0) | → | active(0) |
| s(active(X)) | → | s(X) | | take(X1, active(X2)) | → | take(X1, X2) |
| cons(X1, active(X2)) | → | cons(X1, X2) | | active(eq(X, Y)) | → | mark(false) |
| active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) | | mark(eq(X1, X2)) | → | active(eq(X1, X2)) |
| mark(length(X)) | → | active(length(mark(X))) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(inf(X)) | → | active(inf(mark(X))) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| take(mark(X1), X2) | → | take(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| take(X1, mark(X2)) | → | take(X1, X2) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| mark(false) | → | active(false) | | cons(mark(X1), X2) | → | cons(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | s(mark(X)) | → | s(X) |
| length(active(X)) | → | length(X) | | take(active(X1), X2) | → | take(X1, X2) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | active(eq(0, 0)) | → | mark(true) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| active#(inf(X)) | → | mark#(cons(X, inf(s(X)))) | | mark#(inf(X)) | → | active#(inf(mark(X))) |
| mark#(length(X)) | → | active#(length(mark(X))) |
Problem 17: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| active#(eq(s(X), s(Y))) | → | mark#(eq(X, Y)) | | mark#(eq(X1, X2)) | → | active#(eq(X1, X2)) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, inf, length, true, active, false, mark, eq, cons, nil
Strategy
Polynomial Interpretation
- 0: 0
- active(x): 3x + 1
- active#(x): 2x
- cons(x,y): 0
- eq(x,y): y
- false: 0
- inf(x): 0
- length(x): 0
- mark(x): 3x
- mark#(x): 2x + 2
- nil: 0
- s(x): x + 1
- take(x,y): 0
- true: 0
Standard Usable rules
| eq(X1, active(X2)) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(mark(X1), X2) | → | eq(X1, X2) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(eq(X1, X2)) | → | active#(eq(X1, X2)) |
Problem 18: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| active#(eq(s(X), s(Y))) | → | mark#(eq(X, Y)) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, length, inf, false, active, true, mark, nil, cons, eq
Strategy
There are no SCCs!
Problem 7: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(mark(X1), X2) | → | cons#(X1, X2) |
| cons#(active(X1), X2) | → | cons#(X1, X2) | | cons#(X1, mark(X2)) | → | cons#(X1, X2) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, inf, length, true, active, false, mark, eq, cons, nil
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) |
Problem 10: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(X1, mark(X2)) | → | cons#(X1, X2) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, length, inf, false, active, true, mark, nil, cons, eq
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| cons#(X1, active(X2)) | → | cons#(X1, X2) | | cons#(X1, mark(X2)) | → | cons#(X1, X2) |
Problem 8: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| eq#(X1, active(X2)) | → | eq#(X1, X2) | | eq#(active(X1), X2) | → | eq#(X1, X2) |
| eq#(mark(X1), X2) | → | eq#(X1, X2) | | eq#(X1, mark(X2)) | → | eq#(X1, X2) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, inf, length, true, active, false, mark, eq, cons, nil
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| eq#(active(X1), X2) | → | eq#(X1, X2) | | eq#(mark(X1), X2) | → | eq#(X1, X2) |
Problem 11: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| eq#(X1, active(X2)) | → | eq#(X1, X2) | | eq#(X1, mark(X2)) | → | eq#(X1, X2) |
Rewrite Rules
| active(eq(0, 0)) | → | mark(true) | | active(eq(s(X), s(Y))) | → | mark(eq(X, Y)) |
| active(eq(X, Y)) | → | mark(false) | | active(inf(X)) | → | mark(cons(X, inf(s(X)))) |
| active(take(0, X)) | → | mark(nil) | | active(take(s(X), cons(Y, L))) | → | mark(cons(Y, take(X, L))) |
| active(length(nil)) | → | mark(0) | | active(length(cons(X, L))) | → | mark(s(length(L))) |
| mark(eq(X1, X2)) | → | active(eq(X1, X2)) | | mark(0) | → | active(0) |
| mark(true) | → | active(true) | | mark(s(X)) | → | active(s(X)) |
| mark(false) | → | active(false) | | mark(inf(X)) | → | active(inf(mark(X))) |
| mark(cons(X1, X2)) | → | active(cons(X1, X2)) | | mark(take(X1, X2)) | → | active(take(mark(X1), mark(X2))) |
| mark(nil) | → | active(nil) | | mark(length(X)) | → | active(length(mark(X))) |
| eq(mark(X1), X2) | → | eq(X1, X2) | | eq(X1, mark(X2)) | → | eq(X1, X2) |
| eq(active(X1), X2) | → | eq(X1, X2) | | eq(X1, active(X2)) | → | eq(X1, X2) |
| s(mark(X)) | → | s(X) | | s(active(X)) | → | s(X) |
| inf(mark(X)) | → | inf(X) | | inf(active(X)) | → | inf(X) |
| 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) |
| take(mark(X1), X2) | → | take(X1, X2) | | take(X1, mark(X2)) | → | take(X1, X2) |
| take(active(X1), X2) | → | take(X1, X2) | | take(X1, active(X2)) | → | take(X1, X2) |
| length(mark(X)) | → | length(X) | | length(active(X)) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: 0, s, take, length, inf, false, active, true, mark, nil, cons, eq
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| eq#(X1, active(X2)) | → | eq#(X1, X2) | | eq#(X1, mark(X2)) | → | eq#(X1, X2) |