"That is, a variable only unifies to a term if this term does not contain the variable itself."

Another example:

Arbitrarily choosing LHS and RHS of "LHS = RHS":

Remembering that terms are trees and variables can only name leaves of such a tree:

- You have the LHS term/tree with A naming some leaf node.
- You have the RHS term/tree with the same A naming some leaf node.
- A is a freshvar (i.e. the leaf nodes are "holes")

LHS:

vars: A ↓ term: a─b─☐ a(b( A ))

RHS:

vars: A ↓ term: a─b─x─y─z─☐ a(b( x(y(z(A))) ))

A on the LHS will be unified with x─y─z─☐ which contains a place named by A.

This yields an infinite (cyclic) subterm.

vars: A A A The term named by A now has a beginning but no end ↓ ↓ ↓ term: a─b─x─y─z─x─y─z─x─y─z-...

?- a(b(A)) = a(b(x(y(z(A))))). A = x(y(z(A))). ?- unify_with_occurs_check(a(b(A)) , a(b(x(y(z(A)))))). false.

See also: