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