English
For any right move i of an impartial P-Game G, the Grundy value of the resulting game G.moveRight i is different from the Grundy value of G.
Русский
Для любого правого хода i в непредвзятой игре G значение Гранди получившейся игры G.moveRight i отличается от значения Гранди самой G.
LaTeX
$$$\\\\forall i: G.\\\\RightMoves, \\\\operatorname{grundyValue}(G.moveRight(i)) \\\\neq \\\\operatorname{grundyValue}(G).$$$$
Lean4
theorem grundyValue_ne_moveRight {G : PGame} [G.Impartial] (i : G.RightMoves) :
grundyValue (G.moveRight i) ≠ grundyValue G := by
convert grundyValue_ne_moveLeft (toLeftMovesNeg i) using 1 <;> simp