The TRS could be proven terminating. The proof took 108 ms.
Problem 1 was processed with processor DependencyGraph (3ms). | – Problem 2 was processed with processor PolynomialLinearRange4 (55ms).
| T(g(x_1)) | → | T(x_1) | f#(f(a)) | → | f#(g(f(a))) | |
| T(f(a)) | → | f#(a) |
| f(f(a)) | → | f(g(f(a))) |
Termination of terms over the following signature is verified: f, g, a
Context-sensitive strategy:
μ(f) = μ(T) = μ(f#) = μ(a) = ∅
μ(g) = {1}
| T(g(x_1)) → T(x_1) |
| T(g(x_1)) | → | T(x_1) |
| f(f(a)) | → | f(g(f(a))) |
Termination of terms over the following signature is verified: f, g, a
Context-sensitive strategy:
μ(f) = μ(T) = μ(f#) = μ(a) = ∅
μ(g) = {1}
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| T(g(x_1)) | → | T(x_1) |