(VAR x y )
(STRATEGY INNERMOST)
(RULES 
        lt(0,s(x)) -> true
        lt(x,0) -> false
        lt(s(x),s(y)) -> lt(x,y)
        logarithm(x) -> ifa(lt(0,x),x)
        ifa(true,x) -> help(x,1)
        ifa(false,x) -> logZeroError
        help(x,y) -> ifb(lt(y,x),x,y)
        ifb(true,x,y) -> help(half(x),s(y))
        ifb(false,x,y) -> y
        half(0) -> 0
        half(s(0)) -> 0
        half(s(s(x))) -> s(half(x))
        
)