Term Rewriting System R:

   [X, Y, N, M, Z]
   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)))

Termination of R to be shown.


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   APPEND(add(N, X), Y) -> APPEND(X, Y)
   LT(s(X), s(Y)) -> LT(X, Y)
   SPLIT(N, add(M, Y)) -> F_1(split(N, Y), N, M, Y)
   SPLIT(N, add(M, Y)) -> SPLIT(N, Y)
   QSORT(add(N, X)) -> F_3(split(N, X), N, X)
   QSORT(add(N, X)) -> SPLIT(N, X)
   F_3(pair(Y, Z), N, X) -> APPEND(qsort(Y), add(X, qsort(Z)))
   F_3(pair(Y, Z), N, X) -> QSORT(Y)
   F_3(pair(Y, Z), N, X) -> QSORT(Z)
   F_1(pair(X, Z), N, M, Y) -> F_2(lt(N, M), N, M, Y, X, Z)
   F_1(pair(X, Z), N, M, Y) -> LT(N, M)

Furthermore, R contains four SCCs.


SCC1:

APPEND(add(N, X), Y) -> APPEND(X, Y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(add(x_1, x_2)) = 1 + x_1 + x_2
POL(APPEND(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   APPEND(add(N, X), Y) -> APPEND(X, Y)



 This transformation is resulting in no new subcycles.


SCC2:

LT(s(X), s(Y)) -> LT(X, Y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(s(x_1)) = 1 + x_1
POL(LT(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   LT(s(X), s(Y)) -> LT(X, Y)



 This transformation is resulting in no new subcycles.


SCC3:

SPLIT(N, add(M, Y)) -> SPLIT(N, Y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(add(x_1, x_2)) = 1 + x_1 + x_2
POL(SPLIT(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   SPLIT(N, add(M, Y)) -> SPLIT(N, Y)



 This transformation is resulting in no new subcycles.


SCC4:

F_3(pair(Y, Z), N, X) -> QSORT(Z)
F_3(pair(Y, Z), N, X) -> QSORT(Y)
QSORT(add(N, X)) -> F_3(split(N, X), N, X)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   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)


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(nil) = 0
POL(add(x_1, x_2)) = 1 + x_2
POL(s(x_1)) = 0
POL(f_1(x_1, x_2, x_3, x_4)) = 1 + x_1
POL(split(x_1, x_2)) = x_2
POL(pair(x_1, x_2)) = x_1 + x_2
POL(F_3(x_1, x_2, x_3)) = 1 + x_1
POL(0) = 0
POL(true) = 0
POL(lt(x_1, x_2)) = 0
POL(f_2(x_1, x_2, x_3, x_4, x_5, x_6)) = 1 + x_5 + x_6
POL(QSORT(x_1)) = x_1
POL(false) = 0

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 1.46 seconds.