On Ordinal Notations

Authors:

Description:

This contribution contains data structures for ordinals less than Gamma0 under Cantor and Veblen normal forms. Well-foundedness is established thanks to RPO with status for generic terms. This contribution also includes termination proofs of Hydra battles and Goodstein sequences as well as a computation of the length of the Goodstein sequence starting from 4 in base 2.

This work is supported by INRIA-Futurs (Logical project-team), CNRS and the French ANR via the A3PAT project (http://www3.iie.cnam.fr/~urbain/a3pat/).

Keywords:

Source files:

• Cantor.prelude.list_set
• Cantor.epsilon0.Goodstein
• Cantor.misc.G4
• Cantor.prelude.Tools
• Cantor.prelude.more_list
• Cantor.prelude.More_nat
• Cantor.prelude.PartialFix
• Cantor.prelude.not_decreasing
• Cantor.gamma0.Gamma0_prelude
• Cantor.epsilon0.Hydra
• Cantor.prelude.dickson
• Cantor.prelude.list_permut
• Cantor.epsilon0.MSE0
• Cantor.rpo.term
• Cantor.prelude.AccP
• Cantor.gamma0.Gamma0_length
• Cantor.epsilon0.EPSILON0
• Cantor.gamma0.Gamma0
• Cantor.prelude.closure
• Cantor.rpo.rpo
• Cantor.prelude.decidable_set