(COMMENT harder variant of AG01 4.24)
(VAR b x y)
(RULES
empty(nil) -> true
empty(cons(x,y)) -> false
tail(nil) -> nil
tail(cons(x,y)) -> y
head(cons(x,y)) -> x

zero(0) -> true
zero(s(x)) -> false
p(0) -> 0
p(s(0)) -> 0
p(s(s(x))) -> s(p(s(x)))

intlist(x) -> if_intlist(empty(x),x)
if_intlist(true,x) -> nil
if_intlist(false,x) -> cons(s(head(x)),intlist(tail(x)))

int(x,y) -> if_int(zero(x),zero(y),x,y)
if_int(true,b,x,y) -> if1(b,x,y)
if_int(false,b,x,y) -> if2(b,x,y)
if1(true,x,y) -> cons(0,nil)
if1(false,x,y) -> cons(0,int(s(0),y))
if2(true,x,y) -> nil
if2(false,x,y) -> intlist(int(p(x),p(y)))
)