noncomputable def leftEnd_not_leftEnd_not_ge.auxT (g h : GameForm) : GameForm

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

Equations

• leftEnd_not_leftEnd_not_ge.auxT g h = !{Set.range fun (hr : ↑(Moves.moves Player.right h)) => ↑hr° | {!{∅ | Set.range fun (gl : ↑(Moves.moves Player.left g)) => ↑gl°}}}

theorem short_auxT {g h : GameForm} (h_g : Form.IsShort g) (h_h : Form.IsShort h) : Form.IsShort (leftEnd_not_leftEnd_not_ge.auxT g h)

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

theorem not_misereGE_of_isEnd_left_not_isEnd_left {A : GameForm → Prop} {g h : GameForm} (h0 : A (leftEnd_not_leftEnd_not_ge.auxT 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).

theorem ClosedUnderNeg.not_misereGE_of_isEnd_right_not_isEnd_right {A : GameForm → Prop} [Form.ClosedUnderNeg A] {g h : GameForm} (h0 : A (leftEnd_not_leftEnd_not_ge.auxT (-g) (-h))) (h1 : Form.IsEnd Player.right h) (h2 : ¬Form.IsEnd Player.right g) : ¬h ≥m A g

class EqZeroIdentical (A : GameForm → Prop) extends Form.ClosedUnderNeg A : Prop

• neg_of {g : GameForm} (h1 : A g) : A (-g)
• has_T_g_zero {g : GameForm} (h1 : A g) : A (leftEnd_not_leftEnd_not_ge.auxT g 0)

instance instEqZeroIdenticalIsLongGameForm : EqZeroIdentical Form.IsLong

instance instEqZeroIdenticalIsShortGameForm : EqZeroIdentical Form.IsShort

theorem EqZeroIdentical.not_misereEQ_zero_of_ne_zero {A : GameForm → Prop} [EqZeroIdentical A] {g : GameForm} (h0 : A g) (h1 : g ≠ 0) : ¬g =m A 0

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

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

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