Nuprl Definition : ses-protocol1-legal
Legal(bss) == ActionsDisjoint ⇒ (∀A:Id. ∀es:EO+(Info). ∀thr:Thread. ((thr is one of bss at A) ⇒ Legal(thr)@A))
Definitions occuring in Statement :
ses-protocol1-thread: (thr is one of bss at A),
ses-legal-thread: Legal(thr)@A,
ses-thread: Thread,
ses-disjoint: ActionsDisjoint,
ses-info: Info,
event-ordering+: EO+(Info),
Id: Id,
all: ∀x:A. B[x],
implies: P ⇒ Q
FDL editor aliases :
ses-protocol1-legal
Latex:
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:
2015_07_23-PM-00_16_50
Last ObjectModification:
2012_08_30-PM-04_33_34
Home
Index