Nuprl Lemma : hdf-halt-compose2
∀[X:Top]. (hdf-halt() o X ~ hdf-halt())
Proof
Definitions occuring in Statement :
hdf-compose2: X o Y,
hdf-halt: hdf-halt(),
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Lemmas :
hdf_halted_halt_red_lemma,
hdf_ap_halt_lemma,
bag_combine_empty_lemma,
top_wf
\mforall{}[X:Top]. (hdf-halt() o X \msim{} hdf-halt())
Date html generated:
2015_07_17-AM-08_05_35
Last ObjectModification:
2015_01_27-PM-00_15_38
Home
Index