proposition: Theorem PCPb_MM_HALTS_ON_ZERO : PCPb ⪯ MM_HALTS_ON_ZERO.
proof: Proof. eapply reduces_transitive. exact PCPb_iff_iPCPb.reductionLR. eapply reduces_transitive. exact iPCPb_to_BSM_HALTING. apply BSM_MM_HALTS_ON_ZERO. Qed.
imports: Undecidability.Synthetic(Definitions ReducibilityFacts) Undecidability.PCP(PCP PCPb_iff_iPCPb) Undecidability.StackMachines(BSM iPCPb_to_BSM_HALTING) Undecidability.MinskyMachines(MM MM_sss BSM_MM)