---

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

∀[Info,B1,B2,C:Type]. ∀[X1:Id ⟶ hdataflow(Info;B1)]. ∀[X2:Id ⟶ hdataflow(Info;B2)].
∀[Y1:B1 ⟶ Id ⟶ hdataflow(Info;C)]. ∀[Y2:B2 ⟶ Id ⟶ hdataflow(Info;C)].
  (X1 >>= Y1 || X2 >>= Y2
     = X1 + X2 >>= λb.case b of inl(b1) => Y1 b1 | inr(b2) => Y2 b2
     ∈ (Id ⟶ hdataflow(Info;C))) supposing 
     (valueall-type(C) and 
     valueall-type(B1) and 
     valueall-type(B2))
BY
{ (Auto
   THEN (InstLemma `local-class-equality` [⌜Info⌝;⌜C⌝;⌜hdataflow-class(X1) + hdataflow-class(X2) >b> case b
                                                        of inl(b1) =>
                                                        hdataflow-class(Y1 b1)
                                                        | inr(b2) =>
                                                        hdataflow-class(Y2 b2)⌝]⋅
         THENA Auto
         )
   THEN BHyp -1 
   THEN Try ((Auto
              THEN RepUR ``parallel-class-program bind-class-program eclass-disju-program eclass1-program`` 0
              THEN (RWO "hdf-union-eq-disju<" 0 THENA Auto)
              THEN (InstLemma `hdf-parallel-bind-halt-eq-gen` [⌜Info⌝;⌜B1⌝;⌜B2⌝;⌜C⌝;⌜X1 i⌝;⌜X2 i⌝;⌜λx.(Y1 x i)⌝;⌜λx.(Y2 
                                                                                                                     x 
                                                                                                                     i)⌝
                    ;⌜inputs⌝]⋅
                    THENA Auto
                    )
              THEN RepUR ``so_apply`` (-1)
              THEN (RWO "-1" 0 THEN Auto)
              THEN Repeat ((EqCD THEN Auto))
              THEN DProdsAndUnions
              THEN AllReduce
              THEN Auto))
   THEN Try (Complete ((Auto THEN ExtWith [`b'] [⌜(B1 + B2) ⟶ Id ⟶ hdataflow(Info;C)⌝]⋅ THEN Auto)))
   THEN SubsumeC ⌜LocalClass(hdataflow-class(X1) >b> hdataflow-class(Y1 b)
                             || hdataflow-class(X2) >b> hdataflow-class(Y2 b))⌝⋅
   THEN Try (Complete ((Auto
                        THEN Try (Complete ((ExtWith [`b'] [⌜B1 ⟶ Id ⟶ hdataflow(Info;C)⌝]⋅ THEN Auto)))
                        THEN Try (Complete ((ExtWith [`b'] [⌜B2 ⟶ Id ⟶ hdataflow(Info;C)⌝]⋅ THEN Auto))))))
   THEN (BLemma `subtype_rel-equal` THEN Auto)
   THEN EqCD
   THEN Auto
   THEN Symmetry
   THEN BLemma `eclass-disju-bind-left`
   THEN Auto)⋅ }

---

Latex:

---

Latex:
\mforall{}[Info,B1,B2,C:Type].  \mforall{}[X1:Id  {}\mrightarrow{}  hdataflow(Info;B1)].  \mforall{}[X2:Id  {}\mrightarrow{}  hdataflow(Info;B2)].
\mforall{}[Y1:B1  {}\mrightarrow{}  Id  {}\mrightarrow{}  hdataflow(Info;C)].  \mforall{}[Y2:B2  {}\mrightarrow{}  Id  {}\mrightarrow{}  hdataflow(Info;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(B1)  and 
          valueall-type(B2))


By

---

Latex:

(Auto
  THEN  (InstLemma  `local-class-equality`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};
              \mkleeneopen{}hdataflow-class(X1)  +  hdataflow-class(X2)  >b>  case  b
                  of  inl(b1)  =>
                  hdataflow-class(Y1  b1)
                  |  inr(b2)  =>
                  hdataflow-class(Y2  b2)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  BHyp  -1 
  THEN  Try  ((Auto
                        THEN  ...
                        THEN  (RWO  "hdf-union-eq-disju<"  0  THENA  Auto)
                        THEN  (InstLemma  `hdf-parallel-bind-halt-eq-gen`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}B1\mkleeneclose{};\mkleeneopen{}B2\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X1  i\mkleeneclose{};\mkleeneopen{}X2  i\mkleeneclose{};
                                    \mkleeneopen{}\mlambda{}x.(Y1  x  i)\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(Y2  x  i)\mkleeneclose{};\mkleeneopen{}inputs\mkleeneclose{}]\mcdot{}
                                    THENA  Auto
                                    )
                        THEN  RepUR  ``so\_apply``  (-1)
                        THEN  (RWO  "-1"  0  THEN  Auto)
                        THEN  Repeat  ((EqCD  THEN  Auto))
                        THEN  DProdsAndUnions
                        THEN  AllReduce
                        THEN  Auto))
  THEN  Try  (Complete  ((Auto  THEN  ExtWith  [`b']  [\mkleeneopen{}(B1  +  B2)  {}\mrightarrow{}  Id  {}\mrightarrow{}  hdataflow(Info;C)\mkleeneclose{}]\mcdot{}  THEN  Auto)))
  THEN  SubsumeC  \mkleeneopen{}LocalClass(hdataflow-class(X1)  >b>  hdataflow-class(Y1  b)
                                                      ||  hdataflow-class(X2)  >b>  hdataflow-class(Y2  b))\mkleeneclose{}\mcdot{}
  THEN  Try  (Complete  ((Auto
                                            THEN  Try  (Complete  ((ExtWith  [`b']  [\mkleeneopen{}B1  {}\mrightarrow{}  Id  {}\mrightarrow{}  hdataflow(Info;C)\mkleeneclose{}]\mcdot{}
                                                                                      THEN  Auto
                                                                                      )))
                                            THEN  Try  (Complete  ((ExtWith  [`b']  [\mkleeneopen{}B2  {}\mrightarrow{}  Id  {}\mrightarrow{}  hdataflow(Info;C)\mkleeneclose{}]\mcdot{}
                                                                                      THEN  Auto
                                                                                      ))))))
  THEN  (BLemma  `subtype\_rel-equal`  THEN  Auto)
  THEN  EqCD
  THEN  Auto
  THEN  Symmetry
  THEN  BLemma  `eclass-disju-bind-left`
  THEN  Auto)\mcdot{}

---

Home Index