proposition: Lemma constr_rel (a b c d : nat) (f:nat -> D) (n:nat) : repr_nums f n -> b <= n -> a <= n -> c <= n -> d <= n -> h10upc_sem_direct ((a,b),(c,d)) -> D_Not (forall pl pr, isPair pl (f a) (f b) -> isPair pr (f c) (f d) -> i_Pr pl pr -> D_wFalse).
proof: Proof. intros Hreprnums Hbn. pose proof Hreprnums as Hrepr_nums. destruct Hreprnums as [Zrepr Hrepr]. induction b as [|b IH] in a,c,d|-*; intros Han Hcn Hdn Habcd. - cbn in Habcd. assert (c = S a /\ d = 0) as [Hc Hd]. 1:lia. rewrite Hc, Hd, !Zrepr in *. destruct (Hrepr a) as [pl [pr [Ha [Hpl Hpr]]]]. 1:lia. intros Hcr. now apply (Hcr pl pr). - destruct (@h10upc_inv a b c d Habcd) as [c' [d' [Habcd' [Hc' Hd']]]]. rewrite <- Hc', <- Hd' in *. assert (h10upc_sem_direct ((d',b),(d'+b+1,d'))) as Hdb. + split. 1: now lia. apply Habcd'. + intros Hcr. apply (IH a c' d'). 1-3: lia. 1: easy. intros pab pc'd' Hpab Hpc'd' Hpabc'd'. apply (IH d' (d'+b+1) d'). 1-3: lia. 1: easy. intros pd'b pd'bd' Hpd'b Hpd'bd' Hpd'bd'bd'. destruct (Hrepr b) as [pb [pb' [Nsb [Hpb [Hpb' Hpbpb']]]]]. 1:lia. destruct (Hrepr c') as [pc [pc' [Nsc [Hpc [Hpc' Hpcpc']]]]]. 1:lia. pose proof (@vF_succ_right valid_in pc' pc pb' pb pd'bd' pd'b pc'd' pab (f (S c')) (f (S b)) (f(d' + b + 1)) (f d') (f c') (f b) (f a)) as sr. apply sr; cbn; fold isNum. 1-5: now destruct Hpab as [H'l [H'r [H'p [H'pl H'pr]]]]. 1-5: now destruct Hpc'd' as [H'l [H'r [H'p [H'pl H'pr]]]]. 1: easy. 1-5: now destruct Hpd'b as [H'l [H'r [H'p [H'pl H'pr]]]]. 1-5: now destruct Hpd'bd' as [H'l [H'r [H'p [H'pl H'pr]]]]. 1: easy. 1-5: now destruct Hpb as [H'l [H'r [H'p [H'pl H'pr]]]]. 1-5: now destruct Hpb' as [H'l [H'r [H'p [H'pl H'pr]]]]. 1: easy. 1-5: now destruct Hpc as [H'l [H'r [H'p [H'pl H'pr]]]]. 1-5: now destruct Hpc' as [H'l [H'r [H'p [H'pl H'pr]]]]. 1: easy. intros pScsum paSb HpaSb H'a H'Sb HlpaSb HrpaSb HpScsum H'Sc H'dsum HlpScsum HrpScsum Hprel. apply (Hcr paSb pScsum). all: now repeat split. 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.FOL.Reductions(H10UPC_to_FOL_minimal H10UPC_to_FOL_constructions) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Synthetic(Definitions) Coq(Arith Lia List)