proposition: Lemma maybe_basic_state_grow l r m X : exists '(l', r', n', X', Y'), maybe_reachable maybe_basic_state_grow_time (l, §0^m ++ r, basic_state X) (l', §0^(m+1) ++ r', goto n' X' Y').
proof: Proof. Proof using NP_spec. rewrite /maybe_basic_state_grow_time. case: X. - case. + have [e He] := maybe_bounded_yes_grow l r m. exists e. move: e He => [[[[l' r'] n'] X'] Y']. by apply: maybe_reachable_mon'; [ lia | ]. + have [e He] := maybe_bounded_try_grow l r m. exists e. move: e He => [[[[l' r'] n'] X'] Y']. by apply: maybe_reachable_mon'; [ lia | ]. - case=> i. + have [e He] := maybe_index_try_grow l r m i. exists e. move: e He => [[[[l' r'] n'] X'] Y']. by apply: maybe_reachable_mon'; [ lia | ]. + have [e He] := maybe_index_yes_grow l r m i. exists e. move: e He => [[[[l' r'] n'] X'] Y']. by apply: maybe_reachable_mon'; [ lia | ]. + have [e He] := maybe_index_no_grow l r m i. exists e. move: e He => [[[[l' r'] n'] X'] Y']. by apply: maybe_reachable_mon'; [ lia | ]. - case=> i. + have [e He] := maybe_increase_try_grow l r m i. exists e. move: e He => [[[[l' r'] n'] X'] Y']. by apply: maybe_reachable_mon'; [ lia | ]. + have [e He] := maybe_increase_yes_grow l r m i. exists e. move: e He => [[[[l' r'] n'] X'] Y']. by apply: maybe_reachable_mon'; [ lia | ]. + have [e He] := maybe_increase_no_grow l r m i. exists e. move: e He => [[[[l' r'] n'] X'] Y']. by apply: maybe_reachable_mon'; [ 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