Unification is reflexive: (== x x) = x for all x It is commutative: (== x y) = (== y x) for all x and y It is idempotent: (== x (== x y)) = (==

Unification is reflexive: (== x x) = x for all x It is commutative: (== x y) = (== y x) for all x and y It is idempotent: (== x (== x y)) = (== x y) for all x and y And it is associative: (== x (== y z)) = (== (== x y) z) It's not transitive, e.g. if we unify pairs (using made up syntax [a, b]) then (== [x, 1] [2, y]) = [2, 1] (== [2, y] [z, 3]) = [2, 3] (== [x, 1] [z, 3]) does not unify (since 1 does not unify with 3)