A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems.