<HTML><HEAD><TITLE>HOL/Lambda/ReadMe</TITLE></HEAD>
<BODY>
<H1>Lambda Calculus in de Bruijn's Notation</H1>
This theory defines lambda-calculus terms with de Bruijn indixes and proves
confluence of beta, eta and beta+eta.
<P>
Beta is proved confluent both in the traditional way (see Barendregt's book)
and also following Takahashi's elegant version using developments.
<P>
A report describing the whole theory with the exception of eta-reduction is
found here: <A HREF =
"ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/church-rosser.html"
>More Church-Rosser Proofs (in Isabelle)</A>.
</BODY>
</HTML>