Normal-order normalization theorem
= 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.