proposition: Lemma reachable_n_bounded {X Y: config} {n: nat} {L: list config} : (forall Z, reachable_n n X Z -> In Z L) -> reachable_n n X Y -> reachable_n (length L) X Y.
proof: Proof. elim /(Nat.measure_induction _ id): n L X Y. case. { move=> /= *. apply: reachable_n_monotone; last by eassumption. by lia. } move=> n IH L X Y HL. case: (reachable_n_dec n X Y) => HXY. { move=> _. apply: (IH n ltac:(lia)); last by eassumption. move=> ? ?. apply: HL. apply: reachable_n_monotone; last by eassumption. by lia. } move=> H'XY. have := HL _ H'XY. move /(@in_split config) => [L1 [L2 ?]]. subst L. move: H'XY => /reachable_SnE. case. { move=> ->. by apply: rn_refl. } move=> [Z [HXZ HZY]]. rewrite ?app_length /length -?/(length _). have ->: (length L1 + S (length L2)) = 1 + length (L1 ++ L2) by rewrite app_length; lia. apply: rn_step; last by eassumption. apply: (IH n ltac:(lia)); last by eassumption. move=> Z' HXZ'. have HYZ' : Y <> Z' by move=> ?; subst. move: HXZ' HYZ' => /reachable_n_monotone => /(_ (1+n) ltac:(lia)) /HL. rewrite ?in_app_iff /In -?/(In _ _). clear. by firstorder done. Qed.
imports: PeanoNat Lia Relation_Operators Operators_Properties List ssreflect ssrfun ssrbool Undecidability.StackMachines.SSM