cgames_1.miz



    begin

    reserve x,y,y1,y2,z,e,s for set;

    reserve alpha,beta,gamma for Ordinal;

    reserve n,m,k for Nat;

    definition

      struct left-right (# the LeftOptions, RightOptions -> set #)

       attr strict strict;

    end

    definition

      :: CGAMES_1:def1

      func ConwayZero -> set equals left-right (# {} , {} #);

      coherence by TARSKI: 1;

    end

    registration

      cluster strict for left-right;

      existence

      proof

        take ConwayZero ;

        thus thesis;

      end;

    end

    deffunc ConwayNextDay( Sequence) = the set of all left-right (# x, y #) where x,y be Subset of ( union ( rng $1));

    defpred ConwayIteration[ Sequence] means for beta st beta in ( dom $1) holds ($1 . beta) = ConwayNextDay(|);

    

     Lm1: for f be Sequence st ConwayIteration[f] holds for alpha holds ConwayIteration[(f | alpha)]

    proof

      let f be Sequence;

      assume

       A1: ConwayIteration[f];

      let alpha, beta;

      assume

       A2: beta in ( dom (f | alpha));

      ( dom (f | alpha)) c= ( dom f) by RELAT_1: 60;

      then

       A3: (f . beta) = ConwayNextDay(|) 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 thesis by A3, A2, FUNCT_1: 47;

    end;

    definition

      let alpha;

      :: CGAMES_1:def2

      func ConwayDay (alpha) -> set means

      : Def2: ex f be Sequence st alpha in ( dom f) & (f . alpha) = it & for beta st beta in ( dom f) holds (f . beta) = the set of all left-right (# x, y #) where x,y be Subset of ( union ( rng (f | beta)));

      existence

      proof

        consider f be Sequence such that

         A1: ( dom f) = ( succ alpha) & for beta holds for f1 be Sequence st beta in ( succ alpha) & f1 = (f | beta) holds (f . beta) = ConwayNextDay(f1) from ORDINAL1:sch 4;

        take (f . alpha);

        take f;

        thus alpha in ( dom f) by A1, ORDINAL1: 6;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let x, y;

        assume ex f1 be Sequence st alpha in ( dom f1) & (f1 . alpha) = x & ConwayIteration[f1];

        then

        consider f1 be Sequence such that

         A2: alpha in ( dom f1) & (f1 . alpha) = x & ConwayIteration[f1];

        set f1r = (f1 | ( succ alpha));

        assume ex f2 be Sequence st alpha in ( dom f2) & (f2 . alpha) = y & ConwayIteration[f2];

        then

        consider f2 be Sequence such that

         A3: alpha in ( dom f2) & (f2 . alpha) = y & ConwayIteration[f2];

        set f2r = (f2 | ( succ alpha));

        

         A4: ( dom f1r) = ( succ alpha) & for beta holds for f be Sequence st beta in ( succ alpha) & f = (f1r | beta) holds (f1r . beta) = ConwayNextDay(f)

        proof

          ( succ alpha) c= ( dom f1) by A2, ORDINAL1: 21;

          hence

           A5: ( dom f1r) = ( succ alpha) by RELAT_1: 62;

          let beta;

          let f be Sequence;

          assume beta in ( succ alpha) & f = (f1r | beta);

          hence thesis by A5, Lm1, A2;

        end;

        

         A6: ( dom f2r) = ( succ alpha) & for beta holds for f be Sequence st beta in ( succ alpha) & f = (f2r | beta) holds (f2r . beta) = ConwayNextDay(f)

        proof

          ( succ alpha) c= ( dom f2) by A3, ORDINAL1: 21;

          hence

           A7: ( dom f2r) = ( succ alpha) by RELAT_1: 62;

          let beta;

          let f be Sequence;

          assume beta in ( succ alpha) & f = (f2r | beta);

          hence thesis by A7, Lm1, A3;

        end;

        

         A8: (f1r . alpha) = (f1 . alpha) & (f2r . alpha) = (f2 . alpha) by FUNCT_1: 49, ORDINAL1: 6;

        f1r = f2r from ORDINAL1:sch 3( A4, A6);

        hence x = y by A2, A3, A8;

      end;

    end

    theorem :: CGAMES_1:1

    

     Th1: for z be object holds z in ( ConwayDay alpha) iff ex w be strict left-right st z = w & for x st x in (the LeftOptions of w \/ the RightOptions of w) holds ex beta st beta in alpha & x in ( ConwayDay beta)

    proof

      let z be object;

      consider f be Sequence such that

       A1: alpha in ( dom f) & (f . alpha) = ( ConwayDay alpha) & ConwayIteration[f] by Def2;

      hereby

        assume z in ( ConwayDay alpha);

        then z in ConwayNextDay(|) by A1;

        then

        consider x,y be 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;

        thus z = w;

        let e;

        assume e in (the LeftOptions of w \/ the RightOptions of w);

        then e in x or e in y by A2, XBOOLE_0:def 3;

        then

        consider r be set such that

         A3: e in r & r in ( rng (f | alpha)) by TARSKI:def 4;

        ex beta be object st beta in ( dom (f | alpha)) & r = ((f | alpha) . beta) by A3, FUNCT_1:def 3;

        then

        consider beta such that

         A4: beta in ( dom (f | alpha)) & r = ((f | alpha) . beta);

        take beta;

        ( dom (f | alpha)) c= alpha by RELAT_1: 58;

        hence beta in alpha by A4;

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

      end;

      hereby

        assume ex w be strict left-right st z = w & for x st x in (the LeftOptions of w \/ the RightOptions of w) holds ex beta st beta in alpha & x in ( ConwayDay beta);

        then

        consider w be strict left-right such that

         A5: w = z & for x st x in (the LeftOptions of w \/ the RightOptions of w) holds ex beta 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 object;

            assume e in (the LeftOptions of w \/ the RightOptions of w);

            then

            consider beta 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;

          end;

          hence thesis by XBOOLE_1: 11;

        end;

        then w in ConwayNextDay(|);

        hence z in ( ConwayDay alpha) by A1, A5;

      end;

    end;

    theorem :: CGAMES_1:2

    

     Th2: ( ConwayDay 0 ) = { ConwayZero }

    proof

      

       A1: ( ConwayDay 0 ) c= { ConwayZero }

      proof

        let z be object;

        assume z in ( ConwayDay 0 );

        then

        consider w be strict left-right such that

         A2: z = w & for e st e in (the LeftOptions of w \/ the RightOptions of w) holds ex beta st beta in 0 & e in ( ConwayDay beta) by Th1;

        (the LeftOptions of w \/ the RightOptions of w) = {}

        proof

          assume not thesis;

          then

          consider e be object such that

           A3: e in (the LeftOptions of w \/ the RightOptions of w) by XBOOLE_0:def 1;

          ex beta st beta in 0 & e in ( ConwayDay beta) by A2, A3;

          hence contradiction;

        end;

        then the LeftOptions of w = {} & the RightOptions of w = {} ;

        hence z in { ConwayZero } by A2, TARSKI:def 1;

      end;

      for e st e in ( {} \/ {} ) holds ex beta 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 thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: CGAMES_1:3

    

     Th3: alpha c= beta implies ( ConwayDay alpha) c= ( ConwayDay beta)

    proof

      assume

       A1: alpha c= beta;

      let z be object;

      assume z in ( ConwayDay alpha);

      then

      consider w be strict left-right such that

       A2: w = z & (for e st e in (the LeftOptions of w \/ the RightOptions of w) holds ex gamma st gamma in alpha & e in ( ConwayDay gamma)) by Th1;

      now

        let e;

        assume e in (the LeftOptions of w \/ the RightOptions of w);

        then ex gamma st gamma in alpha & e in ( ConwayDay gamma) by A2;

        hence ex gamma st gamma in beta & e in ( ConwayDay gamma) by A1;

      end;

      hence z in ( ConwayDay beta) by Th1, A2;

    end;

    registration

      let alpha;

      cluster ( ConwayDay alpha) -> non empty;

      coherence

      proof

         0 c= alpha;

        then ( ConwayDay 0 ) c= ( ConwayDay alpha) by Th3;

        hence thesis by Th2;

      end;

    end

    begin

    definition

      let x;

      :: CGAMES_1:def3

      attr x is ConwayGame-like means

      : Def3: ex alpha st x in ( ConwayDay alpha);

    end

    registration

      let alpha;

      cluster -> ConwayGame-like for Element of ( ConwayDay alpha);

      coherence ;

    end

    registration

      cluster ConwayZero -> ConwayGame-like;

      coherence

      proof

         ConwayZero in ( ConwayDay 0 ) by Th2, TARSKI:def 1;

        hence thesis;

      end;

    end

    registration

      cluster ConwayGame-like strict for left-right;

      existence

      proof

        take ConwayZero ;

        thus thesis;

      end;

      cluster ConwayGame-like for set;

      existence

      proof

        take ConwayZero ;

        thus thesis;

      end;

    end

    definition

      mode ConwayGame is ConwayGame-like set;

    end

    definition

      :: original: ConwayZero

      redefine

      func ConwayZero -> Element of ( ConwayDay 0 ) ;

      coherence by Th2, TARSKI:def 1;

    end

    definition

      :: CGAMES_1:def4

      func ConwayOne -> Element of ( ConwayDay 1) equals left-right (# { ConwayZero }, {} #);

      coherence

      proof

        set w = left-right (# { ConwayZero }, {} #);

        for x st x in (the LeftOptions of w \/ the RightOptions of w) holds ex beta st beta in 1 & x in ( ConwayDay beta)

        proof

          let x;

          assume x in (the LeftOptions of w \/ the RightOptions of w);

          then

           A1: x = ConwayZero by TARSKI:def 1;

          take 0 ;

          1 = ( succ 0 );

          hence thesis by A1, ORDINAL1: 6;

        end;

        hence thesis by Th1;

      end;

      :: CGAMES_1:def5

      func ConwayStar -> Element of ( ConwayDay 1) equals left-right (# { ConwayZero }, { ConwayZero } #);

      coherence

      proof

        set w = left-right (# { ConwayZero }, { ConwayZero } #);

        for x st x in (the LeftOptions of w \/ the RightOptions of w) holds ex beta st beta in 1 & x in ( ConwayDay beta)

        proof

          let x;

          assume x in (the LeftOptions of w \/ the RightOptions of w);

          then

           A2: x = ConwayZero by TARSKI:def 1;

          take 0 ;

          1 = ( succ 0 );

          hence thesis by A2, ORDINAL1: 6;

        end;

        hence thesis by Th1;

      end;

    end

    reserve g,g0,g1,g2,gO,gL,gR,gLL,gLR,gRL,gRR for ConwayGame;

    theorem :: CGAMES_1:4

    

     Th4: g is strict left-right

    proof

      consider alpha such that

       A1: g in ( ConwayDay alpha) by Def3;

      ex w be strict left-right st w = g & for x st x in (the LeftOptions of w \/ the RightOptions of w) holds ex beta st beta in alpha & x in ( ConwayDay beta) by A1, Th1;

      hence thesis;

    end;

    registration

      cluster ConwayGame-like -> strict for left-right;

      coherence by Th4;

    end

    definition

      let g;

      :: CGAMES_1:def6

      func the_LeftOptions_of g -> set means

      : Def6: ex w be left-right st g = w & it = the LeftOptions of w;

      existence

      proof

        reconsider w = g as left-right by Th4;

        take the LeftOptions of w;

        thus thesis;

      end;

      uniqueness ;

      :: CGAMES_1:def7

      func the_RightOptions_of g -> set means

      : Def7: ex w be left-right st g = w & it = the RightOptions of w;

      existence

      proof

        reconsider w = g as left-right by Th4;

        take the RightOptions of w;

        thus thesis;

      end;

      uniqueness ;

    end

    definition

      let g;

      :: CGAMES_1:def8

      func the_Options_of g -> set equals (( the_LeftOptions_of g) \/ ( the_RightOptions_of g));

      correctness ;

    end

    theorem :: CGAMES_1:5

    

     Th5: g1 = g2 iff (( the_LeftOptions_of g1) = ( the_LeftOptions_of g2) & ( the_RightOptions_of g1) = ( the_RightOptions_of g2))

    proof

      thus g1 = g2 implies (( the_LeftOptions_of g1) = ( the_LeftOptions_of g2) & ( the_RightOptions_of g1) = ( the_RightOptions_of 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);

      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;

    end;

    registration

      cluster ( the_LeftOptions_of ConwayZero ) -> empty;

      coherence by Def6;

      cluster ( the_RightOptions_of ConwayZero ) -> empty;

      coherence by Def7;

      cluster ( the_RightOptions_of ConwayOne ) -> empty;

      coherence by Def7;

    end

    theorem :: CGAMES_1:6

    

     Th6: g = ConwayZero iff ( the_Options_of g) = {}

    proof

      hereby

        assume g = ConwayZero ;

        then ( the_LeftOptions_of g) = {} & ( the_RightOptions_of g) = {} ;

        hence ( the_Options_of g) = {} ;

      end;

      hereby

        reconsider w = g as strict left-right by Th4;

        assume ( the_Options_of g) = {} ;

        then ( the_LeftOptions_of g) = {} & ( the_RightOptions_of g) = {} ;

        then the LeftOptions of w = {} & the RightOptions of w = {} by Def6, Def7;

        hence g = ConwayZero ;

      end;

    end;

    theorem :: CGAMES_1:7

    

     Th7: x in ( the_LeftOptions_of ConwayOne ) iff x = ConwayZero

    proof

      ( the_LeftOptions_of ConwayOne ) = { ConwayZero } by Def6;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: CGAMES_1:8

    

     Th8: (x in ( the_Options_of ConwayStar ) iff x = ConwayZero ) & (x in ( the_LeftOptions_of ConwayStar ) iff x = ConwayZero ) & (x in ( the_RightOptions_of ConwayStar ) iff x = ConwayZero )

    proof

      ( the_LeftOptions_of ConwayStar ) = { ConwayZero } & ( the_RightOptions_of ConwayStar ) = { ConwayZero } by Def6, Def7;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: CGAMES_1:9

    

     Th9: g in ( ConwayDay alpha) iff for x st x in ( the_Options_of g) holds ex beta st beta in alpha & x in ( ConwayDay beta)

    proof

      hereby

        assume g in ( ConwayDay alpha);

        then

        consider w be strict left-right such that

         A1: g = w & for x st x in (the LeftOptions of w \/ the RightOptions of w) holds ex beta st beta in alpha & x in ( ConwayDay beta) by Th1;

        let x;

        

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

        hence ex beta st beta in alpha & x in ( ConwayDay beta) by A1, A2;

      end;

      hereby

        assume

         A3: for x st x in ( the_Options_of g) holds ex beta st beta in alpha & x in ( ConwayDay beta);

        ex w be strict left-right st g = w & for x st x in (the LeftOptions of w \/ the RightOptions of w) holds ex beta st beta in alpha & x in ( ConwayDay beta)

        proof

          reconsider w = g as strict left-right by Th4;

          take w;

          the LeftOptions of w = ( the_LeftOptions_of g) & the RightOptions of w = ( the_RightOptions_of g) by Def6, Def7;

          hence thesis by A3;

        end;

        hence g in ( ConwayDay alpha) by Th1;

      end;

    end;

    definition

      let g be set;

      assume

       A1: g is ConwayGame;

      :: CGAMES_1:def9

      func ConwayRank (g) -> Ordinal means

      : Def9: g in ( ConwayDay it ) & for beta st beta in it holds not g in ( ConwayDay beta);

      existence

      proof

        defpred Included[ Ordinal] means g in ( ConwayDay $1);

        

         A2: ex alpha st Included[alpha] by Def3, A1;

        consider alpha such that

         A3: Included[alpha] & for beta st Included[beta] holds alpha c= beta from ORDINAL1:sch 1( A2);

        take alpha;

        thus g in ( ConwayDay alpha) by A3;

        let beta;

        assume

         A4: beta in alpha;

        assume g in ( ConwayDay beta);

        then alpha c= beta by A3;

        then beta in beta by A4;

        hence contradiction;

      end;

      uniqueness

      proof

        let alpha1,alpha2 be Ordinal;

        assume

         A5: g in ( ConwayDay alpha1) & for beta st beta in alpha1 holds not g in ( ConwayDay beta);

        assume

         A6: g in ( ConwayDay alpha2) & for beta st beta in alpha2 holds not g in ( ConwayDay beta);

        assume

         A7: alpha1 <> alpha2;

        per cases by A7, ORDINAL1: 14;

          suppose alpha1 in alpha2;

          hence contradiction by A5, A6;

        end;

          suppose alpha2 in alpha1;

          hence contradiction by A5, A6;

        end;

      end;

    end

    theorem :: CGAMES_1:10

    

     Th10: g in ( ConwayDay alpha) & x in ( the_Options_of g) implies x in ( ConwayDay alpha)

    proof

      assume g in ( ConwayDay alpha) & x in ( the_Options_of g);

      then

      consider beta 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;

    end;

    theorem :: CGAMES_1:11

    

     Th11: g in ( ConwayDay alpha) & (x in ( the_LeftOptions_of g) or x in ( the_RightOptions_of g)) implies x in ( ConwayDay alpha)

    proof

      (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 thesis by Th10;

    end;

    theorem :: CGAMES_1:12

    

     Th12: g in ( ConwayDay alpha) iff ( ConwayRank g) c= alpha

    proof

      hereby

        assume

         A1: g in ( ConwayDay alpha);

        assume not ( ConwayRank g) c= alpha;

        then alpha in ( ConwayRank g) by ORDINAL1: 16;

        hence contradiction by A1, Def9;

      end;

      hereby

        assume ( ConwayRank g) c= 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;

      end;

    end;

    theorem :: CGAMES_1:13

    

     Th13: ( ConwayRank g) in alpha iff ex beta st beta in alpha & g in ( ConwayDay beta)

    proof

      hereby

        assume

         A1: ( ConwayRank g) in alpha;

        take beta = ( ConwayRank g);

        thus beta in alpha by A1;

        thus g in ( ConwayDay beta) by Th12;

      end;

      thus (ex beta st beta in alpha & g in ( ConwayDay beta)) implies ( ConwayRank g) in alpha by Th12, ORDINAL1: 12;

    end;

    theorem :: CGAMES_1:14

    

     Th14: gO in ( the_Options_of g) implies ( ConwayRank gO) in ( ConwayRank g)

    proof

      set alpha = ( ConwayRank g);

      

       A1: g in ( ConwayDay alpha) by Def9;

      assume gO in ( the_Options_of g);

      then

      consider beta such that

       A2: beta in alpha & gO in ( ConwayDay beta) by A1, Th9;

      ( ConwayRank gO) c= beta by A2, Th12;

      hence thesis by A2, ORDINAL1: 12;

    end;

    theorem :: CGAMES_1:15

    (gO in ( the_LeftOptions_of g) or gO in ( the_RightOptions_of g)) implies ( ConwayRank gO) in ( ConwayRank g)

    proof

      assume gO in ( the_LeftOptions_of g) or gO in ( the_RightOptions_of g);

      then gO in ( the_Options_of g) by XBOOLE_0:def 3;

      hence thesis by Th14;

    end;

    theorem :: CGAMES_1:16

    

     Th16: not g in ( the_Options_of g)

    proof

      assume not thesis;

      then ( ConwayRank g) in ( ConwayRank g) by Th14;

      hence contradiction;

    end;

    theorem :: CGAMES_1:17

    

     Th17: x in ( the_Options_of g) implies x is ConwayGame-like left-right

    proof

      consider alpha such that

       A1: g in ( ConwayDay alpha) by Def3;

      assume x in ( the_Options_of g);

      then x in ( ConwayDay alpha) by Th10, A1;

      hence thesis by Th4;

    end;

    theorem :: CGAMES_1:18

    

     Th18: (x in ( the_LeftOptions_of g) or x in ( the_RightOptions_of g)) implies x is ConwayGame-like left-right

    proof

      assume x in ( the_LeftOptions_of g) or x in ( the_RightOptions_of g);

      then x in ( the_Options_of g) by XBOOLE_0:def 3;

      hence thesis by Th17;

    end;

    theorem :: CGAMES_1:19

    

     Th19: for w be strict left-right holds w is ConwayGame iff for z st z in (the LeftOptions of w \/ the RightOptions of w) holds z is ConwayGame

    proof

      let w be strict left-right;

      hereby

        assume w 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 st z in (the LeftOptions of w \/ the RightOptions of w) holds z is ConwayGame by Th17;

      end;

      hereby

        assume

         A1: for z st z in (the LeftOptions of w \/ the RightOptions of w) holds z is ConwayGame;

        set Z = the set of all ( ConwayRank z) where z be Element of (the LeftOptions of w \/ the RightOptions of w);

        set alpha = ( sup Z);

        now

          let z;

          assume

           A2: z in (the LeftOptions of w \/ the RightOptions of w);

          then ( ConwayRank z) in Z;

          then ( ConwayRank z) in ( On Z) & ( On Z) c= alpha by ORDINAL1:def 9, ORDINAL2:def 3;

          then

           A3: ( ConwayRank z) c= alpha by ORDINAL1:def 2;

          take beta = alpha;

          thus beta in ( succ alpha) by ORDINAL1: 6;

          z is ConwayGame by A1, A2;

          hence z in ( ConwayDay beta) by A3, Th12;

        end;

        then w in ( ConwayDay ( succ alpha)) by Th1;

        hence w is ConwayGame;

      end;

    end;

    begin

    scheme :: CGAMES_1:sch1

    ConwayGameMinTot { P[ ConwayGame] } :

ex g st P[g] & for g1 st ( ConwayRank g1) in ( ConwayRank g) holds not P[g1]

      provided

       A1: ex g st P[g];

      defpred Empty[ Ordinal] means for g st g in ( ConwayDay $1) holds not P[g];

      assume

       A2: not thesis;

      

       A3: for alpha st for beta st beta in alpha holds Empty[beta] holds Empty[alpha]

      proof

        let alpha;

        assume

         A4: for beta st beta in alpha holds Empty[beta];

        let g;

        assume

         A5: g in ( ConwayDay alpha) & P[g];

        then

        consider g1 such that

         A6: ( ConwayRank g1) in ( ConwayRank g) & P[g1] by A2;

        ( ConwayRank g) c= alpha by Th12, A5;

        then

        consider beta such that

         A7: beta in alpha & g1 in ( ConwayDay beta) by Th13, A6;

        thus contradiction by A4, A7, A6;

      end;

      

       A8: for alpha holds Empty[alpha] from ORDINAL1:sch 2( A3);

      consider g such that

       A9: P[g] by A1;

      consider alpha such that

       A10: g in ( ConwayDay alpha) by Def3;

      thus contradiction by A8, A9, A10;

    end;

    scheme :: CGAMES_1:sch2

    ConwayGameMin { P[ ConwayGame] } :

ex g st P[g] & for gO st gO in ( the_Options_of g) holds not P[gO]

      provided

       A1: ex g st P[g];

      consider g such that

       A2: P[g] & for g1 st ( ConwayRank g1) in ( ConwayRank g) holds not P[g1] from ConwayGameMinTot( A1);

      take g;

      thus P[g] by A2;

      let gO;

      assume gO in ( the_Options_of g);

      then ( ConwayRank gO) in ( ConwayRank g) by Th14;

      hence not P[gO] by A2;

    end;

    scheme :: CGAMES_1:sch3

    ConwayGameInd { P[ ConwayGame] } :

for g holds P[g]

      provided

       A1: for g st (for gO st gO in ( the_Options_of g) holds P[gO]) holds P[g];

      defpred NP[ ConwayGame] means not P[$1];

      assume

       A2: ex g st NP[g];

      ex g st NP[g] & for gO st gO in ( the_Options_of g) holds not NP[gO] from ConwayGameMin( A2);

      hence contradiction by A1;

    end;

    begin

    definition

      let f be Function;

      :: CGAMES_1:def10

      attr f is ConwayGame-valued means

      : Def10: for x st x in ( dom f) holds (f . x) is ConwayGame;

    end

    registration

      let g;

      cluster <*g*> -> ConwayGame-valued;

      coherence

      proof

        let x;

        assume x in ( dom <*g*>);

        then x = 1 by FINSEQ_1: 90;

        hence thesis by FINSEQ_1:def 8;

      end;

    end

    registration

      cluster ConwayGame-valued non empty for FinSequence;

      existence

      proof

        take <* ConwayZero *>;

        thus thesis;

      end;

    end

    registration

      let f be non empty FinSequence;

      cluster -> natural non empty for Element of ( dom f);

      coherence by FINSEQ_3: 24;

    end

    registration

      let f be ConwayGame-valued non empty Function;

      let x be Element of ( dom f);

      cluster (f . x) -> ConwayGame-like;

      coherence by Def10;

    end

    definition

      let f be ConwayGame-valued non empty FinSequence;

      :: CGAMES_1:def11

      attr f is ConwayGameChain-like means

      : Def11: for n be Element of ( dom f) st n > 1 holds (f . (n - 1)) in ( the_Options_of (f . n));

    end

    theorem :: CGAMES_1:20

    

     Th20: for f be FinSequence holds for n st n in ( dom f) & n > 1 holds (n - 1) in ( dom f)

    proof

      let f be FinSequence;

      consider l be Nat such that

       A1: ( dom f) = ( Seg l) by FINSEQ_1:def 2;

      thus thesis by A1, FINSEQ_3: 12;

    end;

    registration

      let g;

      cluster <*g*> -> ConwayGameChain-like;

      coherence

      proof

        let n be Element of ( dom <*g*>);

        ( dom <*g*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      cluster ConwayGameChain-like for ConwayGame-valued non empty FinSequence;

      existence

      proof

        set g = the ConwayGame;

        take <*g*>;

        thus thesis;

      end;

    end

    definition

      mode ConwayGameChain is ConwayGameChain-like ConwayGame-valued non empty FinSequence;

    end

    theorem :: CGAMES_1:21

    

     Th21: for f be ConwayGameChain holds for n,m be Element of ( dom f) st n < m holds ( ConwayRank (f . n)) in ( ConwayRank (f . m))

    proof

      let f be ConwayGameChain;

      let n,m be Element of ( dom f) such that

       A1: n < m;

      consider l be Nat such that

       A2: ( dom f) = ( Seg l) by FINSEQ_1:def 2;

      defpred True[ 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: True[1]

      proof

        assume (m - 1) in ( dom f);

        then

        reconsider m1 = (m - 1) as Element of ( dom f);

        (f . m1) in ( the_Options_of (f . m)) by A3, Def11;

        hence thesis by Th14;

      end;

      

       A5: for k be non zero Nat st True[k] holds True[(k + 1)]

      proof

        let k be non zero Nat;

        assume

         A6: True[k];

        assume (m - (k + 1)) in ( dom f);

        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;

        

         A8: mk1 = (mk - 1);

        mk1 > 0 ;

        then (mk1 + 1) > 1 by XREAL_1: 29;

        then (f . mk1) in ( the_Options_of (f . mk)) by Def11, A8;

        then ( ConwayRank (f . mk1)) in ( ConwayRank (f . mk)) & ( ConwayRank (f . mk)) in ( ConwayRank (f . m)) by Th14, A6;

        hence thesis by ORDINAL1: 10;

      end;

      

       A9: for k be non zero Nat holds True[k] from NAT_1:sch 10( A4, A5);

      reconsider k = (m - n) as non zero Nat by A1, NAT_1: 21;

      (m - k) = n;

      hence thesis by A9;

    end;

    theorem :: CGAMES_1:22

    

     Th22: for f be ConwayGameChain holds for n,m be Element of ( dom f) st n <= m holds ( ConwayRank (f . n)) c= ( ConwayRank (f . m))

    proof

      let f be ConwayGameChain;

      let n,m be Element of ( dom f) such that

       A1: n <= m;

      per cases by A1, XXREAL_0: 1;

        suppose n < m;

        then ( ConwayRank (f . n)) in ( ConwayRank (f . m)) by Th21;

        hence thesis by ORDINAL1:def 2;

      end;

        suppose n = m;

        hence thesis;

      end;

    end;

    theorem :: CGAMES_1:23

    

     Th23: for f be ConwayGameChain st (f . ( len f)) in ( ConwayDay alpha) holds (f . 1) in ( ConwayDay alpha)

    proof

      let f be ConwayGameChain;

      assume

       A1: (f . ( len f)) 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;

      hence (f . 1) in ( ConwayDay alpha) by Th12;

    end;

    

     Lm2: ex f be ConwayGameChain st (f . 1) = g & (f . ( len f)) = g

    proof

      take f = <*g*>;

      ( len f) = 1 by FINSEQ_1: 40;

      hence thesis by FINSEQ_1: 40;

    end;

    definition

      let g;

      :: CGAMES_1:def12

      func the_Tree_of g -> set means

      : Def12: z in it iff ex f be ConwayGameChain st (f . 1) = z & (f . ( len f)) = g;

      existence

      proof

        consider alpha such that

         A1: g in ( ConwayDay alpha) by Def3;

        take s = { x where x be Element of ( ConwayDay alpha) : ex f be ConwayGameChain st (f . 1) = x & (f . ( len f)) = g };

        let z;

        hereby

          assume z in s;

          then

          consider x be Element of ( ConwayDay alpha) such that

           A2: x = z & ex f be ConwayGameChain st (f . 1) = x & (f . ( len f)) = g;

          thus ex f be ConwayGameChain st (f . 1) = z & (f . ( len f)) = g by A2;

        end;

        assume ex f be ConwayGameChain st (f . 1) = z & (f . ( len f)) = g;

        then

        consider f be 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;

      end;

      uniqueness

      proof

        let t1,t2 be set;

        assume

         A4: z in t1 iff ex f be ConwayGameChain st (f . 1) = z & (f . ( len f)) = g;

        assume

         A5: z in t2 iff ex f be ConwayGameChain st (f . 1) = z & (f . ( len f)) = g;

        now

          let z be object;

          hereby

            assume z in t1;

            then ex f be ConwayGameChain st (f . 1) = z & (f . ( len f)) = g by A4;

            hence z in t2 by A5;

          end;

          hereby

            assume z in t2;

            then ex f be ConwayGameChain st (f . 1) = z & (f . ( len f)) = g by A5;

            hence z in t1 by A4;

          end;

        end;

        hence t1 = t2 by TARSKI: 2;

      end;

    end

    registration

      let g;

      cluster ( the_Tree_of g) -> non empty;

      coherence

      proof

        ex f be ConwayGameChain st (f . 1) = g & (f . ( len f)) = g by Lm2;

        hence thesis by Def12;

      end;

    end

    definition

      let g;

      :: CGAMES_1:def13

      func the_proper_Tree_of g -> Subset of ( the_Tree_of g) equals (( the_Tree_of g) \ {g});

      coherence ;

    end

    theorem :: CGAMES_1:24

    

     Th24: g in ( the_Tree_of g)

    proof

      ex f be ConwayGameChain st (f . 1) = g & (f . ( len f)) = g by Lm2;

      hence thesis by Def12;

    end;

    definition

      let alpha;

      let g be Element of ( ConwayDay alpha);

      :: original: the_Tree_of

      redefine

      func the_Tree_of g -> Subset of ( ConwayDay alpha) ;

      coherence

      proof

        ( the_Tree_of g) c= ( ConwayDay alpha)

        proof

          let z be object;

          assume z in ( the_Tree_of g);

          then

          consider f be ConwayGameChain such that

           A1: (f . 1) = z & (f . ( len f)) = g by Def12;

          thus z in ( ConwayDay alpha) by A1, Th23;

        end;

        hence thesis;

      end;

    end

    registration

      let g;

      cluster -> ConwayGame-like for Element of ( the_Tree_of g);

      coherence

      proof

        let g1 be Element of ( the_Tree_of g);

        consider alpha such that

         A1: g in ( ConwayDay alpha) by Def3;

        ex f be ConwayGameChain st (f . 1) = g1 & (f . ( len f)) = g by Def12;

        then g1 in ( ConwayDay alpha) by Th23, A1;

        hence thesis;

      end;

    end

    theorem :: CGAMES_1:25

    

     Th25: for f be ConwayGameChain holds for n be non zero Nat holds (f | n) is ConwayGameChain

    proof

      let f be ConwayGameChain;

      let n be non zero Nat;

      set ls = ( len (f | n));

      

       A1: (f | n) is ConwayGame-valued

      proof

        let x such that

         A2: x in ( dom (f | n));

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

      end;

      reconsider fs = (f | n) as ConwayGame-valued non empty FinSequence by A1;

      fs is ConwayGameChain-like

      proof

        let n be Element of ( dom fs) such that

         A3: n > 1;

        ( 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 thesis by Def11, A3;

      end;

      hence thesis;

    end;

    theorem :: CGAMES_1:26

    

     Th26: for f1,f2 be ConwayGameChain st ex g st g = (f2 . 1) & (f1 . ( len f1)) in ( the_Options_of g) holds (f1 ^ f2) is ConwayGameChain

    proof

      let f1,f2 be ConwayGameChain;

      assume

       A1: ex g st g = (f2 . 1) & (f1 . ( len f1)) in ( the_Options_of g);

      then

      reconsider g = (f2 . 1) as ConwayGame;

      (f1 ^ f2) is ConwayGame-valued

      proof

        let x;

        set y = ((f1 ^ f2) . x);

        assume x in ( dom (f1 ^ f2));

        then y in ( rng (f1 ^ f2)) by FUNCT_1: 3;

        then

         A2: y in (( rng f1) \/ ( rng f2)) by FINSEQ_1: 31;

        per cases by A2, XBOOLE_0:def 3;

          suppose y in ( rng f1);

          then ex z be object st z in ( dom f1) & y = (f1 . z) by FUNCT_1:def 3;

          hence y is ConwayGame;

        end;

          suppose y in ( rng f2);

          then ex z be object st z in ( dom f2) & y = (f2 . z) by FUNCT_1:def 3;

          hence y is ConwayGame;

        end;

      end;

      then

      reconsider f12 = (f1 ^ f2) as ConwayGame-valued non empty FinSequence;

      f12 is ConwayGameChain-like

      proof

        let n be Element of ( dom f12);

        assume

         A3: n > 1;

        per cases by XXREAL_0: 1;

          suppose n < (( len f1) + 1);

          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 thesis by A3, Def11;

        end;

          suppose

           A4: n = (( len f1) + 1);

          ( 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 thesis by A1;

        end;

          suppose

           A5: n > (( len f1) + 1);

          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 thesis by A6, Def11;

        end;

      end;

      hence thesis;

    end;

    theorem :: CGAMES_1:27

    

     Th27: x in ( the_Tree_of g) iff (x = g or ex gO st gO in ( the_Options_of g) & x in ( the_Tree_of gO))

    proof

      hereby

        assume x in ( the_Tree_of g);

        then

        consider f be 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;

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

        thus gO in ( the_Options_of g) by Def11, A3, A1;

        n1 is non zero;

        then

        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;

      end;

      hereby

        assume

         A4: x = g or ex gO st gO in ( the_Options_of g) & x in ( the_Tree_of gO);

        per cases by A4;

          suppose x = g;

          hence x in ( the_Tree_of g) by Th24;

        end;

          suppose ex gO st gO in ( the_Options_of g) & x in ( the_Tree_of gO);

          then

          consider gO such that

           A5: gO in ( the_Options_of g) & x in ( the_Tree_of gO);

          consider f be ConwayGameChain such that

           A6: (f . 1) = x & (f . ( len f)) = gO by A5, Def12;

          ex g1 st g1 = ( <*g*> . 1) & (f . ( len f)) in ( the_Options_of g1)

          proof

            take g;

            thus thesis by A5, A6, FINSEQ_1:def 8;

          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;

        end;

      end;

    end;

    theorem :: CGAMES_1:28

    

     Th28: gO in ( the_Tree_of g) implies (gO = g or ( ConwayRank gO) in ( ConwayRank g))

    proof

      assume gO in ( the_Tree_of g);

      then

      consider f be 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;

      per cases by A2, XXREAL_0: 1;

        suppose m = 1;

        hence thesis by A1;

      end;

        suppose m > 1;

        then ( ConwayRank (f . n)) in ( ConwayRank (f . m)) by Th21;

        hence thesis by A1;

      end;

    end;

    theorem :: CGAMES_1:29

    

     Th29: gO in ( the_Tree_of g) implies ( ConwayRank gO) c= ( ConwayRank g)

    proof

      assume

       A1: gO in ( the_Tree_of g);

      per cases by A1, Th28;

        suppose gO = g;

        hence thesis;

      end;

        suppose ( ConwayRank gO) in ( ConwayRank g);

        hence thesis by ORDINAL1:def 2;

      end;

    end;

    theorem :: CGAMES_1:30

    for s be set st g in s & for g1 st g1 in s holds ( the_Options_of g1) c= s holds ( the_Tree_of g) c= s

    proof

      let s be set such that

       A1: g in s & for g1 st g1 in s holds ( the_Options_of g1) c= s;

      hereby

        let z be object;

        assume z in ( the_Tree_of g);

        then

        consider f be ConwayGameChain such that

         A2: (f . 1) = z & (f . ( len f)) = g by Def12;

        defpred OK[ 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;

         OK[m] by A2, A1;

        then

         A3: ex k st OK[k];

        

         A4: for k st k <> 0 & OK[k] holds ex n st n < k & OK[n]

        proof

          let k;

          assume

           A5: k <> 0 & OK[k];

          then

          reconsider m = (k - 1) as Nat by NAT_1: 20;

          take m;

          thus m < k by XREAL_1: 147;

          then (m + 1) < (k + 1) by XREAL_1: 6;

          hence (m + 1) <= ( len f) by A5, XXREAL_0: 2;

          

           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;

        end;

         OK[ 0 ] from NAT_1:sch 7( A3, A4);

        hence z in s by A2;

      end;

    end;

    theorem :: CGAMES_1:31

    

     Th31: g1 in ( the_Tree_of g2) implies ( the_Tree_of g1) c= ( the_Tree_of g2)

    proof

      assume g1 in ( the_Tree_of g2);

      then

      consider f2 be ConwayGameChain such that

       A1: (f2 . 1) = g1 & (f2 . ( len f2)) = g2 by Def12;

      hereby

        let x be object;

        assume x in ( the_Tree_of g1);

        then

        consider f1 be ConwayGameChain such that

         A2: (f1 . 1) = x & (f1 . ( len f1)) = g1 by Def12;

        

         A3: ( len f1) >= 1 by NAT_1: 14;

        per cases by A3, XXREAL_0: 1;

          suppose ( len f1) = 1;

          hence x in ( the_Tree_of g2) by A1, A2, Def12;

        end;

          suppose

           A4: ( len f1) > 1;

          then

          reconsider n0 = (( len f1) - 1) as non zero 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;

        end;

      end;

    end;

    theorem :: CGAMES_1:32

    

     Th32: g1 in ( the_Tree_of g2) implies ( the_proper_Tree_of g1) c= ( the_proper_Tree_of g2)

    proof

      assume

       A1: g1 in ( the_Tree_of g2);

      then

       A2: ( the_Tree_of g1) c= ( the_Tree_of g2) by Th31;

      let x be object;

      assume

       A3: x in ( the_proper_Tree_of g1);

      then

       A4: x in ( the_Tree_of g1) & x <> g1 by ZFMISC_1: 56;

      assume

       A5: not x in ( the_proper_Tree_of g2);

      then

       A6: x = g2 by A2, A4, ZFMISC_1: 56;

      per cases by Th28, A1;

        suppose g1 = g2;

        hence contradiction by A3, A5;

      end;

        suppose

         A7: ( ConwayRank g1) in ( ConwayRank g2);

        reconsider g = x as ConwayGame by A3;

        ( ConwayRank g) in ( ConwayRank g2) by A7, Th29, A4, ORDINAL1: 12;

        hence contradiction by A6;

      end;

    end;

    theorem :: CGAMES_1:33

    

     Th33: ( the_Options_of g) c= ( the_proper_Tree_of g)

    proof

      let x be object such that

       A1: x in ( the_Options_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 thesis by A1, Th16;

    end;

    theorem :: CGAMES_1:34

    

     Th34: ( the_Options_of g) c= ( the_Tree_of g)

    proof

      ( the_Options_of g) c= ( the_proper_Tree_of g) by Th33;

      hence thesis by XBOOLE_1: 1;

    end;

    theorem :: CGAMES_1:35

    

     Th35: g1 in ( the_proper_Tree_of g2) implies ( the_Tree_of g1) c= ( the_proper_Tree_of g2)

    proof

      assume

       A1: g1 in ( 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);

        then ( ConwayRank g2) c= ( ConwayRank g1) by Th29;

        then ( ConwayRank g1) in ( ConwayRank g1) by A4;

        hence contradiction;

      end;

      hence thesis by A3, ZFMISC_1: 34;

    end;

    theorem :: CGAMES_1:36

    gO in ( the_Options_of g) implies ( the_Tree_of gO) c= ( the_proper_Tree_of g)

    proof

      assume

       A1: gO in ( the_Options_of g);

      ( the_Options_of g) c= ( the_proper_Tree_of g) by Th33;

      hence thesis by Th35, A1;

    end;

    theorem :: CGAMES_1:37

    ( the_Tree_of ConwayZero ) = { ConwayZero } by Th2, ZFMISC_1: 33;

    theorem :: CGAMES_1:38

     ConwayZero in ( the_Tree_of g)

    proof

      defpred Bad[ ConwayGame] means not ConwayZero in ( the_Tree_of $1);

      assume not thesis;

      then

       A1: ex g st Bad[g];

      consider g such that

       A2: Bad[g] & for gO st gO in ( the_Options_of g) holds not Bad[gO] from ConwayGameMin( A1);

      per cases by Th6;

        suppose g = ConwayZero ;

        hence contradiction by Th24, A2;

      end;

        suppose ( the_Options_of g) <> {} ;

        then

        consider x be object 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;

      end;

    end;

    scheme :: CGAMES_1:sch4

    ConwayGameMin2 { P[ ConwayGame] } :

ex g st P[g] & for gO st gO in ( the_proper_Tree_of g) holds not P[gO]

      provided

       A1: ex g st P[g];

      consider g such that

       A2: P[g] & for g1 st ( ConwayRank g1) in ( ConwayRank g) holds not P[g1] from ConwayGameMinTot( A1);

      take g;

      now

        let gO;

        assume gO in ( the_proper_Tree_of g);

        then gO in ( the_Tree_of g) & gO <> g by ZFMISC_1: 56;

        then ( ConwayRank gO) in ( ConwayRank g) by Th28;

        hence not P[gO] by A2;

      end;

      hence thesis by A2;

    end;

    begin

    scheme :: CGAMES_1:sch5

    Func1RecUniq { F( ConwayGame, Function) -> set } :

for g holds for f1,f2 be Function st ( dom f1) = ( the_Tree_of g) & ( dom f2) = ( the_Tree_of g) & (for g1 st g1 in ( dom f1) holds (f1 . g1) = F(g1,|)) & (for g1 st g1 in ( dom f2) holds (f2 . g1) = F(g1,|)) holds f1 = f2;

      let g;

      let f1,f2 be Function such that

       A1: ( dom f1) = ( the_Tree_of g) & ( dom f2) = ( the_Tree_of g) & (for g1 st g1 in ( dom f1) holds (f1 . g1) = F(g1,|)) & (for g1 st g1 in ( dom f2) holds (f2 . g1) = F(g1,|));

      defpred Bad[ ConwayGame] means $1 in ( the_Tree_of g) & (f1 . $1) <> (f2 . $1);

      assume f1 <> f2;

      then ex x be object st x in ( the_Tree_of g) & (f1 . x) <> (f2 . x) by A1;

      then

       A2: ex g0 st Bad[g0];

      consider gm be ConwayGame such that

       A3: Bad[gm] & for gO st gO in ( the_proper_Tree_of gm) holds not Bad[gO] from ConwayGameMin2( A2);

      

       A4: (f1 | ( the_proper_Tree_of gm)) = (f2 | ( the_proper_Tree_of gm))

      proof

        now

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

          

           A7: ( dom f1r) = ( the_proper_Tree_of gm) & ( dom f2r) = ( the_proper_Tree_of gm) by A1, A5, RELAT_1: 62, XBOOLE_1: 1;

          hence ( dom f1r) = ( dom f2r);

          hereby

            let x be object such that

             A8: x in ( dom f1r);

            reconsider g0 = x as ConwayGame by A7, A8;

            (f1 . x) = (f2 . x) & (f1r . x) = (f1 . x) & (f2r . x) = (f2 . x) by A3, A6, A7, A8, FUNCT_1: 47;

            hence (f1r . x) = (f2r . x);

          end;

        end;

        hence thesis;

      end;

      (f1 . gm) = F(gm,|) & (f2 . gm) = F(gm,|) by A1, A3;

      hence contradiction by A4, A3;

    end;

    scheme :: CGAMES_1:sch6

    Func1RecEx { F( ConwayGame, Function) -> set } :

ex f be Function st ( dom f) = ( the_Tree_of g) & for g1 st g1 in ( dom f) holds (f . g1) = F(g1,|);

      defpred GoodFun[ Function] means for g st g in ( dom $1) holds ($1 . g) = F(g,|);

      defpred GoodG[ ConwayGame] means ex f be Function st ( dom f) = ( the_Tree_of $1) & GoodFun[f];

      defpred GF[ object, object] means ex g be ConwayGame st $1 = g & ex f be Function st $2 = f & ( dom f) = ( the_Tree_of g) & GoodFun[f];

      

       A1: for g holds for f1,f2 be Function st ( dom f1) = ( the_Tree_of g) & ( dom f2) = ( the_Tree_of g) & (for g1 st g1 in ( dom f1) holds (f1 . g1) = F(g1,|)) & (for g1 st g1 in ( dom f2) holds (f2 . g1) = F(g1,|)) holds f1 = f2 from Func1RecUniq;

      then

       A2: for x,y,z be object st GF[x, y] & GF[x, z] holds y = z;

      

       A3: for g holds for f be Function st GoodFun[f] holds GoodFun[(f | ( the_Tree_of g))]

      proof

        let g;

        let f be Function such that

         A4: GoodFun[f];

        let g1 such that

         A5: g1 in ( dom (f | ( the_Tree_of g)));

        ( dom (f | ( the_Tree_of g))) c= ( dom f) by RELAT_1: 60;

        then

         A6: (f . g1) = F(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 thesis by A6, RELAT_1: 74, XBOOLE_1: 1;

      end;

      

       A7: for g st (for gO st gO in ( the_Options_of g) holds GoodG[gO]) holds GoodG[g]

      proof

        let g;

        assume

         A8: for gO st gO in ( the_Options_of g) holds GoodG[gO];

        consider FUNCS be set such that

         A9: for y be object holds y in FUNCS iff ex x be object st x in ( the_Tree_of g) & GF[x, y] from TARSKI:sch 1( A2);

        FUNCS is functional compatible

        proof

          thus FUNCS is functional

          proof

            let y be object;

            assume y in FUNCS;

            then ex x be object st x in ( the_Tree_of g) & GF[x, y] by A9;

            hence thesis;

          end;

          now

            let f1,f2 be Function;

            assume f1 in FUNCS;

            then ex x be object st x in ( the_Tree_of g) & GF[x, f1] by A9;

            then

            consider g1 such that

             A10: g1 in ( the_Tree_of g) & ( dom f1) = ( the_Tree_of g1) & GoodFun[f1];

            assume f2 in FUNCS;

            then ex x be object st x in ( the_Tree_of g) & GF[x, f2] by A9;

            then

            consider g2 such that

             A11: g2 in ( the_Tree_of g) & ( dom f2) = ( the_Tree_of g2) & GoodFun[f2];

            thus f1 tolerates f2

            proof

              let x be object;

              assume x in (( dom f1) /\ ( dom f2));

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

              T c= ( dom f1) & T c= ( dom f2) by Th31, A10, A11, A12;

              then ( dom (f1 | T)) = T & ( dom (f2 | T)) = T & GoodFun[(f1 | T)] & GoodFun[(f2 | T)] by A3, A10, A11, RELAT_1: 62;

              then (f1 | T) = (f2 | T) & g0 in ( dom (f1 | T)) & g0 in ( dom (f2 | T)) by A1, Th24;

              then (f1 | T) = (f2 | T) & (f1 . g0) = ((f1 | T) . g0) & (f2 . g0) = ((f2 | T) . g0) by FUNCT_1: 47;

              hence thesis;

            end;

          end;

          hence FUNCS is compatible by COMPUT_1:def 1;

        end;

        then

        reconsider FS = FUNCS as functional compatible set;

        reconsider f = ( union FS) as Function;

        take f;

        

         A13: ( the_proper_Tree_of g) c= ( dom f)

        proof

          let x be object;

          assume x in ( the_proper_Tree_of g);

          then x in ( the_Tree_of g) & x <> g by ZFMISC_1: 56;

          then

          consider gO such that

           A14: gO in ( the_Options_of g) & x in ( the_Tree_of gO) by Th27;

          consider fO be Function such that

           A15: ( dom fO) = ( the_Tree_of gO) & GoodFun[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 thesis;

        end;

        

         A16: ( dom f) c= ( the_Tree_of g)

        proof

          let x be object;

          assume x in ( dom f);

          then [x, (f . x)] in f by FUNCT_1:def 2;

          then ex y st [x, (f . x)] in y & y in FUNCS by TARSKI:def 4;

          then

          consider f1 be Function such that

           A17: [x, (f . x)] in f1 & f1 in FUNCS;

          ex y be object st y in ( the_Tree_of g) & GF[y, f1] by A17, A9;

          then

          consider g1 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);

        end;

        

         A19: GoodFun[f]

        proof

          let g1;

          assume g1 in ( dom f);

          then [g1, (f . g1)] in f by FUNCT_1:def 2;

          then ex x st [g1, (f . g1)] in x & x in FUNCS by TARSKI:def 4;

          then

          consider fO be Function such that

           A20: [g1, (f . g1)] in fO & fO in FUNCS;

          ex x be object st x in ( the_Tree_of g) & GF[x, fO] by A9, A20;

          then

          consider gO such that

           A21: gO in ( the_Tree_of g) & ( dom fO) = ( the_Tree_of gO) & GoodFun[fO];

          

           A22: (fO | ( the_proper_Tree_of g1)) = (f | ( the_proper_Tree_of g1))

          proof

            now

              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;

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

              hereby

                let x be object;

                assume

                 A25: x in ( dom (fO | ( the_proper_Tree_of g1)));

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

              end;

            end;

            hence thesis;

          end;

          g1 in ( the_Tree_of gO) by A20, A21, FUNCT_1: 1;

          then (fO . g1) = F(g1,|) & (fO . g1) = (f . g1) by A21, A20, COMPUT_1: 13;

          hence (f . g1) = F(g1,|) by A22;

        end;

        g in ( dom f)

        proof

          assume

           A26: not g in ( dom f);

          set v = F(g,|);

          ( dom { [g, v]}) = {g} by RELAT_1: 9;

          then { [g, v]} tolerates f by A26, PARTFUN1: 56, ZFMISC_1: 50;

          then

          reconsider h = ( { [g, v]} \/ f) as Function by PARTFUN1: 51;

          

           A27: ( dom h) = (( dom f) \/ ( dom { [g, v]})) by XTUPLE_0: 23;

          then

           A28: ( dom h) = (( dom f) \/ {g}) by RELAT_1: 9;

          

           A29: GF[g, h]

          proof

            take g;

            thus g = g;

            take h;

            thus h = h;

            now

              hereby

                let x be object;

                assume x in ( the_Tree_of g);

                then

                 A30: x in (( {g} /\ ( the_Tree_of g)) \/ (( the_Tree_of g) \ {g})) by XBOOLE_1: 51;

                per cases by A30, XBOOLE_0:def 3;

                  suppose x in ( {g} /\ ( the_Tree_of g));

                  then x in {g} & {g} c= ( dom h) by A28, XBOOLE_0:def 4, XBOOLE_1: 7;

                  hence x in ( dom h);

                end;

                  suppose x in ( the_proper_Tree_of g);

                  then x in ( dom f) & ( dom f) c= ( dom h) by A13, A27, XBOOLE_1: 7;

                  hence x in ( dom h);

                end;

              end;

              hereby

                let x be object;

                assume

                 A31: x in ( dom h);

                per cases by A31, A28, ZFMISC_1: 136;

                  suppose x = g;

                  hence x in ( the_Tree_of g) by Th24;

                end;

                  suppose x in ( dom f);

                  hence x in ( the_Tree_of g) by A16;

                end;

              end;

            end;

            hence

             A32: ( dom h) = ( the_Tree_of g) by TARSKI: 2;

            thus GoodFun[h]

            proof

              let g1;

              assume

               A33: g1 in ( dom h);

              now

                thus (f | ( the_proper_Tree_of g1)) c= (h | ( the_proper_Tree_of g1)) by RELAT_1: 76, XBOOLE_1: 7;

                

                 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;

                thus ( dom (f | ( the_proper_Tree_of g1))) = ( the_proper_Tree_of g1) by A34, A13, RELAT_1: 62, XBOOLE_1: 1;

                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;

              end;

              then

               A36: (h | ( the_proper_Tree_of g1)) = (f | ( the_proper_Tree_of g1)) by GRFUNC_1: 3;

              per cases by A33, A28, ZFMISC_1: 136;

                suppose

                 A37: g1 = g;

                 [g, v] in h by ZFMISC_1: 136;

                hence thesis by A36, A33, A37, FUNCT_1:def 2;

              end;

                suppose

                 A38: g1 in ( dom f);

                f c= h by XBOOLE_1: 7;

                then (f . g1) = (h . g1) by A38, GRFUNC_1: 2;

                hence thesis by A19, A38, A36;

              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;

        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;

        thus GoodFun[f] by A19;

      end;

      for g holds GoodG[g] from ConwayGameInd( A7);

      hence thesis;

    end;

    begin

    

     Lm3: for f be Function holds { ((f | ( the_proper_Tree_of g1)) . gR) where gR be Element of ( the_RightOptions_of g1) : ( the_RightOptions_of g1) <> {} } = { (f . gR) where gR be Element of ( the_RightOptions_of g1) : ( the_RightOptions_of g1) <> {} } & { ((f | ( the_proper_Tree_of g1)) . gL) where gL be Element of ( the_LeftOptions_of g1) : ( the_LeftOptions_of g1) <> {} } = { (f . gL) where gL be Element of ( the_LeftOptions_of g1) : ( the_LeftOptions_of g1) <> {} }

    proof

      let f be Function;

      set R1 = { ((f | ( the_proper_Tree_of g1)) . gR) where gR be Element of ( the_RightOptions_of g1) : ( the_RightOptions_of g1) <> {} };

      set R2 = { (f . gR) where gR be Element of ( the_RightOptions_of g1) : ( the_RightOptions_of g1) <> {} };

      set L1 = { ((f | ( the_proper_Tree_of g1)) . gL) where gL be Element of ( the_LeftOptions_of g1) : ( the_LeftOptions_of g1) <> {} };

      set L2 = { (f . gL) where gL be Element of ( the_LeftOptions_of g1) : ( the_LeftOptions_of g1) <> {} };

      

       A1: for gO 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;

        assume gO in ( the_LeftOptions_of g1) or gO in ( the_RightOptions_of g1);

        then gO in ( the_Options_of g1) & ( the_Options_of g1) c= ( the_proper_Tree_of g1) by Th33, XBOOLE_0:def 3;

        hence thesis by FUNCT_1: 49;

      end;

      now

        hereby

          let x be object;

          assume x in R1;

          then

          consider gR be 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 R2 by A2;

        end;

        hereby

          let x be object;

          assume x in R2;

          then

          consider gR be 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 R1 by A3;

        end;

      end;

      hence R1 = R2 by TARSKI: 2;

      now

        hereby

          let x be object;

          assume x in L1;

          then

          consider gL be 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 L2 by A4;

        end;

        hereby

          let x be object;

          assume x in L2;

          then

          consider gL be 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 L1 by A5;

        end;

      end;

      hence L1 = L2 by TARSKI: 2;

    end;

    definition

      let g;

      :: CGAMES_1:def14

      func - g -> set means

      : Def14: ex f be Function st ( dom f) = ( the_Tree_of g) & it = (f . g) & for g1 st g1 in ( dom f) holds (f . g1) = left-right (# { (f . gR) where gR be Element of ( the_RightOptions_of g1) : ( the_RightOptions_of g1) <> {} }, { (f . gL) where gL be Element of ( the_LeftOptions_of g1) : ( the_LeftOptions_of g1) <> {} } #);

      existence

      proof

        deffunc F( ConwayGame, Function) = left-right (# { ($2 . gR) where gR be Element of ( the_RightOptions_of $1) : ( the_RightOptions_of $1) <> {} }, { ($2 . gL) where gL be Element of ( the_LeftOptions_of $1) : ( the_LeftOptions_of $1) <> {} } #);

        for g holds ex f be Function st ( dom f) = ( the_Tree_of g) & for g1 st g1 in ( dom f) holds (f . g1) = F(g1,|) from Func1RecEx;

        then

        consider f be Function such that

         A1: ( dom f) = ( the_Tree_of g) & for g1 st g1 in ( dom f) holds (f . g1) = F(g1,|);

        take v = (f . g);

        take f;

        thus ( dom f) = ( the_Tree_of g) by A1;

        thus (f . g) = v;

        let g1 such that

         A2: g1 in ( dom f);

        { ((f | ( the_proper_Tree_of g1)) . gR) where gR be Element of ( the_RightOptions_of g1) : ( the_RightOptions_of g1) <> {} } = { (f . gR) where gR be Element of ( the_RightOptions_of g1) : ( the_RightOptions_of g1) <> {} } & { ((f | ( the_proper_Tree_of g1)) . gL) where gL be Element of ( the_LeftOptions_of g1) : ( the_LeftOptions_of g1) <> {} } = { (f . gL) where gL be Element of ( the_LeftOptions_of g1) : ( the_LeftOptions_of g1) <> {} } by Lm3;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        deffunc F( ConwayGame, Function) = left-right (# { ($2 . gR) where gR be Element of ( the_RightOptions_of $1) : ( the_RightOptions_of $1) <> {} }, { ($2 . gL) where gL be Element of ( the_LeftOptions_of $1) : ( the_LeftOptions_of $1) <> {} } #);

        let g1,g2 be set;

        assume ex f1 be Function st ( dom f1) = ( the_Tree_of g) & g1 = (f1 . g) & for g0 st g0 in ( dom f1) holds (f1 . g0) = F(g0,f1);

        then

        consider f1 be Function such that

         A3: ( dom f1) = ( the_Tree_of g) & g1 = (f1 . g) & for g0 st g0 in ( dom f1) holds (f1 . g0) = F(g0,f1);

        assume ex f2 be Function st ( dom f2) = ( the_Tree_of g) & g2 = (f2 . g) & for g0 st g0 in ( dom f2) holds (f2 . g0) = F(g0,f2);

        then

        consider f2 be Function such that

         A4: ( dom f2) = ( the_Tree_of g) & g2 = (f2 . g) & for g0 st g0 in ( dom f2) holds (f2 . g0) = F(g0,f2);

        

         A5: for g0 st g0 in ( dom f1) holds (f1 . g0) = F(g0,|)

        proof

          let g0;

          set LOr = { ((f1 | ( the_proper_Tree_of g0)) . gR) where gR be Element of ( the_RightOptions_of g0) : ( the_RightOptions_of g0) <> {} };

          set ROr = { ((f1 | ( the_proper_Tree_of g0)) . gL) where gL be Element of ( the_LeftOptions_of g0) : ( the_LeftOptions_of g0) <> {} };

          set LOu = { (f1 . gR) where gR be Element of ( the_RightOptions_of g0) : ( the_RightOptions_of g0) <> {} };

          set ROu = { (f1 . gL) where gL be Element of ( the_LeftOptions_of g0) : ( the_LeftOptions_of g0) <> {} };

          LOu = LOr & ROu = ROr by Lm3;

          hence thesis by A3;

        end;

        

         A6: for g0 st g0 in ( dom f2) holds (f2 . g0) = F(g0,|)

        proof

          let g0;

          set LOr = { ((f2 | ( the_proper_Tree_of g0)) . gR) where gR be Element of ( the_RightOptions_of g0) : ( the_RightOptions_of g0) <> {} };

          set ROr = { ((f2 | ( the_proper_Tree_of g0)) . gL) where gL be Element of ( the_LeftOptions_of g0) : ( the_LeftOptions_of g0) <> {} };

          set LOu = { (f2 . gR) where gR be Element of ( the_RightOptions_of g0) : ( the_RightOptions_of g0) <> {} };

          set ROu = { (f2 . gL) where gL be Element of ( the_LeftOptions_of g0) : ( the_LeftOptions_of g0) <> {} };

          LOu = LOr & ROu = ROr by Lm3;

          hence thesis by A4;

        end;

        for g holds for f1,f2 be Function st ( dom f1) = ( the_Tree_of g) & ( dom f2) = ( the_Tree_of g) & (for g1 st g1 in ( dom f1) holds (f1 . g1) = F(g1,|)) & (for g1 st g1 in ( dom f2) holds (f2 . g1) = F(g1,|)) holds f1 = f2 from Func1RecUniq;

        hence thesis by A3, A4, A5, A6;

      end;

    end

    registration

      let g;

      cluster ( - g) -> ConwayGame-like;

      coherence

      proof

        consider f be Function such that

         A1: ( dom f) = ( the_Tree_of g) & ( - g) = (f . g) & for g1 st g1 in ( dom f) holds (f . g1) = left-right (# { (f . gR) where gR be Element of ( the_RightOptions_of g1) : ( the_RightOptions_of g1) <> {} }, { (f . gL) where gL be Element of ( the_LeftOptions_of g1) : ( the_LeftOptions_of g1) <> {} } #) by Def14;

        defpred GV[ ConwayGame] means $1 in ( dom f) implies (f . $1) is ConwayGame;

        

         A2: for g1 st (for gO st gO in ( the_Options_of g1) holds GV[gO]) holds GV[g1]

        proof

          let g1;

          assume

           A3: for gO st gO in ( the_Options_of g1) holds GV[gO];

          assume

           A4: g1 in ( dom f);

          set L = { (f . gR) where gR be Element of ( the_RightOptions_of g1) : ( the_RightOptions_of g1) <> {} };

          set R = { (f . gL) where gL be Element of ( the_LeftOptions_of g1) : ( the_LeftOptions_of g1) <> {} };

          

           A5: (f . g1) = left-right (# L, R #) by A1, A4;

          now

            let z;

            assume

             A6: z in (L \/ R);

            ex gO st gO in ( the_Options_of g1) & z = (f . gO)

            proof

              per cases by A6, XBOOLE_0:def 3;

                suppose z in L;

                then

                consider gR be 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;

                thus thesis by A7, XBOOLE_0:def 3;

              end;

                suppose z in R;

                then

                consider gL be 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;

                thus thesis by A8, XBOOLE_0:def 3;

              end;

            end;

            then

            consider gO 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);

            hence z is ConwayGame by A3, A9;

          end;

          hence thesis by A5, Th19;

        end;

        

         A10: for g holds GV[g] from ConwayGameInd( A2);

        g in ( the_Tree_of g) by Th24;

        hence thesis by A1, A10;

      end;

    end

    

     Lm4: for f be Function st ( dom f) = ( the_Tree_of g) & for g1 st g1 in ( dom f) holds (f . g1) = left-right (# { (f . gR) where gR be Element of ( the_RightOptions_of g1) : ( the_RightOptions_of g1) <> {} }, { (f . gL) where gL be Element of ( the_LeftOptions_of g1) : ( the_LeftOptions_of g1) <> {} } #) holds for g1 st g1 in ( dom f) holds (f . g1) = ( - g1)

    proof

      let f be Function such that

       A1: ( dom f) = ( the_Tree_of g) & for g1 st g1 in ( dom f) holds (f . g1) = left-right (# { (f . gR) where gR be Element of ( the_RightOptions_of g1) : ( the_RightOptions_of g1) <> {} }, { (f . gL) where gL be Element of ( the_LeftOptions_of g1) : ( the_LeftOptions_of g1) <> {} } #);

      let g1 such that

       A2: g1 in ( dom f);

      set f1 = (f | ( the_Tree_of g1));

      

       A3: ( dom f1) = ( the_Tree_of g1) by A1, A2, Th31, RELAT_1: 62;

      now

        let g2 such that

         A4: g2 in ( dom f1);

        set L = { (f . gR) where gR be Element of ( the_RightOptions_of g2) : ( the_RightOptions_of g2) <> {} };

        set L1 = { (f1 . gR) where gR be Element of ( the_RightOptions_of g2) : ( the_RightOptions_of g2) <> {} };

        set R = { (f . gL) where gL be Element of ( the_LeftOptions_of g2) : ( the_LeftOptions_of g2) <> {} };

        set R1 = { (f1 . gL) where gL be Element of ( the_LeftOptions_of g2) : ( the_LeftOptions_of g2) <> {} };

        ( dom f1) c= ( dom f) by RELAT_1: 60;

        then

         A5: (f . g2) = left-right (# L, R #) by A1, A4;

        

         A6: for gO st (gO in ( the_LeftOptions_of g2) or gO in ( the_RightOptions_of g2)) holds (f1 . gO) = (f . gO)

        proof

          let gO;

          assume gO in ( the_LeftOptions_of g2) or gO in ( the_RightOptions_of g2);

          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 f1) by Th31, A4, A3;

          hence thesis by FUNCT_1: 47;

        end;

        now

          hereby

            let x be object;

            assume x in L;

            then

            consider gR be 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 (f1 . gR) = (f . gR) by A6;

            hence x in L1 by A7;

          end;

          hereby

            let x be object;

            assume x in L1;

            then

            consider gR be Element of ( the_RightOptions_of g2) such that

             A8: x = (f1 . gR) & ( the_RightOptions_of g2) <> {} ;

            gR in ( the_RightOptions_of g2) & gR is ConwayGame by A8, Th18;

            then (f1 . gR) = (f . gR) by A6;

            hence x in L by A8;

          end;

        end;

        then

         A9: L = L1 by TARSKI: 2;

        now

          hereby

            let x be object;

            assume x in R;

            then

            consider gL be 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 (f1 . gL) = (f . gL) by A6;

            hence x in R1 by A10;

          end;

          hereby

            let x be object;

            assume x in R1;

            then

            consider gL be Element of ( the_LeftOptions_of g2) such that

             A11: x = (f1 . gL) & ( the_LeftOptions_of g2) <> {} ;

            gL in ( the_LeftOptions_of g2) & gL is ConwayGame by A11, Th18;

            then (f1 . gL) = (f . gL) by A6;

            hence x in R by A11;

          end;

        end;

        then R = R1 by TARSKI: 2;

        hence (f1 . g2) = left-right (# L1, R1 #) by A4, A5, A9, FUNCT_1: 47;

      end;

      then (f1 . g1) = ( - g1) & g1 in ( dom f1) by Def14, A3, Th24;

      hence thesis by FUNCT_1: 47;

    end;

    theorem :: CGAMES_1:39

    

     Th39: (for x holds x in ( the_LeftOptions_of ( - g)) iff ex gR st gR in ( the_RightOptions_of g) & x = ( - gR)) & (for x holds x in ( the_RightOptions_of ( - g)) iff ex gL st gL in ( the_LeftOptions_of g) & x = ( - gL))

    proof

      consider f be Function such that

       A1: ( dom f) = ( the_Tree_of g) & (f . g) = ( - g) & for g1 st g1 in ( dom f) holds (f . g1) = left-right (# { (f . gR) where gR be Element of ( the_RightOptions_of g1) : ( the_RightOptions_of g1) <> {} }, { (f . gL) where gL be Element of ( the_LeftOptions_of g1) : ( the_LeftOptions_of g1) <> {} } #) by Def14;

      

       A2: (gO in ( the_RightOptions_of g) or gO in ( the_LeftOptions_of g)) implies (f . gO) = ( - gO)

      proof

        assume gO in ( the_RightOptions_of g) or gO in ( the_LeftOptions_of g);

        then gO in ( the_Options_of g) & ( the_Options_of g) c= ( the_Tree_of g) by Th34, XBOOLE_0:def 3;

        hence thesis by Lm4, A1;

      end;

      set L = { (f . gR) where gR be Element of ( the_RightOptions_of g) : ( the_RightOptions_of g) <> {} };

      set R = { (f . gL) where gL be Element of ( the_LeftOptions_of g) : ( the_LeftOptions_of g) <> {} };

      ( - g) = left-right (# L, R #) by A1, Th24;

      then

       A3: ( the_LeftOptions_of ( - g)) = L & ( the_RightOptions_of ( - g)) = R by Def6, Def7;

      hereby

        let x;

        hereby

          assume x in ( the_LeftOptions_of ( - g));

          then

          consider gR0 be 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;

          thus gR in ( the_RightOptions_of g) & x = ( - gR) by A4, A2;

        end;

        hereby

          assume ex gR st gR in ( the_RightOptions_of g) & x = ( - gR);

          then

          consider gR 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;

        end;

      end;

      hereby

        let x;

        hereby

          assume x in ( the_RightOptions_of ( - g));

          then

          consider gL0 be 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;

          thus gL in ( the_LeftOptions_of g) & x = ( - gL) by A6, A2;

        end;

        hereby

          assume ex gL st gL in ( the_LeftOptions_of g) & x = ( - gL);

          then

          consider gL 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;

        end;

      end;

    end;

    theorem :: CGAMES_1:40

    

     Th40: ( - ( - g)) = g

    proof

      defpred Bad[ ConwayGame] means ( - ( - $1)) <> $1;

      assume not thesis;

      then

       A1: ex g st Bad[g];

      consider g such that

       A2: Bad[g] & for gO st gO in ( the_Options_of g) holds not Bad[gO] from ConwayGameMin( A1);

      now

        hereby

          let x be object;

          assume x in ( the_LeftOptions_of ( - ( - g)));

          then

          consider gR such that

           A3: gR in ( the_RightOptions_of ( - g)) & x = ( - gR) by Th39;

          consider gL 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;

        end;

        hereby

          let x be object;

          assume

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

        end;

      end;

      then

       A6: ( the_LeftOptions_of ( - ( - g))) = ( the_LeftOptions_of g) by TARSKI: 2;

      now

        hereby

          let x be object;

          assume x in ( the_RightOptions_of ( - ( - g)));

          then

          consider gL such that

           A7: gL in ( the_LeftOptions_of ( - g)) & x = ( - gL) by Th39;

          consider gR 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;

        end;

        hereby

          let x be object;

          assume

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

        end;

      end;

      then ( the_RightOptions_of ( - ( - g))) = ( the_RightOptions_of g) by TARSKI: 2;

      hence contradiction by A2, A6, Th5;

    end;

    theorem :: CGAMES_1:41

    (gO in ( the_LeftOptions_of ( - g)) iff ( - gO) in ( the_RightOptions_of g)) & (gO in ( the_LeftOptions_of g) iff ( - gO) in ( the_RightOptions_of ( - g))) & (gO in ( the_RightOptions_of ( - g)) iff ( - gO) in ( the_LeftOptions_of g)) & (gO in ( the_RightOptions_of g) iff ( - gO) in ( the_LeftOptions_of ( - g)))

    proof

      g = ( - ( - g)) & gO = ( - ( - gO)) by Th40;

      hence thesis by Th39;

    end;

    definition

      let g;

      :: CGAMES_1:def15

      attr g is nonnegative means ex s st g in s & for g1 st g1 in s holds for gR st gR in ( the_RightOptions_of g1) holds ex gRL st gRL in ( the_LeftOptions_of gR) & gRL in s;

    end

    definition

      let g;

      :: CGAMES_1:def16

      attr g is nonpositive means

      : Def16: ( - g) is nonnegative;

    end

    definition

      let g;

      :: CGAMES_1:def17

      attr g is zero means g is nonnegative & g is nonpositive;

      :: CGAMES_1:def18

      attr g is fuzzy means not g is nonnegative & not g is nonpositive;

    end

    definition

      let g;

      :: CGAMES_1:def19

      attr g is positive means g is nonnegative & not g is zero;

      :: CGAMES_1:def20

      attr g is negative means g is nonpositive & not g is zero;

    end

    registration

      cluster zero -> nonnegative nonpositive for ConwayGame;

      coherence ;

      cluster nonpositive nonnegative -> zero for ConwayGame;

      coherence ;

      cluster negative -> nonpositive non zero for ConwayGame;

      coherence ;

      cluster nonpositive non zero -> negative for ConwayGame;

      coherence ;

      cluster positive -> nonnegative non zero for ConwayGame;

      coherence ;

      cluster nonnegative non zero -> positive for ConwayGame;

      coherence ;

      cluster fuzzy -> non nonnegative non nonpositive for ConwayGame;

      coherence ;

      cluster non nonnegative non nonpositive -> fuzzy for ConwayGame;

      coherence ;

    end

    theorem :: CGAMES_1:42

    g is zero or g is positive or g is negative or g is fuzzy;

    theorem :: CGAMES_1:43

    

     Th43: g is nonnegative iff for gR st gR in ( the_RightOptions_of g) holds ex gRL st gRL in ( the_LeftOptions_of gR) & gRL is nonnegative

    proof

      defpred S[ set] means for g st g in $1 holds for gR st gR in ( the_RightOptions_of g) holds ex gRL st gRL in ( the_LeftOptions_of gR) & gRL in $1;

      

       A1: S[s] implies S[(s /\ ( ConwayDay alpha))]

      proof

        assume

         A2: S[s];

        let g;

        assume g in (s /\ ( ConwayDay alpha));

        then

         A3: g in s & g in ( ConwayDay alpha) by XBOOLE_0:def 4;

        let gR;

        assume

         A4: gR in ( the_RightOptions_of g);

        then

        consider gRL such that

         A5: gRL in ( the_LeftOptions_of gR) & gRL in s by A2, A3;

        take gRL;

        gR in ( ConwayDay alpha) by Th11, A3, A4;

        then gRL in ( ConwayDay alpha) by Th11, A5;

        hence thesis by A5, XBOOLE_0:def 4;

      end;

      hereby

        assume g is nonnegative;

        then

        consider s such that

         A6: g in s & S[s];

        let gR;

        assume gR in ( the_RightOptions_of g);

        then

        consider gRL such that

         A7: gRL in ( the_LeftOptions_of gR) & gRL in s by A6;

        take gRL;

        thus gRL in ( the_LeftOptions_of gR) by A7;

        thus gRL is nonnegative by A6, A7;

      end;

      hereby

        assume

         A8: for gR st gR in ( the_RightOptions_of g) holds ex gRL st gRL in ( the_LeftOptions_of gR) & gRL is nonnegative;

        consider alpha such that

         A9: g in ( ConwayDay alpha) by Def3;

        now

          set ss = { s1 where s1 be Subset of ( ConwayDay alpha) : S[s1] };

          take s = ( union ss);

          

           A10: S[s]

          proof

            let g1;

            assume g1 in s;

            then

            consider s2 be set such that

             A11: g1 in s2 & s2 in ss by TARSKI:def 4;

            consider s1 be Subset of ( ConwayDay alpha) such that

             A12: s1 = s2 & S[s1] by A11;

            let gR;

            assume gR in ( the_RightOptions_of g1);

            then

            consider gRL such that

             A13: gRL in ( the_LeftOptions_of gR) & gRL in s1 by A11, A12;

            take gRL;

            s2 c= s by A11, ZFMISC_1: 74;

            hence thesis by A12, A13;

          end;

          thus g in s

          proof

            now

              let x;

              assume x in ss;

              then ex s1 be Subset of ( ConwayDay alpha) st x = s1 & S[s1];

              hence x c= ( ConwayDay alpha);

            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;

             S[sg]

            proof

              let g1 such that

               A15: g1 in sg;

              let gR such that

               A16: gR in ( the_RightOptions_of g1);

              per cases by A15, XBOOLE_0:def 3;

                suppose g1 in s;

                then

                consider gRL such that

                 A17: gRL in ( the_LeftOptions_of gR) & gRL in s by A10, A16;

                take gRL;

                thus gRL in ( the_LeftOptions_of gR) by A17;

                s c= sg by XBOOLE_1: 7;

                hence gRL in sg by A17;

              end;

                suppose g1 in {g};

                then g1 = g by TARSKI:def 1;

                then

                consider gRL such that

                 A18: gRL in ( the_LeftOptions_of gR) & gRL is nonnegative by A8, A16;

                consider s0 be set such that

                 A19: gRL in s0 & S[s0] by A18;

                take gRL;

                thus gRL in ( the_LeftOptions_of gR) by A18;

                reconsider s1 = (s0 /\ ( ConwayDay alpha)) as Subset of ( ConwayDay alpha) by XBOOLE_1: 17;

                 S[s1] by A19, A1;

                then s1 in ss;

                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;

              end;

            end;

            then

             A21: sg in ss;

            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;

          end;

          thus S[s] by A10;

        end;

        hence g is nonnegative;

      end;

    end;

    theorem :: CGAMES_1:44

    

     Th44: g is nonpositive iff for gL st gL in ( the_LeftOptions_of g) holds ex gLR st gLR in ( the_RightOptions_of gL) & gLR is nonpositive

    proof

      hereby

        assume g is nonpositive;

        then

         A1: ( - g) is nonnegative;

        let gL;

        assume gL in ( the_LeftOptions_of g);

        then ( - gL) in ( the_RightOptions_of ( - g)) by Th39;

        then

        consider gRL such that

         A2: gRL in ( the_LeftOptions_of ( - gL)) & gRL is nonnegative by A1, Th43;

        take gLR = ( - gRL);

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

      end;

      assume

       A3: for gL st gL in ( the_LeftOptions_of g) holds ex gLR st gLR in ( the_RightOptions_of gL) & gLR is nonpositive;

      now

        let gR;

        assume gR in ( the_RightOptions_of ( - g));

        then ( - gR) in ( the_LeftOptions_of ( - ( - g))) & ( - ( - g)) = g by Th39, Th40;

        then

        consider gLR such that

         A4: gLR in ( the_RightOptions_of ( - gR)) & gLR is nonpositive by A3;

        take gRL = ( - gLR);

        gRL in ( the_LeftOptions_of ( - ( - gR))) & ( - ( - gR)) = gR by A4, Th39, Th40;

        hence gRL in ( the_LeftOptions_of gR) & gRL is nonnegative by A4;

      end;

      then ( - g) is nonnegative by Th43;

      hence g is nonpositive;

    end;

    theorem :: CGAMES_1:45

    

     Th45: (g is nonnegative iff for gR st gR in ( the_RightOptions_of g) holds gR is fuzzy or gR is positive) & (g is nonpositive iff for gL st gL in ( the_LeftOptions_of g) holds gL is fuzzy or gL is negative)

    proof

      defpred Good[ ConwayGame] means ($1 is nonnegative iff for gR st gR in ( the_RightOptions_of $1) holds gR is fuzzy or gR is positive) & ($1 is nonpositive iff for gL st gL in ( the_LeftOptions_of $1) holds gL is fuzzy or gL is negative);

      

       A1: for g st (for gO st gO in ( the_Options_of g) holds Good[gO]) holds Good[g]

      proof

        let g;

        assume

         A2: for gO st gO in ( the_Options_of g) holds Good[gO];

        hereby

          assume

           A3: g is nonnegative;

          let gR such that

           A4: gR in ( the_RightOptions_of g);

          consider gRL such that

           A5: gRL in ( the_LeftOptions_of gR) & gRL is nonnegative by A3, A4, Th43;

          now

            gR in ( the_Options_of g) by A4, XBOOLE_0:def 3;

            hence Good[gR] by A2;

            hereby

              take gRL;

              thus gRL in ( the_LeftOptions_of gR) by A5;

              thus gRL is non fuzzy non negative by A5;

            end;

          end;

          then gR is non negative non zero;

          hence gR is fuzzy or gR is positive;

        end;

        hereby

          assume

           A6: for gR st gR in ( the_RightOptions_of g) holds gR is fuzzy or gR is positive;

          now

            let gR;

            assume

             A7: gR in ( the_RightOptions_of g);

            now

              gR in ( the_Options_of g) by A7, XBOOLE_0:def 3;

              hence Good[gR] by A2;

              gR is fuzzy or gR is positive by A6, A7;

              hence gR is non nonpositive;

            end;

            then

            consider gRL such that

             A8: gRL in ( the_LeftOptions_of gR) & gRL is non fuzzy non negative;

            take gRL;

            thus gRL in ( the_LeftOptions_of gR) & gRL is nonnegative by A8;

          end;

          hence g is nonnegative by Th43;

        end;

        hereby

          assume

           A9: g is nonpositive;

          let gL such that

           A10: gL in ( the_LeftOptions_of g);

          consider gLR such that

           A11: gLR in ( the_RightOptions_of gL) & gLR is nonpositive by A9, A10, Th44;

          now

            gL in ( the_Options_of g) by A10, XBOOLE_0:def 3;

            hence Good[gL] by A2;

            hereby

              take gLR;

              thus gLR in ( the_RightOptions_of gL) by A11;

              thus gLR is non fuzzy non positive by A11;

            end;

          end;

          then gL is non positive non zero;

          hence gL is fuzzy or gL is negative;

        end;

        hereby

          assume

           A12: for gL st gL in ( the_LeftOptions_of g) holds gL is fuzzy or gL is negative;

          now

            let gL;

            assume

             A13: gL in ( the_LeftOptions_of g);

            now

              gL in ( the_Options_of g) by A13, XBOOLE_0:def 3;

              hence Good[gL] by A2;

              gL is fuzzy or gL is negative by A12, A13;

              hence gL is non nonnegative;

            end;

            then

            consider gLR such that

             A14: gLR in ( the_RightOptions_of gL) & gLR is non fuzzy non positive;

            take gLR;

            thus gLR in ( the_RightOptions_of gL) & gLR is nonpositive by A14;

          end;

          hence g is nonpositive by Th44;

        end;

      end;

      for g holds Good[g] from ConwayGameInd( A1);

      hence thesis;

    end;

    theorem :: CGAMES_1:46

    

     Th46: g is fuzzy iff (ex gL st gL in ( the_LeftOptions_of g) & gL is nonnegative) & (ex gR st gR in ( the_RightOptions_of g) & gR is nonpositive)

    proof

      hereby

        assume

         A1: g is fuzzy;

        hereby

          consider gL such that

           A2: gL in ( the_LeftOptions_of g) & for gLR st gLR in ( the_RightOptions_of gL) holds gLR is non nonpositive by A1, Th44;

          take gL;

          thus gL in ( the_LeftOptions_of g) by A2;

          for gLR st gLR in ( the_RightOptions_of gL) holds gLR is fuzzy or gLR is positive by A2;

          hence gL is nonnegative by Th45;

        end;

        hereby

          consider gR such that

           A3: gR in ( the_RightOptions_of g) & for gRL st gRL in ( the_LeftOptions_of gR) holds gRL is non nonnegative by A1, Th43;

          take gR;

          thus gR in ( the_RightOptions_of g) by A3;

          for gRL st gRL in ( the_LeftOptions_of gR) holds gRL is fuzzy or gRL is negative by A3;

          hence gR is nonpositive by Th45;

        end;

      end;

      hereby

        assume ex gL st gL in ( the_LeftOptions_of g) & gL is nonnegative;

        then

        consider gL such that

         A4: gL in ( the_LeftOptions_of g) & gL is nonnegative;

        assume ex gR st gR in ( the_RightOptions_of g) & gR is nonpositive;

        then

        consider gR such that

         A5: gR in ( the_RightOptions_of g) & gR is nonpositive;

        gL is non fuzzy non negative & gR is non fuzzy non positive by A4, A5;

        then g is non nonpositive & g is non nonnegative by Th45, A4, A5;

        hence g is fuzzy;

      end;

    end;

    theorem :: CGAMES_1:47

    

     Th47: g is zero iff (for gL st gL in ( the_LeftOptions_of g) holds gL is fuzzy or gL is negative) & (for gR st gR in ( the_RightOptions_of g) holds gR is fuzzy or gR is positive) by Th45;

    theorem :: CGAMES_1:48

    

     Th48: g is positive iff (for gR st gR in ( the_RightOptions_of g) holds gR is fuzzy or gR is positive) & (ex gL st gL in ( the_LeftOptions_of g) & gL is nonnegative)

    proof

      hereby

        assume

         A1: g is positive;

        hence

         A2: for gR st gR in ( the_RightOptions_of g) holds gR is fuzzy or gR is positive by Th45;

        consider gL such that

         A3: gL in ( the_LeftOptions_of g) & gL is non fuzzy non negative by Th47, A1, A2;

        take gL;

        thus gL in ( the_LeftOptions_of g) & gL is nonnegative by A3;

      end;

      hereby

        assume for gR st gR in ( the_RightOptions_of g) holds gR is fuzzy or gR is positive;

        then

         A4: g is nonnegative by Th45;

        assume ex gL st gL in ( the_LeftOptions_of g) & gL is nonnegative;

        then

        consider gL such that

         A5: gL in ( the_LeftOptions_of g) & gL is nonnegative;

        gL is non fuzzy non negative by A5;

        then not g is zero by Th47, A5;

        hence g is positive by A4;

      end;

    end;

    theorem :: CGAMES_1:49

    g is negative iff (for gL st gL in ( the_LeftOptions_of g) holds gL is fuzzy or gL is negative) & (ex gR st gR in ( the_RightOptions_of g) & gR is nonpositive)

    proof

      hereby

        assume

         A1: g is negative;

        hence

         A2: for gL st gL in ( the_LeftOptions_of g) holds gL is fuzzy or gL is negative by Th45;

        consider gR such that

         A3: gR in ( the_RightOptions_of g) & gR is non fuzzy non positive by Th47, A1, A2;

        take gR;

        thus gR in ( the_RightOptions_of g) & gR is nonpositive by A3;

      end;

      hereby

        assume for gL st gL in ( the_LeftOptions_of g) holds gL is fuzzy or gL is negative;

        then

         A4: g is nonpositive by Th45;

        assume ex gR st gR in ( the_RightOptions_of g) & gR is nonpositive;

        then

        consider gR such that

         A5: gR in ( the_RightOptions_of g) & gR is nonpositive;

        gR is non fuzzy non positive by A5;

        then not g is zero by Th47, A5;

        hence g is negative by A4;

      end;

    end;

    registration

      cluster ConwayZero -> zero;

      coherence

      proof

        (for gL st gL in ( the_LeftOptions_of ConwayZero ) holds gL is fuzzy or gL is negative) & (for gR st gR in ( the_RightOptions_of ConwayZero ) holds gR is fuzzy or gR is positive);

        hence thesis by Th47;

      end;

    end

    registration

      cluster ConwayOne -> positive;

      coherence

      proof

        set gL = ConwayZero ;

        gL in ( the_LeftOptions_of ConwayOne ) & gL is nonnegative & for gR st gR in ( the_RightOptions_of ConwayOne ) holds gR is fuzzy or gR is positive by Th7;

        hence thesis by Th48;

      end;

      cluster ConwayStar -> fuzzy;

      coherence

      proof

        set gL = ConwayZero ;

        gL in ( the_LeftOptions_of ConwayStar ) & gL is nonnegative & gL in ( the_RightOptions_of ConwayStar ) & gL is nonpositive by Th8;

        hence thesis by Th46;

      end;

    end

    registration

      cluster zero for ConwayGame;

      existence

      proof

        take ConwayZero ;

        thus thesis;

      end;

      cluster positive for ConwayGame;

      existence

      proof

        take ConwayOne ;

        thus thesis;

      end;

      cluster fuzzy for ConwayGame;

      existence

      proof

        take ConwayStar ;

        thus thesis;

      end;

    end

    registration

      let g be nonpositive ConwayGame;

      cluster ( - g) -> nonnegative;

      coherence by Def16;

    end

    registration

      let g be nonnegative ConwayGame;

      cluster ( - g) -> nonpositive;

      coherence by Th40;

    end

    registration

      let g be positive ConwayGame;

      cluster ( - g) -> negative;

      coherence

      proof

        g = ( - ( - g)) by Th40;

        then ( - g) is non zero nonpositive;

        hence thesis;

      end;

    end

    registration

      cluster negative for ConwayGame;

      existence

      proof

        take ( - ConwayOne );

        thus thesis;

      end;

    end

    registration

      let g be negative ConwayGame;

      cluster ( - g) -> positive;

      coherence

      proof

        g = ( - ( - g)) by Th40;

        then ( - g) is non zero nonnegative;

        hence thesis;

      end;

    end

    registration

      let g be fuzzy ConwayGame;

      cluster ( - g) -> fuzzy;

      coherence

      proof

        g = ( - ( - g)) by Th40;

        then ( - g) is non positive non negative non zero;

        hence thesis;

      end;

    end