Term Rewriting System R:

   [x, y, n, m]
   minus(x, 0) -> x
   minus(s(x), s(y)) -> minus(x, y)
   quot(0, s(y)) -> 0
   quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
   le(0, y) -> true
   le(s(x), 0) -> false
   le(s(x), s(y)) -> le(x, y)
   app(nil, y) -> y
   app(add(n, x), y) -> add(n, app(x, y))
   low(n, nil) -> nil
   low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
   if_low(true, n, add(m, x)) -> add(m, low(n, x))
   if_low(false, n, add(m, x)) -> low(n, x)
   high(n, nil) -> nil
   high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
   if_high(true, n, add(m, x)) -> high(n, x)
   if_high(false, n, add(m, x)) -> add(m, high(n, x))
   quicksort(nil) -> nil
   quicksort(add(n, x)) -> app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))

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: 


   APP(add(n, x), y) -> APP(x, y)
   IF_HIGH(true, n, add(m, x)) -> HIGH(n, x)
   IF_HIGH(false, n, add(m, x)) -> HIGH(n, x)
   HIGH(n, add(m, x)) -> IF_HIGH(le(m, n), n, add(m, x))
   HIGH(n, add(m, x)) -> LE(m, n)
   LE(s(x), s(y)) -> LE(x, y)
   MINUS(s(x), s(y)) -> MINUS(x, y)
   QUICKSORT(add(n, x)) -> APP(quicksort(low(n, x)), add(n, quicksort(high(n, x))))
   QUICKSORT(add(n, x)) -> QUICKSORT(low(n, x))
   QUICKSORT(add(n, x)) -> LOW(n, x)
   QUICKSORT(add(n, x)) -> QUICKSORT(high(n, x))
   QUICKSORT(add(n, x)) -> HIGH(n, x)
   LOW(n, add(m, x)) -> IF_LOW(le(m, n), n, add(m, x))
   LOW(n, add(m, x)) -> LE(m, n)
   QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))
   QUOT(s(x), s(y)) -> MINUS(x, y)
   IF_LOW(false, n, add(m, x)) -> LOW(n, x)
   IF_LOW(true, n, add(m, x)) -> LOW(n, x)

Furthermore, R contains seven SCCs.


SCC1:

APP(add(n, x), y) -> APP(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(APP(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   APP(add(n, x), y) -> APP(x, y)



 This transformation is resulting in no new subcycles.


SCC2:

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.


SCC3:

MINUS(s(x), s(y)) -> MINUS(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(MINUS(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   MINUS(s(x), s(y)) -> MINUS(x, y)



 This transformation is resulting in no new subcycles.


SCC4:

IF_HIGH(false, n, add(m, x)) -> HIGH(n, x)
HIGH(n, add(m, x)) -> IF_HIGH(le(m, n), n, add(m, x))
IF_HIGH(true, n, add(m, x)) -> HIGH(n, x)

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(add(x_1, x_2)) = 1 + x_2
POL(s(x_1)) = 0
POL(le(x_1, x_2)) = 0
POL(true) = 0
POL(IF_HIGH(x_1, x_2, x_3)) = x_3
POL(0) = 0
POL(false) = 0
POL(HIGH(x_1, x_2)) = x_2

 resulting in no subcycles.


SCC5:

IF_LOW(true, n, add(m, x)) -> LOW(n, x)
IF_LOW(false, n, add(m, x)) -> LOW(n, x)
LOW(n, add(m, x)) -> IF_LOW(le(m, n), n, add(m, x))

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(add(x_1, x_2)) = 1 + x_2
POL(s(x_1)) = 0
POL(le(x_1, x_2)) = 0
POL(IF_LOW(x_1, x_2, x_3)) = x_3
POL(LOW(x_1, x_2)) = x_2
POL(true) = 0
POL(0) = 0
POL(false) = 0

 resulting in no subcycles.


SCC6:

QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))

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

Additionally, the following rules can be oriented: 

   minus(x, 0) -> x
   minus(s(x), s(y)) -> minus(x, y)


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(s(x_1)) = 1 + x_1
POL(minus(x_1, x_2)) = x_1
POL(QUOT(x_1, x_2)) = x_1 + x_2
POL(0) = 1

 resulting in no subcycles.


SCC7:

QUICKSORT(add(n, x)) -> QUICKSORT(high(n, x))
QUICKSORT(add(n, x)) -> QUICKSORT(low(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: 

   if_high(true, n, add(m, x)) -> high(n, x)
   if_high(false, n, add(m, x)) -> add(m, high(n, x))
   high(n, nil) -> nil
   high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
   if_low(false, n, add(m, x)) -> low(n, x)
   if_low(true, n, add(m, x)) -> add(m, low(n, x))
   low(n, nil) -> nil
   low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(nil) = 0
POL(add(x_1, x_2)) = 1 + x_2
POL(if_high(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(if_low(x_1, x_2, x_3)) = x_3
POL(QUICKSORT(x_1)) = x_1
POL(true) = 0
POL(low(x_1, x_2)) = x_2
POL(0) = 0
POL(false) = 0

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 1.643 seconds.