We give a denotational semantics for the language L given by the
grammar

b:bit ::= "0" | "1"

n:bin ::= b | n b

The semantics is given by the model N, the natural numbers, and the
interpretation

[[ "0" ]] := 0
[[ "1" ]] := 1
[[ n b ]] := 2 * [[n]] + [[b]]

In the lecture, we have recursively defined the operation 0(n), which
prefixes a binary numeral n with a leading "0" as follows.

O("0") := "0" "0"
O("1") := "0" "1"
O(n b) := O(n) b

We have given an operational semantics => via the rules

"0" => "0" "0"

"1" => "0" "1"

If n => m, then n b => m b.


Exercises:
=========

-- Define the operation S(n), 
   which computes the binary numeral which is the successor of n. 

-- Give an operational semantics for S(n), in the form of a relation 
   n => m such that S(n) = m iff n => m (and prove this!)

-- Prove [[S(n)]] = [[n]] + 1 for all n.

( As a hint you may first try:
-- Prove that 0(n) = m iff n => m

-- Prove [[0(n)]] = [[n]] for all n.
)