Term Rewriting System R:
[X]
ac -> af(g(c))
ac -> c
af(g(X)) -> g(X)
af(X) -> f(X)
mark(c) -> ac
mark(f(X)) -> af(X)
mark(g(X)) -> g(X)

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

AC -> AF(g(c))
MARK(c) -> AC
MARK(f(X)) -> AF(X)

R contains no SCCs.

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