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.