Tree automata for rewrite strategies

For a constructor-based rewrite system R, a regular set of ground terms E, and assuming some additional restrictions, we build finite tree automata that recognize the descendants of E, i.e. the terms issued from E by rewriting, according to innermost, outermost, leftmost, and innermost-leftmost strategies.