---

Step * of Lemma hdf-parallel-compose-eq

∀[A,B,C:Type]. ∀[X1,X2:hdataflow(A;B ⟶ bag(C))]. ∀[X:hdataflow(A;B)].
  (X1 o X || X2 o X = (X1 || X2 o X) ∈ hdataflow(A;C)) supposing (valueall-type(C) and valueall-type(B) and (↓B))
BY
{ (InstLemma `parallel-compose2-program-eq` []
   THEN RepeatFor 3 (ParallelLast')
   THEN Auto
   THEN (InstHyp [⌜λi.X1⌝;⌜λi.X2⌝;⌜λi.X⌝] 4⋅ THENA Auto)
   THEN RepUR ``eclass2-program parallel-class-program`` (-1)
   THEN (ApFunToHypEquands `F' ⌜F "any"⌝ ⌜hdataflow(A;C)⌝ (-1)⋅ THENA Auto)
   THEN Reduce (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[X1,X2:hdataflow(A;B  {}\mrightarrow{}  bag(C))].  \mforall{}[X: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  RepeatFor  3  (ParallelLast')
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}i.X1\mkleeneclose{};\mkleeneopen{}\mlambda{}i.X2\mkleeneclose{};\mkleeneopen{}\mlambda{}i.X\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
  THEN  RepUR  ``eclass2-program  parallel-class-program``  (-1)
  THEN  (ApFunToHypEquands  `F'  \mkleeneopen{}F  "any"\mkleeneclose{}  \mkleeneopen{}hdataflow(A;C)\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Auto)

---

Home Index