proposition: Lemma reduction : HaltL ⪯ HaltTM 5.
proof: Proof. apply (reduces_transitive HaltL_to_HaltLclosed.reduction). apply (reduces_transitive HaltLclosed_to_wCBNclosed.reduction). apply (reduces_transitive wCBNclosed_to_KrivineMclosed_HALT.reduction). apply (reduces_transitive KrivineMclosed_HALT_to_MMA_HALTING.reduction). exact MMA_HALTING_n_to_HaltTM_n.reduction. Qed.
imports: Undecidability(L.L TM.TM Synthetic.Definitions Synthetic.ReducibilityFacts)