It is possible to define two simple functions to add or subtract the number one from the number represented by a from a stream of signed binary digits (provided the stream represents a number in a suitable interval). Let us define these functions as follows:

These functions may be implemented as follows:

= | |

f(0::x') | = |

f(1::x') | = |

g(0::x') | = |

g(1::x') | = |

The proof of correctness for such definitions is as follows. Let us
consider the function *f* applied to a numeral *x*. The proof for the
function *g* is similar. We use to denote the number
represented by the numeral *x*. We examine the three cases in turn:

**Input***x*starts with the digit 1:- If the input
*x*starts with a one we know that . Hence we can output an infinite stream of ones () by the function definition. **Input***x*starts with the digit :- If the input is
*x*is of the form (0::*x*'), we know that*x*represents the value . Now, using the properties described in section 3.6.2: **Input***x*starts with the digit :- If the input
*x*is of the form , we can simply add the number one at the first digit and return (1::*x*'):