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