proposition: Lemma translate_list_correct (e:env D) zz n f : zz > highest_var_list h10 -> chain m n f -> (forall k, rho' k = e (k+zz)) -> e ⊨ translate_list zz h10 -> forall h10v, In h10v h10 -> h10upc_sem (fun k => chain_env f (e k)) h10v.
proof: Proof. Proof using vTrans vSucc vDescr2 vDescr rho fini decP Hrho. intros Hv ch Hrhok Hl h10v. induction h10 as [|h10x h10r IH] in Hl,Hrhok,ch,Hv|-*. - intros []. - destruct Hl as [Hl1 Hl2]. intros [Hin|Hr]. + subst h10x. apply (@translate_single_correct e h10v zz n f). 2-4:easy. cbn in Hv. lia. + apply IH. 2-5:easy. cbn in Hv. lia. Qed.
imports: Vector Undecidability.DiophantineConstraints(H10C Util.H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullSoundness Semantics.Tarski.FullFacts Syntax.BinSig Semantics.FiniteTarski.Full) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Shared.Libs.DLW.Wf(wf_finite) Coq(Arith Lia List) Undecidability.FOL.Semantics.FiniteTarski(Full DoubleNegation) Undecidability.Synthetic(Definitions DecidabilityFacts) Undecidability.Synthetic.Definitions Datatypes Relation_Definitions Setoid Relation_Definitions