proposition: Lemma loop_bounded K x : In (steps K x) (path K x) -> bounded K x.
proof: Proof. move=> /path_loopE' H. 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 /H {}H. apply /in_map_iff. by exists (Some y). Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun