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