NUM_NORMALIZE_CONV : term -> thm

SYNOPSIS
Puts natural number expressions built using addition, multiplication and powers in canonical polynomial form.

DESCRIPTION
Given a term t of natural number type built up from other ``atomic'' components (not necessarily simple variables) and numeral constants by addition, multiplication and exponentiation by constant exponents, NUM_NORMALIZE_CONV t will return |- t = t' where t' is the result of putting the term into a normalized form, essentially a multiplied-out polynomial with a specific ordering of and within monomials.

FAILURE CONDITIONS
Should never fail.

EXAMPLE
  # NUM_NORMALIZE_CONV `1 + (1 + x + x EXP 2) * (x + (x * x) EXP 2)`;;
  val it : thm =
    |- 1 + (1 + x + x EXP 2) * (x + (x * x) EXP 2) =
       x EXP 6 + x EXP 5 + x EXP 4 + x EXP 3 + x EXP 2 + x + 1

COMMENTS
This can be used to prove simple algebraic equations, but NUM_RING or ARITH_RULE are generally more powerful and convenient for that. In particular, this function does not handle cutoff subtraction or other such operations.

SEE ALSO
ARITH_RULE, NUM_REDUCE_CONV, NUM_RING, REAL_POLY_CONV, SEMIRING_NORMALIZERS_CONV.