We will use the following notation for an active lemma and its selected element:
where 
is an active lemma and i ( 
) is the index of the selected element in the body of the
lemma. We will call such structure an active item. The
structure of unit lemmas will be represented as:
where 
indicates that since the body of the lemma is empty
the selected element is also. We will call such structures passive items.
When new lemmas are generated, the actual
selection function determines the next element to process.
This is either an element of the body of a lemma in the case the new
lemma is non-unit, or for unit lemmas.