LP permits users to prove induction rules as well as assert them. To prove a structural induction rule such as

LP creates a single subgoal that involves proving the formulasort Set generated by {}, {__}, \U

whereisGenerated({}) isGenerated({e}) isGenerated(s1) /\ isGenerated(s2) => isGenerated(s1 /\ s2)

To prove a structural induction rule such as

LP also attempts to prove the subgoalssort Nat generated freely by 0:->Nat, f:Nat->Nat, g:Nat->Nat

in addition to the subgoalf(n) ~= 0 f(n) = f(n1) <=> n = n1 f(n) ~= g(n1) g(n) ~= 0 g(n) = g(n1) <=> n = n1

To prove a well-founded induction rule such as
`well founded <`, LP creates a single subgoal that involves proving the
formula
`isGenerated(x)` using the hypothesis

\A n1 (n1 < n => isGenerated(n1)) => isGenerated(n)