proposition: Lemma synchronize_step {x y} : step M' x y -> exists z, reachable_n M' 1 x z /\ reachable_n M' 1 z y /\ valid_state (get_state z).
proof: Proof. Proof using lp_XY Y_fresh XY_neq. move=> /[dup] [[]] >. rewrite /M' in_app_iff -/M'. move=> [[|[|]]|]. - move=> [] <- <- <- <- <- <- ?. eexists. constructor; first by apply: rn_refl. by constructor; first by (apply: rn_step; [by eassumption | by apply: rn_refl]). - move=> [] <- <- <- <- <- <- ?. eexists. constructor; first by (apply: rn_step; [by eassumption | by apply: rn_refl]). by constructor; first by apply: rn_refl. - done. - have := Y_fresh. rewrite Forall_forall => H /H [? ?] ?. eexists. constructor; first by apply: rn_refl. by constructor; first by (apply: rn_step; [by eassumption | by apply: rn_refl]). Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun