proposition: Lemma Σn_Σ2_correct (A : fol_form Σn) d r φ ψ : HR1 (ψ d) (ψ r) -> HR2 (ψ d) (ψ r) -> HR3 (ψ d) (ψ r) -> (forall x, x ∊ fol_vars A -> R (φ x) (ψ x)) -> ⟪ A ⟫' φ <-> ⟪Σn_Σ2 d r A⟫ ψ.
proof: Proof. revert d r φ ψ. induction A as [ | [] v | b A HA B HB | [] A HA ]; intros l r phi psy H1 H2 H3 H. + simpl; tauto. + simpl; red in H3. rewrite H3 with (w := vec_map (fun x => psy (Σrel_var x)) v). * apply (fol_quant_sem_ext fol_ex); intros x. apply (fol_bin_sem_ext fol_conj); try tauto. rewrite Σ2_is_tuple_spec; simpl. rewrite !vec_map_map; simpl; tauto. * intros p; rewrite !vec_pos_map. case_eq (vec_pos v p). 2: intros []. simpl; intros x Hx; rewrite Hx; simpl. apply H; simpl; apply in_flat_map. exists (vec_pos v p); split. - apply in_vec_list, in_vec_pos. - simpl; rewrite Hx; simpl; auto. + simpl; apply fol_bin_sem_ext; [ apply HA | apply HB ]; intros; auto; apply H, in_or_app; simpl; auto. + simpl; split. * intros (x & Hx). destruct (H1 x) as (y & G1 & G2). exists y; split. - rew fot; simpl; auto. - revert Hx; apply HA; auto. intros [ | n' ]; simpl; auto. intros; apply H; simpl; apply in_flat_map; exists (S n'); simpl; auto. * intros (y & G1 & G2); revert G1 G2; rew fot; simpl; intros G1 G2. destruct (H2 _ G1) as (x & G3). exists x; revert G2; apply HA; auto. intros [ | n' ]; simpl; auto. intros; apply H; simpl; apply in_flat_map; exists (S n'); simpl; auto. + simpl; split. * intros G1 y; rew fot; simpl; intros G2. destruct (H2 _ G2) as (x & G3). generalize (G1 x); apply HA; auto. intros [ | n' ]; simpl; auto. intros; apply H; simpl; apply in_flat_map; exists (S n'); simpl; auto. * intros G1 x. destruct (H1 x) as (y & G2 & G3). generalize (G1 _ G2); apply HA; auto. intros [ | n' ]; simpl; auto. intros; apply H; simpl; apply in_flat_map; exists (S n'); simpl; 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.Shared.Libs.DLW.Wf(wf_finite) Undecidability.FOL.TRAKHTENBROT(notations decidable fol_ops fo_sig fo_terms fo_logic fo_sat membership hfs reln_hfs)