R
↳Dependency Pair Analysis
MINUS(s(x), s(y)) -> MINUS(x, y)
QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))
QUOT(s(x), s(y)) -> MINUS(x, y)
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)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳AFS
→DP Problem 7
↳AFS
MINUS(s(x), s(y)) -> MINUS(x, y)
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)) -> 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))))
MINUS(s(x), s(y)) -> MINUS(x, y)
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)) -> 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))))
quot > s
{true, le} > false
quicksort > {add, app}
MINUS(x1, x2) -> MINUS(x1, x2)
s(x1) -> s(x1)
minus(x1, x2) -> x1
quot(x1, x2) -> quot(x1, x2)
le(x1, x2) -> le(x1, x2)
app(x1, x2) -> app(x1, x2)
add(x1, x2) -> add(x1, x2)
low(x1, x2) -> x2
iflow(x1, x2, x3) -> x3
high(x1, x2) -> x2
ifhigh(x1, x2, x3) -> x3
quicksort(x1) -> quicksort(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 8
↳Dependency Graph
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳AFS
→DP Problem 7
↳AFS
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)) -> 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))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳AFS
→DP Problem 7
↳AFS
LE(s(x), s(y)) -> LE(x, y)
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)) -> 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))))
LE(s(x), s(y)) -> LE(x, y)
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)) -> 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))))
quot > {false, s}
{true, le}
quicksort > {add, app}
LE(x1, x2) -> LE(x1, x2)
s(x1) -> s(x1)
minus(x1, x2) -> x1
quot(x1, x2) -> quot(x1, x2)
le(x1, x2) -> le(x1, x2)
app(x1, x2) -> app(x1, x2)
add(x1, x2) -> add(x1, x2)
low(x1, x2) -> x2
iflow(x1, x2, x3) -> x3
high(x1, x2) -> x2
ifhigh(x1, x2, x3) -> x3
quicksort(x1) -> quicksort(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 9
↳Dependency Graph
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳AFS
→DP Problem 7
↳AFS
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)) -> 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))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Argument Filtering and Ordering
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳AFS
→DP Problem 7
↳AFS
APP(add(n, x), y) -> APP(x, y)
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)) -> 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))))
APP(add(n, x), y) -> APP(x, y)
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)) -> 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))))
high > {0, false}
quot > {0, false}
APP > {0, false}
low > {0, false}
nil > {0, false}
iflow > {0, false}
quicksort > {add, app} > {0, false}
minus > {0, false}
ifhigh > {0, false}
s > {0, false}
le > true > {0, false}
APP(x1, x2) -> APP(x1, x2)
add(x1, x2) -> add(x1, x2)
minus(x1, x2) -> minus(x1, x2)
s(x1) -> x1
quot(x1, x2) -> x2
le(x1, x2) -> le(x1, x2)
app(x1, x2) -> app(x1, x2)
low(x1, x2) -> x2
iflow(x1, x2, x3) -> x3
high(x1, x2) -> x2
ifhigh(x1, x2, x3) -> x3
quicksort(x1) -> quicksort(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 10
↳Dependency Graph
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳AFS
→DP Problem 7
↳AFS
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)) -> 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))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳Argument Filtering and Ordering
→DP Problem 5
↳AFS
→DP Problem 6
↳AFS
→DP Problem 7
↳AFS
QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))
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)) -> 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))))
QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))
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)) -> 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))))
quot > s > false
{true, le}
quicksort > {add, app}
QUOT(x1, x2) -> QUOT(x1, x2)
s(x1) -> s(x1)
minus(x1, x2) -> x1
quot(x1, x2) -> quot(x1, x2)
le(x1, x2) -> le(x1, x2)
app(x1, x2) -> app(x1, x2)
add(x1, x2) -> add(x1, x2)
low(x1, x2) -> x2
iflow(x1, x2, x3) -> x3
high(x1, x2) -> x2
ifhigh(x1, x2, x3) -> x3
quicksort(x1) -> quicksort(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 11
↳Dependency Graph
→DP Problem 5
↳AFS
→DP Problem 6
↳AFS
→DP Problem 7
↳AFS
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)) -> 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))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Argument Filtering and Ordering
→DP Problem 6
↳AFS
→DP Problem 7
↳AFS
IFLOW(false, n, add(m, x)) -> LOW(n, x)
IFLOW(true, n, add(m, x)) -> LOW(n, x)
LOW(n, add(m, x)) -> IFLOW(le(m, n), n, add(m, x))
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)) -> 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))))
IFLOW(false, n, add(m, x)) -> LOW(n, x)
IFLOW(true, n, add(m, x)) -> LOW(n, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
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)))
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))))
high > false
quot > s > false
0 > true > false
{LOW, IFLOW} > false
low > false
nil > false
iflow > false
quicksort > app > add > false
minus > false
ifhigh > false
le > false
LOW(x1, x2) -> LOW(x1, x2)
IFLOW(x1, x2, x3) -> IFLOW(x2, x3)
add(x1, x2) -> add(x1, x2)
le(x1, x2) -> le(x1, x2)
s(x1) -> s(x1)
minus(x1, x2) -> x1
quot(x1, x2) -> quot(x1, x2)
app(x1, x2) -> app(x1, x2)
low(x1, x2) -> x2
iflow(x1, x2, x3) -> x3
high(x1, x2) -> x2
ifhigh(x1, x2, x3) -> x3
quicksort(x1) -> quicksort(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 12
↳Dependency Graph
→DP Problem 6
↳AFS
→DP Problem 7
↳AFS
LOW(n, add(m, x)) -> IFLOW(le(m, n), n, add(m, x))
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)) -> 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))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Argument Filtering and Ordering
→DP Problem 7
↳AFS
IFHIGH(false, n, add(m, x)) -> HIGH(n, x)
IFHIGH(true, n, add(m, x)) -> HIGH(n, x)
HIGH(n, add(m, x)) -> IFHIGH(le(m, n), n, add(m, x))
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)) -> 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))))
IFHIGH(false, n, add(m, x)) -> HIGH(n, x)
IFHIGH(true, n, add(m, x)) -> HIGH(n, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
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)))
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))))
quot > s
0 > true
quicksort > app > add
{false, le}
IFHIGH(x1, x2, x3) -> x3
add(x1, x2) -> add(x1, x2)
HIGH(x1, x2) -> x2
le(x1, x2) -> le(x1, x2)
s(x1) -> s(x1)
minus(x1, x2) -> x1
quot(x1, x2) -> quot(x1, x2)
app(x1, x2) -> app(x1, x2)
low(x1, x2) -> x2
iflow(x1, x2, x3) -> x3
high(x1, x2) -> x2
ifhigh(x1, x2, x3) -> x3
quicksort(x1) -> quicksort(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳AFS
→DP Problem 13
↳Dependency Graph
→DP Problem 7
↳AFS
HIGH(n, add(m, x)) -> IFHIGH(le(m, n), n, add(m, x))
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)) -> 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))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳AFS
→DP Problem 7
↳Argument Filtering and Ordering
QUICKSORT(add(n, x)) -> QUICKSORT(high(n, x))
QUICKSORT(add(n, x)) -> QUICKSORT(low(n, x))
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)) -> 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))))
QUICKSORT(add(n, x)) -> QUICKSORT(high(n, x))
QUICKSORT(add(n, x)) -> QUICKSORT(low(n, x))
high(n, nil) -> nil
high(n, add(m, x)) -> ifhigh(le(m, n), n, add(m, x))
low(n, nil) -> nil
low(n, add(m, x)) -> iflow(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))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
iflow(true, n, add(m, x)) -> add(m, low(n, x))
iflow(false, n, add(m, x)) -> low(n, x)
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)))
app(nil, y) -> y
app(add(n, x), y) -> add(n, app(x, y))
quicksort(nil) -> nil
quicksort(add(n, x)) -> app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))
quot > s
{0, false}
quicksort > app > add
le > true
QUICKSORT(x1) -> QUICKSORT(x1)
add(x1, x2) -> add(x1, x2)
high(x1, x2) -> x2
low(x1, x2) -> x2
ifhigh(x1, x2, x3) -> x3
iflow(x1, x2, x3) -> x3
le(x1, x2) -> le(x1, x2)
s(x1) -> s(x1)
minus(x1, x2) -> x1
quot(x1, x2) -> quot(x1, x2)
app(x1, x2) -> app(x1, x2)
quicksort(x1) -> quicksort(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳AFS
→DP Problem 7
↳AFS
→DP Problem 14
↳Dependency Graph
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)) -> 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))))