The TRS could be proven terminating. The proof took 157 ms.
Problem 1 was processed with processor PolynomialLinearRange4iUR (98ms).
| f#(x, s(y)) | → | f#(y, x) | f#(s(x), y) | → | f#(x, s(x)) |
| f(s(x), y) | → | f(x, s(x)) | f(x, s(y)) | → | f(y, 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#(x, s(y)) | → | f#(y, x) | f#(s(x), y) | → | f#(x, s(x)) |