The TRS could be proven terminating. The proof took 38 ms.
Problem 1 was processed with processor DependencyGraph (28ms).
| f#(x, y) | → | g2#(y, y, x) | g1#(y, x, x) | → | h#(x, y) | |
| f#(x, y) | → | g1#(x, x, y) | g1#(x, x, y) | → | h#(x, y) | |
| f#(x, y) | → | g1#(y, x, x) | g2#(x, y, y) | → | h#(x, y) | |
| f#(x, y) | → | g2#(x, y, y) | g2#(y, y, x) | → | h#(x, y) |
| f(x, y) | → | g1(x, x, y) | f(x, y) | → | g1(y, x, x) | |
| f(x, y) | → | g2(x, y, y) | f(x, y) | → | g2(y, y, x) | |
| g1(x, x, y) | → | h(x, y) | g1(y, x, x) | → | h(x, y) | |
| g2(x, y, y) | → | h(x, y) | g2(y, y, x) | → | h(x, y) | |
| h(x, x) | → | x |
Termination of terms over the following signature is verified: f, g2, g1, h