Grundy数がXORになることの証明

スナネコです。
Grundy数がxorで計算できることの説明をしてほしいとサーバルさんに頼まれたのでします。

ざっと検索してみましたが、「Grundy数が0でないとき0にできる」くらいしか証明が書いてあるものは見つけられないですね。これではXORになることの説明には不十分です。
（追記）この記事にかかれていました　Grundy数（Nim数, Nimber）の理論（追記終わり）

私が以前 Nimber の解説を書いたときも、方針だけ書いて細かい証明は書いていませんでした。
せっかくなのでちゃんと証明しましょう。
ここから先では XOR を $\oplus$ で表すことにします。

"山"の個数に関する帰納法から、"山"が2個のときを示せば十分です。
grundy数が a と b の2つの"山"を合わせた局面のgrundy数を $g(a,b)$ と表すことにします。
定義から分かっていることは $g(a,b) = {\mathrm mex}(\{g(a,b') \mid b'< b\}\cup \{g(a',b) \mid a'< a \})$ で、示したいことは $g(a,b)=a\oplus b$ です。
$a,b$ に関する帰納法で示します。 $a+b$ の小さい順だと思ってもいいですし、 $(a,b)$ の辞書順だと思ってもいいです。
定義から $g(0,0)={\mathrm mex}(\emptyset)=0$ であり、 $(a,b)=(0,0)$ のとき成り立っています。
$(a,b)\neq(0,0)$ のとき帰納法の仮定から
$g(a,b) = {\mathrm mex}(\{a\oplus b' \mid b'< b\}\cup \{a'\oplus b \mid a'< a \})$ です。なので示すべきことは
・ $a\oplus b$ は $\{a\oplus b' \mid b'< b\}\cup \{a'\oplus b \mid a'< a \}$ に含まれない
・0 以上 $a\oplus b$ 未満の任意の数は $\{a\oplus b' \mid b'< b\}\cup \{a'\oplus b \mid a'< a \}$ に含まれる
の2つです。
1つ目は $x\neq b \Rightarrow a\oplus x \neq a \oplus b$ と $x\neq a \Rightarrow x\oplus b \neq a \oplus b$ が成り立つので言えます。
2つ目を示すのはちょっと大変です。
示したいことは「 $n < a \oplus b$ ならば『 $b \oplus n < a$ または $a \oplus n < b$ 』」です。
$b \oplus n < a$ なら、 $a'=b \oplus n$ とすれば $a'\oplus b=n$ にできて、 $a \oplus n < b$ なら、 $b'=a \oplus n$ とすれば $a\oplus b'=n$ にできますからね。
証明には、「 $x < y$ ⇔ $x\oplus y$ の最上位bitの位置では、 $x$ のbitが0で、 $y$ のbitが1」という事実を使います。
$n < a \oplus b$ ⇔ $a\oplus b\oplus n$ の最上位bitの位置では、 $n$ のbitは0で、 $a \oplus b$ のbitは1。つまり(n,a,b)は(0,0,1)か(0,1,0)。
$b\oplus n < a$ ⇔ $a\oplus b\oplus n$ の最上位bitの位置では、 $b\oplus n$ のbitは0で、 $a$ のbitは1。つまり(n,a,b)は(0,1,0)か(1,1,1)。
$a\oplus n < b$ ⇔ $a\oplus b\oplus n$ の最上位bitの位置では、 $a\oplus n$ のbitは0で、 $b$ のbitは1。つまり(n,a,b)は(0,0,1)か(1,1,1)。
となることから、たしかに「 $n < a \oplus b$ ならば『 $b \oplus n < a$ または $a \oplus n < b$ 』」が成り立っていることがわかりました。

これで $g(a,b)=a\oplus b$ が証明できました。