MAYBE
0.18/0.20	MAYBE
0.18/0.20	
0.18/0.20	Problem:
0.18/0.20	 eq(0(),0()) -> true()
0.18/0.20	 eq(0(),s(y)) -> false()
0.18/0.20	 eq(s(x),0()) -> false()
0.18/0.20	 eq(s(x),s(y)) -> eq(x,y)
0.18/0.20	 lt(0(),s(y)) -> true()
0.18/0.20	 lt(x,0()) -> false()
0.18/0.20	 lt(s(x),s(y)) -> lt(x,y)
0.18/0.20	 bin2s(nil()) -> 0()
0.18/0.20	 bin2s(cons(x,xs)) -> bin2ss(x,xs)
0.18/0.20	 bin2ss(x,nil()) -> x
0.18/0.20	 bin2ss(x,cons(0(),xs)) -> bin2ss(double(x),xs)
0.18/0.20	 bin2ss(x,cons(1(),xs)) -> bin2ss(s(double(x)),xs)
0.18/0.20	 half(0()) -> 0()
0.18/0.20	 half(s(0())) -> 0()
0.18/0.20	 half(s(s(x))) -> s(half(x))
0.18/0.20	 log(0()) -> 0()
0.18/0.20	 log(s(0())) -> 0()
0.18/0.20	 log(s(s(x))) -> s(log(half(s(s(x)))))
0.18/0.20	 more(nil()) -> nil()
0.18/0.20	 more(cons(xs,ys)) -> cons(cons(0(),xs),cons(cons(1(),xs),cons(xs,ys)))
0.18/0.20	 s2bin(x) -> s2bin1(x,0(),cons(nil(),nil()))
0.18/0.20	 s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists)
0.18/0.20	 if1(true(),x,y,lists) -> s2bin1(x,s(y),more(lists))
0.18/0.20	 if1(false(),x,y,lists) -> s2bin2(x,lists)
0.18/0.20	 s2bin2(x,nil()) -> bug_list_not()
0.18/0.20	 s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys)
0.18/0.20	 if2(true(),x,xs,ys) -> xs
0.18/0.20	 if2(false(),x,xs,ys) -> s2bin2(x,ys)
0.18/0.20	
0.18/0.20	Proof:
0.18/0.20	 Open
0.18/0.20	EOF