Require Import Undecidability.Synthetic.Definitions.

Require Import Undecidability.CounterMachines.CM2.
From Undecidability.CounterMachines.Deciders Require
  CM2_REV_dec CM2_REV_HALT_dec CM2_UBOUNDED_dec CM2_UMORTAL_dec.

Theorem CM2_REV_dec : decidable CM2_REV.
Proof.
  exists CM2_REV_dec.decide.
  exact CM2_REV_dec.decide_spec.
Qed.

Check CM2_REV_dec.

Theorem CM2_REV_HALT_dec : decidable CM2_REV_HALT.
Proof.
  exists CM2_REV_HALT_dec.decide.
  exact CM2_REV_HALT_dec.decide_spec.
Qed.

Check CM2_REV_HALT_dec.

Theorem CM2_UBOUNDED_dec : decidable CM2_UBOUNDED.
Proof.
  exists CM2_UBOUNDED_dec.decide.
  exact CM2_UBOUNDED_dec.decide_spec.
Qed.

Check CM2_UBOUNDED_dec.
Theorem CM2_UMORTAL_dec : decidable CM2_UMORTAL.
Proof.
  exists CM2_UMORTAL_dec.decide.
  exact CM2_UMORTAL_dec.decide_spec.
Qed.

Check CM2_UMORTAL_dec.