proposition: Theorem Sig_rem_cst_dep_red A : { B | @fo_form_fin_dec_SAT Σ A <-> @fo_form_fin_dec_SAT (Σrem_cst Σ) B }.
proof: Proof. Proof using Σ0 Σd. generalize (fol_vars_max_spec A). set (m := fol_vars_max A); intros Hm. destruct (syms_map A) as (g & f & Hfg). set (σ s := g s + S m). exists (encode σ A). split. + intros (X & M & G1 & G2 & phi & G3). exists X, (Σrem_cst_model M), G1. exists. { intros r; simpl; apply G2. } set (psi n := match le_lt_dec (S m) n with | left _ => match f (n - S m) with | Some s => fom_syms M s (cast ø (eq_sym (Σ0 _))) | None => phi 0 end | right _ => phi n end). exists psi. revert G3; apply soundness with (HΣ := Σ0) (ls := fol_syms A); auto. * intros s Hs; unfold σ; intros H. apply Hm in H; lia. * intros n Hn; apply Hm in Hn. unfold psi. destruct (le_lt_dec (S m) n); try lia; auto. * intros s Hs. unfold psi, σ. apply Hfg in Hs. replace (g s + S m - S m) with (g s) by lia. rewrite Hs. destruct (le_lt_dec (S m) (g s + S m)); auto; lia. + intros (X & M' & G1 & G2 & psi & G3). exists X, (Σadd_cst_model M' σ psi), G1. exists. { intros r; simpl; apply G2. } exists psi. revert G3; apply completeness with (ls := fol_syms A); auto. intros s Hs; unfold σ; intros H. apply Hm in H; lia. 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 decidable fol_ops fo_sig fo_terms fo_logic fo_sat)