proposition: Lemma maybe_bounded_yes_grow l r m : exists '(l', r', n, X, Y), maybe_reachable 1 (l, §0^m ++ r, '+|) (l', §0^(m+1) ++ r', goto n X Y).
proof: Proof. Proof using capped_P. have := Exists_dec (fun '(i, (n, X, Y)) => l = ([§1] ++ §0^i ++ [§1] ++ §0^(G-2-i)) ++ skipn G l) igotos. case. { move=> [i] [[n X] Y]. by do 2 (decide equality). } - rewrite Exists_exists. move=> [[i] [[n X] Y]] [Hi ->]. exists ((§0^(n + 1) ++ skipn G l), (§0^(G - (n + 2)) ++ r), n, X, Y). apply: (maybe_first_step (bound_yes_spec (i, (n, X, Y))) (skipn G l) (§0^m ++ r)); [by lia | by auto with M | done |]. apply: maybe_reachable_refl'. have ? := igotos_capped Hi. rewrite /G ?app_norm /gotos ?app_length /=. do 4 f_equal. by lia. - move=> H. exists ([], [], 0, +|, +|). apply: terminal_maybe_reachable. move=> y /stepE [] > [] *; subst; try done. apply: H. apply /Exists_exists. eexists. constructor; first by eassumption. rewrite /= ?app_norm. do 4 f_equal. rewrite ?app_assoc skipn_app. have ? := in_igotos_lt ltac:(eassumption). set s := (skipn G _). have -> : s = []. { rewrite /s skipn_all2; last done. rewrite ?app_length ?repeat_length /= /G. by lia. } rewrite ?app_length ?repeat_length /= /G. set k := (k in skipn k _). have -> : k = 0 by lia. done. 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