(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
average(x, y) → if(ge(x, y), x, y)
if(true, x, y) → averIter(y, x, y)
if(false, x, y) → averIter(x, y, x)
averIter(x, y, z) → ifIter(ge(x, y), x, y, z)
ifIter(true, x, y, z) → z
ifIter(false, x, y, z) → averIter(plus(x, s(s(s(0)))), plus(y, s(0)), plus(z, s(0)))
append(nil, y) → y
append(cons(n, x), y) → cons(n, app(x, y))
low(n, nil) → nil
low(n, cons(m, x)) → if_low(ge(m, n), n, cons(m, x))
if_low(false, n, cons(m, x)) → cons(m, low(n, x))
if_low(true, n, cons(m, x)) → low(n, x)
high(n, nil) → nil
high(n, cons(m, x)) → if_high(ge(m, n), n, cons(m, x))
if_high(false, n, cons(m, x)) → high(n, x)
if_high(true, n, cons(m, x)) → cons(average(m, m), high(n, x))
quicksort(x) → ifquick(isempty(x), x)
ifquick(true, x) → nil
ifquick(false, x) → append(quicksort(low(head(x), tail(x))), cons(tail(x), quicksort(high(head(x), tail(x)))))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
isempty(nil) → true
isempty(cons(n, x)) → false
head(nil) → error
head(cons(n, x)) → n
tail(nil) → nil
tail(cons(n, x)) → x
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → b
a → c
Q is empty.