---

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:


\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

ProveWfLemma

---

Home Index