 Normal-order normalization theorem

If an untyped lambda term has a beta-normal form, leftmost outermost beta reduction reaches a normal form. Thus an infinite normal-order computation certifies the absence of a beta-normal form. This is the normalization result needed to make a lambda simulation respect undefined outputs.