proposition: Theorem ra_univ_ad_spec : ex (⟦ra_univ_ad⟧ (k##vec_nil)) <-> exists φ, forall c, In c lc -> h10uc_sem φ c.
proof: Proof. Proof using Hf_tot. split. + intros (v & Hv). simpl in Hv; red in Hv. destruct Hv as (H1 & H2). destruct (h10luc_sem_dec lc (beta v)) as [ (c & H) | H ]. * assert (⟦ f ⟧ (v ## k ## vec_nil) 1) as C. { apply Hf_val_1; exists c; auto. } generalize (ra_rel_fun _ _ _ _ H1 C); discriminate. * exists (beta v); auto. + intros (phi & Hphi). destruct (godel_beta_fun_inv (h10luc_bound lc) phi) as (a & b & Hab). generalize (h10luc_bound_prop _ _ Hab); clear Hab; intros Hab. apply ra_min_ex; auto. exists (recomp a b); simpl. apply Hf_val_0. intros c Hc; rewrite decomp_l_recomp, decomp_r_recomp; apply Hab; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list crt pos vec) Undecidability.MuRec.Util(recalg ra_utils ra_enum recomp ra_recomp beta ra_godel_beta) Undecidability.DiophantineConstraints(H10C Util.h10c_utils)