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