proposition: Theorem PCPb_MM_HALTING : PCPb ⪯ Halt_MM.
proof: Proof. eapply reduces_transitive. exact PCPb_iff_iPCPb.reductionLR. eapply reduces_transitive. exact iPCPb_to_BSM_HALTING. apply BSM_MM_HALTING. 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)