(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

a__f(f(a)) → a__f(g(f(a)))
mark(f(X)) → a__f(mark(X))
mark(a) → a
mark(g(X)) → g(X)
a__f(X) → f(X)

Q is empty.