LP, the Larch Prover -- Sample proofs: getting started

To invoke LP, type lp at the Unix command prompt. LP will respond with the following message:
Welcome to LP (the Larch Prover), Release 3.1 (94/12/30).
Copyright (C) 1994, S. J. Garland and J. V. Guttag
Type `help lp' (followed by a carriage return) for help.

LP is a command-driven system. The last line of LP's welcoming message, LP1:, is a prompt for the first command. LP prompts users to enter subsequent commands with LP2:, LP3:, ...

You can type input directly in response to LP's prompts, or you can create a file of LP commands (e.g., set1.lp) and then use LP's execute command to cause LP to execute the commands in that file as if you had typed them directly. Here's the start of a session in which commands are executed from the file set1.lp:

LP1: execute set1

LP1.1: % Some simple theorems about finite sets

The first command, execute set1, was typed by the user. The second was obtained from the file set1.lp. This command is a comment: LP ignores all input following a percent sign. The prompts LP1.1: and LP1.2: indicate that LP is taking input from the file being executed as a result of the command entered in response to the prompt LP1:.