proposition: Theorem fo_model_simulation A φ ψ : fol_syms A ⊑ ls -> fol_rels A ⊑ lr -> (forall n, n ∊ fol_vars A -> φ n ⋈ ψ n) -> ⟪A⟫ φ <-> ⟪A⟫' ψ.
proof: Proof. revert φ ψ. induction A as [ | r v | b A HA B HB | q A HA ]; intros phi psi Hs1 Hr1 Hp; simpl; try tauto. + apply (fos_rels R). * apply Hr1; simpl; auto. * intros p; do 2 rewrite vec_pos_map. apply fo_term_simulation. - intros n Hn; apply Hp; simpl. apply in_flat_map. exists (vec_pos v p); split; auto. apply in_vec_list, in_vec_pos. - apply incl_tran with (2 := Hs1). intros s' Hs'; simpl. apply in_flat_map. exists (vec_pos v p); split; auto. apply in_vec_list, in_vec_pos. + apply fol_bin_sem_ext; [ apply HA | apply HB ]. 3,6: intros; apply Hp; simpl; apply in_or_app; auto. 1,3: apply incl_tran with (2 := Hs1); intros ? ?; apply in_or_app; auto. 1,2: apply incl_tran with (2 := Hr1); intros ? ?; apply in_or_app; auto. + destruct q; simpl; split. 1: intros (x & Hx); destruct (fos_total R x) as (y & Hy); exists y; revert Hx; apply HA; eauto. 2: intros (y & Hy); destruct (fos_surj R y) as (x & Hx); exists x; revert Hy; apply HA; eauto. 3: intros H y; destruct (fos_surj R y) as (x & Hx); generalize (H x); apply HA; eauto. 4: intros H x; destruct (fos_total R x) as (y & Hy); generalize (H y); apply HA; eauto. all: intros []; simpl; auto; intros; apply Hp, in_flat_map; exists (S n); simpl; auto. Qed.
imports: List Arith Lia 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) Undecidability.Shared.ListAutomation