proposition: Theorem FSAT_MONADIC_DEC : decidable (FSAT _ A).
proof: Proof. Proof using H2 H1. destruct Sig_discrete_to_pos with (A := A) as (n & m & i & j & B & HB). + simpl; intros s; destruct (H1 s). + apply H2. + assert (n = 0) as ->. { destruct n; auto. destruct (H1 (i pos0)). } simpl in *. destruct FSAT_ΣP1_dec with (V := pos 0) (A := B) as [ H | H ]. * intros p; invert pos p. * left; apply HB; auto. * right; rewrite HB; 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)