Thus ψ is a reducing substitution for c and ρ. Lemma 3 ensures that there exists a reducing substitution for every derivation of an acyclic f-structure F in G. By Lemma 2 we know that such a substitution preserves equivalence.
14 the collections of instantiated rules that result from the derivations for F and their reducing substitutions must belong to the set consisting of all possible collections of appropriately instantiated and pair-wise compatible rules that together provide descriptions of F. If we extend the Inst function in the obvious way to sets of instantiated rules IR then this set is defined as follows.