Nuprl Definition : solves-information-flow

`solves-information-flow(es;T;S;F;In;X;f) ==`
`  (E(In) ⊆r E(X))`
`  ∧ es-interface-locs-list(es;X;S)`
`  ∧ (∀e:E(X)`
`       ((((f e) = e ∈ E(X) `⇐⇒` ↑e ∈b In) ∧ ((↑e ∈b In) `` (X(e) = In(e) ∈ T)))`
`       ∧ ((¬((f e) = e ∈ E(X)))`
`         `` (information-flow-relation(es;X;F;f e;loc(e)) ∧ (X(e) = information-flow-to(es;X;F;f e;loc(e)) ∈ T)))))`
`  ∧ (∀e:E(X). ∀i:Id.`
`       ((i ∈ S)`
`       `` information-flow-relation(es;X;F;e;i)`
`       `` (∃e':E(X). ((loc(e') = i ∈ Id) ∧ ((f e') = e ∈ E(X)) ∧ (¬(e' = e ∈ E(X)))))))`

Definitions occuring in Statement :  information-flow-to: `information-flow-to(es;X;F;e;i)` information-flow-relation: `information-flow-relation(es;X;F;e;i)` es-interface-locs-list: `es-interface-locs-list(es;X;S)` es-E-interface: `E(X)` eclass-val: `X(e)` in-eclass: `e ∈b X` es-loc: `loc(e)` Id: `Id` l_member: `(x ∈ l)` assert: `↑b` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` not: `¬A` implies: `P `` Q` and: `P ∧ Q` apply: `f a` equal: `s = t ∈ T`
FDL editor aliases :  solves-information-flow

Latex:
solves-information-flow(es;T;S;F;In;X;f)  ==
(E(In)  \msubseteq{}r  E(X))
\mwedge{}  es-interface-locs-list(es;X;S)
\mwedge{}  (\mforall{}e:E(X)
((((f  e)  =  e  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  In)  \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  In)  {}\mRightarrow{}  (X(e)  =  In(e))))
\mwedge{}  ((\mneg{}((f  e)  =  e))
{}\mRightarrow{}  (information-flow-relation(es;X;F;f  e;loc(e))
\mwedge{}  (X(e)  =  information-flow-to(es;X;F;f  e;loc(e)))))))
\mwedge{}  (\mforall{}e:E(X).  \mforall{}i:Id.
((i  \mmember{}  S)
{}\mRightarrow{}  information-flow-relation(es;X;F;e;i)
{}\mRightarrow{}  (\mexists{}e':E(X).  ((loc(e')  =  i)  \mwedge{}  ((f  e')  =  e)  \mwedge{}  (\mneg{}(e'  =  e))))))

Date html generated: 2015_07_20-PM-03_54_03
Last ObjectModification: 2012_02_25-PM-01_57_52

Home Index