Nuprl Lemma : flow-graph-information-flow-relation
∀[Info,T:Type].
∀S:Id List. ∀G:Graph(S). ∀F:information-flow(T;S). ∀es:EO+(Info). ∀X:EClass(T). ∀e:E(X). ∀i:Id.
((i ∈ S)
⇒ es-interface-locs-list(es;X;S)
⇒ flow-graph(S;T;F;G)
⇒ (loc(e)─→i)∈G supposing information-flow-relation(es;X;F;e;i))
Proof
Definitions occuring in Statement :
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: EClass(A[eo; e]),
event-ordering+: EO+(Info),
flow-graph: flow-graph(S;T;F;G),
information-flow: information-flow(T;S),
es-loc: loc(e),
id-graph-edge: (i─→j)∈G,
id-graph: Graph(S),
Id: Id,
l_member: (x ∈ l),
list: T List,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
universe: Type
Lemmas :
assert_witness,
information-flow-relation_wf,
l_member_wf,
Id_wf,
flow-graph_wf,
es-interface-locs-list_wf,
es-interface-subtype_rel2,
es-E_wf,
event-ordering+_subtype,
event-ordering+_wf,
top_wf,
es-E-interface_wf,
eclass_wf,
information-flow_wf,
id-graph_wf,
list_wf,
less_than_wf,
length_wf,
isl_wf,
length-es-interface-vals,
es-interface-predecessors-nonempty,
es-loc_wf
Latex:
\mforall{}[Info,T:Type].
\mforall{}S:Id List. \mforall{}G:Graph(S). \mforall{}F:information-flow(T;S). \mforall{}es:EO+(Info). \mforall{}X:EClass(T). \mforall{}e:E(X). \mforall{}i:Id.
((i \mmember{} S)
{}\mRightarrow{} es-interface-locs-list(es;X;S)
{}\mRightarrow{} flow-graph(S;T;F;G)
{}\mRightarrow{} (loc(e){}\mrightarrow{}i)\mmember{}G supposing information-flow-relation(es;X;F;e;i))
Date html generated:
2015_07_20-PM-03_53_10
Last ObjectModification:
2015_01_27-PM-10_15_24
Home
Index