Nim on a cube

DefinitionRotation move on the cube#✓fully proved

Label the faces of a cube \(f_a, f_b, f_c, f_A, f_B, f_C\), where \(f_A\), \(f_B\), \(f_C\) are opposite \(f_a\), \(f_b\), \(f_c\), and record a position as the tuple \(p = (a, b, c, A, B, C)\) of numbers of tokens on these faces. A rotation is one of the three belts of four faces \(\{f_a, f_b, f_A, f_B\}\), \(\{f_a, f_c, f_A, f_C\}\) and \(\{f_b, f_c, f_B, f_C\}\). In the game \(C_R\) there is a move from a position \(p\) to a position \(q\) when, for some rotation, \(q\) agrees with \(p\) on the two faces outside the rotation, \(q \le p\) on every face, and \(q \ne p\); that is, at least one token in total is removed from the four faces of the rotation.

def CubeRotationMove (p q : Fin 6 → ℕ) : Prop :=
  ∃ i j : Fin 6, ((i = 0 ∧ j = 1) ∨ (i = 0 ∧ j = 2) ∨ (i = 1 ∧ j = 2)) ∧
    q ≤ p ∧ q ≠ p ∧
    ∀ k : Fin 6, k ≠ i → k ≠ j → k ≠ i + 3 → k ≠ j + 3 → q k = p k
Sources
  • Balaji R. Kadam and A. J. Shaiju, Variations of the Nim Game Played on a Cube, INTEGERS 25 (2025), Article G2, Section 2 (the variation C_R).
Used by 4
Used byRotation moves at the empty cube · Misère P-positions of rotation Nim on a cube · P-positions of rotation Nim on a cube · P-positions of slow rotation Nim on a cube

TheoremRotation moves at the empty cube#✓fully proved

Write positions as tuples \((a, b, c, A, B, C)\) of numbers of tokens on the faces \(f_a, f_b, f_c, f_A, f_B, f_C\) of a cube. In the game \(C_R\) there is a rotation move from \((0, 0, 0, 0, 0, 1)\) to the empty position \((0, 0, 0, 0, 0, 0)\), and there is no rotation move from the empty position.

theorem cubeRotationMove_examples :
    CubeRotationMove ![0, 0, 0, 0, 0, 1] 0 ∧ ∀ q, ¬ CubeRotationMove 0 q
Sources
  • Balaji R. Kadam and A. J. Shaiju, Variations of the Nim Game Played on a Cube, INTEGERS 25 (2025), Article G2, Section 2 (the variation C_R).
Uses 1
Statement usesRotation move on the cube

DefinitionVertex move on the cube#✓fully proved

Label the faces of a cube \(f_a, f_b, f_c, f_A, f_B, f_C\), where \(f_A\), \(f_B\), \(f_C\) are opposite \(f_a\), \(f_b\), \(f_c\), and record a position as the tuple \(p = (a, b, c, A, B, C)\) of numbers of tokens on these faces. In the game \(C_V\) there is a move from a position \(p\) to a position \(q\) when, for some choice of one face from each opposite pair \(\{f_a, f_A\}\), \(\{f_b, f_B\}\), \(\{f_c, f_C\}\) (three faces that meet at a vertex), \(q\) agrees with \(p\) on the other three faces, \(q \le p\) on every face, and \(q \ne p\); that is, at least one token in total is removed from the three faces at one vertex.

def CubeVertexMove (p q : Fin 6 → ℕ) : Prop :=
  ∃ x y z : Fin 6, x.val % 3 = 0 ∧ y.val % 3 = 1 ∧ z.val % 3 = 2 ∧ q ≤ p ∧ q ≠ p ∧
    ∀ k : Fin 6, k ≠ x → k ≠ y → k ≠ z → q k = p k
Sources
  • Balaji R. Kadam and A. J. Shaiju, Variations of the Nim Game Played on a Cube, INTEGERS 25 (2025), Article G2, Section 1 (the variation C_V).
Used by 4
Used byExamples of vertex, edge and face moves · Misère P-positions of vertex Nim on a cube · P-positions of vertex Nim on a cube · P-positions of slow vertex Nim on a cube

DefinitionEdge move on the cube#✓fully proved

Label the faces of a cube \(f_a, f_b, f_c, f_A, f_B, f_C\), where \(f_A\), \(f_B\), \(f_C\) are opposite \(f_a\), \(f_b\), \(f_c\), and record a position as the tuple \(p = (a, b, c, A, B, C)\) of numbers of tokens on these faces. In the game \(C_E\) there is a move from a position \(p\) to a position \(q\) when, for some two faces from different opposite pairs (two faces that share an edge), \(q\) agrees with \(p\) on the other four faces, \(q \le p\) on every face, and \(q \ne p\); that is, at least one token in total is removed from the two faces at one edge.

def CubeEdgeMove (p q : Fin 6 → ℕ) : Prop :=
  ∃ x y : Fin 6, x.val % 3 ≠ y.val % 3 ∧ q ≤ p ∧ q ≠ p ∧ ∀ k : Fin 6, k ≠ x → k ≠ y → q k = p k
Sources
  • Balaji R. Kadam and A. J. Shaiju, Variations of the Nim Game Played on a Cube, INTEGERS 25 (2025), Article G2, Section 1 (the variation C_E).
Used by 3
Used byP-positions of edge Nim on a cube · Examples of vertex, edge and face moves · P-positions of slow edge Nim on a cube

DefinitionFace move on the cube#✓fully proved

Label the faces of a cube \(f_a, f_b, f_c, f_A, f_B, f_C\), where \(f_A\), \(f_B\), \(f_C\) are opposite \(f_a\), \(f_b\), \(f_c\), and record a position as the tuple \(p = (a, b, c, A, B, C)\) of numbers of tokens on these faces. In the game \(C_F\) there is a move from a position \(p\) to a position \(q\) when, for some face, \(q\) agrees with \(p\) on the other five faces, \(q \le p\) on every face, and \(q \ne p\); that is, at least one token is removed from one face. So \(C_F\) is Nim with six heaps.

def CubeFaceMove (p q : Fin 6 → ℕ) : Prop :=
  ∃ x : Fin 6, q ≤ p ∧ q ≠ p ∧ ∀ k : Fin 6, k ≠ x → q k = p k
Sources
  • Balaji R. Kadam and A. J. Shaiju, Variations of the Nim Game Played on a Cube, INTEGERS 25 (2025), Article G2, Section 1 (the variation C_F).
Used by 3
Used byMisère P-positions of face Nim on a cube · Examples of vertex, edge and face moves · P-positions of slow face Nim on a cube

TheoremExamples of vertex, edge and face moves#✓fully proved

Write positions as tuples \((a, b, c, A, B, C)\) of numbers of tokens on the faces \(f_a, f_b, f_c, f_A, f_B, f_C\) of a cube. There is a vertex move (game \(C_V\)) from \((1, 1, 1, 0, 0, 0)\) to the empty position \((0, 0, 0, 0, 0, 0)\), an edge move (game \(C_E\)) from \((1, 1, 0, 0, 0, 0)\) to the empty position, and a face move (game \(C_F\)) from \((1, 1, 1, 0, 0, 0)\) to \((0, 1, 1, 0, 0, 0)\). No vertex move, edge move or face move starts at the empty position.

theorem cubeVertexEdgeFaceMove_examples :
    CubeVertexMove ![1, 1, 1, 0, 0, 0] 0 ∧ CubeEdgeMove ![1, 1, 0, 0, 0, 0] 0 ∧
      CubeFaceMove ![1, 1, 1, 0, 0, 0] ![0, 1, 1, 0, 0, 0] ∧
      ∀ q, ¬ CubeVertexMove 0 q ∧ ¬ CubeEdgeMove 0 q ∧ ¬ CubeFaceMove 0 q
Sources
  • Balaji R. Kadam and A. J. Shaiju, Variations of the Nim Game Played on a Cube, INTEGERS 25 (2025), Article G2, Section 1.
Uses 3
Statement usesEdge move on the cube · Face move on the cube · Vertex move on the cube

TheoremP-positions of rotation Nim on a cube#●ready to prove

Write positions of the game \(C_R\) as tuples \((a, b, c, A, B, C)\) of numbers of tokens on the faces \(f_a, f_b, f_c, f_A, f_B, f_C\), where \(f_A\), \(f_B\), \(f_C\) are opposite \(f_a\), \(f_b\), \(f_c\). Let \(\mathcal P\) be the set of positions with \(a + A = b + B = c + C\). Then no rotation move leads from a position in \(\mathcal P\) to a position in \(\mathcal P\), and from every position outside \(\mathcal P\) there is a rotation move to a position in \(\mathcal P\).

Every move removes a token, so the game terminates and \(\mathcal P\) is exactly the set of P-positions (second-player wins) under normal play.

public theorem_wanted cubeRotationNim_pPositions :
    let P : Set (Fin 6 → ℕ) := {p | p 0 + p 3 = p 1 + p 4 ∧ p 1 + p 4 = p 2 + p 5}
    (∀ p q, p ∈ P → CubeRotationMove p q → q ∉ P) ∧
      ∀ p, p ∉ P → ∃ q, CubeRotationMove p q ∧ q ∈ P
Sources
  • Balaji R. Kadam and A. J. Shaiju, Variations of the Nim Game Played on a Cube, INTEGERS 25 (2025), Article G2, Theorem 5.
Uses 1
Statement usesRotation move on the cube

TheoremP-positions of vertex Nim on a cube#●ready to prove

Write a position of the cube game as \(p = (a, b, c, A, B, C)\), the numbers of tokens on the six faces of a cube, where the faces carrying \(A\), \(B\), \(C\) are opposite those carrying \(a\), \(b\), \(c\); a vertex move removes at least one token in total from the three faces at one vertex (one face from each opposite pair). Let \(P\) be the set of positions with \(a = A\), \(b = B\) and \(c = C\). Then no vertex move leads from a position in \(P\) to a position in \(P\), and from every position not in \(P\) some vertex move leads to a position in \(P\).

Since every play terminates, these two properties make \(P\) the set of P-positions (second-player wins) under normal play.

public theorem_wanted cubeVertexNim_pPositions :
    let P : Set (Fin 6 → ℕ) := {p | p 0 = p 3 ∧ p 1 = p 4 ∧ p 2 = p 5}
    (∀ p q, p ∈ P → CubeVertexMove p q → q ∉ P) ∧
      ∀ p, p ∉ P → ∃ q, CubeVertexMove p q ∧ q ∈ P
Sources
  • Balaji R. Kadam and A. J. Shaiju, Variations of the Nim Game Played on a Cube, INTEGERS 25 (2025), Article G2, Theorem 2.
Uses 1
Statement usesVertex move on the cube

TheoremP-positions of edge Nim on a cube#●ready to prove

Write positions of the game \(C_E\) as tuples \((a, b, c, A, B, C)\) of numbers of tokens on the faces \(f_a, f_b, f_c, f_A, f_B, f_C\), where \(f_A\), \(f_B\), \(f_C\) are opposite \(f_a\), \(f_b\), \(f_c\), and let \(\oplus\) be the Nim-sum (bitwise exclusive or) of natural numbers. Let \(\mathcal P\) be the set of positions with \(a \oplus A = b \oplus B = c \oplus C\). Then no edge move leads from a position in \(\mathcal P\) to a position in \(\mathcal P\), and from every position outside \(\mathcal P\) there is an edge move to a position in \(\mathcal P\).

Every move removes a token, so the game terminates and \(\mathcal P\) is exactly the set of P-positions (second-player wins) under normal play.

public theorem_wanted cubeEdgeNim_pPositions :
    let P : Set (Fin 6 → ℕ) := {p | p 0 ^^^ p 3 = p 1 ^^^ p 4 ∧ p 1 ^^^ p 4 = p 2 ^^^ p 5}
    (∀ p q, p ∈ P → CubeEdgeMove p q → q ∉ P) ∧
      ∀ p, p ∉ P → ∃ q, CubeEdgeMove p q ∧ q ∈ P
Sources
  • Balaji R. Kadam and A. J. Shaiju, Variations of the Nim Game Played on a Cube, INTEGERS 25 (2025), Article G2, Theorem 3.
Uses 1
Statement usesEdge move on the cube

TheoremMisère P-positions of vertex Nim on a cube#●ready to prove

Write a position of the cube game as \(p = (a, b, c, A, B, C)\), the numbers of tokens on the six faces of a cube, where the faces carrying \(A\), \(B\), \(C\) are opposite those carrying \(a\), \(b\), \(c\); a vertex move removes at least one token in total from the three faces at one vertex (one face from each opposite pair). Let \(P\) be any set of positions such that \(p \in P\) if and only if \(p\) has a vertex move and no vertex move from \(p\) leads to a position in \(P\) (the misère P-positions). Then for every position \(p\) with \(a \le A\), \(b \le B\), \(a \le b\) and \(C\) at least every entry of \(p\), we have \(p \in P\) if and only if either \(a = A\), \(b = B\), \(c = C\) and \(C \ge 2\) all hold, or \(p\) is one of \((0, 0, 0, 0, 0, 1)\), \((0, 1, 1, 0, 1, 1)\) and \((1, 1, 1, 1, 1, 1)\).

public theorem_wanted cubeVertexNim_misere_pPositions (P : Set (Fin 6 → ℕ))
    (hP : ∀ p, p ∈ P ↔ (∃ q, CubeVertexMove p q) ∧ ∀ q, CubeVertexMove p q → q ∉ P)
    (p : Fin 6 → ℕ) (hC : ∀ k, p k ≤ p 5) (ha : p 0 ≤ p 3) (hb : p 1 ≤ p 4) (hab : p 0 ≤ p 1) :
    p ∈ P ↔ (p 0 = p 3 ∧ p 1 = p 4 ∧ p 2 = p 5 ∧ 2 ≤ p 5) ∨ p = ![0, 0, 0, 0, 0, 1] ∨
      p = ![0, 1, 1, 0, 1, 1] ∨ p = ![1, 1, 1, 1, 1, 1]
Sources
  • Balaji R. Kadam and A. J. Shaiju, Variations of the Nim Game Played on a Cube, INTEGERS 25 (2025), Article G2, Theorem 6.
Uses 1
Statement usesVertex move on the cube

TheoremMisère P-positions of rotation Nim on a cube#●ready to prove

Write positions of the game \(C_R\) as tuples \(p = (a, b, c, A, B, C)\) of numbers of tokens on the faces \(f_a, f_b, f_c, f_A, f_B, f_C\), where \(f_A\), \(f_B\), \(f_C\) are opposite \(f_a\), \(f_b\), \(f_c\). Let \(\mathcal P\) be any set of positions such that a position lies in \(\mathcal P\) if and only if it has a rotation move and every rotation move from it leads to a position outside \(\mathcal P\); this is the set of P-positions under misère play, where the player making the last move loses. Let \(p\) be a position in which every entry is at most \(C\), and \(a \le A\), \(b \le B\) and \(a \le b\). Then \(p \in \mathcal P\) if and only if either \(C \ge 2\) and \(a + A = b + B = c + C\), or \(p = (0, 0, 0, 0, 0, 1)\), or \(p = (1, 1, 1, 1, 1, 1)\).

public theorem_wanted cubeRotationNim_misere_pPositions (P : Set (Fin 6 → ℕ))
    (hP : ∀ p, p ∈ P ↔ (∃ q, CubeRotationMove p q) ∧ ∀ q, CubeRotationMove p q → q ∉ P)
    (p : Fin 6 → ℕ) (hC : ∀ k, p k ≤ p 5) (ha : p 0 ≤ p 3) (hb : p 1 ≤ p 4) (hab : p 0 ≤ p 1) :
    p ∈ P ↔ (2 ≤ p 5 ∧ p 0 + p 3 = p 1 + p 4 ∧ p 1 + p 4 = p 2 + p 5) ∨
      p = ![0, 0, 0, 0, 0, 1] ∨ p = ![1, 1, 1, 1, 1, 1]
Sources
  • Balaji R. Kadam and A. J. Shaiju, Variations of the Nim Game Played on a Cube, INTEGERS 25 (2025), Article G2, Theorem 8.
Uses 1
Statement usesRotation move on the cube

TheoremMisère P-positions of face Nim on a cube#●ready to prove

Write positions of the game \(C_F\) (Nim with six heaps) as tuples \(p = (a, b, c, A, B, C)\) of numbers of tokens on the faces \(f_a, f_b, f_c, f_A, f_B, f_C\), where \(f_A\), \(f_B\), \(f_C\) are opposite \(f_a\), \(f_b\), \(f_c\), and let \(\oplus\) be the Nim-sum (bitwise exclusive or) of natural numbers. Let \(\mathcal P\) be any set of positions such that a position lies in \(\mathcal P\) if and only if it has a face move and every face move from it leads to a position outside \(\mathcal P\); this is the set of P-positions under misère play, where the player making the last move loses. Let \(p\) be a position in which every entry is at most \(C\), and \(a \le A\), \(b \le B\) and \(a \le b\). Then \(p \in \mathcal P\) if and only if either \(C \ge 2\) and \(a \oplus b \oplus c \oplus A \oplus B \oplus C = 0\), or \(C < 2\) and \(a \oplus b \oplus c \oplus A \oplus B \oplus C = 1\).

public theorem_wanted cubeFaceNim_misere_pPositions (P : Set (Fin 6 → ℕ))
    (hP : ∀ p, p ∈ P ↔ (∃ q, CubeFaceMove p q) ∧ ∀ q, CubeFaceMove p q → q ∉ P)
    (p : Fin 6 → ℕ) (hC : ∀ k, p k ≤ p 5) (ha : p 0 ≤ p 3) (hb : p 1 ≤ p 4) (hab : p 0 ≤ p 1) :
    p ∈ P ↔ (2 ≤ p 5 ∧ p 0 ^^^ p 1 ^^^ p 2 ^^^ p 3 ^^^ p 4 ^^^ p 5 = 0) ∨
      (p 5 < 2 ∧ p 0 ^^^ p 1 ^^^ p 2 ^^^ p 3 ^^^ p 4 ^^^ p 5 = 1)
Sources
  • Balaji R. Kadam and A. J. Shaiju, Variations of the Nim Game Played on a Cube, INTEGERS 25 (2025), Article G2, Theorem 9.
Uses 1
Statement usesFace move on the cube

TheoremP-positions of slow vertex Nim on a cube#●ready to prove

Write a position of the cube game as \(p = (a, b, c, A, B, C)\), the numbers of tokens on the six faces of a cube, where the faces carrying \(A\), \(B\), \(C\) are opposite those carrying \(a\), \(b\), \(c\). A slow vertex move is a vertex move (removing at least one token in total from the three faces at one vertex, one face from each opposite pair) in which each face loses at most one token. Let \(P\) be the set of positions for which \(a + A\), \(b + B\) and \(c + C\) are all even. Then no slow vertex move leads from a position in \(P\) to a position in \(P\), and from every position not in \(P\) some slow vertex move leads to a position in \(P\).

Since every play terminates, these two properties make \(P\) the set of P-positions of the slow game under normal play.

public theorem_wanted slowCubeVertexNim_pPositions :
    let M : (Fin 6 → ℕ) → (Fin 6 → ℕ) → Prop := fun p q =>
      CubeVertexMove p q ∧ ∀ k, p k ≤ q k + 1
    let P : Set (Fin 6 → ℕ) :=
      {p | (p 0 + p 3) % 2 = 0 ∧ (p 1 + p 4) % 2 = 0 ∧ (p 2 + p 5) % 2 = 0}
    (∀ p q, p ∈ P → M p q → q ∉ P) ∧ ∀ p, p ∉ P → ∃ q, M p q ∧ q ∈ P
Sources
  • Balaji R. Kadam and A. J. Shaiju, Variations of the Nim Game Played on a Cube, INTEGERS 25 (2025), Article G2, Theorem 10.
Uses 1
Statement usesVertex move on the cube

TheoremP-positions of slow edge Nim on a cube#●ready to prove

Write a position of the cube game as \(p = (a, b, c, A, B, C)\), the numbers of tokens on the six faces of a cube, where the faces carrying \(A\), \(B\), \(C\) are opposite those carrying \(a\), \(b\), \(c\). A slow edge move is an edge move (removing at least one token in total from two faces in different opposite pairs) in which each face loses at most one token. Let \(P\) be the set of positions for which \(a + A\), \(b + B\) and \(c + C\) are all even or all odd. Then no slow edge move leads from a position in \(P\) to a position in \(P\), and from every position not in \(P\) some slow edge move leads to a position in \(P\).

Since every play terminates, these two properties make \(P\) the set of P-positions of the slow game under normal play.

public theorem_wanted slowCubeEdgeNim_pPositions :
    let M : (Fin 6 → ℕ) → (Fin 6 → ℕ) → Prop := fun p q =>
      CubeEdgeMove p q ∧ ∀ k, p k ≤ q k + 1
    let P : Set (Fin 6 → ℕ) :=
      {p | (p 0 + p 3) % 2 = (p 1 + p 4) % 2 ∧ (p 1 + p 4) % 2 = (p 2 + p 5) % 2}
    (∀ p q, p ∈ P → M p q → q ∉ P) ∧ ∀ p, p ∉ P → ∃ q, M p q ∧ q ∈ P
Sources
  • Balaji R. Kadam and A. J. Shaiju, Variations of the Nim Game Played on a Cube, INTEGERS 25 (2025), Article G2, Theorem 11.
Uses 1
Statement usesEdge move on the cube

TheoremP-positions of slow face Nim on a cube#●ready to prove

Write a position of the cube game as \(p = (a, b, c, A, B, C)\), the numbers of tokens on the six faces of a cube. A slow face move is a face move that removes exactly one token from one face. Let \(P\) be the set of positions with \(a + b + c + A + B + C\) even. Then no slow face move leads from a position in \(P\) to a position in \(P\), and from every position not in \(P\) some slow face move leads to a position in \(P\).

Since every play terminates, these two properties make \(P\) the set of P-positions of the slow game under normal play.

public theorem_wanted slowCubeFaceNim_pPositions :
    let M : (Fin 6 → ℕ) → (Fin 6 → ℕ) → Prop := fun p q =>
      CubeFaceMove p q ∧ ∀ k, p k ≤ q k + 1
    let P : Set (Fin 6 → ℕ) := {p | (∑ k, p k) % 2 = 0}
    (∀ p q, p ∈ P → M p q → q ∉ P) ∧ ∀ p, p ∉ P → ∃ q, M p q ∧ q ∈ P
Sources
  • Balaji R. Kadam and A. J. Shaiju, Variations of the Nim Game Played on a Cube, INTEGERS 25 (2025), Article G2, Theorem 12.
Uses 1
Statement usesFace move on the cube

TheoremP-positions of slow rotation Nim on a cube#●ready to prove

Write a position of the cube game as \(p = (a, b, c, A, B, C)\), the numbers of tokens on the six faces of a cube, where the faces carrying \(A\), \(B\), \(C\) are opposite those carrying \(a\), \(b\), \(c\). A slow rotation move is a rotation move (removing at least one token in total from the four faces of one rotation, that is from the faces of two opposite pairs) in which each face loses at most one token. Let \(P\) be any set of positions such that \(p \in P\) if and only if no slow rotation move from \(p\) leads to a position in \(P\) (the P-positions under normal play). Then for every position \(p\) with \(a \le A\), \(b \le B\) and \(c \le C\), we have \(p \in P\) if and only if the vector of remainders \((a, b, c, A, B, C) \bmod 2\) is one of \((0, 0, 0, 0, 0, 0)\), \((0, 0, 0, 1, 1, 1)\), \((1, 1, 1, 0, 0, 0)\) and \((1, 1, 1, 1, 1, 1)\).

public theorem_wanted slowCubeRotationNim_pPositions (P : Set (Fin 6 → ℕ))
    (hP : ∀ p, p ∈ P ↔ ∀ q, (CubeRotationMove p q ∧ ∀ k, p k ≤ q k + 1) → q ∉ P)
    (p : Fin 6 → ℕ) (ha : p 0 ≤ p 3) (hb : p 1 ≤ p 4) (hc : p 2 ≤ p 5) :
    p ∈ P ↔ (fun k => p k % 2) ∈ ({![0, 0, 0, 0, 0, 0], ![0, 0, 0, 1, 1, 1], ![1, 1, 1, 0, 0, 0],
      ![1, 1, 1, 1, 1, 1]} : Set (Fin 6 → ℕ))
Sources
  • Balaji R. Kadam and A. J. Shaiju, Variations of the Nim Game Played on a Cube, INTEGERS 25 (2025), Article G2, Theorem 13.
Uses 1
Statement usesRotation move on the cube
6 fully proved10 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.