MAYBE 0.08/0.17 MAYBE 0.08/0.17 0.08/0.17 Problem: 0.08/0.17 half(0()) -> 0() 0.08/0.17 half(s(0())) -> 0() 0.08/0.17 half(s(s(x))) -> s(half(x)) 0.08/0.17 le(0(),y) -> true() 0.08/0.17 le(s(x),0()) -> false() 0.08/0.17 le(s(x),s(y)) -> le(x,y) 0.08/0.17 inc(0()) -> 0() 0.08/0.17 inc(s(x)) -> s(inc(x)) 0.08/0.17 log(x) -> log2(x,0()) 0.08/0.17 log2(x,y) -> if(le(x,s(0())),x,inc(y)) 0.08/0.17 if(true(),x,s(y)) -> y 0.08/0.17 if(false(),x,y) -> log2(half(x),y) 0.08/0.17 0.08/0.17 Proof: 0.08/0.17 Open 0.08/0.18 EOF