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: {}
Lemmas :
hdf_halted_halt_red_lemma,
bag_null_empty_lemma,
hdf_ap_halt_lemma,
empty_bag_append_lemma,
bag_map_empty_lemma,
top_wf
\mforall{}[Y:Top]. (hdf-halt() (\{\}) >>= Y \msim{} hdf-halt())
Date html generated:
2015_07_17-AM-08_06_59
Last ObjectModification:
2015_01_27-PM-00_06_39
Home
Index