proposition: Lemma simulation {x y} : reachable M x y -> SSM.reachable M' x y.
proof: Proof. Proof using basic_M. elim. - move=> ? ? /simulation_step ?. by apply: rt_step. - move=> *. by apply: rt_refl. - move=> *. apply: rt_trans; 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