(0) Obligation:
Clauses:
e(X) :- ','(=(Y, .(e, .(o, Y))), c(Y, X)).
c(.(e, X1), 0).
c(.(X2, X), s(Y)) :- c(X, Y).
Query: e(g)
(1) PrologToTRSTransformerProof (SOUND transformation)
Transformed Prolog program to TRS.
(2) Obligation:
Q restricted rewrite system:
R is empty.
Q is empty.
(3) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(4) YES