Output zero case:

If the numerator input starts with a zero, or two digits which could be rewritten as a zero and another digit, the algorithm is simple.

$$\begin{array} {lll} \mathrm{divide}(0::x', & y ) = & 0::\mat... ...y) = & 0::\mathrm{divide}(\overline{1}::x', \ y)\ \end{array}$$

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

$$x \in \Big [-\frac{1}{2},\frac{1}{2}\Big ], \qquad y \in \Big [\frac{1}{4},1 \Big]$$

$$\Rightarrow \frac{x}{4y} \in \Big[ -\frac{1}{2},\frac{1}{2}\Big]$$

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

$$\frac{x}{4y} = 0 :: \mathrm{divide}(x'',\ 4y) \qquad = 0 \oplus \frac{x''}{4y}$$

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