proposition: Lemma simulation_step {x y} : step M x y -> SSM.step M' x y.
proof: Proof. Proof using basic_M. case=> v w l r l' r' {}x {}y Hop. move: Hop (Hop) => /basic_instructions. move H1op: (l, r, x, (l', r', y)) => op H2op. case: H2op H1op. - move=> > [] *. subst. apply: SSM.step_r. rewrite /M' in_map_iff. eexists. by constructor; last by eassumption. - move=> > [] *. subst. apply: SSM.step_l. rewrite /M' in_map_iff. eexists. by constructor; last by eassumption. Qed.
imports: List Lia Relation_Operators Operators_Properties Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(Nat_facts List_facts SMN_facts) Undecidability.StackMachines.Util.SMN_transform ssreflect ssrbool ssrfun