This is the accompanying material for the paper:

• Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers

by Karol Pąk and Cezary Kaliszyk submitted to ITP 2024

The formalization was tested with latest Mizar Windows version 8.1.14 5.77.1462 and Linux version 8.1.14 5.76.1452

Links to selected definitions and theorems referenced in the article:

• Games(α),
• Day(R,α),
• Lemma 3,
• ProcO,
• ProcC,
• Almost No order,
• Comp(Ord,α),
• Theorem 8: 1.i, 1.ii, 1.iii c1., 1.iii c2., 2. step 1, 2. step 2, 2. step 3,
• No^{<=} α,
• Comparison condition,
• -x, x+y, x·y, x^{−1}, sqrt(x),
• exists x,y such that x ≈ y < 0 & sqrt (x) < sqrt(y),
• Equation 12: x + y = y + x , x · y = y · x , (x + y) + z = x + (y + z) , x + 0 = x , x · 1 = x , x + (−x) ≈ 0 , x · (y + z) ≈ x · y + x · z , (x · y) · z ≈ x · (y · z) , not x ≈ 0 → x · x^{−1} ≈ 1
• Theorem 10: existence , uniqueness
• s_Z , s_D , s_R
• Uniq ,
• ω^x: L_{ω^x} , R_{ω^x}
• x <= y → ω^x <= {ω^y}, x < y → ω^x <^\infty {ω^y}, ω^{x+y}≈{ω^x}·{ω^y}, {ω^x}^{−1}≈ω^{-x},
• Partial_Sums(r,y),
• SURREALC: 100, 102,

In order to recheck the formalization under Windows:

• Unpack Mizar into c:\mizar
• Run:

  install c:\mizar
  

• Put the formalization directories text and dict [.tgz] in c:\mizar
• Build a local library

  miz2prel text\surreali
  miz2prel text\surreals
  miz2prel text\surrealn
  miz2prel text\surrealc
  

  or add the content of formalization directories prel in c:\mizar\prel
• Run the verifier:

  mizf text\surreal0
  mizf text\surrealo
  mizf text\surrealr
  mizf text\surreali
  mizf text\surreals
  mizf text\surrealn
  mizf text\surrealc
  

• The above step already verified the proofs, but to additionally obtain the more readable abstracts run:

  miz2abs text\surreal0
  miz2abs text\surrealo
  miz2abs text\surrealr
  miz2abs text\surreali
  miz2abs text\surreals
  miz2abs text\surrealn
  miz2abs text\surrealc
  

  or add the content of formalization directories abstr

For other systems (e.g. Linux):

• Make sure Mizar is installed, in the path and the MIZFILES environment variable is set according to the message at the end of installation
• Add the supplementary dicts_extra

    mv dicts_extra/* dicts

• Run:

    for i in 0 o r i n s c; do mizf text/surreal${i}.miz; miz2prel text/surreal${i}.miz; done

   Name                    Last modified      Size  Description
   Parent Directory                             -   
   surreal.tgz             18-Mar-2024 21:57  239K  Source: Complete package for interactive use
   surreal0.html           18-Mar-2024 20:35  1.5M  HTML: Surreal Numbers -- Formal Introduction
   surrealc.html           18-Mar-2024 20:36  2.8M  HTML: Conway Normal Form
   surreali.html           18-Mar-2024 20:36  2.0M  HTML: Inverse of surreal numbres
   surrealn.html           18-Mar-2024 20:36  4.5M  HTML: Construction of the surreal numbers, order, quotient
   surrealo.html           18-Mar-2024 20:36  1.2M  HTML: Integration of Game Theoretic and Tree Theoretic Approaches to Conway Numbers
   surrealr.html           18-Mar-2024 20:36  3.9M  HTML: The Ring of Conway Numbers in Mizar
   surreals.html           18-Mar-2024 20:36  1.5M  HTML: The Square Root
  

  Apache/2.2.3 (Red Hat) Server at cl-informatik.uibk.ac.at Port 80