proposition: Theorem FSAT_FULL_MONADIC_FSAT_11 : FSAT Σ ⪯ᵢ FSAT (Σ11 (syms Σ) (rels Σ)).
proof: Proof. Proof using HΣ2 HΣ1. apply ireduces_transitive with (Q := FSAT (Σno_props Σ)). + exists (Σrem_props HΣ2 0); intros A. apply exists_equiv; intro; apply Σrem_props_correct. + assert (forall s, ar_syms (Σno_props Σ) s <= 1) as H1. { simpl; auto. } exists (Σrem_constants H1 0); intros A. apply exists_equiv; intro; apply Σrem_constants_correct. 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)