Consider the TRS R consisting of the rewrite rules

1: eq(0,0) -> true
2: eq(0,s(X)) -> false
3: eq(s(X),0) -> false
4: eq(s(X),s(Y)) -> eq(X,Y)
5: rm(N,nil) -> nil
6: rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
7: ifrm(true,N,add(M,X)) -> rm(N,X)
8: ifrm(false,N,add(M,X)) -> add(M,rm(N,X))
9: purge(nil) -> nil
10: purge(add(N,X)) -> add(N,purge(rm(N,X)))

There are 7 dependency pairs:

11: EQ(s(X),s(Y)) -> EQ(X,Y)
12: RM(N,add(M,X)) -> IFRM(eq(N,M),N,add(M,X))
13: RM(N,add(M,X)) -> EQ(N,M)
14: IFRM(true,N,add(M,X)) -> RM(N,X)
15: IFRM(false,N,add(M,X)) -> RM(N,X)
16: PURGE(add(N,X)) -> PURGE(rm(N,X))
17: PURGE(add(N,X)) -> RM(N,X)

The approximated dependency graph contains 3 SCCs:
{11},
{12,14,15}
and {16}.

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

- Consider the SCC {12,14,15}.
The usable rules are {1-4}.
By taking the polynomial interpretation
[0] = [false] = [true] = 1,
[s](x) = x + 1,
[add](x,y) = [eq](x,y) = [RM](x,y) = x + y + 1
and [IFRM](x,y,z) = y + z + 1,
rule 12
is weakly decreasing and
the rules in {1-4,14,15}
are strictly decreasing.

- Consider the SCC {16}.
The usable rules are {1-8}.
By taking the polynomial interpretation
[0] = [false] = [nil] = [true] = 1,
[PURGE](x) = [s](x) = x + 1,
[rm](x,y) = x + y,
[add](x,y) = [eq](x,y) = x + y + 1
and [ifrm](x,y,z) = y + z,
the rules in {5,6,8}
are weakly decreasing and
the rules in {1-4,7,16}
are strictly decreasing.

Hence the TRS is terminating.