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))