The TRS could be proven terminating. The proof took 129 ms.
Problem 1 was processed with processor DependencyGraph (6ms). | – Problem 2 was processed with processor PolynomialLinearRange4 (75ms). | | – Problem 3 was processed with processor PolynomialLinearRange4 (14ms).
| T(f(g(f(a)))) | → | f#(g(f(a))) | T(g(x_1)) | → | T(x_1) | |
| T(f(x_1)) | → | T(x_1) | T(f(a)) | → | f#(a) |
| f(f(a)) | → | c(f(g(f(a)))) |
Termination of terms over the following signature is verified: f, g, c, a
Context-sensitive strategy:
μ(T) = μ(c) = μ(a) = ∅
μ(f) = μ(g) = μ(f#) = {1}
| T(g(x_1)) → T(x_1) | T(f(x_1)) → T(x_1) |
| T(g(x_1)) | → | T(x_1) | T(f(x_1)) | → | T(x_1) |
| f(f(a)) | → | c(f(g(f(a)))) |
Termination of terms over the following signature is verified: f, g, c, a
Context-sensitive strategy:
μ(T) = μ(c) = μ(a) = ∅
μ(f) = μ(g) = μ(f#) = {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(f(x_1)) | → | T(x_1) |
| T(g(x_1)) | → | T(x_1) |
| f(f(a)) | → | c(f(g(f(a)))) |
Termination of terms over the following signature is verified: f, g, c, a
Context-sensitive strategy:
μ(T) = μ(c) = μ(a) = ∅
μ(f) = μ(g) = μ(f#) = {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) |