Nuprl Lemma : hdf-bind-gen-halt-left
∀[Y:Top]. (hdf-halt() ({}) >>= Y ~ hdf-halt())
Proof
Definitions occuring in Statement :
hdf-bind-gen: X (hdfs) >>= Y,
hdf-halt: hdf-halt(),
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t,
empty-bag: {}
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
hdf-bind-gen: X (hdfs) >>= Y,
bind-nxt: bind-nxt(Y;p;a),
mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0),
all: ∀x:A. B[x],
top: Top,
btrue: tt,
band: p ∧b q,
ifthenelse: if b then t else f fi
Latex:
\mforall{}[Y:Top]. (hdf-halt() (\{\}) >>= Y \msim{} hdf-halt())
Date html generated:
2016_05_16-AM-10_43_01
Last ObjectModification:
2015_12_28-PM-07_42_58
Theory : halting!dataflow
Home
Index