Global, inductive definitions.
A Horner polynomial is either a constant, or a product P × (i + Q), where i
is a variable.
Polynomials satisfy a uniqueness condition whenever they are valid. A
polynomial p satisfies valid n p whenever it is well-formed and each of
its variable indices is < n.
Linear polynomials are valid polynomials in which every variable appears at
most once.