proposition: Lemma index_yes_step_shape {y l r i j n} : In (i, (j, n)) iP -> SMX.step M (l, r, '#+ i) y -> (r = [§1] ++ skipn 1 r) \/ (r = §0^(1+n) ++ skipn (n+1) r).
proof: Proof. move=> H1i /stepE [] > [] *; subst; try done. - by left. - right. move Hn': (n' in §0^(1 + n') ++ _) => n'. have [_ <-] := in_iP_unique (n := n) (n' := n') ltac:(eassumption) ltac:(subst; eassumption). rewrite skipn_app repeat_length (_ : n + 1 - (1 + n) = 0); first by lia. by rewrite skipn_all2; first by (rewrite repeat_length; 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