Nuprl Lemma : hdf-bind-compose1-left

[A,B,C,U:Type]. ∀[f:B ⟶ C]. ∀[X:hdataflow(A;B)]. ∀[Y:C ⟶ hdataflow(A;U)].
  (f X >>X >>f ∈ hdataflow(A;U)) supposing (valueall-type(C) and valueall-type(U))


Definitions occuring in Statement :  hdf-bind: X >>Y hdf-compose1: X hdataflow: hdataflow(A;B) compose: g valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a top: Top guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q

\mforall{}[A,B,C,U:Type].  \mforall{}[f:B  {}\mrightarrow{}  C].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[Y:C  {}\mrightarrow{}  hdataflow(A;U)].
    (f  o  X  >>=  Y  =  X  >>=  Y  o  f)  supposing  (valueall-type(C)  and  valueall-type(U))

Date html generated: 2016_05_16-AM-10_43_32
Last ObjectModification: 2015_12_28-PM-07_41_25

Theory : halting!dataflow

Home Index