@MISC{CGAMES_1.MIZ,
  AUTHOR = {Nittka, Robin},
  TITLE = {Conway's Games and Some of Their Basic Properties},
  SECTION1 = {Construction of Days},
  SECTION2 = {Games},
  SECTION3 = {Schemes of Induction},
  SECTION4 = {Tree of a Game},
  SECTION5 = {Scheme about Definability of Functions by Recursion},
  SECTION6 = {The Negative and Signs},
  DAY = {13},
  MONTH = {October},
  YEAR = {2010},
  ADDRESS1 = {Institute of Applied Analysis\\University of Ulm\\89069 Ulm\\Germany},
  SUMMARY = {We formulate a few basic concepts of J.\ H.\ Conway's theory of
  games based on his book~\cite{Conway:2001}. This is a first step towards formalizing
  Conway's theory of numbers into Mizar, which is an approach to proving the existence of a
  FIELD (i.e., a proper class that satisfies the axioms of a real-closed field)
  that includes the reals and ordinals, thus providing a uniform, independent and simple
  approach to these two constructions that does not go via the rational numbers and
  hence does for example not need the notion of a quotient field.\par
  In this first article on Conway's games, we provide a definition of games, their
  birthdays (or ranks), their trees (a notion which is not in Conway's book, but is useful as
  a tool), their negates and their signs, together with some elementary properties of these
  notions. If one is interested only in Conway's numbers, it would have been easier to define
  them directly, but going via the notion of a game is a more general approach in the sense that
  a number is a special instance of a game and that there is a rich theory of games that are
  not numbers.\par
  The main obstacle in formulating these topics in Mizar is that all definitions are highly
  recursive, which is not entirely simple to translate into the Mizar language. For example,
  according to Conway's definition, a game is an object consisting of left and right options
  which are themselves games, and this is by definition the only way to construct a game.
  This cannot directly be translated into Mizar, but a theorem is included in the article
  which proves that our definition is equivalent to Conway's.}}

@book{Conway:2001,
    AUTHOR = {Conway, J. H.},
     TITLE = {On numbers and games},
   EDITION = {Second},
 PUBLISHER = {A K Peters Ltd.},
   ADDRESS = {Natick, MA},
      YEAR = {2001},
     PAGES = {xii+242},
      ISBN = {1-56881-127-6}
}
