A mechanical proof of the Church-Rosser theorem

Abstract

The Church-Rosser theorem is a celebrated metamathematical result on the lambda calculus. We describe a formalization and proof of the Church-Rosser theorem that was carried out with the Boyer-Moore theorem prover. The proof presented in this paper is based on that of Tait and Martin-Löf. The mechanical proof illustrates the effective use of the Boyer-Moore theorem prover in proof checking difficult metamathematical proofs.