proposition: Lemma inverse_simulation_step {x y} : SSM.step M' x y -> step M x y.
proof: Proof. Proof using basic_M. case=> >. - rewrite /M' in_map_iff. move=> [[[[l r] {}x] [[l' r'] {}y]]] [] + HM. move: HM (HM) => /basic_instructions. move H1op: (l, r, x, (l', r', y)) => op H2op. case: H2op H1op. + move=> > /=. by congruence. + move=> > [] /= ? ? ? ? ? ? + [] *. subst. move /transition. by apply. - rewrite /M' in_map_iff. move=> [[[[l r] {}x] [[l' r'] {}y]]] [] + HM. move: HM (HM) => /basic_instructions. move H1op: (l, r, x, (l', r', y)) => op H2op. case: H2op H1op. + move=> > [] /= ? ? ? ? ? ? + [] *. subst. move /transition. by apply. + move=> > /=. by congruence. 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