Nuprl Lemma : hdf-bind-ap

`∀[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:B ⟶ hdataflow(A;C)]. ∀[a:A].`
`  X >>= Y(a)`
`  = <fst(X(a)) ([y∈bag-map(λx.(fst(Y x(a)));snd(X(a)))|¬bhdf-halted(y)]) >>= Y, ⋃p∈bag-map(λx.Y x(a);snd(X(a))).snd(p)>`
`  ∈ (hdataflow(A;C) × bag(C)) `
`  supposing valueall-type(C)`

Proof

Definitions occuring in Statement :  hdf-bind-gen: `X (hdfs) >>= Y` hdf-bind: `X >>= Y` hdf-halted: `hdf-halted(P)` hdf-ap: `X(a)` hdataflow: `hdataflow(A;B)` valueall-type: `valueall-type(T)` bnot: `¬bb` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` pi1: `fst(t)` pi2: `snd(t)` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` pair: `<a, b>` product: `x:A × B[x]` universe: `Type` equal: `s = t ∈ T` bag-combine: `⋃x∈bs.f[x]` bag-filter: `[x∈b|p[x]]` bag-map: `bag-map(f;bs)` bag: `bag(T)`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` top: `Top` all: `∀x:A. B[x]` compose: `f o g` implies: `P `` Q` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` pi2: `snd(t)`

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[Y:B  {}\mrightarrow{}  hdataflow(A;C)].  \mforall{}[a:A].
X  >>=  Y(a)
=  <fst(X(a))  ([y\mmember{}bag-map(\mlambda{}x.(fst(Y  x(a)));snd(X(a)))|\mneg{}\msubb{}hdf-halted(y)])  >>=  Y
,  \mcup{}p\mmember{}bag-map(\mlambda{}x.Y  x(a);snd(X(a))).snd(p)
>
supposing  valueall-type(C)

Date html generated: 2016_05_16-AM-10_43_15
Last ObjectModification: 2015_12_28-PM-07_43_13

Theory : halting!dataflow

Home Index