---

Step * of Lemma hdf-comb3_wf

∀[A,C,B1,B2,B3:Type]. ∀[f:B1 ⟶ B2 ⟶ B3 ⟶ bag(C)]. ∀[X:hdataflow(A;B1)]. ∀[Y:hdataflow(A;B2)]. ∀[Z:hdataflow(A;B3)].
  hdf-comb3(f;X;Y;Z) ∈ hdataflow(A;C) supposing ((↓B2) ∧ (↓B3)) ∧ valueall-type(C)
BY
{ (ProveWfLemma THEN SqExRepD THEN D 0) }

---

Latex:

---

Latex:
\mforall{}[A,C,B1,B2,B3:Type].  \mforall{}[f:B1  {}\mrightarrow{}  B2  {}\mrightarrow{}  B3  {}\mrightarrow{}  bag(C)].  \mforall{}[X:hdataflow(A;B1)].  \mforall{}[Y:hdataflow(A;B2)].
\mforall{}[Z:hdataflow(A;B3)].
    hdf-comb3(f;X;Y;Z)  \mmember{}  hdataflow(A;C)  supposing  ((\mdownarrow{}B2)  \mwedge{}  (\mdownarrow{}B3))  \mwedge{}  valueall-type(C)


By

---

Latex:
(ProveWfLemma  THEN  SqExRepD  THEN  D  0)

---

Home Index