(VAR x y )
(RULES 
        tower(x) -> f(a, x, s(0))
        f(a, 0, y) -> y
        f(a, s(x), y) -> f(b, y, s(x))
        f(b, y, x) -> f(a, half(x), exp(y))
        exp(0) -> s(0)
        exp(s(x)) -> double(exp(x))
        double(0) -> 0
        double(s(x)) -> s(s(double(x)))
        half(0) -> double(0)
        half(s(0)) -> half(0)
        half(s(s(x))) -> s(half(x))
        
)