⁶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 ∃X₁,…,X_ks →^∗t, for each ρ such that ρ(s) →_R,Ax^∗ρ(t), and for all the substitutions σ₁,…,σ_n,… provided by narrowing from s, there is an index i and a substitution τ such that ρ = _Axσ_i; τ.