---

Step * 1 of Lemma Process-stream_wf


1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. u : pMsg(P.M[P])
4. v : pMsg(P.M[P]) List
5. ∀[P:Process(P.M[P])]. (data-stream(P;v) ∈ pExt(P.M[P]) List)
6. P : Process(P.M[P])
⊢ [snd(P(u)) / data-stream(fst(P(u));v)] ∈ pExt(P.M[P]) List
BY
{ (Unfold `dataflow-ap` 0 THEN Fold `Process-apply` 0 THEN MemCD THEN Try (BackThruSomeHyp) THEN Auto) }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  u  :  pMsg(P.M[P])
4.  v  :  pMsg(P.M[P])  List
5.  \mforall{}[P:Process(P.M[P])].  (data-stream(P;v)  \mmember{}  pExt(P.M[P])  List)
6.  P  :  Process(P.M[P])
\mvdash{}  [snd(P(u))  /  data-stream(fst(P(u));v)]  \mmember{}  pExt(P.M[P])  List


By

---

Latex:
(Unfold  `dataflow-ap`  0  THEN  Fold  `Process-apply`  0  THEN  MemCD  THEN  Try  (BackThruSomeHyp)  THEN  Auto)

---

Home Index