Nuprl Definition : ses-protocol1-thread
(thr is one of bss at A) == ∃B:Id. (∃bs∈bss. thr[A;B] |= bs)
Definitions occuring in Statement :
is-basic-seq: thr[A;B] |= bs,
Id: Id,
l_exists: (∃x∈L. P[x]),
exists: ∃x:A. B[x]
FDL editor aliases :
ses-protocol1-thread
Latex:
(thr is one of bss at A) == \mexists{}B:Id. (\mexists{}bs\mmember{}bss. thr[A;B] |= bs)
Date html generated:
2015_07_23-PM-00_16_37
Last ObjectModification:
2013_10_02-PM-01_01_45
Home
Index