Consider the TRS R consisting of the rewrite rules

1: lt(0,s(X)) -> true
2: lt(s(X),0) -> false
3: lt(s(X),s(Y)) -> lt(X,Y)
4: append(nil,Y) -> Y
5: append(add(N,X),Y) -> add(N,append(X,Y))
6: split(N,nil) -> pair(nil,nil)
7: split(N,add(M,Y)) -> f_1(split(N,Y),N,M,Y)
8: f_1(pair(X,Z),N,M,Y) -> f_2(lt(N,M),N,M,Y,X,Z)
9: f_2(true,N,M,Y,X,Z) -> pair(X,add(M,Z))
10: f_2(false,N,M,Y,X,Z) -> pair(add(M,X),Z)
11: qsort(nil) -> nil
12: qsort(add(N,X)) -> f_3(split(N,X),N,X)
13: f_3(pair(Y,Z),N,X) -> append(qsort(Y),add(X,qsort(Z)))

There are 11 dependency pairs:

14: LT(s(X),s(Y)) -> LT(X,Y)
15: APPEND(add(N,X),Y) -> APPEND(X,Y)
16: SPLIT(N,add(M,Y)) -> F_1(split(N,Y),N,M,Y)
17: SPLIT(N,add(M,Y)) -> SPLIT(N,Y)
18: F_1(pair(X,Z),N,M,Y) -> F_2(lt(N,M),N,M,Y,X,Z)
19: F_1(pair(X,Z),N,M,Y) -> LT(N,M)
20: QSORT(add(N,X)) -> F_3(split(N,X),N,X)
21: QSORT(add(N,X)) -> SPLIT(N,X)
22: F_3(pair(Y,Z),N,X) -> APPEND(qsort(Y),add(X,qsort(Z)))
23: F_3(pair(Y,Z),N,X) -> QSORT(Y)
24: F_3(pair(Y,Z),N,X) -> QSORT(Z)

The approximated dependency graph contains 4 SCCs:
{15},
{14},
{17}
and {20,23,24}.

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

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

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

- Consider the SCC {20,23,24}.
The usable rules are {1-3,6-10}.
By taking the polynomial interpretation
[nil] = 0,
[0] = [false] = [true] = 1,
[QSORT](x) = [s](x) = x + 1,
[pair](x,y) = x + y,
[add](x,y) = [F_3](x,y,z) = [lt](x,y) = x + y + 1,
[f_1](x,y,z,w) = x + z + 1,
[split](x,y) = y
and [f_2](x,y,z,w,v,u) = z + v + u + 1,
the rules in {6-10,23,24}
are weakly decreasing and
the rules in {1-3,20}
are strictly decreasing.

Hence the TRS is terminating.