proposition: Lemma maybe_index_yes_grow l r m i: exists '(l', r', n, X, Y), maybe_reachable maybe_index_yes_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_yes_grow_time. pose dummy := ([§0], [§0], 0, +|, +|). have [[n ->] | ] := list_symbol_shape r. { exists dummy. 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' [+ ->]] => {}r. have [Hi | /in_iPI [j [n Hijn]]]: length P <= i \/ i < length P by lia. { exists dummy. apply: terminal_maybe_reachable. by apply: large_index_terminal. } rewrite ?app_norm. suff: exists '(l', r', n, X, Y), maybe_reachable maybe_index_yes_grow_time (l, §0^(m+m') ++ [§1] ++ r, '#+i) (l', §0^((m+m')+1) ++ r', goto n X Y). { move=> [[[[[l' r'] n'] X'] Y'] H]. exists (l', §0^m' ++ r', n', X', Y'). move: H. apply: maybe_reachable_mon'; first by (rewrite /maybe_index_yes_grow_time; lia). rewrite ?app_norm. do 5 f_equal. by lia. } move: (m + m') => {}m {m'}. rewrite /maybe_index_yes_grow_time. move: m => [|m]. { move: l => [|a l]. { exists dummy. apply: (maybe_first_step (index_yes_spec_1 (i, (j, n))) [] r); [by lia | by auto with M | done |]. by apply: terminal_maybe_reachable => ? /index_try_step_shape [? ?]. } case: a. { have [/in_iPI [j'] [n'] Hjj'n' | Hj] : j < length P \/ length P <= j by lia. { exists (([§1] ++ r), l, n', (#+j), (#-j)). apply: (maybe_first_step (index_yes_spec_1 (i, (j, n))) ([§0] ++ l) r); [by lia | by auto with M | done |]. by apply: (maybe_first_step (index_try_spec (j, (j', n'))) r l); [by lia | by auto with M | done | by apply: maybe_reachable_refl']. } exists dummy. apply: (maybe_first_step (index_yes_spec_1 (i, (j, n))) ([§0] ++ l) r); [by lia | by auto with M | done |]. apply: terminal_maybe_reachable. by apply: large_index_terminal. } exists dummy. apply: (maybe_first_step (index_yes_spec_1 (i, (j, n))) ([§1] ++ l) r); [by lia | by auto with M | done |]. apply: terminal_maybe_reachable. by move=> ? /index_try_step_shape [? ?]. } have [[k ->] |] := list_symbol_shape l. { exists dummy. have [? | ?]: S m < n + 1 \/ n + 1 <= S m by lia. { apply: terminal_maybe_reachable=> ? /(index_yes_step_shape Hijn) [|/zero_prefix_lt]; [ done | by lia]. } apply: (maybe_first_step (index_yes_spec_n1 (i, (j, n))) (§0^k) (§0^(m-n) ++ [§1] ++ r)); [by lia | by auto with M | by rewrite ?app_norm; do 4 f_equal; lia | ]. rewrite ?app_norm. apply: maybe_goto_1_futile. by lia. } move=> [k1] [l' ->]. have [|]:= list_symbol_shape l'. { move=> [k2 ->]. pose k := (S m) / (1+n). have [? | ?] : k <= k2 \/ k2 < k by lia. { have [/in_iPI [j'] [n'] Hjj'n' | Hj]: j < length P \/ length P <= j by lia. { have := maybe_increase_next [] r i j n (S m) k2 k1 Hijn ltac:(lia). move Hm': (k1 + S m + S m / (1 + n) + S m mod (1 + n)) => m'. move: (k2 - S m / (1 + n)) => m'' H. have ? := @div_mod_pos n m. exists (([§1] ++ r), (§0^(m' - (S m + 1)) ++ [§1] ++ §0^m''), n', (#+j), (#-j)). move: H. apply: (maybe_reachable_trans' 1); [by lia | by rewrite ?app_norm |]. apply: (maybe_first_step (index_try_spec (j, (j', n'))) r (§0^(m'-1) ++ [§1] ++ §0^m'')); [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. } exists dummy. have := maybe_increase_next [] r i j n (S m) k2 k1 Hijn ltac:(lia). apply: (maybe_reachable_trans' 0); [by lia | by rewrite ?app_norm |]. apply: terminal_maybe_reachable. by apply: large_index_terminal. } exists dummy. have := maybe_increase_stop r i j n (S m) k2 k1 ([§0], §0^(S m + 1) ++ [§0], goto 0 +| +|) Hijn ltac:(lia). by apply: maybe_reachable_mon'; first by lia. } move=> [k2] [{}l' ->]. pose k := (S m) / (1+n). have [? | ?]: k <= k2 \/ k2 < k by lia. { have [/in_iPI [j'] [n'] Hjj'n' | Hj] : j < length P \/ length P <= j by lia. { have := maybe_increase_next ([§1] ++ l') r i j n (S m) k2 k1 Hijn ltac:(lia). move Hm': (k1 + S m + S m / (1 + n) + S m mod (1 + n)) => m'. move: (k2 - S m / (1 + n)) => m'' H. have ? := @div_mod_pos n m. exists (([§1] ++ r), (§0^(m' - (S m + 1)) ++ [§1] ++ §0^m'' ++ [§1] ++ l'), n', (#+j), (#-j)). move: H. apply: (maybe_reachable_trans' 1); [by lia | by rewrite ?app_norm |]. apply: (maybe_first_step (index_try_spec (j, (j', n'))) r (§0^(m'-1) ++ [§1] ++ §0^m'' ++ [§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. } exists dummy. have := maybe_increase_next ([§1] ++ l') r i j n (S m) k2 k1 Hijn ltac:(lia). apply: (maybe_reachable_trans' 0); [by lia | by rewrite ?app_norm |]. apply: terminal_maybe_reachable. by apply: large_index_terminal. } have [[[[[l'' r''] n''] X''] Y''] Hz] := maybe_bounded_yes_grow ([§1] ++ r) ([§1] ++ l') (S m + k1 + k2 + 1). exists (l'', (§0^(k1 + k2 + 1) ++ r''), n'', X'', Y''). have := maybe_increase_fail l' r i j n (S m) k2 k1 Hijn ltac:(lia). apply: (maybe_reachable_trans' 1); [by lia | done |]. move: Hz. 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