(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
p(s(x)) → x
p(0) → 0
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
average(x, y) → if(le(x, 0), le(y, 0), le(y, s(0)), le(y, s(s(0))), x, y)
if(true, b1, b2, b3, x, y) → if2(b1, b2, b3, x, y)
if(false, b1, b2, b3, x, y) → average(p(x), s(y))
if2(true, b2, b3, x, y) → 0
if2(false, b2, b3, x, y) → if3(b2, b3, x, y)
if3(true, b3, x, y) → 0
if3(false, b3, x, y) → if4(b3, x, y)
if4(true, x, y) → s(0)
if4(false, x, y) → average(s(x), p(p(y)))
Q is empty.