(COMMENT
log(x) by doubling 1 repeatedly, until
x is reached
)
(VAR x y z)
(RULES
le(s(x), 0) -> false
le(0, y) -> true
le(s(x), s(y)) -> le(x, y)

double(0) -> 0
double(s(x)) -> s(s(double(x)))

log(0) -> logError
log(s(x)) -> loop(s(x),s(0),0)

loop(x,s(y),z) -> if(le(x,s(y)),x,s(y),z)
if(true,x,y,z) -> z
if(false,x,y,z) -> loop(x,double(y),s(z))
)