MAYBE
160.60/55.85	MAYBE
160.60/55.85	
160.60/55.85	Problem:
160.60/55.85	 tower(x) -> f(a(),x,s(0()))
160.60/55.85	 f(a(),0(),y) -> y
160.60/55.85	 f(a(),s(x),y) -> f(b(),y,s(x))
160.60/55.85	 f(b(),y,x) -> f(a(),half(x),exp(y))
160.60/55.85	 exp(0()) -> s(0())
160.60/55.85	 exp(s(x)) -> double(exp(x))
160.60/55.85	 double(0()) -> 0()
160.60/55.85	 double(s(x)) -> s(s(double(x)))
160.60/55.85	 half(0()) -> double(0())
160.60/55.85	 half(s(0())) -> half(0())
160.60/55.85	 half(s(s(x))) -> s(half(x))
160.60/55.85	
160.60/55.85	Proof:
160.60/55.85	 Open
160.60/55.85	EOF