From Undecidability.Shared.Libs.DLW
  Require Import utils_tac.

Require Import Undecidability.Synthetic.Undecidability.
Require Import Undecidability.Synthetic.ReducibilityFacts.

From Undecidability.PCP Require Import PCP PCP_undec.
From Undecidability.StackMachines Require Import BSM.
From Undecidability.MinskyMachines Require Import MM.

From Undecidability.ILL
  Require Import EILL ILL iBPCP_MM MM_EILL EILL_ILL.

Require Import Undecidability.PCP.Reductions.HaltTM_1_to_PCPb.

Import ReductionChainNotations UndecidabilityNotations.


Theorem PCP_chain_ILL :
  ⎩ PCP ⪯ₘ PCPb ⪯ₘ iPCPb ⪯ₘ BSM_HALTING ⪯ₘ MM_HALTS_ON_ZERO ⪯ₘ EILL_PROVABILITY ⪯ₘ ILL_PROVABILITY ⎭.
Proof.
  msplit 5; ( apply PCP_chain_iPCPb || apply iBPCP_chain_MM || idtac).
  + apply MM_HALTS_ON_ZERO_EILL_PROVABILITY.
  + apply EILL_ILL_PROVABILITY.
Qed.

Check PCP_chain_ILL.


Local Hint Resolve EILL_rILL_cf_PROVABILITY
                   EILL_rILL_PROVABILITY
                   EILL_ILL_cf_PROVABILITY
                 : core.


Theorem EILL_undec : undecidable EILL_PROVABILITY.
Proof. undec from PCP_undec using chain PCP_chain_ILL. Qed.


Theorem ILL_undec : undecidable ILL_PROVABILITY.
Proof. undec from PCP_undec using chain PCP_chain_ILL. Qed.


Theorem ILL_cf_undec : undecidable ILL_cf_PROVABILITY.
Proof. undec from EILL_undec; auto. Qed.


Theorem rILL_cf_undec : undecidable rILL_cf_PROVABILITY.
Proof. undec from EILL_undec; auto. Qed.


Theorem rILL_undec : undecidable rILL_PROVABILITY.
Proof. undec from EILL_undec; auto. Qed.