proposition: Theorem reduction : HaltTM 1 ⪯ SysF_TYP.
proof: Proof. apply (reduces_transitive HaltTM_1_to_CSSM_UB.reduction). apply (reduces_transitive CSSM_UB_to_SSemiU.reduction). apply (reduces_transitive SSemiU_to_RU2SemiU.reduction). apply (reduces_transitive RU2SemiU_to_LU2SemiU.reduction). exact LU2SemiU_to_SysF_TYP.reduction. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.TM.TM Undecidability.SystemF.SysF