Term Rewriting System R:
[x]
d(x) -> e(u(x))
d(u(x)) -> c(x)
c(u(x)) -> b(x)
v(e(x)) -> x
b(u(x)) -> a(e(x))

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

D(u(x)) -> C(x)
C(u(x)) -> B(x)

R contains no SCCs.

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