Consider the TRS R consisting of the rewrite rules

1: a__f(g(X),Y) -> a__f(mark(X),f(g(X),Y))
2: mark(f(X1,X2)) -> a__f(mark(X1),X2)
3: mark(g(X)) -> g(mark(X))
4: a__f(X1,X2) -> f(X1,X2)

There are 5 dependency pairs:

5: A__F(g(X),Y) -> A__F(mark(X),f(g(X),Y))
6: A__F(g(X),Y) -> MARK(X)
7: MARK(f(X1,X2)) -> A__F(mark(X1),X2)
8: MARK(f(X1,X2)) -> MARK(X1)
9: MARK(g(X)) -> MARK(X)

The approximated dependency graph contains one SCC:
{5-9}.

- Consider the SCC {5-9}.
By taking the polynomial interpretation
[a__f](x,y) = [A__F](x,y) = [f](x,y) = [g](x) = [mark](x) = [MARK](x) = x + 1,
the rules in {1-5,7}
are weakly decreasing and
the rules in {6,8,9}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {5}.
By taking the polynomial interpretation
[mark](x) = x
and [a__f](x,y) = [A__F](x,y) = [f](x,y) = [g](x) = x + 1,
the rules in {2-4}
are weakly decreasing and
the rules in {1,5}
are strictly decreasing.


Hence the TRS is terminating.