proposition: Theorem FSAT_REL2_to_FUNnREL1 n : 2 <= n -> FSAT (Σrel 2) ⪯ᵢ FSAT (Σn1 n).
proof: Proof. intros Hn; destruct n as [ | [ | n ] ]; try (exfalso; lia); clear Hn. exists (Σ2_ΣSSn1_enc n); intros A; split. + intros (X & M2 & H1 & H2 & phi & H3). apply Σ2_ΣSSn1_enc_sound with (1 := H3); auto. + intros (Y & M21 & H1 & H2 & psi & H3). apply Σ2_ΣSSn1_enc_complete with (2 := H3); auto. 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 )