Term Rewriting System R:
[]
f(g(f(a), h(a, f(a)))) -> f(h(g(f(a), a), g(f(a), f(a))))

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

F(g(f(a), h(a, f(a)))) -> F(h(g(f(a), a), g(f(a), f(a))))

R contains no SCCs.

Innermost Termination of R successfully shown.
Duration:
0:00 minutes