Nuprl Lemma : hdf-parallel-bind-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)].
(X1 >>= Y1 || X2 >>= Y2 = X1 + X2 >>= λb.case b of inl(b1) => Y1 b1 | inr(b2) => Y2 b2 ∈ hdataflow(A;C)) supposing
(valueall-type(C) and
valueall-type(B2) and
valueall-type(B1))
Proof
Definitions occuring in Statement :
valueall-type: valueall-type(T),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
apply: f a,
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,
hdataflow: hdataflow(A;B)
Lemmas :
parallel-bind-program-eq-gen,
Id_wf,
hdataflow_wf,
hdf-bind_wf,
squash_wf,
valueall-type_wf,
hdf-parallel_wf,
hdf-compose1_wf,
union-valueall-type,
hdf-union-eq-disju,
iff_weakening_equal,
equal_wf,
hdf-union_wf
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)].
(X1 >>= Y1 || X2 >>= Y2 = X1 + X2 >>= \mlambda{}b.case b of inl(b1) => Y1 b1 | inr(b2) => Y2 b2) supposing
(valueall-type(C) and
valueall-type(B2) and
valueall-type(B1))
Date html generated:
2015_07_22-PM-00_05_58
Last ObjectModification:
2015_02_04-PM-05_09_21
Home
Index