---

Step * of Lemma hdf-union-eq-disju

∀[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)].
  (X + Y = (λx.(inl x)) o X || (λx.(inr x )) o Y ∈ hdataflow(A;B + C)) supposing 
     (valueall-type(B) and 
     valueall-type(C))
BY
{ (Auto THEN BLemma `hdataflow-equal` THEN Auto) }

1
1. A : Type
2. B : Type
3. C : Type
4. X : hdataflow(A;B)
5. Y : hdataflow(A;C)
6. valueall-type(C)
7. valueall-type(B)
8. inputs : A List
⊢ hdf-halted(X + Y*(inputs)) = hdf-halted((λx.(inl x)) o X || (λx.(inr x )) o Y*(inputs))

2
1. A : Type
2. B : Type
3. C : Type
4. X : hdataflow(A;B)
5. Y : hdataflow(A;C)
6. valueall-type(C)
7. valueall-type(B)
8. inputs : A List
9. hdf-halted(X + Y*(inputs)) = hdf-halted((λx.(inl x)) o X || (λx.(inr x )) o Y*(inputs))
10. a : A
⊢ hdf-out(X + Y*(inputs);a) = hdf-out((λx.(inl x)) o X || (λx.(inr x )) o Y*(inputs);a) ∈ bag(B + C)

---

Latex:


\mforall{}[A,B,C:Type].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[Y:hdataflow(A;C)].
    (X  +  Y  =  (\mlambda{}x.(inl  x))  o  X  ||  (\mlambda{}x.(inr  x  ))  o  Y)  supposing 
          (valueall-type(B)  and 
          valueall-type(C))


By

(Auto  THEN  BLemma  `hdataflow-equal`  THEN  Auto)

---

Home Index