 An equational theory as a set of pairs of terms amounts to a binary relation on the set of all terms. Rules R1–R3 correspond to respectively reflexivity, symmetry, and transitivity of this binary relation, \(i.e\). these three rules assert that an equational theory is an equivalence relation. Rule R4 expresses the further property that this binary relation is a congruence. Rule R5 further asserts that the relation is a substitutive congruence. It can be shown that a binary relation on the set of terms is an equational theory if and only if it is a substitutive congruence. These five rules therefore completely axiomatize equational logic in the sense that every consequence of a set \(A\) of equations can be produced from \(A\) via finitely many applications of these five rules.