Documentation

CombinatorialGames.Misere.PFreeDeadEnding

$\mathscr{P}$-free dead-ending games #

The main results are

source
instance instOutcomeStableGameFormIsDeadEnding :
OutcomeStable Form.IsDeadEnding
source
@[reducible, inline]
abbrev PFreeDeadEnding (g : GameForm) :
Prop
Equations
Instances For
    source
    instance instDeadEndingGameFormPFreeDeadEnding :
    Form.DeadEnding PFreeDeadEnding
    source
    instance instShortGameFormPFreeDeadEnding :
    Form.Short PFreeDeadEnding
    source
    instance instOutcomeStableGameFormShortDeadEnding :
    OutcomeStable Form.DeadEnding.ShortDeadEnding
    source
    instance instClosedUnderAddNatGameFormShortDeadEnding :
    Form.ClosedUnderAddNat Form.DeadEnding.ShortDeadEnding
    source
    instance instClosedUnderAddGameFormShortDeadEnding :
    Form.ClosedUnderAdd Form.DeadEnding.ShortDeadEnding
    source
    instance instClosedUnderAddGameFormPFreeDeadEnding :
    Form.ClosedUnderAdd PFreeDeadEnding
    source
    theorem PFreeDeadEnding.misereGE_of_int_le (a b : ℤ) (h1 : a ≥ b) :
    ↑b ≥m PFreeDeadEnding↑a
    source
    theorem PFreeDeadEnding.misereGE_of_nat_le (a b : ℕ) (h1 : a ≥ b) :
    ↑b ≥m PFreeDeadEnding↑a
    source
    theorem PFreeDeadEnding.misereOutcome_ne_P_iff_winsGoingFirst {g : GameForm} :
    Form.Misere.Outcome.MisereOutcome g ≠ Outcome.P ↔ Form.Misere.Outcome.WinsGoingFirst Player.right g ∨ Form.Misere.Outcome.WinsGoingFirst Player.left g
    source
    @[simp]
    theorem PFreeDeadEnding.Set.insert_ne_empty {A : Type u_1} (x : A) (xs : Set A) :
    insert x xs ≠ ∅
    source
    theorem PFreeDeadEnding.not_isEnd_nonempty {p : Player} {g : GameForm} (h1 : ¬Form.IsEnd p g) :
    Nonempty ↑(Moves.moves p g)
    source
    theorem 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
    @[simp]
    theorem PFreeDeadEnding.isEnd_ofSets {p : Player} {st : Player → Set GameForm} [Small.{u_1, u_1 + 1} ↑(st Player.left)] [Small.{u_1, u_1 + 1} ↑(st Player.right)] :
    Form.IsEnd p !{st} ↔ st p = ∅
    source
    theorem 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 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 PFreeDeadEnding.isEnd_right_exists_intCast_misereEQ {g : GameForm} (h_g : PFreeDeadEnding g) (h_isEnd : Form.IsEnd Player.right g) :
    ∃ (n : ℕ), g =m PFreeDeadEnding↑↑n

    If $G \in \operatorname{pf}(\mathcal{E})$ is a Right end, then it is equivalent to some non-negative integer.

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