YES
The TRS could be proven terminating. The proof took 165 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (74ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor SubtermCriterion (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| mark#(inf(X)) | → | mark#(X) | | mark#(take(X1, X2)) | → | mark#(X1) |
| a__eq#(s(X), s(Y)) | → | a__eq#(X, Y) | | mark#(eq(X1, X2)) | → | a__eq#(X1, X2) |
| mark#(take(X1, X2)) | → | a__take#(mark(X1), mark(X2)) | | mark#(take(X1, X2)) | → | mark#(X2) |
| mark#(length(X)) | → | mark#(X) | | mark#(inf(X)) | → | a__inf#(mark(X)) |
| mark#(length(X)) | → | a__length#(mark(X)) |
Rewrite Rules
| a__eq(0, 0) | → | true | | a__eq(s(X), s(Y)) | → | a__eq(X, Y) |
| a__eq(X, Y) | → | false | | a__inf(X) | → | cons(X, inf(s(X))) |
| a__take(0, X) | → | nil | | a__take(s(X), cons(Y, L)) | → | cons(Y, take(X, L)) |
| a__length(nil) | → | 0 | | a__length(cons(X, L)) | → | s(length(L)) |
| mark(eq(X1, X2)) | → | a__eq(X1, X2) | | mark(inf(X)) | → | a__inf(mark(X)) |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(0) | → | 0 | | mark(true) | → | true |
| mark(s(X)) | → | s(X) | | mark(false) | → | false |
| mark(cons(X1, X2)) | → | cons(X1, X2) | | mark(nil) | → | nil |
| a__eq(X1, X2) | → | eq(X1, X2) | | a__inf(X) | → | inf(X) |
| a__take(X1, X2) | → | take(X1, X2) | | a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__take, a__length, inf, true, mark, a__eq, 0, s, a__inf, take, length, false, nil, cons, eq
Strategy
The following SCCs where found
| mark#(inf(X)) → mark#(X) | mark#(take(X1, X2)) → mark#(X1) |
| mark#(take(X1, X2)) → mark#(X2) | mark#(length(X)) → mark#(X) |
| a__eq#(s(X), s(Y)) → a__eq#(X, Y) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| a__eq#(s(X), s(Y)) | → | a__eq#(X, Y) |
Rewrite Rules
| a__eq(0, 0) | → | true | | a__eq(s(X), s(Y)) | → | a__eq(X, Y) |
| a__eq(X, Y) | → | false | | a__inf(X) | → | cons(X, inf(s(X))) |
| a__take(0, X) | → | nil | | a__take(s(X), cons(Y, L)) | → | cons(Y, take(X, L)) |
| a__length(nil) | → | 0 | | a__length(cons(X, L)) | → | s(length(L)) |
| mark(eq(X1, X2)) | → | a__eq(X1, X2) | | mark(inf(X)) | → | a__inf(mark(X)) |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(0) | → | 0 | | mark(true) | → | true |
| mark(s(X)) | → | s(X) | | mark(false) | → | false |
| mark(cons(X1, X2)) | → | cons(X1, X2) | | mark(nil) | → | nil |
| a__eq(X1, X2) | → | eq(X1, X2) | | a__inf(X) | → | inf(X) |
| a__take(X1, X2) | → | take(X1, X2) | | a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__take, a__length, inf, true, mark, a__eq, 0, s, a__inf, take, length, false, nil, cons, eq
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| a__eq#(s(X), s(Y)) | → | a__eq#(X, Y) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| mark#(inf(X)) | → | mark#(X) | | mark#(take(X1, X2)) | → | mark#(X1) |
| mark#(take(X1, X2)) | → | mark#(X2) | | mark#(length(X)) | → | mark#(X) |
Rewrite Rules
| a__eq(0, 0) | → | true | | a__eq(s(X), s(Y)) | → | a__eq(X, Y) |
| a__eq(X, Y) | → | false | | a__inf(X) | → | cons(X, inf(s(X))) |
| a__take(0, X) | → | nil | | a__take(s(X), cons(Y, L)) | → | cons(Y, take(X, L)) |
| a__length(nil) | → | 0 | | a__length(cons(X, L)) | → | s(length(L)) |
| mark(eq(X1, X2)) | → | a__eq(X1, X2) | | mark(inf(X)) | → | a__inf(mark(X)) |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | | mark(length(X)) | → | a__length(mark(X)) |
| mark(0) | → | 0 | | mark(true) | → | true |
| mark(s(X)) | → | s(X) | | mark(false) | → | false |
| mark(cons(X1, X2)) | → | cons(X1, X2) | | mark(nil) | → | nil |
| a__eq(X1, X2) | → | eq(X1, X2) | | a__inf(X) | → | inf(X) |
| a__take(X1, X2) | → | take(X1, X2) | | a__length(X) | → | length(X) |
Original Signature
Termination of terms over the following signature is verified: a__take, a__length, inf, true, mark, a__eq, 0, s, a__inf, take, length, false, nil, cons, eq
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| mark#(inf(X)) | → | mark#(X) | | mark#(take(X1, X2)) | → | mark#(X1) |
| mark#(length(X)) | → | mark#(X) | | mark#(take(X1, X2)) | → | mark#(X2) |