Norrish, MichaelHuffman, Brian2015-12-109783642396335http://hdl.handle.net/1885/66272We describe a comprehensive HOL mechanisation of the theory of ordinal numbers, focusing on the basic arithmetic operations. Mechanised results include the existence of fixpoints such as ε 0, the existence of normal forms, and the validation of algorithmKeywords: Arithmetic operations; Fixpoints; Mechanisation; Normal form; Ordinal number; Machinery; Number theory; Theorem proving201310.1007/978-3-642-39634-2_122016-02-24