(0) Obligation:
Clauses:
minus(X, Y, Z) :- ','(=(X, 0), ','(!, =(Z, 0))).
minus(X, Y, Z) :- ','(=(Y, 0), ','(!, =(Z, X))).
minus(X, Y, Z) :- ','(=(X, s(A)), ','(=(Y, s(B)), minus(A, B, Z))).
div(X, Y, Z) :- ','(=(Y, 0), ','(!, fail)).
div(X, Y, Z) :- ','(=(X, 0), ','(!, =(Z, 0))).
div(X, Y, Z) :- ','(minus(X, Y, U), ','(div(U, Y, V), =(Z, s(V)))).
=(X, X).
Query: div(g,g,a)
(1) BuiltinConflictTransformerProof (EQUIVALENT transformation)
Renamed defined predicates conflicting with built-in predicates [PROLOG].
(2) Obligation:
Clauses:
minus(X, Y, Z) :- ','(user_defined_=(X, 0), ','(!, user_defined_=(Z, 0))).
minus(X, Y, Z) :- ','(user_defined_=(Y, 0), ','(!, user_defined_=(Z, X))).
minus(X, Y, Z) :- ','(user_defined_=(X, s(A)), ','(user_defined_=(Y, s(B)), minus(A, B, Z))).
div(X, Y, Z) :- ','(user_defined_=(Y, 0), ','(!, fail)).
div(X, Y, Z) :- ','(user_defined_=(X, 0), ','(!, user_defined_=(Z, 0))).
div(X, Y, Z) :- ','(minus(X, Y, U), ','(div(U, Y, V), user_defined_=(Z, s(V)))).
user_defined_=(X, X).
Query: div(g,g,a)
(3) PrologDeterminacyProcessorProof (EQUIVALENT transformation)
The root node satisfies the determinacy criterion.
(4) YES