proposition: Lemma iP_spec rho' k l r dk dl dr : rho' k = dk -> rho' l = dl -> rho' r = dr -> rho' ⊨ P k l r <-> iP dk dl dr.
proof: Proof. intros H1 H2 H3. unfold P,iP. erewrite <- !iPr_spec, <- !iN_spec, <- iP'_spec. 1:cbn;reflexivity. all:easy. 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