Slow Nim

DefinitionPlaying on a set of stacks#✓fully proved

Let \(p\) be a position of Slow\(A\)-Nim on \(n\) stacks, with \(p_i\) tokens on stack \(i\), and let \(S\) be a set of stacks. The position after playing on \(S\) is obtained by removing one token from each stack of \(S\): its stack \(i\) holds \(p_i - 1\) if \(i \in S\) and \(p_i\) otherwise, where an empty stack of \(S\) stays empty.

public def slowANimAfter {n : ℕ} (p : Fin n → ℕ) (S : Finset (Fin n)) : Fin n → ℕ :=
  fun i => if i ∈ S then p i - 1 else p i

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Definition in Section 1.

Used by 12

Used byOptions in Princess and the Roses · Moves at a position supported by an (A0) basic vector (Lemma 2) · Unique critical-lowering move for odd parameter (Corollary 1 (ii)) · The M-move · General reduction lemma · Legal move sequences in Slow A-Nim · Options in Slow A-Nim · Terminal positions of exact slow \(k\)-NIM · The empty position has no options · Options with reduction in Slow {n - 1}-Nim · Options without reduction in Slow {n - 1}-Nim · Moves in Slow\(A\)-Nim decrease the token count

DefinitionOptions in Slow A-Nim#✓fully proved

Let \(A\) be a finite set of natural numbers and \(p\) a position on \(n\) stacks. The options of \(p\) in Slow\(A\)-Nim are the positions obtained from \(p\) by choosing a nonempty set \(S\) of stacks with \(|S| \in A\), each holding at least one token, and removing one token from each stack of \(S\).

public def slowANimMoves {n : ℕ} (A : Finset ℕ) (p : Fin n → ℕ) : Finset (Fin n → ℕ) :=
  ((Finset.univ : Finset (Finset (Fin n))).filter
      fun S => S.Nonempty ∧ S.card ∈ A ∧ ∀ i ∈ S, 1 ≤ p i).image (slowANimAfter p)

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Definition in Section 1.

Uses 1 · Used by 17

Statement usesPlaying on a set of stacks

Used byOptions in Princess and the Roses · In two-pile Princess and the Roses, \((1, 1)\) moves to \((0, 0)\) · Positions supported by a (B) basic vector (Lemma 1) · Moves at a position supported by an (A1) basic vector (Lemma 3) · Moves from critical positions with even parameter (Corollary 1 (i)) · Unique critical-lowering move for odd parameter (Corollary 1 (ii)) · Successor step of the truncated M-rule length · The empty position is terminal in the playable game graph · Slow\(A\)-Nim · Terminal positions of exact slow \(k\)-NIM · The empty position has no options · Reduced positions of Slow \(A\)-Nim · Moves of the playable game graph of Slow \(A\)-Nim · The empty position is reduced · Reduction of a Slow\(A\)-Nim position · The reduction never adds tokens · Moves in Slow\(A\)-Nim decrease the token count

TheoremMoves in Slow\(A\)-Nim decrease the token count#✓fully proved

For every finite set \(A\) of natural numbers and all positions \(p\), \(q\) of Slow\(A\)-Nim on \(n\) stacks, if \(q\) is reached from \(p\) by one move, then the total number of tokens strictly decreases: \(\sum_i q_i < \sum_i p_i\).

public theorem sum_lt_of_mem_slowANimMoves {n : ℕ} (A : Finset ℕ) (p q : Fin n → ℕ)
    (h : q ∈ slowANimMoves A p) : ∑ i, q i < ∑ i, p i

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Definition in Section 1.

Uses 2 · Used by 1

Statement usesOptions in Slow A-Nim

Proof usesPlaying on a set of stacks

Used bySlow\(A\)-Nim

DefinitionSlow\(A\)-Nim#✓fully proved

For \(n \in \mathbb{N}\) and a finite set \(A\) of natural numbers, Slow\(A\)-Nim \(\mathrm{SN}(n, A)\) is the impartial game whose positions assign a number \(p_i\) of tokens to each of \(n\) labelled stacks \(i\), and whose options from \(p\) are obtained by choosing a nonempty set \(S\) of stacks with \(|S| \in A\), each holding at least one token, and removing one token from each stack of \(S\). Its rank is the total number of tokens \(\sum_i p_i\), which every move lowers, and its start position is the empty position.

public def slowANimGame (n : ℕ) (A : Finset ℕ) : SpragueGrundy.ImpartialGame where
  Pos := Fin n → ℕ
  eqDec := inferInstance
  moves := slowANimMoves A
  rank := fun p => ∑ i, p i
  rank_lt := sum_lt_of_mem_slowANimMoves A
  start := fun _ => 0

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Definition in Section 1.

Uses 3 · Used by 16

Statement usesImpartial game · Options in Slow A-Nim · Moves in Slow\(A\)-Nim decrease the token count

Used byThe Princess and the Roses game · Basic-vector value equals Smith's remoteness (Lemma 4) · Theorem 2 (the M-rule realizes Smith's remoteness) · Proposition 1 (odd P-positions of exact slow k-NIM) · Remoteness of exact slow k-NIM from a list of piles · \(m\)-critical positions of exact slow \(k\)-NIM · The empty position is \(0\)-critical · Positions with the same reduction have the same outcome · P-positions of Slow \(A\)-Nim via the playable game graph · The empty position is a P-position · P-positions of Slow A-Nim with A = {1, n}, n even · P-positions of Slow A-Nim with A = {1, k}, k odd · P-positions of Slow A-Nim with A = {1, 2} on five stacks · P-positions of Slow \(\{1,2\}\)-Nim on four stacks · P-positions of Slow \(\{1,2\}\)-Nim on three stacks · Partial structure of the P-positions of Slow \(A\)-Nim

TheoremThe empty position has no options#✓fully proved

For every finite set \(A\) of natural numbers, the position of Slow\(A\)-Nim on \(n\) stacks in which every stack is empty has no options.

public theorem slowANimMoves_zero {n : ℕ} (A : Finset ℕ) :
    slowANimMoves A (fun _ : Fin n => 0) = ∅

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Section 2.

Uses 2 · Used by 4

Statement usesOptions in Slow A-Nim

Proof usesPlaying on a set of stacks

Used byThe empty position is \(0\)-critical · The empty position is terminal in the playable game graph · The empty position is a P-position · The empty position is reduced

TheoremThe empty position is a P-position#✓fully proved

For every \(n\) and every finite set \(A\) of natural numbers, the position of Slow\(A\)-Nim \(\mathrm{SN}(n, A)\) with all \(n\) stacks empty is a P-position, since it has no options.

public theorem slowANim_isP_zero (n : ℕ) (A : Finset ℕ) :
    SpragueGrundy.IsP (slowANimGame n A) (fun _ => 0)

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Section 2.

Uses 5

Statement usesP-positions · Slow\(A\)-Nim

Proof usesImpartial game · Recursive characterization of P-positions · The empty position has no options

DefinitionReduced positions of Slow \(A\)-Nim#✓fully proved

A position \(p\) of Slow \(A\)-Nim on \(n\) stacks is reduced when for every stack \(i\) there is a terminal position \(t\) (one with no options) that is reachable from \(p\) by a sequence of zero or more moves and has \(t_i = 0\).

In the source's notation, \(u_i(p) = \min_j t^{(j)}_i(p)\), the minimum over the terminal positions \(t^{(j)}(p)\) reachable from \(p\), counts the unplayable tokens of stack \(i\), and \(p\) is reduced exactly when \(u_i(p) = 0\) for every \(i\).

public def SlowANimReduced {n : ℕ} (A : Finset ℕ) (p : Fin n → ℕ) : Prop :=
  ∀ i, ∃ t, Relation.ReflTransGen (fun x y => y ∈ slowANimMoves A x) p t ∧
    slowANimMoves A t = ∅ ∧ t i = 0

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Definition in Section 3.1.

Uses 1 · Used by 12

Statement usesOptions in Slow A-Nim

Used byThe empty position is terminal in the playable game graph · General reduction lemma · P-positions of Slow \(A\)-Nim via the playable game graph · Options with reduction in Slow {n - 1}-Nim · Options without reduction in Slow {n - 1}-Nim · Moves of the playable game graph of Slow \(A\)-Nim · NIRB criterion for reduced positions · P-positions of the reduced game of Slow \(\{n-1\}\)-Nim · P-positions of the reduced game of Slow \(\{n-1, n\}\)-Nim · Chopping a reduced position keeps it reduced · The empty position is reduced · The reduction chops at the largest reduced height

DefinitionReduction of a Slow\(A\)-Nim position#✓fully proved

Let \(A\) be a finite set of natural numbers and let \(p\) be a position of Slow\(A\)-Nim on \(n\) stacks. For each stack \(i\), let \(u_i(p)\) be the least height of stack \(i\) over all terminal positions (positions with no moves) reachable from \(p\) by a sequence of zero or more moves. The reduction of \(p\) is the position \(r(p)\) with \(r(p)_i = p_i - u_i(p)\) for every stack \(i\).

public noncomputable def slowANimReduction {n : ℕ} (A : Finset ℕ) (p : Fin n → ℕ) :
    Fin n → ℕ :=
  fun i => p i - sInf ((fun t : Fin n → ℕ => t i) ''
    {t | Relation.ReflTransGen (fun x y => y ∈ slowANimMoves A x) p t ∧
      slowANimMoves A t = ∅})

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Definition in Section 3.1.

Uses 1 · Used by 8

Statement usesOptions in Slow A-Nim

Used byThe empty position is terminal in the playable game graph · Positions with the same reduction have the same outcome · P-positions of Slow \(A\)-Nim via the playable game graph · Legal move sequences depend only on the reduction · Options with reduction in Slow {n - 1}-Nim · Moves of the playable game graph of Slow \(A\)-Nim · The reduction chops at the largest reduced height · The reduction never adds tokens

TheoremThe empty position is reduced#✓fully proved

For every finite set \(A\) of natural numbers and every \(n\), the position of Slow \(A\)-Nim on \(n\) stacks in which every stack is empty is reduced.

public theorem slowANimReduced_zero {n : ℕ} (A : Finset ℕ) :
    SlowANimReduced A (fun _ : Fin n => 0)

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Definition in Section 3.1.

Uses 3 · Used by 1

Statement usesReduced positions of Slow \(A\)-Nim

Proof usesOptions in Slow A-Nim · The empty position has no options

Used byThe empty position is terminal in the playable game graph

TheoremThe reduction never adds tokens#✓fully proved

For every finite set \(A\) of natural numbers, every position \(p\) of Slow\(A\)-Nim on \(n\) stacks and every stack \(i\), the reduction \(r(p)\) of \(p\) satisfies \(r(p)_i \le p_i\).

public theorem slowANimReduction_le {n : ℕ} (A : Finset ℕ) (p : Fin n → ℕ) (i : Fin n) :
    slowANimReduction A p i ≤ p i

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Definition in Section 3.1.

Uses 2

Statement usesReduction of a Slow\(A\)-Nim position

Proof usesOptions in Slow A-Nim

DefinitionLegal move sequences in Slow A-Nim#✓fully proved

Let \(A\) be a finite set of natural numbers and \(p\) a position of Slow\(A\)-Nim on \(n\) stacks. A finite sequence \(S_1, \dots, S_m\) of sets of stacks is legal from \(p\) when it is empty, or when \(S_1\) is nonempty, \(|S_1| \in A\), every stack in \(S_1\) holds at least one token in \(p\), and \(S_2, \dots, S_m\) is legal from the position obtained from \(p\) by removing one token from each stack of \(S_1\).

public def SlowANimLegalSeq {n : ℕ} (A : Finset ℕ) : (Fin n → ℕ) → List (Finset (Fin n)) → Prop
  | _, [] => True
  | p, S :: ss =>
    S.Nonempty ∧ S.card ∈ A ∧ (∀ i ∈ S, 1 ≤ p i) ∧ SlowANimLegalSeq A (slowANimAfter p S) ss

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Lemma 1 and its proof.

Uses 1 · Used by 2

Statement usesPlaying on a set of stacks

Used byThe empty move sequence is legal · Legal move sequences depend only on the reduction

TheoremThe empty move sequence is legal#✓fully proved

For every finite set \(A\) of natural numbers and every position \(p\) of Slow\(A\)-Nim on \(n\) stacks, the empty sequence of moves is legal from \(p\).

public theorem slowANimLegalSeq_nil {n : ℕ} (A : Finset ℕ) (p : Fin n → ℕ) :
    SlowANimLegalSeq A p []

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Lemma 1 and its proof.

Uses 1

Statement usesLegal move sequences in Slow A-Nim

DefinitionSet of P-positions#✓fully proved

Let \(R\) be a move relation on a type of positions, where \(R\,x\,y\) means that \(y\) is an option of \(x\). A set \(P\) of positions is a set of P-positions for \(R\) when no position of \(P\) has an option in \(P\), and every position outside \(P\) has an option in \(P\).

When there is no infinite sequence of moves, there is at most one such set.

public def IsPPositionSet {α : Type*} (R : α → α → Prop) (P : Set α) : Prop :=
  (∀ x y, x ∈ P → R x y → y ∉ P) ∧ ∀ x, x ∉ P → ∃ y, R x y ∧ y ∈ P

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Section 1 (characterization of P-positions).

Used by 5

Used byUniqueness of the set of P-positions · P-positions after adding moves · P-positions of Slow \(A\)-Nim via the playable game graph · P-positions of the reduced game of Slow \(\{n-1\}\)-Nim · P-positions of the reduced game of Slow \(\{n-1, n\}\)-Nim

TheoremUniqueness of the set of P-positions#✓fully proved

Let \(R\) be a move relation on a type of positions, where \(R\,x\,y\) means that \(y\) is an option of \(x\), and suppose that there is no infinite sequence of moves (the relation "\(y\) is an option of \(x\)" is well-founded). If \(P\) and \(Q\) are both sets of P-positions for \(R\), then \(P = Q\).

public theorem IsPPositionSet.eq {α : Type*} {R : α → α → Prop}
    (hR : WellFounded fun y x => R x y) {P Q : Set α} (hP : IsPPositionSet R P)
    (hQ : IsPPositionSet R Q) : P = Q

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Section 1 (characterization of P-positions).

Uses 2

Statement usesSet of P-positions

Proof usesUniqueness of the P-positions of a terminating impartial game

TheoremPartial structure of the P-positions of Slow \(A\)-Nim#●ready to prove

Let \(A \subseteq \{1, \dots, n\}\) and let \(p\) be a position of Slow \(A\)-Nim on \(n\) stacks. If every stack height of \(p\) is even, then \(p\) is a P-position. If the number of stacks of \(p\) with odd height lies in \(A\), then \(p\) is not a P-position.

public theorem_wanted slowANim_partialStructure (n : ℕ) (A : Finset ℕ)
    (hA : A ⊆ Finset.Icc 1 n) (p : Fin n → ℕ) :
    ((∀ i, Even (p i)) → SpragueGrundy.IsP (slowANimGame n A) p) ∧
      ((Finset.univ.filter fun i => Odd (p i)).card ∈ A →
        ¬ SpragueGrundy.IsP (slowANimGame n A) p)

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Proposition 1.

Uses 2

Statement usesP-positions · Slow\(A\)-Nim

TheoremP-positions of Slow A-Nim with A = {1, k}, k odd#●ready to prove

Let \(k\) be odd with \(1 \le k \le n\) and let \(A = \{1, k\}\). A position \(p = (p_1, \dots, p_n)\) of Slow\(A\)-Nim on \(n\) stacks is a P-position if and only if its total number of tokens \(p_1 + \dots + p_n\) is even.

public theorem_wanted slowANim_one_odd_isP_iff (n k : ℕ) (hA : ({1, k} : Finset ℕ) ⊆ Finset.Icc 1 n)
    (hk : Odd k) (p : Fin n → ℕ) :
    SpragueGrundy.IsP (slowANimGame n {1, k}) p ↔ Even (∑ i, p i)

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Theorem 2.

Uses 2

Statement usesP-positions · Slow\(A\)-Nim

TheoremP-positions of Slow A-Nim with A = {1, n}, n even#●ready to prove

Let \(n \ge 1\) be even and let \(A = \{1, n\}\). A position \(p = (p_1, \dots, p_n)\) of Slow\(A\)-Nim on \(n\) stacks is a P-position if and only if its total number of tokens \(p_1 + \dots + p_n\) and its smallest stack \(\min_i p_i\) are both even.

public theorem_wanted slowANim_one_n_even_isP_iff (n : ℕ) (hn : 0 < n) (hne : Even n)
    (p : Fin n → ℕ) :
    SpragueGrundy.IsP (slowANimGame n {1, n}) p ↔
      Even (∑ i, p i) ∧ ∃ i, (∀ j, p i ≤ p j) ∧ Even (p i)

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Theorem 2.

Uses 2

Statement usesP-positions · Slow\(A\)-Nim

TheoremP-positions of Slow \(\{1,2\}\)-Nim on three stacks#●ready to prove

In Slow \(A\)-Nim with \(A = \{1, 2\}\) on three stacks, let \(p = (p_0, p_1, p_2)\) be a position with \(p_0 \le p_1 \le p_2\). Then \(p\) is a P-position if and only if its three stack heights are all even or all odd.

public theorem_wanted slowANim_one_two_three_isP_iff (p : Fin 3 → ℕ) (hp : Monotone p) :
    SpragueGrundy.IsP (slowANimGame 3 {1, 2}) p ↔ (∀ i, Even (p i)) ∨ ∀ i, Odd (p i)

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Theorem 3.

Uses 2

Statement usesP-positions · Slow\(A\)-Nim

TheoremP-positions of Slow \(\{1,2\}\)-Nim on four stacks#●ready to prove

In Slow \(A\)-Nim with \(A = \{1, 2\}\) on four stacks, let \(p = (p_0, p_1, p_2, p_3)\) be a position with \(p_0 \le p_1 \le p_2 \le p_3\). Then \(p\) is a P-position if and only if either all four stack heights are even, or \(p_0\) is even and \(p_1\), \(p_2\), \(p_3\) are odd.

public theorem_wanted slowANim_one_two_four_isP_iff (p : Fin 4 → ℕ) (hp : Monotone p) :
    SpragueGrundy.IsP (slowANimGame 4 {1, 2}) p ↔
      (∀ i, Even (p i)) ∨ (Even (p 0) ∧ Odd (p 1) ∧ Odd (p 2) ∧ Odd (p 3))

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Theorem 3.

Uses 2

Statement usesP-positions · Slow\(A\)-Nim

TheoremP-positions of Slow A-Nim with A = {1, 2} on five stacks#●ready to prove

Let \(A = \{1, 2\}\) and let \(p = (p_1, \dots, p_5)\) be a position of Slow\(A\)-Nim on five stacks in canonical form, that is, \(p_1 \le p_2 \le \dots \le p_5\). Then \(p\) is a P-position if and only if all five stacks are even, or \(p_1, p_2\) are even and \(p_3, p_4, p_5\) are odd, or \(p_1, p_2, p_5\) are odd and \(p_3, p_4\) are even, or \(p_1, p_2, p_3, p_4\) are odd and \(p_5\) is even.

public theorem_wanted slowANim_one_two_five_isP_iff (p : Fin 5 → ℕ) (hp : Monotone p) :
    SpragueGrundy.IsP (slowANimGame 5 {1, 2}) p ↔
      (∀ i, Even (p i)) ∨
      (Even (p 0) ∧ Even (p 1) ∧ Odd (p 2) ∧ Odd (p 3) ∧ Odd (p 4)) ∨
      (Odd (p 0) ∧ Odd (p 1) ∧ Even (p 2) ∧ Even (p 3) ∧ Odd (p 4)) ∨
      (Odd (p 0) ∧ Odd (p 1) ∧ Odd (p 2) ∧ Odd (p 3) ∧ Even (p 4))

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Theorem 3.

Uses 2

Statement usesP-positions · Slow\(A\)-Nim

TheoremNIRB criterion for reduced positions#●ready to prove

Let \(A \subseteq \{1, \dots, n\}\) be nonempty with least element \(a\), and let \(p\) be a position of Slow \(A\)-Nim on \(n\) stacks. Then \(p\) is reduced if and only if \(a \cdot M \le \sum_i p_i\), where \(M\) is the largest stack height of \(p\) (taken to be \(0\) when \(n = 0\)).

The source assumes \(n \ge 3\); the statement here is made for every \(n\).

public theorem_wanted slowANimReduced_iff_nirb (n : ℕ) (A : Finset ℕ)
    (hA : A ⊆ Finset.Icc 1 n) (hAne : A.Nonempty) (p : Fin n → ℕ) :
    SlowANimReduced A p ↔ A.min' hAne * Finset.univ.sup p ≤ ∑ i, p i

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Theorem 4.

Uses 1

Statement usesReduced positions of Slow \(A\)-Nim

TheoremLegal move sequences depend only on the reduction#●ready to prove

Let \(A \subseteq \{1, \dots, n\}\) and let \(p\) be a position of Slow\(A\)-Nim on \(n\) stacks, with reduction \(r(p)\). A finite sequence of moves, each given by its set of stacks, is legal from \(r(p)\) if and only if it is legal from \(p\).

public theorem_wanted slowANimLegalSeq_reduction_iff (n : ℕ) (A : Finset ℕ)
    (hA : A ⊆ Finset.Icc 1 n) (p : Fin n → ℕ) (ss : List (Finset (Fin n))) :
    SlowANimLegalSeq A (slowANimReduction A p) ss ↔ SlowANimLegalSeq A p ss

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Lemma 1.

Uses 2

Statement usesLegal move sequences in Slow A-Nim · Reduction of a Slow\(A\)-Nim position

TheoremPositions with the same reduction have the same outcome#●ready to prove

Let \(A \subseteq \{1, \dots, n\}\). If two positions \(p\) and \(q\) of Slow\(A\)-Nim \(\mathrm{SN}(n, A)\) have the same reduction, \(r(p) = r(q)\), then \(p\) is a P-position if and only if \(q\) is a P-position.

public theorem_wanted slowANim_isP_iff_of_reduction_eq (n : ℕ) (A : Finset ℕ)
    (hA : A ⊆ Finset.Icc 1 n) (p q : Fin n → ℕ)
    (h : slowANimReduction A p = slowANimReduction A q) :
    SpragueGrundy.IsP (slowANimGame n A) p ↔ SpragueGrundy.IsP (slowANimGame n A) q

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Corollary 1.

Uses 3

Statement usesP-positions · Slow\(A\)-Nim · Reduction of a Slow\(A\)-Nim position

TheoremChopping a reduced position keeps it reduced#●ready to prove

Let \(A \subseteq \{1, \dots, n\}\) and let \(p\) be a reduced position of Slow \(A\)-Nim on \(n\) stacks. Then for every \(m \in \mathbb{N}\) the position \(\mathrm{ctt}(p, m)\) with stack heights \(\mathrm{ctt}(p, m)_i = \min(p_i, m)\) is reduced.

public theorem_wanted slowANimReduced_min (n : ℕ) (A : Finset ℕ) (hA : A ⊆ Finset.Icc 1 n)
    (p : Fin n → ℕ) (hp : SlowANimReduced A p) (m : ℕ) :
    SlowANimReduced A fun i => min (p i) m

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Lemma 2.

Uses 1

Statement usesReduced positions of Slow \(A\)-Nim

TheoremThe reduction chops at the largest reduced height#●ready to prove

Let \(A \subseteq \{1, \dots, n\}\) and let \(p\) be a position of Slow\(A\)-Nim on \(n\) stacks, with largest stack height \(M = \max_i p_i\) (\(M = 0\) when \(n = 0\)). For \(m \in \mathbb{N}\) write \(\mathrm{ctt}(p, m)\) for the position whose stack \(i\) has height \(\min(p_i, m)\). If \(m \le M\), the position \(\mathrm{ctt}(p, m)\) is reduced, and \(\mathrm{ctt}(p, m')\) is not reduced for any \(m'\) with \(m < m' \le M\), then the reduction of \(p\) is \(r(p) = \mathrm{ctt}(p, m)\).

public theorem_wanted slowANimReduction_eq_min (n : ℕ) (A : Finset ℕ) (hA : A ⊆ Finset.Icc 1 n)
    (p : Fin n → ℕ) (m : ℕ) (hm : m ≤ Finset.univ.sup p)
    (hred : SlowANimReduced A fun i => min (p i) m)
    (hmax : ∀ m', m < m' → m' ≤ Finset.univ.sup p → ¬ SlowANimReduced A fun i => min (p i) m') :
    slowANimReduction A p = fun i => min (p i) m

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Lemma 3.

Uses 2

Statement usesReduced positions of Slow \(A\)-Nim · Reduction of a Slow\(A\)-Nim position

TheoremGeneral reduction lemma#●ready to prove

Let \(A \subseteq \{1, \dots, n\}\) be nonempty with least element \(a\), and let \(p\) be a reduced position of Slow\(A\)-Nim \(\mathrm{SN}(n, A)\) with largest stack height \(M\) and total \(\Sigma(p) = \sum_i p_i\). Let \(S\) be a set of \(\ell \in A\) stacks, each holding at least one token, and suppose that the position obtained from \(p\) by removing one token from each stack of \(S\) is not reduced. Then \(a M \le \Sigma(p)\) and, writing \(r = \Sigma(p) - a M\), either (R1) \(\ell > a\), every stack of height \(M\) lies in \(S\), and \(r < \ell - a\); or (R2) some stack of height \(M\) is not in \(S\), and \(r < \ell\).

The hypothesis that \(p\) is reduced is implicit in the source, whose proof uses \(r \ge 0\).

public theorem_wanted slowANim_generalReduction (n : ℕ) (A : Finset ℕ)
    (hA : A ⊆ Finset.Icc 1 n) (hAne : A.Nonempty) (p : Fin n → ℕ) (hp : SlowANimReduced A p)
    (S : Finset (Fin n)) (hS : S.card ∈ A) (hSp : ∀ i ∈ S, 1 ≤ p i)
    (hnot : ¬ SlowANimReduced A (slowANimAfter p S)) :
    (A.min' hAne < S.card ∧ (∀ i, p i = Finset.univ.sup p → i ∈ S) ∧
        A.min' hAne * Finset.univ.sup p ≤ ∑ i, p i ∧
        ∑ i, p i < A.min' hAne * Finset.univ.sup p + (S.card - A.min' hAne)) ∨
      ((∃ i, p i = Finset.univ.sup p ∧ i ∉ S) ∧
        A.min' hAne * Finset.univ.sup p ≤ ∑ i, p i ∧
        ∑ i, p i < A.min' hAne * Finset.univ.sup p + S.card)

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Lemma 4.

Uses 2

Statement usesReduced positions of Slow \(A\)-Nim · Playing on a set of stacks

TheoremP-positions after adding moves#●ready to prove

Let \(M\) and \(E\) be move relations on a type of positions, let \(P\) be a set of P-positions for \(M\), and let \(Q \subseteq P\). Suppose that (1) no element of \(P \setminus Q\) has an \(E\)-move to an element of \(P \setminus Q\), (2) every position outside \(P\) that has an \(M\)-move into \(Q\) has an \(M\)-move or an \(E\)-move into \(P \setminus Q\), and (3) every position of \(Q\) has an \(E\)-move into \(P \setminus Q\). Then \(P \setminus Q\) is a set of P-positions for the move relation "\(M\) or \(E\)".

The relations \(M\) and \(E\) need not be disjoint.

public theorem_wanted isPPositionSet_extend {α : Type*} (M E : α → α → Prop) (P Q : Set α)
    (hP : IsPPositionSet M P) (hQP : Q ⊆ P)
    (h1 : ∀ x y, x ∈ P \ Q → y ∈ P \ Q → ¬ E x y)
    (h2 : ∀ x, x ∉ P → (∃ y ∈ Q, M x y) → ∃ y ∈ P \ Q, M x y ∨ E x y)
    (h3 : ∀ x ∈ Q, ∃ y ∈ P \ Q, E x y) :
    IsPPositionSet (fun x y => M x y ∨ E x y) (P \ Q)

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Proposition 7.

Uses 1

Statement usesSet of P-positions

DefinitionMoves of the playable game graph of Slow \(A\)-Nim#✓fully proved

The playable (reduced) game graph of Slow \(A\)-Nim on \(n\) stacks has the reduced positions as its positions. For reduced positions \(x\) and \(y\), there is a move from \(x\) to \(y\) when \(y\) is the reduction \(r(q)\) of some option \(q\) of \(x\) in Slow \(A\)-Nim, that is, of some position reached from \(x\) by one legal move.

public def SlowANimReducedGraphMove {n : ℕ} (A : Finset ℕ)
    (x y : {p : Fin n → ℕ // SlowANimReduced A p}) : Prop :=
  ∃ q ∈ slowANimMoves A x.1, y.1 = slowANimReduction A q

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Definition 3.

Uses 3 · Used by 4

Statement usesReduced positions of Slow \(A\)-Nim · Options in Slow A-Nim · Reduction of a Slow\(A\)-Nim position

Used byThe empty position is terminal in the playable game graph · P-positions of Slow \(A\)-Nim via the playable game graph · P-positions of the reduced game of Slow \(\{n-1\}\)-Nim · P-positions of the reduced game of Slow \(\{n-1, n\}\)-Nim

TheoremThe empty position is terminal in the playable game graph#✓fully proved

For every \(n\) and every finite set \(A\) of natural numbers, the position of Slow\(A\)-Nim \(\mathrm{SN}(n, A)\) with all \(n\) stacks empty has no move to any position in the playable game graph of \(\mathrm{SN}(n, A)\).

public theorem not_slowANimReducedGraphMove_zero {n : ℕ} (A : Finset ℕ)
    (y : {p : Fin n → ℕ // SlowANimReduced A p}) :
    ¬ SlowANimReducedGraphMove A ⟨fun _ => 0, slowANimReduced_zero A⟩ y

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Definition 3.

Uses 6

Statement usesReduced positions of Slow \(A\)-Nim · Moves of the playable game graph of Slow \(A\)-Nim · The empty position is reduced

Proof usesOptions in Slow A-Nim · The empty position has no options · Reduction of a Slow\(A\)-Nim position

TheoremP-positions of Slow \(A\)-Nim via the playable game graph#●ready to prove

Let \(n \in \mathbb{N}\) and \(A \subseteq \{1, \dots, n\}\). Let \(\tilde P\) be a set of P-positions for the moves of the playable game graph of Slow\(A\)-Nim \(\mathrm{SN}(n, A)\), whose positions are the reduced positions: no position in \(\tilde P\) has a move to a position in \(\tilde P\), and every reduced position outside \(\tilde P\) has a move to a position in \(\tilde P\). Then a position \(p\) of \(\mathrm{SN}(n, A)\) is a P-position if and only if its reduction \(r(p)\) lies in \(\tilde P\).

This combines the source's two statements, one for P-positions and one for N-positions.

public theorem_wanted slowANim_isP_iff_reduction_mem (n : ℕ) (A : Finset ℕ)
    (hA : A ⊆ Finset.Icc 1 n) {P : Set {p : Fin n → ℕ // SlowANimReduced A p}}
    (hP : IsPPositionSet (SlowANimReducedGraphMove A) P) (p : Fin n → ℕ) :
    SpragueGrundy.IsP (slowANimGame n A) p ↔ ∃ q ∈ P, q.1 = slowANimReduction A p

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Theorem 5.

Uses 6

Statement usesSet of P-positions · Reduced positions of Slow \(A\)-Nim · Moves of the playable game graph of Slow \(A\)-Nim · P-positions · Slow\(A\)-Nim · Reduction of a Slow\(A\)-Nim position

TheoremOptions without reduction in Slow {n - 1}-Nim#●ready to prove

Let \(n \ge 2\), \(k = n - 1\) and \(A = \{k\}\), so that a move removes one token from each of exactly \(k\) nonempty stacks. Let \(p\) be a reduced position of Slow\(A\)-Nim on \(n\) stacks, with \(s = (p_1 + \dots + p_n) \bmod 2k\) and \(o\) odd stacks. Let \(p'\) be obtained from \(p\) by playing on a set \(S\) of \(k\) stacks, each holding at least one token in \(p\), and let \(j\) be the stack not in \(S\). If \(p'\) is reduced, then \(s' = (p'_1 + \dots + p'_n) \bmod 2k\) equals \(s + k\) when \(s < k\) and \(s - k\) when \(s \ge k\), and the number \(o'\) of odd stacks of \(p'\) is \(n - o + 1\) if \(p_j\) is odd and \(n - o - 1\) if \(p_j\) is even.

The closing remark of Lemma 5 that both values of \(o'\) are legal when \(0 < o < n\) is omitted: it fails for \(n = 3\) at \(p = (0, 1, 1)\), whose only move omits the empty stack.

public theorem_wanted slowANim_n_sub_one_option_of_reduced (n : ℕ) (hn : 2 ≤ n)
    (p : Fin n → ℕ) (hp : SlowANimReduced {n - 1} p) (S : Finset (Fin n))
    (hS : S.card = n - 1) (hSp : ∀ i ∈ S, 1 ≤ p i)
    (hred : SlowANimReduced {n - 1} (slowANimAfter p S)) (j : Fin n) (hj : j ∉ S) :
    (∑ i, slowANimAfter p S i) % (2 * (n - 1)) =
        (if (∑ i, p i) % (2 * (n - 1)) < n - 1 then (∑ i, p i) % (2 * (n - 1)) + (n - 1)
          else (∑ i, p i) % (2 * (n - 1)) - (n - 1)) ∧
      (Finset.univ.filter fun i => Odd (slowANimAfter p S i)).card =
        if Odd (p j) then n - (Finset.univ.filter fun i => Odd (p i)).card + 1
        else n - (Finset.univ.filter fun i => Odd (p i)).card - 1

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Lemma 5.

Uses 2

Statement usesReduced positions of Slow \(A\)-Nim · Playing on a set of stacks

TheoremOptions with reduction in Slow {n - 1}-Nim#●ready to prove

Let \(n \ge 2\), \(k = n - 1\) and \(A = \{k\}\). Let \(p\) be a reduced position of Slow\(A\)-Nim on \(n\) stacks, with \(s = (p_1 + \dots + p_n) \bmod 2k\), \(o\) odd stacks, and maximum \(M = \max_i p_i\) attained by \(\alpha\) stacks. Let \(p'\) be obtained from \(p\) by playing on a set \(S\) of \(k\) stacks, each holding at least one token in \(p\), and suppose that \(p'\) is not reduced. Write \(r = r(p')\) for its reduction, \(s' = (r_1 + \dots + r_n) \bmod 2k\) and \(o'\) for the number of odd stacks of \(r\). Then \(M\) is even if \(s < k\) and odd if \(s \ge k\). If \(s \not\equiv 0 \pmod k\), then \(r_i = \max(p_i - 1, 0)\) for every stack \(i\), \(o' = n - o\), and \(s' = s + k - 1\) if \(s < k\), \(s' = s - (k + 1)\) if \(s > k\). If \(s \equiv 0 \pmod k\), then \(r_i = \max(p_i - 2, 0)\) for the stacks with \(p_i = M\) and \(r_i = \max(p_i - 1, 0)\) for the others; moreover, if \(s = 0\) then \(\alpha \le \min(n - o, n - 2)\), \(s' = k - 1 - \alpha\) and \(o' = n - o - \alpha\), and if \(s = k\) then \(\alpha \le \min(o, n - 2)\), \(s' = 2k - 1 - \alpha\) and \(o' = n - o + \alpha\).

Stacks are labelled, so the paper's canonical-form display of \(r(p')\) is written stackwise.

MetaMathlibExt.slowANim_n_sub_one_option_of_not_reduced · 18 lines

public theorem_wanted slowANim_n_sub_one_option_of_not_reduced (n : ℕ) (hn : 2 ≤ n)
    (p : Fin n → ℕ) (hp : SlowANimReduced {n - 1} p) (S : Finset (Fin n))
    (hS : S.card = n - 1) (hSp : ∀ i ∈ S, 1 ≤ p i)
    (hred : ¬ SlowANimReduced {n - 1} (slowANimAfter p S)) :
    let k := n - 1
    let s := (∑ i, p i) % (2 * k)
    let o := (Finset.univ.filter fun i => Odd (p i)).card
    let M := Finset.univ.sup p
    let α := (Finset.univ.filter fun i => p i = M).card
    let r := slowANimReduction {n - 1} (slowANimAfter p S)
    let s' := (∑ i, r i) % (2 * k)
    let o' := (Finset.univ.filter fun i => Odd (r i)).card
    (s < k → Even M) ∧ (k ≤ s → Odd M) ∧
      (s % k ≠ 0 → r = (fun i => p i - 1) ∧ o' = n - o ∧
        s' = if s < k then s + k - 1 else s - (k + 1)) ∧
      (s % k = 0 → r = (fun i => if p i = M then p i - 2 else p i - 1) ∧
        (s = 0 → α ≤ n - o ∧ α ≤ n - 2 ∧ s' = k - 1 - α ∧ o' = n - o - α) ∧
        (s = k → α ≤ o ∧ α ≤ n - 2 ∧ s' = 2 * k - 1 - α ∧ o' = n - o + α))

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Lemma 6.

Uses 3

Statement usesReduced positions of Slow \(A\)-Nim · Playing on a set of stacks · Reduction of a Slow\(A\)-Nim position

TheoremP-positions of the reduced game of Slow \(\{n-1\}\)-Nim#●ready to prove

Let \(n \ge 2\) and \(A = \{n - 1\}\), and let \(\tilde P\) be a set of P-positions of the playable game graph of Slow \(A\)-Nim on \(n\) stacks: no move of that graph joins two elements of \(\tilde P\), and every reduced position outside \(\tilde P\) has a move into \(\tilde P\). For a reduced position \(q\), let \(s\) be the remainder of \(\sum_i q_i\) modulo \(2(n - 1)\) and let \(o\) be the number of stacks of \(q\) of odd height. Then \(s\) and \(o\) have the same parity, and \(q \in \tilde P\) if and only if \(s < n - 2\) and \(o \le s\), or \(s = n - 2\) and \(o \equiv n \pmod 2\), or \(n - 2 < s < 2n - 3\) and \(o \le 2(n - 2) - s\).

public theorem_wanted slowANimReduced_mem_pPositions_n_sub_one_iff (n : ℕ) (hn : 2 ≤ n)
    {P : Set {p : Fin n → ℕ // SlowANimReduced {n - 1} p}}
    (hP : IsPPositionSet (SlowANimReducedGraphMove {n - 1}) P)
    (q : {p : Fin n → ℕ // SlowANimReduced {n - 1} p}) :
    let s := (∑ i, q.1 i) % (2 * (n - 1))
    let o := (Finset.univ.filter fun i => Odd (q.1 i)).card
    s % 2 = o % 2 ∧
      (q ∈ P ↔ (s < n - 2 ∧ o ≤ s) ∨ (s = n - 2 ∧ o % 2 = n % 2) ∨
        (n - 2 < s ∧ s < 2 * (n - 1) - 1 ∧ o ≤ 2 * (n - 2) - s))

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Theorem 6.

Uses 3

Statement usesSet of P-positions · Reduced positions of Slow \(A\)-Nim · Moves of the playable game graph of Slow \(A\)-Nim

TheoremP-positions of the reduced game of Slow \(\{n-1, n\}\)-Nim#●ready to prove

Let \(n \ge 2\) and \(A = \{n - 1, n\}\), and let \(\tilde P\) be a set of P-positions of the playable game graph of Slow \(A\)-Nim on \(n\) stacks: no move of that graph joins two elements of \(\tilde P\), and every reduced position outside \(\tilde P\) has a move into \(\tilde P\). For a reduced position \(q\), let \(s\) be the remainder of \(\sum_i q_i\) modulo \(2n - 2\) and let \(o\) be the number of stacks of \(q\) of odd height. Then \(s\) and \(o\) have the same parity, and \(q \in \tilde P\) if and only if \(s < n - 2\) and \(o \le s\), or \(s = n - 2\), \(o \equiv n \pmod 2\) and \(o \ne n\), or \(n - 2 < s < 2n - 3\) and \(o \le 2(n - 2) - s\).

public theorem_wanted slowANimReduced_mem_pPositions_n_sub_one_n_iff (n : ℕ) (hn : 2 ≤ n)
    {P : Set {p : Fin n → ℕ // SlowANimReduced {n - 1, n} p}}
    (hP : IsPPositionSet (SlowANimReducedGraphMove {n - 1, n}) P)
    (q : {p : Fin n → ℕ // SlowANimReduced {n - 1, n} p}) :
    let s := (∑ i, q.1 i) % (2 * n - 2)
    let o := (Finset.univ.filter fun i => Odd (q.1 i)).card
    s % 2 = o % 2 ∧
      (q ∈ P ↔ (s < n - 2 ∧ o ≤ s) ∨ (s = n - 2 ∧ o % 2 = n % 2 ∧ o ≠ n) ∨
        (n - 2 < s ∧ s < 2 * n - 3 ∧ o ≤ 2 * (n - 2) - s))

Sources

• Matthieu Dufour and Silvia Heubach, On the 𝒫-Positions of Some Infinite Families of SlowA-Nim, INTEGERS 26 (2026), Article G3, Theorem 8.

Uses 3

Statement usesSet of P-positions · Reduced positions of Slow \(A\)-Nim · Moves of the playable game graph of Slow \(A\)-Nim

Definition\(m\)-critical positions of exact slow \(k\)-NIM#✓fully proved

Let \(k\) and \(m\) be natural numbers and let \(\mathrm{NIM}(k + 1, k)\) be Slow\(A\)-Nim on \(k + 1\) piles with \(A = \{k\}\): a move chooses a nonempty set of exactly \(k\) nonempty piles and removes one stone from each. Let \(R\) be Smith's remoteness function of this game. A position \(x = (x_0, \dots, x_k)\) is \(m\)-critical when \(R(x) = m\) and \(R(y) \ne m\) for every position \(y < x\), where \(y < x\) means \(y_i \le x_i\) for every \(i\) and \(y \ne x\).

public def IsExactSlowNimCritical (k m : ℕ) (x : Fin (k + 1) → ℕ) : Prop :=
  SpragueGrundy.smithRemoteness (slowANimGame (k + 1) {k}) x = m ∧
    ∀ y : Fin (k + 1) → ℕ, y < x → SpragueGrundy.smithRemoteness (slowANimGame (k + 1) {k}) y ≠ m

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Theorem 1.

Uses 2 · Used by 4

Statement usesSmith's remoteness function · Slow\(A\)-Nim

Used byMoves from critical positions with even parameter (Corollary 1 (i)) · Unique critical-lowering move for odd parameter (Corollary 1 (ii)) · \(m\)-critical positions of exact slow \(k\)-NIM with \(k + 1\) piles (Theorem 1) · The empty position is \(0\)-critical

TheoremThe empty position is \(0\)-critical#✓fully proved

Let \(k\) be a natural number and let \(\mathrm{NIM}(k + 1, k)\) be Slow\(A\)-Nim on \(k + 1\) piles with \(A = \{k\}\), in which a move chooses a nonempty set of exactly \(k\) nonempty piles and removes one stone from each. The position \(x\) of \(\mathrm{NIM}(k + 1, k)\) in which all \(k + 1\) piles are empty is \(0\)-critical: its Smith remoteness is \(0\), and no position \(y\) with \(y_i \le x_i\) for every \(i\) and \(y \ne x\) has remoteness \(0\).

public theorem isExactSlowNimCritical_zero (k : ℕ) :
    IsExactSlowNimCritical k 0 (fun _ => 0)

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Theorem 1.

Uses 5

Statement uses\(m\)-critical positions of exact slow \(k\)-NIM

Proof usesSmith's remoteness function · Smith's remoteness vanishes at terminal positions · Slow\(A\)-Nim · The empty position has no options

DefinitionPile kept by the M-rule#✓fully proved

For a position \(x \in \mathbb{N}^{n+1}\) with piles indexed by \(0, \dots, n\): if some entry of \(x\) is even, the kept pile is the least index \(i\) such that \(x_i\) is even and \(x_i \le x_j\) for every \(j\) with \(x_j\) even; otherwise it is the least index \(i\) such that \(x_j \le x_i\) for every \(j\).

public def exactSlowNimMRuleKept {n : ℕ} (x : Fin (n + 1) → ℕ) : Fin (n + 1) :=
  let piles := List.finRange (n + 1)
  if piles.any fun i => decide (Even (x i)) then
    (piles.find? fun i => decide (Even (x i) ∧ ∀ j, Even (x j) → x i ≤ x j)).getD 0
  else
    (piles.find? fun i => decide (∀ j, x j ≤ x i)).getD 0

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Section 2 (the index e(x)). Such a pile always exists, so the default 0 of getD is never used.

Used by 1

Used byThe M-move

DefinitionThe M-move#✓fully proved

For a position \(x\) on \(n + 1\) piles, the M-move keeps one pile, chosen by the M-rule as the first pile holding the smallest even entry if some entry of \(x\) is even, and otherwise the first pile holding a largest entry. It removes one stone from every other pile, where an empty pile stays empty.

public def exactSlowNimMRuleMove {n : ℕ} (x : Fin (n + 1) → ℕ) : Fin (n + 1) → ℕ :=
  slowANimAfter x (Finset.univ.erase (exactSlowNimMRuleKept x))

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Sections 1.2 and 2 (the M-rule).

Uses 2 · Used by 5

Statement usesPile kept by the M-rule · Playing on a set of stacks

Used byMoves at a position supported by an (A1) basic vector (Lemma 3) · Moves from critical positions with even parameter (Corollary 1 (i)) · Unique critical-lowering move for odd parameter (Corollary 1 (ii)) · Fuel-bounded length of M-rule play · Successor step of the truncated M-rule length

TheoremTerminal positions of exact slow \(k\)-NIM#✓fully proved

Let \(n\) and \(k\) be natural numbers and let \(x = (x_0, \dots, x_{n-1})\) be a position of Slow\(A\)-Nim on \(n\) piles with \(A = \{k\}\). Then \(x\) has no options if and only if \(k = 0\) or fewer than \(k\) of the piles are nonempty.

When \(k = 0\) there is no move, since a move uses a nonempty set of exactly \(k\) piles.

public theorem slowANimMoves_singleton_eq_empty_iff {n k : ℕ} (x : Fin n → ℕ) :
    slowANimMoves {k} x = ∅ ↔ k = 0 ∨ (Finset.univ.filter fun i => 0 < x i).card < k

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Section 1.1 (the moves of NIM(n, k)).

Uses 2 · Used by 1

Statement usesOptions in Slow A-Nim

Proof usesPlaying on a set of stacks

Used bySuccessor step of the truncated M-rule length

DefinitionFuel-bounded length of M-rule play#✓fully proved

Let \(k\) and \(f\) be natural numbers and let \(x\) be a position on \(k + 1\) piles. Call \(x\) terminal when \(k = 0\) or fewer than \(k\) of its piles are nonempty. The value at \(f\) and \(x\) is \(0\) when \(f = 0\) or \(x\) is terminal; otherwise it is \(1\) plus the value at \(f - 1\) and the position reached from \(x\) by the M-move. Thus it counts the M-moves played from \(x\), stopping at a terminal position or after \(f\) moves.

public def exactSlowNimMRuleLengthAux (k : ℕ) : ℕ → (Fin (k + 1) → ℕ) → ℕ
  | 0, _ => 0
  | f + 1, x =>
    if k = 0 ∨ (Finset.univ.filter fun i => 0 < x i).card < k then 0
    else 1 + exactSlowNimMRuleLengthAux k f (exactSlowNimMRuleMove x)

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Section 1.2 (the function M).

Uses 1 · Used by 2

Statement usesThe M-move

Used byM-rule length · Successor step of the truncated M-rule length

TheoremSuccessor step of the truncated M-rule length#✓fully proved

Let \(k, f \in \mathbb{N}\) and \(x \in \mathbb{N}^{k+1}\), and write \(M_f(x)\) for the number of M-rule steps from \(x\) in Slow\(\{k\}\)-Nim on \(k + 1\) stacks, counted for at most \(f\) steps. Then \(M_{f+1}(x) = 0\) if \(x\) has no options, and otherwise \(M_{f+1}(x) = 1 + M_f(x')\), where \(x'\) is the position obtained from \(x\) by the M-move.

public theorem exactSlowNimMRuleLengthAux_succ (k f : ℕ) (x : Fin (k + 1) → ℕ) :
    exactSlowNimMRuleLengthAux k (f + 1) x =
      if slowANimMoves {k} x = ∅ then 0
      else 1 + exactSlowNimMRuleLengthAux k f (exactSlowNimMRuleMove x)

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Section 1.2 (the function M).

Uses 4

Statement usesFuel-bounded length of M-rule play · The M-move · Options in Slow A-Nim

Proof usesTerminal positions of exact slow \(k\)-NIM

DefinitionM-rule length#✓fully proved

Let \(k\) be a natural number and let \(x = (x_0, \dots, x_k)\) be a position on \(k + 1\) piles. Then \(M(x)\) is the number of M-moves played from \(x\) until a terminal position (one with \(k = 0\) or fewer than \(k\) nonempty piles) is reached, computed as the fuel-bounded length of M-rule play with fuel \(x_0 + \dots + x_k\).

For \(0 < k\) every M-move from a nonterminal position removes \(k\) stones, so this much fuel suffices and \(M(x)\) is the full length of the M-rule play from \(x\).

public def exactSlowNimMRuleLength (k : ℕ) (x : Fin (k + 1) → ℕ) : ℕ :=
  exactSlowNimMRuleLengthAux k (∑ i, x i) x

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Section 1.2 (the function M).

Uses 1 · Used by 3

Statement usesFuel-bounded length of M-rule play

Used byTheorem 2 (the M-rule realizes Smith's remoteness) · M-rule length of the position (3, 5, 5) · M-rule length of the position (3, 3, 3)

TheoremM-rule length of the position (3, 3, 3)#✓fully proved

In exact slow \(2\)-NIM on three piles, \(\mathrm{NIM}(3, 2)\), where a move removes one stone from each of exactly two nonempty piles, the M-rule length of the position \((3, 3, 3)\) is \(M(3, 3, 3) = 4\).

public theorem exactSlowNimMRuleLength_three_three_three :
    exactSlowNimMRuleLength 2 ![3, 3, 3] = 4

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Section 1.6 (example after Theorem 1).

Uses 1

Statement usesM-rule length

TheoremM-rule length of the position (3, 5, 5)#✓fully proved

In exact slow \(2\)-NIM on three piles, \(\mathrm{NIM}(3, 2)\), where a move removes one stone from each of exactly two nonempty piles, the M-rule length of the position \((3, 5, 5)\) is \(M(3, 5, 5) = 6\).

public theorem exactSlowNimMRuleLength_three_five_five :
    exactSlowNimMRuleLength 2 ![3, 5, 5] = 6

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Section 1.6 (example after Theorem 1).

Uses 1

Statement usesM-rule length

DefinitionBasic vectors of type (A0)#✓fully proved

Let \(k\) and \(b\) be natural numbers. A vector \(z = (z_0, \dots, z_k)\) of \(k + 1\) natural numbers is basic of type (A0) for \(b\) when \(z_0 + \dots + z_k = kb\), \(z_i \le b\) for every \(i\), \(b\) is even, and every \(z_i\) is even.

public def IsExactSlowNimBasicA0 (k b : ℕ) (z : Fin (k + 1) → ℕ) : Prop :=
  ∑ i, z i = k * b ∧ (∀ i, z i ≤ b) ∧ Even b ∧ ∀ i, Even (z i)

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Section 2 (basic vectors).

Used by 3

Used byBasic-vector value · Moves at a position supported by an (A0) basic vector (Lemma 2) · The basic value is attained

DefinitionBasic vectors of type (A1)#✓fully proved

Let \(k\) and \(b\) be natural numbers. A vector \(z = (z_0, \dots, z_k)\) of \(k + 1\) natural numbers is basic of type (A1) for \(b\) when \(z_0 + \dots + z_k = kb\), \(z_i \le b\) for every \(i\), \(b\) is odd, and exactly one \(z_i\) is even.

public def IsExactSlowNimBasicA1 (k b : ℕ) (z : Fin (k + 1) → ℕ) : Prop :=
  ∑ i, z i = k * b ∧ (∀ i, z i ≤ b) ∧ Odd b ∧ ∃! i, Even (z i)

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Section 2 (basic vectors).

Used by 3

Used byBasic-vector value · Moves at a position supported by an (A1) basic vector (Lemma 3) · The basic value is attained

DefinitionBasic vectors of type (B)#✓fully proved

Let \(k\) and \(b\) be natural numbers. A vector \(z = (z_0, \dots, z_k)\) of \(k + 1\) natural numbers is basic of type (B) for \(b\) when \(z_0 + \dots + z_k = kb + k - 1\), \(z_i < b\) for every \(i\), \(b\) is even, and every \(z_i\) is odd. Here \(kb + k - 1\) is computed in the natural numbers, so it is \(0\) when \(k = 0\).

public def IsExactSlowNimBasicB (k b : ℕ) (z : Fin (k + 1) → ℕ) : Prop :=
  ∑ i, z i = k * b + k - 1 ∧ (∀ i, z i < b) ∧ Even b ∧ ∀ i, Odd (z i)

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Section 2 (basic vectors).

Used by 3

Used byBasic-vector value · Positions supported by a (B) basic vector (Lemma 1) · The basic value is attained

DefinitionBasic-vector value#✓fully proved

For \(k \in \mathbb{N}\) and \(x \in \mathbb{N}^{k+1}\), the basic-vector value \(B(x)\) is the largest \(b \le \sum_i x_i\) for which some \(z \le x\) (componentwise) is a basic vector of type (A0), (A1) or (B) with parameter \(b\); such a \(b\) exists, since \(z = 0\) is basic of type (A0) with parameter \(0\). For \(k \ge 1\) the bound is automatic, because every basic \(z \le x\) with parameter \(b\) has \(b \le k b \le \sum_i z_i \le \sum_i x_i\), so \(B(x)\) is the largest parameter of a basic vector \(z \le x\).

For \(k = 0\) that maximum does not exist (\(z = 0\) is basic of type (A0) for every even \(b\)), and the bound \(b \le \sum_i x_i\) totalizes this degenerate case.

public noncomputable def exactSlowNimBasicValue (k : ℕ) (x : Fin (k + 1) → ℕ) : ℕ :=
  open Classical in
  Nat.findGreatest (fun b => ∃ z ≤ x, IsExactSlowNimBasicA0 k b z ∨
    IsExactSlowNimBasicA1 k b z ∨ IsExactSlowNimBasicB k b z) (∑ i, x i)

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Section 2, equation (1).

Uses 3 · Used by 5

Statement usesBasic vectors of type (A0) · Basic vectors of type (A1) · Basic vectors of type (B)

Used byBasic-vector value equals Smith's remoteness (Lemma 4) · Positions supported by a (B) basic vector (Lemma 1) · Moves at a position supported by an (A0) basic vector (Lemma 2) · Moves at a position supported by an (A1) basic vector (Lemma 3) · The basic value is attained

TheoremThe basic value is attained#✓fully proved

Let \(k\) be a natural number, let \(x\) be a position on \(k + 1\) piles, and let \(b = B(x)\) be its basic value. Then some \(z \le x\) (componentwise) is a basic vector of type (A0), (A1) or (B) with parameter \(b\), that is, \(z\) supports \(x\). Here type (A0) means \(\sum_i z_i = kb\), \(z_i \le b\) for all \(i\), and \(b\) and every \(z_i\) are even; type (A1) means \(\sum_i z_i = kb\), \(z_i \le b\) for all \(i\), \(b\) is odd and exactly one \(z_i\) is even; and type (B) means \(\sum_i z_i = kb + k - 1\) (truncated subtraction), \(z_i < b\) for all \(i\), \(b\) is even and every \(z_i\) is odd.

public theorem exists_supports_exactSlowNimBasicValue (k : ℕ) (x : Fin (k + 1) → ℕ) :
    ∃ z ≤ x, IsExactSlowNimBasicA0 k (exactSlowNimBasicValue k x) z ∨
      IsExactSlowNimBasicA1 k (exactSlowNimBasicValue k x) z ∨
      IsExactSlowNimBasicB k (exactSlowNimBasicValue k x) z

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Section 2, equation (1).

Uses 4

Statement usesBasic vectors of type (A0) · Basic vectors of type (A1) · Basic vectors of type (B) · Basic-vector value

Theorem\(m\)-critical positions of exact slow \(k\)-NIM with \(k + 1\) piles (Theorem 1)#●ready to prove

Let \(k \ge 1\) and \(m\) be natural numbers, and let \(x = (x_0, \dots, x_k)\) be a position of \(\mathrm{NIM}(k + 1, k)\), the game on \(k + 1\) piles in which a move removes one stone from each of exactly \(k\) nonempty piles. Call \(x\) \(m\)-critical when its Smith remoteness is \(m\) and no position \(y < x\) (that is, \(y_i \le x_i\) for every \(i\) and \(y \ne x\)) has remoteness \(m\). Then \(x\) is \(m\)-critical if and only if either (A) \(x_0 + \dots + x_k = km\), \(x_i \le m\) for every \(i\), every \(x_i\) is even if \(m\) is even, and exactly one \(x_i\) is even if \(m\) is odd; or (B) \(x_0 + \dots + x_k = km + k - 1\), \(x_i < m\) for every \(i\), \(m\) is even, and every \(x_i\) is odd.

public theorem_wanted isExactSlowNimCritical_iff {k : ℕ} (hk : 0 < k) (m : ℕ)
    (x : Fin (k + 1) → ℕ) :
    IsExactSlowNimCritical k m x ↔
      (∑ i, x i = k * m ∧ (∀ i, x i ≤ m) ∧ (Even m → ∀ i, Even (x i)) ∧
          (Odd m → ∃! i, Even (x i))) ∨
        (∑ i, x i = k * m + k - 1 ∧ (∀ i, x i < m) ∧ Even m ∧ ∀ i, Odd (x i))

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Theorem 1.

Uses 1

Statement uses\(m\)-critical positions of exact slow \(k\)-NIM

TheoremMoves from critical positions with even parameter (Corollary 1 (i))#●ready to prove

Let \(k \ge 1\), let \(m > 0\) be even, and let \(x \in \mathbb{N}^{k+1}\) be an \(m\)-critical position of Slow\(\{k\}\)-Nim on \(k + 1\) stacks. Then the entries of \(x\) are either all odd or all even. If they are all even, then some entry satisfies \(x_i < m\); every option \(y\) of \(x\) with \(y_i < x_i\) for every \(i\) such that \(x_i = m\) is \((m - 1)\)-critical; and the position \(x'\) obtained from \(x\) by the M-move satisfies \(x'_i < x_i\) for every \(i\) with \(x_i = m\) and is \((m - 1)\)-critical.

The hypothesis \(m > 0\) and the restriction of the move claims to all-even \(x\) are deviations from the source.

public theorem_wanted exactSlowNim_critical_of_even {k m : ℕ} (hk : 0 < k) (hm0 : 0 < m)
    (hm : Even m) (x : Fin (k + 1) → ℕ) (hx : IsExactSlowNimCritical k m x) :
    ((∀ i, Odd (x i)) ∨ (∀ i, Even (x i))) ∧
      ((∀ i, Even (x i)) →
        (∃ i, x i < m) ∧
          (∀ y ∈ slowANimMoves {k} x, (∀ i, x i = m → y i < x i) →
            IsExactSlowNimCritical k (m - 1) y) ∧
          (∀ i, x i = m → exactSlowNimMRuleMove x i < x i) ∧
          IsExactSlowNimCritical k (m - 1) (exactSlowNimMRuleMove x))

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Corollary 1 (i).

Uses 3

Statement uses\(m\)-critical positions of exact slow \(k\)-NIM · The M-move · Options in Slow A-Nim

TheoremUnique critical-lowering move for odd parameter (Corollary 1 (ii))#●ready to prove

Let \(k \ge 2\), let \(m\) be odd, and let \(x \in \mathbb{N}^{k+1}\) be an \(m\)-critical position of Slow\(\{k\}\)-Nim on \(k + 1\) stacks. Then \(x\) has exactly one even entry \(x_i\). The position \(x'\) obtained from \(x\) by removing one token from every pile other than \(i\) is an option of \(x\), it is the only option of \(x\) that is \((m - 1)\)-critical, and it is the position reached from \(x\) by the M-move.

public theorem_wanted exactSlowNim_critical_of_odd {k m : ℕ} (hk : 2 ≤ k) (hm : Odd m)
    (x : Fin (k + 1) → ℕ) (hx : IsExactSlowNimCritical k m x) :
    ∃ i, Even (x i) ∧ (∀ j, Even (x j) → j = i) ∧
      slowANimAfter x (Finset.univ.erase i) ∈ slowANimMoves {k} x ∧
      (∀ y ∈ slowANimMoves {k} x,
        IsExactSlowNimCritical k (m - 1) y ↔ y = slowANimAfter x (Finset.univ.erase i)) ∧
      exactSlowNimMRuleMove x = slowANimAfter x (Finset.univ.erase i)

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Corollary 1 (ii).

Uses 4

Statement uses\(m\)-critical positions of exact slow \(k\)-NIM · The M-move · Playing on a set of stacks · Options in Slow A-Nim

TheoremProposition 1 (odd P-positions of exact slow k-NIM)#●ready to prove

Let \(0 < k\) and let \(\mathrm{NIM}(k + 1, k)\) be Slow\(A\)-Nim on \(k + 1\) stacks with \(A = \{k\}\). A position \(x = (x_0, \dots, x_k)\) of \(\mathrm{NIM}(k + 1, k)\) all of whose entries are odd is a P-position if and only if there is a natural number \(m\) such that \(x_0 + \dots + x_k = km + k - 1\), \(x_i < m\) for every \(i\), and \(m\) is even.

public theorem_wanted exactSlowNim_odd_isP_iff {k : ℕ} (hk : 0 < k) (x : Fin (k + 1) → ℕ)
    (hx : ∀ i, Odd (x i)) :
    SpragueGrundy.IsP (slowANimGame (k + 1) {k}) x ↔
      ∃ m, ∑ i, x i = k * m + k - 1 ∧ (∀ i, x i < m) ∧ Even m

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Proposition 1.

Uses 2

Statement usesP-positions · Slow\(A\)-Nim

TheoremTheorem 2 (the M-rule realizes Smith's remoteness)#●ready to prove

Let \(0 < k\) and let \(\mathrm{NIM}(k + 1, k)\) be exact slow \(k\)-NIM on \(k + 1\) piles, that is, Slow\(A\)-Nim on \(k + 1\) stacks with \(A = \{k\}\), where a move removes one stone from each of exactly \(k\) nonempty piles. For every position \(x\) of \(\mathrm{NIM}(k + 1, k)\), the M-rule length \(M(x)\) equals Smith's remoteness \(R(x)\) of \(x\) in \(\mathrm{NIM}(k + 1, k)\).

public theorem_wanted exactSlowNimMRuleLength_eq_smithRemoteness {k : ℕ} (hk : 0 < k)
    (x : Fin (k + 1) → ℕ) :
    exactSlowNimMRuleLength k x = SpragueGrundy.smithRemoteness (slowANimGame (k + 1) {k}) x

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Theorem 2.

Uses 3

Statement usesSmith's remoteness function · M-rule length · Slow\(A\)-Nim

TheoremPositions supported by a (B) basic vector (Lemma 1)#●ready to prove

Let \(k \ge 1\), let \(B\) be the basic-vector value on \(\mathbb{N}^{k+1}\), and let \(x, z \in \mathbb{N}^{k+1}\) with \(z \le x\) componentwise, where \(z\) is a basic vector of type (B) with parameter \(B(x)\). Then \(x = z\), and every option \(x'\) of \(x\) in Slow\(\{k\}\)-Nim on \(k + 1\) stacks (a move removes one token from each of exactly \(k\) nonempty stacks) satisfies \(B(x') = B(x) - 1\), where subtraction is truncated at \(0\).

public theorem_wanted exactSlowNimBasicValue_of_supports_basicB {k : ℕ} (hk : 0 < k)
    (x z : Fin (k + 1) → ℕ) (hzx : z ≤ x)
    (hz : IsExactSlowNimBasicB k (exactSlowNimBasicValue k x) z) :
    x = z ∧ ∀ x' ∈ slowANimMoves {k} x,
      exactSlowNimBasicValue k x' = exactSlowNimBasicValue k x - 1

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Lemma 1.

Uses 3

Statement usesBasic vectors of type (B) · Basic-vector value · Options in Slow A-Nim

TheoremMoves at a position supported by an (A0) basic vector (Lemma 2)#●ready to prove

Let \(k \ge 1\), let \(B\) be the basic-vector value on \(\mathbb{N}^{k+1}\), and let \(x, z \in \mathbb{N}^{k+1}\) with \(z \le x\) componentwise, where \(z\) is a basic vector of type (A0) with parameter \(B(x)\). Let \(j\) be a pile with \(x_i > 0\) for every \(i \ne j\), and let \(x'\) be obtained from \(x\) by removing one token from every pile other than \(j\). Then \(B(x') \le B(x) - 1\) and \(B(x')\) is odd. Moreover, if \(z_j < B(x)\), or if \(z_j = B(x)\) and \(z_i < \min(B(x), x_i)\) for some \(i\), then \(B(x') = B(x) - 1\). Here \(B(x) - 1\) is truncated subtraction in \(\mathbb{N}\).

public theorem_wanted exactSlowNimBasicValue_of_supports_basicA0 {k : ℕ} (hk : 0 < k)
    (x z : Fin (k + 1) → ℕ) (hzx : z ≤ x)
    (hz : IsExactSlowNimBasicA0 k (exactSlowNimBasicValue k x) z) (j : Fin (k + 1))
    (hj : ∀ i, i ≠ j → 0 < x i) :
    exactSlowNimBasicValue k (slowANimAfter x (Finset.univ.erase j)) ≤
        exactSlowNimBasicValue k x - 1 ∧
      Odd (exactSlowNimBasicValue k (slowANimAfter x (Finset.univ.erase j))) ∧
      (z j < exactSlowNimBasicValue k x ∨
          (z j = exactSlowNimBasicValue k x ∧
            ∃ i, z i < min (exactSlowNimBasicValue k x) (x i)) →
        exactSlowNimBasicValue k (slowANimAfter x (Finset.univ.erase j)) =
          exactSlowNimBasicValue k x - 1)

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Lemma 2.

Uses 3

Statement usesBasic vectors of type (A0) · Basic-vector value · Playing on a set of stacks

TheoremMoves at a position supported by an (A1) basic vector (Lemma 3)#●ready to prove

Let \(k \ge 1\), let \(B\) be the basic-vector value on \(\mathbb{N}^{k+1}\), and let \(x, z \in \mathbb{N}^{k+1}\) with \(z \le x\) componentwise, where \(z\) is a basic vector of type (A1) with parameter \(B(x)\). Then every option \(x'\) of \(x\) in Slow\(\{k\}\)-Nim on \(k + 1\) stacks (a move removes one token from each of exactly \(k\) nonempty stacks) satisfies \(B(x') \ge B(x) - 2\), and the position \(x''\) obtained from \(x\) by the M-move satisfies \(B(x'') = B(x) - 1\), where subtraction is truncated at \(0\).

public theorem_wanted exactSlowNimBasicValue_of_supports_basicA1 {k : ℕ} (hk : 0 < k)
    (x z : Fin (k + 1) → ℕ) (hzx : z ≤ x)
    (hz : IsExactSlowNimBasicA1 k (exactSlowNimBasicValue k x) z) :
    (∀ x' ∈ slowANimMoves {k} x, exactSlowNimBasicValue k x - 2 ≤ exactSlowNimBasicValue k x') ∧
      exactSlowNimBasicValue k (exactSlowNimMRuleMove x) = exactSlowNimBasicValue k x - 1

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Lemma 3.

Uses 4

Statement usesBasic vectors of type (A1) · Basic-vector value · The M-move · Options in Slow A-Nim

TheoremBasic-vector value equals Smith's remoteness (Lemma 4)#●ready to prove

Let \(k \ge 1\) and consider Slow\(\{k\}\)-Nim on \(k + 1\) stacks, in which a move removes one token from each of exactly \(k\) nonempty stacks. For every position \(x \in \mathbb{N}^{k+1}\), the basic-vector value \(B(x)\) equals Smith's remoteness of \(x\) in this game.

public theorem_wanted exactSlowNimBasicValue_eq_smithRemoteness {k : ℕ} (hk : 0 < k)
    (x : Fin (k + 1) → ℕ) :
    exactSlowNimBasicValue k x = SpragueGrundy.smithRemoteness (slowANimGame (k + 1) {k}) x

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Lemma 4.

Uses 3

Statement usesSmith's remoteness function · Basic-vector value · Slow\(A\)-Nim

DefinitionBinary encoding of natural numbers#✓fully proved

The bitstring encoding of \(\mathbb{N}\) that writes \(0\) as the empty string and a positive integer \(n\) as its binary digits, least significant bit first, together with Mathlib's decoding map, which recovers \(n\) from its encoding. It is a definition, not an instance; Theorem 3 installs it locally so that lists of piles are encoded as self-delimiting binary blocks.

@[instance_reducible]
public def exactSlowNimBinaryNatEncoding : BitstringEncoding ℕ where
  toEncoding := Computability.encodingNatBool

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Theorem 3 ("integers are presented in binary").

Uses 1 · Used by 1

Statement usesBitstring encodings

Used byTheorem 3 (Smith's remoteness of exact slow k-NIM is polynomial-time computable)

DefinitionRemoteness of exact slow k-NIM from a list of piles#✓fully proved

For a list \((x_0, \dots, x_{n-1})\) of natural numbers of length \(n\), the value is Smith's remoteness of the position \((x_0, \dots, x_{n-1})\) of Slow\(A\)-Nim on \(n\) stacks with \(A = \{n - 1\}\), where \(0 - 1 = 0\). For \(n = k + 1\) this game is exact slow \(k\)-NIM \(\mathrm{NIM}(k + 1, k)\), so \(k\) is part of the input; the empty list gives the game on no stacks.

public noncomputable def exactSlowNimRemotenessOfList (l : List ℕ) : ℕ :=
  SpragueGrundy.smithRemoteness (slowANimGame l.length {l.length - 1}) fun i => l.get i

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Theorem 3.

Uses 2 · Used by 1

Statement usesSmith's remoteness function · Slow\(A\)-Nim

Used byTheorem 3 (Smith's remoteness of exact slow k-NIM is polynomial-time computable)

TheoremTheorem 3 (Smith's remoteness of exact slow k-NIM is polynomial-time computable)#●ready to prove

The map sending a list \((x_0, \dots, x_{n-1})\) of natural numbers of length \(n\) to Smith's remoteness of the position \((x_0, \dots, x_{n-1})\) of Slow\(A\)-Nim on \(n\) stacks with \(A = \{n - 1\}\) (where \(0 - 1 = 0\)) is polynomial-time computable. Here natural numbers, in the input and the output, are encoded in binary, and a list is encoded as the concatenation of the self-delimiting forms of the encodings of its entries. For \(n = k + 1\) this is the game \(\mathrm{NIM}(k + 1, k)\), so \(k\) is part of the input.

public theorem_wanted exactSlowNimRemoteness_isPolyTime :
    letI : BitstringEncoding ℕ := exactSlowNimBinaryNatEncoding
    ComplexityTheory.IsPolyTime exactSlowNimRemotenessOfList

Sources

• Vladimir Gurvich, Denis Martynov, Vladislav Maximchuk, and Michael Vyalyi, On Remoteness Functions of Exact Slow k-NIM with k+1 Piles, INTEGERS 24 (2024), Article G1, Theorem 3.

Uses 11

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Polynomial-time computable functions · Binary encoding of natural numbers · Remoteness of exact slow k-NIM from a list of piles

33 fully proved28 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.