proposition: Lemma stepE X Y : SM.step M X Y -> step_spec X Y.
proof: Proof. case=> >. rewrite /M ?in_app_iff -?lock. move=> [|[|[|]]]. - rewrite /index_ops ?in_app_iff ?in_map_iff. move=> [|[|[|]]] [[? [? ?]]] [[]] *; subst; by eauto using step_spec. - rewrite /increase_ops ?in_app_iff ?in_map_iff. move=> [|[|[|]]] [[? [? ?]]] [[]] *; subst; rewrite ?app_norm; by eauto using step_spec. - rewrite /goto_ops ?in_app_iff in_flat_map ?in_map_iff. move=> [|]. + move=> [[? [[? ?] ?]]] [[]] *. subst. rewrite ?app_norm. by eauto using step_spec. + move=> [?]. rewrite in_seq in_map_iff. move=> [[? ?]] [[? [[? ?] ?]]] [[]] *. subst. rewrite ?app_norm. by eauto using step_spec. - rewrite /bound_ops ?in_app_iff in_map_iff. move=> [|]. + move=> [[? [[? ?] ?]]] [[]] *. subst. rewrite ?app_norm. by eauto using step_spec. + move=> [|[|]]; (case; last done); move=> [] *; subst; rewrite -?app_assoc; by eauto using step_spec. 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