proposition: Lemma m_P m (e : env (model m)) (p a b : nat) : e ⊨ P p a b <-> exists n1 u1 n2 u2, (e a) = Num (@fN _ n1 u1) /\ (e b) = Num (@fN _ n2 u2) /\ (e p) = Pair (@fN _ n1 u1) (@fN _ n2 u2).
proof: Proof. split. - intros [[[[[nl' [ul' [nr' [ur' H1]]]]%m_P' [nl [ul Hl]]%m_N] [nr [ur Hr]]%m_N] H4] H5]. exists nl, ul, nr, ur. split. 2:split. 1-2:easy. rewrite H1. cbn in H4, H5. rewrite H1, Hl in H4. rewrite H1, Hr in H5. subst nl'. subst nr'. f_equal; f_equal; apply le_unique. - intros [nl [ul [nr [ur [Hl [Hr Hp]]]]]]. cbn -[model_rel]. split. 1:split. 1:split. 1:split. + change (e ⊨ P' p). rewrite m_P'. eauto. + change (e ⊨ N a). rewrite m_N. eauto. + change (e ⊨ N b). rewrite m_N. eauto. + cbn. rewrite Hl, Hp. easy. + cbn. rewrite Hr, Hp. easy. Qed.
imports: Vector Undecidability.DiophantineConstraints(H10C Util.H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullSoundness Semantics.Tarski.FullFacts Syntax.BinSig Semantics.FiniteTarski.Full) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Shared.Libs.DLW.Wf(wf_finite) Coq(Arith Lia List) Undecidability.FOL.Semantics.FiniteTarski(Full DoubleNegation) Undecidability.Synthetic(Definitions DecidabilityFacts) Undecidability.Synthetic.Definitions Datatypes Relation_Definitions Setoid Relation_Definitions