(VAR x ) (RULES half(0) -> 0 half(s(0)) -> 0 half(s(s(x))) -> s(half(x)) s(log(0)) -> s(0) log(s(x)) -> s(log(half(s(x)))) )