We show that the monadic second-order theory of an infinite tree
recognized by a higher-order pushdown automaton of any level is
decidable. We also show that trees recognized by automata of
level n coincide with trees generated by safe higher-order grammars
of level n. Our decidability result extends the result of Courcelle
on algebraic (pushdown of level 1) trees and our own result on
trees of level 2.
