proposition: Lemma maybe_goto_1_grow_iter l r m n X Y : exists '(l', r', n', X', Y'), maybe_reachable (m*maybe_goto_1_grow_time) (l, r, goto n X Y) (l', §0^m ++ r', goto n' X' Y').
proof: Proof. Proof using NP_spec. elim: m l r n X Y. { move=> l r n X Y. exists (l, r, n, X, Y). by apply: maybe_reachable_refl'. } move=> m + l r n X Y. move /(_ l r n X Y) => [[[[[l' r'] n'] X'] Y'] He']. have [e He] := maybe_goto_1_grow l' r' m n' X' Y'. exists e. move: e He => [[[[l'' r''] n''] X''] Y''] He. move: He'. apply: (maybe_reachable_trans' maybe_goto_1_grow_time); [by lia |done | by have ->: (S m) = m+1 by lia]. Qed.
imports: Relation_Operators Operators_Properties Lia PeanoNat List Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.SMX_facts Undecidability.StackMachines.Util(Nat_facts List_facts) ssreflect ssrbool ssrfun