Consider the TRS R consisting of the rewrite rules

1: eq(0,0) -> true
2: eq(0,s(Y)) -> false
3: eq(s(X),0) -> false
4: eq(s(X),s(Y)) -> eq(X,Y)
5: le(0,Y) -> true
6: le(s(X),0) -> false
7: le(s(X),s(Y)) -> le(X,Y)
8: min(cons(0,nil)) -> 0
9: min(cons(s(N),nil)) -> s(N)
10: min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L)))
11: ifmin(true,cons(N,cons(M,L))) -> min(cons(N,L))
12: ifmin(false,cons(N,cons(M,L))) -> min(cons(M,L))
13: replace(N,M,nil) -> nil
14: replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L))
15: ifrepl(true,N,M,cons(K,L)) -> cons(M,L)
16: ifrepl(false,N,M,cons(K,L)) -> cons(K,replace(N,M,L))
17: selsort(nil) -> nil
18: selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L))
19: ifselsort(true,cons(N,L)) -> cons(N,selsort(L))
20: ifselsort(false,cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L)))

There are 16 dependency pairs:

21: EQ(s(X),s(Y)) -> EQ(X,Y)
22: LE(s(X),s(Y)) -> LE(X,Y)
23: MIN(cons(N,cons(M,L))) -> IFMIN(le(N,M),cons(N,cons(M,L)))
24: MIN(cons(N,cons(M,L))) -> LE(N,M)
25: IFMIN(true,cons(N,cons(M,L))) -> MIN(cons(N,L))
26: IFMIN(false,cons(N,cons(M,L))) -> MIN(cons(M,L))
27: REPLACE(N,M,cons(K,L)) -> IFREPL(eq(N,K),N,M,cons(K,L))
28: REPLACE(N,M,cons(K,L)) -> EQ(N,K)
29: IFREPL(false,N,M,cons(K,L)) -> REPLACE(N,M,L)
30: SELSORT(cons(N,L)) -> IFSELSORT(eq(N,min(cons(N,L))),cons(N,L))
31: SELSORT(cons(N,L)) -> EQ(N,min(cons(N,L)))
32: SELSORT(cons(N,L)) -> MIN(cons(N,L))
33: IFSELSORT(true,cons(N,L)) -> SELSORT(L)
34: IFSELSORT(false,cons(N,L)) -> SELSORT(replace(min(cons(N,L)),N,L))
35: IFSELSORT(false,cons(N,L)) -> REPLACE(min(cons(N,L)),N,L)
36: IFSELSORT(false,cons(N,L)) -> MIN(cons(N,L))

The approximated dependency graph contains 5 SCCs:
{21},
{22},
{23,25,26},
{27,29}
and {30,33,34}.

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

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

- Consider the SCC {23,25,26}.
The usable rules are {5-7}.
By taking the polynomial interpretation
[0] = [false] = [true] = 1,
[MIN](x) = [s](x) = x + 1,
[cons](x,y) = [le](x,y) = x + y + 1
and [IFMIN](x,y) = y + 1,
rule 23
is weakly decreasing and
the rules in {5-7,25,26}
are strictly decreasing.

- Consider the SCC {27,29}.
The usable rules are {1-4}.
By taking the polynomial interpretation
[0] = [false] = [true] = 1,
[s](x) = x + 1,
[cons](x,y) = [eq](x,y) = x + y + 1,
[REPLACE](x,y,z) = x + y + z + 1
and [IFREPL](x,y,z,w) = y + z + w + 1,
rule 27
is weakly decreasing and
the rules in {1-4,29}
are strictly decreasing.

- Consider the SCC {30,33,34}.
The usable rules are {1-16}.
By taking the polynomial interpretation
[0] = [false] = [le](x,y) = [nil] = [true] = 1,
[min](x) = [s](x) = [SELSORT](x) = x + 1,
[ifmin](x,y) = x + y,
[cons](x,y) = [eq](x,y) = x + y + 1,
[IFSELSORT](x,y) = y + 1,
[replace](x,y,z) = y + z + 1
and [ifrepl](x,y,z,w) = z + w + 1,
the rules in {5-7,10,14,16,30,34}
are weakly decreasing and
the rules in {1-4,8,9,11-13,15,33}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {30,34}.
By taking the polynomial interpretation
[0] = [false] = [le](x,y) = [nil] = [true] = 1,
[min](x) = [s](x) = [SELSORT](x) = x + 1,
[ifmin](x,y) = x + y,
[cons](x,y) = [eq](x,y) = x + y + 1,
[IFSELSORT](x,y) = y + 1,
[replace](x,y,z) = y + z
and [ifrepl](x,y,z,w) = z + w,
the rules in {5-7,10,13-16,30}
are weakly decreasing and
the rules in {1-4,8,9,11,12,34}
are strictly decreasing.


Hence the TRS is terminating.