Nuprl Definition : ses-disjoint
ActionsDisjoint ==
∀es:EO+(Info)
∃f:E ⟶ ℤ
∀e:E
(((↑e ∈b New) ⇒ ((f e) = 1 ∈ ℤ))
∧ ((↑e ∈b Send) ⇒ ((f e) = 2 ∈ ℤ))
∧ ((↑e ∈b Rcv) ⇒ ((f e) = 3 ∈ ℤ))
∧ ((↑e ∈b Sign) ⇒ ((f e) = 4 ∈ ℤ))
∧ ((↑e ∈b Verify) ⇒ ((f e) = 5 ∈ ℤ))
∧ ((↑e ∈b Encrypt) ⇒ ((f e) = 6 ∈ ℤ))
∧ ((↑e ∈b Decrypt) ⇒ ((f e) = 7 ∈ ℤ)))
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],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
ses-disjoint
Latex:
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:
2016_05_17-PM-00_25_45
Last ObjectModification:
2012_08_30-PM-04_24_53
Theory : event-logic-applications
Home
Index