proposition: Lemma maybe_index_try_futile l m i z : maybe_reachable maybe_index_try_futile_time (l, §0^m, '#?i) z.
proof: Proof. Proof using NP_spec. rewrite /maybe_index_try_futile_time. move: l => [|a l]. { by apply: terminal_maybe_reachable => ? /index_try_step_shape [? ?]. } case: a. { by apply: terminal_maybe_reachable => ? /index_try_step_shape [? ?]. } have [-> | ?] : m = 0 \/ 1 <= m by lia. { by apply: terminal_maybe_reachable => ? /index_try_step_shape [? ?]. } have [? | /in_iPI [j [n Hijn]]]: length P <= i \/ i < length P by lia. { apply: terminal_maybe_reachable. by apply: large_index_terminal. } apply: (maybe_first_step (index_try_spec (i, (j, n))) l (§0^(m-1))); [ 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. 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