Misere combinatorial games.

@[simp]

theorem MisereGames.GameForm.birthday_eq_zero {x : GameForm} : Form.birthday x = 0 ↔ x = 0

noncomputable def MisereGames.GameForm.birthdayFinset : ℕ → Finset GameForm

The finite set of game forms born by day n.

Equations

• One or more equations did not get rendered due to their size.
• MisereGames.GameForm.birthdayFinset 0 = {0}

theorem MisereGames.GameForm.mem_birthdayFinset_succ {x : GameForm} {n : ℕ} : x ∈ birthdayFinset (n + 1) ↔ ∃ (l : Finset GameForm) (r : Finset GameForm), (l ⊆ birthdayFinset n ∧ r ⊆ birthdayFinset n) ∧ !{↑l | ↑r} = x

@[simp]

theorem MisereGames.GameForm.birthdayFinset_zero : birthdayFinset 0 = {0}

@[simp]

theorem MisereGames.GameForm.mem_birthdayFinset {x : GameForm} {n : ℕ} : x ∈ birthdayFinset n ↔ Form.birthday x ≤ ↑n