Consider the TRS R consisting of the rewrite rules

1: del(x . (y . z)) -> f(x = y,x,y,z)
2: f(true,x,y,z) -> del(y . z)
3: f(false,x,y,z) -> x . del(y . z)
4: nil = nil -> true
5: (x . y) = nil -> false
6: nil = (y . z) -> false
7: (x . y) = (u . v) -> and(x = u,y = v)

There are 6 dependency pairs:

8: DEL(x . (y . z)) -> F(x = y,x,y,z)
9: DEL(x . (y . z)) -> x =# y
10: F(true,x,y,z) -> DEL(y . z)
11: F(false,x,y,z) -> DEL(y . z)
12: (x . y) =# (u . v) -> x =# u
13: (x . y) =# (u . v) -> y =# v

The approximated dependency graph contains one SCC:
{8,10,11}.

- Consider the SCC {8,10,11}.
The usable rules are {4-7}.
By taking the polynomial interpretation
[false] = [nil] = [true] = [u] = [v] = 1,
[DEL](x) = x,
[.](x,y) = [=](x,y) = [and](x,y) = x + y + 1
and [F](x,y,z,w) = y + z + w + 1,
the rules in {7,10,11}
are weakly decreasing and
the rules in {4-6,8}
are strictly decreasing.

Hence the TRS is terminating.