### Nuprl Lemma : hdf-compose2-ap

`∀[A,B,C:Type]. ∀[X:hdataflow(A;B ⟶ bag(C))]. ∀[Y:hdataflow(A;B)].`
`  ∀[a:A]. (X o Y(a) = <(fst(X(a))) o (fst(Y(a))), ⋃f∈snd(X(a)).⋃b∈snd(Y(a)).f b> ∈ (hdataflow(A;C) × bag(C))) `
`  supposing valueall-type(C)`

Proof

Definitions occuring in Statement :  hdf-compose2: `X o Y` hdf-ap: `X(a)` hdataflow: `hdataflow(A;B)` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` pi1: `fst(t)` pi2: `snd(t)` apply: `f a` 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: `bag(T)`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` hdf-ap: `X(a)` hdf-compose2: `X o Y` mk-hdf: `mk-hdf(s,m.G[s; m];st.H[st];s0)` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` bor: `p ∨bq` ifthenelse: `if b then t else f fi ` top: `Top` subtype_rel: `A ⊆r B` ext-eq: `A ≡ B` assert: `↑b` bfalse: `ff` false: `False` prop: `ℙ` hdf-halt: `hdf-halt()` pi1: `fst(t)` pi2: `snd(t)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` callbyvalueall: callbyvalueall evalall: `evalall(t)` bag-combine: `⋃x∈bs.f[x]` bag-union: `bag-union(bbs)` concat: `concat(ll)` reduce: `reduce(f;k;as)` list_ind: list_ind bag-map: `bag-map(f;bs)` map: `map(f;as)` empty-bag: `{}` nil: `[]` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` exposed-bfalse: `exposed-bfalse` not: `¬A` true: `True` has-value: `(a)↓` has-valueall: `has-valueall(a)`

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[X:hdataflow(A;B  {}\mrightarrow{}  bag(C))].  \mforall{}[Y:hdataflow(A;B)].
\mforall{}[a:A].  (X  o  Y(a)  =  <(fst(X(a)))  o  (fst(Y(a))),  \mcup{}f\mmember{}snd(X(a)).\mcup{}b\mmember{}snd(Y(a)).f  b>)
supposing  valueall-type(C)

Date html generated: 2016_05_16-AM-10_39_31
Last ObjectModification: 2015_12_28-PM-07_45_48

Theory : halting!dataflow

Home Index