---

Step * of Lemma parallel-class-program-compose2-eq

∀[A,B,C:Type]. ∀[X1,X2:Id ─→ hdataflow(A;B ─→ bag(C))]. ∀[X:Id ─→ hdataflow(A;B)].
  (X1 o X || X2 o X = X1 || X2 o X ∈ (Id ─→ hdataflow(A;C))) supposing (valueall-type(C) and valueall-type(B) and (↓B))
BY
{ (InstLemma `parallel-compose2-program-eq` [] THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[X1,X2:Id  {}\mrightarrow{}  hdataflow(A;B  {}\mrightarrow{}  bag(C))].  \mforall{}[X:Id  {}\mrightarrow{}  hdataflow(A;B)].
    (X1  o  X  ||  X2  o  X  =  X1  ||  X2  o  X)  supposing  (valueall-type(C)  and  valueall-type(B)  and  (\mdownarrow{}B))


By

---

Latex:
(InstLemma  `parallel-compose2-program-eq`  []  THEN  Trivial)

---

Home Index