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.

Solution

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

 Solution

ID: past-exam-of-the-mathematics-course-of-the-university-of-cambridge/2025/iii/paper-120/2/a/solution