---

Step * of Lemma hdf-at-locs_wf

∀[A,B:Type]. ∀[pr:Id ⟶ hdataflow(A;B)]. ∀[i:Id]. ∀[locs:bag(Id)].  (hdf-at-locs(pr;i;locs) ∈ hdataflow(A;B))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[pr:Id  {}\mrightarrow{}  hdataflow(A;B)].  \mforall{}[i:Id].  \mforall{}[locs:bag(Id)].
    (hdf-at-locs(pr;i;locs)  \mmember{}  hdataflow(A;B))


By

---

Latex:
ProveWfLemma

---

Home Index