Surreal 4

mmset.raw.html

@@ -5423,7 +5423,7 @@
 [QA251.5 .G642 1999].
 </LI>
 <LI>
-<A NAME="Goshnor"></A> [Goshnor] Goshnor, Harry, <I>An Introduction to
+<A NAME="Gonshor"></A> [Gonshor] Gonshor, Harry, <I>An Introduction to
 the Theory of Surreal Numbers,</I> London Mathematical Society (1986)
 [QA241.G63 1986].
 </LI>

set.mm

@@ -524491,6 +524491,16 @@ Real and complex numbers (cont.)
       AEUANPPABQACDETRS $.
   $}
 
+  $( The union of two ordinals is in a third iff both of the first two are.
+     (Contributed by Scott Fenton, 10-Sep-2024.) $)
+  onunel $p |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A u. B ) e. C <->
+  ( A e. C /\ B e. C ) ) ) $=
+    ( con0 wcel w3a wss cun wa wb wceq biimpi eleq1d adantl ontr2 expdimp bitrd
+    wi word eloni ssequn1 3adant2 pm4.71rd ssequn2 3adant1 wo ordtri2or2 syl2an
+    pm4.71d 3adant3 mpjaodan ) ADEZBDEZCDEZFZABGZABHZCEZACEZBCEZIZJBAGZUOUPIZUR
+    UTVAUPURUTJUOUPUQBCUPUQBKABUALMNVCUTUSUOUPUTUSULUNUPUTIUSRUMABCOUBPUCQUOVBI
+    ZURUSVAVBURUSJUOVBUQACVBUQAKBAUDLMNVDUSUTUOVBUSUTUMUNVBUSIUTRULBACOUEPUIQUL
+    UMUPVBUFZUNULASBSVEUMATBTABUGUHUJUK $.
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -529385,9 +529395,9 @@ C Fn ( ( S i^i dom F ) u. { z } ) ) $=
        class of numbers developed by John H. Conway and introduced by Donald
        Knuth in 1975.  They form a proper class into which all ordered fields
        can be embedded.  The approach we take to defining them was first
-       introduced by Hary Goshnor, and is based on the conception of a "sign
+       introduced by Hary Gonshor, and is based on the conception of a "sign
        expansion" of a surreal number.  We define the surreals as
-       ordinal-indexed sequences of ` 1o ` and ` 2o ` , analagous to Goshnor's
+       ordinal-indexed sequences of ` 1o ` and ` 2o ` , analagous to Gonshor's
        ` ( - ) ` and ` ( + ) ` .
 
        After introducing this definition, we will abstract away from it using
@@ -532548,7 +532558,7 @@ C Fn ( ( S i^i dom F ) u. { z } ) ) $=
     $( Define the cut operator on surreal numbers.  This operator, which Conway
        takes as the primitive operator over surreals, picks the surreal lying
        between two sets of surreals of minimal birthday.  Definition from
-       [Goshnor] p. 7.  (Contributed by Scott Fenton, 7-Dec-2021.) $)
+       [Gonshor] p. 7.  (Contributed by Scott Fenton, 7-Dec-2021.) $)
     df-scut $a |- |s = ( a e. ~P No , b e. ( <<s " { a } ) |->
       ( iota_ x e. { y e. No | ( a <<s { y } /\ { y } <<s b ) }
         ( bday ` x ) =
@@ -532616,6 +532626,21 @@ C Fn ( ( S i^i dom F ) u. { z } ) ) $=
       DEFCGHDGHIZCJKZDJKZALBLMFBDNACNZOIUBABCDPSTUAUBQR $.
   $}
 
+  ${
+    $d A x y $.  $d B x y $.  $d ph x y $.
+    ssltd.1 $e |- ( ph -> A e. V ) $.
+    ssltd.2 $e |- ( ph -> B e. W ) $.
+    ssltd.3 $e |- ( ph -> A C_ No ) $.
+    ssltd.4 $e |- ( ph -> B C_ No ) $.
+    ssltd.5 $e |- ( ( ph /\ x e. A /\ y e. B ) -> x <s y ) $.
+    $( Deduce surreal set less than.  (Contributed by Scott Fenton,
+       24-Sep-2024.) $)
+    ssltd $p |- ( ph -> A <<s B ) $=
+      ( cvv wcel csur wss cv wbr wral elexd cslt w3a ralrimivva 3jca syl21anbrc
+      csslt 3expb brsslt ) ADMNEMNDOPZEOPZBQZCQZUARZCESBDSZUBDEUFRADFHTAEGITAUI
+      UJUNJKAUMBCDEAUKDNULENUMLUGUCUDBCDEUHUE $.
+  $}
+
   ${
     $d A x y $.  $d B x y $.  $d X x y $.  $d Y x y $.
     $( Two elements of separated sets obey less than.  (Contributed by Scott
@@ -532641,28 +532666,27 @@ C Fn ( ( S i^i dom F ) u. { z } ) ) $=
        Scott Fenton, 9-Dec-2021.) $)
     sssslt2 $p |- ( ( A <<s B /\ C C_ B ) -> A <<s C ) $=
       ( vx vy csslt wbr wss wa cvv wcel csur cv cslt w3a ssltex1 adantr ssltex2
-      wral simpr ssexd ssltss1 ssltss2 sstrd ssltsep wi ssralv syl ralimdv 3jca
-      mpd brsslt syl21anbrc ) ABFGZCBHZIZAJKZCJKALHZCLHZDMEMNGZECSZDASZOACFGUNU
-      QUOABPQUPCBJUNBJKUOABRQUNUOTZUAUPURUSVBUNURUOABUBQUPCBLVCUNBLHUOABUCQUDUP
-      UTEBSZDASZVBUNVEUODEABUEQUPVDVADAUPUOVDVAUFVCUTECBUGUHUIUKUJDEACULUM $.
+      wral simpr ssexd ssltss1 ssltss2 sstrd ssltsep ssralv ralimdv 3jca brsslt
+      mpan9 syl21anbrc ) ABFGZCBHZIZAJKZCJKALHZCLHZDMEMNGZECSZDASZOACFGULUOUMAB
+      PQUNCBJULBJKUMABRQULUMTZUAUNUPUQUTULUPUMABUBQUNCBLVAULBLHUMABUCQUDULUREBS
+      ZDASUMUTDEABUEUMVBUSDAURECBUFUGUJUHDEACUIUK $.
   $}
 
   ${
     $d A x y $.
     $( The empty set is less than any set of surreals.  (Contributed by Scott
        Fenton, 8-Dec-2021.) $)
     nulsslt $p |- ( A e. ~P No -> (/) <<s A ) $=
-      ( vx vy csur cpw wcel c0 cvv wa wss cv cslt wbr wral w3a csslt elex jctil
-      0ex a1i 0ss elpwi ral0 3jca brsslt sylanbrc ) ADEZFZGHFZAHFZIGDJZADJZBKCK
-      LMCANZBGNZOGAPMUHUJUIAUGQSRUHUKULUNUKUHDUATADUBUNUHUMBUCTUDBCGAUEUF $.
+      ( vx vy csur cpw wcel c0 cvv 0ex a1i id wss 0ss elpwi cv cslt wbr pm2.21i
+      noel 3ad2ant2 ssltd ) ADEZFZBCGAHUBGHFUCIJUCKGDLUCDMJADNBOZGFZUCUDCOZPQZU
+      FAFUEUGUDSRTUA $.
 
     $( The empty set is greater than any set of surreals.  (Contributed by
        Scott Fenton, 8-Dec-2021.) $)
     nulssgt $p |- ( A e. ~P No -> A <<s (/) ) $=
-      ( vx vy csur cpw wcel cvv c0 wa wss cv cslt wbr wral w3a csslt elex jctir
-      0ex a1i elpwi 0ss ral0 rgenw 3jca brsslt sylanbrc ) ADEZFZAGFZHGFZIADJZHD
-      JZBKCKLMZCHNZBANZOAHPMUIUJUKAUHQSRUIULUMUPADUAUMUIDUBTUPUIUOBAUNCUCUDTUEB
-      CAHUFUG $.
+      ( vx vy csur cpw wcel c0 cvv id 0ex a1i elpwi wss 0ss cv cslt wbr pm2.21i
+      noel 3ad2ant3 ssltd ) ADEZFZBCAGUBHUCIGHFUCJKADLGDMUCDNKCOZGFZUCBOZUDPQZU
+      FAFUEUGUDSRTUA $.
   $}
 
   ${
@@ -532834,23 +532858,22 @@ property of surreals and will be used (via surreal cuts) to prove many
     $( Union law for surreal set less than.  (Contributed by Scott Fenton,
        9-Dec-2021.) $)
     ssltun1 $p |- ( ( A <<s C /\ B <<s C ) -> ( A u. B ) <<s C ) $=
-      ( vx vy csslt wbr wa cvv wcel csur wss wral ssltex1 adantr ssltss1 adantl
-      cv ssltsep sylanbrc cun w3a unexg syl2an ssltex2 jca unssd ssltss2 ralunb
-      cslt 3jca brsslt ) ACFGZBCFGZHZABUAZIJZCIJZHUPKLZCKLZDRERUJGECMZDUPMZUBUP
-      CFGUOUQURUMAIJBIJUQUNACNBCNABIIUCUDUMURUNACUEOUFUOUSUTVBUOABKUMAKLUNACPOU
-      NBKLUMBCPQUGUNUTUMBCUHQUOVADAMZVADBMZVBUMVCUNDEACSOUNVDUMDEBCSQVADABUITUK
-      DEUPCULT $.
+      ( vx vy csslt wbr cvv wcel ssltex1 adantr adantl csur ssltss1 cv ssltsepc
+      wss wi 3exp com12 wa cun unexd ssltex2 unssd ssltss2 cslt elun jaoi sylbi
+      wo 3imp21 ssltd ) ACFGZBCFGZUAZDEABUBZCHHUPABHHUNAHIUOACJKUOBHIUNBCJLUCUN
+      CHIUOACUDKUPABMUNAMQUOACNKUOBMQUNBCNLUEUNCMQUOACUFKDOZUQIZUPEOZCIZURUTUGG
+      ZUSURAIZURBIZUKUPVAVBRZRZURABUHVCVFVDUPVCVEUNVCVERUOUNVCVAVBACURUTPSKTUPV
+      DVEUOVDVERUNUOVDVAVBBCURUTPSLTUIUJULUM $.
 
     $( Union law for surreal set less than.  (Contributed by Scott Fenton,
        9-Dec-2021.) $)
     ssltun2 $p |- ( ( A <<s B /\ A <<s C ) -> A <<s ( B u. C ) ) $=
-      ( vx vy csslt wbr wa cvv wcel csur wss wral adantr ssltex2 ssltss2 adantl
-      cv ssltsep sylanbrc cun w3a ssltex1 unexg syl2an jca ssltss1 unssd ralunb
-      cslt ralbii r19.26 bitri 3jca brsslt ) ABFGZACFGZHZAIJZBCUAZIJZHAKLZUTKLZ
-      DRERUJGZEUTMZDAMZUBAUTFGURUSVAUPUSUQABUCNUPBIJCIJVAUQABOACOBCIIUDUEUFURVB
-      VCVFUPVBUQABUGNURBCKUPBKLUQABPNUQCKLUPACPQUHURVDEBMZDAMZVDECMZDAMZVFUPVHU
-      QDEABSNUQVJUPDEACSQVFVGVIHZDAMVHVJHVEVKDAVDEBCUIUKVGVIDAULUMTUNDEAUTUOT
-      $.
+      ( vx vy csslt wbr cvv wcel adantr ssltex2 adantl csur ssltss2 cv ssltsepc
+      wss wi 3exp com3r wa cun ssltex1 unexd ssltss1 unssd cslt elun jaoi sylbi
+      wo 3imp231 ssltd ) ABFGZACFGZUAZDEABCUBZHHUNAHIUOABUCJUPBCHHUNBHIUOABKJUO
+      CHIUNACKLUDUNAMQUOABUEJUPBCMUNBMQUOABNJUOCMQUNACNLUFEOZUQIZUPDOZAIZUTURUG
+      GZUSURBIZURCIZUKUPVAVBRRZURBCUHVCVEVDUPVAVCVBUNVAVCVBRRUOUNVAVCVBABUTURPS
+      JTUPVAVDVBUOVAVDVBRRUNUOVAVDVBACUTURPSLTUIUJULUM $.
   $}
 
   ${
@@ -533033,7 +533056,7 @@ property of surreals and will be used (via surreal cuts) to prove many
     $d X a d $.  $d Y a d $.
     $( A comparison law for surreals considered as cuts of sets of surreals.
        Definition from [Conway] p. 4.  Theorem 4 of [Alling] p. 186.  Theorem
-       2.5 of [Goshnor] p. 9.  (Contributed by Scott Fenton, 11-Dec-2021.) $)
+       2.5 of [Gonshor] p. 9.  (Contributed by Scott Fenton, 11-Dec-2021.) $)
     slerec $p |- ( ( ( A <<s B /\ C <<s D ) /\
      ( X = ( A |s B ) /\ Y = ( C |s D ) ) ) ->
      ( X <_s Y <-> ( A. d e. D X <s d /\ A. a e. A a <s Y ) ) ) $=
@@ -533098,6 +533121,55 @@ property of surreals and will be used (via surreal cuts) to prove many
       JVKVLUMVMVN $.
   $}
 
+  ${
+    $d A x $.  $d B x $.
+    $( If ` A ` preceeds ` B ` , then ` A ` and ` B ` are disjoint.
+       (Contributed by Scott Fenton, 18-Sep-2024.) $)
+    ssltdisj $p |- ( A <<s B -> ( A i^i B ) = (/) ) $=
+      ( vx csslt wbr cv wcel wn wral c0 wceq wa cslt csur ssltss1 sselda sltirr
+      cin syl ssltsepc 3expa mtand ralrimiva disj sylibr ) ABDEZCFZBGZHZCAIABRJ
+      KUFUICAUFUGAGZLZUHUGUGMEZUKUGNGULHUFANUGABOPUGQSUFUJUHULABUGUGTUAUBUCCABU
+      DUE $.
+  $}
+
+  ${
+    $d A a b c x $.  $d B a b c x y $.  $d C a b c $.
+    $( If every element of ` A ` is less than some element of ` B ` and ` B `
+       precedes ` C ` , then ` A ` precedes ` C ` .  Note - we will often use
+       the term "cofinal" to denote that every element of ` A ` is less than
+       some element of ` B ` .  Similarly, we will use the term "coinitial" to
+       denote that every element of ` A ` is greater than some element of
+       ` B ` .  (Contributed by Scott Fenton, 24-Sep-2024.) $)
+    cofsslt $p |- ( ( A e. ~P No /\
+     A. x e. A E. y e. B x <s y /\ B <<s C ) -> A <<s C ) $=
+      ( va vc vb csur wcel cv cslt wbr wrex w3a 3ad2ant3 3ad2ant1 adantr sseldd
+      wss cpw wral csslt cvv simp1 ssltex2 elpwi ssltss2 weq breq1 simp12 simp2
+      rexbidv rspcdva breq2 cbvrexvw sylibr simpl2 ssltss1 simprl simpl3 simprr
+      wa simpl13 ssltsepc syl3anc slttrd rexlimddv ssltd ) CIUAZJZAKZBKZLMZBDNZ
+      ACUBZDEUCMZOZFGCEVJUDVKVPVQUEVQVKEUDJVPDEUFPVKVPCITZVQCIUGQZVQVKEITZVPDEU
+      HPZVRFKZCJZGKZEJZOZWCHKZLMZWCWELMHDWGWCVMLMZBDNZWIHDNWGVOWKACWCAFUIVNWJBD
+      VLWCVMLUJUMVKVPVQWDWFUKVRWDWFULUNWIWJHBDWHVMWCLUOUPUQWGWHDJZWIVCZVCZWCWHW
+      EWNCIWCWGVSWMVRWDVSWFVTQRVRWDWFWMURSWNDIWHWGDITZWMVRWDWOWFVQVKWOVPDEUSPQR
+      WGWLWIUTZSWNEIWEWGWAWMVRWDWAWFWBQRVRWDWFWMVAZSWGWLWIVBWNVQWLWFWHWELMVKVPV
+      QWDWFWMVDWPWQDEWHWEVEVFVGVHVI $.
+  $}
+
+  ${
+    $d A a b c $.  $d B a b c x $.  $d C a b c x y $.
+    $( If ` B ` is coinitial with ` C ` and ` A ` precedes ` C ` , then ` A `
+       precedes ` B ` .  (Contributed by Scott Fenton, 24-Sep-2024.) $)
+    coinitsslt $p |- ( ( B e. ~P No /\
+     A. x e. B E. y e. C y <s x /\ A <<s C ) -> A <<s B ) $=
+      ( va vb vc csur wcel cv cslt wbr wrex w3a cvv 3ad2ant3 wss elpwid sseldd
+      cpw wral csslt ssltex1 simp1 ssltss1 weq breq2 rexbidv simp12 simp3 breq1
+      rspcdva cbvrexvw sylib simpl13 syl simpl2 ssltss2 simprl simpl11 ssltsepc
+      wa simpl3 syl3anc simprr slttrd rexlimddv ssltd ) DIUAZJZBKZAKZLMZBENZADU
+      BZCEUCMZOZFGCDPVJVQVKCPJVPCEUDQVKVPVQUEZVQVKCIRZVPCEUFZQVRDIVSSVRFKZCJZGK
+      ZDJZOZHKZWDLMZWBWDLMHEWFVLWDLMZBENZWHHENWFVOWJADWDAGUGVNWIBEVMWDVLLUHUIVK
+      VPVQWCWEUJVRWCWEUKUMWIWHBHEVLWGWDLULUNUOWFWGEJZWHVCZVCZWBWGWDWMCIWBWMVQVT
+      VKVPVQWCWEWLUPZWAUQVRWCWEWLURZTWMEIWGWMVQEIRWNCEUSUQWFWKWHUTZTWMDIWDWMDIV
+      KVPVQWCWEWLVASVRWCWEWLVDTWMVQWCWKWBWGLMWNWOWPCEWBWGVBVEWFWKWHVFVGVHVI $.
+  $}
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -533827,6 +533899,74 @@ property of surreals and will be used (via surreal cuts) to prove many
       UTEPVBUNUTEUEURUSEUFUIUGUJUHBACDEUKUL $.
   $}
 
+  ${
+    $d X x y $.  $d Y x y $.
+    $( If ` X ` is less than ` Y ` , then either ` ( _L `` Y ) ` or
+       ` ( _R `` X ) ` is non-empty.  (Contributed by Scott Fenton,
+       10-Dec-2024.) $)
+    sltn0 $p |- ( ( X e. No /\ Y e. No /\ X <s Y ) ->
+     ( ( _L ` Y ) =/= (/) \/ ( _R ` X ) =/= (/) ) ) $=
+      ( vy vx csur wcel wbr cv csle cleft cfv wrex cright wo c0 wne csslt cscut
+      co wceq cslt w3a wa wb lltropt adantr adantl lrcut eqcomd sltrec syl22anc
+      biimp3a rexn0 orim12i syl ) AEFZBEFZABUAGZUBACHIGZCBJKZLZDHBIGZDAMKZLZNZU
+      TOPZVCOPZNUPUQURVEUPUQUCAJKZVCQGZUTBMKZQGZAVHVCRSZTZBUTVJRSZTZURVEUDUPVIU
+      QAUEUFUQVKUPBUEUGUPVMUQUPVLAAUHUIUFUQVOUPUQVNBBUHUIUGVHVCUTVJABDCUJUKULVA
+      VFVDVGUSCUTUMVBDVCUMUNUO $.
+  $}
+
+  $( If two surreals share a birthday, then the union of their left and right
+     sets are equal.  (Contributed by Scott Fenton, 17-Sep-2024.) $)
+  lruneq $p |- ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) ->
+     ( ( _L ` X ) u. ( _R ` X ) ) = ( ( _L ` Y ) u. ( _R ` Y ) ) ) $=
+    ( csur wcel cbday cfv wceq w3a cold cleft cun fveq2 3ad2ant3 lrold 3ad2ant1
+    cright 3ad2ant2 3eqtr4d ) ACDZBCDZAEFZBEFZGZHUAIFZUBIFZAJFAPFKZBJFBPFKZUCSU
+    DUEGTUAUBILMSTUFUDGUCANOTSUGUEGUCBNQR $.
+
+  ${
+    $d X x $.  $d Y x $.
+    $( If two surreals share a birthday, then ` X <s Y ` iff the left set of
+       ` X ` is a proper subset of the left set of ` Y ` .  (Contributed by
+       Scott Fenton, 17-Sep-2024.) $)
+    sltlpss $p |- ( ( X e. No /\ Y e. No /\ ( bday ` X ) = ( bday ` Y ) ) ->
+     ( X <s Y <-> ( _L ` X ) C. ( _L ` Y ) ) ) $=
+      ( vx csur wcel cfv wceq cslt wbr wss cold con0 eleq2d syl bitrdi cun cdif
+      wa wn c0 cbday w3a cleft wpss cv wf oldf bdayelon ffvelrn mp2an fvex elpw
+      cpw mpbi sseli 3ad2ant2 simp1l1 simp1l2 simp3 simp1r 3exp imdistand fveq2
+      slttrd 3ad2ant3 adantr anbi1d sylibd simpl1 leftval simpl2 3imtr4d sltirr
+      crab rabid ssrdv breq1 notbid syl5ibrcom con2d imp cright cscut co lruneq
+      simpr difeq12d difundir difid uneq1i 0un 3eqtri cin incom simpll1 lltropt
+      csslt ssltdisj 3syl eqtr3id disjdif2 syl5eq simpll2 3eqtr3d oveq12d lrcut
+      mtand dfpss2 sylanbrc ex dfpss3 ssdif0 necon3bbii n0 bitri eldif wo ianor
+      wex wne wb bi2anan9r 3adant3 simprl simpl3 fveq2d eleqtrrd pm2.24d sseldi
+      csle slenlt syl2anc biimpar simplrr slelttrd jaod expimpd sylbid exlimdv
+      syl5bi adantld impbid ) ADEZBDEZAUAFZBUAFZGZUBZABHIZAUCFZBUCFZUDZUUHUUIUU
+      LUUHUUIRZUUJUUKJZUUJUUKGZSUULUUMCUUJUUKUUMCUEZUUEKFZEZUUPAHIZRZUUPUUFKFZE
+      ZUUPBHIZRZUUPUUJEZUUPUUKEZUUMUUTUURUVCRUVDUUMUURUUSUVCUUMUURUUSUVCUUMUURU
+      USUBUUPABUURUUMUUPDEZUUSUUQDUUPUUQDUMZEZUUQDJLUVHKUFZUUELEUVIUGAUHLUVHUUE
+      KUIUJUUQDUUEKUKULUNUOUPUUCUUDUUGUUIUURUUSUQUUCUUDUUGUUIUURUUSURUUMUURUUSU
+      SUUHUUIUURUUSUTVDVAVBUUMUURUVBUVCUUMUUQUVAUUPUUHUUQUVAGZUUIUUGUUCUVKUUDUU
+      EUUFKVCVEVFMVGVHUUMUVEUUPUUSCUUQVNZEZUUTUUMUUJUVLUUPUUMUUCUUJUVLGUUCUUDUU
+      GUUIVICAVJZNMUUSCUUQVOZOUUMUVFUUPUVCCUVAVNZEZUVDUUMUUKUVPUUPUUMUUDUUKUVPG
+      UUCUUDUUGUUIVKCBVJZNMUVCCUVAVOZOVLVPUUMUUOABGZUUHUUIUVTSUUHUVTUUIUUHUUISU
+      VTBBHIZSZUUDUUCUWBUUGBVMUPUVTUUIUWAABBHVQVRVSVTWAUUMUUORZUUJAWBFZWCWDZUUK
+      BWBFZWCWDZABUWCUUJUUKUWDUWFWCUUMUUOWFZUWCUUJUWDPZUUJQZUUKUWFPZUUKQZUWDUWF
+      UWCUWIUWKUUJUUKUUMUWIUWKGZUUOUUHUWMUUIABWEVFVFUWHWGUWCUWJUWDUUJQZUWDUWJUU
+      JUUJQZUWNPTUWNPUWNUUJUWDUUJWHUWOTUWNUUJWIWJUWNWKWLUWCUWDUUJWMZTGUWNUWDGUW
+      CUWPUUJUWDWMZTUUJUWDWNUWCUUCUUJUWDWQIUWQTGUUCUUDUUGUUIUUOWOZAWPUUJUWDWRWS
+      WTUWDUUJXANXBUWCUWLUWFUUKQZUWFUWLUUKUUKQZUWSPTUWSPUWSUUKUWFUUKWHUWTTUWSUU
+      KWIWJUWSWKWLUWCUWFUUKWMZTGUWSUWFGUWCUXAUUKUWFWMZTUUKUWFWNUWCUUDUUKUWFWQIU
+      XBTGUUCUUDUUGUUIUUOXCZBWPUUKUWFWRWSWTUWFUUKXANXBXDXEUWCUUCUWEAGUWRAXFNUWC
+      UUDUWGBGUXCBXFNXDXGUUJUUKXHXIXJUULUUNUUKUUJJZSZRUUHUUIUUJUUKXKUUHUXEUUIUU
+      NUXEUUPUUKUUJQZEZCXSZUUHUUIUXEUXFTXTUXHUXDUXFTUUKUUJXLXMCUXFXNXOUUHUXGUUI
+      CUXGUVFUVESZRZUUHUUIUUPUUKUUJXPUUHUXJUVDUURSZUUSSZXQZRZUUIUUCUUDUXJUXNYAU
+      UGUUDUVFUVDUUCUXIUXMUUDUVFUVQUVDUUDUUKUVPUUPUVRMUVSOUUCUXIUUTSUXMUUCUVEUU
+      TUUCUVEUVMUUTUUCUUJUVLUUPUVNMUVOOVRUURUUSXROYBYCUUHUVDUXMUUIUUHUVDRZUXKUU
+      IUXLUXOUURUUIUXOUUPUVAUUQUUHUVBUVCYDZUXOUUEUUFKUUCUUDUUGUVDYEYFYGYHUXOUXL
+      UUIUXOUXLRAUUPBUUCUUDUUGUVDUXLWOUXOUVGUXLUXOUVADUUPUVAUVHEZUVADJUVJUUFLEU
+      XQUGBUHLUVHUUFKUIUJUVADUUFKUKULUNUXPYIZVFUUCUUDUUGUVDUXLXCUXOAUUPYJIZUXLU
+      XOUUCUVGUXSUXLYAUUCUUDUUGUVDVIUXRAUUPYKYLYMUUHUVBUVCUXLYNYOXJYPYQYRYTYSYT
+      UUAYTUUB $.
+  $}
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -534353,7 +534493,7 @@ property of surreals and will be used (via surreal cuts) to prove many
   ${
     $d x y z a l r $.
     $( Define surreal addition.  This is the first of the field operations on
-       the surreals.  Definition from [Conway] p. 5.  Definition from [Goshnor]
+       the surreals.  Definition from [Conway] p. 5.  Definition from [Gonshor]
        p. 13.  (Contributed by Scott Fenton, 20-Aug-2024.) $)
     df-adds $a |- +s = norec2 (
      ( x e. _V , a e. _V |->