Consider the TRS R consisting of the rewrite rules

1: app(nil,y) -> y
2: app(add(n,x),y) -> add(n,app(x,y))
3: reverse(nil) -> nil
4: reverse(add(n,x)) -> app(reverse(x),add(n,nil))
5: shuffle(nil) -> nil
6: shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))

There are 5 dependency pairs:

7: APP(add(n,x),y) -> APP(x,y)
8: REVERSE(add(n,x)) -> APP(reverse(x),add(n,nil))
9: REVERSE(add(n,x)) -> REVERSE(x)
10: SHUFFLE(add(n,x)) -> SHUFFLE(reverse(x))
11: SHUFFLE(add(n,x)) -> REVERSE(x)

The approximated dependency graph contains 3 SCCs:
{7},
{9}
and {10}.

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

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

- Consider the SCC {10}.
The usable rules are {1-4}.
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 {1-4}
are weakly decreasing and
rule 10
is strictly decreasing.

Hence the TRS is terminating.