begin
:: deftheorem defines ConwayZero CGAMES_1:def 1 :
ConwayZero = left-right(# {},{} #);
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]
:: 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:
theorem Th2:
theorem Th3:
begin
:: 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 );
:: 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:
:: 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 ) );
:: 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:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
:: 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:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
begin
begin
:: 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 );
:: 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:
theorem Th21:
theorem Th22:
theorem Th23:
Lm2:
for g being ConwayGame ex f being ConwayGameChain st
( f . 1 = g & f . (len f) = g )
:: 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 ) ) );
:: 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:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem
theorem
begin
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 <> {} } & { ((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 <> {} } )
:: 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 <> {} } #) ) ) );
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
theorem Th39:
theorem Th40:
theorem
:: 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 & ( 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 ) ) ) );
:: deftheorem Def16 defines nonpositive CGAMES_1:def 16 :
for g being ConwayGame holds
( g is nonpositive iff - g is nonnegative );
:: deftheorem Def17 defines zero CGAMES_1:def 17 :
for g being ConwayGame holds
( g is zero iff ( g is nonnegative & g is nonpositive ) );
:: deftheorem Def18 defines fuzzy CGAMES_1:def 18 :
for g being ConwayGame holds
( g is fuzzy iff ( not g is nonnegative & not g is nonpositive ) );
:: deftheorem Def19 defines positive CGAMES_1:def 19 :
for g being ConwayGame holds
( g is positive iff ( g is nonnegative & not g is zero ) );
:: deftheorem Def20 defines negative CGAMES_1:def 20 :
for g being ConwayGame holds
( g is negative iff ( g is nonpositive & not g is zero ) );
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem