proposition: Lemma path_loopE K x : In (steps K x) (path K x) -> forall k, In (steps k x) (path K x).
proof: Proof. elim: K x; first done. move=> K IH x. rewrite (steps_plus' (k := 1) (k' := K)). case Hxz: (steps 1 x) => [z|]. - move=> H. rewrite (path_S z Hxz) /= in H. case: H. + move=> Hzx k. have /steps_loop_mod -> : steps (S K) x = Some x. { by rewrite (steps_plus' (k := 1) (k' := K)) Hxz. } by apply /In_pathI /(Nat.mod_upper_bound k (S K)). + rewrite (path_S z Hxz). move=> /IH {}IH [|k]; first by left. rewrite (steps_plus' (k := 1) (k' := k)) Hxz. right. by apply: IH. - move=> /in_map_iff [k] [Hk] /in_seq HK. move=> k'. have [|Hkk'] : k' < k \/ k <= k' by lia. + move=> ?. apply: In_pathI. lia. + move: (Hk) => /(steps_k_monotone k') /(_ Hkk') ->. rewrite /= in Hk. rewrite -Hk. apply: In_pathI. lia. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun