proposition: Lemma reachable_dec (X Y: config) : decidable (reachable M X Y).
proof: Proof. have := reachable_n_dec (length (space X)) X Y. case=> HXY; [left | right]. - apply: reachable_n_to_reachable. by eassumption. - move /reachable_to_reachable_n => [n H'XY]. apply: HXY. apply: reachable_n_bounded; last by eassumption. move=> *. apply: spaceP0. apply: reachable_n_to_reachable. by eassumption. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM