### 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: 2015_07_23-PM-00_07_46
Last ObjectModification: 2012_08_30-PM-04_24_53

Home Index