proposition: Theorem finsat_reduction_1 R : dPCPb R -> FSATd (finsat_formula R).
proof: Proof. intros H. - apply BPCP_P in H as [n [s H]]. exists (obstring n), (@FIB R n), (fun _ => None). split; try apply listable_obstring. cbn. split. 2:split. 2: apply signature_is_decidable. 1: { exists (fun '(a,b) => if obstring_eqdec a b then true else false). intros [a b]. destruct (obstring_eqdec a b) as [Ht|Hf]; now split. } rsplit 17. + apply (@FIB_HP R). + apply FIB_HS1. + apply FIB_HS2. + intros x. apply (@FIB_HF1 R _ true x). + intros x. apply (@FIB_HF1 R _ false x). + intros x y H1 H2. now destruct (FIB_HF2 (R:=R) H1 H2). + intros x y H1 H2. now destruct (FIB_HF2 (R:=R) H1 H2). + apply (@FIB_HF2' R). + intros x. apply (@FIB_HF3 R _ true x). + intros x. apply (@FIB_HF3 R _ false x). + intros u v [[a[b[H1 H2]]]|[a[b[a'[b'[H1 H2]]]]]] % (@FIB_HI R _ u v); apply list_or_spec. * exists (ax_HI' (a/b)). split; try now apply in_map. left. cbn. now rewrite !tprep_eval. * exists (ax_HI' (a/b)). split; try now apply in_map. right. exists a', b'. cbn. rewrite !tprep_eval. tauto. + congruence. + congruence. + congruence. + congruence. + congruence. + congruence. + try now exists s. 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