Reference for tree of bad sequences of WPO

Question

I'm looking for a reference to give in Wikipedia for the following result: Let $X$ be a WPO. Let $T_X$ be the tree of bad sequnces of $X$, and let $o(X)$ be the ordinal height of the root of $T_X$. Then there exists a linearization of $X$ that achieves ordinal type $o(X)$.

I see that van der Meeren in his 2015 PhD thesis states this result (right after Theorem 1.54), and credits de Jongh and Parikh (1979).

Indeed the result follows from Lemma 2.6 and Corollary 2.14 in de Jongh and Parikh. But the result is very "buried", and the reader has to do a lot of work of putting things together. They do not explicitly talk about the tree of bad sequences, nor about its height. The reader has to recall that the ordinal height of a node in a tree is given by $o(v) = \lim_{w \text{ child of } v} (o(w)+1)$, and see that the relation between $o(X)$ and $l(x)$ in de Jongh and Parikh, together with the fact that no linearization can exceed the height of $T_X$, yields the desired result.

What is a good reference for this result, that one can give in Wikipedia?

Answer 1

OK I found an answer myself. Blass and Gurevich (2008) fill in the missing details (and reprove the result in its entirety).

Andreas Blass and Yuri Gurevich, Program termination and well partial orderings, ACM Transactions on Computational Logic 9(3), article 18, 26 pages, 2008. https://doi.org/10.1145/1352582.1352586