proposition: Lemma deterministic_MN : deterministic MN.
proof: Proof. Proof using flip_consistent_MX deterministic_MX. move=> [[L R] X]. have [x [b_x [l [r [b_y Hx]]]]]:= inverse_simulation_step L R X. move=> [[? ?] ?] [[? ?] ?] /Hx + /Hx. move=> [y [ly [ry [{}Hx [-> Hy]]]]] [z [lz [rz [_ [-> Hz]]]]]. move: b_x b_y Hx Hy Hz. move=> [|] [|] ?; move /deterministic_MX => H /H; by congruence. 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