proposition: Lemma maybe_goto_1_grow l r m n X Y : exists '(l', r', n', X', Y'), maybe_reachable maybe_goto_1_grow_time (l, §0^m ++ r, goto n X Y) (l', §0^(m+1) ++ r', goto n' X' Y').
proof: Proof. Proof using NP_spec. rewrite /maybe_goto_1_grow_time. case: (list_symbol_shape r). { move=> [m' ->]. exists ([], [], 0, +|, +|). rewrite /maybe_basic_state_grow_time ?app_norm. apply: maybe_goto_1_futile. by lia. } move=> [m' [+ ->]] => {}r. rewrite ?app_norm. move Hk: ((m + m') mod (n + 1)) => k. move: k Hk => [|k] Hk. { have [e He] := maybe_basic_state_grow ([§1] ++ r) (§0^m' ++ l) m X. exists e. move: e He => [[[[l' r'] n'] X'] Y'] He. apply: (maybe_first_goto_1 maybe_basic_state_grow_time); first by lia. rewrite Hk. move: He. apply: maybe_reachable_mon'; [by lia | by rewrite ?app_norm]. } have [e He] := maybe_basic_state_grow ([§1] ++ r) (§0^m' ++ l) m Y. exists e. move: e He => [[[[l' r'] n'] X'] Y'] He. apply: (maybe_first_goto_1 maybe_basic_state_grow_time); first by lia. rewrite Hk. move: He. apply: maybe_reachable_mon'; [by lia | by rewrite ?app_norm]. 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