Descendants of a recognizable tree language for sets of linear monadic term rewrite rules

For a tree language L and a set S of term rewrite rules over Σ, the descendant of L for S is the set S∗(L) of trees reachable from a tree in L by rewriting in S. For a recognizable tree language L, we study the set D(L) of descendants of L for all sets of linear monadic term rewrite rules over Σ. We show that D(L) is finite. For each tree automaton A over Σ, we can effectively construct a set {R1,…,Rk} of linear monadic term rewrite systems over Σ such that and for any 1⩽i