proposition: Lemma simulation {x y z} : step M' x y -> reachable M' y z -> reachable M y z.
proof: Proof. Proof using unique_step_l' unique_step_l derivable XY_neq. move=> Hxy. move /rt_rtn1. elim; first by apply: rt_refl. move=> y' {}z Hy'z. case: Hy'z. move=> v w >. rewrite /M' in_app_iff. case; first last. { move /transition => *. apply: rt_trans; first by eassumption. by apply: rt_step. } case; last done. move=> [] <- <- <- <- <- <-. rewrite -/M'. clear y'. move Hy': ([] ++ v, R ++ w, X) => y' Hyy'. case: Hyy' Hy' Hxy. { move=> <- /= /unique_step_M'l' -> _. by apply: reachable_stack_app. } move=> {}y' {}z + + ?. subst z. move=> /= /unique_step_M'l' -> *. apply: rt_trans; first by eassumption. by apply: reachable_stack_app. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun