proposition: Lemma boundedE {K' x} : bounded K' x -> (In (steps K' x) (path M K' x)) + (steps K' x = None).
proof: Proof. move=> HK'. case Hy: (steps K' x) => [y|]; last by right. have [|] := In_dec option_mm2_state_eq_dec (Some y) (path M K' x). { rewrite -Hy => ?. by left. } rewrite -Hy. move=> /path_noloopI /NoDup_not_bounded. by move=> /(_ y Hy HK'). Qed.
imports: List PeanoNat Lia Relation_Operators Operators_Properties ConstructiveEpsilon Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Deciders.MM2_UBOUNDED_dec Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun