proposition: Lemma IB_translate_rec rho phi f e hv : rho_descr_phi rho phi hv -> (rho ⊨ f <-> dom_rel (rho (1+hv)) (rho (2+hv))) -> highest_var_list e < hv -> ((forall c, In c e -> h10upc_sem phi c) -> rho ⊨ f) -> rho ⊨ translate_rec f (S hv) e.
proof: Proof. intros Hrhophi Hsat Hhv H. induction e as [|eh er IH] in H,Hsat,Hhv|-*. - apply H. intros l []. - cbn. intros Hts. apply IH. + easy. + cbn in Hhv. lia. + intros HH. rewrite Hsat. eapply (IB_single_constr (h:=eh)). * exact Hrhophi. * pose proof (@highest_var_list_descr (eh::er) eh ltac:(now left)). lia. * easy. * intros Hsem. rewrite <- Hsat. apply H. intros c [il|ir]. 2:now apply HH. congruence. 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)