proposition: Lemma maybe_increase_yes_grow l r m i : exists '(l', r', n, X, Y), maybe_reachable maybe_increase_yes_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_increase_yes_grow_time. have [? | /in_iPI [j [n Hijn]]]: length P <= i \/ i < length P by lia. { exists dummy. apply: terminal_maybe_reachable. by apply: large_increase_terminal. } move: l => [|a l]. { exists dummy. by apply: terminal_maybe_reachable => ? /increase_yes_step_shape. } case: a. { exists dummy. by apply: terminal_maybe_reachable => ? /increase_yes_step_shape. } have [|]:= list_symbol_shape l. { move=> [m' ->]. exists dummy. apply: (maybe_first_step (increase_yes_spec (i, (j, n))) (§0^m') (§0^m ++ r)); [ by lia | by auto with M | by rewrite ?app_norm | ]. apply: (maybe_reachable_mon' (n := maybe_index_yes_futile_time)); [by lia | by rewrite ?app_norm; reflexivity | by apply: maybe_index_yes_futile]. } move=> [m' [+ ->]] => {}l. have [-> |] : m' = 0 \/ (0 < m' /\ m' < n+1) \/ n+1 <= m' by lia. { have [e He] := maybe_index_try_grow ([§1] ++ l) (§0^1 ++ r) m j. exists e. move: e He => [[[[l' r'] n'] X'] Y'] He. apply: (maybe_first_step (increase_yes_spec (i, (j, n))) ([§1] ++ l) (§0^m ++ r)); [by lia | by auto with M | by rewrite ?app_norm | ]. apply: (maybe_first_step (index_yes_spec_1 (i, (j, n))) (§0^(1 + m) ++ r) l); [by lia | by auto with M | by rewrite ?app_norm | ]. move: He. apply: maybe_reachable_mon'; first by lia. rewrite ?app_norm. do 5 f_equal. by lia. } case=> Hm'. { exists dummy. apply: (maybe_first_step (increase_yes_spec (i, (j, n))) (§0^m' ++ [§1] ++ l) (§0^m ++ r)); [ by lia | by auto with M | by rewrite ?app_norm |]. apply: terminal_maybe_reachable. rewrite ?app_norm. have ->: m' = 1+(m'-1) by lia. move=> ? /(index_yes_step_shape Hijn) [| /zero_prefix_lt]; by [| lia]. } exists (([§1] ++ §0^(m' - (n + 1)) ++ [§1] ++ l), (§0^n ++ r), 0, $?i, $?i). apply: (maybe_first_step (increase_yes_spec (i, (j, n))) (§0^m' ++ [§1] ++ l) (§0^m ++ r)); [ by lia | by auto with M | by rewrite ?app_norm |]. apply: (maybe_first_step (index_yes_spec_n1 (i, (j, n))) (§0^(1+m) ++ r) (§0^(m'-(n+1)) ++ [§1] ++ l)); [ by lia | by auto with M | by rewrite ?app_norm; do 4 f_equal; lia |]. apply: maybe_reachable_refl'. rewrite ?app_norm. do 4 f_equal. 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