---

Step * of Lemma Process-stream_wf

∀[M:Type ⟶ Type]
  ∀[msgs:pMsg(P.M[P]) List]. ∀[P:Process(P.M[P])].  (Process-stream(P;msgs) ∈ pExt(P.M[P]) List) 
  supposing Continuous+(P.M[P])
BY
{ (Unfold `Process-stream` 0
   THEN InductionOnList
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN (D 0 THENA Auto)
   THEN (RWO "data-stream-cons" 0 THENA Auto)) }

1
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

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[msgs:pMsg(P.M[P])  List].  \mforall{}[P:Process(P.M[P])].    (Process-stream(P;msgs)  \mmember{}  pExt(P.M[P])  List) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(Unfold  `Process-stream`  0
  THEN  InductionOnList
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  (D  0  THENA  Auto)
  THEN  (RWO  "data-stream-cons"  0  THENA  Auto))

---

Home Index