CM1_HALT is undecidable

Require Import Undecidability.Synthetic.Undecidability.

Require Import Undecidability.CounterMachines.CM1.
Require Import Undecidability.CounterMachines.Reductions.MM2_HALTING_to_CM1_HALT.

Require Import Undecidability.MinskyMachines.MM2_undec.

Lemma CM1_HALT_undec : undecidable CM1_HALT.
Proof.
apply (undecidability_from_reducibility MM2_HALTING_undec).
exact MM2_HALTING_to_CM1_HALT.reduction.
Qed.

Check CM1_HALT_undec.