@[irreducible]

def Form.IsDeadEnd {G : Type (u + 1)} [Form G] (p : Player) (g : G) : Prop

Equations

• Form.IsDeadEnd p g = (Form.IsEnd p g ∧ ∀ gp ∈ Moves.moves (-p) g, Form.IsDeadEnd p gp)

theorem Form.isDeadEnd_def {G : Type (u + 1)} [Form G] (p : Player) (g : G) : IsDeadEnd p g ↔ IsEnd p g ∧ ∀ gp ∈ moves (-p) g, IsDeadEnd p gp

theorem Form.isEnd_of_isDeadEnd {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : IsDeadEnd p g) : IsEnd p g

theorem Form.IsDeadEnd.hereditary_def {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : IsDeadEnd p g) (gp : G) : gp ∈ moves (-p) g → IsDeadEnd p gp

@[simp]

theorem Form.not_mem_moves_of_isDeadEnd {G : Type (u + 1)} [Form G] {g gp : G} {p : Player} (h1 : IsDeadEnd p g) : gp ∉ moves p g

theorem Form.player_eq_neg_of_isDeadEnd_mem_moves {G : Type (u + 1)} [Form G] {g gp : G} {p1 p2 : Player} (h1 : IsDeadEnd p1 g) (h2 : gp ∈ moves p2 g) : p2 = -p1

theorem Form.isDeadEnd_of_mem_moves {G : Type (u + 1)} [Form G] {g gp : G} {p1 p2 : Player} (h1 : IsDeadEnd p1 g) (h2 : gp ∈ moves p2 g) : IsDeadEnd p1 gp

theorem Form.isDeadEnd_isOption {G : Type (u + 1)} [Form G] {p : Player} {g gp : G} (h1 : IsDeadEnd p g) (h2 : IsOption gp g) : gp ∈ moves (-p) g

theorem Form.isDeadEnd_of_isOption {G : Type (u + 1)} [Form G] {g gp : G} {p : Player} (h1 : IsDeadEnd p g) (h2 : IsOption gp g) : IsDeadEnd p gp

@[irreducible]

theorem Form.IsDeadEnd.add {G : Type (u + 1)} [Form G] {g h : G} {p : Player} (h1 : IsDeadEnd p g) (h2 : IsDeadEnd p h) : IsDeadEnd p (g + h)

@[simp]

theorem Form.IsDeadEnd.neg_iff {G : Type (u + 1)} [Form G] {g : G} {p : Player} : IsDeadEnd p (-g) ↔ IsDeadEnd (-p) g

@[simp]

theorem Form.isDeadEnd_zero {G : Type (u + 1)} [Form G] {p : Player} : IsDeadEnd p 0

@[simp]

theorem Form.isDeadEnd_right_natCast {G : Type (u + 1)} [Form G] (n : ℕ) : IsDeadEnd Player.right ↑n

@[simp]

theorem Form.isDeadEnd_right_nonneg_intCast {G : Type (u + 1)} [Form G] (k : ℤ) (h1 : k ≥ 0) : IsDeadEnd Player.right ↑k

@[simp]

theorem Form.isDeadEnd_left_nonpos_intCast {G : Type (u + 1)} [Form G] (k : ℤ) (h1 : k ≤ 0) : IsDeadEnd Player.left ↑k

@[irreducible]

theorem Form.isPFree_of_isDeadEnd {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : IsDeadEnd p g) : IsPFree g

@[irreducible]

def Form.IsDeadEnding {G : Type (u + 1)} [Form G] (g : G) : Prop

Equations

• Form.IsDeadEnding g = ((∀ (p : Player), Form.IsEnd p g → Form.IsDeadEnd p g) ∧ ∀ (p : Player), ∀ gp ∈ Moves.moves p g, Form.IsDeadEnding gp)

@[simp]

theorem Form.isDeadEnd_of_isDeadEnding {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : IsDeadEnding g) (h2 : IsEnd p g) : IsDeadEnd p g

theorem Form.isDeadEnding_of_mem_moves {G : Type (u + 1)} [Form G] {g h : G} {p : Player} (h1 : IsDeadEnding g) (h2 : h ∈ moves p g) : IsDeadEnding h

theorem Form.isDeadEnding_of_isOption {G : Type (u + 1)} [Form G] {g g' : G} (h1 : IsDeadEnding g) (h2 : IsOption g' g) : IsDeadEnding g'

instance Form.instHereditaryIsDeadEnding {G : Type (u + 1)} [Form G] : Hereditary IsDeadEnding

class Form.DeadEnding {G : Type (u + 1)} [Form G] (A : G → Prop) : Prop

• isDeadEnding {g : G} (hA : A g) : IsDeadEnding g

instance Form.instDeadEndingIsDeadEnding {G : Type (u + 1)} [Form G] : DeadEnding IsDeadEnding

@[simp, irreducible]

theorem Form.DeadEnding.IsDeadEnding.add {G : Type (u + 1)} [Form G] {g h : G} (h1 : IsDeadEnding g) (h2 : IsDeadEnding h) : IsDeadEnding (g + h)

instance Form.DeadEnding.instClosedUnderNegIsDeadEnding {G : Type (u + 1)} [Form G] : ClosedUnderNeg IsDeadEnding

@[simp]

theorem Form.DeadEnding.isDeadEnding_zero {G : Type (u + 1)} [Form G] : IsDeadEnding 0

@[simp]

theorem Form.DeadEnding.isDeadEnding_natCast {G : Type (u + 1)} [Form G] (n : ℕ) : IsDeadEnding ↑n

@[simp]

theorem Form.DeadEnding.isDeadEnding_intCast {G : Type (u + 1)} [Form G] (k : ℤ) : IsDeadEnding ↑k

@[simp]

theorem Form.DeadEnding.isDeadEnding_one {G : Type (u + 1)} [Form G] : IsDeadEnding 1

structure Form.DeadEnding.ShortDeadEnding {G : Type (u + 1)} [Form G] (g : G) : Prop

• short : IsShort g
• dead_ending : IsDeadEnding g

instance Form.DeadEnding.instShortDeadEnding {G : Type (u + 1)} [Form G] : DeadEnding ShortDeadEnding

instance Form.DeadEnding.instHereditaryShortDeadEnding {G : Type (u + 1)} [Form G] : Hereditary ShortDeadEnding

instance Form.DeadEnding.instShortUniverseShortDeadEnding {G : Type (u + 1)} [Form G] : ShortUniverse ShortDeadEnding

instance Form.DeadEnding.instHasNatShortDeadEnding {G : Type (u + 1)} [Form G] : HasNat ShortDeadEnding

instance Form.DeadEnding.instHasIntShortDeadEnding {G : Type (u + 1)} [Form G] : HasInt ShortDeadEnding

instance Form.DeadEnding.instShortShortDeadEnding {G : Type (u + 1)} [Form G] : Short ShortDeadEnding

theorem GameForm.DeadEnding.isDeadEnd_left_misereOutcome_L (g : GameForm) (h1 : g ≠ 0) (h2 : Form.IsDeadEnd Player.left g) : Form.Misere.Outcome.MisereOutcome g = Outcome.L

This is Milley, Renault (Lemma 3 on p. 5).

theorem GameForm.DeadEnding.isDeadEnd_right_misereOutcome_R (g : GameForm) (h1 : g ≠ 0) (h2 : Form.IsDeadEnd Player.right g) : Form.Misere.Outcome.MisereOutcome g = Outcome.R

This is Milley, Renault (Lemma 3 on p. 5).

instance GameForm.DeadEnding.instIntegerInvertibleShortDeadEnding : IntegerInvertible Form.DeadEnding.ShortDeadEnding

instance GameForm.DeadEnding.instPropertyXShortDeadEnding : IntegerInvertible.PropertyX Form.DeadEnding.ShortDeadEnding

theorem GameForm.DeadEnding.eq_zero_of_misereOutcome {g : GameForm} (hg : Form.IsDeadEnding g) (hN : Form.Misere.Outcome.MisereOutcome g = Outcome.N) (h_left_end : Form.IsEnd Player.left g) : g = 0

theorem Form.misereGE_iff_strong_of_isDeadEnd_left {G : Type (u + 1)} [Form G] {A IsAmbient : G → Prop} (h_promain : Promain IsAmbient A) {g h : G} (h_g_dead : IsDeadEnd Player.left g) (h_h_dead : IsDeadEnd Player.left h) (h_g : IsAmbient g) (h_h : IsAmbient h) : g ≥m A h ↔ (IsEndLike Player.right g → Strong A h Player.right) ∧ ∀ gr ∈ moves Player.right g, ∃ hr ∈ moves Player.right h, gr ≥m A hr

For Left dead ends g and h (with A promain), comparison g ≥m A h reduces to the Right proviso plus maintenance of Right's moves.

theorem Form.misereGE_iff_isEndLike_of_isDeadEnd_left {G : Type (u + 1)} [Form G] {A IsAmbient : G → Prop} (h_promain : Promain IsAmbient A) (hA_end : ∃ (x : G), A x ∧ IsEnd Player.left x ∧ IsEnd Player.right x) {g h : G} (h_g_dead : IsDeadEnd Player.left g) (h_h_dead : IsDeadEnd Player.left h) (h_g : IsAmbient g) (h_h : IsAmbient h) : g ≥m A h ↔ (IsEndLike Player.right g → IsEndLike Player.right h) ∧ ∀ gr ∈ moves Player.right g, ∃ hr ∈ moves Player.right h, gr ≥m A hr

For Left dead ends, if A has a form that is an end for both players (such as 0), the Right proviso simplifies to Right end-like positions being preserved.

@[irreducible]

theorem Form.isDeadEnd_strongTest_winsGoingFirst {p : Player} {x g : GameForm} (hxd : IsDeadEnd p x) (h_test : IsStrongTest p g) : Misere.Outcome.WinsGoingFirst p (g + x)

@[irreducible]

theorem Form.isDeadEnd_strongTest_not_winsGoingFirst {p : Player} {x g : GameForm} (h_isDeadEnd : IsDeadEnd p x) (h_outcome : Misere.Outcome.MisereOutcome g = Outcome.ofPlayer p) (h_test : IsStrongTest p g) (h_gr : ∀ gr ∈ moves (-p) g, IsStrongTest p gr) : ¬Misere.Outcome.WinsGoingFirst (-p) (g + x)

theorem Form.IsStrongTest.deadEnding_strong {p : Player} {A : GameForm → Prop} [DeadEnding A] {g : GameForm} (h_test : IsStrongTest p g) : Strong A g p

This is one direction specialized to dead-ending of Davies, Milley (Theorem 3.1 on p. 7)

theorem Form.PFree.strong_iff_misereOutcome {p : Player} {A : GameForm → Prop} [DeadEnding A] [HasZero A] {g : GameForm} (h_isPFree : IsPFree g) : Strong A g p ↔ Misere.Outcome.MisereOutcome g ≠ Outcome.ofPlayer (-p)