---

Step * 2 of Lemma flow-graph-information-flow-relation


1. [Info] : Type
2. [T] : Type
3. S : Id List@i
4. G : Graph(S)@i
5. F : information-flow(T;S)@i
6. es : EO+(Info)@i'
7. X : EClass(T)@i'
8. e : E(X)@i
9. i : Id@i
10. (i ∈ S)@i
11. es-interface-locs-list(es;X;S)@i
12. flow-graph(S;T;F;G)@i
13. information-flow-relation(es;X;F;e;i)
⊢ (loc(e)─→i)∈G
BY
{ (UnfoldTopAb (-1) THEN UnfoldTopAb (-2) THEN FHyp (-2) [-1] THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  [T]  :  Type
3.  S  :  Id  List@i
4.  G  :  Graph(S)@i
5.  F  :  information-flow(T;S)@i
6.  es  :  EO+(Info)@i'
7.  X  :  EClass(T)@i'
8.  e  :  E(X)@i
9.  i  :  Id@i
10.  (i  \mmember{}  S)@i
11.  es-interface-locs-list(es;X;S)@i
12.  flow-graph(S;T;F;G)@i
13.  information-flow-relation(es;X;F;e;i)
\mvdash{}  (loc(e){}\mrightarrow{}i)\mmember{}G


By

---

Latex:
(UnfoldTopAb  (-1)  THEN  UnfoldTopAb  (-2)  THEN  FHyp  (-2)  [-1]  THEN  Auto)\mcdot{}

---

Home Index