proposition: Theorem fo_form_fin_discr_dec_SAT_pos : fo_form_fin_discr_dec_SAT A <-> exists n, fo_form_fin_dec_SAT_in A (pos n).
proof: Proof. split. 2: intros (n & Hn); exists (pos n); exists; auto. intros (X & HX & M & Xf & H2 & phi & H3). destruct (finite_t_discrete_bij_t_pos Xf HX) as (n & i & j & Hji & Hij). set (M' := Mk_fo_model Σ (fun s v => i (fom_syms M s (vec_map j v))) (fun r v => fom_rels M r (vec_map j v))). exists n, M'. exists. { apply finite_t_pos. } exists. { intros r v; apply H2. } exists (fun x => i (phi x)). cut (fol_sem M phi A <-> fol_sem M' (fun x : nat => i (phi x)) A); try tauto. clear H3; revert phi; induction A as [ | r v | b B HB C HC | [] B HB ]; intros phi. + simpl; tauto. + simpl; rewrite vec_map_map; apply fol_equiv_ext; f_equal. apply vec_pos_ext; intros p; simpl; rew vec. generalize (vec_pos v p); clear r v p. intros t; induction t as [ x | s v IH ]. * simpl; rewrite Hji; auto. * rew fot; unfold M' at 1; simpl; rewrite Hji. f_equal; apply vec_pos_ext; intros p; rew vec. + apply fol_bin_sem_ext; auto. + simpl; split. * intros (x & Hx); exists (i x). apply HB in Hx. revert Hx; apply fol_sem_ext; intros []; simpl; auto. * intros (p & Hp); exists (j p). apply HB; revert Hp. apply fol_sem_ext; intros []; simpl; auto. + simpl; split. * intros H p; generalize (H (j p)); rewrite HB. apply fol_sem_ext; intros []; simpl; auto. * intros H x; generalize (H (i x)); rewrite HB. apply fol_sem_ext; intros []; 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.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms fo_logic fo_sat decidable)