English
The Grundy value of the sum of two Nim games equals the nimber addition of their nimber values.
Русский
Значение Гранди суммы двух игр Nim равно nimber-сложению их nimber-значений.
LaTeX
$$$\\\\operatorname{grundyValue}(\\\\text{nim } x + \\\\text{nim } y) = \\\\ast x + \\\\ast y.$$$
Lean4
/-- The Grundy value of the sum of two nim games equals their nimber addition. -/
theorem grundyValue_nim_add_nim (x y : Ordinal) : grundyValue (nim x + nim y) = ∗x + ∗y :=
by
apply (grundyValue_le_of_forall_moveLeft _).antisymm (le_grundyValue_of_Iio_subset_moveLeft _)
· intro i
apply leftMoves_add_cases i <;> intro j <;> have := (toLeftMovesNim_symm_lt j).ne
· simpa [grundyValue_nim_add_nim (toLeftMovesNim.symm j) y]
· simpa [grundyValue_nim_add_nim x (toLeftMovesNim.symm j)]
· intro k hk
obtain h | h := Nimber.lt_add_cases hk
· let a := toOrdinal (k + ∗y)
use toLeftMovesAdd (Sum.inl (toLeftMovesNim ⟨a, h⟩))
simp [a, grundyValue_nim_add_nim a y]
· let a := toOrdinal (k + ∗x)
use toLeftMovesAdd (Sum.inr (toLeftMovesNim ⟨a, h⟩))
simp [a, grundyValue_nim_add_nim x a, add_comm (∗x)]
termination_by (x, y)
