proposition: Lemma IB_F_succ_right rho : rho_canon rho -> rho ⊨ F_succ_right.
proof: Proof. intros H0. unfold F_succ_right. intros p1 p2 p3 p4 p5 p6 p7 p8 a' y' c b a y x. apply IB_rel_i. cbn. intros [nx [ny [na [nb [Hp8 [Hp7 [Hx [Hy [Ha [Hb [Hr1l Hr1r]]]]]]]]]]]. apply IB_rel_i. cbn. intros [nb' [ny' [nc [nb'' [Hp6 [Hp5 [Hb' [Hy' [Hc [Hb'' [Hr2l Hr2r]]]]]]]]]]]. apply IB_rel_i. cbn. intros [ny'' [z [n'y [z' [Hp4 [Hp3 [Hy'' [Hz [H'y [Hz' [Hr3l Hr3r]]]]]]]]]]]. apply IB_rel_i. cbn. intros [na' [z'' [n'a [z''' [Hp2 [Hp1 [Ha' [Hz'' [H'a [Hz''' [Hr4l Hr4r]]]]]]]]]]]. unfold erel. cbn. rewrite IB_Not. intros H. rewrite H0 in *. specialize (H (Pair n'a (nc)) (Pair nx n'y)). eapply IB_P_e in H. 2-4: easy. 2: exists nx, n'y; cbn; firstorder. eapply IB_P_e in H. 2-4: easy. 2: exists n'a, nc; cbn; firstorder. cbn in H. rewrite IB_wFalse in H. apply H. assert (z=0 /\ z' = 0 /\ z'' = 0 /\ z''' = 0) as [Hz0 [Hz01 [Hz02 Hz03]]]. 1:firstorder;congruence. cbn -[dom_rel] in H. rewrite Hz0, Hz01, Hz02, Hz03 in *. split. - assert (ny'' = ny /\ na' = na) as [HHy HHa]. 1:firstorder;congruence. lia. - assert (nb' = nb /\ ny' = ny /\ ny'' = ny /\ na'=na) as [HHb [HHy [HHHy HHa]]]. 1:firstorder;congruence. 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)