Nuprl Lemma : hdf-parallel-bind-eq
∀[A,B,C:Type]. ∀[X1,X2:hdataflow(A;B)]. ∀[X:B ⟶ hdataflow(A;C)].
(X1 >>= X || X2 >>= X = X1 || X2 >>= X ∈ hdataflow(A;C)) supposing (valueall-type(C) and valueall-type(B))
Proof
Definitions occuring in Statement :
hdf-bind: X >>= Y,
hdf-parallel: X || Y,
hdataflow: hdataflow(A;B),
valueall-type: valueall-type(T),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
parallel-class-program: X || Y,
bind-class-program: xpr >>= ypr,
mkid: "$x",
Id: Id,
guard: {T},
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q,
prop: ℙ,
squash: ↓T
Latex:
\mforall{}[A,B,C:Type]. \mforall{}[X1,X2:hdataflow(A;B)]. \mforall{}[X:B {}\mrightarrow{} hdataflow(A;C)].
(X1 >>= X || X2 >>= X = X1 || X2 >>= X) supposing (valueall-type(C) and valueall-type(B))
Date html generated:
2016_05_17-AM-09_12_19
Last ObjectModification:
2016_01_17-PM-09_11_54
Theory : local!classes
Home
Index