---

ActionsDisjoint ==
  es:EO+(Info)
    f:E  
     e:E
       (((e  New)  ((f e) = 1))
        ((e  Send)  ((f e) = 2))
        ((e  Rcv)  ((f e) = 3))
        ((e  Sign)  ((f e) = 4))
        ((e  Verify)  ((f e) = 5))
        ((e  Encrypt)  ((f e) = 6))
        ((e  Decrypt)  ((f e) = 7)))

---

Definitions :  event-ordering+: EO+(Info),  ses-info: Info,  exists: x:A. B[x],  function: x:A  B[x],  all: x:A. B[x],  es-E: E,  ses-new: New,  ses-send: Send,  ses-rcv: Rcv,  ses-sign: Sign,  ses-verify: Verify,  and: P  Q,  ses-encrypt: Encrypt,  implies: P  Q,  assert: b,  in-eclass: e  X,  ses-decrypt: Decrypt,  equal: s = t,  int: ,  apply: f a,  natural_number: $n
FDL editor aliases :  ses-disjoint

---

ActionsDisjoint  ==
    \mforall{}es:EO+(Info)
        \mexists{}f:E  {}\mrightarrow{}  \mBbbZ{}
          \mforall{}e:E
              (((\muparrow{}e  \mmember{}\msubb{}  New)  {}\mRightarrow{}  ((f  e)  =  1))
              \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  Send)  {}\mRightarrow{}  ((f  e)  =  2))
              \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  Rcv)  {}\mRightarrow{}  ((f  e)  =  3))
              \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  Sign)  {}\mRightarrow{}  ((f  e)  =  4))
              \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  Verify)  {}\mRightarrow{}  ((f  e)  =  5))
              \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  Encrypt)  {}\mRightarrow{}  ((f  e)  =  6))
              \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  Decrypt)  {}\mRightarrow{}  ((f  e)  =  7)))


Date html generated: 2010_08_28-AM-02_34_46
Last ObjectModification: 2010_03_12-PM-03_20_20

Home Index