proposition: Lemma IB_single_constr rho φ (n:nat) (h:h10upc) : rho_descr_phi rho φ n -> highest_var h < n -> rho ⊨ translate_single h (S n) -> (h10upc_sem φ h -> dom_rel (rho (1+n)) (rho (2+n))) -> dom_rel (rho (1+n)) (rho (2+n)).
proof: Proof. intros Hrhophi Hmaxhall. destruct h as [[a b][c d]]. unfold translate_single. cbn in Hmaxhall. intros Htr Hcon. unfold erel in Htr. rewrite IB_Not in Htr. apply Htr. intros p2 p1. apply IB_P_i. cbn. intros na nb Hp1 Ha Hb. apply IB_P_i. cbn. intros nc nd Hp2 Hc Hd. rewrite Hp1, Hp2. intros Habcd. apply Hcon. assert (na = φ a) as ->. 1: pose (@Hrhophi a) as Hp; rewrite Ha in Hp; apply Hp; lia. assert (nb = φ b) as ->. 1: pose (@Hrhophi b) as Hp; rewrite Hb in Hp; apply Hp; lia. assert (nc = φ c) as ->. 1: pose (@Hrhophi c) as Hp; rewrite Hc in Hp; apply Hp; lia. assert (nd = φ d) as ->. 1: pose (@Hrhophi d) as Hp; rewrite Hd in Hp; apply Hp; lia. apply Habcd. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FragmentNDFacts Semantics.Tarski.FragmentSoundness Semantics.Tarski.FragmentFacts Syntax.BinSig Semantics.Kripke.FragmentCore Semantics.Kripke.FragmentSoundness Semantics.Kripke.FragmentToTarski) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Shared(ListAutomation) Coq(Arith Lia List)