Nuprl Definition : eq-Game
G ≡ H ==
((∀i:left-indices(G). ∃j:left-indices(H). left-move(G;i) ≡ left-move(H;j))
∧ (∀i:right-indices(G). ∃j:right-indices(H). right-move(G;i) ≡ right-move(H;j)))
∧ (∀i:left-indices(H). ∃j:left-indices(G). left-move(H;i) ≡ left-move(G;j))
∧ (∀i:right-indices(H). ∃j:right-indices(G). right-move(H;i) ≡ right-move(G;j))
Definitions occuring in Statement :
right-move: right-move(g;x),
left-move: left-move(g;x),
right-indices: right-indices(g),
left-indices: left-indices(g),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q
Definitions occuring in definition :
and: P ∧ Q,
left-indices: left-indices(g),
left-move: left-move(g;x),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
right-indices: right-indices(g),
right-move: right-move(g;x)
FDL editor aliases :
eq-Game
Latex:
G \mequiv{} H ==
((\mforall{}i:left-indices(G). \mexists{}j:left-indices(H). left-move(G;i) \mequiv{} left-move(H;j))
\mwedge{} (\mforall{}i:right-indices(G). \mexists{}j:right-indices(H). right-move(G;i) \mequiv{} right-move(H;j)))
\mwedge{} (\mforall{}i:left-indices(H). \mexists{}j:left-indices(G). left-move(H;i) \mequiv{} left-move(G;j))
\mwedge{} (\mforall{}i:right-indices(H). \mexists{}j:right-indices(G). right-move(H;i) \mequiv{} right-move(G;j))
Date html generated:
2018_05_22-PM-09_53_13
Last ObjectModification:
2018_02_15-AM-10_17_25
Theory : Numbers!and!Games
Home
Index