 Recall that a term is said to be in \(\beta\)-normal form if it has no \(\beta\)-redexes, that is, subterms of the shape \((\lambda x[M]\))N. A term has a \(\beta\)-normal form if it can be reduced to a term in \(\beta\)-normal form. It should be intuitively clear that if a term has a \(\beta\)-normal form, then we can find one by exhaustively contracting all all \(\beta\)-redexes of the term, then exhaustively contracting all \(\beta\)-redexes of all resulting terms, and so forth. To say that a term has a \(\beta\)-normal form amounts to saying that this blind search for one will eventually terminate.