proposition: Theorem FSAT_in_dec : decidable (@fo_form_fin_dec_SAT_in Σ A X).
proof: Proof. Proof using HΣ2 HΣ1 HX2 HX1. destruct HX1 as ([ | x l ] & Hl). + right; intros (M & _ & _ & rho & _). apply (Hl (rho 0)). + clear l Hl. assert (H : decidable (exists M, @FO_sem _ X M A)). { destruct finite_t_model_upto with (X := X) (ls := fol_syms A) (lr := fol_rels A) (ln := fol_vars A) as (lM & HlM); auto. apply decidable_list_upto_ex with (l := lM) (R := FO_model_equiv (fol_syms A) (fol_rels A) (fol_vars A)); auto. * intros (M & rho & H); simpl; apply fol_sem_dec; auto. * intros ? ? ?; eapply FO_model_equiv_spec. 2-4: apply incl_refl. trivial. } destruct H as [ H | H ]; [ left | right ]. * revert H; apply FSAT_FO_sem_eq; auto. * contradict H; revert H; apply FSAT_FO_sem_eq; auto. Qed.
imports: List Arith Bool Lia Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms fo_logic fo_sat decidable)