proposition: Lemma fsatdc_reduction : reduction (@F_cform) H10UPC_SAT FSATdc.
proof: Proof. intros Hl. unfold F_cform. split. - intros [rho H]. pose (@m Hl rho) as m. exists (model m). exists (model_interp m). exists (fun _ => Num (fN le0)). repeat split. + apply m_listable. + apply m_discrete. + apply m_decidable. + apply (@valid Hl rho H). - intros [D [I [rho [lst [tdisc [tdec H]]]]]]. specialize (tdec tt). destruct lst as [l Hlst]. destruct tdec 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 Hc. apply Hf in Hc. congruence. + exists l. exact Hlst. + exact 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