Nuprl Definition : Game-add
G ⊕ H ==
{mkGame(case x
of inl(a) =>
left-move(G;a) ⊕ H
| inr(b) =>
G ⊕ left-move(H;b) with x:left-indices(G) + left-indices(H) | case y
of inl(a) =>
right-move(G;a) ⊕ H
| inr(b) =>
G ⊕ right-move(H;b) with y:right-indices(G) + right-indices(H)}
Definitions occuring in Statement :
mkGame: {mkGame(f[a] with a:L | g[b] with b:R},
right-move: right-move(g;x),
left-move: left-move(g;x),
right-indices: right-indices(g),
left-indices: left-indices(g),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
union: left + right
Definitions occuring in definition :
mkGame: {mkGame(f[a] with a:L | g[b] with b:R},
left-indices: left-indices(g),
union: left + right,
right-indices: right-indices(g),
left-move: left-move(g;x),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
right-move: right-move(g;x)
FDL editor aliases :
Game-add
Latex:
G \moplus{} H ==
\{mkGame(case x
of inl(a) =>
left-move(G;a) \moplus{} H
| inr(b) =>
G \moplus{} left-move(H;b) with x:left-indices(G) + left-indices(H) | case y
of inl(a) =>
right-move(G;a) \moplus{} H
| inr(b) =>
G \moplus{} right-move(H;b) with y:right-indices(G) + right-indices(H)\}
Date html generated:
2018_05_22-PM-09_52_59
Last ObjectModification:
2018_02_14-PM-10_58_39
Theory : Numbers!and!Games
Home
Index