(0) Obligation:
Clauses:
rev(L, R) :- rev(L, [], R).
rev([], Y, Z) :- ','(!, eq(Y, Z)).
rev(L, S, R) :- ','(head(L, X), ','(tail(L, T), rev(T, .(X, S), R))).
head([], X1).
head(.(X, X2), X).
tail([], []).
tail(.(X3, Xs), Xs).
eq(X, X).
Query: rev(g,a)
(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)
The root node satisfies the determinacy criterion.
(2) YES