proposition: Lemma deterministic_confluent {M} : deterministic M -> confluent M.
proof: Proof. move=> HM ? ? + /rt_rt1n Hxy1. elim: Hxy1. { move=> *. eexists. by constructor; last by apply: rt_refl. } move=> ? ? ? Hxy1 /rt_rt1n Hy1z1 IH ? /rt_rt1n Hxy2. case: Hxy2 Hxy1. - move=> ?. eexists. constructor; first by apply: rt_refl. apply: rt_trans; last by eassumption. apply: rt_step. by eassumption. - move=> > Hxy2 /rt_rt1n Hy2z2 Hxy1. have ? := HM _ _ _ Hxy1 Hxy2. subst. by apply: IH. Qed.
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun