---

Step * of Lemma information-flow-to_wf

∀[Info,T:Type]. ∀[S:Id List]. ∀[F:information-flow(T;S)]. ∀[es:EO+(Info)]. ∀[X:EClass(T)].
  ∀[i:{i:Id| (i ∈ S)} ]. ∀[e:E(X)].  information-flow-to(es;X;F;e;i) ∈ T supposing information-flow-relation(es;X;F;e;i)\000C 
  supposing es-interface-locs-list(es;X;S)
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN Unfolds ``information-flow-relation information-flow-to`` 0
   THEN (GenConcl ⌜X(≤(X)(e)) = s ∈ {s:T List| 0 < ||s||} ⌝⋅
         THENA (Auto
                THEN (RWO "length-es-interface-vals" 0 THEN Auto)
                THEN BLemma `es-interface-predecessors-nonempty`
                THEN Auto)
         )) }

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

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].  \mforall{}[S:Id  List].  \mforall{}[F:information-flow(T;S)].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(T)].
    \mforall{}[i:\{i:Id|  (i  \mmember{}  S)\}  ].  \mforall{}[e:E(X)].
        information-flow-to(es;X;F;e;i)  \mmember{}  T  supposing  information-flow-relation(es;X;F;e;i) 
    supposing  es-interface-locs-list(es;X;S)


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  Unfolds  ``information-flow-relation  information-flow-to``  0
  THEN  (GenConcl  \mkleeneopen{}X(\mleq{}(X)(e))  =  s\mkleeneclose{}\mcdot{}
              THENA  (Auto
                            THEN  (RWO  "length-es-interface-vals"  0  THEN  Auto)
                            THEN  BLemma  `es-interface-predecessors-nonempty`
                            THEN  Auto)
              ))

---

Home Index