Consider the TRS R consisting of the rewrite rules

1: minus(x,0) -> x
2: minus(s(x),s(y)) -> minus(x,y)
3: quot(0,s(y)) -> 0
4: quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
5: app(nil,y) -> y
6: app(add(n,x),y) -> add(n,app(x,y))
7: reverse(nil) -> nil
8: reverse(add(n,x)) -> app(reverse(x),add(n,nil))
9: shuffle(nil) -> nil
10: shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
11: concat(leaf,y) -> y
12: concat(cons(u,v),y) -> cons(u,concat(v,y))
13: less_leaves(x,leaf) -> false
14: less_leaves(leaf,cons(w,z)) -> true
15: less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))

There are 12 dependency pairs:

16: MINUS(s(x),s(y)) -> MINUS(x,y)
17: QUOT(s(x),s(y)) -> QUOT(minus(x,y),s(y))
18: QUOT(s(x),s(y)) -> MINUS(x,y)
19: APP(add(n,x),y) -> APP(x,y)
20: REVERSE(add(n,x)) -> APP(reverse(x),add(n,nil))
21: REVERSE(add(n,x)) -> REVERSE(x)
22: SHUFFLE(add(n,x)) -> SHUFFLE(reverse(x))
23: SHUFFLE(add(n,x)) -> REVERSE(x)
24: CONCAT(cons(u,v),y) -> CONCAT(v,y)
25: LESS_LEAVES(cons(u,v),cons(w,z)) -> LESS_LEAVES(concat(u,v),concat(w,z))
26: LESS_LEAVES(cons(u,v),cons(w,z)) -> CONCAT(u,v)
27: LESS_LEAVES(cons(u,v),cons(w,z)) -> CONCAT(w,z)

The approximated dependency graph contains 7 SCCs:
{19},
{24},
{25},
{16},
{17},
{21}
and {22}.

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

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

- Consider the SCC {25}.
The usable rules are {11,12}.
By taking the polynomial interpretation
[leaf] = 1,
[concat](x,y) = x + y
and [cons](x,y) = [LESS_LEAVES](x,y) = x + y + 1,
rule 12
is weakly decreasing and
the rules in {11,25}
are strictly decreasing.

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

- Consider the SCC {17}.
The usable rules are {1,2}.
By taking the polynomial interpretation
[0] = 1,
[minus](x,y) = x,
[s](x) = x + 1
and [QUOT](x,y) = x + y + 1,
rule 1
is weakly decreasing and
the rules in {2,17}
are strictly decreasing.

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

- Consider the SCC {22}.
The usable rules are {5-8}.
By taking the polynomial interpretation
[nil] = 0,
[reverse](x) = x,
[SHUFFLE](x) = x + 1,
[app](x,y) = x + y
and [add](x,y) = x + y + 1,
the rules in {5-8}
are weakly decreasing and
rule 22
is strictly decreasing.

Hence the TRS is terminating.