proposition: Theorem FSAT_Σ11_DEC : decidable (FSAT _ A).
proof: Proof. Proof using HP2 HP1. destruct FSAT_MONADIC_11_FSAT_MONADIC_1 with (n := n) (1 := HP1) as (f & Hf). specialize (Hf A). destruct FSAT_MONADIC_DEC with (A := f A) as [ H | H ]; simpl; auto; try easy. + left; revert H; apply Hf. + right; contradict H; revert H; apply Hf. 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)