YES
The TRS could be proven terminating. The proof took 17 ms.
Problem 1 was processed with processor DependencyGraph (3ms).
g#(a, x) | → | f#(b, x) | f#(a, x) | → | f#(b, x) | |
f#(a, x) | → | g#(a, x) |
f(a, x) | → | g(a, x) | g(a, x) | → | f(b, x) | |
f(a, x) | → | f(b, x) |
Termination of terms over the following signature is verified: f, g, b, a