(0) Obligation:
Clauses:
append(X, Y, Z) :- ','(=(X, []), ','(!, =(Y, Z))).
append(X, Y, Z) :- ','(=(X, .(H, Xs)), ','(!, ','(=(Z, .(H, Zs)), append(Xs, Y, Zs)))).
=(X, X).
Query: append(g,a,a)
(1) BuiltinConflictTransformerProof (EQUIVALENT transformation)
Renamed defined predicates conflicting with built-in predicates [PROLOG].
(2) Obligation:
Clauses:
append(X, Y, Z) :- ','(user_defined_=(X, []), ','(!, user_defined_=(Y, Z))).
append(X, Y, Z) :- ','(user_defined_=(X, .(H, Xs)), ','(!, ','(user_defined_=(Z, .(H, Zs)), append(Xs, Y, Zs)))).
user_defined_=(X, X).
Query: append(g,a,a)
(3) PrologDeterminacyProcessorProof (EQUIVALENT transformation)
The root node satisfies the determinacy criterion.
(4) YES