proposition: Theorem reduction : Halt_BSM ⪯ MM2_HALTING.
proof: Proof. apply (reduces_transitive BSM_MM.BSM_MM_HALTING). apply (reduces_transitive MM_FRACTRAN.MM_FRACTRAN_REG_HALTING). apply (reduces_transitive FRACTRAN_to_MMA2.FRACTRAN_REG_MMA2_HALTING). exact MMA2_to_MM2.MMA2_MM2_HALTING. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.MinskyMachines.MM2 Undecidability.StackMachines.BSM