Require Import Undecidability.Synthetic.Definitions.

Require Import Undecidability.MinskyMachines.MM2.
From Undecidability.MinskyMachines.Deciders Require
  MM2_REV_dec MM2_REV_HALT_dec MM2_UBOUNDED_dec MM2_UMORTAL_dec.

Theorem MM2_REV_dec : decidable MM2_REV.
Proof.
  exists MM2_REV_dec.decide.
  exact MM2_REV_dec.decide_spec.
Qed.

Check MM2_REV_dec.

Theorem MM2_REV_HALT_dec : decidable MM2_REV_HALT.
Proof.
  exists MM2_REV_HALT_dec.decide.
  exact MM2_REV_HALT_dec.decide_spec.
Qed.

Check MM2_REV_HALT_dec.

Theorem MM2_UBOUNDED_dec : decidable MM2_UBOUNDED.
Proof.
  exists MM2_UBOUNDED_dec.decide.
  exact MM2_UBOUNDED_dec.decide_spec.
Qed.

Check MM2_UBOUNDED_dec.

Theorem MM2_UMORTAL_dec : decidable MM2_UMORTAL.
Proof.
  exists MM2_UMORTAL_dec.decide.
  exact MM2_UMORTAL_dec.decide_spec.
Qed.

Check MM2_UMORTAL_dec.