(0) Obligation:

Clauses:

f(c(s(X), Y)) :- f(c(X, s(Y))).
g(c(X, s(Y))) :- g(c(s(X), Y)).
h(X) :- ','(f(X), g(X)).

Query: h(g)

(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)

The root node satisfies the determinacy criterion.

(2) YES