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

Equations

• Form.Maintenance A g h Player.right = ∀ gr ∈ Moves.moves Player.right g, (∃ hr ∈ Moves.moves Player.right h, gr ≥m A hr) ∨ ∃ grl ∈ Moves.moves Player.left gr, grl ≥m A h
• Form.Maintenance A g h Player.left = ∀ hl ∈ Moves.moves Player.left h, (∃ gl ∈ Moves.moves Player.left g, gl ≥m A hl) ∨ ∃ hlr ∈ Moves.moves Player.right hl, g ≥m A hlr

theorem 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 Form.Strong {G : Type (u + 1)} [Form G] (A : G → Prop) (g : G) (p : Player) : Prop

Equations

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

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

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

@[irreducible]

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

This is the test given by Davies, Milley (Theorem 3.1 on p. 7).

Equations

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

theorem 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 Form.IsStrongTest.neg_iff {p : Player} {g : GameForm} : IsStrongTest p (-g) ↔ IsStrongTest (-p) g

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

Equations

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

theorem 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 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 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 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 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 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

theorem Form.Hereditary.misereEQ_of_left_subset_dominated {A : GameForm → Prop} [Hereditary A] {g g' : GameForm} (h_right : moves Player.right g' = moves Player.right g) (h_subset : moves Player.left g' ⊆ moves Player.left g) (h_dom : ∀ gl ∈ moves Player.left g, ∃ gl' ∈ moves Player.left g', gl' ≥m A gl) : g =m A g'

theorem Form.Hereditary.misereEQ_of_right_subset_dominated {A : GameForm → Prop} [Hereditary A] {g g' : GameForm} (h_left : moves Player.left g' = moves Player.left g) (h_subset : moves Player.right g' ⊆ moves Player.right g) (h_dom : ∀ gr ∈ moves Player.right g, ∃ gr' ∈ moves Player.right g', gr ≥m A gr') : g =m A g'

theorem Form.Hereditary.misereEQ_removeLeft_of_dominated {A : GameForm → Prop} [Hereditary A] {L R : Set GameForm} [Small.{u, u + 1} ↑L] [Small.{u, u + 1} ↑R] {gl1 gl2 : GameForm} (h_gl2 : gl2 ∈ L) (h_ne : gl2 ≠ gl1) (h_dom : gl2 ≥m A gl1) : !{L | R} =m A !{L \ {gl1} | R}