Invariants Identity &x == &y implies x == y Reflexivity x == x Symmetry x == y implies y == x Transitivity x == y and y == z implies x == z