Consider the TRS R consisting of the rewrite rules

1: purge(nil) -> nil
2: purge(x . y) -> x . purge(remove(x,y))
3: remove(x,nil) -> nil
4: remove(x,y . z) -> if(x = y,remove(x,z),y . remove(x,z))

There are 3 dependency pairs:

5: PURGE(x . y) -> PURGE(remove(x,y))
6: PURGE(x . y) -> REMOVE(x,y)
7: REMOVE(x,y . z) -> REMOVE(x,z)

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

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

- Consider the SCC {5}.
The usable rules are {3,4}.
By taking the polynomial interpretation
[=](x,y) = 0,
[nil] = 1,
[PURGE](x) = x + 1,
[remove](x,y) = x + y,
[.](x,y) = x + y + 1
and [if](x,y,z) = x + z,
the rules in {3,4}
are weakly decreasing and
rule 5
is strictly decreasing.

Hence the TRS is terminating.