Misere combinatorial games.

def MisereGames.Form.Maintenance {G : Type (u + 1)} [Form G] (A : G → Prop) (g h : G) (p : Player) : Prop

The maintenance condition for comparison modulo A.

Equations

• One or more equations did not get rendered due to their size.

theorem MisereGames.Form.Maintenance.neg_iff {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderNeg A] {g h : G} (p : Player) : Maintenance A (-h) (-g) (-p) ↔ Maintenance A g h p

def MisereGames.Form.Strong {G : Type (u + 1)} [Form G] (A : G → Prop) (g : G) (p : Player) : Prop

The strong outcome condition for a form against ends in A.

Equations

• MisereGames.Form.Strong A g p = ∀ (x : G), A x → MisereGames.Form.IsEndLike p x → MisereGames.Form.Misere.Outcome.WinsGoingFirst p (g + x)

theorem MisereGames.Form.strong_of_isEnd {A : GameForm → Prop} {p : Player} {g : GameForm} (he : IsEnd p g) : Strong A g p

theorem MisereGames.Form.Strong.neg_iff {A : GameForm → Prop} [ClosedUnderNeg A] {p : Player} {g : GameForm} : Strong A (-g) p ↔ Strong A g (-p)

@[irreducible]

def MisereGames.Form.IsStrongTest (p : Player) (g : GameForm) : Prop

This is the test given by [Davies, Milley (Theorem 3.1 on p. 7)][davies:OrderInversesMonoid:2026].

Equations

• One or more equations did not get rendered due to their size.

theorem MisereGames.Form.isStrongTest_def (p : Player) (g : GameForm) : IsStrongTest p g ↔ IsEnd p g ∨ ∃ (gl : GameForm) (_ : gl ∈ moves p g), Misere.Outcome.MisereOutcome gl = Outcome.ofPlayer p ∧ IsStrongTest p gl ∧ ∀ glr ∈ moves (-p) gl, IsStrongTest p glr

theorem MisereGames.Form.IsStrongTest.neg_iff {p : Player} {g : GameForm} : IsStrongTest p (-g) ↔ IsStrongTest (-p) g

def MisereGames.Form.Proviso {G : Type (u + 1)} [Form G] (A : G → Prop) (g h : G) (p : Player) : Prop

The proviso condition for comparison modulo A.

Equations

• MisereGames.Form.Proviso A g h p = (MisereGames.Form.IsEndLike p g → MisereGames.Form.Strong A h p)

theorem MisereGames.Form.Proviso.neg_iff {G : Type (u + 1)} [Form G] {A : G → Prop} [ClosedUnderNeg A] {g h : G} (p : Player) : Proviso A (-g) (-h) (-p) ↔ Proviso A g h p

theorem MisereGames.Form.proviso_right_of_misereGE {G : Type (u + 1)} [Form G] {A : G → Prop} {g h : G} (hge : g ≥m A h) : Proviso A g h Player.right

theorem MisereGames.Form.proviso_left_of_misereGE {G : Type (u + 1)} [Form G] {A : G → Prop} {g h : G} (hge : g ≥m A h) : Proviso A h g Player.left

theorem MisereGames.Form.Hereditary.misereGE_of_maintenance_proviso {G : Type (u + 1)} [Form G] (A : G → Prop) [Hereditary A] {g h : G} (h2 : Maintenance A g h Player.right) (h3 : Maintenance A g h Player.left) (h4 : Proviso A g h Player.right) (h5 : Proviso A h g Player.left) : g ≥m A h

theorem MisereGames.Form.Hereditary.misereGE_of_moves {A : GameForm → Prop} [Hereditary A] {g h : GameForm} (hl1 : ∀ gl ∈ moves Player.left g, ∃ (hl : GameForm), hl ∈ moves Player.left h) (hl2 : ∀ hl ∈ moves Player.left h, ∃ gl ∈ moves Player.left g, gl ≥m A hl) (hr1 : ∀ gr ∈ moves Player.right g, ∃ hr ∈ moves Player.right h, gr ≥m A hr) (hr2 : ∀ hr ∈ moves Player.right h, ∃ (gr : GameForm), gr ∈ moves Player.right g) : g ≥m A h

theorem MisereGames.Form.Hereditary.misereEQ_of_moves {A : GameForm → Prop} [Hereditary A] {g h : GameForm} (hl1 : ∀ gl ∈ moves Player.left g, ∃ hl ∈ moves Player.left h, gl =m A hl) (hl2 : ∀ hl ∈ moves Player.left h, ∃ gl ∈ moves Player.left g, hl =m A gl) (hr1 : ∀ gr ∈ moves Player.right g, ∃ hr ∈ moves Player.right h, gr =m A hr) (hr2 : ∀ hr ∈ moves Player.right h, ∃ gr ∈ moves Player.right g, hr =m A gr) : g =m A h