proposition: Lemma bounded_mortal_bound {k x} : bounded (S K) x -> mortal k x -> mortal K x.
proof: Proof. move=> /boundedE + /mortal_steps_iff Hk. case. - move=> /path_loopE /(_ (S k)). rewrite Hk => /In_None_pathE ?. by apply /mortal_steps_iff. - move=> ?. by apply /mortal_steps_iff. 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