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

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
Polynomial Ordering
       →DP Problem 2
Remaining
       →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))))





The following dependency pair can be strictly oriented:

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


Additionally, the following rules can be oriented:

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


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(LE(x1, x2))=  x1  
  POL(if_low(x1, x2, x3))=  0  
  POL(false)=  0  
  POL(high(x1, x2))=  0  
  POL(low(x1, x2))=  0  
  POL(true)=  0  
  POL(add(x1, x2))=  0  
  POL(0)=  0  
  POL(quicksort(x1))=  0  
  POL(if_high(x1, x2, x3))=  0  
  POL(nil)=  0  
  POL(s(x1))=  1 + x1  
  POL(le(x1, x2))=  0  
  POL(app(x1, x2))=  x2  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
           →DP Problem 6
Dependency Graph
       →DP Problem 2
Remaining
       →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))))





Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Remaining Obligation(s)
       →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
Polo
       →DP Problem 2
Remaining Obligation(s)
       →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
Polo
       →DP Problem 2
Remaining Obligation(s)
       →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
Polo
       →DP Problem 2
Remaining Obligation(s)
       →DP Problem 3
Remaining Obligation(s)
       →DP Problem 4
Remaining Obligation(s)
       →DP Problem 5
Remaining Obligation(s)




The following remains to be proven:

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