$\operatorname{pf}(\mathcal{E})$ embeds in $\operatorname{pf}(\mathcal{B})$

Every short dead-ending form is short blocking, and on forms of $\operatorname{pf}(\mathcal{E})$ comparison modulo $\operatorname{pf}(\mathcal{E})$ and modulo $\operatorname{pf}(\mathcal{B})$ agree (misereGE_pfree_iff_of_subset), so the quotient of $\operatorname{pf}(\mathcal{E})$ embeds in the quotient of $\operatorname{pf}(\mathcal{B})$ as an ordered monoid. Since every end of $\operatorname{pf}(\mathcal{B})$ is an integer (PFreeBlocking.isEnd_exists_intCast_misereEQ), the embedding is onto (exists_pfreeDeadEnding_misereEQ), so the two quotients are isomorphic.

The main results are

• misereGE_pfreeDeadEnding_iff_pfreeBlocking
• misereEQ_pfreeDeadEnding_iff_pfreeBlocking
• exists_pfreeDeadEnding_misereEQ

theorem PFree.shortBlocking_of_shortDeadEnding {g : GameForm} (h_g : Form.DeadEnding.ShortDeadEnding g) : Form.ShortBlocking g

theorem PFree.pfreeBlocking_of_pfreeDeadEnding {g : GameForm} (h_g : PFreeDeadEnding g) : g.PFreeBlocking

theorem PFree.misereGE_pfreeDeadEnding_iff_pfreeBlocking {g h : GameForm} (h_g : PFreeDeadEnding g) (h_h : PFreeDeadEnding h) : g ≥m PFreeDeadEnding h ↔ g ≥m GameForm.PFreeBlocking h

theorem PFree.misereEQ_pfreeDeadEnding_iff_pfreeBlocking {g h : GameForm} (h_g : PFreeDeadEnding g) (h_h : PFreeDeadEnding h) : g =m PFreeDeadEnding h ↔ g =m GameForm.PFreeBlocking h

@[irreducible]

theorem PFree.exists_pfreeDeadEnding_misereEQ {g : GameForm} (h_g : g.PFreeBlocking) : ∃ (h : GameForm), PFreeDeadEnding h ∧ g =m GameForm.PFreeBlocking h

Every form of $\operatorname{pf}(\mathcal{B})$ is equivalent modulo $\operatorname{pf}(\mathcal{B})$ to a form of $\operatorname{pf}(\mathcal{E})$: ends are integers, and in a non-end every option can be replaced by an equivalent dead-ending form.