proposition: Lemma translate_single_correct (e:env D) (h10v : h10upc) zz n f : zz > highest_var h10v -> chain m n f -> (forall k, rho' k = e (k+zz)) -> e ⊨ translate_single h10v zz -> h10upc_sem (fun k => chain_env f (e k)) h10v.
proof: Proof. Proof using vTrans vSucc vDescr2 vDescr rho fini decP Hrho. destruct h10v as [[a b][c d]]. intros Hv ch Hrhok [[[[Hrel Ha] Hb] Hc] Hd]. rewrite ! to_leq in Ha,Hb,Hc,Hd. pose proof Hrhok 0 as Hrho0. cbn in Hrho0. rewrite <- Hrho0 in Ha,Hb,Hc,Hd. rewrite Hrho in Ha,Hb,Hc,Hd. cbn in Ha,Hb,Hc,Hd. rewrite to_rel in Hrel. destruct (chain_proves ch Hb Hrel) as [na [nb [nc [nd [Hsem [Hna [Hnb [Hnc Hnd]]]]]]]]. 1-3: easy. unfold h10upc_sem, chain_env. rewrite !Hna,!Hnb,!Hnc,!Hnd. cbn in Hsem. cbn. nia. 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