MAYBE
0.09/0.17	MAYBE
0.09/0.17	
0.09/0.17	Problem:
0.09/0.17	 log(x,s(s(y))) -> cond(le(x,s(s(y))),x,y)
0.09/0.17	 cond(true(),x,y) -> s(0())
0.09/0.17	 cond(false(),x,y) -> double(log(x,square(s(s(y)))))
0.09/0.17	 le(0(),v) -> true()
0.09/0.17	 le(s(u),0()) -> false()
0.09/0.17	 le(s(u),s(v)) -> le(u,v)
0.09/0.17	 double(0()) -> 0()
0.09/0.17	 double(s(x)) -> s(s(double(x)))
0.09/0.17	 square(0()) -> 0()
0.09/0.17	 square(s(x)) -> s(plus(square(x),double(x)))
0.09/0.17	 plus(n,0()) -> n
0.09/0.17	 plus(n,s(m)) -> s(plus(n,m))
0.09/0.17	
0.09/0.17	Proof:
0.09/0.17	 Open
0.09/0.18	EOF