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