proposition: Lemma m_rel (m:nat) (e : env (model m)) (a b c d : nat) : m > 0 -> e ⊨ rel a b c d <-> exists na ua nb ub nc uc nd ud, (e a) = Num (@fN _ na ua) /\ (e b) = Num (@fN _ nb ub) /\ (e c) = Num (@fN _ nc uc) /\ (e d) = Num (@fN _ nd ud) /\ h10upc_sem_direct ((na,nb),(nc,nd)).
proof: Proof. intros Hm0. split. - cbn -[model_rel P]. intros [pl [pr [[[na [ua [nb [ub [Ha [Hb Hpl]]]]]]%m_P [nc [uc [nd [ud [Hc [Hd Hpr]]]]]]%m_P] Hpp]]]. exists na,ua,nb,ub,nc,uc,nd,ud. split. 2: split. 3:split. 4:split. 1-4:easy. cbn in Hpl,Hpr,Ha,Hb,Hc,Hd. rewrite Hpr,Hpl in Hpp. apply Hpp. - intros [na [ua [nb [ub [nc [uc [nd [ud [Ha [Hb [Hc [Hd Hrel]]]]]]]]]]]]. cbn -[model_rel P]. exists (Pair (fN ua) (fN ub)), (Pair (fN uc) (fN ud)). split. 1:split. 3:easy. + rewrite m_P. exists na,ua,nb,ub. tauto. + rewrite m_P. exists nc,uc,nd,ud. tauto. 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