(0) Obligation:
Clauses:
add(X, 0, X).
add(X, Y, s(Z)) :- ','(\+(isZero(Y)), ','(p(Y, P), add(X, P, Z))).
p(0, 0).
p(s(X), X).
isZero(0).
Query: add(a,g,a)
(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)
The root node satisfies the determinacy criterion.
(2) YES