proposition: Lemma H10p_to_PA2_standard_model_sat e : H10p e <-> Standard_Model ⊨ encode_problem e.
proof: Proof. split. - destruct e as [p q]; cbn; intros [alpha H]; hnf. eapply exists_n_sat_1. + now apply (sat_encoding alpha (empty_PA2_env _)). + repeat split; apply polynomial_first_order. + apply exists_n_bounded. apply (encoding_closed (p, q)). - destruct e as [p q]; unfold H10p; cbn. intros H. specialize (H (empty_PA2_env Standard_Model)). apply exists_n_sat_2 in H. + destruct H as [sigma H]. exists (get_indi sigma). apply (sat_encoding _ sigma). eapply sat_ext. 2: apply H. easy. + repeat split; apply polynomial_first_order. + apply exists_n_bounded. apply (encoding_closed (p, q)). Qed.
imports: PeanoNat Lia Vector List Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski PA2_facts PA2_categoricity) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.H10(H10p) Undecidability.Shared.Dec