proposition: Lemma translate_rec_correct hv hn (cc:chain hn) (h:list h10upc) phi f rho' : rho' ⊨ f -> (forall k, In k h -> h10upc_sem phi k) -> highest_var_list h < hv -> highest_num phi hv < hn -> rho_descr_chain rho' phi cc hv -> rho' ⊨ translate_rec f (S hv) h.
proof: Proof. Proof using D HA3 I rho. intros Hf Hsat Hhv Hhn Hc. induction h as [|[[a b][c d]] hr IH] in Hhv,Hsat|-*. - cbn. easy. - cbn -[erel]. cbn in Hhv. split. + rewrite ierel_spec. 2-5:rewrite Hc; [easy|lia]. apply chain_proves. 1: eapply (Hsat ((a,b),(c,d))); now left. all: match goal with |- ?phi ?a < ?hn => enough (phi a <= highest_num phi hv) by lia end. all: apply highest_num_descr. all:lia. + apply IH. * intros x Hx. apply Hsat. now right. * 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