---

Step * of Lemma hdf-parallel-bind-eq

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

---

Latex:

---

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


By

---

Latex:
(InstLemma  `parallel-bind-program-eq`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}i.X1\mkleeneclose{};\mkleeneopen{}\mlambda{}i.X2\mkleeneclose{};\mkleeneopen{}\mlambda{}b,i.  (X  b)\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
  THEN  RepUR  ``bind-class-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  Assert  \mkleeneopen{}X  =  (\mlambda{}x.(X  x))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Ext
  THEN  Reduce  0
  THEN  Auto)

---

Home Index