Require Import Undecidability.Synthetic.Undecidability.

From Undecidability.MinskyMachines
  Require Import ndMM2 ndMM2_undec.

From Undecidability.ILL
  Require Import IMSELL ndMM2_IMSELL.

Local Infix "≤" := (@IMSELL_le _) (at level 70).
Local Notation "u ≰ v" := (~ u ≤ v) (at level 70).
Local Notation U := (@IMSELL_U _).


Theorem IMSELL_undec (S : IMSELL_sig3) : undecidable (@IMSELL_cf_PROVABILITY3 S).
Proof.
  apply (undecidability_from_reducibility ndMM2_undec).
  now apply ndMM2_IMSELL.reduction.
Qed.

Theorem IMSELL3_undec : undecidable (@IMSELL_cf_PROVABILITY imsell3).
Proof.
  refine (@IMSELL_undec (exist _ imsell3 _)).
  now exists (Some true), (Some false), None.
Qed.