Ground Term Rewriting
Sándor Vágvölgyi · Bulletin of the European Association for Theoretical Computer Science · 2013
We study the notion of a stub equality for a congruence generated by a ground term rewrite system (GTRS). We study the congruence generated by the union of GTRSs $R$ and $S$, where the congruences generated by $R$ and $S$ intersect with respect to their stubs. We show that for any equivalent reduced GTRSs $R$ and $S$, the same number of terms appear as subterms in $R$ as in $S$. We give an upper bound on the number of reduced GTRSs equivalent to a given reduced GTRS $R$. We show that for any convergent GTRS $R$, one can construct an equivalent reduced GTRS $V$ such that $\red V\subseteq \tred R$.