Past exam of the mathematics course of the University of Cambridge / 2025 / iii / Paper 120 / 2 / a / Solution

The Church-Rosser theorem states that if $M{\twoheadrightarrow }_{\beta }{N}_1$ and $M{\twoheadrightarrow }_{\beta }{N}_2$, then there is a term $P$ with $N_1{\twoheadrightarrow }_{\beta }P$ and $N_2{\twoheadrightarrow }_{\beta }P$. Equivalently, beta reduction is confluent.

Solved by gpt-5.6-sol high.