proposition: Theorem FSAT_ΣP1_dec n V (A : fol_form (ΣP1 V n)) : (V -> False) -> decidable (fo_form_fin_dec_SAT A).
proof: Proof. intros HV. assert (H : decidable (exists P : vec bool n -> bool, fo_form_fin_dec_SAT_in A (sig (fun v => P v = true)))). { apply ex_fun_bool_decidable. + apply finite_t_vec, finite_t_bool. + intros v w; apply vec_eq_dec, bool_dec. + intros P Q H; apply FSAT_in_ext; intro; rewrite H; tauto. + intro; apply FSAT_in_dec; simpl. * intros s; destruct (HV s). * red; apply pos_eq_dec. * apply finite_t_sig_bool, finite_t_vec, finite_t_bool. * intros (x & Hx) (y & Hy). destruct (vec_eq_dec bool_dec x y) as [ H | H ]. - subst; left; f_equal; apply eq_bool_pirr. - right; contradict H; inversion H; auto. } destruct H as [ H | H ]. + left. destruct H as (P & HP). exists { v | P v = true }; auto. + right; intros (X & HX). apply H, Monadic_model_bounded; auto; exists X; 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 fo_sat_dec)