proposition: Theorem Σdiscriminable_discrete_correct (A : fol_form (Σ11 X Y)) : fol_syms A ⊑ lX -> fol_rels A ⊑ lY -> { DX : _ & { DY : _ & { _ : discrete DX & { _ : discrete DY & { _ : finite_t DX & { _ : finite_t DY & { B : fol_form (Σ11 DX DY) | FSAT _ A <-> FSAT _ B } } } } } } }.
proof: Proof. Proof using HlY HlX DY_fin DY_discr DY DX_fin DX_discr DX. intros HX HY. exists DX, DY. do 4 (exists; [ auto | ]). exists (Σdiscriminable_discrete A). split. + rewrite fo_form_fin_dec_SAT_discr_equiv. intros (K & H0 & M & H1 & H2 & phi & H3). apply Σdiscriminable_discrete_sound with K M phi; auto. + intros (K & M & H1 & H2 & phi & H3). apply Σdiscriminable_discrete_complete with K M phi; 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)