proposition: Theorem reduction : SBTM_HALT ⪯ MMA2_HALTING.
proof: Proof. eapply reduces_transitive. apply SBTM_HALT_to_PCTM_HALT.reduction. eapply reduces_transitive. apply PCTM_HALT_to_BSM_HALTING.reduction. eapply reduces_transitive. apply BSM_to_MMA_HALTING.reduction. apply MMA3_to_MMA2_HALTING.reduction. Qed.
imports: Undecidability.Synthetic(Definitions ReducibilityFacts) Undecidability.TM(SBTM) Undecidability.MinskyMachines(MMA)