:: Conway's Games and Some of Their Basic Properties
:: by Robin Nittka
::
:: Received October 13, 2010
:: Copyright (c) 2010-2021 Association of Mizar Users


definition
attr c1 is strict ;
struct left-right -> ;
aggr left-right(# LeftOptions, RightOptions #) -> left-right ;
sel LeftOptions c1 -> set ;
sel RightOptions c1 -> set ;
end;

definition
func ConwayZero -> set equals :: CGAMES_1:def 1
 left-right(# {},{} #);
coherence
left-right(# {},{} #) is set by TARSKI:1;
end;

:: deftheorem defines ConwayZero CGAMES_1:def 1 :
ConwayZero = left-right(# {},{} #);

registration
cluster strict for left-right ;
existence
ex b1 being left-right st b1 is strict
proof end;
end;

deffunc H1( Sequence) -> set = { left-right(# x,y #) where x, y is Subset of (union (rng $1)) : verum } ;

defpred S1[ Sequence] means for beta being Ordinal st beta in dom $1 holds
$1 . beta = H1($1 | beta);

Lm1: for f being Sequence st S1[f] holds
for alpha being Ordinal holds S1[f | alpha]
proof end;

definition
let alpha be Ordinal;
func ConwayDay alpha -> set means :Def2: :: CGAMES_1:def 2
 ex f being Sequence st
( alpha in dom f & f . alpha = it & ( for beta being Ordinal st beta in dom f holds
f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) );
existence
ex b1 being set ex f being Sequence st
( alpha in dom f & f . alpha = b1 & ( for beta being Ordinal st beta in dom f holds
f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) )
proof end;
uniqueness
for b1, b2 being set st ex f being Sequence st
( alpha in dom f & f . alpha = b1 & ( for beta being Ordinal st beta in dom f holds
f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) ) & ex f being Sequence st
( alpha in dom f & f . alpha = b2 & ( for beta being Ordinal st beta in dom f holds
f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines ConwayDay CGAMES_1:def 2 :
for alpha being Ordinal
for b2 being set holds
( b2 = ConwayDay alpha iff ex f being Sequence st
( alpha in dom f & f . alpha = b2 & ( for beta being Ordinal st beta in dom f holds
f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) ) );

theorem Th1: :: CGAMES_1:1
for alpha being Ordinal
for z being object holds
( z in ConwayDay alpha iff ex w being strict left-right st
( z = w & ( for x being set st x in the LeftOptions of w \/ the RightOptions of w holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) ) ) )
proof end;

theorem Th2: :: CGAMES_1:2
ConwayDay 0 = {ConwayZero}
proof end;

theorem Th3: :: CGAMES_1:3
for alpha, beta being Ordinal st alpha c= beta holds
ConwayDay alpha c= ConwayDay beta
proof end;

registration
let alpha be Ordinal;
cluster ConwayDay alpha -> non empty ;
coherence
not ConwayDay alpha is empty
proof end;
end;

definition
let x be set ;
attr x is ConwayGame-like means :Def3: :: CGAMES_1:def 3
 ex alpha being Ordinal st x in ConwayDay alpha;
end;

:: deftheorem Def3 defines ConwayGame-like CGAMES_1:def 3 :
for x being set holds
( x is ConwayGame-like iff ex alpha being Ordinal st x in ConwayDay alpha );

registration
let alpha be Ordinal;
cluster -> ConwayGame-like for Element of ConwayDay alpha;
coherence
for b1 being Element of ConwayDay alpha holds b1 is ConwayGame-like ;
end;

registration
cluster ConwayZero -> ConwayGame-like ;
coherence
ConwayZero is ConwayGame-like
proof end;
end;

registration
cluster strict ConwayGame-like for left-right ;
existence
ex b1 being left-right st
( b1 is ConwayGame-like & b1 is strict )
proof end;
cluster ConwayGame-like for set ;
existence
ex b1 being set st b1 is ConwayGame-like
proof end;
end;

definition
mode ConwayGame is ConwayGame-like set ;
end;

definition
:: original: ConwayZero
redefine func ConwayZero -> Element of ConwayDay 0;
coherence
ConwayZero is Element of ConwayDay 0 by Th2, TARSKI:def 1;
end;

definition
func ConwayOne -> Element of ConwayDay 1 equals :: CGAMES_1:def 4
 left-right(# {ConwayZero},{} #);
coherence
left-right(# {ConwayZero},{} #) is Element of ConwayDay 1
proof end;
func ConwayStar -> Element of ConwayDay 1 equals :: CGAMES_1:def 5
 left-right(# {ConwayZero},{ConwayZero} #);
coherence
left-right(# {ConwayZero},{ConwayZero} #) is Element of ConwayDay 1
proof end;
end;

:: deftheorem defines ConwayOne CGAMES_1:def 4 :
ConwayOne = left-right(# {ConwayZero},{} #);

:: deftheorem defines ConwayStar CGAMES_1:def 5 :
ConwayStar = left-right(# {ConwayZero},{ConwayZero} #);

theorem Th4: :: CGAMES_1:4
for g being ConwayGame holds g is strict left-right
proof end;

registration
cluster ConwayGame-like -> strict for left-right ;
coherence
for b1 being left-right st b1 is ConwayGame-like holds
b1 is strict by Th4;
end;

definition
let g be ConwayGame;
func the_LeftOptions_of g -> set means :Def6: :: CGAMES_1:def 6
 ex w being left-right st
( g = w & it = the LeftOptions of w );
existence
ex b1 being set ex w being left-right st
( g = w & b1 = the LeftOptions of w )
proof end;
uniqueness
for b1, b2 being set st ex w being left-right st
( g = w & b1 = the LeftOptions of w ) & ex w being left-right st
( g = w & b2 = the LeftOptions of w ) holds
b1 = b2 ;
func the_RightOptions_of g -> set means :Def7: :: CGAMES_1:def 7
 ex w being left-right st
( g = w & it = the RightOptions of w );
existence
ex b1 being set ex w being left-right st
( g = w & b1 = the RightOptions of w )
proof end;
uniqueness
for b1, b2 being set st ex w being left-right st
( g = w & b1 = the RightOptions of w ) & ex w being left-right st
( g = w & b2 = the RightOptions of w ) holds
b1 = b2 ;
end;

:: deftheorem Def6 defines the_LeftOptions_of CGAMES_1:def 6 :
for g being ConwayGame
for b2 being set holds
( b2 = the_LeftOptions_of g iff ex w being left-right st
( g = w & b2 = the LeftOptions of w ) );

:: deftheorem Def7 defines the_RightOptions_of CGAMES_1:def 7 :
for g being ConwayGame
for b2 being set holds
( b2 = the_RightOptions_of g iff ex w being left-right st
( g = w & b2 = the RightOptions of w ) );

definition
let g be ConwayGame;
func the_Options_of g -> set equals :: CGAMES_1:def 8
(the_LeftOptions_of g) \/ (the_RightOptions_of g);
correctness
coherence
(the_LeftOptions_of g) \/ (the_RightOptions_of g) is set ;
;
end;

:: deftheorem defines the_Options_of CGAMES_1:def 8 :
for g being ConwayGame holds the_Options_of g = (the_LeftOptions_of g) \/ (the_RightOptions_of g);

theorem Th5: :: CGAMES_1:5
for g1, g2 being ConwayGame holds
( g1 = g2 iff ( the_LeftOptions_of g1 = the_LeftOptions_of g2 & the_RightOptions_of g1 = the_RightOptions_of g2 ) )
proof end;

registration
cluster the_LeftOptions_of ConwayZero -> empty ;
coherence
the_LeftOptions_of ConwayZero is empty by Def6;
cluster the_RightOptions_of ConwayZero -> empty ;
coherence
the_RightOptions_of ConwayZero is empty by Def7;
cluster the_RightOptions_of ConwayOne -> empty ;
coherence
the_RightOptions_of ConwayOne is empty by Def7;
end;

theorem Th6: :: CGAMES_1:6
for g being ConwayGame holds
( g = ConwayZero iff the_Options_of g = {} )
proof end;

theorem Th7: :: CGAMES_1:7
for x being set holds
( x in the_LeftOptions_of ConwayOne iff x = ConwayZero )
proof end;

theorem Th8: :: CGAMES_1:8
for x being set holds
( ( x in the_Options_of ConwayStar implies x = ConwayZero ) & ( x = ConwayZero implies x in the_Options_of ConwayStar ) & ( x in the_LeftOptions_of ConwayStar implies x = ConwayZero ) & ( x = ConwayZero implies x in the_LeftOptions_of ConwayStar ) & ( x in the_RightOptions_of ConwayStar implies x = ConwayZero ) & ( x = ConwayZero implies x in the_RightOptions_of ConwayStar ) )
proof end;

theorem Th9: :: CGAMES_1:9
for alpha being Ordinal
for g being ConwayGame holds
( g in ConwayDay alpha iff for x being set st x in the_Options_of g holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) )
proof end;

definition
let g be set ;
assume A1: g is ConwayGame ;
func ConwayRank g -> Ordinal means :Def9: :: CGAMES_1:def 9
( g in ConwayDay it & ( for beta being Ordinal st beta in it holds
not g in ConwayDay beta ) );
existence
ex b1 being Ordinal st
( g in ConwayDay b1 & ( for beta being Ordinal st beta in b1 holds
not g in ConwayDay beta ) )
proof end;
uniqueness
for b1, b2 being Ordinal st g in ConwayDay b1 & ( for beta being Ordinal st beta in b1 holds
not g in ConwayDay beta ) & g in ConwayDay b2 & ( for beta being Ordinal st beta in b2 holds
not g in ConwayDay beta ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines ConwayRank CGAMES_1:def 9 :
for g being set st g is ConwayGame holds
for b2 being Ordinal holds
( b2 = ConwayRank g iff ( g in ConwayDay b2 & ( for beta being Ordinal st beta in b2 holds
not g in ConwayDay beta ) ) );

theorem Th10: :: CGAMES_1:10
for x being set
for alpha being Ordinal
for g being ConwayGame st g in ConwayDay alpha & x in the_Options_of g holds
x in ConwayDay alpha
proof end;

theorem Th11: :: CGAMES_1:11
for x being set
for alpha being Ordinal
for g being ConwayGame st g in ConwayDay alpha & ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) holds
x in ConwayDay alpha
proof end;

theorem Th12: :: CGAMES_1:12
for alpha being Ordinal
for g being ConwayGame holds
( g in ConwayDay alpha iff ConwayRank g c= alpha )
proof end;

theorem Th13: :: CGAMES_1:13
for alpha being Ordinal
for g being ConwayGame holds
( ConwayRank g in alpha iff ex beta being Ordinal st
( beta in alpha & g in ConwayDay beta ) )
proof end;

theorem Th14: :: CGAMES_1:14
for g, gO being ConwayGame st gO in the_Options_of g holds
ConwayRank gO in ConwayRank g
proof end;

theorem :: CGAMES_1:15
for g, gO being ConwayGame st ( gO in the_LeftOptions_of g or gO in the_RightOptions_of g ) holds
ConwayRank gO in ConwayRank g
proof end;

theorem Th16: :: CGAMES_1:16
for g being ConwayGame holds not g in the_Options_of g
proof end;

theorem Th17: :: CGAMES_1:17
for x being set
for g being ConwayGame st x in the_Options_of g holds
x is ConwayGame-like left-right
proof end;

theorem Th18: :: CGAMES_1:18
for x being set
for g being ConwayGame st ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) holds
x is ConwayGame-like left-right
proof end;

theorem Th19: :: CGAMES_1:19
for w being strict left-right holds
( w is ConwayGame iff for z being set st z in the LeftOptions of w \/ the RightOptions of w holds
z is ConwayGame )
proof end;

scheme :: CGAMES_1:sch 1
ConwayGameMinTot{ P1[ ConwayGame] } :
ex g being ConwayGame st
( P1[g] & ( for g1 being ConwayGame st ConwayRank g1 in ConwayRank g holds
not P1[g1] ) )
provided
A1: ex g being ConwayGame st P1[g]
proof end;

scheme :: CGAMES_1:sch 2
ConwayGameMin{ P1[ ConwayGame] } :
ex g being ConwayGame st
( P1[g] & ( for gO being ConwayGame st gO in the_Options_of g holds
not P1[gO] ) )
provided
A1: ex g being ConwayGame st P1[g]
proof end;

scheme :: CGAMES_1:sch 3
ConwayGameInd{ P1[ ConwayGame] } :
for g being ConwayGame holds P1[g]
provided
A1: for g being ConwayGame st ( for gO being ConwayGame st gO in the_Options_of g holds
P1[gO] ) holds
P1[g]
proof end;

definition
let f be Function;
attr f is ConwayGame-valued means :Def10: :: CGAMES_1:def 10
 for x being set st x in dom f holds
f . x is ConwayGame;
end;

:: deftheorem Def10 defines ConwayGame-valued CGAMES_1:def 10 :
for f being Function holds
( f is ConwayGame-valued iff for x being set st x in dom f holds
f . x is ConwayGame );

registration
let g be ConwayGame;
cluster <*g*> -> ConwayGame-valued ;
coherence
<*g*> is ConwayGame-valued
proof end;
end;

registration
cluster Relation-like omega -defined Function-like non empty V41() FinSequence-like FinSubsequence-like ConwayGame-valued for set ;
existence
ex b1 being FinSequence st
( b1 is ConwayGame-valued & not b1 is empty )
proof end;
end;

registration
let f be non empty FinSequence;
cluster -> natural non empty for Element of dom f;
coherence
for b1 being Element of dom f holds
( b1 is natural & not b1 is empty ) by FINSEQ_3:24;
end;

registration
let f be non empty ConwayGame-valued Function;
let x be Element of dom f;
cluster f . x -> ConwayGame-like ;
coherence
f . x is ConwayGame-like by Def10;
end;

definition
let f be non empty ConwayGame-valued FinSequence;
attr f is ConwayGameChain-like means :Def11: :: CGAMES_1:def 11
 for n being Element of dom f st n > 1 holds
f . (n - 1) in the_Options_of (f . n);
end;

:: deftheorem Def11 defines ConwayGameChain-like CGAMES_1:def 11 :
for f being non empty ConwayGame-valued FinSequence holds
( f is ConwayGameChain-like iff for n being Element of dom f st n > 1 holds
f . (n - 1) in the_Options_of (f . n) );

theorem Th20: :: CGAMES_1:20
for f being FinSequence
for n being Nat st n in dom f & n > 1 holds
n - 1 in dom f
proof end;

registration
let g be ConwayGame;
cluster <*g*> -> ConwayGameChain-like ;
coherence
<*g*> is ConwayGameChain-like
proof end;
end;

registration
cluster Relation-like omega -defined Function-like non empty V41() FinSequence-like FinSubsequence-like ConwayGame-valued ConwayGameChain-like for set ;
existence
ex b1 being non empty ConwayGame-valued FinSequence st b1 is ConwayGameChain-like
proof end;
end;

definition
mode ConwayGameChain is non empty ConwayGame-valued ConwayGameChain-like FinSequence;
end;

theorem Th21: :: CGAMES_1:21
for f being ConwayGameChain
for n, m being Element of dom f st n < m holds
ConwayRank (f . n) in ConwayRank (f . m)
proof end;

theorem Th22: :: CGAMES_1:22
for f being ConwayGameChain
for n, m being Element of dom f st n <= m holds
ConwayRank (f . n) c= ConwayRank (f . m)
proof end;

theorem Th23: :: CGAMES_1:23
for alpha being Ordinal
for f being ConwayGameChain st f . (len f) in ConwayDay alpha holds
f . 1 in ConwayDay alpha
proof end;

Lm2: for g being ConwayGame ex f being ConwayGameChain st
( f . 1 = g & f . (len f) = g )
proof end;

definition
let g be ConwayGame;
func the_Tree_of g -> set means :Def12: :: CGAMES_1:def 12
 for z being set holds
( z in it iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) );
existence
ex b1 being set st
for z being set holds
( z in b1 iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) )
proof end;
uniqueness
for b1, b2 being set st ( for z being set holds
( z in b1 iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) ) ) & ( for z being set holds
( z in b2 iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines the_Tree_of CGAMES_1:def 12 :
for g being ConwayGame
for b2 being set holds
( b2 = the_Tree_of g iff for z being set holds
( z in b2 iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) ) );

registration
let g be ConwayGame;
cluster the_Tree_of g -> non empty ;
coherence
not the_Tree_of g is empty
proof end;
end;

definition
let g be ConwayGame;
func the_proper_Tree_of g -> Subset of (the_Tree_of g) equals :: CGAMES_1:def 13
(the_Tree_of g) \ {g};
coherence
(the_Tree_of g) \ {g} is Subset of (the_Tree_of g) ;
end;

:: deftheorem defines the_proper_Tree_of CGAMES_1:def 13 :
for g being ConwayGame holds the_proper_Tree_of g = (the_Tree_of g) \ {g};

theorem Th24: :: CGAMES_1:24
for g being ConwayGame holds g in the_Tree_of g
proof end;

definition
let alpha be Ordinal;
let g be Element of ConwayDay alpha;
:: original: the_Tree_of
redefine func the_Tree_of g -> Subset of (ConwayDay alpha);
coherence
the_Tree_of g is Subset of (ConwayDay alpha)
proof end;
end;

registration
let g be ConwayGame;
cluster -> ConwayGame-like for Element of the_Tree_of g;
coherence
for b1 being Element of the_Tree_of g holds b1 is ConwayGame-like
proof end;
end;

theorem Th25: :: CGAMES_1:25
for f being ConwayGameChain
for n being non zero Nat holds f | n is ConwayGameChain
proof end;

theorem Th26: :: CGAMES_1:26
for f1, f2 being ConwayGameChain st ex g being ConwayGame st
( g = f2 . 1 & f1 . (len f1) in the_Options_of g ) holds
f1 ^ f2 is ConwayGameChain
proof end;

theorem Th27: :: CGAMES_1:27
for x being set
for g being ConwayGame holds
( x in the_Tree_of g iff ( x = g or ex gO being ConwayGame st
( gO in the_Options_of g & x in the_Tree_of gO ) ) )
proof end;

theorem Th28: :: CGAMES_1:28
for g, gO being ConwayGame holds
( not gO in the_Tree_of g or gO = g or ConwayRank gO in ConwayRank g )
proof end;

theorem Th29: :: CGAMES_1:29
for g, gO being ConwayGame st gO in the_Tree_of g holds
ConwayRank gO c= ConwayRank g
proof end;

theorem :: CGAMES_1:30
for g being ConwayGame
for s being set st g in s & ( for g1 being ConwayGame st g1 in s holds
the_Options_of g1 c= s ) holds
the_Tree_of g c= s
proof end;

theorem Th31: :: CGAMES_1:31
for g1, g2 being ConwayGame st g1 in the_Tree_of g2 holds
the_Tree_of g1 c= the_Tree_of g2
proof end;

theorem Th32: :: CGAMES_1:32
for g1, g2 being ConwayGame st g1 in the_Tree_of g2 holds
the_proper_Tree_of g1 c= the_proper_Tree_of g2
proof end;

theorem Th33: :: CGAMES_1:33
for g being ConwayGame holds the_Options_of g c= the_proper_Tree_of g
proof end;

theorem Th34: :: CGAMES_1:34
for g being ConwayGame holds the_Options_of g c= the_Tree_of g
proof end;

theorem Th35: :: CGAMES_1:35
for g1, g2 being ConwayGame st g1 in the_proper_Tree_of g2 holds
the_Tree_of g1 c= the_proper_Tree_of g2
proof end;

theorem :: CGAMES_1:36
for g, gO being ConwayGame st gO in the_Options_of g holds
the_Tree_of gO c= the_proper_Tree_of g
proof end;

theorem :: CGAMES_1:37
the_Tree_of ConwayZero = {ConwayZero} by Th2, ZFMISC_1:33;

theorem :: CGAMES_1:38
for g being ConwayGame holds ConwayZero in the_Tree_of g
proof end;

scheme :: CGAMES_1:sch 4
ConwayGameMin2{ P1[ ConwayGame] } :
ex g being ConwayGame st
( P1[g] & ( for gO being ConwayGame st gO in the_proper_Tree_of g holds
not P1[gO] ) )
provided
A1: ex g being ConwayGame st P1[g]
proof end;

scheme :: CGAMES_1:sch 5
Func1RecUniq{ F1( ConwayGame, Function) -> set } :
for g being ConwayGame
for f1, f2 being Function st dom f1 = the_Tree_of g & dom f2 = the_Tree_of g & ( for g1 being ConwayGame st g1 in dom f1 holds
f1 . g1 = F1(g1,(f1 | (the_proper_Tree_of g1))) ) & ( for g1 being ConwayGame st g1 in dom f2 holds
f2 . g1 = F1(g1,(f2 | (the_proper_Tree_of g1))) ) holds
f1 = f2
proof end;

scheme :: CGAMES_1:sch 6
Func1RecEx{ F1( ConwayGame, Function) -> set } :
for g being ConwayGame ex f being Function st
( dom f = the_Tree_of g & ( for g1 being ConwayGame st g1 in dom f holds
f . g1 = F1(g1,(f | (the_proper_Tree_of g1))) ) )
proof end;

Lm3: for g1 being ConwayGame
for f being Function holds
( { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } = { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } & { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } = { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } )
proof end;

definition
let g be ConwayGame;
func - g -> set means :Def14: :: CGAMES_1:def 14
 ex f being Function st
( dom f = the_Tree_of g & it = f . g & ( for g1 being ConwayGame st g1 in dom f holds
f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) );
existence
ex b1 being set ex f being Function st
( dom f = the_Tree_of g & b1 = f . g & ( for g1 being ConwayGame st g1 in dom f holds
f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) )
proof end;
uniqueness
for b1, b2 being set st ex f being Function st
( dom f = the_Tree_of g & b1 = f . g & ( for g1 being ConwayGame st g1 in dom f holds
f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) ) & ex f being Function st
( dom f = the_Tree_of g & b2 = f . g & ( for g1 being ConwayGame st g1 in dom f holds
f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines - CGAMES_1:def 14 :
for g being ConwayGame
for b2 being set holds
( b2 = - g iff ex f being Function st
( dom f = the_Tree_of g & b2 = f . g & ( for g1 being ConwayGame st g1 in dom f holds
f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) ) );

registration
let g be ConwayGame;
cluster - g -> ConwayGame-like ;
coherence
- g is ConwayGame-like
proof end;
end;

Lm4: for g being ConwayGame
for f being Function st dom f = the_Tree_of g & ( for g1 being ConwayGame st g1 in dom f holds
f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) holds
for g1 being ConwayGame st g1 in dom f holds
f . g1 = - g1
proof end;

theorem Th39: :: CGAMES_1:39
for g being ConwayGame holds
( ( for x being set holds
( x in the_LeftOptions_of (- g) iff ex gR being ConwayGame st
( gR in the_RightOptions_of g & x = - gR ) ) ) & ( for x being set holds
( x in the_RightOptions_of (- g) iff ex gL being ConwayGame st
( gL in the_LeftOptions_of g & x = - gL ) ) ) )
proof end;

theorem Th40: :: CGAMES_1:40
for g being ConwayGame holds - (- g) = g
proof end;

theorem :: CGAMES_1:41
for g, gO being ConwayGame holds
( ( gO in the_LeftOptions_of (- g) implies - gO in the_RightOptions_of g ) & ( - gO in the_RightOptions_of g implies gO in the_LeftOptions_of (- g) ) & ( gO in the_LeftOptions_of g implies - gO in the_RightOptions_of (- g) ) & ( - gO in the_RightOptions_of (- g) implies gO in the_LeftOptions_of g ) & ( gO in the_RightOptions_of (- g) implies - gO in the_LeftOptions_of g ) & ( - gO in the_LeftOptions_of g implies gO in the_RightOptions_of (- g) ) & ( gO in the_RightOptions_of g implies - gO in the_LeftOptions_of (- g) ) & ( - gO in the_LeftOptions_of (- g) implies gO in the_RightOptions_of g ) )
proof end;

definition
let g be ConwayGame;
attr g is nonnegative means :: CGAMES_1:def 15
 ex s being set st
( g in s & ( for g1 being ConwayGame st g1 in s holds
for gR being ConwayGame st gR in the_RightOptions_of g1 holds
ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL in s ) ) );
end;

:: deftheorem defines nonnegative CGAMES_1:def 15 :
for g being ConwayGame holds
( g is nonnegative iff ex s being set st
( g in s & ( for g1 being ConwayGame st g1 in s holds
for gR being ConwayGame st gR in the_RightOptions_of g1 holds
ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL in s ) ) ) );

definition
let g be ConwayGame;
attr g is nonpositive means :Def16: :: CGAMES_1:def 16
 - g is nonnegative ;
end;

:: deftheorem Def16 defines nonpositive CGAMES_1:def 16 :
for g being ConwayGame holds
( g is nonpositive iff - g is nonnegative );

definition
let g be ConwayGame;
attr g is zero means :: CGAMES_1:def 17
( g is nonnegative & g is nonpositive );
attr g is fuzzy means :: CGAMES_1:def 18
( not g is nonnegative & not g is nonpositive );
end;

:: deftheorem defines zero CGAMES_1:def 17 :
for g being ConwayGame holds
( g is zero iff ( g is nonnegative & g is nonpositive ) );

:: deftheorem defines fuzzy CGAMES_1:def 18 :
for g being ConwayGame holds
( g is fuzzy iff ( not g is nonnegative & not g is nonpositive ) );

definition
let g be ConwayGame;
attr g is positive means :: CGAMES_1:def 19
( g is nonnegative & not g is zero );
attr g is negative means :: CGAMES_1:def 20
( g is nonpositive & not g is zero );
end;

:: deftheorem defines positive CGAMES_1:def 19 :
for g being ConwayGame holds
( g is positive iff ( g is nonnegative & not g is zero ) );

:: deftheorem defines negative CGAMES_1:def 20 :
for g being ConwayGame holds
( g is negative iff ( g is nonpositive & not g is zero ) );

registration
cluster ConwayGame-like zero -> nonnegative nonpositive for set ;
coherence
for b1 being ConwayGame st b1 is zero holds
( b1 is nonnegative & b1 is nonpositive ) ;
cluster ConwayGame-like nonnegative nonpositive -> zero for set ;
coherence
for b1 being ConwayGame st b1 is nonpositive & b1 is nonnegative holds
b1 is zero ;
cluster ConwayGame-like negative -> nonpositive non zero for set ;
coherence
for b1 being ConwayGame st b1 is negative holds
( b1 is nonpositive & not b1 is zero ) ;
cluster ConwayGame-like nonpositive non zero -> negative for set ;
coherence
for b1 being ConwayGame st b1 is nonpositive & not b1 is zero holds
b1 is negative ;
cluster ConwayGame-like positive -> nonnegative non zero for set ;
coherence
for b1 being ConwayGame st b1 is positive holds
( b1 is nonnegative & not b1 is zero ) ;
cluster ConwayGame-like nonnegative non zero -> positive for set ;
coherence
for b1 being ConwayGame st b1 is nonnegative & not b1 is zero holds
b1 is positive ;
cluster ConwayGame-like fuzzy -> non nonnegative non nonpositive for set ;
coherence
for b1 being ConwayGame st b1 is fuzzy holds
( not b1 is nonnegative & not b1 is nonpositive ) ;
cluster ConwayGame-like non nonnegative non nonpositive -> fuzzy for set ;
coherence
for b1 being ConwayGame st not b1 is nonnegative & not b1 is nonpositive holds
b1 is fuzzy ;
end;

theorem :: CGAMES_1:42
for g being ConwayGame holds
( g is zero or g is positive or g is negative or g is fuzzy ) ;

theorem Th43: :: CGAMES_1:43
for g being ConwayGame holds
( g is nonnegative iff for gR being ConwayGame st gR in the_RightOptions_of g holds
ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL is nonnegative ) )
proof end;

theorem Th44: :: CGAMES_1:44
for g being ConwayGame holds
( g is nonpositive iff for gL being ConwayGame st gL in the_LeftOptions_of g holds
ex gLR being ConwayGame st
( gLR in the_RightOptions_of gL & gLR is nonpositive ) )
proof end;

theorem Th45: :: CGAMES_1:45
for g being ConwayGame holds
( ( g is nonnegative implies for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) & ( ( for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) implies g is nonnegative ) & ( g is nonpositive implies for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) implies g is nonpositive ) )
proof end;

theorem Th46: :: CGAMES_1:46
for g being ConwayGame holds
( g is fuzzy iff ( ex gL being ConwayGame st
( gL in the_LeftOptions_of g & gL is nonnegative ) & ex gR being ConwayGame st
( gR in the_RightOptions_of g & gR is nonpositive ) ) )
proof end;

theorem Th47: :: CGAMES_1:47
for g being ConwayGame holds
( g is zero iff ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ( for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) ) ) by Th45;

theorem Th48: :: CGAMES_1:48
for g being ConwayGame holds
( g is positive iff ( ( for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) & ex gL being ConwayGame st
( gL in the_LeftOptions_of g & gL is nonnegative ) ) )
proof end;

theorem :: CGAMES_1:49
for g being ConwayGame holds
( g is negative iff ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ex gR being ConwayGame st
( gR in the_RightOptions_of g & gR is nonpositive ) ) )
proof end;

registration
cluster ConwayZero -> zero ;
coherence
ConwayZero is zero
proof end;
end;

registration
cluster ConwayOne -> positive ;
coherence
ConwayOne is positive
proof end;
cluster ConwayStar -> fuzzy ;
coherence
ConwayStar is fuzzy
proof end;
end;

registration
cluster ConwayGame-like zero for set ;
existence
ex b1 being ConwayGame st b1 is zero
proof end;
cluster ConwayGame-like positive for set ;
existence
ex b1 being ConwayGame st b1 is positive
proof end;
cluster ConwayGame-like fuzzy for set ;
existence
ex b1 being ConwayGame st b1 is fuzzy
proof end;
end;

registration
let g be nonpositive ConwayGame;
cluster - g -> nonnegative ;
coherence
- g is nonnegative by Def16;
end;

registration
let g be nonnegative ConwayGame;
cluster - g -> nonpositive ;
coherence
- g is nonpositive by Th40;
end;

registration
let g be positive ConwayGame;
cluster - g -> negative ;
coherence
- g is negative
proof end;
end;

registration
cluster ConwayGame-like negative for set ;
existence
ex b1 being ConwayGame st b1 is negative
proof end;
end;

registration
let g be negative ConwayGame;
cluster - g -> positive ;
coherence
- g is positive
proof end;
end;

registration
let g be fuzzy ConwayGame;
cluster - g -> fuzzy ;
coherence
- g is fuzzy
proof end;
end;