Standardization theorem for beta reduction
= Standardization theorem for beta reduction
A finite <beta reduction> can be rearranged into standard order, contracting earlier residual redexes before later ones. In particular, a <lambda term> with a <head normal form> reaches one by head reduction, and a term with a <beta-normal form> reaches it by <normal-order beta reduction>. Head reduction contracts the outermost redex on the left application spine, including under initial <lambda abstractions>.