proposition: Lemma continue {x y} : reachable M' x y -> valid_state (get_state x) -> exists z, reachable M' y z /\ valid_state (get_state z).
proof: Proof. Proof using lp_XY Y_fresh XY_neq. have : {get_state y = Y} + {get_state y <> Y} by decide equality. case; first last. { move=> *. eexists. by constructor; first by apply: rt_refl. } move=> Hy. move /rt_rtn1 => Hxy. case: Hxy Hy; first by congruence. move=> ? ? /step_app. case; first last. { case=> >. have := Y_fresh. rewrite Forall_forall => H /H /= []. by congruence. } case=> v w > /= [|[|]]; [| by congruence | done]. move=> [] <- <- <- <- <- <- _ _ _. exists (L ++ v, R ++ w, X). constructor; last done. apply: rt_step. apply: transition. right. by left. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun