proposition: Lemma iBPCP_chain_MM : iPCPb ⪯ Halt_BSM /\ Halt_BSM ⪯ MM_HALTS_ON_ZERO.
proof: Proof. msplit 1. + apply iPCPb_to_BSM_HALTING. + apply BSM_MM_HALTS_ON_ZERO. Qed.
imports: List Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.Shared.Libs.DLW(utils) Undecidability.PCP(PCP) Undecidability.StackMachines(BSM iPCPb_to_BSM_HALTING) Undecidability.MinskyMachines(MM BSM_MM MM_sss)