MAYBE

Problem:
 half(0()) -> 0()
 half(s(0())) -> 0()
 half(s(s(x))) -> s(half(x))
 bits(0()) -> 0()
 bits(s(x)) -> s(bits(half(s(x))))

Proof:
 Open