Documentation

LeanPool.MisereGames.Misere.NonInvertible

Misere combinatorial games.

source
noncomputable def MisereGames.leftEndNotLeftEndNotGeAuxT (g h : GameForm) :
GameForm

Definition of $T$ from [Siegel, "Combinatorial Game Theory" (Theorem 6.6 on p. 270)][siegel:CombinatorialGameTheory:2013]: $$ T = \left\{ \left( H^R \right)^{\circ} \mid \left\{ \cdot \mid \left( G^L \right)^{\circ} \right\} \right\}. $$

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MisereGames.short_auxT {g h : GameForm} (h_g : Form.IsShort g) (h_h : Form.IsShort h) :
    Form.IsShort (leftEndNotLeftEndNotGeAuxT g h)

    $T$ is short if $G$ and $H$ are short.

    source
    theorem MisereGames.not_misereGE_of_isEnd_left_not_isEnd_left {A : GameForm → Prop} {g h : GameForm} (h0 : A (leftEndNotLeftEndNotGeAuxT g h)) (h1 : Form.IsEnd Player.left h) (h2 : ¬Form.IsEnd Player.left g) :
    ¬g ≥m A h

    Generalisaton of [Siegel, "Combinatorial Game Theory" (Theorem 6.6 on p. 270)][siegel:CombinatorialGameTheory:2013].

    source
    theorem MisereGames.ClosedUnderNeg.not_misereGE_of_isEnd_right_not_isEnd_right {A : GameForm → Prop} [Form.ClosedUnderNeg A] {g h : GameForm} (h0 : A (leftEndNotLeftEndNotGeAuxT (-g) (-h))) (h1 : Form.IsEnd Player.right h) (h2 : ¬Form.IsEnd Player.right g) :
    ¬h ≥m A g
    source
    class MisereGames.EqZeroIdentical (A : GameForm → Prop) extends MisereGames.Form.ClosedUnderNeg A :
    Prop

    Predicates where equivalence to zero is identical equality to zero.

    Instances
      source
      instance MisereGames.instEqZeroIdenticalIsLongGameForm :
      EqZeroIdentical Form.IsLong
      source
      instance MisereGames.instEqZeroIdenticalIsShortGameForm :
      EqZeroIdentical Form.IsShort
      source
      theorem MisereGames.EqZeroIdentical.not_misereEQ_zero_of_ne_zero {A : GameForm → Prop} [EqZeroIdentical A] {g : GameForm} (h0 : A g) (h1 : g ≠ 0) :
      ¬g =m A 0
      source
      theorem MisereGames.EqZeroIdentical.misereEQ_zero_iff_eq_zero {A : GameForm → Prop} [EqZeroIdentical A] {g : GameForm} (h0 : A g) :
      g =m A 0 ↔ g = 0

      Generalisaton of [Siegel, "Combinatorial Game Theory" (Proposition 6.7 on p. 270)][siegel:CombinatorialGameTheory:2013].

      source
      theorem MisereGames.Short.misereEQ_zero_iff_eq_zero {g : GameForm} (h_g : Form.IsShort g) :
      g =m Form.IsShort 0 ↔ g = 0

      [Siegel, "Combinatorial Game Theory" (Proposition 6.7 on p. 270)][siegel:CombinatorialGameTheory:2013].

      source
      theorem MisereGames.Long.misereeq_zero_iff_eq_zero {g : GameForm} :
      g =m Form.IsLong 0 ↔ g = 0

      Transfinite generalisaton of [Siegel, "Combinatorial Game Theory" (Proposition 6.7 on p. 270)][siegel:CombinatorialGameTheory:2013].