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: 2016_05_17-PM-00_42_20 Last ObjectModification: 2013_10_02-PM-01_01_45 Theory : event-logic-applications Home Index