Nuprl Definition : ses-disjoint-old
ses-disjoint-old{i:l}(ses) ==
∀es:EO+(Info). ∀e:E.
(((↑e ∈b New)
⇒ ((((((¬↑e ∈b Send) ∧ (¬↑e ∈b Rcv)) ∧ (¬↑e ∈b Sign)) ∧ (¬↑e ∈b Verify)) ∧ (¬↑e ∈b Encrypt)) ∧ (¬↑e ∈b Decrypt)))
∧ ((↑e ∈b Send)
⇒ ((((((¬↑e ∈b New) ∧ (¬↑e ∈b Rcv)) ∧ (¬↑e ∈b Sign)) ∧ (¬↑e ∈b Verify)) ∧ (¬↑e ∈b Encrypt)) ∧ (¬↑e ∈b Decrypt)))
∧ ((↑e ∈b Rcv)
⇒ ((((((¬↑e ∈b Send) ∧ (¬↑e ∈b New)) ∧ (¬↑e ∈b Sign)) ∧ (¬↑e ∈b Verify)) ∧ (¬↑e ∈b Encrypt)) ∧ (¬↑e ∈b Decrypt)))
∧ ((↑e ∈b Sign)
⇒ ((((((¬↑e ∈b Send) ∧ (¬↑e ∈b Rcv)) ∧ (¬↑e ∈b New)) ∧ (¬↑e ∈b Verify)) ∧ (¬↑e ∈b Encrypt)) ∧ (¬↑e ∈b Decrypt)))
∧ ((↑e ∈b Verify)
⇒ ((((((¬↑e ∈b Send) ∧ (¬↑e ∈b Rcv)) ∧ (¬↑e ∈b Sign)) ∧ (¬↑e ∈b New)) ∧ (¬↑e ∈b Encrypt)) ∧ (¬↑e ∈b Decrypt)))
∧ ((↑e ∈b Encrypt)
⇒ ((((((¬↑e ∈b Send) ∧ (¬↑e ∈b Rcv)) ∧ (¬↑e ∈b Sign)) ∧ (¬↑e ∈b Verify)) ∧ (¬↑e ∈b New)) ∧ (¬↑e ∈b Decrypt)))
∧ ((↑e ∈b Decrypt)
⇒ ((((((¬↑e ∈b Send) ∧ (¬↑e ∈b Rcv)) ∧ (¬↑e ∈b Sign)) ∧ (¬↑e ∈b Verify)) ∧ (¬↑e ∈b Encrypt)) ∧ (¬↑e ∈b New))))
Definitions occuring in Statement :
ses-decrypt: Decrypt,
ses-encrypt: Encrypt,
ses-verify: Verify,
ses-sign: Sign,
ses-rcv: Rcv,
ses-send: Send,
ses-new: New,
ses-info: Info,
in-eclass: e ∈b X,
event-ordering+: EO+(Info),
es-E: E,
assert: ↑b,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q
FDL editor aliases :
ses-disjoint-old
Latex:
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:
2016_05_17-PM-00_25_58
Last ObjectModification:
2012_08_30-PM-04_25_01
Theory : event-logic-applications
Home
Index