proposition: Theorem H10_converges : H10 ⪯ converges.
proof: Proof. eapply reduces_transitive. eapply red. eapply L_enumerable_halt. 2: eapply H10_enumerable. exists (fun '( (p1, p2), (p1', p2')) => poly_eqb p1 p1' && poly_eqb p2 p2'). split. - econstructor. extract. - intros ( (p1, p2), (p1', p2')). destruct (poly_eqb_spec p1 p1'), (poly_eqb_spec p2 p2'); cbn; firstorder congruence. Qed.
imports: Undecidability.H10(H10 dio_single dio_logic) Undecidability.PCP.Util.PCP_facts Undecidability.Shared.Libs.PSL.FiniteTypes Undecidability.L.Datatypes(LNat LProd) Undecidability.L(Tactics.LTactics Computability.MuRec Computability.Synthetic Tactics.GenEncode) Undecidability.Shared.Libs.DLW.Vec(pos) Undecidability.L.Datatypes.List(List_basics List_extra) Nat Datatypes