Left Termination of the query pattern minus_in_3(g, g, a) w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

minus(X, Y, Z) :- ','(f(X, 0), ','(!, =(Z, 0))).
f(X, Y) :- ','(!, =(X, Y)).
f(X, Y) :- f(X, Y).
=(X, X).

Queries:

minus(g,g,a).

(1) BuiltinConflictTransformerProof (SOUND transformation)

Renamed defined predicates conflicting with built-in predicates [PROLOG].

(2) Obligation:

Clauses:

minus(X, Y, Z) :- ','(f(X, 0), ','(!, user_defined_=(Z, 0))).
f(X, Y) :- ','(!, user_defined_=(X, Y)).
f(X, Y) :- f(X, Y).
user_defined_=(X, X).

Queries:

minus(g,g,a).

(3) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(4) Obligation:

Triples:


Clauses:


Afs:

(5) TPisEmptyProof (EQUIVALENT transformation)

There are no more dependency triples. Hence, the dependency triple problem trivially terminates.

(6) YES