The TRS could be proven terminating. The proof took 16 ms.
Problem 1 was processed with processor DependencyGraph (6ms).
| f#(g(i(a, b, b'), c), d) | → | f#(.(b, c), d') | f#(g(h(a, b), c), d) | → | f#(c, d') | |
| f#(g(h(a, b), c), d) | → | f#(.(b, g(h(a, b), c)), d) | f#(g(i(a, b, b'), c), d) | → | f#(.(b', c), d') |
| f(g(i(a, b, b'), c), d) | → | if(e, f(.(b, c), d'), f(.(b', c), d')) | f(g(h(a, b), c), d) | → | if(e, f(.(b, g(h(a, b), c)), d), f(c, d')) |
Termination of terms over the following signature is verified: f, g, d, e, b, c, a, ., h, i, if, b', d'