A Formalised First-Order Confluence Proof for
   the lambda-Calculus using One-Sorted Variable Names
       (Barendregt was right after all ... almost)

         Rene Vestergaard and James Brotherston


We present the titular proof development which has been
implemented in Isabelle/HOL. As a first, the proof is conducted
exclusively by the primitive induction principles of the standard
syntax and 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 coincides with Curry's and Hindley's when terms are
considered equal up-to alpha and (ii) that the confluence
properties of all considered calculi are equivalent.