 Definition A \(\beta\)-redex of a \(\lambda\)-term \(M\) is (an occurrence of) a subterm of \(M\) of the form \((\lambda x[P])Q\). (‘redex’ comes from ‘reducible expression.) A \(\beta\)-redex is simply a candidate for an application of \(\beta\)-reduction. Doing so, one contracts the \(\beta\)-redex. A term is said to be in \(\beta\)-normal form if it has no \(\beta\)-redexes.