The <Weak normalization theorem for simply typed lambda calculus> states that every well-typed term of the <simply typed lambda calculus> admits at least one finite sequence of <beta reduction>[beta reductions] ending in a <beta-normal form>.

Solution

Past exam of the mathematics course of the University of Cambridge / 2023 / iii / Paper 120 / 2 / d / Solution

 Solution (source code)