---

Step * 1 of Lemma information-flow-to_wf


1. Info : Type
2. T : Type
3. S : Id List
4. F : information-flow(T;S)
5. es : EO+(Info)
6. X : EClass(T)
7. es-interface-locs-list(es;X;S)
8. i : {i:Id| (i ∈ S)} 
9. e : E(X)
10. s : {s:T List| 0 < ||s||} @i
11. X(≤(X)(e)) = s ∈ {s:T List| 0 < ||s||} @i
⊢ (↑can-apply(F loc(e) i;s)) ⇒ (do-apply(F loc(e) i;s) ∈ T)
BY
{ Auto }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  T  :  Type
3.  S  :  Id  List
4.  F  :  information-flow(T;S)
5.  es  :  EO+(Info)
6.  X  :  EClass(T)
7.  es-interface-locs-list(es;X;S)
8.  i  :  \{i:Id|  (i  \mmember{}  S)\} 
9.  e  :  E(X)
10.  s  :  \{s:T  List|  0  <  ||s||\}  @i
11.  X(\mleq{}(X)(e))  =  s@i
\mvdash{}  (\muparrow{}can-apply(F  loc(e)  i;s))  {}\mRightarrow{}  (do-apply(F  loc(e)  i;s)  \mmember{}  T)


By

---

Latex:
Auto

---

Home Index