(0) Obligation:

Clauses:

e(X) :- ','(=(Y, f(e, f(o, Y))), ','(!, c(Y, X))).
e(X) :- e(X).
c(f(e, X1), 0).
c(f(X2, X), s(Y)) :- c(X, Y).

Query: e(g)

(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)

The root node satisfies the determinacy criterion.

(2) YES