proposition: Theorem Σ_noeq_complete : fo_form_fin_dec_SAT (Σ_noeq A) -> fo_form_fin_dec_eq_SAT e H_ae A.
proof: Proof. Proof using HA1 HA2. intros (X & M & H1 & H2 & phi & H5 & H3). apply fol_sem_congruence in H5 as ((H4 & H5) & (H6 & H8 & H7)). set (R x y := fom_rels M e (cast (x ## y ## ø) (eq_sym H_ae))). destruct H1 as (lX & HlX). destruct decidable_EQUIV_fin_quotient with (l := lX) (R := R) as [ n cls repr G1 G2 ]; auto. + intros; apply H2. + intros x; exists x; split; auto; apply H6. + exists (pos n). set (Mn := Mk_fo_model Σ (fun s v => cls (fom_syms M s (vec_map repr v))) (fun r v => fom_rels M r (vec_map repr v))). exists Mn. exists; auto. exists. { intros r v; apply H2. } exists. { intros p q. unfold Mn; simpl. rewrite cast_fun; simpl. unfold R in G2; rewrite G2, !G1; tauto. } exists (fun n => cls (phi n)). revert H3. apply fo_model_projection' with (i := cls) (j := repr) (ls := ls) (lr := lr); auto. * intros s v Hs; simpl; apply G2. rewrite vec_map_map; red. apply H4; auto. intros p; rew vec; apply G2. rewrite G1; auto. * intros r v Hr; simpl. rewrite vec_map_map. apply H5; auto. intros p; rew vec; apply G2. rewrite G1; auto. Qed.
imports: List Arith Lia Relations 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_congruence fo_sat)