Nuprl Definition : win2strat
A strategy that allows player two to respond to n plays by player one.
Anything is such a strategy for n=0.
For 0 < n, the strategy must also work for n-1, and for any play of the
game of length 2*n that has followed that strategy, the strategy
gives a legal move for player two that extends that play.⋅
win2strat(g;n) ==
if (n =z 0)
then Top
else s:win2strat(g;n - 1) ⋂ moves:{f:strat2play(g;n - 1;s)| ||f|| = (2 * n) ∈ ℤ} ⟶ {p:Pos(g)| Legal2(moves[(2 * n) -\000C 1];p)}
fi
Definitions occuring in Statement :
play-len: ||moves||,
play-item: moves[i],
sg-legal2: Legal2(x;y),
sg-pos: Pos(g),
dep-isect: x:A ⋂ B[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
top: Top,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
multiply: n * m,
subtract: n - m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
top: Top,
dep-isect: x:A ⋂ B[x],
function: x:A ⟶ B[x],
equal: s = t ∈ T,
int: ℤ,
play-len: ||moves||,
set: {x:A| B[x]} ,
sg-pos: Pos(g),
sg-legal2: Legal2(x;y),
play-item: moves[i],
subtract: n - m,
multiply: n * m,
natural_number: $n
FDL editor aliases :
win2strat
Latex:
win2strat(g;n) ==
if (n =\msubz{} 0)
then Top
else s:win2strat(g;n - 1) \mcap{} moves:\{f:strat2play(g;n - 1;s)| ||f|| = (2 * n)\} {}\mrightarrow{} \{p:Pos(g)| Legal2\000C(moves[(2 * n) - 1];p)\}
fi
Date html generated:
2018_07_25-PM-01_31_33
Last ObjectModification:
2018_07_11-PM-11_01_38
Theory : co-recursion
Home
Index