Description
This page accompanies a paper that will be presented at CPP 2021.
We present a formalization (in Isabelle/HOL, on top of IsaFoR) of a decision procedure of the first-order theory of rewriting for linear, variable-separated rewrite systems.