proposition: Lemma NoDup_not_bounded {K x y} : steps K x = Some y -> NoDup (path (K + 1) x) -> not (bounded K x).
proof: Proof. move=> Hxy HK [L [? HL]]. apply: (pigeonhole (path (K+1) x) (map Some L)). - move=> [z|] /in_map_iff [k] [Hk] /in_seq ?. { apply /in_map_iff. exists z. split; first done. apply: HL. by apply: (steps_reaches Hk). } by move: Hk Hxy => /(steps_k_monotone K) /(_ ltac:(lia)) ->. - rewrite map_length path_length. lia. - done. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun