---

Step * of Lemma hdf-union-halt

hdf-halt() + hdf-halt() ~ hdf-halt()
BY
{ (RepUR ``hdf-union`` 0 THEN RecUnfold `mk-hdf` 0 THEN Reduce 0 THEN Auto) }

---

Latex:


hdf-halt()  +  hdf-halt()  \msim{}  hdf-halt()


By

(RepUR  ``hdf-union``  0  THEN  RecUnfold  `mk-hdf`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index