(0) Obligation:

Clauses:

n :- ','(=(X, f(1, f(0, X))), g(X)).
g(f(X, f(X, X1))) :- !.
g(f(X2, X)) :- g(X).

Query: n()

(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