⁶That is, theories where every rewrite step is performed only at the top position of the term. In such theories completeness can be simplified as follows: given $\exists <!--FUNCTION\; APPLICATION-->x_1,\dots ,x_{k}s{\to }^{\ast }t$, for each $\rho$ such that $\rho (s){\to }_{R,Ax}^{\ast }\rho (t)$, and for all the substitutions ${\sigma }_1,\dots ,{\sigma }_n,\dots$ provided by narrowing from $s$, there is an index $i$ and a substitution $\tau$ such that $\rho {=}_{Ax}{\sigma }_i;\tau$.