Test example (remove this): Cantor normal form

Test example (originally using Cantor normal for ordinals up to ε₀, now will have dynamic base)

Format for inputting terms:

• 0

  for 0

• L^(a)

  for Λ^a

• a+b

  for a+b

Test example (remove this): Veblen normal form

Test example

Format for inputting terms:

• 0

  for 0

• f(a,b)

  for ϕ(a,b)

• a+b

  for a+b

First-order reflection

Ordinal notation from Arai, "A simplified ordinal analysis of first-order reflection"

Format for inputting terms:

Single stable ordinal

Π₁-collection

Second-order arithmetic