SURREALO: Integration of Game Theoretic and Tree Theoretic Approaches to {C}onway Numbers

Preorder of Surreal Numbers - Reflexivity, Conway Ch.1 Th.0(iii)

proof end;

end;

:: deftheorem defines 1_No SURREALO:def 1 :

theorem Th1: :: SURREALO:1

for x, y being Surreal st y in (L_ x) \/ (R_ x) holds
born y in born x

proof end;

theorem :: SURREALO:2

for x being Surreal holds
( L_ x <> {x} & {x} <> R_ x )

proof end;

theorem Th3: :: SURREALO:3

for x being Surreal holds x <= x

proof end;

Preorder of Surreal Numbers - Transitivity, Conway Ch.1 Th.1

theorem Th4: :: SURREALO:4

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

proof end;

theorem Th5: :: SURREALO:5

for x being Surreal holds
( L_ x <<= {x} & {x} <<= R_ x )

proof end;

Preorder of Surreal Numbers - Total, Conway Ch.1 Th.2(ii)

theorem Th6: :: SURREALO:6

for x, y being Surreal st not y <= x holds
x <= y

proof end;

theorem Th7: :: SURREALO:7

for A being Ordinal st A is finite holds
Day A is finite

proof end;

theorem :: SURREALO:8

for x being Surreal st born x is finite holds
( L_ x is finite & R_ x is finite )

proof end;

definition

let x, y be Surreal;
:: original: >=
redefine pred x <= y;
reflexivity by Th3;
connectedness by Th6;

end;

notation

let x, y be Surreal;
synonym y >= x for x <= y;

end;

notation

let x, y be Surreal;
antonym y < x for x <= y;
antonym x > y for x <= y;

end;

definition

let x, y be Surreal;

pred x == y means :: SURREALO:def 2
( x <= y & y <= x );

reflexivity ;
symmetry ;

end;

:: deftheorem defines == SURREALO:def 2 :

theorem :: SURREALO:9

for x, y, z being Surreal st x <= y & y < z holds
x < z by Th4;

theorem :: SURREALO:10

for x, y, z being Surreal st x == y & y == z holds
x == z by Th4;

Conway Ch.1 Th.2(i)

theorem Th11: :: SURREALO:11

for x being Surreal holds
( L_ x << {x} & {x} << R_ x )

proof end;

theorem Th12: :: SURREALO:12

for S being non empty surreal-membered set st S is finite holds
ex Min, Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) )

proof end;

theorem Th13: :: SURREALO:13

for x, y being Surreal holds
( not x < y or ex xR being Surreal st
( xR in R_ x & x < xR & xR <= y ) or ex yL being Surreal st
( yL in L_ y & x <= yL & yL < y ) )

proof end;

theorem Th14: :: SURREALO:14

for x, y being Surreal st L_ y << {x} & {x} << R_ y holds
[((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] is Surreal

proof end;

theorem Th15: :: SURREALO:15

for x, y, z being Surreal st L_ y << {x} & {x} << R_ y & z = [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] holds
x == z

proof end;

The Simplicity Theorem for Surreal Numbers

theorem Th16: :: SURREALO:16

for x, y being Surreal st L_ y << {x} & {x} << R_ y & ( for z being Surreal st L_ y << {z} & {z} << R_ y holds
born x c= born z ) holds
x == y

proof end;

theorem Th17: :: SURREALO:17

for X being set
for x, y being Surreal st X << {x} & x <= y holds
X << {y}

proof end;

theorem Th18: :: SURREALO:18

for X being set
for x, y being Surreal st {x} << X & y <= x holds
{y} << X

proof end;

theorem :: SURREALO:19

for x, y being Surreal st x == y holds
[((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] is Surreal

proof end;

theorem :: SURREALO:20

for x, y, z being Surreal st x == y & z = [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] holds
x == z

proof end;

theorem Th21: :: SURREALO:21

for x, y being Surreal holds
( {x} << {y} iff x < y )

proof end;

theorem :: SURREALO:22

for x, y being Surreal holds
( [{x},{y}] is Surreal iff x < y )

proof end;

theorem Th23: :: SURREALO:23

for x, Max being Surreal st ( for y being Surreal st y in L_ x holds
y <= Max ) & Max in L_ x holds
( [{Max},(R_ x)] is Surreal & ( for y being Surreal st y = [{Max},(R_ x)] holds
( y == x & born y c= born x ) ) )

proof end;

theorem Th24: :: SURREALO:24

for x, Min being Surreal st ( for y being Surreal st y in R_ x holds
Min <= y ) & Min in R_ x holds
( [(L_ x),{Min}] is Surreal & ( for y being Surreal st y = [(L_ x),{Min}] holds
( y == x & born y c= born x ) ) )

proof end;

theorem :: SURREALO:25

for X being set
for x, y, z, t being Surreal st x <= y & z = [{x,y},X] & t = [{y},X] holds
z == t

proof end;

theorem :: SURREALO:26

for X being set
for x, y, z being Surreal st z = [{x,y},X] holds
[{x},X] is Surreal

proof end;

theorem :: SURREALO:27

for X being set
for x, y, z, t being Surreal st x <= y & z = [X,{x,y}] & t = [X,{x}] holds
z == t

proof end;

theorem :: SURREALO:28

for X being set
for x, y, z being Surreal st z = [X,{x,y}] holds
[X,{x}] is Surreal

proof end;

definition

let X, Y be set ;

pred X <=_ Y means :Def3: :: SURREALO:def 3
for x being Surreal st x in X holds
ex y1, y2 being Surreal st
( y1 in Y & y2 in Y & y1 <= x & x <= y2 );

reflexivity ;

end;

:: deftheorem Def3 defines <=_ SURREALO:def 3 :

definition

let X, Y be set ;

pred X <==> Y means :: SURREALO:def 4
( X <=_ Y & Y <=_ X );

reflexivity ;
symmetry ;

end;

:: deftheorem defines <==> SURREALO:def 4 :

theorem Th29: :: SURREALO:29

for x, y being Surreal
for X1, X2, Y1, Y2 being set st X1 <==> X2 & Y1 <==> Y2 & x = [X1,Y1] & y = [X2,Y2] holds
x == y

proof end;

theorem :: SURREALO:30

for X, Y being set st X c= Y holds
X <=_ Y ;

theorem :: SURREALO:31

for X1, X2, Y1, Y2 being set st X1 <=_ X2 & Y1 <=_ Y2 holds
X1 \/ Y1 <=_ X2 \/ Y2

proof end;

theorem :: SURREALO:32

for x, y being Surreal st x == y holds
{x} <=_ {y}

proof end;

definition

let x be Surreal;

func born_eq x -> Ordinal means :Def5: :: SURREALO:def 5
( ex y being Surreal st
( born y = it & y == x ) & ( for y being Surreal st y == x holds
it c= born y ) );

proof end;

proof end;

end;

:: deftheorem Def5 defines born_eq SURREALO:def 5 :

definition

let x be Surreal;

func born_eq_set x -> surreal-membered set means :Def6: :: SURREALO:def 6
for y being Surreal holds
( y in it iff ( y == x & y in Day (born_eq x) ) );

proof end;

proof end;

end;

:: deftheorem Def6 defines born_eq_set SURREALO:def 6 :

registration

let x be Surreal;

cluster born_eq_set x -> non empty surreal-membered ;

proof end;

end;

definition

let A be non empty surreal-membered set ;
let x be Surreal;

attr x is A -smallest means :Def7: :: SURREALO:def 7
( x in A & ( for y being Surreal st y in A & y == x holds
(card (L_ x)) (+) (card (R_ x)) c= (card (L_ y)) (+) (card (R_ y)) ) );

end;

:: deftheorem Def7 defines -smallest SURREALO:def 7 :

registration

let A be non empty surreal-membered set ;

cluster non empty pair surreal A -smallest for set ;

proof end;

end;

theorem Th33: :: SURREALO:33

for x, y being Surreal st x == y holds
born_eq x = born_eq y

proof end;

Lm1: for x, y being Surreal st x == y holds
born_eq_set x c= born_eq_set y

proof end;

theorem Th34: :: SURREALO:34

for x, y being Surreal st x == y holds
born_eq_set x = born_eq_set y

proof end;

theorem :: SURREALO:35

for x, y being Surreal st y in born_eq_set x holds
( born y = born_eq y & born_eq y = born_eq x )

proof end;

theorem :: SURREALO:36

for A being Ordinal holds
( [{},(Day A)] in (Day (succ A)) \ (Day A) & [(Day A),{}] in (Day (succ A)) \ (Day A) )

proof end;

definition

let A be set ;

func made_of A -> surreal-membered set means :Def8: :: SURREALO:def 8
for o being object holds
( o in it iff ( o is surreal & (L_ o) \/ (R_ o) c= A ) );

proof end;

proof end;

end;

:: deftheorem Def8 defines made_of SURREALO:def 8 :

definition

let A be Ordinal;

func unique_No_op A -> Sequence means :Def9: :: SURREALO:def 9
( dom it = succ A & ( for B being Ordinal st B in succ A holds
( it . B c= Day B & ( for x being Surreal holds
( x in it . B iff ( x in union (rng (it | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (it | B)))) & x = the b₃ -smallest Surreal ) ) ) ) ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def9 defines unique_No_op SURREALO:def 9 :

registration

let A be Ordinal;
let o be object ;

cluster (unique_No_op A) . o -> surreal-membered ;

proof end;

end;

theorem Th37: :: SURREALO:37

for A, B being Ordinal st A c= B holds
(unique_No_op B) | (succ A) = unique_No_op A

proof end;

theorem Th38: :: SURREALO:38

for A, B being Ordinal
for x being Surreal st x in (unique_No_op A) . B holds
( born_eq x = born x & born x c= B & x in (unique_No_op A) . (born x) & not x in union (rng ((unique_No_op A) | (born x))) )

proof end;

theorem Th39: :: SURREALO:39

for A, B, O being Ordinal st O c= A & A c= B holds
(unique_No_op A) . O = (unique_No_op B) . O

proof end;

theorem :: SURREALO:40

for A, B, C being Ordinal st A c= B & B in succ C holds
(unique_No_op C) . A c= (unique_No_op C) . B

proof end;

definition

let x be Surreal;

func Unique_No x -> Surreal means :Def10: :: SURREALO:def 10
( it == x & it in (unique_No_op (born_eq x)) . (born_eq x) );

proof end;

proof end;

end;

:: deftheorem Def10 defines Unique_No SURREALO:def 10 :

theorem Th41: :: SURREALO:41

for x, y being Surreal st x == y holds
Unique_No x = Unique_No y

proof end;

theorem Th42: :: SURREALO:42

0_No = Unique_No 0_No

proof end;

definition

let x be Surreal;

attr x is uniq-surreal means :Def11: :: SURREALO:def 11
x = Unique_No x;

end;

:: deftheorem Def11 defines uniq-surreal SURREALO:def 11 :

registration

cluster 0_No -> uniq-surreal ;

coherence by Th42;

cluster non empty pair surreal uniq-surreal for set ;

existence by Th42;

end;

definition

mode uSurreal is uniq-surreal Surreal;

end;

theorem Th43: :: SURREALO:43

for o being object
for x being Surreal st x is uSurreal & o in (L_ x) \/ (R_ x) holds
o is uSurreal

proof end;

theorem :: SURREALO:44

for x being Surreal st not L_ x is empty & L_ x is finite & x is uSurreal holds
card (L_ x) = 1

proof end;

theorem :: SURREALO:45

for x being Surreal st not R_ x is empty & R_ x is finite & x is uSurreal holds
card (R_ x) = 1

proof end;

theorem :: SURREALO:46

for x being Surreal holds
( (card (L_ x)) (+) (card (R_ x)) = 0 iff x = 0_No )

proof end;

theorem :: SURREALO:47

for x being Surreal holds
( (card (L_ x)) (+) (card (R_ x)) = 1 iff ex y being Surreal st
( x = [{},{y}] or x = [{y},{}] ) )

proof end;

definition

let X be set ;

attr X is uniq-surreal-membered means :Def12: :: SURREALO:def 12
for o being object st o in X holds
o is uSurreal;

end;

:: deftheorem Def12 defines uniq-surreal-membered SURREALO:def 12 :

registration

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

coherence ;
let x be uSurreal;

cluster (L_ x) \/ (R_ x) -> uniq-surreal-membered ;

coherence by Th43;

cluster {x} -> uniq-surreal-membered ;

coherence by TARSKI:def 1;

end;

registration

let X, Y be uniq-surreal-membered set ;

cluster X \/ Y -> uniq-surreal-membered ;

proof end;

end;

registration

let x be Surreal;

cluster Unique_No x -> uniq-surreal ;