### Nuprl Lemma : hdf-parallel-bind-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)].`
`  (X1 >>= Y1 || X2 >>= Y2 = X1 + X2 >>= λb.case b of inl(b1) => Y1 b1 | inr(b2) => Y2 b2 ∈ hdataflow(A;C)) supposing `
`     (valueall-type(C) and `
`     valueall-type(B2) and `
`     valueall-type(B1))`

Proof

Definitions occuring in Statement :  valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` apply: `f a` lambda: `λx.A[x]` function: `x:A ─→ B[x]` decide: `case b of inl(x) => s[x] | inr(y) => t[y]` universe: `Type` equal: `s = t ∈ T` hdf-bind: `X >>= Y` hdf-union: `X + Y` hdf-parallel: `X || Y` hdataflow: `hdataflow(A;B)`
Lemmas :  parallel-bind-program-eq-gen Id_wf hdataflow_wf hdf-bind_wf squash_wf valueall-type_wf hdf-parallel_wf hdf-compose1_wf union-valueall-type hdf-union-eq-disju iff_weakening_equal equal_wf hdf-union_wf

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)].
(X1  >>=  Y1  ||  X2  >>=  Y2  =  X1  +  X2  >>=  \mlambda{}b.case  b  of  inl(b1)  =>  Y1  b1  |  inr(b2)  =>  Y2  b2)  supposing
(valueall-type(C)  and
valueall-type(B2)  and
valueall-type(B1))

Date html generated: 2015_07_22-PM-00_05_58
Last ObjectModification: 2015_02_04-PM-05_09_21

Home Index