@[reducible, inline]

abbrev GameForm.PFreeBlocking : GameForm → Prop

Equations

• GameForm.PFreeBlocking = PFreeSubset Form.ShortBlocking

instance GameForm.instBlockingPFreeSubset {A : GameForm → Prop} [Form.Blocking A] : Form.Blocking (PFreeSubset A)

If A is a blocking universe then so is pf(A) = PFreeSubset A.

@[irreducible]

theorem GameForm.misereOutcome_ofPlayer_add_isEnd {A : GameForm → Prop} [Form.Blocking A] [Form.Hereditary A] {p : Player} {g h : GameForm} (hg : PFreeSubset A g) (hh : PFreeSubset A h) (hgL : Form.Misere.Outcome.MisereOutcome g = Outcome.ofPlayer p) (hhe : Form.IsEnd p h) : Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.ofPlayer p

If G, H ∈ pf(B) with o(G) = L and H a Left end, then o(G + H) = L.

This is Davies, Miller, Milley (Lemma 4.1 on p. 24)

instance GameForm.instOutcomeStableShortBlocking : OutcomeStable Form.ShortBlocking

This is Davies, Miller, Milley (Lemma 4.2 on p. 25).

@[irreducible]

theorem GameForm.miserePlayerOutcome_right_isEnd_left_NN {A : GameForm → Prop} [Form.Blocking A] [Form.Hereditary A] [OutcomeStable A] [Form.ClosedUnderNeg A] {g h : GameForm} (hg : PFreeSubset A g) (hh : PFreeSubset A h) (hge : Form.IsEnd Player.left g) (hgN : Form.Misere.Outcome.MisereOutcome g = Outcome.N) (hhN : Form.Misere.Outcome.MisereOutcome h = Outcome.N) : Form.Misere.Outcome.MiserePlayerOutcome (g + h) Player.right = Player.right

This is Davies, Miller, Milley (Lemma 4.7 on p. 26).

theorem GameForm.miserePlayerOutcome_left_isEnd_right_NN {A : GameForm → Prop} [Form.Blocking A] [Form.Hereditary A] [OutcomeStable A] [Form.ClosedUnderNeg A] {g h : GameForm} (hg : PFreeSubset A g) (hh : PFreeSubset A h) (hge : Form.IsEnd Player.right g) (hgN : Form.Misere.Outcome.MisereOutcome g = Outcome.N) (hhN : Form.Misere.Outcome.MisereOutcome h = Outcome.N) : Form.Misere.Outcome.MiserePlayerOutcome (g + h) Player.left = Player.left

This is the mirror of Davies, Miller, Milley (Lemma 4.7 on p. 26).

@[irreducible]

theorem GameForm.miserePlayerOutcome_right_isEnd_right_NN {A : GameForm → Prop} [Form.Blocking A] [Form.Hereditary A] [OutcomeStable A] [Form.ClosedUnderNeg A] {g h : GameForm} (hg : PFreeSubset A g) (hh : PFreeSubset A h) (hge : Form.IsEnd Player.right g) (hgN : Form.Misere.Outcome.MisereOutcome g = Outcome.N) (hhN : Form.Misere.Outcome.MisereOutcome h = Outcome.N) : Form.Misere.Outcome.MiserePlayerOutcome (g + h) Player.right = Player.right

theorem GameForm.misereOutcome_N_isEnd_NN {A : GameForm → Prop} [Form.Blocking A] [Form.Hereditary A] [OutcomeStable A] [Form.ClosedUnderNeg A] {g h : GameForm} (hg : PFreeSubset A g) (hh : PFreeSubset A h) {p : Player} (hge : Form.IsEnd p g) (hgN : Form.Misere.Outcome.MisereOutcome g = Outcome.N) (hhN : Form.Misere.Outcome.MisereOutcome h = Outcome.N) : Form.Misere.Outcome.MisereOutcome (g + h) = Outcome.N

instance GameForm.instPropertyXShortBlocking : IntegerInvertible.PropertyX Form.ShortBlocking

This is Davies, Miller, Milley (Lemma 4.8 on p. 26).

instance GameForm.instClosedUnderAddPFreeBlocking : Form.ClosedUnderAdd PFreeBlocking

This is Davies, Miller, Milley (Lemma 4.9 on p. 27).

theorem GameForm.Strong.of_subset {p : Player} {A B : GameForm → Prop} {g : GameForm} (h_strong : Form.Strong B g p) (h_subset : ∀ (x : GameForm), A x → B x) : Form.Strong A g p

theorem GameForm.PFreeBlocking.strong_iff_misereOutcome_ne {A : GameForm → Prop} [Form.Blocking A] [Form.HasZero A] {p : Player} {g : GameForm} (hg : IsPFree g) : Form.Strong A g p ↔ Form.Misere.Outcome.MisereOutcome g ≠ Outcome.ofPlayer (-p)

theorem GameForm.PFreeBlocking.misereGE_of_maintenance_proviso {A : GameForm → Prop} [Form.Blocking A] [Form.Hereditary A] [Form.HasZero A] {g h : GameForm} (hg : IsPFree g) (hh : IsPFree h) (h_m_r : Form.Maintenance A g h Player.right) (h_m_l : Form.Maintenance A g h Player.left) (h_p_r : Form.IsEnd Player.right g → Form.Misere.Outcome.MisereOutcome h ≠ Outcome.L) (h_p_l : Form.IsEnd Player.left h → Form.Misere.Outcome.MisereOutcome g ≠ Outcome.R) : g ≥m A h

theorem GameForm.PFreeBlocking.add_neg_self_strong {A : GameForm → Prop} [Form.Blocking A] [Form.ClosedUnderAdd A] [Form.ClosedUnderNeg A] [PFree A] {p : Player} {g : GameForm} (hg : A g) : Form.Strong PFreeBlocking (g + -g) p

theorem GameForm.IsBlocking.strong_of_misereOutcome_ne_R {A : GameForm → Prop} [Form.Blocking A] {g : GameForm} (hg : IsPFree g) (h_out : Form.Misere.Outcome.MisereOutcome g ≠ Outcome.R) : Form.Strong A g Player.left

This is Davies, Miller, Milley (Lemma 4.4 on p. 25).

theorem GameForm.IsBlocking.add_neg_self_strong_left {A : GameForm → Prop} [Form.Blocking A] [PFree A] [Form.ClosedUnderAdd A] [Form.ClosedUnderNeg A] {g : GameForm} (hg : A g) : Form.Strong A (g + -g) Player.left

This is Davies, Miller, Milley (Lemma 4.10 on p. 27).

@[reducible, inline]

noncomputable abbrev GameForm.Blocking.Plugged (g : GameForm) : GameForm

Equations

• GameForm.Blocking.Plugged g = !{Moves.moves Player.left g | {1}}

theorem GameForm.Blocking.plugged_misereOutcome {g : GameForm} : Form.Misere.Outcome.WinsGoingFirst Player.right (Plugged g)

theorem GameForm.Blocking.plugged_mem {A : GameForm → Prop} [ShortUniverse A] [Form.Blocking A] [OutcomeStable A] [Form.HasInt A] [Form.Short A] {g : GameForm} (h_g : PFreeSubset A g) (h_not_left : ¬Form.IsEnd Player.left g) : PFreeSubset A (Plugged g)

theorem GameForm.Blocking.isEnd_right_zero_misereGE {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_g_isEnd : Form.IsEnd Player.right g) : 0 ≥m (PFreeSubset U)g

theorem GameForm.Blocking.isEnd_left_misereGE_zero {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_g_isEnd : Form.IsEnd Player.left g) : g ≥m (PFreeSubset U)0

theorem GameForm.Blocking.reduction_plug_end_not_isEnd_left {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_isEnd : Form.IsEnd Player.right g) (h_not_left : ¬Form.IsEnd Player.left g) : g =m (PFreeSubset U)!{Moves.moves Player.left g | {1}}

theorem GameForm.Blocking.pluggedLeft_mem {A : GameForm → Prop} [ShortUniverse A] [Form.Blocking A] [OutcomeStable A] [Form.HasInt A] [Form.Short A] {g : GameForm} (h_g : PFreeSubset A g) (h_not_right : ¬Form.IsEnd Player.right g) : PFreeSubset A !{{-1} | Moves.moves Player.right g}

Left/Right mirror of plugged_mem, for a g that is a Left end but not a Right end.

theorem GameForm.Blocking.reduction_plug_end_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_isEnd : Form.IsEnd Player.left g) (h_not_right : ¬Form.IsEnd Player.right g) : g =m (PFreeSubset U)!{{-1} | Moves.moves Player.right g}

Left/Right mirror of reduction_plug_end_not_isEnd_left, for a g that is a Left end but not a Right end.

Separation

theorem PFree.rightSeparating_of_leftSeparating {A : GameForm → Prop} [Form.Short A] [ClosedUnderDicotic Form.IsShort A] [Form.HasInt A] {g h : GameForm} (h_h : Form.IsShort h) (h_left : Form.AreLeftSeparating (PFreeSubset A) g h) : Form.AreRightSeparating (PFreeSubset A) g h

theorem PFree.rightSeparating_iff_leftSeparating {A : GameForm → Prop} [Form.Short A] [ClosedUnderDicotic Form.IsShort A] [Form.HasInt A] [Form.ClosedUnderNeg A] {g h : GameForm} (h_g : Form.IsShort g) (h_h : Form.IsShort h) : Form.AreRightSeparating (PFreeSubset A) g h ↔ Form.AreLeftSeparating (PFreeSubset A) g h

theorem PFree.separating_pair_of_right_iff_left {A : GameForm → Prop} [Form.Short A] [ClosedUnderDicotic Form.IsShort A] [Form.HasInt A] [Form.ClosedUnderNeg A] {g h : GameForm} (h_g : Form.IsShort g) (h_h : Form.IsShort h) (h_not_ge : ¬g ≥m (PFreeSubset A)h) : Form.AreLeftSeparating (PFreeSubset A) g h ∧ Form.AreRightSeparating (PFreeSubset A) g h

instance PFree.instSeparatingGameFormIsShortPFreeSubset {A : GameForm → Prop} [Form.Short A] [ClosedUnderDicotic Form.IsShort A] [Form.ClosedUnderNeg A] [Form.HasInt A] : Form.Separating Form.IsShort (PFreeSubset A)

theorem PFree.downlinked_of_not_isEnd_left {U : GameForm → Prop} [OutcomeStable U] [Form.Short U] [ShortUniverse U] [Form.HasInt U] {g h : GameForm} (h_g : PFreeSubset U g) (h_h : PFreeSubset U h) (h_g_not_isEnd : ¬Form.IsEnd Player.left g) (h_moves_g : ∀ gl ∈ Moves.moves Player.left g, ¬gl ≥m (PFreeSubset U)h) (h_moves_h : ∀ hr ∈ Moves.moves Player.right h, ¬g ≥m (PFreeSubset U)hr) : Form.Downlinked (PFreeSubset U) g h

theorem PFree.downlinked_of_not_isEnd_right {U : GameForm → Prop} [OutcomeStable U] [Form.Short U] [ShortUniverse U] [Form.HasInt U] {g h : GameForm} (h_g : PFreeSubset U g) (h_h : PFreeSubset U h) (h_h_not_isEnd : ¬Form.IsEnd Player.right h) (h_moves_g : ∀ gl ∈ Moves.moves Player.left g, ¬gl ≥m (PFreeSubset U)h) (h_moves_h : ∀ hr ∈ Moves.moves Player.right h, ¬g ≥m (PFreeSubset U)hr) : Form.Downlinked (PFreeSubset U) g h

theorem PFree.downlinked_intCast_of_not_leftMoves_misereGE {U : GameForm → Prop} [OutcomeStable U] [Form.Short U] [ShortUniverse U] [Form.HasInt U] {g : GameForm} {n : ℤ} (h_g : PFreeSubset U g) (h_not_left_end : ¬Form.IsEnd Player.left g) (h_n : 0 ≤ n) (h : ∀ gl ∈ Moves.moves Player.left g, ¬gl ≥m (PFreeSubset U)↑n) : Form.Downlinked (PFreeSubset U) g ↑n

theorem PFree.misereGE_iff_promain_not_isEnd_left_right {U : GameForm → Prop} [OutcomeStable U] [Form.Short U] [ShortUniverse U] [Form.HasInt U] [Form.ClosedUnderAddNat U] [IntegerInvertible U] {g h : GameForm} (h_g : PFreeSubset U g) (h_h : PFreeSubset U h) (h_g_not_isEnd : ¬Form.IsEnd Player.left g) (h_h_not_isEnd : ¬Form.IsEnd Player.right h) : g ≥m (PFreeSubset U)h ↔ Form.Promain.Test (PFreeSubset U) g h

theorem PFree.misereGE_intCast_iff_promain_not_isEnd_left {U : GameForm → Prop} [OutcomeStable U] [Form.Short U] [ShortUniverse U] [Form.HasInt U] [Form.ClosedUnderAddNat U] [IntegerInvertible U] {g : GameForm} {n : ℤ} (h_n : 0 ≤ n) (h_g : PFreeSubset U g) (h_g_not_isEnd : ¬Form.IsEnd Player.left g) : g ≥m (PFreeSubset U)↑n ↔ Form.Promain.Test (PFreeSubset U) g !{{↑(n - 1)} | {1}}

theorem PFree.misereGE_iff_promain_not_isEnd_left_left {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) (h_g_not_isEnd : ¬Form.IsEnd Player.left g) (h_h_not_isEnd : ¬Form.IsEnd Player.left h) (h_h_isEnd : Form.IsEnd Player.right h) : g ≥m (PFreeSubset U)h ↔ Form.Promain.Test (PFreeSubset U) g !{Moves.moves Player.left h | {1}}

theorem PFree.misereGE_iff_promain_not_isEnd_right_right {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) (h_g_isEnd : Form.IsEnd Player.left g) (h_g_not_isEnd : ¬Form.IsEnd Player.right g) (h_h_not_isEnd : ¬Form.IsEnd Player.right h) : g ≥m (PFreeSubset U)h ↔ Form.Promain.Test (PFreeSubset U) !{{-1} | Moves.moves Player.right g} h

theorem PFree.misereGE_intCast_iff_promain_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} {n : ℤ} (h_n : 0 ≤ n) (h_g : PFreeSubset U g) (h_g_isEnd : Form.IsEnd Player.left g) (h_g_not_isEnd : ¬Form.IsEnd Player.right g) : g ≥m (PFreeSubset U)↑n ↔ Form.Promain.Test (PFreeSubset U) !{{-1} | Moves.moves Player.right g} !{{↑(n - 1)} | {1}}

theorem PFree.misereGE_iff_promain_not_isEnd_right_left {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) (h_g_isEnd : Form.IsEnd Player.left g) (h_g_not_isEnd : ¬Form.IsEnd Player.right g) (h_h_not_isEnd : ¬Form.IsEnd Player.left h) (h_h_isEnd : Form.IsEnd Player.right h) : g ≥m (PFreeSubset U)h ↔ Form.Promain.Test (PFreeSubset U) !{{-1} | Moves.moves Player.right g} !{Moves.moves Player.left h | {1}}

theorem PFree.misereGE_iff_promain_zero_left {U : GameForm → Prop} [OutcomeStable U] [Form.Short U] [ShortUniverse U] [Form.HasInt U] {h : GameForm} (h_h : ∀ hl ∈ Moves.moves Player.left h, PFreeSubset U hl) (h_h_left_not_end : ∀ hl ∈ Moves.moves Player.left h, ¬Form.IsEnd Player.right hl) : 0 ≥m (PFreeSubset U)h ↔ Form.Promain.Test (PFreeSubset U) 0 h

theorem PFree.Promain.Test.neg_iff {A : GameForm → Prop} [Form.ClosedUnderNeg A] {g h : GameForm} : Form.Promain.Test A (-h) (-g) ↔ Form.Promain.Test A g h

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.

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

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}

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}}

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}

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}

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

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

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

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)