The TRS could be proven terminating. The proof took 123 ms.
Problem 1 was processed with processor PolynomialLinearRange4iUR (80ms).
| f#(s(x), y, y) | → | f#(y, x, s(x)) |
| g(x, y) | → | x | g(x, y) | → | y | |
| f(s(x), y, y) | → | f(y, x, s(x)) |
Termination of terms over the following signature is verified: f, g, 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)) |