proposition: Lemma confluent_M' : SSM.confluent M'.
proof: Proof. Proof using basic_M confluent_M. move=> ? ? ? /inverse_simulation /= H1 /inverse_simulation /= H2. have [? []] := confluent_M _ _ _ H1 H2. move=> /simulation /= ? /simulation /= ?. eexists. constructor; by eassumption. Qed.
imports: List Lia Relation_Operators Operators_Properties Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(Nat_facts List_facts SMN_facts) Undecidability.StackMachines.Util.SMN_transform ssreflect ssrbool ssrfun