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