Induction

Suppose P is a predicate on terms.

Induction on depth:

If, for each term s,

given P(r) for all r such that depth(r) < depth(s)

we can show P(s),

then P(s) holds for all s.

Induction on size:

If, for each term s,

given P(r) for all r such that size(r) < size(s)

we can show P(s),

then P(s) holds for all s.

Structural induction:

If, for each term s,

given P(r) for all immediate subterms r of s

we can show P(s),

then P(s) holds for all s.

page revision: 0, last edited: 15 Jan 2008 22:06