(COMMENT harder variant of Ex 3.15 in AG01)
(VAR x y b1 b2 b3)
(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)))
)