proposition: Theorem deterministic_M : SM.deterministic M.
proof: Proof. move=> X Y Z + /stepE [] > H2X -> * => /stepE [] > H1X -> *; move: H2X H1X => -> []; rewrite ?app_singP ?app_repeat_cons /=; try congruence; move=> *; subst. all: (do ? unify_iP); (do ? unify_app); (do ? unify_igotos); try by [| congruence]. Qed.
imports: Relation_Operators Operators_Properties Lia PeanoNat List Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.SMX_facts Undecidability.StackMachines.Util(Nat_facts List_facts) ssreflect ssrbool ssrfun