On Nash-Williams' Theorem regarding sequences with finite range

The famous theorem of Higman states that for any well-quasi-order (wqo) Q the embeddability order on finite sequences over Q is also wqo. In his celebrated 1965 paper, Nash-Williams established that the same conclusion holds even for all the transfinite sequences with finite range, thus proving a far reaching generalization of Higman's theorem. In the present paper we show that Nash-Williams' Theorem is provable in the system ATR₀ of second-order arithmetic, thus solving an open problem by Antonio Montalb\'an and proving the reverse-mathematical equivalence of Nash-Williams' Theorem and ATR₀. In order to accomplish this, we establish equivalent characterization of transfinite Higman's order and an order on the cumulative hierarchy with urelements from the starting wqo Q, and find some new connection that can be of purely order-theoretic interest. Moreover, in this paper we present a new setup that allows us to develop the theory of α-wqo's in a way that is formalizable within primitive-recursive set theory with urelements, in a smooth and code-free fashion.