Nuprl Definition : ses-protocol1

Protocol1(bss) ==
  λA.∀es:EO+(Info)
       (Honest(A)
       ⇒ (∀e:Act
             ((loc(e) = A ∈ Id)
             ⇒ ((∃thr:Thread. (e ∈ thr ∧ (thr is one of bss at A) ∧ loc(thr)= A))
                ∧ (∀thr1,thr2:Thread.
                     (e ∈ thr1
                     ⇒ (thr1 is one of bss at A)
                     ⇒ e ∈ thr2
                     ⇒ (thr2 is one of bss at A)
                     ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1)))))))


Definitions occuring in Statement :  ses-protocol1-thread: (thr is one of bss at A),  ses-thread-loc: loc(thr)= A,  ses-thread-member: e ∈ thr,  ses-thread: Thread,  ses-act: Act,  ses-honest: Honest(A),  ses-info: Info,  event-ordering+: EO+(Info),  es-loc: loc(e),  Id: Id,  iseg: l1 ≤ l2,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  or: P ∨ Q,  and: P ∧ Q,  lambda: λx.A[x],  equal: s = t ∈ T
FDL editor aliases :  ses-protocol1
Latex:
Protocol1(bss)  ==
    \mlambda{}A.\mforall{}es:EO+(Info)
              (Honest(A)
              {}\mRightarrow{}  (\mforall{}e:Act
                          ((loc(e)  =  A)
                          {}\mRightarrow{}  ((\mexists{}thr:Thread.  (e  \mmember{}  thr  \mwedge{}  (thr  is  one  of  bss  at  A)  \mwedge{}  loc(thr)=  A))
                                \mwedge{}  (\mforall{}thr1,thr2:Thread.
                                          (e  \mmember{}  thr1
                                          {}\mRightarrow{}  (thr1  is  one  of  bss  at  A)
                                          {}\mRightarrow{}  e  \mmember{}  thr2
                                          {}\mRightarrow{}  (thr2  is  one  of  bss  at  A)
                                          {}\mRightarrow{}  (thr1  \mleq{}  thr2  \mvee{}  thr2  \mleq{}  thr1)))))))


Date html generated: 2015_07_23-PM-00_16_44
Last ObjectModification: 2012_08_30-PM-04_33_26

Home Index