proposition: Theorem FULL_MONADIC_discernable (Σ : fo_signature) : { _ : forall u v : syms Σ, decidable (u ≢ v) & { _ : forall u v : rels Σ, decidable (u ≢ v) | (forall s, ar_syms Σ s <= 1) /\ (forall r, ar_rels Σ r <= 1) } } + { _ : forall u v : rels Σ, decidable (u ≢ v) | forall r, ar_rels Σ r = 0 } -> forall A, decidable (FSAT Σ A).
proof: Proof. intros [ (H1 & H2 & H3 & H4) | (H1 & H2) ]. + apply FSAT_FULL_MONADIC_discernable; auto. + apply FSAT_PROP_ONLY_discernable; auto. Qed.
imports: List Arith Undecidability.Synthetic(Definitions ReducibilityFacts InformativeDefinitions InformativeReducibilityFacts) Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils decidable discernable fol_ops fo_sig fo_terms fo_logic fo_sat fo_sat_dec red_utils Sig_Sig_fin Sig_rem_props Sig_rem_constants Sig0 Sig1 Sig1_1 Sig_discernable)