---

Step * of Lemma iterate-Process_wf

∀[M:Type ⟶ Type]
  ∀[msgs:pMsg(P.M[P]) List]. ∀[P:Process(P.M[P])].  (iterate-Process(P;msgs) ∈ Process(P.M[P])) 
  supposing Continuous+(P.M[P])
BY
{ (Unfold `iterate-Process` 0
   THEN InductionOnList
   THEN Reduce 0
   THEN Auto
   THEN BackThruSomeHyp
   THEN Unfold `dataflow-ap` 0
   THEN Fold `Process-apply` 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `iterate-Process`  0
  THEN  InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Unfold  `dataflow-ap`  0
  THEN  Fold  `Process-apply`  0
  THEN  Auto)

---

Home Index