proposition: Lemma reachable_n_stack_app {M n l r x l' r' y v w} : reachable_n M n (l, r, x) (l', r', y) -> reachable_n M n (l ++ v, r ++ w, x) (l' ++ v, r' ++ w, y).
proof: Proof. elim: n l r x l' r' y. { move=> > /reachable_0E [] <- <- <-. apply: rn_refl. } move=> n IH l r x l' r' y /reachable_SnE [[] <- <- <- | [z] [+]]; first by apply: rn_refl. move Hx': (l, r, x) => x' Hx'z. case: Hx'z Hx'. move=> > H [] -> -> -> /IH {}IH. apply: rn_step; last by eassumption. rewrite -?app_assoc. by apply: transition. Qed.
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun