proposition: Theorem FSATd_undec : undecidable FSATd.
proof: Proof. apply (undecidability_from_reducibility dPCPb_undec). apply (reduces_transitive dPCPb_to_BPCP). eapply reduces_transitive; try apply reduction_disc. eapply reduces_transitive; try apply (@FULL_TRAKHTENBROT_non_informative (Σrel 2)). - left. exists tt. auto. - exists (fun phi => phi). intros phi. apply red_utils.fo_form_fin_dec_SAT_discr_equiv. Qed.
imports: Undecidability.FOL.TRAKHTENBROT(bpcp red_chain_undec_full fo_sig) Undecidability.Synthetic(Undecidability ReducibilityFacts) Undecidability.FOL.Syntax(Core) Undecidability.FOL(FSAT Reductions.FSATd_to_FSATdc Reductions.TRAKHTENBROT_to_FSAT) Undecidability.PCP(PCP_undec)