(thr is one of bss at A) == 
B:Id. (bs
bss. thr[A;B] |= bs)
Definitions :
exists: x:A. B[x],
Id: Id,
l_exists: (xL. P[x]),
ses-basic-sequence1: Basic1,
is-basic-seq: thr[A;B] |= bs
FDL editor aliases :
ses-protocol1-thread
(thr is one of bss at A) == \mexists{}B:Id. (\mexists{}bs\mmember{}bss. thr[A;B] |= bs)
Date html generated:
2010_08_28-AM-03_14_19
Last ObjectModification:
2010_02_23-AM-10_59_59
Home
Index