Term Rewriting System R:
[y, x, n, m]
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)) -> iflow(le(m, n), n, add(m, x))
iflow(true, n, add(m, x)) -> add(m, low(n, x))
iflow(false, n, add(m, x)) -> low(n, x)
high(n, nil) -> nil
high(n, add(m, x)) -> ifhigh(le(m, n), n, add(m, x))
ifhigh(true, n, add(m, x)) -> high(n, x)
ifhigh(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))))

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(add(n, x), y) -> APP(x, y)
LOW(n, add(m, x)) -> IFLOW(le(m, n), n, add(m, x))
LOW(n, add(m, x)) -> LE(m, n)
IFLOW(true, n, add(m, x)) -> LOW(n, x)
IFLOW(false, n, add(m, x)) -> LOW(n, x)
HIGH(n, add(m, x)) -> IFHIGH(le(m, n), n, add(m, x))
HIGH(n, add(m, x)) -> LE(m, n)
IFHIGH(true, n, add(m, x)) -> HIGH(n, x)
IFHIGH(false, n, add(m, x)) -> HIGH(n, x)
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)

Furthermore, R contains five SCCs.


   R
DPs
       →DP Problem 1
Argument Filtering and Ordering
       →DP Problem 2
AFS
       →DP Problem 3
Remaining
       →DP Problem 4
Remaining
       →DP Problem 5
Remaining


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(add(n, x), y) -> add(n, app(x, y))
low(n, nil) -> nil
low(n, add(m, x)) -> iflow(le(m, n), n, add(m, x))
iflow(true, n, add(m, x)) -> add(m, low(n, x))
iflow(false, n, add(m, x)) -> low(n, x)
high(n, nil) -> nil
high(n, add(m, x)) -> ifhigh(le(m, n), n, add(m, x))
ifhigh(true, n, add(m, x)) -> high(n, x)
ifhigh(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))))


Strategy:

innermost




The following dependency pair can be strictly oriented:

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


There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
LE(x1, x2) -> LE(x1, x2)
s(x1) -> s(x1)


   R
DPs
       →DP Problem 1
AFS
           →DP Problem 6
Dependency Graph
       →DP Problem 2
AFS
       →DP Problem 3
Remaining
       →DP Problem 4
Remaining
       →DP Problem 5
Remaining


Dependency Pair:


Rules:


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)) -> iflow(le(m, n), n, add(m, x))
iflow(true, n, add(m, x)) -> add(m, low(n, x))
iflow(false, n, add(m, x)) -> low(n, x)
high(n, nil) -> nil
high(n, add(m, x)) -> ifhigh(le(m, n), n, add(m, x))
ifhigh(true, n, add(m, x)) -> high(n, x)
ifhigh(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))))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
Argument Filtering and Ordering
       →DP Problem 3
Remaining
       →DP Problem 4
Remaining
       →DP Problem 5
Remaining


Dependency Pair:

APP(add(n, x), y) -> APP(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(add(n, x), y) -> add(n, app(x, y))
low(n, nil) -> nil
low(n, add(m, x)) -> iflow(le(m, n), n, add(m, x))
iflow(true, n, add(m, x)) -> add(m, low(n, x))
iflow(false, n, add(m, x)) -> low(n, x)
high(n, nil) -> nil
high(n, add(m, x)) -> ifhigh(le(m, n), n, add(m, x))
ifhigh(true, n, add(m, x)) -> high(n, x)
ifhigh(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))))


Strategy:

innermost




The following dependency pair can be strictly oriented:

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


There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
APP(x1, x2) -> APP(x1, x2)
add(x1, x2) -> add(x1, x2)


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
           →DP Problem 7
Dependency Graph
       →DP Problem 3
Remaining
       →DP Problem 4
Remaining
       →DP Problem 5
Remaining


Dependency Pair:


Rules:


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)) -> iflow(le(m, n), n, add(m, x))
iflow(true, n, add(m, x)) -> add(m, low(n, x))
iflow(false, n, add(m, x)) -> low(n, x)
high(n, nil) -> nil
high(n, add(m, x)) -> ifhigh(le(m, n), n, add(m, x))
ifhigh(true, n, add(m, x)) -> high(n, x)
ifhigh(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))))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Remaining Obligation(s)
       →DP Problem 4
Remaining Obligation(s)
       →DP Problem 5
Remaining Obligation(s)




The following remains to be proven:


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Remaining Obligation(s)
       →DP Problem 4
Remaining Obligation(s)
       →DP Problem 5
Remaining Obligation(s)




The following remains to be proven:


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Remaining Obligation(s)
       →DP Problem 4
Remaining Obligation(s)
       →DP Problem 5
Remaining Obligation(s)




The following remains to be proven:

Innermost Termination of R could not be shown.
Duration:
0:00 minutes