proposition: Lemma bounded_M' NM : bounded M NM -> bounded M' (NM * (1 + length M') * (1 + length M') * 4).
proof: Proof. Proof using lp_XY Y_fresh XY_neq. move=> bounded_M. move=> x. have [Lx [HLx H2Lx]] := next_n_configs M' 1 [x]. have [L2x [HL2x H2L2x]] := concat_reachable Lx bounded_M. have [L3x [HL3x H2L3x]] := next_n_configs M' 1 L2x. exists L3x. constructor. - move=> ? /synchronize => [[z1]] [z2] [/HLx] /(_ ltac:(by left)). by move /HL2x => H [+ /H /HL3x {}H] => /H. - suff : length L2x <= NM * (1 + length M') * 2 by move: H2L3x => /=; clear; nia. move: H2Lx H2L2x => /=. clear. by nia. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun