The TRS could be proven terminating. The proof took 15 ms.
Problem 1 was processed with processor DependencyGraph (4ms).
| g#(x) | → | h#(x) | f#(x, y) | → | U01#(x, y, x) | |
| g#(x) | → | U11#(h(x), x) |
| f(x, y) | → | U01(x, y, x) | U01(z, y, x) | → | z | |
| g(x) | → | U11(h(x), x) | U11(d, x) | → | b | |
| h(c) | → | d |
Termination of terms over the following signature is verified: f, g, d, b, c, h
Context-sensitive strategy:
μ(d) = μ(b) = μ(c) = μ(T) = ∅
μ(g) = μ(U11#) = μ(h#) = μ(g#) = μ(h) = μ(U01) = μ(U11) = μ(U01#) = {1}
μ(f) = μ(f#) = {1, 2}