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