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
↳Nar
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
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))))
innermost
MINUS(s(x), s(y)) -> MINUS(x, y)
MINUS(x1, x2) -> MINUS(x1, x2)
s(x1) -> s(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
↳Nar
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
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))))
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Nar
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
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))))
innermost
LE(s(x), s(y)) -> LE(x, y)
LE(x1, x2) -> LE(x1, x2)
s(x1) -> s(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
↳Nar
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
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))))
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Argument Filtering and Ordering
→DP Problem 4
↳AFS
→DP Problem 5
↳Nar
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
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))))
innermost
APP(add(n, x), y) -> APP(x, y)
APP(x1, x2) -> APP(x1, x2)
add(x1, x2) -> add(x1, x2)
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
↳Nar
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
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))))
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳Argument Filtering and Ordering
→DP Problem 5
↳Nar
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
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))))
innermost
QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
QUOT(x1, x2) -> QUOT(x1, x2)
s(x1) -> s(x1)
minus(x1, x2) -> 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
↳Nar
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
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))))
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Narrowing Transformation
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
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))))
innermost
three new Dependency Pairs are created:
LOW(n, add(m, x)) -> IFLOW(le(m, n), n, add(m, x))
LOW(n', add(0, x)) -> IFLOW(true, n', add(0, x))
LOW(0, add(s(x''), x)) -> IFLOW(false, 0, add(s(x''), x))
LOW(s(y'), add(s(x''), x)) -> IFLOW(le(x'', y'), s(y'), add(s(x''), x))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Nar
→DP Problem 12
↳Instantiation Transformation
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
LOW(s(y'), add(s(x''), x)) -> IFLOW(le(x'', y'), s(y'), add(s(x''), x))
LOW(0, add(s(x''), x)) -> IFLOW(false, 0, add(s(x''), x))
IFLOW(true, n, add(m, x)) -> LOW(n, x)
LOW(n', add(0, x)) -> IFLOW(true, n', add(0, 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)))
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
two new Dependency Pairs are created:
IFLOW(true, n, add(m, x)) -> LOW(n, x)
IFLOW(true, n', add(0, x'')) -> LOW(n', x'')
IFLOW(true, s(y'''), add(s(x'''''), x')) -> LOW(s(y'''), x')
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Nar
→DP Problem 12
↳Inst
...
→DP Problem 13
↳Instantiation Transformation
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
IFLOW(true, s(y'''), add(s(x'''''), x')) -> LOW(s(y'''), x')
LOW(0, add(s(x''), x)) -> IFLOW(false, 0, add(s(x''), x))
IFLOW(true, n', add(0, x'')) -> LOW(n', x'')
LOW(n', add(0, x)) -> IFLOW(true, n', add(0, x))
IFLOW(false, n, add(m, x)) -> LOW(n, x)
LOW(s(y'), add(s(x''), x)) -> IFLOW(le(x'', y'), s(y'), add(s(x''), 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))))
innermost
two new Dependency Pairs are created:
IFLOW(false, n, add(m, x)) -> LOW(n, x)
IFLOW(false, 0, add(s(x''''), x'')) -> LOW(0, x'')
IFLOW(false, s(y'''), add(s(x'''''), x')) -> LOW(s(y'''), x')
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Nar
→DP Problem 12
↳Inst
...
→DP Problem 14
↳Forward Instantiation Transformation
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
IFLOW(false, s(y'''), add(s(x'''''), x')) -> LOW(s(y'''), x')
LOW(s(y'), add(s(x''), x)) -> IFLOW(le(x'', y'), s(y'), add(s(x''), x))
IFLOW(false, 0, add(s(x''''), x'')) -> LOW(0, x'')
LOW(0, add(s(x''), x)) -> IFLOW(false, 0, add(s(x''), x))
IFLOW(true, n', add(0, x'')) -> LOW(n', x'')
LOW(n', add(0, x)) -> IFLOW(true, n', add(0, x))
IFLOW(true, s(y'''), add(s(x'''''), x')) -> LOW(s(y'''), 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))))
innermost
three new Dependency Pairs are created:
IFLOW(true, n', add(0, x'')) -> LOW(n', x'')
IFLOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
IFLOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
IFLOW(true, s(y'''), add(0, add(s(x''''), x'0))) -> LOW(s(y'''), add(s(x''''), x'0))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Nar
→DP Problem 12
↳Inst
...
→DP Problem 15
↳Forward Instantiation Transformation
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
IFLOW(true, s(y'''), add(s(x'''''), x')) -> LOW(s(y'''), x')
LOW(s(y'), add(s(x''), x)) -> IFLOW(le(x'', y'), s(y'), add(s(x''), x))
IFLOW(true, s(y'''), add(0, add(s(x''''), x'0))) -> LOW(s(y'''), add(s(x''''), x'0))
IFLOW(false, 0, add(s(x''''), x'')) -> LOW(0, x'')
LOW(0, add(s(x''), x)) -> IFLOW(false, 0, add(s(x''), x))
IFLOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
IFLOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
LOW(n', add(0, x)) -> IFLOW(true, n', add(0, x))
IFLOW(false, s(y'''), add(s(x'''''), x')) -> LOW(s(y'''), 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))))
innermost
three new Dependency Pairs are created:
LOW(n', add(0, x)) -> IFLOW(true, n', add(0, x))
LOW(n'', add(0, add(0, x'''''))) -> IFLOW(true, n'', add(0, add(0, x''''')))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IFLOW(true, 0, add(0, add(s(x''''''), x'0'')))
LOW(s(y'''''), add(0, add(s(x''''''), x'0''))) -> IFLOW(true, s(y'''''), add(0, add(s(x''''''), x'0'')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Nar
→DP Problem 12
↳Inst
...
→DP Problem 16
↳Forward Instantiation Transformation
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
IFLOW(true, s(y'''), add(0, add(s(x''''), x'0))) -> LOW(s(y'''), add(s(x''''), x'0))
LOW(s(y'''''), add(0, add(s(x''''''), x'0''))) -> IFLOW(true, s(y'''''), add(0, add(s(x''''''), x'0'')))
IFLOW(false, 0, add(s(x''''), x'')) -> LOW(0, x'')
LOW(0, add(s(x''), x)) -> IFLOW(false, 0, add(s(x''), x))
IFLOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IFLOW(true, 0, add(0, add(s(x''''''), x'0'')))
IFLOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
LOW(n'', add(0, add(0, x'''''))) -> IFLOW(true, n'', add(0, add(0, x''''')))
IFLOW(false, s(y'''), add(s(x'''''), x')) -> LOW(s(y'''), x')
LOW(s(y'), add(s(x''), x)) -> IFLOW(le(x'', y'), s(y'), add(s(x''), x))
IFLOW(true, s(y'''), add(s(x'''''), x')) -> LOW(s(y'''), 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))))
innermost
three new Dependency Pairs are created:
IFLOW(true, s(y'''), add(s(x'''''), x')) -> LOW(s(y'''), x')
IFLOW(true, s(y''''), add(s(x'''''), add(s(x''''), x0'))) -> LOW(s(y''''), add(s(x''''), x0'))
IFLOW(true, s(y''''), add(s(x'''''), add(0, add(0, x''''''')))) -> LOW(s(y''''), add(0, add(0, x''''''')))
IFLOW(true, s(y''''), add(s(x'''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(s(y''''), add(0, add(s(x''''''''), x'0'''')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Nar
→DP Problem 12
↳Inst
...
→DP Problem 17
↳Forward Instantiation Transformation
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
IFLOW(true, s(y''''), add(s(x'''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(s(y''''), add(0, add(s(x''''''''), x'0'''')))
IFLOW(true, s(y''''), add(s(x'''''), add(0, add(0, x''''''')))) -> LOW(s(y''''), add(0, add(0, x''''''')))
IFLOW(true, s(y''''), add(s(x'''''), add(s(x''''), x0'))) -> LOW(s(y''''), add(s(x''''), x0'))
LOW(s(y'''''), add(0, add(s(x''''''), x'0''))) -> IFLOW(true, s(y'''''), add(0, add(s(x''''''), x'0'')))
IFLOW(false, 0, add(s(x''''), x'')) -> LOW(0, x'')
LOW(0, add(s(x''), x)) -> IFLOW(false, 0, add(s(x''), x))
IFLOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IFLOW(true, 0, add(0, add(s(x''''''), x'0'')))
IFLOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
LOW(n'', add(0, add(0, x'''''))) -> IFLOW(true, n'', add(0, add(0, x''''')))
IFLOW(false, s(y'''), add(s(x'''''), x')) -> LOW(s(y'''), x')
LOW(s(y'), add(s(x''), x)) -> IFLOW(le(x'', y'), s(y'), add(s(x''), x))
IFLOW(true, s(y'''), add(0, add(s(x''''), x'0))) -> LOW(s(y'''), add(s(x''''), x'0))
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))))
innermost
three new Dependency Pairs are created:
IFLOW(false, 0, add(s(x''''), x'')) -> LOW(0, x'')
IFLOW(false, 0, add(s(x''''), add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
IFLOW(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> LOW(0, add(0, add(0, x''''''')))
IFLOW(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(0, add(0, add(s(x''''''''), x'0'''')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Nar
→DP Problem 12
↳Inst
...
→DP Problem 18
↳Forward Instantiation Transformation
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
IFLOW(true, s(y''''), add(s(x'''''), add(0, add(0, x''''''')))) -> LOW(s(y''''), add(0, add(0, x''''''')))
IFLOW(true, s(y''''), add(s(x'''''), add(s(x''''), x0'))) -> LOW(s(y''''), add(s(x''''), x0'))
IFLOW(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(0, add(0, add(s(x''''''''), x'0'''')))
IFLOW(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> LOW(0, add(0, add(0, x''''''')))
IFLOW(false, 0, add(s(x''''), add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(s(x''), x)) -> IFLOW(false, 0, add(s(x''), x))
IFLOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IFLOW(true, 0, add(0, add(s(x''''''), x'0'')))
IFLOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
LOW(n'', add(0, add(0, x'''''))) -> IFLOW(true, n'', add(0, add(0, x''''')))
IFLOW(false, s(y'''), add(s(x'''''), x')) -> LOW(s(y'''), x')
LOW(s(y'), add(s(x''), x)) -> IFLOW(le(x'', y'), s(y'), add(s(x''), x))
IFLOW(true, s(y'''), add(0, add(s(x''''), x'0))) -> LOW(s(y'''), add(s(x''''), x'0))
LOW(s(y'''''), add(0, add(s(x''''''), x'0''))) -> IFLOW(true, s(y'''''), add(0, add(s(x''''''), x'0'')))
IFLOW(true, s(y''''), add(s(x'''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(s(y''''), add(0, add(s(x''''''''), x'0'''')))
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))))
innermost
three new Dependency Pairs are created:
LOW(0, add(s(x''), x)) -> IFLOW(false, 0, add(s(x''), x))
LOW(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IFLOW(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
LOW(0, add(s(x'''), add(0, add(0, x''''''''')))) -> IFLOW(false, 0, add(s(x'''), add(0, add(0, x'''''''''))))
LOW(0, add(s(x'''), add(0, add(s(x''''''''''), x'0'''''')))) -> IFLOW(false, 0, add(s(x'''), add(0, add(s(x''''''''''), x'0''''''))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Nar
→DP Problem 12
↳Inst
...
→DP Problem 19
↳Forward Instantiation Transformation
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
IFLOW(true, s(y''''), add(s(x'''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(s(y''''), add(0, add(s(x''''''''), x'0'''')))
IFLOW(true, s(y''''), add(s(x'''''), add(s(x''''), x0'))) -> LOW(s(y''''), add(s(x''''), x0'))
IFLOW(false, s(y'''), add(s(x'''''), x')) -> LOW(s(y'''), x')
LOW(s(y'), add(s(x''), x)) -> IFLOW(le(x'', y'), s(y'), add(s(x''), x))
IFLOW(true, s(y'''), add(0, add(s(x''''), x'0))) -> LOW(s(y'''), add(s(x''''), x'0))
LOW(s(y'''''), add(0, add(s(x''''''), x'0''))) -> IFLOW(true, s(y'''''), add(0, add(s(x''''''), x'0'')))
IFLOW(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(0, add(0, add(s(x''''''''), x'0'''')))
LOW(0, add(s(x'''), add(0, add(s(x''''''''''), x'0'''''')))) -> IFLOW(false, 0, add(s(x'''), add(0, add(s(x''''''''''), x'0''''''))))
IFLOW(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> LOW(0, add(0, add(0, x''''''')))
LOW(0, add(s(x'''), add(0, add(0, x''''''''')))) -> IFLOW(false, 0, add(s(x'''), add(0, add(0, x'''''''''))))
IFLOW(false, 0, add(s(x''''), add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IFLOW(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
IFLOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IFLOW(true, 0, add(0, add(s(x''''''), x'0'')))
IFLOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
LOW(n'', add(0, add(0, x'''''))) -> IFLOW(true, n'', add(0, add(0, x''''')))
IFLOW(true, s(y''''), add(s(x'''''), add(0, add(0, x''''''')))) -> LOW(s(y''''), add(0, add(0, 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))))
innermost
three new Dependency Pairs are created:
IFLOW(false, s(y'''), add(s(x'''''), x')) -> LOW(s(y'''), x')
IFLOW(false, s(y''''), add(s(x'''''), add(s(x''''), x0'))) -> LOW(s(y''''), add(s(x''''), x0'))
IFLOW(false, s(y''''), add(s(x'''''), add(0, add(0, x''''''')))) -> LOW(s(y''''), add(0, add(0, x''''''')))
IFLOW(false, s(y''''), add(s(x'''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(s(y''''), add(0, add(s(x''''''''), x'0'''')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Nar
→DP Problem 12
↳Inst
...
→DP Problem 20
↳Forward Instantiation Transformation
→DP Problem 6
↳Remaining
→DP Problem 7
↳Remaining
IFLOW(false, s(y''''), add(s(x'''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(s(y''''), add(0, add(s(x''''''''), x'0'''')))
IFLOW(false, s(y''''), add(s(x'''''), add(0, add(0, x''''''')))) -> LOW(s(y''''), add(0, add(0, x''''''')))
IFLOW(false, s(y''''), add(s(x'''''), add(s(x''''), x0'))) -> LOW(s(y''''), add(s(x''''), x0'))
IFLOW(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(0, add(0, add(s(x''''''''), x'0'''')))
LOW(0, add(s(x'''), add(0, add(s(x''''''''''), x'0'''''')))) -> IFLOW(false, 0, add(s(x'''), add(0, add(s(x''''''''''), x'0''''''))))
IFLOW(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> LOW(0, add(0, add(0, x''''''')))
LOW(0, add(s(x'''), add(0, add(0, x''''''''')))) -> IFLOW(false, 0, add(s(x'''), add(0, add(0, x'''''''''))))
IFLOW(false, 0, add(s(x''''), add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IFLOW(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
IFLOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IFLOW(true, 0, add(0, add(s(x''''''), x'0'')))
IFLOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
LOW(n'', add(0, add(0, x'''''))) -> IFLOW(true, n'', add(0, add(0, x''''')))
IFLOW(true, s(y''''), add(s(x'''''), add(0, add(0, x''''''')))) -> LOW(s(y''''), add(0, add(0, x''''''')))
IFLOW(true, s(y''''), add(s(x'''''), add(s(x''''), x0'))) -> LOW(s(y''''), add(s(x''''), x0'))
LOW(s(y'), add(s(x''), x)) -> IFLOW(le(x'', y'), s(y'), add(s(x''), x))
IFLOW(true, s(y'''), add(0, add(s(x''''), x'0))) -> LOW(s(y'''), add(s(x''''), x'0))
LOW(s(y'''''), add(0, add(s(x''''''), x'0''))) -> IFLOW(true, s(y'''''), add(0, add(s(x''''''), x'0'')))
IFLOW(true, s(y''''), add(s(x'''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(s(y''''), add(0, add(s(x''''''''), x'0'''')))
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))))
innermost
three new Dependency Pairs are created:
LOW(s(y'), add(s(x''), x)) -> IFLOW(le(x'', y'), s(y'), add(s(x''), x))
LOW(s(y''), add(s(x''''), add(s(x''''0'), x0'''))) -> IFLOW(le(x'''', y''), s(y''), add(s(x''''), add(s(x''''0'), x0''')))
LOW(s(y''), add(s(x''''), add(0, add(0, x''''''''')))) -> IFLOW(le(x'''', y''), s(y''), add(s(x''''), add(0, add(0, x'''''''''))))
LOW(s(y''), add(s(x''''), add(0, add(s(x''''''''''), x'0'''''')))) -> IFLOW(le(x'''', y''), s(y''), add(s(x''''), add(0, add(s(x''''''''''), x'0''''''))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Nar
→DP Problem 6
↳Remaining Obligation(s)
→DP Problem 7
↳Remaining Obligation(s)
IFLOW(false, s(y''''), add(s(x'''''), add(s(x''''), x0'))) -> LOW(s(y''''), add(s(x''''), x0'))
IFLOW(true, s(y''''), add(s(x'''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(s(y''''), add(0, add(s(x''''''''), x'0'''')))
LOW(s(y''), add(s(x''''), add(0, add(s(x''''''''''), x'0'''''')))) -> IFLOW(le(x'''', y''), s(y''), add(s(x''''), add(0, add(s(x''''''''''), x'0''''''))))
IFLOW(false, s(y''''), add(s(x'''''), add(0, add(0, x''''''')))) -> LOW(s(y''''), add(0, add(0, x''''''')))
IFLOW(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(0, add(0, add(s(x''''''''), x'0'''')))
LOW(0, add(s(x'''), add(0, add(s(x''''''''''), x'0'''''')))) -> IFLOW(false, 0, add(s(x'''), add(0, add(s(x''''''''''), x'0''''''))))
IFLOW(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> LOW(0, add(0, add(0, x''''''')))
LOW(0, add(s(x'''), add(0, add(0, x''''''''')))) -> IFLOW(false, 0, add(s(x'''), add(0, add(0, x'''''''''))))
IFLOW(false, 0, add(s(x''''), add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IFLOW(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
IFLOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IFLOW(true, 0, add(0, add(s(x''''''), x'0'')))
IFLOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
LOW(n'', add(0, add(0, x'''''))) -> IFLOW(true, n'', add(0, add(0, x''''')))
IFLOW(true, s(y''''), add(s(x'''''), add(0, add(0, x''''''')))) -> LOW(s(y''''), add(0, add(0, x''''''')))
LOW(s(y''), add(s(x''''), add(0, add(0, x''''''''')))) -> IFLOW(le(x'''', y''), s(y''), add(s(x''''), add(0, add(0, x'''''''''))))
IFLOW(true, s(y''''), add(s(x'''''), add(s(x''''), x0'))) -> LOW(s(y''''), add(s(x''''), x0'))
LOW(s(y''), add(s(x''''), add(s(x''''0'), x0'''))) -> IFLOW(le(x'''', y''), s(y''), add(s(x''''), add(s(x''''0'), x0''')))
IFLOW(true, s(y'''), add(0, add(s(x''''), x'0))) -> LOW(s(y'''), add(s(x''''), x'0))
LOW(s(y'''''), add(0, add(s(x''''''), x'0''))) -> IFLOW(true, s(y'''''), add(0, add(s(x''''''), x'0'')))
IFLOW(false, s(y''''), add(s(x'''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(s(y''''), add(0, add(s(x''''''''), x'0'''')))
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))))
innermost
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))))
innermost
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))))
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Nar
→DP Problem 6
↳Remaining Obligation(s)
→DP Problem 7
↳Remaining Obligation(s)
IFLOW(false, s(y''''), add(s(x'''''), add(s(x''''), x0'))) -> LOW(s(y''''), add(s(x''''), x0'))
IFLOW(true, s(y''''), add(s(x'''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(s(y''''), add(0, add(s(x''''''''), x'0'''')))
LOW(s(y''), add(s(x''''), add(0, add(s(x''''''''''), x'0'''''')))) -> IFLOW(le(x'''', y''), s(y''), add(s(x''''), add(0, add(s(x''''''''''), x'0''''''))))
IFLOW(false, s(y''''), add(s(x'''''), add(0, add(0, x''''''')))) -> LOW(s(y''''), add(0, add(0, x''''''')))
IFLOW(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(0, add(0, add(s(x''''''''), x'0'''')))
LOW(0, add(s(x'''), add(0, add(s(x''''''''''), x'0'''''')))) -> IFLOW(false, 0, add(s(x'''), add(0, add(s(x''''''''''), x'0''''''))))
IFLOW(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> LOW(0, add(0, add(0, x''''''')))
LOW(0, add(s(x'''), add(0, add(0, x''''''''')))) -> IFLOW(false, 0, add(s(x'''), add(0, add(0, x'''''''''))))
IFLOW(false, 0, add(s(x''''), add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IFLOW(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
IFLOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IFLOW(true, 0, add(0, add(s(x''''''), x'0'')))
IFLOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
LOW(n'', add(0, add(0, x'''''))) -> IFLOW(true, n'', add(0, add(0, x''''')))
IFLOW(true, s(y''''), add(s(x'''''), add(0, add(0, x''''''')))) -> LOW(s(y''''), add(0, add(0, x''''''')))
LOW(s(y''), add(s(x''''), add(0, add(0, x''''''''')))) -> IFLOW(le(x'''', y''), s(y''), add(s(x''''), add(0, add(0, x'''''''''))))
IFLOW(true, s(y''''), add(s(x'''''), add(s(x''''), x0'))) -> LOW(s(y''''), add(s(x''''), x0'))
LOW(s(y''), add(s(x''''), add(s(x''''0'), x0'''))) -> IFLOW(le(x'''', y''), s(y''), add(s(x''''), add(s(x''''0'), x0''')))
IFLOW(true, s(y'''), add(0, add(s(x''''), x'0))) -> LOW(s(y'''), add(s(x''''), x'0))
LOW(s(y'''''), add(0, add(s(x''''''), x'0''))) -> IFLOW(true, s(y'''''), add(0, add(s(x''''''), x'0'')))
IFLOW(false, s(y''''), add(s(x'''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(s(y''''), add(0, add(s(x''''''''), x'0'''')))
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))))
innermost
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))))
innermost
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))))
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Nar
→DP Problem 6
↳Remaining Obligation(s)
→DP Problem 7
↳Remaining Obligation(s)
IFLOW(false, s(y''''), add(s(x'''''), add(s(x''''), x0'))) -> LOW(s(y''''), add(s(x''''), x0'))
IFLOW(true, s(y''''), add(s(x'''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(s(y''''), add(0, add(s(x''''''''), x'0'''')))
LOW(s(y''), add(s(x''''), add(0, add(s(x''''''''''), x'0'''''')))) -> IFLOW(le(x'''', y''), s(y''), add(s(x''''), add(0, add(s(x''''''''''), x'0''''''))))
IFLOW(false, s(y''''), add(s(x'''''), add(0, add(0, x''''''')))) -> LOW(s(y''''), add(0, add(0, x''''''')))
IFLOW(false, 0, add(s(x''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(0, add(0, add(s(x''''''''), x'0'''')))
LOW(0, add(s(x'''), add(0, add(s(x''''''''''), x'0'''''')))) -> IFLOW(false, 0, add(s(x'''), add(0, add(s(x''''''''''), x'0''''''))))
IFLOW(false, 0, add(s(x''''), add(0, add(0, x''''''')))) -> LOW(0, add(0, add(0, x''''''')))
LOW(0, add(s(x'''), add(0, add(0, x''''''''')))) -> IFLOW(false, 0, add(s(x'''), add(0, add(0, x'''''''''))))
IFLOW(false, 0, add(s(x''''), add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(s(x'''), add(s(x'''''''), x'0''))) -> IFLOW(false, 0, add(s(x'''), add(s(x'''''''), x'0'')))
IFLOW(true, 0, add(0, add(s(x''''), x'0))) -> LOW(0, add(s(x''''), x'0))
LOW(0, add(0, add(s(x''''''), x'0''))) -> IFLOW(true, 0, add(0, add(s(x''''''), x'0'')))
IFLOW(true, n''', add(0, add(0, x'''))) -> LOW(n''', add(0, x'''))
LOW(n'', add(0, add(0, x'''''))) -> IFLOW(true, n'', add(0, add(0, x''''')))
IFLOW(true, s(y''''), add(s(x'''''), add(0, add(0, x''''''')))) -> LOW(s(y''''), add(0, add(0, x''''''')))
LOW(s(y''), add(s(x''''), add(0, add(0, x''''''''')))) -> IFLOW(le(x'''', y''), s(y''), add(s(x''''), add(0, add(0, x'''''''''))))
IFLOW(true, s(y''''), add(s(x'''''), add(s(x''''), x0'))) -> LOW(s(y''''), add(s(x''''), x0'))
LOW(s(y''), add(s(x''''), add(s(x''''0'), x0'''))) -> IFLOW(le(x'''', y''), s(y''), add(s(x''''), add(s(x''''0'), x0''')))
IFLOW(true, s(y'''), add(0, add(s(x''''), x'0))) -> LOW(s(y'''), add(s(x''''), x'0))
LOW(s(y'''''), add(0, add(s(x''''''), x'0''))) -> IFLOW(true, s(y'''''), add(0, add(s(x''''''), x'0'')))
IFLOW(false, s(y''''), add(s(x'''''), add(0, add(s(x''''''''), x'0'''')))) -> LOW(s(y''''), add(0, add(s(x''''''''), x'0'''')))
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))))
innermost
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))))
innermost
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))))
innermost