proposition: Theorem reduction : HaltTM 1 ⪯ SysF_INH.
proof: Proof. apply (reduces_transitive HaltTM_1_to_FRACTRAN_HALTING.HaltTM_to_FRACTRAN_HALTING). apply (reduces_transitive FRACTRAN_DIO.FRACTRAN_HALTING_DIO_LOGIC_SAT). apply (reduces_transitive FRACTRAN_DIO.DIO_LOGIC_ELEM_SAT). apply (reduces_transitive FRACTRAN_to_H10C_SAT.DIO_ELEM_H10C_SAT). exact H10C_SAT_to_SysF_INH.reduction. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.TM.TM Undecidability.SystemF.SysF