Term Rewriting System R:
[x, y, n, m]
app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))

Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(minus, x)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(quot, app'(app'(minus, x), y))
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(minus, x)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(le, x)
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(add, n), app'(app'(app, x), y))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app, x)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(iflow, app'(app'(le, m), n))
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(le, m)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(add, m), app'(app'(low, n), x))
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(low, n)
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(low, n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(ifhigh, app'(app'(le, m), n))
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(le, m)
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(high, n)
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(add, m), app'(app'(high, n), x))
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(high, n)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app, app'(quicksort, app'(app'(low, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(quicksort, app'(app'(low, n), x))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(low, n)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(quicksort, app'(app'(high, n), x))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(high, n)

Furthermore, R contains one SCC.


   R
DPs
       →DP Problem 1
Narrowing Transformation


Dependency Pairs:

APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(quicksort, app'(app'(high, n), x))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(quicksort, app'(app'(low, n), x))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(add, m), app'(app'(high, n), x))
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(add, m), app'(app'(low, n), x))
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(add, n), app'(app'(app, x), y))
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(add, n), app'(app'(app, x), y))
two new Dependency Pairs are created:

APP'(app'(app, app'(app'(add, n), nil)), y'') -> APP'(app'(add, n), y'')
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), x''))), y'') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(app, x''), y'')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Narrowing Transformation


Dependency Pairs:

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), x''))), y'') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(app, x''), y'')))
APP'(app'(app, app'(app'(add, n), nil)), y'') -> APP'(app'(add, n), y'')
APP'(quicksort, app'(app'(add, n), x)) -> APP'(quicksort, app'(app'(high, n), x))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(quicksort, app'(app'(low, n), x))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(add, m), app'(app'(high, n), x))
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(add, m), app'(app'(low, n), x))
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(add, m), app'(app'(low, n), x))
two new Dependency Pairs are created:

APP'(app'(app'(iflow, true), n''), app'(app'(add, m), nil)) -> APP'(app'(add, m), nil)
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(iflow, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 3
Narrowing Transformation


Dependency Pairs:

APP'(app'(app'(iflow, true), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(iflow, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), nil)) -> APP'(app'(add, m), nil)
APP'(app'(app, app'(app'(add, n), nil)), y'') -> APP'(app'(add, n), y'')
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(quicksort, app'(app'(high, n), x))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(quicksort, app'(app'(low, n), x))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(add, m), app'(app'(high, n), x))
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), x''))), y'') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(app, x''), y'')))


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(add, m), app'(app'(high, n), x))
two new Dependency Pairs are created:

APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), nil)) -> APP'(app'(add, m), nil)
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(ifhigh, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 4
Narrowing Transformation


Dependency Pairs:

APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(ifhigh, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), nil)) -> APP'(app'(add, m), nil)
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), nil)) -> APP'(app'(add, m), nil)
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), x''))), y'') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(app, x''), y'')))
APP'(app'(app, app'(app'(add, n), nil)), y'') -> APP'(app'(add, n), y'')
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(quicksort, app'(app'(high, n), x))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(quicksort, app'(app'(low, n), x))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(iflow, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP'(quicksort, app'(app'(add, n), x)) -> APP'(quicksort, app'(app'(low, n), x))
two new Dependency Pairs are created:

APP'(quicksort, app'(app'(add, n''), nil)) -> APP'(quicksort, nil)
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(iflow, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 5
Narrowing Transformation


Dependency Pairs:

APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(iflow, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), nil)) -> APP'(app'(add, m), nil)
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(iflow, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), nil)) -> APP'(app'(add, m), nil)
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), x''))), y'') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(app, x''), y'')))
APP'(app'(app, app'(app'(add, n), nil)), y'') -> APP'(app'(add, n), y'')
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(quicksort, app'(app'(high, n), x))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(ifhigh, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP'(quicksort, app'(app'(add, n), x)) -> APP'(quicksort, app'(app'(high, n), x))
two new Dependency Pairs are created:

APP'(quicksort, app'(app'(add, n''), nil)) -> APP'(quicksort, nil)
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(ifhigh, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 6
Narrowing Transformation


Dependency Pairs:

APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(ifhigh, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(ifhigh, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), nil)) -> APP'(app'(add, m), nil)
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(iflow, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), nil)) -> APP'(app'(add, m), nil)
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), x''))), y'') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(app, x''), y'')))
APP'(app'(app, app'(app'(add, n), nil)), y'') -> APP'(app'(add, n), y'')
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(iflow, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP'(app'(app, app'(app'(add, n), nil)), y'') -> APP'(app'(add, n), y'')
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 7
Narrowing Transformation


Dependency Pairs:

APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(iflow, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(ifhigh, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), nil)) -> APP'(app'(add, m), nil)
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(iflow, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), nil)) -> APP'(app'(add, m), nil)
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), x''))), y'') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(app, x''), y'')))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(ifhigh, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), x''))), y'') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(app, x''), y'')))
two new Dependency Pairs are created:

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), nil))), y''') -> APP'(app'(add, n), app'(app'(add, n''), y'''))
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), x')))), y''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(app, x'), y'''))))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 8
Narrowing Transformation


Dependency Pairs:

APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(ifhigh, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(ifhigh, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), x')))), y''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(app, x'), y'''))))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), nil)) -> APP'(app'(add, m), nil)
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(iflow, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), nil))), y''') -> APP'(app'(add, n), app'(app'(add, n''), y'''))
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), nil)) -> APP'(app'(add, m), nil)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(iflow, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP'(app'(app'(iflow, true), n''), app'(app'(add, m), nil)) -> APP'(app'(add, m), nil)
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 9
Narrowing Transformation


Dependency Pairs:

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), x')))), y''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(app, x'), y'''))))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(iflow, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(ifhigh, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), nil))), y''') -> APP'(app'(add, n), app'(app'(add, n''), y'''))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), nil)) -> APP'(app'(add, m), nil)
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(iflow, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(ifhigh, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), nil)) -> APP'(app'(add, m), nil)
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 10
Narrowing Transformation


Dependency Pairs:

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), nil))), y''') -> APP'(app'(add, n), app'(app'(add, n''), y'''))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(ifhigh, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(iflow, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(ifhigh, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(iflow, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), x')))), y''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(app, x'), y'''))))


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), nil))), y''') -> APP'(app'(add, n), app'(app'(add, n''), y'''))
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 11
Narrowing Transformation


Dependency Pairs:

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), x')))), y''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(app, x'), y'''))))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(iflow, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(ifhigh, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(iflow, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(ifhigh, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), x')))), y''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(app, x'), y'''))))
two new Dependency Pairs are created:

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), nil)))), y'''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), y'''')))
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), x''))))), y'''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(app, x''), y'''')))))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 12
Narrowing Transformation


Dependency Pairs:

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), x''))))), y'''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(app, x''), y'''')))))
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), nil)))), y'''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), y'''')))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(ifhigh, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(ifhigh, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(iflow, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(iflow, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), nil)))), y'''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), y'''')))
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 13
Narrowing Transformation


Dependency Pairs:

APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(ifhigh, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(iflow, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(ifhigh, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(iflow, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), x''))))), y'''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(app, x''), y'''')))))


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), x''))))), y'''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(app, x''), y'''')))))
two new Dependency Pairs are created:

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), nil))))), y''''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), y'''''))))
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), x')))))), y''''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), app'(app'(app, x'), y'''''))))))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 14
Narrowing Transformation


Dependency Pairs:

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), x')))))), y''''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), app'(app'(app, x'), y'''''))))))
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), nil))))), y''''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), y'''''))))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(iflow, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(ifhigh, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(iflow, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(ifhigh, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), nil))))), y''''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), y'''''))))
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 15
Narrowing Transformation


Dependency Pairs:

APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(ifhigh, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(iflow, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(ifhigh, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(iflow, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), x')))))), y''''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), app'(app'(app, x'), y'''''))))))


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), x')))))), y''''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), app'(app'(app, x'), y'''''))))))
two new Dependency Pairs are created:

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), nil)))))), y'''''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), y'''''')))))
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), app'(app'(add, n'2), x''))))))), y'''''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), app'(app'(add, n'2), app'(app'(app, x''), y'''''')))))))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 16
Narrowing Transformation


Dependency Pairs:

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), app'(app'(add, n'2), x''))))))), y'''''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), app'(app'(add, n'2), app'(app'(app, x''), y'''''')))))))
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), nil)))))), y'''''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), y'''''')))))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(iflow, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(ifhigh, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(iflow, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(ifhigh, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), nil)))))), y'''''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), y'''''')))))
no new Dependency Pairs are created.
The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Nar
           →DP Problem 2
Nar
             ...
               →DP Problem 17
Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(ifhigh, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(quicksort, app'(app'(add, n''), app'(app'(add, m'), x''))) -> APP'(quicksort, app'(app'(app'(iflow, app'(app'(le, m'), n'')), n''), app'(app'(add, m'), x'')))
APP'(app'(app'(ifhigh, false), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(ifhigh, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(app'(app'(iflow, true), n''), app'(app'(add, m), app'(app'(add, m''), x''))) -> APP'(app'(add, m), app'(app'(app'(iflow, app'(app'(le, m''), n'')), n''), app'(app'(add, m''), x'')))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(high, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(add, n), app'(quicksort, app'(app'(high, n), x)))
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(low, n), x)
APP'(quicksort, app'(app'(add, n), x)) -> APP'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))
APP'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(ifhigh, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(le, m), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(iflow, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app, app'(app'(add, n), x)), y) -> APP'(app'(app, x), y)
APP'(app'(le, app'(s, x)), app'(s, y)) -> APP'(app'(le, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(app, app'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), app'(app'(add, n'2), x''))))))), y'''''') -> APP'(app'(add, n), app'(app'(add, n''), app'(app'(add, n'''), app'(app'(add, n'0), app'(app'(add, n'1), app'(app'(add, n'2), app'(app'(app, x''), y'''''')))))))


Rules:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(le, 0), y) -> true
app'(app'(le, app'(s, x)), 0) -> false
app'(app'(le, app'(s, x)), app'(s, y)) -> app'(app'(le, x), y)
app'(app'(app, nil), y) -> y
app'(app'(app, app'(app'(add, n), x)), y) -> app'(app'(add, n), app'(app'(app, x), y))
app'(app'(low, n), nil) -> nil
app'(app'(low, n), app'(app'(add, m), x)) -> app'(app'(app'(iflow, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(iflow, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(iflow, false), n), app'(app'(add, m), x)) -> app'(app'(low, n), x)
app'(app'(high, n), nil) -> nil
app'(app'(high, n), app'(app'(add, m), x)) -> app'(app'(app'(ifhigh, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(ifhigh, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(ifhigh, false), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(high, n), x))
app'(quicksort, nil) -> nil
app'(quicksort, app'(app'(add, n), x)) -> app'(app'(app, app'(quicksort, app'(app'(low, n), x))), app'(app'(add, n), app'(quicksort, app'(app'(high, n), x))))




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