---

Step * of Lemma hdf-halted-compose2

∀[A,B,C:Type]. ∀[X1:hdataflow(A;B ─→ bag(C))]. ∀[X2:hdataflow(A;B)].
  uiff(↑hdf-halted(X1 o X2);↑(hdf-halted(X1) ∨bhdf-halted(X2))) supposing valueall-type(C)
BY
{ Auto }

1
1. A : Type
2. B : Type
3. C : Type
4. X1 : hdataflow(A;B ─→ bag(C))
5. X2 : hdataflow(A;B)
6. valueall-type(C)
7. ↑hdf-halted(X1 o X2)
⊢ (↑hdf-halted(X1)) ∨ (↑hdf-halted(X2))

2
1. A : Type
2. B : Type
3. C : Type
4. X1 : hdataflow(A;B ─→ bag(C))
5. X2 : hdataflow(A;B)
6. valueall-type(C)
7. ↑(hdf-halted(X1) ∨bhdf-halted(X2))
⊢ ↑hdf-halted(X1 o X2)

---

Latex:


\mforall{}[A,B,C:Type].  \mforall{}[X1:hdataflow(A;B  {}\mrightarrow{}  bag(C))].  \mforall{}[X2:hdataflow(A;B)].
    uiff(\muparrow{}hdf-halted(X1  o  X2);\muparrow{}(hdf-halted(X1)  \mvee{}\msubb{}hdf-halted(X2)))  supposing  valueall-type(C)


By

Auto

---

Home Index