proposition: Lemma maybe_index_no_grow l r m i : exists '(l', r', n, X, Y), maybe_reachable maybe_index_no_grow_time (l, §0^m ++ r, '#-i) (l', §0^(m+1) ++ r', goto n X Y).
proof: Proof. Proof using NP_spec. pose dummy := ([§0], [§0], 0, +|, +|). rewrite /maybe_index_no_grow_time. have [? | /in_iPI [j [n Hjn]]] : length P <= i \/ i < length P by lia. { exists dummy. apply: terminal_maybe_reachable. by apply: large_index_terminal. } case: (list_symbol_shape r). { move=> [m' ->]. exists dummy. rewrite ?app_norm. case: (m + m'). { by apply: terminal_maybe_reachable => ? /index_no_step_shape. } move=> {}m'. apply: (maybe_first_step (index_no_spec (i, (j, n))) l (§0^m')); [by lia | by auto with M | by rewrite ?app_norm |]. rewrite ?app_norm. apply: maybe_goto_1_futile. by lia. } move=> [m' [+ ->]] => {}r. rewrite ?app_norm. move Hm'': (m + m') => m''. move: m'' Hm'' => [|m''] Hm''. { exists dummy. by apply: terminal_maybe_reachable => ? /index_no_step_shape. } have [e He] := maybe_index_try_grow ([§1] ++ r) (§0^m' ++ l) m (1+i). exists e. move: e He => [[[[l' r'] n'] X'] Y'] He. apply: (maybe_first_step (index_no_spec (i, (j, n))) l (§0^m'' ++ [§1] ++ r)); [by lia | by auto with M | by rewrite ?app_norm | ]. rewrite ?app_norm. apply: (maybe_first_goto_1 maybe_index_try_grow_time); first by lia. move: He. apply: maybe_reachable_mon'; [by lia | by rewrite ?app_norm Hm'']. 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