Recursive definition of an ordinal notation. zero denotes the ordinal 0, and oadd e n a is intended to refer to ω^e * n + a. For this to be valid Cantor normal form, we must have the exponents decrease to the right, but we can't state this condition until we've defined repr, so it is a separate definition NF.

Notation for 0

Notation for 1

Notation for ω

The ordinal denoted by a notation

Print an ordinal notation

Print an ordinal notation

Convert a nat into an ordinal

Compare ordinal notations

NF_below o b says that o is a normal form ordinal notation satisfying repr o < ω ^ b.

A normal form ordinal notation has the form

ω ^ a₁ * n₁ + ω ^ a₂ * n₂ + ... ω ^ aₖ * nₖ

where a₁ > a₂ > ... > aₖ and all the aᵢ are also in normal form.

We will essentially only be interested in normal form ordinal notations, but to avoid complicating the algorithms we define everything over general ordinal notations and only prove correctness with normal form as an invariant.

top_below b o asserts that the largest exponent in o, if it exists, is less than b. This is an auxiliary definition for decidability of NF.

Addition of ordinal notations (correct only for normal input)

Subtraction of ordinal notations (correct only for normal input)

Multiplication of ordinal notations (correct only for normal input)

Calculate division and remainder of o mod ω. split' o = (a, n) means o = ω * a + n.

Calculate division and remainder of o mod ω. split o = (a, n) means o = a + n, where ω ∣ a.

scale x o is the ordinal notation for ω ^ x * o.

mul_nat o n is the ordinal notation for o * n.

power o₁ o₂ calculates the ordinal notation for the ordinal exponential o₁ ^ o₂.

The type of normal ordinal notations. (It would have been nicer to define this right in the inductive type, but NF o requires repr which requires onote, so all these things would have to be defined at once, which messes up the VM representation.)

Construct a nonote from an ordinal notation (and infer normality)

The ordinal represented by an ordinal notation. (This function is noncomputable because ordinal arithmetic is noncomputable. In computational applications nonote can be used exclusively without reference to ordinal, but this function allows for correctness results to be stated.)

Convert a natural number to an ordinal notation

Compare ordinal notations

Asserts that repr a < ω ^ repr b. Used in nonote.rec_on

The oadd pseudo-constructor for nonote

This is a recursor-like theorem for nonote suggesting an inductive definition, which can't actually be defined this way due to conflicting dependencies.

Addition of ordinal notations

Subtraction of ordinal notations

Multiplication of ordinal notations

Exponentiation of ordinal notations