proposition: Lemma IB_aux_transport rho : rho_canon rho -> rho ⊨ translate_constraints h10 -> H10UPC_SAT h10.
proof: Proof. intros (Hrho0&Hrho1&Hrho2). pose ((S (highest_var_list h10))) as h10vars. unfold translate_constraints. fold h10vars. intros H. cbn in H. rewrite Hrho1, Hrho2 in H. apply H. 2:easy. apply IB_emplace_forall. intros f. pose (fun n => match (f n) with (Num k) => k | _ => 0 end) as phi. eapply (IB_translate_rec (e:=h10) (hv:=h10vars) (phi:= phi)). - intros x HH. destruct (Nat.ltb_lt x h10vars) as [_ Hr]. rewrite Hr. 2:easy. unfold phi. now destruct (f x). - split. 2:split. all: rewrite less_ge; [|lia]. 1: rewrite <- Hrho0. 2: rewrite <- Hrho1. 3: rewrite <- Hrho2. all: f_equal; lia. - cbn -[dom_rel' Nat.leb Nat.sub]. easy. - lia. - intros HG. cbn -[dom_rel' Nat.leb Nat.sub]. destruct (Nat.ltb_ge (S h10vars) h10vars) as [_ H1]. rewrite H1. 2:lia. destruct (Nat.ltb_ge (S (S h10vars)) h10vars) as [_ H2]. rewrite H2. 2:lia. assert (S h10vars-h10vars = 1) as ->. 1:lia. assert (S(S h10vars)-h10vars = 2) as ->. 1:lia. rewrite Hrho1, Hrho2. cbn. exists phi. easy. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Utils.FriedmanTranslationFragment 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) Coq(Arith Lia List) Undecidability.FOL.Reductions(H10UPC_to_FOL_constructions)