proposition: Lemma path_noloopI k x : ~ In (steps k x) (path k x) -> NoDup (path (k + 1) x).
proof: Proof. elim: k x. { move=> ??. constructor; [done| constructor]. } move=> k IH x. rewrite path_S_last /steps in_app_iff /= -/(steps k x). move=> /Decidable.not_or. have [|/IH ?] := In_dec option_mm2_state_eq_dec (steps k x) (path k x). - move=> /path_loopE /(_ (S k)). tauto. - move=> [?] ?. apply /(NoDup_Add (a := steps (S k) x) (l := path (k + 1) x)). + rewrite path_S_last. have := Add_app (steps (k + 1) x) (path (k + 1) x) []. congr Add. * congr steps. lia. * by rewrite app_nil_r. + constructor; first done. have ->: k + 1 = S k by lia. rewrite path_S_last in_app_iff /=. tauto. Qed.
imports: List ListDec PeanoNat Lia Relation_Operators Operators_Properties Permutation Undecidability.MinskyMachines.MM2 Undecidability.MinskyMachines.Util.MM2_facts ssreflect ssrbool ssrfun