LeanPool.MisereGames.Misere.PFreeDeadEnding

Misere combinatorial games.

source

instance MisereGames.instOutcomeStableGameFormIsDeadEnding :

OutcomeStable Form.IsDeadEnding

source

@[reducible, inline]

abbrev MisereGames.PFreeDeadEnding (g : GameForm) :

Prop

The P-free subpredicate of short dead-ending games.

Equations

MisereGames.PFreeDeadEnding g = MisereGames.PFreeSubset MisereGames.Form.DeadEnding.ShortDeadEnding g

Instances For

source

theorem MisereGames.PFreeDeadEnding.isDeadEnding {g : GameForm} (h_g : PFreeDeadEnding g) :

Form.IsDeadEnding g

P-free dead-ending games are dead-ending.

source

instance MisereGames.instDeadEndingGameFormPFreeDeadEnding :

Form.DeadEnding PFreeDeadEnding

source

theorem MisereGames.PFreeDeadEnding.isShort {g : GameForm} (h_g : PFreeDeadEnding g) :

Form.IsShort g

P-free dead-ending games are short.

source

instance MisereGames.instOutcomeStableGameFormShortDeadEnding :

OutcomeStable Form.DeadEnding.ShortDeadEnding

source

instance MisereGames.instClosedUnderAddNatGameFormShortDeadEnding :

Form.ClosedUnderAddNat Form.DeadEnding.ShortDeadEnding

source

instance MisereGames.instClosedUnderAddGameFormShortDeadEnding :

Form.ClosedUnderAdd Form.DeadEnding.ShortDeadEnding

source

instance MisereGames.instClosedUnderAddGameFormPFreeDeadEnding :

Form.ClosedUnderAdd PFreeDeadEnding

source

theorem MisereGames.PFreeDeadEnding.misereGE_of_int_le (a b : ℤ) (h1 : a ≥ b) :

↑b ≥m PFreeDeadEnding↑a

source

theorem MisereGames.PFreeDeadEnding.misereGE_of_nat_le (a b : ℕ) (h1 : a ≥ b) :

↑b ≥m PFreeDeadEnding↑a

source

theorem MisereGames.PFreeDeadEnding.a_one_MisereOutcome {a : ℤ} (h0 : 0 ≤ a) :

Form.Misere.Outcome.MisereOutcome !{{↑a} | {1}} = Outcome.R

source

theorem MisereGames.PFreeDeadEnding.a_one_pfreeDeadEnding {a : ℤ} (h0 : 0 ≤ a) :

PFreeDeadEnding !{{↑a} | {1}}

source

theorem MisereGames.PFreeDeadEnding.misereGE_of_maintenance_proviso {g h : GameForm} (hg : IsPFree g) (hh : IsPFree h) (h_m_r : Form.Maintenance PFreeDeadEnding g h Player.right) (h_m_l : Form.Maintenance PFreeDeadEnding g h Player.left) (h_p_r : Form.IsEnd Player.right g → Form.Misere.Outcome.MisereOutcome h ≠ Outcome.L) (h_p_l : Form.IsEnd Player.left h → Form.Misere.Outcome.MisereOutcome g ≠ Outcome.R) :

g ≥m PFreeDeadEnding h

source

theorem MisereGames.PFreeDeadEnding.reduction_a_one_int {a : ℤ} (h0 : 0 ≤ a) :

!{{↑a} | {1}} =m PFreeDeadEnding↑(a + 1)

source

theorem MisereGames.PFreeDeadEnding.reduction_ab_int (a b : ℤ) (h0 : 0 ≤ a) (h1 : 1 ≤ b) (h2 : b ≤ a + 2) :

!{{↑a} | {↑b}} =m PFreeDeadEnding↑(a + 1)

source

theorem MisereGames.PFreeDeadEnding.strong_left_of_misereOutcome_L {A : GameForm → Prop} [PFree A] [OutcomeStable A] {g : GameForm} (h1 : PFreeSubset A g) (h2 : Form.Misere.Outcome.MisereOutcome g = Outcome.L) :

Form.Strong (PFreeSubset A) g Player.left

source

theorem MisereGames.PFreeDeadEnding.strong_right_of_misereOutcome_R {A : GameForm → Prop} [PFree A] [OutcomeStable A] {g : GameForm} (h1 : PFreeSubset A g) (h2 : Form.Misere.Outcome.MisereOutcome g = Outcome.R) :

Form.Strong (PFreeSubset A) g Player.right

source

theorem MisereGames.PFreeDeadEnding.reduction_ab_between_int_left {a b : ℤ} (h0 : 0 ≤ a) (h1 : a + 2 ≤ b) :

!{{↑a} | {↑b}} ≥m PFreeDeadEnding↑(b - 1)

source

theorem MisereGames.PFreeDeadEnding.reduction_ab_between_int_right {a b : ℤ} (h0 : 0 ≤ a) (h1 : 1 ≤ b) :

↑(a + 1) ≥m PFreeDeadEnding !{{↑a} | {↑b}}

source

theorem MisereGames.PFreeDeadEnding.reduction_a_eq_neg_ba_c {a b c : ℤ} (h1 : 1 ≤ a) (h2 : 1 ≤ b) (h3 : 1 ≤ c) (h4 : c ≤ a + 1) :

!{{!{{↑(-b)} | {↑a}}} | {↑c}} =m PFreeDeadEnding↑a

source

theorem MisereGames.PFreeDeadEnding.isEnd_exists_intCast_misereEQ {p : Player} {g : GameForm} (h_g : PFreeDeadEnding g) (h_isEnd : Form.IsEnd p g) :

∃ (k : ℤ), g =m PFreeDeadEnding↑k

If $G \in \operatorname{pf}(\mathcal{E})$ is an end, then it is equivalent to some integer.

source

theorem MisereGames.PFreeDeadEnding.pfreeDeadEnding_ofSets {L R : Set GameForm} [Small.{u, u + 1} ↑L] [Small.{u, u + 1} ↑R] (h_L_mem : ∀ gl ∈ L, PFreeDeadEnding gl) (h_R_mem : ∀ gr ∈ R, PFreeDeadEnding gr) (h_L_nonempty : L.Nonempty) (h_L_finite : L.Finite) (h_R_nonempty : R.Nonempty) (h_R_finite : R.Finite) (h_outcome_ne_P : Form.Misere.Outcome.MisereOutcome !{L | R} ≠ Outcome.P) :

PFreeDeadEnding !{L | R}

source

theorem MisereGames.PFreeDeadEnding.rightSeparating_of_leftSeparating {g h : GameForm} (h_h : Form.IsShort h) (h_left : Form.AreLeftSeparating PFreeDeadEnding g h) :

Form.AreRightSeparating PFreeDeadEnding g h

source

instance MisereGames.PFreeDeadEnding.instSeparatingGameFormIsShort :

Form.Separating Form.IsShort PFreeDeadEnding