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))))

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

LE(s(X), s(Y)) -> LE(X, Y)
APP(cons(N, L), Y) -> APP(L, Y)
LOW(N, cons(M, L)) -> IFLOW(le(M, N), N, cons(M, L))
LOW(N, cons(M, L)) -> LE(M, N)
IFLOW(true, N, cons(M, L)) -> LOW(N, L)
IFLOW(false, N, cons(M, L)) -> LOW(N, L)
HIGH(N, cons(M, L)) -> IFHIGH(le(M, N), N, cons(M, L))
HIGH(N, cons(M, L)) -> LE(M, N)
IFHIGH(true, N, cons(M, L)) -> HIGH(N, L)
IFHIGH(false, N, cons(M, L)) -> HIGH(N, L)
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. 


   R
     ↳DPs
       →DP Problem 1
         ↳Usable Rules (Innermost)
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules


Dependency Pair:

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


Rules:


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))))


Strategy:

innermost




As we are in the innermost case, we can delete all 15 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
           →DP Problem 6
             ↳Size-Change Principle
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules


Dependency Pair:

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


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. LE(s(X), s(Y)) -> LE(X, Y)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
2>2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
s(x1) -> s(x1)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳Usable Rules (Innermost)
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules


Dependency Pair:

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


Rules:


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))))


Strategy:

innermost




As we are in the innermost case, we can delete all 15 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
           →DP Problem 7
             ↳Size-Change Principle
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules


Dependency Pair:

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


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. APP(cons(N, L), Y) -> APP(L, Y)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
2=2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1
2=2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
cons(x1, x2) -> cons(x1, x2)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳Usable Rules (Innermost)
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules


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))


Rules:


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))))


Strategy:

innermost




As we are in the innermost case, we can delete all 12 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
           →DP Problem 8
             ↳Size-Change Principle
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules


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))


Rules:


le(s(X), 0) -> false
le(0, Y) -> true
le(s(X), s(Y)) -> le(X, Y)


Strategy:

innermost




We number the DPs as follows:
  1. IFLOW(false, N, cons(M, L)) -> LOW(N, L)
  2. IFLOW(true, N, cons(M, L)) -> LOW(N, L)
  3. LOW(N, cons(M, L)) -> IFLOW(le(M, N), N, cons(M, L))
and get the following Size-Change Graph(s):
{1, 2} , {1, 2}
2=1
3>2
{3} , {3}
1=2
2=3

which lead(s) to this/these maximal multigraph(s):
{1, 2} , {3}
2=2
3>3
{3} , {1, 2}
1=1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
cons(x1, x2) -> cons(x1, x2)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳Usable Rules (Innermost)
       →DP Problem 5
         ↳UsableRules


Dependency Pairs:

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))


Rules:


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))))


Strategy:

innermost




As we are in the innermost case, we can delete all 12 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
           →DP Problem 9
             ↳Size-Change Principle
       →DP Problem 5
         ↳UsableRules


Dependency Pairs:

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))


Rules:


le(s(X), 0) -> false
le(0, Y) -> true
le(s(X), s(Y)) -> le(X, Y)


Strategy:

innermost




We number the DPs as follows:
  1. IFHIGH(false, N, cons(M, L)) -> HIGH(N, L)
  2. IFHIGH(true, N, cons(M, L)) -> HIGH(N, L)
  3. HIGH(N, cons(M, L)) -> IFHIGH(le(M, N), N, cons(M, L))
and get the following Size-Change Graph(s):
{1, 2} , {1, 2}
2=1
3>2
{3} , {3}
1=2
2=3

which lead(s) to this/these maximal multigraph(s):
{3} , {1, 2}
1=1
2>2
{1, 2} , {3}
2=2
3>3

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
cons(x1, x2) -> cons(x1, x2)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳Usable Rules (Innermost)


Dependency Pairs:

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


Rules:


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))))


Strategy:

innermost




As we are in the innermost case, we can delete all 4 non-usable-rules.


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules
           →DP Problem 10
             ↳Negative Polynomial Order


Dependency Pairs:

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


Rules:


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))
le(s(X), 0) -> false
le(0, Y) -> true
le(s(X), s(Y)) -> le(X, Y)
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))


Strategy:

innermost




The following Dependency Pairs can be strictly oriented using the given order.

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


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

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))
le(s(X), 0) -> false
le(0, Y) -> true
le(s(X), s(Y)) -> le(X, Y)
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 Order with Interpretation:

POL( QUICKSORT(x1) ) = x1

POL( cons(x1, x2) ) = x2 + 1

POL( high(x1, x2) ) = x2

POL( low(x1, x2) ) = x2

POL( nil ) = 0

POL( ifhigh(x1, ..., x3) ) = x3

POL( le(x1, x2) ) = 0

POL( false ) = 0

POL( true ) = 0

POL( iflow(x1, ..., x3) ) = x3


This results in one new DP problem. 


   R
     ↳DPs
       →DP Problem 1
         ↳UsableRules
       →DP Problem 2
         ↳UsableRules
       →DP Problem 3
         ↳UsableRules
       →DP Problem 4
         ↳UsableRules
       →DP Problem 5
         ↳UsableRules
           →DP Problem 10
             ↳Neg POLO
             ...
               →DP Problem 11
                 ↳Dependency Graph


Dependency Pair:


Rules:


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))
le(s(X), 0) -> false
le(0, Y) -> true
le(s(X), s(Y)) -> le(X, Y)
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))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:01 minutes