`∀s:SES`
`  (SecurityAxioms`
`  `` (∀es:EO+(Info). ∀A:Id. ∀thr:Thread.`
`        (Legal(thr)@A`
`        `` (∀n:E(New). ∀e:Act.`
`              (e ∈ thr`
`              `` e has* New(n)`
`              `` (∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)) ∨ (e = n ∈ E) `
`                 supposing ∀e':E`
`                             ((e' < e) `` Action(e') `` e' has* New(n) `` ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈b Send))))))))`

Proof

Definitions occuring in Statement :  ses-legal-thread: `Legal(thr)@A` ses-thread-member: `e ∈ thr` ses-thread: `Thread` ses-axioms: `SecurityAxioms` event-has*: `e has* a` ses-act: `Act` ses-action: `Action(e)` ses-send: `Send` ses-new: `New` ses-info: `Info` security-event-structure: `SES` es-E-interface: `E(X)` eclass-val: `X(e)` in-eclass: `e ∈b X` event-ordering+: `EO+(Info)` es-locl: `(e <loc e')` es-causl: `(e < e')` es-loc: `loc(e)` es-E: `E` Id: `Id` assert: `↑b` uimplies: `b supposing a` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` equal: `s = t ∈ T`

Latex:
\mforall{}s:SES
(SecurityAxioms
(Legal(thr)@A
{}\mRightarrow{}  (\mforall{}n:E(New).  \mforall{}e:Act.
(e  \mmember{}  thr
{}\mRightarrow{}  e  has*  New(n)
{}\mRightarrow{}  (\mexists{}e':E.  ((e'  <loc  e)  \mwedge{}  Action(e')  \mwedge{}  e'  has*  New(n)  \mwedge{}  e'  \mmember{}  thr))  \mvee{}  (e  =  n)
supposing  \mforall{}e':E
((e'  <  e)
{}\mRightarrow{}  Action(e')
{}\mRightarrow{}  e'  has*  New(n)
{}\mRightarrow{}  ((loc(e')  =  A)  \mwedge{}  (\mneg{}\muparrow{}e'  \mmember{}\msubb{}  Send))))))))

Date html generated: 2015_07_23-PM-00_12_38
Last ObjectModification: 2015_02_04-PM-03_51_53

Home Index