term_factorized/3

Availability:built-in

[det]term_factorized(+Term, -Skeleton, -Substitution)

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.