---

Step * of Lemma hdf-run_wf

∀[A,B:Type]. ∀[P:A ⟶ (hdataflow(A;B) × bag(B))].  (hdf-run(P) ∈ hdataflow(A;B))
BY
{ (ProveWfLemma
   THEN (InstLemma `hdataflow-ext` [⌜A⌝;⌜B⌝]⋅ THENA Auto)
   THEN SubsumeC ⌜A ⟶ (hdataflow(A;B) × bag(B))?⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[P:A  {}\mrightarrow{}  (hdataflow(A;B)  \mtimes{}  bag(B))].    (hdf-run(P)  \mmember{}  hdataflow(A;B))


By

---

Latex:
(ProveWfLemma
  THEN  (InstLemma  `hdataflow-ext`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SubsumeC  \mkleeneopen{}A  {}\mrightarrow{}  (hdataflow(A;B)  \mtimes{}  bag(B))?\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index