The command

In general, LP constructs the basis and induction steps using the set `G` of
generators for the sort `S` of `x` specified by the induction rule `IR`,
as follows.

Definition 1. A (`G`,`F`,`C`)-*ground term*, where `C` is a set of
constants of sort `S`, is a quantifier-free term of sort `S` in which all
operators are either in `C` or are inductive generators in `G`, no variable
has sort `S`, no variable occurs more than once, and no variable also occurs
in `F`.

Definition 2. A (`G`,`F`)-*ground term* is a
(`G`,`F`,`B`)-ground term, where `B` is the set of basis generators in
`G`.

Definition 3. The *depth* of a quantifier-free term is 0 if the term
consists of a variable; otherwise it is one more than the maximum depth of its
arguments.

Definition 4. A (`G`,`F`,{`c1`,...,`cm`})-ground term is
*canonical* if it contains exactly one occurrence of each of `c1`, ...,
`ck` for some `k <= m`.

The basis step involves proving all formulas of the form `F(x gets t)` where
`t` is an (`G`,`F`,`B`)-ground term of depth at most `n`.

The induction step introduces a set `C` = {`c1`,...,`cm`} of new
constants of sort `S`, where `m` is the maximum number of arguments of sort
`S` in a generator in `G` raised to the power `n`. The induction step
involves proving all formulas of the form `F(x gets t)`, where `t` is a
canonical (`G`,`F`,`C`)-ground term of depth `n+1`. The induction
hypotheses available in the induction step consist of all formulas of the form
`F(x gets t)`, where `t` is a (`G`,`F`,`C`)-ground term of depth at
most `n`.

When `n` is 1, the induction hypotheses consist of all formulas of the form
`F(x gets c)`, where `c` is in `C`; and the induction step involves
proving all formulas of the form `F(x gets t)`, where `t` is a canonical
(`G`,`F`,`C`)-ground term of depth 2.

Examples:

Gener- Level Basis Induction Induction ators Subgoals Hypotheses Subgoals 0, s 1 f(0) f(c) f(s(c)) 0, s 2 f(0) f(c) f(s(s(c))) f(s(0)) f(s(c)) 0, 1, + 1 f(0) f(c1) f(c1+c2) f(1) f(c2) 0, 1, + 2 f(0) f(c1), f(c2) f(c1+(c2+c3) f(1) f(c3), f(c4) f((c1+c2)+c3) f(0+0) f(c1+c1), f(c1+c2), ... f((c1+c2)+(c3+c4)) f(0+1) f(c2+c1), f(c2+c2), ... f(1+0) f(c3+c1), f(c3+c2), ... f(1+1) f(c4+c1), f(c4+c2), ... nil 1 f(nil) f(c) f(cons(x, c)) cons nil 2 f(nil) f(c) f(cons(x,cons(y,c)) cons f(cons(x,nil)) f(cons(x,c))