  An inductive theorem proving method for constrained term rewriting systems,
which is based on rewriting induction, needs a decision procedure for
reduction-completeness of constrained terms. In addition, the sufficient
complete property of constrained term rewriting systems enables us to relax the
side conditions of some inference rules in the proving method. These two
properties can be reduced to intersection emptiness problems related to sets of
ground instances for constrained terms. This paper proposes a method to
construct deterministic, complete, and constraint-complete constrained tree
automata recognizing ground instances of constrained terms.
