### Nuprl Lemma : hdf-buffer_wf

`∀[A,B:Type]. ∀[X:hdataflow(A;B ⟶ bag(B))]. ∀[bs:bag(B)].  hdf-buffer(X;bs) ∈ hdataflow(A;B) supposing valueall-type(B)`

Proof

Definitions occuring in Statement :  hdf-buffer: `hdf-buffer(X;bs)` hdataflow: `hdataflow(A;B)` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type` bag: `bag(T)`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` hdf-buffer: `hdf-buffer(X;bs)` all: `∀x:A. B[x]` implies: `P `` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` callbyvalueall: callbyvalueall has-value: `(a)↓` has-valueall: `has-valueall(a)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` uiff: `uiff(P;Q)` and: `P ∧ Q` exists: `∃x:A. B[x]` prop: `ℙ` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]`

Latex:
\mforall{}[A,B:Type].  \mforall{}[X:hdataflow(A;B  {}\mrightarrow{}  bag(B))].  \mforall{}[bs:bag(B)].
hdf-buffer(X;bs)  \mmember{}  hdataflow(A;B)  supposing  valueall-type(B)

Date html generated: 2016_05_16-AM-10_40_00
Last ObjectModification: 2016_01_17-AM-11_13_07

Theory : halting!dataflow

Home Index