An equational theory is a set of formulae, each of the form . Each formula is either an axiom or it is provable using the axioms for equality and the substitution rule of equals for equals.