proposition: Lemma reachable_n_reachable {M T x y} : reachable_n M T x y -> reachable M x y.
proof: Proof. elim: T x y. { move HT: (0) => T x y Hxy. case: Hxy HT => *; [by apply: rt_refl | by lia]. } move=> T IH x y. move HT': (S T) => T' Hxy. case: Hxy HT'; first by (move=> *; apply: rt_refl). move=> {}T' {}x z {}y /(@rt_step Config) Hxz + ?. have ->: T' = T by lia. move /IH. by apply: rt_trans. Qed.
imports: List Lia Relation_Operators Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.Reductions.CM1_HALT_to_SMNdl_UB.SMX ssreflect ssrbool ssrfun