The next transformation step transforms clauses represented as into clauses (only information contained in is needed). clauses are RELFUN clauses with the following features:

• structures and lists are represented by LL constructors, selectors, and test predicates,
• the premises have already been ordered such that all arguments are ground and test predicates come before selectors,
• unification (i.e., each entry in ) has been transformed into assignments (via is) and equality tests (via equal),
• expressions have been inserted as arguments for other expressions when possible, and
• all cuts are removed (this is allowed since clauses are only used as an intermediate representation).

For our example, the following clauses created:

fac/2-1(Arg#1) :- equal(0, Arg#1) & 1.
fac/2-1(Arg#1) :-& *(Arg#1, fac/2-1(-(Arg#1, 1))).

f/2-1(Arg#1) :-
         structp(Arg#1),
         equal(s, functor(Arg#1)),
         equal(2, arity(Arg#1)),
         X is elt(Arg#1, 0),
         equal(X, fac/2-1(X)),
         Y is elt(Arg#1, 1),
         equal(X, -(Y, X)),
         equal(Y, fac/2-1(Y))
         & struct(u, Arg#1, Arg#1).
f/2-1(Arg#1) :-& cons(Arg#1, cons(Arg#1, nil)).