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