Documentation

LeanPool.MisereGames.Misere.PFreeBlocking

Misere combinatorial games.

source
@[reducible, inline]
abbrev MisereGames.GameForm.PFreeBlocking :
GameForm → Prop

The P-free subpredicate of the short blocking games.

Equations
Instances For
    source
    theorem MisereGames.GameForm.misereOutcome_L_add_isEnd_left {g h : GameForm} (hg : g.PFreeBlocking) (hh : h.PFreeBlocking) (hgL : Form.Misere.Outcome.MisereOutcome g = Outcome.L) (hhe : Form.IsEnd Player.left h) :
    Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.L

    If G, H ∈ pf(B) with o(G) = L and H a Left end, then o(G + H) = L.

    This is [Davies, Miller, Milley (Lemma 4.1 on p. 24)][davies:SumsPFreeForms:2025]

    source
    theorem MisereGames.GameForm.misereOutcome_R_add_isEnd_right {g h : GameForm} (hg : g.PFreeBlocking) (hh : h.PFreeBlocking) (hgR : Form.Misere.Outcome.MisereOutcome g = Outcome.R) (hhe : Form.IsEnd Player.right h) :
    Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.R

    This is the mirror of [Davies, Miller, Milley (Lemma 4.1 on p. 24)][davies:SumsPFreeForms:2025].

    source
    instance MisereGames.GameForm.instOutcomeStableShortBlocking :
    OutcomeStable Form.ShortBlocking

    This is [Davies, Miller, Milley (Lemma 4.2 on p. 25)][davies:SumsPFreeForms:2025].

    source
    theorem MisereGames.GameForm.miserePlayerOutcome_right_isEnd_left_NN {g h : GameForm} (hg : g.PFreeBlocking) (hh : h.PFreeBlocking) (hge : Form.IsEnd Player.left g) (hgN : Form.Misere.Outcome.MisereOutcome g = Outcome.N) (hhN : Form.Misere.Outcome.MisereOutcome h = Outcome.N) :
    Form.Misere.Outcome.MiserePlayerOutcome (g + h) Player.right = Player.right

    This is [Davies, Miller, Milley (Lemma 4.7 on p. 26)][davies:SumsPFreeForms:2025].

    source
    theorem MisereGames.GameForm.miserePlayerOutcome_left_isEnd_right_NN {g h : GameForm} (hg : g.PFreeBlocking) (hh : h.PFreeBlocking) (hge : Form.IsEnd Player.right g) (hgN : Form.Misere.Outcome.MisereOutcome g = Outcome.N) (hhN : Form.Misere.Outcome.MisereOutcome h = Outcome.N) :
    Form.Misere.Outcome.MiserePlayerOutcome (g + h) Player.left = Player.left

    This is the mirror of [Davies, Miller, Milley (Lemma 4.7 on p. 26)][davies:SumsPFreeForms:2025].

    source
    instance MisereGames.GameForm.instPropertyXShortBlocking :
    IntegerInvertible.PropertyX Form.ShortBlocking

    This is [Davies, Miller, Milley (Lemma 4.8 on p. 26)][davies:SumsPFreeForms:2025].

    source
    instance MisereGames.GameForm.instClosedUnderAddPFreeBlocking :
    Form.ClosedUnderAdd PFreeBlocking

    This is [Davies, Miller, Milley (Lemma 4.9 on p. 27)][davies:SumsPFreeForms:2025].