proposition: Lemma maybe_goto_1_futile {T l n X Y m z} : maybe_index_try_stop_time + 2 <= T -> maybe_reachable T (l, §0^m, goto n X Y) z.
proof: Proof. Proof using NP_spec. move=> ?. suff: maybe_reachable (maybe_index_try_stop_time + 2) (l, §0^m, goto n X Y) z by apply: maybe_reachable_mon'. rewrite /maybe_index_try_stop_time. have /(_ ltac:(do 4 decide equality)) [HnXY | /not_in_gotos_terminal ?] := in_dec _ (n, X, Y) gotos; last by apply: terminal_maybe_reachable. have [? | ?]: G+CP+1 <= m \/ m <= G+CP by lia. { have := @maybe_goto_1_far l [] m. rewrite ?app_norm. apply; by lia. } have [? | ?]: m < G \/ G <= m by lia. { right. exists (l, §0^m, goto n X Y). constructor; first by apply: reach_refl. move=> y /stepE [] > []; try done. - move=> ? /(f_equal (@length Symbol)). rewrite ?app_length ?repeat_length. by lia. - move=> ? Hm. exfalso. have : not (In §1 (§0^m)) by move /(@repeat_spec Symbol). apply. rewrite Hm ?in_app_iff. clear. by firstorder done. } move: (HnXY) => /gotos_igotos => [[i ?]]. apply: (maybe_first_step (goto_spec_G (i, (n, X, Y))) l (§0^(m - G))); [by lia | by auto with M | by rewrite ?app_norm; do 4 f_equal; lia |]. have [? | ?] : m - G < 2 \/ 2 <= m - G by lia. { right. eexists. constructor; first by apply: reach_refl. move=> ? /bound_try_step_shape. have : m - G = 0 \/ m - G = 1 by lia. move=> [-> | ->]; clear; by firstorder done. } apply: (maybe_first_step bound_try_spec_00 (§0^(m - G - 2)) (§0^i ++ [§1] ++ §0^(G - 2 - i) ++ l)); [by lia | by auto with M | by rewrite ?app_norm; do 3 f_equal; lia |]. rewrite ?app_norm. apply: maybe_index_try_stop. rewrite /maybe_index_try_stop_time. 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