proposition: Lemma maybe_index_try_run l r z : maybe_reachable (NP * step_time CP TP) ([§1] ++ l, [§0] ++ [§1] ++ §0^(CP-1) ++ r, '#?0) z.
proof: Proof. Proof using NP_spec. right. have := iter_cm_step HTP l r NP. rewrite -/cm_end /= -/CP. move /(_ ltac:(lia)) => ?. eexists. constructor; first by eassumption. apply: large_index_terminal. suff : not (CM.state cm_end < length P) by lia. move /CM_facts.step_progress => /(_ CP_pos). move: (NP_spec). rewrite -/cm_end /CM.halting. move=> -> [|]; last by lia. move /(f_equal CM.state) => /=. 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