nim_one_moveRight — Mathlib

English

For Nim with value 1, every right move yields Nim 0; i.e., all right options of Nim(1) are Nim(0).

Русский

Для Nim со значением 1 каждый правый ход приводит к Nim 0; то есть все правые варианты Nim(1) равны Nim(0).

LaTeX

$$$ \forall i \in \text{RightMoves}(\mathrm{nim}(1)),\quad (\mathrm{nim}(1)).moveRight(i) = \mathrm{nim}(0). $$$

Lean4

theorem nim_one_moveRight (x) : (nim 1).moveRight x = nim 0 := by simp

Похожие утверждения