---

Step * of 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))
BY
{ (BasicUniformUnivCD Auto THEN (UnivCD THENA Try (Complete (Auto)))) }

1
.....wf..... 
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. ↑can-apply(F loc(e) i;X(≤(X)(e)))
⊢ can-apply(F loc(e) i;X(≤(X)(e))) ∈ 𝔹

2
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

---

Latex:

---

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))


By

---

Latex:
(BasicUniformUnivCD  Auto  THEN  (UnivCD  THENA  Try  (Complete  (Auto))))

---

Home Index