Bounding finite-image sequences of length ${\omega }^k$

Given a well-quasi-order $X$ and an ordinal $\alpha$, the set $s_{\alpha }^F(X)$ of transfinite sequences on $X$ with length less than $\alpha$ and with finite image is also a well-quasi-order, as proven by Nash-Williams. Before Nash-Williams proved it for general $\alpha$, however, it was proven for $\alpha <{\omega }^{\omega }$ by Erdős and Rado. In this paper, we revisit Erdős and Rado’s proof and improve upon it, using it to obtain upper bounds on the maximum linearization of $s_{{\omega }^k}^F(X)$ in terms of $k$ and $o(X)$, where $o(X)$ denotes the maximum linearization of $X$. We show that, for fixed $k$, $o(s_{{\omega }^k}^F(X))$ is bounded above by a function which can roughly be described as $(k+1)$-times exponential in $o(X)$. We also show that, for $k\le 2$, this bound is not far from tight.