proposition: Theorem FINITARY_TO_BINARY : FSAT Σ ⪯ᵢ FSAT (Σrel 2).
proof: Proof. Proof using max_syms max_rels HΣ4 HΣ3 HΣ2 HΣ1. destruct max_syms as (ns & Hns). destruct max_rels as (nr & Hnr). set (m := lmax (2::(S ns)::nr::nil)). eapply ireduces_transitive. { apply FSAT_Σnosyms; auto. } eapply ireduces_transitive. { apply FSAT_UNIFORM with (n := m). intros [ [] | [] ]. + apply lmax_prop; simpl; auto. + apply Nat.le_trans with (S ns). * simpl; apply le_n_S, Hns. * apply lmax_prop; simpl; auto. + apply Nat.le_trans with nr. * simpl; auto. * apply lmax_prop; simpl; auto. } eapply ireduces_transitive. { apply FSAT_ONE_REL; simpl; auto; intros []. } eapply ireduces_transitive. { apply FSAT_NOCST; simpl; auto. } apply (FSAT_REL_nto2 (S m)). 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 )