proposition: Theorem reduction : HaltTM 1 ⪯ iPCPb.
proof: Proof. apply (reduces_transitive HaltTM_1_to_PCP.reduction). apply (reduces_transitive PCP_to_PCPb.reduction). exact PCPb_iff_iPCPb.reductionLR. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.TM.TM Undecidability.PCP.PCP Undecidability.PCP.Reductions.PCP_to_PCPb Undecidability.PCP.Reductions.PCPb_iff_iPCPb