LP, the Larch Prover -- Some sample proofs

We illustrate how to use LP by presenting some sample proofs along with explanatory comments. The proofs show how to derive some basic facts about finite sets from a simple axiomatization.

Getting started
Sample declarations for sorts, operators
Sample axioms for finite sets
Useful kinds of axioms
Sample conjectures
Two easy theorems
Three theorems about union
Alternative proofs of theorems about union
Three theorems about subset
An alternate induction rule
Two final theorems about subset
How to guide a proof