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


begin

definition
attrc1 is strict ;
struct left-right  -> ;
aggrleft-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 ;
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
proofend;
end;

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

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

Lm1:  for f being T-Sequence st S1[f] holds
for alpha being Ordinal holds S1[f | alpha]
proofend;

definition
let alpha be Ordinal;
func ConwayDay alpha ->  set  means :Def2: :: CGAMES_1:def 2
 ex f being T-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 T-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  }  ) )
proofend;
uniqueness
 for b1, b2 being set st ex f being T-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 T-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
proofend;
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 T-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 z being set
for alpha being Ordinal 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 ) ) ) )
proofend;

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

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

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

begin

definition
let x be set ;
attrx 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
proofend;
end;

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

registration
cluster strict ConwayGame-like for left-right ;
existence
 ex b1 being left-right st
( b1 is ConwayGame-like & b1 is strict )
proofend;
cluster ConwayGame-like for set ;
existence
 ex b1 being set st b1 is ConwayGame-like
proofend;
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
proofend;
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
proofend;
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
proofend;

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 )
proofend;
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 )
proofend;
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 ) )
proofend;

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 = {} )
proofend;

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

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 ) )
proofend;

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 ) )
proofend;

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 ) )
proofend;
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
proofend;
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
proofend;

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
proofend;

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

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 ) )
proofend;

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

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

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

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
proofend;

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
proofend;

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 )
proofend;

begin

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]
proofend;

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]
proofend;

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]
proofend;

begin

definition
let f be Function;
attrf 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
proofend;
end;

registration
cluster Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like ConwayGame-valued for set ;
existence
 ex b1 being FinSequence st
( b1 is ConwayGame-valued &amp; not b1 is empty )
proofend;
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 &amp; 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;
clusterf . x ->  ConwayGame-like ;
coherence
 f . x is ConwayGame-like by Def10;
end;

definition
let f be non empty ConwayGame-valued FinSequence;
attrf 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 &amp; n > 1 holds
n - 1 in dom f
proofend;

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

registration
cluster Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like ConwayGame-valued ConwayGameChain-like for set ;
existence
 ex b1 being non empty ConwayGame-valued FinSequence st b1 is ConwayGameChain-like
proofend;
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)
proofend;

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)
proofend;

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
proofend;

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

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 &amp; 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 &amp; f . (len f) = g ) )
proofend;
uniqueness
 for b1, b2 being set st ( for z being set holds
( z in b1 iff ex f being ConwayGameChain st
( f . 1 = z &amp; f . (len f) = g ) ) ) &amp; ( for z being set holds
( z in b2 iff ex f being ConwayGameChain st
( f . 1 = z &amp; f . (len f) = g ) ) ) holds
b1 = b2
proofend;
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 &amp; f . (len f) = g ) ) );

registration
let g be ConwayGame;
cluster the_Tree_of g ->  non empty ;
coherence
 not the_Tree_of g is empty
proofend;
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
proofend;

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)
proofend;
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
proofend;
end;

theorem Th25: :: CGAMES_1:25
for f being ConwayGameChain
for n being non empty Nat holds f | n is ConwayGameChain
proofend;

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

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 &amp; x in the_Tree_of gO ) ) )
proofend;

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

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

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

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
proofend;

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
proofend;

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

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

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
proofend;

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

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
proofend;

scheme :: CGAMES_1:sch 4
ConwayGameMin2{ P1[ ConwayGame] } :
 ex g being ConwayGame st
( P1[g] &amp; ( 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]
proofend;

begin

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 &amp; dom f2 = the_Tree_of g &amp; ( for g1 being ConwayGame st g1 in dom f1 holds
f1 . g1 = F1(g1,(f1 | (the_proper_Tree_of g1))) ) &amp; ( for g1 being ConwayGame st g1 in dom f2 holds
f2 . g1 = F1(g1,(f2 | (the_proper_Tree_of g1))) ) holds
f1 = f2
proofend;

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 &amp; ( for g1 being ConwayGame st g1 in dom f holds
f . g1 = F1(g1,(f | (the_proper_Tree_of g1))) ) )
proofend;

begin

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 <> {}  }  &amp;  {  ((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 <> {}  }  )
proofend;

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 &amp; it = f . g &amp; ( 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 &amp; b1 = f . g &amp; ( 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 <> {}  }  #) ) )
proofend;
uniqueness
 for b1, b2 being set st ex f being Function st
( dom f = the_Tree_of g &amp; b1 = f . g &amp; ( 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 <> {}  }  #) ) ) &amp; ex f being Function st
( dom f = the_Tree_of g &amp; b2 = f . g &amp; ( 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
proofend;
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 &amp; b2 = f . g &amp; ( 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
proofend;
end;

Lm4:  for g being ConwayGame
for f being Function st dom f = the_Tree_of g &amp; ( 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
proofend;

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 &amp; x = - gR ) ) ) &amp; ( for x being set holds
( x in the_RightOptions_of (- g) iff ex gL being ConwayGame st
( gL in the_LeftOptions_of g &amp; x = - gL ) ) ) )
proofend;

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

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

definition
let g be ConwayGame;
attrg is nonnegative  means :Def15: :: CGAMES_1:def 15
 ex s being set st
( g in s &amp; ( 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 &amp; gRL in s ) ) );
end;

:: deftheorem Def15 defines nonnegative CGAMES_1:def_15_:_
 for g being ConwayGame holds
( g is nonnegative iff ex s being set st
( g in s &amp; ( 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 &amp; gRL in s ) ) ) );

definition
let g be ConwayGame;
attrg 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;
attrg is zero  means :Def17: :: CGAMES_1:def 17
( g is nonnegative &amp; g is nonpositive );
attrg is fuzzy  means :Def18: :: CGAMES_1:def 18
( not g is nonnegative &amp; not g is nonpositive );
end;

:: deftheorem Def17 defines zero CGAMES_1:def_17_:_
 for g being ConwayGame holds
( g is zero iff ( g is nonnegative &amp; g is nonpositive ) );

:: deftheorem Def18 defines fuzzy CGAMES_1:def_18_:_
 for g being ConwayGame holds
( g is fuzzy iff ( not g is nonnegative &amp; not g is nonpositive ) );

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

:: deftheorem Def19 defines positive CGAMES_1:def_19_:_
 for g being ConwayGame holds
( g is positive iff ( g is nonnegative &amp; not g is zero ) );

:: deftheorem Def20 defines negative CGAMES_1:def_20_:_
 for g being ConwayGame holds
( g is negative iff ( g is nonpositive &amp; 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 &amp; b1 is nonpositive ) by Def17;
cluster ConwayGame-like nonnegative nonpositive  ->  zero for set ;
coherence
 for b1 being ConwayGame st b1 is nonpositive &amp; b1 is nonnegative holds
b1 is zero by Def17;
cluster ConwayGame-like negative  ->  nonpositive non zero for set ;
coherence
 for b1 being ConwayGame st b1 is negative holds
( b1 is nonpositive &amp; not b1 is zero ) by Def20;
cluster ConwayGame-like nonpositive non zero  ->  negative for set ;
coherence
 for b1 being ConwayGame st b1 is nonpositive &amp; not b1 is zero holds
b1 is negative by Def20;
cluster ConwayGame-like positive  ->  nonnegative non zero for set ;
coherence
 for b1 being ConwayGame st b1 is positive holds
( b1 is nonnegative &amp; not b1 is zero ) by Def19;
cluster ConwayGame-like nonnegative non zero  ->  positive for set ;
coherence
 for b1 being ConwayGame st b1 is nonnegative &amp; not b1 is zero holds
b1 is positive by Def19;
cluster ConwayGame-like fuzzy  ->  non nonnegative non nonpositive for set ;
coherence
 for b1 being ConwayGame st b1 is fuzzy holds
( not b1 is nonnegative &amp; not b1 is nonpositive ) by Def18;
cluster ConwayGame-like non nonnegative non nonpositive  ->  fuzzy for set ;
coherence
 for b1 being ConwayGame st not b1 is nonnegative &amp; not b1 is nonpositive holds
b1 is fuzzy by Def18;
end;

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

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 &amp; gRL is nonnegative ) )
proofend;

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 &amp; gLR is nonpositive ) )
proofend;

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 ) ) &amp; ( ( for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) implies g is nonnegative ) &amp; ( g is nonpositive implies for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) &amp; ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) implies g is nonpositive ) )
proofend;

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 &amp; gL is nonnegative ) &amp; ex gR being ConwayGame st
( gR in the_RightOptions_of g &amp; gR is nonpositive ) ) )
proofend;

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 ) ) &amp; ( for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) ) )
proofend;

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 ) ) &amp; ex gL being ConwayGame st
( gL in the_LeftOptions_of g &amp; gL is nonnegative ) ) )
proofend;

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 ) ) &amp; ex gR being ConwayGame st
( gR in the_RightOptions_of g &amp; gR is nonpositive ) ) )
proofend;

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

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

registration
cluster ConwayGame-like zero for set ;
existence
 ex b1 being ConwayGame st b1 is zero
proofend;
cluster ConwayGame-like positive for set ;
existence
 ex b1 being ConwayGame st b1 is positive
proofend;
cluster ConwayGame-like fuzzy for set ;
existence
 ex b1 being ConwayGame st b1 is fuzzy
proofend;
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
proofend;
end;

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

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

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

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