Tree generating regular systems

Trees are defined as mappings from tree structures (in the graph-theoretic sense) into sets of symbols.Regular systems are defined in which the production rules are of the form Φ → ψ, where Φ and ψ are trees. An application of a rule involves replacing a subtree Φ by the tree ψ.The main result is that the sets of trees generated by regular systems are exactly those that are accepted by tree automata. This generalizes a theorem of BÜchi, proved for strings