proposition: Lemma nat_sat : forall E rho, sat interp_nat rho (embed_problem E) <-> H10p_sem E rho.
proof: Proof. intros E rho. split. - destruct E as [a b]. unfold H10p_sem. cbn. now rewrite !nat_eval_poly. - intros. eapply (@sat_ext _ _ _ _ _ (rho >> @iμ nat interp_nat)). intros x. change ((rho >> iμ) x) with (@iμ nat interp_nat (rho x)). induction (rho x). reflexivity. cbn. now rewrite IHn. eapply problem_to_model. apply nat_is_FA_model. assumption. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullFacts Semantics.Tarski.FullSoundness) Undecidability.FOL.PA Undecidability.FOL.Arithmetics(TarskiFacts DeductionFacts NatModel) Undecidability.H10(H10p) List Lia