Term Rewriting System R:
[x]
a(b(a(b(x)))) -> b(a(b(a(a(b(x))))))

Innermost Termination of R to be shown.



   TRS
Dependency Pair Analysis



R contains the following Dependency Pairs:

A(b(a(b(x)))) -> A(b(a(a(b(x)))))
A(b(a(b(x)))) -> A(a(b(x)))

R contains no SCCs.

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