LP, the Larch Prover -- Proofs by well-founded induction

To prove a formula F by well-founded induction over a variable x of sort S using a relation R that has been asserted or proved to be well founded, LP generates a single subgoal that involves proving the formula F(xc) using the additional hypothesis R(x, xc) => F(x), where xc is a new constant of sort S.

Example

assert well founded <
prove 0 + x = x by induction

  New constant:         xc
  Induction subgoal:    0 + xc = xc
  Induction hypothesis: x < xc => 0 + x = x