proposition: Lemma reachable_configurations {T x z} : reachable_n T x z -> terminal M z -> exists L, (forall y, SM.reachable M x y -> In y L) /\ length L <= S T.
proof: Proof. elim: T x z. { move=> x z. move HT: (0) => T Hxz. case: Hxz HT; last done. move=> ? {}x <- Hx. exists [x]. constructor; last by (move=> /=; lia). move=> y /clos_rt_rt1n_iff Hxy. case: Hxy Hx; first by (move=> *; left). by move=> > + ? Hx => /Hx. } move=> T IH x z. move HT': (S T) => T' Hxz. case: Hxz HT'. { move=> ? {}x <- Hx. exists [x]. constructor; last by (move=> /=; lia). move=> y /clos_rt_rt1n_iff Hxy. case: Hxy Hx; first by (move=> *; left). by move=> > + ? Hx => /Hx. } move=> {}T' {}x y {}z Hxy Hyz ?. have ?: T = T' by lia. subst T'. move /(IH y _ Hyz) => [L [H1L H2L]]. exists (x :: L). constructor; first last. { rewrite /length -/(length _). by lia. } move=> y'. move HT': (1 + T) => T' /clos_rt_rt1n_iff Hxy'. case: Hxy' HT' Hxy; first by (move=> *; left). move=> {}y' z' Hxy' Hy'z' ? Hxy. right. apply: H1L. have -> : y = y' by apply: deterministic_M; eassumption. by apply /clos_rt_rt1n_iff. Qed.
imports: Relation_Operators Operators_Properties Lia PeanoNat List Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.SMX_facts Undecidability.StackMachines.Util(Nat_facts List_facts) ssreflect ssrbool ssrfun