Nuprl Lemma : hdf-parallel-bind-eq

[A,B,C:Type]. ∀[X1,X2:hdataflow(A;B)]. ∀[X:B ─→ hdataflow(A;C)].
  (X1 >>|| X2 >>X1 || X2 >>X ∈ hdataflow(A;C)) supposing (valueall-type(C) and valueall-type(B))


Definitions occuring in Statement :  valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] function: x:A ─→ B[x] universe: Type equal: t ∈ T hdf-bind: X >>Y hdf-parallel: || Y hdataflow: hdataflow(A;B)
Lemmas :  parallel-bind-program-eq Id_wf hdataflow_wf eta_conv iff_weakening_equal and_wf equal_wf hdf-bind_wf hdf-parallel_wf squash_wf valueall-type_wf

\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: 2015_07_22-PM-00_05_56
Last ObjectModification: 2015_02_04-PM-05_09_19

Home Index