proposition: Lemma mortal_bounded {K x} : steps K x = None -> bounded K x.
proof: Proof. move=> HK. exists (map (fun oy => if oy is Some y then y else x) (path K x)). split. { by rewrite map_length path_length. } move=> y /reaches_steps [k]. have [?|?] : k < K \/ K <= k by lia. - move=> Hk. apply /in_map_iff. exists (Some y). split; first done. rewrite -Hk. by apply: In_pathI. - by move: HK => /(steps_k_monotone k) /(_ ltac:(lia)) ->. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun