Short games

A combinatorial game is Short if it is finite and loopfree: it has only finite many distinct subpositions, and every run has finite length. See Siegel, Definition 4.1 on p. 34.

@[irreducible]

def Form.IsShort {G : Type (u + 1)} [Form G] (x : G) : Prop

Equations

• Form.IsShort x = ∀ (p : Player), (Moves.moves p x).Finite ∧ ∀ y ∈ Moves.moves p x, Form.IsShort y

theorem Form.isShort_def {G : Type (u + 1)} [Form G] {x : G} : IsShort x ↔ ∀ (p : Player), (moves p x).Finite ∧ ∀ y ∈ moves p x, IsShort y

theorem Form.IsShort.mk {G : Type (u + 1)} [Form G] {x : G} : (∀ (p : Player), (moves p x).Finite ∧ ∀ y ∈ moves p x, IsShort y) → IsShort x

Alias of the reverse direction of Form.isShort_def.

theorem Form.IsShort.finite_moves {G : Type (u + 1)} [Form G] (p : Player) {x : G} (hx : IsShort x) : (moves p x).Finite

theorem Form.IsShort.finite_moves' {G : Type (u + 1)} [Form G] (p : Player) {x : G} (hx : IsShort x) : Finite ↑(moves p x)

theorem Form.IsShort.finite_setOf_isOption {G : Type (u + 1)} [Form G] {x : G} (hx : IsShort x) : {y : G | IsOption y x}.Finite

theorem Form.IsShort.of_mem_moves {G : Type (u + 1)} [Form G] {x y : G} (hx : IsShort x) {p : Player} (hy : y ∈ moves p x) : IsShort y

theorem Form.IsShort.isOption {G : Type (u + 1)} [Form G] {x y : G} (hx : IsShort x) (h : IsOption y x) : IsShort y

theorem Moves.IsOption.isShort {G : Type (u + 1)} [Form G] {x y : G} (hx : Form.IsShort x) (h : IsOption y x) : Form.IsShort y

Alias of Form.IsShort.isOption.

@[irreducible]

theorem Form.IsShort.subposition {G : Type (u + 1)} [Form G] {x y : G} (hx : IsShort x) (h : Subposition y x) : IsShort y

theorem Moves.IsOption.subposition {G : Type (u + 1)} [Form G] {x y : G} (hx : Form.IsShort x) (h : Subposition y x) : Form.IsShort y

Alias of Form.IsShort.subposition.

@[irreducible]

theorem Form.IsShort.finite_setOf_subposition {G : Type (u + 1)} [Form G] {x : G} (hx : IsShort x) : {y : G | Subposition y x}.Finite

@[irreducible]

theorem Moves.short_iff_finite_setOf_subposition {G : Type (u + 1)} [Form G] {x : G} : Form.IsShort x ↔ {y : G | Subposition y x}.Finite

@[irreducible]

theorem Form.IsShort.add {G : Type (u + 1)} [Form G] {x y : G} (hx : IsShort x) (hy : IsShort y) : IsShort (x + y)

@[irreducible]

theorem Form.IsShort.neg {G : Type (u + 1)} [Form G] {x : G} (hx : IsShort x) : IsShort (-x)

instance Form.IsShort.instClosedUnderNeg {G : Type (u + 1)} [Form G] : ClosedUnderNeg IsShort

instance Form.IsShort.instHereditary {G : Type (u + 1)} [Form G] : Hereditary IsShort

theorem Form.IsShort.neg_iff {G : Type (u + 1)} [Form G] {x : G} : IsShort (-x) ↔ IsShort x

theorem Form.IsShort.short_iff_finite_setOf_subposition {G : Type (u + 1)} [Form G] {x : G} : IsShort x ↔ {y : G | Subposition y x}.Finite

@[simp]

theorem Form.IsShort.zero {G : Type (u + 1)} [Form G] : IsShort 0

instance Form.IsShort.instHasZero {G : Type (u + 1)} [Form G] : HasZero IsShort

theorem Form.IsShort.ofSets {G : Type (u + 1)} [Form G] {s t : Set G} [Small.{u, u + 1} ↑s] [Small.{u, u + 1} ↑t] (hs_fin : s.Finite) (hs_short : ∀ g ∈ s, IsShort g) (ht_fin : t.Finite) (ht_short : ∀ g ∈ t, IsShort g) : IsShort !{s | t}

@[simp]

theorem Form.IsShort.star {G : Type (u + 1)} [Form G] : IsShort !{{0} | {0}}

@[simp]

theorem Form.IsShort.one {G : Type (u + 1)} [Form G] : IsShort 1

theorem Form.IsShort.sub {x y : GameForm} (hx : IsShort x) (hy : IsShort y) : IsShort (x - y)

@[simp]

theorem Form.IsShort.natCast {G : Type (u + 1)} [Form G] (n : ℕ) : IsShort ↑n

@[simp]

theorem Form.IsShort.ofNat {G : Type (u + 1)} [Form G] (n : ℕ) [n.AtLeastTwo] : IsShort (OfNat.ofNat n)

@[simp]

theorem Form.IsShort.intCast {G : Type (u + 1)} [Form G] (n : ℤ) : IsShort ↑n

class Form.Short {G : Type (u + 1)} [Form G] (A : G → Prop) : Prop

• isShort {g : G} (h_g : A g) : IsShort g

@[irreducible]

theorem GameForm.short_iff_birthday_finite {g : GameForm} : Form.IsShort g ↔ Form.birthday g < NatOrdinal.of Ordinal.omega0

theorem GameForm.short_iff_birthday_nat {x : GameForm} : Form.IsShort x ↔ ∃ (n : ℕ), Form.birthday x = ↑n