proposition: Theorem reduction : HaltTM 1 ⪯ CM1_HALT.
proof: Proof. apply (reduces_transitive HaltTM_to_FRACTRAN_REG_HALTING). apply (reduces_transitive FRACTRAN_REG_MMA2_HALTING). apply (reduces_transitive MMA2_MM2_HALTING). exact MM2_HALTING_to_CM1_HALT.reduction. Qed.
imports: Undecidability.Synthetic(Definitions ReducibilityFacts) Undecidability.TM.TM Undecidability.FRACTRAN.Reductions.HaltTM_1_to_FRACTRAN_HALTING Undecidability.MinskyMachines(FRACTRAN_to_MMA2 MMA2_to_MM2) Undecidability.CounterMachines(CM1 MM2_HALTING_to_CM1_HALT)