`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
```

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.