proposition: Lemma simulation_step_false {l r x l' r' y} : SMX.step MX (l, r, x) (l', r', y) -> step MN (encode_Stack l, encode_Stack r, to_nat (x, false)) (encode_Stack l', encode_Stack r', to_nat (y, false)) \/ step MN (encode_Stack l, encode_Stack r, to_nat (x, false)) (encode_Stack r', encode_Stack l', to_nat (y, true)).
proof: Proof. move Hc: (l, r, x) => c. move Hd: (l', r', y) => d Hcd. case: Hcd Hc Hd. move=> v w r1 s1 r2 s2 x' y' [|] HMX [] ? ? ? [] ? ? ?; subst. - right. rewrite ?encode_Stack_app. apply: transition. rewrite in_flat_map. eexists. constructor; first by eassumption. by left. - left. rewrite ?encode_Stack_app. apply: transition. rewrite in_flat_map. eexists. constructor; first by eassumption. by left. 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