Induction using term orders (Q1915132)

There are two kinds of proof methods used in automating inductive theorem proving: explicit induction, which uses induction schemes, and implicit induction (sometimes called `inductionless induction'), which is based on procedures like Knuth-Bendix completion. The former offers the flexibility of induction over arbitrary well-founded orders and the latter better supports mutual induction (where a theorem and a lemma can appeal to each other in their proofs). The authors propose a proof method that combines the benefits of both by showing how explicit induction can use well-founded orders on terms that represent propositions.