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'(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 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'(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''), 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'(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'(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 9
                 ↳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'(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'(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))))




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