# example

WWhen2 a != 0, there are two solutions to ax^2 + bx + c = 0 and they are2

x = (-b +- sqrt(b^2-4ac))/(2a) .

# building blocks

{x in R| x * 2}

# 3.3.4 Theorem [Principles of Induction 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.


/section>