(VAR x y )
(RULES 
        f(tt,x) -> f(eq(x,half(double(x))),s(x))
        eq(s(x),s(y)) -> eq(x,y)
        eq(0,0) -> tt
        double(s(x)) -> s(s(double(x)))
        double(0) -> 0
        half(s(s(x))) -> s(half(x))
        half(0) -> 0
        
)