proposition: Lemma chain_proves_P_High (h:nat) (c:chain h) (i:nat) A f : h > 0 -> i < h -> incl (chain_exists c) A -> A ⊢I P (findPairHigh c (S i)) (findNum c (S i)) 0 f -> A ⊢I f.
proof: Proof. intros Hh Hi HA Hpf. unfold P in Hpf. destruct (@chain_lower (S i) _ c) as [cc Hcc]. 1-2:lia. pose proof (@chain_exists_lower (S i) h cc c ltac:(lia)) as Hlower. eapply IE. 1:eapply IE. 1:eapply IE. 1:eapply IE. 1:eapply IE. 1: unfold findPairHigh, findNum in Hpf; apply Hpf. all: apply Ctx, HA. 3: { pose proof (@chain_proves_N h c 0) as H0. unfold findNum in H0. rewrite chainData_0 in H0. apply H0. lia. } all: rewrite Hcc; [apply Hlower; [intros k Hk;symmetry;now apply Hcc|idtac]|lia]. 2: apply chain_proves_N; lia. all: destruct (chain_inversion cc) as [[[[n pl] ph] ch'] Hch]; subst cc; cbn [chain_exists chainData]. - do 2 right. left. destruct (Dec _); [easy|lia]. - do 6 right. left. destruct (Dec _); [easy|lia]. - do 5 right. left. destruct (Dec _); [easy|lia]. 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)