proposition: Theorem FSAT_ONE_REL Σ n : (syms Σ -> False) -> (forall r : rels Σ, ar_rels _ r = n) -> finite_t (rels Σ) -> FSAT Σ ⪯ᵢ FSAT (Σone_rel Σ n).
proof: Proof. intros Hs Hn (lr & Hr). exists (Σunif_one_rel Hs Hn); intros A; split. + intros (X & M & H1 & H2 & phi & H3). exists (X + rels Σ)%type, (Σunif_one_rel_model Hn M (phi 0)). exists. { apply finite_t_sum; auto; exists lr; auto. } exists. { intros [] v; vec split v with x; destruct x; simpl; try tauto; apply H2. } exists (fun n => inl (phi n)). revert H3; apply Σunif_one_rel_sound. + intros (X & M' & H1 & H2 & phi & H3). exists X, (Σone_unif_rel_model Hs Hn M'), H1. exists. { intros ? ?; apply H2. } exists phi. revert H3; apply Σunif_one_rel_complete. 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 )