proposition: Theorem confluent_M' : confluent M'.
proof: Proof. Proof using confluent_M lp_XY Y_fresh XY_neq. move=> x y1 y2. have : {get_state x = Y} + {get_state x <> Y} by decide equality. case; first last. { move=> *. apply: confluent_valid_M'; by eassumption. } move=> Hx /rt_rt1n Hxy1. case: Hxy1 Hx. { move=> *. eexists. constructor; first by eassumption. by apply: rt_refl. } move=> {}y1 y1' + + + /rt_rt1n Hxy2. case: Hxy2. - move=> ? /rt_rt1n ? ?. eexists. constructor; first by apply: rt_refl. apply: rt_trans; last by eassumption. by apply: rt_step. - move=> {}y2 y2'. move: x y1 y2 => [[l r] x] [[l1 r1] y1] [[l2 r2] y2]. move=> + + + + /= Hx. subst x. move=> /step_fresh_l [] ? ? ? + /step_fresh_l [] ? ? ?. subst. move=> /rt_rt1n H1 /rt_rt1n H2. by apply: confluent_valid_M'; [| by eassumption | by eassumption]. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun