proposition: Lemma maybe_bounded_try_grow l r m : exists '(l', r', n, X, Y), maybe_reachable maybe_bounded_try_grow_time (l, §0^m ++ r, '?|) (l', §0^(m+1) ++ r', goto n X Y).
proof: Proof. Proof using NP_spec. rewrite /maybe_bounded_try_grow_time. move: m => [|m]; first last. { exists ([], [], 0, +|, +|). by apply: terminal_maybe_reachable => ? /bound_try_step_shape [? ?]. } have [e He] := maybe_bounded_yes_grow r l 0. exists e. move: e He => [[[[l' r'] n] X] Y] He. have := maybe_bounded_try r l. by apply: (maybe_reachable_trans' 1); 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