Nuprl Definition : sub-spread
s' ≤ s == ∃n:ℕ. ∃p:ℕn ⟶ MoveChoice(Pos;a.Mv[a]). (subgame(s;p;n) = (inl s') ∈ (Spread(Pos;a.Mv[a])?))
Definitions occuring in Statement :
subgame: subgame(g;p;n)
,
MoveChoice: MoveChoice(Pos;a.Mv[a])
,
Spread: Spread(Pos;a.Mv[a])
,
int_seg: {i..j-}
,
nat: ℕ
,
exists: ∃x:A. B[x]
,
unit: Unit
,
function: x:A ⟶ B[x]
,
inl: inl x
,
union: left + right
,
natural_number: $n
,
equal: s = t ∈ T
Definitions occuring in definition :
nat: ℕ
,
exists: ∃x:A. B[x]
,
function: x:A ⟶ B[x]
,
int_seg: {i..j-}
,
natural_number: $n
,
MoveChoice: MoveChoice(Pos;a.Mv[a])
,
equal: s = t ∈ T
,
union: left + right
,
Spread: Spread(Pos;a.Mv[a])
,
unit: Unit
,
subgame: subgame(g;p;n)
,
inl: inl x
FDL editor aliases :
sub-spread
Latex:
s' \mleq{} s == \mexists{}n:\mBbbN{}. \mexists{}p:\mBbbN{}n {}\mrightarrow{} MoveChoice(Pos;a.Mv[a]). (subgame(s;p;n) = (inl s'))
Date html generated:
2016_05_14-PM-03_56_27
Last ObjectModification:
2015_09_22-PM-06_01_53
Theory : spread
Home
Index