proposition: Theorem length_preserving_MN : length_preserving MN.
proof: Proof. Proof using length_preserving_MX. move=> s t X s' t' Y. rewrite /MN in_flat_map /encode_Instruction. move=> [[[[[? ?] ?] [[? ?] ?]] b]] [/length_preserving_MX [H1 H2]]. case: b; (case; last (case; last done)). all: move=> [] *; subst; move: H1 H2; rewrite /encode_Stack ?app_length ?map_length; by lia. Qed.
imports: Relation_Operators Lia PeanoNat List Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(Nat_facts List_facts Enumerable) Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.CM1_to_SMX ssreflect ssrbool ssrfun