YES
The TRS could be proven terminating. The proof took 19 ms.
Problem 1 was processed with processor DependencyGraph (2ms).
f#(X, X) | → | f#(a, b) | T(b) | → | b# |
f(X, X) | → | f(a, b) | b | → | a |
Termination of terms over the following signature is verified: f, b, a
Context-sensitive strategy:
μ(T) = μ(b) = μ(a) = μ(b#) = ∅
μ(f) = μ(f#) = {1}