proposition: Lemma simulation {n x y} : reachable_n M' n x y -> valid_state (get_state x) -> valid_state (get_state y) -> reachable_n M n x y.
proof: Proof. Proof using lp_XY Y_fresh XY_neq. elim: n x y; first by (move=> > /reachable_0E -> *; apply: rn_refl). move=> n IH x y /reachable_SnE [|]; first by (move=> -> *; apply: rn_refl). move=> [z1]. have : {get_state z1 = Y} + {get_state z1 <> Y} by decide equality. case; first last. { move=> Hz1 [Hxz1] /IH {}IH Hx ?. apply: rn_step; last by apply: IH. move: Hxz1 Hx Hz1 => /step_app. case; last done. case=> > [|[|]]; move=> [] /= *; by congruence. } move: n IH => [|n] IH; first by (move=> ? [_ /reachable_0E ?]; congruence). move=> + [+ /reachable_SnE H]. case: H; first by congruence. move=> [z2] [+]. move: z1 => [[l1 r1] z1] /= + + ?. subst z1. move: x z2 => [[l r] x] [[l2 r2] z2]. move=> /step_fresh_l [] ? ? ? + /step_fresh_r [] => *. subst. apply: (reachable_n_monotone (m := S n)); first by lia. apply: IH; [|done|done]. apply: reachable_n_monotone; last by eassumption. by lia. Qed.
imports: Relation_Operators Operators_Properties List Lia PeanoNat Undecidability.StackMachines.SMN Undecidability.StackMachines.Util(List_facts SMN_facts) ssreflect ssrbool ssrfun