Consider the TRS R consisting of the rewrite rules

1: eq(0,0) -> true
2: eq(0,s(m)) -> false
3: eq(s(n),0) -> false
4: eq(s(n),s(m)) -> eq(n,m)
5: le(0,m) -> true
6: le(s(n),0) -> false
7: le(s(n),s(m)) -> le(n,m)
8: min(cons(0,nil)) -> 0
9: min(cons(s(n),nil)) -> s(n)
10: min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
11: if_min(true,cons(n,cons(m,x))) -> min(cons(n,x))
12: if_min(false,cons(n,cons(m,x))) -> min(cons(m,x))
13: replace(n,m,nil) -> nil
14: replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
15: if_replace(true,n,m,cons(k,x)) -> cons(m,x)
16: if_replace(false,n,m,cons(k,x)) -> cons(k,replace(n,m,x))
17: sort(nil) -> nil
18: sort(cons(n,x)) -> cons(min(cons(n,x)),sort(replace(min(cons(n,x)),n,x)))

There are 12 dependency pairs:

19: EQ(s(n),s(m)) -> EQ(n,m)
20: LE(s(n),s(m)) -> LE(n,m)
21: MIN(cons(n,cons(m,x))) -> IF_MIN(le(n,m),cons(n,cons(m,x)))
22: MIN(cons(n,cons(m,x))) -> LE(n,m)
23: IF_MIN(true,cons(n,cons(m,x))) -> MIN(cons(n,x))
24: IF_MIN(false,cons(n,cons(m,x))) -> MIN(cons(m,x))
25: REPLACE(n,m,cons(k,x)) -> IF_REPLACE(eq(n,k),n,m,cons(k,x))
26: REPLACE(n,m,cons(k,x)) -> EQ(n,k)
27: IF_REPLACE(false,n,m,cons(k,x)) -> REPLACE(n,m,x)
28: SORT(cons(n,x)) -> SORT(replace(min(cons(n,x)),n,x))
29: SORT(cons(n,x)) -> REPLACE(min(cons(n,x)),n,x)
30: SORT(cons(n,x)) -> MIN(cons(n,x))

The approximated dependency graph contains 5 SCCs:
{19},
{20},
{21,23,24},
{25,27}
and {28}.

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

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

- Consider the SCC {21,23,24}.
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 [IF_MIN](x,y) = y + 1,
rule 21
is weakly decreasing and
the rules in {5-7,23,24}
are strictly decreasing.

- Consider the SCC {25,27}.
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 [IF_REPLACE](x,y,z,w) = y + z + w + 1,
rule 25
is weakly decreasing and
the rules in {1-4,27}
are strictly decreasing.

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

Hence the TRS is terminating.