# LP, the Larch Prover -- Proofs by structural induction

A proof of a formula F by structural induction on a variable x of sort S is based on an induction rule that specifies a set G of generators for S, that is, a set of operators with range S. LP generates subgoals for the basis and induction steps in a proof by structural induction, as follows.
• The basis subgoals involve proving the formulas that result from substituting the basis generators in G for x in F. Basis generators are those with no arguments of sort S; fresh variables are used for variables of other sorts, as in {e}.

• LP introduces additional hypotheses for the induction subgoals by substituting one or more new constants for x in F. Each induction subgoal involves proving a formula that results from substituting a nonbasis generator of G (applied to these constants) for x in F (e.g., s(xc) or xc \U xc1).

## Examples

```assert sort Nat generated by 0, s
prove 0 + x = x by induction
Basis subgoal:        0 + 0 = 0
New constant:         xc
Induction hypothesis: 0 + xc = xc
Induction subgoal:    0 + s(xc) = s(xc)
```
```assert sort Set generated by {}, {__}, \U
prove x \subseteq x by induction
Basis subgoals:       {} \subseteq {},    {e} \subseteq {e}
New constants:        xc,                 xc1
Induction hypotheses: xc \subseteq xc,    xc1 \subseteq xc1
Induction subgoal:    (xc \U xc1) \subseteq (xc \U xc1)
```