---

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

∀[A,B,C:Type]. ∀[X1,X2:hdataflow(A;B)]. ∀[X:B ⟶ hdataflow(A;C)].
  (∀inputs:A List. hdf-halted(X1 >>= X || X2 >>= X*(inputs)) = hdf-halted(X1 || X2 >>= X*(inputs))) supposing 
     (valueall-type(C) and 
     valueall-type(B))
BY
{ Auto }

1
1. A : Type
2. B : Type
3. C : Type
4. X1 : hdataflow(A;B)
5. X2 : hdataflow(A;B)
6. X : B ⟶ hdataflow(A;C)
7. valueall-type(B)
8. valueall-type(C)
9. inputs : A List@i
⊢ hdf-halted(X1 >>= X || X2 >>= X*(inputs)) = hdf-halted(X1 || X2 >>= X*(inputs))

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index