proposition: Lemma F_correct : rho ⊨ F -> H10UPC_SAT h10.
proof: Proof. Proof using fini decP. intros [z [m [[[[[vpTrans vpPred] vpSucc] vpDescr] vpDescr2] [rho2 [Hlist Hrho]]%remove_emplace_exists]]]. assert (H10UPC_SAT h10 \/ iN m) as [Hl|Nm]. - destruct h10 as [|h10v h10r]. 1:left;exists (fun _ => 0); intros k []. right. destruct Hlist as [Hr _]. destruct h10v as [[ha hb][hc hd]]. cbn in Hr. rewrite ! to_leq in Hr. destruct Hr as [_ [_ [Hr _]]]. specialize (Hrho 0). cbn in Hrho. congruence. - easy. - destruct (@mkchain m z (m.:z.:rho) eq_refl vpTrans vpPred vpSucc m Nm) as [n [f c]]. exists (fun k => chain_env f (rho2 k)). apply (@translate_list_correct m z (m.:z.:rho) eq_refl vpTrans vpSucc vpDescr vpDescr2 rho2 (S(highest_var_list h10)) n f ltac:(lia)). all:easy. 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