@[reducible, inline]

abbrev Form.Misere.Adjoint.IsRoot {G : Type (u + 1)} [Form G] (A : G → Prop) (r : G) : Prop

r is a root for A if adding it to any p end in A leaves p winning going first, just as 0 does (isRoot_zero). This is what lets the r-rooted adjoint behave like the standard adjoint in misereOutcome_add_rootedAdjoint_eq_P.

Equations

• Form.Misere.Adjoint.IsRoot A r = ∀ ⦃p : Player⦄ ⦃d : G⦄, A d → Form.IsEnd p d → Form.Misere.Outcome.WinsGoingFirst p (d + r)

theorem Form.Misere.Adjoint.isRoot_of_isZeroLike {G : Type (u + 1)} [Form G] (A : G → Prop) {r : G} (hr : IsZeroLike r) : IsRoot A r

Every zero-like form is a root for every set of forms.

theorem Form.Misere.Adjoint.isRoot_zero {G : Type (u + 1)} [Form G] (A : G → Prop) : IsRoot A 0

0 is a root for every set of forms: adding 0 to an end yields an end.

@[irreducible]

theorem Form.Misere.Adjoint.misereOutcome_add_rootedAdjoint_eq_P {G : Type (u + 1)} [Form G] {A : G → Prop} [Hereditary A] {r : G} (h_isRoot : IsRoot A r) {g : G} (hg : A g) : Outcome.MisereOutcome (g + rootedAdjoint r g) = Outcome.P

For every form g in A, the sum g + rootedAdjoint r g is a $\mathscr{P}$-position, provided r is a root for the hereditary set A (IsRoot).

This generalises misereOutcome_add_adjoint_eq_P, which is the case where A is arbitrary and r = 0.

theorem Form.Misere.Adjoint.misereOutcome_add_adjoint_eq_P {G : Type (u + 1)} [Form G] (g : G) : Outcome.MisereOutcome (g + g°) = Outcome.P

Siegel, (Proposition 3.3 on p. 228) showed that, for every short game form $G$, the sum $G+G^\circ$ is always a $\mathscr{P}$-position. (See also Siegel, (Proposition 6.4 on p. 270).) Siegel, (Proposition 5.7 on p. 214) later extended this result to short augmented forms. The present result generalises further to transfinite augmented forms.