Documentation

def OnFactorisationsOfLeftDeadEnds.definition_2_1 {G : Type (u + 1)} [Form G] (A : G → Prop) :

Equations

@OnFactorisationsOfLeftDeadEnds.definition_2_1 = @ShortUniverse

Instances For

def OnFactorisationsOfLeftDeadEnds.definition_2_2 {G : Type (u + 1)} [Form G] (A : G → Prop) (hA : A ≤ Form.IsShort) :

G → Prop

Given a set of games $\mathcal{A}$, define the universal closure of $\mathcal{A}$, denoted $\mathcal{D}(\mathcal{A})$, as the minimal universe containing $\mathcal{A}$ (with respect to set inclusion).

This is Davies (Definition 2.2 on p. 6).

Equations

@OnFactorisationsOfLeftDeadEnds.definition_2_2 = @ShortUniverse.closure

Instances For

TODO: Proposition 2.3

theorem OnFactorisationsOfLeftDeadEnds.theorem_2_4 {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) :

g ≥m Form.DeadEnding.ShortDeadEnding h ↔ (Form.IsEnd Player.right g → Form.IsEnd Player.right h) ∧ ∀ gr ∈ Moves.moves Player.right g, ∃ hr ∈ Moves.moves Player.right h, gr ≥m Form.DeadEnding.ShortDeadEnding hr

If $\mathcal{U}$ is a universe, and $G$ and $H$ are Left dead ends, then $G \ge_{\mathcal{U}} H$ if and only if the following hold:

if $G \cong 0$, then $H \cong 0$; otherwise,
for every $G^R \in G^{\mathcal{R}}$, there exists some $H^R \in H^{\mathcal{R}}$ such that $G^R \ge_{\mathcal{U}} H^R$.

This is Davies (Theorem 2.4 on p. 7).

TODO: Corollary 2.5 (multiversality of comparison)

def OnFactorisationsOfLeftDeadEnds.definition_2_6 (g : GameForm) :

In a monoid $M$, we call a non-invertible element $m \in M$ a molecule if $m$ is atomic but not an atom.

This is Davies (Definition 2.6 on p. 9).

Equations

OnFactorisationsOfLeftDeadEnds.definition_2_6 = GameForm.LeftDeadEnd.IsMolecule

Instances For

3. Properties of the monoid #

theorem OnFactorisationsOfLeftDeadEnds.theorem_3_1 {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) :

g =m Form.DeadEnding.ShortDeadEnding 0 ↔ g = 0

The monoid of Left dead ends $\mathcal{L}$ is reduced.

This is Davies (Theorem 3.1 on p. 10).

theorem OnFactorisationsOfLeftDeadEnds.corollary_3_2 {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hge : g ≥m Form.DeadEnding.ShortDeadEnding h) {l : List GameForm} (hl : GameForm.LeftDeadEnd.IsRun (g :: l)) :

∃ (m : List GameForm), GameForm.LeftDeadEnd.IsRun (h :: m) ∧ List.Forall₂ (fun (a b : GameForm) => a ≥m Form.DeadEnding.ShortDeadEnding b) (g :: l) (h :: m)

If $G$ and $H$ are Left dead ends with $G \ge H$, and $k$ is an integer satisfying $0 \le k \le \tilde{b}(G)$, then, for any run $(G_0, G_1, \ldots, G_k)$ of $G$ of length $k$, there exists a run $(H_0, H_1, \ldots, H_k)$ of $H$ of length $k$ such that $G_i \ge H_i$ for every $0 \le i \le k$.

This is Davies (Corollary 3.2 on p. 10).

def OnFactorisationsOfLeftDeadEnds.definition_3_3 (gr g : GameForm) :

If $G$ is a combinatorial game, then we will say that a (Left, respectively Right) option $G'$ of $G$ is good if it is not strictly dominated by another (Left, respectively Right) option of $G$.

This is Davies (Definition 3.3 on p. 11).

Equations

OnFactorisationsOfLeftDeadEnds.definition_3_3 = GameForm.LeftDeadEnd.IsGoodOption

Instances For

theorem OnFactorisationsOfLeftDeadEnds.corollary_3_4 {g h gr : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hge : g ≥m Form.DeadEnding.ShortDeadEnding h) (hgr : GameForm.LeftDeadEnd.IsGoodOption gr g) :

∃ (hr : GameForm), GameForm.LeftDeadEnd.IsGoodOption hr h ∧ gr ≥m Form.DeadEnding.ShortDeadEnding hr

If $G \ge H$ and $G^R$ is a good option of $G$, then some (good) option $H^R$ of $H$ has $G^R \ge H^R$.

This is the $\ge$ case of Davies (Corollary 3.4 on p. 11).

theorem OnFactorisationsOfLeftDeadEnds.corollary_3_4_eq {g h gr : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (heq : g =m Form.DeadEnding.ShortDeadEnding h) (hgr : GameForm.LeftDeadEnd.IsGoodOption gr g) :

∃ (hr : GameForm), GameForm.LeftDeadEnd.IsGoodOption hr h ∧ gr =m Form.DeadEnding.ShortDeadEnding hr

If $G = H$ and $G^R$ is a good option of $G$, then some (good) option $H^R$ of $H$ has $G^R = H^R$.

This is the $=$ case of Davies (Corollary 3.4 on p. 11).

theorem OnFactorisationsOfLeftDeadEnds.lemma_3_5 {A : GameForm → Prop} {g h j : GameForm} (hgA : A g) (hhA : A h) (hj : GameForm.LeftDeadEnd.IsPocancellativeIn A j) (hge : (g + j) ≥m A h + j) :

g ≥m A h

If $\mathcal{U}$ is a universe, $G, H \in \mathcal{U}$ are Left dead ends, and $J$ is a pocancellative element of $\mathcal{U}$ satisfying $G + J \ge H + J$, then $G \ge H$.

This is Davies (Lemma 3.5 on p. 12).

theorem OnFactorisationsOfLeftDeadEnds.lemma_3_6 {A : GameForm → Prop} {g h j : GameForm} (hgA : A g) (hhA : A h) (hj : GameForm.LeftDeadEnd.IsCancellativeIn A j) (heq : (g + j) =m A h + j) :

g =m A h

If $\mathcal{U}$ is a universe, $G, H \in \mathcal{U}$ are Left dead ends, and $J$ is a cancellative element of $\mathcal{U}$ satisfying $G + J = H + J$, then $G = H$.

This is Davies (Lemma 3.6 on p. 12).

theorem OnFactorisationsOfLeftDeadEnds.theorem_3_7 {g h k : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hk : GameForm.LeftDeadEnd.IsLde k) (hge : (g + k) ≥m Form.DeadEnding.ShortDeadEnding h + k) :

g ≥m Form.DeadEnding.ShortDeadEnding h

The monoid of Left dead ends $\mathcal{L}$ is pocancellative.

This is Davies (Theorem 3.7 on p. 12).

theorem OnFactorisationsOfLeftDeadEnds.theorem_3_7_cancellative {g h k : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hk : GameForm.LeftDeadEnd.IsLde k) (heq : (g + k) =m Form.DeadEnding.ShortDeadEnding h + k) :

g =m Form.DeadEnding.ShortDeadEnding h

The monoid of Left dead ends $\mathcal{L}$ is cancellative.

This is Davies (Theorem 3.7 on p. 12).

theorem OnFactorisationsOfLeftDeadEnds.proposition_3_8 {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) {n : ℕ} (hn : 0 < n) (heq : (n • g) =m Form.DeadEnding.ShortDeadEnding n • h) :

g =m Form.DeadEnding.ShortDeadEnding h

If $G$ and $H$ are Left dead ends with $n \cdot G = n \cdot H$ for some $n > 0$, then $G = H$.

This is Davies (Proposition 3.8 on p. 13).

TODO: Corollary 3.9 (the group of differences of $\mathcal{L}$ is torsion-free)

TODO: Open Problem 3.10 (the isomorphism type of the group of differences)

def OnFactorisationsOfLeftDeadEnds.definition_3_11 (l : List GameForm) :

If $G$ is a combinatorial game and $(G_0, G_1, \ldots, G_k)$ is a run of $G$ such that $G_k \cong 0$, then we say the run is terminal.

This is Davies (Definition 3.11 on p. 14).

Equations

OnFactorisationsOfLeftDeadEnds.definition_3_11 = GameForm.LeftDeadEnd.IsTerminalRun

Instances For

def OnFactorisationsOfLeftDeadEnds.definition_3_12 (g : GameForm) :

Set ℕ

If $G$ is a short game, then we define the set of terminal lengths of $G$, denoted $T(G)$, as the set of all $n$ such that there exists a terminal run of $G$ of length $n$.

This is Davies (Definition 3.12 on p. 14), taken here in the equivalent recursive form of Lemma 3.13.

Equations

OnFactorisationsOfLeftDeadEnds.definition_3_12 = GameForm.LeftDeadEnd.terminalLengths

Instances For

theorem OnFactorisationsOfLeftDeadEnds.definition_3_12_runs {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) {n : ℕ} :

n ∈ GameForm.LeftDeadEnd.terminalLengths g ↔ ∃ (l : List GameForm), GameForm.LeftDeadEnd.IsTerminalRun (g :: l) ∧ l.length = n

$n \in T(G)$ if and only if there exists a terminal run of $G$ of length $n$.

This is Davies (Definition 3.12 on p. 14), recovered as a theorem from the recursive definition of terminalLengths.

theorem OnFactorisationsOfLeftDeadEnds.lemma_3_13 {g : GameForm} (hne : g ≠ 0) :

GameForm.LeftDeadEnd.terminalLengths g = ⋃ gr ∈ Moves.moves Player.right g, (fun (x : ℕ) => x + 1) '' GameForm.LeftDeadEnd.terminalLengths gr

If $G$ is a non-zero Left dead end, then $T(G) = \bigcup (T(G') + 1)$, where $G'$ ranges over all options of $G$.

This is Davies (Lemma 3.13 on p. 14).

noncomputable def OnFactorisationsOfLeftDeadEnds.definition_3_14 (g : GameForm) :

ℕ

If $G$ is a short game, define the race of $G$, denoted $r(G)$, as $r(G) := \min(T(G))$.

This is Davies (Definition 3.14 on p. 15).

Equations

OnFactorisationsOfLeftDeadEnds.definition_3_14 = GameForm.LeftDeadEnd.race

Instances For

def OnFactorisationsOfLeftDeadEnds.definition_3_14_integer (g : GameForm) :

A Left dead end is an integer if it is isomorphic either to $0 := \{\cdot \mid \cdot\}$ or to $\overline{n} := \{\cdot \mid \overline{n - 1}\}$ for some $n \ge 1$ (where $\overline{0} := 0$).

This is Davies (p. 15).

Equations

OnFactorisationsOfLeftDeadEnds.definition_3_14_integer = GameForm.LeftDeadEnd.IsInteger

Instances For

GameForm.LeftDeadEnd.IsInteger g ↔ (GameForm.LeftDeadEnd.terminalLengths g).Subsingleton

theorem OnFactorisationsOfLeftDeadEnds.lemma_3_15 {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) :

A Left dead end $G$ is an integer if and only if $|T(G)| = 1$. In particular, $G = \overline{n}$ if and only if $T(G) = \{n\}$.

This is Davies (Lemma 3.15 on p. 15).

theorem OnFactorisationsOfLeftDeadEnds.lemma_3_16 {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) :

[g =m Form.DeadEnding.ShortDeadEnding 0, g = 0, 0 ∈ GameForm.LeftDeadEnd.terminalLengths g, GameForm.LeftDeadEnd.race g = 0, Form.birthday g = 0].TFAE

If $G$ is a Left dead end, then the following are equivalent: $G = 0$; $G \cong 0$; $0 \in T(G)$; $r(G) = 0$; $b(G) = 0$.

This is Davies (Lemma 3.16 on p. 15).

theorem OnFactorisationsOfLeftDeadEnds.lemma_3_16_race {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) :

GameForm.LeftDeadEnd.race g = 0 ↔ g = 0

See lde_zero_tfae.

GameForm.LeftDeadEnd.terminalLengths g ⊆ GameForm.LeftDeadEnd.terminalLengths h

theorem OnFactorisationsOfLeftDeadEnds.theorem_3_17 {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hge : g ≥m Form.DeadEnding.ShortDeadEnding h) :

If $G$ and $H$ are Left dead ends with $G \ge H$, then $T(G) \subseteq T(H)$.

This is Davies (Theorem 3.17 on p. 16).

theorem OnFactorisationsOfLeftDeadEnds.corollary_3_18_race {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hge : g ≥m Form.DeadEnding.ShortDeadEnding h) :

GameForm.LeftDeadEnd.race h ≤ GameForm.LeftDeadEnd.race g

If $G$ and $H$ are Left dead ends with $G \ge H$, then $r(G) \ge r(H)$.

This is the race half of Davies (Corollary 3.18 on p. 16).

theorem OnFactorisationsOfLeftDeadEnds.corollary_3_18_birthday {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hge : g ≥m Form.DeadEnding.ShortDeadEnding h) :

Form.birthday g ≤ Form.birthday h

If $G$ and $H$ are Left dead ends with $G \ge H$, then $b(G) \le b(H)$.

This is the birthday half of Davies (Corollary 3.18 on p. 16).

theorem OnFactorisationsOfLeftDeadEnds.corollary_3_18_birthday_eq {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) :

Form.birthday g = ↑(sSup (GameForm.LeftDeadEnd.terminalLengths g))

On a Left dead end, $b(G) = \max(T(G))$.

theorem OnFactorisationsOfLeftDeadEnds.corollary_3_19 {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hge : g ≥m Form.DeadEnding.ShortDeadEnding h) {l : List GameForm} (hl : GameForm.LeftDeadEnd.IsRun (g :: l)) :

∃ (m : List GameForm), GameForm.LeftDeadEnd.IsRun (h :: m) ∧ List.Forall₂ (fun (a b : GameForm) => GameForm.LeftDeadEnd.terminalLengths a ⊆ GameForm.LeftDeadEnd.terminalLengths b) (g :: l) (h :: m)

This is Davies (Corollary 3.19 on p. 17).

theorem OnFactorisationsOfLeftDeadEnds.proposition_3_20 {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) :

GameForm.LeftDeadEnd.terminalLengths (g + h) = {x : ℕ | ∃ a ∈ GameForm.LeftDeadEnd.terminalLengths g, ∃ b ∈ GameForm.LeftDeadEnd.terminalLengths h, a + b = x}

If $G$ and $H$ are Left dead ends, then $T(G + H) = T(G) + T(H)$, a Minkowski sum.

This is Davies (Proposition 3.20 on p. 18).

theorem OnFactorisationsOfLeftDeadEnds.proposition_3_20_race {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) :

GameForm.LeftDeadEnd.race (g + h) = GameForm.LeftDeadEnd.race g + GameForm.LeftDeadEnd.race h

If $G$ and $H$ are Left dead ends, then $r(G + H) = r(G) + r(H)$.

This is the race half of Davies (Proposition 3.20 on p. 18).

theorem OnFactorisationsOfLeftDeadEnds.corollary_3_21 {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) :

(GameForm.LeftDeadEnd.terminalLengths (g + h)).ncard = max (GameForm.LeftDeadEnd.terminalLengths g).ncard (GameForm.LeftDeadEnd.terminalLengths h).ncard ↔ GameForm.LeftDeadEnd.IsInteger g ∨ GameForm.LeftDeadEnd.IsInteger h

If $G$ and $H$ are Left dead ends, then $|T(G + H)| \ge \max(|T(G)|, |T(H)|)$, with equality if and only if at least one of $G$ and $H$ is an integer.

This is Davies (Corollary 3.21 on p. 18).

theorem OnFactorisationsOfLeftDeadEnds.corollary_3_21_ge {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) :

max (GameForm.LeftDeadEnd.terminalLengths g).ncard (GameForm.LeftDeadEnd.terminalLengths h).ncard ≤ (GameForm.LeftDeadEnd.terminalLengths (g + h)).ncard

If $G$ and $H$ are Left dead ends, then $|T(G + H)| \ge \max(|T(G)|, |T(H)|)$.

This is the inequality half of Davies (Corollary 3.21 on p. 18).

theorem OnFactorisationsOfLeftDeadEnds.lemma_3_22 {g h k : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hk : GameForm.LeftDeadEnd.IsLde k) (hk0 : k ≠ 0) (heq : g =m Form.DeadEnding.ShortDeadEnding h + k) :

Form.birthday h < Form.birthday g

If $G$, $H$, and $K$ are non-zero Left dead ends with $G = H + K$, then $b(H) < b(G)$.

This is Davies (Lemma 3.22 on p. 19).

theorem OnFactorisationsOfLeftDeadEnds.lemma_3_23 {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) :

∃ (s : Multiset GameForm), GameForm.LeftDeadEnd.IsFactorisation s g

The monoid of Left dead ends $\mathcal{L}$ is atomic.

This is Davies (Lemma 3.23 on p. 19).

theorem OnFactorisationsOfLeftDeadEnds.lemma_3_24 {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) {s : Multiset GameForm} (hs : GameForm.LeftDeadEnd.IsFactorisation s g) :

s.card ≤ GameForm.LeftDeadEnd.race g

The monoid of Left dead ends $\mathcal{L}$ is a BF-monoid. In particular, if $G$ is a Left dead end, then the length of each factorisation of $G$ is at most $r(G)$; that is, $\overline{\mathsf{L}(G)} \le r(G)$.

This is Davies (Lemma 3.24 on p. 19).

theorem OnFactorisationsOfLeftDeadEnds.corollary_3_25 {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hr : GameForm.LeftDeadEnd.race g = 1) :

If $G$ is a Left dead end with $r(G) = 1$, then $G$ is an atom.

This is Davies (Corollary 3.25 on p. 20).

theorem OnFactorisationsOfLeftDeadEnds.theorem_3_26 {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) :

{s : Multiset GameForm | GameForm.LeftDeadEnd.IsFactorisation s g}.Finite

The monoid of Left dead ends $\mathcal{L}$ is an FF-monoid.

This is Davies (Theorem 3.26 on p. 20).

4. In search of a prime #

theorem OnFactorisationsOfLeftDeadEnds.lemma_4_1 {g gr : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hgr : gr ∈ Moves.moves Player.right g) :

(-1 + gr) ≥m Form.DeadEnding.ShortDeadEnding g

If $G$ is a Left dead end, then $\overline{1} + G' \ge G$ for every option $G'$ of $G$.

This is Davies (Lemma 4.1 on p. 20).

theorem OnFactorisationsOfLeftDeadEnds.proposition_4_2 {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) :

(-1 + g) =m Form.DeadEnding.ShortDeadEnding !{∅ | {g}}

If $G$ is a Left dead end, then $\overline{1} + G = \{\cdot \mid G\}$.

This is Davies (Proposition 4.2 on p. 21).

theorem OnFactorisationsOfLeftDeadEnds.proposition_4_3 {g gr : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hgr : GameForm.LeftDeadEnd.IsLde gr) :

(∃ (x : GameForm), GameForm.LeftDeadEnd.IsGoodOption x g ∧ x =m Form.DeadEnding.ShortDeadEnding gr ∧ ∀ (y : GameForm), GameForm.LeftDeadEnd.IsGoodOption y g → y =m Form.DeadEnding.ShortDeadEnding gr) ↔ g =m Form.DeadEnding.ShortDeadEnding-1 + gr

If $G$ and $G'$ are Left dead ends, then $G$ has exactly one good option (equal to) $G'$ if and only if $G = \overline{1} + G'$.

This is Davies (Proposition 4.3 on p. 21).

theorem OnFactorisationsOfLeftDeadEnds.theorem_4_4 :

GameForm.LeftDeadEnd.IsLdePrime (-1)

The game $\overline{1}$ is prime in the monoid of Left dead ends $\mathcal{L}$.

This is Davies (Theorem 4.4 on p. 21).

def OnFactorisationsOfLeftDeadEnds.open_problem_4_5 :

This is Davies (Open problem 4.5 on p. 22).

Equations

OnFactorisationsOfLeftDeadEnds.open_problem_4_5 = GameForm.LeftDeadEnd.LdeOtherPrimeProblem

Instances For

def OnFactorisationsOfLeftDeadEnds.open_problem_4_5_non_prime_atom :

This is Davies (Open problem 4.5 on p. 22).

Equations

OnFactorisationsOfLeftDeadEnds.open_problem_4_5_non_prime_atom = GameForm.LeftDeadEnd.LdeNonPrimeAtomProblem

Instances For

5. Flexibility #

noncomputable def OnFactorisationsOfLeftDeadEnds.definition_5_1 (g : GameForm) :

ℕ

If $G$ is a Left dead end, then we define the flexibility of $G$, written $f(G)$, recursively as $f(G) = 1 + \max(f(G'))$, where $G'$ ranges over all options of $G$, when $G$ is not an integer, and as $f(G) := 0$ otherwise.

This is Davies (Definition 5.1 on p. 22).

Equations

OnFactorisationsOfLeftDeadEnds.definition_5_1 = GameForm.LeftDeadEnd.flexibility

Instances For

theorem OnFactorisationsOfLeftDeadEnds.proposition_5_2 {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hf : GameForm.LeftDeadEnd.flexibility g ≤ 1) (hT : GameForm.LeftDeadEnd.terminalLengths g ⊆ GameForm.LeftDeadEnd.terminalLengths h) :

g ≥m Form.DeadEnding.ShortDeadEnding h

If $G$ and $H$ are Left dead ends with $f(G) \le 1$ and $T(G) \subseteq T(H)$, then $G \ge H$.

This is Davies (Proposition 5.2 on p. 23).

def OnFactorisationsOfLeftDeadEnds.definition_5_3 (gr g : GameForm) :

If $G$ is a Left dead end, then we say an option $G'$ of $G$ is versatile if $f(G') \ge f(G) - 1$.

This is Davies (Definition 5.3 on p. 23).

Equations

OnFactorisationsOfLeftDeadEnds.definition_5_3 = GameForm.LeftDeadEnd.IsVersatileOption

Instances For

theorem OnFactorisationsOfLeftDeadEnds.lemma_5_4 {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) :

↑(GameForm.LeftDeadEnd.flexibility g) ≤ Form.birthday g

If $G$ is a Left dead end, then $f(G) \le b(G)$, with equality if and only if $G = 0$.

This is Davies (Lemma 5.4 on p. 24).

theorem OnFactorisationsOfLeftDeadEnds.lemma_5_4_eq {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) :

↑(GameForm.LeftDeadEnd.flexibility g) = Form.birthday g ↔ g = 0

See flexibility_le_birthday.

GameForm.LeftDeadEnd.flexibility g ≤ GameForm.LeftDeadEnd.flexibility h

theorem OnFactorisationsOfLeftDeadEnds.proposition_5_5 {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hge : g ≥m Form.DeadEnding.ShortDeadEnding h) :

If $G$ and $H$ are Left dead ends with $G \ge H$, then $f(G) \le f(H)$.

This is Davies (Proposition 5.5 on p. 24).

def OnFactorisationsOfLeftDeadEnds.definition_5_6 (l : List GameForm) :

If $G$ is a Left dead end, then we say a run $(G_0, G_1, \ldots, G_n)$ of $G$ of length $n > 0$ is flexible if $G_i$ is not an integer for $i < n$. We define all runs of length $0$ to be flexible.

This is Davies (Definition 5.6 on p. 25).

Equations

OnFactorisationsOfLeftDeadEnds.definition_5_6 = GameForm.LeftDeadEnd.IsFlexibleRun

Instances For

def OnFactorisationsOfLeftDeadEnds.definition_5_6_maximal (l : List GameForm) :

A flexible run is maximal if it ends at an integer; that is, if it cannot be extended to a longer flexible run.

This is Davies (Definition 5.6 on p. 25).

Equations

OnFactorisationsOfLeftDeadEnds.definition_5_6_maximal = GameForm.LeftDeadEnd.IsMaximalFlexibleRun

Instances For

theorem OnFactorisationsOfLeftDeadEnds.lemma_5_7 {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) :

GameForm.LeftDeadEnd.flexibility g = sSup {n : ℕ | ∃ (l : List GameForm), GameForm.LeftDeadEnd.IsFlexibleRun (g :: l) ∧ l.length = n}

If $G$ is a Left dead end, then $f(G)$ is equal to the length of a longest flexible run of $G$.

This is Davies (Lemma 5.7 on p. 25).

def OnFactorisationsOfLeftDeadEnds.definition_5_8 (gr g : GameForm) :

If $G$ is a Left dead end, then we define a racing option of $G$ to be an option $G'$ such that $r(G') = r(G) - 1$.

This is Davies (Definition 5.8 on p. 25).

Equations

OnFactorisationsOfLeftDeadEnds.definition_5_8 = GameForm.LeftDeadEnd.IsRacingOption

Instances For

def OnFactorisationsOfLeftDeadEnds.definition_5_9 (gr g : GameForm) :

If $G$ is a Left dead end, then we define a stalling option of $G$ to be an option $G'$ such that $b(G') = b(G) - 1$.

This is Davies (Definition 5.9 on p. 25).

Equations

OnFactorisationsOfLeftDeadEnds.definition_5_9 = GameForm.LeftDeadEnd.IsStallingOption

Instances For

theorem OnFactorisationsOfLeftDeadEnds.proposition_5_10_int {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hgi : ¬GameForm.LeftDeadEnd.IsInteger g) (n : ℕ) :

GameForm.LeftDeadEnd.flexibility (g + -↑n) = GameForm.LeftDeadEnd.flexibility g + n

If $G$ is a non-integer Left dead end, then $f(G + \overline{n}) = f(G) + n$ for all $n \ge 0$.

This is Davies (Proposition 5.10(1) on p. 26).

theorem OnFactorisationsOfLeftDeadEnds.proposition_5_10_add {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hgi : ¬GameForm.LeftDeadEnd.IsInteger g) (hhi : ¬GameForm.LeftDeadEnd.IsInteger h) :

↑(GameForm.LeftDeadEnd.flexibility (g + h)) = max (Form.birthday g + ↑(GameForm.LeftDeadEnd.flexibility h)) (↑(GameForm.LeftDeadEnd.flexibility g) + Form.birthday h)

If $G$ and $H$ are non-integer Left dead ends, then $f(G + H) = \max(b(G) + f(H), f(G) + b(H))$.

This is Davies (Proposition 5.10(2) on p. 26).

theorem OnFactorisationsOfLeftDeadEnds.proposition_5_11 {g h k : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hk : GameForm.LeftDeadEnd.IsLde k) (hh0 : h ≠ 0) (hk_ni : ¬GameForm.LeftDeadEnd.IsInteger k) (hge : (h + k) ≥m Form.DeadEnding.ShortDeadEnding g) :

Form.birthday h < ↑(GameForm.LeftDeadEnd.flexibility g)

If $G$, $H$, and $K$ are Left dead ends such that $H$ is non-zero, $K$ is not an integer, and $H + K \ge G$, then $b(H) < f(G)$.

This is Davies (Proposition 5.11 on p. 27).

theorem OnFactorisationsOfLeftDeadEnds.corollary_5_12 {g h k : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hk : GameForm.LeftDeadEnd.IsLde k) (hh0 : h ≠ 0) (hk0 : k ≠ 0) (hmulti : ∃ (a : GameForm) (b : GameForm), GameForm.LeftDeadEnd.IsGoodOption a g ∧ GameForm.LeftDeadEnd.IsGoodOption b g ∧ ¬a =m Form.DeadEnding.ShortDeadEnding b) (heq : g =m Form.DeadEnding.ShortDeadEnding h + k) :

Form.birthday h < ↑(GameForm.LeftDeadEnd.flexibility g) ∧ Form.birthday k < ↑(GameForm.LeftDeadEnd.flexibility g)

If $G$ is a Left dead end with more than one good option, then, for any non-zero Left dead ends $H$ and $K$ with $H + K = G$, it holds that $b(H), b(K) < f(G)$.

This is Davies (Corollary 5.12 on p. 28).

theorem OnFactorisationsOfLeftDeadEnds.corollary_5_13 {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hmulti : ∃ (a : GameForm) (b : GameForm), GameForm.LeftDeadEnd.IsGoodOption a g ∧ GameForm.LeftDeadEnd.IsGoodOption b g ∧ ¬a =m Form.DeadEnding.ShortDeadEnding b) (hb : ↑(GameForm.LeftDeadEnd.flexibility g) + ↑(GameForm.LeftDeadEnd.flexibility g) < Form.birthday g + 2) :

If $G$ is a Left dead end with more than one good option, and $b(G) > 2 \cdot f(G) - 2$, then $G$ is an atom.

This is Davies (Corollary 5.13 on p. 28).

theorem OnFactorisationsOfLeftDeadEnds.proposition_5_14 {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hf : GameForm.LeftDeadEnd.flexibility g = 1) :

If $G$ is a Left dead end with $f(G) = 1$, then $G$ is an atom.

This is Davies (Proposition 5.14 on p. 28).

GameForm.LeftDeadEnd.HasUniqueGoodOption g ∨ GameForm.LeftDeadEnd.IsLdeAtom g

theorem OnFactorisationsOfLeftDeadEnds.proposition_5_14_two {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hf : GameForm.LeftDeadEnd.flexibility g = 2) :

If $G$ is a Left dead end with $f(G) = 2$, then either $G$ has exactly one good option (i.e. $\overline{1} \mid G$), or $G$ is an atom.

This is Davies (Proposition 5.14 on p. 28).

theorem OnFactorisationsOfLeftDeadEnds.proposition_5_14_three {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hf : GameForm.LeftDeadEnd.flexibility g = 3) :

GameForm.LeftDeadEnd.HasUniqueGoodOption g ∨ g =m Form.DeadEnding.ShortDeadEnding 2 • GameForm.LeftDeadEnd.waitingGame 2 ∨ GameForm.LeftDeadEnd.IsLdeAtom g

If $G$ is a Left dead end with $f(G) = 3$, then either $G$ has exactly one good option, $G = 2 \cdot W_2$, or $G$ is an atom.

This is Davies (Proposition 5.14 on p. 28).

6. Lengths of factorisations #

GameForm.LeftDeadEnd.longestFactorisationLen g ≤ GameForm.LeftDeadEnd.longestFactorisationLen gr + 1

theorem OnFactorisationsOfLeftDeadEnds.lemma_6_1 {g gr : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hgr : GameForm.LeftDeadEnd.IsGoodOption gr g) :

If $G$ is a Left dead end, then $\overline{\mathsf{L}(G)} \le \overline{\mathsf{L}(G')} + 1$ for every good option $G'$ of $G$.

This is Davies (Lemma 6.1 on p. 30).

GameForm.LeftDeadEnd.longestFactorisationLen g = GameForm.LeftDeadEnd.longestFactorisationLen gr + 1

theorem OnFactorisationsOfLeftDeadEnds.theorem_6_2 {g gr : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hgr : GameForm.LeftDeadEnd.IsLde gr) (hgood : GameForm.LeftDeadEnd.IsGoodOption gr g) (huniq : ∀ (gr' : GameForm), GameForm.LeftDeadEnd.IsGoodOption gr' g → gr' =m Form.DeadEnding.ShortDeadEnding gr) :

If $G$ is a Left dead end with exactly one good option $G'$, then $\overline{\mathsf{L}(G)} = \overline{\mathsf{L}(G')} + 1$.

This is Davies (Theorem 6.2 on p. 30).

theorem OnFactorisationsOfLeftDeadEnds.theorem_6_3 {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hmulti : ∃ (a : GameForm) (b : GameForm), GameForm.LeftDeadEnd.IsGoodOption a g ∧ GameForm.LeftDeadEnd.IsGoodOption b g ∧ ¬a =m Form.DeadEnding.ShortDeadEnding b) :

If $G$ is a Left dead end with more than one good option, then $$\overline{\mathsf{L}(G)} \le \min\left\{r(G),\ \overline{\mathsf{L}(G')} + 1,\ |T(G)| - 1,\ \frac{f(G) + 1}{2}\right\},$$ where $G'$ ranges over all good options of $G$.

This is Davies (Theorem 6.3 on p. 30).

7. Uniqueness of factorisations #

theorem OnFactorisationsOfLeftDeadEnds.proposition_7_1 {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hgood : GameForm.LeftDeadEnd.IsGoodOption h g) (hlen : GameForm.LeftDeadEnd.longestFactorisationLen g = GameForm.LeftDeadEnd.longestFactorisationLen h + 1) {s : Multiset GameForm} (hs : GameForm.LeftDeadEnd.IsFactorisation s g) (hcard : s.card = GameForm.LeftDeadEnd.longestFactorisationLen g) :

∃ (a : GameForm) (t : Multiset GameForm), s = a ::ₘ t ∧ GameForm.LeftDeadEnd.IsLdeAtom a ∧ GameForm.LeftDeadEnd.race a = 1 ∧ GameForm.LeftDeadEnd.IsFactorisation t h ∧ t.card = GameForm.LeftDeadEnd.longestFactorisationLen h

Every longest factorisation of $G$ is of the form $H_1 + \cdots + H_k + K$, where $H_1 + \cdots + H_k$ is a longest factorisation of $H$.

This is Davies (Proposition 7.1(3) on p. 32).

theorem OnFactorisationsOfLeftDeadEnds.proposition_7_1_2 {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hgood : GameForm.LeftDeadEnd.IsGoodOption h g) (hlen : GameForm.LeftDeadEnd.longestFactorisationLen g = GameForm.LeftDeadEnd.longestFactorisationLen h + 1) :

∃ (k : GameForm), GameForm.LeftDeadEnd.IsLdeAtom k ∧ GameForm.LeftDeadEnd.race k = 1 ∧ g =m Form.DeadEnding.ShortDeadEnding h + k

There exists an atom $K$ such that $G = H + K$, and $K$ is terminable.

This is the existence half of Davies (Proposition 7.1(2) on p. 32).

theorem OnFactorisationsOfLeftDeadEnds.proposition_7_1_racing {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hgood : GameForm.LeftDeadEnd.IsGoodOption h g) (hlen : GameForm.LeftDeadEnd.longestFactorisationLen g = GameForm.LeftDeadEnd.longestFactorisationLen h + 1) :

GameForm.LeftDeadEnd.IsRacingOption h g ∧ ∃ (k : GameForm), GameForm.LeftDeadEnd.IsLdeAtom k ∧ GameForm.LeftDeadEnd.race k = 1 ∧ g =m Form.DeadEnding.ShortDeadEnding h + k ∧ ∀ (k' : GameForm), GameForm.LeftDeadEnd.IsLdeAtom k' → g =m Form.DeadEnding.ShortDeadEnding h + k' → k' =m Form.DeadEnding.ShortDeadEnding k

If $G$ is a Left dead end with a good option $H$ such that $\overline{\mathsf{L}(G)} = \overline{\mathsf{L}(H)} + 1$, then

$H$ is a racing option of $G$; and
there exists a unique atom $K$ such that $G = H + K$, and $K$ is terminable.

This is Davies (Proposition 7.1 on p. 32).

GameForm.LeftDeadEnd.UniquelyFactorisable g

theorem OnFactorisationsOfLeftDeadEnds.corollary_7_2 {g h : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLdeAtom h) (hgo : GameForm.LeftDeadEnd.IsGoodOption h g) :

If $G$ is a Left dead end with a good option to an atom $H$, then either $G$ is an atom, or $H$ is a racing option of $G$ and there exists a unique (terminable) atom $K$ such that $G = H + K$; in particular, $G$ is uniquely factorisable.

This is the "in particular" of Davies (Corollary 7.2 on p. 33).

theorem OnFactorisationsOfLeftDeadEnds.corollary_7_3 {g h k : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLdeAtom h) (hk : GameForm.LeftDeadEnd.IsLdeAtom k) (hgh : GameForm.LeftDeadEnd.IsGoodOption h g) (hgk : GameForm.LeftDeadEnd.IsGoodOption k g) (hne : ¬h =m Form.DeadEnding.ShortDeadEnding k) :

GameForm.LeftDeadEnd.IsLdeAtom g ∨ GameForm.LeftDeadEnd.IsFactorisation {h, k} g

If $G$ is a Left dead end with good options to distinct atoms $H$ and $K$, then either $G$ is an atom, or $H + K$ is the unique factorisation of $G$.

This is Davies (Corollary 7.3 on p. 33).

theorem OnFactorisationsOfLeftDeadEnds.corollary_7_3_race {g h k : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLdeAtom h) (hk : GameForm.LeftDeadEnd.IsLdeAtom k) (hgh : GameForm.LeftDeadEnd.IsGoodOption h g) (hgk : GameForm.LeftDeadEnd.IsGoodOption k g) (hne : ¬h =m Form.DeadEnding.ShortDeadEnding k) (hrace : GameForm.LeftDeadEnd.race g ≠ 2) :

If either of $H$ or $K$ is not terminable (i.e. if $r(G) \ne 2$), then $G$ is an atom.

This is the "in particular" of Davies (Corollary 7.3 on p. 33).

theorem OnFactorisationsOfLeftDeadEnds.corollary_7_4 {g a b c : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (ha : GameForm.LeftDeadEnd.IsLdeAtom a) (hb : GameForm.LeftDeadEnd.IsLdeAtom b) (hc : GameForm.LeftDeadEnd.IsLdeAtom c) (hga : GameForm.LeftDeadEnd.IsGoodOption a g) (hgb : GameForm.LeftDeadEnd.IsGoodOption b g) (hgc : GameForm.LeftDeadEnd.IsGoodOption c g) (hab : ¬a =m Form.DeadEnding.ShortDeadEnding b) (hbc : ¬b =m Form.DeadEnding.ShortDeadEnding c) (hac : ¬a =m Form.DeadEnding.ShortDeadEnding c) :

If $G$ is a Left dead end with at least three good options to pairwise distinct atoms, then $G$ is an atom.

This is Davies (Corollary 7.4 on p. 33).

theorem OnFactorisationsOfLeftDeadEnds.lemma_7_5 {a : GameForm} {s' t : Multiset GameForm} (hs : GameForm.LeftDeadEnd.IsFactorisation (a ::ₘ s') (a + s'.sum)) (ht : GameForm.LeftDeadEnd.IsFactorisation t (a + s'.sum)) {ar : GameForm} (har : ar ∈ Moves.moves Player.right a) (hgood : GameForm.LeftDeadEnd.IsGoodOption (ar + s'.sum) (a + s'.sum)) (hpf : GameForm.LeftDeadEnd.IsPrimeFactorisable ar) :

∃ b ∈ t, a =m Form.DeadEnding.ShortDeadEnding b

If $G := G_1 + \cdots + G_n = H_1 + \cdots + H_m =: H$ are factorisations of a Left dead end $G$, and there is a good option of $G$ playing on the component $G_1$ to some prime-factorisable $G'_1$, then there exists an index $j$ such that $G_1 = H_j$.

This is Davies (Lemma 7.5 on p. 34).

GameForm.LeftDeadEnd.UniquelyFactorisable g

theorem OnFactorisationsOfLeftDeadEnds.theorem_7_6 {g : GameForm} {s : Multiset GameForm} (hs : GameForm.LeftDeadEnd.IsFactorisation s g) (hchain : GameForm.LeftDeadEnd.IsGoodPfChain s) :

If $G := G_1 + \cdots + G_k$ is a factorisation of a Left dead end such that, for every $1 \le i \le k$, there exists a good option of $G_i + \cdots + G_k$ on the component $G_i$ to some prime-factorisable $G'_i$, then $G$ is uniquely factorisable.

This is Davies (Theorem 7.6 on p. 35).

def OnFactorisationsOfLeftDeadEnds.theorem_7_6_chain :

Multiset GameForm → Prop

Reading a factorisation as $G_1 + \cdots + G_k$: for every $1 \le i \le k$, there exists a good option of $G_i + \cdots + G_k$ on the component $G_i$ to some prime-factorisable $G'_i$.

This is the hypothesis of Davies (Theorem 7.6 on p. 35).

Equations

OnFactorisationsOfLeftDeadEnds.theorem_7_6_chain = GameForm.LeftDeadEnd.IsGoodPfChain

Instances For

theorem OnFactorisationsOfLeftDeadEnds.lemma_7_7 {g h gr : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hh : GameForm.LeftDeadEnd.IsLde h) (hgr : gr ∈ Moves.moves Player.right g) (hgood : GameForm.LeftDeadEnd.IsGoodOption (gr + h) (g + h)) :

GameForm.LeftDeadEnd.IsGoodOption gr g

If $G + H$ is a sum of Left dead ends, and $G' + H$ is a good option of $G + H$, then $G'$ is a good option of $G$.

This is Davies (Lemma 7.7 on p. 35).

GameForm.LeftDeadEnd.UniquelyFactorisable s.sum

theorem OnFactorisationsOfLeftDeadEnds.theorem_7_8 {S : GameForm → Prop} (hS : ∀ (a : GameForm), S a → GameForm.LeftDeadEnd.IsLdeAtom a) (hpf : ∀ (a : GameForm), S a → ∀ (ar : GameForm), GameForm.LeftDeadEnd.IsGoodOption ar a → GameForm.LeftDeadEnd.IsRacingOption ar a → GameForm.LeftDeadEnd.IsPrimeFactorisable ar) {s : Multiset GameForm} (hs : ∀ a ∈ s, S a) :

If $S \subseteq \mathcal{L}$ is a set of atoms such that every good racing option of every $G \in S$ is prime-factorisable, then every $S$-factorisation is uniquely factorisable.

This is Davies (Theorem 7.8 on p. 36).

GameForm.LeftDeadEnd.UniquelyFactorisable s.sum

theorem OnFactorisationsOfLeftDeadEnds.theorem_7_9 {S : GameForm → Prop} (hS : ∀ (a : GameForm), S a → GameForm.LeftDeadEnd.IsLdeAtom a) (hpf : ∀ (a : GameForm), S a → ∀ (ar : GameForm), GameForm.LeftDeadEnd.IsGoodOption ar a → GameForm.LeftDeadEnd.IsStallingOption ar a → GameForm.LeftDeadEnd.IsPrimeFactorisable ar) {s : Multiset GameForm} (hs : ∀ a ∈ s, S a) :

If $S \subseteq \mathcal{L}$ is a set of atoms such that every good stalling option of every $G \in S$ is prime-factorisable, then every $S$-factorisation is uniquely factorisable.

This is Davies (Theorem 7.9 on p. 36).

GameForm.LeftDeadEnd.UniquelyFactorisable g

theorem OnFactorisationsOfLeftDeadEnds.proposition_7_10 {g gr : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hgo : GameForm.LeftDeadEnd.IsGoodOption gr g) (hpf : GameForm.LeftDeadEnd.IsPrimeFactorisable gr) :

If $G$ is a Left dead end with a good prime-factorisable option $H$, then $G$ is uniquely factorisable.

This is Davies (Proposition 7.10 on p. 37).

theorem OnFactorisationsOfLeftDeadEnds.proposition_7_11 {g : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) {n : ℕ} (hgo : GameForm.LeftDeadEnd.IsGoodOption (-↑n) g) :

g =m Form.DeadEnding.ShortDeadEnding -↑(n + 1) ∨ GameForm.LeftDeadEnd.IsLdeAtom g

If $G$ is a Left dead end with a good option $\overline{n}$, then either $G = \overline{n + 1}$, or else $G$ is an atom.

This is Davies (Proposition 7.11 on p. 37).

def OnFactorisationsOfLeftDeadEnds.question_7_12 :

This is Davies (Question 7.12 on p. 38).

Equations

OnFactorisationsOfLeftDeadEnds.question_7_12 = GameForm.LeftDeadEnd.GoodPrimeFactorisableQuestion

Instances For

theorem OnFactorisationsOfLeftDeadEnds.lemma_7_13 {g gr : GameForm} (hg : GameForm.LeftDeadEnd.IsLde g) (hgr : gr ∈ Moves.moves Player.right g) (n : ℕ) :

GameForm.LeftDeadEnd.IsGoodOption (gr + n • g) ((n + 1) • g) ↔ GameForm.LeftDeadEnd.IsGoodOption gr g

If $G$ is a Left dead end, then, for every $n \in \mathbb{N}_1$, $G'$ is a good option of $G$ if and only if $G' + (n - 1) \cdot G$ is a good option of $n \cdot G$.

This is Davies (Lemma 7.13 on p. 38).