Require Import Undecidability.Synthetic.Undecidability.

Require Import Undecidability.StackMachines.SMN.

Require Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.
Require Import Undecidability.CounterMachines.CM1_undec.

Theorem SMNdl_UB_undec : undecidable SMNdl_UB.
Proof.
  apply (undecidability_from_reducibility CM1_HALT_undec).
  exact CM1_HALT_to_SMNdl_UB.reduction.
Qed.