YES
The TRS could be proven terminating. The proof took 545 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (12ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (478ms).
| | – Problem 4 was processed with processor DependencyGraph (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| rev2#(x, cons(y, l)) | → | rev2#(y, l) | | rev1#(x, cons(y, l)) | → | rev1#(y, l) |
| rev#(cons(x, l)) | → | rev2#(x, l) | | rev#(cons(x, l)) | → | rev1#(x, l) |
| rev2#(x, cons(y, l)) | → | rev#(cons(x, rev2(y, l))) |
Rewrite Rules
| rev(nil) | → | nil | | rev(cons(x, l)) | → | cons(rev1(x, l), rev2(x, l)) |
| rev1(0, nil) | → | 0 | | rev1(s(x), nil) | → | s(x) |
| rev1(x, cons(y, l)) | → | rev1(y, l) | | rev2(x, nil) | → | nil |
| rev2(x, cons(y, l)) | → | rev(cons(x, rev2(y, l))) |
Original Signature
Termination of terms over the following signature is verified: rev, rev1, rev2, 0, s, nil, cons
Strategy
The following SCCs where found
| rev1#(x, cons(y, l)) → rev1#(y, l) |
| rev2#(x, cons(y, l)) → rev2#(y, l) | rev#(cons(x, l)) → rev2#(x, l) |
| rev2#(x, cons(y, l)) → rev#(cons(x, rev2(y, l))) |
Problem 2: SubtermCriterion
Dependency Pair Problem
Dependency Pairs
| rev1#(x, cons(y, l)) | → | rev1#(y, l) |
Rewrite Rules
| rev(nil) | → | nil | | rev(cons(x, l)) | → | cons(rev1(x, l), rev2(x, l)) |
| rev1(0, nil) | → | 0 | | rev1(s(x), nil) | → | s(x) |
| rev1(x, cons(y, l)) | → | rev1(y, l) | | rev2(x, nil) | → | nil |
| rev2(x, cons(y, l)) | → | rev(cons(x, rev2(y, l))) |
Original Signature
Termination of terms over the following signature is verified: rev, rev1, rev2, 0, 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) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| rev2#(x, cons(y, l)) | → | rev2#(y, l) | | rev#(cons(x, l)) | → | rev2#(x, l) |
| rev2#(x, cons(y, l)) | → | rev#(cons(x, rev2(y, l))) |
Rewrite Rules
| rev(nil) | → | nil | | rev(cons(x, l)) | → | cons(rev1(x, l), rev2(x, l)) |
| rev1(0, nil) | → | 0 | | rev1(s(x), nil) | → | s(x) |
| rev1(x, cons(y, l)) | → | rev1(y, l) | | rev2(x, nil) | → | nil |
| rev2(x, cons(y, l)) | → | rev(cons(x, rev2(y, l))) |
Original Signature
Termination of terms over the following signature is verified: rev, rev1, rev2, 0, s, nil, cons
Strategy
Polynomial Interpretation
- 0: 0
- cons(x,y): 2y + 2
- nil: 0
- rev(x): x
- rev#(x): x
- rev1(x,y): 0
- rev2(x,y): y
- rev2#(x,y): y
- s(x): 3x + 3
Improved Usable rules
| rev2(x, nil) | → | nil | | rev(nil) | → | nil |
| rev(cons(x, l)) | → | cons(rev1(x, l), rev2(x, l)) | | rev2(x, cons(y, l)) | → | rev(cons(x, rev2(y, l))) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| rev2#(x, cons(y, l)) | → | rev2#(y, l) | | rev#(cons(x, l)) | → | rev2#(x, l) |
Problem 4: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| rev2#(x, cons(y, l)) | → | rev#(cons(x, rev2(y, l))) |
Rewrite Rules
| rev(nil) | → | nil | | rev(cons(x, l)) | → | cons(rev1(x, l), rev2(x, l)) |
| rev1(0, nil) | → | 0 | | rev1(s(x), nil) | → | s(x) |
| rev1(x, cons(y, l)) | → | rev1(y, l) | | rev2(x, nil) | → | nil |
| rev2(x, cons(y, l)) | → | rev(cons(x, rev2(y, l))) |
Original Signature
Termination of terms over the following signature is verified: rev1, rev, 0, rev2, s, cons, nil
Strategy
There are no SCCs!