 The first three rules of inference in  Section 1.3.1  are called rules of λ-conversion. If \(\bD\) and \(\bE\) are wffs, we write \(\bD \conv \bE\) to indicate that \(\bD\) can be converted to \(\bE\) by applications of these rules. This is an equivalence relation between wffs. A wff \(\bD\) is in β-normal form iff it has no well-formed parts of the form \([[\lambda \bx_{\alpha}\bB_{\beta}]\bA_{\alpha}]\). Every wff is convertible to one in β-normal form. Indeed, every sequence of contractions (applications of rule 2, combined as necessary with alphabetic changes of bound variables) of a wff is finite; obviously, if such a sequence cannot be extended, it terminates with a wff in β-normal form. (This is called the strong normalization theorem.) By the Church-Rosser Theorem, this wff in β-normal form is unique modulo alphabetic changes of bound variables. For each wff \(\bA\) we denote by \({\downarrow}\bA\) the first wff (in some enumeration) in β-normal form such that \(\bA \conv {\downarrow} \bA\). Then \(\bD \conv \bE\) if and only if \({\downarrow} \bD = {\downarrow} \bE\).