Consider the TRS R consisting of the rewrite rules

1: f(cons(nil,y)) -> y
2: f(cons(f(cons(nil,y)),z)) -> copy(n,y,z)
3: copy(0,y,z) -> f(z)
4: copy(s(x),y,z) -> copy(x,y,cons(f(y),z))

There are 4 dependency pairs:

5: F(cons(f(cons(nil,y)),z)) -> COPY(n,y,z)
6: COPY(0,y,z) -> F(z)
7: COPY(s(x),y,z) -> COPY(x,y,cons(f(y),z))
8: COPY(s(x),y,z) -> F(y)

The approximated dependency graph contains one SCC:
{7}.

- Consider the SCC {7}.
By taking the polynomial interpretation
[0] = [n] = [nil] = 1,
[f](x) = [s](x) = x + 1,
[COPY](x,y,z) = x + y + 1,
[copy](x,y,z) = x + z + 1
and [cons](x,y) = y + 1,
the rules in {2,4}
are weakly decreasing and
the rules in {1,3,7}
are strictly decreasing.

Hence the TRS is terminating.