CombinatorialGames.Misere.PFreeBlocking

The maintenance–proviso test is invariant under conjugation (negating and swapping both sides), which lets each *_right result be derived from its *_left/no-suffix counterpart.

source

theorem PFree.misereGE_iff_promain_zero_right {U : GameForm → Prop} [OutcomeStable U] [Form.Short U] [ShortUniverse U] [Form.HasInt U] {g : GameForm} (h_g : ∀ gr ∈ Moves.moves Player.right g, PFreeSubset U gr) (h_g_right_not_end : ∀ gr ∈ Moves.moves Player.right g, ¬Form.IsEnd Player.left gr) :

g ≥m (PFreeSubset U)0 ↔ Form.Promain.Test (PFreeSubset U) g 0

source

theorem PFree.misereEQ_dominated_not_isEnd_right {A : GameForm → Prop} [Form.Hereditary A] [OutcomeStable A] [Form.Short A] [ShortUniverse A] [Form.HasInt A] [Form.ClosedUnderAddNat A] [IntegerInvertible A] [Form.Blocking A] {h : GameForm} (h_h : PFreeSubset A h) (h_win : Form.Misere.Outcome.WinsGoingFirst Player.left h) :

h =m (PFreeSubset A)!{{hl : GameForm | hl ∈ Moves.moves Player.left h ∧ ¬Form.IsEnd Player.right hl} | Moves.moves Player.right h}

source

theorem PFree.misereEQ_dominated_not_isEnd_left {A : GameForm → Prop} [Form.Hereditary A] [OutcomeStable A] [Form.Short A] [ShortUniverse A] [Form.HasInt A] [Form.ClosedUnderAddNat A] [IntegerInvertible A] [Form.Blocking A] {g : GameForm} (h_g : PFreeSubset A g) (h_win : Form.Misere.Outcome.WinsGoingFirst Player.right g) :

g =m (PFreeSubset A)!{Moves.moves Player.left g | {gr : GameForm | gr ∈ Moves.moves Player.right g ∧ ¬Form.IsEnd Player.left gr}}

source

theorem PFree.zero_misereGE_iff_promain_of_winsGoingFirst {U : GameForm → Prop} [OutcomeStable U] [Form.Short U] [ShortUniverse U] [Form.HasInt U] [Form.ClosedUnderAddNat U] [IntegerInvertible U] [Form.Blocking U] {h : GameForm} (h_h : PFreeSubset U h) (h_win : Form.Misere.Outcome.WinsGoingFirst Player.left h) :

0 ≥m (PFreeSubset U)h ↔ Form.Promain.Test (PFreeSubset U) 0 !{{hl : GameForm | hl ∈ Moves.moves Player.left h ∧ ¬Form.IsEnd Player.right hl} | Moves.moves Player.right h}

source

theorem PFree.zero_misereGE_iff {U : GameForm → Prop} [OutcomeStable U] [Form.Short U] [ShortUniverse U] [Form.HasInt U] [Form.ClosedUnderAddNat U] [IntegerInvertible U] [Form.Blocking U] {h : GameForm} (h_h : PFreeSubset U h) :

0 ≥m (PFreeSubset U)h ↔ Form.Misere.Outcome.MisereOutcome h = Outcome.R ∨ Form.Misere.Outcome.MisereOutcome h = Outcome.N ∧ Form.Promain.Test (PFreeSubset U) 0 !{{hl : GameForm | hl ∈ Moves.moves Player.left h ∧ ¬Form.IsEnd Player.right hl} | Moves.moves Player.right h}

source

theorem PFree.misereGE_zero_iff_promain_of_winsGoingFirst {U : GameForm → Prop} [OutcomeStable U] [Form.Short U] [ShortUniverse U] [Form.HasInt U] [Form.ClosedUnderAddNat U] [IntegerInvertible U] [Form.Blocking U] {g : GameForm} (h_g : PFreeSubset U g) (h_win : Form.Misere.Outcome.WinsGoingFirst Player.right g) :

g ≥m (PFreeSubset U)0 ↔ Form.Promain.Test (PFreeSubset U) !{Moves.moves Player.left g | {gr : GameForm | gr ∈ Moves.moves Player.right g ∧ ¬Form.IsEnd Player.left gr}} 0

source

theorem PFree.not_misereGE_zero_of_misereOutcome_R {U : GameForm → Prop} [Form.HasInt U] [Form.ClosedUnderNeg U] {g : GameForm} (h_out : Form.Misere.Outcome.MisereOutcome g = Outcome.R) :

¬g ≥m (PFreeSubset U)0

source

theorem PFree.misereGE_zero_iff {U : GameForm → Prop} [OutcomeStable U] [Form.Short U] [ShortUniverse U] [Form.HasInt U] [Form.ClosedUnderAddNat U] [IntegerInvertible U] [Form.Blocking U] {g : GameForm} (h_g : PFreeSubset U g) :

g ≥m (PFreeSubset U)0 ↔ Form.Misere.Outcome.MisereOutcome g = Outcome.L ∨ Form.Misere.Outcome.MisereOutcome g = Outcome.N ∧ Form.Promain.Test (PFreeSubset U) !{Moves.moves Player.left g | {gr : GameForm | gr ∈ Moves.moves Player.right g ∧ ¬Form.IsEnd Player.left gr}} 0

source

theorem PFree.misereGE_iff_promain {U : GameForm → Prop} [OutcomeStable U] [Form.Short U] [ShortUniverse U] [Form.HasInt U] [Form.ClosedUnderAddNat U] [IntegerInvertible U] [Form.Blocking U] {g h : GameForm} (h_g : PFreeSubset U g) (h_h : PFreeSubset U h) :

g ≥m (PFreeSubset U)h ↔ if Form.IsEnd Player.left g ∧ Form.IsEnd Player.right g then 0 ≥m (PFreeSubset U)h else if Form.IsEnd Player.left h ∧ Form.IsEnd Player.right h then g ≥m (PFreeSubset U)0 else Form.Promain.Test (PFreeSubset U) (if Form.IsEnd Player.left g then !{{-1} | Moves.moves Player.right g} else g) (if Form.IsEnd Player.right h then !{Moves.moves Player.left h | {1}} else h)

Comparison across universes #

source

theorem PFree.isPFree_dominated_not_isEnd_right {U : GameForm → Prop} [OutcomeStable U] [Form.Short U] [ShortUniverse U] [Form.HasInt U] [Form.ClosedUnderAddNat U] [IntegerInvertible U] [Form.Blocking U] {g : GameForm} (h_g : PFreeSubset U g) (h_win : Form.Misere.Outcome.WinsGoingFirst Player.left g) :

IsPFree !{{gl : GameForm | gl ∈ Moves.moves Player.left g ∧ ¬Form.IsEnd Player.right gl} | Moves.moves Player.right g}

The dominated form of misereEQ_dominated_not_isEnd_right is P-free.

source

@[irreducible]

theorem PFree.misereGE_of_subset_pfree {U V : GameForm → Prop} [OutcomeStable U] [Form.Short U] [ShortUniverse U] [Form.HasInt U] [Form.ClosedUnderAddNat U] [IntegerInvertible U] [Form.Blocking U] [OutcomeStable V] [Form.Short V] [ShortUniverse V] [Form.HasInt V] [Form.ClosedUnderAddNat V] [IntegerInvertible V] [Form.Blocking V] (h_le : ∀ (g : GameForm), V g → U g) {g h : GameForm} (h_g : PFreeSubset V g) (h_h : PFreeSubset V h) (h_ge : g ≥m (PFreeSubset V)h) :

g ≥m (PFreeSubset U)h

Comparison modulo pf(V) implies comparison modulo the larger pf(U) on forms of pf(V).

source

theorem PFree.misereGE_pfree_iff_of_subset {U V : GameForm → Prop} [OutcomeStable U] [Form.Short U] [ShortUniverse U] [Form.HasInt U] [Form.ClosedUnderAddNat U] [IntegerInvertible U] [Form.Blocking U] [OutcomeStable V] [Form.Short V] [ShortUniverse V] [Form.HasInt V] [Form.ClosedUnderAddNat V] [IntegerInvertible V] [Form.Blocking V] (h_le : ∀ (g : GameForm), V g → U g) {g h : GameForm} (h_g : PFreeSubset V g) (h_h : PFreeSubset V h) :

g ≥m (PFreeSubset V)h ↔ g ≥m (PFreeSubset U)h

On forms of pf(V), comparison modulo pf(V) and modulo the larger pf(U) coincide, so pf(V) embeds in pf(U) as a preorder.

source

theorem PFree.misereEQ_pfree_iff_of_subset {U V : GameForm → Prop} [OutcomeStable U] [Form.Short U] [ShortUniverse U] [Form.HasInt U] [Form.ClosedUnderAddNat U] [IntegerInvertible U] [Form.Blocking U] [OutcomeStable V] [Form.Short V] [ShortUniverse V] [Form.HasInt V] [Form.ClosedUnderAddNat V] [IntegerInvertible V] [Form.Blocking V] (h_le : ∀ (g : GameForm), V g → U g) {g h : GameForm} (h_g : PFreeSubset V g) (h_h : PFreeSubset V h) :

g =m (PFreeSubset V)h ↔ g =m (PFreeSubset U)h