Require Import Undecidability.Synthetic.Undecidability.
Require Import Undecidability.SemiUnification.SemiU.
Require Undecidability.SemiUnification.Reductions.CSSM_UB_to_SSemiU.
Require Undecidability.SemiUnification.Reductions.SSemiU_to_RU2SemiU.
Require Undecidability.SemiUnification.Reductions.RU2SemiU_to_LU2SemiU.
Require Undecidability.SemiUnification.Reductions.RU2SemiU_to_SemiU.
Require Import Undecidability.StackMachines.SSM_undec.
Theorem SSemiU_undec : undecidable SSemiU.
Proof.
apply (undecidability_from_reducibility CSSM_UB_undec).
exact CSSM_UB_to_SSemiU.reduction.
Qed.
Theorem RU2SemiU_undec : undecidable RU2SemiU.
Proof.
apply (undecidability_from_reducibility SSemiU_undec).
exact SSemiU_to_RU2SemiU.reduction.
Qed.
Theorem LU2SemiU_undec : undecidable LU2SemiU.
Proof.
apply (undecidability_from_reducibility RU2SemiU_undec).
exact RU2SemiU_to_LU2SemiU.reduction.
Qed.
Theorem SemiU_undec : undecidable SemiU.
Proof.
apply (undecidability_from_reducibility RU2SemiU_undec).
exact RU2SemiU_to_SemiU.reduction.
Qed.
Check SemiU_undec.