Term Rewriting System R:
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)

Termination of R to be shown.

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.

Termination of R successfully shown.
0:00 minutes