proposition: Theorem FSAT_equiv_discernable_rels : FSAT Σ (test P ⟑ (test Q ⤑ ⊥)) <-> P ≢ Q.
proof: Proof. rewrite discernable_equiv1. split. + intros (D & M & H1 & H2 & rho & H3 & H4). exists (fun K => if @H2 K (vec_set_pos (fun _ => rho 0)) then true else false). simpl in H3, H4 |- *. rewrite vec_map_set_pos in H3, H4. do 2 match goal with |- context[if ?c then _ else _] => destruct c end; auto; tauto. + intros (f & H1 & H2). apply discernable_rels_FSAT with f; 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)