Nuprl Definition : WfdSpread

WfdSpread(Pos;a.Mv[a]) ==  {g:Spread(Pos;a.Mv[a])| ∀p:ℕ ⟶ MoveChoice(Pos;a.Mv[a]). (↓∃n:ℕresigned(subgame(g;p;n)))} 



Definitions occuring in Statement :  resigned: resigned(x) subgame: subgame(g;p;n) MoveChoice: MoveChoice(Pos;a.Mv[a]) Spread: Spread(Pos;a.Mv[a]) nat: all: x:A. B[x] exists: x:A. B[x] squash: T set: {x:A| B[x]}  function: x:A ⟶ B[x]
Definitions occuring in definition :  set: {x:A| B[x]}  Spread: Spread(Pos;a.Mv[a]) all: x:A. B[x] function: x:A ⟶ B[x] MoveChoice: MoveChoice(Pos;a.Mv[a]) squash: T exists: x:A. B[x] nat: resigned: resigned(x) subgame: subgame(g;p;n)
FDL editor aliases :  WfdSpread

Latex:
WfdSpread(Pos;a.Mv[a])  ==
    \{g:Spread(Pos;a.Mv[a])|  \mforall{}p:\mBbbN{}  {}\mrightarrow{}  MoveChoice(Pos;a.Mv[a]).  (\mdownarrow{}\mexists{}n:\mBbbN{}.  resigned(subgame(g;p;n)))\} 



Date html generated: 2016_05_14-PM-03_56_45
Last ObjectModification: 2015_09_22-PM-06_01_54

Theory : spread


Home Index