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