proposition: Lemma maybe_index_try_grow l r m i : exists '(l', r', n, X, Y), maybe_reachable maybe_index_try_grow_time (l, §0^m ++ r, '#?i) (l', §0^(m+1) ++ r', goto n X Y).
proof: Proof. Proof using NP_spec. rewrite /maybe_index_try_grow_time. pose dummy := ([§0], [§0], 0, +|, +|). have [[n ->]|] := list_symbol_shape r. { exists dummy. apply: (maybe_reachable_mon' (n := maybe_index_try_futile_time)); [by lia | by rewrite ?app_norm; reflexivity | by apply: maybe_index_try_futile]. } move=> [n [+ ->]] => {}r. move Hk: (length P - i) => k. suff: exists '(l', r', n', X', Y'), maybe_reachable (maybe_index_try_futile_time + k * maybe_index_try_step_time + maybe_index_yes_grow_time + maybe_goto_1_time + 1) (l, §0^(m+n) ++ [§1] ++ r, '#? i) (l', §0^((m+n)+1) ++ r', goto n' X' Y'). { move=> [[[[[l' r'] n'] X'] Y'] H]. exists (l', §0^n ++ r', n', X', Y'). move: H. apply: maybe_reachable_mon'; first by (rewrite /maybe_index_try_grow_time; lia). rewrite ?app_norm. do 5 f_equal. by lia. } move: (m + n) l => {}m {n} [|a l]. { exists dummy. by apply: terminal_maybe_reachable => ? /index_try_step_shape [? ?]. } case: a. { exists dummy. by apply: terminal_maybe_reachable => ? /index_try_step_shape [? ?]. } move: r m => r [|m]. { exists dummy. by apply: terminal_maybe_reachable => ? /index_try_step_shape [? ?]. } elim: k i r Hk. { move=> *. exists dummy. apply: terminal_maybe_reachable. apply: large_index_terminal. by lia. } move=> k IH i r Hk /=. have /in_iPI [j [n Hijn]] : i < length P by lia. pose x := {| CM.state := i; CM.value := S m |}. move Hi'm': (CM.step P x) => [i' m']. have := CM_facts.step_progress P x. move /(_ ltac:(rewrite /x /=; lia) ltac:(rewrite /x /=; lia)). case. { rewrite Hi'm'. move=> [? ?]. subst i' m'. have [e He] := IH (1+i) r ltac:(lia). exists e. move: e He => [[[[? ?] ?] ?] ?] He. have := maybe_index_try_step l r x. rewrite /x Hi'm' /= ?nat_norm ?app_norm. by apply: (maybe_reachable_trans' (maybe_index_try_futile_time + k * maybe_index_try_step_time + maybe_index_yes_grow_time + maybe_goto_1_time + 1)); first by lia. } move=> Hx. have [[j' n'] [/nth_error_Some_In_iP HxIp /= Hmn']] := CM_facts.inc_value_mod Hx. have [e He] := maybe_index_yes_grow ([§1] ++ r) ([§1] ++ l) (S m) i. exists e. move: e He => [[[[? ?] ?] ?] ?] He. apply: (maybe_first_step (index_try_spec (i, (j, n))) l (§0^m ++ [§1] ++ r)); [ by nia | by auto with M | by rewrite ?app_norm | ]. rewrite ?app_norm. apply: (maybe_first_goto_1 maybe_index_yes_grow_time); first by nia. subst x. have [_ ->]:= in_iP_unique (n := n) (n' := n') ltac:(eassumption) ltac:(eassumption). rewrite Hmn'. move: He. by apply: maybe_reachable_mon'; first 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