(0) Obligation:
Clauses:
h(X) :- ','(f(X), g(X)).
f(c(0, X1)) :- !.
f(c(X, Y)) :- ','(p(X, P), f(c(P, s(Y)))).
g(c(X2, 0)) :- !.
g(c(X, Y)) :- ','(p(Y, P), g(c(s(X), P))).
p(0, 0).
p(s(X), X).
Query: h(g)
(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)
The root node satisfies the determinacy criterion.
(2) YES