---

ses-disjoint-old{i:l}(ses) ==
  es:EO+(Info). e:E.
    (((e  New)
      ((((((e  Send)  (e  Rcv))  (e  Sign))  (e  Verify))
         (e  Encrypt))
         (e  Decrypt)))
     ((e  Send)
       ((((((e  New)  (e  Rcv))  (e  Sign))  (e  Verify))
          (e  Encrypt))
          (e  Decrypt)))
     ((e  Rcv)
       ((((((e  Send)  (e  New))  (e  Sign))  (e  Verify))
          (e  Encrypt))
          (e  Decrypt)))
     ((e  Sign)
       ((((((e  Send)  (e  Rcv))  (e  New))  (e  Verify))
          (e  Encrypt))
          (e  Decrypt)))
     ((e  Verify)
       ((((((e  Send)  (e  Rcv))  (e  Sign))  (e  New))
          (e  Encrypt))
          (e  Decrypt)))
     ((e  Encrypt)
       ((((((e  Send)  (e  Rcv))  (e  Sign))  (e  Verify))
          (e  New))
          (e  Decrypt)))
     ((e  Decrypt)
       ((((((e  Send)  (e  Rcv))  (e  Sign))  (e  Verify))
          (e  Encrypt))
          (e  New))))

---

Definitions :  event-ordering+: EO+(Info),  ses-info: Info,  all: x:A. B[x],  es-E: E,  implies: P  Q,  ses-decrypt: Decrypt,  and: P  Q,  ses-send: Send,  ses-rcv: Rcv,  ses-sign: Sign,  ses-verify: Verify,  ses-encrypt: Encrypt,  not: A,  assert: b,  in-eclass: e  X,  ses-new: New
FDL editor aliases :  ses-disjoint-old

---

ses-disjoint-old\{i:l\}(ses)  ==
    \mforall{}es:EO+(Info).  \mforall{}e:E.
        (((\muparrow{}e  \mmember{}\msubb{}  New)
          {}\mRightarrow{}  ((((((\mneg{}\muparrow{}e  \mmember{}\msubb{}  Send)  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Rcv))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Sign))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Verify))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Encrypt))
                \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Decrypt)))
        \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  Send)
            {}\mRightarrow{}  ((((((\mneg{}\muparrow{}e  \mmember{}\msubb{}  New)  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Rcv))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Sign))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Verify))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Encrypt))
                  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Decrypt)))
        \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  Rcv)
            {}\mRightarrow{}  ((((((\mneg{}\muparrow{}e  \mmember{}\msubb{}  Send)  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  New))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Sign))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Verify))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Encrypt))
                  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Decrypt)))
        \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  Sign)
            {}\mRightarrow{}  ((((((\mneg{}\muparrow{}e  \mmember{}\msubb{}  Send)  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Rcv))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  New))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Verify))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Encrypt))
                  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Decrypt)))
        \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  Verify)
            {}\mRightarrow{}  ((((((\mneg{}\muparrow{}e  \mmember{}\msubb{}  Send)  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Rcv))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Sign))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  New))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Encrypt))
                  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Decrypt)))
        \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  Encrypt)
            {}\mRightarrow{}  ((((((\mneg{}\muparrow{}e  \mmember{}\msubb{}  Send)  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Rcv))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Sign))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Verify))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  New))
                  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Decrypt)))
        \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  Decrypt)
            {}\mRightarrow{}  ((((((\mneg{}\muparrow{}e  \mmember{}\msubb{}  Send)  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Rcv))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Sign))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Verify))  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Encrypt))
                  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  New))))


Date html generated: 2010_08_28-AM-02_34_56
Last ObjectModification: 2010_03_12-PM-03_17_58

Home Index