Nuprl Definition : ses-action
Action(e) ==
(↑e ∈b New) ∨ (↑e ∈b Send) ∨ (↑e ∈b Rcv) ∨ (↑e ∈b Encrypt) ∨ (↑e ∈b Decrypt) ∨ (↑e ∈b Sign) ∨ (↑e ∈b Verify)
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
,
in-eclass: e ∈b X
,
assert: ↑b
,
or: P ∨ Q
FDL editor aliases :
ses-action
Latex:
Action(e) ==
(\muparrow{}e \mmember{}\msubb{} New)
\mvee{} (\muparrow{}e \mmember{}\msubb{} Send)
\mvee{} (\muparrow{}e \mmember{}\msubb{} Rcv)
\mvee{} (\muparrow{}e \mmember{}\msubb{} Encrypt)
\mvee{} (\muparrow{}e \mmember{}\msubb{} Decrypt)
\mvee{} (\muparrow{}e \mmember{}\msubb{} Sign)
\mvee{} (\muparrow{}e \mmember{}\msubb{} Verify)
Date html generated:
2016_05_17-AM-11_46_01
Last ObjectModification:
2012_08_30-PM-02_30_22
Theory : event-logic-applications
Home
Index