proposition: Lemma confluent_valid_M' {x y1 y2} : valid_state (get_state x) -> reachable M' x y1 -> reachable M' x y2 -> exists z : Config, reachable M' y1 z /\ reachable M' y2 z.
proof: Proof. Proof using confluent_M lp_XY Y_fresh XY_neq. move=> Hx Hxy1 Hxy2. move: (Hxy1) => /continue => /(_ Hx). move=> [z1 [Hy1z1 ?]]. move: (Hxy2) => /continue => /(_ Hx). move=> [z2 [Hy2z2 ?]]. have Hxz1 : reachable M x z1. { apply: simulation'; [| done | done]. by apply: rt_trans; last by eassumption. } have Hxz2 : reachable M x z2. { apply: simulation'; [| done | done]. by apply: rt_trans; last by eassumption. } have [? [? ?]]:= confluent_M Hxz1 Hxz2. eexists. constructor; (apply: rt_trans; first by eassumption); apply: inverse_simulation'; by eassumption. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun