1. Install the LPTP system (see the file INSTALL.md).

2. The directory lptp/doc contains the documentation (user.ps).

3. In Chapter 1 you will find an example session.

   • Read Chapter 1 (Introduction). Try it out yourself.

4. Read Appendix B (Emacs mode) of the documentation.

5. Read Chapter 2 (Basic concepts of LPTP) of the documentation.

6. Read Section 3.1 (Syntax and Grammar) of Chapter 3 of the documentation.

7. Take the file lptp/lib/list/list.pr.

   • Delete all proofs.
   • Do the proofs yourself using LPTP.

8. Read the rest of the documentation.

Robert F. Staerk, staerk@inf.ethz.ch