:: Conway's Games and Some of Their Basic Properties
:: by Robin Nittka
::
:: Received October 13, 2010
:: Copyright (c) 2010-2026 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;
definitions FUNCT_1, TARSKI, PARTFUN1;
equalities FINSEQ_1, ORDINAL1;
expansions FUNCT_1, TARSKI, ORDINAL1;
theorems TARSKI, ORDINAL1, FUNCT_1, ZFMISC_1, RELAT_1, XBOOLE_0, ORDINAL2,
XBOOLE_1, PARTFUN1, COMPUT_1, NAT_1, FINSEQ_1, XXREAL_0, XREAL_1,
FINSEQ_2, FINSEQ_3, FINSEQ_5, GRFUNC_1, XTUPLE_0;
schemes ORDINAL1, NAT_1, TARSKI;
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 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 is Subset of union(rng $1) ;
defpred ConwayIteration[Sequence] means
for beta st beta in dom $1 holds $1.beta = ConwayNextDay($1|beta);
Lm1:
for f being 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(f|beta) by A1,A2;
dom (f|alpha) c= alpha by RELAT_1:58;
then beta c= alpha by A2,ORDINAL1:def 2;
then (f|alpha)|beta = f|beta by FUNCT_1:51;
hence thesis by A3,A2,FUNCT_1:47;
end;
definition
let alpha;
func ConwayDay(alpha) -> set means
:Def2:
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)) ;
existence
proof
consider f being Sequence such that
A1: dom f = succ alpha
& for beta for f1 being 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 being Sequence st alpha in dom f1 & f1.alpha = x
& ConwayIteration[f1];
then consider f1 being Sequence such that
A2: alpha in dom f1 & f1.alpha = x & ConwayIteration[f1];
set f1r = f1|succ alpha;
assume ex f2 being Sequence st alpha in dom f2 & f2.alpha = y
& ConwayIteration[f2];
then consider f2 being 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 for f being 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 for f being 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 Th1:
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)
proof let z be object;
consider f being 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(f|alpha) by A1;
then consider x,y being Subset of union(rng (f|alpha)) such that
A2: z = left-right(#x,y#);
reconsider w = z as strict left-right by A2;
take w;
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 being set such that
A3: e in r & r in rng (f|alpha) by TARSKI:def 4;
ex beta being 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 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);
then consider w being strict left-right such that
A5: w = z & for x st x in (the LeftOptions of w) \/ (the RightOptions of w)
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(f|alpha);
hence z in ConwayDay(alpha) by A1,A5;
end;
end;
theorem Th2:
ConwayDay(0) = { ConwayZero }
proof
A1:
ConwayDay(0) c= { ConwayZero }
proof
let z be object;
assume z in ConwayDay(0);
then consider w being strict left-right such that
A2: z = w & for e st e in (the LeftOptions of w) \/ (the RightOptions of w)
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 being 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 {} \/ {} 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 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 being strict left-right such that
A2: w = z & (for e st e in (the LeftOptions of w) \/ (the RightOptions of w)
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 :: Games
definition
let x;
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
redefine func ConwayZero -> Element of ConwayDay(0); :: redefines ConwayZero (CGAMES_1, definition)
coherence by Th2,TARSKI:def 1;
end;
definition
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)
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;
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)
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 Th4:
g is strict left-right
proof
consider alpha such that
A1: g in ConwayDay(alpha) by Def3;
ex w being strict left-right st w = g &
for x st x in (the LeftOptions of w) \/ (the RightOptions of w)
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;
func the_LeftOptions_of g -> set means
:Def6:
ex w being 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;
func the_RightOptions_of g -> set means
:Def7:
ex w being 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;
func the_Options_of g -> set equals
(the_LeftOptions_of g) \/ (the_RightOptions_of g);
correctness;
end;
theorem 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 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 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 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 Th9:
g in ConwayDay(alpha) iff
for x st x in the_Options_of g
ex beta st beta in alpha & x in ConwayDay(beta)
proof
hereby
assume g in ConwayDay(alpha);
then consider w being strict left-right such that
A1: g = w & for x st x in (the LeftOptions of w) \/ (the RightOptions of w)
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
ex beta st beta in alpha & x in ConwayDay(beta);
ex w being strict left-right st g = w &
for x st x in (the LeftOptions of w) \/ (the RightOptions of w)
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;
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 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 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 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 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 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
(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 Th16:
not g in the_Options_of g
proof
assume not thesis;
then ConwayRank(g) in ConwayRank(g) by Th14;
hence contradiction;
end;
theorem 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 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 Th19:
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
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 is 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 :: Schemes of induction
scheme 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]
proof
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 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]
proof
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 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]
proof
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 :: Tree of a game
definition
let f be Function;
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;
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;
attr f is ConwayGameChain-like means
:Def11:
for n being Element of dom f st n > 1 holds
f.(n-1) in the_Options_of f.n;
end;
theorem Th20:
for f being FinSequence for n st n in dom f & n > 1
holds n-1 in dom f
proof
let f be FinSequence;
consider l being 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,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 Th21:
for f being ConwayGameChain
for n,m being Element of dom f st n < m holds
ConwayRank(f.n) in ConwayRank(f.m)
proof
let f be ConwayGameChain;
let n,m be Element of dom f such that
A1: n < m;
consider l being 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 being 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,43;
then
A7: 1 <= m-k & m-k <= l by XXREAL_0:2;
then m >= k+1 & k <= k+1 by XREAL_1:19,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 being 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 Th22:
for f being ConwayGameChain
for n,m being Element of dom f st n <= m holds
ConwayRank(f.n) c= ConwayRank(f.m)
proof
let f be ConwayGameChain;
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 Th23:
for f being 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 being ConwayGameChain st f.1 = g & f.(len f) = g
proof
take f = <*g*>;
len f = 1 by FINSEQ_1:40;
hence thesis;
end;
definition
let g;
func the_Tree_of g -> set means
:Def12:
z in it iff ex f being 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 is Element of ConwayDay(alpha) :
ex f being ConwayGameChain st f.1 = x & f.(len f) = g };
let z;
hereby
assume z in s;
then consider x being Element of ConwayDay(alpha) such that
A2: x = z & ex f being ConwayGameChain st f.1 = x & f.(len f) = g;
thus ex f being ConwayGameChain st f.1 = z & f.(len f) = g by A2;
end;
assume ex f being ConwayGameChain st f.1 = z & f.(len f) = g;
then consider f being ConwayGameChain such that
A3: f.1 = z & f.(len f) = g;
f.1 in ConwayDay(alpha) by Th23,A1,A3;
hence z in s by A3;
end;
uniqueness
proof
let t1,t2 be set;
assume
A4: z in t1 iff ex f being ConwayGameChain st f.1 = z & f.(len f) = g;
assume
A5: z in t2 iff ex f being ConwayGameChain st f.1 = z & f.(len f) = g;
now
let z be object;
hereby
assume z in t1;
then ex f being 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 being 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 being ConwayGameChain st f.1 = g & f.(len f) = g by Lm2;
hence thesis by Def12;
end;
end;
definition
let g;
func the_proper_Tree_of g -> Subset of the_Tree_of g equals
the_Tree_of g \ {g};
coherence;
end;
theorem Th24:
g in the_Tree_of g
proof
ex f being 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);
redefine func the_Tree_of g -> Subset of ConwayDay(alpha); :: redefines the_Tree_of (CGAMES_1, definition)
coherence
proof
the_Tree_of(g) c= ConwayDay(alpha)
proof
let z be object;
assume z in the_Tree_of g;
then consider f being ConwayGameChain such that
A1: f.1 = z & f.(len f) = g by Def12;
thus z in ConwayDay(alpha) by A1,Th23;
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 being ConwayGameChain st f.1 = g1 & f.(len f) = g by Def12;
then g1 in ConwayDay(alpha) by Th23,A1;
hence thesis;
end;
end;
theorem Th25:
for f being ConwayGameChain for n being 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 Th26:
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
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 being 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 being 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 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 being ConwayGameChain such that
A1: f.1 = x & f.(len f) = g by Def12;
reconsider n = len f as Element of dom f by FINSEQ_5:6;
assume
A2: x <> g;
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 being 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 by A5,A6;
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,def 7;
hence x in the_Tree_of g by Def12;
end;
end;
end;
theorem 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 being ConwayGameChain such that
A1: f.1 = gO & f.(len f) = g by Def12;
reconsider n = 1 as Element of dom f by FINSEQ_5:6;
reconsider m = len f as Element of dom f by FINSEQ_5:6;
A2:
m >= 1 by NAT_1:14;
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 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
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
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 being 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] 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 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 being 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 being 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 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 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 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 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
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
the_Tree_of ConwayZero = { ConwayZero } by Th2,ZFMISC_1:33;
theorem
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 being 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 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]
proof
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 about definability of functions by recursion
scheme 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
proof
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,f1|the_proper_Tree_of g1))
& (for g1 st g1 in dom f2 holds f2.g1 = F(g1,f2|the_proper_Tree_of g1));
defpred Bad[ConwayGame] means $1 in the_Tree_of g & f1.$1 <> f2.$1;
assume f1 <> f2;
then ex x being object st x in the_Tree_of g & f1.x <> f2.x
by A1;
then
A2: ex g0 st Bad[g0];
consider gm being 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 being 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,f1|the_proper_Tree_of gm)
& f2.gm = F(gm,f2|the_proper_Tree_of gm) by A1,A3;
hence contradiction by A4,A3;
end;
scheme 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)
proof
defpred GoodFun[Function] means
for g st g in dom $1 holds $1.g = F(g,$1|the_proper_Tree_of g);
defpred GoodG[ConwayGame] means
ex f being Function st dom f = the_Tree_of $1 & GoodFun[f];
defpred GF[object,object] means ex g being ConwayGame st $1 = g
& ex f being Function st $2 = f & dom f = the_Tree_of g & GoodFun[f];
A1:
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 from Func1RecUniq;
then
A2: for x,y,z being object st GF[x,y] & GF[x,z] holds y=z;
A3:
for g for f being 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|the_proper_Tree_of g1)
& f.g1 = (f|(the_Tree_of g)).g1 by A4,A5,FUNCT_1:47;
dom (f|(the_Tree_of g)) c= the_Tree_of g by RELAT_1:58;
then the_Tree_of g1 c= the_Tree_of g by Th31,A5;
hence 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 being set such that
A9: for y being object holds y in FUNCS iff
ex x being 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 being 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 being 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 being 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 being 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 being Function such that
A17: [x,f.x] in f1 & f1 in FUNCS;
ex y being 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 being Function such that
A20: [g1,f.g1] in fO & fO in FUNCS;
ex x being 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|the_proper_Tree_of g1)
& fO.g1 = f.g1 by A21,A20,COMPUT_1:13;
hence f.g1 = F(g1,f|the_proper_Tree_of g1) by A22;
end;
g in dom f
proof
assume
A26: not g in dom f;
set v = F(g, f|the_proper_Tree_of 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 :: The negative and signs
Lm3:
for f being Function holds
{ (f|the_proper_Tree_of g1).gR
where gR is Element of the_RightOptions_of g1 :
the_RightOptions_of g1 <> {} }
= { f.gR where gR is Element of the_RightOptions_of g1 :
the_RightOptions_of g1 <> {} }
& { (f|the_proper_Tree_of g1).gL
where gL is Element of the_LeftOptions_of g1 :
the_LeftOptions_of g1 <> {} }
= { f.gL where gL is Element of the_LeftOptions_of g1 :
the_LeftOptions_of g1 <> {} }
proof
let f be Function;
set R1 = { (f|the_proper_Tree_of g1).gR where
gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} };
set R2 = { f.gR where
gR is Element of the_RightOptions_of g1 : the_RightOptions_of g1 <> {} };
set L1 = { (f|the_proper_Tree_of g1).gL where
gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} };
set L2 = { f.gL where
gL is Element of the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} };
A1:
for gO 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 being Element of the_RightOptions_of g1 such that
A2: x = (f|the_proper_Tree_of g1).gR & the_RightOptions_of g1 <> {};
gR in the_RightOptions_of g1 & gR is ConwayGame by A2,Th18;
then (f|the_proper_Tree_of g1).gR = f.gR by A1;
hence x in R2 by A2;
end;
hereby
let x be object;
assume x in R2;
then consider gR being Element of the_RightOptions_of g1 such that
A3: x = f.gR & the_RightOptions_of g1 <> {};
gR in the_RightOptions_of g1 & gR is ConwayGame by A3,Th18;
then (f|the_proper_Tree_of g1).gR = f.gR by A1;
hence x in R1 by A3;
end;
end;
hence R1 = R2 by TARSKI:2;
now
hereby
let x be object;
assume x in L1;
then consider gL being Element of the_LeftOptions_of g1 such that
A4: x = (f|the_proper_Tree_of g1).gL & the_LeftOptions_of g1 <> {};
gL in the_LeftOptions_of g1 & gL is ConwayGame by A4,Th18;
then (f|the_proper_Tree_of g1).gL = f.gL by A1;
hence x in L2 by A4;
end;
hereby
let x be object;
assume x in L2;
then consider gL being Element of the_LeftOptions_of g1 such that
A5: x = f.gL & the_LeftOptions_of g1 <> {};
gL in the_LeftOptions_of g1 & gL is ConwayGame by A5,Th18;
then (f|the_proper_Tree_of g1).gL = f.gL by A1;
hence x in L1 by A5;
end;
end;
hence L1 = L2 by TARSKI:2;
end;
definition
let g;
func -g -> set means
:Def14:
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 <> {} } #);
existence
proof
deffunc F(ConwayGame,Function) = left-right(#
{ $2.gR where gR is Element of the_RightOptions_of $1 :
the_RightOptions_of $1 <> {} },
{ $2.gL where gL is Element of the_LeftOptions_of $1 :
the_LeftOptions_of $1 <> {} } #);
for g 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)
from Func1RecEx;
then consider f being Function such that
A1: dom f = the_Tree_of g & for g1 st g1 in dom f holds
f.g1 = F(g1,f|the_proper_Tree_of 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 is Element of
the_RightOptions_of g1 : the_RightOptions_of g1 <> {} }
= { f.gR where gR is Element of
the_RightOptions_of g1 : the_RightOptions_of g1 <> {} }
& { (f|the_proper_Tree_of g1).gL where gL is Element of
the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} }
= { f.gL where gL is Element of
the_LeftOptions_of g1 : the_LeftOptions_of g1 <> {} } by Lm3;
hence thesis by A1,A2;
end;
uniqueness
proof
deffunc F(ConwayGame,Function) = left-right(#
{ $2.gR where gR is Element of the_RightOptions_of $1 :
the_RightOptions_of $1 <> {} },
{ $2.gL where gL is Element of the_LeftOptions_of $1 :
the_LeftOptions_of $1 <> {} } #);
let g1,g2 be set;
assume ex f1 being 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 being 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 being 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 being 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, f1|the_proper_Tree_of g0)
proof
let g0;
set LOr = { (f1|the_proper_Tree_of g0).gR where gR is
Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} };
set ROr = { (f1|the_proper_Tree_of g0).gL where gL is
Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} };
set LOu = { f1.gR where gR is
Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} };
set ROu = { f1.gL where gL is
Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} };
LOu = LOr & ROu = ROr by Lm3;
hence thesis by A3;
end;
A6: for g0 st g0 in dom f2 holds f2.g0 = F(g0, f2|the_proper_Tree_of g0)
proof
let g0;
set LOr = { (f2|the_proper_Tree_of g0).gR where gR is
Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} };
set ROr = { (f2|the_proper_Tree_of g0).gL where gL is
Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} };
set LOu = { f2.gR where gR is
Element of the_RightOptions_of g0 : the_RightOptions_of g0 <> {} };
set ROu = { f2.gL where gL is
Element of the_LeftOptions_of g0 : the_LeftOptions_of g0 <> {} };
LOu = LOr & ROu = ROr by Lm3;
hence thesis by A4;
end;
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
from Func1RecUniq;
hence thesis by A3,A4,A5,A6;
end;
end;
registration
let g;
cluster -g -> ConwayGame-like;
coherence
proof
consider f being 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 is Element of the_RightOptions_of g1 :
the_RightOptions_of g1 <> {} },
{ f.gL where gL is Element of the_LeftOptions_of g1 :
the_LeftOptions_of g1 <> {} } #) by Def14;
defpred 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 is Element of the_RightOptions_of g1
: the_RightOptions_of g1 <> {} };
set R = { f.gL where gL is Element of the_LeftOptions_of g1
: the_LeftOptions_of g1 <> {} };
A5: f.g1 = left-right(#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 being Element of the_RightOptions_of g1
such that
A7: z = f.gR & the_RightOptions_of g1 <> {};
reconsider gO = gR as ConwayGame by Th18,A7;
take gO;
thus thesis by A7,XBOOLE_0:def 3;
end;
suppose z in R;
then consider gL being Element of the_LeftOptions_of g1
such that
A8: z = f.gL & the_LeftOptions_of g1 <> {};
reconsider gO = gL as ConwayGame by Th18,A8;
take gO;
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 being Function st dom f = the_Tree_of 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 <> {} } #)
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 is Element of the_RightOptions_of g1 :
the_RightOptions_of g1 <> {} },
{ f.gL where gL is Element of the_LeftOptions_of g1 :
the_LeftOptions_of g1 <> {} } #);
let g1 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 is Element of the_RightOptions_of g2 :
the_RightOptions_of g2 <> {} };
set L1 = { f1.gR where gR is Element of the_RightOptions_of g2 :
the_RightOptions_of g2 <> {} };
set R = { f.gL where gL is Element of the_LeftOptions_of g2 :
the_LeftOptions_of g2 <> {} };
set R1 = { f1.gL where gL is 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 being Element of the_RightOptions_of g2 such that
A7: x = f.gR & the_RightOptions_of g2 <> {};
gR in the_RightOptions_of g2 & gR is ConwayGame by A7,Th18;
then 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 being 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 being Element of the_LeftOptions_of g2 such that
A10: x = f.gL & the_LeftOptions_of g2 <> {};
gL in the_LeftOptions_of g2 & gL is ConwayGame by A10,Th18;
then 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 being 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 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 being 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 is Element of the_RightOptions_of g1 :
the_RightOptions_of g1 <> {} },
{ f.gL where gL is Element of the_LeftOptions_of g1 :
the_LeftOptions_of g1 <> {} } #) by Def14;
A2:
(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 is Element of the_RightOptions_of g
: the_RightOptions_of g <> {} };
set R = { f.gL where gL is Element of the_LeftOptions_of g
: the_LeftOptions_of g <> {} };
-g = left-right(#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 being Element of the_RightOptions_of g such that
A4: x = f.gR0 & the_RightOptions_of g <> {} by A3;
reconsider gR = gR0 as ConwayGame by Th18,A4;
take gR;
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 being Element of the_LeftOptions_of g such that
A6: x = f.gL0 & the_LeftOptions_of g <> {} by A3;
reconsider gL = gL0 as ConwayGame by Th18,A6;
take gL;
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 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
(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;
attr g is nonnegative means
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
:Def16:
-g is nonnegative;
end;
definition
let g;
attr g is zero means
g is nonnegative & g is nonpositive;
attr g is fuzzy means
not g is nonnegative & not g is nonpositive;
end;
definition
let g;
attr g is positive means
g is nonnegative & not g is zero;
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
g is zero or g is positive or g is negative or g is fuzzy;
theorem Th43:
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
proof
defpred S[set] means
for g st g in $1 for gR st gR in the_RightOptions_of g
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
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 is Subset of ConwayDay(alpha) : S[s1] };
take s = union ss;
A10: S[s]
proof
let g1;
assume g1 in s;
then consider s2 being set such that
A11: g1 in s2 & s2 in ss by TARSKI:def 4;
consider s1 being 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 being 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 being 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 Th44:
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
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
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 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 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 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 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
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;