proposition: Lemma maybe_increase_no_grow l r m i : exists '(l', r', n, X, Y), maybe_reachable maybe_increase_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_increase_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_increase_terminal. } move: l => [|a l]. { exists dummy. by apply: terminal_maybe_reachable => ? /increase_no_step_shape. } case: a. { exists dummy. by apply: terminal_maybe_reachable => ? /increase_no_step_shape. } have [[m' ->]|] := list_symbol_shape l. { exists dummy. apply: (maybe_first_step (increase_no_spec (i, (j, n))) (§0^m') (§0^m ++ r)); [ by lia | by auto with M | by rewrite ?app_norm | ]. rewrite ?app_norm. apply: maybe_goto_1_futile. by lia. } move=> [m' [+ ->]] => {}l. have [e He] := maybe_bounded_yes_grow ([§1] ++ l) (§0^(m'+1) ++ r) m. exists e. move: e He => [[[[l' r'] n'] X'] Y'] He. apply: (maybe_first_step (increase_no_spec (i, (j, n))) (§0^m' ++ [§1] ++ l) (§0^m ++ r)); [by lia | by auto with M | by rewrite ?app_norm | ]. rewrite ?app_norm. apply: (maybe_first_goto_1 1); first by lia. move: He. apply: maybe_reachable_mon'; first by lia. rewrite ?app_norm. do 5 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