environ
vocabularies HIDDEN, CGAMES_1, RELAT_1, TARSKI, XBOOLE_0, ORDINAL1, FUNCT_1, CARD_1, SUBSET_1, XXREAL_0, ORDINAL2, SUPINF_2, ARYTM_1, PARTFUN1, MSUALG_6, FINSEQ_1, ARYTM_3, NAT_1, ORDINAL4, MESFUNC5, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, XXREAL_0, RELAT_1, ORDINAL1, FUNCT_1, CARD_1, PARTFUN1, ORDINAL2, SUBSET_1, COMPUT_1, FINSEQ_1, XCMPLX_0;
definitions FUNCT_1, TARSKI, PARTFUN1;
theorems TARSKI, ORDINAL1, FUNCT_1, ZFMISC_1, RELAT_1, XBOOLE_0, ORDINAL2, XBOOLE_1, PARTFUN1, COMPUT_1, NAT_1, FINSEQ_1, XXREAL_0, XREAL_1, FINSEQ_2, FINSEQ_3, FINSEQ_5, GRFUNC_1, XTUPLE_0;
schemes ORDINAL1, NAT_1, TARSKI;
registrations XBOOLE_0, XREAL_0, XXREAL_0, ORDINAL1, FUNCT_1, CARD_1, SUBSET_1, RELAT_1, COMPUT_1, FINSEQ_1, NAT_1;
constructors HIDDEN, ORDINAL2, COMPUT_1, RELSET_1;
requirements HIDDEN, REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
equalities FINSEQ_1, ORDINAL1;
expansions FUNCT_1, TARSKI, ORDINAL1;
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]
Lm2:
for g being ConwayGame ex f being ConwayGameChain st
( f . 1 = g & f . (len f) = g )
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 <> {} } )
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