The proof is as follows. Here, one can say:

Hence we can output a zero. Now to express the remainder of the result as a recursive call, we want to find a stream *x*'' such that

This is achieved by setting (*x*'' = 2*x*). We can represent 2*x* using a signed
binary stream as the initial two digits of *x* scanned indicate that
it be expressed in the form (0::*x*').