YES
The TRS could be proven terminating. The proof took 694 ms.
The following DP Processors were used
Problem 1 was processed with processor PolynomialLinearRange4iUR (393ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (241ms).
Problem 1: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| -#(-(neg(x), neg(x)), -(neg(y), neg(y))) | → | -#(-(x, y), -(x, y)) | | -#(-(neg(x), neg(x)), -(neg(y), neg(y))) | → | -#(x, y) |
Rewrite Rules
| -(-(neg(x), neg(x)), -(neg(y), neg(y))) | → | -(-(x, y), -(x, y)) |
Original Signature
Termination of terms over the following signature is verified: neg, -
Strategy
Polynomial Interpretation
- -(x,y): 2y + 1
- -#(x,y): y
- neg(x): x
Improved Usable rules
| -(-(neg(x), neg(x)), -(neg(y), neg(y))) | → | -(-(x, y), -(x, y)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| -#(-(neg(x), neg(x)), -(neg(y), neg(y))) | → | -#(x, y) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| -#(-(neg(x), neg(x)), -(neg(y), neg(y))) | → | -#(-(x, y), -(x, y)) |
Rewrite Rules
| -(-(neg(x), neg(x)), -(neg(y), neg(y))) | → | -(-(x, y), -(x, y)) |
Original Signature
Termination of terms over the following signature is verified: neg, -
Strategy
Polynomial Interpretation
- -(x,y): y
- -#(x,y): y
- neg(x): 2x + 2
Improved Usable rules
| -(-(neg(x), neg(x)), -(neg(y), neg(y))) | → | -(-(x, y), -(x, y)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| -#(-(neg(x), neg(x)), -(neg(y), neg(y))) | → | -#(-(x, y), -(x, y)) |