YES
The TRS could be proven terminating. The proof took 880 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (17ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (813ms).
| – Problem 3 was processed with processor SubtermCriterion (3ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| rev2#(X, cons(Y, L)) | → | rev#(cons(X, rev(rev2(Y, L)))) | | rev#(cons(X, L)) | → | rev1#(X, L) |
| rev#(cons(X, L)) | → | rev2#(X, L) | | rev2#(X, cons(Y, L)) | → | rev#(rev2(Y, L)) |
| rev2#(X, cons(Y, L)) | → | rev2#(Y, L) | | rev1#(X, cons(Y, L)) | → | rev1#(Y, L) |
Rewrite Rules
| rev1(0, nil) | → | 0 | | rev1(s(X), nil) | → | s(X) |
| rev1(X, cons(Y, L)) | → | rev1(Y, L) | | rev(nil) | → | nil |
| rev(cons(X, L)) | → | cons(rev1(X, L), rev2(X, L)) | | rev2(X, nil) | → | nil |
| rev2(X, cons(Y, L)) | → | rev(cons(X, rev(rev2(Y, L)))) |
Original Signature
Termination of terms over the following signature is verified: rev1, rev, 0, rev2, s, nil, cons
Strategy
The following SCCs where found
| rev2#(X, cons(Y, L)) → rev#(cons(X, rev(rev2(Y, L)))) | rev#(cons(X, L)) → rev2#(X, L) |
| rev2#(X, cons(Y, L)) → rev2#(Y, L) | rev2#(X, cons(Y, L)) → rev#(rev2(Y, L)) |
| rev1#(X, cons(Y, L)) → rev1#(Y, L) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| rev2#(X, cons(Y, L)) | → | rev#(cons(X, rev(rev2(Y, L)))) | | rev#(cons(X, L)) | → | rev2#(X, L) |
| rev2#(X, cons(Y, L)) | → | rev2#(Y, L) | | rev2#(X, cons(Y, L)) | → | rev#(rev2(Y, L)) |
Rewrite Rules
| rev1(0, nil) | → | 0 | | rev1(s(X), nil) | → | s(X) |
| rev1(X, cons(Y, L)) | → | rev1(Y, L) | | rev(nil) | → | nil |
| rev(cons(X, L)) | → | cons(rev1(X, L), rev2(X, L)) | | rev2(X, nil) | → | nil |
| rev2(X, cons(Y, L)) | → | rev(cons(X, rev(rev2(Y, L)))) |
Original Signature
Termination of terms over the following signature is verified: rev1, rev, 0, rev2, s, nil, cons
Strategy
Polynomial Interpretation
- 0: 2
- cons(x,y): y + 1
- nil: 0
- rev(x): x
- rev#(x): 2x
- rev1(x,y): 2
- rev2(x,y): y
- rev2#(x,y): 2y + 1
- s(x): 2x + 3
Improved Usable rules
| rev2(X, nil) | → | nil | | rev2(X, cons(Y, L)) | → | rev(cons(X, rev(rev2(Y, L)))) |
| rev(cons(X, L)) | → | cons(rev1(X, L), rev2(X, L)) | | rev(nil) | → | nil |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| rev2#(X, cons(Y, L)) | → | rev#(cons(X, rev(rev2(Y, L)))) | | rev#(cons(X, L)) | → | rev2#(X, L) |
| rev2#(X, cons(Y, L)) | → | rev#(rev2(Y, L)) | | rev2#(X, cons(Y, L)) | → | rev2#(Y, L) |
Problem 3: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| rev1#(X, cons(Y, L)) | → | rev1#(Y, L) |
Rewrite Rules
| rev1(0, nil) | → | 0 | | rev1(s(X), nil) | → | s(X) |
| rev1(X, cons(Y, L)) | → | rev1(Y, L) | | rev(nil) | → | nil |
| rev(cons(X, L)) | → | cons(rev1(X, L), rev2(X, L)) | | rev2(X, nil) | → | nil |
| rev2(X, cons(Y, L)) | → | rev(cons(X, rev(rev2(Y, L)))) |
Original Signature
Termination of terms over the following signature is verified: rev1, rev, 0, rev2, s, nil, cons
Strategy
Projection
The following projection was used:
Thus, the following dependency pairs are removed:
| rev1#(X, cons(Y, L)) | → | rev1#(Y, L) |