Term Rewriting System R:

   [Y, X, N, L, M]
   le(0, Y) -> true
   le(s(X), 0) -> false
   le(s(X), s(Y)) -> le(X, Y)
   app(nil, Y) -> Y
   app(cons(N, L), Y) -> cons(N, app(L, Y))
   low(N, nil) -> nil
   low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L))
   iflow(true, N, cons(M, L)) -> cons(M, low(N, L))
   iflow(false, N, cons(M, L)) -> low(N, L)
   high(N, nil) -> nil
   high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L))
   ifhigh(true, N, cons(M, L)) -> high(N, L)
   ifhigh(false, N, cons(M, L)) -> cons(M, high(N, L))
   quicksort(nil) -> nil
   quicksort(cons(N, L)) -> app(quicksort(low(N, L)), cons(N, quicksort(high(N, L))))

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: 


   IFLOW(false, N, cons(M, L)) -> LOW(N, L)
   IFLOW(true, N, cons(M, L)) -> LOW(N, L)
   LOW(N, cons(M, L)) -> IFLOW(le(M, N), N, cons(M, L))
   LOW(N, cons(M, L)) -> LE(M, N)
   APP(cons(N, L), Y) -> APP(L, Y)
   IFHIGH(false, N, cons(M, L)) -> HIGH(N, L)
   IFHIGH(true, N, cons(M, L)) -> HIGH(N, L)
   HIGH(N, cons(M, L)) -> IFHIGH(le(M, N), N, cons(M, L))
   HIGH(N, cons(M, L)) -> LE(M, N)
   LE(s(X), s(Y)) -> LE(X, Y)
   QUICKSORT(cons(N, L)) -> APP(quicksort(low(N, L)), cons(N, quicksort(high(N, L))))
   QUICKSORT(cons(N, L)) -> QUICKSORT(low(N, L))
   QUICKSORT(cons(N, L)) -> LOW(N, L)
   QUICKSORT(cons(N, L)) -> QUICKSORT(high(N, L))
   QUICKSORT(cons(N, L)) -> HIGH(N, L)

Furthermore, R contains five SCCs.


SCC1:

LE(s(X), s(Y)) -> LE(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(LE(x_1, x_2)) = 1 + x_1 + x_2
POL(s(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

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



 This transformation is resulting in no new subcycles.


SCC2:

APP(cons(N, L), Y) -> APP(L, 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(APP(x_1, x_2)) = 1 + x_1 + x_2
POL(cons(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   APP(cons(N, L), Y) -> APP(L, Y)



 This transformation is resulting in no new subcycles.


SCC3:

IFLOW(true, N, cons(M, L)) -> LOW(N, L)
LOW(N, cons(M, L)) -> IFLOW(le(M, N), N, cons(M, L))
IFLOW(false, N, cons(M, L)) -> LOW(N, L)

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

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(s(x_1)) = 0
POL(le(x_1, x_2)) = 0
POL(LOW(x_1, x_2)) = x_2
POL(true) = 0
POL(IFLOW(x_1, x_2, x_3)) = x_3
POL(0) = 0
POL(false) = 0
POL(cons(x_1, x_2)) = 1 + x_2

 resulting in no subcycles.


SCC4:

IFHIGH(true, N, cons(M, L)) -> HIGH(N, L)
HIGH(N, cons(M, L)) -> IFHIGH(le(M, N), N, cons(M, L))
IFHIGH(false, N, cons(M, L)) -> HIGH(N, L)

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

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(s(x_1)) = 0
POL(le(x_1, x_2)) = 0
POL(true) = 0
POL(IFHIGH(x_1, x_2, x_3)) = x_3
POL(0) = 0
POL(false) = 0
POL(HIGH(x_1, x_2)) = x_2
POL(cons(x_1, x_2)) = 1 + x_2

 resulting in no subcycles.


SCC5:

QUICKSORT(cons(N, L)) -> QUICKSORT(high(N, L))
QUICKSORT(cons(N, L)) -> QUICKSORT(low(N, L))

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

Additionally, the following rules can be oriented: 

   high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L))
   high(N, nil) -> nil
   ifhigh(false, N, cons(M, L)) -> cons(M, high(N, L))
   ifhigh(true, N, cons(M, L)) -> high(N, L)
   iflow(false, N, cons(M, L)) -> low(N, L)
   iflow(true, N, cons(M, L)) -> cons(M, low(N, L))
   low(N, nil) -> nil
   low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(nil) = 0
POL(iflow(x_1, x_2, x_3)) = x_3
POL(s(x_1)) = 0
POL(le(x_1, x_2)) = 0
POL(high(x_1, x_2)) = x_2
POL(QUICKSORT(x_1)) = x_1
POL(true) = 0
POL(low(x_1, x_2)) = x_2
POL(0) = 0
POL(ifhigh(x_1, x_2, x_3)) = x_3
POL(false) = 0
POL(cons(x_1, x_2)) = 1 + x_2

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 1.339 seconds.