proposition: Lemma synchronize {x y} : reachable M' x y -> exists z1 z2, reachable_n M' 1 x z1 /\ reachable_n M' 1 z2 y /\ reachable M z1 z2.
proof: Proof. Proof using lp_XY Y_fresh XY_neq. move /rt_rt1n. case. { exists x, x. constructor; first by apply: rn_refl. constructor; first by apply: rn_refl. by apply: rt_refl. } move=> ? ? + /rt_rt1n /rt_rtn1 Hz1y. case: Hz1y. { move /synchronize_step => [z] [? [? ?]]. exists z, z. constructor; first done. constructor; first done. by apply: rt_refl. } move=> ? ? /synchronize_step => [[z2]] [/reachable_n_to_reachable ? [? ?]]. move=> /rt_rtn1 ? /synchronize_step => [[z1]] [? [/reachable_n_to_reachable ? ?]]. exists z1, z2. constructor; first done. constructor; first done. apply: simulation'; [| done | done]. apply: rt_trans; first by eassumption. by apply: rt_trans; first by eassumption. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun