proposition: Lemma bounded_MX : SMX.bounded MX (2*NMN).
proof: Proof. Proof using bounded_MN. rewrite /SMX.bounded. move=> [[l r] x]. have [T [H1T H2T]]:= bounded_MN (encode_Stack l, encode_Stack r, encode_State (x, false)). exists ((map (fun '(L, R, X) => (decode_Stack L, decode_Stack R, fst (decode_State X))) T) ++ (map (fun '(L, R, X) => (decode_Stack R, decode_Stack L, fst (decode_State X))) T)). constructor; first last. { rewrite ?app_length ?map_length. move: (length T) H2T. by lia. } move=> [[l' r'] y] /simulation /=. rewrite ?in_app_iff ?in_map_iff. move=> [] _ [Hxy|Hxy]. - left. exists (encode_Stack l', encode_Stack r', to_nat (y, false)). rewrite ?decode_encode_Stack /decode_State ?enumP /=. constructor; first done. by apply: H1T. - right. exists (encode_Stack r', encode_Stack l', to_nat (y, true)). rewrite ?decode_encode_Stack /decode_State ?enumP /=. constructor; first done. by apply: H1T. 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