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