A Formalised First-Order Confluence Proof for
   the lambda-Calculus using One-Sorted Variable Names

         Rene Vestergaard and James Brotherston


We present the titular proof development that has been verified in
Isabelle/HOL. As a first, the proof is conducted exclusively by
the primitive proof principles of the standard syntax and of the
considered reduction relations: the naive way, so to speak.
Curiously, the Barendregt Variable Convention takes on a central
technical role in the proof. We also show (i) that our
presentation of the lambda-calculus coincides with Curry's and
Hindley's when terms are considered equal up to alpha-equivalence
and (ii) that the confluence properties of all considered systems
are equivalent.