proposition: Lemma translate_constraints_correct : rho ⊨ translate_constraints (h10).
proof: Proof. Proof using D HA1 HA2 HA3 Hφ I h10 rho φ. unfold translate_constraints. pose (S(highest_var_list h10)) as hv. fold hv. pose (S(highest_num φ hv)) as hn. destruct (chain_build hn) as [c]. apply emplace_exists_spec. exists (φ >> c). eapply (@translate_rec_correct hv hn c _ φ _ _). - cbn. easy. - exact Hφ. - unfold hv. lia. - unfold hn. lia. - intros m Hm. destruct (m <? hv) eqn:Heq. + easy. + apply Nat.ltb_ge in Heq. lia. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullSoundness Semantics.Tarski.FullFacts Syntax.BinSig) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Coq(Arith Lia List) Undecidability.Synthetic.Definitions