proposition: Theorem FSAT_equiv_discernable_syms : FSAT Σ (testt f ⟑ (testt g ⤑ ⊥)) <-> f ≢ g.
proof: Proof. rewrite discernable_equiv1. split. + intros (D & M & H1 & H2 & rho & H3 & H4). simpl in H3, H4 |- *. exists (fun k => if H2 P (vec_map (fo_term_sem M rho) (cast (termt k ## ø) (eq_sym HP))) then true else false). do 2 match goal with |- context[if ?c then _ else _] => destruct c end; auto; tauto. + intros (δ & H1 & H2). apply discernable_syms_FSAT with δ; auto. Qed.
imports: List Bool Undecidability.Synthetic(Definitions ReducibilityFacts InformativeDefinitions InformativeReducibilityFacts) Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_decidable finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils decidable discernable fol_ops fo_sig fo_terms fo_logic fo_sat Sig1_1 red_utils)