Page "Structural induction" Paragraph 1

In general, the idea is that one wishes to prove some proposition P ( x ), where x is any instance of some sort of recursively defined structure such as lists or trees.

A well-founded partial order is defined on the structures (" sublist " for lists and " subtree " for trees ).

The structural induction proof is a proof that the proposition holds for all the minimal structures, and that if it holds for the immediate substructures of a certain structure S, then it must hold for S also.

( Formally speaking, this then satisfies the premises of an axiom of well-founded induction, which asserts that these two conditions are sufficient for the proposition to hold for all x.