---

Step * of Lemma parallel-bind-program-eq

∀[Info,B,C:Type]. ∀[X1,X2:Id ⟶ hdataflow(Info;B)]. ∀[X:B ⟶ Id ⟶ hdataflow(Info;C)].
  (X1 >>= X || X2 >>= X = X1 || X2 >>= X ∈ (Id ⟶ hdataflow(Info;C))) supposing (valueall-type(C) and valueall-type(B))
BY
{ (Auto
   THEN (InstLemma `local-class-equality` [⌜Info⌝;⌜C⌝;
         ⌜hdataflow-class(X1) || hdataflow-class(X2) >b> hdataflow-class(X b)⌝]⋅
         THENA Auto
         )
   THEN BHyp -1 
   THEN Try ((Auto
              THEN RepUR ``parallel-class-program bind-class-program`` 0
              THEN BLemma `hdf-parallel-bind-halt-eq`
              THEN Auto))
   THEN Try (Complete ((Auto THEN ExtWith [`b'] [⌜B ⟶ Id ⟶ hdataflow(Info;C)⌝]⋅ THEN Auto)))
   THEN SubsumeC ⌜LocalClass(hdataflow-class(X1) >b> hdataflow-class(X b)
                             || hdataflow-class(X2) >b> hdataflow-class(X b))⌝⋅
   THEN Try (Complete ((Auto THEN ExtWith [`b'] [⌜B ⟶ Id ⟶ hdataflow(Info;C)⌝]⋅ THEN Auto)))
   THEN (BLemma `subtype_rel-equal` THEN Auto)
   THEN EqCD
   THEN Auto
   THEN Symmetry
   THEN BLemma `parallel-class-bind-left`
   THEN Auto)⋅ }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `local-class-equality`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};
              \mkleeneopen{}hdataflow-class(X1)  ||  hdataflow-class(X2)  >b>  hdataflow-class(X  b)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  BHyp  -1 
  THEN  Try  ((Auto
                        THEN  RepUR  ``parallel-class-program  bind-class-program``  0
                        THEN  BLemma  `hdf-parallel-bind-halt-eq`
                        THEN  Auto))
  THEN  Try  (Complete  ((Auto  THEN  ExtWith  [`b']  [\mkleeneopen{}B  {}\mrightarrow{}  Id  {}\mrightarrow{}  hdataflow(Info;C)\mkleeneclose{}]\mcdot{}  THEN  Auto)))
  THEN  SubsumeC  \mkleeneopen{}LocalClass(hdataflow-class(X1)  >b>  hdataflow-class(X  b)
                                                      ||  hdataflow-class(X2)  >b>  hdataflow-class(X  b))\mkleeneclose{}\mcdot{}
  THEN  Try  (Complete  ((Auto  THEN  ExtWith  [`b']  [\mkleeneopen{}B  {}\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  `parallel-class-bind-left`
  THEN  Auto)\mcdot{}

---

Home Index