---

Step * of Lemma hdf-parallel-bind-halt-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)].
  (∀inputs:A List
     hdf-halted(X1 >>= Y1 || X2 >>= Y2*(inputs)) 
     = hdf-halted(X1 + X2 >>= λx.case x of inl(b1) => Y1[b1] | inr(b2) => Y2[b2]*(inputs))) supposing 
     (valueall-type(C) and 
     valueall-type(B1) and 
     valueall-type(B2))
BY
{ (Auto
   THEN (InstLemma `hdf-union-eq-disju` [⌈A⌉;⌈B1⌉;⌈B2⌉;⌈X1⌉;⌈X2⌉]⋅ THENA Auto)
   THEN (HypSubst' -1 0 THENA (Auto THEN Using [`A',⌈A⌉;`B',⌈C⌉] (BLemma `hdf-halted_wf`)⋅ THEN Auto))
   THEN (InstLemma `hdf-parallel-bind-halt-eq` [⌈A⌉;⌈B1 + B2⌉;⌈C⌉;⌈(λx.(inl x)) o X1⌉;⌈(λx.(inr x )) o X2⌉;
         ⌈λx.case x of inl(b1) => Y1[b1] | inr(b2) => Y2[b2]⌉;⌈inputs⌉]⋅
         THENA Auto
         )
   THEN RevHypSubst' (-1) 0
   THEN (InstLemma `hdf-bind-compose1-left` [⌈A⌉;⌈B1⌉;⌈B1 + B2⌉;⌈C⌉;⌈λx.(inl x)⌉;⌈X1⌉;⌈λx.case x
                                                                                           of inl(b1) =>
                                                                                           Y1[b1]
                                                                                           | inr(b2) =>
                                                                                           Y2[b2]⌉]⋅
         THENA Auto
         )
   THEN (HypSubst (-1) 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN (InstLemma `hdf-bind-compose1-left` [⌈A⌉;⌈B2⌉;⌈B1 + B2⌉;⌈C⌉;⌈λx.(inr x )⌉;⌈X2⌉;⌈λx.case x
                                                                                            of inl(b1) =>
                                                                                            Y1[b1]
                                                                                            | inr(b2) =>
                                                                                            Y2[b2]⌉]⋅
         THENA Auto
         )
   THEN (HypSubst (-1) 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN Repeat ((EqCD THEN Auto))
   THEN Ext
   THEN RepUR ``so_apply`` 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)].
    (\mforall{}inputs:A  List
          hdf-halted(X1  >>=  Y1  ||  X2  >>=  Y2*(inputs)) 
          =  hdf-halted(X1  +  X2
                                      >>=  \mlambda{}x.case  x  of  inl(b1)  =>  Y1[b1]  |  inr(b2)  =>  Y2[b2]*(inputs)))  supposing 
          (valueall-type(C)  and 
          valueall-type(B1)  and 
          valueall-type(B2))


By

---

Latex:
(Auto
  THEN  (InstLemma  `hdf-union-eq-disju`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B1\mkleeneclose{};\mkleeneopen{}B2\mkleeneclose{};\mkleeneopen{}X1\mkleeneclose{};\mkleeneopen{}X2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  -1  0  THENA  (Auto  THEN  Using  [`A',\mkleeneopen{}A\mkleeneclose{};`B',\mkleeneopen{}C\mkleeneclose{}]  (BLemma  `hdf-halted\_wf`)\mcdot{}  THEN  Auto))
  THEN  (InstLemma  `hdf-parallel-bind-halt-eq`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B1  +  B2\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}(\mlambda{}x.(inl  x))  o  X1\mkleeneclose{};
              \mkleeneopen{}(\mlambda{}x.(inr  x  ))  o  X2\mkleeneclose{};\mkleeneopen{}\mlambda{}x.case  x  of  inl(b1)  =>  Y1[b1]  |  inr(b2)  =>  Y2[b2]\mkleeneclose{};\mkleeneopen{}inputs\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  RevHypSubst'  (-1)  0
  THEN  (InstLemma  `hdf-bind-compose1-left`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B1\mkleeneclose{};\mkleeneopen{}B1  +  B2\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(inl  x)\mkleeneclose{};\mkleeneopen{}X1\mkleeneclose{};
              \mkleeneopen{}\mlambda{}x.case  x  of  inl(b1)  =>  Y1[b1]  |  inr(b2)  =>  Y2[b2]\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (HypSubst  (-1)  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  (InstLemma  `hdf-bind-compose1-left`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B2\mkleeneclose{};\mkleeneopen{}B1  +  B2\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(inr  x  )\mkleeneclose{};\mkleeneopen{}X2\mkleeneclose{};
              \mkleeneopen{}\mlambda{}x.case  x  of  inl(b1)  =>  Y1[b1]  |  inr(b2)  =>  Y2[b2]\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (HypSubst  (-1)  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  Repeat  ((EqCD  THEN  Auto))
  THEN  Ext
  THEN  RepUR  ``so\_apply``  0
  THEN  Auto)

---

Home Index