proposition: Lemma confluent_M' : confluent M'.
proof: Proof. Proof using unique_step_l' unique_step_l derivable XY_neq confluent_M. move=> ? ? ? /rt_rt1n + /rt_rt1n. case. { move=> /rt_rt1n ?. eexists. constructor; first by eassumption. by apply: rt_refl. } move=> ? ? Hxy1 /rt_rt1n Hy1z1 Hxy2. case: Hxy2 Hxy1. { move=> ?. eexists. constructor; first by apply: rt_refl. apply: rt_trans; last by eassumption. by apply: rt_step. } move=> ? ? Hxy2 /rt_rt1n Hy2z2 Hxy1. move: Hy1z1 Hy2z2 => /simulation => /(_ _ Hxy1) Hy1z1 /simulation => /(_ _ Hxy2) Hy2z2. case: Hxy1 Hxy2 Hy1z1 Hy2z2 => v1 w1 >. rewrite /M' in_app_iff -/M'. case. - case; last done. move=> [] <- <- <- <- <- <- /=. move Hx: (v1, R ++ w1, X) => x Hxy2. case: Hxy2 Hx => v2 w2 >. rewrite /M' in_app_iff -/M'. case. { case; last done. move=> [] <- <- <- <- <- <- [] <- /app_inv_head <- /=. move=> /confluent_M => H /H => [[? [? ?]]]. eexists. constructor; apply: inverse_simulation; by eassumption. } move /transition => /(_ v2 w2) + H. rewrite -H. move=> Hxy2. move: Hxy2 (Hxy2) => /unique_step_l ->. move=> /(@rt_step Config) /(@rt_trans Config) => {}H + /H. have /reachable_stack_app := derivable. move=> /(_ (skipn 1 v1) w1) /(@rt_trans Config) => {}H /H. move=> /confluent_M => {}H /H [? [? ?]]. eexists. constructor; apply: inverse_simulation; by eassumption. - move /transition => /(_ v1 w1) Hxy2. move Hx: (c in step M' c _) => ? Hxy1. case: Hxy1 Hx Hxy2. move=> v2 w2 >. rewrite /M' in_app_iff -/M'. case. { case; last done. move=> [] <- <- <- <- <- <- /= ->. move=> Hxy1. move: Hxy1 (Hxy1) => /unique_step_l ->. move=> /(@rt_step Config) /(@rt_trans Config) => {}H /H Hxz1. have /reachable_stack_app := derivable. move=> /(_ (skipn 1 v2) w2) /(@rt_trans Config) => {}H /H. move: Hxz1=> /confluent_M {}H /H [? [? ?]]. eexists. constructor; apply: inverse_simulation; by eassumption. } move /transition => /(_ v2 w2) + ->. move=> /(@rt_step Config) /(@rt_trans Config) => {}H + + /H. move=> /(@rt_step Config) /(@rt_trans Config) => {}H /H. move=> /confluent_M => {}H /H [? [? ?]]. eexists. constructor; 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