(VAR x y ) (RULES half(0) -> 0 half(s(0)) -> 0 half(s(s(x))) -> s(half(x)) le(0, y) -> true le(s(x), 0) -> false le(s(x), s(y)) -> le(x, y) inc(0) -> 0 inc(s(x)) -> s(inc(x)) log(x) -> log2(x, 0) log2(x, y) -> if(le(x, s(0)), x, inc(y)) if(true, x, s(y)) -> y if(false, x, y) -> log2(half(x), y) )