:: by Robin Nittka

::

:: Received October 13, 2010

:: Copyright (c) 2010-2018 Association of Mizar Users

definition

attr c_{1} is strict ;

struct left-right -> ;

aggr left-right(# LeftOptions, RightOptions #) -> left-right ;

sel LeftOptions c_{1} -> set ;

sel RightOptions c_{1} -> set ;

end;
struct left-right -> ;

aggr left-right(# LeftOptions, RightOptions #) -> left-right ;

sel LeftOptions c

sel RightOptions c

registration
end;

deffunc H

defpred S

$1 . beta = H

Lm1: for f being Sequence st S

for alpha being Ordinal holds S

proof end;

definition

let alpha be Ordinal;

ex b_{1} being set ex f being Sequence st

( alpha in dom f & f . alpha = b_{1} & ( for beta being Ordinal st beta in dom f holds

f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) )

for b_{1}, b_{2} being set st ex f being Sequence st

( alpha in dom f & f . alpha = b_{1} & ( for beta being Ordinal st beta in dom f holds

f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) ) & ex f being Sequence st

( alpha in dom f & f . alpha = b_{2} & ( for beta being Ordinal st beta in dom f holds

f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) ) holds

b_{1} = b_{2}

end;
func ConwayDay alpha -> set means :Def2: :: CGAMES_1:def 2

ex f being Sequence st

( alpha in dom f & f . alpha = it & ( for beta being Ordinal st beta in dom f holds

f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) );

existence ex f being Sequence st

( alpha in dom f & f . alpha = it & ( for beta being Ordinal st beta in dom f holds

f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) );

ex b

( alpha in dom f & f . alpha = b

f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) )

proof end;

uniqueness for b

( alpha in dom f & f . alpha = b

f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) ) & ex f being Sequence st

( alpha in dom f & f . alpha = b

f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) ) holds

b

proof end;

:: deftheorem Def2 defines ConwayDay CGAMES_1:def 2 :

for alpha being Ordinal

for b_{2} being set holds

( b_{2} = ConwayDay alpha iff ex f being Sequence st

( alpha in dom f & f . alpha = b_{2} & ( for beta being Ordinal st beta in dom f holds

f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) ) );

for alpha being Ordinal

for b

( b

( alpha in dom f & f . alpha = b

f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) ) );

theorem Th1: :: CGAMES_1:1

for alpha being Ordinal

for z being object holds

( z in ConwayDay alpha iff ex w being strict left-right st

( z = w & ( for x being set st x in the LeftOptions of w \/ the RightOptions of w holds

ex beta being Ordinal st

( beta in alpha & x in ConwayDay beta ) ) ) )

for z being object holds

( z in ConwayDay alpha iff ex w being strict left-right st

( z = w & ( for x being set st x in the LeftOptions of w \/ the RightOptions of w holds

ex beta being Ordinal st

( beta in alpha & x in ConwayDay beta ) ) ) )

proof end;

definition

let x be set ;

end;
attr x is ConwayGame-like means :Def3: :: CGAMES_1:def 3

ex alpha being Ordinal st x in ConwayDay alpha;

ex alpha being Ordinal st x in ConwayDay alpha;

:: deftheorem Def3 defines ConwayGame-like CGAMES_1:def 3 :

for x being set holds

( x is ConwayGame-like iff ex alpha being Ordinal st x in ConwayDay alpha );

for x being set holds

( x is ConwayGame-like iff ex alpha being Ordinal st x in ConwayDay alpha );

registration

let alpha be Ordinal;

coherence

for b_{1} being Element of ConwayDay alpha holds b_{1} is ConwayGame-like
;

end;
coherence

for b

registration
end;

registration

existence

ex b_{1} being left-right st

( b_{1} is ConwayGame-like & b_{1} is strict )

ex b_{1} being set st b_{1} is ConwayGame-like

end;
ex b

( b

proof end;

existence ex b

proof end;

definition

:: original: ConwayZero

redefine func ConwayZero -> Element of ConwayDay 0;

coherence

ConwayZero is Element of ConwayDay 0 by Th2, TARSKI:def 1;

end;
redefine func ConwayZero -> Element of ConwayDay 0;

coherence

ConwayZero is Element of ConwayDay 0 by Th2, TARSKI:def 1;

definition

coherence

left-right(# {ConwayZero},{} #) is Element of ConwayDay 1

left-right(# {ConwayZero},{ConwayZero} #) is Element of ConwayDay 1

end;
left-right(# {ConwayZero},{} #) is Element of ConwayDay 1

proof end;

func ConwayStar -> Element of ConwayDay 1 equals :: CGAMES_1:def 5

left-right(# {ConwayZero},{ConwayZero} #);

coherence left-right(# {ConwayZero},{ConwayZero} #);

left-right(# {ConwayZero},{ConwayZero} #) is Element of ConwayDay 1

proof end;

:: deftheorem defines ConwayStar CGAMES_1:def 5 :

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

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

registration
end;

definition

let g be ConwayGame;

ex b_{1} being set ex w being left-right st

( g = w & b_{1} = the LeftOptions of w )

for b_{1}, b_{2} being set st ex w being left-right st

( g = w & b_{1} = the LeftOptions of w ) & ex w being left-right st

( g = w & b_{2} = the LeftOptions of w ) holds

b_{1} = b_{2}
;

ex b_{1} being set ex w being left-right st

( g = w & b_{1} = the RightOptions of w )

for b_{1}, b_{2} being set st ex w being left-right st

( g = w & b_{1} = the RightOptions of w ) & ex w being left-right st

( g = w & b_{2} = the RightOptions of w ) holds

b_{1} = b_{2}
;

end;
func the_LeftOptions_of g -> set means :Def6: :: CGAMES_1:def 6

ex w being left-right st

( g = w & it = the LeftOptions of w );

existence ex w being left-right st

( g = w & it = the LeftOptions of w );

ex b

( g = w & b

proof end;

uniqueness for b

( g = w & b

( g = w & b

b

func the_RightOptions_of g -> set means :Def7: :: CGAMES_1:def 7

ex w being left-right st

( g = w & it = the RightOptions of w );

existence ex w being left-right st

( g = w & it = the RightOptions of w );

ex b

( g = w & b

proof end;

uniqueness for b

( g = w & b

( g = w & b

b

:: deftheorem Def6 defines the_LeftOptions_of CGAMES_1:def 6 :

for g being ConwayGame

for b_{2} being set holds

( b_{2} = the_LeftOptions_of g iff ex w being left-right st

( g = w & b_{2} = the LeftOptions of w ) );

for g being ConwayGame

for b

( b

( g = w & b

:: deftheorem Def7 defines the_RightOptions_of CGAMES_1:def 7 :

for g being ConwayGame

for b_{2} being set holds

( b_{2} = the_RightOptions_of g iff ex w being left-right st

( g = w & b_{2} = the RightOptions of w ) );

for g being ConwayGame

for b

( b

( g = w & b

definition

let g be ConwayGame;

coherence

(the_LeftOptions_of g) \/ (the_RightOptions_of g) is set ;

;

end;
func the_Options_of g -> set equals :: CGAMES_1:def 8

(the_LeftOptions_of g) \/ (the_RightOptions_of g);

correctness (the_LeftOptions_of g) \/ (the_RightOptions_of g);

coherence

(the_LeftOptions_of g) \/ (the_RightOptions_of g) is set ;

;

:: deftheorem defines the_Options_of CGAMES_1:def 8 :

for g being ConwayGame holds the_Options_of g = (the_LeftOptions_of g) \/ (the_RightOptions_of g);

for g being ConwayGame holds the_Options_of g = (the_LeftOptions_of g) \/ (the_RightOptions_of g);

theorem Th5: :: CGAMES_1:5

for g1, g2 being ConwayGame holds

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

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

proof end;

registration

coherence

the_LeftOptions_of ConwayZero is empty by Def6;

coherence

the_RightOptions_of ConwayZero is empty by Def7;

coherence

the_RightOptions_of ConwayOne is empty by Def7;

end;
the_LeftOptions_of ConwayZero is empty by Def6;

coherence

the_RightOptions_of ConwayZero is empty by Def7;

coherence

the_RightOptions_of ConwayOne is empty by Def7;

theorem Th8: :: CGAMES_1:8

for x being set holds

( ( x in the_Options_of ConwayStar implies x = ConwayZero ) & ( x = ConwayZero implies x in the_Options_of ConwayStar ) & ( x in the_LeftOptions_of ConwayStar implies x = ConwayZero ) & ( x = ConwayZero implies x in the_LeftOptions_of ConwayStar ) & ( x in the_RightOptions_of ConwayStar implies x = ConwayZero ) & ( x = ConwayZero implies x in the_RightOptions_of ConwayStar ) )

( ( x in the_Options_of ConwayStar implies x = ConwayZero ) & ( x = ConwayZero implies x in the_Options_of ConwayStar ) & ( x in the_LeftOptions_of ConwayStar implies x = ConwayZero ) & ( x = ConwayZero implies x in the_LeftOptions_of ConwayStar ) & ( x in the_RightOptions_of ConwayStar implies x = ConwayZero ) & ( x = ConwayZero implies x in the_RightOptions_of ConwayStar ) )

proof end;

theorem Th9: :: CGAMES_1:9

for alpha being Ordinal

for g being ConwayGame holds

( g in ConwayDay alpha iff for x being set st x in the_Options_of g holds

ex beta being Ordinal st

( beta in alpha & x in ConwayDay beta ) )

for g being ConwayGame holds

( g in ConwayDay alpha iff for x being set st x in the_Options_of g holds

ex beta being Ordinal st

( beta in alpha & x in ConwayDay beta ) )

proof end;

definition

let g be set ;

assume A1: g is ConwayGame ;

ex b_{1} being Ordinal st

( g in ConwayDay b_{1} & ( for beta being Ordinal st beta in b_{1} holds

not g in ConwayDay beta ) )

for b_{1}, b_{2} being Ordinal st g in ConwayDay b_{1} & ( for beta being Ordinal st beta in b_{1} holds

not g in ConwayDay beta ) & g in ConwayDay b_{2} & ( for beta being Ordinal st beta in b_{2} holds

not g in ConwayDay beta ) holds

b_{1} = b_{2}

end;
assume A1: g is ConwayGame ;

func ConwayRank g -> Ordinal means :Def9: :: CGAMES_1:def 9

( g in ConwayDay it & ( for beta being Ordinal st beta in it holds

not g in ConwayDay beta ) );

existence ( g in ConwayDay it & ( for beta being Ordinal st beta in it holds

not g in ConwayDay beta ) );

ex b

( g in ConwayDay b

not g in ConwayDay beta ) )

proof end;

uniqueness for b

not g in ConwayDay beta ) & g in ConwayDay b

not g in ConwayDay beta ) holds

b

proof end;

:: deftheorem Def9 defines ConwayRank CGAMES_1:def 9 :

for g being set st g is ConwayGame holds

for b_{2} being Ordinal holds

( b_{2} = ConwayRank g iff ( g in ConwayDay b_{2} & ( for beta being Ordinal st beta in b_{2} holds

not g in ConwayDay beta ) ) );

for g being set st g is ConwayGame holds

for b

( b

not g in ConwayDay beta ) ) );

theorem Th10: :: CGAMES_1:10

for x being set

for alpha being Ordinal

for g being ConwayGame st g in ConwayDay alpha & x in the_Options_of g holds

x in ConwayDay alpha

for alpha being Ordinal

for g being ConwayGame st g in ConwayDay alpha & x in the_Options_of g holds

x in ConwayDay alpha

proof end;

theorem Th11: :: CGAMES_1:11

for x being set

for alpha being Ordinal

for g being ConwayGame st g in ConwayDay alpha & ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) holds

x in ConwayDay alpha

for alpha being Ordinal

for g being ConwayGame st g in ConwayDay alpha & ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) holds

x in ConwayDay alpha

proof end;

theorem Th12: :: CGAMES_1:12

for alpha being Ordinal

for g being ConwayGame holds

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

for g being ConwayGame holds

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

proof end;

theorem Th13: :: CGAMES_1:13

for alpha being Ordinal

for g being ConwayGame holds

( ConwayRank g in alpha iff ex beta being Ordinal st

( beta in alpha & g in ConwayDay beta ) )

for g being ConwayGame holds

( ConwayRank g in alpha iff ex beta being Ordinal st

( beta in alpha & g in ConwayDay beta ) )

proof end;

theorem :: CGAMES_1:15

for g, gO being ConwayGame st ( gO in the_LeftOptions_of g or gO in the_RightOptions_of g ) holds

ConwayRank gO in ConwayRank g

ConwayRank gO in ConwayRank g

proof end;

theorem Th17: :: CGAMES_1:17

for x being set

for g being ConwayGame st x in the_Options_of g holds

x is ConwayGame-like left-right

for g being ConwayGame st x in the_Options_of g holds

x is ConwayGame-like left-right

proof end;

theorem Th18: :: CGAMES_1:18

for x being set

for g being ConwayGame st ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) holds

x is ConwayGame-like left-right

for g being ConwayGame st ( x in the_LeftOptions_of g or x in the_RightOptions_of g ) holds

x is ConwayGame-like left-right

proof end;

theorem Th19: :: CGAMES_1:19

for w being strict left-right holds

( w is ConwayGame iff for z being set st z in the LeftOptions of w \/ the RightOptions of w holds

z is ConwayGame )

( w is ConwayGame iff for z being set st z in the LeftOptions of w \/ the RightOptions of w holds

z is ConwayGame )

proof end;

scheme :: CGAMES_1:sch 1

ConwayGameMinTot{ P_{1}[ ConwayGame] } :

ConwayGameMinTot{ P

ex g being ConwayGame st

( P_{1}[g] & ( for g1 being ConwayGame st ConwayRank g1 in ConwayRank g holds

not P_{1}[g1] ) )

provided
( P

not P

proof end;

scheme :: CGAMES_1:sch 2

ConwayGameMin{ P_{1}[ ConwayGame] } :

ConwayGameMin{ P

ex g being ConwayGame st

( P_{1}[g] & ( for gO being ConwayGame st gO in the_Options_of g holds

not P_{1}[gO] ) )

provided
( P

not P

proof end;

scheme :: CGAMES_1:sch 3

ConwayGameInd{ P_{1}[ ConwayGame] } :

provided

ConwayGameInd{ P

provided

A1:
for g being ConwayGame st ( for gO being ConwayGame st gO in the_Options_of g holds

P_{1}[gO] ) holds

P_{1}[g]

P

P

proof end;

definition

let f be Function;

end;
attr f is ConwayGame-valued means :Def10: :: CGAMES_1:def 10

for x being set st x in dom f holds

f . x is ConwayGame;

for x being set st x in dom f holds

f . x is ConwayGame;

:: deftheorem Def10 defines ConwayGame-valued CGAMES_1:def 10 :

for f being Function holds

( f is ConwayGame-valued iff for x being set st x in dom f holds

f . x is ConwayGame );

for f being Function holds

( f is ConwayGame-valued iff for x being set st x in dom f holds

f . x is ConwayGame );

registration

ex b_{1} being FinSequence st

( b_{1} is ConwayGame-valued & not b_{1} is empty )
end;

cluster Relation-like omega -defined Function-like non empty V41() FinSequence-like FinSubsequence-like ConwayGame-valued for FinSequence;

existence ex b

( b

proof end;

registration

let f be non empty FinSequence;

coherence

for b_{1} being Element of dom f holds

( b_{1} is natural & not b_{1} is empty )
by FINSEQ_3:24;

end;
coherence

for b

( b

registration

let f be non empty ConwayGame-valued Function;

let x be Element of dom f;

coherence

f . x is ConwayGame-like by Def10;

end;
let x be Element of dom f;

coherence

f . x is ConwayGame-like by Def10;

definition

let f be non empty ConwayGame-valued FinSequence;

end;
attr f is ConwayGameChain-like means :Def11: :: CGAMES_1:def 11

for n being Element of dom f st n > 1 holds

f . (n - 1) in the_Options_of (f . n);

for n being Element of dom f st n > 1 holds

f . (n - 1) in the_Options_of (f . n);

:: deftheorem Def11 defines ConwayGameChain-like CGAMES_1:def 11 :

for f being non empty ConwayGame-valued FinSequence holds

( f is ConwayGameChain-like iff for n being Element of dom f st n > 1 holds

f . (n - 1) in the_Options_of (f . n) );

for f being non empty ConwayGame-valued FinSequence holds

( f is ConwayGameChain-like iff for n being Element of dom f st n > 1 holds

f . (n - 1) in the_Options_of (f . n) );

registration

ex b_{1} being non empty ConwayGame-valued FinSequence st b_{1} is ConwayGameChain-like
end;

cluster Relation-like omega -defined Function-like non empty V41() FinSequence-like FinSubsequence-like ConwayGame-valued ConwayGameChain-like for FinSequence;

existence ex b

proof end;

definition
end;

theorem Th21: :: CGAMES_1:21

for f being ConwayGameChain

for n, m being Element of dom f st n < m holds

ConwayRank (f . n) in ConwayRank (f . m)

for n, m being Element of dom f st n < m holds

ConwayRank (f . n) in ConwayRank (f . m)

proof end;

theorem Th22: :: CGAMES_1:22

for f being ConwayGameChain

for n, m being Element of dom f st n <= m holds

ConwayRank (f . n) c= ConwayRank (f . m)

for n, m being Element of dom f st n <= m holds

ConwayRank (f . n) c= ConwayRank (f . m)

proof end;

theorem Th23: :: CGAMES_1:23

for alpha being Ordinal

for f being ConwayGameChain st f . (len f) in ConwayDay alpha holds

f . 1 in ConwayDay alpha

for f being ConwayGameChain st f . (len f) in ConwayDay alpha holds

f . 1 in ConwayDay alpha

proof end;

Lm2: for g being ConwayGame ex f being ConwayGameChain st

( f . 1 = g & f . (len f) = g )

proof end;

definition

let g be ConwayGame;

ex b_{1} being set st

for z being set holds

( z in b_{1} iff ex f being ConwayGameChain st

( f . 1 = z & f . (len f) = g ) )

for b_{1}, b_{2} being set st ( for z being set holds

( z in b_{1} iff ex f being ConwayGameChain st

( f . 1 = z & f . (len f) = g ) ) ) & ( for z being set holds

( z in b_{2} iff ex f being ConwayGameChain st

( f . 1 = z & f . (len f) = g ) ) ) holds

b_{1} = b_{2}

end;
func the_Tree_of g -> set means :Def12: :: CGAMES_1:def 12

for z being set holds

( z in it iff ex f being ConwayGameChain st

( f . 1 = z & f . (len f) = g ) );

existence for z being set holds

( z in it iff ex f being ConwayGameChain st

( f . 1 = z & f . (len f) = g ) );

ex b

for z being set holds

( z in b

( f . 1 = z & f . (len f) = g ) )

proof end;

uniqueness for b

( z in b

( f . 1 = z & f . (len f) = g ) ) ) & ( for z being set holds

( z in b

( f . 1 = z & f . (len f) = g ) ) ) holds

b

proof end;

:: deftheorem Def12 defines the_Tree_of CGAMES_1:def 12 :

for g being ConwayGame

for b_{2} being set holds

( b_{2} = the_Tree_of g iff for z being set holds

( z in b_{2} iff ex f being ConwayGameChain st

( f . 1 = z & f . (len f) = g ) ) );

for g being ConwayGame

for b

( b

( z in b

( f . 1 = z & f . (len f) = g ) ) );

definition

let g be ConwayGame;

(the_Tree_of g) \ {g} is Subset of (the_Tree_of g) ;

end;
func the_proper_Tree_of g -> Subset of (the_Tree_of g) equals :: CGAMES_1:def 13

(the_Tree_of g) \ {g};

coherence (the_Tree_of g) \ {g};

(the_Tree_of g) \ {g} is Subset of (the_Tree_of g) ;

:: deftheorem defines the_proper_Tree_of CGAMES_1:def 13 :

for g being ConwayGame holds the_proper_Tree_of g = (the_Tree_of g) \ {g};

for g being ConwayGame holds the_proper_Tree_of g = (the_Tree_of g) \ {g};

definition

let alpha be Ordinal;

let g be Element of ConwayDay alpha;

:: original: the_Tree_of

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

coherence

the_Tree_of g is Subset of (ConwayDay alpha)

end;
let g be Element of ConwayDay alpha;

:: original: the_Tree_of

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

coherence

the_Tree_of g is Subset of (ConwayDay alpha)

proof end;

registration

let g be ConwayGame;

coherence

for b_{1} being Element of the_Tree_of g holds b_{1} is ConwayGame-like

end;
coherence

for b

proof end;

theorem Th26: :: CGAMES_1:26

for f1, f2 being ConwayGameChain st ex g being ConwayGame st

( g = f2 . 1 & f1 . (len f1) in the_Options_of g ) holds

f1 ^ f2 is ConwayGameChain

( g = f2 . 1 & f1 . (len f1) in the_Options_of g ) holds

f1 ^ f2 is ConwayGameChain

proof end;

theorem Th27: :: CGAMES_1:27

for x being set

for g being ConwayGame holds

( x in the_Tree_of g iff ( x = g or ex gO being ConwayGame st

( gO in the_Options_of g & x in the_Tree_of gO ) ) )

for g being ConwayGame holds

( x in the_Tree_of g iff ( x = g or ex gO being ConwayGame st

( gO in the_Options_of g & x in the_Tree_of gO ) ) )

proof end;

theorem Th28: :: CGAMES_1:28

for g, gO being ConwayGame holds

( not gO in the_Tree_of g or gO = g or ConwayRank gO in ConwayRank g )

( not gO in the_Tree_of g or gO = g or ConwayRank gO in ConwayRank g )

proof end;

theorem :: CGAMES_1:30

for g being ConwayGame

for s being set st g in s & ( for g1 being ConwayGame st g1 in s holds

the_Options_of g1 c= s ) holds

the_Tree_of g c= s

for s being set st g in s & ( for g1 being ConwayGame st g1 in s holds

the_Options_of g1 c= s ) holds

the_Tree_of g c= s

proof end;

theorem Th32: :: CGAMES_1:32

for g1, g2 being ConwayGame st g1 in the_Tree_of g2 holds

the_proper_Tree_of g1 c= the_proper_Tree_of g2

the_proper_Tree_of g1 c= the_proper_Tree_of g2

proof end;

theorem Th35: :: CGAMES_1:35

for g1, g2 being ConwayGame st g1 in the_proper_Tree_of g2 holds

the_Tree_of g1 c= the_proper_Tree_of g2

the_Tree_of g1 c= the_proper_Tree_of g2

proof end;

scheme :: CGAMES_1:sch 4

ConwayGameMin2{ P_{1}[ ConwayGame] } :

ConwayGameMin2{ P

ex g being ConwayGame st

( P_{1}[g] & ( for gO being ConwayGame st gO in the_proper_Tree_of g holds

not P_{1}[gO] ) )

provided
( P

not P

proof end;

scheme :: CGAMES_1:sch 5

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

Func1RecUniq{ F

for g being ConwayGame

for f1, f2 being Function st dom f1 = the_Tree_of g & dom f2 = the_Tree_of g & ( for g1 being ConwayGame st g1 in dom f1 holds

f1 . g1 = F_{1}(g1,(f1 | (the_proper_Tree_of g1))) ) & ( for g1 being ConwayGame st g1 in dom f2 holds

f2 . g1 = F_{1}(g1,(f2 | (the_proper_Tree_of g1))) ) holds

f1 = f2

for f1, f2 being Function st dom f1 = the_Tree_of g & dom f2 = the_Tree_of g & ( for g1 being ConwayGame st g1 in dom f1 holds

f1 . g1 = F

f2 . g1 = F

f1 = f2

proof end;

scheme :: CGAMES_1:sch 6

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

Func1RecEx{ F

for g being ConwayGame ex f being Function st

( dom f = the_Tree_of g & ( for g1 being ConwayGame st g1 in dom f holds

f . g1 = F_{1}(g1,(f | (the_proper_Tree_of g1))) ) )

( dom f = the_Tree_of g & ( for g1 being ConwayGame st g1 in dom f holds

f . g1 = F

proof end;

Lm3: for g1 being ConwayGame

for f being Function holds

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

proof end;

definition

let g be ConwayGame;

ex b_{1} being set ex f being Function st

( dom f = the_Tree_of g & b_{1} = f . g & ( for g1 being ConwayGame st g1 in dom f holds

f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) )

for b_{1}, b_{2} being set st ex f being Function st

( dom f = the_Tree_of g & b_{1} = f . g & ( for g1 being ConwayGame st g1 in dom f holds

f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) ) & ex f being Function st

( dom f = the_Tree_of g & b_{2} = f . g & ( for g1 being ConwayGame st g1 in dom f holds

f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) ) holds

b_{1} = b_{2}

end;
func - g -> set means :Def14: :: CGAMES_1:def 14

ex f being Function st

( dom f = the_Tree_of g & it = f . g & ( for g1 being ConwayGame st g1 in dom f holds

f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) );

existence ex f being Function st

( dom f = the_Tree_of g & it = f . g & ( for g1 being ConwayGame st g1 in dom f holds

f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) );

ex b

( dom f = the_Tree_of g & b

f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) )

proof end;

uniqueness for b

( dom f = the_Tree_of g & b

f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) ) & ex f being Function st

( dom f = the_Tree_of g & b

f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) ) holds

b

proof end;

:: deftheorem Def14 defines - CGAMES_1:def 14 :

for g being ConwayGame

for b_{2} being set holds

( b_{2} = - g iff ex f being Function st

( dom f = the_Tree_of g & b_{2} = f . g & ( for g1 being ConwayGame st g1 in dom f holds

f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) ) );

for g being ConwayGame

for b

( b

( dom f = the_Tree_of g & b

f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) ) );

registration
end;

Lm4: for g being ConwayGame

for f being Function st dom f = the_Tree_of g & ( for g1 being ConwayGame st g1 in dom f holds

f . g1 = left-right(# { (f . gR) where gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} } , { (f . gL) where gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } #) ) holds

for g1 being ConwayGame st g1 in dom f holds

f . g1 = - g1

proof end;

theorem Th39: :: CGAMES_1:39

for g being ConwayGame holds

( ( for x being set holds

( x in the_LeftOptions_of (- g) iff ex gR being ConwayGame st

( gR in the_RightOptions_of g & x = - gR ) ) ) & ( for x being set holds

( x in the_RightOptions_of (- g) iff ex gL being ConwayGame st

( gL in the_LeftOptions_of g & x = - gL ) ) ) )

( ( for x being set holds

( x in the_LeftOptions_of (- g) iff ex gR being ConwayGame st

( gR in the_RightOptions_of g & x = - gR ) ) ) & ( for x being set holds

( x in the_RightOptions_of (- g) iff ex gL being ConwayGame st

( gL in the_LeftOptions_of g & x = - gL ) ) ) )

proof end;

theorem :: CGAMES_1:41

for g, gO being ConwayGame holds

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

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

proof end;

definition

let g be ConwayGame;

end;
attr g is nonnegative means :: CGAMES_1:def 15

ex s being set st

( g in s & ( for g1 being ConwayGame st g1 in s holds

for gR being ConwayGame st gR in the_RightOptions_of g1 holds

ex gRL being ConwayGame st

( gRL in the_LeftOptions_of gR & gRL in s ) ) );

ex s being set st

( g in s & ( for g1 being ConwayGame st g1 in s holds

for gR being ConwayGame st gR in the_RightOptions_of g1 holds

ex gRL being ConwayGame st

( gRL in the_LeftOptions_of gR & gRL in s ) ) );

:: deftheorem defines nonnegative CGAMES_1:def 15 :

for g being ConwayGame holds

( g is nonnegative iff ex s being set st

( g in s & ( for g1 being ConwayGame st g1 in s holds

for gR being ConwayGame st gR in the_RightOptions_of g1 holds

ex gRL being ConwayGame st

( gRL in the_LeftOptions_of gR & gRL in s ) ) ) );

for g being ConwayGame holds

( g is nonnegative iff ex s being set st

( g in s & ( for g1 being ConwayGame st g1 in s holds

for gR being ConwayGame st gR in the_RightOptions_of g1 holds

ex gRL being ConwayGame st

( gRL in the_LeftOptions_of gR & gRL in s ) ) ) );

definition
end;

:: deftheorem Def16 defines nonpositive CGAMES_1:def 16 :

for g being ConwayGame holds

( g is nonpositive iff - g is nonnegative );

for g being ConwayGame holds

( g is nonpositive iff - g is nonnegative );

:: deftheorem defines zero CGAMES_1:def 17 :

for g being ConwayGame holds

( g is zero iff ( g is nonnegative & g is nonpositive ) );

for g being ConwayGame holds

( g is zero iff ( g is nonnegative & g is nonpositive ) );

:: deftheorem defines fuzzy CGAMES_1:def 18 :

for g being ConwayGame holds

( g is fuzzy iff ( not g is nonnegative & not g is nonpositive ) );

for g being ConwayGame holds

( g is fuzzy iff ( not g is nonnegative & not g is nonpositive ) );

:: deftheorem defines positive CGAMES_1:def 19 :

for g being ConwayGame holds

( g is positive iff ( g is nonnegative & not g is zero ) );

for g being ConwayGame holds

( g is positive iff ( g is nonnegative & not g is zero ) );

:: deftheorem defines negative CGAMES_1:def 20 :

for g being ConwayGame holds

( g is negative iff ( g is nonpositive & not g is zero ) );

for g being ConwayGame holds

( g is negative iff ( g is nonpositive & not g is zero ) );

registration

coherence

for b_{1} being ConwayGame st b_{1} is zero holds

( b_{1} is nonnegative & b_{1} is nonpositive )
;

coherence

for b_{1} being ConwayGame st b_{1} is nonpositive & b_{1} is nonnegative holds

b_{1} is zero
;

coherence

for b_{1} being ConwayGame st b_{1} is negative holds

( b_{1} is nonpositive & not b_{1} is zero )
;

coherence

for b_{1} being ConwayGame st b_{1} is nonpositive & not b_{1} is zero holds

b_{1} is negative
;

coherence

for b_{1} being ConwayGame st b_{1} is positive holds

( b_{1} is nonnegative & not b_{1} is zero )
;

coherence

for b_{1} being ConwayGame st b_{1} is nonnegative & not b_{1} is zero holds

b_{1} is positive
;

coherence

for b_{1} being ConwayGame st b_{1} is fuzzy holds

( not b_{1} is nonnegative & not b_{1} is nonpositive )
;

coherence

for b_{1} being ConwayGame st not b_{1} is nonnegative & not b_{1} is nonpositive holds

b_{1} is fuzzy
;

end;
for b

( b

coherence

for b

b

coherence

for b

( b

coherence

for b

b

coherence

for b

( b

coherence

for b

b

coherence

for b

( not b

coherence

for b

b

theorem :: CGAMES_1:42

theorem Th43: :: CGAMES_1:43

for g being ConwayGame holds

( g is nonnegative iff for gR being ConwayGame st gR in the_RightOptions_of g holds

ex gRL being ConwayGame st

( gRL in the_LeftOptions_of gR & gRL is nonnegative ) )

( g is nonnegative iff for gR being ConwayGame st gR in the_RightOptions_of g holds

ex gRL being ConwayGame st

( gRL in the_LeftOptions_of gR & gRL is nonnegative ) )

proof end;

theorem Th44: :: CGAMES_1:44

for g being ConwayGame holds

( g is nonpositive iff for gL being ConwayGame st gL in the_LeftOptions_of g holds

ex gLR being ConwayGame st

( gLR in the_RightOptions_of gL & gLR is nonpositive ) )

( g is nonpositive iff for gL being ConwayGame st gL in the_LeftOptions_of g holds

ex gLR being ConwayGame st

( gLR in the_RightOptions_of gL & gLR is nonpositive ) )

proof end;

theorem Th45: :: CGAMES_1:45

for g being ConwayGame holds

( ( g is nonnegative implies for gR being ConwayGame holds

( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) & ( ( for gR being ConwayGame holds

( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) implies g is nonnegative ) & ( g is nonpositive implies for gL being ConwayGame holds

( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ( ( for gL being ConwayGame holds

( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) implies g is nonpositive ) )

( ( g is nonnegative implies for gR being ConwayGame holds

( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) & ( ( for gR being ConwayGame holds

( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) implies g is nonnegative ) & ( g is nonpositive implies for gL being ConwayGame holds

( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ( ( for gL being ConwayGame holds

( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) implies g is nonpositive ) )

proof end;

theorem Th46: :: CGAMES_1:46

for g being ConwayGame holds

( g is fuzzy iff ( ex gL being ConwayGame st

( gL in the_LeftOptions_of g & gL is nonnegative ) & ex gR being ConwayGame st

( gR in the_RightOptions_of g & gR is nonpositive ) ) )

( g is fuzzy iff ( ex gL being ConwayGame st

( gL in the_LeftOptions_of g & gL is nonnegative ) & ex gR being ConwayGame st

( gR in the_RightOptions_of g & gR is nonpositive ) ) )

proof end;

theorem Th47: :: CGAMES_1:47

for g being ConwayGame holds

( g is zero iff ( ( for gL being ConwayGame holds

( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ( for gR being ConwayGame holds

( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) ) ) by Th45;

( g is zero iff ( ( for gL being ConwayGame holds

( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ( for gR being ConwayGame holds

( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) ) ) by Th45;

theorem Th48: :: CGAMES_1:48

for g being ConwayGame holds

( g is positive iff ( ( for gR being ConwayGame holds

( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) & ex gL being ConwayGame st

( gL in the_LeftOptions_of g & gL is nonnegative ) ) )

( g is positive iff ( ( for gR being ConwayGame holds

( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) & ex gL being ConwayGame st

( gL in the_LeftOptions_of g & gL is nonnegative ) ) )

proof end;

theorem :: CGAMES_1:49

for g being ConwayGame holds

( g is negative iff ( ( for gL being ConwayGame holds

( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ex gR being ConwayGame st

( gR in the_RightOptions_of g & gR is nonpositive ) ) )

( g is negative iff ( ( for gL being ConwayGame holds

( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ex gR being ConwayGame st

( gR in the_RightOptions_of g & gR is nonpositive ) ) )

proof end;

registration
end;

registration

existence

ex b_{1} being ConwayGame st b_{1} is zero

ex b_{1} being ConwayGame st b_{1} is positive

ex b_{1} being ConwayGame st b_{1} is fuzzy

end;
ex b

proof end;

existence ex b

proof end;

existence ex b

proof end;

registration
end;

registration
end;

registration
end;

registration
end;