Skip to content

Princess and the Roses game

TheoremEquivalence of impartial games via their sum#●ready to prove

Two finite impartial games \(G\) and \(H\) are equivalent if and only if their sum \(G + H\) is a P-position, that is, the position of \(G + H\) in which both \(G\) and \(H\) are at their starting positions is a P-position.

public theorem_wanted impartialGame_equiv_iff_isP_gameSum (G H : ImpartialGame) :
    Equiv G H ↔ IsP (gameSum G H) ((G.start, H.start) : (gameSum G H).Pos)
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Lemma 5.
Uses 4
Statement usesEquivalence of impartial games · Impartial game · P-positions · Sum of impartial games

TheoremP-positions are the games of Sprague–Grundy value zero#●ready to prove

Let \(G\) be a finite impartial game and \(n\) a natural number such that \(G\) is equivalent to the Nim heap \(*n\), that is, \(G\) has Sprague–Grundy value \(n\). Then the starting position of \(G\) is a P-position if and only if \(n = 0\).

public theorem_wanted isP_start_iff_of_equiv_nimHeap (G : ImpartialGame) (n : ℕ)
    (hG : Equiv G (nimHeap n)) :
    IsP G G.start ↔ n = 0
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Theorem 6.
Uses 4
Statement usesEquivalence of impartial games · Impartial game · P-positions · Nim heap

TheoremMex rule for Sprague–Grundy values#●ready to prove

Let \(G\) be a finite impartial game and \(n\) a natural number such that \(G\) is equivalent to the Nim heap \(*n\), that is, \(G\) has Sprague–Grundy value \(n\). For a move from the start position of \(G\) to a position \(q\), write \(G_q\) for the game \(G\) started at \(q\). Then no \(G_q\) is equivalent to \(*n\), and for every natural number \(m < n\) some \(G_q\) is equivalent to \(*m\). That is, the Sprague–Grundy value of \(G\) is the mex of the Sprague–Grundy values of the games \(G_q\).

public theorem_wanted spragueGrundyValue_eq_mex_options (G : ImpartialGame) (n : ℕ)
    (hG : Equiv G (nimHeap n)) :
    (∀ q ∈ G.moves G.start, ¬ Equiv { G with start := q } (nimHeap n)) ∧
      ∀ m < n, ∃ q ∈ G.moves G.start, Equiv { G with start := q } (nimHeap m)
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Corollary 4.
Uses 3
Statement usesEquivalence of impartial games · Impartial game · Nim heap
15 fully proved19 ready to prove

The Princess and the Roses game

DefinitionThe Princess and the Roses game#✓fully proved

For \(k \in \mathbb{N}\) and \(p \in \mathbb{N}^k\), the Princess and the Roses game (P&R) with \(k\) labelled piles started at \(p\) is the impartial game whose positions are the \(q \in \mathbb{N}^k\), with \(q_i\) objects on pile \(i\), and whose moves remove one object from one nonempty pile, or one object from each of two distinct nonempty piles. It is Slow\(A\)-Nim \(\mathrm{SN}(k, \{1, 2\})\) started at \(p\), and its rank is the total number of objects \(\sum_i q_i\).

Pile order is not normalized; the paper's convention of listing piles in non-increasing order does not change the game.

public def princessRoses {k : ℕ} (p : Fin k → ℕ) : ImpartialGame :=
  { slowANimGame k {1, 2} with start := p }
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Section 2.1.
Uses 2 · Used by 7
Statement usesImpartial game · Slow\(A\)-Nim
Used byFour-pile P&R reduces to P&R Helper · Four-pile P&R is equivalent to simplified P&R · Lim's theorem on five-pile P&R · Adding to the three largest piles of four-pile P&R · Sprague–Grundy values of three-pile Princess and the Roses · Sprague–Grundy values of two-pile Princess and the Roses · In two-pile Princess and the Roses, \((1, 1)\) moves to \((0, 0)\)

TheoremOptions in Princess and the Roses#✓fully proved

Let \(p\) and \(q\) be positions of Slow\(A\)-Nim on \(k\) stacks with \(A = \{1, 2\}\), which is the Princess and the Roses game. Then \(q\) is an option of \(p\) if and only if there are stacks \(i \le j\) with \(p_i \ge 1\) and \(p_j \ge 1\) such that \(q_l = p_l - 1\) for \(l \in \{i, j\}\) and \(q_l = p_l\) for every other stack \(l\); that is, \(q\) removes one token from stack \(i\) when \(i = j\), and one token from each of stacks \(i\) and \(j\) otherwise.

public theorem mem_slowANimMoves_one_two {k : ℕ} {p q : Fin k → ℕ} :
    q ∈ slowANimMoves {1, 2} p ↔
      ∃ i j : Fin k, i ≤ j ∧ 0 < p i ∧ 0 < p j ∧
        q = fun l => if l = i ∨ l = j then p l - 1 else p l
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Section 2.1.
Uses 2 · Used by 1
Statement usesOptions in Slow A-Nim
Proof usesPlaying on a set of stacks
Used byIn two-pile Princess and the Roses, \((1, 1)\) moves to \((0, 0)\)

TheoremIn two-pile Princess and the Roses, \((1, 1)\) moves to \((0, 0)\)#✓fully proved

In the Princess and the Roses game on two piles, \((0, 0)\) is an option of the position \((1, 1)\): one may take one object from each pile.

public theorem zero_zero_mem_princessRoses_moves_one_one :
    ![0, 0] ∈ (princessRoses ![1, 1]).moves ![1, 1]
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Section 2.1.
Uses 4
Statement usesImpartial game · The Princess and the Roses game
Proof usesOptions in Princess and the Roses · Options in Slow A-Nim

TheoremLim's theorem on five-pile P&R#●ready to prove

Let \(a \ge b \ge c \ge d \ge e\) be natural numbers. The Princess and the Roses position \((a, b, c, d, e)\) is a P-position if and only if the parities of \(a, b, c, d, e\) are, in this order, (even, even, even, even, even), (odd, odd, odd, even, even), (even, odd, odd, odd, odd) or (odd, even, even, odd, odd).

Positions with fewer piles are the cases with trailing zero piles.

public theorem_wanted princessRoses_five_piles_isP_iff (a b c d e : ℕ) (hab : b ≤ a)
    (hbc : c ≤ b) (hcd : d ≤ c) (hde : e ≤ d) :
    IsP (princessRoses ![a, b, c, d, e]) (princessRoses ![a, b, c, d, e]).start ↔
      (Even a ∧ Even b ∧ Even c ∧ Even d ∧ Even e) ∨
        (Odd a ∧ Odd b ∧ Odd c ∧ Even d ∧ Even e) ∨
        (Even a ∧ Odd b ∧ Odd c ∧ Odd d ∧ Odd e) ∨
        (Odd a ∧ Even b ∧ Even c ∧ Odd d ∧ Odd e)
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Theorem 7.
Uses 3
Statement usesImpartial game · P-positions · The Princess and the Roses game

TheoremSprague–Grundy values of two-pile Princess and the Roses#●ready to prove

For natural numbers \(a \ge b\), the Princess and the Roses position \((a, b)\) is equivalent to the Nim heap \(*n\), that is, it has Sprague–Grundy value \(n\), where \(n = 0\) if \(a\) and \(b\) are both even, \(n = 1\) if \(a\) is odd and \(b\) is even, \(n = 2\) if \(a\) and \(b\) are both odd, and \(n = 3\) if \(a\) is even and \(b\) is odd.

public theorem_wanted princessRoses_two_piles_equiv_nimHeap (a b : ℕ) (hab : b ≤ a) :
    Equiv (princessRoses ![a, b])
      (nimHeap (if Even a then (if Even b then 0 else 3) else (if Even b then 1 else 2)))
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Theorem 8.
Uses 3
Statement usesEquivalence of impartial games · Nim heap · The Princess and the Roses game

TheoremSprague–Grundy values of three-pile Princess and the Roses#●ready to prove

For natural numbers \(a \ge b \ge c\), the Princess and the Roses position \((a, b, c)\) is equivalent to the Nim heap \(*n\), that is, it has Sprague–Grundy value \(n\), where \(n = 0\) if \(a\) and \(b\) both have the parity of \(c\), \(n = 1\) if \(a\) differs from \(c\) in parity and \(b\) does not, \(n = 2\) if \(a\) and \(b\) both differ from \(c\) in parity, and \(n = 3\) if \(b\) differs from \(c\) in parity and \(a\) does not.

Writing \(E\) for even and \(O\) for odd, the value is \(0\) on \((E, E, E)\) and \((O, O, O)\), \(1\) on \((O, E, E)\) and \((E, O, O)\), \(2\) on \((O, O, E)\) and \((E, E, O)\), and \(3\) on \((E, O, E)\) and \((O, E, O)\).

public theorem_wanted princessRoses_three_piles_equiv_nimHeap (a b c : ℕ) (hab : b ≤ a)
    (hbc : c ≤ b) :
    Equiv (princessRoses ![a, b, c])
      (nimHeap (if a % 2 = c % 2 then (if b % 2 = c % 2 then 0 else 3)
        else (if b % 2 = c % 2 then 1 else 2)))
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Corollary 10.
Uses 3
Statement usesEquivalence of impartial games · Nim heap · The Princess and the Roses game

TheoremAdding to the three largest piles of four-pile P&R#●ready to prove

For natural numbers \(a \ge b \ge c \ge d\) and every natural number \(n\), the Princess and the Roses positions \((a, b, c, d)\) and \((a + n, b + n, c + n, d)\) are equivalent; that is, they have the same Sprague–Grundy value.

public theorem_wanted princessRoses_four_piles_equiv_add_three_largest (a b c d n : ℕ)
    (hab : b ≤ a) (hbc : c ≤ b) (hcd : d ≤ c) :
    Equiv (princessRoses ![a, b, c, d]) (princessRoses ![a + n, b + n, c + n, d])
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Lemma 9.
Uses 2
Statement usesEquivalence of impartial games · The Princess and the Roses game

Simplified P&R

DefinitionMoves of simplified P&R#✓fully proved

The simplified Princess and the Roses game on four sorted piles \((a, b, c, d)\) has seven moves, given as the amounts removed from \((a, b, c, d)\): \((1, 0, 0, 0)\), \((0, 1, 0, 0)\), \((0, 0, 0, 1)\), \((1, 1, 0, 0)\), \((1, 0, 0, 1)\), \((0, 1, 0, 1)\) and \((0, 0, 1, 1)\).

These are the moves of four-pile Princess and the Roses except taking one object from the third pile alone or together with the first or second pile, so the third pile may be taken from only together with the fourth.

public def simplifiedPrincessRosesMoveList : List (ℕ × ℕ × ℕ × ℕ) :=
  [(1, 0, 0, 0), (0, 1, 0, 0), (0, 0, 0, 1), (1, 1, 0, 0), (1, 0, 0, 1), (0, 1, 0, 1),
    (0, 0, 1, 1)]
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Section 3.1.
Used by 3
Used byCharacterization of simplified P&R options · Options in simplified Princess and the Roses · Simplified P&R moves decrease the number of objects

DefinitionOptions in simplified Princess and the Roses#✓fully proved

The seven simplified Princess and the Roses moves are the removal vectors \((1, 0, 0, 0)\), \((0, 1, 0, 0)\), \((0, 0, 0, 1)\), \((1, 1, 0, 0)\), \((1, 0, 0, 1)\), \((0, 1, 0, 1)\) and \((0, 0, 1, 1)\). For a quadruple \((a, b, c, d)\) of natural numbers, its options are the quadruples \((a - r_1, b - r_2, c - r_3, d - r_4)\) for those moves \((r_1, r_2, r_3, r_4)\) with \(r_1 \le a\), \(r_2 \le b\), \(r_3 \le c\) and \(r_4 \le d\) whose result is in non-increasing order: \(a - r_1 \ge b - r_2 \ge c - r_3 \ge d - r_4\).

public def simplifiedPrincessRosesMoves (p : ℕ × ℕ × ℕ × ℕ) : Finset (ℕ × ℕ × ℕ × ℕ) :=
  (simplifiedPrincessRosesMoveList.toFinset.filter fun m =>
      m.1 ≤ p.1 ∧ m.2.1 ≤ p.2.1 ∧ m.2.2.1 ≤ p.2.2.1 ∧ m.2.2.2 ≤ p.2.2.2 ∧
        p.2.1 - m.2.1 ≤ p.1 - m.1 ∧ p.2.2.1 - m.2.2.1 ≤ p.2.1 - m.2.1 ∧
        p.2.2.2 - m.2.2.2 ≤ p.2.2.1 - m.2.2.1).image
    fun m => (p.1 - m.1, p.2.1 - m.2.1, p.2.2.1 - m.2.2.1, p.2.2.2 - m.2.2.2)
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Sections 2.2 and 3.1.
Uses 1 · Used by 4
Statement usesMoves of simplified P&R
Used byCharacterization of simplified P&R options · Simplified Princess and the Roses · Simplified P&R moves decrease the number of objects · A terminal position of simplified P&R

TheoremCharacterization of simplified P&R options#✓fully proved

For natural numbers \(a, b, c, d\) and \(a', b', c', d'\), the position \([a', b', c', d']\) is an option of the simplified P&R position \([a, b, c, d]\) if and only if \(a' \le a\), \(b' \le b\), \(c' \le c\), \(d' \le d\), \(a' \ge b' \ge c' \ge d'\), and the amounts removed \((a - a', b - b', c - c', d - d')\) form one of the seven simplified P&R moves \((1, 0, 0, 0)\), \((0, 1, 0, 0)\), \((0, 0, 0, 1)\), \((1, 1, 0, 0)\), \((1, 0, 0, 1)\), \((0, 1, 0, 1)\) and \((0, 0, 1, 1)\).

public theorem mem_simplifiedPrincessRosesMoves {a b c d a' b' c' d' : ℕ} :
    (a', b', c', d') ∈ simplifiedPrincessRosesMoves (a, b, c, d) ↔
      a' ≤ a ∧ b' ≤ b ∧ c' ≤ c ∧ d' ≤ d ∧ b' ≤ a' ∧ c' ≤ b' ∧ d' ≤ c' ∧
        (a - a', b - b', c - c', d - d') ∈ simplifiedPrincessRosesMoveList
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Sections 2.2 and 3.1.
Uses 2 · Used by 1
Statement usesMoves of simplified P&R · Options in simplified Princess and the Roses
Used bySimplified P&R moves decrease the number of objects

TheoremSimplified P&R moves decrease the number of objects#✓fully proved

For all quadruples \((a, b, c, d)\) and \((a', b', c', d')\) of natural numbers, if \((a', b', c', d')\) is an option of \((a, b, c, d)\) in simplified Princess and the Roses, then \(a' + b' + c' + d' < a + b + c + d\).

public theorem simplifiedPrincessRosesMoves_rank_lt {p q : ℕ × ℕ × ℕ × ℕ}
    (h : q ∈ simplifiedPrincessRosesMoves p) :
    q.1 + q.2.1 + q.2.2.1 + q.2.2.2 < p.1 + p.2.1 + p.2.2.1 + p.2.2.2
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Section 3.1.
Uses 3 · Used by 1
Statement usesOptions in simplified Princess and the Roses
Proof usesCharacterization of simplified P&R options · Moves of simplified P&R
Used bySimplified Princess and the Roses

TheoremA terminal position of simplified P&R#✓fully proved

In simplified Princess and the Roses, the position \((3, 3, 3, 0)\) has no options.

public theorem simplifiedPrincessRosesMoves_three_three_three_zero :
    simplifiedPrincessRosesMoves (3, 3, 3, 0) = ∅
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Section 3.1.
Uses 1
Statement usesOptions in simplified Princess and the Roses

DefinitionSimplified Princess and the Roses#✓fully proved

For a quadruple \(p\) of natural numbers, simplified Princess and the Roses started at \(p\) is the impartial game whose positions are all quadruples \((a, b, c, d)\) of natural numbers, whose options from a position are its simplified Princess and the Roses options (the results of the seven simplified moves that take no pile below zero and leave the piles in non-increasing order), whose rank is the total number of objects \(a + b + c + d\), and whose start position is \(p\).

public def simplifiedPrincessRoses (p : ℕ × ℕ × ℕ × ℕ) : ImpartialGame where
  Pos := ℕ × ℕ × ℕ × ℕ
  eqDec := inferInstance
  moves := simplifiedPrincessRosesMoves
  rank := fun q => q.1 + q.2.1 + q.2.2.1 + q.2.2.2
  rank_lt := fun _ _ h => simplifiedPrincessRosesMoves_rank_lt h
  start := p
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Section 3.1.
Uses 3 · Used by 1
Statement usesImpartial game · Options in simplified Princess and the Roses · Simplified P&R moves decrease the number of objects
Used byFour-pile P&R is equivalent to simplified P&R

TheoremFour-pile P&R is equivalent to simplified P&R#●ready to prove

For natural numbers \(a \ge b \ge c \ge d\) and every natural number \(n\), the Princess and the Roses position \((a, b, c, d)\) is equivalent to the simplified P&R position \([a + n, b + n, c + n, d]\); that is, the two have the same Sprague–Grundy value.

public theorem_wanted princessRoses_equiv_simplifiedPrincessRoses (a b c d n : ℕ)
    (hab : b ≤ a) (hbc : c ≤ b) (hcd : d ≤ c) :
    Equiv (princessRoses ![a, b, c, d]) (simplifiedPrincessRoses (a + n, b + n, c + n, d))
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Lemma 11.
Uses 3
Statement usesEquivalence of impartial games · The Princess and the Roses game · Simplified Princess and the Roses

The P&R Helper game

DefinitionMoves of P&R Helper#✓fully proved

The list of the seven moves of P&R Helper on a position \([x, y, z]\), each given as the triple of amounts removed from \((x, y, z)\): in order, \((1, 1, 1)\), \((1, 0, 0)\), \((1, 2, 1)\), \((1, 1, 2)\), \((0, 1, 0)\), \((0, 1, 1)\) and \((0, 0, 1)\). As changes to the position these are \((-1, -1, -1)\), \((-1, 0, 0)\), \((-1, -2, -1)\), \((-1, -1, -2)\), \((0, -1, 0)\), \((0, -1, -1)\) and \((0, 0, -1)\).

public def princessRosesHelperMoveList : List (ℕ × ℕ × ℕ) :=
  [(1, 1, 1), (1, 0, 0), (1, 2, 1), (1, 1, 2), (0, 1, 0), (0, 1, 1), (0, 0, 1)]
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Section 3.1.
Used by 3
Used byCharacterization of P&R Helper options · Options in P&R Helper · P&R Helper moves decrease the coordinate sum

DefinitionOptions in P&R Helper#✓fully proved

The P&R Helper game is played on triples of natural numbers with the seven moves that subtract \((1, 1, 1)\), \((1, 0, 0)\), \((1, 2, 1)\), \((1, 1, 2)\), \((0, 1, 0)\), \((0, 1, 1)\) or \((0, 0, 1)\). The options of a position \((x, y, z)\) are the triples \((x - u, y - v, z - w)\) for those moves \((u, v, w)\) with \(u \le x\), \(v \le y\), \(w \le z\) and \(x - u \le y - v \le z - w\).

public def princessRosesHelperMoves (p : ℕ × ℕ × ℕ) : Finset (ℕ × ℕ × ℕ) :=
  (princessRosesHelperMoveList.toFinset.filter fun m =>
      m.1 ≤ p.1 ∧ m.2.1 ≤ p.2.1 ∧ m.2.2 ≤ p.2.2 ∧ p.1 - m.1 ≤ p.2.1 - m.2.1 ∧
        p.2.1 - m.2.1 ≤ p.2.2 - m.2.2).image
    fun m => (p.1 - m.1, p.2.1 - m.2.1, p.2.2 - m.2.2)
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Section 3.1.
Uses 1 · Used by 4
Statement usesMoves of P&R Helper
Used byCharacterization of P&R Helper options · The P&R Helper game · P&R Helper moves decrease the coordinate sum · Small P&R Helper positions

TheoremCharacterization of P&R Helper options#✓fully proved

For natural numbers \(x, y, z, x', y', z'\), the position \([x', y', z']\) is an option of the P&R Helper position \([x, y, z]\) if and only if \(x' \le x\), \(y' \le y\), \(z' \le z\), \(x' \le y' \le z'\), and the amounts removed \((x - x', y - y', z - z')\) form one of the seven P&R Helper moves \((1, 1, 1)\), \((1, 0, 0)\), \((1, 2, 1)\), \((1, 1, 2)\), \((0, 1, 0)\), \((0, 1, 1)\) and \((0, 0, 1)\).

public theorem mem_princessRosesHelperMoves {x y z x' y' z' : ℕ} :
    (x', y', z') ∈ princessRosesHelperMoves (x, y, z) ↔
      x' ≤ x ∧ y' ≤ y ∧ z' ≤ z ∧ x' ≤ y' ∧ y' ≤ z' ∧
        (x - x', y - y', z - z') ∈ princessRosesHelperMoveList
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Section 3.1.
Uses 2 · Used by 1
Statement usesMoves of P&R Helper · Options in P&R Helper
Used byP&R Helper moves decrease the coordinate sum

TheoremP&R Helper moves decrease the coordinate sum#✓fully proved

For all triples \((x, y, z)\) and \((x', y', z')\) of natural numbers, if \((x', y', z')\) is an option of \((x, y, z)\) in the P&R Helper game, then \(x' + y' + z' < x + y + z\).

public theorem princessRosesHelperMoves_rank_lt {p q : ℕ × ℕ × ℕ}
    (h : q ∈ princessRosesHelperMoves p) : q.1 + q.2.1 + q.2.2 < p.1 + p.2.1 + p.2.2
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Section 3.1.
Uses 3 · Used by 1
Statement usesOptions in P&R Helper
Proof usesCharacterization of P&R Helper options · Moves of P&R Helper
Used byThe P&R Helper game

TheoremSmall P&R Helper positions#✓fully proved

In the P&R Helper game, the position \((0, 0, 0)\) has no options, and the options of \((1, 1, 1)\) are exactly \((0, 0, 0)\) and \((0, 1, 1)\).

public theorem princessRosesHelperMoves_small :
    princessRosesHelperMoves (0, 0, 0) = ∅ ∧
      princessRosesHelperMoves (1, 1, 1) = {(0, 0, 0), (0, 1, 1)}
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Section 3.1.
Uses 1
Statement usesOptions in P&R Helper

DefinitionThe P&R Helper game#✓fully proved

For a triple \(p\) of natural numbers, P&R Helper started at \(p\) is the impartial game whose positions are the triples \((x, y, z)\) of natural numbers, whose options from \((x, y, z)\) are the triples \((x - u, y - v, z - w)\) for \((u, v, w)\) among \((1, 1, 1)\), \((1, 0, 0)\), \((1, 2, 1)\), \((1, 1, 2)\), \((0, 1, 0)\), \((0, 1, 1)\) and \((0, 0, 1)\) with \(u \le x\), \(v \le y\), \(w \le z\) and \(x - u \le y - v \le z - w\), whose rank is \(x + y + z\), and which starts at \(p\).

public def princessRosesHelper (p : ℕ × ℕ × ℕ) : ImpartialGame where
  Pos := ℕ × ℕ × ℕ
  eqDec := inferInstance
  moves := princessRosesHelperMoves
  rank := fun q => q.1 + q.2.1 + q.2.2
  rank_lt := fun _ _ h => princessRosesHelperMoves_rank_lt h
  start := p
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Section 3.1.
Uses 3 · Used by 11
Statement usesImpartial game · Options in P&R Helper · P&R Helper moves decrease the coordinate sum
Used byFour-pile P&R reduces to P&R Helper · Sprague–Grundy value \(5\) of P&R Helper on region \(U\) · P&R Helper positions of Sprague–Grundy value 4 on region U · Sprague–Grundy values of P&R Helper on region R · Sprague–Grundy values of P&R Helper on region L · Sprague–Grundy values of P&R Helper on region D · P&R Helper positions of Sprague–Grundy value 1 on regions U and R · P&R Helper positions of Sprague–Grundy value 6 or 7 on region U · P&R Helper positions of Sprague–Grundy value 3 on region U · P&R Helper positions of Sprague–Grundy value 2 on region U · P&R Helper positions of Sprague–Grundy value 0

TheoremFour-pile P&R reduces to P&R Helper#●ready to prove

For natural numbers \(a \ge b \ge c \ge d\), the Princess and the Roses position \((a, b, c, d)\) is equivalent to the P&R Helper position \([d, b - c + d, a - c + d]\); that is, the two have the same Sprague–Grundy value.

public theorem_wanted princessRoses_equiv_princessRosesHelper (a b c d : ℕ) (hab : b ≤ a)
    (hbc : c ≤ b) (hcd : d ≤ c) :
    Equiv (princessRoses ![a, b, c, d]) (princessRosesHelper (d, b - c + d, a - c + d))
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Theorem 12.
Uses 3
Statement usesEquivalence of impartial games · The Princess and the Roses game · The P&R Helper game

Theorem 13: Sprague–Grundy values of P&R Helper

TheoremP&R Helper positions of Sprague–Grundy value 0#●ready to prove

For natural numbers \(x \le y \le z\), the P&R Helper game started at \([x, y, z]\) is equivalent to the Nim heap of size \(0\) (that is, has Sprague–Grundy value \(0\)) if and only if \(x\), \(y\) and \(z\) are all even.

public theorem_wanted princessRosesHelper_equiv_nimHeap_zero_iff (x y z : ℕ) (hxy : x ≤ y)
    (hyz : y ≤ z) :
    Equiv (princessRosesHelper (x, y, z)) (nimHeap 0) ↔ Even x ∧ Even y ∧ Even z
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Theorem 13, first bullet.
Uses 3
Statement usesEquivalence of impartial games · Nim heap · The P&R Helper game

TheoremP&R Helper positions of Sprague–Grundy value 1 on regions U and R#●ready to prove

For natural numbers \(x \le y \le z\) with \(z < x + y\) (the union of the regions \(U\) and \(R\)), the P&R Helper game started at \([x, y, z]\) is equivalent to the Nim heap of size \(1\) (that is, has Sprague–Grundy value \(1\)) if and only if one of the following holds: \((x, y, z) = (1, 1, 1)\); or \(y = x\), \(z = x\) and \(x \equiv 3 \pmod 4\); or \(y = x\), \(z = x + 1\), \(x \equiv 1 \pmod 4\) and \(x \ne 1\); or \(y = x + 1\), \(z = x + 1\), \(x \equiv 0 \pmod 4\) and \(x \ne 0\); or \(y + z - x \equiv 1 \pmod 4\) and \(z > x + 1\).

public theorem_wanted princessRosesHelper_equiv_nimHeap_one_iff_of_lt_add (x y z : ℕ)
    (hxy : x ≤ y) (hyz : y ≤ z) (hUR : z < x + y) :
    Equiv (princessRosesHelper (x, y, z)) (nimHeap 1) ↔
      (x, y, z) = (1, 1, 1) ∨
        (y = x ∧ z = x ∧ x % 4 = 3) ∨
        (y = x ∧ z = x + 1 ∧ x % 4 = 1 ∧ x ≠ 1) ∨
        (y = x + 1 ∧ z = x + 1 ∧ x % 4 = 0 ∧ x ≠ 0) ∨
        ((y + z - x) % 4 = 1 ∧ x + 1 < z)
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Theorem 13, value 1 on U ∪ R.
Uses 3
Statement usesEquivalence of impartial games · Nim heap · The P&R Helper game

TheoremP&R Helper positions of Sprague–Grundy value 2 on region U#●ready to prove

For natural numbers \(x \le y \le z\) with \(z < x + y\) and \(y \le 2x + 1\) (the region \(U\)), write \(s = y + z - x\). The P&R Helper game started at \([x, y, z]\) is equivalent to the Nim heap of size \(2\) (that is, has Sprague–Grundy value \(2\)) if and only if one of the following holds: (a) \(y = x\), \(z = x\), \(x \equiv 1 \pmod 4\) and \(x \ne 1\); (b) \(y = x\), \(z = x + 1\) and \(x \equiv 3 \pmod 4\); (c) \(y = x + 1\), \(z = x + 1\), \(x \equiv 2 \pmod 4\) and \(x \ne 2\); (d) \(y = x\), \(z = x + 2\), \(x \equiv 1 \pmod 4\) and \(x \ne 1\); (e) \(y = x + 1\), \(z = x + 2\), \(x \equiv 0 \pmod 4\) and \(x \ne 0\); (f) \(y = x + 2\), \(z = x + 2\) and \(x \equiv 3 \pmod 4\); (g) \(s \equiv 7 \pmod 8\), and either \(z > x + 4\) and \(y = x\), or \(z > x + 5\) and \(y = x + 1\), or \(z > x + 2\) and \(z = x + y - 1\); (h) \(s \equiv 4 \pmod 8\), \(y = x\), \(x\) is odd and \(z > x + 4\); (i) \(s \equiv 2 \pmod 4\), \(x\), \(y\), \(z\) are not all even, \(z > x + 2\), it is not the case that \(s \equiv 6 \pmod 8\), \(z > x + 4\) and \(y \le x + 1\), and it is not the case that \(s \equiv 6 \pmod 8\) and \(z = x + y - 2\).

MetaMathlibExt.princessRosesHelper_equiv_nimHeap_two_iff_of_mem_U · 15 lines 
public theorem_wanted princessRosesHelper_equiv_nimHeap_two_iff_of_mem_U (x y z : ℕ)
    (hxy : x ≤ y) (hyz : y ≤ z) (hU : z < x + y ∧ y ≤ 2 * x + 1) :
    Equiv (princessRosesHelper (x, y, z)) (nimHeap 2) ↔
      (y = x ∧ z = x ∧ x % 4 = 1 ∧ x ≠ 1) ∨
        (y = x ∧ z = x + 1 ∧ x % 4 = 3) ∨
        (y = x + 1 ∧ z = x + 1 ∧ x % 4 = 2 ∧ x ≠ 2) ∨
        (y = x ∧ z = x + 2 ∧ x % 4 = 1 ∧ x ≠ 1) ∨
        (y = x + 1 ∧ z = x + 2 ∧ x % 4 = 0 ∧ x ≠ 0) ∨
        (y = x + 2 ∧ z = x + 2 ∧ x % 4 = 3) ∨
        ((y + z - x) % 8 = 7 ∧
          ((x + 4 < z ∧ y = x) ∨ (x + 5 < z ∧ y = x + 1) ∨ (x + 2 < z ∧ z = x + y - 1))) ∨
        ((y + z - x) % 8 = 4 ∧ x = y ∧ Odd x ∧ x + 4 < z) ∨
        ((y + z - x) % 4 = 2 ∧ ¬ (Even x ∧ Even y ∧ Even z) ∧ x + 2 < z ∧
          ¬ ((y + z - x) % 8 = 6 ∧ x + 4 < z ∧ y ≤ x + 1) ∧
          ¬ ((y + z - x) % 8 = 6 ∧ z = x + y - 2))
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Theorem 13, value 2 on U.
Uses 3
Statement usesEquivalence of impartial games · Nim heap · The P&R Helper game

TheoremP&R Helper positions of Sprague–Grundy value 3 on region U#●ready to prove

For natural numbers \(x \le y \le z\) with \(z < x + y\) and \(y \le 2x + 1\) (the region \(U\)), write \(s = y + z - x\). The P&R Helper game started at \([x, y, z]\) is equivalent to the Nim heap of size \(3\) (that is, has Sprague–Grundy value \(3\)) if and only if one of the following holds: (a) \((x, y, z)\) is one of \((1, 2, 2)\), \((2, 2, 3)\), \((5, 6, 6)\), \((6, 6, 7)\), \((3, 4, 5)\), \((5, 5, 8)\); (b) \(y = x\), \(z = x + 1\), \(x \equiv 0 \pmod 4\) and \(x \notin \{0, 4\}\); (c) \(y = x + 1\), \(z = x + 1\), \(x \equiv 3 \pmod 4\) and \(x \notin \{3, 7\}\); (d) \(y = x + 1\), \(z = x + 2\), \(x \equiv 1 \pmod 4\) and \(x \notin \{1, 5\}\); (e) \(s \equiv 0 \pmod 8\), \(y = x\), \(x\) is odd and \(z > x + 5\); (f) \(s \equiv 6 \pmod 8\), \(x\), \(y\), \(z\) are not all even, and either \(z > x + 4\) and \(y \le x + 1\), or \(z > x + 2\) and \(z = x + y - 2\); (g) \(s \equiv 3 \pmod 4\), \(z > x + 2\), it is not the case that \(s \equiv 7 \pmod 8\), \(z > x + 4\) and \(y \le x + 2\), and it is not the case that \(s \equiv 7 \pmod 8\), \(y \le 2x\) and \(x + y - z \le 3\).

public theorem_wanted princessRosesHelper_equiv_nimHeap_three_iff_of_mem_U (x y z : ℕ)
    (hxy : x ≤ y) (hyz : y ≤ z) (hU : z < x + y ∧ y ≤ 2 * x + 1) :
    Equiv (princessRosesHelper (x, y, z)) (nimHeap 3) ↔
      (x, y, z) ∈ [(1, 2, 2), (2, 2, 3), (5, 6, 6), (6, 6, 7), (3, 4, 5), (5, 5, 8)] ∨
        (y = x ∧ z = x + 1 ∧ x % 4 = 0 ∧ x ≠ 0 ∧ x ≠ 4) ∨
        (y = x + 1 ∧ z = x + 1 ∧ x % 4 = 3 ∧ x ≠ 3 ∧ x ≠ 7) ∨
        (y = x + 1 ∧ z = x + 2 ∧ x % 4 = 1 ∧ x ≠ 1 ∧ x ≠ 5) ∨
        ((y + z - x) % 8 = 0 ∧ x = y ∧ Odd x ∧ x + 5 < z) ∨
        ((y + z - x) % 8 = 6 ∧ ¬ (Even x ∧ Even y ∧ Even z) ∧
          ((x + 4 < z ∧ y ≤ x + 1) ∨ (x + 2 < z ∧ z = x + y - 2))) ∨
        ((y + z - x) % 4 = 3 ∧ x + 2 < z ∧
          ¬ ((y + z - x) % 8 = 7 ∧ x + 4 < z ∧ y ≤ x + 2) ∧
          ¬ ((y + z - x) % 8 = 7 ∧ y ≤ 2 * x ∧ x + y - z ≤ 3))
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Theorem 13, value 3 on U.
Uses 3
Statement usesEquivalence of impartial games · Nim heap · The P&R Helper game

TheoremP&R Helper positions of Sprague–Grundy value 4 on region U#●ready to prove

For natural numbers \(x \le y \le z\) with \(z < x + y\) and \(y \le 2x + 1\) (the region \(U\)), write \(s = y + z - x\). The P&R Helper game started at \([x, y, z]\) is equivalent to the Nim heap of size \(4\) (that is, has Sprague–Grundy value \(4\)) if and only if one of the following holds: (a) \((x, y, z)\) is one of \((2, 3, 3)\), \((5, 6, 7)\), \((4, 4, 5)\), \((7, 8, 8)\); (b) \(y = x\), \(z = x + 1\), \(x \equiv 2 \pmod 4\) and \(x \notin \{2, 6\}\); (c) \(y = x + 1\), \(z = x + 1\), \(x \equiv 1 \pmod 4\) and \(x \notin \{1, 5\}\); (d) \(y = x + 1\), \(z = x + 2\), \(x \equiv 3 \pmod 4\) and \(x \notin \{3, 7\}\); (e) \(y = x + 1\), \(z = x + 5\) and \(x \equiv 1 \pmod 8\); (f) \(s \equiv 0 \pmod 4\), \(x\), \(y\), \(z\) are not all even, \(z > x + 2\), and none of the following holds: \((x, y, z) = (5, 5, 8)\); \(z > x + 4\), \(s \equiv 4 \pmod 8\) and \(y = x\); \(z > x + 5\), \(s \equiv 0 \pmod 8\) and \(y = x\); \(y = x + 1\), \(z = x + 3\), \(x \equiv 0 \pmod 4\) and \(x \notin \{0, 4, 8\}\); \(y = x + 2\), \(z = x + 3\), \(x \equiv 3 \pmod 4\) and \(x \notin \{3, 7\}\); \(y = x + 1\), \(z = x + 5\) and \(x \equiv 2 \pmod 8\); \(y = x + 2\), \(z = x + 5\) and \(x \equiv 1 \pmod 8\); \(y = x + 1\), \(z = x + 6\) and \(x \equiv 1 \pmod 8\).

MetaMathlibExt.princessRosesHelper_equiv_nimHeap_four_iff_of_mem_U · 17 lines 
public theorem_wanted princessRosesHelper_equiv_nimHeap_four_iff_of_mem_U (x y z : ℕ)
    (hxy : x ≤ y) (hyz : y ≤ z) (hU : z < x + y ∧ y ≤ 2 * x + 1) :
    Equiv (princessRosesHelper (x, y, z)) (nimHeap 4) ↔
      (x, y, z) ∈ [(2, 3, 3), (5, 6, 7), (4, 4, 5), (7, 8, 8)] ∨
        (y = x ∧ z = x + 1 ∧ x % 4 = 2 ∧ x ≠ 2 ∧ x ≠ 6) ∨
        (y = x + 1 ∧ z = x + 1 ∧ x % 4 = 1 ∧ x ≠ 1 ∧ x ≠ 5) ∨
        (y = x + 1 ∧ z = x + 2 ∧ x % 4 = 3 ∧ x ≠ 3 ∧ x ≠ 7) ∨
        (y = x + 1 ∧ z = x + 5 ∧ x % 8 = 1) ∨
        ((y + z - x) % 4 = 0 ∧ ¬ (Even x ∧ Even y ∧ Even z) ∧ x + 2 < z ∧
          ¬ ((x, y, z) = (5, 5, 8) ∨
            (x + 4 < z ∧ (y + z - x) % 8 = 4 ∧ x = y) ∨
            (x + 5 < z ∧ (y + z - x) % 8 = 0 ∧ x = y) ∨
            (y = x + 1 ∧ z = x + 3 ∧ x % 4 = 0 ∧ x ≠ 0 ∧ x ≠ 4 ∧ x ≠ 8) ∨
            (y = x + 2 ∧ z = x + 3 ∧ x % 4 = 3 ∧ x ≠ 3 ∧ x ≠ 7) ∨
            (y = x + 1 ∧ z = x + 5 ∧ x % 8 = 2) ∨
            (y = x + 2 ∧ z = x + 5 ∧ x % 8 = 1) ∨
            (y = x + 1 ∧ z = x + 6 ∧ x % 8 = 1)))
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Theorem 13, value 4 on U.
Uses 3
Statement usesEquivalence of impartial games · Nim heap · The P&R Helper game

TheoremSprague–Grundy value \(5\) of P&R Helper on region \(U\)#●ready to prove

Let \(x \le y \le z\) be natural numbers with \(z < x + y\) and \(y \le 2x + 1\) (the region \(U\)). The P&R Helper position \([x, y, z]\) is equivalent to the Nim heap \(*5\), that is, has Sprague–Grundy value \(5\), if and only if one of the following holds: - \([x, y, z]\) is \([3, 4, 4]\) or \([7, 8, 9]\); - \(y = x + 1\), \(z = x + 3\), \(x \equiv 0 \pmod 4\) and \(x \notin \{0, 4, 8\}\); - \(y = x + 2\), \(z = x + 3\), \(x \equiv 3 \pmod 4\) and \(x \notin \{3, 7\}\); - \(y = x + 1\), \(z = x + 5\) and \(x \equiv 2 \pmod 8\); - \(y = x + 1\), \(z = x + 6\) and \(x \equiv 1 \pmod 8\); - \(y + z - x \equiv 7 \pmod 8\), \(y = x + 2\), \(z > x + 4\) and \(x + y - z > 2\); - \(y + z - x \equiv 7 \pmod 8\), \(z = x + y - 3\) and \(x + 2 < y \le 2x\).

public theorem_wanted princessRosesHelper_equiv_nimHeap_five_iff_of_mem_U (x y z : ℕ)
    (hxy : x ≤ y) (hyz : y ≤ z) (hU : z < x + y ∧ y ≤ 2 * x + 1) :
    Equiv (princessRosesHelper (x, y, z)) (nimHeap 5) ↔
      (x, y, z) ∈ [(3, 4, 4), (7, 8, 9)] ∨
        (y = x + 1 ∧ z = x + 3 ∧ x % 4 = 0 ∧ x ≠ 0 ∧ x ≠ 4 ∧ x ≠ 8) ∨
        (y = x + 2 ∧ z = x + 3 ∧ x % 4 = 3 ∧ x ≠ 3 ∧ x ≠ 7) ∨
        (y = x + 1 ∧ z = x + 5 ∧ x % 8 = 2) ∨
        (y = x + 1 ∧ z = x + 6 ∧ x % 8 = 1) ∨
        ((y + z - x) % 8 = 7 ∧ x + 4 < z ∧ y = x + 2 ∧ 2 < x + y - z) ∨
        ((y + z - x) % 8 = 7 ∧ z = x + y - 3 ∧ x + 2 < y ∧ y ≤ 2 * x)
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Theorem 13, value 5 on U.
Uses 3
Statement usesEquivalence of impartial games · Nim heap · The P&R Helper game

TheoremP&R Helper positions of Sprague–Grundy value 6 or 7 on region U#●ready to prove

For natural numbers \(x \le y \le z\) with \(z < x + y\) and \(y \le 2x + 1\) (the region \(U\)), the P&R Helper game started at \([x, y, z]\) is equivalent to the Nim heap of size \(6\) (that is, has Sprague–Grundy value \(6\)) if and only if \(y = x + 2\), \(z = x + 5\) and \(x \equiv 1 \pmod 8\); and it is never equivalent to the Nim heap of size \(7\).

public theorem_wanted princessRosesHelper_equiv_nimHeap_six_iff_of_mem_U (x y z : ℕ)
    (hxy : x ≤ y) (hyz : y ≤ z) (hU : z < x + y ∧ y ≤ 2 * x + 1) :
    (Equiv (princessRosesHelper (x, y, z)) (nimHeap 6) ↔
        y = x + 2 ∧ z = x + 5 ∧ x % 8 = 1) ∧
      ¬ Equiv (princessRosesHelper (x, y, z)) (nimHeap 7)
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Theorem 13, values 6 and 7 on U.
Uses 3
Statement usesEquivalence of impartial games · Nim heap · The P&R Helper game

TheoremSprague–Grundy values of P&R Helper on region R#●ready to prove

Let \(x \le y \le z\) be natural numbers with \(z < x + y\) and \(y > 2x + 1\) (the region \(R\)), and write \(s = y + z - x\). For every natural number \(n\), the P&R Helper game started at \([x, y, z]\) is equivalent to the Nim heap of size \(n\) (that is, has Sprague–Grundy value \(n\)) if and only if one of the following holds: \(n = 0\) and \(x\), \(y\), \(z\) are all even; \(n = 1\) and \(s \equiv 1 \pmod 4\); \(n = 2\), \(x\) is even and \(y\), \(z\) are odd; \(n = 3\) and \(s \equiv 3 \pmod 4\); \(n = 4\), \(x\) is odd and \(s \equiv 0 \pmod 4\); \(n = 5\), \(x\) is odd and \(s \equiv 2 \pmod 4\).

public theorem_wanted princessRosesHelper_equiv_nimHeap_iff_of_mem_R (x y z n : ℕ)
    (hxy : x ≤ y) (hyz : y ≤ z) (hR : z < x + y ∧ 2 * x + 1 < y) :
    Equiv (princessRosesHelper (x, y, z)) (nimHeap n) ↔
      (n = 0 ∧ Even x ∧ Even y ∧ Even z) ∨
        (n = 1 ∧ (y + z - x) % 4 = 1) ∨
        (n = 2 ∧ Even x ∧ Odd y ∧ Odd z) ∨
        (n = 3 ∧ (y + z - x) % 4 = 3) ∨
        (n = 4 ∧ Odd x ∧ (y + z - x) % 4 = 0) ∨
        (n = 5 ∧ Odd x ∧ (y + z - x) % 4 = 2)
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Theorem 13, region R.
Uses 3
Statement usesEquivalence of impartial games · Nim heap · The P&R Helper game

TheoremSprague–Grundy values of P&R Helper on region L#●ready to prove

Let \(x \le y \le z\) be natural numbers with \(z \ge x + y\) and \(y \le 2x\) (the region \(L\)). For every natural number \(n\), the P&R Helper game started at \([x, y, z]\) is equivalent to the Nim heap of size \(n\) (that is, has Sprague–Grundy value \(n\)) if and only if one of the following holds: \(n = 0\) and \(x\), \(y\), \(z\) are all even; \(n = 1\), \(x\) and \(y\) are even and \(z\) is odd; \(n = 2\) and \(y + 2z - 2x \equiv 3 \pmod 4\); \(n = 3\) and \(y + 2z - 2x \equiv 1 \pmod 4\); \(n = 4\), \(x\) and \(z\) are odd and \(y\) is even; \(n = 5\), \(x\) is odd and \(y\) and \(z\) are even.

public theorem_wanted princessRosesHelper_equiv_nimHeap_iff_of_mem_L (x y z n : ℕ)
    (hxy : x ≤ y) (hyz : y ≤ z) (hL : x + y ≤ z ∧ y ≤ 2 * x) :
    Equiv (princessRosesHelper (x, y, z)) (nimHeap n) ↔
      (n = 0 ∧ Even x ∧ Even y ∧ Even z) ∨
        (n = 1 ∧ Even x ∧ Even y ∧ Odd z) ∨
        (n = 2 ∧ (y + 2 * z - 2 * x) % 4 = 3) ∨
        (n = 3 ∧ (y + 2 * z - 2 * x) % 4 = 1) ∨
        (n = 4 ∧ Odd x ∧ Even y ∧ Odd z) ∨
        (n = 5 ∧ Odd x ∧ Even y ∧ Even z)
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Theorem 13, region L.
Uses 3
Statement usesEquivalence of impartial games · Nim heap · The P&R Helper game

TheoremSprague–Grundy values of P&R Helper on region D#●ready to prove

Let \(x \le y \le z\) be natural numbers with \(z \ge x + y\) and \(y > 2x\) (the region \(D\)). For every natural number \(n\), the P&R Helper game started at \([x, y, z]\) is equivalent to the Nim heap of size \(n\) (that is, has Sprague–Grundy value \(n\)) if and only if \(n\) is the number assigned to the parities of \((x, y, z)\) as follows: \(0\) to (even, even, even), \(1\) to (even, even, odd), \(2\) to (even, odd, odd), \(3\) to (even, odd, even), \(4\) to (odd, even, odd), \(5\) to (odd, even, even), \(6\) to (odd, odd, even) and \(7\) to (odd, odd, odd).

public theorem_wanted princessRosesHelper_equiv_nimHeap_iff_of_mem_D (x y z n : ℕ)
    (hxy : x ≤ y) (hyz : y ≤ z) (hD : x + y ≤ z ∧ 2 * x < y) :
    Equiv (princessRosesHelper (x, y, z)) (nimHeap n) ↔
      (n = 0 ∧ Even x ∧ Even y ∧ Even z) ∨
        (n = 1 ∧ Even x ∧ Even y ∧ Odd z) ∨
        (n = 2 ∧ Even x ∧ Odd y ∧ Odd z) ∨
        (n = 3 ∧ Even x ∧ Odd y ∧ Even z) ∨
        (n = 4 ∧ Odd x ∧ Even y ∧ Odd z) ∨
        (n = 5 ∧ Odd x ∧ Even y ∧ Even z) ∨
        (n = 6 ∧ Odd x ∧ Odd y ∧ Even z) ∨
        (n = 7 ∧ Odd x ∧ Odd y ∧ Odd z)
Sources
  • Zev Friedman, Sprague-Grundy Values for 4-Pile Princess and the Roses, INTEGERS 26 (2026), Article G4, Theorem 13, region D.
Uses 3
Statement usesEquivalence of impartial games · Nim heap · The P&R Helper game

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.