Termination Proof using AProVE

Term Rewriting System R:
[X]
a_{_c} -> a_{_f}(g(c))
a_{_c} -> c
a_{_f}(g(X)) -> g(X)
a_{_f}(X) -> f(X)
mark(c) -> a_{_c}
mark(f(X)) -> a_{_f}(X)
mark(g(X)) -> g(X)

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

A_{_C} -> A_{_F}(g(c))
MARK(c) -> A_{_C}
MARK(f(X)) -> A_{_F}(X)

R contains no SCCs.

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