---

Legal(bss) ==
  ActionsDisjoint
   (A:Id. es:EO+(Info). thr:Thread.
        ((thr is one of bss at A)  Legal(thr)@A))

---

Definitions :  ses-disjoint: ActionsDisjoint,  Id: Id,  event-ordering+: EO+(Info),  ses-info: Info,  all: x:A. B[x],  ses-thread: Thread,  implies: P  Q,  ses-protocol1-thread: (thr is one of bss at A),  ses-legal-thread: Legal(thr)@A
FDL editor aliases :  ses-protocol1-legal

---

Legal(bss)  ==
    ActionsDisjoint
    {}\mRightarrow{}  (\mforall{}A:Id.  \mforall{}es:EO+(Info).  \mforall{}thr:Thread.    ((thr  is  one  of  bss  at  A)  {}\mRightarrow{}  Legal(thr)@A))


Date html generated: 2010_08_28-AM-03_14_33
Last ObjectModification: 2010_02_23-PM-02_39_18

Home Index