:: Conway's Games and Some of Their Basic Properties
:: by Robin Nittka
::
:: Received October 13, 2010
:: Copyright (c) 2010-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies CGAMES_1, RELAT_1, TARSKI, XBOOLE_0, ORDINAL1, FUNCT_1, CARD_1,
SUBSET_1, XXREAL_0, ORDINAL2, SUPINF_2, ARYTM_1, PARTFUN1, MSUALG_6,
FINSEQ_1, ARYTM_3, NAT_1, ORDINAL4, MESFUNC5, XCMPLX_0;
notations TARSKI, XBOOLE_0, XXREAL_0, RELAT_1, ORDINAL1, FUNCT_1, CARD_1,
PARTFUN1, ORDINAL2, SUBSET_1, COMPUT_1, FINSEQ_1, XCMPLX_0;
constructors ORDINAL2, COMPUT_1, RELSET_1;
registrations XBOOLE_0, XREAL_0, XXREAL_0, ORDINAL1, FUNCT_1, CARD_1,
SUBSET_1, RELAT_1, COMPUT_1, FINSEQ_1, NAT_1;
requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
begin :: Construction of days
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(# LeftOptions,RightOptions -> set #);
end;
definition
func ConwayZero -> set equals
:: CGAMES_1:def 1
left-right(#{},{}#);
end;
registration
cluster strict for left-right;
end;
definition
let alpha;
func ConwayDay(alpha) -> set means
:: CGAMES_1:def 2
ex f being 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 is Subset of union(rng (f|beta)) ;
end;
theorem :: CGAMES_1:1
for z being object holds
z in ConwayDay(alpha) iff ex w being strict left-right st z = w &
for x st x in (the LeftOptions of w) \/ (the RightOptions of w)
ex beta st beta in alpha & x in ConwayDay(beta);
theorem :: CGAMES_1:2
ConwayDay(0) = { ConwayZero };
theorem :: CGAMES_1:3
alpha c= beta implies ConwayDay(alpha) c= ConwayDay(beta);
registration
let alpha;
cluster ConwayDay(alpha) -> non empty;
end;
begin :: Games
definition
let x;
attr x is ConwayGame-like means
:: CGAMES_1:def 3
ex alpha st x in ConwayDay(alpha);
end;
registration
let alpha;
cluster -> ConwayGame-like for Element of ConwayDay(alpha);
end;
registration
cluster ConwayZero -> ConwayGame-like;
end;
registration
cluster ConwayGame-like strict for left-right;
cluster ConwayGame-like for set;
end;
definition
mode ConwayGame is ConwayGame-like set;
end;
definition
redefine func ConwayZero -> Element of ConwayDay(0);
end;
definition
func ConwayOne -> Element of ConwayDay(1) equals
:: CGAMES_1:def 4
left-right(#{ConwayZero},{}#);
func ConwayStar -> Element of ConwayDay(1) equals
:: CGAMES_1:def 5
left-right(#{ConwayZero},{ConwayZero}#);
end;
reserve g,g0,g1,g2,gO,gL,gR,gLL,gLR,gRL,gRR for ConwayGame;
theorem :: CGAMES_1:4
g is strict left-right;
registration
cluster ConwayGame-like -> strict for left-right;
end;
definition
let g;
func the_LeftOptions_of g -> set means
:: CGAMES_1:def 6
ex w being left-right st g = w & it = the LeftOptions of w;
func the_RightOptions_of g -> set means
:: CGAMES_1:def 7
ex w being left-right st g = w & it = the RightOptions of w;
end;
definition
let g;
func the_Options_of g -> set equals
:: CGAMES_1:def 8
(the_LeftOptions_of g) \/ (the_RightOptions_of g);
end;
theorem :: CGAMES_1:5
g1 = g2 iff
(the_LeftOptions_of g1 = the_LeftOptions_of g2
& the_RightOptions_of g1 = the_RightOptions_of g2);
registration
cluster the_LeftOptions_of ConwayZero -> empty;
cluster the_RightOptions_of ConwayZero -> empty;
cluster the_RightOptions_of ConwayOne -> empty;
end;
theorem :: CGAMES_1:6
g = ConwayZero iff the_Options_of g = {};
theorem :: CGAMES_1:7
x in the_LeftOptions_of ConwayOne iff x = ConwayZero;
theorem :: CGAMES_1:8
(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);
theorem :: CGAMES_1:9
g in ConwayDay(alpha) iff
for x st x in the_Options_of g
ex beta st beta in alpha & x in ConwayDay(beta);
definition
let g be set;
assume
g is ConwayGame;
func ConwayRank(g) -> Ordinal means
:: CGAMES_1:def 9
g in ConwayDay(it) & for beta st beta in it holds not g in ConwayDay(beta);
end;
theorem :: CGAMES_1:10
g in ConwayDay(alpha) & x in the_Options_of g implies x in ConwayDay(alpha);
theorem :: CGAMES_1:11
g in ConwayDay(alpha) &
(x in the_LeftOptions_of g or x in the_RightOptions_of g)
implies x in ConwayDay(alpha);
theorem :: CGAMES_1:12
g in ConwayDay(alpha) iff ConwayRank(g) c= alpha;
theorem :: CGAMES_1:13
ConwayRank(g) in alpha iff ex beta st beta in alpha & g in ConwayDay(beta);
theorem :: CGAMES_1:14
gO in the_Options_of g implies ConwayRank(gO) in ConwayRank(g);
theorem :: CGAMES_1:15
(gO in the_LeftOptions_of g or gO in the_RightOptions_of g)
implies ConwayRank(gO) in ConwayRank(g);
theorem :: CGAMES_1:16
not g in the_Options_of g;
theorem :: CGAMES_1:17
x in the_Options_of g implies x is ConwayGame-like left-right;
theorem :: CGAMES_1:18
(x in the_LeftOptions_of g or x in the_RightOptions_of g)
implies x is ConwayGame-like left-right;
theorem :: CGAMES_1:19
for w being 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;
begin :: Schemes of induction
scheme :: CGAMES_1:sch 1
ConwayGameMinTot { P[ConwayGame] } :
ex g st P[g] & for g1 st ConwayRank(g1) in ConwayRank(g) holds not P[g1]
provided
ex g st P[g];
scheme :: CGAMES_1:sch 2
ConwayGameMin { P[ConwayGame] } :
ex g st P[g] & for gO st gO in the_Options_of g holds not P[gO]
provided
ex g st P[g];
scheme :: CGAMES_1:sch 3
ConwayGameInd { P[ConwayGame] } : for g holds P[g]
provided
for g st (for gO st gO in the_Options_of g holds P[gO]) holds P[g];
begin :: Tree of a game
definition
let f be Function;
attr f is ConwayGame-valued means
:: CGAMES_1:def 10
for x st x in dom f holds f.x is ConwayGame;
end;
registration
let g;
cluster <*g*> -> ConwayGame-valued;
end;
registration
cluster ConwayGame-valued non empty for FinSequence;
end;
registration
let f be non empty FinSequence;
cluster -> natural non empty for Element of dom f;
end;
registration
let f be ConwayGame-valued non empty Function;
let x be Element of dom f;
cluster f.x -> ConwayGame-like;
end;
definition
let f be ConwayGame-valued non empty FinSequence;
attr f is ConwayGameChain-like means
:: CGAMES_1:def 11
for n being Element of dom f st n > 1 holds
f.(n-1) in the_Options_of f.n;
end;
theorem :: CGAMES_1:20
for f being FinSequence for n st n in dom f & n > 1
holds n-1 in dom f;
registration
let g;
cluster <*g*> -> ConwayGameChain-like;
end;
registration
cluster ConwayGameChain-like for ConwayGame-valued non empty FinSequence;
end;
definition
mode ConwayGameChain is
ConwayGameChain-like ConwayGame-valued non empty FinSequence;
end;
theorem :: 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);
theorem :: 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);
theorem :: CGAMES_1:23
for f being ConwayGameChain st f.(len f) in ConwayDay(alpha)
holds f.1 in ConwayDay(alpha);
definition
let g;
func the_Tree_of g -> set means
:: CGAMES_1:def 12
z in it iff ex f being ConwayGameChain st f.1 = z & f.(len f) = g;
end;
registration
let g;
cluster the_Tree_of g -> non empty;
end;
definition
let g;
func the_proper_Tree_of g -> Subset of the_Tree_of g equals
:: CGAMES_1:def 13
the_Tree_of g \ {g};
end;
theorem :: CGAMES_1:24
g in the_Tree_of g;
definition
let alpha;
let g be Element of ConwayDay(alpha);
redefine func the_Tree_of g -> Subset of ConwayDay(alpha);
end;
registration
let g;
cluster -> ConwayGame-like for Element of the_Tree_of g;
end;
theorem :: CGAMES_1:25
for f being ConwayGameChain for n being non zero Nat holds
f|n is ConwayGameChain;
theorem :: CGAMES_1:26
for f1,f2 being ConwayGameChain st
ex g st g = f2.1 & f1.(len f1) in the_Options_of g
holds f1^f2 is ConwayGameChain;
theorem :: CGAMES_1:27
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);
theorem :: CGAMES_1:28
gO in the_Tree_of g implies (gO = g or ConwayRank(gO) in ConwayRank(g));
theorem :: CGAMES_1:29
gO in the_Tree_of g implies ConwayRank(gO) c= ConwayRank(g);
theorem :: CGAMES_1:30
for s being 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;
theorem :: CGAMES_1:31
g1 in the_Tree_of g2 implies the_Tree_of g1 c= the_Tree_of g2;
theorem :: CGAMES_1:32
g1 in the_Tree_of g2 implies the_proper_Tree_of g1 c= the_proper_Tree_of g2;
theorem :: CGAMES_1:33
the_Options_of g c= the_proper_Tree_of g;
theorem :: CGAMES_1:34
the_Options_of g c= the_Tree_of g;
theorem :: CGAMES_1:35
g1 in the_proper_Tree_of g2 implies the_Tree_of g1 c= the_proper_Tree_of g2;
theorem :: CGAMES_1:36
gO in the_Options_of g implies the_Tree_of gO c= the_proper_Tree_of g;
theorem :: CGAMES_1:37
the_Tree_of ConwayZero = { ConwayZero };
theorem :: CGAMES_1:38
ConwayZero in the_Tree_of g;
scheme :: CGAMES_1:sch 4
ConwayGameMin2 { P[ConwayGame] } :
ex g st P[g] & for gO st gO in the_proper_Tree_of g holds not P[gO]
provided
ex g st P[g];
begin :: Scheme about definability of functions by recursion
scheme :: CGAMES_1:sch 5
Func1RecUniq { F(ConwayGame,Function) -> set } :
for g for f1,f2 being 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,f1|the_proper_Tree_of g1))
& (for g1 st g1 in dom f2 holds f2.g1 = F(g1,f2|the_proper_Tree_of g1))
holds f1 = f2;
scheme :: CGAMES_1:sch 6
Func1RecEx { F(ConwayGame,Function) -> set } :
ex f being Function st dom f = the_Tree_of g &
for g1 st g1 in dom f holds f.g1 = F(g1,f|the_proper_Tree_of g1);
begin
definition
let g;
func -g -> set means
:: CGAMES_1:def 14
ex f being 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 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 <> {} } #);
end;
registration
let g;
cluster -g -> ConwayGame-like;
end;
theorem :: CGAMES_1:39
(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);
theorem :: CGAMES_1:40
-(-g) = g;
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);
definition
let g;
attr g is nonnegative means
:: CGAMES_1:def 15
ex s st g in s & for g1 st g1 in s for gR st gR in the_RightOptions_of g1
ex gRL st gRL in the_LeftOptions_of gR & gRL in s;
end;
definition
let g;
attr g is nonpositive means
:: CGAMES_1:def 16
-g is nonnegative;
end;
definition
let g;
attr g is zero means
:: CGAMES_1:def 17
g is nonnegative & g is nonpositive;
attr g is fuzzy means
:: CGAMES_1:def 18
not g is nonnegative & not g is nonpositive;
end;
definition
let g;
attr g is positive means
:: CGAMES_1:def 19
g is nonnegative & not g is zero;
attr g is negative means
:: CGAMES_1:def 20
g is nonpositive & not g is zero;
end;
registration
cluster zero -> nonnegative nonpositive for ConwayGame;
cluster nonpositive nonnegative -> zero for ConwayGame;
cluster negative -> nonpositive non zero for ConwayGame;
cluster nonpositive non zero -> negative for ConwayGame;
cluster positive -> nonnegative non zero for ConwayGame;
cluster nonnegative non zero -> positive for ConwayGame;
cluster fuzzy -> non nonnegative non nonpositive for ConwayGame;
cluster non nonnegative non nonpositive -> fuzzy for ConwayGame;
end;
theorem :: CGAMES_1:42
g is zero or g is positive or g is negative or g is fuzzy;
theorem :: CGAMES_1:43
g is nonnegative iff
for gR st gR in the_RightOptions_of g
ex gRL st gRL in the_LeftOptions_of gR & gRL is nonnegative;
theorem :: CGAMES_1:44
g is nonpositive iff
for gL st gL in the_LeftOptions_of g
ex gLR st gLR in the_RightOptions_of gL & gLR is nonpositive;
theorem :: CGAMES_1:45
(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);
theorem :: CGAMES_1:46
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);
theorem :: CGAMES_1:47
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);
theorem :: CGAMES_1:48
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);
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);
registration
cluster ConwayZero -> zero;
end;
registration
cluster ConwayOne -> positive;
cluster ConwayStar -> fuzzy;
end;
registration
cluster zero for ConwayGame;
cluster positive for ConwayGame;
cluster fuzzy for ConwayGame;
end;
registration
let g be nonpositive ConwayGame;
cluster -g -> nonnegative;
end;
registration
let g be nonnegative ConwayGame;
cluster -g -> nonpositive;
end;
registration
let g be positive ConwayGame;
cluster -g -> negative;
end;
registration
cluster negative for ConwayGame;
end;
registration
let g be negative ConwayGame;
cluster -g -> positive;
end;
registration
let g be fuzzy ConwayGame;
cluster -g -> fuzzy;
end;