  We show the diagonal problem for higher-order pushdown automata (HOPDA), and
hence the simultaneous unboundedness problem, is decidable. From recent work by
Zetzsche this means that we can construct the downward closure of the set of
words accepted by a given HOPDA. This also means we can construct the downward
closure of the Parikh image of a HOPDA. Both of these consequences play an
important role in verifying concurrent higher-order programs expressed as HOPDA
or safe higher-order recursion schemes.
