Consider the TRS R consisting of the rewrite rules

1: f(a,empty) -> g(a,empty)
2: f(a,cons(x,k)) -> f(cons(x,a),k)
3: g(empty,d) -> d
4: g(cons(x,k),d) -> g(k,cons(x,d))

There are 3 dependency pairs:

5: F(a,empty) -> G(a,empty)
6: F(a,cons(x,k)) -> F(cons(x,a),k)
7: G(cons(x,k),d) -> G(k,cons(x,d))

The approximated dependency graph contains 2 SCCs:
{7}
and {6}.

- Consider the SCC {7}.
There are no usable rules.
By taking the polynomial interpretation
[G](x,y) = x + 1
and [cons](x,y) = x + y + 1,
rule 7
is strictly decreasing.

- Consider the SCC {6}.
There are no usable rules.
By taking the polynomial interpretation
[cons](x,y) = x + y + 1
and [F](x,y) = y + 1,
rule 6
is strictly decreasing.

Hence the TRS is terminating.