---

Step * of Lemma hdf-until-halt-left

∀[Y:Top]. (hdf-until(hdf-halt();Y) ~ hdf-halt())
BY
{ (Auto THEN RepUR ``hdf-until`` 0 THEN RecUnfold `mk-hdf` 0⋅ THEN Reduce 0 THEN Auto) }

---

Latex:


\mforall{}[Y:Top].  (hdf-until(hdf-halt();Y)  \msim{}  hdf-halt())


By

(Auto  THEN  RepUR  ``hdf-until``  0  THEN  RecUnfold  `mk-hdf`  0\mcdot{}  THEN  Reduce  0  THEN  Auto)

---

Home Index