Major Section: PROGRAMMING
An ACL2 infinite ordinal is a list whose elements are exponent-coefficient
pairs (see o-p and see o-infp). The first exponent and first coefficient
of an ordinal can be obtained by using
o-first-coeff respectively. To obtain the rest of the ordinal (for
recursive analysis), use the
o-rst function. It returns the rest of the
ordinal after the first exponent and coefficient are removed.