proposition: Theorem FULL_TRAKHTENBROT Σ : { r | 2 <= ar_rels Σ r } + { f : _ & { r | 2 <= ar_syms Σ f /\ ar_rels Σ r = 1 } } -> BPCP_problem ⪯ᵢ FSAT Σ.
proof: Proof. intros H. apply ireduces_transitive with (1 := BPCP_Sig2). revert H; intros [ (r & Hr) | (f & r & Hf & Hr) ]. + apply ireduces_transitive with (1 := FSAT_REL_2ton Hr). apply FSAT_RELn_ANY with (1 := eq_refl). + apply ireduces_transitive with (1 := FSAT_REL2_to_FUNnREL1 Hf). apply FSAT_FUNnREL1_ANY with f r; auto. Qed.
imports: List Arith Bool Lia Eqdep_dec Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.Synthetic.InformativeDefinitions Undecidability.Synthetic.InformativeReducibilityFacts Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.Shared.Libs.DLW.Wf(wf_finite) Undecidability.FOL.TRAKHTENBROT(notations utils decidable bpcp fo_sig fo_terms fo_logic fo_sat red_utils Sig_discrete BPCP_SigBPCP Sig_rem_syms Sig_uniform Sig_one_rel Sig_rem_cst Sign_Sig2 Sig2_Sign Sign_Sig Sig_Sig_fin Sig2_SigSSn1 Sign1_Sig )