  The following problem is shown undecidable: given regular languages L,K of
finite trees, decide if there exists a deterministic tree-walking automaton
which accepts all trees in L and rejects all trees in K. The proof uses a
technique of Kopczy\'nski from LICS 2016.
