While working on UVa 11173, I found that there are numerous implementations of binary to gray conversion with a right shift and an xor operation, like this wikipedia article and this code snnipet. Unfortunately, none of them explain why this algorithm works. I was curious and decided to prove it on my own.

At first glance, there is no obvious solution because nothing in my knowledge base links the binary form of a number to another form except for radix conversion. Yet the reflection procedure described in the problem hardly has anything to do with radix. As aways, when there is no easy proof, go with induction. The target is to prove

Apparently the length of the binary/Gray number is what we want to base our induction on. The base case is trivial - all we need to do is to manually verify that \(0 = 0 \oplus (0 \gg 1)\) and \(1 = 1 \oplus (1 \gg 1)\). The tricky part is the induction step. Our induction hypothesis is that for any binary number \(n\) of length \(k\), \(G(n) = n \oplus (n \gg 1)\). And we want to prove the same holds when the length comes to \(k+1\).

We will denote the binary form of a number \(n\) with length \(k\) as follows:

and the Gray form as follows:

The induction hypothesis then becomes that for each \(n\) of length \(k\),

And the target to prove is for each \(n\) of length \(k+1\),

It might (or might not) be possible to prove this vertical addition
* forward* (top-down), i.e. the xor of a number and its shifted version
gives the correct Gray code, but it is actually very hard to find out the
“correct Gray code”, especially when the most significant bit (\(b_{k}\)) is
\(1\). Meanwhile, if we look at the construction procedure, the generation
is actually driven by (reflecting) the Gray codes rather than the binary
numbers. This reminds us to prove it

*- from the Gray code back to the binary format.*

**backward**Any Gray code of length \(k+1\) can be seen as the concatenation of \(0\) or \(1\), with a Gray code of length \(k\).

- if it’s \(0g_{k-1}\cdots g_0\): it is pretty straightforward to see that its binary form is \(0b_{k-1}\cdots b_0\), which is the same old Gray code prepended with a \(0\). Because of our hypothesis for \(n=k\) case, it is easy to verify the conclusion holds for \(n=k+1\) case as well.
- if it’s \(1g_{k-1}\cdots g_0\): since we already know from the step above that the binary form of \(0g_{k-1}\cdots g_0\) is \(tmp=0b_{k-1}\cdots b_0\), and that the reflection is symmetric, it can be concluded the binary form for \(1g_{k-1}\cdots g_0\) is \(2^{k+1}-1-tmp\). But what is this value? The subtration is actually just flipping every bit of the binary number, which results in \(1\overline{b_{k-1}}\overline{b_{k-2}}\cdots\overline{b_0}\). Alright, now we have got the binary value of any Gray code starting with \(1\). Do the right shift and xor, and you will see the conclusion is correct.