proposition: Lemma HaltTM_1_to_iPCPb : HaltTM 1 ⪯ iPCPb.
proof: Proof. repeat (eapply reduces_transitive; [eapply HaltTM_1_chain_iPCPb | try now eapply reduces_reflexive]). Qed.
imports: List Undecidability.Shared.Libs.DLW(utils) Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.TM.TM Undecidability.StringRewriting(SR) Undecidability.PCP(PCP) Undecidability.TM(SBTM)