---

Step * of Lemma hdf-parallel-bind-eq-gen

∀[A,B1,B2,C:Type]. ∀[X1:hdataflow(A;B1)]. ∀[X2:hdataflow(A;B2)]. ∀[Y1:B1 ⟶ hdataflow(A;C)]. ∀[Y2:B2 ⟶ hdataflow(A;C)].
  (X1 >>= Y1 || X2 >>= Y2 = X1 + X2 >>= λb.case b of inl(b1) => Y1 b1 | inr(b2) => Y2 b2 ∈ hdataflow(A;C)) supposing 
     (valueall-type(C) and 
     valueall-type(B2) and 
     valueall-type(B1))
BY
{ (InstLemma `parallel-bind-program-eq-gen` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Auto
   THEN (InstHyp [⌜λi.X1⌝;⌜λi.X2⌝;⌜λb,i. (Y1 b)⌝;⌜λb,i. (Y2 b)⌝] 5⋅ THENA Auto)
   THEN RepUR ``bind-class-program parallel-class-program eclass-disju-program eclass1-program`` (-1)
   THEN (ApFunToHypEquands `F' ⌜F "any"⌝ ⌜hdataflow(A;C)⌝ (-1)⋅ THENA Auto)
   THEN Reduce (-1)
   THEN (Assert ⌜Y1 = (λx.(Y1 x)) ∈ (B1 ⟶ hdataflow(A;C))⌝⋅ THENA (Ext THEN Reduce 0 THEN Auto))
   THEN (Assert ⌜Y2 = (λx.(Y2 x)) ∈ (B2 ⟶ hdataflow(A;C))⌝⋅ THENA (Ext THEN Reduce 0 THEN Auto))
   THEN (HypSubst (-1) 0 THENA Auto)
   THEN (HypSubst (-2) 0 THENA Auto)
   THEN (HypSubst (-3) 0 THENA Auto)
   THEN Repeat ((EqCD THEN Auto))
   THEN Try (DProdsAndUnions)
   THEN AllReduce
   THEN Auto
   THEN RWO "hdf-union-eq-disju<" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B1,B2,C:Type].  \mforall{}[X1:hdataflow(A;B1)].  \mforall{}[X2:hdataflow(A;B2)].  \mforall{}[Y1:B1  {}\mrightarrow{}  hdataflow(A;C)].
\mforall{}[Y2:B2  {}\mrightarrow{}  hdataflow(A;C)].
    (X1  >>=  Y1  ||  X2  >>=  Y2  =  X1  +  X2  >>=  \mlambda{}b.case  b  of  inl(b1)  =>  Y1  b1  |  inr(b2)  =>  Y2  b2)  supposing 
          (valueall-type(C)  and 
          valueall-type(B2)  and 
          valueall-type(B1))


By

---

Latex:
(InstLemma  `parallel-bind-program-eq-gen`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}i.X1\mkleeneclose{};\mkleeneopen{}\mlambda{}i.X2\mkleeneclose{};\mkleeneopen{}\mlambda{}b,i.  (Y1  b)\mkleeneclose{};\mkleeneopen{}\mlambda{}b,i.  (Y2  b)\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  RepUR  ``bind-class-program  parallel-class-program  eclass-disju-program  eclass1-program``  (-1)
  THEN  (ApFunToHypEquands  `F'  \mkleeneopen{}F  "any"\mkleeneclose{}  \mkleeneopen{}hdataflow(A;C)\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  (Assert  \mkleeneopen{}Y1  =  (\mlambda{}x.(Y1  x))\mkleeneclose{}\mcdot{}  THENA  (Ext  THEN  Reduce  0  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}Y2  =  (\mlambda{}x.(Y2  x))\mkleeneclose{}\mcdot{}  THENA  (Ext  THEN  Reduce  0  THEN  Auto))
  THEN  (HypSubst  (-1)  0  THENA  Auto)
  THEN  (HypSubst  (-2)  0  THENA  Auto)
  THEN  (HypSubst  (-3)  0  THENA  Auto)
  THEN  Repeat  ((EqCD  THEN  Auto))
  THEN  Try  (DProdsAndUnions)
  THEN  AllReduce
  THEN  Auto
  THEN  RWO  "hdf-union-eq-disju<"  0
  THEN  Auto)

---

Home Index