(VAR x y z)

(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))
)

(COMMENT
tower(x) computes 2^2^...^2 with log_2(x) many 2's.
)