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: le(0,y) -> true
6: le(s(x),0) -> false
7: le(s(x),s(y)) -> le(x,y)
8: app(nil,y) -> y
9: app(add(n,x),y) -> add(n,app(x,y))
10: min(add(n,nil)) -> n
11: min(add(n,add(m,x))) -> if_min(le(n,m),add(n,add(m,x)))
12: if_min(true,add(n,add(m,x))) -> min(add(n,x))
13: if_min(false,add(n,add(m,x))) -> min(add(m,x))
14: rm(n,nil) -> nil
15: rm(n,add(m,x)) -> if_rm(eq(n,m),n,add(m,x))
16: if_rm(true,n,add(m,x)) -> rm(n,x)
17: if_rm(false,n,add(m,x)) -> add(m,rm(n,x))
18: minsort(nil,nil) -> nil
19: minsort(add(n,x),y) -> if_minsort(eq(n,min(add(n,x))),add(n,x),y)
20: if_minsort(true,add(n,x),y) -> add(n,minsort(app(rm(n,x),y),nil))
21: if_minsort(false,add(n,x),y) -> minsort(x,add(n,y))

There are 18 dependency pairs:

22: EQ(s(x),s(y)) -> EQ(x,y)
23: LE(s(x),s(y)) -> LE(x,y)
24: APP(add(n,x),y) -> APP(x,y)
25: MIN(add(n,add(m,x))) -> IF_MIN(le(n,m),add(n,add(m,x)))
26: MIN(add(n,add(m,x))) -> LE(n,m)
27: IF_MIN(true,add(n,add(m,x))) -> MIN(add(n,x))
28: IF_MIN(false,add(n,add(m,x))) -> MIN(add(m,x))
29: RM(n,add(m,x)) -> IF_RM(eq(n,m),n,add(m,x))
30: RM(n,add(m,x)) -> EQ(n,m)
31: IF_RM(true,n,add(m,x)) -> RM(n,x)
32: IF_RM(false,n,add(m,x)) -> RM(n,x)
33: MINSORT(add(n,x),y) -> IF_MINSORT(eq(n,min(add(n,x))),add(n,x),y)
34: MINSORT(add(n,x),y) -> EQ(n,min(add(n,x)))
35: MINSORT(add(n,x),y) -> MIN(add(n,x))
36: IF_MINSORT(true,add(n,x),y) -> MINSORT(app(rm(n,x),y),nil)
37: IF_MINSORT(true,add(n,x),y) -> APP(rm(n,x),y)
38: IF_MINSORT(true,add(n,x),y) -> RM(n,x)
39: IF_MINSORT(false,add(n,x),y) -> MINSORT(x,add(n,y))

The approximated dependency graph contains 6 SCCs:
{24},
{22},
{23},
{25,27,28},
{29,31,32}
and {33,36,39}.

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

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

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

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

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

- Consider the SCC {33,36,39}.
The usable rules are {1-17}.
By taking the polynomial interpretation
[nil] = 0,
[0] = [false] = [le](x,y) = [true] = 1,
[min](x) = [s](x) = x + 1,
[app](x,y) = [if_min](x,y) = [rm](x,y) = x + y,
[add](x,y) = [eq](x,y) = [MINSORT](x,y) = x + y + 1,
[if_rm](x,y,z) = y + z
and [IF_MINSORT](x,y,z) = y + z + 1,
the rules in {5-9,11,14,15,17,33,39}
are weakly decreasing and
the rules in {1-4,10,12,13,16,36}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {33,39}.
The usable rules are {1-7,10-13}.
By taking the polynomial interpretation
[0] = [false] = [le](x,y) = [nil] = [true] = 1,
[min](x) = [MINSORT](x,y) = [s](x) = x + 1,
[if_min](x,y) = x + y,
[add](x,y) = [eq](x,y) = x + y + 1
and [IF_MINSORT](x,y,z) = y + 1,
the rules in {5-7,11,33}
are weakly decreasing and
the rules in {1-4,10,12,13,39}
are strictly decreasing.


Hence the TRS is terminating.