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