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:
2016_05_16-PM-11_14_51
Last ObjectModification:
2012_02_25-PM-01_57_52
Theory : event-ordering
Home
Index