YES
(VAR X Y N M Z)
(RULES 
lt(0,s(X)) -> true
lt(s(X),0) -> false
lt(s(X),s(Y)) -> lt(X,Y)
append(nil,Y) -> Y
append(add(N,X),Y) -> add(N,append(X,Y))
split(N,nil) -> pair(nil,nil)
split(N,add(M,Y)) -> f_1(split(N,Y),N,M,Y)
f_1(pair(X,Z),N,M,Y) -> f_2(lt(N,M),N,M,Y,X,Z)
f_2(true,N,M,Y,X,Z) -> pair(X,add(M,Z))
f_2(false,N,M,Y,X,Z) -> pair(add(M,X),Z)
qsort(nil) -> nil
qsort(add(N,X)) -> f_3(split(N,X),N,X)
f_3(pair(Y,Z),N,X) -> append(qsort(Y),add(X,qsort(Z)))
)

The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting.

Proving termination of innermost rewriting for enno:

-> Dependency pairs:
nF_lt(s(X),s(Y)) -> nF_lt(X,Y)
nF_append(add(N,X),Y) -> nF_append(X,Y)
nF_split(N,add(M,Y)) -> nF_f_1(split(N,Y),N,M,Y)
nF_split(N,add(M,Y)) -> nF_split(N,Y)
nF_f_1(pair(X,Z),N,M,Y) -> nF_f_2(lt(N,M),N,M,Y,X,Z)
nF_f_1(pair(X,Z),N,M,Y) -> nF_lt(N,M)
nF_qsort(add(N,X)) -> nF_f_3(split(N,X),N,X)
nF_qsort(add(N,X)) -> nF_split(N,X)
nF_f_3(pair(Y,Z),N,X) -> nF_append(qsort(Y),add(X,qsort(Z)))
nF_f_3(pair(Y,Z),N,X) -> nF_qsort(Y)
nF_f_3(pair(Y,Z),N,X) -> nF_qsort(Z)

-> Proof of termination for enno_1_1:
-> -> Dependency pairs in cycle:
nF_qsort(add(N,X)) -> nF_f_3(split(N,X),N,X)
nF_f_3(pair(Y,Z),N,X) -> nF_qsort(Z)
nF_f_3(pair(Y,Z),N,X) -> nF_qsort(Y)

UsableRules:
lt(0,s(X)) -> true
lt(s(X),0) -> false
lt(s(X),s(Y)) -> lt(X,Y)
split(N,nil) -> pair(nil,nil)
split(N,add(M,Y)) -> f_1(split(N,Y),N,M,Y)
f_1(pair(X,Z),N,M,Y) -> f_2(lt(N,M),N,M,Y,X,Z)
f_2(true,N,M,Y,X,Z) -> pair(X,add(M,Z))
f_2(false,N,M,Y,X,Z) -> pair(add(M,X),Z)

Polynomial Interpretation:

[lt](X1,X2) = X2
[0] = 1
[s](X) = X
[true] = 0
[false] = 0
[append](X1,X2) = 0
[nil] = 0
[add](X1,X2) = X2 + 1
[split](X1,X2) = X2
[pair](X1,X2) = X1 + X2
[f_1](X1,X2,X3,X4) = X1 + 1
[f_2](X1,X2,X3,X4,X5,X6) = X5 + X6 + 1
[qsort](X) = 0
[f_3](X1,X2,X3) = 0
[nF_qsort](X) = X
[nF_f_3](X1,X2,X3) = X1 + 1

TIME: 0.128306

-> -> Dependency pairs in cycle:
nF_qsort(add(N,X)) -> nF_f_3(split(N,X),N,X)
nF_f_3(pair(Y,Z),N,X) -> nF_qsort(Z)

UsableRules:
lt(0,s(X)) -> true
lt(s(X),0) -> false
lt(s(X),s(Y)) -> lt(X,Y)
split(N,nil) -> pair(nil,nil)
split(N,add(M,Y)) -> f_1(split(N,Y),N,M,Y)
f_1(pair(X,Z),N,M,Y) -> f_2(lt(N,M),N,M,Y,X,Z)
f_2(true,N,M,Y,X,Z) -> pair(X,add(M,Z))
f_2(false,N,M,Y,X,Z) -> pair(add(M,X),Z)

Polynomial Interpretation:

[lt](X1,X2) = 1
[0] = 0
[s](X) = 0
[true] = 1
[false] = 0
[append](X1,X2) = 0
[nil] = 1
[add](X1,X2) = X2 + 1
[split](X1,X2) = X2 + 1
[pair](X1,X2) = X2 + 1
[f_1](X1,X2,X3,X4) = X1 + 1
[f_2](X1,X2,X3,X4,X5,X6) = X1 + X6 + 1
[qsort](X) = 0
[f_3](X1,X2,X3) = 0
[nF_qsort](X) = X
[nF_f_3](X1,X2,X3) = X1

TIME: 0.256511


-> Proof of termination for enno_1_2:
-> -> Dependency pairs in cycle:
nF_split(N,add(M,Y)) -> nF_split(N,Y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for enno_1_3:
-> -> Dependency pairs in cycle:
nF_append(add(N,X),Y) -> nF_append(X,Y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for enno_1_4:
-> -> Dependency pairs in cycle:
nF_lt(s(X),s(Y)) -> nF_lt(X,Y)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.