:: Conway's Normal Form in the {M}izar System
:: by Karol P\kak
::
:: Received April 10, 2025
:: Copyright (c) 2025 Association of Mizar Users

theorem Th1: :: SURREALC:1

for r being Real holds uReal . r in Day omega

proof end;

definition

func No_omega -> No_ordinal uSurreal equals :: SURREALC:def 1
No_uOrdinal_op omega;

coherence
No_uOrdinal_op omega is No_ordinal uSurreal ;

end;

:: deftheorem defines No_omega SURREALC:def 1 :
No_omega = No_uOrdinal_op omega;

definition

let x, y be Surreal;

pred x,y are_commensurate means :: SURREALC:def 2
( ex n being positive Nat st x < (uInt . n) * y & ex n being positive Nat st y < (uInt . n) * x );

symmetry
for x, y being Surreal st ex n being positive Nat st x < (uInt . n) * y & ex n being positive Nat st y < (uInt . n) * x holds
( ex n being positive Nat st y < (uInt . n) * x & ex n being positive Nat st x < (uInt . n) * y ) ;

end;

:: deftheorem defines are_commensurate SURREALC:def 2 :
for x, y being Surreal holds
( x,y are_commensurate iff ( ex n being positive Nat st x < (uInt . n) * y & ex n being positive Nat st y < (uInt . n) * x ) );

theorem Th2: :: SURREALC:2

for x being Surreal st x is positive holds
x,x are_commensurate

proof end;

theorem Th3: :: SURREALC:3

for x, y being Surreal st x,y are_commensurate holds
x is positive

proof end;

theorem Th4: :: SURREALC:4

for x, y, z being Surreal st x,y are_commensurate & y,z are_commensurate holds
x,z are_commensurate

proof end;

theorem Th5: :: SURREALC:5

for x, y, z being Surreal st x == y & x,z are_commensurate holds
y,z are_commensurate

proof end;

theorem :: SURREALC:6

for x, y, z being Surreal st x,z are_commensurate & x <= y & y <= z holds
( x,y are_commensurate & y,z are_commensurate )

proof end;

theorem Th7: :: SURREALC:7

for x, y being Surreal holds
( x,y are_commensurate iff ex n being positive Nat st
( x < (uInt . n) * y & y < (uInt . n) * x ) )

proof end;

theorem Th8: :: SURREALC:8

for x, y being Surreal st x is positive & x == y holds
x,y are_commensurate by Th2, Th5;

definition

let x, y be Surreal;

pred x infinitely< y means :: SURREALC:def 3
for r being positive Real holds x * (uReal . r) < y;

end;

:: deftheorem defines infinitely< SURREALC:def 3 :
for x, y being Surreal holds
( x infinitely< y iff for r being positive Real holds x * (uReal . r) < y );

theorem Th9: :: SURREALC:9

for x, y being Surreal st x infinitely< y holds
x < y

proof end;

theorem :: SURREALC:10

for r being Real holds uReal . r infinitely< No_omega

proof end;

theorem Th11: :: SURREALC:11

for x, y, z being Surreal st x <= y & y infinitely< z holds
x infinitely< z

proof end;

theorem :: SURREALC:12

for x, y, z being Surreal st x infinitely< y & y <= z holds
x infinitely< z by SURREALO:4;

theorem Th13: :: SURREALC:13

for r being positive Real
for x, y being Surreal st x infinitely< y holds
( x * (uReal . r) infinitely< y & x infinitely< y * (uReal . r) )

proof end;

theorem Th14: :: SURREALC:14

for x, y, z being Surreal st x infinitely< y & y infinitely< z holds
x infinitely< z

proof end;

theorem Th15: :: SURREALC:15

for x, y, z being Surreal st x,y are_commensurate & y infinitely< z holds
x infinitely< z

proof end;

Lm1: for x being Surreal
for r, r1 being Real holds (x * (uReal . r)) * (uReal . r1) == x * (uReal . (r * r1))

proof end;

Lm2: for x being Surreal
for r being Real st r <> 0 holds
(x * (uReal . r)) * (uReal . (1 / r)) == x

proof end;

Lm3: for x being Surreal
for r, r1, r2 being Real holds ((x * (uReal . r)) * (uReal . r1)) * (uReal . r2) == x * (uReal . ((r * r1) * r2))

proof end;

theorem Th16: :: SURREALC:16

for x, y, z being Surreal st x,y are_commensurate & z infinitely< x holds
z infinitely< y

proof end;

theorem Th17: :: SURREALC:17

for x, y, z being Surreal st x == y & y infinitely< z holds
x infinitely< z

proof end;

theorem Th18: :: SURREALC:18

for x, y, z being Surreal st x infinitely< z & y infinitely< z holds
x + y infinitely< z

proof end;

theorem :: SURREALC:19

for x, y, z being Surreal st x == y & z infinitely< x holds
z infinitely< y by SURREALO:4;

theorem Th20: :: SURREALC:20

for x, y being Surreal
for r being Real st 0_No <= x & x infinitely< y holds
x * (uReal . r) < y

proof end;

definition

let A be Ordinal;

func No_omega_op A -> ManySortedSet of Day A means :Def4: :: SURREALC:def 4
ex S being Function-yielding c=-monotone Sequence st
( dom S = succ A & it = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for x being object st x in Day B holds
SB . x = [({0_No} \/ { (((union (rng (S | B))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } ), { (((union (rng (S | B))) . xR) *' (uReal . r)) where xR is Element of R_ x, r is Element of REAL : ( xR in R_ x & r is positive ) } ] ) ) ) );

existence
ex b₁ being ManySortedSet of Day A ex S being Function-yielding c=-monotone Sequence st
( dom S = succ A & b₁ = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for x being object st x in Day B holds
SB . x = [({0_No} \/ { (((union (rng (S | B))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } ), { (((union (rng (S | B))) . xR) *' (uReal . r)) where xR is Element of R_ x, r is Element of REAL : ( xR in R_ x & r is positive ) } ] ) ) ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of Day A st ex S being Function-yielding c=-monotone Sequence st
( dom S = succ A & b₁ = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for x being object st x in Day B holds
SB . x = [({0_No} \/ { (((union (rng (S | B))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } ), { (((union (rng (S | B))) . xR) *' (uReal . r)) where xR is Element of R_ x, r is Element of REAL : ( xR in R_ x & r is positive ) } ] ) ) ) ) & ex S being Function-yielding c=-monotone Sequence st
( dom S = succ A & b₂ = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for x being object st x in Day B holds
SB . x = [({0_No} \/ { (((union (rng (S | B))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } ), { (((union (rng (S | B))) . xR) *' (uReal . r)) where xR is Element of R_ x, r is Element of REAL : ( xR in R_ x & r is positive ) } ] ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines No_omega_op SURREALC:def 4 :
for A being Ordinal
for b₂ being ManySortedSet of Day A holds
( b₂ = No_omega_op A iff ex S being Function-yielding c=-monotone Sequence st
( dom S = succ A & b₂ = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for x being object st x in Day B holds
SB . x = [({0_No} \/ { (((union (rng (S | B))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } ), { (((union (rng (S | B))) . xR) *' (uReal . r)) where xR is Element of R_ x, r is Element of REAL : ( xR in R_ x & r is positive ) } ] ) ) ) ) );

theorem Th21: :: SURREALC:21

for S being Function-yielding c=-monotone Sequence st ( for B being Ordinal st B in dom S holds
ex SB being ManySortedSet of Day B st
( S . B = SB & ( for x being object st x in Day B holds
SB . x = [({0_No} \/ { (((union (rng (S | B))) . xL) *' (uReal . r)) where xL is Element of L_ x, r is Element of REAL : ( xL in L_ x & r is positive ) } ), { (((union (rng (S | B))) . xR) *' (uReal . r)) where xR is Element of R_ x, r is Element of REAL : ( xR in R_ x & r is positive ) } ] ) ) ) holds
for A being Ordinal st A in dom S holds
No_omega_op A = S . A

proof end;

definition

let x be Surreal;

func No_omega^ x -> set equals :: SURREALC:def 5
(No_omega_op (born x)) . x;

coherence
(No_omega_op (born x)) . x is set ;

end;

:: deftheorem defines No_omega^ SURREALC:def 5 :
for x being Surreal holds No_omega^ x = (No_omega_op (born x)) . x;

Lm4: for o being object
for x being Surreal holds
( No_omega^ x is pair & ( not o in L_ (No_omega^ x) or o = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ x & o = (No_omega^ xL) *' (uReal . r) ) ) & ( ( o = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ x & o = (No_omega^ xL) *' (uReal . r) ) ) implies o in L_ (No_omega^ x) ) & ( o in R_ (No_omega^ x) implies ex xR being Surreal ex r being positive Real st
( xR in R_ x & o = (No_omega^ xR) *' (uReal . r) ) ) & ( ex xR being Surreal ex r being positive Real st
( xR in R_ x & o = (No_omega^ xR) *' (uReal . r) ) implies o in R_ (No_omega^ x) ) )

proof end;

Lm5: for x being Surreal holds
( No_omega^ x is positive Surreal & ( for y1, y2, Ny1, Ny2 being Surreal st Ny1 = No_omega^ y1 & Ny2 = No_omega^ y2 holds
( ( y1 <= y2 implies Ny1 <= Ny2 ) & ( y1 < y2 implies Ny1 infinitely< Ny2 ) ) ) )

proof end;

registration

let x be Surreal;

cluster No_omega^ x -> surreal ;

coherence
No_omega^ x is surreal by Lm5;

end;

registration

let x be Surreal;

cluster No_omega^ x -> positive ;

coherence
No_omega^ x is positive by Lm5;

end;

theorem Th22: :: SURREALC:22

for o being object
for x being Surreal holds
( o in L_ (No_omega^ x) iff ( o = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ x & o = (No_omega^ xL) * (uReal . r) ) ) )

proof end;

theorem Th23: :: SURREALC:23

for o being object
for x being Surreal holds
( o in R_ (No_omega^ x) iff ex xR being Surreal ex r being positive Real st
( xR in R_ x & o = (No_omega^ xR) * (uReal . r) ) )

proof end;

theorem :: SURREALC:24

for x, y being Surreal st x <= y holds
No_omega^ x <= No_omega^ y by Lm5;

theorem Th25: :: SURREALC:25

for x, y being Surreal st x < y holds
No_omega^ x infinitely< No_omega^ y by Lm5;

theorem Th26: :: SURREALC:26

No_omega^ 0_No = 1_No

proof end;

theorem Th27: :: SURREALC:27

for x, y being Surreal holds (No_omega^ x) * (No_omega^ y) == No_omega^ (x + y)

proof end;

theorem :: SURREALC:28

for x being Surreal holds (No_omega^ x) " == No_omega^ (- x)

proof end;

theorem Th29: :: SURREALC:29

for y, xL, x being Surreal st xL <= x & xL, No_omega^ y are_commensurate & not x, No_omega^ y are_commensurate holds
No_omega^ y infinitely< x

proof end;

theorem Th30: :: SURREALC:30

for y, x, xR being Surreal st 0_No < x & x <= xR & xR, No_omega^ y are_commensurate & not x, No_omega^ y are_commensurate holds
x infinitely< No_omega^ y

proof end;

definition

let x be Surreal;

func |.x.| -> Surreal equals :Def6: :: SURREALC:def 6
x if 0_No <= x
otherwise - x;

coherence
( ( 0_No <= x implies x is Surreal ) & ( not 0_No <= x implies - x is Surreal ) ) ;
correctness
consistency
for b₁ being Surreal holds verum;
;

end;

:: deftheorem Def6 defines |. SURREALC:def 6 :
for x being Surreal holds
( ( 0_No <= x implies |.x.| = x ) & ( not 0_No <= x implies |.x.| = - x ) );

theorem Th31: :: SURREALC:31

for x being Surreal holds 0_No <= |.x.|

proof end;

theorem :: SURREALC:32

for x being Surreal holds
( |.x.| = x or |.x.| = - x ) by Def6;

theorem :: SURREALC:33

for x being Surreal holds
( x == 0_No iff |.x.| == 0_No )

proof end;

theorem Th34: :: SURREALC:34

for x being Surreal holds
( - |.x.| <= x & x <= |.x.| )

proof end;

theorem Th35: :: SURREALC:35

for x, y being Surreal holds
( ( - y <= x & x <= y ) iff |.x.| <= y )

proof end;

theorem Th36: :: SURREALC:36

for x being Surreal st not x == 0_No holds
|.x.| is positive

proof end;

theorem Th37: :: SURREALC:37

for x, y being Surreal holds |.(x + y).| <= |.x.| + |.y.|

proof end;

theorem Th38: :: SURREALC:38

for x being Surreal st x == 0_No holds
|.(- x).| == |.x.|

proof end;

theorem Th39: :: SURREALC:39

for x being Surreal st not x == 0_No holds
|.(- x).| = |.x.|

proof end;

theorem Th40: :: SURREALC:40

for x being Surreal holds |.(- x).| == |.x.| by Th39, Th38;

theorem Th41: :: SURREALC:41

for x, y, z being Surreal st |.x.| infinitely< z & |.y.| infinitely< z holds
|.(x + y).| infinitely< z

proof end;

theorem Th42: :: SURREALC:42

for x, z being Surreal st |.x.| infinitely< z holds
|.(- x).| infinitely< z

proof end;

theorem Th43: :: SURREALC:43

for x, y, z being Surreal st |.x.| infinitely< z & |.y.| infinitely< z holds
|.(x - y).| infinitely< z

proof end;

theorem Th44: :: SURREALC:44

for x, y being Surreal st |.y.| infinitely< x holds
not x + y == 0_No

proof end;

theorem Th45: :: SURREALC:45

for x, y being Surreal st |.y.| infinitely< |.x.| holds
not x + y == 0_No

proof end;

theorem Th46: :: SURREALC:46

for x, y being Surreal st |.y.| infinitely< x holds
not x == 0_No

proof end;

theorem Th47: :: SURREALC:47

for x, y being Surreal st |.y.| infinitely< |.x.| holds
not x == 0_No

proof end;

theorem Th48: :: SURREALC:48

for x, y being Surreal st x == y holds
|.x.| == |.y.|

proof end;

theorem Th49: :: SURREALC:49

for x, y being Surreal holds |.(|.x.| - |.y.|).| <= |.(x - y).|

proof end;

theorem :: SURREALC:50

for x being Surreal holds |.|.x.|.| = |.x.| by Th31, Def6;

theorem Th51: :: SURREALC:51

for x, y, z being Surreal st x <= y & y <= z holds
|.y.| <= |.x.| + |.z.|

proof end;

theorem Th52: :: SURREALC:52

for x, y being Surreal holds
( ( - y < x & x < y ) iff |.x.| < y )

proof end;

theorem Th53: :: SURREALC:53

for x, y being Surreal
for r being Real st 0_No <= x & x infinitely< y holds
|.(x * (uReal . r)).| infinitely< y

proof end;

Lm6: for x being Surreal st x is positive holds
ex y being Surreal st x, No_omega^ y are_commensurate

proof end;

Lm7: for x being Surreal st x is positive holds
for y1, y2 being Surreal st x, No_omega^ y1 are_commensurate & x, No_omega^ y2 are_commensurate holds
y1 <= y2

proof end;

:: as a Pair of Commensurate Leader and Positive Real Number

definition

let x be Surreal;
assume A1: not x == 0_No ;

func omega-y x -> uSurreal means :Def7: :: SURREALC:def 7
|.x.|, No_omega^ it are_commensurate ;

existence
ex b₁ being uSurreal st |.x.|, No_omega^ b₁ are_commensurate

proof end;

uniqueness
for b₁, b₂ being uSurreal st |.x.|, No_omega^ b₁ are_commensurate & |.x.|, No_omega^ b₂ are_commensurate holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines omega-y SURREALC:def 7 :
for x being Surreal st not x == 0_No holds
for b₂ being uSurreal holds
( b₂ = omega-y x iff |.x.|, No_omega^ b₂ are_commensurate );

theorem Th54: :: SURREALC:54

for x, y being Surreal st x, No_omega^ y are_commensurate holds
ex s being positive Real st |.(x - ((No_omega^ y) * (uReal . s))).| infinitely< x

proof end;

theorem :: SURREALC:55

for x, y being Surreal
for r being Real st x is positive & |.(x - ((No_omega^ y) * (uReal . r))).| infinitely< x holds
r is positive

proof end;

Lm8: for x, y being Surreal
for r1, r2 being Real st x, No_omega^ y are_commensurate & |.(x - ((No_omega^ y) * (uReal . r1))).| infinitely< x & |.(x - ((No_omega^ y) * (uReal . r2))).| infinitely< x holds
r2 <= r1

proof end;

theorem Th56: :: SURREALC:56

for x being Surreal st not x == 0_No holds
omega-y x = omega-y (- x)

proof end;

Lm9: for x, y being Surreal
for r1, r2 being Real st |.x.|, No_omega^ y are_commensurate & |.(x - ((No_omega^ y) * (uReal . r1))).| infinitely< |.x.| & |.(x - ((No_omega^ y) * (uReal . r2))).| infinitely< |.x.| holds
r2 = r1

proof end;

definition

let x be Surreal;
assume A1: not x == 0_No ;

func omega-r x -> non zero Real means :Def8: :: SURREALC:def 8
|.(x - ((No_omega^ (omega-y x)) * (uReal . it))).| infinitely< |.x.|;

existence
ex b₁ being non zero Real st |.(x - ((No_omega^ (omega-y x)) * (uReal . b₁))).| infinitely< |.x.|

proof end;

uniqueness
for b₁, b₂ being non zero Real st |.(x - ((No_omega^ (omega-y x)) * (uReal . b₁))).| infinitely< |.x.| & |.(x - ((No_omega^ (omega-y x)) * (uReal . b₂))).| infinitely< |.x.| holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines omega-r SURREALC:def 8 :
for x being Surreal st not x == 0_No holds
for b₂ being non zero Real holds
( b₂ = omega-r x iff |.(x - ((No_omega^ (omega-y x)) * (uReal . b₂))).| infinitely< |.x.| );

theorem Th57: :: SURREALC:57

for x, y being Surreal
for n being positive Nat st |.y.| * (uReal . ((n + 1) / n)) < |.x.| holds
|.x.|,|.(x + y).| are_commensurate

proof end;

theorem :: SURREALC:58

for x being Surreal st |.x.| is positive holds
not x == 0_No by Def6;

theorem Th59: :: SURREALC:59

for x, y being Surreal
for r, r1, r2 being Real st x * (uReal . r1) < y * (uReal . r2) & 0 < r holds
x * (uReal . (r1 * r)) < y * (uReal . (r2 * r))

proof end;

theorem :: SURREALC:60

for x, y being Surreal
for r, r1, r2 being Real st x * (uReal . r1) <= y * (uReal . r2) & 0 <= r holds
x * (uReal . (r1 * r)) <= y * (uReal . (r2 * r))

proof end;

theorem Th61: :: SURREALC:61

for x, y being Surreal st not x == 0_No & not y == 0_No holds
( omega-y x = omega-y y iff |.x.|,|.y.| are_commensurate )

proof end;

theorem Th62: :: SURREALC:62

for x, y being Surreal st not x == 0_No & not x + y == 0_No & omega-y x = omega-y (x + y) & omega-r x = omega-r (x + y) holds
|.y.| infinitely< |.x.|

proof end;

theorem Th63: :: SURREALC:63

for x, y being Surreal st |.y.| infinitely< |.x.| holds
( not x == 0_No & not x + y == 0_No & omega-y x = omega-y (x + y) & omega-r x = omega-r (x + y) )

proof end;

theorem Th64: :: SURREALC:64

for x, y being Surreal st not x == 0_No & y == 0_No holds
y infinitely< |.x.|

proof end;

theorem :: SURREALC:65

for r being Real st uReal . r == 0_No holds
r = 0

proof end;

Lm10: for x being Surreal
for r being Real st x is positive & r > 0 holds
(uReal . r) * x,x are_commensurate

proof end;

theorem Th66: :: SURREALC:66

for x being Surreal
for r being Real st x is positive & r <> 0 holds
|.((uReal . r) * x).|,x are_commensurate

proof end;

scheme :: SURREALC:sch 1
Simplest{ P₁[ Surreal] } :

ex s being uSurreal st
( P₁[s] & ( for x being uSurreal st P₁[x] & x <> s holds
born s in born x ) )

provided

A1: ex x being Surreal st P₁[x] and
A2: for x, y, z being Surreal st x <= y & y <= z & P₁[x] & P₁[z] holds
P₁[y]

proof end;

definition

let f be Function;

attr f is surreal-valued means :Def9: :: SURREALC:def 9
rng f is surreal-membered ;

end;

:: deftheorem Def9 defines surreal-valued SURREALC:def 9 :
for f being Function holds
( f is surreal-valued iff rng f is surreal-membered );

registration

let s be Surreal;

cluster <%s%> -> surreal-valued ;

coherence
<%s%> is surreal-valued

proof end;

end;

registration

cluster Relation-like Function-like Sequence-like surreal-valued for set ;

existence
ex b₁ being Sequence st b₁ is surreal-valued

proof end;

end;

registration

let f be surreal-valued Function;

cluster proj2 f -> surreal-membered ;

coherence
rng f is surreal-membered by Def9;

end;

definition

mode Surreal-Sequence is surreal-valued Sequence;

end;

registration

let X be surreal-membered set ;

cluster -> surreal-membered for Element of bool X;

coherence
for b₁ being Subset of X holds b₁ is surreal-membered by SURREAL0:def 16;

end;

registration

let f be surreal-valued Function;
let X be set ;

cluster f | X -> surreal-valued ;

coherence
f | X is surreal-valued

proof end;

end;

registration

let f, g be Surreal-Sequence;

cluster f ^ g -> surreal-valued ;

coherence
f ^ g is surreal-valued

proof end;

end;

definition

let f be Function;

attr f is uniq-surreal-valued means :Def10: :: SURREALC:def 10
rng f is uniq-surreal-membered ;

end;

:: deftheorem Def10 defines uniq-surreal-valued SURREALC:def 10 :
for f being Function holds
( f is uniq-surreal-valued iff rng f is uniq-surreal-membered );

registration

let s be uSurreal;

cluster <%s%> -> uniq-surreal-valued ;

coherence
<%s%> is uniq-surreal-valued

proof end;

end;

registration

cluster Relation-like Function-like Sequence-like uniq-surreal-valued for set ;

existence
ex b₁ being Sequence st b₁ is uniq-surreal-valued

proof end;

end;

registration

let f be uniq-surreal-valued Function;

cluster proj2 f -> uniq-surreal-membered ;

coherence
rng f is uniq-surreal-membered by Def10;

end;

definition

mode uSurreal-Sequence is uniq-surreal-valued Sequence;

end;

registration

let X be uniq-surreal-membered set ;

cluster -> uniq-surreal-membered for Element of bool X;

coherence
for b₁ being Subset of X holds b₁ is uniq-surreal-membered by SURREALO:def 12;

end;

registration

let f be uniq-surreal-valued Function;
let X be set ;

cluster f | X -> uniq-surreal-valued ;

coherence
f | X is uniq-surreal-valued

proof end;

end;

registration

let f, g be uSurreal-Sequence;

cluster f ^ g -> uniq-surreal-valued ;

coherence
f ^ g is uniq-surreal-valued

proof end;

end;

registration

cluster uniq-surreal-membered -> surreal-membered for set ;

coherence
for b₁ being set st b₁ is uniq-surreal-membered holds
b₁ is surreal-membered ;

end;

registration

cluster Relation-like Function-like uniq-surreal-valued -> surreal-valued for set ;

coherence
for b₁ being Function st b₁ is uniq-surreal-valued holds
b₁ is surreal-valued ;

end;

definition

let S be Surreal-Sequence;

attr S is strictly_decreasing means :Def11: :: SURREALC:def 11
for a, b being Ordinal st a in b & b in dom S holds
for sa, sb being Surreal st sa = S . a & sb = S . b holds
sb < sa;

end;

:: deftheorem Def11 defines strictly_decreasing SURREALC:def 11 :
for S being Surreal-Sequence holds
( S is strictly_decreasing iff for a, b being Ordinal st a in b & b in dom S holds
for sa, sb being Surreal st sa = S . a & sb = S . b holds
sb < sa );

registration

let s be uSurreal;

cluster <%s%> -> strictly_decreasing ;

coherence
<%s%> is strictly_decreasing

proof end;

end;

registration

cluster Relation-like Function-like Sequence-like surreal-valued uniq-surreal-valued strictly_decreasing for set ;

existence
ex b₁ being uSurreal-Sequence st b₁ is strictly_decreasing

proof end;

end;

registration

let s1, s2 be non-zero Sequence;

cluster s1 ^ s2 -> non-zero ;

coherence
s1 ^ s2 is non-zero

proof end;

end;

registration

cluster Relation-like REAL -valued Function-like Sequence-like non-zero complex-valued ext-real-valued real-valued for set ;

existence
ex b₁ being Sequence of REAL st b₁ is non-zero

proof end;

end;

definition

let s be object ;
let y be Surreal;
let r be Real;
let x be object ;

attr x is s,y,r _term means :: SURREALC:def 12
( not x +' (-' s) == 0_No & omega-y (x +' (-' s)) == y & omega-r (x +' (-' s)) = r );

end;

:: deftheorem defines _term SURREALC:def 12 :
for s being object
for y being Surreal
for r being Real
for x being object holds
( x is s,y,r _term iff ( not x +' (-' s) == 0_No & omega-y (x +' (-' s)) == y & omega-r (x +' (-' s)) = r ) );

definition

let s, y be Surreal;
let r be Real;
let x be Surreal;

redefine attr x is s,y,r _term means :: SURREALC:def 13
( not x - s == 0_No & omega-y (x - s) == y & omega-r (x - s) = r );

compatibility
( x is s,y,r _term iff ( not x - s == 0_No & omega-y (x - s) == y & omega-r (x - s) = r ) ) ;

end;

:: deftheorem defines _term SURREALC:def 13 :
for s, y being Surreal
for r being Real
for x being Surreal holds
( x is s,y,r _term iff ( not x - s == 0_No & omega-y (x - s) == y & omega-r (x - s) = r ) );

theorem Th67: :: SURREALC:67

for y being Surreal
for r being Real st r <> 0 holds
not (uReal . r) * (No_omega^ y) == 0_No

proof end;

theorem Th68: :: SURREALC:68

for y being Surreal
for r being Real st r <> 0 holds
omega-y ((uReal . r) * (No_omega^ y)) = Unique_No y

proof end;

theorem Th69: :: SURREALC:69

for y being Surreal
for r being Real
for s being Surreal st r <> 0 holds
s + ((uReal . r) * (No_omega^ y)) is s,y,r _term

proof end;

theorem Th70: :: SURREALC:70

for x, y being Surreal st x == y & not x == 0_No holds
( omega-y x = omega-y y & omega-r x = omega-r y )

proof end;

theorem Th71: :: SURREALC:71

for x, y being Surreal
for r being Real
for s being Surreal st r <> 0 holds
( (s + ((uReal . r) * (No_omega^ y))) + x is s,y,r _term iff |.x.| infinitely< No_omega^ y )

proof end;

theorem Th72: :: SURREALC:72

for x, y, z being Surreal
for r being Real
for s being Surreal st r <> 0 & x is s,y,r _term & x == z holds
z is s,y,r _term

proof end;

theorem Th73: :: SURREALC:73

for x, y being Surreal
for r being Real
for s being Surreal st r <> 0 holds
( x is s,y,r _term iff |.(x - (s + ((uReal . r) * (No_omega^ y)))).| infinitely< No_omega^ y )

proof end;

theorem Th74: :: SURREALC:74

for r being Real
for s, p being Surreal st r <> 0 holds
for x, y, z being Surreal st x is s,p,r _term & z is s,p,r _term & x <= y & y <= z holds
y is s,p,r _term

proof end;

definition

let r be Sequence of REAL ;
let y, s be Sequence;
let alpha be Ordinal;
let x be Surreal;

pred x in_meets_terms s,y,r,alpha means :: SURREALC:def 14
for beta being Ordinal
for sb, yb being Surreal st beta in alpha & sb = s . beta & yb = y . beta holds
x is sb,yb,r . beta _term ;

end;

:: deftheorem defines in_meets_terms SURREALC:def 14 :
for r being Sequence of REAL
for y, s being Sequence
for alpha being Ordinal
for x being Surreal holds
( x in_meets_terms s,y,r,alpha iff for beta being Ordinal
for sb, yb being Surreal st beta in alpha & sb = s . beta & yb = y . beta holds
x is sb,yb,r . beta _term );

definition

let r be Sequence of REAL ;
let y, s be Sequence;
let alpha be Ordinal;

pred s,y,r simplest_on_position alpha means :: SURREALC:def 15
for sa being Surreal st sa = s . alpha holds
( ( 0 = alpha implies sa = 0_No ) & ( 0 <> alpha implies ( sa in_meets_terms s,y,r,alpha & ( for x being uSurreal st x in_meets_terms s,y,r,alpha & x <> sa holds
born sa in born x ) ) ) );

end;

:: deftheorem defines simplest_on_position SURREALC:def 15 :
for r being Sequence of REAL
for y, s being Sequence
for alpha being Ordinal holds
( s,y,r simplest_on_position alpha iff for sa being Surreal st sa = s . alpha holds
( ( 0 = alpha implies sa = 0_No ) & ( 0 <> alpha implies ( sa in_meets_terms s,y,r,alpha & ( for x being uSurreal st x in_meets_terms s,y,r,alpha & x <> sa holds
born sa in born x ) ) ) ) );

theorem Th75: :: SURREALC:75

for x being Surreal
for r being Sequence of REAL
for y, s1, s2 being Sequence
for alpha being Ordinal st s1 | alpha = s2 | alpha & x in_meets_terms s1,y,r,alpha holds
x in_meets_terms s2,y,r,alpha

proof end;

theorem Th76: :: SURREALC:76

for r being Sequence of REAL
for y, s1, s2 being Sequence
for alpha being Ordinal st s1 . alpha is uSurreal & s2 . alpha is uSurreal & s1 | alpha = s2 | alpha & s1,y,r simplest_on_position alpha & s2,y,r simplest_on_position alpha holds
s1 . alpha = s2 . alpha

proof end;

definition

let r be Sequence of REAL ;
let y, s be Sequence;
let alpha be Ordinal;

pred s,y,r simplest_up_to alpha means :: SURREALC:def 16
for beta being Ordinal st beta in alpha holds
s,y,r simplest_on_position beta;

end;

:: deftheorem defines simplest_up_to SURREALC:def 16 :
for r being Sequence of REAL
for y, s being Sequence
for alpha being Ordinal holds
( s,y,r simplest_up_to alpha iff for beta being Ordinal st beta in alpha holds
s,y,r simplest_on_position beta );

theorem Th77: :: SURREALC:77

for r being Sequence of REAL
for y being Sequence
for s1, s2 being uSurreal-Sequence
for alpha being Ordinal st alpha c= dom s1 & alpha c= dom s2 & s1,y,r simplest_up_to alpha & s2,y,r simplest_up_to alpha holds
s1 | alpha = s2 | alpha

proof end;

theorem :: SURREALC:78

for r being Sequence of REAL
for y, s being Sequence
for alpha, beta being Ordinal st beta c= alpha & s,y,r simplest_up_to alpha holds
s,y,r simplest_up_to beta ;

theorem Th79: :: SURREALC:79

for x being Surreal
for r being Sequence of REAL
for y, s being Sequence
for alpha being Ordinal holds
( x in_meets_terms s,y,r,alpha iff x in_meets_terms s | (succ alpha),y,r,alpha )

proof end;

theorem Th80: :: SURREALC:80

for r being Sequence of REAL
for y, s being Sequence
for alpha being Ordinal holds
( s | (succ alpha),y,r simplest_on_position alpha iff s,y,r simplest_on_position alpha )

proof end;

theorem Th81: :: SURREALC:81

for r being non-zero Sequence of REAL
for p, s being Sequence
for alpha being Ordinal st alpha c= dom r holds
for x, y, z being Surreal st x <= y & y <= z & x in_meets_terms s,p,r,alpha & z in_meets_terms s,p,r,alpha holds
y in_meets_terms s,p,r,alpha

proof end;

theorem Th82: :: SURREALC:82

for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence ex s being uSurreal-Sequence st
( dom s = succ ((dom r) /\ (dom y)) & s,y,r simplest_up_to dom s )

proof end;

definition

let r be non-zero Sequence of REAL ;
let y be strictly_decreasing Surreal-Sequence;

func Partial_Sums (r,y) -> uSurreal-Sequence means :Def17: :: SURREALC:def 17
( dom it = succ ((dom r) /\ (dom y)) & ( for A being Ordinal st A in dom it holds
it,y,r simplest_on_position A ) );

existence
ex b₁ being uSurreal-Sequence st
( dom b₁ = succ ((dom r) /\ (dom y)) & ( for A being Ordinal st A in dom b₁ holds
b₁,y,r simplest_on_position A ) )

proof end;

uniqueness
for b₁, b₂ being uSurreal-Sequence st dom b₁ = succ ((dom r) /\ (dom y)) & ( for A being Ordinal st A in dom b₁ holds
b₁,y,r simplest_on_position A ) & dom b₂ = succ ((dom r) /\ (dom y)) & ( for A being Ordinal st A in dom b₂ holds
b₂,y,r simplest_on_position A ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def17 defines Partial_Sums SURREALC:def 17 :
for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for b₃ being uSurreal-Sequence holds
( b₃ = Partial_Sums (r,y) iff ( dom b₃ = succ ((dom r) /\ (dom y)) & ( for A being Ordinal st A in dom b₃ holds
b₃,y,r simplest_on_position A ) ) );

definition

let r be non-zero Sequence of REAL ;
let y be strictly_decreasing Surreal-Sequence;

func Sum (r,y) -> uSurreal equals :: SURREALC:def 18
(Partial_Sums (r,y)) . ((dom r) /\ (dom y));

coherence
(Partial_Sums (r,y)) . ((dom r) /\ (dom y)) is uSurreal

proof end;

end;

:: deftheorem defines Sum SURREALC:def 18 :
for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence holds Sum (r,y) = (Partial_Sums (r,y)) . ((dom r) /\ (dom y));

registration

let s be strictly_decreasing Surreal-Sequence;
let A be Ordinal;

cluster s | A -> strictly_decreasing ;

coherence
s | A is strictly_decreasing

proof end;

end;

registration

let R be non-zero Relation;
let X be set ;

cluster R | X -> non-zero ;

coherence
R | X is non-zero

proof end;

end;

theorem Th83: :: SURREALC:83

for x being Surreal
for r being Sequence of REAL
for y, s being Sequence
for A, B being Ordinal st A c= B holds
( x in_meets_terms s,y,r,A iff x in_meets_terms s,y | B,r | B,A )

proof end;

theorem Th84: :: SURREALC:84

for r being Sequence of REAL
for y, s being Sequence
for A, B being Ordinal st B c= A holds
( s,y | A,r | A simplest_on_position B iff s,y,r simplest_on_position B )

proof end;

theorem Th85: :: SURREALC:85

for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for A being Ordinal holds (Partial_Sums (r,y)) | (succ A) = Partial_Sums ((r | A),(y | A))

proof end;

definition

let r be non-zero Sequence of REAL ;
let y be strictly_decreasing Surreal-Sequence;
let alpha be Ordinal;
let x be Surreal;

pred r,y,alpha name_like x means :: SURREALC:def 19
( alpha c= dom r & dom r = dom y & ( for beta being Ordinal st beta in alpha holds
for Pb being Surreal st Pb = (Partial_Sums (r,y)) . beta holds
( not x == Pb & r . beta = omega-r (x - Pb) & y . beta = omega-y (x - Pb) ) ) );

end;

:: deftheorem defines name_like SURREALC:def 19 :
for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for alpha being Ordinal
for x being Surreal holds
( r,y,alpha name_like x iff ( alpha c= dom r & dom r = dom y & ( for beta being Ordinal st beta in alpha holds
for Pb being Surreal st Pb = (Partial_Sums (r,y)) . beta holds
( not x == Pb & r . beta = omega-r (x - Pb) & y . beta = omega-y (x - Pb) ) ) ) );

theorem Th86: :: SURREALC:86

for x being Surreal
for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for alpha, beta being Ordinal st alpha c= beta & r,y,beta name_like x holds
r,y,alpha name_like x by XBOOLE_1:1;

theorem Th87: :: SURREALC:87

for x being Surreal
for r1, r2 being non-zero Sequence of REAL
for y1, y2 being strictly_decreasing Surreal-Sequence
for A being Ordinal st r1,y1,A name_like x & r2,y2,A name_like x holds
( r1 | A = r2 | A & y1 | A = y2 | A )

proof end;

theorem Th88: :: SURREALC:88

for x being Surreal
for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for A being Ordinal st r,y,A name_like x holds
x in_meets_terms Partial_Sums (r,y),y,r,A

proof end;

theorem Th89: :: SURREALC:89

for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence holds Sum (r,y) in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y)

proof end;

theorem Th90: :: SURREALC:90

for x, z being Surreal
for r being non-zero Sequence of REAL
for y being Sequence
for s being Surreal-Sequence
for A, B being Ordinal st B in A & A c= (dom r) /\ (dom y) & A c= dom s holds
for yb being Surreal st yb = y . B & x in_meets_terms s,y,r,A & z in_meets_terms s,y,r,A holds
|.(x - z).| infinitely< No_omega^ yb

proof end;

theorem :: SURREALC:91

for x being Surreal
for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for alpha being Ordinal st r,y,alpha name_like x holds
r | alpha,y | alpha,alpha name_like x

proof end;

theorem Th92: :: SURREALC:92

for z being Surreal
for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence st z in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y) & not z == Sum (r,y) holds
for A being Ordinal
for yA being Surreal st A in (dom r) /\ (dom y) & yA = y . A holds
omega-y ((Sum (r,y)) - z) < yA

proof end;

theorem :: SURREALC:93

for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for A being Ordinal st A c= (dom r) /\ (dom y) holds
(Partial_Sums (r,y)) . A = Sum ((r | A),(y | A))

proof end;

theorem :: SURREALC:94

for x, z being Surreal
for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence st x in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y) & z in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y) & not x == z holds
for A being Ordinal
for yA being Surreal st A in (dom r) /\ (dom y) & yA = y . A holds
omega-y (x - z) < yA

proof end;

theorem Th95: :: SURREALC:95

for x being Surreal st ( for r being non-zero Sequence of REAL
for y being strictly_decreasing uSurreal-Sequence st dom r = dom y & r,y, dom r name_like x holds
not Sum (r,y) == x ) holds
for alpha being Ordinal ex r being non-zero Sequence of REAL ex y being strictly_decreasing uSurreal-Sequence st
( dom r = succ alpha & succ alpha = dom y & r,y, succ alpha name_like x )

proof end;

definition

let s be Surreal-Sequence;

func born s -> Ordinal-Sequence means :Def20: :: SURREALC:def 20
( dom it = dom s & ( for alpha being Ordinal st alpha in dom s holds
for sa being Surreal st sa = s . alpha holds
it . alpha = born sa ) );

existence
ex b₁ being Ordinal-Sequence st
( dom b₁ = dom s & ( for alpha being Ordinal st alpha in dom s holds
for sa being Surreal st sa = s . alpha holds
b₁ . alpha = born sa ) )

proof end;

uniqueness
for b₁, b₂ being Ordinal-Sequence st dom b₁ = dom s & ( for alpha being Ordinal st alpha in dom s holds
for sa being Surreal st sa = s . alpha holds
b₁ . alpha = born sa ) & dom b₂ = dom s & ( for alpha being Ordinal st alpha in dom s holds
for sa being Surreal st sa = s . alpha holds
b₂ . alpha = born sa ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines born SURREALC:def 20 :
for s being Surreal-Sequence
for b₂ being Ordinal-Sequence holds
( b₂ = born s iff ( dom b₂ = dom s & ( for alpha being Ordinal st alpha in dom s holds
for sa being Surreal st sa = s . alpha holds
b₂ . alpha = born sa ) ) );

theorem Th96: :: SURREALC:96

for r being Sequence of REAL
for y being Surreal-Sequence
for s being uSurreal-Sequence
for A being Ordinal st s,y,r simplest_up_to A & A c= succ (dom y) holds
s | A is one-to-one

proof end;

registration

let r be non-zero Sequence of REAL ;
let y be strictly_decreasing Surreal-Sequence;

cluster Partial_Sums (r,y) -> one-to-one ;

coherence
Partial_Sums (r,y) is one-to-one

proof end;

end;

theorem Th97: :: SURREALC:97

for r being Sequence of REAL
for y being Surreal-Sequence
for s being uSurreal-Sequence
for alpha being Ordinal st s,y,r simplest_up_to alpha & s | alpha is one-to-one holds
(born s) | alpha is increasing

proof end;

registration

let r be non-zero Sequence of REAL ;
let y be strictly_decreasing Surreal-Sequence;

cluster born (Partial_Sums (r,y)) -> increasing ;

coherence
born (Partial_Sums (r,y)) is increasing

proof end;

end;

theorem Th98: :: SURREALC:98

for x being Surreal
for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for s being uSurreal-Sequence
for A being Ordinal st A c= dom r & x in_meets_terms s,y,r,A & s,y,r simplest_up_to succ A holds
rng (born (s | (succ A))) c= succ (born_eq x)

proof end;

theorem Th99: :: SURREALC:99

for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence holds (dom r) /\ (dom y) c= born (Sum (r,y))

proof end;

:: Conway Normal Form:

theorem Th100: :: SURREALC:100

for x being Surreal ex r being non-zero Sequence of REAL ex y being strictly_decreasing uSurreal-Sequence st
( dom r = dom y & dom y c= born_eq x & Sum (r,y) == x )

proof end;

theorem Th101: :: SURREALC:101

for r being non-zero Sequence of REAL
for y being strictly_decreasing uSurreal-Sequence st dom r = dom y holds
r,y, dom r name_like Sum (r,y)

proof end;

theorem Th102: :: SURREALC:102

for r1, r2 being non-zero Sequence of REAL
for y1, y2 being strictly_decreasing uSurreal-Sequence st dom r1 = dom y1 & dom r2 = dom y2 & Sum (r1,y1) == Sum (r2,y2) holds
( r1 = r2 & y1 = y2 )

proof end;

theorem Th103: :: SURREALC:103

for r being non-zero Sequence of REAL
for y being strictly_decreasing uSurreal-Sequence
for A being Ordinal st A c= dom r & dom r = dom y holds
for x, z being Surreal st r,y,A name_like x & x == z holds
r,y,A name_like z

proof end;

definition

let x be surreal number ;

func name-ord x -> Ordinal means :Def21: :: SURREALC:def 21
ex r being non-zero Sequence of REAL ex y being strictly_decreasing uSurreal-Sequence st
( it = dom r & dom r = dom y & Sum (r,y) == x );

existence
ex b₁ being Ordinal ex r being non-zero Sequence of REAL ex y being strictly_decreasing uSurreal-Sequence st
( b₁ = dom r & dom r = dom y & Sum (r,y) == x )

proof end;

uniqueness
for b₁, b₂ being Ordinal st ex r being non-zero Sequence of REAL ex y being strictly_decreasing uSurreal-Sequence st
( b₁ = dom r & dom r = dom y & Sum (r,y) == x ) & ex r being non-zero Sequence of REAL ex y being strictly_decreasing uSurreal-Sequence st
( b₂ = dom r & dom r = dom y & Sum (r,y) == x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def21 defines name-ord SURREALC:def 21 :
for x being surreal number
for b₂ being Ordinal holds
( b₂ = name-ord x iff ex r being non-zero Sequence of REAL ex y being strictly_decreasing uSurreal-Sequence st
( b₂ = dom r & dom r = dom y & Sum (r,y) == x ) );

theorem Th104: :: SURREALC:104

for r being non-zero Sequence of REAL
for y being strictly_decreasing uSurreal-Sequence
for x being Surreal st dom r = dom y & Sum (r,y) == x holds
name-ord x = dom r

proof end;

definition

let x be surreal number ;

func name-r x -> non-zero Sequence of REAL means :Def22: :: SURREALC:def 22
ex y being strictly_decreasing uSurreal-Sequence st
( dom y = dom it & Sum (it,y) == x );

existence
ex b₁ being non-zero Sequence of REAL ex y being strictly_decreasing uSurreal-Sequence st
( dom y = dom b₁ & Sum (b₁,y) == x )

proof end;

uniqueness
for b₁, b₂ being non-zero Sequence of REAL st ex y being strictly_decreasing uSurreal-Sequence st
( dom y = dom b₁ & Sum (b₁,y) == x ) & ex y being strictly_decreasing uSurreal-Sequence st
( dom y = dom b₂ & Sum (b₂,y) == x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def22 defines name-r SURREALC:def 22 :
for x being surreal number
for b₂ being non-zero Sequence of REAL holds
( b₂ = name-r x iff ex y being strictly_decreasing uSurreal-Sequence st
( dom y = dom b₂ & Sum (b₂,y) == x ) );

definition

let x be surreal number ;

func name-y x -> strictly_decreasing uSurreal-Sequence means :Def23: :: SURREALC:def 23
( dom (name-r x) = dom it & Sum ((name-r x),it) == x );

existence
ex b₁ being strictly_decreasing uSurreal-Sequence st
( dom (name-r x) = dom b₁ & Sum ((name-r x),b₁) == x )

proof end;

uniqueness
for b₁, b₂ being strictly_decreasing uSurreal-Sequence st dom (name-r x) = dom b₁ & Sum ((name-r x),b₁) == x & dom (name-r x) = dom b₂ & Sum ((name-r x),b₂) == x holds
b₁ = b₂

proof end;

end;

:: deftheorem Def23 defines name-y SURREALC:def 23 :
for x being surreal number
for b₂ being strictly_decreasing uSurreal-Sequence holds
( b₂ = name-y x iff ( dom (name-r x) = dom b₂ & Sum ((name-r x),b₂) == x ) );

theorem Th105: :: SURREALC:105

for x being Surreal holds
( dom (name-r x) = name-ord x & name-ord x = dom (name-y x) )

proof end;

theorem :: SURREALC:106

for x being Surreal holds name-r x, name-y x, name-ord x name_like x

proof end;