proposition: Lemma IB_emplace_exists rho n i : rho ⊨ emplace_exists n i -> (exists f, (fun k => if k <? n then f (k) else rho (k-n)) ⊨ i).
proof: Proof. unfold emplace_exists. intros H. induction n as [|n IH] in rho,H|-*. - cbn. exists (fun _ => Num 0). eapply (sat_ext IB (rho:=rho) (xi:=fun k => rho(k-0))). 2: easy. intros x. now rewrite Nat.sub_0_r. - cbn in H. destruct H as (d&Hd). specialize (IH (d.:rho) Hd). destruct IH as [f Hf]. exists (fun kk => if kk =? n then d else f kk). eapply (sat_ext IB (xi:=fun k => if k <? n then f k else (d .: rho) (k - n))). 2: easy. intros x. destruct (Nat.eq_dec x n) as [Hxn|Hnxn]. + destruct (Nat.ltb_ge x n) as [_ Hlt]. rewrite Hlt. 2:lia. clear Hlt. destruct (Nat.ltb_lt x (S n)) as [_ Hlt]. rewrite Hlt. 2:lia. clear Hlt. cbn. assert (x-n=0) as ->. 1: lia. cbn. destruct (Nat.eqb_eq x n) as [_ HH]. now rewrite HH. + destruct (x <? n) eqn:Hneq. * destruct (Nat.ltb_lt x n) as [Hlt _]. apply Hlt in Hneq. clear Hlt. destruct (Nat.ltb_lt x (S n)) as [_ Hlt]. rewrite Hlt. 2:lia. clear Hlt. cbn. destruct (Nat.eqb_neq x n) as [_ HH]. rewrite HH. 1: easy. lia. * destruct (Nat.ltb_ge x n) as [Hlt _]. apply Hlt in Hneq. clear Hlt. destruct (Nat.ltb_ge x (S n)) as [_ Hlt]. rewrite Hlt. 2:lia. clear Hlt. assert (x-n=S(x-S n)) as ->. 1:lia. easy. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullSoundness Semantics.Tarski.FullFacts Syntax.BinSig) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Coq(Arith Lia List) Undecidability.Synthetic.Definitions