Editing Sprague–Grundy theorem (section)

==Proof of the Sprague–Grundy theorem==
We prove that all positions are equivalent to a nimber by [[structural induction]].  The more specific result, that the given game's initial position must be equivalent to a nimber, shows that the game is itself equivalent to a nimber.

Consider a position <math>G = \{G_1, G_2, \ldots, G_k\}</math>. By the [[Mathematical induction | induction hypothesis]], all of the options are equivalent to nimbers, say <math>G_i \approx *n_i</math>. So let <math>G'=\{*n_1, *n_2, \ldots, *n_k\}</math>.  We will show that <math>G \approx *m</math>, where <math>m</math> is the [[mex (mathematics)|mex (minimum exclusion)]] of the numbers <math>n_1, n_2, \ldots, n_k</math>, that is, the smallest non-negative integer not equal to some <math>n_i</math>.

The first thing we need to note is that <math>G \approx G'</math>, by way of the second lemma. If <math>k</math> is zero, the claim is trivially true.  Otherwise, consider <math>G+G'</math>. If the next player makes a move to <math>G_i</math> in <math>G</math>, then the previous player can move to <math>*n_i</math> in <math>G'</math>, and conversely if the next player makes a move in <math>G'</math>. After this, the position is a <math>\mathcal{P}</math>-position by the lemma's forward implication. Therefore, <math>G+G'</math> is a <math>\mathcal{P}</math>-position, and, citing the lemma's reverse implication, <math>G \approx G'</math>.

Now let us show that <math>G'+*m</math> is a <math>\mathcal{P}</math>-position, which, using the second lemma once again, means that <math>G'\approx *m</math>. We do so by giving an explicit strategy for the previous player.

Suppose that <math>G'</math> and <math>*m</math> are empty.  Then <math>G'+*m</math> is the null set, clearly a <math>\mathcal{P}</math>-position.

Or consider the case that the next player moves in the component <math>*m</math> to the option <math>*m'</math> where <math>m'<m</math>. Because <math>m</math> was the ''minimum'' excluded number, the previous player can move in <math>G'</math> to <math>*m'</math>.  And, as shown before, any position plus itself is a <math>\mathcal{P}</math>-position.

Finally, suppose instead that the next player moves in the component <math>G'</math> to the option <math>*n_i</math>. If <math>n_i < m</math> then the previous player moves in <math>*m</math> to <math>*n_i</math>; otherwise, if <math>n_i > m</math>, the previous player moves in <math>*n_i</math> to <math>*m</math>; in either case the result is a position plus itself. (It is not possible that <math>n_i = m</math> because <math>m</math> was defined to be different from all the <math>n_i</math>.)

In summary, we have <math>G\approx G'</math> and <math>G'\approx *m</math>.  By transitivity, we conclude that <math>G \approx *m</math>, as desired.