Require Import List.

From Undecidability.Synthetic
  Require Import Definitions
                 ReducibilityFacts
                 InformativeDefinitions
                 InformativeReducibilityFacts.

From Undecidability.PCP Require Import PCP.

From Undecidability.Shared.Libs.DLW.Utils
  Require Import utils_tac utils_list finite.

From Undecidability.Shared.Libs.DLW.Vec
  Require Import pos vec.

From Undecidability.TRAKHTENBROT
  Require Import notations bpcp
                 fo_sig fo_terms fo_logic fo_sat

                 Sig_discrete
                 Sig_noeq
                 .

Set Default Proof Using "Type".

Set Implicit Arguments.



Theorem BPCP_BPCP_problem_eq R : BPCP_problem R <-> BPCP R.
Proof.
  split; intros (u & Hu).
  + constructor 1 with u; auto.
  + exists u; auto.
Qed.


Theorem BPCP_BPCP_problem : BPCP ⪯ᵢ BPCP_problem.
Proof.
  exists (fun x => x); red; symmetry; apply BPCP_BPCP_problem_eq.
Qed.


Theorem fo_form_fin_dec_SAT_discr_equiv Σ A : FSAT Σ A <-> FSAT' Σ A.
Proof.
  split.
  + apply fo_form_fin_dec_SAT_fin_discr_dec.
  + apply fo_form_fin_discr_dec_SAT_fin_dec.
Qed.


Corollary FIN_DEC_SAT_FIN_DISCR_DEC_SAT Σ : FSAT Σ ⪯ᵢ FSAT' Σ.
Proof. exists (fun A => A); red; apply fo_form_fin_dec_SAT_discr_equiv. Qed.



Section FIN_DEC_EQ_SAT_FIN_DEC_SAT.

  Variable (Σ : fo_signature) (e : rels Σ) (He : ar_rels _ e = 2).

  Theorem FIN_DEC_EQ_SAT_FIN_DEC_SAT : FSATEQ e He ⪯ᵢ FSAT Σ.
  Proof.
    exists (fun A => Σ_noeq (fol_syms A) (e::fol_rels A) _ He A).
    intros A; split.
    + intros (X & HX); exists X; revert HX.
      apply Σ_noeq_sound.
    + apply Σ_noeq_complete; cbv; auto.
  Qed.

End FIN_DEC_EQ_SAT_FIN_DEC_SAT.