The TRS could be proven terminating. The proof took 15 ms.
Problem 1 was processed with processor DependencyGraph (2ms).
| 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:
μ(T) = μ(g) = μ(a) = ∅
μ(f) = μ(f#) = {1}