proposition: Lemma reachable_app {x x': state} {A B A' B' C D: stack} : reachable M (A, B, x) (A', B', x') -> reachable M (A++C, B++D, x) (A'++C, B'++D, x').
proof: Proof. move HX: (A, B, x) => X. move HX': (A', B', x') => X'. move=> H. elim: H C D x x' A B A' B' HX HX'; clear. - move=> X X'. case; clear. + move=> > H >. case=> -> -> ->. case=> -> -> ->. apply: rt_step. by apply: step_l. + move=> > H >. case=> -> -> ->. case=> -> -> ->. apply: rt_step. by apply: step_r. - move=> > <-. case=> -> -> ->. by apply: rt_refl. - move=> X [[A' B'] x'] Z ? IHXY ? IHYZ *. apply: rt_trans; [by apply: IHXY | by apply: IHYZ]. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM