True when Skeleton is Term with every subterm that
is used more than once replaced by a variable, and Substitution
is a list of Var = Value giving those subterms. After
unifying all substitutions in Substitution, Term ==
Skeleton.
Term may be cyclic. The cycles come back through the
substitutions, so Skeleton itself is acyclic:
?- X = a(X), term_factorized(b(X,X), Y, S).
Y = b(_A, _A),
S = [_A=a(_A)].
Subterms are the same when they are ==/2.
For a
rational tree that means when they denote the same infinite
tree, so Term is factorized as far as it can be:
?- X = f(X), Y = f(f(Y)), term_factorized(p(X,Y), S, B).
S = p(_A, _A),
B = [_A=f(_A)].
The substitutions come in a canonical order, which makes
Skeleton-Substitution a key for =@=/2.
