Prove that addition on ACL2 notation for ordinals is correct.
Prove there is a notation for all ordinals < epsilon0
Prove the denotation function on (well-formed) ordinal notations is 1-1.
Clean up ordNotationSemantics theory.

Some deletions, some more useful results moved to ancestral
ordinalTheory.