(0) Obligation:
Clauses:
bin_tree(void) :- !.
bin_tree(T) :- ','(left(T, L), ','(right(T, R), ','(bin_tree(L), bin_tree(R)))).
left(void, void).
left(tree(X1, L, X2), L).
right(void, void).
right(tree(X3, X4, R), R).
Query: bin_tree(g)
(1) PrologDeterminacyProcessorProof (EQUIVALENT transformation)
The root node satisfies the determinacy criterion.
(2) YES