proposition: Theorem finsat_reduction_2 R : FSAT (finsat_formula R) -> dPCPb R.
proof: Proof. intros H. - destruct H as (D & (I & rho & HF & HE & (((((((((((((((((H1 & H2) & H3) & H4) & H5) & H6) & H7) & H8) & H9) & H10) & H11) & H12) & H13) & H14) & H15) & H16) & H17) & s & H18))). cbn in *. eapply P_BPCP with (x:=s); trivial; unfold not in *; cbn in *. + intros [|]. apply H4. apply H5. + intros [|] [|] d1 d2 Hi1 Hi2. 1: split; try easy; now apply H6. 3: split; try easy; now apply H7. all: exfalso. 2: apply H13 in Hi2. all: destruct (H8 _ _ Hi2) as [Hi3 Hi4]. all:easy. + intros [|]. apply H9. apply H10. + intros d1 d2 [|]. apply H15. apply H16. + cbn in H11. intros x y H. specialize (H11 x y H). apply list_or_spec in H11 as [c[[[u v][<- HR]] % in_map_iff [H'|[a[b H']]]]]. * left. exists u, v. split; trivial. cbn in H'. rewrite !tprep_eval in H'. apply H'. * right. exists u, v, a, b. split; trivial. cbn in H'. rewrite !tprep_eval in H'. tauto. 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