:: CGAMES_1 semantic presentation
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
proof
take ConwayZero ; ::_thesis: ( ConwayZero is left-right & ConwayZero is strict )
thus ( ConwayZero is left-right & ConwayZero is strict ) ; ::_thesis: verum
end;
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]
proof
let f be T-Sequence; ::_thesis: ( S1[f] implies for alpha being Ordinal holds S1[f | alpha] )
assume A1: S1[f] ; ::_thesis: for alpha being Ordinal holds S1[f | alpha]
let alpha, beta be Ordinal; ::_thesis: ( beta in dom (f | alpha) implies (f | alpha) . beta = H1((f | alpha) | beta) )
assume A2: beta in dom (f | alpha) ; ::_thesis: (f | alpha) . beta = H1((f | alpha) | beta)
dom (f | alpha) c= dom f by RELAT_1:60;
then A3: f . beta = H1(f | beta) by A1, A2;
dom (f | alpha) c= alpha by RELAT_1:58;
then beta c= alpha by A2, ORDINAL1:def_2;
then (f | alpha) | beta = f | beta by FUNCT_1:51;
hence (f | alpha) . beta = H1((f | alpha) | beta) by A3, A2, FUNCT_1:47; ::_thesis: verum
end;
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 } ) )
proof
consider f being T-Sequence such that
A1: ( dom f = succ alpha & ( for beta being Ordinal
for f1 being T-Sequence st beta in succ alpha & f1 = f | beta holds
f . beta = H1(f1) ) ) from ORDINAL1:sch_4();
take f . alpha ; ::_thesis: ex f being T-Sequence st
( alpha in dom f & f . alpha = f . alpha & ( 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 } ) )
take f ; ::_thesis: ( alpha in dom f & f . alpha = f . alpha & ( 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 } ) )
thus alpha in dom f by A1, ORDINAL1:6; ::_thesis: ( f . alpha = f . alpha & ( 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 } ) )
thus ( f . alpha = f . alpha & ( 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 } ) ) by A1; ::_thesis: verum
end;
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
proof
let x, y be set ; ::_thesis: ( ex f being T-Sequence st
( alpha in dom f & f . alpha = x & ( 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 = y & ( 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 } ) ) implies x = y )
assume ex f1 being T-Sequence st
( alpha in dom f1 & f1 . alpha = x & S1[f1] ) ; ::_thesis: ( for f being T-Sequence holds
( not alpha in dom f or not f . alpha = y or ex beta being Ordinal st
( beta in dom f & not f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) ) or x = y )
then consider f1 being T-Sequence such that
A2: ( alpha in dom f1 & f1 . alpha = x & S1[f1] ) ;
set f1r = f1 | (succ alpha);
assume ex f2 being T-Sequence st
( alpha in dom f2 & f2 . alpha = y & S1[f2] ) ; ::_thesis: x = y
then consider f2 being T-Sequence such that
A3: ( alpha in dom f2 & f2 . alpha = y & S1[f2] ) ;
set f2r = f2 | (succ alpha);
A4: ( dom (f1 | (succ alpha)) = succ alpha & ( for beta being Ordinal
for f being T-Sequence st beta in succ alpha & f = (f1 | (succ alpha)) | beta holds
(f1 | (succ alpha)) . beta = H1(f) ) )
proof
succ alpha c= dom f1 by A2, ORDINAL1:21;
hence A5: dom (f1 | (succ alpha)) = succ alpha by RELAT_1:62; ::_thesis: for beta being Ordinal
for f being T-Sequence st beta in succ alpha & f = (f1 | (succ alpha)) | beta holds
(f1 | (succ alpha)) . beta = H1(f)
let beta be Ordinal; ::_thesis: for f being T-Sequence st beta in succ alpha & f = (f1 | (succ alpha)) | beta holds
(f1 | (succ alpha)) . beta = H1(f)
let f be T-Sequence; ::_thesis: ( beta in succ alpha & f = (f1 | (succ alpha)) | beta implies (f1 | (succ alpha)) . beta = H1(f) )
assume ( beta in succ alpha & f = (f1 | (succ alpha)) | beta ) ; ::_thesis: (f1 | (succ alpha)) . beta = H1(f)
hence (f1 | (succ alpha)) . beta = H1(f) by A5, Lm1, A2; ::_thesis: verum
end;
A6: ( dom (f2 | (succ alpha)) = succ alpha & ( for beta being Ordinal
for f being T-Sequence st beta in succ alpha & f = (f2 | (succ alpha)) | beta holds
(f2 | (succ alpha)) . beta = H1(f) ) )
proof
succ alpha c= dom f2 by A3, ORDINAL1:21;
hence A7: dom (f2 | (succ alpha)) = succ alpha by RELAT_1:62; ::_thesis: for beta being Ordinal
for f being T-Sequence st beta in succ alpha & f = (f2 | (succ alpha)) | beta holds
(f2 | (succ alpha)) . beta = H1(f)
let beta be Ordinal; ::_thesis: for f being T-Sequence st beta in succ alpha & f = (f2 | (succ alpha)) | beta holds
(f2 | (succ alpha)) . beta = H1(f)
let f be T-Sequence; ::_thesis: ( beta in succ alpha & f = (f2 | (succ alpha)) | beta implies (f2 | (succ alpha)) . beta = H1(f) )
assume ( beta in succ alpha & f = (f2 | (succ alpha)) | beta ) ; ::_thesis: (f2 | (succ alpha)) . beta = H1(f)
hence (f2 | (succ alpha)) . beta = H1(f) by A7, Lm1, A3; ::_thesis: verum
end;
A8: ( (f1 | (succ alpha)) . alpha = f1 . alpha & (f2 | (succ alpha)) . alpha = f2 . alpha ) by FUNCT_1:49, ORDINAL1:6;
f1 | (succ alpha) = f2 | (succ alpha) from ORDINAL1:sch_3(A4, A6);
hence x = y by A2, A3, A8; ::_thesis: verum
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 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 ) ) ) )
proof
let z be set ; ::_thesis: 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 ) ) ) )
let alpha be Ordinal; ::_thesis: ( 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 ) ) ) )
consider f being T-Sequence such that
A1: ( alpha in dom f & f . alpha = ConwayDay alpha & S1[f] ) by Def2;
hereby ::_thesis: ( 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 ) ) ) implies z in ConwayDay alpha )
assume z in ConwayDay alpha ; ::_thesis: ex w being strict left-right st
( z = w & ( for e being set st e in the LeftOptions of w \/ the RightOptions of w holds
ex beta being Ordinal st
( beta in alpha & e in ConwayDay beta ) ) )
then z in H1(f | alpha) by A1;
then consider x, y being Subset of (union (rng (f | alpha))) such that
A2: z = left-right(# x,y #) ;
reconsider w = z as strict left-right by A2;
take w = w; ::_thesis: ( z = w & ( for e being set st e in the LeftOptions of w \/ the RightOptions of w holds
ex beta being Ordinal st
( beta in alpha & e in ConwayDay beta ) ) )
thus z = w ; ::_thesis: for e being set st e in the LeftOptions of w \/ the RightOptions of w holds
ex beta being Ordinal st
( beta in alpha & e in ConwayDay beta )
let e be set ; ::_thesis: ( e in the LeftOptions of w \/ the RightOptions of w implies ex beta being Ordinal st
( beta in alpha & e in ConwayDay beta ) )
assume e in the LeftOptions of w \/ the RightOptions of w ; ::_thesis: ex beta being Ordinal st
( beta in alpha & e in ConwayDay beta )
then ( e in x or e in y ) by A2, XBOOLE_0:def_3;
then consider r being set such that
A3: ( e in r & r in rng (f | alpha) ) by TARSKI:def_4;
ex beta being set st
( beta in dom (f | alpha) & r = (f | alpha) . beta ) by A3, FUNCT_1:def_3;
then consider beta being Ordinal such that
A4: ( beta in dom (f | alpha) & r = (f | alpha) . beta ) ;
take beta = beta; ::_thesis: ( beta in alpha & e in ConwayDay beta )
dom (f | alpha) c= alpha by RELAT_1:58;
hence beta in alpha by A4; ::_thesis: e in ConwayDay beta
dom (f | alpha) c= dom f by RELAT_1:60;
then f . beta = ConwayDay beta by A1, Def2, A4;
hence e in ConwayDay beta by A3, A4, FUNCT_1:47; ::_thesis: verum
end;
hereby ::_thesis: verum
assume 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 ) ) ) ; ::_thesis: z in ConwayDay alpha
then consider w being strict left-right such that
A5: ( w = z & ( 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 ) ) ) ;
( the LeftOptions of w is Subset of (union (rng (f | alpha))) & the RightOptions of w is Subset of (union (rng (f | alpha))) )
proof
the LeftOptions of w \/ the RightOptions of w c= union (rng (f | alpha))
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the LeftOptions of w \/ the RightOptions of w or e in union (rng (f | alpha)) )
assume e in the LeftOptions of w \/ the RightOptions of w ; ::_thesis: e in union (rng (f | alpha))
then consider beta being Ordinal such that
A6: ( beta in alpha & e in ConwayDay beta ) by A5;
A7: alpha c= dom f by A1, ORDINAL1:def_2;
then f . beta = ConwayDay beta by Def2, A1, A6;
then ConwayDay beta c= union (rng (f | alpha)) by A6, A7, FUNCT_1:50, ZFMISC_1:74;
hence e in union (rng (f | alpha)) by A6; ::_thesis: verum
end;
hence ( the LeftOptions of w is Subset of (union (rng (f | alpha))) & the RightOptions of w is Subset of (union (rng (f | alpha))) ) by XBOOLE_1:11; ::_thesis: verum
end;
then w in H1(f | alpha) ;
hence z in ConwayDay alpha by A1, A5; ::_thesis: verum
end;
end;
theorem Th2: :: CGAMES_1:2
ConwayDay 0 = {ConwayZero}
proof
A1: ConwayDay 0 c= {ConwayZero}
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ConwayDay 0 or z in {ConwayZero} )
assume z in ConwayDay 0 ; ::_thesis: z in {ConwayZero}
then consider w being strict left-right such that
A2: ( z = w & ( for e being set st e in the LeftOptions of w \/ the RightOptions of w holds
ex beta being Ordinal st
( beta in 0 & e in ConwayDay beta ) ) ) by Th1;
the LeftOptions of w \/ the RightOptions of w = {}
proof
assume not the LeftOptions of w \/ the RightOptions of w = {} ; ::_thesis: contradiction
then consider e being set such that
A3: e in the LeftOptions of w \/ the RightOptions of w by XBOOLE_0:def_1;
ex beta being Ordinal st
( beta in 0 & e in ConwayDay beta ) by A2, A3;
hence contradiction ; ::_thesis: verum
end;
then ( the LeftOptions of w = {} & the RightOptions of w = {} ) ;
hence z in {ConwayZero} by A2, TARSKI:def_1; ::_thesis: verum
end;
for e being set st e in {} \/ {} holds
ex beta being Ordinal st
( beta in 0 & e in ConwayDay beta ) ;
then ConwayZero in ConwayDay 0 by Th1;
then {ConwayZero} c= ConwayDay 0 by ZFMISC_1:31;
hence ConwayDay 0 = {ConwayZero} by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th3: :: CGAMES_1:3
for alpha, beta being Ordinal st alpha c= beta holds
ConwayDay alpha c= ConwayDay beta
proof
let alpha, beta be Ordinal; ::_thesis: ( alpha c= beta implies ConwayDay alpha c= ConwayDay beta )
assume A1: alpha c= beta ; ::_thesis: ConwayDay alpha c= ConwayDay beta
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in ConwayDay alpha or z in ConwayDay beta )
assume z in ConwayDay alpha ; ::_thesis: z in ConwayDay beta
then consider w being strict left-right such that
A2: ( w = z & ( for e being set st e in the LeftOptions of w \/ the RightOptions of w holds
ex gamma being Ordinal st
( gamma in alpha & e in ConwayDay gamma ) ) ) by Th1;
now__::_thesis:_for_e_being_set_st_e_in_the_LeftOptions_of_w_\/_the_RightOptions_of_w_holds_
ex_gamma_being_Ordinal_st_
(_gamma_in_beta_&_e_in_ConwayDay_gamma_)
let e be set ; ::_thesis: ( e in the LeftOptions of w \/ the RightOptions of w implies ex gamma being Ordinal st
( gamma in beta & e in ConwayDay gamma ) )
assume e in the LeftOptions of w \/ the RightOptions of w ; ::_thesis: ex gamma being Ordinal st
( gamma in beta & e in ConwayDay gamma )
then ex gamma being Ordinal st
( gamma in alpha & e in ConwayDay gamma ) by A2;
hence ex gamma being Ordinal st
( gamma in beta & e in ConwayDay gamma ) by A1; ::_thesis: verum
end;
hence z in ConwayDay beta by Th1, A2; ::_thesis: verum
end;
registration
let alpha be Ordinal;
cluster ConwayDay alpha -> non empty ;
coherence
not ConwayDay alpha is empty
proof
0 c= alpha ;
then ConwayDay 0 c= ConwayDay alpha by Th3;
hence not ConwayDay alpha is empty by Th2; ::_thesis: verum
end;
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
proof
let x be Element of ConwayDay alpha; ::_thesis: x is ConwayGame-like
take alpha ; :: according to CGAMES_1:def_3 ::_thesis: x in ConwayDay alpha
thus x in ConwayDay alpha ; ::_thesis: verum
end;
end;
registration
cluster ConwayZero -> ConwayGame-like ;
coherence
ConwayZero is ConwayGame-like
proof
ConwayZero in ConwayDay 0 by Th2, TARSKI:def_1;
hence ConwayZero is ConwayGame-like ; ::_thesis: verum
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
take ConwayZero ; ::_thesis: ( ConwayZero is left-right & ConwayZero is ConwayGame-like & ConwayZero is strict )
thus ( ConwayZero is left-right & ConwayZero is ConwayGame-like & ConwayZero is strict ) ; ::_thesis: verum
end;
cluster ConwayGame-like for set ;
existence
ex b1 being set st b1 is ConwayGame-like
proof
take ConwayZero ; ::_thesis: ConwayZero is ConwayGame-like
thus ConwayZero is ConwayGame-like ; ::_thesis: verum
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
set w = left-right(# {ConwayZero},{} #);
for x being set st x in the LeftOptions of left-right(# {ConwayZero},{} #) \/ the RightOptions of left-right(# {ConwayZero},{} #) holds
ex beta being Ordinal st
( beta in 1 & x in ConwayDay beta )
proof
let x be set ; ::_thesis: ( x in the LeftOptions of left-right(# {ConwayZero},{} #) \/ the RightOptions of left-right(# {ConwayZero},{} #) implies ex beta being Ordinal st
( beta in 1 & x in ConwayDay beta ) )
assume x in the LeftOptions of left-right(# {ConwayZero},{} #) \/ the RightOptions of left-right(# {ConwayZero},{} #) ; ::_thesis: ex beta being Ordinal st
( beta in 1 & x in ConwayDay beta )
then A1: x = ConwayZero by TARSKI:def_1;
take 0 ; ::_thesis: ( 0 in 1 & x in ConwayDay 0 )
1 = succ 0 ;
hence ( 0 in 1 & x in ConwayDay 0 ) by A1, ORDINAL1:6; ::_thesis: verum
end;
hence left-right(# {ConwayZero},{} #) is Element of ConwayDay 1 by Th1; ::_thesis: verum
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
set w = left-right(# {ConwayZero},{ConwayZero} #);
for x being set st x in the LeftOptions of left-right(# {ConwayZero},{ConwayZero} #) \/ the RightOptions of left-right(# {ConwayZero},{ConwayZero} #) holds
ex beta being Ordinal st
( beta in 1 & x in ConwayDay beta )
proof
let x be set ; ::_thesis: ( x in the LeftOptions of left-right(# {ConwayZero},{ConwayZero} #) \/ the RightOptions of left-right(# {ConwayZero},{ConwayZero} #) implies ex beta being Ordinal st
( beta in 1 & x in ConwayDay beta ) )
assume x in the LeftOptions of left-right(# {ConwayZero},{ConwayZero} #) \/ the RightOptions of left-right(# {ConwayZero},{ConwayZero} #) ; ::_thesis: ex beta being Ordinal st
( beta in 1 & x in ConwayDay beta )
then A2: x = ConwayZero by TARSKI:def_1;
take 0 ; ::_thesis: ( 0 in 1 & x in ConwayDay 0 )
1 = succ 0 ;
hence ( 0 in 1 & x in ConwayDay 0 ) by A2, ORDINAL1:6; ::_thesis: verum
end;
hence left-right(# {ConwayZero},{ConwayZero} #) is Element of ConwayDay 1 by Th1; ::_thesis: verum
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
let g be ConwayGame; ::_thesis: g is strict left-right
consider alpha being Ordinal such that
A1: g in ConwayDay alpha by Def3;
ex w being strict left-right st
( w = g & ( 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 ) ) ) by A1, Th1;
hence g is strict left-right ; ::_thesis: verum
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
reconsider w = g as left-right by Th4;
take the LeftOptions of w ; ::_thesis: ex w being left-right st
( g = w & the LeftOptions of w = the LeftOptions of w )
thus ex w being left-right st
( g = w & the LeftOptions of w = the LeftOptions of w ) ; ::_thesis: verum
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
reconsider w = g as left-right by Th4;
take the RightOptions of w ; ::_thesis: ex w being left-right st
( g = w & the RightOptions of w = the RightOptions of w )
thus ex w being left-right st
( g = w & the RightOptions of w = the RightOptions of w ) ; ::_thesis: verum
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
let g1, g2 be ConwayGame; ::_thesis: ( g1 = g2 iff ( the_LeftOptions_of g1 = the_LeftOptions_of g2 & the_RightOptions_of g1 = the_RightOptions_of g2 ) )
thus ( g1 = g2 implies ( the_LeftOptions_of g1 = the_LeftOptions_of g2 & the_RightOptions_of g1 = the_RightOptions_of g2 ) ) ; ::_thesis: ( the_LeftOptions_of g1 = the_LeftOptions_of g2 & the_RightOptions_of g1 = the_RightOptions_of g2 implies g1 = g2 )
reconsider w1 = g1 as strict left-right by Th4;
reconsider w2 = g2 as strict left-right by Th4;
assume A1: ( the_LeftOptions_of g1 = the_LeftOptions_of g2 & the_RightOptions_of g1 = the_RightOptions_of g2 ) ; ::_thesis: g1 = g2
( the LeftOptions of w1 = the_LeftOptions_of g1 & the LeftOptions of w2 = the_LeftOptions_of g2 & the RightOptions of w1 = the_RightOptions_of g1 & the RightOptions of w2 = the_RightOptions_of g2 ) by Def6, Def7;
hence g1 = g2 by A1; ::_thesis: verum
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
let g be ConwayGame; ::_thesis: ( g = ConwayZero iff the_Options_of g = {} )
hereby ::_thesis: ( the_Options_of g = {} implies g = ConwayZero )
assume g = ConwayZero ; ::_thesis: the_Options_of g = {}
then ( the_LeftOptions_of g = {} & the_RightOptions_of g = {} ) ;
hence the_Options_of g = {} ; ::_thesis: verum
end;
hereby ::_thesis: verum
reconsider w = g as strict left-right by Th4;
assume the_Options_of g = {} ; ::_thesis: g = ConwayZero
then ( the_LeftOptions_of g = {} & the_RightOptions_of g = {} ) ;
then ( the LeftOptions of w = {} & the RightOptions of w = {} ) by Def6, Def7;
hence g = ConwayZero ; ::_thesis: verum
end;
end;
theorem Th7: :: CGAMES_1:7
for x being set holds
( x in the_LeftOptions_of ConwayOne iff x = ConwayZero )
proof
let x be set ; ::_thesis: ( x in the_LeftOptions_of ConwayOne iff x = ConwayZero )
the_LeftOptions_of ConwayOne = {ConwayZero} by Def6;
hence ( x in the_LeftOptions_of ConwayOne iff x = ConwayZero ) by TARSKI:def_1; ::_thesis: verum
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
let x be set ; ::_thesis: ( ( 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 ) )
( the_LeftOptions_of ConwayStar = {ConwayZero} & the_RightOptions_of ConwayStar = {ConwayZero} ) by Def6, Def7;
hence ( ( 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 ) ) by TARSKI:def_1; ::_thesis: verum
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
let alpha be Ordinal; ::_thesis: 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 ) )
let g be ConwayGame; ::_thesis: ( 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 ) )
hereby ::_thesis: ( ( for x being set st x in the_Options_of g holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) ) implies g in ConwayDay alpha )
assume g in ConwayDay alpha ; ::_thesis: for x being set st x in the_Options_of g holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta )
then consider w being strict left-right such that
A1: ( g = 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 ) ) ) by Th1;
let x be set ; ::_thesis: ( x in the_Options_of g implies ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) )
A2: ( the LeftOptions of w = the_LeftOptions_of g & the RightOptions of w = the_RightOptions_of g ) by A1, Def6, Def7;
assume x in the_Options_of g ; ::_thesis: ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta )
hence ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) by A1, A2; ::_thesis: verum
end;
hereby ::_thesis: verum
assume A3: for x being set st x in the_Options_of g holds
ex beta being Ordinal st
( beta in alpha & x in ConwayDay beta ) ; ::_thesis: g in ConwayDay alpha
ex w being left-right st
( g = 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
reconsider w = g as strict left-right by Th4;
take w ; ::_thesis: ( g = 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 ) ) )
( the LeftOptions of w = the_LeftOptions_of g & the RightOptions of w = the_RightOptions_of g ) by Def6, Def7;
hence ( g = 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 ) ) ) by A3; ::_thesis: verum
end;
hence g in ConwayDay alpha by Th1; ::_thesis: verum
end;
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
defpred S2[ Ordinal] means g in ConwayDay $1;
A2: ex alpha being Ordinal st S2[alpha] by Def3, A1;
consider alpha being Ordinal such that
A3: ( S2[alpha] & ( for beta being Ordinal st S2[beta] holds
alpha c= beta ) ) from ORDINAL1:sch_1(A2);
take alpha ; ::_thesis: ( g in ConwayDay alpha & ( for beta being Ordinal st beta in alpha holds
not g in ConwayDay beta ) )
thus g in ConwayDay alpha by A3; ::_thesis: for beta being Ordinal st beta in alpha holds
not g in ConwayDay beta
let beta be Ordinal; ::_thesis: ( beta in alpha implies not g in ConwayDay beta )
assume A4: beta in alpha ; ::_thesis: not g in ConwayDay beta
assume g in ConwayDay beta ; ::_thesis: contradiction
then alpha c= beta by A3;
then beta in beta by A4;
hence contradiction ; ::_thesis: verum
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
let alpha1, alpha2 be Ordinal; ::_thesis: ( g in ConwayDay alpha1 & ( for beta being Ordinal st beta in alpha1 holds
not g in ConwayDay beta ) & g in ConwayDay alpha2 & ( for beta being Ordinal st beta in alpha2 holds
not g in ConwayDay beta ) implies alpha1 = alpha2 )
assume A5: ( g in ConwayDay alpha1 & ( for beta being Ordinal st beta in alpha1 holds
not g in ConwayDay beta ) ) ; ::_thesis: ( not g in ConwayDay alpha2 or ex beta being Ordinal st
( beta in alpha2 & g in ConwayDay beta ) or alpha1 = alpha2 )
assume A6: ( g in ConwayDay alpha2 & ( for beta being Ordinal st beta in alpha2 holds
not g in ConwayDay beta ) ) ; ::_thesis: alpha1 = alpha2
assume A7: alpha1 <> alpha2 ; ::_thesis: contradiction
percases ( alpha1 in alpha2 or alpha2 in alpha1 ) by A7, ORDINAL1:14;
suppose alpha1 in alpha2 ; ::_thesis: contradiction
hence contradiction by A5, A6; ::_thesis: verum
end;
suppose alpha2 in alpha1 ; ::_thesis: contradiction
hence contradiction by A5, A6; ::_thesis: verum
end;
end;
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
let x be set ; ::_thesis: for alpha being Ordinal
for g being ConwayGame st g in ConwayDay alpha & x in the_Options_of g holds
x in ConwayDay alpha
let alpha be Ordinal; ::_thesis: for g being ConwayGame st g in ConwayDay alpha & x in the_Options_of g holds
x in ConwayDay alpha
let g be ConwayGame; ::_thesis: ( g in ConwayDay alpha & x in the_Options_of g implies x in ConwayDay alpha )
assume ( g in ConwayDay alpha & x in the_Options_of g ) ; ::_thesis: x in ConwayDay alpha
then consider beta being Ordinal such that
A1: ( beta in alpha & x in ConwayDay beta ) by Th9;
beta c= alpha by A1, ORDINAL1:def_2;
then ConwayDay beta c= ConwayDay alpha by Th3;
hence x in ConwayDay alpha by A1; ::_thesis: verum
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
let x be set ; ::_thesis: 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
let alpha be Ordinal; ::_thesis: 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
let g be ConwayGame; ::_thesis: ( g in ConwayDay alpha & ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) implies x in ConwayDay alpha )
( ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) implies x in the_Options_of g ) by XBOOLE_0:def_3;
hence ( g in ConwayDay alpha & ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) implies x in ConwayDay alpha ) by Th10; ::_thesis: verum
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
let alpha be Ordinal; ::_thesis: for g being ConwayGame holds
( g in ConwayDay alpha iff ConwayRank g c= alpha )
let g be ConwayGame; ::_thesis: ( g in ConwayDay alpha iff ConwayRank g c= alpha )
hereby ::_thesis: ( ConwayRank g c= alpha implies g in ConwayDay alpha )
assume A1: g in ConwayDay alpha ; ::_thesis: ConwayRank g c= alpha
assume not ConwayRank g c= alpha ; ::_thesis: contradiction
then alpha in ConwayRank g by ORDINAL1:16;
hence contradiction by A1, Def9; ::_thesis: verum
end;
hereby ::_thesis: verum
assume ConwayRank g c= alpha ; ::_thesis: g in ConwayDay alpha
then A2: ConwayDay (ConwayRank g) c= ConwayDay alpha by Th3;
g in ConwayDay (ConwayRank g) by Def9;
hence g in ConwayDay alpha by A2; ::_thesis: verum
end;
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
let alpha be Ordinal; ::_thesis: for g being ConwayGame holds
( ConwayRank g in alpha iff ex beta being Ordinal st
( beta in alpha & g in ConwayDay beta ) )
let g be ConwayGame; ::_thesis: ( ConwayRank g in alpha iff ex beta being Ordinal st
( beta in alpha & g in ConwayDay beta ) )
hereby ::_thesis: ( ex beta being Ordinal st
( beta in alpha & g in ConwayDay beta ) implies ConwayRank g in alpha )
assume A1: ConwayRank g in alpha ; ::_thesis: ex beta being Ordinal st
( beta in alpha & g in ConwayDay beta )
take beta = ConwayRank g; ::_thesis: ( beta in alpha & g in ConwayDay beta )
thus beta in alpha by A1; ::_thesis: g in ConwayDay beta
thus g in ConwayDay beta by Th12; ::_thesis: verum
end;
hereby ::_thesis: verum
assume ex beta being Ordinal st
( beta in alpha & g in ConwayDay beta ) ; ::_thesis: ConwayRank g in alpha
then consider beta being Ordinal such that
A2: ( beta in alpha & g in ConwayDay beta ) ;
ConwayRank g c= beta by Th12, A2;
hence ConwayRank g in alpha by A2, ORDINAL1:12; ::_thesis: verum
end;
end;
theorem Th14: :: CGAMES_1:14
for gO, g being ConwayGame st gO in the_Options_of g holds
ConwayRank gO in ConwayRank g
proof
let gO, g be ConwayGame; ::_thesis: ( gO in the_Options_of g implies ConwayRank gO in ConwayRank g )
set alpha = ConwayRank g;
A1: g in ConwayDay (ConwayRank g) by Def9;
assume gO in the_Options_of g ; ::_thesis: ConwayRank gO in ConwayRank g
then consider beta being Ordinal such that
A2: ( beta in ConwayRank g & gO in ConwayDay beta ) by A1, Th9;
ConwayRank gO c= beta by A2, Th12;
hence ConwayRank gO in ConwayRank g by A2, ORDINAL1:12; ::_thesis: verum
end;
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
proof
let gO, g be ConwayGame; ::_thesis: ( ( gO in the_LeftOptions_of g or gO in the_RightOptions_of g ) implies ConwayRank gO in ConwayRank g )
assume ( gO in the_LeftOptions_of g or gO in the_RightOptions_of g ) ; ::_thesis: ConwayRank gO in ConwayRank g
then gO in the_Options_of g by XBOOLE_0:def_3;
hence ConwayRank gO in ConwayRank g by Th14; ::_thesis: verum
end;
theorem Th16: :: CGAMES_1:16
for g being ConwayGame holds not g in the_Options_of g
proof
let g be ConwayGame; ::_thesis: not g in the_Options_of g
assume g in the_Options_of g ; ::_thesis: contradiction
then ConwayRank g in ConwayRank g by Th14;
hence contradiction ; ::_thesis: verum
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
let x be set ; ::_thesis: for g being ConwayGame st x in the_Options_of g holds
x is ConwayGame-like left-right
let g be ConwayGame; ::_thesis: ( x in the_Options_of g implies x is ConwayGame-like left-right )
consider alpha being Ordinal such that
A1: g in ConwayDay alpha by Def3;
assume x in the_Options_of g ; ::_thesis: x is ConwayGame-like left-right
then x in ConwayDay alpha by Th10, A1;
hence x is ConwayGame-like left-right by Th4; ::_thesis: verum
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
let x be set ; ::_thesis: 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
let g be ConwayGame; ::_thesis: ( ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) implies x is ConwayGame-like left-right )
assume ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) ; ::_thesis: x is ConwayGame-like left-right
then x in the_Options_of g by XBOOLE_0:def_3;
hence x is ConwayGame-like left-right by Th17; ::_thesis: verum
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
let w be strict left-right ; ::_thesis: ( w is ConwayGame iff for z being set st z in the LeftOptions of w \/ the RightOptions of w holds
z is ConwayGame )
hereby ::_thesis: ( ( for z being set st z in the LeftOptions of w \/ the RightOptions of w holds
z is ConwayGame ) implies w is ConwayGame )
assume w is ConwayGame ; ::_thesis: for z being set st z in the LeftOptions of w \/ the RightOptions of w holds
z is ConwayGame
then reconsider g = w as ConwayGame ;
( the LeftOptions of w = the_LeftOptions_of g & the RightOptions of w = the_RightOptions_of g ) by Def6, Def7;
then the LeftOptions of w \/ the RightOptions of w = the_Options_of g ;
hence for z being set st z in the LeftOptions of w \/ the RightOptions of w holds
z is ConwayGame by Th17; ::_thesis: verum
end;
hereby ::_thesis: verum
assume A1: for z being set st z in the LeftOptions of w \/ the RightOptions of w holds
z is ConwayGame ; ::_thesis: w is ConwayGame
set Z = { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ;
set alpha = sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ;
now__::_thesis:_for_z_being_set_st_z_in_the_LeftOptions_of_w_\/_the_RightOptions_of_w_holds_
ex_beta_being_set_st_
(_beta_in_succ_(sup__{__(ConwayRank_z)_where_z_is_Element_of_the_LeftOptions_of_w_\/_the_RightOptions_of_w_:_verum__}__)_&_z_in_ConwayDay_beta_)
let z be set ; ::_thesis: ( z in the LeftOptions of w \/ the RightOptions of w implies ex beta being set st
( beta in succ (sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ) & z in ConwayDay beta ) )
assume A2: z in the LeftOptions of w \/ the RightOptions of w ; ::_thesis: ex beta being set st
( beta in succ (sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ) & z in ConwayDay beta )
then ConwayRank z in { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ;
then ( ConwayRank z in On { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } & On { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } c= sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ) by ORDINAL1:def_9, ORDINAL2:def_3;
then A3: ConwayRank z c= sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } by ORDINAL1:def_2;
take beta = sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ; ::_thesis: ( beta in succ (sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ) & z in ConwayDay beta )
thus beta in succ (sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } ) by ORDINAL1:6; ::_thesis: z in ConwayDay beta
z is ConwayGame by A1, A2;
hence z in ConwayDay beta by A3, Th12; ::_thesis: verum
end;
then w in ConwayDay (succ (sup { (ConwayRank z) where z is Element of the LeftOptions of w \/ the RightOptions of w : verum } )) by Th1;
hence w is ConwayGame ; ::_thesis: verum
end;
end;
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]
proof
defpred S2[ Ordinal] means for g being ConwayGame st g in ConwayDay $1 holds
not P1[g];
assume A2: for g being ConwayGame holds
( not P1[g] or ex g1 being ConwayGame st
( ConwayRank g1 in ConwayRank g & P1[g1] ) ) ; ::_thesis: contradiction
A3: for alpha being Ordinal st ( for beta being Ordinal st beta in alpha holds
S2[beta] ) holds
S2[alpha]
proof
let alpha be Ordinal; ::_thesis: ( ( for beta being Ordinal st beta in alpha holds
S2[beta] ) implies S2[alpha] )
assume A4: for beta being Ordinal st beta in alpha holds
S2[beta] ; ::_thesis: S2[alpha]
let g be ConwayGame; ::_thesis: ( g in ConwayDay alpha implies not P1[g] )
assume A5: ( g in ConwayDay alpha & P1[g] ) ; ::_thesis: contradiction
then consider g1 being ConwayGame such that
A6: ( ConwayRank g1 in ConwayRank g & P1[g1] ) by A2;
ConwayRank g c= alpha by Th12, A5;
then consider beta being Ordinal such that
A7: ( beta in alpha & g1 in ConwayDay beta ) by Th13, A6;
thus contradiction by A4, A7, A6; ::_thesis: verum
end;
A8: for alpha being Ordinal holds S2[alpha] from ORDINAL1:sch_2(A3);
consider g being ConwayGame such that
A9: P1[g] by A1;
consider alpha being Ordinal such that
A10: g in ConwayDay alpha by Def3;
thus contradiction by A8, A9, A10; ::_thesis: verum
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
consider g being ConwayGame such that
A2: ( P1[g] & ( for g1 being ConwayGame st ConwayRank g1 in ConwayRank g holds
not P1[g1] ) ) from CGAMES_1:sch_1(A1);
take g ; ::_thesis: ( P1[g] & ( for gO being ConwayGame st gO in the_Options_of g holds
not P1[gO] ) )
thus P1[g] by A2; ::_thesis: for gO being ConwayGame st gO in the_Options_of g holds
not P1[gO]
let gO be ConwayGame; ::_thesis: ( gO in the_Options_of g implies not P1[gO] )
assume gO in the_Options_of g ; ::_thesis: P1[gO]
then ConwayRank gO in ConwayRank g by Th14;
hence P1[gO] by A2; ::_thesis: verum
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
defpred S2[ ConwayGame] means P1[$1];
assume A2: ex g being ConwayGame st S2[g] ; ::_thesis: contradiction
ex g being ConwayGame st
( S2[g] & ( for gO being ConwayGame st gO in the_Options_of g holds
not S2[gO] ) ) from CGAMES_1:sch_2(A2);
hence contradiction by A1; ::_thesis: verum
end;
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
proof
let x be set ; :: according to CGAMES_1:def_10 ::_thesis: ( x in dom <*g*> implies <*g*> . x is ConwayGame )
assume x in dom <*g*> ; ::_thesis: <*g*> . x is ConwayGame
then x = 1 by FINSEQ_1:90;
hence <*g*> . x is ConwayGame by FINSEQ_1:def_8; ::_thesis: verum
end;
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 & not b1 is empty )
proof
take <*ConwayZero*> ; ::_thesis: ( <*ConwayZero*> is ConwayGame-valued & not <*ConwayZero*> is empty )
thus ( <*ConwayZero*> is ConwayGame-valued & not <*ConwayZero*> is empty ) ; ::_thesis: verum
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;
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 & n > 1 holds
n - 1 in dom f
proof
let f be FinSequence; ::_thesis: for n being Nat st n in dom f & n > 1 holds
n - 1 in dom f
consider l being Nat such that
A1: dom f = Seg l by FINSEQ_1:def_2;
thus for n being Nat st n in dom f & n > 1 holds
n - 1 in dom f by A1, FINSEQ_3:12; ::_thesis: verum
end;
registration
let g be ConwayGame;
cluster<*g*> -> ConwayGameChain-like ;
coherence
<*g*> is ConwayGameChain-like
proof
let n be Element of dom <*g*>; :: according to CGAMES_1:def_11 ::_thesis: ( n > 1 implies <*g*> . (n - 1) in the_Options_of (<*g*> . n) )
dom <*g*> = {1} by FINSEQ_1:2, FINSEQ_1:def_8;
hence ( n > 1 implies <*g*> . (n - 1) in the_Options_of (<*g*> . n) ) by TARSKI:def_1; ::_thesis: verum
end;
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
proof
set g = the ConwayGame;
take <* the ConwayGame*> ; ::_thesis: <* the ConwayGame*> is ConwayGameChain-like
thus <* the ConwayGame*> is ConwayGameChain-like ; ::_thesis: verum
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
let f be ConwayGameChain; ::_thesis: for n, m being Element of dom f st n < m holds
ConwayRank (f . n) in ConwayRank (f . m)
let n, m be Element of dom f; ::_thesis: ( n < m implies ConwayRank (f . n) in ConwayRank (f . m) )
assume A1: n < m ; ::_thesis: ConwayRank (f . n) in ConwayRank (f . m)
consider l being Nat such that
A2: dom f = Seg l by FINSEQ_1:def_2;
defpred S2[ Nat] means ( m - $1 in dom f implies ConwayRank (f . (m - $1)) in ConwayRank (f . m) );
n >= 1 by A2, FINSEQ_1:1;
then A3: m > 1 by A1, XXREAL_0:2;
A4: S2[1]
proof
assume m - 1 in dom f ; ::_thesis: ConwayRank (f . (m - 1)) in ConwayRank (f . m)
then reconsider m1 = m - 1 as Element of dom f ;
f . m1 in the_Options_of (f . m) by A3, Def11;
hence ConwayRank (f . (m - 1)) in ConwayRank (f . m) by Th14; ::_thesis: verum
end;
A5: for k being non empty Nat st S2[k] holds
S2[k + 1]
proof
let k be non empty Nat; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A6: S2[k] ; ::_thesis: S2[k + 1]
assume m - (k + 1) in dom f ; ::_thesis: ConwayRank (f . (m - (k + 1))) in ConwayRank (f . m)
then reconsider mk1 = m - (k + 1) as Element of dom f ;
k <= k + 1 by XREAL_1:31;
then ( 1 <= mk1 & mk1 <= m - k & m - k <= m & m <= l ) by A2, FINSEQ_1:1, XREAL_1:10, XREAL_1:43;
then A7: ( 1 <= m - k & m - k <= l ) by XXREAL_0:2;
then ( m >= k + 1 & k <= k + 1 ) by XREAL_1:19, XREAL_1:31;
then m - k is Nat by NAT_1:21, XXREAL_0:2;
then reconsider mk = m - k as Element of dom f by A7, A2, FINSEQ_1:1;
( mk1 + 1 > 1 & mk1 = mk - 1 ) by XREAL_1:29;
then f . mk1 in the_Options_of (f . mk) by Def11;
then ( ConwayRank (f . mk1) in ConwayRank (f . mk) & ConwayRank (f . mk) in ConwayRank (f . m) ) by Th14, A6;
hence ConwayRank (f . (m - (k + 1))) in ConwayRank (f . m) by ORDINAL1:10; ::_thesis: verum
end;
A8: for k being non empty Nat holds S2[k] from NAT_1:sch_10(A4, A5);
reconsider k = m - n as non empty Nat by A1, NAT_1:21;
m - k = n ;
hence ConwayRank (f . n) in ConwayRank (f . m) by A8; ::_thesis: verum
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
let f be ConwayGameChain; ::_thesis: for n, m being Element of dom f st n <= m holds
ConwayRank (f . n) c= ConwayRank (f . m)
let n, m be Element of dom f; ::_thesis: ( n <= m implies ConwayRank (f . n) c= ConwayRank (f . m) )
assume A1: n <= m ; ::_thesis: ConwayRank (f . n) c= ConwayRank (f . m)
percases ( n < m or n = m ) by A1, XXREAL_0:1;
suppose n < m ; ::_thesis: ConwayRank (f . n) c= ConwayRank (f . m)
then ConwayRank (f . n) in ConwayRank (f . m) by Th21;
hence ConwayRank (f . n) c= ConwayRank (f . m) by ORDINAL1:def_2; ::_thesis: verum
end;
suppose n = m ; ::_thesis: ConwayRank (f . n) c= ConwayRank (f . m)
hence ConwayRank (f . n) c= ConwayRank (f . m) ; ::_thesis: verum
end;
end;
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
let alpha be Ordinal; ::_thesis: for f being ConwayGameChain st f . (len f) in ConwayDay alpha holds
f . 1 in ConwayDay alpha
let f be ConwayGameChain; ::_thesis: ( f . (len f) in ConwayDay alpha implies f . 1 in ConwayDay alpha )
assume A1: f . (len f) in ConwayDay alpha ; ::_thesis: f . 1 in ConwayDay alpha
reconsider n = 1 as Element of dom f by FINSEQ_5:6;
reconsider m = len f as Element of dom f by FINSEQ_5:6;
n <= m by NAT_1:14;
then ( ConwayRank (f . n) c= ConwayRank (f . m) & ConwayRank (f . m) c= alpha ) by Th22, A1, Th12;
then ConwayRank (f . n) c= alpha by XBOOLE_1:1;
hence f . 1 in ConwayDay alpha by Th12; ::_thesis: verum
end;
Lm2: for g being ConwayGame ex f being ConwayGameChain st
( f . 1 = g & f . (len f) = g )
proof
let g be ConwayGame; ::_thesis: ex f being ConwayGameChain st
( f . 1 = g & f . (len f) = g )
take f = <*g*>; ::_thesis: ( f . 1 = g & f . (len f) = g )
len f = 1 by FINSEQ_1:40;
hence ( f . 1 = g & f . (len f) = g ) by FINSEQ_1:40; ::_thesis: verum
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
consider alpha being Ordinal such that
A1: g in ConwayDay alpha by Def3;
take s = { x where x is Element of ConwayDay alpha : ex f being ConwayGameChain st
( f . 1 = x & f . (len f) = g ) } ; ::_thesis: for z being set holds
( z in s iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) )
let z be set ; ::_thesis: ( z in s iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) )
hereby ::_thesis: ( ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) implies z in s )
assume z in s ; ::_thesis: ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g )
then consider x being Element of ConwayDay alpha such that
A2: ( x = z & ex f being ConwayGameChain st
( f . 1 = x & f . (len f) = g ) ) ;
thus ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) by A2; ::_thesis: verum
end;
assume ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) ; ::_thesis: z in s
then consider f being ConwayGameChain such that
A3: ( f . 1 = z & f . (len f) = g ) ;
f . 1 in ConwayDay alpha by Th23, A1, A3;
hence z in s by A3; ::_thesis: verum
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
let t1, t2 be set ; ::_thesis: ( ( for z being set holds
( z in t1 iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) ) ) & ( for z being set holds
( z in t2 iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) ) ) implies t1 = t2 )
assume A4: for z being set holds
( z in t1 iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) ) ; ::_thesis: ( ex z being set st
( ( z in t2 implies ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) ) implies ( ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) & not z in t2 ) ) or t1 = t2 )
assume A5: for z being set holds
( z in t2 iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) ) ; ::_thesis: t1 = t2
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_t1_implies_z_in_t2_)_&_(_z_in_t2_implies_z_in_t1_)_)
let z be set ; ::_thesis: ( ( z in t1 implies z in t2 ) & ( z in t2 implies z in t1 ) )
hereby ::_thesis: ( z in t2 implies z in t1 )
assume z in t1 ; ::_thesis: z in t2
then ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) by A4;
hence z in t2 by A5; ::_thesis: verum
end;
hereby ::_thesis: verum
assume z in t2 ; ::_thesis: z in t1
then ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) by A5;
hence z in t1 by A4; ::_thesis: verum
end;
end;
hence t1 = t2 by TARSKI:1; ::_thesis: verum
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
ex f being ConwayGameChain st
( f . 1 = g & f . (len f) = g ) by Lm2;
hence not the_Tree_of g is empty by Def12; ::_thesis: verum
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
let g be ConwayGame; ::_thesis: g in the_Tree_of g
ex f being ConwayGameChain st
( f . 1 = g & f . (len f) = g ) by Lm2;
hence g in the_Tree_of g by Def12; ::_thesis: verum
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
the_Tree_of g c= ConwayDay alpha
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in the_Tree_of g or z in ConwayDay alpha )
assume z in the_Tree_of g ; ::_thesis: z in ConwayDay alpha
then consider f being ConwayGameChain such that
A1: ( f . 1 = z & f . (len f) = g ) by Def12;
thus z in ConwayDay alpha by A1, Th23; ::_thesis: verum
end;
hence the_Tree_of g is Subset of (ConwayDay alpha) ; ::_thesis: verum
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
let g1 be Element of the_Tree_of g; ::_thesis: g1 is ConwayGame-like
consider alpha being Ordinal such that
A1: g in ConwayDay alpha by Def3;
ex f being ConwayGameChain st
( f . 1 = g1 & f . (len f) = g ) by Def12;
then g1 in ConwayDay alpha by Th23, A1;
hence g1 is ConwayGame-like ; ::_thesis: verum
end;
end;
theorem Th25: :: CGAMES_1:25
for f being ConwayGameChain
for n being non empty Nat holds f | n is ConwayGameChain
proof
let f be ConwayGameChain; ::_thesis: for n being non empty Nat holds f | n is ConwayGameChain
let n be non empty Nat; ::_thesis: f | n is ConwayGameChain
set ls = len (f | n);
A1: f | n is ConwayGame-valued
proof
let x be set ; :: according to CGAMES_1:def_10 ::_thesis: ( x in dom (f | n) implies (f | n) . x is ConwayGame )
assume A2: x in dom (f | n) ; ::_thesis: (f | n) . x is ConwayGame
dom (f | n) c= dom f by RELAT_1:60;
then f . x is ConwayGame by A2;
hence (f | n) . x is ConwayGame by A2, FUNCT_1:47; ::_thesis: verum
end;
( len f >= 1 & n >= 1 & len (f | n) = min (n,(len f)) ) by FINSEQ_2:21, NAT_1:14;
then reconsider fs = f | n as non empty ConwayGame-valued FinSequence by A1, XXREAL_0:20;
fs is ConwayGameChain-like
proof
let n be Element of dom fs; :: according to CGAMES_1:def_11 ::_thesis: ( n > 1 implies fs . (n - 1) in the_Options_of (fs . n) )
assume A3: n > 1 ; ::_thesis: fs . (n - 1) in the_Options_of (fs . n)
( dom fs c= dom f & n in dom fs & n - 1 in dom fs ) by Th20, A3, RELAT_1:60;
then ( n in dom f & f . n = fs . n & f . (n - 1) = fs . (n - 1) ) by FUNCT_1:47;
hence fs . (n - 1) in the_Options_of (fs . n) by Def11, A3; ::_thesis: verum
end;
hence f | n is ConwayGameChain ; ::_thesis: verum
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
let f1, f2 be ConwayGameChain; ::_thesis: ( ex g being ConwayGame st
( g = f2 . 1 & f1 . (len f1) in the_Options_of g ) implies f1 ^ f2 is ConwayGameChain )
assume A1: ex g being ConwayGame st
( g = f2 . 1 & f1 . (len f1) in the_Options_of g ) ; ::_thesis: f1 ^ f2 is ConwayGameChain
then reconsider g = f2 . 1 as ConwayGame ;
f1 ^ f2 is ConwayGame-valued
proof
let x be set ; :: according to CGAMES_1:def_10 ::_thesis: ( x in dom (f1 ^ f2) implies (f1 ^ f2) . x is ConwayGame )
set y = (f1 ^ f2) . x;
assume x in dom (f1 ^ f2) ; ::_thesis: (f1 ^ f2) . x is ConwayGame
then (f1 ^ f2) . x in rng (f1 ^ f2) by FUNCT_1:3;
then A2: (f1 ^ f2) . x in (rng f1) \/ (rng f2) by FINSEQ_1:31;
percases ( (f1 ^ f2) . x in rng f1 or (f1 ^ f2) . x in rng f2 ) by A2, XBOOLE_0:def_3;
suppose (f1 ^ f2) . x in rng f1 ; ::_thesis: (f1 ^ f2) . x is ConwayGame
then ex z being set st
( z in dom f1 & (f1 ^ f2) . x = f1 . z ) by FUNCT_1:def_3;
hence (f1 ^ f2) . x is ConwayGame ; ::_thesis: verum
end;
suppose (f1 ^ f2) . x in rng f2 ; ::_thesis: (f1 ^ f2) . x is ConwayGame
then ex z being set st
( z in dom f2 & (f1 ^ f2) . x = f2 . z ) by FUNCT_1:def_3;
hence (f1 ^ f2) . x is ConwayGame ; ::_thesis: verum
end;
end;
end;
then reconsider f12 = f1 ^ f2 as non empty ConwayGame-valued FinSequence ;
f12 is ConwayGameChain-like
proof
let n be Element of dom f12; :: according to CGAMES_1:def_11 ::_thesis: ( n > 1 implies f12 . (n - 1) in the_Options_of (f12 . n) )
assume A3: n > 1 ; ::_thesis: f12 . (n - 1) in the_Options_of (f12 . n)
percases ( n < (len f1) + 1 or n = (len f1) + 1 or n > (len f1) + 1 ) by XXREAL_0:1;
suppose n < (len f1) + 1 ; ::_thesis: f12 . (n - 1) in the_Options_of (f12 . n)
then n <= len f1 by NAT_1:22;
then reconsider n0 = n as Element of dom f1 by A3, FINSEQ_3:25;
n0 - 1 in dom f1 by Th20, A3;
then ( f1 . n0 = f12 . n0 & f1 . (n0 - 1) = f12 . (n0 - 1) ) by FINSEQ_1:def_7;
hence f12 . (n - 1) in the_Options_of (f12 . n) by A3, Def11; ::_thesis: verum
end;
supposeA4: n = (len f1) + 1 ; ::_thesis: f12 . (n - 1) in the_Options_of (f12 . n)
( len f1 in dom f1 & 1 in dom f2 ) by FINSEQ_5:6;
then ( f12 . (n - 1) = f1 . (len f1) & f12 . n = f2 . 1 ) by A4, FINSEQ_1:def_7;
hence f12 . (n - 1) in the_Options_of (f12 . n) by A1; ::_thesis: verum
end;
supposeA5: n > (len f1) + 1 ; ::_thesis: f12 . (n - 1) in the_Options_of (f12 . n)
( n <= len f12 & len f12 = (len f1) + (len f2) & n >= len f1 ) by A5, FINSEQ_1:22, FINSEQ_3:25, XREAL_1:38;
then A6: ( n - (len f1) > 1 & n - (len f1) <= len f2 & n - (len f1) is Nat ) by A5, NAT_1:21, XREAL_1:20;
then reconsider k = n - (len f1) as Element of dom f2 by FINSEQ_3:25;
k - 1 in dom f2 by A6, Th20;
then ( f12 . ((len f1) + k) = f2 . k & f12 . ((len f1) + (k - 1)) = f2 . (k - 1) ) by FINSEQ_1:def_7;
hence f12 . (n - 1) in the_Options_of (f12 . n) by A6, Def11; ::_thesis: verum
end;
end;
end;
hence f1 ^ f2 is ConwayGameChain ; ::_thesis: verum
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
let x be set ; ::_thesis: 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 ) ) )
let g be ConwayGame; ::_thesis: ( 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 ) ) )
hereby ::_thesis: ( ( x = g or ex gO being ConwayGame st
( gO in the_Options_of g & x in the_Tree_of gO ) ) implies x in the_Tree_of g )
assume x in the_Tree_of g ; ::_thesis: ( x <> g implies ex gO being set st
( gO in the_Options_of g & x in the_Tree_of gO ) )
then consider f being ConwayGameChain such that
A1: ( f . 1 = x & f . (len f) = g ) by Def12;
reconsider n = len f as Element of dom f by FINSEQ_5:6;
assume A2: x <> g ; ::_thesis: ex gO being set st
( gO in the_Options_of g & x in the_Tree_of gO )
then A3: n > 1 by A1, NAT_1:53;
reconsider n1 = n - 1 as Element of dom f by Th20, A1, A2, NAT_1:53;
take gO = f . n1; ::_thesis: ( gO in the_Options_of g & x in the_Tree_of gO )
thus gO in the_Options_of g by Def11, A3, A1; ::_thesis: x in the_Tree_of gO
reconsider nf = f | n1 as ConwayGameChain by Th25;
( n1 < n & 1 in dom nf & len nf in dom nf ) by FINSEQ_5:6, XREAL_1:44;
then ( len nf = n1 & nf . 1 = f . 1 & nf . (len nf) = f . (len nf) ) by FINSEQ_1:59, FUNCT_1:47;
hence x in the_Tree_of gO by Def12, A1; ::_thesis: verum
end;
hereby ::_thesis: verum
assume A4: ( x = g or ex gO being ConwayGame st
( gO in the_Options_of g & x in the_Tree_of gO ) ) ; ::_thesis: x in the_Tree_of g
percases ( x = g or ex gO being ConwayGame st
( gO in the_Options_of g & x in the_Tree_of gO ) ) by A4;
suppose x = g ; ::_thesis: x in the_Tree_of g
hence x in the_Tree_of g by Th24; ::_thesis: verum
end;
suppose ex gO being ConwayGame st
( gO in the_Options_of g & x in the_Tree_of gO ) ; ::_thesis: x in the_Tree_of g
then consider gO being ConwayGame such that
A5: ( gO in the_Options_of g & x in the_Tree_of gO ) ;
consider f being ConwayGameChain such that
A6: ( f . 1 = x & f . (len f) = gO ) by A5, Def12;
ex g1 being ConwayGame st
( g1 = <*g*> . 1 & f . (len f) in the_Options_of g1 )
proof
take g ; ::_thesis: ( g = <*g*> . 1 & f . (len f) in the_Options_of g )
thus ( g = <*g*> . 1 & f . (len f) in the_Options_of g ) by A5, A6, FINSEQ_1:def_8; ::_thesis: verum
end;
then reconsider nf = f ^ <*g*> as ConwayGameChain by Th26;
( 1 in dom f & len nf = (len f) + 1 ) by FINSEQ_2:16, FINSEQ_5:6;
then ( nf . 1 = x & nf . (len nf) = g ) by A6, FINSEQ_1:42, FINSEQ_1:def_7;
hence x in the_Tree_of g by Def12; ::_thesis: verum
end;
end;
end;
end;
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 )
proof
let gO, g be ConwayGame; ::_thesis: ( not gO in the_Tree_of g or gO = g or ConwayRank gO in ConwayRank g )
assume gO in the_Tree_of g ; ::_thesis: ( gO = g or ConwayRank gO in ConwayRank g )
then consider f being ConwayGameChain such that
A1: ( f . 1 = gO & f . (len f) = g ) by Def12;
reconsider n = 1 as Element of dom f by FINSEQ_5:6;
reconsider m = len f as Element of dom f by FINSEQ_5:6;
A2: m >= 1 by NAT_1:14;
percases ( m = 1 or m > 1 ) by A2, XXREAL_0:1;
suppose m = 1 ; ::_thesis: ( gO = g or ConwayRank gO in ConwayRank g )
hence ( gO = g or ConwayRank gO in ConwayRank g ) by A1; ::_thesis: verum
end;
suppose m > 1 ; ::_thesis: ( gO = g or ConwayRank gO in ConwayRank g )
then ConwayRank (f . n) in ConwayRank (f . m) by Th21;
hence ( gO = g or ConwayRank gO in ConwayRank g ) by A1; ::_thesis: verum
end;
end;
end;
theorem Th29: :: CGAMES_1:29
for gO, g being ConwayGame st gO in the_Tree_of g holds
ConwayRank gO c= ConwayRank g
proof
let gO, g be ConwayGame; ::_thesis: ( gO in the_Tree_of g implies ConwayRank gO c= ConwayRank g )
assume A1: gO in the_Tree_of g ; ::_thesis: ConwayRank gO c= ConwayRank g
percases ( gO = g or ConwayRank gO in ConwayRank g ) by A1, Th28;
suppose gO = g ; ::_thesis: ConwayRank gO c= ConwayRank g
hence ConwayRank gO c= ConwayRank g ; ::_thesis: verum
end;
suppose ConwayRank gO in ConwayRank g ; ::_thesis: ConwayRank gO c= ConwayRank g
hence ConwayRank gO c= ConwayRank g by ORDINAL1:def_2; ::_thesis: verum
end;
end;
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
let g be ConwayGame; ::_thesis: 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
let s be set ; ::_thesis: ( g in s & ( for g1 being ConwayGame st g1 in s holds
the_Options_of g1 c= s ) implies the_Tree_of g c= s )
assume A1: ( g in s & ( for g1 being ConwayGame st g1 in s holds
the_Options_of g1 c= s ) ) ; ::_thesis: the_Tree_of g c= s
hereby :: according to TARSKI:def_3 ::_thesis: verum
let z be set ; ::_thesis: ( z in the_Tree_of g implies z in s )
assume z in the_Tree_of g ; ::_thesis: z in s
then consider f being ConwayGameChain such that
A2: ( f . 1 = z & f . (len f) = g ) by Def12;
defpred S2[ Nat] means ( $1 + 1 <= len f & f . ($1 + 1) in s );
len f > 0 ;
then reconsider m = (len f) - 1 as Nat by NAT_1:20;
S2[m] by A2, A1;
then A3: ex k being Nat st S2[k] ;
A4: for k being Nat st k <> 0 & S2[k] holds
ex n being Nat st
( n < k & S2[n] )
proof
let k be Nat; ::_thesis: ( k <> 0 & S2[k] implies ex n being Nat st
( n < k & S2[n] ) )
assume A5: ( k <> 0 & S2[k] ) ; ::_thesis: ex n being Nat st
( n < k & S2[n] )
then reconsider m = k - 1 as Nat by NAT_1:20;
take m ; ::_thesis: ( m < k & S2[m] )
thus m < k by XREAL_1:147; ::_thesis: S2[m]
then m + 1 < k + 1 by XREAL_1:6;
hence m + 1 <= len f by A5, XXREAL_0:2; ::_thesis: f . (m + 1) in s
A6: k + 1 > 1 by A5, XREAL_1:29;
then reconsider k1 = k + 1 as Element of dom f by A5, FINSEQ_3:25;
( f . (k1 - 1) in the_Options_of (f . k1) & the_Options_of (f . k1) c= s ) by Def11, A1, A5, A6;
hence f . (m + 1) in s ; ::_thesis: verum
end;
S2[ 0 ] from NAT_1:sch_7(A3, A4);
hence z in s by A2; ::_thesis: verum
end;
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
let g1, g2 be ConwayGame; ::_thesis: ( g1 in the_Tree_of g2 implies the_Tree_of g1 c= the_Tree_of g2 )
assume g1 in the_Tree_of g2 ; ::_thesis: the_Tree_of g1 c= the_Tree_of g2
then consider f2 being ConwayGameChain such that
A1: ( f2 . 1 = g1 & f2 . (len f2) = g2 ) by Def12;
hereby :: according to TARSKI:def_3 ::_thesis: verum
let x be set ; ::_thesis: ( x in the_Tree_of g1 implies b1 in the_Tree_of g2 )
assume x in the_Tree_of g1 ; ::_thesis: b1 in the_Tree_of g2
then consider f1 being ConwayGameChain such that
A2: ( f1 . 1 = x & f1 . (len f1) = g1 ) by Def12;
A3: len f1 >= 1 by NAT_1:14;
percases ( len f1 = 1 or len f1 > 1 ) by A3, XXREAL_0:1;
suppose len f1 = 1 ; ::_thesis: b1 in the_Tree_of g2
hence x in the_Tree_of g2 by A1, A2, Def12; ::_thesis: verum
end;
supposeA4: len f1 > 1 ; ::_thesis: b1 in the_Tree_of g2
then reconsider n0 = (len f1) - 1 as non empty Nat by NAT_1:21;
reconsider f0 = f1 | n0 as ConwayGameChain by Th25;
( len f1 is Element of dom f1 & n0 <= len f1 ) by FINSEQ_5:6, XREAL_1:43;
then ( f1 . n0 in the_Options_of g1 & f0 . n0 = f1 . n0 & len f0 = n0 ) by Def11, A2, A4, FINSEQ_1:59, FINSEQ_3:112;
then reconsider f = f0 ^ f2 as ConwayGameChain by Th26, A1;
n0 >= 1 by NAT_1:14;
then ( 1 in dom f0 & len f2 in dom f2 & f0 . 1 = f1 . 1 & len f = (len f0) + (len f2) ) by FINSEQ_1:22, FINSEQ_3:112, FINSEQ_5:6;
then ( f . 1 = x & f . (len f) = g2 ) by A1, A2, FINSEQ_1:def_7;
hence x in the_Tree_of g2 by Def12; ::_thesis: verum
end;
end;
end;
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
let g1, g2 be ConwayGame; ::_thesis: ( g1 in the_Tree_of g2 implies the_proper_Tree_of g1 c= the_proper_Tree_of g2 )
assume A1: g1 in the_Tree_of g2 ; ::_thesis: the_proper_Tree_of g1 c= the_proper_Tree_of g2
then A2: the_Tree_of g1 c= the_Tree_of g2 by Th31;
hereby :: according to TARSKI:def_3 ::_thesis: verum
let x be set ; ::_thesis: ( x in the_proper_Tree_of g1 implies x in the_proper_Tree_of g2 )
assume A3: x in the_proper_Tree_of g1 ; ::_thesis: x in the_proper_Tree_of g2
then A4: ( x in the_Tree_of g1 & x <> g1 ) by ZFMISC_1:56;
assume A5: not x in the_proper_Tree_of g2 ; ::_thesis: contradiction
then A6: x = g2 by A2, A4, ZFMISC_1:56;
percases ( g1 = g2 or ConwayRank g1 in ConwayRank g2 ) by Th28, A1;
suppose g1 = g2 ; ::_thesis: contradiction
hence contradiction by A3, A5; ::_thesis: verum
end;
supposeA7: ConwayRank g1 in ConwayRank g2 ; ::_thesis: contradiction
reconsider g = x as ConwayGame by A3;
ConwayRank g in ConwayRank g2 by A7, Th29, A4, ORDINAL1:12;
hence contradiction by A6; ::_thesis: verum
end;
end;
end;
end;
theorem Th33: :: CGAMES_1:33
for g being ConwayGame holds the_Options_of g c= the_proper_Tree_of g
proof
let g be ConwayGame; ::_thesis: the_Options_of g c= the_proper_Tree_of g
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the_Options_of g or x in the_proper_Tree_of g )
assume A1: x in the_Options_of g ; ::_thesis: x in the_proper_Tree_of g
reconsider gO = x as ConwayGame by A1, Th17;
gO in the_Tree_of gO by Th24;
then gO in the_Tree_of g by A1, Th27;
then ( gO = g or gO in the_proper_Tree_of g ) by ZFMISC_1:56;
hence x in the_proper_Tree_of g by A1, Th16; ::_thesis: verum
end;
theorem Th34: :: CGAMES_1:34
for g being ConwayGame holds the_Options_of g c= the_Tree_of g
proof
let g be ConwayGame; ::_thesis: the_Options_of g c= the_Tree_of g
the_Options_of g c= the_proper_Tree_of g by Th33;
hence the_Options_of g c= the_Tree_of g by XBOOLE_1:1; ::_thesis: verum
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
let g1, g2 be ConwayGame; ::_thesis: ( g1 in the_proper_Tree_of g2 implies the_Tree_of g1 c= the_proper_Tree_of g2 )
assume A1: g1 in the_proper_Tree_of g2 ; ::_thesis: the_Tree_of g1 c= the_proper_Tree_of g2
then A2: ( g1 in the_Tree_of g2 & g1 <> g2 ) by ZFMISC_1:56;
A3: the_Tree_of g1 c= the_Tree_of g2 by Th31, A1;
not g2 in the_Tree_of g1
proof
A4: ConwayRank g1 in ConwayRank g2 by A2, Th28;
assume g2 in the_Tree_of g1 ; ::_thesis: contradiction
then ConwayRank g2 c= ConwayRank g1 by Th29;
then ConwayRank g1 in ConwayRank g1 by A4;
hence contradiction ; ::_thesis: verum
end;
hence the_Tree_of g1 c= the_proper_Tree_of g2 by A3, ZFMISC_1:34; ::_thesis: verum
end;
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
proof
let gO, g be ConwayGame; ::_thesis: ( gO in the_Options_of g implies the_Tree_of gO c= the_proper_Tree_of g )
assume A1: gO in the_Options_of g ; ::_thesis: the_Tree_of gO c= the_proper_Tree_of g
the_Options_of g c= the_proper_Tree_of g by Th33;
hence the_Tree_of gO c= the_proper_Tree_of g by Th35, A1; ::_thesis: verum
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
let g be ConwayGame; ::_thesis: ConwayZero in the_Tree_of g
defpred S2[ ConwayGame] means not ConwayZero in the_Tree_of $1;
assume not ConwayZero in the_Tree_of g ; ::_thesis: contradiction
then A1: ex g being ConwayGame st S2[g] ;
consider g being ConwayGame such that
A2: ( S2[g] & ( for gO being ConwayGame st gO in the_Options_of g holds
not S2[gO] ) ) from CGAMES_1:sch_2(A1);
percases ( g = ConwayZero or the_Options_of g <> {} ) by Th6;
suppose g = ConwayZero ; ::_thesis: contradiction
hence contradiction by Th24, A2; ::_thesis: verum
end;
suppose the_Options_of g <> {} ; ::_thesis: contradiction
then consider x being set such that
A3: x in the_Options_of g by XBOOLE_0:def_1;
reconsider gO = x as ConwayGame by Th17, A3;
A4: ConwayZero in the_Tree_of gO by A2, A3;
the_Options_of g c= the_Tree_of g by Th34;
then the_Tree_of gO c= the_Tree_of g by Th31, A3;
hence contradiction by A2, A4; ::_thesis: verum
end;
end;
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
consider g being ConwayGame such that
A2: ( P1[g] & ( for g1 being ConwayGame st ConwayRank g1 in ConwayRank g holds
not P1[g1] ) ) from CGAMES_1:sch_1(A1);
take g ; ::_thesis: ( P1[g] & ( for gO being ConwayGame st gO in the_proper_Tree_of g holds
not P1[gO] ) )
now__::_thesis:_for_gO_being_ConwayGame_st_gO_in_the_proper_Tree_of_g_holds_
not_P1[gO]
let gO be ConwayGame; ::_thesis: ( gO in the_proper_Tree_of g implies not P1[gO] )
assume gO in the_proper_Tree_of g ; ::_thesis: P1[gO]
then ( gO in the_Tree_of g & gO <> g ) by ZFMISC_1:56;
then ConwayRank gO in ConwayRank g by Th28;
hence P1[gO] by A2; ::_thesis: verum
end;
hence ( P1[g] & ( for gO being ConwayGame st gO in the_proper_Tree_of g holds
not P1[gO] ) ) by A2; ::_thesis: verum
end;
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 & 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
let g be ConwayGame; ::_thesis: 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
let f1, f2 be Function; ::_thesis: ( 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))) ) implies f1 = f2 )
assume A1: ( 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))) ) ) ; ::_thesis: f1 = f2
defpred S2[ ConwayGame] means ( $1 in the_Tree_of g & f1 . $1 <> f2 . $1 );
assume f1 <> f2 ; ::_thesis: contradiction
then ex x being set st
( x in the_Tree_of g & f1 . x <> f2 . x ) by A1, FUNCT_1:def_11;
then A2: ex g0 being ConwayGame st S2[g0] ;
consider gm being ConwayGame such that
A3: ( S2[gm] & ( for gO being ConwayGame st gO in the_proper_Tree_of gm holds
not S2[gO] ) ) from CGAMES_1:sch_4(A2);
A4: f1 | (the_proper_Tree_of gm) = f2 | (the_proper_Tree_of gm)
proof
now__::_thesis:_(_dom_(f1_|_(the_proper_Tree_of_gm))_=_dom_(f2_|_(the_proper_Tree_of_gm))_&_(_for_x_being_set_st_x_in_dom_(f1_|_(the_proper_Tree_of_gm))_holds_
(f1_|_(the_proper_Tree_of_gm))_._x_=_(f2_|_(the_proper_Tree_of_gm))_._x_)_)
set f1r = f1 | (the_proper_Tree_of gm);
set f2r = f2 | (the_proper_Tree_of gm);
A5: the_Tree_of gm c= the_Tree_of g by A3, Th31;
then A6: the_proper_Tree_of gm c= the_Tree_of g by XBOOLE_1:1;
A7: ( dom (f1 | (the_proper_Tree_of gm)) = the_proper_Tree_of gm & dom (f2 | (the_proper_Tree_of gm)) = the_proper_Tree_of gm ) by A1, A5, RELAT_1:62, XBOOLE_1:1;
hence dom (f1 | (the_proper_Tree_of gm)) = dom (f2 | (the_proper_Tree_of gm)) ; ::_thesis: for x being set st x in dom (f1 | (the_proper_Tree_of gm)) holds
(f1 | (the_proper_Tree_of gm)) . x = (f2 | (the_proper_Tree_of gm)) . x
hereby ::_thesis: verum
let x be set ; ::_thesis: ( x in dom (f1 | (the_proper_Tree_of gm)) implies (f1 | (the_proper_Tree_of gm)) . x = (f2 | (the_proper_Tree_of gm)) . x )
assume A8: x in dom (f1 | (the_proper_Tree_of gm)) ; ::_thesis: (f1 | (the_proper_Tree_of gm)) . x = (f2 | (the_proper_Tree_of gm)) . x
reconsider g0 = x as ConwayGame by A7, A8;
( f1 . x = f2 . x & (f1 | (the_proper_Tree_of gm)) . x = f1 . x & (f2 | (the_proper_Tree_of gm)) . x = f2 . x ) by A3, A6, A7, A8, FUNCT_1:47;
hence (f1 | (the_proper_Tree_of gm)) . x = (f2 | (the_proper_Tree_of gm)) . x ; ::_thesis: verum
end;
end;
hence f1 | (the_proper_Tree_of gm) = f2 | (the_proper_Tree_of gm) by FUNCT_1:def_11; ::_thesis: verum
end;
( f1 . gm = F1(gm,(f1 | (the_proper_Tree_of gm))) & f2 . gm = F1(gm,(f2 | (the_proper_Tree_of gm))) ) by A1, A3;
hence contradiction by A4, A3; ::_thesis: verum
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
defpred S2[ Function] means for g being ConwayGame st g in dom $1 holds
$1 . g = F1(g,($1 | (the_proper_Tree_of g)));
defpred S3[ ConwayGame] means ex f being Function st
( dom f = the_Tree_of $1 & S2[f] );
defpred S4[ set , set ] means ex g being ConwayGame st
( $1 = g & ex f being Function st
( $2 = f & dom f = the_Tree_of g & S2[f] ) );
A1: 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 from CGAMES_1:sch_5();
then A2: for x, y, z being set st S4[x,y] & S4[x,z] holds
y = z ;
A3: for g being ConwayGame
for f being Function st S2[f] holds
S2[f | (the_Tree_of g)]
proof
let g be ConwayGame; ::_thesis: for f being Function st S2[f] holds
S2[f | (the_Tree_of g)]
let f be Function; ::_thesis: ( S2[f] implies S2[f | (the_Tree_of g)] )
assume A4: S2[f] ; ::_thesis: S2[f | (the_Tree_of g)]
let g1 be ConwayGame; ::_thesis: ( g1 in dom (f | (the_Tree_of g)) implies (f | (the_Tree_of g)) . g1 = F1(g1,((f | (the_Tree_of g)) | (the_proper_Tree_of g1))) )
assume A5: g1 in dom (f | (the_Tree_of g)) ; ::_thesis: (f | (the_Tree_of g)) . g1 = F1(g1,((f | (the_Tree_of g)) | (the_proper_Tree_of g1)))
dom (f | (the_Tree_of g)) c= dom f by RELAT_1:60;
then A6: ( f . g1 = F1(g1,(f | (the_proper_Tree_of g1))) & f . g1 = (f | (the_Tree_of g)) . g1 ) by A4, A5, FUNCT_1:47;
dom (f | (the_Tree_of g)) c= the_Tree_of g by RELAT_1:58;
then the_Tree_of g1 c= the_Tree_of g by Th31, A5;
hence (f | (the_Tree_of g)) . g1 = F1(g1,((f | (the_Tree_of g)) | (the_proper_Tree_of g1))) by A6, RELAT_1:74, XBOOLE_1:1; ::_thesis: verum
end;
A7: for g being ConwayGame st ( for gO being ConwayGame st gO in the_Options_of g holds
S3[gO] ) holds
S3[g]
proof
let g be ConwayGame; ::_thesis: ( ( for gO being ConwayGame st gO in the_Options_of g holds
S3[gO] ) implies S3[g] )
assume A8: for gO being ConwayGame st gO in the_Options_of g holds
S3[gO] ; ::_thesis: S3[g]
consider FUNCS being set such that
A9: for y being set holds
( y in FUNCS iff ex x being set st
( x in the_Tree_of g & S4[x,y] ) ) from TARSKI:sch_1(A2);
( FUNCS is functional & FUNCS is compatible )
proof
thus FUNCS is functional ::_thesis: FUNCS is compatible
proof
let y be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not y in FUNCS or y is set )
assume y in FUNCS ; ::_thesis: y is set
then ex x being set st
( x in the_Tree_of g & S4[x,y] ) by A9;
hence y is set ; ::_thesis: verum
end;
now__::_thesis:_for_f1,_f2_being_Function_st_f1_in_FUNCS_&_f2_in_FUNCS_holds_
f1_tolerates_f2
let f1, f2 be Function; ::_thesis: ( f1 in FUNCS & f2 in FUNCS implies f1 tolerates f2 )
assume f1 in FUNCS ; ::_thesis: ( f2 in FUNCS implies f1 tolerates f2 )
then ex x being set st
( x in the_Tree_of g & S4[x,f1] ) by A9;
then consider g1 being ConwayGame such that
A10: ( g1 in the_Tree_of g & dom f1 = the_Tree_of g1 & S2[f1] ) ;
assume f2 in FUNCS ; ::_thesis: f1 tolerates f2
then ex x being set st
( x in the_Tree_of g & S4[x,f2] ) by A9;
then consider g2 being ConwayGame such that
A11: ( g2 in the_Tree_of g & dom f2 = the_Tree_of g2 & S2[f2] ) ;
thus f1 tolerates f2 ::_thesis: verum
proof
let x be set ; :: according to PARTFUN1:def_4 ::_thesis: ( not x in (dom f1) /\ (dom f2) or f1 . x = f2 . x )
assume x in (dom f1) /\ (dom f2) ; ::_thesis: f1 . x = f2 . x
then A12: ( x in the_Tree_of g1 & x in the_Tree_of g2 ) by A10, A11, XBOOLE_0:def_4;
then reconsider g0 = x as ConwayGame ;
set T = the_Tree_of g0;
( the_Tree_of g0 c= dom f1 & the_Tree_of g0 c= dom f2 ) by Th31, A10, A11, A12;
then ( dom (f1 | (the_Tree_of g0)) = the_Tree_of g0 & dom (f2 | (the_Tree_of g0)) = the_Tree_of g0 & S2[f1 | (the_Tree_of g0)] & S2[f2 | (the_Tree_of g0)] ) by A3, A10, A11, RELAT_1:62;
then ( f1 | (the_Tree_of g0) = f2 | (the_Tree_of g0) & g0 in dom (f1 | (the_Tree_of g0)) & g0 in dom (f2 | (the_Tree_of g0)) ) by A1, Th24;
then ( f1 | (the_Tree_of g0) = f2 | (the_Tree_of g0) & f1 . g0 = (f1 | (the_Tree_of g0)) . g0 & f2 . g0 = (f2 | (the_Tree_of g0)) . g0 ) by FUNCT_1:47;
hence f1 . x = f2 . x ; ::_thesis: verum
end;
end;
hence FUNCS is compatible by COMPUT_1:def_1; ::_thesis: verum
end;
then reconsider FS = FUNCS as functional compatible set ;
reconsider f = union FS as Function ;
take f ; ::_thesis: ( dom f = the_Tree_of g & S2[f] )
A13: the_proper_Tree_of g c= dom f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the_proper_Tree_of g or x in dom f )
assume x in the_proper_Tree_of g ; ::_thesis: x in dom f
then ( x in the_Tree_of g & x <> g ) by ZFMISC_1:56;
then consider gO being ConwayGame such that
A14: ( gO in the_Options_of g & x in the_Tree_of gO ) by Th27;
consider fO being Function such that
A15: ( dom fO = the_Tree_of gO & S2[fO] ) by A8, A14;
the_Options_of g c= the_Tree_of g by Th34;
then fO in FUNCS by A9, A14, A15;
then ( dom fO c= dom f & x in dom fO ) by A14, A15, COMPUT_1:13;
hence x in dom f ; ::_thesis: verum
end;
A16: dom f c= the_Tree_of g
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in the_Tree_of g )
assume x in dom f ; ::_thesis: x in the_Tree_of g
then [x,(f . x)] in f by FUNCT_1:def_2;
then ex y being set st
( [x,(f . x)] in y & y in FUNCS ) by TARSKI:def_4;
then consider f1 being Function such that
A17: ( [x,(f . x)] in f1 & f1 in FUNCS ) ;
ex y being set st
( y in the_Tree_of g & S4[y,f1] ) by A17, A9;
then consider g1 being ConwayGame such that
A18: ( g1 in the_Tree_of g & dom f1 = the_Tree_of g1 ) ;
( x in dom f1 & dom f1 c= the_Tree_of g ) by A17, A18, Th31, XTUPLE_0:def_12;
hence x in the_Tree_of g ; ::_thesis: verum
end;
A19: S2[f]
proof
let g1 be ConwayGame; ::_thesis: ( g1 in dom f implies f . g1 = F1(g1,(f | (the_proper_Tree_of g1))) )
assume g1 in dom f ; ::_thesis: f . g1 = F1(g1,(f | (the_proper_Tree_of g1)))
then [g1,(f . g1)] in f by FUNCT_1:def_2;
then ex x being set st
( [g1,(f . g1)] in x & x in FUNCS ) by TARSKI:def_4;
then consider fO being Function such that
A20: ( [g1,(f . g1)] in fO & fO in FUNCS ) ;
ex x being set st
( x in the_Tree_of g & S4[x,fO] ) by A9, A20;
then consider gO being ConwayGame such that
A21: ( gO in the_Tree_of g & dom fO = the_Tree_of gO & S2[fO] ) ;
A22: fO | (the_proper_Tree_of g1) = f | (the_proper_Tree_of g1)
proof
now__::_thesis:_(_dom_(fO_|_(the_proper_Tree_of_g1))_=_dom_(f_|_(the_proper_Tree_of_g1))_&_(_for_x_being_set_st_x_in_dom_(fO_|_(the_proper_Tree_of_g1))_holds_
(fO_|_(the_proper_Tree_of_g1))_._x_=_(f_|_(the_proper_Tree_of_g1))_._x_)_)
g1 in the_Tree_of gO by A20, A21, FUNCT_1:1;
then the_Tree_of g1 c= the_Tree_of gO by Th31;
then A23: the_proper_Tree_of g1 c= dom fO by A21, XBOOLE_1:1;
dom fO c= dom f by A20, COMPUT_1:13;
then A24: ( dom (fO | (the_proper_Tree_of g1)) = the_proper_Tree_of g1 & dom (f | (the_proper_Tree_of g1)) = the_proper_Tree_of g1 ) by A23, RELAT_1:62, XBOOLE_1:1;
hence dom (fO | (the_proper_Tree_of g1)) = dom (f | (the_proper_Tree_of g1)) ; ::_thesis: for x being set st x in dom (fO | (the_proper_Tree_of g1)) holds
(fO | (the_proper_Tree_of g1)) . x = (f | (the_proper_Tree_of g1)) . x
hereby ::_thesis: verum
let x be set ; ::_thesis: ( x in dom (fO | (the_proper_Tree_of g1)) implies (fO | (the_proper_Tree_of g1)) . x = (f | (the_proper_Tree_of g1)) . x )
assume A25: x in dom (fO | (the_proper_Tree_of g1)) ; ::_thesis: (fO | (the_proper_Tree_of g1)) . x = (f | (the_proper_Tree_of g1)) . x
then ( x in dom fO & x in dom (f | (the_proper_Tree_of g1)) ) by A24, RELAT_1:57;
then ( fO . x = f . x & (fO | (the_proper_Tree_of g1)) . x = fO . x & (f | (the_proper_Tree_of g1)) . x = f . x ) by A25, A20, COMPUT_1:13, FUNCT_1:47;
hence (fO | (the_proper_Tree_of g1)) . x = (f | (the_proper_Tree_of g1)) . x ; ::_thesis: verum
end;
end;
hence fO | (the_proper_Tree_of g1) = f | (the_proper_Tree_of g1) by FUNCT_1:def_11; ::_thesis: verum
end;
g1 in the_Tree_of gO by A20, A21, FUNCT_1:1;
then ( fO . g1 = F1(g1,(fO | (the_proper_Tree_of g1))) & fO . g1 = f . g1 ) by A21, A20, COMPUT_1:13;
hence f . g1 = F1(g1,(f | (the_proper_Tree_of g1))) by A22; ::_thesis: verum
end;
g in dom f
proof
assume A26: not g in dom f ; ::_thesis: contradiction
set v = F1(g,(f | (the_proper_Tree_of g)));
dom {[g,F1(g,(f | (the_proper_Tree_of g)))]} = {g} by RELAT_1:9;
then {[g,F1(g,(f | (the_proper_Tree_of g)))]} tolerates f by A26, PARTFUN1:56, ZFMISC_1:50;
then ex h being Function st h = {[g,F1(g,(f | (the_proper_Tree_of g)))]} \/ f by PARTFUN1:51;
then reconsider h = {[g,F1(g,(f | (the_proper_Tree_of g)))]} \/ f as Function ;
A27: dom h = (dom f) \/ (dom {[g,F1(g,(f | (the_proper_Tree_of g)))]}) by RELAT_1:1;
then A28: dom h = (dom f) \/ {g} by RELAT_1:9;
A29: S4[g,h]
proof
take g ; ::_thesis: ( g = g & ex f being Function st
( h = f & dom f = the_Tree_of g & S2[f] ) )
thus g = g ; ::_thesis: ex f being Function st
( h = f & dom f = the_Tree_of g & S2[f] )
take h ; ::_thesis: ( h = h & dom h = the_Tree_of g & S2[h] )
thus h = h ; ::_thesis: ( dom h = the_Tree_of g & S2[h] )
now__::_thesis:_(_(_for_x_being_set_st_x_in_the_Tree_of_g_holds_
x_in_dom_h_)_&_(_for_x_being_set_st_x_in_dom_h_holds_
x_in_the_Tree_of_g_)_)
hereby ::_thesis: for x being set st x in dom h holds
x in the_Tree_of g
let x be set ; ::_thesis: ( x in the_Tree_of g implies b1 in dom h )
assume x in the_Tree_of g ; ::_thesis: b1 in dom h
then A30: x in ({g} /\ (the_Tree_of g)) \/ ((the_Tree_of g) \ {g}) by XBOOLE_1:51;
percases ( x in {g} /\ (the_Tree_of g) or x in the_proper_Tree_of g ) by A30, XBOOLE_0:def_3;
suppose x in {g} /\ (the_Tree_of g) ; ::_thesis: b1 in dom h
then ( x in {g} & {g} c= dom h ) by A28, XBOOLE_0:def_4, XBOOLE_1:7;
hence x in dom h ; ::_thesis: verum
end;
suppose x in the_proper_Tree_of g ; ::_thesis: b1 in dom h
then ( x in dom f & dom f c= dom h ) by A13, A27, XBOOLE_1:7;
hence x in dom h ; ::_thesis: verum
end;
end;
end;
hereby ::_thesis: verum
let x be set ; ::_thesis: ( x in dom h implies b1 in the_Tree_of g )
assume A31: x in dom h ; ::_thesis: b1 in the_Tree_of g
percases ( x = g or x in dom f ) by A31, A28, ZFMISC_1:136;
suppose x = g ; ::_thesis: b1 in the_Tree_of g
hence x in the_Tree_of g by Th24; ::_thesis: verum
end;
suppose x in dom f ; ::_thesis: b1 in the_Tree_of g
hence x in the_Tree_of g by A16; ::_thesis: verum
end;
end;
end;
end;
hence A32: dom h = the_Tree_of g by TARSKI:1; ::_thesis: S2[h]
thus S2[h] ::_thesis: verum
proof
let g1 be ConwayGame; ::_thesis: ( g1 in dom h implies h . g1 = F1(g1,(h | (the_proper_Tree_of g1))) )
assume A33: g1 in dom h ; ::_thesis: h . g1 = F1(g1,(h | (the_proper_Tree_of g1)))
now__::_thesis:_(_f_|_(the_proper_Tree_of_g1)_c=_h_|_(the_proper_Tree_of_g1)_&_dom_(f_|_(the_proper_Tree_of_g1))_=_the_proper_Tree_of_g1_&_dom_(h_|_(the_proper_Tree_of_g1))_=_the_proper_Tree_of_g1_)
thus f | (the_proper_Tree_of g1) c= h | (the_proper_Tree_of g1) by RELAT_1:76, XBOOLE_1:7; ::_thesis: ( dom (f | (the_proper_Tree_of g1)) = the_proper_Tree_of g1 & dom (h | (the_proper_Tree_of g1)) = the_proper_Tree_of g1 )
A34: the_proper_Tree_of g1 c= the_proper_Tree_of g by Th32, A32, A33;
then A35: the_proper_Tree_of g1 c= dom f by A13, XBOOLE_1:1;
thus dom (f | (the_proper_Tree_of g1)) = the_proper_Tree_of g1 by A34, A13, RELAT_1:62, XBOOLE_1:1; ::_thesis: dom (h | (the_proper_Tree_of g1)) = the_proper_Tree_of g1
f c= h by XBOOLE_1:7;
then dom f c= dom h by RELAT_1:11;
hence dom (h | (the_proper_Tree_of g1)) = the_proper_Tree_of g1 by A35, RELAT_1:62, XBOOLE_1:1; ::_thesis: verum
end;
then A36: h | (the_proper_Tree_of g1) = f | (the_proper_Tree_of g1) by GRFUNC_1:3;
percases ( g1 = g or g1 in dom f ) by A33, A28, ZFMISC_1:136;
supposeA37: g1 = g ; ::_thesis: h . g1 = F1(g1,(h | (the_proper_Tree_of g1)))
[g,F1(g,(f | (the_proper_Tree_of g)))] in h by ZFMISC_1:136;
hence h . g1 = F1(g1,(h | (the_proper_Tree_of g1))) by A36, A33, A37, FUNCT_1:def_2; ::_thesis: verum
end;
supposeA38: g1 in dom f ; ::_thesis: h . g1 = F1(g1,(h | (the_proper_Tree_of g1)))
f c= h by XBOOLE_1:7;
then f . g1 = h . g1 by A38, GRFUNC_1:2;
hence h . g1 = F1(g1,(h | (the_proper_Tree_of g1))) by A19, A38, A36; ::_thesis: verum
end;
end;
end;
end;
g in the_Tree_of g by Th24;
then h in FUNCS by A9, A29;
then h c= f by ZFMISC_1:74;
hence contradiction by A26, A28, RELAT_1:11, ZFMISC_1:39; ::_thesis: verum
end;
then A39: {g} c= dom f by ZFMISC_1:31;
the_Tree_of g = (the_proper_Tree_of g) \/ {g} by Th24, ZFMISC_1:116;
then the_Tree_of g c= dom f by A39, A13, XBOOLE_1:8;
hence dom f = the_Tree_of g by A16, XBOOLE_0:def_10; ::_thesis: S2[f]
thus S2[f] by A19; ::_thesis: verum
end;
for g being ConwayGame holds S3[g] from CGAMES_1:sch_3(A7);
hence 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))) ) ) ; ::_thesis: verum
end;
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 <> {} } )
proof
let g1 be ConwayGame; ::_thesis: 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 <> {} } )
let f be Function; ::_thesis: ( { ((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 <> {} } )
set R1 = { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } ;
set R2 = { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } ;
set L1 = { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ;
set L2 = { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ;
A1: for gO being ConwayGame st ( gO in the_LeftOptions_of g1 or gO in the_RightOptions_of g1 ) holds
(f | (the_proper_Tree_of g1)) . gO = f . gO
proof
let gO be ConwayGame; ::_thesis: ( ( gO in the_LeftOptions_of g1 or gO in the_RightOptions_of g1 ) implies (f | (the_proper_Tree_of g1)) . gO = f . gO )
assume ( gO in the_LeftOptions_of g1 or gO in the_RightOptions_of g1 ) ; ::_thesis: (f | (the_proper_Tree_of g1)) . gO = f . gO
then ( gO in the_Options_of g1 & the_Options_of g1 c= the_proper_Tree_of g1 ) by Th33, XBOOLE_0:def_3;
hence (f | (the_proper_Tree_of g1)) . gO = f . gO by FUNCT_1:49; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_set_st_x_in__{__((f_|_(the_proper_Tree_of_g1))_._gR)_where_gR_is_Element_of_the_RightOptions_of_g1_:_the_RightOptions_of_g1_<>_{}__}__holds_
x_in__{__(f_._gR)_where_gR_is_Element_of_the_RightOptions_of_g1_:_the_RightOptions_of_g1_<>_{}__}__)_&_(_for_x_being_set_st_x_in__{__(f_._gR)_where_gR_is_Element_of_the_RightOptions_of_g1_:_the_RightOptions_of_g1_<>_{}__}__holds_
x_in__{__((f_|_(the_proper_Tree_of_g1))_._gR)_where_gR_is_Element_of_the_RightOptions_of_g1_:_the_RightOptions_of_g1_<>_{}__}__)_)
hereby ::_thesis: for x being set st x in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } holds
x in { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} }
let x be set ; ::_thesis: ( x in { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } implies x in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } )
assume x in { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } ; ::_thesis: x in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} }
then consider gR being Element of the_RightOptions_of g1 such that
A2: ( x = (f | (the_proper_Tree_of g1)) . gR & the_RightOptions_of g1 <> {} ) ;
( gR in the_RightOptions_of g1 & gR is ConwayGame ) by A2, Th18;
then (f | (the_proper_Tree_of g1)) . gR = f . gR by A1;
hence x in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } by A2; ::_thesis: verum
end;
hereby ::_thesis: verum
let x be set ; ::_thesis: ( x in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } implies x in { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } )
assume x in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } ; ::_thesis: x in { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} }
then consider gR being Element of the_RightOptions_of g1 such that
A3: ( x = f . gR & the_RightOptions_of g1 <> {} ) ;
( gR in the_RightOptions_of g1 & gR is ConwayGame ) by A3, Th18;
then (f | (the_proper_Tree_of g1)) . gR = f . gR by A1;
hence x in { ((f | (the_proper_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } by A3; ::_thesis: verum
end;
end;
hence { ((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 <> {} } by TARSKI:1; ::_thesis: { ((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 <> {} }
now__::_thesis:_(_(_for_x_being_set_st_x_in__{__((f_|_(the_proper_Tree_of_g1))_._gL)_where_gL_is_Element_of_the_LeftOptions_of_g1_:_the_LeftOptions_of_g1_<>_{}__}__holds_
x_in__{__(f_._gL)_where_gL_is_Element_of_the_LeftOptions_of_g1_:_the_LeftOptions_of_g1_<>_{}__}__)_&_(_for_x_being_set_st_x_in__{__(f_._gL)_where_gL_is_Element_of_the_LeftOptions_of_g1_:_the_LeftOptions_of_g1_<>_{}__}__holds_
x_in__{__((f_|_(the_proper_Tree_of_g1))_._gL)_where_gL_is_Element_of_the_LeftOptions_of_g1_:_the_LeftOptions_of_g1_<>_{}__}__)_)
hereby ::_thesis: for x being set st x in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } holds
x in { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} }
let x be set ; ::_thesis: ( x in { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } implies x in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } )
assume x in { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ; ::_thesis: x in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} }
then consider gL being Element of the_LeftOptions_of g1 such that
A4: ( x = (f | (the_proper_Tree_of g1)) . gL & the_LeftOptions_of g1 <> {} ) ;
( gL in the_LeftOptions_of g1 & gL is ConwayGame ) by A4, Th18;
then (f | (the_proper_Tree_of g1)) . gL = f . gL by A1;
hence x in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } by A4; ::_thesis: verum
end;
hereby ::_thesis: verum
let x be set ; ::_thesis: ( x in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } implies x in { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } )
assume x in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ; ::_thesis: x in { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} }
then consider gL being Element of the_LeftOptions_of g1 such that
A5: ( x = f . gL & the_LeftOptions_of g1 <> {} ) ;
( gL in the_LeftOptions_of g1 & gL is ConwayGame ) by A5, Th18;
then (f | (the_proper_Tree_of g1)) . gL = f . gL by A1;
hence x in { ((f | (the_proper_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } by A5; ::_thesis: verum
end;
end;
hence { ((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 <> {} } by TARSKI:1; ::_thesis: verum
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
deffunc H2( ConwayGame, Function) -> left-right = left-right(# { ($2 . gR) where gR is Element of the_RightOptions_of $1 : the_RightOptions_of $1 <> {} } , { ($2 . gL) where gL is Element of the_LeftOptions_of $1 : the_LeftOptions_of $1 <> {} } #);
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 = H2(g1,f | (the_proper_Tree_of g1)) ) ) from CGAMES_1:sch_6();
then consider f being Function such that
A1: ( dom f = the_Tree_of g & ( for g1 being ConwayGame st g1 in dom f holds
f . g1 = H2(g1,f | (the_proper_Tree_of g1)) ) ) ;
take v = f . g; ::_thesis: ex f being Function st
( dom f = the_Tree_of g & v = 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 <> {} } #) ) )
take f ; ::_thesis: ( dom f = the_Tree_of g & v = 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 <> {} } #) ) )
thus dom f = the_Tree_of g by A1; ::_thesis: ( v = 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 <> {} } #) ) )
thus f . g = v ; ::_thesis: 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 <> {} } #)
let g1 be ConwayGame; ::_thesis: ( g1 in dom f implies 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 <> {} } #) )
assume A2: g1 in dom f ; ::_thesis: 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 <> {} } #)
( { ((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 <> {} } ) by Lm3;
hence 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 <> {} } #) by A1, A2; ::_thesis: verum
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
deffunc H2( ConwayGame, Function) -> left-right = left-right(# { ($2 . gR) where gR is Element of the_RightOptions_of $1 : the_RightOptions_of $1 <> {} } , { ($2 . gL) where gL is Element of the_LeftOptions_of $1 : the_LeftOptions_of $1 <> {} } #);
let g1, g2 be set ; ::_thesis: ( ex f being Function st
( dom f = the_Tree_of g & g1 = 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 & g2 = 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 <> {} } #) ) ) implies g1 = g2 )
assume ex f1 being Function st
( dom f1 = the_Tree_of g & g1 = f1 . g & ( for g0 being ConwayGame st g0 in dom f1 holds
f1 . g0 = H2(g0,f1) ) ) ; ::_thesis: ( for f being Function holds
( not dom f = the_Tree_of g or not g2 = f . g or ex g1 being ConwayGame st
( g1 in dom f & not 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 <> {} } #) ) ) or g1 = g2 )
then consider f1 being Function such that
A3: ( dom f1 = the_Tree_of g & g1 = f1 . g & ( for g0 being ConwayGame st g0 in dom f1 holds
f1 . g0 = H2(g0,f1) ) ) ;
assume ex f2 being Function st
( dom f2 = the_Tree_of g & g2 = f2 . g & ( for g0 being ConwayGame st g0 in dom f2 holds
f2 . g0 = H2(g0,f2) ) ) ; ::_thesis: g1 = g2
then consider f2 being Function such that
A4: ( dom f2 = the_Tree_of g & g2 = f2 . g & ( for g0 being ConwayGame st g0 in dom f2 holds
f2 . g0 = H2(g0,f2) ) ) ;
A5: for g0 being ConwayGame st g0 in dom f1 holds
f1 . g0 = H2(g0,f1 | (the_proper_Tree_of g0))
proof
let g0 be ConwayGame; ::_thesis: ( g0 in dom f1 implies f1 . g0 = H2(g0,f1 | (the_proper_Tree_of g0)) )
set LOr = { ((f1 | (the_proper_Tree_of g0)) . gR) where gR is Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} } ;
set ROr = { ((f1 | (the_proper_Tree_of g0)) . gL) where gL is Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} } ;
set LOu = { (f1 . gR) where gR is Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} } ;
set ROu = { (f1 . gL) where gL is Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} } ;
( { (f1 . gR) where gR is Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} } = { ((f1 | (the_proper_Tree_of g0)) . gR) where gR is Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} } & { (f1 . gL) where gL is Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} } = { ((f1 | (the_proper_Tree_of g0)) . gL) where gL is Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} } ) by Lm3;
hence ( g0 in dom f1 implies f1 . g0 = H2(g0,f1 | (the_proper_Tree_of g0)) ) by A3; ::_thesis: verum
end;
A6: for g0 being ConwayGame st g0 in dom f2 holds
f2 . g0 = H2(g0,f2 | (the_proper_Tree_of g0))
proof
let g0 be ConwayGame; ::_thesis: ( g0 in dom f2 implies f2 . g0 = H2(g0,f2 | (the_proper_Tree_of g0)) )
set LOr = { ((f2 | (the_proper_Tree_of g0)) . gR) where gR is Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} } ;
set ROr = { ((f2 | (the_proper_Tree_of g0)) . gL) where gL is Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} } ;
set LOu = { (f2 . gR) where gR is Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} } ;
set ROu = { (f2 . gL) where gL is Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} } ;
( { (f2 . gR) where gR is Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} } = { ((f2 | (the_proper_Tree_of g0)) . gR) where gR is Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} } & { (f2 . gL) where gL is Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} } = { ((f2 | (the_proper_Tree_of g0)) . gL) where gL is Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} } ) by Lm3;
hence ( g0 in dom f2 implies f2 . g0 = H2(g0,f2 | (the_proper_Tree_of g0)) ) by A4; ::_thesis: verum
end;
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 = H2(g1,f1 | (the_proper_Tree_of g1)) ) & ( for g1 being ConwayGame st g1 in dom f2 holds
f2 . g1 = H2(g1,f2 | (the_proper_Tree_of g1)) ) holds
f1 = f2 from CGAMES_1:sch_5();
hence g1 = g2 by A3, A4, A5, A6; ::_thesis: verum
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
consider f being Function such that
A1: ( dom f = the_Tree_of g & - g = 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 <> {} } #) ) ) by Def14;
defpred S2[ ConwayGame] means ( g in dom f implies f . g is ConwayGame );
A2: for g1 being ConwayGame st ( for gO being ConwayGame st gO in the_Options_of g1 holds
S2[gO] ) holds
S2[g1]
proof
let g1 be ConwayGame; ::_thesis: ( ( for gO being ConwayGame st gO in the_Options_of g1 holds
S2[gO] ) implies S2[g1] )
assume A3: for gO being ConwayGame st gO in the_Options_of g1 holds
S2[gO] ; ::_thesis: S2[g1]
assume A4: g1 in dom f ; ::_thesis: f . g1 is ConwayGame
set L = { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } ;
set R = { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ;
A5: 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 <> {} } #) by A1, A4;
now__::_thesis:_for_z_being_set_st_z_in__{__(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_
z_is_ConwayGame
let z be set ; ::_thesis: ( z in { (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 <> {} } implies z is ConwayGame )
assume A6: z in { (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 <> {} } ; ::_thesis: z is ConwayGame
ex gO being ConwayGame st
( gO in the_Options_of g1 & z = f . gO )
proof
percases ( z in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } or z in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ) by A6, XBOOLE_0:def_3;
suppose z in { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } ; ::_thesis: ex gO being ConwayGame st
( gO in the_Options_of g1 & z = f . gO )
then consider gR being Element of the_RightOptions_of g1 such that
A7: ( z = f . gR & the_RightOptions_of g1 <> {} ) ;
reconsider gO = gR as ConwayGame by Th18, A7;
take gO ; ::_thesis: ( gO in the_Options_of g1 & z = f . gO )
thus ( gO in the_Options_of g1 & z = f . gO ) by A7, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose z in { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } ; ::_thesis: ex gO being ConwayGame st
( gO in the_Options_of g1 & z = f . gO )
then consider gL being Element of the_LeftOptions_of g1 such that
A8: ( z = f . gL & the_LeftOptions_of g1 <> {} ) ;
reconsider gO = gL as ConwayGame by Th18, A8;
take gO ; ::_thesis: ( gO in the_Options_of g1 & z = f . gO )
thus ( gO in the_Options_of g1 & z = f . gO ) by A8, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
then consider gO being ConwayGame such that
A9: ( gO in the_Options_of g1 & z = f . gO ) ;
( the_Options_of g1 c= the_Tree_of g1 & the_Tree_of g1 c= dom f ) by Th34, Th31, A4, A1;
then the_Options_of g1 c= dom f by XBOOLE_1:1;
hence z is ConwayGame by A3, A9; ::_thesis: verum
end;
hence f . g1 is ConwayGame by A5, Th19; ::_thesis: verum
end;
A10: for g being ConwayGame holds S2[g] from CGAMES_1:sch_3(A2);
g in the_Tree_of g by Th24;
hence - g is ConwayGame-like by A1, A10; ::_thesis: verum
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
let g be ConwayGame; ::_thesis: 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
let f be Function; ::_thesis: ( 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 <> {} } #) ) implies for g1 being ConwayGame st g1 in dom f holds
f . g1 = - g1 )
assume A1: ( 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 <> {} } #) ) ) ; ::_thesis: for g1 being ConwayGame st g1 in dom f holds
f . g1 = - g1
let g1 be ConwayGame; ::_thesis: ( g1 in dom f implies f . g1 = - g1 )
assume A2: g1 in dom f ; ::_thesis: f . g1 = - g1
set f1 = f | (the_Tree_of g1);
A3: dom (f | (the_Tree_of g1)) = the_Tree_of g1 by A1, A2, Th31, RELAT_1:62;
now__::_thesis:_for_g2_being_ConwayGame_st_g2_in_dom_(f_|_(the_Tree_of_g1))_holds_
(f_|_(the_Tree_of_g1))_._g2_=_left-right(#__{__((f_|_(the_Tree_of_g1))_._gR)_where_gR_is_Element_of_the_RightOptions_of_g2_:_the_RightOptions_of_g2_<>_{}__}__,_{__((f_|_(the_Tree_of_g1))_._gL)_where_gL_is_Element_of_the_LeftOptions_of_g2_:_the_LeftOptions_of_g2_<>_{}__}__#)
let g2 be ConwayGame; ::_thesis: ( g2 in dom (f | (the_Tree_of g1)) implies (f | (the_Tree_of g1)) . g2 = left-right(# { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } , { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } #) )
assume A4: g2 in dom (f | (the_Tree_of g1)) ; ::_thesis: (f | (the_Tree_of g1)) . g2 = left-right(# { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } , { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } #)
set L = { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } ;
set L1 = { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } ;
set R = { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } ;
set R1 = { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } ;
dom (f | (the_Tree_of g1)) c= dom f by RELAT_1:60;
then A5: f . g2 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } #) by A1, A4;
A6: for gO being ConwayGame st ( gO in the_LeftOptions_of g2 or gO in the_RightOptions_of g2 ) holds
(f | (the_Tree_of g1)) . gO = f . gO
proof
let gO be ConwayGame; ::_thesis: ( ( gO in the_LeftOptions_of g2 or gO in the_RightOptions_of g2 ) implies (f | (the_Tree_of g1)) . gO = f . gO )
assume ( gO in the_LeftOptions_of g2 or gO in the_RightOptions_of g2 ) ; ::_thesis: (f | (the_Tree_of g1)) . gO = f . gO
then ( gO in the_Options_of g2 & the_Options_of g2 c= the_Tree_of g2 ) by Th34, XBOOLE_0:def_3;
then ( gO in the_Tree_of g2 & the_Tree_of g2 c= dom (f | (the_Tree_of g1)) ) by Th31, A4, A3;
hence (f | (the_Tree_of g1)) . gO = f . gO by FUNCT_1:47; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_set_st_x_in__{__(f_._gR)_where_gR_is_Element_of_the_RightOptions_of_g2_:_the_RightOptions_of_g2_<>_{}__}__holds_
x_in__{__((f_|_(the_Tree_of_g1))_._gR)_where_gR_is_Element_of_the_RightOptions_of_g2_:_the_RightOptions_of_g2_<>_{}__}__)_&_(_for_x_being_set_st_x_in__{__((f_|_(the_Tree_of_g1))_._gR)_where_gR_is_Element_of_the_RightOptions_of_g2_:_the_RightOptions_of_g2_<>_{}__}__holds_
x_in__{__(f_._gR)_where_gR_is_Element_of_the_RightOptions_of_g2_:_the_RightOptions_of_g2_<>_{}__}__)_)
hereby ::_thesis: for x being set st x in { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } holds
x in { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} }
let x be set ; ::_thesis: ( x in { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } implies x in { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } )
assume x in { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } ; ::_thesis: x in { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} }
then consider gR being Element of the_RightOptions_of g2 such that
A7: ( x = f . gR & the_RightOptions_of g2 <> {} ) ;
( gR in the_RightOptions_of g2 & gR is ConwayGame ) by A7, Th18;
then (f | (the_Tree_of g1)) . gR = f . gR by A6;
hence x in { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } by A7; ::_thesis: verum
end;
hereby ::_thesis: verum
let x be set ; ::_thesis: ( x in { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } implies x in { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } )
assume x in { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } ; ::_thesis: x in { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} }
then consider gR being Element of the_RightOptions_of g2 such that
A8: ( x = (f | (the_Tree_of g1)) . gR & the_RightOptions_of g2 <> {} ) ;
( gR in the_RightOptions_of g2 & gR is ConwayGame ) by A8, Th18;
then (f | (the_Tree_of g1)) . gR = f . gR by A6;
hence x in { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } by A8; ::_thesis: verum
end;
end;
then A9: { (f . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } = { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } by TARSKI:1;
now__::_thesis:_(_(_for_x_being_set_st_x_in__{__(f_._gL)_where_gL_is_Element_of_the_LeftOptions_of_g2_:_the_LeftOptions_of_g2_<>_{}__}__holds_
x_in__{__((f_|_(the_Tree_of_g1))_._gL)_where_gL_is_Element_of_the_LeftOptions_of_g2_:_the_LeftOptions_of_g2_<>_{}__}__)_&_(_for_x_being_set_st_x_in__{__((f_|_(the_Tree_of_g1))_._gL)_where_gL_is_Element_of_the_LeftOptions_of_g2_:_the_LeftOptions_of_g2_<>_{}__}__holds_
x_in__{__(f_._gL)_where_gL_is_Element_of_the_LeftOptions_of_g2_:_the_LeftOptions_of_g2_<>_{}__}__)_)
hereby ::_thesis: for x being set st x in { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } holds
x in { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} }
let x be set ; ::_thesis: ( x in { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } implies x in { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } )
assume x in { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } ; ::_thesis: x in { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} }
then consider gL being Element of the_LeftOptions_of g2 such that
A10: ( x = f . gL & the_LeftOptions_of g2 <> {} ) ;
( gL in the_LeftOptions_of g2 & gL is ConwayGame ) by A10, Th18;
then (f | (the_Tree_of g1)) . gL = f . gL by A6;
hence x in { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } by A10; ::_thesis: verum
end;
hereby ::_thesis: verum
let x be set ; ::_thesis: ( x in { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } implies x in { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } )
assume x in { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } ; ::_thesis: x in { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} }
then consider gL being Element of the_LeftOptions_of g2 such that
A11: ( x = (f | (the_Tree_of g1)) . gL & the_LeftOptions_of g2 <> {} ) ;
( gL in the_LeftOptions_of g2 & gL is ConwayGame ) by A11, Th18;
then (f | (the_Tree_of g1)) . gL = f . gL by A6;
hence x in { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } by A11; ::_thesis: verum
end;
end;
then { (f . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } = { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } by TARSKI:1;
hence (f | (the_Tree_of g1)) . g2 = left-right(# { ((f | (the_Tree_of g1)) . gR) where gR is Element of the_RightOptions_of g2 : the_RightOptions_of g2 <> {} } , { ((f | (the_Tree_of g1)) . gL) where gL is Element of the_LeftOptions_of g2 : the_LeftOptions_of g2 <> {} } #) by A4, A5, A9, FUNCT_1:47; ::_thesis: verum
end;
then ( (f | (the_Tree_of g1)) . g1 = - g1 & g1 in dom (f | (the_Tree_of g1)) ) by Def14, A3, Th24;
hence f . g1 = - g1 by FUNCT_1:47; ::_thesis: verum
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
let g be ConwayGame; ::_thesis: ( ( 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 ) ) ) )
consider f being Function such that
A1: ( dom f = the_Tree_of g & f . g = - 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 <> {} } #) ) ) by Def14;
A2: for gO being ConwayGame st ( gO in the_RightOptions_of g or gO in the_LeftOptions_of g ) holds
f . gO = - gO
proof
let gO be ConwayGame; ::_thesis: ( ( gO in the_RightOptions_of g or gO in the_LeftOptions_of g ) implies f . gO = - gO )
assume ( gO in the_RightOptions_of g or gO in the_LeftOptions_of g ) ; ::_thesis: f . gO = - gO
then ( gO in the_Options_of g & the_Options_of g c= the_Tree_of g ) by Th34, XBOOLE_0:def_3;
hence f . gO = - gO by Lm4, A1; ::_thesis: verum
end;
set L = { (f . gR) where gR is Element of the_RightOptions_of g : the_RightOptions_of g <> {} } ;
set R = { (f . gL) where gL is Element of the_LeftOptions_of g : the_LeftOptions_of g <> {} } ;
- g = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g : the_RightOptions_of g <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g : the_LeftOptions_of g <> {} } #) by A1, Th24;
then A3: ( the_LeftOptions_of (- g) = { (f . gR) where gR is Element of the_RightOptions_of g : the_RightOptions_of g <> {} } & the_RightOptions_of (- g) = { (f . gL) where gL is Element of the_LeftOptions_of g : the_LeftOptions_of g <> {} } ) by Def6, Def7;
hereby ::_thesis: 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 ) )
let x be set ; ::_thesis: ( ( x in the_LeftOptions_of (- g) implies ex gR being ConwayGame st
( gR in the_RightOptions_of g & x = - gR ) ) & ( ex gR being ConwayGame st
( gR in the_RightOptions_of g & x = - gR ) implies x in the_LeftOptions_of (- g) ) )
hereby ::_thesis: ( ex gR being ConwayGame st
( gR in the_RightOptions_of g & x = - gR ) implies x in the_LeftOptions_of (- g) )
assume x in the_LeftOptions_of (- g) ; ::_thesis: ex gR being ConwayGame st
( gR in the_RightOptions_of g & x = - gR )
then consider gR0 being Element of the_RightOptions_of g such that
A4: ( x = f . gR0 & the_RightOptions_of g <> {} ) by A3;
reconsider gR = gR0 as ConwayGame by Th18, A4;
take gR = gR; ::_thesis: ( gR in the_RightOptions_of g & x = - gR )
thus ( gR in the_RightOptions_of g & x = - gR ) by A4, A2; ::_thesis: verum
end;
hereby ::_thesis: verum
assume ex gR being ConwayGame st
( gR in the_RightOptions_of g & x = - gR ) ; ::_thesis: x in the_LeftOptions_of (- g)
then consider gR being ConwayGame such that
A5: ( x = - gR & gR in the_RightOptions_of g ) ;
f . gR = - gR by A2, A5;
hence x in the_LeftOptions_of (- g) by A3, A5; ::_thesis: verum
end;
end;
hereby ::_thesis: verum
let x be set ; ::_thesis: ( ( x in the_RightOptions_of (- g) implies ex gL being ConwayGame st
( gL in the_LeftOptions_of g & x = - gL ) ) & ( ex gL being ConwayGame st
( gL in the_LeftOptions_of g & x = - gL ) implies x in the_RightOptions_of (- g) ) )
hereby ::_thesis: ( ex gL being ConwayGame st
( gL in the_LeftOptions_of g & x = - gL ) implies x in the_RightOptions_of (- g) )
assume x in the_RightOptions_of (- g) ; ::_thesis: ex gL being ConwayGame st
( gL in the_LeftOptions_of g & x = - gL )
then consider gL0 being Element of the_LeftOptions_of g such that
A6: ( x = f . gL0 & the_LeftOptions_of g <> {} ) by A3;
reconsider gL = gL0 as ConwayGame by Th18, A6;
take gL = gL; ::_thesis: ( gL in the_LeftOptions_of g & x = - gL )
thus ( gL in the_LeftOptions_of g & x = - gL ) by A6, A2; ::_thesis: verum
end;
hereby ::_thesis: verum
assume ex gL being ConwayGame st
( gL in the_LeftOptions_of g & x = - gL ) ; ::_thesis: x in the_RightOptions_of (- g)
then consider gL being ConwayGame such that
A7: ( x = - gL & gL in the_LeftOptions_of g ) ;
f . gL = - gL by A2, A7;
hence x in the_RightOptions_of (- g) by A3, A7; ::_thesis: verum
end;
end;
end;
theorem Th40: :: CGAMES_1:40
for g being ConwayGame holds - (- g) = g
proof
let g be ConwayGame; ::_thesis: - (- g) = g
defpred S2[ ConwayGame] means - (- $1) <> $1;
assume not - (- g) = g ; ::_thesis: contradiction
then A1: ex g being ConwayGame st S2[g] ;
consider g being ConwayGame such that
A2: ( S2[g] & ( for gO being ConwayGame st gO in the_Options_of g holds
not S2[gO] ) ) from CGAMES_1:sch_2(A1);
now__::_thesis:_(_(_for_x_being_set_st_x_in_the_LeftOptions_of_(-_(-_g))_holds_
x_in_the_LeftOptions_of_g_)_&_(_for_x_being_set_st_x_in_the_LeftOptions_of_g_holds_
x_in_the_LeftOptions_of_(-_(-_g))_)_)
hereby ::_thesis: for x being set st x in the_LeftOptions_of g holds
x in the_LeftOptions_of (- (- g))
let x be set ; ::_thesis: ( x in the_LeftOptions_of (- (- g)) implies x in the_LeftOptions_of g )
assume x in the_LeftOptions_of (- (- g)) ; ::_thesis: x in the_LeftOptions_of g
then consider gR being ConwayGame such that
A3: ( gR in the_RightOptions_of (- g) & x = - gR ) by Th39;
consider gL being ConwayGame such that
A4: ( gL in the_LeftOptions_of g & gR = - gL ) by Th39, A3;
gL in the_Options_of g by A4, XBOOLE_0:def_3;
hence x in the_LeftOptions_of g by A2, A3, A4; ::_thesis: verum
end;
hereby ::_thesis: verum
let x be set ; ::_thesis: ( x in the_LeftOptions_of g implies x in the_LeftOptions_of (- (- g)) )
assume A5: x in the_LeftOptions_of g ; ::_thesis: x in the_LeftOptions_of (- (- g))
reconsider gL = x as ConwayGame by Th18, A5;
( - gL in the_RightOptions_of (- g) & gL in the_Options_of g ) by Th39, A5, XBOOLE_0:def_3;
then ( - (- gL) in the_LeftOptions_of (- (- g)) & - (- gL) = gL ) by Th39, A2;
hence x in the_LeftOptions_of (- (- g)) ; ::_thesis: verum
end;
end;
then A6: the_LeftOptions_of (- (- g)) = the_LeftOptions_of g by TARSKI:1;
now__::_thesis:_(_(_for_x_being_set_st_x_in_the_RightOptions_of_(-_(-_g))_holds_
x_in_the_RightOptions_of_g_)_&_(_for_x_being_set_st_x_in_the_RightOptions_of_g_holds_
x_in_the_RightOptions_of_(-_(-_g))_)_)
hereby ::_thesis: for x being set st x in the_RightOptions_of g holds
x in the_RightOptions_of (- (- g))
let x be set ; ::_thesis: ( x in the_RightOptions_of (- (- g)) implies x in the_RightOptions_of g )
assume x in the_RightOptions_of (- (- g)) ; ::_thesis: x in the_RightOptions_of g
then consider gL being ConwayGame such that
A7: ( gL in the_LeftOptions_of (- g) & x = - gL ) by Th39;
consider gR being ConwayGame such that
A8: ( gR in the_RightOptions_of g & gL = - gR ) by Th39, A7;
gR in the_Options_of g by A8, XBOOLE_0:def_3;
hence x in the_RightOptions_of g by A2, A7, A8; ::_thesis: verum
end;
hereby ::_thesis: verum
let x be set ; ::_thesis: ( x in the_RightOptions_of g implies x in the_RightOptions_of (- (- g)) )
assume A9: x in the_RightOptions_of g ; ::_thesis: x in the_RightOptions_of (- (- g))
reconsider gR = x as ConwayGame by Th18, A9;
( - gR in the_LeftOptions_of (- g) & gR in the_Options_of g ) by Th39, A9, XBOOLE_0:def_3;
then ( - (- gR) in the_RightOptions_of (- (- g)) & - (- gR) = gR ) by Th39, A2;
hence x in the_RightOptions_of (- (- g)) ; ::_thesis: verum
end;
end;
then the_RightOptions_of (- (- g)) = the_RightOptions_of g by TARSKI:1;
hence contradiction by A2, A6, Th5; ::_thesis: verum
end;
theorem :: CGAMES_1:41
for gO, g 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
let gO, g be ConwayGame; ::_thesis: ( ( 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 ) )
( g = - (- g) & gO = - (- gO) ) by Th40;
hence ( ( 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 ) ) by Th39; ::_thesis: verum
end;
definition
let g be ConwayGame;
attrg is nonnegative means :Def15: :: 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 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 ) ) ) );
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 & g is nonpositive );
attrg is fuzzy means :Def18: :: CGAMES_1:def 18
( not g is nonnegative & 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 & 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 ) );
definition
let g be ConwayGame;
attrg is positive means :Def19: :: CGAMES_1:def 19
( g is nonnegative & not g is zero );
attrg is negative means :Def20: :: CGAMES_1:def 20
( g is nonpositive & 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 & 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 ) );
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 ) by Def17;
cluster ConwayGame-like nonnegative nonpositive -> zero for set ;
coherence
for b1 being ConwayGame st b1 is nonpositive & 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 & not b1 is zero ) by Def20;
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 by Def20;
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 ) by Def19;
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 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 & 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 & 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 )
proof
let g be ConwayGame; ::_thesis: ( g is zero or g is positive or g is negative or g is fuzzy )
assume ( not g is zero & not g is positive & not g is negative ) ; ::_thesis: g is fuzzy
then ( not g is nonnegative & not g is nonpositive ) ;
hence g is fuzzy ; ::_thesis: verum
end;
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
let g be ConwayGame; ::_thesis: ( 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 ) )
defpred S2[ set ] means for g being ConwayGame st g in $1 holds
for gR being ConwayGame st gR in the_RightOptions_of g holds
ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL in $1 );
A1: for s being set
for alpha being Ordinal st S2[s] holds
S2[s /\ (ConwayDay alpha)]
proof
let s be set ; ::_thesis: for alpha being Ordinal st S2[s] holds
S2[s /\ (ConwayDay alpha)]
let alpha be Ordinal; ::_thesis: ( S2[s] implies S2[s /\ (ConwayDay alpha)] )
assume A2: S2[s] ; ::_thesis: S2[s /\ (ConwayDay alpha)]
let g be ConwayGame; ::_thesis: ( g in s /\ (ConwayDay alpha) implies for gR being ConwayGame st gR in the_RightOptions_of g holds
ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL in s /\ (ConwayDay alpha) ) )
assume g in s /\ (ConwayDay alpha) ; ::_thesis: for gR being ConwayGame st gR in the_RightOptions_of g holds
ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL in s /\ (ConwayDay alpha) )
then A3: ( g in s & g in ConwayDay alpha ) by XBOOLE_0:def_4;
let gR be ConwayGame; ::_thesis: ( gR in the_RightOptions_of g implies ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL in s /\ (ConwayDay alpha) ) )
assume A4: gR in the_RightOptions_of g ; ::_thesis: ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL in s /\ (ConwayDay alpha) )
then consider gRL being ConwayGame such that
A5: ( gRL in the_LeftOptions_of gR & gRL in s ) by A2, A3;
take gRL ; ::_thesis: ( gRL in the_LeftOptions_of gR & gRL in s /\ (ConwayDay alpha) )
gR in ConwayDay alpha by Th11, A3, A4;
then gRL in ConwayDay alpha by Th11, A5;
hence ( gRL in the_LeftOptions_of gR & gRL in s /\ (ConwayDay alpha) ) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
hereby ::_thesis: ( ( 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 ) ) implies g is nonnegative )
assume g is nonnegative ; ::_thesis: 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 )
then consider s being set such that
A6: ( g in s & S2[s] ) by Def15;
let gR be ConwayGame; ::_thesis: ( gR in the_RightOptions_of g implies ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL is nonnegative ) )
assume gR in the_RightOptions_of g ; ::_thesis: ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL is nonnegative )
then consider gRL being ConwayGame such that
A7: ( gRL in the_LeftOptions_of gR & gRL in s ) by A6;
take gRL = gRL; ::_thesis: ( gRL in the_LeftOptions_of gR & gRL is nonnegative )
thus gRL in the_LeftOptions_of gR by A7; ::_thesis: gRL is nonnegative
thus gRL is nonnegative ::_thesis: verum
proof
take s ; :: according to CGAMES_1:def_15 ::_thesis: ( gRL 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 ) ) )
thus ( gRL 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 ) ) ) by A6, A7; ::_thesis: verum
end;
end;
hereby ::_thesis: verum
assume A8: 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 ) ; ::_thesis: g is nonnegative
consider alpha being Ordinal such that
A9: g in ConwayDay alpha by Def3;
now__::_thesis:_ex_s_being_set_st_
(_g_in_s_&_S2[s]_)
set ss = { s1 where s1 is Subset of (ConwayDay alpha) : S2[s1] } ;
take s = union { s1 where s1 is Subset of (ConwayDay alpha) : S2[s1] } ; ::_thesis: ( g in s & S2[s] )
A10: S2[s]
proof
let g1 be ConwayGame; ::_thesis: ( g1 in s implies 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 ) )
assume g1 in s ; ::_thesis: 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 )
then consider s2 being set such that
A11: ( g1 in s2 & s2 in { s1 where s1 is Subset of (ConwayDay alpha) : S2[s1] } ) by TARSKI:def_4;
consider s1 being Subset of (ConwayDay alpha) such that
A12: ( s1 = s2 & S2[s1] ) by A11;
let gR be ConwayGame; ::_thesis: ( gR in the_RightOptions_of g1 implies ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL in s ) )
assume gR in the_RightOptions_of g1 ; ::_thesis: ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL in s )
then consider gRL being ConwayGame such that
A13: ( gRL in the_LeftOptions_of gR & gRL in s1 ) by A11, A12;
take gRL ; ::_thesis: ( gRL in the_LeftOptions_of gR & gRL in s )
s2 c= s by A11, ZFMISC_1:74;
hence ( gRL in the_LeftOptions_of gR & gRL in s ) by A12, A13; ::_thesis: verum
end;
thus g in s ::_thesis: S2[s]
proof
now__::_thesis:_for_x_being_set_st_x_in__{__s1_where_s1_is_Subset_of_(ConwayDay_alpha)_:_S2[s1]__}__holds_
x_c=_ConwayDay_alpha
let x be set ; ::_thesis: ( x in { s1 where s1 is Subset of (ConwayDay alpha) : S2[s1] } implies x c= ConwayDay alpha )
assume x in { s1 where s1 is Subset of (ConwayDay alpha) : S2[s1] } ; ::_thesis: x c= ConwayDay alpha
then ex s1 being Subset of (ConwayDay alpha) st
( x = s1 & S2[s1] ) ;
hence x c= ConwayDay alpha ; ::_thesis: verum
end;
then A14: s c= ConwayDay alpha by ZFMISC_1:76;
{g} c= ConwayDay alpha by A9, ZFMISC_1:31;
then reconsider sg = s \/ {g} as Subset of (ConwayDay alpha) by A14, XBOOLE_1:8;
S2[sg]
proof
let g1 be ConwayGame; ::_thesis: ( g1 in sg implies 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 sg ) )
assume A15: g1 in sg ; ::_thesis: 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 sg )
let gR be ConwayGame; ::_thesis: ( gR in the_RightOptions_of g1 implies ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL in sg ) )
assume A16: gR in the_RightOptions_of g1 ; ::_thesis: ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL in sg )
percases ( g1 in s or g1 in {g} ) by A15, XBOOLE_0:def_3;
suppose g1 in s ; ::_thesis: ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL in sg )
then consider gRL being ConwayGame such that
A17: ( gRL in the_LeftOptions_of gR & gRL in s ) by A10, A16;
take gRL ; ::_thesis: ( gRL in the_LeftOptions_of gR & gRL in sg )
thus gRL in the_LeftOptions_of gR by A17; ::_thesis: gRL in sg
s c= sg by XBOOLE_1:7;
hence gRL in sg by A17; ::_thesis: verum
end;
suppose g1 in {g} ; ::_thesis: ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL in sg )
then g1 = g by TARSKI:def_1;
then consider gRL being ConwayGame such that
A18: ( gRL in the_LeftOptions_of gR & gRL is nonnegative ) by A8, A16;
consider s0 being set such that
A19: ( gRL in s0 & S2[s0] ) by Def15, A18;
take gRL ; ::_thesis: ( gRL in the_LeftOptions_of gR & gRL in sg )
thus gRL in the_LeftOptions_of gR by A18; ::_thesis: gRL in sg
reconsider s1 = s0 /\ (ConwayDay alpha) as Subset of (ConwayDay alpha) by XBOOLE_1:17;
S2[s1] by A19, A1;
then s1 in { s1 where s1 is Subset of (ConwayDay alpha) : S2[s1] } ;
then A20: s1 c= s by ZFMISC_1:74;
gR in ConwayDay alpha by A15, A16, Th11;
then gRL in ConwayDay alpha by A18, Th11;
then gRL in s1 by A19, XBOOLE_0:def_4;
hence gRL in sg by A20, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
then A21: sg in { s1 where s1 is Subset of (ConwayDay alpha) : S2[s1] } ;
g in {g} by TARSKI:def_1;
then g in sg by XBOOLE_0:def_3;
hence g in s by A21, TARSKI:def_4; ::_thesis: verum
end;
thus S2[s] by A10; ::_thesis: verum
end;
hence g is nonnegative by Def15; ::_thesis: verum
end;
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
let g be ConwayGame; ::_thesis: ( 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 ) )
hereby ::_thesis: ( ( 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 ) ) implies g is nonpositive )
assume g is nonpositive ; ::_thesis: for gL being ConwayGame st gL in the_LeftOptions_of g holds
ex gLR being set st
( gLR in the_RightOptions_of gL & gLR is nonpositive )
then A1: - g is nonnegative by Def16;
let gL be ConwayGame; ::_thesis: ( gL in the_LeftOptions_of g implies ex gLR being set st
( gLR in the_RightOptions_of gL & gLR is nonpositive ) )
assume gL in the_LeftOptions_of g ; ::_thesis: ex gLR being set st
( gLR in the_RightOptions_of gL & gLR is nonpositive )
then - gL in the_RightOptions_of (- g) by Th39;
then consider gRL being ConwayGame such that
A2: ( gRL in the_LeftOptions_of (- gL) & gRL is nonnegative ) by A1, Th43;
take gLR = - gRL; ::_thesis: ( gLR in the_RightOptions_of gL & gLR is nonpositive )
( gLR in the_RightOptions_of (- (- gL)) & - (- gL) = gL & - gLR = gRL ) by A2, Th39, Th40;
hence ( gLR in the_RightOptions_of gL & gLR is nonpositive ) by Def16, A2; ::_thesis: verum
end;
assume A3: 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 ) ; ::_thesis: g is nonpositive
now__::_thesis:_for_gR_being_ConwayGame_st_gR_in_the_RightOptions_of_(-_g)_holds_
ex_gRL_being_set_st_
(_gRL_in_the_LeftOptions_of_gR_&_gRL_is_nonnegative_)
let gR be ConwayGame; ::_thesis: ( gR in the_RightOptions_of (- g) implies ex gRL being set st
( gRL in the_LeftOptions_of gR & gRL is nonnegative ) )
assume gR in the_RightOptions_of (- g) ; ::_thesis: ex gRL being set st
( gRL in the_LeftOptions_of gR & gRL is nonnegative )
then ( - gR in the_LeftOptions_of (- (- g)) & - (- g) = g ) by Th39, Th40;
then consider gLR being ConwayGame such that
A4: ( gLR in the_RightOptions_of (- gR) & gLR is nonpositive ) by A3;
take gRL = - gLR; ::_thesis: ( gRL in the_LeftOptions_of gR & gRL is nonnegative )
( gRL in the_LeftOptions_of (- (- gR)) & - (- gR) = gR ) by A4, Th39, Th40;
hence ( gRL in the_LeftOptions_of gR & gRL is nonnegative ) by A4, Def16; ::_thesis: verum
end;
then - g is nonnegative by Th43;
hence g is nonpositive by Def16; ::_thesis: verum
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
let g be ConwayGame; ::_thesis: ( ( 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 ) )
defpred S2[ ConwayGame] means ( ( $1 is nonnegative implies for gR being ConwayGame holds
( not gR in the_RightOptions_of $1 or gR is fuzzy or gR is positive ) ) & ( ( for gR being ConwayGame holds
( not gR in the_RightOptions_of $1 or gR is fuzzy or gR is positive ) ) implies $1 is nonnegative ) & ( $1 is nonpositive implies for gL being ConwayGame holds
( not gL in the_LeftOptions_of $1 or gL is fuzzy or gL is negative ) ) & ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of $1 or gL is fuzzy or gL is negative ) ) implies $1 is nonpositive ) );
A1: for g being ConwayGame st ( for gO being ConwayGame st gO in the_Options_of g holds
S2[gO] ) holds
S2[g]
proof
let g be ConwayGame; ::_thesis: ( ( for gO being ConwayGame st gO in the_Options_of g holds
S2[gO] ) implies S2[g] )
assume A2: for gO being ConwayGame st gO in the_Options_of g holds
S2[gO] ; ::_thesis: S2[g]
hereby ::_thesis: ( ( ( 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 ) )
assume A3: g is nonnegative ; ::_thesis: for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive )
let gR be ConwayGame; ::_thesis: ( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive )
assume A4: gR in the_RightOptions_of g ; ::_thesis: ( gR is fuzzy or gR is positive )
consider gRL being ConwayGame such that
A5: ( gRL in the_LeftOptions_of gR & gRL is nonnegative ) by A3, A4, Th43;
now__::_thesis:_(_S2[gR]_&_ex_gRL_being_ConwayGame_st_
(_gRL_in_the_LeftOptions_of_gR_&_not_gRL_is_fuzzy_&_not_gRL_is_negative_)_)
gR in the_Options_of g by A4, XBOOLE_0:def_3;
hence S2[gR] by A2; ::_thesis: ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & not gRL is fuzzy & not gRL is negative )
hereby ::_thesis: verum
take gRL = gRL; ::_thesis: ( gRL in the_LeftOptions_of gR & not gRL is fuzzy & not gRL is negative )
thus gRL in the_LeftOptions_of gR by A5; ::_thesis: ( not gRL is fuzzy & not gRL is negative )
thus ( not gRL is fuzzy & not gRL is negative ) by A5; ::_thesis: verum
end;
end;
then ( not gR is negative & not gR is zero ) ;
hence ( gR is fuzzy or gR is positive ) by Th42; ::_thesis: verum
end;
hereby ::_thesis: ( g is nonpositive iff for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) )
assume A6: for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ; ::_thesis: g is nonnegative
now__::_thesis:_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_)
let gR be ConwayGame; ::_thesis: ( gR in the_RightOptions_of g implies ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL is nonnegative ) )
assume A7: gR in the_RightOptions_of g ; ::_thesis: ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL is nonnegative )
now__::_thesis:_(_S2[gR]_&_not_gR_is_nonpositive_)
gR in the_Options_of g by A7, XBOOLE_0:def_3;
hence S2[gR] by A2; ::_thesis: not gR is nonpositive
( gR is fuzzy or gR is positive ) by A6, A7;
hence not gR is nonpositive ; ::_thesis: verum
end;
then consider gRL being ConwayGame such that
A8: ( gRL in the_LeftOptions_of gR & not gRL is fuzzy & not gRL is negative ) ;
take gRL = gRL; ::_thesis: ( gRL in the_LeftOptions_of gR & gRL is nonnegative )
( gRL is zero or gRL is positive ) by A8, Th42;
hence ( gRL in the_LeftOptions_of gR & gRL is nonnegative ) by A8; ::_thesis: verum
end;
hence g is nonnegative by Th43; ::_thesis: verum
end;
hereby ::_thesis: ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) implies g is nonpositive )
assume A9: g is nonpositive ; ::_thesis: for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative )
let gL be ConwayGame; ::_thesis: ( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative )
assume A10: gL in the_LeftOptions_of g ; ::_thesis: ( gL is fuzzy or gL is negative )
consider gLR being ConwayGame such that
A11: ( gLR in the_RightOptions_of gL & gLR is nonpositive ) by A9, A10, Th44;
now__::_thesis:_(_S2[gL]_&_ex_gLR_being_ConwayGame_st_
(_gLR_in_the_RightOptions_of_gL_&_not_gLR_is_fuzzy_&_not_gLR_is_positive_)_)
gL in the_Options_of g by A10, XBOOLE_0:def_3;
hence S2[gL] by A2; ::_thesis: ex gLR being ConwayGame st
( gLR in the_RightOptions_of gL & not gLR is fuzzy & not gLR is positive )
hereby ::_thesis: verum
take gLR = gLR; ::_thesis: ( gLR in the_RightOptions_of gL & not gLR is fuzzy & not gLR is positive )
thus gLR in the_RightOptions_of gL by A11; ::_thesis: ( not gLR is fuzzy & not gLR is positive )
thus ( not gLR is fuzzy & not gLR is positive ) by A11; ::_thesis: verum
end;
end;
then ( not gL is positive & not gL is zero ) ;
hence ( gL is fuzzy or gL is negative ) by Th42; ::_thesis: verum
end;
hereby ::_thesis: verum
assume A12: for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ; ::_thesis: g is nonpositive
now__::_thesis:_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_)
let gL be ConwayGame; ::_thesis: ( gL in the_LeftOptions_of g implies ex gLR being ConwayGame st
( gLR in the_RightOptions_of gL & gLR is nonpositive ) )
assume A13: gL in the_LeftOptions_of g ; ::_thesis: ex gLR being ConwayGame st
( gLR in the_RightOptions_of gL & gLR is nonpositive )
now__::_thesis:_(_S2[gL]_&_not_gL_is_nonnegative_)
gL in the_Options_of g by A13, XBOOLE_0:def_3;
hence S2[gL] by A2; ::_thesis: not gL is nonnegative
( gL is fuzzy or gL is negative ) by A12, A13;
hence not gL is nonnegative ; ::_thesis: verum
end;
then consider gLR being ConwayGame such that
A14: ( gLR in the_RightOptions_of gL & not gLR is fuzzy & not gLR is positive ) ;
take gLR = gLR; ::_thesis: ( gLR in the_RightOptions_of gL & gLR is nonpositive )
( gLR is zero or gLR is negative ) by A14, Th42;
hence ( gLR in the_RightOptions_of gL & gLR is nonpositive ) by A14; ::_thesis: verum
end;
hence g is nonpositive by Th44; ::_thesis: verum
end;
end;
for g being ConwayGame holds S2[g] from CGAMES_1:sch_3(A1);
hence ( ( 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 ) ) ; ::_thesis: verum
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
let g be ConwayGame; ::_thesis: ( 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 ) ) )
hereby ::_thesis: ( 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 ) implies g is fuzzy )
assume A1: g is fuzzy ; ::_thesis: ( 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 ) )
hereby ::_thesis: ex gR being ConwayGame st
( gR in the_RightOptions_of g & gR is nonpositive )
consider gL being ConwayGame such that
A2: ( gL in the_LeftOptions_of g & ( for gLR being ConwayGame st gLR in the_RightOptions_of gL holds
not gLR is nonpositive ) ) by A1, Th44;
take gL = gL; ::_thesis: ( gL in the_LeftOptions_of g & gL is nonnegative )
thus gL in the_LeftOptions_of g by A2; ::_thesis: gL is nonnegative
now__::_thesis:_for_gLR_being_ConwayGame_holds_
(_not_gLR_in_the_RightOptions_of_gL_or_gLR_is_fuzzy_or_gLR_is_positive_)
let gLR be ConwayGame; ::_thesis: ( not gLR in the_RightOptions_of gL or gLR is fuzzy or gLR is positive )
assume gLR in the_RightOptions_of gL ; ::_thesis: ( gLR is fuzzy or gLR is positive )
then ( not gLR is negative & not gLR is zero ) by A2;
hence ( gLR is fuzzy or gLR is positive ) by Th42; ::_thesis: verum
end;
hence gL is nonnegative by Th45; ::_thesis: verum
end;
hereby ::_thesis: verum
consider gR being ConwayGame such that
A3: ( gR in the_RightOptions_of g & ( for gRL being ConwayGame st gRL in the_LeftOptions_of gR holds
not gRL is nonnegative ) ) by A1, Th43;
take gR = gR; ::_thesis: ( gR in the_RightOptions_of g & gR is nonpositive )
thus gR in the_RightOptions_of g by A3; ::_thesis: gR is nonpositive
now__::_thesis:_for_gRL_being_ConwayGame_holds_
(_not_gRL_in_the_LeftOptions_of_gR_or_gRL_is_fuzzy_or_gRL_is_negative_)
let gRL be ConwayGame; ::_thesis: ( not gRL in the_LeftOptions_of gR or gRL is fuzzy or gRL is negative )
assume gRL in the_LeftOptions_of gR ; ::_thesis: ( gRL is fuzzy or gRL is negative )
then ( not gRL is positive & not gRL is zero ) by A3;
hence ( gRL is fuzzy or gRL is negative ) by Th42; ::_thesis: verum
end;
hence gR is nonpositive by Th45; ::_thesis: verum
end;
end;
hereby ::_thesis: verum
assume ex gL being ConwayGame st
( gL in the_LeftOptions_of g & gL is nonnegative ) ; ::_thesis: ( ex gR being ConwayGame st
( gR in the_RightOptions_of g & gR is nonpositive ) implies g is fuzzy )
then consider gL being ConwayGame such that
A4: ( gL in the_LeftOptions_of g & gL is nonnegative ) ;
assume ex gR being ConwayGame st
( gR in the_RightOptions_of g & gR is nonpositive ) ; ::_thesis: g is fuzzy
then consider gR being ConwayGame such that
A5: ( gR in the_RightOptions_of g & gR is nonpositive ) ;
( not gL is fuzzy & not gL is negative & not gR is fuzzy & not gR is positive ) by A4, A5;
then ( not g is nonpositive & not g is nonnegative ) by Th45, A4, A5;
hence g is fuzzy ; ::_thesis: verum
end;
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 ) ) ) )
proof
let g be ConwayGame; ::_thesis: ( 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 ) ) ) )
thus ( g is zero implies ( ( 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; ::_thesis: ( ( 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 ) ) implies g is zero )
assume ( ( 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 ) ) ) ; ::_thesis: g is zero
then ( g is nonpositive & g is nonnegative ) by Th45;
hence g is zero ; ::_thesis: verum
end;
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
let g be ConwayGame; ::_thesis: ( 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 ) ) )
hereby ::_thesis: ( ( 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 ) implies g is positive )
assume A1: g is positive ; ::_thesis: ( ( 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 ) )
hence A2: for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) by Th45; ::_thesis: ex gL being ConwayGame st
( gL in the_LeftOptions_of g & gL is nonnegative )
consider gL being ConwayGame such that
A3: ( gL in the_LeftOptions_of g & not gL is fuzzy & not gL is negative ) by Th47, A1, A2;
take gL = gL; ::_thesis: ( gL in the_LeftOptions_of g & gL is nonnegative )
( gL is zero or gL is positive ) by A3, Th42;
hence ( gL in the_LeftOptions_of g & gL is nonnegative ) by A3; ::_thesis: verum
end;
hereby ::_thesis: verum
assume for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ; ::_thesis: ( ex gL being ConwayGame st
( gL in the_LeftOptions_of g & gL is nonnegative ) implies g is positive )
then A4: g is nonnegative by Th45;
assume ex gL being ConwayGame st
( gL in the_LeftOptions_of g & gL is nonnegative ) ; ::_thesis: g is positive
then consider gL being ConwayGame such that
A5: ( gL in the_LeftOptions_of g & gL is nonnegative ) ;
( not gL is fuzzy & not gL is negative ) by A5;
then not g is zero by Th47, A5;
hence g is positive by A4; ::_thesis: verum
end;
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
let g be ConwayGame; ::_thesis: ( 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 ) ) )
hereby ::_thesis: ( ( 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 ) implies g is negative )
assume A1: g is negative ; ::_thesis: ( ( 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 ) )
hence A2: for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) by Th45; ::_thesis: ex gR being ConwayGame st
( gR in the_RightOptions_of g & gR is nonpositive )
consider gR being ConwayGame such that
A3: ( gR in the_RightOptions_of g & not gR is fuzzy & not gR is positive ) by Th47, A1, A2;
take gR = gR; ::_thesis: ( gR in the_RightOptions_of g & gR is nonpositive )
( gR is zero or gR is negative ) by A3, Th42;
hence ( gR in the_RightOptions_of g & gR is nonpositive ) by A3; ::_thesis: verum
end;
hereby ::_thesis: verum
assume for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ; ::_thesis: ( ex gR being ConwayGame st
( gR in the_RightOptions_of g & gR is nonpositive ) implies g is negative )
then A4: g is nonpositive by Th45;
assume ex gR being ConwayGame st
( gR in the_RightOptions_of g & gR is nonpositive ) ; ::_thesis: g is negative
then consider gR being ConwayGame such that
A5: ( gR in the_RightOptions_of g & gR is nonpositive ) ;
( not gR is fuzzy & not gR is positive ) by A5;
then not g is zero by Th47, A5;
hence g is negative by A4; ::_thesis: verum
end;
end;
registration
cluster ConwayZero -> zero ;
coherence
ConwayZero is zero
proof
( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of ConwayZero or gL is fuzzy or gL is negative ) ) & ( for gR being ConwayGame holds
( not gR in the_RightOptions_of ConwayZero or gR is fuzzy or gR is positive ) ) ) ;
hence ConwayZero is zero by Th47; ::_thesis: verum
end;
end;
registration
cluster ConwayOne -> positive ;
coherence
ConwayOne is positive
proof
now__::_thesis:_(_(_for_gR_being_ConwayGame_holds_
(_not_gR_in_the_RightOptions_of_ConwayOne_or_gR_is_fuzzy_or_gR_is_positive_)_)_&_ex_gL_being_Element_of_ConwayDay_0_st_
(_gL_in_the_LeftOptions_of_ConwayOne_&_gL_is_nonnegative_)_)
thus for gR being ConwayGame holds
( not gR in the_RightOptions_of ConwayOne or gR is fuzzy or gR is positive ) ; ::_thesis: ex gL being Element of ConwayDay 0 st
( gL in the_LeftOptions_of ConwayOne & gL is nonnegative )
hereby ::_thesis: verum
take gL = ConwayZero ; ::_thesis: ( gL in the_LeftOptions_of ConwayOne & gL is nonnegative )
thus gL in the_LeftOptions_of ConwayOne by Th7; ::_thesis: gL is nonnegative
thus gL is nonnegative ; ::_thesis: verum
end;
end;
hence ConwayOne is positive by Th48; ::_thesis: verum
end;
cluster ConwayStar -> fuzzy ;
coherence
ConwayStar is fuzzy
proof
now__::_thesis:_(_ex_gL_being_Element_of_ConwayDay_0_st_
(_gL_in_the_LeftOptions_of_ConwayStar_&_gL_is_nonnegative_)_&_ex_gR_being_Element_of_ConwayDay_0_st_
(_gR_in_the_RightOptions_of_ConwayStar_&_gR_is_nonpositive_)_)
hereby ::_thesis: ex gR being Element of ConwayDay 0 st
( gR in the_RightOptions_of ConwayStar & gR is nonpositive )
take gL = ConwayZero ; ::_thesis: ( gL in the_LeftOptions_of ConwayStar & gL is nonnegative )
thus gL in the_LeftOptions_of ConwayStar by Th8; ::_thesis: gL is nonnegative
thus gL is nonnegative ; ::_thesis: verum
end;
hereby ::_thesis: verum
take gR = ConwayZero ; ::_thesis: ( gR in the_RightOptions_of ConwayStar & gR is nonpositive )
thus gR in the_RightOptions_of ConwayStar by Th8; ::_thesis: gR is nonpositive
thus gR is nonpositive ; ::_thesis: verum
end;
end;
hence ConwayStar is fuzzy by Th46; ::_thesis: verum
end;
end;
registration
cluster ConwayGame-like zero for set ;
existence
ex b1 being ConwayGame st b1 is zero
proof
take ConwayZero ; ::_thesis: ConwayZero is zero
thus ConwayZero is zero ; ::_thesis: verum
end;
cluster ConwayGame-like positive for set ;
existence
ex b1 being ConwayGame st b1 is positive
proof
take ConwayOne ; ::_thesis: ConwayOne is positive
thus ConwayOne is positive ; ::_thesis: verum
end;
cluster ConwayGame-like fuzzy for set ;
existence
ex b1 being ConwayGame st b1 is fuzzy
proof
take ConwayStar ; ::_thesis: ConwayStar is fuzzy
thus ConwayStar is fuzzy ; ::_thesis: verum
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
proof
g = - (- g) by Th40;
hence - g is nonpositive by Def16; ::_thesis: verum
end;
end;
registration
let g be positive ConwayGame;
cluster - g -> negative ;
coherence
- g is negative
proof
g = - (- g) by Th40;
then ( not - g is zero & - g is nonpositive ) ;
hence - g is negative ; ::_thesis: verum
end;
end;
registration
cluster ConwayGame-like negative for set ;
existence
ex b1 being ConwayGame st b1 is negative
proof
take - ConwayOne ; ::_thesis: - ConwayOne is negative
thus - ConwayOne is negative ; ::_thesis: verum
end;
end;
registration
let g be negative ConwayGame;
cluster - g -> positive ;
coherence
- g is positive
proof
g = - (- g) by Th40;
then ( not - g is zero & - g is nonnegative ) ;
hence - g is positive ; ::_thesis: verum
end;
end;
registration
let g be fuzzy ConwayGame;
cluster - g -> fuzzy ;
coherence
- g is fuzzy
proof
g = - (- g) by Th40;
then ( not - g is positive & not - g is negative & not - g is zero ) ;
hence - g is fuzzy by Th42; ::_thesis: verum
end;
end;