English
Let G be an impartial P-Game. Then the Grundy value of G equals the least nimber not attained by any right move, i.e. the mex of the Grundy values of its right options.
Русский
Пусть G — непредвзятая игра в рамках PGame. Тогда значение Гранди для G равно наименьшему не входящему в множество значений Гранди среди правых ходов; т.е. значение Гранди равно mex множества { Grundy(G.moveRight i) } для i ∈ G.RightMoves.
LaTeX
$$$\\\\operatorname{grundyValue}(G) = \\\\operatorname{mex}\\\\{ \\\\operatorname{grundyValue}(G.moveRight(i)) \\\\mid i \\\\in G.\\\\text{RightMoves} \\\\$ \\\\}$$$
Lean4
theorem grundyValue_eq_sInf_moveRight (G : PGame) [G.Impartial] :
grundyValue G = sInf (Set.range (grundyValue ∘ G.moveRight))ᶜ :=
by
obtain ⟨l, r, L, R⟩ := G
rw [← grundyValue_neg, grundyValue_eq_sInf_moveLeft]
iterate 3 apply congr_arg
ext i
exact @grundyValue_neg _ (@Impartial.moveRight_impartial ⟨l, r, L, R⟩ _ _)
