Consider the TRS R consisting of the rewrite rules

1: bsort(nil) -> nil
2: bsort(x . y) -> last(bubble(x . y) . bsort(butlast(bubble(x . y))))
3: bubble(nil) -> nil
4: bubble(x . nil) -> x . nil
5: bubble(x . (y . z)) -> if(x <= y,y . bubble(x . z),x . bubble(y . z))
6: last(nil) -> 0
7: last(x . nil) -> x
8: last(x . (y . z)) -> last(y . z)
9: butlast(nil) -> nil
10: butlast(x . nil) -> nil
11: butlast(x . (y . z)) -> x . butlast(y . z)

There are 8 dependency pairs:

12: BSORT(x . y) -> LAST(bubble(x . y) . bsort(butlast(bubble(x . y))))
13: BSORT(x . y) -> BSORT(butlast(bubble(x . y)))
14: BSORT(x . y) -> BUTLAST(bubble(x . y))
15: BSORT(x . y) -> BUBBLE(x . y)
16: BUBBLE(x . (y . z)) -> BUBBLE(x . z)
17: BUBBLE(x . (y . z)) -> BUBBLE(y . z)
18: LAST(x . (y . z)) -> LAST(y . z)
19: BUTLAST(x . (y . z)) -> BUTLAST(y . z)

The approximated dependency graph contains 4 SCCs:
{16,17},
{19},
{18}
and {13}.

- Consider the SCC {16,17}.
There are no usable rules.
By taking the polynomial interpretation
[BUBBLE](x) = x + 1
and [.](x,y) = x + y + 1,
the rules in {16,17}
are strictly decreasing.

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

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

- Consider the SCC {13}.
The usable rules are {3-5,9-11}.
By taking the polynomial interpretation
[if](x,y,z) = [nil] = 0,
[bubble](x) = 1,
[<=](x,y) = qy + px + o,
[BSORT](x) = x,
[butlast](x) = x - 1
and [.](x,y) = y + 1,
we obtain a quasi-model of the usable rules.
Furthermore, dependency pair 13
is strictly decreasing.

Hence the TRS is terminating.