Nuprl Lemma : hdf-bind_wf
∀[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:B ─→ hdataflow(A;C)].  X >>= Y ∈ hdataflow(A;C) supposing valueall-type(C)
Proof
Definitions occuring in Statement : 
hdf-bind: X >>= Y
, 
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
Lemmas : 
mk-hdf_wf, 
bag_wf, 
hdataflow_wf, 
empty-bag_wf, 
hdf-halted_wf, 
bool_wf, 
eqtt_to_assert, 
bag-null_wf, 
bind-nxt_wf, 
valueall-type_wf
\mforall{}[A,B,C:Type].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[Y:B  {}\mrightarrow{}  hdataflow(A;C)].
    X  >>=  Y  \mmember{}  hdataflow(A;C)  supposing  valueall-type(C)
Date html generated:
2015_07_17-AM-08_06_53
Last ObjectModification:
2015_01_27-PM-00_06_41
Home
Index