proposition: Lemma fval_reduction : reduction (fun k => @F k → falsity) (fun l => ~ (H10UPC_SAT l)) FVAL.
proof: Proof. intros Hl. split. - intros Hc D I rho [lst tdec] H. apply Hc. destruct lst as [l Hlst]. destruct (tdec tt) as [f Hf]. apply (@F_correct Hl D I rho). + intros a b. cbn. destruct (f (Vector.cons D a 1 (Vector.cons D b 0 (Vector.nil D)))) as [|] eqn:Hdec. * left. now apply Hf. * right. intros Hc1. apply Hf in Hc1. congruence. + exists l. exact Hlst. + exact H. - intros Hc [rho H]. pose (@m Hl rho) as m. specialize (Hc (model m)). specialize (Hc (model_interp m)). specialize (Hc (fun _ => Num (fN le0))). apply Hc. 1: split. + apply m_listable. + apply m_decidable. + apply (@valid Hl rho H). 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