proposition: Lemma concat_reachable {M} {NM: nat} (xs : list Config) : bounded M NM -> exists L, (forall x y, In x xs -> reachable M x y -> In y L) /\ length L <= NM * length xs.
proof: Proof. move=> bounded_M. elim: xs. { exists []. constructor; [done | by (move=> /=; lia) ]. } move=> x xs [Lxs [HLxs ?]]. have [Lx [HLx ?]] := bounded_M x. exists (Lx ++ Lxs). constructor; last by (rewrite app_length /=; lia). move=> ? ? /=. rewrite in_app_iff. case. - move=> <- /HLx *. by left. - move=> *. right. apply: HLxs; by eassumption. Qed.
imports: Arith Lia Relation_Operators Operators_Properties List Undecidability.StackMachines.Util(Nat_facts List_facts) Undecidability.StackMachines.SMN ssreflect ssrbool ssrfun