We investigate the problem of deciding first-order theories of finite trees
with several distinguished congruence relations, each of them given by some
equational axioms. We give an automata-based solution for the case where the
different equational axiom systems are linear and variable-disjoint (this
includes the case where all axioms are ground), and where the logic does not
permit to express tree relations x = f(y,z). We show that the problem is
undecidable when these restrictions are relaxed. As motivation and
application, we show how to translate the model-checking problem of ApiL, a
spatial equational logic for the applied pi-calculus, to the validity of
first-order formulas in term algebras with multiple congruence relations.