Consider the TRS R consisting of the rewrite rules

1: a__f(0) -> cons(0,f(s(0)))
2: a__f(s(0)) -> a__f(a__p(s(0)))
3: a__p(s(0)) -> 0
4: mark(f(X)) -> a__f(mark(X))
5: mark(p(X)) -> a__p(mark(X))
6: mark(0) -> 0
7: mark(cons(X1,X2)) -> cons(mark(X1),X2)
8: mark(s(X)) -> s(mark(X))
9: a__f(X) -> f(X)
10: a__p(X) -> p(X)

There are 8 dependency pairs:

11: A__F(s(0)) -> A__F(a__p(s(0)))
12: A__F(s(0)) -> A__P(s(0))
13: MARK(f(X)) -> A__F(mark(X))
14: MARK(f(X)) -> MARK(X)
15: MARK(p(X)) -> A__P(mark(X))
16: MARK(p(X)) -> MARK(X)
17: MARK(cons(X1,X2)) -> MARK(X1)
18: MARK(s(X)) -> MARK(X)

The approximated dependency graph contains 2 SCCs:
{11}
and {14,16-18}.

- Consider the SCC {11}.
The usable rules are {3,10}.
By taking the polynomial interpretation
[0] = [a__p](x) = [p](x) = 1
and [A__F](x) = [s](x) = x + 1,
the rules in {3,10}
are weakly decreasing and
rule 11
is strictly decreasing.

- Consider the SCC {14,16-18}.
There are no usable rules.
By taking the polynomial interpretation
[f](x) = [MARK](x) = [p](x) = [s](x) = x + 1
and [cons](x,y) = x + y + 1,
the rules in {14,16-18}
are strictly decreasing.

Hence the TRS is terminating.