(COMMENT conversion of binary to unary encoding and back)
(VAR x y xs ys lists)
(RULES
eq(0,0) -> true
eq(0,s(y)) -> false
eq(s(x),0) -> false
eq(s(x),s(y)) -> eq(x,y)

lt(0,s(y)) -> true
lt(x,0) -> false
lt(s(x),s(y)) -> lt(x,y)

bin2s(nil) -> 0
bin2s(cons(x,xs)) -> bin2ss(x,xs)
bin2ss(x,nil) -> x
bin2ss(x,cons(0,xs)) -> bin2ss(double(x),xs)
bin2ss(x,cons(1,xs)) -> bin2ss(s(double(x)),xs)

half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
log(0) -> 0
log(s(0)) -> 0
log(s(s(x))) -> s(log(half(s(s(x)))))

more(nil) -> nil
more(cons(xs,ys)) -> cons(cons(0,xs),cons(cons(1,xs),cons(xs,ys)))

s2bin(x) -> s2bin1(x,0,cons(nil,nil))
s2bin1(x,y,lists) -> if1(lt(y,log(x)),x,y,lists)
if1(true,x,y,lists) -> s2bin1(x,s(y),more(lists))
if1(false,x,y,lists) -> s2bin2(x,lists)
s2bin2(x,nil) -> bug_list_not
s2bin2(x,cons(xs,ys)) -> if2(eq(x,bin2s(xs)),x,xs,ys)
if2(true,x,xs,ys) -> xs
if2(false,x,xs,ys) -> s2bin2(x,ys)
)