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