proposition: Lemma IB_aux_transport rho : rho 0 = Num 0 -> rho ⊨ translate_constraints h10 -> H10UPC_SAT h10.
proof: Proof. intros Hrho0. pose ((S (highest_var_list h10))) as h10vars. unfold translate_constraints. fold h10vars. intros H. apply IB_emplace_exists in H. destruct H as [f Hf]. pose (fun n => match (f n) with (Num k) => k | _ => 0 end) as phi. exists phi. unshelve eapply (IB_translate_rec (e:=h10) (hv:=h10vars) (phi:= phi) _ _ Hf). - intros x HH. destruct (Nat.ltb_lt x h10vars) as [_ Hr]. rewrite Hr. 2:easy. unfold phi. now destruct (f x). - lia. 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