Termination Proof using AProVE

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'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_low, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(if_low, 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'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_high, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(if_high, 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))))

Innermost Termination of R to be shown.

     ↳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'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(if_low, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(if_low, 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'(if_low, true), n), app'(app'(add, m), x)) -> APP'(app'(add, m), app'(app'(low, n), x))
APP'(app'(app'(if_low, true), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(if_low, true), n), app'(app'(add, m), x)) -> APP'(low, n)
APP'(app'(app'(if_low, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(if_low, false), n), app'(app'(add, m), x)) -> APP'(low, n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(if_high, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(if_high, 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'(if_high, true), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(if_high, true), n), app'(app'(add, m), x)) -> APP'(high, n)
APP'(app'(app'(if_high, false), n), app'(app'(add, m), x)) -> APP'(app'(add, m), app'(app'(high, n), x))
APP'(app'(app'(if_high, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(if_high, 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.

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

The following remains to be proven:
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'(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'(if_high, false), n), app'(app'(add, m), x)) -> APP'(app'(high, n), x)
APP'(app'(app'(if_high, 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'(if_high, app'(app'(le, m), n)), n)
APP'(app'(high, n), app'(app'(add, m), x)) -> APP'(app'(app'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
APP'(app'(app'(if_low, false), n), app'(app'(add, m), x)) -> APP'(app'(low, n), x)
APP'(app'(app'(if_low, 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'(if_low, app'(app'(le, m), n)), n)
APP'(app'(low, n), app'(app'(add, m), x)) -> APP'(app'(app'(if_low, 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)

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'(if_low, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_low, true), n), app'(app'(add, m), x)) -> app'(app'(add, m), app'(app'(low, n), x))
app'(app'(app'(if_low, 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'(if_high, app'(app'(le, m), n)), n), app'(app'(add, m), x))
app'(app'(app'(if_high, true), n), app'(app'(add, m), x)) -> app'(app'(high, n), x)
app'(app'(app'(if_high, 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))))

Strategy:

innermost

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