proposition: Theorem BSM_undec : undecidable Halt_BSM.
proof: Proof. apply (undecidability_from_reducibility iPCPb_undec). apply iPCPb_to_BSM_HALTING. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.PCP(PCP PCP_undec) Undecidability.StackMachines(BSM iPCPb_to_BSM_HALTING BSM_sss)