proposition: Theorem reduction : HaltTM 1 ⪯ fun '(M,t) => @HaltsTM (finType_CS bool) 1 M t.
proof: Proof. unshelve eexists. - intros [Σ M t]. exact (M' M, ts' t). - intros [Σ M t]. now apply HaltTM_Σ_to_HaltTM_bool_correct. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString Undecidability.Synthetic.Definitions