The TRS could be proven terminating. The proof took 98 ms.
Problem 1 was processed with processor PolynomialLinearRange4iUR (79ms).
| f#(s(x), y, y) | → | f#(y, x, s(x)) |
| f(s(x), y, y) | → | f(y, x, s(x)) |
Termination of terms over the following signature is verified: f, s
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f#(s(x), y, y) | → | f#(y, x, s(x)) |