proposition: Lemma space_length {X Y: config} : width X <= width Y -> length (space X) <= length (space Y).
proof: Proof. rewrite /space => /=. move: (width X) => l1. move: (width Y) => l2. clear. move=> H. apply: le_n_S. apply: length_flat_map_le; first by lia. move=> i. rewrite ? length_enum_configs ? length_enum_stacks. have ?: 2 ^ (l1 - i) <= 2 ^ (l2 - i). { apply: Nat.pow_le_mono_r; by lia. } suff : 2 ^ i * 2 ^ (l1 - i) <= 2 ^ i * 2 ^ (l2 - i) by nia. by nia. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM