From PCF2.external.Synthetic Require Import Undecidability ReducibilityFacts DecidabilityFacts EnumerabilityFacts.
From PCF2 Require Import SATIS CE SATIS_PS PS_RPS co_RPS_CE.
From PCF2.external Require Import SR.

Section undecidability.

Variable Loaders_word_enc : list (val_word_enc).

Axiom SR_SATIS_equiv :
  forall p R, SATIS Loaders_word_enc R p <-> SR R p.

Axiom SR_undec :
  exists R_undec, undecidable (complement (SR R_undec)).

Lemma reduces_SR_SATIS:
  forall R, reduces (SR R) (SATIS Loaders_word_enc R).
Proof.
  intros R. exists (fun p => p).
  split. all: now rewrite SR_SATIS_equiv.
Qed.

Lemma reduces_co_SR_co_SATIS:
  forall R, reduces (complement (SR R)) (complement (SATIS Loaders_word_enc R)).
Proof.
  intros R. apply reduces_complement. apply reduces_SR_SATIS.
Qed.

Lemma co_SR_reduces_CE:
  forall R, reduces (complement (SR R)) CE.
Proof.
  intros R.
  eapply reduces_transitive.
  1: apply reduces_co_SR_co_SATIS.
  eapply reduces_transitive.
  1: apply reduces_co_SATIS_co_PS.
  eapply reduces_transitive.
  1: apply reduces_co_PS_co_RPS.
  apply reduces_co_RPS_CE_closed.
Qed.

Theorem CE_undecidable:
  undecidable CE.
Proof.
  destruct SR_undec as [R_undec HR_undec].
  eapply undecidability_from_reducibility. 1: exact HR_undec.
  apply co_SR_reduces_CE.
Qed.

Lemma reduces_CE_CE_open:
  reduces CE CE_open.
Proof.
  exists (fun '(p, A) => (nil, p, A)).
  now intros [[s t] A].
Qed.

Corollary CE_open_undecidable:
  undecidable CE_open.
Proof.
  eapply undecidability_from_reducibility. 1: exact CE_undecidable.
  apply reduces_CE_CE_open.
Qed.

End undecidability.