proposition: Lemma H10_enumerable : L_enumerable (fun '(p1, p2) => exists L, eval p1 L = eval p2 L).
proof: Proof. eapply L_enumerable_ext. eapply projection with (Y := list nat). instantiate (1 := fun '( (p1,p2), L) => eval p1 L = eval p2 L). 2:{ intros []. firstorder. } eapply L_enumerable_enum. exists (fix L n := match n with 0 => [] | S n => L n ++ filter test_eq (list_prod (list_prod (L_poly n) (L_poly n)) (T_list_nat n)) end)%list. repeat split. - extract. - eauto. - destruct x as [[p1 p2] L]. intros. destruct (enum_poly p1) as [m1], (enum_poly p2) as [m2], (enumerator__T_list opt_to_list _ L) as [m3]. exists (1 + m1 + m2 + m3). in_app 2. fold plus. eapply filter_In. split. + rewrite !in_prod_iff. repeat split; eapply cum_ge'; try eassumption; eauto; lia. + unfold test_eq. edestruct (Nat.eqb_spec (eval p1 L) (eval p2 L)); eauto. - destruct x as [[p1 p2] L]. intros [m]. induction m. + inv H. + eapply in_app_iff in H as [|]. * eauto. * eapply filter_In in H as []. unfold test_eq in H0. destruct (Nat.eqb_spec (eval p1 L) (eval p2 L)); easy. 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