Nim

TheoremBouton's move properties in Nim#✓fully proved

Let a Nim position be a finite list of heap sizes \(a_1, \dots, a_n \in \mathbb{N}\), with nim-sum \(a_1 \oplus \cdots \oplus a_n\), where \(\oplus\) is bitwise exclusive or and the empty list has nim-sum \(0\). A move chooses an index \(i\) and replaces \(a_i\) by a natural number \(y < a_i\). Then: (i) if the position has nim-sum \(0\), every move leads to a position with nonzero nim-sum; (ii) if the position has nonzero nim-sum, some move leads to a position with nim-sum \(0\).

Positions with no move (the empty list and the all-zero lists) have nim-sum \(0\), so the two properties determine the normal-play labelling by induction on the game: the positions with nim-sum \(0\) are exactly the P-positions (previous player wins) and the others are the N-positions.

theorem bouton_nim_p_positions
    (pos : List ℕ) :
    (List.foldl Nat.xor 0 pos = 0 →
      ∀ (i : Fin pos.length) (y : ℕ), y < pos.get i →
        List.foldl Nat.xor 0 (pos.set i.val y) ≠ 0) ∧
    (List.foldl Nat.xor 0 pos ≠ 0 →
      ∃ (i : Fin pos.length) (y : ℕ), y < pos.get i ∧
        List.foldl Nat.xor 0 (pos.set i.val y) = 0)

Sources

• Tanya Khovanova and Joshua Xiong, "Nim Fractals", Journal of Integer Sequences 17 (2014), theorem lines 155–159, https://cs.uwaterloo.ca/journals/JIS/VOL17/Khovanova/khova6.tex.

TheoremNim-sum zero via the last pile#✓fully proved

For natural numbers \(a_1, \dots, a_n\) (the preceding piles) and \(b\) (the last pile), the nim-sum \(a_1 \oplus \cdots \oplus a_n \oplus b\) is \(0\) if and only if \(b = a_1 \oplus \cdots \oplus a_n\), where \(\oplus\) is bitwise exclusive or and the nim-sum of no piles is \(0\).

This is only the nim-sum identity behind the source's corollary. The corollary itself characterizes P-positions; its game-theoretic content, that the nim-sum-zero positions are exactly the P-positions, is Bouton's theorem.

theorem nim_sum_eq_zero_iff_last_eq_xor_fold
    (preceding : List Nat) (last : Nat) :
    List.foldl Nat.xor 0 (preceding ++ [last]) = 0 ↔ last = List.foldl Nat.xor 0 preceding

Sources

• Tanya Khovanova and Joshua Xiong, "Nim Fractals," Journal of Integer Sequences 17 (2014), Article 14.7.8, Corollary, lines 163–165, https://cs.uwaterloo.ca/journals/JIS/VOL17/Khovanova/khova6.tex

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.