H. Paul Williams: A formalisation of the arithmetic of the ordinals less than W<sup>ω</sup>. Notre Dame J. Formal Log. 10(1): 77-89 (1969)