proposition: Lemma reachable_n_dec (n: nat) (X Y: config) : decidable (reachable_n n X Y).
proof: Proof. elim: n X Y. { move=> X Y. have : {X = Y} + {X <> Y} by do 4 (decide equality). case. - move=> ->. left. by apply: rn_refl. - move=> ?. right. by move /reachable_0E. } move=> n IH X Y. have : {X = Y} + {X <> Y} by do 4 (decide equality). case. { move=> ->. left. by apply: rn_refl. } move=> ?. case: (Exists_dec (fun Z => reachable_n n X Z /\ step M Z Y) (space X)). - move=> Z. have := IH X Z. have := step_dec Z Y. by firstorder done. - move=> + /ltac:(left). rewrite Exists_exists. move=> [?] [?] [?] ?. apply: rn_step; by eassumption. - move=> H. right. move=> /reachable_SnE. case; first done. move=> [Z [? ?]]. apply: H. rewrite Exists_exists. exists Z. constructor; last by constructor. apply: spaceP0. apply: reachable_n_to_reachable. by eassumption. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM