YES
(VAR X)
(RULES 
a__f(f(a)) -> a__f(g(f(a)))
mark(f(X)) -> a__f(X)
mark(a) -> a
mark(g(X)) -> g(mark(X))
a__f(X) -> f(X)
)

Proving termination of rewriting for Ex15_Luc06_GM:

-> Dependency pairs:
nF_a__f(f(a)) -> nF_a__f(g(f(a)))
nF_mark(f(X)) -> nF_a__f(X)
nF_mark(g(X)) -> nF_mark(X)

-> Proof of termination for Ex15_Luc06_GM_1:
-> -> Dependency pairs in cycle:
nF_mark(g(X)) -> nF_mark(X)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.