proposition: Lemma maybe_goto_1_far {l r m n X Y z T} : (NP * step_time CP TP + 2) <= T -> G + (CP+1) <= m -> maybe_reachable T (l, §0^m ++ r, goto n X Y) z.
proof: Proof. Proof using NP_spec. move=> ? ?. suff: maybe_reachable (NP * step_time CP TP + 2) (l, §0^(G + (CP+1)) ++ §0^(m-(G + (CP + 1))) ++ r, goto n X Y) z. { apply maybe_reachable_mon'; first by lia. rewrite ?app_norm. do 5 f_equal. by lia. } have := in_dec _ (n, X, Y) gotos. move=> /(_ ltac:(do 4 (decide equality))) [/gotos_igotos [i ?]| ?]; first last. { apply: terminal_maybe_reachable. by apply: not_in_gotos_terminal. } apply: (maybe_first_step (goto_spec_G (i, (n, X, Y))) l (§0^(CP + 1) ++ §0^(m-(G + (CP + 1))) ++ r)); [by lia | by auto with M | by rewrite ?app_norm |]. have ? := CP_pos. apply: (maybe_first_step bound_try_spec_00 (§0^(CP - 1 + (m - (G + (CP + 1)))) ++ r) (§0^i ++ [§1] ++ §0^(G - 2 - i) ++ l)); [by lia | by auto with M | rewrite ?app_norm; do 4 f_equal; lia |]. have := maybe_index_try_run ((§0^i ++ [§1] ++ §0^(G - 2 - i)) ++ l) (§0^(m - (G + (CP + 1))) ++ r) z. apply: maybe_reachable_mon'; [by lia | by rewrite ?app_norm]. 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