### Nuprl 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))`

Proof

Definitions occuring in Statement :  list: `T List` valueall-type: `valueall-type(T)` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` 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` iterate-hdataflow: `P*(inputs)` hdf-halted: `hdf-halted(P)` hdataflow: `hdataflow(A;B)`
Lemmas :  hdf-union-eq-disju hdf-parallel-bind-halt-eq hdf-compose1_wf union-valueall-type subtype_base_sq bool_wf bool_subtype_base hdf-bind-compose1-left hdf-halted_wf hdataflow_wf iterate-hdataflow_wf hdf-parallel_wf hdf-bind_wf list_wf squash_wf valueall-type_wf eta_conv iff_weakening_equal equal_wf void-valueall-type

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))

Date html generated: 2015_07_22-PM-00_05_52
Last ObjectModification: 2015_02_04-PM-05_09_23

Home Index