(COMMENT harder, tail recursive variant of AG01 3.7) (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) )