---

Step * of Lemma loop-class-state-program-wf-hdf

∀[Info,B:Type].
  ∀[init:Id ─→ bag(B)]. ∀[pr:Id ─→ hdataflow(Info;B ─→ B)].
    (loop-class-state-program(pr;init) ∈ Id ─→ hdataflow(Info;B)) 
  supposing valueall-type(B)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].
    \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[pr:Id  {}\mrightarrow{}  hdataflow(Info;B  {}\mrightarrow{}  B)].
        (loop-class-state-program(pr;init)  \mmember{}  Id  {}\mrightarrow{}  hdataflow(Info;B)) 
    supposing  valueall-type(B)


By

---

Latex:
ProveWfLemma

---

Home Index