proposition: Lemma bounded_M' NM : bounded M NM -> bounded M' (1 + NM * length M').
proof: Proof. Proof using unique_step_l' unique_step_l derivable XY_neq non_nil. move=> bounded_M x. have [ys [Hys H'ys]] := next_configs M' x. have [L [HL H'L]] := concat_reachable ys bounded_M. exists ([x] ++ L). constructor; first last. { move: H'ys H'L. rewrite app_length /=. by nia. } move=> ? /rt_rt1n Hxz. rewrite in_app_iff. case: Hxz Hys; first by (move=> *; left; left). move=> ? ? Hxy + Hys. move: Hxy (Hxy) => /Hys ? /simulation Hyz /rt_rt1n ?. right. apply: HL; [by eassumption | by apply: Hyz]. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun