proposition: Theorem FSATd_reduction R : dPCPb R <-> FSATd (finsat_formula R).
proof: Proof. split; intros H. 1: now apply finsat_reduction_1. destruct H as (D & I & rho & Hlis & Hdis & HH). apply finsat_reduction_2. exists D, I, rho. now split. Qed.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation